diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-13 18:11:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-13 18:11:19 +0000 |
| commit | a5ffc59246b09a389e5f8cbc2f217e323e76990f (patch) | |
| tree | e1bc7cc54518aad7c20645f187cee8110de8cff9 | |
| parent | 4daccd62b92b23016d3f343d5691f9c164a8a951 (diff) | |
Revised handling of annotation statements, and more generally built-in functions, and more generally external functions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
45 files changed, 1140 insertions, 469 deletions
@@ -1,3 +1,15 @@ +- Revised handling of annotation statements. Now they come in two forms: + 1. __builtin_annot("format", x1, ..., xN) + (arbitrarily many arguments; no code generated, even if some + of the xi's were spilled; no return value) + 2. __builtin_annot_intval("format", x1) + (one integer argument, reloaded in a register if needed, + returned as result). + +- Related clean-ups in the handling of external functions and + compiler built-ins. + + Release 1.8.2, 2011-05-24 ========================= @@ -170,7 +170,12 @@ Inductive instruction : Type := | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) - | 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: @@ -531,6 +536,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | _ => Error end | 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 @@ -584,20 +590,27 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := Mem.loadv Mfloat64 m (Val.add (rs (IR IR13)) (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 IR13) = 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 := @@ -618,6 +631,14 @@ Inductive step: state -> trace -> state -> Prop := find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) -> external_call ef ge (map rs args) m t v m' -> step (State rs m) t (State (nextinstr(rs # 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/arm/Asmgen.v b/arm/Asmgen.v index a1f8d96..91a636b 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -436,6 +436,14 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := | Tfloat => storeind_float (freg_of src) base ofs 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) := @@ -494,6 +502,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb 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/arm/Asmgenproof.v b/arm/Asmgenproof.v index b7a7ff0..82e54c8 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -822,7 +822,8 @@ Proof. Qed. Lemma storev_8_signed_unsigned:
forall m a v,
Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
Proof.
intros. unfold Mem.storev. - destruct a; auto.
apply Mem.store_signed_unsigned_8.
Qed.
Lemma storev_16_signed_unsigned:
forall m a v,
Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
intros. unfold Mem.storev. destruct a; auto.
apply Mem.store_signed_unsigned_16.
Qed. + destruct a; auto.
apply Mem.store_signed_unsigned_8.
Qed. +
Lemma storev_16_signed_unsigned:
forall m a v,
Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
intros. unfold Mem.storev. destruct a; auto.
apply Mem.store_signed_unsigned_16.
Qed. Lemma exec_Mstore_prop: forall (s : list stackframe) (fb : block) (sp : val) @@ -1016,6 +1017,35 @@ Proof. intros. 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) @@ -1335,6 +1365,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/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 9312f30..d6ad203 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -337,14 +337,14 @@ 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. - exists (@nil val); split; constructor. + 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]]. - exists(v1' :: vl'); split. constructor; auto. constructor; auto. + destruct IHlist_forall2 as [vl' [C D]]. + exists (v1' :: vl'); split; constructor; auto. Qed. Lemma extcall_arguments_match: @@ -358,6 +358,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/arm/PrintAsm.ml b/arm/PrintAsm.ml index 4f5d1cd..cc42f3c 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -17,6 +17,7 @@ open Datatypes open Camlcoq open Sections open AST +open Memdata open Asm (* On-the-fly label renaming *) @@ -42,7 +43,9 @@ module IdentSet = Set.Make(struct type t = ident let compare = compare end) let extfuns = (ref IdentSet.empty) -let need_stub ef = List.mem Tfloat ef.ef_sig.sig_args +let need_stub = function + | EF_external(name, sg) -> List.mem Tfloat sg.sig_args + | _ -> false let record_extfun (Coq_pair(name, defn)) = match defn with @@ -216,20 +219,21 @@ let call_helper oc fn dst arg1 arg2 = (* ... for a total of at most 7 instructions *) 7 -(* 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 IR14 + registers; preserve all registers the temporaries + (IR10, IR12, IR14, FP2, FP4) - inlined while printing asm code; take their arguments in 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 -> @@ -239,28 +243,35 @@ 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"; - begin match args, res with - | [], _ -> 0 + 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 0 else (fprintf oc " mr %a, %a\n" ireg dst ireg src; 1) + if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1) | FR src :: _, FR dst -> - if dst = src then 0 else (fprintf oc " fmr %a, %a\n" freg dst freg src; 1) + if dst = src then 0 else (fprintf oc " mvfd %a, %a\n" freg dst freg src; 1) | _, _ -> assert false - end - -(* Handling of __builtin_memcpy_alX_szY *) -let re_builtin_memcpy = - Str.regexp "__builtin_memcpy\\(_al\\([248]\\)\\)?_sz\\([0-9]+\\)$" +(* Handling of memcpy *) (* The ARM has strict alignment constraints. *) -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 ninstr = if sz >= 4 && al >= 4 then begin fprintf oc " ldr %a, [%a, #%d]\n" ireg IR14 ireg src ofs; @@ -276,49 +287,63 @@ let print_builtin_memcpy oc sz al dst src = copy (ofs + 1) (sz - 1) (ninstr + 2) end else ninstr in - copy 0 sz 0 + fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n" + comment sz al; + let n = copy 0 sz 0 in + fprintf oc "%s end builtin __builtin_memcpy\n" comment; n + +let print_builtin_vload oc chunk args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + let n = + begin match chunk, args, res with + | Mint8unsigned, [IR addr], IR res -> + fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint8signed, [IR addr], IR res -> + fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint16unsigned, [IR addr], IR res -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint16signed, [IR addr], IR res -> + fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint32, [IR addr], IR res -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mfloat32, [IR addr], FR res -> + fprintf oc " ldfs %a, [%a, #0]\n" freg res ireg addr; + fprintf oc " mvfd %a, %a\n" freg res freg res; 2 + | Mfloat64, [IR addr], FR res -> + fprintf oc " ldfd %a, [%a, #0]\n" freg res ireg addr; 1 + | _ -> + assert false + end in + fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n + +let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + let n = + begin match chunk, args with + | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> + fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 + | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> + fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 + | Mint32, [IR addr; IR src] -> + fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 + | Mfloat32, [IR addr; FR src] -> + fprintf oc " mvfs %a, %a\n" freg FR2 freg src; + fprintf oc " stfs %a, [%a, #0]\n" freg FR2 ireg addr; 2 + | Mfloat64, [IR addr; FR src] -> + fprintf oc " stfd %a, [%a, #0]\n" freg src ireg addr; 1 + | _ -> + assert false + end in + fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n (* Handling of compiler-inlined builtins *) -let print_builtin_inlined oc name args res = +let print_builtin_inline oc name args res = fprintf oc "%s begin %s\n" comment name; let n = match name, args, res with - (* Volatile reads *) - | "__builtin_volatile_read_int8unsigned", [IR addr], IR res -> - fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 - | "__builtin_volatile_read_int8signed", [IR addr], IR res -> - fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 - | "__builtin_volatile_read_int16unsigned", [IR addr], IR res -> - fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 - | "__builtin_volatile_read_int16signed", [IR addr], IR res -> - fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 - | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res -> - fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 - | "__builtin_volatile_read_float32", [IR addr], FR res -> - fprintf oc " ldfs %a, [%a, #0]\n" freg res ireg addr; - fprintf oc " mvfd %a, %a\n" freg res freg res; 2 - | "__builtin_volatile_read_float64", [IR addr], FR res -> - fprintf oc " ldfd %a, [%a, #0]\n" freg res ireg addr; 1 - (* Volatile writes *) - | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ -> - fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 - | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ -> - fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 - | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ -> - fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 - | "__builtin_volatile_write_float32", [IR addr; FR src], _ -> - fprintf oc " mvfs %a, %a\n" freg FR2 freg src; - fprintf oc " stfs %a, [%a, #0]\n" freg FR2 ireg addr; 2 - | "__builtin_volatile_write_float64", [IR addr; FR src], _ -> - fprintf oc " stfd %a, [%a, #0]\n" freg src ireg addr; 1 (* Float arithmetic *) | "__builtin_fabs", [FR a1], FR res -> fprintf oc " absd %a, %a\n" freg res freg a1; 1 - (* 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) @@ -528,10 +553,28 @@ let print_instruction oc = function tbl; 2 + List.length tbl | 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; 0 + | _ -> + assert false + end let no_fallthrough = function | Pb _ -> true @@ -617,7 +660,7 @@ let print_fundef oc (Coq_pair(name, defn)) = print_function oc name code | External ef -> if need_stub ef && not(is_builtin_function name) - then print_external_function oc name ef.ef_sig + then print_external_function oc name (ef_sig ef) (* Data *) diff --git a/backend/Bounds.v b/backend/Bounds.v index 0415670..23fa3b5 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -75,6 +75,7 @@ Definition instr_within_bounds (i: instruction) := | Lload chunk addr args dst => mreg_within_bounds dst | Lcall sig ros => size_arguments sig <= bound_outgoing b | Lbuiltin ef args res => mreg_within_bounds res + | Lannot ef args => forall s, In (S s) args -> slot_within_bounds s | _ => True end. @@ -107,6 +108,7 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lcall sig ros => nil | Ltailcall sig ros => nil | Lbuiltin ef args res => res :: nil + | Lannot ef args => nil | Llabel lbl => nil | Lgoto lbl => nil | Lcond cond args lbl => nil @@ -114,10 +116,18 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lreturn => nil end. +Fixpoint slots_of_locs (l: list loc) : list slot := + match l with + | nil => nil + | S s :: l' => s :: slots_of_locs l' + | R r :: l' => slots_of_locs l' + end. + Definition slots_of_instr (i: instruction) : list slot := match i with | Lgetstack s r => s :: nil | Lsetstack r s => s :: nil + | Lannot ef args => slots_of_locs args | _ => nil end. @@ -343,6 +353,14 @@ Proof. split. simpl in H1. exact H1. eapply outgoing_slot_bound; eauto. Qed. +Lemma slots_of_locs_charact: + forall s l, In s (slots_of_locs l) <-> In (S s) l. +Proof. + induction l; simpl; intros. + tauto. + destruct a; simpl; intuition congruence. +Qed. + (** It follows that every instruction in the function is within bounds, in the sense of the [instr_within_bounds] predicate. *) @@ -356,9 +374,16 @@ Proof. destruct i; generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H); simpl; intros; auto. +(* getstack *) inv H0. split; auto. +(* setstack *) inv H0; auto. +(* call *) eapply size_arguments_bound; eauto. +(* annot *) + inv H0. apply H1. rewrite slots_of_locs_charact; auto. + generalize (H8 _ H3). unfold loc_acceptable, slot_valid. + destruct s; (contradiction || omega). Qed. Lemma function_is_within_bounds: diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 1cd245e..0b48c0f 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -352,7 +352,7 @@ proc: fn_stackspace = $8; fn_body = $10 }) } | EXTERN STRINGLIT COLON signature - { Coq_pair($2, External({ef_id = $2; ef_sig = $4; ef_inline = false})) } + { Coq_pair($2, External(EF_external($2, $4))) } ; signature: diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index c928f3f..1a20f73 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -73,7 +73,7 @@ Inductive wt_instr : instruction -> Prop := forall ef args res, List.map Loc.type args = (ef_sig ef).(sig_args) -> Loc.type res = proj_sig_res (ef_sig ef) -> - arity_ok (ef_sig ef).(sig_args) = true -> + arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false -> locs_acceptable args -> loc_acceptable res -> wt_instr (Lbuiltin ef args res) | wt_Llabel: forall lbl, diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 791c755..40a584f 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -94,7 +94,7 @@ Inductive wt_instr : instruction -> Prop := forall ef args res s, List.map Loc.type args = (ef_sig ef).(sig_args) -> Loc.type res = proj_sig_res (ef_sig ef) -> - arity_ok (ef_sig ef).(sig_args) = true -> + arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false -> locs_acceptable args -> loc_acceptable res -> valid_successor s -> wt_instr (Lbuiltin ef args res s) diff --git a/backend/Linear.v b/backend/Linear.v index 31c3fed..23f0324 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -44,6 +44,7 @@ Inductive instruction: Type := | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction | Lbuiltin: external_function -> list mreg -> mreg -> instruction + | Lannot: external_function -> list loc -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -296,6 +297,11 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge (reglist rs args) m t v m' -> step (State s f sp (Lbuiltin ef args res :: b) rs m) t (State s f sp b (Locmap.set (R res) v (undef_temps rs)) m') + | exec_Lannot: + forall s f sp rs m ef args b t v m', + external_call ef ge (map rs args) m t v m' -> + step (State s f sp (Lannot ef args :: b) rs m) + t (State s f sp b rs m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index ef6194c..390b630 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -93,6 +93,12 @@ Inductive wt_instr : instruction -> Prop := mreg_type res = proj_sig_res (ef_sig ef) -> arity_ok (ef_sig ef).(sig_args) = true -> wt_instr (Lbuiltin ef args res) + | wt_Lannot: + forall ef args, + List.map Loc.type args = (ef_sig ef).(sig_args) -> + ef_reloads ef = false -> + locs_acceptable args -> + wt_instr (Lannot ef args) | wt_Llabel: forall lbl, wt_instr (Llabel lbl) diff --git a/backend/Mach.v b/backend/Mach.v index 223d5ab..3210a9e 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -60,11 +60,16 @@ Inductive instruction: Type := | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction | Mbuiltin: external_function -> list mreg -> mreg -> instruction + | Mannot: external_function -> list annot_param -> instruction | Mlabel: label -> instruction | Mgoto: label -> instruction | Mcond: condition -> list mreg -> label -> instruction | Mjumptable: mreg -> list label -> instruction - | Mreturn: instruction. + | Mreturn: instruction + +with annot_param: Type := + | APreg: mreg -> annot_param + | APstack: memory_chunk -> Z -> annot_param. Definition code := list instruction. @@ -87,7 +92,12 @@ Definition funsig (fd: fundef) := Definition genv := Genv.t fundef unit. -(** * Dynamic semantics *) +(** * Elements of dynamic semantics *) + +(** The operational semantics is in module [Machsem]. *) + +Definition chunk_of_type (ty: typ) := + match ty with Tint => Mint32 | Tfloat => Mfloat64 end. Module RegEq. Definition t := mreg. diff --git a/backend/Machsem.v b/backend/Machsem.v index 1a167a9..fe0ec37 100644 --- a/backend/Machsem.v +++ b/backend/Machsem.v @@ -56,16 +56,13 @@ function. The [return_address_offset] predicate from module the Asm code generated later will store in the reserved location. *) -Definition chunk_of_type (ty: typ) := - match ty with Tint => Mint32 | Tfloat => Mfloat64 end. - Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) := Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)). Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) := Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v. -(** Extract the values of the arguments of an external call. *) +(** Extract the values of the arguments to an external call. *) Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := | extcall_arg_reg: forall rs m sp r, @@ -74,16 +71,22 @@ Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v -> extcall_arg rs m sp (S (Outgoing ofs ty)) v. -Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := - | extcall_args_nil: forall rs m sp, - extcall_args rs m sp nil nil - | extcall_args_cons: forall rs m sp l1 ll v1 vl, - extcall_arg rs m sp l1 v1 -> extcall_args rs m sp ll vl -> - extcall_args rs m sp (l1 :: ll) (v1 :: vl). - Definition extcall_arguments - (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := - extcall_args rs m sp (loc_arguments sg) args. + (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := + list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args. + +(** Extract the values of the arguments to an annotation. *) + +Inductive annot_arg: regset -> mem -> val -> annot_param -> val -> Prop := + | annot_arg_reg: forall rs m sp r, + annot_arg rs m sp (APreg r) (rs r) + | annot_arg_stack: forall rs m stk base chunk ofs v, + Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> + annot_arg rs m (Vptr stk base) (APstack chunk ofs) v. + +Definition annot_arguments + (rs: regset) (m: mem) (sp: val) (params: list annot_param) (args: list val) : Prop := + list_forall2 (annot_arg rs m sp) params args. (** Mach execution states. *) @@ -193,6 +196,12 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge rs##args m t v m' -> step (State s f sp (Mbuiltin ef args res :: b) rs m) t (State s f sp b ((undef_temps rs)#res <- v) m') + | exec_Mannot: + forall s f sp rs m ef args b vargs t v m', + annot_arguments rs m sp args vargs -> + external_call ef ge vargs m t v m' -> + step (State s f sp (Mannot ef args :: b) rs m) + t (State s f sp b rs m') | exec_Mgoto: forall s fb f sp lbl c rs m c', Genv.find_funct_ptr ge fb = Some (Internal f) -> diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 95ceafe..2d8c83d 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -77,6 +77,10 @@ Inductive wt_instr : instruction -> Prop := List.map mreg_type args = (ef_sig ef).(sig_args) -> mreg_type res = proj_sig_res (ef_sig ef) -> wt_instr (Mbuiltin ef args res) + | wt_Mannot: + forall ef args, + ef_reloads ef = false -> + wt_instr (Mannot ef args) | wt_Mgoto: forall lbl, wt_instr (Mgoto lbl) diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index cce00f6..3bfd803 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -20,11 +20,10 @@ open AST open Integers open Locations open LTL +open PrintAST open PrintOp open PrintRTL -let name_of_typ = function Tint -> "int" | Tfloat -> "float" - let loc pp l = match l with | R r -> @@ -78,6 +77,10 @@ let print_instruction pp (pc, i) = | Ltailcall(sg, fn, args) -> fprintf pp "tailcall %a(%a)@ " ros fn locs args + | Lbuiltin(ef, args, res, s) -> + fprintf pp "%a = builtin %s(%a)@ " + loc res (name_of_external ef) locs args; + print_succ pp s (Int32.pred pc) | Lcond(cond, args, s1, s2) -> fprintf pp "if (%a) goto %ld else goto %ld@ " (print_condition loc) (cond, args) diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml index e0a3204..adff483 100644 --- a/backend/PrintLTLin.ml +++ b/backend/PrintLTLin.ml @@ -21,21 +21,9 @@ open Integers open Locations open Machregsaux open LTLin +open PrintAST open PrintOp -let name_of_chunk = function - | Mint8signed -> "int8signed" - | Mint8unsigned -> "int8unsigned" - | Mint16signed -> "int16signed" - | Mint16unsigned -> "int16unsigned" - | Mint32 -> "int32" - | Mfloat32 -> "float32" - | Mfloat64 -> "float64" - -let name_of_type = function - | Tint -> "int" - | Tfloat -> "float" - let reg pp loc = match loc with | R r -> @@ -80,8 +68,8 @@ let print_instruction pp i = fprintf pp "tailcall %a(%a)@ " ros fn regs args | Lbuiltin(ef, args, res) -> - fprintf pp "%a = builtin \"%s\"(%a)@ " - reg res (extern_atom ef.ef_id) regs args + fprintf pp "%a = builtin %s(%a)@ " + reg res (name_of_external ef) regs args | Llabel lbl -> fprintf pp "%ld:@ " (camlint_of_positive lbl) | Lgoto lbl -> diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index 5b4887e..a6a1cc5 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -21,21 +21,9 @@ open Integers open Locations open Machregsaux open Mach +open PrintAST open PrintOp -let name_of_chunk = function - | Mint8signed -> "int8signed" - | Mint8unsigned -> "int8unsigned" - | Mint16signed -> "int16signed" - | Mint16unsigned -> "int16unsigned" - | Mint32 -> "int32" - | Mfloat32 -> "float32" - | Mfloat64 -> "float64" - -let name_of_type = function - | Tint -> "int" - | Tfloat -> "float" - let reg pp r = match name_of_register r with | Some s -> fprintf pp "%s" s @@ -46,6 +34,15 @@ let rec regs pp = function | [r] -> reg pp r | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl +let annot_param pp = function + | APreg r -> reg pp r + | APstack(chunk, ofs) -> fprintf pp "stack(%s,%ld)" (name_of_chunk chunk) (camlint_of_coqint ofs) + +let rec annot_params pp = function + | [] -> () + | [r] -> annot_param pp r + | r1::rl -> fprintf pp "%a, %a" annot_param r1 annot_params rl + let ros pp = function | Coq_inl r -> reg pp r | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) @@ -78,8 +75,10 @@ let print_instruction pp i = | Mtailcall(sg, fn) -> fprintf pp "tailcall %a@ " ros fn | Mbuiltin(ef, args, res) -> - fprintf pp "%a = builtin \"%s\"(%a)@ " - reg res (extern_atom ef.ef_id) regs args + fprintf pp "%a = builtin %s(%a)@ " + reg res (name_of_external ef) regs args + | Mannot(ef, args) -> + fprintf pp "%s(%a)@ " (name_of_external ef) annot_params args | Mlabel lbl -> fprintf pp "%ld:@ " (camlint_of_positive lbl) | Mgoto lbl -> diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 62ee2c9..620a949 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -19,19 +19,11 @@ open Maps open AST open Integers open RTL +open PrintAST open PrintOp (* Printing of RTL code *) -let name_of_chunk = function - | Mint8signed -> "int8signed" - | Mint8unsigned -> "int8unsigned" - | Mint16signed -> "int16signed" - | Mint16unsigned -> "int16unsigned" - | Mint32 -> "int32" - | Mfloat32 -> "float32" - | Mfloat64 -> "float64" - let reg pp r = fprintf pp "x%ld" (camlint_of_positive r) @@ -79,8 +71,8 @@ let print_instruction pp (pc, i) = fprintf pp "tailcall %a(%a)@ " ros fn regs args | Ibuiltin(ef, args, res, s) -> - fprintf pp "%a = builtin \"%s\"(%a)@ " - reg res (extern_atom ef.ef_id) regs args; + fprintf pp "%a = builtin %s(%a)@ " + reg res (name_of_external ef) regs args; print_succ pp s (Int32.pred pc) | Icond(cond, args, s1, s2) -> fprintf pp "if (%a) goto %ld else goto %ld@ " diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 49f339d..02359b9 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -110,7 +110,7 @@ Inductive wt_instr : instruction -> Prop := forall ef args res s, List.map env args = (ef_sig ef).(sig_args) -> env res = proj_sig_res (ef_sig ef) -> - arity_ok (ef_sig ef).(sig_args) = true -> + arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false -> valid_successor s -> wt_instr (Ibuiltin ef args res s) | wt_Icond: @@ -236,7 +236,7 @@ Definition check_instr (i: instruction) : bool := | Ibuiltin ef args res s => check_regs args (ef_sig ef).(sig_args) && check_reg res (proj_sig_res (ef_sig ef)) - && arity_ok (ef_sig ef).(sig_args) + && (if ef_reloads ef then arity_ok (ef_sig ef).(sig_args) else true) && check_successor s | Icond cond args s1 s2 => check_regs args (type_of_condition cond) @@ -349,6 +349,7 @@ Proof. apply check_regs_correct; auto. apply check_reg_correct; auto. auto. + destruct (ef_reloads e); auto. apply check_successor_correct; auto. (* cond *) constructor. apply check_regs_correct; auto. diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index 7549ff4..17acbc6 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -20,6 +20,7 @@ open Memdata open Op open Registers open RTL +open PrintAST exception Type_error of string @@ -93,11 +94,11 @@ let type_instr retty (Coq_pair(pc, i)) = let sg = ef_sig ef in set_types args sg.sig_args; set_type res (match sg.sig_res with None -> Tint | Some ty -> ty); - if not (Conventions.arity_ok sg.sig_args) then + if ef_reloads ef && not (Conventions.arity_ok sg.sig_args) then raise(Type_error "wrong arity") with Type_error msg -> raise(Type_error (Printf.sprintf "type mismatch in Ibuiltin(%s): %s" - (extern_atom ef.ef_id) msg)) + (name_of_external ef) msg)) end | Icond(cond, args, _, _) -> set_types args (type_of_condition cond) diff --git a/backend/Reload.v b/backend/Reload.v index 81b6199..0ad53e6 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -236,10 +236,13 @@ Definition transf_instr (Ltailcall sig (inr _ id) :: k) end | LTLin.Lbuiltin ef args dst => - let rargs := regs_for args in - let rdst := reg_for dst in - add_reloads args rargs - (Lbuiltin ef rargs rdst :: add_spill rdst dst k) + if ef_reloads ef then + (let rargs := regs_for args in + let rdst := reg_for dst in + add_reloads args rargs + (Lbuiltin ef rargs rdst :: add_spill rdst dst k)) + else + Lannot ef args :: k | LTLin.Llabel lbl => Llabel lbl :: k | LTLin.Lgoto lbl => diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 09a9101..49640a3 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -799,7 +799,7 @@ Proof. FL. FL. destruct s0; FL; FL; FL. destruct s0; FL; FL; FL. - FL. + destruct (ef_reloads e). FL. FL. FL. destruct o; FL. Qed. @@ -1254,8 +1254,9 @@ Proof. (* Lbuiltin *) ExploitWT; inv WTI. + case_eq (ef_reloads ef); intro RELOADS. exploit add_reloads_correct. - instantiate (1 := args). apply arity_ok_enough. rewrite H3. auto. auto. + instantiate (1 := args). apply arity_ok_enough. rewrite H3. destruct H5. auto. congruence. auto. intros [ls2 [A [B C]]]. exploit external_call_mem_extends; eauto. apply agree_locs; eauto. @@ -1273,6 +1274,19 @@ Proof. rewrite E. rewrite Locmap.gss. auto. intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_temps_others; auto. apply reg_for_diff; auto. + (* no reload *) + exploit external_call_mem_extends; eauto. + apply agree_locs; eauto. + intros [v' [tm' [P [Q [R S]]]]]. + assert (EQ: v = Vundef). + destruct ef; simpl in RELOADS; try congruence. simpl in H; inv H. auto. + subst v. + left; econstructor; split. + apply plus_one. eapply exec_Lannot. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. + apply agree_set with ls; auto. (* Llabel *) left; econstructor; split. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 60be59b..eba5ad6 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -33,9 +33,7 @@ Require Import Reloadproof. generate well-typed instruction sequences, given sufficient typing and well-formedness hypotheses over the locations involved. *) -Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove - wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lbuiltin - wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty. +Hint Constructors wt_instr: reloadty. Remark wt_code_cons: forall f i c, wt_instr f i -> wt_code f c -> wt_code f (i :: c). @@ -292,9 +290,12 @@ Proof. destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. auto 10 with reloadty. + destruct (ef_reloads ef) as [] _eqn. + assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence. assert (map mreg_type (regs_for args) = map Loc.type args). apply wt_regs_for. apply arity_ok_enough. congruence. assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty. + auto 10 with reloadty. auto with reloadty. diff --git a/backend/Selection.v b/backend/Selection.v index 9e11bc3..9c037b8 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -184,7 +184,7 @@ Definition expr_is_addrof_builtin (ge: Cminor.genv) (e: Cminor.expr) : option ex | None => None | Some b => match Genv.find_funct_ptr ge b with - | Some(External ef) => if ef.(ef_inline) then Some ef else None + | Some(External ef) => if ef_inline ef then Some ef else None | _ => None end end diff --git a/backend/Stacking.v b/backend/Stacking.v index 09d98d6..23a112c 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -130,6 +130,16 @@ Definition transl_op (fe: frame_env) (op: operation) := Definition transl_addr (fe: frame_env) (addr: addressing) := shift_stack_addressing (Int.repr fe.(fe_stack_data)) addr. +(** Translation of an annotation argument. *) + +Definition transl_annot_param (fe: frame_env) (l: loc) : annot_param := + match l with + | R r => APreg r + | S (Local ofs ty) => APstack (chunk_of_type ty) (offset_of_index fe (FI_local ofs ty)) + | S _ => APstack Mint32 (-1) (**r never happens *) + end. + + (** Translation of a Linear instruction. Prepends the corresponding Mach instructions to the given list of instructions. [Lgetstack] and [Lsetstack] moves between registers and stack slots @@ -173,6 +183,8 @@ Definition transl_instr (Mtailcall sig ros :: k) | Lbuiltin ef args dst => Mbuiltin ef args dst :: k + | Lannot ef args => + Mannot ef (map (transl_annot_param fe) args) :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d651220..fbe8882 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -2172,7 +2172,7 @@ Lemma transl_external_arguments_rec: forall locs, incl locs (loc_arguments sg) -> exists vl, - extcall_args rs m' (parent_sp cs') locs vl /\ val_list_inject j ls##locs vl. + list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ val_list_inject j ls##locs vl. Proof. induction locs; simpl; intros. exists (@nil val); split. constructor. constructor. @@ -2193,6 +2193,61 @@ Qed. End EXTERNAL_ARGUMENTS. +(** Preservation of the arguments to an annotation. *) + +Section ANNOT_ARGUMENTS. + +Variable f: Linear.function. +Let b := function_bounds f. +Let fe := make_env b. +Variable j: meminj. +Variables m m': mem. +Variables ls ls0: locset. +Variable rs: regset. +Variables sp sp': block. +Variables parent retaddr: val. +Hypothesis AGR: agree_regs j ls rs. +Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent retaddr. + +Lemma transl_annot_param_correct: + forall l, + loc_acceptable l -> + match l with S s => slot_within_bounds f b s | _ => True end -> + exists v, annot_arg rs m' (Vptr sp' Int.zero) (transl_annot_param fe l) v + /\ val_inject j (ls l) v. +Proof. + intros. destruct l; red in H. +(* reg *) + exists (rs m0); split. constructor. auto. +(* stack *) + destruct s; try contradiction. + exploit agree_locals; eauto. intros [v [A B]]. inv A. + exists v; split. constructor. rewrite Zplus_0_l. auto. auto. +Qed. + +Lemma transl_annot_params_correct: + forall ll, + locs_acceptable ll -> + (forall s, In (S s) ll -> slot_within_bounds f b s) -> + exists vl, + annot_arguments rs m' (Vptr sp' Int.zero) (map (transl_annot_param fe) ll) vl + /\ val_list_inject j (map ls ll) vl. +Proof. + induction ll; intros. + exists (@nil val); split; constructor. + exploit (transl_annot_param_correct a). + apply H; auto with coqlib. + destruct a; auto with coqlib. + intros [v1 [A B]]. + exploit IHll. + red; intros; apply H; auto with coqlib. + intros; apply H0; auto with coqlib. + intros [vl [C D]]. + exists (v1 :: vl); split; constructor; auto. +Qed. + +End ANNOT_ARGUMENTS. + (** The proof of semantic preservation relies on simulation diagrams of the following form: << @@ -2466,6 +2521,29 @@ Proof. eapply agree_valid_mach; eauto. inv WTI. simpl; rewrite H4. eapply external_call_well_typed; eauto. + (* Lannot *) + inv WTI. + exploit transl_annot_params_correct; eauto. + intros [vargs' [P Q]]. + exploit external_call_mem_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]]. + econstructor; split. + apply plus_one. econstructor; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. + eapply match_stack_change_extcall; eauto. + apply Zlt_le_weak. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. + apply Zlt_le_weak. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto. + eapply agree_regs_inject_incr; eauto. + eapply agree_frame_inject_incr; eauto. + apply agree_frame_extcall_invariant with m m'0; auto. + eapply external_call_valid_block; eauto. + eapply external_call_bounds; eauto. eapply agree_valid_linear; eauto. + eapply external_call_valid_block; eauto. + eapply agree_valid_mach; eauto. + (* Llabel *) econstructor; split. apply plus_one; apply exec_Mlabel. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index d00d1b2..27de557 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -179,6 +179,9 @@ Proof. (* builtin *) apply wt_instrs_cons; auto. constructor; auto. + (* annot *) + apply wt_instrs_cons; auto. + constructor; auto. (* label *) apply wt_instrs_cons; auto. constructor. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 98384fa..225905a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -71,39 +71,6 @@ let builtins_generic = { (* Floating-point absolute value *) "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); - (* The volatile read/volatile write functions *) - "__builtin_volatile_read_int8unsigned", - (TInt(IUChar, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int8signed", - (TInt(ISChar, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int16unsigned", - (TInt(IUShort, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int16signed", - (TInt(IShort, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int32", - (TInt(IInt, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_float32", - (TFloat(FFloat, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_float64", - (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_pointer", - (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_write_int8unsigned", - (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false); - "__builtin_volatile_write_int8signed", - (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false); - "__builtin_volatile_write_int16unsigned", - (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false); - "__builtin_volatile_write_int16signed", - (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false); - "__builtin_volatile_write_int32", - (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false); - "__builtin_volatile_write_float32", - (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false); - "__builtin_volatile_write_float64", - (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false); - "__builtin_volatile_write_pointer", - (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false); (* Block copy *) "__builtin_memcpy", (TVoid [], @@ -130,9 +97,13 @@ let builtins_generic = { TInt(Cutil.size_t_ikind, [])], false); (* Annotations *) - "__builtin_annotation", - (TVoid [], (* overriden during elaboration *) + "__builtin_annot", + (TVoid [], [TPtr(TInt(IChar, [AConst]), [])], + true); + "__builtin_annot_intval", + (TInt(IInt, []), + [TPtr(TInt(IChar, [AConst]), []); TInt(IInt, [])], false) ] } @@ -188,19 +159,14 @@ let globals_for_strings globs = let special_externals_table : (string, fundef) Hashtbl.t = Hashtbl.create 47 -let register_special_external c_name int_name targs tres inline = - if not (Hashtbl.mem special_externals_table c_name) then begin - Hashtbl.add special_externals_table c_name - (External({ef_id = intern_string int_name; - ef_sig = signature_of_type targs tres; - ef_inline = inline}, - targs, tres)) - end +let register_special_external name ef targs tres = + if not (Hashtbl.mem special_externals_table name) then + Hashtbl.add special_externals_table name (External(ef, targs, tres)) let declare_special_externals k = Hashtbl.fold - (fun c_name fd k -> - Datatypes.Coq_pair(intern_string c_name, fd) :: k) + (fun name fd k -> + Datatypes.Coq_pair(intern_string name, fd) :: k) special_externals_table k (** ** Handling of stubs for variadic functions *) @@ -217,35 +183,51 @@ let register_stub_function name tres targs = let stub_name = name ^ "$" ^ String.concat "" (letters_of_type targs) in let targs = types_of_types targs in - register_special_external stub_name stub_name targs tres false; + let ef = EF_external(intern_string stub_name, signature_of_type targs tres) in + register_special_external stub_name ef targs tres; (stub_name, Tfunction (targs, tres)) (** ** Handling of annotations *) let annot_function_next = ref 0 -let register_annotation_function txt targs tres = +let register_annotation_stmt txt targs = + let tres = Tvoid in incr annot_function_next; let fun_name = - Printf.sprintf "__builtin_annotation_%d" !annot_function_next - and int_name = - Printf.sprintf "__builtin_annotation_\"%s\"" txt in - register_special_external fun_name int_name targs tres true; + Printf.sprintf "__builtin_annot_%d" !annot_function_next + and ef = + EF_annot (intern_string txt, typlist_of_typelist targs) in + register_special_external fun_name ef targs tres; Evalof(Evar(intern_string fun_name, Tfunction(targs, tres)), Tfunction(targs, tres)) -(** ** Handling of inlined memcpy functions *) +let register_annotation_val txt targ = + let targs = Tcons(targ, Tnil) + and tres = targ in + incr annot_function_next; + let fun_name = + Printf.sprintf "__builtin_annot_val_%d" !annot_function_next + and ef = + EF_annot_val (intern_string txt, typ_of_type targ) in + register_special_external fun_name ef targs tres; + Evalof(Evar(intern_string fun_name, Tfunction(targs, tres)), + Tfunction(targs, tres)) -let alignof_pointed ty = - match ty with - | Tpointer ty' -> camlint_of_z (alignof ty') - | _ -> 1l (* safe default *) +(** ** Handling of inlined memcpy functions *) let register_inlined_memcpy basename sz = + let al = + match basename with + | "__builtin_memcpy_al2" -> 2l + | "__builtin_memcpy_al4" -> 4l + | "__builtin_memcpy_al8" -> 8l + | _ -> 1l in let name = Printf.sprintf "%s_sz%ld" basename sz in - let targs = Tcons(Tpointer Tvoid, Tcons(Tpointer Tvoid, Tnil)) in - let tres = Tvoid in - register_special_external name name targs tres true; + let targs = Tcons(Tpointer Tvoid, Tcons(Tpointer Tvoid, Tnil)) + and tres = Tvoid + and ef = EF_memcpy(coqint_of_camlint sz, coqint_of_camlint al) in + register_special_external name ef targs tres; Evalof(Evar(intern_string name, Tfunction(targs, tres)), Tfunction(targs, tres)) @@ -407,29 +389,33 @@ let is_volatile_access env e = List.mem C.AVolatile (Cutil.attributes_of_type env e.etyp) && Cutil.is_lvalue env e -let volatile_fun_suffix_type ty = +let volatile_kind ty = match ty with - | Tint(I8, Unsigned) -> ("int8unsigned", ty) - | Tint(I8, Signed) -> ("int8signed", ty) - | Tint(I16, Unsigned) -> ("int16unsigned", ty) - | Tint(I16, Signed) -> ("int16signed", ty) - | Tint(I32, _) -> ("int32", Tint(I32, Signed)) - | Tfloat F32 -> ("float32", ty) - | Tfloat F64 -> ("float64", ty) + | Tint(I8, Unsigned) -> ("int8unsigned", ty, Mint8unsigned) + | Tint(I8, Signed) -> ("int8signed", ty, Mint8signed) + | Tint(I16, Unsigned) -> ("int16unsigned", ty, Mint16unsigned) + | Tint(I16, Signed) -> ("int16signed", ty, Mint16signed) + | Tint(I32, _) -> ("int32", Tint(I32, Signed), Mint32) + | Tfloat F32 -> ("float32", ty, Mfloat32) + | Tfloat F64 -> ("float64", ty, Mfloat64) | Tpointer _ | Tarray _ | Tfunction _ | Tcomp_ptr _ -> - ("pointer", Tpointer Tvoid) + ("pointer", Tpointer Tvoid, Mint32) | _ -> - unsupported "operation on volatile struct or union"; ("", Tvoid) + unsupported "operation on volatile struct or union"; ("", Tvoid, Mint32) let volatile_read_fun ty = - let (suffix, ty') = volatile_fun_suffix_type ty in - let funty = Tfunction(Tcons(Tpointer Tvoid, Tnil), ty') in - Evalof(Evar(intern_string ("__builtin_volatile_read_" ^ suffix), funty), funty) + let (suffix, ty', chunk) = volatile_kind ty in + let targs = Tcons(Tpointer Tvoid, Tnil) in + let name = "__builtin_volatile_read_" ^ suffix in + register_special_external name (EF_vload chunk) targs ty'; + Evalof(Evar(intern_string name, Tfunction(targs, ty')), Tfunction(targs, ty')) let volatile_write_fun ty = - let (suffix, ty') = volatile_fun_suffix_type ty in - let funty = Tfunction(Tcons(Tpointer Tvoid, Tcons(ty', Tnil)), Tvoid) in - Evalof(Evar(intern_string ("__builtin_volatile_write_" ^ suffix), funty), funty) + let (suffix, ty', chunk) = volatile_kind ty in + let targs = Tcons(Tpointer Tvoid, Tcons(ty', Tnil)) in + let name = "__builtin_volatile_write_" ^ suffix in + register_special_external name (EF_vstore chunk) targs Tvoid; + Evalof(Evar(intern_string name, Tfunction(targs, Tvoid)), Tfunction(targs, Tvoid)) (** Expressions *) @@ -562,20 +548,29 @@ let rec convertExpr env e = | C.ECast(ty1, e1) -> Ecast(convertExpr env e1, convertTyp env ty1) - | C.ECall({edesc = C.EVar {name = "__builtin_annotation"}}, args) -> + | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> - if List.length args1 > 2 then - error "too many arguments to __builtin_annotation"; let targs1 = convertTypList env (List.map (fun e -> e.etyp) args1) in - let fn' = register_annotation_function txt targs1 ty in + let fn' = register_annotation_stmt txt targs1 in Ecall(fn', convertExprList env args1, ty) | _ -> - error "ill-formed __builtin_annotation (first argument must be string literal)"; + error "ill-formed __builtin_annot (first argument must be string literal)"; + ezero + end + + | C.ECall({edesc = C.EVar {name = "__builtin_annot_intval"}}, args) -> + begin match args with + | [ {edesc = C.EConst(CStr txt)}; arg ] -> + let targ = convertTyp env arg.etyp in + let fn' = register_annotation_val txt targ in + Ecall(fn', convertExprList env [arg], ty) + | _ -> + error "ill-formed __builtin_annot_intval (first argument must be string literal)"; ezero end - | C.ECall({edesc = C.EVar {name = ("__builtin_memcpy" + | C.ECall({edesc = C.EVar {name = ("__builtin_memcpy" |"__builtin_memcpy_al2" |"__builtin_memcpy_al4" |"__builtin_memcpy_al8" as name)}} as fn, @@ -780,11 +775,12 @@ let convertFundecl env (sto, id, ty, optinit) = | Tfunction(args, res) -> (args, res) | _ -> assert false in let id' = intern_string id.name in + let sg = signature_of_type args res in let ef = - { ef_id = id'; - ef_sig = signature_of_type args res; - ef_inline = List.mem_assoc id.name builtins.functions - && not (List.mem id.name noninlined_builtin_functions) } in + if List.mem_assoc id.name builtins.functions + && not (List.mem id.name noninlined_builtin_functions) + then EF_builtin(id', sg) + else EF_external(id', sg) in Datatypes.Coq_pair(id', External(ef, args, res)) (** Initializers *) diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index f1f7c0a..cc24316 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -606,8 +606,8 @@ Definition transl_fundef (f: Clight.fundef) : res fundef := | Clight.Internal g => do tg <- transl_function g; OK(AST.Internal tg) | Clight.External ef args res => - if list_typ_eq ef.(ef_sig).(sig_args) (typlist_of_typelist args) - && opt_typ_eq ef.(ef_sig).(sig_res) (opttyp_of_type res) + if list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist args) + && opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type res) then OK(AST.External ef) else Error(msg "Cshmgen.transl_fundef: wrong external signature") end. diff --git a/common/AST.v b/common/AST.v index bca0535..4f113c7 100644 --- a/common/AST.v +++ b/common/AST.v @@ -397,15 +397,84 @@ Qed. (** * External functions *) (** For most languages, the functions composing the program are either - internal functions, defined within the language, or external functions - (a.k.a. system calls) that emit an event when applied. We define - a type for such functions and some generic transformation functions. *) - -Record external_function : Type := mkextfun { - ef_id: ident; - ef_sig: signature; - ef_inline: bool -}. + internal functions, defined within the language, or external functions, + defined outside. External functions include system calls but also + compiler built-in functions. We define a type for external functions + and associated operations. *) + +Inductive external_function : Type := + | EF_external (name: ident) (sg: signature) + (** A system call or library function. Produces an event + in the trace. *) + | EF_builtin (name: ident) (sg: signature) + (** A compiler built-in function. Behaves like an external, but + can be inlined by the compiler. *) + | EF_vload (chunk: memory_chunk) + (** A volatile read operation. If the adress given as first argument + points within a volatile global variable, generate an + event and return the value found in this event. Otherwise, + produce no event and behave like a regular memory load. *) + | EF_vstore (chunk: memory_chunk) + (** A volatile store operation. If the adress given as first argument + points within a volatile global variable, generate an event. + Otherwise, produce no event and behave like a regular memory store. *) + | EF_malloc + (** Dynamic memory allocation. Takes the requested size in bytes + as argument; returns a pointer to a fresh block of the given size. + Produces no observable event. *) + | EF_free + (** Dynamic memory deallocation. Takes a pointer to a block + allocated by an [EF_malloc] external call and frees the + corresponding block. + Produces no observable event. *) + | EF_memcpy (sz: Z) (al: Z) + (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *) + | EF_annot (text: ident) (targs: list typ) + (** A programmer-supplied annotation. Takes zero, one or several arguments, + produces an event carrying the text and the values of these arguments, + and returns no value. *) + | EF_annot_val (text:ident) (targ: typ). + (** Another form of annotation that takes one argument, produces + an event carrying the text and the value of this argument, + and returns the value of the argument. *) + +(** The type signature of an external function. *) + +Definition ef_sig (ef: external_function): signature := + match ef with + | EF_external name sg => sg + | EF_builtin name sg => sg + | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) + | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None + | EF_malloc => mksignature (Tint :: nil) (Some Tint) + | EF_free => mksignature (Tint :: nil) None + | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None + | EF_annot text targs => mksignature targs None + | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) + end. + +(** Whether an external function should be inlined by the compiler. *) + +Definition ef_inline (ef: external_function) : bool := + match ef with + | EF_external name sg => false + | EF_builtin name sg => true + | EF_vload chunk => true + | EF_vstore chunk => true + | EF_malloc => false + | EF_free => false + | EF_memcpy sz al => true + | EF_annot text targs => true + | EF_annot_val text targ => true + end. + +(** Whether an external function must reload its arguments. *) + +Definition ef_reloads (ef: external_function) : bool := + match ef with + | EF_annot text targs => false + | _ => true + end. (** Function definitions are the union of internal and external functions. *) diff --git a/common/Events.v b/common/Events.v index b369d46..ac6c1a0 100644 --- a/common/Events.v +++ b/common/Events.v @@ -401,41 +401,6 @@ End EVENTVAL_INV. (** * Semantics of external functions *) -(** Each external function is of one of the following kinds: *) - -Inductive extfun_kind: signature -> Type := - | EF_syscall (name: ident) (sg: signature): extfun_kind sg - (** A system call. Takes representable arguments (integers, floats, - pointers to globals), produces a representable result, - does not modify the memory, and produces an [Event_syscall] event - in the trace. *) - | EF_vload (chunk: memory_chunk): extfun_kind (mksignature (Tint :: nil) (Some (type_of_chunk chunk))) - (** A volatile read operation. If the adress given as first argument - points within a volatile global variable, generate an [Event_vload] - event and return the value found in this event. Otherwise, - produce no event and behave like a regular memory load. *) - | EF_vstore (chunk: memory_chunk): extfun_kind (mksignature (Tint :: type_of_chunk chunk :: nil) None) - (** A volatile store operation. If the adress given as first argument - points within a volatile global variable, generate an [Event_vstore] - event. Otherwise, produce no event and behave like a regular memory store. *) - | EF_malloc: extfun_kind (mksignature (Tint :: nil) (Some Tint)) - (** Dynamic memory allocation. Takes the requested size in bytes - as argument; returns a pointer to a fresh block of the given size. - Produces no observable event. *) - | EF_free: extfun_kind (mksignature (Tint :: nil) None) - (** Dynamic memory deallocation. Takes a pointer to a block - allocated by an [EF_malloc] external call and frees the - corresponding block. - Produces no observable event. *) - | EF_annotation (text: ident) (sg: signature): extfun_kind sg. - (** A programmer-supplied annotation. Takes representable arguments, - returns its first argument as result (or [Vundef] if no arguments), - does not modify the memory, and produces an [Event_annot] - event in the trace. *) - -Parameter classify_external_function: - forall (ef: external_function), extfun_kind (ef.(ef_sig)). - (** For each external function, its behavior is defined by a predicate relating: - the global environment - the values of the arguments passed to this function @@ -934,6 +899,20 @@ Proof. inv H; inv H0. intuition congruence. Qed. +(** ** Semantics of [memcpy] operations. *) + +(** To be done once [storebytes] is added to the [Memtype] interface. *) + +Definition extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := + fun vargs m1 t vres m2 => False. + +Lemma extcall_memcpy_ok: + forall sz al, + extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None). +Proof. + intros. unfold extcall_memcpy_sem; constructor; contradiction. +Qed. + (** ** Semantics of system calls. *) Inductive extcall_io_sem (name: ident) (sg: signature) (F V: Type) (ge: Genv.t F V): @@ -984,23 +963,19 @@ Qed. (** ** Semantics of annotation. *) -Inductive extcall_annot_sem (text: ident) (sg: signature) (F V: Type) (ge: Genv.t F V): +Inductive extcall_annot_sem (text: ident) (targs: list typ) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := - | extcall_annot_sem_intro: forall vargs m args vres, - eventval_list_match ge args (sig_args sg) vargs -> - sig_res sg = match sig_args sg with nil => None | t1 :: _ => Some t1 end -> - vres = match vargs with nil => Vundef | v1 :: _ => v1 end -> - extcall_annot_sem text sg ge vargs m (Event_annot text args :: E0) vres m. + | extcall_annot_sem_intro: forall vargs m args, + eventval_list_match ge args targs vargs -> + extcall_annot_sem text targs ge vargs m (Event_annot text args :: E0) Vundef m. Lemma extcall_annot_ok: - forall text sg, - extcall_properties (extcall_annot_sem text sg) sg. + forall text targs, + extcall_properties (extcall_annot_sem text targs) (mksignature targs None). Proof. intros; constructor; intros. - inv H. unfold proj_sig_res. rewrite H1. inv H0. - constructor. - eapply eventval_match_type; eauto. + inv H. simpl. auto. inv H. eapply eventval_list_match_length; eauto. @@ -1012,17 +987,15 @@ Proof. inv H; auto. inv H. - exists (match vargs' with nil => Vundef | v1 :: _ => v1 end); exists m1'; intuition. + exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. - inv H1; auto. red; auto. inv H0. - exists f; exists (match vargs' with nil => Vundef | v1 :: _ => v1 end); exists m1'; intuition. + exists f; exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. - inv H2; auto. red; auto. red; auto. red; intros; congruence. @@ -1032,6 +1005,48 @@ Proof. intuition. Qed. +Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_annot_val_sem_intro: forall varg m arg, + eventval_match ge arg targ varg -> + extcall_annot_val_sem text targ ge (varg :: nil) m (Event_annot text (arg :: nil) :: E0) varg m. + +Lemma extcall_annot_val_ok: + forall text targ, + extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ)). +Proof. + intros; constructor; intros. + + inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. + + inv H. auto. + + inv H1. econstructor; eauto. + eapply eventval_match_preserved; eauto. + + inv H; auto. + + inv H; auto. + + inv H. inv H1. inv H6. + exists v2; exists m1'; intuition. + econstructor; eauto. + eapply eventval_match_lessdef; eauto. + red; auto. + + inv H0. inv H2. inv H7. + exists f; exists v'; exists m1'; intuition. + econstructor; eauto. + eapply eventval_match_inject; eauto. + red; auto. + red; auto. + red; intros; congruence. + + inv H; inv H0. simpl in H1. + assert (arg = arg0). eapply eventval_match_determ_2; eauto. subst arg0. + intuition. +Qed. + (** ** Combined semantics of external calls *) (** Combining the semantics given above for the various kinds of external calls, @@ -1046,26 +1061,32 @@ Qed. This predicate is used in the semantics of all CompCert languages. *) Definition external_call (ef: external_function): extcall_sem := - match classify_external_function ef with - | EF_syscall name sg => extcall_io_sem name sg + match ef with + | EF_external name sg => extcall_io_sem name sg + | EF_builtin name sg => extcall_io_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk | EF_malloc => extcall_malloc_sem | EF_free => extcall_free_sem - | EF_annotation txt sg => extcall_annot_sem txt sg + | EF_memcpy sz al => extcall_memcpy_sem sz al + | EF_annot txt targs => extcall_annot_sem txt targs + | EF_annot_val txt targ=> extcall_annot_val_sem txt targ end. Theorem external_call_spec: forall ef, extcall_properties (external_call ef) (ef_sig ef). Proof. - intros. unfold external_call. destruct (classify_external_function ef). + intros. unfold external_call, ef_sig. destruct ef. + apply extcall_io_ok. apply extcall_io_ok. apply volatile_load_ok. apply volatile_store_ok. apply extcall_malloc_ok. apply extcall_free_ok. + apply extcall_memcpy_ok. apply extcall_annot_ok. + apply extcall_annot_val_ok. Qed. Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 98d9d8b..b52299a 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -796,17 +796,6 @@ let elab_expr loc env a = let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in { edesc = ECall(b1, [b2; b3]); etyp = ty } -(* Hack to treat __builtin_annotation the CompCert way. - Arguments are treated as per the prototype (const char *, ...). - Result type is type of second argument, or void if only one argument. *) - | CALL((VARIABLE "__builtin_annotation" as a1), al) -> - let b1 = elab a1 in - let bl = List.map elab al in - let bl' = elab_arguments 1 bl [Env.fresh_ident "", - TPtr(TInt(IChar, [AConst]),[])] true in - let tyres = match bl' with _ :: b2 :: _ -> b2.etyp | _ -> TVoid[] in - { edesc = ECall(b1, bl'); etyp = tyres } - | CALL(a1, al) -> let b1 = (* Catch the old-style usage of calling a function without diff --git a/driver/Complements.v b/driver/Complements.v index 334b9b0..e6b0095 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -97,15 +97,21 @@ Remark extcall_arguments_deterministic: extcall_arguments rs m sg args -> extcall_arguments rs m sg args' -> args = args'. Proof. - assert ( - forall rs m ll args, - extcall_args rs m ll args -> - forall args', extcall_args rs m ll args' -> args = args'). - induction 1; intros. - inv H. auto. - inv H1. decEq; eauto. - inv H; inv H4; congruence. - unfold extcall_arguments; intros; eauto. + unfold extcall_arguments; intros. + revert args H args' H0. generalize (Conventions1.loc_arguments sg); induction 1; intros. + inv H0; auto. + inv H1; decEq; auto. inv H; inv H4; congruence. +Qed. + +Remark annot_arguments_deterministic: + forall rs m pl args args', + annot_arguments rs m pl args -> + annot_arguments rs m pl args' -> args = args'. +Proof. + unfold annot_arguments; intros. + revert pl args H args' H0. induction 1; intros. + inv H0; auto. + inv H1; decEq; auto. inv H; inv H4; congruence. Qed. Lemma step_internal_deterministic: @@ -113,27 +119,35 @@ Lemma step_internal_deterministic: Asm.step ge s t1 s1 -> Asm.step ge s t2 s2 -> matching_traces t1 t2 -> s1 = s2 /\ t1 = t2. Proof. - intros. inv H; inv H0. - assert (c0 = c) by congruence. - assert (i0 = i) by congruence. - assert (rs'0 = rs') by congruence. - assert (m'0 = m') by congruence. - subst. auto. - replace i with (Pbuiltin ef args res) in H5 by congruence. simpl in H5. inv H5. - congruence. - replace i with (Pbuiltin ef args res) in H12 by congruence. simpl in H12. inv H12. - rewrite H2 in H7; inv H7. rewrite H3 in H8; inv H8. rewrite H4 in H9; inv H9. - exploit external_call_determ. eexact H5. eexact H12. auto. - intros [A [B C]]. subst. auto. - congruence. - congruence. - congruence. - assert (ef0 = ef) by congruence. subst ef0. - assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0. - exploit external_call_determ. - eexact H4. eexact H9. auto. - intros [A [B C]]. subst. - intuition congruence. + +Ltac InvEQ := + match goal with + | [ H1: ?x = ?y, H2: ?x = ?z |- _ ] => rewrite H1 in H2; inv H2; InvEQ + | _ => idtac + end. + + intros. inv H; inv H0; InvEQ. +(* regular, regular *) + split; congruence. +(* regular, builtin *) + simpl in H5; inv H5. +(* regular, annot *) + simpl in H5; inv H5. +(* builtin, regular *) + simpl in H12; inv H12. +(* builtin, builtin *) + exploit external_call_determ. eexact H5. eexact H12. auto. intros [A [B C]]. subst. + auto. +(* annot, regular *) + simpl in H13. inv H13. +(* annot, annot *) + exploit annot_arguments_deterministic. eexact H5. eexact H11. intros EQ; subst. + exploit external_call_determ. eexact H6. eexact H14. auto. intros [A [B C]]. subst. + auto. +(* extcall, extcall *) + exploit extcall_arguments_deterministic. eexact H5. eexact H10. intros EQ; subst. + exploit external_call_determ. eexact H4. eexact H9. auto. intros [A [B C]]. subst. + auto. Qed. Lemma initial_state_deterministic: @@ -146,10 +160,7 @@ Qed. Lemma final_state_not_step: forall ge st r, final_state st r -> nostep step ge st. Proof. - unfold nostep. intros. red; intros. inv H. inv H0. - unfold Vzero in H1. congruence. - unfold Vzero in H1. congruence. - unfold Vzero in H1. congruence. + unfold nostep. intros. red; intros. inv H. inv H0; unfold Vzero in H1; congruence. Qed. Lemma final_state_deterministic: @@ -186,7 +186,12 @@ Inductive instruction: Type := | Plabel(l: label) | Pallocframe(sz: Z)(ofs_ra ofs_link: int) | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) - | Pbuiltin(ef: external_function)(args: list preg)(res: preg). + | Pbuiltin(ef: external_function)(args: list preg)(res: preg) + | Pannot(ef: external_function)(args: list annot_param) + +with annot_param : Type := + | APreg: preg -> annot_param + | APstack: memory_chunk -> Z -> annot_param. Definition code := list instruction. Definition fundef := AST.fundef code. @@ -655,6 +660,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome end | Pbuiltin ef args res => Stuck (**r treated specially below *) + | Pannot ef args => + Stuck (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers @@ -696,20 +703,27 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := Mem.loadv Mfloat64 m (Val.add (rs (IR ESP)) (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 ESP) = 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 := @@ -734,13 +748,22 @@ Inductive step: state -> trace -> state -> Prop := #XMM6 <- Vundef #XMM7 <- Vundef #ST0 <- 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 -> Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> - extcall_arguments rs m ef.(ef_sig) args -> - rs' = (rs#(loc_external_result ef.(ef_sig)) <- res + extcall_arguments rs m (ef_sig ef) args -> + rs' = (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs RA)) -> step (State rs m) t (State rs' m'). diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 0e14dee..c87167b 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -441,6 +441,14 @@ Definition transl_store (chunk: memory_chunk) do r <- freg_of src; OK(Pmovsd_mf am r :: 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) @@ -486,6 +494,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) Pret :: k) | Mbuiltin ef args res => OK (Pbuiltin ef (List.map preg_of args) (preg_of res) :: k) + | Mannot ef args => + OK (Pannot ef (map transl_annot_param args) :: k) end. (** Translation of a code sequence *) diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 304b5da..a9b9f3b 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -479,6 +479,7 @@ Opaque loadind. destruct s0; monadInv H; auto. destruct s0; monadInv H; auto. monadInv H; auto. + monadInv H; auto. inv H; simpl. destruct (peq lbl l). congruence. auto. monadInv H; auto. eapply trans_eq. eapply transl_cond_label; eauto. auto. @@ -1009,6 +1010,36 @@ Proof. congruence. 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. monadInv H4. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H3); 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. + eapply match_states_intro with (ep := false); eauto with coqlib. + unfold nextinstr. rewrite Pregmap.gss. + rewrite <- H1; simpl. econstructor; eauto. + eapply code_tail_next_int; eauto. + apply agree_nextinstr. auto. + congruence. +Qed. + Lemma exec_Mcond_true_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (cond : condition) (args : list mreg) (lbl : Mach.label) @@ -1224,6 +1255,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/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index eb107ea..b3e7aaa 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -369,13 +369,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. exists (@nil val); split; 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. constructor; auto. Qed. @@ -390,6 +390,40 @@ 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. + unfold preg_of. destruct (mreg_type r); 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/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 9facf85..c9ee970 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/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 *) @@ -217,20 +218,20 @@ let need_masks = ref false (* Built-in functions *) -(* 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 ECX, EDX, XMM6 and XMM7 - inlined while printing asm code; take their arguments in 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 -> @@ -240,28 +241,36 @@ 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(ESP + %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 " movl %a, %a\n" ireg src ireg dst | FR src :: _, FR dst -> if dst <> src then fprintf oc " movsd %a, %a\n" freg src freg dst | _, _ -> assert false -(* Handling of __builtin_memcpy_alX_szY *) - -let re_builtin_memcpy = - Str.regexp "__builtin_memcpy\\(_al\\([248]\\)\\)?_sz\\([0-9]+\\)$" +(* Handling of memcpy *) (* Unaligned memory accesses are quite fast on IA32, so use large memory accesses regardless of alignment. *) -let print_builtin_memcpy oc sz 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 tmp = if src <> ECX && dst <> ECX then ECX else if src <> EDX && dst <> EDX then EDX @@ -284,54 +293,73 @@ let print_builtin_memcpy oc sz dst src = fprintf oc " movb %a, %d(%a)\n" ireg8 tmp ofs ireg dst; copy (ofs + 1) (sz - 1) end in + fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n" + comment sz al; if tmp = EAX && sz mod 4 <> 0 then fprintf oc " movd %a, %a\n" ireg EAX freg XMM7; copy 0 sz; if tmp = EAX && sz mod 4 <> 0 then - fprintf oc " movd %a, %a\n" freg XMM7 ireg EAX + fprintf oc " movd %a, %a\n" freg XMM7 ireg EAX; + 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; - 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 " movzbl 0(%a), %a\n" ireg addr ireg res - | "__builtin_volatile_read_int8signed", [IR addr], IR res -> + | Mint8signed, [IR addr], IR res -> fprintf oc " movsbl 0(%a), %a\n" ireg addr ireg res - | "__builtin_volatile_read_int16unsigned", [IR addr], IR res -> + | Mint16unsigned, [IR addr], IR res -> fprintf oc " movzwl 0(%a), %a\n" ireg addr ireg res - | "__builtin_volatile_read_int16signed", [IR addr], IR res -> + | Mint16signed, [IR addr], IR res -> fprintf oc " movswl 0(%a), %a\n" ireg addr ireg res - | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res -> + | Mint32, [IR addr], IR res -> fprintf oc " movl 0(%a), %a\n" ireg addr ireg res - | "__builtin_volatile_read_float32", [IR addr], FR res -> + | Mfloat32, [IR addr], FR res -> fprintf oc " cvtss2sd 0(%a), %a\n" ireg addr freg res - | "__builtin_volatile_read_float64", [IR addr], FR res -> + | Mfloat64, [IR addr], FR res -> fprintf oc " movsd 0(%a), %a\n" ireg addr freg res - (* 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] -> if Asmgen.low_ireg src then fprintf oc " movb %a, 0(%a)\n" ireg8 src ireg addr else begin fprintf oc " movl %a, %%ecx\n" ireg src; fprintf oc " movb %%cl, 0(%a)\n" ireg addr end - | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ -> + | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> if Asmgen.low_ireg src then fprintf oc " movw %a, 0(%a)\n" ireg16 src ireg addr else begin fprintf oc " movl %a, %%ecx\n" ireg src; fprintf oc " movw %%cx, 0(%a)\n" ireg addr end - | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ -> + | Mint32, [IR addr; IR src] -> fprintf oc " movl %a, 0(%a)\n" ireg src ireg addr - | "__builtin_volatile_write_float32", [IR addr; FR src], _ -> + | Mfloat32, [IR addr; FR src] -> fprintf oc " cvtsd2ss %a, %%xmm7\n" freg src; fprintf oc " movss %%xmm7, 0(%a)\n" ireg addr - | "__builtin_volatile_write_float64", [IR addr; FR src], _ -> + | Mfloat64, [IR addr; FR src] -> fprintf oc " movsd %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; + begin match name, args, res with (* Memory accesses *) | "__builtin_read_int16_reversed", [IR a1], IR res -> let tmp = if Asmgen.low_ireg res then res else ECX in @@ -380,10 +408,6 @@ let print_builtin_inlined oc name args res = fprintf oc " movsd %a, %a\n" freg a1 freg res; fprintf oc " minsd %a, %a\n" freg a2 freg res end - (* 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 - print_builtin_memcpy oc sz dst src (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -655,10 +679,28 @@ let print_instruction oc = function let sz = sp_adjustment sz in fprintf oc " addl $%ld, %%esp\n" sz | 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) = fprintf oc "%a: .quad 0x%Lx\n" label lbl n diff --git a/powerpc/Asm.v b/powerpc/Asm.v index d698524..fc29db0 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 6b47d75..4370753 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 3846a6c..0efe646 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 8f6f725..ee3aa38 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 ef53411..0c19932 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 diff --git a/test/regression/annot1.c b/test/regression/annot1.c index 42ab826..85ba9f7 100644 --- a/test/regression/annot1.c +++ b/test/regression/annot1.c @@ -2,22 +2,23 @@ /* Annotations */ -int f(int x, int y) +int f(int x) { - return __builtin_annotation("f(%1,%2)", x, y); + return __builtin_annot_intval("f(%1)", x + 1); } -double g(double x) +double g(double x, double y) { - return __builtin_annotation("g(%1 + 1.0)", x + 1.0); + __builtin_annot("g(%1, %2)", x, y); + return x + y; } int main() { - __builtin_annotation("calling f"); - printf("f returns %d\n", f(12, 34)); - __builtin_annotation("calling g"); - printf("f returns %.2f\n", g(3.14)); + __builtin_annot("calling f"); + printf("f returns %d\n", f(12)); + __builtin_annot("calling g"); + printf("g returns %.2f\n", g(3.14, 2.718)); return 0; } |