diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 45 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 10 | ||||
-rw-r--r-- | powerpc/Asmgenproof.v | 31 | ||||
-rw-r--r-- | powerpc/Asmgenproof1.v | 38 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 137 |
5 files changed, 200 insertions, 61 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index d698524d..fc29db04 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -130,7 +130,7 @@ Inductive instruction : Type := | Paddi: ireg -> ireg -> constant -> instruction (**r add immediate *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) | Paddze: ireg -> ireg -> instruction (**r add Carry bit *) - | Pallocframe: Z -> int -> instruction (**r allocate new stack frame *) + | Pallocframe: Z -> int -> instruction (**r allocate new stack frame *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) @@ -154,7 +154,7 @@ Inductive instruction : Type := | Peqv: ireg -> ireg -> ireg -> instruction (**r bitwise not-xor *) | Pextsb: ireg -> ireg -> instruction (**r 8-bit sign extension *) | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) - | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) + | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | Pfabs: freg -> freg -> instruction (**r float absolute value *) | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) @@ -215,7 +215,12 @@ 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 -> preg -> instruction. (**r built-in *) + | Pbuiltin: external_function -> list preg -> preg -> instruction (**r built-in function *) + | Pannot: external_function -> list annot_param -> instruction (**r annotation statement *) + +with annot_param : Type := + | APreg: preg -> annot_param + | APstack: memory_chunk -> Z -> annot_param. (** The pseudo-instructions are the following: @@ -740,6 +745,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr rs) m | Pbuiltin ef args res => Error (**r treated specially below *) + | Pannot ef args => + Error (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers @@ -803,20 +810,27 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := Mem.loadv Mfloat64 m (Val.add (rs (IR GPR1)) (Vint (Int.repr bofs))) = Some v -> extcall_arg rs m (S (Outgoing ofs Tfloat)) v. -Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop := - | extcall_args_nil: - extcall_args rs m nil nil - | extcall_args_cons: forall l1 ll v1 vl, - extcall_arg rs m l1 v1 -> extcall_args rs m ll vl -> - extcall_args rs m (l1 :: ll) (v1 :: vl). - Definition extcall_arguments (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - extcall_args rs m (loc_arguments sg) args. + list_forall2 (extcall_arg rs m) (loc_arguments sg) args. Definition loc_external_result (sg: signature) : preg := preg_of (loc_result sg). +(** Extract the values of the arguments of an annotation. *) + +Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop := + | annot_arg_reg: forall r, + annot_arg rs m (APreg r) (rs r) + | annot_arg_stack: forall chunk ofs stk base v, + rs (IR GPR1) = Vptr stk base -> + Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> + annot_arg rs m (APstack chunk ofs) v. + +Definition annot_arguments + (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop := + list_forall2 (annot_arg rs m) params args. + (** Execution of the instruction at [rs#PC]. *) Inductive state: Type := @@ -841,6 +855,15 @@ Inductive step: state -> trace -> state -> Prop := #FPR12 <- Vundef #FPR13 <- Vundef #FPR0 <- Vundef #CTR <- Vundef #res <- v)) m') + | exec_step_annot: + forall b ofs c ef args rs m vargs t v m', + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal c) -> + find_instr (Int.unsigned ofs) c = Some (Pannot ef args) -> + annot_arguments rs 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 -> diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 6b47d750..4370753b 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -399,6 +399,14 @@ Definition transl_load_store (* should not happen *) k end. +(** Translation of arguments to annotations *) + +Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param := + match p with + | Mach.APreg r => APreg (preg_of r) + | Mach.APstack chunk ofs => APstack chunk ofs + end. + (** Translation of a Mach instruction. *) Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := @@ -478,6 +486,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pbs symb :: k | Mbuiltin ef args res => Pbuiltin ef (map preg_of args) (preg_of res) :: k + | Mannot ef args => + Pannot ef (map transl_annot_param args) :: k | Mlabel lbl => Plabel lbl :: k | Mgoto lbl => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 3846a6cc..0efe646d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -447,6 +447,7 @@ Proof. destruct op; destruct args; try (destruct args); try (destruct args); try (destruct args); try reflexivity; autorewrite with labels; try reflexivity. case (mreg_type m); reflexivity. + case (symbol_is_small_data i i0); reflexivity. case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. Qed. @@ -1126,6 +1127,35 @@ Proof. intros. repeat rewrite Pregmap.gso; auto. Qed. +Lemma exec_Mannot_prop: + forall (s : list stackframe) (f : block) (sp : val) + (ms : Mach.regset) (m : mem) (ef : external_function) + (args : list Mach.annot_param) (b : list Mach.instruction) + (vargs: list val) (t : trace) (v : val) (m' : mem), + Machsem.annot_arguments ms m sp args vargs -> + external_call ef ge vargs m t v m' -> + exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t + (Machsem.State s f sp b ms m'). +Proof. + intros; red; intros; inv MS. + inv AT. simpl in H3. + generalize (functions_transl _ _ FIND); intro FN. + generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. + exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [A [B [C D]]]]]. + left. econstructor; split. apply plus_one. + eapply exec_step_annot. eauto. eauto. + eapply find_instr_tail; eauto. eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. + unfold nextinstr. rewrite Pregmap.gss. + rewrite <- H1; simpl. econstructor; auto. + eapply code_tail_next_int; eauto. + apply agree_nextinstr. auto. +Qed. + Lemma exec_Mgoto_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) @@ -1458,6 +1488,7 @@ Proof exec_Mcall_prop exec_Mtailcall_prop exec_Mbuiltin_prop + exec_Mannot_prop exec_Mgoto_prop exec_Mcond_true_prop exec_Mcond_false_prop diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 8f6f7255..ee3aa38a 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -503,13 +503,13 @@ Qed. Lemma extcall_args_match: forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> forall ll vl, - Machsem.extcall_args ms m sp ll vl -> - exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'. + list_forall2 (Machsem.extcall_arg ms m sp) ll vl -> + exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'. Proof. induction 3; intros. exists (@nil val); split. constructor. constructor. exploit extcall_arg_match; eauto. intros [v1' [A B]]. - exploit IHextcall_args; eauto. intros [vl' [C D]]. + destruct IHlist_forall2 as [vl' [C D]]. exists (v1' :: vl'); split; constructor; auto. Qed. @@ -523,6 +523,38 @@ Proof. eapply extcall_args_match; eauto. Qed. +(** Translation of arguments to annotations. *) + +Lemma annot_arg_match: + forall ms sp rs m m' p v, + agree ms sp rs -> + Mem.extends m m' -> + Machsem.annot_arg ms m sp p v -> + exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'. +Proof. + intros. inv H1; simpl. +(* reg *) + exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto. +(* stack *) + exploit Mem.load_extends; eauto. intros [v' [A B]]. + exists v'; split; auto. + inv H. econstructor; eauto. +Qed. + +Lemma annot_arguments_match: + forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> + forall pl vl, + Machsem.annot_arguments ms m sp pl vl -> + exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction 3; intros. + exists (@nil val); split. constructor. constructor. + exploit annot_arg_match; eauto. intros [v1' [A B]]. + destruct IHlist_forall2 as [vl' [C D]]. + exists (v1' :: vl'); split; constructor; auto. +Qed. + (** * Execution of straight-line code *) Section STRAIGHTLINE. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index ef53411b..0c199322 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -17,6 +17,7 @@ open Datatypes open Camlcoq open Sections open AST +open Memdata open Asm (* Recognition of target ABI and asm syntax *) @@ -264,7 +265,9 @@ let rec log2 n = assert (n > 0); if n = 1 then 0 else 1 + log2 (n lsr 1) -(* Built-ins. They come in two flavors: +(* Built-ins. They come in three flavors: + - annotation statements: take their arguments in registers or stack + locations; generate no code; - inlined by the compiler: take their arguments in arbitrary registers; preserve all registers except the temporaries (GPR0, GPR11, GPR12, FPR0, FPR12, FPR13); @@ -272,13 +275,11 @@ let rec log2 n = locations dictated by the calling conventions; preserve callee-save regs only. *) -(* Handling of __builtin_annotation *) - -let re_builtin_annotation = Str.regexp "__builtin_annotation_\"\\(.*\\)\"$" +(* Handling of annotations *) let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" -let print_annotation oc txt args res = +let print_annot_text print_arg oc txt args = fprintf oc "%s annotation: " comment; let print_fragment = function | Str.Text s -> @@ -288,23 +289,29 @@ let print_annotation oc txt args res = | Str.Delim s -> let n = int_of_string (String.sub s 1 (String.length s - 1)) in try - preg oc (List.nth args (n-1)) + print_arg oc (List.nth args (n-1)) with Failure _ -> fprintf oc "<bad parameter %s>" s in List.iter print_fragment (Str.full_split re_annot_param txt); - fprintf oc "\n"; + fprintf oc "\n" + +let print_annot_stmt oc txt args = + let print_annot_param oc = function + | APreg r -> preg oc r + | APstack(chunk, ofs) -> + fprintf oc "mem(R1 + %a, %a)" coqint ofs coqint (size_chunk chunk) in + print_annot_text print_annot_param oc txt args + +let print_annot_val oc txt args res = + print_annot_text preg oc txt args; match args, res with - | [], _ -> () | IR src :: _, IR dst -> if dst <> src then fprintf oc " mr %a, %a\n" ireg dst ireg src | FR src :: _, FR dst -> if dst <> src then fprintf oc " fmr %a, %a\n" freg dst freg src | _, _ -> assert false -(* Handling of __builtin_memcpy_alX_szY *) - -let re_builtin_memcpy = - Str.regexp "__builtin_memcpy\\(_al\\([248]\\)\\)?_sz\\([0-9]+\\)$" +(* Handling of memcpy *) (* On the PowerPC, unaligned accesses to 16- and 32-bit integers are fast, but unaligned accesses to 64-bit floats can be slow @@ -312,7 +319,9 @@ let re_builtin_memcpy = So, use 64-bit accesses only if alignment >= 8. Note that lfd and stfd cannot trap on ill-formed floats. *) -let print_builtin_memcpy oc sz al dst src = +let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in let rec copy ofs sz = if sz >= 8 && al >= 8 then begin fprintf oc " lfd %a, %d(%a)\n" freg FPR0 ofs ireg src; @@ -331,42 +340,61 @@ let print_builtin_memcpy oc sz al dst src = fprintf oc " stb %a, %d(%a)\n" ireg GPR0 ofs ireg dst; copy (ofs + 1) (sz - 1) end in - copy 0 sz + fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n" + comment sz al; + copy 0 sz; + fprintf oc "%s end builtin __builtin_memcpy\n" comment -(* Handling of compiler-inlined builtins *) +(* Handling of volatile reads and writes *) -let print_builtin_inlined oc name args res = - fprintf oc "%s begin builtin %s\n" comment name; - (* Can use as temporaries: GPR0, GPR11, GPR12, FPR0, FPR12, FPR13 *) - begin match name, args, res with - (* Volatile reads *) - | "__builtin_volatile_read_int8unsigned", [IR addr], IR res -> +let print_builtin_vload oc chunk args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + begin match chunk, args, res with + | Mint8unsigned, [IR addr], IR res -> fprintf oc " lbz %a, 0(%a)\n" ireg res ireg addr - | "__builtin_volatile_read_int8signed", [IR addr], IR res -> + | Mint8signed, [IR addr], IR res -> fprintf oc " lbz %a, 0(%a)\n" ireg res ireg addr; fprintf oc " extsb %a, %a\n" ireg res ireg res - | "__builtin_volatile_read_int16unsigned", [IR addr], IR res -> + | Mint16unsigned, [IR addr], IR res -> fprintf oc " lhz %a, 0(%a)\n" ireg res ireg addr - | "__builtin_volatile_read_int16signed", [IR addr], IR res -> + | Mint16signed, [IR addr], IR res -> fprintf oc " lha %a, 0(%a)\n" ireg res ireg addr - | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res -> + | Mint32, [IR addr], IR res -> fprintf oc " lwz %a, 0(%a)\n" ireg res ireg addr - | "__builtin_volatile_read_float32", [IR addr], FR res -> + | Mfloat32, [IR addr], FR res -> fprintf oc " lfs %a, 0(%a)\n" freg res ireg addr - | "__builtin_volatile_read_float64", [IR addr], FR res -> + | Mfloat64, [IR addr], FR res -> fprintf oc " lfd %a, 0(%a)\n" freg res ireg addr - (* Volatile writes *) - | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ -> + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + +let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + begin match chunk, args with + | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> fprintf oc " stb %a, 0(%a)\n" ireg src ireg addr - | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ -> + | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> fprintf oc " sth %a, 0(%a)\n" ireg src ireg addr - | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ -> + | Mint32, [IR addr; IR src] -> fprintf oc " stw %a, 0(%a)\n" ireg src ireg addr - | "__builtin_volatile_write_float32", [IR addr; FR src], _ -> + | Mfloat32, [IR addr; FR src] -> fprintf oc " frsp %a, %a\n" freg FPR13 freg src; fprintf oc " stfs %a, 0(%a)\n" freg FPR13 ireg addr - | "__builtin_volatile_write_float64", [IR addr; FR src], _ -> + | Mfloat64, [IR addr; FR src] -> fprintf oc " stfd %a, 0(%a)\n" freg src ireg addr + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + +(* Handling of compiler-inlined builtins *) + +let print_builtin_inline oc name args res = + fprintf oc "%s begin builtin %s\n" comment name; + (* Can use as temporaries: GPR0, GPR11, GPR12, FPR0, FPR12, FPR13 *) + begin match name, args, res with (* Integer arithmetic *) | "__builtin_mulhw", [IR a1; IR a2], IR res -> fprintf oc " mulhw %a, %a, %a\n" ireg res ireg a1 ireg a2 @@ -407,11 +435,6 @@ let print_builtin_inlined oc name args res = fprintf oc " isync\n" | "__builtin_trap", [], _ -> fprintf oc " trap\n" - (* Inlined memcpy *) - | name, [IR dst; IR src], _ when Str.string_match re_builtin_memcpy name 0 -> - let sz = int_of_string (Str.matched_group 3 name) in - let al = try int_of_string (Str.matched_group 2 name) with Not_found -> 1 in - print_builtin_memcpy oc sz al dst src (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -707,10 +730,28 @@ let print_instruction oc = function | Plabel lbl -> fprintf oc "%a:\n" label (transl_label lbl) | Pbuiltin(ef, args, res) -> - let name = extern_atom ef.ef_id in - if Str.string_match re_builtin_annotation name 0 - then print_annotation oc (Str.matched_group 1 name) args res - else print_builtin_inlined oc name args res + begin match ef with + | EF_builtin(name, sg) -> + print_builtin_inline oc (extern_atom name) args res + | EF_vload chunk -> + print_builtin_vload oc chunk args res + | EF_vstore chunk -> + print_builtin_vstore oc chunk args + | EF_memcpy(sz, al) -> + print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) + (Int32.to_int (camlint_of_coqint al)) args + | EF_annot_val(txt, targ) -> + print_annot_val oc (extern_atom txt) args res + | _ -> + assert false + end + | Pannot(ef, args) -> + begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) args + | _ -> + assert false + end let print_literal oc (lbl, n) = let nlo = Int64.to_int32 n @@ -740,11 +781,13 @@ let print_function oc name code = end; if !float_literals <> [] then begin section oc lit; + fprintf oc " .align 3\n"; List.iter (print_literal oc) !float_literals; float_literals := [] end; if !jumptables <> [] then begin section oc jmptbl; + fprintf oc " .align 2\n"; List.iter (print_jumptable oc) !jumptables; jumptables := [] end @@ -849,13 +892,13 @@ let non_variadic_stub oc name = fprintf oc " .indirect_symbol _%s\n" name; fprintf oc " .long 0\n" -let stub_function oc name ef = +let stub_function oc name sg = let name = extern_atom name in section oc Section_text; fprintf oc " .align 2\n"; fprintf oc "L%s$stub:\n" name; if Str.string_match re_variadic_stub name 0 - then variadic_stub oc name (Str.matched_group 1 name) (ef_sig ef).sig_args + then variadic_stub oc name (Str.matched_group 1 name) sg.sig_args else non_variadic_stub oc name let function_needs_stub name = true @@ -876,11 +919,11 @@ let variadic_stub oc stub_name fun_name args = else fprintf oc " crxor 6, 6, 6\n"; fprintf oc " b %s\n" fun_name -let stub_function oc name ef = +let stub_function oc name sg = let name = extern_atom name in (* Only variadic functions need a stub *) if Str.string_match re_variadic_stub name 0 - then variadic_stub oc name (Str.matched_group 1 name) (ef_sig ef).sig_args + then variadic_stub oc name (Str.matched_group 1 name) sg.sig_args let function_needs_stub name = Str.string_match re_variadic_stub (extern_atom name) 0 @@ -902,7 +945,7 @@ let print_fundef oc (Coq_pair(name, defn)) = | Internal code -> print_function oc name code | External ef -> - if not (is_builtin_function name) then stub_function oc name ef + if not (is_builtin_function name) then stub_function oc name (ef_sig ef) let record_extfun (Coq_pair(name, defn)) = match defn with |