Skip to content

Commit f482630

Browse files
sim642sim642
committed
Implement ana.apron.invariant.diff-box directly in domain
This should be faster, because it doesn't require box domain analysis in parallel. The domain is converted to box and back only during invariant generation. It's also more precise in some sense because it can exclude box-like constraints, which cannot be inferred by box alone. But maybe that's also a downside because it can exclude constraints, which still need the more precise domain.
1 parent 6f7c881 commit f482630

File tree

5 files changed

+123
-105
lines changed

5 files changed

+123
-105
lines changed

‎src/analyses/apron/apronAnalysis.apron.ml‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,6 @@ let spec_module: (module MCPSpec) Lazy.t =
88
lazy (
99
let module Man = (val ApronDomain.get_manager ()) in
1010
let module AD = ApronDomain.D2 (Man) in
11-
let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in
12-
let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in
1311
let module Priv = (val RelationPriv.get_priv ()) in
1412
let module Spec =
1513
struct

‎src/cdomains/apron/apronDomain.apron.ml‎

Lines changed: 29 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -544,17 +544,37 @@ struct
544544
d
545545
end
546546

547-
let invariant x =
547+
(** Keep only box-representable constraints.
548+
Used for [diff-box] in {!invariant}. *)
549+
let boxify d =
550+
let {box1_env; interval_array}: A.box1 = A.to_box Man.mgr d in
551+
let ivs, fvs = Environment.vars box1_env in
552+
assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
553+
A.of_box Man.mgr box1_env ivs interval_array
554+
555+
let to_lincons_set d =
556+
Lincons1Set.of_earray (A.to_lincons_array Man.mgr d)
557+
558+
let invariant d =
548559
(* Would like to minimize to get rid of multi-var constraints directly derived from one-var constraints,
549560
but not implemented in Apron at all: https://github.com/antoinemine/apron/issues/44 *)
550-
(* let x = A.copy Man.mgr x in
551-
A.minimize Man.mgr x; *)
552-
let {lincons0_array; array_env}: Lincons1.earray = A.to_lincons_array Man.mgr x in
553-
Array.to_seq lincons0_array
554-
|> Seq.map (fun (lincons0: Lincons0.t) -> Lincons1.{lincons0; env = array_env})
555-
|> Lincons1Set.of_seq
561+
(* let d = A.copy Man.mgr d in
562+
A.minimize Man.mgr d; *)
563+
let lcd = to_lincons_set d in
564+
if GobConfig.get_bool "ana.apron.invariant.diff-box" then (
565+
(* diff via lincons *)
566+
(* TODO: is there benefit to also Lincons1Set.simplify before diff? might make a difference if y=0 is represented as y>=0 && y<=0 or not *)
567+
let b = boxify d in (* convert back to same Apron domain (instead of box) to make lincons use the same format (e.g. oct doesn't return equalities, but box does) *)
568+
let lcb = to_lincons_set b in
569+
Lincons1Set.diff lcd lcb
570+
)
571+
else
572+
lcd
573+
574+
let invariant d =
575+
invariant d
556576
|> (if Oct.manager_is_oct Man.mgr then Lincons1Set.simplify else Fun.id)
557-
|> Lincons1Set.elements
577+
|> Lincons1Set.elements (* TODO: remove list conversion? *)
558578
end
559579

560580
(** With heterogeneous environments. *)
@@ -840,7 +860,7 @@ end
840860
(** Lift [D] to a non-reduced product with box.
841861
Both are updated in parallel, but [D] answers to queries.
842862
Box domain is used to filter out non-relational invariants for output. *)
843-
module BoxProd0 (D: S3) =
863+
module BoxProd0 (D: S3) = (* TODO: remove? *)
844864
struct
845865
module BoxD = D2 (IntervalManager)
846866

‎tests/regression/36-apron/01-octagon_simple.t‎

Lines changed: 37 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -196,7 +196,7 @@ With diff-box:
196196
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (01-octagon_simple.c:44:10-44:11)
197197
[Info][Witness] witness generation summary:
198198
location invariants: 0
199-
loop invariants: 6
199+
loop invariants: 2
200200
flow-insensitive invariants: 0
201201
total generation entries: 1
202202

@@ -212,24 +212,6 @@ With diff-box:
212212
function: main
213213
value: (long long )N >= (long long )X
214214
format: c_expression
215-
- invariant:
216-
type: loop_invariant
217-
location:
218-
file_name: 01-octagon_simple.c
219-
line: 10
220-
column: 3
221-
function: main
222-
value: 2147483647LL >= (long long )X
223-
format: c_expression
224-
- invariant:
225-
type: loop_invariant
226-
location:
227-
file_name: 01-octagon_simple.c
228-
line: 10
229-
column: 3
230-
function: main
231-
value: 4294967294LL >= (long long )X + (long long )N
232-
format: c_expression
233215
- invariant:
234216
type: loop_invariant
235217
location:
@@ -239,29 +221,29 @@ With diff-box:
239221
function: two
240222
value: (long long )N >= (long long )X
241223
format: c_expression
242-
- invariant:
243-
type: loop_invariant
244-
location:
245-
file_name: 01-octagon_simple.c
246-
line: 44
247-
column: 3
248-
function: two
249-
value: 2147483647LL >= (long long )X
250-
format: c_expression
251-
- invariant:
252-
type: loop_invariant
253-
location:
254-
file_name: 01-octagon_simple.c
255-
line: 44
256-
column: 3
257-
function: two
258-
value: 4294967294LL >= (long long )X + (long long )N
259-
format: c_expression
260224

261225
Compare witnesses:
262226

263227
$ yamlWitnessStripDiff witness-disable-diff-box.yml witness-enable-diff-box.yml
264228
# Left-only invariants:
229+
- invariant:
230+
type: loop_invariant
231+
location:
232+
file_name: 01-octagon_simple.c
233+
line: 44
234+
column: 3
235+
function: two
236+
value: 4294967294LL >= (long long )X + (long long )N
237+
format: c_expression
238+
- invariant:
239+
type: loop_invariant
240+
location:
241+
file_name: 01-octagon_simple.c
242+
line: 44
243+
column: 3
244+
function: two
245+
value: 2147483647LL >= (long long )X
246+
format: c_expression
265247
- invariant:
266248
type: loop_invariant
267249
location:
@@ -307,6 +289,24 @@ Compare witnesses:
307289
function: two
308290
value: (long long )N >= 0LL
309291
format: c_expression
292+
- invariant:
293+
type: loop_invariant
294+
location:
295+
file_name: 01-octagon_simple.c
296+
line: 10
297+
column: 3
298+
function: main
299+
value: 4294967294LL >= (long long )X + (long long )N
300+
format: c_expression
301+
- invariant:
302+
type: loop_invariant
303+
location:
304+
file_name: 01-octagon_simple.c
305+
line: 10
306+
column: 3
307+
function: main
308+
value: 2147483647LL >= (long long )X
309+
format: c_expression
310310
- invariant:
311311
type: loop_invariant
312312
location:

‎tests/regression/36-apron/52-queuesize.t‎

Lines changed: 20 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@ With diff-box:
160160
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:56:10-56:11)
161161
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:78:12-78:13)
162162
[Info][Witness] witness generation summary:
163-
location invariants: 6
163+
location invariants: 4
164164
loop invariants: 0
165165
flow-insensitive invariants: 0
166166
total generation entries: 1
@@ -170,6 +170,7 @@ With diff-box:
170170
unsafe: 0
171171
total memory locations: 3
172172

173+
TODO: Should (long long )free >= 0LL somehow still remain, because it cannot be inferred by box alone?
173174
$ yamlWitnessStrip < witness.yml | tee witness-enable-diff-box.yml
174175
- entry_type: invariant_set
175176
content:
@@ -182,15 +183,6 @@ With diff-box:
182183
function: pop
183184
value: (long long )capacity >= (long long )free
184185
format: c_expression
185-
- invariant:
186-
type: location_invariant
187-
location:
188-
file_name: 52-queuesize.c
189-
line: 15
190-
column: 3
191-
function: pop
192-
value: (long long )free >= 0LL
193-
format: c_expression
194186
- invariant:
195187
type: location_invariant
196188
location:
@@ -209,15 +201,6 @@ With diff-box:
209201
function: push
210202
value: (long long )capacity >= (long long )free
211203
format: c_expression
212-
- invariant:
213-
type: location_invariant
214-
location:
215-
file_name: 52-queuesize.c
216-
line: 36
217-
column: 3
218-
function: push
219-
value: (long long )free >= 0LL
220-
format: c_expression
221204
- invariant:
222205
type: location_invariant
223206
location:
@@ -241,6 +224,15 @@ Compare witnesses:
241224
function: push
242225
value: 2147483647LL >= (long long )capacity
243226
format: c_expression
227+
- invariant:
228+
type: location_invariant
229+
location:
230+
file_name: 52-queuesize.c
231+
line: 36
232+
column: 3
233+
function: push
234+
value: (long long )free >= 0LL
235+
format: c_expression
244236
- invariant:
245237
type: location_invariant
246238
location:
@@ -250,4 +242,13 @@ Compare witnesses:
250242
function: pop
251243
value: 2147483647LL >= (long long )capacity
252244
format: c_expression
245+
- invariant:
246+
type: location_invariant
247+
location:
248+
file_name: 52-queuesize.c
249+
line: 15
250+
column: 3
251+
function: pop
252+
value: (long long )free >= 0LL
253+
format: c_expression
253254
---

‎tests/regression/89-apron3/03-octagon_simplest.t‎

Lines changed: 37 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -179,11 +179,10 @@ With diff-box:
179179
[Warning][Deadcode][CWE-570] condition 'N < 0' is always false (03-octagon_simplest.c:9:6-9:11)
180180
[Info][Witness] witness generation summary:
181181
location invariants: 0
182-
loop invariants: 5
182+
loop invariants: 1
183183
flow-insensitive invariants: 0
184184
total generation entries: 1
185185

186-
TODO: diff-box isn't enough to get rid of invariants with Y (which is known to be 0)
187186
$ yamlWitnessStrip < witness.yml | tee witness-enable-diff-box.yml
188187
- entry_type: invariant_set
189188
content:
@@ -196,47 +195,29 @@ TODO: diff-box isn't enough to get rid of invariants with Y (which is known to b
196195
function: main
197196
value: (long long )N >= (long long )X
198197
format: c_expression
199-
- invariant:
200-
type: loop_invariant
201-
location:
202-
file_name: 03-octagon_simplest.c
203-
line: 11
204-
column: 3
205-
function: main
206-
value: (long long )Y + 2147483647LL >= (long long )X
207-
format: c_expression
208-
- invariant:
209-
type: loop_invariant
210-
location:
211-
file_name: 03-octagon_simplest.c
212-
line: 11
213-
column: 3
214-
function: main
215-
value: 2147483647LL >= (long long )X
216-
format: c_expression
217-
- invariant:
218-
type: loop_invariant
219-
location:
220-
file_name: 03-octagon_simplest.c
221-
line: 11
222-
column: 3
223-
function: main
224-
value: 2147483647LL >= (long long )Y + (long long )X
225-
format: c_expression
226-
- invariant:
227-
type: loop_invariant
228-
location:
229-
file_name: 03-octagon_simplest.c
230-
line: 11
231-
column: 3
232-
function: main
233-
value: 4294967294LL >= (long long )X + (long long )N
234-
format: c_expression
235198

236199
Compare witnesses:
237200

238201
$ yamlWitnessStripDiff witness-disable-diff-box.yml witness-enable-diff-box.yml
239202
# Left-only invariants:
203+
- invariant:
204+
type: loop_invariant
205+
location:
206+
file_name: 03-octagon_simplest.c
207+
line: 11
208+
column: 3
209+
function: main
210+
value: 4294967294LL >= (long long )X + (long long )N
211+
format: c_expression
212+
- invariant:
213+
type: loop_invariant
214+
location:
215+
file_name: 03-octagon_simplest.c
216+
line: 11
217+
column: 3
218+
function: main
219+
value: 2147483647LL >= (long long )Y + (long long )X
220+
format: c_expression
240221
- invariant:
241222
type: loop_invariant
242223
location:
@@ -246,6 +227,15 @@ Compare witnesses:
246227
function: main
247228
value: 2147483647LL >= (long long )Y + (long long )N
248229
format: c_expression
230+
- invariant:
231+
type: loop_invariant
232+
location:
233+
file_name: 03-octagon_simplest.c
234+
line: 11
235+
column: 3
236+
function: main
237+
value: 2147483647LL >= (long long )X
238+
format: c_expression
249239
- invariant:
250240
type: loop_invariant
251241
location:
@@ -264,6 +254,15 @@ Compare witnesses:
264254
function: main
265255
value: (long long )Y == 0LL
266256
format: c_expression
257+
- invariant:
258+
type: loop_invariant
259+
location:
260+
file_name: 03-octagon_simplest.c
261+
line: 11
262+
column: 3
263+
function: main
264+
value: (long long )Y + 2147483647LL >= (long long )X
265+
format: c_expression
267266
- invariant:
268267
type: loop_invariant
269268
location:

0 commit comments

Comments
 (0)