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

Merge pull request #241 from chriseth/why3VariablesInConditions

Browse Source 
Why3 variables in conditions
This commit is contained in:
chriseth 2015-11-24 11:33:35 +01:00
commit e59b9b445a
2 changed files with 116 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

97
libsolidity/formal/Why3Translator.cpp
View File

@ -198,6 +198,14 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
return false;
}
m_localVariables.clear();
for (auto const& var: _function.parameters())
m_localVariables[var->name()] = var.get();
for (auto const& var: _function.returnParameters())
m_localVariables[var->name()] = var.get();
for (auto const& var: _function.localVariables())
m_localVariables[var->name()] = var;
add("let rec _" + _function.name());
add(" (state: state)");
for (auto const& param: _function.parameters())
@ -268,6 +276,11 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
return false;
}
void Why3Translator::endVisit(FunctionDefinition const&)
{
m_localVariables.clear();
}
bool Why3Translator::visit(Block const& _node)
{
addSourceFromDocStrings(_node.annotation());
@ -452,11 +465,25 @@ bool Why3Translator::visit(FunctionCall const& _node)
return true;
}
FunctionType const& function = dynamic_cast<FunctionType const&>(*_node.expression().annotation().type);
if (function.location() != FunctionType::Location::Internal)
switch (function.location())
{
error(_node, "Only internal function calls supported.");
return true;
case FunctionType::Location::AddMod:
case FunctionType::Location::MulMod:
{
//@todo require that third parameter is not zero
add("(of_int (mod (Int.(");
add(function.location() == FunctionType::Location::AddMod ? "+" : "*");
add(") (to_int ");
_node.arguments().at(0)->accept(*this);
add(") (to_int ");
_node.arguments().at(1)->accept(*this);
add(")) (to_int ");
_node.arguments().at(2)->accept(*this);
add(")))");
return false;
}
case FunctionType::Location::Internal:
{
if (!_node.names().empty())
{
error(_node, "Function calls with named arguments not supported.");
@ -475,6 +502,11 @@ bool Why3Translator::visit(FunctionCall const& _node)
}
add(")");
return false;
}
default:
error(_node, "Only internal function calls supported.");
return true;
}
}
bool Why3Translator::visit(MemberAccess const& _node)
@ -569,6 +601,28 @@ bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
return false;
}
bool Why3Translator::isStateVariable(string const& _name) const
{
solAssert(!!m_stateVariables, "");
for (auto const& var: *m_stateVariables)
if (var->name() == _name)
return true;
return false;
}
bool Why3Translator::isLocalVariable(VariableDeclaration const* _var) const
{
for (auto const& var: m_localVariables)
if (var.second == _var)
return true;
return false;
}
bool Why3Translator::isLocalVariable(string const& _name) const
{
return m_localVariables.count(_name);
}
void Why3Translator::visitIndentedUnlessBlock(Statement const& _statement)
{
bool isBlock = !!dynamic_cast<Block const*>(&_statement);
@ -587,5 +641,40 @@ void Why3Translator::addSourceFromDocStrings(DocumentedAnnotation const& _annota
{
auto why3Range = _annotation.docTags.equal_range("why3");
for (auto i = why3Range.first; i != why3Range.second; ++i)
addLine(i->second.content);
addLine(transformVariableReferences(i->second.content));
}
string Why3Translator::transformVariableReferences(string const& _annotation)
{
string ret;
auto pos = _annotation.begin();
while (true)
{
auto hash = find(pos, _annotation.end(), '#');
ret.append(pos, hash);
if (hash == _annotation.end())
break;
auto hashEnd = find_if(hash + 1, _annotation.end(), [](char _c)
{
return
(_c != '_' && _c != '$') &&
!('a' <= _c && _c <= 'z') &&
!('A' <= _c && _c <= 'Z') &&
!('0' <= _c && _c <= '9');
});
string varName(hash + 1, hashEnd);
if (isLocalVariable(varName))
ret += "(to_int !_" + varName + ")";
else if (isStateVariable(varName))
ret += "(to_int !(state._" + varName + "))";
else if (varName == "result") //@todo actually use the name of the return parameters
ret += "(to_int result)";
else
ret.append(hash, hashEnd);
pos = hashEnd;
}
return ret;
}

7
libsolidity/formal/Why3Translator.h
View File

@ -74,6 +74,7 @@ private:
virtual bool visit(ContractDefinition const& _contract) override;
virtual void endVisit(ContractDefinition const& _contract) override;
virtual bool visit(FunctionDefinition const& _function) override;
virtual void endVisit(FunctionDefinition const& _function) override;
virtual bool visit(Block const&) override;
virtual bool visit(IfStatement const& _node) override;
virtual bool visit(WhileStatement const& _node) override;
@ -98,12 +99,17 @@ private:
}
bool isStateVariable(VariableDeclaration const* _var) const;
bool isStateVariable(std::string const& _name) const;
bool isLocalVariable(VariableDeclaration const* _var) const;
bool isLocalVariable(std::string const& _name) const;
/// Visits the givin statement and indents it unless it is a block
/// (which does its own indentation).
void visitIndentedUnlessBlock(Statement const& _statement);
void addSourceFromDocStrings(DocumentedAnnotation const& _annotation);
/// Transforms substring like `#varName` and `#stateVarName` to code that evaluates to their value.
std::string transformVariableReferences(std::string const& _annotation);
size_t m_indentationAtLineStart = 0;
size_t m_indentation = 0;
@ -114,6 +120,7 @@ private:
bool m_errorOccured = false;
std::vector<ASTPointer<VariableDeclaration>> const* m_stateVariables = nullptr;
std::map<std::string, VariableDeclaration const*> m_localVariables;
std::string m_result;
ErrorList& m_errors;