Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CertiCompil
CompCert-KVX
Commits
6bff68d5
Commit
6bff68d5
authored
Mar 02, 2021
by
Léo Gourdin
Browse files
Merge conflicts solved and cleaning in Asmgenproof after expansion
parent
be4dcbd9
Changes
4
Expand all
Hide whitespace changes
Inline
Side-by-side
riscV/Asmgen.v
View file @
6bff68d5
...
...
@@ -105,8 +105,6 @@ Definition addimm32 := opimm32 Paddw Paddiw.
Definition
andimm32
:=
opimm32
Pandw
Pandiw
.
Definition
orimm32
:=
opimm32
Porw
Poriw
.
Definition
xorimm32
:=
opimm32
Pxorw
Pxoriw
.
Definition
sltimm32
:=
opimm32
Psltw
Psltiw
.
Definition
sltuimm32
:=
opimm32
Psltuw
Psltiuw
.
Definition
load_hilo64
(
r
:
ireg
)
(
hi
lo
:
int64
)
k
:=
if
Int64
.
eq
lo
Int64
.
zero
then
Pluil
r
hi
::
k
...
...
@@ -132,8 +130,6 @@ Definition addimm64 := opimm64 Paddl Paddil.
Definition
andimm64
:=
opimm64
Pandl
Pandil
.
Definition
orimm64
:=
opimm64
Porl
Poril
.
Definition
xorimm64
:=
opimm64
Pxorl
Pxoril
.
Definition
sltimm64
:=
opimm64
Psltl
Psltil
.
Definition
sltuimm64
:=
opimm64
Psltul
Psltiul
.
Definition
addptrofs
(
rd
rs
:
ireg
)
(
n
:
ptrofs
)
(
k
:
code
)
:=
if
Ptrofs
.
eq_dec
n
Ptrofs
.
zero
then
...
...
@@ -145,66 +141,6 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
(
**
Translation
of
conditional
branches
.
*
)
Definition
transl_cbranch_int32s
(
cmp
:
comparison
)
(
r1
r2
:
ireg0
)
(
lbl
:
label
)
:=
match
cmp
with
|
Ceq
=>
Pbeqw
r1
r2
lbl
|
Cne
=>
Pbnew
r1
r2
lbl
|
Clt
=>
Pbltw
r1
r2
lbl
|
Cle
=>
Pbgew
r2
r1
lbl
|
Cgt
=>
Pbltw
r2
r1
lbl
|
Cge
=>
Pbgew
r1
r2
lbl
end
.
Definition
transl_cbranch_int32u
(
cmp
:
comparison
)
(
r1
r2
:
ireg0
)
(
lbl
:
label
)
:=
match
cmp
with
|
Ceq
=>
Pbeqw
r1
r2
lbl
|
Cne
=>
Pbnew
r1
r2
lbl
|
Clt
=>
Pbltuw
r1
r2
lbl
|
Cle
=>
Pbgeuw
r2
r1
lbl
|
Cgt
=>
Pbltuw
r2
r1
lbl
|
Cge
=>
Pbgeuw
r1
r2
lbl
end
.
Definition
transl_cbranch_int64s
(
cmp
:
comparison
)
(
r1
r2
:
ireg0
)
(
lbl
:
label
)
:=
match
cmp
with
|
Ceq
=>
Pbeql
r1
r2
lbl
|
Cne
=>
Pbnel
r1
r2
lbl
|
Clt
=>
Pbltl
r1
r2
lbl
|
Cle
=>
Pbgel
r2
r1
lbl
|
Cgt
=>
Pbltl
r2
r1
lbl
|
Cge
=>
Pbgel
r1
r2
lbl
end
.
Definition
transl_cbranch_int64u
(
cmp
:
comparison
)
(
r1
r2
:
ireg0
)
(
lbl
:
label
)
:=
match
cmp
with
|
Ceq
=>
Pbeql
r1
r2
lbl
|
Cne
=>
Pbnel
r1
r2
lbl
|
Clt
=>
Pbltul
r1
r2
lbl
|
Cle
=>
Pbgeul
r2
r1
lbl
|
Cgt
=>
Pbltul
r2
r1
lbl
|
Cge
=>
Pbgeul
r1
r2
lbl
end
.
Definition
transl_cond_float
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
fs1
fs2
:
freg
)
:=
match
cmp
with
|
Ceq
=>
(
Pfeqd
rd
fs1
fs2
,
true
)
|
Cne
=>
(
Pfeqd
rd
fs1
fs2
,
false
)
|
Clt
=>
(
Pfltd
rd
fs1
fs2
,
true
)
|
Cle
=>
(
Pfled
rd
fs1
fs2
,
true
)
|
Cgt
=>
(
Pfltd
rd
fs2
fs1
,
true
)
|
Cge
=>
(
Pfled
rd
fs2
fs1
,
true
)
end
.
Definition
transl_cond_single
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
fs1
fs2
:
freg
)
:=
match
cmp
with
|
Ceq
=>
(
Pfeqs
rd
fs1
fs2
,
true
)
|
Cne
=>
(
Pfeqs
rd
fs1
fs2
,
false
)
|
Clt
=>
(
Pflts
rd
fs1
fs2
,
true
)
|
Cle
=>
(
Pfles
rd
fs1
fs2
,
true
)
|
Cgt
=>
(
Pflts
rd
fs2
fs1
,
true
)
|
Cge
=>
(
Pfles
rd
fs2
fs1
,
true
)
end
.
Definition
apply_bin_r0_r0r0lbl
(
optR0
:
option
bool
)
(
sem
:
ireg0
->
ireg0
->
label
->
instruction
)
(
r1
r2
:
ireg0
)
(
lbl
:
label
)
:=
match
optR0
with
|
None
=>
sem
r1
r2
lbl
...
...
@@ -222,59 +158,6 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru
Definition
transl_cbranch
(
cond
:
condition
)
(
args
:
list
mreg
)
(
lbl
:
label
)
(
k
:
code
)
:=
match
cond
,
args
with
|
Ccomp
c
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
transl_cbranch_int32s
c
r1
r2
lbl
::
k
)
|
Ccompu
c
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
transl_cbranch_int32u
c
r1
r2
lbl
::
k
)
|
Ccompimm
c
n
,
a1
::
nil
=>
do
r1
<-
ireg_of
a1
;
OK
(
if
Int
.
eq
n
Int
.
zero
then
transl_cbranch_int32s
c
r1
X0
lbl
::
k
else
loadimm32
X31
n
(
transl_cbranch_int32s
c
r1
X31
lbl
::
k
))
|
Ccompuimm
c
n
,
a1
::
nil
=>
do
r1
<-
ireg_of
a1
;
OK
(
if
Int
.
eq
n
Int
.
zero
then
transl_cbranch_int32u
c
r1
X0
lbl
::
k
else
loadimm32
X31
n
(
transl_cbranch_int32u
c
r1
X31
lbl
::
k
))
|
Ccompl
c
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
transl_cbranch_int64s
c
r1
r2
lbl
::
k
)
|
Ccomplu
c
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
transl_cbranch_int64u
c
r1
r2
lbl
::
k
)
|
Ccomplimm
c
n
,
a1
::
nil
=>
do
r1
<-
ireg_of
a1
;
OK
(
if
Int64
.
eq
n
Int64
.
zero
then
transl_cbranch_int64s
c
r1
X0
lbl
::
k
else
loadimm64
X31
n
(
transl_cbranch_int64s
c
r1
X31
lbl
::
k
))
|
Ccompluimm
c
n
,
a1
::
nil
=>
do
r1
<-
ireg_of
a1
;
OK
(
if
Int64
.
eq
n
Int64
.
zero
then
transl_cbranch_int64u
c
r1
X0
lbl
::
k
else
loadimm64
X31
n
(
transl_cbranch_int64u
c
r1
X31
lbl
::
k
))
|
Ccompf
c
,
f1
::
f2
::
nil
=>
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
let
(
insn
,
normal
)
:=
transl_cond_float
c
X31
r1
r2
in
OK
(
insn
::
(
if
normal
then
Pbnew
X31
X0
lbl
else
Pbeqw
X31
X0
lbl
)
::
k
)
|
Cnotcompf
c
,
f1
::
f2
::
nil
=>
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
let
(
insn
,
normal
)
:=
transl_cond_float
c
X31
r1
r2
in
OK
(
insn
::
(
if
normal
then
Pbeqw
X31
X0
lbl
else
Pbnew
X31
X0
lbl
)
::
k
)
|
Ccompfs
c
,
f1
::
f2
::
nil
=>
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
let
(
insn
,
normal
)
:=
transl_cond_single
c
X31
r1
r2
in
OK
(
insn
::
(
if
normal
then
Pbnew
X31
X0
lbl
else
Pbeqw
X31
X0
lbl
)
::
k
)
|
Cnotcompfs
c
,
f1
::
f2
::
nil
=>
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
let
(
insn
,
normal
)
:=
transl_cond_single
c
X31
r1
r2
in
OK
(
insn
::
(
if
normal
then
Pbeqw
X31
X0
lbl
else
Pbnew
X31
X0
lbl
)
::
k
)
|
CEbeqw
optR0
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbeqw
r1
r2
lbl
::
k
)
...
...
@@ -327,133 +210,6 @@ Definition transl_cbranch
Error
(
msg
"Asmgen.transl_cond_branch"
)
end
.
(
**
Translation
of
a
condition
operator
.
The
generated
code
sets
the
[
rd
]
target
register
to
0
or
1
depending
on
the
truth
value
of
the
condition
.
*
)
Definition
transl_cond_int32s
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
r1
r2
:
ireg0
)
(
k
:
code
)
:=
match
cmp
with
|
Ceq
=>
Pseqw
rd
r1
r2
::
k
|
Cne
=>
Psnew
rd
r1
r2
::
k
|
Clt
=>
Psltw
rd
r1
r2
::
k
|
Cle
=>
Psltw
rd
r2
r1
::
Pxoriw
rd
rd
Int
.
one
::
k
|
Cgt
=>
Psltw
rd
r2
r1
::
k
|
Cge
=>
Psltw
rd
r1
r2
::
Pxoriw
rd
rd
Int
.
one
::
k
end
.
Definition
transl_cond_int32u
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
r1
r2
:
ireg0
)
(
k
:
code
)
:=
match
cmp
with
|
Ceq
=>
Pseqw
rd
r1
r2
::
k
|
Cne
=>
Psnew
rd
r1
r2
::
k
|
Clt
=>
Psltuw
rd
r1
r2
::
k
|
Cle
=>
Psltuw
rd
r2
r1
::
Pxoriw
rd
rd
Int
.
one
::
k
|
Cgt
=>
Psltuw
rd
r2
r1
::
k
|
Cge
=>
Psltuw
rd
r1
r2
::
Pxoriw
rd
rd
Int
.
one
::
k
end
.
Definition
transl_cond_int64s
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
r1
r2
:
ireg0
)
(
k
:
code
)
:=
match
cmp
with
|
Ceq
=>
Pseql
rd
r1
r2
::
k
|
Cne
=>
Psnel
rd
r1
r2
::
k
|
Clt
=>
Psltl
rd
r1
r2
::
k
|
Cle
=>
Psltl
rd
r2
r1
::
Pxoriw
rd
rd
Int
.
one
::
k
|
Cgt
=>
Psltl
rd
r2
r1
::
k
|
Cge
=>
Psltl
rd
r1
r2
::
Pxoriw
rd
rd
Int
.
one
::
k
end
.
Definition
transl_cond_int64u
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
r1
r2
:
ireg0
)
(
k
:
code
)
:=
match
cmp
with
|
Ceq
=>
Pseql
rd
r1
r2
::
k
|
Cne
=>
Psnel
rd
r1
r2
::
k
|
Clt
=>
Psltul
rd
r1
r2
::
k
|
Cle
=>
Psltul
rd
r2
r1
::
Pxoriw
rd
rd
Int
.
one
::
k
|
Cgt
=>
Psltul
rd
r2
r1
::
k
|
Cge
=>
Psltul
rd
r1
r2
::
Pxoriw
rd
rd
Int
.
one
::
k
end
.
Definition
transl_condimm_int32s
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
r1
:
ireg
)
(
n
:
int
)
(
k
:
code
)
:=
if
Int
.
eq
n
Int
.
zero
then
transl_cond_int32s
cmp
rd
r1
X0
k
else
match
cmp
with
|
Ceq
|
Cne
=>
xorimm32
rd
r1
n
(
transl_cond_int32s
cmp
rd
rd
X0
k
)
|
Clt
=>
sltimm32
rd
r1
n
k
|
Cle
=>
if
Int
.
eq
n
(
Int
.
repr
Int
.
max_signed
)
then
loadimm32
rd
Int
.
one
k
else
sltimm32
rd
r1
(
Int
.
add
n
Int
.
one
)
k
|
_
=>
loadimm32
X31
n
(
transl_cond_int32s
cmp
rd
r1
X31
k
)
end
.
Definition
transl_condimm_int32u
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
r1
:
ireg
)
(
n
:
int
)
(
k
:
code
)
:=
if
Int
.
eq
n
Int
.
zero
then
transl_cond_int32u
cmp
rd
r1
X0
k
else
match
cmp
with
|
Clt
=>
sltuimm32
rd
r1
n
k
|
_
=>
loadimm32
X31
n
(
transl_cond_int32u
cmp
rd
r1
X31
k
)
end
.
Definition
transl_condimm_int64s
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
r1
:
ireg
)
(
n
:
int64
)
(
k
:
code
)
:=
if
Int64
.
eq
n
Int64
.
zero
then
transl_cond_int64s
cmp
rd
r1
X0
k
else
match
cmp
with
|
Ceq
|
Cne
=>
xorimm64
rd
r1
n
(
transl_cond_int64s
cmp
rd
rd
X0
k
)
|
Clt
=>
sltimm64
rd
r1
n
k
|
Cle
=>
if
Int64
.
eq
n
(
Int64
.
repr
Int64
.
max_signed
)
then
loadimm32
rd
Int
.
one
k
else
sltimm64
rd
r1
(
Int64
.
add
n
Int64
.
one
)
k
|
_
=>
loadimm64
X31
n
(
transl_cond_int64s
cmp
rd
r1
X31
k
)
end
.
Definition
transl_condimm_int64u
(
cmp
:
comparison
)
(
rd
:
ireg
)
(
r1
:
ireg
)
(
n
:
int64
)
(
k
:
code
)
:=
if
Int64
.
eq
n
Int64
.
zero
then
transl_cond_int64u
cmp
rd
r1
X0
k
else
match
cmp
with
|
Clt
=>
sltuimm64
rd
r1
n
k
|
_
=>
loadimm64
X31
n
(
transl_cond_int64u
cmp
rd
r1
X31
k
)
end
.
Definition
transl_cond_op
(
cond
:
condition
)
(
rd
:
ireg
)
(
args
:
list
mreg
)
(
k
:
code
)
:=
match
cond
,
args
with
|
Ccomp
c
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
transl_cond_int32s
c
rd
r1
r2
k
)
|
Ccompu
c
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
transl_cond_int32u
c
rd
r1
r2
k
)
|
Ccompimm
c
n
,
a1
::
nil
=>
do
r1
<-
ireg_of
a1
;
OK
(
transl_condimm_int32s
c
rd
r1
n
k
)
|
Ccompuimm
c
n
,
a1
::
nil
=>
do
r1
<-
ireg_of
a1
;
OK
(
transl_condimm_int32u
c
rd
r1
n
k
)
|
Ccompl
c
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
transl_cond_int64s
c
rd
r1
r2
k
)
|
Ccomplu
c
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
transl_cond_int64u
c
rd
r1
r2
k
)
|
Ccomplimm
c
n
,
a1
::
nil
=>
do
r1
<-
ireg_of
a1
;
OK
(
transl_condimm_int64s
c
rd
r1
n
k
)
|
Ccompluimm
c
n
,
a1
::
nil
=>
do
r1
<-
ireg_of
a1
;
OK
(
transl_condimm_int64u
c
rd
r1
n
k
)
|
Ccompf
c
,
f1
::
f2
::
nil
=>
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
let
(
insn
,
normal
)
:=
transl_cond_float
c
rd
r1
r2
in
OK
(
insn
::
if
normal
then
k
else
Pxoriw
rd
rd
Int
.
one
::
k
)
|
Cnotcompf
c
,
f1
::
f2
::
nil
=>
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
let
(
insn
,
normal
)
:=
transl_cond_float
c
rd
r1
r2
in
OK
(
insn
::
if
normal
then
Pxoriw
rd
rd
Int
.
one
::
k
else
k
)
|
Ccompfs
c
,
f1
::
f2
::
nil
=>
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
let
(
insn
,
normal
)
:=
transl_cond_single
c
rd
r1
r2
in
OK
(
insn
::
if
normal
then
k
else
Pxoriw
rd
rd
Int
.
one
::
k
)
|
Cnotcompfs
c
,
f1
::
f2
::
nil
=>
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
let
(
insn
,
normal
)
:=
transl_cond_single
c
rd
r1
r2
in
OK
(
insn
::
if
normal
then
Pxoriw
rd
rd
Int
.
one
::
k
else
k
)
|
_
,
_
=>
Error
(
msg
"Asmgen.transl_cond_op"
)
end
.
(
**
Translation
of
the
arithmetic
operation
[
r
<-
op
(
args
)].
The
corresponding
instructions
are
prepended
to
[
k
].
*
)
...
...
@@ -767,9 +523,6 @@ Definition transl_op
|
Osingleoflongu
,
a1
::
nil
=>
do
rd
<-
freg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pfcvtslu
rd
rs
::
k
)
|
Ocmp
cmp
,
_
=>
do
rd
<-
ireg_of
res
;
transl_cond_op
cmp
rd
args
k
|
OEseqw
optR0
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
...
...
@@ -912,18 +665,12 @@ Definition transl_op
|
Ofloat_of_bits
,
a1
::
nil
=>
do
rd
<-
freg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pfmvdx
rd
rs
::
k
)
|
Ocmp
cmp
,
_
=>
do
rd
<-
ireg_of
res
;
transl_cond_op
cmp
rd
args
k
|
Oselectl
,
b
::
t
::
f
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rb
<-
ireg_of
b
;
do
rt
<-
ireg_of
t
;
do
rf
<-
ireg_of
f
;
OK
(
Pselectl
rd
rb
rt
rf
::
k
)
|
_
,
_
=>
Error
(
msg
"Asmgen.transl_op"
)
end
.
...
...
riscV/Asmgenproof.v
View file @
6bff68d5
...
...
@@ -161,165 +161,37 @@ Proof.
Qed
.
Hint
Resolve
addptrofs_label
:
labels
.
Remark
transl_cond_float_nolabel
:
forall
c
r1
r2
r3
insn
normal
,
transl_cond_float
c
r1
r2
r3
=
(
insn
,
normal
)
->
nolabel
insn
.
Proof
.
unfold
transl_cond_float
;
intros
.
destruct
c
;
inv
H
;
exact
I
.
Qed
.
Remark
transl_cond_single_nolabel
:
forall
c
r1
r2
r3
insn
normal
,
transl_cond_single
c
r1
r2
r3
=
(
insn
,
normal
)
->
nolabel
insn
.
Proof
.
unfold
transl_cond_single
;
intros
.
destruct
c
;
inv
H
;
exact
I
.
Qed
.
Remark
transl_cbranch_label
:
forall
cond
args
lbl
k
c
,
transl_cbranch
cond
args
lbl
k
=
OK
c
->
tail_nolabel
k
c
.
Proof
.
intros
.
unfold
transl_cbranch
in
H
;
destruct
cond
;
TailNoLabel
.
-
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
(
Int
.
eq
n
Int
.
zero
).
destruct
c0
;
simpl
;
TailNoLabel
.
apply
tail_nolabel_trans
with
(
transl_cbranch_int32s
c0
x
X31
lbl
::
k
).
auto
with
labels
.
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
(
Int
.
eq
n
Int
.
zero
).
destruct
c0
;
simpl
;
TailNoLabel
.
apply
tail_nolabel_trans
with
(
transl_cbranch_int32u
c0
x
X31
lbl
::
k
).
auto
with
labels
.
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
(
Int64
.
eq
n
Int64
.
zero
).
destruct
c0
;
simpl
;
TailNoLabel
.
apply
tail_nolabel_trans
with
(
transl_cbranch_int64s
c0
x
X31
lbl
::
k
).
auto
with
labels
.
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
(
Int64
.
eq
n
Int64
.
zero
).
destruct
c0
;
simpl
;
TailNoLabel
.
apply
tail_nolabel_trans
with
(
transl_cbranch_int64u
c0
x
X31
lbl
::
k
).
auto
with
labels
.
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
(
transl_cond_float
c0
X31
x
x0
)
as
[
insn
normal
]
eqn
:
F
;
inv
EQ2
.
apply
tail_nolabel_cons
.
eapply
transl_cond_float_nolabel
;
eauto
.
destruct
normal
;
TailNoLabel
.
-
destruct
(
transl_cond_float
c0
X31
x
x0
)
as
[
insn
normal
]
eqn
:
F
;
inv
EQ2
.
apply
tail_nolabel_cons
.
eapply
transl_cond_float_nolabel
;
eauto
.
destruct
normal
;
TailNoLabel
.
-
destruct
(
transl_cond_single
c0
X31
x
x0
)
as
[
insn
normal
]
eqn
:
F
;
inv
EQ2
.
apply
tail_nolabel_cons
.
eapply
transl_cond_single_nolabel
;
eauto
.
destruct
normal
;
TailNoLabel
.
-
destruct
(
transl_cond_single
c0
X31
x
x0
)
as
[
insn
normal
]
eqn
:
F
;
inv
EQ2
.
apply
tail_nolabel_cons
.
eapply
transl_cond_single_nolabel
;
eauto
.
destruct
normal
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
TailNoLabel
.
all:
destruct
optR0
as
[[]
|
];
TailNoLabel
.
Qed
.
Remark
transl_cond_op_label
:
forall
cond
args
r
k
c
,
transl_cond_op
cond
r
args
k
=
OK
c
->
tail_nolabel
k
c
.
Proof
.
intros
.
unfold
transl_cond_op
in
H
;
destruct
cond
;
TailNoLabel
.
-
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
c0
;
simpl
;
TailNoLabel
.
-
unfold
transl_condimm_int32s
.
destruct
(
Int
.
eq
n
Int
.
zero
).
+
destruct
c0
;
simpl
;
TailNoLabel
.
+
destruct
c0
;
simpl
.
*
eapply
tail_nolabel_trans
;
[
apply
opimm32_label
;
intros
;
exact
I
|
TailNoLabel
].
*
eapply
tail_nolabel_trans
;
[
apply
opimm32_label
;
intros
;
exact
I
|
TailNoLabel
].
*
apply
opimm32_label
;
intros
;
exact
I
.
*
destruct
(
Int
.
eq
n
(
Int
.
repr
Int
.
max_signed
)).
apply
loadimm32_label
.
apply
opimm32_label
;
intros
;
exact
I
.
*
eapply
tail_nolabel_trans
.
apply
loadimm32_label
.
TailNoLabel
.
*
eapply
tail_nolabel_trans
.
apply
loadimm32_label
.
TailNoLabel
.
-
unfold
transl_condimm_int32u
.
destruct
(
Int
.
eq
n
Int
.
zero
).
+
destruct
c0
;
simpl
;
TailNoLabel
.
+
destruct
c0
;
simpl
;
try
(
eapply
tail_nolabel_trans
;
[
apply
loadimm32_label
|
TailNoLabel
]).
apply
opimm32_label
;
intros
;
exact
I
.
-
destruct
c0
;
simpl
;
TailNoLabel
.
-
destruct
c0
;
simpl
;
TailNoLabel
.
-
unfold
transl_condimm_int64s
.
destruct
(
Int64
.
eq
n
Int64
.
zero
).
+
destruct
c0
;
simpl
;
TailNoLabel
.
+
destruct
c0
;
simpl
.
*
eapply
tail_nolabel_trans
;
[
apply
opimm64_label
;
intros
;
exact
I
|
TailNoLabel
].
*
eapply
tail_nolabel_trans
;
[
apply
opimm64_label
;
intros
;
exact
I
|
TailNoLabel
].
*
apply
opimm64_label
;
intros
;
exact
I
.
*
destruct
(
Int64
.
eq
n
(
Int64
.
repr
Int64
.
max_signed
)).
apply
loadimm32_label
.
apply
opimm64_label
;
intros
;
exact
I
.
*
eapply
tail_nolabel_trans
.
apply
loadimm64_label
.
TailNoLabel
.
*
eapply
tail_nolabel_trans
.
apply
loadimm64_label
.
TailNoLabel
.
-
unfold
transl_condimm_int64u
.
destruct
(
Int64
.
eq
n
Int64
.
zero
).
+
destruct
c0
;
simpl
;
TailNoLabel
.
+
destruct
c0
;
simpl
;
try
(
eapply
tail_nolabel_trans
;
[
apply
loadimm64_label
|
TailNoLabel
]).
apply
opimm64_label
;
intros
;
exact
I
.
-
destruct
(
transl_cond_float
c0
r
x
x0
)
as
[
insn
normal
]
eqn
:
F
;
inv
EQ2
.
apply
tail_nolabel_cons
.
eapply
transl_cond_float_nolabel
;
eauto
.
destruct
normal
;
TailNoLabel
.
-
destruct
(
transl_cond_float
c0
r
x
x0
)
as
[
insn
normal
]
eqn
:
F
;
inv
EQ2
.
apply
tail_nolabel_cons
.
eapply
transl_cond_float_nolabel
;
eauto
.
destruct
normal
;
TailNoLabel
.
-
destruct
(
transl_cond_single
c0
r
x
x0
)
as
[
insn
normal
]
eqn
:
F
;
inv
EQ2
.
apply
tail_nolabel_cons
.
eapply
transl_cond_single_nolabel
;
eauto
.
destruct
normal
;
TailNoLabel
.
-
destruct
(
transl_cond_single
c0
r
x
x0
)
as
[
insn
normal
]
eqn
:
F
;
inv
EQ2
.
apply
tail_nolabel_cons
.
eapply
transl_cond_single_nolabel
;
eauto
.
destruct
normal
;
TailNoLabel
.
Qed
.
Remark
transl_op_label
:
forall
op
args
r
k
c
,
transl_op
op
args
r
k
=
OK
c
->
tail_nolabel
k
c
.
Proof
.
Opaque
Int
.
eq
.
unfold
transl_op
;
intros
;
destruct
op
;
TailNoLabel
.
-
destruct
(
preg_of
r
);
try
discriminate
;
destruct
(
preg_of
m
);
inv
H
;
TailNoLabel
.
-
destruct
(
Float
.
eq_dec
n
Float
.
zero
);
TailNoLabel
.
-
destruct
(
Float32
.
eq_dec
n
Float32
.
zero
);
TailNoLabel
.
-
destruct
(
Archi
.
pic_code
tt
&&
negb
(
Ptrofs
.
eq
ofs
Ptrofs
.
zero
)).
+
eapply
tail_nolabel_trans
;
[
|
apply
addptrofs_label
].
TailNoLabel
.
+
TailNoLabel
.
-
apply
opimm32_label
;
intros
;
exact
I
.
-
apply
opimm32_label
;
intros
;
exact
I
.
-
apply
opimm32_label
;
intros
;
exact
I
.
-
apply
opimm32_label
;
intros
;
exact
I
.
-
destruct
(
Int
.
eq
n
Int
.
zero
);
try
destruct
(
Int
.
eq
n
Int
.
one
);
TailNoLabel
.
-
apply
opimm64_label
;
intros
;
exact
I
.
-
apply
opimm64_label
;
intros
;
exact
I
.
-
apply
opimm64_label
;
intros
;
exact
I
.
-
apply
opimm64_label
;
intros
;
exact
I
.
-
destruct
(
Int
.
eq
n
Int
.
zero
);
try
destruct
(
Int
.
eq
n
Int
.
one
);
TailNoLabel
.
-
eapply
transl_cond_op_label
;
eauto
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
-
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
{
destruct
(
preg_of
r
);
try
discriminate
;
destruct
(
preg_of
m
);
inv
H
;
TailNoLabel
.
}
{
destruct
(
Float
.
eq_dec
n
Float
.
zero
);
TailNoLabel
.
}
{
destruct
(
Float32
.
eq_dec
n
Float32
.
zero
);
TailNoLabel
.
}
{
destruct
(
Archi
.
pic_code
tt
&&
negb
(
Ptrofs
.
eq
ofs
Ptrofs
.
zero
)).
+
eapply
tail_nolabel_trans
;
[
|
apply
addptrofs_label
].
TailNoLabel
.
+
TailNoLabel
.
}
{
apply
opimm32_label
;
intros
;
exact
I
.
}
{
apply
opimm32_label
;
intros
;
exact
I
.
}
{
apply
opimm32_label
;
intros
;
exact
I
.
}
{
apply
opimm32_label
;
intros
;
exact
I
.
}
{
destruct
(
Int
.
eq
n
Int
.
zero
);
try
destruct
(
Int
.
eq
n
Int
.
one
);
TailNoLabel
.
}
{
apply
opimm64_label
;
intros
;
exact
I
.
}
{
apply
opimm64_label
;
intros
;
exact
I
.
}
{
apply
opimm64_label
;
intros
;
exact
I
.
}
{
apply
opimm64_label
;
intros
;
exact
I
.
}
{
destruct
(
Int
.
eq
n
Int
.
zero
);
try
destruct
(
Int
.
eq
n
Int
.
one
);
TailNoLabel
.
}
all:
destruct
optR0
as
[[]
|
];
simpl
;
TailNoLabel
.
Qed
.
Remark
indexed_memory_access_label
:
...
...
riscV/Asmgenproof1.v
View file @
6bff68d5
This diff is collapsed.
Click to expand it.
riscV/Op.v
View file @
6bff68d5
...
...
@@ -200,8 +200,7 @@ Inductive operation : Type :=
|
OEfled
(
**
r
compare
less
-
than
/
equal
*
)
|
OEfeqs
(
**
r
compare
equal
*
)
|
OEflts
(
**
r
compare
less
-
than
*
)
|
OEfles
.
(
**
r
compare
less
-
than
/
equal
*
)
|
Ocmp
(
cond
:
condition
)
(
**
r
[
rd
=
1
]
if
condition
holds
,
[
rd
=
0
]
otherwise
.
*
)
|
OEfles
(
**
r
compare
less
-
than
/
equal
*
)
|
Obits_of_single
|
Obits_of_float
|
Osingle_of_bits
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment