diff options
| author | Brian Campbell | 2019-05-17 17:59:03 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-05-19 18:40:26 +0100 |
| commit | 8bed4e4ef414f93e02f28f0e5eb223a855ba3d14 (patch) | |
| tree | 9b46de2f4c356431161a24ab10db336f53cc7472 /src | |
| parent | f0b547154b3d2ce9e4bac74b0c56f20d6db76cd2 (diff) | |
Add constraints to undefined vector functions to ensure that lengths are
sane, and an incomplete check on undefined literals.
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 6 | ||||
| -rw-r--r-- | src/type_check.ml | 13 |
2 files changed, 15 insertions, 4 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 522faab7..3f5592ba 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -923,9 +923,9 @@ let undefined_builtin_val_specs = extern_of_string (mk_id "undefined_string") "unit -> string effect {undef}"; extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; - extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}"; - (* Only used with lem_mwords *) - extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}"; + extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order), 'n >= 0. (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}"; + (* Only used with lem_mwords or coq *) + extern_of_string (mk_id "undefined_bitvector") "forall 'n, 'n >= 0. atom('n) -> vector('n, dec, bit) effect {undef}"; extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"] let generate_undefineds vs_ids (Defs defs) = diff --git a/src/type_check.ml b/src/type_check.ml index 2be68ade..3b42e4fa 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2900,7 +2900,18 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ else typ_error env l "List length didn't match" (* FIXME: improve error message *) | E_lit (L_aux (L_undef, _) as lit), _ -> if is_typ_monomorphic typ || Env.polymorphic_undefineds env - then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef]) + then + (* This is a bit of a stop-gap measure; TODO: check undefined + literals for types that contain embedded vectors. *) + let () = + match destruct_vec_typ l env typ with + | (len, _, _) -> + if prove __POS__ env (nc_gteq len (nint 0)) + then () + else typ_error env l "Unable to prove that undefined vector has non-negative length" + | exception _ -> () + in + annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef]) else typ_error env l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction") | _, _ -> let inferred_exp = irule infer_exp env exp in |