Merge branch 'bugfix/fonenantsoa/bts2405' into 'stable/argon'

Memory initialization for constructors

See merge request frama-c/e-acsl!265

src/plugins/e-acsl/.Makefile.lint

+ML_LINT_KO+=src/plugins/e-acsl/E_ACSL.mli
+ML_LINT_KO+=src/plugins/e-acsl/at_with_lscope.ml
+ML_LINT_KO+=src/plugins/e-acsl/at_with_lscope.mli
+ML_LINT_KO+=src/plugins/e-acsl/builtins.ml
+ML_LINT_KO+=src/plugins/e-acsl/demo/script.ml
+ML_LINT_KO+=src/plugins/e-acsl/dup_functions.ml
+ML_LINT_KO+=src/plugins/e-acsl/env.ml
+ML_LINT_KO+=src/plugins/e-acsl/env.mli
+ML_LINT_KO+=src/plugins/e-acsl/error.ml
+ML_LINT_KO+=src/plugins/e-acsl/error.mli
+ML_LINT_KO+=src/plugins/e-acsl/exit_points.ml
+ML_LINT_KO+=src/plugins/e-acsl/exit_points.mli
+ML_LINT_KO+=src/plugins/e-acsl/functions.ml
+ML_LINT_KO+=src/plugins/e-acsl/functions.mli
+ML_LINT_KO+=src/plugins/e-acsl/gmpz.ml
+ML_LINT_KO+=src/plugins/e-acsl/gmpz.mli
+ML_LINT_KO+=src/plugins/e-acsl/interval.ml
+ML_LINT_KO+=src/plugins/e-acsl/keep_status.ml
+ML_LINT_KO+=src/plugins/e-acsl/label.ml
+ML_LINT_KO+=src/plugins/e-acsl/literal_strings.ml
+ML_LINT_KO+=src/plugins/e-acsl/loops.ml
+ML_LINT_KO+=src/plugins/e-acsl/loops.mli
+ML_LINT_KO+=src/plugins/e-acsl/lscope.ml
+ML_LINT_KO+=src/plugins/e-acsl/lscope.mli
+ML_LINT_KO+=src/plugins/e-acsl/main.ml
+ML_LINT_KO+=src/plugins/e-acsl/misc.ml
+ML_LINT_KO+=src/plugins/e-acsl/misc.mli
+ML_LINT_KO+=src/plugins/e-acsl/mmodel_analysis.ml
+ML_LINT_KO+=src/plugins/e-acsl/mmodel_translate.ml
+ML_LINT_KO+=src/plugins/e-acsl/mmodel_translate.mli
+ML_LINT_KO+=src/plugins/e-acsl/options.ml
+ML_LINT_KO+=src/plugins/e-acsl/prepare_ast.ml
+ML_LINT_KO+=src/plugins/e-acsl/quantif.ml
+ML_LINT_KO+=src/plugins/e-acsl/quantif.mli
+ML_LINT_KO+=src/plugins/e-acsl/rte.ml
+ML_LINT_KO+=src/plugins/e-acsl/temporal.ml
+ML_LINT_KO+=src/plugins/e-acsl/temporal.mli
+ML_LINT_KO+=src/plugins/e-acsl/top/E_ACSL.mli
+ML_LINT_KO+=src/plugins/e-acsl/translate.ml
+ML_LINT_KO+=src/plugins/e-acsl/translate.mli
+ML_LINT_KO+=src/plugins/e-acsl/typing.ml
+ML_LINT_KO+=src/plugins/e-acsl/typing.mli
+ML_LINT_KO+=src/plugins/e-acsl/visit.ml

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/VERSION

-18.0-beta
\ No newline at end of file
+18.0+dev
\ No newline at end of file

src/plugins/e-acsl/doc/Changelog

@@ -23,8 +23,10 @@
 Plugin E-ACSL 18.0 (Argon)
 ##########################
 
+-* runtime      [2018/11/13] Fix bug #!2405 about memory initialization
+                in presence of GCC constructors.
 -* E-ACSL       [2018/10/23] Fix bug #2406 about monitoring of variables
-	        with incomplete types.
+                with incomplete types.
 -* E-ACSL       [2018/10/04] Fix bug #2386 about incorrect typing when
                 performing pointer subtraction.
 -* E-ACSL       [2018/10/04] Support for \at on purely logic variables.

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()
+  __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/segment_model/e_acsl_segment_mmodel.c

@@ -193,19 +193,30 @@ 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() {
+  if(MSPACES_INIT) return;
   describe_run();
+  make_memory_spaces(64*MB, get_heap_size());
+  /* Allocate and log shadow memory layout of the execution.
+    Case of the heap, globals and tls. */
+  init_shadow_layout_heap_global_tls();
+  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. */
-  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 */
-  init_shadow_layout(argc_ref, argv_ref);
+  /* Allocate and log shadow memory layout of the execution. Case of stack. */
+  init_shadow_layout_stack(argc_ref, argv_ref);
   //DEBUG_PRINT_LAYOUT;
   /* Make sure the layout holds */
   DVALIDATE_SHADOW_LAYOUT;

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();
+    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/share/e-acsl/segment_model/e_acsl_shadow_layout.h

@@ -72,8 +72,12 @@ char *strerror(int errnum);
 /*! \brief Size of a program's heap */
 #define PGM_HEAP_SIZE (E_ACSL_HEAP_SIZE * MB)
 
-/*! \brief Size of a program's Thread-local storage (TLS) */
-#define PGM_TLS_SIZE (16 * MB)
+/*! \brief Size of a program's Thread-local storage (TLS).
+  Standard streams stdin, stdout and stderr are put here.
+  Some libraries such as libxml use it quite a lot:
+  it may occur that the given size is not enough,
+  in which case it MUST be increased. */
+#define PGM_TLS_SIZE (32 * MB)
 
 /*! \brief Mspace padding used by shadow segments. This is to make sure that
  * some allocation which exceeds the size of an initial memspace does not
@@ -350,18 +354,9 @@ static void set_shadow_segment(memory_segment *seg, memory_segment *parent,
 
 /*! \brief Initialize memory layout, i.e., determine bounds of program segments,
  * allocate shadow memory spaces and compute offsets. This function populates
- * global struct ::memory_layout holding that information with data. */
-static void init_shadow_layout(int *argc_ref, char ***argv_ref) {
-  memory_partition *pheap = &mem_layout.heap;
-  set_application_segment(&pheap->application, get_heap_start(),
-    get_heap_size(), "heap", mem_spaces.heap_mspace);
-  set_shadow_segment(&pheap->primary, &pheap->application, 1, "heap_primary");
-  set_shadow_segment(&pheap->secondary, &pheap->application, 8, "heap_secondary");
-#ifdef E_ACSL_TEMPORAL
-  set_shadow_segment(&pheap->temporal_primary, &pheap->application, 1, "temporal_heap_primary");
-  set_shadow_segment(&pheap->temporal_secondary, &pheap->application, 1, "temporal_heap_secondary");
-#endif
-
+ * global struct ::memory_layout holding that information with data.
+   Case of the stack. */
+static void init_shadow_layout_stack(int *argc_ref, char ***argv_ref) {
   memory_partition *pstack = &mem_layout.stack;
   set_application_segment(&pstack->application, get_stack_start(argc_ref, argv_ref),
     get_stack_size(), "stack", NULL);
@@ -372,6 +367,24 @@ static void init_shadow_layout(int *argc_ref, char ***argv_ref) {
   set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1, "temporal_stack_secondary");
 #endif
 
+  mem_layout.is_initialized = 1;
+}
+
+/*! \brief Initialize memory layout, i.e., determine bounds of program segments,
+ * allocate shadow memory spaces and compute offsets. This function populates
+ * global struct ::memory_layout holding that information with data.
+   Case of the heap, globals and tls. */
+static void init_shadow_layout_heap_global_tls() {
+  memory_partition *pheap = &mem_layout.heap;
+  set_application_segment(&pheap->application, get_heap_start(),
+    get_heap_size(), "heap", mem_spaces.heap_mspace);
+  set_shadow_segment(&pheap->primary, &pheap->application, 1, "heap_primary");
+  set_shadow_segment(&pheap->secondary, &pheap->application, 8, "heap_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&pheap->temporal_primary, &pheap->application, 1, "temporal_heap_primary");
+  set_shadow_segment(&pheap->temporal_secondary, &pheap->application, 1, "temporal_heap_secondary");
+#endif
+
   memory_partition *pglobal = &mem_layout.global;
   set_application_segment(&pglobal->application, get_global_start(),
     get_global_size(), "global", NULL);

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

+/* run.config
+   COMMENT: bts #2405. Memory not initialized for code executed before main.
+*/
+
+#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");
+  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:16: Warning: 
+  E-ACSL construct `logic function application' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/segment-only/constructor.c:16: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/segment-only/constructor.c:10: Warning: 
+  E-ACSL construct `logic function application' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/segment-only/constructor.c:10: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".

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

+/* Generated by Frama-C */
+#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);
+  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);
+  __retres = 0;
+  __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