diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:27 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:27 +0100 |
| commit | 1acafe8f7f61a8908f47de4c98f3d873f8f9afbd (patch) | |
| tree | eb32229e985eb5b5150ce173f3f9ff120a6bac08 /backend | |
| parent | 6bb5ae7ee76bee8b8be0c99363975bafa5753c0b (diff) | |
| download | compcert-kvx-1acafe8f7f61a8908f47de4c98f3d873f8f9afbd.tar.gz compcert-kvx-1acafe8f7f61a8908f47de4c98f3d873f8f9afbd.zip | |
Verificator finished for handling reversed Icond
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Duplicate.v | 15 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 14 |
2 files changed, 18 insertions, 11 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index c53ff425..18869f39 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -138,12 +138,15 @@ Definition verify_match_inst dupmap inst tinst := | Icond cond lr n1 n2 => match tinst with | Icond cond' lr' n1' n2' => - do u1 <- verify_is_copy dupmap n1 n1'; - do u2 <- verify_is_copy dupmap n2 n2'; - if (eq_condition cond cond') then - if (list_eq_dec Pos.eq_dec lr lr') then OK tt - else Error (msg "Different lr in Icond") - else Error (msg "Different cond in Icond") + if (list_eq_dec Pos.eq_dec lr lr') then + if (eq_condition cond cond') then + do u1 <- verify_is_copy dupmap n1 n1'; + do u2 <- verify_is_copy dupmap n2 n2'; OK tt + else if (eq_condition (negate_condition cond) cond') then + do u1 <- verify_is_copy dupmap n1 n2'; + do u2 <- verify_is_copy dupmap n2 n1'; OK tt + else Error (msg "Incompatible conditions in Icond") + else Error (msg "Different lr in Icond") | _ => Error (msg "verify_match_inst Icond") end | Ijumptable r ln => match tinst with diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index b99fadac..c285e4b3 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -177,12 +177,16 @@ Proof. destruct (builtin_res_eq_pos _ _); try discriminate. subst. constructor. assumption. (* Icond *) - - destruct i'; try (inversion H; fail). monadInv H. - destruct x. eapply verify_is_copy_correct in EQ. - destruct x0. eapply verify_is_copy_correct in EQ1. - destruct (eq_condition _ _); try discriminate. + - destruct i'; try (inversion H; fail). destruct (list_eq_dec _ _ _); try discriminate. subst. - constructor; assumption. + destruct (eq_condition _ _); try discriminate. + + monadInv H. destruct x. eapply verify_is_copy_correct in EQ. + destruct x0. eapply verify_is_copy_correct in EQ1. + constructor; assumption. + + destruct (eq_condition _ _); try discriminate. + monadInv H. destruct x. eapply verify_is_copy_correct in EQ. + destruct x0. eapply verify_is_copy_correct in EQ1. + constructor; assumption. (* Ijumptable *) - destruct i'; try (inversion H; fail). monadInv H. destruct x. eapply verify_is_copy_list_correct in EQ. |