diff options
Diffstat (limited to 'backend/Asmgenproof0.v')
-rw-r--r-- | backend/Asmgenproof0.v | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 70c4323c..3638c465 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -897,6 +897,55 @@ Proof. apply code_tail_next_int with i; auto. Qed. +(** A variant that supports zero steps of execution *) + +Inductive exec_straight_opt: code -> regset -> mem -> code -> regset -> mem -> Prop := + | exec_straight_opt_refl: forall c rs m, + exec_straight_opt c rs m c rs m + | exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2, + exec_straight c1 rs1 m1 c2 rs2 m2 -> + exec_straight_opt c1 rs1 m1 c2 rs2 m2. + +Lemma exec_straight_opt_left: + forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2, + exec_straight c1 rs1 m1 c2 rs2 m2 -> + exec_straight_opt c2 rs2 m2 c3 rs3 m3 -> + exec_straight c1 rs1 m1 c3 rs3 m3. +Proof. + destruct 2; intros. auto. eapply exec_straight_trans; eauto. +Qed. + +Lemma exec_straight_opt_right: + forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2, + exec_straight_opt c1 rs1 m1 c2 rs2 m2 -> + exec_straight c2 rs2 m2 c3 rs3 m3 -> + exec_straight c1 rs1 m1 c3 rs3 m3. +Proof. + destruct 1; intros. auto. eapply exec_straight_trans; eauto. +Qed. + +Lemma exec_straight_opt_step: + forall i c rs1 m1 rs2 m2 c' rs3 m3, + exec_instr ge fn i rs1 m1 = Next rs2 m2 -> + rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> + exec_straight_opt c rs2 m2 c' rs3 m3 -> + exec_straight (i :: c) rs1 m1 c' rs3 m3. +Proof. + intros. inv H1. +- apply exec_straight_one; auto. +- eapply exec_straight_step; eauto. +Qed. + +Lemma exec_straight_opt_step_opt: + forall i c rs1 m1 rs2 m2 c' rs3 m3, + exec_instr ge fn i rs1 m1 = Next rs2 m2 -> + rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> + exec_straight_opt c rs2 m2 c' rs3 m3 -> + exec_straight_opt (i :: c) rs1 m1 c' rs3 m3. +Proof. + intros. apply exec_straight_opt_intro. eapply exec_straight_opt_step; eauto. +Qed. + End STRAIGHTLINE. (** * Properties of the Mach call stack *) |