Still annotating the kernel
authorZach Anderson <zra@zra-intrepid.(none)>
Mon, 17 Aug 2009 03:50:25 +0000 (20:50 -0700)
committerZach Anderson <zra@zra-intrepid.(none)>
Mon, 17 Aug 2009 03:50:25 +0000 (20:50 -0700)
21 files changed:
kern/arch/i386/arch.h
kern/arch/i386/pmap.c
kern/arch/i386/trap.c
kern/arch/i386/types.h
kern/include/multiboot.h
kern/include/pmap.h
kern/include/ros/error.h
kern/include/ros/memlayout.h
kern/include/stdio.h
kern/include/string.h
kern/include/sys/queue.h
kern/include/trap.h
kern/src/multiboot.c
kern/src/pmap.c
kern/src/printf.c
kern/src/printfmt.c
kern/src/readline.c
kern/src/smp.c
kern/src/string.c
kern/src/syscall.c
user/apps/parlib/file_io.c

index cfa69f7..135dedc 100644 (file)
@@ -10,7 +10,7 @@
 #define MAX_NUM_CPUS                           255
 
 static __inline void breakpoint(void) __attribute__((always_inline));
-static __inline void invlpg(void *addr) __attribute__((always_inline));
+static __inline void invlpg(void *SNT addr) __attribute__((always_inline));
 static __inline void tlbflush(void) __attribute__((always_inline));
 static __inline uint64_t read_tsc(void) __attribute__((always_inline));
 static __inline uint64_t read_tsc_serialized(void) __attribute__((always_inline));
index 3fe73eb..c988786 100644 (file)
@@ -17,6 +17,7 @@
 // These variables are set in i386_vm_init()
 pde_t* boot_pgdir;             // Virtual address of boot time page directory
 physaddr_t boot_cr3;           // Physical address of boot time page directory
+char *boot_freemem_base;
 char* boot_freemem;            // Pointer to next byte of free mem
 
 page_t *pages;         // Virtual address of physical page array
index d0bd5ea..13439d5 100644 (file)
@@ -1,6 +1,3 @@
-#ifdef __DEPUTY__
-#pragma noasync
-#endif
 
 #include <arch/mmu.h>
 #include <arch/x86.h>
@@ -32,7 +29,7 @@ pseudodesc_t idt_pd = {
  * of functions to be called when servicing an interrupt.  other cores
  * can set up their own later.
  */
-handler_t interrupt_handlers[NUM_INTERRUPT_HANDLERS];
+handler_t TP(void *) interrupt_handlers[NUM_INTERRUPT_HANDLERS];
 
 static const char *NTS (IN_HANDLER trapname)(int trapno)
 {
@@ -251,7 +248,7 @@ void
        extern handler_wrapper_t handler_wrappers[NUM_HANDLER_WRAPPERS];
 
        // determine the interrupt handler table to use.  for now, pick the global
-       handler_t* handler_tbl = interrupt_handlers;
+       handler_t TP(void *) * handler_tbl = interrupt_handlers;
 
        if (handler_tbl[tf->tf_trapno].isr != 0)
                handler_tbl[tf->tf_trapno].isr(tf, handler_tbl[tf->tf_trapno].data);
@@ -272,7 +269,7 @@ void
 }
 
 void
-register_interrupt_handler(handler_t table[], uint8_t int_num, isr_t handler,
+register_interrupt_handler(handler_t TP(TV(t)) table[], uint8_t int_num, poly_isr_t handler,
                            void* data)
 {
        table[int_num].isr = handler;
index 0e65d64..649ddf5 100644 (file)
@@ -82,6 +82,20 @@ typedef int32_t off_t;
        (typeof(a)) (ROUNDDOWN((uint32_t) (a) + __n - 1, __n)); \
 })
 
+
+// Round down to the nearest multiple of n
+#define PTRROUNDDOWN(a, n)                                             \
+({                                                             \
+       char * __a = (char *) (a);                              \
+       (typeof(a)) (__a - (uint32_t)__a % (n));                                \
+})
+// Round pointer up to the nearest multiple of n
+#define PTRROUNDUP(a, n)                                               \
+({                                                             \
+       uint32_t __n = (uint32_t) (n);                          \
+       (typeof(a)) (PTRROUNDDOWN((char *) (a) + __n - 1, __n));        \
+})
+
 // Return the offset of 'member' relative to the beginning of a struct type
 #ifndef offsetof
 #define offsetof(type, member)  ((size_t) (&((type*)0)->member))
index 9aff3d3..fc7e055 100644 (file)
@@ -7,6 +7,7 @@
 
 extern physaddr_t maxpa;// Maximum physical address
 extern physaddr_t maxaddrpa;    // Maximum directly addressable physical address
+extern void *SNT maxaddrpa_ptr; // same as maxaddrpa, but ptr type for annotations
 extern size_t npage;   // Amount of physical memory (in pages)
 extern size_t naddrpage;       // Amount of addressable physical memory (in pages)
 
index 90fc5af..e832918 100644 (file)
@@ -74,7 +74,8 @@ extern size_t npage;
 extern physaddr_t boot_cr3;
 extern pde_t *COUNT(NPDENTRIES) boot_pgdir;
 
-extern char* boot_freemem;
+extern char (SNT end)[];
+extern char*BND(end, maxaddrpa_ptr + IVY_KERNBASE) boot_freemem;
 extern page_list_t page_free_list;
 
 void*  (DALLOC(n) boot_alloc)(uint32_t n, uint32_t align);
@@ -87,20 +88,20 @@ void        vm_init(void);
 
 void   page_init(void);
 void   page_check(void);
-int        page_alloc(page_t **pp_store);
-int     page_alloc_specific(page_t **pp_store, size_t ppn);
-void   page_free(page_t *pp);
+int        page_alloc(page_t *COUNT(1) *pp_store);
+int     page_alloc_specific(page_t *COUNT(1) *pp_store, size_t ppn);
+void   page_free(page_t *COUNT(1) pp);
 int            page_is_free(size_t ppn);
 int        page_insert(pde_t *COUNT(NPDENTRIES) pgdir, page_t *pp, void *SNT va, int perm);
-void*   page_insert_in_range(pde_t *COUNT(NPDENTRIES) pgdir, page_t *pp, 
+void*COUNT(PGSIZE) page_insert_in_range(pde_t *COUNT(NPDENTRIES) pgdir, page_t *pp, 
                              void *SNT vab, void *SNT vae, int perm);
 void   page_remove(pde_t *COUNT(NPDENTRIES) pgdir, void *SNT va);
-page_t* page_lookup(pde_t *COUNT(NPDENTRIES) pgdir, void *SNT va, pte_t **pte_store);
+page_t*COUNT(1) page_lookup(pde_t *COUNT(NPDENTRIES) pgdir, void *SNT va, pte_t **pte_store);
 error_t        pagetable_remove(pde_t *COUNT(NPDENTRIES) pgdir, void *SNT va);
-void   page_decref(page_t *pp);
+void   page_decref(page_t *COUNT(1) pp);
 
 void setup_default_mtrrs(barrier_t* smp_barrier);
-void   tlb_invalidate(pde_t *COUNT(NPDENTRIES) pgdir, void *va);
+void   tlb_invalidate(pde_t *COUNT(NPDENTRIES) pgdir, void *SNT va);
 void tlb_flush_global(void);
 
 void *COUNT(len)
@@ -113,7 +114,7 @@ error_t
 memcpy_from_user(env_t* env, void* COUNT(len) dest,
                  const void *DANGEROUS va, size_t len);
 
-static inline page_t* ppn2page(size_t ppn)
+static inline page_t*COUNT(1) ppn2page(size_t ppn)
 {
        if( ppn >= npage )
                warn("ppn2page called with ppn (%08u) larger than npage", ppn);
@@ -130,7 +131,7 @@ static inline physaddr_t page2pa(page_t *pp)
        return page2ppn(pp) << PGSHIFT;
 }
 
-static inline page_t* pa2page(physaddr_t pa)
+static inline page_t*COUNT(1) pa2page(physaddr_t pa)
 {
        if (PPN(pa) >= npage)
                warn("pa2page called with pa (0x%08x) larger than npage", pa);
index 6c34999..6885ed8 100644 (file)
@@ -28,7 +28,7 @@ typedef enum {
  * so that -ENOMEM and ENOMEM are equivalent.
  */
 
-static const char * const error_string[NUMERRORS] =
+static const char *NTS const error_string[NUMERRORS] =
 {
        "Success",
        "Generic Failure",
index 88eb8c7..d40ab7e 100644 (file)
@@ -79,6 +79,9 @@
 // All physical memory mapped at this address
 #define        KERNBASE        0xC0000000
 
+// Use this if needed in annotations
+#define IVY_KERNBASE (0xC000U << 16)
+
 // At IOPHYSMEM (640K) there is a 384K hole for I/O.  From the kernel,
 // IOPHYSMEM can be addressed at KERNBASE + IOPHYSMEM.  The hole ends
 // at physical address EXTPHYSMEM.
index 06972b0..8d2e6ae 100644 (file)
@@ -22,22 +22,26 @@ int getchar(void);
 int    iscons(int fd);
 
 // lib/printfmt.c
+#ifdef __DEPUTY__
+void   printfmt(void (*putch)(int, TV(t)), TV(t) putdat, const char *NTS fmt, ...);
+void   vprintfmt(void (*putch)(int, TV(t)), TV(t) putdat, const char *NTS fmt, va_list);
+#else
 void   printfmt(void (*putch)(int, void**), void **putdat, const char *NTS fmt, ...);
-//void vprintfmt(void (*putch)(int, TV(t)), TV(t) putdat, const char *NTS fmt, va_list);
 void   vprintfmt(void (*putch)(int, void**), void **putdat, const char *NTS fmt, va_list);
+#endif
 
 // lib/printf.c
 int    cprintf(const char * NTS fmt, ...);
 int    vcprintf(const char * NTS fmt, va_list);
 
 // lib/sprintf.c
-int    snprintf(char *str, int size, const char *fmt, ...);
-int    vsnprintf(char *COUNT(size) str, int size, const char *fmt, va_list);
+int    snprintf(char *COUNT(size) str, int size, const char *NTS fmt, ...);
+int    vsnprintf(char *COUNT(size) str, int size, const char *NTS fmt, va_list);
 
 // lib/fprintf.c
-int    printf(const char *fmt, ...);
-int    fprintf(int fd, const char *fmt, ...);
-int    vfprintf(int fd, const char *fmt, va_list);
+int    printf(const char *NTS fmt, ...);
+int    fprintf(int fd, const char *NTS fmt, ...);
+int    vfprintf(int fd, const char *NTS fmt, va_list);
 
 // lib/readline.c
 char *NTS readline(const char *NTS prompt);
index b1ca2ab..c8eb281 100644 (file)
@@ -3,26 +3,28 @@
 
 #include <arch/types.h>
 
-#define STRING char *NTS NONNULL
-#define STRBUF(n) char *NT COUNT(n) NONNULL
+#define STRING char *NTS
+#define STRBUF(n) char *NT COUNT(n)
 
 int    strlen(const STRING s);
 int    strnlen(const STRBUF(size) s, size_t size);
-char * strcpy(STRING dst, const STRING src);
-char * strcat(char *dst, const char *src);
-char * strncpy(STRBUF(size) dst, const STRING src, size_t size);
+/* zra : These being used, and they are dangerous, so I'm rm'ing them
+STRING strcpy(STRING dst, const STRING src);
+STRING strcat(STRING dst, const STRING src);
+*/
+STRING strncpy(STRBUF(size) dst, const STRING src, size_t size);
 size_t strlcpy(STRBUF(size-1) dst, const STRING src, size_t size);
 int    strcmp(const STRING s1, const STRING s2);
 int    strncmp(const STRING s1, const STRING s2, size_t size);
-char * strchr(const STRING s, char c);
-char * strfind(const STRING s, char c);
+STRING strchr(const STRING s, char c);
+STRING strfind(const STRING s, char c);
 
-void * memset(void *COUNT(len) dst, int c, size_t len);
-void * memcpy(void *COUNT(len) dst, const void *COUNT(len) src, size_t len);
-void * memmove(void *COUNT(len) dst, const void *COUNT(len) src, size_t len);
+void *COUNT(len) memset(void *COUNT(len) dst, int c, size_t len);
+void *COUNT(len) memcpy(void *COUNT(len) dst, const void *COUNT(len) src, size_t len);
+void *COUNT(len) memmove(void *COUNT(len) dst, const void *COUNT(len) src, size_t len);
 int    memcmp(const void *COUNT(len) s1, const void *COUNT(len) s2, size_t len);
-void * memfind(const void *COUNT(len) s, int c, size_t len);
+void *BND(s,s+len)     memfind(const void *COUNT(len) s, int c, size_t len);
 
-long   strtol(const char *s, char **endptr, int base);
+long   strtol(const char *NTS s, char **endptr, int base);
 
 #endif /* not ROS_INC_STRING_H */
index 205adf0..3dfa6ca 100644 (file)
@@ -273,7 +273,7 @@ struct {                                                            \
  */
 #define        LIST_HEAD(name, type)                                           \
 struct name {                                                          \
-       struct type *SAFE lh_first;     /* first element */                     \
+       struct type *COUNT(1) lh_first; /* first element */                     \
 }
 
 #define        LIST_HEAD_INITIALIZER(head)                                     \
@@ -281,8 +281,8 @@ struct name {                                                               \
 
 #define        LIST_ENTRY(type)                                                \
 struct {                                                               \
-       struct type *le_next NOINIT;    /* next element */                      \
-       struct type **le_prev NOINIT;   /* address of previous next element */  \
+       struct type *COUNT(1) le_next NOINIT;   /* next element */                      \
+       struct type *COUNT(1) *le_prev NOINIT;  /* address of previous next element */  \
 }
 
 /*
index db2792f..455bbb8 100644 (file)
@@ -13,8 +13,8 @@
 typedef void (*poly_isr_t)(trapframe_t* tf, TV(t) data);
 typedef void (*isr_t)(trapframe_t* tf, void * data);
 typedef struct InterruptHandler {
-       isr_t isr;
-       void* data;
+       poly_isr_t isr;
+       TV(t) data;
 } handler_t;
 
 void idt_init(void);
index 6c47bc6..dc6b6e4 100644 (file)
@@ -5,10 +5,6 @@
 #include <ros/memlayout.h>
 #include <stdio.h>
 
-#ifdef __DEPUTY__
-//#pragma nodeputy
-#endif
-
 #ifdef __i386__
 #include <arch/apic.h>
 #endif
@@ -16,6 +12,7 @@
 // These variables are set by i386_detect_memory()
 physaddr_t maxpa;// Maximum physical address
 physaddr_t maxaddrpa;    // Maximum directly addressable physical address
+void *SNT maxaddrpa_ptr;
 size_t npage;   // Amount of physical memory (in pages)
 size_t naddrpage;       // Amount of addressable physical memory (in pages)
 static size_t basemem;  // Amount of base memory (in bytes)
@@ -40,6 +37,7 @@ multiboot_detect_memory(multiboot_info_t *mbi)
        // IOAPIC - KERNBASE is the max amount of virtual addresses we can use
        // for the physical memory mapping (aka - the KERNBASE mapping)
        maxaddrpa = MIN(maxpa, IOAPIC_BASE - KERNBASE);
+       maxaddrpa_ptr = maxaddrpa;
 
        naddrpage = maxaddrpa / PGSIZE;
 
index f557714..62b5866 100644 (file)
@@ -1,7 +1,4 @@
 /* See COPYRIGHT for copyright information. */
-#ifdef __DEPUTY__
-#pragma nodeputy
-#endif
 
 #include <arch/arch.h>
 #include <arch/mmu.h>
@@ -28,7 +25,7 @@
 void*
 boot_alloc(uint32_t n, uint32_t align)
 {
-       extern char end[];
+       extern char (SNT end)[];
        void *v;
 
        // Initialize boot_freemem if this is the first time.
@@ -36,11 +33,12 @@ boot_alloc(uint32_t n, uint32_t align)
        // which points to the end of the kernel's bss segment -
        // i.e., the first virtual address that the linker
        // did _not_ assign to any kernel code or global variables.
-       if (boot_freemem == 0)
-               boot_freemem = end;
+       if (boot_freemem == 0) {
+               boot_freemem = TC(end);
+       }
 
        //      Step 1: round boot_freemem up to be aligned properly
-       boot_freemem = ROUNDUP(boot_freemem, align);
+       boot_freemem = PTRROUNDUP(boot_freemem, align);
 
        //      Step 2: save current value of boot_freemem as allocated chunk
        v = boot_freemem;
@@ -56,7 +54,7 @@ boot_alloc(uint32_t n, uint32_t align)
 void*
 boot_calloc(uint32_t _n, size_t sz, uint32_t align)
 {
-       extern char end[];
+       extern char (SNT end)[];
        uint32_t n = _n *sz;
        void *v;
 
@@ -66,10 +64,10 @@ boot_calloc(uint32_t _n, size_t sz, uint32_t align)
        // i.e., the first virtual address that the linker
        // did _not_ assign to any kernel code or global variables.
        if (boot_freemem == 0)
-               boot_freemem = end;
+               boot_freemem = TC(end);
 
        //      Step 1: round boot_freemem up to be aligned properly
-       boot_freemem = ROUNDUP(boot_freemem, align);
+       boot_freemem = PTRROUNDUP(boot_freemem, align);
 
        //      Step 2: save current value of boot_freemem as allocated chunk
        v = boot_freemem;
@@ -90,7 +88,7 @@ boot_calloc(uint32_t _n, size_t sz, uint32_t align)
 // Note that the corresponding physical page is NOT initialized!
 //
 static void
-page_initpp(page_t *pp)
+page_initpp(page_t *COUNT(1) pp)
 {
        memset(pp, 0, sizeof(*pp));
 }
@@ -107,7 +105,7 @@ page_initpp(page_t *pp)
  *   0         -- on success
  *   -ENOMEM   -- otherwise 
  */
-int page_alloc(page_t **pp_store)
+int page_alloc(page_t *COUNT(1) *pp_store)
 {
        if (LIST_EMPTY(&page_free_list))
                return -ENOMEM;
@@ -235,7 +233,7 @@ void* page_insert_in_range(pde_t *pgdir, page_t *pp,
                            void *vab, void *vae, int perm) 
 {
        pte_t* pte = NULL;
-       void* new_va;
+       void*SNT new_va;
        
        for(new_va = vab; new_va <= vae; new_va+= PGSIZE) {
                pte = pgdir_walk(pgdir, new_va, 1);
@@ -244,7 +242,7 @@ void* page_insert_in_range(pde_t *pgdir, page_t *pp,
        }
        if (!pte) return NULL;
        *pte = page2pa(pp) | PTE_P | perm;
-       return new_va;
+       return TC(new_va); // trusted because mapping a page is like allocation
 }
 
 //
@@ -351,8 +349,8 @@ user_mem_check(env_t *env, const void *DANGEROUS va, size_t len, int perm)
        pte_t *pte;
 
        perm |= PTE_P;
-       start = ROUNDDOWN((void*)va, PGSIZE);
-       end = ROUNDUP((void*)va + len, PGSIZE);
+       start = ROUNDDOWN((void*DANGEROUS)va, PGSIZE);
+       end = ROUNDUP((void*DANGEROUS)va + len, PGSIZE);
        if (start >= end) {
                warn("Blimey!  Wrap around in VM range calculation!");  
                return NULL;
@@ -363,7 +361,7 @@ user_mem_check(env_t *env, const void *DANGEROUS va, size_t len, int perm)
                // ensures the bits we want on are turned on.  if not, error out
                if ( !pte || ((*pte & perm) != perm) ) {
                        if (i = 0)
-                               user_mem_check_addr = (void*)va;
+                               user_mem_check_addr = (void*DANGEROUS)va;
                        else
                                user_mem_check_addr = start;
                        return NULL;
index 721954d..e870dca 100644 (file)
@@ -1,10 +1,6 @@
 // Simple implementation of cprintf console output for the kernel,
 // based on printfmt() and the kernel console's cputchar().
 
-#ifdef __DEPUTY__
-#pragma nodeputy
-#endif
-
 #include <arch/arch.h>
 #include <arch/types.h>
 
@@ -52,7 +48,7 @@ int vcprintf(const char *fmt, va_list ap)
        spin_lock_irqsave(&output_lock);
 
        // do the buffered printf
-       vprintfmt((void*)buffered_putch, (void**)&cntp, fmt, ap);
+       vprintfmt(buffered_putch, &cntp, fmt, ap);
 
        // write out remaining chars in the buffer
        buffered_putch(-1,&cntp);
index ff4104f..5d4fc83 100644 (file)
@@ -2,10 +2,6 @@
 // used in common by printf, sprintf, fprintf, etc.
 // This code is also used by both the kernel and user programs.
 
-#ifdef __DEPUTY__
-#pragma nodeputy
-#endif
-
 #include <arch/types.h>
 #include <ros/error.h>
 #include <stdio.h>
  * Print a number (base <= 16) in reverse order,
  * using specified putch function and associated pointer putdat.
  */
+#ifdef __DEPUTY__
+void printnum(void (*putch)(int, TV(t)), TV(t) putdat,
+                        unsigned long long num, unsigned base, int width, int padc)
+#else
 void printnum(void (*putch)(int, void**), void **putdat,
                         unsigned long long num, unsigned base, int width, int padc)
+#endif
 {
        // first recursively print all preceding (more significant) digits
        if (num >= base) {
@@ -58,24 +59,36 @@ static long long getint(va_list *ap, int lflag)
 
 
 // Main function to format and print a string.
+#ifdef __DEPUTY__
+void printfmt(void (*putch)(int, TV(t)), TV(t) putdat, const char *fmt, ...);
+#else
 void printfmt(void (*putch)(int, void**), void **putdat, const char *fmt, ...);
+#endif
 
+#ifdef __DEPUTY__
+void vprintfmt(void (*putch)(int, TV(t)), TV(t) putdat, const char *fmt, va_list ap)
+#else
 void vprintfmt(void (*putch)(int, void**), void **putdat, const char *fmt, va_list ap)
+#endif
 {
-       register const char *p;
+       register const char *NTS p;
+       const char *NTS last_fmt;
        register int ch, err;
        unsigned long long num;
        int base, lflag, width, precision, altflag;
        char padc;
 
        while (1) {
-               while ((ch = *(unsigned char *) fmt++) != '%') {
+               while ((ch = *(unsigned char *) fmt) != '%') {
                        if (ch == '\0')
                                return;
+                       fmt++;
                        putch(ch, putdat);
                }
+               fmt++;
 
                // Process a %-escape sequence
+               last_fmt = fmt;
                padc = ' ';
                width = -1;
                precision = -1;
@@ -158,11 +171,14 @@ void vprintfmt(void (*putch)(int, void**), void **putdat, const char *fmt, va_li
                        if (width > 0 && padc != '-')
                                for (width -= strnlen(p, precision); width > 0; width--)
                                        putch(padc, putdat);
-                       for (; (ch = *p++) != '\0' && (precision < 0 || --precision >= 0); width--)
+                       for (; (ch = *p) != '\0' && (precision < 0 || --precision >= 0); width--) {
                                if (altflag && (ch < ' ' || ch > '~'))
                                        putch('?', putdat);
                                else
                                        putch(ch, putdat);
+                               // zra: make sure *p isn't '\0' before inc'ing
+                               p++;
+                       }
                        for (; width > 0; width--)
                                putch(' ', putdat);
                        break;
@@ -215,14 +231,19 @@ void vprintfmt(void (*putch)(int, void**), void **putdat, const char *fmt, va_li
                // unrecognized escape sequence - just print it literally
                default:
                        putch('%', putdat);
-                       for (fmt--; fmt[-1] != '%'; fmt--)
+                       fmt = last_fmt;
+                       //for (fmt--; fmt[-1] != '%'; fmt--)
                                /* do nothing */;
                        break;
                }
        }
 }
 
+#ifdef __DEPUTY__
+void printfmt(void (*putch)(int, TV(t)), TV(t) putdat, const char *fmt, ...)
+#else
 void printfmt(void (*putch)(int, void**), void **putdat, const char *fmt, ...)
+#endif
 {
        va_list ap;
 
@@ -232,12 +253,12 @@ void printfmt(void (*putch)(int, void**), void **putdat, const char *fmt, ...)
 }
 
 typedef struct sprintbuf {
-       char *buf;
-       char *ebuf;
+       char *BND(__this,ebuf) buf;
+       char *SNT ebuf;
        int cnt;
 } sprintbuf_t;
 
-static void sprintputch(int ch, sprintbuf_t **b)
+static void sprintputch(int ch, sprintbuf_t *NONNULL *NONNULL b)
 {
        (*b)->cnt++;
        if ((*b)->buf < (*b)->ebuf)
@@ -246,14 +267,19 @@ static void sprintputch(int ch, sprintbuf_t **b)
 
 int vsnprintf(char *buf, int n, const char *fmt, va_list ap)
 {
-       sprintbuf_t b = {buf, buf+n-1, 0};
-       sprintbuf_t *bp = &b;
+       sprintbuf_t b;// = {buf, buf+n-1, 0};
+       sprintbuf_t *COUNT(1) NONNULL bp = &b;
 
        if (buf == NULL || n < 1)
                return -EINVAL;
 
+       b.buf = NULL; // zra : help out the Deputy optimizer a bit
+       b.ebuf = buf+n-1;
+       b.cnt = 0;
+       b.buf = buf;
+
        // print the string to the buffer
-       vprintfmt((void*)sprintputch, (void**)&bp, fmt, ap);
+       vprintfmt(sprintputch, (sprintbuf_t *NONNULL*NONNULL)&bp, fmt, ap);
 
        // null terminate the buffer
        *b.buf = '\0';
index 505f0cb..71a46c6 100644 (file)
@@ -1,12 +1,9 @@
-#ifdef __DEPUTY__
-#pragma nodeputy
-#endif
 
 #include <ros/error.h>
 #include <stdio.h>
 
 #define BUFLEN 1024
-static char buf[BUFLEN];
+static char (NT buf)[BUFLEN];
 
 char *
 readline(const char *prompt)
index 62573ac..c1cdc0e 100644 (file)
@@ -4,10 +4,6 @@
  * See LICENSE for details.
  */
 
-#ifdef __DEPUTY__
-#pragma nodeputy
-#endif
-
 #include <arch/arch.h>
 #include <atomic.h>
 #include <smp.h>
index bb72872..3ee27ca 100644 (file)
@@ -1,9 +1,5 @@
 // Basic string routines.  Not hardware optimized, but not shabby.
 
-#ifdef __DEPUTY__
-#pragma nodeputy
-#endif
-
 #include <string.h>
 
 int
@@ -26,6 +22,7 @@ strnlen(const char *s, size_t size)
        return n;
 }
 
+/* zra: These aren't being used, and they are dangerous, so I'm rm'ing them
 char *
 strcpy(char *dst, const char *src)
 {
@@ -33,7 +30,7 @@ strcpy(char *dst, const char *src)
 
        ret = dst;
        while ((*dst++ = *src++) != '\0')
-               /* do nothing */;
+               ;
        return ret;
 }
 
@@ -43,6 +40,7 @@ strcat(char *dst, const char *src)
        strcpy(dst+strlen(dst),src);
        return dst;
 }
+*/
 
 char *
 strncpy(char *dst, const char *src, size_t size) {
@@ -116,12 +114,14 @@ strfind(const char *s, char c)
 
 // n must be a multiple of 16 and v must be uint32_t-aligned
 static inline void *
-memset16(uint32_t *v, uint32_t c, size_t n)
+memset16(uint32_t *COUNT(n/sizeof(uint32_t)) _v, uint32_t c, size_t n)
 {
        uint32_t *start, *end;
+       uint32_t *BND(_v, end) v;
 
-       start = v;
-       end = v + n/sizeof(uint32_t);
+       start = _v;
+       end = _v + n/sizeof(uint32_t);
+       v = _v;
        c = c | c<<8 | c<<16 | c<<24;
 
        while(v < end)
@@ -136,14 +136,20 @@ memset16(uint32_t *v, uint32_t c, size_t n)
 // n must be a multiple of 16 and v must be 4-byte aligned.
 // as allowed by ISO, behavior undefined if dst/src overlap
 static inline void *
-memcpy16(uint32_t* dst, const uint32_t* src, size_t n)
+memcpy16(uint32_t *COUNT(n/sizeof(uint32_t)) _dst,
+         const uint32_t *COUNT(n/sizeof(uint32_t)) _src, size_t n)
 {
-       uint32_t *dststart, *dstend;
+       uint32_t *dststart, *dstend, *srcend;
+       uint32_t *BND(_dst,dstend) dst;
+       uint32_t *BND(_src,srcend) src;
 
-       dststart = dst;
-       dstend = dst + n/sizeof(uint32_t);
+       dststart = _dst;
+       dstend = _dst + n/sizeof(uint32_t);
+       srcend = _src + n/sizeof(uint32_t);
+       dst = _dst;
+       src = _src;
 
-       while(dst < dstend)
+       while(dst < dstend && src < srcend)
        {
                dst[0] = src[0];
                dst[1] = src[1];
@@ -158,10 +164,13 @@ memcpy16(uint32_t* dst, const uint32_t* src, size_t n)
 }
 
 void *
-memset(void *v, int c, size_t n)
+memset(void *v, int c, size_t _n)
 {
-       char *p;
+       char *BND(v,v+_n) p;
        size_t n0;
+       size_t n = _n;
+
+       if (n == 0) return NULL; // zra: complain here?
 
        p = v;
 
@@ -183,11 +192,12 @@ memset(void *v, int c, size_t n)
 }
 
 void *
-memcpy(void *dst, const void *src, size_t n)
+memcpy(void *dst, const void *src, size_t _n)
 {
-       const char *s;
-       char *d;
+       const char *BND(src,src+_n) s;
+       char *BND(dst,dst+_n) d;
        size_t n0;
+       size_t n = _n;
 
        s = src;
        d = dst;
@@ -208,10 +218,11 @@ memcpy(void *dst, const void *src, size_t n)
 }
 
 void *
-memmove(void *dst, const void *src, size_t n)
+memmove(void *dst, const void *src, size_t _n)
 {
-       const char *s;
-       char *d;
+       const char *BND(src,src+_n) s;
+       char *BND(dst,dst+_n) d;
+       size_t n = _n;
        
        s = src;
        d = dst;
@@ -230,8 +241,8 @@ memmove(void *dst, const void *src, size_t n)
 int
 memcmp(const void *v1, const void *v2, size_t n)
 {
-       const uint8_t *s1 = (const uint8_t *) v1;
-       const uint8_t *s2 = (const uint8_t *) v2;
+       const uint8_t *BND(v1,v1+n) s1 = (const uint8_t *) v1;
+       const uint8_t *BND(v2,v2+n) s2 = (const uint8_t *) v2;
 
        while (n-- > 0) {
                if (*s1 != *s2)
@@ -243,9 +254,10 @@ memcmp(const void *v1, const void *v2, size_t n)
 }
 
 void *
-memfind(const void *s, int c, size_t n)
+memfind(const void *_s, int c, size_t n)
 {
-       const void *ends = (const char *) s + n;
+       const void *SNT ends = (const char *) _s + n;
+       const void *BND(_s,_s + n) s = _s;
        for (; s < ends; s++)
                if (*(const unsigned char *) s == (unsigned char) c)
                        break;
index 20cdda0..e4bda71 100644 (file)
@@ -57,7 +57,7 @@ static ssize_t sys_serial_read(env_t* e, char *DANGEROUS buf, size_t len)
 }
 
 static ssize_t sys_shared_page_alloc(env_t* p1,
-                                     void** addr, envid_t p2_id,
+                                     void**DANGEROUS addr, envid_t p2_id,
                                      int p1_flags, int p2_flags
                                     )
 {
@@ -84,7 +84,7 @@ static ssize_t sys_shared_page_alloc(env_t* p1,
        return ESUCCESS;
 }
 
-static void sys_shared_page_free(env_t* p1, void* addr, envid_t p2)
+static void sys_shared_page_free(env_t* p1, void*DANGEROUS addr, envid_t p2)
 {
 }
 
index 069385a..22ae07e 100644 (file)
@@ -29,8 +29,9 @@ void file_io()
                return;
        }
 
-       char * file_name = malloc(strlen(readline_result) + 1);
-       strcpy(file_name, readline_result);
+    unsigned int fname_len = strlen(readline_result) + 1;
+       char * file_name = malloc(fname_len);
+       strncpy(file_name, readline_result, fname_len);
 
        readline_result = readline("Enter text to write to file: ");
 
@@ -40,12 +41,14 @@ void file_io()
         }
 
 
-       char *buf2 = malloc(strlen(readline_result) + 1);
-       strcpy(buf2, readline_result);
+       unsigned int buf2_len = strlen(readline_result) + 1;
+       char *buf2 = malloc(buf2_len);
+       strncpy(buf2, readline_result, buf2_len);
 
 
-       char * output_full_path = malloc(strlen(file_name) + 8);
-       sprintf(output_full_path, "./test/%s", file_name);
+       unsigned int ofp_len = strlen(file_name) + 8;
+       char * output_full_path = malloc(ofp_len);
+       snprintf(output_full_path, ofp_len, "./test/%s", file_name);
 
        int out_fd = open(output_full_path, O_RDWR | O_CREAT | O_TRUNC,
                       S_IRUSR | S_IWUSR | S_IRGRP | S_IWGRP | S_IROTH);