Check mapping completeness

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;

src/lib/frontend.ml

@@ -79,6 +79,7 @@ let check_ast (asserts_termination : bool) (env : Type_check.Env.t) (ast : untyp
     Type_check.typed_ast * Type_check.Env.t * Effects.side_effect_info =
   let ast, env = Type_error.check env ast in
   let ast = Scattered.descatter ast in
+  let ast, env = Type_error.check Type_check.initial_env (Type_check.strip_ast ast) in
   let side_effects = Effects.infer_side_effects asserts_termination ast in
   Effects.check_side_effects side_effects ast;
   let () = if !opt_ddump_tc_ast then Pretty_print_sail.output_ast stdout (Type_check.strip_ast ast) else () in

src/lib/pattern_completeness.ml

@@ -953,4 +953,113 @@ 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_matrixs ?(keyword = "match") l ctx have_guard typ2matrixs =
+    List.fold_left
+      (fun all_complete (typ, matrix) ->
+        (* be careful, all_complete && match { ... } will skip after warnings *)
+        let complete =
+          match matrix_is_complete l ctx 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.warn "Unreachable pattern match type at" (shrink_loc keyword l)
+                ("The following type is unreachable: " ^ (string_of_typ typ |> Util.yellow |> Util.clear));
+              false
+          | Complete cinfo ->
+              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 matrix);
+              true
+          | Completeness_unknown -> false
+        in
+        all_complete && complete
+      )
+      true typ2matrixs
+
+  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
+    (* TODO: handle unsupported syntax *)
+    try
+      (* 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_matrixs ~keyword:"mapping" l ctx have_guard [(typl, lmatrix); (typr, rmatrix)]
+    with _ -> false
 end

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

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

test/pattern_completeness/mapping.sail

@@ -0,0 +1,10 @@
+struct bool2 = {
+    field: bool,
+}
+
+mapping m : bool <-> bool2 = {
+   true <-> struct { field = true },
+   false <->  struct{ field = false },
+}
+
+let foo = m(true)

test/pattern_completeness/warn_mapping_imcomplete.expect

@@ -0,0 +1,43 @@
+Warning: Incomplete pattern match statement at warn_mapping_imcomplete.sail:10.0-7:
+10 |mapping imcomplete_oneside : bool <-> bool2 = {
+   |^-----^
+   | 
+The following expression is unmatched: struct { field = true }
+
+Warning: Incomplete pattern match statement at warn_mapping_imcomplete.sail:15.0-7:
+15 |mapping imcomplete_both_side : bool <-> bool2 = {
+   |^-----^
+   | 
+The following expression is unmatched: false
+
+Warning: Unreachable pattern match type at warn_mapping_imcomplete.sail:20.0-7:
+20 |mapping forwords_unreachable : bool <-> int = {
+   |^-----^
+   | 
+The following type is unreachable: int
+
+Warning: Unreachable pattern match type at warn_mapping_imcomplete.sail:24.0-7:
+24 |mapping backwords_unreachable : bool <-> int = {
+   |^-----^
+   | 
+The following type is unreachable: bool
+
+Warning: Unreachable pattern match type at warn_mapping_imcomplete.sail:28.0-7:
+28 |mapping multi_warning : bool <-> int = {
+   |^-----^
+   | 
+The following type is unreachable: bool
+
+Warning: Incomplete pattern match statement at warn_mapping_imcomplete.sail:28.0-7:
+28 |mapping multi_warning : bool <-> int = {
+   |^-----^
+   | 
+The following expression is unmatched: 3
+
+Warning: Unreachable pattern match type at Code generated nearby:
+warn_mapping_imcomplete.sail:38.0-79:
+38 |mapping clause encdec = true if enabled <-> struct { field = false } if enabled
+   |^-----------------------------------------------------------------------------^
+   | 
+The following type is unreachable: bool
+

test/pattern_completeness/warn_mapping_imcomplete.sail

@@ -0,0 +1,40 @@
+struct bool2 = {
+    field: bool,
+}
+
+mapping complete : bool <-> bool2 = {
+   true <-> struct { field = false },
+   false <->  struct{ field = true },
+}
+
+mapping imcomplete_oneside : bool <-> bool2 = {
+   true <-> struct { field = false },
+   false <-> struct { field = false },
+}
+
+mapping imcomplete_both_side : bool <-> bool2 = {
+   true <-> struct { field = false },
+   true <-> struct { field = false },
+}
+
+mapping forwords_unreachable : bool <-> int = {
+   forwards _ => 1,
+}
+
+mapping backwords_unreachable : bool <-> int = {
+   backwards _ => false,
+}
+
+mapping multi_warning : bool <-> int = {
+   backwards 2 => false,
+}
+
+register enabled : bool
+
+val encdec : bool <-> bool2
+
+scattered mapping encdec
+
+mapping clause encdec = true if enabled <-> struct { field = false } if enabled
+
+end encdec

test/typecheck/fail/issue243.expect

@@ -1,3 +1,9 @@
+Warning: Incomplete pattern match statement at fail/issue243.sail:6.0-7:
+6 |mapping e_pair_bits : (E,E) <-> bits(2) =
+  |^-----^
+  | 
+The following expression is unmatched: (EB, EA)
+
 Type error:
 fail/issue243.sail:17.70-72:
 17 |mapping f_bits = { FE(struct { e1 = e1, v1 = v1 }) <-> e_pair_bits(e1,e1) @ v1 }