From 5fb2a22f32d022ac41ad739d9e0442aaa6b9c94a Mon Sep 17 00:00:00 2001 From: trdthg Date: Sat, 27 Jul 2024 20:27:38 +0800 Subject: [PATCH] Check mapping completeness Add basic mapdef completeness check, converting mpat to pat, then to gpat, and finally reusing the match checking logic --- src/lib/effects.ml | 4 +- src/lib/pattern_completeness.ml | 99 +++++++++++++++++++ src/lib/pattern_completeness.mli | 1 + src/lib/type_check.ml | 23 ++++- test/pattern_completeness/mapping_let.sail | 10 ++ test/pattern_completeness/warn_mapping.expect | 6 ++ test/pattern_completeness/warn_mapping.sail | 18 ++++ .../warn_mapping_l.expect | 6 ++ test/pattern_completeness/warn_mapping_l.sail | 3 + .../warn_mapping_r.expect | 12 +++ test/pattern_completeness/warn_mapping_r.sail | 4 + 11 files changed, 181 insertions(+), 5 deletions(-) create mode 100644 test/pattern_completeness/mapping_let.sail create mode 100644 test/pattern_completeness/warn_mapping.expect create mode 100644 test/pattern_completeness/warn_mapping.sail create mode 100644 test/pattern_completeness/warn_mapping_l.expect create mode 100644 test/pattern_completeness/warn_mapping_l.sail create mode 100644 test/pattern_completeness/warn_mapping_r.expect create mode 100644 test/pattern_completeness/warn_mapping_r.sail diff --git a/src/lib/effects.ml b/src/lib/effects.ml index e61bff383..4485b26fc 100644 --- a/src/lib/effects.ml +++ b/src/lib/effects.ml @@ -218,7 +218,9 @@ let infer_def_direct_effects asserts_termination def = effects := EffectSet.add IncompleteMatch !effects | None -> Reporting.unreachable l __POS__ "Empty funcls in infer_def_direct_effects" end - | DEF_aux (DEF_mapdef _, _) -> effects := EffectSet.add IncompleteMatch !effects + | DEF_aux (DEF_mapdef _, def_annot) -> + if Option.is_some (get_def_attribute "incomplete" def_annot) then + effects := EffectSet.add IncompleteMatch !effects | DEF_aux (DEF_scattered _, _) -> effects := EffectSet.add Scattered !effects | _ -> () end; diff --git a/src/lib/pattern_completeness.ml b/src/lib/pattern_completeness.ml index 831332de7..ec92cb823 100644 --- a/src/lib/pattern_completeness.ml +++ b/src/lib/pattern_completeness.ml @@ -953,4 +953,103 @@ module Make (C : Config) = struct let is_complete ?(keyword = "match") l ctx cases head_exp_typ = Option.is_some (is_complete_wildcarded ~keyword l ctx cases head_exp_typ) + + let rec pat_of_mpat mpat = + match mpat with + | MP_aux (mpat_aux, l) -> + let res = + match mpat_aux with + | MP_lit lit -> P_lit lit + | MP_id id -> P_id id + | MP_app (id, mpat_list) -> P_app (id, List.map (fun mpat -> pat_of_mpat mpat) mpat_list) + | MP_vector mpat_list -> P_vector (List.map (fun mpat -> pat_of_mpat mpat) mpat_list) + | MP_vector_concat mpat_list -> P_vector_concat (List.map (fun mpat -> pat_of_mpat mpat) mpat_list) + | MP_vector_subrange (id, l, r) -> P_vector_subrange (id, l, r) + | MP_tuple mpat_list -> P_tuple (List.map (fun mpat -> pat_of_mpat mpat) mpat_list) + | MP_list mpat_list -> P_list (List.map (fun mpat -> pat_of_mpat mpat) mpat_list) + | MP_cons (mpat1, mpat2) -> P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2) + | MP_string_append mpat_list -> P_string_append (List.map (fun mpat -> pat_of_mpat mpat) mpat_list) + | MP_typ (mp1, atyp) -> P_typ (atyp, pat_of_mpat mp1) + | MP_struct id_mpat_list -> + let fpl = List.map (fun (id, mpat) -> (id, pat_of_mpat mpat)) id_mpat_list in + P_struct (fpl, FP_no_wild) + | MP_as (mpat, id) -> ( + match pat_of_mpat mpat with P_aux (pat, _id) -> pat + ) + in + P_aux (res, l) + + let is_complete_gpats ?(keyword = "match") l ctx have_guard gpats_matrix = + let res = + match matrix_is_complete l ctx gpats_matrix with + | Incomplete (unmatched :: _) -> + let guard_info = if have_guard then " by unguarded patterns" else "" in + Reporting.warn "Incomplete pattern match statement at" (shrink_loc keyword l) + ("The following expression is unmatched" ^ guard_info ^ ": " + ^ (string_of_exp unmatched |> Util.yellow |> Util.clear) + ); + false + | Incomplete [] -> Reporting.unreachable l __POS__ "Got unmatched pattern matrix without witness" [@coverage off] + | Complete cinfo -> + (* let wildcarded_pats = List.map (fun (_, pat) -> insert_wildcards cinfo pat) pats in *) + List.iter + (fun (idx, _) -> + if IntSet.mem idx.num cinfo.redundant then + Reporting.warn "Redundant case" idx.loc "This match case is never used" + ) + (rows_to_list gpats_matrix); + true + | Completeness_unknown -> false + in + res + + let is_complete_mapcls_wildcarded ?(keyword = "match") l ctx mapcls typl typr = + let have_guard = false in + let rec lpat_of_mapcl mapcl left = + (* We don't consider guarded cases *) + let pat_of_mpexp = function + | MPat_aux (mpexp_aux, l) -> ( + match mpexp_aux with MPat_when (mpat, exp) -> None | MPat_pat mpat -> Some (pat_of_mpat mpat) + ) + in + let rec pexp_to_pat = function + | Pat_aux (Pat_exp ((P_aux (_, (l, _)) as pat), _), _) -> Some pat + | Pat_aux (Pat_when _, _) -> None + in + match mapcl with + | MCL_aux (mapcl_aux, _) -> + if left then ( + match mapcl_aux with + | MCL_bidir (mpexp, _) -> pat_of_mpexp mpexp + | MCL_forwards pexp -> pexp_to_pat pexp + | MCL_backwards pexp -> None + ) + else ( + match mapcl_aux with + | MCL_bidir (_, mpexp) -> pat_of_mpexp mpexp + | MCL_forwards pexp -> None + | MCL_backwards pexp -> pexp_to_pat pexp + ) + in + let rec opt_cases_to_pats from have_guard = function + | [] -> (have_guard, []) + | Some (P_aux (_, (l, _)) as pat) :: cases -> + let pat, from = number_pat from pat in + let have_guard, pats = opt_cases_to_pats from have_guard cases in + (have_guard, (l, pat) :: pats) + | _ :: cases -> opt_cases_to_pats from true cases + in + (* prepare left *) + let lpats = List.map (fun mapcl -> lpat_of_mapcl mapcl true) mapcls in + let _, lpats = opt_cases_to_pats 0 have_guard lpats in + let lmatrix = + Rows (List.mapi (fun i (l, pat) -> ({ loc = l; num = i }, Columns [generalize ctx (Some typl) pat])) lpats) + in + (* prepare right *) + let rpats = List.map (fun mapcl -> lpat_of_mapcl mapcl false) mapcls in + let _, rpats = opt_cases_to_pats 0 have_guard rpats in + let rmatrix = + Rows (List.mapi (fun i (l, pat) -> ({ loc = l; num = i }, Columns [generalize ctx (Some typr) pat])) rpats) + in + is_complete_gpats l ctx have_guard lmatrix && is_complete_gpats l ctx have_guard rmatrix end diff --git a/src/lib/pattern_completeness.mli b/src/lib/pattern_completeness.mli index be22c26dc..0197db6e0 100644 --- a/src/lib/pattern_completeness.mli +++ b/src/lib/pattern_completeness.mli @@ -93,4 +93,5 @@ module Make (C : Config) : sig val is_complete_funcls_wildcarded : ?keyword:string -> Parse_ast.l -> ctx -> C.t funcl list -> typ -> C.t funcl list option val is_complete : ?keyword:string -> Parse_ast.l -> ctx -> C.t pexp list -> typ -> bool + val is_complete_mapcls_wildcarded : ?keyword:string -> Parse_ast.l -> ctx -> C.t mapcl list -> typ -> typ -> bool end diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 9546fd6da..e81d449af 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -4566,6 +4566,12 @@ let check_fundef env def_annot (FD_aux (FD_function (recopt, tannot_opt, funcls) env ) +let check_mapdef_completeness l env mapcls typl typr = + let ctx = pattern_completeness_ctx env in + match PC.is_complete_mapcls_wildcarded l ctx mapcls typl typr with + | true -> add_def_attribute (gen_loc l) "complete" None + | false -> add_def_attribute (gen_loc l) "incomplete" None + let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _))) = typ_print (lazy ("\nChecking mapping " ^ string_of_id id)); let inline_tannot = @@ -4582,11 +4588,11 @@ let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, (Some vs_l, quant, typ) | None, None -> typ_error l "Mapping does not have any declared type" in - begin + let typl, typr = match typ with - | Typ_aux (Typ_bidir (_, _), _) -> () + | Typ_aux (Typ_bidir (l, r), _) -> (l, r) | _ -> typ_error l "Mapping type must be a bi-directional mapping" - end; + in (* If we have a val spec, then the mapping itself shouldn't be marked as private *) let fix_body_visibility = match (have_val_spec, def_annot.visibility) with @@ -4607,7 +4613,16 @@ let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, in let mapcl_env = Env.add_typquant l quant env in let mapcls = List.map (fun mapcl -> check_mapcl mapcl_env mapcl typ) mapcls in - let def_annot = fix_body_visibility def_annot in + + let update_attr = + if + Option.is_some (get_def_attribute "complete" def_annot) + || Option.is_some (get_def_attribute "incomplete" def_annot) + then fun attrs -> attrs + else check_mapdef_completeness l env mapcls typl typr + in + + let def_annot = fix_body_visibility (update_attr def_annot) in let env = Env.define_val_spec id env in ( vs_def @ [DEF_aux (DEF_mapdef (MD_aux (MD_mapping (id, empty_tannot_opt, mapcls), (l, empty_tannot))), def_annot)], env diff --git a/test/pattern_completeness/mapping_let.sail b/test/pattern_completeness/mapping_let.sail new file mode 100644 index 000000000..680035862 --- /dev/null +++ b/test/pattern_completeness/mapping_let.sail @@ -0,0 +1,10 @@ +struct bool2 = { + field: bool, +} + +mapping m : bool <-> bool2 = { + true <-> struct { field = true }, + false <-> struct{ field = false }, +} + +let a = m(true) diff --git a/test/pattern_completeness/warn_mapping.expect b/test/pattern_completeness/warn_mapping.expect new file mode 100644 index 000000000..a474d0192 --- /dev/null +++ b/test/pattern_completeness/warn_mapping.expect @@ -0,0 +1,6 @@ +Warning: Incomplete pattern match statement at warn_mapping.sail:15.0-5: +15 |mapping bool_rev3 : bool <-> bool2 = { +  |^---^ +  | +The following expression is unmatched: struct { field = false } + diff --git a/test/pattern_completeness/warn_mapping.sail b/test/pattern_completeness/warn_mapping.sail new file mode 100644 index 000000000..824907915 --- /dev/null +++ b/test/pattern_completeness/warn_mapping.sail @@ -0,0 +1,18 @@ +struct bool2 = { + field: bool, +} + +mapping bool_rev : bool <-> bool2 = { + true <-> struct { field = true }, + false <-> struct{ field = false }, +} + +mapping bool_rev2 : bool <-> bool2 = { + true <-> struct { field = false }, + false <-> struct{ field = true }, +} + +mapping bool_rev3 : bool <-> bool2 = { + true <-> struct { field = true }, + false <-> struct{ field = true }, +} diff --git a/test/pattern_completeness/warn_mapping_l.expect b/test/pattern_completeness/warn_mapping_l.expect new file mode 100644 index 000000000..75c7bde2d --- /dev/null +++ b/test/pattern_completeness/warn_mapping_l.expect @@ -0,0 +1,6 @@ +Warning: Incomplete pattern match statement at warn_mapping_l.sail:1.0-5: +1 |mapping m : bool <-> int = { +  |^---^ +  | +The following expression is unmatched: false + diff --git a/test/pattern_completeness/warn_mapping_l.sail b/test/pattern_completeness/warn_mapping_l.sail new file mode 100644 index 000000000..99406813a --- /dev/null +++ b/test/pattern_completeness/warn_mapping_l.sail @@ -0,0 +1,3 @@ +mapping m : bool <-> int = { + forwards true => 1, +} diff --git a/test/pattern_completeness/warn_mapping_r.expect b/test/pattern_completeness/warn_mapping_r.expect new file mode 100644 index 000000000..1df09fe6d --- /dev/null +++ b/test/pattern_completeness/warn_mapping_r.expect @@ -0,0 +1,12 @@ +Warning: Deprecated warn_mapping_r.sail:2.3-12: +2 | true => 1, +  | ^-------^ +  | +Single direction mapping clause should be prefixed by a direction, either forwards or backwards + +Warning: Incomplete pattern match statement at warn_mapping_r.sail:1.0-5: +1 |mapping m : bool <-> int = { +  |^---^ +  | +The following expression is unmatched: false + diff --git a/test/pattern_completeness/warn_mapping_r.sail b/test/pattern_completeness/warn_mapping_r.sail new file mode 100644 index 000000000..631a60094 --- /dev/null +++ b/test/pattern_completeness/warn_mapping_r.sail @@ -0,0 +1,4 @@ +mapping m : bool <-> int = { + true => 1, + backwards 2 => false, +}