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
e6fd7a6a
Commit
e6fd7a6a
authored
Apr 10, 2018
by
Cyril SIX
Browse files
MPPA - Oneg + Pnegw
parent
9862e891
Changes
3
Hide whitespace changes
Inline
Side-by-side
mppa_k1c/Asm.v
View file @
e6fd7a6a
...
...
@@ -194,6 +194,7 @@ Inductive instruction : Type :=
(
**
32
-
bit
integer
register
-
register
instructions
*
)
|
Paddw
(
rd
:
ireg
)
(
rs1
rs2
:
ireg
)
(
**
r
integer
addition
*
)
|
Pnegw
(
rd
:
ireg
)
(
rs
:
ireg
)
(
**
r
negate
word
*
)
(
**
64
-
bit
integer
register
-
immediate
instructions
*
)
|
Paddil
(
rd
:
ireg
)
(
rs
:
ireg
)
(
imm
:
int64
)
(
**
r
add
immediate
*
)
...
...
@@ -716,6 +717,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
(
**
32
-
bit
integer
register
-
register
instructions
*
)
|
Paddw
d
s1
s2
=>
Next
(
nextinstr
(
rs
#
d
<-
(
Val
.
add
rs
##
s1
rs
##
s2
)))
m
|
Pnegw
d
s
=>
Next
(
nextinstr
(
rs
#
d
<-
(
Val
.
neg
rs
###
s
)))
m
(
**
64
-
bit
integer
register
-
immediate
instructions
*
)
|
Paddil
d
s
i
=>
...
...
mppa_k1c/Asmgen.v
View file @
e6fd7a6a
...
...
@@ -256,10 +256,10 @@ Definition transl_op
|
Oaddimm
n
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
addimm32
rd
rs
n
k
)
(
*
|
Oneg
,
a1
::
nil
=>
|
Oneg
,
a1
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs
<-
ireg_of
a1
;
OK
(
P
sub
w
rd
GPR0
rs
::
k
)
|
Osub
,
a1
::
a2
::
nil
=>
OK
(
P
neg
w
rd
rs
::
k
)
(
*
|
Osub
,
a1
::
a2
::
nil
=>
do
rd
<-
ireg_of
res
;
do
rs1
<-
ireg_of
a1
;
do
rs2
<-
ireg_of
a2
;
OK
(
Psubw
rd
rs1
rs2
::
k
)
|
Omul
,
a1
::
a2
::
nil
=>
...
...
mppa_k1c/TargetPrinter.ml
View file @
e6fd7a6a
...
...
@@ -219,6 +219,8 @@ module Target : TARGET =
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
|
Pnegw
(
rd
,
rs
)
->
fprintf
oc
" negw %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
...
...
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