Incremental TD3: optimize write-only unknown restarting

scripts/test-incremental.sh

@@ -19,7 +19,7 @@ patch -p0 -b <$patch
 
 ./goblint --conf $conf $args --enable incremental.load --set save_run $base/$test-incrementalrun $source &> $base/$test.after.incr.log
 ./goblint --conf $conf $args --enable incremental.only-rename --set save_run $base/$test-originalrun $source &> $base/$test.after.scratch.log
-./goblint --conf $conf --enable solverdiffs --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source
+./goblint --conf $conf --disable dbg.compare_runs.glob --enable solverdiffs --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source
 
 patch -p0 -b -R <$patch
 rm -r $base/$test-originalrun $base/$test-incrementalrun

src/analyses/accessAnalysis.ml

@@ -25,8 +25,10 @@ struct
   module V =
   struct
     include Printable.Either (V0) (CilType.Varinfo)
+    let name () = "access"
     let access x = `Left x
     let vars x = `Right x
+    let is_write_only _ = true
   end
 
   module V0Set = SetDomain.Make (V0)
@@ -44,8 +46,6 @@ struct
       | _ -> 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
 
   let safe       = ref 0
@@ -60,24 +60,14 @@ struct
   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;
+      if !GU.should_warn then
+        ctx.sideg (V.vars v) (G.create_vars (V0Set.singleton (lv_opt, ty)))
     | None ->
       ()
 
   let side_access ctx ty lv_opt (conf, w, loc, e, a) =
-    let d =
-      if !GU.should_warn then
-        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 (V.access (lv_opt, ty)) d;
+    if !GU.should_warn then
+      ctx.sideg (V.access (lv_opt, ty)) (G.create_access (Access.AS.singleton (conf, w, loc, e, a)));
     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) =

src/analyses/apron/apronAnalysis.apron.ml

@@ -16,7 +16,11 @@ struct
   module D = ApronComponents (AD) (Priv.D)
   module G = Priv.G
   module C = D
-  module V = Priv.V
+  module V =
+  struct
+    include Priv.V
+    include StdV
+  end
 
   open AD
   open (ApronDomain: (sig module V: (module type of ApronDomain.V) end)) (* open only V from ApronDomain (to shadow V of Spec), but don't open D (to not shadow D here) *)

src/analyses/arinc.ml

@@ -91,7 +91,11 @@ struct
   module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (ArincDomain.D)) (* set of created tasks to spawn when going multithreaded *)
   module G = Tasks
   module C = D
-  module V = Printable.UnitConf (struct let name = "tasks" end)
+  module V =
+  struct
+    include Printable.UnitConf (struct let name = "tasks" end)
+    include StdV
+  end
 
   let context fd d = { d with pred = Pred.bot (); ctx = Ctx.bot () }
 

src/analyses/base.ml

@@ -47,6 +47,7 @@ struct
     include Printable.Either (Priv.V) (ThreadIdDomain.Thread)
     let priv x = `Left x
     let thread x = `Right x
+    include StdV
   end
 
   module G =

src/analyses/extract_arinc.ml

@@ -33,7 +33,11 @@ struct
   module C = D
   module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (D)) (* set of created tasks to spawn when going multithreaded *)
   module G = Tasks
-  module V = Printable.UnitConf (struct let name = "tasks" end)
+  module V =
+  struct
+    include Printable.UnitConf (struct let name = "tasks" end)
+    include StdV
+  end
 
   type pname = string (* process name *)
   type fname = string (* function name *)

src/analyses/mCP.ml

@@ -13,12 +13,12 @@ module MCP2 : Analyses.Spec
   with module D = DomListLattice (LocalDomainListSpec)
    and module G = DomVariantLattice (GlobalDomainListSpec)
    and module C = DomListPrintable (ContextListSpec)
-   and module V = DomVariantPrintable (VarListSpec) =
+   and module V = DomVariantSysVar (VarListSpec) =
 struct
   module D = DomListLattice (LocalDomainListSpec)
   module G = DomVariantLattice (GlobalDomainListSpec)
   module C = DomListPrintable (ContextListSpec)
-  module V = DomVariantPrintable (VarListSpec)
+  module V = DomVariantSysVar (VarListSpec)
 
   open List open Obj
   let v_of n v = (n, repr v)

src/analyses/mCPRegistry.ml

@@ -7,7 +7,7 @@ type spec_modules = { name : string
                     ; dom  : (module Lattice.S)
                     ; glob : (module Lattice.S)
                     ; cont : (module Printable.S)
-                    ; var  : (module Printable.S)
+                    ; var  : (module SpecSysVar)
                     ; acc  : (module MCPA) }
 
 let activated  : (int * spec_modules) list ref = ref []
@@ -25,7 +25,7 @@ let register_analysis =
             ; dom  = (module S.D : Lattice.S)
             ; glob = (module S.G : Lattice.S)
             ; cont = (module S.C : Printable.S)
-            ; var  = (module S.V : Printable.S)
+            ; var  = (module S.V : SpecSysVar)
             ; acc  = (module S.A : MCPA)
             }
     in
@@ -45,6 +45,12 @@ sig
   val domain_list : unit -> (int * (module Printable.S)) list
 end
 
+module type DomainListSysVarSpec =
+sig
+  val assoc_dom : int -> (module SpecSysVar)
+  val domain_list : unit -> (int * (module SpecSysVar)) list
+end
+
 module type DomainListMCPASpec =
 sig
   val assoc_dom : int -> (module MCPA)
@@ -81,6 +87,18 @@ struct
     List.map (fun (x,y) -> (x,f y)) (D.domain_list ())
 end
 
+module PrintableOfSysVarSpec (D:DomainListSysVarSpec) : DomainListPrintableSpec =
+struct
+  let assoc_dom n =
+    let f (module L:SpecSysVar) = (module L : Printable.S)
+    in
+    f (D.assoc_dom n)
+
+  let domain_list () =
+    let f (module L:SpecSysVar) = (module L : Printable.S) in
+    List.map (fun (x,y) -> (x,f y)) (D.domain_list ())
+end
+
 module DomListPrintable (DLSpec : DomainListPrintableSpec)
   : Printable.S with type t = (int * unknown) list
 =
@@ -239,6 +257,23 @@ struct
     QCheck.oneof arbs
 end
 
+module DomVariantSysVar (DLSpec : DomainListSysVarSpec)
+  : SpecSysVar with type t = int * unknown
+=
+struct
+  open DLSpec
+  open Obj
+
+  include DomVariantPrintable (PrintableOfSysVarSpec (DLSpec))
+
+  let unop_map f ((n, d):t) =
+    f n (assoc_dom n) d
+
+  let is_write_only = unop_map (fun n (module S: SpecSysVar) x ->
+      S.is_write_only (obj x)
+    )
+end
+
 module DomListLattice (DLSpec : DomainListLatticeSpec)
   : Lattice.S with type t = (int * unknown) list
 =
@@ -339,7 +374,7 @@ struct
   let domain_list () = List.map (fun (n,p) -> n, p.cont) !activated_ctx_sens
 end
 
-module VarListSpec : DomainListPrintableSpec =
+module VarListSpec : DomainListSysVarSpec =
 struct
   let assoc_dom n = (find_spec n).var
   let domain_list () = List.map (fun (n,p) -> n, p.var) !activated

src/analyses/region.ml

@@ -14,7 +14,11 @@ struct
   module D = RegionDomain.RegionDom
   module G = RegPart
   module C = D
-  module V = Printable.UnitConf (struct let name = "partitions" end)
+  module V =
+  struct
+    include Printable.UnitConf (struct let name = "partitions" end)
+    include StdV
+  end
 
   let regions exp part st : Lval.CilLval.t list =
     match st with

src/analyses/threadAnalysis.ml

@@ -14,7 +14,11 @@ struct
   module D = ConcDomain.CreatedThreadSet
   module C = D
   module G = ConcDomain.ThreadCreation
-  module V = T
+  module V =
+  struct
+    include T
+    include StdV
+  end
 
   let should_join = D.equal
 

src/analyses/threadJoins.ml

@@ -14,7 +14,11 @@ struct
   module D = MustTIDs
   module C = D
   module G = MustTIDs
-  module V = TID
+  module V =
+  struct
+    include TID
+    include StdV
+  end
 
   (* transfer functions *)
   let return ctx (exp:exp option) (f:fundec) : D.t =

src/cdomains/basetype.ml

@@ -40,8 +40,6 @@ struct
     | _ -> Local
   let name () = "variables"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
-  let var_id _ = "globals"
-  let node _ = MyCFG.Function Cil.dummyFunDec
 
   let arbitrary () = MyCheck.Arbitrary.varinfo
 end

src/framework/analyses.ml

@@ -12,9 +12,16 @@ module M  = Messages
   * other functions. *)
 type fundecs = fundec list * fundec list * fundec list
 
+module type SysVar =
+sig
+  type t
+  val is_write_only: t -> bool
+end
+
 module type VarType =
 sig
   include Hashtbl.HashedType
+  include SysVar with type t := t
   val pretty_trace: unit -> t -> doc
   val compare : t -> t -> int
 
@@ -62,18 +69,28 @@ struct
 
   let var_id (n,_) = Var.var_id n
   let node (n,_) = n
+  let is_write_only _ = false
+end
+
+module type SpecSysVar =
+sig
+  include Printable.S
+  include SysVar with type t := t
 end
 
-module GVarF (V: Printable.S) =
+module GVarF (V: SpecSysVar) =
 struct
   include Printable.Either (V) (CilType.Fundec)
   let spec x = `Left x
   let contexts x = `Right x
 
   (* from Basetype.Variables *)
-  let var_id _ = "globals"
+  let var_id = show
   let node _ = MyCFG.Function Cil.dummyFunDec
   let pretty_trace = pretty
+  let is_write_only = function
+    | `Left x -> V.is_write_only x
+    | `Right _ -> true
 end
 
 module GVarG (G: Lattice.S) (C: Printable.S) =
@@ -86,7 +103,6 @@ struct
         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)
@@ -366,7 +382,7 @@ sig
   module D : Lattice.S
   module G : Lattice.S
   module C : Printable.S
-  module V: Printable.S (** Global constraint variables. *)
+  module V: SpecSysVar (** Global constraint variables. *)
 
   val name : unit -> string
 
@@ -556,8 +572,22 @@ struct
     BatPrintf.fprintf f "<context>\n%a</context>\n%a" C.printXml c D.printXml d
 end
 
-module VarinfoV = CilType.Varinfo (* TODO: or Basetype.Variables? *)
-module EmptyV = Printable.Empty
+module StdV =
+struct
+  let is_write_only _ = false
+end
+
+module VarinfoV =
+struct
+  include CilType.Varinfo (* TODO: or Basetype.Variables? *)
+  include StdV
+end
+
+module EmptyV =
+struct
+  include Printable.Empty
+  include StdV
+end
 
 module UnitA =
 struct

src/framework/constraints.ml

@@ -484,13 +484,8 @@ struct
     | _ -> S.sync ctx `Normal
 
   let side_context sideg f c =
-    let d =
-      if !GU.postsolving then
-        G.create_contexts (G.CSet.singleton c)
-      else
-        G.create_contexts (G.CSet.empty ()) (* HACK: just to pass validation with MCP DomVariantLattice *)
-    in
-    sideg (GVar.contexts f) d
+    if !GU.postsolving then
+      sideg (GVar.contexts f) (G.create_contexts (G.CSet.singleton c))
 
   let common_ctx var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) ctx * D.t list ref * (lval option * varinfo * exp list * D.t) list ref =
     let r = ref [] in
@@ -839,6 +834,10 @@ struct
   let node = function
     | `L a -> LV.node a
     | `G a -> GV.node a
+
+  let is_write_only = function
+    | `L a -> LV.is_write_only a
+    | `G a -> GV.is_write_only a
 end
 
 (** Translate a [GlobConstrSys] into a [EqConstrSys] *)
@@ -1107,13 +1106,12 @@ struct
     include Printable.Either (S.V) (Node)
     let s x = `Left x
     let node x = `Right x
+    let is_write_only = function
+      | `Left x -> S.V.is_write_only x
+      | `Right _ -> true
   end
 
-  module EM =
-  struct
-    include MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools)
-    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
-  end
+  module EM = MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools)
 
   module G =
   struct

src/solvers/postSolver.ml

@@ -85,10 +85,10 @@ module Verify: F =
 
     let one_side ~vh ~x ~y ~d =
       let y_lhs = try VH.find vh y with Not_found -> S.Dom.bot () in
-      if not (S.Dom.leq d y_lhs) then
+      if S.Var.is_write_only y then
+        VH.replace vh y (S.Dom.join y_lhs d) (* HACK: allow warnings/accesses to be added without complaining *)
+      else if not (S.Dom.leq d y_lhs) then
         complain_side x y ~lhs:y_lhs ~rhs:d
-      else
-        VH.replace vh y (S.Dom.join y_lhs d) (* HACK: allow warnings/accesses to be added *)
 
     let one_constraint ~vh ~x ~rhs =
       let lhs = try VH.find vh x with Not_found -> S.Dom.bot () in