From 97a783a1f7b9ff774a35d9942dd3cc34e3086247 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Sun, 11 Nov 2018 14:25:00 +0100
Subject: [PATCH] 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 | 1 +
src/plugins/e-acsl/share/e-acsl/e_acsl.h | 5 +
.../share/e-acsl/e_acsl_safe_locations.h | 10 +-
.../segment_model/e_acsl_segment_mmodel.c | 22 +++--
.../segment_model/e_acsl_segment_tracking.h | 5 +
.../e-acsl/tests/segment-only/constructor.c | 25 +++++
.../oracle/constructor.res.oracle | 22 +++++
.../segment-only/oracle/gen_constructor.c | 97 +++++++++++++++++++
.../e-acsl/tests/segment-only/test_config | 3 +
9 files changed, 179 insertions(+), 11 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/segment-only/constructor.c
create mode 100644 src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
create mode 100644 src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
create mode 100644 src/plugins/e-acsl/tests/segment-only/test_config
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 9bfbc386ed7..96261e25880 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/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/*
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl.h b/src/plugins/e-acsl/share/e-acsl/e_acsl.h
index 1045095a0b6..d217505a2d6 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl.h
+++ b/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; */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h
index d98a944cc10..78a52b13685 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h
+++ b/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
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index 580274d9b85..033325efd97 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/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);
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index 100e167734f..9a093e62ae0 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/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 */
diff --git a/src/plugins/e-acsl/tests/segment-only/constructor.c b/src/plugins/e-acsl/tests/segment-only/constructor.c
new file mode 100644
index 00000000000..68df399f553
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/constructor.c
@@ -0,0 +1,25 @@
+/* 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
diff --git a/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle b/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
new file mode 100644
index 00000000000..71defa5cfea
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
@@ -0,0 +1,22 @@
+[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).
diff --git a/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c b/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
new file mode 100644
index 00000000000..995599d7c5c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
@@ -0,0 +1,97 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/segment-only/test_config b/src/plugins/e-acsl/tests/segment-only/test_config
new file mode 100644
index 00000000000..3aa2fcbc6b1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/test_config
@@ -0,0 +1,3 @@
+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
--
GitLab