mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Why3: Direct references to variables using #
.
This commit is contained in:
parent
58110b27c1
commit
82a6ab486d
@ -198,6 +198,14 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
|
|||||||
return false;
|
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("let rec _" + _function.name());
|
||||||
add(" (state: state)");
|
add(" (state: state)");
|
||||||
for (auto const& param: _function.parameters())
|
for (auto const& param: _function.parameters())
|
||||||
@ -268,6 +276,11 @@ bool Why3Translator::visit(FunctionDefinition const& _function)
|
|||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void Why3Translator::endVisit(FunctionDefinition const&)
|
||||||
|
{
|
||||||
|
m_localVariables.clear();
|
||||||
|
}
|
||||||
|
|
||||||
bool Why3Translator::visit(Block const& _node)
|
bool Why3Translator::visit(Block const& _node)
|
||||||
{
|
{
|
||||||
addSourceFromDocStrings(_node.annotation());
|
addSourceFromDocStrings(_node.annotation());
|
||||||
@ -569,6 +582,28 @@ bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
|
|||||||
return false;
|
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)
|
void Why3Translator::visitIndentedUnlessBlock(Statement const& _statement)
|
||||||
{
|
{
|
||||||
bool isBlock = !!dynamic_cast<Block const*>(&_statement);
|
bool isBlock = !!dynamic_cast<Block const*>(&_statement);
|
||||||
@ -587,5 +622,37 @@ void Why3Translator::addSourceFromDocStrings(DocumentedAnnotation const& _annota
|
|||||||
{
|
{
|
||||||
auto why3Range = _annotation.docTags.equal_range("why3");
|
auto why3Range = _annotation.docTags.equal_range("why3");
|
||||||
for (auto i = why3Range.first; i != why3Range.second; ++i)
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
|
@ -74,6 +74,7 @@ private:
|
|||||||
virtual bool visit(ContractDefinition const& _contract) override;
|
virtual bool visit(ContractDefinition const& _contract) override;
|
||||||
virtual void endVisit(ContractDefinition const& _contract) override;
|
virtual void endVisit(ContractDefinition const& _contract) override;
|
||||||
virtual bool visit(FunctionDefinition const& _function) override;
|
virtual bool visit(FunctionDefinition const& _function) override;
|
||||||
|
virtual void endVisit(FunctionDefinition const& _function) override;
|
||||||
virtual bool visit(Block const&) override;
|
virtual bool visit(Block const&) override;
|
||||||
virtual bool visit(IfStatement const& _node) override;
|
virtual bool visit(IfStatement const& _node) override;
|
||||||
virtual bool visit(WhileStatement const& _node) override;
|
virtual bool visit(WhileStatement const& _node) override;
|
||||||
@ -98,12 +99,17 @@ private:
|
|||||||
}
|
}
|
||||||
|
|
||||||
bool isStateVariable(VariableDeclaration const* _var) const;
|
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
|
/// Visits the givin statement and indents it unless it is a block
|
||||||
/// (which does its own indentation).
|
/// (which does its own indentation).
|
||||||
void visitIndentedUnlessBlock(Statement const& _statement);
|
void visitIndentedUnlessBlock(Statement const& _statement);
|
||||||
|
|
||||||
void addSourceFromDocStrings(DocumentedAnnotation const& _annotation);
|
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_indentationAtLineStart = 0;
|
||||||
size_t m_indentation = 0;
|
size_t m_indentation = 0;
|
||||||
@ -114,6 +120,7 @@ private:
|
|||||||
bool m_errorOccured = false;
|
bool m_errorOccured = false;
|
||||||
|
|
||||||
std::vector<ASTPointer<VariableDeclaration>> const* m_stateVariables = nullptr;
|
std::vector<ASTPointer<VariableDeclaration>> const* m_stateVariables = nullptr;
|
||||||
|
std::map<std::string, VariableDeclaration const*> m_localVariables;
|
||||||
|
|
||||||
std::string m_result;
|
std::string m_result;
|
||||||
ErrorList& m_errors;
|
ErrorList& m_errors;
|
||||||
|
Loading…
Reference in New Issue
Block a user