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
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
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
