Merge casting with main + decompilation

src/Act/HEVM.hs

@@ -53,6 +53,7 @@ import EVM.SMT (SMTCex(..), assertProps, SMT2(..))
 import EVM.Solvers
 import EVM.Effects
 import EVM.Format as Format
+import EVM.Traversals
 
 import Debug.Trace
 
@@ -628,7 +629,7 @@ getInitContractMap casts store codemap =
     handleCast _ _ = error "Cannot have different casts to the same address"
 
 
-checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> m (ContractMap, ActEnv)
+checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> m (Error String (ContractMap, ActEnv))
 checkConstructors solvers initcode runtimecode store (Contract ctor _) codemap = do
   -- First find all casts from addresses and create a store where all asumed constracts are present
   -- currently ignoring any asts in behaviours, maybe prohibit them explicitly
@@ -657,6 +658,9 @@ checkConstructors solvers initcode runtimecode store (Contract ctor _) codemap =
   where
     removeFails branches = filter isSuccess $ branches
 
+    -- TODO remove when hevm PR is merged
+    symAddrCnstr n = fmap (\i -> EVM.PNeg (EVM.PEq (EVM.WAddr (EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show i))) (EVM.Lit 0))) [1..n]
+
 getContractMap :: [EVM.Expr EVM.End] -> ContractMap
 getContractMap [EVM.Success _ _ _ m] = m
 getContractMap _ = error "Internal error: unexpected shape of Act translation"
@@ -743,7 +747,7 @@ checkInputSpaces solvers l1 l2 = do
 
 
 -- Checks that all the casted addresses of a contract are mutually distinct
-checkAliasing :: App m => SolverGroup -> Constructor -> [Exp AInteger] -> Calldata -> m ()
+checkAliasing :: App m => SolverGroup -> Constructor -> [Exp AInteger] -> Calldata -> m (Error String ())
 checkAliasing solver constructor@(Constructor _ (Interface ifaceName decls) preconds _ _ _) addresses@(_:_) calldata = do
   let addressquery = [prelude <> SMT2 (fmap fromString $ lines . show . pretty $ mksmt) mempty mempty mempty]
   traceShowM addressquery
@@ -780,7 +784,7 @@ checkAliasing solver constructor@(Constructor _ (Interface ifaceName decls) prec
                 "(set-logic ALL)" ]
 
 
-checkAliasing _ _ _ _ = pure ()
+checkAliasing _ _ _ _ = pure $ Success ()
 
 -- | Checks whether all successful EVM behaviors are withing the
 -- interfaces specified by Act

src/Act/HEVM_utils.hs

@@ -29,6 +29,7 @@ import Act.Syntax.Annotated
 import Act.Syntax.Untyped (makeIface)
 
 import qualified EVM.Types as EVM
+import EVM.Types (VM(..))
 import EVM.Expr hiding (op2, inRange)
 import EVM.SymExec hiding (EquivResult, isPartial, abstractVM, loadSymVM)
 import EVM.Solvers
@@ -122,20 +123,21 @@ getRuntimeBranches solvers contracts calldata = do
 
 
 -- | decompiles the given EVM initcode into a list of Expr branches
-getInitcodeBranches :: App m => SolverGroup -> BS.ByteString -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> Calldata -> m [EVM.Expr EVM.End]
-getInitcodeBranches solvers initcode contracts calldata = do
-  initVM <- liftIO $ stToIO $ abstractInitVM initcode contracts calldata
+getInitcodeBranches :: App m => SolverGroup -> BS.ByteString -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> Calldata -> [EVM.Prop] -> m [EVM.Expr EVM.End]
+getInitcodeBranches solvers initcode contracts calldata precond = do
+  initVM <- liftIO $ stToIO $ abstractInitVM initcode contracts calldata precond
   expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased initVM runExpr
   let simpl = simplify expr
   let nodes = flattenExpr simpl
   checkPartial nodes
   pure nodes
 
-abstractInitVM :: BS.ByteString -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> ST s (EVM.VM EVM.Symbolic s)
-abstractInitVM contractCode contracts cd = do
+abstractInitVM :: BS.ByteString -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> [EVM.Prop] -> ST s (EVM.VM EVM.Symbolic s)
+abstractInitVM contractCode contracts cd precond = do
   let value = EVM.TxValue
   let code = EVM.InitCode contractCode (fst cd)
-  loadSymVM (EVM.SymAddr "entrypoint", EVM.initialContract code) contracts value cd True
+  vm <- loadSymVM (EVM.SymAddr "entrypoint", EVM.initialContract code) contracts value cd True
+  pure $ vm { constraints = vm.constraints <> precond }
 
 abstractVM :: [(EVM.Expr EVM.EAddr, EVM.Contract)] -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> ST s (EVM.VM EVM.Symbolic s)
 abstractVM contracts cd = do

src/Act/Traversals.hs

@@ -120,7 +120,10 @@ mapExpM f = \case
   Create p n as -> do
     as' <- mapM (mapTypedExpM f) as
     f (Create p n as')
-
+  AsContract p e c -> do
+    e' <- mapExpM f e
+    f (AsContract p e' c)
+
   --polymorphic
 
   Eq p s a b -> do