From 555dc4f46fae9da72aaff70059686aa34172910b Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Tue, 30 May 2017 09:17:02 +0100 Subject: Remove Why3 generator --- libsolidity/formal/Why3Translator.h | 147 ------------------------------------ 1 file changed, 147 deletions(-) delete mode 100644 libsolidity/formal/Why3Translator.h (limited to 'libsolidity/formal/Why3Translator.h') diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h deleted file mode 100644 index b48317be..00000000 --- a/libsolidity/formal/Why3Translator.h +++ /dev/null @@ -1,147 +0,0 @@ -/* - This file is part of solidity. - - solidity 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. - - solidity 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 solidity. 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. #1043 - * @todo `x = y = z` - * @todo implicit and explicit type conversion - */ -class Why3Translator: private ASTConstVisitor -{ -public: - Why3Translator(ErrorReporter& _errorReporter): m_lines(std::vector{{std::string(), 0}}), m_errorReporter(_errorReporter) {} - - /// Appends formalisation of the given source unit to the output. - /// @returns false on error. - bool process(SourceUnit const& _source); - - std::string translation() const; - -private: - /// Appends imports and constants use throughout the formal code. - void appendPreface(); - - /// @returns a string representation of the corresponding formal type or throws NoFormalType exception. - std::string toFormalType(Type const& _type) const; - using errinfo_noFormalTypeFrom = boost::error_info; - struct NoFormalType: virtual Exception {}; - - void error(ASTNode const& _source, std::string const& _description); - void fatalError(ASTNode const& _source, std::string const& _description); - - void indent() { newLine(); m_lines.back().indentation++; } - void unindent(); - void addLine(std::string const& _line); - void add(std::string const& _str); - void newLine(); - void appendSemicolon(); - - virtual bool visit(SourceUnit const&) override { return true; } - 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; - virtual bool visit(Return const& _node) override; - virtual bool visit(Throw const& _node) override; - virtual bool visit(VariableDeclarationStatement const& _node) override; - virtual bool visit(ExpressionStatement const&) override; - 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 visit(PragmaDirective const& _node) override; - - virtual bool visitNode(ASTNode const& _node) override - { - m_errorReporter.why3TranslatorError(_node, "Code not supported for formal verification."); - return false; - } - - 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; - - /// @returns a string representing an expression that is a copy of this.storage - std::string copyOfStorage() const; - - /// Visits the given 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); - - /// True if we have already seen a contract. For now, only a single contract - /// is supported. - bool m_seenContract = false; - bool m_errorOccured = false; - - /// Metadata relating to the current contract - struct ContractMetadata - { - ContractDefinition const* contract = nullptr; - std::vector stateVariables; - - void reset() { contract = nullptr; stateVariables.clear(); } - }; - - ContractMetadata m_currentContract; - bool m_currentLValueIsRef = false; - std::map m_localVariables; - - struct Line - { - std::string contents; - unsigned indentation; - }; - std::vector m_lines; - ErrorReporter& m_errorReporter; -}; - -} -} -- cgit v1.2.3