Act cleanup (#170)

* syntax: remove constant from untyped AST

* Syntax: remove constant

* tests: regenerate test outputs

* enrich: generate contraints for variables in preconditions and cases

* test: regenerate test outputs

* enrich: fix storage var timings

* enrich: fix in constructor

* smt: wip trying to fix undeclared storage vars

* SMT: declare all mentioned vars

* enrich: only add bounds for pre

* test: remove constant

* test: remove constant

* test: fix compilation error

src/Coq.hs

@@ -77,7 +77,7 @@ reachable constructor behvs = inductive
 
 -- | non-recursive constructor for the reachable relation
 baseCase :: Constructor -> T.Text
-baseCase (Constructor name i@(Interface _ decls) conds _ _ _ _) =
+baseCase (Constructor name i@(Interface _ decls) conds _ _ _ ) =
   T.pack name <> baseSuffix <> " : " <> universal <> "\n" <> constructorBody
   where
     baseval = parens $ T.pack name <> " " <> envVar <> " " <> arguments i
@@ -113,15 +113,15 @@ reachableStep (Behaviour name _ i conds cases _ _ _) =
 
 -- | definition of a base state
 base :: Store -> Constructor -> T.Text
-base store (Constructor name i _ _ _ updates _) =
+base store (Constructor name i _ _ _ updates) =
   definition (T.pack name) (envDecl <> " " <> interface i) $
     stateval store name (\_ t -> defaultSlotValue t) updates
 
 transition :: Store -> Behaviour -> Fresh T.Text
 transition store (Behaviour name cname i _ _ _ rewrites _) = do
   name' <- fresh name
   return $ definition name' (envDecl <> " " <> stateDecl <> " " <> interface i) $
-    stateval store cname (\ref _ -> storageRef ref) (updatesFromRewrites rewrites)
+    stateval store cname (\ref _ -> storageRef ref) rewrites
 
 -- | inductive definition of a return claim
 -- ignores claims that do not specify a return value

src/Enrich.hs

@@ -18,36 +18,36 @@ enrich (Act store contracts) = Act store (enrichContract <$> contracts)
 
 -- |Adds type bounds for calldata , environment vars, and external storage vars as preconditions
 enrichConstructor :: Constructor -> Constructor
-enrichConstructor ctor@(Constructor _ (Interface _ decls) pre _ invs _ storageUpdates) =
+enrichConstructor ctor@(Constructor _ (Interface _ decls) pre _ invs _) =
   ctor { _cpreconditions = pre'
        , _invariants = invs' }
     where
       pre' = pre
              <> mkCallDataBounds decls
-             <> mkStorageBounds storageUpdates
              <> mkEthEnvBounds (ethEnvFromConstructor ctor)
       invs' = enrichInvariant ctor <$> invs
 
 -- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
 enrichBehaviour :: Behaviour -> Behaviour
-enrichBehaviour behv@(Behaviour _ _ (Interface _ decls) pre _ _ stateUpdates _) =
+enrichBehaviour behv@(Behaviour _ _ (Interface _ decls) pre cases _ stateUpdates _) =
   behv { _preconditions = pre' }
     where
       pre' = pre
              <> mkCallDataBounds decls
              <> mkStorageBounds stateUpdates
+             <> mkStorageBoundsLoc (concatMap locsFromExp (pre <> cases))
              <> mkEthEnvBounds (ethEnvFromBehaviour behv)
 
 -- | Adds type bounds for calldata, environment vars, and storage vars
 enrichInvariant :: Constructor -> Invariant -> Invariant
-enrichInvariant (Constructor _ (Interface _ decls) _ _ _ _ _) inv@(Invariant _ preconds storagebounds (predicate,_)) =
+enrichInvariant (Constructor _ (Interface _ decls) _ _ _ _) inv@(Invariant _ preconds storagebounds (predicate,_)) =
   inv { _ipreconditions = preconds', _istoragebounds = storagebounds' }
     where
       preconds' = preconds
                   <> mkCallDataBounds decls
                   <> mkEthEnvBounds (ethEnvFromExp predicate)
       storagebounds' = storagebounds
-                       <> mkStorageBounds (Constant <$> locsFromExp predicate)
+                       <> mkStorageBoundsLoc (locsFromExp predicate)
 
 mkEthEnvBounds :: [EthEnv] -> [Exp ABoolean]
 mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
@@ -74,17 +74,24 @@ mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
       Nonce -> AbiUIntType 256
 
 -- | extracts bounds from the AbiTypes of Integer values in storage
-mkStorageBounds :: [Rewrite] -> [Exp ABoolean]
-mkStorageBounds refs = catMaybes $ mkBound <$> refs
+mkStorageBounds :: [StorageUpdate] -> [Exp ABoolean]
+mkStorageBounds refs = concatMap mkBound refs
   where
-    mkBound :: Rewrite -> Maybe (Exp ABoolean)
-    mkBound (Constant (Loc SInteger item)) = Just $ fromItem item
-    mkBound (Rewrite (Update SInteger item _)) = Just $ fromItem item
-    mkBound _ = Nothing
+    mkBound :: StorageUpdate -> [Exp ABoolean]
+    mkBound (Update SInteger item _) = [fromItem item]
+    mkBound _ = []
 
-    fromItem :: TStorageItem AInteger -> Exp ABoolean
-    fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre item)
-    fromItem (Item _ (ContractType _) _) = LitBool nowhere True
+-- TODO why only Pre items here?
+fromItem :: TStorageItem AInteger -> Exp ABoolean
+fromItem item@(Item _ (PrimitiveType vt) _) = bound vt (TEntry nowhere Pre item)
+fromItem (Item _ (ContractType _) _) = LitBool nowhere True
+
+mkStorageBoundsLoc :: [StorageLocation] -> [Exp ABoolean]
+mkStorageBoundsLoc refs = concatMap mkBound refs
+  where
+    mkBound :: StorageLocation -> [Exp ABoolean]
+    mkBound (Loc SInteger item) = [fromItem item]
+    mkBound _ = []
 
 mkCallDataBounds :: [Decl] -> [Exp ABoolean]
 mkCallDataBounds = concatMap $ \(Decl typ name) -> case fromAbiType typ of

src/HEVM.hs

@@ -125,7 +125,7 @@ translateActConstr (Act store [Contract ctor _]) bytecode = translateConstructor
 translateActConstr (Act _ _) _ = error "TODO multiple contracts"
 
 translateConstructor :: Layout -> Constructor -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata, Sig)
-translateConstructor layout (Constructor cid iface preconds _ _ upds _) bytecode =
+translateConstructor layout (Constructor cid iface preconds _ _ upds) bytecode =
   (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds initmap)],
   calldata, ifaceToSig iface)
   where
@@ -163,10 +163,7 @@ ifaceToSig (Interface name args) = Sig (T.pack name) (fmap fromdecl args)
 
 translateBehv :: Layout -> BS.ByteString -> Behaviour -> EVM.Expr EVM.End
 translateBehv layout bytecode (Behaviour _ cid _ preconds caseconds _ upds ret) =
-  EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr layout cid upds bytecode)
-
-rewritesToExpr :: Layout -> Id -> [Rewrite] -> BS.ByteString -> ContractMap
-rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout cid) initmap rewrites
+  EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (updatesToExpr layout cid upds initmap)
   where
     initcontract = EVM.C { EVM.code  = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode)
                          , EVM.storage = EVM.AbstractStore initAddr
@@ -175,10 +172,6 @@ rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout
                          }
     initmap = M.fromList [(initAddr, initcontract)]
 
-rewriteToExpr :: Layout -> Id -> Rewrite -> ContractMap -> ContractMap
-rewriteToExpr _ _ (Constant _) cmap = cmap
-rewriteToExpr layout cid (Rewrite upd) cmap = updateToExpr layout cid upd cmap
-
 updatesToExpr :: Layout -> Id -> [StorageUpdate] -> ContractMap -> ContractMap
 updatesToExpr layout cid upds initmap = foldl (flip $ updateToExpr layout cid) initmap upds