Martin Blicha
12bca24774
[SMTChecker] Use path condition when creating CHC targets
...
Without path condition, verification targets created inside ternary
operator ignore the condition of the operator inside the branches.
This led to false positives.
Further updates:
- Function calls should consider the conditions under which they are
called, otherwise the analysis may report false positives.
The fix proposed here is to add the current path condition to the edge
that propagates error from a function call.
- Increment error index after function call
This is necessary for the analysis of the ternary operator to work
correctly. No information should leak from a function call inside a
ternary operator in the first branch to the second branch, including
whether or not an error would have occured in the first branch.
However, for the execution that continues after the function call,
we still need to ensure that under the current path condition
the error has not occurred in that function call.
It would be better to isolate the analysis of the branches to separate
clauses, but I do not see an easy way for that now. In this way, even
though the function call in first branch is included in the clause of
the second branch, no information leaks.
- Additonal test for ternary operator
This tests the behaviour of SMTChecker on ternary operator with function
calls inside both branches. Specifically, it tests that SMTChecker
successfully detects a violation of a verification target in the second
branch when the same target is present also in the first branch, but
there it cannot be triggered because of the operator's condition.
2023-04-21 18:56:34 +02:00
Leo Alt
ce9a7ee954
update smtchecker tests
2023-03-28 18:23:54 +02:00
Leo Alt
aacbe72079
group unsupported warnings
2023-03-15 17:06:06 +01:00
Leo Alt
21c0f78650
Report safe properties in BMC and CHC
2023-03-09 14:59:32 +01:00
wechman
aba5ac5e2a
User-defined operators: Tests
2023-02-22 00:40:03 +01:00
Leo
59f9ab4dee
Merge pull request #13939 from pgebal/fix_handling_bitwise_operators_when_parsing_z3_call_result
...
Fixes handling bitwise operators for z3 model checker
2023-02-09 12:16:28 +01:00
Pawel Gebal
a38549dc19
Fixes handling bitwise operators for z3 model checker
2023-02-08 18:37:17 +01:00
Leo Alt
db9c11a2a5
fix abstract nondet exception
2023-02-08 16:59:37 +01:00
Leo Alt
8d91ccf028
[SMTChecker] Add a new trusted mode which assumes that code that is
...
available at compile time is trusted.
2023-02-06 17:02:33 +01:00
Rodrigo Q. Saramago
feba4de509
Add paris constraints to SMTChecker
...
Co-authored-by: Daniel <daniel@ekpyron.org>
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
Co-authored-by: Leo <leo@ethereum.org>
2023-01-31 11:03:04 +01:00
Kamil Śliwak
71506bd3b3
Consistent terminology for attached/bound functions (file rename)
2022-12-07 19:31:44 +01:00
Leo Alt
77698f8108
Fix internal error when deleting struct member of function type
2022-11-30 12:47:32 +01:00
Leo Alt
608b424afc
Fix internal error when using user defined value types as mapping indices or struct members.
2022-11-29 13:04:01 +01:00
Leo Alt
07870d0318
Fix internal error in assignment chains that also assign to fully qualified state variables (, for example), where the contract expression is a tuble.
2022-11-28 18:45:50 +01:00
Leo Alt
a5dab6181c
Fix internal error when the abstract-nondet SMTChecker natspec annotation is used with a wrong option multiple times for the same function
2022-11-28 16:59:35 +01:00
Leo Alt
9a8dd4242f
Fix SMTChecker bug when a public library function is called internally by an internal library function, which in turn is called internally by a contract.
2022-11-28 13:07:18 +01:00
Leo Alt
d660f0cab0
adjust nondeterministic tests
2022-11-24 13:08:06 +01:00
Leo Alt
504b70b6af
update smt tests
2022-11-24 13:08:06 +01:00
Ishtiaque Zahid
3abf2724a1
changed output of formatNumberReadable so that it shows powers of two and one-less-than powers of two in a more compact format
2022-11-14 17:37:38 +01:00
Leo Alt
16c0838f75
Update docker images and tests
2022-08-30 11:51:59 +02:00
Ishtiaque Zahid
61febbd249
formatNumberReadable now prints signed integers as well
2022-06-24 07:15:15 +06:00
Leo Alt
6a126f6ccb
Update tests and hashes for z3 4.8.17
2022-05-13 15:25:10 +02:00
Leo Alt
cbaba6f913
update tests
2022-05-11 20:02:31 +02:00
Kamil Śliwak
0e0d1972f9
Disable non-deterministic counterexamples in some SMT tests
...
- The counterexamples sometimes do appear and the tests fail.
2022-05-10 12:48:01 +02:00
Leo Alt
201c6c6819
fix smt flaky test
2022-05-05 11:38:16 +02:00
Leo Alt
cba3d18f66
adjust for osx nondeterminism
2022-05-04 19:04:54 +02:00
Leo Alt
4fd7de36f1
update smt tests z3 4.8.16
2022-05-03 14:23:27 +02:00
Leo Alt
f9fa76c9d3
smt encode call
2022-04-11 12:19:41 +02:00
Leo Alt
bef69b595b
Ignore cex in SMT test
2022-02-28 18:56:20 +01:00
Leo Alt
098a3cb537
adjust tests for nondeterminism
2022-01-12 18:43:18 +01:00
Daniel Kirchner
1655626e0a
Remove counterexample from test.
2022-01-12 17:58:05 +01:00
Leo Alt
9f171c0f06
update smtchecker tests for new z3
2022-01-12 15:13:34 +01:00
Leo Alt
fb8c138b8b
Do not analyze unecessary contracts
2021-12-24 19:36:32 +01:00
Marenz
7a96953e78
Implement typechecked abi.encodeCall()
2021-12-16 17:35:58 +01:00
Leo Alt
316be7206f
Fix soundness of storage/memory pointers that were not erasing enough knowledge
2021-12-14 12:02:18 +01:00
Leo Alt
16535aae32
Fix ICE when unsafe targets are solved more than once and the cex is different
2021-12-03 00:21:38 +01:00
Leo Alt
a2588533e5
macos nondeterminism
2021-11-24 20:41:22 +01:00
Leo Alt
0c34d9df88
Adjust tests for nondeterminism
2021-11-24 20:41:22 +01:00
Leo Alt
ff5c842d67
update smtchecker tests
2021-11-24 20:41:22 +01:00
Leo Alt
dff280cadc
Fix ICE in CHC when using gas in the function options
2021-11-03 15:40:54 +01:00
Leo Alt
e40cf92b1d
[SMTChecker] Merge all entry points for a target
2021-11-03 11:12:58 +01:00
Leo Alt
38b0cf7f9c
SMTChecker tests
2021-10-26 11:30:30 +02:00
Leo Alt
4c2b661eaa
[SMTChecker] Report values for block, msg and tx variables in counterexamples
2021-10-05 15:19:10 +02:00
Leo Alt
d81ebe97c3
Fix magic access
2021-10-01 12:57:06 +02:00
Leo Alt
d25fb29178
Add isoltest option to ignore OS
2021-10-01 12:45:36 +02:00
Leo Alt
e74f853c6b
[SMTChecker] Support user types
2021-09-21 13:23:17 +02:00
Leo Alt
a1bea368cb
[SMTChecker] Support constants via modules
2021-09-16 14:35:05 +02:00
Leo Alt
b731957e65
Fix BMCs constraints on internal functions
2021-09-15 14:42:39 +02:00
Leo Alt
d91f75deb8
Fix ICE on unique errors
2021-09-09 16:37:43 +02:00
Leo Alt
6e2fe1e340
[SMTChecker] Cleanup spurious messages about TypeTypes
2021-09-07 16:55:25 +02:00
