From adf1bbcd5c356a0cb75c412357a3b7af23795f47 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 11 Feb 2021 20:03:49 +0100 Subject: [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof --- riscV/ValueAOp.v | 50 +++++++++++++++++++++++++++++--------------------- 1 file changed, 29 insertions(+), 21 deletions(-) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index ece28eff..581229c6 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -41,14 +41,18 @@ 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 (cmpu_bool Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32 + | 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 (cmplu_bool Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64 + | 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 @@ -159,8 +163,10 @@ 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) - | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32) + | 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) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) @@ -168,8 +174,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => I (Int.shl n (Int.repr 12)) | OEaddiwr0 n, nil => add (I n) zero32 - | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) - | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64) + | 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) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) @@ -206,7 +214,7 @@ Proof. destruct cond; simpl; eauto with va. inv H2. destruct cond; simpl; eauto with va. - 13: 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; unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va. Qed. @@ -291,23 +299,23 @@ Proof. apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. Qed. -Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0, +Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0 cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp Clt) a1 a0 Op.zero32) - (of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) b1 b0 zero32)). + 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)). Proof. intros. destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. Qed. -Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0, +Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0 cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl Clt) a1 a0 Op.zero64)) - (of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) b1 b0 zero64)). + (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)). Proof. intros. destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; @@ -327,16 +335,16 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - 1,2,4: apply eval_cmpu_sound; auto. - apply eval_cmp_sound; auto. + 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. - unfold zero32; simpl. eauto with va. - 1,2,4: apply eval_cmplu_sound; auto. - apply eval_cmpl_sound; auto. + unfold zero32; simpl; 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 zero64; simpl; eauto with va. all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. -- cgit