From 7560a41adc9415f91514b8c810068e38e6c0a648 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Tue, 13 Nov 2018 19:27:25 +0100
Subject: [PATCH] Julien's review no.1: - Safe locations are ok but need to
increase TLS to 32 Mo for the libxml usecase - Fix order of operations
during memory initialization - TODO: memory allocated before main are not
seen as being valid
---
src/plugins/e-acsl/doc/Changelog | 4 +-
src/plugins/e-acsl/share/e-acsl/e_acsl.h | 2 +-
.../share/e-acsl/e_acsl_safe_locations.h | 10 ++--
.../segment_model/e_acsl_segment_mmodel.c | 19 ++++---
.../segment_model/e_acsl_segment_tracking.h | 2 +-
.../segment_model/e_acsl_shadow_layout.h | 41 ++++++++-----
.../e-acsl/tests/segment-only/constructor.c | 7 ---
.../oracle/constructor.res.oracle | 10 ++--
.../segment-only/oracle/gen_constructor.c | 57 -------------------
9 files changed, 51 insertions(+), 101 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 36f1ff2a80e..83371e18524 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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.
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 d217505a2d6..e25be516e6c 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.h
@@ -177,7 +177,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
/************************************************************************/
/*! \brief Initialize memory locations. */
-void mspaces_init(int *argc_ref, char *** argv_ref)
+void mspaces_init()
__attribute__((FC_BUILTIN));
/*! \brief Initialize memory tracking state.
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 78a52b13685..d98a944cc10 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,11 +69,9 @@ extern FILE *stderr; /* Standard error output stream. */
static void collect_safe_locations() {
/* Tracking of errno and standard streams */
- /* 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");
+ 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 033325efd97..eae9f787e3a 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
@@ -195,17 +195,13 @@ extern int main(void);
int MSPACES_INIT = 0;
-void mspaces_init(int *argc_ref, char *** argv_ref) {
+void mspaces_init() {
if(MSPACES_INIT) return;
describe_run();
make_memory_spaces(64*MB, get_heap_size());
- /* 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);
- //DEBUG_PRINT_LAYOUT;
- /* Make sure the layout holds */
- DVALIDATE_SHADOW_LAYOUT;
+ /* 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;
}
@@ -217,6 +213,13 @@ void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_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. Case of stack. */
+ init_shadow_layout_stack(argc_ref, argv_ref);
+ //DEBUG_PRINT_LAYOUT;
+ /* Make sure the layout holds */
+ DVALIDATE_SHADOW_LAYOUT;
/* 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 9a093e62ae0..e3cf2c42b9e 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
@@ -895,7 +895,7 @@ extern int MSPACES_INIT;
* 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();
MSPACES_INIT = 1;
}
size_t alloc_size = ALLOC_SIZE(size);
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
index 0822602dd21..f7a779e8925 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
+++ b/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);
diff --git a/src/plugins/e-acsl/tests/segment-only/constructor.c b/src/plugins/e-acsl/tests/segment-only/constructor.c
index 68df399f553..6600992870e 100644
--- a/src/plugins/e-acsl/tests/segment-only/constructor.c
+++ b/src/plugins/e-acsl/tests/segment-only/constructor.c
@@ -2,7 +2,6 @@
COMMENT: bts #2405. Memory not initialized for code executed before main.
*/
-#include <errno.h>
#include <stdio.h>
#include <stdlib.h>
@@ -15,11 +14,5 @@ void f() {
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
index 71defa5cfea..fb1184a3e56 100644
--- a/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
@@ -5,18 +5,16 @@
[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] 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:17: Warning:
+[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:11: Warning:
+[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:11: Warning:
+[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".
-[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
index 995599d7c5c..eefdbbe0fd9 100644
--- a/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
@@ -1,5 +1,4 @@
/* Generated by Frama-C */
-#include "errno.h"
#include "stdio.h"
#include "stdlib.h"
char *__gen_e_acsl_literal_string_2;
@@ -24,14 +23,6 @@ void __e_acsl_globals_init(void)
__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;
}
@@ -41,55 +32,7 @@ int main(void)
__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;
}
--
GitLab