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
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
Kamil Śliwak
5b5e853ea0
Warn about missing user-defined operator support in SMTChecker
2023-02-22 00:39:25 +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
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
wechman
64a4f32bc2
Consistent terminology for attached/bound functions
2022-12-07 19:31:41 +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
24df40de9a
Allow running Eldarica from the command line
2022-11-22 21:16:45 +01:00
Marenz
f7cc29bec1
Add std:: qualifier to move() calls
2022-08-30 11:12:15 +02:00
Leo Alt
75d08ea924
Check early if solvers are available.
2022-05-11 20:02:31 +02:00
Leo Alt
f9fa76c9d3
smt encode call
2022-04-11 12:19:41 +02:00
Daniel Kirchner
0f1a63c3fa
Fix import directive visits in type checker and view pure checker.
2022-03-14 14:53:06 +01:00
Tyler
047034544e
Merge branch 'develop' of github.com:tfire/solidity into fix/remove-namespace-ast-annotations
2022-03-09 18:55:22 -05:00
Tyler
519e1c9402
Specify namespaces
...
Fix references into solidity::util
2022-03-08 00:09:17 -05:00
wechman
52dfccca98
Replace all locale-dependent operations with locale-agnostic counterparts
2022-03-07 17:23:08 +01:00
nishant-sachdeva
cc6344c03c
Changed instaces of isByteArrayOrString() to isByteArray() where it's only supposed to return a True for Bytes Type
2022-02-02 17:05:26 +05:30
nishant-sachdeva
9043621747
Changed occurences of isByteArray() to isByteArrayOrString(). The idea
...
is to, in a future commit, replace such occurences of
isByteArrayOrString() which are required to return True only for Bytes
type with a new isByteArray() function.
2022-02-02 14:19:58 +05:30
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
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
37215ffcfd
Add SMTCheckerTest isoltest option to ignore invariants
2021-10-26 11:30:30 +02:00
Leo Alt
d419c30ca6
Add errorCode list to invariants report
2021-10-26 11:30:30 +02:00
Leo Alt
49e7627bd3
Use invariants in CHC
2021-10-26 11:30:30 +02:00
Leo Alt
bc90533c93
Add invariants to ModelCheckerSettings
2021-10-26 11:30:30 +02:00
Leo Alt
d554824f70
Add Invariants which traverses the proof and collects invariants for the given predicates
2021-10-26 11:30:30 +02:00
Leo Alt
9bcd2c18e4
Add expression substitution to Predicate
2021-10-26 11:30:30 +02:00
Leo Alt
ce72d7cd26
Add ExpressionFormatter which translates an smtutil::Expression into a Solidity-like expression string
2021-10-26 11:30:30 +02:00
tcoyvwac
ba0c09e082
Prefer make_unique over new
2021-10-15 19:46:47 +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
chriseth
1531863835
Split Common.h into Numeric.h.
2021-09-23 15:27:29 +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
6e2fe1e340
[SMTChecker] Cleanup spurious messages about TypeTypes
2021-09-07 16:55:25 +02:00
Leo Alt
106c591dde
Support the external call option
2021-09-01 20:18:37 +02:00
Marenz
2b28f87abf
Add type().min/max for enums
2021-09-01 15:02:02 +02:00
Leo Alt
ac528cfd1b
add static array length constraint
2021-08-30 17:15:16 +02:00
Leo Alt
16bc15acac
Fix false negative on storage array references returned by internal functions
2021-08-28 09:30:53 +02:00
Leo Alt
60b866f9d8
Fix ICE on multi-source use of abi.*
2021-08-27 18:55:36 +02:00
Leo Alt
8e81df1bd3
Do not show redundant unsupported errors in SMTChecker
2021-08-27 16:25:09 +02:00
Martin Blicha
Leo Alt
Kamil Śliwak
wechman
Marenz
Tyler
nishant-sachdeva
tcoyvwac
chriseth