diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 22:13:53 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 22:13:53 +0100 |
| commit | 4cc5324db73dd014bcd2c118f5769f88e52f8643 (patch) | |
| tree | 6f3df7b011f34f2cdaa8381342756708f7b02e49 | |
| parent | f321f75979d18ab99f226b2c5d6bbb59bffb5cac (diff) | |
| parent | 2af07d6a328f73a32bc2c768e3108dd3db393ed1 (diff) | |
| download | compcert-kvx-4cc5324db73dd014bcd2c118f5769f88e52f8643.tar.gz compcert-kvx-4cc5324db73dd014bcd2c118f5769f88e52f8643.zip | |
Merge branch 'mppa-madd' into mppa_postpass
| -rw-r--r-- | mppa_k1c/Asm.v | 20 | ||||
| -rw-r--r-- | mppa_k1c/Asmblock.v | 45 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 97 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 34 | ||||
| -rw-r--r-- | mppa_k1c/Machregs.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/NeedOp.v | 9 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 55 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 35 | ||||
| -rw-r--r-- | mppa_k1c/SelectOp.v | 1323 | ||||
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 10 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 12 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 12 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/ImpDep.v | 6 | ||||
| -rw-r--r-- | test/monniaux/madd/madd.c | 11 | ||||
| -rw-r--r-- | test/monniaux/madd/madd_run.c | 9 |
16 files changed, 327 insertions, 1357 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 029ac995..493f4a05 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -151,6 +151,7 @@ Inductive instruction : Type := | Psraw (rd rs1 rs2: ireg) (**r shift right arithmetic word *)
| Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
+ | Pmaddw (rd rs1 rs2: ireg) (**r multiply-add words *)
| Paddl (rd rs1 rs2: ireg) (**r add long *)
| Psubl (rd rs1 rs2: ireg) (**r sub long *)
@@ -166,6 +167,7 @@ Inductive instruction : Type := | Pslll (rd rs1 rs2: ireg) (**r shift left logical long *)
| Psrll (rd rs1 rs2: ireg) (**r shift right logical long *)
| Psral (rd rs1 rs2: ireg) (**r shift right arithmetic long *)
+ | Pmaddl (rd rs1 rs2: ireg) (**r multiply-add long *)
| Pfaddd (rd rs1 rs2: ireg) (**r Float addition double *)
| Pfaddw (rd rs1 rs2: ireg) (**r Float addition word *)
@@ -178,6 +180,7 @@ Inductive instruction : Type := | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *)
| Paddiw (rd rs: ireg) (imm: int) (**r add imm word *)
+ | Pmuliw (rd rs: ireg) (imm: int) (**r mul imm word *)
| Pandiw (rd rs: ireg) (imm: int) (**r and imm word *)
| Pnandiw (rd rs: ireg) (imm: int) (**r nand imm word *)
| Poriw (rd rs: ireg) (imm: int) (**r or imm word *)
@@ -190,6 +193,7 @@ Inductive instruction : Type := | Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
| Pslliw (rd rs: ireg) (imm: int) (**r shift left logical imm word *)
| Proriw (rd rs: ireg) (imm: int) (**r rotate right imm word *)
+ | Pmaddiw (rd rs: ireg) (imm: int) (**r multiply add imm word *)
| Psllil (rd rs: ireg) (imm: int) (**r shift left logical immediate long *)
| Psrlil (rd rs: ireg) (imm: int) (**r shift right logical immediate long *)
| Psrail (rd rs: ireg) (imm: int) (**r shift right arithmetic immediate long *)
@@ -197,6 +201,7 @@ Inductive instruction : Type := (** Arith RRI64 *)
| Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *)
| Paddil (rd rs: ireg) (imm: int64) (**r add immediate long *)
+ | Pmulil (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 *)
@@ -205,7 +210,8 @@ Inductive instruction : Type := | Pnxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *)
| Pandnil (rd rs: ireg) (imm: int64) (**r andn long *)
| Pornil (rd rs: ireg) (imm: int64) (**r orn long *)
- .
+ | Pmaddil (rd rs: ireg) (imm: int64) (**r multiply add imm long *)
+.
(** Correspondance between Asmblock and Asm *)
@@ -320,6 +326,7 @@ Definition basic_to_instruction (b: basic) := (* RRI32 *)
| PArithRRI32 (Asmblock.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
| PArithRRI32 Asmblock.Paddiw rd rs imm => Paddiw rd rs imm
+ | PArithRRI32 Asmblock.Pmuliw rd rs imm => Pmuliw rd rs imm
| PArithRRI32 Asmblock.Pandiw rd rs imm => Pandiw rd rs imm
| PArithRRI32 Asmblock.Pnandiw rd rs imm => Pnandiw rd rs imm
| PArithRRI32 Asmblock.Poriw rd rs imm => Poriw rd rs imm
@@ -339,6 +346,7 @@ Definition basic_to_instruction (b: basic) := (* RRI64 *)
| PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm
| PArithRRI64 Asmblock.Paddil rd rs imm => Paddil rd rs imm
+ | PArithRRI64 Asmblock.Pmulil rd rs imm => Pmulil 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
@@ -348,6 +356,16 @@ Definition basic_to_instruction (b: basic) := | PArithRRI64 Asmblock.Pandnil rd rs imm => Pandnil rd rs imm
| PArithRRI64 Asmblock.Pornil rd rs imm => Pornil rd rs imm
+ (** ARRR *)
+ | PArithARRR Asmblock.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
+ | PArithARRR Asmblock.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
+
+ (** ARRI32 *)
+ | PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
+
+ (** ARRI64 *)
+ | PArithARRI64 Asmblock.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm
+
(** Load *)
| PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra ofs
| PLoadRRO Asmblock.Plbu rd ra ofs => Plbu rd ra ofs
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 03c7e6d5..d335801e 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -379,6 +379,7 @@ Inductive arith_name_rri32 : Type := | Pcompiw (it: itest) (**r comparison imm word *) | Paddiw (**r add imm word *) + | Pmuliw (**r add imm word *) | Pandiw (**r and imm word *) | Pnandiw (**r nand imm word *) | Poriw (**r or imm word *) @@ -399,6 +400,7 @@ Inductive arith_name_rri32 : Type := Inductive arith_name_rri64 : Type := | Pcompil (it: itest) (**r comparison imm long *) | Paddil (**r add immediate long *) + | Pmulil (**r mul immediate long *) | Pandil (**r and immediate long *) | Pnandil (**r nand immediate long *) | Poril (**r or immediate long *) @@ -409,6 +411,19 @@ Inductive arith_name_rri64 : Type := | Pornil (**r orn immediate long *) . +Inductive arith_name_arrr : Type := + | Pmaddw (**r multiply add word *) + | Pmaddl (**r multiply add long *) +. + +Inductive arith_name_arri32 : Type := + | Pmaddiw (**r multiply add word *) +. + +Inductive arith_name_arri64 : Type := + | Pmaddil (**r multiply add long *) +. + Inductive ar_instruction : Type := | PArithR (i: arith_name_r) (rd: ireg) | PArithRR (i: arith_name_rr) (rd rs: ireg) @@ -419,6 +434,9 @@ Inductive ar_instruction : Type := | PArithRRR (i: arith_name_rrr) (rd rs1 rs2: ireg) | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int) | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64) + | PArithARRR (i: arith_name_arrr) (rd rs1 rs2: ireg) + | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int) + | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64) . Coercion PArithR: arith_name_r >-> Funclass. @@ -430,6 +448,9 @@ Coercion PArithRF64: arith_name_rf64 >-> Funclass. Coercion PArithRRR: arith_name_rrr >-> Funclass. Coercion PArithRRI32: arith_name_rri32 >-> Funclass. Coercion PArithRRI64: arith_name_rri64 >-> Funclass. +Coercion PArithARRR: arith_name_arrr >-> Funclass. +Coercion PArithARRI32: arith_name_arri32 >-> Funclass. +Coercion PArithARRI64: arith_name_arri64 >-> Funclass. Inductive basic : Type := | PArith (i: ar_instruction) @@ -1151,6 +1172,7 @@ Definition arith_eval_rri32 n v i := match n with | Pcompiw c => compare_int c v (Vint i) | Paddiw => Val.add v (Vint i) + | Pmuliw => Val.mul v (Vint i) | Pandiw => Val.and v (Vint i) | Pnandiw => Val.notint (Val.and v (Vint i)) | Poriw => Val.or v (Vint i) @@ -1172,6 +1194,7 @@ Definition arith_eval_rri64 n v i := match n with | Pcompil c => compare_long c v (Vlong i) | Paddil => Val.addl v (Vlong i) + | Pmulil => Val.mull v (Vlong i) | Pandil => Val.andl v (Vlong i) | Pnandil => Val.notl (Val.andl v (Vlong i)) | Poril => Val.orl v (Vlong i) @@ -1182,6 +1205,22 @@ Definition arith_eval_rri64 n v i := | Pornil => Val.orl (Val.notl v) (Vlong i) end. +Definition arith_eval_arrr n v1 v2 v3 := + match n with + | Pmaddw => Val.add v1 (Val.mul v2 v3) + | Pmaddl => Val.addl v1 (Val.mull v2 v3) + end. + +Definition arith_eval_arri32 n v1 v2 v3 := + match n with + | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3)) + end. + +Definition arith_eval_arri64 n v1 v2 v3 := + match n with + | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3)) + end. + Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | PArithR n d => rs#d <- (arith_eval_r n) @@ -1198,6 +1237,12 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i) | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i) + + | PArithARRR n d s1 s2 => rs#d <- (arith_eval_arrr n rs#d rs#s1 rs#s2) + + | PArithARRI32 n d s i => rs#d <- (arith_eval_arri32 n rs#d rs#s i) + + | PArithARRI64 n d s i => rs#d <- (arith_eval_arri64 n rs#d rs#s i) end. (** * load/store *) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 7e9fb8f1..501ec212 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -54,6 +54,9 @@ Inductive arith_op := | OArithRRR (n: arith_name_rrr) | OArithRRI32 (n: arith_name_rri32) (imm: int) | OArithRRI64 (n: arith_name_rri64) (imm: int64) + | OArithARRR (n: arith_name_arrr) + | OArithARRI32 (n: arith_name_arri32) (imm: int) + | OArithARRI64 (n: arith_name_arri64) (imm: int64) . Coercion OArithR: arith_name_r >-> arith_op. @@ -111,10 +114,13 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRF64 n i, [] => Some (Val (arith_eval_rf64 n i)) | OArithRRR n, [Val v1; Val v2] => Some (Val (arith_eval_rrr n v1 v2)) - | OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i)) | OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i)) + | OArithARRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrr n v1 v2 v3)) + | OArithARRI32 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri32 n v1 v2 i)) + | OArithARRI64 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri64 n v1 v2 i)) + | _, _ => None end. @@ -282,17 +288,31 @@ Definition iandb (ib1 ib2: ?? bool): ?? bool := RET (andb b1 b2). Definition arith_op_eq (o1 o2: arith_op): ?? bool := - match o1, o2 with - | OArithR n1, OArithR n2 => struct_eq n1 n2 - | OArithRR n1, OArithRR n2 => phys_eq n1 n2 - | OArithRI32 n1 i1, OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRI64 n1 i1, OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRF32 n1 i1, OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRF64 n1 i1, OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRRR n1, OArithRRR n2 => phys_eq n1 n2 - | OArithRRI32 n1 i1, OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | OArithRRI64 n1 i1, OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) - | _, _ => RET false + match o1 with + | OArithR n1 => + match o2 with OArithR n2 => struct_eq n1 n2 | _ => RET false end + | OArithRR n1 => + match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithRI32 n1 i1 => + match o2 with OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRI64 n1 i1 => + match o2 with OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRF32 n1 i1 => + match o2 with OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRF64 n1 i1 => + match o2 with OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRRR n1 => + match o2 with OArithRRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithRRI32 n1 i1 => + match o2 with OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRRI64 n1 i1 => + match o2 with OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithARRR n1 => + match o2 with OArithARRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithARRI32 n1 i1 => + match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithARRI64 n1 i1 => + match o2 with OArithARRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end end. Lemma arith_op_eq_correct o1 o2: @@ -329,7 +349,8 @@ Proof. apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. Qed. - +(* TODO: rewrite control_op_eq in a robust style against the miss of a case + cf. arith_op_eq above *) Definition control_op_eq (c1 c2: control_op): ?? bool := match c1, c2 with | Oj_l l1, Oj_l l2 => phys_eq l1 l2 @@ -353,6 +374,8 @@ Proof. Qed. +(* TODO: rewrite op_eq in a robust style against the miss of a case + cf. arith_op_eq above *) Definition op_eq (o1 o2: op): ?? bool := match o1, o2 with | Arith i1, Arith i2 => arith_op_eq i1 i2 @@ -389,13 +412,12 @@ Qed. (* Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. - Theorem op_eq_correct o1 o2: WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. Proof. wlp_simplify. Qed. - *) +*) End IMPPARAM. @@ -541,6 +563,9 @@ Definition trans_arith (ai: ar_instruction) : macro := | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Enil))] | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))] | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))] + | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (Name(#d) @ Name (#s1) @ Name (#s2) @ Enil))] + | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (Name(#d) @ Name (#s) @ Enil))] + | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (Name(#d) @ Name (#s) @ Enil))] end. @@ -727,6 +752,27 @@ Proof. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRR *) + - inv H; inv H0; + eexists; split; try split. + * simpl. pose (H1 rd); rewrite e. pose (H1 rs1); rewrite e0. pose (H1 rs2); rewrite e1. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRI32 *) + - inv H; inv H0; + eexists; split; try split. + * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRI64 *) + - inv H; inv H0; + eexists; split; try split. + * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. Qed. Lemma forward_simu_basic: @@ -1379,6 +1425,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := match n with Pcompiw _ => "Pcompiw" | Paddiw => "Paddiw" + | Pmuliw => "Pmuliw" | Pandiw => "Pandiw" | Pnandiw => "Pnandiw" | Poriw => "Poriw" @@ -1400,6 +1447,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := match n with Pcompil _ => "Pcompil" | Paddil => "Paddil" + | Pmulil => "Pmulil" | Pandil => "Pandil" | Pnandil => "Pnandil" | Poril => "Poril" @@ -1410,6 +1458,22 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := | Pornil => "Pornil" end. +Definition string_of_name_arrr (n: arith_name_arrr): pstring := + match n with + | Pmaddw => "Pmaddw" + | Pmaddl => "Pmaddl" + end. + +Definition string_of_name_arri32 (n: arith_name_arri32): pstring := + match n with + | Pmaddiw => "Pmaddw" + end. + +Definition string_of_name_arri64 (n: arith_name_arri64): pstring := + match n with + | Pmaddil => "Pmaddl" + end. + Definition string_of_arith (op: arith_op): pstring := match op with | OArithR n => string_of_name_r n @@ -1421,6 +1485,9 @@ Definition string_of_arith (op: arith_op): pstring := | OArithRRR n => string_of_name_rrr n | OArithRRI32 n _ => string_of_name_rri32 n | OArithRRI64 n _ => string_of_name_rri64 n + | OArithARRR n => string_of_name_arrr n + | OArithARRI32 n _ => string_of_name_arri32 n + | OArithARRI64 n _ => string_of_name_arri64 n end. Definition string_of_name_lrro (n: load_name_rro) : pstring := diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index c54394eb..312d2386 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -83,6 +83,7 @@ Definition opimm32 (op: arith_name_rrr) end. Definition addimm32 := opimm32 Paddw Paddiw. +Definition mulimm32 := opimm32 Pmulw Pmuliw. Definition andimm32 := opimm32 Pandw Pandiw. Definition nandimm32 := opimm32 Pnandw Pnandiw. Definition orimm32 := opimm32 Porw Poriw. @@ -107,6 +108,7 @@ Definition opimm64 (op: arith_name_rrr) end. Definition addimm64 := opimm64 Paddl Paddil. +Definition mulimm64 := opimm64 Pmull Pmulil. Definition orimm64 := opimm64 Porl Poril. Definition andimm64 := opimm64 Pandl Pandil. Definition xorimm64 := opimm64 Pxorl Pxoril. @@ -418,6 +420,9 @@ Definition transl_op | Omul, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmulw rd rs1 rs2 ::i k) + | Omulimm n, a1 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; + OK (mulimm32 rd rs1 n ::i k) | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *) | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *) | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") @@ -511,7 +516,17 @@ Definition transl_op | Ororimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Proriw rd rs n ::i k) - + | Omadd, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmaddw r1 r2 r3 ::i k) + | Omaddimm n, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + OK (Pmaddiw r1 r2 n ::i k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -539,6 +554,9 @@ Definition transl_op | Omull, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmull rd rs1 rs2 ::i k) + | Omullimm n, a1 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; + OK (mulimm64 rd rs1 n ::i k) | Omullhs, _ => Error (msg "Asmblockgen.transl_op: Omullhs") (* Normalement pas émis *) | Omullhu, _ => Error (msg "Asmblockgen.transl_op: Omullhu") (* Normalement pas émis *) | Odivl, _ => Error (msg "Asmblockgen.transl_op: Odivl") (* Géré par fonction externe *) @@ -621,7 +639,19 @@ Definition transl_op Psrlil RTMP RTMP (Int.sub Int64.iwordsize' n) ::i Paddl RTMP rs RTMP ::i Psrail rd RTMP n ::i k) - + (* FIXME + | Omaddl, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmaddl r1 r2 r3 ::i k) + | Omaddlimm n, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + OK (Pmaddil r1 r2 n ::i k) +*) | Oabsf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfabsd rd rs ::i k) diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 28154c7f..ef0f97a9 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -210,7 +210,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned => true + | Ocast32unsigned | Omadd | Omaddimm _ => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 12d7a4f7..68f43894 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -25,6 +25,7 @@ Require Import NeedDomain. Definition op1 (nv: nval) := nv :: nil. Definition op2 (nv: nval) := nv :: nv :: nil. +Definition op3 (nv: nval) := nv :: nv :: nv :: nil. Definition needs_of_condition (cond: condition): list nval := nil. @@ -44,6 +45,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oneg => op1 (modarith nv) | Osub => op2 (default nv) | Omul => op2 (modarith nv) + | Omulimm _ => op1 (modarith nv) | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv) | Oand => op2 (bitwise nv) | Oandimm n => op1 (andimm nv n) @@ -68,6 +70,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ororimm n => op1 (ror nv n) | Oshruimm n => op1 (shruimm nv n) | Oshrximm n => op1 (default nv) + | Omadd => op3 (modarith nv) + | Omaddimm n => op2 (modarith nv) | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocast32signed => op1 (default nv) @@ -77,6 +81,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegl => op1 (default nv) | Osubl => op2 (default nv) | Omull => op2 (default nv) + | Omullimm _ => op1 (default nv) | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv) | Oandl => op2 (default nv) | Oandlimm n => op1 (default nv) @@ -168,6 +173,7 @@ Proof. - apply add_sound; auto with na. - apply neg_sound; auto. - apply mul_sound; auto. +- apply mul_sound; auto with na. - apply and_sound; auto. - apply andimm_sound; auto. - apply notint_sound; apply and_sound; auto. @@ -189,6 +195,9 @@ Proof. - apply shrimm_sound; auto. - apply shruimm_sound; auto. - apply ror_sound; auto. + (* madd *) +- apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. +- apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. Qed. Lemma operation_is_redundant_sound: diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 04ea8945..0e9a7af9 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -70,6 +70,7 @@ Inductive operation : Type := | Oneg (**r [rd = - r1] *) | Osub (**r [rd = r1 - r2] *) | Omul (**r [rd = r1 * r2] *) + | Omulimm (n: int) (**r [rd = r1 * n] *) | Omulhs (**r [rd = high part of r1 * r2, signed] *) | Omulhu (**r [rd = high part of r1 * r2, unsigned] *) | Odiv (**r [rd = r1 / r2] (signed) *) @@ -101,6 +102,8 @@ Inductive operation : Type := | Oshruimm (n: int) (**r [rd = r1 >> n] (unsigned) *) | Oshrximm (n: int) (**r [rd = r1 / 2^n] (signed) *) | Ororimm (n: int) (**r rotate right immediate *) + | Omadd (**r [rd = rd + r1 * r2] *) + | Omaddimm (n: int) (**r [rd = rd + r1 * imm] *) (*c 64-bit integer arithmetic: *) | Omakelong (**r [rd = r1 << 32 | r2] *) | Olowlong (**r [rd = low-word(r1)] *) @@ -112,6 +115,7 @@ Inductive operation : Type := | Onegl (**r [rd = - r1] *) | Osubl (**r [rd = r1 - r2] *) | Omull (**r [rd = r1 * r2] *) + | Omullimm (n: int64) (**r [rd = r1 * n] *) | Omullhs (**r [rd = high part of r1 * r2, signed] *) | Omullhu (**r [rd = high part of r1 * r2, unsigned] *) | Odivl (**r [rd = r1 / r2] (signed) *) @@ -142,6 +146,10 @@ Inductive operation : Type := | Oshrlu (**r [rd = r1 >> r2] (unsigned) *) | Oshrluimm (n: int) (**r [rd = r1 >> n] (unsigned) *) | Oshrxlimm (n: int) (**r [rd = r1 / 2^n] (signed) *) + (* FIXME + | Omaddl (**r [rd = rd + r1 * r2] *) + | Omaddlimm (n: int64) (**r [rd = rd + r1 * imm] *) +*) (*c Floating-point arithmetic: *) | Onegf (**r [rd = - r1] *) | Oabsf (**r [rd = abs(r1)] *) @@ -262,6 +270,7 @@ Definition eval_operation | Oneg, v1 :: nil => Some (Val.neg v1) | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2) | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2) + | Omulimm n, v1 :: nil => Some (Val.mul v1 (Vint n)) | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2) | Odiv, v1 :: v2 :: nil => Val.divs v1 v2 @@ -293,6 +302,9 @@ Definition eval_operation | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2) | Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n)) | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) + | Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3)) + | (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n))) + | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2) | Olowlong, v1::nil => Some (Val.loword v1) | Ohighlong, v1::nil => Some (Val.hiword v1) @@ -303,6 +315,7 @@ Definition eval_operation | Onegl, v1::nil => Some (Val.negl v1) | Osubl, v1::v2::nil => Some (Val.subl v1 v2) | Omull, v1::v2::nil => Some (Val.mull v1 v2) + | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n)) | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2) | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2) | Odivl, v1::v2::nil => Val.divls v1 v2 @@ -333,6 +346,12 @@ Definition eval_operation | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2) | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n)) | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n) + + (* + | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3)) + | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n))) + *) + | Onegf, v1::nil => Some (Val.negf v1) | Oabsf, v1::nil => Some (Val.absf v1) | Oaddf, v1::v2::nil => Some (Val.addf v1 v2) @@ -441,6 +460,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oneg => (Tint :: nil, Tint) | Osub => (Tint :: Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) + | Omulimm _ => (Tint :: nil, Tint) | Omulhs => (Tint :: Tint :: nil, Tint) | Omulhu => (Tint :: Tint :: nil, Tint) | Odiv => (Tint :: Tint :: nil, Tint) @@ -472,6 +492,9 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshruimm _ => (Tint :: nil, Tint) | Oshrximm _ => (Tint :: nil, Tint) | Ororimm _ => (Tint :: nil, Tint) + | Omadd => (Tint :: Tint :: Tint :: nil, Tint) + | Omaddimm _ => (Tint :: Tint :: nil, Tint) + | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) | Ohighlong => (Tlong :: nil, Tint) @@ -482,6 +505,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Onegl => (Tlong :: nil, Tlong) | Osubl => (Tlong :: Tlong :: nil, Tlong) | Omull => (Tlong :: Tlong :: nil, Tlong) + | Omullimm _ => (Tlong :: nil, Tlong) | Omullhs => (Tlong :: Tlong :: nil, Tlong) | Omullhu => (Tlong :: Tlong :: nil, Tlong) | Odivl => (Tlong :: Tlong :: nil, Tlong) @@ -512,6 +536,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshrlu => (Tlong :: Tint :: nil, Tlong) | Oshrluimm _ => (Tlong :: nil, Tlong) | Oshrxlimm _ => (Tlong :: nil, Tlong) + (* FIXME + | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong) + | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong) +*) | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat) @@ -601,8 +629,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* neg, sub *) - destruct v0... - unfold Val.sub. destruct v0; destruct v1... - (* mul, mulhs, mulhu *) + (* mul, mulimm, mulhs, mulhu *) - destruct v0; destruct v1... + - destruct v0... - destruct v0; destruct v1... - destruct v0; destruct v1... (* div, divu *) @@ -654,6 +683,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0... (* shrimm *) - destruct v0; simpl... + (* madd *) + - destruct v0; destruct v1; destruct v2... + - destruct v0; destruct v1... (* makelong, lowlong, highlong *) - destruct v0; destruct v1... - destruct v0... @@ -671,6 +703,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (eq_block b b0)... (* mull, mullhs, mullhu *) - destruct v0; destruct v1... + - destruct v0... - destruct v0; destruct v1... - destruct v0; destruct v1... (* divl, divlu *) @@ -720,6 +753,10 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... (* shrxl *) - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0... + (* FIXME + (* maddl, maddlim *) + - destruct v0; destruct v1; destruct v2... + - destruct v0; destruct v1... *) (* negf, absf *) - destruct v0... - destruct v0... @@ -1095,8 +1132,9 @@ Proof. (* neg, sub *) - inv H4; simpl; auto. - apply Val.sub_inject; auto. - (* mul, mulhs, mulhu *) + (* mul, mulimm, mulhs, mulhu *) - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. (* div, divu *) @@ -1153,6 +1191,9 @@ Proof. destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists. (* rorimm *) - inv H4; simpl; auto. + (* madd, maddim *) + - inv H2; inv H3; inv H4; simpl; auto. + - inv H2; inv H4; simpl; auto. (* makelong, highlong, lowlong *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1168,6 +1209,7 @@ Proof. - apply Val.subl_inject; auto. (* mull, mullhs, mullhu *) - inv H4; inv H2; simpl; auto. + - inv H4; simpl; auto. - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. (* divl, divlu *) @@ -1222,6 +1264,15 @@ Proof. (* shrx *) - inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. + + (* + (* maddl, maddlim *) + - inv H2; inv H3; inv H4; simpl; auto; simpl. + destruct Archi.ptr64; trivial. + s + - inv H2; inv H4; simpl; auto. + *) + (* negf, absf *) - inv H4; simpl; auto. - inv H4; simpl; auto. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index ac257af3..2c39e342 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -95,6 +95,7 @@ let arith_rrr_str = function let arith_rri32_str = function | Pcompiw it -> "Pcompiw" | Paddiw -> "Paddiw" + | Pmuliw -> "Pmuliw" | Pandiw -> "Pandiw" | Pnandiw -> "Pnandiw" | Poriw -> "Poriw" @@ -114,6 +115,7 @@ let arith_rri32_str = function let arith_rri64_str = function | Pcompil it -> "Pcompil" | Paddil -> "Paddil" + | Pmulil -> "Pmulil" | Pandil -> "Pandil" | Pnandil -> "Pnandil" | Poril -> "Poril" @@ -123,6 +125,10 @@ let arith_rri64_str = function | Pandnil -> "Pandnil" | Pornil -> "Pornil" +let arith_arrr_str = function + | Pmaddw -> "Pmaddw" + | Pmaddl -> "Pmaddl" + let arith_ri32_str = "Pmake" let arith_ri64_str = "Pmakel" @@ -162,6 +168,12 @@ let arith_rri64_rec i rd rs imm64 = { inst = arith_rri64_str i; write_locs = [Re let arith_rrr_rec i rd rs1 rs2 = { inst = arith_rrr_str i; write_locs = [Reg rd]; read_locs = [Reg rs1; Reg rs2]; imm = None; is_control = false} +let arith_arri32_rec i rd rs imm32 = { inst = "Pmaddiw"; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm32; is_control = false } + +let arith_arri64_rec i rd rs imm64 = { inst = "Pmaddil"; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm64; is_control = false } + +let arith_arrr_rec i rd rs1 rs2 = { inst = arith_arrr_str i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs1; Reg rs2]; imm = None; is_control = false} + let arith_rr_rec i rd rs = { inst = arith_rr_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = None; is_control = false} let arith_r_rec i rd = match i with @@ -173,6 +185,10 @@ let arith_rec i = | PArithRRI32 (i, rd, rs, imm32) -> arith_rri32_rec i (IR rd) (IR rs) (Some (I32 imm32)) | PArithRRI64 (i, rd, rs, imm64) -> arith_rri64_rec i (IR rd) (IR rs) (Some (I64 imm64)) | PArithRRR (i, rd, rs1, rs2) -> arith_rrr_rec i (IR rd) (IR rs1) (IR rs2) + (* Seems like single constant constructor types are elided *) + | PArithARRI32 ((* i,*) rd, rs, imm32) -> arith_arri32_rec () (IR rd) (IR rs) (Some (I32 imm32)) + | PArithARRI64 ((* i,*) rd, rs, imm64) -> arith_arri64_rec () (IR rd) (IR rs) (Some (I64 imm64)) + | PArithARRR (i, rd, rs1, rs2) -> arith_arrr_rec i (IR rd) (IR rs1) (IR rs2) | PArithRI32 (rd, imm32) -> { inst = arith_ri32_str; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I32 imm32)) ; is_control = false} | PArithRI64 (rd, imm64) -> { inst = arith_ri64_str; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I64 imm64)) ; is_control = false} | PArithRF32 (rd, f) -> { inst = arith_rf32_str; write_locs = [Reg (IR rd)]; read_locs = []; @@ -400,6 +416,7 @@ type real_instruction = | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd + | Maddw | Maddd | Make | Nop | Sxwd | Zxwd (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld @@ -423,8 +440,8 @@ let ab_inst_to_real = function | "Pcompl" | "Pcompil" -> Compd | "Pfcompw" -> Fcompw | "Pfcompl" -> Fcompd - | "Pmulw" -> Mulw - | "Pmull" -> Muld + | "Pmulw" | "Pmuliw" -> Mulw + | "Pmull" | "Pmulil" -> Muld | "Porw" | "Poriw" -> Orw | "Pnorw" | "Pnoriw" -> Norw | "Porl" | "Poril" -> Ord @@ -437,6 +454,7 @@ let ab_inst_to_real = function | "Psrll" | "Psrlil" -> Srld | "Psllw" | "Pslliw" -> Sllw | "Proriw" -> Rorw + | "Pmaddw" | "Pmaddiw" -> Maddw | "Pslll" | "Psllil" -> Slld | "Pxorw" | "Pxoriw" -> Xorw | "Pnxorw" | "Pnxoriw" -> Nxorw @@ -446,6 +464,7 @@ let ab_inst_to_real = function | "Pnxorl" | "Pnxoril" -> Nxord | "Pandnl" | "Pandnil" -> Andnd | "Pornl" | "Pornil" -> Ornd + | "Pmaddl" -> Maddd | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make | "Pnop" | "Pcvtw2l" -> Nop | "Psxwd" -> Sxwd @@ -507,11 +526,13 @@ let rec_to_usage r = (* I do not know yet in which context Ofslow can be used by CompCert *) and real_inst = ab_inst_to_real r.inst in match real_inst with - | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw | Andnw | Ornw -> + | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw + | Nxorw | Andnw | Ornw -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | _ -> raise InvalidEncoding) - | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord | Andnd | Ornd -> + | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord + | Nxord | Andnd | Ornd -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y) @@ -531,10 +552,10 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y | _ -> raise InvalidEncoding) - | Mulw -> (match encoding with None -> mau + | Mulw| Maddw -> (match encoding with None -> mau | Some U6 | Some S10 | Some U27L5 -> mau_x | _ -> raise InvalidEncoding) - | Muld -> (match encoding with None | Some U6 | Some S10 -> mau + | Muld | Maddd -> (match encoding with None | Some U6 | Some S10 -> mau | Some U27L5 | Some U27L10 -> mau_x | Some E27U27L10 -> mau_y) | Nop -> alu_nop @@ -567,7 +588,7 @@ let real_inst_to_latency = function | Sxwd | Zxwd | Fcompw | Fcompd -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 - | Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) + | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 3 | Sb | Sh | Sw | Sd -> 1 (* See k1c-Optimization.pdf page 19 *) | Get -> 1 diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v deleted file mode 100644 index edb07e5f..00000000 --- a/mppa_k1c/SelectOp.v +++ /dev/null @@ -1,1323 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* The contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) - -(** Instruction selection for operators *) - -(** The instruction selection pass recognizes opportunities for using - combined arithmetic and logical operations and addressing modes - offered by the target processor. For instance, the expression [x + 1] - can take advantage of the "immediate add" instruction of the processor, - and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned - into a "rotate and mask" instruction. - - This file defines functions for building CminorSel expressions and - statements, especially expressions consisting of operator - applications. These functions examine their arguments to choose - cheaper forms of operators whenever possible. - - For instance, [add e1 e2] will return a CminorSel expression semantically - equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a - [Oaddimm] operator if one of the arguments is an integer constant, - or suppress the addition altogether if one of the arguments is the - null integer. In passing, we perform operator reassociation - ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount - of constant propagation. - - On top of the "smart constructor" functions defined below, - module [Selection] implements the actual instruction selection pass. -*) - -Require Archi. -Require Import Coqlib. -Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. - -Local Open Scope cminorsel_scope. - -(** ** Constants **) - -Definition addrsymbol (id: ident) (ofs: ptrofs) := - Eop (Oaddrsymbol id ofs) Enil. - -Definition addrstack (ofs: ptrofs) := - Eop (Oaddrstack ofs) Enil. - -(** ** Integer addition and pointer addition *) - -(** Original definition: -<< -Nondetfunction addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else - match e with - | Eop (Ointconst m) Enil => Eop (Ointconst (Int.add n m)) Enil - | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil - | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil - | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | _ => Eop (Oaddimm n) (e ::: Enil) - end. ->> -*) - -Inductive addimm_cases: forall (e: expr), Type := - | addimm_case1: forall m, addimm_cases (Eop (Ointconst m) Enil) - | addimm_case2: forall s m, addimm_cases (Eop (Oaddrsymbol s m) Enil) - | addimm_case3: forall m, addimm_cases (Eop (Oaddrstack m) Enil) - | addimm_case4: forall m t, addimm_cases (Eop (Oaddimm m) (t ::: Enil)) - | addimm_default: forall (e: expr), addimm_cases e. - -Definition addimm_match (e: expr) := - match e as zz1 return addimm_cases zz1 with - | Eop (Ointconst m) Enil => addimm_case1 m - | Eop (Oaddrsymbol s m) Enil => addimm_case2 s m - | Eop (Oaddrstack m) Enil => addimm_case3 m - | Eop (Oaddimm m) (t ::: Enil) => addimm_case4 m t - | e => addimm_default e - end. - -Definition addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else match addimm_match e with - | addimm_case1 m => (* Eop (Ointconst m) Enil *) - Eop (Ointconst (Int.add n m)) Enil - | addimm_case2 s m => (* Eop (Oaddrsymbol s m) Enil *) - Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil - | addimm_case3 m => (* Eop (Oaddrstack m) Enil *) - Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil - | addimm_case4 m t => (* Eop (Oaddimm m) (t ::: Enil) *) - Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | addimm_default e => - Eop (Oaddimm n) (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction add (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 - | t1, Eop (Ointconst n2) Enil => addimm n2 t1 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil => - Eop Oadd (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n1) n2)) Enil ::: t1 ::: Enil) - | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => - Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil) - | Eop (Oaddimm n1) (t1:::Enil), t2 => - addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | t1, Eop (Oaddimm n2) (t2:::Enil) => - addimm n2 (Eop Oadd (t1:::t2:::Enil)) - | _, _ => Eop Oadd (e1:::e2:::Enil) - end. ->> -*) - -Inductive add_cases: forall (e1: expr) (e2: expr), Type := - | add_case1: forall n1 t2, add_cases (Eop (Ointconst n1) Enil) (t2) - | add_case2: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil) - | add_case3: forall n1 t1 n2 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) - | add_case4: forall n1 t1 n2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddrstack n2) Enil) - | add_case5: forall n1 n2 t2, add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil)) - | add_case6: forall n1 t1 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) - | add_case7: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) - | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2. - -Definition add_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return add_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => add_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => add_case2 t1 n2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => add_case3 n1 t1 n2 t2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil => add_case4 n1 t1 n2 - | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => add_case5 n1 n2 t2 - | Eop (Oaddimm n1) (t1:::Enil), t2 => add_case6 n1 t1 t2 - | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case7 t1 n2 t2 - | e1, e2 => add_default e1 e2 - end. - -Definition add (e1: expr) (e2: expr) := - match add_match e1 e2 with - | add_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - addimm n1 t2 - | add_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - addimm n2 t1 - | add_case3 n1 t1 n2 t2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) - | add_case4 n1 t1 n2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil *) - Eop Oadd (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n1) n2)) Enil ::: t1 ::: Enil) - | add_case5 n1 n2 t2 => (* Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) *) - Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil) - | add_case6 n1 t1 t2 => (* Eop (Oaddimm n1) (t1:::Enil), t2 *) - addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | add_case7 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) - addimm n2 (Eop Oadd (t1:::t2:::Enil)) - | add_default e1 e2 => - Eop Oadd (e1:::e2:::Enil) - end. - - -(** ** Integer and pointer subtraction *) - -(** Original definition: -<< -Nondetfunction sub (e1: expr) (e2: expr) := - match e1, e2 with - | t1, Eop (Ointconst n2) Enil => - addimm (Int.neg n2) t1 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) - | Eop (Oaddimm n1) (t1:::Enil), t2 => - addimm n1 (Eop Osub (t1:::t2:::Enil)) - | t1, Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) - | _, _ => Eop Osub (e1:::e2:::Enil) - end. ->> -*) - -Inductive sub_cases: forall (e1: expr) (e2: expr), Type := - | sub_case1: forall t1 n2, sub_cases (t1) (Eop (Ointconst n2) Enil) - | sub_case2: forall n1 t1 n2 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) - | sub_case3: forall n1 t1 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) - | sub_case4: forall t1 n2 t2, sub_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) - | sub_default: forall (e1: expr) (e2: expr), sub_cases e1 e2. - -Definition sub_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return sub_cases zz1 zz2 with - | t1, Eop (Ointconst n2) Enil => sub_case1 t1 n2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => sub_case2 n1 t1 n2 t2 - | Eop (Oaddimm n1) (t1:::Enil), t2 => sub_case3 n1 t1 t2 - | t1, Eop (Oaddimm n2) (t2:::Enil) => sub_case4 t1 n2 t2 - | e1, e2 => sub_default e1 e2 - end. - -Definition sub (e1: expr) (e2: expr) := - match sub_match e1 e2 with - | sub_case1 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - addimm (Int.neg n2) t1 - | sub_case2 n1 t1 n2 t2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) - | sub_case3 n1 t1 t2 => (* Eop (Oaddimm n1) (t1:::Enil), t2 *) - addimm n1 (Eop Osub (t1:::t2:::Enil)) - | sub_case4 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) - | sub_default e1 e2 => - Eop Osub (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction negint (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ointconst (Int.neg n)) Enil - | _ => Eop Oneg (e ::: Enil) - end. ->> -*) - -Inductive negint_cases: forall (e: expr), Type := - | negint_case1: forall n, negint_cases (Eop (Ointconst n) Enil) - | negint_default: forall (e: expr), negint_cases e. - -Definition negint_match (e: expr) := - match e as zz1 return negint_cases zz1 with - | Eop (Ointconst n) Enil => negint_case1 n - | e => negint_default e - end. - -Definition negint (e: expr) := - match negint_match e with - | negint_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.neg n)) Enil - | negint_default e => - Eop Oneg (e ::: Enil) - end. - - -(** ** Immediate shifts *) - -(** Original definition: -<< -Nondetfunction shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst (Int.shl n1 n)) Enil - | Eop (Oshlimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshlimm n) (e1:::Enil) - | _ => - Eop (Oshlimm n) (e1:::Enil) - end. ->> -*) - -Inductive shlimm_cases: forall (e1: expr) , Type := - | shlimm_case1: forall n1, shlimm_cases (Eop (Ointconst n1) Enil) - | shlimm_case2: forall n1 t1, shlimm_cases (Eop (Oshlimm n1) (t1:::Enil)) - | shlimm_default: forall (e1: expr) , shlimm_cases e1. - -Definition shlimm_match (e1: expr) := - match e1 as zz1 return shlimm_cases zz1 with - | Eop (Ointconst n1) Enil => shlimm_case1 n1 - | Eop (Oshlimm n1) (t1:::Enil) => shlimm_case2 n1 t1 - | e1 => shlimm_default e1 - end. - -Definition shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shlimm_match e1 with - | shlimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst (Int.shl n1 n)) Enil - | shlimm_case2 n1 t1 => (* Eop (Oshlimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil) - | shlimm_default e1 => - Eop (Oshlimm n) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst (Int.shru n1 n)) Enil - | Eop (Oshruimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshruimm n) (e1:::Enil) - | _ => - Eop (Oshruimm n) (e1:::Enil) - end. ->> -*) - -Inductive shruimm_cases: forall (e1: expr) , Type := - | shruimm_case1: forall n1, shruimm_cases (Eop (Ointconst n1) Enil) - | shruimm_case2: forall n1 t1, shruimm_cases (Eop (Oshruimm n1) (t1:::Enil)) - | shruimm_default: forall (e1: expr) , shruimm_cases e1. - -Definition shruimm_match (e1: expr) := - match e1 as zz1 return shruimm_cases zz1 with - | Eop (Ointconst n1) Enil => shruimm_case1 n1 - | Eop (Oshruimm n1) (t1:::Enil) => shruimm_case2 n1 t1 - | e1 => shruimm_default e1 - end. - -Definition shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shruimm_match e1 with - | shruimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst (Int.shru n1 n)) Enil - | shruimm_case2 n1 t1 => (* Eop (Oshruimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil) - | shruimm_default e1 => - Eop (Oshruimm n) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst (Int.shr n1 n)) Enil - | Eop (Oshrimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshrimm n) (e1:::Enil) - | _ => - Eop (Oshrimm n) (e1:::Enil) - end. ->> -*) - -Inductive shrimm_cases: forall (e1: expr) , Type := - | shrimm_case1: forall n1, shrimm_cases (Eop (Ointconst n1) Enil) - | shrimm_case2: forall n1 t1, shrimm_cases (Eop (Oshrimm n1) (t1:::Enil)) - | shrimm_default: forall (e1: expr) , shrimm_cases e1. - -Definition shrimm_match (e1: expr) := - match e1 as zz1 return shrimm_cases zz1 with - | Eop (Ointconst n1) Enil => shrimm_case1 n1 - | Eop (Oshrimm n1) (t1:::Enil) => shrimm_case2 n1 t1 - | e1 => shrimm_default e1 - end. - -Definition shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shrimm_match e1 with - | shrimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst (Int.shr n1 n)) Enil - | shrimm_case2 n1 t1 => (* Eop (Oshrimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil) - | shrimm_default e1 => - Eop (Oshrimm n) (e1:::Enil) - end. - - -(** ** Integer multiply *) - -Definition mulimm_base (n1: int) (e2: expr) := - match Int.one_bits n1 with - | i :: nil => - shlimm e2 i - | i :: j :: nil => - Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) - | _ => - Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) - end. - -(** Original definition: -<< -Nondetfunction mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.one then e2 - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.mul n1 n2)) Enil - | Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2) - | _ => mulimm_base n1 e2 - end. ->> -*) - -Inductive mulimm_cases: forall (e2: expr), Type := - | mulimm_case1: forall n2, mulimm_cases (Eop (Ointconst n2) Enil) - | mulimm_case2: forall n2 t2, mulimm_cases (Eop (Oaddimm n2) (t2:::Enil)) - | mulimm_default: forall (e2: expr), mulimm_cases e2. - -Definition mulimm_match (e2: expr) := - match e2 as zz1 return mulimm_cases zz1 with - | Eop (Ointconst n2) Enil => mulimm_case1 n2 - | Eop (Oaddimm n2) (t2:::Enil) => mulimm_case2 n2 t2 - | e2 => mulimm_default e2 - end. - -Definition mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.one then e2 else match mulimm_match e2 with - | mulimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.mul n1 n2)) Enil - | mulimm_case2 n2 t2 => (* Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.mul n1 n2) (mulimm_base n1 t2) - | mulimm_default e2 => - mulimm_base n1 e2 - end. - - -(** Original definition: -<< -Nondetfunction mul (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2 - | t1, Eop (Ointconst n2) Enil => mulimm n2 t1 - | _, _ => Eop Omul (e1:::e2:::Enil) - end. ->> -*) - -Inductive mul_cases: forall (e1: expr) (e2: expr), Type := - | mul_case1: forall n1 t2, mul_cases (Eop (Ointconst n1) Enil) (t2) - | mul_case2: forall t1 n2, mul_cases (t1) (Eop (Ointconst n2) Enil) - | mul_default: forall (e1: expr) (e2: expr), mul_cases e1 e2. - -Definition mul_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return mul_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => mul_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => mul_case2 t1 n2 - | e1, e2 => mul_default e1 e2 - end. - -Definition mul (e1: expr) (e2: expr) := - match mul_match e1 e2 with - | mul_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - mulimm n1 t2 - | mul_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - mulimm n2 t1 - | mul_default e1 e2 => - Eop Omul (e1:::e2:::Enil) - end. - - -Definition mulhs (e1: expr) (e2: expr) := - if Archi.ptr64 then - Eop Olowlong - (Eop (Oshrlimm (Int.repr 32)) - (Eop Omull (Eop Ocast32signed (e1 ::: Enil) ::: - Eop Ocast32signed (e2 ::: Enil) ::: Enil) ::: Enil) - ::: Enil) - else - Eop Omulhs (e1 ::: e2 ::: Enil). - -Definition mulhu (e1: expr) (e2: expr) := - if Archi.ptr64 then - Eop Olowlong - (Eop (Oshrluimm (Int.repr 32)) - (Eop Omull (Eop Ocast32unsigned (e1 ::: Enil) ::: - Eop Ocast32unsigned (e2 ::: Enil) ::: Enil) ::: Enil) - ::: Enil) - else - Eop Omulhu (e1 ::: e2 ::: Enil). - -(** ** Bitwise and, or, xor *) - -(** Original definition: -<< -Nondetfunction andimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.mone then e2 - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.and n1 n2)) Enil - | Eop (Oandimm n2) (t2:::Enil) => Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) - | Eop Onot (t2:::Enil) => Eop (Oandnimm n1) (t2:::Enil) - | _ => Eop (Oandimm n1) (e2:::Enil) - end. ->> -*) - -Inductive andimm_cases: forall (e2: expr), Type := - | andimm_case1: forall n2, andimm_cases (Eop (Ointconst n2) Enil) - | andimm_case2: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil)) - | andimm_case3: forall t2, andimm_cases (Eop Onot (t2:::Enil)) - | andimm_default: forall (e2: expr), andimm_cases e2. - -Definition andimm_match (e2: expr) := - match e2 as zz1 return andimm_cases zz1 with - | Eop (Ointconst n2) Enil => andimm_case1 n2 - | Eop (Oandimm n2) (t2:::Enil) => andimm_case2 n2 t2 - | Eop Onot (t2:::Enil) => andimm_case3 t2 - | e2 => andimm_default e2 - end. - -Definition andimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match andimm_match e2 with - | andimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.and n1 n2)) Enil - | andimm_case2 n2 t2 => (* Eop (Oandimm n2) (t2:::Enil) *) - Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) - | andimm_case3 t2 => (* Eop Onot (t2:::Enil) *) - Eop (Oandnimm n1) (t2:::Enil) - | andimm_default e2 => - Eop (Oandimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction and (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => andimm n1 t2 - | t1, Eop (Ointconst n2) Enil => andimm n2 t1 - | (Eop Onot (t1:::Enil)), t2 => Eop Oandn (t1:::t2:::Enil) - | t1, (Eop Onot (t2:::Enil)) => Eop Oandn (t2:::t1:::Enil) - | _, _ => Eop Oand (e1:::e2:::Enil) - end. ->> -*) - -Inductive and_cases: forall (e1: expr) (e2: expr), Type := - | and_case1: forall n1 t2, and_cases (Eop (Ointconst n1) Enil) (t2) - | and_case2: forall t1 n2, and_cases (t1) (Eop (Ointconst n2) Enil) - | and_case3: forall t1 t2, and_cases ((Eop Onot (t1:::Enil))) (t2) - | and_case4: forall t1 t2, and_cases (t1) ((Eop Onot (t2:::Enil))) - | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2. - -Definition and_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return and_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => and_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => and_case2 t1 n2 - | (Eop Onot (t1:::Enil)), t2 => and_case3 t1 t2 - | t1, (Eop Onot (t2:::Enil)) => and_case4 t1 t2 - | e1, e2 => and_default e1 e2 - end. - -Definition and (e1: expr) (e2: expr) := - match and_match e1 e2 with - | and_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - andimm n1 t2 - | and_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - andimm n2 t1 - | and_case3 t1 t2 => (* (Eop Onot (t1:::Enil)), t2 *) - Eop Oandn (t1:::t2:::Enil) - | and_case4 t1 t2 => (* t1, (Eop Onot (t2:::Enil)) *) - Eop Oandn (t2:::t1:::Enil) - | and_default e1 e2 => - Eop Oand (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction orimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 - else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil - | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) - | Eop Onot (t2:::Enil) => Eop (Oornimm n1) (t2:::Enil) - | _ => Eop (Oorimm n1) (e2:::Enil) - end. ->> -*) - -Inductive orimm_cases: forall (e2: expr), Type := - | orimm_case1: forall n2, orimm_cases (Eop (Ointconst n2) Enil) - | orimm_case2: forall n2 t2, orimm_cases (Eop (Oorimm n2) (t2:::Enil)) - | orimm_case3: forall t2, orimm_cases (Eop Onot (t2:::Enil)) - | orimm_default: forall (e2: expr), orimm_cases e2. - -Definition orimm_match (e2: expr) := - match e2 as zz1 return orimm_cases zz1 with - | Eop (Ointconst n2) Enil => orimm_case1 n2 - | Eop (Oorimm n2) (t2:::Enil) => orimm_case2 n2 t2 - | Eop Onot (t2:::Enil) => orimm_case3 t2 - | e2 => orimm_default e2 - end. - -Definition orimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match e2 with - | orimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.or n1 n2)) Enil - | orimm_case2 n2 t2 => (* Eop (Oorimm n2) (t2:::Enil) *) - Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) - | orimm_case3 t2 => (* Eop Onot (t2:::Enil) *) - Eop (Oornimm n1) (t2:::Enil) - | orimm_default e2 => - Eop (Oorimm n1) (e2:::Enil) - end. - - -Definition same_expr_pure (e1 e2: expr) := - match e1, e2 with - | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false - | _, _ => false - end. - -(** Original definition: -<< -Nondetfunction or (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => orimm n1 t2 - | t1, Eop (Ointconst n2) Enil => orimm n2 t1 - | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 - then Eop (Ororimm n2) (t1:::Enil) - else Eop Oor (e1:::e2:::Enil) - | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 - then Eop (Ororimm n2) (t1:::Enil) - else Eop Oor (e1:::e2:::Enil) - | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) - | t1, (Eop Onot (t2:::Enil)) => Eop Oorn (t2:::t1:::Enil) - | _, _ => Eop Oor (e1:::e2:::Enil) - end. ->> -*) - -Inductive or_cases: forall (e1: expr) (e2: expr), Type := - | or_case1: forall n1 t2, or_cases (Eop (Ointconst n1) Enil) (t2) - | or_case2: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil) - | or_case3: forall n1 t1 n2 t2, or_cases (Eop (Oshlimm n1) (t1:::Enil)) (Eop (Oshruimm n2) (t2:::Enil)) - | or_case4: forall n2 t2 n1 t1, or_cases (Eop (Oshruimm n2) (t2:::Enil)) (Eop (Oshlimm n1) (t1:::Enil)) - | or_case5: forall t1 t2, or_cases ((Eop Onot (t1:::Enil))) (t2) - | or_case6: forall t1 t2, or_cases (t1) ((Eop Onot (t2:::Enil))) - | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2. - -Definition or_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return or_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => or_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => or_case2 t1 n2 - | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => or_case3 n1 t1 n2 t2 - | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => or_case4 n2 t2 n1 t1 - | (Eop Onot (t1:::Enil)), t2 => or_case5 t1 t2 - | t1, (Eop Onot (t2:::Enil)) => or_case6 t1 t2 - | e1, e2 => or_default e1 e2 - end. - -Definition or (e1: expr) (e2: expr) := - match or_match e1 e2 with - | or_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - orimm n1 t2 - | or_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - orimm n2 t1 - | or_case3 n1 t1 n2 t2 => (* Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) *) - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil) - | or_case4 n2 t2 n1 t1 => (* Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) *) - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil) - | or_case5 t1 t2 => (* (Eop Onot (t1:::Enil)), t2 *) - Eop Oorn (t1:::t2:::Enil) - | or_case6 t1 t2 => (* t1, (Eop Onot (t2:::Enil)) *) - Eop Oorn (t2:::t1:::Enil) - | or_default e1 e2 => - Eop Oor (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else - match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil - | Eop (Oxorimm n2) (t2:::Enil) => - let n := Int.xor n1 n2 in - if Int.eq n Int.zero then t2 else Eop (Oxorimm n) (t2:::Enil) - | _ => Eop (Oxorimm n1) (e2:::Enil) - end. ->> -*) - -Inductive xorimm_cases: forall (e2: expr), Type := - | xorimm_case1: forall n2, xorimm_cases (Eop (Ointconst n2) Enil) - | xorimm_case2: forall n2 t2, xorimm_cases (Eop (Oxorimm n2) (t2:::Enil)) - | xorimm_default: forall (e2: expr), xorimm_cases e2. - -Definition xorimm_match (e2: expr) := - match e2 as zz1 return xorimm_cases zz1 with - | Eop (Ointconst n2) Enil => xorimm_case1 n2 - | Eop (Oxorimm n2) (t2:::Enil) => xorimm_case2 n2 t2 - | e2 => xorimm_default e2 - end. - -Definition xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else match xorimm_match e2 with - | xorimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.xor n1 n2)) Enil - | xorimm_case2 n2 t2 => (* Eop (Oxorimm n2) (t2:::Enil) *) - let n := Int.xor n1 n2 in if Int.eq n Int.zero then t2 else Eop (Oxorimm n) (t2:::Enil) - | xorimm_default e2 => - Eop (Oxorimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xor (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2 - | t1, Eop (Ointconst n2) Enil => xorimm n2 t1 - | _, _ => Eop Oxor (e1:::e2:::Enil) - end. ->> -*) - -Inductive xor_cases: forall (e1: expr) (e2: expr), Type := - | xor_case1: forall n1 t2, xor_cases (Eop (Ointconst n1) Enil) (t2) - | xor_case2: forall t1 n2, xor_cases (t1) (Eop (Ointconst n2) Enil) - | xor_default: forall (e1: expr) (e2: expr), xor_cases e1 e2. - -Definition xor_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return xor_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => xor_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => xor_case2 t1 n2 - | e1, e2 => xor_default e1 e2 - end. - -Definition xor (e1: expr) (e2: expr) := - match xor_match e1 e2 with - | xor_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - xorimm n1 t2 - | xor_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - xorimm n2 t1 - | xor_default e1 e2 => - Eop Oxor (e1:::e2:::Enil) - end. - - -(** ** Integer logical negation *) - -(** Original definition: -<< -Nondetfunction notint (e: expr) := - match e with - | Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil) - | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil) - | Eop Oor (e1:::e2:::Enil) => Eop Onor (e1:::e2:::Enil) - | Eop (Oorimm n) (e1:::Enil) => Eop (Onorimm n) (e1:::Enil) - | Eop Oxor (e1:::e2:::Enil) => Eop Onxor (e1:::e2:::Enil) - | Eop (Oxorimm n) (e1:::Enil) => Eop (Onxorimm n) (e1:::Enil) - | _ => Eop Onot (e:::Enil) - end. ->> -*) - -Inductive notint_cases: forall (e: expr), Type := - | notint_case1: forall e1 e2, notint_cases (Eop Oand (e1:::e2:::Enil)) - | notint_case2: forall n e1, notint_cases (Eop (Oandimm n) (e1:::Enil)) - | notint_case3: forall e1 e2, notint_cases (Eop Oor (e1:::e2:::Enil)) - | notint_case4: forall n e1, notint_cases (Eop (Oorimm n) (e1:::Enil)) - | notint_case5: forall e1 e2, notint_cases (Eop Oxor (e1:::e2:::Enil)) - | notint_case6: forall n e1, notint_cases (Eop (Oxorimm n) (e1:::Enil)) - | notint_default: forall (e: expr), notint_cases e. - -Definition notint_match (e: expr) := - match e as zz1 return notint_cases zz1 with - | Eop Oand (e1:::e2:::Enil) => notint_case1 e1 e2 - | Eop (Oandimm n) (e1:::Enil) => notint_case2 n e1 - | Eop Oor (e1:::e2:::Enil) => notint_case3 e1 e2 - | Eop (Oorimm n) (e1:::Enil) => notint_case4 n e1 - | Eop Oxor (e1:::e2:::Enil) => notint_case5 e1 e2 - | Eop (Oxorimm n) (e1:::Enil) => notint_case6 n e1 - | e => notint_default e - end. - -Definition notint (e: expr) := - match notint_match e with - | notint_case1 e1 e2 => (* Eop Oand (e1:::e2:::Enil) *) - Eop Onand (e1:::e2:::Enil) - | notint_case2 n e1 => (* Eop (Oandimm n) (e1:::Enil) *) - Eop (Onandimm n) (e1:::Enil) - | notint_case3 e1 e2 => (* Eop Oor (e1:::e2:::Enil) *) - Eop Onor (e1:::e2:::Enil) - | notint_case4 n e1 => (* Eop (Oorimm n) (e1:::Enil) *) - Eop (Onorimm n) (e1:::Enil) - | notint_case5 e1 e2 => (* Eop Oxor (e1:::e2:::Enil) *) - Eop Onxor (e1:::e2:::Enil) - | notint_case6 n e1 => (* Eop (Oxorimm n) (e1:::Enil) *) - Eop (Onxorimm n) (e1:::Enil) - | notint_default e => - Eop Onot (e:::Enil) - end. - - -(** ** Integer division and modulus *) - -Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). -Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil). -Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). -Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil). - -Definition shrximm (e1: expr) (n2: int) := - if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil). - -(* Alternate definition, not convenient for strength reduction during constant propagation *) -(* -(* n2 will be less than 31. *) - -Definition shrximm_inner (e1: expr) (n2: int) := - Eop (Oshruimm (Int.sub Int.iwordsize n2)) - ((Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) - (e1 ::: Enil)) - ::: Enil). - -Definition shrximm (e1: expr) (n2: int) := - if Int.eq n2 Int.zero then e1 - else Eop (Oshrimm n2) - ((Eop Oadd (e1 ::: shrximm_inner e1 n2 ::: Enil)) - ::: Enil). -*) - -(** ** General shifts *) - -(** Original definition: -<< -Nondetfunction shl (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shlimm e1 n2 - | _ => Eop Oshl (e1:::e2:::Enil) - end. ->> -*) - -Inductive shl_cases: forall (e2: expr), Type := - | shl_case1: forall n2, shl_cases (Eop (Ointconst n2) Enil) - | shl_default: forall (e2: expr), shl_cases e2. - -Definition shl_match (e2: expr) := - match e2 as zz1 return shl_cases zz1 with - | Eop (Ointconst n2) Enil => shl_case1 n2 - | e2 => shl_default e2 - end. - -Definition shl (e1: expr) (e2: expr) := - match shl_match e2 with - | shl_case1 n2 => (* Eop (Ointconst n2) Enil *) - shlimm e1 n2 - | shl_default e2 => - Eop Oshl (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shr (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shrimm e1 n2 - | _ => Eop Oshr (e1:::e2:::Enil) - end. ->> -*) - -Inductive shr_cases: forall (e2: expr), Type := - | shr_case1: forall n2, shr_cases (Eop (Ointconst n2) Enil) - | shr_default: forall (e2: expr), shr_cases e2. - -Definition shr_match (e2: expr) := - match e2 as zz1 return shr_cases zz1 with - | Eop (Ointconst n2) Enil => shr_case1 n2 - | e2 => shr_default e2 - end. - -Definition shr (e1: expr) (e2: expr) := - match shr_match e2 with - | shr_case1 n2 => (* Eop (Ointconst n2) Enil *) - shrimm e1 n2 - | shr_default e2 => - Eop Oshr (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shru (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shruimm e1 n2 - | _ => Eop Oshru (e1:::e2:::Enil) - end. ->> -*) - -Inductive shru_cases: forall (e2: expr), Type := - | shru_case1: forall n2, shru_cases (Eop (Ointconst n2) Enil) - | shru_default: forall (e2: expr), shru_cases e2. - -Definition shru_match (e2: expr) := - match e2 as zz1 return shru_cases zz1 with - | Eop (Ointconst n2) Enil => shru_case1 n2 - | e2 => shru_default e2 - end. - -Definition shru (e1: expr) (e2: expr) := - match shru_match e2 with - | shru_case1 n2 => (* Eop (Ointconst n2) Enil *) - shruimm e1 n2 - | shru_default e2 => - Eop Oshru (e1:::e2:::Enil) - end. - - -(** ** Floating-point arithmetic *) - -Definition negf (e: expr) := Eop Onegf (e ::: Enil). -Definition absf (e: expr) := Eop Oabsf (e ::: Enil). -Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). -Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). -Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). - -Definition negfs (e: expr) := Eop Onegfs (e ::: Enil). -Definition absfs (e: expr) := Eop Oabsfs (e ::: Enil). -Definition addfs (e1 e2: expr) := Eop Oaddfs (e1 ::: e2 ::: Enil). -Definition subfs (e1 e2: expr) := Eop Osubfs (e1 ::: e2 ::: Enil). -Definition mulfs (e1 e2: expr) := Eop Omulfs (e1 ::: e2 ::: Enil). - -(** ** Comparisons *) - -(** Original definition: -<< -Nondetfunction compimm (default: comparison -> int -> condition) - (sem: comparison -> int -> int -> bool) - (c: comparison) (e1: expr) (n2: int) := - match c, e1 with - | c, Eop (Ointconst n1) Enil => - Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil - | Ceq, Eop (Ocmp c) el => - if Int.eq_dec n2 Int.zero then - Eop (Ocmp (negate_condition c)) el - else if Int.eq_dec n2 Int.one then - Eop (Ocmp c) el - else - Eop (Ointconst Int.zero) Enil - | Cne, Eop (Ocmp c) el => - if Int.eq_dec n2 Int.zero then - Eop (Ocmp c) el - else if Int.eq_dec n2 Int.one then - Eop (Ocmp (negate_condition c)) el - else - Eop (Ointconst Int.one) Enil - | _, _ => - Eop (Ocmp (default c n2)) (e1 ::: Enil) - end. ->> -*) - -Inductive compimm_cases: forall (c: comparison) (e1: expr) , Type := - | compimm_case1: forall c n1, compimm_cases (c) (Eop (Ointconst n1) Enil) - | compimm_case2: forall c el, compimm_cases (Ceq) (Eop (Ocmp c) el) - | compimm_case3: forall c el, compimm_cases (Cne) (Eop (Ocmp c) el) - | compimm_default: forall (c: comparison) (e1: expr) , compimm_cases c e1. - -Definition compimm_match (c: comparison) (e1: expr) := - match c as zz1, e1 as zz2 return compimm_cases zz1 zz2 with - | c, Eop (Ointconst n1) Enil => compimm_case1 c n1 - | Ceq, Eop (Ocmp c) el => compimm_case2 c el - | Cne, Eop (Ocmp c) el => compimm_case3 c el - | c, e1 => compimm_default c e1 - end. - -Definition compimm (default: comparison -> int -> condition) (sem: comparison -> int -> int -> bool) (c: comparison) (e1: expr) (n2: int) := - match compimm_match c e1 with - | compimm_case1 c n1 => (* c, Eop (Ointconst n1) Enil *) - Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil - | compimm_case2 c el => (* Ceq, Eop (Ocmp c) el *) - if Int.eq_dec n2 Int.zero then Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el else Eop (Ointconst Int.zero) Enil - | compimm_case3 c el => (* Cne, Eop (Ocmp c) el *) - if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el else Eop (Ointconst Int.one) Enil - | compimm_default c e1 => - Eop (Ocmp (default c n2)) (e1 ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => - compimm Ccompimm Int.cmp (swap_comparison c) t2 n1 - | t1, Eop (Ointconst n2) Enil => - compimm Ccompimm Int.cmp c t1 n2 - | _, _ => - Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) - end. ->> -*) - -Inductive comp_cases: forall (e1: expr) (e2: expr), Type := - | comp_case1: forall n1 t2, comp_cases (Eop (Ointconst n1) Enil) (t2) - | comp_case2: forall t1 n2, comp_cases (t1) (Eop (Ointconst n2) Enil) - | comp_default: forall (e1: expr) (e2: expr), comp_cases e1 e2. - -Definition comp_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return comp_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => comp_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => comp_case2 t1 n2 - | e1, e2 => comp_default e1 e2 - end. - -Definition comp (c: comparison) (e1: expr) (e2: expr) := - match comp_match e1 e2 with - | comp_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - compimm Ccompimm Int.cmp (swap_comparison c) t2 n1 - | comp_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - compimm Ccompimm Int.cmp c t1 n2 - | comp_default e1 e2 => - Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => - compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1 - | t1, Eop (Ointconst n2) Enil => - compimm Ccompuimm Int.cmpu c t1 n2 - | _, _ => - Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) - end. ->> -*) - -Inductive compu_cases: forall (e1: expr) (e2: expr), Type := - | compu_case1: forall n1 t2, compu_cases (Eop (Ointconst n1) Enil) (t2) - | compu_case2: forall t1 n2, compu_cases (t1) (Eop (Ointconst n2) Enil) - | compu_default: forall (e1: expr) (e2: expr), compu_cases e1 e2. - -Definition compu_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return compu_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => compu_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => compu_case2 t1 n2 - | e1, e2 => compu_default e1 e2 - end. - -Definition compu (c: comparison) (e1: expr) (e2: expr) := - match compu_match e1 e2 with - | compu_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1 - | compu_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - compimm Ccompuimm Int.cmpu c t1 n2 - | compu_default e1 e2 => - Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) - end. - - -Definition compf (c: comparison) (e1: expr) (e2: expr) := - Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). - -Definition compfs (c: comparison) (e1: expr) (e2: expr) := - Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). - -(** ** Integer conversions *) - -Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. - -(** Original definition: -<< -Nondetfunction cast8signed (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil - | _ => Eop Ocast8signed (e ::: Enil) - end. ->> -*) - -Inductive cast8signed_cases: forall (e: expr), Type := - | cast8signed_case1: forall n, cast8signed_cases (Eop (Ointconst n) Enil) - | cast8signed_default: forall (e: expr), cast8signed_cases e. - -Definition cast8signed_match (e: expr) := - match e as zz1 return cast8signed_cases zz1 with - | Eop (Ointconst n) Enil => cast8signed_case1 n - | e => cast8signed_default e - end. - -Definition cast8signed (e: expr) := - match cast8signed_match e with - | cast8signed_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.sign_ext 8 n)) Enil - | cast8signed_default e => - Eop Ocast8signed (e ::: Enil) - end. - - -Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e. - -(** Original definition: -<< -Nondetfunction cast16signed (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil - | _ => Eop Ocast16signed (e ::: Enil) - end. ->> -*) - -Inductive cast16signed_cases: forall (e: expr), Type := - | cast16signed_case1: forall n, cast16signed_cases (Eop (Ointconst n) Enil) - | cast16signed_default: forall (e: expr), cast16signed_cases e. - -Definition cast16signed_match (e: expr) := - match e as zz1 return cast16signed_cases zz1 with - | Eop (Ointconst n) Enil => cast16signed_case1 n - | e => cast16signed_default e - end. - -Definition cast16signed (e: expr) := - match cast16signed_match e with - | cast16signed_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.sign_ext 16 n)) Enil - | cast16signed_default e => - Eop Ocast16signed (e ::: Enil) - end. - - -(** ** Floating-point conversions *) - -Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). -Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). - -(** Original definition: -<< -Nondetfunction floatofintu (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil - | _ => Eop Ofloatofintu (e ::: Enil) - end. ->> -*) - -Inductive floatofintu_cases: forall (e: expr), Type := - | floatofintu_case1: forall n, floatofintu_cases (Eop (Ointconst n) Enil) - | floatofintu_default: forall (e: expr), floatofintu_cases e. - -Definition floatofintu_match (e: expr) := - match e as zz1 return floatofintu_cases zz1 with - | Eop (Ointconst n) Enil => floatofintu_case1 n - | e => floatofintu_default e - end. - -Definition floatofintu (e: expr) := - match floatofintu_match e with - | floatofintu_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ofloatconst (Float.of_intu n)) Enil - | floatofintu_default e => - Eop Ofloatofintu (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction floatofint (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil - | _ => Eop Ofloatofint (e ::: Enil) - end. ->> -*) - -Inductive floatofint_cases: forall (e: expr), Type := - | floatofint_case1: forall n, floatofint_cases (Eop (Ointconst n) Enil) - | floatofint_default: forall (e: expr), floatofint_cases e. - -Definition floatofint_match (e: expr) := - match e as zz1 return floatofint_cases zz1 with - | Eop (Ointconst n) Enil => floatofint_case1 n - | e => floatofint_default e - end. - -Definition floatofint (e: expr) := - match floatofint_match e with - | floatofint_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ofloatconst (Float.of_int n)) Enil - | floatofint_default e => - Eop Ofloatofint (e ::: Enil) - end. - - -Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil). -Definition singleofint (e: expr) := Eop Osingleofint (e ::: Enil). - -Definition intuofsingle (e: expr) := Eop Ointuofsingle (e ::: Enil). -Definition singleofintu (e: expr) := Eop Osingleofintu (e ::: Enil). - -Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). -Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). - -(** ** Recognition of addressing modes for load and store operations *) - -(** Original definition: -<< -Nondetfunction addressing (chunk: memory_chunk) (e: expr) := - match e with - | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) - | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil) - | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil) - | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil) - | _ => (Aindexed Ptrofs.zero, e:::Enil) - end. ->> -*) - -Inductive addressing_cases: forall (e: expr), Type := - | addressing_case1: forall n, addressing_cases (Eop (Oaddrstack n) Enil) - | addressing_case2: forall id ofs, addressing_cases (Eop (Oaddrsymbol id ofs) Enil) - | addressing_case3: forall n e1, addressing_cases (Eop (Oaddimm n) (e1:::Enil)) - | addressing_case4: forall n e1, addressing_cases (Eop (Oaddlimm n) (e1:::Enil)) - | addressing_default: forall (e: expr), addressing_cases e. - -Definition addressing_match (e: expr) := - match e as zz1 return addressing_cases zz1 with - | Eop (Oaddrstack n) Enil => addressing_case1 n - | Eop (Oaddrsymbol id ofs) Enil => addressing_case2 id ofs - | Eop (Oaddimm n) (e1:::Enil) => addressing_case3 n e1 - | Eop (Oaddlimm n) (e1:::Enil) => addressing_case4 n e1 - | e => addressing_default e - end. - -Definition addressing (chunk: memory_chunk) (e: expr) := - match addressing_match e with - | addressing_case1 n => (* Eop (Oaddrstack n) Enil *) - (Ainstack n, Enil) - | addressing_case2 id ofs => (* Eop (Oaddrsymbol id ofs) Enil *) - if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil) - | addressing_case3 n e1 => (* Eop (Oaddimm n) (e1:::Enil) *) - (Aindexed (Ptrofs.of_int n), e1:::Enil) - | addressing_case4 n e1 => (* Eop (Oaddlimm n) (e1:::Enil) *) - (Aindexed (Ptrofs.of_int64 n), e1:::Enil) - | addressing_default e => - (Aindexed Ptrofs.zero, e:::Enil) - end. - - -(** ** Arguments of builtins *) - -(** Original definition: -<< -Nondetfunction builtin_arg (e: expr) := - match e with - | Eop (Ointconst n) Enil => BA_int n - | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs - | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs - | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => - BA_long (Int64.ofwords h l) - | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) - | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs - | Eop (Oaddimm n) (e1:::Enil) => - if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n) - | Eop (Oaddlimm n) (e1:::Enil) => - if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e - | _ => BA e - end. ->> -*) - -Inductive builtin_arg_cases: forall (e: expr), Type := - | builtin_arg_case1: forall n, builtin_arg_cases (Eop (Ointconst n) Enil) - | builtin_arg_case2: forall id ofs, builtin_arg_cases (Eop (Oaddrsymbol id ofs) Enil) - | builtin_arg_case3: forall ofs, builtin_arg_cases (Eop (Oaddrstack ofs) Enil) - | builtin_arg_case4: forall h l, builtin_arg_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil)) - | builtin_arg_case5: forall h l, builtin_arg_cases (Eop Omakelong (h ::: l ::: Enil)) - | builtin_arg_case6: forall chunk ofs, builtin_arg_cases (Eload chunk (Ainstack ofs) Enil) - | builtin_arg_case7: forall n e1, builtin_arg_cases (Eop (Oaddimm n) (e1:::Enil)) - | builtin_arg_case8: forall n e1, builtin_arg_cases (Eop (Oaddlimm n) (e1:::Enil)) - | builtin_arg_default: forall (e: expr), builtin_arg_cases e. - -Definition builtin_arg_match (e: expr) := - match e as zz1 return builtin_arg_cases zz1 with - | Eop (Ointconst n) Enil => builtin_arg_case1 n - | Eop (Oaddrsymbol id ofs) Enil => builtin_arg_case2 id ofs - | Eop (Oaddrstack ofs) Enil => builtin_arg_case3 ofs - | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => builtin_arg_case4 h l - | Eop Omakelong (h ::: l ::: Enil) => builtin_arg_case5 h l - | Eload chunk (Ainstack ofs) Enil => builtin_arg_case6 chunk ofs - | Eop (Oaddimm n) (e1:::Enil) => builtin_arg_case7 n e1 - | Eop (Oaddlimm n) (e1:::Enil) => builtin_arg_case8 n e1 - | e => builtin_arg_default e - end. - -Definition builtin_arg (e: expr) := - match builtin_arg_match e with - | builtin_arg_case1 n => (* Eop (Ointconst n) Enil *) - BA_int n - | builtin_arg_case2 id ofs => (* Eop (Oaddrsymbol id ofs) Enil *) - BA_addrglobal id ofs - | builtin_arg_case3 ofs => (* Eop (Oaddrstack ofs) Enil *) - BA_addrstack ofs - | builtin_arg_case4 h l => (* Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) *) - BA_long (Int64.ofwords h l) - | builtin_arg_case5 h l => (* Eop Omakelong (h ::: l ::: Enil) *) - BA_splitlong (BA h) (BA l) - | builtin_arg_case6 chunk ofs => (* Eload chunk (Ainstack ofs) Enil *) - BA_loadstack chunk ofs - | builtin_arg_case7 n e1 => (* Eop (Oaddimm n) (e1:::Enil) *) - if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n) - | builtin_arg_case8 n e1 => (* Eop (Oaddlimm n) (e1:::Enil) *) - if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e - | builtin_arg_default e => - BA e - end. - diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 7ec694e2..e4d65ced 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -86,6 +86,14 @@ Nondetfunction add (e1: expr) (e2: expr) := addimm n1 (Eop Oadd (t1:::t2:::Enil)) | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | t1, (Eop Omul (t2:::t3:::Enil)) => + Eop Omadd (t1:::t2:::t3:::Enil) + | (Eop Omul (t2:::t3:::Enil)), t1 => + Eop Omadd (t1:::t2:::t3:::Enil) + | t1, (Eop (Omulimm n) (t2:::Enil)) => + Eop (Omaddimm n) (t1:::t2:::Enil) + | (Eop (Omulimm n) (t2:::Enil)), t1 => + Eop (Omaddimm n) (t1:::t2:::Enil) | _, _ => Eop Oadd (e1:::e2:::Enil) end. @@ -169,7 +177,7 @@ Definition mulimm_base (n1: int) (e2: expr) := | i :: j :: nil => Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) | _ => - Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) + Eop (Omulimm n1) (e2 ::: Enil) end. Nondetfunction mulimm (n1: int) (e2: expr) := diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 57cd3d58..94d162a2 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -182,6 +182,14 @@ Proof. with (Val.add (Val.add x v1) (Vint n2)). apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. reflexivity. + - (* Omadd *) + subst. TrivialExists. + - (* Omadd rev *) + subst. rewrite Val.add_commut. TrivialExists. + - (* Omaddimm *) + subst. TrivialExists. + - (* Omaddimm rev *) + subst. rewrite Val.add_commut. TrivialExists. - TrivialExists. Qed. @@ -297,7 +305,7 @@ Proof. generalize (Int.one_bits_decomp n). generalize (Int.one_bits_range n). destruct (Int.one_bits n). - - intros. auto. + - intros. TrivialExists. - destruct l. + intros. rewrite H1. simpl. rewrite Int.add_zero. @@ -315,7 +323,7 @@ Proof. rewrite Val.mul_add_distr_r. repeat rewrite Val.shl_mul. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto. simpl. repeat rewrite H0; auto with coqlib. - intros. auto. + intros. TrivialExists. Qed. Theorem eval_mulimm: diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index d79a2be8..d4e2afc9 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -394,6 +394,8 @@ module Target (*: TARGET*) = fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psllw (rd, rs1, rs2) -> fprintf oc " sllw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pmaddw (rd, rs1, rs2) -> + fprintf oc " maddw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Paddl (rd, rs1, rs2) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -423,6 +425,8 @@ module Target (*: TARGET*) = fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psral (rd, rs1, rs2) -> fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pmaddl (rd, rs1, rs2) -> + fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pfaddd (rd, rs1, rs2) -> fprintf oc " faddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -442,6 +446,8 @@ module Target (*: TARGET*) = fprintf oc " compw.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint imm | Paddiw (rd, rs, imm) -> fprintf oc " addw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pmuliw (rd, rs, imm) -> + fprintf oc " mulw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pandiw (rd, rs, imm) -> fprintf oc " andw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pnandiw (rd, rs, imm) -> @@ -466,6 +472,8 @@ module Target (*: TARGET*) = fprintf oc " sllw %a = %a, %a\n" ireg rd ireg rs coqint imm | Proriw (rd, rs, imm) -> fprintf oc " rorw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pmaddiw (rd, rs, imm) -> + fprintf oc " maddw %a = %a, %a\n" ireg rd ireg rs coqint imm | Psllil (rd, rs, imm) -> fprintf oc " slld %a = %a, %a\n" ireg rd ireg rs coqint64 imm @@ -479,6 +487,8 @@ module Target (*: TARGET*) = fprintf oc " compd.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm | Paddil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pmulil (rd, rs, imm) -> assert Archi.ptr64; + fprintf oc " muld %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; @@ -495,6 +505,8 @@ module Target (*: TARGET*) = fprintf oc " andnd %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Pornil (rd, rs, imm) -> fprintf oc " ornd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Pmaddil (rd, rs, imm) -> + fprintf oc " maddd %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 57676b35..b43c4d78 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -57,6 +57,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oneg, v1::nil => neg v1 | Osub, v1::v2::nil => sub v1 v2 | Omul, v1::v2::nil => mul v1 v2 + | Omulimm n, v1::nil => mul v1 (I n) | Omulhs, v1::v2::nil => mulhs v1 v2 | Omulhu, v1::v2::nil => mulhu v1 v2 | Odiv, v1::v2::nil => divs v1 v2 @@ -88,6 +89,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshru, v1::v2::nil => shru v1 v2 | Oshruimm n, v1::nil => shru v1 (I n) | Oshrximm n, v1::nil => shrx v1 (I n) + | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3) + | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n)) | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 | Ohighlong, v1::nil => hiword v1 @@ -98,6 +101,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Onegl, v1::nil => negl v1 | Osubl, v1::v2::nil => subl v1 v2 | Omull, v1::v2::nil => mull v1 v2 + | Omullimm n, v1::nil => mull v1 (L n) | Omullhs, v1::v2::nil => mullhs v1 v2 | Omullhu, v1::v2::nil => mullhu v1 v2 | Odivl, v1::v2::nil => divls v1 v2 diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v index 0cce7ce3..9051f6ad 100644 --- a/mppa_k1c/abstractbb/ImpDep.v +++ b/mppa_k1c/abstractbb/ImpDep.v @@ -386,7 +386,7 @@ Variable print_error_end: hdeps -> hdeps -> ?? unit. Variable print_error: pstring -> ?? unit. Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := - DO r <~ (TRY + DO r <~ (TRY DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;; DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;; DO b <~ Dict.eq_test d1 d2 ;; @@ -395,7 +395,7 @@ Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := print_error_end d1 d2 ;; RET false ) - CATCH_FAIL s, _ => + CATCH_FAIL s, _ => print_error s;; RET false ENSURE (fun b => b=true -> forall ge, bblock_equiv ge p1 p2));; @@ -633,7 +633,7 @@ Definition print_witness ext exl cr msg := println(r);; println("=> encoded on " +; msg +; " graph as: ");; print_raw_hlist pl - | _ => FAILWITH "No witness info" + | _ => println "Unexpected failure: no witness info (hint: hash-consing bug ?)" end. diff --git a/test/monniaux/madd/madd.c b/test/monniaux/madd/madd.c new file mode 100644 index 00000000..f847edf3 --- /dev/null +++ b/test/monniaux/madd/madd.c @@ -0,0 +1,11 @@ +unsigned madd(unsigned a, unsigned b, unsigned c) { + return a + b*c; +} + +unsigned maddimm(unsigned a, unsigned b) { + return a + b*17113; +} + +unsigned madd2(unsigned a, unsigned b, unsigned c) { + return c + b*a; +} diff --git a/test/monniaux/madd/madd_run.c b/test/monniaux/madd/madd_run.c new file mode 100644 index 00000000..d4238c53 --- /dev/null +++ b/test/monniaux/madd/madd_run.c @@ -0,0 +1,9 @@ +#include <stdio.h> + +extern unsigned madd(unsigned a, unsigned b, unsigned c); + +int main() { + unsigned a = 7, b = 3, c = 4; + printf("res = %u\n", madd(a, b, c)); + return 0; +} |