diff --git a/CHANGELOG.md b/CHANGELOG.md index dd62087a9..285c8bbc9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,27 @@ Changelog ========= +Sail 0.19 +--------- + +##### Stricter bitvector type indexing + +Stricter indexing for bitvector types. Previous versions of Sail +treated `bitvector('n)` as uninhabited if `'n < 0`, but otherwise +permitted such bitvector types in signatures. Now the type +`bitvector('n)` is only well-formed if `'n >= 0`. This is a breaking +change, as some previously permitted definitions are now rejected +without additional constraints. However Sail has a new kind `Nat` +which allows it to infer these `>= 0` constraints when explicit type +variables are ommited, so in a function signature +``` +val foo : forall 'n. bits('n) -> bool +``` +the `'n` type variable will be inferred as: +``` +val foo : forall ('n : Nat). bits('n) -> bool +``` + Sail 0.18 --------- diff --git a/lib/concurrency_interface/read_write.sail b/lib/concurrency_interface/read_write.sail index dbd33ce96..146adaafe 100644 --- a/lib/concurrency_interface/read_write.sail +++ b/lib/concurrency_interface/read_write.sail @@ -86,7 +86,7 @@ union Access_kind('arch_ak : Type) = { $option -lem_extern_type Mem_read_request $option -coq_extern_type Mem_read_request struct Mem_read_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type, - 'arch_ak: Type), 'n > 0 = { + 'arch_ak : Type), 'n > 0 & 'vasize >= 0 = { access_kind : Access_kind('arch_ak), // There may not always be a virtual address, e.g. when translation is off. // Additionally, translate reads don't have a (VA, PA) pair in the @@ -182,7 +182,7 @@ with $option -lem_extern_type Mem_write_request $option -coq_extern_type Mem_write_request struct Mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type, - 'arch_ak : Type), 'n > 0 = { + 'arch_ak : Type), 'n > 0 & 'vasize >= 0 = { access_kind : Access_kind('arch_ak), va : option(bits('vasize)), pa : 'pa, diff --git a/lib/vector.sail b/lib/vector.sail index 58245422f..aa1caf059 100644 --- a/lib/vector.sail +++ b/lib/vector.sail @@ -53,7 +53,7 @@ $endif $include -type bits('n : Int) = bitvector('n) +type bits('n) = bitvector('n) val eq_bits = pure { ocaml: "eq_list", @@ -129,7 +129,7 @@ function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail overload operator ^ = {sail_mask} -val bitvector_concat = pure {ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec", _: "append"} : forall ('n : Int) ('m : Int). +val bitvector_concat = pure {ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec", _: "append"} : forall 'n 'm. (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} @@ -316,7 +316,7 @@ val slice = pure "slice_inc" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm. (bits('m), int('o), int('n)) -> bits('n) $endif -val replicate_bits = pure "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm) +val replicate_bits = pure "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), int('m)) -> bits('n * 'm) val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) function slice_mask(n,i,l) = diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 380088234..e559ff6cb 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -274,6 +274,7 @@ let rec options = ("-no_warn", Arg.Clear Reporting.opt_warnings, " do not print warnings"); ("-all_warnings", Arg.Set Reporting.opt_all_warnings, " print all warning messages"); ("-strict_var", Arg.Set Type_check.opt_strict_var, " require var expressions for variable declarations"); + ("-strict_bitvector", Arg.Set Initial_check.opt_strict_bitvector, " require bitvectors to be indexed by naturals"); ("-plugin", Arg.String (fun plugin -> load_plugin options plugin), " load a Sail plugin"); ("-just_check", Arg.Set opt_just_check, " terminate immediately after typechecking"); ("-memo_z3", Arg.Set opt_memo_z3, " memoize calls to z3, improving performance when typechecking repeatedly"); diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index 19574989f..489c30bd2 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -788,6 +788,12 @@ let quant_map_items f = function | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l) | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l) +let quant_fold_map_items f acc = function + | TypQ_aux (TypQ_no_forall, l) -> (acc, TypQ_aux (TypQ_no_forall, l)) + | TypQ_aux (TypQ_tq qis, l) -> + let acc, qis = Util.fold_left_map f acc qis in + (acc, TypQ_aux (TypQ_tq qis, l)) + let is_quant_kopt = function QI_aux (QI_id _, _) -> true | _ -> false let is_quant_constraint = function QI_aux (QI_constraint _, _) -> true | _ -> false diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index cf1d9dc2d..fb7ed7c10 100644 --- a/src/lib/ast_util.mli +++ b/src/lib/ast_util.mli @@ -414,6 +414,7 @@ val quant_items : typquant -> quant_item list val quant_kopts : typquant -> kinded_id list val quant_split : typquant -> kinded_id list * n_constraint list val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant +val quant_fold_map_items : ('acc -> quant_item -> 'acc * quant_item) -> 'acc -> typquant -> 'acc * typquant val is_quant_kopt : quant_item -> bool val is_quant_constraint : quant_item -> bool diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml index 8f84bd8be..6e66e15e5 100644 --- a/src/lib/chunk_ast.ml +++ b/src/lib/chunk_ast.ml @@ -460,7 +460,7 @@ let pop_trailing_comment ?space:(n = 0) comments chunks line_num = end let string_of_kind (K_aux (k, _)) = - match k with K_type -> "Type" | K_int -> "Int" | K_order -> "Order" | K_bool -> "Bool" + match k with K_type -> "Type" | K_int -> "Int" | K_nat -> "Nat" | K_order -> "Order" | K_bool -> "Bool" (* Right now, let's just assume we never break up kinded-identifiers *) let chunk_of_kopt (KOpt_aux (KOpt_kind (special, vars, kind, _), l)) = diff --git a/src/lib/constant_propagation.ml b/src/lib/constant_propagation.ml index 162a24109..99be000de 100644 --- a/src/lib/constant_propagation.ml +++ b/src/lib/constant_propagation.ml @@ -268,7 +268,7 @@ let const_props target ast = let interpreter_istate = (* Do not interpret undefined_X functions *) let open Interpreter in - let undefined_builtin_ids = ids_of_defs Initial_check.undefined_builtin_val_specs in + let undefined_builtin_ids = ids_of_defs (Initial_check.undefined_builtin_val_specs ()) in let remove_primop id = StringMap.remove (string_of_id id) in let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in let lstate, gstate = Constant_fold.initial_state ast Type_check.initial_env in diff --git a/src/lib/constraint.ml b/src/lib/constraint.ml index 195b765ba..f43e6c390 100644 --- a/src/lib/constraint.ml +++ b/src/lib/constraint.ml @@ -64,7 +64,7 @@ let cvc4_solver = { command = "cvc4"; args = (fun input -> [| "-L"; "smtlib2"; "--tlimit=2000"; input |]); - header = "(set-logic QF_UFNIA)\n"; + header = "(set-logic UFNIA)\n"; footer = ""; negative_literals = false; uninterpret_power = true; @@ -243,9 +243,14 @@ let to_smt l abstract vars constr = (abstract_decs @ var_decs vars, smt_constr, smt_var, !exponentials) let sailexp_concrete n = - List.init (n + 1) (fun i -> - sfun "=" [sfun "sailexp" [Atom (string_of_int i)]; Atom (Big_int.to_string (Big_int.pow_int_positive 2 i))] - ) + sfun "forall" + [ + List [List [Atom "n"; Atom "Int"]]; + sfun "=>" [sfun ">=" [Atom "n"; Atom "0"]; sfun ">=" [sfun "sailexp" [Atom "n"]; Atom "1"]]; + ] + :: List.init (n + 1) (fun i -> + sfun "=" [sfun "sailexp" [Atom (string_of_int i)]; Atom (Big_int.to_string (Big_int.pow_int_positive 2 i))] + ) let smtlib_of_constraints ?(get_model = false) l abstract vars extra constr : string * (kid -> sexpr * bool) * sexpr list = diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index 8862464e7..1eeb8c49a 100644 --- a/src/lib/initial_check.ml +++ b/src/lib/initial_check.ml @@ -57,6 +57,7 @@ module P = Parse_ast let opt_fast_undefined = ref false let opt_magic_hash = ref false let opt_abstract_types = ref false +let opt_strict_bitvector = ref false let abstract_type_error = "Abstract types are currently experimental, use the --abstract-types flag to enable" @@ -68,7 +69,7 @@ module StringMap = Map.Make (String) $sail_internal marked files in the prelude. *) let reserved_type_ids = IdSet.of_list [mk_id "result"; mk_id "option"] -type type_constructor = kind_aux option list * kind_aux +type type_constructor = P.kind_aux list * P.kind_aux type ctx = { kinds : (kind_aux * P.l) KBindings.t; @@ -147,19 +148,47 @@ let string_contains str char = true with Not_found -> false +let to_ast_kind_aux = function + | P.K_type -> Some K_type + | P.K_int -> Some K_int + | P.K_nat -> Some K_int + | P.K_order -> None + | P.K_bool -> Some K_bool + let to_ast_kind (P.K_aux (k, l)) = match k with | P.K_type -> Some (K_aux (K_type, l)) | P.K_int -> Some (K_aux (K_int, l)) + | P.K_nat -> Some (K_aux (K_int, l)) | P.K_order -> None | P.K_bool -> Some (K_aux (K_bool, l)) +let parse_kind_constraint l v = function + | P.K_nat when !opt_strict_bitvector -> + let v = Nexp_aux (Nexp_var v, kid_loc v) in + Some (NC_aux (NC_ge (v, Nexp_aux (Nexp_constant Big_int.zero, l)), l)) + | _ -> None + +let not_order_kind = function P.K_order -> false | _ -> true + +let filter_order_kinds kinds = List.filter not_order_kind kinds + let string_of_parse_kind_aux = function | P.K_order -> "Order" | P.K_int -> "Int" + | P.K_nat -> if !opt_strict_bitvector then "Nat" else "Int" | P.K_bool -> "Bool" | P.K_type -> "Type" +(* Used for error messages involving lists of kinds *) +let format_parse_kind_aux_list = function + | [kind] -> string_of_parse_kind_aux kind + | kinds -> "(" ^ Util.string_of_list ", " string_of_parse_kind_aux kinds ^ ")" + +let format_kind_aux_list = function + | [kind] -> string_of_kind_aux kind + | kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")" + let to_parse_kind = function | Some K_int -> P.K_int | Some K_bool -> P.K_bool @@ -295,11 +324,6 @@ let parse_infix_atyp ctx = function let to_ast_var (P.Kid_aux (P.Var v, l)) = Kid_aux (Var v, l) -(* Used for error messages involving lists of kinds *) -let format_kind_aux_list = function - | [kind] -> string_of_kind_aux kind - | kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")" - (** The [KindInference] module implements a type-inference module for kind (types of types). @@ -352,9 +376,10 @@ module KindInference = struct in ((), { env with sets = go env.sets }) - let check_same_kind kind l kind' l' = + let unify_kind kind l kind' l' = match (kind, kind') with - | P.K_int, P.K_int | P.K_bool, P.K_bool | P.K_type, P.K_type | P.K_order, P.K_order -> () + | P.K_nat, P.K_int | P.K_int, P.K_nat -> P.K_nat + | P.K_int, P.K_int | P.K_nat, P.K_nat | P.K_bool, P.K_bool | P.K_type, P.K_type | P.K_order, P.K_order -> kind | _ -> raise (Reporting.err_typ @@ -369,8 +394,8 @@ module KindInference = struct | Unknown, Unknown -> Unknown | Unknown, known | known, Unknown -> known | Known (kind, l), Known (kind', l') -> - check_same_kind kind l kind' l'; - Known (kind, l) + let kind'' = unify_kind kind l kind' l' in + Known (kind'', l) let unify n m env = let n_sets, other_sets = List.partition (fun (set, _) -> IntSet.mem n set) env.sets in @@ -421,7 +446,7 @@ module KindInference = struct let n_set, nk = List.hd n_sets in ((), { env with sets = (n_set, merge_unification_kind nk (Known (kind, l))) :: env.sets }) | Kind (kind', l') -> - check_same_kind kind l kind' l'; + let _ = unify_kind kind l kind' l' in ((), env) let atyp_loc (P.ATyp_aux (_, l)) = l @@ -434,7 +459,7 @@ module KindInference = struct let* () = match Bindings.find_opt id' ctx.type_constructors with | None -> return () - | Some ([], ret_kind) -> resolve ~at:l (to_parse_kind (Some ret_kind)) ik + | Some ([], ret_kind) -> resolve ~at:l ret_kind ik | Some (kind_opts, _) -> raise (ksprintf (Reporting.err_typ l) "%s is not a constant" (string_of_id id')) in return atyp @@ -488,19 +513,35 @@ module KindInference = struct let* arg = check ctx arg (Kind (P.K_bool, atyp_loc arg)) in wrap (P.ATyp_app (id, [arg])) | P.ATyp_sum (t1, t2) -> - let* t1 = check ctx t1 ik in - let* t2 = check ctx t2 ik in + let* () = resolve ~at:l K_int ik in + let* t1 = check ctx t1 (Kind (P.K_int, atyp_loc t1)) in + let* t2 = check ctx t2 (Kind (P.K_int, atyp_loc t2)) in wrap (P.ATyp_sum (t1, t2)) - | P.ATyp_times (t1, t2) -> - let* t1 = check ctx t1 ik in - let* t2 = check ctx t2 ik in - wrap (P.ATyp_times (t1, t2)) + | P.ATyp_times (t1, t2) -> begin + (* Special case N * M when either N or M is a constant > 0, in + which case we can infer that if N * M is a Nat then the + non-constant case is also a Nat *) + match (t1, t2) with + | P.ATyp_aux (P.ATyp_lit (P.L_aux (P.L_num n, _)), _), _ when Big_int.greater n Big_int.zero -> + let* t2 = check ctx t2 ik in + wrap (P.ATyp_times (t1, t2)) + | _, P.ATyp_aux (P.ATyp_lit (P.L_aux (P.L_num n, _)), _) when Big_int.greater n Big_int.zero -> + let* t1 = check ctx t1 ik in + wrap (P.ATyp_times (t1, t2)) + | _ -> + let* () = resolve ~at:l K_int ik in + let* t1 = check ctx t1 (Kind (P.K_int, atyp_loc t1)) in + let* t2 = check ctx t2 (Kind (P.K_int, atyp_loc t2)) in + wrap (P.ATyp_times (t1, t2)) + end | P.ATyp_minus (t1, t2) -> - let* t1 = check ctx t1 ik in - let* t2 = check ctx t2 ik in + let* () = resolve ~at:l K_int ik in + let* t1 = check ctx t1 (Kind (P.K_int, atyp_loc t1)) in + let* t2 = check ctx t2 (Kind (P.K_int, atyp_loc t2)) in wrap (P.ATyp_minus (t1, t2)) | P.ATyp_exp t -> - let* t = check ctx t ik in + let* () = resolve ~at:l K_int ik in + let* t = check ctx t (Kind (P.K_int, atyp_loc t)) in wrap (P.ATyp_exp t) | P.ATyp_neg t -> let* t = check ctx t ik in @@ -511,23 +552,19 @@ module KindInference = struct match Bindings.find_opt id' ctx.type_constructors with | None -> raise (ksprintf (Reporting.err_typ l) "Unknown type level operator or function %s" (string_of_id id')) - | Some (kind_opts, ret_kind) -> - let* () = resolve ~at:l (to_parse_kind (Some ret_kind)) ik in + | Some (kinds, ret_kind) -> + let* () = resolve ~at:l ret_kind ik in let args_len = List.length args in - let kind_opts = - if args_len = List.length kind_opts then kind_opts else List.filter Option.is_some kind_opts - in - if List.compare_lengths args kind_opts <> 0 then + let kinds = if args_len = List.length kinds then kinds else filter_order_kinds kinds in + if List.compare_lengths args kinds <> 0 then raise (Reporting.err_typ l (sprintf "%s : %s -> Type expected %d arguments, given %d" (string_of_id id') - (format_kind_aux_list (Util.option_these kind_opts)) - (List.length kind_opts) (List.length args) + (format_parse_kind_aux_list (filter_order_kinds kinds)) + (List.length kinds) (List.length args) ) ); - mapM - (function arg, kind -> check ctx arg (Kind (to_parse_kind kind, id_loc id'))) - (List.combine args kind_opts) + mapM (function arg, kind -> check ctx arg (Kind (kind, id_loc id'))) (List.combine args kinds) in wrap (P.ATyp_app (id, args)) | P.ATyp_lit (P.L_aux (aux, _)) -> @@ -761,11 +798,25 @@ end module ConvertType = struct let to_ast_kopts kenv ctx (P.KOpt_aux (aux, l)) = - let mk_kopt v k = + let open Util.Option_monad in + let mk_kopt v (P.K_aux (aux, _) as k) = let v = to_ast_var v in - Option.map - (fun k -> (KOpt_aux (KOpt_kind (k, v), l), { ctx with kinds = KBindings.add v (unaux_kind k, l) ctx.kinds })) - (to_ast_kind k) + let* k = to_ast_kind k in + Some + ( KOpt_aux (KOpt_kind (k, v), l), + parse_kind_constraint l v aux, + { ctx with kinds = KBindings.add v (unaux_kind k, l) ctx.kinds } + ) + in + let fold_vars vs k = + List.fold_left + (fun (kopts, constrs, ctx) v -> + match mk_kopt v k with + | Some (kopt, None, ctx) -> (kopt :: kopts, constrs, ctx) + | Some (kopt, Some constr, ctx) -> (kopt :: kopts, constr :: constrs, ctx) + | None -> (kopts, constrs, ctx) + ) + ([], [], ctx) vs in match aux with | P.KOpt_kind (attr, vs, None, Some u) -> @@ -774,30 +825,26 @@ module ConvertType = struct | Some k -> P.K_aux (k, gen_loc l) | None -> raise (Reporting.err_typ l "Could not infer Kind for this type variable") in - ( List.fold_left - (fun (kopts, ctx) v -> - match mk_kopt v k with Some (kopt, ctx) -> (kopt :: kopts, ctx) | None -> (kopts, ctx) - ) - ([], ctx) vs, - attr - ) + (fold_vars vs k, attr) | P.KOpt_kind (attr, vs, None, None) -> let k = P.K_aux (P.K_int, gen_loc l) in - ( List.fold_left - (fun (kopts, ctx) v -> - match mk_kopt v k with Some (kopt, ctx) -> (kopt :: kopts, ctx) | None -> (kopts, ctx) - ) - ([], ctx) vs, - attr - ) - | P.KOpt_kind (attr, vs, Some k, _) -> - ( List.fold_left - (fun (kopts, ctx) v -> - match mk_kopt v k with Some (kopt, ctx) -> (kopt :: kopts, ctx) | None -> (kopts, ctx) - ) - ([], ctx) vs, - attr - ) + (fold_vars vs k, attr) + | P.KOpt_kind (attr, vs, Some k, _) -> (fold_vars vs k, attr) + + let get_inference_kinds kenv = function + | P.TypQ_aux (P.TypQ_no_forall, _) -> [] + | P.TypQ_aux (P.TypQ_tq qis, _) -> + let qi_kinds = function + | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, vs, None, Some u), l)), _) -> begin + match KindInference.get_kind ~at:l u kenv with + | Some k -> List.init (List.length vs) (fun _ -> k) + | None -> raise (Reporting.err_typ l "Could not infer Kind for this type variable") + end + | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, vs, Some (P.K_aux (k, _)), _), _)), _) -> + List.init (List.length vs) (fun _ -> k) + | _ -> [] + in + List.concat (List.map qi_kinds qis) let rec to_ast_typ kenv ctx atyp = let (P.ATyp_aux (aux, l)) = parse_infix_atyp ctx atyp in @@ -826,7 +873,8 @@ module ConvertType = struct match Bindings.find_opt id ctx.type_constructors with | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id))) | Some (kinds, _) -> - let non_order_kinds = Util.option_these kinds in + let non_order_kinds = List.filter_map to_ast_kind_aux kinds in + let kinds = List.map to_ast_kind_aux kinds in let args_len = List.length args in if args_len = List.length non_order_kinds then Typ_aux (Typ_app (id, List.map2 (to_ast_typ_arg kenv ctx) args non_order_kinds), l) @@ -851,7 +899,7 @@ module ConvertType = struct let kopts, ctx = List.fold_right (fun kopt (kopts, ctx) -> - let (kopts', ctx), attr = to_ast_kopts kenv ctx kopt in + let (kopts', _, ctx), attr = to_ast_kopts kenv ctx kopt in match attr with | None -> (kopts' @ kopts, ctx) | Some attr -> @@ -931,7 +979,7 @@ module ConvertType = struct match Bindings.find_opt id ctx.type_constructors with | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id))) | Some (kinds, _) -> - let non_order_kinds = Util.option_these kinds in + let non_order_kinds = List.filter_map to_ast_kind_aux kinds in if List.length non_order_kinds = 2 then NC_app (id, List.map2 (to_ast_typ_arg kenv ctx) [t1; t2] non_order_kinds) else @@ -949,7 +997,7 @@ module ConvertType = struct match Bindings.find_opt id ctx.type_constructors with | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id))) | Some (kinds, _) -> - let non_order_kinds = Util.option_these kinds in + let non_order_kinds = List.filter_map to_ast_kind_aux kinds in if List.length args = List.length non_order_kinds then NC_app (id, List.map2 (to_ast_typ_arg kenv ctx) args non_order_kinds) else @@ -972,15 +1020,17 @@ module ConvertType = struct let to_ast_quant_items kenv ctx (P.QI_aux (aux, l)) = match aux with | P.QI_constraint nc -> ([QI_aux (QI_constraint (to_ast_constraint kenv ctx nc), l)], ctx) - | P.QI_id kopt -> ( - let (kopts, ctx), attr = to_ast_kopts kenv ctx kopt in - match attr with - | Some "constant" -> - Reporting.warn "Deprecated" l "constant type variable attribute no longer used"; - (List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx) - | Some attr -> raise (Reporting.err_typ l (sprintf "Unknown attribute %s" attr)) - | None -> (List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx) - ) + | P.QI_id kopt -> + let (kopts, constrs, ctx), attr = to_ast_kopts kenv ctx kopt in + begin + match attr with + | Some "constant" -> Reporting.warn "Deprecated" l "constant type variable attribute no longer used" + | Some attr -> raise (Reporting.err_typ l (sprintf "Unknown attribute %s" attr)) + | None -> () + end; + ( List.map (fun c -> QI_aux (QI_constraint c, l)) constrs @ List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, + ctx + ) let to_ast_typquant kenv ctx (P.TypQ_aux (aux, l)) = match aux with @@ -1049,12 +1099,13 @@ let to_ast_type_union = ConvertType.to_ast_type_union KindInference.initial_env let to_ast_bind ctx typq atyp kind_opt = let open KindInference in let (typq, atyp, kind), kenv = check_bind ctx typq atyp kind_opt initial_env in + let inference_kinds = ConvertType.get_inference_kinds kenv typq in let typq, ctx = ConvertType.to_ast_typquant kenv ctx typq in match to_ast_kind kind with | None -> None | Some kind -> let typ_arg = ConvertType.to_ast_typ_arg kenv ctx atyp (unaux_kind kind) in - Some (typq, typ_arg, kind) + Some (typq, typ_arg, kind, inference_kinds) let to_ast_typschm ctx (P.TypSchm_aux (P.TypSchm_ts (typq, typ), l)) = let open KindInference in @@ -1393,7 +1444,7 @@ let to_ast_outcome ctx (ev : P.outcome_spec) : outcome_spec ctx_out = let outcome_args, inner_ctx = List.fold_left (fun (args, ctx) arg -> - let (arg, ctx), _ = to_ast_kopts ctx arg in + let (arg, _, ctx), _ = to_ast_kopts ctx arg in (arg @ args, ctx) ) ([], ctx) outcome_args @@ -1413,8 +1464,8 @@ let rec to_ast_range ctx (P.BF_aux (r, l)) = ) let add_constructor id typq kind ctx = - let kinds = List.map (fun kopt -> Some (unaux_kind (kopt_kind kopt))) (quant_kopts typq) in - { ctx with type_constructors = Bindings.add id (kinds, kind) ctx.type_constructors } + let kinds = List.map (fun kopt -> to_parse_kind (Some (unaux_kind (kopt_kind kopt)))) (quant_kopts typq) in + { ctx with type_constructors = Bindings.add id (kinds, to_parse_kind (Some kind)) ctx.type_constructors } let anon_rec_constructor_typ record_id = function | P.TypQ_aux (P.TypQ_no_forall, l) -> P.ATyp_aux (P.ATyp_id record_id, Generated l) @@ -1564,9 +1615,13 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_ let id = to_ast_reserved_type_id ctx id in begin match to_ast_bind ctx typq atyp kind_opt with - | Some (typq, typ_arg, kind) -> + | Some (typq, typ_arg, kind, inference_kinds) -> ( [DEF_aux (DEF_type (TD_aux (TD_abbrev (id, typq, typ_arg), (l, empty_uannot))), def_annot)], - add_constructor id typq (unaux_kind kind) ctx + { + ctx with + type_constructors = + Bindings.add id (inference_kinds, to_parse_kind (Some (unaux_kind kind))) ctx.type_constructors; + } ) | None -> raise @@ -1608,11 +1663,11 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_ ) | P.TD_enum (id, fns, enums) -> let id = to_ast_reserved_type_id ctx id in - let ctx = { ctx with type_constructors = Bindings.add id ([], K_type) ctx.type_constructors } in + let ctx = { ctx with type_constructors = Bindings.add id ([], P.K_type) ctx.type_constructors } in let fns = generate_enum_functions l ctx id fns enums in let enums = List.map (fun e -> to_ast_id ctx (fst e)) enums in ( fns @ [DEF_aux (DEF_type (TD_aux (TD_enum (id, enums, false), (l, empty_uannot))), def_annot)], - { ctx with type_constructors = Bindings.add id ([], K_type) ctx.type_constructors } + { ctx with type_constructors = Bindings.add id ([], P.K_type) ctx.type_constructors } ) | P.TD_abstract (id, kind) -> if not !opt_abstract_types then raise (Reporting.err_general l abstract_type_error); @@ -1621,7 +1676,10 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_ match to_ast_kind kind with | Some kind -> ( [DEF_aux (DEF_type (TD_aux (TD_abstract (id, kind), (l, empty_uannot))), def_annot)], - { ctx with type_constructors = Bindings.add id ([], unaux_kind kind) ctx.type_constructors } + { + ctx with + type_constructors = Bindings.add id ([], to_parse_kind (Some (unaux_kind kind))) ctx.type_constructors; + } ) | None -> raise (Reporting.err_general l "Abstract type cannot have Order kind") end @@ -1630,7 +1688,7 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_ let typ = to_ast_typ ctx typ in let ranges = List.map (fun (id, range) -> (to_ast_id ctx id, to_ast_range ctx range)) ranges in ( [DEF_aux (DEF_type (TD_aux (TD_bitfield (id, typ, ranges), (l, empty_uannot))), def_annot)], - { ctx with type_constructors = Bindings.add id ([], K_type) ctx.type_constructors } + { ctx with type_constructors = Bindings.add id ([], P.K_type) ctx.type_constructors } ) let to_ast_rec ctx (P.Rec_aux (r, l) : P.rec_opt) : uannot rec_opt = @@ -2009,33 +2067,33 @@ let initial_ctx = (fun m (k, v) -> Bindings.add (mk_id k) v m) Bindings.empty [ - ("bool", ([], K_type)); - ("nat", ([], K_type)); - ("int", ([], K_type)); - ("unit", ([], K_type)); - ("bit", ([], K_type)); - ("string", ([], K_type)); - ("string_literal", ([], K_type)); - ("real", ([], K_type)); - ("list", ([Some K_type], K_type)); - ("register", ([Some K_type], K_type)); - ("range", ([Some K_int; Some K_int], K_type)); - ("bitvector", ([Some K_int; None], K_type)); - ("vector", ([Some K_int; None; Some K_type], K_type)); - ("atom", ([Some K_int], K_type)); - ("atom_bool", ([Some K_bool], K_type)); - ("implicit", ([Some K_int], K_type)); - ("itself", ([Some K_int], K_type)); - ("not", ([Some K_bool], K_bool)); - ("ite", ([Some K_bool; Some K_int; Some K_int], K_int)); - ("abs", ([Some K_int], K_int)); - ("mod", ([Some K_int; Some K_int], K_int)); - ("div", ([Some K_int; Some K_int], K_int)); - ("float16", ([], K_type)); - ("float32", ([], K_type)); - ("float64", ([], K_type)); - ("float128", ([], K_type)); - ("float_rounding_mode", ([], K_type)); + ("bool", ([], P.K_type)); + ("nat", ([], P.K_type)); + ("int", ([], P.K_type)); + ("unit", ([], P.K_type)); + ("bit", ([], P.K_type)); + ("string", ([], P.K_type)); + ("string_literal", ([], P.K_type)); + ("real", ([], P.K_type)); + ("list", ([P.K_type], P.K_type)); + ("register", ([P.K_type], P.K_type)); + ("range", ([P.K_int; P.K_int], P.K_type)); + ("bitvector", ([P.K_nat; P.K_order], P.K_type)); + ("vector", ([P.K_nat; P.K_order; P.K_type], P.K_type)); + ("atom", ([P.K_int], P.K_type)); + ("atom_bool", ([P.K_bool], P.K_type)); + ("implicit", ([P.K_int], P.K_type)); + ("itself", ([P.K_int], P.K_type)); + ("not", ([P.K_bool], P.K_bool)); + ("ite", ([P.K_bool; P.K_int; P.K_int], P.K_int)); + ("abs", ([P.K_int], P.K_int)); + ("mod", ([P.K_int; P.K_int], P.K_int)); + ("div", ([P.K_int; P.K_int], P.K_int)); + ("float16", ([], P.K_type)); + ("float32", ([], P.K_type)); + ("float64", ([], P.K_type)); + ("float128", ([], P.K_type)); + ("float_rounding_mode", ([], P.K_type)); ]; function_type_variables = Bindings.empty; kinds = KBindings.empty; @@ -2162,7 +2220,7 @@ let generate_undefined_enum id ids = ]; ] -let undefined_builtin_val_specs = +let undefined_builtin_val_specs () = [ extern_of_string (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a"; extern_of_string (mk_id "undefined_bool") "unit -> bool"; @@ -2183,7 +2241,7 @@ let make_global (DEF_aux (def, def_annot)) = DEF_aux (def, add_def_attribute (gen_loc def_annot.loc) "global" None def_annot) let generate_undefineds vs_ids = - List.filter (fun def -> IdSet.is_empty (IdSet.inter vs_ids (ids_of_def def))) undefined_builtin_val_specs + List.filter (fun def -> IdSet.is_empty (IdSet.inter vs_ids (ids_of_def def))) (undefined_builtin_val_specs ()) let rec get_uninitialized_registers = function | DEF_aux (DEF_register (DEC_aux (DEC_reg (typ, id, None), _)), _) :: defs -> begin diff --git a/src/lib/initial_check.mli b/src/lib/initial_check.mli index 2d4c0b77c..b1264db62 100644 --- a/src/lib/initial_check.mli +++ b/src/lib/initial_check.mli @@ -56,6 +56,10 @@ open Ast_util if they are encountered. *) val opt_abstract_types : bool ref +(** If enabled, bitvector types are only well-formed if their + arguments are natural numbers. *) +val opt_strict_bitvector : bool ref + (** Generate faster undefined_T functions. Rather than generating functions that allow for the undefined values of enums and variants to be picked at runtime using a RNG or similar, this creates @@ -93,7 +97,7 @@ val generate_undefined_enum : id -> id list -> untyped_def list (** Val specs of undefined functions for builtin types that get added to the AST by generate_undefinds (minus those functions that already exist in the AST). *) -val undefined_builtin_val_specs : untyped_def list +val undefined_builtin_val_specs : unit -> untyped_def list val generate_undefineds : IdSet.t -> untyped_def list diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index 98ac7137f..c3ce11fc2 100644 --- a/src/lib/lexer.mll +++ b/src/lib/lexer.mll @@ -87,9 +87,10 @@ let kw_table = ("let", (fun _ -> Let_)); ("var", (fun _ -> Var)); ("ref", (fun _ -> Ref)); - ("Int", (fun _ -> Int)); - ("Order", (fun _ -> Order)); - ("Bool", (fun _ -> Bool)); + ("Int", (fun _ -> INT)); + ("Nat", (fun _ -> NAT)); + ("Order", (fun _ -> ORDER)); + ("Bool", (fun _ -> BOOL)); ("pure", (fun _ -> Pure)); ("impure", (fun _ -> Impure)); ("monadic", (fun _ -> Monadic)); diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 506ace698..44dc43965 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -4328,7 +4328,11 @@ module BitvectorSizeCasts = struct let cast_specs, _ = let kid = mk_kid "n" in let bitsn = bitvector_typ (nvar kid) in - let ts = mk_typschm (mk_typquant [mk_qi_id K_int kid]) (function_typ [bitsn] bitsn) in + let ts = + mk_typschm + (mk_typquant [mk_qi_id K_int kid; mk_qi_nc (nc_gteq (nvar kid) (nint 0))]) + (function_typ [bitsn] bitsn) + in let mkfn name = mk_val_spec (VS_val_spec (ts, name, Some { pure = true; bindings = [("_", "zeroExtend")] })) in let defs = List.map mkfn (IdSet.elements !specs_required) in check_defs initial_env defs diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index f68b2fb37..6d4fe318c 100644 --- a/src/lib/parse_ast.ml +++ b/src/lib/parse_ast.ml @@ -85,7 +85,8 @@ type ix = text (* infix identifier *) type kind_aux = | (* base kind *) K_type (* kind of types *) - | K_int (* kind of natural number size expressions *) + | K_int (* kind of integer type expressions *) + | K_nat (* kind of natural type expressions *) | K_order (* kind of vector order specifications *) | K_bool (* kind of constraints *) diff --git a/src/lib/parser.mly b/src/lib/parser.mly index d0c23884d..20282f324 100644 --- a/src/lib/parser.mly +++ b/src/lib/parser.mly @@ -215,7 +215,7 @@ let set_syntax_deprecated l = /*Terminals with no content*/ %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op -%token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast +%token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ INT NAT ORDER BOOL Cast %token Pure Impure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure Instantiation Impl Private @@ -423,13 +423,15 @@ typ_list: { $1 :: $3 } kind: - | Int + | INT { K_aux (K_int, loc $startpos $endpos) } + | NAT + { K_aux (K_nat, loc $startpos $endpos) } | TYPE { K_aux (K_type, loc $startpos $endpos) } - | Order + | ORDER { K_aux (K_order, loc $startpos $endpos) } - | Bool + | BOOL { K_aux (K_bool, loc $startpos $endpos) } kid_list: diff --git a/src/lib/preprocess.ml b/src/lib/preprocess.ml index b51c57020..25bf61fd1 100644 --- a/src/lib/preprocess.ml +++ b/src/lib/preprocess.ml @@ -72,6 +72,7 @@ let default_symbols = "FEATURE_BITVECTOR_TYPE"; "FEATURE_UNION_BARRIER"; "FEATURE_STRICT_VAR"; + "FEATURE_STRICT_BITVECTOR"; ] let symbols = ref default_symbols diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index b974dc0bf..7b1066912 100644 --- a/src/lib/pretty_print_sail.ml +++ b/src/lib/pretty_print_sail.ml @@ -75,13 +75,11 @@ module Printer (Config : PRINT_CONFIG) = struct ^^ match def_annot.visibility with Private _ -> string "private" ^^ space | Public -> empty let doc_kopt_no_parens = function - | kopt when is_int_kopt kopt -> doc_kid (kopt_kid kopt) + | kopt when is_int_kopt kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Int"] | kopt when is_typ_kopt kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Type"] | kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Bool"] - let doc_kopt = function - | kopt when is_int_kopt kopt -> doc_kopt_no_parens kopt - | kopt -> parens (doc_kopt_no_parens kopt) + let doc_kopt kopt = parens (doc_kopt_no_parens kopt) let doc_int n = string (Big_int.to_string n) diff --git a/src/lib/type_check.mli b/src/lib/type_check.mli index b3ef86687..478910402 100644 --- a/src/lib/type_check.mli +++ b/src/lib/type_check.mli @@ -218,7 +218,7 @@ module Env : sig environment is lacking even basic builtins. *) val empty : t - val builtin_typs : typquant Bindings.t + val builtin_typs : (typquant * kind_aux) Bindings.t val get_union_id : id -> t -> typquant * typ diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml index 632c3d5e3..12ec92c2d 100644 --- a/src/lib/type_env.ml +++ b/src/lib/type_env.ml @@ -339,32 +339,42 @@ let k_name () = let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (k_name ())) kinds) let builtin_typs = + let k_counter = ref 0 in + let k_name () = + let kid = mk_kid ("k#" ^ string_of_int !k_counter) in + incr k_counter; + kid + in + let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (k_name ())) kinds) in List.fold_left - (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m) + (fun m (name, parameter_kinds, kind) -> Bindings.add (mk_id name) (kinds_typq parameter_kinds, kind) m) Bindings.empty [ - ("range", [K_int; K_int]); - ("atom", [K_int]); - ("implicit", [K_int]); - ("vector", [K_int; K_type]); - ("bitvector", [K_int]); - ("register", [K_type]); - ("bit", []); - ("unit", []); - ("int", []); - ("nat", []); - ("bool", []); - ("real", []); - ("list", [K_type]); - ("string", []); - ("string_literal", []); - ("itself", [K_int]); - ("atom_bool", [K_bool]); - ("float16", []); - ("float32", []); - ("float64", []); - ("float128", []); - ("float_rounding_mode", []); + ("range", [K_int; K_int], K_type); + ("atom", [K_int], K_type); + ("implicit", [K_int], K_type); + ("vector", [K_int; K_type], K_type); + ("bitvector", [K_int], K_type); + ("register", [K_type], K_type); + ("bit", [], K_type); + ("unit", [], K_type); + ("int", [], K_type); + ("nat", [], K_type); + ("bool", [], K_type); + ("real", [], K_type); + ("list", [K_type], K_type); + ("string", [], K_type); + ("string_literal", [], K_type); + ("itself", [K_int], K_type); + ("atom_bool", [K_bool], K_type); + ("float16", [], K_type); + ("float32", [], K_type); + ("float64", [], K_type); + ("float128", [], K_type); + ("float_rounding_mode", [], K_type); + ("abs", [K_int], K_int); + ("mod", [K_int; K_int], K_int); + ("div", [K_int; K_int], K_int); ] let bound_typ_id env id = @@ -510,91 +520,61 @@ let add_filtered_overload original_id ids env = let infer_kind env id = let l = id_loc id in if Bindings.mem id builtin_typs then Bindings.find id builtin_typs - else if Bindings.mem id env.global.unions then fst (get_item l env (Bindings.find id env.global.unions)) - else if Bindings.mem id env.global.records then fst (get_item l env (Bindings.find id env.global.records)) - else if Bindings.mem id env.global.enums then mk_typquant [] - else if Bindings.mem id env.global.synonyms then - typ_error (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id) - else if Bindings.mem id env.global.abstract_typs then mk_typquant [] + else if Bindings.mem id env.global.unions then (fst (get_item l env (Bindings.find id env.global.unions)), K_type) + else if Bindings.mem id env.global.records then (fst (get_item l env (Bindings.find id env.global.records)), K_type) + else if Bindings.mem id env.global.enums then (mk_typquant [], K_type) + else if Bindings.mem id env.global.synonyms then ( + let typq, arg = get_item l env (Bindings.find id env.global.synonyms) in + (typq, unaux_kind (typ_arg_kind arg)) + ) + else if Bindings.mem id env.global.abstract_typs then ( + let kind = get_item l env (Bindings.find id env.global.abstract_typs) in + (mk_typquant [], unaux_kind kind) + ) else typ_error (id_loc id) ("Cannot infer kind of " ^ string_of_id id) -let check_args_typquant id env args typq = - let kopts, ncs = quant_split typq in - let rec subst_args kopts args = - match (kopts, args) with - | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_int_kopt kopt -> - List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args) - | kopt :: kopts, A_aux (A_typ _, _) :: args when is_typ_kopt kopt -> subst_args kopts args - | kopt :: kopts, A_aux (A_bool _, _) :: args when is_bool_kopt kopt -> subst_args kopts args - | [], [] -> ncs - | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq) - | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq) - in - let ncs = subst_args kopts args in - if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then () - else - typ_error (id_loc id) - ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id) - let get_constraints env = List.map snd env.constraints @ List.map snd env.global.constraints let get_global_constraints env = List.map snd env.global.constraints let get_constraint_reasons env = env.global.constraints @ env.constraints -let mk_synonym typq typ_arg = - let kopts, ncs = quant_split typq in - let kopts = List.map (fun kopt -> (kopt, fresh_existential (kopt_loc kopt) (unaux_kind (kopt_kind kopt)))) kopts in - let ncs = - List.map - (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts) - ncs - in - let typ_arg = - List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts - in - let kopts = List.map snd kopts in - let rec subst_args env l kopts args = - match (kopts, args) with - | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt -> - let typ_arg, ncs = subst_args env l kopts args in - ( typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg, - List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs - ) - | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt -> - let typ_arg, ncs = subst_args env l kopts args in - (typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs) - | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt -> - let typ_arg, ncs = subst_args env l kopts args in - (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs) - | [], [] -> (typ_arg, ncs) - | kopts, args -> - typ_error l - ("Synonym applied to bad arguments " - ^ Util.string_of_list ", " string_of_kinded_id kopts - ^ Util.string_of_list ", " string_of_typ_arg args +module Well_formedness = struct + type existential = { vars : KidSet.t; constr : n_constraint option } + + let no_existential = { vars = KidSet.empty; constr = None } + + let with_existential exs = + match exs.constr with Some ex_constraint -> fun c -> nc_or (nc_not ex_constraint) c | None -> fun c -> c + + let check_args_typquant id exs env args typq = + let kopts, ncs = quant_split typq in + let rec subst_args kopts args = + match (kopts, args) with + | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_int_kopt kopt -> + List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args) + | kopt :: kopts, A_aux (A_typ _, _) :: args when is_typ_kopt kopt -> subst_args kopts args + | kopt :: kopts, A_aux (A_bool _, _) :: args when is_bool_kopt kopt -> subst_args kopts args + | [], [] -> ncs + | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq) + | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq) + in + let ncs = subst_args kopts args in + let unproven = + match env.prove with + | Some prove -> List.filter (fun nc -> not (prove env (with_existential exs nc))) ncs + | None -> ncs + in + match unproven with + | [] -> () + | ncs -> + typ_error (id_loc id) + ("Could not prove " + ^ string_of_list ", " string_of_n_constraint ncs + ^ " for type constructor " ^ string_of_id id ) - in - fun l env args -> - let typ_arg, ncs = subst_args env l kopts args in - if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then typ_arg - else - typ_error l - ("Could not prove constraints " - ^ string_of_list ", " string_of_n_constraint ncs - ^ " in type synonym " ^ string_of_typ_arg typ_arg ^ " with " - ^ Util.string_of_list ", " string_of_n_constraint (get_constraints env) - ) - -let get_typ_synonym id env = - match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.synonyms) with - | Some (typq, arg) -> mk_synonym typq arg - | None -> raise Not_found - -let get_typ_synonyms env = filter_items env env.global.synonyms -module Well_formedness = struct let wf_debug str f x exs = typ_debug ~level:2 - (lazy ("wf_" ^ str ^ ": " ^ f x ^ " exs: " ^ Util.string_of_list ", " string_of_kid (KidSet.elements exs))) + (lazy ("wf_" ^ str ^ ": " ^ f x ^ " exs: " ^ Util.string_of_list ", " string_of_kid (KidSet.elements exs.vars))) [@@coverage off] (* Check if a type, order, n-expression or constraint is @@ -602,9 +582,21 @@ module Well_formedness = struct let rec wf_typ exs env (Typ_aux (typ_aux, l) as typ) = match typ_aux with | Typ_id id when bound_typ_id env id -> - let typq = infer_kind env id in + let typq, k = infer_kind env id in + begin + match k with + | K_type -> () + | _ -> + typ_error l + (string_of_id id ^ " has kind " ^ string_of_kind_aux k + ^ " but was used in a place where a type was expected" + ) + end; if not (Util.list_empty (quant_kopts typq)) then - typ_error l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq) + typ_error l + ("Type constructor " ^ string_of_id id ^ " expected arguments " ^ string_of_typquant typq + ^ ", but was used here with none" + ) else () | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id) | Typ_var kid -> begin @@ -627,15 +619,42 @@ module Well_formedness = struct wf_typ exs env typ1; wf_typ exs env typ2 | Typ_tuple typs -> List.iter (wf_typ exs env) typs + | Typ_app (id, [A_aux (A_nexp nexp, _)]) when string_of_id id = "bitvector" && !Initial_check.opt_strict_bitvector + -> + wf_nexp exs env nexp; + begin + match env.prove with + | Some prove -> + let with_existential = + match exs.constr with + | Some ex_constraint -> fun c -> nc_or (nc_not ex_constraint) c + | None -> fun c -> c + in + if not (prove env (with_existential (nc_gteq nexp (nint 0)))) then + typ_error l "Bitvector index must be greater than or equal to zero" + | None -> Reporting.unreachable l __POS__ "No prover in environment when checking well-formedness" + end | Typ_app (id, [(A_aux (A_nexp _, _) as arg)]) when string_of_id id = "implicit" -> wf_typ_arg exs env arg | Typ_app (id, args) when bound_typ_id env id -> List.iter (wf_typ_arg exs env) args; - check_args_typquant id env args (infer_kind env id) + let typq, k = infer_kind env id in + begin + match k with + | K_type -> () + | _ -> + typ_error l + (string_of_id id ^ " has kind " ^ string_of_kind_aux k + ^ " but was used in a place where a type was expected" + ) + end; + check_args_typquant id exs env args typq | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id) | Typ_exist ([], _, _) -> typ_error l "Existential must have some type variables" - | Typ_exist (kopts, nc, typ) when KidSet.is_empty exs -> - wf_constraint (KidSet.of_list (List.map kopt_kid kopts)) env nc; - wf_typ (KidSet.of_list (List.map kopt_kid kopts)) env typ + | Typ_exist (kopts, nc, typ) when KidSet.is_empty exs.vars -> + let vars = KidSet.of_list (List.map kopt_kid kopts) in + wf_constraint { vars; constr = None } env nc; + let env = List.fold_right (add_typ_var l) kopts env in + wf_typ { vars; constr = Some nc } env typ | Typ_exist (_, _, _) -> typ_error l "Nested existentials are not allowed" | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" [@coverage off] @@ -649,8 +668,24 @@ module Well_formedness = struct wf_debug "nexp" string_of_nexp nexp exs; match nexp_aux with | Nexp_id id when Bindings.mem id env.global.abstract_typs -> () - | Nexp_id id -> typ_error l ("Undefined type synonym " ^ string_of_id id) - | Nexp_var kid when KidSet.mem kid exs -> () + | Nexp_id id when bound_typ_id env id -> + let typq, k = infer_kind env id in + begin + match k with + | K_int -> () + | _ -> + typ_error l + (string_of_id id ^ " has kind " ^ string_of_kind_aux k + ^ " but was used in a place where a type-level number was expected" + ) + end; + if not (Util.list_empty (quant_kopts typq)) then + typ_error l + ("Numeric type constructor " ^ string_of_id id ^ " expected arguments " ^ string_of_typquant typq + ^ ", but was used here with none" + ) + | Nexp_id id -> typ_error l ("Undefined numeric type " ^ string_of_id id) + | Nexp_var kid when KidSet.mem kid exs.vars -> () | Nexp_var kid -> begin match get_typ_var kid env with | K_int -> () @@ -661,12 +696,19 @@ module Well_formedness = struct ) end | Nexp_constant _ -> () - | Nexp_app (id, nexps) -> - let name = string_of_id id in - (* We allow the abs, mod, and div functions that are included in the SMTLIB2 integer theory *) - if name = "abs" || name = "mod" || name = "div" || Bindings.mem id env.global.synonyms then - List.iter (fun n -> wf_nexp exs env n) nexps - else typ_error l ("Unknown type level operator or function " ^ name) + | Nexp_app (id, nexps) when bound_typ_id env id -> + let typq, k = infer_kind env id in + begin + match k with + | K_int -> () + | _ -> + typ_error l + (string_of_id id ^ " has kind " ^ string_of_kind_aux k + ^ " but was used in a place where a type-level number was expected" + ) + end; + List.iter (fun n -> wf_nexp exs env n) nexps + | Nexp_app (id, _) -> typ_error l ("Unknown type level numeric operator or function " ^ string_of_id id) | Nexp_times (nexp1, nexp2) | Nexp_sum (nexp1, nexp2) | Nexp_minus (nexp1, nexp2) -> wf_nexp exs env nexp1; wf_nexp exs env nexp2 @@ -677,11 +719,27 @@ module Well_formedness = struct wf_nexp exs env t; wf_nexp exs env e - and wf_constraint exs env (NC_aux (nc_aux, l) as nc) = + and wf_constraint (exs : existential) env (NC_aux (nc_aux, l) as nc) = wf_debug "constraint" string_of_n_constraint nc exs; match nc_aux with | NC_id id when Bindings.mem id env.global.abstract_typs -> () - | NC_id id -> typ_error l ("Undefined type synonym " ^ string_of_id id) + | NC_id id when bound_typ_id env id -> + let typq, k = infer_kind env id in + begin + match k with + | K_bool -> () + | _ -> + typ_error l + (string_of_id id ^ " has kind " ^ string_of_kind_aux k + ^ " but was used in a place where a constraint was expected" + ) + end; + if not (Util.list_empty (quant_kopts typq)) then + typ_error l + ("Constraint " ^ string_of_id id ^ " expected arguments " ^ string_of_typquant typq + ^ ", but was used here with none" + ) + | NC_id id -> typ_error l ("Undefined type constraint " ^ string_of_id id) | NC_equal (arg1, arg2) | NC_not_equal (arg1, arg2) -> wf_typ_arg exs env arg1; wf_typ_arg exs env arg2 @@ -693,7 +751,7 @@ module Well_formedness = struct wf_constraint exs env nc1; wf_constraint exs env nc2 | NC_app (_, args) -> List.iter (wf_typ_arg exs env) args - | NC_var kid when KidSet.mem kid exs -> () + | NC_var kid when KidSet.mem kid exs.vars -> () | NC_var kid -> begin match get_typ_var kid env with | K_bool -> () @@ -702,6 +760,57 @@ module Well_formedness = struct | NC_true | NC_false -> () end +let mk_synonym typq typ_arg = + let kopts, ncs = quant_split typq in + let kopts = List.map (fun kopt -> (kopt, fresh_existential (kopt_loc kopt) (unaux_kind (kopt_kind kopt)))) kopts in + let ncs = + List.map + (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts) + ncs + in + let typ_arg = + List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts + in + let kopts = List.map snd kopts in + let rec subst_args env l kopts args = + match (kopts, args) with + | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt -> + let typ_arg, ncs = subst_args env l kopts args in + ( typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg, + List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs + ) + | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt -> + let typ_arg, ncs = subst_args env l kopts args in + (typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs) + | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt -> + let typ_arg, ncs = subst_args env l kopts args in + (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs) + | [], [] -> (typ_arg, ncs) + | kopts, args -> + typ_error l + ("Synonym applied to bad arguments " + ^ Util.string_of_list ", " string_of_kinded_id kopts + ^ Util.string_of_list ", " string_of_typ_arg args + ) + in + fun l env args -> + let typ_arg, ncs = subst_args env l kopts args in + if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then typ_arg + else + typ_error l + ("Could not prove constraints " + ^ string_of_list ", " string_of_n_constraint ncs + ^ " in type synonym " ^ string_of_typ_arg typ_arg ^ " with " + ^ Util.string_of_list ", " string_of_n_constraint (get_constraints env) + ) + +let get_typ_synonym id env = + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.synonyms) with + | Some (typq, arg) -> mk_synonym typq arg + | None -> raise Not_found + +let get_typ_synonyms env = filter_items env env.global.synonyms + let add_abstract_typ id kind env = if bound_typ_id env id then typ_error (id_loc id) @@ -850,8 +959,8 @@ and expand_arg_synonyms env (A_aux (typ_arg, l)) = | A_nexp nexp -> A_aux (A_nexp (expand_nexp_synonyms env nexp |> nexp_simp), l) and add_constraint ?(global = false) ?reason constr env = + Well_formedness.wf_constraint Well_formedness.no_existential env constr; let (NC_aux (nc_aux, l) as constr) = constraint_simp (expand_constraint_synonyms env constr) in - Well_formedness.wf_constraint KidSet.empty env constr; let power_vars = constraint_power_variables constr in if KidSet.cardinal power_vars > 1 && !opt_smt_linearize then typ_error l @@ -900,11 +1009,10 @@ and add_constraint ?(global = false) ?reason constr env = ) let wf_typ ~at:at_l env (Typ_aux (_, l) as typ) = - let typ = expand_synonyms env typ in - Well_formedness.wf_debug "typ" string_of_typ typ KidSet.empty; + Well_formedness.wf_debug "typ" string_of_typ typ Well_formedness.no_existential; incr depth; try - Well_formedness.wf_typ KidSet.empty env typ; + Well_formedness.wf_typ Well_formedness.no_existential env typ; decr depth with Type_error (err_l, err) -> decr depth; @@ -912,11 +1020,10 @@ let wf_typ ~at:at_l env (Typ_aux (_, l) as typ) = typ_raise l (err_because (Err_other ("Well-formedness check failed for type" ^ extra), err_l, err)) let wf_constraint ~at:at_l env (NC_aux (_, l) as nc) = - let nc = expand_constraint_synonyms env nc in - Well_formedness.wf_debug "constraint" string_of_n_constraint nc KidSet.empty; + Well_formedness.wf_debug "constraint" string_of_n_constraint nc Well_formedness.no_existential; incr depth; try - Well_formedness.wf_constraint KidSet.empty env nc; + Well_formedness.wf_constraint Well_formedness.no_existential env nc; decr depth with Type_error (err_l, err) -> decr depth; @@ -938,13 +1045,16 @@ let add_typ_synonym id typq arg env = typ_error (id_loc id) ("Cannot define type synonym " ^ string_of_id id ^ ", as a type or synonym with that name already exists") else ( - let typq = - quant_map_items - (function - | QI_aux (QI_constraint nexp, aux) -> QI_aux (QI_constraint (expand_constraint_synonyms env nexp), aux) - | quant_item -> quant_item - ) - typq + let _, typq = + quant_fold_map_items + (fun env quant_item -> + match quant_item with + | QI_aux (QI_constraint constr, l) -> + let constr = expand_constraint_synonyms env constr in + (add_constraint constr env, QI_aux (QI_constraint constr, l)) + | QI_aux (QI_id kopt, l) -> (add_typ_var l kopt env, quant_item) + ) + env typq in typ_print ( lazy diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli index 3152e5e09..a86a7c88f 100644 --- a/src/lib/type_env.mli +++ b/src/lib/type_env.mli @@ -249,4 +249,4 @@ val set_prover : (t -> n_constraint -> bool) option -> t -> t sets up a correct initial environment. *) val empty : t -val builtin_typs : typquant Bindings.t +val builtin_typs : (typquant * kind_aux) Bindings.t diff --git a/src/lib/type_error.ml b/src/lib/type_error.ml index b28be9587..ccce856c2 100644 --- a/src/lib/type_error.ml +++ b/src/lib/type_error.ml @@ -350,6 +350,16 @@ let message_of_type_error type_error = end | Err_instantiation_info (_, err) -> to_message err | Err_unresolved_quants (id, quants, locals, tyvars, ncs) -> + let quants = + List.filter_map + (function + | QI_aux (QI_id _, _) as quant -> Some quant + | QI_aux (QI_constraint nc, _) as quant -> ( + match constraint_simp nc with NC_aux (NC_true, _) -> None | _ -> Some quant + ) + ) + quants + in ( Seq [ Line ("Could not resolve quantifiers for " ^ string_of_id id); diff --git a/src/sail_doc_backend/html_source.ml b/src/sail_doc_backend/html_source.ml index 3d0a59ddb..b60336933 100644 --- a/src/sail_doc_backend/html_source.ml +++ b/src/sail_doc_backend/html_source.ml @@ -77,7 +77,7 @@ let highlights ~filename ~contents = | Id _ -> mark Highlight.Id; go () - | Int | Bool | TYPE | Order -> + | INT | NAT | BOOL | TYPE | ORDER -> mark Highlight.Kind; go () | String _ -> diff --git a/src/sail_ocaml_backend/ocaml_backend.ml b/src/sail_ocaml_backend/ocaml_backend.ml index b0b39f7f4..4f5d5c27c 100644 --- a/src/sail_ocaml_backend/ocaml_backend.ml +++ b/src/sail_ocaml_backend/ocaml_backend.ml @@ -896,7 +896,7 @@ let ocaml_pp_generators ctx defs orig_types required = | TD_abbrev (_, _, _) -> assert false | TD_bitfield _ -> assert false ) - | exception Not_found -> Bindings.find id Type_check.Env.builtin_typs + | exception Not_found -> fst (Bindings.find id Type_check.Env.builtin_typs) in let tquants = quant_kopts allquants in let gen_tyvars = List.map (fun k -> kopt_kid k |> zencode_kid) (List.filter is_typ_kopt tquants) in diff --git a/test/c/get_slice_int.sail b/test/c/get_slice_int.sail index ac19cf9d2..0abd940af 100644 --- a/test/c/get_slice_int.sail +++ b/test/c/get_slice_int.sail @@ -3,7 +3,7 @@ $include /* Use functions to hide the fact that these are really small constants, so they are forced to be represented as big ints */ -val big_five : unit -> int +val big_five : unit -> nat function big_five() = 5 diff --git a/test/c/int_struct.sail b/test/c/int_struct.sail index 9e9099029..86249cf12 100644 --- a/test/c/int_struct.sail +++ b/test/c/int_struct.sail @@ -5,7 +5,7 @@ $include $[sv_module { stdout = true }] val print = "print_endline" : string -> unit -struct Foo('n: Int) = { +struct Foo('n) = { field: bits('n) } diff --git a/test/c/int_struct_constrained.sail b/test/c/int_struct_constrained.sail index c5b8beabb..c9a81c741 100644 --- a/test/c/int_struct_constrained.sail +++ b/test/c/int_struct_constrained.sail @@ -5,7 +5,7 @@ $include $[sv_module { stdout = true }] val print = "print_endline" : string -> unit -struct Foo('n: Int), 'n <= 64 = { +struct Foo('n: Int), 0 <= 'n <= 64 = { field: bits('n) } diff --git a/test/c/issue429.sail b/test/c/issue429.sail index f6c2b2235..61f8deeb7 100644 --- a/test/c/issue429.sail +++ b/test/c/issue429.sail @@ -2,7 +2,7 @@ default Order dec $include -union two_bitvectors('n : Int) = { +union two_bitvectors('n) = { BV1 : bits('n), BV2 : bits('n), } diff --git a/test/c/stack_struct.sail b/test/c/stack_struct.sail index 08c3f9639..2b8b40928 100644 --- a/test/c/stack_struct.sail +++ b/test/c/stack_struct.sail @@ -2,7 +2,7 @@ default Order dec $sail_internal -type bits ('n : Int) = bitvector('n, dec) +type bits('n) = bitvector('n, dec) union option ('a : Type) = { Some : 'a, diff --git a/test/lem/run_tests.py b/test/lem/run_tests.py index 2a9470c6b..12bb87a1d 100755 --- a/test/lem/run_tests.py +++ b/test/lem/run_tests.py @@ -81,7 +81,7 @@ def test_lem(name, opts, skip_list): continue tests[filename] = os.fork() if tests[filename] == 0: - step('{} -lem {} -o {} {}/{}'.format(sail, opts, basename, test_dir, filename)) + step('{} --lem {} --strict-bitvector -o {} {}/{}'.format(sail, opts, basename, test_dir, filename)) step('lem -lib {}/src/gen_lib {}_types.lem {}.lem'.format(sail_dir, basename, basename)) step('rm {}_types.lem {}.lem'.format(basename, basename)) print_ok(filename) diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail index 8f8fef496..c5cf400b0 100644 --- a/test/ocaml/reg_ref/rr.sail +++ b/test/ocaml/reg_ref/rr.sail @@ -33,7 +33,7 @@ overload _mod_GPR = { rGPR, wGPR } /* Create a new type which is a pair of a bitvector and a start index slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */ -newtype slice ('n : Int, 'm : Int) = MkSlice : (atom('n), bits('m)) +newtype slice ('n : Int, 'm : Nat) = MkSlice : (atom('n), bits('m)) /* Extract the bitvector from a slice */ val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m) diff --git a/test/pattern_completeness/run_tests.py b/test/pattern_completeness/run_tests.py index d13d24f59..438d384ae 100755 --- a/test/pattern_completeness/run_tests.py +++ b/test/pattern_completeness/run_tests.py @@ -26,7 +26,7 @@ def test_patterns(name): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: - step('{} -just_check {} 2> {}.error'.format(sail, filename, basename)) + step('{} --just-check {} 2> {}.error'.format(sail, filename, basename)) if filename.startswith('warn'): step('diff {}.error {}.expect'.format(basename, basename)) else: diff --git a/test/pattern_completeness/warn_struct_pattern_incomplete.sail b/test/pattern_completeness/warn_struct_pattern_incomplete.sail index c58a6e69d..c938859f8 100644 --- a/test/pattern_completeness/warn_struct_pattern_incomplete.sail +++ b/test/pattern_completeness/warn_struct_pattern_incomplete.sail @@ -2,7 +2,7 @@ default Order dec $include -struct foo('m: Int, 'n: Int) = { +struct foo('m, 'n) = { f1 : option(bits('n)), f2 : int('m), } diff --git a/test/typecheck/fail/add_vec_lit_old.expect b/test/typecheck/fail/add_vec_lit_old.expect index 98da899d1..b0a1aacb7 100644 --- a/test/typecheck/fail/add_vec_lit_old.expect +++ b/test/typecheck/fail/add_vec_lit_old.expect @@ -1,5 +1,5 @@ Warning: Deprecated fail/add_vec_lit_old.sail:9.4-8: -9 |val cast unsigned : forall ('n : Int). +9 |val cast unsigned : forall 'n.  | ^--^  | Cast annotations are deprecated. They will be removed in a future version of the language. diff --git a/test/typecheck/fail/add_vec_lit_old.sail b/test/typecheck/fail/add_vec_lit_old.sail index cb0054765..af18c2e7e 100644 --- a/test/typecheck/fail/add_vec_lit_old.sail +++ b/test/typecheck/fail/add_vec_lit_old.sail @@ -1,12 +1,12 @@ default Order inc -val add_vec = impure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). +val add_vec = impure {ocaml: "add_vec", lem: "add_vec"}: forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc) -val add_range = impure {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = impure {ocaml: "add_range", lem: "add_range"}: forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val cast unsigned : forall ('n : Int). +val cast unsigned : forall 'n. bitvector('n, inc) -> range(0, 2 ^ 'n - 1) overload operator + = {add_vec, add_range} diff --git a/test/typecheck/fail/bitfield_error.expect b/test/typecheck/fail/bitfield_error.expect index b053b7bd0..ce0080cde 100644 --- a/test/typecheck/fail/bitfield_error.expect +++ b/test/typecheck/fail/bitfield_error.expect @@ -10,5 +10,6 @@  | Bitfield error fail/bitfield_error.sail:6.6-13:  | 6 | b : 0 .. 15,  |  | ^-----^ -  |  | Could not resolve quantifiers for subrange_bits -  |  | * (0 <= 15 & (15 <= 0 & 0 < 15)) +  |  | Well-formedness check failed for type here +  |  | +  |  | Bitvector index must be greater than or equal to zero diff --git a/test/typecheck/fail/missing_tick.expect b/test/typecheck/fail/missing_tick.expect index 5218dff5d..80c023408 100644 --- a/test/typecheck/fail/missing_tick.expect +++ b/test/typecheck/fail/missing_tick.expect @@ -12,4 +12,4 @@  |  | Caused by fail/missing_tick.sail:5.16-17:  |  | 5 |type foo = bits(x)  |  |  | ^ -  |  |  | Undefined type synonym x +  |  |  | Undefined numeric type x diff --git a/test/typecheck/fail/negative_bits_existential.expect b/test/typecheck/fail/negative_bits_existential.expect index 5e9bbd84e..8f91dd007 100644 --- a/test/typecheck/fail/negative_bits_existential.expect +++ b/test/typecheck/fail/negative_bits_existential.expect @@ -1,5 +1,17 @@ Type error: -fail/negative_bits_existential.sail:12.17-26: -12 | let x: Foo = undefined; -  | ^-------^ -  | Type Foo cannot be undefined +fail/negative_bits_existential.sail:5.0-7.1: +5 |struct Foo = { +  |^------------- +7 |} +  |^ +  | Types are not well-formed within this type definition. Note that recursive types are forbidden. +  | +  | Caused by fail/negative_bits_existential.sail:6.8-32: +  | 6 | xs: {'n, 'n == -1. bits('n)} +  |  | ^----------------------^ +  |  | Well-formedness check failed for type +  |  | +  |  | Caused by fail/negative_bits_existential.sail:6.23-27: +  |  | 6 | xs: {'n, 'n == -1. bits('n)} +  |  |  | ^--^ +  |  |  | Could not prove 'n >= 0 for type constructor bits diff --git a/test/typecheck/fail/negative_bits_list.expect b/test/typecheck/fail/negative_bits_list.expect new file mode 100644 index 000000000..44392d38a --- /dev/null +++ b/test/typecheck/fail/negative_bits_list.expect @@ -0,0 +1,10 @@ +Type error: +fail/negative_bits_list.sail:8.11-25: +8 | let x: list(bits(-1)) = [||]; +  | ^------------^ +  | Well-formedness check failed for type +  | +  | Caused by fail/negative_bits_list.sail:8.16-20: +  | 8 | let x: list(bits(-1)) = [||]; +  |  | ^--^ +  |  | Could not prove -1 >= 0 for type constructor bits diff --git a/test/typecheck/pass/negative_bits_list.sail b/test/typecheck/fail/negative_bits_list.sail similarity index 100% rename from test/typecheck/pass/negative_bits_list.sail rename to test/typecheck/fail/negative_bits_list.sail diff --git a/test/typecheck/fail/negative_bits_struct.expect b/test/typecheck/fail/negative_bits_struct.expect index f6c309fda..a7b09249f 100644 --- a/test/typecheck/fail/negative_bits_struct.expect +++ b/test/typecheck/fail/negative_bits_struct.expect @@ -1,5 +1,10 @@ Type error: -fail/negative_bits_struct.sail:14.24-33: +fail/negative_bits_struct.sail:14.11-21: 14 | let x: synonym(1) = undefined; -  | ^-------^ -  | Type synonym(1) cannot be undefined +  | ^--------^ +  | Well-formedness check failed for type +  | +  | Caused by fail/negative_bits_struct.sail:14.11-18: +  | 14 | let x: synonym(1) = undefined; +  |  | ^-----^ +  |  | Could not prove 1 >= 2 for type constructor synonym diff --git a/test/typecheck/fail/negative_bits_struct.sail b/test/typecheck/fail/negative_bits_struct.sail index 9507cf1cb..54cc51fb2 100644 --- a/test/typecheck/fail/negative_bits_struct.sail +++ b/test/typecheck/fail/negative_bits_struct.sail @@ -2,11 +2,11 @@ default Order dec $include -struct Foo('n: Int) = { +struct Foo('n), 'n >= 2 = { xs: bits('n - 2) } -type synonym('n: Int) = Foo('n) +type synonym('n: Int), 'n >= 2 = Foo('n) val foo : unit -> unit diff --git a/test/typecheck/fail/negative_bits_struct2.expect b/test/typecheck/fail/negative_bits_struct2.expect index 49010a5a8..d16c472dd 100644 --- a/test/typecheck/fail/negative_bits_struct2.expect +++ b/test/typecheck/fail/negative_bits_struct2.expect @@ -1,5 +1,17 @@ Type error: -fail/negative_bits_struct2.sail:12.17-26: -12 | let x: Foo = undefined; -  | ^-------^ -  | Type Foo cannot be undefined +fail/negative_bits_struct2.sail:5.0-7.1: +5 |struct Foo = { +  |^------------- +7 |} +  |^ +  | Types are not well-formed within this type definition. Note that recursive types are forbidden. +  | +  | Caused by fail/negative_bits_struct2.sail:6.8-16: +  | 6 | xs: bits(-3) +  |  | ^------^ +  |  | Well-formedness check failed for type +  |  | +  |  | Caused by fail/negative_bits_struct2.sail:6.8-12: +  |  | 6 | xs: bits(-3) +  |  |  | ^--^ +  |  |  | Could not prove -3 >= 0 for type constructor bits diff --git a/test/typecheck/fail/negative_bits_tuple.expect b/test/typecheck/fail/negative_bits_tuple.expect index 553f35f1e..ed5f89ab8 100644 --- a/test/typecheck/fail/negative_bits_tuple.expect +++ b/test/typecheck/fail/negative_bits_tuple.expect @@ -1,5 +1,10 @@ Type error: -fail/negative_bits_tuple.sail:8.29-38: +fail/negative_bits_tuple.sail:8.11-26: 8 | let x: (bits(-1), int) = undefined; -  | ^-------^ -  | Type (bits(-1), int) could be empty +  | ^-------------^ +  | Well-formedness check failed for type +  | +  | Caused by fail/negative_bits_tuple.sail:8.12-16: +  | 8 | let x: (bits(-1), int) = undefined; +  |  | ^--^ +  |  | Could not prove -1 >= 0 for type constructor bits diff --git a/test/typecheck/fail/negative_bits_union.expect b/test/typecheck/fail/negative_bits_union.expect index e78b32efb..82d597497 100644 --- a/test/typecheck/fail/negative_bits_union.expect +++ b/test/typecheck/fail/negative_bits_union.expect @@ -1,5 +1,5 @@ Type error: -fail/negative_bits_union.sail:12.20-29: -12 | let x: Foo(1) = undefined; -  | ^-------^ -  | Type Foo(1) cannot be undefined +fail/negative_bits_union.sail:6.10-22: +6 | Bar : bits('n - 2), +  | ^----------^ +  | Could not prove constraints ('n - 2) >= 0 in type synonym bitvector(('n - 2)) with diff --git a/test/typecheck/fail/negative_bits_union2.expect b/test/typecheck/fail/negative_bits_union2.expect index b0bac9e6c..36f8e6cd3 100644 --- a/test/typecheck/fail/negative_bits_union2.expect +++ b/test/typecheck/fail/negative_bits_union2.expect @@ -1,5 +1,5 @@ Type error: -fail/negative_bits_union2.sail:15.20-29: -15 | let x: Foo(1) = undefined; -  | ^-------^ -  | Type Foo(1) cannot be undefined +fail/negative_bits_union2.sail:8.10-22: +8 | Bar : bits('n - 2), +  | ^----------^ +  | Could not prove constraints ('n - 2) >= 0 in type synonym bitvector(('n - 2)) with diff --git a/test/typecheck/fail/non_synonym.expect b/test/typecheck/fail/non_synonym.expect index 32b27ea71..53e654f4c 100644 --- a/test/typecheck/fail/non_synonym.expect +++ b/test/typecheck/fail/non_synonym.expect @@ -7,4 +7,4 @@  | Caused by fail/non_synonym.sail:6.23-26:  | 6 |let my_vector : vector(max, dec, int) = [1, 2, 3, 4, 5, 6]  |  | ^-^ -  |  | Undefined type synonym max +  |  | Undefined numeric type max diff --git a/test/typecheck/fail/procstate1.expect b/test/typecheck/fail/procstate1.expect index f3c402190..e9e365b67 100644 --- a/test/typecheck/fail/procstate1.expect +++ b/test/typecheck/fail/procstate1.expect @@ -1,5 +1,17 @@ Type error: -fail/procstate1.sail:14.0-30: -14 |register PSTATE : ProcState(1) -  |^----------------------------^ -  | Must provide a default register value for a register of type ProcState(1) +fail/procstate1.sail:7.0-12.1: +7  |struct ProcState('n : Int) = { +  |^----------------------------- +12 |} +  |^ +  | Types are not well-formed within this type definition. Note that recursive types are forbidden. +  | +  | Caused by fail/procstate1.sail:8.6-24: +  | 8 | N : bitvector('n, dec), +  |  | ^----------------^ +  |  | Well-formedness check failed for type +  |  | +  |  | Caused by fail/procstate1.sail:8.6-24: +  |  | 8 | N : bitvector('n, dec), +  |  |  | ^----------------^ +  |  |  | Bitvector index must be greater than or equal to zero diff --git a/test/typecheck/fail/procstate1.sail b/test/typecheck/fail/procstate1.sail index 250b9aaff..0a1736ed9 100644 --- a/test/typecheck/fail/procstate1.sail +++ b/test/typecheck/fail/procstate1.sail @@ -4,7 +4,7 @@ infix 4 == val operator == = pure {lem: "eq_vec"} : forall 'n. (bitvector('n, dec), bitvector('n, dec)) -> bool -struct ProcState ('n : Int) = { +struct ProcState('n : Int) = { N : bitvector('n, dec), Z : bitvector(1, dec), C : bitvector(1, dec), diff --git a/test/typecheck/fail/tuple_lexp1.expect b/test/typecheck/fail/tuple_lexp1.expect index f5532423b..046070d21 100644 --- a/test/typecheck/fail/tuple_lexp1.expect +++ b/test/typecheck/fail/tuple_lexp1.expect @@ -2,7 +2,7 @@ fail/tuple_lexp1.sail:10.11-20: 10 | (x, y) = (2, 3, 4)  | ^-------^ -  | Type mismatch between (int('ex248#), int('ex249#)) and (int(2), int(3), int(4)) +  | Type mismatch between (int('ex180#), int('ex181#)) and (int(2), int(3), int(4))  |  | Caused by fail/tuple_lexp1.sail:10.2-8:  | 10 | (x, y) = (2, 3, 4) diff --git a/test/typecheck/fail/tuple_lexp2.expect b/test/typecheck/fail/tuple_lexp2.expect index d219bc97b..99d73fc46 100644 --- a/test/typecheck/fail/tuple_lexp2.expect +++ b/test/typecheck/fail/tuple_lexp2.expect @@ -2,7 +2,7 @@ fail/tuple_lexp2.sail:10.11-12: 10 | (x, y) = 2  | ^ -  | Type mismatch between (int('ex248#), int('ex249#)) and int(2) +  | Type mismatch between (int('ex180#), int('ex181#)) and int(2)  |  | Caused by fail/tuple_lexp2.sail:10.2-8:  | 10 | (x, y) = 2 diff --git a/test/typecheck/fail/unbound_tyvar.expect b/test/typecheck/fail/unbound_tyvar.expect index aee5a2e32..799bae203 100644 --- a/test/typecheck/fail/unbound_tyvar.expect +++ b/test/typecheck/fail/unbound_tyvar.expect @@ -9,4 +9,4 @@  | Caused by fail/unbound_tyvar.sail:5.23-44:  | 5 |function foo() -> bits(definitelydoesntexist) = {  |  | ^-------------------^ -  |  | Undefined type synonym definitelydoesntexist +  |  | Undefined numeric type definitelydoesntexist diff --git a/test/typecheck/fail/unbound_tyvar2.expect b/test/typecheck/fail/unbound_tyvar2.expect index f5b98be1f..31a5c8006 100644 --- a/test/typecheck/fail/unbound_tyvar2.expect +++ b/test/typecheck/fail/unbound_tyvar2.expect @@ -7,4 +7,4 @@  | Caused by fail/unbound_tyvar2.sail:5.23-44:  | 5 |val foo : unit -> bits(definitelydoesntexist)  |  | ^-------------------^ -  |  | Undefined type synonym definitelydoesntexist +  |  | Undefined numeric type definitelydoesntexist diff --git a/test/typecheck/fail/unscope_type.expect b/test/typecheck/fail/unscope_type.expect index 573a29123..c93dccad8 100644 --- a/test/typecheck/fail/unscope_type.expect +++ b/test/typecheck/fail/unscope_type.expect @@ -2,9 +2,14 @@ fail/unscope_type.sail:18.10-13: 18 | let _ : foo = 0xFFFF_FFFF;  | ^-^ -  | Not in scope +  | Well-formedness check failed for type  | -  | Try requiring module A to bring the following into scope: -  | fail/unscope_type.sail:11.5-8: -  | 11 |type foo = bits(32) -  |  | ^-^ definition here in A +  | Caused by fail/unscope_type.sail:18.10-13: +  | 18 | let _ : foo = 0xFFFF_FFFF; +  |  | ^-^ +  |  | Not in scope +  |  | +  |  | Try requiring module A to bring the following into scope: +  |  | fail/unscope_type.sail:11.5-8: +  |  | 11 |type foo = bits(32) +  |  |  | ^-^ definition here in A diff --git a/test/typecheck/fail/wf_assign_type.expect b/test/typecheck/fail/wf_assign_type.expect index ca00c56ee..015037774 100644 --- a/test/typecheck/fail/wf_assign_type.expect +++ b/test/typecheck/fail/wf_assign_type.expect @@ -7,4 +7,4 @@  | Caused by fail/wf_assign_type.sail:9.15-16:  | 9 | var Y : bits(X) = 0b00;  |  | ^ -  |  | Undefined type synonym X +  |  | Undefined numeric type X diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail index 291b7e168..32d178667 100644 --- a/test/typecheck/pass/Replicate.sail +++ b/test/typecheck/pass/Replicate.sail @@ -6,10 +6,10 @@ $include overload operator / = {ediv_int} overload operator % = {emod_int} -val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. +val Replicate : forall 'M 'N, 'M >= 1. (implicit('N), bits('M)) -> bits('N) effect {escape} function Replicate (N, x) = { assert('N % 'M == 0); replicate_bits(x, 'N / 'M) -} \ No newline at end of file +} diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect index 0499decdd..dd092e23f 100644 --- a/test/typecheck/pass/Replicate/v1.expect +++ b/test/typecheck/pass/Replicate/v1.expect @@ -8,4 +8,6 @@ Explicit effect annotations are deprecated. They are no longer used and can be r pass/Replicate/v1.sail:14.4-30: 14 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Failed to prove constraint: ('M * div('N, 'M)) == 'N +  | Could not resolve quantifiers for replicate_bits +  | * 'M >= 0 +  | * div('N, 'M) >= 0 diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail index 55627db54..0b9feb9ca 100644 --- a/test/typecheck/pass/Replicate/v1.sail +++ b/test/typecheck/pass/Replicate/v1.sail @@ -6,10 +6,10 @@ $include overload operator / = {ediv_int} overload operator % = {emod_int} -val Replicate : forall ('M : Int) ('N : Int), 'M >= 0. +val Replicate : forall 'M 'N. (implicit('N), bits('M)) -> bits('N) effect {escape} function Replicate (N, x) = { assert('N % 'M == 0); replicate_bits(x, 'N / 'M) -} \ No newline at end of file +} diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index fc0f5e158..cb1fedf96 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -8,4 +8,6 @@ Explicit effect annotations are deprecated. They are no longer used and can be r pass/Replicate/v2.sail:13.4-30: 13 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Failed to prove constraint: ('M * 'ex248#) == 'N +  | Could not resolve quantifiers for replicate_bits +  | * 'M >= 0 +  | * 'ex176# >= 0 diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail index 436ef24b0..1cb949f72 100644 --- a/test/typecheck/pass/Replicate/v2.sail +++ b/test/typecheck/pass/Replicate/v2.sail @@ -5,7 +5,7 @@ $include overload operator / = {tdiv_int} overload operator % = {tmod_int} -val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. +val Replicate : forall 'M 'N, 'M >= 1. (implicit('N), bits('M)) -> bits('N) effect {escape} function Replicate (N, x) = { diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail index efe625558..be2261618 100644 --- a/test/typecheck/pass/add_vec_lit.sail +++ b/test/typecheck/pass/add_vec_lit.sail @@ -1,14 +1,13 @@ default Order inc $include -val add_vec = pure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). +val add_vec = pure {ocaml: "add_vec", lem: "add_vec"}: forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc) -val unsigned : forall ('n : Int). +val unsigned : forall 'n. bitvector('n, inc) -> range(0, 2 ^ 'n - 1) overload operator + = {add_vec} let x : range(0, 30) = unsigned(0xF + 0x2) let y : range(0, 30) = unsigned(0xF) + unsigned(0x2) - diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail index 8c08bf95d..3b85f0de4 100644 --- a/test/typecheck/pass/arm_FPEXC1.sail +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -1,12 +1,12 @@ default Order dec -val vector_access = pure {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int). +val vector_access = pure {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall 'n. (bitvector('n, dec), int) -> bit -val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1. +val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall 'n 'm 'o, 'm >= 'o & 'o >= 0 & 'n >= 'm + 1. (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec) -val vector_update_subrange = pure {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. +val vector_update_subrange = pure {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o, 'm - ('o - 1) >= 0. (bitvector('n, dec), atom('m), atom('o), bitvector('m - ('o - 1), dec)) -> bitvector('n, dec) register _FPEXC32_EL2 : bitvector(32, dec) diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect index d9a6e0cc6..5692869b5 100644 --- a/test/typecheck/pass/bool_constraint/v1.expect +++ b/test/typecheck/pass/bool_constraint/v1.expect @@ -9,13 +9,13 @@ All external bindings should be marked as either pure or impure 12 | if b then n else 4  | ^  | int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} -  | as (('b & 'ex239 == 'n) | (not('b) & 'ex239 == 3)) could not be proven +  | as (('b & 'ex171 == 'n) | (not('b) & 'ex171 == 3)) could not be proven  | -  | type variable 'ex239: +  | type variable 'ex171:  | pass/bool_constraint/v1.sail:9.25-73:  | 9 | (bool('b), int('n)) -> {'m, 'b & 'm == 'n | not('b) & 'm == 3. int('m)}  |  | ^----------------------------------------------^ derived from here  | pass/bool_constraint/v1.sail:12.19-20:  | 12 | if b then n else 4  |  | ^ bound here -  |  | has constraint: 4 == 'ex239 +  |  | has constraint: 4 == 'ex171 diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail index cc7225694..3d6ab6630 100644 --- a/test/typecheck/pass/deinfix_plus.sail +++ b/test/typecheck/pass/deinfix_plus.sail @@ -1,6 +1,6 @@ default Order inc -val bv_add = pure {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall ('n : Int). +val bv_add = pure {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc) overload operator + = {bv_add} diff --git a/test/typecheck/pass/ex_cast.sail b/test/typecheck/pass/ex_cast.sail index 6565e9d18..83d4156f8 100644 --- a/test/typecheck/pass/ex_cast.sail +++ b/test/typecheck/pass/ex_cast.sail @@ -4,6 +4,6 @@ val cast ex_int : int -> {'n, true. atom('n)} val zeros : forall 'n. atom('n) -> vector('n, dec, bit) -val test : int -> unit +val test : nat -> unit function test n = { x = zeros(n); () } diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index b4870d796..65f17520d 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -1,5 +1,10 @@ Type error: -pass/exist_synonym/v1.sail:6.28-37: +pass/exist_synonym/v1.sail:6.8-38: 6 |let x : {'n, 0 <= 'n <= 33. regno('n)} = 4 -  | ^-------^ -  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) +  | ^----------------------------^ +  | Well-formedness check failed for type +  | +  | Caused by pass/exist_synonym/v1.sail:6.28-33: +  | 6 |let x : {'n, 0 <= 'n <= 33. regno('n)} = 4 +  |  | ^---^ +  |  | Could not prove (0 <= 'n & 'n < 32) for type constructor regno diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index d88e1aafa..63096bbbf 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -1,5 +1,10 @@ Type error: -pass/exist_synonym/v2.sail:6.27-36: +pass/exist_synonym/v2.sail:6.8-37: 6 |let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 -  | ^-------^ -  | Could not prove constraints (0 <= 'n & 'n < 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) +  | ^---------------------------^ +  | Well-formedness check failed for type +  | +  | Caused by pass/exist_synonym/v2.sail:6.27-32: +  | 6 |let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 +  |  | ^---^ +  |  | Could not prove (0 <= 'n & 'n < 2) for type constructor regno diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index 4aecd8c57..a4d2e7547 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -1,5 +1,10 @@ Type error: -pass/exist_synonym/v3.sail:9.38-47: +pass/exist_synonym/v3.sail:9.11-55: 9 |val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit -  | ^-------^ -  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_#x & '_#x <= 8), (0 <= '_#x#0 & '_#x#0 <= 8) +  | ^------------------------------------------^ +  | Well-formedness check failed for type +  | +  | Caused by pass/exist_synonym/v3.sail:9.38-43: +  | 9 |val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit +  |  | ^---^ +  |  | Could not prove (0 <= 'n & 'n < 32) for type constructor regno diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index f9711cd3c..169c87429 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -1,5 +1,10 @@ Type error: -pass/exist_synonym/v4.sail:9.35-44: +pass/exist_synonym/v4.sail:9.11-52: 9 |val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit -  | ^-------^ -  | Could not prove constraints (0 <= 'n & 'n < 32) in type synonym int('n) with (0 <= '_#x & '_#x <= 8), (0 <= '_#x#0 & '_#x#0 <= 8) +  | ^---------------------------------------^ +  | Well-formedness check failed for type +  | +  | Caused by pass/exist_synonym/v4.sail:9.35-40: +  | 9 |val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit +  |  | ^---^ +  |  | Could not prove (0 <= 'n & 'n < 32) for type constructor regno diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail index 1d0e1d207..40db23a07 100644 --- a/test/typecheck/pass/exist_tlb.sail +++ b/test/typecheck/pass/exist_tlb.sail @@ -1,16 +1,16 @@ $include -val extz : forall ('n : Int) ('m : Int) ('ord : Order). +val extz : forall 'n 'm ('ord : Order). bitvector('n, 'ord) -> bitvector('m, 'ord) -val exts : forall ('n : Int) ('m : Int) ('ord : Order). +val exts : forall 'n 'm ('ord : Order). bitvector('n, 'ord) -> bitvector('m, 'ord) overload EXTZ = {extz} overload EXTS = {exts} -val add_vec : forall ('n : Int) ('ord : Order). +val add_vec : forall 'n ('ord : Order). (bitvector('n, 'ord), bitvector('n, 'ord)) -> bitvector('n, 'ord) overload operator + = {add_vec} @@ -71,10 +71,10 @@ function wordWidthBytes w = match w { D => 8 } -val MEMr_reserve_wrapper : forall ('n : Int). +val MEMr_reserve_wrapper : forall 'n. (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem} -val MEMr_wrapper : forall ('n : Int). +val MEMr_wrapper : forall 'n. (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem} val wGPR : (bitvector(5, dec), bitvector(64, dec)) -> unit effect {wreg} diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 59c047420..eb2b51394 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -9,4 +9,4 @@ Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}. 26 | Some(Ctor1(a, x, c))  | ^------------^ checking function argument has type ast  | Could not resolve quantifiers for Ctor1 -  | * 'ex334# in {32, 64} +  | * 'ex247# in {32, 64} diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index 609d3a744..8ba820a54 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -2,10 +2,10 @@ pass/existential_ast3/v1.sail:17.48-65: 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  | ^---------------^ -  | (int(33), int('ex288)) is not a subtype of (int('ex283), int('ex284)) +  | (int(33), int('ex212)) is not a subtype of (int('ex207), int('ex208))  | as false could not be proven  | -  | type variable 'ex283: +  | type variable 'ex207:  | pass/existential_ast3/v1.sail:16.23-25:  | 16 | let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =  |  | ^^ derived from here @@ -13,7 +13,7 @@  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ bound here  | -  | type variable 'ex284: +  | type variable 'ex208:  | pass/existential_ast3/v1.sail:16.26-28:  | 16 | let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =  |  | ^^ derived from here @@ -21,7 +21,7 @@  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ bound here  | -  | type variable 'ex288: +  | type variable 'ex212:  | pass/existential_ast3/v1.sail:17.48-65:  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ bound here diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 353d38332..f63196c07 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -2,10 +2,10 @@ pass/existential_ast3/v2.sail:17.48-65: 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  | ^---------------^ -  | (int(31), int('ex288)) is not a subtype of (int('ex283), int('ex284)) +  | (int(31), int('ex212)) is not a subtype of (int('ex207), int('ex208))  | as false could not be proven  | -  | type variable 'ex283: +  | type variable 'ex207:  | pass/existential_ast3/v2.sail:16.23-25:  | 16 | let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =  |  | ^^ derived from here @@ -13,7 +13,7 @@  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ bound here  | -  | type variable 'ex284: +  | type variable 'ex208:  | pass/existential_ast3/v2.sail:16.26-28:  | 16 | let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =  |  | ^^ derived from here @@ -21,7 +21,7 @@  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ bound here  | -  | type variable 'ex288: +  | type variable 'ex212:  | pass/existential_ast3/v2.sail:17.48-65:  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ bound here diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 6779d6df8..0e2882dd6 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,4 +3,4 @@ 25 | Some(Ctor(64, unsigned(0b0 @ b @ a)))  | ^-----------------------------^ checking function argument has type ast  | Could not resolve quantifiers for Ctor -  | * (64 in {32, 64} & (0 <= 'ex325# & 'ex325# < 64)) +  | * (64 in {32, 64} & (0 <= 'ex244# & 'ex244# < 64)) diff --git a/test/typecheck/pass/existential_ast3/v4.expect b/test/typecheck/pass/existential_ast3/v4.expect index dc172e036..1636d061b 100644 --- a/test/typecheck/pass/existential_ast3/v4.expect +++ b/test/typecheck/pass/existential_ast3/v4.expect @@ -3,13 +3,13 @@ 36 | if is_64 then 64 else 32;  | ^^  | int(64) is not a subtype of {('d : Int), (('is_64 & 'd == 63) | (not('is_64) & 'd == 32)). int('d)} -  | as (('is_64 & 'ex341 == 63) | (not('is_64) & 'ex341 == 32)) could not be proven +  | as (('is_64 & 'ex256 == 63) | (not('is_64) & 'ex256 == 32)) could not be proven  | -  | type variable 'ex341: +  | type variable 'ex256:  | pass/existential_ast3/v4.sail:35.18-79:  | 35 | let 'datasize : {'d, ('is_64 & 'd == 63) | (not('is_64) & 'd == 32). int('d)} =  |  | ^-----------------------------------------------------------^ derived from here  | pass/existential_ast3/v4.sail:36.18-20:  | 36 | if is_64 then 64 else 32;  |  | ^^ bound here -  |  | has constraint: 64 == 'ex341 +  |  | has constraint: 64 == 'ex256 diff --git a/test/typecheck/pass/existential_ast3/v5.expect b/test/typecheck/pass/existential_ast3/v5.expect index 91b3e4539..57b7e4b62 100644 --- a/test/typecheck/pass/existential_ast3/v5.expect +++ b/test/typecheck/pass/existential_ast3/v5.expect @@ -3,13 +3,13 @@ 37 | let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);  | ^-------------^  | range(0, 63) is not a subtype of range(0, ('datasize - 2)) -  | as (0 <= 'ex349 & 'ex349 <= ('datasize - 2)) could not be proven +  | as (0 <= 'ex264 & 'ex264 <= ('datasize - 2)) could not be proven  | -  | type variable 'ex349: +  | type variable 'ex264:  | pass/existential_ast3/v5.sail:37.10-33:  | 37 | let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);  |  | ^---------------------^ derived from here  | pass/existential_ast3/v5.sail:37.50-65:  | 37 | let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);  |  | ^-------------^ bound here -  |  | has constraint: (0 <= 'ex349 & 'ex349 <= 63) +  |  | has constraint: (0 <= 'ex264 & 'ex264 <= 63) diff --git a/test/typecheck/pass/existential_ast3/v6.expect b/test/typecheck/pass/existential_ast3/v6.expect index bab7bcb89..f56f52ecd 100644 --- a/test/typecheck/pass/existential_ast3/v6.expect +++ b/test/typecheck/pass/existential_ast3/v6.expect @@ -3,13 +3,13 @@ 37 | let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);  | ^-------------^  | range(0, 63) is not a subtype of range(0, ('datasize - 1)) -  | as (0 <= 'ex355 & 'ex355 <= ('datasize - 1)) could not be proven +  | as (0 <= 'ex270 & 'ex270 <= ('datasize - 1)) could not be proven  | -  | type variable 'ex355: +  | type variable 'ex270:  | pass/existential_ast3/v6.sail:37.10-33:  | 37 | let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);  |  | ^---------------------^ derived from here  | pass/existential_ast3/v6.sail:37.71-86:  | 37 | let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);  |  | ^-------------^ bound here -  |  | has constraint: (0 <= 'ex355 & 'ex355 <= 63) +  |  | has constraint: (0 <= 'ex270 & 'ex270 <= 63) diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index ff6f26082..7f5153d48 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -3,7 +3,7 @@ 10 | let _ = 0b100[if R then 0 else f()];  | ^-------------------------^  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex240# & 'ex240# < 3) +  | * (0 <= 'ex172# & 'ex172# < 3)  |  | Caused by pass/if_infer/v1.sail:10.10-37:  | 10 | let _ = 0b100[if R then 0 else f()]; diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index dacec8d6a..53ddc5a53 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -3,7 +3,7 @@ 10 | let _ = 0b1001[if R then 0 else f()];  | ^--------------------------^  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex240# & 'ex240# < 4) +  | * (0 <= 'ex172# & 'ex172# < 4)  |  | Caused by pass/if_infer/v2.sail:10.10-38:  | 10 | let _ = 0b1001[if R then 0 else f()]; diff --git a/test/typecheck/pass/int_synonym.sail b/test/typecheck/pass/int_synonym.sail index 1de6087e7..ff59f2c1c 100644 --- a/test/typecheck/pass/int_synonym.sail +++ b/test/typecheck/pass/int_synonym.sail @@ -3,7 +3,7 @@ default Order dec $include -type bits ('n : Int) = bitvector('n, dec) +type bits('n) = bitvector('n, dec) type xlen : Int = 64 type xlen_bytes : Int = 8 diff --git a/test/typecheck/pass/negative_bits_list/v1.expect b/test/typecheck/pass/negative_bits_list/v1.expect deleted file mode 100644 index f74668439..000000000 --- a/test/typecheck/pass/negative_bits_list/v1.expect +++ /dev/null @@ -1,5 +0,0 @@ -Type error: -pass/negative_bits_list/v1.sail:9.30-39: -9 | let z: list(bits(-1)) = [|undefined|]; -  | ^-------^ -  | Type bitvector(-1) could be empty diff --git a/test/typecheck/pass/negative_bits_list/v1.sail b/test/typecheck/pass/negative_bits_list/v1.sail deleted file mode 100644 index 7a1080162..000000000 --- a/test/typecheck/pass/negative_bits_list/v1.sail +++ /dev/null @@ -1,11 +0,0 @@ -default Order dec - -$include - -val foo : unit -> unit - -function foo() = { - let x: list(bits(-1)) = [||]; - let z: list(bits(-1)) = [|undefined|]; - () -} diff --git a/test/typecheck/pass/negative_bits_list/v2.expect b/test/typecheck/pass/negative_bits_list/v2.expect deleted file mode 100644 index e080a8588..000000000 --- a/test/typecheck/pass/negative_bits_list/v2.expect +++ /dev/null @@ -1,5 +0,0 @@ -Type error: -pass/negative_bits_list/v2.sail:9.28-37: -9 | let y: list(bits(-1)) = undefined; -  | ^-------^ -  | Type list(bits(-1)) cannot be undefined diff --git a/test/typecheck/pass/negative_bits_list/v2.sail b/test/typecheck/pass/negative_bits_list/v2.sail deleted file mode 100644 index c5238a289..000000000 --- a/test/typecheck/pass/negative_bits_list/v2.sail +++ /dev/null @@ -1,11 +0,0 @@ -default Order dec - -$include - -val foo : unit -> unit - -function foo() = { - let x: list(bits(-1)) = [||]; - let y: list(bits(-1)) = undefined; - () -} diff --git a/test/typecheck/pass/nexp_synonym2.sail b/test/typecheck/pass/nexp_synonym2.sail index 9e9bd7b8d..df1e3c507 100644 --- a/test/typecheck/pass/nexp_synonym2.sail +++ b/test/typecheck/pass/nexp_synonym2.sail @@ -6,7 +6,7 @@ type LEN : Int = 30 + 2 type V : Type = bits(LEN) -type V2('n: Int) -> Type = bits('n) +type V2('n : Int), 'n >= 0 -> Type = bits('n) let v : V = 0xFFFF_FFFF diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail index 5c376ba2e..cd5aa5fd6 100644 --- a/test/typecheck/pass/nzcv.sail +++ b/test/typecheck/pass/nzcv.sail @@ -1,6 +1,6 @@ default Order dec -val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. +val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_dec"} : forall 'n 'm 'o, 'o <= 'm <= 'n. (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec) val test : bitvector(4, dec) -> unit diff --git a/test/typecheck/pass/phantom_bitlist_struct.sail b/test/typecheck/pass/phantom_bitlist_struct.sail index 09d0f952a..125db07c3 100644 --- a/test/typecheck/pass/phantom_bitlist_struct.sail +++ b/test/typecheck/pass/phantom_bitlist_struct.sail @@ -2,7 +2,7 @@ default Order dec $include -struct phantom('n: Int) = { +struct phantom('n) = { bits: bits('n), } diff --git a/test/typecheck/pass/phantom_bitlist_union.sail b/test/typecheck/pass/phantom_bitlist_union.sail index 111424a15..6876b86f2 100644 --- a/test/typecheck/pass/phantom_bitlist_union.sail +++ b/test/typecheck/pass/phantom_bitlist_union.sail @@ -2,7 +2,7 @@ default Order dec $include -union phantom('n: Int) = { +union phantom('n) = { Bits: bits('n), } diff --git a/test/typecheck/pass/poly_vector/v2.expect b/test/typecheck/pass/poly_vector/v2.expect index 3dae703f4..8dd069a2a 100644 --- a/test/typecheck/pass/poly_vector/v2.expect +++ b/test/typecheck/pass/poly_vector/v2.expect @@ -1,5 +1,5 @@ Type error: -pass/poly_vector/v2.sail:7.30-48: -7 |val "to_generic" : forall 'n. bitvector('n, dec) -> vector('n, dec, bit) -  | ^----------------^ -  | bitvector : Int -> Type expected 1 arguments, given 2 +pass/poly_vector/v2.sail:5.5-14: +5 |type bitvector('n, 'ord: Order) = vector('n, 'ord, bit) +  | ^-------^ +  | Cannot define type synonym bitvector, as a type or synonym with that name already exists diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail index b837ac27d..a7e96d319 100644 --- a/test/typecheck/pass/procstate1.sail +++ b/test/typecheck/pass/procstate1.sail @@ -1,10 +1,8 @@ default Order dec -infix 4 == +$include -val operator == = pure {lem: "eq_vec"} : forall 'n. (bitvector('n, dec), bitvector('n, dec)) -> bool - -struct ProcState ('n : Int) = { +struct ProcState('n) = { N : bitvector('n, dec), Z : bitvector(1, dec), C : bitvector(1, dec), diff --git a/test/typecheck/pass/reg_32_64/v3.expect b/test/typecheck/pass/reg_32_64/v3.expect index 49775438f..9e5186a94 100644 --- a/test/typecheck/pass/reg_32_64/v3.expect +++ b/test/typecheck/pass/reg_32_64/v3.expect @@ -17,5 +17,5 @@ Explicit effect annotations are deprecated. They are no longer used and can be r  | * sub_int  | pass/reg_32_64/v3.sail:29.15-17:  | 29 | reg_deref(R)['d - 1 .. 0] -  |  | ^^ checking function argument has type int('ex173#) +  |  | ^^ checking function argument has type int('ex105#)  |  | Cannot re-write sizeof('d) diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail index 2bfbf22ff..c6cee7b26 100644 --- a/test/typecheck/pass/vec_pat1.sail +++ b/test/typecheck/pass/vec_pat1.sail @@ -1,12 +1,12 @@ default Order inc -val bv_add = pure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). +val bv_add = pure {ocaml: "add_vec", lem: "add_vec"}: forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc) -val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. +val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_inc"}: forall 'l 'm 'o, 'l >= 0 & 'm <= 'o & 'o <= 'l. (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o + 1 - 'm, inc) -val bitvector_concat = pure {ocaml: "append", lem: "concat_vec"} : forall ('m : Int) ('p : Int). +val bitvector_concat = pure {ocaml: "append", lem: "concat_vec"} : forall 'm 'p. (bitvector('m, inc), bitvector('p, inc)) -> bitvector('m + 'p, inc) val eq_vec = pure {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bool diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail index 88d4bea83..24cde45b4 100644 --- a/test/typecheck/pass/vector_subrange_gen.sail +++ b/test/typecheck/pass/vector_subrange_gen.sail @@ -1,10 +1,10 @@ -val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. +val vector_subrange = pure {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) 'm ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o - 'm + 1, inc) val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm) -val bitvector_length = pure "length" : forall ('n : Int). bitvector('n, inc) -> atom('n) +val bitvector_length = pure "length" : forall ('n : Int), 'n >= 0. bitvector('n, inc) -> atom('n) overload __size = {bitvector_length} diff --git a/test/typecheck/pass/wf_specs/wf_specs.expect b/test/typecheck/pass/wf_specs/wf_specs.expect index ba6a8df22..700f37819 100644 --- a/test/typecheck/pass/wf_specs/wf_specs.expect +++ b/test/typecheck/pass/wf_specs/wf_specs.expect @@ -7,4 +7,4 @@  | Caused by pass/wf_specs/wf_specs.sail:10.25-35:  | 10 |val f : bits(32) -> bits(THIRTY_TWO)  |  | ^--------^ -  |  | Undefined type synonym THIRTY_TWO +  |  | Undefined numeric type THIRTY_TWO diff --git a/test/typecheck/pass/while_MM.sail b/test/typecheck/pass/while_MM.sail index d0cbc8e50..69a012e0e 100644 --- a/test/typecheck/pass/while_MM.sail +++ b/test/typecheck/pass/while_MM.sail @@ -2,7 +2,7 @@ default Order dec val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int -val add_vec_int : forall ('n : Int) ('ord : Order). +val add_vec_int : forall 'n ('ord : Order). (bitvector('n, 'ord), int) -> bitvector('n, 'ord) overload operator + = {add_vec_int, add_int} diff --git a/test/typecheck/run_tests.py b/test/typecheck/run_tests.py index 622bb9b3f..85aa882d0 100755 --- a/test/typecheck/run_tests.py +++ b/test/typecheck/run_tests.py @@ -37,15 +37,15 @@ def test_pass(): continue tests[filename] = os.fork() if tests[filename] == 0: - step('{} -no_memo_z3 -just_check -ddump_tc_ast pass/{} 1> rtpass/{}'.format(sail, filename, filename)) - step('{} -no_memo_z3 -just_check -ddump_tc_ast -dmagic_hash -dno_cast rtpass/{} 1> rtpass2/{}'.format(sail, filename, filename)) + step('{} --no-memo-z3 --just-check --strict-bitvector --ddump-tc-ast pass/{} 1> rtpass/{}'.format(sail, filename, filename)) + step('{} --no-memo-z3 --just-check --strict-bitvector --ddump-tc-ast --dmagic-hash rtpass/{} 1> rtpass2/{}'.format(sail, filename, filename)) step('diff rtpass/{} rtpass2/{}'.format(filename, filename)) i = 0 variantdir = os.path.join('pass', basename); for variantname in os.listdir(variantdir) if os.path.isdir(variantdir) else []: if re.match('.+\.sail$', variantname): variantbasename = os.path.splitext(os.path.basename(variantname))[0] - step('{} -no_memo_z3 pass/{}/{} 2> pass/{}/{}.error'.format(sail, basename, variantname, basename, variantbasename), expected_status = 1) + step('{} --no-memo-z3 --strict-bitvector pass/{}/{} 2> pass/{}/{}.error'.format(sail, basename, variantname, basename, variantbasename), expected_status = 1) step('diff pass/{}/{}.error pass/{}/{}.expect'.format(basename, variantbasename, basename, variantbasename)) step('rm pass/{}/{}.error'.format(basename, variantbasename)) i = i + 1 @@ -83,7 +83,7 @@ def test_fail(): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: - step('{} -no_memo_z3 fail/{} 2> fail/{}.error'.format(sail, filename, basename), expected_status = 1) + step('{} --no-memo-z3 --strict-bitvector fail/{} 2> fail/{}.error'.format(sail, filename, basename), expected_status = 1) step('diff fail/{}.error fail/{}.expect'.format(basename, basename)) step('rm fail/{}.error'.format(basename)) print_ok(filename)