Leonardo
7405dc5b7f
Merge pull request #10836 from ethereum/smt_fix_cex_inheritance
...
Fix inheritance bug in CHC cex
2021-02-03 18:49:25 +01:00
Martin Blicha
d99256aae7
[SMTChecker] refactoring of resetting storage variables
2021-02-03 15:53:58 +01:00
Martin Blicha
f1013427a7
[SMTChecker] refactoring the accessing the encoding state
2021-02-03 15:53:58 +01:00
Leonardo Alt
665ce27c18
Fix inheritance bug in CHC cex
2021-02-02 18:06:32 +01:00
Martin Blicha
a49950cdf3
[SMTChecker] Added transaction constraints also for contract deployment
2021-02-01 16:46:34 +01:00
Leonardo Alt
545305a31f
[SMTChecker] Fix super and virtual
2021-01-28 18:51:29 +01:00
Martin Blicha
deb90d84a6
[SMTChecker] added missing type constraints for Address
2021-01-27 20:39:24 +01:00
Martin Blicha
484e67815a
[SMTChecker] Basic support for inline assembly using over-approximating analysis
2021-01-26 16:20:50 +01:00
chriseth
e9dc9c5baf
Fix merge conflict.
2021-01-26 13:53:22 +01:00
chriseth
4697beeab2
Merge pull request #10769 from ethereum/allocationCleanup
...
Cleanup allocation.
2021-01-26 11:58:11 +01:00
hrkrshnn
526ceec152
Implement IR shortcut for <address>.code.length
2021-01-26 11:07:04 +01:00
hrkrshnn
d6d880dc53
Old codegen: implemented shortcut for <address>.code.length
2021-01-26 11:07:04 +01:00
hrkrshnn
ec57c791ef
Fix infinite loop when accessing circular constants from inline assembly.
2021-01-26 09:22:05 +01:00
Mathias Baumann
07a1d230cd
Fix missing error when accessing unintialized variables.
2021-01-25 14:44:15 +01:00
chriseth
ccdf57c9b1
Merge pull request #10700 from ethereum/whiskers_check_template_contains_tag
...
[whiskers] Add check that template contain tags.
2021-01-25 14:17:05 +01:00
Leonardo Alt
a612daa783
Add msgvalue to cex
2021-01-21 19:05:44 +01:00
Alexander Arlt
061fecbc90
[whiskers] Add check that template contain tags.
2021-01-20 15:26:34 -05:00
Leonardo
a75b87c80e
Merge pull request #10813 from ethereum/smt_targets_option
...
Add CLI and JSON option to select SMTChecker targets
2021-01-20 18:37:08 +01:00
chriseth
3cc07694ed
Cleanup allocation.
2021-01-20 18:25:27 +01:00
Leonardo Alt
3b23cadbdc
Add CLI and JSON option to select SMTChecker targets
2021-01-20 17:35:37 +01:00
chriseth
1fcc76a562
Fix empty packed encoder.
2021-01-19 15:50:04 +01:00
Leonardo
9bde92ca20
Merge pull request #10807 from ethereum/fixIRReasonStrings
...
Properly omit require revert strings in IR code generator if requested.
2021-01-19 10:31:15 +01:00
Leonardo
957e9995a0
Merge pull request #10801 from blishko/issue-10793
...
[SMTChecker] Gather local variables also from nested try/catch clauses
2021-01-18 22:37:16 +01:00
chriseth
185e129657
Merge pull request #10776 from ethereum/fixABIEncoderWithSignature
...
Fix abi encode with signature shortcut.
2021-01-18 19:07:56 +01:00
chriseth
a3ee334b42
Omit require revert strings in IR code generator.
2021-01-18 18:47:55 +01:00
Martin Blicha
35d228d9b6
[SMTChecker] Gather local variables also from nested try/catch clauses
2021-01-18 18:30:18 +01:00
Leonardo Alt
c7ca87c012
Fix static virtual resolution
2021-01-18 16:23:38 +01:00
chriseth
4f3839e4ba
Fix abi encode with signature shortcut.
2021-01-18 13:44:52 +01:00
Djordje Mijovic
a0c80c2bdb
[Sol->Yul] Enabling copying_bytes_multiassign test via ir.
2021-01-18 12:40:51 +01:00
Martin Blicha
18214d1ccc
[SMTChecker] Reset checked/unchecked flag to the default value when inlining function in BMC
2021-01-15 15:36:26 +01:00
Leonardo Alt
007d39871b
[SMTChecker] Synthesize untrusted functions called externally
2021-01-15 11:56:26 +01:00
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
chriseth
28374447d2
Merge pull request #10582 from ethereum/addr-literal
...
Fix crash with oversized address literals
2020-12-14 12:14:28 +01:00
chriseth
561280a5cc
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-14 11:33:40 +01:00
Alex Beregszaszi
33ff2b16ff
Fix crash with oversized address literals
2020-12-11 23:45:23 +00:00
Leonardo
db9aa36d6c
Merge pull request #10567 from blishko/unary-operators-fix
...
[SMTChecker] Fix CHC analysis of increment/decrement
2020-12-11 18:52:12 +01:00
Leonardo
da9cede0fe
Merge pull request #10348 from ethereum/simplify-compiler
...
Simplify abstraction of Compiler/CompilerContext/CompilerStack
2020-12-11 17:42:36 +01:00
Martin Blicha
8927015e5a
[SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine
2020-12-11 17:41:50 +01:00
Alex Beregszaszi
bcaefb57b8
Add evmAssembly and evmRuntimeAssembly pointer in CompilerStack
...
This is a preparation for allowing those outputs to be served from the IR too
2020-12-11 14:53:29 +00:00
Alex Beregszaszi
98d8174d31
Simplify Compiler/CompilerContext by removing extra layers of indirection
2020-12-11 14:43:51 +00:00
chriseth
baaf7c0db8
Implement address(...).code in the IR
2020-12-11 03:00:30 +00:00
Alex Beregszaszi
7b347b9ec2
Introduce address(...).code
2020-12-11 03:00:30 +00:00
Alex Beregszaszi
fa37e69c25
Improved error messages when converting to/from builtin functions
2020-12-10 22:38:15 +00:00
Đorđe Mijović
9e4f3bad06
Merge pull request #10569 from ethereum/byteArrayStorageStorage
...
Fix copying byte arrays from storage to storage.
2020-12-10 22:52:50 +01:00
Alex Beregszaszi
bd641a5206
Enable more C++ compiler warnings
2020-12-10 21:03:58 +00:00
chriseth
7764ee8d86
Fix copying byte arrays from storage to storage.
2020-12-10 21:47:37 +01:00
Alex Beregszaszi
7cd05bf603
Introduce block.chainid
2020-12-10 17:07:54 +00:00
Daniel Kirchner
c400c61fc3
Fix incorrect behaviour on clang 6.
2020-12-10 17:20:30 +01:00
chriseth
d0551b67d7
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-10 17:07:56 +01:00
Daniel Kirchner
7308abc084
Allow loading Z3 dynamically at runtime.
2020-12-10 16:47:47 +01:00
chriseth
4861c9b8d1
Merge pull request #10554 from ethereum/emptyBytesPushSol2Yul
...
[Sol->Yul] Implementing empty byte array push.
2020-12-10 12:19:07 +01:00