From 47a89e964eff434a629ca8980a6a53d1edf0f01b Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 23 Jan 2024 23:14:17 +0000 Subject: [PATCH] Fix issues with missing well-formedness checks Make sure numeric type synonyms with arguments are expanded correctly --- src/lib/type_check.ml | 7 ++++++- src/lib/type_env.ml | 16 +++++++++++++--- test/lem/run_tests.py | 1 + test/typecheck/fail/wf_assign_type.expect | 10 ++++++++++ test/typecheck/fail/wf_assign_type.sail | 11 +++++++++++ test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/wf_register_type.sail | 9 +++++++++ test/typecheck/pass/wf_register_type/v1.expect | 10 ++++++++++ test/typecheck/pass/wf_register_type/v1.sail | 7 +++++++ 9 files changed, 68 insertions(+), 5 deletions(-) create mode 100644 test/typecheck/fail/wf_assign_type.expect create mode 100644 test/typecheck/fail/wf_assign_type.sail create mode 100644 test/typecheck/pass/wf_register_type.sail create mode 100644 test/typecheck/pass/wf_register_type/v1.expect create mode 100644 test/typecheck/pass/wf_register_type/v1.sail diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index da6b361b7..618b28665 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -2824,6 +2824,7 @@ and bind_assignment assign_l env (LE_aux (lexp_aux, (lexp_l, uannot)) as lexp) e match lexp_aux with | LE_app (f, xs) -> (check_exp env (E_aux (E_app (f, xs @ [exp]), (lexp_l, uannot))) unit_typ, env) | LE_typ (typ_annot, _) -> + Env.wf_typ ~at:lexp_l env typ_annot; let checked_exp = crule check_exp env exp typ_annot in let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in (annot_assign tlexp checked_exp, env') @@ -3453,7 +3454,8 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ = let typ_args = match expected_ret_typ with | None -> typ_args - | Some expect when is_exist (Env.expand_synonyms env expect) || is_exist !typ_ret -> typ_args + | Some expect when is_exist (Env.expand_synonyms env expect) -> typ_args + | Some expect when is_exist !typ_ret -> typ_args | Some expect -> ( let goals = quant_kopts (mk_typquant !quants) |> List.map kopt_kid |> KidSet.of_list in try @@ -4626,6 +4628,7 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t = | DEF_default default -> check_default env def_annot default | DEF_overload (id, ids) -> ([DEF_aux (DEF_overload (id, ids), def_annot)], Env.add_overloads def_annot.loc id ids env) | DEF_register (DEC_aux (DEC_reg (typ, id, None), (l, uannot))) -> begin + Env.wf_typ ~at:l env typ; match typ with | Typ_aux (Typ_app (Id_aux (Id "option", _), [_]), _) -> Reporting.warn "No default value" l "Registers of type option should explicitly be given a default value"; @@ -4643,6 +4646,8 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t = ) end | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), (l, _))) -> + typ_print (lazy "WF reg"); + Env.wf_typ ~at:l env typ; let checked_exp = crule check_exp env exp typ in let env = Env.add_register id typ env in ( [ diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml index 9a0ced5fe..9015a1abf 100644 --- a/src/lib/type_env.ml +++ b/src/lib/type_env.ml @@ -556,7 +556,12 @@ let mk_synonym typq typ_arg = let typ_arg, ncs = subst_args env l kopts args in (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs) | [], [] -> (typ_arg, ncs) - | _, _ -> typ_error l "Synonym applied to bad arguments" + | kopts, args -> + typ_error l + ("Synonym applied to bad arguments " + ^ Util.string_of_list ", " string_of_kinded_id kopts + ^ Util.string_of_list ", " string_of_typ_arg args + ) in fun l env args -> let typ_arg, ncs = subst_args env l kopts args in @@ -648,7 +653,12 @@ and wf_nexp ?(exs = KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) = ) end | Nexp_constant _ -> () - | Nexp_app (_, nexps) -> List.iter (fun n -> wf_nexp ~exs env n) nexps + | Nexp_app (id, nexps) -> + let name = string_of_id id in + (* We allow the abs, mod, and div functions that are included in the SMTLIB2 integer theory *) + if name = "abs" || name = "mod" || name = "div" || Bindings.mem id env.global.synonyms then + List.iter (fun n -> wf_nexp ~exs env n) nexps + else typ_error l ("Unknown type level operator or function " ^ name) | Nexp_times (nexp1, nexp2) -> wf_nexp ~exs env nexp1; wf_nexp ~exs env nexp2 @@ -734,7 +744,7 @@ and expand_nexp_synonyms env (Nexp_aux (aux, l) as nexp) = | Nexp_app (id, args) -> ( try begin - match get_typ_synonym id env l env [] with + match get_typ_synonym id env l env (List.map arg_nexp args) with | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp | _ -> typ_error l ("Expected Int when expanding synonym " ^ string_of_id id) end diff --git a/test/lem/run_tests.py b/test/lem/run_tests.py index 32b414939..9f02cd9c5 100755 --- a/test/lem/run_tests.py +++ b/test/lem/run_tests.py @@ -43,6 +43,7 @@ # The Lem backend needs sail_mem_read to be instantiated at a minimum 'concurrency_interface_dec', 'concurrency_interface_inc', + 'wf_register_type', } print('Sail is {}'.format(sail)) diff --git a/test/typecheck/fail/wf_assign_type.expect b/test/typecheck/fail/wf_assign_type.expect new file mode 100644 index 000000000..ca00c56ee --- /dev/null +++ b/test/typecheck/fail/wf_assign_type.expect @@ -0,0 +1,10 @@ +Type error: +fail/wf_assign_type.sail:9.10-17: +9 | var Y : bits(X) = 0b00; +  | ^-----^ +  | Well-formedness check failed for type +  | +  | Caused by fail/wf_assign_type.sail:9.15-16: +  | 9 | var Y : bits(X) = 0b00; +  |  | ^ +  |  | Undefined type synonym X diff --git a/test/typecheck/fail/wf_assign_type.sail b/test/typecheck/fail/wf_assign_type.sail new file mode 100644 index 000000000..797d02821 --- /dev/null +++ b/test/typecheck/fail/wf_assign_type.sail @@ -0,0 +1,11 @@ +default Order dec + +$include + +type bar : Int = 10 + +function foo() -> bits(bar) = { + let X = sizeof(bar); + var Y : bits(X) = 0b00; + Y +} diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index bef20ea7f..6d1bfa9e5 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -9,4 +9,4 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}. 26 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * 'ex340# in {32, 64} +  | * 'ex343# in {32, 64} diff --git a/test/typecheck/pass/wf_register_type.sail b/test/typecheck/pass/wf_register_type.sail new file mode 100644 index 000000000..a2bdda4fa --- /dev/null +++ b/test/typecheck/pass/wf_register_type.sail @@ -0,0 +1,9 @@ +default Order dec + +$include + +type x : Int = 8 + +type operator /('n : Int, 'm : Int) -> Int = div('n, 'm) + +register r : bits(x / 2) = 0x0 diff --git a/test/typecheck/pass/wf_register_type/v1.expect b/test/typecheck/pass/wf_register_type/v1.expect new file mode 100644 index 000000000..8210e817e --- /dev/null +++ b/test/typecheck/pass/wf_register_type/v1.expect @@ -0,0 +1,10 @@ +Type error: +pass/wf_register_type/v1.sail:7.13-24: +7 |register r : bits(x / 2) = 0x0 +  | ^---------^ +  | Well-formedness check failed for type +  | +  | Caused by pass/wf_register_type/v1.sail:7.18-23: +  | 7 |register r : bits(x / 2) = 0x0 +  |  | ^---^ +  |  | Unknown type level operator or function (operator /) diff --git a/test/typecheck/pass/wf_register_type/v1.sail b/test/typecheck/pass/wf_register_type/v1.sail new file mode 100644 index 000000000..ee723ee2c --- /dev/null +++ b/test/typecheck/pass/wf_register_type/v1.sail @@ -0,0 +1,7 @@ +default Order dec + +$include + +type x : Int = 8 + +register r : bits(x / 2) = 0x0