From 0e439055e450d63ace2366653cd558de1a073bed Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 26 Nov 2020 11:39:16 +0100 Subject: Fine tuning for Pfmovimm - Functions to check a float logical immediate were translated from ocaml target printer in coq Asmblock - Some proof are admitted for now (we'll see if it is a good idea after some tests) --- aarch64/Asmgenproof.v | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index f441f20e..9077a292 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -786,9 +786,9 @@ Lemma exec_arith_instr_dont_move_PC ai rs rs': forall Proof. destruct ai; simpl; intros; try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate). - - destruct i; simpl in BASIC; + - admit. (* destruct i; simpl in BASIC; unfold compare_long in BASIC; rewrite <- BASIC; - repeat rewrite Pregmap.gso; try discriminate; reflexivity. + repeat rewrite Pregmap.gso; try discriminate; reflexivity. *) - destruct i; simpl in BASIC. 1,2: rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity. destruct sz; @@ -805,7 +805,8 @@ Proof. try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). -Qed. +(* Qed. *) +Admitted. Lemma exec_basic_dont_move_PC bi rs m rs' m': forall (BASIC: exec_basic lk ge bi rs m = Next rs' m'), @@ -1164,7 +1165,8 @@ Proof. try (exploit next_inst_preserved; eauto); try (repeat destruct_reg_size); try (destruct_ir0_reg). - 1,2: (* Special case for Pfmovimmd / Pfmovimms *) + all: admit. + (* 1,2: (* Special case for Pfmovimmd / Pfmovimms *) try (monadInv TRANSBI); try (destruct_reg_inv); try (inv_matchi); @@ -1173,7 +1175,7 @@ Proof. repeat (eapply match_internal_nextinstr_set_parallel; try congruence); try (econstructor; eauto); try (eapply nextinstr_agree_but_pc; eauto); - try (eapply ptrofs_nextinstr_agree; eauto). + try (eapply ptrofs_nextinstr_agree; eauto). *) } 1,2,3,4,5: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *) destruct i; @@ -1298,7 +1300,8 @@ Proof. try (exploit next_inst_preserved; eauto); rewrite symbol_addresses_preserved; eauto; try (find_rwrt_ag). -Qed. +(* Qed. *) +Admitted. Lemma find_basic_instructions b ofs f bb tc: forall (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) -- cgit From c7f3bd8555c1cae001cc93d21398b52b19d58df0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 26 Nov 2020 23:43:37 +0100 Subject: Proof of Pfmovimm fine tuned OK, moving float checks in Asm Also some simplifications in Asmblockdeps --- aarch64/Asmgenproof.v | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 9077a292..ba785b48 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -786,9 +786,9 @@ Lemma exec_arith_instr_dont_move_PC ai rs rs': forall Proof. destruct ai; simpl; intros; try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate). - - admit. (* destruct i; simpl in BASIC; - unfold compare_long in BASIC; rewrite <- BASIC; - repeat rewrite Pregmap.gso; try discriminate; reflexivity. *) + - destruct i; simpl in BASIC; + try destruct (negb _); rewrite <- BASIC; + repeat rewrite Pregmap.gso; try discriminate; reflexivity. - destruct i; simpl in BASIC. 1,2: rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity. destruct sz; @@ -805,8 +805,7 @@ Proof. try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). -(* Qed. *) -Admitted. +Qed. Lemma exec_basic_dont_move_PC bi rs m rs' m': forall (BASIC: exec_basic lk ge bi rs m = Next rs' m'), @@ -1165,17 +1164,18 @@ Proof. try (exploit next_inst_preserved; eauto); try (repeat destruct_reg_size); try (destruct_ir0_reg). - all: admit. - (* 1,2: (* Special case for Pfmovimmd / Pfmovimms *) + 1,2: (* Special case for Pfmovimmd / Pfmovimms *) try (monadInv TRANSBI); try (destruct_reg_inv); try (inv_matchi); inversion BASIC; clear BASIC; subst; + try (destruct (is_immediate_float64 _)); + try (destruct (is_immediate_float32 _)); eexists; eexists; split; eauto; repeat (eapply match_internal_nextinstr_set_parallel; try congruence); try (econstructor; eauto); try (eapply nextinstr_agree_but_pc; eauto); - try (eapply ptrofs_nextinstr_agree; eauto). *) + try (eapply ptrofs_nextinstr_agree; eauto). } 1,2,3,4,5: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *) destruct i; @@ -1300,8 +1300,7 @@ Proof. try (exploit next_inst_preserved; eauto); rewrite symbol_addresses_preserved; eauto; try (find_rwrt_ag). -(* Qed. *) -Admitted. +Qed. Lemma find_basic_instructions b ofs f bb tc: forall (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) -- cgit