diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Bounds.v | 25 | ||||
-rw-r--r-- | backend/CMparser.mly | 2 | ||||
-rw-r--r-- | backend/LTLintyping.v | 2 | ||||
-rw-r--r-- | backend/LTLtyping.v | 2 | ||||
-rw-r--r-- | backend/Linear.v | 6 | ||||
-rw-r--r-- | backend/Lineartyping.v | 6 | ||||
-rw-r--r-- | backend/Mach.v | 14 | ||||
-rw-r--r-- | backend/Machsem.v | 35 | ||||
-rw-r--r-- | backend/Machtyping.v | 4 | ||||
-rw-r--r-- | backend/PrintLTL.ml | 7 | ||||
-rw-r--r-- | backend/PrintLTLin.ml | 18 | ||||
-rw-r--r-- | backend/PrintMach.ml | 29 | ||||
-rw-r--r-- | backend/PrintRTL.ml | 14 | ||||
-rw-r--r-- | backend/RTLtyping.v | 5 | ||||
-rw-r--r-- | backend/RTLtypingaux.ml | 5 | ||||
-rw-r--r-- | backend/Reload.v | 11 | ||||
-rw-r--r-- | backend/Reloadproof.v | 18 | ||||
-rw-r--r-- | backend/Reloadtyping.v | 7 | ||||
-rw-r--r-- | backend/Selection.v | 2 | ||||
-rw-r--r-- | backend/Stacking.v | 12 | ||||
-rw-r--r-- | backend/Stackingproof.v | 80 | ||||
-rw-r--r-- | backend/Stackingtyping.v | 3 |
22 files changed, 231 insertions, 76 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index 04156707..23fa3b56 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 1cd245ec..0b48c0f6 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 c928f3f6..1a20f735 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 791c7554..40a584f1 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 31c3feda..23f0324e 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 ef6194c0..390b6302 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 223d5ab1..3210a9e2 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 1a167a90..fe0ec37b 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 95ceafe6..2d8c83d3 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 cce00f63..3bfd8039 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 e0a32045..adff4834 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 5b4887e2..a6a1cc56 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 62ee2c99..620a9494 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 49f339d0..02359b93 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 7549ff49..17acbc6e 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 81b61998..0ad53e6e 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 09a91010..49640a34 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 60be59b9..eba5ad62 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 9e11bc35..9c037b82 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 09d98d6c..23a112ce 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 d651220d..fbe88823 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 d00d1b21..27de5571 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. |