cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
19,994 Commits 348 Branches 121 Tags 100 MiB
17f522835f
Commit Graph

625 Commits

Author SHA1 Message Date
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
Leonardo Alt
fa7c9a0dc6 Simplify internal function calls 2020-09-28 15:31:15 +02:00
Leonardo Alt
3519b38055 Move predicate functions from CHC to PredicateInstance 2020-09-28 12:43:19 +02:00
Leonardo Alt
ac93ee1d08 Move error flag from CHC to SymbolicState 2020-09-28 12:37:57 +02:00
Leonardo Alt
e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00
Alex Beregszaszi
9f3d5d3e2f [SMTChecker] Implement support for memory allocation 2020-09-25 15:56:24 +01:00
Alex Beregszaszi
9c1b041dcb [SMTChecker] Keep constraints of string literals after assignment 2020-09-25 11:32:48 +01:00
Alex Beregszaszi
5090353a1a [SMTChecker] Keep knowledge about string literals 2020-09-25 11:32:23 +01:00
Leonardo
57e1b2cb92
Merge pull request #9881 from ethereum/smt_fixed_bytes_index_access 
[SMTChecker] Support fixed bytes index access
 2020-09-25 11:32:56 +02:00
Leonardo Alt
df8c6d94e3 [SMTChecker] Support fixed bytes index access 2020-09-25 09:59:38 +02:00
Alex Beregszaszi
6edfdff187 [SMTChecker] Do not warn on "abi" as an identifer 
There is an approprate warning for the function call.
 2020-09-24 13:57:42 +01:00
Đorđe Mijović
858b4507e2
Merge pull request #9854 from ethereum/bitwiseSmt 
[SMTChecker] Support compound shifts and bitwise and, or, and xor
 2020-09-23 12:35:48 +02:00
Djordje Mijovic
79f550dba9 [SMTChecker] Supporting compound shift operators. 2020-09-23 11:31:37 +02:00
Djordje Mijovic
773e000227 [SMTChecker] Implementing compound bitwise And/Or/Xor operators 2020-09-23 11:31:37 +02:00
Alex Beregszaszi
709d25bd3d [SMTChecker] Support address type conversion with literals 2020-09-22 18:49:11 +01:00
chriseth
6e2d2feb10 Small fixes wrt ReasoningBasedSimplifier. 2020-09-16 18:08:54 +02:00
Alex Beregszaszi
c8c17b693b [SMTChecker] Support events and low-level logs 2020-09-16 11:50:39 +02:00
chriseth
adccc0608d
Merge pull request #9736 from ethereum/yul_smt 
Reasoning based optimizer using integers only
 2020-09-15 18:45:55 +02:00
Leonardo Alt
d87e15e2cd Refactor CHC sorts 2020-09-15 16:45:50 +02:00
chriseth
f73fb726af Reasoning based optimizer. 2020-09-15 15:57:58 +02:00
Alex Beregszaszi
783d66c1a4 [SMTChecker] Support revert() 2020-09-15 11:46:33 +01:00
Alex Beregszaszi
9aa9962f71 Add ContractDefinition::interfaceId() helper 2020-09-14 20:34:52 +01:00
Alex Beregszaszi
83934254ea [SMTChecker] Support type(I).interfaceId 2020-09-14 20:34:52 +01:00
Leonardo
31b5102aa0
Merge pull request #9731 from ethereum/smt_import 
[SMTChecker] Fix CHC encoding
 2020-09-12 00:56:04 +02:00
Alex Beregszaszi
961a199cf5 [SMTChecker] Support type(T).min and type(T).max 2020-09-11 21:37:51 +01:00
Leonardo Alt
23ee011c56 [SMTChecker] Fix imports 2020-09-11 13:34:46 +02:00
Leonardo Alt
40197df104 [SMTChecker] Support shifts 2020-09-09 19:47:52 +02:00
Leonardo Alt
00f6b303b1 [SMTChecker] Change warning message 2020-09-09 16:14:21 +02:00
Leonardo Alt
7b3cd019d4 Make recursive structs unsupported 2020-09-03 15:19:33 +02:00
Leonardo Alt
bd0c46abf5 Remove unreachable/redundant error messages 2020-09-03 15:19:03 +02:00
Leonardo Alt
e61b731647 [SMTChecker] Support structs 2020-09-03 15:19:03 +02:00
Leonardo
0d83977d5a
Merge pull request #9648 from ethereum/smt_refactor_predicates 
[SMTChecker] Refactor CHC predicates
 2020-09-01 20:38:47 +02:00
Leonardo Alt
49d3804de4 [SMTChecker] Fix rational number short circuit 2020-09-01 17:21:13 +02:00
Leonardo Alt
a3b6019131 Move post input and post output filtering from CHC to Predicate 2020-09-01 16:10:12 +02:00
Leonardo Alt
2e2e96cc93 Move state model filtering from CHC to Predicate 2020-09-01 16:10:12 +02:00
Leonardo Alt
e3a8c94ace Move formatFunctionCallCounterexample from CHC to Predicate 2020-09-01 16:10:11 +02:00
Leonardo Alt
5bbb20d3cb Move stateVariablesIncludingInheritedAndPrivate from CHC to SMTEncoder 2020-09-01 16:09:57 +02:00
Leonardo Alt
016b9b83a8 Refactor predicates 2020-09-01 16:09:56 +02:00
Leonardo Alt
238b8a929e [SMTChecker] Fix ICE on tuples of one element that actually have tuple type 2020-09-01 08:31:57 +02:00
Leonardo Alt
5cafbeebec [SMTChecker] Fix ICE on tuple assignment 2020-09-01 08:29:01 +02:00
Leonardo Alt
50e0ada77d [SMTChecker] Fix unary operator on lvalue tuple 2020-09-01 08:25:06 +02:00
Leonardo Alt
8c05db88c0 [SMTChecker] Fix soundness of array pop 2020-08-31 12:11:33 +02:00
Djordje Mijovic
11a7763f49 [SMTChecker] Support bitwise or, xor and not. 2020-08-26 11:06:56 +02:00
Đorđe Mijović
4dd25f7302
Merge pull request #9639 from ethereum/smtConditionalSupport 
[SMTChecker] Supporting conditional operator
 2020-08-21 14:25:47 +02:00
Djordje Mijovic
3f97a1012a [SMTChecker] Supporting conditional operator 2020-08-20 21:39:35 +02:00
chriseth
4dc63875f9
Merge pull request #9113 from ethereum/smt_chc_overflow 
[SMTChecker] Add underflow/overflow target to CHC
 2020-08-20 13:17:00 +02:00
Leonardo Alt
8a06041bbe [SMTChecker] Add underflow/overflow target to CHC 2020-08-14 12:58:27 +02:00
Jason Cobb
888d7037cd
Make FunctionCallAnnotation::kind a SetOnce 2020-08-12 11:57:01 -04:00
Leonardo Alt
ec31d971e6 [SMTChecker] Fix tuple name for arrays 2020-08-07 12:28:10 +02:00
Leonardo Alt
8df8c6e14f [SMTChecker] Fix ICE in BMC function inlining 2020-08-05 11:47:25 +02:00
Leonardo Alt
ad1798b000 [SMTChecker] Fix ICE on fixed bytes access 2020-07-28 17:59:42 +02:00
chriseth
9605b85c21
Merge pull request #9352 from ethereum/smt_cex 
[SMTChecker] CHC counterexamples
 2020-07-27 19:21:04 +02:00
Leonardo Alt
b207222af7 Fix extra parens 2020-07-27 17:14:59 +02:00
Leonardo Alt
de4ae301c4 [SMTChecker] Fix ICE when tuples have extra effectless parens 2020-07-27 13:03:27 +02:00
Leonardo Alt
d5f00842d9 cex2dot debug 2020-07-23 18:49:03 +02:00
Leonardo Alt
5bb4e73693 Review 1 2020-07-23 18:49:03 +02:00
Leonardo Alt
51721c3080 Double SAT run for cex 2020-07-23 18:49:03 +02:00
Leonardo Alt
694ec92688 Generate counterexample message based on cex graph 2020-07-23 18:49:03 +02:00
Leonardo Alt
744905525f Convert z3 cex graph into STL 2020-07-23 18:49:03 +02:00
Leonardo Alt
a7a069c74a Refactor constructor exit 2020-07-23 18:49:03 +02:00
Leonardo Alt
9d2a0947e9 Fix 1-tuple chain 2020-07-23 13:46:41 +02:00
Leonardo Alt
2c93278719 Fix push().push() 2020-07-20 17:17:35 +02:00
Sachin Grover
b7adb2aa42 Add SPDX license identifier if not present already in source file 
Fixes: #9220
 2020-07-17 20:24:12 +05:30
Leonardo Alt
672633af0a [SMTChecker] Fix ICE on compound assignment to array index 2020-07-16 17:44:10 +02:00
Leonardo Alt
46653b2d43 Fix ICE when bitwise operator on fixed bytes 2020-07-15 19:32:15 +02:00
chriseth
b3566ad0d5
Merge pull request #9082 from ethereum/conversionWarnings 
Adding `-Wsign-conversion` flag and fixing errors
 2020-07-13 11:28:09 +02:00
Leonardo Alt
88030c6568 [SMTChecker] Refactor verification targets 2020-07-10 10:28:49 +02:00
Alex Beregszaszi
a0300835eb Change CHC to avoid sign mismatch 2020-07-09 17:22:52 +02:00
Djordje Mijovic
547590b972 Fixing additional signedness errors after adding -Wsign-conversion flag 
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
 2020-07-09 17:22:45 +02:00
Leonardo Alt
f97fa9b520 [SMTChecker] Add current input variables to the function summary 2020-07-02 15:30:29 +02:00
Leonardo Alt
5517e817d5 Do not trust code of external functions 2020-07-01 18:20:46 +02:00
Leonardo Alt
56e7d43384 Rename var 2020-07-01 18:20:34 +02:00
Leonardo Alt
5160f89c1b [SMTChecker] Support to external calls to unknown code 2020-07-01 18:20:33 +02:00
Leonardo Alt
3c4e286390 [SMTChecker] Replace wrap mod by slack vars 2020-06-12 14:57:21 +02:00
Djordje Mijovic
c6e4943089 Adding fixes for signedness warnings in libsolidity 
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
 2020-06-10 10:41:55 +02:00
Leonardo Alt
f49e2424b2 [SMTChecker] Erase knowledge when array variable is pushed 2020-06-08 10:23:06 +02:00
Leonardo
d243f5baac
Merge pull request #9045 from ethereum/smt_fix_tuple 
[SMTChecker] Fix internal error in tuples of tuples.
 2020-06-05 14:21:32 +02:00
Leonardo
731e6466a0
Merge pull request #9067 from ethereum/smt_fix_fp_again 
[SMTChecker] Fix BMC targets with FP
 2020-06-05 12:39:28 +02:00
Leonardo Alt
87ceb72b82 [SMTChecker] Fix internal error in tuples of tuples. 2020-06-05 12:20:47 +02:00
Leonardo Alt
10162016ae [SMTChecker] Fix internal error on try/catch 2020-06-02 16:51:53 +02:00
Leonardo
97cb091ada
Merge pull request #9068 from ethereum/smt_fix_state_var_init_call 
[SMTChecker] Relax assertion about callstack
 2020-06-02 15:53:14 +02:00
Leonardo Alt
ede39fc2da [SMTChecker] Relax assertion about callstack 2020-06-02 12:50:51 +02:00
Leonardo Alt
2128ff9f13 Fix ICE on push for member access 2020-05-29 19:13:27 +02:00
Leonardo Alt
e5d25692a5 [SMTChecker] Fix BMC targets with FP 2020-05-29 18:13:13 +02:00
Leonardo Alt
b90fb1cab6 [SMTChecker] Fix ICE on index access assignment inside single branches 2020-05-28 15:56:46 +02:00