From b4130798bd428ad3586baa17b0f991018854997a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 12 May 2019 19:18:22 +0200 Subject: Asmgenproof0: add predicate exec_straight0 This is a variant of exec_straight where it is allowed to take zero steps. In other words, exec_straight0 is the "star" relation, while exec_straight is the "plus" relation. In the end we need "plus" relations in simulation diagrams, to show the absence of stuttering. But the "star" relation exec_straight0 is useful to reason about code fragments that are always preceded or followed by at least one instruction. --- backend/Asmgenproof0.v | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) (limited to 'backend/Asmgenproof0.v') diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 70c4323c..111e435f 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -897,6 +897,32 @@ Proof. apply code_tail_next_int with i; auto. Qed. +(** A variant that supports zero steps of execution *) + +Inductive exec_straight0: code -> regset -> mem -> + code -> regset -> mem -> Prop := + | exec_straight0_none: + forall c rs m, + exec_straight0 c rs m c rs m + | exec_straight0_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_straight0 c rs2 m2 c' rs3 m3 -> + exec_straight0 (i :: c) rs1 m1 c' rs3 m3. + +Lemma exec_straight_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_straight0 c rs2 m2 c' rs3 m3 -> + exec_straight (i :: c) rs1 m1 c' rs3 m3. +Proof. + intros. revert i rs1 m1 H H0. revert H1. induction 1; intros. +- apply exec_straight_one; auto. +- eapply exec_straight_step; eauto. +Qed. + End STRAIGHTLINE. (** * Properties of the Mach call stack *) -- cgit