18.02.26 Release

18.02.26 Release

fc7d2c6ac530bbee5bde329a9d3d8d44ecc0a2af

Author: yoav-el-certora

Public/TestEVM/FromBugs/CERT-9946/C.sol

@@ -0,0 +1,21 @@
+contract C {
+    uint256 fooCalled = 0;
+    uint256 barCalled = 0;
+    function foo(address x, address z) public returns (uint) {
+        if(x == address(0)){
+            return 0;
+        }
+        address(x).call(abi.encodeWithSignature("bar(address,address)"));
+        fooCalled = fooCalled + 1;
+        return 1;
+    }
+
+    function bar(address y, address z) public returns (uint) {
+        if(y == address(0)){
+            return 0;
+        }
+        address(y).call(abi.encodeWithSignature("foo(address,address)"));
+        barCalled = barCalled + 1;
+        return 1;
+    }
+}

Public/TestEVM/FromBugs/CERT-9946/C.spec

@@ -0,0 +1,13 @@
+methods {
+    function currentContract._ external => HAVOC_ALL;
+    function _.bar(address, address) external => DISPATCHER(true);
+}
+
+rule recurse(method f) {
+    address x;
+    address y;
+    env e;
+    require currentContract.fooCalled == 0 && currentContract.barCalled == 0, "Some initial values";
+    foo(e, x, y);
+    satisfy currentContract.fooCalled == 999 && currentContract.barCalled == 42, "there should be a HAVOC_ALL that will allow these values";
+}

Public/TestEVM/FromBugs/CERT-9946/Default.conf

@@ -0,0 +1,6 @@
+{
+	"files": [
+		"C.sol",
+	],
+	"verify": "C:C.spec",
+}

Public/TestEVM/FromBugs/CERT-9946/expectedDefault.json

@@ -0,0 +1,5 @@
+{
+	"rules": {
+		"recurse": "SUCCESS"
+	}
+}

lib/GeneralUtils/src/main/kotlin/utils/ExtStdlib.kt

@@ -1312,6 +1312,8 @@ fun ClosedRange<BigInteger>.stepBy(step: BigInteger) = sequence<BigInteger> {
     }
 }
 
+fun UInt.checkedMinus(other: UInt): UInt? = if (this >= other) { this - other } else { null }
+
 /**
     Runs the given [block] returns its result wrapped in a [Result].  Any exceptions other than [CancellationException]
     are caught and returned as a failure result.  If a [CancellationException] is thrown, it is rethrown, allowing this

lib/Shared/src/main/kotlin/config/Config.kt

@@ -969,7 +969,21 @@ object Config {
     val MoveModulePath =
         object : ConfigType.StringCmdLine(
             null,
-            Option("movePath", true, "Directory to search for Move modules")
+            Option(
+                "movePath",
+                true,
+                "Directory to search for Move modules.  Ordinarily derived from the spec package path."
+            )
+        ) {}
+
+    val SuiPackageSummaryPath =
+        object : ConfigType.StringCmdLine(
+            null,
+            Option(
+                "suiPackageSummaryPath",
+                true,
+                "Directory with Sui package summary info.  Ordinarily derived from the spec package path."
+            )
         ) {}
 
     val MovePublicSanityCheck = object : ConfigType.BooleanCmdLine(

lib/Shared/src/main/kotlin/config/DestructiveOptimizationsModeEnum.kt

@@ -19,6 +19,7 @@ package config
 
 import cli.ConversionException
 import cli.Converter
+import datastructures.stdcollections.*
 
 enum class DestructiveOptimizationsModeEnum {
     /** Disable destructive optimizations */
@@ -42,3 +43,12 @@ val DestructiveOptimizationsModeConverter = Converter {
         else -> throw ConversionException(it, DestructiveOptimizationsModeEnum::class.java)
     }
 }
+
+fun DestructiveOptimizationsModeEnum.isTwoStageMode(): Boolean {
+    return when(this) {
+        DestructiveOptimizationsModeEnum.TWOSTAGE,
+        DestructiveOptimizationsModeEnum.TWOSTAGE_CHECKED -> true
+        DestructiveOptimizationsModeEnum.DISABLE,
+        DestructiveOptimizationsModeEnum.ENABLE -> false
+    }
+}

lib/Shared/src/main/kotlin/config/ReportTypes.kt

@@ -190,7 +190,6 @@ enum class ReportTypes(val loggerCategory: LoggerTypes) : DumpType, CategoryName
     REMOVE_UNUSED_WRITES(LoggerTypes.OPTIMIZE),
     REMOVE_UNUSED_PARTITIONS(LoggerTypes.OPTIMIZE),
     REWRITE_COPY_LOOP(LoggerTypes.OPTIMIZE),
-    REMOVE_CALL_ANNOTATIONS(LoggerTypes.OPTIMIZE),
     PATH_OPTIMIZE0(LoggerTypes.OPTIMIZE),
     MATERIALIZE_DISJOINT_HASHES(LoggerTypes.INSTRUMENTATION),
     ASSUME_STRICT_MONOTONIC_FP(LoggerTypes.INSTRUMENTATION),
@@ -239,7 +238,7 @@ enum class ReportTypes(val loggerCategory: LoggerTypes) : DumpType, CategoryName
     AXIOM_INLINING(LoggerTypes.INSTRUMENTATION),
     CANONICALIZE_SCALARSET(LoggerTypes.OPTIMIZE),
     GHOST_SUM_INSTRUMENTER(LoggerTypes.INSTRUMENTATION),
-    SNIPPET_REMOVAL(LoggerTypes.PRUNING),
+    ANNOTATION_REMOVAL(LoggerTypes.PRUNING),
     ENVFREE(LoggerTypes.SPEC),
     CANONICALIZATION(LoggerTypes.SPEC),
     STORAGE_REWRITER(LoggerTypes.INLINER),