Skip to content

Commit 4882dd3

Browse files
sim642sim642
authored
Merge pull request #1731 from goblint/delay-widening-cleanup
Use generic `Spec` lifters for delayed widening
2 parents 841fb4f + 32fc632 commit 4882dd3

File tree

2 files changed

+119
-116
lines changed

2 files changed

+119
-116
lines changed

‎src/lifters/specLifters.ml‎

Lines changed: 99 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,14 @@ module type LatticeLifter =
1919
val unlift: t -> L.t
2020
end
2121

22-
module DomainLifter (N: NameLifter) (F: LatticeLifter) (S:Spec)
23-
: Spec with module G = S.G
24-
and module C = S.C
22+
module DomainLifter (N: NameLifter) (F: LatticeLifter) (S:Spec):
23+
sig
24+
include Spec with module G = S.G
25+
and module C = S.C
26+
and module D = F (S.D)
27+
and module V = S.V
28+
val conv: (D.t, G.t, C.t, V.t) man -> (S.D.t, G.t, C.t, V.t) man
29+
end
2530
=
2631
struct
2732
module D = F (S.D)
@@ -104,6 +109,89 @@ struct
104109
D.lift @@ S.event (conv man) e (conv oman)
105110
end
106111

112+
module GlobalDomainLifter (N: NameLifter) (F: LatticeLifter) (S:Spec):
113+
sig
114+
include Spec with module D = S.D
115+
and module G = F (S.G)
116+
and module C = S.C
117+
and module V = S.V
118+
val conv: (D.t, G.t, C.t, V.t) man -> (D.t, S.G.t, C.t, V.t) man
119+
end
120+
=
121+
struct
122+
module D = S.D
123+
module G = F (S.G)
124+
module C = S.C
125+
module V = S.V
126+
module P = S.P
127+
128+
let name () = N.lift_name (S.name ())
129+
130+
type marshal = S.marshal
131+
let init = S.init
132+
let finalize = S.finalize
133+
134+
let startstate = S.startstate
135+
let exitstate = S.exitstate
136+
let morphstate = S.morphstate
137+
138+
let conv man =
139+
{ man with global = (fun v -> G.unlift (man.global v))
140+
; sideg = (fun v g -> man.sideg v (G.lift g))
141+
}
142+
143+
let context man fd = S.context (conv man) fd
144+
let startcontext () = S.startcontext ()
145+
146+
let sync man reason =
147+
S.sync (conv man) reason
148+
149+
let query man =
150+
S.query (conv man)
151+
152+
let assign man lv e =
153+
S.assign (conv man) lv e
154+
155+
let vdecl man v =
156+
S.vdecl (conv man) v
157+
158+
let branch man e tv =
159+
S.branch (conv man) e tv
160+
161+
let body man f =
162+
S.body (conv man) f
163+
164+
let return man r f =
165+
S.return (conv man) r f
166+
167+
let asm man =
168+
S.asm (conv man)
169+
170+
let skip man =
171+
S.skip (conv man)
172+
173+
let enter man r f args =
174+
S.enter (conv man) r f args
175+
176+
let special man r f args =
177+
S.special (conv man) r f args
178+
179+
let combine_env man r fe f args fc es f_ask =
180+
S.combine_env (conv man) r fe f args fc es f_ask
181+
182+
let combine_assign man r fe f args fc es f_ask =
183+
S.combine_assign (conv man) r fe f args fc es f_ask
184+
185+
let threadenter man ~multiple lval f args =
186+
S.threadenter (conv man) ~multiple lval f args
187+
188+
let threadspawn man ~multiple lval f args fman =
189+
S.threadspawn (conv man) ~multiple lval f args (conv fman)
190+
191+
let paths_as_set man = S.paths_as_set (conv man)
192+
let event man e oman = S.event (conv man) e (conv oman)
193+
end
194+
107195
(** Lifts a [Spec] so that the domain is [Hashcons]d *)
108196
module HashconsLifter (S: Spec) = (* keep functor eta-expanded to look up option when lifter is actually used *)
109197
struct
@@ -133,10 +221,14 @@ module type PrintableLifter =
133221
val unlift: t -> P.t
134222
end
135223

136-
module ContextLifter (N: NameLifter) (F: PrintableLifter) (S:Spec)
137-
: Spec with module D = S.D
138-
and module G = S.G
139-
and module C = F (S.C)
224+
module ContextLifter (N: NameLifter) (F: PrintableLifter) (S:Spec):
225+
sig
226+
include Spec with module D = S.D
227+
and module G = S.G
228+
and module C = F (S.C)
229+
and module V = S.V
230+
val conv: (D.t, G.t, C.t, V.t) man -> (D.t, G.t, S.C.t, V.t) man
231+
end
140232
=
141233
struct
142234
module D = S.D

‎src/lifters/wideningDelay.ml‎

Lines changed: 20 additions & 109 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,9 @@ struct
2424
module Chain = Printable.Chain (ChainParams)
2525
include Printable.Prod (Base) (Chain)
2626

27+
let lift d = (d, 0)
28+
let unlift (d, _) = d
29+
2730
let bot () = (Base.bot (), 0)
2831
let is_bot (b, _) = Base.is_bot b
2932
let top () = (Base.top (), ChainParams.n ())
@@ -52,134 +55,42 @@ end
5255
All transfer functions reset the counter to 0, so counting only happens between old and new values at a local unknown. *)
5356
module DLifter (S: Spec): Spec =
5457
struct
55-
module D =
58+
module DD (D: Lattice.S) =
5659
struct
57-
include Dom (S.D) (LocalChainParams)
60+
include Dom (D) (LocalChainParams)
5861

5962
let printXml f (b, i) =
60-
BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" S.D.printXml b Chain.printXml i
63+
BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" D.printXml b Chain.printXml i
6164
end
62-
module G = S.G
63-
module C = S.C
64-
module V = S.V
65-
module P =
65+
66+
module NameLifter =
6667
struct
67-
include S.P
68-
let of_elt (x, _) = of_elt x
68+
let lift_name x = x ^ " with widening delay"
6969
end
70+
include SpecLifters.DomainLifter (NameLifter) (DD) (S)
7071

71-
let name () = S.name () ^ " with widening delay"
72-
73-
type marshal = S.marshal
74-
let init = S.init
75-
let finalize = S.finalize
72+
(* Redefine morphstate and paths_as_set to keep counter instead of resetting to 0. *)
7673

77-
let startstate v = (S.startstate v, 0)
78-
let exitstate v = (S.exitstate v, 0)
7974
let morphstate v (d, l) = (S.morphstate v d, l)
8075

81-
let conv (man: (D.t, G.t, C.t, V.t) man): (S.D.t, S.G.t, S.C.t, S.V.t) man =
82-
{ man with local = fst man.local
83-
; split = (fun d es -> man.split (d, 0) es)
84-
}
85-
86-
let context man fd (d, _) = S.context (conv man) fd d
87-
let startcontext () = S.startcontext ()
88-
89-
let lift_fun man f g h =
90-
f @@ h (g (conv man))
91-
92-
let lift d = (d, 0)
93-
94-
let sync man reason = lift_fun man lift S.sync ((|>) reason)
95-
let query man (type a) (q: a Queries.t): a Queries.result = S.query (conv man) q
96-
let assign man lv e = lift_fun man lift S.assign ((|>) e % (|>) lv)
97-
let vdecl man v = lift_fun man lift S.vdecl ((|>) v)
98-
let branch man e tv = lift_fun man lift S.branch ((|>) tv % (|>) e)
99-
let body man f = lift_fun man lift S.body ((|>) f)
100-
let return man r f = lift_fun man lift S.return ((|>) f % (|>) r)
101-
let asm man = lift_fun man lift S.asm identity
102-
let skip man = lift_fun man lift S.skip identity
103-
let special man r f args = lift_fun man lift S.special ((|>) args % (|>) f % (|>) r)
104-
105-
let enter man r f args =
106-
let liftmap = List.map (Tuple2.mapn lift) in
107-
lift_fun man liftmap S.enter ((|>) args % (|>) f % (|>) r)
108-
let combine_env man r fe f args fc es f_ask = lift_fun man lift S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
109-
let combine_assign man r fe f args fc es f_ask = lift_fun man lift S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
110-
111-
let threadenter man ~multiple lval f args = lift_fun man (List.map lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
112-
let threadspawn man ~multiple lval f args fman = lift_fun man lift (S.threadspawn ~multiple) ((|>) (conv fman) % (|>) args % (|>) f % (|>) lval)
113-
11476
let paths_as_set man =
115-
let liftmap = List.map (fun x -> (x, snd man.local)) in
116-
lift_fun man liftmap S.paths_as_set Fun.id
117-
118-
let event man e oman =
119-
lift_fun man lift S.event ((|>) (conv oman) % (|>) e)
77+
List.map (fun x -> (x, snd man.local)) @@ S.paths_as_set (conv man)
12078
end
12179

12280
(** Lift {!S} to use widening delay for global unknowns. *)
12381
module GLifter (S: Spec): Spec =
12482
struct
125-
module D = S.D
126-
module G =
83+
module GG (G: Lattice.S) =
12784
struct
128-
include Dom (S.G) (GlobalChainParams)
85+
include Dom (G) (GlobalChainParams)
12986

13087
let printXml f (b, i) =
131-
BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" S.G.printXml b Chain.printXml i
88+
BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" G.printXml b Chain.printXml i
13289
end
133-
module C = S.C
134-
module V = S.V
135-
module P = S.P
136-
137-
let name () = S.name () ^ " with widening delay"
138-
139-
type marshal = S.marshal
140-
let init = S.init
141-
let finalize = S.finalize
14290

143-
let startstate v = S.startstate v
144-
let exitstate v = S.exitstate v
145-
let morphstate v d = S.morphstate v d
146-
147-
let conv (man: (D.t, G.t, C.t, V.t) man): (S.D.t, S.G.t, S.C.t, S.V.t) man =
148-
{ man with global = (fun v -> fst (man.global v))
149-
; sideg = (fun v g -> man.sideg v (g, 0))
150-
}
151-
152-
let context man fd d = S.context (conv man) fd d
153-
let startcontext () = S.startcontext ()
154-
155-
let lift_fun man f g h =
156-
f @@ h (g (conv man))
157-
158-
let lift d = d
159-
160-
let sync man reason = lift_fun man lift S.sync ((|>) reason)
161-
let query man (type a) (q: a Queries.t): a Queries.result = S.query (conv man) q
162-
let assign man lv e = lift_fun man lift S.assign ((|>) e % (|>) lv)
163-
let vdecl man v = lift_fun man lift S.vdecl ((|>) v)
164-
let branch man e tv = lift_fun man lift S.branch ((|>) tv % (|>) e)
165-
let body man f = lift_fun man lift S.body ((|>) f)
166-
let return man r f = lift_fun man lift S.return ((|>) f % (|>) r)
167-
let asm man = lift_fun man lift S.asm identity
168-
let skip man = lift_fun man lift S.skip identity
169-
let special man r f args = lift_fun man lift S.special ((|>) args % (|>) f % (|>) r)
170-
171-
let enter man r f args =
172-
let liftmap = List.map (Tuple2.mapn lift) in
173-
lift_fun man liftmap S.enter ((|>) args % (|>) f % (|>) r)
174-
let combine_env man r fe f args fc es f_ask = lift_fun man lift S.combine_env (fun p -> p r fe f args fc es f_ask)
175-
let combine_assign man r fe f args fc es f_ask = lift_fun man lift S.combine_assign (fun p -> p r fe f args fc es f_ask)
176-
177-
let threadenter man ~multiple lval f args = lift_fun man (List.map lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
178-
let threadspawn man ~multiple lval f args fman = lift_fun man lift (S.threadspawn ~multiple) ((|>) (conv fman) % (|>) args % (|>) f % (|>) lval)
179-
180-
let paths_as_set man =
181-
lift_fun man Fun.id S.paths_as_set Fun.id
182-
183-
let event man e oman =
184-
lift_fun man lift S.event ((|>) (conv oman) % (|>) e)
91+
module NameLifter =
92+
struct
93+
let lift_name x = x ^ " with widening delay"
94+
end
95+
include SpecLifters.GlobalDomainLifter (NameLifter) (GG) (S)
18596
end

0 commit comments

Comments
 (0)