diff --git a/src/base/BuiltIns.ml b/src/base/BuiltIns.ml index 2c1d23293..796ec2cc1 100644 --- a/src/base/BuiltIns.ml +++ b/src/base/BuiltIns.ml @@ -1129,7 +1129,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct let contains_elab sc ts = match ts with - | [ MapType (kt, vt); u ] when type_equiv kt u -> + | [ MapType (kt, vt); u ] when type_assignable kt u -> elab_tfun_with_args_no_gas sc [ kt; vt ] | _ -> fail0 "Failed to elaborate" @@ -1151,7 +1151,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct let put_elab sc ts = match ts with | [ MapType (kt, vt); kt'; vt' ] - when type_equiv kt kt' && type_equiv vt vt' -> + when type_assignable kt kt' && type_assignable vt vt' -> elab_tfun_with_args_no_gas sc [ kt; vt ] | _ -> fail0 "Failed to elaborate" @@ -1174,7 +1174,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct let get_elab sc ts = match ts with - | [ MapType (kt, vt); kt' ] when type_equiv kt kt' -> + | [ MapType (kt, vt); kt' ] when type_assignable kt kt' -> elab_tfun_with_args_no_gas sc [ kt; vt ] | _ -> fail0 "Failed to elaborate" @@ -1196,7 +1196,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct let remove_elab sc ts = match ts with - | [ MapType (kt, vt); u ] when type_equiv kt u -> + | [ MapType (kt, vt); u ] when type_assignable kt u -> elab_tfun_with_args_no_gas sc [ kt; vt ] | _ -> fail0 "Failed to elaborate" diff --git a/src/base/Gas.ml b/src/base/Gas.ml index 3fc42abf2..be299c3a6 100644 --- a/src/base/Gas.ml +++ b/src/base/Gas.ml @@ -365,11 +365,11 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct && List.for_all2_exn ~f:(fun t1 t2 -> (* the types should match *) - type_equiv t1 t2 + type_assignable t1 t2 || (* or the built-in record is generic *) - match t2 with TypeVar _ -> true | _ -> false) - arg_types types + match t1 with TypeVar _ -> true | _ -> false) + types arg_types then fcoster op arg_literals base (* this can fail too *) else fail0 @@ "Name or arity doesn't match" in diff --git a/src/base/JSON.ml b/src/base/JSON.ml index 994ba11e3..2a03dbb3f 100644 --- a/src/base/JSON.ml +++ b/src/base/JSON.ml @@ -82,12 +82,22 @@ let build_prim_lit_exn t v = let exn () = mk_invalid_json ("Invalid " ^ pp_typ t ^ " value " ^ v ^ " in JSON") in + let build_prim_literal_of_type t v = + match build_prim_literal t v with + | Some v' -> v' + | None -> raise (exn ()) + in match t with - | PrimType pt -> ( - match build_prim_literal pt v with - | Some v' -> v' - | None -> raise (exn ()) ) - | _ -> raise (exn ()) + | PrimType pt -> + build_prim_literal_of_type pt v + | Address _ -> + build_prim_literal_of_type (Bystrx_typ 20) v + | MapType _ + | FunType _ + | ADT _ + | TypeVar _ + | PolyFun _ + | Unit -> raise (exn ()) (****************************************************************) (* JSON parsing *) @@ -123,7 +133,7 @@ let rec json_to_adtargs cname tlist ajs = JSONParser.constr_pattern_arg_types_exn (ADT (asId dt.tname, tlist)) cname in verify_args_exn cname (List.length ajs) (List.length tmap); - let llist = List.map2_exn tmap ajs ~f:(fun t j -> json_to_lit t j) in + let llist = List.map2_exn tmap ajs ~f:(fun t j -> json_to_lit_exn t j) in ADTValue (cname, tlist, llist) and read_adt_json name j tlist_verify = @@ -144,7 +154,7 @@ and read_adt_json name j tlist_verify = let etyp = List.nth_exn tlist_verify 0 in List.fold_right vli ~f:(fun vl acc -> - ADTValue ("Cons", [ etyp ], [ json_to_lit etyp vl; acc ])) + ADTValue ("Cons", [ etyp ], [ json_to_lit_exn etyp vl; acc ])) ~init:(ADTValue ("Nil", [ etyp ], [])) | `Assoc _ -> let constr = member_exn "constructor" j |> to_string_exn in @@ -167,7 +177,7 @@ and read_adt_json name j tlist_verify = let verify_exn name tlist1 adt = match adt with | ADTValue (_, tlist2, _) -> - if type_equiv_list tlist1 tlist2 then () + if type_assignable_list tlist1 tlist2 then () else let expected = pp_typ_list tlist1 in let observed = pp_typ_list tlist2 in @@ -202,10 +212,10 @@ and mapvalues_from_json m kt vt l = | _ -> raise (mk_invalid_json "Key in Map JSON is not a PrimType") in let vjson = member_exn "val" first in - let vallit = json_to_lit vt vjson in + let vallit = json_to_lit_exn vt vjson in Caml.Hashtbl.replace m keylit vallit) -and json_to_lit t v = +and json_to_lit_exn t v = match t with | MapType (kt, vt) -> let vl = read_map_json kt vt v in @@ -213,17 +223,27 @@ and json_to_lit t v = | ADT (name, tlist) -> let vl = read_adt_json (get_id name) v tlist in vl - | _ -> + | PrimType _ + | Address _ -> let tv = build_prim_lit_exn t (to_string_exn v) in tv - + | FunType _ + | TypeVar _ + | PolyFun _ + | Unit -> + let exn () = + mk_invalid_json ("Invalid type " ^ pp_typ t ^ " in JSON") + in + raise (exn ()) + + let jobj_to_statevar json = let n = member_exn "vname" json |> to_string_exn in let tstring = member_exn "type" json |> to_string_exn in let t = parse_typ_exn tstring in let v = member_exn "value" json in if GlobalConfig.validate_json () (* TODO: Add command line flag. *) then - (n, json_to_lit t v) + (n, json_to_lit_exn t v) else (n, JSONParser.parse_json t v) (****************************************************************) @@ -324,7 +344,7 @@ module ContractState = struct let jstring_to_literal jstring tp = let thunk () = Yojson.Basic.from_string jstring in let jobj = json_exn_wrapper ~filename:"ipc_fetch" thunk in - json_to_lit tp jobj + json_to_lit_exn tp jobj end module Message = struct diff --git a/src/base/ParserFaults.messages b/src/base/ParserFaults.messages index 76d4958ce..1997b2c7f 100644 --- a/src/base/ParserFaults.messages +++ b/src/base/ParserFaults.messages @@ -112,20 +112,6 @@ type_term: CID UNDERSCORE This is an invalid type term, it may be a bad ADT. -type_term: CID WITH -## -## Ends in an error in state: 22. -## -## scid -> CID . [ UNDERSCORE TYPE TRANSITION TID TARROW SEMICOLON RPAREN RBRACE PROCEDURE MAP LPAREN LET IN ID FIELD EQ EOF END CONTRACT COMMA CID BAR ARROW ] -## scid -> CID . PERIOD CID [ UNDERSCORE TYPE TRANSITION TID TARROW SEMICOLON RPAREN RBRACE PROCEDURE MAP LPAREN LET IN ID FIELD EQ EOF END CONTRACT COMMA CID BAR ARROW ] -## -## The known suffix of the stack is as follows: -## CID -## -# see tests/parser/bad/type_t-cid-with.scilla - -This is an invalid type term, the ADT constructor arguments are likely incorrect. This necessitates a proper separated capital identifier, type identifier, type in brackets or a map. - type_term: FORALL TID PERIOD TID WITH ## ## Ends in an error in state: 61. @@ -534,7 +520,7 @@ This function is not terminated early enough or malformed. A possible alteration type_term: TID TARROW WITH ## -## Ends in an error in state: 62. +## Ends in an error in state: ?. ## ## typ -> typ TARROW . typ [ TARROW RPAREN EQ EOF COMMA ] ## @@ -545,19 +531,34 @@ type_term: TID TARROW WITH This function type lacks a result type. +type_term: CID WITH EOF +## +## Ends in an error in state: 62. +## +## +## +## The known suffix of the stack is as follows: +## +## +# see tests/parser/bad/type_t-tid-arrow-with.scilla + +Invalid or incomplete type. + type_term: TID WITH ## -## Ends in an error in state: 312. +## Ends in an error in state: 317. ## ## typ -> typ . TARROW typ [ TARROW EOF ] ## type_term -> typ . EOF [ # ] -## +## scid -> CID . [ UNDERSCORE TYPE TRANSITION TID TARROW SEMICOLON RPAREN RBRACE PROCEDURE MAP LPAREN LET IN ID FIELD EQ EOF END CONTRACT COMMA CID BAR ARROW ] +## scid -> CID . PERIOD CID [ UNDERSCORE TYPE TRANSITION TID TARROW SEMICOLON RPAREN RBRACE PROCEDURE MAP LPAREN LET IN ID FIELD EQ EOF END CONTRACT COMMA CID BAR AR## ## The known suffix of the stack is as follows: ## typ +## CID ## # special case, only by type_term entry point should never happen -This is an invalid type term, following the type it is complete and may only be extended by an arrow. +This is an invalid type term, the ADT constructor arguments are likely incorrect. This necessitates a proper separated capital identifier, type identifier, type in brackets, or a map. type_term: WITH ## @@ -1596,35 +1597,24 @@ This type annotation is not closed properly, or has a missing or misplaced '='. exp_term: FUN LPAREN ID COLON WITH ## -## Ends in an error in state: 61. +## Ends in an error in state: 64. ## ## simple_exp -> FUN LPAREN ID COLON . typ RPAREN ARROW exp [ TYPE TRANSITION SEMICOLON PROCEDURE LET IN FIELD EOF END CONTRACT BAR ARROW ] ## type_annot -> COLON . typ [ EQ ] ## param_pair -> ID COLON . typ [ RPAREN COMMA ] ## field -> FIELD ID COLON . typ EQ exp [ TRANSITION PROCEDURE FIELD EOF ] +## type_annot -> COLON . typ [ EQ ] ## ## The known suffix of the stack is as follows: ## FUN LPAREN ID COLON ## LET ID COLON WITH ## SCILLA_VERSION NUMLIT CONTRACT CID LPAREN ID COLON WITH ## SCILLA_VERSION NUMLIT CONTRACT CID LPAREN RPAREN FIELD ID COLON WITH -## -# see tests/parser/bad/exps/exp_t-fun-lparen-id-colon-with.scilexp - -Missing or invalid type in type annotation. - -cmodule: SCILLA_VERSION NUMLIT CONTRACT CID LPAREN ID COLON ID RPAREN -## -## Ends in an error in state: 58. -## -## type_annot -> COLON . typ [ EQ ] -## -## The known suffix of the stack is as follows: ## SCILLA_VERSION NUMLIT CONTRACT CID LPAREN RPAREN FIELD ID COLON WITH ## # see tests/parser/bad/exps/exp_t-fun-lparen-id-colon-with.scilexp -Invalid type in type annotation. +Missing or invalid type in type annotation. exp_term: FUN LPAREN ID WITH ## diff --git a/src/base/Recursion.ml b/src/base/Recursion.ml index 964f5e516..1efcf3219 100644 --- a/src/base/Recursion.ml +++ b/src/base/Recursion.ml @@ -56,7 +56,17 @@ module ScillaRecursion (SR : Rep) (ER : Rep) = struct forallM ~f:walk targs | PolyFun (_, t) -> walk t | Address fts -> - forallM fts ~f:(fun (_, t) -> walk t) + match List.find_a_dup fts + ~compare:(fun (f1, _) (f2, _) -> + Bytes.compare + (Bytes.of_string (get_id f1)) + (Bytes.of_string (get_id f2))) with + | Some (dup_field, _) -> + fail1 + (sprintf "Duplicate field %s in address type." (get_id dup_field)) + (get_rep dup_field) + | None -> + forallM fts ~f:(fun (_, t) -> walk t) in walk t diff --git a/src/base/ScillaParser.mly b/src/base/ScillaParser.mly index 91d5726ec..ed6edb4d7 100644 --- a/src/base/ScillaParser.mly +++ b/src/base/ScillaParser.mly @@ -204,7 +204,7 @@ typ : | MAP; k=t_map_key; v = t_map_value; { MapType (k, v) } | t1 = typ; TARROW; t2 = typ; { FunType (t1, t2) } | LPAREN; t = typ; RPAREN; { t } -| d = ID; WITH; fs = separated_list(COMMA, address_field_type); END; +| d = CID; WITH; fs = separated_list(COMMA, address_field_type); END; { if d = "ByStr20" then Address fs else raise (SyntaxError ("Invalid primitive type", toLoc $startpos(d))) } diff --git a/src/base/Syntax.ml b/src/base/Syntax.ml index ba56a1ea4..0adfd64f2 100644 --- a/src/base/Syntax.ml +++ b/src/base/Syntax.ml @@ -130,7 +130,7 @@ let rec pp_typ = function let elems = List.map fts ~f:(fun (f, t) -> sprintf "%s : %s" (get_id f) (pp_typ t)) |> String.concat ~sep:", " in - sprintf "ByStr20 with %s end" elems + sprintf "ByStr20 with %s%send" elems (if List.is_empty fts then "" else " ") and with_paren t = match t with @@ -536,29 +536,80 @@ let canonicalize_tfun t = let mk_new_name counter _ = "'_A" ^ Int.to_string counter in rename_bound_vars mk_new_name (const @@ Int.succ) t 1 +(* Type equality - assumes that the types have been canonicalised first. *) +let rec type_equal t1 t2 = + match t1, t2 with + | PrimType p1, PrimType p2 -> p1 = p2 + | TypeVar v1, TypeVar v2 -> String.equal v1 v2 + | Unit, Unit -> true + | ADT (tname1, tl1), ADT (tname2, tl2) -> + equal_id tname1 tname2 + (* Cannot call type_equiv_list because we don't want to canonicalize_tfun again. *) + && List.length tl1 = List.length tl2 + && List.for_all2_exn ~f:type_equal tl1 tl2 + | MapType (t1_1, t1_2), MapType (t2_1, t2_2) + | FunType (t1_1, t1_2), FunType (t2_1, t2_2) -> + type_equal t1_1 t2_1 && type_equal t1_2 t2_2 + | PolyFun (v1, t1''), PolyFun (v2, t2'') -> + String.equal v1 v2 && type_equal t1'' t2'' + | Address fts1, Address fts2 -> + let traverse fts_first fts_second = + List.for_all fts_first ~f:(fun (f1, t1) -> + let f1_id = get_id f1 in + match List.find fts_second ~f:(fun (f2, _) -> String.(f1_id = get_id f2)) with + | None -> false + | Some (_, t2) -> type_equal t1 t2) + in + List.length fts1 = List.length fts2 + && traverse fts1 fts2 + && traverse fts2 fts1 + | _ -> false + (* Type equivalence *) let type_equiv t1 t2 = let t1' = canonicalize_tfun t1 in let t2' = canonicalize_tfun t2 in - let rec equiv t1 t2 = - match (t1, t2) with - | PrimType p1, PrimType p2 -> p1 = p2 - | TypeVar v1, TypeVar v2 -> String.equal v1 v2 - | Unit, Unit -> true + type_equal t1' t2' + +let type_assignable to_typ from_typ = + let to_typ' = canonicalize_tfun to_typ in + let from_typ' = canonicalize_tfun from_typ in + let rec assignable to_typ from_typ = + match to_typ, from_typ with + | Address tfts, Address ffts -> + (* Check that tfts is a subset of ffts, and that types are assignable/equivalent. *) + List.for_all tfts ~f:(fun (tf, tft) -> + let tf_name = get_id tf in + match List.find ffts ~f:(fun (ff, _) -> + String.(tf_name = get_id ff)) with + | None -> + (* to field does not appear in from type *) + false + | Some (_, fft) -> + (* Matching field name. Types must be assignable. *) + assignable tft fft) + | PrimType (Bystrx_typ len), Address _ + when len = address_length -> + (* Any address is assignable to ByStr20. *) + true | ADT (tname1, tl1), ADT (tname2, tl2) -> equal_id tname1 tname2 - (* Cannot call type_equiv_list because we don't want to canonicalize_tfun again. *) && List.length tl1 = List.length tl2 - && List.for_all2_exn ~f:equiv tl1 tl2 - | MapType (t1_1, t1_2), MapType (t2_1, t2_2) + (* Instantiation types must be assignable *) + && List.for_all2_exn ~f:assignable tl1 tl2 + | MapType (t1_1, t1_2), MapType (t2_1, t2_2) -> + assignable t1_1 t2_1 && assignable t1_2 t2_2 | FunType (t1_1, t1_2), FunType (t2_1, t2_2) -> - equiv t1_1 t2_1 && equiv t1_2 t2_2 + (* Must be contravariant in the argument type *) + assignable t2_1 t1_1 && assignable t1_2 t2_2 | PolyFun (v1, t1''), PolyFun (v2, t2'') -> - String.equal v1 v2 && equiv t1'' t2'' - | _ -> false + String.equal v1 v2 && assignable t1'' t2'' + | _, _ -> + (* All other cases require equality up to canonicalisation. *) + type_equal to_typ from_typ in - equiv t1' t2' - + assignable to_typ' from_typ' + (* The same as above, but for a variable with locations *) let subst_type_in_type' tv = subst_type_in_type (get_id tv) diff --git a/src/base/TypeChecker.ml b/src/base/TypeChecker.ml index 34881fd11..d41afa5bd 100644 --- a/src/base/TypeChecker.ml +++ b/src/base/TypeChecker.ml @@ -229,15 +229,17 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct let%bind ((_, (ityp, _)) as checked_lhs), remaining_gas = wrap_type_err erep @@ type_expr tenv lhs remaining_gas in - let%bind () = + let%bind actual_typ = match topt with | Some tannot -> mark_error_as_type_error remaining_gas - @@ assert_type_equiv tannot ityp.tp - | None -> pure () + @@ + let%bind _ = assert_type_assignable tannot ityp.tp in + pure (mk_qual_tp tannot) + | None -> pure ityp in - let tenv' = TEnv.addT (TEnv.copy tenv) i ityp.tp in - let typed_i = add_type_to_ident i ityp in + let tenv' = TEnv.addT (TEnv.copy tenv) i actual_typ.tp in + let typed_i = add_type_to_ident i actual_typ in let%bind ((_, (rhstyp, _)) as checked_rhs), remaining_gas = type_expr tenv' rhs remaining_gas in @@ -320,7 +322,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct type_expr tenv' body remaining_gas in let%bind _ = - mark_error_as_type_error remaining_gas @@ assert_type_equiv t bt.tp + mark_error_as_type_error remaining_gas @@ assert_type_assignable t bt.tp in pure @@ ( ( TypedSyntax.Fixpoint @@ -366,7 +368,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct let payload_type fld pld remaining_gas = let check_field_type seen_type = match Caml.List.assoc_opt fld CU.msg_mandatory_field_types with - | Some fld_t when fld_t <> seen_type -> + | Some fld_t when not @@ type_assignable fld_t seen_type -> fail1 (sprintf "Type mismatch for Message field %s. Expected %s but got \ @@ -489,7 +491,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct let%bind k_t = TEnv.resolveT env.pure (get_id k) ~lopt:(Some (get_rep k)) in - let%bind _ = assert_type_equiv kt (rr_typ k_t).tp in + let%bind _ = assert_type_assignable kt (rr_typ k_t).tp in let%bind typed_keys, res = helper vt rest in let typed_k = add_type_to_ident k (rr_typ k_t) in pure @@ (typed_k :: typed_keys, res) @@ -562,7 +564,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct in let%bind _ = mark_error_as_type_error remaining_gas - @@ assert_type_equiv (rr_typ fr).tp (rr_typ r).tp + @@ assert_type_assignable (rr_typ fr).tp (rr_typ r).tp in let%bind checked_stmts, remaining_gas = type_stmts env sts get_loc remaining_gas @@ -607,7 +609,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct let typed_v = rr_typ v_resolv in let%bind _ = mark_error_as_type_error remaining_gas - @@ assert_type_equiv v_type typed_v.tp + @@ assert_type_assignable v_type typed_v.tp in let typed_v' = add_type_to_ident v typed_v in pure @@ Some typed_v' @@ -726,7 +728,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct let%bind _ = wrap_type_serr stmt @@ mark_error_as_type_error remaining_gas - @@ assert_type_equiv expected i_type.tp + @@ assert_type_assignable expected i_type.tp in let typed_i = add_type_to_ident i i_type in let%bind checked_stmts, remaining_gas = @@ -746,7 +748,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct let%bind _ = wrap_type_serr stmt @@ mark_error_as_type_error remaining_gas - @@ assert_type_equiv event_typ i_type.tp + @@ assert_type_assignable event_typ i_type.tp in let typed_i = add_type_to_ident i i_type in let%bind checked_stmts, remaining_gas = @@ -802,7 +804,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct let%bind _ = wrap_type_serr stmt @@ mark_error_as_type_error remaining_gas - @@ assert_type_equiv exception_typ i_type.tp + @@ assert_type_assignable exception_typ i_type.tp in let typed_i = add_type_to_ident i i_type in pure @@ -843,8 +845,8 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct @@ let param_checker = match comp_type with - | CompTrans -> is_legal_parameter_type - | CompProc -> is_non_map_ground_type + | CompTrans -> is_legal_transition_parameter_type + | CompProc -> is_legal_procedure_parameter_type in let%bind typed_cparams = mark_error_as_type_error remaining_gas @@ -898,7 +900,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct let actual = ar.tp in let%bind _ = mark_error_as_type_error remaining_gas' - @@ assert_type_equiv ft actual + @@ assert_type_assignable ft actual in let typed_fs = add_type_to_ident fn ar in if is_legal_field_type ft then @@ -950,7 +952,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct match topt with | Some tannot -> mark_error_as_type_error remaining_gas' - @@ assert_type_equiv tannot ar.tp + @@ assert_type_assignable tannot ar.tp | None -> pure () in let typed_rn = add_type_to_ident rn ar in @@ -1014,7 +1016,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct match ltopt with | Some tannot -> mark_error_as_type_error remaining_gas - @@ assert_type_equiv tannot tr.tp + @@ assert_type_assignable tannot tr.tp | None -> pure () in let typed_ln = add_type_to_ident ln tr in @@ -1249,7 +1251,7 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct in let%bind _ = mark_error_as_type_error remaining_gas - @@ assert_type_equiv (ADT (asId "Bool", [])) ityp.tp + @@ assert_type_assignable (ADT (asId "Bool", [])) ityp.tp in pure (checked_constraint, remaining_gas) in diff --git a/src/base/TypeUtil.ml b/src/base/TypeUtil.ml index cf0a4cbf2..181b059b1 100644 --- a/src/base/TypeUtil.ml +++ b/src/base/TypeUtil.ml @@ -205,7 +205,19 @@ functor (pp_typ t) ) | PolyFun (arg, bt) -> is_wf_typ' bt (arg :: tb) | Address fts -> - foldM fts ~init:() ~f:(fun _ (_, t) -> is_wf_typ' t tb) + match List.find_a_dup fts + ~compare:(fun (f1, _) (f2, _) -> + Bytes.compare + (Bytes.of_string (get_id f1)) + (Bytes.of_string (get_id f2))) with + | Some (dup_f, _) -> + (* No duplicate fields allowed *) + fail1 + (sprintf "Duplicate field %s in address type" (get_id dup_f)) + (get_rep dup_f) + | None -> + (* Check all types of address fields *) + foldM fts ~init:() ~f:(fun _ (_, t) -> is_wf_typ' t tb) in is_wf_typ' t [] @@ -292,9 +304,22 @@ module TypeUtilities = struct if type_equiv expected given then pure () else fail0 - @@ sprintf "Type mismatch: %s expected, but %s provided." + @@ sprintf "Types not equivalent: %s expected, but %s provided." (pp_typ expected) (pp_typ given) + let type_assignable_list tlist1 tlist2 = + List.length tlist1 = List.length tlist2 + && not + (List.exists2_exn tlist1 tlist2 ~f:(fun t1 t2 -> + not (type_assignable t1 t2))) + + let assert_type_assignable expected given = + if type_assignable expected given then pure () + else + fail0 + @@ sprintf "Type unassignable: %s expected, but %s provided." + (pp_typ expected) (pp_typ given) + (* TODO: make this charge gas *) let assert_type_equiv_with_gas expected given remaining_gas = if type_equiv expected given then pure remaining_gas @@ -312,79 +337,88 @@ module TypeUtilities = struct | MapType (k, v) -> is_ground_type k && is_ground_type v | ADT (_, ts) -> List.for_all ~f:(fun t -> is_ground_type t) ts | PolyFun _ | TypeVar _ -> false - | _ -> true - - let rec is_non_map_ground_type t = - match t with - | FunType (a, r) -> is_non_map_ground_type a && is_non_map_ground_type r - | MapType (_, _) -> false - | ADT (_, ts) -> List.for_all ~f:(fun t -> is_non_map_ground_type t) ts - | PolyFun _ | TypeVar _ -> false - | _ -> true - - let rec is_serializable_storable_helper accept_maps check_addresses t seen_adts = - match t with - | FunType _ | PolyFun _ | Unit -> false - | MapType (kt, vt) -> - if accept_maps then - is_serializable_storable_helper accept_maps check_addresses kt seen_adts - && is_serializable_storable_helper accept_maps check_addresses vt seen_adts - else 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 ~sloc:(get_rep tname) - (get_id 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 -> - is_serializable_storable_helper accept_maps check_addresses carg - (tname :: seen_adts)) - carg_list) - adt.tmap - in - adt_serializable - && List.for_all - ~f:(fun t -> - is_serializable_storable_helper accept_maps check_addresses t seen_adts) - ts ) ) - | Address fts - when check_addresses -> - (* If check_addresses is true, then all field types in the address type should be legal field types. *) - List.for_all fts ~f:(fun (_, t) -> is_legal_field_type t) | Address _ -> - (* If check_addresses is false, then consider Address = ByStr20. *) - true + (* Addresses are represented as ByStr20 *) + true + | _ -> true + + let rec is_serializable_storable_helper accept_maps allow_unserializable check_addresses t seen_adts = + let rec recurser t seen_adts = + match t with + | FunType (a, r) -> + allow_unserializable && + recurser a seen_adts && + recurser r seen_adts + | PolyFun (_, t) -> + allow_unserializable && + recurser t seen_adts + | Unit -> + allow_unserializable + | MapType (kt, vt) -> + accept_maps && + recurser kt seen_adts && + recurser vt seen_adts + | TypeVar _ -> + (* If we are inside an ADT, then type variable + instantiations are handled outside *) + not @@ List.is_empty seen_adts + | PrimType _ -> + (* Messages and Events are not serialisable in terms of contract parameters *) + allow_unserializable || + 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 ~sloc:(get_rep tname) + (get_id 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 -> + recurser carg (tname :: seen_adts)) + carg_list) + adt.tmap + in + adt_serializable + && List.for_all + ~f:(fun t -> + recurser t seen_adts) + ts ) ) + | Address fts + when check_addresses -> + (* If check_addresses is true, then all field types in the address type should be legal field types. + No need to check for serialisability or storability, since addresses are stored and passed as ByStr20. *) + List.for_all fts ~f:(fun (_, t) -> is_legal_field_type t) + | Address _ -> + true + in + recurser t seen_adts and is_legal_message_field_type t = (* Maps are not allowed. Address values are considered ByStr20 when used as message field value. *) - is_serializable_storable_helper false false t [] + is_serializable_storable_helper false false false t [] - and is_legal_parameter_type t = + and is_legal_transition_parameter_type t = (* Maps are not allowed. Address values should be checked for storable field types. *) - is_serializable_storable_helper false true t [] + is_serializable_storable_helper false false true t [] + + and is_legal_procedure_parameter_type t = + (* Like transition parametes, except that polymorphic parameters are allowed, + since parameters do not need to be serializable. *) + is_serializable_storable_helper false true true t [] and is_legal_field_type t = (* Maps are allowed. Address values should be checked for storable field types. *) - is_serializable_storable_helper true true t [] + is_serializable_storable_helper true false true t [] + let get_msgevnt_type m = if List.exists ~f:(fun (s, _) -> s = ContractUtil.MessagePayload.tag_label) m @@ -426,7 +460,7 @@ module TypeUtilities = struct let rec fun_type_applies ft argtypes = match (ft, argtypes) with | FunType (argt, rest), a :: ats -> - let%bind _ = assert_type_equiv argt a in + let%bind _ = assert_type_assignable argt a in fun_type_applies rest ats | FunType (argt, rest), [] when argt = Unit -> pure rest | t, [] -> pure t @@ -443,7 +477,7 @@ module TypeUtilities = struct match List.zip formals actuals with | Ok arg_pairs -> mapM arg_pairs ~f:(fun (formal, actual) -> - assert_type_equiv formal actual) + assert_type_assignable formal actual) | Unequal_lengths -> fail0 "Incorrect number of arguments to procedure" let rec elab_tfun_with_args_no_gas tf args = @@ -678,7 +712,9 @@ module TypeUtilities = struct | StringLit _ -> pure string_typ | BNum _ -> pure bnum_typ | ByStr _ -> pure bystr_typ - | ByStrX bs -> pure (bystrx_typ (Bystrx.width bs)) + | ByStrX bs -> + (* ByStr20 literals are never considered Address types *) + pure (bystrx_typ (Bystrx.width bs)) (* Check that messages and events have storable parameters. *) | Msg bs -> get_msgevnt_type bs | Map ((kt, vt), _) -> pure (MapType (kt, vt)) @@ -703,7 +739,11 @@ module TypeUtilities = struct | StringLit _ -> pure string_typ | BNum _ -> pure bnum_typ | ByStr _ -> pure bystr_typ - | ByStrX bsx -> pure (bystrx_typ (Bystrx.width bsx)) + | ByStrX bsx -> + (* ByStr20 literals may represent addresses, but only statically. + Dynamically, ByStr20 are considered ByStr20, and are checked for + correct address contents only at certain points. *) + pure (bystrx_typ (Bystrx.width bsx)) (* Check that messages and events have legal parameters. *) | Msg m -> let%bind msg_typ = get_msgevnt_type m in @@ -757,7 +797,7 @@ module TypeUtilities = struct let%bind tmap = constr_pattern_arg_types res cname in let%bind arg_typs = mapM ~f:(fun l -> is_wellformed_lit l) args in let args_valid = - List.for_all2_exn tmap arg_typs ~f:(fun t1 t2 -> type_equiv t1 t2) + List.for_all2_exn tmap arg_typs ~f:(fun t1 t2 -> type_assignable t1 t2) in if not args_valid then fail0 diff --git a/src/base/TypeUtil.mli b/src/base/TypeUtil.mli index f85ea91d6..bed93903d 100644 --- a/src/base/TypeUtil.mli +++ b/src/base/TypeUtil.mli @@ -122,14 +122,14 @@ module TypeUtilities : sig val is_legal_message_field_type : typ -> bool - val is_legal_parameter_type : typ -> bool + val is_legal_transition_parameter_type : typ -> bool + val is_legal_procedure_parameter_type : typ -> bool + val is_legal_field_type : typ -> bool val is_ground_type : typ -> bool - val is_non_map_ground_type : typ -> bool - val get_msgevnt_type : (string * 'a) sexp_list -> (typ, scilla_error sexp_list) result @@ -169,6 +169,10 @@ module TypeUtilities : sig val assert_type_equiv : typ -> typ -> (unit, scilla_error list) result + val type_assignable_list : typ list -> typ list -> bool + + val assert_type_assignable : typ -> typ -> (unit, scilla_error list) result + val assert_type_equiv_with_gas : typ -> typ -> diff --git a/src/eval/Eval.ml b/src/eval/Eval.ml index e756ff4c9..c4ff00f57 100644 --- a/src/eval/Eval.ml +++ b/src/eval/Eval.ml @@ -523,7 +523,7 @@ let init_contract clibs elibs cconstraint' cparams' cfields args' init_bal = tryM ~f:(fun (ps, pt) -> let%bind at = fromR @@ literal_type (snd a) in - if get_id ps = fst a && type_equiv pt at then pure true + if get_id ps = fst a && type_assignable pt at then pure true else fail0 "") cparams ~msg:emsg in diff --git a/tests/base/parser/bad/gold/cmodule-contract-cid-lparen-id-colon-with.scilla.gold b/tests/base/parser/bad/gold/cmodule-contract-cid-lparen-id-colon-with.scilla.gold index c8fdb9a27..243945ce3 100644 --- a/tests/base/parser/bad/gold/cmodule-contract-cid-lparen-id-colon-with.scilla.gold +++ b/tests/base/parser/bad/gold/cmodule-contract-cid-lparen-id-colon-with.scilla.gold @@ -1,12 +1,12 @@ { "errors": [ { - "error_message": "Invalid type in type annotation.\n", + "error_message": "Missing or invalid type in type annotation.\n", "start_location": { "file": "base/parser/bad/cmodule-contract-cid-lparen-id-colon-with.scilla", "line": 5, - "column": 20 + "column": 19 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/base/parser/bad/gold/cmodule-field-id-colon-with.scilla.gold b/tests/base/parser/bad/gold/cmodule-field-id-colon-with.scilla.gold index 20d80a7d1..229bd8d8c 100644 --- a/tests/base/parser/bad/gold/cmodule-field-id-colon-with.scilla.gold +++ b/tests/base/parser/bad/gold/cmodule-field-id-colon-with.scilla.gold @@ -1,11 +1,11 @@ { "errors": [ { - "error_message": "Invalid type in type annotation.\n", + "error_message": "Missing or invalid type in type annotation.\n", "start_location": { "file": "base/parser/bad/cmodule-field-id-colon-with.scilla", "line": 9, - "column": 21 + "column": 19 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/base/parser/bad/gold/exp_t-fun-lparen-id-colon-with.scilexp.gold b/tests/base/parser/bad/gold/exp_t-fun-lparen-id-colon-with.scilexp.gold index 5e4dfc0dc..0ae1f8df7 100644 --- a/tests/base/parser/bad/gold/exp_t-fun-lparen-id-colon-with.scilexp.gold +++ b/tests/base/parser/bad/gold/exp_t-fun-lparen-id-colon-with.scilexp.gold @@ -1,11 +1,11 @@ { "errors": [ { - "error_message": "Invalid type in type annotation.\n", + "error_message": "Missing or invalid type in type annotation.\n", "start_location": { "file": "base/parser/bad/exps/exp_t-fun-lparen-id-colon-with.scilexp", "line": 1, - "column": 14 + "column": 13 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/base/parser/bad/gold/exp_t-let-id-colon-with.scilexp.gold b/tests/base/parser/bad/gold/exp_t-let-id-colon-with.scilexp.gold index 8d18946b8..9a0c27917 100644 --- a/tests/base/parser/bad/gold/exp_t-let-id-colon-with.scilexp.gold +++ b/tests/base/parser/bad/gold/exp_t-let-id-colon-with.scilexp.gold @@ -1,11 +1,11 @@ { "errors": [ { - "error_message": "Invalid type in type annotation.\n", + "error_message": "Missing or invalid type in type annotation.\n", "start_location": { "file": "base/parser/bad/exps/exp_t-let-id-colon-with.scilexp", "line": 1, - "column": 15 + "column": 13 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/base/parser/bad/gold/type_t-cid-lparen-with.scilla.gold b/tests/base/parser/bad/gold/type_t-cid-lparen-with.scilla.gold index b12d71e2d..c9489381d 100644 --- a/tests/base/parser/bad/gold/type_t-cid-lparen-with.scilla.gold +++ b/tests/base/parser/bad/gold/type_t-cid-lparen-with.scilla.gold @@ -1,11 +1,12 @@ { "errors": [ { - "error_message": "Invalid type in type annotation.\n", + "error_message": + "This is an invalid type term, it is likely an ADT missing a valid type as an argument in brackets.\n", "start_location": { "file": "base/parser/bad/type_t-cid-lparen-with.scilla", "line": 5, - "column": 31 + "column": 30 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/base/parser/bad/gold/type_t-cid-with.scilla.gold b/tests/base/parser/bad/gold/type_t-cid-with.scilla.gold index 38094fa7e..68eb29ae8 100644 --- a/tests/base/parser/bad/gold/type_t-cid-with.scilla.gold +++ b/tests/base/parser/bad/gold/type_t-cid-with.scilla.gold @@ -1,12 +1,11 @@ { "errors": [ { - "error_message": - "This is an invalid type term, the ADT constructor arguments are likely incorrect. This necessitates a proper separated capital identifier, type identifier, type in brackets or a map.\n", + "error_message": "Invalid or incomplete type.\n", "start_location": { "file": "base/parser/bad/type_t-cid-with.scilla", - "line": 6, - "column": 31 + "line": 7, + "column": 1 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/base/parser/bad/gold/type_t-forall-tid-period-with.scilla.gold b/tests/base/parser/bad/gold/type_t-forall-tid-period-with.scilla.gold index c036e27e9..f9b2f2294 100644 --- a/tests/base/parser/bad/gold/type_t-forall-tid-period-with.scilla.gold +++ b/tests/base/parser/bad/gold/type_t-forall-tid-period-with.scilla.gold @@ -1,11 +1,12 @@ { "errors": [ { - "error_message": "Invalid type in type annotation.\n", + "error_message": + "This is an invalid forall type, after the period (following forall and a type id) the parser expects a valid type.\n", "start_location": { "file": "base/parser/bad/type_t-forall-tid-period-with.scilla", - "line": 8, - "column": 9 + "line": 6, + "column": 27 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/base/parser/bad/gold/type_t-tid-arrow-with.scilla.gold b/tests/base/parser/bad/gold/type_t-tid-arrow-with.scilla.gold index 71ba624fd..877ddf25f 100644 --- a/tests/base/parser/bad/gold/type_t-tid-arrow-with.scilla.gold +++ b/tests/base/parser/bad/gold/type_t-tid-arrow-with.scilla.gold @@ -1,11 +1,11 @@ { "errors": [ { - "error_message": "Invalid type in type annotation.\n", + "error_message": "This function type lacks a result type.\n", "start_location": { "file": "base/parser/bad/type_t-tid-arrow-with.scilla", - "line": 8, - "column": 1 + "line": 7, + "column": 24 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/checker/bad/gold/bad-exception1.scilla.gold b/tests/checker/bad/gold/bad-exception1.scilla.gold index 1c51cec18..b8df4bda8 100644 --- a/tests/checker/bad/gold/bad-exception1.scilla.gold +++ b/tests/checker/bad/gold/bad-exception1.scilla.gold @@ -59,7 +59,7 @@ }, { "error_message": - "Error in throw of 'e':\nType mismatch: Exception expected, but Event provided.", + "Error in throw of 'e':\nType unassignable: Exception expected, but Event provided.", "start_location": { "file": "checker/bad/bad-exception1.scilla", "line": 25, diff --git a/tests/checker/bad/gold/bad_lib_type.scilla.gold b/tests/checker/bad/gold/bad_lib_type.scilla.gold index cf87da855..fd89c7197 100644 --- a/tests/checker/bad/gold/bad_lib_type.scilla.gold +++ b/tests/checker/bad/gold/bad_lib_type.scilla.gold @@ -20,7 +20,8 @@ "end_location": { "file": "", "line": 0, "column": 0 } }, { - "error_message": "Type mismatch: Int128 expected, but Uint32 provided.", + "error_message": + "Type unassignable: Int128 expected, but Uint32 provided.", "start_location": { "file": "", "line": 0, "column": 0 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/checker/bad/gold/bad_lib_type2.scilla.gold b/tests/checker/bad/gold/bad_lib_type2.scilla.gold index f03c2fbf2..d1de4f311 100644 --- a/tests/checker/bad/gold/bad_lib_type2.scilla.gold +++ b/tests/checker/bad/gold/bad_lib_type2.scilla.gold @@ -21,7 +21,7 @@ }, { "error_message": - "Type mismatch: forall 'A. forall 'B. ('A -> Uint128) -> List ('A) -> List (Uint128) expected, but forall 'A. forall 'B. ('A -> 'B) -> List ('A) -> List ('B) provided.", + "Type unassignable: forall 'A. forall 'B. ('A -> Uint128) -> List ('A) -> List (Uint128) expected, but forall 'A. forall 'B. ('A -> 'B) -> List ('A) -> List ('B) provided.", "start_location": { "file": "", "line": 0, "column": 0 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/checker/bad/gold/bad_lib_type3.scilla.gold b/tests/checker/bad/gold/bad_lib_type3.scilla.gold index 009cb5232..70c09fd38 100644 --- a/tests/checker/bad/gold/bad_lib_type3.scilla.gold +++ b/tests/checker/bad/gold/bad_lib_type3.scilla.gold @@ -21,7 +21,7 @@ }, { "error_message": - "Type mismatch: forall 'A. forall 'B. ('A -> 'B) -> List ('A) -> List ('B) expected, but forall 'A. forall 'B. ('A -> Uint128) -> List ('A) -> List (Uint128) provided.", + "Type unassignable: forall 'A. forall 'B. ('A -> 'B) -> List ('A) -> List ('B) expected, but forall 'A. forall 'B. ('A -> Uint128) -> List ('A) -> List (Uint128) provided.", "start_location": { "file": "", "line": 0, "column": 0 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/checker/bad/gold/constraint_type_illegal.scilla.gold b/tests/checker/bad/gold/constraint_type_illegal.scilla.gold index c5fa1c5e3..f4d7fd6c2 100644 --- a/tests/checker/bad/gold/constraint_type_illegal.scilla.gold +++ b/tests/checker/bad/gold/constraint_type_illegal.scilla.gold @@ -20,7 +20,8 @@ "end_location": { "file": "", "line": 0, "column": 0 } }, { - "error_message": "Type mismatch: Bool expected, but Uint128 provided.", + "error_message": + "Type unassignable: Bool expected, but Uint128 provided.", "start_location": { "file": "", "line": 0, "column": 0 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/checker/bad/gold/inplace-map.scilla.gold b/tests/checker/bad/gold/inplace-map.scilla.gold index 2795d742f..0b7a69c43 100644 --- a/tests/checker/bad/gold/inplace-map.scilla.gold +++ b/tests/checker/bad/gold/inplace-map.scilla.gold @@ -30,7 +30,7 @@ }, { "error_message": - "Type error in updating map gmap[k]\nType mismatch: Int32 expected, but String provided.", + "Type error in updating map gmap[k]\nType unassignable: Int32 expected, but String provided.", "start_location": { "file": "checker/bad/inplace-map.scilla", "line": 19, @@ -49,7 +49,7 @@ }, { "error_message": - "Type error in updating map gmap3[c][b][c]\nType mismatch: String expected, but Int64 provided.", + "Type error in updating map gmap3[c][b][c]\nType unassignable: String expected, but Int64 provided.", "start_location": { "file": "checker/bad/inplace-map.scilla", "line": 38, @@ -68,7 +68,7 @@ }, { "error_message": - "Type error in updating map gmap3[a]\nType mismatch: Map (Int32) (Map (Int64) (String)) expected, but String provided.", + "Type error in updating map gmap3[a]\nType unassignable: Map (Int32) (Map (Int64) (String)) expected, but String provided.", "start_location": { "file": "checker/bad/inplace-map.scilla", "line": 45, @@ -116,7 +116,7 @@ }, { "error_message": - "Type error in updating map gmap[dd]\nType mismatch: String expected, but Map (Int64) (String) provided.", + "Type error in updating map gmap[dd]\nType unassignable: String expected, but Map (Int64) (String) provided.", "start_location": { "file": "checker/bad/inplace-map.scilla", "line": 70, @@ -154,7 +154,7 @@ }, { "error_message": - "Type error in updating map gmap3[b]\nType mismatch: String expected, but Int32 provided.", + "Type error in updating map gmap3[b]\nType unassignable: String expected, but Int32 provided.", "start_location": { "file": "checker/bad/inplace-map.scilla", "line": 95, @@ -173,7 +173,7 @@ }, { "error_message": - "Type error in getting map value gmap3[a][c][c]\nType mismatch: Int32 expected, but Int64 provided.", + "Type error in getting map value gmap3[a][c][c]\nType unassignable: Int32 expected, but Int64 provided.", "start_location": { "file": "checker/bad/inplace-map.scilla", "line": 102, diff --git a/tests/checker/bad/gold/lib_bad1.scilla.gold b/tests/checker/bad/gold/lib_bad1.scilla.gold index c043a3adb..a29412110 100644 --- a/tests/checker/bad/gold/lib_bad1.scilla.gold +++ b/tests/checker/bad/gold/lib_bad1.scilla.gold @@ -30,7 +30,7 @@ }, { "error_message": - "Type mismatch: Message expected, but Uint128 provided.", + "Type unassignable: Message expected, but Uint128 provided.", "start_location": { "file": "", "line": 0, "column": 0 }, "end_location": { "file": "", "line": 0, "column": 0 } }, @@ -45,7 +45,7 @@ }, { "error_message": - "Type mismatch: Message expected, but Uint128 provided.", + "Type unassignable: Message expected, but Uint128 provided.", "start_location": { "file": "", "line": 0, "column": 0 }, "end_location": { "file": "", "line": 0, "column": 0 } }, diff --git a/tests/checker/bad/gold/mappair.scilla.gold b/tests/checker/bad/gold/mappair.scilla.gold index a509f1cb4..51d28c74c 100644 --- a/tests/checker/bad/gold/mappair.scilla.gold +++ b/tests/checker/bad/gold/mappair.scilla.gold @@ -30,7 +30,7 @@ }, { "error_message": - "Type error in the binding to into `p`:\nType mismatch: Int32 expected, but Int64 provided.", + "Type error in the binding to into `p`:\nType unassignable: Int32 expected, but Int64 provided.", "start_location": { "file": "checker/bad/mappair.scilla", "line": 56, @@ -49,7 +49,7 @@ }, { "error_message": - "Type error in the binding to into `l2`:\nType mismatch: Int32 expected, but Int64 provided.", + "Type error in the binding to into `l2`:\nType unassignable: Int32 expected, but Int64 provided.", "start_location": { "file": "checker/bad/mappair.scilla", "line": 72, diff --git a/tests/checker/bad/gold/procedure_bad_type.scilla.gold b/tests/checker/bad/gold/procedure_bad_type.scilla.gold index 1711fe35a..e2d9c7a53 100644 --- a/tests/checker/bad/gold/procedure_bad_type.scilla.gold +++ b/tests/checker/bad/gold/procedure_bad_type.scilla.gold @@ -30,7 +30,7 @@ }, { "error_message": - "Type mismatch: Int32 expected, but List (Bool) provided.", + "Type unassignable: Int32 expected, but List (Bool) provided.", "start_location": { "file": "", "line": 0, "column": 0 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/checker/bad/gold/send_event1.scilla.gold b/tests/checker/bad/gold/send_event1.scilla.gold index 45c1473a4..bb6fa8878 100644 --- a/tests/checker/bad/gold/send_event1.scilla.gold +++ b/tests/checker/bad/gold/send_event1.scilla.gold @@ -39,7 +39,7 @@ }, { "error_message": - "Error in create event `msgs`:\nType mismatch: Event expected, but List (Message) provided.", + "Error in create event `msgs`:\nType unassignable: Event expected, but List (Message) provided.", "start_location": { "file": "checker/bad/send_event1.scilla", "line": 222, @@ -68,7 +68,7 @@ }, { "error_message": - "Error in sending messages `e`:\nType mismatch: List (Message) expected, but Event provided.", + "Error in sending messages `e`:\nType unassignable: List (Message) expected, but Event provided.", "start_location": { "file": "checker/bad/send_event1.scilla", "line": 247, diff --git a/tests/checker/bad/gold/send_event2.scilla.gold b/tests/checker/bad/gold/send_event2.scilla.gold index 0cf1a51f6..728b6349f 100644 --- a/tests/checker/bad/gold/send_event2.scilla.gold +++ b/tests/checker/bad/gold/send_event2.scilla.gold @@ -39,7 +39,7 @@ }, { "error_message": - "Type error in storing value of `hopt` into the field `player_a_hash`:\nType error in storing value of `tm1` into the field `timer`:\nType error in the binding to into `msgs`:\nType error in application of `one_msg`:\nType mismatch: Message expected, but Event provided.", + "Type error in storing value of `hopt` into the field `player_a_hash`:\nType error in storing value of `tm1` into the field `timer`:\nType error in the binding to into `msgs`:\nType error in application of `one_msg`:\nType unassignable: Message expected, but Event provided.", "start_location": { "file": "checker/bad/send_event2.scilla", "line": 178, @@ -105,7 +105,7 @@ }, { "error_message": - "Error in create event `e`:\nType mismatch: Event expected, but Message provided.", + "Error in create event `e`:\nType unassignable: Event expected, but Message provided.", "start_location": { "file": "checker/bad/send_event2.scilla", "line": 247, diff --git a/tests/typecheck/bad/gold/builtin-alt-bn128-pairing-product.scilexp.gold b/tests/typecheck/bad/gold/builtin-alt-bn128-pairing-product.scilexp.gold index afb07001f..99181e271 100644 --- a/tests/typecheck/bad/gold/builtin-alt-bn128-pairing-product.scilexp.gold +++ b/tests/typecheck/bad/gold/builtin-alt-bn128-pairing-product.scilexp.gold @@ -2,7 +2,7 @@ "errors": [ { "error_message": - "Type error in the initialiser of `pair2`:\nType mismatch: Pair (ByStr32) (ByStr32) expected, but Pair (ByStr64) (ByStr64) provided.", + "Type error in the initialiser of `pair2`:\nType unassignable: Pair (ByStr32) (ByStr32) expected, but Pair (ByStr64) (ByStr64) provided.", "start_location": { "file": "typecheck/bad/builtin-alt-bn128-pairing-product.scilexp", "line": 18, diff --git a/tests/typecheck/bad/gold/let-error.scilexp.gold b/tests/typecheck/bad/gold/let-error.scilexp.gold index 5dd1fcde7..951c78c8d 100644 --- a/tests/typecheck/bad/gold/let-error.scilexp.gold +++ b/tests/typecheck/bad/gold/let-error.scilexp.gold @@ -1,7 +1,8 @@ { "errors": [ { - "error_message": "Type mismatch: Int32 expected, but Uint32 provided.", + "error_message": + "Type unassignable: Int32 expected, but Uint32 provided.", "start_location": { "file": "", "line": 0, "column": 0 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/typecheck/bad/gold/list-lit.scilexp.gold b/tests/typecheck/bad/gold/list-lit.scilexp.gold index ad03b3295..9ecb55487 100644 --- a/tests/typecheck/bad/gold/list-lit.scilexp.gold +++ b/tests/typecheck/bad/gold/list-lit.scilexp.gold @@ -2,7 +2,7 @@ "errors": [ { "error_message": - "Type error in the initialiser of `l3`:\nType mismatch: List (Int32) expected, but List (Int64) provided.", + "Type error in the initialiser of `l3`:\nType unassignable: List (Int32) expected, but List (Int64) provided.", "start_location": { "file": "typecheck/bad/list-lit.scilexp", "line": 6, diff --git a/tests/typecheck/bad/gold/list-lit2.scilexp.gold b/tests/typecheck/bad/gold/list-lit2.scilexp.gold index 2fc975b0c..6cf3081d9 100644 --- a/tests/typecheck/bad/gold/list-lit2.scilexp.gold +++ b/tests/typecheck/bad/gold/list-lit2.scilexp.gold @@ -2,7 +2,7 @@ "errors": [ { "error_message": - "Type error in the initialiser of `l3`:\nType mismatch: Int64 expected, but Int32 provided.", + "Type error in the initialiser of `l3`:\nType unassignable: Int64 expected, but Int32 provided.", "start_location": { "file": "typecheck/bad/list-lit2.scilexp", "line": 6, diff --git a/tests/typecheck/bad/gold/map-error.scilexp.gold b/tests/typecheck/bad/gold/map-error.scilexp.gold index 4920706fe..9bf5e18dd 100644 --- a/tests/typecheck/bad/gold/map-error.scilexp.gold +++ b/tests/typecheck/bad/gold/map-error.scilexp.gold @@ -2,7 +2,7 @@ "errors": [ { "error_message": - "Type error in the initialiser of `list_map`:\nType error in application of `folder`:\nType mismatch: 'A -> 'B -> 'B expected, but 'A -> List ('B) -> List ('B) provided.", + "Type error in the initialiser of `list_map`:\nType error in application of `folder`:\nType unassignable: 'A -> 'B -> 'B expected, but 'A -> List ('B) -> List ('B) provided.", "start_location": { "file": "typecheck/bad/map-error.scilexp", "line": 8, diff --git a/tests/typecheck/bad/gold/some.scilexp.gold b/tests/typecheck/bad/gold/some.scilexp.gold index 914f3d0e4..7a4059dcd 100644 --- a/tests/typecheck/bad/gold/some.scilexp.gold +++ b/tests/typecheck/bad/gold/some.scilexp.gold @@ -2,7 +2,7 @@ "errors": [ { "error_message": - "Type error in the initialiser of `p`:\nType mismatch: Option (Bool) expected, but Bool provided.", + "Type error in the initialiser of `p`:\nType unassignable: Option (Bool) expected, but Bool provided.", "start_location": { "file": "typecheck/bad/some.scilexp", "line": 4, diff --git a/tests/typecheck/good/Testtypes.ml b/tests/typecheck/good/Testtypes.ml index 68d2766ec..135a2b14a 100644 --- a/tests/typecheck/good/Testtypes.ml +++ b/tests/typecheck/good/Testtypes.ml @@ -16,92 +16,141 @@ scilla. If not, see . *) +open Core_kernel open OUnit2 open Syntax open ErrorUtils module TestTypeUtils = TypeUtil.TypeUtilities -let make_type_equiv_test st1 st2 eq = +let make_type_assignable_equiv_tests st1 st2 eq f_name f = let open FrontEndParser in - let t1, t2 = - match (parse_type st1, parse_type st2) with + let t1, t2 = match (parse_type st1, parse_type st2) with | Ok t1, Ok t2 -> (t1, t2) | _ -> raise (SyntaxError ( "Error parsing types " ^ st1 ^ " and " ^ st2 - ^ " in type_equiv tests", + ^ " in " ^ f_name ^ " tests", dummy_loc )) in let b, bs = - if eq then (type_equiv t1 t2, "=") else (not (type_equiv t1 t2), "<>") + if eq then (f t1 t2, "=") else (not (f t1 t2), "<>") in let err_msg = "Assert " ^ pp_typ t1 ^ " " ^ bs ^ " " ^ pp_typ t2 ^ " test failed" in test_case (fun _ -> assert_bool err_msg b) + +let make_type_assignable_test st1 st2 eq = + make_type_assignable_equiv_tests st1 st2 eq "type_assignable" type_assignable -let make_type_equiv_tests tlist = - List.map (fun (st1, st2, eq) -> make_type_equiv_test st1 st2 eq) tlist +let make_all_type_assignable_tests tlist = + List.map tlist ~f:(fun (st1, st2, eq) -> make_type_assignable_test st1 st2 eq) -let type_equiv_tests = +let make_type_equiv_test st1 st2 eq = + make_type_assignable_equiv_tests st1 st2 eq "type_equiv" type_equiv + +let make_all_type_equiv_tests tlist = + List.map tlist ~f:(fun (st1, st2, eq) -> make_type_equiv_test st1 st2 eq) + +let equivalent_types = [ - ("Uint32", "Uint32", true); - ("Int32", "Uint32", false); - ( "forall 'A. List ('A) -> List ('A)", - "forall 'B. List ('B) -> List ('B)", - true ); + ("Uint32", "Uint32"); ( "forall 'A. List ('A) -> List ('A)", - "forall 'A. List ('A) -> List ('A) -> List ('A)", - false ); + "forall 'B. List ('B) -> List ('B)"); ( "forall 'A. forall 'B. ('B -> 'A -> 'B) -> 'B -> List ('A) -> 'B", - "forall 'B. forall 'A. ('B -> 'A -> 'B) -> 'B -> List ('A) -> 'B", - false ); - ( "forall 'A. forall 'B. ('B -> 'A -> 'B) -> 'B -> List ('A) -> 'B", - "forall 'B. forall 'A. ('A -> 'B -> 'A) -> 'A -> List ('B) -> 'A", - true ); + "forall 'B. forall 'A. ('A -> 'B -> 'A) -> 'A -> List ('B) -> 'A"); ( "forall 'A. 'A -> forall 'B. List ('B)", - "forall 'B. 'B -> forall 'A. List ('A)", - true ); + "forall 'B. 'B -> forall 'A. List ('A)"); ( "forall 'A. 'A -> (forall 'A. List ('A)) -> 'A", - "forall 'B. 'B -> (forall 'C. List ('C)) -> 'B", - true ); - ( "forall 'A. 'A -> (forall 'A. List ('A)) -> 'B", - "forall 'B. 'B -> (forall 'C. List ('C)) -> 'B", - false ); + "forall 'B. 'B -> (forall 'C. List ('C)) -> 'B"); ( "forall 'A. 'A -> (forall 'A. List ('A)) -> 'B", - "forall 'C. 'C -> (forall 'C. List ('C)) -> 'B", - true ); + "forall 'C. 'C -> (forall 'C. List ('C)) -> 'B"); + (* Addresses *) + ( "ByStr20", "ByStr20"); + ( "ByStr20 with end", + "ByStr20 with end"); + ( "ByStr20 with x : Uint32 end", + "ByStr20 with x : Uint32 end"); + ( "ByStr20 with x : Uint32, y : Bool end", + "ByStr20 with x : Uint32, y : Bool end"); + ( "ByStr20 with y : Bool, x : Uint32 end", + "ByStr20 with x : Uint32, y : Bool end"); + ( "ByStr20 with x : Uint32, y : ByStr20 with end end", + "ByStr20 with x : Uint32, y : ByStr20 with end end"); + ( "ByStr20 with x : Uint32, y : ByStr20 with y2 : ByStr20, y1 : Option Int256 end end", + "ByStr20 with x : Uint32, y : ByStr20 with y1 : Option Int256, y2 : ByStr20 end end"); + ] + +let assignable_but_not_equivalent_types = + [ + (* Addresses *) + ( "ByStr20", + "ByStr20 with end"); + ( "ByStr20 with end", + "ByStr20 with x : Uint32 end"); + ( "ByStr20 with x : Uint32 end", + "ByStr20 with x : Uint32, y : Uint32 end"); + ( "ByStr20 with x : Uint32 end", + "ByStr20 with x : Uint32, y : Uint32, z : ByStr20 with end end"); + ( "ByStr20 with y : Uint32, x : Uint32 end", + "ByStr20 with x : Uint32, y : Uint32, z : ByStr20 with end end"); + ( "ByStr20 with x : Uint32, y : ByStr20 with y1 : Int32 end end", + "ByStr20 with x : Uint32, y : ByStr20 with y2 : Bool, y1 : Int32 end end"); ] -let make_ground_type_test ts exp_bool = - let open FrontEndParser in - let open TestTypeUtils in - let t = - match parse_type ts with - | Ok t -> t - | _ -> - raise - (SyntaxError - ("Error parsing type " ^ ts ^ " in type_equiv tests", dummy_loc)) - in - test_case (fun _ -> - let b = is_ground_type t in - assert_bool "TypeUtil: is_ground_type test failed on type" (b = exp_bool)) - -let ground_type_tests = +let not_assignable_types = [ - ("'A", false); - ("Uint32", true); - ("Uint32 -> 'A", false); - ("forall 'A. List ('A) -> List ('A)", false); - ("List ('A)", false); - ("forall 'A. Map Int32 Uint32", false); - ("forall 'A. Pair Int32 'A", false); + ("Int32", "Uint32"); + ( "forall 'A. List ('A) -> List ('A)", + "forall 'A. List ('A) -> List ('A) -> List ('A)"); + ( "forall 'A. forall 'B. ('B -> 'A -> 'B) -> 'B -> List ('A) -> 'B", + "forall 'B. forall 'A. ('B -> 'A -> 'B) -> 'B -> List ('A) -> 'B"); + ( "forall 'A. 'A -> (forall 'A. List ('A)) -> 'B", + "forall 'B. 'B -> (forall 'C. List ('C)) -> 'B"); + (* Addresses *) + ( "ByStr20 with x : Int32 end", + "ByStr20 with x : Uint32 end"); + ( "ByStr20 with x : Int32 end", + "ByStr20 with y : Int32 end"); + ( "ByStr20 with x : ByStr20 with y1 : Int32 end end", + "ByStr20 with x : ByStr20 with y1 : Uint32 end end"); + ( "ByStr20 with x : ByStr20 with y1 : Int32 end end", + "ByStr20 with x : ByStr20 with y2 : Int32 end end"); ] -let make_ground_type_tests tlist = - List.map (fun (st, eq) -> make_ground_type_test st eq) tlist +let make_test eq (t1, t2) = (t1, t2, eq) + +let reverse_test eq (t1, t2) = (t2, t1, eq) + +let all_type_equiv_tests = + (* Equivalent types *) + List.map equivalent_types ~f:(make_test true) + (* Equivalence should be reflexive *) + @ List.map equivalent_types ~f:(reverse_test true) + (* Assignable but not equivalent *) + @ List.map assignable_but_not_equivalent_types ~f:(make_test false) + (* Non-equivalence is reflexive *) + @ List.map assignable_but_not_equivalent_types ~f:(reverse_test false) + (* Non-assignable implies non-equivalence *) + @ List.map not_assignable_types ~f:(make_test false) + (* Non-equivalence is reflexive *) + @ List.map not_assignable_types ~f:(reverse_test false) + +let all_type_assignable_tests = + (* Equivalence implies assignability *) + List.map equivalent_types ~f:(make_test true) + (* Equivalence should be reflexive, and implies assignability *) + @ List.map equivalent_types ~f:(reverse_test true) + (* Assignable but not equivalent *) + @ List.map assignable_but_not_equivalent_types ~f:(make_test true) + (* Intersection of assignable and non-equivalt is non-reflexive *) + @ List.map assignable_but_not_equivalent_types ~f:(reverse_test false) + (* Non-assignable *) + @ List.map not_assignable_types ~f:(make_test false) + (* Non-assignable and non-equivalent is reflexive + - if it becomes assignable, then it should be place in assignable_but_not_equivalent_types. *) + @ List.map not_assignable_types ~f:(reverse_test false) let make_map_access_type_test t at nindices = let open FrontEndParser in @@ -141,15 +190,14 @@ let map_access_type_tests = ] let make_map_access_type_tests tlist = - List.map - (fun (t, at, nindices) -> make_map_access_type_test t at nindices) - tlist + List.map tlist + ~f:(fun (t, at, nindices) -> make_map_access_type_test t at nindices) let type_equiv_tests = - "type_equiv_tests" >::: make_type_equiv_tests type_equiv_tests + "type_equiv_tests" >::: make_all_type_equiv_tests all_type_equiv_tests -let ground_type_tests = - "ground_type_tests" >::: make_ground_type_tests ground_type_tests +let type_assignable_tests = + "type_assignable_tests" >::: make_all_type_assignable_tests all_type_assignable_tests let map_access_type_tests = "map_access_type_tests" >::: make_map_access_type_tests map_access_type_tests @@ -205,7 +253,7 @@ let all_tests env = "type_check_success_tests" >::: [ type_equiv_tests; + type_assignable_tests; Tests.all_tests env; - ground_type_tests; map_access_type_tests; ]