From 173e6c25b2937d6e6941973aa7b116e1d6405513 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 10:10:34 +0100 Subject: Porting the BTL non-trap loads approach to RTL --- scheduling/RTLtoBTLproof.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 0ca93bce..6ec32ffc 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -631,9 +631,13 @@ Proof. erewrite eval_operation_preserved in H12. erewrite H12 in BTL_RUN; simpl in BTL_RUN; auto. intros; rewrite <- symbols_preserved; trivial. } - all: (* Bload / Bstore *) - erewrite eval_addressing_preserved in H12; - try erewrite H12 in BTL_RUN; try erewrite H13 in BTL_RUN; + (* Bload/Bstore *) + inv H12; [ idtac | destruct (eval_addressing) eqn:EVAL in LOAD;[ specialize (LOAD v) |] ]; + rename LOAD into MEMT. + 4: rename H12 into EVAL; rename H13 into MEMT. + all: + erewrite eval_addressing_preserved in EVAL; + try erewrite EVAL in BTL_RUN; try erewrite MEMT in BTL_RUN; simpl in BTL_RUN; try destruct trap; auto; intros; rewrite <- symbols_preserved; trivial. - (* mib_cond *) -- cgit