From 3eadd260f7382f98eb7dcbd706a3ed3e910167eb Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 10 Jun 2019 17:53:58 +0100 Subject: Add well-formedness check for type schemes in valspecs. Fixes #47. Also adjust the nexp substitution so that the error message points to a useful location, and replace the empty environment with the initial environment in a few functions that do type checking to ensure that the prover is set up (which may be needed for the wf check). --- src/ast_util.ml | 8 +++++++- src/monomorphise.ml | 2 +- src/rewrites.ml | 6 +++--- src/type_check.ml | 10 ++++++++-- test/typecheck/pass/Replicate/v2.expect | 2 +- test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/existential_ast3/v1.expect | 8 ++++---- test/typecheck/pass/existential_ast3/v2.expect | 8 ++++---- test/typecheck/pass/existential_ast3/v3.expect | 2 +- test/typecheck/pass/if_infer/v1.expect | 4 ++-- test/typecheck/pass/if_infer/v2.expect | 4 ++-- test/typecheck/pass/wf_specs.sail | 11 +++++++++++ test/typecheck/pass/wf_specs/wf_specs.expect | 6 ++++++ test/typecheck/pass/wf_specs/wf_specs.sail | 10 ++++++++++ 14 files changed, 61 insertions(+), 22 deletions(-) create mode 100644 test/typecheck/pass/wf_specs.sail create mode 100644 test/typecheck/pass/wf_specs/wf_specs.expect create mode 100644 test/typecheck/pass/wf_specs/wf_specs.sail diff --git a/src/ast_util.ml b/src/ast_util.ml index 7a42950c..1f550c73 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1855,7 +1855,13 @@ let order_subst_aux sv subst = function let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst ord, l) -let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l) +let rec nexp_subst sv subst = function + | (Nexp_aux (Nexp_var kid, l)) as nexp -> + begin match subst with + | A_aux (A_nexp n, _) when Kid.compare kid sv = 0 -> n + | _ -> nexp + end + | Nexp_aux (nexp, l) -> Nexp_aux (nexp_subst_aux sv subst nexp, l) and nexp_subst_aux sv subst = function | Nexp_var kid -> begin match subst with diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 93579420..8670139f 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3439,7 +3439,7 @@ let add_bitvector_casts (Defs defs) = mk_val_spec (VS_val_spec (ts,name,[("_", "zeroExtend")],false)) in let defs = List.map mkfn (IdSet.elements !specs_required) in - check Env.empty (Defs defs) + check initial_env (Defs defs) in Defs (cast_specs @ defs) end diff --git a/src/rewrites.ml b/src/rewrites.ml index 4ea52c4d..e3864a7f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1440,7 +1440,7 @@ let rewrite_defs_exp_lift_assign env defs = rewrite_defs_base write_reg_ref (vector_access (GPR, i)) exp *) let rewrite_register_ref_writes (Defs defs) = - let (Defs write_reg_spec) = fst (Type_error.check Env.empty (Defs (List.map gen_vs + let (Defs write_reg_spec) = fst (Type_error.check initial_env (Defs (List.map gen_vs [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")]))) in let lexp_ref_exp (LEXP_aux (_, annot) as lexp) = try @@ -1630,7 +1630,7 @@ let rewrite_defs_early_return env (Defs defs) = FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, List.map (rewrite_funcl_early_return rewriters) funcls), a) in - let (Defs early_ret_spec) = fst (Type_error.check Env.empty (Defs [gen_vs + let (Defs early_ret_spec) = fst (Type_error.check initial_env (Defs [gen_vs ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in rewrite_defs_base @@ -3771,7 +3771,7 @@ let rewrite_defs_remove_superfluous_returns env = let rewrite_defs_remove_e_assign env (Defs defs) = - let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs + let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars"); ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); diff --git a/src/type_check.ml b/src/type_check.ml index 9c37f5c9..02e32f4d 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -825,10 +825,11 @@ end = struct | A_typ typ -> wf_typ ~exs:exs env typ | A_order ord -> wf_order env ord | A_bool nc -> wf_constraint ~exs:exs env nc - and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) = + and wf_nexp ?exs:(exs=KidSet.empty) env nexp = wf_debug "nexp" string_of_nexp nexp exs; + let Nexp_aux (nexp_aux, l) = expand_nexp_synonyms env nexp in match nexp_aux with - | Nexp_id _ -> () + | Nexp_id id -> typ_error env l ("Undefined synonym " ^ string_of_id id) | Nexp_var kid when KidSet.mem kid exs -> () | Nexp_var kid -> begin match get_typ_var kid env with @@ -1324,6 +1325,10 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t = let expand_bind_synonyms l env (typq, typ) = typq, Env.expand_synonyms (add_typquant l typq env) typ +let wf_typschm env (TypSchm_aux (TypSchm_ts (typq, typ), l)) = + let env = add_typquant l typq env in + Env.wf_typ env typ + (* Create vectors with the default order from the environment *) let default_order_error_string = @@ -4899,6 +4904,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) = let vs, id, typq, typ, env = match vs with | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, exts, is_cast) -> typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); + wf_typschm env typschm; let env = Env.add_extern id exts env in let env = if is_cast then Env.add_cast id env else env in let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index acadd4e2..89ab2910 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v2.sail]:13:4-30 13 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex119# : Int), true. vector(('M * 'ex119#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex172# : Int), true. vector(('M * 'ex172#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 7bb8a4ab..56b89364 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * datasize('ex196#) +  | * datasize('ex248#)  | diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index 4b9bd7cc..346b7b75 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))  | Coercion failed because: -  | (int(33), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#)) +  | (int(33), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#))  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex153# bound here +  |  | 'ex205# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex154# bound here +  |  | 'ex206# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex158# bound here +  |  | 'ex210# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 52eb2f13..7f18c94e 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))  | Coercion failed because: -  | (int(31), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#)) +  | (int(31), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#))  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex153# bound here +  |  | 'ex205# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex154# bound here +  |  | 'ex206# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex158# bound here +  |  | 'ex210# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 0e43cd52..585cf2c6 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25 | Some(Ctor(64, unsigned(0b0 @ b @ a)))  | ^-----------------------------^  | Could not resolve quantifiers for Ctor -  | * (datasize(64) & (0 <= 'ex197# & ('ex197# + 1) <= 64)) +  | * (datasize(64) & (0 <= 'ex249# & ('ex249# + 1) <= 64))  | diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index 011ecbdf..50bd530d 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex115# & ('ex115# + 1) <= 3) +  | * (0 <= 'ex166# & ('ex166# + 1) <= 3)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex118# & ('ex118# + 1) <= 3) +  | * (0 <= 'ex169# & ('ex169# + 1) <= 3)  | diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index 9a34f688..27b05208 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex115# & ('ex115# + 1) <= 4) +  | * (0 <= 'ex166# & ('ex166# + 1) <= 4)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex118# & ('ex118# + 1) <= 4) +  | * (0 <= 'ex169# & ('ex169# + 1) <= 4)  | diff --git a/test/typecheck/pass/wf_specs.sail b/test/typecheck/pass/wf_specs.sail new file mode 100644 index 00000000..2bacf7e0 --- /dev/null +++ b/test/typecheck/pass/wf_specs.sail @@ -0,0 +1,11 @@ +/* Example from https://github.com/rems-project/sail/issues/47 where a variable + name is mistakenly used at the type level, which wasn't caught before due to + the lack of a well-formedness check on specs. This is the corrected version. + */ + +default Order dec +$include + +let 'THIRTY_TWO : atom(32) = 32 + +val f : bits(32) -> bits('THIRTY_TWO) diff --git a/test/typecheck/pass/wf_specs/wf_specs.expect b/test/typecheck/pass/wf_specs/wf_specs.expect new file mode 100644 index 00000000..88844e18 --- /dev/null +++ b/test/typecheck/pass/wf_specs/wf_specs.expect @@ -0,0 +1,6 @@ +Type error: +[wf_specs/wf_specs.sail]:10:25-35 +10 |val f : bits(32) -> bits(THIRTY_TWO) +  | ^--------^ +  | Undefined synonym THIRTY_TWO +  | diff --git a/test/typecheck/pass/wf_specs/wf_specs.sail b/test/typecheck/pass/wf_specs/wf_specs.sail new file mode 100644 index 00000000..bb108ee3 --- /dev/null +++ b/test/typecheck/pass/wf_specs/wf_specs.sail @@ -0,0 +1,10 @@ +/* Example from https://github.com/rems-project/sail/issues/47 where a variable + name is mistakenly used at the type level, which wasn't caught before due to + the lack of a well-formedness check on specs. */ + +default Order dec +$include + +let THIRTY_TWO : atom(32) = 32 + +val f : bits(32) -> bits(THIRTY_TWO) -- cgit v1.2.3