Pass ctx to context & Simplify callstring-based approaches

src/analyses/abortUnless.ml

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

src/analyses/accessAnalysis.ml

@@ -56,7 +56,7 @@ struct
   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/apron/relationAnalysis.apron.ml

@@ -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

@@ -618,7 +618,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. *)
@@ -1271,7 +1271,7 @@ struct
           | _, `Bot -> false
           | `Lifted i1, `Lifted i2 ->
             ( let divisor_contains_zero = (ID.is_bot @@ ID.meet i2 (ID.of_int ik Z.zero))  in
-              if divisor_contains_zero then true else 
+              if divisor_contains_zero then true else
                 ( let (min_ik, max_ik) = IntDomain.Size.range ik in
                   let (min_i1, max_i1) = (IntDomain.IntDomTuple.minimal i1, IntDomain.IntDomTuple.maximal i1) in
                   let (min_i2, max_i2) = (IntDomain.IntDomTuple.minimal i2, IntDomain.IntDomTuple.maximal i2) in

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,35 @@ 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 threadenter ctx ~multiple lval v args = [callee_state ctx (Cilfacade.find_varinfo_fundec v)]
+  let context ctx fd _ =
+    let curr_context =
+      try
+        ctx.context ()
+      with Enter_func_has_no_context -> CallString.empty
+    in
+    let elem = CT.new_ele fd ctx in (* receive element that should be added to call string *)
+    CallString.push curr_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/loopfreeCallstring.ml

@@ -1,60 +1,54 @@
-(** 
+(**
    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 context ctx fd x =
+    let curr_context =
+      try
+        ctx.context ()
+      with Enter_func_has_no_context -> []
+    in
+    append fd curr_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,15 +113,6 @@ 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, repr @@ S.context fd (obj d))
-      ) x
-
   let exitstate  v = map (fun (n,{spec=(module S:MCPSpec); _}) -> n, repr @@ S.exitstate  v) !activated
   let startstate v = map (fun (n,{spec=(module S:MCPSpec); _}) -> n, repr @@ S.startstate v) !activated
   let morphstate v x = map (fun (n,(module S:MCPSpec),d) -> n, repr @@ S.morphstate v (obj d)) (spec_list x)
@@ -235,6 +226,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, repr @@ S.context ctx' fd (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/memLeak.ml

@@ -20,7 +20,7 @@ struct
   module V = UnitV
   module G = WasMallocCalled
 
-  let context _ d = d
+  let context ctx _ d = d
 
   let must_be_single_threaded ~since_start ctx =
     ctx.ask (Queries.MustBeSingleThreaded { since_start })

src/analyses/memOutOfBounds.ml

@@ -22,7 +22,7 @@ struct
   module D = Lattice.Unit
   module C = D
 
-  let context _ _ = ()
+  let context ctx _ _ = ()
 
   let name () = "memOutOfBounds"
 

src/analyses/threadId.ml

@@ -60,7 +60,7 @@ struct
 
   let name () = "threadid"
 
-  let context fd ((n,current,td) as d) =
+  let context ctx fd ((n,current,td) as d) =
     if GobConfig.get_bool "ana.thread.context.create-edges" then
       d
     else

src/analyses/tutorials/taint.ml

@@ -28,7 +28,7 @@ struct
   module C = Printable.Unit
 
   (* We are context insensitive in this analysis *)
-  let context _ _ = ()
+  let context ctx _ _ = ()
 
   (** Determines whether an expression [e] is tainted, given a [state]. *)
   let rec is_exp_tainted (state:D.t) (e:Cil.exp) = match e with

src/framework/analyses.ml

@@ -171,8 +171,11 @@ type ('d,'g,'c,'v) ctx =
 
 exception Ctx_failure of string
 (** Failure from ctx, e.g. global initializer *)
+exception Enter_func_has_no_context
+(** Tried to call ctx() on enter_func. Caught by callstring-based approaches and turned into an initial context *)
 
 let ctx_failwith s = raise (Ctx_failure s) (* TODO: use everywhere in ctx *)
+let enter_func_has_no_context () = raise Enter_func_has_no_context
 
 (** Convert [ctx] to [Queries.ask]. *)
 let ask_of_ctx ctx: Queries.ask = { Queries.f = ctx.ask }
@@ -206,7 +209,7 @@ sig
   val morphstate : varinfo -> D.t -> D.t
   val exitstate  : varinfo -> D.t
 
-  val context : fundec -> D.t -> C.t
+  val context : (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t -> C.t
 
   val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `Return] -> D.t
   val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result
@@ -375,7 +378,7 @@ struct
   let sync ctx _ = ctx.local
   (* Most domains do not have a global part. *)
 
-  let context fd x = x
+  let context ctx fd x = x
   (* Everything is context sensitive --- override in MCP and maybe elsewhere*)
 
   let paths_as_set ctx = [ctx.local]
@@ -420,7 +423,7 @@ module IdentityUnitContextsSpec = struct
   include IdentitySpec
   module C = Printable.Unit
 
-  let context _ _ = ()
+  let context ctx _ _ = ()
 end
 
 module type SpecSys =