Merge pull request #1746 from arkocal/demand_constr_2

Introduce demand in constraint system

Author: michael-schwarz

src/constraint/constrSys.ml

@@ -86,6 +86,13 @@ sig
   val postmortem: v -> v list
 end
 
+(** A side-effecting system that supports [demand] calls *)
+module type DemandEqConstrSys =
+sig
+  include EqConstrSys
+  val system: v -> ((v -> d) -> (v -> d -> unit) -> (v -> unit) -> d) option
+end
+
 (** A side-effecting system with globals. *)
 module type GlobConstrSys =
 sig
@@ -100,6 +107,21 @@ sig
   val postmortem: LVar.t -> LVar.t list
 end
 
+(** A side-effecting system with globals that supports [demand] calls *)
+module type DemandGlobConstrSys =
+sig
+  module LVar : VarType
+  module GVar : VarType
+
+  module D : Lattice.S
+  module G : Lattice.S
+  val system: LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (LVar.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
+  val postmortem: LVar.t -> LVar.t list
+end
+
+
 (** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *)
 module CurrentVarEqConstrSys (S: EqConstrSys) =
 struct

src/constraint/solverTypes.ml

@@ -13,6 +13,17 @@ module type GenericEqSolver =
     val solve : (S.v*S.d) list -> S.v list -> S.d H.t
   end
 
+(** A solver is something that can translate a system into a solution (hash-table).
+    These solver can handle [DemandEqConstrSys] *)
+module type DemandEqSolver =
+  functor (S:DemandEqConstrSys) ->
+  functor (H:Hashtbl.S with type key=S.v) ->
+  sig
+    (** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
+        reached from starting values [xs]. *)
+    val solve : (S.v*S.d) list -> S.v list -> S.d H.t
+  end
+
 (** A solver is something that can translate a system into a solution (hash-table).
     Incremental solver has data to be marshaled. *)
 module type GenericEqIncrSolverBase =
@@ -44,11 +55,30 @@ module type GenericEqIncrSolver =
   functor (Arg: IncrSolverArg) ->
     GenericEqIncrSolverBase
 
+module type DemandEqIncrSolverBase =
+  functor (S: DemandEqConstrSys) ->
+  functor (H:Hashtbl.S with type key=S.v) ->
+  sig
+    type marshal
+
+    val copy_marshal: marshal -> marshal
+    val relift_marshal: marshal -> marshal
+
+    (** The hash-map that is the first component of [solve 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) list -> S.v list -> marshal option -> S.d H.t * marshal
+  end
+
+module type DemandEqIncrSolver =
+  functor (Arg: IncrSolverArg) ->
+    DemandEqIncrSolverBase
+
 (** A solver is something that can translate a system into a solution (hash-table)
 
 *)
-module type GenericGlobIncrSolver =
-  functor (S:GlobConstrSys) ->
+module type DemandGlobIncrSolver =
+  functor (S:DemandGlobConstrSys) ->
   functor (LH:Hashtbl.S with type key=S.LVar.t) ->
   functor (GH:Hashtbl.S with type key=S.GVar.t) ->
   sig

src/constraint/translators.ml

@@ -3,13 +3,35 @@ open Batteries
 open ConstrSys
 open SolverTypes
 
+(** Translate a [DemandConstrSys] into a [EqConstrSys] *)
+module EqConstrSysFromDemandConstrSys (S: DemandEqConstrSys)
+  : EqConstrSys   with type v = S.v
+                   and type d = S.d
+                   and module Var = S.Var
+                   and module Dom = S.Dom =
+struct
+  type v = S.v
+  type d = S.d
+  module Var = S.Var
+  module Dom = S.Dom
+
+  let system (x: v) =
+    match S.system x with
+    | None -> None
+    | Some f ->
+      let f' get set = f get set (ignore % get) in
+      Some f'
+
+  let sys_change = S.sys_change
+  let postmortem = S.postmortem
+end
 
-(** Translate a [GlobConstrSys] into a [EqConstrSys] *)
-module EqConstrSysFromGlobConstrSys (S:GlobConstrSys)
-  : EqConstrSys   with type v = Var2(S.LVar)(S.GVar).t
-                   and type d = Lattice.Lift2(S.G)(S.D).t
-                   and module Var = Var2(S.LVar)(S.GVar)
-                   and module Dom = Lattice.Lift2(S.G)(S.D)
+(** Translate a [DemandGlobConstrSys] into a [DemandEqConstrSys] *)
+module EqConstrSysFromGlobConstrSys (S:DemandGlobConstrSys)
+  : DemandEqConstrSys   with type v = Var2(S.LVar)(S.GVar).t
+                         and type d = Lattice.Lift2(S.G)(S.D).t
+                         and module Var = Var2(S.LVar)(S.GVar)
+                         and module Dom = Lattice.Lift2(S.G)(S.D)
 =
 struct
   module Var = Var2(S.LVar)(S.GVar)
@@ -39,8 +61,8 @@ struct
   let l, g = (fun x -> `L x), (fun x -> `G x)
   let lD, gD = (fun x -> `Lifted2 x), (fun x -> `Lifted1 x)
 
-  let conv f get set =
-    f (getL % get % l) (fun x v -> set (l x) (lD v))
+  let conv f get set demand =
+    f (getL % get % l) (fun x v -> set (l x) (lD v)) (fun x -> ignore @@ getL @@ get @@ l x)
       (getG % get % g) (fun x v -> set (g x) (gD v))
     |> lD
 
@@ -57,7 +79,7 @@ struct
 end
 
 (** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *)
-module GlobConstrSolFromEqConstrSolBase (S: GlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) (VH: Hashtbl.S with type key = Var2 (S.LVar) (S.GVar).t) =
+module GlobConstrSolFromEqConstrSolBase (S: DemandGlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) (VH: Hashtbl.S with type key = Var2 (S.LVar) (S.GVar).t) =
 struct
   let split_solution hm =
     let l' = LH.create 113 in
@@ -86,17 +108,25 @@ struct
 end
 
 (** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution. *)
-module GlobConstrSolFromEqConstrSol (S: GlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) =
+module GlobConstrSolFromEqConstrSol (S: DemandGlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) =
 struct
   module S2 = EqConstrSysFromGlobConstrSys (S)
   module VH = Hashtbl.Make (S2.Var)
 
   include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH)
 end
 
-(** Transforms a [GenericEqIncrSolver] into a [GenericGlobIncrSolver]. *)
-module GlobSolverFromEqSolver (Sol:GenericEqIncrSolverBase)
-  = functor (S:GlobConstrSys) ->
+
+module DemandEqIncrSolverFromGenericEqIncrSolver (Sol: GenericEqIncrSolver): DemandEqIncrSolver =
+  functor (Arg: IncrSolverArg) ->
+  functor (S: DemandEqConstrSys) ->
+  functor (H: Hashtbl.S with type key = S.v) ->
+    Sol (Arg) (EqConstrSysFromDemandConstrSys  (S)) (H)
+
+
+(** Transforms a [DemandEqIncrSolver] into a [DemandGlobIncrSolver]. *)
+module GlobSolverFromEqSolver (Sol:DemandEqIncrSolverBase)
+  = functor (S:DemandGlobConstrSys) ->
     functor (LH:Hashtbl.S with type key=S.LVar.t) ->
     functor (GH:Hashtbl.S with type key=S.GVar.t) ->
     struct

src/framework/analyses.ml

@@ -424,7 +424,7 @@ end
 module type SpecSys =
 sig
   module Spec: Spec
-  module EQSys: Goblint_constraint.ConstrSys.GlobConstrSys with module LVar = VarF (Spec.C)
+  module EQSys: Goblint_constraint.ConstrSys.DemandGlobConstrSys with module LVar = VarF (Spec.C)
                                and module GVar = GVarF (Spec.V)
                                and module D = Spec.D
                                and module G = GVarG (Spec.G) (Spec.C)

src/framework/constraints.ml

@@ -15,13 +15,13 @@ sig
 end
 
 
-(** The main point of this file---generating a [GlobConstrSys] from a [Spec]. *)
+(** The main point of this file---generating a [DemandGlobConstrSys] from a [Spec]. *)
 module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment)
   : sig
-    include GlobConstrSys with module LVar = VarF (S.C)
-                           and module GVar = GVarF (S.V)
-                           and module D = S.D
-                           and module G = GVarG (S.G) (S.C)
+    include DemandGlobConstrSys with module LVar = VarF (S.C)
+                                 and module GVar = GVarF (S.V)
+                                 and module D = S.D
+                                 and module G = GVarG (S.G) (S.C)
   end
 =
 struct
@@ -50,7 +50,7 @@ struct
     if !AnalysisState.postsolving then
       sideg (GVar.contexts f) (G.create_contexts (G.CSet.singleton c))
 
-  let common_man var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) man * D.t list ref * (lval option * varinfo * exp list * D.t * bool) list ref =
+  let common_man var edge prev_node pval (getl:lv -> ld) sidel demandl getg sideg : (D.t, S.G.t, S.C.t, S.V.t) man * D.t list ref * (lval option * varinfo * exp list * D.t * bool) list ref =
     let r = ref [] in
     let spawns = ref [] in
     (* now watch this ... *)
@@ -78,7 +78,7 @@ struct
           | fd ->
             let c = S.context man fd d in
             sidel (FunctionEntry fd, c) d;
-            ignore (getl (Function fd, c))
+            demandl (Function fd, c)
           | exception Not_found ->
             (* unknown function *)
             M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname;
@@ -131,13 +131,13 @@ struct
 
   let common_joins man ds splits spawns = common_join man (bigsqcup ds) splits spawns
 
-  let tf_assign var edge prev_node lv e getl sidel getg sideg d =
-    let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
+  let tf_assign var edge prev_node lv e getl sidel demandl getg sideg d =
+    let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
     let d = S.assign man lv e in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
     common_join man d !r !spawns
 
-  let tf_vdecl var edge prev_node v getl sidel getg sideg d =
-    let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
+  let tf_vdecl var edge prev_node v getl sidel demandl getg sideg d =
+    let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
     let d = S.vdecl man v in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
     common_join man d !r !spawns
 
@@ -152,8 +152,8 @@ struct
     let nval = S.sync { man with local = spawning_return } `Return in
     nval
 
-  let tf_ret var edge prev_node ret fd getl sidel getg sideg d =
-    let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
+  let tf_ret var edge prev_node ret fd getl sidel demandl getg sideg d =
+    let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
     let d = (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
       if (CilType.Fundec.equal fd MyCFG.dummy_func ||
           List.mem fd.svar.vname (get_string_list "mainfun")) &&
@@ -163,21 +163,21 @@ struct
     in
     common_join man d !r !spawns
 
-  let tf_entry var edge prev_node fd getl sidel getg sideg d =
+  let tf_entry var edge prev_node fd getl sidel demandl getg sideg d =
     (* Side effect function context here instead of at sidel to FunctionEntry,
        because otherwise context for main functions (entrystates) will be missing or pruned during postsolving. *)
     let c: unit -> S.C.t = snd var |> Obj.obj in
     side_context sideg fd (c ());
-    let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
+    let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
     let d = S.body man fd in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
     common_join man d !r !spawns
 
-  let tf_test var edge prev_node e tv getl sidel getg sideg d =
-    let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
+  let tf_test var edge prev_node e tv getl sidel demandl getg sideg d =
+    let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
     let d = S.branch man e tv in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
     common_join man d !r !spawns
 
-  let tf_normal_call man lv e (f:fundec) args getl sidel getg sideg =
+  let tf_normal_call man lv e (f:fundec) args getl sidel demandl getg sideg =
     let combine (cd, fc, fd) =
       if M.tracing then M.traceli "combine" "local: %a" S.D.pretty cd;
       if M.tracing then M.trace "combine" "function: %a" S.D.pretty fd;
@@ -245,8 +245,8 @@ struct
 
   let tf_special_call man lv f args = S.special man lv f args
 
-  let tf_proc var edge prev_node lv e args getl sidel getg sideg d =
-    let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
+  let tf_proc var edge prev_node lv e args getl sidel demandl getg sideg d =
+    let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
     let functions =
       match e with
       | Lval (Var v, NoOffset) ->
@@ -271,7 +271,7 @@ struct
                 M.info ~category:Analyzer "Using special for defined function %s" f.vname;
                 tf_special_call man lv f args
               | fd ->
-                tf_normal_call man lv e fd args getl sidel getg sideg
+                tf_normal_call man lv e fd args getl sidel demandl getg sideg
               | exception Not_found ->
                 tf_special_call man lv f args)
           end
@@ -292,17 +292,17 @@ struct
     end else
       common_joins man funs !r !spawns
 
-  let tf_asm var edge prev_node getl sidel getg sideg d =
-    let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
+  let tf_asm var edge prev_node getl sidel demandl getg sideg d =
+    let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
     let d = S.asm man in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
     common_join man d !r !spawns
 
-  let tf_skip var edge prev_node getl sidel getg sideg d =
-    let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
+  let tf_skip var edge prev_node getl sidel demandl getg sideg d =
+    let man, r, spawns = common_man var edge prev_node d getl sidel demandl getg sideg in
     let d = S.skip man in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
     common_join man d !r !spawns
 
-  let tf var getl sidel getg sideg prev_node edge d =
+  let tf var getl sidel demandl getg sideg prev_node edge d =
     begin match edge with
       | Assign (lv,rv) -> tf_assign var edge prev_node lv rv
       | VDecl (v)      -> tf_vdecl var edge prev_node v
@@ -312,7 +312,7 @@ struct
       | Test (p,b)     -> tf_test var edge prev_node p b
       | ASM (_, _, _)  -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
       | Skip           -> tf_skip var edge prev_node
-    end getl sidel getg sideg d
+    end getl sidel demandl getg sideg d
 
   type Goblint_backtrace.mark += TfLocation of location
 
@@ -322,7 +322,7 @@ struct
       | _ -> None (* for other marks *)
     )
 
-  let tf var getl sidel getg sideg prev_node (_,edge) d (f,t) =
+  let tf var getl sidel demandl getg sideg prev_node (_,edge) d (f,t) =
     let old_loc  = !Goblint_tracing.current_loc in
     let old_loc2 = !Goblint_tracing.next_loc in
     Goblint_tracing.current_loc := f;
@@ -331,16 +331,16 @@ struct
         Goblint_tracing.current_loc := old_loc;
         Goblint_tracing.next_loc := old_loc2
       ) (fun () ->
-        let d       = tf var getl sidel getg sideg prev_node edge d in
+        let d       = tf var getl sidel demandl getg sideg prev_node edge d in
         d
       )
 
-  let tf (v,c) (edges, u) getl sidel getg sideg =
+  let tf (v,c) (edges, u) getl sidel demandl getg sideg =
     let pval = getl (u,c) in
     let _, locs = List.fold_right (fun (f,e) (t,xs) -> f, (f,t)::xs) edges (Node.location v,[]) in
-    List.fold_left2 (|>) pval (List.map (tf (v,Obj.repr (fun () -> c)) getl sidel getg sideg u) edges) locs
+    List.fold_left2 (|>) pval (List.map (tf (v,Obj.repr (fun () -> c)) getl sidel demandl getg sideg u) edges) locs
 
-  let tf (v,c) (e,u) getl sidel getg sideg =
+  let tf (v,c) (e,u) getl sidel demandl getg sideg =
     let old_node = !current_node in
     let old_fd = Option.map Node.find_fundec old_node |? Cil.dummyFunDec in
     let new_fd = Node.find_fundec v in
@@ -355,7 +355,7 @@ struct
         if not (CilType.Fundec.equal old_fd new_fd) then
           Timing.Program.exit new_fd.svar.vname
       ) (fun () ->
-        let d       = tf (v,c) (e,u) getl sidel getg sideg in
+        let d       = tf (v,c) (e,u) getl sidel demandl getg sideg in
         d
       )
 
@@ -364,8 +364,8 @@ struct
     | FunctionEntry _ ->
       None
     | _ ->
-      let tf getl sidel getg sideg =
-        let tf' eu = tf (v,c) eu getl sidel getg sideg in
+      let tf getl sidel demandl getg sideg =
+        let tf' eu = tf (v,c) eu getl sidel demandl getg sideg in
 
         match NodeH.find_option CfgTools.node_scc_global v with
         | Some scc when NodeH.mem scc.prev v && NodeH.length scc.prev = 1 ->