Address type casts

src/base/Cashflow.ml

@@ -223,6 +223,8 @@ struct
                   (cf_init_tag_pattern p, List.map ~f:cf_init_tag_stmt ss))
                 pss )
       | ReadFromBC (x, s) -> CFSyntax.ReadFromBC (add_noinfo_to_ident x, s)
+      | TypeCast (x, r, t) ->
+          CFSyntax.TypeCast (add_noinfo_to_ident x, add_noinfo_to_ident r, t)
       | AcceptPayment -> CFSyntax.AcceptPayment
       | SendMsgs x -> CFSyntax.SendMsgs (add_noinfo_to_ident x)
       | CreateEvnt x -> CFSyntax.CreateEvnt (add_noinfo_to_ident x)
@@ -1850,6 +1852,22 @@ struct
             new_local_env,
             ctr_tag_map,
             not @@ [%equal: ECFR.money_tag] (get_id_tag x) x_tag )
+      | TypeCast (x, r, t) ->
+          let x_tag = lub_tags NotMoney (lookup_var_tag x local_env) in
+          let new_x = update_id_tag x x_tag in
+          let r_tag = lub_tags NotMoney (lookup_var_tag r local_env) in
+          let new_r = update_id_tag r r_tag in
+          let new_local_env =
+            AssocDictionary.remove (CFIdentifier.as_string x) local_env
+          in
+          ( TypeCast (new_x, new_r, t),
+            param_env,
+            field_env,
+            new_local_env,
+            ctr_tag_map,
+            not
+              ([%equal: ECFR.money_tag] (get_id_tag x) x_tag
+              || [%equal: ECFR.money_tag] (get_id_tag r) r_tag) )
       | AcceptPayment ->
           (AcceptPayment, param_env, field_env, local_env, ctr_tag_map, false)
       | GasStmt g ->

src/base/Disambiguate.ml

@@ -644,6 +644,14 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
               remove_local_id_from_dict var_dict_acc (as_string x)
             in
             pure @@ (PostDisSyntax.ReadFromBC (dis_x, f), new_var_dict)
+        | TypeCast (x, r, t) ->
+            let%bind dis_x = name_def_as_simple_global x in
+            let%bind dis_r = name_def_as_simple_global r in
+            let%bind dis_t = disambiguate_type dicts.typ_dict t in
+            let new_var_dict =
+              remove_local_id_from_dict var_dict_acc (as_string x)
+            in
+            pure @@ (PostDisSyntax.TypeCast (dis_x, dis_r, dis_t), new_var_dict)
         | AcceptPayment -> pure @@ (PostDisSyntax.AcceptPayment, var_dict_acc)
         | Iterate (l, proc) ->
             let%bind dis_l =

src/base/Gas.ml

@@ -49,6 +49,17 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
   open GasLiteral
   open GasSyntax
 
+  let address_typecheck_cost t =
+    let size =
+      match t with
+      | Address (Some fts) ->
+          (* look up _this_address and every listed field *)
+          1 + IdLoc_Comp.Map.length fts
+      | _ -> 0
+    in
+    let cost = 2 + size (* _balance and _nonce must also be looked up *) in
+    GasGasCharge.StaticCost cost
+
   (* The storage cost of a literal, based on it's size. *)
   let rec literal_cost lit =
     match lit with
@@ -189,6 +200,9 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
           | ReadFromBC _ | CallProc _ ->
               let g = GasStmt (GasGasCharge.StaticCost 1) in
               pure @@ [ (g, srep); (s, srep) ]
+          | TypeCast (_x, _r, t) ->
+              let g = address_typecheck_cost t in
+              pure @@ [ (GasStmt g, srep); (s, srep) ]
           | MapUpdate (_, klist, ropt) ->
               let n = GasGasCharge.StaticCost (List.length klist) in
               let g =

src/base/ParserUtil.ml

@@ -132,6 +132,8 @@ module type Syn = sig
     | MatchStmt of
         ParserRep.rep SIdentifier.t * (pattern * stmt_annot list) list
     | ReadFromBC of ParserRep.rep SIdentifier.t * string
+    | TypeCast of
+        ParserRep.rep SIdentifier.t * ParserRep.rep SIdentifier.t * SType.t
     | AcceptPayment
     (* forall l p *)
     | Iterate of ParserRep.rep SIdentifier.t * ParserRep.rep SIdentifier.t

src/base/PatternChecker.ml

@@ -268,6 +268,8 @@ struct
               pure @@ (CheckedPatternSyntax.MatchStmt (x, checked_clauses), rep)
           | ReadFromBC (i, s) ->
               pure @@ (CheckedPatternSyntax.ReadFromBC (i, s), rep)
+          | TypeCast (x, r, t) ->
+              pure @@ (CheckedPatternSyntax.TypeCast (x, r, t), rep)
           | AcceptPayment -> pure @@ (CheckedPatternSyntax.AcceptPayment, rep)
           | Iterate (l, p) -> pure @@ (CheckedPatternSyntax.Iterate (l, p), rep)
           | SendMsgs i -> pure @@ (CheckedPatternSyntax.SendMsgs i, rep)

src/base/Recursion.ml

@@ -205,6 +205,7 @@ module ScillaRecursion (SR : Rep) (ER : Rep) = struct
             in
             pure @@ RecursionSyntax.MatchStmt (x, new_pss)
         | ReadFromBC (x, f) -> pure @@ RecursionSyntax.ReadFromBC (x, f)
+        | TypeCast (x, r, t) -> pure @@ RecursionSyntax.TypeCast (x, r, t)
         | AcceptPayment -> pure @@ RecursionSyntax.AcceptPayment
         | Iterate (l, p) -> pure @@ RecursionSyntax.Iterate (l, p)
         | SendMsgs msg -> pure @@ RecursionSyntax.SendMsgs msg

src/base/SanityChecker.ml

@@ -346,7 +346,8 @@ struct
                 | RemoteLoad (x, _, _)
                 | MapGet (x, _, _, _)
                 | RemoteMapGet (x, _, _, _, _)
-                | ReadFromBC (x, _) ->
+                | ReadFromBC (x, _)
+                | TypeCast (x, _, _) ->
                     check_warn_redef cparams cfields pnames stmt_defs x;
                     pure (get_id x :: acc_stmt_defs)
                 | Store _ | MapUpdate _ | SendMsgs _ | AcceptPayment | GasStmt _

src/base/ScillaParser.mly

@@ -403,8 +403,8 @@ remote_fetch_stmt:
 | l = ID; FETCH; AND; EXISTS; adr = ID; PERIOD; r = ID; keys = nonempty_list(map_access)
   { RemoteMapGet(to_loc_id l (toLoc $startpos(l)), to_loc_id adr (toLoc $startpos(adr)), to_loc_id r (toLoc $startpos(r)), keys, false), toLoc $startpos }
 | (* Adding this production in preparation for address type casts *)
-  _l = ID; FETCH; AND; _adr = sident; AS; address_typ
-  { raise (SyntaxError ("Address type casts not yet supported", toLoc $startpos(_adr))) }
+  l = ID; FETCH; AND; adr = sident; AS; t = address_typ
+  { TypeCast(to_loc_id l (toLoc $startpos(l)), adr, t), toLoc $startpos }
 
 stmt_pm_clause:
 | BAR ; p = pattern ; ARROW ;

src/base/Syntax.ml

@@ -324,6 +324,7 @@ module ScillaSyntax (SR : Rep) (ER : Rep) (Literal : ScillaLiteral) = struct
         * bool
     | MatchStmt of ER.rep SIdentifier.t * (pattern * stmt_annot list) list
     | ReadFromBC of ER.rep SIdentifier.t * string
+    | TypeCast of ER.rep SIdentifier.t * ER.rep SIdentifier.t * SType.t
     | AcceptPayment
     (* forall l p *)
     | Iterate of ER.rep SIdentifier.t * SR.rep SIdentifier.t
@@ -589,6 +590,9 @@ module ScillaSyntax (SR : Rep) (ER : Rep) (Literal : ScillaLiteral) = struct
       | ReadFromBC (x, _) ->
           sprintf "Error in reading from blockchain state into `%s`:\n"
             (as_error_string x)
+      | TypeCast (_, x, t) ->
+          sprintf "Error casting `%s` into type `%s`:\n" (as_error_string x)
+            (SType.pp_typ_error t)
       | AcceptPayment -> sprintf "Error in accepting payment\n"
       | Iterate (l, p) ->
           sprintf "Error iterating `%s` over elements in list `%s`:\n"

src/base/TypeChecker.ml

@@ -817,6 +817,37 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct
             @@ add_stmt_to_stmts_env_gas
                  (TypedSyntax.ReadFromBC (typed_x, bf), rep)
                  checked_stmts
+        | TypeCast (x, r, t) ->
+            (* Only allow casts to address types *)
+            let%bind () =
+              fromR_TE
+              @@ assert_type_assignable
+                   ~lc:(ER.get_loc (get_rep r))
+                   ~expected:(address_typ None) ~actual:t
+            in
+            let%bind r_typ =
+              fromR_TE
+              @@ TEnv.resolveT env.pure (get_id r) ~lopt:(Some (get_rep r))
+            in
+            (* Only allow casts of types that could be an address type *)
+            let%bind () =
+              fromR_TE
+              @@ assert_type_assignable
+                   ~lc:(ER.get_loc (get_rep r))
+                   ~expected:(bystrx_typ Type.address_length)
+                   ~actual:(rr_typ r_typ).tp
+            in
+            let res_typ = mk_qual_tp (option_typ t) in
+            let typed_x = add_type_to_ident x res_typ in
+            let typed_r = add_type_to_ident r (rr_typ r_typ) in
+            let%bind checked_stmts =
+              with_extended_env env get_tenv_pure [ (x, res_typ.tp) ] []
+                (type_stmts sts get_loc)
+            in
+            pure
+            @@ add_stmt_to_stmts_env_gas
+                 (TypedSyntax.TypeCast (typed_x, typed_r, t), rep)
+                 checked_stmts
         | MatchStmt (x, clauses) ->
             if List.is_empty clauses then
               fail

src/base/TypeInfo.ml

@@ -126,6 +126,7 @@ struct
             in
             ots :: List.concat clausets
         | ReadFromBC (v, _) | SendMsgs v | CreateEvnt v -> [ calc_ident_locs v ]
+        | TypeCast (v, r, _) -> [ calc_ident_locs v; calc_ident_locs r ]
         | AcceptPayment | GasStmt _ -> []
         | CallProc (_, il) -> List.map il ~f:calc_ident_locs
         | Iterate (l, _) -> [ calc_ident_locs l ]

src/eval/Eval.ml

@@ -419,6 +419,21 @@ let rec stmt_eval conf stmts =
           let%bind l = Configuration.bc_lookup conf bf in
           let conf' = Configuration.bind conf (get_id x) l in
           stmt_eval conf' sts
+      | TypeCast (x, r, t) ->
+          let%bind l = fromR @@ Configuration.lookup conf r in
+          let%bind l_as_bstr =
+            match l with
+            | ByStrX lbystr when Bystrx.width lbystr = Type.address_length ->
+                pure lbystr
+            | _ -> fail0 "Expected address or ByStr20 in type cast"
+          in
+          let%bind tc_res =
+            fromR
+            @@ EvalTypecheck.typecheck_remote_field_types ~caddr:l_as_bstr t
+          in
+          let res = if tc_res then build_some_lit l t else build_none_lit t in
+          let conf' = Configuration.bind conf (get_id x) res in
+          stmt_eval conf' sts
       | MatchStmt (x, clauses) ->
           let%bind v = fromR @@ Env.lookup conf.env x in
           let%bind (_, branch_stmts), bnds =

src/eval/EvalUtil.ml

@@ -525,36 +525,81 @@ module EvalTypecheck = struct
         pure true
     | _ -> pure false
 
-  let typecheck_remote_field_types ~caddr fts_opt =
-    let open EvalType in
+  let is_address_in_use ~caddr =
+    (* True if the address is in use, false otherwise *)
+    let%bind user_addr = is_user_addr ~caddr in
+    if not user_addr then
+      let%bind contract_addr = is_contract_addr ~caddr in
+      pure contract_addr
+    else pure true
+
+  let typecheck_remote_fields ~caddr fts =
+    (* Check that all fields are defined at caddr, and that their types are assignable to what is expected *)
+    allM fts ~f:(fun (f, t) ->
+        let%bind res =
+          StateService.external_fetch ~caddr ~fname:f ~keys:[] ~ignoreval:true
+        in
+        match res with
+        | _, Some ext_typ ->
+            pure @@ EvalType.type_assignable ~expected:t ~actual:ext_typ
+        | _, None -> pure false)
+
+  type evalTCResult =
+    | AddressNotInUse
+    | NoContractAtAddress
+    | FieldTypeMismatch
+    | Success
+
+  let typecheck_fts ~caddr fts_opt =
     match fts_opt with
     | None ->
-        (* True if the address is in use, false otherwise *)
-        let%bind user_addr = is_user_addr ~caddr in
-        if not user_addr then
-          let%bind contract_addr = is_contract_addr ~caddr in
-          if not contract_addr then
-            fail0
-            @@ sprintf "Address %s not in use."
-                 (EvalLiteral.Bystrx.hex_encoding caddr)
-          else pure true
-        else pure true
+        let%bind in_use = is_address_in_use ~caddr in
+        if not in_use then pure AddressNotInUse else pure Success
     | Some fts ->
         (* True if the address contains a contract with the appropriate fields, false otherwise *)
         let%bind contract_addr = is_contract_addr ~caddr in
-        if not contract_addr then
-          fail0
-          @@ sprintf "No contract found at address %s"
-               (EvalLiteral.Bystrx.hex_encoding caddr)
+        if not contract_addr then pure NoContractAtAddress
         else
-          (* Check that all fields are defined at caddr, and that their types are assignable to what is expected *)
-          allM fts ~f:(fun (f, t) ->
-              let%bind res =
-                StateService.external_fetch ~caddr ~fname:f ~keys:[]
-                  ~ignoreval:true
-              in
-              match res with
-              | _, Some ext_typ ->
-                  pure @@ type_assignable ~expected:t ~actual:ext_typ
-              | _, None -> pure false)
+          let%bind fts_ok = typecheck_remote_fields ~caddr fts in
+          if not fts_ok then pure FieldTypeMismatch else pure Success
+
+  let get_fts_opt_from_address t =
+    let open EvalType in
+    match t with
+    | Address fts_opt -> pure fts_opt
+    | _ ->
+        fail0
+        @@ sprintf "Unable to perform dynamic typecheck on type %s\n" (pp_typ t)
+
+  let assert_typecheck_remote_field_types ~caddr t =
+    let open EvalType in
+    let%bind fts_opt = get_fts_opt_from_address t in
+    let%bind tc_res =
+      typecheck_fts ~caddr (Option.map ~f:IdLoc_Comp.Map.to_alist fts_opt)
+    in
+    match tc_res with
+    | AddressNotInUse ->
+        fail0
+        @@ sprintf "Address %s not in use."
+             (EvalLiteral.Bystrx.hex_encoding caddr)
+    | NoContractAtAddress ->
+        fail0
+        @@ sprintf "No contract found at address %s"
+             (EvalLiteral.Bystrx.hex_encoding caddr)
+    | FieldTypeMismatch ->
+        fail0
+        @@ sprintf "Address %s does not satisfy type %s\n"
+             (EvalLiteral.Bystrx.hex_encoding caddr)
+             (pp_typ t)
+    | Success -> pure ()
+
+  let typecheck_remote_field_types ~caddr t =
+    let open EvalType in
+    let%bind fts_opt = get_fts_opt_from_address t in
+    let%bind tc_res =
+      typecheck_fts ~caddr (Option.map ~f:IdLoc_Comp.Map.to_alist fts_opt)
+    in
+    match tc_res with
+    | AddressNotInUse | NoContractAtAddress | FieldTypeMismatch -> pure false
+    | Success -> pure true
 end