Fixes for C RTS for aarch64 no it's split into multiple files

Fix a bug involving indentifers on the left hand side of assignment
statements not being shadowed correctly within foreach loops.

Make the different between different types of integer division
explicit in at least the C compilation for now. fdiv_int is division
rounding towards -infinity (floor). while tdiv_int is truncating
towards zero. Same for fmod_int and tmod_int.

2 files changed, 63 insertions, 0 deletions

diff --git a/test/c/assign_rename_bug.expect b/test/c/assign_rename_bug.expect
new file mode 100644
index 00000000..ef2503c0
--- /dev/null
+++ b/test/c/assign_rename_bug.expect
@@ -0,0 +1,28 @@
+0xFFF0000000001
+0xFFF0000000001
+0xFFEFFFFFFFFFF
+0xFFEFFFFFFFFFF
+0xFFF0000000002
+0xFFF0000000002
+0xFFEFFFFFFFFFE
+0xFFEFFFFFFFFFE
+0xFFF0000000003
+0xFFF0000000003
+0xFFEFFFFFFFFFD
+0xFFEFFFFFFFFFD
+0xFFF0000000004
+0xFFF0000000004
+0xFFEFFFFFFFFFC
+0xFFEFFFFFFFFFC
+0xFFF0000000005
+0xFFF0000000005
+0xFFEFFFFFFFFFB
+0xFFEFFFFFFFFFB
+0xFFF0000000006
+0xFFF0000000006
+0xFFEFFFFFFFFFA
+0xFFEFFFFFFFFFA
+0xFFF0000000007
+0xFFF0000000007
+0xFFEFFFFFFFFF9
+0xFFEFFFFFFFFF9
diff --git a/test/c/assign_rename_bug.sail b/test/c/assign_rename_bug.sail
new file mode 100644
index 00000000..8b74df2a
--- /dev/null
+++ b/test/c/assign_rename_bug.sail
@@ -0,0 +1,35 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+
+$include <exception_basic.sail>
+
+val sub_vec_int = {
+  ocaml: "sub_vec_int",
+  lem: "sub_vec_int",
+  c: "sub_bits_int"
+} : forall 'n. (bits('n), int) -> bits('n)
+
+overload operator - = {sub_vec_int}
+
+val print_bits52: (string, bits(52)) -> unit
+
+function print_bits52(str, x) = print_bits(str, x)
+
+val main : unit -> unit effect {undef}
+
+function main() = {
+  let addr : bits(52) = 0xF_FF00_0000_0000;
+  i : int = undefined;
+  size : int = 7;
+  ret : unit = ();
+  foreach (i from 1 to size by 1 in inc) {
+    ret = print_bits("", addr + i);
+    ret = print_bits52("", addr + i);
+    ret = print_bits("", addr - i);
+    ret = print_bits52("", addr - i);
+  };
+  return ret
+}