From ebbe03cad6a01f8457b7c788319afc4e63eef733 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 10 May 2019 16:28:29 +0200 Subject: [PATCH] [SMTChecker] Move variable handling to EncodingContext --- libsolidity/formal/EncodingContext.cpp | 100 ++++++++++++-- libsolidity/formal/EncodingContext.h | 53 +++++++- libsolidity/formal/SMTChecker.cpp | 177 ++++++++----------------- libsolidity/formal/SMTChecker.h | 22 --- 4 files changed, 189 insertions(+), 163 deletions(-) diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 176cc3d12..5a605f484 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -21,42 +21,118 @@ using namespace std; using namespace dev; -using namespace dev::solidity; using namespace dev::solidity::smt; EncodingContext::EncodingContext(SolverInterface& _solver): m_solver(_solver), m_thisAddress(make_unique("this", m_solver)) { - auto sort = make_shared( - make_shared(smt::Kind::Int), - make_shared(smt::Kind::Int) + auto sort = make_shared( + make_shared(Kind::Int), + make_shared(Kind::Int) ); m_balances = make_unique(sort, "balances", m_solver); } void EncodingContext::reset() { + resetAllVariables(); m_thisAddress->increaseIndex(); m_balances->increaseIndex(); } -smt::Expression EncodingContext::thisAddress() +/// Variables. + +shared_ptr EncodingContext::variable(solidity::VariableDeclaration const& _varDecl) +{ + solAssert(knownVariable(_varDecl), ""); + return m_variables[&_varDecl]; +} + +bool EncodingContext::createVariable(solidity::VariableDeclaration const& _varDecl) +{ + solAssert(!knownVariable(_varDecl), ""); + auto const& type = _varDecl.type(); + auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), m_solver); + m_variables.emplace(&_varDecl, result.second); + return result.first; +} + +bool EncodingContext::knownVariable(solidity::VariableDeclaration const& _varDecl) +{ + return m_variables.count(&_varDecl); +} + +void EncodingContext::resetVariable(solidity::VariableDeclaration const& _variable) +{ + newValue(_variable); + setUnknownValue(_variable); +} + +void EncodingContext::resetVariables(set const& _variables) +{ + for (auto const* decl: _variables) + resetVariable(*decl); +} + +void EncodingContext::resetVariables(function const& _filter) +{ + for_each(begin(m_variables), end(m_variables), [&](auto _variable) + { + if (_filter(*_variable.first)) + this->resetVariable(*_variable.first); + }); +} + +void EncodingContext::resetAllVariables() +{ + resetVariables([&](solidity::VariableDeclaration const&) { return true; }); +} + +Expression EncodingContext::newValue(solidity::VariableDeclaration const& _decl) +{ + solAssert(knownVariable(_decl), ""); + return m_variables.at(&_decl)->increaseIndex(); +} + +void EncodingContext::setZeroValue(solidity::VariableDeclaration const& _decl) +{ + solAssert(knownVariable(_decl), ""); + setZeroValue(*m_variables.at(&_decl)); +} + +void EncodingContext::setZeroValue(SymbolicVariable& _variable) +{ + setSymbolicZeroValue(_variable, m_solver); +} + +void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl) +{ + solAssert(knownVariable(_decl), ""); + setUnknownValue(*m_variables.at(&_decl)); +} + +void EncodingContext::setUnknownValue(SymbolicVariable& _variable) +{ + setSymbolicUnknownValue(_variable, m_solver); +} + +Expression EncodingContext::thisAddress() { return m_thisAddress->currentValue(); } -smt::Expression EncodingContext::balance() +Expression EncodingContext::balance() { return balance(m_thisAddress->currentValue()); } -smt::Expression EncodingContext::balance(smt::Expression _address) +Expression EncodingContext::balance(Expression _address) { - return smt::Expression::select(m_balances->currentValue(), move(_address)); + return Expression::select(m_balances->currentValue(), move(_address)); } -void EncodingContext::transfer(smt::Expression _from, smt::Expression _to, smt::Expression _value) +void EncodingContext::transfer(Expression _from, Expression _to, Expression _value) { unsigned indexBefore = m_balances->index(); addBalance(_from, 0 - _value); @@ -65,7 +141,7 @@ void EncodingContext::transfer(smt::Expression _from, smt::Expression _to, smt:: solAssert(indexAfter > indexBefore, ""); m_balances->increaseIndex(); /// Do not apply the transfer operation if _from == _to. - auto newBalances = smt::Expression::ite( + auto newBalances = Expression::ite( move(_from) == move(_to), m_balances->valueAtIndex(indexBefore), m_balances->valueAtIndex(indexAfter) @@ -73,9 +149,9 @@ void EncodingContext::transfer(smt::Expression _from, smt::Expression _to, smt:: m_solver.addAssertion(m_balances->currentValue() == newBalances); } -void EncodingContext::addBalance(smt::Expression _address, smt::Expression _value) +void EncodingContext::addBalance(Expression _address, Expression _value) { - auto newBalances = smt::Expression::store( + auto newBalances = Expression::store( m_balances->currentValue(), _address, balance(_address) + move(_value) diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index df6e69c07..e27e4a88a 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -20,6 +20,9 @@ #include #include +#include +#include + namespace dev { namespace solidity @@ -38,22 +41,60 @@ public: /// Resets the entire context. void reset(); - /// Value of `this` address. - smt::Expression thisAddress(); + /// Methods related to variables. + //@{ + /// @returns the symbolic representation of a program variable. + std::shared_ptr variable(solidity::VariableDeclaration const& _varDecl); + /// @returns all symbolic variables. + std::unordered_map> const& variables() const { return m_variables; } + /// Creates a symbolic variable and + /// @returns true if a variable's type is not supported and is therefore abstract. + bool createVariable(solidity::VariableDeclaration const& _varDecl); + /// @returns true if variable was created. + bool knownVariable(solidity::VariableDeclaration const& _varDecl); + + /// Resets a specific variable. + void resetVariable(solidity::VariableDeclaration const& _variable); + /// Resets a set of variables. + void resetVariables(std::set const& _variables); + /// Resets variables according to a predicate. + void resetVariables(std::function const& _filter); + ///Resets all variables. + void resetAllVariables(); + + /// Allocates a new index for the declaration, updates the current + /// index to this value and returns the expression. + Expression newValue(solidity::VariableDeclaration const& _decl); + /// Sets the value of the declaration to zero. + void setZeroValue(solidity::VariableDeclaration const& _decl); + void setZeroValue(SymbolicVariable& _variable); + /// Resets the variable to an unknown value (in its range). + void setUnknownValue(solidity::VariableDeclaration const& decl); + void setUnknownValue(SymbolicVariable& _variable); + //@} + + /// Blockchain related methods. + //@{ + /// Value of `this` address. + Expression thisAddress(); /// @returns the symbolic balance of address `this`. - smt::Expression balance(); + Expression balance(); /// @returns the symbolic balance of an address. - smt::Expression balance(smt::Expression _address); + Expression balance(Expression _address); /// Transfer _value from _from to _to. - void transfer(smt::Expression _from, smt::Expression _to, smt::Expression _value); + void transfer(Expression _from, Expression _to, Expression _value); + //@} private: /// Adds _value to _account's balance. - void addBalance(smt::Expression _account, smt::Expression _value); + void addBalance(Expression _account, Expression _value); SolverInterface& m_solver; + /// Symbolic variables. + std::unordered_map> m_variables; + /// Symbolic `this` address. std::unique_ptr m_thisAddress; diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 12d79cc37..bbbe619b4 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -87,7 +87,7 @@ bool SMTChecker::visit(ContractDefinition const& _contract) void SMTChecker::endVisit(ContractDefinition const&) { - m_variables.clear(); + m_context.resetAllVariables(); } void SMTChecker::endVisit(VariableDeclaration const& _varDecl) @@ -247,7 +247,7 @@ bool SMTChecker::visit(WhileStatement const& _node) { auto indicesBeforeLoop = copyVariableIndices(); auto touchedVars = touchedVariables(_node); - resetVariables(touchedVars); + m_context.resetVariables(touchedVars); decltype(indicesBeforeLoop) indicesAfterLoop; if (_node.isDoWhile()) { @@ -295,7 +295,7 @@ bool SMTChecker::visit(ForStatement const& _node) if (_node.loopExpression()) touchedVars += touchedVariables(*_node.loopExpression()); - resetVariables(touchedVars); + m_context.resetVariables(touchedVars); if (_node.condition()) { @@ -341,13 +341,13 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) for (unsigned i = 0; i < declarations.size(); ++i) { solAssert(components.at(i), ""); - if (declarations.at(i) && knownVariable(*declarations.at(i))) + if (declarations.at(i) && m_context.knownVariable(*declarations.at(i))) assignment(*declarations.at(i), components.at(i)->currentValue(), declarations.at(i)->location()); } } } } - else if (knownVariable(*_varDecl.declarations().front())) + else if (m_context.knownVariable(*_varDecl.declarations().front())) { if (_varDecl.initialValue()) assignment(*_varDecl.declarations().front(), *_varDecl.initialValue(), _varDecl.location()); @@ -383,7 +383,7 @@ void SMTChecker::endVisit(Assignment const& _assignment) ); // Give it a new index anyway to keep the SSA scheme sound. if (auto varDecl = identifierToVariable(_assignment.leftHandSide())) - newValue(*varDecl); + m_context.newValue(*varDecl); } else { @@ -431,7 +431,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) if (component) { if (auto varDecl = identifierToVariable(*component)) - components.push_back(m_variables[varDecl]); + components.push_back(m_context.variable(*varDecl)); else { solAssert(knownExpr(*component), ""); @@ -570,15 +570,15 @@ void SMTChecker::endVisit(UnaryOperation const& _op) auto const& subExpr = _op.subExpression(); if (auto decl = identifierToVariable(subExpr)) { - newValue(*decl); - setZeroValue(*decl); + m_context.newValue(*decl); + m_context.setZeroValue(*decl); } else { solAssert(knownExpr(subExpr), ""); auto const& symbVar = m_expressions[&subExpr]; symbVar->increaseIndex(); - setZeroValue(*symbVar); + m_context.setZeroValue(*symbVar); if (dynamic_cast(&_op.subExpression())) arrayIndexAssignment(_op.subExpression(), symbVar->currentValue()); else @@ -735,7 +735,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall) auto const& symbolicVar = m_globalContext.at(gasLeft); unsigned index = symbolicVar->index(); // We set the current value to unknown anyway to add type constraints. - setUnknownValue(*symbolicVar); + m_context.setUnknownValue(*symbolicVar); if (index > 0) m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); } @@ -788,8 +788,8 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) vector> components; for (auto param: returnParams) { - solAssert(m_variables[param.get()], ""); - components.push_back(m_variables[param.get()]); + solAssert(m_context.variable(*param), ""); + components.push_back(m_context.variable(*param)); } auto const& symbTuple = dynamic_pointer_cast(m_expressions[&_funCall]); solAssert(symbTuple, ""); @@ -869,7 +869,7 @@ void SMTChecker::visitTypeConversion(FunctionCall const& _funCall) else { createExpr(_funCall); - setUnknownValue(*m_expressions.at(&_funCall)); + m_context.setUnknownValue(*m_expressions.at(&_funCall)); auto const& funCallCategory = _funCall.annotation().type->category(); // TODO: truncating and bytesX needs a different approach because of right padding. if (funCallCategory == Type::Category::Integer || funCallCategory == Type::Category::Address) @@ -944,10 +944,10 @@ void SMTChecker::endVisit(Return const& _return) solAssert(components.size() == returnParams.size(), ""); for (unsigned i = 0; i < returnParams.size(); ++i) if (components.at(i)) - m_interface->addAssertion(expr(*components.at(i)) == newValue(*returnParams.at(i))); + m_interface->addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i))); } else if (returnParams.size() == 1) - m_interface->addAssertion(expr(*_return.expression()) == newValue(*returnParams.front())); + m_interface->addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front())); } } @@ -1011,7 +1011,7 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess) { auto varDecl = identifierToVariable(*id); solAssert(varDecl, ""); - array = m_variables[varDecl]; + array = m_context.variable(*varDecl); } else if (auto const& innerAccess = dynamic_cast(&_indexAccess.baseExpression())) { @@ -1055,7 +1055,7 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c solAssert(varDecl, ""); if (varDecl->hasReferenceOrMappingType()) - resetVariables([&](VariableDeclaration const& _var) { + m_context.resetVariables([&](VariableDeclaration const& _var) { if (_var == *varDecl) return false; TypePointer prefix = _var.type(); @@ -1084,15 +1084,15 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c }); smt::Expression store = smt::Expression::store( - m_variables[varDecl]->currentValue(), + m_context.variable(*varDecl)->currentValue(), expr(*indexAccess.indexExpression()), _rightHandSide ); - m_interface->addAssertion(newValue(*varDecl) == store); + m_interface->addAssertion(m_context.newValue(*varDecl) == store); // Update the SMT select value after the assignment, // necessary for sound models. defineExpr(indexAccess, smt::Expression::select( - m_variables[varDecl]->currentValue(), + m_context.variable(*varDecl)->currentValue(), expr(*indexAccess.indexExpression()) )); } @@ -1102,7 +1102,7 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c if (identifier) { auto varDecl = identifierToVariable(*identifier); - newValue(*varDecl); + m_context.newValue(*varDecl); } m_errorReporter.warning( @@ -1123,7 +1123,7 @@ void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _ex { auto result = smt::newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); m_globalContext.emplace(_name, result.second); - setUnknownValue(*result.second); + m_context.setUnknownValue(*result.second); if (result.first) m_errorReporter.warning( _expr.location(), @@ -1414,7 +1414,7 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio addOverflowTarget(OverflowTarget::Type::All, TypeProvider::uint(160), _value, _location); else if (type->category() == Type::Category::Mapping) arrayAssignment(); - m_interface->addAssertion(newValue(_variable) == _value); + m_interface->addAssertion(m_context.newValue(_variable) == _value); } SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression _condition) @@ -1456,7 +1456,7 @@ void SMTChecker::checkCondition( expressionsToEvaluate.emplace_back(*_additionalValue); expressionNames.push_back(_additionalValueName); } - for (auto const& var: m_variables) + for (auto const& var: m_context.variables()) { if (var.first->type()->isValueType()) { @@ -1653,7 +1653,7 @@ void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _fu for (unsigned i = 0; i < funParams.size(); ++i) if (createVariable(*funParams[i])) { - m_interface->addAssertion(_callArgs[i] == newValue(*funParams[i])); + m_interface->addAssertion(_callArgs[i] == m_context.newValue(*funParams[i])); if (funParams[i]->annotation().type->category() == Type::Category::Mapping) m_arrayAssignmentHappened = true; } @@ -1661,16 +1661,16 @@ void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _fu for (auto const& variable: _function.localVariables()) if (createVariable(*variable)) { - newValue(*variable); - setZeroValue(*variable); + m_context.newValue(*variable); + m_context.setZeroValue(*variable); } if (_function.returnParameterList()) for (auto const& retParam: _function.returnParameters()) if (createVariable(*retParam)) { - newValue(*retParam); - setZeroValue(*retParam); + m_context.newValue(*retParam); + m_context.setZeroValue(*retParam); } } @@ -1678,58 +1678,26 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) { for (auto const& variable: _function.localVariables()) if (createVariable(*variable)) - setZeroValue(*variable); + m_context.setZeroValue(*variable); for (auto const& param: _function.parameters()) if (createVariable(*param)) - setUnknownValue(*param); + m_context.setUnknownValue(*param); if (_function.returnParameterList()) for (auto const& retParam: _function.returnParameters()) if (createVariable(*retParam)) - setZeroValue(*retParam); -} - -void SMTChecker::removeLocalVariables() -{ - for (auto it = m_variables.begin(); it != m_variables.end(); ) - { - if (it->first->isLocalVariable()) - it = m_variables.erase(it); - else - ++it; - } -} - -void SMTChecker::resetVariable(VariableDeclaration const& _variable) -{ - newValue(_variable); - setUnknownValue(_variable); + m_context.setZeroValue(*retParam); } void SMTChecker::resetStateVariables() { - resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); }); + m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); }); } void SMTChecker::resetStorageReferences() { - resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); }); -} - -void SMTChecker::resetVariables(set const& _variables) -{ - for (auto const* decl: _variables) - resetVariable(*decl); -} - -void SMTChecker::resetVariables(function const& _filter) -{ - for_each(begin(m_variables), end(m_variables), [&](auto _variable) - { - if (_filter(*_variable.first)) - this->resetVariable(*_variable.first); - }); + m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); }); } TypePointer SMTChecker::typeWithoutPointer(TypePointer const& _type) @@ -1751,7 +1719,7 @@ void SMTChecker::mergeVariables(set const& _variable int trueIndex = _indicesEndTrue.at(decl); int falseIndex = _indicesEndFalse.at(decl); solAssert(trueIndex != falseIndex, ""); - m_interface->addAssertion(newValue(*decl) == smt::Expression::ite( + m_interface->addAssertion(m_context.newValue(*decl) == smt::Expression::ite( _condition, valueAtIndex(*decl, trueIndex), valueAtIndex(*decl, falseIndex)) @@ -1759,16 +1727,24 @@ void SMTChecker::mergeVariables(set const& _variable } } +smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl) +{ + solAssert(m_context.knownVariable(_decl), ""); + return m_context.variable(_decl)->currentValue(); +} + +smt::Expression SMTChecker::valueAtIndex(VariableDeclaration const& _decl, int _index) +{ + solAssert(m_context.knownVariable(_decl), ""); + return m_context.variable(_decl)->valueAtIndex(_index); +} + bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { - // This might be the case for multiple calls to the same function. - if (knownVariable(_varDecl)) + if (m_context.knownVariable(_varDecl)) return true; - auto const& type = _varDecl.type(); - solAssert(m_variables.count(&_varDecl) == 0, ""); - auto result = smt::newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface); - m_variables.emplace(&_varDecl, result.second); - if (result.first) + bool abstract = m_context.createVariable(_varDecl); + if (abstract) { m_errorReporter.warning( _varDecl.location(), @@ -1779,51 +1755,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) return true; } -bool SMTChecker::knownVariable(VariableDeclaration const& _decl) -{ - return m_variables.count(&_decl); -} - -smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl) -{ - solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)->currentValue(); -} - -smt::Expression SMTChecker::valueAtIndex(VariableDeclaration const& _decl, int _index) -{ - solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)->valueAtIndex(_index); -} - -smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl) -{ - solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)->increaseIndex(); -} - -void SMTChecker::setZeroValue(VariableDeclaration const& _decl) -{ - solAssert(knownVariable(_decl), ""); - setZeroValue(*m_variables.at(&_decl)); -} - -void SMTChecker::setZeroValue(smt::SymbolicVariable& _variable) -{ - smt::setSymbolicZeroValue(_variable, *m_interface); -} - -void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) -{ - solAssert(knownVariable(_decl), ""); - setUnknownValue(*m_variables.at(&_decl)); -} - -void SMTChecker::setUnknownValue(smt::SymbolicVariable& _variable) -{ - smt::setSymbolicUnknownValue(_variable, *m_interface); -} - smt::Expression SMTChecker::expr(Expression const& _e) { if (!knownExpr(_e)) @@ -1938,7 +1869,7 @@ bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef) SMTChecker::VariableIndices SMTChecker::copyVariableIndices() { VariableIndices indices; - for (auto const& var: m_variables) + for (auto const& var: m_context.variables()) indices.emplace(var.first, var.second->index()); return indices; } @@ -1946,7 +1877,7 @@ SMTChecker::VariableIndices SMTChecker::copyVariableIndices() void SMTChecker::resetVariableIndices(VariableIndices const& _indices) { for (auto const& var: _indices) - m_variables.at(var.first)->index() = var.second; + m_context.variable(*var.first)->index() = var.second; } FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCall const& _funCall) @@ -2015,7 +1946,7 @@ VariableDeclaration const* SMTChecker::identifierToVariable(Expression const& _e { if (auto decl = dynamic_cast(identifier->annotation().referencedDeclaration)) { - solAssert(knownVariable(*decl), ""); + solAssert(m_context.knownVariable(*decl), ""); return decl; } } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index a4002280c..7a6372450 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -216,11 +216,8 @@ private: void initializeLocalVariables(FunctionDefinition const& _function); void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector const& _callArgs); - void resetVariable(VariableDeclaration const& _variable); void resetStateVariables(); void resetStorageReferences(); - void resetVariables(std::set const& _variables); - void resetVariables(std::function const& _filter); /// @returns the type without storage pointer information if it has it. TypePointer typeWithoutPointer(TypePointer const& _type); @@ -229,29 +226,14 @@ private: /// using the branch condition as guard. void mergeVariables(std::set const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); /// Tries to create an uninitialized variable and returns true on success. - /// This fails if the type is not supported. bool createVariable(VariableDeclaration const& _varDecl); - /// @returns true if _delc is a variable that is known at the current point, i.e. - /// has a valid index - bool knownVariable(VariableDeclaration const& _decl); /// @returns an expression denoting the value of the variable declared in @a _decl /// at the current point. smt::Expression currentValue(VariableDeclaration const& _decl); /// @returns an expression denoting the value of the variable declared in @a _decl /// at the given index. Does not ensure that this index exists. smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index); - /// Allocates a new index for the declaration, updates the current - /// index to this value and returns the expression. - smt::Expression newValue(VariableDeclaration const& _decl); - - /// Sets the value of the declaration to zero. - void setZeroValue(VariableDeclaration const& _decl); - void setZeroValue(smt::SymbolicVariable& _variable); - /// Resets the variable to an unknown value (in its range). - void setUnknownValue(VariableDeclaration const& decl); - void setUnknownValue(smt::SymbolicVariable& _variable); - /// 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) @@ -281,9 +263,6 @@ private: /// Add to the solver: the given expression implied by the current path conditions void addPathImpliedExpression(smt::Expression const& _e); - /// Removes local variables from the context. - void removeLocalVariables(); - /// Copy the SSA indices of m_variables. VariableIndices copyVariableIndices(); /// Resets the variable indices. @@ -305,7 +284,6 @@ private: /// An Expression may have multiple smt::Expression due to /// repeated calls to the same function. std::unordered_map> m_expressions; - std::unordered_map> m_variables; std::unordered_map> m_globalContext; /// Stores the instances of an Uninterpreted Function applied to arguments.