Commit Graph

2954 Commits

Author SHA1 Message Date
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