diff options
| author | Léo Gourdin <leo.gourdin@lilo.org> | 2021-11-02 10:10:34 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@lilo.org> | 2021-11-02 10:10:34 +0100 |
| commit | 173e6c25b2937d6e6941973aa7b116e1d6405513 (patch) | |
| tree | e5f63f343a3d1a1341dc2e8a09f6cdb706226de3 /scheduling/RTLtoBTLproof.v | |
| parent | f9e4d91431334d88992e62a232a9e2ff2f6fcdc9 (diff) | |
| download | compcert-kvx-173e6c25b2937d6e6941973aa7b116e1d6405513.tar.gz compcert-kvx-173e6c25b2937d6e6941973aa7b116e1d6405513.zip | |
Porting the BTL non-trap loads approach to RTL
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 10 |
1 files changed, 7 insertions, 3 deletions
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 *) |