Skip to content

Fix Vojdani privatization protected variables in witnesses #1789

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Sep 12, 2025
Merged

Fix Vojdani privatization protected variables in witnesses #1789

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
dbf1f7d
Add witness cram tests for 13-privatized/19-publish-precision and 20-…
sim642 Jul 23, 2025
9c77c8d
Fix Vojdani privatization protected variables in witnesses (closes #1…
sim642 Jul 23, 2025
82f2091
Merge branch 'master' into vojdani-protected-vars
sim642 Sep 12, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/analyses/apron/relationPriv.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -431,7 +431,7 @@ struct

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

let finalize () = ()

Expand Down
6 changes: 3 additions & 3 deletions src/analyses/basePriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,7 +357,7 @@ struct
| `Thread ->
st

let invariant_vars ask getg st = protected_vars ask
let invariant_vars ask getg st = protected_vars ask ~kind:Write
end

module PerMutexMeetPrivBase =
Expand Down Expand Up @@ -856,7 +856,7 @@ struct
) locks inv
)

let invariant_vars ask getg st = protected_vars ask
let invariant_vars ask getg st = protected_vars ask ~kind:ReadWrite
end


Expand Down Expand Up @@ -1102,7 +1102,7 @@ struct
) locks inv
)

let invariant_vars ask getg st = protected_vars ask
let invariant_vars ask getg st = protected_vars ask ~kind:Write
end

module AbstractLockCenteredGBase (WeakRange: Lattice.S) (SyncRange: Lattice.S) =
Expand Down
4 changes: 2 additions & 2 deletions src/analyses/commonPriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,9 +101,9 @@ struct
not (VD.is_immediate_type x.vtype) &&
ask.f (Q.MustBeProtectedBy {mutex=m; global=x; kind; protection})

let protected_vars (ask: Q.ask): varinfo list =
let protected_vars (ask: Q.ask) ~(kind): varinfo list =
LockDomain.MustLockset.fold (fun ml acc ->
Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; kind = Write})) acc
Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; kind})) acc
) (ask.f Q.MustLockset) (Q.VS.empty ())
|> Q.VS.elements
end
Expand Down
227 changes: 227 additions & 0 deletions tests/regression/13-privatized/19-publish-precision.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,3 +19,230 @@
live: 20
dead: 0
total lines: 20


Protection succeeds on check in t_fun.

$ 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
[Success][Assert] Assertion "glob1 == 0" will succeed (19-publish-precision.c:27:3-27:30)
[Success][Assert] Assertion "glob1 == 5" will succeed (19-publish-precision.c:17:3-17:30)
[Warning][Assert] Assertion "glob1 == 0" is unknown. (19-publish-precision.c:30:3-30:30)
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:31:3-31:30)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 20
dead: 0
total lines: 20
[Info][Witness] witness generation summary:
location invariants: 10
loop invariants: 0
flow-insensitive invariants: 0
total generation entries: 1
[Info][Race] Memory locations race summary:
safe: 1
vulnerable: 0
unsafe: 0
total memory locations: 1

$ yamlWitnessStrip < witness.yml
- entry_type: invariant_set
content:
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 11
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 11
column: 3
function: t_fun
value: 0 <= glob1
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 11
column: 3
function: t_fun
value: glob1 <= 127
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 12
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 12
column: 3
function: t_fun
value: 0 <= glob1
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 12
column: 3
function: t_fun
value: glob1 <= 127
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 17
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 17
column: 3
function: t_fun
value: glob1 == 5
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 30
column: 3
function: main
value: 0 <= glob1
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 30
column: 3
function: main
value: glob1 <= 127
format: c_expression


Vojdani does not succeed on check in t_fun.

$ 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
[Success][Assert] Assertion "glob1 == 0" will succeed (19-publish-precision.c:27:3-27:30)
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:17:3-17:30)
[Warning][Assert] Assertion "glob1 == 0" is unknown. (19-publish-precision.c:30:3-30:30)
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:31:3-31:30)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 20
dead: 0
total lines: 20
[Info][Witness] witness generation summary:
location invariants: 9
loop invariants: 0
flow-insensitive invariants: 0
total generation entries: 1
[Info][Race] Memory locations race summary:
safe: 1
vulnerable: 0
unsafe: 0
total memory locations: 1

Vojdani should not have location_invariant-s on glob1 after locking mutex1 (line 11), only after mutex2.

$ yamlWitnessStrip < witness.yml
- entry_type: invariant_set
content:
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 11
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 12
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 12
column: 3
function: t_fun
value: 0 <= glob1
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 12
column: 3
function: t_fun
value: glob1 <= 127
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 17
column: 3
function: t_fun
value: (unsigned long )arg == 0UL
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 17
column: 3
function: t_fun
value: 0 <= glob1
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 17
column: 3
function: t_fun
value: glob1 <= 127
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 30
column: 3
function: main
value: 0 <= glob1
format: c_expression
- invariant:
type: location_invariant
location:
file_name: 19-publish-precision.c
line: 30
column: 3
function: main
value: glob1 <= 127
format: c_expression
Loading
Loading