From c091f53e691b4d70cd92d785185ab6fef407ee3e Mon Sep 17 00:00:00 2001 From: Taras Date: Sat, 7 Jun 2025 02:25:44 -0500 Subject: [PATCH] Fix internal function summary support for missing bytecode return types Internal functions parsed from bytecode often lack return type information (empty 'res' field), while CVL summaries specify return types. This caused "Bad internal method returns: Different arities" errors when trying to merge signatures. This fix adds special handling in two places: 1. CVLASTBuilder: Trust CVL-specified return types when bytecode has none 2. QualifiedFunctionName.mergeReturns: Handle asymmetric return types This enables summarization of internal functions like OpenZeppelin's Context._msgSender() which are commonly used for access control. Added test case in Public/TestEVM/Summarization/InternalFunctionReturns/ demonstrating the fix with a minimal Context pattern implementation. --- .../InternalFunctionReturns/Context.sol | 15 ++++++++ .../InternalFunctionReturns/README.md | 18 +++++++++ .../InternalFunctionReturns/TestContract.sol | 26 +++++++++++++ .../InternalFunctionReturns/test.spec | 38 +++++++++++++++++++ .../src/main/kotlin/spec/CVLASTBuilder.kt | 17 +++++++-- .../spec/cvlast/QualifiedFunctionName.kt | 10 +++++ 6 files changed, 120 insertions(+), 4 deletions(-) create mode 100644 Public/TestEVM/Summarization/InternalFunctionReturns/Context.sol create mode 100644 Public/TestEVM/Summarization/InternalFunctionReturns/README.md create mode 100644 Public/TestEVM/Summarization/InternalFunctionReturns/TestContract.sol create mode 100644 Public/TestEVM/Summarization/InternalFunctionReturns/test.spec diff --git a/Public/TestEVM/Summarization/InternalFunctionReturns/Context.sol b/Public/TestEVM/Summarization/InternalFunctionReturns/Context.sol new file mode 100644 index 00000000..1cf31b0e --- /dev/null +++ b/Public/TestEVM/Summarization/InternalFunctionReturns/Context.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +/** + * @dev Provides information about the current execution context + */ +abstract contract Context { + function _msgSender() internal view virtual returns (address) { + return msg.sender; + } + + function _msgData() internal view virtual returns (bytes calldata) { + return msg.data; + } +} diff --git a/Public/TestEVM/Summarization/InternalFunctionReturns/README.md b/Public/TestEVM/Summarization/InternalFunctionReturns/README.md new file mode 100644 index 00000000..7772cea2 --- /dev/null +++ b/Public/TestEVM/Summarization/InternalFunctionReturns/README.md @@ -0,0 +1,18 @@ +# Internal Function Return Type Merging Test + +This test verifies that internal function summaries work correctly when the bytecode lacks return type information. + +## Problem +Internal functions parsed from bytecode often don't have return type information (empty `returns` field), while CVL summaries specify return types. This caused an arity mismatch error when trying to merge the signatures. + +## Solution +The fix allows CVL to specify return types for internal functions even when the bytecode doesn't provide this information. + +## Test Components +- `Context.sol` - Minimal implementation of OpenZeppelin's Context pattern with `_msgSender()` internal function +- `TestContract.sol` - Contract using `_msgSender()` for access control +- `test.spec` - CVL specification that summarizes `_msgSender()` to return `e.msg.sender` + +## Test Cases +1. **nonOwnerCannotCallDoSomething** - Verifies that non-owners cannot call protected functions +2. **ownerCanCallDoSomething** - Verifies that owners can call protected functions (using the internal function summary) diff --git a/Public/TestEVM/Summarization/InternalFunctionReturns/TestContract.sol b/Public/TestEVM/Summarization/InternalFunctionReturns/TestContract.sol new file mode 100644 index 00000000..4933a88b --- /dev/null +++ b/Public/TestEVM/Summarization/InternalFunctionReturns/TestContract.sol @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "./Context.sol"; + +contract TestContract is Context { + address public owner; + + constructor() { + owner = _msgSender(); + } + + modifier onlyOwner() { + require(_msgSender() == owner, "Not the owner"); + _; + } + + function setOwner(address newOwner) external onlyOwner { + owner = newOwner; + } + + function doSomething() external onlyOwner returns (bool) { + // Only owner can call this + return true; + } +} diff --git a/Public/TestEVM/Summarization/InternalFunctionReturns/test.spec b/Public/TestEVM/Summarization/InternalFunctionReturns/test.spec new file mode 100644 index 00000000..fd7f2a02 --- /dev/null +++ b/Public/TestEVM/Summarization/InternalFunctionReturns/test.spec @@ -0,0 +1,38 @@ +methods { + function owner() external returns (address) envfree; + function doSomething() external returns (bool); + + // Try using a wildcard summary instead of Context._msgSender() + function _._msgSender() internal with(env e) => e.msg.sender expect address; +} + +// Rule to verify that the owner can successfully call doSomething +rule ownerCanCallDoSomething { + env e; + + // Ensure the caller is the owner + require e.msg.sender == owner(); + + // Call doSomething - should not revert + bool result = doSomething@withrevert(e); + + // Assert that it succeeded (did not revert) + assert !lastReverted, "Owner should be able to call doSomething"; + + // Assert that it returned true + assert result == true, "doSomething should return true"; +} + +// Rule to verify that non-owners cannot call doSomething +rule nonOwnerCannotCallDoSomething { + env e; + + // Ensure the caller is NOT the owner + require e.msg.sender != owner(); + + // Call doSomething - should revert + doSomething@withrevert(e); + + // Assert that it reverted + assert lastReverted, "Non-owner should not be able to call doSomething"; +} diff --git a/lib/Shared/src/main/kotlin/spec/CVLASTBuilder.kt b/lib/Shared/src/main/kotlin/spec/CVLASTBuilder.kt index 0c6100db..5d17ea92 100644 --- a/lib/Shared/src/main/kotlin/spec/CVLASTBuilder.kt +++ b/lib/Shared/src/main/kotlin/spec/CVLASTBuilder.kt @@ -789,10 +789,19 @@ class CVLAstBuilder( } } else { check(annot.methodParameterSignature is MethodSignature) - MergeableSignature.mergeReturns(matching.first().second, annot.methodParameterSignature).bindEither( - errorCallback = { errorList -> CVLError.General(annot.range, "Bad internal method returns: ${errorList.joinToString(", ")}").asError()}, - resultCallback = { ok } - ) + val matchedSignature = matching.first().second + // Special handling for internal functions: if the bytecode signature has no return types + // but the CVL signature does, use the CVL signature's return types + if (matchedSignature.res.isEmpty() && annot.methodParameterSignature.res.isNotEmpty()) { + // Internal functions from bytecode often don't have return type information + // In this case, trust the CVL specification + ok + } else { + MergeableSignature.mergeReturns(matchedSignature, annot.methodParameterSignature).bindEither( + errorCallback = { errorList -> CVLError.General(annot.range, "Bad internal method returns: ${errorList.joinToString(", ")}").asError()}, + resultCallback = { ok } + ) + } } } } diff --git a/lib/Shared/src/main/kotlin/spec/cvlast/QualifiedFunctionName.kt b/lib/Shared/src/main/kotlin/spec/cvlast/QualifiedFunctionName.kt index 9deba1bc..2d1fd419 100644 --- a/lib/Shared/src/main/kotlin/spec/cvlast/QualifiedFunctionName.kt +++ b/lib/Shared/src/main/kotlin/spec/cvlast/QualifiedFunctionName.kt @@ -692,6 +692,16 @@ object MergeableSignature { } fun mergeReturns(m1: MethodSignature, m2: MethodSignature) : CollectingResult, String> { + // Special case for internal functions: if one signature has no return types (from bytecode) + // and the other has return types (from CVL), use the one with return types + if (m1.res.isEmpty() && m2.res.isNotEmpty()) { + // m1 (bytecode) has no return type info, trust m2 (CVL) + return m2.res.lift() + } else if (m2.res.isEmpty() && m1.res.isNotEmpty()) { + // m2 (bytecode) has no return type info, trust m1 (CVL) + return m1.res.lift() + } + return mergeVMParams(m1.res, m2.res).bindEither( resultCallback = { it.lift() }, errorCallback = { errs ->