Implement Solidity's memory layout

src/Act/Coq.hs

@@ -167,7 +167,7 @@ baseRef :: Ref Storage -> StorageUpdate -> Bool
 baseRef baseref (Update _ (Item _ _ r) _) = hasBase r
   where
     hasBase (SVar _ _ _) = False
-    hasBase (SMapping _ r' _) = r' == baseref || hasBase r'
+    hasBase (SMapping _ r' _ _) = r' == baseref || hasBase r'
     hasBase (SField _ r' _ _) = r' == baseref || hasBase r'
 
 
@@ -357,7 +357,7 @@ entry (Item _ _ r) _ = ref r
 ref :: Ref k -> T.Text
 ref (SVar _ _ name) = parens $ T.pack name <> " " <> stateVar
 ref (CVar _ _ name) = T.pack name
-ref (SMapping _ r ixs) = parens $ ref r <> " " <> coqargs ixs
+ref (SMapping _ r _ ixs) = parens $ ref r <> " " <> coqargs ixs
 ref (SField _ r cid name) = parens $ T.pack cid <> "." <> T.pack name <> " " <> ref r
 
 -- | coq syntax for a list of arguments

src/Act/HEVM_utils.hs

@@ -67,12 +67,12 @@ makeCalldata iface@(Interface _ decls) =
     mkArg (Decl typ x) = symAbiArg (T.pack x) typ
     makeSig = T.pack $ makeIface iface
     calldatas = fmap mkArg decls
-    (cdBuf, _) = combineFragments calldatas (EVM.ConcreteBuf "")
+    (cdBuf, props) = combineFragments calldatas (EVM.ConcreteBuf "")
     withSelector = writeSelector cdBuf makeSig
     sizeConstraints
       = (bufLength withSelector EVM..>= cdLen calldatas)
         EVM..&& (bufLength withSelector EVM..< (EVM.Lit (2 ^ (64 :: Integer))))
-  in (withSelector, [sizeConstraints])
+  in (withSelector, sizeConstraints:props)
 
 makeCtrCalldata :: Interface -> Calldata
 makeCtrCalldata (Interface _ decls) =

src/Act/Parse.y

@@ -229,15 +229,15 @@ Decl : AbiType id                                     { Decl $1 (name $2) }
 StorageVar : SlotType id                              { StorageVar (posn $2) $1 (name $2) }
 
 AbiType : 'uint'
-         { case validsize $1 of
+        { case validsize $1 of
 	     True  -> AbiUIntType $1
 	     False -> error $ "invalid uint size: uint" <> (show $1)
-	 }
-       | 'int'
-         { case validsize $1 of
-	     True  -> AbiIntType $1
-	     False -> error $ "invalid int size: int" <> (show $1)
-	 }
+	    }
+        | 'int'
+        { case validsize $1 of
+	        True  -> AbiIntType $1
+	        False -> error $ "invalid int size: int" <> (show $1)
+	    }
        | 'bytes'                                      { AbiBytesType $1 }
        | AbiType '[' ilit ']'                         { AbiArrayType (fromIntegral $ value $3) $1 }
        | 'address'                                    { AbiAddressType }

src/Act/Print.hs

@@ -156,7 +156,7 @@ prettyRef :: Ref k t -> String
 prettyRef = \case
   CVar _ _ n -> n
   SVar _ _ n -> n
-  SMapping _ r args -> prettyRef r <> concatMap (brackets . prettyTypedExp) args
+  SMapping _ r _ args -> prettyRef r <> concatMap (brackets . prettyTypedExp) args
   SField _ r _ n -> prettyRef r <> "." <> n
   where
     brackets str = "[" <> str <> "]"
@@ -199,7 +199,7 @@ prettyInvPred = prettyExp . untime . fst
     untimeRef:: Ref k t -> Ref k Untimed
     untimeRef (SVar p c a) = SVar p c a
     untimeRef (CVar p c a) = CVar p c a
-    untimeRef (SMapping p e xs) = SMapping p (untimeRef e) (fmap untimeTyped xs)
+    untimeRef (SMapping p e ts xs) = SMapping p (untimeRef e) ts (fmap untimeTyped xs)
     untimeRef (SField p e c x) = SField p (untimeRef e) c x
 
     untime :: Exp a t -> Exp a Untimed

src/Act/SMT.hs

@@ -552,7 +552,7 @@ declareStorage :: [When] -> StorageLocation -> [SMT2]
 declareStorage times (Loc _ item@(Item _ _ ref)) = declareRef ref
   where
     declareRef (SVar _ _ _) = (\t -> constant (nameFromSItem t item) (itemType item) ) <$> times
-    declareRef (SMapping _ _ ixs) = (\t -> array (nameFromSItem t item) ixs (itemType item)) <$> times
+    declareRef (SMapping _ _ _ ixs) = (\t -> array (nameFromSItem t item) ixs (itemType item)) <$> times
     declareRef (SField _ ref' _ _) = declareRef ref'
 
 
@@ -693,7 +693,7 @@ nameFromSItem whn (Item _ _ ref) = nameFromSRef ref @@ show whn
 
 nameFromSRef :: Ref Storage -> Id
 nameFromSRef (SVar _ c name) = c @@ name
-nameFromSRef (SMapping _ e _) = nameFromSRef e
+nameFromSRef (SMapping _ e _ _) = nameFromSRef e
 nameFromSRef (SField _ ref c x) = nameFromSRef ref @@ c @@ x
 
 nameFromItem :: When -> TItem k a -> Ctx Id
@@ -706,7 +706,7 @@ nameFromItem whn (Item _ _ ref) = do
 nameFromRef :: Ref k -> Ctx Id
 nameFromRef (CVar _ _ name) = nameFromVarId name
 nameFromRef (SVar _ c name) = pure $ c @@ name
-nameFromRef (SMapping _ e _) = nameFromRef e
+nameFromRef (SMapping _ e _ _) = nameFromRef e
 nameFromRef (SField _ ref c x) = do 
   name <- nameFromRef ref
   pure $ name @@ c @@ x

src/Act/Syntax.hs

@@ -272,7 +272,7 @@ idFromItem (Item _ _ ref) = idFromRef ref
 idFromRef :: Ref k t -> Id
 idFromRef (SVar _ _ x) = x
 idFromRef (CVar _ _ x) = x
-idFromRef (SMapping _ e _) = idFromRef e
+idFromRef (SMapping _ e _ _) = idFromRef e
 idFromRef (SField _ e _ _) = idFromRef e
 
 idFromUpdate :: StorageUpdate t -> Id
@@ -287,7 +287,7 @@ ixsFromItem (Item _ _ item) = ixsFromRef item
 ixsFromRef :: Ref k t -> [TypedExp t]
 ixsFromRef (SVar _ _ _) = []
 ixsFromRef (CVar _ _ _) = []
-ixsFromRef (SMapping _ ref ixs) = ixs ++ ixsFromRef ref
+ixsFromRef (SMapping _ ref _ ixs) = ixs ++ ixsFromRef ref
 ixsFromRef (SField _ ref _ _) = ixsFromRef ref
 
 ixsFromLocation :: StorageLocation t -> [TypedExp t]

src/Act/Syntax/TimeAgnostic.hs

@@ -181,16 +181,16 @@ eqKind fa fb = maybe False (\Refl -> fa == fb) $ testEquality (sing @a) (sing @b
 data Ref (k :: RefKind) (t :: Timing) where
   CVar :: Pn -> AbiType -> Id -> Ref Calldata t     -- Calldata variable
   SVar :: Pn -> Id -> Id -> Ref Storage t           -- Storage variable. First Id is the contract the var belogs to
-  SMapping :: Pn -> Ref k t -> [TypedExp t] -> Ref k t
+  SMapping :: Pn -> Ref k t -> ValueType -> [TypedExp t] -> Ref k t
   SField :: Pn -> Ref k t -> Id -> Id -> Ref k t    -- first Id is the contract the field belogs to
 deriving instance Show (Ref k t)
 
 instance Eq (Ref k t) where
-  CVar _ at x      == CVar _ at' x'      = at == at' && x == x'
-  SVar _ c x       == SVar _ c' x'       = c == c' && x == x'
-  SMapping _ r ixs == SMapping _ r' ixs' = r == r' && ixs == ixs'
-  SField _ r c x   == SField _ r' c' x'  = r == r' && c == c' && x == x'
-  _                == _                  = False
+  CVar _ at x         == CVar _ at' x'          = at == at' && x == x'
+  SVar _ c x          == SVar _ c' x'           = c == c' && x == x'
+  SMapping _ r ts ixs == SMapping _ r' ts' ixs' = r == r' && ts == ts' && ixs == ixs'
+  SField _ r c x      == SField _ r' c' x'      = r == r' && c == c' && x == x'
+  _                   == _                      = False
 
 -- | Item is a reference together with its Act type. The type is
 -- parametrized on a timing `t`, a type `a`, and the reference kind
@@ -373,7 +373,7 @@ instance Timable (TItem a k) where
    setTime time (Item t vt ref) = Item t vt $ setTime time ref
 
 instance Timable (Ref k) where
-  setTime time (SMapping p e ixs) = SMapping p (setTime time e) (setTime time <$> ixs)
+  setTime time (SMapping p e ts ixs) = SMapping p (setTime time e) ts (setTime time <$> ixs)
   setTime time (SField p e c x) = SField p (setTime time e) c x
   setTime _ (SVar p c x) = SVar p c x
   setTime _ (CVar p c x) = CVar p c x
@@ -483,9 +483,9 @@ instance ToJSON (Ref k t) where
                                , "svar" .=  pack x
                                , "contract" .= pack c ]
   toJSON (CVar _ at x) = object [ "kind" .= pack "Var"
-                                  , "var" .=  pack x
-                                  , "abitype" .=  toJSON at ]                                  
-  toJSON (SMapping _ e xs) = mapping e xs
+                                , "var" .=  pack x
+                                , "abitype" .=  toJSON at ]                                  
+  toJSON (SMapping _ e _ xs) = mapping e xs
   toJSON (SField _ e c x) = field e c x
 
 

src/Act/Traversals.hs

@@ -155,10 +155,10 @@ mapRefM :: Monad m => (forall a . Exp a t -> m (Exp a t)) -> Ref k t -> m (Ref k
 mapRefM f = \case
   SVar p a b -> pure (SVar p a b)
   CVar p a b -> pure (CVar p a b)
-  SMapping p a b -> do
+  SMapping p a ts b -> do
     a' <- mapRefM f a
     b' <- mapM (mapTypedExpM f) b
-    pure $ SMapping p a' b'
+    pure $ SMapping p a' ts b'
   SField p r a b -> do
     r' <- mapRefM f r
     pure $ SField p r' a b

src/Act/Type.hs

@@ -339,7 +339,7 @@ checkAssign _ _ = error "todo: support struct assignment in constructors"
 checkDefn :: Pn -> Env -> ValueType -> ValueType -> Id -> U.Defn -> Err StorageUpdate
 checkDefn pn env@Env{contract} keyType vt@(FromVType valType) name (U.Defn k val) =
   _Update
-  <$> (_Item vt . SMapping nowhere (SVar pn contract name) <$> checkIxs env (getPosn k) [k] [keyType])
+  <$> (_Item vt . SMapping nowhere (SVar pn contract name) vt <$> checkIxs env (getPosn k) [k] [keyType])
   <*> checkExpr env valType val
 
 -- | Typechecks a postcondition, returning typed versions of its storage updates and return expression.
@@ -371,7 +371,8 @@ checkEntry Env{contract,store,calldata, pointers} kind (U.EVar p name) = case (k
 checkEntry env kind (U.EMapping p e args) =
   checkEntry env kind e `bindValidation` \(typ, _, ref) -> case typ of
     StorageValue _ -> throw (p, "Expression should have a mapping type" <> show e)
-    StorageMapping argtyps restyp -> (StorageValue restyp, Nothing,) . SMapping p ref <$> checkIxs env p args (NonEmpty.toList argtyps)
+    StorageMapping argtyps restyp -> 
+        (StorageValue restyp, Nothing,) . SMapping p ref restyp <$> checkIxs env p args (NonEmpty.toList argtyps)
 checkEntry env@Env{theirs} kind (U.EField p e x) =
   checkEntry env kind e `bindValidation` \(_, oc, ref) -> case oc of
     Just c -> case Map.lookup c theirs of

tests/hevm/pass/layout1/layout1.act

@@ -0,0 +1,25 @@
+constructor of A
+interface constructor()
+
+iff
+
+  CALLVALUE == 0
+
+creates
+
+  uint128 x := 11
+  uint128 y := 42
+
+behaviour swap of A
+interface swap()
+
+iff
+
+  CALLVALUE == 0
+
+  storage
+
+    x => y
+    y => x
+
+  returns 1

tests/hevm/pass/layout1/layout1.sol

@@ -0,0 +1,19 @@
+contract A {
+    uint128 x;
+    uint128 y;
+
+    constructor() {
+        x = 11;
+        y = 42;
+    }
+
+    function swap() external returns (uint) {
+
+        uint128 tmp = x;
+
+        x = y;
+        y = tmp;
+
+        return 1;
+    }
+}

tests/hevm/pass/layout2/layout2.act

@@ -0,0 +1,73 @@
+constructor of A
+interface constructor()
+
+iff
+
+  CALLVALUE == 0
+
+creates
+
+  uint128 x := 11
+  bool flag := true
+  uint32 u := 17
+  uint8 z := 3
+  uint128 y := 42
+  uint256 i := 128
+
+behaviour foo of A
+interface foo()
+
+iff
+
+  CALLVALUE == 0
+
+storage
+
+  x => y
+  y => x
+  z => 11
+  flag => not flag
+
+returns 1
+
+behaviour set_flag of A
+interface set_flag(bool b)
+
+iff
+
+  CALLVALUE == 0
+
+storage
+
+  flag => b
+
+
+behaviour get_flag of A
+interface get_flag()
+
+iff
+
+  CALLVALUE == 0
+
+returns
+
+  pre(flag)
+
+
+behaviour set_y_if_flag of A
+interface set_y_if_flag(uint128 v)
+
+iff
+
+  CALLVALUE == 0
+
+case flag:
+
+storage
+  y => v
+
+returns 1
+
+case (not flag):
+returns 1
+

tests/hevm/pass/layout2/layout2.sol

@@ -0,0 +1,45 @@
+contract A {
+    uint128 x;
+    bool flag;
+    uint32 u;
+    uint8 z;
+    uint128 y;
+    uint256 i;
+
+    constructor() {
+        x = 11;
+        flag = true;
+        u = 17;
+        z = 3;
+        y = 42;
+        i = 128;
+    }
+
+    function foo() external returns (uint) {
+
+        uint128 tmp = x;
+
+        x = y;
+        y = tmp;
+        z = 11;
+        flag = !flag;
+
+        return 1;
+    }
+
+    function set_flag(bool b) external {
+        flag = b;
+    }
+
+    function get_flag() external returns (bool) {
+        return flag;
+    }
+
+    function set_y_if_flag(uint128 v) external returns (uint) {
+        if (flag) {
+            y = v;
+        }
+
+        return 1;
+    }
+}