Martin Blicha
98446782e2
[SMTChecker] Fix compound assignment to push
2021-03-24 14:54:13 +01:00
Martin Blicha
852e877ae7
[SMTChecker] Handle InaccessibleDynamicType
2021-03-24 11:53:06 +01:00
Mathias Baumann
e197ebbdd1
Replace TypePointer
with Type const*
2021-03-23 11:47:19 +01:00
Leonardo
25b31111df
Merge pull request #11040 from ethereum/smt_fix_virtual_one_more_time
...
[SMTChecker] Fix bug in virtual functions called by constructor
2021-03-17 16:54:36 +01:00
Martin Blicha
432944d0b4
[SMTChecker] Small refactoring of defining SMT expressions for structs/tuples
2021-03-16 15:34:43 +01:00
Martin Blicha
2f52affcc2
[SMTChecker] Correctly resolve current scope contract in VariableUsage.
2021-03-15 13:55:14 +01:00
Martin Blicha
6aa6c5f5f9
[SMTChecker] Reset reference variables on assignment to a variable of reference type
2021-03-12 19:51:31 +01:00
Leonardo Alt
998346e599
Fix bug in virtual functions called by constructor.
2021-03-12 16:42:28 +01:00
Martin Blicha
0cb75293f9
[SMTChecker] fix handling of assignments of array/mapping state variable accessed using contract name
2021-03-12 14:01:07 +01:00
Leonardo Alt
6fd76e830d
Fix CHC cex order
2021-03-11 10:36:40 +01:00
Martin Blicha
4285c2803b
[SMTChecker] Fix ICE on array.pop nested inside 1-tuple
2021-03-09 20:00:51 +01:00
Martin Blicha
5af01f6896
[SMTChecker] Use same sort name for array slice as for the underlying array.
2021-03-09 11:06:22 +01:00
Martin Blicha
385a664f3c
[SMTChecker] Fix public getter for array of structs.
2021-03-08 17:34:20 +01:00
Martin Blicha
0340510c53
[SMTChecker] correct handling of FixedBytes constants initialized with string literal
2021-03-04 15:14:47 +01:00
Martin Blicha
41fc59f00f
[SMTChecker] Ensure that push to a string casted to bytes is registered in the original string
2021-03-03 17:11:42 +01:00
Martin Blicha
41a01de664
[SMTChecker] fix crash on push to string casted to bytes
2021-03-03 15:25:32 +01:00
Alexander Arlt
ae6996efc1
Fix issue with pop on storage array.
2021-02-23 14:26:55 +01:00
Leonardo
7405dc5b7f
Merge pull request #10836 from ethereum/smt_fix_cex_inheritance
...
Fix inheritance bug in CHC cex
2021-02-03 18:49:25 +01:00
Martin Blicha
d99256aae7
[SMTChecker] refactoring of resetting storage variables
2021-02-03 15:53:58 +01:00
Martin Blicha
f1013427a7
[SMTChecker] refactoring the accessing the encoding state
2021-02-03 15:53:58 +01:00
Leonardo Alt
665ce27c18
Fix inheritance bug in CHC cex
2021-02-02 18:06:32 +01:00
Martin Blicha
a49950cdf3
[SMTChecker] Added transaction constraints also for contract deployment
2021-02-01 16:46:34 +01:00
Leonardo Alt
545305a31f
[SMTChecker] Fix super and virtual
2021-01-28 18:51:29 +01:00
Martin Blicha
deb90d84a6
[SMTChecker] added missing type constraints for Address
2021-01-27 20:39:24 +01:00
Martin Blicha
484e67815a
[SMTChecker] Basic support for inline assembly using over-approximating analysis
2021-01-26 16:20:50 +01:00
Leonardo Alt
a612daa783
Add msgvalue to cex
2021-01-21 19:05:44 +01:00
Leonardo Alt
3b23cadbdc
Add CLI and JSON option to select SMTChecker targets
2021-01-20 17:35:37 +01:00
Martin Blicha
35d228d9b6
[SMTChecker] Gather local variables also from nested try/catch clauses
2021-01-18 18:30:18 +01:00
Leonardo Alt
c7ca87c012
Fix static virtual resolution
2021-01-18 16:23:38 +01:00
Martin Blicha
18214d1ccc
[SMTChecker] Reset checked/unchecked flag to the default value when inlining function in BMC
2021-01-15 15:36:26 +01:00
Leonardo Alt
007d39871b
[SMTChecker] Synthesize untrusted functions called externally
2021-01-15 11:56:26 +01:00
Martin Blicha
504e4c22b2
[SMTChecker] Fix in abi handling - tuple expression of size 1 has the type of the member and not TupleType
2021-01-14 14:53:56 +01:00
Martin Blicha
b4d2a71eec
[SMTChecker] Fix in abi handling - fixed missing type conversion
2021-01-14 14:53:44 +01:00
Martin Blicha
32a923c7ef
[SMTChecker] Fix in abi handling - abstracting expressions of type Function inside ABI functions when translating to SMT
2021-01-14 14:53:22 +01:00
Martin Blicha
5e13744423
[SMTChecker] Fixed pushing string literal to bytes array
2021-01-13 16:30:50 +01:00
Martin Blicha
7c6340fe4f
[SMTChecker] Refactoring expression to tuple assignment
2021-01-12 17:15:14 +01:00
Leonardo Alt
b3c3836388
Output internal calls
2021-01-12 14:57:04 +01:00
Leonardo Alt
f1ae24abc7
Remove extra line breaks
2021-01-12 14:00:07 +01:00
Martin Blicha
ff76c989ac
addressing review comments
2021-01-11 14:19:06 +01:00
Martin Blicha
dd43ce1578
fixing try/catch encoding for BMC, refactoring
2021-01-11 13:36:03 +01:00
Martin Blicha
55589a9eec
[SMTChecker] Basic support for try-catch in BMC
2021-01-11 13:36:02 +01:00
Martin Blicha
0f3924186e
[SMTChecker] Support try-catch in CHC engine
2021-01-11 13:36:02 +01:00
Leonardo Alt
11f56861c3
Refactor cex loop
2021-01-07 23:13:02 +01:00
Leonardo Alt
b02722ebda
Add contract name to called function in cex
2021-01-04 10:03:16 +01:00
Leonardo Alt
78d55e6b4a
[SMTChecker] Support check/unchecked
2020-12-30 12:14:30 +01:00
Martin Blicha
be0a0f4d90
[SMTChecker] Added constraints for block properties
2020-12-29 22:17:44 +01:00
Leonardo Alt
9482e7de23
[SMTChecker] Fix calls to virtual/overriden functions
2020-12-29 11:25:20 +01:00
Martin Blicha
bb0003f5ea
removed extra parameter from PredicateInstance::nondetInterface
2020-12-28 19:48:48 +01:00
Martin Blicha
f76ff35225
[SMTChecker] Detect errors caused by reentrancy
2020-12-28 14:32:53 +01:00
Martin Blicha
d90b9da4f0
[SMTChecker] Refactoring
2020-12-22 13:10:48 +01:00
Martin Blicha
87ef0e16f5
[SMTChecker] Fix virtual modifier called statically
2020-12-21 13:52:28 +01:00
Leonardo Alt
034d1ab90f
[SMTChecker] Replace constants by their value in-place
2020-12-18 14:22:28 +01:00
Martin Blicha
7078e8f8f8
[SMTChecker] Fix analysis of overriding modifiers
2020-12-17 17:05:54 +01:00
Leonardo Alt
2cbf33ca1c
SMTChecker support ABI functions as UFs
2020-12-17 14:03:17 +01:00
Leonardo Alt
f5c96ea6da
Fix constant evaluation build
2020-12-16 17:59:00 +01:00
chriseth
3a23df6717
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-16 16:56:45 +01:00
Leonardo Alt
80e85b772b
[SMTChecker] Apply const eval to arithmetic binary expressions
2020-12-16 14:58:00 +01:00
chriseth
ffaf40950a
Merge pull request #10605 from ethereum/develop
...
Merge develop into breaking.
2020-12-15 14:01:01 +01:00
Martin Blicha
e2c27b8ea4
[SMTChecker] Fix internal error on constructor of a recursive struct
2020-12-15 09:53:52 +01:00
Martin Blicha
71f835b71b
[SMTChecker] Fixed internal error when increment/decrement is applied on a result of push().
2020-12-14 22:52:44 +01:00
Martin Blicha
103fa3b7eb
[SMTChecker] Fix internal error on abstract modifier
2020-12-14 18:23:25 +01:00
Martin Blicha
27402781c4
[SMTChecker] Fixed crash on push to bytes on lhs of an assignment
2020-12-14 17:40:45 +01:00
Martin Blicha
0be325dc0d
[SMTChecker] Fix handling of function calls where the function identifier is nested in a tuple.
2020-12-14 16:19:24 +01:00
chriseth
561280a5cc
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-14 11:33:40 +01:00
Martin Blicha
8927015e5a
[SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine
2020-12-11 17:41:50 +01:00
Alex Beregszaszi
bd641a5206
Enable more C++ compiler warnings
2020-12-10 21:03:58 +00:00
Daniel Kirchner
c400c61fc3
Fix incorrect behaviour on clang 6.
2020-12-10 17:20:30 +01:00
chriseth
d0551b67d7
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-10 17:07:56 +01:00
Daniel Kirchner
7308abc084
Allow loading Z3 dynamically at runtime.
2020-12-10 16:47:47 +01:00
chriseth
482bda6887
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-10 12:15:52 +01:00
Leonardo Alt
3c142e0e94
Move CHC counterexamples to primary location
2020-12-09 19:55:18 +01:00
Leonardo Alt
a961a76263
Do not run SMTChecker when file level functions/constants are present.
2020-12-09 12:18:55 +01:00
chriseth
806453aca9
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-08 21:00:09 +01:00
chriseth
b045195c1e
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-08 17:42:31 +01:00
Martin Blicha
eb356735f6
[SMTChecker] Adding support for reporting values of structs in CEX in CHC engine.
2020-12-08 16:40:28 +01:00
Martin Blicha
0ebab439be
removing assert that is not always true
2020-12-08 12:27:59 +01:00
Martin Blicha
ff0c794674
[SMTChecker] Fixing conversion from StringLiteral to FixedBytes
2020-12-07 19:30:51 +01:00
Leonardo Alt
b7ac207391
[SMTChecker] Support return in CHC
2020-12-07 18:17:33 +01:00
chriseth
bff7254d9e
Fix merge conflict.
2020-12-07 13:30:09 +01:00
chriseth
329b8f2a60
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-07 13:04:14 +01:00
Leonardo Alt
7490ffbe13
Use nonlinear clauses instead of inlining for base constructors
2020-12-04 13:25:56 +01:00
chriseth
d56a7bb89e
Merge pull request #10489 from ethereum/develop
...
Merge develop into breaking.
2020-12-03 18:11:12 +01:00
Leonardo
088b694f0b
Merge pull request #10207 from ethereum/smt_tests_asserts
...
[SMTChecker] Add uncovered test and replace uncovered tests by asserts
2020-12-03 08:59:48 +01:00
Martin Blicha
2ee633f404
[SMTChecker] Added support for public getters through this.
2020-12-02 16:06:48 +01:00
chriseth
6de7eaba95
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-01 10:50:13 +01:00
Leonardo Alt
fa561dbd0e
Add uncovered test and replace uncovered tests by asserts
2020-11-30 18:46:47 +01:00
Martin Blicha
cd06d68cbe
[SMTChecker] Keeping better track of path condition through branches with return statement in the BMC engine.
2020-11-30 11:47:49 +01:00
chriseth
18de8a56c9
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-26 11:48:53 +01:00
Djordje Mijovic
26c43cfc66
[SMTChecker] Fix SMT logic error when doing compound assignment with string literlas.
2020-11-24 19:14:15 +01:00
chriseth
253889cbf1
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-24 16:22:03 +01:00
Leonardo Alt
68cfa0a901
Fix spelling in SMTChecker comment
2020-11-23 19:40:29 +01:00
chriseth
a0a02f2307
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-23 19:28:08 +01:00
Martin Blicha
66125b79d6
[SMTChecker] Do not report warning when encountered a Type identifier. The operations are supported now.
2020-11-23 15:41:57 +01:00
Martin Blicha
80d743426f
[SMTChecker] Added support for struct constructor.
2020-11-23 13:45:17 +01:00
Leonardo
61069ec77d
Merge pull request #10355 from blishko/smtchecker-refactoring
...
[SMTChecker] Small refactoring of assignments to provide a common low-level point for model checking engines to hook into.
2020-11-20 14:31:32 -01:00
Leonardo Alt
e4339b0526
[SMTChecker] Support named arguments in function calls
2020-11-20 11:52:26 -01:00
Martin Blicha
fbcb572d69
[SMTChecker] Small refactoring of assignments to provide a common low-level point for model checker engines to hook into.
2020-11-19 22:03:08 +01:00
chriseth
e8a278eefa
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-17 18:51:57 +01:00
Martin Blicha
07427c798c
[SMTChecker] Adding a dummy frame to the call stack for the implicit constructor
2020-11-16 22:46:17 +01:00
Martin Blicha
5ca7a24896
[SMTChecker] Added support for precise modeling of external calls to this
.
...
Modeling external calls to this, since we can trust these calls.
fixed problem with transaction data not being restored after trusted external call
update to the tests
additional tests
changelog entry
added tests for external getters of this
2020-11-13 11:49:09 +01:00
chriseth
14ed67ac4b
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-11 20:33:40 +01:00
Alex Beregszaszi
2f899bbffa
[SMTChecker] Avoid implicit conversion
2020-11-11 16:29:03 +00:00
chriseth
da92fe548e
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-10 13:48:32 +01:00
Leonardo
25b2a38d8b
Merge pull request #10202 from ethereum/smt_fix_modifiers_branches
...
[SMTChecker] Fix CHC false positives when using branches inside modifiers
2020-11-09 16:42:30 +00:00
chriseth
04195439b7
Merge remote-tracking branch 'origin/develop' into HEAD
2020-11-09 14:28:05 +01:00
Leonardo Alt
00858c0ccf
Isoltets SMTChecker option and BMC specific tests
2020-11-06 15:03:38 +00:00
Leonardo Alt
89dce24f24
Force SMT variable creation order
2020-11-06 11:51:01 +00:00
Leonardo Alt
646be53f2f
Sort variables and expressions by AST id
2020-11-06 11:50:43 +00:00
Leonardo Alt
1dbd8f8d67
Fix CHC false positives when using branches inside modifiers
2020-11-04 21:47:07 +00:00
Leonardo
62535c2fd4
Merge pull request #10181 from ethereum/smt_user_timeout
...
[SMTChecker] User timeout option
2020-11-04 10:55:28 +00:00
Leonardo Alt
daf859c15b
[SMTChecker] report SMTEncoder warnings also via CHC
2020-11-03 16:06:17 +00:00
chriseth
5ffee049fa
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-03 14:05:14 +01:00
Leonardo Alt
d03ddeb0fa
[SMTChecker] User timeout option
2020-11-03 10:46:11 +00:00
Leonardo Alt
e38d0db683
[SMTChecker] Fix internal error when array.push() is used as LHS of assignment
2020-11-02 13:32:53 +00:00
Leonardo Alt
94e2506132
Fix inherited state vars for BMC
2020-11-02 11:42:39 +00:00
Martin Blicha
c1a57ffbfe
[SMTChecker] More precise creation of verification targets.
2020-10-30 19:11:28 +01:00
chriseth
e93a84ccd4
Merge remote-tracking branch 'origin/develop' into HEAD
2020-10-28 18:19:31 +01:00
Đorđe Mijović
1f50b86aad
Merge pull request #10073 from ethereum/smt_format_array_cex
...
Format array cex
2020-10-28 12:39:19 +01:00
Leonardo Alt
25f75ce547
Remove nondet tests
2020-10-28 11:03:42 +00:00
Leonardo
07c454949f
Merge pull request #10127 from ethereum/fixIceSmtBitwise
...
[SMTChecker] Fix ICE when using >>>
2020-10-28 09:28:18 +00:00
Djordje Mijovic
9cc37c3fa4
[SMTChecker] Fix ICE when using >>>
2020-10-28 09:25:14 +01:00
Leonardo Alt
f2f84a7f97
Format array cex
2020-10-27 16:32:43 +00:00
Leonardo Alt
446e46fe06
Use Expression instead of plain strings for counterexamples
2020-10-27 12:04:51 +00:00
Leonardo Alt
4755cfe157
Fix assignment to contract member access
2020-10-26 14:39:02 +00:00
Leonardo Alt
d3d77e482c
Fix ICE on conditions with tuples of rationals
2020-10-23 14:47:53 +01:00
chriseth
20f39ab6e9
Merge pull request #10097 from ethereum/develop
...
Merge develop into breaking.
2020-10-23 10:30:24 +02:00
chriseth
bfc8e26007
Remove low-level log functions.
2020-10-22 17:50:14 +02:00
Martin Blicha
ade3b9951c
[SMTChecker] Added support for selector when expression's value is known at compile time
2020-10-22 14:18:52 +02:00
Leonardo Alt
b087fa9750
[SMTChecker] Fix ICE implicit conversion string literal -> byte
2020-10-21 22:03:01 +01:00
Martin Blicha
f0d81601db
[SMTChecker] Adding division by zero checks in the CHC engine
2020-10-21 14:48:33 +02:00
Leonardo Alt
cf35785328
Add unknown message to all verification targets
2020-10-19 20:54:13 +01:00
chriseth
6979952995
Merge remote-tracking branch 'origin/develop' into HEAD
2020-10-19 18:02:50 +02:00
Leonardo
a097f9f124
Merge pull request #10025 from ethereum/smt_crypto_functions
...
[SMTChecker] Support crypto functions in CHC
2020-10-16 16:40:29 +01:00
Leonardo
8d7bdcaba7
Merge pull request #10036 from ethereum/smt_cli_option
...
Add CLI option to choose model checker engine
2020-10-16 16:37:33 +01:00
Martin Blicha
78c8fbc7ce
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
Leonardo Alt
4e49135318
Add CLI option to choose model checker engine
2020-10-16 15:01:47 +01:00
Leonardo Alt
54f76e081a
[SMTChecker] Support crypto functions in CHC
2020-10-16 14:57:13 +01:00
chriseth
979d3062bc
Merge pull request #10033 from ethereum/develop
...
Merge develop into breaking
2020-10-14 14:12:20 +02:00
Leonardo Alt
440e5b3935
[SMTChecker] Fix counterexample state reporting
2020-10-13 22:18:43 +01:00
Leonardo Alt
aec456021d
Add tx constraints to CHC
2020-10-13 17:49:04 +01:00
Leonardo Alt
a2cdde1191
Add tx data to symbolic state
2020-10-13 17:49:04 +01:00
chriseth
f6e57a0eec
Merge pull request #10023 from ethereum/develop
...
Merge develop into breaking.
2020-10-13 18:18:53 +02:00
Mathias Baumann
006e5f2e1f
Allow path syntax for super constructor calls
2020-10-13 14:32:11 +02:00
Leonardo Alt
1e568d7dc6
[SMTChecker] Fix implicit constructor summary predicate
2020-10-13 09:38:58 +01:00
Djordje Mijovic
e23d8f5593
[SMTChecker] Supporting inline arrays.
2020-10-12 16:59:14 +02:00
Leonardo Alt
18cf01c187
Add this and state to CHC
2020-10-12 11:11:52 +01:00
Leonardo Alt
a86f656704
Refactor state as tuple
2020-10-12 11:11:52 +01:00
Alex Beregszaszi
fedbea46cd
[SMTChecker] Support type conversions
2020-10-02 10:26:02 +02:00
Leonardo Alt
c8cc73c80c
Support array slices
2020-10-01 11:52:02 +02:00
Leonardo Alt
352cce5fc8
[SMTChecker] Support addmod and mulmod.
2020-09-29 12:45:19 +02:00