diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-17 11:26:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-17 11:26:22 +0200 |
| commit | 6c34468898e3726b53c875023730fae7caaf88ee (patch) | |
| tree | 4c179bd1514b6c1168f2c5fa0132e4e85e898ce2 /arm/Asm.v | |
| parent | 82c4547961d567003a83d6c489e06f1271e80a7f (diff) | |
| download | compcert-kvx-6c34468898e3726b53c875023730fae7caaf88ee.tar.gz compcert-kvx-6c34468898e3726b53c875023730fae7caaf88ee.zip | |
ARM port: replace Psavelr pseudo-instruction by actual instructions
Saving the return address register (R14) in the function prologue can be done either with a single "str" instruction if the offset is small enough, or by constructing the address using the R12 register as a temporary then storing with "str" relative to R12.
R12 can be used as a temporary because it is marked as destroyed at function entry. We just need to tell Asmgen.translcode whether R12 still contains the back link left there by Pallocframe, or R12 was trashed. In the latter case R12 will be reloaded from the stack at the next Mgetparam instruction.
Diffstat (limited to 'arm/Asm.v')
| -rw-r--r-- | arm/Asm.v | 15 |
1 files changed, 0 insertions, 15 deletions
@@ -201,7 +201,6 @@ Inductive instruction : Type := (* Pseudo-instructions *) | Pallocframe: Z -> ptrofs -> instruction (**r allocate new stack frame *) | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous frame *) - | Psavelr: ptrofs -> instruction (**r store link register in allocated stack frame *) | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> ptrofs -> instruction (**r load the address of a symbol *) | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *) @@ -270,18 +269,6 @@ lbl: .word symbol >> Again, our memory model cannot comprehend that this operation frees (logically) the current stack frame. -- [Psavelr pos]: this pseudo-instruction stores the link register in the - stackframe at the specified position. It handles out-of-range offsets, - i.e. the generated code for in-range offsets is: -<< - str lr, [sp, #pos] ->> - and for out-of-range offsets: -<< - add sp, sp, #pos (* code to expand the immediate *) - str lr, [sp] - sub sp, sp, #pos (* code to expand the immediate *) ->> - [Pbtbl reg table]: this is a N-way branch, implemented via a jump table as follows: << @@ -750,8 +737,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | _ => Stuck end end - | Psavelr pos => - exec_store Mint32 (Val.offset_ptr rs#IR13 pos) IR14 rs m | Plabel lbl => Next (nextinstr rs) m | Ploadsymbol r1 lbl ofs => |