From 467cbf92bc2f506df0f04cd485daaa1f7ff73525 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 4 Aug 2021 18:38:10 +0200 Subject: [PATCH 01/29] Only provide code generator to CodeTransform. --- libsolidity/codegen/CompilerContext.cpp | 2 +- libsolidity/codegen/ContractCompiler.cpp | 16 ++++++---------- libyul/backends/evm/AsmCodeGen.cpp | 4 ++-- libyul/backends/evm/AsmCodeGen.h | 2 +- libyul/backends/evm/EVMCodeTransform.cpp | 14 +++++++------- libyul/backends/evm/EVMCodeTransform.h | 10 +++++----- 6 files changed, 22 insertions(+), 26 deletions(-) diff --git a/libsolidity/codegen/CompilerContext.cpp b/libsolidity/codegen/CompilerContext.cpp index 291bbc255..3a939dcd7 100644 --- a/libsolidity/codegen/CompilerContext.cpp +++ b/libsolidity/codegen/CompilerContext.cpp @@ -520,7 +520,7 @@ void CompilerContext::appendInlineAssembly( analysisInfo, *m_asm, m_evmVersion, - identifierAccess, + identifierAccess.generateCode, _system, _optimiserSettings.optimizeStackAllocation ); diff --git a/libsolidity/codegen/ContractCompiler.cpp b/libsolidity/codegen/ContractCompiler.cpp index fca076b65..378179d5e 100644 --- a/libsolidity/codegen/ContractCompiler.cpp +++ b/libsolidity/codegen/ContractCompiler.cpp @@ -702,15 +702,11 @@ bool ContractCompiler::visit(FunctionDefinition const& _function) bool ContractCompiler::visit(InlineAssembly const& _inlineAssembly) { unsigned startStackHeight = m_context.stackHeight(); - yul::ExternalIdentifierAccess identifierAccess; - identifierAccess.resolve = [&](yul::Identifier const& _identifier, yul::IdentifierContext, bool) - { - auto ref = _inlineAssembly.annotation().externalReferences.find(&_identifier); - if (ref == _inlineAssembly.annotation().externalReferences.end()) - return numeric_limits::max(); - return ref->second.valueSize; - }; - identifierAccess.generateCode = [&](yul::Identifier const& _identifier, yul::IdentifierContext _context, yul::AbstractAssembly& _assembly) + yul::ExternalIdentifierAccess::CodeGenerator identifierAccessCodeGen = [&]( + yul::Identifier const& _identifier, + yul::IdentifierContext _context, + yul::AbstractAssembly& _assembly + ) { auto ref = _inlineAssembly.annotation().externalReferences.find(&_identifier); solAssert(ref != _inlineAssembly.annotation().externalReferences.end(), ""); @@ -918,7 +914,7 @@ bool ContractCompiler::visit(InlineAssembly const& _inlineAssembly) *analysisInfo, *m_context.assemblyPtr(), m_context.evmVersion(), - identifierAccess, + identifierAccessCodeGen, false, m_optimiserSettings.optimizeStackAllocation ); diff --git a/libyul/backends/evm/AsmCodeGen.cpp b/libyul/backends/evm/AsmCodeGen.cpp index bda3ad9e7..5c7865c01 100644 --- a/libyul/backends/evm/AsmCodeGen.cpp +++ b/libyul/backends/evm/AsmCodeGen.cpp @@ -37,7 +37,7 @@ void CodeGenerator::assemble( AsmAnalysisInfo& _analysisInfo, evmasm::Assembly& _assembly, langutil::EVMVersion _evmVersion, - ExternalIdentifierAccess const& _identifierAccess, + ExternalIdentifierAccess::CodeGenerator _identifierAccessCodeGen, bool _useNamedLabelsForFunctions, bool _optimizeStackAllocation ) @@ -51,7 +51,7 @@ void CodeGenerator::assemble( EVMDialect::strictAssemblyForEVM(_evmVersion), builtinContext, _optimizeStackAllocation, - _identifierAccess, + _identifierAccessCodeGen, _useNamedLabelsForFunctions ); transform(_parsedData); diff --git a/libyul/backends/evm/AsmCodeGen.h b/libyul/backends/evm/AsmCodeGen.h index 35db4e7a0..b79338074 100644 --- a/libyul/backends/evm/AsmCodeGen.h +++ b/libyul/backends/evm/AsmCodeGen.h @@ -44,7 +44,7 @@ public: AsmAnalysisInfo& _analysisInfo, evmasm::Assembly& _assembly, langutil::EVMVersion _evmVersion, - ExternalIdentifierAccess const& _identifierAccess = ExternalIdentifierAccess(), + ExternalIdentifierAccess::CodeGenerator _identifierAccess = {}, bool _useNamedLabelsForFunctions = false, bool _optimizeStackAllocation = false ); diff --git a/libyul/backends/evm/EVMCodeTransform.cpp b/libyul/backends/evm/EVMCodeTransform.cpp index bc41eb9b2..c837c8b1a 100644 --- a/libyul/backends/evm/EVMCodeTransform.cpp +++ b/libyul/backends/evm/EVMCodeTransform.cpp @@ -61,7 +61,7 @@ CodeTransform::CodeTransform( bool _allowStackOpt, EVMDialect const& _dialect, BuiltinContext& _builtinContext, - ExternalIdentifierAccess _identifierAccess, + ExternalIdentifierAccess::CodeGenerator _identifierAccessCodeGen, bool _useNamedLabelsForFunctions, shared_ptr _context, vector _delayedReturnVariables, @@ -73,7 +73,7 @@ CodeTransform::CodeTransform( m_builtinContext(_builtinContext), m_allowStackOpt(_allowStackOpt), m_useNamedLabelsForFunctions(_useNamedLabelsForFunctions), - m_identifierAccess(move(_identifierAccess)), + m_identifierAccessCodeGen(move(_identifierAccessCodeGen)), m_context(move(_context)), m_delayedReturnVariables(move(_delayedReturnVariables)), m_functionExitLabel(_functionExitLabel) @@ -292,10 +292,10 @@ void CodeTransform::operator()(Identifier const& _identifier) return; } yulAssert( - m_identifierAccess.generateCode, + m_identifierAccessCodeGen, "Identifier not found and no external access available." ); - m_identifierAccess.generateCode(_identifier, IdentifierContext::RValue, m_assembly); + m_identifierAccessCodeGen(_identifier, IdentifierContext::RValue, m_assembly); } void CodeTransform::operator()(Literal const& _literal) @@ -391,7 +391,7 @@ void CodeTransform::operator()(FunctionDefinition const& _function) m_allowStackOpt, m_dialect, m_builtinContext, - m_identifierAccess, + m_identifierAccessCodeGen, m_useNamedLabelsForFunctions, m_context, _function.returnVariables, @@ -740,10 +740,10 @@ void CodeTransform::generateAssignment(Identifier const& _variableName) else { yulAssert( - m_identifierAccess.generateCode, + m_identifierAccessCodeGen, "Identifier not found and no external access available." ); - m_identifierAccess.generateCode(_variableName, IdentifierContext::LValue, m_assembly); + m_identifierAccessCodeGen(_variableName, IdentifierContext::LValue, m_assembly); } } diff --git a/libyul/backends/evm/EVMCodeTransform.h b/libyul/backends/evm/EVMCodeTransform.h index 894a6d077..8bbd3b818 100644 --- a/libyul/backends/evm/EVMCodeTransform.h +++ b/libyul/backends/evm/EVMCodeTransform.h @@ -65,7 +65,7 @@ class CodeTransform { public: /// Create the code transformer. - /// @param _identifierAccess used to resolve identifiers external to the inline assembly + /// @param _identifierAccessCodeGen used to generate code for identifiers external to the inline assembly /// As a side-effect of its construction, translates the Yul code and appends it to the /// given assembly. /// Throws StackTooDeepError if a variable is not accessible or if a function has too @@ -77,7 +77,7 @@ public: EVMDialect const& _dialect, BuiltinContext& _builtinContext, bool _allowStackOpt = false, - ExternalIdentifierAccess const& _identifierAccess = ExternalIdentifierAccess(), + ExternalIdentifierAccess::CodeGenerator const& _identifierAccessCodeGen = {}, bool _useNamedLabelsForFunctions = false ): CodeTransform( _assembly, @@ -86,7 +86,7 @@ public: _allowStackOpt, _dialect, _builtinContext, - _identifierAccess, + _identifierAccessCodeGen, _useNamedLabelsForFunctions, nullptr, {}, @@ -107,7 +107,7 @@ protected: bool _allowStackOpt, EVMDialect const& _dialect, BuiltinContext& _builtinContext, - ExternalIdentifierAccess _identifierAccess, + ExternalIdentifierAccess::CodeGenerator _identifierAccessCodeGen, bool _useNamedLabelsForFunctions, std::shared_ptr _context, std::vector _delayedReturnVariables, @@ -193,7 +193,7 @@ private: BuiltinContext& m_builtinContext; bool const m_allowStackOpt = true; bool const m_useNamedLabelsForFunctions = false; - ExternalIdentifierAccess m_identifierAccess; + ExternalIdentifierAccess::CodeGenerator m_identifierAccessCodeGen; std::shared_ptr m_context; /// Set of variables whose reference counter has reached zero, From 0112fed73b29f1ffdb91455860a3d2af41aaebd6 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 4 Aug 2021 13:48:39 +0200 Subject: [PATCH 02/29] Yul: Fix cleanup for left shift of bytes types. --- libsolidity/codegen/YulUtilFunctions.cpp | 2 +- .../operators/shifts/shift_bytes_cleanup_viaYul.sol | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/libsolidity/codegen/YulUtilFunctions.cpp b/libsolidity/codegen/YulUtilFunctions.cpp index bd86dc9c2..3113330f8 100644 --- a/libsolidity/codegen/YulUtilFunctions.cpp +++ b/libsolidity/codegen/YulUtilFunctions.cpp @@ -445,7 +445,7 @@ string YulUtilFunctions::typedShiftLeftFunction(Type const& _type, Type const& _ Whiskers(R"( function (value, bits) -> result { bits := (bits) - result := ((bits, value)) + result := ((bits, (value))) } )") ("functionName", functionName) diff --git a/test/libsolidity/semanticTests/operators/shifts/shift_bytes_cleanup_viaYul.sol b/test/libsolidity/semanticTests/operators/shifts/shift_bytes_cleanup_viaYul.sol index 2c605ffd8..68a370454 100644 --- a/test/libsolidity/semanticTests/operators/shifts/shift_bytes_cleanup_viaYul.sol +++ b/test/libsolidity/semanticTests/operators/shifts/shift_bytes_cleanup_viaYul.sol @@ -13,8 +13,8 @@ contract C { } } // ==== -// compileViaYul: true // compileToEwasm: also +// compileViaYul: true // ---- -// l(uint8): 64 -> 0x3930313233343536373839306162636465000000000000000000000000000000 +// l(uint8): 64 -> 0x3930313233343536373839300000000000000000000000000000000000000000 // r(uint8): 64 -> 0x313233343536373839303132000000000000000000000000 From 6b888b531b91291b48d480db3f532f19d22e842c Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 4 Aug 2021 15:48:10 +0200 Subject: [PATCH 03/29] Refactor conversion function. --- libsolidity/codegen/YulUtilFunctions.cpp | 50 +++++++------------ .../yul_source_locations/output.json | 28 +++++++---- .../various/external_types_in_calls.sol | 2 +- 3 files changed, 37 insertions(+), 43 deletions(-) diff --git a/libsolidity/codegen/YulUtilFunctions.cpp b/libsolidity/codegen/YulUtilFunctions.cpp index bd86dc9c2..cd47d417a 100644 --- a/libsolidity/codegen/YulUtilFunctions.cpp +++ b/libsolidity/codegen/YulUtilFunctions.cpp @@ -3258,6 +3258,7 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to) switch (fromCategory) { case Type::Category::Address: + case Type::Category::Contract: body = Whiskers("converted := (value)") ("convert", conversionFunction(IntegerType(160), _to)) @@ -3265,61 +3266,44 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to) break; case Type::Category::Integer: case Type::Category::RationalNumber: - case Type::Category::Contract: { + solAssert(_from.mobileType(), ""); if (RationalNumberType const* rational = dynamic_cast(&_from)) - solUnimplementedAssert(!rational->isFractional(), "Not yet implemented - FixedPointType."); + if (rational->isFractional()) + solAssert(toCategory == Type::Category::FixedPoint, ""); + if (toCategory == Type::Category::FixedBytes) { - solAssert( - fromCategory == Type::Category::Integer || fromCategory == Type::Category::RationalNumber, - "Invalid conversion to FixedBytesType requested." - ); FixedBytesType const& toBytesType = dynamic_cast(_to); body = Whiskers("converted := ((value))") - ("shiftLeft", shiftLeftFunction(256 - toBytesType.numBytes() * 8)) - ("clean", cleanupFunction(_from)) - .render(); + ("shiftLeft", shiftLeftFunction(256 - toBytesType.numBytes() * 8)) + ("clean", cleanupFunction(_from)) + .render(); } else if (toCategory == Type::Category::Enum) - { - solAssert(_from.mobileType(), ""); body = Whiskers("converted := ((value))") ("cleanEnum", cleanupFunction(_to)) - // "mobileType()" returns integer type for rational - ("cleanInt", cleanupFunction(*_from.mobileType())) + ("cleanInt", cleanupFunction(_from)) .render(); - } else if (toCategory == Type::Category::FixedPoint) solUnimplemented("Not yet implemented - FixedPointType."); - else if (toCategory == Type::Category::Address) + else if (toCategory == Type::Category::Address || toCategory == Type::Category::Contract) body = Whiskers("converted := (value)") - ("convert", conversionFunction(_from, IntegerType(160))) - .render(); - else + ("convert", conversionFunction(_from, IntegerType(160))) + .render(); + else if (toCategory == Type::Category::Integer) { - solAssert( - toCategory == Type::Category::Integer || - toCategory == Type::Category::Contract, - ""); - IntegerType const addressType(160); - IntegerType const& to = - toCategory == Type::Category::Integer ? - dynamic_cast(_to) : - addressType; + IntegerType const& to = dynamic_cast(_to); // Clean according to the "to" type, except if this is // a widening conversion. IntegerType const* cleanupType = &to; - if (fromCategory != Type::Category::RationalNumber) + if (fromCategory == Type::Category::Integer) { - IntegerType const& from = - fromCategory == Type::Category::Integer ? - dynamic_cast(_from) : - addressType; + IntegerType const& from = dynamic_cast(_from); if (to.numBits() > from.numBits()) cleanupType = &from; } @@ -3328,6 +3312,8 @@ string YulUtilFunctions::conversionFunction(Type const& _from, Type const& _to) ("cleanInt", cleanupFunction(*cleanupType)) .render(); } + else + solAssert(false, ""); break; } case Type::Category::Bool: diff --git a/test/cmdlineTests/yul_source_locations/output.json b/test/cmdlineTests/yul_source_locations/output.json index f5f57a6d6..ae7d70556 100644 --- a/test/cmdlineTests/yul_source_locations/output.json +++ b/test/cmdlineTests/yul_source_locations/output.json @@ -275,11 +275,7 @@ object \"C_54\" { } function convert_t_contract$_C_$54_to_t_address(value) -> converted { - converted := convert_t_contract$_C_$54_to_t_uint160(value) - } - - function convert_t_contract$_C_$54_to_t_uint160(value) -> converted { - converted := cleanup_t_uint160(value) + converted := convert_t_uint160_to_t_address(value) } function convert_t_int256_to_t_int256(value) -> converted { @@ -290,6 +286,14 @@ object \"C_54\" { converted := cleanup_t_int256(value) } + function convert_t_uint160_to_t_address(value) -> converted { + converted := convert_t_uint160_to_t_uint160(value) + } + + function convert_t_uint160_to_t_uint160(value) -> converted { + converted := cleanup_t_uint160(value) + } + function extract_from_storage_value_dynamict_int256(slot_value, offset) -> value { value := cleanup_from_storage_t_int256(shift_right_unsigned_dynamic(mul(offset, 8), slot_value)) } @@ -875,11 +879,7 @@ object \"D_72\" { } function convert_t_contract$_C_$54_to_t_address(value) -> converted { - converted := convert_t_contract$_C_$54_to_t_uint160(value) - } - - function convert_t_contract$_C_$54_to_t_uint160(value) -> converted { - converted := cleanup_t_uint160(value) + converted := convert_t_uint160_to_t_address(value) } function convert_t_int256_to_t_int256(value) -> converted { @@ -890,6 +890,14 @@ object \"D_72\" { converted := cleanup_t_int256(value) } + function convert_t_uint160_to_t_address(value) -> converted { + converted := convert_t_uint160_to_t_uint160(value) + } + + function convert_t_uint160_to_t_uint160(value) -> converted { + converted := cleanup_t_uint160(value) + } + function extract_from_storage_value_dynamict_int256(slot_value, offset) -> value { value := cleanup_from_storage_t_int256(shift_right_unsigned_dynamic(mul(offset, 8), slot_value)) } diff --git a/test/libsolidity/semanticTests/various/external_types_in_calls.sol b/test/libsolidity/semanticTests/various/external_types_in_calls.sol index 941a06a91..4aee63b93 100644 --- a/test/libsolidity/semanticTests/various/external_types_in_calls.sol +++ b/test/libsolidity/semanticTests/various/external_types_in_calls.sol @@ -27,5 +27,5 @@ contract C { // compileViaYul: also // ---- // test() -> 9, 7 -// gas legacy: 121594 +// gas legacy: 125064 // t2() -> 9 From dc4620d2bec576c5ad9d512d168077b03f691450 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Thu, 5 Aug 2021 17:11:58 +0200 Subject: [PATCH 04/29] cmdlineTests.sh: Suppress message about empty output to get consistent output on release and pre-release builds --- test/cmdlineTests.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/test/cmdlineTests.sh b/test/cmdlineTests.sh index 582a7acde..b5742e3bb 100755 --- a/test/cmdlineTests.sh +++ b/test/cmdlineTests.sh @@ -169,6 +169,7 @@ EOF rm "$stdout_path.bak" else sed -i.bak -e '/^Warning: This is a pre-release compiler version, please do not use it in production./d' "$stderr_path" + sed -i.bak -e '/^Compiler run successful, no output requested\.$/d' "$stderr_path" sed -i.bak -e '/^Warning (3805): This is a pre-release compiler version, please do not use it in production./d' "$stderr_path" sed -i.bak -e 's/\(^[ ]*auxdata: \)0x[0-9a-f]*$/\1/' "$stdout_path" sed -i.bak -e 's/ Consider adding "pragma .*$//' "$stderr_path" From 2803dba9801f8bd1b1f6b9b0f6d4361d5d0634e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Thu, 5 Aug 2021 17:14:16 +0200 Subject: [PATCH 05/29] Add pragmas and SPDX comments to command-line tests to get cleaner error output --- .../combined_json_generated_sources/err | 5 --- .../combined_json_generated_sources/input.sol | 2 ++ test/cmdlineTests/dup_opt_peephole/err | 5 --- test/cmdlineTests/dup_opt_peephole/input.sol | 3 ++ test/cmdlineTests/dup_opt_peephole/output | 18 +++++----- .../keccak_optimization_low_runs/exit | 1 - test/cmdlineTests/message_format_utf8/err | 35 ++++++++----------- .../message_format_utf8/input.sol | 3 ++ .../model_checker_engine_none/err | 5 --- .../model_checker_engine_none/input.sol | 12 +++---- .../model_checker_targets_balance_chc/err | 2 -- .../input.sol | 8 +++-- .../err | 2 -- .../input.sol | 8 +++-- .../err | 2 -- .../input.sol | 8 +++-- .../model_checker_targets_pop_empty_bmc/err | 2 -- .../input.sol | 8 +++-- test/cmdlineTests/stdin/err | 5 --- test/cmdlineTests/stdin/stdin | 3 ++ test/cmdlineTests/too_long_line/err | 10 ++---- test/cmdlineTests/too_long_line/input.sol | 3 ++ .../too_long_line_both_sides_short/err | 10 ++---- .../too_long_line_both_sides_short/input.sol | 3 ++ test/cmdlineTests/too_long_line_edge_in/err | 10 ++---- .../too_long_line_edge_in/input.sol | 3 ++ test/cmdlineTests/too_long_line_edge_out/err | 10 ++---- .../too_long_line_edge_out/input.sol | 3 ++ .../cmdlineTests/too_long_line_left_short/err | 10 ++---- .../too_long_line_left_short/input.sol | 3 ++ test/cmdlineTests/too_long_line_multiline/err | 10 ++---- .../too_long_line_multiline/input.sol | 3 ++ .../too_long_line_right_short/err | 10 ++---- .../too_long_line_right_short/input.sol | 3 ++ 34 files changed, 95 insertions(+), 133 deletions(-) delete mode 100644 test/cmdlineTests/combined_json_generated_sources/err delete mode 100644 test/cmdlineTests/dup_opt_peephole/err delete mode 100644 test/cmdlineTests/keccak_optimization_low_runs/exit delete mode 100644 test/cmdlineTests/model_checker_engine_none/err delete mode 100644 test/cmdlineTests/model_checker_targets_balance_chc/err delete mode 100644 test/cmdlineTests/model_checker_targets_constant_condition_chc/err delete mode 100644 test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/err delete mode 100644 test/cmdlineTests/model_checker_targets_pop_empty_bmc/err delete mode 100644 test/cmdlineTests/stdin/err diff --git a/test/cmdlineTests/combined_json_generated_sources/err b/test/cmdlineTests/combined_json_generated_sources/err deleted file mode 100644 index c6113508b..000000000 --- a/test/cmdlineTests/combined_json_generated_sources/err +++ /dev/null @@ -1,5 +0,0 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> combined_json_generated_sources/input.sol - -Warning: Source file does not specify required compiler version! ---> combined_json_generated_sources/input.sol diff --git a/test/cmdlineTests/combined_json_generated_sources/input.sol b/test/cmdlineTests/combined_json_generated_sources/input.sol index b08878fb1..b99390dee 100644 --- a/test/cmdlineTests/combined_json_generated_sources/input.sol +++ b/test/cmdlineTests/combined_json_generated_sources/input.sol @@ -1,3 +1,5 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; pragma abicoder v2; contract C { diff --git a/test/cmdlineTests/dup_opt_peephole/err b/test/cmdlineTests/dup_opt_peephole/err deleted file mode 100644 index cfaa88dcf..000000000 --- a/test/cmdlineTests/dup_opt_peephole/err +++ /dev/null @@ -1,5 +0,0 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> dup_opt_peephole/input.sol - -Warning: Source file does not specify required compiler version! ---> dup_opt_peephole/input.sol diff --git a/test/cmdlineTests/dup_opt_peephole/input.sol b/test/cmdlineTests/dup_opt_peephole/input.sol index 1474a8f44..c8752d4a1 100644 --- a/test/cmdlineTests/dup_opt_peephole/input.sol +++ b/test/cmdlineTests/dup_opt_peephole/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C { fallback() external { assembly { diff --git a/test/cmdlineTests/dup_opt_peephole/output b/test/cmdlineTests/dup_opt_peephole/output index fec862428..593d330f8 100644 --- a/test/cmdlineTests/dup_opt_peephole/output +++ b/test/cmdlineTests/dup_opt_peephole/output @@ -1,7 +1,7 @@ ======= dup_opt_peephole/input.sol:C ======= EVM assembly: - /* "dup_opt_peephole/input.sol":0:111 contract C {... */ + /* "dup_opt_peephole/input.sol":60:171 contract C {... */ mstore(0x40, 0x80) callvalue dup1 @@ -23,7 +23,7 @@ tag_1: stop sub_0: assembly { - /* "dup_opt_peephole/input.sol":0:111 contract C {... */ + /* "dup_opt_peephole/input.sol":60:171 contract C {... */ mstore(0x40, 0x80) callvalue dup1 @@ -35,19 +35,19 @@ sub_0: assembly { revert tag_3: pop - /* "dup_opt_peephole/input.sol":74:75 0 */ + /* "dup_opt_peephole/input.sol":134:135 0 */ 0x00 - /* "dup_opt_peephole/input.sol":61:76 calldataload(0) */ + /* "dup_opt_peephole/input.sol":121:136 calldataload(0) */ calldataload - /* "dup_opt_peephole/input.sol":100:101 x */ + /* "dup_opt_peephole/input.sol":160:161 x */ dup1 - /* "dup_opt_peephole/input.sol":97:98 0 */ + /* "dup_opt_peephole/input.sol":157:158 0 */ 0x00 - /* "dup_opt_peephole/input.sol":90:102 sstore(0, x) */ + /* "dup_opt_peephole/input.sol":150:162 sstore(0, x) */ sstore - /* "dup_opt_peephole/input.sol":47:106 {... */ + /* "dup_opt_peephole/input.sol":107:166 {... */ pop - /* "dup_opt_peephole/input.sol":0:111 contract C {... */ + /* "dup_opt_peephole/input.sol":60:171 contract C {... */ stop auxdata: diff --git a/test/cmdlineTests/keccak_optimization_low_runs/exit b/test/cmdlineTests/keccak_optimization_low_runs/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/keccak_optimization_low_runs/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/message_format_utf8/err b/test/cmdlineTests/message_format_utf8/err index e14ed61e9..58d45127c 100644 --- a/test/cmdlineTests/message_format_utf8/err +++ b/test/cmdlineTests/message_format_utf8/err @@ -1,36 +1,29 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> message_format_utf8/input.sol - -Warning: Source file does not specify required compiler version! ---> message_format_utf8/input.sol - Warning: Statement has no effect. - --> message_format_utf8/input.sol:2:51: + --> message_format_utf8/input.sol:5:51: | -2 | /* ©©©©ﾩ©©©©© 2017 */ constructor () { unicode"©©©©ﾩ©©©©©" ; } +5 | /* ©©©©ﾩ©©©©© 2017 */ constructor () { unicode"©©©©ﾩ©©©©©" ; } | ^^^^^^^^^^^^^^^^^^^ Warning: Statement has no effect. - --> message_format_utf8/input.sol:6:25: + --> message_format_utf8/input.sol:9:25: | -6 | unicode"S = π × r²"; +9 | unicode"S = π × r²"; | ^^^^^^^^^^^^^^^^^^^ Warning: Statement has no effect. - --> message_format_utf8/input.sol:7:39: - | -7 | /* ₀₁₂₃₄⁵⁶⁷⁸⁹ */ unicode"∑ 1/n! ≈ 2.7"; // tabs in-between - | ^^^^^^^^^^^^^^^^^^^^^ + --> message_format_utf8/input.sol:10:39: + | +10 | /* ₀₁₂₃₄⁵⁶⁷⁸⁹ */ unicode"∑ 1/n! ≈ 2.7"; // tabs in-between + | ^^^^^^^^^^^^^^^^^^^^^ Warning: Statement has no effect. - --> message_format_utf8/input.sol:8:30: - | -8 | /* Ŀŏŗėɯ ïƥŝʉɱ */ unicode"μὴ χεῖρον βέλτιστον"; // tabs in-between and inside - | ^^^^^^^^^^ ^^^^^^ ^^^^^^^^^^ + --> message_format_utf8/input.sol:11:30: + | +11 | /* Ŀŏŗėɯ ïƥŝʉɱ */ unicode"μὴ χεῖρον βέλτιστον"; // tabs in-between and inside + | ^^^^^^^^^^ ^^^^^^ ^^^^^^^^^^ Warning: Function state mutability can be restricted to pure - --> message_format_utf8/input.sol:12:2: + --> message_format_utf8/input.sol:15:2: | -12 | function selector() public returns(uint) { // starts with tab +15 | function selector() public returns(uint) { // starts with tab | ^ (Relevant source part starts here and spans across multiple lines). - diff --git a/test/cmdlineTests/message_format_utf8/input.sol b/test/cmdlineTests/message_format_utf8/input.sol index faf18f139..d16aa8753 100644 --- a/test/cmdlineTests/message_format_utf8/input.sol +++ b/test/cmdlineTests/message_format_utf8/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract Foo { /* ©©©©ﾩ©©©©© 2017 */ constructor () { unicode"©©©©ﾩ©©©©©" ; } diff --git a/test/cmdlineTests/model_checker_engine_none/err b/test/cmdlineTests/model_checker_engine_none/err deleted file mode 100644 index 5b30ff59a..000000000 --- a/test/cmdlineTests/model_checker_engine_none/err +++ /dev/null @@ -1,5 +0,0 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> model_checker_engine_none/input.sol - -Warning: Source file does not specify required compiler version! ---> model_checker_engine_none/input.sol diff --git a/test/cmdlineTests/model_checker_engine_none/input.sol b/test/cmdlineTests/model_checker_engine_none/input.sol index f1fb96386..6f361b952 100644 --- a/test/cmdlineTests/model_checker_engine_none/input.sol +++ b/test/cmdlineTests/model_checker_engine_none/input.sol @@ -1,8 +1,8 @@ -// Removed to yield a warning, otherwise CI test fails with the expectation -// "no output requested" -//pragma solidity >=0.0; +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract test { - function f(uint x) public pure { + function f(uint x) public pure { assert(x > 0); - } -} \ No newline at end of file + } +} diff --git a/test/cmdlineTests/model_checker_targets_balance_chc/err b/test/cmdlineTests/model_checker_targets_balance_chc/err deleted file mode 100644 index e92707d91..000000000 --- a/test/cmdlineTests/model_checker_targets_balance_chc/err +++ /dev/null @@ -1,2 +0,0 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> model_checker_targets_balance_chc/input.sol diff --git a/test/cmdlineTests/model_checker_targets_balance_chc/input.sol b/test/cmdlineTests/model_checker_targets_balance_chc/input.sol index 8ec052a21..4b521b3de 100644 --- a/test/cmdlineTests/model_checker_targets_balance_chc/input.sol +++ b/test/cmdlineTests/model_checker_targets_balance_chc/input.sol @@ -1,7 +1,9 @@ +// SPDX-License-Identifier: GPL-3.0 pragma solidity >=0.0; + contract test { uint[] arr; - function f(address payable a, uint x) public { + function f(address payable a, uint x) public { require(x >= 0); --x; x + type(uint).max; @@ -10,5 +12,5 @@ contract test { assert(x > 0); arr.pop(); arr[x]; - } -} \ No newline at end of file + } +} diff --git a/test/cmdlineTests/model_checker_targets_constant_condition_chc/err b/test/cmdlineTests/model_checker_targets_constant_condition_chc/err deleted file mode 100644 index b6290c6bd..000000000 --- a/test/cmdlineTests/model_checker_targets_constant_condition_chc/err +++ /dev/null @@ -1,2 +0,0 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> model_checker_targets_constant_condition_chc/input.sol diff --git a/test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol b/test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol index 8ec052a21..4b521b3de 100644 --- a/test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol +++ b/test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol @@ -1,7 +1,9 @@ +// SPDX-License-Identifier: GPL-3.0 pragma solidity >=0.0; + contract test { uint[] arr; - function f(address payable a, uint x) public { + function f(address payable a, uint x) public { require(x >= 0); --x; x + type(uint).max; @@ -10,5 +12,5 @@ contract test { assert(x > 0); arr.pop(); arr[x]; - } -} \ No newline at end of file + } +} diff --git a/test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/err b/test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/err deleted file mode 100644 index b165198d1..000000000 --- a/test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/err +++ /dev/null @@ -1,2 +0,0 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> model_checker_targets_out_of_bounds_bmc/input.sol diff --git a/test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/input.sol b/test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/input.sol index 8ec052a21..4b521b3de 100644 --- a/test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/input.sol +++ b/test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/input.sol @@ -1,7 +1,9 @@ +// SPDX-License-Identifier: GPL-3.0 pragma solidity >=0.0; + contract test { uint[] arr; - function f(address payable a, uint x) public { + function f(address payable a, uint x) public { require(x >= 0); --x; x + type(uint).max; @@ -10,5 +12,5 @@ contract test { assert(x > 0); arr.pop(); arr[x]; - } -} \ No newline at end of file + } +} diff --git a/test/cmdlineTests/model_checker_targets_pop_empty_bmc/err b/test/cmdlineTests/model_checker_targets_pop_empty_bmc/err deleted file mode 100644 index 95a4225da..000000000 --- a/test/cmdlineTests/model_checker_targets_pop_empty_bmc/err +++ /dev/null @@ -1,2 +0,0 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> model_checker_targets_pop_empty_bmc/input.sol diff --git a/test/cmdlineTests/model_checker_targets_pop_empty_bmc/input.sol b/test/cmdlineTests/model_checker_targets_pop_empty_bmc/input.sol index 8ec052a21..4b521b3de 100644 --- a/test/cmdlineTests/model_checker_targets_pop_empty_bmc/input.sol +++ b/test/cmdlineTests/model_checker_targets_pop_empty_bmc/input.sol @@ -1,7 +1,9 @@ +// SPDX-License-Identifier: GPL-3.0 pragma solidity >=0.0; + contract test { uint[] arr; - function f(address payable a, uint x) public { + function f(address payable a, uint x) public { require(x >= 0); --x; x + type(uint).max; @@ -10,5 +12,5 @@ contract test { assert(x > 0); arr.pop(); arr[x]; - } -} \ No newline at end of file + } +} diff --git a/test/cmdlineTests/stdin/err b/test/cmdlineTests/stdin/err deleted file mode 100644 index c5254f827..000000000 --- a/test/cmdlineTests/stdin/err +++ /dev/null @@ -1,5 +0,0 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> - -Warning: Source file does not specify required compiler version! ---> diff --git a/test/cmdlineTests/stdin/stdin b/test/cmdlineTests/stdin/stdin index 2dde0d209..f123f6c8b 100644 --- a/test/cmdlineTests/stdin/stdin +++ b/test/cmdlineTests/stdin/stdin @@ -1 +1,4 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C {} diff --git a/test/cmdlineTests/too_long_line/err b/test/cmdlineTests/too_long_line/err index 802cac3cb..25620bd4c 100644 --- a/test/cmdlineTests/too_long_line/err +++ b/test/cmdlineTests/too_long_line/err @@ -1,11 +1,5 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> too_long_line/input.sol - -Warning: Source file does not specify required compiler version! ---> too_long_line/input.sol - Error: Identifier not found or not unique. - --> too_long_line/input.sol:2:164: + --> too_long_line/input.sol:5:164: | -2 | ... ffffffffffffffffffffffffffffffffff(announcementType Type, string Announcement, string ... +5 | ... ffffffffffffffffffffffffffffffffff(announcementType Type, string Announcement, string ... | ^^^^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/too_long_line/input.sol b/test/cmdlineTests/too_long_line/input.sol index 7df1057a9..c4be6acd9 100644 --- a/test/cmdlineTests/too_long_line/input.sol +++ b/test/cmdlineTests/too_long_line/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C { function ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff(announcementType Type, string Announcement, string Link, bool Oppositable, string _str, uint256 _uint, address _addr) onlyOwner external { } diff --git a/test/cmdlineTests/too_long_line_both_sides_short/err b/test/cmdlineTests/too_long_line_both_sides_short/err index 131fab209..5992d6ea9 100644 --- a/test/cmdlineTests/too_long_line_both_sides_short/err +++ b/test/cmdlineTests/too_long_line_both_sides_short/err @@ -1,11 +1,5 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> too_long_line_both_sides_short/input.sol - -Warning: Source file does not specify required compiler version! ---> too_long_line_both_sides_short/input.sol - Error: Identifier not found or not unique. - --> too_long_line_both_sides_short/input.sol:2:15: + --> too_long_line_both_sides_short/input.sol:5:15: | -2 | function f(announcementTypeXXXXXXXXXXXXXXXXXXX ... XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX Type, +5 | function f(announcementTypeXXXXXXXXXXXXXXXXXXX ... XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX Type, | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/too_long_line_both_sides_short/input.sol b/test/cmdlineTests/too_long_line_both_sides_short/input.sol index 062f02925..255a175cd 100644 --- a/test/cmdlineTests/too_long_line_both_sides_short/input.sol +++ b/test/cmdlineTests/too_long_line_both_sides_short/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C { function f(announcementTypeXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX Type, string Announcement, string Link, bool Oppositable, string _str, uint256 _uint, address _addr) onlyOwner external { diff --git a/test/cmdlineTests/too_long_line_edge_in/err b/test/cmdlineTests/too_long_line_edge_in/err index 83cd670e1..1d96ea4cd 100644 --- a/test/cmdlineTests/too_long_line_edge_in/err +++ b/test/cmdlineTests/too_long_line_edge_in/err @@ -1,11 +1,5 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> too_long_line_edge_in/input.sol - -Warning: Source file does not specify required compiler version! ---> too_long_line_edge_in/input.sol - Error: Identifier not found or not unique. - --> too_long_line_edge_in/input.sol:2:36: + --> too_long_line_edge_in/input.sol:5:36: | -2 | function ffffffffffffffffffffff(announcementTypeTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT Ty, string A) onlyOwner external { +5 | function ffffffffffffffffffffff(announcementTypeTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT Ty, string A) onlyOwner external { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/too_long_line_edge_in/input.sol b/test/cmdlineTests/too_long_line_edge_in/input.sol index 6f181c832..1ab67a981 100644 --- a/test/cmdlineTests/too_long_line_edge_in/input.sol +++ b/test/cmdlineTests/too_long_line_edge_in/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C { function ffffffffffffffffffffff(announcementTypeTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT Ty, string A) onlyOwner external { } diff --git a/test/cmdlineTests/too_long_line_edge_out/err b/test/cmdlineTests/too_long_line_edge_out/err index 7d3b54f21..3b3b4ee49 100644 --- a/test/cmdlineTests/too_long_line_edge_out/err +++ b/test/cmdlineTests/too_long_line_edge_out/err @@ -1,11 +1,5 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> too_long_line_edge_out/input.sol - -Warning: Source file does not specify required compiler version! ---> too_long_line_edge_out/input.sol - Error: Identifier not found or not unique. - --> too_long_line_edge_out/input.sol:2:37: + --> too_long_line_edge_out/input.sol:5:37: | -2 | ... function fffffffffffffffffffffff(announcementTypeTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT Typ, string A) onlyOwner external ... +5 | ... function fffffffffffffffffffffff(announcementTypeTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT Typ, string A) onlyOwner external ... | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/too_long_line_edge_out/input.sol b/test/cmdlineTests/too_long_line_edge_out/input.sol index 29d3cee60..e364a0dac 100644 --- a/test/cmdlineTests/too_long_line_edge_out/input.sol +++ b/test/cmdlineTests/too_long_line_edge_out/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C { function fffffffffffffffffffffff(announcementTypeTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT Typ, string A) onlyOwner external { } diff --git a/test/cmdlineTests/too_long_line_left_short/err b/test/cmdlineTests/too_long_line_left_short/err index 0f8c70e5a..4f2359739 100644 --- a/test/cmdlineTests/too_long_line_left_short/err +++ b/test/cmdlineTests/too_long_line_left_short/err @@ -1,11 +1,5 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> too_long_line_left_short/input.sol - -Warning: Source file does not specify required compiler version! ---> too_long_line_left_short/input.sol - Error: Identifier not found or not unique. - --> too_long_line_left_short/input.sol:2:15: + --> too_long_line_left_short/input.sol:5:15: | -2 | function f(announcementType Type, string Announcement, string ... +5 | function f(announcementType Type, string Announcement, string ... | ^^^^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/too_long_line_left_short/input.sol b/test/cmdlineTests/too_long_line_left_short/input.sol index 2accfcce6..6c53fdb46 100644 --- a/test/cmdlineTests/too_long_line_left_short/input.sol +++ b/test/cmdlineTests/too_long_line_left_short/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C { function f(announcementType Type, string Announcement, string Link, bool Oppositable, string _str, uint256 _uint, address _addr) onlyOwner external { } diff --git a/test/cmdlineTests/too_long_line_multiline/err b/test/cmdlineTests/too_long_line_multiline/err index 6f5dcb71c..4523938c6 100644 --- a/test/cmdlineTests/too_long_line_multiline/err +++ b/test/cmdlineTests/too_long_line_multiline/err @@ -1,11 +1,5 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> too_long_line_multiline/input.sol - Error: No visibility specified. Did you intend to add "public"? - --> too_long_line_multiline/input.sol:2:5: + --> too_long_line_multiline/input.sol:5:5: | -2 | function f() returns (bytes1 _b, by ... _b7, bytes22 _b22, bytes32 _b32) { +5 | function f() returns (bytes1 _b, by ... _b7, bytes22 _b22, bytes32 _b32) { | ^ (Relevant source part starts here and spans across multiple lines). - -Warning: Source file does not specify required compiler version! ---> too_long_line_multiline/input.sol diff --git a/test/cmdlineTests/too_long_line_multiline/input.sol b/test/cmdlineTests/too_long_line_multiline/input.sol index 107c6964b..585d87318 100644 --- a/test/cmdlineTests/too_long_line_multiline/input.sol +++ b/test/cmdlineTests/too_long_line_multiline/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C { function f() returns (bytes1 _b, bytes2 _b2, bytes3 _b3, bytes memory _blit, bytes5 _b5, bytes6 _b6, string memory _str, bytes7 _b7, bytes22 _b22, bytes32 _b32) { _b = 0x12; diff --git a/test/cmdlineTests/too_long_line_right_short/err b/test/cmdlineTests/too_long_line_right_short/err index 6837dd8ab..7aa26ff07 100644 --- a/test/cmdlineTests/too_long_line_right_short/err +++ b/test/cmdlineTests/too_long_line_right_short/err @@ -1,11 +1,5 @@ -Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. ---> too_long_line_right_short/input.sol - -Warning: Source file does not specify required compiler version! ---> too_long_line_right_short/input.sol - Error: Identifier not found or not unique. - --> too_long_line_right_short/input.sol:2:164: + --> too_long_line_right_short/input.sol:5:164: | -2 | ... ffffffffffffffffffffffffffffffffff(announcementType Type, +5 | ... ffffffffffffffffffffffffffffffffff(announcementType Type, | ^^^^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/too_long_line_right_short/input.sol b/test/cmdlineTests/too_long_line_right_short/input.sol index 936b39613..8bf6a887a 100644 --- a/test/cmdlineTests/too_long_line_right_short/input.sol +++ b/test/cmdlineTests/too_long_line_right_short/input.sol @@ -1,3 +1,6 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; + contract C { function ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff(announcementType Type, string Announcement, string Link, bool Oppositable, string _str, uint256 _uint, address _addr) onlyOwner external { From 506cc20fe80fc552824774efe55845587e1d20a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Thu, 5 Aug 2021 17:33:25 +0200 Subject: [PATCH 06/29] Remove empty exit files from command-line tests --- test/cmdlineTests/abiencoderv2_no_warning/exit | 1 - test/cmdlineTests/combined_json_generated_sources/exit | 1 - test/cmdlineTests/exp_base_literal/exit | 1 - test/cmdlineTests/keccak_optimization_deploy_code/exit | 1 - .../model_checker_contracts_inexistent_contract/exit | 1 - test/cmdlineTests/model_checker_contracts_inexistent_source/exit | 1 - test/cmdlineTests/object_compiler/exit | 1 - test/cmdlineTests/standard_default_success/exit | 1 - test/cmdlineTests/standard_empty_file_name/exit | 1 - test/cmdlineTests/standard_missing_key_useLiteralContent/exit | 1 - test/cmdlineTests/standard_secondary_source_location/exit | 1 - test/cmdlineTests/standard_wrong_key_auxiliary_input/exit | 1 - test/cmdlineTests/standard_wrong_key_metadata/exit | 1 - test/cmdlineTests/standard_wrong_key_optimizer/exit | 1 - test/cmdlineTests/standard_wrong_key_root/exit | 1 - test/cmdlineTests/standard_wrong_key_settings/exit | 1 - test/cmdlineTests/standard_wrong_key_source/exit | 1 - test/cmdlineTests/standard_wrong_type_auxiliary_input/exit | 1 - .../standard_wrong_type_auxiliary_input_smtlib2responses/exit | 1 - .../exit | 1 - test/cmdlineTests/standard_wrong_type_metadata/exit | 1 - test/cmdlineTests/standard_wrong_type_optimizer/exit | 1 - test/cmdlineTests/standard_wrong_type_output_selection/exit | 1 - .../standard_wrong_type_output_selection_contract/exit | 1 - test/cmdlineTests/standard_wrong_type_output_selection_file/exit | 1 - .../standard_wrong_type_output_selection_output/exit | 1 - test/cmdlineTests/standard_wrong_type_remappings/exit | 1 - test/cmdlineTests/standard_wrong_type_remappings_entry/exit | 1 - test/cmdlineTests/standard_wrong_type_root/exit | 1 - test/cmdlineTests/standard_wrong_type_settings/exit | 1 - test/cmdlineTests/standard_wrong_type_source/exit | 1 - test/cmdlineTests/standard_wrong_type_sources/exit | 1 - test/cmdlineTests/standard_wrong_type_useLiteralContent/exit | 1 - test/cmdlineTests/yul_verbatim/exit | 1 - test/cmdlineTests/yul_verbatim_msize/exit | 1 - 35 files changed, 35 deletions(-) delete mode 100644 test/cmdlineTests/abiencoderv2_no_warning/exit delete mode 100644 test/cmdlineTests/combined_json_generated_sources/exit delete mode 100644 test/cmdlineTests/exp_base_literal/exit delete mode 100644 test/cmdlineTests/keccak_optimization_deploy_code/exit delete mode 100644 test/cmdlineTests/model_checker_contracts_inexistent_contract/exit delete mode 100644 test/cmdlineTests/model_checker_contracts_inexistent_source/exit delete mode 100644 test/cmdlineTests/object_compiler/exit delete mode 100644 test/cmdlineTests/standard_default_success/exit delete mode 100644 test/cmdlineTests/standard_empty_file_name/exit delete mode 100644 test/cmdlineTests/standard_missing_key_useLiteralContent/exit delete mode 100644 test/cmdlineTests/standard_secondary_source_location/exit delete mode 100644 test/cmdlineTests/standard_wrong_key_auxiliary_input/exit delete mode 100644 test/cmdlineTests/standard_wrong_key_metadata/exit delete mode 100644 test/cmdlineTests/standard_wrong_key_optimizer/exit delete mode 100644 test/cmdlineTests/standard_wrong_key_root/exit delete mode 100644 test/cmdlineTests/standard_wrong_key_settings/exit delete mode 100644 test/cmdlineTests/standard_wrong_key_source/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_auxiliary_input/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_auxiliary_input_smtlib2responses/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_auxiliary_input_smtlib2responses_member/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_metadata/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_optimizer/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_output_selection/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_output_selection_contract/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_output_selection_file/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_output_selection_output/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_remappings/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_remappings_entry/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_root/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_settings/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_source/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_sources/exit delete mode 100644 test/cmdlineTests/standard_wrong_type_useLiteralContent/exit delete mode 100644 test/cmdlineTests/yul_verbatim/exit delete mode 100644 test/cmdlineTests/yul_verbatim_msize/exit diff --git a/test/cmdlineTests/abiencoderv2_no_warning/exit b/test/cmdlineTests/abiencoderv2_no_warning/exit deleted file mode 100644 index c22708346..000000000 --- a/test/cmdlineTests/abiencoderv2_no_warning/exit +++ /dev/null @@ -1 +0,0 @@ -0 \ No newline at end of file diff --git a/test/cmdlineTests/combined_json_generated_sources/exit b/test/cmdlineTests/combined_json_generated_sources/exit deleted file mode 100644 index c22708346..000000000 --- a/test/cmdlineTests/combined_json_generated_sources/exit +++ /dev/null @@ -1 +0,0 @@ -0 \ No newline at end of file diff --git a/test/cmdlineTests/exp_base_literal/exit b/test/cmdlineTests/exp_base_literal/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/exp_base_literal/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/keccak_optimization_deploy_code/exit b/test/cmdlineTests/keccak_optimization_deploy_code/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/keccak_optimization_deploy_code/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/model_checker_contracts_inexistent_contract/exit b/test/cmdlineTests/model_checker_contracts_inexistent_contract/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/model_checker_contracts_inexistent_contract/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/model_checker_contracts_inexistent_source/exit b/test/cmdlineTests/model_checker_contracts_inexistent_source/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/model_checker_contracts_inexistent_source/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/object_compiler/exit b/test/cmdlineTests/object_compiler/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/object_compiler/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_default_success/exit b/test/cmdlineTests/standard_default_success/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_default_success/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_empty_file_name/exit b/test/cmdlineTests/standard_empty_file_name/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_empty_file_name/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_missing_key_useLiteralContent/exit b/test/cmdlineTests/standard_missing_key_useLiteralContent/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_missing_key_useLiteralContent/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_secondary_source_location/exit b/test/cmdlineTests/standard_secondary_source_location/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_secondary_source_location/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_key_auxiliary_input/exit b/test/cmdlineTests/standard_wrong_key_auxiliary_input/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_key_auxiliary_input/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_key_metadata/exit b/test/cmdlineTests/standard_wrong_key_metadata/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_key_metadata/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_key_optimizer/exit b/test/cmdlineTests/standard_wrong_key_optimizer/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_key_optimizer/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_key_root/exit b/test/cmdlineTests/standard_wrong_key_root/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_key_root/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_key_settings/exit b/test/cmdlineTests/standard_wrong_key_settings/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_key_settings/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_key_source/exit b/test/cmdlineTests/standard_wrong_key_source/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_key_source/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_auxiliary_input/exit b/test/cmdlineTests/standard_wrong_type_auxiliary_input/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_auxiliary_input/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_auxiliary_input_smtlib2responses/exit b/test/cmdlineTests/standard_wrong_type_auxiliary_input_smtlib2responses/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_auxiliary_input_smtlib2responses/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_auxiliary_input_smtlib2responses_member/exit b/test/cmdlineTests/standard_wrong_type_auxiliary_input_smtlib2responses_member/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_auxiliary_input_smtlib2responses_member/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_metadata/exit b/test/cmdlineTests/standard_wrong_type_metadata/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_metadata/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_optimizer/exit b/test/cmdlineTests/standard_wrong_type_optimizer/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_optimizer/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_output_selection/exit b/test/cmdlineTests/standard_wrong_type_output_selection/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_output_selection/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_output_selection_contract/exit b/test/cmdlineTests/standard_wrong_type_output_selection_contract/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_output_selection_contract/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_output_selection_file/exit b/test/cmdlineTests/standard_wrong_type_output_selection_file/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_output_selection_file/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_output_selection_output/exit b/test/cmdlineTests/standard_wrong_type_output_selection_output/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_output_selection_output/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_remappings/exit b/test/cmdlineTests/standard_wrong_type_remappings/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_remappings/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_remappings_entry/exit b/test/cmdlineTests/standard_wrong_type_remappings_entry/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_remappings_entry/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_root/exit b/test/cmdlineTests/standard_wrong_type_root/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_root/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_settings/exit b/test/cmdlineTests/standard_wrong_type_settings/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_settings/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_source/exit b/test/cmdlineTests/standard_wrong_type_source/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_source/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_sources/exit b/test/cmdlineTests/standard_wrong_type_sources/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_sources/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/standard_wrong_type_useLiteralContent/exit b/test/cmdlineTests/standard_wrong_type_useLiteralContent/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/standard_wrong_type_useLiteralContent/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/yul_verbatim/exit b/test/cmdlineTests/yul_verbatim/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/yul_verbatim/exit +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/test/cmdlineTests/yul_verbatim_msize/exit b/test/cmdlineTests/yul_verbatim_msize/exit deleted file mode 100644 index 573541ac9..000000000 --- a/test/cmdlineTests/yul_verbatim_msize/exit +++ /dev/null @@ -1 +0,0 @@ -0 From 08c065ee0442736072fd6cfe9a7b01ea1d14b5c5 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Thu, 15 Jul 2021 17:39:01 +0200 Subject: [PATCH 07/29] Add option divModWithSlacks --- Changelog.md | 1 + docs/smtchecker.rst | 14 +- docs/using-the-compiler.rst | 6 + libsolidity/formal/ModelCheckerSettings.h | 8 + libsolidity/formal/SMTEncoder.cpp | 3 + libsolidity/interface/StandardCompiler.cpp | 10 +- solc/CommandLineParser.cpp | 10 ++ .../args | 1 + .../input.sol | 8 + .../args | 1 + .../input.sol | 8 + .../args | 1 + .../input.sol | 8 + .../model_checker_divModSlacks_false_all/args | 1 + .../model_checker_divModSlacks_false_all/err | 13 ++ .../input.sol | 8 + .../model_checker_divModSlacks_false_bmc/args | 1 + .../input.sol | 8 + .../model_checker_divModSlacks_false_chc/args | 1 + .../model_checker_divModSlacks_false_chc/err | 13 ++ .../input.sol | 8 + .../input.json | 22 +++ .../output.json | 49 ++++++ .../input.json | 22 +++ .../output.json | 147 +++++++++++++++++ .../input.json | 22 +++ .../output.json | 1 + .../input.json | 23 +++ .../output.json | 153 ++++++++++++++++++ .../input.json | 23 +++ .../output.json | 139 ++++++++++++++++ .../input.json | 23 +++ .../output.json | 15 ++ .../input.json | 23 +++ .../output.json | 1 + test/solc/CommandLineParser.cpp | 13 +- test/tools/fuzzer_common.cpp | 1 + 37 files changed, 799 insertions(+), 10 deletions(-) create mode 100644 test/cmdlineTests/model_checker_divModSlacks_default_all/args create mode 100644 test/cmdlineTests/model_checker_divModSlacks_default_all/input.sol create mode 100644 test/cmdlineTests/model_checker_divModSlacks_default_bmc/args create mode 100644 test/cmdlineTests/model_checker_divModSlacks_default_bmc/input.sol create mode 100644 test/cmdlineTests/model_checker_divModSlacks_default_chc/args create mode 100644 test/cmdlineTests/model_checker_divModSlacks_default_chc/input.sol create mode 100644 test/cmdlineTests/model_checker_divModSlacks_false_all/args create mode 100644 test/cmdlineTests/model_checker_divModSlacks_false_all/err create mode 100644 test/cmdlineTests/model_checker_divModSlacks_false_all/input.sol create mode 100644 test/cmdlineTests/model_checker_divModSlacks_false_bmc/args create mode 100644 test/cmdlineTests/model_checker_divModSlacks_false_bmc/input.sol create mode 100644 test/cmdlineTests/model_checker_divModSlacks_false_chc/args create mode 100644 test/cmdlineTests/model_checker_divModSlacks_false_chc/err create mode 100644 test/cmdlineTests/model_checker_divModSlacks_false_chc/input.sol create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_default_all/output.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json create mode 100644 test/cmdlineTests/standard_model_checker_divModSlacks_wrong/output.json diff --git a/Changelog.md b/Changelog.md index 09ef7db60..d6bb765c5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -10,6 +10,7 @@ Compiler Features: * Yul Optimizer: Move function arguments and return variables to memory with the experimental Stack Limit Evader (which is not enabled by default). * Commandline Interface: option ``--pretty-json`` works also with ``--standard--json``. * SMTChecker: Unproved targets are hidden by default, and the SMTChecker only states how many unproved targets there are. They can be listed using the command line option ``--model-checker-show-unproved`` or the JSON option ``settings.modelChecker.showUnproved``. + * SMTChecker: new setting to enable/disable encoding of division and modulo with slack variables. The command line option is ``--model-checker-div-mod-slacks`` and the JSON option is ``settings.modelChecker.divModWithSlacks``. Bugfixes: diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index e2b61cf35..5c42fb415 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -509,7 +509,17 @@ which has the following form: "source2.sol": ["contract2", "contract3"] } -.. _smtchecker_engines: +Division and Modulo With Slack Variables +======================================== + +Spacer, the default Horn solver used by the SMTChecker, often dislikes division +and modulo operations inside Horn rules. Because of that, by default the +Solidity division and modulo operations are encoded using the constraint +``a = b * d + m`` where ``d = a / b`` and ``m = a % b``. +However, other solvers, such as Eldarica, prefer the syntactically precise operations. +The command line flag ``--model-checker-div-mod-no-slacks`` and the JSON option +``settings.modelChecker.divModNoSlacks`` can be used to toggle the encoding +depending on the used solver preferences. Natspec Function Abstraction ============================ @@ -523,6 +533,8 @@ body of the function is not used, and when called, the function will: - Return a nondeterministic value, and either keep the state variables unchanged if the abstracted function is view/pure, or also set the state variables to nondeterministic values otherwise. This can be used via the annotation ``/// @custom:smtchecker abstract-function-nondet``. - Act as an uninterpreted function. This means that the semantics of the function (given by the body) are ignored, and the only property this function has is that given the same input it guarantees the same output. This is currently under development and will be available via the annotation ``/// @custom:smtchecker abstract-function-uf``. +.. _smtchecker_engines: + Model Checking Engines ====================== diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 381f150cd..cf281b851 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -400,6 +400,12 @@ Input Description "source1.sol": ["contract1"], "source2.sol": ["contract2", "contract3"] }, + // Choose whether division and modulo operations should be replaced by + // multiplication with slack variables. Default is `true`. + // Using `false` here is recommended if you are using the CHC engine + // and not using Spacer as the Horn solver (using Eldarica, for example). + // See the Formal Verification section for a more detailed explanation of this option. + "divModWithSlacks": true, // Choose which model checker engine to use: all (default), bmc, chc, none. "engine": "chc", // Choose whether to output all unproved targets. The default is `false`. diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index ff39ddc9f..5f2dcc91e 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/libsolidity/formal/ModelCheckerSettings.h @@ -112,6 +112,13 @@ struct ModelCheckerTargets struct ModelCheckerSettings { ModelCheckerContracts contracts = ModelCheckerContracts::Default(); + /// Currently division and modulo are replaced by multiplication with slack vars, such that + /// a / b <=> a = b * k + m + /// where k and m are slack variables. + /// This is the default because Spacer prefers that over precise / and mod. + /// This option allows disabling this mechanism since other solvers + /// might prefer the precise encoding. + bool divModNoSlacks = false; ModelCheckerEngine engine = ModelCheckerEngine::None(); bool showUnproved = false; smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All(); @@ -123,6 +130,7 @@ struct ModelCheckerSettings { return contracts == _other.contracts && + divModNoSlacks == _other.divModNoSlacks && engine == _other.engine && showUnproved == _other.showUnproved && solvers == _other.solvers && diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 4069134c9..17f0e46ee 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1916,6 +1916,9 @@ pair SMTEncoder::divModWithSlacks( IntegerType const& _type ) { + if (m_settings.divModNoSlacks) + return {_left / _right, _left % _right}; + IntegerType const* intType = &_type; string suffix = "div_mod_" + to_string(m_context.newUniqueId()); smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context); diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 0a12059d5..4071a1fbe 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -442,7 +442,7 @@ std::optional checkSettingsKeys(Json::Value const& _input) std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { - static set keys{"contracts", "engine", "showUnproved", "solvers", "targets", "timeout"}; + static set keys{"contracts", "divModNoSlacks", "engine", "showUnproved", "solvers", "targets", "timeout"}; return checkKeys(_input, keys, "modelChecker"); } @@ -941,6 +941,14 @@ std::variant StandardCompiler: ret.modelCheckerSettings.contracts = {move(sourceContracts)}; } + if (modelCheckerSettings.isMember("divModNoSlacks")) + { + auto const& divModNoSlacks = modelCheckerSettings["divModNoSlacks"]; + if (!divModNoSlacks.isBool()) + return formatFatalError("JSONError", "settings.modelChecker.divModNoSlacks must be a Boolean."); + ret.modelCheckerSettings.divModNoSlacks = divModNoSlacks.asBool(); + } + if (modelCheckerSettings.isMember("engine")) { if (!modelCheckerSettings["engine"].isString()) diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index 3654bbfc8..d09e101b8 100644 --- a/solc/CommandLineParser.cpp +++ b/solc/CommandLineParser.cpp @@ -86,6 +86,7 @@ static string const g_strMetadata = "metadata"; static string const g_strMetadataHash = "metadata-hash"; static string const g_strMetadataLiteral = "metadata-literal"; static string const g_strModelCheckerContracts = "model-checker-contracts"; +static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks"; static string const g_strModelCheckerEngine = "model-checker-engine"; static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved"; static string const g_strModelCheckerSolvers = "model-checker-solvers"; @@ -720,6 +721,11 @@ General Information)").c_str(), "Multiple pairs : can be selected at the same time, separated by a comma " "and no spaces." ) + ( + g_strModelCheckerDivModNoSlacks.c_str(), + "Encode division and modulo operations with their precise operators" + " instead of multiplication with slack variables." + ) ( g_strModelCheckerEngine.c_str(), po::value()->value_name("all,bmc,chc,none")->default_value("none"), @@ -1092,6 +1098,9 @@ General Information)").c_str(), m_options.modelChecker.settings.contracts = move(*contracts); } + if (m_args.count(g_strModelCheckerDivModNoSlacks)) + m_options.modelChecker.settings.divModNoSlacks = true; + if (m_args.count(g_strModelCheckerEngine)) { string engineStr = m_args[g_strModelCheckerEngine].as(); @@ -1140,6 +1149,7 @@ General Information)").c_str(), m_options.metadata.literalSources = (m_args.count(g_strMetadataLiteral) > 0); m_options.modelChecker.initialize = m_args.count(g_strModelCheckerContracts) || + m_args.count(g_strModelCheckerDivModNoSlacks) || m_args.count(g_strModelCheckerEngine) || m_args.count(g_strModelCheckerShowUnproved) || m_args.count(g_strModelCheckerSolvers) || diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_all/args b/test/cmdlineTests/model_checker_divModSlacks_default_all/args new file mode 100644 index 000000000..5aeb1490e --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_default_all/args @@ -0,0 +1 @@ +--model-checker-engine all diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_all/input.sol b/test/cmdlineTests/model_checker_divModSlacks_default_all/input.sol new file mode 100644 index 000000000..4dcb4cb28 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_default_all/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } +} diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_bmc/args b/test/cmdlineTests/model_checker_divModSlacks_default_bmc/args new file mode 100644 index 000000000..549f20236 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_default_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_bmc/input.sol b/test/cmdlineTests/model_checker_divModSlacks_default_bmc/input.sol new file mode 100644 index 000000000..4dcb4cb28 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_default_bmc/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } +} diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_chc/args b/test/cmdlineTests/model_checker_divModSlacks_default_chc/args new file mode 100644 index 000000000..7458a47d3 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_default_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc diff --git a/test/cmdlineTests/model_checker_divModSlacks_default_chc/input.sol b/test/cmdlineTests/model_checker_divModSlacks_default_chc/input.sol new file mode 100644 index 000000000..4dcb4cb28 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_default_chc/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } +} diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_all/args b/test/cmdlineTests/model_checker_divModSlacks_false_all/args new file mode 100644 index 000000000..75bfbf194 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_false_all/args @@ -0,0 +1 @@ +--model-checker-engine all --model-checker-div-mod-no-slacks diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_all/err b/test/cmdlineTests/model_checker_divModSlacks_false_all/err new file mode 100644 index 000000000..3e4759a94 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_false_all/err @@ -0,0 +1,13 @@ +Warning: CHC: Error trying to invoke SMT solver. + --> model_checker_divModSlacks_false_all/input.sol:6:11: + | +6 | return (a / b, a % b); + | ^^^^^ + +Warning: CHC: Error trying to invoke SMT solver. + --> model_checker_divModSlacks_false_all/input.sol:6:18: + | +6 | return (a / b, a % b); + | ^^^^^ + +Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_all/input.sol b/test/cmdlineTests/model_checker_divModSlacks_false_all/input.sol new file mode 100644 index 000000000..4dcb4cb28 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_false_all/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } +} diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_bmc/args b/test/cmdlineTests/model_checker_divModSlacks_false_bmc/args new file mode 100644 index 000000000..2579bdc1e --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_false_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc --model-checker-div-mod-no-slacks diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_bmc/input.sol b/test/cmdlineTests/model_checker_divModSlacks_false_bmc/input.sol new file mode 100644 index 000000000..4dcb4cb28 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_false_bmc/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } +} diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_chc/args b/test/cmdlineTests/model_checker_divModSlacks_false_chc/args new file mode 100644 index 000000000..b0679b1c6 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_false_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc --model-checker-div-mod-no-slacks diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_chc/err b/test/cmdlineTests/model_checker_divModSlacks_false_chc/err new file mode 100644 index 000000000..56cca82c0 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_false_chc/err @@ -0,0 +1,13 @@ +Warning: CHC: Error trying to invoke SMT solver. + --> model_checker_divModSlacks_false_chc/input.sol:6:11: + | +6 | return (a / b, a % b); + | ^^^^^ + +Warning: CHC: Error trying to invoke SMT solver. + --> model_checker_divModSlacks_false_chc/input.sol:6:18: + | +6 | return (a / b, a % b); + | ^^^^^ + +Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. diff --git a/test/cmdlineTests/model_checker_divModSlacks_false_chc/input.sol b/test/cmdlineTests/model_checker_divModSlacks_false_chc/input.sol new file mode 100644 index 000000000..4dcb4cb28 --- /dev/null +++ b/test/cmdlineTests/model_checker_divModSlacks_false_chc/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +contract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } +} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json new file mode 100644 index 000000000..7ede51865 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/output.json new file mode 100644 index 000000000..64d6be1dd --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_all/output.json @@ -0,0 +1,49 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x10763dfdad96614fe8fcaf54161ed2be500bbaa57bda8e2d706b675f1290f13b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) + +(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1)) +(check-sat) +","0xa0332f5d2cf85238fd31e652cfbcc1d2a774996d4d2368d02b71c393eb375f0e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) + +(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1))) +(check-sat) +"}},"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json new file mode 100644 index 000000000..ccb4839bb --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/output.json new file mode 100644 index 000000000..913a2f432 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/output.json @@ -0,0 +1,147 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x10763dfdad96614fe8fcaf54161ed2be500bbaa57bda8e2d706b675f1290f13b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) + +(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1)) +(check-sat) +","0x2eb208535af4432660b05fdb09b9dfd9c1a1e633a3d266b2886fdbcb487471e3":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_0| () Int) +(declare-fun |d_div_mod_1_0| () Int) +(declare-fun |r_div_mod_1_0| () Int) +(declare-fun |expr_23_1| () Int) +(declare-datatypes ((|tuple(uint256,uint256)| 0)) (((|tuple(uint256,uint256)| (|tuple(uint256,uint256)_accessor_0| Int) (|tuple(uint256,uint256)_accessor_1| Int))))) +(declare-fun |expr_24_1| () |tuple(uint256,uint256)|) +(declare-fun |_8_1| () Int) +(declare-fun |_10_1| () Int) + +(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_22_0 0) (<= expr_22_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_22_0 b_5_0) (and (=> (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 a_3_0) (and (=> (and true true) (and (>= expr_20_1 0) (<= expr_20_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_1 (ite (= expr_19_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (=> (and true true) (and (>= expr_19_0 0) (<= expr_19_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_0 b_5_0) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 a_3_0) (and (=> (and true true) expr_15_1) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))) (= expr_22_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| a_3_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| b_5_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| _8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| _10_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_22_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +","0xa0332f5d2cf85238fd31e652cfbcc1d2a774996d4d2368d02b71c393eb375f0e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) + +(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1))) +(check-sat) +","0xffa9239519f28ed244d2db22aa16da5ade2117d1638913e9fd5eda8332996957":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_0| () Int) +(declare-fun |d_div_mod_1_0| () Int) +(declare-fun |r_div_mod_1_0| () Int) +(declare-fun |expr_23_1| () Int) +(declare-datatypes ((|tuple(uint256,uint256)| 0)) (((|tuple(uint256,uint256)| (|tuple(uint256,uint256)_accessor_0| Int) (|tuple(uint256,uint256)_accessor_1| Int))))) +(declare-fun |expr_24_1| () |tuple(uint256,uint256)|) +(declare-fun |_8_1| () Int) +(declare-fun |_10_1| () Int) + +(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_19_0 0) (<= expr_19_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_0 b_5_0) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 a_3_0) (and (=> (and true true) expr_15_1) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))) (= expr_19_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| a_3_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| b_5_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| _8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| _10_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_19_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +"}},"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json new file mode 100644 index 000000000..e33e97706 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json @@ -0,0 +1,22 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc" + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/output.json new file mode 100644 index 000000000..59b90c8cc --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/output.json @@ -0,0 +1 @@ +{"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json new file mode 100644 index 000000000..efa209cf9 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json @@ -0,0 +1,23 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "all", + "divModNoSlacks": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json new file mode 100644 index 000000000..497482baa --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json @@ -0,0 +1,153 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x10763dfdad96614fe8fcaf54161ed2be500bbaa57bda8e2d706b675f1290f13b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) + +(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1)) +(check-sat) +","0x55de298588de6547098e62309fe1065399b5711eae0146b256137aa05d54806c":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_0| () Int) +(declare-fun |expr_23_1| () Int) +(declare-datatypes ((|tuple(uint256,uint256)| 0)) (((|tuple(uint256,uint256)| (|tuple(uint256,uint256)_accessor_0| Int) (|tuple(uint256,uint256)_accessor_1| Int))))) +(declare-fun |expr_24_1| () |tuple(uint256,uint256)|) +(declare-fun |_8_1| () Int) +(declare-fun |_10_1| () Int) + +(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_22_0 0) (<= expr_22_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_22_0 b_5_0) (and (=> (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 a_3_0) (and (=> (and true true) (and (>= expr_20_1 0) (<= expr_20_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_1 (div expr_18_0 expr_19_0)) (and (=> (and true true) (and (>= expr_19_0 0) (<= expr_19_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_0 b_5_0) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 a_3_0) (and (=> (and true true) expr_15_1) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))) (= expr_22_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| a_3_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| b_5_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| _8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| _10_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_22_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +","0xa0332f5d2cf85238fd31e652cfbcc1d2a774996d4d2368d02b71c393eb375f0e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) + +(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1))) +(check-sat) +","0xab025faeb2e4c20d674670ede4603b61a2424f98dff12acd21022b2ba2d021a2":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_0| () Int) +(declare-fun |expr_23_1| () Int) +(declare-datatypes ((|tuple(uint256,uint256)| 0)) (((|tuple(uint256,uint256)| (|tuple(uint256,uint256)_accessor_0| Int) (|tuple(uint256,uint256)_accessor_1| Int))))) +(declare-fun |expr_24_1| () |tuple(uint256,uint256)|) +(declare-fun |_8_1| () Int) +(declare-fun |_10_1| () Int) + +(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_19_0 0) (<= expr_19_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_0 b_5_0) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 a_3_0) (and (=> (and true true) expr_15_1) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))) (= expr_19_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| a_3_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| b_5_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| _8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| _10_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_19_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +"}},"errors":[{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver. + --> A:7:15: + | +7 | \t\t\t\t\t\treturn (a / b, a % b); + | \t\t\t\t\t\t ^^^^^ + +","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":182,"file":"A","start":177},"type":"Warning"},{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver. + --> A:7:22: + | +7 | \t\t\t\t\t\treturn (a / b, a % b); + | \t\t\t\t\t\t ^^^^^ + +","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":189,"file":"A","start":184},"type":"Warning"},{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + +","message":"CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json new file mode 100644 index 000000000..167b849f4 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json @@ -0,0 +1,23 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "bmc", + "divModNoSlacks": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/output.json new file mode 100644 index 000000000..bbb88285c --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/output.json @@ -0,0 +1,139 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x10763dfdad96614fe8fcaf54161ed2be500bbaa57bda8e2d706b675f1290f13b":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) + +(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1)) +(check-sat) +","0x55de298588de6547098e62309fe1065399b5711eae0146b256137aa05d54806c":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_0| () Int) +(declare-fun |expr_23_1| () Int) +(declare-datatypes ((|tuple(uint256,uint256)| 0)) (((|tuple(uint256,uint256)| (|tuple(uint256,uint256)_accessor_0| Int) (|tuple(uint256,uint256)_accessor_1| Int))))) +(declare-fun |expr_24_1| () |tuple(uint256,uint256)|) +(declare-fun |_8_1| () Int) +(declare-fun |_10_1| () Int) + +(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_22_0 0) (<= expr_22_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_22_0 b_5_0) (and (=> (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 a_3_0) (and (=> (and true true) (and (>= expr_20_1 0) (<= expr_20_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_1 (div expr_18_0 expr_19_0)) (and (=> (and true true) (and (>= expr_19_0 0) (<= expr_19_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_0 b_5_0) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 a_3_0) (and (=> (and true true) expr_15_1) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))) (= expr_22_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| a_3_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| b_5_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| _8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| _10_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_22_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +","0xa0332f5d2cf85238fd31e652cfbcc1d2a774996d4d2368d02b71c393eb375f0e":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) + +(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1))) +(check-sat) +","0xab025faeb2e4c20d674670ede4603b61a2424f98dff12acd21022b2ba2d021a2":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |a_3_0| () Int) +(declare-fun |b_5_0| () Int) +(declare-fun |_8_0| () Int) +(declare-fun |_10_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_0| () Int) +(declare-fun |expr_15_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_0| () Int) +(declare-fun |expr_23_1| () Int) +(declare-datatypes ((|tuple(uint256,uint256)| 0)) (((|tuple(uint256,uint256)| (|tuple(uint256,uint256)_accessor_0| Int) (|tuple(uint256,uint256)_accessor_1| Int))))) +(declare-fun |expr_24_1| () |tuple(uint256,uint256)|) +(declare-fun |_8_1| () Int) +(declare-fun |_10_1| () Int) + +(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_19_0 0) (<= expr_19_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_0 b_5_0) (and (=> (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 a_3_0) (and (=> (and true true) expr_15_1) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))) (= expr_19_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| a_3_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| b_5_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| _8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| _10_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_19_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +"}},"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json new file mode 100644 index 000000000..ac29b462b --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json @@ -0,0 +1,23 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "divModNoSlacks": true + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json new file mode 100644 index 000000000..c4e29b4e8 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json @@ -0,0 +1,15 @@ +{"errors":[{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver. + --> A:7:15: + | +7 | \t\t\t\t\t\treturn (a / b, a % b); + | \t\t\t\t\t\t ^^^^^ + +","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":182,"file":"A","start":177},"type":"Warning"},{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver. + --> A:7:22: + | +7 | \t\t\t\t\t\treturn (a / b, a % b); + | \t\t\t\t\t\t ^^^^^ + +","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":189,"file":"A","start":184},"type":"Warning"},{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query. + +","message":"CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json b/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json new file mode 100644 index 000000000..09be5d735 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json @@ -0,0 +1,23 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { + function f(uint a, uint b) public pure returns (uint, uint) { + require(b != 0); + return (a / b, a % b); + } + }" + } + }, + "settings": + { + "modelChecker": + { + "engine": "chc", + "divModNoSlacks": 42 + } + } +} diff --git a/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/output.json b/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/output.json new file mode 100644 index 000000000..05cca29c4 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_divModSlacks_wrong/output.json @@ -0,0 +1 @@ +{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.divModNoSlacks must be a Boolean.","message":"settings.modelChecker.divModNoSlacks must be a Boolean.","severity":"error","type":"JSONError"}]} diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index bb427232c..f97636a94 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -79,14 +79,7 @@ BOOST_AUTO_TEST_CASE(no_options) CommandLineOptions expectedOptions; expectedOptions.input.paths = {"contract.sol"}; expectedOptions.modelChecker.initialize = true; - expectedOptions.modelChecker.settings = { - ModelCheckerContracts::Default(), - ModelCheckerEngine::None(), - false, - smtutil::SMTSolverChoice::All(), - ModelCheckerTargets::Default(), - nullopt, - }; + expectedOptions.modelChecker.settings = {}; stringstream sout, serr; optional parsedOptions = parseCommandLine(commandLine, sout, serr); @@ -151,6 +144,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--optimize-runs=1000", "--yul-optimizations=agf", "--model-checker-contracts=contract1.yul:A,contract2.yul:B", + "--model-checker-div-mod-no-slacks", "--model-checker-engine=bmc", "--model-checker-show-unproved=true", "--model-checker-solvers=z3,smtlib2", @@ -210,6 +204,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) expectedOptions.modelChecker.initialize = true; expectedOptions.modelChecker.settings = { {{{"contract1.yul", {"A"}}, {"contract2.yul", {"B"}}}}, + true, {true, false}, true, {false, true, true}, @@ -281,6 +276,7 @@ BOOST_AUTO_TEST_CASE(assembly_mode_options) "--model-checker-contracts=" // Ignored in assembly mode "contract1.yul:A," "contract2.yul:B", + "--model-checker-div-mod-no-slacks", // Ignored in assembly mode "--model-checker-engine=bmc", // Ignored in assembly mode "--model-checker-show-unproved=true", // Ignored in assembly mode "--model-checker-solvers=z3,smtlib2", // Ignored in assembly mode @@ -380,6 +376,7 @@ BOOST_AUTO_TEST_CASE(standard_json_mode_options) "--model-checker-contracts=" // Ignored in Standard JSON mode "contract1.yul:A," "contract2.yul:B", + "--model-checker-div-mod-no-slacks", // Ignored in Standard JSON mode "--model-checker-engine=bmc", // Ignored in Standard JSON mode "--model-checker-show-unproved=true", // Ignored in Standard JSON mode "--model-checker-solvers=z3,smtlib2", // Ignored in Standard JSON mode diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index 65749a009..5a1849ea6 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -104,6 +104,7 @@ void FuzzerUtil::testCompiler( forceSMT(_input); compiler.setModelCheckerSettings({ frontend::ModelCheckerContracts::Default(), + /*divModWithSlacks*/true, frontend::ModelCheckerEngine::All(), /*showUnproved=*/false, smtutil::SMTSolverChoice::All(), From e9e3f1238f182393f286ba1238eab7da7dccfb3a Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Fri, 6 Aug 2021 17:40:45 +0200 Subject: [PATCH 08/29] Add solvers to model checker json docs --- docs/using-the-compiler.rst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index cf281b851..afb60acd7 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -410,6 +410,9 @@ Input Description "engine": "chc", // Choose whether to output all unproved targets. The default is `false`. "showUnproved": true, + // Choose which solvers should be used, if available. + // See the Formal Verification section for the solvers description. + "solvers": ["cvc4", "smtlib2", "z3"], // Choose which targets should be checked: constantCondition, // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds. // If the option is not given all targets are checked by default. From 88b5be4224556dcb95520d89c576609e3c67d19d Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Thu, 15 Jul 2021 15:23:40 +0200 Subject: [PATCH 09/29] Update Z3 version to 4.8.12 in PPA script and add static binary package. --- scripts/deps-ppa/static_z3.sh | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) diff --git a/scripts/deps-ppa/static_z3.sh b/scripts/deps-ppa/static_z3.sh index 583338951..66fbd3fa7 100755 --- a/scripts/deps-ppa/static_z3.sh +++ b/scripts/deps-ppa/static_z3.sh @@ -24,10 +24,10 @@ set -ev keyid=70D110489D66E2F6 email=builds@ethereum.org -packagename=libz3-static-dev -version=4.8.10 +packagename=z3-static +version=4.8.12 -DISTRIBUTIONS="focal groovy" +DISTRIBUTIONS="focal groovy hirsute" for distribution in $DISTRIBUTIONS do @@ -62,7 +62,7 @@ mkdir debian echo 9 > debian/compat # TODO: the Z3 packages have different build dependencies cat < debian/control -Source: libz3-static-dev +Source: z3-static Section: science Priority: extra Maintainer: Daniel Kirchner @@ -78,6 +78,22 @@ Homepage: https://github.com/Z3Prover/z3 Vcs-Git: git://github.com/Z3Prover/z3.git Vcs-Browser: https://github.com/Z3Prover/z3 +Package: z3-static +Architecture: any +Breaks: z3 +Replaces: z3 +Depends: \${misc:Depends}, \${shlibs:Depends} +Description: theorem prover from Microsoft Research + Z3 is a state-of-the art theorem prover from Microsoft Research. It can be + used to check the satisfiability of logical formulas over one or more + theories. Z3 offers a compelling match for software analysis and verification + tools, since several common software constructs map directly into supported + theories. + . + The Z3 input format is an extension of the one defined by the SMT-LIB 2.0 + standard. + + Package: libz3-static-dev Section: libdevel Architecture: any-amd64 @@ -133,6 +149,9 @@ usr/include/* usr/lib/*/libz3.a usr/lib/*/cmake/z3/* EOF +cat < debian/z3-static.install +usr/bin/z3 +EOF cat < debian/copyright Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ Upstream-Name: z3 @@ -179,7 +198,7 @@ This program is free software: you can redistribute it and/or modify Public License version 3 can be found in "/usr/share/common-licenses/GPL-3". EOF cat < debian/changelog -libz3-static-dev (0.0.1-1ubuntu0) saucy; urgency=low +z3-static (0.0.1-1ubuntu0) saucy; urgency=low * Initial release. From ee6285d6d745b8e81407e47b5190ae9eba91c370 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 7 Jul 2021 12:31:09 +0200 Subject: [PATCH 10/29] Do not create VCs for underoverflow by default for Sol >=0.8 --- Changelog.md | 1 + docs/smtchecker.rst | 13 +- docs/using-the-compiler.rst | 3 +- libsolidity/formal/ModelCheckerSettings.cpp | 9 +- libsolidity/formal/ModelCheckerSettings.h | 3 + solc/CommandLineParser.cpp | 6 +- .../args | 1 + .../err | 16 +- .../input.sol | 0 .../model_checker_targets_all_bmc/args | 2 +- .../model_checker_targets_all_chc/args | 2 +- .../args | 0 .../err | 78 +++++++++ .../input.sol | 15 ++ .../model_checker_targets_default_bmc/args | 1 + .../model_checker_targets_default_bmc/err | 43 +++++ .../input.sol | 15 ++ .../model_checker_targets_default_chc/args | 1 + .../model_checker_targets_default_chc/err | 59 +++++++ .../input.sol | 15 ++ .../input.json | 0 .../output.json | 162 ++++++------------ .../input.json | 0 .../output.json | 150 +--------------- .../input.json | 0 .../output.json | 50 +----- test/libsolidity/SMTCheckerTest.cpp | 4 + test/libsolidity/SMTCheckerTest.h | 21 ++- 28 files changed, 341 insertions(+), 329 deletions(-) create mode 100644 test/cmdlineTests/model_checker_targets_all_all_engines/args rename test/cmdlineTests/{model_checker_targets_all => model_checker_targets_all_all_engines}/err (75%) rename test/cmdlineTests/{model_checker_targets_all => model_checker_targets_all_all_engines}/input.sol (100%) rename test/cmdlineTests/{model_checker_targets_all => model_checker_targets_default_all_engines}/args (100%) create mode 100644 test/cmdlineTests/model_checker_targets_default_all_engines/err create mode 100644 test/cmdlineTests/model_checker_targets_default_all_engines/input.sol create mode 100644 test/cmdlineTests/model_checker_targets_default_bmc/args create mode 100644 test/cmdlineTests/model_checker_targets_default_bmc/err create mode 100644 test/cmdlineTests/model_checker_targets_default_bmc/input.sol create mode 100644 test/cmdlineTests/model_checker_targets_default_chc/args create mode 100644 test/cmdlineTests/model_checker_targets_default_chc/err create mode 100644 test/cmdlineTests/model_checker_targets_default_chc/input.sol rename test/cmdlineTests/{standard_model_checker_targets_all => standard_model_checker_targets_default_all_engines}/input.json (100%) rename test/cmdlineTests/{standard_model_checker_targets_all => standard_model_checker_targets_default_all_engines}/output.json (90%) rename test/cmdlineTests/{standard_model_checker_targets_all_bmc => standard_model_checker_targets_default_bmc}/input.json (100%) rename test/cmdlineTests/{standard_model_checker_targets_all_bmc => standard_model_checker_targets_default_bmc}/output.json (70%) rename test/cmdlineTests/{standard_model_checker_targets_all_chc => standard_model_checker_targets_default_chc}/input.json (100%) rename test/cmdlineTests/{standard_model_checker_targets_all_chc => standard_model_checker_targets_default_chc}/output.json (61%) diff --git a/Changelog.md b/Changelog.md index d6bb765c5..916dbfde5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -11,6 +11,7 @@ Compiler Features: * Commandline Interface: option ``--pretty-json`` works also with ``--standard--json``. * SMTChecker: Unproved targets are hidden by default, and the SMTChecker only states how many unproved targets there are. They can be listed using the command line option ``--model-checker-show-unproved`` or the JSON option ``settings.modelChecker.showUnproved``. * SMTChecker: new setting to enable/disable encoding of division and modulo with slack variables. The command line option is ``--model-checker-div-mod-slacks`` and the JSON option is ``settings.modelChecker.divModWithSlacks``. + * SMTChecker: Do not check underflow and overflow by default. Bugfixes: diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index 5c42fb415..65b21a10e 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -34,6 +34,9 @@ The other verification targets that the SMTChecker checks at compile time are: - Out of bounds index access. - Insufficient funds for a transfer. +All the targets above are automatically checked by default if all engines are +enabled, except underflow and overflow for Solidity >=0.8.7. + The potential warnings that the SMTChecker reports are: - `` happens here.``. This means that the SMTChecker proved that a certain property fails. A counterexample may be given, however in complex situations it may also not show a counterexample. This result may also be a false positive in certain cases, when the SMT encoding adds abstractions for Solidity code that is either hard or impossible to express. @@ -93,8 +96,10 @@ Overflow } The contract above shows an overflow check example. -The SMTChecker will, by default, check every reachable arithmetic operation -in the contract for potential underflow and overflow. +The SMTChecker does not check underflow and overflow by default for Solidity >=0.8.7, +so we need to use the command line option ``--model-checker-targets "underflow,overflow"`` +or the JSON option ``settings.modelChecker.targets = ["underflow", "overflow"]``. +See :ref:`this section for targets configuration`. Here, it reports the following: .. code-block:: text @@ -447,6 +452,8 @@ If the SMTChecker does not manage to solve the contract properties with the defa a timeout can be given in milliseconds via the CLI option ``--model-checker-timeout