diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-18 11:23:37 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-18 11:23:37 +0200 |
commit | 52e4d71646c07fe32665696ef27523c48c69f127 (patch) | |
tree | 664d46d350ad90be43f4157dcb452898da1d3192 /arm/Asmgen.v | |
parent | d8dcf41334d7a6ff2d2eaa53f215c80ef26cd517 (diff) | |
parent | f66711dc06c73adf3dd715c564cb6d27b51c5199 (diff) | |
download | compcert-52e4d71646c07fe32665696ef27523c48c69f127.tar.gz compcert-52e4d71646c07fe32665696ef27523c48c69f127.zip |
Merge remote-tracking branch 'private/master'
Diffstat (limited to 'arm/Asmgen.v')
-rw-r--r-- | arm/Asmgen.v | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v index e7a3b4fa..1b96416d 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -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; |