Fix Internal Function Summary Support (#20)

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;
+    }
+}

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)

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;
+    }
+}

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";
+}

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 }
+                                        )
+                                    }
                                 }
                             }
                         }

lib/Shared/src/main/kotlin/spec/cvlast/QualifiedFunctionName.kt

@@ -692,6 +692,16 @@ object MergeableSignature {
     }
 
     fun mergeReturns(m1: MethodSignature, m2: MethodSignature) : CollectingResult<List<VMParam>, 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 ->