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
9862e891
Commit
9862e891
authored
Apr 10, 2018
by
Cyril SIX
Browse files
MPPA - Onegl + Pnegl
parent
5541fb2f
Changes
5
Hide whitespace changes
Inline
Side-by-side
mppa_k1c/Asm.v
View file @
9862e891
...
...
@@ -202,6 +202,7 @@ Inductive instruction : Type :=
(
**
64
-
bit
integer
register
-
register
instructions
*
)
|
Paddl
(
rd
:
ireg
)
(
rs1
rs2
:
ireg
)
(
**
r
integer
addition
*
)
|
Pnegl
(
rd
:
ireg
)
(
rs
:
ireg
)
(
**
r
negate
long
*
)
(
*
Unconditional
jumps
.
Links
are
always
to
X1
/
RA
.
*
)
|
Pj_l
(
l
:
label
)
(
**
r
jump
to
label
*
)
...
...
@@ -727,6 +728,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
(
**
64
-
bit
integer
register
-
register
instructions
*
)
|
Paddl
d
s1
s2
=>
Next
(
nextinstr
(
rs
#
d
<-
(
Val
.
addl
rs
###
s1
rs
###
s2
)))
m
|
Pnegl
d
s
=>
Next
(
nextinstr
(
rs
#
d
<-
(
Val
.
negl
rs
###
s
)))
m
(
**
Unconditional
jumps
.
*
)
|
Pj_l
l
=>
...
...
mppa_k1c/Asmgen.v
View file @
9862e891
...
...
@@ -345,10 +345,10 @@ Definition transl_op
|
Oaddlimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
addimm64
rd
rs
n
k
)
(
*
|
Onegl
,
a1
::
nil
=>
|
Onegl
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
P
sub
l
rd
GPR0
rs
::
k
)
|
Osubl
,
a1
::
a2
::
nil
=>
OK
(
P
neg
l
rd
rs
::
k
)
(
*
|
Osubl
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Psubl
rd
rs1
rs2
::
k
)
|
Omull
,
a1
::
a2
::
nil
=>
...
...
mppa_k1c/TargetPrinter.ml
View file @
9862e891
...
...
@@ -217,6 +217,8 @@ module Target : TARGET =
fprintf
oc
" make %a, %a
\n
;;
\n
"
ireg
rd
coqint64
imm
|
Paddl
(
rd
,
rs1
,
rs2
)
->
assert
Archi
.
ptr64
;
fprintf
oc
" addd %a = %a, %a
\n
;;
\n
"
ireg
rd
ireg
rs1
ireg
rs2
|
Pnegl
(
rd
,
rs
)
->
assert
Archi
.
ptr64
;
fprintf
oc
" negd %a = %a
\n
;;
\n
"
ireg
rd
ireg
rs
|
Pcompw
(
it
,
rd
,
rs1
,
rs2
)
->
fprintf
oc
" compw.%a %a = %a, %a
\n
;;
\n
"
icond
it
ireg
rd
ireg
rs1
ireg
rs2
...
...
test/mppa/Makefile
View file @
9862e891
DIR
=
general
TESTNAMES
=
simple call branch
for
forvar forvarl branchz branchzu
CCOMP
=
../../ccomp
TESTS
=
$(
addprefix
$(DIR)
/,
$(TESTNAMES)
)
ELF
=
$(
addsuffix
.bin,
$(TESTS)
)
TOK
=
$(
addsuffix
.tok,
$(TESTS)
)
...
...
@@ -15,10 +16,10 @@ $(DIR)/%.bin: $(DIR)/%.s
k1-gcc
$<
-o
$@
.SECONDARY
:
$(DIR)/%.s
:
$(DIR)/%.c
$(DIR)/%.s
:
$(DIR)/%.c
$(CCOMP)
ccomp
$(DEBUG)
-O0
-v
-S
$<
-o
$@
$(DIR)/%.tok
:
$(DIR)/%.bin
FORCE
$(DIR)/%.tok
:
$(DIR)/%.bin
@
bash check.sh
$<
$@
.PHONY
:
FORCE
...
...
test/mppa/check.sh
View file @
9862e891
...
...
@@ -9,11 +9,6 @@ if [ ! -f $elffile ]; then
shift
;
continue
fi
if
[
-f
$token
]
;
then
echo
"ALREADY PASSED:
$elffile
"
exit
fi
dir
=
"
$(
dirname
$elffile
)
"
elf
=
"
$(
basename
$elffile
)
"
exp
=
"
$dir
/output/
$elf
.exp"
...
...
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