Commit Graph

2973 Commits

Author SHA1 Message Date
Leonardo
264035f0dd
Merge pull request #7120 from ethereum/smt_refactor_inlining
[SMTChecker] Refactor function inlining
2019-07-22 14:20:32 +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
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