Commit Graph
4163 Commits
Author SHA1 Message Date
Alex Beregszaszi 1ab6340828 Move AsmJsonImporter from libsolidity to libyul
It is next to AsmJsonConverter now and interdependencies are shrunk.
2020-10-29 14:06:34 +00:00
chriseth 0c12b2e53a Bit operations for fixed bytes types. 2020-10-28 18:04:54 +01: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 f2f84a7f97 Format array cex 2020-10-27 16:32:43 +00:00
Leonardo Alt 446e46fe06 Use Expression instead of plain strings for counterexamples 2020-10-27 12:04:51 +00: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
chriseth a83ad58109 Merge pull request #10081 from ethereum/maskBytes
Extract mask bytes function.
2020-10-21 10:09:40 +02:00
chrisethandHarikrishnan Mulackal 3920f398aa Update libsolidity/codegen/YulUtilFunctions.h
Co-authored-by: Harikrishnan Mulackal <webmail.hari@gmail.com>
2020-10-21 09:48:22 +02:00
chriseth 53d6721e47 Extract mask bytes function. 2020-10-20 17:36:46 +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 909ce9164a Allow arrays of contract types as type expressions e.g. for abi.decode. 2020-10-16 19:40:41 +02: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 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 Mijovicandchriseth 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 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
Daniel Kirchner 20072918d9 Make sure lValueOfOrdinaryAssignment does not have an undefined value. 2020-10-14 21:00:18 +02:00
Djordje MijovicandDaniel Kirchner 6f7947cfa5 [Sol->Yul] Optimizing delete struct.
Co-authored-by: Daniel Kirchner <daniel@ekpyron.org>
2020-10-14 13:35:15 +02:00
chriseth 25b10b9643 Merge pull request #10028 from ethereum/useArrayLength
Use array length function.
2020-10-14 13:35:09 +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 a737e51533 Use array length function. 2020-10-14 12:22:34 +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
chriseth 8d241fece9 Merge pull request #9849 from ethereum/fixIce9817
Fixing ICE on returning struct with mapping from library
2020-10-14 00:05:19 +02:00
Leonardo Alt 440e5b3935 [SMTChecker] Fix counterexample state reporting 2020-10-13 22:18:43 +01:00
Djordje Mijovicandchriseth 850a94bdc9 [Sol->Yul] Implementing arrays copying to storage.
Co-authored-by: chriseth <chris@ethereum.org>
2020-10-13 20:31:08 +02:00
Djordje Mijovic 1272c474ba Fixing ICE when returning Struct from library 2020-10-13 20:00:11 +02:00
chriseth 5dc3a971cb Use revert for out-of-bounds array index access in getter. 2020-10-13 18:57:41 +02:00
Leonardo Alt aec456021d Add tx constraints to CHC 2020-10-13 17:49:04 +01:00
Leonardo Alt a2cdde1191 Add tx data to symbolic state 2020-10-13 17:49:04 +01:00