From cb81c648f4e3be6880e9141f641cb79a43f5a919 Mon Sep 17 00:00:00 2001
From: Alasdair <alasdair.armstrong@cl.cam.ac.uk>
Date: Tue, 4 Mar 2025 16:59:13 +0000
Subject: [PATCH] Fix bitvector update order for bitfield and single bit
 updates

Fixes #1101
---
 doc/asciidoc/language.adoc    |  3 +++
 src/lib/type_check.ml         |  6 ++++--
 test/c/bv_update_order.expect |  3 +++
 test/c/bv_update_order.sail   | 32 ++++++++++++++++++++++++++++++++
 4 files changed, 42 insertions(+), 2 deletions(-)
 create mode 100644 test/c/bv_update_order.expect
 create mode 100644 test/c/bv_update_order.sail

diff --git a/doc/asciidoc/language.adoc b/doc/asciidoc/language.adoc
index cfb226dcf..16f60accb 100644
--- a/doc/asciidoc/language.adoc
+++ b/doc/asciidoc/language.adoc
@@ -1082,6 +1082,9 @@ using the field names rather than numeric indices:
 
 sail::bitfield_update_example[from=bitf,type=function]
 
+In the case of overlapping fields, the vector update notion will
+update the fields in order from left to right.
+
 Older versions of Sail did not guarantee the underlying representation
 of the bitfield (because it tried to do clever things to optimise
 them). This meant that bitfields had to be accessed using getter and
diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml
index ef1b05015..bd442c8ca 100644
--- a/src/lib/type_check.ml
+++ b/src/lib/type_check.ml
@@ -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
 
diff --git a/test/c/bv_update_order.expect b/test/c/bv_update_order.expect
new file mode 100644
index 000000000..0a4912faf
--- /dev/null
+++ b/test/c/bv_update_order.expect
@@ -0,0 +1,3 @@
+0x6
+0x6
+0x0
diff --git a/test/c/bv_update_order.sail b/test/c/bv_update_order.sail
new file mode 100644
index 000000000..582365a29
--- /dev/null
+++ b/test/c/bv_update_order.sail
@@ -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();
+}