Mlw_expr: fix potentially unsound pattern matching in programs

split the ppat_ghost field in program patterns into two distinct
conditions:
- ppat_ghost, indicating that the pattern starts as ghost,
  meaning that all variables in it are ghost, too;
- ppat_fail, meaning that the pattern contains a refutable
  ghost subpattern, which makes the match in the extracted code
  impossible, which makes the whole match expression ghost.

Until now, the two conditions were disjunctively combined, making
admissible the invalid pattern matching in bench/p/b-d/ghost4.mlw.

bench/programs/bad-typing/ghost4.mlw

+module M
+
+  type t = { ghost a : bool; b : int; c : int }
+
+  let bad (z : t) : int
+    ensures { result = if z.a then z.b else z.c }
+  = match z with
+    | { a = True; b = x } | { a = False; c = x } -> x
+    end
+
+end

src/whyml/mlw_expr.ml

@@ -124,7 +124,8 @@ let pl_clone sm =
 type ppattern = {
   ppat_pattern : pattern;
   ppat_ity     : ity;
-  ppat_ghost   : bool;
+  ppat_ghost   : bool;  (* matches a ghost value *)
+  ppat_fail    : bool;  (* refutable under ghost *)
 }
 
 type pre_ppattern =
@@ -137,7 +138,7 @@ type pre_ppattern =
 
 let make_ppattern pp ?(ghost=false) ity =
   let hv = Hstr.create 3 in
-  let gghost = ref false in
+  let fail = ref false in
   let find id ghost ity =
     try
       let pv = Hstr.find hv id.pre_name in
@@ -155,7 +156,7 @@ let make_ppattern pp ?(ghost=false) ity =
         if pls.pl_hidden then raise (HiddenPLS pls);
         if pls.pl_ls.ls_constr = 0 then
           raise (Term.ConstructorExpected pls.pl_ls);
-        if ghost && pls.pl_ls.ls_constr > 1 then gghost := true;
+        if ghost && pls.pl_ls.ls_constr > 1 then fail := true;
         let ityv = pls.pl_value.fd_ity in
         let sbs = ity_match ity_subst_empty ityv ity in
         let mtch arg pp =
@@ -169,7 +170,7 @@ let make_ppattern pp ?(ghost=false) ity =
     | PPlapp (ls,ppl) ->
         if ls.ls_constr = 0 then
           raise (Term.ConstructorExpected ls);
-        if ghost && ls.ls_constr > 1 then gghost := true;
+        if ghost && ls.ls_constr > 1 then fail := true;
         let ityv = ity_of_ty_opt ls.ls_value in
         let sbs = ity_match ity_subst_empty ityv ity in
         let mtch arg pp =
@@ -185,9 +186,9 @@ let make_ppattern pp ?(ghost=false) ity =
         pat_as (make ghost ity pp) (find id ghost ity).pv_vs;
   in
   let pat = make ghost ity pp in
-  let gh = ghost || !gghost in
   Hstr.fold Mstr.add hv Mstr.empty,
-  { ppat_pattern = pat; ppat_ity = ity; ppat_ghost = gh }
+  { ppat_pattern = pat; ppat_ity = ity;
+    ppat_ghost = ghost; ppat_fail = !fail }
 
 (** program symbols *)
 
@@ -634,18 +635,16 @@ let e_case e0 bl =
   let bity = match bl with
     | (_,e)::_ -> ity_of_expr e
     | [] -> raise Term.EmptyCase in
-  let multi_br = List.length bl > 1 in
   let rec branch ghost eff syms = function
     | (pp,e)::bl ->
-        if e0.e_ghost && not pp.ppat_ghost then
-          Loc.errorm "Non-ghost pattern in a ghost position";
+        if e0.e_ghost <> pp.ppat_ghost then
+          Loc.errorm "Invalid pattern ghost status";
         ity_equal_check (ity_of_expr e0) pp.ppat_ity;
         ity_equal_check (ity_of_expr e) bity;
         let eff = eff_union eff e.e_effect in
         let del_vs vs _ syms = del_pv_syms (restore_pv vs) syms in
         let bsyms = Mvs.fold del_vs pp.ppat_pattern.pat_vars e.e_syms in
-        (* one-branch match is not ghost even if its pattern is ghost *)
-        let ghost = ghost || (multi_br && pp.ppat_ghost) || e.e_ghost in
+        let ghost = ghost || pp.ppat_fail || e.e_ghost in
         branch ghost eff (syms_union syms bsyms) bl
     | [] ->
         (* the cumulated effect of all branches, w/out e0 *)
@@ -655,7 +654,8 @@ let e_case e0 bl =
         let syms = add_e_syms e0 syms in
         mk_expr (Ecase (e0,bl)) (VTvalue bity) ghost eff syms
   in
-  branch false eff_empty syms_empty bl
+  (* one-branch match is not ghost even if the matched value is *)
+  branch (e0.e_ghost && List.length bl > 1) eff_empty syms_empty bl
 
 (* ghost *)
 

src/whyml/mlw_expr.mli

@@ -67,7 +67,8 @@ val pl_clone : Theory.symbol_map -> symbol_map
 type ppattern = private {
   ppat_pattern : pattern;
   ppat_ity     : ity;
-  ppat_ghost   : bool;
+  ppat_ghost   : bool;  (* matches a ghost value *)
+  ppat_fail    : bool;  (* refutable under ghost *)
 }
 
 type pre_ppattern =