Skip to content

Commit

Permalink
Add a better error message for a bitfield with a bits field
Browse files Browse the repository at this point in the history
'bits' is used as the default name for all the bits in a bitfield,
and this would create an error if the user tried to define it as a
user-specified field. However this generated a confusing error message,
as the failure happened when generating the various helper functions.

This commit checks for this earlier and prints a better error
  • Loading branch information
Alasdair committed May 21, 2024
1 parent ac06d86 commit b9f289a
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 0 deletions.
10 changes: 10 additions & 0 deletions src/lib/type_check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4799,6 +4799,16 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list
let ranges =
List.map (fun (f, r) -> (f, expand_range_synonyms r)) ranges |> List.to_seq |> Bindings.of_seq
in
(* This would cause us to fail later, but with a potentially confusing error message *)
Bindings.iter
(fun f _ ->
if Id.compare f (mk_id "bits") = 0 then
typ_error (id_loc f)
"Field with name 'bits' found in bitfield definition.\n\n\
This is used as the default name for all the bits in the bitfield, so should not be \
overridden."
)
ranges;
let def_annot = add_def_attribute l "bitfield" (Some (AD_aux (AD_num size, l))) def_annot in
let defs =
DEF_aux (DEF_type (TD_aux (record_tdef, (l, empty_uannot))), def_annot)
Expand Down
7 changes: 7 additions & 0 deletions test/typecheck/fail/bitfield_bits_field.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Type error:
fail/bitfield_bits_field.sail:6.2-6:
6 | bits : 15 .. 0,
 | ^--^
 | Field with name 'bits' found in bitfield definition.
 |
 | This is used as the default name for all the bits in the bitfield, so should not be overridden.
7 changes: 7 additions & 0 deletions test/typecheck/fail/bitfield_bits_field.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
default Order dec

$include <prelude.sail>

bitfield foo : bits(32) = {
bits : 15 .. 0,
}

0 comments on commit b9f289a

Please sign in to comment.