Skip to content

Disjoint analysis and analysis filters #208

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

Open
N1ark wants to merge 14 commits into
base: main
Choose a base branch
from
Open

Disjoint analysis and analysis filters #208

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
7ee200a
Add a disjoint analysis
N1ark Dec 20, 2025
b4f2d26
Better reduce `Svalue.distinct`
N1ark Dec 20, 2025
31680ba
Handle `not (distinct _)` in eq analysis
N1ark Dec 20, 2025
b51431d
Re-introduce `AddOvf`
N1ark Dec 20, 2025
7eff7a3
Reduce `n +sovf x`
N1ark Dec 20, 2025
6d30d85
Remove `Declared_vars` from non-incr `Bv_solver`
N1ark Dec 20, 2025
e7a27f8
Add `Analyses.filter`
N1ark Dec 20, 2025
449005f
Fix interval analysis filter
N1ark Dec 20, 2025
e3b4b5c
Tests
N1ark Dec 20, 2025
a8a2c47
Lower bound of pointers is their alignment!
N1ark Dec 20, 2025
b934e84
hacky: ineqs for locations are never dirty
N1ark Dec 20, 2025
626610a
Fix concrete reduction of `ashr`
N1ark Dec 20, 2025
565ae94
More reductions
N1ark Dec 20, 2025
9044f87
Make equality analysis store equalities
N1ark Jan 10, 2026
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
4 changes: 2 additions & 2 deletions soteria-c/test/cram/fixme.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@
raw =
{ args = []; pre = [];
pc =
[(0x0000000000000000 != V|1|); (0x0000000000000000 != V|2|);
(V|1| == V|2|)];
[(V|1| == V|2|); (0x0000000000000000 != V|1|);
(0x0000000000000000 != V|2|)];
post =
{ heap =
[(V|2|,
Expand Down
39 changes: 14 additions & 25 deletions soteria-c/test/cram/simple_bi.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@
info = None })];
globs = [] }
];
pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)];
pc = [(V|2| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|1|)];
post =
{ heap =
[(V|1|,
Expand Down Expand Up @@ -122,7 +122,7 @@ NO_COLOR=true is necessary to avoid test output changing in CI. For some reason,
info = None })];
globs = [] }
];
pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)];
pc = [(V|2| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|1|)];
post =
{ heap =
[(V|1|,
Expand Down Expand Up @@ -254,8 +254,8 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
globs = [] }
];
pc =
[(0x0000000000000000 != V|2|); (0x00000001 <=u V|1|);
(V|1| <=u 0x7fffffff); (V|3| <=u 0x7ffffffffffffffb)];
[(0x00000001 <=u V|1|); (V|1| <=u 0x7fffffff);
(V|3| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|2|)];
post =
{ heap =
[(V|2|,
Expand Down Expand Up @@ -308,8 +308,8 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
globs = [] }
];
pc =
[(0x0000000000000000 != V|1|); (V|3| == 0x00000001);
(V|2| <=u 0x7ffffffffffffffb); (V|3| == 0x00000001)];
[(V|3| == 0x00000001); (V|2| <=u 0x7ffffffffffffffb);
(V|3| == 0x00000001); (0x0000000000000000 != V|1|)];
post =
{ heap =
[(V|1|,
Expand Down Expand Up @@ -340,12 +340,9 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
globs = [] }
];
pc =
[(0x0000000000000000 != V|1|);
(0x0000000000000000 <=s (V|2| + 0x0000000000000004));
((V|4| <s 0x00000000) != ((V|4| + V|5|) <s 0x00000000));
((V|4| <s 0x00000000) == (V|5| <s 0x00000000));
(V|2| <=u 0x7ffffffffffffff7); (0x00000002 <=u V|3|);
(V|3| <=u 0x7fffffff)];
[(V|4| +s_ovf V|5|); (V|2| <=u 0x7ffffffffffffff7);
(0x00000002 <=u V|3|); (V|3| <=u 0x7fffffff);
(0x0000000000000000 != V|1|)];
post =
{ heap =
[(V|1|,
Expand Down Expand Up @@ -381,11 +378,9 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
globs = [] }
];
pc =
[(0x0000000000000000 != V|1|);
(0x0000000000000000 <=s (V|2| + 0x0000000000000004));
(((V|4| <s 0x00000000) == ((V|4| + V|5|) <s 0x00000000)) || ((V|4| <s 0x00000000) != (V|5| <s 0x00000000)));
(V|3| == 0x00000002); (V|2| <=u 0x7ffffffffffffff7);
(V|3| == 0x00000002)];
[!((V|4| +s_ovf V|5|)); (V|3| == 0x00000002);
(V|2| <=u 0x7ffffffffffffff7); (V|3| == 0x00000002);
(0x0000000000000000 != V|1|)];
post =
{ heap =
[(V|1|,
Expand All @@ -408,10 +403,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
Summaries for add_561:
Analysed {
raw =
{ args = [V|1|; V|2|]; pre = [];
pc =
[((V|1| <s 0x00000000) != ((V|1| + V|2|) <s 0x00000000));
((V|1| <s 0x00000000) == (V|2| <s 0x00000000))];
{ args = [V|1|; V|2|]; pre = []; pc = [(V|1| +s_ovf V|2|)];
post = { heap = []; globs = [] };
ret =
(Error (Integer overflow,
Expand All @@ -420,10 +412,7 @@ if%sat1 had the wrong semantics and would not correctly backtrack.
manifest_bugs = []}
Analysed {
raw =
{ args = [V|1|; V|2|]; pre = [];
pc =
[(((V|1| <s 0x00000000) == ((V|1| + V|2|) <s 0x00000000)) || ((V|1| <s 0x00000000) != (V|2| <s 0x00000000)))
];
{ args = [V|1|; V|2|]; pre = []; pc = [!((V|1| +s_ovf V|2|))];
post = { heap = []; globs = [] }; ret = (Ok (V|1| +ck V|2|)) };
manifest_bugs = []}

Expand Down
2 changes: 1 addition & 1 deletion soteria-rust/lib/sptr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ module DecayMap : DecayMapS = struct
Rustsymex.assume
[
(addr %@ align ==@ Usize.(0s));
Usize.(0s) <@ addr;
align <=@ addr;
addr <@ Typed.BitVec.usize isize_max -!@ size;
]
in
Expand Down
71 changes: 35 additions & 36 deletions soteria-rust/test/cram/kani.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,70 +97,70 @@ Test kani::vec::any_vec
Compiling... done in <time>
note: len_capacity_invariant: done in <time>, ran 17 branches
PC 1: (extract[0-1](V|18|) == 0b00) /\ (0x0000000000000000 == V|1|) /\
(0x0000000000000000 == V|1|) /\ (0x0000000000000001 <=u V|18|) /\
(0x0000000000000000 == V|1|) /\ (0x0000000000000004 <=u V|18|) /\
(V|18| <=u 0x7fffffffffffffbe)
PC 2: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000f) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000f) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffc2)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffc2)
PC 3: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000e) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000e) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffc6)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffc6)
PC 4: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000d) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000d) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffca)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffca)
PC 5: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000c) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000c) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffce)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffce)
PC 6: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000b) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000b) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffd2)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffd2)
PC 7: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x000000000000000a) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x000000000000000a) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffd6)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffd6)
PC 8: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000009) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000009) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffda)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffda)
PC 9: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000008) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000008) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffde)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffde)
PC 10: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000007) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000007) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffe2)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffe2)
PC 11: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000006) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000006) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffe6)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffe6)
PC 12: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000005) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000005) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffea)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffea)
PC 13: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000004) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000004) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffee)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7fffffffffffffee)
PC 14: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000003) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000003) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffff2)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffff2)
PC 15: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000002) /\
(0b00 == extract[0-1](V|19|)) /\ (V|1| == 0x0000000000000002) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffff6)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffff6)
PC 16: (extract[0-1](V|18|) == 0b00) /\ (0x0000000000000001 == V|1|) /\
(0b00 == extract[0-1](V|19|)) /\ (0x0000000000000001 == V|1|) /\
(0x0000000000000001 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000001 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffffa)
(0x0000000000000004 <=u V|18|) /\ (V|18| <=u 0x7fffffffffffffbe) /\
(0x0000000000000004 <=u V|19|) /\ (V|19| <=u 0x7ffffffffffffffa)
PC 17: (extract[0-1](V|18|) == 0b00) /\ (V|1| == 0x0000000000000010) /\
(V|1| == 0x0000000000000010) /\ (0x0000000000000001 <=u V|18|) /\
(V|1| == 0x0000000000000010) /\ (0x0000000000000004 <=u V|18|) /\
(V|18| <=u 0x7fffffffffffffbe)

Test our simple Kani demo works
Expand All @@ -175,11 +175,10 @@ Test our simple Kani demo works
10 │ let b: u32 = kani::any();
11 │ if a + b < u32::MAX {
│ ^^^^^ Triggering memory operation
PC 1: (((0xffffffff -ck V|1|) <u V|2|) || ((0xffffffff -ck V|2|) <u V|1|))
PC 1: (V|1| +u_ovf V|2|)

note: saturating_add: done in <time>, ran 2 branches
PC 1: (V|1| <u (0xffffffff -ck V|2|)) /\ (V|1| <=u (0xffffffff -ck V|2|)) /\
(V|2| <=u (0xffffffff -ck V|1|))
PC 1: (V|1| <u (0xffffffff -ck V|2|)) /\ !((V|1| +u_ovf V|2|))
PC 2: ((0xffffffff -ck V|2|) <=u V|1|)

error: memory_leak: found issues in <time>, errors in 1 branch (out of 1)
Expand All @@ -190,7 +189,7 @@ Test our simple Kani demo works
│ │
│ Leaking function
│ 1: Entry point
PC 1: (extract[0-1](V|1|) == 0b00) /\ (0x0000000000000001 <=u V|1|) /\
PC 1: (extract[0-1](V|1|) == 0b00) /\ (0x0000000000000004 <=u V|1|) /\
(V|1| <=u 0x7ffffffffffffffa)

error: uninit_access: found issues in <time>, errors in 1 branch (out of 2)
Expand Down
8 changes: 4 additions & 4 deletions soteria-rust/test/cram/simple.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ Test memory leaks
│ │
│ Leaking function
│ 1: Entry point
PC 1: (extract[0-1](V|1|) == 0b00) /\ (0x0000000000000001 <=u V|1|) /\
PC 1: (extract[0-1](V|1|) == 0b00) /\ (0x0000000000000004 <=u V|1|) /\
(V|1| <=u 0x7ffffffffffffffa)

[1]
Expand Down Expand Up @@ -57,9 +57,9 @@ Test that we properly handle the niche optimisation
Compiling... done in <time>
note: main: done in <time>, ran 1 branch
PC 1: (extract[0-1](V|1|) == 0b00) /\ (0b00 == extract[0-1](V|2|)) /\
(0b00 == extract[0-1](V|3|)) /\ (0x0000000000000001 <=u V|1|) /\
(V|1| <=u 0x7ffffffffffffffa) /\ (0x0000000000000001 <=u V|2|) /\
(V|2| <=u 0x7ffffffffffffff6) /\ (0x0000000000000001 <=u V|3|) /\
(0b00 == extract[0-1](V|3|)) /\ (0x0000000000000004 <=u V|1|) /\
(V|1| <=u 0x7ffffffffffffffa) /\ (0x0000000000000004 <=u V|2|) /\
(V|2| <=u 0x7ffffffffffffff6) /\ (0x0000000000000004 <=u V|3|) /\
(V|3| <=u 0x7ffffffffffffffa)

Test function calls on function pointers
Expand Down
Loading
Loading