diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-01 16:44:07 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-01 16:44:07 +0100 |
| commit | d8fafb0add258e47287a2d57454194db8f1dd635 (patch) | |
| tree | 8b47f5fddb0b32fef035bbb4fec68d0d40f27f31 /mppa_k1c/Asmblockgenproof1.v | |
| parent | df32503f46a62b18f92363ac7f81ec0d5b36c64a (diff) | |
| download | compcert-kvx-d8fafb0add258e47287a2d57454194db8f1dd635.tar.gz compcert-kvx-d8fafb0add258e47287a2d57454194db8f1dd635.zip | |
Implemented float comparisons (no branching yet, and no negation)
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 175eca73..f7207c88 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -968,6 +968,36 @@ Proof. split; intros; Simpl. Qed. +Lemma swap_comparison_cmpfs: + forall v1 v2 cmp, + Val.lessdef (Val.cmpfs cmp v1 v2) (Val.cmpfs (swap_comparison cmp) v2 v1). +Proof. + intros. unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. + rewrite Float32.cmp_swap. auto. +Qed. + +Lemma transl_cond_float32_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_float32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.cmpfs cmp rs#r1 rs#r2) rs'#rd + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + intros. destruct cmp; simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpfs. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpfs. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +Qed. + Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> @@ -1003,6 +1033,8 @@ Proof. exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite MKTOT; eauto. ++ (* cmpfloat *) + exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. Qed. (* |