Merge pull request #1745 from arkocal/demand_constr

Refactor `goblint.constraint` dune library

Author: sim642

scripts/goblint-lib-modules.py

@@ -8,6 +8,7 @@
 
 goblint_lib_paths = [
     src_root_path / "goblint_lib.ml",
+    src_root_path / "constraint" / "goblint_constraint.ml",
     src_root_path / "solver" / "goblint_solver.ml",
     src_root_path / "util" / "std" / "goblint_std.ml",
 ]
@@ -34,6 +35,7 @@
 
     # libraries
     "Goblint_std",
+    "Goblint_constraint",
     "Goblint_solver",
     "Goblint_timing",
     "Goblint_backtrace",

src/analyses/apron/relationPriv.apron.ml

@@ -12,6 +12,8 @@ module Q = Queries
 
 module RelationComponents = RelationDomain.RelComponents
 
+module VarQuery = Goblint_constraint.VarQuery
+
 open CommonPriv
 
 

src/analyses/basePriv.ml

@@ -11,6 +11,8 @@ module VD     = BaseDomain.VD
 module CPA    = BaseDomain.CPA
 module BaseComponents = BaseDomain.BaseComponents
 
+module VarQuery = Goblint_constraint.VarQuery
+
 open CommonPriv
 
 

src/analyses/basePriv.mli

@@ -6,6 +6,8 @@ open GoblintCil
 (* Cannot use local module substitutions because ppx_import is still stuck at 4.07 AST: https://github.com/ocaml-ppx/ppx_import/issues/50#issuecomment-775817579. *)
 (* TODO: try again, because ppx_import is now removed *)
 
+module VarQuery = Goblint_constraint.VarQuery
+
 module type S =
 sig
   module D: Lattice.S

src/analyses/commonPriv.ml

@@ -130,7 +130,7 @@ struct
 
   let iter_sys_vars getg vq vf =
     match vq with
-    | VarQuery.Global g -> vf (V.global g)
+    | Goblint_constraint.VarQuery.Global g -> vf (V.global g)
     | _ -> ()
 end
 

src/constraint/constrSys.ml

@@ -1,4 +1,4 @@
-(** {{!MonSystem} constraint system} signatures. *)
+(** {{!EqConstrSys} constraint system} signatures. *)
 
 open Batteries
 
@@ -21,115 +21,6 @@ sig
   val relift    : t -> t (* needed only for incremental+hashcons to re-hashcons contexts after loading *)
 end
 
-(** Abstract incremental change to constraint system.
-    @param 'v constrain system variable type *)
-type 'v sys_change_info = {
-  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. *)
-module type MonSystem =
-sig
-  type v    (* variables *)
-  type d    (* values    *)
-  type 'a m (* basically a monad carrier *)
-
-  (** Variables must be hashable, comparable, etc.  *)
-  module Var : VarType with type t = v
-
-  (** Values must form a lattice. *)
-  module Dom : Lattice.S with type t = d
-
-  (** The system in functional form. *)
-  val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m
-
-  (** Compute incremental constraint system change from old solution. *)
-  val sys_change: (v -> d) -> v sys_change_info
-
-  (** List of unknowns that should be queried again when the argument unknown has shrunk to bot, to eagerly trigger (analysis-time!) abstract garbage collection idependently of reach-based pruning at the end.
-      @see <https://arxiv.org/abs/2504.06026> Stemmler, F., Schwarz, M., Erhard, J., Tilscher, S., Seidl, H. Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses *)
-  val postmortem: v -> v list
-end
-
-(** Any system of side-effecting equations over lattices. *)
-module type EqConstrSys = MonSystem with type 'a m := 'a option
-
-(** A side-effecting system with globals. *)
-module type GlobConstrSys =
-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) -> (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
-
-(** A solver is something that can translate a system into a solution (hash-table).
-    Incremental solver has data to be marshaled. *)
-module type GenericEqIncrSolverBase =
-  functor (S:EqConstrSys) ->
-  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
-
-(** (Incremental) solver argument, indicating which postsolving should be performed by the solver. *)
-module type IncrSolverArg =
-sig
-  val should_prune: bool
-  val should_verify: bool
-  val should_warn: bool
-  val should_save_run: bool
-end
-
-(** An incremental solver takes the argument about postsolving. *)
-module type GenericEqIncrSolver =
-  functor (Arg: IncrSolverArg) ->
-    GenericEqIncrSolverBase
-
-(** A solver is something that can translate a system into a solution (hash-table) *)
-module type GenericEqSolver =
-  functor (S:EqConstrSys) ->
-  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) *)
-module type GenericGlobSolver =
-  functor (S:GlobConstrSys) ->
-  functor (LH:Hashtbl.S with type key=S.LVar.t) ->
-  functor (GH:Hashtbl.S with type key=S.GVar.t) ->
-  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.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
-
-
 (** 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)
@@ -163,124 +54,52 @@ struct
     | `G a -> GV.is_write_only a
 end
 
+(** Abstract incremental change to constraint system.
+    @param 'v constrain system variable type *)
+type 'v sys_change_info = {
+  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. *)
+}
 
-(** 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)
-=
-struct
-  module Var = Var2(S.LVar)(S.GVar)
-  module Dom =
-  struct
-    include Lattice.Lift2 (S.G) (S.D)
-    let printXml f = function
-      | `Lifted1 a -> S.G.printXml f a
-      | `Lifted2 a -> S.D.printXml f a
-      | (`Bot | `Top) as x -> printXml f x
-  end
-  type v = Var.t
-  type d = Dom.t
-
-  let getG = function
-    | `Lifted1 x -> x
-    | `Bot -> S.G.bot ()
-    | `Top -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has top value"
-    | `Lifted2 _ -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has local value"
-
-  let getL = function
-    | `Lifted2 x -> x
-    | `Bot -> S.D.bot ()
-    | `Top -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has top value"
-    | `Lifted1 _ -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has global value"
-
-  let l, g = (fun x -> `L x), (fun x -> `G x)
-  let lD, gD = (fun x -> `Lifted2 x), (fun x -> `Lifted1 x)
+(** A side-effecting system. *)
+module type EqConstrSys =
+sig
+  type v    (* variables *)
+  type d    (* values    *)
 
-  let conv f get set =
-    f (getL % get % l) (fun x v -> set (l x) (lD v))
-      (getG % get % g) (fun x v -> set (g x) (gD v))
-    |> lD
+  (** Variables must be hashable, comparable, etc.  *)
+  module Var : VarType with type t = v
 
-  let system = function
-    | `G _ -> None
-    | `L x -> Option.map conv (S.system x)
+  (** Values must form a lattice. *)
+  module Dom : Lattice.S with type t = d
 
-  let sys_change get =
-    S.sys_change (getL % get % l) (getG % get % g)
+  (** The system in functional form. *)
+  val system : v -> ((v -> d) -> (v -> d -> unit) -> d) option
 
-  let postmortem = function
-    | `L g -> List.map (fun x -> `L x) @@ S.postmortem g
-    | _ -> []
-end
+  (** Compute incremental constraint system change from old solution. *)
+  val sys_change: (v -> d) -> v sys_change_info
 
-(** 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) =
-struct
-  let split_solution hm =
-    let l' = LH.create 113 in
-    let g' = GH.create 113 in
-    let split_vars x d = match x with
-      | `L x ->
-        begin match d with
-          | `Lifted2 d -> LH.replace l' x d
-          (* | `Bot -> () *)
-          (* Since Verify2 is broken and only checks existing keys, add it with local bottom value.
-             This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *)
-          | `Bot -> LH.replace l' x (S.D.bot ())
-          | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has top value"
-          | `Lifted1 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has global value"
-        end
-      | `G x ->
-        begin match d with
-          | `Lifted1 d -> GH.replace g' x d
-          | `Bot -> ()
-          | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has top value"
-          | `Lifted2 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has local value"
-        end
-    in
-    VH.iter split_vars hm;
-    (l', g')
+  (** List of unknowns that should be queried again when the argument unknown has shrunk to bot, to eagerly trigger (analysis-time!) abstract garbage collection idependently of reach-based pruning at the end.
+      @see <https://arxiv.org/abs/2504.06026> Stemmler, F., Schwarz, M., Erhard, J., Tilscher, S., Seidl, H. Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses *)
+  val postmortem: v -> v list
 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) =
-struct
-  module S2 = EqConstrSysFromGlobConstrSys (S)
-  module VH = Hashtbl.Make (S2.Var)
+(** A side-effecting system with globals. *)
+module type GlobConstrSys =
+sig
+  module LVar : VarType
+  module GVar : VarType
 
-  include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH)
+  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
+  val postmortem: LVar.t -> LVar.t list
 end
 
-(** Transforms a [GenericEqIncrSolver] into a [GenericGlobSolver]. *)
-module GlobSolverFromEqSolver (Sol:GenericEqIncrSolverBase)
-  = functor (S:GlobConstrSys) ->
-    functor (LH:Hashtbl.S with type key=S.LVar.t) ->
-    functor (GH:Hashtbl.S with type key=S.GVar.t) ->
-    struct
-      module EqSys = EqConstrSysFromGlobConstrSys (S)
-
-      module VH : Hashtbl.S with type key=EqSys.v = Hashtbl.Make(EqSys.Var)
-      module Sol' = Sol (EqSys) (VH)
-
-      module Splitter = GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH) (* reuse EqSys and VH *)
-
-      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
-        let sv = List.map (fun x -> `L x) l in
-        let hm, solver_data = Sol'.solve vs sv old_data in
-        Splitter.split_solution hm, solver_data
-    end
-
-
 (** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *)
 module CurrentVarEqConstrSys (S: EqConstrSys) =
 struct

src/constraint/constraint.mld

@@ -3,7 +3,6 @@
 (library
  (name goblint_constraint)
  (public_name goblint.constraint)
- (wrapped false) ; TODO: wrap
  (libraries
    batteries.unthreaded
    goblint_std
@@ -17,5 +16,3 @@
     ppx_deriving_hash
     ppx_deriving_yojson))
  (instrumentation (backend bisect_ppx)))
-
-(documentation)

src/constraint/dune

@@ -0,0 +1,15 @@
+(** (Side-effecting) constraint systems. *)
+
+(** {1 Specification} *)
+
+module ConstrSys = ConstrSys
+module SolverTypes = SolverTypes
+
+(** {2 Utilities} *)
+
+module Translators = Translators
+
+
+(** {1 Results} *)
+
+module VarQuery = VarQuery