master thesis: Taming Recursion with Three Context-Sensitive Analyses (Callstring, LoopfreeCallstring, Context Gas)

src/analyses/callstring.ml

@@ -0,0 +1,94 @@
+(**
+   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
+open GoblintCil
+open GobConfig
+
+(* Specifies the type of the call string elements *)
+module type CallstringType =
+sig
+  include CilType.S
+  val ana_name: string
+  val new_ele: fundec -> ('d,'g,'c,'v) ctx -> t option (* returns an element that should be pushed to the call string *)
+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 = 
+struct
+  include Analyses.IdentitySpec
+
+  (* simulates a call string (with or without limitation)*)
+  module CallString = struct
+    include Printable.PQueue (CT)
+
+    (* pushes "elem" to the call string, guarantees a depth of k if limitation is specified with "ana.context.callString_length" *)
+    let push callstr elem = 
+      match elem with
+      | None -> 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 *)
+          match (BatDeque.size new_callstr - (get_int "ana.context.callString_length")) with
+          | 1 -> fst @@ Option.get (BatDeque.rear new_callstr)
+          | x when x <= 0 -> new_callstr
+          | _ -> 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)]
+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 
+    then None
+    else Some f'
+end
+
+module Callsite:CallstringType = struct
+  include CilType.Stmt
+  let ana_name = "site"
+  let new_ele f ctx = 
+    match ctx.prev_node with
+    | Statement stmt -> Some stmt
+    | _ -> None (* first statement is filtered *)
+end
+
+let _ =
+  (* call string approach *)
+  MCP.register_analysis (module Spec (Callstring) : MCPSpec); (* [call_string] *)
+
+  (* call site approach *)
+  MCP.register_analysis (module Spec (Callsite) : MCPSpec); (* [call_site] *)

src/analyses/loopfreeCallstring.ml

@@ -0,0 +1,60 @@
+(** 
+   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 
+   In case no call cycles appears, the call string is identical to the call string of the Call String approach
+   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. 
+*)
+open Analyses
+
+module Spec : MCPSpec =
+struct
+  include Analyses.IdentitySpec
+
+  let name () = "loopfree_callstring"
+
+  module FundecSet = SetDomain.Make (CilType.Fundec)
+  module Either =  Printable.Either (CilType.Fundec) (FundecSet) 
+
+  module D = Lattice.Flat (Printable.Liszt (Either)) (* should be a List containing Sets of Fundecs and Fundecs. Lattice.Flat is used to fulfill the type *) 
+  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
+end
+
+let _ = MCP.register_analysis (module Spec : MCPSpec)

src/analyses/mCP.ml

@@ -36,7 +36,7 @@ struct
   let name () = "MCP2"
 
   let path_sens = ref []
-  let cont_inse = ref []
+  let act_cont_sens = ref Set.empty
   let base_id   = ref (-1)
 
 
@@ -80,10 +80,18 @@ struct
     base_id := find_id "base";
     activated := map (fun s -> s, find_spec s) xs;
     path_sens := map' find_id @@ get_string_list "ana.path_sens";
-    cont_inse := map' find_id @@ get_string_list "ana.ctx_insens";
     check_deps !activated;
     activated := topo_sort_an !activated;
-    activated_ctx_sens := List.filter (fun (n, _) -> not (List.mem n !cont_inse)) !activated;
+    begin
+      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;      
+      | 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;
+    end;
+    act_cont_sens := Set.of_list (List.map (fun (n,p) -> n) !activated_ctx_sens);
     activated_path_sens := List.filter (fun (n, _) -> List.mem n !path_sens) !activated;
     match marshal with
     | Some marshal ->
@@ -108,7 +116,7 @@ struct
   let context fd x =
     let x = spec_list x in
     filter_map (fun (n,(module S:MCPSpec),d) ->
-        if mem n !cont_inse then
+        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))

src/common/domains/printable.ml

@@ -588,6 +588,43 @@ module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) = struct
   let arbitrary () = QCheck.quad (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ()) (Base4.arbitrary ())
 end
 
+module PQueue (Base: S) = 
+struct
+  type t = Base.t BatDeque.dq
+  include Std
+
+  let show x = "[" ^ (BatDeque.fold_right (fun a acc -> Base.show a ^ ", " ^ acc) x "]")
+
+  let pretty () x = text (show x)
+  let name () = Base.name () ^ "queue"
+
+  let relift x = BatDeque.map Base.relift x
+
+  let printXml f xs =
+    let rec loop n q =
+      match BatDeque.front q with
+      | None -> ()
+      | Some (x, xs) -> (BatPrintf.fprintf f "<key>%d</key>\n%a\n" n Base.printXml x; 
+                   loop (n+1) (xs))
+    in
+    BatPrintf.fprintf f "<value>\n<map>\n";
+    loop 0 xs; 
+    BatPrintf.fprintf f "</map>\n</value>\n"
+
+  let to_yojson q = `List (BatDeque.to_list @@ BatDeque.map (Base.to_yojson) q)
+  let hash q = BatDeque.fold_left (fun acc x -> (acc + 71) * (Base.hash x)) 11 q
+  let equal q1 q2 = BatDeque.eq ~eq:Base.equal q1 q2
+  let compare q1 q2 = 
+    match BatDeque.front q1, BatDeque.front q2 with
+    | None, None -> 0
+    | None, Some(_, _) -> -1
+    | Some(_, _), None -> 1
+    | Some(a1, q1'), Some(a2, q2') -> 
+      let c = Base.compare a1 a2 in
+      if c <> 0 then c
+      else compare q1' q2'
+end
+
 module Liszt (Base: S) =
 struct
   type t = Base.t list [@@deriving eq, ord, hash, to_yojson]

src/config/options.schema.json

@@ -356,11 +356,18 @@
         },
         "ctx_insens": {
           "title": "ana.ctx_insens",
-          "description": "List of context-insensitive analyses",
+          "description": "List of context-insensitive analyses, which is ignored if `ctx_sens` is not empty.",
           "type": "array",
           "items": { "type": "string" },
           "default": [ "stack_loc", "stack_trace_set" ]
         },
+        "ctx_sens": {
+          "title": "ana.ctx_sens",
+          "description": "List of context-sensitive analyses. In case of an empty array `ctx_insens` is used, otherwise `ctx_insens` is ignored.",
+          "type": "array",
+          "items": { "type": "string" },
+          "default": []
+        },
         "setjmp" : {
           "title": "ana.setjmp",
           "description": "Setjmp/Longjmp analysis",
@@ -970,6 +977,18 @@
                 "Do widening on contexts. Keeps a map of function to call state; enter will then return the widened local state for recursive calls.",
               "type": "boolean",
               "default": false
+            },
+            "gas_value": {
+              "title": "ana.context.gas_value",
+              "description": "x denotes the gas value for the ContextGasLifter. Negative value means deactivated, zero means context-insensitve analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitive, the remaining with no context.",
+              "type": "integer",
+              "default": -1
+            },
+            "callString_length": {
+              "title": "ana.context.callString_length",
+              "description": "Length of the call string that should be used as context for the call_string and/or call_site analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to be effective, one analysis of the `callstring.ml` file must be activated.",
+              "type": "integer",
+              "default": 2
             }
           },
           "additionalProperties": false

src/framework/constraints.ml

@@ -497,6 +497,91 @@ struct
   let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
 end
 
+module NoContext = struct let name = "no context" end
+module IntConf = 
+struct
+  let n () = max_int
+  let names x = Format.asprintf "%d" x
+end
+
+(** Lifts a [Spec] with the context gas variable. The gas variable limits the number of context-sensitively analyzed function calls in a call stack.
+    For every function call the gas is reduced. If the gas is zero, the remaining function calls are analyzed without context-information *)
+module ContextGasLifter (S:Spec)
+  : Spec with module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf)) 
+          and module C = Printable.Option (S.C) (NoContext)
+          and module G = S.G
+=
+struct
+  include S
+
+  module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) = 
+  struct 
+    include Lattice.Prod (Base1) (Base2)
+    let printXml f (x,y) =
+      BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\nContext Gas Value\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x Base2.printXml y
+  end
+  module D = Context_Gas_Prod (S.D) (Lattice.Chain (IntConf)) (* Product of S.D and an integer, tracking the context gas value *)
+  module C = Printable.Option (S.C) (NoContext)
+  module G = S.G
+  module V = S.V
+  module P =
+  struct
+    include S.P
+    let of_elt (x, _) = of_elt x
+  end
+
+  (* returns context gas value of the given ctx *)
+  let cg_val ctx = snd ctx.local
+
+  type marshal = S.marshal
+  let init = S.init
+  let finalize = S.finalize
+
+  let name () = S.name ()^" with context gas"
+  let startstate v = S.startstate v, get_int "ana.context.gas_value"
+  let exitstate v = S.exitstate v, get_int "ana.context.gas_value"
+  let morphstate v (d,i) = S.morphstate v d, i
+
+  let context fd (d,i) = 
+    (* only keep context if the context gas is greater zero *)
+    if i <= 0 then None else Some (S.context fd d)
+
+  let conv (ctx:(D.t,G.t,C.t,V.t) ctx): (S.D.t,G.t,S.C.t,V.t)ctx =
+    if (cg_val ctx <= 0) 
+    then {ctx with local = fst ctx.local
+                 ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
+                 ; context = (fun () -> ctx_failwith "no context (contextGas = 0)")}
+    else {ctx with local = fst ctx.local
+                 ; split = (fun d es -> ctx.split (d, cg_val ctx) es)
+                 ; context = (fun () -> Option.get (ctx.context ()))}
+
+  let enter ctx r f args =
+    (* callee gas = caller gas - 1 *)
+    let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, max 0 (cg_val ctx - 1))) in
+    liftmap_tup (S.enter (conv ctx) r f args) 
+
+  let threadenter ctx ~multiple lval f args = 
+    let liftmap f = List.map (fun (x) -> (x, max 0 (cg_val ctx - 1))) f in
+    liftmap (S.threadenter (conv ctx) ~multiple lval f args) 
+
+  let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
+  let query ctx q                                 = S.query (conv ctx) q
+  let assign ctx lval expr                        = S.assign (conv ctx) lval expr, cg_val ctx
+  let vdecl ctx v                                 = S.vdecl (conv ctx) v, cg_val ctx
+  let body ctx fundec                             = S.body (conv ctx) fundec, cg_val ctx
+  let branch ctx e tv                             = S.branch (conv ctx) e tv, cg_val ctx
+  let return ctx r f                              = S.return (conv ctx) r f, cg_val ctx
+  let asm ctx                                     = S.asm (conv ctx), cg_val ctx
+  let skip ctx                                    = S.skip (conv ctx), cg_val ctx
+  let special ctx r f args                        = S.special (conv ctx) r f args, cg_val ctx
+  let combine_env ctx r fe f args fc es f_ask     = S.combine_env (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
+  let combine_assign ctx r fe f args fc es f_ask  = S.combine_assign (conv ctx) r fe f args (Option.bind fc Fun.id) (fst es) f_ask, cg_val ctx
+  let paths_as_set ctx                            = List.map (fun (x) -> (x, cg_val ctx)) @@ S.paths_as_set (conv ctx) 
+  let threadspawn ctx ~multiple lval f args fctx  = S.threadspawn (conv ctx) ~multiple lval f args (conv fctx), cg_val ctx
+  let event ctx e octx                            = S.event (conv ctx) e (conv octx), cg_val ctx
+end
+
+
 module type Increment =
 sig
   val increment: increment_data option

src/framework/control.ml

@@ -23,6 +23,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let module S1 =
     (val
       (module MCP.MCP2 : Spec)
+      |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter) 
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)

src/goblint_lib.ml

@@ -151,6 +151,8 @@ module UnitAnalysis = UnitAnalysis
 
 module Assert = Assert
 module LoopTermination = LoopTermination
+module Callstring = Callstring
+module LoopfreeCallstring = LoopfreeCallstring
 module Uninit = Uninit
 module Expsplit = Expsplit
 module StackTrace = StackTrace