From 3f3d7b1fbc4d7ed27897b33a0a0106fe50b835ef Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Wed, 15 Jul 2020 14:29:00 +0200 Subject: First go at showing that translated cfi behave the same Import Axioms in order to use functional extensionality --- aarch64/Asmgenproof.v | 191 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 191 insertions(+) diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 10586f0e..29c746ba 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -20,6 +20,7 @@ Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock. Require Machblockgenproof Asmblockgenproof. Require Import Asmgen. +Require Import Axioms. Module Asmblock_PRESERVATION. @@ -206,6 +207,196 @@ Proof. * rewrite <- functions_bound_max_pos; eauto; omega. Qed. +Lemma incrPC_agree_but_pc: + forall rs r ofs, + r <> PC -> + (incrPC ofs rs)#r = rs#r. +Proof. + intros rs r ofs NOTPC. + unfold incrPC; unfold Pregmap.set; destruct (PregEq.eq r PC). + - contradiction. + - reflexivity. +Qed. + +Lemma cf_instruction_simulated: + forall size_b f tf rs1 m1 rs1' m1' cfi, + (* there are no emnpty basic blocks *) + size_b >= 1 -> + exec_exit ge f (Ptrofs.repr size_b) rs1 m1 (Some (PCtlFlow cfi)) E0 rs1' m1' -> + forall rs2 m2, match_internal (size_b - 1) (State rs1 m1) (State rs2 m2) -> + exists rs2' m2', Asm.exec_instr tge tf (cf_instruction_to_instruction cfi) + rs2 m2 = Next rs2' m2' + /\ match_states (State rs1' m1') (State rs2' m2'). +Proof. + intros. (* XXX auto-generated names *) + destruct cfi. + - (* Pb *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + unfold incrPC, Asm.goto_label, goto_label. + inv H1. rewrite <- AGPC. + (* TODO: show that Asm.label_pos and label_pos behave the same * + * show that both Val.offset_ptr calculation return Vptr _ _ *) + admit. + + constructor. + - (* Pbc *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + admit. + + constructor. + - (* Pbl *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + rewrite symbol_addresses_preserved. + unfold incrPC. + assert ( Val.offset_ptr (rs2 PC) Ptrofs.one + = Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b) + ) as EQPC. { + inv H1. rewrite <- AGPC. + rewrite Val.offset_ptr_assoc. + unfold Ptrofs.one. + rewrite Ptrofs.add_unsigned. + rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr. + rewrite Z.sub_add; reflexivity. + * split; try omega. apply one_le_max_unsigned. + * split; try omega. + (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit. + } rewrite EQPC. + rewrite Pregmap.gss. + assert ( (rs2 # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) + # PC <- (Genv.symbol_address ge id Ptrofs.zero) + = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) + # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) + # PC <- (Genv.symbol_address ge id Ptrofs.zero) + ) as EQRS. { + unfold Pregmap.set. + apply functional_extensionality. + intros x. destruct (PregEq.eq x X30) as [X | X]. + - rewrite X. reflexivity. + - destruct (PregEq.eq x PC) as [X' | X']; auto. + inv H1. rewrite AG; auto. + } rewrite EQRS. inv H1. reflexivity. + + constructor. + - (* Pbs *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + rewrite symbol_addresses_preserved. + unfold incrPC. + assert ( (rs2 # PC <- (Genv.symbol_address ge id Ptrofs.zero)) + = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) + # PC <- (Genv.symbol_address ge id Ptrofs.zero) + ) as EQRS. { + unfold Pregmap.set; apply functional_extensionality. intros x. + destruct (PregEq.eq x PC) as [X | X]; auto. + inv H1; rewrite AG; auto. + } rewrite EQRS; inv H1; auto. + + constructor. + - (* Pblr *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + unfold incrPC. rewrite Pregmap.gss. rewrite Pregmap.gso; try discriminate. + assert ( (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) # PC <- (rs2 r) + = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) + # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) + # PC <- (rs1 r) + ) as EQRS. { + unfold Pregmap.set. apply functional_extensionality. + intros x; destruct (PregEq.eq x PC) as [X | X]. + - inv H1; rewrite AG; auto. discriminate. + - destruct (PregEq.eq x X30) as [X' | X']. + + inv H1. rewrite <- AGPC. + rewrite Val.offset_ptr_assoc. unfold Ptrofs.one. + rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr. + rewrite Z.sub_add; reflexivity. + * split; try omega. apply one_le_max_unsigned. + * split; try omega. + (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit. + + inv H1; rewrite AG; auto. + } rewrite EQRS. inv H1; auto. + + constructor. + - (* Pbr *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + unfold incrPC. rewrite Pregmap.gso; try discriminate. + + assert ( rs2 # PC <- (rs2 r) + = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) + # PC <- (rs1 r) + ) as EQRS. { + unfold Pregmap.set; apply functional_extensionality. + intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate. + - inv H1; rewrite AG; try discriminate. reflexivity. + - inv H1; rewrite AG; auto. + } rewrite EQRS; inv H1; auto. + + constructor. + - (* Pret *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. + rewrite <- H3. unfold incrPC. rewrite Pregmap.gso; try discriminate. + assert ( rs2 # PC <- (rs2 r) + = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) # PC <- (rs1 r) + ) as EQRS. { + unfold Pregmap.set; apply functional_extensionality. + intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate. + - inv H1; rewrite AG; try discriminate. reflexivity. + - inv H1; rewrite AG; auto. + } rewrite EQRS; inv H1; auto. + + constructor. + - (* Pcbnz *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + unfold eval_neg_branch. destruct sz. + * simpl. inv H1. rewrite <- AG; try discriminate. + replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs1 r). 2: { + symmetry. rewrite incrPC_agree_but_pc; try discriminate; auto. + } + assert (Asm.nextinstr rs2 = (incrPC (Ptrofs.repr size_b) rs1)) as EQTrue. { + unfold incrPC, Asm.nextinstr, Ptrofs.one. rewrite <- AGPC. + rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned. + rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr. + - rewrite Z.sub_add; unfold Pregmap.set; apply functional_extensionality. + intros x; destruct (PregEq.eq x PC) as [ X | X ]; auto. rewrite AG; trivial. + - split; try omega. apply one_le_max_unsigned. + - split; try omega. + (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit. + } rewrite EQTrue. fold Stuck. + (* TODO show that Asm.goto_label and goto_label behave the same *) admit. + * (* TODO see/merge above case *) admit. + + constructor. + - (* Pcbz *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + unfold eval_branch. (* TODO, will be very similar to Pcbnz *) admit. + + constructor. + - (* Pcbz *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + unfold eval_branch. + replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs2 r). 2: { + symmetry; rewrite incrPC_agree_but_pc; try discriminate; auto; + inv H1; rewrite AG; try discriminate; auto. + } (* TODO, cf. Pcbnz *) admit. + + constructor. + - (* Ptbz *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + (* TODO, cf. Pcbz *) admit. + + constructor. + - (* Pbtbl *) + simpl; eexists; eexists; split. + + inv H0. simpl in H3. rewrite <- H3. + 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 H1; rewrite AG; auto. + } rewrite <- EQUNDEFX16. + (* TODO Asm.goto_label and goto_label *) admit. + + constructor. +Admitted. + Lemma step_simulation s1 t s1': Asmblock.step lk ge s1 t s1' -> forall s2, match_states s1 s2 -> -- cgit