From 4a4620ac955d3c61b4778dfab3a9e05a91e4fc33 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 12 Oct 2018 15:44:46 +0200 Subject: Refactor SSAVariable such that it only uses Type and not Declaration --- libsolidity/formal/SymbolicBoolVariable.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp') diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index 5cf22d7d..5e5aec8f 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -24,12 +24,13 @@ using namespace dev; using namespace dev::solidity; SymbolicBoolVariable::SymbolicBoolVariable( - Declaration const& _decl, + Type const& _type, + string const& _uniqueName, smt::SolverInterface&_interface ): - SymbolicVariable(_decl, _interface) + SymbolicVariable(_type, _uniqueName, _interface) { - solAssert(m_declaration.type()->category() == Type::Category::Bool, ""); + solAssert(_type.category() == Type::Category::Bool, ""); } smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const -- cgit v1.2.3 From ec39fdcb3c6b3d5eb07ea6768fb3926fe54dc47e Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 15 Oct 2018 17:32:17 +0200 Subject: [SMTChecker] Refactoring types --- libsolidity/formal/SymbolicBoolVariable.cpp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp') diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index 5e5aec8f..f65ecd37 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -17,8 +17,6 @@ #include -#include - using namespace std; using namespace dev; using namespace dev::solidity; @@ -38,11 +36,11 @@ smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const return m_interface.newBool(uniqueSymbol(_seq)); } -void SymbolicBoolVariable::setZeroValue(int _seq) +void SymbolicBoolVariable::setZeroValue() { - m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false)); + m_interface.addAssertion(current() == smt::Expression(false)); } -void SymbolicBoolVariable::setUnknownValue(int) +void SymbolicBoolVariable::setUnknownValue() { } -- cgit v1.2.3 From aa23326e06b00ecbaab032d333a15b28f5aa71d7 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 17 Oct 2018 11:32:01 +0200 Subject: Consistent renaming of 'counters' and 'sequence' to 'index' --- libsolidity/formal/SymbolicBoolVariable.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp') diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index f65ecd37..9c41ca9d 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -31,14 +31,14 @@ SymbolicBoolVariable::SymbolicBoolVariable( solAssert(_type.category() == Type::Category::Bool, ""); } -smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const +smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const { - return m_interface.newBool(uniqueSymbol(_seq)); + return m_interface.newBool(uniqueSymbol(_index)); } void SymbolicBoolVariable::setZeroValue() { - m_interface.addAssertion(current() == smt::Expression(false)); + m_interface.addAssertion(currentValue() == smt::Expression(false)); } void SymbolicBoolVariable::setUnknownValue() -- cgit v1.2.3 From b46b827c30584968c6815b456b8c0c775c35ae48 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 18 Oct 2018 15:03:52 +0200 Subject: [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash --- libsolidity/formal/SymbolicBoolVariable.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp') diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index 9c41ca9d..4d753c5c 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -22,13 +22,13 @@ using namespace dev; using namespace dev::solidity; SymbolicBoolVariable::SymbolicBoolVariable( - Type const& _type, + TypePointer _type, string const& _uniqueName, smt::SolverInterface&_interface ): - SymbolicVariable(_type, _uniqueName, _interface) + SymbolicVariable(move(_type), _uniqueName, _interface) { - solAssert(_type.category() == Type::Category::Bool, ""); + solAssert(m_type->category() == Type::Category::Bool, ""); } smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const -- cgit v1.2.3 From d8cbf321dafbe85f6fde07b5dd4ce7a3abffaeb6 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 22 Oct 2018 10:29:03 +0200 Subject: Grouping of symbolic variables in the same file and support to FixedBytes --- libsolidity/formal/SymbolicBoolVariable.cpp | 46 ----------------------------- 1 file changed, 46 deletions(-) delete mode 100644 libsolidity/formal/SymbolicBoolVariable.cpp (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp') diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp deleted file mode 100644 index 4d753c5c..00000000 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ /dev/null @@ -1,46 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see . -*/ - -#include - -using namespace std; -using namespace dev; -using namespace dev::solidity; - -SymbolicBoolVariable::SymbolicBoolVariable( - TypePointer _type, - string const& _uniqueName, - smt::SolverInterface&_interface -): - SymbolicVariable(move(_type), _uniqueName, _interface) -{ - solAssert(m_type->category() == Type::Category::Bool, ""); -} - -smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const -{ - return m_interface.newBool(uniqueSymbol(_index)); -} - -void SymbolicBoolVariable::setZeroValue() -{ - m_interface.addAssertion(currentValue() == smt::Expression(false)); -} - -void SymbolicBoolVariable::setUnknownValue() -{ -} -- cgit v1.2.3