Merge pull request #1427 from goblint/issue_1379

Pass `ctx` to context & Simplify callstring-based approaches

Author: michael-schwarz

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 ()]