diff options
| -rw-r--r-- | Changelog.md | 1 | ||||
| -rw-r--r-- | libsolidity/formal/Why3Translator.cpp | 898 | ||||
| -rw-r--r-- | libsolidity/formal/Why3Translator.h | 147 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.cpp | 15 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.h | 7 | ||||
| -rw-r--r-- | solc/CommandLineInterface.cpp | 19 | ||||
| -rw-r--r-- | test/fuzzer.cpp | 1 |
7 files changed, 3 insertions, 1085 deletions
diff --git a/Changelog.md b/Changelog.md index ee952a37..87c26176 100644 --- a/Changelog.md +++ b/Changelog.md @@ -12,6 +12,7 @@ Features: * Inline Assembly: ``for`` and ``switch`` statements. * Inline Assembly: function definitions and function calls. * Code Generator: Added the Whiskers template system. + * Remove obsolete Why3 output. Bugfixes: * Type Checker: Fix address literals not being treated as compile-time constants. diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp deleted file mode 100644 index fecab2de..00000000 --- a/libsolidity/formal/Why3Translator.cpp +++ /dev/null @@ -1,898 +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 <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> -#include <boost/algorithm/string/predicate.hpp> - -using namespace std; -using namespace dev; -using namespace dev::solidity; - -bool Why3Translator::process(SourceUnit const& _source) -{ - try - { - if (m_lines.size() != 1 || !m_lines.back().contents.empty()) - fatalError(_source, string("Multiple source units not yet supported")); - appendPreface(); - _source.accept(*this); - } - catch (NoFormalType&) - { - solAssert(false, "There is a call to toFormalType() that does not catch NoFormalType exceptions."); - } - catch (FatalError& /*_e*/) - { - solAssert(m_errorOccured, ""); - } - return !m_errorOccured; -} - -string Why3Translator::translation() const -{ - string result; - for (auto const& line: m_lines) - result += string(line.indentation, '\t') + line.contents + "\n"; - return result; -} - -string Why3Translator::toFormalType(Type const& _type) const -{ - if (_type.category() == Type::Category::Bool) - return "bool"; - else 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)) - { - // Not catching NoFormalType exception. Let the caller deal with it. - string base = toFormalType(*type->baseType()); - return "array " + base; - } - } - else if (auto mappingType = dynamic_cast<MappingType const*>(&_type)) - { - solAssert(mappingType->keyType(), "A mappingType misses a keyType."); - if (dynamic_cast<IntegerType const*>(&*mappingType->keyType())) - { - //@TODO Use the information from the key type and specify the length of the array as an invariant. - // Also the constructor need to specify the length of the array. - solAssert(mappingType->valueType(), "A mappingType misses a valueType."); - // Not catching NoFormalType exception. Let the caller deal with it. - string valueTypeFormal = toFormalType(*mappingType->valueType()); - return "array " + valueTypeFormal; - } - } - - BOOST_THROW_EXCEPTION(NoFormalType() - << errinfo_noFormalTypeFrom(_type.toString(true))); -} - -void Why3Translator::addLine(string const& _line) -{ - newLine(); - add(_line); - newLine(); -} - -void Why3Translator::add(string const& _str) -{ - m_lines.back().contents += _str; -} - -void Why3Translator::newLine() -{ - if (!m_lines.back().contents.empty()) - m_lines.push_back({"", m_lines.back().indentation}); -} - -void Why3Translator::unindent() -{ - newLine(); - solAssert(m_lines.back().indentation > 0, ""); - m_lines.back().indentation--; -} - -bool Why3Translator::visit(ContractDefinition const& _contract) -{ - if (m_seenContract) - error(_contract, "More than one contract not supported."); - m_seenContract = true; - m_currentContract.contract = &_contract; - if (_contract.isLibrary()) - error(_contract, "Libraries not supported."); - - addLine("module Contract_" + _contract.name()); - indent(); - addLine("use import int.Int"); - addLine("use import ref.Ref"); - addLine("use import map.Map"); - addLine("use import array.Array"); - addLine("use import int.ComputerDivision"); - addLine("use import mach.int.Unsigned"); - addLine("use import UInt256"); - addLine("exception Revert"); - addLine("exception Return"); - - if (_contract.stateVariables().empty()) - addLine("type state = ()"); - else - { - addLine("type state = {"); - indent(); - m_currentContract.stateVariables = _contract.stateVariables(); - for (VariableDeclaration const* variable: m_currentContract.stateVariables) - { - string varType; - try - { - varType = toFormalType(*variable->annotation().type); - } - catch (NoFormalType &err) - { - string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err); - string typeName = typeNamePtr ? " \"" + *typeNamePtr + "\"" : ""; - fatalError(*variable, "Type" + typeName + " not supported for state variable."); - } - addLine("mutable _" + variable->name() + ": " + varType); - } - unindent(); - addLine("}"); - } - - addLine("type account = {"); - indent(); - addLine("mutable balance: uint256;"); - addLine("storage: state"); - unindent(); - addLine("}"); - - addLine("val external_call (this: account): bool"); - indent(); - addLine("ensures { result = false -> this = (old this) }"); - addLine("writes { this }"); - addSourceFromDocStrings(m_currentContract.contract->annotation()); - unindent(); - - if (!_contract.baseContracts().empty()) - error(*_contract.baseContracts().front(), "Inheritance not supported."); - if (!_contract.definedStructs().empty()) - error(*_contract.definedStructs().front(), "User-defined types not supported."); - if (!_contract.definedEnums().empty()) - error(*_contract.definedEnums().front(), "User-defined types not supported."); - if (!_contract.events().empty()) - error(*_contract.events().front(), "Events not supported."); - if (!_contract.functionModifiers().empty()) - error(*_contract.functionModifiers().front(), "Modifiers not supported."); - - ASTNode::listAccept(_contract.definedFunctions(), *this); - - return false; -} - -void Why3Translator::endVisit(ContractDefinition const&) -{ - m_currentContract.reset(); - unindent(); - addLine("end"); -} - -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; - } - - 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(" (this: account)"); - for (auto const& param: _function.parameters()) - { - string paramType; - try - { - paramType = toFormalType(*param->annotation().type); - } - catch (NoFormalType &err) - { - string const* typeName = boost::get_error_info<errinfo_noFormalTypeFrom>(err); - error(*param, "Parameter type \"" + (typeName ? *typeName : "") + "\" not supported."); - } - if (param->name().empty()) - error(*param, "Anonymous function parameters not supported."); - add(" (arg_" + param->name() + ": " + paramType + ")"); - } - add(":"); - - indent(); - indent(); - string retString = "("; - for (auto const& retParam: _function.returnParameters()) - { - string paramType; - try - { - paramType = toFormalType(*retParam->annotation().type); - } - catch (NoFormalType &err) - { - string const* typeName = boost::get_error_info<errinfo_noFormalTypeFrom>(err); - error(*retParam, "Parameter type " + (typeName ? *typeName : "") + " not supported."); - } - if (retString.size() != 1) - retString += ", "; - retString += paramType; - } - add(retString + ")"); - unindent(); - - addSourceFromDocStrings(_function.annotation()); - if (!m_currentContract.contract) - error(_function, "Only functions inside contracts allowed."); - addSourceFromDocStrings(m_currentContract.contract->annotation()); - - if (_function.isDeclaredConst()) - addLine("ensures { (old this) = this }"); - else - addLine("writes { this }"); - - addLine("="); - - // store the prestate in the case we need to revert - addLine("let prestate = {balance = this.balance; storage = " + copyOfStorage() + "} in "); - - // 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; - try - { - varType = toFormalType(*variable->annotation().type); - } - catch (NoFormalType &err) - { - string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err); - error(*variable, "Type " + (typeNamePtr ? *typeNamePtr : "") + "in return parameter not yet supported."); - } - 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; - try - { - varType = toFormalType(*variable->annotation().type); - } - catch (NoFormalType &err) - { - string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err); - error(*variable, "Type " + (typeNamePtr ? *typeNamePtr : "") + "in variable declaration not yet supported."); - } - addLine("let _" + variable->name() + ": ref " + varType + " = ref (of_int 0) in"); - } - addLine("try"); - - _function.body().accept(*this); - add(";"); - addLine("raise Return"); - - string retVals; - for (auto const& variable: _function.returnParameters()) - { - if (!retVals.empty()) - retVals += ", "; - retVals += "!_" + variable->name(); - } - addLine("with Return -> (" + retVals + ") |"); - string reversion = " Revert -> this.balance <- prestate.balance; "; - for (auto const* variable: m_currentContract.stateVariables) - reversion += "this.storage._" + variable->name() + " <- prestate.storage._" + variable->name() + "; "; - //@TODO in case of reversion the return values are wrong - we need to change the - // return type to include a bool to signify if an exception was thrown. - reversion += "(" + retVals + ")"; - addLine(reversion); - unindent(); - addLine("end"); - addLine(""); - return false; -} - -void Why3Translator::endVisit(FunctionDefinition const&) -{ - m_localVariables.clear(); -} - -bool Why3Translator::visit(Block const& _node) -{ - addSourceFromDocStrings(_node.annotation()); - add("begin"); - indent(); - for (size_t i = 0; i < _node.statements().size(); ++i) - { - _node.statements()[i]->accept(*this); - if (i != _node.statements().size() - 1) - { - auto it = m_lines.end() - 1; - while (it != m_lines.begin() && it->contents.empty()) - --it; - if (!boost::algorithm::ends_with(it->contents, "begin")) - it->contents += ";"; - } - newLine(); - } - unindent(); - add("end"); - return false; -} - -bool Why3Translator::visit(IfStatement const& _node) -{ - addSourceFromDocStrings(_node.annotation()); - - add("if "); - _node.condition().accept(*this); - add(" then"); - visitIndentedUnlessBlock(_node.trueStatement()); - if (_node.falseStatement()) - { - newLine(); - add("else"); - visitIndentedUnlessBlock(*_node.falseStatement()); - } - return false; -} - -bool Why3Translator::visit(WhileStatement const& _node) -{ - addSourceFromDocStrings(_node.annotation()); - - // Why3 does not appear to support do-while loops, - // so we will simulate them by performing a while - // loop with the body prepended once. - - if (_node.isDoWhile()) - { - visitIndentedUnlessBlock(_node.body()); - newLine(); - } - - add("while "); - _node.condition().accept(*this); - newLine(); - add("do"); - visitIndentedUnlessBlock(_node.body()); - add("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; - } - add("begin _" + params.front()->name() + " := "); - _node.expression()->accept(*this); - add("; raise Return end"); - } - else - add("raise Return"); - return false; -} - -bool Why3Translator::visit(Throw const& _node) -{ - addSourceFromDocStrings(_node.annotation()); - add("raise Revert"); - 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); - } - 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(m_currentLValueIsRef ? " := " : " <- "); - _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) -{ - try - { - toFormalType(*_unaryOperation.annotation().type); - } - catch (NoFormalType &err) - { - string const* typeNamePtr = boost::get_error_info<errinfo_noFormalTypeFrom>(err); - error(_unaryOperation, "Type \"" + (typeNamePtr ? *typeNamePtr : "") + "\" supported in unary operation."); - } - - 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::RationalNumber) - { - auto const& constantNumber = dynamic_cast<RationalNumberType const&>(commonType); - if (constantNumber.isFractional()) - error(_binaryOperation, "Fractional numbers not supported."); - else - 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."); - return true; - } - - add("("); - leftExpression.accept(*this); - add(optrans.at(c_op)); - rightExpression.accept(*this); - add(")"); - - return false; -} - -bool Why3Translator::visit(FunctionCall const& _node) -{ - if (_node.annotation().kind == FunctionCallKind::TypeConversion || _node.annotation().kind == FunctionCallKind::StructConstructorCall) - { - error(_node, "Only ordinary function calls supported."); - return true; - } - FunctionType const& function = dynamic_cast<FunctionType const&>(*_node.expression().annotation().type); - switch (function.kind()) - { - case FunctionType::Kind::AddMod: - case FunctionType::Kind::MulMod: - { - //@todo require that third parameter is not zero - add("(of_int (mod (Int.("); - add(function.kind() == FunctionType::Kind::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::Kind::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; - } - case FunctionType::Kind::Bare: - { - if (!_node.arguments().empty()) - { - error(_node, "Function calls with named arguments not supported."); - return true; - } - - add("("); - indent(); - add("let amount = 0 in "); - _node.expression().accept(*this); - addLine("if amount <= this.balance then"); - indent(); - addLine("let balance_precall = this.balance in"); - addLine("begin"); - indent(); - addLine("this.balance <- this.balance - amount;"); - addLine("if not (external_call this) then begin this.balance = balance_precall; false end else true"); - unindent(); - addLine("end"); - unindent(); - addLine("else false"); - - unindent(); - add(")"); - return false; - } - case FunctionType::Kind::SetValue: - { - add("let amount = "); - solAssert(_node.arguments().size() == 1, ""); - _node.arguments()[0]->accept(*this); - add(" in "); - return false; - } - default: - error(_node, "Only internal function calls supported."); - return true; - } -} - -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 if ( - _node.memberName() == "call" && - *_node.expression().annotation().type == IntegerType(160, IntegerType::Modifier::Address) - ) - { - // Do nothing, do not even visit the address because this will be an external call - //@TODO ensure that the expression itself does not have side-effects - return false; - } - else - error(_node, "Member access: Only call and array length 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)) - { - bool isStateVar = isStateVariable(variable); - bool lvalue = _identifier.annotation().lValueRequested; - if (isStateVar) - add("this.storage."); - else if (!lvalue) - add("!("); - add("_" + variable->name()); - if (!isStateVar && !lvalue) - add(")"); - m_currentLValueIsRef = !isStateVar; - } - 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::RationalNumber: - { - auto const& constantNumber = dynamic_cast<RationalNumberType const&>(*type); - if (constantNumber.isFractional()) - error(_literal, "Fractional numbers not supported."); - else - add("(of_int " + toString(type->literalValue(&_literal)) + ")"); - break; - } - default: - error(_literal, "Not supported."); - } - return false; -} - -bool Why3Translator::visit(PragmaDirective const& _pragma) -{ - if (_pragma.tokens().empty()) - error(_pragma, "Not supported"); - else if (_pragma.literals().empty()) - error(_pragma, "Not supported"); - else if (_pragma.literals()[0] != "solidity") - error(_pragma, "Not supported"); - else if (_pragma.tokens()[0] != Token::Identifier) - error(_pragma, "A literal 'solidity' is not an identifier. Strange"); - - return false; -} - -bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const -{ - return contains(m_currentContract.stateVariables, _var); -} - -bool Why3Translator::isStateVariable(string const& _name) const -{ - for (auto const& var: m_currentContract.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); -} - -string Why3Translator::copyOfStorage() const -{ - if (m_currentContract.stateVariables.empty()) - return "()"; - string ret = "{"; - bool first = true; - for (auto const* variable: m_currentContract.stateVariables) - { - if (first) - first = false; - else - ret += "; "; - ret += "_" + variable->name() + " = this.storage._" + variable->name(); - } - return ret + "}"; -} - -void Why3Translator::visitIndentedUnlessBlock(Statement const& _statement) -{ - bool isBlock = !!dynamic_cast<Block const*>(&_statement); - if (isBlock) - newLine(); - else - indent(); - _statement.accept(*this); - if (isBlock) - newLine(); - else - unindent(); -} - -void Why3Translator::addSourceFromDocStrings(DocumentedAnnotation const& _annotation) -{ - auto why3Range = _annotation.docTags.equal_range("why3"); - for (auto i = why3Range.first; i != why3Range.second; ++i) - 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 += "(!_" + varName + ")"; - else if (isStateVariable(varName)) - ret += "(this.storage._" + varName + ")"; - //@todo return variables - else - ret.append(hash, hashEnd); - - pos = hashEnd; - } - return ret; -} - -void Why3Translator::appendPreface() -{ - m_lines.push_back(Line{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 Address - use import mach.int.Unsigned - type address - constant max_address: int = 0xffffffffffffffffffffffffffffffffffffffff (* 160 bit = 40 f's *) - clone export mach.int.Unsigned with - type t = address, - constant max = max_address -end - )", 0}); -} - -void Why3Translator::error(ASTNode const& _source, std::string const& _description) -{ - m_errorOccured = true; - m_errorReporter.why3TranslatorError(_source, _description); -} -void Why3Translator::fatalError(ASTNode const& _source, std::string const& _description) -{ - m_errorOccured = true; - m_errorReporter.fatalWhy3TranslatorError(_source, _description); -} - 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 <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/ErrorReporter.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. #1043 - * @todo `x = y = z` - * @todo implicit and explicit type conversion - */ -class Why3Translator: private ASTConstVisitor -{ -public: - Why3Translator(ErrorReporter& _errorReporter): m_lines(std::vector<Line>{{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 tag_noFormalTypeFrom, std::string /* name of the type that cannot be translated */ >; - 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<VariableDeclaration const*> stateVariables; - - void reset() { contract = nullptr; stateVariables.clear(); } - }; - - ContractMetadata m_currentContract; - bool m_currentLValueIsRef = false; - std::map<std::string, VariableDeclaration const*> m_localVariables; - - struct Line - { - std::string contents; - unsigned indentation; - }; - std::vector<Line> m_lines; - ErrorReporter& m_errorReporter; -}; - -} -} diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 8be2c8dd..e2507821 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -40,7 +40,6 @@ #include <libsolidity/interface/ABI.h> #include <libsolidity/interface/Natspec.h> #include <libsolidity/interface/GasEstimator.h> -#include <libsolidity/formal/Why3Translator.h> #include <libevmasm/Exceptions.h> @@ -316,20 +315,6 @@ void CompilerStack::link() } } -bool CompilerStack::prepareFormalAnalysis(ErrorReporter* _errorReporter) -{ - if (!_errorReporter) - _errorReporter = &m_errorReporter; - Why3Translator translator(*_errorReporter); - 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 f7435f0e..c51ae9c9 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -129,12 +129,6 @@ public: /// @returns false on error. bool compile(std::string const& _sourceCode, bool _optimize = false, unsigned _runs = 200); - /// Tries to translate all source files into a language suitable for formal analysis. - /// @param _errors list to store errors - defaults to the internal error list. - /// @returns false on error. - bool prepareFormalAnalysis(ErrorReporter* _errorReporter = nullptr); - 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. @@ -290,7 +284,6 @@ private: std::map<ASTNode const*, std::shared_ptr<DeclarationContainer>> m_scopes; std::vector<Source const*> m_sourceOrder; std::map<std::string const, Contract> m_contracts; - std::string m_formalTranslation; ErrorList m_errorList; ErrorReporter m_errorReporter; bool m_metadataLiteralSources = false; diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index 0dbedd3c..d0134113 100644 --- a/solc/CommandLineInterface.cpp +++ b/solc/CommandLineInterface.cpp @@ -37,7 +37,6 @@ #include <libsolidity/interface/SourceReferenceFormatter.h> #include <libsolidity/interface/GasEstimator.h> #include <libsolidity/interface/AssemblyStack.h> -#include <libsolidity/formal/Why3Translator.h> #include <libevmasm/Instruction.h> #include <libevmasm/GasMeter.h> @@ -393,17 +392,6 @@ void CommandLineInterface::handleGasEstimation(string const& _contract) } } -void CommandLineInterface::handleFormal() -{ - if (!m_args.count(g_argFormal)) - return; - - if (m_args.count(g_argOutputDir)) - createFile("solidity.mlw", m_compiler->formalTranslation()); - else - cout << "Formal version:" << endl << m_compiler->formalTranslation() << endl; -} - void CommandLineInterface::readInputFilesAndConfigureRemappings() { bool addStdin = false; @@ -790,10 +778,6 @@ bool CommandLineInterface::processInput() unsigned runs = m_args[g_argOptimizeRuns].as<unsigned>(); bool successful = m_compiler->compile(optimize, runs, m_libraries); - if (successful && m_args.count(g_argFormal)) - if (!m_compiler->prepareFormalAnalysis()) - successful = false; - for (auto const& error: m_compiler->errors()) SourceReferenceFormatter::printExceptionInformation( cerr, @@ -1185,7 +1169,8 @@ void CommandLineInterface::outputCompilationResults() handleNatspec(DocumentationType::NatspecUser, contract); } // end of contracts iteration - handleFormal(); + if (m_args.count(g_argFormal)) + cerr << "Support for the Why3 output was removed." << endl; } } diff --git a/test/fuzzer.cpp b/test/fuzzer.cpp index 053d880f..cf99755f 100644 --- a/test/fuzzer.cpp +++ b/test/fuzzer.cpp @@ -152,7 +152,6 @@ void testCompiler() "Exception during compilation", "Unknown exception during compilation", "Unknown exception while generating contract data output", - "Unknown exception while generating formal method output", "Unknown exception while generating source name output", "Unknown error while generating JSON" }); |