chriseth
|
96d777d7f1
|
Merge commit 'a7d481fb9' into develop_060
|
2019-12-03 20:47:30 +01:00 |
|
Leonardo Alt
|
b1577f5e46
|
[SMTChecker] Fix ICE in array of structs type
|
2019-12-03 01:12:30 +01:00 |
|
Leonardo
|
a7d481fb94
|
Merge pull request #7851 from ethereum/smt_fix_function_type
[SMTChecker] Fix ICE for arrays and mappings of functions.
|
2019-11-30 13:15:08 +01:00 |
|
Leonardo
|
767ce4417f
|
Merge pull request #7850 from ethereum/smt_fix_typetype
[SMTChecker] Fix visit to IndexAccess that has type Type
|
2019-11-29 18:18:26 +01:00 |
|
Leonardo Alt
|
5adc2a40b9
|
[SMTChecker] Fix ICE for arrays and mappings of functions.
|
2019-11-29 18:06:44 +01:00 |
|
Leonardo Alt
|
9eda95caf9
|
[SMTChecker] Fix visit to IndexAccess that has type Type
|
2019-11-29 17:20:50 +01:00 |
|
Leonardo Alt
|
c09da092d2
|
[SMTChecker] Fix constructors with local vars
|
2019-11-29 16:59:15 +01:00 |
|
Leonardo Alt
|
a352abe00d
|
[SMTChecker] Add support to constructors
|
2019-11-28 14:43:23 +01:00 |
|
chriseth
|
f7fc42d8c3
|
Merge pull request #7826 from ethereum/develop
Merge develop into develop_060
|
2019-11-28 13:37:19 +01:00 |
|
Leonardo Alt
|
240ff30878
|
[SMTChecker] Do not visit the name of a modifier invocation
|
2019-11-27 22:34:33 +01:00 |
|
Leonardo Alt
|
ddc478e3e4
|
Add CallbackKind and use it for the SMT solver
|
2019-11-21 22:10:21 +00:00 |
|
Erik K
|
94272d44aa
|
Merge pull request #7745 from ethereum/develop
Merge develop into develop_060
|
2019-11-19 15:30:31 +01:00 |
|
Leonardo Alt
|
d818746e0c
|
[SMTChecker] Fix ICE in abi.decode
|
2019-11-18 13:15:10 +01:00 |
|
chriseth
|
216e1749f4
|
Merge remote-tracking branch 'origin/develop' into develop_060
|
2019-11-14 13:42:46 +01:00 |
|
Leonardo Alt
|
8efacfb545
|
[SMTChecker] Fix ICE in string literal to fixed bytes implicit conversion
|
2019-11-13 22:25:18 +01:00 |
|
Leonardo Alt
|
e3652627fd
|
[SMTChecker] Fix ICE in CHC when function used as argument
|
2019-11-13 15:11:30 +01:00 |
|
chriseth
|
2e5a42836c
|
Merge pull request #7681 from ethereum/develop
Merge develop into develop_060
|
2019-11-11 16:42:03 +01:00 |
|
Leonardo Alt
|
5dacaf57bc
|
Fix ICE in FixedBytes IndexAccess
|
2019-11-08 17:29:40 +01:00 |
|
Leonardo Alt
|
fc945880d1
|
[SMTChecker] Fix override tests
|
2019-11-07 11:49:32 +01:00 |
|
Leonardo Alt
|
6b10efff8c
|
Add CHCSmtLib2Interface
|
2019-11-07 11:12:11 +01:00 |
|
chriseth
|
21e65076b3
|
Merge pull request #7650 from ethereum/develop
Merge develop into develop_060
|
2019-11-06 21:56:55 +01:00 |
|
Leonardo Alt
|
10e70b8603
|
[SMTChecker] Support inheritance and resolve overrides
|
2019-11-06 11:00:06 +01:00 |
|
chriseth
|
4d99bf68f4
|
Merge pull request #7638 from ethereum/develop
Merge develop into develop_060
|
2019-11-05 17:33:54 +01:00 |
|
Leonardo Alt
|
c5e081dc8c
|
[SMTChecker] Refactor CHC loops and add if blocks
|
2019-11-05 09:28:59 +01:00 |
|
chriseth
|
46ac16d25c
|
Merge remote-tracking branch 'origin/develop' into develop_060
|
2019-11-04 19:09:11 +01:00 |
|
Daniel Kirchner
|
3321fc56ea
|
Split fallback function and introduce "fallback()" and "receive()" syntax.
|
2019-11-04 17:17:58 +01:00 |
|
Leonardo Alt
|
8a42e3f87a
|
[SMTChecker] Support assignments to m-d arrays and mappings
|
2019-10-28 17:27:39 +01:00 |
|
Leonardo
|
ca714a2d3d
|
Merge pull request #7485 from ethereum/develop
Merge develop into develop_060
|
2019-09-26 15:43:12 +02:00 |
|
Leonardo Alt
|
83ef34f41d
|
[SMTChecker] Fix SMT name for function identifiers
|
2019-09-24 11:23:10 +02:00 |
|
Leonardo Alt
|
ed9674be8d
|
[SMTChecker] Add as const function to SMTLib2Interface
|
2019-09-18 22:57:14 +02:00 |
|
chriseth
|
5b3efee93b
|
Merge pull request #7442 from ethereum/develop
Merge develop into develop_060
|
2019-09-17 12:16:27 +02:00 |
|
Leonardo Alt
|
e1c238e25f
|
[SMTChecker] Add loop support
|
2019-09-13 12:40:53 +02:00 |
|
Daniel Kirchner
|
4782c800ec
|
Initial introduction of array slices with partial implementation for dynamic calldata arrays.
|
2019-09-13 10:57:53 +02:00 |
|
Leonardo Alt
|
a51577facf
|
Fix Windows build
|
2019-09-02 22:37:30 +02:00 |
|
Leonardo Alt
|
a774b2d905
|
[SMTChecker] Zero-initialize arrays
|
2019-09-02 22:37:30 +02:00 |
|
Leonardo Alt
|
214e5c6369
|
[SMTChecker] Fix index access type type error
|
2019-08-27 16:39:19 +02:00 |
|
Leonardo Alt
|
1a70a46f9b
|
[CHC] Add function blocks and check asserts
|
2019-08-15 12:25:15 +02:00 |
|
Leonardo
|
cbac3a4208
|
Merge pull request #7107 from ethereum/smt_chc_constructor_interface
[SMTChecker] Add CHC constructor/interface/error blocks
|
2019-08-12 15:06:08 +02:00 |
|
Leonardo Alt
|
bef6228810
|
[SMTChecker] Create CHC constructor/interface/error blocks
|
2019-08-12 12:34:57 +02:00 |
|
Leonardo Alt
|
360f868836
|
[SMTChecker] Fix literal string type mismatch
|
2019-08-10 21:51:46 +02:00 |
|
Leonardo Alt
|
4214cd1354
|
[SMTChecker] Fix ICE when reporting cex concerning state vars from different source files
|
2019-08-10 20:56:52 +02:00 |
|
Leonardo
|
67c855e93e
|
Merge pull request #7170 from ethereum/smt_fix_other_contract_state_var
[SMTChecker] Fix ICE when inlining functions from different source
|
2019-08-09 19:14:28 +02:00 |
|
Leonardo Alt
|
7b22496b1f
|
[SMTChecker] Fix ICE when inlining functions that use state vars and are in a different source
|
2019-08-09 17:50:52 +02:00 |
|
Leonardo Alt
|
11d8cf588e
|
[SMTChecker] Set unknown values for return variables of recursive functions
|
2019-08-09 17:01:08 +02:00 |
|
Leonardo Alt
|
369f8cd97f
|
[SMTChecker] CHC create function return variables
|
2019-08-05 12:36:51 +02:00 |
|
Leonardo
|
11632966c9
|
Merge pull request #7171 from ethereum/smt_fix_compound_bitwise
[SMTChecker] Fix ICE compound bitwise op inside branch
|
2019-08-05 12:15:01 +02:00 |
|
Leonardo Alt
|
d5fb8cf58a
|
[SMTChecker] Fix ICE compound bitwise op inside branch
|
2019-08-02 20:02:39 +02:00 |
|
Leonardo Alt
|
7b5863e583
|
Do not erase knowledge about storage pointers when another pointer is assigned
|
2019-08-02 13:09:06 +02:00 |
|
chriseth
|
04f298fd0e
|
Merge pull request #7132 from ethereum/smt_acc_solver
[SMTChecker] EncodingContext config flag to accumulate assertions
|
2019-08-01 13:04:37 +02:00 |
|
Leonardo Alt
|
44d7c6976a
|
Erase pointer knowledge properly inside loops
|
2019-07-30 12:47:50 +02:00 |
|
Leonardo
|
00accd9daa
|
Merge pull request #7141 from ethereum/smt_fix_json
[SMTChecker] Reset SSA index to 0 instead of increasing in context reset
|
2019-07-29 10:20:06 +02:00 |
|
Leonardo
|
0197a200cd
|
Merge pull request #7142 from ethereum/smt_init_numbers
[SMTChecker] Initialize all number types with 0
|
2019-07-29 10:19:17 +02:00 |
|
Leonardo Alt
|
847f574e22
|
[SMTChecker] Fix ICE when inlining function with tuple expression
|
2019-07-26 16:29:29 +02:00 |
|
Leonardo Alt
|
cd5a5b3686
|
[SMTChecker] Initialize all number types with 0
|
2019-07-25 15:15:18 +02:00 |
|
Leonardo Alt
|
6bcbeb1d23
|
[SMTChecker] Reset SSA index to 0 instead of increasing in context reset
|
2019-07-25 14:16:34 +02:00 |
|
Leonardo
|
264035f0dd
|
Merge pull request #7120 from ethereum/smt_refactor_inlining
[SMTChecker] Refactor function inlining
|
2019-07-22 14:20:32 +02:00 |
|
Leonardo Alt
|
b204f27047
|
[SMTChecker] EncodingContext config flag to accumulate assertions
|
2019-07-19 19:31:25 +02:00 |
|
Leonardo Alt
|
03cc124f32
|
Add CHC skeleton
|
2019-07-19 11:52:05 +02:00 |
|
Leonardo Alt
|
382df64899
|
[SMTChecker] Refactor function inlining
|
2019-07-18 13:56:48 +02:00 |
|
Leonardo Alt
|
71144d0d39
|
[CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface
|
2019-07-15 17:31:39 +02:00 |
|
Leonardo
|
75eb67c3e0
|
Merge pull request #7050 from ethereum/smt_set_solver
[SMTChecker] EncodingContext's solver needs to be set dynamically
|
2019-07-08 15:19:55 +02:00 |
|
Leonardo Alt
|
96b0c4c148
|
[SMTChecker] New VariableUsage flag to inline functions
|
2019-07-08 14:40:33 +02:00 |
|
Leonardo Alt
|
01570bbc8c
|
EncodingContext's solver needs to be set dynamically
|
2019-07-08 14:40:15 +02:00 |
|
chriseth
|
25928767b7
|
Merge pull request #7058 from ethereum/smt_reset_context
[SMTChecker] Clear encoding context before engine starts
|
2019-07-08 12:36:50 +02:00 |
|
Leonardo Alt
|
be663680d4
|
[SMTChecker] Clear encoding context before engine starts
|
2019-07-08 11:56:04 +02:00 |
|
Leonardo Alt
|
4aebdcc442
|
[SMTChecker] Allow FunctionSort to be created via sort and not type
|
2019-07-04 12:00:24 +02:00 |
|
Leonardo Alt
|
934e00d235
|
[SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars
|
2019-07-03 16:05:56 +02:00 |
|
chriseth
|
817852c650
|
Merge pull request #7030 from ethereum/smt_move_solver
[SMTChecker] Move solver from SMTEncoder to BMC
|
2019-07-02 14:08:55 +02:00 |
|
chriseth
|
e542e46163
|
Merge pull request #7022 from ethereum/smt_create_expr
[SMTChecker] Always create symbolic expression
|
2019-07-02 14:07:24 +02:00 |
|
chriseth
|
ca10b59b25
|
Merge pull request #7020 from ethereum/smt_fix_callstack_message
[SMTChecker] Fix wrong assertion in callstack message
|
2019-07-02 13:47:49 +02:00 |
|
Leonardo Alt
|
b0818bd002
|
[SMTChecker] Move solver pointer from SMTEncoder to BMC
|
2019-07-02 12:06:52 +02:00 |
|
Leonardo Alt
|
fb3c85633b
|
Always create symbolic expression
|
2019-07-01 16:25:33 +02:00 |
|
Leonardo Alt
|
75663dc91e
|
[SMTChecker] Fix require with message
|
2019-07-01 16:17:06 +02:00 |
|
Leonardo Alt
|
6606a13ed2
|
[SMTChecker] Remove unsound assertion (too strong)
|
2019-07-01 16:16:39 +02:00 |
|
Leonardo Alt
|
3cb4ed83c1
|
[SMTChecker] Split SMTChecker into SMTEncoder and BMC
|
2019-07-01 15:05:03 +02:00 |
|
Leonardo Alt
|
a28b84fdc3
|
[SMTChecker] Add a more general VerificationTarget
|
2019-06-27 10:31:50 +02:00 |
|
Leonardo Alt
|
48d6729164
|
[SMTChecker] Remove overflow check for assignments
|
2019-06-24 17:58:56 +02:00 |
|
Leonardo Alt
|
ed275fd760
|
[SMTChecker] Collect assertions in EncodingContext
|
2019-06-24 15:03:00 +02:00 |
|
Leonardo Alt
|
1221eeebf1
|
[SMTChecker] Report malformed expressions more precisely
|
2019-06-06 11:54:29 +02:00 |
|
Leonardo Alt
|
f281c94b42
|
[SMTChecker] Test that non-Boolean literals are actually integers
|
2019-06-05 10:51:05 +02:00 |
|
Leonardo
|
3a3316393e
|
Merge pull request #6897 from ethereum/smt_check_pragma_earlier
[SMTChecker] Exit early if no pragma
|
2019-06-05 10:26:25 +02:00 |
|
Leonardo
|
c39ea56f93
|
Merge pull request #6896 from ethereum/smt_use_portfolio
[SMTChecker] Use SMTPortfolio directly
|
2019-06-05 10:26:05 +02:00 |
|
Leonardo
|
155af48b9d
|
Merge pull request #6895 from ethereum/smt_keep_assertions
[SMTChecker] Keep a copy of assertions that are added to the solvers
|
2019-06-05 10:25:45 +02:00 |
|
Leonardo Alt
|
4de1e20954
|
[SMTChecker] Exit early if no pragma
|
2019-06-04 17:12:15 +02:00 |
|
Leonardo Alt
|
91653526bb
|
[SMTChecker] Use SMTPortfolio directly instead of pointer to SolverInterface
|
2019-06-04 17:10:52 +02:00 |
|
Leonardo Alt
|
31ef421fff
|
[SMTChecker] Keep a copy of assertions that are added to the solvers
|
2019-06-04 17:09:04 +02:00 |
|
Leonardo Alt
|
d9ce9cab99
|
[SMTChecker] Use smtlib's implies instead of \!a or b
|
2019-06-04 14:23:44 +02:00 |
|
chriseth
|
e08f521b7e
|
Merge pull request #6764 from ethereum/smt_fix_tuple_ice
[SMTChecker] Fix ICE in unsupported function calls with multi return values
|
2019-05-20 15:18:11 +02:00 |
|
Leonardo Alt
|
60a4f03d3d
|
[SMTChecker] Fix ice in unsupported functions with multi return values
|
2019-05-16 18:23:42 +02:00 |
|
Leonardo Alt
|
5493a41842
|
[SMTChecker] Move global variables and functions to encoding context
|
2019-05-16 18:11:31 +02:00 |
|
Leonardo Alt
|
4e430ba0ae
|
[SMTChecker] Move expression handling to EncodingContext
|
2019-05-14 15:56:43 +02:00 |
|
Leonardo Alt
|
ebbe03cad6
|
[SMTChecker] Move variable handling to EncodingContext
|
2019-05-13 16:59:28 +02:00 |
|
chriseth
|
01dd9ba2ae
|
Merge pull request #6717 from ethereum/smt_namespace
Move SMT specific code into smt namespace
|
2019-05-13 12:45:34 +02:00 |
|
chriseth
|
e5d46767f1
|
Merge pull request #6722 from ethereum/smt_fix_variable_usage
[SMTChecker] Fix VariableUsage for IndexAccess
|
2019-05-13 10:17:26 +02:00 |
|
Leonardo Alt
|
fac383a233
|
Move SMT specific code into smt namespace
|
2019-05-10 20:03:11 +02:00 |
|
chriseth
|
cc40e65a4b
|
Merge pull request #6712 from ethereum/smt_unique_ptr
[SMTChecker] Use unique_ptr instead of shared_ptr where applicable
|
2019-05-10 12:53:53 +02:00 |
|
Leonardo Alt
|
3ea5c112d3
|
[SMTChecker] Fix VariableUsage for IndexAccess
|
2019-05-10 11:28:10 +02:00 |
|
Leonardo Alt
|
8d65fd18fc
|
[SMTChecker] Style changes
|
2019-05-09 19:15:43 +02:00 |
|
chriseth
|
89700dbcff
|
Merge pull request #6665 from ethereum/smt_inline_external_this
[SMTChecker] Inline external function calls to `this`
|
2019-05-09 19:09:08 +02:00 |
|
Leonardo Alt
|
ef32bf185f
|
[SMTChecker] Inline external function calls to this.
|
2019-05-09 16:53:30 +02:00 |
|