From 2055ea913f5a15d8386539fe977480dbb8fb15ee Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 18 Oct 2021 18:17:42 +0200
Subject: [PATCH] [eacsl] Add option to support concurrency
---
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 20 +++++++++++++---
src/plugins/e-acsl/src/options.ml | 30 ++++++++++++++++++++++++
src/plugins/e-acsl/src/options.mli | 1 +
3 files changed, 48 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 4094ebaa8ee..9090b64dbd8 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -310,7 +310,7 @@ check_getopt;
LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:,
frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,full-mtracking,gmp,
quiet,logfile:,ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,keep-going,
- frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,
+ frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,concurrency,
print-mmodels,rt-debug,rte-select:,then,e-acsl-extra:,check,fail-with-code:,
temporal,weak-validity,stack-size:,heap-size:,rt-verbose,free-valid-address,
external-assert:,assert-print-data,no-assert-print-data,external-print-value:,
@@ -342,7 +342,8 @@ OPTION_OUTPUT_EXEC="a.out" # Generated executable name
OPTION_EACSL_OUTPUT_EXEC="" # Name of E-ACSL executable
OPTION_EACSL="-e-acsl" # Specifies E-ACSL run
OPTION_FRAMA_STDLIB="-no-frama-c-stdlib" # Use Frama-C stdlib
-OPTION_FULL_MTRACKING= # Instrument as much as possible
+OPTION_FULL_MTRACKING= # Instrument as much as possible
+OPTION_CONCURRENCY= # Activate concurrency support
OPTION_GMP= # Use GMP integers everywhere
OPTION_EACSL_MMODELS="segment" # Memory model used
OPTION_EACSL_SHARE= # Custom E-ACSL share directory
@@ -553,6 +554,11 @@ do
shift;
OPTION_GMP="-e-acsl-gmp-only"
;;
+ # Concurrency support
+ --concurrency)
+ shift;
+ OPTION_CONCURRENCY="-e-acsl-concurrency"
+ ;;
# Supply Frama-C executable name
-I|--frama-c)
shift;
@@ -844,6 +850,12 @@ else
OPT_LDFLAGS=""
fi
+# Concurrency support
+if [ -n "$OPTION_CONCURRENCY" ]; then
+ OPT_CPPFLAGS="$OPT_CPPFLAGS -DE_ACSL_CONCURRENCY_PTHREAD"
+ OPT_LDFLAGS="$OPT_LDFLAGS -pthread"
+fi
+
# Gcc and related flags
CC="$OPTION_CC"
CFLAGS="$OPTION_CFLAGS
@@ -873,7 +885,8 @@ if [ "`basename $CC`" = 'clang' ]; then
-Wno-incompatible-pointer-types-discards-qualifiers"
fi
-CPPFLAGS="$OPTION_CPPFLAGS"
+CPPFLAGS="$OPTION_CPPFLAGS
+ $OPT_CPPFLAGS"
LDFLAGS="$OPTION_LDFLAGS
$OPT_LDFLAGS"
@@ -993,6 +1006,7 @@ if [ -n "$OPTION_EACSL" ]; then
$OPTION_DEBUG
$OPTION_VALIDATE_FORMAT_STRINGS
$OPTION_ASSERT_PRINT_DATA
+ $OPTION_CONCURRENCY
-e-acsl-share="$EACSL_SHARE"
-then-last"
fi
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 900473331b6..7752a5ccf2c 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -108,6 +108,14 @@ module Assert_print_data =
the runtime error message"
end)
+module Concurrency =
+ False
+ (struct
+ let option_name = "-e-acsl-concurrency"
+ let help = "activate the concurrency support of E-ACSL. The option \
+ implies -e-acsl-full-mtracking."
+ end)
+
module Functions =
Kernel_function_set
(struct
@@ -203,6 +211,28 @@ let setup ?(rtl=false) () =
end
end
end;
+ (* Concurrency support *)
+ if Concurrency.get () then begin
+ if Full_mtracking.is_set () && not (Full_mtracking.get ()) then
+ abort
+ "The memory tracking dataflow analysis is incompatible@ \
+ with the concurrency support of E-ACSL.@ \
+ Please use option '-e-acsl-full-mtracking'.";
+ if not rtl && not (Full_mtracking.is_set ()) then
+ feedback
+ "Due to the large number of function pointers in concurrent@ \
+ code, the memory tracking dataflow analysis is deactivated@ \
+ when activating the concurrency support of E-ACSL.";
+ Full_mtracking.on ();
+ if Temporal_validity.get () then
+ abort
+ "The temporal analysis in valid annotations is incompatible@ \
+ with the concurrency support of E-ACSL.@ \
+ Please use '-e-acsl-no-temporal-validity' or '-e-acsl-no-concurrency'@ \
+ to deactivate one or the other.";
+ if rtl then
+ Kernel.CppExtraArgs.add "-DE_ACSL_CONCURRENCY_PTHREAD"
+ end;
(* Additionnal kernel options while parsing the RTL project. *)
if rtl then begin
Kernel.Keep_unused_specified_functions.off ();
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index b0a91ccbc3b..3fe0a48115f 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -32,6 +32,7 @@ module Temporal_validity: Parameter_sig.Bool
module Validate_format_strings: Parameter_sig.Bool
module Replace_libc_functions: Parameter_sig.Bool
module Assert_print_data: Parameter_sig.Bool
+module Concurrency: Parameter_sig.Bool
module Functions: Parameter_sig.Kernel_function_set
module Instrument: Parameter_sig.Kernel_function_set
--
GitLab