Merge pull request #909 from goblint/td3-data

Move incremental data management out of TD3

src/framework/analyses.ml

@@ -476,28 +476,17 @@ sig
   val access: (D.t, G.t, C.t, V.t) ctx -> Queries.access -> A.t
 end
 
-type analyzed_data = {
-  solver_data: Obj.t;
-}
-
 type increment_data = {
   server: bool;
 
-  old_data: analyzed_data option;
+  solver_data: Obj.t;
   changes: CompareCIL.change_info;
 
   (* Globals for which the constraint
      system unknowns should be restarted *)
   restarting: VarQuery.t list;
 }
 
-let empty_increment_data ?(server=false) () = {
-  server;
-  old_data = None;
-  changes = CompareCIL.empty_change_info ();
-  restarting = []
-}
-
 (** A side-effecting system. *)
 module type MonSystem =
 sig
@@ -518,7 +507,7 @@ sig
   val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m
 
   (** Data used for incremental analysis *)
-  val increment : increment_data
+  val increment : increment_data option
 
   val iter_vars: (v -> d) -> VarQuery.t -> v VarQuery.f -> unit
 end
@@ -534,7 +523,7 @@ sig
 
   module D : Lattice.S
   module G : Lattice.S
-  val increment : increment_data
+  val increment : increment_data option
   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
@@ -547,10 +536,13 @@ module type GenericEqBoxIncrSolverBase =
   sig
     type marshal
 
+    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].
         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. *)
@@ -585,10 +577,13 @@ module type GenericGlobSolver =
   sig
     type marshal
 
+    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].
         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) =

src/framework/constraints.ml

@@ -434,7 +434,7 @@ end
 
 module type Increment =
 sig
-  val increment: increment_data
+  val increment: increment_data option
 end
 
 (** The main point of this file---generating a [GlobConstrSys] from a [Spec]. *)
@@ -794,8 +794,10 @@ 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 solve box xs vs _ =
       let vh = Sol.solve box xs vs in
       Post.post xs vs vh;
       (vh, ())
@@ -925,7 +927,6 @@ end
 
 (** Transforms a [GenericEqBoxIncrSolver] into a [GenericGlobSolver]. *)
 module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase)
-  : GenericGlobSolver
   = functor (S:GlobConstrSys) ->
     functor (LH:Hashtbl.S with type key=S.LVar.t) ->
     functor (GH:Hashtbl.S with type key=S.GVar.t) ->
@@ -939,11 +940,14 @@ module GlobSolverFromEqSolver (Sol:GenericEqBoxIncrSolverBase)
 
       type marshal = Sol'.marshal
 
-      let solve ls gs l =
+      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
         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
 

src/framework/control.ml

@@ -421,7 +421,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
@@ -461,10 +461,21 @@ 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
+                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
+                Some (Slvr.relift_marshal solver_data)
+              else
+                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 = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' in
+          let (lh, gh), solver_data = Timing.wrap "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 (
@@ -513,7 +524,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? *)
           CompareGlobSys.compare (get_string "solver", get_string "comparesolver") (lh,gh) (r2)
         in
         compare_with (Selector.choose_solver (get_string "comparesolver"))

src/goblint.ml

@@ -56,7 +56,7 @@ let main () =
         if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then
           diff_and_rename file
         else
-          Analyses.empty_increment_data ()
+          None
       in
       if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;
       file |> do_analyze changeInfo;

src/maingoblint.ml

@@ -527,7 +527,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 =
     let warn m = eprint_color ("{yellow}Warning: "^m) in
     if GobConfig.get_bool "incremental.load" && not (Serialize.results_exist ()) then begin
       warn "incremental.load is activated but no data exists that can be loaded."
@@ -563,11 +563,9 @@ let diff_and_rename current_file =
       Serialize.Cache.(update_data CilFile current_file);
       Serialize.Cache.(update_data VersionData max_ids);
     end;
-    let old_data = match old_file, solver_data with
-      | Some cil_file, Some solver_data -> Some ({solver_data}: Analyses.analyzed_data)
-      | _, _ -> None
-    in
-    {server = false; Analyses.changes = changes; restarting; old_data}
+    match old_file, solver_data with
+    | Some cil_file, Some solver_data -> Some {server = false; Analyses.changes = changes; restarting; solver_data}
+    | _, _ -> None
   in change_info
 
 let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *)

src/solvers/selector.ml

@@ -22,10 +22,20 @@ 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 copy_marshal (marshal: marshal) =
       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
+      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
+      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
+      let module F = Sol (Arg) (S) (VH) in
+      let (vh, marshal) = F.solve box xs vs (Option.map Obj.obj old_data) in
       (vh, Obj.repr marshal)
   end