26.02.26 Release

26.02.26 Release

b923324d63bc0fdefeff0007c11ca3b7047abc49

Author: yoav-el-certora

.circleci/config.yml

@@ -173,7 +173,7 @@ commands:
 jobs:
   build:
     docker:
-      - image: &img public.ecr.aws/certora/cvt-image:2025.05.12-4993-b9e8bfc
+      - image: &img public.ecr.aws/certora/cvt-image:2026.02.23-5696-87a3342
     working_directory: ~/repo
     environment:
       # configure sccache usage

Public/TestEVM/Clz/C.conf

@@ -0,0 +1,7 @@
+{
+    "files": [
+        "C.sol"
+    ],
+    "solc": "solc8.31",
+    "verify": "C:C.spec"
+}

Public/TestEVM/Clz/C.sol

@@ -0,0 +1,7 @@
+contract C {
+    function clz(uint256 x) pure public returns (uint256 r) {
+        assembly {
+            r := clz(x)
+        }
+    }
+}

Public/TestEVM/Clz/C.spec

@@ -0,0 +1,22 @@
+methods {
+    function clz(uint256) external returns (uint256) envfree;
+}
+
+rule clz() {
+    uint256 x = 127;
+    uint256 r = clz(x);
+    assert r <= 256;
+    mathint bound = 2^(256 - r);
+    assert x < bound;
+    assert x >= bound / 2;
+}
+
+rule clz_tests {
+    // https://eips.ethereum.org/EIPS/eip-7939#test-cases
+    assert clz(0x0000000000000000000000000000000000000000000000000000000000000000) == 0x0000000000000000000000000000000000000000000000000000000000000100;
+    assert clz(0x8000000000000000000000000000000000000000000000000000000000000000) == 0x0000000000000000000000000000000000000000000000000000000000000000;
+    assert clz(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) == 0x0000000000000000000000000000000000000000000000000000000000000000;
+    assert clz(0x4000000000000000000000000000000000000000000000000000000000000000) == 0x0000000000000000000000000000000000000000000000000000000000000001;
+    assert clz(0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) == 0x0000000000000000000000000000000000000000000000000000000000000001;
+    assert clz(0x0000000000000000000000000000000000000000000000000000000000000001) == 0x00000000000000000000000000000000000000000000000000000000000000ff;
+}

Public/TestEVM/Clz/C_bv.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "C.sol"
+    ],
+    "solc": "solc8.31",
+    "verify": "C:C.spec",
+    "smt_use_bv": true
+}

Public/TestEVM/Clz/expectedC.json

@@ -0,0 +1,11 @@
+{
+	"rules": {
+		"clz": "SUCCESS",
+		"clz_tests": "SUCCESS",
+		"envfreeFuncsStaticCheck": {
+			"SUCCESS": [
+				"clz(uint256)"
+			]
+		}
+	}
+}

Public/TestEVM/Clz/expectedC_bv.json

@@ -0,0 +1,11 @@
+{
+	"rules": {
+		"clz": "SUCCESS",
+		"clz_tests": "SUCCESS",
+		"envfreeFuncsStaticCheck": {
+			"SUCCESS": [
+				"clz(uint256)"
+			]
+		}
+	}
+}

lib/GeneralUtils/src/main/kotlin/algorithms/Reachability.kt

@@ -81,3 +81,43 @@ inline fun <V> traverseBFS(start: Iterable<V>, nexts: (V) -> Iterable<V>?): Unit
 inline fun <V> traverseBFS1(start: V, nexts: (V) -> Iterable<V>?): Unit {
     traverseBFS(listOf(start), nexts)
 }
+
+/**
+ * Compacts a graph to only include edges between target nodes.
+ * Intermediate (non-target) nodes are collapsed, creating direct edges between target nodes.
+ *
+ * For each target node, finds all other target nodes reachable from it through paths
+ * that may traverse non-target intermediate nodes.
+ *
+ *
+ * @param targetNodes Nodes to keep in the compacted graph
+ * @param nexts Function returning successors for each node
+ * @return MultiMap representing the compacted graph's adjacency list
+ */
+inline fun <V> compactGraph(targetNodes: Set<V>, crossinline nexts: (V) -> Iterable<V>?): MultiMap<V, V> {
+    val result = mutableMapOf<V, Set<V>>()
+
+    for (startNode in targetNodes) {
+        // Get immediate successors of this target node
+        val immediateSuccessors = nexts(startNode) ?: emptyList()
+
+        // Find all target nodes reachable through non-target intermediate nodes
+        val reachableTargets = getReachable(immediateSuccessors) { node ->
+            if (node in targetNodes) {
+                // Reached a target node - include it but don't traverse further
+                null
+            } else {
+                // Non-target node - traverse through it
+                nexts(node)
+            }
+        }
+
+        // Store all reachable target nodes as successors
+        val targets = reachableTargets.filter { it in targetNodes }.toSet()
+        if (targets.isNotEmpty()) {
+            result[startNode] = targets
+        }
+    }
+
+    return result
+}

lib/Shared/src/main/kotlin/compiler/SourceContext.kt

@@ -18,13 +18,15 @@
 package compiler
 
 import com.certora.collect.*
+import config.Config
 import log.Logger
 import log.LoggerTypes
 import report.TreeViewLocation
 import utils.Range
 import utils.*
 import java.io.File
 import java.io.Serializable
+import kotlin.io.path.Path
 
 private val logger = Logger(LoggerTypes.COMMON)
 
@@ -130,6 +132,8 @@ data class SourceSegment(
             )
         }
 
+
+
         fun resolveFromContext(context: SourceContext, identifier: SourceIdentifier): SourceSegment? {
             val sourceFile = identifier.resolve(context) ?: return null
             val relativeFile = identifier.relativeSourceFile(context)?.toString() ?: return null
@@ -138,6 +142,44 @@ data class SourceSegment(
     }
 }
 
+/**
+ * Takes a [range] and approximates the [compiler.SourceSegment] for it.
+ *
+ * Note, that this function is used in Solana where a Range doesn't have a precise end
+ * and the returned [compiler.SourceSegment]'s content will just start at
+ * [range]'s start and contain the remaining content of the start line.
+ */
+fun Range.Range?.toHeuristicSourceSegment(): SourceSegment? {
+    val sourceFile = this?.file ?: return null
+    val (allBytes, lineStarts) = try {
+        val sourceFilePath = Path(sourceFile)
+        val s = if(sourceFilePath.isAbsolute){
+            CertoraFileCache.tryResolvePathInCargoHome(sourceFile)?.toString() ?: sourceFile
+        } else{
+            Config.prependSourcesDir(sourceFile)
+        }
+        CertoraFileCache.byteContent(s) to CertoraFileCache.lineStarts(s)
+    } catch (e: CertoraFileCacheException) {
+        logger.warn(e.cause) { "Had error when reading from source file $sourceFile" }
+        return null
+    }
+    val startIndex =
+        lineStarts.lineNumberStartOffset(start.line.toInt())?.let { it + start.charByteOffset.toInt() }
+            ?: return null
+    // This is a heuristic, we don't have the full range, but only the start. As end range we define the offset
+    // at the end of the start line, or if not existent, the remaining content of the file. The result
+    // is that content of the returned SourceSegment will be the start line until the end of this line.
+    val endIndex = lineStarts.lineNumberStartOffset(start.line.toInt() + 1) ?: allBytes.size
+
+    if (startIndex >= allBytes.size) {
+        logger.warn { "Trying to source contents starting at ($startIndex) which is out of the bounds of the file content of ($sourceFile)" }
+        return null
+    }
+    return SourceSegment(
+        this,
+        content = String(allBytes, startIndex, endIndex - startIndex).removeNonPrintableChars()
+    )
+}
 
 @Suppress("ForbiddenMethodCall") // for Regex
 private fun String.removeNonPrintableChars() = replace(Regex( "[^\\P{C}\\s]"), "").let {

lib/Shared/src/main/kotlin/disassembler/EVMInstruction.kt

@@ -73,6 +73,7 @@ enum class EVMInstruction(
     SHL(0x1bu, 2, 1),
     SHR(0x1cu, 2, 1),
     SAR(0x1du, 2, 1),
+    CLZ(0x1eu, 1, 1),
     KECCAK256(0x20u, 2, 1),
     ADDRESS(0x30u, 0, 1),
     BALANCE(0x31u, 1, 1),