Skip to content

Commit

Permalink
Extract constraint systems from Constraints module
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Dec 28, 2023
1 parent 0602af0 commit f97869c
Show file tree
Hide file tree
Showing 14 changed files with 218 additions and 223 deletions.
176 changes: 175 additions & 1 deletion src/framework/constrSys.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,4 +122,178 @@ module type GenericGlobSolver =
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
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 -> GoblintCil.Pretty.dprintf "L:%a" LV.pretty_trace a
| `G a -> GoblintCil.Pretty.dprintf "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

let is_write_only = function
| `L a -> LV.is_write_only a
| `G a -> GV.is_write_only a
end


(** Translate a [GlobConstrSys] into a [EqConstrSys] *)
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)

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

let system = function
| `G _ -> None
| `L x -> Option.map conv (S.system x)

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]. *)
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')
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)

include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH)
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
let current_var = ref None

module S =
struct
include S

let system x =
match S.system x with
| None -> None
| Some f ->
let f' get set =
let old_current_var = !current_var in
current_var := Some x;
Fun.protect ~finally:(fun () ->
current_var := old_current_var
) (fun () ->
f get set
)
in
Some f'
end
end
189 changes: 0 additions & 189 deletions src/framework/constraints.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -502,38 +502,6 @@ sig
val increment: increment_data option
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 -> Pretty.dprintf "L:%a" LV.pretty_trace a
| `G a -> Pretty.dprintf "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

let is_write_only = function
| `L a -> LV.is_write_only a
| `G a -> GV.is_write_only a
end

(** The main point of this file---generating a [GlobConstrSys] from a [Spec]. *)
module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment)
Expand Down Expand Up @@ -1054,137 +1022,6 @@ struct
{obsolete; delete; reluctant; restart}
end

(** Convert a non-incremental solver into an "incremental" solver.
It will solve from scratch, perform standard postsolving and have no marshal data. *)
module EqIncrSolverFromEqSolver (Sol: GenericEqSolver): GenericEqIncrSolver =
functor (Arg: IncrSolverArg) (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
struct
module Sol = Sol (S) (VH)
module Post = PostSolver.MakeList (PostSolver.ListArgFromStdArg (S) (VH) (Arg))

type marshal = unit
let copy_marshal () = ()
let relift_marshal () = ()

let solve xs vs _ =
let vh = Sol.solve xs vs in
Post.post xs vs vh;
(vh, ())
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)
=
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)

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

let system = function
| `G _ -> None
| `L x -> Option.map conv (S.system x)

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]. *)
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')
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)

include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH)
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


(** Add path sensitivity to a analysis *)
module PathSensitive2 (Spec:Spec)
Expand Down Expand Up @@ -2057,29 +1894,3 @@ struct
ignore (Pretty.printf "Nodes comparison summary: %t\n" (fun () -> msg));
print_newline ();
end

(** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *)
module CurrentVarEqConstrSys (S: EqConstrSys) =
struct
let current_var = ref None

module S =
struct
include S

let system x =
match S.system x with
| None -> None
| Some f ->
let f' get set =
let old_current_var = !current_var in
current_var := Some x;
Fun.protect ~finally:(fun () ->
current_var := old_current_var
) (fun () ->
f get set
)
in
Some f'
end
end
Loading

0 comments on commit f97869c

Please sign in to comment.