diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 17:06:06 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 17:06:06 +0200 |
commit | cb7d444a5a97626a794f2167c2a4bc4d51f4ed67 (patch) | |
tree | ea436e9752befd8b1fba3080e0badb330fc361e2 /backend/Duplicate.v | |
parent | 5ffa8534d09272e5f44c51193e74cffdbc2b043c (diff) | |
download | compcert-kvx-cb7d444a5a97626a794f2167c2a4bc4d51f4ed67.tar.gz compcert-kvx-cb7d444a5a97626a794f2167c2a4bc4d51f4ed67.zip |
Finished Duplicate proof.
Diffstat (limited to 'backend/Duplicate.v')
-rw-r--r-- | backend/Duplicate.v | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 0f3c2ba9..d1458bd4 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -45,6 +45,17 @@ Definition verify_is_copy revmap n n' := | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end end. +Fixpoint verify_is_copy_list revmap ln ln' := + match ln with + | n::ln => match ln' with + | n'::ln' => do u <- verify_is_copy revmap n n'; + verify_is_copy_list revmap ln ln' + | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => match ln' with + | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | nil => OK tt end + end. + Lemma product_eq {A B: Type} : (forall (a b: A), {a=b} + {a<>b}) -> (forall (c d: B), {c=d} + {c<>d}) -> @@ -152,12 +163,18 @@ Definition verify_match_inst revmap inst tinst := else Error (msg "Different cond in Icond") | _ => Error (msg "verify_match_inst Icond") end + | Ijumptable r ln => match tinst with + | Ijumptable r' ln' => + do u <- verify_is_copy_list revmap ln ln'; + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Ijumptable") + | _ => Error (msg "verify_match_inst Ijumptable") end + | Ireturn or => match tinst with | Ireturn or' => if (option_eq Pos.eq_dec or or') then OK tt else Error (msg "Different or in Ireturn") | _ => Error (msg "verify_match_inst Ireturn") end - | _ => Error(msg "not implemented") end. Definition verify_mapping_mn f xf (m: positive*positive) := |