Skip to content

Commit 56fff3c

Browse files
sim642sim642
authored
Merge pull request #1692 from goblint/generic-spec-lifters
Extract generic `Spec` domain and context lifters
2 parents db16544 + 91ca675 commit 56fff3c

File tree

3 files changed

+53
-94
lines changed

3 files changed

+53
-94
lines changed

‎src/domain/lattice.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,7 @@ struct
145145
end
146146

147147
(* HAS SIDE-EFFECTS ---- PLEASE INSTANCIATE ONLY ONCE!!! *)
148-
module HConsed (Base:S) (Arg: sig val assume_idempotent: bool end) =
148+
module HConsed (Arg: sig val assume_idempotent: bool end) (Base:S) =
149149
struct
150150
include Printable.HConsed (Base)
151151

‎src/domain/mapDomain.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -263,7 +263,7 @@ module HConsed (M: S) : S with
263263
type key = M.key and
264264
type value = M.value =
265265
struct
266-
include Lattice.HConsed (M) (struct let assume_idempotent = false end)
266+
include Lattice.HConsed (struct let assume_idempotent = false end) (M)
267267

268268
type key = M.key
269269
type value = M.value

‎src/lifters/specLifters.ml‎

Lines changed: 51 additions & 92 deletions
Original file line numberDiff line numberDiff line change
@@ -5,20 +5,26 @@ open GoblintCil
55
open Analyses
66
open GobConfig
77

8+
module type NameLifter =
9+
sig
10+
val lift_name: string -> string
11+
end
812

9-
(** Lifts a [Spec] so that the domain is [Hashcons]d *)
10-
module HashconsLifter (S:Spec)
13+
module type LatticeLifter =
14+
functor (L: Lattice.S) ->
15+
sig
16+
include Lattice.S
17+
18+
val lift: L.t -> t
19+
val unlift: t -> L.t
20+
end
21+
22+
module DomainLifter (N: NameLifter) (F: LatticeLifter) (S:Spec)
1123
: Spec with module G = S.G
1224
and module C = S.C
1325
=
1426
struct
15-
module HConsedArg =
16-
struct
17-
(* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
18-
(* see https://github.com/goblint/analyzer/issues/1005 *)
19-
let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never"
20-
end
21-
module D = Lattice.HConsed (S.D) (HConsedArg)
27+
module D = F (S.D)
2228
module G = S.G
2329
module C = S.C
2430
module V = S.V
@@ -28,9 +34,9 @@ struct
2834
let of_elt x = of_elt (D.unlift x)
2935
end
3036

31-
let name () = S.name () ^" hashconsed"
37+
let name () = N.lift_name (S.name ())
3238

33-
type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
39+
type marshal = S.marshal
3440
let init = S.init
3541
let finalize = S.finalize
3642

@@ -98,104 +104,50 @@ struct
98104
D.lift @@ S.event (conv man) e (conv oman)
99105
end
100106

101-
(** Lifts a [Spec] so that the context is [Hashcons]d. *)
102-
module HashconsContextLifter (S:Spec)
103-
: Spec with module D = S.D
104-
and module G = S.G
105-
and module C = Printable.HConsed (S.C)
106-
=
107+
(** Lifts a [Spec] so that the domain is [Hashcons]d *)
108+
module HashconsLifter (S: Spec) = (* keep functor eta-expanded to look up option when lifter is actually used *)
107109
struct
108-
module D = S.D
109-
module G = S.G
110-
module C = Printable.HConsed (S.C)
111-
module V = S.V
112-
module P = S.P
113-
114-
let name () = S.name () ^" context hashconsed"
115-
116-
type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
117-
let init = S.init
118-
let finalize = S.finalize
119-
120-
let startstate = S.startstate
121-
let exitstate = S.exitstate
122-
let morphstate = S.morphstate
123-
124-
let conv man =
125-
{ man with context = (fun () -> C.unlift (man.context ())) }
126-
127-
let context man fd = C.lift % S.context (conv man) fd
128-
let startcontext () = C.lift @@ S.startcontext ()
129-
130-
let sync man reason =
131-
S.sync (conv man) reason
132-
133-
let query man (type a) (q: a Queries.t): a Queries.result =
134-
match q with
135-
| Queries.IterPrevVars f ->
136-
let g i (n, c, j) e = f i (n, Obj.repr (C.lift (Obj.obj c)), j) e in
137-
S.query (conv man) (Queries.IterPrevVars g)
138-
| _ -> S.query (conv man) q
139-
140-
let assign man lv e =
141-
S.assign (conv man) lv e
142-
143-
let vdecl man v =
144-
S.vdecl (conv man) v
145-
146-
let branch man e tv =
147-
S.branch (conv man) e tv
148-
149-
let body man f =
150-
S.body (conv man) f
151-
152-
let return man r f =
153-
S.return (conv man) r f
154-
155-
let asm man =
156-
S.asm (conv man)
157-
158-
let skip man =
159-
S.skip (conv man)
160-
161-
let enter man r f args =
162-
S.enter (conv man) r f args
163-
164-
let special man r f args =
165-
S.special (conv man) r f args
110+
module NameLifter =
111+
struct
112+
let lift_name x = x ^ " hashconsed"
113+
end
166114

167-
let combine_env man r fe f args fc es f_ask =
168-
S.combine_env (conv man) r fe f args (Option.map C.unlift fc) es f_ask
115+
module HConsedArg =
116+
struct
117+
(* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
118+
(* see https://github.com/goblint/analyzer/issues/1005 *)
119+
let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never"
120+
end
169121

170-
let combine_assign man r fe f args fc es f_ask =
171-
S.combine_assign (conv man) r fe f args (Option.map C.unlift fc) es f_ask
122+
include DomainLifter (NameLifter) (Lattice.HConsed (HConsedArg)) (S)
172123

173-
let threadenter man ~multiple lval f args =
174-
S.threadenter (conv man) ~multiple lval f args
124+
(* TODO: should marshal hashcons table to avoid relift altogether? *)
125+
end
175126

176-
let threadspawn man ~multiple lval f args fman =
177-
S.threadspawn (conv man) ~multiple lval f args (conv fman)
127+
module type PrintableLifter =
128+
functor (P: Printable.S) ->
129+
sig
130+
include Printable.S
178131

179-
let paths_as_set man = S.paths_as_set (conv man)
180-
let event man e oman = S.event (conv man) e (conv oman)
181-
end
132+
val lift: P.t -> t
133+
val unlift: t -> P.t
134+
end
182135

183-
(** Lifts a [Spec] so that the context is [HashCached]. *)
184-
module HashCachedContextLifter (S:Spec)
136+
module ContextLifter (N: NameLifter) (F: PrintableLifter) (S:Spec)
185137
: Spec with module D = S.D
186138
and module G = S.G
187-
and module C = Printable.HashCached (S.C)
139+
and module C = F (S.C)
188140
=
189141
struct
190142
module D = S.D
191143
module G = S.G
192-
module C = Printable.HashCached (S.C)
144+
module C = F (S.C)
193145
module V = S.V
194146
module P = S.P
195147

196-
let name () = S.name () ^" context hashcached"
148+
let name () = N.lift_name (S.name ())
197149

198-
type marshal = S.marshal
150+
type marshal = S.marshal
199151
let init = S.init
200152
let finalize = S.finalize
201153

@@ -262,6 +214,13 @@ struct
262214
let event man e oman = S.event (conv man) e (conv oman)
263215
end
264216

217+
(** Lifts a [Spec] so that the context is [Hashcons]d. *)
218+
module HashconsContextLifter = ContextLifter (struct let lift_name s = s ^ " context hashconsed" end) (Printable.HConsed)
219+
(* TODO: should marshal hashcons table to avoid relift altogether? *)
220+
221+
(** Lifts a [Spec] so that the context is [HashCached]. *)
222+
module HashCachedContextLifter = ContextLifter (struct let lift_name s = s ^ " context hashcached" end) (Printable.HashCached)
223+
265224
(* see option ana.opt.equal *)
266225
module OptEqual (S: Spec) = struct
267226
module D = struct include S.D let equal x y = x == y || equal x y end

0 commit comments

Comments
 (0)