Pass ctx to context & Simplify callstring-based approaches

src/analyses/abortUnless.ml

@@ -13,7 +13,8 @@ struct
   module D = BoolDomain.MustBool
   module C = Printable.Unit
 
-  let context _ _ = ()
+  let context ctx _ _ = ()
+  let startcontext () = ()
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =

src/analyses/accessAnalysis.ml

@@ -14,7 +14,7 @@ struct
   let name () = "access"
 
   module D = Lattice.Unit
-  module C = Printable.Unit
+  include Analyses.ValueContexts(D)
 
   module V =
   struct
@@ -52,11 +52,12 @@ struct
     );
     if M.tracing then M.traceu "access" "access_one_top"
 
+
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
   let threadenter ctx ~multiple lval f args = [()]
   let exitstate  v = ()
-  let context fd d = ()
+  let context ctx fd d = ()
 
 
   (** Transfer functions: *)

src/analyses/activeSetjmp.ml

@@ -10,7 +10,7 @@ struct
   let name () = "activeSetjmp"
 
   module D = JmpBufDomain.JmpBufSet
-  module C = JmpBufDomain.JmpBufSet
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D)
 
   let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask): D.t =

src/analyses/apron/relationAnalysis.apron.ml

@@ -20,7 +20,7 @@ struct
   module Priv = Priv (RD)
   module D = RelationDomain.RelComponents (RD) (Priv.D)
   module G = Priv.G
-  module C = D
+  include Analyses.ValueContexts(D)
   module V =
   struct
     include Priv.V
@@ -40,7 +40,7 @@ struct
   (* Result map used for comparison of results for relational traces paper. *)
   let results = PCU.RH.create 103
 
-  let context fd x =
+  let context ctx fd x =
     if ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.relation.context" ~removeAttr:"relation.no-context" ~keepAttr:"relation.context" fd then
       x
     else

src/analyses/base.ml

@@ -38,7 +38,7 @@ struct
   module Dom    = BaseDomain.DomFunctor (Priv.D) (RVEval)
   type t = Dom.t
   module D      = Dom
-  module C      = Dom
+  include Analyses.ValueContexts(D)
 
   (* Two global invariants:
      1. Priv.V -> Priv.G  --  used for Priv
@@ -79,6 +79,7 @@ struct
   type glob_diff = (V.t * G.t) list
 
   let name () = "base"
+
   let startstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
   let exitstate  v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
 
@@ -622,7 +623,7 @@ struct
 
   let drop_intervalSet = CPA.map (function Int x -> Int (ID.no_intervalSet x) | x -> x )
 
-  let context (fd: fundec) (st: store): store =
+  let context ctx (fd: fundec) (st: store): store =
     let f keep drop_fn (st: store) = if keep then st else { st with cpa = drop_fn st.cpa} in
     st |>
     (* Here earlyglobs only drops syntactic globals from the context and does not consider e.g. escaped globals. *)

src/analyses/callstring.ml

@@ -1,7 +1,7 @@
 (**
-   Call String analysis [call_string] and/or Call Site analysis [call_site]. 
-   The call string limitation for both approaches can be adjusted with the "callString_length" option. 
-   By adding new implementations of the CallstringType, additional analyses can be added. 
+   Call String analysis [call_string] and/or Call Site analysis [call_site].
+   The call string limitation for both approaches can be adjusted with the "callString_length" option.
+   By adding new implementations of the CallstringType, additional analyses can be added.
 *)
 
 open Analyses
@@ -18,20 +18,22 @@ end
 
 (** Analysis with infinite call string or with limited call string (k-CFA, tracks the last k call stack elements).
     With the CT argument it is possible to specify the type of the call string elements *)
-module Spec (CT:CallstringType) : MCPSpec = 
+module Spec (CT:CallstringType) : MCPSpec =
 struct
-  include Analyses.IdentitySpec
+  include UnitAnalysis.Spec
 
   (* simulates a call string (with or without limitation)*)
   module CallString = struct
     include Printable.PQueue (CT)
 
+    let (empty:t) = BatDeque.empty
+
     (* pushes "elem" to the call string, guarantees a depth of k if limitation is specified with "ana.context.callString_length" *)
-    let push callstr elem = 
+    let push callstr elem =
       match elem with
       | None -> callstr
-      | Some e -> 
-        let new_callstr = BatDeque.cons e callstr in (* pushes new element to callstr *)     
+      | Some e ->
+        let new_callstr = BatDeque.cons e callstr in (* pushes new element to callstr *)
         if get_int "ana.context.callString_length" < 0
         then new_callstr (* infinite call string *)
         else (* maximum of k elements *)
@@ -41,46 +43,32 @@ struct
           | _ -> failwith "CallString Error: It shouldn't happen that more than one element must be deleted to maintain the correct height!"
   end
 
-  module D = Lattice.Flat (CallString) (* should be the CallString (C=D). Since a Lattice is required, Lattice.Flat is used to fulfill the type *) 
   module C = CallString
-  module V = EmptyV
-  module G = Lattice.Unit
 
   let name () = "call_"^ CT.ana_name
-  let startstate v = `Lifted (BatDeque.empty)
-  let exitstate v =  `Lifted (BatDeque.empty)
-
-  let context fd x = match x with 
-    | `Lifted x -> x
-    | _ -> failwith "CallString: Context error! The context cannot be derived from Top or Bottom!"
-
-  let callee_state ctx f = 
-    let elem = CT.new_ele f ctx in (* receive element that should be added to call string *)
-    let new_callstr = CallString.push (context f ctx.local) elem in
-    `Lifted new_callstr
-
-  let enter ctx r f args = [ctx.local, callee_state ctx f]
 
-  let combine_env ctx lval fexp f args fc au f_ask = ctx.local
+  let startcontext () = CallString.empty
 
-  let threadenter ctx ~multiple lval v args = [callee_state ctx (Cilfacade.find_varinfo_fundec v)]
+  let context ctx fd _ =
+    let elem = CT.new_ele fd ctx in (* receive element that should be added to call string *)
+    CallString.push (ctx.context ()) elem
 end
 
 (* implementations of CallstringTypes*)
 module Callstring: CallstringType = struct
   include CilType.Fundec
   let ana_name = "string"
-  let new_ele f ctx = 
-    let f' = Node.find_fundec ctx.node in 
-    if CilType.Fundec.equal f' dummyFunDec 
+  let new_ele f ctx =
+    let f' = Node.find_fundec ctx.node in
+    if CilType.Fundec.equal f' dummyFunDec
     then None
     else Some f'
 end
 
 module Callsite: CallstringType = struct
   include CilType.Stmt
   let ana_name = "site"
-  let new_ele f ctx = 
+  let new_ele f ctx =
     match ctx.prev_node with
     | Statement stmt -> Some stmt
     | _ -> None (* first statement is filtered *)

src/analyses/condVars.ml

@@ -58,7 +58,7 @@ struct
 
   let name () = "condvars"
   module D = Domain
-  module C = Domain
+  include Analyses.ValueContexts(D)
 
   (* >? is >>=, |? is >> *)
   let (>?) = Option.bind

src/analyses/expsplit.ml

@@ -13,7 +13,7 @@ struct
   let name () = "expsplit"
 
   module D = MapDomain.MapBot (Basetype.CilExp) (ID)
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let startstate v = D.bot ()
   let exitstate = startstate

src/analyses/extractPthread.ml

@@ -866,7 +866,7 @@ module Spec : Analyses.MCPSpec = struct
   (** Domains *)
   module D = PthreadDomain.D
 
-  module C = D
+  include Analyses.ValueContexts(D)
 
   (** Set of created tasks to spawn when going multithreaded *)
   module G = Tasks

src/analyses/locksetAnalysis.ml

@@ -15,7 +15,7 @@ struct
   let name () = "lockset"
 
   module D = D
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let startstate v = D.empty ()
   let threadenter ctx ~multiple lval f args = [D.empty ()]

src/analyses/loopTermination.ml

@@ -30,7 +30,8 @@ struct
   let name () = "termination"
 
   module D = Lattice.Unit
-  module C = D
+  include Analyses.ValueContexts(D)
+
   module V = struct
     include UnitV
     let is_write_only _ = true

src/analyses/loopfreeCallstring.ml

@@ -1,60 +1,49 @@
-(** 
+(**
    Loopfree Callstring analysis [loopfree_callstring] that reduces the call string length of the classical Call String approach for recursions
-   The idea is to improve the Call String analysis by representing all detected call cycle of the call string in a set 
+   The idea is to improve the Call String analysis by representing all detected call cycle of the call string in a set
    In case no call cycles appears, the call string is identical to the call string of the Call String approach
-   For example: 
+   For example:
    - call string [main, a, b, c, a] is represented as [main, {a, b, c}]
    - call string [main, a, a, b, b, b] is represented as [main, {a}, {b}]
 
    This approach is inspired by
-   @see <https://arxiv.org/abs/2301.06439> Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Appendix F. 
+   @see <https://arxiv.org/abs/2301.06439> Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Appendix F.
 *)
 open Analyses
 
 module Spec : MCPSpec =
 struct
-  include Analyses.IdentitySpec
+  include UnitAnalysis.Spec
 
   let name () = "loopfree_callstring"
 
   module FundecSet = SetDomain.Make (CilType.Fundec)
-  module Either =  Printable.Either (CilType.Fundec) (FundecSet) 
-
-  module D = Lattice.Flat (Printable.Liszt (Either)) (* A domain element is a list containing fundecs and sets of fundecs.*) 
-  module C = D
-  module V = EmptyV
-  module G = Lattice.Unit
-  let startstate v = `Lifted([])
-  let exitstate  v = `Lifted([])
-
-  let get_list list = match list with
-    | `Lifted e -> e
-    | _ -> failwith "Error loopfreeCallstring (get_list): The list cannot be derived from Top or Bottom!"
-
-  let loop_detected f = function
-    (* note: a call string contains each Fundec at most once *)
-    | `Left ele -> CilType.Fundec.equal f ele
-    | `Right set -> FundecSet.mem f set 
-
-  let add_to_set old = function
-    | `Left ele -> FundecSet.add ele old
-    | `Right set -> FundecSet.join old set
-
-  let rec callee_state f prev_set prev_list = function
-    | [] -> (`Left f)::(List.rev prev_list) (* f is not yet contained in the call string *)
-    | e::rem_list -> 
-      let new_set = add_to_set prev_set e in
-      if loop_detected f e (* f is already present in the call string *)
-      then (`Right new_set)::rem_list (* combine all elements of the call cycle in a set *)
-      else callee_state f new_set (e::prev_list) rem_list
-
-  let callee_state f ctx = `Lifted(callee_state f (FundecSet.empty ()) [] (get_list ctx.local))
-
-  let enter ctx r f args = [ctx.local, callee_state f ctx]
-
-  let threadenter ctx ~multiple lval v args = [callee_state (Cilfacade.find_varinfo_fundec v) ctx]
-
-  let combine_env ctx lval fexp f args fc au f_ask = ctx.local
+  module Either =  Printable.Either (CilType.Fundec) (FundecSet)
+
+  module C = Printable.Liszt (Either)
+
+  let append fd current =
+    let loop_detected f = function
+      (* note: a call string contains each Fundec at most once *)
+      | `Left ele -> CilType.Fundec.equal f ele
+      | `Right set -> FundecSet.mem f set
+    in
+    let add_to_set old = function
+      | `Left ele -> FundecSet.add ele old
+      | `Right set -> FundecSet.join old set
+    in
+    let rec append f prev_set prev_list = function
+      | [] -> (`Left f)::(List.rev prev_list) (* f is not yet contained in the call string *)
+      | e::rem_list ->
+        let new_set = add_to_set prev_set e in
+        if loop_detected f e (* f is already present in the call string *)
+        then (`Right new_set)::rem_list (* combine all elements of the call cycle in a set *)
+        else append f new_set (e::prev_list) rem_list
+    in
+    append fd (FundecSet.empty ()) [] current
+
+  let startcontext () = []
+  let context ctx fd x = append fd (ctx.context ())
 end
 
 let _ = MCP.register_analysis (module Spec : MCPSpec)

src/analyses/mCP.ml

@@ -83,10 +83,10 @@ struct
     check_deps !activated;
     activated := topo_sort_an !activated;
     begin
-      match get_string_list "ana.ctx_sens" with 
+      match get_string_list "ana.ctx_sens" with
       | [] -> (* use values of "ana.ctx_insens" (blacklist) *)
         let cont_inse = map' find_id @@ get_string_list "ana.ctx_insens" in
-        activated_ctx_sens := List.filter (fun (n, _) -> not (List.mem n cont_inse)) !activated;      
+        activated_ctx_sens := List.filter (fun (n, _) -> not (List.mem n cont_inse)) !activated;
       | sens -> (* use values of "ana.ctx_sens" (whitelist) *)
         let cont_sens = map' find_id @@ sens in
         activated_ctx_sens := List.filter (fun (n, _) -> List.mem n cont_sens) !activated;
@@ -113,19 +113,18 @@ struct
     let ys = fold_left one_el [] xs in
     List.rev ys, !dead
 
-  let context fd x =
-    let x = spec_list x in
-    filter_map (fun (n,(module S:MCPSpec),d) ->
-        if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
-          None
-        else
-          Some (n, Obj.repr @@ S.context fd (Obj.obj d))
-      ) x
-
   let exitstate  v = map (fun (n,{spec=(module S:MCPSpec); _}) -> n, Obj.repr @@ S.exitstate  v) !activated
   let startstate v = map (fun (n,{spec=(module S:MCPSpec); _}) -> n, Obj.repr @@ S.startstate v) !activated
   let morphstate v x = map (fun (n,(module S:MCPSpec),d) -> n, Obj.repr @@ S.morphstate v (Obj.obj d)) (spec_list x)
 
+  let startcontext () =
+    filter_map (fun (n,{spec=(module S:MCPSpec); _}) ->
+        if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
+          None
+        else
+          Some (n, Obj.repr @@ S.startcontext ())
+      ) !activated
+
   let rec assoc_replace (n,c) = function
     | [] -> failwith "assoc_replace"
     | (n',c')::xs -> if n=n' then (n,c)::xs else (n',c') :: assoc_replace (n,c) xs
@@ -235,6 +234,17 @@ struct
     if M.tracing then M.traceu "event" "";
     ctx'.local
 
+  and context ctx fd x =
+    let ctx'' = outer_ctx "context_computation" ctx in
+    let x = spec_list x in
+    filter_map (fun (n,(module S:MCPSpec),d) ->
+        if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
+          None
+        else
+          let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "context_computation" ctx'' n d in
+          Some (n, Obj.repr @@ S.context ctx' fd (Obj.obj d))
+      ) x
+
   and branch (ctx:(D.t, G.t, C.t, V.t) ctx) (e:exp) (tv:bool) =
     let spawns = ref [] in
     let splits = ref [] in

src/analyses/mallocFresh.ml

@@ -10,7 +10,7 @@ struct
 
   (* must fresh variables *)
   module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
-  module C = D
+  include Analyses.ValueContexts(D)
 
   let name () = "mallocFresh"
 

src/analyses/malloc_null.ml

@@ -13,7 +13,7 @@ struct
 
   module Addr = ValueDomain.Addr
   module D = ValueDomain.AddrSetDomain
-  module C = ValueDomain.AddrSetDomain
+  include Analyses.ValueContexts(D)
   module P = IdentityP (D)
 
   (*