Merge pull request #209 from lefterislazar/rocq-pointers

Rocq Pointers

Author: lefterislazar

Makefile

@@ -60,7 +60,7 @@ hevm_multi_fast=$(filter-out $(hevm_multi_slow), $(hevm_multi_pass))
 failing_typing=tests/frontend/pass/dss/vat.act tests/frontend/pass/creation/createMultiple.act tests/frontend/pass/staticstore/staticstore.act
 
 
-coq-examples = tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20-simple tests/coq/ERC20 tests/coq/multi tests/coq/amm
+#coq-examples = tests/coq/multi tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20-simple tests/coq/ERC20  tests/coq/amm tests/coq/pointers
 
 .PHONY: test-coq $(coq-examples)
 test-coq: compiler $(coq-examples)
@@ -129,5 +129,5 @@ tests/hevm/pass/%.act.hevm.pass.fast:
 	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.sol))
 	./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --solver bitwuzla --smttimeout 100000000
 
-test-ci: test-parse test-type test-invariant test-postcondition test-coq test-hevm
+test-ci: test-parse test-type test-invariant test-postcondition test-coq test-hevm-fast
 test: test-ci test-cabal

lib/ActLib.v

@@ -11,17 +11,35 @@ Definition address := Z.
 Record Env : Set :=
   { Callvalue : Z;
     Caller : address;
+    This : address;
     Blockhash : Z;
     Blocknumber : Z;
     Difficulty : Z;
     Timestamp : Z;
     Gaslimit : Z;
     Coinbase : address;
     Chainid : Z;
-    This : address;
     Origin : address;
     Nonce : Z;
-    Calldepth : Z }.
+    Calldepth : Z;
+    NextAddr : address }.
+
+Definition NextEnv (ENV : Env) : Env :=
+  {| Callvalue := Callvalue ENV;
+     Caller := Caller ENV;
+     This := This ENV;
+     Blockhash := Blockhash ENV;
+     Blocknumber := Blocknumber ENV;
+     Difficulty := Difficulty ENV;
+     Timestamp := Timestamp ENV;
+     Gaslimit := Gaslimit ENV;
+     Coinbase := Coinbase ENV;
+     Chainid := Chainid ENV;
+     Origin := Origin ENV;
+     Nonce := Nonce ENV;
+     Calldepth := Calldepth ENV;
+     NextAddr := (NextAddr ENV + 1)%Z |}.
+
 
 (** * integer bounds *)
 Definition UINT_MIN (n : Z) := 0.

src/Act/Bounds.hs

@@ -10,6 +10,7 @@ import Data.Type.Equality
 import Act.Syntax
 import Act.Syntax.TypedExplicit
 import Act.Type (globalEnv)
+import Debug.Trace
 
 
 {-|
@@ -30,7 +31,7 @@ addBounds (Act store contracts) = Act store (addBoundsContract <$> contracts)
 -- | Adds type bounds for calldata, environment vars, and external storage vars
 -- as preconditions
 addBoundsConstructor :: Constructor -> Constructor
-addBoundsConstructor ctor@(Constructor _ (Interface _ decls) _ pre post invs stateUpdates) =
+addBoundsConstructor ctor@(Constructor _ (Interface _ decls) pre post invs stateUpdates) =
   ctor { _cpreconditions = pre'
        , _cpostconditions = post'
        , _invariants = invs' }
@@ -41,7 +42,7 @@ addBoundsConstructor ctor@(Constructor _ (Interface _ decls) _ pre post invs sta
               -- The following is sound as values of locations outside local storage
               -- already exist as the constructor starts executing,
               -- and the constructor cannot modify non-local locations.
-             <> mkLocationBounds nonlocalLocs
+             <> mkLocationBounds (toPrestate stateUpdates <$> nonlocalLocs)
       invs' = addBoundsInvariant ctor <$> invs
       post' = post <> mkStorageBounds stateUpdates Post
 
@@ -50,15 +51,48 @@ addBoundsConstructor ctor@(Constructor _ (Interface _ decls) _ pre post invs sta
              <> concatMap locsFromUpdate stateUpdates
       nonlocalLocs = filter (not . isLocalLoc) locs
 
+
+changeBase :: Location -> StorageUpdate -> Maybe Location
+changeBase _ (Update _ (Item _ _ _) e) | isCreate e = Nothing
+  -- TODO: suppport!
+  where
+    isCreate :: Exp a -> Bool
+    isCreate (Address _ (Create _ _ _)) = True
+    isCreate (Create _ _ _) = True
+    isCreate _ = False
+changeBase (Loc st SStorage (Item _ vt baseref)) (Update _ (Item _ _ updatedRef) (VarRef _ _ sk' (Item _ _ ru'))) =
+  Loc st sk' . Item st vt <$> hasBase baseref ru'
+  where
+    hasBase :: Ref Storage -> Ref k -> Maybe (Ref k)
+    hasBase r''@(SVar _ _ _) ru =
+      if updatedRef == r'' then Just ru else Nothing
+    hasBase r''@(SArray pn r' vt' ixs) ru =
+      if updatedRef == r'' then Just ru
+      else (\_r -> SArray pn _r vt' ixs) <$> hasBase r' ru
+    hasBase r''@(SMapping pn r' vt' ixs) ru =
+      if updatedRef == r'' then Just ru
+      else (\_r -> SMapping pn _r vt' ixs) <$> hasBase r' ru
+    hasBase r''@(SField pn r' id' id'') ru =
+      if updatedRef == r'' then Just ru
+      else (\_r -> SField pn _r id' id'') <$> hasBase r' ru
+changeBase _ _ = Nothing
+
+toPrestate :: [StorageUpdate] -> Location -> Location
+toPrestate _ loc@(Loc _ SCalldata _) = loc
+toPrestate updates loc@(Loc _ SStorage _) =
+  case mapMaybe (changeBase loc) updates of
+    [] -> loc
+    l -> last l
+
 -- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
 addBoundsBehaviour :: Behaviour -> Behaviour
-addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) _ pre cases post stateUpdates ret) =
+addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) pre cases post stateUpdates ret) =
   behv { _preconditions = pre', _postconditions = post' }
     where
       pre' = nub $ pre
              <> mkCallDataBounds decls
              <> mkStorageBounds stateUpdates Pre
-             <> mkLocationBounds locs
+             <> mkLocationBounds (toPrestate stateUpdates <$> locs)
              <> mkEthEnvBounds (ethEnvFromBehaviour behv)
       post' = post
               <> mkStorageBounds stateUpdates Post
@@ -69,7 +103,7 @@ addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) _ pre cases post stat
 
 -- | Adds type bounds for calldata, environment vars, and storage vars
 addBoundsInvariant :: Constructor -> Invariant -> Invariant
-addBoundsInvariant (Constructor _ (Interface _ decls) _ _ _ _ _) inv@(Invariant _ preconds storagebounds (PredTimed predicate _)) =
+addBoundsInvariant (Constructor _ (Interface _ decls) _ _ _ _) inv@(Invariant _ preconds storagebounds (PredTimed predicate _)) =
   inv { _ipreconditions = preconds', _istoragebounds = storagebounds' }
     where
       preconds' = nub $ preconds
@@ -139,9 +173,12 @@ mkLocationBounds refs = concatMap mkBound refs
     mkItemBounds SCalldata = mkCItemBounds
 
 mkCallDataBounds :: [Decl] -> [Exp ABoolean]
-mkCallDataBounds = concatMap $ \(Decl typ name) -> case typ of
-  -- Array element bounds are applied lazily when needed in mkCalldataLocationBounds
-  (AbiArrayType _ _) -> []
-  _ -> case fromAbiType typ of
-        AInteger -> [bound typ (_Var typ name)]
-        _ -> []
+mkCallDataBounds = concatMap $ \(Decl argtyp name) -> case argtyp of
+  (AbiArg typ) ->
+    case typ of
+      -- Array element bounds are applied lazily when needed in mkCalldataLocationBounds
+      (AbiArrayType _ _) -> []
+      _ -> case fromAbiType typ of
+            AInteger -> [bound typ (_Var typ name)]
+            _ -> []
+  (ContractArg _ cid) -> [bound AbiAddressType (Address cid (_Var AbiAddressType name))]

src/Act/Consistency.hs

@@ -70,7 +70,7 @@ mkExhaustiveAssertion caseconds =
 
 -- | Create a query for cases
 mkCaseQuery :: ([Exp ABoolean] -> Exp ABoolean) -> [Behaviour] -> (Id, SMTExp, (SolverInstance -> IO Model))
-mkCaseQuery props behvs@((Behaviour _ _ (Interface ifaceName decls) _ preconds _ _ _ _):_) =
+mkCaseQuery props behvs@((Behaviour _ _ (Interface ifaceName decls) preconds _ _ _ _):_) =
   (ifaceName, smt, getModel)
   where
     locs = nub $ concatMap locsFromExp (preconds <> caseconds)
@@ -120,7 +120,7 @@ checkCases (Act _ contracts) solver' smttimeout debug = do
 
     where
 
-      sameIface (Behaviour _ _ iface _ _ _ _ _ _) (Behaviour _ _ iface' _ _ _ _ _ _) =
+      sameIface (Behaviour _ _ iface _ _ _ _ _) (Behaviour _ _ iface' _ _ _ _ _) =
         makeIface iface == makeIface iface'
 
       checkRes :: String -> (Id, SMT.SMTResult) -> IO ()
@@ -154,7 +154,7 @@ mkStorageBounds (Loc _ _ (Item _ _ ref)) = mkRefBounds ref
 
 -- TODO: There are locs that don't need to be checked, e.g. assignment locs cannot be out of bounds
 mkConstrArrayBoundsQuery :: Constructor -> (Id, [Location], SMTExp, SolverInstance -> IO Model)
-mkConstrArrayBoundsQuery constructor@(Constructor _ (Interface ifaceName decls) _ preconds _ _ initialStorage) =
+mkConstrArrayBoundsQuery constructor@(Constructor _ (Interface ifaceName decls) preconds _ _ initialStorage) =
   (ifaceName, arrayLocs, smt, getModel)
   where
     -- Declare vars
@@ -171,7 +171,7 @@ mkConstrArrayBoundsQuery constructor@(Constructor _ (Interface ifaceName decls)
     getModel = getCtorModel constructor
 
 mkBehvArrayBoundsQuery :: Behaviour -> (Id, [Location], SMTExp, SolverInstance -> IO Model)
-mkBehvArrayBoundsQuery behv@(Behaviour _ _ (Interface ifaceName decls) _ preconds caseconds _ stateUpdates _) =
+mkBehvArrayBoundsQuery behv@(Behaviour _ _ (Interface ifaceName decls) preconds caseconds _ stateUpdates _) =
   (ifaceName, arrayLocs, smt, getModel)
   where
     -- Declare vars
@@ -280,7 +280,7 @@ mkAliasingAssertion :: [Location] -> Exp ABoolean
 mkAliasingAssertion ls = mkOr $ map (uncurry mkEqualityAssertion) $ combine ls
 
 mkAliasingQuery :: Behaviour -> (Id, [[Location]], SMTExp, SolverInstance -> IO Model)
-mkAliasingQuery behv@(Behaviour _ _ (Interface ifaceName decls) _ preconds caseconds _ stateUpdates _) =
+mkAliasingQuery behv@(Behaviour _ _ (Interface ifaceName decls) preconds caseconds _ stateUpdates _) =
   (ifaceName, groupedLocs, smt, getModel)
   where
     updatedLocs = locFromUpdate <$> stateUpdates
@@ -391,6 +391,7 @@ modelExpand :: SType (AArray a) -> Exp (AArray a) -> ModelCtx [Exp (Base (AArray
 modelExpand (SSArray SInteger) (Array _ l) = pure l
 modelExpand (SSArray SBoolean) (Array _ l) = pure l
 modelExpand (SSArray SByteStr) (Array _ l) = pure l
+modelExpand (SSArray SContract) (Array _ l) = pure l
 modelExpand (SSArray s@(SSArray _)) (Array _ l) = concat <$> mapM (modelExpand s) l
 modelExpand typ (VarRef _ whn SStorage item) = do
   model <- ask