aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--libsolidity/formal/SMTChecker.cpp65
-rw-r--r--libsolidity/formal/SMTChecker.h13
-rw-r--r--libsolidity/formal/SSAVariable.cpp56
-rw-r--r--libsolidity/formal/SSAVariable.h42
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.cpp8
-rw-r--r--libsolidity/formal/SymbolicBoolVariable.h6
-rw-r--r--libsolidity/formal/SymbolicIntVariable.cpp14
-rw-r--r--libsolidity/formal/SymbolicIntVariable.h4
-rw-r--r--libsolidity/formal/SymbolicTypes.cpp72
-rw-r--r--libsolidity/formal/SymbolicTypes.h45
-rw-r--r--libsolidity/formal/SymbolicVariable.cpp3
-rw-r--r--libsolidity/formal/SymbolicVariable.h24
12 files changed, 202 insertions, 150 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 0cb75530..d84d6794 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -22,6 +22,7 @@
#include <libsolidity/formal/SSAVariable.h>
#include <libsolidity/formal/SymbolicIntVariable.h>
#include <libsolidity/formal/VariableUsage.h>
+#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/interface/ErrorReporter.h>
@@ -116,9 +117,7 @@ bool SMTChecker::visit(IfStatement const& _node)
touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
}
else
- {
- countersEndFalse = m_variables;
- }
+ countersEndFalse = copyVariableSequenceCounters();
mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
@@ -176,7 +175,6 @@ bool SMTChecker::visit(ForStatement const& _node)
checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
}
- VariableSequenceCounters sequenceCountersStart = m_variables;
m_interface->push();
if (_node.condition())
m_interface->addAssertion(expr(*_node.condition()));
@@ -187,7 +185,6 @@ bool SMTChecker::visit(ForStatement const& _node)
m_interface->pop();
m_loopExecutionHappened = true;
- std::swap(sequenceCountersStart, m_variables);
resetVariables(touchedVariables);
@@ -220,7 +217,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
_assignment.location(),
"Assertion checker does not yet implement compound assignment."
);
- else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category()))
+ else if (!isSupportedType(_assignment.annotation().type->category()))
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
@@ -281,7 +278,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
{
case Token::Not: // !
{
- solAssert(SSAVariable::isBool(_op.annotation().type->category()), "");
+ solAssert(isBool(_op.annotation().type->category()), "");
defineExpr(_op, !expr(_op.subExpression()));
break;
}
@@ -289,7 +286,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
case Token::Dec: // -- (pre- or postfix)
{
- solAssert(SSAVariable::isInteger(_op.annotation().type->category()), "");
+ solAssert(isInteger(_op.annotation().type->category()), "");
solAssert(_op.subExpression().annotation().lValueRequested, "");
if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
{
@@ -461,7 +458,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
// Will be translated as part of the node that requested the lvalue.
}
- else if (SSAVariable::isSupportedType(_identifier.annotation().type->category()))
+ else if (isSupportedType(_identifier.annotation().type->category()))
{
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
defineExpr(_identifier, currentValue(*decl));
@@ -567,13 +564,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
void SMTChecker::compareOperation(BinaryOperation const& _op)
{
solAssert(_op.annotation().commonType, "");
- if (SSAVariable::isSupportedType(_op.annotation().commonType->category()))
+ if (isSupportedType(_op.annotation().commonType->category()))
{
smt::Expression left(expr(_op.leftExpression()));
smt::Expression right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator();
shared_ptr<smt::Expression> value;
- if (SSAVariable::isInteger(_op.annotation().commonType->category()))
+ if (isInteger(_op.annotation().commonType->category()))
{
value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) :
@@ -586,7 +583,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
}
else // Bool
{
- solUnimplementedAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "Operation not yet supported");
+ solUnimplementedAssert(isBool(_op.annotation().commonType->category()), "Operation not yet supported");
value = make_shared<smt::Expression>(
op == Token::Equal ? (left == right) :
/*op == Token::NotEqual*/ (left != right)
@@ -656,17 +653,15 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s
SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
{
- VariableSequenceCounters beforeVars = m_variables;
-
+ auto countersBeforeBranch = copyVariableSequenceCounters();
if (_condition)
pushPathCondition(*_condition);
_statement.accept(*this);
if (_condition)
popPathCondition();
-
- std::swap(m_variables, beforeVars);
-
- return beforeVars;
+ auto countersAfterBranch = copyVariableSequenceCounters();
+ resetVariableCounters(countersBeforeBranch);
+ return countersAfterBranch;
}
void SMTChecker::checkCondition(
@@ -905,8 +900,8 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia
for (auto const* decl: uniqueVars)
{
solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), "");
- int trueCounter = _countersEndTrue.at(decl).index();
- int falseCounter = _countersEndFalse.at(decl).index();
+ int trueCounter = _countersEndTrue.at(decl);
+ int falseCounter = _countersEndFalse.at(decl);
solAssert(trueCounter != falseCounter, "");
m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
_condition,
@@ -921,10 +916,11 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
// This might be the case for multiple calls to the same function.
if (hasVariable(_varDecl))
return true;
- else if (SSAVariable::isSupportedType(_varDecl.type()->category()))
+ auto const& type = _varDecl.type();
+ if (isSupportedType(type->category()))
{
solAssert(m_variables.count(&_varDecl) == 0, "");
- m_variables.emplace(&_varDecl, SSAVariable(*_varDecl.type(), _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
+ m_variables.emplace(&_varDecl, newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
return true;
}
else
@@ -950,32 +946,31 @@ bool SMTChecker::knownVariable(VariableDeclaration const& _decl)
smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl)
{
solAssert(knownVariable(_decl), "");
- return m_variables.at(&_decl)();
+ return m_variables.at(&_decl)->current();
}
smt::Expression SMTChecker::valueAtSequence(VariableDeclaration const& _decl, int _sequence)
{
solAssert(knownVariable(_decl), "");
- return m_variables.at(&_decl)(_sequence);
+ return m_variables.at(&_decl)->valueAtSequence(_sequence);
}
smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
{
solAssert(knownVariable(_decl), "");
- ++m_variables.at(&_decl);
- return m_variables.at(&_decl)();
+ return m_variables.at(&_decl)->increase();
}
void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
{
solAssert(knownVariable(_decl), "");
- m_variables.at(&_decl).setZeroValue();
+ m_variables.at(&_decl)->setZeroValue();
}
void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
{
solAssert(knownVariable(_decl), "");
- m_variables.at(&_decl).setUnknownValue();
+ m_variables.at(&_decl)->setUnknownValue();
}
smt::Expression SMTChecker::expr(Expression const& _e)
@@ -1074,3 +1069,17 @@ bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef)
{
return contains(m_functionPath, _funDef);
}
+
+SMTChecker::VariableSequenceCounters SMTChecker::copyVariableSequenceCounters()
+{
+ VariableSequenceCounters counters;
+ for (auto var: m_variables)
+ counters.emplace(var.first, var.second->index());
+ return counters;
+}
+
+void SMTChecker::resetVariableCounters(VariableSequenceCounters const& _counters)
+{
+ for (auto var: _counters)
+ m_variables.at(var.first)->index() = var.second;
+}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index bef6ea0c..ae697204 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -19,14 +19,14 @@
#include <libsolidity/formal/SolverInterface.h>
-
-#include <libsolidity/formal/SSAVariable.h>
+#include <libsolidity/formal/SymbolicVariable.h>
#include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/interface/ReadFile.h>
#include <map>
+#include <unordered_map>
#include <string>
#include <vector>
@@ -86,7 +86,7 @@ private:
void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
/// Maps a variable to an SSA index.
- using VariableSequenceCounters = std::map<VariableDeclaration const*, SSAVariable>;
+ using VariableSequenceCounters = std::unordered_map<VariableDeclaration const*, int>;
/// Visits the branch given by the statement, pushes and pops the current path conditions.
/// @param _condition if present, asserts that this condition is true within the branch.
@@ -176,13 +176,18 @@ private:
/// Checks if VariableDeclaration was seen.
bool hasVariable(VariableDeclaration const& _e) const;
+ /// Copy the SSA indices of m_variables.
+ VariableSequenceCounters copyVariableSequenceCounters();
+ /// Resets the variable counters.
+ void resetVariableCounters(VariableSequenceCounters const& _counters);
+
std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage;
bool m_loopExecutionHappened = false;
/// An Expression may have multiple smt::Expression due to
/// repeated calls to the same function.
std::multimap<Expression const*, smt::Expression> m_expressions;
- std::map<VariableDeclaration const*, SSAVariable> m_variables;
+ std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter;
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index ceeea49a..aeb12c9f 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/libsolidity/formal/SSAVariable.cpp
@@ -17,46 +17,12 @@
#include <libsolidity/formal/SSAVariable.h>
-#include <libsolidity/formal/SymbolicBoolVariable.h>
-#include <libsolidity/formal/SymbolicIntVariable.h>
-
-#include <libsolidity/ast/AST.h>
-
using namespace std;
-using namespace dev;
using namespace dev::solidity;
-SSAVariable::SSAVariable(
- Type const& _type,
- string const& _uniqueName,
- smt::SolverInterface& _interface
-)
+SSAVariable::SSAVariable()
{
resetIndex();
-
- if (isInteger(_type.category()))
- m_symbolicVar = make_shared<SymbolicIntVariable>(_type, _uniqueName, _interface);
- else if (isBool(_type.category()))
- m_symbolicVar = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _interface);
- else
- {
- solAssert(false, "");
- }
-}
-
-bool SSAVariable::isSupportedType(Type::Category _category)
-{
- return isInteger(_category) || isBool(_category);
-}
-
-bool SSAVariable::isInteger(Type::Category _category)
-{
- return _category == Type::Category::Integer || _category == Type::Category::Address;
-}
-
-bool SSAVariable::isBool(Type::Category _category)
-{
- return _category == Type::Category::Bool;
}
void SSAVariable::resetIndex()
@@ -65,23 +31,3 @@ void SSAVariable::resetIndex()
m_nextFreeSequenceCounter.reset (new int);
*m_nextFreeSequenceCounter = 1;
}
-
-int SSAVariable::index() const
-{
- return m_currentSequenceCounter;
-}
-
-int SSAVariable::next() const
-{
- return *m_nextFreeSequenceCounter;
-}
-
-void SSAVariable::setZeroValue()
-{
- m_symbolicVar->setZeroValue(index());
-}
-
-void SSAVariable::setUnknownValue()
-{
- m_symbolicVar->setUnknownValue(index());
-}
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index f4a4e93e..f8317b79 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/libsolidity/formal/SSAVariable.h
@@ -17,8 +17,6 @@
#pragma once
-#include <libsolidity/formal/SymbolicVariable.h>
-
#include <memory>
namespace dev
@@ -32,53 +30,19 @@ namespace solidity
class SSAVariable
{
public:
- /// @param _type Forwarded to the symbolic var.
- /// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
- SSAVariable(
- Type const& _type,
- std::string const& _uniqueName,
- smt::SolverInterface& _interface
- );
-
+ SSAVariable();
void resetIndex();
/// This function returns the current index of this SSA variable.
- int index() const;
- /// This function returns the next free index of this SSA variable.
- int next() const;
+ int index() const { return m_currentSequenceCounter; }
+ int& index() { return m_currentSequenceCounter; }
int operator++()
{
return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++;
}
- smt::Expression operator()() const
- {
- return valueAtSequence(index());
- }
-
- smt::Expression operator()(int _seq) const
- {
- return valueAtSequence(_seq);
- }
-
- /// These two functions forward the call to the symbolic var
- /// which generates the constraints according to the type.
- void setZeroValue();
- void setUnknownValue();
-
- /// So far Int and Bool are supported.
- static bool isSupportedType(Type::Category _category);
- static bool isInteger(Type::Category _category);
- static bool isBool(Type::Category _category);
-
private:
- smt::Expression valueAtSequence(int _seq) const
- {
- return (*m_symbolicVar)(_seq);
- }
-
- std::shared_ptr<SymbolicVariable> m_symbolicVar = nullptr;
int m_currentSequenceCounter;
/// The next free sequence counter is a shared pointer because we want
/// the copy and the copied to share it.
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 <libsolidity/formal/SymbolicBoolVariable.h>
-#include <libsolidity/ast/AST.h>
-
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()
{
}
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
index 33ac9061..3d735889 100644
--- a/libsolidity/formal/SymbolicBoolVariable.h
+++ b/libsolidity/formal/SymbolicBoolVariable.h
@@ -37,9 +37,9 @@ public:
);
/// Sets the var to false.
- void setZeroValue(int _seq);
- /// Does nothing since the SMT solver already knows the valid values.
- void setUnknownValue(int _seq);
+ void setZeroValue();
+ /// Does nothing since the SMT solver already knows the valid values for Bool.
+ void setUnknownValue();
protected:
smt::Expression valueAtSequence(int _seq) const;
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index 0adb9d09..877495bd 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -40,26 +40,26 @@ smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const
return m_interface.newInteger(uniqueSymbol(_seq));
}
-void SymbolicIntVariable::setZeroValue(int _seq)
+void SymbolicIntVariable::setZeroValue()
{
- m_interface.addAssertion(valueAtSequence(_seq) == 0);
+ m_interface.addAssertion(current() == 0);
}
-void SymbolicIntVariable::setUnknownValue(int _seq)
+void SymbolicIntVariable::setUnknownValue()
{
if (m_type.category() == Type::Category::Integer)
{
auto intType = dynamic_cast<IntegerType const*>(&m_type);
solAssert(intType, "");
- m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType));
- m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType));
+ m_interface.addAssertion(current() >= minValue(*intType));
+ m_interface.addAssertion(current() <= maxValue(*intType));
}
else
{
solAssert(m_type.category() == Type::Category::Address, "");
IntegerType addrType{160};
- m_interface.addAssertion(valueAtSequence(_seq) >= minValue(addrType));
- m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(addrType));
+ m_interface.addAssertion(current() >= minValue(addrType));
+ m_interface.addAssertion(current() <= maxValue(addrType));
}
}
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
index 92eeb13d..3b0c0311 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -37,9 +37,9 @@ public:
);
/// Sets the var to 0.
- void setZeroValue(int _seq);
+ void setZeroValue();
/// Sets the variable to the full valid value range.
- void setUnknownValue(int _seq);
+ void setUnknownValue();
static smt::Expression minValue(IntegerType const& _t);
static smt::Expression maxValue(IntegerType const& _t);
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
new file mode 100644
index 00000000..deb52ac1
--- /dev/null
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -0,0 +1,72 @@
+/*
+ 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/SymbolicTypes.h>
+
+#include <libsolidity/formal/SymbolicBoolVariable.h>
+#include <libsolidity/formal/SymbolicIntVariable.h>
+
+#include <libsolidity/ast/Types.h>
+
+#include <memory>
+
+using namespace std;
+using namespace dev::solidity;
+
+bool dev::solidity::isSupportedType(Type::Category _category)
+{
+ return isInteger(_category) || isBool(_category);
+}
+
+bool dev::solidity::isSupportedType(Type const& _type)
+{
+ return isSupportedType(_type.category());
+}
+
+bool dev::solidity::isInteger(Type::Category _category)
+{
+ return _category == Type::Category::Integer || _category == Type::Category::Address;
+}
+
+bool dev::solidity::isInteger(Type const& _type)
+{
+ return isInteger(_type.category());
+}
+
+bool dev::solidity::isBool(Type::Category _category)
+{
+ return _category == Type::Category::Bool;
+}
+
+bool dev::solidity::isBool(Type const& _type)
+{
+ return isBool(_type.category());
+}
+
+shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver)
+{
+ if (!isSupportedType(_type))
+ return nullptr;
+ if (isBool(_type.category()))
+ return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
+ else if (isInteger(_type.category()))
+ return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
+ else
+ solAssert(false, "");
+}
+
+
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
new file mode 100644
index 00000000..f9df6853
--- /dev/null
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -0,0 +1,45 @@
+/*
+ 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/SolverInterface.h>
+#include <libsolidity/formal/SymbolicVariable.h>
+
+#include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/Types.h>
+
+namespace dev
+{
+namespace solidity
+{
+
+/// So far int, bool and address are supported.
+/// Returns true if type is supported.
+bool isSupportedType(Type::Category _category);
+bool isSupportedType(Type const& _type);
+
+bool isInteger(Type::Category _category);
+bool isInteger(Type const& _type);
+
+bool isBool(Type::Category _category);
+bool isBool(Type const& _type);
+
+std::shared_ptr<SymbolicVariable> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
+
+}
+}
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
index afbc01ba..18cf00dc 100644
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ b/libsolidity/formal/SymbolicVariable.cpp
@@ -30,7 +30,8 @@ SymbolicVariable::SymbolicVariable(
):
m_type(_type),
m_uniqueName(_uniqueName),
- m_interface(_interface)
+ m_interface(_interface),
+ m_ssa(make_shared<SSAVariable>())
{
}
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index 977515f8..9ed5ce01 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -17,6 +17,8 @@
#pragma once
+#include <libsolidity/formal/SSAVariable.h>
+
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/ast/Types.h>
@@ -43,25 +45,35 @@ public:
);
virtual ~SymbolicVariable() = default;
- smt::Expression operator()(int _seq) const
+ smt::Expression current() const
{
- return valueAtSequence(_seq);
+ return valueAtSequence(m_ssa->index());
}
- std::string uniqueSymbol(int _seq) const;
+ virtual smt::Expression valueAtSequence(int _seq) const = 0;
+
+ smt::Expression increase()
+ {
+ ++(*m_ssa);
+ return current();
+ }
+
+ int index() const { return m_ssa->index(); }
+ int& index() { return m_ssa->index(); }
/// Sets the var to the default value of its type.
- virtual void setZeroValue(int _seq) = 0;
+ virtual void setZeroValue() = 0;
/// The unknown value is the full range of valid values,
/// and that's sub-type dependent.
- virtual void setUnknownValue(int _seq) = 0;
+ virtual void setUnknownValue() = 0;
protected:
- virtual smt::Expression valueAtSequence(int _seq) const = 0;
+ std::string uniqueSymbol(int _seq) const;
Type const& m_type;
std::string m_uniqueName;
smt::SolverInterface& m_interface;
+ std::shared_ptr<SSAVariable> m_ssa = nullptr;
};
}
generated by cgit (git 2.34.1) at 2024-11-17 14:16:08 +0800