diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 14:27:32 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 14:27:32 +0200 |
| commit | 5ff1a009561973e65437edadd752f627c12c1a29 (patch) | |
| tree | 018b292d946990ebb9f36ed21d59ccfe0d7e6b25 /backend/Selectionproof.v | |
| parent | 515fbe8f873d9dd1b246b0dab7531103b1b59cf6 (diff) | |
| download | compcert-kvx-5ff1a009561973e65437edadd752f627c12c1a29.tar.gz compcert-kvx-5ff1a009561973e65437edadd752f627c12c1a29.zip | |
itemize the proof (better for debugging)
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 50ff377a..23d10382 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -856,35 +856,35 @@ Remark find_label_commut: Proof. induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) - unfold store. destruct (addressing m (sel_expr e)); simpl; auto. +- unfold store. destruct (addressing m (sel_expr e)); simpl; auto. (* call *) - destruct (classify_call (prog_defmap cunit) e); simpl; auto. +- destruct (classify_call (prog_defmap cunit) e); simpl; auto. (* tailcall *) - destruct (classify_call (prog_defmap cunit) e); simpl; auto. +- destruct (classify_call (prog_defmap cunit) e); simpl; auto. (* seq *) - exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. +- exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ]; intuition. apply IHs2; auto. (* ifthenelse *) - exploit (IHs1 k); eauto. +- exploit (IHs1 k); eauto. destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ]; destruct (find_label lbl x k') as [[sy ky] | ]; intuition. apply IHs2; auto. (* loop *) - apply IHs. constructor; auto. simpl; rewrite EQ; auto. auto. +- apply IHs. constructor; auto. simpl; rewrite EQ; auto. auto. (* block *) - apply IHs. constructor; auto. auto. +- apply IHs. constructor; auto. auto. (* switch *) - destruct b. +- destruct b. destruct (validate_switch Int64.modulus n l (compile_switch Int64.modulus n l)); inv SE. simpl; auto. destruct (validate_switch Int.modulus n l (compile_switch Int.modulus n l)); inv SE. simpl; auto. (* return *) - destruct o; inv SE; simpl; auto. +- destruct o; inv SE; simpl; auto. (* label *) - destruct (ident_eq lbl l). auto. apply IHs; auto. +- destruct (ident_eq lbl l). auto. apply IHs; auto. Qed. Definition measure (s: Cminor.state) : nat := |