diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-07 19:35:02 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-07 19:35:02 +0200 |
| commit | 73e20bd6e0586e38fbc7d87d8c306fad7b578418 (patch) | |
| tree | 3b4ffcfd6ab4df231a2fa66716fa58b4d5ab1b76 /powerpc/Asm.v | |
| parent | 76d82e41797ef79531e6bf3d530f380dddd3310e (diff) | |
| download | compcert-kvx-73e20bd6e0586e38fbc7d87d8c306fad7b578418.tar.gz compcert-kvx-73e20bd6e0586e38fbc7d87d8c306fad7b578418.zip | |
Added builtins for call frame and return address.
This builtins can be used to get the call frame address and the return
address. To correctly compute the load address of the return address
the allocframe is extended to contain the offset of the return address.
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 2ad99304..796bad3d 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -142,7 +142,7 @@ Inductive instruction : Type := | Paddic: ireg -> ireg -> constant -> instruction (**r add immediate and set carry *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) | Paddze: ireg -> ireg -> instruction (**r add carry *) - | Pallocframe: Z -> int -> instruction (**r allocate new stack frame (pseudo) *) + | Pallocframe: Z -> int -> int -> instruction (**r allocate new stack frame (pseudo) *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) @@ -324,7 +324,7 @@ lbl: .double floatcst lfd rdst, 0(r1) addi r1, r1, 8 >> -- [Pallocframe sz ofs]: in the formal semantics, this pseudo-instruction +- [Pallocframe sz ofs retofs]: in the formal semantics, this pseudo-instruction allocates a memory block with bounds [0] and [sz], stores the value of register [r1] (the stack pointer, by convention) at offset [ofs] in this block, and sets [r1] to a pointer to the bottom of this @@ -623,7 +623,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Paddze rd r1 => Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m - | Pallocframe sz ofs => + | Pallocframe sz ofs _ => let (m1, stk) := Mem.alloc m 0 sz in let sp := Vptr stk Int.zero in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with |