diff options
author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-15 08:39:44 +0200 |
---|---|---|
committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-15 08:39:44 +0200 |
commit | de570ba3c125334ae9d180f3017a16854e41f222 (patch) | |
tree | 165baaae5b67350ecfa5418095f99188be4ce928 /aarch64/Asmgenproof.v | |
parent | d83bdbfb0f32f41fd979d37d6972e92c2f27325c (diff) | |
download | compcert-kvx-de570ba3c125334ae9d180f3017a16854e41f222.tar.gz compcert-kvx-de570ba3c125334ae9d180f3017a16854e41f222.zip |
Add definition of match_internal
This relation will hold between Asmblock and Asm states while inside an
Asmblock block.
Diffstat (limited to 'aarch64/Asmgenproof.v')
-rw-r--r-- | aarch64/Asmgenproof.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 97612601..93a0ef66 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -77,6 +77,24 @@ Proof (Genv.find_funct_ptr_transf_partial TRANSF). (* Asmblock and Asm share the same definition of state *) Definition match_states (s1 s2 : state) := s1 = s2. +Inductive match_internal: forall n, state -> state -> Prop := + | match_internal_intro n rs1 m1 rs2 m2 + (MEM: m1 = m2) + (AG: forall r, r <> PC -> rs1 r = rs2 r) + (AGPC: Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC) + : match_internal n (State rs1 m1) (State rs2 m2). + +(* match_internal from match_states *) +Lemma mi_from_ms: + forall rs1 m1 rs2 m2 b ofs, + match_states (State rs1 m1) (State rs2 m2) -> + rs1#PC = Vptr b ofs -> + match_internal 0 (State rs1 m1) (State rs2 m2). +Proof. + intros rs1 m1 rs2 m2 b ofs MS PCVAL. + inv MS; constructor; auto; unfold Val.offset_ptr; + rewrite PCVAL; rewrite Ptrofs.add_zero; reflexivity. +Qed. Lemma transf_initial_states: forall s1, Asmblock.initial_state prog s1 -> exists s2, Asm.initial_state tprog s2 /\ match_states s1 s2. |