14.12.25 Release

14.12.25 Release

75d6c9b97dff2712b7bce2b623446fe2d2df7832

Author: yoav-el-certora

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "scripts/graphcore"]
+	path = scripts/graphcore
+	url = git@github.com:Certora/graphcore.git

Public/CITests/testCertoraClient.py

@@ -230,8 +230,6 @@ def test_valid_runs(self) -> None:
                              run_flags=[f"{_p('A.sol')}:B", '--verify', f"B:{_p('spec1.spec')}"])
         suite.expect_success(description='multiple files single assert',
                              run_flags=[_p('A.sol'), _p('B.sol'), '--verify', f"A:{_p('spec1.spec')}"])
-        suite.expect_success(description='file is repeated',
-                             run_flags=[f"{_p('A.sol')}:B", f"{_p('A.sol')}:B", '--verify', f"B:{_p('spec1.spec')}"])
         suite.expect_success(description='2 contracts in a single file',
                              run_flags=[f"{_p('A.sol')}:B", _p('A.sol'), '--verify', f"B:{_p('spec1.spec')}"])
         suite.expect_success(description='--verify with spec file',
@@ -355,8 +353,6 @@ def test_valid_runs(self) -> None:
         suite.expect_success(description='valid --struct_link multiple entries',
                              run_flags=[_p('A.sol'), _p('B.sol'), '--verify', f"A:{_p('spec1.spec')}", '--struct_link',
                                         'A:1=B', 'A:2=B', 'A:1009=A'])
-        suite.expect_success(description='valid --struct_link duplicate entries',
-                             run_flags=[_p('A.sol'), '--verify', f"A:{_p('spec1.spec')}", '--struct_link', 'A:0XC=A', 'A:0XC=A'])
         suite.expect_success(description='valid --build_only',
                              run_flags=[_p('A.sol'), '--verify', f"A:{_p('spec1.spec')}", '--build_only'])
         suite.expect_success(description='valid --build_only duplicate entries',
@@ -548,6 +544,10 @@ def test_invalid_runs(self) -> None:
                              run_flags=[_p('A.sol'), '--verify', f"A:{_p('spec1.spec')}", '--compilation_steps_only',
                                         '--build_only'],
                              expected="cannot use both 'compilation_steps_only' and 'build_only'")
+        suite.expect_failure(description='valid --struct_link duplicate entries',
+                             run_flags=[_p('A.sol'), '--verify', f"A:{_p('spec1.spec')}",
+                                        '--struct_link', 'A:0XC=A', 'A:0XC=A'],
+                             expected="The value of attribute 'struct_link' contains duplicate entries")
         suite.expect_failure(description="illegal struct_link",
                              run_flags=[_p('tac_file.conf'), '--struct_link', 'tac_file:0=tac_file'],
                              expected="'struct_link' argument tac_file:0=tac_file is illegal")
@@ -585,6 +585,9 @@ def test_invalid_runs(self) -> None:
         suite.expect_failure(description="other files with conf file",
                              run_flags=[_p('tac_file.conf'), _p('empty.tac')],
                              expected="No other files are allowed when using a config file")
+        suite.expect_failure(description='file is repeated',
+                             run_flags=[f"{_p('A.sol')}:B", f"{_p('A.sol')}:B", '--verify', f"B:{_p('spec1.spec')}"],
+                             expected="The value of attribute 'files' contains duplicate entries")
         suite.expect_failure(description="illegal contract in verify",
                              run_flags=[_p('empty.tac'), '--verify', f"A:{_p('spec1.spec')}"],
                              expected="'verify' argument, A, doesn't match any contract name")
@@ -817,7 +820,7 @@ def test_package_file(self) -> None:
         def check_run(expect: List[str]) -> None:
             packages_attr = getattr(result, 'packages', None)
             assert packages_attr, f"{description}: package is None"
-            got = sorted([dep.split('=')[0] for dep in packages_attr])
+            got = sorted([dep.split('=')[0].rstrip('/') for dep in packages_attr])
             assert expect == got, f"{description}. Expected: {expect}. Got: {got}"
 
         suite = TestUtil.ProverTestSuite(conf_file_template=_p('mutation_conf_top_level.conf'),
@@ -830,37 +833,44 @@ def check_run(expect: List[str]) -> None:
         assert not packages, f"expected 'packages' to be None. Got: {result.packages}"
 
         remapping = "a=lib\nb=lib"
-        with open(Util.REMAPPINGS_FILE, "w") as file:
-            file.write(remapping)
-        description = f"running with {Util.REMAPPINGS_FILE}"
-        result = suite.expect_checkpoint(description=description)
-        check_run(['a', 'b'])
-
-        remapping = '{"dependencies": {"c": "^3.4.1"},"devDependencies": {"d": "^5.0.8"}}'
-        with open(Util.PACKAGE_FILE, "w") as file:
-            file.write(remapping)
-        description = f"running with {Util.REMAPPINGS_FILE} and {Util.PACKAGE_FILE}"
-        result = suite.expect_checkpoint(description=description)
-        check_run(['a', 'b', 'c', 'd'])
+        try:
+            with open(Util.REMAPPINGS_FILE, "w") as file:
+                file.write(remapping)
+            description = f"running with {Util.REMAPPINGS_FILE}"
+            result = suite.expect_checkpoint(description=description)
+            check_run(['a', 'b'])
+
+            remapping = '{"dependencies": {"c": "^3.4.1"},"devDependencies": {"d": "^5.0.8"}}'
+            with open(Util.PACKAGE_FILE, "w") as file:
+                file.write(remapping)
+            description = f"running with {Util.REMAPPINGS_FILE} and {Util.PACKAGE_FILE}"
+            result = suite.expect_checkpoint(description=description)
+            check_run(['a', 'b', 'c', 'd'])
+        finally:
+            Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
 
         description = "--packages - ignore files"
         result = suite.expect_checkpoint(description=description, run_flags=['--packages', 'd=lib'])
         check_run(['d'])
 
         # duplications
         remapping = "a=lib\na=lib"
-        with open(Util.REMAPPINGS_FILE, "w") as file:
-            file.write(remapping)
-        description = f"identical duplicates in {Util.REMAPPINGS_FILE}"
-        suite.expect_success(description=description)
-        Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
+        try:
+            with open(Util.REMAPPINGS_FILE, "w") as file:
+                file.write(remapping)
+            description = f"identical duplicates in {Util.REMAPPINGS_FILE}"
+            suite.expect_success(description=description)
+        finally:
+            Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
 
         remapping = "a=lib\na=lib2"
-        with open(Util.REMAPPINGS_FILE, "w") as file:
-            file.write(remapping)
-        description = f"non-identical duplicates in {Util.REMAPPINGS_FILE}"
-        suite.expect_failure(description=description, expected="Conflicting values in remappings.txt for key 'a'")
-        Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
+        try:
+            with open(Util.REMAPPINGS_FILE, "w") as file:
+                file.write(remapping)
+            description = f"non-identical duplicates in {Util.REMAPPINGS_FILE}"
+            suite.expect_failure(description=description, expected="Conflicting values in remappings.txt for key 'a'")
+        finally:
+            Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
 
         remapping = '{"dependencies": {"c": "^3.4.1"},"devDependencies": {"c": "^5.0.8"}}'
         with open(Util.PACKAGE_FILE, "w") as file:
@@ -870,24 +880,28 @@ def check_run(expect: List[str]) -> None:
         Path(Util.PACKAGE_FILE).unlink(missing_ok=True)
 
         remapping = "a=lib\nb=lib"
-        with open(Util.REMAPPINGS_FILE, "w") as file:
-            file.write(remapping)
-        remapping = '{"dependencies": {"b": "^3.4.1"},"devDependencies": {"c": "^5.0.8"}}'
-        with open(Util.PACKAGE_FILE, "w") as file:
-            file.write(remapping)
-        description = f"duplicates in {Util.REMAPPINGS_FILE} and Util.PACKAGE_FILE"
-        suite.expect_failure(description=description, expected="package.json and remappings.txt include duplicated")
-        Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
-        Path(Util.PACKAGE_FILE).unlink(missing_ok=True)
+        try:
+            with open(Util.REMAPPINGS_FILE, "w") as file:
+                file.write(remapping)
+            remapping = '{"dependencies": {"b": "^3.4.1"},"devDependencies": {"c": "^5.0.8"}}'
+            with open(Util.PACKAGE_FILE, "w") as file:
+                file.write(remapping)
+            description = f"duplicates in {Util.REMAPPINGS_FILE} and Util.PACKAGE_FILE"
+            suite.expect_failure(description=description, expected="package.json and remappings.txt include duplicated")
+        finally:
+            Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
+            Path(Util.PACKAGE_FILE).unlink(missing_ok=True)
 
 
         remapping = "a=lib\nb=lib=lib2"
-        with open(Util.REMAPPINGS_FILE, "w") as file:
-            file.write(remapping)
+        try:
+            with open(Util.REMAPPINGS_FILE, "w") as file:
+                file.write(remapping)
 
-        description = f"remappings.txt with bad format"
-        suite.expect_failure(description=description, expected="Invalid remapping in remappings.txt")
-        Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
+            description = f"remappings.txt with bad format"
+            suite.expect_failure(description=description, expected="Invalid remapping in remappings.txt")
+        finally:
+            Path(Util.REMAPPINGS_FILE).unlink(missing_ok=True)
 
     def test_solc_args(self) -> None:
 

Public/TestEVM/CVLCompilation/Preserved/C.spec

@@ -31,7 +31,6 @@ invariant DInitializedBeforeC()
     currentContract.timestamp > 0 => d.initialized_at() > 0
     {
         preserved constructor() {
-            // TODO(CERT-9671) This is a SANITY_FAIL for now because D's storage is zeroed. It will become a success.
             require d.initialized_at() != 0, "assume D was initialized already when calling Cs constructor";
         }
         preserved foo(uint i) with (env e) {

Public/TestEVM/CVLCompilation/Preserved/expectedDefault.json

@@ -7,6 +7,6 @@
     },
 		"holdsWithParamRestrictions": "FAIL",
 		"holdsWithEnvRestrictions": "SUCCESS",
-		"DInitializedBeforeC": "SANITY_FAIL"
+		"DInitializedBeforeC": "SUCCESS"
 	}
 }

Public/TestEVM/Fallback/FallbackAndReceive.sol

@@ -48,6 +48,13 @@ contract C is FallbackAndReceive {
 
 contract Caller {
     FallbackAndReceive a;
+    constructor(FallbackAndReceive _a) {
+        a = _a;
+        require(a.n() == 0 &&
+        a.last_called_fallback() == false &&
+        a.last_called_receive() == false &&
+        a.last_called_nameclash() == false);
+    }
     function noSuchFun() external {}
     function should_call_fallback() external {
         address(a).call(abi.encodeWithSignature("noSuchFun()"));

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

@@ -137,3 +137,9 @@ fun <U, T: U, R> Either<T, R>.leftOrElse(default: (R) -> U): U = when (this) {
    is Either.Left -> this.d
    is Either.Right -> default(this.d)
 }
+
+/* special case for when both "sides" are the same type */
+fun <T> Either<T, T>.leftOrRight() = when (this) {
+    is Either.Left -> this.d
+    is Either.Right -> this.d
+}

lib/Shared/src/main/kotlin/com/certora/certoraprover/cvl/formatter/Comments.kt

@@ -20,11 +20,8 @@ package com.certora.certoraprover.cvl.formatter
 import com.certora.certoraprover.cvl.formatter.util.TerminalId
 import com.certora.certoraprover.cvl.formatter.util.ensure
 import com.certora.certoraprover.cvl.formatter.util.foundOrNull
-import com.certora.certoraprover.cvl.formatter.util.invariantBroken
 import com.certora.certoraprover.cvl.sym
-import datastructures.NonEmptyList
 import datastructures.stdcollections.*
-import datastructures.toNonEmptyList
 import utils.Range
 import utils.SourcePosition
 
@@ -47,8 +44,8 @@ internal data class Comments(
     }
 
     fun bindToToken(prevEmitted: Entry.Emitted?, nextEmitted: Entry.Emitted): Binding {
-        fun beforeNext() = Binding(Association.Before, nextEmitted, this)
-        fun afterPrev() = Binding(Association.After, prevEmitted!!, this)
+        fun beforeNext() = Binding(Association.Before, prev = prevEmitted, next = nextEmitted, this)
+        fun afterPrev() = Binding(Association.After,   prev = prevEmitted, next = nextEmitted, this)
 
         return when {
             prevEmitted == null -> beforeNext()
@@ -104,37 +101,89 @@ internal fun Comments(buffer: List<Entry.NotEmitted>): Comments {
 
 internal enum class Association { Before, After }
 
-internal data class Binding(val association: Association, val token: Entry.Emitted, val comments: Comments)
-
-private class CommentRunBuffer(private val buffer: MutableList<Entry.NotEmitted>, var inProgress: Boolean) {
-    fun add(entry: Entry.NotEmitted) {
-        this.buffer.add(entry)
-    }
+internal data class Binding(
+    val association: Association,
+    val prev: Entry.Emitted?,
+    val next: Entry.Emitted?,
+    val comments: Comments,
+) {
+    // technically, this makes storing the association redundant (can just do object comparison.)
+    val boundToken: Entry.Emitted = when (this.association) {
+        Association.Before -> this.next
+        Association.After -> this.prev
+    }.let(::requireNotNull)
+
+    fun expand(): List<Token> {
+        val comments = this@Binding.comments
+
+        val content = comments
+            .concatenate()
+            .flatMap {
+                when (it) {
+                    is Entry.NotEmitted.Comment -> Token.Terminal(str = it.content, id = null, space = Space.TT).asList()
+                    is Entry.NotEmitted.LineBreaks -> {
+                        List(it.count) { Token.LineBreak.Hard }
+                    }
+                    is Entry.NotEmitted.Whitespace -> {
+                        // we discard the user's whitespace and just use the current indent.
+                        // actually, I have no idea if this is going to work.
+                        emptyList()
+                    }
+                }
+            }
 
-    fun takeBuffer(): NonEmptyList<Entry.NotEmitted>? {
-        val buffer = if (this.inProgress) {
-            this.buffer.toNonEmptyList() ?: invariantBroken("we added a comment when we transitioned to in-progress")
+        val before = if (this.prev == null || comments.before.isEmpty()) {
+            emptyList()
         } else {
-            null
+            when (lineDifference(prev.range, comments.range)) {
+                0 -> Token.SingleWhiteSpace.asList()
+                1 -> Token.LineBreak.Soft.asList()
+                else -> listOf(Token.LineBreak.Soft, Token.LineBreak.Hard)
+            }
         }
 
-        this.buffer.clear()
-        this.inProgress = false
+        val after = if (this.next == null || comments.after.isEmpty()) {
+            emptyList()
+        } else {
+            when (lineDifference(comments.range, next.range)) {
+                0 -> Token.SingleWhiteSpace.asList()
+                1 -> Token.LineBreak.Soft.asList()
+                else -> listOf(Token.LineBreak.Soft, Token.LineBreak.Hard)
+            }
+        }
 
-        return buffer
+        return flatListOf(before, content, after)
     }
 }
 
 internal class CommentsBuilder {
-    private val currentRun: CommentRunBuffer = CommentRunBuffer(mutableListOf(), inProgress = false)
-
     private var prevEmitted: Entry.Emitted? = null
     private val bindings: MutableList<Binding> = mutableListOf()
 
+    private val buffer: MutableList<Entry.NotEmitted> = mutableListOf()
+    private var bufferValid: Boolean = false
+
+    fun takeBuffer(): List<Entry.NotEmitted>? {
+        val buffer = if (this.bufferValid) {
+            val bufferClone = this.buffer.toMutableList()
+
+            ensure(!bufferClone.isEmpty(), "we added a comment when we transitioned to in-progress")
+            this.bufferValid = false
+
+            bufferClone
+        } else {
+            null
+        }
+
+        this.buffer.clear()
+
+        return buffer
+    }
+
     fun register(entry: Entry) {
         when (entry) {
             is Entry.Emitted -> {
-                val buffer: List<Entry.NotEmitted>? = this.currentRun.takeBuffer()
+                val buffer = this.takeBuffer()
 
                 if (buffer != null) {
                     val binding = Comments(buffer).bindToToken(this.prevEmitted, nextEmitted = entry)
@@ -145,16 +194,20 @@ internal class CommentsBuilder {
             }
 
             is Entry.NotEmitted.Comment -> {
-                this.currentRun.inProgress = true
-                this.currentRun.add(entry)
+                this.bufferValid = true
+                buffer.add(entry)
+            }
+            is Entry.NotEmitted.LineBreaks -> {
+                buffer.add(entry)
+            }
+            is Entry.NotEmitted.Whitespace -> {
+                buffer.add(entry)
             }
-            is Entry.NotEmitted.LineBreaks -> this.currentRun.add(entry)
-            is Entry.NotEmitted.Whitespace -> this.currentRun.add(entry)
         }
     }
 
     fun build(lastTokenOfFile: Entry.Emitted?): List<Binding> {
-        val buffer = this.currentRun.takeBuffer()
+        val buffer = this.takeBuffer()
         if (buffer != null) {
             val token = if (lastTokenOfFile != null) {
                 lastTokenOfFile
@@ -169,7 +222,7 @@ internal class CommentsBuilder {
                 zeroSizedEntry(fileName)
             }
 
-            val trailingComments = Binding(Association.After, token, Comments(buffer))
+            val trailingComments = Binding(Association.After, prev = token, next = null, Comments(buffer))
             this.bindings.add(trailingComments)
         }