From c19ecc9326d0278989d7651bf8c8cf0d1c387235 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 6 Mar 2021 12:36:11 +0100 Subject: Adding a mini CSE pass in the expansion oracle --- riscV/ValueAOp.v | 41 ++++++++++++++++++++--------------------- 1 file changed, 20 insertions(+), 21 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 97f3ff61..d50bd00f 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -27,24 +27,18 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 | Some false => sem v1 vz end. -Definition may_undef_int (is_long: bool) (sem: aval -> aval -> aval) (v1 vimm vz: aval): aval := +Definition may_undef_int (is_long: bool) (v1 v2: aval): aval := if negb is_long then match v1 with - | I _ => sem vimm vz + | I _ => v2 | _ => Ifptr Ptop end else match v1 with - | L _ => sem vimm vz + | L _ => v2 | _ => Ifptr Ptop end. -Definition may_undef_luil (v1: aval) (n: int64): aval := - match v1 with - | L _ => sign_ext 32 (shll (L n) (L (Int64.repr 12))) - | _ => Ifptr Ptop - end. - Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -223,8 +217,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) - | OEluiw n is_long, v1::nil => may_undef_int is_long shl v1 (I n) (I (Int.repr 12)) - | OEaddiwr0 n is_long, v1::nil => may_undef_int is_long add v1 (I n) zero32 + | OEluiw n, nil => shl (I n) (I (Int.repr 12)) + | OEaddiwr0 n, nil => add (I n) zero32 | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) @@ -234,9 +228,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OExoril n, v1::nil => xorl v1 (L n) - | OEluil n, v1::nil => may_undef_luil v1 n - | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64 + | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) + | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) + | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) @@ -464,14 +459,18 @@ Proof. 1,2,3: apply eval_cmp_sound; auto. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - unfold zero32; simpl; eauto with va. - - 1,2,11,12: - try unfold Op.may_undef_int, may_undef_int, Op.zero32, zero32, Op.zero64, zero64; - try unfold Op.may_undef_luil, may_undef_luil; simpl; unfold ntop1; - inv H1; try destruct is_long; simpl; try destruct (Int.ltu _ _); eauto with va; - try apply vmatch_ifptr_i; try apply vmatch_ifptr_l. - + + simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; + try apply vmatch_ifptr_undef. + 10: + simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; + apply vmatch_ifptr_l. + 1,10: simpl; eauto with va. + 9: + unfold Op.may_undef_int, may_undef_int; destruct is_long; + simpl; inv H0; inv H1; eauto with va; inv H; + apply vmatch_ifptr_p; eauto with va. + 3,4,6: apply eval_cmplu_sound; auto. 1,2,3: apply eval_cmpl_sound; auto. unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. -- cgit From 95205e72ca536907fa89c7c884f0e22fc605063d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 26 Mar 2021 12:49:02 +0100 Subject: Adding more expansions, improving miniCSE, and tuning prepass --- riscV/ValueAOp.v | 65 ++++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 56 insertions(+), 9 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index d50bd00f..fe519921 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -39,6 +39,32 @@ Definition may_undef_int (is_long: bool) (v1 v2: aval): aval := | _ => Ifptr Ptop end. +Definition shrx_imm_undef (v1 v2: aval): aval := + match v1 with + | I n1 => + match v2 with + | I n2 => + if Int.ltu n2 (Int.repr 31) + then I n1 + else Ifptr Ptop + | _ => Ifptr Ptop + end + | _ => Ifptr Ptop + end. + +Definition shrxl_imm_undef (v1 v2: aval): aval := + match v1 with + | L n1 => + match v2 with + | I n2 => + if Int.ltu n2 (Int.repr 63) + then L n1 + else Ifptr Ptop + | _ => Ifptr Ptop + end + | _ => Ifptr Ptop + end. + Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -218,7 +244,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => shl (I n) (I (Int.repr 12)) + | OEaddiw n, v1::nil => add (I n) v1 | OEaddiwr0 n, nil => add (I n) zero32 + | OEandiw n, v1::nil => and (I n) v1 + | OEoriw n, v1::nil => or (I n) v1 | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) @@ -227,11 +256,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) + | OEandil n, v1::nil => andl (L n) v1 + | OEoril n, v1::nil => orl (L n) v1 | OExoril n, v1::nil => xorl v1 (L n) | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) + | OEaddil n, v1::nil => addl (L n) v1 | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2 + | OEshrxundef n, v1::nil => shrx_imm_undef v1 (I n) + | OEshrxlundef n, v1::nil => shrxl_imm_undef v1 (I n) | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) @@ -460,22 +494,35 @@ Proof. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; - try apply vmatch_ifptr_undef. - 10: - simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; - apply vmatch_ifptr_l. + { fold (Val.add (Vint n) a1); eauto with va. } + { unfold zero32; simpl; eauto with va. } + { fold (Val.and (Vint n) a1); eauto with va. } + { fold (Val.or (Vint n) a1); eauto with va. } + { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; + try apply vmatch_ifptr_undef. } + 9: { fold (Val.addl (Vlong n) a1); eauto with va. } + 10: { fold (Val.andl (Vlong n) a1); eauto with va. } + 10: { fold (Val.orl (Vlong n) a1); eauto with va. } + 10: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; + apply vmatch_ifptr_l. } + 1,10: simpl; eauto with va. - 9: + 2: unfold Op.may_undef_int, may_undef_int; destruct is_long; simpl; inv H0; inv H1; eauto with va; inv H; apply vmatch_ifptr_p; eauto with va. 3,4,6: apply eval_cmplu_sound; auto. 1,2,3: apply eval_cmpl_sound; auto. - unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. - unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. - unfold zero64; simpl; eauto with va. + { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. } + { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. } + { unfold zero64; simpl; eauto with va. } + { unfold Op.shrx_imm_undef, shrx_imm_undef. + simpl; inv H1; eauto with va; + destruct (Int.ltu _ _); simpl; eauto with va. } + { unfold Op.shrxl_imm_undef, shrxl_imm_undef. + simpl; inv H1; eauto with va; + destruct (Int.ltu _ _); simpl; eauto with va. } all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. -- cgit From 0d98d7fec937d3a9a2324f1731b041cfbf16dcbe Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 10:11:01 +0200 Subject: Refactoring the mayundef OP to be more general... --- riscV/ValueAOp.v | 67 +++++++++++++++++++------------------------------------- 1 file changed, 23 insertions(+), 44 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index fe519921..82291f9c 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -27,42 +27,28 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 | Some false => sem v1 vz end. -Definition may_undef_int (is_long: bool) (v1 v2: aval): aval := - if negb is_long then - match v1 with - | I _ => v2 - | _ => Ifptr Ptop - end - else - match v1 with - | L _ => v2 - | _ => Ifptr Ptop - end. - -Definition shrx_imm_undef (v1 v2: aval): aval := - match v1 with - | I n1 => - match v2 with - | I n2 => - if Int.ltu n2 (Int.repr 31) - then I n1 - else Ifptr Ptop +Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := + match mu with + | MUint => match v1 with + | I _ => v2 + | _ => Ifptr Ptop + end + | MUlong => match v1 with + | L _ => v2 + | _ => Ifptr Ptop + end + | MUshrx i => + match v1 with + | I _ => + if Int.ltu i (Int.repr 31) then v1 else Ifptr Ptop | _ => Ifptr Ptop end - | _ => Ifptr Ptop - end. - -Definition shrxl_imm_undef (v1 v2: aval): aval := - match v1 with - | L n1 => - match v2 with - | I n2 => - if Int.ltu n2 (Int.repr 63) - then L n1 - else Ifptr Ptop + | MUshrxl i => + match v1 with + | L _ => + if Int.ltu i (Int.repr 63) then v1 else Ifptr Ptop | _ => Ifptr Ptop end - | _ => Ifptr Ptop end. Definition eval_static_condition (cond: condition) (vl: list aval): abool := @@ -263,9 +249,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEaddil n, v1::nil => addl (L n) v1 | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) - | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2 - | OEshrxundef n, v1::nil => shrx_imm_undef v1 (I n) - | OEshrxlundef n, v1::nil => shrxl_imm_undef v1 (I n) + | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) @@ -508,21 +492,16 @@ Proof. 1,10: simpl; eauto with va. 2: - unfold Op.may_undef_int, may_undef_int; destruct is_long; - simpl; inv H0; inv H1; eauto with va; inv H; - apply vmatch_ifptr_p; eauto with va. + unfold Op.eval_may_undef, eval_may_undef; destruct mu; + inv H1; inv H0; eauto with va; + try destruct (Int.ltu _ _); simpl; + try eapply vmatch_ifptr_p, pmatch_top'; eauto with va. 3,4,6: apply eval_cmplu_sound; auto. 1,2,3: apply eval_cmpl_sound; auto. { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. } { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. } { unfold zero64; simpl; eauto with va. } - { unfold Op.shrx_imm_undef, shrx_imm_undef. - simpl; inv H1; eauto with va; - destruct (Int.ltu _ _); simpl; eauto with va. } - { unfold Op.shrxl_imm_undef, shrxl_imm_undef. - simpl; inv H1; eauto with va; - destruct (Int.ltu _ _); simpl; eauto with va. } all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. -- cgit From 83b556a101b7ed490acf9e127c5b4b9db40e1019 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 11:25:28 +0200 Subject: Now a more general way to perform imm operations --- riscV/ValueAOp.v | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 82291f9c..b64040e1 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -51,6 +51,12 @@ Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := end end. +Definition eval_opimmR0 (opi: opimm): aval := + match opi with + | OPimmADD i => add (I i) zero32 + | OPimmADDL i => addl (L i) zero64 + end. + Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -220,6 +226,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) + | OEimmR0 opi, nil => eval_opimmR0 opi | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32) | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32) | OEsequw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) @@ -231,7 +238,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => shl (I n) (I (Int.repr 12)) | OEaddiw n, v1::nil => add (I n) v1 - | OEaddiwr0 n, nil => add (I n) zero32 | OEandiw n, v1::nil => and (I n) v1 | OEoriw n, v1::nil => or (I n) v1 | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) @@ -247,7 +253,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OExoril n, v1::nil => xorl v1 (L n) | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) | OEaddil n, v1::nil => addl (L n) v1 - | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) @@ -472,36 +477,36 @@ Proof. destruct (propagate_float_constants tt); constructor. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - + + unfold Op.eval_opimmR0, eval_opimmR0, Op.zero32, zero32, Op.zero64, zero64; + destruct opi; eauto with va. 3,4,6: apply eval_cmpu_sound; auto. 1,2,3: apply eval_cmp_sound; auto. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. { fold (Val.add (Vint n) a1); eauto with va. } - { unfold zero32; simpl; eauto with va. } { fold (Val.and (Vint n) a1); eauto with va. } { fold (Val.or (Vint n) a1); eauto with va. } { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; try apply vmatch_ifptr_undef. } 9: { fold (Val.addl (Vlong n) a1); eauto with va. } - 10: { fold (Val.andl (Vlong n) a1); eauto with va. } - 10: { fold (Val.orl (Vlong n) a1); eauto with va. } - 10: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; + 9: { fold (Val.andl (Vlong n) a1); eauto with va. } + 9: { fold (Val.orl (Vlong n) a1); eauto with va. } + 9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; apply vmatch_ifptr_l. } 1,10: simpl; eauto with va. - 2: + 10: unfold Op.eval_may_undef, eval_may_undef; destruct mu; inv H1; inv H0; eauto with va; try destruct (Int.ltu _ _); simpl; try eapply vmatch_ifptr_p, pmatch_top'; eauto with va. - 3,4,6: apply eval_cmplu_sound; auto. - 1,2,3: apply eval_cmpl_sound; auto. - { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. } - { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. } - { unfold zero64; simpl; eauto with va. } + 4,5,7: apply eval_cmplu_sound; auto. + 1,3,4: apply eval_cmpl_sound; auto. + 2: { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. } + 2: { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. } all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. -- cgit From df9aab806ae8d20393b56e4175e210ed6cff1ef1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 12:48:51 +0200 Subject: a more general way to manage special registers before introducing SP --- riscV/ValueAOp.v | 98 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 49 insertions(+), 49 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index b64040e1..e48c4a5b 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -20,11 +20,11 @@ Require Import Zbits. Definition zero32 := (I Int.zero). Definition zero64 := (L Int64.zero). -Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := - match optR0 with +Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := + match optR with | None => sem v1 v2 - | Some true => sem vz v1 - | Some false => sem v1 vz + | Some X0_L => sem vz v1 + | Some X0_R => sem v1 vz end. Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := @@ -71,22 +71,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) - | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32 - | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32 - | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32 - | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32 - | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32 - | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cge) v1 v2 zero32 - | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cge) v1 v2 zero32 - | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64 - | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64 - | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64 - | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64 - | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64 - | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cge) v1 v2 zero64 - | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cge) v1 v2 zero64 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 | _, _ => Bnone end. @@ -227,12 +227,12 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) | OEimmR0 opi, nil => eval_opimmR0 opi - | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32) - | OEsequw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) - | OEsneuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32) - | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32) - | OEsltuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32) + | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32) + | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32) + | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32) + | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32) + | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32) + | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) @@ -240,12 +240,12 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEaddiw n, v1::nil => add (I n) v1 | OEandiw n, v1::nil => and (I n) v1 | OEoriw n, v1::nil => or (I n) v1 - | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) - | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) - | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) - | OEsneul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64) - | OEsltl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64) - | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64) + | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64) + | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64) + | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64) + | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64) + | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64) + | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OEandil n, v1::nil => andl (L n) v1 @@ -358,7 +358,7 @@ Proof. inv H2. destruct cond; simpl; eauto with va. 17: destruct cond; simpl; eauto with va. - all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0; + all: destruct optR as [[]|]; unfold apply_bin_oreg, Op.apply_bin_oreg; unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va. Qed. @@ -415,53 +415,53 @@ Proof. inv H; auto. simpl. destruct b; constructor. Qed. -Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m, +Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) - (of_optbool (apply_bin_r0 optR0 (cmpu_bool c) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. Qed. -Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR0 m, +Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc (Val.maketotal - (Op.apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) c) a1 a0 + (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0 Op.zero64)) - (of_optbool (apply_bin_r0 optR0 (cmplu_bool c) b1 b0 zero64)). + (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. Qed. -Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0 cmp, +Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp cmp) a1 a0 Op.zero32) - (of_optbool (apply_bin_r0 optR0 (cmp_bool cmp) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. Qed. -Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0 cmp, +Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl cmp) a1 a0 Op.zero64)) - (of_optbool (apply_bin_r0 optR0 (cmpl_bool cmp) b1 b0 zero64)). + (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64)) + (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. Qed. -- cgit From dd4767e17235adb5de922626ed1fea15f4eb9e3b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 6 Apr 2021 23:37:22 +0200 Subject: Important commit on expansions' mini CSE, and a draft for addptrofs --- riscV/ValueAOp.v | 133 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 68 insertions(+), 65 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index e48c4a5b..3ba2732d 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -19,44 +19,41 @@ Require Import Zbits. Definition zero32 := (I Int.zero). Definition zero64 := (L Int64.zero). - -Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := + +(** Functions to select a special register (see Op.v) *) + +Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz sp: aval): B := match optR with | None => sem v1 v2 | Some X0_L => sem vz v1 | Some X0_R => sem v1 vz + | Some SP_S => sem v1 sp end. Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := match mu with - | MUint => match v1 with - | I _ => v2 - | _ => Ifptr Ptop + | MUint => match v1, v2 with + | I _, I _ => v2 + | _, _ => Ifptr Ptop end - | MUlong => match v1 with - | L _ => v2 - | _ => Ifptr Ptop + | MUlong => match v1, v2 with + | L _, I _ => v2 + | _, _ => Ifptr Ptop end | MUshrx i => - match v1 with - | I _ => - if Int.ltu i (Int.repr 31) then v1 else Ifptr Ptop - | _ => Ifptr Ptop + match v1, v2 with + | I _, I _ => + if Int.ltu i (Int.repr 31) then v2 else Ifptr Ptop + | _, _ => Ifptr Ptop end | MUshrxl i => - match v1 with - | L _ => - if Int.ltu i (Int.repr 63) then v1 else Ifptr Ptop - | _ => Ifptr Ptop + match v1, v2 with + | L _, L _ => + if Int.ltu i (Int.repr 63) then v2 else Ifptr Ptop + | _, _ => Ifptr Ptop end end. -Definition eval_opimmR0 (opi: opimm): aval := - match opi with - | OPimmADD i => add (I i) zero32 - | OPimmADDL i => addl (L i) zero64 - end. - Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -71,22 +68,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) - | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 - | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 - | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 - | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 - | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 - | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 - | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 - | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 - | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 - | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 - | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 - | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 - | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 - | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 - | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 - | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop) + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop) + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop) + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop) + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop) + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop) + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 (Ifptr Ptop) + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 (Ifptr Ptop) + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop) + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop) + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop) + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop) + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop) + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop) + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 (Ifptr Ptop) + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 (Ifptr Ptop) | _, _ => Bnone end. @@ -226,33 +223,35 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) - | OEimmR0 opi, nil => eval_opimmR0 opi - | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32) - | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32) - | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32) - | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32) - | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32) - | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32) + | OEmoveSP, nil => Ptr Stack + | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) + | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop)) + | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) + | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop)) + | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop)) + | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop)) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => shl (I n) (I (Int.repr 12)) - | OEaddiw n, v1::nil => add (I n) v1 + | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 (Ifptr Ptop) + | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) | OEandiw n, v1::nil => and (I n) v1 | OEoriw n, v1::nil => or (I n) v1 - | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64) - | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64) - | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64) - | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64) - | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64) - | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64) + | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) + | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop)) + | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) + | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop)) + | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop)) + | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop)) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OEandil n, v1::nil => andl (L n) v1 | OEoril n, v1::nil => orl (L n) v1 | OExoril n, v1::nil => xorl v1 (L n) | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) - | OEaddil n, v1::nil => addl (L n) v1 + | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 (Ifptr Ptop) + | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) | OEloadli n, nil => L (n) | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) @@ -419,8 +418,8 @@ Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) - (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32 Vundef) + (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -434,8 +433,8 @@ Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m, vmatch bc (Val.maketotal (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0 - Op.zero64)) - (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)). + Op.zero64 Vundef)) + (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -445,8 +444,8 @@ Qed. Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32) - (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32 Vundef) + (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -457,8 +456,8 @@ Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64)) - (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)). + (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64 Vundef)) + (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -478,19 +477,23 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - unfold Op.eval_opimmR0, eval_opimmR0, Op.zero32, zero32, Op.zero64, zero64; - destruct opi; eauto with va. 3,4,6: apply eval_cmpu_sound; auto. 1,2,3: apply eval_cmp_sound; auto. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - { fold (Val.add (Vint n) a1); eauto with va. } + { destruct optR as [[]|]; simpl; eauto with va; + InvHyps; eauto with va; + destruct Archi.ptr64 eqn:A; simpl; + inv H1; simpl; try rewrite A; simpl; eauto with va. } { fold (Val.and (Vint n) a1); eauto with va. } { fold (Val.or (Vint n) a1); eauto with va. } { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; try apply vmatch_ifptr_undef. } - 9: { fold (Val.addl (Vlong n) a1); eauto with va. } + 9: { destruct optR as [[]|]; simpl; eauto with va; + InvHyps; eauto with va; + destruct Archi.ptr64 eqn:A; simpl; + inv H1; simpl; try rewrite A; simpl; eauto with va. } 9: { fold (Val.andl (Vlong n) a1); eauto with va. } 9: { fold (Val.orl (Vlong n) a1); eauto with va. } 9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; -- cgit From b7720bc5973e9890e7c320bb34b784e2e2b2da69 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 9 Apr 2021 11:02:52 +0200 Subject: Removing addptrofs draft, next will be merging --- riscV/ValueAOp.v | 98 +++++++++++++++++++++++++++----------------------------- 1 file changed, 47 insertions(+), 51 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 3ba2732d..d29180e4 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -22,12 +22,11 @@ Definition zero64 := (L Int64.zero). (** Functions to select a special register (see Op.v) *) -Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz sp: aval): B := +Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := match optR with | None => sem v1 v2 | Some X0_L => sem vz v1 | Some X0_R => sem v1 vz - | Some SP_S => sem v1 sp end. Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := @@ -68,22 +67,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) - | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop) - | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop) - | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop) - | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop) - | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop) - | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop) - | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 (Ifptr Ptop) - | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 (Ifptr Ptop) - | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop) - | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop) - | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop) - | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop) - | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop) - | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop) - | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 (Ifptr Ptop) - | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 (Ifptr Ptop) + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 | _, _ => Bnone end. @@ -223,35 +222,34 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) - | OEmoveSP, nil => Ptr Stack - | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) - | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop)) - | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) - | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop)) - | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop)) - | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop)) + | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32) + | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32) + | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32) + | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32) + | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32) + | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => shl (I n) (I (Int.repr 12)) - | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 (Ifptr Ptop) - | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) + | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 + | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (I n) (Ifptr Ptop) | OEandiw n, v1::nil => and (I n) v1 | OEoriw n, v1::nil => or (I n) v1 - | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) - | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop)) - | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) - | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop)) - | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop)) - | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop)) + | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64) + | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64) + | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64) + | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64) + | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64) + | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OEandil n, v1::nil => andl (L n) v1 | OEoril n, v1::nil => orl (L n) v1 | OExoril n, v1::nil => xorl v1 (L n) | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) - | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 (Ifptr Ptop) - | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) + | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 + | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (L n) (Ifptr Ptop) | OEloadli n, nil => L (n) | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) @@ -418,8 +416,8 @@ Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32 Vundef) - (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32 (Ifptr Ptop))). + vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -433,8 +431,8 @@ Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m, vmatch bc (Val.maketotal (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0 - Op.zero64 Vundef)) - (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64 (Ifptr Ptop))). + Op.zero64)) + (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -444,8 +442,8 @@ Qed. Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32 Vundef) - (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32 (Ifptr Ptop))). + vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -456,8 +454,8 @@ Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64 Vundef)) - (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64 (Ifptr Ptop))). + (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64)) + (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -482,18 +480,16 @@ Proof. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - { destruct optR as [[]|]; simpl; eauto with va; - InvHyps; eauto with va; - destruct Archi.ptr64 eqn:A; simpl; - inv H1; simpl; try rewrite A; simpl; eauto with va. } + { destruct optR as [[]|]; simpl; eauto with va. } + { destruct optR as [[]|]; + unfold apply_bin_oreg, Op.apply_bin_oreg; eauto with va. } { fold (Val.and (Vint n) a1); eauto with va. } { fold (Val.or (Vint n) a1); eauto with va. } { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; try apply vmatch_ifptr_undef. } - 9: { destruct optR as [[]|]; simpl; eauto with va; - InvHyps; eauto with va; - destruct Archi.ptr64 eqn:A; simpl; - inv H1; simpl; try rewrite A; simpl; eauto with va. } + 9: { destruct optR as [[]|]; simpl; eauto with va. } + 9: { destruct optR as [[]|]; + unfold apply_bin_oreg, Op.apply_bin_oreg; eauto with va. } 9: { fold (Val.andl (Vlong n) a1); eauto with va. } 9: { fold (Val.orl (Vlong n) a1); eauto with va. } 9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; -- cgit