cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
14,822 Commits 348 Branches 121 Tags 100 MiB
301215f186
Commit Graph

300 Commits

Author SHA1 Message Date
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
Leonardo Alt
c8a017ccd6 [SMTChecker] Use unique_ptr instead of shared_ptr where applicable. 2019-05-09 16:34:22 +02:00
Leonardo Alt
6027383ae5 [SMTChecker] Fix call to function at state var init 2019-05-09 16:12:44 +02:00
Leonardo Alt
3d52a6ca68 [SMTChecker] Fix ICE in branch-inline function call-modify local variable 2019-05-09 09:15:11 +02:00
Leonardo Alt
9893cae27a [SMTChecker] Make mergeVariables deterministic 2019-05-08 20:46:01 +02:00
Leonardo Alt
0b046897ae [SMTChecker] Fix unsupported type assignment 2019-05-08 14:28:23 +02:00
Leonardo Alt
3c7540ceb2 [SMTChecker] Support tuples with multiple var decls 2019-05-07 16:57:27 +02:00
Leonardo Alt
2139c20776 [SMTChecker] Support delete 2019-05-06 18:32:10 +02:00
Leonardo
e99efec085
Merge pull request #6652 from ethereum/smt_tuple_function 
[SMTChecker] Support tuples as function calls with multiple return values
 2019-05-06 15:19:24 +02:00
Leonardo Alt
80712f44cb Fix short circuit with assignments 2019-05-06 11:04:43 +02:00
Leonardo Alt
5440a53d4d [SMTChecker] Support tuples as function calls with multiple return values 2019-05-03 06:10:22 +02:00
Leonardo Alt
204dcf1771 [SMTChecker] Support tuple assignments 2019-05-02 12:55:34 +02:00
Leonardo Alt
6c7527ac90 [SMTChecker] Support tuple type declaration 2019-05-02 12:05:21 +02:00
Leonardo Alt
66655b87b0 [SMTChecker] Fix ICE in fixed point operations 2019-05-02 10:59:23 +02:00
Leonardo Alt
dd4e938265 [SMTChecker] Fix ICE in inherited state var 2019-05-02 10:03:12 +02:00
Leonardo Alt
a6db37ac9c [SMTChecker] Fix bad cast in base constructor modifier. 2019-04-30 18:48:13 +02:00
Leonardo Alt
e4989369d0 Refactor cast from identifier ref decl to var decl 2019-04-30 11:08:36 +02:00
Leonardo Alt
762f79f84d Refactor assignment handling 2019-04-30 11:08:36 +02:00
Leonardo Alt
fc482de695 [SMTChecker] Support address members 2019-04-25 16:24:36 +02:00
Leonardo Alt
dd1afeba52 [SMTChecker] Support this as address 2019-04-18 17:56:52 +02:00
chriseth
fce19bde58
Merge pull request #6545 from ethereum/smt_contracts 
[SMTChecker] Support contract type
 2019-04-18 13:01:18 +02:00
Leonardo Alt
ecd89393ee [SMTChecker] Support contract type 2019-04-17 16:30:11 +02:00
Leonardo Alt
03d18f1b98 [SMTChecker] Add note about not inlining external function calls 2019-04-17 16:14:07 +02:00
Christian Parpart
721bf367a3
[libsolidity] TypeProvider: eliminate redundant "Type" suffix in provider function signatures. 2019-04-17 14:42:07 +02:00
Christian Parpart
862b65d6e3
[libsolidity] remove ReferenceType::copyForLocationIfReference (use TypeProvider instead) 2019-04-17 13:25:03 +02:00
Christian Parpart
58a45f2cb6 [libsolidity] TypeProvider: adds explicit uint256() accessor and removes default params in integerType(...). 2019-04-16 18:28:40 +02:00
Christian Parpart
bf43eebea9 libsolidity: Introducing TypeProvider API, for clear type system ownership. 2019-04-16 18:26:45 +02:00
Leonardo Alt
07fac9e381 [SMTChecker] Allow SymbolicVariable from smt::Sort 2019-04-15 14:52:46 +02:00
chriseth
bf5792f7ca
Merge pull request #6483 from ethereum/smt_support_mod 
[SMTChecker] Support mod
 2019-04-15 13:42:18 +02:00
chriseth
73ac8f6220
Merge pull request #6421 from ethereum/smt_fix_variable_usage 
[SMTChecker] Refactor VariableUsage
 2019-04-15 13:39:10 +02:00
Leonardo Alt
af9f16e014 [SMTChecker] Support mod 2019-04-12 12:39:25 +02:00
Leonardo Alt
4fe303530a [SMTChecker] Show unsupported warning for asm blocks 2019-04-05 16:41:15 +02:00
Leonardo Alt
79d8a4e13a [SMTChecker] Refactor VariableUsage 2019-04-05 11:38:37 +02:00
Leonardo Alt
aa9b9aa87e [SMTChecker] Support unary inc/dec for array/mapping access 2019-04-02 16:53:19 +02:00
chriseth
84251e5a22
Merge pull request #6405 from ethereum/smt_compound_assignment 
[SMTChecker] Support arithmetic compound assignment operators.
 2019-03-28 18:27:25 +01:00
Leonardo Alt
a7e826a224 [SMTChecker] Implement short circuit 2019-03-28 16:08:30 +01:00
Leonardo Alt
15269067b5 Support arithmetic compound assignment operators 2019-03-28 15:27:52 +01:00
Leonardo Alt
ecbf36f271 Refactor computing symbolic arithmetic operation 2019-03-28 15:27:36 +01:00
Leonardo Alt
1d63b97857 Take inlined function calls into account when collecting touched variables 2019-03-28 14:32:47 +01:00
Leonardo Alt
6f9b69ebc3 Refactor function that retrieves FunctionDefinition from FunctionCall 2019-03-28 14:32:47 +01:00
Leonardo Alt
a207d7f44c [SMTChecker] Add callstack model to overflow checks 2019-03-21 16:25:33 +01:00
Leonardo Alt
de89733bd6 [SMTChecker] Fix nullptr deref 2019-03-21 15:46:54 +01:00
Leonardo Alt
9659f40c8d [SMTChecker] Support modifiers 2019-03-20 11:32:20 +01:00
Leonardo Alt
3296fb3764 Add callstack to model report 2019-03-20 10:35:29 +01:00
Leonardo Alt
a8209e9899 [SMTChecker] Shortcut RationalNumber expressions 2019-03-11 12:53:49 +01:00
Leonardo Alt
02d0e609b9 [SMTChecker] Support enums 2019-03-07 15:15:12 +01:00
Leonardo Alt
29b2ab6f66 Handle aliasing 2019-03-06 11:29:54 +01:00
Leonardo Alt
467c34999f Do not throw on string literals 2019-03-06 11:29:26 +01:00
Leonardo Alt
e74f58130e Add SMT type support to Solidity arrays 2019-03-06 11:29:26 +01:00
Mathias Baumann
f782125463 Fix SMT Checker crash due to missing type information 2019-02-28 11:55:45 +01:00
Leonardo Alt
bbd2c91e19 [SMTChecker] Replace dynamic_cast by category check 2019-02-26 00:47:59 +01:00
Leonardo Alt
34470f3549 [SMTChecker] Only check for overflow/underflow in the end of the function 2019-02-18 23:55:58 +01:00
chriseth
cb0ad2266c
Merge pull request #6008 from ethereum/smt_fix_abstract_assignment 
[SMTChecker] Assert type is not function when assigning
 2019-02-18 14:54:20 +01:00
Leonardo Alt
22cdfb18d4 [SMTChecker] Assert type is not function when assigning 2019-02-14 13:32:56 +01:00
Daniel Kirchner
8ca6715e18 More style checks. 2019-02-14 11:41:20 +01:00
Leonardo Alt
637546850f [SMTChecker] Add mod operator 2019-02-07 14:24:40 +01:00
Leonardo Alt
9a33367bc6 [SMTChecker] Warn when no solver was found and there are unhandled queries. 2019-01-29 14:29:07 +01:00
Leonardo Alt
7f8ceaadab [SMTChecker] Clear state knowledge after external function calls 2019-01-21 12:58:40 +01:00
Leonardo Alt
a10db051de [SMTChecker] Support basic typecast 2019-01-16 13:00:54 +01:00
Leonardo Alt
cce377833a Sort includes in libsolidity/formal 2018-12-17 18:26:10 +01:00
Leonardo Alt
9199718ec0 Clear all mapping knowledge after array variable assignment 2018-12-14 12:21:53 +01:00
Leonardo Alt
6a2809a582 [SMTChecker] Support to mapping 2018-12-14 12:21:53 +01:00
Leonardo Alt
08737e43dc [SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions 2018-12-11 11:28:25 +01:00
Leonardo Alt
de46bb2c42 [SMTChecker] Introduce SymbolicFunctionVariable 2018-12-10 11:34:29 +01:00
Kevin Kelley
fb6fd1b3c2 add a 'readable' format for large hex values 2018-12-05 22:15:02 +01:00
Leonardo Alt
b9f424e373 [SMTChecker] Simplify symbolic variables 2018-12-05 09:56:52 +01:00
Leonardo Alt
8069bb61da [SMTChecker] Loops are unrolled once 2018-12-04 12:35:19 +01:00
Leonardo Alt
6d41ffb4a5 [SMTChecker] Remove unary plus operator 2018-12-03 10:35:38 +01:00
Leonardo Alt
2f6de12e8c [SMTChecker] Make smt::Sort::operator== virtual 2018-11-30 10:41:15 +01:00
chriseth
9e9250c961 Fix move bug. 2018-11-29 15:32:38 +01:00
Leonardo Alt
aaaa92012c [SMTChecker] Unknown answer for constant condition check should not do anything 2018-11-26 12:54:02 +01:00
Leonardo Alt
6251a289dd Testing with smtlib2 interface always there 2018-11-23 09:43:49 +01:00