Commit Graph
4557 Commits
Author SHA1 Message Date
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
Daniel Kirchner 0dca223b45 Add another argument to setimmutable and the AssignImmutable opcode, allowing to modify code at any memory offset. 2020-10-15 18:14:41 +02:00
chriseth 00fb152316 Merge pull request #10048 from ethereum/develop
Merge develop into breaking
2020-10-15 17:30:11 +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
chriseth 979d3062bc Merge pull request #10033 from ethereum/develop
Merge develop into breaking
2020-10-14 14:12:20 +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
chriseth f6e57a0eec Merge pull request #10023 from ethereum/develop
Merge develop into breaking.
2020-10-13 18:18:53 +02:00
chriseth c86ea59384 Merge pull request #10019 from ethereum/exp-associativity
[BREAKING] Exp associativity
2020-10-13 17:03:18 +02:00
hrkrshnn 13e7012e1e Parser: Exponentiation is right associative 2020-10-13 16:38:37 +02:00
Leonardo 8fd6de9403 Merge pull request #10014 from ethereum/smt_fix_predicagte
[SMTChecker] Fix implicit constructor summary predicate
2020-10-13 14:55:52 +01:00
Mathias Baumann 006e5f2e1f Allow path syntax for super constructor calls 2020-10-13 14:32:11 +02:00
Mathias Baumann 0b7b174945 Add AST Node IdentifierPath 2020-10-13 14:32:11 +02:00
Mathias Baumann 32b4f18023 Print warning for unnamed return parameters and no return statement 2020-10-13 13:11:29 +02:00
chriseth 0ea4bdafcd Merge pull request #10017 from ethereum/develop
Merge develop into breaking.
2020-10-13 12:58:23 +02:00
Leonardo Alt 1e568d7dc6 [SMTChecker] Fix implicit constructor summary predicate 2020-10-13 09:38:58 +01:00
chriseth abfa136afb Merge pull request #10012 from ethereum/extractSelectorFunction
Extract function to compute function selector from signature.
2020-10-12 20:32:05 +02:00
chriseth 4b342a7cad Merge pull request #9816 from ethereum/exp-base-literals
[Sol->Yul] Optimization for exponentiation when the base is a literal
2020-10-12 19:34:38 +02:00
Harikrishnan Mulackal 418aa01c5b Optimization for exponentiation when the base is a literal 2020-10-12 18:54:58 +02:00
chriseth cb0d1134b7 Extract function to compute function selector from signature. 2020-10-12 17:57:34 +02:00
Djordje Mijovic e23d8f5593 [SMTChecker] Supporting inline arrays. 2020-10-12 16:59:14 +02:00
chriseth 8a1bf41ac0 Merge pull request #10010 from ethereum/develop
Merge develop into breaking.
2020-10-12 15:33:34 +02:00
Kamil Śliwak e1cc888369 Fix checkBaseABICompatibility() to make it actually check return parameters and not just ordinary parameters twice 2020-10-12 15:14:56 +02:00
Kamil Śliwak 3128e82a9a Look for experimental pragmas in the module containing the definition when generating code for modifiers and inherited functions 2020-10-12 14:29:53 +02:00
chriseth 1a125cf755 Merge pull request #10006 from ethereum/bug-9229-fix
Fixes internal compiler error with an unused reference to module member.
2020-10-12 13:43:35 +02:00
Leonardo Alt 18cf01c187 Add this and state to CHC 2020-10-12 11:11:52 +01:00
Leonardo Alt a86f656704 Refactor state as tuple 2020-10-12 11:11:52 +01:00
Christian Parpart 712d0805eb Fixes internal compiler error with an unused reference to module member. 2020-10-12 11:56:01 +02:00
chriseth 3739b03af6 Merge pull request #9877 from a3d4/fix-homonymous-declarations-warnings
Fix shadowing/same-name warnings for later declarations
2020-10-08 22:27:15 +02:00
a3d4 90c8c32d86 If a declaration shadows several others, group them together 2020-10-08 21:01:25 +02:00