diff options
-rw-r--r-- | aarch64/Asmblock.v | 11 | ||||
-rw-r--r-- | aarch64/Asmgen.v | 2 | ||||
-rw-r--r-- | aarch64/Asmgenproof.v | 79 |
3 files changed, 68 insertions, 24 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 950e28e9..67ad2aa5 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -217,7 +217,7 @@ Inductive control: Type := | PCtlFlow (i: cf_instruction) (** Pseudo-instructions *) | Pbuiltin (ef: external_function) - (args: list (builtin_arg preg)) (res: builtin_res preg) (**r built-in function (pseudo) *) + (args: list (builtin_arg dreg)) (res: builtin_res dreg) (**r built-in function (pseudo) *) . Coercion PCtlFlow: cf_instruction >-> control. @@ -1900,7 +1900,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out [X30] is used for the return address, and can also be used as temporary. [X16] can be used as temporary. *) -Definition preg_of (r: mreg) : preg := +Definition dreg_of (r: mreg) : dreg := match r with | R0 => X0 | R1 => X1 | R2 => X2 | R3 => X3 | R4 => X4 | R5 => X5 | R6 => X6 | R7 => X7 @@ -1920,6 +1920,9 @@ Definition preg_of (r: mreg) : preg := | F28 => D28 | F29 => D29 | F30 => D30 | F31 => D31 end. +Definition preg_of (r: mreg) : preg := + dreg_of r. + (** Undefine all registers except SP and callee-save registers *) Definition undef_caller_save_regs (rs: regset) : regset := @@ -1979,10 +1982,10 @@ Inductive exec_exit (f: function) size_b (rs: regset) (m: mem): (option control) exec_cfi f cfi (incrPC size_b rs) m = Next rs' m' -> exec_exit f size_b rs m (Some (PCtlFlow cfi)) E0 rs' m' | builtin_step ef args res vargs t vres rs' m': - eval_builtin_args ge rs rs#SP m args vargs -> + eval_builtin_args ge (fun (r: dreg) => rs r) rs#SP m args vargs -> external_call ef ge vargs m t vres m' -> rs' = incrPC size_b - (set_res res vres + (set_res (map_builtin_res DR res) vres (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> exec_exit f size_b rs m (Some (Pbuiltin ef args res)) t rs' m' . diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 4e81a936..5dec10e9 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -288,7 +288,7 @@ Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction Definition control_to_instruction (c: control) := match c with | PCtlFlow i => cf_instruction_to_instruction i - | Pbuiltin ef args res => Asm.Pbuiltin ef args res + | Pbuiltin ef args res => Asm.Pbuiltin ef (List.map (map_builtin_arg DR) args) (map_builtin_res DR res) end. Fixpoint unfold_label (ll: list label) := diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index b2671972..1d13fa7e 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1859,6 +1859,60 @@ Proof. exploit list_nth_z_range; eauto; omega. Qed. +Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m + (ATPC : rs PC = Vptr b ofs) + (MATCHI : match_internal (size bb - 1) + {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} + {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}), + _rs PC = Vptr b (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))). +Proof. + intros; inv MATCHI. rewrite <- AGPC; rewrite ATPC; unfold Val.offset_ptr; eauto. +Qed. + +Lemma find_instr_ofs_somei: forall ofs bb f tc asmi rs m _rs _m + (BOUNDOFS : Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) + (FIND_INSTR : Asm.find_instr (Ptrofs.unsigned ofs + (size bb - 1)) tc = + Some (asmi)) + (MATCHI : match_internal (size bb - 1) + {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} + {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}), + Asm.find_instr (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) + (Asm.fn_code {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}) = + Some (asmi). +Proof. + intros; simpl. + replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) + with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption. + generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros. + unfold Ptrofs.add. + rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega. + rewrite Ptrofs.unsigned_repr; omega. +Qed. + +Lemma eval_builtin_arg_match: forall rs _m _rs a1 b1 + (AG : forall r : preg, r <> PC -> rs r = _rs r) + (EVAL : eval_builtin_arg tge (fun r : dreg => rs r) (rs SP) _m a1 b1), + eval_builtin_arg tge _rs (_rs SP) _m (map_builtin_arg DR a1) b1. +Proof. + intros; induction EVAL; simpl in *; try rewrite AG; try rewrite AG in EVAL; try discriminate; try congruence; eauto with barg. + econstructor. rewrite <- AG; try discriminate; auto. +Qed. + +Lemma eval_builtin_args_match: forall bb rs m _rs _m args vargs + (MATCHI : match_internal (size bb - 1) + {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} + {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}) + (EVAL : eval_builtin_args tge (fun r : dreg => rs r) (rs SP) m args vargs), + eval_builtin_args tge _rs (_rs SP) _m (map (map_builtin_arg DR) args) vargs. +Proof. + intros; inv MATCHI. + induction EVAL; subst. + - econstructor. + - econstructor. + + eapply eval_builtin_arg_match; eauto. + + eauto. +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) @@ -1899,18 +1953,11 @@ Proof. intros (tf & FINDtf' & TRANSf). inversion FINDtf'; subst; clear FINDtf'. exploit exec_cfi_simulation; eauto. (* extract exec_cfi_simulation's conclusion as separate hypotheses *) - (* TODO: ligne ci-dessous à remplacer avec un intro (rs2' & m2' & ...) *) - intro H3; destruct H3; destruct H3; destruct H3. rewrite H5. - inversion MATCHI. + intros (rs2' & m2' & EXECI & MATCHS); rewrite MATCHS. apply plus_one. eapply Asm.exec_step_internal; eauto. - - rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto. - - simpl. replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) - with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption. - generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros. - unfold Ptrofs.add. - rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega. - rewrite Ptrofs.unsigned_repr; omega. + - eapply pc_ptr_exec_step; eauto. + - eapply find_instr_ofs_somei; eauto. * (* builtin *) destruct s2. rewrite H in EXIT. @@ -1921,15 +1968,9 @@ Proof. eapply external_call_symbols_preserved in H10; try (apply senv_preserved). eapply eval_builtin_args_preserved in H6; try (apply symbols_preserved). eapply Asm.exec_step_builtin; eauto. - - inv MATCHI. rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto. - - (* XXX copy-paste from case above *) - simpl. replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) - with (Ptrofs.unsigned ofs + (size bb - 1)); eauto. - generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros. - unfold Ptrofs.add. - rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega. - rewrite Ptrofs.unsigned_repr; omega. - - simpl. (* TODO something like eval_builtin_args_match *) admit. + - eapply pc_ptr_exec_step; eauto. + - eapply find_instr_ofs_somei; eauto. + - eapply eval_builtin_args_match; eauto. - inv MATCHI; eauto. - rewrite H11. (* TODO lemmas for set_res, undef_regs ... *) admit. Admitted. |