Merge pull request #5283 from ethereum/smt_fixed_bytes

[SMTChecker] Support FixedBytes

15 files changed, 160 insertions, 288 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
+	);
+};
+
 }
 }
diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol
index d0f263eb..1c693914 100644
--- a/test/libsolidity/smtCheckerTests/special/blockhash.sol
+++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol
@@ -7,8 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning: (86-98): Assertion checker does not yet support this special variable.
-// Warning: (86-98): Assertion checker does not yet implement this type.
-// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons
-// Warning: (86-102): Internal error: Expression undefined for SMT solver.
 // Warning: (79-103): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol
index 6f832179..109470a8 100644
--- a/test/libsolidity/smtCheckerTests/special/msg_sig.sol
+++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol
@@ -7,8 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning: (86-93): Assertion checker does not yet support this special variable.
-// Warning: (86-93): Assertion checker does not yet implement this type.
-// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons
-// Warning: (86-107): Internal error: Expression undefined for SMT solver.
 // Warning: (79-108): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol
new file mode 100644
index 00000000..541fff54
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	bytes32 x;
+	function f(bytes8 y) public view {
+		assert(x != y);
+		assert(x != g());
+	}
+	function g() public view returns (bytes32) {
+		return x;
+	}
+}
+// ----
+// Warning: (96-110): Assertion violation happens here
+// Warning: (114-130): Assertion violation happens here