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/Op.v | 124 ++++++++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 98 insertions(+), 26 deletions(-) (limited to 'riscV/Op.v') diff --git a/riscV/Op.v b/riscV/Op.v index c99c3b43..28760a72 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -51,14 +51,18 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) (* Expansed branches *) - | CEbeqw (optR0: option bool) (**r branch-if-equal *) + | CEbeqw (optR0: option bool) (**r branch-if-equal signed *) | CEbnew (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbequw (optR0: option bool) (**r branch-if-equal unsigned *) + | CEbneuw (optR0: option bool) (**r branch-if-not-equal unsigned *) | CEbltw (optR0: option bool) (**r branch-if-less signed *) | CEbltuw (optR0: option bool) (**r branch-if-less unsigned *) | CEbgew (optR0: option bool) (**r branch-if-greater-or-equal signed *) | CEbgeuw (optR0: option bool) (**r branch-if-greater-or-equal unsigned *) - | CEbeql (optR0: option bool) (**r branch-if-equal *) + | CEbeql (optR0: option bool) (**r branch-if-equal signed *) | CEbnel (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbequl (optR0: option bool) (**r branch-if-equal unsigned *) + | CEbneul (optR0: option bool) (**r branch-if-not-equal unsigned *) | CEbltl (optR0: option bool) (**r branch-if-less signed *) | CEbltul (optR0: option bool) (**r branch-if-less unsigned *) | CEbgel (optR0: option bool) (**r branch-if-greater-or-equal signed *) @@ -167,8 +171,10 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (* Expansed conditions *) - | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] (pseudo) *) - | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] (pseudo) *) + | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) + | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) + | OEsequw (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneuw (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) | OEsltw (optR0: option bool) (**r set-less-than *) | OEsltuw (optR0: option bool) (**r set-less-than unsigned *) | OEsltiw (n: int) (**r set-less-than immediate *) @@ -176,8 +182,10 @@ Inductive operation : Type := | OExoriw (n: int) (**r xor immediate *) | OEluiw (n: int) (**r load upper-immediate *) | OEaddiwr0 (n: int) (**r add immediate *) - | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] (pseudo) *) - | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] (pseudo) *) + | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) + | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) + | OEsequl (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneul (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) | OEsltl (optR0: option bool) (**r set-less-than *) | OEsltul (optR0: option bool) (**r set-less-than unsigned *) | OEsltil (n: int64) (**r set-less-than immediate *) @@ -270,14 +278,18 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) (* Expansed branches *) - | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 + | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cne) v1 v2 zero32 + | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 + | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Clt) v1 v2 zero32 | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cge) v1 v2 zero32 | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 - | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 + | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 + | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Clt) v1 v2 zero64 | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cge) v1 v2 zero64 @@ -383,8 +395,10 @@ Definition eval_operation | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) (* Expansed conditions *) - | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) + | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Ceq) v1 v2 zero32) + | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Cne) v1 v2 zero32) + | OEsequw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) + | OEsneuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32) | OEsltuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32) | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n)) @@ -392,8 +406,10 @@ Definition eval_operation | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) | OEluiw n, nil => Some(Vint (Int.shl n (Int.repr 12))) | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32) - | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) - | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) + | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64)) + | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64)) + | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) + | OEsneul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) | OEsltl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Clt) v1 v2 zero64)) | OEsltul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64)) | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n))) @@ -469,12 +485,16 @@ Definition type_of_condition (c: condition) : list typ := | Cnotcompfs _ => Tsingle :: Tsingle :: nil | CEbeqw _ => Tint :: Tint :: nil | CEbnew _ => Tint :: Tint :: nil + | CEbequw _ => Tint :: Tint :: nil + | CEbneuw _ => Tint :: Tint :: nil | CEbltw _ => Tint :: Tint :: nil | CEbltuw _ => Tint :: Tint :: nil | CEbgew _ => Tint :: Tint :: nil | CEbgeuw _ => Tint :: Tint :: nil | CEbeql _ => Tlong :: Tlong :: nil | CEbnel _ => Tlong :: Tlong :: nil + | CEbequl _ => Tlong :: Tlong :: nil + | CEbneul _ => Tlong :: Tlong :: nil | CEbltl _ => Tlong :: Tlong :: nil | CEbltul _ => Tlong :: Tlong :: nil | CEbgel _ => Tlong :: Tlong :: nil @@ -578,6 +598,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocmp c => (type_of_condition c, Tint) | OEseqw _ => (Tint :: Tint :: nil, Tint) | OEsnew _ => (Tint :: Tint :: nil, Tint) + | OEsequw _ => (Tint :: Tint :: nil, Tint) + | OEsneuw _ => (Tint :: Tint :: nil, Tint) | OEsltw _ => (Tint :: Tint :: nil, Tint) | OEsltuw _ => (Tint :: Tint :: nil, Tint) | OEsltiw _ => (Tint :: nil, Tint) @@ -587,6 +609,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEaddiwr0 _ => (nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) | OEsnel _ => (Tlong :: Tlong :: nil, Tint) + | OEsequl _ => (Tlong :: Tlong :: nil, Tint) + | OEsneul _ => (Tlong :: Tlong :: nil, Tint) | OEsltl _ => (Tlong :: Tlong :: nil, Tint) | OEsltul _ => (Tlong :: Tlong :: nil, Tint) | OEsltil _ => (Tlong :: nil, Tint) @@ -808,9 +832,15 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* OEseqw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsequw *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... - (* OEsnew *) + (* OEsneuw *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... (* OEsltw *) @@ -831,9 +861,15 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEaddiwr0 *) - trivial. (* OEseql *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsequl *) - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... - (* OEsnel *) + (* OEsneul *) - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... (* OEsltl *) @@ -944,12 +980,16 @@ Definition negate_condition (cond: condition): condition := | Cnotcompfs c => Ccompfs c | CEbeqw optR0 => CEbnew optR0 | CEbnew optR0 => CEbeqw optR0 + | CEbequw optR0 => CEbneuw optR0 + | CEbneuw optR0 => CEbequw optR0 | CEbltw optR0 => CEbgew optR0 | CEbltuw optR0 => CEbgeuw optR0 | CEbgew optR0 => CEbltw optR0 | CEbgeuw optR0 => CEbltuw optR0 | CEbeql optR0 => CEbnel optR0 | CEbnel optR0 => CEbeql optR0 + | CEbequl optR0 => CEbneul optR0 + | CEbneul optR0 => CEbequl optR0 | CEbltl optR0 => CEbgel optR0 | CEbltul optR0 => CEbgeul optR0 | CEbgel optR0 => CEbltl optR0 @@ -974,6 +1014,10 @@ Proof. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; apply Val.negate_cmpu_bool. repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; @@ -987,6 +1031,10 @@ Proof. repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; apply Val.negate_cmpu_bool. repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; apply Val.negate_cmplu_bool. repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; apply Val.negate_cmplu_bool. @@ -1094,12 +1142,12 @@ Definition cond_depends_on_memory (cond : condition) : bool := | Ccompuimm _ _ => negb Archi.ptr64 | Ccomplu _ => Archi.ptr64 | Ccompluimm _ _ => Archi.ptr64 - | CEbeqw _ => negb Archi.ptr64 - | CEbnew _ => negb Archi.ptr64 + | CEbequw _ => negb Archi.ptr64 + | CEbneuw _ => negb Archi.ptr64 | CEbltuw _ => negb Archi.ptr64 | CEbgeuw _ => negb Archi.ptr64 - | CEbeql _ => Archi.ptr64 - | CEbnel _ => Archi.ptr64 + | CEbequl _ => Archi.ptr64 + | CEbneul _ => Archi.ptr64 | CEbltul _ => Archi.ptr64 | CEbgeul _ => Archi.ptr64 | _ => false @@ -1108,12 +1156,12 @@ Definition cond_depends_on_memory (cond : condition) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp cmp => cond_depends_on_memory cmp - | OEseqw _ => negb Archi.ptr64 - | OEsnew _ => negb Archi.ptr64 + | OEsequw _ => negb Archi.ptr64 + | OEsneuw _ => negb Archi.ptr64 | OEsltiuw _ => negb Archi.ptr64 | OEsltuw _ => negb Archi.ptr64 - | OEseql _ => Archi.ptr64 - | OEsnel _ => Archi.ptr64 + | OEsequl _ => Archi.ptr64 + | OEsneul _ => Archi.ptr64 | OEsltul _ => Archi.ptr64 | OEsltiul _ => Archi.ptr64 | _ => false @@ -1379,6 +1427,10 @@ Proof. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; eapply eval_cmpu_bool_inj'; eauto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; @@ -1391,6 +1443,10 @@ Proof. inv H3; inv H2; simpl in H0; inv H0; auto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + inv H3; inv H2; simpl in H0; inv H0; auto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; eapply eval_cmplu_bool_inj'; eauto. - destruct optR0 as [[]|]; unfold apply_bin_r0 in *; @@ -1612,8 +1668,16 @@ Proof. destruct b; simpl; constructor. simpl; constructor. (* OEseqw *) - - apply eval_cmpu_bool_inj_opt; auto. + - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsequw *) + - apply eval_cmpu_bool_inj_opt; auto. + (* OEsneuw *) - apply eval_cmpu_bool_inj_opt; auto. (* OEsltw *) - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; @@ -1628,8 +1692,16 @@ Proof. (* OExoriw *) - inv H4; simpl; auto. (* OEseql *) - - apply eval_cmplu_bool_inj_opt; auto. + - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; + try apply Val.inject_int. + (* OEsequl *) + - apply eval_cmplu_bool_inj_opt; auto. + (* OEsneul *) - apply eval_cmplu_bool_inj_opt; auto. (* OEsltl *) - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; -- cgit