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
19,111 Commits 348 Branches 121 Tags 100 MiB
e299d8ba64
Commit Graph

560 Commits

Author SHA1 Message Date
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
chriseth
806507d5c0 addmod and mulmod for why3. 2015-11-23 00:58:17 +01:00
chriseth
82a6ab486d Why3: Direct references to variables using #. 2015-11-23 00:58:17 +01:00
chriseth
12f19fa46b Formal Verification: State variables. 2015-11-19 02:04:33 +01:00
chriseth
34829ae764 Fix problems with statement blocks. 2015-11-11 15:21:01 +01:00
chriseth
56f5d58850 Rename error type. 2015-10-27 17:45:58 +01:00
chriseth
a957322fd7 Preliminary why3 code output. 2015-10-27 00:49:27 +01:00