From 82a6ab486d6ee1fa565db1d0b02f2b34c855e796 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 23 Nov 2015 00:26:04 +0100 Subject: [PATCH 1/3] Why3: Direct references to variables using `#`. --- libsolidity/formal/Why3Translator.cpp | 69 ++++++++++++++++++++++++++- libsolidity/formal/Why3Translator.h | 7 +++ 2 files changed, 75 insertions(+), 1 deletion(-) diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index 4c187a56b..8a3b767bc 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()); @@ -569,6 +582,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(&_statement); @@ -587,5 +622,37 @@ 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 989047e84..21dafa3c3 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> const* m_stateVariables = nullptr; + std::map m_localVariables; std::string m_result; ErrorList& m_errors; From 806507d5c0a12c64771d2611487cb100f88fe4ff Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 23 Nov 2015 00:57:58 +0100 Subject: [PATCH 2/3] addmod and mulmod for why3. --- libsolidity/formal/Why3Translator.cpp | 57 ++++++++++++++++++--------- 1 file changed, 38 insertions(+), 19 deletions(-) diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index 8a3b767bc..cd0366623 100644 --- a/libsolidity/formal/Why3Translator.cpp +++ b/libsolidity/formal/Why3Translator.cpp @@ -465,29 +465,48 @@ bool Why3Translator::visit(FunctionCall const& _node) return true; } FunctionType const& function = dynamic_cast(*_node.expression().annotation().type); - if (function.location() != FunctionType::Location::Internal) + switch (function.location()) { + 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."); + return true; + } + + //@TODO check type conversions + + 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; } - if (!_node.names().empty()) - { - error(_node, "Function calls with named arguments not supported."); - return true; - } - - //@TODO check type conversions - - add("("); - _node.expression().accept(*this); - add(" state"); - for (auto const& arg: _node.arguments()) - { - add(" "); - arg->accept(*this); - } - add(")"); - return false; } bool Why3Translator::visit(MemberAccess const& _node) From 10fe0a2434519e9be0b556c3566d8a7b17700750 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 23 Nov 2015 16:30:51 +0100 Subject: [PATCH 3/3] Style. --- libsolidity/formal/Why3Translator.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index cd0366623..356a336c7 100644 --- a/libsolidity/formal/Why3Translator.cpp +++ b/libsolidity/formal/Why3Translator.cpp @@ -650,7 +650,6 @@ string Why3Translator::transformVariableReferences(string const& _annotation) auto pos = _annotation.begin(); while (true) { - auto hash = find(pos, _annotation.end(), '#'); ret.append(pos, hash); if (hash == _annotation.end()) @@ -658,7 +657,11 @@ string Why3Translator::transformVariableReferences(string const& _annotation) 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'); + return + (_c != '_' && _c != '$') && + !('a' <= _c && _c <= 'z') && + !('A' <= _c && _c <= 'Z') && + !('0' <= _c && _c <= '9'); }); string varName(hash + 1, hashEnd); if (isLocalVariable(varName))