diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-11-20 21:37:46 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-11-20 21:37:46 +0100 |
commit | c10f3ec4dbcd8be682e01937762dc70d478ca2df (patch) | |
tree | 822e5b3a66d445bba8918c3a06a22a2f0f91d38a /scheduling | |
parent | a0cc099cb27ef311b6e8fd4ce85001a1d390db8a (diff) | |
download | compcert-kvx-c10f3ec4dbcd8be682e01937762dc70d478ca2df.tar.gz compcert-kvx-c10f3ec4dbcd8be682e01937762dc70d478ca2df.zip |
prepass scheduling proof finished !
proof of the two remaining lemmas
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/RTLpathSE_theory.v | 80 |
1 files changed, 56 insertions, 24 deletions
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v index c43c530e..4c492ecd 100644 --- a/scheduling/RTLpathSE_theory.v +++ b/scheduling/RTLpathSE_theory.v @@ -1727,6 +1727,7 @@ Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := | BA_addrglobal id ptr => Some (BA_addrglobal id ptr) end. + Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 := match lbsv with | nil => Some nil @@ -1744,6 +1745,34 @@ Proof. try destruct (seval_list_builtin_sval _ _ _ _ _); discriminate. Qed. +Lemma seval_builtin_sval_arg (ge:RTL.genv) sp rs0 m0 bs: + forall ba m v, + seval_builtin_sval ge sp bs rs0 m0 = Some ba -> + eval_builtin_arg ge (fun id => id) sp m ba v -> + seval_builtin_arg ge sp m rs0 m0 bs v. +Proof. + induction bs; simpl; + try (intros ba m v H; inversion H; subst; clear H; + intros H; inversion H; subst; + econstructor; auto; fail). + - intros ba m v; destruct (seval_sval _ _ _ _ _) eqn: SV; + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; auto. + - intros ba m v. + destruct (seval_builtin_sval _ _ bs1 _ _) eqn: SV1; try congruence. + destruct (seval_builtin_sval _ _ bs2 _ _) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. + - intros ba m v. + destruct (seval_builtin_sval _ _ bs1 _ _) eqn: SV1; try congruence. + destruct (seval_builtin_sval _ _ bs2 _ _) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. +Qed. + Lemma seval_builtin_arg_sval ge sp m rs0 m0 v: forall bs, seval_builtin_arg ge sp m rs0 m0 bs v -> exists ba, @@ -1768,6 +1797,23 @@ Proof. + constructor; assumption. Qed. +Lemma seval_builtin_sval_args (ge:RTL.genv) sp rs0 m0 lbs: + forall lba m v, + seval_list_builtin_sval ge sp lbs rs0 m0 = Some lba -> + list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba v -> + seval_builtin_args ge sp m rs0 m0 lbs v. +Proof. + unfold seval_builtin_args; induction lbs; simpl; intros lba m v. + - intros H; inversion H; subst; clear H. + intros H; inversion H. econstructor. + - destruct (seval_builtin_sval _ _ _ _ _) eqn:SV; try congruence. + destruct (seval_list_builtin_sval _ _ _ _ _) eqn: SVL; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst; clear H. + econstructor; eauto. + eapply seval_builtin_sval_arg; eauto. +Qed. + Lemma seval_builtin_args_sval ge sp m rs0 m0 lv: forall lbs, seval_builtin_args ge sp m rs0 m0 lbs lv -> exists lba, @@ -1790,36 +1836,22 @@ Lemma seval_builtin_sval_correct ge sp m rs0 m0: forall bs1 v bs2, (seval_builtin_sval ge sp bs1 rs0 m0) = (seval_builtin_sval ge sp bs2 rs0 m0) -> seval_builtin_arg ge sp m rs0 m0 bs2 v. Proof. - induction bs1. - all: try(destruct bs2; - intros Hinv Hrew; - inv Hinv; - cbn in *; - try constructor; - repeat (destruct seval_sval; [idtac | discriminate]); - repeat (destruct seval_builtin_sval; [idtac | discriminate]); - try congruence; - inv Hrew; - constructor). - - admit. - - admit. -Admitted. + intros. exploit seval_builtin_arg_sval; eauto. + intros (ba & X1 & X2). + eapply seval_builtin_sval_arg; eauto. + congruence. +Qed. Lemma seval_list_builtin_sval_correct ge sp m rs0 m0 vargs: forall lbs1, seval_builtin_args ge sp m rs0 m0 lbs1 vargs -> forall lbs2, (seval_list_builtin_sval ge sp lbs1 rs0 m0) = (seval_list_builtin_sval ge sp lbs2 rs0 m0) -> seval_builtin_args ge sp m rs0 m0 lbs2 vargs. Proof. - induction 1. - - simpl. intros. - exploit seval_list_builtin_sval_nil; eauto. intro. subst. constructor. - - eapply seval_builtin_arg_sval in H. destruct H as (ba & A & B). - eapply seval_builtin_args_sval in H0. destruct H0 as (lba & A' & B'). - intros. destruct lbs2. - + simpl in H. rewrite A in H. rewrite A' in H. - discriminate. - + constructor. 2: apply IHlist_forall2. 2: admit. -Admitted. + intros. exploit seval_builtin_args_sval; eauto. + intros (ba & X1 & X2). + eapply seval_builtin_sval_args; eauto. + congruence. +Qed. (* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract the [match_states] *) Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (ctx: simu_proof_context f): sfval -> sfval -> Prop := |