Commit Graph

5016 Commits

Author SHA1 Message Date
Alexander Arlt
ff7c47a1f3 Fix test/stopAfterParseTests.sh for macos. 2020-10-28 17:59:56 -05:00
chriseth
d00ef95a72 Refactor isoltest function call kind. 2020-10-28 19:04:24 +01:00
chriseth
7b26c099b3
Merge pull request #10122 from ethereum/ewasm-interpreter
[ewasm] Fix EwasmBuiltinInterpreter to follow the specs
2020-10-28 13:11:44 +01:00
chriseth
fb40f29594
Merge pull request #10133 from ethereum/asm-error-codes
Split error codes for EVM opcodes
2020-10-28 13:00:23 +01:00
Alex Beregszaszi
6b2942e7f0 [ewasm] Properly touch memory in EwasmInterpreter 2020-10-28 11:57:18 +00:00
Alex Beregszaszi
9dc5ceae94 [ewasm] Implement "create" properly in EwasmInterpreter 2020-10-28 11:57:18 +00:00
Alex Beregszaszi
62028c90f0 [ewasm] Overhaul memory handling in EwasmInterpreter
Introduce writeMemory and read/writeBytes32/Address helpers.
Fix read/writeU128/U256 to be little-endian.
Update each instruction to follow the specification.
2020-10-28 11:57:18 +00:00
Alex Beregszaszi
24d8c2ed90 Split error codes for EVM opcodes 2020-10-28 11:45:46 +00: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
chriseth
cc4b44058d
Merge pull request #10126 from ethereum/fixIceStructCalldataToStorageSol2Yul
[Sol->Yul] Fixing ice when copying struct that contains nested array to storage
2020-10-28 11:46:22 +01: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
28f92064b9 [Sol->Yul] Fixing ice when copying struct that contains nested array to storage 2020-10-28 09:28:40 +01:00
Djordje Mijovic
9cc37c3fa4 [SMTChecker] Fix ICE when using >>> 2020-10-28 09:25:14 +01: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
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
Mathias Baumann
a4dc110b38 Fix dependency tracking for abstract contracts for Yul codegen 2020-10-20 16:58:24 +02:00
Mathias Baumann
e991465336 Fix dependency tracking for abstract contracts 2020-10-20 16:58:24 +02:00
Leonardo Alt
cf35785328 Add unknown message to all verification targets 2020-10-19 20:54:13 +01:00
Leonardo Alt
b67ade5163 Move modelCheckerSettings out of settings in StandardCompiler 2020-10-19 10:39:06 +01:00
Daniel Kirchner
79d9a1ca81 Tests for abi.encode. 2020-10-16 20:24:43 +02:00
Daniel Kirchner
e06d4303fb Semantic tests. 2020-10-16 19:40:41 +02:00
Daniel Kirchner
909ce9164a Allow arrays of contract types as type expressions e.g. for abi.decode. 2020-10-16 19:40:41 +02:00
Leonardo
eedd12ad1d
Merge pull request #10056 from ethereum/smt_fix_develop
Fix SMT command line test
2020-10-16 18:37:55 +01:00
Leonardo Alt
289ac23fe6 Fix smt cmdlinetest 2020-10-16 17:58:45 +01:00
Daniel Kirchner
db4dd51739
Merge pull request #10055 from ethereum/userDefinedLibraryTypes
Disallow invalid use of library names as type names.
2020-10-16 18:55:42 +02:00
Daniel Kirchner
3f14c904b0 Disallow invalid use of library names as type names. 2020-10-16 18:25:08 +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
8c351278ac [SMTChecker] added test to check correct handling of the sign of the modulo operation 2020-10-16 16:17:32 +02: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
Djordje Mijovic
5f0b8dd716 [Sol->Yul] Changing yul unimplemented test as delete bytes is implemented now. 2020-10-15 22:05:40 +02:00
Djordje Mijovic
4a66723ff9 [Sol->Yul] Implementing resizing of dynamic byte arrays
Co-authored-by: chriseth <chris@ethereum.org>
2020-10-15 22:05:35 +02:00
chriseth
c9ed1b9ae9
Merge pull request #10047 from ethereum/removeMemoryGuards
Disable StackLimitEvader again until we have stronger correctness guarantees.
2020-10-15 18:56:33 +02:00
chriseth
89bdad2096
Merge pull request #10043 from ethereum/emptyArrayCopy
Fix empty array copy bug.
2020-10-15 17:07:54 +02:00
chriseth
38abadf502 Fix empty array copy bug. 2020-10-15 16:48:08 +02:00
Daniel Kirchner
2e984a3651 Remove memoryguard calls from command line test expectations. 2020-10-15 16:25:15 +02:00
Daniel Kirchner
82876fd00e Disable StackLimitEvader again until we have stronger correctness guarantees. 2020-10-15 16:16:41 +02:00
chriseth
e17d6853a9
Merge pull request #9985 from ethereum/optimizeDeleteStructSol2Yul
[Sol->Yul] Optimizing delete struct.
2020-10-15 16:03:06 +02:00
Bhargava Shastry
5023d3decb ossfuzz: Remove antlr4 build deps 2020-10-15 12:59:18 +02:00
chriseth
837dd004c8 Enable some more Yul tests. 2020-10-14 17:43:19 +02:00
Djordje Mijovic
6f7947cfa5 [Sol->Yul] Optimizing delete struct.
Co-authored-by: Daniel Kirchner <daniel@ekpyron.org>
2020-10-14 13:35:15 +02:00
chriseth
92a2cddbfa
Merge pull request #10024 from ethereum/outofBoundsGetter
Use revert for out-of-bounds array index access in getter.
2020-10-14 12:33:41 +02:00
chriseth
9b1f90512b
Merge pull request #10027 from ethereum/yul-syntax-test-extractions
Continued Yul syntax test extractions.
2020-10-14 12:32:39 +02:00
chriseth
56d6855222
Merge pull request #9738 from ethereum/arrayCopyingSol2Yul
[Sol->Yul] Implementing copying of arrays to storage
2020-10-14 12:22:09 +02:00