fix bug in translation

ethereum · Jan 17, 2025 · b79ad8d · b79ad8d
1 parent e3b2209
commit b79ad8d
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs
@@ -253,7 +253,7 @@ applyUpdate readMap writeMap (Update typ (Item _ _ ref) e) = do
         fresh <- getFreshIncr
         let freshAddr = EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show fresh)
         writeMap' <- localCaddr freshAddr $ createContract readMap writeMap freshAddr e
-        pure $ M.insert caddr' (updateNonce (updateStorage (EVM.SStore addr (EVM.WAddr freshAddr))contract), cid) writeMap'
+        pure $ M.insert caddr' (updateNonce (updateStorage (EVM.SStore addr (EVM.WAddr freshAddr)) contract), cid) writeMap'
       _ -> do
         e' <- toExpr readMap e
 
@@ -614,7 +614,7 @@ refToExp cmap r = do
   (slot, offset, size) <- refOffset cmap r
   let word = accessStorage cmap slot caddr
   let mask = (2 ^ (8 * size) - 1) `shiftL` (offset * 8)
-  pure $ EVM.Div (EVM.And word (EVM.Lit mask)) (EVM.Lit (2 ^(8 * size)))
+  pure $ EVM.Div (EVM.And word (EVM.Lit mask)) (EVM.Lit (2 ^ (8 * offset)))
 
 accessStorage :: ContractMap -> EVM.Expr EVM.EWord -> EVM.Expr EVM.EAddr -> EVM.Expr EVM.EWord
 accessStorage cmap slot addr = case M.lookup addr cmap of

diff --git a/tests/hevm/pass/layout1/layout1.act b/tests/hevm/pass/layout1/layout1.act
@@ -7,8 +7,8 @@ iff
 
 creates
 
-  uint128 x := 0
-  uint128 y := 0
+  uint128 x := 11
+  uint128 y := 42
 
 behaviour swap of A
 interface swap()
@@ -20,5 +20,6 @@ iff
   storage
 
     x => y
+    y => x
 
   returns 1
diff --git a/tests/hevm/pass/layout1/layout1.sol b/tests/hevm/pass/layout1/layout1.sol
@@ -3,14 +3,16 @@ contract A {
     uint128 y;
 
     constructor() {
-        x = 0;
-        y = 0;
+        x = 11;
+        y = 42;
     }
 
     function swap() external returns (uint) {
 
+        uint128 tmp = x;
+
         x = y;
-        // y = x;
+        y = tmp;
 
         return 1;
     }