diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 8 | ||||
| -rw-r--r-- | src/initial_check.ml | 1 | ||||
| -rw-r--r-- | src/pretty_print_sail2.ml | 2 | ||||
| -rw-r--r-- | src/process_file.ml | 2 | ||||
| -rw-r--r-- | src/trace_viewer/index.html | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 41 |
6 files changed, 48 insertions, 8 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 92628014..707ec93c 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -769,9 +769,11 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = wrap (E_app (prepend_id "undefined_" id, List.concat (List.map (undefined_of_typ_args mwords l annot) args))) typ | Typ_var kid -> - (* FIXME: bit of a hack, need to add a restriction to how - polymorphic undefined can be in the type checker to - guarantee this always works. *) + (* Undefined monomorphism restriction in the type checker should + guarantee that the typ_(kid) parameter was always one created + in an undefined_(type) function created in + initial_check.ml. i.e. the rewriter should only encounter this + case when re-writing those functions. *) wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ | Typ_fn _ -> assert false and undefined_of_typ_args mwords l annot (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = diff --git a/src/initial_check.ml b/src/initial_check.ml index b33d90f5..2ccfee04 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -968,6 +968,7 @@ let generate_undefineds vs_ids (Defs defs) = gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}"; gen_vs (mk_id "undefined_real") "unit -> real effect {undef}"; gen_vs (mk_id "undefined_string") "unit -> string effect {undef}"; + gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; (* FIXME: How to handle inc/dec order correctly? *) gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}"; diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 39fc25d3..efcfc8b9 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -181,7 +181,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps) | E_if (if_exp, then_exp, else_exp) -> group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp]) - | E_list exps -> string "E_list" + | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]" | E_cons (exp1, exp2) -> string "E_cons" | E_record fexps -> string "E_record" | E_loop (While, cond, exp) -> diff --git a/src/process_file.ml b/src/process_file.ml index aea53ca7..b95d54f7 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -245,7 +245,7 @@ let rewrite_step defs (name,rewriter) = let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in output "" Lem_ast_out [filename, defs]; let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in - Pretty_print_sail.pp_defs ot defs; + Pretty_print_sail2.pp_defs ot defs; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) end diff --git a/src/trace_viewer/index.html b/src/trace_viewer/index.html index 75c5e035..9efcca56 100644 --- a/src/trace_viewer/index.html +++ b/src/trace_viewer/index.html @@ -2,7 +2,7 @@ <html> <head> <meta charset="UTF-8"> - <title>Sail Log Viewer</title> + <title>Sail Trace Viewer</title> <script type="text/javascript"> var exports = {} </script> diff --git a/src/type_check.ml b/src/type_check.ml index 6489195a..aede9c67 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -387,6 +387,8 @@ module Env : sig val no_casts : t -> t val enable_casts : t -> t val add_cast : id -> t -> t + val allow_polymorphic_undefineds : t -> t + val polymorphic_undefineds : t -> bool val lookup_id : id -> t -> lvar val fresh_kid : ?kid:kid -> t -> kid val expand_synonyms : t -> typ -> typ @@ -413,7 +415,8 @@ end = struct allow_casts : bool; constraints : n_constraint list; default_order : order option; - ret_typ : typ option + ret_typ : typ option; + poly_undefineds : bool } let empty = @@ -437,6 +440,7 @@ end = struct constraints = []; default_order = None; ret_typ = None; + poly_undefineds = false; } let counter = ref 0 @@ -892,6 +896,11 @@ end = struct | targ -> rewrap targ in aux (expand_synonyms env typ) + let allow_polymorphic_undefineds env = + { env with poly_undefineds = true } + + let polymorphic_undefineds env = env.poly_undefineds + end @@ -972,6 +981,21 @@ let destruct_vector env typ = in destruct_vector' (Env.expand_synonyms env typ) +let rec is_typ_monomorphic (Typ_aux (typ, _)) = + match typ with + | Typ_wild -> assert false (* Typ_wild is bad in general *) + | Typ_id _ -> true + | Typ_tup typs -> List.for_all is_typ_monomorphic typs + | Typ_app (id, args) -> List.for_all is_typ_arg_monomorphic args + | Typ_fn (typ1, typ2, _) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2 + | Typ_exist _ | Typ_var _ -> false +and is_typ_arg_monomorphic (Typ_arg_aux (arg, _)) = + match arg with + | Typ_arg_nexp _ -> true + | Typ_arg_typ typ -> is_typ_monomorphic typ + | Typ_arg_order (Ord_aux (Ord_dec, _)) | Typ_arg_order (Ord_aux (Ord_inc, _)) -> true + | Typ_arg_order (Ord_aux (Ord_var _, _)) -> false + (**************************************************************************) (* 3. Subtyping and constraint solving *) (**************************************************************************) @@ -2057,7 +2081,9 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ if prove env (nc_eq (nconstant (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ else typ_error l "List length didn't match" (* FIXME: improve error message *) | E_lit (L_aux (L_undef, _) as lit), _ -> - annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef]) + if is_typ_monomorphic typ || Env.polymorphic_undefineds env + then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef]) + else typ_error l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction") (* This rule allows registers of type t to be passed by name with type register<t>*) | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "register" && Env.is_register reg env -> @@ -3171,6 +3197,17 @@ let check_funcl env (FCL_aux (FCL_Funcl (id, pat, exp), (l, _))) typ = begin let typed_pat, env = bind_pat env (strip_pat pat) typ_arg in let env = Env.add_ret_typ typ_ret env in + (* We want to forbid polymorphic undefined values in all cases, + except when type checking the specific undefined_(type) + functions created by the -undefined_gen functions in + initial_check.ml. Only in these functions will the rewriter + be able to correctly re-write the polymorphic undefineds + (due to the specific form the functions have *) + let env = + if Str.string_match (Str.regexp_string "undefined_") (string_of_id id) 0 + then Env.allow_polymorphic_undefineds env + else env + in let exp = propagate_exp_effect (crule check_exp env (strip_exp exp) typ_ret) in FCL_aux (FCL_Funcl (id, typed_pat, exp), (l, Some (env, typ, effect_of exp))) end |