Skip to content

Commit

Permalink
WIP in typing
Browse files Browse the repository at this point in the history
  • Loading branch information
@zoep
zoep committed Oct 9, 2024
1 parent 457b8ef commit 7353ffb
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 38 deletions.
32 changes: 16 additions & 16 deletions src/Act/Syntax/TimeAgnostic.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,13 +170,13 @@ instance Eq (StorageRef t) where
-- with two identifiers: the contract that the fields belongs to and
-- the name of the field name.
data VarRef (t :: Timing) where
VVar :: Pn -> Id -> VarRef t
VField :: Pn -> VarRef t -> Id -> Id -> VarRef t
VVar :: Pn -> AbiType -> Id -> VarRef t
VField :: Pn -> SlotType -> VarRef t -> Id -> Id -> VarRef t
deriving instance Show (VarRef t)

instance Eq (VarRef t) where
VVar _ x == VVar _ x' = x == x'
VField _ r c x == VField _ r' c' x' = r == r' && c == c' && x == x'
VVar _ t x == VVar _ t' x' = t == t' && x == x'
VField _ r vt c x == VField _ r' vt' c' x' = vt == vt' && r == r' && c == c' && x == x'
_ == _ = False

_Item :: SingI a => ValueType -> StorageRef t -> TStorageItem a t
Expand Down Expand Up @@ -237,7 +237,7 @@ data Exp (a :: ActType) (t :: Timing) where
Eq :: Pn -> SType a -> Exp a t -> Exp a t -> Exp ABoolean t
NEq :: Pn -> SType a -> Exp a t -> Exp a t -> Exp ABoolean t
ITE :: Pn -> Exp ABoolean t -> Exp a t -> Exp a t -> Exp a t
Var :: Pn -> SType a -> AbiType -> VarRef t -> Exp a t
Var :: Pn -> SType a -> VarRef t -> Exp a t
TEntry :: Pn -> Time t -> TStorageItem a t -> Exp a t
deriving instance Show (Exp a t)

Expand Down Expand Up @@ -279,7 +279,7 @@ instance Eq (Exp a t) where

ITE _ a b c == ITE _ d e f = a == d && b == e && c == f
TEntry _ a t == TEntry _ b u = a == b && t == u
Var _ _ _ a == Var _ _ _ b = a == b
Var _ _ a == Var _ _ b = a == b

Create _ a b == Create _ c d = a == c && b == d

Expand Down Expand Up @@ -340,7 +340,7 @@ instance Timable (Exp a) where
NEq p s x y -> NEq p s (go x) (go y)
ITE p x y z -> ITE p (go x) (go y) (go z)
TEntry p _ item -> TEntry p time (go item)
Var p t a x -> Var p t a (go x)
Var p t x -> Var p t (go x)
where
go :: Timable c => c Untimed -> c Timed
go = setTime time
Expand All @@ -354,8 +354,8 @@ instance Timable StorageRef where
setTime _ (SVar p c x) = SVar p c x

instance Timable VarRef where
setTime time (VField p e c x) = VField p (setTime time e) c x
setTime _ (VVar p x) = VVar p x
setTime time (VField p vt e c x) = VField p vt(setTime time e) c x
setTime _ (VVar p at x) = VVar p at x

------------------------
-- * JSON instances * --
Expand Down Expand Up @@ -464,10 +464,11 @@ instance ToJSON (StorageRef t) where
toJSON (SField _ e c x) = field e c x

instance ToJSON (VarRef t) where
toJSON (VVar _ x) = object [ "kind" .= pack "Var"
, "var" .= pack x
]
toJSON (VField _ e c x) = field e c x
toJSON (VVar _ at x) = object [ "kind" .= pack "Var"
, "var" .= pack x
, "abitype" .= toJSON at
]
toJSON (VField _ _ e c x) = field e c x

mapping :: (ToJSON a1, ToJSON a2) => a1 -> a2 -> Value
mapping a b = object [ "kind" .= pack "Mapping"
Expand Down Expand Up @@ -538,9 +539,8 @@ instance ToJSON (Exp a t) where
, "type" .= pack "bytestring" ]
toJSON (TEntry _ t a) = object [ "entry" .= toJSON a
, "timing" .= show t ]
toJSON (Var _ t abitype a) = object [ "var" .= toJSON a
, "abitype" .= toJSON abitype
, "type" .= show t ]
toJSON (Var _ t a) = object [ "var" .= toJSON a
, "type" .= show t ]
toJSON (Create _ f xs) = object [ "symbol" .= pack "create"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [object [ "fun" .= String (pack f) ], toJSON xs]) ]
Expand Down
47 changes: 25 additions & 22 deletions src/Act/Type.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -385,34 +385,33 @@ validateEntry env entry =
StorageMapping _ _ -> throw (getPosEntry entry, "Top-level expressions cannot have mapping type")


checkVar :: forall t. Typeable t => Env -> U.Entry -> Err (SlotType, StorageRef t)
checkVar Env{contract,store,calldata} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of
checkVar :: forall t. Typeable t => Env -> U.Entry -> Err (SlotType, Maybe Id, VarRef t)
checkVar Env{contract,store,calldata, pointers} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of
(Just _, Just _) -> throw (p, "Ambiguous variable " <> name)
(Just typ, Nothing) -> pure (typ, SVar p contract name)
(Nothing, Just _) -> throw (p, "Variable " <> name <> " is not a storage variable")
(Nothing, Nothing) -> throw (p, "Unknown storage variable " <> show name)
(Nothing, Just typ) -> do
pure (StorageValue (PrimitiveType typ), Map.lookup name pointers, VVar p typ name)
(Just _, Nothing) -> error $ "Internal error: Variable must be a calldata variable."
(Nothing, Nothing) -> throw (p, "Unknown variable " <> show name)
-- TODO more consitent check of name overlap between calldata and storage
checkVar env (U.EMapping p e args) =
checkEntry env e `bindValidation` \(typ, ref) -> case typ of
StorageValue _ -> throw (p, "Expression should have a mapping type" <> show e)
StorageMapping argtyps restyp -> (StorageValue restyp,) . SMapping p ref <$> checkIxs env p args (NonEmpty.toList argtyps)
checkVar env (U.EMapping p e args) = throw (p, "Variables cannot have a mapping type")
checkVar env@Env{theirs} (U.EField p e x) =
checkEntry env e `bindValidation` \(typ, ref) -> case typ of
StorageValue (ContractType c) -> case Map.lookup c theirs of
checkVar env e `bindValidation` \(typ, oc, ref) -> case oc of
Just c -> case Map.lookup c theirs of
Just cenv -> case Map.lookup x cenv of
Just (t, _) -> pure (t, SField p ref c x)
Just (st@(StorageValue (ContractType c')), _) -> pure (st, Just c', VField p st ref c x)
Just (st, _) -> pure (st, Nothing, VField p st ref c x)
Nothing -> throw (p, "Contract " <> c <> " does not have field " <> x)
Nothing -> error $ "Internal error: Invalid contract type " <> show c
_ -> throw (p, "Expression should have a contract type" <> show e)



validateVar :: forall t. Typeable t => Env -> U.Entry -> Err (AbiType, VarRef t)
validateVar env entry =
checkEntry env entry `bindValidation` \(typ, ref) -> case typ of
validateVar :: forall t. Typeable t => Env -> U.Entry -> Err (ValueType, VarRef t)
validateVar env var =
checkVar env var `bindValidation` \(typ, _, ref) -> case typ of
StorageValue t -> pure (t, ref)
-- TODO can mappings be assigned?
StorageMapping _ _ -> throw (getPosEntry entry, "Top-level expressions cannot have mapping type")
StorageMapping _ _ -> throw (getPosEntry var, "Top-level expressions cannot have mapping type")


-- | Typechecks a non-constant rewrite.
checkStorageExpr :: Env -> U.Entry -> U.Expr -> Err StorageUpdate
Expand All @@ -439,7 +438,7 @@ checkIffs env = foldr check (pure [])

genInRange :: AbiType -> Exp AInteger t -> [Exp ABoolean t]
genInRange t e@(LitInt _ _) = [InRange nowhere t e]
genInRange t e@(Var _ _ _ _) = [InRange nowhere t e]
genInRange t e@(Var _ _ _) = [InRange nowhere t e]
genInRange t e@(TEntry _ _ _) = [InRange nowhere t e]
genInRange t e@(Add _ e1 e2) = [InRange nowhere t e] <> genInRange t e1 <> genInRange t e2
genInRange t e@(Sub _ e1 e2) = [InRange nowhere t e] <> genInRange t e1 <> genInRange t e2
Expand Down Expand Up @@ -516,8 +515,9 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of
Just AByteStr -> pure $ ByEnv p v1
_ -> throw (p, "Unknown environment variable " <> show v1)
-- Variable references
(_, U.EUTEntry entry) | isCalldataEntry env entry -> validateVar env entry `bindValidation` \(at@(FromAbi varType), ref) ->
checkTime (getPosEntry entry) <*> (Var (getPosEntry entry) typ at ref <$ checkEq (getPosEntry entry) typ varTyp)
(_, U.EUTEntry entry) | isCalldataEntry env entry -> validateVar env entry `bindValidation` \((FromVType typ'), ref) ->
checkTime (getPosEntry entry) <*> (Var (getPosEntry entry) typ ref <$ checkEq (getPosEntry entry) typ typ')
-- Storage references
(_, U.EUTEntry entry) -> validateEntry env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
checkTime (getPosEntry entry) <*> (TEntry (getPosEntry entry) Neither (Item typ vt ref) <$ checkEq (getPosEntry entry) typ typ')
(_, U.EPreEntry entry) -> validateEntry env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
Expand Down Expand Up @@ -560,11 +560,14 @@ checkContractType env SInteger (ITE p _ a b) =
(_, _ )-> pure Nothing
checkContractType _ SInteger (Create _ c _) = pure $ Just c
-- TODO Fix
checkContractType Env{pointers} SInteger (Var _ _ _ x) =
checkContractType Env{pointers} SInteger (Var _ _ (VVar _ _ x)) =
case Map.lookup x pointers of
Just c -> pure $ Just c
Nothing -> pure Nothing

checkContractType Env{pointers} SInteger (Var _ _ (VField _ st _ _ _)) =
case st of
StorageValue (ContractType c) -> pure $ Just c
_ -> pure $ Nothing
checkContractType _ _ (TEntry _ _ (Item _ (ContractType c) _)) = pure $ Just c
checkContractType _ SInteger _ = pure Nothing
checkContractType _ SBoolean _ = pure Nothing
Expand Down

0 comments on commit 7353ffb

Please sign in to comment.