cerc-io/solidity
16
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,105 Commits 348 Branches 121 Tags 100 MiB
be663680d4
Commit Graph

256 Commits

Author SHA1 Message Date
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
Leonardo Alt
dee0c4ded8 Error message stays in the SMTChecker 2018-11-23 09:43:49 +01:00
Leonardo Alt
f3c2309c73 Display better error message in SMTLib2 2018-11-23 09:43:49 +01:00
chriseth
54bed454f6 Rename function and warn if responses are supplied for Z3. 2018-11-23 09:43:49 +01:00
chriseth
bb10be789c Inject SMTLIB2 queries and responses via standard-json-io. 2018-11-23 09:43:49 +01:00
chriseth
d686807153 Style 2018-11-22 21:13:02 +01:00
Leonardo Alt
ec84a7dc9b [SMTChecker] Refactor setZeroValue and setUnknownValue 2018-11-22 16:42:51 +01:00
Leonardo Alt
20accf1a90 [SMTChecker] Add ArraySort and array operations 2018-11-22 14:04:20 +01:00
Leonardo Alt
13a142b039 [SMTChecker] Add FunctionSort and refactors the solver interface to create variables 2018-11-22 10:04:04 +01:00
Christian Parpart
d67322a186 Introduce namespace langutil in liblangutil directory. 
Also:
- Use {}-style list initialisation for SourceLocation construction
- Introduce new system includes
- Changes the API of the Scanner to take source as value (with move) as opposed to as a reference
 2018-11-21 19:13:44 +00:00
Christian Parpart
87821c53c3 Isolating files shared between Yul- and Solidity language frontend. 2018-11-21 18:58:12 +00:00
Alex Beregszaszi
2c6e1888eb
Merge pull request #5466 from ethereum/smt_refactor_sort_patch1 
[SMTChecker] Refactor smt::Sort and its usage
 2018-11-21 15:17:58 +00:00
Leonardo Alt
01ce43e51b [SMTChecker] Refactor smt::Sort and its usage 2018-11-21 15:46:47 +01:00
mordax
ea8b7d803e Removing redundant virtual from override function declaration 
Remove trailing whitespace

Remove changelog change
 2018-11-21 14:37:32 +00:00
Leonardo Alt
06c3f0953a [SMTChecker] Support bound function calls 2018-11-19 15:29:00 +01:00
Leonardo Alt
70bb0eaf95 [SMTChecker] Implement uninterpreted functions and use it for blockhash() 2018-11-15 09:12:42 +01:00
Leonardo Alt
9a4fd946c3 Add Scanner function that prints source based on SourceLocation 2018-11-13 13:49:29 +01:00
Leonardo Alt
d8cbf321da Grouping of symbolic variables in the same file and support to FixedBytes 2018-10-25 09:30:48 +02:00
chriseth
01566c2e1a
Merge pull request #5272 from ethereum/smt_special_vars 
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
 2018-10-24 14:34:17 +02:00
Leonardo Alt
e2cf5f6ed9 Add gasleft constraint and use full member access name 2018-10-22 18:19:11 +02:00
Christian Parpart
f112377dd4
Refactor solidity::Token into an enum class with TokenTraits helper namespace 2018-10-22 17:00:51 +02:00
Leonardo Alt
b46b827c30 [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash 2018-10-19 15:52:16 +02:00
Leonardo Alt
070471d8d4 Fix possibly effectless map emplace 2018-10-17 19:00:38 +02:00
Leonardo Alt
c92d3b537d [SMTChecker] Refactor expressions such that they also use SymbolicVariable 2018-10-17 18:36:24 +02:00
Leonardo
3db1ce0e14
Merge pull request #5235 from ethereum/smt_refactor_types 
[SMTChecker] Refactoring types
 2018-10-17 18:35:48 +02:00
Bhargava Shastry
67fd3ca4a7 Retained move/copy semantics; removed const qualifier from Expression's members name (of type std::string) and arguments (of type std::vector<Expression>) 2018-10-17 16:46:18 +02:00
Bhargava Shastry
546b08c158 Fix compiler warning: clang-8 warns of explicitly-defined op implicitly deleted for Expression object's copy and move constructors 2018-10-17 16:42:51 +02:00
Leonardo Alt
afe83cc28b Refactor SymbolicAddressVariable and SymbolicVariable allocation 2018-10-17 15:58:13 +02:00
Leonardo Alt
aa23326e06 Consistent renaming of 'counters' and 'sequence' to 'index' 2018-10-17 15:58:13 +02:00
Leonardo Alt
ec39fdcb3c [SMTChecker] Refactoring types 2018-10-17 15:58:13 +02:00
chriseth
2384947521
Merge pull request #5209 from ethereum/smt_ssa_refactor 
[SMTChecker] Refactor SSAVariable such that it only uses Type and not Declaration
 2018-10-15 16:49:47 +02:00
Leonardo Alt
e4851cf59e [SMTChecker] Inline calls to internal functions 2018-10-15 15:11:21 +02:00
Leonardo Alt
4a4620ac95 Refactor SSAVariable such that it only uses Type and not Declaration 2018-10-15 14:20:54 +02:00
Alex Beregszaszi
fa0ce6a7e7 Use empty() instead of size() == 0 2018-10-09 04:29:37 +01:00
Anurag Dashputre
3321000f67 Removing extra default cases to force compile time error, instead of runtime. 2018-09-30 12:40:38 +05:30
Daniel Kirchner
87804b6419 Split IntegerType into IntegerType and AddressType. 2018-09-05 12:19:14 +02:00
Daniel Kirchner
9b4546c487 Add workarounds for building against CVC4 on ArchLinux. 2018-08-08 19:02:59 +02:00
Alex Beregszaszi
f024efb7ab SMT: do not crash on referencing MagicVariableDeclaration 2018-08-07 20:43:20 +01:00
Alex Beregszaszi
6003ed2abd
Merge pull request #4603 from ethereum/smtlib2 
[SMTLib2] Fix repeated declarations
 2018-08-02 12:04:58 +01:00
Leonardo Alt
90f319615f SMT model variables are sorted and printed as secondary source location 2018-08-01 23:27:46 +02:00
Leonardo Alt
b6a2655513 Replace "value" by "<result>" in the SMT model 2018-08-01 23:27:11 +02:00
Leonardo Alt
41ac3d6cfb Remove repeated declarations in Z3 and CVC4 as well 2018-08-01 11:12:56 +02:00
Alex Beregszaszi
179427fd65 Import dev::solidity namespace in SMTPortfolio 2018-07-27 23:17:17 +01:00
Leonardo Alt
f249f9c86f [SMTLib2] Fix repeated declarations 2018-07-27 17:34:44 +01:00
Alex Beregszaszi
dea0567e06 Fix unterminated parentheses typo in SMTLib2 
Found by @leonardoalt
 2018-07-27 17:33:53 +01:00
Leonardo Alt
55c1fb60b4 [SMTChecker] Add CheckResult::CONFLICTING 2018-07-27 16:16:26 +01:00
Leonardo Alt
87a38e1abe [SMTChecker] SMTPortfolio: use all SMT solvers available 2018-07-27 16:15:34 +01:00
Leonardo Alt
b356f6a7f9 Setting timeout to Z3 and CVC4 2018-07-27 16:01:48 +02:00
Leonardo Alt
06dbcb3afe Only ask for a model if it's SAT 2018-07-27 14:13:22 +02:00
Alex Beregszaszi
ae15b52d93
Merge pull request #4565 from ethereum/smt-stringutils-crash 
Add assert for both branches in mergeVariables in SMTChecker
 2018-07-25 11:08:47 +01:00
Alex Beregszaszi
a5a61a0b77 More consistent catch statements 
Also take const& in all cases.
 2018-07-25 01:18:09 +01:00
Alex Beregszaszi
d30a6de942 Add better warning on binary operation on non-integer types in SMT Checker 2018-07-24 23:23:54 +01:00
Alex Beregszaszi
278372c13d Add assert for both branches in mergeVariables in SMTChecker 2018-07-24 22:43:05 +01:00
Cryptomental
140dbfdbd8 Code, Changelog, ReleaseChecklist: Fix typos. 
Refs: #4442
 2018-07-11 00:26:23 +02:00
Leonardo Alt
207d5859d1 Refactoring Declaration -> VariableDeclaration (more precise) 2018-06-12 10:58:50 +02:00
Leonardo Alt
48652c88af Review comments 2018-06-12 10:58:50 +02:00
Leonardo Alt
678a769cd7 Refactoring how storage and local variables are managed. 2018-06-12 10:58:50 +02:00
Leonardo Alt
0b6eea0c55 Bool variables should not allow arithmetic comparison 2018-05-16 18:32:47 +02:00
Leonardo Alt
4117e859eb [SMTChecker] Declaring all state vars before any function is visited 2018-05-15 14:28:08 +02:00
Leonardo Alt
2dbb35d4a8 [SMTChecker] Support to integer and Bool storage vars 2018-05-15 14:22:50 +02:00
chriseth
8debded743
Revert "BREAKING: Bool variables should not allow arithmetic comparison" 2018-05-02 15:56:59 +02:00
chriseth
42289b642f
Merge pull request #4003 from ethereum/bool_vars_comparison 
BREAKING: Bool variables should not allow arithmetic comparison
 2018-05-02 15:56:06 +02:00
Alexander Arlt
f94b793472 Add virtual destructors on base classes. 2018-05-02 13:29:16 +02:00
Leonardo Alt
ab251c7e7d Bool variables should not allow arithmetic comparison 2018-04-27 11:35:58 +02:00
Leonardo Alt
ba3d16fc58 [SMTChecker] Remove 'information is erase' message for if-else 2018-04-19 09:28:44 +02:00
Leonardo Alt
78ba34608f [SMTChecker] Using solUnimplementedAssert instead of solAssert when applicable 2018-04-18 13:17:59 +02:00
Leonardo Alt
ae3350ae03 [SMTChecker] Integration with CVC4 2018-04-17 12:26:58 +01:00
Leonardo Alt
8d087d1889 [SMTChecker] Removing usage of UFs to access SSA indices 2018-04-05 12:48:58 +02:00
Leonardo Alt
9b64dc501d [SMTChecker_Bool] Fix PR review comments: method renaming and solAssert 2018-03-12 20:16:47 +01:00
Leonardo Alt
c2d26eb6a2 [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests. 2018-03-12 20:16:47 +01:00
Leonardo Alt
6a940f0a99 [SMTChecker] Support to Bool variables 2018-03-12 20:16:47 +01:00
Leonardo Alt
5d74b862a3 This z3 option is necessary for good solving performance 2018-03-04 14:42:36 +01:00
Leonardo Alt
8b1b4b78c0 Fix PR comments 2018-02-28 18:31:11 +01:00
Leonardo Alt
cff0836c03 Fix PR comments 2018-02-28 18:05:20 +01:00
Leonardo Alt
21c6b80fc9 Supported types listed in SSAVariable 2018-02-28 18:05:20 +01:00
Leonardo Alt
3b2851ee41 Integer min and max values placed under SymbolicIntVar instead of SMTChecker 2018-02-28 18:05:20 +01:00
Leonardo Alt
f41591b3dd [SMTChecker] A little refactoring on SSA vars 2018-02-28 18:05:20 +01:00
Leonardo Alt
d0abc5359b [SMTChecker] Variables are merged after branches (ite variables) 2018-01-04 18:20:12 +01:00
Leonardo Alt
b588134840 [SMTChecker] Fix typo in the code (satisifable->satisfiable) 2017-12-18 17:31:27 +01:00
Leonardo Alt
a1e296e392 [SMTChecker] Helper functions to add an expression to the solver conjoined with or implied by the current path conditions 2017-12-13 17:59:36 +01:00
Leonardo Alt
2af4d7c7dd [SMTChecker] Keep track of current path conditions 2017-12-13 17:39:10 +01:00
chriseth
a256983320 Fix expression creation problems. 2017-11-30 01:20:21 +01:00
chriseth
d160ec8595 Fix signed division. 2017-11-30 01:20:21 +01:00
chriseth
19e067465a Unary operators and division. 2017-11-30 01:20:21 +01:00
chriseth
0e2a9658d2 Explain IntIntFun and merge assertion. 2017-11-23 19:02:47 +01:00
chriseth
762d591a47 Introduce sorts for smt expressions. 2017-11-22 15:20:26 +01:00
chriseth
8538a25f8d Fix problem with non-value-typed variables. 2017-11-22 02:35:34 +00:00
chriseth
19d5c42429 For loop. 2017-11-22 02:35:34 +00:00
chriseth
95a65dc04c Fix boolean constants. 2017-11-22 02:35:34 +00:00
chriseth
22c689d516 Check for conditions being constant. 2017-11-22 02:35:34 +00:00
chriseth
e5de4a66ed Tests. 2017-11-22 02:35:34 +00:00
chriseth
b37377641d Track usage of variables. 2017-11-22 02:35:34 +00:00
chriseth
f62caf587e Handle branches. 2017-11-22 02:35:34 +00:00
chriseth
7d0e46bf59 Merge pull request #3030 from ethereum/smt-variable-types 
SMT enforce variable types
 2017-10-20 16:55:09 +02:00
Alex Beregszaszi
7a4c165518 Remove unused variable in Z3 2017-10-18 23:18:11 +01:00
chriseth
153ae98878 Catch exception in Z3. 
Note: This exception might not be the result of resource limitation,
it might also hint towards usage error.
 2017-10-17 18:30:10 +01:00
Alex Beregszaszi
a71c6faf0f Remove duplicate >= in Z3 2017-10-17 18:30:07 +01:00
chriseth
1f97c1ea8f Rename variables in SMT checker. 2017-10-17 18:29:53 +01:00
Alex Beregszaszi
18ae0c3d78 SMT enforce variable types 2017-10-05 12:29:20 +01:00
Alex Beregszaszi
10529e994f SMT should not crash on typecast/structs 2017-10-05 11:41:11 +01:00
Alex Beregszaszi
66b188cce9 Merge pull request #3022 from ethereum/assert 
Use solAssert and not assert
 2017-10-04 14:11:43 +01:00
Alex Beregszaszi
a9847c9551 Use solAssert and not assert 2017-10-04 13:05:55 +01:00
chriseth
5ee3ceaef7 Remove leftover couts. 2017-09-29 12:44:39 +02:00
Alex Beregszaszi
1c0c5d923a Mark constructors explicit 2017-09-20 01:23:21 +01:00
chriseth
9e63710b8e Remove parameter names for defaulted functions. 2017-08-31 12:16:41 +02:00
chriseth
cf5e1d6120 Review changes. 2017-08-23 17:37:35 +02:00
chriseth
c93f0434cd Use experimental feature pragma for SMT checker. 2017-08-23 17:37:35 +02:00
chriseth
75f09f2a84 Partial support for if statements. 2017-08-23 17:37:35 +02:00
chriseth
5bfd5d98c1 Format numbers more nicely. 2017-08-23 17:37:35 +02:00
chriseth
1e05ebe50e Refactor Z3 read callback. 2017-08-23 17:37:35 +02:00
chriseth
9ac2ac14c1 Rename read file callback. 2017-08-23 17:37:35 +02:00
chriseth
ab5e3a8f6d Introduce native Z3 support. 2017-08-23 17:37:35 +02:00
chriseth
4cea3d4aa4 Insert abstraction layer. 2017-08-23 17:37:35 +02:00
chriseth
c9cf24458b Prepare build system for Z3. 2017-08-23 17:37:35 +02:00
chriseth
b3f8ed457a Cleanup. 2017-08-23 14:24:30 +02:00
chriseth
39fc798999 Use file to communicate with z3. 2017-08-23 14:24:05 +02:00
chriseth
df848859da Rewrite using SMTLIB2 interface. 2017-08-23 14:24:05 +02:00
chriseth
1ece7bf443 z3 conditions 2017-08-23 14:24:04 +02:00
Alex Beregszaszi
555dc4f46f Remove Why3 generator 2017-06-25 12:26:16 +01:00
Rhett Aultman
89b60ffbd4 Refactor error reporting 
This commit introduces ErrorReporter, a utility class which consolidates
all of the error logging functionality into a common set of functions.
It also replaces all direct interactions with an ErrorList with calls to
an ErrorReporter.

This commit resolves issue #2209
 2017-05-30 07:28:31 -07:00
djudjuu
1d22233a43 refactoring functionCallAnnotation 2017-05-19 15:48:07 +02:00
Alex Beregszaszi
3ae88377d6 Change references to FunctionType::Location 2017-03-16 12:49:52 +00:00
VoR0220
3f9f725737 Fix licensing headers 
Signed-off-by: VoR0220 <rj@erisindustries.com>
 2016-11-23 12:22:33 +01:00
Rhett Aultman
4524ad0870 Add support for do/while loops 
This commit adds support for a standard do <statement> while <expr>;
form of statement.  While loops were already being supported; supporting
a do/while loop mostly involves reusing code from while loops but putting
the conditional checking last.
 2016-11-10 07:07:25 -08:00
Yoichi Hirai
ab1f4632aa Chack for non-version pragmas 2016-10-11 00:07:11 +02:00
Yoichi Hirai
092e5829d8 formal: ignore pragmas during Why3 code generation 
Fixes #1177
 2016-10-11 00:01:29 +02:00
Yoichi Hirai
4337e70cca Prepare for leaky exceptions 
Now toFormalType() reports errors by exceptions, they will be
sometimes leaked to the wider context.  This commits adds a catch.
 2016-09-09 20:15:13 +02:00
Yoichi Hirai
ac7c6ae7d2 toFormalType reports errors by an exception 
This allows error reporting without passing `ASTNode` to `toFormalType()`
 2016-09-09 20:15:08 +02:00
Yoichi Hirai
c861cf579d Translate mapping types into Why3 arrays when keys are integers 
Even when the keys are signed the translation is supposed to work
because Why3 arrays allow negative indices.
 2016-09-09 19:11:15 +02:00
Yoichi Hirai
a98edb22e5 Add Address module in the WhyML prelude 
In the `--formal` output, this commit adds a module called `Address`,
which defines the address type as unsigned integer type bounded at
2^160-1.
 2016-09-07 20:39:23 +02:00
chriseth
ce11580988 Merge pull request #1041 from pirapira/typo_and_whitespace 
Fix a typo and a whitespace inconsistency
 2016-09-07 20:05:30 +02:00
Yoichi Hirai
0a8f0fb051 Append an issue id #1043 to a @todo comment about it 2016-09-07 15:21:02 +02:00
Yoichi Hirai
c9b23d9829 Fix a typo and whitespaces 2016-09-07 14:29:01 +02:00
chriseth
345c0f36fb Fix crash when using json compiler with exponentiation. 2016-08-20 03:45:39 +02:00
chriseth
26e5faa038 Handle external effects. 2016-07-13 11:16:00 +02:00
chriseth
656405240e Simplify interface of RationalNumber. 2016-05-10 19:40:37 +02:00
VoR0220
4b749fc333 changed names for Rational Constants and categories 2016-05-09 11:41:02 -05:00
RJ Catalano
9a075458ad initial work for fixed types...potentially needing a constant literal type for this 
notation

Rational implemented...trying to figure out exponential

fix for token bug, also quick fix for the wei and seconds

fixed problem with var...probably a conversion problem for fixed in size capabilities

adding fixed type tests

Removing bitshift and regrouping fixed type tests together

size capabilities functioning properly for fixed types

got exponents up and working with their inverse, changed a few of the tests....something is working that likely shouldn't be

slight changes to how to flip the rational negative around...still trying to figure it out

tests added

updated tests

odd differences in trying soltest from solc binary, let me know if you can replicate

test not working for odd reason

fixed test problem with fixed literals...still need a way to log this error

broken up the tests, added some, changed some things in types and began compiler work

moar tests and prepping for rebuilding much of the types.cpp file

further fixing

initial work for fixed types...potentially needing a constant literal type for this
 2016-05-09 11:41:02 -05:00
Bob Summerwill
a1ce66b304 Fixed Windows warnings 2016-03-18 01:22:15 -07:00
LianaHus
58e07151e3 - inline and assembly keywords added 
- some style fixes
 2016-03-11 17:49:32 +01:00
chriseth
b47d593252 Do not store elements of a contract by AST node type. 2015-11-26 15:37:55 +01:00
chriseth
e06768e8b5 Fix MSVC errors and warnings. 2015-11-26 14:47:28 +01:00
chriseth
20542d1623 Style. 2015-11-25 14:24:00 +01:00
chriseth
36ba7d11ca Again some why3 fixes with regards to separators in blocks. 2015-11-25 14:24:00 +01:00
chriseth
10fe0a2434 Style. 2015-11-23 16:30:51 +01:00