diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 8 | ||||
| -rw-r--r-- | src/ast_util.mli | 9 | ||||
| -rw-r--r-- | src/c_backend.ml | 2 | ||||
| -rw-r--r-- | src/pattern_completeness.ml | 294 | ||||
| -rw-r--r-- | src/sail.ml | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 13 | ||||
| -rw-r--r-- | src/type_check.mli | 7 | ||||
| -rw-r--r-- | src/util.ml | 7 | ||||
| -rw-r--r-- | src/util.mli | 4 |
9 files changed, 333 insertions, 14 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 5756c954..53f00825 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -52,6 +52,10 @@ open Ast open Util module Big_int = Nat_big_num +type mut = Immutable | Mutable + +type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound + let no_annot = (Parse_ast.Unknown, ()) let gen_loc l = Parse_ast.Generated l @@ -924,3 +928,7 @@ let split_defs f (Defs defs) = Some (Defs (List.rev pre_defs), def, Defs post_defs) let append_ast (Defs ast1) (Defs ast2) = Defs (ast1 @ ast2) + +let type_union_id (Tu_aux (aux, _)) = match aux with + | Tu_id id -> id + | Tu_ty_id (_, id) -> id diff --git a/src/ast_util.mli b/src/ast_util.mli index c9869cce..4452ee3f 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -53,6 +53,13 @@ open Ast module Big_int = Nat_big_num +type mut = Immutable | Mutable + +(** [lvar] is the type of variables - they can either be registers, + local mutable or immutable variables, nullary union constructors + (i.e. None in option), or unbound identifiers *) +type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound + val no_annot : unit annot val gen_loc : Parse_ast.l -> Parse_ast.l @@ -293,3 +300,5 @@ val rename_fundef : id -> 'a fundef -> 'a fundef val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option val append_ast : 'a defs -> 'a defs -> 'a defs + +val type_union_id : type_union -> id diff --git a/src/c_backend.ml b/src/c_backend.ml index ce891e3f..c1f5ddb9 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -78,7 +78,7 @@ type aexp = and aval = | AV_lit of lit * typ - | AV_id of id * Type_check.lvar + | AV_id of id * lvar | AV_tuple of aval list | AV_C_fragment of string * typ diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml new file mode 100644 index 00000000..4a2b5cfa --- /dev/null +++ b/src/pattern_completeness.ml @@ -0,0 +1,294 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +module Big_int = Nat_big_num + +type ctx = + { lookup_id : id -> lvar; + enums : IdSet.t Bindings.t; + variants : IdSet.t Bindings.t + } + +let hex_to_bin hex = + Util.string_to_list hex + |> List.map Sail_lib.hex_char + |> List.concat + |> List.map Sail_lib.char_of_bit + |> (fun bits -> String.init (List.length bits) (List.nth bits)) + +type gpat = + | GP_lit of lit + | GP_wild + | GP_vector of gpat list + | GP_vector_concat of gpat list + | GP_tup of gpat list + | GP_list of gpat list + | GP_cons of gpat * gpat + | GP_app of (gpat Bindings.t) + | GP_record of (gpat Bindings.t) + +let rec string_of_gpat = function + | GP_lit lit -> string_of_lit lit + | GP_wild -> "_" + | GP_vector gpats -> "[" ^ Util.string_of_list ", " string_of_gpat gpats ^ "]" + | GP_vector_concat gpats -> Util.string_of_list " @ " string_of_gpat gpats + | GP_tup gpats -> "(" ^ Util.string_of_list ", " string_of_gpat gpats ^ ")" + | GP_list gpats -> "[|" ^ Util.string_of_list ", " string_of_gpat gpats ^ "|]" + | GP_cons (gpat1, gpat2) -> string_of_gpat gpat1 ^ " :: " ^ string_of_gpat gpat2 + | GP_app app -> + Util.string_of_list "|" (fun (id, gpat) -> string_of_id id ^ string_of_gpat gpat) (Bindings.bindings app) + | GP_record _ -> "GP RECORD" + +let is_wild = function + | GP_wild -> true + | _ -> false + +let rec generalize ctx (P_aux (p_aux, _) as pat) = + match p_aux with + | P_lit lit -> GP_lit lit + | P_wild -> GP_wild + | P_as (pat, _) -> generalize ctx pat + | P_typ (_, pat) -> generalize ctx pat (* This will possibly overapproximate how general P_typ is *) + | P_id id -> + begin + match ctx.lookup_id id with + | Unbound -> GP_wild + | Local (Immutable, _) -> GP_wild + | Register _ | Local (Mutable, _) -> Util.warn "Matching on register or mutable variable"; GP_wild + | Enum _ | Union _ -> GP_app (Bindings.singleton id GP_wild) + end + | P_var (pat, _) -> generalize ctx pat + | P_vector pats -> + let gpats = List.map (generalize ctx) pats in + if List.for_all is_wild gpats then GP_wild else GP_vector gpats + | P_vector_concat pats -> + let gpats = List.map (generalize ctx) pats in + if List.for_all is_wild gpats then GP_wild else GP_vector_concat gpats + | P_tup pats -> + let gpats = List.map (generalize ctx) pats in + if List.for_all is_wild gpats then GP_wild else GP_tup gpats + | P_list pats -> + let gpats = List.map (generalize ctx) pats in + if List.for_all is_wild gpats then GP_wild else GP_list gpats + | P_cons (hd_pat, tl_pat) -> + let ghd_pat = generalize ctx hd_pat in + let gtl_pat = generalize ctx tl_pat in + if is_wild ghd_pat && is_wild gtl_pat then GP_wild else GP_cons (ghd_pat, gtl_pat) + | P_app (f, pats) -> + let gpats = List.map (generalize ctx) pats in + if List.for_all is_wild gpats then + GP_app (Bindings.singleton f GP_wild) + else + GP_app (Bindings.singleton f (GP_tup gpats)) + | P_record (fpats, flag) -> + let gfpats = List.concat (List.map (generalize_fpat ctx) fpats) in + GP_record (List.fold_left (fun m (fid, gpat) -> Bindings.add fid gpat m) Bindings.empty gfpats) + +and generalize_fpat ctx (FP_aux (FP_Fpat (field_id, pat), annot)) = + let gpat = generalize ctx pat in + if is_wild gpat then [] + else + [(field_id, gpat)] + +let vector_pat bits = + let bit_pat = function + | '0' -> GP_lit (mk_lit L_zero) + | '1' -> GP_lit (mk_lit L_one) + | _ -> failwith "Invalid bit pattern" + in + GP_vector (List.map bit_pat (Util.string_to_list bits)) + +let join_bits bits1 bits2 = + let join_bit bit1 bit2 = match bit1, bit2 with + | '0', '0' -> GP_lit (mk_lit L_zero) + | '1', '1' -> GP_lit (mk_lit L_one) + | _, _ -> GP_wild + in + let joined = List.map2 join_bit (Util.string_to_list bits1) (Util.string_to_list bits2) in + if List.for_all is_wild joined then GP_wild else GP_vector joined + +(* The join_lit function takes two patterns and produces a pattern + that matches both literals *) +let rec join_lit (L_aux (l_aux1, _) as lit1) (L_aux (l_aux2, _) as lit2) = + match l_aux1, l_aux2 with + (* The only literal with type unit is the unit literal *) + | L_unit, _ -> GP_lit lit1 + | _, L_unit -> GP_lit lit2 + + (* Bit literals don't change when they're the same, become wildcard + when we match both *) + | L_zero, L_zero -> GP_lit lit1 + | L_one, L_one -> GP_lit lit1 + | L_zero, L_one -> GP_wild + | L_one, L_zero -> GP_wild + + (* Boolean literals work the same as bit literals *) + | L_false, L_false -> GP_lit lit1 + | L_true, L_true -> GP_lit lit2 + | L_false, L_true -> GP_wild + | L_true, L_false -> GP_wild + + | L_hex hex, _ -> join_lit (mk_lit (L_bin (hex_to_bin hex))) lit2 + | _, L_hex hex -> join_lit lit1 (mk_lit (L_bin (hex_to_bin hex))) + | L_bin bits1, L_bin bits2 -> join_bits bits1 bits2 + + (* The set of numbers is infinite, so no finite sequence of number + literals can match all numbers. As such we need a wildcard, so + the join lit function just returns one of the two numbers. *) + | L_num _, L_num _ -> GP_lit lit1 + + (* Strings are similar to number literals. *) + | L_string _, L_string _ -> GP_lit lit1 + + | L_real _, L_real _ -> GP_lit lit1 + + | L_undef, _ -> GP_wild + | _, L_undef -> GP_wild + + | _, _ -> + (* This shouldn't happen if both patterns are well-typed, but we + include it here to ensure that join_lit won't fail. *) + let message = + Printf.sprintf "Have two differently typed pattern literals %s and %s matching the same thing" + (string_of_lit lit1) (string_of_lit lit2) + in + Util.warn message; + GP_wild + +let rec join ctx gpat1 gpat2 = + (* prerr_endline ("Join :" ^ string_of_gpat gpat1 ^ " with " ^ string_of_gpat gpat2); *) + match gpat1, gpat2 with + | GP_wild, _ -> GP_wild + | _, GP_wild -> GP_wild + + | GP_lit lit1, GP_lit lit2 -> join_lit lit1 lit2 + + | GP_tup gpats1, GP_tup gpats2 -> + let joined = List.map2 (join ctx) gpats1 gpats2 in + if List.for_all is_wild joined then GP_wild else GP_tup joined + + | GP_lit (L_aux (L_hex hex, _)), GP_vector _ -> + join ctx (vector_pat (hex_to_bin hex)) gpat2 + | GP_lit (L_aux (L_bin bin, _)), GP_vector _ -> + join ctx (vector_pat bin) gpat2 + | GP_vector _, GP_lit (L_aux (L_hex hex, annot)) -> + join ctx gpat1 (vector_pat (hex_to_bin hex)) + | GP_vector _, GP_lit (L_aux (L_bin bin, _)) -> + join ctx gpat1 (vector_pat bin) + + | GP_vector gpats1, GP_vector gpats2 -> + let joined = List.map2 (join ctx) gpats1 gpats2 in + if List.for_all is_wild joined then GP_wild else GP_vector joined + + | GP_list gpats1, GP_list gpats2 -> + let joined = List.map2 (join ctx) gpats1 gpats2 in + if List.for_all is_wild joined then GP_wild else GP_list joined + + | GP_app ctors1, GP_app ctors2 -> + let ctor_merge ctor args1 args2 = + match args1, args2 with + | None, None -> None + | Some args1, None -> Some args1 + | None, Some args2 -> Some args2 + | Some args1, Some args2 -> + assert false + in + let ctors = Bindings.merge ctor_merge ctors1 ctors2 in + if Bindings.for_all (fun _ gpat -> is_wild gpat) ctors then + let ids = IdSet.of_list (List.map fst (Bindings.bindings ctors)) in + let enums = List.map snd (Bindings.bindings ctx.enums) in + let variants = List.map snd (Bindings.bindings ctx.variants) in + if List.exists (fun ids' -> IdSet.equal ids ids') (enums @ variants) then + GP_wild + else + GP_app ctors + else + GP_app ctors + + | _, _ -> GP_wild + +let combine ctx gpat (l, pat) = + match gpat, generalize ctx pat with + | GP_wild, GP_app _ -> + (* This warning liable to false positives as join returns a + pattern that overapproximates what can match, so we only + report when the second match is a constructor. *) + Util.warn (Printf.sprintf "Possible redundant pattern match at %s\n" (Reporting_basic.loc_to_string l)); + GP_wild + | _, gpat' -> join ctx gpat gpat' + +let rec cases_to_pats = function + | [] -> [] + | Pat_aux (Pat_exp (P_aux (_, (l, _)) as pat, _), _) :: cases -> (l, pat) :: cases_to_pats cases + (* We don't consider guarded cases *) + | Pat_aux (Pat_when _, _) :: cases -> cases_to_pats cases + +(* Just highlight the match keyword and no the whole match block. *) +let shrink_loc = function + | Parse_ast.Range (n, m) -> + Lexing.(Parse_ast.Range (n, { n with pos_cnum = n.pos_cnum + 5 })) + | l -> l + +let check l ctx cases = + match cases_to_pats cases with + | [] -> Util.warn (Printf.sprintf "No non-guarded patterns at %s\n" (Reporting_basic.loc_to_string (shrink_loc l))) + | (_, pat) :: pats -> + let top_pat = List.fold_left (combine ctx) (generalize ctx pat) pats in + if is_wild top_pat then + () + else + let message = + Printf.sprintf "Possible incomplete pattern match at %s\n\nMost general matched pattern is %s\n" + (Reporting_basic.loc_to_string (shrink_loc l)) + (string_of_gpat top_pat |> Util.cyan |> Util.clear) + in + Util.warn message diff --git a/src/sail.ml b/src/sail.ml index d5ef684b..d6d5eebc 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -78,6 +78,9 @@ let options = Arg.align ([ Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen; Arg.String (fun s -> opt_interactive_script := Some s)], "<filename> start interactive interpreter and execute commands in script"); + ( "-no_warn", + Arg.Clear Util.opt_warnings, + " do not print warnings"); ( "-ocaml", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], " output an OCaml translated version of the input"); diff --git a/src/type_check.ml b/src/type_check.ml index d4920c5a..41438592 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -285,10 +285,6 @@ let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_ (* 2. Environment *) (**************************************************************************) -type mut = Immutable | Mutable - -type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound - module Env : sig type t val add_val_spec : id -> typquant * typ -> t -> t @@ -357,6 +353,8 @@ module Env : sig (* This must not be exported, initial_env sets up a correct initial environment. *) val empty : t + + val pattern_completeness_ctx : t -> Pattern_completeness.ctx end = struct type t = { top_val_specs : (typquant * typ) Bindings.t; @@ -927,6 +925,12 @@ end = struct { env with poly_undefineds = true } let polymorphic_undefineds env = env.poly_undefineds + + let pattern_completeness_ctx env = + { Pattern_completeness.lookup_id = (fun id -> lookup_id id env); + Pattern_completeness.enums = env.enums; + Pattern_completeness.variants = Bindings.map (fun (_, tus) -> IdSet.of_list (List.map type_union_id tus)) env.variants + } end @@ -2053,6 +2057,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ annot_exp (E_block (check_block l env exps typ)) typ end | E_case (exp, cases), _ -> + Pattern_completeness.check l (Env.pattern_completeness_ctx env) cases; let inferred_exp = irule infer_exp env exp in let inferred_typ = typ_of inferred_exp in annot_exp (E_case (inferred_exp, List.map (fun case -> check_case env inferred_typ case typ) cases)) typ diff --git a/src/type_check.mli b/src/type_check.mli index b904769f..340cf6e0 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -63,13 +63,6 @@ val opt_tc_debug : int ref re-writer passes, so it should only be used for debugging. *) val opt_no_effects : bool ref -type mut = Immutable | Mutable - -(** [lvar] is the type of variables - they can either be registers, - local mutable or immutable variables, nullary union constructors - (i.e. None in option), or unbound identifiers *) -type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound - (** {2 Type errors} *) type type_error = diff --git a/src/util.ml b/src/util.ml index 6d4b3726..e2dc9b9f 100644 --- a/src/util.ml +++ b/src/util.ml @@ -94,6 +94,8 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) +let opt_warnings = ref true + let rec last = function | [x] -> x | _ :: xs -> last xs @@ -414,4 +416,7 @@ let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.ma let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str)) -let warn str = prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str) +let warn str = + if !opt_warnings then + prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str) + else () diff --git a/src/util.mli b/src/util.mli index c9eae02f..2b4d2e93 100644 --- a/src/util.mli +++ b/src/util.mli @@ -51,6 +51,8 @@ (* Last element of a list *) val last : 'a list -> 'a +val opt_warnings : bool ref + val butlast : 'a list -> 'a list (** Mixed useful things *) @@ -241,6 +243,6 @@ val blue : string -> string val clear : string -> string val warn : string -> unit - + val zencode_string : string -> string val zencode_upper_string : string -> string |