Abstract syntax and semantics for ARM assembly language
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Locations.
Require Stacklayout.
Require Import Conventions.
Require ExtValues.
Require Import Compopts.
Require Import Decidableplus.
Abstract syntax
Integer registers, floating-point registers.
Inductive ireg:
Type :=
|
IR0:
ireg |
IR1:
ireg |
IR2:
ireg |
IR3:
ireg
|
IR4:
ireg |
IR5:
ireg |
IR6:
ireg |
IR7:
ireg
|
IR8:
ireg |
IR9:
ireg |
IR10:
ireg |
IR11:
ireg
|
IR12:
ireg |
IR13:
ireg |
IR14:
ireg.
Inductive freg:
Type :=
|
FR0:
freg |
FR1:
freg |
FR2:
freg |
FR3:
freg
|
FR4:
freg |
FR5:
freg |
FR6:
freg |
FR7:
freg
|
FR8:
freg |
FR9:
freg |
FR10:
freg |
FR11:
freg
|
FR12:
freg |
FR13:
freg |
FR14:
freg |
FR15:
freg.
Inductive sreg:
Type :=
|
SR0:
sreg |
SR1:
sreg |
SR2:
sreg |
SR3:
sreg
|
SR4:
sreg |
SR5:
sreg |
SR6:
sreg |
SR7:
sreg
|
SR8:
sreg |
SR9:
sreg |
SR10:
sreg |
SR11:
sreg
|
SR12:
sreg |
SR13:
sreg |
SR14:
sreg |
SR15:
sreg
|
SR16:
sreg |
SR17:
sreg |
SR18:
sreg |
SR19:
sreg
|
SR20:
sreg |
SR21:
sreg |
SR22:
sreg |
SR23:
sreg
|
SR24:
sreg |
SR25:
sreg |
SR26:
sreg |
SR27:
sreg
|
SR28:
sreg |
SR29:
sreg |
SR30:
sreg |
SR31:
sreg.
Lemma ireg_eq:
forall (
x y:
ireg), {
x=
y} + {
x<>
y}.
Proof.
decide equality. Defined.
Lemma freg_eq:
forall (
x y:
freg), {
x=
y} + {
x<>
y}.
Proof.
decide equality. Defined.
Bits in the condition register.
Inductive crbit:
Type :=
|
CN:
crbit (* negative *)
|
CZ:
crbit (* zero *)
|
CC:
crbit (* carry *)
|
CV:
crbit.
(* overflow *)
Lemma crbit_eq:
forall (
x y:
crbit), {
x=
y} + {
x<>
y}.
Proof.
decide equality. Defined.
We model the following registers of the ARM architecture.
Inductive dreg:
Type :=
|
IR:
ireg ->
dreg (* integer registers *)
|
FR:
freg ->
dreg.
(* double-precision VFP float registers *)
Inductive preg:
Type :=
|
DR:
dreg ->
preg (* data registers *)
|
CR:
crbit ->
preg (* bits in the condition register *)
|
PC:
preg.
(* program counter *)
Coercion IR:
ireg >->
dreg.
Coercion FR:
freg >->
dreg.
Coercion DR:
dreg >->
preg.
Coercion CR:
crbit >->
preg.
Lemma dreg_eq:
forall (
x y:
dreg), {
x=
y} + {
x<>
y}.
Proof.
Lemma preg_eq:
forall (
x y:
preg), {
x=
y} + {
x<>
y}.
Proof.
Module PregEq.
Definition t :=
preg.
Definition eq :=
preg_eq.
End PregEq.
Module Pregmap :=
EMap(
PregEq).
Conventional names for stack pointer (SP) and return address (RA)
Declare Scope asm.
Notation "'SP'" :=
IR13 (
only parsing) :
asm.
Notation "'RA'" :=
IR14 (
only parsing) :
asm.
The instruction set. Most instructions correspond exactly to
actual instructions of the ARM processor. See the ARM
reference manuals for more details. Some instructions,
described below, are pseudo-instructions: they expand to
canned instruction sequences during the printing of the assembly
code. Most instructions are common to Thumb2 and ARM classic.
We use a few Thumb2-specific instructions when available, and avoid
to use ARM classic features that are not in Thumb2.
Definition label :=
positive.
Inductive shift_op :
Type :=
|
SOimm:
int ->
shift_op
|
SOreg:
ireg ->
shift_op
|
SOlsl:
ireg ->
int ->
shift_op
|
SOlsr:
ireg ->
int ->
shift_op
|
SOasr:
ireg ->
int ->
shift_op
|
SOror:
ireg ->
int ->
shift_op.
Definition shift_op_eq :
forall (
x y :
shift_op), {
x =
y} + {
x <>
y}.
Proof.
Inductive testcond :
Type :=
|
TCeq:
testcond (* equal *)
|
TCne:
testcond (* not equal *)
|
TChs:
testcond (* unsigned higher or same *)
|
TClo:
testcond (* unsigned lower *)
|
TCmi:
testcond (* negative *)
|
TCpl:
testcond (* positive *)
|
TChi:
testcond (* unsigned higher *)
|
TCls:
testcond (* unsigned lower or same *)
|
TCge:
testcond (* signed greater or equal *)
|
TClt:
testcond (* signed less than *)
|
TCgt:
testcond (* signed greater *)
|
TCle:
testcond.
(* signed less than or equal *)
Inductive code_constant:
Type :=
|
Float32 :
label ->
float32 ->
code_constant
|
Float64 :
label ->
float ->
code_constant
|
Symbol :
label ->
qualident ->
ptrofs ->
code_constant.
Inductive mcpy_addr:
Type :=
|
Ofs :
int ->
mcpy_addr
|
PostIncr :
int ->
mcpy_addr
|
PreIncr :
int ->
mcpy_addr.
Inductive instruction :
Type :=
|
Padd:
ireg ->
ireg ->
shift_op ->
instruction (* integer addition *)
|
Pand:
ireg ->
ireg ->
shift_op ->
instruction (* bitwise and *)
|
Pasr:
ireg ->
ireg ->
ireg ->
instruction (* arithmetic shift right *)
|
Pb:
label ->
instruction (* branch to label *)
|
Pbc:
testcond ->
label ->
instruction (* conditional branch to label *)
|
Pcbnz:
ireg ->
label ->
instruction (* branch if not zero *)
|
Pcbz:
ireg ->
label ->
instruction (* branch if zero *)
|
Pbsymb:
qualident ->
signature ->
instruction (* branch to symbol *)
|
Pbreg:
ireg ->
signature ->
instruction (* computed branch *)
|
Pblsymb:
qualident ->
signature ->
instruction(* branch and link to symbol *)
|
Pblreg:
ireg ->
signature ->
instruction (* computed branch and link *)
|
Pbic:
ireg ->
ireg ->
shift_op ->
instruction (* bitwise bit-clear *)
|
Pcmp:
ireg ->
shift_op ->
instruction (* integer comparison *)
|
Pcmn:
ireg ->
shift_op ->
instruction (* integer comparison with opposite *)
|
Ptst:
ireg ->
shift_op ->
instruction (* bitwise and, set flags only *)
|
Peor:
ireg ->
ireg ->
shift_op ->
instruction (* bitwise exclusive or *)
|
Pldr:
ireg ->
ireg ->
shift_op ->
instruction (* int32 load *)
|
Pldr_a:
ireg ->
ireg ->
shift_op ->
instruction (* any32 load to int register *)
|
Pldr_u:
ireg ->
ireg ->
shift_op ->
instruction (* int32 unaligned load *)
|
Pldrd:
ireg ->
ireg ->
ireg ->
memory_chunk ->
memory_chunk ->
int ->
instruction (* load double *)
|
Pldrb:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int8 load *)
|
Pldrh:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int16 load *)
|
Pldrsb:
ireg ->
ireg ->
shift_op ->
instruction (* signed int8 load *)
|
Pldrsh:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int16 load *)
|
Plsl:
ireg ->
ireg ->
ireg ->
instruction (* shift left *)
|
Plsr:
ireg ->
ireg ->
ireg ->
instruction (* logical shift right *)
|
Pror:
ireg ->
ireg ->
ireg ->
instruction (* rotate right by register amount *)
|
Pmla:
ireg ->
ireg ->
ireg ->
ireg ->
instruction (* integer multiply-add *)
|
Pmls:
ireg ->
ireg ->
ireg ->
ireg ->
instruction (* integer multiply-subtract *)
|
Pmov:
ireg ->
shift_op ->
instruction (* integer move *)
|
Pmovw:
ireg ->
int ->
instruction (* move 16-bit immediate *)
|
Pmovt:
ireg ->
int ->
instruction (* set high 16 bits *)
|
Pmul:
ireg ->
ireg ->
ireg ->
instruction (* integer multiplication *)
|
Pmvn:
ireg ->
shift_op ->
instruction (* integer complement *)
|
Porr:
ireg ->
ireg ->
shift_op ->
instruction (* bitwise or *)
|
Ppush:
list ireg ->
instruction
|
Prsb:
ireg ->
ireg ->
shift_op ->
instruction (* integer reverse subtraction *)
|
Pubfx:
ireg ->
ireg ->
int ->
int ->
instruction (* unsigned bitfield extract *)
|
Psbfx:
ireg ->
ireg ->
int ->
int ->
instruction (* signed bitfield extract *)
|
Puxtb:
ireg ->
ireg ->
instruction (* unsigned extend byte *)
|
Psxtb:
ireg ->
ireg ->
instruction (* signed extend byte *)
|
Puxth:
ireg ->
ireg ->
instruction (* unsigned extend halfword *)
|
Psxth:
ireg ->
ireg ->
instruction (* signed extend halfword *)
|
Pbfc:
ireg ->
int ->
int ->
instruction
|
Pbfi:
ireg ->
ireg ->
int ->
int ->
instruction
|
Pstr:
ireg ->
ireg ->
shift_op ->
instruction (* int32 store *)
|
Pstr_a:
ireg ->
ireg ->
shift_op ->
instruction (* any32 store from int register *)
|
Pstr_u:
ireg ->
ireg ->
shift_op ->
instruction (* int32 unaligned store *)
|
Pstrd:
ireg ->
ireg ->
ireg ->
memory_chunk ->
memory_chunk ->
int ->
instruction (* store double *)
|
Pstrb:
ireg ->
ireg ->
shift_op ->
instruction (* int8 store *)
|
Pstrh:
ireg ->
ireg ->
shift_op ->
instruction (* int16 store *)
|
Pstm:
ireg ->
list (
ireg *
memory_chunk) ->
instruction (* store multiple int *)
|
Pldm:
ireg ->
list (
ireg *
memory_chunk) ->
instruction (* load multiple int *)
|
Pvstm:
ireg ->
list (
freg *
memory_chunk) ->
instruction (* store multiple VFP-d *)
|
Pvldm:
ireg ->
list (
freg *
memory_chunk) ->
instruction (* load multiple VFP-d *)
|
Psdiv:
ireg ->
ireg ->
ireg ->
instruction (* signed division *)
|
Psmull:
ireg ->
ireg ->
ireg ->
ireg ->
instruction (* signed multiply long *)
|
Psub:
ireg ->
ireg ->
shift_op ->
instruction (* integer subtraction *)
|
Pudiv:
ireg ->
ireg ->
ireg ->
instruction (* unsigned division *)
|
Pumull:
ireg ->
ireg ->
ireg ->
ireg ->
instruction (* unsigned multiply long *)
|
Pfcpyd:
freg ->
freg ->
instruction (* float move *)
|
Pfabsd:
freg ->
freg ->
instruction (* float absolute value *)
|
Pfnegd:
freg ->
freg ->
instruction (* float opposite *)
|
Pfaddd:
freg ->
freg ->
freg ->
instruction (* float addition *)
|
Pfdivd:
freg ->
freg ->
freg ->
instruction (* float division *)
|
Pfmuld:
freg ->
freg ->
freg ->
instruction (* float multiplication *)
|
Pfmlad:
freg ->
freg ->
freg ->
instruction (* float multiplication-add *)
|
Pfmlsd:
freg ->
freg ->
freg ->
instruction (* float multiplication-subtract *)
|
Pfsubd:
freg ->
freg ->
freg ->
instruction (* float subtraction *)
|
Pflid:
freg ->
float ->
instruction (* load float constant *)
|
Pfcmpd:
freg ->
freg ->
instruction (* float comparison *)
|
Pfcmpzd:
freg ->
instruction (* float comparison with 0.0 *)
|
Pfsitod:
freg ->
ireg ->
instruction (* signed int to float *)
|
Pfuitod:
freg ->
ireg ->
instruction (* unsigned int to float *)
|
Pftosizd:
ireg ->
freg ->
instruction (* float to signed int *)
|
Pftouizd:
ireg ->
freg ->
instruction (* float to unsigned int *)
|
Pfabss:
freg ->
freg ->
instruction (* float absolute value *)
|
Pfnegs:
freg ->
freg ->
instruction (* float opposite *)
|
Pfadds:
freg ->
freg ->
freg ->
instruction (* float addition *)
|
Pfdivs:
freg ->
freg ->
freg ->
instruction (* float division *)
|
Pfmuls:
freg ->
freg ->
freg ->
instruction (* float multiplication *)
|
Pfmlas:
freg ->
freg ->
freg ->
instruction (* float multiplication-add *)
|
Pfmlss:
freg ->
freg ->
freg ->
instruction (* float multiplication-subtract *)
|
Pfsubs:
freg ->
freg ->
freg ->
instruction (* float subtraction *)
|
Pflis:
freg ->
float32 ->
instruction (* load float constant *)
|
Pfcmps:
freg ->
freg ->
instruction (* float comparison *)
|
Pfcmpzs:
freg ->
instruction (* float comparison with 0.0 *)
|
Pfsitos:
freg ->
ireg ->
instruction (* signed int to float *)
|
Pfuitos:
freg ->
ireg ->
instruction (* unsigned int to float *)
|
Pftosizs:
ireg ->
freg ->
instruction (* float to signed int *)
|
Pftouizs:
ireg ->
freg ->
instruction (* float to unsigned int *)
|
Pfcvtsd:
freg ->
freg ->
instruction (* round to single precision *)
|
Pfcvtds:
freg ->
freg ->
instruction (* expand to double precision *)
|
Pfldd:
freg ->
ireg ->
int ->
instruction (* float64 load *)
|
Pfldd_a:
freg ->
ireg ->
int ->
instruction (* any64 load to FP reg *)
|
Pflds:
freg ->
ireg ->
int ->
instruction (* float32 load *)
|
Pfstd:
freg ->
ireg ->
int ->
instruction (* float64 store *)
|
Pfstd_a:
freg ->
ireg ->
int ->
instruction (* any64 store from FP reg *)
|
Pfsts:
freg ->
ireg ->
int ->
instruction (* float32 store *)
|
Pallocframe:
Z ->
ptrofs ->
instruction (* allocate new stack frame *)
|
Pfreeframe:
Z ->
ptrofs ->
instruction (* deallocate stack frame and restore previous frame *)
|
Plabel:
label ->
instruction (* define a code label *)
|
Ploadsymbol:
ireg ->
qualident ->
ptrofs ->
instruction (* load the address of a symbol *)
|
Pmovite:
testcond ->
ireg ->
shift_op ->
shift_op ->
instruction (* integer conditional move *)
|
Pfmovite:
testcond ->
freg ->
freg ->
freg ->
instruction (* FP conditional move *)
|
Pbtbl:
ireg ->
list label ->
instruction (* N-way branch through a jump table *)
|
Pbuiltin:
external_function ->
list (
builtin_arg preg) ->
builtin_res preg ->
instruction (* built-in function (pseudo) *)
|
Padc:
ireg ->
ireg ->
shift_op ->
instruction (* add with carry *)
|
Pcfi_adjust:
int ->
instruction (* .cfi_adjust debug directive *)
|
Pcfi_rel_offset:
int ->
instruction (* .cfi_rel_offset debug directive *)
|
Pclz:
ireg ->
ireg ->
instruction (* count leading zeros. *)
|
Prbit:
ireg ->
ireg ->
instruction (* reverse bits. *)
|
Pfsqrtd:
freg ->
freg ->
instruction (* double-precision floating-point square root. *)
|
Pfsqrts:
freg ->
freg ->
instruction (* single-precision floating-point square root. *)
|
Prev:
ireg ->
ireg ->
instruction (* reverse bytes and reverse bits. *)
|
Prev16:
ireg ->
ireg ->
instruction (* reverse bytes and reverse bits. *)
|
Prsc:
ireg ->
ireg ->
shift_op ->
instruction (* reverse subtract without carry. *)
|
Psbc:
ireg ->
ireg ->
shift_op ->
instruction (* subtract with carry *)
|
Pnop :
bool ->
instruction (* nop instruction *)
|
Padds:
ireg ->
ireg ->
shift_op ->
instruction (* integer addition with update of condition flags *)
|
Psubs:
ireg ->
ireg ->
shift_op ->
instruction (* integer subtraction with update of condition flags *)
|
Psbcs:
ireg ->
ireg ->
shift_op ->
instruction (* subtract-with-carry, set condition flags
(ARMv7-A ARM A8.8.157 SBCS). Conceptually:
result_33 = unsigned(Rn) + unsigned(NOT(op2)) + unsigned(APSR.C)
Rd = low 32 bits of result_33
APSR.N = bit_31(Rd)
APSR.Z = (Rd == 0)
APSR.C = bit_32(result_33) (carry-out of the 33-bit add)
APSR.V = signed overflow of (Rn - op2 - (1 - APSR.C))
Equivalently: result = Rn - op2 - (1 - APSR.C) = Rn - op2 - bin
where bin is the borrow-in (= 1 when previous C was clear).
Model verified against hardware (Cortex-A53) over 200k+ probes:
match exact for {N,Z,C,V} and result. *)
|
Prsbs:
ireg ->
ireg ->
shift_op ->
instruction (* integer reverse subtraction with update of condition flags *)
|
Pdmb:
instruction (* data memory barrier *)
|
Pdsb:
instruction (* data synchronization barrier *)
|
Pisb:
instruction (* instruction synchronization barrier *)
|
Pbne:
label ->
instruction (* branch if negative macro *)
|
Pldr_p:
ireg ->
ireg ->
shift_op ->
instruction (* int32 load with post increment *)
|
Pldrb_p:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int8 load with post increment *)
|
Pldrh_p:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int16 load with post increment *)
|
Pstr_p:
ireg ->
ireg ->
shift_op ->
instruction (* int32 store with post increment *)
|
Pstrb_p:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int8 store with post increment *)
|
Pstrh_p:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int16 store with post increment *)
|
Pldr_pi:
ireg ->
ireg ->
shift_op ->
instruction (* int32 load with post increment *)
|
Pldr_api:
ireg ->
ireg ->
shift_op ->
instruction (* any32 load with post increment *)
|
Pldrb_pi:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int8 load with post increment *)
|
Pldrh_pi:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int16 load with post increment *)
|
Pldrsb_pi:
ireg ->
ireg ->
shift_op ->
instruction (* signed int8 load with post increment *)
|
Pldrsh_pi:
ireg ->
ireg ->
shift_op ->
instruction (* signed int16 load with post increment *)
|
Pldrd_pi:
ireg ->
ireg ->
ireg ->
memory_chunk ->
memory_chunk ->
int ->
instruction (* load double with post increment *)
|
Pstr_pi:
ireg ->
ireg ->
shift_op ->
instruction (* int32 store with post increment *)
|
Pstr_api:
ireg ->
ireg ->
shift_op ->
instruction (* any32 store with post increment *)
|
Pstrb_pi:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int8 store with post increment *)
|
Pstrh_pi:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int16 store with post increment *)
|
Pstrd_pi:
ireg ->
ireg ->
ireg ->
memory_chunk ->
memory_chunk ->
int ->
instruction (* store double with post increment *)
|
Pldr_pd:
ireg ->
ireg ->
shift_op ->
instruction (* int32 load with pre-decrement *)
|
Pldr_apd:
ireg ->
ireg ->
shift_op ->
instruction (* any32 load with pre-decrement *)
|
Pldrb_pd:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int8 load with pre-decrement *)
|
Pldrh_pd:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int16 load with pre-decrement *)
|
Pldrsb_pd:
ireg ->
ireg ->
shift_op ->
instruction (* signed int8 load with pre-decrement *)
|
Pldrsh_pd:
ireg ->
ireg ->
shift_op ->
instruction (* signed int16 load with pre-decrement *)
|
Pstr_pd:
ireg ->
ireg ->
shift_op ->
instruction (* int32 store with pre-decrement *)
|
Pstr_apd:
ireg ->
ireg ->
shift_op ->
instruction (* any32 store with pre-decrement *)
|
Pstrb_pd:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int8 store with pre-decrement *)
|
Pstrh_pd:
ireg ->
ireg ->
shift_op ->
instruction (* unsigned int16 store with pre-decrement *)
|
Pfcpy_fs:
freg ->
sreg ->
instruction (* single precision float move for incoming arguments *)
|
Pfcpy_sf:
sreg ->
freg ->
instruction (* single precision float move for outgoing arguments *)
|
Pfcpy_fii:
freg ->
ireg ->
ireg ->
instruction (* copy integer register pair to double fp-register *)
|
Pfcpy_fi:
freg ->
ireg ->
instruction (* copy integer register to single fp-register *)
|
Pfcpy_iif:
ireg ->
ireg ->
freg ->
instruction (* copy double fp-register to integer register pair *)
|
Pfcpy_if:
ireg ->
freg ->
instruction (* copy single fp-register to integer register *)
|
Pconstants:
list code_constant ->
instruction (* constants in code *)
|
Ploadsymbol_imm:
ireg ->
qualident ->
ptrofs ->
instruction (* move symbol address in register *)
|
Pflid_lbl:
freg ->
label ->
float ->
instruction (* load float64 from label *)
|
Pflis_lbl:
freg ->
label ->
float32 ->
instruction (* load float32 from label *)
|
Pflid_imm:
freg ->
float ->
instruction (* move float64 into register *)
|
Pflis_imm:
freg ->
float32 ->
instruction (* move float32 into register *)
|
Ploadsymbol_lbl:
ireg ->
label ->
qualident ->
ptrofs ->
instruction (* load symbol address from label *)
|
Pbits_of_single :
ireg ->
freg ->
instruction
|
Psingle_of_bits :
freg ->
ireg ->
instruction
|
Phibits_of_float:
ireg ->
freg ->
instruction
|
Pgetcanary (
rd:
ireg)
|
Pstack_chk_fail
|
Pmemcpy8:
ireg ->
ireg ->
mcpy_addr ->
mcpy_addr ->
ireg ->
instruction (* byte memory copy *)
|
Pmemcpy16:
ireg ->
ireg ->
mcpy_addr ->
mcpy_addr ->
ireg ->
instruction (* halfword memory copy *)
|
Pmemcpy32:
ireg ->
ireg ->
mcpy_addr ->
mcpy_addr ->
ireg ->
instruction (* word memory copy *)
|
Pmemcpy64:
ireg ->
ireg ->
mcpy_addr ->
mcpy_addr ->
ireg ->
ireg ->
instruction (* doubleword memory copy *)
|
Pmemcpyf64:
ireg ->
ireg ->
freg ->
int ->
int ->
instruction.
(* doubleword memory copy *)
The pseudo-instructions are the following:
-
Plabel: define a code label at the current program point.
-
Ploadsymbol: load the address of a symbol in an integer register.
Expands to a load from an address in the constant data section
initialized with the symbol value:
ldr rdst, lbl
.const_data
lbl: .word symbol
.text
Initialized data in the constant data section are not modeled here,
which is why we use a pseudo-instruction for this purpose.
-
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 r10, sp
sub sp, sp, #sz
str r10, [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 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
is just a load of register sp relative to sp itself:
ldr sp, [sp, #pos]
Again, our memory model cannot comprehend that this operation
frees (logically) the current stack frame.
-
Pbtbl reg table: this is a N-way branch, implemented via a jump table
as follows:
ldr pc, [pc, reg]
mov r0, r0 (* no-op *)
.word table[0], table[1], ...
Note that reg contains 4 times the index of the desired table entry.
In Thumb2 mode, if -ffast-jumptables (default) is set, and there are no
negative offsets, the tbh instruction is used instead.
:=
list instruction.
Record function :
Type :=
mkfunction {
fn_sig:
signature;
fn_code:
code }.
Definition fundef :=
AST.fundef function.
Definition program :=
AST.program fundef unit.
Operational semantics
The semantics operates over a single mapping from registers
(type preg) to values. We maintain (but do not enforce)
the convention that integer registers are mapped to values of
type Tint, float registers to values of type Tfloat,
and condition bits to either Vzero or Vone.
Definition regset :=
Pregmap.t val.
Definition genv :=
Genv.t fundef unit.
Notation "a # b" := (
a b) (
at level 1,
only parsing) :
asm.
Notation "a # b <- c" := (
Pregmap.set b c a) (
at level 1,
b at next level) :
asm.
Open Scope asm.
Undefining some registers
Fixpoint undef_regs (
l:
list preg) (
rs:
regset) :
regset :=
match l with
|
nil =>
rs
|
r ::
l' =>
undef_regs l' (
rs#
r <-
Vundef)
end.
Undefining the condition codes
Definition undef_flags (
rs:
regset) :
regset :=
fun r =>
match r with CR _ =>
Vundef | _ =>
rs r end.
Assigning a register pair
Definition set_pair (
p:
rpair preg) (
v:
val) (
rs:
regset) :
regset :=
match p with
|
One r =>
rs#
r <-
v
|
Twolong rhi rlo =>
rs#
rhi <- (
Val.hiword v) #
rlo <- (
Val.loword v)
end.
Assigning the result of a builtin
Fixpoint set_res (
res:
builtin_res preg) (
v:
val) (
rs:
regset) :
regset :=
match res with
|
BR r =>
rs#
r <-
v
|
BR_none =>
rs
|
BR_splitlong hi lo =>
set_res lo (
Val.loword v) (
set_res hi (
Val.hiword v)
rs)
end.
Section RELSEM.
Looking up instructions in a code sequence by position.
Fixpoint find_instr (
pos:
Z) (
c:
code) {
struct c} :
option instruction :=
match c with
|
nil =>
None
|
i ::
il =>
if zeq pos 0
then Some i else find_instr (
pos - 1)
il
end.
Position corresponding to a label
Definition is_label (
lbl:
label) (
instr:
instruction) :
bool :=
match instr with
|
Plabel lbl' =>
if peq lbl lbl' then true else false
| _ =>
false
end.
Lemma is_label_correct:
forall lbl instr,
if is_label lbl instr then instr =
Plabel lbl else instr <>
Plabel lbl.
Proof.
intros.
destruct instr;
simpl;
try discriminate.
case (
peq lbl l);
intro;
congruence.
Qed.
Fixpoint label_pos (
lbl:
label) (
pos:
Z) (
c:
code) {
struct c} :
option Z :=
match c with
|
nil =>
None
|
instr ::
c' =>
if is_label lbl instr then Some pos else label_pos lbl (
pos + 1)
c'
end.
Variable ge:
genv.
The semantics is purely small-step and defined as a function
from the current state (a register set + a memory state)
to either Next rs' m' where rs' and m' are the updated register
set and memory state after execution of the instruction at rs#PC,
or Stuck if the processor is stuck.
Inductive outcome:
Type :=
|
Next:
regset ->
mem ->
outcome
|
Stuck:
outcome.
Manipulations over the PC register: continuing with the next
instruction (nextinstr) or branching to a label (goto_label).
Definition nextinstr (
rs:
regset) :=
rs#
PC <- (
Val.offset_ptr rs#
PC Ptrofs.one).
Definition nextinstr_nf (
rs:
regset) :=
nextinstr (
undef_flags rs).
Definition goto_label (
f:
function) (
lbl:
label) (
rs:
regset) (
m:
mem) :=
match label_pos lbl 0 (
fn_code f)
with
|
None =>
Stuck
|
Some pos =>
match rs#
PC with
|
Vptr b ofs =>
Next (
rs#
PC <- (
Vptr b (
Ptrofs.repr pos)))
m
| _ =>
Stuck
end
end.
Evaluation of shift_op operands
Definition eval_shift_op (
so:
shift_op) (
rs:
regset) :=
match so with
|
SOimm n =>
Vint n
|
SOreg r =>
rs r
|
SOlsl r n =>
Val.shl (
rs r) (
Vint n)
|
SOlsr r n =>
Val.shru (
rs r) (
Vint n)
|
SOasr r n =>
Val.shr (
rs r) (
Vint n)
|
SOror r n =>
Val.ror (
rs r) (
Vint n)
end.
Auxiliaries for memory accesses
Definition ls_double_next_reg (
r:
preg) :=
match r with
|
IR0 =>
Some IR1 |
IR2 =>
Some IR3 |
IR4 =>
Some IR5 |
IR6 =>
Some IR7
|
IR8 =>
Some IR9 |
IR10 =>
Some IR11 |
IR12 =>
Some IR13 | _ =>
None
end.
Definition ls_pair_reg (
r1 r2:
preg) :=
match r1,
r2 with
|
IR0,
IR1 =>
Some IR0
|
IR1,
IR0 =>
Some IR0
|
IR2,
IR3 =>
Some IR2
|
IR3,
IR2 =>
Some IR2
|
IR4,
IR5 =>
Some IR4
|
IR5,
IR4 =>
Some IR4
|
IR6,
IR7 =>
Some IR6
|
IR7,
IR6 =>
Some IR6
|
IR8,
IR9 =>
Some IR8
|
IR9,
IR8 =>
Some IR8
|
IR10,
IR11 =>
Some IR10
|
IR11,
IR10 =>
Some IR10
|
IR12,
IR13 =>
Some IR12
|
IR13,
IR12 =>
Some IR12
| _, _ =>
None
end.
Definition ls_double_constraints (
rd1 rd2:
ireg) (
chk1 chk2:
memory_chunk) (
i1 i2:
int) :=
match Int.eq (
Int.add i1 (
Int.repr 4))
i2,
Int.eq (
Int.add i2 (
Int.repr 4))
i1,
ls_pair_reg rd1 rd2 with
|
true,
false,
Some rd =>
if Asm.preg_eq rd rd1 then Some (
rd1,
rd2,
chk1,
chk2,
i1)
else None
|
false,
true,
Some rd =>
if Asm.preg_eq rd rd2 then Some (
rd2,
rd1,
chk2,
chk1,
i2)
else None
| _, _, _ =>
None
end.
Definition ls_double_valid_regs (
rd1 rd2:
preg) :=
match ls_double_next_reg rd1 with
|
Some rd2' =>
proj_sumbool (
PregEq.eq rd2 rd2')
| _ =>
false
end.
Definition exec_load (
chunk:
memory_chunk) (
addr:
val) (
r:
preg)
(
rs:
regset) (
m:
mem) :=
match Mem.loadv chunk m addr with
|
None =>
Stuck
|
Some v =>
Next (
nextinstr (
rs#
r <-
v))
m
end.
Definition exec_load_double (
chk1 chk2:
memory_chunk) (
addr:
val) (
r1 r2:
preg)
(
rs:
regset) (
m:
mem) :=
if negb (
thumb tt ||
ls_double_valid_regs r1 r2)
then Stuck else
let addr' :=
Val.add addr (
Vint (
Int.repr 4))
in
match Mem.loadv chk1 m addr,
Mem.loadv chk2 m addr' with
|
Some v1,
Some v2 =>
Next (
nextinstr (
rs#
r1 <-
v1 #
r2 <-
v2))
m
| _, _ =>
Stuck
end.
Definition exec_load_pi (
chunk:
memory_chunk) (
addr:
val) (
rd ra:
preg)
(
rs:
regset) (
m:
mem) :=
match Mem.loadv chunk m rs#
ra with
|
None =>
Stuck
|
Some v =>
Next (
nextinstr_nf (
rs#
ra <-
addr #
rd <-
v))
m
end.
Definition exec_store (
chunk:
memory_chunk) (
addr:
val) (
r:
preg)
(
rs:
regset) (
m:
mem) :=
match Mem.storev chunk m addr rs#
r with
|
None =>
Stuck
|
Some m' =>
Next (
nextinstr rs)
m'
end.
Definition exec_store_double (
chk1 chk2:
memory_chunk) (
addr:
val) (
r1 r2:
preg)
(
rs:
regset) (
m:
mem) :=
if negb (
thumb tt ||
ls_double_valid_regs r1 r2)
then Stuck else
let addr' :=
Val.add addr (
Vint (
Int.repr 4))
in
match Mem.storev chk1 m addr rs#
r1 with
|
Some m' =>
match Mem.storev chk2 m' addr' rs#
r2 with
|
Some m'' =>
Next (
nextinstr rs)
m''
|
None =>
Stuck
end
| _ =>
Stuck
end.
Definition exec_store_pi (
chunk:
memory_chunk) (
addr:
val) (
rf ra:
preg)
(
rs:
regset) (
m:
mem) :=
match Mem.storev chunk m rs#
ra rs#
rf with
|
None =>
Stuck
|
Some m' =>
Next (
nextinstr_nf (
rs#
ra <-
addr))
m'
end.
Definition exec_load_pi_double (
chk1 chk2:
memory_chunk) (
addr_new:
val)
(
r1 r2 ra:
preg) (
rs:
regset) (
m:
mem) :=
if negb (
thumb tt ||
ls_double_valid_regs r1 r2)
then Stuck else
let addr :=
rs#
ra in
let addr' :=
Val.add addr (
Vint (
Int.repr 4))
in
match Mem.loadv chk1 m addr,
Mem.loadv chk2 m addr' with
|
Some v1,
Some v2 =>
Next (
nextinstr_nf (
rs#
ra <-
addr_new #
r1 <-
v1 #
r2 <-
v2))
m
| _, _ =>
Stuck
end.
Definition exec_store_pi_double (
chk1 chk2:
memory_chunk) (
addr_new:
val)
(
r1 r2 ra:
preg) (
rs:
regset) (
m:
mem) :=
if negb (
thumb tt ||
ls_double_valid_regs r1 r2)
then Stuck else
let addr :=
rs#
ra in
let addr' :=
Val.add addr (
Vint (
Int.repr 4))
in
match Mem.storev chk1 m addr rs#
r1 with
|
Some m' =>
match Mem.storev chk2 m' addr' rs#
r2 with
|
Some m'' =>
Next (
nextinstr_nf (
rs#
ra <-
addr_new))
m''
|
None =>
Stuck
end
| _ =>
Stuck
end.
Definition exec_load_pd (
chunk:
memory_chunk) (
addr:
val) (
rd ra:
preg)
(
rs:
regset) (
m:
mem) :=
match Mem.loadv chunk m addr with
|
None =>
Stuck
|
Some v =>
Next (
nextinstr_nf (
rs#
ra <-
addr #
rd <-
v))
m
end.
Definition exec_store_pd (
chunk:
memory_chunk) (
addr:
val) (
rf ra:
preg)
(
rs:
regset) (
m:
mem) :=
match Mem.storev chunk m addr rs#
rf with
|
None =>
Stuck
|
Some m' =>
Next (
nextinstr_nf (
rs#
ra <-
addr))
m'
end.
Multi-register stores/loads (ARM stm/ldm and VFP vstm/vldm).
Each instruction takes a base register and a list of (reg, chunk) pairs.
Accesses happen sequentially starting at rs#ra, and the address
advances by size_chunk chk per element. Both ARM stm/ldm and VFP
vstm/vldm encodings have no offset field, so the IR base address is
simply rs#ra; non-zero start offsets must be materialized by a
preceding Padd into a scratch register chosen by the peephole.
The chunk whitelist matches what the encodings can express:
- stm/ldm carry 32-bit values, so Mint32 and Many32 are accepted
(this lets the peephole fuse Pstr with Pstr_a);
- vstm/vldm-d carry 64-bit values, so Mfloat64 and Many64 are
accepted (fusing Pfstd with Pfstd_a).
Other chunks are rejected with Stuck.
Definition stm_chunk_ok (
chk:
memory_chunk) :
bool :=
match chk with Mint32 |
Many32 =>
true | _ =>
false end.
Definition vstm_chunk_ok (
chk:
memory_chunk) :
bool :=
match chk with Mfloat64 |
Many64 =>
true | _ =>
false end.
Definition ireg_index (
r:
ireg) :
Z :=
match r with
|
IR0 => 0 |
IR1 => 1 |
IR2 => 2 |
IR3 => 3
|
IR4 => 4 |
IR5 => 5 |
IR6 => 6 |
IR7 => 7
|
IR8 => 8 |
IR9 => 9 |
IR10 => 10 |
IR11 => 11
|
IR12 => 12 |
IR13 => 13 |
IR14 => 14
end.
Definition freg_index (
r:
freg) :
Z :=
match r with
|
FR0 => 0 |
FR1 => 1 |
FR2 => 2 |
FR3 => 3
|
FR4 => 4 |
FR5 => 5 |
FR6 => 6 |
FR7 => 7
|
FR8 => 8 |
FR9 => 9 |
FR10 => 10 |
FR11 => 11
|
FR12 => 12 |
FR13 => 13 |
FR14 => 14 |
FR15 => 15
end.
Well-formedness predicates: registers in strictly-increasing order,
base register not among destinations (loads), chunks in whitelist.
Fixpoint stm_iregs_sorted (
prev:
Z) (
l:
list (
ireg *
memory_chunk)) :
bool :=
match l with
|
nil =>
true
| (
r, _) ::
tl =>
Z.ltb prev (
ireg_index r) &&
stm_iregs_sorted (
ireg_index r)
tl
end.
Fixpoint stm_iregs_chunks_ok (
l:
list (
ireg *
memory_chunk)) :
bool :=
match l with
|
nil =>
true
| (_,
chk) ::
tl =>
stm_chunk_ok chk &&
stm_iregs_chunks_ok tl
end.
Fixpoint stm_iregs_no_base (
ra:
ireg) (
l:
list (
ireg *
memory_chunk)) :
bool :=
match l with
|
nil =>
true
| (
r, _) ::
tl =>
negb (
proj_sumbool (
ireg_eq ra r)) &&
stm_iregs_no_base ra tl
end.
Definition stm_iregs_wf (
ra:
ireg) (
l:
list (
ireg *
memory_chunk)) :
bool :=
stm_iregs_sorted (-1)
l &&
stm_iregs_chunks_ok l.
Definition ldm_iregs_wf (
ra:
ireg) (
l:
list (
ireg *
memory_chunk)) :
bool :=
stm_iregs_wf ra l &&
stm_iregs_no_base ra l.
vstmia/vldmia encode a starting register and a count (not a bitmask),
so the d-register list must be strictly consecutive. The initial sentinel
prev = -1 accepts any first register.
Fixpoint vstm_fregs_sorted (
prev:
Z) (
l:
list (
freg *
memory_chunk)) :
bool :=
match l with
|
nil =>
true
| (
r, _) ::
tl =>
((
Z.ltb prev 0) ||
Z.eqb (
prev + 1) (
freg_index r))
&&
vstm_fregs_sorted (
freg_index r)
tl
end.
Fixpoint vstm_fregs_chunks_ok (
l:
list (
freg *
memory_chunk)) :
bool :=
match l with
|
nil =>
true
| (_,
chk) ::
tl =>
vstm_chunk_ok chk &&
vstm_fregs_chunks_ok tl
end.
Definition vstm_fregs_wf (
l:
list (
freg *
memory_chunk)) :
bool :=
vstm_fregs_sorted (-1)
l &&
vstm_fregs_chunks_ok l.
Definition vldm_fregs_wf :=
vstm_fregs_wf.
Sequential walk over the (reg, chunk) list, advancing the address
by size_chunk chk per element.
Fixpoint exec_store_multi_i (
base:
val) (
ofs:
Z) (
l:
list (
ireg *
memory_chunk))
(
rs:
regset) (
m:
mem) :
option mem :=
match l with
|
nil =>
Some m
| (
r,
chk) ::
tl =>
match Mem.storev chk m (
Val.add base (
Vint (
Int.repr ofs)))
rs#
r with
|
Some m' =>
exec_store_multi_i base (
ofs +
size_chunk chk)
tl rs m'
|
None =>
None
end
end.
Fixpoint exec_load_multi_i (
base:
val) (
ofs:
Z) (
l:
list (
ireg *
memory_chunk))
(
rs:
regset) (
m:
mem) :
option regset :=
match l with
|
nil =>
Some rs
| (
r,
chk) ::
tl =>
match Mem.loadv chk m (
Val.add base (
Vint (
Int.repr ofs)))
with
|
Some v =>
exec_load_multi_i base (
ofs +
size_chunk chk)
tl (
rs#
r <-
v)
m
|
None =>
None
end
end.
Fixpoint exec_store_multi_f (
base:
val) (
ofs:
Z) (
l:
list (
freg *
memory_chunk))
(
rs:
regset) (
m:
mem) :
option mem :=
match l with
|
nil =>
Some m
| (
r,
chk) ::
tl =>
match Mem.storev chk m (
Val.add base (
Vint (
Int.repr ofs)))
rs#
r with
|
Some m' =>
exec_store_multi_f base (
ofs +
size_chunk chk)
tl rs m'
|
None =>
None
end
end.
Fixpoint exec_load_multi_f (
base:
val) (
ofs:
Z) (
l:
list (
freg *
memory_chunk))
(
rs:
regset) (
m:
mem) :
option regset :=
match l with
|
nil =>
Some rs
| (
r,
chk) ::
tl =>
match Mem.loadv chk m (
Val.add base (
Vint (
Int.repr ofs)))
with
|
Some v =>
exec_load_multi_f base (
ofs +
size_chunk chk)
tl (
rs#
r <-
v)
m
|
None =>
None
end
end.
Memcpy
Definition mcpy_rs_use_addr (
a:
mcpy_addr) :=
match a with
|
Ofs n |
PreIncr n =>
Some n
| _ =>
None
end.
Definition mcpy_rs_ret_addr (
a:
mcpy_addr) :=
match a with
|
PostIncr n |
PreIncr n =>
Some n
| _ =>
None
end.
Definition mcpy_rs (
tr:
list dreg) (
ras rad:
ireg) (
mas mad:
mcpy_addr) (
rs:
regset) (
chg_fn:
mcpy_addr ->
option int) :=
match chg_fn mas,
chg_fn mad with
|
Some ns,
Some nd =>
undef_flags ((
undef_regs (
map DR tr) (
rs#
ras <- (
Val.add rs#
ras (
Vint ns))))
#
rad <- (
Val.add rs#
rad (
Vint nd)))
|
Some ns,
None =>
undef_flags (
undef_regs (
map DR tr) (
rs#
ras <- (
Val.add rs#
ras (
Vint ns))))
|
None,
Some nd =>
undef_flags ((
undef_regs (
map DR tr)
rs) #
rad <- (
Val.add rs#
rad (
Vint nd)))
|
None,
None =>
undef_regs (
map DR tr)
rs
end.
Definition mcpy_rs_use_src (
tr:
list dreg) (
ras:
ireg) (
mas:
mcpy_addr) (
rs:
regset) :=
match mcpy_rs_use_addr mas with
|
Some ns =>
rs#
ras <- (
Val.add rs#
ras (
Vint ns))
|
None =>
rs
end.
Definition exec_memcpy (
tr:
list dreg) (
ras rad:
ireg) (
mas mad:
mcpy_addr)
(
sz:
Z) (
rs:
regset) (
m:
mem) :=
let rss :=
mcpy_rs_use_src tr ras mas rs in
let rsd :=
mcpy_rs tr ras rad mas mad rs mcpy_rs_use_addr in
let rsr :=
mcpy_rs tr ras rad mas mad rs mcpy_rs_ret_addr in
match rss#
ras,
rsd#
rad with
|
Vptr bsrc osrc,
Vptr bdst odst =>
match Mem.loadbytes m bsrc (
Ptrofs.unsigned osrc)
sz with
|
Some bytes =>
match Mem.storebytes m bdst (
Ptrofs.unsigned odst)
bytes with
|
Some m' =>
Next (
nextinstr rsr)
m'
|
None =>
Stuck
end
|
None =>
Stuck
end
| _, _ =>
Stuck
end.
Definition mcpy_valid_reg (
ras rad:
ireg) (
mas mad:
mcpy_addr) :=
match mas,
mad with
|
Ofs _,
Ofs _ =>
true
| _, _ =>
negb (
PregEq.eq ras rad)
end.
Comparisons.
Definition compare_int (
rs:
regset) (
v1 v2:
val) (
m:
mem) :=
rs#
CN <- (
Val.negative (
Val.sub v1 v2))
#
CZ <- (
Val.cmpu (
Mem.valid_pointer m)
Ceq v1 v2)
#
CC <- (
Val.cmpu (
Mem.valid_pointer m)
Cge v1 v2)
#
CV <- (
Val.sub_overflow v1 v2).
Flag-update for ADDS v1 + v2. Defined as compare_int v1 (-v2) so
that the flags are the SUB-style flags of v1 - (-v2) = v1 + v2. This
matches the existing symbolic translation of Pcmn (which negates the
second operand and reuses v_compare_int).
Definition compare_int_add (
rs:
regset) (
v1 v2:
val) (
m:
mem) :=
compare_int rs v1 (
Val.neg v2)
m.
Subtract-with-carry, set flags. ARMv7-A ARM A8.8.157 SBCS.
Inputs: rn = the Rn register's value.
op = the (already-evaluated) shifter operand.
cin = the previous APSR.C value (Vint 0 or Vint 1).
Effect: computes result = rn - op - (1 - cin) = rn - op - bin
where bin = 1 - cin is the borrow-in, and updates the
four flag pseudo-registers CN, CZ, CC, CV to reflect
the ARM SBCS semantics.
Definition compare_int_sbc (
rs:
regset) (
rn op cin:
val) (
m:
mem) :
regset :=
let bin :=
Val.sub (
Vint Int.one)
cin in
let result :=
Val.sub (
Val.sub rn op)
bin in
let cv :=
match rn,
op,
bin with
|
Vint x,
Vint y,
Vint b =>
Vint (
Int.sub_overflow x y b)
| _, _, _ =>
Vundef
end in
rs#
CN <- (
Val.negative result)
#
CZ <- (
Val.cmpu (
Mem.valid_pointer m)
Ceq result (
Vint Int.zero))
#
CC <- (
Val.add_carry rn (
Val.notint op)
cin)
#
CV <-
cv.
tst semantics: AND, set N from sign bit and Z from "is zero".
C is the shifter carry-out (left undefined here; not consumed by any
cbranch we generate) and V is preserved (modelled as undef).
Definition compare_int_test (
rs:
regset) (
v1 v2:
val) :=
let v :=
Val.and v1 v2 in
rs#
CN <- (
Val.negative v)
#
CZ <- (
Val.cmp Ceq v (
Vint Int.zero))
#
CC <-
Vundef
#
CV <-
Vundef.
Semantics of
fcmp instructions:
== N=0 Z=1 C=1 V=0
< N=1 Z=0 C=0 V=0
> N=0 Z=0 C=1 V=0
unord N=0 Z=0 C=1 V=1
(
rs:
regset) (
v1 v2:
val) :=
match v1,
v2 with
|
Vfloat f1,
Vfloat f2 =>
rs#
CN <- (
Val.of_bool (
Float.cmp Clt f1 f2))
#
CZ <- (
Val.of_bool (
Float.cmp Ceq f1 f2))
#
CC <- (
Val.of_bool (
negb (
Float.cmp Clt f1 f2)))
#
CV <- (
Val.of_bool (
negb (
Float.cmp Ceq f1 f2 ||
Float.cmp Clt f1 f2 ||
Float.cmp Cgt f1 f2)))
| _, _ =>
rs#
CN <-
Vundef
#
CZ <-
Vundef
#
CC <-
Vundef
#
CV <-
Vundef
end.
Definition compare_float32 (
rs:
regset) (
v1 v2:
val) :=
match v1,
v2 with
|
Vsingle f1,
Vsingle f2 =>
rs#
CN <- (
Val.of_bool (
Float32.cmp Clt f1 f2))
#
CZ <- (
Val.of_bool (
Float32.cmp Ceq f1 f2))
#
CC <- (
Val.of_bool (
negb (
Float32.cmp Clt f1 f2)))
#
CV <- (
Val.of_bool (
negb (
Float32.cmp Ceq f1 f2 ||
Float32.cmp Clt f1 f2 ||
Float32.cmp Cgt f1 f2)))
| _, _ =>
rs#
CN <-
Vundef
#
CZ <-
Vundef
#
CC <-
Vundef
#
CV <-
Vundef
end.
Testing a condition
Definition eval_testcond (
c:
testcond) (
rs:
regset) :
option bool :=
match c with
|
TCeq =>
(* equal *)
match rs CZ with
|
Vint n =>
Some (
Int.eq n Int.one)
| _ =>
None
end
|
TCne =>
(* not equal *)
match rs CZ with
|
Vint n =>
Some (
Int.eq n Int.zero)
| _ =>
None
end
|
TClo =>
(* unsigned less than *)
match rs CC with
|
Vint n =>
Some (
Int.eq n Int.zero)
| _ =>
None
end
|
TCls =>
(* unsigned less or equal *)
match rs CC,
rs CZ with
|
Vint c,
Vint z =>
Some (
Int.eq c Int.zero ||
Int.eq z Int.one)
| _, _ =>
None
end
|
TChs =>
(* unsigned greater or equal *)
match rs CC with
|
Vint n =>
Some (
Int.eq n Int.one)
| _ =>
None
end
|
TChi =>
(* unsigned greater *)
match rs CC,
rs CZ with
|
Vint c,
Vint z =>
Some (
Int.eq c Int.one &&
Int.eq z Int.zero)
| _, _ =>
None
end
|
TClt =>
(* signed less than *)
match rs CV,
rs CN with
|
Vint o,
Vint s =>
Some (
Int.eq (
Int.xor o s)
Int.one)
| _, _ =>
None
end
|
TCle =>
(* signed less or equal *)
match rs CV,
rs CN,
rs CZ with
|
Vint o,
Vint s,
Vint z =>
Some (
Int.eq (
Int.xor o s)
Int.one ||
Int.eq z Int.one)
| _, _, _ =>
None
end
|
TCge =>
(* signed greater or equal *)
match rs CV,
rs CN with
|
Vint o,
Vint s =>
Some (
Int.eq (
Int.xor o s)
Int.zero)
| _, _ =>
None
end
|
TCgt =>
(* signed greater *)
match rs CV,
rs CN,
rs CZ with
|
Vint o,
Vint s,
Vint z =>
Some (
Int.eq (
Int.xor o s)
Int.zero &&
Int.eq z Int.zero)
| _, _, _ =>
None
end
|
TCpl =>
(* positive *)
match rs CN with
|
Vint n =>
Some (
Int.eq n Int.zero)
| _ =>
None
end
|
TCmi =>
(* negative *)
match rs CN with
|
Vint n =>
Some (
Int.eq n Int.one)
| _ =>
None
end
end.
Execution of a single instruction i in initial state
rs and m. Return updated state. For instructions
that correspond to actual ARM instructions, the cases are
straightforward transliterations of the informal descriptions
given in the ARM reference manuals. For pseudo-instructions,
refer to the informal descriptions given above.
Note that we set to Vundef the registers used as temporaries by
the expansions of the pseudo-instructions, so that the ARM code we
generate cannot use those registers to hold values that must
survive the execution of the pseudo-instruction.
Likewise, for several instructions we set the condition flags
to Vundef, so that we can expand them later to the S form
or to the non-S form, whichever is more compact in Thumb2.
Definition eval_testzero (
v:
val):
option bool :=
Val.mxcmpu_bool Ceq v (
Vint Int.zero).
Definition exec_instr (
f:
function) (
i:
instruction) (
rs:
regset) (
m:
mem) :
outcome :=
match i with
|
Padd r1 r2 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.add rs#
r2 (
eval_shift_op so rs))))
m
|
Pand r1 r2 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.and rs#
r2 (
eval_shift_op so rs))))
m
|
Pasr r1 r2 r3 =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.shr rs#
r2 rs#
r3)))
m
|
Pb lbl =>
goto_label f lbl rs m
|
Pbc cond lbl =>
match eval_testcond cond rs with
|
Some true =>
goto_label f lbl rs m
|
Some false =>
Next (
nextinstr rs)
m
|
None =>
Stuck
end
|
Pcbz r lbl =>
match eval_testzero rs#
r with
|
Some true =>
goto_label f lbl rs m
|
Some false =>
Next (
nextinstr rs)
m
|
None =>
Stuck
end
|
Pcbnz r lbl =>
match eval_testzero rs#
r with
|
Some true =>
Next (
nextinstr rs)
m
|
Some false =>
goto_label f lbl rs m
|
None =>
Stuck
end
|
Pbsymb id sg =>
Next (
rs#
PC <- (
Genv.symbol_address ge id Ptrofs.zero))
m
|
Pbreg r sg =>
Next (
rs#
PC <- (
rs#
r))
m
|
Pblsymb id sg =>
Next (
rs#
IR14 <- (
Val.offset_ptr rs#
PC Ptrofs.one) #
PC <- (
Genv.symbol_address ge id Ptrofs.zero))
m
|
Pblreg r sg =>
Next (
rs#
IR14 <- (
Val.offset_ptr rs#
PC Ptrofs.one) #
PC <- (
rs#
r))
m
|
Pbic r1 r2 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.and rs#
r2 (
Val.notint (
eval_shift_op so rs)))))
m
|
Pcmp r1 so =>
Next (
nextinstr (
compare_int rs rs#
r1 (
eval_shift_op so rs)
m))
m
|
Pcmn r1 so =>
Next (
nextinstr (
compare_int rs rs#
r1 (
Val.neg (
eval_shift_op so rs))
m))
m
|
Ptst r1 so =>
Next (
nextinstr (
compare_int_test rs rs#
r1 (
eval_shift_op so rs)))
m
|
Peor r1 r2 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.xor rs#
r2 (
eval_shift_op so rs))))
m
|
Pldr r1 r2 sa =>
exec_load Mint32 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pldr_a r1 r2 sa =>
exec_load Many32 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pldr_u r1 r2 sa =>
exec_load Mint32al1 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pldrd r1 r2 ra chk1 chk2 i =>
exec_load_double chk1 chk2 (
Val.add rs#
ra (
Vint i))
r1 r2 rs m
|
Pldrb r1 r2 sa =>
exec_load Mint8unsigned (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pldrh r1 r2 sa =>
exec_load Mint16unsigned (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pldrsb r1 r2 sa =>
exec_load Mint8signed (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pldrsh r1 r2 sa =>
exec_load Mint16signed (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pldr_pi r1 r2 sa =>
exec_load_pi Mint32 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldr_api r1 r2 sa =>
exec_load_pi Many32 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrb_pi r1 r2 sa =>
exec_load_pi Mint8unsigned (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrh_pi r1 r2 sa =>
exec_load_pi Mint16unsigned (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrsb_pi r1 r2 sa =>
exec_load_pi Mint8signed (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrsh_pi r1 r2 sa =>
exec_load_pi Mint16signed (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrd_pi r1 r2 ra chk1 chk2 i =>
exec_load_pi_double chk1 chk2 (
Val.add rs#
ra (
Vint i))
r1 r2 ra rs m
|
Plsl r1 r2 r3 =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.shl rs#
r2 rs#
r3)))
m
|
Plsr r1 r2 r3 =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.shru rs#
r2 rs#
r3)))
m
|
Pror r1 r2 r3 =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.ror rs#
r2 rs#
r3)))
m
|
Pmla r1 r2 r3 r4 =>
Next (
nextinstr (
rs#
r1 <- (
Val.add (
Val.mul rs#
r2 rs#
r3)
rs#
r4)))
m
|
Pmls r1 r2 r3 r4 =>
Next (
nextinstr (
rs#
r1 <- (
Val.sub rs#
r4 (
Val.mul rs#
r2 rs#
r3))))
m
|
Pmov r1 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
eval_shift_op so rs)))
m
|
Pmovw r n =>
Next (
nextinstr (
rs#
r <- (
Vint n)))
m
|
Pmovt r n =>
Next (
nextinstr (
rs#
r <- (
Val.or (
Val.and rs#
r (
Vint (
Int.repr 65535)))
(
Vint (
Int.shl n (
Int.repr 16))))))
m
|
Pmul r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.mul rs#
r2 rs#
r3)))
m
|
Pmvn r1 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.notint (
eval_shift_op so rs))))
m
|
Porr r1 r2 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.or rs#
r2 (
eval_shift_op so rs))))
m
|
Prsb r1 r2 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.sub (
eval_shift_op so rs)
rs#
r2)))
m
|
Pstr r1 r2 sa =>
exec_store Mint32 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pstr_a r1 r2 sa =>
exec_store Many32 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pstr_u r1 r2 sa =>
exec_store Mint32al1 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pstrd r1 r2 ra chk1 chk2 i =>
exec_store_double chk1 chk2 (
Val.add rs#
ra (
Vint i))
r1 r2 rs m
|
Pstrb r1 r2 sa =>
exec_store Mint8unsigned (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pstrh r1 r2 sa =>
exec_store Mint16unsigned (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 rs m
|
Pstm ra l =>
if stm_iregs_wf ra l then
match exec_store_multi_i rs#
ra 0
l rs m with
|
Some m' =>
Next (
nextinstr rs)
m'
|
None =>
Stuck
end
else Stuck
|
Pldm ra l =>
if ldm_iregs_wf ra l then
match exec_load_multi_i rs#
ra 0
l rs m with
|
Some rs' =>
Next (
nextinstr rs')
m
|
None =>
Stuck
end
else Stuck
|
Pvstm ra l =>
if vstm_fregs_wf l then
match exec_store_multi_f rs#
ra 0
l rs m with
|
Some m' =>
Next (
nextinstr rs)
m'
|
None =>
Stuck
end
else Stuck
|
Pvldm ra l =>
if vldm_fregs_wf l then
match exec_load_multi_f rs#
ra 0
l rs m with
|
Some rs' =>
Next (
nextinstr rs')
m
|
None =>
Stuck
end
else Stuck
|
Pstr_pi r1 r2 sa =>
exec_store_pi Mint32 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pstr_api r1 r2 sa =>
exec_store_pi Many32 (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pstrb_pi r1 r2 sa =>
exec_store_pi Mint8unsigned (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pstrh_pi r1 r2 sa =>
exec_store_pi Mint16unsigned (
Val.add rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pstrd_pi r1 r2 ra chk1 chk2 i =>
exec_store_pi_double chk1 chk2 (
Val.add rs#
ra (
Vint i))
r1 r2 ra rs m
|
Pldr_pd r1 r2 sa =>
exec_load_pd Mint32 (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldr_apd r1 r2 sa =>
exec_load_pd Many32 (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrb_pd r1 r2 sa =>
exec_load_pd Mint8unsigned (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrh_pd r1 r2 sa =>
exec_load_pd Mint16unsigned (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrsb_pd r1 r2 sa =>
exec_load_pd Mint8signed (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pldrsh_pd r1 r2 sa =>
exec_load_pd Mint16signed (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pstr_pd r1 r2 sa =>
exec_store_pd Mint32 (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pstr_apd r1 r2 sa =>
exec_store_pd Many32 (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pstrb_pd r1 r2 sa =>
exec_store_pd Mint8unsigned (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Pstrh_pd r1 r2 sa =>
exec_store_pd Mint16unsigned (
Val.sub rs#
r2 (
eval_shift_op sa rs))
r1 r2 rs m
|
Psdiv rd r1 r2 =>
match Val.divs rs#
r1 rs#
r2 with
|
Some v =>
if Archi.hardware_idiv tt then
Next (
nextinstr (
rs#
rd <-
v))
m
else
let rs :=
undef_regs
(
DR IR0 ::
DR IR1 ::
DR IR2 ::
DR IR3 ::
DR IR12
::
DR FR0 ::
DR FR1 ::
DR FR2 ::
DR FR3
::
DR FR4 ::
DR FR5 ::
DR FR6 ::
DR FR7 ::
nil)
rs in
Next (
nextinstr (
rs#
rd <-
v))
m
|
None =>
Stuck
end
|
Pubfx r1 r2 lsb sz =>
Next (
nextinstr (
rs#
r1 <- (
Val.zero_ext (
Int.unsigned sz) (
Val.shru rs#
r2 (
Vint lsb)))))
m
|
Psbfx r1 r2 lsb sz =>
Next (
nextinstr (
rs#
r1 <- (
Val.sign_ext (
Int.unsigned sz) (
Val.shru rs#
r2 (
Vint lsb)))))
m
|
Puxtb r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.zero_ext 8
rs#
r2)))
m
|
Psxtb r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.sign_ext 8
rs#
r2)))
m
|
Puxth r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.zero_ext 16
rs#
r2)))
m
|
Psxth r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.sign_ext 16
rs#
r2)))
m
|
Pbfc r1 lsb sz =>
Next (
nextinstr (
rs#
r1 <- (
ExtValues.clearf lsb sz (
rs#
r1))))
m
|
Pbfi r1 r2 lsb sz =>
Next (
nextinstr (
rs#
r1 <- (
ExtValues.insf lsb sz (
rs#
r1) (
rs#
r2))))
m
|
Psmull rdl rdh r1 r2 =>
Next (
nextinstr (
rs#
rdl <- (
Val.mul rs#
r1 rs#
r2)
#
rdh <- (
Val.mulhs rs#
r1 rs#
r2)))
m
|
Psub r1 r2 so =>
Next (
nextinstr_nf (
rs#
r1 <- (
Val.sub rs#
r2 (
eval_shift_op so rs))))
m
|
Psubs r1 r2 so =>
let v2 :=
eval_shift_op so rs in
Next (
nextinstr ((
compare_int rs rs#
r2 v2 m) #
r1 <- (
Val.sub rs#
r2 v2)))
m
|
Psbcs r1 r2 so =>
let v2 :=
eval_shift_op so rs in
let cin :=
rs#
CC in
let bin :=
Val.sub (
Vint Int.one)
cin in
let result :=
Val.sub (
Val.sub rs#
r2 v2)
bin in
Next (
nextinstr ((
compare_int_sbc rs rs#
r2 v2 cin m) #
r1 <-
result))
m
|
Pudiv rd r1 r2 =>
match Val.divu rs#
r1 rs#
r2 with
|
Some v =>
if Archi.hardware_idiv tt then
Next (
nextinstr (
rs#
rd <-
v))
m
else
let rs :=
undef_regs
(
DR IR0 ::
DR IR1 ::
DR IR2 ::
DR IR3 ::
DR IR12
::
DR FR0 ::
DR FR1 ::
DR FR2 ::
DR FR3
::
DR FR4 ::
DR FR5 ::
DR FR6 ::
DR FR7 ::
nil)
rs in
Next (
nextinstr (
rs#
rd <-
v))
m
|
None =>
Stuck
end
|
Pumull rdl rdh r1 r2 =>
Next (
nextinstr (
rs#
rdl <- (
Val.mul rs#
r1 rs#
r2)
#
rdh <- (
Val.mulhu rs#
r1 rs#
r2)))
m
|
Pfcpyd r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
rs#
r2)))
m
|
Pfabsd r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.absf rs#
r2)))
m
|
Pfnegd r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.negf rs#
r2)))
m
|
Pfaddd r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.addf rs#
r2 rs#
r3)))
m
|
Pfdivd r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.divf rs#
r2 rs#
r3)))
m
|
Pfmuld r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.mulf rs#
r2 rs#
r3)))
m
|
Pfmlad r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.addf rs#
r1 (
Val.mulf rs#
r2 rs#
r3))))
m
|
Pfmlsd r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.subf rs#
r1 (
Val.mulf rs#
r2 rs#
r3))))
m
|
Pfsubd r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.subf rs#
r2 rs#
r3)))
m
|
Pflid r1 f =>
Next (
nextinstr (
rs#
IR14 <-
Vundef #
r1 <- (
Vfloat f)))
m
|
Pfcmpd r1 r2 =>
Next (
nextinstr (
compare_float rs rs#
r1 rs#
r2))
m
|
Pfcmpzd r1 =>
Next (
nextinstr (
compare_float rs rs#
r1 (
Vfloat Float.zero)))
m
|
Pfsitod r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.maketotal (
Val.floatofint rs#
r2))))
m
|
Pfuitod r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.maketotal (
Val.floatofintu rs#
r2))))
m
|
Pftosizd r1 r2 =>
Next (
nextinstr (
rs #
FR6 <-
Vundef #
r1 <- (
Val.maketotal (
Val.intoffloat rs#
r2))))
m
|
Pftouizd r1 r2 =>
Next (
nextinstr (
rs #
FR6 <-
Vundef #
r1 <- (
Val.maketotal (
Val.intuoffloat rs#
r2))))
m
|
Pfabss r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.absfs rs#
r2)))
m
|
Pfnegs r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.negfs rs#
r2)))
m
|
Pfadds r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.addfs rs#
r2 rs#
r3)))
m
|
Pfdivs r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.divfs rs#
r2 rs#
r3)))
m
|
Pfmuls r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.mulfs rs#
r2 rs#
r3)))
m
|
Pfmlas r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.addfs rs#
r1 (
Val.mulfs rs#
r2 rs#
r3))))
m
|
Pfmlss r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.subfs rs#
r1 (
Val.mulfs rs#
r2 rs#
r3))))
m
|
Pfsubs r1 r2 r3 =>
Next (
nextinstr (
rs#
r1 <- (
Val.subfs rs#
r2 rs#
r3)))
m
|
Pflis r1 f =>
Next (
nextinstr (
rs#
r1 <- (
Vsingle f)))
m
|
Pfcmps r1 r2 =>
Next (
nextinstr (
compare_float32 rs rs#
r1 rs#
r2))
m
|
Pfcmpzs r1 =>
Next (
nextinstr (
compare_float32 rs rs#
r1 (
Vsingle Float32.zero)))
m
|
Pfsitos r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.maketotal (
Val.singleofint rs#
r2))))
m
|
Pfuitos r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.maketotal (
Val.singleofintu rs#
r2))))
m
|
Pftosizs r1 r2 =>
Next (
nextinstr (
rs #
FR6 <-
Vundef #
r1 <- (
Val.maketotal (
Val.intofsingle rs#
r2))))
m
|
Pftouizs r1 r2 =>
Next (
nextinstr (
rs #
FR6 <-
Vundef #
r1 <- (
Val.maketotal (
Val.intuofsingle rs#
r2))))
m
|
Pfcvtsd r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.singleoffloat rs#
r2)))
m
|
Pfcvtds r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.floatofsingle rs#
r2)))
m
|
Pfldd r1 r2 n =>
exec_load Mfloat64 (
Val.add rs#
r2 (
Vint n))
r1 rs m
|
Pfldd_a r1 r2 n =>
exec_load Many64 (
Val.add rs#
r2 (
Vint n))
r1 rs m
|
Pflds r1 r2 n =>
exec_load Mfloat32 (
Val.add rs#
r2 (
Vint n))
r1 rs m
|
Pfstd r1 r2 n =>
exec_store Mfloat64 (
Val.add rs#
r2 (
Vint n))
r1 rs m
|
Pfstd_a r1 r2 n =>
exec_store Many64 (
Val.add rs#
r2 (
Vint n))
r1 rs m
|
Pfsts r1 r2 n =>
exec_store Mfloat32 (
Val.add rs#
r2 (
Vint n))
r1 rs m
|
Pbits_of_single r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.bits_of_single rs#
r2)))
m
|
Psingle_of_bits r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.single_of_bits rs#
r2)))
m
|
Phibits_of_float r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.hiword (
Val.bits_of_float rs#
r2))))
m
|
Pfcpy_fii rd rlo rhi =>
Next (
nextinstr (
rs#
rd <- (
Val.floatofwords rs#
rhi rs#
rlo)))
m
|
Pfsqrtd r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.sqrtf rs#
r2)))
m
|
Pfsqrts r1 r2 =>
Next (
nextinstr (
rs#
r1 <- (
Val.sqrtfs rs#
r2)))
m
|
Pallocframe sz pos =>
let (
m1,
stk) :=
Mem.alloc m 0
sz 8
in
let sp := (
Vptr stk Ptrofs.zero)
in
match Mem.storev Mint32 m1 (
Val.offset_ptr sp pos)
rs#
IR13 with
|
None =>
Stuck
|
Some m2 =>
Next (
nextinstr (
rs #
IR12 <- (
rs#
IR13) #
IR13 <-
sp))
m2
end
|
Pfreeframe sz pos =>
match Mem.loadv Mint32 m (
Val.offset_ptr rs#
IR13 pos)
with
|
None =>
Stuck
|
Some v =>
match rs#
IR13 with
|
Vptr stk ofs =>
match Mem.free m stk 0
sz with
|
None =>
Stuck
|
Some m' =>
Next (
nextinstr (
rs#
IR13 <-
v))
m'
end
| _ =>
Stuck
end
end
|
Plabel lbl =>
Next (
nextinstr rs)
m
|
Ploadsymbol r1 lbl ofs =>
Next (
nextinstr (
rs#
r1 <- (
Genv.symbol_address ge lbl ofs)))
m
|
Pmovite cond r1 ifso ifnot =>
let v :=
match eval_testcond cond rs with
|
Some true =>
eval_shift_op ifso rs
|
Some false =>
eval_shift_op ifnot rs
|
None =>
Vundef
end in
Next (
nextinstr (
rs#
r1 <-
v))
m
|
Pfmovite cond r1 ifso ifnot =>
let v :=
match eval_testcond cond rs with
|
Some true =>
rs#
ifso
|
Some false =>
rs#
ifnot
|
None =>
Vundef
end in
Next (
nextinstr (
rs#
r1 <-
v))
m
|
Pbtbl r tbl =>
match rs#
r with
|
Vint n =>
match list_nth_z tbl (
Int.unsigned n)
with
|
None =>
Stuck
|
Some lbl =>
goto_label f lbl (
rs#
IR14 <-
Vundef)
m
end
| _ =>
Stuck
end
|
Pcfi_rel_offset ofs =>
Next (
nextinstr rs)
m
|
Pnop _ =>
Next (
nextinstr rs)
m
|
Pgetcanary rd =>
Next (
nextinstr (
rs #
rd <- (
canary_val tt)))
m
|
Pmemcpy8 r1 r2 ma1 ma2 tr =>
if PregEq.eq r2 tr ||
negb (
mcpy_valid_reg r1 r2 ma1 ma2)
then Stuck
else exec_memcpy (
IR tr ::
nil)
r1 r2 ma1 ma2 1
rs m
|
Pmemcpy16 r1 r2 ma1 ma2 tr =>
if PregEq.eq r2 tr ||
negb (
mcpy_valid_reg r1 r2 ma1 ma2)
then Stuck
else exec_memcpy (
IR tr ::
nil)
r1 r2 ma1 ma2 2
rs m
|
Pmemcpy32 r1 r2 ma1 ma2 tr =>
if PregEq.eq r2 tr ||
negb (
mcpy_valid_reg r1 r2 ma1 ma2)
then Stuck
else exec_memcpy (
IR tr ::
nil)
r1 r2 ma1 ma2 4
rs m
|
Pmemcpy64 r1 r2 ma1 ma2 tr1 tr2 =>
if PregEq.eq r2 tr1 ||
negb (
mcpy_valid_reg r1 r2 ma1 ma2) ||
negb (
thumb tt ||
ls_double_valid_regs tr1 tr2)
then Stuck
else exec_memcpy (
IR tr1 ::
IR tr2 ::
nil)
r1 r2 ma1 ma2 8
rs m
|
Pmemcpyf64 r1 r2 tr ofs1 ofs2 =>
exec_memcpy (
FR tr ::
nil)
r1 r2 (
Ofs ofs1) (
Ofs ofs2) 8
rs m
|
Pclz rd r1 =>
Next (
nextinstr (
rs#
rd <- (
match rs#
r1 with Vint n =>
Vint (
Int.clz n) | _ =>
Vundef end)))
m
|
Prbit rd r1 =>
Next (
nextinstr (
rs#
rd <- (
match rs#
r1 with Vint n =>
Vint (
Int.reverse_bits n) | _ =>
Vundef end)))
m
|
Prev rd r1 =>
Next (
nextinstr (
rs#
rd <- (
ExtValues.val_bswap32 (
rs#
r1))))
m
|
Padds r1 r2 so =>
let v2 :=
eval_shift_op so rs in
Next (
nextinstr ((
compare_int_add rs rs#
r2 v2 m) #
r1 <- (
Val.add rs#
r2 v2)))
m
|
Pbuiltin ef args res =>
Stuck (* treated specially below *)
The following instructions and directives are not generated directly by Asmgen,
so we do not model them.
|
Ppush _
|
Padc _ _ _
|
Pcfi_adjust _
|
Prev16 _ _
|
Prsc _ _ _
|
Psbc _ _ _
|
Prsbs _ _ _
|
Pdmb
|
Pdsb
|
Pisb
|
Pbne _
|
Pldr_p _ _ _
|
Pldrb_p _ _ _
|
Pldrh_p _ _ _
|
Pstr_p _ _ _
|
Pstrb_p _ _ _
|
Pstrh_p _ _ _
|
Pfcpy_fs _ _
|
Pfcpy_sf _ _
|
Pfcpy_fi _ _
|
Pfcpy_iif _ _ _
|
Pfcpy_if _ _
|
Pconstants _
|
Ploadsymbol_imm _ _ _
|
Pflid_lbl _ _ _
|
Pflis_lbl _ _ _
|
Pflid_imm _ _
|
Pflis_imm _ _
|
Ploadsymbol_lbl _ _ _ _
|
Pstack_chk_fail
=>
Stuck
end.
Translation of the LTL/Linear/Mach view of machine registers
to the ARM view. Note that no LTL register maps to IR14.
This register is reserved as temporary, to be used
by the generated ARM code.
Definition dreg_of (
r:
mreg) :
dreg :=
match r with
|
R0 =>
IR0 |
R1 =>
IR1 |
R2 =>
IR2 |
R3 =>
IR3
|
R4 =>
IR4 |
R5 =>
IR5 |
R6 =>
IR6 |
R7 =>
IR7
|
R8 =>
IR8 |
R9 =>
IR9 |
R10 =>
IR10 |
R11 =>
IR11
|
R12 =>
IR12
|
F0 =>
FR0 |
F1 =>
FR1 |
F2 =>
FR2 |
F3 =>
FR3
|
F4 =>
FR4 |
F5 =>
FR5 |
F6 =>
FR6 |
F7 =>
FR7
|
F8 =>
FR8 |
F9 =>
FR9 |
F10 =>
FR10 |
F11 =>
FR11
|
F12 =>
FR12 |
F13 =>
FR13 |
F14 =>
FR14 |
F15 =>
FR15
end.
Definition preg_of (
r:
mreg):
preg :=
dreg_of r.
Undefine all registers except SP and callee-save registers
Definition undef_caller_save_regs (
rs:
regset) :
regset :=
fun r =>
if preg_eq r SP
||
In_dec preg_eq r (
List.map preg_of (
List.filter is_callee_save all_mregs))
then rs r
else Vundef.
Extract the values of the arguments of an external call.
We exploit the calling conventions from module Conventions, except that
we use ARM registers instead of locations.
Inductive extcall_arg (
rs:
regset) (
m:
mem):
loc ->
val ->
Prop :=
|
extcall_arg_reg:
forall r,
extcall_arg rs m (
R r) (
rs (
preg_of r))
|
extcall_arg_stack:
forall ofs ty bofs v,
bofs =
Stacklayout.fe_ofs_arg + 4 *
ofs ->
Mem.loadv (
chunk_of_type ty)
m
(
Val.offset_ptr (
rs (
IR IR13)) (
Ptrofs.repr bofs)) =
Some v ->
extcall_arg rs m (
S Outgoing ofs ty)
v.
Inductive extcall_arg_pair (
rs:
regset) (
m:
mem):
rpair loc ->
val ->
Prop :=
|
extcall_arg_one:
forall l v,
extcall_arg rs m l v ->
extcall_arg_pair rs m (
One l)
v
|
extcall_arg_twolong:
forall hi lo vhi vlo,
extcall_arg rs m hi vhi ->
extcall_arg rs m lo vlo ->
extcall_arg_pair rs m (
Twolong hi lo) (
Val.longofwords vhi vlo).
Definition extcall_arguments
(
rs:
regset) (
m:
mem) (
sg:
signature) (
args:
list val) :
Prop :=
list_forall2 (
extcall_arg_pair rs m) (
loc_arguments sg)
args.
Definition loc_external_result (
sg:
signature) :
rpair preg :=
map_rpair preg_of (
loc_result sg).
Execution of the instruction at rs#PC.
Inductive state:
Type :=
|
State:
regset ->
mem ->
state.
Inductive step:
state ->
trace ->
state ->
Prop :=
|
exec_step_internal:
forall b ofs f i rs m rs' m',
rs PC =
Vptr b ofs ->
Genv.find_funct_ptr ge b =
Some (
Internal f) ->
find_instr (
Ptrofs.unsigned ofs) (
fn_code f) =
Some i ->
exec_instr f i rs m =
Next rs' m' ->
step (
State rs m)
E0 (
State rs' m')
|
exec_step_builtin:
forall b ofs f ef args res rs m vargs t vres rs' m',
rs PC =
Vptr b ofs ->
Genv.find_funct_ptr ge b =
Some (
Internal f) ->
find_instr (
Ptrofs.unsigned ofs)
f.(
fn_code) =
Some (
Pbuiltin ef args res) ->
eval_builtin_args ge rs (
rs SP)
m args vargs ->
external_call ef ge vargs m t vres m' ->
rs' =
nextinstr
(
set_res res vres
(
undef_regs (
DR IR14 ::
map preg_of (
destroyed_by_builtin ef))
rs)) ->
step (
State rs m)
t (
State rs' m')
|
exec_step_external:
forall b ef args res rs m t rs' m',
rs PC =
Vptr b Ptrofs.zero ->
Genv.find_funct_ptr ge b =
Some (
External ef) ->
external_call ef ge args m t res m' ->
extcall_arguments rs m (
ef_sig ef)
args ->
rs' = (
set_pair (
loc_external_result (
ef_sig ef) )
res (
undef_caller_save_regs rs))#
PC <- (
rs IR14) ->
step (
State rs m)
t (
State rs' m').
End RELSEM.
Execution of whole programs.
Inductive initial_state (
p:
program):
state ->
Prop :=
|
initial_state_intro:
forall m0,
let ge :=
Genv.globalenv p in
let rs0 :=
(
Pregmap.init Vundef)
#
PC <- (
Genv.symbol_address ge p.(
prog_main)
Ptrofs.zero)
#
IR14 <-
Vzero
#
IR13 <-
Vzero in
Genv.init_mem p =
Some m0 ->
initial_state p (
State rs0 m0).
Inductive final_state:
state ->
int ->
Prop :=
|
final_state_intro:
forall rs m r,
rs#
PC =
Vzero ->
rs#
IR0 =
Vint r ->
final_state (
State rs m)
r.
Definition semantics (
p:
program) :=
Semantics step (
initial_state p)
final_state (
Genv.globalenv p).
Determinacy of the Asm semantics.
Remark extcall_arguments_determ:
forall rs m sg args1 args2,
extcall_arguments rs m sg args1 ->
extcall_arguments rs m sg args2 ->
args1 =
args2.
Proof.
Lemma semantics_determinate:
forall p,
determinate (
semantics p).
Proof.
Ltac Equalities :=
match goal with
| [
H1: ?
a = ?
b,
H2: ?
a = ?
c |- _ ] =>
rewrite H1 in H2;
inv H2;
Equalities
| _ =>
idtac
end.
intros;
constructor;
simpl;
intros.
inv H;
inv H0;
Equalities.
split.
constructor.
auto.
discriminate.
discriminate.
assert (
vargs0 =
vargs)
by (
eapply eval_builtin_args_determ;
eauto).
subst vargs0.
exploit external_call_determ.
eexact H5.
eexact H11.
intros [
A B].
split.
auto.
intros.
destruct B;
auto.
subst.
auto.
assert (
args0 =
args)
by (
eapply extcall_arguments_determ;
eauto).
subst args0.
exploit external_call_determ.
eexact H3.
eexact H8.
intros [
A B].
split.
auto.
intros.
destruct B;
auto.
subst.
auto.
red;
intros;
inv H;
simpl.
lia.
inv H3;
eapply external_call_trace_length;
eauto.
eapply external_call_trace_length;
eauto.
inv H;
inv H0.
f_equal.
congruence.
inv H.
unfold Vzero in H0.
red;
intros;
red;
intros.
inv H;
congruence.
inv H;
inv H0.
congruence.
Qed.
Classification functions for processor registers (used in Asmgenproof).
Definition data_preg (
r:
preg) :
bool :=
match r with
|
IR IR14 =>
false
|
IR _ =>
true
|
FR _ =>
true
|
CR _ =>
false
|
PC =>
false
end.