From 0c6e2d98365d78283058f3c1497bc0b382771491 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Oct 2020 17:05:44 +0200 Subject: cfi_simu finished --- aarch64/Asmgenproof.v | 51 ++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 36 insertions(+), 15 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index df83e6a7..833c6f03 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1815,21 +1815,42 @@ Proof. destruct b. * exploit next_inst_incr_pc_preserved; eauto. * exploit goto_label_preserved; eauto. - (* - (* Pbtbl *) - simpl; eexists; eexists; split. - + rewrite <- H0. - assert ( rs2 # X16 <- Vundef r1 - = (incrPC (Ptrofs.repr size_b) rs1) # X16 <- Vundef r1 - ) as EQUNDEFX16. { - unfold incrPC, Pregmap.set. - destruct (PregEq.eq r1 X16) as [X16 | X16]; auto. - destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate. - inv MI; rewrite AG; auto. - } rewrite <- EQUNDEFX16. - (* TODO Asm.goto_label and goto_label *) admit. - + constructor. -*) -Admitted. + - (* Pbtbl *) + assert (rs2 # X16 <- Vundef r1 = (incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef r1) + as EQUNDEFX16. { + unfold incrPC, Pregmap.set. + destruct (PregEq.eq r1 X16) as [X16 | X16]; auto. + destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate. + inv MATCHI; rewrite AG; auto. + } rewrite <- EQUNDEFX16 in H0. + destruct_reg_inv; next_stuck_cong. + unfold goto_label, Asm.goto_label in *. + rewrite <- (label_pos_preserved f); auto. + inversion MATCHI; subst. + destruct label_pos; next_stuck_cong. + destruct (((incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef) # X17 <- Vundef PC) eqn:INCRPC; next_stuck_cong. + inversion H0; auto. repeat (econstructor; eauto). + rewrite !Pregmap.gso; try congruence. + rewrite <- AGPC. + unfold incrPC in *. + destruct (rs1 PC) eqn:EQRS1; simpl in *; try discriminate. + replace (((rs2 # X16 <- Vundef) # X17 <- Vundef) # PC <- (Vptr b0 (Ptrofs.repr z))) with + ((((rs1 # PC <- (Vptr b0 (Ptrofs.add i1 (Ptrofs.repr (size bb))))) # X16 <- + Vundef) # X17 <- Vundef) # PC <- (Vptr b (Ptrofs.repr z))); auto. + eapply functional_extensionality; intros x. + destruct (PregEq.eq x PC); subst. + + rewrite Pregmap.gso in INCRPC; try congruence. + rewrite Pregmap.gso in INCRPC; try congruence. + rewrite Pregmap.gss in INCRPC. + rewrite !Pregmap.gss in *; congruence. + + rewrite Pregmap.gso; auto. + rewrite (Pregmap.gso (i := x) (j := PC)); auto. + destruct (PregEq.eq x X17); subst. + * rewrite !Pregmap.gss; auto. + * rewrite !(Pregmap.gso (i := x) (j:= X17)); auto. destruct (PregEq.eq x X16); subst. + -- rewrite !Pregmap.gss; auto. + -- rewrite !Pregmap.gso; auto. +Qed. Lemma last_instruction_cannot_be_label bb: list_nth_z (header bb) (size bb - 1) = None. -- cgit