From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'arm/Asm.v') diff --git a/arm/Asm.v b/arm/Asm.v index 7ea1a8a3..051b7e47 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -165,8 +165,8 @@ Inductive instruction : Type := | Psufd: freg -> freg -> freg -> instruction (**r float subtraction *) (* Pseudo-instructions *) - | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) - | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) + | Pallocframe: Z -> int -> instruction (**r allocate new stack frame *) + | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) @@ -186,20 +186,20 @@ lbl: .word symbol >> Initialized data in the constant data section are not modeled here, which is why we use a pseudo-instruction for this purpose. -- [Pallocframe lo hi pos]: in the formal semantics, this pseudo-instruction - allocates a memory block with bounds [lo] and [hi], stores the value +- [Pallocframe sz pos]: in the formal semantics, this pseudo-instruction + allocates a memory block with bounds [0] and [sz], stores the value of the stack pointer at offset [pos] in this block, and sets the stack pointer to the address of the bottom of this block. In the printed ASM assembly code, this allocation is: << mov r12, sp - sub sp, sp, #(hi - lo) + sub sp, sp, #sz str r12, [sp, #pos] >> This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed following a stack discipline. -- [Pfreeframe pos]: in the formal semantics, this pseudo-instruction +- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction reads the word at [pos] of the block pointed by the stack pointer, frees this block, and sets the stack pointer to the value read. In the printed ASM assembly code, this freeing @@ -494,20 +494,20 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Psufd r1 r2 r3 => OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m (* Pseudo-instructions *) - | Pallocframe lo hi pos => - let (m1, stk) := Mem.alloc m lo hi in - let sp := (Vptr stk (Int.repr lo)) in + | Pallocframe sz pos => + 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 pos)) rs#IR13 with | None => Error - | Some m2 => OK (nextinstr (rs#IR13 <- sp)) m2 + | Some m2 => OK (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2 end - | Pfreeframe lo hi pos => + | Pfreeframe sz pos => match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with | None => Error | Some v => match rs#IR13 with | Vptr stk ofs => - match Mem.free m stk lo hi with + match Mem.free m stk 0 sz with | None => Error | Some m' => OK (nextinstr (rs#IR13 <- v)) m' end @@ -521,7 +521,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pbtbl r tbl => match rs#r with | Vint n => - let pos := Int.signed n in + let pos := Int.unsigned n in if zeq (Zmod pos 4) 0 then match list_nth_z tbl (pos / 4) with | None => Error -- cgit