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
b3009fc0
Commit
b3009fc0
authored
Apr 09, 2021
by
Léo Gourdin
Browse files
Merge branch 'riscv-work' into kvx-work
parents
706b6384
b0252257
Changes
21
Expand all
Hide whitespace changes
Inline
Side-by-side
backend/Stackingproof.v
View file @
b3009fc0
...
...
@@ -868,7 +868,8 @@ Qed.
Remark
transl_destroyed_by_op
:
forall
op
e
,
destroyed_by_op
(
transl_op
e
op
)
=
destroyed_by_op
op
.
Proof
.
intros
;
destruct
op
;
reflexivity
.
intros
;
destruct
op
;
try
reflexivity
;
simpl
.
all:
destruct
optR
as
[[]
|
];
simpl
;
try
reflexivity
.
Qed
.
Remark
transl_destroyed_by_load
:
...
...
driver/Clflags.ml
View file @
b3009fc0
...
...
@@ -105,7 +105,6 @@ let option_fmadd = ref true
let
option_div_i32
=
ref
"stsud"
let
option_div_i64
=
ref
"stsud"
let
option_fcoalesce_mem
=
ref
true
let
option_fexpanse_rtlcond
=
ref
true
let
option_fforward_moves
=
ref
false
let
option_fmove_loop_invariants
=
ref
false
let
option_fnontrap_loads
=
ref
true
...
...
driver/Driver.ml
View file @
b3009fc0
...
...
@@ -444,7 +444,6 @@ let cmdline_actions =
@
f_opt
"madd"
option_fmadd
@
f_opt
"nontrap-loads"
option_fnontrap_loads
@
f_opt
"coalesce-mem"
option_fcoalesce_mem
@
f_opt
"expanse-rtlcond"
option_fexpanse_rtlcond
@
f_opt
"all-loads-nontrap"
option_all_loads_nontrap
@
f_opt
"forward-moves"
option_fforward_moves
(* Code generation options *)
...
...
riscV/Asm.v
View file @
b3009fc0
...
...
@@ -982,6 +982,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
end
|
Pbuiltin
ef
args
res
=>
Stuck
(
**
r
treated
specially
below
*
)
|
Pnop
=>
Next
(
nextinstr
rs
)
m
(
**
r
Pnop
is
used
by
an
oracle
during
expansion
*
)
(
**
The
following
instructions
and
directives
are
not
generated
directly
by
Asmgen
,
so
we
do
not
model
them
.
*
)
...
...
@@ -1002,7 +1003,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
|
Pfmsubd
_
_
_
_
|
Pfnmaddd
_
_
_
_
|
Pfnmsubd
_
_
_
_
|
Pnop
=>
Stuck
end
.
...
...
riscV/Asmexpand.ml
View file @
b3009fc0
...
...
@@ -23,6 +23,7 @@ open Asm
open
Asmexpandaux
open
AST
open
Camlcoq
open
Asmgen
open
!
Integers
exception
Error
of
string
...
...
@@ -44,11 +45,13 @@ let align n a = (n + a - 1) land (-a)
(* Emit instruction sequences that set or offset a register by a constant. *)
let
expand_loadimm32
dst
n
=
List
.
iter
emit
(
Asmgen
.
loadimm32
dst
n
[]
)
match
make_immed32
n
with
|
Imm32_single
imm
->
emit
(
Paddiw
(
dst
,
X0
,
imm
))
|
Imm32_pair
(
hi
,
lo
)
->
List
.
iter
emit
(
load_hilo32
dst
hi
lo
[]
)
let
expand_addptrofs
dst
src
n
=
List
.
iter
emit
(
Asmgen
.
addptrofs
dst
src
n
[]
)
List
.
iter
emit
(
addptrofs
dst
src
n
[]
)
let
expand_storeind_ptr
src
base
ofs
=
List
.
iter
emit
(
Asmgen
.
storeind_ptr
src
base
ofs
[]
)
List
.
iter
emit
(
storeind_ptr
src
base
ofs
[]
)
(* Built-ins. They come in two flavors:
- annotation statements: take their arguments in registers or stack
...
...
riscV/Asmgen.v
View file @
b3009fc0
...
...
@@ -86,12 +86,6 @@ Definition make_immed64 (val: int64) :=
Definition
load_hilo32
(
r
:
ireg
)
(
hi
lo
:
int
)
k
:=
if
Int
.
eq
lo
Int
.
zero
then
Pluiw
r
hi
::
k
else
Pluiw
r
hi
::
Paddiw
r
r
lo
::
k
.
Definition
loadimm32
(
r
:
ireg
)
(
n
:
int
)
(
k
:
code
)
:=
match
make_immed32
n
with
|
Imm32_single
imm
=>
Paddiw
r
X0
imm
::
k
|
Imm32_pair
hi
lo
=>
load_hilo32
r
hi
lo
k
end
.
Definition
opimm32
(
op
:
ireg
->
ireg0
->
ireg0
->
instruction
)
(
opimm
:
ireg
->
ireg0
->
int
->
instruction
)
...
...
@@ -102,21 +96,11 @@ Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction)
end
.
Definition
addimm32
:=
opimm32
Paddw
Paddiw
.
Definition
andimm32
:=
opimm32
Pandw
Pandiw
.
Definition
orimm32
:=
opimm32
Porw
Poriw
.
Definition
xorimm32
:=
opimm32
Pxorw
Pxoriw
.
Definition
load_hilo64
(
r
:
ireg
)
(
hi
lo
:
int64
)
k
:=
if
Int64
.
eq
lo
Int64
.
zero
then
Pluil
r
hi
::
k
else
Pluil
r
hi
::
Paddil
r
r
lo
::
k
.
Definition
loadimm64
(
r
:
ireg
)
(
n
:
int64
)
(
k
:
code
)
:=
match
make_immed64
n
with
|
Imm64_single
imm
=>
Paddil
r
X0
imm
::
k
|
Imm64_pair
hi
lo
=>
load_hilo64
r
hi
lo
k
|
Imm64_large
imm
=>
Ploadli
r
imm
::
k
end
.
Definition
opimm64
(
op
:
ireg
->
ireg0
->
ireg0
->
instruction
)
(
opimm
:
ireg
->
ireg0
->
int64
->
instruction
)
(
rd
rs
:
ireg
)
(
n
:
int64
)
(
k
:
code
)
:=
...
...
@@ -127,9 +111,6 @@ Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
end
.
Definition
addimm64
:=
opimm64
Paddl
Paddil
.
Definition
andimm64
:=
opimm64
Pandl
Pandil
.
Definition
orimm64
:=
opimm64
Porl
Poril
.
Definition
xorimm64
:=
opimm64
Pxorl
Pxoril
.
Definition
addptrofs
(
rd
rs
:
ireg
)
(
n
:
ptrofs
)
(
k
:
code
)
:=
if
Ptrofs
.
eq_dec
n
Ptrofs
.
zero
then
...
...
@@ -139,73 +120,88 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
then
addimm64
rd
rs
(
Ptrofs
.
to_int64
n
)
k
else
addimm32
rd
rs
(
Ptrofs
.
to_int
n
)
k
.
(
**
Translation
of
conditional
branches
.
*
)
(
**
Functions
to
select
a
special
register
according
to
the
op
"oreg"
argument
from
RTL
*
)
Definition
apply_bin_
r0_r0r0lbl
(
optR
0
:
option
bool
)
(
sem
:
ireg0
->
ireg0
->
label
->
instruction
)
(
r1
r2
:
ireg0
)
(
lbl
:
label
)
:=
match
optR
0
with
|
None
=>
sem
r1
r2
lbl
|
Some
true
=>
sem
X0
r1
lbl
|
Some
false
=>
sem
r1
X0
lbl
Definition
apply_bin_
oreg_ireg0
(
optR
:
option
oreg
)
(
r1
r2
:
ireg0
)
:
(
ireg0
*
ireg0
)
:=
match
optR
with
|
None
=>
(
r1
,
r2
)
|
Some
X0_L
=>
(
X0
,
r1
)
|
Some
X0_R
=>
(
r1
,
X0
)
end
.
Definition
apply_bin_r0_r0r0
(
optR0
:
option
bool
)
(
sem
:
ireg0
->
ireg0
->
instruction
)
(
r1
r2
:
ireg0
)
:=
match
optR0
with
|
None
=>
sem
r1
r2
|
Some
true
=>
sem
X0
r1
|
Some
false
=>
sem
r1
X0
end
.
Definition
get_oreg
(
optR
:
option
oreg
)
(
r
:
ireg0
)
:=
match
optR
with
|
Some
X0_L
|
Some
X0_R
=>
X0
|
_
=>
r
end
.
Definition
transl_cbranch
(
cond
:
condition
)
(
args
:
list
mreg
)
(
lbl
:
label
)
(
k
:
code
)
:=
match
cond
,
args
with
|
CEbeqw
optR
0
,
a1
::
a2
::
nil
=>
|
CEbeqw
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbeqw
r1
r2
lbl
::
k
)
|
CEbnew
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbeqw
r1
'
r2
'
lbl
::
k
)
|
CEbnew
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbnew
r1
r2
lbl
::
k
)
|
CEbequw
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbnew
r1
'
r2
'
lbl
::
k
)
|
CEbequw
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbeqw
r1
r2
lbl
::
k
)
|
CEbneuw
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbeqw
r1
'
r2
'
lbl
::
k
)
|
CEbneuw
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbnew
r1
r2
lbl
::
k
)
|
CEbltw
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbnew
r1
'
r2
'
lbl
::
k
)
|
CEbltw
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbltw
r1
r2
lbl
::
k
)
|
CEbltuw
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbltw
r1
'
r2
'
lbl
::
k
)
|
CEbltuw
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbltuw
r1
r2
lbl
::
k
)
|
CEbgew
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbltuw
r1
'
r2
'
lbl
::
k
)
|
CEbgew
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbgew
r1
r2
lbl
::
k
)
|
CEbgeuw
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbgew
r1
'
r2
'
lbl
::
k
)
|
CEbgeuw
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbgeuw
r1
r2
lbl
::
k
)
|
CEbeql
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbgeuw
r1
'
r2
'
lbl
::
k
)
|
CEbeql
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbeql
r1
r2
lbl
::
k
)
|
CEbnel
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbeql
r1
'
r2
'
lbl
::
k
)
|
CEbnel
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbnel
r1
r2
lbl
::
k
)
|
CEbequl
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbnel
r1
'
r2
'
lbl
::
k
)
|
CEbequl
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbeql
r1
r2
lbl
::
k
)
|
CEbneul
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbeql
r1
'
r2
'
lbl
::
k
)
|
CEbneul
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbnel
r1
r2
lbl
::
k
)
|
CEbltl
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbnel
r1
'
r2
'
lbl
::
k
)
|
CEbltl
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbltl
r1
r2
lbl
::
k
)
|
CEbltul
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbltl
r1
'
r2
'
lbl
::
k
)
|
CEbltul
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbltul
r1
r2
lbl
::
k
)
|
CEbgel
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbltul
r1
'
r2
'
lbl
::
k
)
|
CEbgel
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbgel
r1
r2
lbl
::
k
)
|
CEbgeul
optR0
,
a1
::
a2
::
nil
=>
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbgel
r1
'
r2
'
lbl
::
k
)
|
CEbgeul
optR
,
a1
::
a2
::
nil
=>
do
r1
<-
ireg_of
a1
;
do
r2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0lbl
optR0
Pbgeul
r1
r2
lbl
::
k
)
let
(
r1
'
,
r2
'
)
:=
apply_bin_oreg_ireg0
optR
r1
r2
in
OK
(
Pbgeul
r1
'
r2
'
lbl
::
k
)
|
_
,
_
=>
Error
(
msg
"Asmgen.transl_cond_branch"
)
end
.
...
...
@@ -222,22 +218,6 @@ Definition transl_op
|
FR
r
,
FR
a
=>
OK
(
Pfmv
r
a
::
k
)
|
_
,
_
=>
Error
(
msg
"Asmgen.Omove"
)
end
|
Ointconst
n
,
nil
=>
do
rd
<-
ireg_of
res
;
OK
(
loadimm32
rd
n
k
)
|
Olongconst
n
,
nil
=>
do
rd
<-
ireg_of
res
;
OK
(
loadimm64
rd
n
k
)
|
Ofloatconst
f
,
nil
=>
do
rd
<-
freg_of
res
;
OK
(
if
Float
.
eq_dec
f
Float
.
zero
then
Pfcvtdw
rd
X0
::
k
else
Ploadfi
rd
f
::
k
)
|
Osingleconst
f
,
nil
=>
do
rd
<-
freg_of
res
;
OK
(
if
Float32
.
eq_dec
f
Float32
.
zero
then
Pfcvtsw
rd
X0
::
k
else
Ploadsi
rd
f
::
k
)
|
Oaddrsymbol
s
ofs
,
nil
=>
do
rd
<-
ireg_of
res
;
OK
(
if
Archi
.
pic_code
tt
&&
negb
(
Ptrofs
.
eq
ofs
Ptrofs
.
zero
)
...
...
@@ -247,18 +227,9 @@ Definition transl_op
do
rd
<-
ireg_of
res
;
OK
(
addptrofs
rd
SP
n
k
)
|
Ocast8signed
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pslliw
rd
rs
(
Int
.
repr
24
)
::
Psraiw
rd
rd
(
Int
.
repr
24
)
::
k
)
|
Ocast16signed
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pslliw
rd
rs
(
Int
.
repr
16
)
::
Psraiw
rd
rd
(
Int
.
repr
16
)
::
k
)
|
Oadd
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Paddw
rd
rs1
rs2
::
k
)
|
Oaddimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
addimm32
rd
rs
n
k
)
|
Oneg
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Psubw
rd
X0
rs
::
k
)
...
...
@@ -289,21 +260,12 @@ Definition transl_op
|
Oand
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Pandw
rd
rs1
rs2
::
k
)
|
Oandimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
andimm32
rd
rs
n
k
)
|
Oor
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Porw
rd
rs1
rs2
::
k
)
|
Oorimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
orimm32
rd
rs
n
k
)
|
Oxor
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Pxorw
rd
rs1
rs2
::
k
)
|
Oxorimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
xorimm32
rd
rs
n
k
)
|
Oshl
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Psllw
rd
rs1
rs2
::
k
)
...
...
@@ -322,19 +284,6 @@ Definition transl_op
|
Oshruimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Psrliw
rd
rs
n
::
k
)
|
Oshrximm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
if
Int
.
eq
n
Int
.
zero
then
Pmv
rd
rs
::
k
else
if
Int
.
eq
n
Int
.
one
then
Psrliw
X31
rs
(
Int
.
repr
31
)
::
Paddw
X31
rs
X31
::
Psraiw
rd
X31
Int
.
one
::
k
else
Psraiw
X31
rs
(
Int
.
repr
31
)
::
Psrliw
X31
X31
(
Int
.
sub
Int
.
iwordsize
n
)
::
Paddw
X31
rs
X31
::
Psraiw
rd
X31
n
::
k
)
(
*
[
Omakelong
],
[
Ohighlong
]
should
not
occur
*
)
|
Olowlong
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
...
...
@@ -343,16 +292,9 @@ Definition transl_op
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
assertion
(
ireg_eq
rd
rs
);
OK
(
Pcvtw2l
rd
::
k
)
|
Ocast32unsigned
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
assertion
(
ireg_eq
rd
rs
);
OK
(
Pcvtw2l
rd
::
Psllil
rd
rd
(
Int
.
repr
32
)
::
Psrlil
rd
rd
(
Int
.
repr
32
)
::
k
)
|
Oaddl
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Paddl
rd
rs1
rs2
::
k
)
|
Oaddlimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
addimm64
rd
rs
n
k
)
|
Onegl
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Psubl
rd
X0
rs
::
k
)
...
...
@@ -383,21 +325,12 @@ Definition transl_op
|
Oandl
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Pandl
rd
rs1
rs2
::
k
)
|
Oandlimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
andimm64
rd
rs
n
k
)
|
Oorl
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Porl
rd
rs1
rs2
::
k
)
|
Oorlimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
orimm64
rd
rs
n
k
)
|
Oxorl
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Pxorl
rd
rs1
rs2
::
k
)
|
Oxorlimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
xorimm64
rd
rs
n
k
)
|
Oshll
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Pslll
rd
rs1
rs2
::
k
)
...
...
@@ -416,19 +349,6 @@ Definition transl_op
|
Oshrluimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Psrlil
rd
rs
n
::
k
)
|
Oshrxlimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
if
Int
.
eq
n
Int
.
zero
then
Pmv
rd
rs
::
k
else
if
Int
.
eq
n
Int
.
one
then
Psrlil
X31
rs
(
Int
.
repr
63
)
::
Paddl
X31
rs
X31
::
Psrail
rd
X31
Int
.
one
::
k
else
Psrail
X31
rs
(
Int
.
repr
63
)
::
Psrlil
X31
X31
(
Int
.
sub
Int64
.
iwordsize
'
n
)
::
Paddl
X31
rs
X31
::
Psrail
rd
X31
n
::
k
)
|
Onegf
,
a1
::
nil
=>
do
rd
<-
freg_of
res
;
do
rs
<-
freg_of
a1
;
OK
(
Pfnegd
rd
rs
::
k
)
...
...
@@ -523,36 +443,44 @@ Definition transl_op
|
Osingleoflongu
,
a1
::
nil
=>
do
rd
<-
freg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pfcvtslu
rd
rs
::
k
)
|
OEseqw
optR0
,
a1
::
a2
::
nil
=>
(
*
Instructions
expanded
in
RTL
*
)
|
OEseqw
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Pseqw
rd
)
rs1
rs2
::
k
)
|
OEsnew
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Pseqw
rd
rs1
'
rs2
'
::
k
)
|
OEsnew
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Psnew
rd
)
rs1
rs2
::
k
)
|
OEsequw
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Psnew
rd
rs1
'
rs2
'
::
k
)
|
OEsequw
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Pseqw
rd
)
rs1
rs2
::
k
)
|
OEsneuw
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Pseqw
rd
rs1
'
rs2
'
::
k
)
|
OEsneuw
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Psnew
rd
)
rs1
rs2
::
k
)
|
OEsltw
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Psnew
rd
rs1
'
rs2
'
::
k
)
|
OEsltw
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Psltw
rd
)
rs1
rs2
::
k
)
|
OEsltuw
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Psltw
rd
rs1
'
rs2
'
::
k
)
|
OEsltuw
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Psltuw
rd
)
rs1
rs2
::
k
)
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Psltuw
rd
rs1
'
rs2
'
::
k
)
|
OEsltiw
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
...
...
@@ -565,42 +493,62 @@ Definition transl_op
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pxoriw
rd
rs
n
::
k
)
|
OEluiw
n
_
,
a1
::
nil
=>
|
OEluiw
n
,
nil
=>
do
rd
<-
ireg_of
res
;
OK
(
Pluiw
rd
n
::
k
)
|
OEaddiwr0
n
_
,
a1
::
nil
=>
|
OEaddiw
optR
n
,
nil
=>
do
rd
<-
ireg_of
res
;
let
rs
:=
get_oreg
optR
X0
in
OK
(
Paddiw
rd
rs
n
::
k
)
|
OEaddiw
optR
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
OK
(
Paddiw
rd
X0
n
::
k
)
|
OEseql
optR0
,
a1
::
a2
::
nil
=>
do
rs
<-
ireg_of
a1
;
let
rs
'
:=
get_oreg
optR
rs
in
OK
(
Paddiw
rd
rs
'
n
::
k
)
|
OEandiw
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pandiw
rd
rs
n
::
k
)
|
OEoriw
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Poriw
rd
rs
n
::
k
)
|
OEseql
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Pseql
rd
)
rs1
rs2
::
k
)
|
OEsnel
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Pseql
rd
rs1
'
rs2
'
::
k
)
|
OEsnel
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Psnel
rd
)
rs1
rs2
::
k
)
|
OEsequl
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Psnel
rd
rs1
'
rs2
'
::
k
)
|
OEsequl
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Pseql
rd
)
rs1
rs2
::
k
)
|
OEsneul
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Pseql
rd
rs1
'
rs2
'
::
k
)
|
OEsneul
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Psnel
rd
)
rs1
rs2
::
k
)
|
OEsltl
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Psnel
rd
rs1
'
rs2
'
::
k
)
|
OEsltl
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Psltl
rd
)
rs1
rs2
::
k
)
|
OEsltul
optR0
,
a1
::
a2
::
nil
=>
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Psltl
rd
rs1
'
rs2
'
::
k
)
|
OEsltul
optR
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
apply_bin_r0_r0r0
optR0
(
Psltul
rd
)
rs1
rs2
::
k
)
let
(
rs1
'
,
rs2
'
)
:=
apply_bin_oreg_ireg0
optR
rs1
rs2
in
OK
(
Psltul
rd
rs1
'
rs2
'
::
k
)
|
OEsltil
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
...
...
@@ -613,12 +561,26 @@ Definition transl_op
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pxoril
rd
rs
n
::
k
)
|
OEluil
n
,
a1
::
nil
=>
|
OEluil
n
,
nil
=>
do
rd
<-
ireg_of
res
;
OK
(
Pluil
rd
n
::
k
)
|
OEaddilr0
n
,
a1
::
nil
=>
|
OEaddil
optR
n
,
nil
=>
do
rd
<-
ireg_of
res
;
let
rs
:=
get_oreg
optR
X0
in
OK
(
Paddil
rd
rs
n
::
k
)
|
OEaddil
optR
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
let
rs
'
:=
get_oreg
optR
rs
in
OK
(
Paddil
rd
rs
'
n
::
k
)
|
OEandil
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
OK
(
Paddil
rd
X0
n
::
k
)
do
rs
<-
ireg_of
a1
;
OK
(
Pandil
rd
rs
n
::
k
)
|
OEoril
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Poril
rd
rs
n
::
k
)
|
OEloadli
n
,
nil
=>
do
rd
<-
ireg_of
res
;
OK
(
Ploadli
rd
n
::
k
)
...
...
@@ -652,6 +614,13 @@ Definition transl_op
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
OK
(
Pfles
rd
r1
r2
::
k
)
|
OEmayundef
_
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
r2
<-
ireg_of
a2
;
if
ireg_eq
rd
r2
then
OK
(
Pnop
::
k
)
else
OK
(
Pmv
rd
r2
::
k
)
|
Obits_of_single
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
freg_of
a1
;
...
...
riscV/Asmgenproof.v
View file @
b3009fc0
...
...
@@ -115,14 +115,6 @@ Qed.
Section
TRANSL_LABEL
.
Remark
loadimm32_label
:
forall
r
n
k
,
tail_nolabel
k
(
loadimm32
r
n
k
).
Proof
.
intros
;
unfold
loadimm32
.
destruct
(
make_immed32
n
);
TailNoLabel
.
unfold
load_hilo32
.
destruct
(
Int
.
eq
lo
Int
.
zero
);
TailNoLabel
.
Qed
.
Hint
Resolve
loadimm32_label
:
labels
.
Remark
opimm32_label
:
forall
op
opimm
r1
r2
n
k
,
(
forall
r1
r2
r3
,
nolabel
(
op
r1
r2
r3
))
->
...
...
@@ -134,14 +126,6 @@ Proof.
Qed
.
Hint
Resolve
opimm32_label
:
labels
.