diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 | ||||
| -rw-r--r-- | mppa_k1c/Asmgen.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 2 |
3 files changed, 8 insertions, 3 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index e1359cb0..568a88af 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -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 => diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 4fed544f..1113bd4f 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -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 (Psubl rd GPR0 rs :: k) - | Osubl, a1 :: a2 :: nil => + OK (Pnegl 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 => diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index dcae5b10..cb978ba8 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -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 |