AST: move timing to storage variables only

Author: zoep

src/Act/Coq.hs

@@ -147,7 +147,7 @@ retVal _ = return ""
 -- 'handler' defines what to do in cases where a given name isn't updated
 stateval :: Store -> Id -> (Ref Storage -> SlotType -> T.Text) -> [StorageUpdate] -> T.Text
 stateval store contract handler updates = T.unwords $
-  stateConstructor : fmap (\(n, (t, _)) -> updateVar store updates handler (SVar nowhere contract n) t) (M.toList store')
+  stateConstructor : fmap (\(n, (t, _)) -> updateVar store updates handler (SVar nowhere contract n Pre) t) (M.toList store')
   where
     store' = contractStore contract store
 
@@ -166,7 +166,7 @@ eqRef r (Update _ (Item _ _ r') _) = r == r'
 baseRef :: Ref Storage -> StorageUpdate -> Bool
 baseRef baseref (Update _ (Item _ _ r) _) = hasBase r
   where
-    hasBase (SVar _ _ _) = False
+    hasBase (SVar _ _ _ _) = False
     hasBase (SMapping _ r' _) = r' == baseref || hasBase r'
     hasBase (SField _ r' _ _) = r' == baseref || hasBase r'
 
@@ -306,7 +306,7 @@ coqexp (UIntMax _ n) = parens $ "UINT_MAX " <> T.pack (show n)
 coqexp (InRange _ t e) = coqexp (bound t e)
 
 -- polymorphic
-coqexp (TEntry _ w _ e) = entry e w
+coqexp (TEntry _ _ e) = entry e
 coqexp (ITE _ b e1 e2) = parens $ "if "
                                <> coqexp b
                                <> " then "
@@ -349,13 +349,13 @@ coqprop e = error "ill formed proposition: " <> T.pack (show e)
 typedexp :: TypedExp -> T.Text
 typedexp (TExp _ e) = coqexp e
 
-entry :: TItem k a -> When -> T.Text
-entry (Item SByteStr _ _) _ = error "bytestrings not supported"
-entry e Post = error $ "TODO: missing support for poststate references in coq backend. Entry: \n" <> show e
-entry (Item _ _ r) _ = ref r
+entry :: TItem k a -> T.Text
+entry (Item SByteStr _ _) = error "bytestrings not supported"
+entry (Item _ _ r) = ref r
 
 ref :: Ref k -> T.Text
-ref (SVar _ _ name) = parens $ T.pack name <> " " <> stateVar
+ref (SVar _ _ name Post) = error $ "TODO: missing support for poststate references in coq backend. Entry: \n" <> name
+ref (SVar _ _ name _) = parens $ T.pack name <> " " <> stateVar
 ref (CVar _ _ name) = T.pack name
 ref (SMapping _ r ixs) = parens $ ref r <> " " <> coqargs ixs
 ref (SField _ r cid name) = parens $ T.pack cid <> "." <> T.pack name <> " " <> ref r

src/Act/Decompile.hs

@@ -277,7 +277,7 @@ mkRewrites cname (DistinctStore writes) = forM (Map.toList writes) $ \(name,(val
           AbiTupleType _ -> Left "cannot decompile methods that write to tuple in storage"
           AbiFunctionType -> Left "cannot decompile methods that store function pointers"
           _ -> do
-            pure (Update SInteger (Item SInteger v (SVar nowhere (T.unpack cname) (T.unpack name))) val)
+            pure (Update SInteger (Item SInteger v (SVar nowhere (T.unpack cname) (T.unpack name) Post)) val)
         Dynamic -> Left "cannot decompile methods that store dynamically sized types"
       ContractType {} -> Left "cannot decompile contracts that have contract types in storage"
     StorageMapping {} -> Left "cannot decompile contracts that write to mappings"
@@ -378,7 +378,7 @@ fromWord layout w = simplify <$> go w
     go :: EVM.Expr EVM.EWord -> Either Text (Exp AInteger)
     go (EVM.Lit a) = Right $ LitInt nowhere (toInteger a)
     -- TODO: get the actual abi type from the compiler output
-    go (EVM.Var a) = Right $ _Var Pre (AbiBytesType 32) (T.unpack a)
+    go (EVM.Var a) = Right $ _Var (AbiBytesType 32) (T.unpack a)
     go (EVM.TxValue) = Right $ IntEnv nowhere Callvalue
 
     -- overflow checks
@@ -438,7 +438,7 @@ fromWord layout w = simplify <$> go w
            Nothing -> Left "read from a storage location that is not present in the solc layout"
            Just (nm, tp) -> case tp of
              -- TODO: get lookup contract name by address
-             StorageValue t@(PrimitiveType _) -> Right $ TEntry nowhere Pre SStorage (Item SInteger t (SVar nowhere (T.unpack "Basic") (T.unpack nm)))
+             StorageValue t@(PrimitiveType _) -> Right $ TEntry nowhere SStorage (Item SInteger t (SVar nowhere (T.unpack "Basic") (T.unpack nm) Pre))
              _ -> Left $ "unable to handle storage reads for variables of type: " <> T.pack (show tp)
 
     go e = err e

src/Act/Enrich.hs

@@ -83,7 +83,7 @@ mkStorageBounds refs = concatMap mkBound refs
 
 -- TODO why only Pre items here?
 fromItem :: TItem AInteger Storage -> Exp ABoolean
-fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre SStorage item)
+fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere SStorage item)
 fromItem (Item _ (ContractType _) _) = LitBool nowhere True
 
 mkStorageBoundsLoc :: [StorageLocation] -> [Exp ABoolean]
@@ -95,5 +95,5 @@ mkStorageBoundsLoc refs = concatMap mkBound refs
 
 mkCallDataBounds :: [Decl] -> [Exp ABoolean]
 mkCallDataBounds = concatMap $ \(Decl typ name) -> case fromAbiType typ of
-  AInteger -> [bound typ (_Var Pre typ name)]
+  AInteger -> [bound typ (_Var typ name)]
   _ -> []

src/Act/HEVM.hs

@@ -274,9 +274,9 @@ substItem subst (Item st vt sref) = case substRef subst sref of
   ERef k ref -> ETItem k (Item st vt ref)
 
 substRef :: M.Map Id TypedExp -> Ref k -> ERef
-substRef _ var@(SVar _ _ _) = ERef SStorage var
+substRef _ var@(SVar _ _ _ _) = ERef SStorage var
 substRef subst (CVar _ _ x) = case M.lookup x subst of
-    Just (TExp _ (TEntry _ _ k (Item _ _ ref))) -> ERef k ref
+    Just (TExp _ (TEntry _ k (Item _ _ ref))) -> ERef k ref
     Just _ -> error "Internal error: cannot access fields of non-pointer var"
     Nothing -> error "Internal error: ill-formed substitution"
 substRef subst (SMapping pn sref args) = case substRef subst sref of
@@ -328,11 +328,11 @@ substExp subst expr = case expr of
 
   ITE pn a b c -> ITE pn (substExp subst a) (substExp subst b) (substExp subst c)
 
-  TEntry _ _ SCalldata (Item st _ (CVar _ _ x)) -> case M.lookup x subst of
+  TEntry _ SCalldata (Item st _ (CVar _ _ x)) -> case M.lookup x subst of
     Just (TExp st' exp') -> maybe (error "Internal error: type missmatch") (\Refl -> exp') $ testEquality st st'
     Nothing -> error "Internal error: Ill-defined substitution"
-  TEntry pn whn _ item -> case substItem subst item of
-    ETItem k' item' ->  TEntry pn whn k' item'
+  TEntry pn _ item -> case substItem subst item of
+    ETItem k' item' ->  TEntry pn k' item'
 
   Create pn a b -> Create pn a (substArgs subst b)
 
@@ -373,7 +373,7 @@ getSlot layout cid name =
 
 refOffset :: Monad m => ContractMap -> Ref k -> ActT m (EVM.Expr EVM.EWord)
 refOffset _ (CVar _ _ _) = error "Internal error: ill-typed entry"
-refOffset _ (SVar _ cid name) = do
+refOffset _ (SVar _ cid name _) = do
   layout <- getLayout
   let slot = getSlot layout cid name
   pure $ EVM.Lit (fromIntegral slot)
@@ -388,7 +388,7 @@ refOffset _ (SField _ _ cid name) = do
   pure $ EVM.Lit (fromIntegral slot)
 
 baseAddr :: Monad m => ContractMap -> Ref k -> ActT m (EVM.Expr EVM.EAddr)
-baseAddr _ (SVar _ _ _) = getCaddr
+baseAddr _ (SVar _ _ _ _) = getCaddr
 baseAddr _ (CVar _ _ _) = error "Internal error: ill-typed entry"
 baseAddr cmap (SField _ ref _ _) = do
   expr <- refToExp cmap ref 
@@ -445,7 +445,7 @@ toProp cmap = \case
     pure $ EVM.PNeg e
   (NEq _ _ _ _) -> error "unsupported"
   (ITE _ _ _ _) -> error "Internal error: expecting flat expression"
-  (TEntry _ _ _ _) -> error "TODO" -- EVM.SLoad addr idx
+  (TEntry _ _ _) -> error "TODO" -- EVM.SLoad addr idx
   (InRange _ t e) -> toProp cmap (inRange t e)
   where
     op2 :: Monad m => forall a b. (EVM.Expr (ExprType b) -> EVM.Expr (ExprType b) -> a) -> Exp b -> Exp b -> ActT m a
@@ -527,7 +527,7 @@ toExpr cmap =  fmap stripMods . go
         pure $ EVM.Not e
       (NEq _ _ _ _) -> error "unsupported"
 
-      (TEntry _ _ _ (Item SInteger _ ref)) -> refToExp cmap ref
+      (TEntry _ _ (Item SInteger _ ref)) -> refToExp cmap ref
 
       e@(ITE _ _ _ _) -> error $ "Internal error: expecting flat expression. got: " <> show e
 
@@ -572,7 +572,7 @@ inRange t e = bound t e
 
 checkOp :: Exp AInteger -> Exp ABoolean
 checkOp (LitInt _ i) = LitBool nowhere $ i <= (fromIntegral (maxBound :: Word256))
-checkOp (TEntry _ _ _ _)  = LitBool nowhere True
+checkOp (TEntry _ _ _)  = LitBool nowhere True
 checkOp e@(Add _ e1 _) = LEQ nowhere e1 e -- check for addition overflow
 checkOp e@(Sub _ e1 _) = LEQ nowhere e e1
 checkOp (Mul _ e1 e2) = Or nowhere (Eq nowhere SInteger e1 (LitInt nowhere 0))

src/Act/Print.hs

@@ -142,7 +142,7 @@ prettyExp e = case e of
 
   --polymorphic
   ITE _ a b c -> "(if " <> prettyExp a <> " then " <> prettyExp b <> " else " <> prettyExp c <> ")"
-  TEntry _ t _ a -> timeParens t $ prettyItem a
+  TEntry _ _ a ->  prettyItem a
   where
     print2 sym a b = "(" <> prettyExp a <> " " <> sym <> " " <> prettyExp b <> ")"
 
@@ -155,7 +155,7 @@ prettyItem (Item _ _ r) = prettyRef r
 prettyRef :: Ref k t -> String
 prettyRef = \case
   CVar _ _ n -> n
-  SVar _ _ n -> n
+  SVar _ n _ t -> timeParens t n
   SMapping _ r args -> prettyRef r <> concatMap (brackets . prettyTypedExp) args
   SField _ r _ n -> prettyRef r <> "." <> n
   where
@@ -197,7 +197,7 @@ prettyInvPred = prettyExp . untime . fst
     untimeTyped (TExp t e) = TExp t (untime e)
 
     untimeRef:: Ref k t -> Ref k Untimed
-    untimeRef (SVar p c a) = SVar p c a
+    untimeRef (SVar p c a _) = SVar p c a Neither
     untimeRef (CVar p c a) = CVar p c a
     untimeRef (SMapping p e xs) = SMapping p (untimeRef e) (fmap untimeTyped xs)
     untimeRef (SField p e c x) = SField p (untimeRef e) c x
@@ -235,7 +235,7 @@ prettyInvPred = prettyExp . untime . fst
       ByEnv p a   -> ByEnv p a
       ITE p x y z -> ITE p (untime x) (untime y) (untime z)
       Slice p a b c -> Slice p (untime a) (untime b) (untime c)
-      TEntry p _ k (Item t vt a) -> TEntry p Neither k (Item t vt (untimeRef a))
+      TEntry p k (Item t vt a) -> TEntry p k (Item t vt (untimeRef a))
 
 
 -- | Doc type for terminal output

src/Act/SMT.hs

@@ -540,7 +540,7 @@ parseSMTModel s = if length s0Caps == 1
 encodeUpdate :: Id -> StorageUpdate -> SMT2
 encodeUpdate behvName (Update _ item expr) =
   let
-    postentry  = withInterface behvName $ expToSMT2 (TEntry nowhere Post SStorage item)
+    postentry  = withInterface behvName $ expToSMT2 (TEntry nowhere SStorage item)
     expression = withInterface behvName $ expToSMT2 expr
   in "(assert (= " <> postentry <> " " <> expression <> "))"
 
@@ -551,7 +551,7 @@ encodeConstant loc = "(assert (= " <> nameFromLoc Pre loc <> " " <> nameFromLoc
 declareStorage :: [When] -> StorageLocation -> [SMT2]
 declareStorage times (Loc _ item@(Item _ _ ref)) = declareRef ref
   where
-    declareRef (SVar _ _ _) = (\t -> constant (nameFromSItem t item) (itemType item) ) <$> times
+    declareRef (SVar _ _ _ _) = (\t -> constant (nameFromSItem t item) (itemType item) ) <$> times
     declareRef (SMapping _ _ ixs) = (\t -> array (nameFromSItem t item) ixs (itemType item)) <$> times
     declareRef (SField _ ref' _ _) = declareRef ref'
 
@@ -625,7 +625,7 @@ expToSMT2 expr = case expr of
   Eq _ _ a b -> binop "=" a b
   NEq p s a b -> unop "not" (Eq p s a b)
   ITE _ a b c -> triop "ite" a b c
-  TEntry _ w _ item -> entry item w
+  TEntry _ _ item -> entry item
   where
     unop :: String -> Exp a -> Ctx SMT2
     unop op a = ["(" <> op <> " " <> a' <> ")" | a' <- expToSMT2 a]
@@ -638,11 +638,11 @@ expToSMT2 expr = case expr of
     triop op a b c = ["(" <> op <> " " <> a' <> " " <> b' <> " " <> c' <> ")"
                         | a' <- expToSMT2 a, b' <- expToSMT2 b, c' <- expToSMT2 c]
 
-    entry :: TItem k a ->  When -> Ctx SMT2
-    entry item whn = case ixsFromItem item of
-      []       -> nameFromItem whn item
+    entry :: TItem k a -> Ctx SMT2
+    entry item = case ixsFromItem item of
+      []       -> nameFromItem item
       (ix:ixs) -> do
-        name <- nameFromItem whn item
+        name <- nameFromItem item
         select name (ix :| ixs)
 
 -- | SMT2 has no support for exponentiation, but we can do some preprocessing
@@ -689,23 +689,19 @@ sType' (TExp t _) = sType $ actType t
 
 -- Construct the smt2 variable name for a given storage item
 nameFromSItem :: When -> TItem a Storage -> Id
-nameFromSItem whn (Item _ _ ref) = nameFromSRef ref @@ show whn
+nameFromSItem whn (Item _ _ ref) = nameFromSRef whn ref @@ show whn
 
-nameFromSRef :: Ref Storage -> Id
-nameFromSRef (SVar _ c name) = c @@ name
-nameFromSRef (SMapping _ e _) = nameFromSRef e
-nameFromSRef (SField _ ref c x) = nameFromSRef ref @@ c @@ x
+nameFromSRef :: When -> Ref Storage -> Id
+nameFromSRef whn (SVar _ c name _) = c @@ name @@ show whn
+nameFromSRef whn (SMapping _ e _) = nameFromSRef whn e
+nameFromSRef whn (SField _ ref c x) = nameFromSRef whn ref @@ c @@ x
 
-nameFromItem :: When -> TItem k a -> Ctx Id
-nameFromItem whn (Item _ _ ref) = do
-  name <- nameFromRef ref
-  case ref of -- TODO: this feels rather adhoc, but I can't find a better way to handle timings
-    CVar _ _ _ -> pure name
-    _ -> pure $ name @@ show whn
+nameFromItem :: TItem k a -> Ctx Id
+nameFromItem (Item _ _ ref) = nameFromRef ref
 
 nameFromRef :: Ref k -> Ctx Id
 nameFromRef (CVar _ _ name) = nameFromVarId name
-nameFromRef (SVar _ c name) = pure $ c @@ name
+nameFromRef (SVar _ c name whn) = pure $ c @@ name @@ show whn
 nameFromRef (SMapping _ e _) = nameFromRef e
 nameFromRef (SField _ ref c x) = do 
   name <- nameFromRef ref

src/Act/Syntax.hs

@@ -113,7 +113,7 @@ locsFromExp = nub . go
       ByEnv {} -> []
       Create _ _ es -> concatMap locsFromTypedExp es
       ITE _ x y z -> go x <> go y <> go z
-      TEntry _ _ k a -> locsFromItem k a
+      TEntry _ k a -> locsFromItem k a
 
 createsFromExp :: Exp a t -> [Id]
 createsFromExp = nub . go
@@ -151,7 +151,7 @@ createsFromExp = nub . go
       ByEnv {} -> []
       Create _ f es -> [f] <> concatMap createsFromTypedExp es
       ITE _ x y z -> go x <> go y <> go z
-      TEntry _ _ _ a -> createsFromItem a
+      TEntry _ _ a -> createsFromItem a
 
 createsFromItem :: TItem k a t -> [Id]
 createsFromItem item = concatMap createsFromTypedExp (ixsFromItem item)
@@ -264,13 +264,13 @@ ethEnvFromExp = nub . go
       IntEnv _ a -> [a]
       ByEnv _ a -> [a]
       Create _ _ ixs -> concatMap ethEnvFromTypedExp ixs
-      TEntry _ _ _ a -> ethEnvFromItem a
+      TEntry _ _ a -> ethEnvFromItem a
 
 idFromItem :: TItem k a t -> Id
 idFromItem (Item _ _ ref) = idFromRef ref
 
 idFromRef :: Ref k t -> Id
-idFromRef (SVar _ _ x) = x
+idFromRef (SVar _ _ x _) = x
 idFromRef (CVar _ _ x) = x
 idFromRef (SMapping _ e _) = idFromRef e
 idFromRef (SField _ e _ _) = idFromRef e
@@ -285,7 +285,7 @@ ixsFromItem :: TItem k a t -> [TypedExp t]
 ixsFromItem (Item _ _ item) = ixsFromRef item
 
 ixsFromRef :: Ref k t -> [TypedExp t]
-ixsFromRef (SVar _ _ _) = []
+ixsFromRef (SVar _ _ _ _) = []
 ixsFromRef (CVar _ _ _) = []
 ixsFromRef (SMapping _ ref ixs) = ixs ++ ixsFromRef ref
 ixsFromRef (SField _ ref _ _) = ixsFromRef ref
@@ -342,7 +342,7 @@ posnFromExp e = case e of
   Eq  p _ _ _ -> p
   NEq p _ _ _ -> p
   ITE p _ _ _ -> p
-  TEntry p _ _ _ -> p
+  TEntry p _ _ -> p
 --------------------------------------
 -- * Extraction from untyped ASTs * --
 --------------------------------------

src/Act/Syntax/Annotated.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE InstanceSigs #-}
 
 {-|
 Module      : Syntax.Annotated
@@ -63,6 +64,5 @@ instance Annotatable Agnostic.Behaviour where
     }
 
 instance Annotatable Agnostic.StorageUpdate where
-  -- The timing in items only refers to the timing of mapping indices of a
-  -- storage update. Hence, it should be Pre
-  annotate (Update typ item expr) = Update typ (setPre item) (setPre expr)
+  annotate :: Agnostic.StorageUpdate Untimed -> Agnostic.StorageUpdate Timed
+  annotate (Update typ item expr) = Update typ (setPost item) (setPre expr)