From b6ba61c4c7df3f173f7aad2d96d8927d1a525fe3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Dec 2022 19:33:03 +0100 Subject: 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. --- arm/Asmgen.v | 6 +++--- 1 file 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. -- cgit