diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 08:17:07 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 08:17:07 +0200 |
| commit | 7a2137b50bd494033a2dcda76be44e6a32e12208 (patch) | |
| tree | 1952452f694ffd84781858aa6f4ab6719d12281c /aarch64 | |
| parent | 68edea74c5ac8b4767f5a19d1aadc072959e1107 (diff) | |
| download | compcert-kvx-7a2137b50bd494033a2dcda76be44e6a32e12208.tar.gz compcert-kvx-7a2137b50bd494033a2dcda76be44e6a32e12208.zip | |
Idea for find_instr_bblock's recursive case
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 42 |
1 files changed, 35 insertions, 7 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 2c693b25..b4765978 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -124,13 +124,6 @@ Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop := i = control_to_instruction cfi -> is_nth_inst bb n i. -Lemma find_instr_bblock n pos lb tlb bb: - find_bblock pos lb = Some bb -> - unfold lb = OK tlb -> - 0 <= n < size bb -> - exists i, is_nth_inst bb n i /\ Asm.find_instr (pos+n) tlb = Some i. -Admitted. - (* Asmblock and Asm share the same definition of state *) Definition match_states (s1 s2 : state) := s1 = s2. @@ -631,6 +624,41 @@ Proof. intros n H; destruct (zeq _ _); (try eapply IHl); omega. Qed. +Lemma find_instr_bblock_tail: + forall pos c i bb tbb, + Asm.find_instr pos c = Some i -> + unfold_bblock bb = OK tbb -> + Asm.find_instr (pos + size bb ) (tbb ++ c) = Some i. +Proof. +Admitted. + +Lemma find_instr_bblock: + forall lb pos n bb tlb + (FINDBB: find_bblock pos lb = Some bb) + (UNFOLD: unfold lb = OK tlb) + (SIZE: 0 <= n < size bb), + exists i, is_nth_inst bb n i /\ Asm.find_instr (pos+n) tlb = Some i. +Proof. + induction lb. + - intros ? ? ? ? FINDBB. inversion FINDBB. + - intros pos n bb tlb FINDBB UNFOLD SIZE. + destruct pos. + + admit. + + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. + inversion UNFOLD as (UNFOLD'). + apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')). + apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD' & TLB)). + inversion TLB. + + generalize (IHlb _ n _ _ FINDBB UNFOLD'). intros IH. + destruct IH as (? & (IH_is_nth & IH_find_instr)); eauto. + eexists; split. + * apply IH_is_nth. + * replace (Z.pos p + n) with (Z.pos p + n - size a + size a) by omega. + eapply find_instr_bblock_tail; try assumption. + replace (Z.pos p + n - size a) with (Z.pos p - size a + n) by omega. + apply IH_find_instr. +Admitted. Lemma exec_header_simulation b ofs f bb rs m: forall (ATPC: rs PC = Vptr b ofs) |