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
be4dcbd9
Commit
be4dcbd9
authored
Mar 02, 2021
by
Léo Gourdin
Browse files
Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work
parents
fd1a0395
a9763cd4
Changes
19
Hide whitespace changes
Inline
Side-by-side
backend/Selectionproof.v
View file @
be4dcbd9
...
...
@@ -783,6 +783,8 @@ Lemma sel_select_opt_correct:
Cminor
.
eval_expr
ge
sp
e
m
cond
vcond
->
Cminor
.
eval_expr
ge
sp
e
m
a1
v1
->
Cminor
.
eval_expr
ge
sp
e
m
a2
v2
->
Val
.
has_type
v1
ty
->
Val
.
has_type
v2
ty
->
Val
.
bool_of_val
vcond
b
->
env_lessdef
e
e
'
->
Mem
.
extends
m
m
'
->
exists
v
'
,
eval_expr
tge
sp
e
'
m
'
le
a
v
'
/
\
Val
.
lessdef
(
Val
.
select
(
Some
b
)
v1
v2
ty
)
v
'
.
...
...
@@ -792,7 +794,7 @@ Proof.
exploit
sel_expr_correct
.
eexact
H0
.
eauto
.
eauto
.
intros
(
vcond
'
&
EVC
&
LDC
).
exploit
sel_expr_correct
.
eexact
H1
.
eauto
.
eauto
.
intros
(
v1
'
&
EV1
&
LD1
).
exploit
sel_expr_correct
.
eexact
H2
.
eauto
.
eauto
.
intros
(
v2
'
&
EV2
&
LD2
).
assert
(
Val
.
bool_of_val
vcond
'
b
)
by
(
inv
H
3
;
inv
LDC
;
constructor
).
assert
(
Val
.
bool_of_val
vcond
'
b
)
by
(
inv
H
5
;
inv
LDC
;
constructor
).
exploit
eval_condition_of_expr
.
eexact
EVC
.
eauto
.
rewrite
C
.
intros
(
vargs
'
&
EVARGS
&
EVCOND
).
exploit
eval_select
;
eauto
.
intros
(
v
'
&
X
&
Y
).
exists
v
'
;
split
;
eauto
.
...
...
common/Values.v
View file @
be4dcbd9
...
...
@@ -89,6 +89,27 @@ Definition has_type (v: val) (t: typ) : Prop :=
|
_
,
_
=>
False
end
.
Definition
has_type_b
(
v
:
val
)
(
t
:
typ
)
:=
match
v
,
t
with
|
Vundef
,
_
=>
true
|
Vint
_
,
Tint
=>
true
|
Vlong
_
,
Tlong
=>
true
|
Vfloat
_
,
Tfloat
=>
true
|
Vsingle
_
,
Tsingle
=>
true
|
Vptr
_
_
,
Tint
=>
negb
Archi
.
ptr64
|
Vptr
_
_
,
Tlong
=>
Archi
.
ptr64
|
(
Vint
_
|
Vsingle
_
),
Tany32
=>
true
|
Vptr
_
_
,
Tany32
=>
negb
Archi
.
ptr64
|
_
,
Tany64
=>
true
|
_
,
_
=>
false
end
.
Lemma
has_type_b_correct
:
forall
v
t
,
has_type_b
v
t
=
true
<->
has_type
v
t
.
Proof
.
destruct
v
;
destruct
t
;
cbn
;
destruct
Archi
.
ptr64
;
cbn
;
split
;
intros
;
auto
;
discriminate
.
Qed
.
Fixpoint
has_type_list
(
vl
:
list
val
)
(
tl
:
list
typ
)
{
struct
vl
}
:
Prop
:=
match
vl
,
tl
with
|
nil
,
nil
=>
True
...
...
configure
View file @
be4dcbd9
...
...
@@ -842,6 +842,13 @@ BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
EOF
fi
if
[
"
$arch
"
=
"riscV"
]
;
then
cat
>>
Makefile.config
<<
EOF
EXTRA_EXTRACTION=Asm.ireg_eq Asm.ireg0_eq
BACKENDLIB=Asmgenproof0.v Asmgenproof1.v ExtValues.v
EOF
fi
#
# Generate Merlin and CoqProject files to simplify development
#
...
...
riscV/Asm.v
View file @
be4dcbd9
...
...
@@ -30,6 +30,7 @@ Require Import Smallstep.
Require
Import
Locations
.
Require
Stacklayout
.
Require
Import
Conventions
.
Require
ExtValues
.
(
**
*
Abstract
syntax
*
)
...
...
@@ -62,10 +63,10 @@ Inductive freg: Type :=
|
F24
:
freg
|
F25
:
freg
|
F26
:
freg
|
F27
:
freg
|
F28
:
freg
|
F29
:
freg
|
F30
:
freg
|
F31
:
freg
.
Lemma
ireg_eq
:
forall
(
x
y
:
ireg
),
{
x
=
y
}
+
{
x
<>
y
}
.
Definition
ireg_eq
:
forall
(
x
y
:
ireg
),
{
x
=
y
}
+
{
x
<>
y
}
.
Proof
.
decide
equality
.
Defined
.
Lemma
ireg0_eq
:
forall
(
x
y
:
ireg0
),
{
x
=
y
}
+
{
x
<>
y
}
.
Definition
ireg0_eq
:
forall
(
x
y
:
ireg0
),
{
x
=
y
}
+
{
x
<>
y
}
.
Proof
.
decide
equality
.
apply
ireg_eq
.
Defined
.
Lemma
freg_eq
:
forall
(
x
y
:
freg
),
{
x
=
y
}
+
{
x
<>
y
}
.
...
...
@@ -255,8 +256,10 @@ Inductive instruction : Type :=
(
*
floating
point
register
move
*
)
|
Pfmv
(
rd
:
freg
)
(
rs
:
freg
)
(
**
r
move
*
)
|
Pfmvxs
(
rd
:
ireg
)
(
rs
:
freg
)
(
**
r
move
FP
single
to
integer
register
*
)
|
Pfmvxd
(
rd
:
ireg
)
(
rs
:
freg
)
(
**
r
move
FP
double
to
integer
register
*
)
|
Pfmvxs
(
rd
:
ireg
)
(
rs
:
freg
)
(
**
r
bitwise
move
FP
single
to
integer
register
*
)
|
Pfmvxd
(
rd
:
ireg
)
(
rs
:
freg
)
(
**
r
bitwise
move
FP
double
to
integer
register
*
)
|
Pfmvsx
(
rd
:
freg
)
(
rs
:
ireg
)
(
**
r
bitwise
move
integer
register
to
FP
single
*
)
|
Pfmvdx
(
rd
:
freg
)
(
rs
:
ireg
)
(
**
r
bitwise
move
integer
register
to
FP
double
*
)
(
*
32
-
bit
(
single
-
precision
)
floating
point
*
)
|
Pfls
(
rd
:
freg
)
(
ra
:
ireg
)
(
ofs
:
offset
)
(
**
r
load
float
*
)
...
...
@@ -345,6 +348,7 @@ Inductive instruction : Type :=
|
Pbtbl
(
r
:
ireg
)
(
tbl
:
list
label
)
(
**
r
N
-
way
branch
through
a
jump
table
*
)
|
Pbuiltin
:
external_function
->
list
(
builtin_arg
preg
)
->
builtin_res
preg
->
instruction
(
**
r
built
-
in
function
(
pseudo
)
*
)
|
Pselectl
(
rd
:
ireg
)
(
rb
:
ireg0
)
(
rt
:
ireg0
)
(
rf
:
ireg0
)
|
Pnop
:
instruction
.
(
**
r
nop
instruction
*
)
...
...
@@ -918,6 +922,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
Next
(
nextinstr
(
rs
#
d
<-
(
Val
.
floatofsingle
rs
#
s
)))
m
|
Pfcvtsd
d
s
=>
Next
(
nextinstr
(
rs
#
d
<-
(
Val
.
singleoffloat
rs
#
s
)))
m
|
Pfmvxs
d
s
=>
Next
(
nextinstr
(
rs
#
d
<-
(
ExtValues
.
bits_of_single
rs
#
s
)))
m
|
Pfmvxd
d
s
=>
Next
(
nextinstr
(
rs
#
d
<-
(
ExtValues
.
bits_of_float
rs
#
s
)))
m
|
Pfmvsx
d
s
=>
Next
(
nextinstr
(
rs
#
d
<-
(
ExtValues
.
single_of_bits
rs
#
s
)))
m
|
Pfmvdx
d
s
=>
Next
(
nextinstr
(
rs
#
d
<-
(
ExtValues
.
float_of_bits
rs
#
s
)))
m
(
**
Pseudo
-
instructions
*
)
|
Pallocframe
sz
pos
=>
...
...
@@ -940,6 +955,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
|
_
=>
Stuck
end
end
|
Pselectl
rd
rb
rt
rf
=>
Next
(
nextinstr
(
rs
#
rd
<-
(
ExtValues
.
select01_long
(
rs
###
rb
)
(
rs
###
rt
)
(
rs
###
rf
)))
#
X31
<-
Vundef
)
m
|
Plabel
lbl
=>
Next
(
nextinstr
rs
)
m
|
Ploadsymbol
rd
s
ofs
=>
...
...
@@ -968,9 +987,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
so
we
do
not
model
them
.
*
)
|
Pfence
|
Pfmvxs
_
_
|
Pfmvxd
_
_
|
Pfmins
_
_
_
|
Pfmaxs
_
_
_
|
Pfsqrts
_
_
...
...
riscV/Asmexpand.ml
View file @
be4dcbd9
...
...
@@ -582,9 +582,49 @@ let expand_builtin_inline name args res =
raise
(
Error
(
"unrecognized builtin "
^
name
))
(* Expansion of instructions *)
let
expand_instruction
instr
=
match
instr
with
|
Pselectl
(
rd
,
rb
,
rt
,
rf
)
->
if
not
Archi
.
ptr64
then
failwith
"Pselectl not available on RV32, only on RV64"
else
if
ireg0_eq
rt
rf
then
begin
if
ireg0_eq
(
X
rd
)
rt
then
begin
end
else
begin
emit
(
Paddl
(
rd
,
X0
,
rt
))
end
end
else
if
(
ireg0_eq
(
X
rd
)
rt
)
then
begin
emit
(
Psubl
(
X31
,
X0
,
rb
));
emit
(
Pandl
(
X31
,
X
X31
,
rt
));
emit
(
Paddil
(
rd
,
rb
,
Int64
.
mone
));
emit
(
Pandl
(
rd
,
X
rd
,
rf
));
emit
(
Porl
(
rd
,
X
rd
,
X
X31
))
end
else
if
(
ireg0_eq
(
X
rd
)
rf
)
then
begin
emit
(
Paddil
(
X31
,
rb
,
Int64
.
mone
));
emit
(
Pandl
(
X31
,
X
X31
,
rf
));
emit
(
Psubl
(
rd
,
X0
,
rb
));
emit
(
Pandl
(
rd
,
X
rd
,
rt
));
emit
(
Porl
(
rd
,
X
rd
,
X
X31
))
end
else
begin
emit
(
Psubl
(
X31
,
X0
,
rb
));
emit
(
Paddil
(
rd
,
rb
,
Int64
.
mone
));
emit
(
Pandl
(
X31
,
X
X31
,
rt
));
emit
(
Pandl
(
rd
,
X
rd
,
rf
));
emit
(
Porl
(
rd
,
X
rd
,
X
X31
))
end
|
Pallocframe
(
sz
,
ofs
)
->
let
sg
=
get_current_function_sig
()
in
emit
(
Pmv
(
X30
,
X2
));
...
...
riscV/Asmgen.v
View file @
be4dcbd9
...
...
@@ -899,6 +899,31 @@ Definition transl_op
do
r1
<-
freg_of
f1
;
do
r2
<-
freg_of
f2
;
OK
(
Pfles
rd
r1
r2
::
k
)
|
Obits_of_single
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
freg_of
a1
;
OK
(
Pfmvxs
rd
rs
::
k
)
|
Obits_of_float
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
freg_of
a1
;
OK
(
Pfmvxd
rd
rs
::
k
)
|
Osingle_of_bits
,
a1
::
nil
=>
do
rd
<-
freg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
Pfmvsx
rd
rs
::
k
)
|
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/Asmgenproof1.v
View file @
be4dcbd9
...
...
@@ -1268,6 +1268,54 @@ Opaque Int.eq.
split
;
intros
;
Simpl
.
all:
destruct
(
rs
x0
);
auto
.
all:
destruct
(
rs
x1
);
auto
.
exists
rs
'
;
split
;
eauto
.
rewrite
B
;
auto
with
asmgen
.
-
(
*
shrxlimm
*
)
destruct
(
Val
.
shrxl
(
rs
x0
)
(
Vint
n
))
eqn
:
TOTAL
.
{
exploit
Val
.
shrxl_shrl_3
;
eauto
.
intros
E
;
subst
v
.
destruct
(
Int
.
eq
n
Int
.
zero
).
+
econstructor
;
split
.
apply
exec_straight_one
.
simpl
;
eauto
.
auto
.
split
;
intros
;
Simpl
.
+
destruct
(
Int
.
eq
n
Int
.
one
).
*
econstructor
;
split
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
apply
exec_straight_one
.
simpl
;
reflexivity
.
auto
.
split
;
intros
;
Simpl
.
*
change
(
Int
.
repr
64
)
with
Int64
.
iwordsize
'
.
set
(
n
'
:=
Int
.
sub
Int64
.
iwordsize
'
n
).
econstructor
;
split
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
apply
exec_straight_one
.
simpl
;
reflexivity
.
auto
.
split
;
intros
;
Simpl
.
}
destruct
(
Int
.
eq
n
Int
.
zero
).
+
econstructor
;
split
.
apply
exec_straight_one
.
simpl
;
eauto
.
auto
.
split
;
intros
;
Simpl
.
+
destruct
(
Int
.
eq
n
Int
.
one
).
*
econstructor
;
split
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
apply
exec_straight_one
.
simpl
;
reflexivity
.
auto
.
split
;
intros
;
Simpl
.
*
change
(
Int
.
repr
64
)
with
Int64
.
iwordsize
'
.
set
(
n
'
:=
Int
.
sub
Int64
.
iwordsize
'
n
).
econstructor
;
split
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
eapply
exec_straight_step
.
simpl
;
reflexivity
.
auto
.
apply
exec_straight_one
.
simpl
;
reflexivity
.
auto
.
split
;
intros
;
Simpl
.
-
(
*
cond
*
)
exploit
transl_cond_op_correct
;
eauto
.
intros
(
rs
'
&
A
&
B
&
C
).
exists
rs
'
;
split
.
eexact
A
.
eauto
with
asmgen
.
-
(
*
select
*
)
econstructor
;
split
.
apply
exec_straight_one
.
simpl
;
eauto
.
auto
.
split
;
intros
;
Simpl
.
apply
Val
.
lessdef_normalize
.
Qed
.
(
**
Memory
accesses
*
)
...
...
riscV/Builtins1.v
View file @
be4dcbd9
...
...
@@ -18,16 +18,35 @@
Require
Import
String
Coqlib
.
Require
Import
AST
Integers
Floats
Values
.
Require
Import
Builtins0
.
Require
ExtValues
.
Inductive
platform_builtin
:
Type
:=
.
Inductive
platform_builtin
:
Type
:=
|
BI_bits_of_float
|
BI_bits_of_double
|
BI_float_of_bits
|
BI_double_of_bits
.
Local
Open
Scope
string_scope
.
Definition
platform_builtin_table
:
list
(
string
*
platform_builtin
)
:=
nil
.
(
"__builtin_bits_of_float"
,
BI_bits_of_float
)
::
(
"__builtin_bits_of_double"
,
BI_bits_of_double
)
::
(
"__builtin_float_of_bits"
,
BI_float_of_bits
)
::
(
"__builtin_double_of_bits"
,
BI_double_of_bits
)
::
nil
.
Definition
platform_builtin_sig
(
b
:
platform_builtin
)
:
signature
:=
match
b
with
end
.
match
b
with
|
BI_bits_of_float
=>
mksignature
(
Tsingle
::
nil
)
Tint
cc_default
|
BI_bits_of_double
=>
mksignature
(
Tfloat
::
nil
)
Tlong
cc_default
|
BI_float_of_bits
=>
mksignature
(
Tint
::
nil
)
Tsingle
cc_default
|
BI_double_of_bits
=>
mksignature
(
Tlong
::
nil
)
Tfloat
cc_default
end
.
Definition
platform_builtin_sem
(
b
:
platform_builtin
)
:
builtin_sem
(
sig_res
(
platform_builtin_sig
b
))
:=
match
b
with
end
.
match
b
with
|
BI_bits_of_float
=>
mkbuiltin_n1t
Tsingle
Tint
Float32
.
to_bits
|
BI_bits_of_double
=>
mkbuiltin_n1t
Tfloat
Tlong
Float
.
to_bits
|
BI_float_of_bits
=>
mkbuiltin_n1t
Tint
Tsingle
Float32
.
of_bits
|
BI_double_of_bits
=>
mkbuiltin_n1t
Tlong
Tfloat
Float
.
of_bits
end
.
riscV/CBuiltins.ml
View file @
be4dcbd9
...
...
@@ -46,6 +46,14 @@ let builtins = {
(
TFloat
(
FDouble
,
[]
)
,
[
TFloat
(
FDouble
,
[]
);
TFloat
(
FDouble
,
[]
)]
,
false
);
"__builtin_fmin"
,
(
TFloat
(
FDouble
,
[]
)
,
[
TFloat
(
FDouble
,
[]
);
TFloat
(
FDouble
,
[]
)]
,
false
);
"__builtin_bits_of_double"
,
(
TInt
(
IULong
,
[]
)
,
[
TFloat
(
FDouble
,
[]
)]
,
false
);
"__builtin_bits_of_float"
,
(
TInt
(
IUInt
,
[]
)
,
[
TFloat
(
FFloat
,
[]
)]
,
false
);
"__builtin_double_of_bits"
,
(
TFloat
(
FDouble
,
[]
)
,
[
TInt
(
IULong
,
[]
)]
,
false
);
"__builtin_float_of_bits"
,
(
TFloat
(
FFloat
,
[]
)
,
[
TInt
(
IUInt
,
[]
)]
,
false
);
]
}
...
...
riscV/ExtValues.v
0 → 100644
View file @
be4dcbd9
Require
Import
Coqlib
.
Require
Import
Integers
.
Require
Import
Values
.
Require
Import
Floats
.
Require
Import
Memory
.
Require
Import
Lia
.
Definition
bits_of_float
x
:=
match
x
with
|
Vfloat
f
=>
Vlong
(
Float
.
to_bits
f
)
|
_
=>
Vundef
end
.
Definition
bits_of_single
x
:=
match
x
with
|
Vsingle
f
=>
Vint
(
Float32
.
to_bits
f
)
|
_
=>
Vundef
end
.
Definition
float_of_bits
x
:=
match
x
with
|
Vlong
f
=>
Vfloat
(
Float
.
of_bits
f
)
|
_
=>
Vundef
end
.
Definition
single_of_bits
x
:=
match
x
with
|
Vint
f
=>
Vsingle
(
Float32
.
of_bits
f
)
|
_
=>
Vundef
end
.
Definition
bitwise_select_long
b
vtrue
vfalse
:=
Int64
.
or
(
Int64
.
and
(
Int64
.
neg
b
)
vtrue
)
(
Int64
.
and
(
Int64
.
sub
b
Int64
.
one
)
vfalse
).
Lemma
bitwise_select_long_true
:
forall
vtrue
vfalse
,
bitwise_select_long
Int64
.
one
vtrue
vfalse
=
vtrue
.
Proof
.
intros
.
unfold
bitwise_select_long
.
cbn
.
change
(
Int64
.
neg
Int64
.
one
)
with
Int64
.
mone
.
rewrite
Int64
.
and_commut
.
rewrite
Int64
.
and_mone
.
rewrite
Int64
.
sub_idem
.
rewrite
Int64
.
and_commut
.
rewrite
Int64
.
and_zero
.
apply
Int64
.
or_zero
.
Qed
.
Lemma
bitwise_select_long_false
:
forall
vtrue
vfalse
,
bitwise_select_long
Int64
.
zero
vtrue
vfalse
=
vfalse
.
Proof
.
intros
.
unfold
bitwise_select_long
.
cbn
.
rewrite
Int64
.
neg_zero
.
rewrite
Int64
.
and_commut
.
rewrite
Int64
.
and_zero
.
rewrite
Int64
.
sub_zero_r
.
change
(
Int64
.
neg
Int64
.
one
)
with
Int64
.
mone
.
rewrite
Int64
.
and_commut
.
rewrite
Int64
.
and_mone
.
rewrite
Int64
.
or_commut
.
apply
Int64
.
or_zero
.
Qed
.
Definition
select01_long
(
vb
:
val
)
(
vtrue
:
val
)
(
vfalse
:
val
)
:
val
:=
match
vb
with
|
(
Vint
b
)
=>
if
Int
.
eq
b
Int
.
one
then
vtrue
else
if
Int
.
eq
b
Int
.
zero
then
vfalse
else
Vundef
|
_
=>
Vundef
end
.
Lemma
normalize_select01
:
forall
x
y
z
,
Val
.
normalize
(
select01_long
x
y
z
)
AST
.
Tlong
=
select01_long
x
(
Val
.
normalize
y
AST
.
Tlong
)
(
Val
.
normalize
z
AST
.
Tlong
).
Proof
.
unfold
select01_long
.
intros
.
destruct
x
;
cbn
;
trivial
.
destruct
(
Int
.
eq
i
Int
.
one
);
trivial
.
destruct
(
Int
.
eq
i
Int
.
zero
);
trivial
.
Qed
.
Lemma
select01_long_true
:
forall
vt
vf
,
select01_long
Vtrue
vt
vf
=
vt
.
Proof
.
intros
.
unfold
select01_long
.
cbn
.
rewrite
Int
.
eq_true
.
reflexivity
.
Qed
.
Lemma
select01_long_false
:
forall
vt
vf
,
select01_long
Vfalse
vt
vf
=
vf
.
Proof
.
intros
.
unfold
select01_long
.
cbn
.
rewrite
Int
.
eq_true
.
rewrite
Int
.
eq_false
.
reflexivity
.
cbv
.
discriminate
.
Qed
.
Lemma
float_bits_normalize
:
forall
v1
,
ExtValues
.
float_of_bits
(
Val
.
normalize
(
ExtValues
.
bits_of_float
v1
)
AST
.
Tlong
)
=
Val
.
normalize
v1
AST
.
Tfloat
.
Proof
.
destruct
v1
;
cbn
;
trivial
.
f_equal
.
apply
Float
.
of_to_bits
.
Qed
.
Lemma
single_bits_normalize
:
forall
v1
,
ExtValues
.
single_of_bits
(
Val
.
normalize
(
ExtValues
.
bits_of_single
v1
)
AST
.
Tint
)
=
Val
.
normalize
v1
AST
.
Tsingle
.
Proof
.
destruct
v1
;
cbn
;
trivial
.
f_equal
.
apply
Float32
.
of_to_bits
.
Qed
.
riscV/NeedOp.v
View file @
be4dcbd9
...
...
@@ -116,6 +116,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
|
OEfeqs
=>
op2
(
default
nv
)
|
OEflts
=>
op2
(
default
nv
)
|
OEfles
=>
op2
(
default
nv
)
|
Obits_of_single
=>
op1
(
default
nv
)
|
Obits_of_float
=>
op1
(
default
nv
)
|
Osingle_of_bits
=>
op1
(
default
nv
)
|
Ofloat_of_bits
=>
op1
(
default
nv
)
|
Oselectl
=>
All
::
nv
::
nv
::
nil
end
.
Definition
operation_is_redundant
(
op
:
operation
)
(
nv
:
nval
)
:
bool
:=
...
...
@@ -184,6 +189,16 @@ Proof.
-
apply
shrimm_sound
;
auto
.
-
apply
shruimm_sound
;
auto
.
-
apply
xor_sound
;
auto
with
na
.
-
(
*
selectl
*
)
unfold
ExtValues
.
select01_long
.
destruct
v0
;
auto
with
na
.
assert
(
Val
.
lessdef
(
Vint
i
)
v4
)
as
LESSDEF
by
auto
with
na
.
inv
LESSDEF
.
destruct
(
Int
.
eq
i
Int
.
one
).
{
apply
normalize_sound
;
auto
.
}
destruct
(
Int
.
eq
i
Int
.
zero
).
{
apply
normalize_sound
;
auto
.
}
cbn
.
auto
with
na
.
Qed
.
Lemma
operation_is_redundant_sound
:
...
...
riscV/Op.v
View file @
be4dcbd9
...
...
@@ -32,6 +32,7 @@
Require
Import
BoolEqual
Coqlib
.
Require
Import
AST
Integers
Floats
.
Require
Import
Values
Memory
Globalenvs
Events
.
Require
ExtValues
.
Set
Implicit
Arguments
.
...
...
@@ -200,6 +201,12 @@ Inductive operation : Type :=
|
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
.
*
)
|
Obits_of_single
|
Obits_of_float
|
Osingle_of_bits
|
Ofloat_of_bits
|
Oselectl
.
(
**
Addressing
modes
.
[
r1
],
[
r2
],
etc
,
are
the
arguments
to
the
addressing
.
*
)
...
...
@@ -411,6 +418,10 @@ Definition eval_operation
|
Olonguofsingle
,
v1
::
nil
=>
Some
(
Val
.
maketotal
(
Val
.
longuofsingle
v1
))
|
Osingleoflong
,
v1
::
nil
=>
Some
(
Val
.
maketotal
(
Val
.
singleoflong
v1
))
|
Osingleoflongu
,
v1
::
nil
=>
Some
(
Val
.
maketotal
(
Val
.
singleoflongu
v1
))
|
Obits_of_single
,
v1
::
nil
=>
Some
(
ExtValues
.
bits_of_single
v1
)
|
Obits_of_float
,
v1
::
nil
=>
Some
(
ExtValues
.
bits_of_float
v1
)
|
Osingle_of_bits
,
v1
::
nil
=>
Some
(
ExtValues
.
single_of_bits
v1
)
|
Ofloat_of_bits
,
v1
::
nil
=>
Some
(
ExtValues
.
float_of_bits
v1
)
|
Ocmp
c
,
_
=>
Some
(
Val
.
of_optbool
(
eval_condition
c
vl
m
))
(
*
Expansed
conditions
*
)
|
OEseqw
optR0
,
v1
::
v2
::
nil
=>
Some
(
apply_bin_r0
optR0
(
Val
.
cmp
Ceq
)
v1
v2
zero32
)
...
...
@@ -442,6 +453,7 @@ Definition eval_operation
|
OEfeqs
,
v1
::
v2
::
nil
=>
Some
(
Val
.
cmpfs
Ceq
v1
v2
)
|
OEflts
,
v1
::
v2
::
nil
=>
Some
(
Val
.
cmpfs
Clt
v1
v2
)
|
OEfles
,
v1
::
v2
::
nil
=>
Some
(
Val
.
cmpfs
Cle
v1
v2
)
|
Oselectl
,
vb
::
vt
::
vf
::
nil
=>
Some
(
Val
.
normalize
(
ExtValues
.
select01_long
vb
vt
vf
)
Tlong
)
|
_
,
_
=>
None
end
.
...
...
@@ -472,9 +484,9 @@ Qed.
Ltac
FuncInv
:=
match
goal
with
|
H
:
(
match
?
x
with
nil
=>
_
|
_
::
_
=>
_
end
=
Some
_
)
|-
_
=>
destruct
x
;
simpl
in
H
;
FuncInv
destruct
x
;
cbn
in
H
;
FuncInv
|
H
:
(
match
?
v
with
Vundef
=>
_
|
Vint
_
=>
_
|
Vfloat
_
=>
_
|
Vptr
_
_
=>
_
end
=
Some
_
)
|-
_
=>
destruct
v
;
simpl
in
H
;
FuncInv
destruct
v
;
cbn
in
H
;
FuncInv
|
H
:
(
if
Archi
.
ptr64
then
_
else
_
)
=
Some
_
|-
_
=>
destruct
Archi
.
ptr64
eqn
:?
;
FuncInv
|
H
:
(
Some
_
=
Some
_
)
|-
_
=>
...
...
@@ -643,6 +655,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
|
OEfeqs
=>
(
Tsingle
::
Tsingle
::
nil
,
Tint
)
|
OEflts
=>
(
Tsingle
::
Tsingle
::
nil
,
Tint
)
|
OEfles
=>
(
Tsingle
::
Tsingle
::
nil
,
Tint
)
|
Obits_of_single
=>
(
Tsingle
::
nil
,
Tint
)
|
Obits_of_float
=>
(
Tfloat
::
nil
,
Tlong
)
|
Osingle_of_bits
=>
(
Tint
::
nil
,
Tsingle
)
|
Ofloat_of_bits
=>
(
Tlong
::
nil
,
Tfloat
)
|
Oselectl
=>
(
Tint
::
Tlong
::
Tlong
::
nil
,
Tlong
)
end
.
Definition
type_of_addressing
(
addr
:
addressing
)
:
list
typ
:=
...
...
@@ -929,6 +946,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
(
*
OEfles
*
)
-
destruct
v0
;
destruct
v1
;
cbn
;
auto
.
destruct
Float32
.
cmp
;
cbn
;
auto
.
(
*
Bits_of_single
,
float
*
)
-
destruct
v0
;
cbn
;
trivial
.
-
destruct
v0
;
cbn
;
trivial
.
(
*
single
,
float
of
bits
*
)
-
destruct
v0
;
cbn
;
trivial
.
-
destruct
v0
;
cbn
;
trivial
.
(
*
selectl
*
)
-
destruct
v0
;
cbn
;
trivial
.
destruct
Int
.
eq
;
cbn
.
apply
Val
.
normalize_type
.
destruct
Int
.
eq
;
cbn
;
trivial
.
apply
Val
.
normalize_type
.
Qed
.
(
*
This
should
not
be
simplified
to
"false"
because
it
breaks
proofs
elsewhere
.
*
)
...
...
@@ -1767,6 +1796,17 @@ Proof.
(
*
OEfles
*
)
-
inv
H4
;
inv
H2
;
cbn
;
simpl
;
auto
.
destruct
Float32
.
cmp
;
unfold
Vtrue
,
Vfalse
;
cbn
;
auto
.
(
*
Bits_of_single
,
double
*
)
-
inv
H4
;
simpl
;
auto
.
-
inv
H4
;
simpl
;
auto
.
(
*
single
,
double
of
bits
*
)
-
inv
H4
;
simpl
;
auto
.
-
inv
H4
;
simpl
;
auto
.
(
*
selectl
*
)
-
inv
H4
;
trivial
.
cbn
.
destruct
(
Int
.
eq
i
Int
.
one
).
+
auto
using
Val
.
normalize_inject
.
+
destruct
(
Int
.
eq
i
Int
.
zero
);
cbn
;
auto
using
Val
.
normalize_inject
.
Qed
.
Lemma
eval_addressing_inj
:
...
...
riscV/PrintOp.ml
View file @
be4dcbd9
...
...
@@ -222,6 +222,11 @@ let print_operation reg pp = function
|
OEfeqs
,
[
r1
;
r2
]
->
fprintf
pp
"OEfeqs(%a,%s,%a)"
reg
r1
(
comparison_name
Ceq
)
reg
r2
|
OEflts
,
[
r1
;
r2
]
->
fprintf
pp
"OEflts(%a,%s,%a)"
reg
r1
(
comparison_name
Clt
)
reg
r2
|
OEfles
,
[
r1
;
r2
]
->
fprintf
pp
"OEfles(%a,%s,%a)"
reg
r1
(
comparison_name
Cle
)
reg
r2
|
Obits_of_single
,
[
r1
]
->
fprintf
pp
"bits_of_single(%a)"
reg
r1
|
Obits_of_float
,
[
r1
]
->
fprintf