Skip to content

Commit f97869c

Browse files
sim642sim642
committed
Extract constraint systems from Constraints module
1 parent 0602af0 commit f97869c

File tree

14 files changed

+218
-223
lines changed

14 files changed

+218
-223
lines changed

‎src/framework/constrSys.ml‎

Lines changed: 175 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,4 +122,178 @@ module type GenericGlobSolver =
122122
reached from starting values [xs].
123123
As a second component the solver returns data structures for incremental serialization. *)
124124
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
125-
end
125+
end
126+
127+
128+
(** Combined variables so that we can also use the more common [EqConstrSys]
129+
that uses only one kind of a variable. *)
130+
module Var2 (LV:VarType) (GV:VarType)
131+
: VarType
132+
with type t = [ `L of LV.t | `G of GV.t ]
133+
=
134+
struct
135+
type t = [ `L of LV.t | `G of GV.t ] [@@deriving eq, ord, hash]
136+
let relift = function
137+
| `L x -> `L (LV.relift x)
138+
| `G x -> `G (GV.relift x)
139+
140+
let pretty_trace () = function
141+
| `L a -> GoblintCil.Pretty.dprintf "L:%a" LV.pretty_trace a
142+
| `G a -> GoblintCil.Pretty.dprintf "G:%a" GV.pretty_trace a
143+
144+
let printXml f = function
145+
| `L a -> LV.printXml f a
146+
| `G a -> GV.printXml f a
147+
148+
let var_id = function
149+
| `L a -> LV.var_id a
150+
| `G a -> GV.var_id a
151+
152+
let node = function
153+
| `L a -> LV.node a
154+
| `G a -> GV.node a
155+
156+
let is_write_only = function
157+
| `L a -> LV.is_write_only a
158+
| `G a -> GV.is_write_only a
159+
end
160+
161+
162+
(** Translate a [GlobConstrSys] into a [EqConstrSys] *)
163+
module EqConstrSysFromGlobConstrSys (S:GlobConstrSys)
164+
: EqConstrSys with type v = Var2(S.LVar)(S.GVar).t
165+
and type d = Lattice.Lift2(S.G)(S.D).t
166+
and module Var = Var2(S.LVar)(S.GVar)
167+
and module Dom = Lattice.Lift2(S.G)(S.D)
168+
=
169+
struct
170+
module Var = Var2(S.LVar)(S.GVar)
171+
module Dom =
172+
struct
173+
include Lattice.Lift2 (S.G) (S.D)
174+
let printXml f = function
175+
| `Lifted1 a -> S.G.printXml f a
176+
| `Lifted2 a -> S.D.printXml f a
177+
| (`Bot | `Top) as x -> printXml f x
178+
end
179+
type v = Var.t
180+
type d = Dom.t
181+
182+
let getG = function
183+
| `Lifted1 x -> x
184+
| `Bot -> S.G.bot ()
185+
| `Top -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has top value"
186+
| `Lifted2 _ -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has local value"
187+
188+
let getL = function
189+
| `Lifted2 x -> x
190+
| `Bot -> S.D.bot ()
191+
| `Top -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has top value"
192+
| `Lifted1 _ -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has global value"
193+
194+
let l, g = (fun x -> `L x), (fun x -> `G x)
195+
let lD, gD = (fun x -> `Lifted2 x), (fun x -> `Lifted1 x)
196+
197+
let conv f get set =
198+
f (getL % get % l) (fun x v -> set (l x) (lD v))
199+
(getG % get % g) (fun x v -> set (g x) (gD v))
200+
|> lD
201+
202+
let system = function
203+
| `G _ -> None
204+
| `L x -> Option.map conv (S.system x)
205+
206+
let sys_change get =
207+
S.sys_change (getL % get % l) (getG % get % g)
208+
end
209+
210+
(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *)
211+
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) =
212+
struct
213+
let split_solution hm =
214+
let l' = LH.create 113 in
215+
let g' = GH.create 113 in
216+
let split_vars x d = match x with
217+
| `L x ->
218+
begin match d with
219+
| `Lifted2 d -> LH.replace l' x d
220+
(* | `Bot -> () *)
221+
(* Since Verify2 is broken and only checks existing keys, add it with local bottom value.
222+
This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *)
223+
| `Bot -> LH.replace l' x (S.D.bot ())
224+
| `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has top value"
225+
| `Lifted1 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has global value"
226+
end
227+
| `G x ->
228+
begin match d with
229+
| `Lifted1 d -> GH.replace g' x d
230+
| `Bot -> ()
231+
| `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has top value"
232+
| `Lifted2 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has local value"
233+
end
234+
in
235+
VH.iter split_vars hm;
236+
(l', g')
237+
end
238+
239+
(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution. *)
240+
module GlobConstrSolFromEqConstrSol (S: GlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) =
241+
struct
242+
module S2 = EqConstrSysFromGlobConstrSys (S)
243+
module VH = Hashtbl.Make (S2.Var)
244+
245+
include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH)
246+
end
247+
248+
(** Transforms a [GenericEqIncrSolver] into a [GenericGlobSolver]. *)
249+
module GlobSolverFromEqSolver (Sol:GenericEqIncrSolverBase)
250+
= functor (S:GlobConstrSys) ->
251+
functor (LH:Hashtbl.S with type key=S.LVar.t) ->
252+
functor (GH:Hashtbl.S with type key=S.GVar.t) ->
253+
struct
254+
module EqSys = EqConstrSysFromGlobConstrSys (S)
255+
256+
module VH : Hashtbl.S with type key=EqSys.v = Hashtbl.Make(EqSys.Var)
257+
module Sol' = Sol (EqSys) (VH)
258+
259+
module Splitter = GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH) (* reuse EqSys and VH *)
260+
261+
type marshal = Sol'.marshal
262+
263+
let copy_marshal = Sol'.copy_marshal
264+
let relift_marshal = Sol'.relift_marshal
265+
266+
let solve ls gs l old_data =
267+
let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls
268+
@ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in
269+
let sv = List.map (fun x -> `L x) l in
270+
let hm, solver_data = Sol'.solve vs sv old_data in
271+
Splitter.split_solution hm, solver_data
272+
end
273+
274+
275+
(** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *)
276+
module CurrentVarEqConstrSys (S: EqConstrSys) =
277+
struct
278+
let current_var = ref None
279+
280+
module S =
281+
struct
282+
include S
283+
284+
let system x =
285+
match S.system x with
286+
| None -> None
287+
| Some f ->
288+
let f' get set =
289+
let old_current_var = !current_var in
290+
current_var := Some x;
291+
Fun.protect ~finally:(fun () ->
292+
current_var := old_current_var
293+
) (fun () ->
294+
f get set
295+
)
296+
in
297+
Some f'
298+
end
299+
end

‎src/framework/constraints.ml‎

Lines changed: 0 additions & 189 deletions
Original file line numberDiff line numberDiff line change
@@ -502,38 +502,6 @@ sig
502502
val increment: increment_data option
503503
end
504504

505-
(** Combined variables so that we can also use the more common [EqConstrSys]
506-
that uses only one kind of a variable. *)
507-
module Var2 (LV:VarType) (GV:VarType)
508-
: VarType
509-
with type t = [ `L of LV.t | `G of GV.t ]
510-
=
511-
struct
512-
type t = [ `L of LV.t | `G of GV.t ] [@@deriving eq, ord, hash]
513-
let relift = function
514-
| `L x -> `L (LV.relift x)
515-
| `G x -> `G (GV.relift x)
516-
517-
let pretty_trace () = function
518-
| `L a -> Pretty.dprintf "L:%a" LV.pretty_trace a
519-
| `G a -> Pretty.dprintf "G:%a" GV.pretty_trace a
520-
521-
let printXml f = function
522-
| `L a -> LV.printXml f a
523-
| `G a -> GV.printXml f a
524-
525-
let var_id = function
526-
| `L a -> LV.var_id a
527-
| `G a -> GV.var_id a
528-
529-
let node = function
530-
| `L a -> LV.node a
531-
| `G a -> GV.node a
532-
533-
let is_write_only = function
534-
| `L a -> LV.is_write_only a
535-
| `G a -> GV.is_write_only a
536-
end
537505

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

1057-
(** Convert a non-incremental solver into an "incremental" solver.
1058-
It will solve from scratch, perform standard postsolving and have no marshal data. *)
1059-
module EqIncrSolverFromEqSolver (Sol: GenericEqSolver): GenericEqIncrSolver =
1060-
functor (Arg: IncrSolverArg) (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
1061-
struct
1062-
module Sol = Sol (S) (VH)
1063-
module Post = PostSolver.MakeList (PostSolver.ListArgFromStdArg (S) (VH) (Arg))
1064-
1065-
type marshal = unit
1066-
let copy_marshal () = ()
1067-
let relift_marshal () = ()
1068-
1069-
let solve xs vs _ =
1070-
let vh = Sol.solve xs vs in
1071-
Post.post xs vs vh;
1072-
(vh, ())
1073-
end
1074-
1075-
1076-
(** Translate a [GlobConstrSys] into a [EqConstrSys] *)
1077-
module EqConstrSysFromGlobConstrSys (S:GlobConstrSys)
1078-
: EqConstrSys with type v = Var2(S.LVar)(S.GVar).t
1079-
and type d = Lattice.Lift2(S.G)(S.D).t
1080-
and module Var = Var2(S.LVar)(S.GVar)
1081-
and module Dom = Lattice.Lift2(S.G)(S.D)
1082-
=
1083-
struct
1084-
module Var = Var2(S.LVar)(S.GVar)
1085-
module Dom =
1086-
struct
1087-
include Lattice.Lift2 (S.G) (S.D)
1088-
let printXml f = function
1089-
| `Lifted1 a -> S.G.printXml f a
1090-
| `Lifted2 a -> S.D.printXml f a
1091-
| (`Bot | `Top) as x -> printXml f x
1092-
end
1093-
type v = Var.t
1094-
type d = Dom.t
1095-
1096-
let getG = function
1097-
| `Lifted1 x -> x
1098-
| `Bot -> S.G.bot ()
1099-
| `Top -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has top value"
1100-
| `Lifted2 _ -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has local value"
1101-
1102-
let getL = function
1103-
| `Lifted2 x -> x
1104-
| `Bot -> S.D.bot ()
1105-
| `Top -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has top value"
1106-
| `Lifted1 _ -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has global value"
1107-
1108-
let l, g = (fun x -> `L x), (fun x -> `G x)
1109-
let lD, gD = (fun x -> `Lifted2 x), (fun x -> `Lifted1 x)
1110-
1111-
let conv f get set =
1112-
f (getL % get % l) (fun x v -> set (l x) (lD v))
1113-
(getG % get % g) (fun x v -> set (g x) (gD v))
1114-
|> lD
1115-
1116-
let system = function
1117-
| `G _ -> None
1118-
| `L x -> Option.map conv (S.system x)
1119-
1120-
let sys_change get =
1121-
S.sys_change (getL % get % l) (getG % get % g)
1122-
end
1123-
1124-
(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *)
1125-
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) =
1126-
struct
1127-
let split_solution hm =
1128-
let l' = LH.create 113 in
1129-
let g' = GH.create 113 in
1130-
let split_vars x d = match x with
1131-
| `L x ->
1132-
begin match d with
1133-
| `Lifted2 d -> LH.replace l' x d
1134-
(* | `Bot -> () *)
1135-
(* Since Verify2 is broken and only checks existing keys, add it with local bottom value.
1136-
This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *)
1137-
| `Bot -> LH.replace l' x (S.D.bot ())
1138-
| `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has top value"
1139-
| `Lifted1 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has global value"
1140-
end
1141-
| `G x ->
1142-
begin match d with
1143-
| `Lifted1 d -> GH.replace g' x d
1144-
| `Bot -> ()
1145-
| `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has top value"
1146-
| `Lifted2 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has local value"
1147-
end
1148-
in
1149-
VH.iter split_vars hm;
1150-
(l', g')
1151-
end
1152-
1153-
(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution. *)
1154-
module GlobConstrSolFromEqConstrSol (S: GlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) =
1155-
struct
1156-
module S2 = EqConstrSysFromGlobConstrSys (S)
1157-
module VH = Hashtbl.Make (S2.Var)
1158-
1159-
include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH)
1160-
end
1161-
1162-
(** Transforms a [GenericEqIncrSolver] into a [GenericGlobSolver]. *)
1163-
module GlobSolverFromEqSolver (Sol:GenericEqIncrSolverBase)
1164-
= functor (S:GlobConstrSys) ->
1165-
functor (LH:Hashtbl.S with type key=S.LVar.t) ->
1166-
functor (GH:Hashtbl.S with type key=S.GVar.t) ->
1167-
struct
1168-
module EqSys = EqConstrSysFromGlobConstrSys (S)
1169-
1170-
module VH : Hashtbl.S with type key=EqSys.v = Hashtbl.Make(EqSys.Var)
1171-
module Sol' = Sol (EqSys) (VH)
1172-
1173-
module Splitter = GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH) (* reuse EqSys and VH *)
1174-
1175-
type marshal = Sol'.marshal
1176-
1177-
let copy_marshal = Sol'.copy_marshal
1178-
let relift_marshal = Sol'.relift_marshal
1179-
1180-
let solve ls gs l old_data =
1181-
let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls
1182-
@ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in
1183-
let sv = List.map (fun x -> `L x) l in
1184-
let hm, solver_data = Sol'.solve vs sv old_data in
1185-
Splitter.split_solution hm, solver_data
1186-
end
1187-
11881025

11891026
(** Add path sensitivity to a analysis *)
11901027
module PathSensitive2 (Spec:Spec)
@@ -2057,29 +1894,3 @@ struct
20571894
ignore (Pretty.printf "Nodes comparison summary: %t\n" (fun () -> msg));
20581895
print_newline ();
20591896
end
2060-
2061-
(** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *)
2062-
module CurrentVarEqConstrSys (S: EqConstrSys) =
2063-
struct
2064-
let current_var = ref None
2065-
2066-
module S =
2067-
struct
2068-
include S
2069-
2070-
let system x =
2071-
match S.system x with
2072-
| None -> None
2073-
| Some f ->
2074-
let f' get set =
2075-
let old_current_var = !current_var in
2076-
current_var := Some x;
2077-
Fun.protect ~finally:(fun () ->
2078-
current_var := old_current_var
2079-
) (fun () ->
2080-
f get set
2081-
)
2082-
in
2083-
Some f'
2084-
end
2085-
end

0 commit comments

Comments
 (0)