Skip to content

Commit

Permalink
Fix bitvector update order for bitfield and single bit updates
Browse files Browse the repository at this point in the history
Fixes #1101
  • Loading branch information
Alasdair committed Mar 4, 2025
1 parent 89a3b5e commit 513acd9
Show file tree
Hide file tree
Showing 3 changed files with 39 additions and 2 deletions.
6 changes: 4 additions & 2 deletions src/lib/type_check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3842,12 +3842,14 @@ and infer_vector_update l env v n exp =
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
v (List.rev 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
List.fold_left
(fun v (n, exp, l) -> mk_exp ~loc:l (E_app (mk_id "vector_update", [v; n; exp])))
v (List.rev updates)
in
infer_exp env update_exp

Expand Down
3 changes: 3 additions & 0 deletions test/c/bv_update_order.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
0x6
0x6
0x0
32 changes: 32 additions & 0 deletions test/c/bv_update_order.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
default Order dec

$include <prelude.sail>

bitfield Foo : bits(4) = {
A : 3 .. 0,
B : 3 .. 0
}

function foo() -> unit = {
let x = Mk_Foo(sail_zeros(4));
let y = [x with A = 0x5, B = 0x6];
print_endline(bits_str(y[A]))
}

function bar() -> unit = {
let x = sail_zeros(4);
let y = [x with 3 .. 0 = 0x5, 3 .. 0 = 0x6];
print_endline(bits_str(y[3 .. 0]))
}

function baz() -> unit = {
let x = sail_zeros(4);
let y = [x with 0 = bitone, 0 = bitzero];
print_endline(bits_str(y[3 .. 0]))
}

function main() -> unit = {
foo();
bar();
baz();
}

0 comments on commit 513acd9

Please sign in to comment.