diff options
| -rw-r--r-- | libsolidity/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | libsolidity/formal/Why3Translator.cpp | 525 | ||||
| -rw-r--r-- | libsolidity/formal/Why3Translator.h | 115 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.cpp | 13 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.h | 7 | ||||
| -rw-r--r-- | libsolidity/interface/Exceptions.cpp | 39 | ||||
| -rw-r--r-- | libsolidity/interface/Exceptions.h | 1 | ||||
| -rw-r--r-- | solc/CommandLineInterface.cpp | 69 | ||||
| -rw-r--r-- | solc/CommandLineInterface.h | 4 |
9 files changed, 730 insertions, 44 deletions
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 <http://www.gnu.org/licenses/>. +*/ +/** + * @author Christian <c@ethdev.com> + * @date 2015 + * Component that translates Solidity code into the why3 programming language. + */ + +#include <libsolidity/formal/Why3Translator.h> + +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>(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<IntegerType const*>(&_type)) + { + if (!type->isAddress() && !type->isSigned() && type->numBits() == 256) + return "uint256"; + } + else if (auto type = dynamic_cast<ArrayType const*>(&_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<Token::Value, char const*> 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<FunctionType const&>(*_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<ArrayType const*>(_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<FunctionDefinition const*>(declaration)) + add("_" + functionDef->name()); + else if (auto variable = dynamic_cast<VariableDeclaration const*>(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 <http://www.gnu.org/licenses/>. +*/ +/** + * @author Christian <c@ethdev.com> + * @date 2015 + * Component that translates Solidity code into the why3 programming language. + */ + +#pragma once + +#include <libsolidity/ast/ASTVisitor.h> +#include <libsolidity/interface/Exceptions.h> +#include <string> + +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 <libsolidity/codegen/Compiler.h> #include <libsolidity/interface/CompilerStack.h> #include <libsolidity/interface/InterfaceHandler.h> +#include <libsolidity/formal/Why3Translator.h> #include <libdevcore/SHA3.h> @@ -205,6 +206,18 @@ void CompilerStack::link(const std::map<string, h160>& _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<std::string, h160> 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<GlobalContext> m_globalContext; std::vector<Source const*> m_sourceOrder; std::map<std::string const, Contract> 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 <libsolidity/interface/CompilerStack.h> #include <libsolidity/interface/SourceReferenceFormatter.h> #include <libsolidity/interface/GasEstimator.h> +#include <libsolidity/formal/Why3Translator.h> 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<unsigned>(); 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. |