From 5929b9b958a2a2c614782e5d211556fef383cfa5 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 9 Feb 2024 15:18:55 +0000 Subject: [PATCH] Fix typing rule for E_vector_update Potentially means a few less things typecheck, but should be much simpler and avoids bad cases where it could backtrack a lot --- src/lib/type_check.ml | 44 +++++++++++++------- test/typecheck/fail/bv_update_error.expect | 7 ++++ test/typecheck/fail/bv_update_error.sail | 15 +++++++ test/typecheck/pass/vec_length/v2.expect | 5 --- test/typecheck/pass/vec_length/v2_inc.expect | 5 --- 5 files changed, 50 insertions(+), 26 deletions(-) create mode 100644 test/typecheck/fail/bv_update_error.expect create mode 100644 test/typecheck/fail/bv_update_error.sail diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index d89c5be12..0cc1d960d 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -3274,22 +3274,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = ) | exn -> raise exn end - | E_vector_update (v, n, exp) -> begin - try infer_exp env (E_aux (E_app (mk_id "vector_update", [v; n; exp]), (l, uannot))) with - | Type_error (err_l, err) -> ( - try - let inferred_v = infer_exp env v in - begin - match (typ_of inferred_v, n) with - | Typ_aux (Typ_id id, _), E_aux (E_id field, _) -> - let update_id = (Bitfield.field_accessor_ids id field).update in - infer_exp env (mk_exp ~loc:l (E_app (update_id, [v; exp]))) - | _, _ -> typ_error l "Vector update could not be interpreted as a bitfield update" - end - with Type_error (err_l', err') -> typ_raise err_l (err_because (err, err_l', err')) - ) - | exn -> raise exn - end + | E_vector_update (v, n, exp) -> infer_vector_update l env v n exp | E_vector_update_subrange (v, n, m, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update_subrange", [v; n; m; exp]), (l, uannot))) | E_vector_append (v1, E_aux (E_vector [], _)) -> infer_exp env v1 @@ -3371,6 +3356,33 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = and infer_funapp l env f xs ret_ctx_typ = infer_funapp' l env f (Env.get_val_spec f env) xs ret_ctx_typ +and infer_vector_update l env v n exp = + let rec nested_updates acc = function + | E_aux (E_vector_update (v, n, exp), (l, _)) -> nested_updates ((n, exp, l) :: acc) v + | v -> (v, List.rev acc) + in + let v, updates = nested_updates [(n, exp, l)] v in + let inferred_v = infer_exp env v in + match typ_of inferred_v with + | Typ_aux (Typ_id id, _) when Env.is_bitfield id env -> + let update_exp = + List.fold_left + (fun v (field, exp, l) -> + match field with + | E_aux (E_id field_id, (field_id_loc, _)) -> + let (Id_aux (update_name, _)) = (Bitfield.field_accessor_ids id field_id).update in + mk_exp ~loc:l (E_app (Id_aux (update_name, field_id_loc), [v; exp])) + | _ -> typ_error l "Vector update could not be interpreted as a bitfield update" + ) + v updates + in + infer_exp env update_exp + | _ -> + let update_exp = + List.fold_left (fun v (n, exp, l) -> mk_exp ~loc:l (E_app (mk_id "vector_update", [v; n; exp]))) v updates + in + infer_exp env update_exp + and instantiation_of (E_aux (_, (l, tannot)) as exp) = match fst tannot with | Some t -> begin diff --git a/test/typecheck/fail/bv_update_error.expect b/test/typecheck/fail/bv_update_error.expect new file mode 100644 index 000000000..7a0b87e55 --- /dev/null +++ b/test/typecheck/fail/bv_update_error.expect @@ -0,0 +1,7 @@ +Type error: +fail/bv_update_error.sail:13.18-22: +13 | let _ = [v with FIEL = 0xFF]; +  | ^--^ +  | No function type found for _update_b_FIEL +  | +  | Did you mean _update_b_FIELD? diff --git a/test/typecheck/fail/bv_update_error.sail b/test/typecheck/fail/bv_update_error.sail new file mode 100644 index 000000000..bee9aae2d --- /dev/null +++ b/test/typecheck/fail/bv_update_error.sail @@ -0,0 +1,15 @@ +default Order dec + +$include + +bitfield b : bits(32) = { + FIELD : 7 .. 0 +} + +val main : unit -> unit + +function main() = { + let v = Mk_b(0x0000_0000); + let _ = [v with FIEL = 0xFF]; + () +} diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect index c659648bd..305795f88 100644 --- a/test/typecheck/pass/vec_length/v2.expect +++ b/test/typecheck/pass/vec_length/v2.expect @@ -8,8 +8,3 @@  | * (0 <= 10 & 10 < 8)  | * plain_vector_update  | Could not unify vector('n, 'a) and bitvector(8) -  | -  | Caused by pass/vec_length/v2.sail:7.10-25: -  | 7 | let z = [x with 10 = y]; -  |  | ^-------------^ -  |  | Vector update could not be interpreted as a bitfield update diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect index d6c22952d..7160e93ce 100644 --- a/test/typecheck/pass/vec_length/v2_inc.expect +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -8,8 +8,3 @@  | * (0 <= 10 & 10 < 8)  | * plain_vector_update  | Could not unify vector('n, 'a) and bitvector(8) -  | -  | Caused by pass/vec_length/v2_inc.sail:7.10-25: -  | 7 | let z = [x with 10 = y]; -  |  | ^-------------^ -  |  | Vector update could not be interpreted as a bitfield update