diff options
author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 13:17:07 +0200 |
---|---|---|
committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 13:17:07 +0200 |
commit | 238bf23479d90a4cbb77d5bdf94c54ca761adc92 (patch) | |
tree | 2f5824b4a18c58a4df5f38b2a1403a546f3600f8 | |
parent | f3d0622f2dc0c3398ec9f81d9367fbb70e40bbff (diff) | |
download | compcert-kvx-238bf23479d90a4cbb77d5bdf94c54ca761adc92.tar.gz compcert-kvx-238bf23479d90a4cbb77d5bdf94c54ca761adc92.zip |
Begin proof of exec_exit_simulation_plus
Mostly proving the absurd cases following inversion of is_nth_inst
-rw-r--r-- | aarch64/Asmgenproof.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 9e12655a..4b18e712 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -759,6 +759,26 @@ Lemma exec_body_dont_move_PC bb rs m rs' m': forall rs PC = rs' PC. Admitted. +Lemma list_nth_z_range_exceeded A (l : list A) n: + n >= list_length_z l -> + list_nth_z l n = None. +Proof. + intros N. + remember (list_nth_z l n) as opt eqn:H. symmetry in H. + destruct opt; auto. + exploit list_nth_z_range; eauto. omega. +Qed. + +Lemma last_instruction_cannot_be_label bb: + list_nth_z (header bb) (size bb - 1) = None. +Proof. + assert (list_length_z (header bb) <= size bb - 1). { + rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). omega. + } + remember (list_nth_z (header bb) (size bb - 1)) as label_opt; destruct label_opt; auto; + exploit list_nth_z_range; eauto; omega. +Qed. + Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) @@ -767,6 +787,28 @@ Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall (EXIT: exec_exit ge f (Ptrofs.repr (size bb)) rs m (exit bb) t rs' m') (ATPC: rs PC = Vptr b ofs), plus Asm.step tge s2 t (State rs' m'). +Proof. + intros. apply plus_one. + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & _). + + exploit (find_instr_bblock (size bb - 1)); eauto. + { generalize (bblock_size_pos bb). omega. } + intros (i' & NTH & FIND_INSTR). + inv NTH. + + rewrite last_instruction_cannot_be_label in *. discriminate. + + destruct (exit bb) as [ctrl |] eqn:NEMPTY_EXIT'. 2: { contradiction. } + rewrite bblock_size_aux in *. rewrite NEMPTY_EXIT' in *. simpl in *. + (* XXX: Is there a better way to simplify this expression i.e. automatically? *) + replace (list_length_z (header bb) + list_length_z (body bb) + 1 - 1 - + list_length_z (header bb)) with (list_length_z (body bb)) in H by omega. + rewrite list_nth_z_range_exceeded in H; try omega. discriminate. + + destruct cfi. + * (* controlf low instruction *) + rewrite H in EXIT. + inv EXIT. + admit. + * (* builtin *) admit. Admitted. Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall |