Pattern Completeness: Warn about future clauses in scattered enums

src/lib/pattern_completeness.ml

@@ -57,6 +57,7 @@ type ctx = {
   variants : (typquant * type_union list) Bindings.t;
   structs : (typquant * (typ * id) list) Bindings.t;
   enums : IdSet.t Bindings.t;
+  is_open : id -> bool;
   constraints : n_constraint list;
   is_mapping : id -> bool;
 }
@@ -755,7 +756,8 @@ module Make (C : Config) = struct
     )
 
   let split_matrix_enum e c matrix =
-    let is_enum_row = function GP_enum (_, id) -> Id.compare e id = 0 | GP_wild -> true | _ -> false in
+    let is_member id = match e with Some member -> Id.compare id member = 0 | None -> false in
+    let is_enum_row = function GP_enum (_, id) -> is_member id | GP_wild -> true | _ -> false in
     Rows
       (rows_to_list matrix
       |> List.filter (fun (_, row) -> columns_to_list row |> (fun xs -> List.nth xs c) |> is_enum_row)
@@ -798,9 +800,9 @@ module Make (C : Config) = struct
     let xs, ys = Util.split_after i unmatcheds in
     xs @ (mk_exp (E_list []) :: ys)
 
-  let reenum e i unmatcheds =
+  let reenum exp i unmatcheds =
     let xs, ys = Util.split_after i unmatcheds in
-    xs @ (mk_exp (E_id e) :: ys)
+    xs @ (exp :: ys)
 
   let rec undefs_except n c v len =
     if n = len then []
@@ -881,22 +883,30 @@ module Make (C : Config) = struct
               | Completeness_unknown -> Completeness_unknown
             end
         | Enum_column typ_id ->
-            let members = Bindings.find typ_id ctx.enums in
-            IdSet.fold
-              (fun member unmatcheds ->
+            let members = Bindings.find typ_id ctx.enums |> IdSet.elements |> List.map (fun id -> Some id) in
+            let members = if ctx.is_open typ_id then members @ [None] else members in
+            let mk_counterexample = function
+              | Some id -> mk_exp (E_id id)
+              | None ->
+                  let id = mk_id (Printf.sprintf "<future %s clause>" (string_of_id typ_id)) in
+                  mk_exp (E_id id)
+            in
+            List.fold_left
+              (fun unmatcheds member ->
                 match unmatcheds with
                 | Incomplete unmatcheds -> Incomplete unmatcheds
                 | Completeness_unknown -> Completeness_unknown
                 | Complete cinfo ->
                     let enum_matrix = split_matrix_enum member i matrix in
                     if row_matrix_empty enum_matrix then (
                       let width = row_matrix_width l matrix in
-                      Incomplete (undefs_except 0 i (mk_exp (E_id member)) width)
+                      Incomplete (undefs_except 0 i (mk_counterexample member) width)
                     )
                     else
-                      matrix_is_complete l ctx enum_matrix |> completeness_map (reenum member i) (union_complete cinfo)
+                      matrix_is_complete l ctx enum_matrix
+                      |> completeness_map (reenum (mk_counterexample member) i) (union_complete cinfo)
               )
-              members (mk_complete [] [])
+              (mk_complete [] []) members
         | Unknown_column -> Completeness_unknown
       end
 

src/lib/pattern_completeness.mli

@@ -58,6 +58,7 @@ type ctx = {
   variants : (typquant * type_union list) Bindings.t;
   structs : (typquant * (typ * id) list) Bindings.t;
   enums : IdSet.t Bindings.t;
+  is_open : id -> bool;
   constraints : n_constraint list;
   is_mapping : id -> bool;
 }

src/lib/rewrites.ml

@@ -903,6 +903,7 @@ let pats_complete l env ps typ =
       Pattern_completeness.variants = Env.get_variants env;
       Pattern_completeness.structs = Env.get_records env;
       Pattern_completeness.enums = Env.get_enums env;
+      Pattern_completeness.is_open = (fun id -> Env.is_scattered_open id env);
       Pattern_completeness.constraints = Env.get_constraints env;
       Pattern_completeness.is_mapping = (fun id -> Env.is_mapping id env);
     }

src/lib/type_check.ml

@@ -2077,6 +2077,7 @@ let pattern_completeness_ctx env =
     Pattern_completeness.variants = Env.get_variants env;
     Pattern_completeness.structs = Env.get_records env;
     Pattern_completeness.enums = Env.get_enums env;
+    Pattern_completeness.is_open = (fun id -> Env.is_scattered_open id env);
     Pattern_completeness.constraints = Env.get_constraints env;
     Pattern_completeness.is_mapping = (fun id -> Env.is_mapping id env);
   }

src/lib/type_check.mli

@@ -198,6 +198,11 @@ module Env : sig
 
   val is_mapping : id -> t -> bool
 
+  (** A scattered definition is open if it can have new clauses added to
+      it, i.e. it exists and has not been closed by the [end]
+      keyword. *)
+  val is_scattered_open : id -> t -> bool
+
   val is_register : id -> t -> bool
 
   (** Check if the type with the given id is a bitfield type *)

src/lib/type_env.ml

@@ -1346,6 +1346,9 @@ let add_scattered_enum id attrs env = env |> add_scattered_id id attrs |> add_en
 
 let is_scattered_id id env = Bindings.mem id env.global.scattered_ids
 
+let is_scattered_open id env =
+  match Bindings.find_opt id env.global.scattered_ids with Some (Ok _) -> true | _ -> false
+
 let end_scattered_id ~at:l id env =
   let attrs = ref [] in
   let updater = function

src/lib/type_env.mli

@@ -217,6 +217,7 @@ val lookup_id : id -> t -> typ lvar
 
 val add_scattered_id : id -> (l * string * Ast.attribute_data option) list -> t -> t
 val is_scattered_id : id -> t -> bool
+val is_scattered_open : id -> t -> bool
 val end_scattered_id : at:Ast.l -> id -> t -> t
 
 val expand_synonyms : t -> typ -> typ

test/pattern_completeness/enum_open_end.sail

@@ -0,0 +1,22 @@
+default Order dec
+
+$include <prelude.sail>
+
+scattered enum E
+
+enum clause E = A
+
+register R : E = A
+
+enum clause E = B
+
+end E
+
+val foo : unit -> unit
+
+function foo() = {
+  match R {
+    A => (),
+    B => (),
+  }
+}

test/pattern_completeness/warn_enum_open.expect

@@ -0,0 +1,6 @@
+Warning: Incomplete pattern match statement at warn_enum_open.sail:16.2-7:
+16 |  match R {
+   |  ^---^
+   | 
+The following expression is unmatched: <future E clause>
+

test/pattern_completeness/warn_enum_open.sail

@@ -0,0 +1,22 @@
+default Order dec
+
+$include <prelude.sail>
+
+scattered enum E
+
+enum clause E = A
+
+register R : E = A
+
+enum clause E = B
+
+val foo : unit -> unit
+
+function foo() = {
+  match R {
+    A => (),
+    B => (),
+  }
+}
+
+end E

test/pattern_completeness/warn_enum_open_other.expect

@@ -0,0 +1,6 @@
+Warning: Incomplete pattern match statement at warn_enum_open_other.sail:18.2-7:
+18 |  match R {
+   |  ^---^
+   | 
+The following expression is unmatched: C
+

test/pattern_completeness/warn_enum_open_other.sail

@@ -0,0 +1,24 @@
+default Order dec
+
+$include <prelude.sail>
+
+scattered enum E
+
+enum clause E = A
+
+register R : E = A
+
+enum clause E = B
+
+enum clause E = C
+
+val foo : unit -> unit
+
+function foo() = {
+  match R {
+    A => (),
+    B => (),
+  }
+}
+
+end E