From 59ada6044d3ee99fcde58999dd4953cb59afc0f5 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 18 Oct 2021 18:19:19 +0200
Subject: [PATCH] [eacsl] Add code generation support for concurrency
---
.../e-acsl/src/analyses/memory_tracking.ml | 58 +++++++++++++------
.../e-acsl/src/analyses/memory_tracking.mli | 18 ++++++
.../e-acsl/src/code_generator/injector.ml | 12 ++++
src/plugins/e-acsl/src/libraries/functions.ml | 9 +++
.../e-acsl/src/libraries/functions.mli | 14 +++++
5 files changed, 93 insertions(+), 18 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index fcfc5c3d3bb..6237f181b57 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -731,6 +731,17 @@ let consolidated_must_monitor_vi vi =
Env.consolidated_mem vi
end
+let concurrent_function_ref = ref None
+
+let abort_because_of_concurrent ~loc vi =
+ Cil.CurrentLoc.set loc;
+ Options.abort
+ ~current:true
+ "Found concurrent function %a and monitored memory properties.\n\
+ Please use option '-e-acsl-concurrency' to add concurrency support."
+ Printer.pp_varinfo vi
+
+
let must_monitor_vi ?kf ?stmt vi =
let _kf = match kf, stmt with
| None, None | Some _, _ -> kf
@@ -739,26 +750,29 @@ let must_monitor_vi ?kf ?stmt vi =
(* [JS 2013/05/07] that is unsound to take the env from the given stmt in
presence of aliasing with an address (see tests address.i).
TODO: could be optimized though *)
- consolidated_must_monitor_vi vi
-(* match stmt, kf with
- | None, _ -> consolidated_must_monitor_vi vi
- | Some _, None ->
- assert false
- | Some stmt, Some kf ->
- if not (Env.is_consolidated ()) then
- ignore (consolidated_must_monitor_vi vi);
- try
- let tbl = Env.find kf in
+ let res = consolidated_must_monitor_vi vi in
+ (* match stmt, kf with
+ | None, _ -> consolidated_must_monitor_vi vi
+ | Some _, None ->
+ assert false
+ | Some stmt, Some kf ->
+ if not (Env.is_consolidated ()) then
+ ignore (consolidated_must_monitor_vi vi);
try
- let set = Stmt.Hashtbl.find tbl stmt in
- Varinfo.Hptset.mem vi (Env.default_varinfos set)
+ let tbl = Env.find kf in
+ try
+ let set = Stmt.Hashtbl.find tbl stmt in
+ Varinfo.Hptset.mem vi (Env.default_varinfos set)
+ with Not_found ->
+ (* new statement *)
+ consolidated_must_monitor_vi vi
with Not_found ->
- (* new statement *)
- consolidated_must_monitor_vi vi
- with Not_found ->
- (* [kf] is dead code *)
- false
-*)
+ (* [kf] is dead code *)
+ false
+ *)
+ match res, !concurrent_function_ref with
+ | true, Some (loc, vi) -> abort_because_of_concurrent ~loc vi
+ | _, _ -> res
let rec apply_on_vi_base_from_lval f ?kf ?stmt = function
| Var vi, _ -> f ?kf ?stmt vi
@@ -823,6 +837,14 @@ let use_monitoring () =
|| Options.Full_mtracking.get ()
|| Env.has_heap_allocations ()
+let found_concurrent_function ~loc vi =
+ if use_monitoring () then
+ abort_because_of_concurrent ~loc vi
+ else
+ match !concurrent_function_ref with
+ | None -> concurrent_function_ref := Some (loc, vi)
+ | Some _ -> ()
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.mli b/src/plugins/e-acsl/src/analyses/memory_tracking.mli
index 78e29d61ecc..4a90e24f50b 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.mli
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.mli
@@ -42,6 +42,24 @@ val must_monitor_lval: ?kf:kernel_function -> ?stmt:stmt -> lval -> bool
val must_monitor_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
(** Same as {!must_model_vi}, for expressions *)
+val found_concurrent_function: loc:location -> varinfo -> unit
+(** [found_concurrent_function ~loc fvi] signals to the memory tracking
+ sub-system that a concurrent function [fvi] has been found at [loc] while
+ parsing the sources. This function needs only to be called if the
+ concurrency support of E-ACSL is deactivated.
+
+ If the memory monitoring is in use when a concurrent function is found,
+ abort the parsing: the user needs to activate the concurrency support.
+
+ Otherwise store the information of the first concurrent function found.
+ Later if the memory monitoring is used because of memory properties to
+ verify, then abort the parsing: the user needs to activate the concurrency
+ support.
+
+ In summary, an analyzed source code can be concurrent with the concurrency
+ support of E-ACSL deactivated only if no memory properties are to be
+ verified. *)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 528ce36f51b..fe2bb263fc6 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -60,6 +60,18 @@ let rename_caller ~loc caller args =
in
fvi, args
end
+ else if Functions.Concurrency.has_replacement caller.vorig_name then
+ if Options.Concurrency.get () then
+ let fvi =
+ Rtl.Symbols.replacement
+ ~get_name:Functions.Concurrency.replacement_name
+ caller
+ in
+ fvi, args
+ else begin
+ Memory_tracking.found_concurrent_function ~loc caller;
+ caller, args
+ end
else if Options.Validate_format_strings.get ()
&& Functions.Libc.is_printf_name caller.vorig_name then
(* rewrite names of format functions (such as printf). This case differs
diff --git a/src/plugins/e-acsl/src/libraries/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml
index d44745b0694..1d44e2869d6 100644
--- a/src/plugins/e-acsl/src/libraries/functions.ml
+++ b/src/plugins/e-acsl/src/libraries/functions.ml
@@ -212,6 +212,15 @@ module Libc = struct
end
+module Concurrency = struct
+ let has_replacement fn =
+ match fn with
+ | "pthread_create" -> true
+ | _ -> false
+
+ let replacement_name fn = RTL.api_prefix ^ fn
+end
+
let check kf =
(* [kf] is monitored iff all functions must be monitored or [kf] belongs to
the white list *)
diff --git a/src/plugins/e-acsl/src/libraries/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli
index c2d1453c34e..f5d13814748 100644
--- a/src/plugins/e-acsl/src/libraries/functions.mli
+++ b/src/plugins/e-acsl/src/libraries/functions.mli
@@ -181,6 +181,20 @@ module Libc: sig
end (* Libc *)
+(* ************************************************************************** *)
+(** {2 Concurrency} Operations concerning the support of concurrency *)
+(* ************************************************************************** *)
+
+module Concurrency: sig
+ val has_replacement: string -> bool
+ (** Given the name of C library function return true if there is a drop-in
+ replacement function for it in the RTL. *)
+
+ val replacement_name: string -> string
+ (** Given the name of C library function return the name of the RTL function
+ that potentially replaces it. *)
+end (* Concurrency *)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
--
GitLab