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