From 3b2851ee4163bcfbca9e4e23650dfeee1a06653a Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leonardoaltt@gmail.com>
Date: Sat, 17 Feb 2018 09:34:38 +0100
Subject: Integer min and max values placed under SymbolicIntVar instead of
SMTChecker
---
libsolidity/formal/SMTChecker.cpp | 14 +++-----------
libsolidity/formal/SMTChecker.h | 3 ---
libsolidity/formal/SymbolicIntVariable.cpp | 4 ++--
libsolidity/formal/SymbolicIntVariable.h | 7 ++++---
4 files changed, 9 insertions(+), 19 deletions(-)
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 37dce96c..ad42c105 100644
--- 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
index 7481e1c8..7e7996cf 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -140,9 +140,6 @@ private:
/// 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
index 6ed7037f..c206f1cd 100644
--- 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
index efe05af8..0066bb75 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -39,12 +39,13 @@ public:
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);
};
}
--
cgit v1.2.3