diff --git a/.circleci/config.yml b/.circleci/config.yml index 2cde85f2d..119dbd372 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -476,7 +476,7 @@ jobs: b_ems: docker: - - image: trzeci/emscripten:sdk-tag-1.38.22-64bit + - image: trzeci/emscripten:sdk-tag-1.39.3-64bit environment: TERM: xterm steps: diff --git a/.travis.yml b/.travis.yml index 5754fa0a9..38d59fa93 100644 --- a/.travis.yml +++ b/.travis.yml @@ -110,7 +110,7 @@ matrix: before_install: - nvm install 8 - nvm use 8 - - docker pull trzeci/emscripten:sdk-tag-1.38.22-64bit + - docker pull trzeci/emscripten:sdk-tag-1.39.3-64bit env: - SOLC_EMSCRIPTEN=On - SOLC_INSTALL_DEPS_TRAVIS=Off @@ -127,7 +127,7 @@ matrix: # # This key here has no significant on anything, apart from caching. Please keep # it in sync with the version above. - - EMSCRIPTEN_VERSION_KEY="1.38.22" + - EMSCRIPTEN_VERSION_KEY="1.39.3" # OS X Mavericks (10.9) # https://en.wikipedia.org/wiki/OS_X_Mavericks diff --git a/Changelog.md b/Changelog.md index 2f9d1b5f0..e97fd4877 100644 --- a/Changelog.md +++ b/Changelog.md @@ -46,12 +46,18 @@ Language Features: Compiler Features: + * SMTChecker: Add support to constructors including constructor inheritance. * Yul: When compiling via Yul, string literals from the Solidity code are kept as string literals if every character is safely printable. * Yul Optimizer: Perform loop-invariant code motion. +Build System: + * Update to emscripten version 1.39.3. + + Bugfixes: * SMTChecker: Fix internal error when using ``abi.decode``. + * SMTChecker: Fix internal error when using arrays or mappings of functions. diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake index eb55feef1..afd145118 100644 --- a/cmake/EthCompilerSettings.cmake +++ b/cmake/EthCompilerSettings.cmake @@ -86,7 +86,7 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA elseif(EMSCRIPTEN) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} --memory-init-file 0") # Leave only exported symbols as public and aggressively remove others - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdata-sections -ffunction-sections -Wl,--gc-sections -fvisibility=hidden") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdata-sections -ffunction-sections -fvisibility=hidden") # Optimisation level set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O3") # Re-enable exception catching (optimisations above -O1 disable it) @@ -110,9 +110,12 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -s STRICT=1") # Export the Emscripten-generated auxiliary methods which are needed by solc-js. # Which methods of libsolc itself are exported is specified in libsolc/CMakeLists.txt. - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -s EXTRA_EXPORTED_RUNTIME_METHODS=['cwrap','addFunction','removeFunction','Pointer_stringify','lengthBytesUTF8','_malloc','stringToUTF8','setValue']") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -s EXTRA_EXPORTED_RUNTIME_METHODS=['cwrap','addFunction','removeFunction','UTF8ToString','lengthBytesUTF8','_malloc','stringToUTF8','setValue']") # Do not build as a WebAssembly target - we need an asm.js output. set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -s WASM=0") + + # Disable warnings about not being pure asm.js due to memory growth. + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-almost-asm") endif() endif() diff --git a/cmake/jsoncpp.cmake b/cmake/jsoncpp.cmake index 3e72a8be2..1377041b9 100644 --- a/cmake/jsoncpp.cmake +++ b/cmake/jsoncpp.cmake @@ -37,9 +37,9 @@ endif() ExternalProject_Add(jsoncpp-project PREFIX "${prefix}" DOWNLOAD_DIR "${CMAKE_SOURCE_DIR}/deps/downloads" - DOWNLOAD_NAME jsoncpp-1.8.4.tar.gz - URL https://github.com/open-source-parsers/jsoncpp/archive/1.8.4.tar.gz - URL_HASH SHA256=c49deac9e0933bcb7044f08516861a2d560988540b23de2ac1ad443b219afdb6 + DOWNLOAD_NAME jsoncpp-1.9.2.tar.gz + URL https://github.com/open-source-parsers/jsoncpp/archive/1.9.2.tar.gz + URL_HASH SHA256=77a402fb577b2e0e5d0bdc1cf9c65278915cdb25171e3452c68b6da8a561f8f0 CMAKE_COMMAND ${JSONCPP_CMAKE_COMMAND} CMAKE_ARGS -DCMAKE_INSTALL_PREFIX= -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} diff --git a/libdevcore/CommonData.cpp b/libdevcore/CommonData.cpp index 1299939f5..b151ba604 100644 --- a/libdevcore/CommonData.cpp +++ b/libdevcore/CommonData.cpp @@ -179,14 +179,13 @@ bool dev::isValidDecimal(string const& _string) return true; } -// Returns a quoted string if all characters are printable ASCII chars, -// or its hex representation otherwise. -std::string dev::formatAsStringOrNumber(std::string const& _value) +string dev::formatAsStringOrNumber(string const& _value) { - if (_value.length() <= 32) - for (auto const& c: _value) - if (c <= 0x1f || c >= 0x7f || c == '"') - return "0x" + h256(_value, h256::AlignLeft).hex(); + assertThrow(_value.length() <= 32, StringTooLong, "String to be formatted longer than 32 bytes."); + + for (auto const& c: _value) + if (c <= 0x1f || c >= 0x7f || c == '"') + return "0x" + h256(_value, h256::AlignLeft).hex(); return "\"" + _value + "\""; } diff --git a/libdevcore/CommonData.h b/libdevcore/CommonData.h index 439134cc2..c34472ed0 100644 --- a/libdevcore/CommonData.h +++ b/libdevcore/CommonData.h @@ -401,6 +401,7 @@ bool isValidDecimal(std::string const& _string); /// @returns a quoted string if all characters are printable ASCII chars, /// or its hex representation otherwise. +/// _value cannot be longer than 32 bytes. std::string formatAsStringOrNumber(std::string const& _value); template diff --git a/libdevcore/Exceptions.h b/libdevcore/Exceptions.h index df7a9ba01..851be4ea1 100644 --- a/libdevcore/Exceptions.h +++ b/libdevcore/Exceptions.h @@ -49,6 +49,7 @@ DEV_SIMPLE_EXCEPTION(BadHexCharacter); DEV_SIMPLE_EXCEPTION(BadHexCase); DEV_SIMPLE_EXCEPTION(FileError); DEV_SIMPLE_EXCEPTION(DataTooLong); +DEV_SIMPLE_EXCEPTION(StringTooLong); // error information to be added to exceptions using errinfo_comment = boost::error_info; diff --git a/libdevcore/JSON.cpp b/libdevcore/JSON.cpp index 0b08616da..80c116bbe 100644 --- a/libdevcore/JSON.cpp +++ b/libdevcore/JSON.cpp @@ -32,8 +32,8 @@ using namespace std; static_assert( - (JSONCPP_VERSION_MAJOR == 1) && (JSONCPP_VERSION_MINOR == 8) && (JSONCPP_VERSION_PATCH == 4), - "Unexpected jsoncpp version: " JSONCPP_VERSION_STRING ". Expecting 1.8.4." + (JSONCPP_VERSION_MAJOR == 1) && (JSONCPP_VERSION_MINOR == 9) && (JSONCPP_VERSION_PATCH == 2), + "Unexpected jsoncpp version: " JSONCPP_VERSION_STRING ". Expecting 1.9.2." ); namespace dev diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 6950e95c0..1fc594978 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -114,11 +114,6 @@ bool BMC::visit(ContractDefinition const& _contract) { initContract(_contract); - /// Check targets created by state variable initialization. - smt::Expression constraints = m_context.assertions(); - checkVerificationTargets(constraints); - m_verificationTargets.clear(); - SMTEncoder::visit(_contract); return false; @@ -126,6 +121,17 @@ bool BMC::visit(ContractDefinition const& _contract) void BMC::endVisit(ContractDefinition const& _contract) { + if (auto constructor = _contract.constructor()) + constructor->accept(*this); + else + { + inlineConstructorHierarchy(_contract); + /// Check targets created by state variable initialization. + smt::Expression constraints = m_context.assertions(); + checkVerificationTargets(constraints); + m_verificationTargets.clear(); + } + SMTEncoder::endVisit(_contract); } @@ -136,10 +142,14 @@ bool BMC::visit(FunctionDefinition const& _function) solAssert(m_currentContract, ""); auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; if (find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end()) - initializeStateVariables(*contract); + createStateVariables(*contract); if (m_callStack.empty()) + { reset(); + initFunction(_function); + resetStateVariables(); + } /// Already visits the children. SMTEncoder::visit(_function); @@ -451,10 +461,6 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) // The reason why we need to pushCallStack here instead of visit(FunctionDefinition) // is that there we don't have `_funCall`. pushCallStack({funDef, &_funCall}); - // If an internal function is called to initialize - // a state variable. - if (m_callStack.empty()) - initFunction(*funDef); funDef->accept(*this); } diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 92acca004..3a142616e 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -67,6 +67,15 @@ void CHC::analyze(SourceUnit const& _source) m_context.setAssertionAccumulation(false); m_variableUsage.setFunctionInlining(false); + auto boolSort = make_shared(smt::Kind::Bool); + auto genesisSort = make_shared( + vector(), + boolSort + ); + m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis"); + auto genesis = (*m_genesisPredicate)({}); + addRule(genesis, genesis.name); + _source.accept(*this); } @@ -96,10 +105,10 @@ bool CHC::visit(ContractDefinition const& _contract) else m_stateSorts.push_back(smt::smtSort(*var->type())); - clearIndices(); + clearIndices(&_contract); - string interfaceName = "interface_" + _contract.name() + "_" + to_string(_contract.id()); - m_interfacePredicate = createSymbolicBlock(interfaceSort(), interfaceName); + string suffix = _contract.name() + "_" + to_string(_contract.id()); + m_interfacePredicate = createSymbolicBlock(interfaceSort(), "interface_" + suffix); // TODO create static instances for Bool/Int sorts in SolverInterface. auto boolSort = make_shared(smt::Kind::Bool); @@ -107,27 +116,11 @@ bool CHC::visit(ContractDefinition const& _contract) vector(), boolSort ); - m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error"); - // If the contract has a constructor it is handled as a function. - // Otherwise we zero-initialize all state vars. - if (!_contract.constructor()) - { - string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id()); - m_constructorPredicate = createSymbolicBlock(constructorSort(), constructorName); - smt::Expression constructorPred = (*m_constructorPredicate)({}); - addRule(constructorPred, constructorName); - - for (auto const& var: m_stateVariables) - { - auto const& symbVar = m_context.variable(*var); - symbVar->increaseIndex(); - m_interface->declareVariable(symbVar->currentName(), symbVar->sort()); - m_context.setZeroValue(*symbVar); - } - - connectBlocks(constructorPred, interface()); - } + m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error_" + suffix); + m_constructorPredicate = createSymbolicBlock(constructorSort(), "implicit_constructor_" + to_string(_contract.id())); + auto stateExprs = currentStateVariables(); + setCurrentBlock(*m_interfacePredicate, &stateExprs); SMTEncoder::visit(_contract); return false; @@ -138,6 +131,23 @@ void CHC::endVisit(ContractDefinition const& _contract) if (!shouldVisit(_contract)) return; + for (auto const& var: m_stateVariables) + { + solAssert(m_context.knownVariable(*var), ""); + m_context.setZeroValue(*var); + } + auto genesisPred = (*m_genesisPredicate)({}); + auto implicitConstructor = (*m_constructorPredicate)(currentStateVariables()); + connectBlocks(genesisPred, implicitConstructor); + m_currentBlock = implicitConstructor; + + if (auto constructor = _contract.constructor()) + constructor->accept(*this); + else + inlineConstructorHierarchy(_contract); + + connectBlocks(m_currentBlock, interface()); + for (unsigned i = 0; i < m_verificationTargets.size(); ++i) { auto const& target = m_verificationTargets.at(i); @@ -154,6 +164,16 @@ bool CHC::visit(FunctionDefinition const& _function) if (!shouldVisit(_function)) return false; + // This is the case for base constructor inlining. + if (m_currentFunction) + { + solAssert(m_currentFunction->isConstructor(), ""); + solAssert(_function.isConstructor(), ""); + solAssert(_function.scope() != m_currentContract, ""); + SMTEncoder::visit(_function); + return false; + } + solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented"); m_currentFunction = &_function; @@ -165,20 +185,11 @@ bool CHC::visit(FunctionDefinition const& _function) auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables()); auto bodyPred = predicate(*bodyBlock); - // Store the constraints related to variable initialization. - smt::Expression const& initAssertions = m_context.assertions(); - m_context.pushSolver(); - - connectBlocks(interface(), functionPred); + connectBlocks(m_currentBlock, functionPred); connectBlocks(functionPred, bodyPred); - m_context.popSolver(); - setCurrentBlock(*bodyBlock); - // We need to re-add the constraints that were created for initialization of variables. - m_context.addAssertion(initAssertions); - SMTEncoder::visit(*m_currentFunction); return false; @@ -189,10 +200,39 @@ void CHC::endVisit(FunctionDefinition const& _function) if (!shouldVisit(_function)) return; - connectBlocks(m_currentBlock, interface()); + // This is the case for base constructor inlining. + if (m_currentFunction != &_function) + { + solAssert(m_currentFunction && m_currentFunction->isConstructor(), ""); + solAssert(_function.isConstructor(), ""); + solAssert(_function.scope() != m_currentContract, ""); + } + else + { + // We create an extra exit block for constructors that simply + // connects to the interface in case an explicit constructor + // exists in the hierarchy. + // It is not connected directly here, as normal functions are, + // because of the case where there are only implicit constructors. + // This is done in endVisit(ContractDefinition). + if (_function.isConstructor()) + { + auto constructorExit = createSymbolicBlock(interfaceSort(), "constructor_exit_" + to_string(_function.id())); + connectBlocks(m_currentBlock, predicate(*constructorExit, currentStateVariables())); + clearIndices(m_currentContract, m_currentFunction); + auto stateExprs = currentStateVariables(); + setCurrentBlock(*constructorExit, &stateExprs); + } + else + { + connectBlocks(m_currentBlock, interface()); + clearIndices(m_currentContract, m_currentFunction); + auto stateExprs = currentStateVariables(); + setCurrentBlock(*m_interfacePredicate, &stateExprs); + } + m_currentFunction = nullptr; + } - solAssert(&_function == m_currentFunction, ""); - m_currentFunction = nullptr; SMTEncoder::endVisit(_function); } @@ -447,7 +487,6 @@ void CHC::reset() m_verificationTargets.clear(); m_safeAssertions.clear(); m_unknownFunctionCallSeen = false; - m_blockCounter = 0; m_breakDest = nullptr; m_continueDest = nullptr; } @@ -472,28 +511,31 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const { if ( _function.isPublic() && - _function.isImplemented() && - !_function.isConstructor() + _function.isImplemented() ) return true; return false; } -void CHC::setCurrentBlock(smt::SymbolicFunctionVariable const& _block) +void CHC::setCurrentBlock( + smt::SymbolicFunctionVariable const& _block, + vector const* _arguments +) { m_context.popSolver(); - clearIndices(); + solAssert(m_currentContract, ""); + clearIndices(m_currentContract, m_currentFunction); m_context.pushSolver(); - m_currentBlock = predicate(_block); + if (_arguments) + m_currentBlock = predicate(_block, *_arguments); + else + m_currentBlock = predicate(_block); } smt::SortPointer CHC::constructorSort() { - solAssert(m_currentContract, ""); - auto boolSort = make_shared(smt::Kind::Bool); - if (!m_currentContract->constructor()) - return make_shared(vector{}, boolSort); - return sort(*m_currentContract->constructor()); + // TODO this will change once we support function calls. + return interfaceSort(); } smt::SortPointer CHC::interfaceSort() @@ -558,19 +600,6 @@ unique_ptr CHC::createSymbolicBlock(smt::SortPoin return block; } -smt::Expression CHC::constructor() -{ - solAssert(m_currentContract, ""); - - if (!m_currentContract->constructor()) - return (*m_constructorPredicate)({}); - - vector paramExprs; - for (auto const& var: m_currentContract->constructor()->parameters()) - paramExprs.push_back(m_context.variable(*var)->currentValue()); - return (*m_constructorPredicate)(paramExprs); -} - smt::Expression CHC::interface() { vector paramExprs; @@ -615,37 +644,31 @@ void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to addRule(edge, _from.name + "_to_" + _to.name); } +vector CHC::currentStateVariables() +{ + solAssert(m_currentContract, ""); + vector exprs; + for (auto const& var: m_stateVariables) + exprs.push_back(m_context.variable(*var)->currentValue()); + return exprs; +} + vector CHC::currentFunctionVariables() { - solAssert(m_currentFunction, ""); vector paramExprs; - for (auto const& var: m_stateVariables) - paramExprs.push_back(m_context.variable(*var)->currentValue()); - for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters()) - paramExprs.push_back(m_context.variable(*var)->currentValue()); - return paramExprs; + if (m_currentFunction) + for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters()) + paramExprs.push_back(m_context.variable(*var)->currentValue()); + return currentStateVariables() + paramExprs; } vector CHC::currentBlockVariables() { - solAssert(m_currentFunction, ""); vector paramExprs; - for (auto const& var: m_currentFunction->localVariables()) - paramExprs.push_back(m_context.variable(*var)->currentValue()); - return currentFunctionVariables() + paramExprs; -} - -void CHC::clearIndices() -{ - for (auto const& var: m_stateVariables) - m_context.variable(*var)->resetIndex(); if (m_currentFunction) - { - for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters()) - m_context.variable(*var)->resetIndex(); for (auto const& var: m_currentFunction->localVariables()) - m_context.variable(*var)->resetIndex(); - } + paramExprs.push_back(m_context.variable(*var)->currentValue()); + return currentFunctionVariables() + paramExprs; } string CHC::predicateName(ASTNode const* _node) @@ -673,7 +696,6 @@ smt::Expression CHC::predicate( return _block(_arguments); } - void CHC::addRule(smt::Expression const& _rule, string const& _ruleName) { m_interface->addRule(_rule, _ruleName); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 8e6484a18..8c3e322ce 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -86,7 +86,7 @@ private: void eraseKnowledge(); bool shouldVisit(ContractDefinition const& _contract) const; bool shouldVisit(FunctionDefinition const& _function) const; - void setCurrentBlock(smt::SymbolicFunctionVariable const& _block); + void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector const* _arguments = nullptr); //@} /// Sort helpers. @@ -102,8 +102,6 @@ private: /// @returns a new block of given _sort and _name. std::unique_ptr createSymbolicBlock(smt::SortPointer _sort, std::string const& _name); - /// Constructor predicate over current variables. - smt::Expression constructor(); /// Interface predicate over current variables. smt::Expression interface(); /// Error predicate over current variables. @@ -119,17 +117,16 @@ private: void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true)); + /// @returns the current symbolic values of the current state variables. + std::vector currentStateVariables(); + /// @returns the current symbolic values of the current function's /// input and output parameters. std::vector currentFunctionVariables(); - /// @returns the samve as currentFunctionVariables plus + /// @returns the same as currentFunctionVariables plus /// local variables. std::vector currentBlockVariables(); - /// Sets the SSA indices of the variables in scope to 0. - /// Used when starting a new block. - void clearIndices(); - /// @returns the predicate name for a given node. std::string predicateName(ASTNode const* _node); /// @returns a predicate application over the current scoped variables. @@ -155,8 +152,11 @@ private: /// Predicates. //@{ - /// Constructor predicate. - /// Default constructor sets state vars to 0. + /// Genesis predicate. + std::unique_ptr m_genesisPredicate; + + /// Implicit constructor predicate. + /// Explicit constructors are handled as functions. std::unique_ptr m_constructorPredicate; /// Artificial Interface predicate. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index d253087bd..6fb85a15c 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -22,6 +22,7 @@ #include #include +#include using namespace std; using namespace dev; @@ -39,11 +40,28 @@ bool SMTEncoder::visit(ContractDefinition const& _contract) solAssert(m_currentContract, ""); for (auto const& node: _contract.subNodes()) - if (!dynamic_pointer_cast(node)) + if ( + !dynamic_pointer_cast(node) && + !dynamic_pointer_cast(node) + ) node->accept(*this); vector resolvedFunctions = _contract.definedFunctions(); for (auto const& base: _contract.annotation().linearizedBaseContracts) + { + // Look for all the constructor invocations bottom up. + if (auto const& constructor = base->constructor()) + for (auto const& invocation: constructor->modifiers()) + { + auto refDecl = invocation->name()->annotation().referencedDeclaration; + if (auto const& baseContract = dynamic_cast(refDecl)) + { + solAssert(!m_baseConstructorCalls.count(baseContract), ""); + m_baseConstructorCalls[baseContract] = invocation.get(); + } + } + + // Check for function overrides. for (auto const& baseFunction: base->definedFunctions()) { if (baseFunction->isConstructor()) @@ -63,9 +81,18 @@ bool SMTEncoder::visit(ContractDefinition const& _contract) if (!overridden) resolvedFunctions.push_back(baseFunction); } + } + // Functions are visited first since they might be used + // for state variable initialization which is part of + // the constructor. + // Constructors are visited as part of the constructor + // hierarchy inlining. for (auto const& function: resolvedFunctions) - function->accept(*this); + if (!function->isConstructor()) + function->accept(*this); + + // Constructors need to be handled by the engines separately. return false; } @@ -74,13 +101,16 @@ void SMTEncoder::endVisit(ContractDefinition const& _contract) { m_context.resetAllVariables(); + m_baseConstructorCalls.clear(); + solAssert(m_currentContract == &_contract, ""); m_currentContract = nullptr; } void SMTEncoder::endVisit(VariableDeclaration const& _varDecl) { - if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) + // State variables are handled by the constructor. + if (_varDecl.isLocalVariable() &&_varDecl.value()) assignment(_varDecl, *_varDecl.value()); } @@ -91,25 +121,22 @@ bool SMTEncoder::visit(ModifierDefinition const&) bool SMTEncoder::visit(FunctionDefinition const& _function) { - // Not visited by a function call - if (m_callStack.empty()) - initFunction(_function); - m_modifierDepthStack.push_back(-1); + if (_function.isConstructor()) - { - m_errorReporter.warning( - _function.location(), - "Assertion checker does not yet support constructors." - ); - } - else - { - _function.parameterList().accept(*this); - if (_function.returnParameterList()) - _function.returnParameterList()->accept(*this); - visitFunctionOrModifier(); - } + inlineConstructorHierarchy(dynamic_cast(*_function.scope())); + + // Base constructors' parameters should be set by explicit calls, + // but the most derived one needs to be initialized. + if (_function.scope() == m_currentContract) + initializeLocalVariables(_function); + + _function.parameterList().accept(*this); + if (_function.returnParameterList()) + _function.returnParameterList()->accept(*this); + + visitFunctionOrModifier(); + return false; } @@ -131,27 +158,87 @@ void SMTEncoder::visitFunctionOrModifier() solAssert(m_modifierDepthStack.back() < int(function.modifiers().size()), ""); ASTPointer const& modifierInvocation = function.modifiers()[m_modifierDepthStack.back()]; solAssert(modifierInvocation, ""); - modifierInvocation->accept(*this); - auto const& modifierDef = dynamic_cast( - *modifierInvocation->name()->annotation().referencedDeclaration - ); - vector modifierArgsExpr; - if (auto const* arguments = modifierInvocation->arguments()) - { - auto const& modifierParams = modifierDef.parameters(); - solAssert(modifierParams.size() == arguments->size(), ""); - for (unsigned i = 0; i < arguments->size(); ++i) - modifierArgsExpr.push_back(expr(*arguments->at(i), modifierParams.at(i)->type())); - } - initializeFunctionCallParameters(modifierDef, modifierArgsExpr); - pushCallStack({&modifierDef, modifierInvocation.get()}); - modifierDef.body().accept(*this); - popCallStack(); + auto refDecl = modifierInvocation->name()->annotation().referencedDeclaration; + if (dynamic_cast(refDecl)) + visitFunctionOrModifier(); + else if (auto modifierDef = dynamic_cast(refDecl)) + inlineModifierInvocation(modifierInvocation.get(), modifierDef); + else + solAssert(false, ""); } --m_modifierDepthStack.back(); } +void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition) +{ + solAssert(_invocation, ""); + _invocation->accept(*this); + + vector args; + if (auto const* arguments = _invocation->arguments()) + { + auto const& modifierParams = _definition->parameters(); + solAssert(modifierParams.size() == arguments->size(), ""); + for (unsigned i = 0; i < arguments->size(); ++i) + args.push_back(expr(*arguments->at(i), modifierParams.at(i)->type())); + } + + initializeFunctionCallParameters(*_definition, args); + + pushCallStack({_definition, _invocation}); + if (auto modifier = dynamic_cast(_definition)) + { + modifier->body().accept(*this); + popCallStack(); + } + else if (auto function = dynamic_cast(_definition)) + { + if (function->isImplemented()) + function->accept(*this); + // Functions are popped from the callstack in endVisit(FunctionDefinition) + } +} + +void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract) +{ + auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; + auto it = find(begin(hierarchy), end(hierarchy), &_contract); + solAssert(it != end(hierarchy), ""); + + auto nextBase = it + 1; + // Initialize the base contracts here as long as their constructors are implicit, + // stop when the first explicit constructor is found. + while (nextBase != end(hierarchy)) + { + if (auto baseConstructor = (*nextBase)->constructor()) + { + createLocalVariables(*baseConstructor); + // If any subcontract explicitly called baseConstructor, use those arguments. + if (m_baseConstructorCalls.count(*nextBase)) + inlineModifierInvocation(m_baseConstructorCalls.at(*nextBase), baseConstructor); + else if (baseConstructor->isImplemented()) + { + // The first constructor found is handled like a function + // and its pushed into the callstack there. + // This if avoids duplication in the callstack. + if (!m_callStack.empty()) + pushCallStack({baseConstructor, nullptr}); + baseConstructor->accept(*this); + // popped by endVisit(FunctionDefinition) + } + break; + } + else + { + initializeStateVariables(**nextBase); + ++nextBase; + } + } + + initializeStateVariables(_contract); +} + bool SMTEncoder::visit(PlaceholderStatement const&) { solAssert(!m_callStack.empty(), ""); @@ -552,20 +639,25 @@ void SMTEncoder::initContract(ContractDefinition const& _contract) solAssert(m_currentContract == nullptr, ""); m_currentContract = &_contract; - initializeStateVariables(_contract); + m_context.reset(); + m_context.pushSolver(); + createStateVariables(_contract); + clearIndices(m_currentContract, nullptr); } void SMTEncoder::initFunction(FunctionDefinition const& _function) { solAssert(m_callStack.empty(), ""); + solAssert(m_currentContract, ""); m_context.reset(); m_context.pushSolver(); m_pathConditions.clear(); pushCallStack({&_function, nullptr}); m_uninterpretedTerms.clear(); - resetStateVariables(); - initializeLocalVariables(_function); + createStateVariables(*m_currentContract); + createLocalVariables(_function); m_arrayAssignmentHappened = false; + clearIndices(m_currentContract, &_function); } void SMTEncoder::visitAssert(FunctionCall const& _funCall) @@ -808,11 +900,8 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) return; } - if (!_indexAccess.indexExpression()) - { - solAssert(_indexAccess.annotation().type->category() == Type::Category::TypeType, ""); + if (_indexAccess.annotation().type->category() == Type::Category::TypeType) return; - } solAssert(array, ""); defineExpr(_indexAccess, smt::Expression::select( @@ -1249,26 +1338,61 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu } } -void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract) +void SMTEncoder::createStateVariables(ContractDefinition const& _contract) { for (auto var: _contract.stateVariablesIncludingInherited()) createVariable(*var); } -void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function) +void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract) +{ + for (auto var: _contract.stateVariables()) + { + solAssert(m_context.knownVariable(*var), ""); + m_context.setZeroValue(*var); + } + + for (auto var: _contract.stateVariables()) + if (var->value()) + { + var->value()->accept(*this); + assignment(*var, *var->value()); + } +} + +void SMTEncoder::createLocalVariables(FunctionDefinition const& _function) { for (auto const& variable: _function.localVariables()) - if (createVariable(*variable)) - m_context.setZeroValue(*variable); + createVariable(*variable); for (auto const& param: _function.parameters()) - if (createVariable(*param)) - m_context.setUnknownValue(*param); + createVariable(*param); if (_function.returnParameterList()) for (auto const& retParam: _function.returnParameters()) - if (createVariable(*retParam)) - m_context.setZeroValue(*retParam); + createVariable(*retParam); +} + +void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function) +{ + for (auto const& variable: _function.localVariables()) + { + solAssert(m_context.knownVariable(*variable), ""); + m_context.setZeroValue(*variable); + } + + for (auto const& param: _function.parameters()) + { + solAssert(m_context.knownVariable(*param), ""); + m_context.setUnknownValue(*param); + } + + if (_function.returnParameterList()) + for (auto const& retParam: _function.returnParameters()) + { + solAssert(m_context.knownVariable(*retParam), ""); + m_context.setZeroValue(*retParam); + } } void SMTEncoder::resetStateVariables() @@ -1448,6 +1572,20 @@ void SMTEncoder::resetVariableIndices(VariableIndices const& _indices) m_context.variable(*var.first)->index() = var.second; } +void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function) +{ + solAssert(_contract, ""); + for (auto var: _contract->stateVariablesIncludingInherited()) + m_context.variable(*var)->resetIndex(); + if (_function) + { + for (auto const& var: _function->parameters() + _function->returnParameters()) + m_context.variable(*var)->resetIndex(); + for (auto const& var: _function->localVariables()) + m_context.variable(*var)->resetIndex(); + } +} + Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess) { Expression const* base = &_indexAccess.baseExpression(); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 078cc385c..b39fff270 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -123,6 +123,12 @@ protected: /// visit depth. void visitFunctionOrModifier(); + /// Inlines a modifier or base constructor call. + void inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition); + + /// Inlines the constructor hierarchy into a single constructor. + void inlineConstructorHierarchy(ContractDefinition const& _contract); + /// Defines a new global variable or function. void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false); @@ -162,7 +168,9 @@ protected: using CallStackEntry = std::pair; + void createStateVariables(ContractDefinition const& _contract); void initializeStateVariables(ContractDefinition const& _contract); + void createLocalVariables(FunctionDefinition const& _function); void initializeLocalVariables(FunctionDefinition const& _function); void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector const& _callArgs); void resetStateVariables(); @@ -210,6 +218,9 @@ protected: VariableIndices copyVariableIndices(); /// Resets the variable indices. void resetVariableIndices(VariableIndices const& _indices); + /// Used when starting a new block. + void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr); + /// @returns variables that are touched in _node's subtree. std::set touchedVariables(ASTNode const& _node); @@ -254,6 +265,8 @@ protected: /// Needs to be a stack because of function calls. std::vector m_modifierDepthStack; + std::map m_baseConstructorCalls; + ContractDefinition const* m_currentContract = nullptr; /// Stores the context of the encoding. diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 591158a25..0fe05e723 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -63,7 +63,7 @@ SortPointer smtSort(solidity::Type const& _type) { auto mapType = dynamic_cast(&_type); solAssert(mapType, ""); - return make_shared(smtSort(*mapType->keyType()), smtSort(*mapType->valueType())); + return make_shared(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType())); } else if (isStringLiteral(_type.category())) { @@ -77,7 +77,7 @@ SortPointer smtSort(solidity::Type const& _type) solAssert(isArray(_type.category()), ""); auto arrayType = dynamic_cast(&_type); solAssert(arrayType, ""); - return make_shared(make_shared(Kind::Int), smtSort(*arrayType->baseType())); + return make_shared(make_shared(Kind::Int), smtSortAbstractFunction(*arrayType->baseType())); } } default: @@ -94,6 +94,13 @@ vector smtSort(vector const& _types) return sorts; } +SortPointer smtSortAbstractFunction(solidity::Type const& _type) +{ + if (isFunction(_type.category())) + return make_shared(Kind::Int); + return smtSort(_type); +} + Kind smtKind(solidity::Type::Category _category) { if (isNumber(_category)) diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 30a341431..2db2807ac 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -32,6 +32,9 @@ namespace smt /// Returns the SMT sort that models the Solidity type _type. SortPointer smtSort(solidity::Type const& _type); std::vector smtSort(std::vector const& _types); +/// If _type has type Function, abstract it to Integer. +/// Otherwise return smtSort(_type). +SortPointer smtSortAbstractFunction(solidity::Type const& _type); /// Returns the SMT kind that models the Solidity type type category _category. Kind smtKind(solidity::Type::Category _category); diff --git a/scripts/build_emscripten.sh b/scripts/build_emscripten.sh index 25f6f7f8c..b457b741d 100755 --- a/scripts/build_emscripten.sh +++ b/scripts/build_emscripten.sh @@ -34,7 +34,7 @@ else BUILD_DIR="$1" fi -docker run -v $(pwd):/root/project -w /root/project trzeci/emscripten:sdk-tag-1.38.22-64bit \ +docker run -v $(pwd):/root/project -w /root/project trzeci/emscripten:sdk-tag-1.39.3-64bit \ ./scripts/travis-emscripten/install_deps.sh -docker run -v $(pwd):/root/project -w /root/project trzeci/emscripten:sdk-tag-1.38.22-64bit \ +docker run -v $(pwd):/root/project -w /root/project trzeci/emscripten:sdk-tag-1.39.3-64bit \ ./scripts/travis-emscripten/build_emscripten.sh $BUILD_DIR diff --git a/scripts/travis-emscripten/build_emscripten.sh b/scripts/travis-emscripten/build_emscripten.sh index 5c8a06e58..8011205db 100755 --- a/scripts/travis-emscripten/build_emscripten.sh +++ b/scripts/travis-emscripten/build_emscripten.sh @@ -55,11 +55,11 @@ fi WORKSPACE=/root/project # Increase nodejs stack size -if ! [ -e /emsdk_portable/node/bin/node_orig ] +if ! [ -e /emsdk_portable/node/current/bin/node_orig ] then - mv /emsdk_portable/node/bin/node /emsdk_portable/node/bin/node_orig - echo -e '#!/bin/sh\nexec /emsdk_portable/node/bin/node_orig --stack-size=8192 $@' > /emsdk_portable/node/bin/node - chmod 755 /emsdk_portable/node/bin/node + mv /emsdk_portable/node/current/bin/node /emsdk_portable/node/current/bin/node_orig + echo -e '#!/bin/sh\nexec /emsdk_portable/node/current/bin/node_orig --stack-size=8192 $@' > /emsdk_portable/node/current/bin/node + chmod 755 /emsdk_portable/node/current/bin/node fi # Boost @@ -70,8 +70,8 @@ cd "$WORKSPACE"/boost_1_70_0 --with-system --with-filesystem --with-test --with-program_options cxxflags="-Wno-unused-local-typedef -Wno-variadic-macros -Wno-c99-extensions -Wno-all" \ --prefix="$WORKSPACE"/boost_1_70_0_install install ) -ln -sf "$WORKSPACE"/boost_1_70_0_install/lib/* /emsdk_portable/sdk/system/lib -ln -sf "$WORKSPACE"/boost_1_70_0_install/include/* /emsdk_portable/sdk/system/include +ln -sf "$WORKSPACE"/boost_1_70_0_install/lib/* /emsdk_portable/emscripten/sdk/system/lib +ln -sf "$WORKSPACE"/boost_1_70_0_install/include/* /emsdk_portable/emscripten/sdk/system/include echo -en 'travis_fold:end:compiling_boost\\r' echo -en 'travis_fold:start:install_cmake.sh\\r' @@ -94,8 +94,6 @@ make -j 4 cd .. mkdir -p upload -# Patch soljson.js to provide backwards-compatibility with older emscripten versions -echo ";/* backwards compatibility */ Module['Runtime'] = Module;" >> $BUILD_DIR/libsolc/soljson.js cp $BUILD_DIR/libsolc/soljson.js upload/ cp $BUILD_DIR/libsolc/soljson.js ./ diff --git a/scripts/travis-emscripten/emscripten.jam b/scripts/travis-emscripten/emscripten.jam new file mode 100644 index 000000000..0cc92bd56 --- /dev/null +++ b/scripts/travis-emscripten/emscripten.jam @@ -0,0 +1,186 @@ +# Modified version of emscripten.jam from https://github.com/tee3/boost-build-emscripten +# which is released under the following license: +# +# Boost Software License - Version 1.0 - August 17th, 2003 +# +# Permission is hereby granted, free of charge, to any person or organization +# obtaining a copy of the software and accompanying documentation covered by +# this license (the "Software") to use, reproduce, display, distribute, +# execute, and transmit the Software, and to prepare derivative works of the +# Software, and to permit third-parties to whom the Software is furnished to +# do so, all subject to the following: +# +# The copyright notices in the Software and this entire statement, including +# the above license grant, this restriction and the following disclaimer, +# must be included in all copies of the Software, in whole or in part, and +# all derivative works of the Software, unless such copies or derivative +# works are solely in the form of machine-executable object code generated by +# a source language processor. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT +# SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE +# FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE, +# ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +# DEALINGS IN THE SOFTWARE. +# +# Boost.Build support for Emscipten. +# +# @todo add support for dynamic linking +# @todo add support for --js-library, --pre-js, and --post-js options + +import generators ; +import type ; +import toolset ; +import feature ; +import common ; +import errors ; + +if [ MATCH (--debug-configuration) : [ modules.peek : ARGV ] ] +{ + .debug-configuration = true ; +} + +# add an emscripten toolset +feature.extend toolset : emscripten ; + +# extend the target-os list to include emscripten +feature.extend target-os : emscripten ; +# make emscripten the default target-os when compiling with the emscripten toolset +feature.set-default target-os : emscripten ; + +# initialize the emscripten toolset +rule init ( version ? : command * : options * ) +{ + command = [ common.get-invocation-command emscripten : em++ : $(command) ] ; + + if $(command) + { + version ?= [ MATCH "^([0-9.]+)" : [ SHELL \""$(command)\" --version" ] ] ; + if $(version) + { + local actual_version = [ MATCH "^([0-9.]+)" : [ SHELL \""$(command)\" --version" ] ] ; + if $(actual_version) != $(version) + { + errors.user-error "emscripten: detected version $(actual_version) does not match desired $(version)" ; + } + } + } + else + { + errors.user-error "emscripten: em++ not found" ; + } + + local condition = [ common.check-init-parameters emscripten : version $(version) ] ; + + common.handle-options emscripten : $(condition) : $(command) : $(options) ; + + # @todo this seems to be the right way, but this is a list somehow + toolset.add-requirements emscripten:node ; + + toolset.flags emscripten.compile STDHDRS $(condition) : /emsdk_portable/emscripten/sdk/system/include ; + toolset.flags emscripten.link STDLIBPATH $(condition) : /emsdk_portable/emscripten/sdk/system/lib ; + toolset.flags emscripten AR $(condition) : /emsdk_portable/emscripten/sdk/emar ; + toolset.flags emscripten RANLIB $(condition) : /emsdk_portable/emscripten/sdk/emranlib ; +} + +type.set-generated-target-suffix EXE : emscripten : js ; +#type.set-generated-target-suffix STATIC_LIB : emscripten : bc ; +#type.set-generated-target-suffix SHARED_LIB : emscripten : bc ; +#type.set-generated-target-suffix OBJ : emscripten : bc ; + +generators.register-linker emscripten.link : OBJ STATIC_LIB : EXE : emscripten ; + +generators.register-archiver emscripten.archive : OBJ : STATIC_LIB : emscripten ; + +generators.register-c-compiler emscripten.compile.c++.preprocess : CPP : PREPROCESSED_CPP : emscripten ; +generators.register-c-compiler emscripten.compile.c.preprocess : C : PREPROCESSED_C : emscripten ; +generators.register-c-compiler emscripten.compile.c++ : CPP : OBJ : emscripten ; +generators.register-c-compiler emscripten.compile.c : C : OBJ : emscripten ; + +# Declare flags + +toolset.flags emscripten.compile OPTIONS off : -O0 ; +toolset.flags emscripten.compile OPTIONS speed : -O3 ; +toolset.flags emscripten.compile OPTIONS space : -Os ; + +toolset.flags emscripten.compile OPTIONS off : -fno-inline ; +toolset.flags emscripten.compile OPTIONS on : -Wno-inline ; +toolset.flags emscripten.compile OPTIONS full : -finline-functions -Wno-inline ; + +toolset.flags emscripten.compile OPTIONS off : -w ; +toolset.flags emscripten.compile OPTIONS on : -Wall ; +toolset.flags emscripten.compile OPTIONS all : -Wall -pedantic ; +toolset.flags emscripten.compile OPTIONS on : -Werror ; + +toolset.flags emscripten.compile OPTIONS on : -g ; +toolset.flags emscripten.compile OPTIONS on : -pg ; + +toolset.flags emscripten.compile.c++ OPTIONS off : -fno-rtti ; +toolset.flags emscripten.compile.c++ OPTIONS off : -fno-exceptions ; + +toolset.flags emscripten.compile USER_OPTIONS ; +toolset.flags emscripten.compile.c++ USER_OPTIONS ; +toolset.flags emscripten.compile DEFINES ; +toolset.flags emscripten.compile INCLUDES ; +toolset.flags emscripten.compile.c++ TEMPLATE_DEPTH ; +toolset.flags emscripten.compile.fortran USER_OPTIONS ; + +toolset.flags emscripten.link DEFAULTS : -Wno-warn-absolute-paths ; + +toolset.flags emscripten.link LIBRARY_PATH ; +toolset.flags emscripten.link FINDLIBS_ST ; +toolset.flags emscripten.link FINDLIBS_SA ; +toolset.flags emscripten.link LIBRARIES ; + +toolset.flags emscripten.link OPTIONS ; + +toolset.flags emscripten.archive AROPTIONS ; + +rule compile.c++ ( targets * : sources * : properties * ) +{ + # Some extensions are compiled as C++ by default. For others, we need to + # pass -x c++. We could always pass -x c++ but distcc does not work with it. + if ! $(>:S) in .cc .cp .cxx .cpp .c++ .C + { + LANG on $(<) = "-x c++" ; + } +} + +rule compile.c ( targets * : sources * : properties * ) +{ + LANG on $(<) = "-x c" ; +} + +actions compile.c++ +{ + "$(CONFIG_COMMAND)" $(LANG) $(OPTIONS) $(USER_OPTIONS) -D$(DEFINES) -I"$(INCLUDES)" -c -o "$(<:W)" "$(>:W)" +} + +actions compile.c +{ + "$(CONFIG_COMMAND)" $(LANG) $(OPTIONS) $(USER_OPTIONS) -D$(DEFINES) -I"$(INCLUDES)" -c -o "$(<)" "$(>)" +} + +actions compile.c++.preprocess +{ + "$(CONFIG_COMMAND)" $(LANG) $(OPTIONS) $(USER_OPTIONS) -D$(DEFINES) -I"$(INCLUDES)" "$(>:W)" -E >"$(<:W)" +} + +actions compile.c.preprocess +{ + "$(CONFIG_COMMAND)" $(LANG) $(OPTIONS) $(USER_OPTIONS) -D$(DEFINES) -I"$(INCLUDES)" "$(>)" -E >$(<) +} + +actions link +{ + "$(CONFIG_COMMAND)" $(DEFAULTS) $(OPTIONS) -L"$(LIBRARY_PATH:W)" -L"$(STDLIBPATH:W)" -o "$(<:W)" "$(>:W)" -l"$(LIBRARIES:W)" -l"$(STDLIBRARIES:W)" +} + +RM = [ common.rm-command ] ; +actions piecemeal archive +{ + $(RM) "$(<)" + $(AR) $(AROPTIONS) rc "$(<:W)" "$(>:W)" +} diff --git a/scripts/travis-emscripten/install_deps.sh b/scripts/travis-emscripten/install_deps.sh index fc81851c2..7544da4e2 100755 --- a/scripts/travis-emscripten/install_deps.sh +++ b/scripts/travis-emscripten/install_deps.sh @@ -29,6 +29,8 @@ set -ev +SCRIPT_DIR="$(realpath $(dirname $0))" + echo -en 'travis_fold:start:installing_dependencies\\r' test -e boost_1_70_0_install/include/boost/version.hpp || ( rm -rf boost_1_70_0 @@ -40,8 +42,7 @@ tar -xzf boost.tar.gz rm boost.tar.gz cd boost_1_70_0 ./bootstrap.sh -wget -q 'https://raw.githubusercontent.com/tee3/boost-build-emscripten/master/emscripten.jam' -test "$(shasum emscripten.jam)" = "a7e13fc2c1e53b0e079ef440622f879aa6da3049 emscripten.jam" +cp "${SCRIPT_DIR}/emscripten.jam" . echo "using emscripten : : em++ ;" >> project-config.jam ) cd .. diff --git a/test/externalTests/zeppelin.sh b/test/externalTests/zeppelin.sh index 7c932786e..49b6c3e42 100755 --- a/test/externalTests/zeppelin.sh +++ b/test/externalTests/zeppelin.sh @@ -36,7 +36,6 @@ function zeppelin_test truffle_setup https://github.com/erak/openzeppelin-contracts.git master_060 run_install install_fn - truffle_run_test compile_fn test_fn } diff --git a/test/liblll/Compiler.cpp b/test/liblll/Compiler.cpp index 3e2b38889..d44ccb49f 100644 --- a/test/liblll/Compiler.cpp +++ b/test/liblll/Compiler.cpp @@ -193,6 +193,8 @@ BOOST_AUTO_TEST_CASE(valid_opcodes_functional) "4300", "4400", "4500", + "4600", + "4700", "60005000", "60005100", "600060005200", @@ -420,6 +422,8 @@ BOOST_AUTO_TEST_CASE(valid_opcodes_asm) "4300", "4400", "4500", + "4600", + "4700", "60005000", "60005100", "600060005200", @@ -559,6 +563,8 @@ BOOST_AUTO_TEST_CASE(valid_opcodes_asm) "(asm NUMBER)", "(asm DIFFICULTY)", "(asm GASLIMIT)", + "(asm CHAINID)", + "(asm SELFBALANCE)", "(asm 0 POP)", "(asm 0 MLOAD)", "(asm 0 0 MSTORE)", diff --git a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol index d846dde0f..a37a7e64e 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol @@ -53,6 +53,5 @@ contract MyConc{ // ---- // Warning: (773-792): This declaration shadows an existing declaration. // Warning: (1009-1086): Function state mutability can be restricted to view -// Warning: (874-879): Underflow (resulting value less than 0) happens here. -// Warning: (874-879): Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning: (985-1002): Underflow (resulting value less than 0) happens here. // Warning: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol index 2053fff48..29f15c689 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol @@ -137,4 +137,3 @@ contract PropagateThroughReturnValue { // Warning: (748-755): Assertion checker does not yet support this expression. // Warning: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer // Warning: (748-770): Assertion checker does not yet implement such assignments. -// Warning: (849-905): Assertion checker does not yet support constructors. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol b/test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol index 8e5c57cf6..f1ea2e053 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol @@ -13,5 +13,3 @@ contract B is A { } } // ---- -// Warning: (56-90): Assertion checker does not yet support constructors. -// Warning: (113-151): Assertion checker does not yet support constructors. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol index ebc674edf..9a772b27e 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol @@ -1,6 +1,16 @@ pragma experimental SMTChecker; -contract C { constructor(uint) public {} } -contract A is C { constructor() C(2) public {} } +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract A is C { + constructor() C(2) public { + assert(a == 2); + assert(a == 3); + } +} // ---- -// Warning: (45-72): Assertion checker does not yet support constructors. -// Warning: (93-121): Assertion checker does not yet support constructors. +// Warning: (166-180): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol index 0b96c566c..b5a3f36d8 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol @@ -1,10 +1,7 @@ pragma experimental SMTChecker; -contract C { constructor(uint) public {} } -contract A is C { constructor() C(2) public {} } -contract B is C { constructor() C(3) public {} } -contract J is C { constructor() C(3) public {} } +contract C { uint a; constructor(uint x) public { a = x; } } +contract A is C { constructor() C(2) public { assert(a == 2); } } +contract B is C { constructor() C(3) public { assert(a == 3); } } +contract J is C { constructor() C(3) public { assert(a == 4); } } // ---- -// Warning: (45-72): Assertion checker does not yet support constructors. -// Warning: (93-121): Assertion checker does not yet support constructors. -// Warning: (142-170): Assertion checker does not yet support constructors. -// Warning: (191-219): Assertion checker does not yet support constructors. +// Warning: (271-285): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol new file mode 100644 index 000000000..4db811ee2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract B is C { + constructor(uint x) public { + a = x; + } +} + +contract A is B { + constructor(uint x) B(x) C(x + 2) public { + assert(a == x); + assert(a == x + 1); + } +} +// ---- +// Warning: (244-262): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol new file mode 100644 index 000000000..63a229614 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract B is C { + constructor(uint x) public { + a = x; + } +} + +contract A is B { + constructor(uint x) C(x + 2) B(x + 1) public { + assert(a == x + 1); + } +} +// ---- +// Warning: (212-217): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (242-247): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol new file mode 100644 index 000000000..44e600a0d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract B1 is C { + constructor(uint x) public { + a = x; + } +} + +contract B2 is C { + constructor(uint x) C(x + 2) public { + a = x; + } +} + +contract A is B2, B1 { + constructor(uint x) B2(x) B1(x) public { + assert(a == x); + assert(a == x + 1); + } +} +// ---- +// Warning: (205-210): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (321-339): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol new file mode 100644 index 000000000..03922d16e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract B1 is C { + constructor(uint x) public { + a = x; + } +} + +contract B2 is C { + constructor(uint x) C(x + 2) public { + a = x; + } +} + +contract A is B2, B1 { + constructor(uint x) B1(x) B2(x) public { + assert(a == x); + assert(a == x + 1); + } +} +// ---- +// Warning: (205-210): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (321-339): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol new file mode 100644 index 000000000..429b5d135 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol @@ -0,0 +1,34 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract B1 is C { + uint b1; + constructor(uint x) public { + b1 = x + a; + } +} + +contract B2 is C { + uint b2; + constructor(uint x) C(x + 2) public { + b2 = x + a; + } +} + +contract A is B2, B1 { + constructor(uint x) B2(x) B1(x) public { + assert(b1 == b2); + assert(b1 != b2); + } +} +// ---- +// Warning: (165-170): Underflow (resulting value less than 0) happens here +// Warning: (165-170): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (253-258): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (353-369): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol new file mode 100644 index 000000000..7819019e9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor() public { + a = 2; + } +} + +contract B is C { +} + +contract B2 is C { +} + +contract A is B, B2 { + constructor(uint x) public { + assert(a == 2); + assert(a == 3); + } +} +// ---- +// Warning: (171-177): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning: (208-222): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle_empty_base.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle_empty_base.sol new file mode 100644 index 000000000..7c35f4fae --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle_empty_base.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor() public { + a = 2; + } +} + +contract B is C { +} + +contract B2 is C { + constructor() public { + assert(a == 2); + } +} + +contract A is B, B2 { +} diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol new file mode 100644 index 000000000..2c7d8827d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; +contract F { + uint a; + constructor() public { + a = 2; + } +} + +contract E is F {} +contract D is E {} +contract C is D {} +contract B is C {} + +contract A is B { + constructor(uint x) public { + assert(a == 2); + assert(a == 3); + } +} +// ---- +// Warning: (201-207): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning: (238-252): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol new file mode 100644 index 000000000..fbd3436dc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor() public { + a = 2; + } +} + +contract B is C { +} + +contract A is B { + constructor(uint x) B() public { + assert(a == 2); + assert(a == 3); + } +} +// ---- +// Warning: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning: (186-200): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol new file mode 100644 index 000000000..8b94c53a9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor() public { + a = 2; + } +} + +contract B is C { +} + +contract A is B { + constructor(uint x) public { + assert(a == 3); + } +} +// ---- +// Warning: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning: (164-178): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol new file mode 100644 index 000000000..ec534a431 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; +contract F { + uint a; + constructor() public { + a = 2; + } +} + +contract E is F {} +contract D is E { + constructor() public { + a = 3; + } +} +contract C is D {} +contract B is C { + constructor() public { + a = 4; + } +} + +contract A is B { + constructor(uint x) public { + assert(a == 4); + assert(a == 5); + } +} +// ---- +// Warning: (275-281): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning: (312-326): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_empty_base.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_empty_base.sol new file mode 100644 index 000000000..71cbbd13c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_empty_base.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; +contract F { + uint a; + constructor() public { + a = 2; + } +} + +contract E is F {} +contract D is E { + constructor() public { + a = 3; + } +} +contract C is D {} +contract B is C { + constructor() public { + assert(a == 3); + a = 4; + } +} + +contract A is B { +} diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol new file mode 100644 index 000000000..eaa7c5dc4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol @@ -0,0 +1,35 @@ +pragma experimental SMTChecker; +contract F { + uint a; + constructor() public { + uint f = 2; + a = f; + } +} + +contract E is F {} +contract D is E { + constructor() public { + uint d = 3; + a = d; + } +} +contract C is D {} +contract B is C { + constructor() public { + uint b = 4; + a = b; + } +} + +contract A is B { + constructor(uint x) public { + uint a1 = 4; + uint a2 = 5; + assert(a == a1); + assert(a == a2); + } +} +// ---- +// Warning: (317-323): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning: (385-400): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol new file mode 100644 index 000000000..66380328d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; +contract F { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract E is F {} +contract D is E { + constructor() public { + a = 3; + } +} +contract C is D {} +contract B is C { + constructor(uint x) F(x + 1) public { + } +} + +contract A is B { + constructor(uint x) B(x) public { + assert(a == 3); + assert(a == 4); + } +} +// ---- +// Warning: (234-239): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (329-343): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol new file mode 100644 index 000000000..12890009a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; +contract F { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract E is F {} +contract D is E { + constructor() public { + a = 3; + } +} +contract C is D {} +contract B is C { + constructor() F(1) public { + assert(a == 3); + assert(a == 2); + } +} + +contract A is B { +} +// ---- +// Warning: (260-274): Assertion violation happens here +// Warning: (260-274): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol new file mode 100644 index 000000000..3feff4dae --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C { + uint a; + modifier n { _; a = 7; } + constructor(uint x) n public { + a = x; + } +} + +contract A is C { + modifier m { a = 5; _; } + constructor() C(2) public { + assert(a == 4); + } +} +// ---- +// Warning: (202-216): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol new file mode 100644 index 000000000..a607a9556 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract A is C { + constructor() C(2) public { + assert(a == 0); + assert(C.a == 0); + } +} +// ---- +// Warning: (148-162): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_simple.sol b/test/libsolidity/smtCheckerTests/functions/constructor_simple.sol new file mode 100644 index 000000000..b4f68e33a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_simple.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + uint x; + + constructor() public { + assert(x == 0); + x = 10; + } + + function f(uint y) public view { + assert(y == x); + } +} +// ---- +// Warning: (148-162): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol new file mode 100644 index 000000000..1df298f13 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + uint x = 5; + + constructor() public { + assert(x == 5); + x = 10; + } + + function f(uint y) public view { + assert(y == x); + } +} +// ---- +// Warning: (152-166): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol new file mode 100644 index 000000000..e7349e044 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract B { + uint x = 5; +} + +contract C is B { + constructor() public { + assert(x == 5); + x = 10; + } + + function f(uint y) public view { + assert(y == x); + } +} +// ---- +// Warning: (172-186): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol new file mode 100644 index 000000000..214eb1cd6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C { + uint x = 5; + + constructor(uint a, uint b) public { + assert(x == 5); + x = a + b; + } + + function f(uint y) public view { + assert(y == x); + } +} +// ---- +// Warning: (169-183): Assertion violation happens here +// Warning: (122-127): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_this.sol b/test/libsolidity/smtCheckerTests/functions/constructor_this.sol new file mode 100644 index 000000000..0a308a166 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/constructor_this.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure {} + constructor() public { + C c = this; + c.f(); // this does not warn now, but should warn in the future + this.f(); + (this).f(); + } +} +// ---- +// Warning: (204-208): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed. +// Warning: (223-227): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol new file mode 100644 index 000000000..66380328d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; +contract F { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract E is F {} +contract D is E { + constructor() public { + a = 3; + } +} +contract C is D {} +contract B is C { + constructor(uint x) F(x + 1) public { + } +} + +contract A is B { + constructor(uint x) B(x) public { + assert(a == 3); + assert(a == 4); + } +} +// ---- +// Warning: (234-239): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (329-343): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init.sol new file mode 100644 index 000000000..bef807b81 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C { + uint x = 2; + constructor () public { + assert(x == 2); + assert(x == 3); + } +} +// ---- +// Warning: (104-118): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_base.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_base.sol new file mode 100644 index 000000000..179b2c6c6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_base.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C { + uint x = 2; +} + +contract D is C { + constructor() public { + assert(x == 2); + assert(x == 3); + } +} +// ---- +// Warning: (124-138): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain.sol new file mode 100644 index 000000000..e43d9e73a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract A { + uint x = 1; +} + +contract B is A { + constructor() public { x = 2; } +} + +contract C is B { + constructor() public { x = 3; } +} + +contract D is C { + constructor() public { + assert(x == 3); + assert(x == 2); + } +} +// ---- +// Warning: (232-246): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_alternate.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_alternate.sol new file mode 100644 index 000000000..ee1b098a5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_alternate.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract A { + uint x = 1; +} + +contract B is A { + constructor() public { x = 2; } +} + +contract C is B { +} + +contract D is C { + constructor() public { + assert(x == 2); + assert(x == 3); + } +} +// ---- +// Warning: (199-213): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol new file mode 100644 index 000000000..edc6eeb33 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract B is C { + uint b; + constructor(uint x) public { + b = a + x; + } +} + +contract A is B { + constructor(uint x) B(x) C(x + 2) public { + assert(a == x + 2); + assert(b == x + x + 2); + assert(a == x + 5); + } +} + +// ---- +// Warning: (162-167): Underflow (resulting value less than 0) happens here +// Warning: (162-167): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (287-305): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol new file mode 100644 index 000000000..7efffde55 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; +contract C { + uint a; + constructor(uint x) public { + a = x; + } +} + +contract B is C { + uint b; + constructor(uint x) public { + b = x + 10; + } +} + +contract A is B { + constructor(uint x) B(x) C(x + 2) public { + assert(a == x + 2); + assert(b == x + 10); + assert(b == x + 5); + } +} + +// ---- +// Warning: (162-168): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning: (285-303): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond.sol new file mode 100644 index 000000000..65fddfe52 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract A { + uint x = 2; +} + +contract B is A { +} + +contract C is A { +} + +contract D is B, C { + constructor() public { + assert(x == 2); + assert(x == 3); + } +} +// ---- +// Warning: (169-183): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol new file mode 100644 index 000000000..5a28788c4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract A { + uint x = 1; +} + +contract B is A { + constructor() public { x = 2; } +} + +contract C is A { + constructor() public { x = 3; } +} + +contract D is B, C { + constructor() public { + assert(x == 3); + assert(x == 4); + } +} +// ---- +// Warning: (235-249): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_function_call.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_function_call.sol new file mode 100644 index 000000000..91798ec0c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_function_call.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C { + uint x = f(2); + constructor () public { + assert(x == 2); + } + + function f(uint y) internal view returns (uint) { + assert(y > 0); + assert(x == 0); + return y; + } +} +// ---- +// Warning: (162-175): Assertion violation happens here +// Warning: (179-193): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/inheritance/functions_1.sol b/test/libsolidity/smtCheckerTests/inheritance/functions_1.sol index a5ac2ed61..0a11df6c4 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/functions_1.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/functions_1.sol @@ -15,7 +15,7 @@ contract A { // 2 warnings, B.f and A.g contract B is A { function f() public view override { - assert(x == 0); + assert(x == 1); } } // ---- diff --git a/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol b/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol index d78ffe9b5..d462e7c9a 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/functions_2.sol @@ -17,7 +17,7 @@ contract B is A { uint y; function f() public view override { - assert(x == 0); + assert(x == 1); } } // ---- diff --git a/test/libsolidity/smtCheckerTests/inheritance/functions_3.sol b/test/libsolidity/smtCheckerTests/inheritance/functions_3.sol index 7f64fea31..a2d1d9f3e 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/functions_3.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/functions_3.sol @@ -17,10 +17,10 @@ contract B is A { uint y; function f() public view virtual override { - assert(x == 0); + assert(x == 1); } function h() public view { - assert(x == 2); + assert(x == 1); } } @@ -29,10 +29,10 @@ contract C is B { uint z; function f() public view override { - assert(x == 0); + assert(x == 1); } function i() public view { - assert(x == 0); + assert(x == 1); } } // ---- diff --git a/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol new file mode 100644 index 000000000..1eeb4e640 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract A { + uint x; + constructor (uint y) public { assert(x == 0); x = y; } +} + +contract B is A { + constructor () A(2) public { assert(x == 2); } +} + +contract C is B { + function f() public view { + assert(x == 2); + } +} diff --git a/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol b/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol new file mode 100644 index 000000000..c724b7289 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +contract A { + uint x; + function h() public view { + assert(x == 0); + } +} + +contract B is A { + function g() public view { + assert(x == 0); + } +} + +contract C is B { + function f() public view { + assert(x == 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index b9f3c80ba..c20780065 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -3,12 +3,15 @@ pragma experimental "ABIEncoderV2"; contract C { struct S { uint x; uint[] b; } - function f() public pure returns (S memory, bytes memory) { - return abi.decode("abc", (S, bytes)); + function f() public pure returns (S memory, bytes memory, uint[][2] memory) { + return abi.decode("abc", (S, bytes, uint[][2])); } } // ---- // Warning: (151-159): Assertion checker does not yet support the type of this variable. -// Warning: (188-191): Assertion checker does not yet implement type abi -// Warning: (207-208): Assertion checker does not yet implement type type(struct C.S storage pointer) -// Warning: (188-217): Assertion checker does not yet implement this type of function call. +// Warning: (206-209): Assertion checker does not yet implement type abi +// Warning: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer) +// Warning: (235-241): Assertion checker does not yet implement type type(uint256[] memory) +// Warning: (235-241): Assertion checker does not yet implement this expression. +// Warning: (235-244): Assertion checker does not yet implement type type(uint256[] memory[2] memory) +// Warning: (206-246): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/data_location_in_function_type.sol b/test/libsolidity/smtCheckerTests/types/data_location_in_function_type.sol new file mode 100644 index 000000000..9aa72ea7d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/data_location_in_function_type.sol @@ -0,0 +1,5 @@ +pragma experimental SMTChecker; +library L { + struct Nested { uint y; } + function c(function(Nested memory) external returns (uint)[] storage) external pure {} +} diff --git a/test/libsolidity/smtCheckerTests/types/function_type_array_as_reference_type.sol b/test/libsolidity/smtCheckerTests/types/function_type_array_as_reference_type.sol new file mode 100644 index 000000000..2500d3ec7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/function_type_array_as_reference_type.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + struct Nested { uint y; } + // ensure that we consider array of function pointers as reference type + function b(function(Nested memory) external returns (uint)[] storage) internal pure {} + function c(function(Nested memory) external returns (uint)[] memory) public pure {} + function d(function(Nested memory) external returns (uint)[] calldata) external pure {} +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol b/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol new file mode 100644 index 000000000..f004b5514 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C { + function(uint) external returns (uint)[] public x; + function(uint) internal returns (uint)[10] y; + function f() view public { + function(uint) returns (uint)[10] memory a; + function(uint) returns (uint)[10] storage b = y; + function(uint) external returns (uint)[] memory c; + c = new function(uint) external returns (uint)[](200); + a; b; + } +} +// ---- +// Warning: (361-410): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/mapping_and_array_of_functions.sol b/test/libsolidity/smtCheckerTests/types/mapping_and_array_of_functions.sol new file mode 100644 index 000000000..a10559ece --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/mapping_and_array_of_functions.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; +contract test { + mapping (address => function() internal returns (uint)) a; + mapping (address => function() external) b; + mapping (address => function() external[]) c; + function() external[] d; +}