From ca34ea47f863c074a9d0ca890097786c5829267c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 22:36:22 +0200 Subject: ternary ops for float/double --- mppa_k1c/Asmblockgenproof1.v | 28 ++++++++++++++++++++++++++++ mppa_k1c/Machregs.v | 2 +- mppa_k1c/NeedOp.v | 44 +++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 72 insertions(+), 2 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 99ab1b91..f75f0bd3 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1665,6 +1665,34 @@ Opaque Int.eq. destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. +- (* Oselectf *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold selectl. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. +- (* Oselectfs *) + econstructor; split. + + eapply exec_straight_one. + simpl; reflexivity. + + split. + * unfold selectl. + destruct (rs x1) eqn:eqX1; try constructor. + destruct (rs x) eqn:eqX; try constructor. + destruct (rs x0) eqn:eqX0; try constructor. + simpl. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. + * intros. + rewrite Pregmap.gso; congruence. Qed. (** Memory accesses *) diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index f494c67d..f89f952f 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -209,7 +209,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect | Oselectl => true + | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect | Oselectl | Oselectf | Oselectfs => true | _ => false end. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index a6ecb820..f3ce8361 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -117,7 +117,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c - | Oselect | Oselectl => op3 (default nv) + | Oselect | Oselectl | Oselectf | Oselectfs => op3 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -227,6 +227,44 @@ Proof. constructor. Qed. +Lemma selectf_sound: + forall v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (selectf v0 v1 v2) (selectf w0 w1 w2) x. +Proof. + unfold default; intros. + destruct x; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + inv H. inv H0. inv H1. simpl. + constructor. +Qed. + +Lemma selectfs_sound: + forall v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (selectfs v0 v1 v2) (selectfs w0 w1 w2) x. +Proof. + unfold default; intros. + destruct x; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + - destruct v2; simpl; trivial. + destruct v0; simpl; trivial. + destruct v1; simpl; trivial. + inv H. inv H0. inv H1. simpl. + constructor. +Qed. + Remark default_idem: forall nv, default (default nv) = default nv. Proof. destruct nv; simpl; trivial. @@ -283,6 +321,10 @@ Proof. - apply select_sound; trivial. (* selectl *) - apply selectl_sound; trivial. + (* selectf *) +- apply selectf_sound; trivial. + (* selectfs *) +- apply selectfs_sound; trivial. Qed. Lemma operation_is_redundant_sound: -- cgit