diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 14:57:24 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 14:57:24 +0200 |
commit | 2a5715729f6454a9e664fcce52f269ee8c13e9e1 (patch) | |
tree | f1f1c8a200a6a78cfc349e1d8bb9ea3d63b39683 /backend | |
parent | e7da402f36d030484d11960cf12581fd1c1f159a (diff) | |
download | compcert-kvx-2a5715729f6454a9e664fcce52f269ee8c13e9e1.tar.gz compcert-kvx-2a5715729f6454a9e664fcce52f269ee8c13e9e1.zip |
Itailcall
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Duplicate.v | 9 | ||||
-rw-r--r-- | backend/Duplicateproof.v | 10 |
2 files changed, 17 insertions, 2 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index ec03009d..24fb8e78 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -116,6 +116,15 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different ri in Icall") else Error (msg "Different signatures in Icall") | _ => Error (msg "verify_match_inst Icall") end + | Itailcall s ri lr => match tinst with + | Itailcall s' ri' lr' => + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then OK tt + else Error (msg "Different lr in Itailcall") + else Error (msg "Different ri in Itailcall") + else Error (msg "Different signatures in Itailcall") + | _ => Error (msg "verify_match_inst Itailcall") end | Ibuiltin ef lbar brr n => match tinst with | Ibuiltin ef' lbar' brr' n' => do u <- verify_is_copy revmap n n'; diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 37c583df..aa605bea 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -26,8 +26,8 @@ Inductive match_inst (is_copy: node -> option node): instruction -> instruction is_copy n' = (Some n) -> match_inst is_copy (Istore m a lr r n) (Istore m a lr r n') | match_inst_call: forall n n' s ri lr r, is_copy n' = (Some n) -> match_inst is_copy (Icall s ri lr r n) (Icall s ri lr r n') - | match_inst_tailcall: forall n n' s ri lr, - is_copy n' = (Some n) -> match_inst is_copy (Itailcall s ri lr) (Itailcall s ri lr) + | match_inst_tailcall: forall s ri lr, + match_inst is_copy (Itailcall s ri lr) (Itailcall s ri lr) | match_inst_builtin: forall n n' ef la br, is_copy n' = (Some n) -> match_inst is_copy (Ibuiltin ef la br n) (Ibuiltin ef la br n') | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr, @@ -114,6 +114,12 @@ Proof. destruct (Pos.eq_dec _ _); try discriminate. eapply verify_is_copy_correct_one. destruct x. eassumption. subst. constructor. +(* Itailcall *) + - destruct i'; try (inversion H; fail). + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. clear H. + constructor. (* Ibuiltin *) - destruct i'; try (inversion H; fail). monadInv H. destruct (external_function_eq _ _); try discriminate. |