From 8fb49d85f9464bfa0d17ac77d2e19b3ba371c53c Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 26 Oct 2015 17:20:29 +0100 Subject: Allow docstrings for statements. --- libsolidity/analysis/DocStringAnalyser.cpp | 33 ++++++++++----- libsolidity/analysis/DocStringAnalyser.h | 9 +++- libsolidity/ast/AST.cpp | 7 +++ libsolidity/ast/AST.h | 53 ++++++++++++++++------- libsolidity/ast/ASTAnnotations.h | 8 +++- libsolidity/parsing/Parser.cpp | 68 +++++++++++++++++------------- libsolidity/parsing/Parser.h | 12 +++--- 7 files changed, 126 insertions(+), 64 deletions(-) diff --git a/libsolidity/analysis/DocStringAnalyser.cpp b/libsolidity/analysis/DocStringAnalyser.cpp index 41bff87e..4f75f03d 100644 --- a/libsolidity/analysis/DocStringAnalyser.cpp +++ b/libsolidity/analysis/DocStringAnalyser.cpp @@ -39,12 +39,8 @@ bool DocStringAnalyser::analyseDocStrings(SourceUnit const& _sourceUnit) bool DocStringAnalyser::visit(ContractDefinition const& _node) { - parseDocStrings(_node, _node.annotation()); - - static const set validTags = set{"author", "title", "dev", "notice"}; - for (auto const& docTag: _node.annotation().docTags) - if (!validTags.count(docTag.first)) - appendError("Doc tag @" + docTag.first + " not valid for contracts."); + static const set validTags = set{"author", "title", "dev", "notice", "why3"}; + parseDocStrings(_node, _node.annotation(), validTags, "contracts"); return true; } @@ -69,17 +65,24 @@ bool DocStringAnalyser::visit(EventDefinition const& _node) return true; } +bool DocStringAnalyser::visitNode(ASTNode const& _node) +{ + if (auto node = dynamic_cast(&_node)) + { + static const set validTags = {"why3"}; + parseDocStrings(*node, node->annotation(), validTags, "statements"); + } + return true; +} + void DocStringAnalyser::handleCallable( CallableDeclaration const& _callable, Documented const& _node, DocumentedAnnotation& _annotation ) { - parseDocStrings(_node, _annotation); static const set validTags = set{"author", "dev", "notice", "return", "param", "why3"}; - for (auto const& docTag: _annotation.docTags) - if (!validTags.count(docTag.first)) - appendError("Doc tag @" + docTag.first + " not valid for functions."); + parseDocStrings(_node, _annotation, validTags, "functions"); set validParams; for (auto const& p: _callable.parameters()) @@ -97,7 +100,12 @@ void DocStringAnalyser::handleCallable( ); } -void DocStringAnalyser::parseDocStrings(Documented const& _node, DocumentedAnnotation& _annotation) +void DocStringAnalyser::parseDocStrings( + Documented const& _node, + DocumentedAnnotation& _annotation, + set const& _validTags, + string const& _nodeName +) { DocStringParser parser; if (_node.documentation() && !_node.documentation()->empty()) @@ -106,6 +114,9 @@ void DocStringAnalyser::parseDocStrings(Documented const& _node, DocumentedAnnot m_errorOccured = true; _annotation.docTags = parser.tags(); } + for (auto const& docTag: _annotation.docTags) + if (!_validTags.count(docTag.first)) + appendError("Doc tag @" + docTag.first + " not valid for " + _nodeName + "."); } void DocStringAnalyser::appendError(string const& _description) diff --git a/libsolidity/analysis/DocStringAnalyser.h b/libsolidity/analysis/DocStringAnalyser.h index 06384c8d..cdf297e3 100644 --- a/libsolidity/analysis/DocStringAnalyser.h +++ b/libsolidity/analysis/DocStringAnalyser.h @@ -46,13 +46,20 @@ private: virtual bool visit(ModifierDefinition const& _modifier) override; virtual bool visit(EventDefinition const& _event) override; + virtual bool visitNode(ASTNode const&) override; + void handleCallable( CallableDeclaration const& _callable, Documented const& _node, DocumentedAnnotation& _annotation ); - void parseDocStrings(Documented const& _node, DocumentedAnnotation& _annotation); + void parseDocStrings( + Documented const& _node, + DocumentedAnnotation& _annotation, + std::set const& _validTags, + std::string const& _nodeName + ); void appendError(std::string const& _description); diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp index 9d1fb811..41a4d182 100644 --- a/libsolidity/ast/AST.cpp +++ b/libsolidity/ast/AST.cpp @@ -336,6 +336,13 @@ VariableDeclarationAnnotation& VariableDeclaration::annotation() const return static_cast(*m_annotation); } +StatementAnnotation& Statement::annotation() const +{ + if (!m_annotation) + m_annotation = new StatementAnnotation(); + return static_cast(*m_annotation); +} + ReturnAnnotation& Return::annotation() const { if (!m_annotation) diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h index 6a593d3e..1a204dca 100644 --- a/libsolidity/ast/AST.h +++ b/libsolidity/ast/AST.h @@ -792,10 +792,15 @@ private: /** * Abstract base class for statements. */ -class Statement: public ASTNode +class Statement: public ASTNode, public Documented { public: - explicit Statement(SourceLocation const& _location): ASTNode(_location) {} + explicit Statement( + SourceLocation const& _location, + ASTPointer const& _docString + ): ASTNode(_location), Documented(_docString) {} + + virtual StatementAnnotation& annotation() const override; }; /** @@ -806,9 +811,10 @@ class Block: public Statement public: Block( SourceLocation const& _location, + ASTPointer const& _docString, std::vector> const& _statements ): - Statement(_location), m_statements(_statements) {} + Statement(_location, _docString), m_statements(_statements) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; @@ -823,7 +829,10 @@ private: class PlaceholderStatement: public Statement { public: - explicit PlaceholderStatement(SourceLocation const& _location): Statement(_location) {} + explicit PlaceholderStatement( + SourceLocation const& _location, + ASTPointer const& _docString + ): Statement(_location, _docString) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; @@ -838,11 +847,12 @@ class IfStatement: public Statement public: IfStatement( SourceLocation const& _location, + ASTPointer const& _docString, ASTPointer const& _condition, ASTPointer const& _trueBody, ASTPointer const& _falseBody ): - Statement(_location), + Statement(_location, _docString), m_condition(_condition), m_trueBody(_trueBody), m_falseBody(_falseBody) @@ -867,7 +877,10 @@ private: class BreakableStatement: public Statement { public: - explicit BreakableStatement(SourceLocation const& _location): Statement(_location) {} + explicit BreakableStatement( + SourceLocation const& _location, + ASTPointer const& _docString + ): Statement(_location, _docString) {} }; class WhileStatement: public BreakableStatement @@ -875,10 +888,11 @@ class WhileStatement: public BreakableStatement public: WhileStatement( SourceLocation const& _location, + ASTPointer const& _docString, ASTPointer const& _condition, ASTPointer const& _body ): - BreakableStatement(_location), m_condition(_condition), m_body(_body) {} + BreakableStatement(_location, _docString), m_condition(_condition), m_body(_body) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; @@ -898,12 +912,13 @@ class ForStatement: public BreakableStatement public: ForStatement( SourceLocation const& _location, + ASTPointer const& _docString, ASTPointer const& _initExpression, ASTPointer const& _conditionExpression, ASTPointer const& _loopExpression, ASTPointer const& _body ): - BreakableStatement(_location), + BreakableStatement(_location, _docString), m_initExpression(_initExpression), m_condExpression(_conditionExpression), m_loopExpression(_loopExpression), @@ -931,7 +946,8 @@ private: class Continue: public Statement { public: - explicit Continue(SourceLocation const& _location): Statement(_location) {} + explicit Continue(SourceLocation const& _location, ASTPointer const& _docString): + Statement(_location, _docString) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; }; @@ -939,7 +955,8 @@ public: class Break: public Statement { public: - explicit Break(SourceLocation const& _location): Statement(_location) {} + explicit Break(SourceLocation const& _location, ASTPointer const& _docString): + Statement(_location, _docString) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; }; @@ -947,8 +964,11 @@ public: class Return: public Statement { public: - Return(SourceLocation const& _location, ASTPointer _expression): - Statement(_location), m_expression(_expression) {} + Return( + SourceLocation const& _location, + ASTPointer const& _docString, + ASTPointer _expression + ): Statement(_location, _docString), m_expression(_expression) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; @@ -966,7 +986,8 @@ private: class Throw: public Statement { public: - explicit Throw(SourceLocation const& _location): Statement(_location) {} + explicit Throw(SourceLocation const& _location, ASTPointer const& _docString): + Statement(_location, _docString) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; }; @@ -985,10 +1006,11 @@ class VariableDeclarationStatement: public Statement public: VariableDeclarationStatement( SourceLocation const& _location, + ASTPointer const& _docString, std::vector> const& _variables, ASTPointer const& _initialValue ): - Statement(_location), m_variables(_variables), m_initialValue(_initialValue) {} + Statement(_location, _docString), m_variables(_variables), m_initialValue(_initialValue) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; @@ -1012,9 +1034,10 @@ class ExpressionStatement: public Statement public: ExpressionStatement( SourceLocation const& _location, + ASTPointer const& _docString, ASTPointer _expression ): - Statement(_location), m_expression(_expression) {} + Statement(_location, _docString), m_expression(_expression) {} virtual void accept(ASTVisitor& _visitor) override; virtual void accept(ASTConstVisitor& _visitor) const override; diff --git a/libsolidity/ast/ASTAnnotations.h b/libsolidity/ast/ASTAnnotations.h index 094a178e..bb59ceae 100644 --- a/libsolidity/ast/ASTAnnotations.h +++ b/libsolidity/ast/ASTAnnotations.h @@ -90,7 +90,11 @@ struct VariableDeclarationAnnotation: ASTAnnotation TypePointer type; }; -struct ReturnAnnotation: ASTAnnotation +struct StatementAnnotation: ASTAnnotation, DocumentedAnnotation +{ +}; + +struct ReturnAnnotation: StatementAnnotation { /// Reference to the return parameters of the function. ParameterList const* functionReturnParameters = nullptr; @@ -109,7 +113,7 @@ struct UserDefinedTypeNameAnnotation: TypeNameAnnotation Declaration const* referencedDeclaration = nullptr; }; -struct VariableDeclarationStatementAnnotation: ASTAnnotation +struct VariableDeclarationStatementAnnotation: StatementAnnotation { /// Information about which component of the value is assigned to which variable. /// The pointer can be null to signify that the component is discarded. diff --git a/libsolidity/parsing/Parser.cpp b/libsolidity/parsing/Parser.cpp index 35872f78..d89218bb 100644 --- a/libsolidity/parsing/Parser.cpp +++ b/libsolidity/parsing/Parser.cpp @@ -600,7 +600,7 @@ ASTPointer Parser::parseParameterList( return nodeFactory.createNode(parameters); } -ASTPointer Parser::parseBlock() +ASTPointer Parser::parseBlock(ASTPointer const& _docString) { ASTNodeFactory nodeFactory(*this); expectToken(Token::LBrace); @@ -609,29 +609,32 @@ ASTPointer Parser::parseBlock() statements.push_back(parseStatement()); nodeFactory.markEndPosition(); expectToken(Token::RBrace); - return nodeFactory.createNode(statements); + return nodeFactory.createNode(_docString, statements); } ASTPointer Parser::parseStatement() { + ASTPointer docString; + if (m_scanner->currentCommentLiteral() != "") + docString = make_shared(m_scanner->currentCommentLiteral()); ASTPointer statement; switch (m_scanner->currentToken()) { case Token::If: - return parseIfStatement(); + return parseIfStatement(docString); case Token::While: - return parseWhileStatement(); + return parseWhileStatement(docString); case Token::For: - return parseForStatement(); + return parseForStatement(docString); case Token::LBrace: - return parseBlock(); + return parseBlock(docString); // starting from here, all statements must be terminated by a semicolon case Token::Continue: - statement = ASTNodeFactory(*this).createNode(); + statement = ASTNodeFactory(*this).createNode(docString); m_scanner->next(); break; case Token::Break: - statement = ASTNodeFactory(*this).createNode(); + statement = ASTNodeFactory(*this).createNode(docString); m_scanner->next(); break; case Token::Return: @@ -643,31 +646,31 @@ ASTPointer Parser::parseStatement() expression = parseExpression(); nodeFactory.setEndPositionFromNode(expression); } - statement = nodeFactory.createNode(expression); + statement = nodeFactory.createNode(docString, expression); break; } case Token::Throw: { - statement = ASTNodeFactory(*this).createNode(); + statement = ASTNodeFactory(*this).createNode(docString); m_scanner->next(); break; } case Token::Identifier: if (m_insideModifier && m_scanner->currentLiteral() == "_") { - statement = ASTNodeFactory(*this).createNode(); + statement = ASTNodeFactory(*this).createNode(docString); m_scanner->next(); return statement; } // fall-through default: - statement = parseSimpleStatement(); + statement = parseSimpleStatement(docString); } expectToken(Token::Semicolon); return statement; } -ASTPointer Parser::parseIfStatement() +ASTPointer Parser::parseIfStatement(ASTPointer const& _docString) { ASTNodeFactory nodeFactory(*this); expectToken(Token::If); @@ -684,10 +687,10 @@ ASTPointer Parser::parseIfStatement() } else nodeFactory.setEndPositionFromNode(trueBody); - return nodeFactory.createNode(condition, trueBody, falseBody); + return nodeFactory.createNode(_docString, condition, trueBody, falseBody); } -ASTPointer Parser::parseWhileStatement() +ASTPointer Parser::parseWhileStatement(ASTPointer const& _docString) { ASTNodeFactory nodeFactory(*this); expectToken(Token::While); @@ -696,10 +699,10 @@ ASTPointer Parser::parseWhileStatement() expectToken(Token::RParen); ASTPointer body = parseStatement(); nodeFactory.setEndPositionFromNode(body); - return nodeFactory.createNode(condition, body); + return nodeFactory.createNode(_docString, condition, body); } -ASTPointer Parser::parseForStatement() +ASTPointer Parser::parseForStatement(ASTPointer const& _docString) { ASTNodeFactory nodeFactory(*this); ASTPointer initExpression; @@ -710,7 +713,7 @@ ASTPointer Parser::parseForStatement() // LTODO: Maybe here have some predicate like peekExpression() instead of checking for semicolon and RParen? if (m_scanner->currentToken() != Token::Semicolon) - initExpression = parseSimpleStatement(); + initExpression = parseSimpleStatement(ASTPointer()); expectToken(Token::Semicolon); if (m_scanner->currentToken() != Token::Semicolon) @@ -718,18 +721,21 @@ ASTPointer Parser::parseForStatement() expectToken(Token::Semicolon); if (m_scanner->currentToken() != Token::RParen) - loopExpression = parseExpressionStatement(); + loopExpression = parseExpressionStatement(ASTPointer()); expectToken(Token::RParen); ASTPointer body = parseStatement(); nodeFactory.setEndPositionFromNode(body); - return nodeFactory.createNode(initExpression, - conditionExpression, - loopExpression, - body); + return nodeFactory.createNode( + _docString, + initExpression, + conditionExpression, + loopExpression, + body + ); } -ASTPointer Parser::parseSimpleStatement() +ASTPointer Parser::parseSimpleStatement(ASTPointer const& _docString) { // These two cases are very hard to distinguish: // x[7 * 20 + 3] a; - x[7 * 20 + 3] = 9; @@ -740,9 +746,9 @@ ASTPointer Parser::parseSimpleStatement() switch (peekStatementType()) { case LookAheadInfo::VariableDeclarationStatement: - return parseVariableDeclarationStatement(); + return parseVariableDeclarationStatement(_docString); case LookAheadInfo::ExpressionStatement: - return parseExpressionStatement(); + return parseExpressionStatement(_docString); default: break; } @@ -781,12 +787,13 @@ ASTPointer Parser::parseSimpleStatement() } if (m_scanner->currentToken() == Token::Identifier || Token::isLocationSpecifier(m_scanner->currentToken())) - return parseVariableDeclarationStatement(typeNameIndexAccessStructure(path, indices)); + return parseVariableDeclarationStatement(_docString, typeNameIndexAccessStructure(path, indices)); else - return parseExpressionStatement(expressionFromIndexAccessStructure(path, indices)); + return parseExpressionStatement(_docString, expressionFromIndexAccessStructure(path, indices)); } ASTPointer Parser::parseVariableDeclarationStatement( + ASTPointer const& _docString, ASTPointer const& _lookAheadArrayType ) { @@ -845,15 +852,16 @@ ASTPointer Parser::parseVariableDeclarationStateme value = parseExpression(); nodeFactory.setEndPositionFromNode(value); } - return nodeFactory.createNode(variables, value); + return nodeFactory.createNode(_docString, variables, value); } ASTPointer Parser::parseExpressionStatement( + ASTPointer const& _docString, ASTPointer const& _lookAheadIndexAccessStructure ) { ASTPointer expression = parseExpression(_lookAheadIndexAccessStructure); - return ASTNodeFactory(*this, expression).createNode(expression); + return ASTNodeFactory(*this, expression).createNode(_docString, expression); } ASTPointer Parser::parseExpression( diff --git a/libsolidity/parsing/Parser.h b/libsolidity/parsing/Parser.h index 5e226ba5..663c0f92 100644 --- a/libsolidity/parsing/Parser.h +++ b/libsolidity/parsing/Parser.h @@ -82,17 +82,19 @@ private: VarDeclParserOptions const& _options, bool _allowEmpty = true ); - ASTPointer parseBlock(); + ASTPointer parseBlock(ASTPointer const& _docString = {}); ASTPointer parseStatement(); - ASTPointer parseIfStatement(); - ASTPointer parseWhileStatement(); - ASTPointer parseForStatement(); + ASTPointer parseIfStatement(ASTPointer const& _docString); + ASTPointer parseWhileStatement(ASTPointer const& _docString); + ASTPointer parseForStatement(ASTPointer const& _docString); /// A "simple statement" can be a variable declaration statement or an expression statement. - ASTPointer parseSimpleStatement(); + ASTPointer parseSimpleStatement(ASTPointer const& _docString); ASTPointer parseVariableDeclarationStatement( + ASTPointer const& _docString, ASTPointer const& _lookAheadArrayType = ASTPointer() ); ASTPointer parseExpressionStatement( + ASTPointer const& _docString, ASTPointer const& _lookAheadIndexAccessStructure = ASTPointer() ); ASTPointer parseExpression( -- cgit v1.2.3 From a957322fd7ff87460e5de3b1c5abcfb021acc1b2 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 21 Oct 2015 16:43:31 +0200 Subject: Preliminary why3 code output. --- libsolidity/CMakeLists.txt | 1 + libsolidity/formal/Why3Translator.cpp | 525 ++++++++++++++++++++++++++++++++ libsolidity/formal/Why3Translator.h | 115 +++++++ libsolidity/interface/CompilerStack.cpp | 13 + libsolidity/interface/CompilerStack.h | 7 +- libsolidity/interface/Exceptions.cpp | 39 +-- libsolidity/interface/Exceptions.h | 1 + solc/CommandLineInterface.cpp | 69 +++-- solc/CommandLineInterface.h | 4 +- 9 files changed, 730 insertions(+), 44 deletions(-) create mode 100644 libsolidity/formal/Why3Translator.cpp create mode 100644 libsolidity/formal/Why3Translator.h diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 62e7bf93..d59afc2d 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -3,6 +3,7 @@ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DSTATICLIB") aux_source_directory(analysis SRC_LIST) aux_source_directory(ast SRC_LIST) aux_source_directory(codegen SRC_LIST) +aux_source_directory(formal SRC_LIST) aux_source_directory(interface SRC_LIST) aux_source_directory(parsing SRC_LIST) diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp new file mode 100644 index 00000000..0d3d1586 --- /dev/null +++ b/libsolidity/formal/Why3Translator.cpp @@ -0,0 +1,525 @@ +/* + This file is part of cpp-ethereum. + + cpp-ethereum is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + cpp-ethereum is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with cpp-ethereum. If not, see . +*/ +/** + * @author Christian + * @date 2015 + * Component that translates Solidity code into the why3 programming language. + */ + +#include + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +bool Why3Translator::process(SourceUnit const& _source) +{ + try + { + m_indentation = 0; + if (!m_result.empty()) + fatalError(_source, "Multiple source units not yet supported"); + appendPreface(); + _source.accept(*this); + addLine("end"); + } + catch (FatalError& _e) + { + solAssert(m_errorOccured, ""); + } + return !m_errorOccured; +} + +void Why3Translator::error(ASTNode const& _node, string const& _description) +{ + auto err = make_shared(Error::Type::FormalError); + *err << + errinfo_sourceLocation(_node.location()) << + errinfo_comment(_description); + m_errors.push_back(err); + m_errorOccured = true; +} + +void Why3Translator::fatalError(ASTNode const& _node, string const& _description) +{ + error(_node, _description); + BOOST_THROW_EXCEPTION(FatalError()); +} + +void Why3Translator::appendPreface() +{ + m_result += R"( +module UInt256 + use import mach.int.Unsigned + type uint256 + constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff + clone export mach.int.Unsigned with + type t = uint256, + constant max = max_uint256 +end + +module Solidity +use import int.Int +use import ref.Ref +use import map.Map +use import array.Array +use import int.ComputerDivision +use import mach.int.Unsigned +use import UInt256 + +exception Ret +type state = StateUnused +)"; +} + +string Why3Translator::toFormalType(Type const& _type) const +{ + if (auto type = dynamic_cast(&_type)) + { + if (!type->isAddress() && !type->isSigned() && type->numBits() == 256) + return "uint256"; + } + else if (auto type = dynamic_cast(&_type)) + if (!type->isByteArray() && type->isDynamicallySized() && type->dataStoredIn(DataLocation::Memory)) + { + string base = toFormalType(*type->baseType()); + if (!base.empty()) + return "array " + base; + } + + return ""; +} + +void Why3Translator::addLine(string const& _line) +{ + newLine(); + add(_line); + newLine(); +} + +void Why3Translator::add(string const& _str) +{ + m_currentLine += _str; +} + +void Why3Translator::newLine() +{ + if (!m_currentLine.empty()) + { + for (size_t i = 0; i < m_indentation; ++i) + m_result.push_back('\t'); + m_result += m_currentLine; + m_result.push_back('\n'); + m_currentLine.clear(); + } +} + +void Why3Translator::unindent() +{ + solAssert(m_indentation > 0, ""); + m_indentation--; +} + +bool Why3Translator::visit(ContractDefinition const& _contract) +{ + if (m_seenContract) + error(_contract, "More than one contract not supported."); + m_seenContract = true; + if (_contract.isLibrary()) + error(_contract, "Libraries not supported."); + + addSourceFromDocStrings(_contract.annotation()); + + return true; +} + +bool Why3Translator::visit(FunctionDefinition const& _function) +{ + if (!_function.isImplemented()) + { + error(_function, "Unimplemented functions not supported."); + return false; + } + if (_function.name().empty()) + { + error(_function, "Fallback functions not supported."); + return false; + } + if (!_function.modifiers().empty()) + { + error(_function, "Modifiers not supported."); + return false; + } + + add("let rec _" + _function.name()); + add(" (state: state)"); + for (auto const& param: _function.parameters()) + { + string paramType = toFormalType(*param->annotation().type); + if (paramType.empty()) + error(*param, "Parameter type not supported."); + if (param->name().empty()) + error(*param, "Anonymous function parameters not supported."); + add(" (arg_" + param->name() + ": " + paramType + ")"); + } + add(":"); + newLine(); + + indent(); + indent(); + string retString = "("; + for (auto const& retParam: _function.returnParameters()) + { + string paramType = toFormalType(*retParam->annotation().type); + if (paramType.empty()) + error(*retParam, "Parameter type not supported."); + if (retString.size() != 1) + retString += ", "; + retString += paramType; + } + addLine(retString + ")"); + unindent(); + + addSourceFromDocStrings(_function.annotation()); + + addLine("="); + + // initialise local variables + for (auto const& variable: _function.parameters()) + addLine("let _" + variable->name() + " = ref arg_" + variable->name() + " in"); + for (auto const& variable: _function.returnParameters()) + { + if (variable->name().empty()) + error(*variable, "Unnamed return variables not yet supported."); + string varType = toFormalType(*variable->annotation().type); + addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in"); + } + for (VariableDeclaration const* variable: _function.localVariables()) + { + if (variable->name().empty()) + error(*variable, "Unnamed variables not yet supported."); + string varType = toFormalType(*variable->annotation().type); + addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in"); + } + addLine("try"); + + _function.body().accept(*this); + addLine("raise Ret"); + + string retVals; + for (auto const& variable: _function.returnParameters()) + { + if (!retVals.empty()) + retVals += ", "; + retVals += "!_" + variable->name(); + } + addLine("with Ret -> (" + retVals + ")"); + newLine(); + unindent(); + addLine("end"); + addLine(""); + return false; +} + +bool Why3Translator::visit(Block const& _node) +{ + addSourceFromDocStrings(_node.annotation()); + addLine("begin"); + indent(); + return true; +} + +bool Why3Translator::visit(IfStatement const& _node) +{ + addSourceFromDocStrings(_node.annotation()); + + add("if "); + _node.condition().accept(*this); + add(" then"); + newLine(); + _node.trueStatement().accept(*this); + if (_node.falseStatement()) + { + addLine("else"); + _node.falseStatement()->accept(*this); + } + return false; +} + +bool Why3Translator::visit(WhileStatement const& _node) +{ + addSourceFromDocStrings(_node.annotation()); + + add("while "); + _node.condition().accept(*this); + add(" do"); + newLine(); + _node.body().accept(*this); + addLine("done;"); + return false; +} + +bool Why3Translator::visit(Return const& _node) +{ + addSourceFromDocStrings(_node.annotation()); + + if (_node.expression()) + { + solAssert(!!_node.annotation().functionReturnParameters, ""); + auto const& params = _node.annotation().functionReturnParameters->parameters(); + if (params.size() != 1) + { + error(_node, "Directly returning tuples not supported. Rather assign to return variable."); + return false; + } + newLine(); + add("begin _" + params.front()->name() + " := "); + _node.expression()->accept(*this); + add("; raise Ret end"); + newLine(); + } + else + addLine("raise Ret;"); + return false; +} + +bool Why3Translator::visit(VariableDeclarationStatement const& _node) +{ + addSourceFromDocStrings(_node.annotation()); + + if (_node.declarations().size() != 1) + { + error(_node, "Multiple variables not supported."); + return false; + } + if (_node.initialValue()) + { + add("_" + _node.declarations().front()->name() + " := "); + _node.initialValue()->accept(*this); + add(";"); + newLine(); + } + return false; +} + +bool Why3Translator::visit(ExpressionStatement const& _node) +{ + addSourceFromDocStrings(_node.annotation()); + return true; +} + +bool Why3Translator::visit(Assignment const& _node) +{ + if (_node.assignmentOperator() != Token::Assign) + error(_node, "Compound assignment not supported."); + + _node.leftHandSide().accept(*this); + add(" := "); + _node.rightHandSide().accept(*this); + + return false; +} + +bool Why3Translator::visit(TupleExpression const& _node) +{ + if (_node.components().size() != 1) + error(_node, "Only tuples with exactly one component supported."); + add("("); + return true; +} + +bool Why3Translator::visit(UnaryOperation const& _unaryOperation) +{ + if (toFormalType(*_unaryOperation.annotation().type).empty()) + error(_unaryOperation, "Type not supported."); + + switch (_unaryOperation.getOperator()) + { + case Token::Not: // ! + add("(not "); + break; + default: + error(_unaryOperation, "Operator not supported."); + break; + } + + _unaryOperation.subExpression().accept(*this); + add(")"); + + return false; +} + +bool Why3Translator::visit(BinaryOperation const& _binaryOperation) +{ + Expression const& leftExpression = _binaryOperation.leftExpression(); + Expression const& rightExpression = _binaryOperation.rightExpression(); + solAssert(!!_binaryOperation.annotation().commonType, ""); + Type const& commonType = *_binaryOperation.annotation().commonType; + Token::Value const c_op = _binaryOperation.getOperator(); + + if (commonType.category() == Type::Category::IntegerConstant) + { + add("(of_int " + toString(commonType.literalValue(nullptr)) + ")"); + return false; + } + static const map optrans({ + {Token::And, " && "}, + {Token::Or, " || "}, + {Token::BitOr, " lor "}, + {Token::BitXor, " lxor "}, + {Token::BitAnd, " land "}, + {Token::Add, " + "}, + {Token::Sub, " - "}, + {Token::Mul, " * "}, + {Token::Div, " / "}, + {Token::Mod, " mod "}, + {Token::Equal, " = "}, + {Token::NotEqual, " <> "}, + {Token::LessThan, " < "}, + {Token::GreaterThan, " > "}, + {Token::LessThanOrEqual, " <= "}, + {Token::GreaterThanOrEqual, " >= "} + }); + if (!optrans.count(c_op)) + error(_binaryOperation, "Operator not supported."); + + add("("); + leftExpression.accept(*this); + add(optrans.at(c_op)); + rightExpression.accept(*this); + add(")"); + + return false; +} + +bool Why3Translator::visit(FunctionCall const& _node) +{ + if (_node.annotation().isTypeConversion || _node.annotation().isStructConstructorCall) + { + error(_node, "Only ordinary function calls supported."); + return true; + } + FunctionType const& function = dynamic_cast(*_node.expression().annotation().type); + if (function.location() != FunctionType::Location::Internal) + { + 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(" StateUnused"); + for (auto const& arg: _node.arguments()) + { + add(" "); + arg->accept(*this); + } + add(")"); + return false; +} + +bool Why3Translator::visit(MemberAccess const& _node) +{ + if ( + _node.expression().annotation().type->category() == Type::Category::Array && + _node.memberName() == "length" && + !_node.annotation().lValueRequested + ) + { + add("(of_int "); + _node.expression().accept(*this); + add(".length"); + add(")"); + } + else + error(_node, "Only read-only length access for arrays supported."); + return false; +} + +bool Why3Translator::visit(IndexAccess const& _node) +{ + auto baseType = dynamic_cast(_node.baseExpression().annotation().type.get()); + if (!baseType) + { + error(_node, "Index access only supported for arrays."); + return true; + } + if (_node.annotation().lValueRequested) + { + error(_node, "Assignment to array elements not supported."); + return true; + } + add("("); + _node.baseExpression().accept(*this); + add("[to_int "); + _node.indexExpression()->accept(*this); + add("]"); + add(")"); + + return false; +} + +bool Why3Translator::visit(Identifier const& _identifier) +{ + Declaration const* declaration = _identifier.annotation().referencedDeclaration; + if (FunctionDefinition const* functionDef = dynamic_cast(declaration)) + add("_" + functionDef->name()); + else if (auto variable = dynamic_cast(declaration)) + { + if (_identifier.annotation().lValueRequested) + add("_" + variable->name()); + else + add("!_" + variable->name()); + } + else + error(_identifier, "Not supported."); + return false; +} + +bool Why3Translator::visit(Literal const& _literal) +{ + TypePointer type = _literal.annotation().type; + switch (type->category()) + { + case Type::Category::Bool: + if (type->literalValue(&_literal) == 0) + add("false"); + else + add("true"); + break; + case Type::Category::IntegerConstant: + add("(of_int " + toString(type->literalValue(&_literal)) + ")"); + break; + default: + error(_literal, "Not supported."); + } + return false; +} + +void Why3Translator::addSourceFromDocStrings(const DocumentedAnnotation& _annotation) +{ + auto why3Range = _annotation.docTags.equal_range("why3"); + for (auto i = why3Range.first; i != why3Range.second; ++i) + addLine(i->second.content); +} diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h new file mode 100644 index 00000000..21ead977 --- /dev/null +++ b/libsolidity/formal/Why3Translator.h @@ -0,0 +1,115 @@ +/* + This file is part of cpp-ethereum. + + cpp-ethereum is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + cpp-ethereum is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with cpp-ethereum. If not, see . +*/ +/** + * @author Christian + * @date 2015 + * Component that translates Solidity code into the why3 programming language. + */ + +#pragma once + +#include +#include +#include + +namespace dev +{ +namespace solidity +{ + +class SourceUnit; + +/** + * Simple translator from Solidity to Why3. + * + * @todo detect side effects in sub-expressions and limit them to one per statement. + * @todo `x = y = z` + * @todo implicit and explicit type conversion + */ +class Why3Translator: private ASTConstVisitor +{ +public: + Why3Translator(ErrorList& _errors): m_errors(_errors) {} + + /// Appends formalisation of the given source unit to the output. + /// @returns false on error. + bool process(SourceUnit const& _source); + + std::string translation() const { return m_result; } + +private: + /// Returns an error. + void error(ASTNode const& _node, std::string const& _description); + /// Reports a fatal error and throws. + void fatalError(ASTNode const& _node, std::string const& _description); + + /// Appends imports and constants use throughout the formal code. + void appendPreface(); + + /// @returns a string representation of the corresponding formal type or the empty string + /// if the type is not supported. + std::string toFormalType(Type const& _type) const; + + void indent() { m_indentation++; } + void unindent(); + void addLine(std::string const& _line); + void add(std::string const& _str); + void newLine(); + + virtual bool visit(SourceUnit const&) override { return true; } + virtual bool visit(ContractDefinition const& _contract) override; + virtual bool visit(FunctionDefinition const& _function) override; + virtual bool visit(Block const&) override; + virtual void endVisit(Block const&) override { unindent(); addLine("end;"); } + virtual bool visit(IfStatement const& _node) override; + virtual bool visit(WhileStatement const& _node) override; + virtual bool visit(Return const& _node) override; + virtual bool visit(VariableDeclarationStatement const& _node) override; + virtual bool visit(ExpressionStatement const&) override; + virtual void endVisit(ExpressionStatement const&) override { add(";"); newLine(); } + virtual bool visit(Assignment const& _node) override; + virtual bool visit(TupleExpression const& _node) override; + virtual void endVisit(TupleExpression const&) override { add(")"); } + virtual bool visit(UnaryOperation const& _node) override; + virtual bool visit(BinaryOperation const& _node) override; + virtual bool visit(FunctionCall const& _node) override; + virtual bool visit(MemberAccess const& _node) override; + virtual bool visit(IndexAccess const& _node) override; + virtual bool visit(Identifier const& _node) override; + virtual bool visit(Literal const& _node) override; + + virtual bool visitNode(ASTNode const& _node) override + { + error(_node, "Code not supported for formal verification."); + return false; + } + + void addSourceFromDocStrings(DocumentedAnnotation const& _annotation); + + size_t m_indentation = 0; + std::string m_currentLine; + /// True if we have already seen a contract. For now, only a single contract + /// is supported. + bool m_seenContract = false; + bool m_errorOccured = false; + std::string m_result; + ErrorList& m_errors; +}; + + +} +} diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 6b55b408..18eec0a2 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -32,6 +32,7 @@ #include #include #include +#include #include @@ -205,6 +206,18 @@ void CompilerStack::link(const std::map& _libraries) } } +bool CompilerStack::prepareFormalAnalysis() +{ + Why3Translator translator(m_errors); + for (Source const* source: m_sourceOrder) + if (!translator.process(*source->ast)) + return false; + + m_formalTranslation = translator.translation(); + + return true; +} + eth::AssemblyItems const* CompilerStack::assemblyItems(string const& _contractName) const { Contract const& currentContract = contract(_contractName); diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index ac71da2e..0473d58b 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -108,6 +108,11 @@ public: /// Inserts the given addresses into the linker objects of all compiled contracts. void link(std::map const& _libraries); + /// Tries to translate all source files into a language suitable for formal analysis. + /// @returns false on error. + bool prepareFormalAnalysis(); + std::string const& formalTranslation() const { return m_formalTranslation; } + /// @returns the assembled object for a contract. eth::LinkerObject const& object(std::string const& _contractName = "") const; /// @returns the runtime object for the contract. @@ -167,7 +172,6 @@ public: /// @returns the list of errors that occured during parsing and type checking. ErrorList const& errors() const { return m_errors; } - private: /** * Information pertaining to one source unit, filled gradually during parsing and compilation. @@ -211,6 +215,7 @@ private: std::shared_ptr m_globalContext; std::vector m_sourceOrder; std::map m_contracts; + std::string m_formalTranslation; ErrorList m_errors; }; diff --git a/libsolidity/interface/Exceptions.cpp b/libsolidity/interface/Exceptions.cpp index 2e79ab39..84d4d108 100644 --- a/libsolidity/interface/Exceptions.cpp +++ b/libsolidity/interface/Exceptions.cpp @@ -30,23 +30,26 @@ Error::Error(Type _type): m_type(_type) { switch(m_type) { - case Type::DeclarationError: - m_typeName = "Declaration Error"; - break; - case Type::DocstringParsingError: - m_typeName = "Docstring Parsing Error"; - break; - case Type::ParserError: - m_typeName = "Parser Error"; - break; - case Type::TypeError: - m_typeName = "Type Error"; - break; - case Type::Warning: - m_typeName = "Warning"; - break; - default: - solAssert(false, ""); - break; + case Type::DeclarationError: + m_typeName = "Declaration Error"; + break; + case Type::DocstringParsingError: + m_typeName = "Docstring Parsing Error"; + break; + case Type::ParserError: + m_typeName = "Parser Error"; + break; + case Type::TypeError: + m_typeName = "Type Error"; + break; + case Type::FormalError: + m_typeName = "Formal Error"; + break; + case Type::Warning: + m_typeName = "Warning"; + break; + default: + solAssert(false, ""); + break; } } diff --git a/libsolidity/interface/Exceptions.h b/libsolidity/interface/Exceptions.h index cda6b97e..830ec286 100644 --- a/libsolidity/interface/Exceptions.h +++ b/libsolidity/interface/Exceptions.h @@ -47,6 +47,7 @@ public: DocstringParsingError, ParserError, TypeError, + FormalError, Warning }; diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index fcea5bf9..b4121574 100644 --- a/solc/CommandLineInterface.cpp +++ b/solc/CommandLineInterface.cpp @@ -45,6 +45,7 @@ #include #include #include +#include using namespace std; namespace po = boost::program_options; @@ -96,28 +97,30 @@ static void version() exit(0); } -static inline bool humanTargetedStdout(po::variables_map const& _args, string const& _name) -{ - return _args.count(_name) && !(_args.count("output-dir")); -} - static bool needsHumanTargetedStdout(po::variables_map const& _args) { - - return - _args.count(g_argGas) || - humanTargetedStdout(_args, g_argAbiStr) || - humanTargetedStdout(_args, g_argSolInterfaceStr) || - humanTargetedStdout(_args, g_argSignatureHashes) || - humanTargetedStdout(_args, g_argNatspecUserStr) || - humanTargetedStdout(_args, g_argAstJson) || - humanTargetedStdout(_args, g_argNatspecDevStr) || - humanTargetedStdout(_args, g_argAsmStr) || - humanTargetedStdout(_args, g_argAsmJsonStr) || - humanTargetedStdout(_args, g_argOpcodesStr) || - humanTargetedStdout(_args, g_argBinaryStr) || - humanTargetedStdout(_args, g_argRuntimeBinaryStr) || - humanTargetedStdout(_args, g_argCloneBinaryStr); + if (_args.count(g_argGas)) + return true; + if (_args.count("output-dir")) + return false; + for (string const& arg: { + g_argAbiStr, + g_argSolInterfaceStr, + g_argSignatureHashes, + g_argNatspecUserStr, + g_argAstJson, + g_argNatspecDevStr, + g_argAsmStr, + g_argAsmJsonStr, + g_argOpcodesStr, + g_argBinaryStr, + g_argRuntimeBinaryStr, + g_argCloneBinaryStr, + string("formal") + }) + if (_args.count(arg)) + return true; + return false; } void CommandLineInterface::handleBinary(string const& _contract) @@ -164,7 +167,6 @@ void CommandLineInterface::handleOpcode(string const& _contract) cout << eth::disassemble(m_compiler->object(_contract).bytecode); cout << endl; } - } void CommandLineInterface::handleBytecode(string const& _contract) @@ -284,6 +286,17 @@ void CommandLineInterface::handleGasEstimation(string const& _contract) } } +void CommandLineInterface::handleFormal() +{ + if (!m_args.count("formal")) + return; + + if (m_args.count("output-dir")) + createFile("solidity.mlw", m_compiler->formalTranslation()); + else + cout << "Formal version:" << endl << m_compiler->formalTranslation() << endl; +} + bool CommandLineInterface::parseLibraryOption(string const& _input) { namespace fs = boost::filesystem; @@ -391,7 +404,8 @@ Allowed options)", (g_argSolInterfaceStr.c_str(), "Solidity interface of the contracts.") (g_argSignatureHashes.c_str(), "Function signature hashes of the contracts.") (g_argNatspecUserStr.c_str(), "Natspec user documentation of all contracts.") - (g_argNatspecDevStr.c_str(), "Natspec developer documentation of all contracts."); + (g_argNatspecDevStr.c_str(), "Natspec developer documentation of all contracts.") + ("formal", "Translated source suitable for formal analysis."); desc.add(outputComponents); po::options_description allOptions = desc; @@ -492,15 +506,22 @@ bool CommandLineInterface::processInput() bool optimize = m_args.count("optimize") > 0; unsigned runs = m_args["optimize-runs"].as(); bool successful = m_compiler->compile(optimize, runs); + if (successful) + m_compiler->link(m_libraries); + + if (successful && m_args.count("formal")) + if (!m_compiler->prepareFormalAnalysis()) + successful = false; + for (auto const& error: m_compiler->errors()) SourceReferenceFormatter::printExceptionInformation( cerr, *error, (error->type() == Error::Type::Warning) ? "Warning" : "Error", *m_compiler ); + if (!successful) return false; - m_compiler->link(m_libraries); } catch (CompilerError const& _exception) { @@ -755,6 +776,8 @@ void CommandLineInterface::outputCompilationResults() handleMeta(DocumentationType::NatspecDev, contract); handleMeta(DocumentationType::NatspecUser, contract); } // end of contracts iteration + + handleFormal(); } } diff --git a/solc/CommandLineInterface.h b/solc/CommandLineInterface.h index 1cde2acb..7c7aa4b4 100644 --- a/solc/CommandLineInterface.h +++ b/solc/CommandLineInterface.h @@ -57,9 +57,9 @@ private: void handleOpcode(std::string const& _contract); void handleBytecode(std::string const& _contract); void handleSignatureHashes(std::string const& _contract); - void handleMeta(DocumentationType _type, - std::string const& _contract); + void handleMeta(DocumentationType _type, std::string const& _contract); void handleGasEstimation(std::string const& _contract); + void handleFormal(); /// Tries to read from the file @a _input or interprets _input literally if that fails. /// It then tries to parse the contents and appends to m_libraries. -- cgit v1.2.3 From 56f5d5885090a03ea9223f2210e70b6c78a1cb75 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 27 Oct 2015 17:45:58 +0100 Subject: Rename error type. --- libsolidity/formal/Why3Translator.cpp | 2 +- libsolidity/interface/Exceptions.cpp | 4 ++-- libsolidity/interface/Exceptions.h | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index 0d3d1586..944b1e7b 100644 --- a/libsolidity/formal/Why3Translator.cpp +++ b/libsolidity/formal/Why3Translator.cpp @@ -46,7 +46,7 @@ bool Why3Translator::process(SourceUnit const& _source) void Why3Translator::error(ASTNode const& _node, string const& _description) { - auto err = make_shared(Error::Type::FormalError); + auto err = make_shared(Error::Type::Why3TranslatorError); *err << errinfo_sourceLocation(_node.location()) << errinfo_comment(_description); diff --git a/libsolidity/interface/Exceptions.cpp b/libsolidity/interface/Exceptions.cpp index 84d4d108..465c3d2f 100644 --- a/libsolidity/interface/Exceptions.cpp +++ b/libsolidity/interface/Exceptions.cpp @@ -42,8 +42,8 @@ Error::Error(Type _type): m_type(_type) case Type::TypeError: m_typeName = "Type Error"; break; - case Type::FormalError: - m_typeName = "Formal Error"; + case Type::Why3TranslatorError: + m_typeName = "Why3 Translator Error"; break; case Type::Warning: m_typeName = "Warning"; diff --git a/libsolidity/interface/Exceptions.h b/libsolidity/interface/Exceptions.h index 830ec286..14be3c3d 100644 --- a/libsolidity/interface/Exceptions.h +++ b/libsolidity/interface/Exceptions.h @@ -47,7 +47,7 @@ public: DocstringParsingError, ParserError, TypeError, - FormalError, + Why3TranslatorError, Warning }; -- cgit v1.2.3