From 7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 16 Mar 2019 19:47:03 +0100 Subject: long nand, nor, nxor --- mppa_k1c/Asm.v | 12 ++++++++++++ mppa_k1c/Asmblock.v | 12 ++++++++++++ mppa_k1c/Asmblockdeps.v | 6 ++++++ mppa_k1c/Asmblockgen.v | 21 +++++++++++++++++++++ mppa_k1c/NeedOp.v | 6 ++++++ mppa_k1c/Op.v | 36 ++++++++++++++++++++++++++++++++++++ mppa_k1c/PostpassSchedulingOracle.ml | 15 ++++++++++++--- mppa_k1c/SelectLong.vp | 13 +++++++++++-- mppa_k1c/SelectLongproof.v | 12 ++++++++++-- mppa_k1c/TargetPrinter.ml | 12 ++++++++++++ mppa_k1c/ValueAOp.v | 6 ++++++ 11 files changed, 144 insertions(+), 7 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 2fd46689..354840d4 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -150,8 +150,11 @@ Inductive instruction : Type := | Paddl (rd rs1 rs2: ireg) (**r add long *) | Psubl (rd rs1 rs2: ireg) (**r sub long *) | Pandl (rd rs1 rs2: ireg) (**r and long *) + | Pnandl (rd rs1 rs2: ireg) (**r nand long *) | Porl (rd rs1 rs2: ireg) (**r or long *) + | Pnorl (rd rs1 rs2: ireg) (**r nor long *) | Pxorl (rd rs1 rs2: ireg) (**r xor long *) + | Pnxorl (rd rs1 rs2: ireg) (**r nxor long *) | Pmull (rd rs1 rs2: ireg) (**r mul long (low part) *) | Pslll (rd rs1 rs2: ireg) (**r shift left logical long *) | Psrll (rd rs1 rs2: ireg) (**r shift right logical long *) @@ -186,8 +189,11 @@ Inductive instruction : Type := | Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *) | Paddil (rd rs: ireg) (imm: int64) (**r add immediate long *) | Pandil (rd rs: ireg) (imm: int64) (**r and immediate long *) + | Pnandil (rd rs: ireg) (imm: int64) (**r and immediate long *) | Poril (rd rs: ireg) (imm: int64) (**r or immediate long *) + | Pnoril (rd rs: ireg) (imm: int64) (**r and immediate long *) | Pxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *) + | Pnxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *) . (** Correspondance between Asmblock and Asm *) @@ -277,8 +283,11 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmblock.Paddl rd rs1 rs2 => Paddl rd rs1 rs2 | PArithRRR Asmblock.Psubl rd rs1 rs2 => Psubl rd rs1 rs2 | PArithRRR Asmblock.Pandl rd rs1 rs2 => Pandl rd rs1 rs2 + | PArithRRR Asmblock.Pnandl rd rs1 rs2 => Pnandl rd rs1 rs2 | PArithRRR Asmblock.Porl rd rs1 rs2 => Porl rd rs1 rs2 + | PArithRRR Asmblock.Pnorl rd rs1 rs2 => Pnorl rd rs1 rs2 | PArithRRR Asmblock.Pxorl rd rs1 rs2 => Pxorl rd rs1 rs2 + | PArithRRR Asmblock.Pnxorl rd rs1 rs2 => Pnxorl rd rs1 rs2 | PArithRRR Asmblock.Pmull rd rs1 rs2 => Pmull rd rs1 rs2 | PArithRRR Asmblock.Pslll rd rs1 rs2 => Pslll rd rs1 rs2 | PArithRRR Asmblock.Psrll rd rs1 rs2 => Psrll rd rs1 rs2 @@ -312,8 +321,11 @@ Definition basic_to_instruction (b: basic) := | PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm | PArithRRI64 Asmblock.Paddil rd rs imm => Paddil rd rs imm | PArithRRI64 Asmblock.Pandil rd rs imm => Pandil rd rs imm + | PArithRRI64 Asmblock.Pnandil rd rs imm => Pnandil rd rs imm | PArithRRI64 Asmblock.Poril rd rs imm => Poril rd rs imm + | PArithRRI64 Asmblock.Pnoril rd rs imm => Pnoril rd rs imm | PArithRRI64 Asmblock.Pxoril rd rs imm => Pxoril rd rs imm + | PArithRRI64 Asmblock.Pnxoril rd rs imm => Pnxoril rd rs imm (** Load *) | PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra ofs diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 6e55b074..5279bd29 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -350,8 +350,11 @@ Inductive arith_name_rrr : Type := | Paddl (**r add long *) | Psubl (**r sub long *) | Pandl (**r and long *) + | Pnandl (**r nand long *) | Porl (**r or long *) + | Pnorl (**r nor long *) | Pxorl (**r xor long *) + | Pnxorl (**r nxor long *) | Pmull (**r mul long (low part) *) | Pslll (**r shift left logical long *) | Psrll (**r shift right logical long *) @@ -388,8 +391,11 @@ Inductive arith_name_rri64 : Type := | Pcompil (it: itest) (**r comparison imm long *) | Paddil (**r add immediate long *) | Pandil (**r and immediate long *) + | Pnandil (**r nand immediate long *) | Poril (**r or immediate long *) + | Pnoril (**r nor immediate long *) | Pxoril (**r xor immediate long *) + | Pnxoril (**r nxor immediate long *) . Inductive ar_instruction : Type := @@ -1109,8 +1115,11 @@ Definition arith_eval_rrr n v1 v2 := | Paddl => Val.addl v1 v2 | Psubl => Val.subl v1 v2 | Pandl => Val.andl v1 v2 + | Pnandl => Val.notl (Val.andl v1 v2) | Porl => Val.orl v1 v2 + | Pnorl => Val.notl (Val.orl v1 v2) | Pxorl => Val.xorl v1 v2 + | Pnxorl => Val.notl (Val.xorl v1 v2) | Pmull => Val.mull v1 v2 | Pslll => Val.shll v1 v2 | Psrll => Val.shrlu v1 v2 @@ -1148,8 +1157,11 @@ Definition arith_eval_rri64 n v i := | Pcompil c => compare_long c v (Vlong i) | Paddil => Val.addl v (Vlong i) | Pandil => Val.andl v (Vlong i) + | Pnandil => Val.notl (Val.andl v (Vlong i)) | Poril => Val.orl v (Vlong i) + | Pnoril => Val.notl (Val.orl v (Vlong i)) | Pxoril => Val.xorl v (Vlong i) + | Pnxoril => Val.notl (Val.xorl v (Vlong i)) end. Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 9266a09b..c5b5bd56 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1311,8 +1311,11 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Paddl => "Paddl" | Psubl => "Psubl" | Pandl => "Pandl" + | Pnandl => "Pnandl" | Porl => "Porl" + | Pnorl => "Pnorl" | Pxorl => "Pxorl" + | Pnxorl => "Pnxorl" | Pmull => "Pmull" | Pslll => "Pslll" | Psrll => "Psrll" @@ -1349,8 +1352,11 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := Pcompil _ => "Pcompil" | Paddil => "Paddil" | Pandil => "Pandil" + | Pnandil => "Pnandil" | Poril => "Poril" + | Pnoril => "Pnoril" | Pxoril => "Pxoril" + | Pnxoril => "Pnxoril" end. Definition string_of_arith (op: arith_op): pstring := diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index f32d14bb..9d682bed 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -112,6 +112,9 @@ Definition addimm64 := opimm64 Paddl Paddil. Definition orimm64 := opimm64 Porl Poril. Definition andimm64 := opimm64 Pandl Pandil. Definition xorimm64 := opimm64 Pxorl Pxoril. +Definition norimm64 := opimm64 Pnorl Pnoril. +Definition nandimm64 := opimm64 Pnandl Pnandil. +Definition nxorimm64 := opimm64 Pnxorl Pnxoril. (* Definition sltimm64 := opimm64 Psltl Psltil. @@ -535,18 +538,36 @@ Definition transl_op | Oandlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (andimm64 rd rs n ::i k) + | Onandl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnandl rd rs1 rs2 ::i k) + | Onandlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (nandimm64 rd rs n ::i 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 ::i k) | Oorlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (orimm64 rd rs n ::i k) + | Onorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnorl rd rs1 rs2 ::i k) + | Onorlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (norimm64 rd rs n ::i 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 ::i k) | Oxorlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (xorimm64 rd rs n ::i k) + | Onxorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Pnxorl rd rs1 rs2 ::i k) + | Onxorlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (nxorimm64 rd rs n ::i 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 ::i k) diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index b8f120f5..f7b13cad 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -75,10 +75,16 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv) | Oandl => op2 (default nv) | Oandlimm n => op1 (default nv) + | Onandl => op2 (default nv) + | Onandlimm n => op1 (default nv) | Oorl => op2 (default nv) | Oorlimm n => op1 (default nv) + | Onorl => op2 (default nv) + | Onorlimm n => op1 (default nv) | Oxorl => op2 (default nv) | Oxorlimm n => op1 (default nv) + | Onxorl => op2 (default nv) + | Onxorlimm n => op1 (default nv) | Oshll | Oshrl | Oshrlu => op2 (default nv) | Oshllimm n => op1 (default nv) | Oshrlimm n => op1 (default nv) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index a67fa27f..bf42b65f 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -115,10 +115,16 @@ Inductive operation : Type := | Omodlu (**r [rd = r1 % r2] (unsigned) *) | Oandl (**r [rd = r1 & r2] *) | Oandlimm (n: int64) (**r [rd = r1 & n] *) + | Onandl (**r [rd = ~(r1 & r2)] *) + | Onandlimm (n: int64) (**r [rd = ~(r1 & n)] *) | Oorl (**r [rd = r1 | r2] *) | Oorlimm (n: int64) (**r [rd = r1 | n] *) + | Onorl (**r [rd = ~(r1 | r2)] *) + | Onorlimm (n: int64) (**r [rd = ~(r1 | n)] *) | Oxorl (**r [rd = r1 ^ r2] *) | Oxorlimm (n: int64) (**r [rd = r1 ^ n] *) + | Onxorl (**r [rd = ~(r1 ^ r2)] *) + | Onxorlimm (n: int64) (**r [rd = ~(r1 ^ n)] *) | Oshll (**r [rd = r1 << r2] *) | Oshllimm (n: int) (**r [rd = r1 << n] *) | Oshrl (**r [rd = r1 >> r2] (signed) *) @@ -290,10 +296,16 @@ Definition eval_operation | Omodlu, v1::v2::nil => Val.modlu v1 v2 | Oandl, v1::v2::nil => Some(Val.andl v1 v2) | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n)) + | Onandl, v1::v2::nil => Some(Val.notl (Val.andl v1 v2)) + | Onandlimm n, v1::nil => Some(Val.notl (Val.andl v1 (Vlong n))) | Oorl, v1::v2::nil => Some(Val.orl v1 v2) | Oorlimm n, v1::nil => Some (Val.orl v1 (Vlong n)) + | Onorl, v1::v2::nil => Some(Val.notl (Val.orl v1 v2)) + | Onorlimm n, v1::nil => Some(Val.notl (Val.orl v1 (Vlong n))) | Oxorl, v1::v2::nil => Some(Val.xorl v1 v2) | Oxorlimm n, v1::nil => Some (Val.xorl v1 (Vlong n)) + | Onxorl, v1::v2::nil => Some(Val.notl (Val.xorl v1 v2)) + | Onxorlimm n, v1::nil => Some(Val.notl (Val.xorl v1 (Vlong n))) | Oshll, v1::v2::nil => Some (Val.shll v1 v2) | Oshllimm n, v1::nil => Some (Val.shll v1 (Vint n)) | Oshrl, v1::v2::nil => Some (Val.shrl v1 v2) @@ -453,10 +465,16 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omodlu => (Tlong :: Tlong :: nil, Tlong) | Oandl => (Tlong :: Tlong :: nil, Tlong) | Oandlimm _ => (Tlong :: nil, Tlong) + | Onandl => (Tlong :: Tlong :: nil, Tlong) + | Onandlimm _ => (Tlong :: nil, Tlong) | Oorl => (Tlong :: Tlong :: nil, Tlong) | Oorlimm _ => (Tlong :: nil, Tlong) + | Onorl => (Tlong :: Tlong :: nil, Tlong) + | Onorlimm _ => (Tlong :: nil, Tlong) | Oxorl => (Tlong :: Tlong :: nil, Tlong) | Oxorlimm _ => (Tlong :: nil, Tlong) + | Onxorl => (Tlong :: Tlong :: nil, Tlong) + | Onxorlimm _ => (Tlong :: nil, Tlong) | Oshll => (Tlong :: Tint :: nil, Tlong) | Oshllimm _ => (Tlong :: nil, Tlong) | Oshrl => (Tlong :: Tint :: nil, Tlong) @@ -630,12 +648,21 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* andl, andlimm *) - destruct v0; destruct v1... - destruct v0... + (* nandl, nandlimm *) + - destruct v0; destruct v1... + - destruct v0... (* orl, orlimm *) - destruct v0; destruct v1... - destruct v0... + (* norl, norlimm *) + - destruct v0; destruct v1... + - destruct v0... (* xorl, xorlimm *) - destruct v0; destruct v1... - destruct v0... + (* nxorl, nxorlimm *) + - destruct v0; destruct v1... + - destruct v0... (* shll, shllimm *) - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... @@ -1106,12 +1133,21 @@ Proof. (* andl, andlimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. + (* nandl, nandlimm *) + - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. (* orl, orlimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. + (* norl, norlimm *) + - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. (* xorl, xorlimm *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. + (* nxorl, nxorlimm *) + - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. (* shll, shllimm *) - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 2d25c281..3c242441 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -72,8 +72,11 @@ let arith_rrr_str = function | Paddl -> "Paddl" | Psubl -> "Psubl" | Pandl -> "Pandl" + | Pnandl -> "Pnandl" | Porl -> "Porl" + | Pnorl -> "Pnorl" | Pxorl -> "Pxorl" + | Pnxorl -> "Pnxorl" | Pmull -> "Pmull" | Pslll -> "Pslll" | Psrll -> "Psrll" @@ -106,8 +109,11 @@ let arith_rri64_str = function | Pcompil it -> "Pcompil" | Paddil -> "Paddil" | Pandil -> "Pandil" + | Pnandil -> "Pnandil" | Poril -> "Poril" + | Pnoril -> "Pnoril" | Pxoril -> "Pxoril" + | Pnxoril -> "Pnxoril" let arith_ri32_str = "Pmake" @@ -384,7 +390,7 @@ type real_instruction = (* ALU *) | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord - | Nandw | Norw | Nxorw + | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Make | Nop | Sxwd | Zxwd (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld @@ -403,6 +409,7 @@ let ab_inst_to_real = function | "Pandw" | "Pandiw" -> Andw | "Pnandw" | "Pnandiw" -> Nandw | "Pandl" | "Pandil" -> Andd + | "Pnandl" | "Pnandil" -> Nandd | "Pcompw" | "Pcompiw" -> Compw | "Pcompl" | "Pcompil" -> Compd | "Pfcompw" -> Fcompw @@ -412,6 +419,7 @@ let ab_inst_to_real = function | "Porw" | "Poriw" -> Orw | "Pnorw" | "Pnoriw" -> Norw | "Porl" | "Poril" -> Ord + | "Pnorl" | "Pnoril" -> Nord | "Psubw" | "Pnegw" -> Sbfw | "Psubl" | "Pnegl" -> Sbfd | "Psraw" | "Psraiw" -> Sraw @@ -424,6 +432,7 @@ let ab_inst_to_real = function | "Pxorw" | "Pxoriw" -> Xorw | "Pnxorw" | "Pnxoriw" -> Nxorw | "Pxorl" | "Pxoril" -> Xord + | "Pnxorl" | "Pnxoril" -> Nxord | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make | "Pnop" | "Pcvtw2l" -> Nop | "Psxwd" -> Sxwd @@ -489,7 +498,7 @@ let rec_to_usage r = (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | _ -> raise InvalidEncoding) - | Addd | Andd | Ord | Sbfd | Xord -> + | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y) @@ -538,7 +547,7 @@ let rec_to_usage r = let real_inst_to_latency = function | Nop -> 0 (* Only goes through ID *) | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw - | Rorw | Nandw | Norw | Nxorw + | Rorw | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make | Sxwd | Zxwd | Fcompw | Fcompd -> 1 diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 5e94fbb5..cc266abd 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -287,8 +287,17 @@ Nondetfunction xorl (e1: expr) (e2: expr) := (** ** Integer logical negation *) -Definition notl (e: expr) := - if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e. +Nondetfunction notl (e: expr) := + match e with + | Eop Oandl (e1:::e2:::Enil) => Eop Onandl (e1:::e2:::Enil) + | Eop (Oandlimm n) (e1:::Enil) => Eop (Onandlimm n) (e1:::Enil) + | Eop Oorl (e1:::e2:::Enil) => Eop Onorl (e1:::e2:::Enil) + | Eop (Oorlimm n) (e1:::Enil) => Eop (Onorlimm n) (e1:::Enil) + | Eop Oxorl (e1:::e2:::Enil) => Eop Onxorl (e1:::e2:::Enil) + | Eop (Oxorlimm n) (e1:::Enil) => Eop (Onxorlimm n) (e1:::Enil) + | _ => xorlimm Int64.mone e + end. +(* old: if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e. *) (** ** Integer division and modulus *) diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 44846a6f..a8a6bc9c 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -441,8 +441,16 @@ Qed. Theorem eval_notl: unary_constructor_sound notl Val.notl. Proof. - unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl. - red; intros. rewrite Val.notl_xorl. apply eval_xorlimm; auto. + assert (forall v, Val.lessdef (Val.notl (Val.notl v)) v). + destruct v; simpl; auto. rewrite Int64.not_involutive; auto. + unfold notl; red; intros until x; case (notl_match a); intros; InvEval. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - apply eval_xorlimm; assumption. Qed. Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 49ea53b9..d30d62a2 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -393,10 +393,16 @@ module Target (*: TARGET*) = fprintf oc " sbfd %a = %a, %a\n" ireg rd ireg rs2 ireg rs1 | Pandl (rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " andd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pnandl (rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " nandd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Porl (rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " ord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pnorl (rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " nord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pxorl (rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " xord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pnxorl (rd, rs1, rs2) -> assert Archi.ptr64; + fprintf oc " nxord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pmull (rd, rs1, rs2) -> fprintf oc " muld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pslll (rd, rs1, rs2) -> @@ -459,10 +465,16 @@ module Target (*: TARGET*) = fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pandil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " andd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pnandil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " andd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Poril (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " ord %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pnoril (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " nord %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pxoril (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " xord %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pnxoril (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " nxord %a = %a, %a\n" ireg rd ireg rs coqint64 imm let get_section_names name = let (text, lit) = diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 15378811..33f4d8a9 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -101,10 +101,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omodlu, v1::v2::nil => modlu v1 v2 | Oandl, v1::v2::nil => andl v1 v2 | Oandlimm n, v1::nil => andl v1 (L n) + | Onandl, v1::v2::nil => notl (andl v1 v2) + | Onandlimm n, v1::nil => notl (andl v1 (L n)) | Oorl, v1::v2::nil => orl v1 v2 | Oorlimm n, v1::nil => orl v1 (L n) + | Onorl, v1::v2::nil => notl (orl v1 v2) + | Onorlimm n, v1::nil => notl (orl v1 (L n)) | Oxorl, v1::v2::nil => xorl v1 v2 | Oxorlimm n, v1::nil => xorl v1 (L n) + | Onxorl, v1::v2::nil => notl (xorl v1 v2) + | Onxorlimm n, v1::nil => notl (xorl v1 (L n)) | Oshll, v1::v2::nil => shll v1 v2 | Oshllimm n, v1::nil => shll v1 (I n) | Oshrl, v1::v2::nil => shrl v1 v2 -- cgit