cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Consistent renaming of 'counters' and 'sequence' to 'index'

Browse Source
This commit is contained in:
Leonardo Alt 2018-10-17 11:32:01 +02:00
parent ec39fdcb3c
commit aa23326e06
10 changed files with 71 additions and 71 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

58
libsolidity/formal/SMTChecker.cpp
View File

@ -108,18 +108,18 @@ bool SMTChecker::visit(IfStatement const& _node)
if (isRootFunction())
checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
auto indicesEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
decltype(countersEndTrue) countersEndFalse;
decltype(indicesEndTrue) indicesEndFalse;
if (_node.falseStatement())
{
countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
indicesEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
}
else
countersEndFalse = copyVariableSequenceCounters();
indicesEndFalse = copyVariableIndices();
mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
mergeVariables(touchedVariables, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
return false;
}
@ -646,22 +646,22 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
m_interface->addAssertion(newValue(_variable) == _value);
}
SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
{
return visitBranch(_statement, &_condition);
}
SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
{
auto countersBeforeBranch = copyVariableSequenceCounters();
auto indicesBeforeBranch = copyVariableIndices();
if (_condition)
pushPathCondition(*_condition);
_statement.accept(*this);
if (_condition)
popPathCondition();
auto countersAfterBranch = copyVariableSequenceCounters();
resetVariableCounters(countersBeforeBranch);
return countersAfterBranch;
auto indicesAfterBranch = copyVariableIndices();
resetVariableIndices(indicesBeforeBranch);
return indicesAfterBranch;
}
void SMTChecker::checkCondition(
@ -894,19 +894,19 @@ void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables)
}
}
void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse)
void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
{
set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end());
for (auto const* decl: uniqueVars)
{
solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), "");
int trueCounter = _countersEndTrue.at(decl);
int falseCounter = _countersEndFalse.at(decl);
solAssert(trueCounter != falseCounter, "");
solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), "");
int trueIndex = _indicesEndTrue.at(decl);
int falseIndex = _indicesEndFalse.at(decl);
solAssert(trueIndex != falseIndex, "");
m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
_condition,
valueAtSequence(*decl, trueCounter),
valueAtSequence(*decl, falseCounter))
valueAtIndex(*decl, trueIndex),
valueAtIndex(*decl, falseIndex))
);
}
}
@ -946,19 +946,19 @@ bool SMTChecker::knownVariable(VariableDeclaration const& _decl)
smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl)
{
solAssert(knownVariable(_decl), "");
return m_variables.at(&_decl)->current();
return m_variables.at(&_decl)->currentValue();
}
smt::Expression SMTChecker::valueAtSequence(VariableDeclaration const& _decl, int _sequence)
smt::Expression SMTChecker::valueAtIndex(VariableDeclaration const& _decl, int _index)
{
solAssert(knownVariable(_decl), "");
return m_variables.at(&_decl)->valueAtSequence(_sequence);
return m_variables.at(&_decl)->valueAtIndex(_index);
}
smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
{
solAssert(knownVariable(_decl), "");
return m_variables.at(&_decl)->increase();
return m_variables.at(&_decl)->increaseIndex();
}
void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
@ -1070,16 +1070,16 @@ bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef)
return contains(m_functionPath, _funDef);
}
SMTChecker::VariableSequenceCounters SMTChecker::copyVariableSequenceCounters()
SMTChecker::VariableIndices SMTChecker::copyVariableIndices()
{
VariableSequenceCounters counters;
for (auto var: m_variables)
counters.emplace(var.first, var.second->index());
return counters;
VariableIndices indices;
for (auto const& var: m_variables)
indices.emplace(var.first, var.second->index());
return indices;
}
void SMTChecker::resetVariableCounters(VariableSequenceCounters const& _counters)
void SMTChecker::resetVariableIndices(VariableIndices const& _indices)
{
for (auto var: _counters)
for (auto const& var: _indices)
m_variables.at(var.first)->index() = var.second;
}

26
libsolidity/formal/SMTChecker.h
View File

@ -86,13 +86,13 @@ private:
void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
/// Maps a variable to an SSA index.
using VariableSequenceCounters = std::unordered_map<VariableDeclaration const*, int>;
using VariableIndices = 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.
/// @returns the variable sequence counter after visiting the branch.
VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression _condition);
/// @returns the variable indices after visiting the branch.
VariableIndices visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
VariableIndices visitBranch(Statement const& _statement, smt::Expression _condition);
/// Check that a condition can be satisfied.
void checkCondition(
@ -125,7 +125,7 @@ private:
/// Given two different branches and the touched variables,
/// merge the touched variables into after-branch ite variables
/// using the branch condition as guard.
void mergeVariables(std::vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse);
void mergeVariables(std::vector<VariableDeclaration const*> 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);
@ -133,16 +133,16 @@ private:
static std::string uniqueSymbol(Expression const& _expr);
/// @returns true if _delc is a variable that is known at the current point, i.e.
/// has a valid sequence number
/// 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 sequence point. Does not ensure that this sequence point exists.
smt::Expression valueAtSequence(VariableDeclaration const& _decl, int _sequence);
/// Allocates a new sequence number for the declaration, updates the current
/// sequence number to this value and returns the expression.
/// 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.
@ -177,9 +177,9 @@ private:
bool hasVariable(VariableDeclaration const& _e) const;
/// Copy the SSA indices of m_variables.
VariableSequenceCounters copyVariableSequenceCounters();
/// Resets the variable counters.
void resetVariableCounters(VariableSequenceCounters const& _counters);
VariableIndices copyVariableIndices();
/// Resets the variable indices.
void resetVariableIndices(VariableIndices const& _indices);
std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage;

6
libsolidity/formal/SSAVariable.cpp
View File

@ -27,7 +27,7 @@ SSAVariable::SSAVariable()
void SSAVariable::resetIndex()
{
m_currentSequenceCounter = 0;
m_nextFreeSequenceCounter.reset (new int);
*m_nextFreeSequenceCounter = 1;
m_currentIndex = 0;
m_nextFreeIndex.reset (new int);
*m_nextFreeIndex = 1;
}

12
libsolidity/formal/SSAVariable.h
View File

@ -34,19 +34,19 @@ public:
void resetIndex();
/// This function returns the current index of this SSA variable.
int index() const { return m_currentSequenceCounter; }
int& index() { return m_currentSequenceCounter; }
int index() const { return m_currentIndex; }
int& index() { return m_currentIndex; }
int operator++()
{
return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++;
return m_currentIndex = (*m_nextFreeIndex)++;
}
private:
int m_currentSequenceCounter;
/// The next free sequence counter is a shared pointer because we want
int m_currentIndex;
/// The next free index is a shared pointer because we want
/// the copy and the copied to share it.
std::shared_ptr<int> m_nextFreeSequenceCounter;
std::shared_ptr<int> m_nextFreeIndex;
};
}

6
libsolidity/formal/SymbolicBoolVariable.cpp
View File

@ -31,14 +31,14 @@ SymbolicBoolVariable::SymbolicBoolVariable(
solAssert(_type.category() == Type::Category::Bool, "");
}
smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const
smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
{
return m_interface.newBool(uniqueSymbol(_seq));
return m_interface.newBool(uniqueSymbol(_index));
}
void SymbolicBoolVariable::setZeroValue()
{
m_interface.addAssertion(current() == smt::Expression(false));
m_interface.addAssertion(currentValue() == smt::Expression(false));
}
void SymbolicBoolVariable::setUnknownValue()

2
libsolidity/formal/SymbolicBoolVariable.h
View File

@ -42,7 +42,7 @@ public:
void setUnknownValue();
protected:
smt::Expression valueAtSequence(int _seq) const;
smt::Expression valueAtIndex(int _index) const;
};
}

14
libsolidity/formal/SymbolicIntVariable.cpp
View File

@ -35,14 +35,14 @@ SymbolicIntVariable::SymbolicIntVariable(
);
}
smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const
smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
{
return m_interface.newInteger(uniqueSymbol(_seq));
return m_interface.newInteger(uniqueSymbol(_index));
}
void SymbolicIntVariable::setZeroValue()
{
m_interface.addAssertion(current() == 0);
m_interface.addAssertion(currentValue() == 0);
}
void SymbolicIntVariable::setUnknownValue()
@ -51,15 +51,15 @@ void SymbolicIntVariable::setUnknownValue()
{
auto intType = dynamic_cast<IntegerType const*>(&m_type);
solAssert(intType, "");
m_interface.addAssertion(current() >= minValue(*intType));
m_interface.addAssertion(current() <= maxValue(*intType));
m_interface.addAssertion(currentValue() >= minValue(*intType));
m_interface.addAssertion(currentValue() <= maxValue(*intType));
}
else
{
solAssert(m_type.category() == Type::Category::Address, "");
IntegerType addrType{160};
m_interface.addAssertion(current() >= minValue(addrType));
m_interface.addAssertion(current() <= maxValue(addrType));
m_interface.addAssertion(currentValue() >= minValue(addrType));
m_interface.addAssertion(currentValue() <= maxValue(addrType));
}
}

2
libsolidity/formal/SymbolicIntVariable.h
View File

@ -45,7 +45,7 @@ public:
static smt::Expression maxValue(IntegerType const& _t);
protected:
smt::Expression valueAtSequence(int _seq) const;
smt::Expression valueAtIndex(int _index) const;
};
}

4
libsolidity/formal/SymbolicVariable.cpp
View File

@ -35,9 +35,9 @@ SymbolicVariable::SymbolicVariable(
{
}
string SymbolicVariable::uniqueSymbol(int _seq) const
string SymbolicVariable::uniqueSymbol(int _index) const
{
return m_uniqueName + "_" + to_string(_seq);
return m_uniqueName + "_" + to_string(_index);
}

12
libsolidity/formal/SymbolicVariable.h
View File

@ -45,17 +45,17 @@ public:
);
virtual ~SymbolicVariable() = default;
smt::Expression current() const
smt::Expression currentValue() const
{
return valueAtSequence(m_ssa->index());
return valueAtIndex(m_ssa->index());
}
virtual smt::Expression valueAtSequence(int _seq) const = 0;
virtual smt::Expression valueAtIndex(int _index) const = 0;
smt::Expression increase()
smt::Expression increaseIndex()
{
++(*m_ssa);
return current();
return currentValue();
}
int index() const { return m_ssa->index(); }
@ -68,7 +68,7 @@ public:
virtual void setUnknownValue() = 0;
protected:
std::string uniqueSymbol(int _seq) const;
std::string uniqueSymbol(int _index) const;
Type const& m_type;
std::string m_uniqueName;