[Libc] add spec and stub for posix_memalign

share/libc/stdlib.c

@@ -187,4 +187,19 @@ int unsetenv(const char *name)
 char __fc_strerror[64];
 #endif
 
+// Note: this implementation does not check the alignment, since it cannot
+//       currently be specified in the memory model of most plug-ins
+int posix_memalign(void **memptr, size_t alignment, size_t size) {
+  // By default, specifications in the libc are ignored for defined functions,
+  // and since we do not actually use alignment, we need to check its validity.
+  // The assertion below is the requires in the specification.
+  /*@ assert alignment_is_a_suitable_power_of_two:
+      alignment >= sizeof(void*) &&
+      ((size_t)alignment & ((size_t)alignment - 1)) == 0;
+  */
+  *memptr = malloc(size);
+  if (!*memptr) return ENOMEM;
+  return 0;
+}
+
 __POP_FC_STDLIB

share/libc/stdlib.h

@@ -594,6 +594,34 @@ extern size_t wcstombs(char * restrict s,
      size_t n);
 
 
+// Note: this specification should ideally use a more specific predicate,
+//       such as 'is_allocable_aligned(alignment, size)'.
+/*@
+  requires valid_memptr: \valid(memptr);
+  requires alignment_is_a_suitable_power_of_two:
+    alignment >= sizeof(void*) &&
+    ((size_t)alignment & ((size_t)alignment - 1)) == 0;
+  allocates *memptr;
+  assigns __fc_heap_status \from indirect:alignment, size, __fc_heap_status;
+  assigns \result \from indirect:alignment, indirect:size,
+                        indirect:__fc_heap_status;
+  behavior allocation:
+    assumes can_allocate: is_allocable(size);
+    assigns __fc_heap_status \from indirect:alignment, size, __fc_heap_status;
+    assigns \result \from indirect:alignment, indirect:size,
+                          indirect:__fc_heap_status;
+    ensures allocation: \fresh(*memptr,size);
+    ensures result_zero: \result == 0;
+  behavior no_allocation:
+    assumes cannot_allocate: !is_allocable(size);
+    assigns \result \from indirect:alignment;
+    allocates \nothing;
+    ensures result_non_zero: \result < 0 || \result > 0;
+  complete behaviors;
+  disjoint behaviors;
+ */
+extern int posix_memalign(void **memptr, size_t alignment, size_t size);
+
 __END_DECLS
 
 __POP_FC_STDLIB

src/plugins/value/utils/library_functions.ml

@@ -79,6 +79,7 @@ let unsupported_specifications =
     "strdup", "string.c";
     "strndup", "string.c";
     "getenv", "stdlib.c";
+    "posix_memalign", "stdlib.c";
     "putenv", "stdlib.c";
     "setenv", "stdlib.c";
     "unsetenv", "stdlib.c"

tests/libc/oracle/coverage.res.oracle

@@ -28,7 +28,7 @@
   main: 4 stmts out of 4 (100.0%)
 [metrics] Eva coverage statistics
   =======================
-  Syntactically reachable functions = 2 (out of 75)
+  Syntactically reachable functions = 2 (out of 76)
   Semantically reached functions = 2
   Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva

tests/libc/oracle/fc_libc.0.res.oracle

@@ -13,7 +13,7 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
-[metrics] Defined functions (73)
+[metrics] Defined functions (74)
   ======================
    Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
    Frama_C_interval (13 calls); Frama_C_nondet (11 calls);
@@ -28,14 +28,14 @@
    isprint (0 call); ispunct (0 call); isspace (1 call); isupper (0 call);
    isxdigit (0 call); localeconv (0 call); main (0 call); memchr (0 call);
    memcmp (0 call); memcpy (2 calls); memmove (0 call); memrchr (0 call);
-   memset (1 call); putenv (0 call); setenv (0 call); setlocale (0 call);
-   strcasecmp (0 call); strcat (0 call); strchr (3 calls); strcmp (0 call);
-   strcpy (0 call); strdup (0 call); strerror (0 call); strlen (6 calls);
-   strncat (0 call); strncmp (0 call); strncpy (0 call); strndup (0 call);
-   strnlen (0 call); strrchr (0 call); strstr (0 call); tolower (0 call);
-   toupper (0 call); unsetenv (0 call); wcscat (0 call); wcscpy (0 call);
-   wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
-   wmemset (0 call); 
+   memset (1 call); posix_memalign (0 call); putenv (0 call); setenv (0 call);
+   setlocale (0 call); strcasecmp (0 call); strcat (0 call); strchr (3 calls);
+   strcmp (0 call); strcpy (0 call); strdup (0 call); strerror (0 call);
+   strlen (6 calls); strncat (0 call); strncmp (0 call); strncpy (0 call);
+   strndup (0 call); strnlen (0 call); strrchr (0 call); strstr (0 call);
+   tolower (0 call); toupper (0 call); unsetenv (0 call); wcscat (0 call);
+   wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
+   wmemcpy (0 call); wmemset (0 call); 
   
   Undefined functions (360)
   =========================
@@ -104,7 +104,7 @@
    localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
    log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
    logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
-   malloc (6 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+   malloc (7 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
    memoverlap (1 call); mkdir (0 call); mktime (0 call); nan (0 call);
    nanf (0 call); nanl (0 call); nanosleep (0 call); ntohl (0 call);
    ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
@@ -162,18 +162,18 @@
   
   Global metrics
   ============== 
-  Sloc = 948
-  Decision point = 183
+  Sloc = 956
+  Decision point = 184
   Global variables = 58
-  If = 174
+  If = 175
   Loop = 40
-  Goto = 78
-  Assignment = 379
-  Exit point = 73
-  Function = 433
-  Function call = 73
-  Pointer dereferencing = 146
-  Cyclomatic complexity = 256
+  Goto = 79
+  Assignment = 382
+  Exit point = 74
+  Function = 434
+  Function call = 74
+  Pointer dereferencing = 148
+  Cyclomatic complexity = 258
 /* Generated by Frama-C */
 #include "__fc_builtin.c"
 #include "__fc_builtin.h"

tests/libc/oracle/fc_libc.1.res.oracle

@@ -1906,6 +1906,8 @@ extern size_t mbstowcs(wchar_t * __restrict pwcs, char const * __restrict s,
 extern size_t wcstombs(char * __restrict s, wchar_t const * __restrict pwcs,
                        size_t n);
 
+int posix_memalign(void **memptr, size_t alignment, size_t size);
+
 int glob(char const *pattern, int flags,
          int (*errfunc)(char const *epath, int eerrno), glob_t *pglob)
 {
@@ -4346,6 +4348,59 @@ int unsetenv(char const *name)
   return_label: return __retres;
 }
 
+/*@ requires valid_memptr: \valid(memptr);
+    requires
+      alignment_is_a_suitable_power_of_two:
+        alignment ≥ sizeof(void *) ∧
+        ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+    assigns __fc_heap_status, \result;
+    assigns __fc_heap_status
+      \from (indirect: alignment), size, __fc_heap_status;
+    assigns \result
+      \from (indirect: alignment), (indirect: size),
+            (indirect: __fc_heap_status);
+    allocates *\old(memptr);
+    
+    behavior allocation:
+      assumes can_allocate: is_allocable(size);
+      ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size));
+      ensures result_zero: \result ≡ 0;
+      assigns __fc_heap_status, \result;
+      assigns __fc_heap_status
+        \from (indirect: alignment), size, __fc_heap_status;
+      assigns \result
+        \from (indirect: alignment), (indirect: size),
+              (indirect: __fc_heap_status);
+    
+    behavior no_allocation:
+      assumes cannot_allocate: ¬is_allocable(size);
+      ensures result_non_zero: \result < 0 ∨ \result > 0;
+      assigns \result;
+      assigns \result \from (indirect: alignment);
+      allocates \nothing;
+    
+    complete behaviors no_allocation, allocation;
+    disjoint behaviors no_allocation, allocation;
+ */
+int posix_memalign(void **memptr, size_t alignment, size_t size)
+{
+  int __retres;
+  /*@
+  assert
+  alignment_is_a_suitable_power_of_two:
+    alignment ≥ sizeof(void *) ∧
+    ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+   */
+  ;
+  *memptr = malloc(size);
+  if (! *memptr) {
+    __retres = 12;
+    goto return_label;
+  }
+  __retres = 0;
+  return_label: return __retres;
+}
+
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
     requires

tests/libc/oracle/stdlib_c.0.res.oracle

@@ -76,9 +76,42 @@
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32'
   (0..31/34359738367) to fit 0..63/34359738367
+[eva] computing for function posix_memalign <- main.
+  Called from tests/libc/stdlib_c.c:37.
+[eva] share/libc/stdlib.c:197: 
+  assertion 'alignment_is_a_suitable_power_of_two' got status valid.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+  Called from tests/libc/stdlib_c.c:38.
+[eva] using specification for function free
+[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:38: 
+  function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function posix_memalign <- main.
+  Called from tests/libc/stdlib_c.c:39.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: 
+  allocating variable __malloc_posix_memalign_l200_0
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+  Called from tests/libc/stdlib_c.c:40.
+[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:40: 
+  function free: precondition 'freeable' got status valid.
+[eva] Done for function free
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function posix_memalign:
+  __fc_heap_status ∈ [--..--]
+  p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
+  p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+  __retres ∈ {0; 12}
 [eva:final-states] Values at end of function main:
   __fc_heap_status ∈ [--..--]
   Frama_C_entropy_source ∈ [--..--]
@@ -87,5 +120,9 @@
   q ∈ {{ NULL ; &__calloc_main_l21[0] }}
   r ∈ {0}
   s ∈ {{ NULL ; &__calloc_w_main_l32[0] }}
+  p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
+  p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }}
+  p_memal_res ∈ {0; 12}
+  p_memal_res2 ∈ {0; 12}
   __retres ∈ {0}
   __calloc_w_main_l32[0..1073741823] ∈ {0; 42}

tests/libc/oracle/stdlib_c.1.res.oracle

@@ -95,9 +95,42 @@
 [eva:malloc] tests/libc/stdlib_c.c:32: 
   resizing variable `__calloc_w_main_l32'
   (0..31/34359738367) to fit 0..191/34359738367
+[eva] computing for function posix_memalign <- main.
+  Called from tests/libc/stdlib_c.c:37.
+[eva] share/libc/stdlib.c:197: 
+  assertion 'alignment_is_a_suitable_power_of_two' got status valid.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+  Called from tests/libc/stdlib_c.c:38.
+[eva] using specification for function free
+[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:38: 
+  function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function posix_memalign <- main.
+  Called from tests/libc/stdlib_c.c:39.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: 
+  allocating variable __malloc_posix_memalign_l200_0
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+  Called from tests/libc/stdlib_c.c:40.
+[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:40: 
+  function free: precondition 'freeable' got status valid.
+[eva] Done for function free
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function posix_memalign:
+  __fc_heap_status ∈ [--..--]
+  p_al0 ∈ {{ &__malloc_posix_memalign_l200[0] }}
+  p_al1 ∈ {{ &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+  __retres ∈ {0}
 [eva:final-states] Values at end of function main:
   __fc_heap_status ∈ [--..--]
   Frama_C_entropy_source ∈ [--..--]
@@ -106,5 +139,9 @@
   q ∈ {{ NULL ; &__calloc_main_l21[0] }}
   r ∈ {0}
   s ∈ {{ NULL ; &__calloc_w_main_l32[0] }}
+  p_al0 ∈ {{ &__malloc_posix_memalign_l200[0] }}
+  p_al1 ∈ {{ &__malloc_posix_memalign_l200_0[0] }}
+  p_memal_res ∈ {0}
+  p_memal_res2 ∈ {0}
   __retres ∈ {0}
   __calloc_w_main_l32[0..1073741823] ∈ {0; 42}

tests/libc/oracle/stdlib_c.2.res.oracle

@@ -94,6 +94,34 @@
 [eva] Done for function memset
 [eva] Recording results for calloc
 [eva] Done for function calloc
+[eva] computing for function posix_memalign <- main.
+  Called from tests/libc/stdlib_c.c:37.
+[eva] share/libc/stdlib.c:197: 
+  assertion 'alignment_is_a_suitable_power_of_two' got status valid.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: allocating variable __malloc_posix_memalign_l200
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+  Called from tests/libc/stdlib_c.c:38.
+[eva] using specification for function free
+[eva] tests/libc/stdlib_c.c:38: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:38: 
+  function free: precondition 'freeable' got status valid.
+[eva] Done for function free
+[eva] computing for function posix_memalign <- main.
+  Called from tests/libc/stdlib_c.c:39.
+[eva] share/libc/stdlib.c:200: Call to builtin Frama_C_malloc_by_stack
+[eva] share/libc/stdlib.c:200: 
+  allocating variable __malloc_posix_memalign_l200_0
+[eva] Recording results for posix_memalign
+[eva] Done for function posix_memalign
+[eva] computing for function free <- main.
+  Called from tests/libc/stdlib_c.c:40.
+[eva] tests/libc/stdlib_c.c:40: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/stdlib_c.c:40: 
+  function free: precondition 'freeable' got status valid.
+[eva] Done for function free
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -110,6 +138,11 @@
   __malloc_calloc_l72[0..3] ∈ [--..--] or UNINITIALIZED
   __malloc_calloc_l72_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
   __malloc_w_calloc_l72_1[0..4294967291] ∈ [--..--] or UNINITIALIZED
+[eva:final-states] Values at end of function posix_memalign:
+  __fc_heap_status ∈ [--..--]
+  p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
+  p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }} or UNINITIALIZED
+  __retres ∈ {0; 12}
 [eva:final-states] Values at end of function main:
   __fc_heap_status ∈ [--..--]
   Frama_C_entropy_source ∈ [--..--]
@@ -118,6 +151,10 @@
   q ∈ {{ NULL ; (int *)&__malloc_calloc_l72_0 }}
   r ∈ {0}
   s ∈ {{ NULL ; (int *)&__malloc_w_calloc_l72_1 }} or UNINITIALIZED
+  p_al0 ∈ {{ NULL ; &__malloc_posix_memalign_l200[0] }}
+  p_al1 ∈ {{ NULL ; &__malloc_posix_memalign_l200_0[0] }}
+  p_memal_res ∈ {0; 12}
+  p_memal_res2 ∈ {0; 12}
   __retres ∈ {0}
   __malloc_calloc_l72[0..3] ∈ [--..--] or UNINITIALIZED
   __malloc_calloc_l72_0[0..4294967291] ∈ [--..--] or UNINITIALIZED

tests/libc/stdlib_c.c

@@ -33,5 +33,11 @@ int main() {
     if (s) s[i-1] = 42;
   }
 
+  char *p_al0, *p_al1;
+  int p_memal_res = posix_memalign((void**)&p_al0, 32, 0);
+  free(p_al0);
+  int p_memal_res2 = posix_memalign((void**)&p_al1, 32, 42);
+  free(p_al1);
+
   return 0;
 }