aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/SMTChecker.cpp2
-rw-r--r--libsolidity/formal/SMTChecker.h2
-rw-r--r--libsolidity/formal/SymbolicAddressVariable.cpp40
-rw-r--r--libsolidity/formal/SymbolicAddressVariable.h43
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.cpp46
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.h49
-rw-r--r--libsolidity/formal/SymbolicIntVariable.h49
-rw-r--r--libsolidity/formal/SymbolicTypes.cpp16
-rw-r--r--libsolidity/formal/SymbolicTypes.h3
-rw-r--r--libsolidity/formal/SymbolicVariable.cpp43
-rw-r--r--libsolidity/formal/SymbolicVariables.cpp (renamed from libsolidity/formal/SymbolicIntVariable.cpp)62
-rw-r--r--libsolidity/formal/SymbolicVariables.h (renamed from libsolidity/formal/SymbolicVariable.h)69
12 files changed, 144 insertions, 280 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 631a9eee..51b310ae 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -19,8 +19,6 @@
#include <libsolidity/formal/SMTPortfolio.h>
-#include <libsolidity/formal/SSAVariable.h>
-#include <libsolidity/formal/SymbolicIntVariable.h>
#include <libsolidity/formal/VariableUsage.h>
#include <libsolidity/formal/SymbolicTypes.h>
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 95e01708..376b73fd 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -19,7 +19,7 @@
#include <libsolidity/formal/SolverInterface.h>
-#include <libsolidity/formal/SymbolicVariable.h>
+#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/ast/ASTVisitor.h>
diff --git a/libsolidity/formal/SymbolicAddressVariable.cpp b/libsolidity/formal/SymbolicAddressVariable.cpp
deleted file mode 100644
index 67a18540..00000000
--- a/libsolidity/formal/SymbolicAddressVariable.cpp
+++ /dev/null
@@ -1,40 +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 <http://www.gnu.org/licenses/>.
-*/
-
-#include <libsolidity/formal/SymbolicAddressVariable.h>
-
-#include <libsolidity/formal/SymbolicTypes.h>
-
-using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-
-SymbolicAddressVariable::SymbolicAddressVariable(
- string const& _uniqueName,
- smt::SolverInterface& _interface
-):
- SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface)
-{
-}
-
-void SymbolicAddressVariable::setUnknownValue()
-{
- auto intType = dynamic_cast<IntegerType const*>(m_type.get());
- solAssert(intType, "");
- m_interface.addAssertion(currentValue() >= minValue(*intType));
- m_interface.addAssertion(currentValue() <= maxValue(*intType));
-}
diff --git a/libsolidity/formal/SymbolicAddressVariable.h b/libsolidity/formal/SymbolicAddressVariable.h
deleted file mode 100644
index 3c9c379a..00000000
--- a/libsolidity/formal/SymbolicAddressVariable.h
+++ /dev/null
@@ -1,43 +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 <http://www.gnu.org/licenses/>.
-*/
-
-#pragma once
-
-#include <libsolidity/formal/SymbolicIntVariable.h>
-
-namespace dev
-{
-namespace solidity
-{
-
-/**
- * Specialization of SymbolicVariable for Address
- */
-class SymbolicAddressVariable: public SymbolicIntVariable
-{
-public:
- SymbolicAddressVariable(
- std::string const& _uniqueName,
- smt::SolverInterface& _interface
- );
-
- /// Sets the variable to the full valid value range.
- void setUnknownValue();
-};
-
-}
-}
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 <http://www.gnu.org/licenses/>.
-*/
-
-#include <libsolidity/formal/SymbolicBoolVariable.h>
-
-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()
-{
-}
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
deleted file mode 100644
index 438af2c6..00000000
--- a/libsolidity/formal/SymbolicBoolVariable.h
+++ /dev/null
@@ -1,49 +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 <http://www.gnu.org/licenses/>.
-*/
-
-#pragma once
-
-#include <libsolidity/formal/SymbolicVariable.h>
-
-namespace dev
-{
-namespace solidity
-{
-
-/**
- * Specialization of SymbolicVariable for Bool
- */
-class SymbolicBoolVariable: public SymbolicVariable
-{
-public:
- SymbolicBoolVariable(
- TypePointer _type,
- std::string const& _uniqueName,
- smt::SolverInterface& _interface
- );
-
- /// Sets the var to false.
- void setZeroValue();
- /// Does nothing since the SMT solver already knows the valid values for Bool.
- void setUnknownValue();
-
-protected:
- smt::Expression valueAtIndex(int _index) const;
-};
-
-}
-}
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
deleted file mode 100644
index a9e51b1b..00000000
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ /dev/null
@@ -1,49 +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 <http://www.gnu.org/licenses/>.
-*/
-
-#pragma once
-
-#include <libsolidity/formal/SymbolicVariable.h>
-
-namespace dev
-{
-namespace solidity
-{
-
-/**
- * Specialization of SymbolicVariable for Integers
- */
-class SymbolicIntVariable: public SymbolicVariable
-{
-public:
- SymbolicIntVariable(
- TypePointer _type,
- std::string const& _uniqueName,
- smt::SolverInterface& _interface
- );
-
- /// Sets the var to 0.
- void setZeroValue();
- /// Sets the variable to the full valid value range.
- virtual void setUnknownValue();
-
-protected:
- smt::Expression valueAtIndex(int _index) const;
-};
-
-}
-}
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 7e5db7bd..3eb1c1ce 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -17,10 +17,6 @@
#include <libsolidity/formal/SymbolicTypes.h>
-#include <libsolidity/formal/SymbolicBoolVariable.h>
-#include <libsolidity/formal/SymbolicIntVariable.h>
-#include <libsolidity/formal/SymbolicAddressVariable.h>
-
#include <libsolidity/ast/Types.h>
#include <memory>
@@ -55,6 +51,12 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
else if (isInteger(_type.category()))
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
+ else if (isFixedBytes(_type.category()))
+ {
+ auto fixedBytesType = dynamic_cast<FixedBytesType const*>(type.get());
+ solAssert(fixedBytesType, "");
+ var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver);
+ }
else if (isAddress(_type.category()))
var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver);
else if (isRational(_type.category()))
@@ -86,6 +88,11 @@ bool dev::solidity::isRational(Type::Category _category)
return _category == Type::Category::RationalNumber;
}
+bool dev::solidity::isFixedBytes(Type::Category _category)
+{
+ return _category == Type::Category::FixedBytes;
+}
+
bool dev::solidity::isAddress(Type::Category _category)
{
return _category == Type::Category::Address;
@@ -95,6 +102,7 @@ bool dev::solidity::isNumber(Type::Category _category)
{
return isInteger(_category) ||
isRational(_category) ||
+ isFixedBytes(_category) ||
isAddress(_category);
}
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 0887fa41..dcdd9ea4 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -18,7 +18,7 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
-#include <libsolidity/formal/SymbolicVariable.h>
+#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/Types.h>
@@ -35,6 +35,7 @@ bool isSupportedType(Type const& _type);
bool isInteger(Type::Category _category);
bool isRational(Type::Category _category);
+bool isFixedBytes(Type::Category _category);
bool isAddress(Type::Category _category);
bool isNumber(Type::Category _category);
bool isBool(Type::Category _category);
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
deleted file mode 100644
index 530564d2..00000000
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ /dev/null
@@ -1,43 +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 <http://www.gnu.org/licenses/>.
-*/
-
-#include <libsolidity/formal/SymbolicVariable.h>
-
-#include <libsolidity/ast/AST.h>
-
-using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-
-SymbolicVariable::SymbolicVariable(
- TypePointer _type,
- string const& _uniqueName,
- smt::SolverInterface& _interface
-):
- m_type(move(_type)),
- m_uniqueName(_uniqueName),
- m_interface(_interface),
- m_ssa(make_shared<SSAVariable>())
-{
-}
-
-string SymbolicVariable::uniqueSymbol(unsigned _index) const
-{
- return m_uniqueName + "_" + to_string(_index);
-}
-
-
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicVariables.cpp
index a5939842..85818ba0 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -15,14 +15,57 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
-#include <libsolidity/formal/SymbolicIntVariable.h>
+#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/formal/SymbolicTypes.h>
+#include <libsolidity/ast/AST.h>
+
using namespace std;
using namespace dev;
using namespace dev::solidity;
+SymbolicVariable::SymbolicVariable(
+ TypePointer _type,
+ string const& _uniqueName,
+ smt::SolverInterface& _interface
+):
+ m_type(move(_type)),
+ m_uniqueName(_uniqueName),
+ m_interface(_interface),
+ m_ssa(make_shared<SSAVariable>())
+{
+}
+
+string SymbolicVariable::uniqueSymbol(unsigned _index) const
+{
+ return m_uniqueName + "_" + to_string(_index);
+}
+
+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()
+{
+}
+
SymbolicIntVariable::SymbolicIntVariable(
TypePointer _type,
string const& _uniqueName,
@@ -50,3 +93,20 @@ void SymbolicIntVariable::setUnknownValue()
m_interface.addAssertion(currentValue() >= minValue(*intType));
m_interface.addAssertion(currentValue() <= maxValue(*intType));
}
+
+SymbolicAddressVariable::SymbolicAddressVariable(
+ string const& _uniqueName,
+ smt::SolverInterface& _interface
+):
+ SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface)
+{
+}
+
+SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
+ unsigned _numBytes,
+ string const& _uniqueName,
+ smt::SolverInterface& _interface
+):
+ SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface)
+{
+}
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariables.h
index e554139f..4fd9b245 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -33,7 +33,7 @@ namespace solidity
class Type;
/**
- * This class represents the symbolic version of a program variable.
+ * This abstract class represents the symbolic version of a program variable.
*/
class SymbolicVariable
{
@@ -78,5 +78,72 @@ protected:
std::shared_ptr<SSAVariable> m_ssa = nullptr;
};
+/**
+ * Specialization of SymbolicVariable for Bool
+ */
+class SymbolicBoolVariable: public SymbolicVariable
+{
+public:
+ SymbolicBoolVariable(
+ TypePointer _type,
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+
+ /// Sets the var to false.
+ void setZeroValue();
+ /// Does nothing since the SMT solver already knows the valid values for Bool.
+ void setUnknownValue();
+
+protected:
+ smt::Expression valueAtIndex(int _index) const;
+};
+
+/**
+ * Specialization of SymbolicVariable for Integers
+ */
+class SymbolicIntVariable: public SymbolicVariable
+{
+public:
+ SymbolicIntVariable(
+ TypePointer _type,
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+
+ /// Sets the var to 0.
+ void setZeroValue();
+ /// Sets the variable to the full valid value range.
+ void setUnknownValue();
+
+protected:
+ smt::Expression valueAtIndex(int _index) const;
+};
+
+/**
+ * Specialization of SymbolicVariable for Address
+ */
+class SymbolicAddressVariable: public SymbolicIntVariable
+{
+public:
+ SymbolicAddressVariable(
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+};
+
+/**
+ * Specialization of SymbolicVariable for FixedBytes
+ */
+class SymbolicFixedBytesVariable: public SymbolicIntVariable
+{
+public:
+ SymbolicFixedBytesVariable(
+ unsigned _numBytes,
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+};
+
}
}
generated by cgit (git 2.34.1) at 2024-11-17 17:25:59 +0800