diff options
| -rw-r--r-- | libsolidity/formal/Why3Translator.cpp | 125 | ||||
| -rw-r--r-- | libsolidity/formal/Why3Translator.h | 7 |
2 files changed, 114 insertions, 18 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index 4c187a56..356a336c 100644 --- a/libsolidity/formal/Why3Translator.cpp +++ b/libsolidity/formal/Why3Translator.cpp @@ -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,29 +465,48 @@ 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; - } - if (!_node.names().empty()) + case FunctionType::Location::AddMod: + case FunctionType::Location::MulMod: { - error(_node, "Function calls with named arguments not supported."); - return true; + //@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."); + return true; + } - //@TODO check type conversions + //@TODO check type conversions - add("("); - _node.expression().accept(*this); - add(" state"); - for (auto const& arg: _node.arguments()) - { - add(" "); - arg->accept(*this); + add("("); + _node.expression().accept(*this); + add(" state"); + for (auto const& arg: _node.arguments()) + { + add(" "); + arg->accept(*this); + } + add(")"); + return false; + } + default: + error(_node, "Only internal function calls supported."); + return true; } - add(")"); - return false; } 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; } + diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h index 989047e8..21dafa3c 100644 --- a/libsolidity/formal/Why3Translator.h +++ b/libsolidity/formal/Why3Translator.h @@ -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; |