Memory initialization for constructors. TODO:

 - safe locations (standard streams)
 - memory operations other than malloc that require memory_init to be called beforehand
 - bittree model

src/plugins/e-acsl/.gitignore

@@ -63,6 +63,7 @@
 /tests/no-main/result/*
 /tests/full-mmodel/result/*
 /tests/full-mmodel-only/result/*
+/tests/segment-only/result/*
 /tests/bts/result/*
 /tests/gmp/result/*
 /tests/reject/result/*

src/plugins/e-acsl/share/e-acsl/e_acsl.h

@@ -84,6 +84,7 @@
 
 /* Memory state initialization */
 #define memory_clean          export_alias(memory_clean)
+#define mspaces_init          export_alias(mspaces_init)
 #define memory_init           export_alias(memory_init)
 
 /* Heap size */
@@ -175,6 +176,10 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
 /*** Memory tracking {{{ ***/
 /************************************************************************/
 
+/*! \brief Initialize memory locations. */
+void mspaces_init(int *argc_ref, char *** argv_ref)
+  __attribute__((FC_BUILTIN));
+
 /*! \brief Initialize memory tracking state.
  * Called before any other statement in \p main */
 /*@ assigns \nothing; */

src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h

@@ -69,9 +69,11 @@ extern FILE *stderr;		/* Standard error output stream. */
 
 static void collect_safe_locations() {
   /* Tracking of errno and standard streams */
-  add_safe_location((uintptr_t)&errno, sizeof(int), "errno");
-  add_safe_location((uintptr_t)stdout, sizeof(FILE), "stdout");
-  add_safe_location((uintptr_t)stderr, sizeof(FILE), "stderr");
-  add_safe_location((uintptr_t)stdin, sizeof(FILE), "stdin");
+  /* TODO: how to corrrectly add the following locations
+     in presence of contructors? */
+  // add_safe_location((uintptr_t)&errno, sizeof(int), "errno");
+  // add_safe_location((uintptr_t)stdout, sizeof(FILE), "stdout");
+  // add_safe_location((uintptr_t)stderr, sizeof(FILE), "stderr");
+  // add_safe_location((uintptr_t)stdin, sizeof(FILE), "stdin");
 }
 #endif

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c

@@ -193,15 +193,12 @@ static void argv_alloca(int *argc_ref,  char *** argv_ref) {
 /* Program initialization {{{ */
 extern int main(void);
 
-void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
+int MSPACES_INIT = 0;
+
+void mspaces_init(int *argc_ref, char *** argv_ref) {
+  if(MSPACES_INIT) return;
   describe_run();
-  /** Verify that the given size of a pointer matches the one in the present
-   * architecture. This is a guard against Frama-C instrumentations using
-   * architectures different to the given one. */
   make_memory_spaces(64*MB, get_heap_size());
-  arch_assert(ptr_size);
-  /* Initialize report file with debug logs (only in debug mode). */
-  initialize_report_file(argc_ref, argv_ref);
   /* Lift stack limit to account for extra stack memory overhead.  */
   increase_stack_limit(get_stack_size()*2);
   /* Allocate and log shadow memory layout of the execution */
@@ -209,6 +206,17 @@ void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
   //DEBUG_PRINT_LAYOUT;
   /* Make sure the layout holds */
   DVALIDATE_SHADOW_LAYOUT;
+  MSPACES_INIT = 1;
+}
+
+void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
+  mspaces_init(argc_ref, argv_ref);
+  /** Verify that the given size of a pointer matches the one in the present
+   * architecture. This is a guard against Frama-C instrumentations using
+   * architectures different to the given one. */
+  arch_assert(ptr_size);
+  /* Initialize report file with debug logs (only in debug mode). */
+  initialize_report_file(argc_ref, argv_ref);
   /* Track program arguments. */
   if (argc_ref && argv_ref)
     argv_alloca(argc_ref, argv_ref);

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h

@@ -880,6 +880,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
   }
 }
 
+extern int MSPACES_INIT;
 /*! \brief Replacement for a malloc function that additionally tracks the
  * allocated memory block.
  *
@@ -893,6 +894,10 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
  *    behaviour is as if the size were some non-zero value, except that the
  *    returned pointer shall not be used to access an object." */
 void* malloc(size_t size) {
+  if(! MSPACES_INIT) {
+    mspaces_init(0, 0); // arguments of main are not (?) known at this point
+    MSPACES_INIT = 1;
+  }
   size_t alloc_size = ALLOC_SIZE(size);
 
   /* Return NULL if the size is too large to be aligned */

src/plugins/e-acsl/tests/segment-only/constructor.c

+/* run.config
+   COMMENT: bts #2405. Memory not initialized for code executed before main.
+*/
+
+#include <errno.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+__attribute__((constructor))
+void f() {
+  printf("f\n");
+  char *buf = (char*)malloc(10*sizeof(char));
+  free(buf);
+}
+
+int main() {
+  printf("main\n");
+  int *p = &errno;
+  // TODO: see e_acsl_safe_locations.h regarding the standard streams
+  /*@ assert ! \valid(p);      */ ;
+  /*@ assert ! \valid(stderr); */ ;
+  /*@ assert ! \valid(stdin);  */ ;
+  /*@ assert ! \valid(stdout); */ ;
+  return 0;
+}
\ No newline at end of file

src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `printf_va_1':
+  the generated program may miss memory instrumentation
+  if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `printf_va_2':
+  the generated program may miss memory instrumentation
+  if there are memory-related annotations.
+[e-acsl] tests/segment-only/constructor.c:17: Warning: 
+  E-ACSL construct `logic function application' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/segment-only/constructor.c:17: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/segment-only/constructor.c:11: Warning: 
+  E-ACSL construct `logic function application' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/segment-only/constructor.c:11: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/segment-only/constructor.c:19: Warning: 
+  assertion got status invalid (stopping propagation).

src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c

+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdio.h"
+#include "stdlib.h"
+char *__gen_e_acsl_literal_string_2;
+char *__gen_e_acsl_literal_string;
+void f(void) __attribute__((__constructor__));
+void f(void)
+{
+  __gen_e_acsl_printf_va_1(__gen_e_acsl_literal_string);
+  char *buf = malloc((unsigned long)10 * sizeof(char));
+  free((void *)buf);
+  return;
+}
+
+void __e_acsl_globals_init(void)
+{
+  __gen_e_acsl_literal_string_2 = "main\n";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+                       sizeof("main\n"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+  __gen_e_acsl_literal_string = "f\n";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("f\n"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+  __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+  __e_acsl_store_block((void *)(& stdout),(size_t)8);
+  __e_acsl_full_init((void *)(& stdout));
+  __e_acsl_store_block((void *)(& stdin),(size_t)8);
+  __e_acsl_full_init((void *)(& stdin));
+  __e_acsl_store_block((void *)(& stderr),(size_t)8);
+  __e_acsl_full_init((void *)(& stderr));
+  __e_acsl_store_block((void *)(& errno),(size_t)4);
+  __e_acsl_full_init((void *)(& errno));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_globals_init();
+  __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string_2);
+  int *p = & errno;
+  __e_acsl_store_block((void *)(& p),(size_t)8);
+  __e_acsl_full_init((void *)(& p));
+  /*@ assert ¬\valid(p); */
+  {
+    int __gen_e_acsl_initialized;
+    int __gen_e_acsl_and;
+    __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
+                                                    sizeof(int *));
+    if (__gen_e_acsl_initialized) {
+      int __gen_e_acsl_valid;
+      __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
+                                          (void *)(& p));
+      __gen_e_acsl_and = __gen_e_acsl_valid;
+    }
+    else __gen_e_acsl_and = 0;
+    __e_acsl_assert(! __gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+                    (char *)"!\\valid(p)",19);
+  }
+  /*@ assert ¬\valid(__fc_stderr); */
+  {
+    int __gen_e_acsl_valid_2;
+    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stderr,sizeof(FILE),
+                                          (void *)stderr,(void *)(& stderr));
+    __e_acsl_assert(! __gen_e_acsl_valid_2,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\valid(__fc_stderr)",20);
+  }
+  /*@ assert ¬\valid(__fc_stdin); */
+  {
+    int __gen_e_acsl_valid_3;
+    __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdin,sizeof(FILE),
+                                          (void *)stdin,(void *)(& stdin));
+    __e_acsl_assert(! __gen_e_acsl_valid_3,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\valid(__fc_stdin)",21);
+  }
+  /*@ assert ¬\valid(__fc_stdout); */
+  {
+    int __gen_e_acsl_valid_4;
+    __gen_e_acsl_valid_4 = __e_acsl_valid((void *)stdout,sizeof(FILE),
+                                          (void *)stdout,(void *)(& stdout));
+    __e_acsl_assert(! __gen_e_acsl_valid_4,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\valid(__fc_stdout)",22);
+  }
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& stdout));
+  __e_acsl_delete_block((void *)(& stdin));
+  __e_acsl_delete_block((void *)(& stderr));
+  __e_acsl_delete_block((void *)(& errno));
+  __e_acsl_delete_block((void *)(& p));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/segment-only/test_config

+LOG: gen_@PTEST_NAME@.c
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/segment-only/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0
+EXEC: ./scripts/testrun.sh @PTEST_NAME@ segment-only "" "--frama-c=@frama-c@" "segment"
\ No newline at end of file