From 6321948ff345cc96dbf2702552451785eec75905 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 14 Feb 2022 12:35:26 +0200 Subject: [PATCH 01/17] Extract function and node specific logic from TD3 (issue #545) --- src/framework/analyses.ml | 8 ++ src/framework/constraints.ml | 153 ++++++++++++++++++++++++++++------- src/solvers/td3.ml | 100 ++--------------------- 3 files changed, 141 insertions(+), 120 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 70f84fd7e0..79bc0e66c6 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -448,6 +448,12 @@ let empty_increment_data file = { changes = CompareCIL.empty_change_info () } +type 'v sys_change_info = { + obsolete: 'v list; + delete: 'v list; + reluctant: 'v list; +} + (** A side-effecting system. *) module type MonSystem = sig @@ -471,6 +477,7 @@ sig val increment : increment_data val iter_vars: (v -> d) -> VarQuery.t -> v VarQuery.f -> unit + val sys_change: (v -> d) -> v sys_change_info end (** Any system of side-effecting equations over lattices. *) @@ -487,6 +494,7 @@ sig 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 + val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info 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 index 204ad649ad..2530512c6e 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -451,6 +451,35 @@ sig val increment: increment_data end +(** Combined variables so that we can also use the more common [EqConstrSys] + that uses only one kind of a variable. *) +module Var2 (LV:VarType) (GV:VarType) + : VarType + with type t = [ `L of LV.t | `G of GV.t ] += +struct + type t = [ `L of LV.t | `G of GV.t ] [@@deriving eq, ord, hash] + let relift = function + | `L x -> `L (LV.relift x) + | `G x -> `G (GV.relift x) + + let pretty_trace () = function + | `L a -> LV.pretty_trace () a + | `G a -> GV.pretty_trace () a + + let printXml f = function + | `L a -> LV.printXml f a + | `G a -> GV.printXml f a + + let var_id = function + | `L a -> LV.var_id a + | `G a -> GV.var_id a + + let node = function + | `L a -> LV.node a + | `G a -> GV.node a +end + (** The main point of this file---generating a [GlobConstrSys] from a [Spec]. *) module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment) : sig @@ -794,6 +823,99 @@ struct ) cs | _ -> () + + let sys_change getl getg = + let open CompareCIL in + + let c = I.increment.changes in + List.(Printf.printf "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed)); + + let changed_funs = List.filter_map (function + | {old = GFun (f, _); diff = None; _} -> + print_endline ("Completely changed function: " ^ f.svar.vname); + Some f + | _ -> None + ) I.increment.changes.changed + in + let part_changed_funs = List.filter_map (function + | {old = GFun (f, _); diff = Some nd; _} -> + print_endline ("Partially changed function: " ^ f.svar.vname); + Some (f, nd.primObsoleteNodes, nd.unchangedNodes) + | _ -> None + ) I.increment.changes.changed + in + let removed_funs = List.filter_map (function + | GFun (f, _) -> + print_endline ("Removed function: " ^ f.svar.vname); + Some f + | _ -> None + ) I.increment.changes.removed + in + + let module HM = Hashtbl.Make (Var2 (LVar) (GVar)) in + + let mark_node hm f node = + iter_vars getl getg (Node {node; fundec = Some f}) (fun v -> + HM.replace hm (`L v) () + ) (fun v -> + HM.replace hm (`G v) () + ) + in + + let obsolete_ret = HM.create 103 in + let obsolete_entry = HM.create 103 in + let obsolete_prim = HM.create 103 in + List.iter (fun f -> + mark_node obsolete_entry f (FunctionEntry f); + mark_node obsolete_ret f (Function f); + ) changed_funs; + List.iter (fun (f, pn, _) -> + List.iter (fun n -> + mark_node obsolete_prim f n + ) pn; + mark_node obsolete_ret f (Function f); + ) part_changed_funs; + + let obsolete = Enum.append (HM.keys obsolete_entry) (HM.keys obsolete_prim) |> List.of_enum in + let reluctant = HM.keys obsolete_ret |> List.of_enum in + + let marked_for_deletion = HM.create 103 in + + let dummy_pseudo_return_node f = + (* not the same as in CFG, but compares equal because of sid *) + Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f}) + in + let add_nodes_of_fun (functions: fundec list) withEntry = + let add_stmts (f: fundec) = + List.iter (fun s -> + mark_node marked_for_deletion f (Statement s) + ) f.sallstmts + in + List.iter (fun f -> + if withEntry then + mark_node marked_for_deletion f (FunctionEntry f); + mark_node marked_for_deletion f (Function f); + add_stmts f; + mark_node marked_for_deletion f (dummy_pseudo_return_node f) + ) functions; + in + + add_nodes_of_fun changed_funs (not (GobConfig.get_bool "incremental.reluctant.on")); + add_nodes_of_fun removed_funs true; + (* it is necessary to remove all unknowns for changed pseudo-returns because they have static ids *) + let add_pseudo_return f un = + let pseudo = dummy_pseudo_return_node f in + if not (List.exists (Node.equal pseudo % fst) un) then + mark_node marked_for_deletion f (dummy_pseudo_return_node f) + in + List.iter (fun (f,_,un) -> + mark_node marked_for_deletion f (Function f); + add_pseudo_return f un + ) part_changed_funs; + + let delete = HM.keys marked_for_deletion |> List.of_enum in + + {obsolete; delete; reluctant} end (** Convert a non-incremental solver into an "incremental" solver. @@ -812,34 +934,6 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve (vh, ()) end -(** Combined variables so that we can also use the more common [EqConstrSys] - that uses only one kind of a variable. *) -module Var2 (LV:VarType) (GV:VarType) - : VarType - with type t = [ `L of LV.t | `G of GV.t ] -= -struct - type t = [ `L of LV.t | `G of GV.t ] [@@deriving eq, ord, hash] - let relift = function - | `L x -> `L (LV.relift x) - | `G x -> `G (GV.relift x) - - let pretty_trace () = function - | `L a -> LV.pretty_trace () a - | `G a -> GV.pretty_trace () a - - let printXml f = function - | `L a -> LV.printXml f a - | `G a -> GV.printXml f a - - let var_id = function - | `L a -> LV.var_id a - | `G a -> GV.var_id a - - let node = function - | `L a -> LV.node a - | `G a -> GV.node a -end (** Translate a [GlobConstrSys] into a [EqConstrSys] *) module EqConstrSysFromGlobConstrSys (S:GlobConstrSys) @@ -890,6 +984,9 @@ struct let iter_vars get vq f = S.iter_vars (getL % get % l) (getG % get % g) vq (f % l) (f % g) + + let sys_change get = + S.sys_change (getL % get % l) (getG % get % g) end (** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index f4662535b4..10bd4a34ef 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -11,10 +11,7 @@ open Prelude open Analyses -open Constraints open Messages -open CompareCIL -open Cil module WP = functor (Arg: IncrSolverArg) -> @@ -523,8 +520,6 @@ module WP = start_event (); if GobConfig.get_bool "incremental.load" then ( - let c = S.increment.changes in - List.(Printf.printf "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed)); let restart_leaf x = if tracing then trace "sol2" "Restarting to bot %a\n" S.Var.pretty_trace x; @@ -598,110 +593,31 @@ module WP = else destabilize_normal; - let changed_funs = List.filter_map (function - | {old = GFun (f, _); diff = None; _} -> - print_endline ("Completely changed function: " ^ f.svar.vname); - Some f - | _ -> None - ) S.increment.changes.changed - in - let part_changed_funs = List.filter_map (function - | {old = GFun (f, _); diff = Some nd; _} -> - print_endline ("Partially changed function: " ^ f.svar.vname); - Some (f, nd.primObsoleteNodes, nd.unchangedNodes) - | _ -> None - ) S.increment.changes.changed - in - let removed_funs = List.filter_map (function - | GFun (f, _) -> - print_endline ("Removed function: " ^ f.svar.vname); - Some f - | _ -> None - ) S.increment.changes.removed - in - - let mark_node hm f node = - let get x = try HM.find rho x with Not_found -> S.Dom.bot () in - S.iter_vars get (Node {node; fundec = Some f}) (fun v -> - HM.replace hm v () - ) - in - - let obsolete_ret = HM.create 103 in - let obsolete_entry = HM.create 103 in - let obsolete_prim = HM.create 103 in - List.iter (fun f -> - mark_node obsolete_entry f (FunctionEntry f); - mark_node obsolete_ret f (Function f); - ) changed_funs; - List.iter (fun (f, pn, _) -> - List.iter (fun n -> - mark_node obsolete_prim f n - ) pn; - mark_node obsolete_ret f (Function f); - ) part_changed_funs; + let sys_change = S.sys_change (fun v -> try HM.find rho v with Not_found -> S.Dom.bot ()) in let old_ret = HM.create 103 in if GobConfig.get_bool "incremental.reluctant.on" then ( (* save entries of changed functions in rho for the comparison whether the result has changed after a function specific solve *) - HM.iter (fun k v -> + List.iter (fun k -> if HM.mem rho k then ( let old_rho = HM.find rho k in let old_infl = HM.find_default infl k VS.empty in HM.replace old_ret k (old_rho, old_infl) ) - ) obsolete_ret; + ) sys_change.reluctant; ) else ( (* If reluctant destabilization is turned off we need to destabilize all nodes in completely changed functions and the primary obsolete nodes of partly changed functions *) print_endline "Destabilizing changed functions and primary old nodes ..."; - HM.iter (fun k _ -> + List.iter (fun k -> if HM.mem stable k then destabilize k - ) obsolete_entry; - HM.iter (fun k _ -> - if HM.mem stable k then - destabilize k - ) obsolete_prim; + ) sys_change.obsolete; ); (* We remove all unknowns for program points in changed or removed functions from rho, stable, infl and wpoint *) - let marked_for_deletion = HM.create 103 in - - let dummy_pseudo_return_node f = - (* not the same as in CFG, but compares equal because of sid *) - Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f}) - in - let add_nodes_of_fun (functions: fundec list) withEntry = - let add_stmts (f: fundec) = - List.iter (fun s -> - mark_node marked_for_deletion f (Statement s) - ) f.sallstmts - in - List.iter (fun f -> - if withEntry then - mark_node marked_for_deletion f (FunctionEntry f); - mark_node marked_for_deletion f (Function f); - add_stmts f; - mark_node marked_for_deletion f (dummy_pseudo_return_node f) - ) functions; - in - - add_nodes_of_fun changed_funs (not (GobConfig.get_bool "incremental.reluctant.on")); - add_nodes_of_fun removed_funs true; - (* it is necessary to remove all unknowns for changed pseudo-returns because they have static ids *) - let add_pseudo_return f un = - let pseudo = dummy_pseudo_return_node f in - if not (List.exists (Node.equal pseudo % fst) un) then - mark_node marked_for_deletion f (dummy_pseudo_return_node f) - in - List.iter (fun (f,_,un) -> - mark_node marked_for_deletion f (Function f); - add_pseudo_return f un - ) part_changed_funs; - print_endline "Removing data for changed and removed functions..."; - let delete_marked s = HM.iter (fun k _ -> HM.remove s k) marked_for_deletion in + let delete_marked s = List.iter (fun k -> HM.remove s k) sys_change.delete in delete_marked rho; delete_marked infl; delete_marked wpoint; @@ -710,12 +626,12 @@ module WP = if restart_sided then ( (* restarts old copies of functions and their (removed) side effects *) print_endline "Destabilizing sides of changed functions, primary old nodes and removed functions ..."; - HM.iter (fun k _ -> + List.iter (fun k -> if HM.mem stable k then ( ignore (Pretty.printf "marked %a\n" S.Var.pretty_trace k); destabilize k ) - ) marked_for_deletion + ) sys_change.delete ); let restart_and_destabilize x = (* destabilize_with_side doesn't restart x itself *) From 8ba3144911bf922729355ebf750547797ebe8f56 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 15 Feb 2022 17:34:49 +0200 Subject: [PATCH 02/17] Fix missing sys_change in SolverTest --- unittest/solver/solverTest.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/unittest/solver/solverTest.ml b/unittest/solver/solverTest.ml index 7d8cd41858..22b1441d5c 100644 --- a/unittest/solver/solverTest.ml +++ b/unittest/solver/solverTest.ml @@ -45,6 +45,7 @@ module ConstrSys = struct | _ -> None let iter_vars _ _ _ _ _ = () + let sys_change _ _ = {Analyses.obsolete = []; delete = []; reluctant = []} end module LH = BatHashtbl.Make (ConstrSys.LVar) From 960491b76e029142217913c39884b363eea7fd49 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 15 Feb 2022 18:00:15 +0200 Subject: [PATCH 03/17] Pass incremental data to solver via argument instead of constraint system module --- src/framework/analyses.ml | 10 ++++------ src/framework/constraints.ml | 12 ++++-------- src/framework/control.ml | 6 +++--- src/solvers/selector.ml | 4 ++-- src/solvers/td3.ml | 6 +++--- unittest/solver/solverTest.ml | 4 +--- 6 files changed, 17 insertions(+), 25 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 79bc0e66c6..f96d0b2a4f 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -473,10 +473,9 @@ sig (** The system in functional form. *) val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m - (** Data used for incremental analysis *) - val increment : increment_data - val iter_vars: (v -> d) -> VarQuery.t -> v VarQuery.f -> unit + + (** Data used for incremental analysis *) val sys_change: (v -> d) -> v sys_change_info end @@ -491,7 +490,6 @@ sig module D : Lattice.S 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 val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info @@ -508,7 +506,7 @@ module type GenericEqBoxIncrSolverBase = (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs], reached from starting values [xs]. As a second component the solver returns data structures for incremental serialization. *) - val solve : (S.v -> S.d -> S.d -> S.d) -> (S.v*S.d) list -> S.v list -> S.d H.t * marshal + val solve : (S.v -> S.d -> S.d -> S.d) -> (S.v*S.d) list -> S.v list -> marshal option -> S.d H.t * marshal end (** (Incremental) solver argument, indicating which postsolving should be performed by the solver. *) @@ -546,7 +544,7 @@ module type GenericGlobSolver = (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs], reached from starting values [xs]. As a second component the solver returns data structures for incremental serialization. *) - val solve : (S.LVar.t*S.D.t) list -> (S.GVar.t*S.G.t) list -> S.LVar.t list -> (S.D.t LH.t * S.G.t GH.t) * marshal + val solve : (S.LVar.t*S.D.t) list -> (S.GVar.t*S.G.t) list -> S.LVar.t list -> marshal option -> (S.D.t LH.t * S.G.t GH.t) * marshal end module ResultType2 (S:Spec) = diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 2530512c6e..0f8e6fbbb2 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -504,9 +504,6 @@ struct 1. S.V -> S.G -- used for Spec 2. fundec -> set of S.C -- used for IterSysVars Node *) - (* Dummy module. No incremental analysis supported here*) - let increment = I.increment - let sync ctx = match Cfg.prev ctx.prev_node with | _ :: _ :: _ -> S.sync ctx `Join @@ -928,7 +925,7 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve type marshal = unit - let solve box xs vs = + let solve box xs vs _ = let vh = Sol.solve box xs vs in Post.post xs vs vh; (vh, ()) @@ -952,7 +949,6 @@ struct | `Lifted2 a -> S.D.printXml f a | (`Bot | `Top) as x -> printXml f x end - let increment = S.increment type v = Var.t type d = Dom.t @@ -1029,7 +1025,7 @@ end (** Transforms a [GenericEqBoxIncrSolver] into a [GenericGlobSolver]. *) module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase) - : GenericGlobSolver + (* : GenericGlobSolver *) = functor (S:GlobConstrSys) -> functor (LH:Hashtbl.S with type key=S.LVar.t) -> functor (GH:Hashtbl.S with type key=S.GVar.t) -> @@ -1043,11 +1039,11 @@ module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase) type marshal = Sol'.marshal - let solve ls gs l = + let solve ls gs l old_data = let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls @ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in let sv = List.map (fun x -> `L x) l in - let hm, solver_data = Sol'.solve EqSys.box vs sv in + let hm, solver_data = Sol'.solve EqSys.box vs sv old_data in Splitter.split_solution hm, solver_data end diff --git a/src/framework/control.ml b/src/framework/control.ml index c623fdadf0..4c17fddafc 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -401,7 +401,7 @@ struct let lh, gh = if load_run <> "" then ( let module S2' = (GlobSolverFromEqSolver (Generic.LoadRunIncrSolver (PostSolverArg))) (EQSys) (LHT) (GHT) in - let (r2, _) = S2'.solve entrystates entrystates_global startvars' in + let (r2, _) = S2'.solve entrystates entrystates_global startvars' None in (* TODO: has incremental data? *) r2 ) else if compare_runs <> [] then ( match compare_runs with @@ -436,7 +436,7 @@ struct if get_bool "dbg.verbose" then print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); Goblintutil.should_warn := get_string "warn_at" = "early" || gobview; - let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' in + let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' (Option.map (fun {solver_data; _} -> solver_data) Inc.increment.old_data) in if GobConfig.get_bool "incremental.save" then Serialize.store_data solver_data Serialize.SolverData; if save_run <> "" then ( @@ -484,7 +484,7 @@ struct end in let module S2' = (GlobSolverFromEqSolver (S2 (PostSolverArg2))) (EQSys) (LHT) (GHT) in - let (r2, _) = S2'.solve entrystates entrystates_global startvars' in + let (r2, _) = S2'.solve entrystates entrystates_global startvars' None in (* TODO: has incremental data? *) Comp.compare (get_string "solver", get_string "comparesolver") (lh,gh) (r2) in compare_with (Selector.choose_solver (get_string "comparesolver")) diff --git a/src/solvers/selector.ml b/src/solvers/selector.ml index 856ceaca91..cc75ed96e8 100644 --- a/src/solvers/selector.ml +++ b/src/solvers/selector.ml @@ -22,10 +22,10 @@ module Make = struct type marshal = Obj.t (* cannot use Sol.marshal because cannot unpack first-class module in applicative functor *) - let solve box xs vs = + let solve box xs vs (old_data: marshal option) = let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in let module F = Sol (Arg) (S) (VH) in - let (vh, marshal) = F.solve box xs vs in + let (vh, marshal) = F.solve box xs vs (Option.map Obj.obj old_data) in (vh, Obj.repr marshal) end diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 10bd4a34ef..52d4b56baf 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -877,12 +877,12 @@ module WP = {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages} - let solve box st vs = + let solve box st vs (old_data: marshal option) = let reuse_stable = GobConfig.get_bool "incremental.stable" in let reuse_wpoint = GobConfig.get_bool "incremental.wpoint" in if GobConfig.get_bool "incremental.load" then ( - let loaded, data = match S.increment.old_data with - | Some d -> true, Obj.obj d.solver_data + let loaded, data = match old_data with + | Some d -> true, d | _ -> false, create_empty_data () in (* This hack is for fixing hashconsing. diff --git a/unittest/solver/solverTest.ml b/unittest/solver/solverTest.ml index 22b1441d5c..b6286a8639 100644 --- a/unittest/solver/solverTest.ml +++ b/unittest/solver/solverTest.ml @@ -29,8 +29,6 @@ module ConstrSys = struct module D = Int module G = IntR - let increment = Analyses.empty_increment_data Cil.dummyFile - (* 1. x := g 2. y := 8 @@ -61,7 +59,7 @@ module Solver = Constraints.GlobSolverFromEqSolver (Constraints.EqIncrSolverFrom let test1 _ = let id x = x in - let ((sol, gsol), _) = Solver.solve [] [] ["w"] in + let ((sol, gsol), _) = Solver.solve [] [] ["w"] None in assert_equal ~printer:id "42" (Int.show (GH.find gsol "g")); assert_equal ~printer:id "42" (Int.show (LH.find sol "x")); assert_equal ~printer:id "8" (Int.show (LH.find sol "y")); From e14c71282e7e2938185ff5213c03cb604926c8ff Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 16 Feb 2022 10:28:14 +0200 Subject: [PATCH 04/17] Adapt Gobview to solve with incremental data argument --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index 09eb40764f..23a54c0388 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 09eb40764f82c94fd44ce7ba5137fd49ec8d8874 +Subproject commit 23a54c0388179abe7a5128b8fce3449d77f86763 From bff531585730d668de8a376f9e62e5423814890b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 16 Feb 2022 10:42:33 +0200 Subject: [PATCH 05/17] Remove write-only increment_data.new_file field --- src/framework/analyses.ml | 4 +--- src/maingoblint.ml | 4 ++-- src/util/server.ml | 4 ++-- 3 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index f96d0b2a4f..0ee9a44a1d 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -438,13 +438,11 @@ type analyzed_data = { type increment_data = { old_data: analyzed_data option; - new_file: Cil.file; changes: CompareCIL.change_info } -let empty_increment_data file = { +let empty_increment_data = { old_data = None; - new_file = file; changes = CompareCIL.empty_change_info () } diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 2e420c6e14..e4a5a07444 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -472,7 +472,7 @@ let diff_and_rename current_file = | Some cil_file, Some solver_data -> Some ({cil_file; solver_data}: Analyses.analyzed_data) | _, _ -> None in - {Analyses.changes = changes; old_data; new_file = current_file} + {Analyses.changes = changes; old_data } in change_info let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *) @@ -505,7 +505,7 @@ let main () = ) in if get_bool "server.enabled" then Server.start file do_analyze else ( - let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data file in + let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data in file|> do_analyze changeInfo; do_stats (); do_html_output (); diff --git a/src/util/server.ml b/src/util/server.ml index fb8425a61d..c9dcbceb00 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -113,8 +113,8 @@ let analyze ?(reset=false) ({ file; do_analyze; _ }: t)= | Some solver_data -> let changes = CompareCIL.compareCilFiles file file in let old_data = Some { Analyses.cil_file = file; solver_data } in - { Analyses.changes; old_data; new_file = file }, false - | _ -> Analyses.empty_increment_data file, true + { Analyses.changes; old_data }, false + | _ -> Analyses.empty_increment_data, true in GobConfig.set_bool "incremental.load" (not fresh); do_analyze increment_data file; From ea8eb4c9a64bbfe92c3cd4f50c5b1e7dca6f877d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 16 Feb 2022 10:44:46 +0200 Subject: [PATCH 06/17] Remove write-only analyzed_data.cil_file field --- src/framework/analyses.ml | 1 - src/maingoblint.ml | 2 +- src/util/server.ml | 2 +- 3 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 0ee9a44a1d..37fce872e4 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -432,7 +432,6 @@ sig end type analyzed_data = { - cil_file: Cil.file ; solver_data: Obj.t; } diff --git a/src/maingoblint.ml b/src/maingoblint.ml index e4a5a07444..7731cc0b3b 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -469,7 +469,7 @@ let diff_and_rename current_file = Serialize.store_data (version_map, max_ids) Serialize.VersionData end; let old_data = match old_file, solver_data with - | Some cil_file, Some solver_data -> Some ({cil_file; solver_data}: Analyses.analyzed_data) + | Some cil_file, Some solver_data -> Some ({solver_data}: Analyses.analyzed_data) | _, _ -> None in {Analyses.changes = changes; old_data } diff --git a/src/util/server.ml b/src/util/server.ml index c9dcbceb00..4aa1da73c1 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -112,7 +112,7 @@ let analyze ?(reset=false) ({ file; do_analyze; _ }: t)= let increment_data, fresh = match !Serialize.server_solver_data with | Some solver_data -> let changes = CompareCIL.compareCilFiles file file in - let old_data = Some { Analyses.cil_file = file; solver_data } in + let old_data = Some { Analyses.solver_data } in { Analyses.changes; old_data }, false | _ -> Analyses.empty_increment_data, true in From 51d8cffe4b7b3037baa07ff369ccfd1ea5fa43f1 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 16 Feb 2022 10:46:35 +0200 Subject: [PATCH 07/17] Remove analyzed_data record --- src/framework/analyses.ml | 8 ++------ src/framework/control.ml | 2 +- src/maingoblint.ml | 6 +++--- src/util/server.ml | 4 ++-- 4 files changed, 8 insertions(+), 12 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 37fce872e4..a617d0983a 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -431,17 +431,13 @@ sig val access: (D.t, G.t, C.t, V.t) ctx -> exp -> varinfo option -> bool -> A.t end -type analyzed_data = { - solver_data: Obj.t; -} - type increment_data = { - old_data: analyzed_data option; + solver_data: Obj.t option; changes: CompareCIL.change_info } let empty_increment_data = { - old_data = None; + solver_data = None; changes = CompareCIL.empty_change_info () } diff --git a/src/framework/control.ml b/src/framework/control.ml index 4c17fddafc..3af535e1be 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -436,7 +436,7 @@ struct if get_bool "dbg.verbose" then print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); Goblintutil.should_warn := get_string "warn_at" = "early" || gobview; - let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' (Option.map (fun {solver_data; _} -> solver_data) Inc.increment.old_data) in + let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' Inc.increment.solver_data in if GobConfig.get_bool "incremental.save" then Serialize.store_data solver_data Serialize.SolverData; if save_run <> "" then ( diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 7731cc0b3b..4440cc2a98 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -468,11 +468,11 @@ let diff_and_rename current_file = Serialize.store_data current_file Serialize.CilFile; Serialize.store_data (version_map, max_ids) Serialize.VersionData end; - let old_data = match old_file, solver_data with - | Some cil_file, Some solver_data -> Some ({solver_data}: Analyses.analyzed_data) + let solver_data = match old_file, solver_data with + | Some cil_file, Some solver_data -> Some solver_data | _, _ -> None in - {Analyses.changes = changes; old_data } + {Analyses.changes = changes; solver_data } in change_info let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *) diff --git a/src/util/server.ml b/src/util/server.ml index 4aa1da73c1..6afe5aa2fb 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -112,8 +112,8 @@ let analyze ?(reset=false) ({ file; do_analyze; _ }: t)= let increment_data, fresh = match !Serialize.server_solver_data with | Some solver_data -> let changes = CompareCIL.compareCilFiles file file in - let old_data = Some { Analyses.solver_data } in - { Analyses.changes; old_data }, false + let solver_data = Some solver_data in + { Analyses.changes; solver_data }, false | _ -> Analyses.empty_increment_data, true in GobConfig.set_bool "incremental.load" (not fresh); From 680c3e1bbb2d732b8be85f9c4ba8501c93929417 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 16 Feb 2022 10:55:23 +0200 Subject: [PATCH 08/17] Make incremental_data optional --- gobview | 2 +- src/framework/analyses.ml | 7 +------ src/framework/constraints.ml | 13 ++++++++----- src/framework/control.ml | 2 +- src/maingoblint.ml | 12 +++++------- src/util/server.ml | 7 +++---- 6 files changed, 19 insertions(+), 24 deletions(-) diff --git a/gobview b/gobview index 23a54c0388..cc5985a844 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 23a54c0388179abe7a5128b8fce3449d77f86763 +Subproject commit cc5985a84438911a272bad359a08f27697b36185 diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index a617d0983a..87debf0a3b 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -432,15 +432,10 @@ sig end type increment_data = { - solver_data: Obj.t option; + solver_data: Obj.t; changes: CompareCIL.change_info } -let empty_increment_data = { - solver_data = None; - changes = CompareCIL.empty_change_info () -} - type 'v sys_change_info = { obsolete: 'v list; delete: 'v list; diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 0f8e6fbbb2..46a829abf9 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -448,7 +448,7 @@ end module type Increment = sig - val increment: increment_data + val increment: increment_data option end (** Combined variables so that we can also use the more common [EqConstrSys] @@ -824,7 +824,10 @@ struct let sys_change getl getg = let open CompareCIL in - let c = I.increment.changes in + let c = match I.increment with + | Some {changes; _} -> changes + | None -> empty_change_info () + in List.(Printf.printf "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed)); let changed_funs = List.filter_map (function @@ -832,21 +835,21 @@ struct print_endline ("Completely changed function: " ^ f.svar.vname); Some f | _ -> None - ) I.increment.changes.changed + ) c.changed in let part_changed_funs = List.filter_map (function | {old = GFun (f, _); diff = Some nd; _} -> print_endline ("Partially changed function: " ^ f.svar.vname); Some (f, nd.primObsoleteNodes, nd.unchangedNodes) | _ -> None - ) I.increment.changes.changed + ) c.changed in let removed_funs = List.filter_map (function | GFun (f, _) -> print_endline ("Removed function: " ^ f.svar.vname); Some f | _ -> None - ) I.increment.changes.removed + ) c.removed in let module HM = Hashtbl.Make (Var2 (LVar) (GVar)) in diff --git a/src/framework/control.ml b/src/framework/control.ml index 3af535e1be..7f872eadaa 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -436,7 +436,7 @@ struct if get_bool "dbg.verbose" then print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); Goblintutil.should_warn := get_string "warn_at" = "early" || gobview; - let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' Inc.increment.solver_data in + let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' (Option.map (fun {solver_data; _} -> solver_data) Inc.increment) in if GobConfig.get_bool "incremental.save" then Serialize.store_data solver_data Serialize.SolverData; if save_run <> "" then ( diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 4440cc2a98..f2feb8f527 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -444,7 +444,7 @@ let handle_extraspecials () = (* Detects changes and renames vids and sids. *) let diff_and_rename current_file = (* Create change info, either from old results, or from scratch if there are no previous results. *) - let change_info: Analyses.increment_data = + let change_info: Analyses.increment_data option = if GobConfig.get_bool "incremental.load" && not (Serialize.results_exist ()) then begin let warn m = eprint_color ("{yellow}Warning: "^m) in warn "incremental.load is activated but no data exists that can be loaded." @@ -468,11 +468,9 @@ let diff_and_rename current_file = Serialize.store_data current_file Serialize.CilFile; Serialize.store_data (version_map, max_ids) Serialize.VersionData end; - let solver_data = match old_file, solver_data with - | Some cil_file, Some solver_data -> Some solver_data - | _, _ -> None - in - {Analyses.changes = changes; solver_data } + match old_file, solver_data with + | Some cil_file, Some solver_data -> Some {Analyses.changes = changes; solver_data } + | _, _ -> None in change_info let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *) @@ -505,7 +503,7 @@ let main () = ) in if get_bool "server.enabled" then Server.start file do_analyze else ( - let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data in + let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else None in file|> do_analyze changeInfo; do_stats (); do_html_output (); diff --git a/src/util/server.ml b/src/util/server.ml index 6afe5aa2fb..fb2b68ac78 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -5,7 +5,7 @@ exception Failure of Response.Error.Code.t * string type t = { file: Cil.file; - do_analyze: Analyses.increment_data -> Cil.file -> unit; + do_analyze: Analyses.increment_data option -> Cil.file -> unit; input: IO.input; output: unit IO.output; } @@ -112,9 +112,8 @@ let analyze ?(reset=false) ({ file; do_analyze; _ }: t)= let increment_data, fresh = match !Serialize.server_solver_data with | Some solver_data -> let changes = CompareCIL.compareCilFiles file file in - let solver_data = Some solver_data in - { Analyses.changes; solver_data }, false - | _ -> Analyses.empty_increment_data, true + Some { Analyses.changes; solver_data }, false + | _ -> None, true in GobConfig.set_bool "incremental.load" (not fresh); do_analyze increment_data file; From ed36dd2f279eeb2b9debdf7e5fc94da6a6d73e95 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Oct 2022 13:57:36 +0300 Subject: [PATCH 09/17] Fix partial Stats.time in Control --- src/framework/control.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/framework/control.ml b/src/framework/control.ml index 2a367cd3e6..f70b2a1885 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -463,7 +463,7 @@ struct if get_bool "dbg.verbose" then print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); Goblintutil.should_warn := get_string "warn_at" = "early" || gobview; - let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' (Option.map (fun {solver_data; _} -> solver_data) Inc.increment) in + let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global startvars') (Option.map (fun {solver_data; _} -> solver_data) Inc.increment) in if GobConfig.get_bool "incremental.save" then Serialize.Cache.(update_data SolverData solver_data); if save_run_str <> "" then ( From 63ee7bd1ef375df2174edc4bd93a36673e92a93f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Oct 2022 14:11:46 +0300 Subject: [PATCH 10/17] Extract copy_marshal and relift_marshal in TD3 --- src/solvers/td3.ml | 139 +++++++++++++++++++++++---------------------- 1 file changed, 72 insertions(+), 67 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index edb306383c..0c4a0e6324 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -70,6 +70,73 @@ module WP = (* vice versa doesn't currently hold, because stable is not pruned *) ) + let copy_marshal (data: marshal): unit = (* TODO: should return new marshal? *) + data.rho <- HM.copy data.rho; + data.stable <- HM.copy data.stable; + data.wpoint <- HM.copy data.wpoint; + data.infl <- HM.copy data.infl; + data.side_infl <- HM.copy data.side_infl; + data.side_dep <- HM.copy data.side_dep; + (* data.st is immutable, no need to copy *) + data.var_messages <- HM.copy data.var_messages; + data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *) + data.dep <- HM.copy data.dep + + let relift_marshal (data: marshal): unit = (* TODO: should return new marshal? *) + let rho' = HM.create (HM.length data.rho) in + HM.iter (fun k v -> + (* call hashcons on contexts and abstract values; results in new tags *) + let k' = S.Var.relift k in + let v' = S.Dom.relift v in + HM.replace rho' k' v'; + ) data.rho; + data.rho <- rho'; + let stable' = HM.create (HM.length data.stable) in + HM.iter (fun k v -> + HM.replace stable' (S.Var.relift k) v + ) data.stable; + data.stable <- stable'; + let wpoint' = HM.create (HM.length data.wpoint) in + HM.iter (fun k v -> + HM.replace wpoint' (S.Var.relift k) v + ) data.wpoint; + data.wpoint <- wpoint'; + let infl' = HM.create (HM.length data.infl) in + HM.iter (fun k v -> + HM.replace infl' (S.Var.relift k) (VS.map S.Var.relift v) + ) data.infl; + data.infl <- infl'; + let side_infl' = HM.create (HM.length data.side_infl) in + HM.iter (fun k v -> + HM.replace side_infl' (S.Var.relift k) (VS.map S.Var.relift v) + ) data.side_infl; + data.side_infl <- side_infl'; + let side_dep' = HM.create (HM.length data.side_dep) in + HM.iter (fun k v -> + HM.replace side_dep' (S.Var.relift k) (VS.map S.Var.relift v) + ) data.side_dep; + data.side_dep <- side_dep'; + data.st <- List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st; + let var_messages' = HM.create (HM.length data.var_messages) in + HM.iter (fun k v -> + HM.add var_messages' (S.Var.relift k) v (* var_messages contains duplicate keys, so must add not replace! *) + ) data.var_messages; + data.var_messages <- var_messages'; + let rho_write' = HM.create (HM.length data.rho_write) in + HM.iter (fun x w -> + let w' = HM.create (HM.length w) in + HM.iter (fun y d -> + HM.add w' (S.Var.relift y) (S.Dom.relift d) (* w contains duplicate keys, so must add not replace! *) + ) w; + HM.replace rho_write' (S.Var.relift x) w'; + ) data.rho_write; + data.rho_write <- rho_write'; + let dep' = HM.create (HM.length data.dep) in + HM.iter (fun k v -> + HM.replace dep' (S.Var.relift k) (VS.map S.Var.relift v) + ) data.dep; + data.dep <- dep' + let exists_key f hm = HM.fold (fun k _ a -> a || f k) hm false module P = @@ -903,73 +970,11 @@ module WP = * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have * the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values). *) - if loaded && (false (* && S.increment.server *)) then ( (* TODO: fix server *) - data.rho <- HM.copy data.rho; - data.stable <- HM.copy data.stable; - data.wpoint <- HM.copy data.wpoint; - data.infl <- HM.copy data.infl; - data.side_infl <- HM.copy data.side_infl; - data.side_dep <- HM.copy data.side_dep; - (* data.st is immutable, no need to copy *) - data.var_messages <- HM.copy data.var_messages; - data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *) - data.dep <- HM.copy data.dep; - ) - else if loaded && GobConfig.get_bool "ana.opt.hashcons" then ( - let rho' = HM.create (HM.length data.rho) in - HM.iter (fun k v -> - (* call hashcons on contexts and abstract values; results in new tags *) - let k' = S.Var.relift k in - let v' = S.Dom.relift v in - HM.replace rho' k' v'; - ) data.rho; - data.rho <- rho'; - let stable' = HM.create (HM.length data.stable) in - HM.iter (fun k v -> - HM.replace stable' (S.Var.relift k) v - ) data.stable; - data.stable <- stable'; - let wpoint' = HM.create (HM.length data.wpoint) in - HM.iter (fun k v -> - HM.replace wpoint' (S.Var.relift k) v - ) data.wpoint; - data.wpoint <- wpoint'; - let infl' = HM.create (HM.length data.infl) in - HM.iter (fun k v -> - HM.replace infl' (S.Var.relift k) (VS.map S.Var.relift v) - ) data.infl; - data.infl <- infl'; - let side_infl' = HM.create (HM.length data.side_infl) in - HM.iter (fun k v -> - HM.replace side_infl' (S.Var.relift k) (VS.map S.Var.relift v) - ) data.side_infl; - data.side_infl <- side_infl'; - let side_dep' = HM.create (HM.length data.side_dep) in - HM.iter (fun k v -> - HM.replace side_dep' (S.Var.relift k) (VS.map S.Var.relift v) - ) data.side_dep; - data.side_dep <- side_dep'; - data.st <- List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st; - let var_messages' = HM.create (HM.length data.var_messages) in - HM.iter (fun k v -> - HM.add var_messages' (S.Var.relift k) v (* var_messages contains duplicate keys, so must add not replace! *) - ) data.var_messages; - data.var_messages <- var_messages'; - let rho_write' = HM.create (HM.length data.rho_write) in - HM.iter (fun x w -> - let w' = HM.create (HM.length w) in - HM.iter (fun y d -> - HM.add w' (S.Var.relift y) (S.Dom.relift d) (* w contains duplicate keys, so must add not replace! *) - ) w; - HM.replace rho_write' (S.Var.relift x) w'; - ) data.rho_write; - data.rho_write <- rho_write'; - let dep' = HM.create (HM.length data.dep) in - HM.iter (fun k v -> - HM.replace dep' (S.Var.relift k) (VS.map S.Var.relift v) - ) data.dep; - data.dep <- dep'; - ); + if loaded && (false (* && S.increment.server *)) then (* TODO: fix server *) + copy_marshal data + else if loaded && GobConfig.get_bool "ana.opt.hashcons" then + relift_marshal data; + if not reuse_stable then ( print_endline "Destabilizing everything!"; data.stable <- HM.create 10; From 8caf7ea03464c3ada17eb3ce9bc2b51245ec4844 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Oct 2022 14:15:17 +0300 Subject: [PATCH 11/17] Add copy_marshal and relift_marshal to solver signature --- src/framework/analyses.ml | 3 +++ src/framework/constraints.ml | 2 ++ src/solvers/selector.ml | 10 ++++++++++ 3 files changed, 15 insertions(+) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 67c89566a3..2256bcd88d 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -548,6 +548,9 @@ module type GenericEqBoxIncrSolverBase = sig type marshal + val copy_marshal: marshal -> unit + val relift_marshal: marshal -> unit + (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs], reached from starting values [xs]. As a second component the solver returns data structures for incremental serialization. *) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index c36d46cc1d..943d6bddb0 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -928,6 +928,8 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve module Post = PostSolver.MakeList (PostSolver.ListArgFromStdArg (S) (VH) (Arg)) type marshal = unit + let copy_marshal () = () + let relift_marshal () = () let solve box xs vs _ = let vh = Sol.solve box xs vs in diff --git a/src/solvers/selector.ml b/src/solvers/selector.ml index cc75ed96e8..ec6131e85c 100644 --- a/src/solvers/selector.ml +++ b/src/solvers/selector.ml @@ -22,6 +22,16 @@ module Make = struct type marshal = Obj.t (* cannot use Sol.marshal because cannot unpack first-class module in applicative functor *) + let copy_marshal (marshal: marshal) = + let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in + let module F = Sol (Arg) (S) (VH) in + F.copy_marshal (Obj.obj marshal) + + let relift_marshal (marshal: marshal) = + let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in + let module F = Sol (Arg) (S) (VH) in + F.relift_marshal (Obj.obj marshal) + let solve box xs vs (old_data: marshal option) = let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in let module F = Sol (Arg) (S) (VH) in From 2b403fdaedd741e247b2f084a02132e8a3be3559 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Oct 2022 14:57:47 +0300 Subject: [PATCH 12/17] Move solver data relifting out of TD3 --- src/framework/analyses.ml | 3 +++ src/framework/constraints.ml | 3 +++ src/framework/control.ml | 12 +++++++++++- src/solvers/td3.ml | 4 ---- 4 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 2256bcd88d..2a3f02267c 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -589,6 +589,9 @@ module type GenericGlobSolver = sig type marshal + val copy_marshal: marshal -> unit + val relift_marshal: marshal -> unit + (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs], reached from starting values [xs]. As a second component the solver returns data structures for incremental serialization. *) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 943d6bddb0..86822a9aa0 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1045,6 +1045,9 @@ module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase) type marshal = Sol'.marshal + let copy_marshal = Sol'.copy_marshal + let relift_marshal = Sol'.relift_marshal + let solve ls gs l old_data = let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls @ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in diff --git a/src/framework/control.ml b/src/framework/control.ml index f70b2a1885..6c1867e105 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -460,10 +460,20 @@ struct r1 (* return the result of the first run for further options -- maybe better to exit early since compare_runs is its own mode. Only excluded verify below since it's on by default. *) | _ -> failwith "Currently only two runs can be compared!"; ) else ( + let solver_data = + match Inc.increment with + | Some {solver_data; server; _} -> + if server then + Slvr.copy_marshal solver_data + else if GobConfig.get_bool "ana.opt.hashcons" then + Slvr.relift_marshal solver_data; + Some solver_data + | None -> None + in if get_bool "dbg.verbose" then print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ "."); Goblintutil.should_warn := get_string "warn_at" = "early" || gobview; - let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global startvars') (Option.map (fun {solver_data; _} -> solver_data) Inc.increment) in + let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global startvars') solver_data in if GobConfig.get_bool "incremental.save" then Serialize.Cache.(update_data SolverData solver_data); if save_run_str <> "" then ( diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 0c4a0e6324..2fa4d6c4a7 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -970,10 +970,6 @@ module WP = * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have * the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values). *) - if loaded && (false (* && S.increment.server *)) then (* TODO: fix server *) - copy_marshal data - else if loaded && GobConfig.get_bool "ana.opt.hashcons" then - relift_marshal data; if not reuse_stable then ( print_endline "Destabilizing everything!"; From e1c73d1bb3e750709830e51b8c4a017507de7bf3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Oct 2022 15:06:20 +0300 Subject: [PATCH 13/17] Clean up incremental solve wrapping in TD3 --- src/solvers/td3.ml | 74 +++++++++++++++++++++------------------------- 1 file changed, 33 insertions(+), 41 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 2fa4d6c4a7..45c92e006f 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -82,6 +82,21 @@ module WP = data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *) data.dep <- HM.copy data.dep + (* This hack is for fixing hashconsing. + * If hashcons is enabled now, then it also was for the loaded values (otherwise it would crash). If it is off, we don't need to do anything. + * HashconsLifter uses BatHashcons.hashcons on Lattice operations like join, so we call join (with bot) to make sure that the old values will populate the empty hashcons table via side-effects and at the same time get new tags that are conform with its state. + * The tags are used for `equals` and `compare` to avoid structural comparisons. TODO could this be replaced by `==` (if values are shared by hashcons they should be physically equal)? + * We have to replace all tags since they are not derived from the value (like hash) but are incremented starting with 1, i.e. dependent on the order in which lattice operations for different values are called, which will very likely be different for an incremental run. + * If we didn't do this, during solve, a rhs might give the same value as from the old rho but it wouldn't be detected as equal since the tags would be different. + * In the worst case, every rhs would yield the same value, but we would destabilize for every var in rho until we replaced all values (just with new tags). + * The other problem is that we would likely use more memory since values from old rho would not be shared with the same values in the hashcons table. So we would keep old values in memory until they are replace in rho and eventually garbage collected. + *) + (* Another problem are the tags for the context part of a S.Var.t. + * This will cause problems when old and new vars interact or when new S.Dom values are used as context: + * - reachability is a problem since it marks vars reachable with a new tag, which will remove vars with the same context but old tag from rho. + * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have + * the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values). + *) let relift_marshal (data: marshal): unit = (* TODO: should return new marshal? *) let rho' = HM.create (HM.length data.rho) in HM.iter (fun k v -> @@ -151,7 +166,23 @@ module WP = module CurrentVarS = Constraints.CurrentVarEqConstrSys (S) module S = CurrentVarS.S - let solve box st vs data = + let solve box st vs marshal = + let reuse_stable = GobConfig.get_bool "incremental.stable" in + let reuse_wpoint = GobConfig.get_bool "incremental.wpoint" in + let data = + match marshal with + | Some data -> + if not reuse_stable then ( + print_endline "Destabilizing everything!"; + data.stable <- HM.create 10; + data.infl <- HM.create 10 + ); + if not reuse_wpoint then data.wpoint <- HM.create 10; + data + | None -> + create_empty_data () + in + let term = GobConfig.get_bool "solvers.td3.term" in let side_widen = GobConfig.get_string "solvers.td3.side_widen" in let space = GobConfig.get_bool "solvers.td3.space" in @@ -945,46 +976,7 @@ module WP = print_data data "Data after postsolve"; verify_data data; - {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep} - - let solve box st vs (old_data: marshal option) = - let reuse_stable = GobConfig.get_bool "incremental.stable" in - let reuse_wpoint = GobConfig.get_bool "incremental.wpoint" in - if GobConfig.get_bool "incremental.load" then ( - let loaded, data = match old_data with - | Some d -> true, d - | _ -> false, create_empty_data () - in - (* This hack is for fixing hashconsing. - * If hashcons is enabled now, then it also was for the loaded values (otherwise it would crash). If it is off, we don't need to do anything. - * HashconsLifter uses BatHashcons.hashcons on Lattice operations like join, so we call join (with bot) to make sure that the old values will populate the empty hashcons table via side-effects and at the same time get new tags that are conform with its state. - * The tags are used for `equals` and `compare` to avoid structural comparisons. TODO could this be replaced by `==` (if values are shared by hashcons they should be physically equal)? - * We have to replace all tags since they are not derived from the value (like hash) but are incremented starting with 1, i.e. dependent on the order in which lattice operations for different values are called, which will very likely be different for an incremental run. - * If we didn't do this, during solve, a rhs might give the same value as from the old rho but it wouldn't be detected as equal since the tags would be different. - * In the worst case, every rhs would yield the same value, but we would destabilize for every var in rho until we replaced all values (just with new tags). - * The other problem is that we would likely use more memory since values from old rho would not be shared with the same values in the hashcons table. So we would keep old values in memory until they are replace in rho and eventually garbage collected. - *) - (* Another problem are the tags for the context part of a S.Var.t. - * This will cause problems when old and new vars interact or when new S.Dom values are used as context: - * - reachability is a problem since it marks vars reachable with a new tag, which will remove vars with the same context but old tag from rho. - * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have - * the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values). - *) - - if not reuse_stable then ( - print_endline "Destabilizing everything!"; - data.stable <- HM.create 10; - data.infl <- HM.create 10 - ); - if not reuse_wpoint then data.wpoint <- HM.create 10; - let result = solve box st vs data in - result.rho, result - ) - else ( - let data = create_empty_data () in - let result = solve box st vs data in - result.rho, result - ) + (rho, {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}) end let _ = From 28bb206c9b6ee27e777f3a5fdc6e69678cc16faf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Oct 2022 15:10:29 +0300 Subject: [PATCH 14/17] Remove iter_vars from constraint system --- src/framework/analyses.ml | 3 --- src/framework/constraints.ml | 3 --- 2 files changed, 6 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 2a3f02267c..49f303b7b7 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -518,8 +518,6 @@ sig (** The system in functional form. *) val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m - val iter_vars: (v -> d) -> VarQuery.t -> v VarQuery.f -> unit - (** Data used for incremental analysis *) val sys_change: (v -> d) -> v sys_change_info end @@ -536,7 +534,6 @@ sig module D : Lattice.S module G : Lattice.S 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 val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info end diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 86822a9aa0..85f8df4e24 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -984,9 +984,6 @@ struct | `G _ -> None | `L x -> Option.map conv (S.system x) - let iter_vars get vq f = - S.iter_vars (getL % get % l) (getG % get % g) vq (f % l) (f % g) - let sys_change get = S.sys_change (getL % get % l) (getG % get % g) end From e281f7a6ad2add14827eb861e65f61501ead2624 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Oct 2022 15:23:24 +0300 Subject: [PATCH 15/17] Update sys_change documentation --- src/framework/analyses.ml | 12 +++++++----- src/solvers/td3.ml | 6 ++++-- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 49f303b7b7..091ef0e18c 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -492,11 +492,13 @@ type increment_data = { restarting: VarQuery.t list; } +(** Abstract incremental change to constraint system. + @param 'v constrain system variable type *) type 'v sys_change_info = { - obsolete: 'v list; - delete: 'v list; - reluctant: 'v list; - restart: 'v list; + obsolete: 'v list; (** Variables to destabilize. *) + delete: 'v list; (** Variables to delete. *) + reluctant: 'v list; (** Variables to solve reluctantly. *) + restart: 'v list; (** Variables to restart. *) } (** A side-effecting system. *) @@ -518,8 +520,8 @@ sig (** The system in functional form. *) val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m - (** Data used for incremental analysis *) val sys_change: (v -> d) -> v sys_change_info + (** Compute incremental constraint system change from old solution. *) end (** Any system of side-effecting equations over lattices. *) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 45c92e006f..a80a404982 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -212,6 +212,8 @@ module WP = These don't have to be re-verified and warnings can be reused. *) let superstable = HM.copy stable in + let reluctant = GobConfig.get_bool "incremental.reluctant.enabled" in + let var_messages = data.var_messages in let rho_write = data.rho_write in let dep = data.dep in @@ -557,7 +559,7 @@ module WP = let sys_change = S.sys_change (fun v -> try HM.find rho v with Not_found -> S.Dom.bot ()) in let old_ret = HM.create 103 in - if GobConfig.get_bool "incremental.reluctant.enabled" then ( + if reluctant then ( (* save entries of changed functions in rho for the comparison whether the result has changed after a function specific solve *) List.iter (fun k -> if HM.mem rho k then ( @@ -677,7 +679,7 @@ module WP = (* TODO: reluctant doesn't call destabilize on removed functions or old copies of modified functions (e.g. after removing write), so those globals don't get restarted *) - if GobConfig.get_bool "incremental.reluctant.enabled" then ( + if reluctant then ( (* solve on the return node of changed functions. Only destabilize the function's return node if the analysis result changed *) print_endline "Separately solving changed functions..."; let op = if GobConfig.get_string "incremental.reluctant.compare" = "leq" then S.Dom.leq else S.Dom.equal in From 7b06f1ba0109443913e6eff5cd616068dc3c8bfe Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Oct 2022 16:03:35 +0300 Subject: [PATCH 16/17] Make TD3 solver data record immutable --- src/framework/analyses.ml | 8 +-- src/framework/control.ml | 7 +-- src/solvers/selector.ml | 4 +- src/solvers/td3.ml | 108 +++++++++++++++++++------------------- 4 files changed, 64 insertions(+), 63 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 091ef0e18c..a5d5a715e0 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -547,8 +547,8 @@ module type GenericEqBoxIncrSolverBase = sig type marshal - val copy_marshal: marshal -> unit - val relift_marshal: marshal -> unit + val copy_marshal: marshal -> marshal + val relift_marshal: marshal -> marshal (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs], reached from starting values [xs]. @@ -588,8 +588,8 @@ module type GenericGlobSolver = sig type marshal - val copy_marshal: marshal -> unit - val relift_marshal: marshal -> unit + val copy_marshal: marshal -> marshal + val relift_marshal: marshal -> marshal (** The hash-map that is the first component of [solve box xs vs] is a local solution for interesting variables [vs], reached from starting values [xs]. diff --git a/src/framework/control.ml b/src/framework/control.ml index 6c1867e105..8e33afc1eb 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -464,10 +464,11 @@ struct match Inc.increment with | Some {solver_data; server; _} -> if server then - Slvr.copy_marshal solver_data + Some (Slvr.copy_marshal solver_data) (* Copy, so that we can abort and reuse old data unmodified. *) else if GobConfig.get_bool "ana.opt.hashcons" then - Slvr.relift_marshal solver_data; - Some solver_data + Some (Slvr.relift_marshal solver_data) + else + Some solver_data | None -> None in if get_bool "dbg.verbose" then diff --git a/src/solvers/selector.ml b/src/solvers/selector.ml index ec6131e85c..082c11b410 100644 --- a/src/solvers/selector.ml +++ b/src/solvers/selector.ml @@ -25,12 +25,12 @@ module Make = let copy_marshal (marshal: marshal) = let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in let module F = Sol (Arg) (S) (VH) in - F.copy_marshal (Obj.obj marshal) + Obj.repr (F.copy_marshal (Obj.obj marshal)) let relift_marshal (marshal: marshal) = let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in let module F = Sol (Arg) (S) (VH) in - F.relift_marshal (Obj.obj marshal) + Obj.repr (F.relift_marshal (Obj.obj marshal)) let solve box xs vs (old_data: marshal option) = let module Sol = (val choose_solver (get_string "solver") : GenericEqBoxIncrSolver) in diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index a80a404982..a4120b1e63 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -24,17 +24,17 @@ module WP = module VS = Set.Make (S.Var) type solver_data = { - mutable st: (S.Var.t * S.Dom.t) list; (* needed to destabilize start functions if their start state changed because of some changed global initializer *) - mutable infl: VS.t HM.t; - mutable sides: VS.t HM.t; - mutable rho: S.Dom.t HM.t; - mutable wpoint: unit HM.t; - mutable stable: unit HM.t; - mutable side_dep: VS.t HM.t; (** Dependencies of side-effected variables. Knowing these allows restarting them and re-triggering all side effects. *) - mutable side_infl: VS.t HM.t; (** Influences to side-effected variables. Not normally in [infl], but used for restarting them. *) - mutable var_messages: Message.t HM.t; (** Messages from right-hand sides of variables. Used for incremental postsolving. *) - mutable rho_write: S.Dom.t HM.t HM.t; (** Side effects from variables to write-only variables with values. Used for fast incremental restarting of write-only variables. *) - mutable dep: VS.t HM.t; (** Dependencies of variables. Inverse of [infl]. Used for fast pre-reachable pruning in incremental postsolving. *) + st: (S.Var.t * S.Dom.t) list; (* needed to destabilize start functions if their start state changed because of some changed global initializer *) + infl: VS.t HM.t; + sides: VS.t HM.t; + rho: S.Dom.t HM.t; + wpoint: unit HM.t; + stable: unit HM.t; + side_dep: VS.t HM.t; (** Dependencies of side-effected variables. Knowing these allows restarting them and re-triggering all side effects. *) + side_infl: VS.t HM.t; (** Influences to side-effected variables. Not normally in [infl], but used for restarting them. *) + var_messages: Message.t HM.t; (** Messages from right-hand sides of variables. Used for incremental postsolving. *) + rho_write: S.Dom.t HM.t HM.t; (** Side effects from variables to write-only variables with values. Used for fast incremental restarting of write-only variables. *) + dep: VS.t HM.t; (** Dependencies of variables. Inverse of [infl]. Used for fast pre-reachable pruning in incremental postsolving. *) } type marshal = solver_data @@ -70,17 +70,20 @@ module WP = (* vice versa doesn't currently hold, because stable is not pruned *) ) - let copy_marshal (data: marshal): unit = (* TODO: should return new marshal? *) - data.rho <- HM.copy data.rho; - data.stable <- HM.copy data.stable; - data.wpoint <- HM.copy data.wpoint; - data.infl <- HM.copy data.infl; - data.side_infl <- HM.copy data.side_infl; - data.side_dep <- HM.copy data.side_dep; - (* data.st is immutable, no need to copy *) - data.var_messages <- HM.copy data.var_messages; - data.rho_write <- HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *) - data.dep <- HM.copy data.dep + let copy_marshal (data: marshal): marshal = + { + rho = HM.copy data.rho; + stable = HM.copy data.stable; + wpoint = HM.copy data.wpoint; + infl = HM.copy data.infl; + sides = HM.copy data.sides; + side_infl = HM.copy data.side_infl; + side_dep = HM.copy data.side_dep; + st = data.st; (* data.st is immutable *) + var_messages = HM.copy data.var_messages; + rho_write = HM.map (fun x w -> HM.copy w) data.rho_write; (* map copies outer HM *) + dep = HM.copy data.dep; + } (* This hack is for fixing hashconsing. * If hashcons is enabled now, then it also was for the loaded values (otherwise it would crash). If it is off, we don't need to do anything. @@ -97,60 +100,56 @@ module WP = * - If we destabilized a node with a call, we will also destabilize all vars of the called function. However, if we end up with the same state at the caller node, without hashcons we would only need to go over all vars in the function once to restabilize them since we have * the old values, whereas with hashcons, we would get a context with a different tag, could not find the old value for that var, and have to recompute all vars in the function (without access to old values). *) - let relift_marshal (data: marshal): unit = (* TODO: should return new marshal? *) - let rho' = HM.create (HM.length data.rho) in + let relift_marshal (data: marshal): marshal = + let rho = HM.create (HM.length data.rho) in HM.iter (fun k v -> (* call hashcons on contexts and abstract values; results in new tags *) let k' = S.Var.relift k in let v' = S.Dom.relift v in - HM.replace rho' k' v'; + HM.replace rho k' v'; ) data.rho; - data.rho <- rho'; - let stable' = HM.create (HM.length data.stable) in + let stable = HM.create (HM.length data.stable) in HM.iter (fun k v -> - HM.replace stable' (S.Var.relift k) v + HM.replace stable (S.Var.relift k) v ) data.stable; - data.stable <- stable'; - let wpoint' = HM.create (HM.length data.wpoint) in + let wpoint = HM.create (HM.length data.wpoint) in HM.iter (fun k v -> - HM.replace wpoint' (S.Var.relift k) v + HM.replace wpoint (S.Var.relift k) v ) data.wpoint; - data.wpoint <- wpoint'; - let infl' = HM.create (HM.length data.infl) in + let infl = HM.create (HM.length data.infl) in HM.iter (fun k v -> - HM.replace infl' (S.Var.relift k) (VS.map S.Var.relift v) + HM.replace infl (S.Var.relift k) (VS.map S.Var.relift v) ) data.infl; - data.infl <- infl'; - let side_infl' = HM.create (HM.length data.side_infl) in + let sides = HM.create (HM.length data.sides) in HM.iter (fun k v -> - HM.replace side_infl' (S.Var.relift k) (VS.map S.Var.relift v) + HM.replace sides (S.Var.relift k) (VS.map S.Var.relift v) + ) data.sides; + let side_infl = HM.create (HM.length data.side_infl) in + HM.iter (fun k v -> + HM.replace side_infl (S.Var.relift k) (VS.map S.Var.relift v) ) data.side_infl; - data.side_infl <- side_infl'; - let side_dep' = HM.create (HM.length data.side_dep) in + let side_dep = HM.create (HM.length data.side_dep) in HM.iter (fun k v -> - HM.replace side_dep' (S.Var.relift k) (VS.map S.Var.relift v) + HM.replace side_dep (S.Var.relift k) (VS.map S.Var.relift v) ) data.side_dep; - data.side_dep <- side_dep'; - data.st <- List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st; - let var_messages' = HM.create (HM.length data.var_messages) in + let st = List.map (fun (k, v) -> S.Var.relift k, S.Dom.relift v) data.st in + let var_messages = HM.create (HM.length data.var_messages) in HM.iter (fun k v -> - HM.add var_messages' (S.Var.relift k) v (* var_messages contains duplicate keys, so must add not replace! *) + HM.add var_messages (S.Var.relift k) v (* var_messages contains duplicate keys, so must add not replace! *) ) data.var_messages; - data.var_messages <- var_messages'; - let rho_write' = HM.create (HM.length data.rho_write) in + let rho_write = HM.create (HM.length data.rho_write) in HM.iter (fun x w -> let w' = HM.create (HM.length w) in HM.iter (fun y d -> HM.add w' (S.Var.relift y) (S.Dom.relift d) (* w contains duplicate keys, so must add not replace! *) ) w; - HM.replace rho_write' (S.Var.relift x) w'; + HM.replace rho_write (S.Var.relift x) w'; ) data.rho_write; - data.rho_write <- rho_write'; - let dep' = HM.create (HM.length data.dep) in + let dep = HM.create (HM.length data.dep) in HM.iter (fun k v -> - HM.replace dep' (S.Var.relift k) (VS.map S.Var.relift v) + HM.replace dep (S.Var.relift k) (VS.map S.Var.relift v) ) data.dep; - data.dep <- dep' + {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep} let exists_key f hm = HM.fold (fun k _ a -> a || f k) hm false @@ -174,10 +173,11 @@ module WP = | Some data -> if not reuse_stable then ( print_endline "Destabilizing everything!"; - data.stable <- HM.create 10; - data.infl <- HM.create 10 + HM.clear data.stable; + HM.clear data.infl ); - if not reuse_wpoint then data.wpoint <- HM.create 10; + if not reuse_wpoint then + HM.clear data.wpoint; data | None -> create_empty_data () From 1e443776e6acfbed7867f0ab9a7d40e376493260 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 30 Nov 2022 13:35:13 +0200 Subject: [PATCH 17/17] Remove unused Stats alias in TD3 --- src/solvers/td3.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index f22c94aba3..caf2cd2bab 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -13,8 +13,6 @@ open Prelude open Analyses open Messages -module Stats = GoblintCil.Stats - module WP = functor (Arg: IncrSolverArg) -> functor (S:EqConstrSys) ->