summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/ast_util.ml8
-rw-r--r--src/initial_check.ml1
-rw-r--r--src/pretty_print_sail2.ml2
-rw-r--r--src/process_file.ml2
-rw-r--r--src/trace_viewer/index.html2
-rw-r--r--src/type_check.ml41
-rw-r--r--test/typecheck/pass/exist_pattern.sail4
-rw-r--r--test/typecheck/pass/nondet_assert.sail2
8 files changed, 53 insertions, 9 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
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
index 46913de4..4561074a 100644
--- a/test/typecheck/pass/exist_pattern.sail
+++ b/test/typecheck/pass/exist_pattern.sail
@@ -4,6 +4,10 @@ register nat n
register nat x
register nat y
+val (int, int) -> bool effect pure eq_int
+
+overload (deinfix ==) [eq_int]
+
typedef wordsize = exist 'n, 'n IN {8,16,32}. [|'n|]
let (wordsize) word = ([|8|]) 8
diff --git a/test/typecheck/pass/nondet_assert.sail b/test/typecheck/pass/nondet_assert.sail
index e90bb6f2..501432d3 100644
--- a/test/typecheck/pass/nondet_assert.sail
+++ b/test/typecheck/pass/nondet_assert.sail
@@ -1,7 +1,7 @@
register int z
-val unit -> int effect {wreg, rreg} test
+val unit -> int effect {wreg, rreg, escape} test
function int test () = {
nondet {
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 14:13:13 +0000