diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-12 19:18:22 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:38:34 +0200 |
commit | b4130798bd428ad3586baa17b0f991018854997a (patch) | |
tree | 7330a228071a119a60a0fcb0fe9448d7f8262de6 /backend | |
parent | 659c06eb4fabce59751476ddeb2e065759f19765 (diff) | |
download | compcert-b4130798bd428ad3586baa17b0f991018854997a.tar.gz compcert-b4130798bd428ad3586baa17b0f991018854997a.zip |
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.
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Asmgenproof0.v | 26 |
1 files changed, 26 insertions, 0 deletions
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 *) |