diff options
Diffstat (limited to 'arm/Asmgen.v')
| -rw-r--r-- | arm/Asmgen.v | 32 |
1 files changed, 25 insertions, 7 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v index e7a3b4fa..ed64e2f0 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -162,7 +162,7 @@ Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code) (** Smart constructors for integer immediate arguments. *) -Definition loadimm_thumb (r: ireg) (n: int) (k: code) := +Definition loadimm_word (r: ireg) (n: int) (k: code) := let hi := Int.shru n (Int.repr 16) in if Int.eq hi Int.zero then Pmovw r n :: k @@ -177,8 +177,8 @@ Definition loadimm (r: ireg) (n: int) (k: code) := Pmov r (SOimm n) :: k else if Nat.leb l2 1%nat then Pmvn r (SOimm (Int.not n)) :: k - else if thumb tt then - loadimm_thumb r n k + else if Archi.thumb2_support then + loadimm_word r n k else if Nat.leb l1 l2 then iterate_op (Pmov r) (Porr r r) d1 k else @@ -365,14 +365,14 @@ Definition transl_op OK (addimm r IR13 (Ptrofs.to_int n) k) | Ocast8signed, a1 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; - OK (if thumb tt then + OK (if Archi.thumb2_support then Psbfx r r1 Int.zero (Int.repr 8) :: k else Pmov r (SOlsl r1 (Int.repr 24)) :: Pmov r (SOasr r (Int.repr 24)) :: k) | Ocast16signed, a1 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; - OK (if thumb tt then + OK (if Archi.thumb2_support then Psbfx r r1 Int.zero (Int.repr 16) :: k else Pmov r (SOlsl r1 (Int.repr 16)) :: @@ -602,6 +602,22 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : Error (msg "Asmgen.storeind") end. +(** This is a variant of [storeind] that is used to save the return address + at the beginning of a function. It uses [R12] instead of [R14] as + temporary register. *) + +Definition save_lr (ofs: ptrofs) (k: code) := + let n := Ptrofs.to_int ofs in + let n1 := mk_immed_mem_word n in + if Int.eq n n1 + then Pstr IR14 IR13 (SOimm n) :: k + else addimm IR12 IR13 (Int.sub n n1) (Pstr IR14 IR12 (SOimm n1) :: k). + +Definition save_lr_preserves_R12 (ofs: ptrofs) : bool := + let n := Ptrofs.to_int ofs in + let n1 := mk_immed_mem_word n in + Int.eq n n1. + (** Translation of memory accesses *) Definition transl_memory_access @@ -787,10 +803,12 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - do c <- transl_code f f.(Mach.fn_code) true; + do c <- transl_code f f.(Mach.fn_code) + (save_lr_preserves_R12 f.(fn_retaddr_ofs)); OK (mkfunction f.(Mach.fn_sig) (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pstr IR14 IR13 (SOimm (Ptrofs.to_int f.(fn_retaddr_ofs))) :: c)). + save_lr f.(fn_retaddr_ofs) + (Pcfi_rel_offset (Ptrofs.to_int f.(fn_retaddr_ofs)):: c))). Definition transf_function (f: Mach.function) : res Asm.function := do tf <- transl_function f; |