diff --git a/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c b/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c
index be59fec25029ee982890a09a45d3aa4c268d56a4..1e7d5016f843628504740cf187156ff9d0cf120d 100644
--- a/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c
+++ b/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c
@@ -797,7 +797,17 @@ struct mallinfo {
Try to persuade compilers to inline. The most critical functions for
inlining are defined as macros, so these aren't used for them.
*/
-
+// MinGW defines `FORCEINLINE` as `__forceinline`, and defines `__forceinline`
+// with an "extern" storage class. Since the macro `FORCEINLINE` is used here
+// on `static` function, a compilation error occurs because `static` and
+// `extern` cannot be used at the same time.
+// This implementation "problem" is known to the MinGW team but is explicitely
+// marked as "won't fix": https://sourceforge.net/p/mingw-w64/bugs/269/
+// So the workaround here is to `undef FORCEINLINE` if the file is being
+// compiled by MinGW.
+#ifdef __MINGW32__ // defined for 32 bits and 64 bits MinGW
+#undef FORCEINLINE
+#endif
#ifndef FORCEINLINE
#if defined(__GNUC__)
#define FORCEINLINE __inline __attribute__ ((always_inline))
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 5a7d4b618dba3400398d2be044936114698e65bd..c988d92e0c9f25a6faf85cfe8ab5724c1e4ef286 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,7 @@
Plugin E-ACSL <next-release>
############################
+- E-ACSL [2020-12-09] Add RTL support for Windows.
- E-ACSL [2020-11-17] Update e-acsl-gcc.sh so that the library dlmalloc
can be compiled and used from sources.
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index cf2b2a13c0e9dec43354173a1758d67cf4a4132d..b7f88f446f513c056e4509f5ddc8b1a51215af0a 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -21,6 +21,7 @@ share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h: CEA_LGPL_OR_PROP
share/e-acsl/internals/e_acsl_alias.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_bits.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_bits.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+share/e-acsl/internals/e_acsl_config.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_debug.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_debug.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_malloc.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index e3bc300bdb9cfecd266095c95aa89fecf275b056..884dfb189ef701e5fe8a7ebe7d234fa76d4abe90 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -123,6 +123,13 @@ alternatives that include internal runtime error checking.
always use GMP integers instead of C integral types.
By default the GMP integers are used on as-needed basis.
.TP
+.B --mbits=\fI<BITS>
+architecture to compile to. Valid arguments are \fI16\fP, \fI32\fP or \fI64\fP.
+Default to the architecture of the current environment.
+This option is used to select the \fBmachdep\fP when calling \fBFrama-C\fP, and
+to pass the corresponding \fB-m16\fP, \fB-m32\fP or \fB-m64\fP flag to the
+compiler.
+.TP
.B -l, --ld-flags=\fI<FLAGS>
pass the specified flags to the linker.
.TP
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
index 2195d4cca8d9f0cd09df9a5d0a57093c7ceff68b..ba42f3854cab950f8e08416fd90a90132e6bd20d 100644
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
@@ -36,7 +36,7 @@ _eacsl_gcc() {
--no-trace
--ocode= --oexec= --oexec-e-acsl=
--ld-flags= --cpp-flags= --extra-cpp-args=
- --frama-c-extra= --frama-c= --gcc= --ar= --ranlib=
+ --frama-c-extra= --frama-c= --gcc= --ar= --ranlib= --mbits=
--e-acsl-share= --memory-model= --e-acsl-extra=
--compile --compile-only --print-mmodels --frama-c-only --instrumented-only
--gmp --full-mtracking --rte= --rte-select= --no-int-overflow
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 044bd8fab58bd62175ed6405651c14984df607fa..f446a9f3c49a22f19c6641f64c89bd545703e2f5 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -276,7 +276,7 @@ LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:,
temporal,weak-validity,stack-size:,heap-size:,rt-verbose,free-valid-address,
external-assert:,validate-format-strings,no-trace,libc-replacements,
with-dlmalloc:,dlmalloc-from-sources,dlmalloc-compile-only,
- dlmalloc-compile-flags:,odlmalloc:,ar:,ranlib:"
+ dlmalloc-compile-flags:,odlmalloc:,ar:,ranlib:,mbits:"
SHORTOPTIONS="h,c,C,d:,D,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,I:,G:,X,a:,T,k,V"
# Prefix for an error message due to wrong arguments
ERROR="ERROR parsing arguments:"
@@ -286,6 +286,7 @@ OPTION_CFLAGS= # Compiler flags
OPTION_CPPFLAGS= # Preprocessor flags
OPTION_LDFLAGS= # Linker flags
OPTION_FRAMAC="frama-c" # Frama-C executable name
+OPTION_MBITS= # Which architecture to compile to
OPTION_CC="gcc" # GCC executable name
OPTION_AR="ar" # AR executable name
OPTION_RANLIB="ranlib" # RANLIB executable name
@@ -684,6 +685,12 @@ do
OPTION_OUTPUT_DLMALLOC="$1"
shift;
;;
+ # Architecture selection
+ --mbits)
+ shift;
+ OPTION_MBITS="$1"
+ shift;
+ ;;
esac
done
shift;
@@ -732,7 +739,11 @@ fi
# Architecture-dependent flags. Since by default Frama-C uses 32-bit
# architecture we need to make sure that same architecture is used for
# instrumentation and for compilation.
-MACHDEPFLAGS="`getconf LONG_BIT`"
+if [ -n "$OPTION_MBITS" ]; then
+ MACHDEPFLAGS="$OPTION_MBITS"
+else
+ MACHDEPFLAGS="`getconf LONG_BIT`"
+fi
# Check if getconf gives out the value accepted by Frama-C/GCC
echo "$MACHDEPFLAGS" | grep '16\|32\|64' 2>&1 >/dev/null \
|| error "$MACHDEPFLAGS-bit architecture not supported"
@@ -846,6 +857,7 @@ if [ "$OPTION_DLMALLOC_FROM_SOURCES" = "1" -o \
fi
DLMALLOC_FLAGS="\
+ $GCCMACHDEP \
-DHAVE_MORECORE=0 \
-DHAVE_MMAP=1 \
-DNO_MALLINFO=1 \
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
index 7e74611ac5ee19b82530640f0ffa594151660c7b..4317ace0b93bc35b60ff88efe31380acb44035b1 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
@@ -25,6 +25,14 @@
# define _DEFAULT_SOURCE 1
#endif
+/* On Windows, setup minimum version to Windows 8 (or Server 2012) to be able to
+ use some specific API functions.
+ Check directly for windows instead of using E_ACSL_OS_IS_WINDOWS so that it
+ can be done without including anything. */
+#if defined(WIN32) || defined(_WIN32) || defined(__WIN32)
+# define _WIN32_WINNT 0x0602
+#endif
+
// Internals
#include "internals/e_acsl_bits.c"
#include "internals/e_acsl_debug.c"
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h
new file mode 100644
index 0000000000000000000000000000000000000000..7ab971cc8b2ea03672415c85629ed54d3c755b94
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h
@@ -0,0 +1,66 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2020 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+/*! ***********************************************************************
+ * \file
+ * \brief Internal defines for E-ACSL set according to the current environment.
+ *
+ * Instead of using complicated logic with predefined macros in the RTL, the
+ * logic should be done in this file and an E-ACSL specific define set to record
+ * the result of the logic.
+ */
+
+#ifndef E_ACSL_CONFIG_H
+#define E_ACSL_CONFIG_H
+
+// OS detection
+// - Assign values to specific OSes
+#define E_ACSL_OS_LINUX_VALUE 1
+#define E_ACSL_OS_WINDOWS_VALUE 2
+#define E_ACSL_OS_OTHER_VALUE 999
+// - Declare defines to test for a specific OS
+/*!
+ * \brief True if the target OS is linux, false otherwise
+ */
+#define E_ACSL_OS_IS_LINUX E_ACSL_OS == E_ACSL_OS_LINUX_VALUE
+/*!
+ * \brief True if the target OS is windows, false otherwise
+ */
+#define E_ACSL_OS_IS_WINDOWS E_ACSL_OS == E_ACSL_OS_WINDOWS_VALUE
+/*!
+ * \brief True if the target OS is unknown, false otherwise
+ */
+#define E_ACSL_OS_IS_OTHER E_ACSL_OS == E_ACSL_OS_OTHER_VALUE
+// - Check current OS
+#ifdef __linux__
+// Linux compilation
+# define E_ACSL_OS E_ACSL_OS_LINUX_VALUE
+#elif defined(WIN32) || defined(_WIN32) || defined(__WIN32)
+// Windows compilation
+# define E_ACSL_OS E_ACSL_OS_WINDOWS_VALUE
+#else
+// Other
+# define E_ACSL_OS E_ACSL_OS_OTHER_VALUE
+# error "Unsupported OS for E-ACSL RTL"
+#endif
+
+#endif // E_ACSL_CONFIG_H
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
index 0c42873864c1d7b89465dcc26403ac252afb3de3..3389f05f78e8d93125ba3759ce1baf45771047d4 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
@@ -24,6 +24,7 @@
#include <fcntl.h>
#include "../observation_model/internals/e_acsl_omodel_debug.h"
+#include "e_acsl_config.h"
#include "e_acsl_private_assert.h"
#include "e_acsl_rtl_io.h"
@@ -45,8 +46,13 @@ void initialize_report_file(int *argc, char ***argv) {
if (!strcmp(dlog_name, "-") || !strcmp(dlog_name, "1")) {
dlog_fd = 2;
} else {
- dlog_fd = open(dlog_name, O_WRONLY | O_CREAT | O_TRUNC |O_NONBLOCK
+#if E_ACSL_OS_IS_LINUX
+ dlog_fd = open(dlog_name, O_WRONLY | O_CREAT | O_TRUNC | O_NONBLOCK
| O_NOCTTY, S_IRUSR | S_IWUSR | S_IRGRP | S_IWGRP | S_IROTH | S_IWOTH);
+#elif E_ACSL_OS_IS_WINDOWS
+ dlog_fd = _open(dlog_name, _O_WRONLY | _O_CREAT | _O_TRUNC,
+ _S_IREAD | _S_IWRITE);
+#endif
}
if (dlog_fd == -1)
private_abort("Cannot open file descriptor for %s\n", dlog_name);
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
index 94516feab171db3523c2e71ce28f0fefd575cfb6..b5133be6fdc26828abba82fa819ce520af351ac9 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
@@ -20,16 +20,12 @@
/* */
/**************************************************************************/
-/* Get default definitions and macros e.g., PATH_MAX */
-// #ifndef _DEFAULT_SOURCE
-// # define _DEFAULT_SOURCE 1
-// #endif
-
#include <limits.h>
#include <signal.h>
#include <stdarg.h>
#include <stddef.h>
+#include "e_acsl_config.h"
#include "e_acsl_rtl_io.h"
#include "e_acsl_trace.h"
@@ -54,14 +50,18 @@ void raise_abort(const char *file, int line) {
void private_abort_fail(const char * file, int line, char *fmt, ...) {
va_list va;
+#if E_ACSL_OS_IS_LINUX
sigset_t defer_abrt;
sigemptyset(&defer_abrt);
sigaddset(&defer_abrt,SIGABRT);
sigprocmask(SIG_BLOCK,&defer_abrt,NULL);
+#endif // E_ACSL_OS_IS_LINUX
va_start(va,fmt);
rtl_veprintf(fmt, va);
va_end(va);
+#if E_ACSL_OS_IS_LINUX
sigprocmask(SIG_UNBLOCK,&defer_abrt,NULL);
+#endif // E_ACSL_OS_IS_LINUX
raise_abort(file, line);
}
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c
index e13e8dfdaa1972564d400fdb2d673294841a18cf..77f1b91237ebb27d9c8d6610089f6c2e190fd6fa 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c
@@ -25,6 +25,11 @@
* \brief Implementation for running shell commands
***************************************************************************/
+#include "e_acsl_config.h"
+
+// Only available on linux
+#if E_ACSL_OS_IS_LINUX
+
#include <errno.h>
#include <stddef.h>
#include <sys/types.h>
@@ -201,3 +206,5 @@ ipr_t* shexec (char **data, const char *sin) {
/* Run the command returning a pointer to `ipr_t` */
return __shexec(ipr);
}
+
+#endif // E_ACSL_OS_IS_LINUX
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h
index 16cb2d9a1d3a0161bc39ca0159d03962d07a8a00..754cabb418656fbde4bbfc1cb8a6bd9dbc85780b 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h
@@ -28,6 +28,11 @@
#ifndef E_ACSL_SHEXEC_H
#define E_ACSL_SHEXEC_H
+#include "e_acsl_config.h"
+
+// Only available on linux
+#if E_ACSL_OS_IS_LINUX
+
#include <sys/types.h>
/*! \class ipr_t
@@ -68,4 +73,6 @@ typedef struct {
* `free_ipr` function. */
ipr_t* shexec (char **data, const char *sin);
+#endif // E_ACSL_OS_IS_LINUX
+
#endif // E_ACSL_SHEXEC_H
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
index 892f53f5c204ed69fda30a7f89bd4452384825b3..64336e758bd4f23af52d118a5a8854be7985bed3 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
@@ -28,6 +28,7 @@
#include <limits.h>
#include <stddef.h>
+#include "e_acsl_config.h"
#include "e_acsl_malloc.h"
#include "e_acsl_rtl_io.h"
#include "e_acsl_rtl_string.h"
@@ -35,6 +36,7 @@
#include "e_acsl_trace.h"
+#if E_ACSL_OS_IS_LINUX
extern void *__libc_stack_end;
struct frame_layout {
@@ -69,9 +71,10 @@ static int native_backtrace (void **array, int size) {
}
return cnt;
}
+#endif
void trace() {
-# ifdef __linux__
+# if E_ACSL_OS_IS_LINUX
int size = 24;
void **bb = private_malloc(sizeof(void*)*size);
@@ -107,5 +110,5 @@ void trace() {
counter++;
}
STDOUT("/***************************************/\n");
-# endif /* __linux__ */
+# endif /* E_ACSL_OS_IS_LINUX */
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
index a605bbdb95f10e6f31fb443915653495c2e7ae4a..e0dcc56094698aaf8d1c0df34008a8b6d4ee2ee6 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
@@ -25,12 +25,24 @@
* \brief Patricia Trie API Implementation
***************************************************************************/
+#include "../../internals/e_acsl_config.h"
#include "../../internals/e_acsl_malloc.h"
#include "../../internals/e_acsl_private_assert.h"
#include "e_acsl_bittree.h"
+#if E_ACSL_OS_IS_LINUX
#define WORDBITS __WORDSIZE
+#elif E_ACSL_OS_IS_WINDOWS
+// On windows, __WORDSIZE is not available
+# ifdef _WIN64
+# define WORDBITS 64
+# else
+# define WORDBITS 32
+# endif
+#else
+# error "Unsupported OS"
+#endif
static size_t mask(size_t, size_t);
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
index e729c281313b6d416e029212f012a2cc90f31695..1f6296b66387b1971aa988af762766526fe9e681 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
@@ -587,11 +587,13 @@ void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
int i;
for (i = 0; i < get_safe_locations_count(); i++) {
memory_location * loc = get_safe_location(i);
- void *addr = (void*)loc->address;
- uintptr_t len = loc->length;
- eacsl_store_block(addr, len);
- if (loc->is_initialized)
- eacsl_initialize(addr, len);
+ if (loc->is_on_static) {
+ void *addr = (void*)loc->address;
+ uintptr_t len = loc->length;
+ eacsl_store_block(addr, len);
+ if (loc->is_initialized)
+ eacsl_initialize(addr, len);
+ }
}
init_infinity_values();
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
index 86d1ad4e0a63e4cc6c1b927e520a7f6877e2c4cd..9c2e61b587126620383f4c16337b7a457d4a3f58 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
@@ -23,6 +23,7 @@
#include <stdio.h>
#include <errno.h>
+#include "../../internals/e_acsl_config.h"
#include "e_acsl_safe_locations.h"
/* An array storing safe locations up to `safe_location_counter` position.
@@ -31,18 +32,20 @@
static memory_location safe_locations [16];
static int safe_location_counter = 0;
-#define add_safe_location(_addr,_len,_init) { \
+#define add_safe_location(_addr,_len,_init,_on_static) do { \
safe_locations[safe_location_counter].address = _addr; \
safe_locations[safe_location_counter].length = _len; \
+ safe_locations[safe_location_counter].is_initialized = _init; \
+ safe_locations[safe_location_counter].is_on_static = _on_static; \
safe_location_counter++; \
-}
+} while (0)
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");
+ add_safe_location((uintptr_t)&errno, sizeof(int), 1, E_ACSL_OS_IS_LINUX);
+ add_safe_location((uintptr_t)stdout, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
+ add_safe_location((uintptr_t)stderr, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
+ add_safe_location((uintptr_t)stdin, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
}
size_t get_safe_locations_count() {
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
index fa24ba37f875a71bbdf3d110be9d8054f47d5741..1b34dab3f464665b0b03c0ba6ac6e7a79960aada 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
@@ -34,11 +34,17 @@
#include <stdint.h>
#include <stddef.h>
-/* Simple representation of a safe location */
+/*! Simple representation of a safe location */
struct memory_location {
- uintptr_t address; /* Address */
- uintptr_t length; /* Byte-length */
- int is_initialized; /* Notion of initialization */
+ /*! Address */
+ uintptr_t address;
+ /*! Byte-length */
+ uintptr_t length;
+ /*! Notion of initialization */
+ int is_initialized;
+ /*! True if the address is on static memory, false if it is on dynamic
+ memory */
+ int is_on_static;
};
typedef struct memory_location memory_location;
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
index 87e369e22b43f37edb1567fb21ffe9f4f204a764..5dfcd7efd90c29821dfd16f131c1531c90a8b7b3 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
@@ -215,8 +215,8 @@ void mspaces_init() {
describe_run();
eacsl_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();
+ Case of the segments available before main. */
+ init_shadow_layout_pre_main();
already_run = 1;
}
}
@@ -235,8 +235,9 @@ void eacsl_memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
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);
+ /* Allocate and log shadow memory layout of the execution. Case of the
+ segments available after main. */
+ init_shadow_layout_main(argc_ref, argv_ref);
//DEBUG_PRINT_LAYOUT;
/* Make sure the layout holds */
DVALIDATE_SHADOW_LAYOUT;
@@ -250,12 +251,14 @@ void eacsl_memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
collect_safe_locations();
int i;
for (i = 0; i < get_safe_locations_count(); i++) {
- memory_location * loc = get_safe_location(i);
- void *addr = (void*)loc->address;
- uintptr_t len = loc->length;
- shadow_alloca(addr, len);
- if (loc->is_initialized)
- eacsl_initialize(addr, len);
+ memory_location * loc = get_safe_location(i);
+ if (loc->is_on_static) {
+ void *addr = (void*)loc->address;
+ uintptr_t len = loc->length;
+ shadow_alloca(addr, len);
+ if (loc->is_initialized)
+ eacsl_initialize(addr, len);
+ }
}
init_infinity_values();
already_run = 1;
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c
index 9be75d5bb9e087c6eda750aed9e13e53c3fc02cd..d6be5cd96e4abbc8a2202e9fa44ad4b7b1139b0d 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c
@@ -20,6 +20,7 @@
/* */
/**************************************************************************/
+#include "../../internals/e_acsl_bits.h"
#include "../../internals/e_acsl_rtl_io.h"
#include "e_acsl_segment_tracking.h"
#include "e_acsl_shadow_layout.h"
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
index 852f1447084e3b2569b4c28eb681abfe3f7bb06b..6e3011ce48c98c4637fcc3259b094df2c0cd8188 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
@@ -345,14 +345,6 @@ void shadow_freea(void *ptr) {
/* Static querying {{{ */
-/*! \brief Checking whether a globally allocated memory block containing an
- * address _addr has read-only access. Note, this is light checking that
- * relies on the fact that a single block cannot contain read/write and
- * read-only parts, that is to check whether the block has read-only access it
- * is sufficient to check any of its bytes. */
-#define global_readonly(_addr) \
- checkbit(READONLY_BIT, (*(char*)PRIMARY_GLOBAL_SHADOW(addr)))
-
int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr) {
unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr);
/* Unless the address belongs to tracked allocation 0 is returned */
@@ -557,7 +549,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
private_assert(mem_spaces.heap_end > max_addr,
"Exceeded heap allocation limit of %luMB\n", E_ACSL_HEAP_SIZE);
- DVALIDATE_MEMORY_INIT;
+ DVALIDATE_MEMORY_PRE_MAIN_INIT;
/* Ensure the shadowed block in on the tracked heap portion */
DVALIDATE_IS_ON_HEAP(((uintptr_t)ptr) - HEAP_SEGMENT, size);
DVALIDATE_ALIGNMENT(ptr); /* Make sure alignment is right */
@@ -664,7 +656,7 @@ void *shadow_copy(const void *ptr, size_t size, int init) {
* \param function - name of the de-allocation function (e.g., `free` or `cfree`)
*/
static void unset_heap_segment(void *ptr, int init, const char *function) {
- DVALIDATE_MEMORY_INIT;
+ DVALIDATE_MEMORY_PRE_MAIN_INIT;
DVALIDATE_FREEABLE(((uintptr_t)ptr));
/* Base address of shadow block */
uintptr_t *base_shadow = (uintptr_t*)HEAP_SHADOW(ptr);
@@ -1134,10 +1126,23 @@ void print_shadow_layout() {
print_memory_partition(&mem_layout.heap);
DLOG(">>> STACK --------------------\n");
print_memory_partition(&mem_layout.stack);
+#if E_ACSL_OS_IS_LINUX
DLOG(">>> GLOBAL -------------------\n");
print_memory_partition(&mem_layout.global);
DLOG(">>> TLS ----------------------\n");
print_memory_partition(&mem_layout.tls);
+#elif E_ACSL_OS_IS_WINDOWS
+ DLOG(">>> TEXT ---------------------\n");
+ print_memory_partition(&mem_layout.text);
+ DLOG(">>> BSS ----------------------\n");
+ print_memory_partition(&mem_layout.bss);
+ DLOG(">>> DATA --------------------\n");
+ print_memory_partition(&mem_layout.data);
+ DLOG(">>> IDATA --------------------\n");
+ print_memory_partition(&mem_layout.idata);
+ DLOG(">>> RDATA --------------------\n");
+ print_memory_partition(&mem_layout.rdata);
+#endif
DLOG(">>> --------------------------\n");
}
@@ -1147,10 +1152,23 @@ const char* which_segment(uintptr_t addr) {
loc = "stack";
else if (IS_ON_HEAP(addr))
loc = "heap";
+#if E_ACSL_OS_IS_LINUX
else if (IS_ON_GLOBAL(addr))
loc = "global";
else if (IS_ON_TLS(addr))
loc = "TLS";
+#elif E_ACSL_OS_IS_WINDOWS
+ else if (IS_ON_TEXT(addr))
+ loc = "text";
+ else if (IS_ON_BSS(addr))
+ loc = "bss";
+ else if (IS_ON_DATA(addr))
+ loc = "data";
+ else if (IS_ON_IDATA(addr))
+ loc = "idata";
+ else if (IS_ON_RDATA(addr))
+ loc = "rdata";
+#endif
else
loc = "untracked";
return loc;
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
index 4379e1cda6f1baa4d0783ba51654a0a788245248..0baf6b56c0f0942270575031dadcf9756bc79db5 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
@@ -114,8 +114,18 @@
DVASSERT(((uintptr_t)_addr) % HEAP_SEGMENT == 0, \
"Heap base address %a is unaligned", _addr)
+#define DVALIDATE_MEMORY_PRE_MAIN_INIT \
+ DVASSERT(mem_layout.is_initialized_pre_main != 0, \
+ "Un-initialized pre-main shadow layout", NULL)
+
+#define DVALIDATE_MEMORY_MAIN_INIT \
+ DVASSERT(mem_layout.is_initialized_main != 0, \
+ "Un-initialized main shadow layout", NULL)
+
#define DVALIDATE_MEMORY_INIT \
- DVASSERT(mem_layout.is_initialized != 0, "Un-initialized shadow layout", NULL)
+ DVASSERT(mem_layout.is_initialized_pre_main != 0 && \
+ mem_layout.is_initialized_main != 0, \
+ "Un-initialized shadow layout", NULL)
/* Debug function making sure that the order of program segments is as expected
* and that the program and the shadow segments used do not overlap. */
@@ -137,12 +147,24 @@ void validate_shadow_layout();
/* Assert that [_addr, _addr+_size] are within stack segment */
#define DVALIDATE_IS_ON_STACK(_addr, _size) \
DVALIDATE_IS_ON(_addr, _size, STACK)
+#if E_ACSL_OS_IS_LINUX
/* Assert that [_addr, _addr+_size] are within global segment */
-#define DVALIDATE_IS_ON_GLOBAL(_addr, _size) \
+# define DVALIDATE_IS_ON_GLOBAL(_addr, _size) \
DVALIDATE_IS_ON(_addr, _size, GLOBAL)
/* Assert that [_addr, _addr+_size] are within TLS segment */
-#define DVALIDATE_IS_ON_TLS(_addr, _size) \
+# define DVALIDATE_IS_ON_TLS(_addr, _size) \
DVALIDATE_IS_ON(_addr, _size, TLS)
+#elif E_ACSL_OS_IS_WINDOWS
+/* Assert that [_addr, _addr+_size] are within text segment */
+# define DVALIDATE_IS_ON_TEXT(_addr, _size) \
+ DVALIDATE_IS_ON(_addr, _size, TEXT)
+/* Assert that [_addr, _addr+_size] are within bss segment */
+# define DVALIDATE_IS_ON_BSS(_addr, _size) \
+ DVALIDATE_IS_ON(_addr, _size, BSS)
+/* Assert that [_addr, _addr+_size] are within idata segment */
+# define DVALIDATE_IS_ON_IDATA(_addr, _size) \
+ DVALIDATE_IS_ON(_addr, _size, IDATA)
+#endif
/* Assert that [_addr, _addr+_size] are within stack, global or TLS segments */
#define DVALIDATE_IS_ON_STATIC(_addr, _size) \
DVALIDATE_IS_ON(_addr, _size, STATIC)
@@ -222,6 +244,8 @@ void validate_shadow_layout();
#else
/*! \cond exclude from doxygen */
+# define DVALIDATE_MEMORY_PRE_MAIN_INIT
+# define DVALIDATE_MEMORY_MAIN_INIT
# define DVALIDATE_MEMORY_INIT
# define DVALIDATE_SHADOW_LAYOUT
# define DVALIDATE_HEAP_ACCESS
@@ -231,8 +255,14 @@ void validate_shadow_layout();
# define DVALIDATE_IS_ON
# define DVALIDATE_IS_ON_HEAP
# define DVALIDATE_IS_ON_STACK
+# if E_ACSL_OS_IS_LINUX
# define DVALIDATE_IS_ON_GLOBAL
# define DVALIDATE_IS_ON_TLS
+# elif E_ACSL_OS_IS_WINDOWS
+# define DVALIDATE_IS_ON_TEXT
+# define DVALIDATE_IS_ON_BSS
+# define DVALIDATE_IS_ON_IDATA
+# endif
# define DVALIDATE_IS_ON_STATIC
# define DVALIDATE_FREEABLE
# define DVALIDATE_STATIC_FREE
@@ -309,6 +339,14 @@ void shadow_freea(void *ptr);
/* Static querying {{{ */
+/*! \brief Checking whether a globally allocated memory block containing an
+ * address _addr has read-only access. Note, this is light checking that
+ * relies on the fact that a single block cannot contain read/write and
+ * read-only parts, that is to check whether the block has read-only access it
+ * is sufficient to check any of its bytes. */
+#define global_readonly(_addr) \
+ checkbit(READONLY_BIT, (*(char*)PRIMARY_GLOBAL_SHADOW(_addr)))
+
/*! \brief Return a non-zero value if a memory region of length `size`
* starting at address `addr` belongs to a tracked stack, tls or
* global memory block and 0 otherwise.
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
index e070180edfc3d7f90a539120704675f210a28a6c..5ddb496007a2074e7581ad6089aca7c4fda0ce56 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
@@ -20,7 +20,6 @@
/* */
/**************************************************************************/
-#include <sys/resource.h>
#include <errno.h>
#include <stddef.h>
@@ -29,8 +28,23 @@
#include "e_acsl_shadow_layout.h"
+#if E_ACSL_OS_IS_LINUX
+
+#include <sys/resource.h>
+
/** Program stack information {{{ */
+/* Symbols exported by the linker script */
+
+/*!\brief The first address past the end of the text segment. */
+extern char etext;
+/*!\brief The first address past the end of the initialized data segment. */
+extern char edata;
+/*!\brief The first address past the end of the uninitialized data segment. */
+extern char end;
+/*!\brief The first address of a program. */
+extern char __executable_start;
+
size_t increase_stack_limit(const size_t size) {
rlim_t stacksz = (rlim_t)size;
struct rlimit rl;
@@ -59,7 +73,15 @@ size_t get_stack_size() {
return rlim.rlim_cur;
}
-uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
+
+extern char ** environ;
+
+/*! \brief Return the greatest (known) address on a program's stack.
+ * This function presently determines the address using the address of the
+ * last string in `environ`. That is, it assumes that argc and argv are
+ * stored below environ, which holds for GCC or Clang and Glibc but is not
+ * necessarily true for some other compilers/libraries. */
+static uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
char **env = environ;
while (env[1])
env++;
@@ -72,74 +94,72 @@ uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
* ::argv_alloca. */
uintptr_t stack_end = addr + ULONG_BITS;
uintptr_t stack_start = stack_end - get_stack_size();
- return stack_start;
-}
-/* }}} */
-/** Program heap information {{{ */
-uintptr_t get_heap_start() {
- return mem_spaces.heap_start;
-}
-
-size_t get_heap_size() {
- return PGM_HEAP_SIZE;
-}
+ // Check that the assumption that argc and argv are stored below environ in
+ // the stack holds
+ DVASSERT(stack_start <= (uintptr_t)argc_ref
+ && (uintptr_t)argc_ref <= stack_end,
+ "Assumption that argc is stored below environ is not verified.\n\
+ \tStack: [%a - %a]\n\t&argc: %a",
+ stack_start, stack_end, argc_ref);
+ DVASSERT(stack_start <= (uintptr_t)argv_ref
+ && (uintptr_t)argv_ref <= stack_end,
+ "Assumption that argv is stored below environ is not verified.\n\
+ \tStack: [%a - %a]\n\t&argc: %a",
+ stack_start, stack_end, argc_ref);
-size_t get_heap_init_size() {
- return get_heap_size()/8;
+ return stack_start;
}
+/* }}} */
-uintptr_t get_global_start() {
+/** Program global information {{{ */
+/*! \brief Return the start address of a segment holding globals (generally
+ * BSS and Data segments). */
+static uintptr_t get_global_start() {
return (uintptr_t)&__executable_start;
}
-size_t get_global_size() {
+/*! \brief Return byte-size of global segment */
+static size_t get_global_size() {
return ((uintptr_t)&end - get_global_start());
}
/** }}} */
-/** Shadow Layout {{{ */
+/** Thread-local storage information {{{ */
-void set_application_segment(memory_segment *seg, uintptr_t start,
- size_t size, const char *name, mspace msp) {
- seg->name = name;
- seg->start = start;
- seg->size = size;
- seg->end = seg->start + seg->size;
- seg->mspace = msp;
- seg->parent = NULL;
- seg->shadow_ratio = 0;
- seg->shadow_offset = 0;
-}
+/*! Thread-local storage (TLS) keeps track of copies of per-thread variables.
+ * Even though at the present stage, E-ACSL's RTL is not thread-safe, some
+ * of the variables (for instance ::errno) are allocated there. In X86, TLS
+ * is typically located somewhere below the program's stack but above mmap
+ * areas. TLS is typically separated into two sections: .tdata and .tbss.
+ * Similar to globals using .data and .bss, .tdata keeps track of initialized
+ * thread-local variables, while .tbss holds uninitialized ones.
+ *
+ * Start and end addresses of TLS are obtained by taking addresses of
+ * initialized and uninitialized variables in TLS (::id_tdata and ::id_tss)
+ * and adding fixed amount of shadow space around them. Visually it looks
+ * as follows:
+ *
+ * end TLS address (&id_tdata + TLS_SHADOW_SIZE/2)
+ * id_tdata address
+ * ...
+ * id_tbss address
+ * start TLS address (&id_bss - TLS_SHADOW_SIZE/2)
+ *
+ * HOWEVER problems can occur if PGM_TLS_SIZE is too big:
+ * see get_tls_start for details.
+ */
-void set_shadow_segment(memory_segment *seg, memory_segment *parent,
- size_t ratio, const char *name) {
- seg->parent = parent;
- seg->name = name;
- seg->shadow_ratio = ratio;
- seg->size = parent->size/seg->shadow_ratio;
- seg->mspace = eacsl_create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0);
- seg->start = (uintptr_t)eacsl_mspace_malloc(seg->mspace,1);
- seg->end = seg->start + seg->size;
- seg->shadow_offset = parent->start - seg->start;
+/*! \brief Return byte-size of the TLS segment */
+inline static size_t get_tls_size() {
+ return PGM_TLS_SIZE;
}
-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);
- /* Changes of the ratio in the following will require changes in get_tls_start */
- set_shadow_segment(&pstack->primary, &pstack->application, 1, "stack_primary");
- set_shadow_segment(&pstack->secondary, &pstack->application, 1, "stack_secondary");
-#ifdef E_ACSL_TEMPORAL
- set_shadow_segment(&pstack->temporal_primary, &pstack->application, 1, "temporal_stack_primary");
- set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1, "temporal_stack_secondary");
-#endif
-
- mem_layout.is_initialized = 1;
-}
+static __thread int id_tdata = 1;
+static __thread int id_tbss;
-uintptr_t get_tls_start() {
+/*! \brief Return start address of a program's TLS */
+static uintptr_t get_tls_start() {
size_t tls_size = get_tls_size();
uintptr_t data = (uintptr_t)&id_tdata,
bss = (uintptr_t)&id_tbss;
@@ -173,17 +193,10 @@ uintptr_t get_tls_start() {
return tls_start_half > max_shadow ? tls_start_half : max_shadow;
}
-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 partitions {{{ */
+static void init_shadow_layout_global() {
memory_partition *pglobal = &mem_layout.global;
set_application_segment(&pglobal->application, get_global_start(),
get_global_size(), "global", NULL);
@@ -193,7 +206,9 @@ void init_shadow_layout_heap_global_tls() {
set_shadow_segment(&pglobal->temporal_primary, &pglobal->application, 1, "temporal_global_primary");
set_shadow_segment(&pglobal->temporal_secondary, &pglobal->application, 1, "temporal_global_secondary");
#endif
+}
+static void init_shadow_layout_tls() {
memory_partition *ptls = &mem_layout.tls;
set_application_segment(&ptls->application, get_tls_start(),
get_tls_size(), "tls", NULL);
@@ -203,12 +218,260 @@ void init_shadow_layout_heap_global_tls() {
set_shadow_segment(&ptls->temporal_primary, &ptls->application, 1, "temporal_tls_primary");
set_shadow_segment(&ptls->temporal_secondary, &ptls->application, 1, "temporal_tls_secondary");
#endif
+}
+
+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);
+ /* Changes of the ratio in the following will require changes in get_tls_start */
+ set_shadow_segment(&pstack->primary, &pstack->application, 1, "stack_primary");
+ set_shadow_segment(&pstack->secondary, &pstack->application, 1, "stack_secondary");
+#ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&pstack->temporal_primary, &pstack->application, 1, "temporal_stack_primary");
+ set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1, "temporal_stack_secondary");
+#endif
+}
+/** }}} */
+#elif E_ACSL_OS_IS_WINDOWS
+
+#include <processthreadsapi.h>
+#include <windows.h>
+#include <dbghelp.h>
+
+
+/** Program segment informations {{{ */
+typedef struct mem_loc_info {
+ uintptr_t start;
+ size_t size;
+} mem_loc_info_t;
+
+static mem_loc_info_t get_section_info(HANDLE hModule, const char * section_name) {
+ // Get the location of the module's IMAGE_NT_HEADERS structure
+ IMAGE_NT_HEADERS *pNtHdr = ImageNtHeader(hModule);
+
+ // Section table immediately follows the IMAGE_NT_HEADERS
+ IMAGE_SECTION_HEADER *pSectionHdr = (IMAGE_SECTION_HEADER *)(pNtHdr + 1);
+
+ const char* imageBase = (const char*)hModule;
+ size_t scnNameSize = sizeof(pSectionHdr->Name);
+ char scnName[scnNameSize + 1];
+ // Enforce nul-termination for scn names that are the whole length of
+ // pSectionHdr->Name[]
+ scnName[scnNameSize] = '\0';
+
+ mem_loc_info_t res = { .start = 0, .size = 0 };
+
+ for (int scn = 0; scn < pNtHdr->FileHeader.NumberOfSections; ++scn, ++pSectionHdr) {
+ // Note: pSectionHdr->Name[] is 8-byte long. If the scn name is 8-byte
+ // long, ->Name[] will not be nul-terminated. For this reason, copy it to a
+ // local buffer that is nul-terminated to be sure we only print the real scn
+ // name, and no extra garbage beyond it.
+ strncpy(scnName, (const char*)pSectionHdr->Name, scnNameSize);
+
+ if (strcmp(scnName, section_name) == 0) {
+ res.start = (uintptr_t)imageBase + pSectionHdr->VirtualAddress;
+ res.size = pSectionHdr->Misc.VirtualSize;
+ break;
+ }
+ }
+
+ return res;
+}
+/** }}} */
+
+/** Program stack information {{{ */
+static mem_loc_info_t get_stack_mem_loc_info() {
+ ULONG_PTR low;
+ ULONG_PTR high;
+ GetCurrentThreadStackLimits(&low, &high);
+ return (mem_loc_info_t) {
+ .start = low,
+ .size = high - low + 1
+ };
+}
+
+size_t increase_stack_limit(const size_t size) {
+ size_t actual_size = get_stack_size();
+ if (actual_size < size) {
+ DLOG("Increasing stack size at runtime is unsupported on Windows.\n\
+ \t Actual stack size: %lu\n\
+ \tRequested stack size: %lu\n",
+ actual_size, size);
+ }
+ return actual_size;
+}
+
+size_t get_stack_size() {
+ return get_stack_mem_loc_info().size;
+}
+/** }}} */
+
+/** Memory partitions {{{ */
+static void init_shadow_layout_stack(int *argc_ref, char ***argv_ref) {
+ memory_partition *pstack = &mem_layout.stack;
+ mem_loc_info_t stack_loc_info = get_stack_mem_loc_info();
+ set_application_segment(&pstack->application, stack_loc_info.start,
+ stack_loc_info.size, "stack", NULL);
+ set_shadow_segment(&pstack->primary, &pstack->application, 1, "stack_primary");
+ set_shadow_segment(&pstack->secondary, &pstack->application, 1, "stack_secondary");
+#ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&pstack->temporal_primary, &pstack->application, 1, "temporal_stack_primary");
+ set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1, "temporal_stack_secondary");
+#endif
+}
+
+static void init_shadow_layout_text(HMODULE module) {
+ // Retrieve mem loc info for the text section
+ mem_loc_info_t text = get_section_info(module, ".text");
+
+ memory_partition *ptext = &mem_layout.text;
+ set_application_segment(&ptext->application, text.start,
+ text.size, "text", NULL);
+ set_shadow_segment(&ptext->primary, &ptext->application, 1, "text_primary");
+ set_shadow_segment(&ptext->secondary, &ptext->application, 1, "text_secondary");
+#ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&ptext->temporal_primary, &ptext->application, 1, "temporal_text_primary");
+ set_shadow_segment(&ptext->temporal_secondary, &ptext->application, 1, "temporal_text_secondary");
+#endif
+}
+
+static void init_shadow_layout_bss(HMODULE module) {
+ // Retrieve mem loc info for the uninidialized data segment
+ mem_loc_info_t bss = get_section_info(module, ".bss");
+
+ memory_partition *pbss = &mem_layout.bss;
+ set_application_segment(&pbss->application, bss.start, bss.size, "bss", NULL);
+ set_shadow_segment(&pbss->primary, &pbss->application, 1, "bss_primary");
+ set_shadow_segment(&pbss->secondary, &pbss->application, 1, "bss_secondary");
+#ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&pbss->temporal_primary, &pbss->application, 1, "temporal_bss_primary");
+ set_shadow_segment(&pbss->temporal_secondary, &pbss->application, 1, "temporal_bss_secondary");
+#endif
+}
+
+static void init_shadow_layout_data(HMODULE module) {
+ // Retrieve mem loc info for the initialized data segment
+ mem_loc_info_t data = get_section_info(module, ".data");
+
+ memory_partition *pdata = &mem_layout.data;
+ set_application_segment(&pdata->application, data.start, data.size, "data", NULL);
+ set_shadow_segment(&pdata->primary, &pdata->application, 1, "data_primary");
+ set_shadow_segment(&pdata->secondary, &pdata->application, 1, "data_secondary");
+#ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&pdata->temporal_primary, &pdata->application, 1, "temporal_data_primary");
+ set_shadow_segment(&pdata->temporal_secondary, &pdata->application, 1, "temporal_data_secondary");
+#endif
+}
+
+static void init_shadow_layout_idata(HMODULE module) {
+ // Retrieve mem loc info for the initialized data segment
+ mem_loc_info_t idata = get_section_info(module, ".idata");
+
+ memory_partition *pidata = &mem_layout.idata;
+ set_application_segment(&pidata->application, idata.start, idata.size, "idata", NULL);
+ set_shadow_segment(&pidata->primary, &pidata->application, 1, "idata_primary");
+ set_shadow_segment(&pidata->secondary, &pidata->application, 1, "idata_secondary");
+#ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&pidata->temporal_primary, &pidata->application, 1, "temporal_idata_primary");
+ set_shadow_segment(&pidata->temporal_secondary, &pidata->application, 1, "temporal_idata_secondary");
+#endif
+}
+
+static void init_shadow_layout_rdata(HMODULE module) {
+ // Retrieve mem loc info for the initialized data segment
+ mem_loc_info_t rdata = get_section_info(module, ".rdata");
+
+ memory_partition *prdata = &mem_layout.rdata;
+ set_application_segment(&prdata->application, rdata.start, rdata.size, "rdata", NULL);
+ set_shadow_segment(&prdata->primary, &prdata->application, 1, "rdata_primary");
+ set_shadow_segment(&prdata->secondary, &prdata->application, 1, "rdata_secondary");
+#ifdef E_ACSL_TEMPORAL
+ set_shadow_segment(&prdata->temporal_primary, &prdata->application, 1, "temporal_rdata_primary");
+ set_shadow_segment(&prdata->temporal_secondary, &prdata->application, 1, "temporal_rdata_secondary");
+#endif
+}
+/** }}} */
+#endif
+
+/** Program heap information {{{ */
+static uintptr_t get_heap_start() {
+ return mem_spaces.heap_start;
+}
+
+size_t get_heap_size() {
+ return PGM_HEAP_SIZE;
+}
+
+static size_t get_heap_init_size() {
+ return get_heap_size()/8;
+}
+
+static void init_shadow_layout_heap() {
+ 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
+}
+/** }}} */
+
+/** Shadow Layout {{{ */
+
+void set_application_segment(memory_segment *seg, uintptr_t start,
+ size_t size, const char *name, mspace msp) {
+ seg->name = name;
+ seg->start = start;
+ seg->size = size;
+ seg->end = seg->start + seg->size;
+ seg->mspace = msp;
+ seg->parent = NULL;
+ seg->shadow_ratio = 0;
+ seg->shadow_offset = 0;
+}
+
+void set_shadow_segment(memory_segment *seg, memory_segment *parent,
+ size_t ratio, const char *name) {
+ seg->parent = parent;
+ seg->name = name;
+ seg->shadow_ratio = ratio;
+ seg->size = parent->size/seg->shadow_ratio;
+ seg->mspace = eacsl_create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0);
+ seg->start = (uintptr_t)eacsl_mspace_malloc(seg->mspace,1);
+ seg->end = seg->start + seg->size;
+ seg->shadow_offset = parent->start - seg->start;
+}
+
+void init_shadow_layout_pre_main() {
+ init_shadow_layout_heap();
+
+#if E_ACSL_OS_IS_LINUX
+ init_shadow_layout_global();
+ init_shadow_layout_tls();
+#elif E_ACSL_OS_IS_WINDOWS
+ HANDLE module = GetModuleHandle(NULL);
+ init_shadow_layout_text(module);
+ init_shadow_layout_bss(module);
+ init_shadow_layout_data(module);
+ init_shadow_layout_idata(module);
+ init_shadow_layout_rdata(module);
+#endif
+
+ mem_layout.is_initialized_pre_main = 1;
+}
+
+void init_shadow_layout_main(int *argc_ref, char *** argv_ref) {
+ init_shadow_layout_stack(argc_ref, argv_ref);
- mem_layout.is_initialized = 1;
+ mem_layout.is_initialized_main = 1;
}
void clean_shadow_layout() {
- if (mem_layout.is_initialized) {
+ if (mem_layout.is_initialized_pre_main && mem_layout.is_initialized_main) {
int i;
for (i = 0; i < sizeof(mem_partitions)/sizeof(memory_partition*); i++) {
if (mem_partitions[i]->primary.mspace)
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
index b15415383d498ef48e84b392a5e6323cbbac5912..93dc849c54d3710c0b0a95581551d5b3e9a687ef 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
@@ -30,6 +30,7 @@
#include <stddef.h>
#include <stdint.h>
+#include "../../internals/e_acsl_config.h"
#include "../../internals/e_acsl_malloc.h"
/* Default size of a program's heap tracked via shadow memory */
@@ -42,21 +43,6 @@
#define E_ACSL_STACK_SIZE 64
#endif
-/* Symbols exported by the linker script */
-
-/*!\brief The first address past the end of the text segment. */
-extern char etext;
-/*!\brief The first address past the end of the initialized data segment. */
-extern char edata;
-/*!\brief The first address past the end of the uninitialized data segment. */
-extern char end;
-/*!\brief The first address of a program. */
-extern char __executable_start;
-
-/* \cond */
-void *sbrk(intptr_t increment);
-char *strerror(int errnum);
-
/* MAP_ANONYMOUS is a mmap flag indicating that the contents of allocated blocks
* should be nullified. Set value from <bits/mman-linux.h>, if MAP_ANONYMOUS is
* undefined */
@@ -95,43 +81,7 @@ char *strerror(int errnum);
#define SHADOW_SEGMENT_PADDING (512*KB)
/* }}} */
-/** Thread-local storage information {{{ */
-
-/*! Thread-local storage (TLS) keeps track of copies of per-thread variables.
- * Even though at the present stage RTL of E-ACSL is not thread-safe, some
- * of the variables (for instance ::errno) are allocated there. In X86 TLS
- * is typically located somewhere below the program's stack but above mmap
- * areas. TLS is typically separated into two sections: .tdata and .tbss.
- * Similar to globals using .data and .bss, .tdata keeps track of initialized
- * thread-local variables, while .tbss holds uninitialized ones.
- *
- * Start and end addresses of TLS are obtained by taking addresses of
- * initialized and uninitialized variables in TLS (::id_tdata and ::id_tss)
- * and adding fixed amount of shadow space around them. Visually it looks
- * as follows:
- *
- * end TLS address (&id_tdata + TLS_SHADOW_SIZE/2)
- * id_tdata address
- * ...
- * id_tbss address
- * start TLS address (&id_bss - TLS_SHADOW_SIZE/2)
- *
- * HOWEVER problems can occur if PGM_TLS_SIZE is too big:
- * see get_tls_start for details.
- */
-
-/*! \brief Return byte-size of the TLS segment */
-inline static size_t get_tls_size() {
- return PGM_TLS_SIZE;
-}
-
-static __thread int id_tdata = 1;
-static __thread int id_tbss;
-
-/* }}} */
-
/** Program stack information {{{ */
-extern char ** environ;
/*! \brief Set a new soft stack limit
*
@@ -149,35 +99,11 @@ size_t increase_stack_limit(const size_t size);
/*! \brief Return byte-size of a program's stack. The return value is the soft
* stack limit, i.e., it can be programmatically increased at runtime. */
size_t get_stack_size();
-
-/*! \brief Return greatest (known) address on a program's stack.
- * This function presently determines the address using the address of the
- * last string in `environ`. That is, it assumes that argc and argv are
- * stored below environ, which holds for GCC/Glibc but is not necessarily
- * true for some other compilers/libraries. */
-uintptr_t get_stack_start(int *argc_ref, char *** argv_ref);
/* }}} */
/** Program heap information {{{ */
-/*! \brief Return the start address of a program's heap. */
-uintptr_t get_heap_start();
-
/*! \brief Return the tracked size of a program's heap. */
size_t get_heap_size();
-
-/*! \brief Return the size of a secondary shadow region tracking
- * initialization (i.e., init shadow). */
-size_t get_heap_init_size();
-
-/** }}} */
-
-/** Program global information {{{ */
-/*! \brief Return the start address of a segment holding globals (generally
- * BSS and Data segments). */
-uintptr_t get_global_start();
-
-/*! \brief Return byte-size of global segment */
-size_t get_global_size();
/** }}} */
/** Shadow Layout {{{ */
@@ -257,20 +183,48 @@ typedef struct memory_partition memory_partition;
struct memory_layout {
memory_partition heap;
memory_partition stack;
+#if E_ACSL_OS_IS_LINUX
+ // On linux
+ // The text, bss and data segments are contiguous and regrouped here in a
+ // global memory partition
memory_partition global;
+ // The TLS is in a specific section and identifiable
memory_partition tls;
- int is_initialized;
+#elif E_ACSL_OS_IS_WINDOWS
+ // On windows
+ // The text, bss and data segments are not necessarily contiguous so each one
+ // is in its own memory partition
+ memory_partition text;
+ memory_partition bss;
+ memory_partition data;
+ memory_partition idata;
+ memory_partition rdata;
+ // The TLS is stored on the heap and is indistiguishable from it
+#endif
+ int is_initialized_pre_main;
+ int is_initialized_main;
};
/*! \brief Full program memory layout. */
-struct memory_layout mem_layout;
+struct memory_layout mem_layout = {
+ .is_initialized_pre_main = 0,
+ .is_initialized_main = 0,
+};
/*! \brief Array of used partitions */
memory_partition *mem_partitions [] = {
&mem_layout.heap,
&mem_layout.stack,
+#if E_ACSL_OS_IS_LINUX
&mem_layout.global,
- &mem_layout.tls
+ &mem_layout.tls,
+#elif E_ACSL_OS_IS_WINDOWS
+ &mem_layout.text,
+ &mem_layout.bss,
+ &mem_layout.data,
+ &mem_layout.idata,
+ &mem_layout.rdata,
+#endif
};
/*! \brief Initialize an application memory segment.
@@ -296,17 +250,18 @@ 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.
- Case of the stack. */
-void init_shadow_layout_stack(int *argc_ref, char ***argv_ref);
-
-/*! \brief Return start address of a program's TLS */
-uintptr_t get_tls_start();
+ *
+ * Case of segments available before main (for instance from a function marked
+ * as `__constructor__`). */
+void init_shadow_layout_pre_main();
/*! \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. */
-void init_shadow_layout_heap_global_tls();
+ *
+ * Case of segments only available once inside of main (for instance the stack
+ * of the program). */
+void init_shadow_layout_main(int *argc_ref, char ***argv_ref);
/*! \brief Deallocate shadow regions used by runtime analysis */
void clean_shadow_layout();
@@ -333,10 +288,23 @@ void clean_shadow_layout();
#define heap_secondary_offset mem_layout.heap.secondary.shadow_offset
#define stack_primary_offset mem_layout.stack.primary.shadow_offset
#define stack_secondary_offset mem_layout.stack.secondary.shadow_offset
-#define global_primary_offset mem_layout.global.primary.shadow_offset
-#define global_secondary_offset mem_layout.global.secondary.shadow_offset
-#define tls_primary_offset mem_layout.tls.primary.shadow_offset
-#define tls_secondary_offset mem_layout.tls.secondary.shadow_offset
+#if E_ACSL_OS_IS_LINUX
+# define global_primary_offset mem_layout.global.primary.shadow_offset
+# define global_secondary_offset mem_layout.global.secondary.shadow_offset
+# define tls_primary_offset mem_layout.tls.primary.shadow_offset
+# define tls_secondary_offset mem_layout.tls.secondary.shadow_offset
+#elif E_ACSL_OS_IS_WINDOWS
+# define text_primary_offset mem_layout.text.primary.shadow_offset
+# define text_secondary_offset mem_layout.text.secondary.shadow_offset
+# define bss_primary_offset mem_layout.bss.primary.shadow_offset
+# define bss_secondary_offset mem_layout.bss.secondary.shadow_offset
+# define data_primary_offset mem_layout.data.primary.shadow_offset
+# define data_secondary_offset mem_layout.data.secondary.shadow_offset
+# define idata_primary_offset mem_layout.idata.primary.shadow_offset
+# define idata_secondary_offset mem_layout.idata.secondary.shadow_offset
+# define rdata_primary_offset mem_layout.rdata.primary.shadow_offset
+# define rdata_secondary_offset mem_layout.rdata.secondary.shadow_offset
+#endif
/*! \brief Compute a shadow address using displacement offset
* @param _addr - an application space address
@@ -374,29 +342,97 @@ void clean_shadow_layout();
#define SECONDARY_STACK_SHADOW(_addr) \
SHADOW_ACCESS(_addr, stack_secondary_offset)
+#if E_ACSL_OS_IS_LINUX
/*! \brief Convert a global address into its primary shadow counterpart */
-#define PRIMARY_GLOBAL_SHADOW(_addr) \
+# define PRIMARY_GLOBAL_SHADOW(_addr) \
SHADOW_ACCESS(_addr, global_primary_offset)
/*! \brief Convert a global address into its secondary shadow counterpart */
-#define SECONDARY_GLOBAL_SHADOW(_addr) \
+# define SECONDARY_GLOBAL_SHADOW(_addr) \
SHADOW_ACCESS(_addr, global_secondary_offset)
/*! \brief Convert a TLS address into its primary shadow counterpart */
-#define PRIMARY_TLS_SHADOW(_addr) \
+# define PRIMARY_TLS_SHADOW(_addr) \
SHADOW_ACCESS(_addr, tls_primary_offset)
/*! \brief Convert a TLS address into its secondary shadow counterpart */
-#define SECONDARY_TLS_SHADOW(_addr) \
+# define SECONDARY_TLS_SHADOW(_addr) \
SHADOW_ACCESS(_addr, tls_secondary_offset)
+#elif E_ACSL_OS_IS_WINDOWS
+/*! \brief Convert a text address into its primary shadow counterpart */
+# define PRIMARY_TEXT_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, text_primary_offset)
+
+/*! \brief Convert a text address into its secondary shadow counterpart */
+# define SECONDARY_TEXT_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, text_secondary_offset)
+
+/*! \brief Convert a bss address into its primary shadow counterpart */
+# define PRIMARY_BSS_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, bss_primary_offset)
+
+/*! \brief Convert a bss address into its secondary shadow counterpart */
+# define SECONDARY_BSS_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, bss_secondary_offset)
+
+/*! \brief Convert an data address into its primary shadow counterpart */
+# define PRIMARY_DATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, data_primary_offset)
+
+/*! \brief Convert an data address into its secondary shadow counterpart */
+# define SECONDARY_DATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, data_secondary_offset)
+
+/*! \brief Convert an idata address into its primary shadow counterpart */
+# define PRIMARY_IDATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, idata_primary_offset)
+
+/*! \brief Convert an idata address into its secondary shadow counterpart */
+# define SECONDARY_IDATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, idata_secondary_offset)
+
+/*! \brief Convert an rdata address into its primary shadow counterpart */
+# define PRIMARY_RDATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, rdata_primary_offset)
+
+/*! \brief Convert an rdata address into its secondary shadow counterpart */
+# define SECONDARY_RDATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, rdata_secondary_offset)
+
+/*! \brief Convert a global address into its primary shadow counterpart */
+# define PRIMARY_GLOBAL_SHADOW(_addr) \
+ (IS_ON_TEXT(_addr) ? PRIMARY_TEXT_SHADOW(_addr) : \
+ IS_ON_BSS(_addr) ? PRIMARY_BSS_SHADOW(_addr) : \
+ IS_ON_DATA(_addr) ? PRIMARY_DATA_SHADOW(_addr) : \
+ IS_ON_IDATA(_addr) ? PRIMARY_IDATA_SHADOW(_addr) : \
+ IS_ON_RDATA(_addr) ? PRIMARY_RDATA_SHADOW(_addr) : (intptr_t)0)
+
+/*! \brief Convert a global address into its secondary shadow counterpart */
+# define SECONDARY_GLOBAL_SHADOW(_addr) \
+ (IS_ON_TEXT(_addr) ? SECONDARY_TEXT_SHADOW(_addr) : \
+ IS_ON_BSS(_addr) ? SECONDARY_BSS_SHADOW(_addr) : \
+ IS_ON_DATA(_addr) ? SECONDARY_DATA_SHADOW(_addr) : \
+ IS_ON_IDATA(_addr) ? SECONDARY_IDATA_SHADOW(_addr) : \
+ IS_ON_RDATA(_addr) ? SECONDARY_RDATA_SHADOW(_addr) : (intptr_t)0)
+#endif
/* \brief Compute a primary or a secondary shadow address (based on the value of
* parameter `_region`) of an address tracked via an offset-based encoding.
* For an untracked address `0` is returned. */
-#define SHADOW_REGION_ADDRESS(_addr, _region) \
- (IS_ON_STACK(_addr) ? _region##_STACK_SHADOW(_addr) : \
- IS_ON_GLOBAL(_addr) ? _region##_GLOBAL_SHADOW(_addr) : \
- IS_ON_TLS(_addr) ? _region##_TLS_SHADOW(_addr) : 0)
+#if E_ACSL_OS_IS_LINUX
+# define SHADOW_REGION_ADDRESS(_addr, _region) \
+ (IS_ON_STACK(_addr) ? _region##_STACK_SHADOW(_addr) : \
+ IS_ON_GLOBAL(_addr) ? _region##_GLOBAL_SHADOW(_addr) : \
+ IS_ON_TLS(_addr) ? _region##_TLS_SHADOW(_addr) : (intptr_t)0)
+#elif E_ACSL_OS_IS_WINDOWS
+# define SHADOW_REGION_ADDRESS(_addr, _region) \
+ (IS_ON_STACK(_addr) ? _region##_STACK_SHADOW(_addr) : \
+ IS_ON_TEXT(_addr) ? _region##_TEXT_SHADOW(_addr) : \
+ IS_ON_BSS(_addr) ? _region##_BSS_SHADOW(_addr) : \
+ IS_ON_DATA(_addr) ? _region##_DATA_SHADOW(_addr) : \
+ IS_ON_IDATA(_addr) ? _region##_IDATA_SHADOW(_addr) : \
+ IS_ON_RDATA(_addr) ? _region##_RDATA_SHADOW(_addr) : (intptr_t)0)
+#endif
/*! \brief Primary shadow address of a non-dynamic region */
#define PRIMARY_SHADOW(_addr) SHADOW_REGION_ADDRESS(_addr, PRIMARY)
@@ -422,22 +458,50 @@ void clean_shadow_layout();
/*! \brief Evaluate to true if `_addr` is a stack address */
#define IS_ON_STACK(_addr) IS_ON(_addr, mem_layout.stack.application)
+#if E_ACSL_OS_IS_LINUX
/*! \brief Evaluate to true if `_addr` is a global address */
-#define IS_ON_GLOBAL(_addr) IS_ON(_addr, mem_layout.global.application)
+# define IS_ON_GLOBAL(_addr) IS_ON(_addr, mem_layout.global.application)
/*! \brief Evaluate to true if _addr is a TLS address */
-#define IS_ON_TLS(_addr) IS_ON(_addr, mem_layout.tls.application)
+# define IS_ON_TLS(_addr) IS_ON(_addr, mem_layout.tls.application)
/*! \brief Shortcut for evaluating an address via ::IS_ON_STACK,
* ::IS_ON_GLOBAL or ::IS_ON_TLS */
-#define IS_ON_STATIC(_addr) \
- (IS_ON_STACK(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
+# define IS_ON_STATIC(_addr) \
+ (IS_ON_STACK(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
+#elif E_ACSL_OS_IS_WINDOWS
+/*! \brief Evaluate to true if `_addr` is a text address */
+# define IS_ON_TEXT(_addr) IS_ON(_addr, mem_layout.text.application)
+
+/*! \brief Evaluate to true if `_addr` is a bss address */
+# define IS_ON_BSS(_addr) IS_ON(_addr, mem_layout.bss.application)
+
+/*! \brief Evaluate to true if `_addr` is an idata address */
+# define IS_ON_DATA(_addr) IS_ON(_addr, mem_layout.data.application)
+
+/*! \brief Evaluate to true if `_addr` is an idata address */
+# define IS_ON_IDATA(_addr) IS_ON(_addr, mem_layout.idata.application)
+
+/*! \brief Evaluate to true if `_addr` is an rdata address */
+# define IS_ON_RDATA(_addr) IS_ON(_addr, mem_layout.rdata.application)
+
+/*! \brief Evaluate to true if `_addr` is a global address */
+# define IS_ON_GLOBAL(_addr) \
+ (IS_ON_TEXT(_addr) || IS_ON_BSS(_addr) || IS_ON_DATA(_addr) || \
+ IS_ON_IDATA(_addr) || IS_ON_RDATA(_addr))
+
+/*! \brief Shortcut for evaluating an address via ::IS_ON_STACK,
+ * ::IS_ON_TEXT, :: IS_ON_BSS, ::IS_ON_IDATA, or ::IS_ON_RDATA */
+# define IS_ON_STATIC(_addr) \
+ (IS_ON_STACK(_addr) || IS_ON_TEXT(_addr) || IS_ON_BSS(_addr) || \
+ IS_ON_DATA(_addr) || IS_ON_IDATA(_addr) || IS_ON_RDATA(_addr))
+#endif
/*! \brief Evaluate to a true value if a given address belongs to tracked
- * allocation (i.e., found within tls, stack, heap or globally) */
+ * allocation (i.e., found within static or dynamic allocation) */
#define IS_ON_VALID(_addr) \
- (IS_ON_STACK(_addr) || IS_ON_HEAP(_addr) || \
- IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
+ (IS_ON_STATIC(_addr) || IS_ON_HEAP(_addr))
+
/* }}} */
#ifdef E_ACSL_TEMPORAL /* {{{ */
@@ -453,21 +517,79 @@ void clean_shadow_layout();
#define TEMPORAL_SECONDARY_STACK_SHADOW(_addr) \
SHADOW_ACCESS(_addr, mem_layout.stack.temporal_secondary.shadow_offset)
+#if E_ACSL_OS_IS_LINUX
/*! \brief Convert a global address into its primary temporal shadow counterpart */
-#define TEMPORAL_PRIMARY_GLOBAL_SHADOW(_addr) \
- SHADOW_ACCESS(_addr, mem_layout.global.temporal_primary.shadow_offset)
+# define TEMPORAL_PRIMARY_GLOBAL_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.global.temporal_primary.shadow_offset)
/*! \brief Convert a global address into its primary temporal shadow counterpart */
-#define TEMPORAL_SECONDARY_GLOBAL_SHADOW(_addr) \
- SHADOW_ACCESS(_addr, mem_layout.global.temporal_secondary.shadow_offset)
+# define TEMPORAL_SECONDARY_GLOBAL_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.global.temporal_secondary.shadow_offset)
/*! \brief Convert a TLS address into its primary temporal shadow counterpart */
-#define TEMPORAL_PRIMARY_TLS_SHADOW(_addr) \
- SHADOW_ACCESS(_addr, mem_layout.tls.temporal_primary.shadow_offset)
+# define TEMPORAL_PRIMARY_TLS_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.tls.temporal_primary.shadow_offset)
/*! \brief Convert a TLS address into its secondary temporal shadow counterpart */
-#define TEMPORAL_SECONDARY_TLS_SHADOW(_addr) \
- SHADOW_ACCESS(_addr, mem_layout.tls.temporal_secondary.shadow_offset)
+# define TEMPORAL_SECONDARY_TLS_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.tls.temporal_secondary.shadow_offset)
+#elif E_ACSL_OS_IS_WINDOWS
+/*! \brief Convert a text address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_TEXT_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.text.temporal_primary.shadow_offset)
+
+/*! \brief Convert a text address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_TEXT_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.text.temporal_secondary.shadow_offset)
+
+/*! \brief Convert a bss address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_BSS_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.bss.temporal_primary.shadow_offset)
+
+/*! \brief Convert a bss address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_BSS_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.bss.temporal_secondary.shadow_offset)
+
+/*! \brief Convert an data address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_DATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.data.temporal_primary.shadow_offset)
+
+/*! \brief Convert an data address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_DATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.data.temporal_secondary.shadow_offset)
+
+/*! \brief Convert an idata address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_IDATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.idata.temporal_primary.shadow_offset)
+
+/*! \brief Convert an idata address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_IDATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.idata.temporal_secondary.shadow_offset)
+
+/*! \brief Convert an rdata address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_RDATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.rdata.temporal_primary.shadow_offset)
+
+/*! \brief Convert an rdata address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_RDATA_SHADOW(_addr) \
+ SHADOW_ACCESS(_addr, mem_layout.rdata.temporal_secondary.shadow_offset)
+
+/*! \brief Convert a global address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_GLOBAL_SHADOW(_addr) \
+ (IS_ON_TEXT(_addr) ? TEMPORAL_PRIMARY_TEXT_SHADOW(_addr) : \
+ IS_ON_BSS(_addr) ? TEMPORAL_PRIMARY_BSS_SHADOW(_addr) : \
+ IS_ON_DATA(_addr) ? TEMPORAL_PRIMARY_DATA_SHADOW(_addr) : \
+ IS_ON_IDATA(_addr) ? TEMPORAL_PRIMARY_IDATA_SHADOW(_addr) : \
+ IS_ON_RDATA(_addr) ? TEMPORAL_PRIMARY_RDATA_SHADOW(_addr) : (intptr_t)0)
+
+/*! \brief Convert a global address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_GLOBAL_SHADOW(_addr) \
+ (IS_ON_TEXT(_addr) ? TEMPORAL_SECONDARY_TEXT_SHADOW(_addr) : \
+ IS_ON_BSS(_addr) ? TEMPORAL_SECONDARY_BSS_SHADOW(_addr) : \
+ IS_ON_DATA(_addr) ? TEMPORAL_SECONDARY_DATA_SHADOW(_addr) : \
+ IS_ON_IDATA(_addr) ? TEMPORAL_SECONDARY_IDATA_SHADOW(_addr) : \
+ IS_ON_RDATA(_addr) ? TEMPORAL_SECONDARY_RDATA_SHADOW(_addr) : (intptr_t)0)
+#endif
/*! \brief Temporal primary shadow address of a non-dynamic region */
#define TEMPORAL_PRIMARY_STATIC_SHADOW(_addr) \
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index 671ea306b1f641e8cacba62184345c3256d526fd..ea38062b647d72c07d3ef2942cdef132c60e8a6a 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -260,7 +260,7 @@ let to_exp ~loc kf env pot label =
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
- Smart_stmt.lib_call ~loc
+ Smart_stmt.call ~loc
~result:(Cil.var vi)
"malloc"
[ e_size ]
@@ -273,7 +273,7 @@ let to_exp ~loc kf env pot label =
| Typing.(Rational | Real | Nan) ->
Error.not_yet "quantification over non-integer type"
in
- let free_stmt = Smart_stmt.lib_call ~loc "free" [e] in
+ let free_stmt = Smart_stmt.call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var].
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 8a2b5385f1cb1830a92ff5272cb14bd0cd3d7c69..cfc504740298f8517998be505a7512b21b9e50a4 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -33,7 +33,7 @@ let apply_on_var ~loc funname e =
else if Gmp_types.Q.is_t ty then "__gmpq_"
else assert false
in
- Smart_stmt.lib_call ~loc (prefix ^ funname) [ e ]
+ Smart_stmt.rtl_call ~loc ~prefix funname [ e ]
let init ~loc e = apply_on_var "init" ~loc e
let clear ~loc e = apply_on_var "clear" ~loc e
@@ -90,7 +90,7 @@ let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
let suf, args = get_set_suffix_and_arg ty e in
- Smart_stmt.lib_call ~loc (fname ^ suf) (ev :: args)
+ Smart_stmt.rtl_call ~loc ~prefix:"" (fname ^ suf) (ev :: args)
end else
Smart_stmt.assigns ~loc:e.eloc ~result:lv e
@@ -111,7 +111,8 @@ let init_set ~loc lv ev e =
| Lval elv ->
assert (Gmp_types.Z.is_t (Cil.typeOf ev));
let call =
- Smart_stmt.lib_call ~loc
+ Smart_stmt.rtl_call ~loc
+ ~prefix:""
"__gmpz_import"
[ ev;
Cil.one ~loc;
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 38166949656b8f5e50598e58004cac88cca831ed..524df6755b2c5334a2db69a67b89e771eda1e1c3 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -159,8 +159,9 @@ let gmp_to_sizet ~loc kf env size p =
sizet
(fun vi _ ->
[ Smart_stmt.runtime_check Smart_stmt.RTE kf guard p;
- Smart_stmt.lib_call ~loc
+ Smart_stmt.rtl_call ~loc
~result:(Cil.var vi)
+ ~prefix:""
"__gmpz_get_ui"
[ size ] ])
in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 2f4417b0191213b6730879074147a5f66f68fe43..0af7f3b0697137395bd885f1e88f797bc4943209 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -148,8 +148,9 @@ let add_cast ~loc ?name e env kf ty =
None
Cil.doubleType
(fun v _ ->
- [ Smart_stmt.lib_call ~loc
+ [ Smart_stmt.rtl_call ~loc
~result:(Cil.var v)
+ ~prefix:""
"__gmpq_get_d"
[ e ] ])
in
@@ -197,7 +198,11 @@ let cmp ~loc bop e1 e2 env kf t_opt =
~name
Cil.intType
(fun v _ ->
- [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var v)
+ ~prefix:""
+ fname
+ [ e1; e2 ] ])
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
@@ -226,7 +231,10 @@ let binop ~loc bop e1 e2 env kf t_opt =
[e2] *)
let e1, env = create ~loc e1 env kf None in
let e2, env = create ~loc e2 env kf None in
- let mk_stmts _ e = [ Smart_stmt.lib_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
+ ~prefix:""
+ name
+ [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env = new_var_and_init ~loc ~name env kf t_opt mk_stmts in
e, env
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index 984188546901494f65d6ab58fc6a88919f95dc49..2c3497df87388788c01f9b46c4b751bb24bc240f 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -30,7 +30,7 @@ let stmt sk = Cil.mkStmt ~valid_sid:true sk
let instr i = stmt (Instr i)
let block_stmt blk = stmt (Block blk)
let block_from_stmts stmts = block_stmt (Cil.mkBlock stmts)
-let call ~loc ?result e args = instr (Call(result, e, args, loc))
+let call_instr ~loc ?result e args = instr (Call(result, e, args, loc))
let assigns ~loc ~result e = instr (Set(result, e, loc))
@@ -68,13 +68,7 @@ let block stmt b = match b.bstmts with
(* E-ACSL specific code *)
(* ********************************************************************** *)
-let lib_call ~loc ?result fname args =
- let vi =
- try Rtl.Symbols.find_vi fname
- with Rtl.Symbols.Unregistered _ as exn ->
- try Builtins.find fname
- with Not_found -> raise exn
- in
+let do_call ~loc ?result vi args =
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
let make_args ~variadic args param_ty =
@@ -95,7 +89,7 @@ let lib_call ~loc ?result fname args =
Options.fatal
"Mismatch between the number of expressions given and the number \
of arguments in the signature when calling function '%s'"
- fname
+ vi.vname
in
List.rev (make_rev_args [] args param_ty)
in
@@ -104,10 +98,27 @@ let lib_call ~loc ?result fname args =
| TFun(_, None, _, _) -> []
| _ -> assert false
in
- call ~loc ?result f args
+ call_instr ~loc ?result f args
+
+let call ~loc ?result fname args =
+ let kf =
+ try Globals.Functions.find_by_name fname
+ with Not_found ->
+ Options.fatal "Unable to find function '%s'" fname
+ in
+ let vi = Globals.Functions.get_vi kf in
+ do_call ~loc ?result vi args
-let rtl_call ~loc ?result fname args =
- lib_call ~loc ?result (Functions.RTL.mk_api_name fname) args
+let rtl_call ~loc ?result ?(prefix=Functions.RTL.api_prefix) fname args =
+ let fname = prefix ^ fname in
+ let vi =
+ try Rtl.Symbols.find_vi fname
+ with Rtl.Symbols.Unregistered _ as exn ->
+ try Builtins.find fname
+ with Not_found ->
+ raise exn
+ in
+ do_call ~loc ?result vi args
(* ************************************************************************** *)
(** {2 Handling the E-ACSL's C-libraries, part II} *)
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index 3aebb9f4cc27419db8d9337096af57fb2d3cebb6..abd797824e97d0e018a076089db1919abbab50cc 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
@@ -56,15 +56,22 @@ val break: loc:location -> stmt
(* E-ACSL specific code: build calls to its RTL API *)
(* ********************************************************************** *)
-val lib_call: loc:location -> ?result:lval -> string -> exp list -> stmt
+val call: loc:location -> ?result:lval -> string -> exp list -> stmt
+(** Construct a call to a function with the given name.
+ @raise Not_found if the given string does not represent a function in the
+ AST, for instance if the function does not exist. *)
+
+val rtl_call:
+ loc:location -> ?result:lval -> ?prefix:string -> string -> exp list -> stmt
(** Construct a call to a library function with the given name.
+
+ [prefix] defaults to the E-ACSL RTL API prefix and can be explicitely
+ provided to call functions without this prefix.
+
@raise Rtl.Symbols.Unregistered if the given string does not represent
such a function or if library functions were never registered (only possible
when using E-ACSL through its API). *)
-val rtl_call: loc:location -> ?result:lval -> string -> exp list -> stmt
-(** Special version of [lib_call] for E-ACSL's RTL functions. *)
-
val store_stmt: ?str_size:exp -> varinfo -> stmt
(** Construct a call to [__e_acsl_store_block] that observes the allocation of
the given varinfo. See [share/e-acsl/e_acsl.h] for details about this
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index d0f6ced85f13d7305efda530e904f39ae1dd8cfc..f56c6d4837ff97b473c525cca032457295cdb14c 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -75,13 +75,13 @@ module Mk: sig
end = struct
let store_reference ~loc flow lhs rhs =
+ let prefix = RTL.temporal_prefix in
let fname = match flow with
| Direct -> "store_nblock"
| Indirect -> "store_nreferent"
| Copy -> Options.fatal "Copy flow type in store_reference"
in
- let fname = RTL.mk_temporal_name fname in
- Smart_stmt.lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ Cil.mkAddrOf ~loc lhs; rhs ]
let save_param ~loc flow lhs pos =
let infix = match flow with
@@ -89,17 +89,19 @@ end = struct
| Indirect -> "nreferent"
| Copy -> "copy"
in
+ let prefix = RTL.temporal_prefix in
let fname = "save_" ^ infix ^ "_parameter" in
- let fname = RTL.mk_temporal_name fname in
- Smart_stmt.lib_call ~loc fname [ lhs ; Cil.integer ~loc pos ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ lhs ; Cil.integer ~loc pos ]
let pull_param ~loc vi pos =
+ let prefix = RTL.temporal_prefix in
+ let fname = "pull_parameter" in
let exp = Cil.mkAddrOfVi vi in
- let fname = RTL.mk_temporal_name "pull_parameter" in
let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
- Smart_stmt.lib_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ exp ; Cil.integer ~loc pos ; sz ]
let handle_return_referent ~save ~loc lhs =
+ let prefix = RTL.temporal_prefix in
let fname = match save with
| true -> "save_return"
| false -> "pull_return"
@@ -108,15 +110,17 @@ end = struct
(match (Cil.typeOf lhs) with
| TPtr _ -> ()
| _ -> Error.not_yet "Struct in return");
- Smart_stmt.lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ lhs ]
let reset_return_referent ~loc =
- Smart_stmt.lib_call ~loc (RTL.mk_temporal_name "reset_return") []
+ let prefix = RTL.temporal_prefix in
+ Smart_stmt.rtl_call ~loc ~prefix "reset_return" []
let temporal_memcpy_struct ~loc lhs rhs =
- let fname = RTL.mk_temporal_name "memcpy" in
+ let prefix = RTL.temporal_prefix in
+ let fname = "memcpy" in
let size = Cil.sizeOf ~loc (Cil.typeOfLval lhs) in
- Smart_stmt.lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
end
(* }}} *)
@@ -301,12 +305,13 @@ end = struct
associated with memcpy/memset call *)
let call_memxxx current_stmt loc args fexp env kf =
if Libc.is_memcpy fexp || Libc.is_memset fexp then
+ let prefix = RTL.temporal_prefix in
let name = match fexp.enode with
| Lval(Var vi, _) -> vi.vname
| _ -> Options.fatal "[Temporal.call_memxxx] not a left-value"
in
let stmt =
- Smart_stmt.lib_call ~loc (RTL.mk_temporal_name name) args
+ Smart_stmt.rtl_call ~loc ~prefix name args
in
Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else
@@ -320,8 +325,11 @@ end = struct
it makes sense to make this somewhat-debug-level-call. In production mode
the implementation of the function should be empty and compiler should
be able to optimize that code out. *)
- let name = (RTL.mk_temporal_name "reset_parameters") in
- let stmt = Smart_stmt.lib_call ~loc name [] in
+ let stmt =
+ let prefix = RTL.temporal_prefix in
+ let name = "reset_parameters" in
+ Smart_stmt.rtl_call ~loc ~prefix name []
+ in
let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
let stmt = Mk.reset_return_referent ~loc in
let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2570aa9bbfb2c6436d373bf25d5c4c3ddbaab96f..8d7be521858fa77177cee84e5e5f194ffce896e5 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -135,7 +135,11 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
None
new_ty
(fun v _ ->
- [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e ] ])
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var v)
+ ~prefix:""
+ fname
+ [ e ] ])
in
e, env
else if Gmp_types.Q.is_t ty || strnum = Str_R then
@@ -297,7 +301,7 @@ and context_insensitive_term_to_exp kf env t =
kf
~name:vname
(Some t)
- (fun _ ev -> [ Smart_stmt.lib_call ~loc name [ ev; e ] ])
+ (fun _ ev -> [ Smart_stmt.rtl_call ~loc ~prefix:"" name [ ev; e ] ])
in
e, env, C_number, ""
else if Gmp_types.Q.is_t ty then
@@ -326,7 +330,10 @@ and context_insensitive_term_to_exp kf env t =
let e2, env = term_to_exp kf env t2 in
if Gmp_types.Z.is_t ty then
let name = name_of_mpz_arith_bop bop in
- let mk_stmts _ e = [ Smart_stmt.lib_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
+ ~prefix:""
+ name
+ [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env =
Env.new_var_and_mpz_init ~loc ~name env kf (Some t) mk_stmts
@@ -371,7 +378,7 @@ and context_insensitive_term_to_exp kf env t =
p
in
Env.add_assert kf cond p;
- let instr = Smart_stmt.lib_call ~loc name [ e; e1; e2 ] in
+ let instr = Smart_stmt.rtl_call ~loc ~prefix:"" name [ e; e1; e2 ] in
[ cond; instr ]
in
let name = Misc.name_of_binop bop in
@@ -429,7 +436,7 @@ and context_insensitive_term_to_exp kf env t =
(fun vi _e ->
let result = Cil.var vi in
let fname = "__gmpz_fits_ulong_p" in
- [ Smart_stmt.lib_call ~loc ~result fname [ e2 ] ])
+ [ Smart_stmt.rtl_call ~loc ~result ~prefix:"" fname [ e2 ] ])
in
e, env
in
@@ -459,7 +466,7 @@ and context_insensitive_term_to_exp kf env t =
in
let result = Cil.var vi in
let name = "__gmpz_get_ui" in
- let instr = Smart_stmt.lib_call ~loc ~result name [ e2 ] in
+ let instr = Smart_stmt.rtl_call ~loc ~result ~prefix:"" name [ e2 ] in
[ coerce_guard_cond; instr ]
in
let name = e2_name ^ bop_name ^ "_coerced" in
@@ -478,7 +485,10 @@ and context_insensitive_term_to_exp kf env t =
(* Create the shift instruction *)
let mk_shift_instr result_e =
let name = name_of_mpz_arith_bop bop in
- Smart_stmt.lib_call ~loc name [ result_e; e1; e2_as_bitcnt_e ]
+ Smart_stmt.rtl_call ~loc
+ ~prefix:""
+ name
+ [ result_e; e1; e2_as_bitcnt_e ]
in
(* Put t in an option to use with comparison_to_exp and
@@ -569,7 +579,7 @@ and context_insensitive_term_to_exp kf env t =
if Gmp_types.Z.is_t ty then
let mk_stmts _v e =
let name = name_of_mpz_arith_bop bop in
- let instr = Smart_stmt.lib_call ~loc name [ e; e1; e2 ] in
+ let instr = Smart_stmt.rtl_call ~loc ~prefix:"" name [ e; e1; e2 ] in
[ instr ]
in
let name = Misc.name_of_binop bop in
@@ -648,7 +658,11 @@ and context_insensitive_term_to_exp kf env t =
(Some t)
(Misc.cty (Extlib.the li.l_type))
(fun vi _ ->
- [ Smart_stmt.lib_call ~loc ~result:(Cil.var vi) fname args ])
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var vi)
+ ~prefix:""
+ fname
+ args ])
else
(* build the arguments and compute the integer_ty of the parameters *)
let params_ty, args, env =
@@ -797,8 +811,9 @@ and comparison_to_exp
~name
Cil.intType
(fun v _ ->
- [ Smart_stmt.lib_call ~loc
+ [ Smart_stmt.rtl_call ~loc
~result:(Cil.var v)
+ ~prefix:""
"__gmpz_cmp"
[ e1; e2 ] ])
in
diff --git a/src/plugins/e-acsl/src/libraries/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml
index 37cf8f8319f67d966635e0704b8ed32bd6a5f91e..4a82689a9640e376c84f739cf32cf3c0b6844697 100644
--- a/src/plugins/e-acsl/src/libraries/functions.ml
+++ b/src/plugins/e-acsl/src/libraries/functions.ml
@@ -63,14 +63,14 @@ let has_fundef exp = match exp.enode with
module RTL = struct
(* prefix of all functions/variables from the public E-ACSL API *)
- let e_acsl_api_prefix = "__e_acsl_"
+ let api_prefix = "__e_acsl_"
(* prefix of temporal analysis functions of the public E-ACSL API *)
- let e_acsl_temporal_prefix = e_acsl_api_prefix ^ "temporal_"
+ let temporal_prefix = api_prefix ^ "temporal_"
(* prefix of all builtin functions/variables from the public E-ACSL API,
Builtin functions replace original calls in programs. *)
- let e_acsl_builtin_prefix = e_acsl_api_prefix ^ "builtin_"
+ let e_acsl_builtin_prefix = api_prefix ^ "builtin_"
(* prefix of functions/variables generated by E-ACSL *)
let e_acsl_gen_prefix = "__gen_e_acsl_"
@@ -78,9 +78,9 @@ module RTL = struct
(* prefix of literal strings generated by E-ACSL *)
let e_acsl_lit_string_prefix = e_acsl_gen_prefix ^ "literal_string"
- let mk_api_name fname = e_acsl_api_prefix ^ fname
+ let mk_api_name fname = api_prefix ^ fname
- let mk_temporal_name fname = e_acsl_temporal_prefix ^ fname
+ let mk_temporal_name fname = temporal_prefix ^ fname
let mk_gen_name name = e_acsl_gen_prefix ^ name
diff --git a/src/plugins/e-acsl/src/libraries/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli
index 4963870c28539b1b89d055be1bb0285158b71366..f2d66cb65e8309f057da05db34d3338a3951c3ef 100644
--- a/src/plugins/e-acsl/src/libraries/functions.mli
+++ b/src/plugins/e-acsl/src/libraries/functions.mli
@@ -38,6 +38,12 @@ val instrument: kernel_function -> bool
(* ************************************************************************** *)
module RTL: sig
+ val api_prefix: string
+ (** Prefix used for the public API of E-ACSL runtime library. *)
+
+ val temporal_prefix:string
+ (** Prefix used for the public API of E-ACSL runtime library dealing with
+ temporal analysis. *)
val mk_api_name: string -> string
(** Prefix a name (of a variable or a function) with a string that identifies