diff options
-rw-r--r-- | backend/Duplicate.v | 33 | ||||
-rw-r--r-- | backend/Duplicateproof.v | 2 |
2 files changed, 34 insertions, 1 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index a18892cd..07577704 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -39,6 +39,39 @@ Definition verify_mapping_entrypoint (f: function) (xf: xfunction) : res unit := end end. +Definition verify_is_copy revmap n n' := + match revmap!n' with + | None => Error(msg "verify_is_copy None") + | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + end. + +Definition verify_match_inst revmap inst tinst := + match inst with + | Inop n => match tinst with Inop n' => do u <- verify_is_copy revmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end + | _ => Error(msg "not implemented") + end. + +Definition verify_mapping_mn f xf (m: positive*positive) := + let (tn, n) := m in + match (fn_code f)!n with + | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code f)!n") + | Some inst => match (fn_code (fn_RTL xf))!tn with + | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code xf)!tn") + | Some tinst => verify_match_inst (fn_revmap xf) inst tinst + end + end. + +Fixpoint verify_mapping_mn_rec f xf lm := + match lm with + | nil => OK tt + | m :: lm => do u <- verify_mapping_mn f xf m; + do u2 <- verify_mapping_mn_rec f xf lm; + OK tt + end. + +Definition verify_mapping_match_nodes (f: function) (xf: xfunction) : res unit := + verify_mapping_mn_rec f xf (PTree.elements (fn_revmap xf)). + (** Verifies that the [fn_revmap] of the translated function [xf] is giving correct information in regards to [f] *) Definition verify_mapping (f: function) (xf: xfunction) : res unit := do u <- verify_mapping_entrypoint f xf; OK tt. diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index fe26db55..4ffd2c5d 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -41,7 +41,7 @@ Inductive match_inst (is_copy: node -> option node): instruction -> instruction Axiom revmap_correct: forall f xf n n', transf_function_aux f = OK xf -> (fn_revmap xf)!n' = Some n -> - (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n => (fn_revmap xf)!n) i i'). + (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n' => (fn_revmap xf)!n') i i'). Theorem revmap_entrypoint: forall f xf, transf_function_aux f = OK xf -> (fn_revmap xf)!(fn_entrypoint (fn_RTL xf)) = Some (fn_entrypoint f). |