Merge pull request #549 from goblint/issue-544-2-td3

sim642 · web-flow · commit c8431cdcb867 · 2022-01-28T12:52:06.000+02:00
Collect constraint unknown sets in global invariant, use them for TD3 incremental load
diff --git a/g2html b/g2html
@@ -1 +1 @@
-Subproject commit 120a326f8ecadcc01fe601dc824decb8af2cf630
+Subproject commit 49a7a8d21c6741d57d35ee5ba175c8ff32a4d0b9
diff --git a/gobview b/gobview
@@ -1 +1 @@
-Subproject commit 3acd89c9ec9b0714433ae3b9aa82d596a5c34aac
+Subproject commit 3f4a3cdd56c9f4d2c5548d15eac3bb58b670dd1a
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
@@ -17,13 +17,36 @@ struct
   module D = Lattice.Unit
   module C = Lattice.Unit
 
+  (* Two global invariants:
+     1. (lval, type) -> accesses  --  used for warnings
+     2. varinfo -> set of (lval, type)  --  used for IterSysVars Global *)
+
+  module V0 = Printable.Prod (Access.LVOpt) (Access.T)
+  module V =
+  struct
+    include Printable.Either (V0) (CilType.Varinfo)
+    let access x = `Left x
+    let vars x = `Right x
+  end
+
+  module V0Set = SetDomain.Make (V0)
   module G =
   struct
-    include Access.AS
+    include Lattice.Lift2 (Access.AS) (V0Set) (Printable.DefaultNames)
+
+    let access = function
+      | `Bot -> Access.AS.bot ()
+      | `Lifted1 x -> x
+      | _ -> failwith "Access.access"
+    let vars = function
+      | `Bot -> V0Set.bot ()
+      | `Lifted2 x -> x
+      | _ -> failwith "Access.vars"
+    let create_access access = `Lifted1 access
+    let create_vars vars = `Lifted2 vars
 
     let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
-  module V = Printable.Prod (Access.LVOpt) (Access.T)
 
   let safe       = ref 0
   let vulnerable = ref 0
@@ -34,14 +57,28 @@ struct
     vulnerable := 0;
     unsafe := 0
 
+  let side_vars ctx lv_opt ty =
+    match lv_opt with
+    | Some (v, _) ->
+      let d =
+        if !GU.should_warn then
+          G.create_vars (V0Set.singleton (lv_opt, ty))
+        else
+          G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
+      in
+      ctx.sideg (V.vars v) d;
+    | None ->
+      ()
+
   let side_access ctx ty lv_opt (conf, w, loc, e, a) =
     let d =
       if !GU.should_warn then
-        Access.AS.singleton (conf, w, loc, e, a)
+        G.create_access (Access.AS.singleton (conf, w, loc, e, a))
       else
         G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
     in
-    ctx.sideg (lv_opt, ty) d
+    ctx.sideg (V.access (lv_opt, ty)) d;
+    side_vars ctx lv_opt ty
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (w:bool) (reach:bool) (conf:int) (e:exp) =
     let open Queries in
@@ -204,9 +241,18 @@ struct
     match q with
     | WarnGlobal g ->
       let g: V.t = Obj.obj g in
-      (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
-      let accs = ctx.global g in
-      Stats.time "access" (Access.warn_global safe vulnerable unsafe g) accs
+      begin match g with
+        | `Left g' -> (* accesses *)
+          (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
+          let accs = G.access (ctx.global g) in
+          Stats.time "access" (Access.warn_global safe vulnerable unsafe g') accs
+        | `Right _ -> (* vars *)
+          ()
+      end
+    | IterSysVars (Global g, vf) ->
+      V0Set.iter (fun v ->
+          vf (Obj.repr (V.access v))
+        ) (G.vars (ctx.global (V.vars g)))
     | _ -> Queries.Result.top q
 
   let finalize () =
diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
@@ -377,6 +377,9 @@ struct
       let exp = (BinOp (Cil.Lt, exp1, exp2, TInt (IInt, []))) in
       let is_lt = eval_int exp in
       Option.default true (ID.to_bool is_lt)
+    | Queries.IterSysVars (vq, vf) ->
+      let vf' x = vf (Obj.repr x) in
+      Priv.iter_sys_vars ctx.global vq vf'
     | _ -> Result.top q
 
 
diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml
@@ -39,6 +39,7 @@ module type S =
 
     val thread_join: Q.ask -> (V.t -> G.t) -> Cil.exp -> apron_components_t -> apron_components_t
     val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> apron_components_t -> apron_components_t
+    val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit (** [Queries.IterSysVars] for apron. *)
 
     val init: unit -> unit
     val finalize: unit -> unit
@@ -68,6 +69,7 @@ struct
 
   let enter_multithreaded ask getg sideg st = st
   let threadenter ask getg st = st
+  let iter_sys_vars getg vq vf = ()
 
   let init () = ()
   let finalize () = ()
@@ -342,6 +344,8 @@ struct
   let threadenter ask getg (st: apron_components_t): apron_components_t =
     {apr = getg (); priv = startstate ()}
 
+  let iter_sys_vars getg vq vf = () (* TODO: or report singleton global for any Global query? *)
+
   let finalize () = ()
 end
 
@@ -1040,6 +1044,11 @@ struct
     let _,lmust,l = st.priv in
     {apr = AD.bot (); priv = (W.bot (),lmust,l)}
 
+  let iter_sys_vars getg vq vf =
+    match vq with
+    | VarQuery.Global g -> vf (V.global g)
+    | _ -> ()
+
   let finalize () = finalize ()
 end
 
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -38,6 +38,10 @@ struct
   module D      = Dom
   module C      = Dom
 
+  (* Two global invariants:
+     1. Priv.V -> Priv.G  --  used for Priv
+     2. thread -> VD  --  used for thread returns *)
+
   module V =
   struct
     include Printable.Either (Priv.V) (ThreadIdDomain.Thread)
@@ -1079,6 +1083,9 @@ struct
         | _ -> true
       end
     | Q.IsMultiple v -> WeakUpdates.mem v ctx.local.weak
+    | Q.IterSysVars (vq, vf) ->
+      let vf' x = vf (Obj.repr (V.priv x)) in
+      Priv.iter_sys_vars (priv_getg ctx.global) vq vf'
     | _ -> Q.Result.top q
 
   let update_variable variable typ value cpa =
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
@@ -35,6 +35,7 @@ sig
   val escape: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseComponents (D).t
   val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t
   val threadenter: Q.ask -> BaseComponents (D).t -> BaseComponents (D).t
+  val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit
 
   val init: unit -> unit
   val finalize: unit -> unit
@@ -59,6 +60,7 @@ module OldPrivBase =
 struct
   include NoFinalize
   module D = Lattice.Unit
+  module V = VarinfoV
 
   let startstate () = ()
 
@@ -76,14 +78,18 @@ struct
       true
     | _ ->
       !GU.earlyglobs && not (ThreadFlag.is_multi ask)
+
+  let iter_sys_vars getg vq vf =
+    match vq with
+    | VarQuery.Global g -> vf g
+    | _ -> ()
 end
 
 (* Copy of ProtectionBasedOldPriv with is_private constantly false. *)
 module NonePriv: S =
 struct
   include OldPrivBase
   module G = BaseDomain.VD
-  module V = VarinfoV
 
   let init () = ()
 
@@ -135,7 +141,6 @@ struct
   include OldPrivBase
 
   module G = BaseDomain.VD
-  module V = VarinfoV
 
   let init () =
     if get_string "ana.osek.oil" = "" then ConfCheck.RequireMutexActivatedInit.init ()
@@ -408,7 +413,6 @@ struct
 
   module D = MustVars
   module G = BaseDomain.VD
-  module V = VarinfoV
 
   let init () =
     if get_string "ana.osek.oil" = "" then ConfCheck.RequireMutexActivatedInit.init ()
@@ -599,6 +603,13 @@ struct
       ) st.cpa st
 
   let threadenter = startstate_threadenter startstate
+
+  let iter_sys_vars getg vq vf =
+    match vq with
+    | VarQuery.Global g ->
+      vf (V.unprotected g);
+      vf (V.protected g);
+    | _ -> ()
 end
 
 module AbstractLockCenteredGBase (WeakRange: Lattice.S) (SyncRange: Lattice.S) =
@@ -1351,6 +1362,7 @@ struct
   let escape ask getg sideg st escaped = time "escape" (Priv.escape ask getg sideg st) escaped
   let enter_multithreaded ask getg sideg st = time "enter_multithreaded" (Priv.enter_multithreaded ask getg sideg) st
   let threadenter ask st = time "threadenter" (Priv.threadenter ask) st
+  let iter_sys_vars getg vq vf = time "iter_sys_vars" (Priv.iter_sys_vars getg vq) vf
 
   let init () = time "init" (Priv.init) ()
   let finalize () = time "finalize" (Priv.finalize) ()
diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli
@@ -21,6 +21,7 @@ sig
   val escape: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseDomain.BaseComponents (D).t
   val enter_multithreaded: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
   val threadenter: Queries.ask -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
+  val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit (** [Queries.IterSysVars] for base. *)
 
   val init: unit -> unit
   val finalize: unit -> unit
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
@@ -89,6 +89,11 @@ struct
     let mutex_inits: t = `Left (`Right ())
     let global x: t = `Right x
   end
+
+  let iter_sys_vars getg vq vf =
+    match vq with
+    | VarQuery.Global g -> vf (V.global g)
+    | _ -> ()
 end
 
 module MayVars =
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
@@ -361,6 +361,13 @@ struct
         f ~q:(WarnGlobal (Obj.repr g)) (Result.top ()) (n, spec n, assoc n ctx.local)
       | Queries.PartAccess {exp; var_opt; write} ->
         Obj.repr (access ctx exp var_opt write)
+      | Queries.IterSysVars (vq, fi) ->
+        (* IterSysVars is special: argument function is lifted for each analysis *)
+        iter (fun ((n,(module S:MCPSpec),d) as t) ->
+            let fi' x = fi (Obj.repr (v_of n x)) in
+            let q' = Queries.IterSysVars (vq, fi') in
+            f ~q:q' () t
+          ) @@ spec_list ctx.local
       (* | EvalInt e ->
         (* TODO: only query others that actually respond to EvalInt *)
         (* 2x speed difference on SV-COMP nla-digbench-scaling/ps6-ll_valuebound5.c *)
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
@@ -151,6 +151,8 @@ struct
     | Queries.MustBeAtomic ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in
       Mutexes.mem verifier_atomic held_locks
+    | Queries.IterSysVars (Global g, f) ->
+      f (Obj.repr g)
     | _ -> Queries.Result.top q
 
   module A =
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
@@ -95,6 +95,7 @@ type _ t =
   | CreatedThreads: ConcDomain.ThreadSet.t t
   | MustJoinedThreads: ConcDomain.MustThreadSet.t t
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
+  | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *)
 
 type 'a result = 'a
 
@@ -147,6 +148,7 @@ struct
     | CreatedThreads ->  (module ConcDomain.ThreadSet)
     | MustJoinedThreads -> (module ConcDomain.MustThreadSet)
     | WarnGlobal _ -> (module Unit)
+    | IterSysVars _ -> (module Unit)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -198,6 +200,7 @@ struct
     | CreatedThreads -> ConcDomain.ThreadSet.top ()
     | MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
     | WarnGlobal _ -> Unit.top ()
+    | IterSysVars _ -> Unit.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -247,6 +250,7 @@ struct
       | Any CreatedThreads -> 33
       | Any MustJoinedThreads -> 34
       | Any (WarnGlobal _) -> 35
+      | Any (IterSysVars _) -> 36
     in
     let r = Stdlib.compare (order a) (order b) in
     if r <> 0 then
@@ -282,6 +286,7 @@ struct
       | Any (IsMultiple v1), Any (IsMultiple v2) -> CilType.Varinfo.compare v1 v2
       | Any (EvalThread e1), Any (EvalThread e2) -> CilType.Exp.compare e1 e2
       | Any (WarnGlobal vi1), Any (WarnGlobal vi2) -> compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
+      | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
       (* only argumentless queries should remain *)
       | _, _ -> Stdlib.compare (order a) (order b)
 end
diff --git a/src/domains/setDomain.ml b/src/domains/setDomain.ml
@@ -119,6 +119,8 @@ struct
 
   let hash x = fold (fun x y -> y + Base.hash x) x 0
 
+  let relift x = map Base.relift x
+
   let pretty_diff () ((x:t),(y:t)): Pretty.doc =
     if leq x y then dprintf "%s: These are fine!" (name ()) else
     if is_bot y then dprintf "%s: %a instead of bot" (name ()) pretty x else begin
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
@@ -70,13 +70,48 @@ end
 
 module GVarF (V: Printable.S) =
 struct
-  include V
+  include Printable.Either (V) (CilType.Fundec)
+  let spec x = `Left x
+  let contexts x = `Right x
+
   (* from Basetype.Variables *)
   let var_id _ = "globals"
   let node _ = MyCFG.Function Cil.dummyFunDec
   let pretty_trace = pretty
 end
 
+module GVarG (G: Lattice.S) (C: Printable.S) =
+struct
+  module CSet =
+  struct
+    include SetDomain.Make (
+      struct
+        include C
+        let printXml f c = BatPrintf.fprintf f "<value>%a</value>" printXml c (* wrap in <value> for HTML printing *)
+      end
+      )
+    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
+  end
+
+  include Lattice.Lift2 (G) (CSet) (Printable.DefaultNames)
+
+  let spec = function
+    | `Bot -> G.bot ()
+    | `Lifted1 x -> x
+    | _ -> failwith "GVarG.spec"
+  let contexts = function
+    | `Bot -> CSet.bot ()
+    | `Lifted2 x -> x
+    | _ -> failwith "GVarG.contexts"
+  let create_spec spec = `Lifted1 spec
+  let create_contexts contexts = `Lifted2 contexts
+
+  let printXml f = function
+    | `Lifted1 x -> G.printXml f x
+    | `Lifted2 x -> BatPrintf.fprintf f "<analysis name=\"fromspec-contexts\">%a</analysis>" CSet.printXml x
+    | x -> BatPrintf.fprintf f "<analysis name=\"fromspec\">%a</analysis>" printXml x
+end
+
 
 exception Deadcode
 
@@ -447,6 +482,8 @@ sig
 
   (** Data used for incremental analysis *)
   val increment : increment_data
+
+  val iter_vars: (v -> d) -> VarQuery.t -> v VarQuery.f -> unit
 end
 
 (** Any system of side-effecting equations over lattices. *)
@@ -462,6 +499,7 @@ sig
   module G : Lattice.S
   val increment : increment_data
   val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option
+  val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit
 end
 
 (** A solver is something that can translate a system into a solution (hash-table).
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
diff --git a/src/framework/control.ml b/src/framework/control.ml
diff --git a/src/framework/varQuery.ml b/src/framework/varQuery.ml
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
diff --git a/unittest/solver/solverTest.ml b/unittest/solver/solverTest.ml
