From 5ee9b2f5d09fb3bc365ad541434ed4975be32932 Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Sun, 18 May 2025 13:00:17 -0300 Subject: [PATCH 1/9] Add and update tests --- .../array/length/constant_member_access.sol | 10 ++++++++++ .../constantEvaluator/member_access.sol | 8 ++++++++ ...constant_variables_as_static_array_length.sol | 11 ++++------- ...constant_with_dependencies_as_array_sizes.sol | 16 ++++++++-------- 4 files changed, 30 insertions(+), 15 deletions(-) create mode 100644 test/libsolidity/syntaxTests/array/length/constant_member_access.sol create mode 100644 test/libsolidity/syntaxTests/constantEvaluator/member_access.sol diff --git a/test/libsolidity/syntaxTests/array/length/constant_member_access.sol b/test/libsolidity/syntaxTests/array/length/constant_member_access.sol new file mode 100644 index 000000000000..d6343b8c07b1 --- /dev/null +++ b/test/libsolidity/syntaxTests/array/length/constant_member_access.sol @@ -0,0 +1,10 @@ +contract A { + uint constant INHERITED = 42; +} + +contract C is A { + uint constant CONST = 64; + uint[A.INHERITED] x; + uint[C.CONST] y; +} +// ---- diff --git a/test/libsolidity/syntaxTests/constantEvaluator/member_access.sol b/test/libsolidity/syntaxTests/constantEvaluator/member_access.sol new file mode 100644 index 000000000000..e75ea651569b --- /dev/null +++ b/test/libsolidity/syntaxTests/constantEvaluator/member_access.sol @@ -0,0 +1,8 @@ +contract A { + uint constant INHERITED = 1; +} +contract C is A { + uint constant CONST = 2 + A.INHERITED; + uint[CONST] array; +} +// ---- diff --git a/test/libsolidity/syntaxTests/constants/constant_variables_as_static_array_length.sol b/test/libsolidity/syntaxTests/constants/constant_variables_as_static_array_length.sol index 19e8bfee2108..5eb9ac7ce402 100644 --- a/test/libsolidity/syntaxTests/constants/constant_variables_as_static_array_length.sol +++ b/test/libsolidity/syntaxTests/constants/constant_variables_as_static_array_length.sol @@ -7,15 +7,15 @@ library L1 { contract C1 { uint256 internal constant CONST1 = L1.INT; - uint256[L1.INT] internal arr1; // error, backward reference + uint256[L1.INT] internal arr1; uint256[L2.INT] internal arr2; // error, forward reference } contract C2 is C1 { uint256 internal constant CONST2 = CONST1; - uint256[CONST1] internal arr3; // error, inherited constants - uint256[CONST2] internal arr4; // error, same contract constant + uint256[CONST1] internal arr3; + uint256[CONST2] internal arr4; } library L2 { @@ -23,7 +23,4 @@ library L2 { } // ---- -// TypeError 5462: (158-164): Invalid array length, expected integer literal or constant expression. -// TypeError 5462: (222-228): Invalid array length, expected integer literal or constant expression. -// TypeError 5462: (356-362): Invalid array length, expected integer literal or constant expression. -// TypeError 5462: (421-427): Invalid array length, expected integer literal or constant expression. +// TypeError 5462: (193-199): Invalid array length, expected integer literal or constant expression. diff --git a/test/libsolidity/syntaxTests/constants/constant_with_dependencies_as_array_sizes.sol b/test/libsolidity/syntaxTests/constants/constant_with_dependencies_as_array_sizes.sol index a2a1ce20ee15..c17df7842579 100644 --- a/test/libsolidity/syntaxTests/constants/constant_with_dependencies_as_array_sizes.sol +++ b/test/libsolidity/syntaxTests/constants/constant_with_dependencies_as_array_sizes.sol @@ -5,12 +5,14 @@ library L1 { } contract C1 { - uint256 internal constant CONST = 20 + L2.INT; // forward reference + uint256 internal constant CONST = 30 + L1.INT; // backward reference + uint256 internal constant CONST2 = 30 + L2.INT; // forward reference uint256 internal constant LIMIT = MAX * L1.INT; // same file & external library constant uint256 internal constant NESTED = LIMIT + CONST; // nested & same contract constant - uint256[L1.INT] internal arr1; // error, backward reference + uint256[L1.INT] internal arr1; // ok, backward reference uint256[L2.INT] internal arr2; // error, forward reference + uint256[CONST2] internal arr3; // error, computed with forward reference } contract C2 is C1 { @@ -20,8 +22,8 @@ contract C2 is C1 { contract C3 is C2 { uint256 internal constant NESTED_INHERITED = INHERITED + NESTED + CONST * LIMIT; // nest-inherited constants - uint256[CONST] internal arr3; // error, nest-inherited constants - uint256[NESTED_INHERITED] internal arr4; // error, same contract constant + uint256[CONST] internal arr4; // nest-inherited constants + uint256[NESTED_INHERITED] internal arr5; // same contract constant } library L2 { @@ -29,7 +31,5 @@ library L2 { } // ---- -// TypeError 5462: (366-372): Invalid array length, expected integer literal or constant expression. -// TypeError 5462: (430-436): Invalid array length, expected integer literal or constant expression. -// TypeError 5462: (742-747): Invalid array length, expected integer literal or constant expression. -// TypeError 5462: (822-838): Invalid array length, expected integer literal or constant expression. +// TypeError 5462: (501-507): Invalid array length, expected integer literal or constant expression. +// TypeError 5462: (564-570): Invalid array length, expected integer literal or constant expression. From 74d4cffafc2897a99c982aa602ba041921a0cb40 Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Sat, 17 May 2025 15:52:33 -0300 Subject: [PATCH 2/9] Support member access --- Changelog.md | 1 + libsolidity/analysis/ConstantEvaluator.cpp | 23 ++++++++++++++++++++++ libsolidity/analysis/ConstantEvaluator.h | 1 + 3 files changed, 25 insertions(+) diff --git a/Changelog.md b/Changelog.md index 18e0deeaf612..b097a84ec2a0 100644 --- a/Changelog.md +++ b/Changelog.md @@ -3,6 +3,7 @@ Language Features: Compiler Features: +* Constant Evaluator: Support for constants referenced by member access expressions. * ethdebug: Experimental support for instructions and source locations under EOF. Bugfixes: diff --git a/libsolidity/analysis/ConstantEvaluator.cpp b/libsolidity/analysis/ConstantEvaluator.cpp index 0d953be93ff4..bd6bb4e59561 100644 --- a/libsolidity/analysis/ConstantEvaluator.cpp +++ b/libsolidity/analysis/ConstantEvaluator.cpp @@ -27,6 +27,8 @@ #include #include +#include + #include using namespace solidity; @@ -407,3 +409,24 @@ void ConstantEvaluator::endVisit(TupleExpression const& _tuple) if (!_tuple.isInlineArray() && _tuple.components().size() == 1) m_values[&_tuple] = evaluate(*_tuple.components().front()); } + +void ConstantEvaluator::endVisit(MemberAccess const& _memberAccess) +{ + if (auto const* parentIdentifier = dynamic_cast(&_memberAccess.expression())) + { + if (auto const* contract = dynamic_cast(parentIdentifier->annotation().referencedDeclaration)) + { + auto contractVariables = contract->stateVariables(); + auto variable = ranges::find_if( + contractVariables, + [&](VariableDeclaration const* _variable) { return _variable->name() == _memberAccess.memberName(); } + ); + + if ( + variable != ranges::end(contractVariables) && + (*variable)->isConstant() + ) + m_values[&_memberAccess] = evaluate(**variable); + } + } +} diff --git a/libsolidity/analysis/ConstantEvaluator.h b/libsolidity/analysis/ConstantEvaluator.h index 297d5f6e80c9..78a9a30f9fa2 100644 --- a/libsolidity/analysis/ConstantEvaluator.h +++ b/libsolidity/analysis/ConstantEvaluator.h @@ -79,6 +79,7 @@ class ConstantEvaluator: private ASTConstVisitor void endVisit(Literal const& _literal) override; void endVisit(Identifier const& _identifier) override; void endVisit(TupleExpression const& _tuple) override; + void endVisit(MemberAccess const& _memberAcess) override; langutil::ErrorReporter& m_errorReporter; /// Current recursion depth. From 094d4e7c6c5edca3b79fab1d008879d88a772d9b Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Wed, 16 Jul 2025 01:45:06 -0300 Subject: [PATCH 3/9] fixup! Add and update tests --- .../syntaxTests/constantEvaluator/member_access.sol | 1 + .../member_access_module_constant.sol | 8 ++++++++ .../member_access_module_contract_constant.sol | 11 +++++++++++ .../constantEvaluator/member_access_non_constant.sol | 8 ++++++++ 4 files changed, 28 insertions(+) create mode 100644 test/libsolidity/syntaxTests/constantEvaluator/member_access_module_constant.sol create mode 100644 test/libsolidity/syntaxTests/constantEvaluator/member_access_module_contract_constant.sol create mode 100644 test/libsolidity/syntaxTests/constantEvaluator/member_access_non_constant.sol diff --git a/test/libsolidity/syntaxTests/constantEvaluator/member_access.sol b/test/libsolidity/syntaxTests/constantEvaluator/member_access.sol index e75ea651569b..b119f7fb810d 100644 --- a/test/libsolidity/syntaxTests/constantEvaluator/member_access.sol +++ b/test/libsolidity/syntaxTests/constantEvaluator/member_access.sol @@ -4,5 +4,6 @@ contract A { contract C is A { uint constant CONST = 2 + A.INHERITED; uint[CONST] array; + uint[1 + A.INHERITED + 2] array2; } // ---- diff --git a/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_constant.sol b/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_constant.sol new file mode 100644 index 000000000000..67a908e3be07 --- /dev/null +++ b/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_constant.sol @@ -0,0 +1,8 @@ +==== Source: A.sol ==== +uint constant CONST = 2; +==== Source: B.sol ==== +import "A.sol" as M; +contract C { + uint[M.CONST] array1; +} +// ---- diff --git a/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_contract_constant.sol b/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_contract_constant.sol new file mode 100644 index 000000000000..c5d8139f6fba --- /dev/null +++ b/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_contract_constant.sol @@ -0,0 +1,11 @@ +==== Source: A.sol ==== +contract A { + uint constant CONST = 2; +} +==== Source: B.sol ==== +import "A.sol" as M; +contract C is M.A { + uint[M.A.CONST] array; +} +// ---- +// TypeError 5462: (B.sol:50-59): Invalid array length, expected integer literal or constant expression. diff --git a/test/libsolidity/syntaxTests/constantEvaluator/member_access_non_constant.sol b/test/libsolidity/syntaxTests/constantEvaluator/member_access_non_constant.sol new file mode 100644 index 000000000000..5645ae1e6f86 --- /dev/null +++ b/test/libsolidity/syntaxTests/constantEvaluator/member_access_non_constant.sol @@ -0,0 +1,8 @@ +contract A { + uint notConst = 1; +} +contract C is A { + uint[A.notConst] array; +} +// ---- +// TypeError 5462: (65-75): Invalid array length, expected integer literal or constant expression. From 8c55ec776306fe337dad1f5d5cecb667aea9e8a4 Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Wed, 16 Jul 2025 01:45:33 -0300 Subject: [PATCH 4/9] fixup! Support member access --- libsolidity/analysis/ConstantEvaluator.cpp | 27 ++++++++++++---------- 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/libsolidity/analysis/ConstantEvaluator.cpp b/libsolidity/analysis/ConstantEvaluator.cpp index bd6bb4e59561..58ca48c76549 100644 --- a/libsolidity/analysis/ConstantEvaluator.cpp +++ b/libsolidity/analysis/ConstantEvaluator.cpp @@ -414,19 +414,22 @@ void ConstantEvaluator::endVisit(MemberAccess const& _memberAccess) { if (auto const* parentIdentifier = dynamic_cast(&_memberAccess.expression())) { - if (auto const* contract = dynamic_cast(parentIdentifier->annotation().referencedDeclaration)) + Declaration const* referencedDeclaration = parentIdentifier->annotation().referencedDeclaration; + std::vector candidateVariables; + if (auto const* contract = dynamic_cast(referencedDeclaration)) + candidateVariables = contract->stateVariables(); + else if (auto const* import = dynamic_cast(referencedDeclaration)) { - auto contractVariables = contract->stateVariables(); - auto variable = ranges::find_if( - contractVariables, - [&](VariableDeclaration const* _variable) { return _variable->name() == _memberAccess.memberName(); } - ); - - if ( - variable != ranges::end(contractVariables) && - (*variable)->isConstant() - ) - m_values[&_memberAccess] = evaluate(**variable); + if (SourceUnit const* sourceUnit = import->annotation().sourceUnit) + candidateVariables = ASTNode::filteredNodes(sourceUnit->nodes()); } + + auto variable = ranges::find_if( + candidateVariables, + [&](VariableDeclaration const* _variable) { return _variable->name() == _memberAccess.memberName(); } + ); + + if (variable != ranges::end(candidateVariables) && (*variable)->isConstant()) + m_values[&_memberAccess] = evaluate(**variable); } } From 2d6060336502c220ea62d5e814d9ef8f628384f4 Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Wed, 16 Jul 2025 18:02:11 -0300 Subject: [PATCH 5/9] fixup! Add and update tests --- .../constantEvaluator/member_access_module_contract_constant.sol | 1 - 1 file changed, 1 deletion(-) diff --git a/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_contract_constant.sol b/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_contract_constant.sol index c5d8139f6fba..f79eac5207dc 100644 --- a/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_contract_constant.sol +++ b/test/libsolidity/syntaxTests/constantEvaluator/member_access_module_contract_constant.sol @@ -8,4 +8,3 @@ contract C is M.A { uint[M.A.CONST] array; } // ---- -// TypeError 5462: (B.sol:50-59): Invalid array length, expected integer literal or constant expression. From ec81d3c2dbb2e08eafe03b6fa072e461f4a5f0a9 Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Wed, 16 Jul 2025 18:02:46 -0300 Subject: [PATCH 6/9] fixup! nested member access --- libsolidity/analysis/ConstantEvaluator.cpp | 37 ++++++++++++++++------ 1 file changed, 28 insertions(+), 9 deletions(-) diff --git a/libsolidity/analysis/ConstantEvaluator.cpp b/libsolidity/analysis/ConstantEvaluator.cpp index 58ca48c76549..52ad10a2a9f4 100644 --- a/libsolidity/analysis/ConstantEvaluator.cpp +++ b/libsolidity/analysis/ConstantEvaluator.cpp @@ -412,10 +412,29 @@ void ConstantEvaluator::endVisit(TupleExpression const& _tuple) void ConstantEvaluator::endVisit(MemberAccess const& _memberAccess) { - if (auto const* parentIdentifier = dynamic_cast(&_memberAccess.expression())) + std::vector candidateVariables; + if (auto const* nestedMemberAccess = dynamic_cast(&_memberAccess.expression())) + { + // The nested expression can only be accessing a contract inside an imported module + auto const* moduleIdentifier = dynamic_cast(&nestedMemberAccess->expression()); + solAssert(moduleIdentifier); + auto const* importedModule = dynamic_cast(moduleIdentifier->annotation().referencedDeclaration); + solAssert(importedModule); + SourceUnit const* sourceUnit = importedModule->annotation().sourceUnit; + solAssert(sourceUnit); + + auto contracts = ASTNode::filteredNodes(sourceUnit->nodes()); + auto contract = ranges::find_if( + contracts, + [&](ContractDefinition const* _contract) { return _contract->name() == nestedMemberAccess->memberName(); } + ); + if (contract != ranges::end(contracts)) + candidateVariables = (*contract)->stateVariables(); + + } + else if (auto const* parentIdentifier = dynamic_cast(&_memberAccess.expression())) { Declaration const* referencedDeclaration = parentIdentifier->annotation().referencedDeclaration; - std::vector candidateVariables; if (auto const* contract = dynamic_cast(referencedDeclaration)) candidateVariables = contract->stateVariables(); else if (auto const* import = dynamic_cast(referencedDeclaration)) @@ -423,13 +442,13 @@ void ConstantEvaluator::endVisit(MemberAccess const& _memberAccess) if (SourceUnit const* sourceUnit = import->annotation().sourceUnit) candidateVariables = ASTNode::filteredNodes(sourceUnit->nodes()); } + } - auto variable = ranges::find_if( - candidateVariables, - [&](VariableDeclaration const* _variable) { return _variable->name() == _memberAccess.memberName(); } - ); + auto variable = ranges::find_if( + candidateVariables, + [&](VariableDeclaration const* _variable) { return _variable->name() == _memberAccess.memberName(); } + ); - if (variable != ranges::end(candidateVariables) && (*variable)->isConstant()) - m_values[&_memberAccess] = evaluate(**variable); - } + if (variable != ranges::end(candidateVariables) && (*variable)->isConstant()) + m_values[&_memberAccess] = evaluate(**variable); } From e18043d2b4b1731ea6c554edcd99516d509c30cd Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Mon, 21 Jul 2025 09:41:50 -0300 Subject: [PATCH 7/9] fixup! nested member access --- libsolidity/analysis/ConstantEvaluator.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/libsolidity/analysis/ConstantEvaluator.cpp b/libsolidity/analysis/ConstantEvaluator.cpp index 52ad10a2a9f4..d420650e22f2 100644 --- a/libsolidity/analysis/ConstantEvaluator.cpp +++ b/libsolidity/analysis/ConstantEvaluator.cpp @@ -415,14 +415,16 @@ void ConstantEvaluator::endVisit(MemberAccess const& _memberAccess) std::vector candidateVariables; if (auto const* nestedMemberAccess = dynamic_cast(&_memberAccess.expression())) { - // The nested expression can only be accessing a contract inside an imported module + // The nested expression should be accessing a contract inside an imported module auto const* moduleIdentifier = dynamic_cast(&nestedMemberAccess->expression()); - solAssert(moduleIdentifier); + if (!moduleIdentifier) + return; auto const* importedModule = dynamic_cast(moduleIdentifier->annotation().referencedDeclaration); - solAssert(importedModule); + if (!importedModule) + return; + SourceUnit const* sourceUnit = importedModule->annotation().sourceUnit; solAssert(sourceUnit); - auto contracts = ASTNode::filteredNodes(sourceUnit->nodes()); auto contract = ranges::find_if( contracts, @@ -430,16 +432,15 @@ void ConstantEvaluator::endVisit(MemberAccess const& _memberAccess) ); if (contract != ranges::end(contracts)) candidateVariables = (*contract)->stateVariables(); - } else if (auto const* parentIdentifier = dynamic_cast(&_memberAccess.expression())) { Declaration const* referencedDeclaration = parentIdentifier->annotation().referencedDeclaration; if (auto const* contract = dynamic_cast(referencedDeclaration)) candidateVariables = contract->stateVariables(); - else if (auto const* import = dynamic_cast(referencedDeclaration)) + else if (auto const* importedModule = dynamic_cast(referencedDeclaration)) { - if (SourceUnit const* sourceUnit = import->annotation().sourceUnit) + if (SourceUnit const* sourceUnit = importedModule->annotation().sourceUnit) candidateVariables = ASTNode::filteredNodes(sourceUnit->nodes()); } } From 4496590f9fc849f730ffd2021641a0a10542cbf3 Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Mon, 21 Jul 2025 09:48:23 -0300 Subject: [PATCH 8/9] [WIP] Updated smt tests --- .../abi/abi_encode_with_selector_array_slice.sol | 6 ++---- .../abi/abi_encode_with_selector_array_slice_2.sol | 4 +--- .../smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol | 2 +- .../smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol | 6 ++---- .../abi/abi_encode_with_sig_array_slice_2.sol | 6 ++---- .../bmc_coverage/compound_bitwise_or_uint_3.sol | 2 +- .../external_calls/external_call_indirect_2.sol | 2 +- .../external_calls/external_call_indirect_3.sol | 2 +- .../external_calls/external_call_indirect_5.sol | 2 +- .../smtCheckerTests/functions/getters/array_2.sol | 2 +- .../operators/compound_bitwise_or_uint_1.sol | 3 +-- .../operators/compound_bitwise_or_uint_3.sol | 2 +- 12 files changed, 15 insertions(+), 24 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol index 25f08dff48ee..10ca5e5af23e 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol @@ -27,8 +27,6 @@ contract C { // SMTIgnoreCex: yes // SMTIgnoreOS: macos // ---- -// Warning 6328: (325-355): CHC: Assertion violation happens here. +// Warning 6328: (325-355): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\ndata = [0x52]\nb2 = [0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(0x0, [0x52]) // Warning 6328: (578-608): CHC: Assertion violation happens here. -// Warning 6328: (691-721): CHC: Assertion violation happens here. -// Warning 6328: (959-989): CHC: Assertion violation happens here. -// Warning 6328: (1079-1109): CHC: Assertion violation happens here. +// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol index d2446c5f92e6..fd489283ce08 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol @@ -29,6 +29,4 @@ contract C { // ---- // Warning 6328: (326-356): CHC: Assertion violation happens here. // Warning 6328: (579-609): CHC: Assertion violation happens here. -// Warning 6328: (692-722): CHC: Assertion violation happens here. -// Warning 6328: (960-990): CHC: Assertion violation happens here. -// Warning 6328: (1080-1110): CHC: Assertion violation happens here. +// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol index e4b42c926378..4b4f7a3ace98 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol @@ -12,4 +12,4 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 6328: (330-360): CHC: Assertion violation might happen here. -// Warning 4661: (330-360): BMC: Assertion violation happens here. +// Warning 7812: (330-360): BMC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol index 3bc9da4d63fe..6167cc670b23 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol @@ -24,11 +24,9 @@ contract C { } // ==== // SMTEngine: chc -// SMTIgnoreOS: macos // SMTIgnoreCex: yes +// SMTIgnoreOS: macos // ---- // Warning 6328: (334-364): CHC: Assertion violation happens here. // Warning 6328: (588-618): CHC: Assertion violation happens here. -// Warning 6328: (702-732): CHC: Assertion violation happens here. -// Warning 6328: (971-1001): CHC: Assertion violation happens here. -// Warning 6328: (1086-1116): CHC: Assertion violation happens here. +// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol index dbf28814d0ea..0128d5e433e7 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol @@ -24,11 +24,9 @@ contract C { } // ==== // SMTEngine: chc -// SMTIgnoreOS: macos // SMTIgnoreCex: yes +// SMTIgnoreOS: macos // ---- // Warning 6328: (335-365): CHC: Assertion violation happens here. // Warning 6328: (589-619): CHC: Assertion violation happens here. -// Warning 6328: (703-733): CHC: Assertion violation happens here. -// Warning 6328: (972-1002): CHC: Assertion violation happens here. -// Warning 6328: (1087-1117): CHC: Assertion violation happens here. +// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol index 9562653806df..02d538d7d64c 100644 --- a/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol +++ b/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol @@ -12,4 +12,4 @@ contract C { // SMTEngine: bmc // SMTShowUnproved: no // ---- -// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 2788: BMC: 1 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/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol index 16779bb89a1f..884ffbd6b8b7 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol @@ -50,5 +50,5 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 6328: (434-455): CHC: Assertion violation happens here. -// Warning 6328: (1270-1291): CHC: Assertion violation happens here. +// Warning 6328: (1270-1291): CHC: Assertion violation might happen here. // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol index 3e8e4f409650..ff17649dd968 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol @@ -42,5 +42,5 @@ contract C { // SMTExtCalls: trusted // SMTIgnoreOS: macos // ---- -// Warning 6328: (561-582): CHC: Assertion violation happens here. +// Warning 6328: (561-582): CHC: Assertion violation might happen here. // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol index 26d39838ef4b..9313858ce2b1 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol @@ -47,5 +47,5 @@ contract C { // SMTEngine: chc // SMTExtCalls: trusted // ---- -// Warning 6328: (601-622): CHC: Assertion violation happens here. +// Warning 6328: (601-622): CHC: Assertion violation might happen here. // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol index 2d92413d5e24..45e9008a3bf0 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol @@ -19,5 +19,5 @@ contract C { // SMTEngine: all // SMTIgnoreCex: no // ---- -// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\na = [[], [], [0, 0, 0, 0]]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [[], [], [0, 0, 0, 0]]\nC.f() +// Warning 6328: (242-256): CHC: Assertion violation happens here. // Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol index f0916cf7e869..53d8ecc8b5ce 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol @@ -13,5 +13,4 @@ contract C { // Warning 6368: (76-80): CHC: Out of bounds access might happen here. // Warning 6368: (115-119): CHC: Out of bounds access might happen here. // Warning 6368: (141-145): CHC: Out of bounds access might happen here. -// Warning 6328: (134-151): CHC: Assertion violation might happen here. -// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol index ff246b362c54..2650b08975bd 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol @@ -12,4 +12,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (125-140): CHC: Assertion violation might happen here. -// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 7812: (125-140): BMC: Assertion violation might happen here. From e000da606a8275a23f9382d67cee1c2ddda15b7a Mon Sep 17 00:00:00 2001 From: Matheus Aguiar Date: Mon, 21 Jul 2025 22:55:55 -0300 Subject: [PATCH 9/9] fixup! Add and update tests --- .../constantEvaluator/member_access_library_constant.sol | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test/libsolidity/syntaxTests/constantEvaluator/member_access_library_constant.sol diff --git a/test/libsolidity/syntaxTests/constantEvaluator/member_access_library_constant.sol b/test/libsolidity/syntaxTests/constantEvaluator/member_access_library_constant.sol new file mode 100644 index 000000000000..6fad2ca2ae2a --- /dev/null +++ b/test/libsolidity/syntaxTests/constantEvaluator/member_access_library_constant.sol @@ -0,0 +1,7 @@ +library L { + uint public constant CONST = 32; +} +contract C { + uint[L.CONST] a; +} +// ---- \ No newline at end of file