Hotfix: thread arguments in Alias backend

Author: TDacik

common/src/concurrency_model/ConcurrencyModel.ml

@@ -119,5 +119,8 @@ let classify_stmt stmt = match stmt.skind with
   | Return _ -> Return
   | _ -> Other
 
+let get_thread_arg stmt = match classify_stmt stmt with
+  | Thread_create (_, _, arg) -> arg
+
 let is_atomic_fn var =
   AtomicFunctions.exists (fun a -> Str.string_match (Str.regexp a) var.vname 0)

common/src/concurrency_model/ConcurrencyModel.mli

@@ -39,4 +39,6 @@ type stmt =
 
 val classify_stmt : Stmt.t -> stmt
 
+val get_thread_arg : Stmt.t -> Exp.t
+
 val is_atomic_fn : Varinfo.t -> bool

common/src/thread_analysis/ThreadAnalysis.ml

@@ -224,8 +224,13 @@ module Make (ValueAnalysis : VALUE_ANALYSIS) = struct
       (Stmt.Set.cardinal stmts)
       Core0.pp_globals (fst initial');
 
+    let args =
+      Stmt.Set.elements stmts
+      |> List.map ConcurrencyModel.get_thread_arg
+      |> Exp.Set.of_list
+    in
     ValueAnalysis.set_active_thread parent;
-    ValueAnalysis.update_thread child initial';
+    ValueAnalysis.update_thread child args initial';
     initial'
 
   module WTO = Graph.WeakTopological.Make(ThreadGraph)
@@ -313,8 +318,6 @@ module Make (ValueAnalysis : VALUE_ANALYSIS) = struct
     graph := res.thread_graph;
     let res = compute_fixpoint res in
 
-    ValueAnalysis.set_escaped_bases res.escaped_bases;
-
     Logger.feedback "%a" ThreadAnalysis0.pp_short res;
     Logger.debug ~level:3 "Thread analysis: %a" pp res;
     Logger.debug ~level:3 "Active threads: %s" (ThreadAnalysis0.show_stmt_summaries res);

common/src/value_analysis/AliasF.ml

@@ -5,20 +5,34 @@
  *
  * Author: Tomas Dacik (idacik@fit.vut.cz), 2024 *)
 
-
+open Cil_types
 open Cil_datatype
 
 module Self = struct
 
   let name = "alias"
 
+  module Logger = Core0.Logger(struct let dkey = "alias" end)
+
   (** Include references to active thread and initial states. *)
   include ValueAnalysis_Base.Make ()
 
+  let compute () =
+    Alias.Analysis.compute ();
+    let print_kf_alias_sets kf =
+      if Kernel_function.has_definition kf then
+        let alias_sets = Alias.API.Function.alias_sets_lvals ~kf in
+        List.iter (fun lset ->
+          Logger.debug "%a: %a" Kernel_function.pretty kf Alias.API.LSet.pretty lset
+        ) alias_sets
+      else ()
+    in
+    Globals.Functions.iter print_kf_alias_sets
+
   let init main =
     init main;
     Syntactic.init main;
-    Alias.Analysis.compute ()
+    compute ()
 
   let set_active_thread thread =
     set_active_thread thread;
@@ -36,23 +50,47 @@ module Self = struct
   let eval_expr = Syntactic.Self.eval_expr
   let stmt_state = Syntactic.Self.stmt_state
 
+  let lval_to_base lval = match lval with
+    | Var var, NoOffset -> Base.of_varinfo var
+    | _, _ -> failwith "TODO"
+
+  (** TODO: this is a quick fix for issue with thread arguments *)
+  let process_thread_arg thread base =
+    if BaseUtils.is_thread_arg thread base then base
+    else try
+      Thread.Map.find thread !thread_args
+      |> Exp.Set.elements
+      |> List.map Cil.extract_varinfos_from_exp
+      |> List.map Varinfo.Set.elements
+      |> List.concat
+      |> List.hd
+      |> Base.of_varinfo
+    with _ -> base
+
   let choose_representant keep_local lval base varset =
     let thread = get_active_thread () in
-    try
-      Varinfo.Set.elements varset
-      |> List.map Base.of_varinfo
+    let aliases =
+      LvalStructEq.Set.elements varset
+      |> List.map lval_to_base
       |> List.filter (fun base -> keep_local || BaseUtils.keep_for_racer thread base)
-      |> List.hd
-    with _ -> base
+    in
+    let representant =
+      if List.is_empty aliases then base
+      else List.hd aliases
+    in
+    process_thread_arg thread representant
+
 
   let normalise_address keep_local stmt (base, offset) =
     let lval = Cil.var @@ Base.to_varinfo base in
-    let aliases = Alias.API.Statement.points_to_vars ~stmt lval in
+    let kf = Kernel_function.find_englobing_kf stmt in
+    let state = Option.get @@ Alias.API.get_state_before_stmt kf stmt in
+    let aliases = Alias.API.Abstract_state.find_synonyms lval state in
     Core0.debug "Aliases of %a (as lval: %a) at %a: %a"
       Base.pretty base
       LvalStructEq.pretty lval
       Print_utils.pretty_stmt_short stmt
-      Varinfo.Set.pretty aliases;
+      LvalStructEq.Set.pretty aliases;
     choose_representant keep_local lval base aliases, offset
 
   (** Apply aliases:
@@ -73,10 +111,15 @@ module Self = struct
 
   let memory_accesses ?(local=false) stmt =
     let reads, writes = Syntactic.memory_accesses ~local:true stmt in
+
+    Format.printf "Memory accesses at %a:\n" Print_utils.pretty_stmt_short stmt;
+    List.iter (fun m -> Format.printf " - r: %s\n" (MemoryAddress.show m)) reads;
+    List.iter (fun m -> Format.printf " - w: %s\n" (MemoryAddress.show m)) writes;
+
     (normalise stmt reads, normalise stmt writes)
 
   let expr_reads ?(local=false) stmt expr =
-    Syntactic.expr_reads ~local stmt expr
+    Syntactic.expr_reads ~local:true stmt expr
     |> normalise stmt
 
 end

common/src/value_analysis/Syntactic.ml

@@ -132,13 +132,13 @@ module Self = struct
     |> List.filter (fun (base, _) -> (BaseUtils.keep_for_racer thread base))
 
   let memory_accesses ?(local=false) stmt =
-    try
+    (*try
       Logger.debug "R: %a : %a" Stmt.pretty stmt Locations.Zone.pretty (Inout.stmt_inputs stmt);
       Logger.debug "W: %a : %a" Stmt.pretty stmt Locations.Zone.pretty (Inout.stmt_outputs stmt);
       let reads = get_accesses local @@ Inout.stmt_inputs stmt in
       let writes = get_accesses local @@ Inout.stmt_outputs stmt in
       (reads, writes)
-    with _ ->
+    with _ ->*)
       let reads = compute_reads local stmt in
       let writes = compute_writes local stmt in
       (reads, writes)

common/src/value_analysis/ValueAnalysis_Base.ml

@@ -2,20 +2,24 @@
  *
  * Author: Tomas Dacik (idacik@fit.vut.cz), 2024 *)
 
+open Cil_datatype
+
 module Make () = struct
 
   let main_thread : Thread.t option ref = ref None
   let active_thread : Thread.t option ref = ref None
   let thread_states = ref (Thread.Map.empty : Thread.InitialState.t Thread.Map.t)
-  let escaped_bases: Base.t list ref = ref []
+  let thread_args = ref (Thread.Map.empty : Exp.Set.t Thread.Map.t)
 
   let init main =
     let main = Thread.mk main in
     main_thread := Some main;
     active_thread := Some main;
-    thread_states := Thread.Map.singleton main Thread.InitialState.bottom
+    thread_states := Thread.Map.singleton main Thread.InitialState.bottom;
+    thread_args := Thread.Map.singleton main Exp.Set.empty
 
-  let update_thread thread state =
+  let update_thread thread args state =
+    thread_args := Thread.Map.add thread args !thread_args;
     try
       let old = Thread.Map.find thread !thread_states in
       let join = Thread.InitialState.join state old in
@@ -34,7 +38,4 @@ module Make () = struct
     try Thread.Map.find thread !thread_states
     with Not_found -> Thread.InitialState.bottom
 
-  let set_escaped_bases bases =
-    escaped_bases := bases
-
 end

common/src/value_analysis/ValueAnalysis_sig.mli

@@ -41,12 +41,10 @@ module type VALUE_ANALYSIS = sig
 
   include VALUE_ANALYSIS_BASE
 
-  val update_thread : Thread.t -> Thread.InitialState.t -> unit
+  val update_thread : Thread.t -> Exp.Set.t -> Thread.InitialState.t -> unit
 
   val set_active_thread : Thread.t -> unit
 
   val get_active_thread : unit -> Thread.t
 
-  val set_escaped_bases : Base.t list -> unit
-
 end