[eacsl] Add code generation support for concurrency

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 ../../../../.."

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 ../../../../.."

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

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 *)

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 ../../../../.."