Skip to content

Commit 662e770

Browse files
sim642sim642
authored
Merge pull request #1871 from goblint/apron-octagon-invariant-simplify
Fix `GobApron.Linxexpr0.neg` not negating all dimensions
2 parents 5ee8c42 + 6f7c881 commit 662e770

File tree

6 files changed

+735
-5
lines changed

6 files changed

+735
-5
lines changed

‎.semgrep/apron.yml‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
rules:
2+
- id: apron-linexp0-get_size
3+
pattern-either:
4+
- pattern: Linexpr0.get_size
5+
- pattern: Apron.Linexpr0.get_size
6+
- pattern: GobApron.Linexpr0.get_size
7+
message: don't use (returns some internal size, not number of dimensions)
8+
languages: [ocaml]
9+
severity: ERROR

‎src/cdomains/apron/gobApron.apron.ml‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,10 @@ struct
4444
(** Negate linear expression. *)
4545
let neg (linexpr0: t): t =
4646
let r = copy linexpr0 in
47-
let n = Linexpr0.get_size r in
48-
for i = 0 to n - 1 do
49-
Linexpr0.set_coeff r i (Coeff.neg (Linexpr0.get_coeff r i))
50-
done;
51-
Linexpr0.set_cst r (Coeff.neg (Linexpr0.get_cst r));
47+
Linexpr0.iter (fun c i ->
48+
Linexpr0.set_coeff r i (Coeff.neg c)
49+
) linexpr0;
50+
Linexpr0.set_cst r (Coeff.neg (Linexpr0.get_cst linexpr0));
5251
r
5352
end
5453

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

Lines changed: 355 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,355 @@
1+
Without diff-box:
2+
3+
$ goblint --set ana.activated[+] apron --set ana.apron.domain octagon --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["loop_invariant"]' --disable ana.base.invariant.enabled --enable ana.relation.invariant.one-var --disable ana.apron.invariant.diff-box 01-octagon_simple.c
4+
[Success][Assert] Assertion "X - N == 0" will succeed (01-octagon_simple.c:14:3-14:28)
5+
[Success][Assert] Assertion "X == N" will succeed (01-octagon_simple.c:15:3-15:26)
6+
[Success][Assert] Assertion "N == 8" will succeed (01-octagon_simple.c:24:3-24:26)
7+
[Success][Assert] Assertion "X <= N" will succeed (01-octagon_simple.c:42:3-42:26)
8+
[Success][Assert] Assertion "X - N == 0" will succeed (01-octagon_simple.c:53:3-53:30)
9+
[Success][Assert] Assertion "X == N" will succeed (01-octagon_simple.c:54:3-54:26)
10+
[Warning][Deadcode] Function 'main' has dead code:
11+
on line 21 (01-octagon_simple.c:21-21)
12+
[Warning][Deadcode] Function 'two' has dead code:
13+
on line 39 (01-octagon_simple.c:39-39)
14+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
15+
live: 25
16+
dead: 2
17+
total lines: 27
18+
[Warning][Deadcode][CWE-570] condition 'N < 0' is always false (01-octagon_simple.c:8:6-8:11)
19+
[Warning][Deadcode][CWE-571] condition 'X == N' is always true (01-octagon_simple.c:17:6-17:12)
20+
[Warning][Deadcode][CWE-570] condition 'N < 0' is always false (01-octagon_simple.c:38:7-38:12)
21+
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (01-octagon_simple.c:44:10-44:11)
22+
[Info][Witness] witness generation summary:
23+
location invariants: 0
24+
loop invariants: 16
25+
flow-insensitive invariants: 0
26+
total generation entries: 1
27+
28+
$ yamlWitnessStrip < witness.yml | tee witness-disable-diff-box.yml
29+
- entry_type: invariant_set
30+
content:
31+
- invariant:
32+
type: loop_invariant
33+
location:
34+
file_name: 01-octagon_simple.c
35+
line: 10
36+
column: 3
37+
function: main
38+
value: (long long )N >= (long long )X
39+
format: c_expression
40+
- invariant:
41+
type: loop_invariant
42+
location:
43+
file_name: 01-octagon_simple.c
44+
line: 10
45+
column: 3
46+
function: main
47+
value: (long long )N >= 0LL
48+
format: c_expression
49+
- invariant:
50+
type: loop_invariant
51+
location:
52+
file_name: 01-octagon_simple.c
53+
line: 10
54+
column: 3
55+
function: main
56+
value: (long long )X + (long long )N >= 0LL
57+
format: c_expression
58+
- invariant:
59+
type: loop_invariant
60+
location:
61+
file_name: 01-octagon_simple.c
62+
line: 10
63+
column: 3
64+
function: main
65+
value: (long long )X + 2147483647LL >= (long long )N
66+
format: c_expression
67+
- invariant:
68+
type: loop_invariant
69+
location:
70+
file_name: 01-octagon_simple.c
71+
line: 10
72+
column: 3
73+
function: main
74+
value: (long long )X >= 0LL
75+
format: c_expression
76+
- invariant:
77+
type: loop_invariant
78+
location:
79+
file_name: 01-octagon_simple.c
80+
line: 10
81+
column: 3
82+
function: main
83+
value: 2147483647LL >= (long long )N
84+
format: c_expression
85+
- invariant:
86+
type: loop_invariant
87+
location:
88+
file_name: 01-octagon_simple.c
89+
line: 10
90+
column: 3
91+
function: main
92+
value: 2147483647LL >= (long long )X
93+
format: c_expression
94+
- invariant:
95+
type: loop_invariant
96+
location:
97+
file_name: 01-octagon_simple.c
98+
line: 10
99+
column: 3
100+
function: main
101+
value: 4294967294LL >= (long long )X + (long long )N
102+
format: c_expression
103+
- invariant:
104+
type: loop_invariant
105+
location:
106+
file_name: 01-octagon_simple.c
107+
line: 44
108+
column: 3
109+
function: two
110+
value: (long long )N >= (long long )X
111+
format: c_expression
112+
- invariant:
113+
type: loop_invariant
114+
location:
115+
file_name: 01-octagon_simple.c
116+
line: 44
117+
column: 3
118+
function: two
119+
value: (long long )N >= 0LL
120+
format: c_expression
121+
- invariant:
122+
type: loop_invariant
123+
location:
124+
file_name: 01-octagon_simple.c
125+
line: 44
126+
column: 3
127+
function: two
128+
value: (long long )X + (long long )N >= 0LL
129+
format: c_expression
130+
- invariant:
131+
type: loop_invariant
132+
location:
133+
file_name: 01-octagon_simple.c
134+
line: 44
135+
column: 3
136+
function: two
137+
value: (long long )X + 2147483647LL >= (long long )N
138+
format: c_expression
139+
- invariant:
140+
type: loop_invariant
141+
location:
142+
file_name: 01-octagon_simple.c
143+
line: 44
144+
column: 3
145+
function: two
146+
value: (long long )X >= 0LL
147+
format: c_expression
148+
- invariant:
149+
type: loop_invariant
150+
location:
151+
file_name: 01-octagon_simple.c
152+
line: 44
153+
column: 3
154+
function: two
155+
value: 2147483647LL >= (long long )N
156+
format: c_expression
157+
- invariant:
158+
type: loop_invariant
159+
location:
160+
file_name: 01-octagon_simple.c
161+
line: 44
162+
column: 3
163+
function: two
164+
value: 2147483647LL >= (long long )X
165+
format: c_expression
166+
- invariant:
167+
type: loop_invariant
168+
location:
169+
file_name: 01-octagon_simple.c
170+
line: 44
171+
column: 3
172+
function: two
173+
value: 4294967294LL >= (long long )X + (long long )N
174+
format: c_expression
175+
176+
With diff-box:
177+
178+
$ goblint --set ana.activated[+] apron --set ana.apron.domain octagon --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["loop_invariant"]' --disable ana.base.invariant.enabled --enable ana.relation.invariant.one-var --enable ana.apron.invariant.diff-box 01-octagon_simple.c
179+
[Success][Assert] Assertion "X - N == 0" will succeed (01-octagon_simple.c:14:3-14:28)
180+
[Success][Assert] Assertion "X == N" will succeed (01-octagon_simple.c:15:3-15:26)
181+
[Success][Assert] Assertion "N == 8" will succeed (01-octagon_simple.c:24:3-24:26)
182+
[Success][Assert] Assertion "X <= N" will succeed (01-octagon_simple.c:42:3-42:26)
183+
[Success][Assert] Assertion "X - N == 0" will succeed (01-octagon_simple.c:53:3-53:30)
184+
[Success][Assert] Assertion "X == N" will succeed (01-octagon_simple.c:54:3-54:26)
185+
[Warning][Deadcode] Function 'main' has dead code:
186+
on line 21 (01-octagon_simple.c:21-21)
187+
[Warning][Deadcode] Function 'two' has dead code:
188+
on line 39 (01-octagon_simple.c:39-39)
189+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
190+
live: 25
191+
dead: 2
192+
total lines: 27
193+
[Warning][Deadcode][CWE-570] condition 'N < 0' is always false (01-octagon_simple.c:8:6-8:11)
194+
[Warning][Deadcode][CWE-571] condition 'X == N' is always true (01-octagon_simple.c:17:6-17:12)
195+
[Warning][Deadcode][CWE-570] condition 'N < 0' is always false (01-octagon_simple.c:38:7-38:12)
196+
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (01-octagon_simple.c:44:10-44:11)
197+
[Info][Witness] witness generation summary:
198+
location invariants: 0
199+
loop invariants: 6
200+
flow-insensitive invariants: 0
201+
total generation entries: 1
202+
203+
$ yamlWitnessStrip < witness.yml | tee witness-enable-diff-box.yml
204+
- entry_type: invariant_set
205+
content:
206+
- invariant:
207+
type: loop_invariant
208+
location:
209+
file_name: 01-octagon_simple.c
210+
line: 10
211+
column: 3
212+
function: main
213+
value: (long long )N >= (long long )X
214+
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
233+
- invariant:
234+
type: loop_invariant
235+
location:
236+
file_name: 01-octagon_simple.c
237+
line: 44
238+
column: 3
239+
function: two
240+
value: (long long )N >= (long long )X
241+
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
260+
261+
Compare witnesses:
262+
263+
$ yamlWitnessStripDiff witness-disable-diff-box.yml witness-enable-diff-box.yml
264+
# Left-only invariants:
265+
- invariant:
266+
type: loop_invariant
267+
location:
268+
file_name: 01-octagon_simple.c
269+
line: 44
270+
column: 3
271+
function: two
272+
value: 2147483647LL >= (long long )N
273+
format: c_expression
274+
- invariant:
275+
type: loop_invariant
276+
location:
277+
file_name: 01-octagon_simple.c
278+
line: 44
279+
column: 3
280+
function: two
281+
value: (long long )X >= 0LL
282+
format: c_expression
283+
- invariant:
284+
type: loop_invariant
285+
location:
286+
file_name: 01-octagon_simple.c
287+
line: 44
288+
column: 3
289+
function: two
290+
value: (long long )X + 2147483647LL >= (long long )N
291+
format: c_expression
292+
- invariant:
293+
type: loop_invariant
294+
location:
295+
file_name: 01-octagon_simple.c
296+
line: 44
297+
column: 3
298+
function: two
299+
value: (long long )X + (long long )N >= 0LL
300+
format: c_expression
301+
- invariant:
302+
type: loop_invariant
303+
location:
304+
file_name: 01-octagon_simple.c
305+
line: 44
306+
column: 3
307+
function: two
308+
value: (long long )N >= 0LL
309+
format: c_expression
310+
- invariant:
311+
type: loop_invariant
312+
location:
313+
file_name: 01-octagon_simple.c
314+
line: 10
315+
column: 3
316+
function: main
317+
value: 2147483647LL >= (long long )N
318+
format: c_expression
319+
- invariant:
320+
type: loop_invariant
321+
location:
322+
file_name: 01-octagon_simple.c
323+
line: 10
324+
column: 3
325+
function: main
326+
value: (long long )X >= 0LL
327+
format: c_expression
328+
- invariant:
329+
type: loop_invariant
330+
location:
331+
file_name: 01-octagon_simple.c
332+
line: 10
333+
column: 3
334+
function: main
335+
value: (long long )X + 2147483647LL >= (long long )N
336+
format: c_expression
337+
- invariant:
338+
type: loop_invariant
339+
location:
340+
file_name: 01-octagon_simple.c
341+
line: 10
342+
column: 3
343+
function: main
344+
value: (long long )X + (long long )N >= 0LL
345+
format: c_expression
346+
- invariant:
347+
type: loop_invariant
348+
location:
349+
file_name: 01-octagon_simple.c
350+
line: 10
351+
column: 3
352+
function: main
353+
value: (long long )N >= 0LL
354+
format: c_expression
355+
---

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// SKIP CRAM PARAM: --set ana.activated[+] apron --enable ana.int.interval
2+
// Simplified from 36-apron/01-octagon_simple
3+
#include <goblint.h>
4+
5+
void main(void) {
6+
int X = 0;
7+
int Y = 0;
8+
int N = rand();
9+
if(N < 0) { N = 0; }
10+
11+
while(X < N) {
12+
X++;
13+
}
14+
}

0 commit comments

Comments
 (0)