Add check for unserializable transition parameters (#412)

* Add check for unserializable transition parameters

* Fixed check of serializable types in message fields

src/lang/base/TypeChecker.ml

@@ -235,7 +235,7 @@ module ScillaTypechecker
  ~lopt:(Some (get_rep i)) in
  let t = rr_typ r in
  let rtp = t.tp in
- if is_storable_type rtp
+ if is_serializable_type rtp
  then pure @@ TypedSyntax.MVar (add_type_to_ident i t)
  else fail1 (sprintf "Cannot send values of type %s." (pp_typ rtp))
  (ER.get_loc (get_rep i)))
@@ -451,14 +451,16 @@ module ScillaTypechecker
  let type_transition env0 tr : (TypedSyntax.transition, scilla_error list) result =
  let {tname; tparams; tbody} = tr in
  let tenv0 = env0.pure in
- let lift_ident_e (id, t) = (add_type_to_id id (mk_qual_tp t), t) in
- let typed_tparams = List.map tparams ~f:lift_ident_e in
+ let msg = sprintf "Type error(s) in transition %s:\n" (get_id tname) in
+ wrap_with_info (msg, SR.get_loc (get_rep tname)) @@
+ let%bind typed_tparams = mapM ~f:(fun (param, t) ->
+ if is_serializable_type t
+ then pure (add_type_to_id param (mk_qual_tp t), t)
+ else fail1 (sprintf "Type %s cannot be used as transition parameter" (pp_typ t)) (ER.get_loc (get_rep param))) tparams in
  let append_params = CU.append_implict_trans_params tparams in
  let tenv1 = TEnv.addTs tenv0 append_params in
  let env = {env0 with pure = tenv1} in
- let msg = sprintf "Type error(s) in transition %s:\n" (get_id tname) in
- let%bind (typed_stmts, _) = wrap_with_info (msg, SR.get_loc (get_rep tname)) @@
- type_stmts env tbody ER.get_loc in
+ let%bind (typed_stmts, _) = type_stmts env tbody ER.get_loc in
  pure @@ ({ TypedSyntax.tname = tname ;
  TypedSyntax.tparams = typed_tparams;
  TypedSyntax.tbody = typed_stmts })

src/lang/base/TypeUtil.ml

@@ -277,6 +277,39 @@ module TypeUtilities
  not (t = PrimTypes.msg_typ || t = PrimTypes.event_typ) in
  storable_helper t []
 
+ let is_serializable_type t =
+ let rec serializable_helper t seen_adts =
+ match t with
+ | FunType _ 
+ | MapType _
+ | PolyFun _
+ | Unit -> false
+ | TypeVar _ ->
+ (* If we are inside an ADT, then type variable 
+ instantiations are handled outside *)
+ (match seen_adts with
+ | [] -> false 
+ | _ -> true)
+ | PrimType _ ->
+ (* Messages and Events are not serialisable in terms of contract parameters *)
+ not (t = PrimTypes.msg_typ || t = PrimTypes.event_typ)
+ | ADT (tname, ts) ->
+ (match List.findi ~f:(fun _ seen -> seen = tname) seen_adts with
+ | Some _ -> true (* Inductive ADT - ignore this branch *)
+ | None ->
+ (* Check that ADT is serializable *)
+ match DataTypeDictionary.lookup_name tname with
+ | Error _ -> false (* Handle errors outside *)
+ | Ok adt -> 
+ let adt_serializable =
+ List.for_all ~f:(fun (_, carg_list) ->
+ List.for_all ~f:(fun carg ->
+ serializable_helper carg (tname :: seen_adts))
+ carg_list)
+ adt.tmap in
+ adt_serializable && List.for_all ~f:(fun t -> serializable_helper t seen_adts) ts) in
+ serializable_helper t []
+
  let get_msgevnt_type m =
  if (List.exists ~f:(fun (s, _) -> s = ContractUtil.MessagePayload.tag_label) m)
  then pure PrimTypes.msg_typ else

src/lang/base/TypeUtil.mli

@@ -96,6 +96,7 @@ module TypeUtilities
  (****************************************************************)
 
  val is_storable_type : typ -> bool
+ val is_serializable_type : typ -> bool
  val is_ground_type : typ -> bool
  val get_msgevnt_type : (string * 'a) sexp_list -> (typ, scilla_error sexp_list) result
 

tests/checker/bad/TestCheckerFail.ml

@@ -49,6 +49,7 @@ module Tests = TestUtil.DiffBasedTests(
  "bad_adt_2.scilla";
  "bad_adt_3.scilla";
  "bad_adt_4.scilla";
+ "unserializable_param.scilla";
  "unstorable_adt.scilla";
  ]
  let exit_code : Unix.process_status = WEXITED 1

tests/checker/bad/gold/unserializable_param.scilla.gold

@@ -0,0 +1,50 @@
+{
+ "errors": [
+ {
+ "error_message": "Type error(s) in contract UnstorableADT:\n",
+ "start_location": {
+ "file": "checker/bad/unserializable_param.scilla",
+ "line": 15,
+ "column": 10
+ },
+ "end_location": { "file": "", "line": 0, "column": 0 }
+ },
+ {
+ "error_message": "Type error(s) in transition BadADTTrans:\n",
+ "start_location": {
+ "file": "checker/bad/unserializable_param.scilla",
+ "line": 19,
+ "column": 12
+ },
+ "end_location": { "file": "", "line": 0, "column": 0 }
+ },
+ {
+ "error_message": "Type Test cannot be used as transition parameter",
+ "start_location": {
+ "file": "checker/bad/unserializable_param.scilla",
+ "line": 19,
+ "column": 25
+ },
+ "end_location": { "file": "", "line": 0, "column": 0 }
+ },
+ {
+ "error_message": "Type error(s) in transition BadPrimTrans:\n",
+ "start_location": {
+ "file": "checker/bad/unserializable_param.scilla",
+ "line": 22,
+ "column": 12
+ },
+ "end_location": { "file": "", "line": 0, "column": 0 }
+ },
+ {
+ "error_message": "Type Message cannot be used as transition parameter",
+ "start_location": {
+ "file": "checker/bad/unserializable_param.scilla",
+ "line": 22,
+ "column": 26
+ },
+ "end_location": { "file": "", "line": 0, "column": 0 }
+ }
+ ],
+ "warnings": []
+}

tests/checker/bad/unserializable_param.scilla

@@ -0,0 +1,23 @@
+scilla_version 0
+
+(***************************************************)
+(* Associated library *)
+(***************************************************)
+
+library UnserializableADT
+
+type Test =
+ | Bad of (Uint32 -> Uint32)
+
+(***************************************************)
+(* The contract definition *)
+(***************************************************)
+contract UnstorableADT
+(
+)
+
+transition BadADTTrans (p : Test)
+end
+
+transition BadPrimTrans (p : Message)
+end