Nits in the typechecker and more tests

src/Act/Syntax.hs

@@ -324,6 +324,48 @@ itemType (Item t _ _) = actType t
 isMapping :: StorageLocation t -> Bool
 isMapping = not . null . ixsFromLocation
 
+posnFromExp :: Exp a t -> Pn
+posnFromExp e = case e of
+  And p _ _ -> p
+  Or p _ _ -> p
+  Impl p _ _ -> p
+  Neg p _ -> p
+  LT p _ _ -> p
+  LEQ p _ _ -> p
+  GEQ p _ _ -> p
+  GT p _ _ -> p
+  LitBool p _ -> p
+  -- integers
+  Add p _ _ -> p
+  Sub p _ _ -> p
+  Mul p _ _ -> p
+  Div p _ _ -> p
+  Mod p _ _ -> p
+  Exp p _ _ -> p
+  LitInt p _ -> p
+  IntEnv p _ -> p
+  -- bounds
+  IntMin p _ -> p
+  IntMax p _ -> p
+  UIntMin p _ -> p
+  UIntMax p _ -> p
+  InRange p _ _ -> p
+
+  -- bytestrings
+  Cat p _ _ -> p
+  Slice p _ _ _ -> p
+  ByStr p _ -> p
+  ByLit p _ -> p
+  ByEnv p _ -> p
+  -- contracts
+  Create p _ _ -> p
+
+  -- polymorphic
+  Eq  p _ _ _ -> p
+  NEq p _ _ _ -> p
+  ITE p _ _ _ -> p
+  TEntry p _ _ -> p
+  Var p _ _ _ _ -> p
 --------------------------------------
 -- * Extraction from untyped ASTs * --
 --------------------------------------

src/Act/Type.hs

@@ -489,7 +489,7 @@ andExps (c:cs) = foldl (\cs' c' -> And nowhere c' cs') c cs
 
 -- | Check the type of an expression and construct a typed expression
 checkExpr :: forall a t. Typeable t => Env -> SType a -> U.Expr -> Err (Exp a t)
-checkExpr env@Env{constructors} typ e = case (typ, e) of
+checkExpr env@Env{constructors, calldata} typ e = case (typ, e) of
   -- Boolean expressions
   (SBoolean, U.ENot    p v1)    -> Neg  p <$> checkExpr env SBoolean v1
   (SBoolean, U.EAnd    p v1 v2) -> And  p <$> checkExpr env SBoolean v1 <*> checkExpr env SBoolean v2
@@ -516,8 +516,8 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of
   (SInteger, U.ECreate p c args) -> case Map.lookup c constructors of
     Just ctrs ->
       let (typs, ptrs) = unzip ctrs in
-      checkIxs env p args (fmap PrimitiveType typs) `bindValidation` (\args ->
-      pure (Create p c args) <* traverse_ (\(e, t) -> checkContractType env e t) (zip args ptrs))
+      checkIxs env p args (fmap PrimitiveType typs) `bindValidation` (\args' ->
+      pure (Create p c args') <* traverse_ (\(e', t) -> checkContractType env e' t) (zip args' ptrs))
     Nothing -> throw (p, "Unknown constructor " <> show c)
 
    -- Control
@@ -537,16 +537,16 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of
     _             -> throw (p, "Unknown environment variable " <> show v1)
 
   -- Variable references
-  (_, U.EUTEntry entry) | isCalldataEntry env entry -> -- TODO more principled way of treating timings
+  (_, U.EUTEntry entry) | isCalldataEntry entry -> -- TODO more principled way of treating timings
      case (eqT @t @Timed, eqT @t @Untimed) of
        (Just Refl, _) -> validateVar env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
          Var (getPosEntry entry) Pre typ vt ref <$ checkEq (getPosEntry entry) typ typ'
        (_, Just Refl) -> validateVar env entry `bindValidation` \(vt@(FromVType typ'), ref) ->
          Var (getPosEntry entry) Neither typ vt ref <$ checkEq (getPosEntry entry) typ typ'
        (_,_) -> error "Internal error: Timing should be either Timed or Untimed"
        -- Var (getPosEntry entry) Neither typ vt ref <$ checkEq (getPosEntry entry) typ typ'
-  (_, U.EPreEntry entry) | isCalldataEntry env entry -> error "Not supported"
-  (_, U.EPostEntry entry) | isCalldataEntry env entry -> error "Not supported"
+  (_, U.EPreEntry entry) | isCalldataEntry entry -> error "Not supported"
+  (_, U.EPostEntry entry) | isCalldataEntry entry -> error "Not supported"
   -- 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')
@@ -576,11 +576,11 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of
       Nothing   -> throw (pn, (tail . show $ typeRep @t) <> " variable needed here.")
 
     -- TODO FIX
-    isCalldataEntry Env{calldata} (U.EVar _ name) = case Map.lookup name calldata of
+    isCalldataEntry (U.EVar _ name) = case Map.lookup name calldata of
       Just _  -> True
       _ -> False
-    isCalldataEntry env (U.EMapping _ entry _) = isCalldataEntry env entry
-    isCalldataEntry env (U.EField _ entry _) = isCalldataEntry env entry
+    isCalldataEntry (U.EMapping _ entry _) = isCalldataEntry entry
+    isCalldataEntry (U.EField _ entry _) = isCalldataEntry entry
 
 
 -- | Find the contract id of an expression with contract type
@@ -601,9 +601,9 @@ checkContractType :: Env -> TypedExp t -> Maybe Id -> Err ()
 checkContractType _ _ Nothing = pure ()
 checkContractType env (TExp _ e) (Just c) =
   findContractType env e `bindValidation` \oc ->
-  case oc of -- TODO fix position
-    Just c' -> assert (nowhere, "Expression was expected to have contract type " <> c <> " but has contract type " <> c') (c == c')
-    Nothing -> throw (nowhere, "Expression was expected to have contract type " <> c)
+  case oc of
+    Just c' -> assert (posnFromExp e, "Expression was expected to have contract type " <> c <> " but has contract type " <> c') (c == c')
+    Nothing -> throw (posnFromExp e, "Expression was expected to have contract type " <> c)
 
 checkEq :: forall a b. Pn -> SType a -> SType b -> Err ()
 checkEq p t1 t2 = maybe err (\Refl -> pure ()) $  testEquality t1 t2

tests/frontend/fail/cast.act

@@ -0,0 +1,43 @@
+constructor of A
+interface constructor(uint w1)
+
+iff
+    CALLVALUE == 0
+
+creates
+    uint w := w1
+
+constructor of B
+interface constructor(uint z1)
+
+iff
+    CALLVALUE == 0
+
+creates
+    uint z := z1
+
+constructor of C
+interface constructor(address a1, address a2)
+
+pointers
+  a1 |-> A
+  a2 |-> B
+
+iff
+    CALLVALUE == 0
+
+creates
+    A a := a1
+    B b := a2
+
+constructor of D
+interface constructor(address a1, address a2)
+
+pointers
+  a1 |-> A
+
+iff
+    CALLVALUE == 0    
+
+creates
+    C c1 := create C(a1, a2)

tests/hevm/pass/cast-5/cast-5.act

@@ -1,4 +1,13 @@
-constructor of C
+constructor of A
+interface constructor(uint w1)
+
+iff
+    CALLVALUE == 0
+
+creates
+    uint w := w1
+
+constructor of B
 interface constructor(uint z1)
 
 iff
@@ -7,28 +16,28 @@ iff
 creates
     uint z := z1
 
-constructor of A
-interface constructor(uint x1)
+constructor of C
+interface constructor(address a1, address a2)
 
+pointers
+  a1 |-> A
+  a2 |-> B
+
 iff
     CALLVALUE == 0
 
 creates
-    uint x := x1
-    C c := create C(42)
+    A a := a1
+    B b := a2
 
-
-constructor of B
-interface constructor(address x, address y)
+constructor of D
+interface constructor(address a1, address a2)
 
 pointers
-  x |-> A
-  y |-> A
+  a1 |-> A
 
 iff
-    CALLVALUE == 0
-    x =/= y
+    CALLVALUE == 0    
 
 creates
-    A a1 := x
-    C c := x.c
+    C c1 := create C(a1, a2)

tests/hevm/pass/cast-5/cast-5.sol

@@ -1,6 +1,6 @@
 pragma solidity >=0.8.0;
 
-contract C {
+contract A {
     uint z;
 
     constructor(uint z1) {
@@ -9,25 +9,28 @@ contract C {
 
 }
 
+contract B {
+    uint t;
 
-contract A {
-    uint x;
-    public C c;
-
-    constructor(uint x1) {
-	x = x1;
-	c = new C(42);
+    constructor(uint t1) {
+	t = t1;
     }
 }
 
+contract C {
+    A a;
+    B b;
 
-contract B {
-    A a1;
-    A a2;
+    constructor(address x, address y) {
+	a = A(x);
+	b = B(y);	
+    }
+}
 
+contract D {
+    C c2;
+
     constructor(address x, address y) {
-	require (x != y);
-	a1 = A(x);
-	a2 = a1.c();
+	c2 = new C(x,y);	
     }
 }

tests/hevm/pass/cast-6/cast-6.act

@@ -0,0 +1,40 @@
+constructor of C
+interface constructor(uint z1)
+
+iff
+    CALLVALUE == 0
+
+creates
+    uint z := z1
+
+constructor of A
+interface constructor(uint x1)
+
+iff
+    CALLVALUE == 0
+
+creates
+    uint x := x1
+    C c := create C(42)
+
+
+behaviour c of A
+interface c()
+
+iff
+    CALLVALUE == 0
+
+returns (pre(c))
+
+constructor of B
+interface constructor(address x)
+
+pointers
+  x |-> A
+
+iff
+    CALLVALUE == 0
+
+creates
+    A a := x
+    C c := x.c

tests/hevm/pass/cast-6/cast-6.sol

@@ -0,0 +1,32 @@
+pragma solidity >=0.8.0;
+
+contract C {
+    uint z;
+
+    constructor(uint z1) {
+	z = z1;
+    }
+
+}
+
+
+contract A {
+    uint x;
+    C public c;
+
+    constructor(uint x1) {
+	x = x1;
+	c = new C(42);
+    }
+}
+
+
+contract B {
+    A a;
+    C c;
+
+    constructor(address x) {
+	a = A(x);
+	c = a.c();
+    }
+}