Skip to content

Commit 0f224a8

Browse files
sim642sim642
authored
Merge pull request #1789 from goblint/vojdani-protected-vars
Fix Vojdani privatization protected variables in witnesses
2 parents ccb20dc + 82f2091 commit 0f224a8

File tree

5 files changed

+527
-6
lines changed

5 files changed

+527
-6
lines changed

‎src/analyses/apron/relationPriv.apron.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -431,7 +431,7 @@ struct
431431

432432
let iter_sys_vars getg vq vf = () (* TODO: or report singleton global for any Global query? *)
433433
let invariant_global ask getg g = Invariant.none
434-
let invariant_vars ask getg st = protected_vars ask (* TODO: is this right? *)
434+
let invariant_vars ask getg st = protected_vars ask ~kind:Write (* TODO: is this right? *)
435435

436436
let finalize () = ()
437437

‎src/analyses/basePriv.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -357,7 +357,7 @@ struct
357357
| `Thread ->
358358
st
359359

360-
let invariant_vars ask getg st = protected_vars ask
360+
let invariant_vars ask getg st = protected_vars ask ~kind:Write
361361
end
362362

363363
module PerMutexMeetPrivBase =
@@ -856,7 +856,7 @@ struct
856856
) locks inv
857857
)
858858

859-
let invariant_vars ask getg st = protected_vars ask
859+
let invariant_vars ask getg st = protected_vars ask ~kind:ReadWrite
860860
end
861861

862862

@@ -1102,7 +1102,7 @@ struct
11021102
) locks inv
11031103
)
11041104

1105-
let invariant_vars ask getg st = protected_vars ask
1105+
let invariant_vars ask getg st = protected_vars ask ~kind:Write
11061106
end
11071107

11081108
module AbstractLockCenteredGBase (WeakRange: Lattice.S) (SyncRange: Lattice.S) =

‎src/analyses/commonPriv.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,9 +101,9 @@ struct
101101
not (VD.is_immediate_type x.vtype) &&
102102
ask.f (Q.MustBeProtectedBy {mutex=m; global=x; kind; protection})
103103

104-
let protected_vars (ask: Q.ask): varinfo list =
104+
let protected_vars (ask: Q.ask) ~(kind): varinfo list =
105105
LockDomain.MustLockset.fold (fun ml acc ->
106-
Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; kind = Write})) acc
106+
Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; kind})) acc
107107
) (ask.f Q.MustLockset) (Q.VS.empty ())
108108
|> Q.VS.elements
109109
end

‎tests/regression/13-privatized/19-publish-precision.t‎

Lines changed: 227 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,3 +19,230 @@
1919
live: 20
2020
dead: 0
2121
total lines: 20
22+
23+
24+
Protection succeeds on check in t_fun.
25+
26+
$ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --disable witness.invariant.other 19-publish-precision.c
27+
[Success][Assert] Assertion "glob1 == 0" will succeed (19-publish-precision.c:27:3-27:30)
28+
[Success][Assert] Assertion "glob1 == 5" will succeed (19-publish-precision.c:17:3-17:30)
29+
[Warning][Assert] Assertion "glob1 == 0" is unknown. (19-publish-precision.c:30:3-30:30)
30+
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:31:3-31:30)
31+
[Info][Deadcode] Logical lines of code (LLoC) summary:
32+
live: 20
33+
dead: 0
34+
total lines: 20
35+
[Info][Witness] witness generation summary:
36+
location invariants: 10
37+
loop invariants: 0
38+
flow-insensitive invariants: 0
39+
total generation entries: 1
40+
[Info][Race] Memory locations race summary:
41+
safe: 1
42+
vulnerable: 0
43+
unsafe: 0
44+
total memory locations: 1
45+
46+
$ yamlWitnessStrip < witness.yml
47+
- entry_type: invariant_set
48+
content:
49+
- invariant:
50+
type: location_invariant
51+
location:
52+
file_name: 19-publish-precision.c
53+
line: 11
54+
column: 3
55+
function: t_fun
56+
value: (unsigned long )arg == 0UL
57+
format: c_expression
58+
- invariant:
59+
type: location_invariant
60+
location:
61+
file_name: 19-publish-precision.c
62+
line: 11
63+
column: 3
64+
function: t_fun
65+
value: 0 <= glob1
66+
format: c_expression
67+
- invariant:
68+
type: location_invariant
69+
location:
70+
file_name: 19-publish-precision.c
71+
line: 11
72+
column: 3
73+
function: t_fun
74+
value: glob1 <= 127
75+
format: c_expression
76+
- invariant:
77+
type: location_invariant
78+
location:
79+
file_name: 19-publish-precision.c
80+
line: 12
81+
column: 3
82+
function: t_fun
83+
value: (unsigned long )arg == 0UL
84+
format: c_expression
85+
- invariant:
86+
type: location_invariant
87+
location:
88+
file_name: 19-publish-precision.c
89+
line: 12
90+
column: 3
91+
function: t_fun
92+
value: 0 <= glob1
93+
format: c_expression
94+
- invariant:
95+
type: location_invariant
96+
location:
97+
file_name: 19-publish-precision.c
98+
line: 12
99+
column: 3
100+
function: t_fun
101+
value: glob1 <= 127
102+
format: c_expression
103+
- invariant:
104+
type: location_invariant
105+
location:
106+
file_name: 19-publish-precision.c
107+
line: 17
108+
column: 3
109+
function: t_fun
110+
value: (unsigned long )arg == 0UL
111+
format: c_expression
112+
- invariant:
113+
type: location_invariant
114+
location:
115+
file_name: 19-publish-precision.c
116+
line: 17
117+
column: 3
118+
function: t_fun
119+
value: glob1 == 5
120+
format: c_expression
121+
- invariant:
122+
type: location_invariant
123+
location:
124+
file_name: 19-publish-precision.c
125+
line: 30
126+
column: 3
127+
function: main
128+
value: 0 <= glob1
129+
format: c_expression
130+
- invariant:
131+
type: location_invariant
132+
location:
133+
file_name: 19-publish-precision.c
134+
line: 30
135+
column: 3
136+
function: main
137+
value: glob1 <= 127
138+
format: c_expression
139+
140+
141+
Vojdani does not succeed on check in t_fun.
142+
143+
$ goblint --set ana.base.privatization vojdani --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --disable witness.invariant.other 19-publish-precision.c
144+
[Success][Assert] Assertion "glob1 == 0" will succeed (19-publish-precision.c:27:3-27:30)
145+
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:17:3-17:30)
146+
[Warning][Assert] Assertion "glob1 == 0" is unknown. (19-publish-precision.c:30:3-30:30)
147+
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:31:3-31:30)
148+
[Info][Deadcode] Logical lines of code (LLoC) summary:
149+
live: 20
150+
dead: 0
151+
total lines: 20
152+
[Info][Witness] witness generation summary:
153+
location invariants: 9
154+
loop invariants: 0
155+
flow-insensitive invariants: 0
156+
total generation entries: 1
157+
[Info][Race] Memory locations race summary:
158+
safe: 1
159+
vulnerable: 0
160+
unsafe: 0
161+
total memory locations: 1
162+
163+
Vojdani should not have location_invariant-s on glob1 after locking mutex1 (line 11), only after mutex2.
164+
165+
$ yamlWitnessStrip < witness.yml
166+
- entry_type: invariant_set
167+
content:
168+
- invariant:
169+
type: location_invariant
170+
location:
171+
file_name: 19-publish-precision.c
172+
line: 11
173+
column: 3
174+
function: t_fun
175+
value: (unsigned long )arg == 0UL
176+
format: c_expression
177+
- invariant:
178+
type: location_invariant
179+
location:
180+
file_name: 19-publish-precision.c
181+
line: 12
182+
column: 3
183+
function: t_fun
184+
value: (unsigned long )arg == 0UL
185+
format: c_expression
186+
- invariant:
187+
type: location_invariant
188+
location:
189+
file_name: 19-publish-precision.c
190+
line: 12
191+
column: 3
192+
function: t_fun
193+
value: 0 <= glob1
194+
format: c_expression
195+
- invariant:
196+
type: location_invariant
197+
location:
198+
file_name: 19-publish-precision.c
199+
line: 12
200+
column: 3
201+
function: t_fun
202+
value: glob1 <= 127
203+
format: c_expression
204+
- invariant:
205+
type: location_invariant
206+
location:
207+
file_name: 19-publish-precision.c
208+
line: 17
209+
column: 3
210+
function: t_fun
211+
value: (unsigned long )arg == 0UL
212+
format: c_expression
213+
- invariant:
214+
type: location_invariant
215+
location:
216+
file_name: 19-publish-precision.c
217+
line: 17
218+
column: 3
219+
function: t_fun
220+
value: 0 <= glob1
221+
format: c_expression
222+
- invariant:
223+
type: location_invariant
224+
location:
225+
file_name: 19-publish-precision.c
226+
line: 17
227+
column: 3
228+
function: t_fun
229+
value: glob1 <= 127
230+
format: c_expression
231+
- invariant:
232+
type: location_invariant
233+
location:
234+
file_name: 19-publish-precision.c
235+
line: 30
236+
column: 3
237+
function: main
238+
value: 0 <= glob1
239+
format: c_expression
240+
- invariant:
241+
type: location_invariant
242+
location:
243+
file_name: 19-publish-precision.c
244+
line: 30
245+
column: 3
246+
function: main
247+
value: glob1 <= 127
248+
format: c_expression

0 commit comments

Comments
 (0)