cerc-io/solidity
16
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
23,135 Commits 348 Branches 121 Tags 100 MiB
2b70b08d5f
Commit Graph

698 Commits

Author SHA1 Message Date
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
Leonardo Alt
a73ec6a82f [SMTChecker] Fix ICE in inlining function calls while short circuiting 2020-05-28 13:14:19 +02:00
Leonardo Alt
cb1cbbc1f1 [SMTChecker] Fix fixed point inc/dec 2020-05-28 10:56:06 +02:00
Leonardo Alt
9e9f0c52e1 [SMTChecker] Support to bitwise 2020-05-27 20:59:00 +02:00
chriseth
9604174151 Rename asCallableFunction. 2020-05-26 11:35:12 +02:00
Leonardo Alt
7a91c9b971 Remove Type from SolverInterface 2020-05-20 12:55:19 +02:00
Leonardo Alt
45eba27424 Rename namespace 2020-05-20 12:55:18 +02:00
Leonardo Alt
087605ea02 Create libsmtutil 2020-05-20 12:55:18 +02:00
Leonardo Alt
2435ab938c Add verification target for empty pop 2020-05-18 16:35:56 +02:00
Leonardo Alt
d4d26c02e4 Assume that push will not overflow 2020-05-18 16:35:56 +02:00
Leonardo Alt
82db35e563 [SMTChecker] Support array push/pop 2020-05-18 16:33:34 +02:00
Leonardo Alt
a0c605aa85 [SMTChecker] Support array length 2020-05-14 23:32:29 +02:00
a3d4
7cae074b8a Add error IDs to BMC 2020-05-12 11:39:18 +02:00
Alex Beregszaszi
c31a93b3f2 Remove boost::filesystem where it is not needed 
A two uses in CommonIO remain for the compiler (plus testing/tools use it extensively)
 2020-05-11 11:19:11 +01:00
a3d4
8f68c04358 Add unique IDs to error reporting calls 2020-05-06 13:53:46 +02:00
Leonardo Alt
059d0bdebb Revert "Use Spacer option to improve performance of constant arrays" 
This reverts commit 92059fa848.
 2020-04-24 11:55:58 +02:00
hrkrshnn
e2e32d372f virtual modifiers (in Abstract contracts) allow empty bodies 2020-04-23 17:26:59 +05:30
Leonardo Alt
92059fa848 Use Spacer option to improve performance of constant arrays 2020-04-23 10:45:02 +02:00
Leonardo Alt
cfe3686116 Fix internal error when using array slices 2020-04-22 23:20:10 +02:00
Leonardo
6d98b907ef
Merge pull request #8746 from ethereum/smt_fix_fixed_point 
Fix ICE with fixed point
 2020-04-22 23:18:41 +02:00
Leonardo Alt
b191139f2a Fix undefined behavior with nullptr 2020-04-22 20:49:40 +02:00
Leonardo Alt
83c9e82099 Fix ICE with fixed point 2020-04-22 19:57:00 +02:00
chriseth
41ef13129b
Merge pull request #8678 from ethereum/smt_remove_redundant_constraints 
[SMTChecker] Remove redundant CHC constraints
 2020-04-20 15:44:59 +02:00
hrkrshnn
4760b8589d Replaced all instances of lValueRequested to willBeWrittenTo 2020-04-20 12:33:30 +05:30
Leonardo Alt
45f22e3ff4 Add functional map and fold generic functions 2020-04-16 19:21:36 +02:00
Leonardo Alt
bca43586c6 [SMTChecker] Remove redundant CHC constraints 2020-04-15 18:11:39 +02:00
Alexander Arlt
aac7a1e434 Apply modernize-pass-by-value. 2020-04-14 10:32:13 -05:00
Leonardo Alt
4fc9920112 Use tuple sort name plus index for field name 2020-04-09 12:59:57 +02:00
Leonardo Alt
5d9dd654cf [SMTChecker] Add and use tuple sort 2020-04-08 18:26:03 +02:00
chriseth
823a119117
Merge pull request #8570 from aarlt/clang-tidy-apply-modernize-use-emplace 
clang-tidy: Apply modernize-use-emplace.
 2020-04-07 17:28:50 +02:00
Leonardo Alt
e3ec22124e [SMTChecker] Fix ICE in CHC internal calls 2020-04-07 01:09:03 +02:00
Leonardo Alt
05a85461fe Symbolic state 2020-04-06 12:27:53 +02:00
Leonardo Alt
2cfa44bba3 Allow constructing symbolic arrays from smt sort 2020-04-06 10:50:00 +02:00
Alexander Arlt
90bb1d8a7c Apply modernize-use-emplace. 2020-04-02 17:35:48 -05:00
Leonardo Alt
d2f65ea8b1 [SMTChecker] Add SortProvider 2020-03-26 14:55:54 +01:00
Leonardo Alt
07368c2e1e Add support to internal function calls 2020-03-11 16:29:07 +01:00
Leonardo
32ca1a5e26
Merge pull request #8311 from ethereum/smt_split_2 
[SMTChecker] Change CHC encoding from explicit CFG to function forests
 2020-03-03 13:16:14 +01:00
Leonardo Alt
3bee348525 Change CHC encoding to functions forest instead of explicit CFG 2020-03-03 12:12:26 +01:00
Leonardo Alt
96a230af50 [SMTChecker] Fix ICEs with tuples 2020-03-03 11:35:58 +01:00
Leonardo Alt
d31a2a8d21 CHC clears indices so that initial is 0 and current is 1 2020-02-12 11:47:58 -03:00
Leonardo Alt
34d64761d9 Extract symbolicArguments function 2020-02-12 11:47:58 -03:00
Leonardo Alt
6451a4d2a0 Move VerificationTarget and add BMCVerificationTarget 2020-02-12 11:47:58 -03:00
Leonardo Alt
ba576bc6c3 Fix new namespaces 2020-02-12 10:35:44 -03:00
Leonardo Alt
a02308cfa5 Replace void cast by maybe_unused 2020-01-09 13:41:30 +01:00
Christian Parpart
345f9928ab Library libdevcore renamed to libsolutil. 2020-01-07 15:51:50 +01:00
Christian Parpart
6b23412fae C++ namespace cleanup (except tests). 2020-01-07 15:51:50 +01:00
Leonardo Alt
f4f83690f3 Replace some shared_ptr by unique_ptr or raw pointers 2020-01-06 14:16:49 +01:00
chriseth
f6916a637e Merge remote-tracking branch 'origin/develop' into develop_060 2019-12-09 17:16:58 +01:00
Leonardo Alt
225041738e Add SMTCheckerTest for isoltest 2019-12-09 15:32:08 +01:00
chriseth
e061f1e743 Merge remote-tracking branch 'origin/develop' into HEAD 2019-12-05 16:44:26 +01:00
Leonardo Alt
7be6b54fc7 Add comment 2019-12-04 17:31:44 +01:00
Leonardo Alt
48c3a5c225 [SMTChecker] Create options to choose SMT solver in runtime 2019-12-04 17:31:44 +01:00
chriseth
42d9a8e962 Merge remote-tracking branch 'origin/develop' into develop_060 2019-12-04 17:01:44 +01:00
Leonardo Alt
67d82fc8a7 [SMTChecker] Use rlimit instead of tlimit for SMT queries 2019-12-04 11:52:18 +01:00
chriseth
2f11ac3590 Merge remote-tracking branch 'origin/develop' into develop_060 2019-12-03 21:17:15 +01:00
chriseth
96d777d7f1 Merge commit 'a7d481fb9' into develop_060 2019-12-03 20:47:30 +01:00
Leonardo Alt
b1577f5e46 [SMTChecker] Fix ICE in array of structs type 2019-12-03 01:12:30 +01:00
Leonardo
a7d481fb94
Merge pull request #7851 from ethereum/smt_fix_function_type 
[SMTChecker] Fix ICE for arrays and mappings of functions.
 2019-11-30 13:15:08 +01:00
Leonardo
767ce4417f
Merge pull request #7850 from ethereum/smt_fix_typetype 
[SMTChecker] Fix visit to IndexAccess that has type Type
 2019-11-29 18:18:26 +01:00
Leonardo Alt
5adc2a40b9 [SMTChecker] Fix ICE for arrays and mappings of functions. 2019-11-29 18:06:44 +01:00
Leonardo Alt
9eda95caf9 [SMTChecker] Fix visit to IndexAccess that has type Type 2019-11-29 17:20:50 +01:00
Leonardo Alt
c09da092d2 [SMTChecker] Fix constructors with local vars 2019-11-29 16:59:15 +01:00
Leonardo Alt
a352abe00d [SMTChecker] Add support to constructors 2019-11-28 14:43:23 +01:00
chriseth
f7fc42d8c3
Merge pull request #7826 from ethereum/develop 
Merge develop into develop_060
 2019-11-28 13:37:19 +01:00
Leonardo Alt
240ff30878 [SMTChecker] Do not visit the name of a modifier invocation 2019-11-27 22:34:33 +01:00
Leonardo Alt
ddc478e3e4 Add CallbackKind and use it for the SMT solver 2019-11-21 22:10:21 +00:00
Erik K
94272d44aa
Merge pull request #7745 from ethereum/develop 
Merge develop into develop_060
 2019-11-19 15:30:31 +01:00
Leonardo Alt
d818746e0c [SMTChecker] Fix ICE in abi.decode 2019-11-18 13:15:10 +01:00
chriseth
216e1749f4 Merge remote-tracking branch 'origin/develop' into develop_060 2019-11-14 13:42:46 +01:00
Leonardo Alt
8efacfb545 [SMTChecker] Fix ICE in string literal to fixed bytes implicit conversion 2019-11-13 22:25:18 +01:00
Leonardo Alt
e3652627fd [SMTChecker] Fix ICE in CHC when function used as argument 2019-11-13 15:11:30 +01:00
chriseth
2e5a42836c
Merge pull request #7681 from ethereum/develop 
Merge develop into develop_060
 2019-11-11 16:42:03 +01:00
Leonardo Alt
5dacaf57bc Fix ICE in FixedBytes IndexAccess 2019-11-08 17:29:40 +01:00
Leonardo Alt
fc945880d1 [SMTChecker] Fix override tests 2019-11-07 11:49:32 +01:00
Leonardo Alt
6b10efff8c Add CHCSmtLib2Interface 2019-11-07 11:12:11 +01:00
chriseth
21e65076b3
Merge pull request #7650 from ethereum/develop 
Merge develop into develop_060
 2019-11-06 21:56:55 +01:00
Leonardo Alt
10e70b8603 [SMTChecker] Support inheritance and resolve overrides 2019-11-06 11:00:06 +01:00
chriseth
4d99bf68f4
Merge pull request #7638 from ethereum/develop 
Merge develop into develop_060
 2019-11-05 17:33:54 +01:00
Leonardo Alt
c5e081dc8c [SMTChecker] Refactor CHC loops and add if blocks 2019-11-05 09:28:59 +01:00
chriseth
46ac16d25c Merge remote-tracking branch 'origin/develop' into develop_060 2019-11-04 19:09:11 +01:00
Daniel Kirchner
3321fc56ea Split fallback function and introduce "fallback()" and "receive()" syntax. 2019-11-04 17:17:58 +01:00
Leonardo Alt
8a42e3f87a [SMTChecker] Support assignments to m-d arrays and mappings 2019-10-28 17:27:39 +01:00
Leonardo
ca714a2d3d
Merge pull request #7485 from ethereum/develop 
Merge develop into develop_060
 2019-09-26 15:43:12 +02:00
Leonardo Alt
83ef34f41d [SMTChecker] Fix SMT name for function identifiers 2019-09-24 11:23:10 +02:00
Leonardo Alt
ed9674be8d [SMTChecker] Add as const function to SMTLib2Interface 2019-09-18 22:57:14 +02:00
chriseth
5b3efee93b
Merge pull request #7442 from ethereum/develop 
Merge develop into develop_060
 2019-09-17 12:16:27 +02:00
Leonardo Alt
e1c238e25f [SMTChecker] Add loop support 2019-09-13 12:40:53 +02:00
Daniel Kirchner
4782c800ec Initial introduction of array slices with partial implementation for dynamic calldata arrays. 2019-09-13 10:57:53 +02:00
Leonardo Alt
a51577facf Fix Windows build 2019-09-02 22:37:30 +02:00
Leonardo Alt
a774b2d905 [SMTChecker] Zero-initialize arrays 2019-09-02 22:37:30 +02:00
Leonardo Alt
214e5c6369 [SMTChecker] Fix index access type type error 2019-08-27 16:39:19 +02:00
Leonardo Alt
1a70a46f9b [CHC] Add function blocks and check asserts 2019-08-15 12:25:15 +02:00
Leonardo
cbac3a4208
Merge pull request #7107 from ethereum/smt_chc_constructor_interface 
[SMTChecker] Add CHC constructor/interface/error blocks
 2019-08-12 15:06:08 +02:00
Leonardo Alt
bef6228810 [SMTChecker] Create CHC constructor/interface/error blocks 2019-08-12 12:34:57 +02:00
Leonardo Alt
360f868836 [SMTChecker] Fix literal string type mismatch 2019-08-10 21:51:46 +02:00
Leonardo Alt
4214cd1354 [SMTChecker] Fix ICE when reporting cex concerning state vars from different source files 2019-08-10 20:56:52 +02:00
Leonardo
67c855e93e
Merge pull request #7170 from ethereum/smt_fix_other_contract_state_var 
[SMTChecker] Fix ICE when inlining functions from different source
 2019-08-09 19:14:28 +02:00
Leonardo Alt
7b22496b1f [SMTChecker] Fix ICE when inlining functions that use state vars and are in a different source 2019-08-09 17:50:52 +02:00
Leonardo Alt
11d8cf588e [SMTChecker] Set unknown values for return variables of recursive functions 2019-08-09 17:01:08 +02:00
Leonardo Alt
369f8cd97f [SMTChecker] CHC create function return variables 2019-08-05 12:36:51 +02:00
Leonardo
11632966c9
Merge pull request #7171 from ethereum/smt_fix_compound_bitwise 
[SMTChecker] Fix ICE compound bitwise op inside branch
 2019-08-05 12:15:01 +02:00
Leonardo Alt
d5fb8cf58a [SMTChecker] Fix ICE compound bitwise op inside branch 2019-08-02 20:02:39 +02:00
Leonardo Alt
7b5863e583 Do not erase knowledge about storage pointers when another pointer is assigned 2019-08-02 13:09:06 +02:00
chriseth
04f298fd0e
Merge pull request #7132 from ethereum/smt_acc_solver 
[SMTChecker] EncodingContext config flag to accumulate assertions
 2019-08-01 13:04:37 +02:00
Leonardo Alt
44d7c6976a Erase pointer knowledge properly inside loops 2019-07-30 12:47:50 +02:00
Leonardo
00accd9daa
Merge pull request #7141 from ethereum/smt_fix_json 
[SMTChecker] Reset SSA index to 0 instead of increasing in context reset
 2019-07-29 10:20:06 +02:00
Leonardo
0197a200cd
Merge pull request #7142 from ethereum/smt_init_numbers 
[SMTChecker] Initialize all number types with 0
 2019-07-29 10:19:17 +02:00
Leonardo Alt
847f574e22 [SMTChecker] Fix ICE when inlining function with tuple expression 2019-07-26 16:29:29 +02:00
Leonardo Alt
cd5a5b3686 [SMTChecker] Initialize all number types with 0 2019-07-25 15:15:18 +02:00
Leonardo Alt
6bcbeb1d23 [SMTChecker] Reset SSA index to 0 instead of increasing in context reset 2019-07-25 14:16:34 +02:00
Leonardo
264035f0dd
Merge pull request #7120 from ethereum/smt_refactor_inlining 
[SMTChecker] Refactor function inlining
 2019-07-22 14:20:32 +02:00
Leonardo Alt
b204f27047 [SMTChecker] EncodingContext config flag to accumulate assertions 2019-07-19 19:31:25 +02:00
Leonardo Alt
03cc124f32 Add CHC skeleton 2019-07-19 11:52:05 +02:00
Leonardo Alt
382df64899 [SMTChecker] Refactor function inlining 2019-07-18 13:56:48 +02:00
Leonardo Alt
71144d0d39 [CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface 2019-07-15 17:31:39 +02:00
Leonardo
75eb67c3e0
Merge pull request #7050 from ethereum/smt_set_solver 
[SMTChecker] EncodingContext's solver needs to be set dynamically
 2019-07-08 15:19:55 +02:00
Leonardo Alt
96b0c4c148 [SMTChecker] New VariableUsage flag to inline functions 2019-07-08 14:40:33 +02:00
Leonardo Alt
01570bbc8c EncodingContext's solver needs to be set dynamically 2019-07-08 14:40:15 +02:00
chriseth
25928767b7
Merge pull request #7058 from ethereum/smt_reset_context 
[SMTChecker] Clear encoding context before engine starts
 2019-07-08 12:36:50 +02:00
Leonardo Alt
be663680d4 [SMTChecker] Clear encoding context before engine starts 2019-07-08 11:56:04 +02:00
Leonardo Alt
4aebdcc442 [SMTChecker] Allow FunctionSort to be created via sort and not type 2019-07-04 12:00:24 +02:00
Leonardo Alt
934e00d235 [SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars 2019-07-03 16:05:56 +02:00
chriseth
817852c650
Merge pull request #7030 from ethereum/smt_move_solver 
[SMTChecker] Move solver from SMTEncoder to BMC
 2019-07-02 14:08:55 +02:00
chriseth
e542e46163
Merge pull request #7022 from ethereum/smt_create_expr 
[SMTChecker] Always create symbolic expression
 2019-07-02 14:07:24 +02:00
chriseth
ca10b59b25
Merge pull request #7020 from ethereum/smt_fix_callstack_message 
[SMTChecker] Fix wrong assertion in callstack message
 2019-07-02 13:47:49 +02:00
Leonardo Alt
b0818bd002 [SMTChecker] Move solver pointer from SMTEncoder to BMC 2019-07-02 12:06:52 +02:00
Leonardo Alt
fb3c85633b Always create symbolic expression 2019-07-01 16:25:33 +02:00
Leonardo Alt
75663dc91e [SMTChecker] Fix require with message 2019-07-01 16:17:06 +02:00
Leonardo Alt
6606a13ed2 [SMTChecker] Remove unsound assertion (too strong) 2019-07-01 16:16:39 +02:00
Leonardo Alt
3cb4ed83c1 [SMTChecker] Split SMTChecker into SMTEncoder and BMC 2019-07-01 15:05:03 +02:00
Leonardo Alt
a28b84fdc3 [SMTChecker] Add a more general VerificationTarget 2019-06-27 10:31:50 +02:00
Leonardo Alt
48d6729164 [SMTChecker] Remove overflow check for assignments 2019-06-24 17:58:56 +02:00
Leonardo Alt
ed275fd760 [SMTChecker] Collect assertions in EncodingContext 2019-06-24 15:03:00 +02:00
Leonardo Alt
1221eeebf1 [SMTChecker] Report malformed expressions more precisely 2019-06-06 11:54:29 +02:00
Leonardo Alt
f281c94b42 [SMTChecker] Test that non-Boolean literals are actually integers 2019-06-05 10:51:05 +02:00
Leonardo
3a3316393e
Merge pull request #6897 from ethereum/smt_check_pragma_earlier 
[SMTChecker] Exit early if no pragma
 2019-06-05 10:26:25 +02:00
Leonardo
c39ea56f93
Merge pull request #6896 from ethereum/smt_use_portfolio 
[SMTChecker] Use SMTPortfolio directly
 2019-06-05 10:26:05 +02:00
Leonardo
155af48b9d
Merge pull request #6895 from ethereum/smt_keep_assertions 
[SMTChecker] Keep a copy of assertions that are added to the solvers
 2019-06-05 10:25:45 +02:00
Leonardo Alt
4de1e20954 [SMTChecker] Exit early if no pragma 2019-06-04 17:12:15 +02:00
Leonardo Alt
91653526bb [SMTChecker] Use SMTPortfolio directly instead of pointer to SolverInterface 2019-06-04 17:10:52 +02:00
Leonardo Alt
31ef421fff [SMTChecker] Keep a copy of assertions that are added to the solvers 2019-06-04 17:09:04 +02:00
Leonardo Alt
d9ce9cab99 [SMTChecker] Use smtlib's implies instead of \!a or b 2019-06-04 14:23:44 +02:00
chriseth
e08f521b7e
Merge pull request #6764 from ethereum/smt_fix_tuple_ice 
[SMTChecker] Fix ICE in unsupported function calls with multi return values
 2019-05-20 15:18:11 +02:00
Leonardo Alt
60a4f03d3d [SMTChecker] Fix ice in unsupported functions with multi return values 2019-05-16 18:23:42 +02:00
Leonardo Alt
5493a41842 [SMTChecker] Move global variables and functions to encoding context 2019-05-16 18:11:31 +02:00
Leonardo Alt
4e430ba0ae [SMTChecker] Move expression handling to EncodingContext 2019-05-14 15:56:43 +02:00
Leonardo Alt
ebbe03cad6 [SMTChecker] Move variable handling to EncodingContext 2019-05-13 16:59:28 +02:00
chriseth
01dd9ba2ae
Merge pull request #6717 from ethereum/smt_namespace 
Move SMT specific code into smt namespace
 2019-05-13 12:45:34 +02:00
chriseth
e5d46767f1
Merge pull request #6722 from ethereum/smt_fix_variable_usage 
[SMTChecker] Fix VariableUsage for IndexAccess
 2019-05-13 10:17:26 +02:00
Leonardo Alt
fac383a233 Move SMT specific code into smt namespace 2019-05-10 20:03:11 +02:00
chriseth
cc40e65a4b
Merge pull request #6712 from ethereum/smt_unique_ptr 
[SMTChecker] Use unique_ptr instead of shared_ptr where applicable
 2019-05-10 12:53:53 +02:00
Leonardo Alt
3ea5c112d3 [SMTChecker] Fix VariableUsage for IndexAccess 2019-05-10 11:28:10 +02:00
Leonardo Alt
8d65fd18fc [SMTChecker] Style changes 2019-05-09 19:15:43 +02:00
chriseth
89700dbcff
Merge pull request #6665 from ethereum/smt_inline_external_this 
[SMTChecker] Inline external function calls to `this`
 2019-05-09 19:09:08 +02:00
Leonardo Alt
ef32bf185f [SMTChecker] Inline external function calls to this. 2019-05-09 16:53:30 +02:00
Leonardo Alt
c8a017ccd6 [SMTChecker] Use unique_ptr instead of shared_ptr where applicable. 2019-05-09 16:34:22 +02:00
Leonardo Alt
6027383ae5 [SMTChecker] Fix call to function at state var init 2019-05-09 16:12:44 +02:00
Leonardo Alt
3d52a6ca68 [SMTChecker] Fix ICE in branch-inline function call-modify local variable 2019-05-09 09:15:11 +02:00
Leonardo Alt
9893cae27a [SMTChecker] Make mergeVariables deterministic 2019-05-08 20:46:01 +02:00
Leonardo Alt
0b046897ae [SMTChecker] Fix unsupported type assignment 2019-05-08 14:28:23 +02:00
Leonardo Alt
3c7540ceb2 [SMTChecker] Support tuples with multiple var decls 2019-05-07 16:57:27 +02:00
Leonardo Alt
2139c20776 [SMTChecker] Support delete 2019-05-06 18:32:10 +02:00
Leonardo
e99efec085
Merge pull request #6652 from ethereum/smt_tuple_function 
[SMTChecker] Support tuples as function calls with multiple return values
 2019-05-06 15:19:24 +02:00
Leonardo Alt
80712f44cb Fix short circuit with assignments 2019-05-06 11:04:43 +02:00
Leonardo Alt
5440a53d4d [SMTChecker] Support tuples as function calls with multiple return values 2019-05-03 06:10:22 +02:00
Leonardo Alt
204dcf1771 [SMTChecker] Support tuple assignments 2019-05-02 12:55:34 +02:00
Leonardo Alt
6c7527ac90 [SMTChecker] Support tuple type declaration 2019-05-02 12:05:21 +02:00
Leonardo Alt
66655b87b0 [SMTChecker] Fix ICE in fixed point operations 2019-05-02 10:59:23 +02:00
Leonardo Alt
dd4e938265 [SMTChecker] Fix ICE in inherited state var 2019-05-02 10:03:12 +02:00
Leonardo Alt
a6db37ac9c [SMTChecker] Fix bad cast in base constructor modifier. 2019-04-30 18:48:13 +02:00
Leonardo Alt
e4989369d0 Refactor cast from identifier ref decl to var decl 2019-04-30 11:08:36 +02:00
Leonardo Alt
762f79f84d Refactor assignment handling 2019-04-30 11:08:36 +02:00
Leonardo Alt
fc482de695 [SMTChecker] Support address members 2019-04-25 16:24:36 +02:00
Leonardo Alt
dd1afeba52 [SMTChecker] Support this as address 2019-04-18 17:56:52 +02:00
chriseth
fce19bde58
Merge pull request #6545 from ethereum/smt_contracts 
[SMTChecker] Support contract type
 2019-04-18 13:01:18 +02:00
Leonardo Alt
ecd89393ee [SMTChecker] Support contract type 2019-04-17 16:30:11 +02:00
Leonardo Alt
03d18f1b98 [SMTChecker] Add note about not inlining external function calls 2019-04-17 16:14:07 +02:00
Christian Parpart
721bf367a3
[libsolidity] TypeProvider: eliminate redundant "Type" suffix in provider function signatures. 2019-04-17 14:42:07 +02:00
Christian Parpart
862b65d6e3
[libsolidity] remove ReferenceType::copyForLocationIfReference (use TypeProvider instead) 2019-04-17 13:25:03 +02:00
Christian Parpart
58a45f2cb6 [libsolidity] TypeProvider: adds explicit uint256() accessor and removes default params in integerType(...). 2019-04-16 18:28:40 +02:00
Christian Parpart
bf43eebea9 libsolidity: Introducing TypeProvider API, for clear type system ownership. 2019-04-16 18:26:45 +02:00
Leonardo Alt
07fac9e381 [SMTChecker] Allow SymbolicVariable from smt::Sort 2019-04-15 14:52:46 +02:00
chriseth
bf5792f7ca
Merge pull request #6483 from ethereum/smt_support_mod 
[SMTChecker] Support mod
 2019-04-15 13:42:18 +02:00
chriseth
73ac8f6220
Merge pull request #6421 from ethereum/smt_fix_variable_usage 
[SMTChecker] Refactor VariableUsage
 2019-04-15 13:39:10 +02:00
Leonardo Alt
af9f16e014 [SMTChecker] Support mod 2019-04-12 12:39:25 +02:00
Leonardo Alt
4fe303530a [SMTChecker] Show unsupported warning for asm blocks 2019-04-05 16:41:15 +02:00
Leonardo Alt
79d8a4e13a [SMTChecker] Refactor VariableUsage 2019-04-05 11:38:37 +02:00
Leonardo Alt
aa9b9aa87e [SMTChecker] Support unary inc/dec for array/mapping access 2019-04-02 16:53:19 +02:00
chriseth
84251e5a22
Merge pull request #6405 from ethereum/smt_compound_assignment 
[SMTChecker] Support arithmetic compound assignment operators.
 2019-03-28 18:27:25 +01:00
Leonardo Alt
a7e826a224 [SMTChecker] Implement short circuit 2019-03-28 16:08:30 +01:00
Leonardo Alt
15269067b5 Support arithmetic compound assignment operators 2019-03-28 15:27:52 +01:00
Leonardo Alt
ecbf36f271 Refactor computing symbolic arithmetic operation 2019-03-28 15:27:36 +01:00
Leonardo Alt
1d63b97857 Take inlined function calls into account when collecting touched variables 2019-03-28 14:32:47 +01:00
Leonardo Alt
6f9b69ebc3 Refactor function that retrieves FunctionDefinition from FunctionCall 2019-03-28 14:32:47 +01:00
Leonardo Alt
a207d7f44c [SMTChecker] Add callstack model to overflow checks 2019-03-21 16:25:33 +01:00
Leonardo Alt
de89733bd6 [SMTChecker] Fix nullptr deref 2019-03-21 15:46:54 +01:00
Leonardo Alt
9659f40c8d [SMTChecker] Support modifiers 2019-03-20 11:32:20 +01:00
Leonardo Alt
3296fb3764 Add callstack to model report 2019-03-20 10:35:29 +01:00
Leonardo Alt
a8209e9899 [SMTChecker] Shortcut RationalNumber expressions 2019-03-11 12:53:49 +01:00
Leonardo Alt
02d0e609b9 [SMTChecker] Support enums 2019-03-07 15:15:12 +01:00
Leonardo Alt
29b2ab6f66 Handle aliasing 2019-03-06 11:29:54 +01:00
Leonardo Alt
467c34999f Do not throw on string literals 2019-03-06 11:29:26 +01:00
Leonardo Alt
e74f58130e Add SMT type support to Solidity arrays 2019-03-06 11:29:26 +01:00
Mathias Baumann
f782125463 Fix SMT Checker crash due to missing type information 2019-02-28 11:55:45 +01:00
Leonardo Alt
bbd2c91e19 [SMTChecker] Replace dynamic_cast by category check 2019-02-26 00:47:59 +01:00
Leonardo Alt
34470f3549 [SMTChecker] Only check for overflow/underflow in the end of the function 2019-02-18 23:55:58 +01:00
chriseth
cb0ad2266c
Merge pull request #6008 from ethereum/smt_fix_abstract_assignment 
[SMTChecker] Assert type is not function when assigning
 2019-02-18 14:54:20 +01:00
Leonardo Alt
22cdfb18d4 [SMTChecker] Assert type is not function when assigning 2019-02-14 13:32:56 +01:00
Daniel Kirchner
8ca6715e18 More style checks. 2019-02-14 11:41:20 +01:00
Leonardo Alt
637546850f [SMTChecker] Add mod operator 2019-02-07 14:24:40 +01:00
Leonardo Alt
9a33367bc6 [SMTChecker] Warn when no solver was found and there are unhandled queries. 2019-01-29 14:29:07 +01:00
Leonardo Alt
7f8ceaadab [SMTChecker] Clear state knowledge after external function calls 2019-01-21 12:58:40 +01:00
Leonardo Alt
a10db051de [SMTChecker] Support basic typecast 2019-01-16 13:00:54 +01:00
Leonardo Alt
cce377833a Sort includes in libsolidity/formal 2018-12-17 18:26:10 +01:00
Leonardo Alt
9199718ec0 Clear all mapping knowledge after array variable assignment 2018-12-14 12:21:53 +01:00
Leonardo Alt
6a2809a582 [SMTChecker] Support to mapping 2018-12-14 12:21:53 +01:00
Leonardo Alt
08737e43dc [SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions 2018-12-11 11:28:25 +01:00
Leonardo Alt
de46bb2c42 [SMTChecker] Introduce SymbolicFunctionVariable 2018-12-10 11:34:29 +01:00
Kevin Kelley
fb6fd1b3c2 add a 'readable' format for large hex values 2018-12-05 22:15:02 +01:00
Leonardo Alt
b9f424e373 [SMTChecker] Simplify symbolic variables 2018-12-05 09:56:52 +01:00
Leonardo Alt
8069bb61da [SMTChecker] Loops are unrolled once 2018-12-04 12:35:19 +01:00
Leonardo Alt
6d41ffb4a5 [SMTChecker] Remove unary plus operator 2018-12-03 10:35:38 +01:00
Leonardo Alt
2f6de12e8c [SMTChecker] Make smt::Sort::operator== virtual 2018-11-30 10:41:15 +01:00
chriseth
9e9250c961 Fix move bug. 2018-11-29 15:32:38 +01:00
Leonardo Alt
aaaa92012c [SMTChecker] Unknown answer for constant condition check should not do anything 2018-11-26 12:54:02 +01:00
Leonardo Alt
6251a289dd Testing with smtlib2 interface always there 2018-11-23 09:43:49 +01:00
Leonardo Alt
dee0c4ded8 Error message stays in the SMTChecker 2018-11-23 09:43:49 +01:00
Leonardo Alt
f3c2309c73 Display better error message in SMTLib2 2018-11-23 09:43:49 +01:00