From d5013fc04c672331eeaee0ee1737157c9acdab0e Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 15 May 2017 15:27:37 +0200
Subject: [PATCH] Initialize program arguments from within RTL
---
.../bittree_model/e_acsl_bittree_mmodel.c | 35 ++++++++++++++-----
.../segment_model/e_acsl_segment_mmodel.c | 34 +++++++++++++++++-
.../segment_model/e_acsl_segment_tracking.h | 15 --------
.../tests/runtime/oracle/gen_bypassed_var.c | 1 -
.../tests/runtime/oracle/gen_mainargs.c | 2 --
src/plugins/e-acsl/visit.ml | 6 ++--
6 files changed, 63 insertions(+), 30 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 2dfec7bee2c..56ea8d22c63 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -516,16 +516,33 @@ static void memory_clean() {
bt_clean();
}
-/* add `argv` to the memory model */
-static void init_argv(int argc, char **argv) {
- int i;
+extern char **environ;
- store_block(argv, (argc+1)*sizeof(char*));
- full_init(argv);
+/* add `argv` to the memory model */
+static void argv_alloca(int *argc_ref, char *** argv_ref) {
+ /* Track a top-level containers */
+ store_block((void*)argc_ref, sizeof(int));
+ store_block((void*)argv_ref, sizeof(char**));
+ int argc = *argc_ref;
+ char** argv = *argv_ref;
+ /* Track argv */
+
+ size_t argvlen = (argc + 1)*sizeof(char*);
+ store_block(argv, argvlen);
+ initialize(argv, (argc + 1)*sizeof(char*));
+
+ while (*argv) {
+ size_t arglen = strlen(*argv) + 1;
+ store_block(*argv, arglen);
+ initialize(*argv, arglen);
+ argv++;
+ }
- for (i = 0; i < argc; i++) {
- store_block(argv[i], strlen(argv[i])+1);
- full_init(argv[i]);
+ while (*environ) {
+ size_t envlen = strlen(*environ) + 1;
+ store_block(*environ, envlen);
+ initialize(*environ, envlen);
+ environ++;
}
}
@@ -535,7 +552,7 @@ static void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
initialize_report_file(argc_ref, argv_ref);
/* Tracking program arguments */
if (argc_ref)
- init_argv(*argc_ref, *argv_ref);
+ argv_alloca(argc_ref, argv_ref);
/* Tracking safe locations */
collect_safe_locations();
int i;
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 a4002694bf5..9be817a176a 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
@@ -128,6 +128,38 @@ static size_t get_heap_allocation_size(void) {
}
/* }}} */
+/* Track program arguments (ARGC/ARGV) {{{ */
+extern char ** environ;
+
+static void argv_alloca(int *argc_ref, char *** argv_ref) {
+ /* Track a top-level containers */
+ shadow_alloca((void*)argc_ref, sizeof(int));
+ shadow_alloca((void*)argv_ref, sizeof(char**));
+ int argc = *argc_ref;
+ char** argv = *argv_ref;
+ /* Track argv */
+ size_t argvlen = (argc + 1)*sizeof(char*);
+ shadow_alloca(argv, argvlen);
+ initialize_static_region((uintptr_t)argv, (argc + 1)*sizeof(char*));
+
+ /* Track argument strings */
+ while (*argv) {
+ size_t arglen = strlen(*argv) + 1;
+ shadow_alloca(*argv, arglen);
+ initialize_static_region((uintptr_t)*argv, arglen);
+ argv++;
+ }
+
+ while (*environ) {
+ size_t envlen = strlen(*environ) + 1;
+ shadow_alloca(*environ, envlen);
+ initialize_static_region((uintptr_t)*environ, envlen);
+ environ++;
+ }
+}
+/* }}} */
+
+/* Program initialization {{{ */
static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
describe_run();
/** Verify that the given size of a pointer matches the one in the present
@@ -144,7 +176,7 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
DVALIDATE_SHADOW_LAYOUT;
/* Track program arguments. */
if (argc_ref && argv_ref)
- argv_alloca(*argc_ref, *argv_ref);
+ argv_alloca(argc_ref, argv_ref);
/* Tracking safe locations */
collect_safe_locations();
int i;
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 2cce5183102..45fd1e1ab79 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
@@ -771,21 +771,6 @@ static void mark_readonly_region (uintptr_t addr, long size) {
}
/* }}} */
-/* Track program arguments (ARGC/ARGV) {{{ */
-static void argv_alloca(int argc, char ** argv) {
- /* Track a top-level container (i.e., `*argv`) */
- shadow_alloca(argv, (argc + 1)*sizeof(char*));
- initialize_static_region((uintptr_t)argv, (argc + 1)*sizeof(char*));
- /* Track argument strings */
- while (*argv) {
- size_t arglen = strlen(*argv) + 1;
- shadow_alloca(*argv, arglen);
- initialize_static_region((uintptr_t)*argv, arglen);
- argv++;
- }
-}
-/* }}} */
-
/* Heap allocation {{{ (malloc/calloc) */
/*! \brief Amount of heap memory allocated by the program.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
index 7787974a786..4e7868fd36b 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
@@ -4,7 +4,6 @@ int main(int argc, char const **argv)
{
int __retres;
__e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
- __e_acsl_store_block((void *)(& argc),(size_t)4);
goto L;
{
int *p;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index f0a7e6b8479..6377f308afc 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -9,8 +9,6 @@ int main(int argc, char **argv)
/*@ assert \valid(&argc); */
{
int __gen_e_acsl_valid;
- __e_acsl_store_block((void *)(& argv),(size_t)8);
- __e_acsl_store_block((void *)(& argc),(size_t)4);
__gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int),
(void *)(& argc),(void *)(& argc));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 767ea2bc422..2bfb8b9f0af 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -524,8 +524,10 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if self#is_first_stmt kf stmt then
(* JS: should be done in the new project? *)
let env =
- if generate then Memory.store env kf (Kernel_function.get_formals kf)
- else env
+ if generate && not is_main then
+ Memory.store env kf (Kernel_function.get_formals kf)
+ else
+ env
in
(* translate the precondition of the function *)
if Dup_functions.is_generated (Extlib.the self#current_kf) then
--
GitLab