Commit Graph

4498 Commits

Author SHA1 Message Date
chriseth
db4b39e09e Round up allocations to multiples of 32. 2021-01-14 21:52:17 +00:00
chriseth
7d6331e26f Use round up function. 2021-01-14 21:01:43 +00:00
Alex Beregszaszi
6ad0ea9f23
Merge pull request #10773 from ethereum/useArrayAllocationFunction
Fix array allocation.
2021-01-14 20:25:31 +00:00
chriseth
f4479fd7ed Fix array allocation. 2021-01-14 19:56:37 +01:00
Alex Beregszaszi
7c7fd22062 Include revert strings in IR 2021-01-14 18:45:12 +01:00
Leonardo
110e0e1f25
Merge pull request #10763 from blishko/smt-abi-fixes
[SMTChecker] Small fixes in handling ABI functions
2021-01-14 16:00:49 +01:00
chriseth
7d036dcb81
Merge pull request #10762 from ethereum/packedStorageOverflowSol2Yul
[Sol->Yul] Fixing uncheked increment/decrement.
2021-01-14 15:32:55 +01:00
Martin Blicha
504e4c22b2 [SMTChecker] Fix in abi handling - tuple expression of size 1 has the type of the member and not TupleType 2021-01-14 14:53:56 +01:00
Martin Blicha
b4d2a71eec [SMTChecker] Fix in abi handling - fixed missing type conversion 2021-01-14 14:53:44 +01:00
Martin Blicha
32a923c7ef [SMTChecker] Fix in abi handling - abstracting expressions of type Function inside ABI functions when translating to SMT 2021-01-14 14:53:22 +01:00
chriseth
a65415cdad Fix accessing libraries inside modules. 2021-01-14 14:07:08 +01:00
Djordje Mijovic
dc3e76bc2c [Sol->Yul] Fixing uncheked increment/decrement. 2021-01-14 13:46:04 +01:00
chriseth
170cd5d2ae
Merge pull request #10760 from ethereum/asmConstantsFileLevel
Fix accessing constants at file level from inline assembly.
2021-01-14 11:33:47 +01:00
chriseth
8905af28c3
Merge pull request #10759 from ethereum/nestedBytesArraySol2Yul
[Sol->Yul] Fixing nested bytes array push.
2021-01-14 11:33:06 +01:00
chriseth
45be47fc6b
Merge pull request #10756 from ethereum/fixModifierLookup
Fix modifier lookup
2021-01-14 11:28:26 +01:00
chriseth
8ad9290086 Fix modifier lookup. 2021-01-14 11:01:14 +01:00
chriseth
30305ebbd9 Fix accessing constants at file level from inline assembly. 2021-01-14 10:51:47 +01:00
chriseth
afbf68f79c
Merge pull request #10753 from ethereum/ir-negate
Fix YulUtilFunctions::negateNumberWrappingFunction
2021-01-14 10:48:15 +01:00
Djordje Mijovic
7c45509a77 [Sol->Yul] Fixing nested bytes array push. 2021-01-14 10:32:31 +01:00
Alex Beregszaszi
c15c6d26b7 Fix YulUtilFunctions::negateNumberWrappingFunction 2021-01-13 21:29:37 +00:00
Martin Blicha
5e13744423 [SMTChecker] Fixed pushing string literal to bytes array 2021-01-13 16:30:50 +01:00
chriseth
6eea2f5c08
Merge pull request #9959 from a3d4/fix-ice-struct-with-mapping-assignment
Fix ICE caused by const structs with mappings
2021-01-13 15:19:02 +01:00
Leonardo
fe344ed6e5
Merge pull request #10748 from blishko/smt-refactoring
[SMTChecker] Refactoring common functionality
2021-01-13 14:23:19 +01:00
a3d4
35a25b107f Fix ICE caused by const structs with mappings 2021-01-12 18:39:54 +01:00
Martin Blicha
7c6340fe4f [SMTChecker] Refactoring expression to tuple assignment 2021-01-12 17:15:14 +01:00
Daniel Kirchner
162b1508da
Merge pull request #10744 from ethereum/useDropEx
Use drop_exactly.
2021-01-12 17:11:54 +01:00
chriseth
d97b9ba865
Merge pull request #10686 from ethereum/libraryCallGuard
Library call guard.
2021-01-12 16:52:24 +01:00
Leonardo
fa28e48415
Merge pull request #10727 from ethereum/smt_cex_internal_calls
[SMTChecker] Report internal calls in CHC transaction trace
2021-01-12 15:44:12 +01:00
chriseth
99add1e4e5
Merge pull request #10710 from ethereum/implicit-conversion-bug
Disallow certain implicit conversions between integer types.
2021-01-12 15:42:12 +01:00
Leonardo Alt
b3c3836388 Output internal calls 2021-01-12 14:57:04 +01:00
chriseth
24aded266e Dereference. 2021-01-12 14:28:27 +01:00
chriseth
7487a7d927 Use drop_exactly. 2021-01-12 14:01:10 +01:00
Leonardo Alt
f1ae24abc7 Remove extra line breaks 2021-01-12 14:00:07 +01:00
Leonardo
66a773aef9
Merge pull request #10721 from blishko/smt-try-catch
[SMTChecker] Support try-catch statements
2021-01-12 12:04:38 +01:00
hrkrshnn
e107d51f46 Disallow certain implicit conversions between integer types.
Disallow implicit conversion from ``uintN`` and ``intM`` when ``M > N``, and by extension, explicit
conversion between the same types are also disallowed.
2021-01-12 08:23:47 +01:00
chriseth
b9de0c6155 Use zip. 2021-01-11 20:54:28 +01:00
chriseth
5c453acbe8 Fix encoding of library return values. 2021-01-11 20:37:45 +01:00
chriseth
e807c9bb63 Library call guard. 2021-01-11 20:37:44 +01:00
chriseth
67d21a87c5
Merge pull request #10737 from ethereum/range-v3
Add range-v3.
2021-01-11 19:24:13 +01:00
Daniel Kirchner
eac2bcf72f Add range-v3. 2021-01-11 18:44:55 +01:00
Djordje Mijovic
85b8325f0b [Sol->Yul] Implementing dynamic array push for arrays of structs. 2021-01-11 17:49:42 +01:00
Djordje Mijovic
b06936b11c [refactor] Move copying struct to storage to it's own util function. 2021-01-11 16:26:14 +01:00
Martin Blicha
ff76c989ac addressing review comments 2021-01-11 14:19:06 +01:00
Martin Blicha
dd43ce1578 fixing try/catch encoding for BMC, refactoring 2021-01-11 13:36:03 +01:00
Martin Blicha
55589a9eec [SMTChecker] Basic support for try-catch in BMC 2021-01-11 13:36:02 +01:00
Martin Blicha
0f3924186e [SMTChecker] Support try-catch in CHC engine 2021-01-11 13:36:02 +01:00
chriseth
994fdb7517 Determine encoding type earlier. 2021-01-11 11:57:22 +01:00
Leonardo Alt
11f56861c3 Refactor cex loop 2021-01-07 23:13:02 +01:00
Harikrishnan Mulackal
5241b7b761
Merge pull request #10684 from ethereum/fixIRWrappingExp
Use wrapping arithmetic for exp in unchecked blocks.
2021-01-06 18:53:54 +01:00
Alex Beregszaszi
8edfa26f0a Mark the empty version pragma as invalid 2021-01-04 19:28:36 +00:00
Leonardo Alt
b02722ebda Add contract name to called function in cex 2021-01-04 10:03:16 +01:00
Djordje Mijovic
047d693ac9 Refactoring copyLiteralToMemoryFunction and reusing it from other functions.
Co-authored-by: Leonardo <leo@ethereum.org>

Co-authored-by: Alex Beregszaszi <alex@rtfs.hu>
2020-12-30 17:31:20 +01:00
Djordje Mijovic
ddb05769a5 [Sol->Yul] Implementing type name. 2020-12-30 17:19:03 +01:00
Leonardo Alt
78d55e6b4a [SMTChecker] Support check/unchecked 2020-12-30 12:14:30 +01:00
Martin Blicha
be0a0f4d90 [SMTChecker] Added constraints for block properties 2020-12-29 22:17:44 +01:00
Leonardo Alt
9482e7de23 [SMTChecker] Fix calls to virtual/overriden functions 2020-12-29 11:25:20 +01:00
Martin Blicha
bb0003f5ea removed extra parameter from PredicateInstance::nondetInterface 2020-12-28 19:48:48 +01:00
Martin Blicha
f76ff35225 [SMTChecker] Detect errors caused by reentrancy 2020-12-28 14:32:53 +01:00
Suriyaa Sundararuban
8649df169d
Update Natspec documentation URL 2020-12-27 14:55:40 +01:00
chriseth
2ab83217e3 Use wrapping arithmetic for exp in unchecked blocks. 2020-12-22 16:49:55 +01:00
chriseth
04d83af1d2
Merge pull request #10492 from ethereum/arrayClearingDiffBaseSol2Yul
[Sol->Yul] Fixing array clearing when copying from storage to storage.
2020-12-22 15:15:03 +01:00
Martin Blicha
d90b9da4f0 [SMTChecker] Refactoring 2020-12-22 13:10:48 +01:00
chriseth
0437ee7ad9 Fix length check when decoding error data. 2020-12-22 11:08:44 +01:00
chriseth
b965446182 Catch panic. 2020-12-22 11:08:44 +01:00
Đorđe Mijović
b78443ac75
Merge pull request #10577 from ethereum/deleteMappingSol2Yul
[Sol->Yul] Skipping mapping types when deleting structs and arrays.
2020-12-21 20:08:51 +01:00
Leonardo
a48106ca1f
Merge pull request #10670 from blishko/smt-virtual-modifiers-fix
[SMTChecker] Fix virtual modifier called statically
2020-12-21 18:05:02 +01:00
Djordje Mijovic
adb9d0c41a [Sol->Yul] Fixing array clearing when copying from storage to storage. 2020-12-21 17:33:06 +01:00
Djordje Mijovic
2d5a2c65a8 [Sol->Yul] Implementing getters for bytes and structs containing bytes member.
Co-authored-by: chriseth <chris@ethereum.org>
2020-12-21 14:46:06 +01:00
Martin Blicha
87ef0e16f5 [SMTChecker] Fix virtual modifier called statically 2020-12-21 13:52:28 +01:00
Djordje Mijovic
9b8634f2a7 [Sol->Yul] Skipping mapping types when deleting structs and arrays. 2020-12-21 13:19:25 +01:00
Leonardo
158154bac3
Merge pull request #10345 from ethereum/ir-runtime
Output runtime object in IR
2020-12-18 17:19:40 +01:00
Alex Beregszaszi
7e20a095a8
Merge pull request #10652 from ethereum/smt_constants_inplce
[SMTChecker] Replace constants by their value in-place
2020-12-18 14:22:32 +00:00
chriseth
c4ade1753e
Merge pull request #10445 from ethereum/modifiers
[Sol->Yul] Implement function modifiers.
2020-12-18 14:29:00 +01:00
Leonardo Alt
034d1ab90f [SMTChecker] Replace constants by their value in-place 2020-12-18 14:22:28 +01:00
Alex Beregszaszi
b14a6a10cc Report meaningful error if parsing a version pragma failed 2020-12-18 11:50:37 +00:00
Martin Blicha
7078e8f8f8 [SMTChecker] Fix analysis of overriding modifiers 2020-12-17 17:05:54 +01:00
chriseth
35908c602b Modifiers for constructors. 2020-12-17 17:00:51 +01:00
chriseth
ccaa81fbe7 Implement function modifiers. 2020-12-17 17:00:51 +01:00
Leonardo Alt
2cbf33ca1c SMTChecker support ABI functions as UFs 2020-12-17 14:03:17 +01:00
Alex Beregszaszi
953d18c6cb Output runtime object in IR 2020-12-16 19:23:10 +00:00
Leonardo Alt
f5c96ea6da Fix constant evaluation build 2020-12-16 17:59:00 +01:00
chriseth
3a23df6717 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-16 16:56:45 +01:00
Leonardo Alt
80e85b772b [SMTChecker] Apply const eval to arithmetic binary expressions 2020-12-16 14:58:00 +01:00
Alex Beregszaszi
cad4f74012 Unary minus is not implemented for fixed point type 2020-12-15 18:02:10 +00:00
hrkrshnn
2fb191175b Disallow some explicit conversions to address payable
The following explicit conversions are disallowed:

1. uint160 -> address payable
2. bytes20 -> address payable
3. literals -> address payable (payable(0) is an exception)
2020-12-15 15:01:40 +01:00
chriseth
ffaf40950a
Merge pull request #10605 from ethereum/develop
Merge develop into breaking.
2020-12-15 14:01:01 +01:00
chriseth
2a54079d41
Merge pull request #10575 from ethereum/calldataArraySlices
Conversion of calldata array slices to memory
2020-12-15 12:21:33 +01:00
Martin Blicha
e2c27b8ea4 [SMTChecker] Fix internal error on constructor of a recursive struct 2020-12-15 09:53:52 +01:00
Djordje Mijovic
64f0120622 Change assertions to align to TypeChecker. 2020-12-15 09:21:50 +01:00
Martin Blicha
71f835b71b [SMTChecker] Fixed internal error when increment/decrement is applied on a result of push(). 2020-12-14 22:52:44 +01:00
Djordje Mijovic
8aa4568b10 [Sol->Yul] Implementing conversion from calldata slices to memory arrays.
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
2020-12-14 22:21:37 +01:00
Djordje Mijovic
b99a74fb34 Implementing conversion from calldata slices to memory arrays. 2020-12-14 22:21:37 +01:00
Djordje Mijovic
0efd52a38e Allowing implicit conversion from calldata slice to memory and storage array types. 2020-12-14 22:21:37 +01:00
hrkrshnn
f30c7cbac8 All explicit address conversions return a non-payable address 2020-12-14 18:41:27 +01:00
Martin Blicha
103fa3b7eb [SMTChecker] Fix internal error on abstract modifier 2020-12-14 18:23:25 +01:00
Martin Blicha
27402781c4 [SMTChecker] Fixed crash on push to bytes on lhs of an assignment 2020-12-14 17:40:45 +01:00
hrkrshnn
e1a95cfd42 Disallow conversions from literals to payable address
To get a payable address, one has to go through address. For example, `payable(address(0))`.
2020-12-14 16:55:48 +01:00
hrkrshnn
9bd778d728 Make msg.sender and tx.origin have type address
Previously both of them had type address payable. The idea is that anything that is not know to be
payable should be non-payable.
2020-12-14 16:55:48 +01:00
Martin Blicha
0be325dc0d [SMTChecker] Fix handling of function calls where the function identifier is nested in a tuple. 2020-12-14 16:19:24 +01:00
chriseth
e1e1337aca Move functions into anonymous namespace. 2020-12-14 14:18:03 +01:00