diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-08-18 11:23:05 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-08-18 11:23:05 +0200 |
| commit | f66711dc06c73adf3dd715c564cb6d27b51c5199 (patch) | |
| tree | e68a132caa6df4bc3215b638dfe83ddf9db7a506 /arm/Asm.v | |
| parent | ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee (diff) | |
| parent | fc1b2bfea598354a3e939de35d270376c880e1b0 (diff) | |
| download | compcert-f66711dc06c73adf3dd715c564cb6d27b51c5199.tar.gz compcert-f66711dc06c73adf3dd715c564cb6d27b51c5199.zip | |
Merge pull request #22 from AbsIntPrivate/arm_large_offsets
Issue #P18: handle large offsets when accessing return address and back link in the stack frame
Diffstat (limited to 'arm/Asm.v')
| -rw-r--r-- | arm/Asm.v | 9 |
1 files changed, 6 insertions, 3 deletions
@@ -199,15 +199,16 @@ Inductive instruction : Type := | Pfsts: freg -> ireg -> int -> instruction (**r float32 store *) (* Pseudo-instructions *) - | Pallocframe: Z -> ptrofs -> instruction (**r allocate new stack frame *) - | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous frame *) - | Plabel: label -> instruction (**r define a code label *) + | Pallocframe: Z -> ptrofs -> instruction (**r allocate new stack frame *) + | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous 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 *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) | Padc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) + | Pcfi_rel_offset: int -> instruction (**r .cfi_rel_offset debug directive *) | Pclz: ireg -> ireg -> instruction (**r count leading zeros. *) | Pfsqrt: freg -> freg -> instruction (**r floating-point square root. *) | Prev: ireg -> ireg -> instruction (**r reverse bytes and reverse bits. *) @@ -757,6 +758,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | _ => Stuck end + | Pcfi_rel_offset ofs => + Next (nextinstr rs) m | Pbuiltin ef args res => Stuck (**r treated specially below *) (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) |