Integer min and max values placed under SymbolicIntVar instead of SMT…

…Checker
sledrho · Feb 28, 2018 · 3b2851e · 3b2851e
1 parent f41591b
commit 3b2851e
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 19 deletions.
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
@@ -24,6 +24,7 @@
 #endif
 
 #include <libsolidity/formal/SSAVariable.h>
+#include <libsolidity/formal/SymbolicIntVariable.h>
 #include <libsolidity/formal/VariableUsage.h>
 
 #include <libsolidity/interface/ErrorReporter.h>
@@ -244,14 +245,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
 {
 	checkCondition(
-		_value < minValue(_type),
+		_value < SymbolicIntVariable::minValue(_type),
 		_location,
 		"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
 		"value",
 		&_value
 	);
 	checkCondition(
-		_value > maxValue(_type),
+		_value > SymbolicIntVariable::maxValue(_type),
 		_location,
 		"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
 		"value",
@@ -828,15 +829,6 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
 	m_interface->addAssertion(expr(_e) == _value);
 }
 
-smt::Expression SMTChecker::minValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.minValue());
-}
-
-smt::Expression SMTChecker::maxValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.maxValue());
-}
 void SMTChecker::popPathCondition()
 {
 	solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty.");

diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
@@ -140,9 +140,6 @@ class SMTChecker: private ASTConstVisitor
 	/// Resets the variable to an unknown value (in its range).
 	void setUnknownValue(Declaration const& decl);
 
-	static smt::Expression minValue(IntegerType const& _t);
-	static smt::Expression maxValue(IntegerType const& _t);
-
 	/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
 	smt::Expression expr(Expression const& _e);
 	/// Creates the expression (value can be arbitrary)

diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -43,12 +43,12 @@ void SymbolicIntVariable::setUnknownValue(int _seq)
 	m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType));
 }
 
-smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) const
+smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t)
 {
 	return smt::Expression(_t.minValue());
 }
 
-smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) const
+smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t)
 {
 	return smt::Expression(_t.maxValue());
 }
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
@@ -39,12 +39,13 @@ class SymbolicIntVariable : public SymbolicVariable
 	SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default;
 	SymbolicIntVariable& operator=(SymbolicIntVariable&&) = default;
 
+	/// Sets the var to 0.
 	void setZeroValue(int _seq);
+	/// Sets the valid interval for the var.
 	void setUnknownValue(int _seq);
 
-private:
-	smt::Expression minValue(IntegerType const& _t) const;
-	smt::Expression maxValue(IntegerType const& _t) const;
+	static smt::Expression minValue(IntegerType const& _t);
+	static smt::Expression maxValue(IntegerType const& _t);
 };
 
 }