From d3b2c5637600704caf0cf8babbc55a4708b8811f Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 17 Jul 2020 08:23:41 +0200 Subject: suggestion of translation from find_bblock to find_instr --- aarch64/Asmgenproof.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'aarch64') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 6b73c5d6..342b98d0 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -75,6 +75,28 @@ Lemma functions_translated: Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_ptr_transf_partial TRANSF). +Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop := + | is_nth_label l: + list_nth_z (header bb) n = Some l -> + i = Asm.Plabel l -> + is_nth_inst bb n i + | is_nth_basic bi: + list_nth_z (body bb) (n - list_length_z (header bb)) = Some bi -> + basic_to_instruction bi = OK i -> + is_nth_inst bb n i + | is_nth_ctlflow cfi: + (exit bb) = Some cfi -> + n = size bb - 1 -> + i = control_to_instruction cfi -> + is_nth_inst bb n i. + +Lemma find_bblock_find_instr_correct pos n 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. -- cgit