Spurious Counterexample With Nested Arrays

[d-xo]

The following test gives a counterexample that does not seem to reproduce in foundry:

    function prove_nested_append(uint v, uint w) public {
        arr2.push([v,w]);
        arr2.push();
        arr2.push();

        arr2[1].push(arr2[0][0]);

        arr2[2].push(w);
        // TODO: this is the problematic line!
        // changing this to arr2[1].push(1), and updating the assertion for the
        // value of arr2[1][1] to reflect the change makes this test pass...
        arr2[1].push(w);

        assert(arr2.length == 3);

        assert(arr2[0].length == 2);
        assert(arr2[0][0] == v);
        assert(arr2[0][1] == w);

        assert(arr2[1].length == 2);
        assert(arr2[1][0] == v);
        assert(arr2[1][1] == w);

        assert(arr2[2].length == 1);
        assert(arr2[2][0] == w);
    }

This gives me a cex of prove_nested_append(0,2);, but when I try to run that in foundry as a concrete test, I don't trigger any assertions...

[msooseth]

This seems to go into a loop on dc0000163fabe2f128f018ff87ba3f93aefce3d5 during interpretation. Something is a bit weird. Maybe to do with the dual array.

[msooseth]

Diff to add to check:

diff --git a/test/test.hs b/test/test.hs
index f7102e7d..da46d476 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -304,6 +304,42 @@ tests = testGroup "hevm"
       let simpExpr = mapExprM Expr.decomposeStorage expr
       -- putStrLnM $ T.unpack $ formatExpr (fromJust simpExpr)
       assertEqualM "Decompose did not succeed." (isJust simpExpr) True
+    , test "decompose-bug" $ do
+      Just c <- solcRuntime "MyContract"
+        [i|
+        contract MyContract {
+          uint[][] arr2;
+          function prove_nested_append(uint v, uint w) public {
+            arr2.push([v,w]);
+            arr2.push();
+            arr2.push();
+
+            arr2[1].push(arr2[0][0]);
+
+            arr2[2].push(w);
+            // TODO: this is the problematic line!
+            // changing this to arr2[1].push(1), and updating the assertion for the
+            // value of arr2[1][1] to reflect the change makes this test pass...
+            arr2[1].push(w);
+
+            assert(arr2.length == 3);
+
+            assert(arr2[0].length == 2);
+            assert(arr2[0][0] == v);
+            assert(arr2[0][1] == w);
+
+            assert(arr2[1].length == 2);
+            assert(arr2[1][0] == v);
+            assert(arr2[1][1] == w);
+
+            assert(arr2[2].length == 1);
+            assert(arr2[2][0] == w);
+          }
+        }
+        |]
+      let fun = (Just (Sig "prove_nested_append(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256]))
+      (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c fun [] defaultVeriOpts
+      putStrLnM "All good."
     -- TODO check what's going on here. Likely the "arbitrary write through array" is the reason why we fail
     , expectFail $ test "decompose-6-fail" $ do
       Just c <- solcRuntime "MyContract"

[msooseth]

So this is super-annoying. When I make it into a .sol file, compile with forge build --ast, and run it as hevm test ... it actually passes, which is great. But when I put it into test.hs, it has trouble exploring it. I am suspecting we are calling solc slightly differently... Anyway, at least it works with forge , which is what the users experience. I will try to debug today.

[msooseth]

Same exect behaviour with

    , test "decompose-bug" $ do
      Just c <- solcRuntime "MyContract"
        [i|
        contract MyContract {
          uint[][] arr2;
          function prove_nested_append(uint v, uint w) public {
            arr2.push([1,2]);
          }
        }
        |]
      let fun = (Just (Sig "prove_nested_append(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256]))
      (_, [Qed _]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s defaultPanicCodes c fun [] defaultVeriOpts
      putStrLnM "All good."

Again in a sol & forge build --ast together with hevm test it works perfectly fine.