syntax for pointers block

src/Act/Lex.x

@@ -40,6 +40,7 @@ tokens :-
   iff $white+ in $white+ range          { mk IFFINRANGE }
   inRange                               { mk INRANGE }
   iff                                   { mk IFF }
+  pointers                              { mk POINTERS }
   and                                   { mk AND }
   not                                   { mk NOT }
   or                                    { mk OR }
@@ -89,6 +90,7 @@ tokens :-
   -- symbols
   ":="                                  { mk ASSIGN }
   "=>"                                  { mk ARROW }
+  "|->"                                 { mk POINTSTO }
   "=="                                  { mk EQEQ }
   "=/="                                 { mk NEQ }
   ">="                                  { mk GE }
@@ -136,6 +138,8 @@ data LEX =
   | IFFINRANGE
   | INRANGE
   | IFF
+  | POINTERS
+  | POINTSTO
   | AND
   | NOT
   | OR

src/Act/Parse.y

@@ -29,6 +29,7 @@ import Act.Error
   'iff in range'              { L IFFINRANGE _ }
   'inRange'                   { L INRANGE _ }
   'iff'                       { L IFF _ }
+  'pointers'                  { L POINTERS _ }
   'and'                       { L AND _ }
   'not'                       { L NOT _ }
   'or'                        { L OR _ }
@@ -76,6 +77,7 @@ import Act.Error
   -- symbols
   ':='                        { L ASSIGN _ }
   '=>'                        { L ARROW _ }
+  '|->'                       { L POINTSTO _ }
   '=='                        { L EQEQ _ }
   '=/='                       { L NEQ _ }
   '>='                        { L GE _ }
@@ -163,18 +165,20 @@ Contract : Constructor list(Transition)              { Contract $1 $2 }
 
 Transition : 'behaviour' id 'of' id
              Interface
+             list(Pointer)
              list(Precondition)
              Cases
              Ensures                                  { Transition (posn $1) (name $2) (name $4)
-                                                        $5 $6 $7 $8 }
+                                                        $5 $6 $7 $8 $9 }
 
 Constructor : 'constructor' 'of' id
               CInterface
+              list(Pointer)
               list(Precondition)
               Creation
               Ensures
               Invariants                              { Definition (posn $3) (name $3)
-                                                         $4 $5 $6 $7 $8 }
+                                                         $4 $5 $6 $7 $8 $9 }
 
 Ensures : optblock('ensures', Expr)                   { $1 }
 
@@ -184,6 +188,8 @@ Interface : 'interface' id '(' seplist(Decl, ',') ')' { Interface (name $2) $4 }
 
 CInterface : 'interface' 'constructor' '(' seplist(Decl, ',') ')' { Interface "constructor" $4 }
 
+Pointer : id '|->' id                                 { PointsTo (posn $2) (name $1) (name $3) }
+
 Cases : Post                                          { Direct $1 }
       | nonempty(Case)                                { Branches $1 }
 
@@ -282,7 +288,6 @@ Expr : '(' Expr ')'                                   { $2 }
   | 'pre'  '(' Entry ')'                              { EPreEntry $3 }
   | 'post' '(' Entry ')'                              { EPostEntry $3 }
   | 'create' id '(' seplist(Expr, ',') ')'            { ECreate (posn $2) (name $2) $4 }
-  | Expr 'as' id                                      { EAsContract (posn $2) $1 (name $3) }
   | Expr '++' Expr                                    { ECat   (posn $2) $1 $3 }
 --  | id '[' Expr '..' Expr ']'                       { ESlice (posn $2) $1 $3 $5 }
   | 'CALLER'                                          { EnvExp (posn $1) Caller }
@@ -318,6 +323,6 @@ parseError ((L token pn):_) =
     show token])
 
 emptyConstructor :: Transition -> Definition
-emptyConstructor (Transition _ _ c _ _ _ _) = Definition nowhere c (Interface "constructor" []) [] (Creates []) [] []
+emptyConstructor (Transition _ _ c _ _ _ _ _) = Definition nowhere c (Interface "constructor" []) [] [] (Creates []) [] []
 
 }

src/Act/Print.hs

@@ -29,9 +29,10 @@ prettyContract :: Contract t -> String
 prettyContract (Contract ctor behvs) = unlines $ intersperse "\n" $ (prettyCtor ctor):(fmap prettyBehaviour behvs)
 
 prettyCtor :: Constructor t -> String
-prettyCtor (Constructor name interface pres posts invs initStore)
+prettyCtor (Constructor name interface ptrs pres posts invs initStore)
   =   "constructor of " <> name
   >-< "interface " <> show interface
+  <> prettyPtrs ptrs
   <> prettyPre pres
   <> prettyCreates initStore
   <> prettyPost posts
@@ -52,9 +53,10 @@ prettyValueType = \case
 
 
 prettyBehaviour :: Behaviour t -> String
-prettyBehaviour (Behaviour name contract interface preconditions cases postconditions stateUpdates returns)
+prettyBehaviour (Behaviour name contract interface ptrs preconditions cases postconditions stateUpdates returns)
   =   "behaviour " <> name <> " of " <> contract
   >-< "interface " <> (show interface)
+  <> prettyPtrs ptrs
   <> prettyPre preconditions
   <> prettyCases cases
   <> prettyStorage stateUpdates
@@ -69,6 +71,12 @@ prettyBehaviour (Behaviour name contract interface preconditions cases postcondi
 
 
 
+prettyPtrs :: [(Pn, Id, Id)] -> String
+prettyPtrs [] = ""
+prettyPtrs ptrs = header "pointers" >-< block (prettyPtr <$> p)
+  where
+    prettyPtr (_, x, c) = x <> " |-> " <> c
+
 prettyPre :: [Exp ABoolean t] -> String
 prettyPre [] = ""
 prettyPre p = header "iff" >-< block (prettyExp <$> p)
@@ -131,7 +139,6 @@ prettyExp e = case e of
 
   -- contracts
   Create _ f ixs -> f <> "(" <> (intercalate "," $ fmap prettyTypedExp ixs) <> ")"
-  AsContract _ a c -> prettyExp a <> " as " <> c
 
   --polymorphic
   ITE _ a b c -> "(if " <> prettyExp a <> " then " <> prettyExp b <> " else " <> prettyExp c <> ")"
@@ -223,7 +230,6 @@ prettyInvPred = prettyExp . untime . fst
       InRange p a b -> InRange p a (untime b)
       LitBool p a -> LitBool p a
       Create p f xs -> Create p f (fmap untimeTyped xs)
-      AsContract p a c -> AsContract p (untime a) c
       IntEnv p a  -> IntEnv p a
       ByEnv p a   -> ByEnv p a
       ITE p x y z -> ITE p (untime x) (untime y) (untime z)

src/Act/Syntax.hs

@@ -28,15 +28,15 @@ invExp :: Annotated.InvariantPred -> Annotated.Exp ABoolean
 invExp = uncurry (<>)
 
 locsFromBehaviour :: Annotated.Behaviour -> [Annotated.StorageLocation]
-locsFromBehaviour (Behaviour _ _ _ preconds cases postconds rewrites returns) = nub $
+locsFromBehaviour (Behaviour _ _ _ _ preconds cases postconds rewrites returns) = nub $
   concatMap locsFromExp preconds
   <> concatMap locsFromExp cases
   <> concatMap locsFromExp postconds
   <> concatMap locsFromUpdate rewrites
   <> maybe [] locsFromTypedExp returns
 
 locsFromConstructor :: Annotated.Constructor -> [Annotated.StorageLocation]
-locsFromConstructor (Constructor _ _ pre post inv initialStorage) = nub $
+locsFromConstructor (Constructor _ _ _ pre post inv initialStorage) = nub $
   concatMap locsFromExp pre
   <> concatMap locsFromExp post
   <> concatMap locsFromInvariant inv
@@ -52,7 +52,7 @@ locsFromInvariant (Invariant _ pre bounds (predpre, predpost)) =
 ------------------------------------
 
 nameOfContract :: Contract t -> Id
-nameOfContract (Contract (Constructor cname _ _ _ _ _) _) = cname
+nameOfContract (Contract (Constructor cname _ _ _ _ _ _) _) = cname
 
 behvsFromAct :: Agnostic.Act t -> [Behaviour t]
 behvsFromAct (Act _ contracts) = behvsFromContracts contracts
@@ -111,7 +111,6 @@ locsFromExp = nub . go
       IntEnv {} -> []
       ByEnv {} -> []
       Create _ _ es -> concatMap locsFromTypedExp es
-      AsContract _ x _ -> go x
       ITE _ x y z -> go x <> go y <> go z
       TEntry _ _ a -> locsFromItem a
       Var {} -> []
@@ -151,7 +150,6 @@ createsFromExp = nub . go
       IntEnv {} -> []
       ByEnv {} -> []
       Create _ f es -> [f] <> concatMap createsFromTypedExp es
-      AsContract _ x _ -> go x
       ITE _ x y z -> go x <> go y <> go z
       TEntry _ _ a -> createsFromItem a
       Var {} -> []
@@ -167,7 +165,7 @@ createsFromContract (Contract constr behvs) =
   createsFromConstructor constr <> concatMap createsFromBehaviour behvs
 
 createsFromConstructor :: Typed.Constructor -> [Id]
-createsFromConstructor (Constructor _ _ pre post inv initialStorage) = nub $
+createsFromConstructor (Constructor _ _ _ pre post inv initialStorage) = nub $
   concatMap createsFromExp pre
   <> concatMap createsFromExp post
   <> concatMap createsFromInvariant inv
@@ -182,43 +180,23 @@ createsFromUpdate update = nub $ case update of
   Update _ item e -> createsFromItem item <> createsFromExp e
 
 createsFromBehaviour :: Behaviour t -> [Id]
-createsFromBehaviour (Behaviour _ _ _ _ preconds postconds rewrites returns) = nub $
+createsFromBehaviour (Behaviour _ _ _ _ _ preconds postconds rewrites returns) = nub $
   concatMap createsFromExp preconds
   <> concatMap createsFromExp postconds
   <> concatMap createsFromUpdate rewrites
   <> maybe [] createsFromTypedExp returns
 
 
-castsFromExp :: Exp a t -> [(Exp AInteger t, Id)]
-castsFromExp = nub . go
-  where
-    go :: Exp a t -> [(Exp AInteger t, Id)]
-    go e = case e of
-      AsContract _ e' c -> [(e', c)]
-      _ -> []
-
-castsFromUpdate :: StorageUpdate t -> [(Exp AInteger t, Id)]
-castsFromUpdate update = nub $ case update of
-  Update _ _ e -> castsFromExp e
-
-castsFromContract :: Contract t -> [(Exp AInteger t, Id)]
-castsFromContract (Contract constr _) =
-  castsFromConstructor constr
-
-castsFromConstructor :: Constructor t -> [(Exp AInteger t, Id)]
-castsFromConstructor (Constructor _ _ _ _ _ initialStorage) = nub $ concatMap castsFromUpdate initialStorage
-
-
 ethEnvFromBehaviour :: Behaviour t -> [EthEnv]
-ethEnvFromBehaviour (Behaviour _ _ _ preconds cases postconds rewrites returns) = nub $
+ethEnvFromBehaviour (Behaviour _ _ _ _ preconds cases postconds rewrites returns) = nub $
   concatMap ethEnvFromExp preconds
   <> concatMap ethEnvFromExp cases
   <> concatMap ethEnvFromExp postconds
   <> concatMap ethEnvFromUpdate rewrites
   <> maybe [] ethEnvFromTypedExp returns
 
 ethEnvFromConstructor :: Annotated.Constructor -> [EthEnv]
-ethEnvFromConstructor (Constructor _ _ pre post inv initialStorage) = nub $
+ethEnvFromConstructor (Constructor _ _ _ pre post inv initialStorage) = nub $
   concatMap ethEnvFromExp pre
   <> concatMap ethEnvFromExp post
   <> concatMap ethEnvFromInvariant inv
@@ -275,7 +253,6 @@ ethEnvFromExp = nub . go
       IntEnv _ a -> [a]
       ByEnv _ a -> [a]
       Create _ _ ixs -> concatMap ethEnvFromTypedExp ixs
-      AsContract _ a _ -> go a
       TEntry _ _ a -> ethEnvFromItem a
       Var {} -> []
 
@@ -339,7 +316,7 @@ nameFromEntry (EMapping _ e _) = nameFromEntry e
 nameFromEntry (EField _ e _) = nameFromEntry e
 
 nameFromBehv :: Annotated.Behaviour -> Id
-nameFromBehv (Behaviour _ _ (Interface ifaceName _) _ _ _ _ _) = ifaceName
+nameFromBehv (Behaviour _ _ (Interface ifaceName _) _ _ _ _ _ _) = ifaceName
 
 getPosEntry :: Entry -> Pn
 getPosEntry (EVar pn _) = pn
@@ -366,7 +343,6 @@ getPosn expr = case expr of
     EMod pn _ _ -> pn
     EExp pn _ _ -> pn
     ECreate pn _ _ -> pn
-    EAsContract pn _ _ -> pn
     EUTEntry e -> getPosEntry e
     EPreEntry e -> getPosEntry e
     EPostEntry e -> getPosEntry e
@@ -412,7 +388,6 @@ idFromRewrites e = case e of
   EPreEntry en      -> idFromEntry en
   EPostEntry en     -> idFromEntry en
   ECreate p x es    -> insertWith (<>) x [p] $ idFromRewrites' es
-  EAsContract p a c -> insertWith (<>) c [p] $ idFromRewrites a
   ListConst a       -> idFromRewrites a
   ECat _ a b        -> idFromRewrites' [a,b]
   ESlice _ a b c    -> idFromRewrites' [a,b,c]

src/Act/Syntax/TimeAgnostic.hs

@@ -48,7 +48,7 @@ import Data.Kind
 import Act.Parse          as Act.Syntax.TimeAgnostic (nowhere)
 import Act.Syntax.Types   as Act.Syntax.TimeAgnostic
 import Act.Syntax.Timing  as Act.Syntax.TimeAgnostic
-import Act.Syntax.Untyped as Act.Syntax.TimeAgnostic (Id, Pn, Interface(..), EthEnv(..), Decl(..), SlotType(..), ValueType(..))
+import Act.Syntax.Untyped as Act.Syntax.TimeAgnostic (Id, Pn, Interface(..), EthEnv(..), Decl(..), SlotType(..), ValueType(..), Pointer(..))
 
 -- AST post typechecking
 data Act t = Act Store [Contract t]
@@ -96,6 +96,7 @@ type family InvariantPred (t :: Timing) = (pred :: Type) | pred -> t where
 data Constructor t = Constructor
   { _cname :: Id
   , _cinterface :: Interface
+  , _cpointers :: [Pointer]
   , _cpreconditions :: [Exp ABoolean t]
   , _cpostconditions :: [Exp ABoolean Timed]
   , _invariants :: [Invariant t]
@@ -109,6 +110,7 @@ data Behaviour t = Behaviour
   { _name :: Id
   , _contract :: Id
   , _interface :: Interface
+  , _pointers :: [Pointer]
   , _preconditions :: [Exp ABoolean t] -- if preconditions are not satisfied execution is reverted
   , _caseconditions :: [Exp ABoolean t] -- if preconditions are satisfied and a case condition is not, some other instance of the bahaviour should apply
   , _postconditions :: [Exp ABoolean Timed]
@@ -177,7 +179,6 @@ _TExp expr = TExp sing expr
 instance Eq (TypedExp t) where
   TExp SType e1 == TExp SType e2 = eqS e1 e2
 
-
 -- | Expressions parametrized by a timing `t` and a type `a`. `t` can be either `Timed` or `Untimed`.
 -- All storage entries within an `Exp a t` contain a value of type `Time t`.
 -- If `t ~ Timed`, the only possible such values are `Pre, Post :: Time Timed`, so each storage entry
@@ -218,7 +219,6 @@ data Exp (a :: ActType) (t :: Timing) where
   ByEnv :: Pn -> EthEnv -> Exp AByteStr t
   -- contracts
   Create   :: Pn -> Id -> [TypedExp t] -> Exp AContract t
-  AsContract :: Pn -> Exp AInteger t -> Id -> Exp AContract t
   -- polymorphic
   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
@@ -268,7 +268,6 @@ instance Eq (Exp a t) where
   Var _ _ _ a == Var _ _ _ b = a == b
 
   Create _ a b == Create _ c d = a == c && b == d
-  AsContract _ a b == AsContract _ c d = a == c && b == d
 
   _ == _ = False
 
@@ -321,7 +320,6 @@ instance Timable (Exp a) where
     ByEnv p x -> ByEnv p x
     -- contracts
     Create p x y -> Create p x (go <$> y)
-    AsContract p x y -> AsContract p (go x) y
 
     -- polymorphic
     Eq  p s x y -> Eq p s (go x) (go y)
@@ -377,6 +375,7 @@ instance ToJSON (Constructor Timed) where
   toJSON Constructor{..} = object [ "kind" .= String "Constructor"
                                   , "contract" .= _cname
                                   , "interface" .= toJSON _cinterface
+                                  , "pointers" .= toJSON _cpointers
                                   , "preConditions" .= toJSON _cpreconditions
                                   , "postConditions" .= toJSON _cpostconditions
                                   , "invariants" .= listValue (\i@Invariant{..} -> invariantJSON i _predicate) _invariants
@@ -386,6 +385,7 @@ instance ToJSON (Constructor Untimed) where
   toJSON Constructor{..} = object [ "kind" .= String "Constructor"
                                   , "contract" .= _cname
                                   , "interface" .= toJSON _cinterface
+                                  , "pointers" .= toJSON _cpointers
                                   , "preConditions" .= toJSON _cpreconditions
                                   , "postConditions" .= toJSON _cpostconditions
                                   , "invariants" .= listValue (\i@Invariant{..} -> invariantJSON i _predicate) _invariants
@@ -396,6 +396,7 @@ instance ToJSON (Behaviour t) where
                                 , "name" .= _name
                                 , "contract" .= _contract
                                 , "interface" .= toJSON _interface
+                                , "pointers" .= toJSON _pointers
                                 , "preConditions" .= toJSON _preconditions
                                 , "case" .= toJSON _caseconditions
                                 , "postConditions" .= toJSON _postconditions
@@ -414,6 +415,10 @@ instance ToJSON Decl where
                                    , "abitype" .= toJSON abitype
                                    ]
 
+instance ToJSON Pointer where
+  toJSON (PointsTo _ x c) = object [ "kind" .= String "PointsTo"
+                                   , "var" .= x
+                                   , "contract" .= c ]
 
 invariantJSON :: ToJSON pred => Invariant t -> pred -> Value
 invariantJSON Invariant{..} predicate = object [ "kind" .= String "Invariant"
@@ -515,9 +520,6 @@ instance ToJSON (Exp a t) where
   toJSON (Create _ f xs) = object [ "symbol" .= pack "create"
                                   , "arity"  .= Data.Aeson.Types.Number 2
                                   , "args"   .= Array (fromList [object [ "fun" .=  String (pack f) ], toJSON xs]) ]
-  toJSON (AsContract _ addr c) = object [ "symbol" .= pack "as_contract"
-                                        , "arity"  .= Data.Aeson.Types.Number 2
-                                        , "args"   .= Array (fromList [toJSON addr, object [ "fun" .=  String (pack c) ]]) ]
 
   toJSON v = error $ "todo: json ast for: " <> show v
 
@@ -575,7 +577,6 @@ eval e = case e of
   ITE _ a b c   -> eval a >>= \cond -> if cond then eval b else eval c
 
   Create _ _ _ -> error "eval of contracts not supported"
-  AsContract _ _ _ -> error "eval of contracts not supported"
   _              -> empty
 
 intmin :: Int -> Integer