Fix bitvector update order for bitfield and single bit updates

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

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
 

test/c/bv_update_order.expect

@@ -0,0 +1,3 @@
+0x6
+0x6
+0x0

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();
+}