Commit eda92a0b authored by Andrei Paskevich's avatar Andrei Paskevich

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.
parent 66768c1b
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
......@@ -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 *)
......
......@@ -68,7 +68,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 =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment