From 4f187fdafdac0cf4a8b83964c89d79741dbd813e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 21 Aug 2015 17:53:44 +0200 Subject: Adapt the PowerPC port to the new builtin representation. __builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating. --- powerpc/Asm.v | 49 +++++++++++++++++++++++-------------------------- 1 file changed, 23 insertions(+), 26 deletions(-) (limited to 'powerpc/Asm.v') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index b7656dc4..a724f932 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -232,6 +232,8 @@ Inductive instruction : Type := | Pmr: ireg -> ireg -> instruction (**r integer move *) | Pmtctr: ireg -> instruction (**r move ireg to CTR *) | Pmtlr: ireg -> instruction (**r move ireg to LR *) + | Pmfspr: ireg -> int -> instruction (**r move from special register *) + | Pmtspr: int -> ireg -> instruction (**r move to special register *) | Pmulli: ireg -> ireg -> constant -> instruction (**r integer multiply immediate *) | Pmullw: ireg -> ireg -> ireg -> instruction (**r integer multiply *) | Pmulhw: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) @@ -279,8 +281,7 @@ Inductive instruction : Type := | Pxori: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate *) | Pxoris: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate high *) | Plabel: label -> instruction (**r define a code label *) - | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function (pseudo) *) - | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement (pseudo) *) + | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) | Pcfi_rel_offset: int -> instruction. (**r .cfi_rel_offset lr debug directive *) @@ -386,6 +387,15 @@ Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset := | _, _ => rs end. +(** Assigning the result of a builtin *) + +Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := + match res with + | BR r => rs#r <- v + | BR_none => rs + | BR_longofwords hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + end. + Section RELSEM. (** Looking up instructions in a code sequence by position. *) @@ -852,10 +862,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr rs) m | Pbuiltin ef args res => Stuck (**r treated specially below *) - | Pannot ef args => - Stuck (**r treated specially below *) - (** The following instructions and directives are not generated directly by Asmgen, - so we do not model them. *) + (** The following instructions and directives are not generated + directly by [Asmgen], so we do not model them. *) | Pbdnz _ | Pcntlzw _ _ | Pcreqv _ _ _ @@ -881,6 +889,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plhbrx _ _ _ | Plwzu _ _ _ | Pmfcr _ + | Pmfspr _ _ + | Pmtspr _ _ | Pstwbrx _ _ _ | Pstwcx_ _ _ _ | Pstfdu _ _ _ @@ -954,24 +964,16 @@ Inductive step: state -> trace -> state -> Prop := exec_instr f i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: - forall b ofs f ef args res rs m t vl rs' m', + forall b ofs f ef args res rs m vargs t vres rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> - external_call' ef ge (map rs args) m t vl m' -> + eval_builtin_args ge rs (rs GPR1) m args vargs -> + external_call ef ge vargs m t vres m' -> rs' = nextinstr - (set_regs res vl + (set_res res vres (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') - | exec_step_annot: - forall b ofs f ef args rs m vargs t v m', - rs PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) -> - eval_annot_args ge rs (rs GPR1) m args vargs -> - external_call ef ge vargs m t v m' -> - step (State rs m) t - (State (nextinstr rs) m') | exec_step_external: forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> @@ -1035,12 +1037,8 @@ Ltac Equalities := split. constructor. auto. discriminate. discriminate. - inv H11. - exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. - split. auto. intros. destruct B; auto. subst. auto. - inv H12. - assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. - exploit external_call_determ. eexact H5. eexact H13. intros [A B]. + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H11. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. @@ -1048,7 +1046,6 @@ Ltac Equalities := (* trace length *) red; intros. inv H; simpl. omega. - inv H3; eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. inv H2; eapply external_call_trace_length; eauto. (* initial states *) @@ -1068,4 +1065,4 @@ Definition data_preg (r: preg) : bool := | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false | CARRY => false | _ => true - end. \ No newline at end of file + end. -- cgit