111 Commits

Author	SHA1	Message	Date
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 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
Alex Beregszaszi	f024efb7ab	SMT: do not crash on referencing MagicVariableDeclaration	2018-08-07 20:43:20 +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	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
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
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	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	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	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	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	1f97c1ea8f	Rename variables in SMT checker.	2017-10-17 18:29:53 +01:00
Alex Beregszaszi	10529e994f	SMT should not crash on typecast/structs	2017-10-05 11:41:11 +01: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	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	1ece7bf443	z3 conditions	2017-08-23 14:24:04 +02:00