diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 16:51:04 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 16:51:04 +0100 |
| commit | 6bb5ae7ee76bee8b8be0c99363975bafa5753c0b (patch) | |
| tree | a30c2ac2c9fca3e26b84e5c9520d36cc633425c2 /backend/Duplicateproof.v | |
| parent | 04a46f516487557df00f43453c8decbc8567c458 (diff) | |
| download | compcert-kvx-6bb5ae7ee76bee8b8be0c99363975bafa5753c0b.tar.gz compcert-kvx-6bb5ae7ee76bee8b8be0c99363975bafa5753c0b.zip | |
Added clause in match_inst to allow Icond reversal
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 67d16580..b99fadac 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -26,6 +26,9 @@ Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr, dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) -> match_inst dupmap (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot') + | match_inst_revcond: forall ifso ifso' ifnot ifnot' c lr, + dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) -> + match_inst dupmap (Icond c lr ifso ifnot) (Icond (negate_condition c) lr ifnot' ifso') | match_inst_jumptable: forall ln ln' r, list_forall2 (fun n n' => (dupmap!n' = (Some n))) ln ln' -> match_inst dupmap (Ijumptable r ln) (Ijumptable r ln') @@ -464,10 +467,16 @@ Proof. (* Icond *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. - pose symbols_preserved as SYMPRES. - eexists. split. - + eapply exec_Icond; eauto. - + econstructor; eauto. destruct b; auto. + * (* match_inst_cond *) + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Icond; eauto. + + econstructor; eauto. destruct b; auto. + * (* match_inst_revcond *) + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Icond; eauto. rewrite eval_negate_condition. rewrite H0. simpl. eauto. + + econstructor; eauto. destruct b; auto. (* Ijumptable *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. |