Commit Graph

3054 Commits

Author SHA1 Message Date
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
chriseth
74f16ef186 Refactor IRLValue so that it does not require IRGenerationContext. 2019-08-08 17:27:35 +02:00
chriseth
9955c51769
Merge pull request #7077 from ethereum/sol-yul-delete-fixed-storage
[Sol->Yul] Implement delete for fixed-sized storage arrays
2019-08-08 16:47:16 +02:00
mingchuan
15631a7fbe Split calldataEncodedSize into calldataEncodedSize, calldataEncodedTailSize and calldataHeadSize and fix all usages. 2019-08-08 15:52:21 +02:00
Mathias Baumann
e072885031 [Sol->Yul] Implement delete for fixed-sized storage arrays 2019-08-07 18:28:52 +02:00
chriseth
6166dc8e8f
Merge pull request #6856 from rocky/recoveringParser1-ast
Produce AST even when there are parser errors
2019-08-07 15:56:45 +02:00
chriseth
c8f04b88bf
Merge pull request #7176 from ethereum/decodeMemoryLocation
Always copy dynamically-sized memory arrays during CompilerUtils::abiDecode
2019-08-07 15:42:14 +02:00
rocky
7fd7cc1e76 Produce AST even when there are parser errors 2019-08-07 15:25:53 +02:00
Daniel Kirchner
efb34bdf22 Always copy dynamically-sized memory arrays during CompilerUtils::abiDecode. 2019-08-06 14:11:14 +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
chriseth
9b375edfe3
Merge pull request #6787 from ethereum/sol2yul-ctor-code
Improve constructor-code codegen (wrt. state variable initialization)
2019-08-05 11:50:34 +02:00
Christian Parpart
235638b3fc Implements constructor code for state variables. 2019-08-05 11:23: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
2a25d7461f
Merge pull request #7123 from rocky/tolerate-pragma-mismatch
A pragma version mismatch is not fatal if ...
2019-08-01 14:48:24 +02:00
chriseth
6730a59f74
Merge pull request #7157 from ethereum/fix-7155
FunctionType: Return correct stacksize for transfer/send
2019-08-01 14:40:35 +02:00
Mathias Baumann
e887c06f6b FunctionType: Return correct stacksize for transfer/send 2019-08-01 13:56:09 +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
chriseth
aa87a607fd
Merge pull request #7152 from ethereum/smt_fix_pointer_cleanup
[SMTChecker] Erase pointer knowledge properly inside loops
2019-08-01 12:46:20 +02:00
Leonardo Alt
44d7c6976a Erase pointer knowledge properly inside loops 2019-07-30 12:47:50 +02:00
Mathias Baumann
d9addbcf49 Fix error in g++7 with -O2 flag 2019-07-29 16:17:41 +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
508cf66da2
Merge pull request #7062 from ethereum/smt_chc_checker
[SMTChecker] Add skeleton for CHC
2019-07-19 15:41:43 +02:00
Leonardo Alt
03cc124f32 Add CHC skeleton 2019-07-19 11:52:05 +02:00
chriseth
a30be56c27 Additional type info for ABI. 2019-07-18 16:54:11 +02:00
Leonardo Alt
382df64899 [SMTChecker] Refactor function inlining 2019-07-18 13:56:48 +02:00
rocky
f9b631f410 A pragma version mismatch is not fatal if ...
error recovery is desired.

Fixes #7085
2019-07-17 19:01:01 -04:00
Leonardo Alt
71144d0d39 [CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface 2019-07-15 17:31:39 +02:00
chriseth
579bdaddb9
Merge pull request #7088 from ethereum/diffLegYul
Document differences between legacy Solidity and Solidity via Yul.
2019-07-11 17:59:01 +02:00
chriseth
76d7ea888b Document differences between legacy Solidity and Solidity via Yul. 2019-07-11 17:48:06 +02:00
chriseth
869d69d293 Supply full object to stack compressor and Optimizer Suite. 2019-07-10 18:49:42 +02:00
Mathias Baumann
d264e3e0ba [Sol->Yul] Implement getter functions 2019-07-10 13:42:39 +02:00
Mathias Baumann
37f04976a2 [Sol->Yul] Implement keccak256 2019-07-09 18:25:07 +02:00
chriseth
15eb8fec50
Merge pull request #7015 from ethereum/sol-yul-arrays
[Sol->Yul] Implement uint256[] memory arrays
2019-07-09 17:34:46 +02:00
Mathias Baumann
0f24fcea17 [Sol->Yul] Implement uint256[] memory arrays 2019-07-09 15:36:02 +02:00
chriseth
859dbaa2a3
Merge pull request #7053 from djudjuu/moveSuffixHelper
move SuffixHelper to StringUtils
2019-07-09 14:32:05 +02:00
djudjuu
cafa01cbf6 moved SuffixHelper to StringUtils 2019-07-09 13:50:07 +02:00
chriseth
9cb9021c36 Cope with constants without value in inline assembly. 2019-07-09 11:12:13 +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
18072586c9 Remove trailing whitespace in error message. 2019-07-08 14:28:38 +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
chriseth
aac226f7c1
Merge pull request #7041 from ethereum/smt_function_sort
[SMTChecker] Allow symbolic functions to be created via Sort
2019-07-08 12:33:38 +02:00
chriseth
7267873a96
Merge pull request #7038 from ethereum/addSecondaryLocationToStandardIO
Provide secondary source location for error messages in standard json.
2019-07-08 12:00:09 +02:00
Leonardo Alt
be663680d4 [SMTChecker] Clear encoding context before engine starts 2019-07-08 11:56:04 +02:00
chriseth
2e01816c6b
Merge pull request #7042 from ethereum/make-whiskers-fail-early
Make Whiskers fail early when called with int
2019-07-04 12:19:54 +02:00
Leonardo Alt
4aebdcc442 [SMTChecker] Allow FunctionSort to be created via sort and not type 2019-07-04 12:00:24 +02:00
chriseth
d3e542d32c Provide secondary source location for error messages in standard json. 2019-07-04 10:54:01 +02:00
Mathias Baumann
3e51d14c6d Fix missing int -> string conversion 2019-07-04 09:31:24 +02:00
Leonardo Alt
934e00d235 [SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars 2019-07-03 16:05:56 +02:00
chriseth
b837705259
Merge pull request #7018 from ethereum/compile_only_requested
Compile only requested sources and contracts
2019-07-03 14:11:42 +02:00
chriseth
2b91022b25 Fix view/pure checker for access to base. 2019-07-03 11:19:57 +02:00
chriseth
60525dbf52
Merge pull request #7026 from ethereum/asmConstants
Support direct constants in inline assembly.
2019-07-02 14:21:24 +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
cdd137e3d1 Support constant numbers in inline assembly. 2019-07-02 14:01:05 +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
6f8fd309a2 Compile only requested sources and contracts 2019-07-01 18:52:21 +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
chriseth
3be21800ac
Merge pull request #6683 from ethereum/updateSwarm
Update swarm hash.
2019-06-27 13:18:29 +02:00
chriseth
53f37f487f
Merge pull request #6994 from ethereum/smt_refactor_targets
[SMTChecker] Delay all checks
2019-06-27 12:56:34 +02:00
chriseth
89f0e1e6da Use updated swarm hash. 2019-06-27 12:49:06 +02:00
chriseth
aa11ad7d0a Update swarm hash. 2019-06-27 12:48:51 +02:00
chriseth
8d18003808
Merge pull request #6716 from ethereum/wasmTranslation
[Yul] EVM to Wasm translation
2019-06-27 12:31:35 +02:00
Leonardo Alt
a28b84fdc3 [SMTChecker] Add a more general VerificationTarget 2019-06-27 10:31:50 +02:00
chriseth
b4a0a79398
Merge pull request #6993 from ethereum/smt_false_positives
[SMTChecker] Remove overflow check for assignments
2019-06-26 13:06:31 +02:00
chriseth
c6f7f5b2b0 Enable EWasm output. 2019-06-25 19:07:38 +02:00
chriseth
fe9aa59b8f Fix conversion during storing. 2019-06-25 13:00:02 +02:00
Leonardo Alt
48d6729164 [SMTChecker] Remove overflow check for assignments 2019-06-24 17:58:56 +02:00
chriseth
efd8d8fe5e
Merge pull request #6991 from ethereum/check_style-no-space-before-range-based-for-loop-colon
Adds a test to check_style.sh to check for spaces before colon (:) in range based for loops.
2019-06-24 17:42:06 +02:00
Christian Parpart
7b3aba81fb Adds a test to check_style.sh to check for spaces before colon (:) in range based for loops. 2019-06-24 17:32:58 +02:00
chriseth
2563178a0a
Merge pull request #6990 from ethereum/sol-yul-storage-array-index
Enable yul for more end to end tests
2019-06-24 16:30:33 +02:00
Leonardo Alt
ed275fd760 [SMTChecker] Collect assertions in EncodingContext 2019-06-24 15:03:00 +02:00
Mathias Baumann
0e812b16c2 Minor indent fix 2019-06-24 14:51:04 +02:00
chriseth
9c129a4087
Merge pull request #6984 from ethereum/yul-reindent
yul: adds reindent() function to reindent yul source code and makes us of it in IRGenerator
2019-06-24 12:54:40 +02:00
Christian Parpart
0fd1db533e yul: adds reindent() function to reindent yul source code and makes use of it in IRGenerator.
This function does count curly and round braces and reindents
accordingly the beginning of each line.

It does consider line-comments (// and ///) but not multiline comments (/* ... */).
2019-06-24 12:53:50 +02:00
chriseth
350631ae0d
Merge pull request #6940 from ethereum/sol-yul-storage-array-index
[Sol->Yul] Implement index access for storage arrays
2019-06-24 12:49:19 +02:00
Mathias Baumann
1dd63f416e [Sol->Yul] Implement index access for storage arrays 2019-06-20 16:14:51 +02:00
Mathias Baumann
346c512cd7 [Sol->Yul] Implement _slot/_offset suffix for storage variables 2019-06-20 14:50:52 +02:00
chriseth
9bb7160c4c
Merge pull request #6958 from sifmelcara/fix-abiencoderv2-codegen
Fix incorrect abi encoding of storage array of data type that occupy multiple storage slots
2019-06-20 13:08:42 +02:00
Daniel Kirchner
fcd3410f26 Implement checked mod for sol->yul code generation. 2019-06-20 12:30:32 +02:00
Daniel Kirchner
a5b9f634ef Implement signed multiplication for sol->yul code generation. 2019-06-20 12:30:30 +02:00
Daniel Kirchner
e4c884ae13 Unify style of checked integer division for sol->yul code generation. 2019-06-20 12:18:18 +02:00
Daniel Kirchner
5f6af8b374 Implement signed subtraction for sol->yul code generation. 2019-06-20 12:16:56 +02:00
Daniel Kirchner
88988af561 Implement signed addition for sol->yul code generation. 2019-06-20 11:42:50 +02:00
Mathias Baumann
b03cb2bce6 YulUtilFuncs: Add missing/adjust existing documentation 2019-06-19 18:09:23 +02:00