ARM code generation: fix offset checks for loads

The check `Int.ltu x Int.zero` is always false, we replace this by using
signed integer comparisons.

We cannot use `Int.sign_ext` because the offsets are not signed
integers but rather unsigned integers plus an additional sign bit.

1 files changed, 3 insertions, 3 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 1a1e7f2f..64bb9c34 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -93,20 +93,20 @@ In particular, if [n] is a representable immediate argument, we should have
 *)
 
 Definition mk_immed_mem_word (x: int): int :=
-  if Int.ltu x Int.zero then
+  if Int.lt x Int.zero then
     Int.neg (Int.zero_ext (if thumb tt then 8 else 12) (Int.neg x))
   else
     Int.zero_ext 12 x.
 
 Definition mk_immed_mem_small (x: int): int :=
-  if Int.ltu x Int.zero then
+  if Int.lt x Int.zero then
     Int.neg (Int.zero_ext 8 (Int.neg x))
   else
     Int.zero_ext 8 x.
 
 Definition mk_immed_mem_float (x: int): int :=
   let x := Int.and x (Int.repr (-4)) in   (**r mask low 2 bits off *)
-  if Int.ltu x Int.zero then
+  if Int.lt x Int.zero then
     Int.neg (Int.zero_ext 10 (Int.neg x))
   else
     Int.zero_ext 10 x.