Open d-xo opened 8 months ago
This seems to go into a loop on dc0000163fabe2f128f018ff87ba3f93aefce3d5
during interpretation. Something is a bit weird. Maybe to do with the dual array.
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"
The following test gives a counterexample that does not seem to reproduce in foundry:
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...