diff options
71 files changed, 1736 insertions, 516 deletions
@@ -204,11 +204,7 @@ Inductive instruction : Type := | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list preg -> list 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. + | Pannot: external_function -> list (annot_arg preg) -> instruction. (**r annotation statement *) (** The pseudo-instructions are the following: @@ -766,20 +762,6 @@ Definition extcall_arguments Definition loc_external_result (sg: signature) : list preg := map 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 := @@ -808,8 +790,8 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) (fn_code f) = Some (Pannot ef args) -> - annot_arguments rs m args vargs -> - external_call' ef ge vargs m t v m' -> + eval_annot_args ge rs (rs SP) 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', @@ -860,16 +842,6 @@ Proof. intros. red in H0; red in H1. eauto. Qed. -Remark annot_arguments_determ: - forall rs m params args1 args2, - annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. -Proof. - unfold annot_arguments. intros. revert params args1 H args2 H0. - induction 1; intros. - inv H0; auto. - inv H1. decEq; eauto. inv H; inv H4. auto. congruence. -Qed. - Lemma semantics_determinate: forall p, determinate (semantics p). Proof. Ltac Equalities := @@ -888,8 +860,8 @@ Ltac Equalities := exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. inv H12. - assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. - exploit external_call_determ'. eexact H5. eexact H13. intros [A B]. + assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. @@ -898,7 +870,7 @@ Ltac Equalities := red; intros; inv H; simpl. omega. inv H3; eapply external_call_trace_length; eauto. - inv H4; eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. inv H2; eapply external_call_trace_length; eauto. (* initial states *) inv H; inv H0. f_equal. congruence. diff --git a/arm/Asmgen.v b/arm/Asmgen.v index de4b87fb..5a3a48e1 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -695,14 +695,6 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) Error (msg "Asmgen.transl_store") 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) @@ -737,7 +729,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mbuiltin ef args res => OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) | Mannot ef args => - OK (Pannot ef (map transl_annot_param args) :: k) + OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) | Mlabel lbl => OK (Plabel lbl :: k) | Mgoto lbl => diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index c687722c..6d9b134f 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -771,13 +771,16 @@ Opaque loadind. 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. + exploit annot_args_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. + erewrite <- sp_val by eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. + exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 6102d82d..fea99ef5 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -489,3 +489,16 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | _ => (Aindexed Int.zero, e:::Enil) end. +(** ** Arguments of annotations *) + +Nondetfunction annot_arg (e: expr) := + match e with + | Eop (Ointconst n) Enil => AA_int n + | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs + | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + AA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) + | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs + | _ => AA_base e + end. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index c68d2277..d3c3239a 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -864,4 +864,19 @@ Proof. exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Int.add_zero; auto. Qed. +Theorem eval_annot_arg: + forall a v, + eval_expr ge sp e m nil a v -> + CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. +Proof. + intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. +- constructor. +- constructor. +- constructor. +- simpl in H5. inv H5. constructor. +- subst v. constructor; auto. +- inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- constructor; auto. +Qed. + End CMCONSTR. diff --git a/backend/Allocation.v b/backend/Allocation.v index 919843b5..37b79a1a 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -22,6 +22,7 @@ Require Import Maps. Require Import Lattice. Require Import AST. Require Import Integers. +Require Import Floats. Require Import Memdata. Require Import Op. Require Import Registers. @@ -95,8 +96,9 @@ Inductive block_shape: Type := | BSbuiltin (ef: external_function) (args: list reg) (res: reg) (mv1: moves) (args': list mreg) (res': list mreg) (mv2: moves) (s: node) - | BSannot (text: ident) (targs: list annot_arg) (args: list reg) (res: reg) - (mv: moves) (args': list loc) (s: node) + | BSannot (ef: external_function) + (args: list (annot_arg reg)) (args': list (annot_arg loc)) + (s: node) | BScond (cond: condition) (args: list reg) (mv: moves) (args': list mreg) (s1 s2: node) | BSjumptable (arg: reg) @@ -276,13 +278,14 @@ Definition pair_instr_block assertion (external_function_eq ef ef'); assertion (check_succ s b3); Some(BSbuiltin ef args res mv1 args' res' mv2 s) - | Lannot ef' args' :: b2 => + | _ => None + end + | Iannot ef args s => + match b with + | Lannot ef' args' :: b1 => assertion (external_function_eq ef ef'); - assertion (check_succ s b2); - match ef with - | EF_annot txt typ => Some(BSannot txt typ args res mv1 args' s) - | _ => None - end + assertion (check_succ s b1); + Some(BSannot ef args args' s) | _ => None end | Icond cond args s1 s2 => @@ -696,6 +699,57 @@ Definition add_equation_ros (ros: reg + ident) (ros': mreg + ident) (e: eqs) : o | _, _ => None end. +(** [add_equations_annot_arg] adds the needed equations for annotation + arguments. *) + +Fixpoint add_equations_annot_arg (env: regenv) (arg: annot_arg reg) (arg': annot_arg loc) (e: eqs) : option eqs := + match arg, arg' with + | AA_base r, AA_base l => + Some (add_equation (Eq Full r l) e) + | AA_base r, AA_longofwords (AA_base lhi) (AA_base llo) => + assertion (typ_eq (env r) Tlong); + Some (add_equation (Eq Low r llo) (add_equation (Eq High r lhi) e)) + | AA_int n, AA_int n' => + assertion (Int.eq_dec n n'); Some e + | AA_long n, AA_long n' => + assertion (Int64.eq_dec n n'); Some e + | AA_float f, AA_float f' => + assertion (Float.eq_dec f f'); Some e + | AA_single f, AA_single f' => + assertion (Float32.eq_dec f f'); Some e + | AA_loadstack chunk ofs, AA_loadstack chunk' ofs' => + assertion (chunk_eq chunk chunk'); + assertion (Int.eq_dec ofs ofs'); + Some e + | AA_addrstack ofs, AA_addrstack ofs' => + assertion (Int.eq_dec ofs ofs'); + Some e + | AA_loadglobal chunk id ofs, AA_loadglobal chunk' id' ofs' => + assertion (chunk_eq chunk chunk'); + assertion (ident_eq id id'); + assertion (Int.eq_dec ofs ofs'); + Some e + | AA_addrglobal id ofs, AA_addrglobal id' ofs' => + assertion (ident_eq id id'); + assertion (Int.eq_dec ofs ofs'); + Some e + | AA_longofwords hi lo, AA_longofwords hi' lo' => + do e1 <- add_equations_annot_arg env hi hi' e; + add_equations_annot_arg env lo lo' e1 + | _, _ => + None + end. + +Fixpoint add_equations_annot_args (env: regenv) + (args: list(annot_arg reg)) (args': list(annot_arg loc)) (e: eqs) : option eqs := + match args, args' with + | nil, nil => Some e + | a1 :: al, a1' :: al' => + do e1 <- add_equations_annot_arg env a1 a1' e; + add_equations_annot_args env al al' e1 + | _, _ => None + end. + (** [can_undef ml] returns true if all machine registers in [ml] are unconstrained and can harmlessly be undefined. *) @@ -926,9 +980,8 @@ Definition transfer_aux (f: RTL.function) (env: regenv) assertion (can_undef (destroyed_by_builtin ef) e2); do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2; track_moves env mv1 e3 - | BSannot txt typ args res mv1 args' s => - do e1 <- add_equations_args args (annot_args_typ typ) args' e; - track_moves env mv1 e1 + | BSannot ef args args' s => + add_equations_annot_args env args args' e | BScond cond args mv args' s1 s2 => assertion (can_undef (destroyed_by_cond cond) e); do e1 <- add_equations args args' e; @@ -1099,7 +1152,7 @@ Definition successors_block_shape (bsh: block_shape) : list node := | BScall sg ros args res mv1 ros' mv2 s => s :: nil | BStailcall sg ros args mv1 ros' => nil | BSbuiltin ef args res mv1 args' res' mv2 s => s :: nil - | BSannot txt typ args res mv1 args' s => s :: nil + | BSannot ef args args' s => s :: nil | BScond cond args mv args' s1 s2 => s1 :: s2 :: nil | BSjumptable arg mv arg' tbl => tbl | BSreturn optarg mv => nil diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 2612ebf2..875d4929 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -165,12 +165,10 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr (Ibuiltin ef args res s) (expand_moves mv1 (Lbuiltin ef args' res' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_annot: forall txt typ args res mv args' s k, - wf_moves mv -> - expand_block_shape (BSannot txt typ args res mv args' s) - (Ibuiltin (EF_annot txt typ) args res s) - (expand_moves mv - (Lannot (EF_annot txt typ) args' :: Lbranch s :: k)) + | ebs_annot: forall ef args args' s k, + expand_block_shape (BSannot ef args args' s) + (Iannot ef args s) + (Lannot ef args' :: Lbranch s :: k) | ebs_cond: forall cond args mv args' s1 s2 k, wf_moves mv -> expand_block_shape (BScond cond args mv args' s1 s2) @@ -322,7 +320,8 @@ Proof. (* builtin *) destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. econstructor; eauto. - destruct ef; inv H. econstructor; eauto. +(* annot *) + destruct b; MonadInv. destruct i; MonadInv. UseParsingLemmas. constructor. (* cond *) destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. econstructor; eauto. (* jumptable *) @@ -1348,6 +1347,75 @@ Proof. rewrite Int64.hi_ofwords, Int64.lo_ofwords; auto. Qed. +Lemma add_equations_annot_arg_satisf: + forall env rs ls arg arg' e e', + add_equations_annot_arg env arg arg' e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction arg; destruct arg'; simpl; intros; MonadInv; eauto. + eapply add_equation_satisf; eauto. + destruct arg'1; MonadInv. destruct arg'2; MonadInv. eauto using add_equation_satisf. +Qed. + +Lemma add_equations_annot_arg_lessdef: + forall env (ge: RTL.genv) sp rs ls m arg v, + eval_annot_arg ge (fun r => rs#r) sp m arg v -> + forall e e' arg', + add_equations_annot_arg env arg arg' e = Some e' -> + satisf rs ls e' -> + wt_regset env rs -> + exists v', eval_annot_arg ge ls sp m arg' v' /\ Val.lessdef v v'. +Proof. + induction 1; simpl; intros e e' arg' AE SAT WT; destruct arg'; MonadInv. +- exploit add_equation_lessdef; eauto. simpl; intros. + exists (ls x0); auto with aarg. +- destruct arg'1; MonadInv. destruct arg'2; MonadInv. + exploit add_equation_lessdef. eauto. simpl; intros LD1. + exploit add_equation_lessdef. eapply add_equation_satisf. eauto. simpl; intros LD2. + exists (Val.longofwords (ls x0) (ls x1)); split; auto with aarg. + rewrite <- (val_longofwords_eq rs#x). apply Val.longofwords_lessdef; auto. + rewrite <- e0; apply WT. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- exploit IHeval_annot_arg1; eauto. eapply add_equations_annot_arg_satisf; eauto. + intros (v1 & A & B). + exploit IHeval_annot_arg2; eauto. intros (v2 & C & D). + exists (Val.longofwords v1 v2); split; auto with aarg. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma add_equations_annot_args_satisf: + forall env rs ls arg arg' e e', + add_equations_annot_args env arg arg' e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction arg; destruct arg'; simpl; intros; MonadInv; eauto using add_equations_annot_arg_satisf. +Qed. + +Lemma add_equations_annot_args_lessdef: + forall env (ge: RTL.genv) sp rs ls m tm arg vl, + eval_annot_args ge (fun r => rs#r) sp m arg vl -> + forall arg' e e', + add_equations_annot_args env arg arg' e = Some e' -> + satisf rs ls e' -> + wt_regset env rs -> + Mem.extends m tm -> + exists vl', eval_annot_args ge ls sp tm arg' vl' /\ Val.lessdef_list vl vl'. +Proof. + induction 1; simpl; intros; destruct arg'; MonadInv. +- exists (@nil val); split; constructor. +- exploit IHlist_forall2; eauto. intros (vl' & A & B). + exploit add_equations_annot_arg_lessdef; eauto. + eapply add_equations_annot_args_satisf; eauto. intros (v1' & C & D). + exploit (@eval_annot_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F). + exists (v1'' :: vl'); split; constructor; auto. eapply Val.lessdef_trans; eauto. +Qed. + (** * Properties of the dataflow analysis *) Lemma analyze_successors: @@ -2035,27 +2103,21 @@ Proof. econstructor; eauto. (* annot *) -- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto. - inv WTI. simpl in H4. rewrite <- H4. apply wt_regset_list; auto. - intros [v' [m'' [F [G [J K]]]]]. - assert (v = Vundef). red in H0; inv H0. auto. +- exploit add_equations_annot_args_lessdef; eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros [vres' [m'' [F [G [J K]]]]]. econstructor; split. eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. eapply star_two. econstructor. - eapply external_call_symbols_preserved' with (ge1 := ge). - econstructor; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved with (ge1 := ge); eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eauto. constructor. eauto. eauto. traceEq. + constructor. eauto. traceEq. exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply satisf_undef_reg with (r := res). - eapply add_equations_args_satisf; eauto. + eapply add_equations_annot_args_satisf; eauto. intros [enext [U V]]. econstructor; eauto. - change (destroyed_by_builtin (EF_annot txt typ)) with (@nil mreg). - simpl. subst v. assumption. - apply wt_regset_assign; auto. subst v. constructor. (* cond *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 3801a4f6..ba7fa3a6 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -358,34 +358,27 @@ 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' -> - Mach.annot_arg ms m sp p v -> - exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'. +Remark annot_arg_match: + forall ge (rs: regset) sp m a v, + eval_annot_arg ge (fun r => rs (preg_of r)) sp m a v -> + eval_annot_arg ge rs sp m (map_annot_arg preg_of a) 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. + induction 1; simpl; eauto with aarg. Qed. -Lemma annot_arguments_match: - forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall pl vl, - Mach.annot_arguments ms m sp pl vl -> - exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl' +Lemma annot_args_match: + forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> + forall al vl, eval_annot_args ge ms sp m al vl -> + exists vl', eval_annot_args ge rs sp m' (map (map_annot_arg preg_of) al) 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]]. + induction 3; intros; simpl. + exists (@nil val); split; constructor. + exploit (@eval_annot_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto. + intros; eapply preg_val; eauto. + intros (v1' & A & B). destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. + exists (v1' :: vl'); split; constructor; auto. apply annot_arg_match; auto. Qed. (** * Correspondence between Mach code and Asm code *) diff --git a/backend/Bounds.v b/backend/Bounds.v index bcd28487..249ff796 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -69,7 +69,7 @@ Definition instr_within_bounds (i: instruction) := | Lbuiltin ef args res => forall r, In r res \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r | Lannot ef args => - forall sl ofs ty, In (S sl ofs ty) args -> slot_within_bounds sl ofs ty + forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args args) -> slot_within_bounds sl ofs ty | _ => True end. @@ -121,7 +121,7 @@ Definition slots_of_instr (i: instruction) : list (slot * Z * typ) := match i with | Lgetstack sl ofs ty r => (sl, ofs, ty) :: nil | Lsetstack r sl ofs ty => (sl, ofs, ty) :: nil - | Lannot ef args => slots_of_locs args + | Lannot ef args => slots_of_locs (params_of_annot_args args) | _ => nil end. diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 10cf8bf4..69b70e72 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -55,8 +55,7 @@ let mkef sg toks = | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] -> EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al) | [EFT_tok "annot"; EFT_string txt] -> - EF_annot(intern_string txt, - List.map (fun t -> AA_arg t) sg.sig_args) + EF_annot(intern_string txt, sg.sig_args) | [EFT_tok "annot_val"; EFT_string txt] -> if sg.sig_args = [] then raise Parsing.Parse_error; EF_annot_val(intern_string txt, List.hd sg.sig_args) diff --git a/backend/CSE.v b/backend/CSE.v index fa229871..2c0c5f33 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -492,6 +492,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb | EF_vload _ | EF_vload_global _ _ _ | EF_annot _ _ | EF_annot_val _ _ => set_unknown before res end + | Iannot ef args s => + before | Icond cond args ifso ifnot => before | Ijumptable arg tbl => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index ae8052be..74e3ceca 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1144,6 +1144,21 @@ Proof. + apply CASE1. * apply set_reg_lessdef; auto. +- (* Iannot *) + exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros (v' & m1' & P & Q & R & S). + econstructor; split. + eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. replace m' with m; auto. + destruct ef; try contradiction. inv H2; auto. + - (* Icond *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. elim SAT; intros valu1 NH1. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index f952f1ea..d48a0553 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -296,7 +296,9 @@ Proof. econstructor; eauto with coqlib. (* Lannot *) left; econstructor; split. - econstructor; eauto. eapply external_call_symbols_preserved'; eauto. + econstructor; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. (* Llabel *) diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 03ef0926..668eb808 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -79,6 +79,7 @@ Inductive stmt : Type := | Scall : option ident -> signature -> expr + ident -> exprlist -> stmt | Stailcall: signature -> expr + ident -> exprlist -> stmt | Sbuiltin : option ident -> external_function -> exprlist -> stmt + | Sannot : external_function -> list (annot_arg expr) -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -248,6 +249,32 @@ Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := Genv.find_symbol ge id = Some b -> eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero). +Inductive eval_annot_arg: annot_arg expr -> val -> Prop := + | eval_AA_base: forall a v, + eval_expr nil a v -> + eval_annot_arg (AA_base a) v + | eval_AA_int: forall n, + eval_annot_arg (AA_int n) (Vint n) + | eval_AA_long: forall n, + eval_annot_arg (AA_long n) (Vlong n) + | eval_AA_float: forall n, + eval_annot_arg (AA_float n) (Vfloat n) + | eval_AA_single: forall n, + eval_annot_arg (AA_single n) (Vsingle n) + | eval_AA_loadstack: forall chunk ofs v, + Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v -> + eval_annot_arg (AA_loadstack chunk ofs) v + | eval_AA_addrstack: forall ofs, + eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs)) + | eval_AA_loadglobal: forall chunk id ofs v, + Mem.loadv chunk m (Genv.symbol_address ge id ofs) = Some v -> + eval_annot_arg (AA_loadglobal chunk id ofs) v + | eval_AA_addrglobal: forall id ofs, + eval_annot_arg (AA_addrglobal id ofs) (Genv.symbol_address ge id ofs) + | eval_AA_longofwords: forall a1 a2 v1 v2, + eval_expr nil a1 v1 -> eval_expr nil a2 v2 -> + eval_annot_arg (AA_longofwords (AA_base a1) (AA_base a2)) (Val.longofwords v1 v2). + End EVAL_EXPR. (** Pop continuation until a call or stop *) @@ -343,6 +370,13 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sbuiltin optid ef al) k sp e m) t (State f Sskip k sp (set_optvar optid v e) m') + | step_annot: forall f ef al k sp e m vl t v m', + match ef with EF_annot _ _ => True | _ => False end -> + list_forall2 (eval_annot_arg sp e m) al vl -> + external_call ef ge vl m t v m' -> + step (State f (Sannot ef al) k sp e m) + t (State f Sskip k sp e m') + | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) diff --git a/backend/Constprop.v b/backend/Constprop.v index bdfc4b17..ce56ff62 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -102,23 +102,22 @@ Definition num_iter := 10%nat. Definition successor (f: function) (ae: AE.t) (pc: node) : node := successor_rec num_iter f ae pc. -Fixpoint annot_strength_reduction - (ae: AE.t) (targs: list annot_arg) (args: list reg) := - match targs, args with - | AA_arg ty :: targs', arg :: args' => - let (targs'', args'') := annot_strength_reduction ae targs' args' in - match ty, areg ae arg with - | Tint, I n => (AA_int n :: targs'', args'') - | Tfloat, F n => if Compopts.generate_float_constants tt - then (AA_float n :: targs'', args'') - else (AA_arg ty :: targs'', arg :: args'') - | _, _ => (AA_arg ty :: targs'', arg :: args'') +Fixpoint annot_strength_reduction (ae: AE.t) (a: annot_arg reg) := + match a with + | AA_base r => + match areg ae r with + | I n => AA_int n + | L n => AA_long n + | F n => if Compopts.generate_float_constants tt then AA_float n else a + | FS n => if Compopts.generate_float_constants tt then AA_single n else a + | _ => a end - | targ :: targs', _ => - let (targs'', args'') := annot_strength_reduction ae targs' args in - (targ :: targs'', args'') - | _, _ => - (targs, args) + | AA_longofwords hi lo => + match annot_strength_reduction ae hi, annot_strength_reduction ae lo with + | AA_int nhi, AA_int nlo => AA_long (Int64.ofwords nhi nlo) + | hi', lo' => AA_longofwords hi' lo' + end + | _ => a end. Function builtin_strength_reduction @@ -134,9 +133,6 @@ Function builtin_strength_reduction | Ptr(Gl symb n1) => (EF_vstore_global chunk symb n1, r2 :: nil) | _ => (ef, args) end - | EF_annot text targs, args => - let (targs', args') := annot_strength_reduction ae targs args in - (EF_annot text targs', args') | _, _ => (ef, args) end. @@ -180,6 +176,8 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) | Ibuiltin ef args res s => let (ef', args') := builtin_strength_reduction ae ef args in Ibuiltin ef' args' res s + | Iannot ef args s => + Iannot ef (List.map (annot_strength_reduction ae) args) s | Icond cond args s1 s2 => let aargs := aregs ae args in match resolve_branch (eval_static_condition cond aargs) with diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 450050de..30bdd674 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -211,83 +211,56 @@ Proof. unfold successor; intros. apply match_successor_rec. Qed. -Section BUILTIN_STRENGTH_REDUCTION. - -Variable bc: block_classification. -Hypothesis GE: genv_match bc ge. -Variable ae: AE.t. -Variable rs: regset. -Hypothesis MATCH: ematch bc rs ae. - Lemma annot_strength_reduction_correct: - forall targs args targs' args' eargs, - annot_strength_reduction ae targs args = (targs', args') -> - eventval_list_match ge eargs (annot_args_typ targs) rs##args -> - exists eargs', - eventval_list_match ge eargs' (annot_args_typ targs') rs##args' - /\ annot_eventvals targs' eargs' = annot_eventvals targs eargs. + forall bc sp m rs ae, ematch bc rs ae -> + forall a v, + eval_annot_arg ge (fun r => rs#r) sp m a v -> + eval_annot_arg ge (fun r => rs#r) sp m (annot_strength_reduction ae a) v. Proof. - induction targs; simpl; intros. -- inv H. simpl. exists eargs; auto. -- destruct a. - + destruct args as [ | arg args0]; simpl in H0; inv H0. - destruct (annot_strength_reduction ae targs args0) as [targs'' args''] eqn:E. - exploit IHtargs; eauto. intros [eargs'' [A B]]. - assert (DFL: - exists eargs', - eventval_list_match ge eargs' (annot_args_typ (AA_arg ty :: targs'')) rs##(arg :: args'') - /\ annot_eventvals (AA_arg ty :: targs'') eargs' = ev1 :: annot_eventvals targs evl). - { - exists (ev1 :: eargs''); split. - simpl; constructor; auto. simpl. congruence. - } - destruct ty; destruct (areg ae arg) as [] eqn:E2; inv H; auto. - * exists eargs''; split; auto; simpl; f_equal; auto. - generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM. - inv VM. rewrite <- H0 in *. inv H5; auto. - * destruct (Compopts.generate_float_constants tt); inv H1; auto. - exists eargs''; split; auto; simpl; f_equal; auto. - generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM. - inv VM. rewrite <- H0 in *. inv H5; auto. - + destruct (annot_strength_reduction ae targs args) as [targs'' args''] eqn:E. - inv H. - exploit IHtargs; eauto. intros [eargs'' [A B]]. - exists eargs''; simpl; split; auto. congruence. - + destruct (annot_strength_reduction ae targs args) as [targs'' args''] eqn:E. - inv H. - exploit IHtargs; eauto. intros [eargs'' [A B]]. - exists eargs''; simpl; split; auto. congruence. + induction 2; simpl; eauto with aarg. +- specialize (H x). unfold areg. destruct (AE.get x ae); try constructor. + + inv H. constructor. + + inv H. constructor. + + destruct (Compopts.generate_float_constants tt); [inv H|idtac]; constructor. + + destruct (Compopts.generate_float_constants tt); [inv H|idtac]; constructor. +- destruct (annot_strength_reduction ae hi); auto with aarg. + destruct (annot_strength_reduction ae lo); auto with aarg. + inv IHeval_annot_arg1; inv IHeval_annot_arg2. constructor. Qed. -Lemma vmatch_ptr_gl': - forall v id ofs, - vmatch bc v (Ptr (Gl id ofs)) -> - v = Vundef \/ exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b ofs. +Lemma annot_strength_reduction_correct_2: + forall bc sp m rs ae, ematch bc rs ae -> + forall al vl, + eval_annot_args ge (fun r => rs#r) sp m al vl -> + eval_annot_args ge (fun r => rs#r) sp m (List.map (annot_strength_reduction ae) al) vl. Proof. - intros. inv H; auto. inv H2. right; exists b; split; auto. eapply GE; eauto. -Qed. + induction 2; simpl; constructor; auto. eapply annot_strength_reduction_correct; eauto. +Qed. Lemma builtin_strength_reduction_correct: - forall ef args m t vres m', + forall bc ae rs ef args m t vres m', + genv_match bc ge -> + ematch bc rs ae -> external_call ef ge rs##args m t vres m' -> let (ef', args') := builtin_strength_reduction ae ef args in external_call ef' ge rs##args' m t vres m'. Proof. - intros until m'. functional induction (builtin_strength_reduction ae ef args); intros; auto. + intros until m'. intros GE MATCH. + assert (M: forall v id ofs, + vmatch bc v (Ptr (Gl id ofs)) -> + v = Vundef \/ exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b ofs). + { intros. inv H; auto. inv H2. right; exists b; split; auto. eapply GE; eauto. } + functional induction (builtin_strength_reduction ae ef args); intros; auto. + simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). - exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]]. + exploit M; eauto. intros [A | [b [A B]]]. * simpl in H; rewrite A in H; inv H. * simpl; rewrite volatile_load_global_charact; simpl. exists b; split; congruence. + simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). - exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]]. + exploit M; eauto. intros [A | [b [A B]]]. * simpl in H; rewrite A in H; inv H. * simpl; rewrite volatile_store_global_charact; simpl. exists b; split; congruence. -+ inv H. exploit annot_strength_reduction_correct; eauto. intros [eargs' [A B]]. - rewrite <- B. econstructor; eauto. Qed. -End BUILTIN_STRENGTH_REDUCTION. - (** The proof of semantic preservation is a simulation argument based on "option" diagrams of the following form: << @@ -521,6 +494,21 @@ Opaque builtin_strength_reduction. eapply match_states_succ; eauto. simpl; auto. apply set_reg_lessdef; auto. + (* Iannot *) + rename pc'0 into pc. TransfInstr; intros. + exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). + apply REGS. eauto. + eapply annot_strength_reduction_correct_2 with (ae := ae); eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros (v' & P & Q & R & S & T). + left; econstructor; econstructor; split. + eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved. eexact symbols_preserved. eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply match_states_succ; eauto. + (* Icond, preserved *) rename pc' into pc. TransfInstr. set (ac := eval_static_condition cond (aregs ae args)). diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 98bc14a8..9a8f85d2 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -70,6 +70,17 @@ Definition is_dead (v: nval) := Definition is_int_zero (v: nval) := match v with I n => Int.eq n Int.zero | _ => false end. +Fixpoint transfer_annot_arg (na: NA.t) (a: annot_arg reg) : NA.t := + let (ne, nm) := na in + match a with + | AA_base r => (add_need_all r ne, nm) + | AA_int _ | AA_long _ | AA_float _ | AA_single _ + | AA_addrstack _ | AA_addrglobal _ _ => (ne, nm) + | AA_loadstack chunk ofs => (ne, nmem_add nm (Stk ofs) (size_chunk chunk)) + | AA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk)) + | AA_longofwords hi lo => transfer_annot_arg (transfer_annot_arg na hi) lo + end. + Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) (res: reg) (ne: NE.t) (nm: nmem) : NA.t := match ef, args with @@ -128,6 +139,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) nmem_dead_stack f.(fn_stacksize)) | Some(Ibuiltin ef args res s) => transfer_builtin approx!!pc ef args res ne nm + | Some(Iannot ef args s) => + List.fold_left transfer_annot_arg args after | Some(Icond cond args s1 s2) => (add_needs args (needs_of_condition cond) ne, nm) | Some(Ijumptable arg tbl) => diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 4d09c5ba..b998c631 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -547,39 +547,77 @@ Proof. eapply magree_monotone; eauto. intros; apply B; auto. Qed. -(** Properties of volatile memory accesses *) - -(* -Lemma transf_volatile_load: - - forall s f sp pc e m te r tm nm chunk t v m', - - volatile_load_sem chunk ge (addr :: nil) m t v m' -> - Val.lessdef addr taddr -> +(** Annotation arguments *) + +Lemma transfer_annot_arg_sound: + forall bc e e' sp m m' a v, + eval_annot_arg ge (fun r => e#r) (Vptr sp Int.zero) m a v -> + forall ne1 nm1 ne2 nm2, + transfer_annot_arg (ne1, nm1) a = (ne2, nm2) -> + eagree e e' ne2 -> + magree m m' (nlive ge sp nm2) -> genv_match bc ge -> bc sp = BCstack -> - pmatch - - sound_state prog (State s f (Vptr sp Int.zero) pc e m) -> - Val.lessdef e#r te#r -> - magree m tm - (nlive ge sp - (nmem_add nm (aaddr (vanalyze rm f) # pc r) (size_chunk chunk))) -> - m' = m /\ - exists tv, volatile_load_sem chunk ge (te#r :: nil) tm t tv tm /\ Val.lessdef v tv. + exists v', + eval_annot_arg ge (fun r => e'#r) (Vptr sp Int.zero) m' a v' + /\ Val.lessdef v v' + /\ eagree e e' ne1 + /\ magree m m' (nlive ge sp nm1). Proof. - intros. inv H2. split; auto. rewrite <- H3 in H0; inv H0. inv H4. -- (* volatile *) - exists (Val.load_result chunk v0); split; auto. - constructor. constructor; auto. -- (* not volatile *) + induction 1; simpl; intros until nm2; intros TR EA MA GM SPM; inv TR. +- exists e'#x; intuition auto. constructor. eauto 2 with na. eauto 2 with na. +- exists (Vint n); intuition auto. constructor. +- exists (Vlong n); intuition auto. constructor. +- exists (Vfloat n); intuition auto. constructor. +- exists (Vsingle n); intuition auto. constructor. +- simpl in H. exploit magree_load; eauto. + intros. eapply nlive_add; eauto with va. rewrite Int.add_zero_l in H0; auto. + intros (v' & A & B). + exists v'; intuition auto. constructor; auto. + eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto. +- exists (Vptr sp (Int.add Int.zero ofs)); intuition auto with na. constructor. +- unfold Senv.symbol_address in H; simpl in H. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; simpl in H; try discriminate. exploit magree_load; eauto. - exploit aaddr_sound; eauto. intros (bc & P & Q & R). - intros. eapply nlive_add; eauto. - intros (v' & P & Q). - exists v'; split. constructor. econstructor; eauto. auto. + intros. eapply nlive_add; eauto. constructor. apply GM; auto. + intros (v' & A & B). + exists v'; intuition auto. + constructor. simpl. unfold Senv.symbol_address; simpl; rewrite FS; auto. + eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto. +- exists (Senv.symbol_address ge id ofs); intuition auto with na. constructor. +- destruct (transfer_annot_arg (ne1, nm1) hi) as [ne' nm'] eqn:TR. + exploit IHeval_annot_arg2; eauto. intros (vlo' & A & B & C & D). + exploit IHeval_annot_arg1; eauto. intros (vhi' & P & Q & R & S). + exists (Val.longofwords vhi' vlo'); intuition auto. + constructor; auto. + apply Val.longofwords_lessdef; auto. +Qed. + +Lemma transfer_annot_args_sound: + forall e sp m e' m' bc al vl, + eval_annot_args ge (fun r => e#r) (Vptr sp Int.zero) m al vl -> + forall ne1 nm1 ne2 nm2, + List.fold_left transfer_annot_arg al (ne1, nm1) = (ne2, nm2) -> + eagree e e' ne2 -> + magree m m' (nlive ge sp nm2) -> + genv_match bc ge -> + bc sp = BCstack -> + exists vl', + eval_annot_args ge (fun r => e'#r) (Vptr sp Int.zero) m' al vl' + /\ Val.lessdef_list vl vl' + /\ eagree e e' ne1 + /\ magree m m' (nlive ge sp nm1). +Proof. +Local Opaque transfer_annot_arg. + induction 1; simpl; intros. +- inv H. exists (@nil val); intuition auto. constructor. +- destruct (transfer_annot_arg (ne1, nm1) a1) as [ne' nm'] eqn:TR. + exploit IHlist_forall2; eauto. intros (vs' & A1 & B1 & C1 & D1). + exploit transfer_annot_arg_sound; eauto. intros (v1' & A2 & B2 & C2 & D2). + exists (v1' :: vs'); intuition auto. constructor; auto. Qed. -*) + +(** Properties of volatile memory accesses *) Lemma transf_volatile_store: forall v1 v2 v1' v2' m tm chunk sp nm t v m', @@ -930,6 +968,21 @@ Ltac UseTransfer := apply eagree_update; eauto 3 with na. eapply mextends_agree; eauto. +- (* annot *) + TransfInstr; UseTransfer. + destruct (fold_left transfer_annot_arg args (ne, nm)) as [ne1 nm1] eqn:TR; simpl in *. + inv SS. exploit transfer_annot_args_sound; eauto. intros (vargs' & A & B & C & D). + assert (EC: m' = m /\ external_call ef ge vargs' tm t Vundef tm). + { destruct ef; try contradiction. inv H2. split; auto. simpl. constructor. + eapply eventval_list_match_lessdef; eauto. } + destruct EC as [EC1 EC2]; subst m'. + econstructor; split. + eapply exec_Iannot. eauto. auto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved with (ge1 := ge); eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply match_succ_states; eauto. simpl; auto. + - (* conditional *) TransfInstr; UseTransfer. econstructor; split. diff --git a/backend/Inlining.v b/backend/Inlining.v index cd347345..4f17d59c 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -203,6 +203,15 @@ Definition sop (ctx: context) (op: operation) := Definition saddr (ctx: context) (addr: addressing) := shift_stack_addressing (Int.repr ctx.(dstk)) addr. +Fixpoint sannotarg (ctx: context) (a: annot_arg reg) : annot_arg reg := + match a with + | AA_base x => AA_base (sreg ctx x) + | AA_loadstack chunk ofs => AA_loadstack chunk (Int.add ofs (Int.repr ctx.(dstk))) + | AA_addrstack ofs => AA_addrstack (Int.add ofs (Int.repr ctx.(dstk))) + | AA_longofwords hi lo => AA_longofwords (sannotarg ctx hi) (sannotarg ctx lo) + | _ => a + end. + (** The initial context, used to copy the CFG of a toplevel function. *) Definition initcontext (dpc dreg nreg: positive) (sz: Z) := @@ -382,6 +391,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit := | Ibuiltin ef args res s => set_instr (spc ctx pc) (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) + | Iannot ef args s => + set_instr (spc ctx pc) + (Iannot ef (map (sannotarg ctx) args) (spc ctx s)) | Icond cond args s1 s2 => set_instr (spc ctx pc) (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 9b1aec4c..e3c5bf2a 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -400,6 +400,63 @@ Proof. eapply function_ptr_translated; eauto. Qed. +(** Translation of annotation arguments. *) + +Lemma tr_annot_arg: + forall F bound ctx rs rs' sp sp' m m', + match_globalenvs F bound -> + agree_regs F ctx rs rs' -> + F sp = Some(sp', ctx.(dstk)) -> + Mem.inject F m m' -> + forall a v, + eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v -> + exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sannotarg ctx a) v' + /\ val_inject F v v'. +Proof. + intros until m'; intros MG AG SP MI. induction 1; simpl. +- exists rs'#(sreg ctx x); split. constructor. eapply agree_val_reg; eauto. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- exploit Mem.loadv_inject; eauto. + instantiate (1 := Vptr sp' (Int.add ofs (Int.repr (dstk ctx)))). + simpl. econstructor; eauto. rewrite Int.add_zero_l; auto. + intros (v' & A & B). exists v'; split; auto. constructor. simpl. rewrite Int.add_zero_l; auto. +- econstructor; split. constructor. simpl. econstructor; eauto. rewrite ! Int.add_zero_l; auto. +- assert (val_inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). + { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + inv MG. econstructor. eauto. rewrite Int.add_zero; auto. } + exploit Mem.loadv_inject; eauto. intros (v' & A & B). + exists v'; eauto with aarg. +- econstructor; split. constructor. + unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + inv MG. econstructor. eauto. rewrite Int.add_zero; auto. +- destruct IHeval_annot_arg1 as (v1 & A1 & B1). + destruct IHeval_annot_arg2 as (v2 & A2 & B2). + econstructor; split. eauto with aarg. apply val_longofwords_inject; auto. +Qed. + +Lemma tr_annot_args: + forall F bound ctx rs rs' sp sp' m m', + match_globalenvs F bound -> + agree_regs F ctx rs rs' -> + F sp = Some(sp', ctx.(dstk)) -> + Mem.inject F m m' -> + forall al vl, + eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl -> + exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sannotarg ctx) al) vl' + /\ val_list_inject F vl vl'. +Proof. + induction 5; simpl. +- exists (@nil val); split; constructor. +- exploit tr_annot_arg; eauto. intros (v1' & A & B). + destruct IHlist_forall2 as (vl' & C & D). + exists (v1' :: vl'); split; constructor; auto. +Qed. + (** ** Relating stacks *) Inductive match_stacks (F: meminj) (m m': mem): @@ -1030,6 +1087,29 @@ Proof. auto. intros. apply SSZ2. eapply external_call_max_perm; eauto. +(* annot *) + exploit tr_funbody_inv; eauto. intros TR; inv TR. + exploit match_stacks_inside_globalenvs; eauto. intros [bound MG]. + exploit tr_annot_args; eauto. intros (vargs' & P & Q). + exploit external_call_mem_inject; eauto. + eapply match_stacks_inside_globals; eauto. + intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]]. + left; econstructor; split. + eapply plus_one. eapply exec_Iannot; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + econstructor. + eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. + intros; eapply external_call_max_perm; eauto. + intros; eapply external_call_max_perm; eauto. + auto. + eapply agree_regs_incr; eauto. auto. auto. + eapply external_call_valid_block; eauto. + eapply range_private_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + auto. + intros. apply SSZ2. eapply external_call_max_perm; eauto. + (* cond *) exploit tr_funbody_inv; eauto. intros TR; inv TR. assert (eval_condition cond rs'##(sregs ctx args) m' = Some b). diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index b5948a22..f7e6c317 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -316,6 +316,9 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop := Ple res ctx.(mreg) -> c!(spc ctx pc) = Some (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) -> tr_instr ctx pc (Ibuiltin ef args res s) c + | tr_annot: forall ctx pc c ef args s, + c!(spc ctx pc) = Some (Iannot ef (map (sannotarg ctx) args) (spc ctx s)) -> + tr_instr ctx pc (Iannot ef args s) c | tr_cond: forall ctx pc cond args s1 s2 c, c!(spc ctx pc) = Some (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) -> tr_instr ctx pc (Icond cond args s1 s2) c diff --git a/backend/LTL.v b/backend/LTL.v index dd79c8e3..8c2749a7 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -45,7 +45,7 @@ Inductive instruction: Type := | Lcall (sg: signature) (ros: mreg + ident) | Ltailcall (sg: signature) (ros: mreg + ident) | Lbuiltin (ef: external_function) (args: list mreg) (res: list mreg) - | Lannot (ef: external_function) (args: list loc) + | Lannot (ef: external_function) (args: list (annot_arg loc)) | Lbranch (s: node) | Lcond (cond: condition) (args: list mreg) (s1 s2: node) | Ljumptable (arg: mreg) (tbl: list node) @@ -244,8 +244,9 @@ Inductive step: state -> trace -> state -> Prop := rs' = Locmap.setlist (map R res) vl (undef_regs (destroyed_by_builtin ef) rs) -> step (Block s f sp (Lbuiltin ef args res :: bb) rs m) t (Block s f sp bb rs' m') - | exec_Lannot: forall s f sp ef args bb rs m t vl m', - external_call' ef ge (map rs args) m t vl m' -> + | exec_Lannot: forall s f sp ef args bb rs vl m t v' m', + eval_annot_args ge rs sp m args vl -> + external_call ef ge vl m t v' m' -> step (Block s f sp (Lannot ef args :: bb) rs m) t (Block s f sp bb rs m') | exec_Lbranch: forall s f sp pc bb rs m, diff --git a/backend/Linear.v b/backend/Linear.v index 56d1eb99..5d1fc0d8 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -42,7 +42,7 @@ Inductive instruction: Type := | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction | Lbuiltin: external_function -> list mreg -> list mreg -> instruction - | Lannot: external_function -> list loc -> instruction + | Lannot: external_function -> list (annot_arg loc) -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -204,8 +204,9 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Lbuiltin ef args res :: b) rs m) t (State s f sp b 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' -> + forall s f sp rs m ef args vl b t v m', + eval_annot_args ge rs sp m args vl -> + external_call ef ge vl 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: diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 63fa6565..08bcd3f3 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -651,7 +651,8 @@ Proof. (* Lannot *) left; econstructor; split. simpl. apply plus_one. eapply exec_Lannot; eauto. - eapply external_call_symbols_preserved'; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index ccf17e1e..c093b62d 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -76,7 +76,7 @@ Definition wt_instr (i: instruction) : bool := | Lbuiltin ef args res => subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res) | Lannot ef args => - forallb loc_valid args + forallb loc_valid (params_of_annot_args args) | _ => true end. @@ -365,7 +365,7 @@ Qed. Lemma wt_state_annot: forall s f sp ef args c rs m, wt_state (State s f sp (Lannot ef args :: c) rs m) -> - forallb (loc_valid f) args = true. + forallb (loc_valid f) (params_of_annot_args args) = true. Proof. intros. inv H. simpl in WTC; InvBooleans. auto. Qed. diff --git a/backend/Liveness.v b/backend/Liveness.v index 3a5bde97..ce1a798a 100644 --- a/backend/Liveness.v +++ b/backend/Liveness.v @@ -93,6 +93,8 @@ Definition transfer reg_list_live args (reg_sum_live ros Regset.empty) | Ibuiltin ef args res s => reg_list_live args (reg_dead res after) + | Iannot ef args s => + reg_list_live (params_of_annot_args args) after | Icond cond args ifso ifnot => reg_list_live args after | Ijumptable arg tbl => diff --git a/backend/Mach.v b/backend/Mach.v index ff72a828..fe00d42d 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -61,16 +61,12 @@ Inductive instruction: Type := | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction | Mbuiltin: external_function -> list mreg -> list mreg -> instruction - | Mannot: external_function -> list annot_param -> instruction + | Mannot: external_function -> list (annot_arg mreg) -> instruction | Mlabel: label -> instruction | Mgoto: label -> instruction | Mcond: condition -> list mreg -> label -> instruction | Mjumptable: mreg -> list label -> instruction - | Mreturn: instruction - -with annot_param: Type := - | APreg: mreg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Mreturn: instruction. Definition code := list instruction. @@ -225,19 +221,6 @@ Definition extcall_arguments (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. *) (** Mach execution states. *) @@ -352,8 +335,8 @@ Inductive step: state -> trace -> state -> Prop := t (State s f sp b rs' 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' -> + eval_annot_args ge rs sp m 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: diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 54174b9f..0176224d 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -90,11 +90,34 @@ let print_file_line_d1 oc pref file line = let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" -type arg_value = - | Reg of preg - | Stack of memory_chunk * Int.int - | Intconst of Int.int - | Floatconst of float +let rec print_annot print_preg sp_reg_name oc = function + | AA_base x -> print_preg oc x + | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n) + | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) + | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) + | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) + | AA_loadstack(chunk, ofs) -> + fprintf oc "mem(%s + %ld, %ld)" + sp_reg_name + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrstack ofs -> + fprintf oc "(%s + %ld)" + sp_reg_name + (camlint_of_coqint ofs) + | AA_loadglobal(chunk, id, ofs) -> + fprintf oc "mem(\"%s\" + %ld, %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrglobal(id, ofs) -> + fprintf oc "(\"%s\" + %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + | AA_longofwords(hi, lo) -> + fprintf oc "(%a * 0x100000000 + %a)" + (print_annot print_preg sp_reg_name) hi + (print_annot print_preg sp_reg_name) lo let print_annot_text print_preg sp_reg_name oc txt args = let print_fragment = function @@ -105,42 +128,18 @@ let print_annot_text print_preg sp_reg_name oc txt args = | Str.Delim s -> let n = int_of_string (String.sub s 1 (String.length s - 1)) in try - match List.nth args (n-1) with - | Reg r -> - print_preg oc r - | Stack(chunk, ofs) -> - fprintf oc "mem(%s + %ld, %ld)" - sp_reg_name - (camlint_of_coqint ofs) - (camlint_of_coqint (size_chunk chunk)) - | Intconst n -> - fprintf oc "%ld" (camlint_of_coqint n) - | Floatconst n -> - fprintf oc "%.18g" (camlfloat_of_coqfloat n) + print_annot print_preg sp_reg_name 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" -let rec annot_args tmpl args = - match tmpl, args with - | [], _ -> [] - | AA_arg _ :: tmpl', APreg r :: args' -> - Reg r :: annot_args tmpl' args' - | AA_arg _ :: tmpl', APstack(chunk, ofs) :: args' -> - Stack(chunk, ofs) :: annot_args tmpl' args' - | AA_arg _ :: tmpl', [] -> [] (* should never happen *) - | AA_int n :: tmpl', _ -> - Intconst n :: annot_args tmpl' args - | AA_float n :: tmpl', _ -> - Floatconst n :: annot_args tmpl' args - -let print_annot_stmt print_preg sp_reg_name oc txt tmpl args = - print_annot_text print_preg sp_reg_name oc txt (annot_args tmpl args) +let print_annot_stmt print_preg sp_reg_name oc txt tys args = + print_annot_text print_preg sp_reg_name oc txt args let print_annot_val print_preg oc txt args = print_annot_text print_preg "<internal error>" oc txt - (List.map (fun r -> Reg r) args) + (List.map (fun r -> AA_base r) args) (* Print CompCert version and command-line as asm comment *) diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 52e51309..27936f9b 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -81,8 +81,8 @@ let print_instruction pp succ = function fprintf pp "%a = %s(%a)" mregs res (name_of_external ef) mregs args | Lannot(ef, args) -> - fprintf pp "%s(%a)" - (name_of_external ef) locs args + fprintf pp "%s(%a)\n" + (name_of_external ef) (print_annot_args loc) args | Lbranch s -> print_succ pp s succ | Lcond(cond, args, s1, s2) -> diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index b356ca9e..8484a5c3 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -34,15 +34,6 @@ 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,7 +69,8 @@ let print_instruction pp i = fprintf pp "\t%a = %s(%a)\n" regs res (name_of_external ef) regs args | Mannot(ef, args) -> - fprintf pp "\t%s(%a)\n" (name_of_external ef) annot_params args + fprintf pp "\t%s(%a)\n" + (name_of_external ef) (print_annot_args reg) args | Mlabel lbl -> fprintf pp "%5d:" (P.to_int lbl) | Mgoto lbl -> diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 5c8347cb..ce2275cf 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -74,6 +74,10 @@ let print_instruction pp (pc, i) = fprintf pp "%a = %s(%a)\n" reg res (name_of_external ef) regs args; print_succ pp s (pc - 1) + | Iannot(ef, args, s) -> + fprintf pp "%s(%a)\n" + (name_of_external ef) (print_annot_args reg) args; + print_succ pp s (pc - 1) | Icond(cond, args, s1, s2) -> fprintf pp "if (%a) goto %d else goto %d\n" (PrintOp.print_condition reg) (cond, args) diff --git a/backend/RTL.v b/backend/RTL.v index e8ec1391..83761c42 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -74,6 +74,9 @@ Inductive instruction: Type := (** [Ibuiltin ef args dest succ] calls the built-in function identified by [ef], giving it the values of [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) + | Iannot: external_function -> list (annot_arg reg) -> node -> instruction + (** [Iannot ef args succ] is similar to [Ibuiltin] but specialized + to annotations. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -255,6 +258,14 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge rs##args m t v m' -> step (State s f sp pc rs m) t (State s f sp pc' (rs#res <- v) m') + | exec_Iannot: + forall s f sp pc rs m ef args pc' vargs vres t m', + (fn_code f)!pc = Some(Iannot ef args pc') -> + match ef with EF_annot _ _ => True | _ => False end -> + eval_annot_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + step (State s f sp pc rs m) + t (State s f sp pc' rs m') | exec_Icond: forall s f sp pc rs m cond args ifso ifnot b pc', (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> @@ -358,11 +369,14 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (State s0 f sp pc' (rs#res <- vres2) m2). eapply exec_Ibuiltin; eauto. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (State s0 f sp pc' rs m2). eapply exec_Iannot; eauto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate s0 vres2 m2). econstructor; eauto. (* trace length *) red; intros; inv H; simpl; try omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. Qed. (** * Operations on RTL abstract syntax *) @@ -397,6 +411,7 @@ Definition successors_instr (i: instruction) : list node := | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil | Ibuiltin ef args res s => s :: nil + | Iannot ef args s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ijumptable arg tbl => tbl | Ireturn optarg => nil @@ -418,6 +433,7 @@ Definition instr_uses (i: instruction) : list reg := | Itailcall sig (inl r) args => r :: args | Itailcall sig (inr id) args => args | Ibuiltin ef args res s => args + | Iannot ef args s => params_of_annot_args args | Icond cond args ifso ifnot => args | Ijumptable arg tbl => arg :: nil | Ireturn None => nil @@ -435,6 +451,7 @@ Definition instr_defs (i: instruction) : option reg := | Icall sig ros args res s => Some res | Itailcall sig ros args => None | Ibuiltin ef args res s => Some res + | Iannot ef args s => None | Icond cond args ifso ifnot => None | Ijumptable arg tbl => None | Ireturn optarg => None @@ -476,6 +493,7 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := | Itailcall sig (inl r) args => fold_left Pmax args (Pmax r m) | Itailcall sig (inr id) args => fold_left Pmax args m | Ibuiltin ef args res s => fold_left Pmax args (Pmax res m) + | Iannot ef args s => fold_left Pmax (params_of_annot_args args) m | Icond cond args ifso ifnot => fold_left Pmax args m | Ijumptable arg tbl => Pmax arg m | Ireturn None => m diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 26f51e3f..b1c36513 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -455,6 +455,39 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) transl_expr map b r nc end. +(** Translation of arguments to annotations. *) + +Definition exprlist_of_expr_list (l: list expr) : exprlist := + List.fold_right Econs Enil l. + +Fixpoint convert_annot_arg {A: Type} (a: annot_arg expr) (rl: list A) : annot_arg A * list A := + match a with + | AA_base a => + match rl with + | r :: rs => (AA_base r, rs) + | nil => (AA_int Int.zero, nil) (**r never happens *) + end + | AA_int n => (AA_int n, rl) + | AA_long n => (AA_long n, rl) + | AA_float n => (AA_float n, rl) + | AA_single n => (AA_single n, rl) + | AA_loadstack chunk ofs => (AA_loadstack chunk ofs, rl) + | AA_addrstack ofs => (AA_addrstack ofs, rl) + | AA_loadglobal chunk id ofs => (AA_loadglobal chunk id ofs, rl) + | AA_addrglobal id ofs => (AA_addrglobal id ofs, rl) + | AA_longofwords hi lo => + let (hi', rl1) := convert_annot_arg hi rl in + let (lo', rl2) := convert_annot_arg lo rl1 in + (AA_longofwords hi' lo', rl2) + end. + +Fixpoint convert_annot_args {A: Type} (al: list (annot_arg expr)) (rl: list A) : list (annot_arg A) := + match al with + | nil => nil + | a1 :: al => + let (a1', rl1) := convert_annot_arg a1 rl in a1' :: convert_annot_args al rl1 + end. + (** Auxiliary for translating exit expressions. *) Definition transl_exit (nexits: list node) (n: nat) : mon node := @@ -558,6 +591,11 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do r <- alloc_optreg map optid; do n1 <- add_instr (Ibuiltin ef rargs r nd); transl_exprlist map al rargs n1 + | Sannot ef args => + let al := exprlist_of_expr_list (params_of_annot_args args) in + do rargs <- alloc_regs map al; + do n1 <- add_instr (Iannot ef (convert_annot_args args rargs) nd); + transl_exprlist map al rargs n1 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 8acce510..02460f67 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -972,6 +972,234 @@ Proof. auto. Qed. +(** Annotation arguments. *) + +Lemma eval_exprlist_append: + forall le al1 vl1 al2 vl2, + eval_exprlist ge sp e m le (exprlist_of_expr_list al1) vl1 -> + eval_exprlist ge sp e m le (exprlist_of_expr_list al2) vl2 -> + eval_exprlist ge sp e m le (exprlist_of_expr_list (al1 ++ al2)) (vl1 ++ vl2). +Proof. + induction al1; simpl; intros vl1 al2 vl2 E1 E2; inv E1. +- auto. +- simpl. constructor; eauto. +Qed. + +Lemma invert_eval_annot_arg: + forall a v, + eval_annot_arg ge sp e m a v -> + exists vl, + eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_annot_arg a)) vl + /\ Events.eval_annot_arg ge (fun v => v) sp m (fst (convert_annot_arg a vl)) v + /\ (forall vl', convert_annot_arg a (vl ++ vl') = (fst (convert_annot_arg a vl), vl')). +Proof. + induction 1; simpl; econstructor; intuition eauto with evalexpr aarg. + constructor. + constructor. + repeat constructor. +Qed. + +Lemma invert_eval_annot_args: + forall al vl, + list_forall2 (eval_annot_arg ge sp e m) al vl -> + exists vl', + eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_annot_args al)) vl' + /\ Events.eval_annot_args ge (fun v => v) sp m (convert_annot_args al vl') vl. +Proof. + induction 1; simpl. +- exists (@nil val); split; constructor. +- exploit invert_eval_annot_arg; eauto. intros (vl1 & A & B & C). + destruct IHlist_forall2 as (vl2 & D & E). + exists (vl1 ++ vl2); split. + apply eval_exprlist_append; auto. + rewrite C; simpl. constructor; auto. +Qed. + +Lemma transl_eval_annot_arg: + forall rs a vl rl v, + Val.lessdef_list vl rs##rl -> + Events.eval_annot_arg ge (fun v => v) sp m (fst (convert_annot_arg a vl)) v -> + exists v', + Events.eval_annot_arg ge (fun r => rs#r) sp m (fst (convert_annot_arg a rl)) v' + /\ Val.lessdef v v' + /\ Val.lessdef_list (snd (convert_annot_arg a vl)) rs##(snd (convert_annot_arg a rl)). +Proof. + induction a; simpl; intros until v; intros LD EV; + try (now (inv EV; econstructor; eauto with aarg)). +- destruct rl; simpl in LD; inv LD; inv EV; simpl. + econstructor; eauto with aarg. + exists (rs#p); intuition auto. constructor. +- destruct (convert_annot_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *. + destruct (convert_annot_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *. + destruct (convert_annot_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *. + destruct (convert_annot_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *. + inv EV. + exploit IHa1; eauto. rewrite CV1; simpl; eauto. + rewrite CV1, CV3; simpl. intros (v1' & A1 & B1 & C1). + exploit IHa2. eexact C1. rewrite CV2; simpl; eauto. + rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2). + exists (Val.longofwords v1' v2'); split. constructor; auto. + split; auto. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma transl_eval_annot_args: + forall rs al vl1 rl vl, + Val.lessdef_list vl1 rs##rl -> + Events.eval_annot_args ge (fun v => v) sp m (convert_annot_args al vl1) vl -> + exists vl', + Events.eval_annot_args ge (fun r => rs#r) sp m (convert_annot_args al rl) vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction al; simpl; intros until vl; intros LD EV. +- inv EV. exists (@nil val); split; constructor. +- destruct (convert_annot_arg a vl1) as [a1' vl2] eqn:CV1; simpl in *. + inv EV. + exploit transl_eval_annot_arg. eauto. instantiate (2 := a). rewrite CV1; simpl; eauto. + rewrite CV1; simpl. intros (v1' & A1 & B1 & C1). + exploit IHal. eexact C1. eauto. intros (vl' & A2 & B2). + destruct (convert_annot_arg a rl) as [a1'' rl2]; simpl in *. + exists (v1' :: vl'); split; constructor; auto. +Qed. + + +(* +Definition transl_annot_arg_prop (a: annot_arg expr) (v: val): Prop := + forall tm cs f map pr ns nd a' rs + (MWF: map_wf map) + (TR: tr_annot_arg f.(fn_code) map pr a ns nd a') + (ME: match_env map e nil rs) + (EXT: Mem.extends m tm), + exists rs', exists tm', exists v', + star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm') + /\ match_env map e nil rs' + /\ Events.eval_annot_arg tge (fun r => rs'#r) sp tm' a' v' + /\ Val.lessdef v v' + /\ (forall r, In r pr -> rs'#r = rs#r) + /\ Mem.extends m tm'. + +Theorem transl_annot_arg_correct: + forall a v, + eval_annot_arg ge sp e m a v -> + transl_annot_arg_prop a v. +Proof. + induction 1; red; intros; inv TR. +- exploit transl_expr_correct; eauto. intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exists rs1, tm1, rs1#r; intuition eauto. constructor. +- exists rs, tm, (Vint n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vlong n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vfloat n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vsingle n); intuition auto using star_refl with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). + exists rs, tm, v'; intuition auto using star_refl with aarg. +- exists rs, tm, (Val.add sp (Vint ofs)); intuition auto using star_refl with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). + replace (Genv.symbol_address ge id ofs) + with (Senv.symbol_address tge id ofs) in P. + exists rs, tm, v'; intuition auto using star_refl with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. +- exists rs, tm, (Senv.symbol_address tge id ofs); intuition auto using star_refl with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. +- inv H5. inv H9. simpl in H5. + exploit transl_expr_correct. eexact H. eauto. eauto. eauto. eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit transl_expr_correct. eexact H0. eauto. eauto. eauto. eauto. + intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2). + exists rs2, tm2, (Val.longofwords rs2#r rs2#r0); intuition auto. + eapply star_trans; eauto. + constructor. constructor. constructor. + rewrite (D2 r) by auto with coqlib. apply Val.longofwords_lessdef; auto. + transitivity rs1#r1; auto with coqlib. +Qed. + + +Definition transl_annot_args_prop (l: list (annot_arg expr)) (vl: list val): Prop := + forall tm cs f map pr ns nd l' rs + (MWF: map_wf map) + (TR: tr_annot_args f.(fn_code) map pr l ns nd l') + (ME: match_env map e nil rs) + (EXT: Mem.extends m tm), + exists rs', exists tm', exists vl', + star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm') + /\ match_env map e nil rs' + /\ eval_annot_args tge (fun r => rs'#r) sp tm' l' vl' + /\ Val.lessdef_list vl vl' + /\ (forall r, In r pr -> rs'#r = rs#r) + /\ Mem.extends m tm'. + +Theorem transl_annot_args_correct: + forall l vl, + list_forall2 (eval_annot_arg ge sp e m) l vl -> + transl_annot_args_prop l vl. +Proof. + induction 1; red; intros. +- inv TR. exists rs, tm, (@nil val). + split. constructor. + split. auto. + split. constructor. + split. constructor. + split. auto. + auto. +- inv TR. inv H; inv H5. + + exploit transl_expr_correct; eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit (IHlist_forall2 tm1 cs); eauto. + intros (rs2 & tm2 & vl2 & A2 & B2 & C2 & D2 & E2 & F2). simpl in E2. + exists rs2, tm2, (rs2#r :: vl2); intuition auto. + eapply star_trans; eauto. + constructor; auto. constructor. + rewrite E2; auto. + transitivity rs1#r0; auto. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vint n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vlong n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vfloat n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vsingle n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exploit Mem.loadv_extends; eauto. intros (v1' & P & Q). + exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; eauto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Val.add sp (Vint ofs) :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exploit Mem.loadv_extends; eauto. intros (v1' & P & Q). + replace (Genv.symbol_address ge id ofs) + with (Senv.symbol_address tge id ofs) in P. + exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; auto with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Genv.symbol_address tge id ofs :: vl'); simpl; intuition auto. + constructor; auto with aarg. constructor. + unfold Genv.symbol_address. rewrite symbols_preserved; auto. + + inv H7. inv H12. + exploit transl_expr_correct. eexact H1. eauto. eauto. eauto. eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit transl_expr_correct. eexact H2. eauto. eauto. eauto. eexact E1. + intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2). simpl in D2. + exploit (IHlist_forall2 tm2 cs); eauto. + intros (rs3 & tm3 & vl3 & A3 & B3 & C3 & D3 & E3 & F3). simpl in E3. + exists rs3, tm3, (Val.longofwords rs3#r rs3#r0 :: vl3); intuition auto. + eapply star_trans; eauto. eapply star_trans; eauto. auto. + constructor; auto with aarg. constructor. constructor. constructor. + constructor; auto. apply Val.longofwords_lessdef. + rewrite E3, D2; auto. + rewrite E3; auto. + transitivity rs1#r1; auto. transitivity rs2#r1; auto. +Qed. +*) + End CORRECTNESS_EXPR. (** ** Measure over CminorSel states *) @@ -1304,6 +1532,25 @@ Proof. econstructor; eauto. constructor. eapply match_env_update_dest; eauto. + (* annot *) + inv TS. exploit invert_eval_annot_args; eauto. intros (vparams & P & Q). + exploit transl_exprlist_correct; eauto. + intros [rs' [tm' [E [F [G [J K]]]]]]. + exploit transl_eval_annot_args; eauto. + intros (vargs' & U & V). + exploit (@eval_annot_args_lessdef _ ge (fun r => rs'#r) (fun r => rs'#r)); eauto. + intros (vargs'' & X & Y). + assert (Z: Val.lessdef_list vl vargs'') by (eapply Val.lessdef_list_trans; eauto). + edestruct external_call_mem_extends as [tv [tm'' [A [B [C D]]]]]; eauto. + econstructor; split. + left. eapply plus_right. eexact E. + eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved. eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + traceEq. + econstructor; eauto. constructor. + (* seq *) inv TS. econstructor; split. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 32f35bb4..1ca9faa0 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -220,6 +220,13 @@ Proof. intros; red; intros. elim H1; intro. subst r1; auto. auto. Qed. +Lemma regs_valid_app: + forall rl1 rl2 s, + regs_valid rl1 s -> regs_valid rl2 s -> regs_valid (rl1 ++ rl2) s. +Proof. + intros; red; intros. apply in_app_iff in H1. destruct H1; auto. +Qed. + Lemma regs_valid_incr: forall s1 s2 rl, state_incr s1 s2 -> regs_valid rl s1 -> regs_valid rl s2. Proof. @@ -847,6 +854,10 @@ Inductive tr_stmt (c: code) (map: mapping): c!n1 = Some (Ibuiltin ef rargs rd nd) -> reg_map_ok map rd optid -> tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret + | tr_Sannot: forall ef al ns nd nexits ngoto nret rret n1 rargs, + tr_exprlist c map nil (exprlist_of_expr_list (params_of_annot_args al)) ns n1 rargs -> + c!n1 = Some (Iannot ef (convert_annot_args al rargs) nd) -> + tr_stmt c map (Sannot ef al) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> @@ -1196,7 +1207,7 @@ Proof. apply tr_exitexpr_incr with s1; auto. eapply IHa; eauto with rtlg. apply add_letvar_valid; eauto with rtlg. Qed. - + Lemma transl_stmt_charact: forall map stmt nd nexits ngoto nret rret s ns s' INCR (TR: transl_stmt map stmt nd nexits ngoto nret rret s = OK ns s' INCR) @@ -1250,6 +1261,9 @@ Proof. econstructor; eauto 4 with rtlg. eapply transl_exprlist_charact; eauto 3 with rtlg. eapply alloc_optreg_map_ok with (s1 := s0); eauto with rtlg. + (* Sannot *) + econstructor; eauto 4 with rtlg. + eapply transl_exprlist_charact; eauto 3 with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 5042c775..8961fc0b 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -65,6 +65,20 @@ Variable env: regenv. Definition valid_successor (s: node) : Prop := exists i, funct.(fn_code)!s = Some i. +Definition type_of_annot_arg (a: annot_arg reg) : typ := + match a with + | AA_base r => env r + | AA_int _ => Tint + | AA_long _ => Tlong + | AA_float _ => Tfloat + | AA_single _ => Tsingle + | AA_loadstack chunk ofs => type_of_chunk chunk + | AA_addrstack ofs => Tint + | AA_loadglobal chunk id ofs => type_of_chunk chunk + | AA_addrglobal id ofs => Tint + | AA_longofwords hi lo => Tlong + end. + Inductive wt_instr : instruction -> Prop := | wt_Inop: forall s, @@ -114,6 +128,11 @@ Inductive wt_instr : instruction -> Prop := env res = proj_sig_res (ef_sig ef) -> valid_successor s -> wt_instr (Ibuiltin ef args res s) + | wt_Iannot: + forall ef args s, + map type_of_annot_arg args = (ef_sig ef).(sig_args) -> + valid_successor s -> + wt_instr (Iannot ef args s) | wt_Icond: forall cond args s1 s2, map env args = type_of_condition cond -> @@ -211,6 +230,32 @@ Definition type_ros (e: S.typenv) (ros: reg + ident) : res S.typenv := Definition is_move (op: operation) : bool := match op with Omove => true | _ => false end. +Definition type_expect (e: S.typenv) (t1 t2: typ) : res S.typenv := + if typ_eq t1 t2 then OK e else Error(msg "unexpected type"). + +Definition type_annot_arg (e: S.typenv) (a: annot_arg reg) (ty: typ) : res S.typenv := + match a with + | AA_base r => S.set e r ty + | AA_int _ => type_expect e ty Tint + | AA_long _ => type_expect e ty Tlong + | AA_float _ => type_expect e ty Tfloat + | AA_single _ => type_expect e ty Tsingle + | AA_loadstack chunk ofs => type_expect e ty (type_of_chunk chunk) + | AA_addrstack ofs => type_expect e ty Tint + | AA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk) + | AA_addrglobal id ofs => type_expect e ty Tint + | AA_longofwords hi lo => type_expect e ty Tlong + end. + +Fixpoint type_annot_args (e: S.typenv) (al: list (annot_arg reg)) (tyl: list typ) : res S.typenv := + match al, tyl with + | nil, nil => OK e + | a1 :: al, ty1 :: tyl => + do e1 <- type_annot_arg e a1 ty1; type_annot_args e1 al tyl + | _, _ => + Error (msg "annotation arity mismatch") + end. + Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := match i with | Inop s => @@ -251,6 +296,9 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := do x <- check_successor s; do e1 <- S.set_list e args sig.(sig_args); S.set e1 res (proj_sig_res sig) + | Iannot ef args s => + do x <- check_successor s; + type_annot_args e args (sig_args (ef_sig ef)) | Icond cond args s1 s2 => do x1 <- check_successor s1; do x2 <- check_successor s2; @@ -332,6 +380,55 @@ Proof. monadInv H. destruct H0. subst a; eauto with ty. eauto. Qed. +Remark type_expect_incr: + forall e ty1 ty2 e' te, type_expect e ty1 ty2 = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + unfold type_expect; intros. destruct (typ_eq ty1 ty2); inv H. auto. +Qed. + +Hint Resolve type_expect_incr: ty. + +Lemma type_expect_sound: + forall e ty1 ty2 e', type_expect e ty1 ty2 = OK e' -> ty1 = ty2. +Proof. + unfold type_expect; intros. destruct (typ_eq ty1 ty2); inv H. auto. +Qed. + +Lemma type_annot_arg_incr: + forall e a ty e' te, type_annot_arg e a ty = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + unfold type_annot_arg; intros; destruct a; eauto with ty. +Qed. + +Lemma type_annot_args_incr: + forall a ty e e' te, type_annot_args e a ty = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + induction a; destruct ty; simpl; intros; try discriminate. + inv H; auto. + monadInv H. eapply type_annot_arg_incr; eauto. +Qed. + +Hint Resolve type_annot_args_incr: ty. + +Lemma type_annot_arg_sound: + forall e a ty e' te, + type_annot_arg e a ty = OK e' -> S.satisf te e' -> type_of_annot_arg te a = ty. +Proof. + intros. destruct a; simpl in *; try (symmetry; eapply type_expect_sound; eassumption). + eapply S.set_sound; eauto. +Qed. + +Lemma type_annot_args_sound: + forall al tyl e e' te, + type_annot_args e al tyl = OK e' -> S.satisf te e' -> List.map (type_of_annot_arg te) al = tyl. +Proof. + induction al as [|a al]; destruct tyl as [|ty tyl]; simpl; intros; try discriminate. +- auto. +- monadInv H. f_equal. + eapply type_annot_arg_sound; eauto with ty. + eauto. +Qed. + Lemma type_instr_incr: forall e i e' te, type_instr e i = OK e' -> S.satisf te e' -> S.satisf te e. @@ -403,6 +500,10 @@ Proof. eapply S.set_list_sound; eauto with ty. eapply S.set_sound; eauto with ty. eauto with ty. +- (* annot *) + constructor. + eapply type_annot_args_sound; eauto. + eauto with ty. - (* cond *) constructor. eapply S.set_list_sound; eauto with ty. @@ -483,6 +584,33 @@ Proof. destruct H as [i EQ]; rewrite EQ; auto. Qed. +Lemma type_expect_complete: + forall e ty, type_expect e ty ty = OK e. +Proof. + unfold type_expect; intros. rewrite dec_eq_true; auto. +Qed. + +Lemma type_annot_arg_complete: + forall te a e, + S.satisf te e -> + exists e', type_annot_arg e a (type_of_annot_arg te a) = OK e' /\ S.satisf te e'. +Proof. + intros. destruct a; simpl; try (exists e; split; [apply type_expect_complete|assumption]). + apply S.set_complete; auto. +Qed. + +Lemma type_annot_args_complete: + forall te al e, + S.satisf te e -> + exists e', type_annot_args e al (List.map (type_of_annot_arg te) al) = OK e' /\ S.satisf te e'. +Proof. + induction al; simpl; intros. +- exists e; auto. +- destruct (type_annot_arg_complete te a e) as (e1 & A & B); auto. + destruct (IHal e1) as (e2 & C & D); auto. + exists e2; split; auto. rewrite A. auto. +Qed. + Lemma type_instr_complete: forall te e i, S.satisf te e -> @@ -539,6 +667,10 @@ Proof. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; auto. +- (* annot *) + exploit type_annot_args_complete; eauto. intros [e1 [A B]]. + exists e1; split; auto. rewrite check_successor_complete by auto. + simpl; rewrite <- H0; eauto. - (* cond *) exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. exists e1; split; auto. @@ -782,6 +914,8 @@ Proof. inv WTI. rewrite <- H7. apply wt_regset_list. auto. (* Ibuiltin *) econstructor; eauto. eapply wt_exec_Ibuiltin; eauto. + (* Iannot *) + econstructor; eauto. (* Icond *) econstructor; eauto. (* Ijumptable *) diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 687cbbd3..3a7f5d99 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -114,6 +114,24 @@ let xparmove srcs dsts k = | [src], [dst] -> move src dst k | _, _ -> Xparmove(srcs, dsts, new_temp Tint, new_temp Tfloat) :: k +let rec convert_annot_arg tyenv = function + | AA_base r -> + begin match tyenv r with + | Tlong -> AA_longofwords(AA_base(V(r, Tint)), + AA_base(V(twin_reg r, Tint))) + | ty -> AA_base(V(r, ty)) + end + | AA_int n -> AA_int n + | AA_long n -> AA_long n + | AA_float n -> AA_float n + | AA_single n -> AA_single n + | AA_loadstack(chunk, ofs) -> AA_loadstack(chunk, ofs) + | AA_addrstack(ofs) -> AA_addrstack(ofs) + | AA_loadglobal(chunk, id, ofs) -> AA_loadglobal(chunk, id, ofs) + | AA_addrglobal(id, ofs) -> AA_addrglobal(id, ofs) + | AA_longofwords(hi, lo) -> + AA_longofwords(convert_annot_arg tyenv hi, convert_annot_arg tyenv lo) + (* Return the XTL basic block corresponding to the given RTL instruction. Move and parallel move instructions are introduced to honor calling conventions and register constraints on some operations. @@ -192,6 +210,8 @@ let block_of_RTL_instr funsig tyenv = function let args2 = constrain_regs args1 cargs and res2 = constrain_regs res1 cres in movelist args1 args2 (Xbuiltin(ef, args2, res2) :: movelist res2 res1 [Xbranch s]) + | RTL.Iannot(ef, args, s) -> + [Xannot(ef, List.map (convert_annot_arg tyenv) args); Xbranch s] | RTL.Icond(cond, args, s1, s2) -> [Xcond(cond, vregs tyenv args, s1, s2)] | RTL.Ijumptable(arg, tbl) -> @@ -231,6 +251,11 @@ let vset_removelist vl after = List.fold_right VSet.remove vl after let vset_addlist vl after = List.fold_right VSet.add vl after let vset_addros vos after = match vos with Coq_inl v -> VSet.add v after | Coq_inr id -> after +let rec vset_addannot a after = + match a with + | AA_base v -> VSet.add v after + | AA_longofwords(hi, lo) -> vset_addannot hi (vset_addannot lo after) + | _ -> after let live_before instr after = match instr with @@ -256,6 +281,8 @@ let live_before instr after = vset_addlist args (vset_addros ros VSet.empty) | Xbuiltin(ef, args, res) -> vset_addlist args (vset_removelist res after) + | Xannot(ef, args) -> + List.fold_right vset_addannot args after | Xbranch s -> after | Xcond(cond, args, s1, s2) -> @@ -431,16 +458,14 @@ let spill_costs f = | EF_vstore _ | EF_vstore_global _ | EF_memcpy _ -> (* result is not used but should not be spilled *) charge_list 10 1 args; charge_list max_int 0 res - | EF_annot _ -> - (* arguments are not actually used, so don't charge; - result is never used but should not be spilled *) - charge_list max_int 0 res | EF_annot_val _ -> (* like a move *) charge_list 1 1 args; charge_list 1 1 res | _ -> charge_list 10 1 args; charge_list 10 1 res end + | Xannot(ef, args) -> + () | Xbranch _ -> () | Xcond(cond, args, _, _) -> charge_list 10 1 args @@ -556,6 +581,8 @@ let add_interfs_instr g instr live = | EF_annot_val _, [arg], [res] -> IRC.add_pref g arg res (* like a move *) | _ -> () end + | Xannot(ef, args) -> + () | Xbranch s -> () | Xcond(cond, args, s1, s2) -> @@ -631,10 +658,9 @@ let tospill_instr alloc instr ts = | Xtailcall(sg, vos, args) -> addros_tospill alloc vos ts | Xbuiltin(ef, args, res) -> - begin match ef with - | EF_annot _ -> ts - | _ -> addlist_tospill alloc args (addlist_tospill alloc res ts) - end + addlist_tospill alloc args (addlist_tospill alloc res ts) + | Xannot(ef, args) -> + ts | Xbranch s -> ts | Xcond(cond, args, s1, s2) -> @@ -794,14 +820,11 @@ let spill_instr tospill eqs instr = | Xtailcall(sg, Coq_inr id, args) -> ([instr], []) | Xbuiltin(ef, args, res) -> - begin match ef with - | EF_annot _ -> - ([instr], eqs) - | _ -> - let (args', c1, eqs1) = reload_vars tospill eqs args in - let (res', c2, eqs2) = save_vars tospill eqs1 res in - (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2) - end + let (args', c1, eqs1) = reload_vars tospill eqs args in + let (res', c2, eqs2) = save_vars tospill eqs1 res in + (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2) + | Xannot(ef, args) -> + ([instr], eqs) | Xbranch s -> ([instr], eqs) | Xcond(cond, args, s1, s2) -> @@ -940,12 +963,9 @@ let transl_instr alloc instr k = | Xtailcall(sg, vos, args) -> LTL.Ltailcall(sg, mros_of alloc vos) :: [] | Xbuiltin(ef, args, res) -> - begin match ef with - | EF_annot _ -> - LTL.Lannot(ef, List.map alloc args) :: k - | _ -> - LTL.Lbuiltin(ef, mregs_of alloc args, mregs_of alloc res) :: k - end + LTL.Lbuiltin(ef, mregs_of alloc args, mregs_of alloc res) :: k + | Xannot(ef, args) -> + LTL.Lannot(ef, List.map (AST.map_annot_arg alloc) args) :: k | Xbranch s -> LTL.Lbranch s :: [] | Xcond(cond, args, s1, s2) -> diff --git a/backend/Renumber.v b/backend/Renumber.v index 0a2c2f12..634fe56a 100644 --- a/backend/Renumber.v +++ b/backend/Renumber.v @@ -48,6 +48,7 @@ Definition renum_instr (i: instruction) : instruction := | Icall sg ros args res s => Icall sg ros args res (renum_pc s) | Itailcall sg ros args => i | Ibuiltin ef args res s => Ibuiltin ef args res (renum_pc s) + | Iannot ef args s => Iannot ef args (renum_pc s) | Icond cond args s1 s2 => Icond cond args (renum_pc s1) (renum_pc s2) | Ijumptable arg tbl => Ijumptable arg (List.map renum_pc tbl) | Ireturn or => i diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 19c3b680..09faa131 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -201,6 +201,13 @@ Proof. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. eapply reach_succ; eauto. simpl; auto. +(* annot *) + econstructor; split. + eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* cond *) econstructor; split. eapply exec_Icond; eauto. diff --git a/backend/Selection.v b/backend/Selection.v index 11125856..ae9da0a7 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -203,6 +203,23 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := end end. +(** Annotations *) + +Definition builtin_is_annot (ef: external_function) (optid: option ident) : bool := + match ef, optid with + | EF_annot _ _, None => true + | _, _ => false + end. + +Function sel_annot_arg (e: Cminor.expr) : AST.annot_arg expr := + match e with + | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => AA_addrglobal id ofs + | Cminor.Econst (Cminor.Oaddrstack ofs) => AA_addrstack ofs + | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrsymbol id ofs)) => AA_loadglobal chunk id ofs + | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrstack ofs)) => AA_loadstack chunk ofs + | _ => annot_arg (sel_expr e) + end. + (** Conversion of Cminor [switch] statements to decision trees. *) Parameter compile_switch: Z -> nat -> table -> comptree. @@ -263,7 +280,9 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args) end) | Cminor.Sbuiltin optid ef args => - OK (Sbuiltin optid ef (sel_exprlist args)) + OK (if builtin_is_annot ef optid + then Sannot ef (List.map sel_annot_arg args) + else Sbuiltin optid ef (sel_exprlist args)) | Cminor.Stailcall sg fn args => OK (match classify_call ge fn with | Call_imm id => Stailcall sg (inr _ id) (sel_exprlist args) diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 20b6cf93..d7b1e675 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -520,6 +520,14 @@ Proof. auto. Qed. +Lemma set_optvar_lessdef: + forall e1 e2 optid v1 v2, + env_lessdef e1 e2 -> Val.lessdef v1 v2 -> + env_lessdef (set_optvar optid v1 e1) (set_optvar optid v2 e2). +Proof. + unfold set_optvar; intros. destruct optid; auto. apply set_var_lessdef; auto. +Qed. + Lemma set_params_lessdef: forall il vl1 vl2, Val.lessdef_list vl1 vl2 -> @@ -590,6 +598,47 @@ Proof. exists (v1' :: vl'); split; auto. constructor; eauto. Qed. +Lemma sel_annot_arg_correct: + forall sp e e' m m', + env_lessdef e e' -> Mem.extends m m' -> + forall a v, + Cminor.eval_expr ge sp e m a v -> + exists v', + CminorSel.eval_annot_arg tge sp e' m' (sel_annot_arg a) v' + /\ Val.lessdef v v'. +Proof. + intros until v. functional induction (sel_annot_arg a); intros EV. +- inv EV. simpl in H2; inv H2. econstructor; split. constructor. + unfold Genv.symbol_address. rewrite symbols_preserved. auto. +- inv EV. simpl in H2; inv H2. econstructor; split. constructor. auto. +- inv EV. inv H3. exploit Mem.loadv_extends; eauto. intros (v' & A & B). + exists v'; split; auto. constructor. + replace (Genv.symbol_address tge id ofs) with vaddr; auto. + simpl in H2; inv H2. unfold Genv.symbol_address. rewrite symbols_preserved. auto. +- inv EV. inv H3. simpl in H2; inv H2. exploit Mem.loadv_extends; eauto. intros (v' & A & B). + exists v'; split; auto. constructor; auto. +- exploit sel_expr_correct; eauto. intros (v1 & A & B). + exists v1; split; auto. eapply eval_annot_arg; eauto. +Qed. + +Lemma sel_annot_args_correct: + forall sp e e' m m', + env_lessdef e e' -> Mem.extends m m' -> + forall al vl, + Cminor.eval_exprlist ge sp e m al vl -> + exists vl', + list_forall2 (CminorSel.eval_annot_arg tge sp e' m') + (List.map sel_annot_arg al) + vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction 3; simpl. +- exists (@nil val); split; constructor. +- exploit sel_annot_arg_correct; eauto. intros (v1' & A & B). + destruct IHeval_exprlist as (vl' & C & D). + exists (v1' :: vl'); split; auto. constructor; auto. +Qed. + (** Semantic preservation for functions and statements. *) Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := @@ -675,6 +724,8 @@ Proof. destruct (classify_call ge e); simpl; auto. (* tailcall *) destruct (classify_call ge e); simpl; auto. +(* builtin *) + destruct (builtin_is_annot e); simpl; auto. (* seq *) exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; @@ -776,14 +827,32 @@ Proof. econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. constructor; auto. apply call_cont_commut; auto. - (* Sbuiltin *) + destruct (builtin_is_annot ef optid) eqn:ISANNOT. ++ (* annotation *) + assert (X: exists text targs, ef = EF_annot text targs). + { destruct ef; try discriminate. econstructor; econstructor; eauto. } + destruct X as (text & targs & EQ). + assert (Y: optid = None). + { destruct ef; try discriminate. destruct optid; try discriminate. auto. } + exploit sel_annot_args_correct; eauto. + intros (vargs' & P & Q). + exploit external_call_mem_extends; eauto. + intros [vres' [m2 [A [B [C D]]]]]. + left; econstructor; split. + econstructor. + rewrite EQ; auto. + eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + rewrite Y. constructor; auto. ++ (* other builtin *) exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - constructor; auto. - destruct optid; simpl; auto. apply set_var_lessdef; auto. + constructor; auto. apply set_optvar_lessdef; auto. - (* Seq *) left; econstructor; split. constructor. constructor; auto. constructor; auto. diff --git a/backend/Splitting.ml b/backend/Splitting.ml index 3530ba99..53600c98 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -163,6 +163,8 @@ let ren_instr f maps pc i = Itailcall(sg, ren_ros before ros, ren_regs before args) | Ibuiltin(ef, args, res, s) -> Ibuiltin(ef, ren_regs before args, ren_reg after res, s) + | Iannot(ef, args, s) -> + Iannot(ef, List.map (AST.map_annot_arg (ren_reg before)) args, s) | Icond(cond, args, s1, s2) -> Icond(cond, ren_regs before args, s1, s2) | Ijumptable(arg, tbl) -> diff --git a/backend/Stacking.v b/backend/Stacking.v index 4ee43bb1..c17dc038 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -130,14 +130,26 @@ Definition transl_addr (fe: frame_env) (addr: addressing) := (** 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 *) +Fixpoint transl_annot_arg (fe: frame_env) (a: annot_arg loc) : annot_arg mreg := + match a with + | AA_base (R r) => AA_base r + | AA_base (S Local ofs ty) => + AA_loadstack (chunk_of_type ty) (Int.repr (offset_of_index fe (FI_local ofs ty))) + | AA_base (S _ _ __) => AA_int Int.zero (**r never happens *) + | AA_int n => AA_int n + | AA_long n => AA_long n + | AA_float n => AA_float n + | AA_single n => AA_single n + | AA_loadstack chunk ofs => + AA_loadstack chunk (Int.add ofs (Int.repr fe.(fe_stack_data))) + | AA_addrstack ofs => + AA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data))) + | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs + | AA_addrglobal id ofs => AA_addrglobal id ofs + | AA_longofwords hi lo => + AA_longofwords (transl_annot_arg fe hi) (transl_annot_arg fe lo) 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 @@ -182,7 +194,7 @@ Definition transl_instr | Lbuiltin ef args dst => Mbuiltin ef args dst :: k | Lannot ef args => - Mannot ef (map (transl_annot_param fe) args) :: k + Mannot ef (map (transl_annot_arg fe) args) :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index e3e3a0d0..f4a1935f 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -2382,6 +2382,8 @@ Section ANNOT_ARGUMENTS. Variable f: Linear.function. Let b := function_bounds f. Let fe := make_env b. +Variable tf: Mach.function. +Hypothesis TRANSF_F: transf_function f = OK tf. Variable j: meminj. Variables m m': mem. Variables ls ls0: locset. @@ -2390,39 +2392,67 @@ 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_valid f l = true -> - match l with S sl ofs ty => slot_within_bounds b sl ofs ty | _ => 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; simpl in H. -(* reg *) - exists (rs r); split. constructor. auto. -(* stack *) - destruct sl; try discriminate. - 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, - forallb (loc_valid f) ll = true -> - (forall sl ofs ty, In (S sl ofs ty) ll -> slot_within_bounds b sl ofs ty) -> - 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; simpl; intros. - exists (@nil val); split; constructor. - InvBooleans. - exploit (transl_annot_param_correct a). auto. destruct a; auto. - intros [v1 [A B]]. - exploit IHll. auto. auto. - intros [vl [C D]]. - exists (v1 :: vl); split; constructor; auto. +Hypothesis MINJ: Mem.inject j m m'. +Hypothesis GINJ: meminj_preserves_globals ge j. + +Lemma transl_annot_arg_correct: + forall a v, + eval_annot_arg ge ls (Vptr sp Int.zero) m a v -> + (forall l, In l (params_of_annot_arg a) -> loc_valid f l = true) -> + (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_arg a) -> slot_within_bounds b sl ofs ty) -> + exists v', + eval_annot_arg ge rs (Vptr sp' Int.zero) m' (transl_annot_arg fe a) v' + /\ val_inject j v v'. +Proof. +Local Opaque fe offset_of_index. + induction 1; simpl; intros VALID BOUNDS. +- assert (loc_valid f x = true) by auto. + destruct x as [r | [] ofs ty]; try discriminate. + + exists (rs r); auto with aarg. + + exploit agree_locals; eauto. intros [v [A B]]. inv A. + exists v; split; auto. constructor. simpl. rewrite Int.add_zero_l. +Local Transparent fe. + unfold fe, b. erewrite offset_of_index_no_overflow by eauto. exact H1. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- simpl in H. exploit Mem.load_inject; eauto. eapply agree_inj; eauto. + intros (v' & A & B). exists v'; split; auto. constructor. + unfold Mem.loadv, Val.add. rewrite <- Int.add_assoc. + unfold fe, b; erewrite shifted_stack_offset_no_overflow; eauto. + eapply agree_bounds; eauto. eapply Mem.valid_access_perm. eapply Mem.load_valid_access; eauto. +- econstructor; split; eauto with aarg. + unfold Val.add. rewrite ! Int.add_zero_l. econstructor. eapply agree_inj; eauto. auto. +- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). + { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) eqn:FS; auto. + econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. } + exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with aarg. +- econstructor; split; eauto with aarg. + unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) eqn:FS; auto. + econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. +- destruct IHeval_annot_arg1 as (v1 & A1 & B1); auto using in_or_app. + destruct IHeval_annot_arg2 as (v2 & A2 & B2); auto using in_or_app. + exists (Val.longofwords v1 v2); split; auto with aarg. + apply val_longofwords_inject; auto. +Qed. + +Lemma transl_annot_args_correct: + forall al vl, + eval_annot_args ge ls (Vptr sp Int.zero) m al vl -> + (forall l, In l (params_of_annot_args al) -> loc_valid f l = true) -> + (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args al) -> slot_within_bounds b sl ofs ty) -> + exists vl', + eval_annot_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_annot_arg fe) al) vl' + /\ val_list_inject j vl vl'. +Proof. + induction 1; simpl; intros VALID BOUNDS. +- exists (@nil val); split; constructor. +- exploit transl_annot_arg_correct; eauto using in_or_app. intros (v1' & A & B). + exploit IHlist_forall2; eauto using in_or_app. intros (vl' & C & D). + exists (v1'::vl'); split; constructor; auto. Qed. End ANNOT_ARGUMENTS. @@ -2705,25 +2735,28 @@ Proof. eapply agree_valid_mach; eauto. - (* Lannot *) - exploit transl_annot_params_correct; eauto. eapply wt_state_annot; eauto. + exploit transl_annot_args_correct; eauto. + eapply match_stacks_preserves_globals; eauto. + rewrite <- forallb_forall. eapply wt_state_annot; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_inject'; eauto. + 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. + apply plus_one. econstructor; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. - inv H; inv A. eapply match_stack_change_extcall; eauto. + eapply match_stack_change_extcall; eauto. apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. apply Plt_Ple. 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. - intros. inv H; eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. - eapply external_call_valid_block'; eauto. + eapply external_call_valid_block; eauto. + intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. + eapply external_call_valid_block; eauto. eapply agree_valid_mach; eauto. - (* Llabel *) diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 5ee7ccc1..bd9b227f 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -513,6 +513,19 @@ Proof. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply regset_set; auto. +(* annot *) + TransfInstr. + exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. + intros (vargs' & P & Q). + exploit external_call_mem_extends; eauto. + intros [v' [m'1 [A [B [C D]]]]]. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'1); split. + eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + econstructor; eauto. + (* cond *) TransfInstr. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index e6588938..52318ede 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -344,8 +344,9 @@ Proof. econstructor; eauto. (* Lannot *) left; simpl; econstructor; split. - eapply exec_Lannot; eauto. - eapply external_call_symbols_preserved'; eauto. + eapply exec_Lannot; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 55a093a4..400c19d9 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -60,6 +60,7 @@ Definition ref_instruction (i: instruction) : list ident := | Itailcall _ (inl r) _ => nil | Itailcall _ (inr id) _ => id :: nil | Ibuiltin ef _ _ _ => globals_external ef + | Iannot _ args _ => globals_of_annot_args args | Icond cond _ _ _ => nil | Ijumptable _ _ => nil | Ireturn _ => nil diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index fbf43866..90d7f270 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -741,6 +741,64 @@ Proof. auto. Qed. +Lemma eval_annot_arg_inject: + forall rs sp m j rs' sp' m' a v, + eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v -> + j sp = Some(sp', 0) -> + meminj_preserves_globals j -> + regset_inject j rs rs' -> + Mem.inject j m m' -> + (forall id, In id (globals_of_annot_arg a) -> kept id) -> + exists v', + eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' a v' + /\ val_inject j v v'. +Proof. + induction 1; intros SP GL RS MI K; simpl in K. +- exists rs'#x; split; auto. constructor. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. + intros (v' & A & B). exists v'; auto with aarg. +- econstructor; split; eauto with aarg. simpl. econstructor; eauto. rewrite Int.add_zero; auto. +- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). + { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. + econstructor; eauto. rewrite Int.add_zero; auto. } + exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with aarg. +- econstructor; split; eauto with aarg. + unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. + econstructor; eauto. rewrite Int.add_zero; auto. +- destruct IHeval_annot_arg1 as (v1' & A1 & B1); eauto using in_or_app. + destruct IHeval_annot_arg2 as (v2' & A2 & B2); eauto using in_or_app. + exists (Val.longofwords v1' v2'); split; auto with aarg. + apply val_longofwords_inject; auto. +Qed. + +Lemma eval_annot_args_inject: + forall rs sp m j rs' sp' m' al vl, + eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl -> + j sp = Some(sp', 0) -> + meminj_preserves_globals j -> + regset_inject j rs rs' -> + Mem.inject j m m' -> + (forall id, In id (globals_of_annot_args al) -> kept id) -> + exists vl', + eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl' + /\ val_list_inject j vl vl'. +Proof. + induction 1; intros. +- exists (@nil val); split; constructor. +- simpl in H5. + exploit eval_annot_arg_inject; eauto using in_or_app. intros (v1' & A & B). + destruct IHlist_forall2 as (vl' & C & D); eauto using in_or_app. + exists (v1' :: vl'); split; constructor; auto. +Qed. + Theorem step_simulation: forall S1 t S2, step ge S1 t S2 -> forall S1' (MS: match_states S1 S1'), @@ -845,6 +903,25 @@ Proof. unfold Mem.valid_block in *; xomega. apply set_reg_inject; auto. apply regset_inject_incr with j; auto. +- (* annot *) + exploit eval_annot_args_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + intros. apply KEPT. red. econstructor; econstructor; eauto. + intros (vargs' & P & Q). + exploit external_call_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + destruct ef; contradiction. + intros (j' & tv & tm' & A & B & C & D & E & F & G). + econstructor; split. + eapply exec_Iannot; eauto. + eapply match_states_regular with (j := j'); eauto. + apply match_stacks_incr with j; auto. + intros. exploit G; eauto. intros [U V]. + assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto). + assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto). + unfold Mem.valid_block in *; xomega. + apply regset_inject_incr with j; auto. + - (* cond *) assert (C: eval_condition cond trs##args tm = Some b). { eapply eval_condition_inject; eauto. apply regs_inject; auto. } diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 4249a8da..8720ce50 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -55,7 +55,6 @@ Inductive builtin_kind : Type := | Builtin_vload (chunk: memory_chunk) (aaddr: aval) | Builtin_vstore (chunk: memory_chunk) (aaddr av: aval) | Builtin_memcpy (sz al: Z) (adst asrc: aval) - | Builtin_annot | Builtin_annot_val (av: aval) | Builtin_default. @@ -66,7 +65,6 @@ Definition classify_builtin (ef: external_function) (args: list reg) (ae: aenv) | EF_vstore chunk, a1::a2::nil => Builtin_vstore chunk (areg ae a1) (areg ae a2) | EF_vstore_global chunk id ofs, a1::nil => Builtin_vstore chunk (Ptr (Gl id ofs)) (areg ae a1) | EF_memcpy sz al, a1::a2::nil => Builtin_memcpy sz al (areg ae a1) (areg ae a2) - | EF_annot _ _, _ => Builtin_annot | EF_annot_val _ _, a1::nil => Builtin_annot_val (areg ae a1) | _, _ => Builtin_default end. @@ -86,8 +84,6 @@ Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_func let p := loadbytes am rm (aptr_of_aval asrc) in let am' := storebytes am (aptr_of_aval adst) sz p in VA.State (AE.set res itop ae) am' - | Builtin_annot => - VA.State (AE.set res itop ae) am | Builtin_annot_val av => VA.State (AE.set res av ae) am | Builtin_default => @@ -115,6 +111,8 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) : VA.Bot | Some(Ibuiltin ef args res s) => transfer_builtin ae am rm ef args res + | Some(Iannot ef args s) => + VA.State ae am | Some(Icond cond args s1 s2) => VA.State ae am | Some(Ijumptable arg tbl) => @@ -306,7 +304,6 @@ Lemma classify_builtin_sound: exists dst, exists src, extcall_memcpy_sem sz al ge (dst::src::nil) m t res m' /\ vmatch bc dst adst /\ vmatch bc src asrc - | Builtin_annot => m' = m /\ res = Vundef | Builtin_annot_val av => m' = m /\ vmatch bc res av | Builtin_default => True end. @@ -329,8 +326,6 @@ Proof. - (* memcpy *) destruct args; auto. destruct args; auto. destruct args; auto. exists (e#p), (e#p0); eauto. -- (* annot *) - simpl in H1. inv H1. auto. - (* annot val *) destruct args; auto. destruct args; auto. simpl in H1. inv H1. eauto. @@ -1303,10 +1298,6 @@ Proof. intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. eapply romatch_storebytes; eauto. eapply sound_stack_storebytes; eauto. -+ (* annot *) - intros (A & B); subst. - eapply sound_succ_state; eauto. simpl; auto. - apply ematch_update; auto. constructor. + (* annot val *) intros (A & B); subst. eapply sound_succ_state; eauto. simpl; auto. @@ -1359,6 +1350,11 @@ Proof. rewrite C; auto. exact AA. +- (* annot *) + destruct ef; try contradiction. inv H2. + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H; eauto. + - (* cond *) eapply sound_succ_state; eauto. simpl. destruct b; auto. diff --git a/backend/XTL.ml b/backend/XTL.ml index 9cb8e0a1..0e5ce0c4 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -35,6 +35,7 @@ type instruction = | Xcall of signature * (var, ident) sum * var list * var list | Xtailcall of signature * (var, ident) sum * var list | Xbuiltin of external_function * var list * var list + | Xannot of external_function * var annot_arg list | Xbranch of node | Xcond of condition * var list * node * node | Xjumptable of var * node list @@ -124,6 +125,12 @@ let rec set_vars_type vl tyl = let unify_var_type v1 v2 = if typeof v1 <> typeof v2 then raise Type_error +let rec type_annot_arg a ty = + match a with + | AA_base v -> set_var_type v ty + | AA_longofwords(a1, a2) -> type_annot_arg a1 Tint; type_annot_arg a2 Tint + | _ -> () + let type_instr = function | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) -> unify_var_type src dst @@ -153,6 +160,11 @@ let type_instr = function let sg = ef_sig ef in set_vars_type args sg.sig_args; set_vars_type res (Events.proj_sig_res' sg) + | Xannot(ef, args) -> + let sg = ef_sig ef in + if List.length args = List.length sg.sig_args + then List.iter2 type_annot_arg args sg.sig_args + else raise Type_error | Xbranch s -> () | Xcond(cond, args, s1, s2) -> diff --git a/backend/XTL.mli b/backend/XTL.mli index 75a3d657..9794565c 100644 --- a/backend/XTL.mli +++ b/backend/XTL.mli @@ -36,6 +36,7 @@ type instruction = | Xcall of signature * (var, ident) sum * var list * var list | Xtailcall of signature * (var, ident) sum * var list | Xbuiltin of external_function * var list * var list + | Xannot of external_function * var annot_arg list | Xbranch of node | Xcond of condition * var list * node * node | Xjumptable of var * node list diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4cb4ded6..fd10efb4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -737,8 +737,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(intern_string txt, - List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)), + EF_annot(intern_string txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 52e9eaac..7c00ab47 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -513,10 +513,10 @@ Definition do_ef_memcpy (sz al: Z) | _ => None end. -Definition do_ef_annot (text: ident) (targs: list annot_arg) +Definition do_ef_annot (text: ident) (targs: list typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - do args <- list_eventval_of_val vargs (annot_args_typ targs); - Some(w, Event_annot text (annot_eventvals targs args) :: E0, Vundef, m). + do args <- list_eventval_of_val vargs targs; + Some(w, Event_annot text args :: E0, Vundef, m). Definition do_ef_annot_val (text: ident) (targ: typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := diff --git a/common/AST.v b/common/AST.v index 9c29a374..d2926178 100644 --- a/common/AST.v +++ b/common/AST.v @@ -576,7 +576,7 @@ Inductive external_function : Type := 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 annot_arg) + | 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. *) @@ -584,27 +584,15 @@ Inductive external_function : Type := (** 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. *) - | EF_inline_asm (text: ident) + | EF_inline_asm (text: ident). (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic preservation theorem. Generated only if [-finline-asm] is given. *) -with annot_arg : Type := - | AA_arg (ty: typ) - | AA_int (n: int) - | AA_float (n: float). - (** The type signature of an external function. *) -Fixpoint annot_args_typ (targs: list annot_arg) : list typ := - match targs with - | nil => nil - | AA_arg ty :: targs' => ty :: annot_args_typ targs' - | _ :: targs' => annot_args_typ targs' - end. - Definition ef_sig (ef: external_function): signature := match ef with | EF_external name sg => sg @@ -616,7 +604,7 @@ Definition ef_sig (ef: external_function): signature := | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default - | EF_annot text targs => mksignature (annot_args_typ targs) None cc_default + | EF_annot text targs => mksignature targs None cc_default | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default | EF_inline_asm text => mksignature nil None cc_default end. @@ -653,7 +641,7 @@ Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} Proof. generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. decide equality. apply Float.eq_dec. + apply list_eq_dec. auto. Defined. Global Opaque external_function_eq. @@ -699,3 +687,56 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := end. End TRANSF_PARTIAL_FUNDEF. + +(** * Arguments to annotations *) + +Set Contextual Implicit. + +Inductive annot_arg (A: Type) : Type := + | AA_base (x: A) + | AA_int (n: int) + | AA_long (n: int64) + | AA_float (f: float) + | AA_single (f: float32) + | AA_loadstack (chunk: memory_chunk) (ofs: int) + | AA_addrstack (ofs: int) + | AA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) + | AA_addrglobal (id: ident) (ofs: int) + | AA_longofwords (hi lo: annot_arg A). + +Fixpoint globals_of_annot_arg (A: Type) (a: annot_arg A) : list ident := + match a with + | AA_loadglobal chunk id ofs => id :: nil + | AA_addrglobal id ofs => id :: nil + | AA_longofwords hi lo => globals_of_annot_arg hi ++ globals_of_annot_arg lo + | _ => nil + end. + +Definition globals_of_annot_args (A: Type) (al: list (annot_arg A)) : list ident := + List.fold_right (fun a l => globals_of_annot_arg a ++ l) nil al. + +Fixpoint params_of_annot_arg (A: Type) (a: annot_arg A) : list A := + match a with + | AA_base x => x :: nil + | AA_longofwords hi lo => params_of_annot_arg hi ++ params_of_annot_arg lo + | _ => nil + end. + +Definition params_of_annot_args (A: Type) (al: list (annot_arg A)) : list A := + List.fold_right (fun a l => params_of_annot_arg a ++ l) nil al. + +Fixpoint map_annot_arg (A B: Type) (f: A -> B) (a: annot_arg A) : annot_arg B := + match a with + | AA_base x => AA_base (f x) + | AA_int n => AA_int n + | AA_long n => AA_long n + | AA_float n => AA_float n + | AA_single n => AA_single n + | AA_loadstack chunk ofs => AA_loadstack chunk ofs + | AA_addrstack ofs => AA_addrstack ofs + | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs + | AA_addrglobal id ofs => AA_addrglobal id ofs + | AA_longofwords hi lo => + AA_longofwords (map_annot_arg f hi) (map_annot_arg f lo) + end. + diff --git a/common/Events.v b/common/Events.v index 3fb58806..15bf4e12 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1344,25 +1344,16 @@ Qed. (** ** Semantics of annotations. *) -Fixpoint annot_eventvals (targs: list annot_arg) (vargs: list eventval) : list eventval := - match targs, vargs with - | AA_arg ty :: targs', varg :: vargs' => varg :: annot_eventvals targs' vargs' - | AA_int n :: targs', _ => EVint n :: annot_eventvals targs' vargs - | AA_float n :: targs', _ => EVfloat n :: annot_eventvals targs' vargs - | _, _ => vargs - end. - -Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (ge: Senv.t): +Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_annot_sem_intro: forall vargs m args, - eventval_list_match ge args (annot_args_typ targs) vargs -> - extcall_annot_sem text targs ge vargs m - (Event_annot text (annot_eventvals targs args) :: E0) Vundef m. + 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 targs, extcall_properties (extcall_annot_sem text targs) - (mksignature (annot_args_typ targs) None cc_default) + (mksignature targs None cc_default) nil. Proof. intros; constructor; intros. @@ -1794,9 +1785,133 @@ Proof. split; congruence. Qed. +(** * Evaluation of annotation arguments *) + +Section EVAL_ANNOT_ARG. + +Variable A: Type. +Variable ge: Senv.t. +Variable e: A -> val. +Variable sp: val. +Variable m: mem. + +Inductive eval_annot_arg: annot_arg A -> val -> Prop := + | eval_AA_base: forall x, + eval_annot_arg (AA_base x) (e x) + | eval_AA_int: forall n, + eval_annot_arg (AA_int n) (Vint n) + | eval_AA_long: forall n, + eval_annot_arg (AA_long n) (Vlong n) + | eval_AA_float: forall n, + eval_annot_arg (AA_float n) (Vfloat n) + | eval_AA_single: forall n, + eval_annot_arg (AA_single n) (Vsingle n) + | eval_AA_loadstack: forall chunk ofs v, + Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v -> + eval_annot_arg (AA_loadstack chunk ofs) v + | eval_AA_addrstack: forall ofs, + eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs)) + | eval_AA_loadglobal: forall chunk id ofs v, + Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v -> + eval_annot_arg (AA_loadglobal chunk id ofs) v + | eval_AA_addrglobal: forall id ofs, + eval_annot_arg (AA_addrglobal id ofs) (Senv.symbol_address ge id ofs) + | eval_AA_longofwords: forall hi lo vhi vlo, + eval_annot_arg hi vhi -> eval_annot_arg lo vlo -> + eval_annot_arg (AA_longofwords hi lo) (Val.longofwords vhi vlo). + +Definition eval_annot_args (al: list (annot_arg A)) (vl: list val) : Prop := + list_forall2 eval_annot_arg al vl. + +Lemma eval_annot_arg_determ: + forall a v, eval_annot_arg a v -> forall v', eval_annot_arg a v' -> v' = v. +Proof. + induction 1; intros v' EV; inv EV; try congruence. + f_equal; eauto. +Qed. + +Lemma eval_annot_args_determ: + forall al vl, eval_annot_args al vl -> forall vl', eval_annot_args al vl' -> vl' = vl. +Proof. + induction 1; intros v' EV; inv EV; f_equal; eauto using eval_annot_arg_determ. +Qed. + +End EVAL_ANNOT_ARG. + +Hint Constructors eval_annot_arg: aarg. + +(** Invariance by change of global environment. *) + +Section EVAL_ANNOT_ARG_PRESERVED. + +Variables A F1 V1 F2 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. +Variable e: A -> val. +Variable sp: val. +Variable m: mem. + +Hypothesis symbols_preserved: + forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. + +Lemma eval_annot_arg_preserved: + forall a v, eval_annot_arg ge1 e sp m a v -> eval_annot_arg ge2 e sp m a v. +Proof. + assert (EQ: forall id ofs, Senv.symbol_address ge2 id ofs = Senv.symbol_address ge1 id ofs). + { unfold Senv.symbol_address; simpl; intros. rewrite symbols_preserved; auto. } + induction 1; eauto with aarg. rewrite <- EQ in H; eauto with aarg. rewrite <- EQ; eauto with aarg. +Qed. +Lemma eval_annot_args_preserved: + forall al vl, eval_annot_args ge1 e sp m al vl -> eval_annot_args ge2 e sp m al vl. +Proof. + induction 1; constructor; auto; eapply eval_annot_arg_preserved; eauto. +Qed. +End EVAL_ANNOT_ARG_PRESERVED. +(** Compatibility with the "is less defined than" relation. *) +Section EVAL_ANNOT_ARG_LESSDEF. +Variable A: Type. +Variable ge: Senv.t. +Variables e1 e2: A -> val. +Variable sp: val. +Variables m1 m2: mem. + +Hypothesis env_lessdef: forall x, Val.lessdef (e1 x) (e2 x). +Hypothesis mem_extends: Mem.extends m1 m2. + +Lemma eval_annot_arg_lessdef: + forall a v1, eval_annot_arg ge e1 sp m1 a v1 -> + exists v2, eval_annot_arg ge e2 sp m2 a v2 /\ Val.lessdef v1 v2. +Proof. + induction 1. +- exists (e2 x); auto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. +- econstructor; eauto with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. +- econstructor; eauto with aarg. +- destruct IHeval_annot_arg1 as (vhi' & P & Q). + destruct IHeval_annot_arg2 as (vlo' & R & S). + econstructor; split; eauto with aarg. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma eval_annot_args_lessdef: + forall al vl1, eval_annot_args ge e1 sp m1 al vl1 -> + exists vl2, eval_annot_args ge e2 sp m2 al vl2 /\ Val.lessdef_list vl1 vl2. +Proof. + induction 1. +- econstructor; split. constructor. auto. +- exploit eval_annot_arg_lessdef; eauto. intros (v1' & P & Q). + destruct IHlist_forall2 as (vl' & U & V). + exists (v1'::vl'); split; constructor; auto. +Qed. + +End EVAL_ANNOT_ARG_LESSDEF. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index c0eab04f..52aa963a 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -54,3 +54,28 @@ let name_of_external = function | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text) + +let rec print_annot_arg px oc = function + | AA_base x -> px oc x + | AA_int n -> fprintf oc "int %ld" (camlint_of_coqint n) + | AA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n) + | AA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n) + | AA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n) + | AA_loadstack(chunk, ofs) -> + fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs) + | AA_addrstack(ofs) -> + fprintf oc "sp + %ld" (camlint_of_coqint ofs) + | AA_loadglobal(chunk, id, ofs) -> + fprintf oc "%s[&%s + %ld]" + (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) + | AA_addrglobal(id, ofs) -> + fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs) + | AA_longofwords(hi, lo) -> + fprintf oc "longofwords(%a, %a)" + (print_annot_arg px) hi (print_annot_arg px) lo + +let rec print_annot_args px oc = function + | [] -> () + | [a] -> print_annot_arg px oc a + | a1 :: al -> + fprintf oc "%a, %a" (print_annot_arg px) a1 (print_annot_args px) al diff --git a/common/Values.v b/common/Values.v index e7dce7e9..12b380b7 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1383,6 +1383,12 @@ Proof. left; congruence. tauto. tauto. Qed. +Lemma lessdef_list_trans: + forall vl1 vl2, lessdef_list vl1 vl2 -> forall vl3, lessdef_list vl2 vl3 -> lessdef_list vl1 vl3. +Proof. + induction 1; intros vl3 LD; inv LD; constructor; eauto using lessdef_trans. +Qed. + (** Compatibility of operations with the [lessdef] relation. *) Lemma load_result_lessdef: @@ -212,11 +212,7 @@ Inductive instruction: Type := | Pallocframe(sz: Z)(ofs_ra ofs_link: int) | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) | Pbuiltin(ef: external_function)(args: list preg)(res: list preg) - | Pannot(ef: external_function)(args: list annot_param) - -with annot_param : Type := - | APreg: preg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Pannot(ef: external_function)(args: list (annot_arg preg)). Definition code := list instruction. Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. @@ -798,20 +794,6 @@ Definition extcall_arguments Definition loc_external_result (sg: signature) : list preg := map 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 := @@ -840,8 +822,8 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) -> - annot_arguments rs m args vargs -> - external_call' ef ge vargs m t v m' -> + eval_annot_args ge rs (rs ESP) m args vargs -> + external_call ef ge vargs m t v m' -> step (State rs m) t (State (nextinstr rs) m') | exec_step_external: @@ -893,16 +875,6 @@ Proof. intros. red in H0; red in H1. eauto. Qed. -Remark annot_arguments_determ: - forall rs m params args1 args2, - annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. -Proof. - unfold annot_arguments. intros. revert params args1 H args2 H0. - induction 1; intros. - inv H0; auto. - inv H1. decEq; eauto. inv H; inv H4. auto. congruence. -Qed. - Lemma semantics_determinate: forall p, determinate (semantics p). Proof. Ltac Equalities := @@ -912,32 +884,32 @@ Ltac Equalities := | _ => idtac end. intros; constructor; simpl; intros. -(* determ *) +- (* determ *) inv H; inv H0; Equalities. - split. constructor. auto. - discriminate. - discriminate. - inv H11. - exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. ++ split. constructor. auto. ++ discriminate. ++ discriminate. ++ inv H11. ++ exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. - inv H12. - assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. - exploit external_call_determ'. eexact H5. eexact H13. intros [A B]. ++ inv H12. ++ assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. - assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. ++ assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. -(* trace length *) +- (* trace length *) red; intros; inv H; simpl. omega. inv H3. eapply external_call_trace_length; eauto. - inv H4. eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. inv H3. eapply external_call_trace_length; eauto. -(* initial states *) +- (* initial states *) inv H; inv H0. f_equal. congruence. -(* final no step *) +- (* final no step *) inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence. -(* final states *) +- (* final states *) inv H; inv H0. congruence. Qed. diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 9c0a76e0..2c1afc11 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -492,14 +492,6 @@ Definition transl_store (chunk: memory_chunk) Error (msg "Asmgen.transl_store") 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) @@ -546,7 +538,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mbuiltin ef args res => OK (Pbuiltin ef (List.map preg_of args) (List.map preg_of res) :: k) | Mannot ef args => - OK (Pannot ef (map transl_annot_param args) :: k) + OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) end. (** Translation of a code sequence *) diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 57d7de4a..3570da2e 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -700,13 +700,16 @@ Opaque loadind. 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. + exploit annot_args_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. + erewrite <- sp_val by eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. + exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index b6aef725..74e3fbd7 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -507,3 +507,17 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | _ => (Aindexed Int.zero, e:::Enil) end. +(** ** Arguments of annotations *) + +Nondetfunction annot_arg (e: expr) := + match e with + | Eop (Ointconst n) Enil => AA_int n + | Eop (Olea (Aglobal id ofs)) Enil => AA_addrglobal id ofs + | Eop (Olea (Ainstack ofs)) Enil => AA_addrstack ofs + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + AA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) + | Eload chunk (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs + | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs + | _ => AA_base e + end. diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 50688621..50f0d9b6 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -898,4 +898,20 @@ Proof. exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto. Qed. +Theorem eval_annot_arg: + forall a v, + eval_expr ge sp e m nil a v -> + CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. +Proof. + intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. +- constructor. +- constructor. +- constructor. +- simpl in H5. inv H5. constructor. +- subst v. constructor; auto. +- inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- inv H. InvEval. simpl in H6. inv H6. constructor; auto. +- constructor; auto. +Qed. + End CMCONSTR. diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index c00dfc57..cb4905ef 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -339,7 +339,7 @@ module Target(System: SYSTEM):TARGET = (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args + PrintAnnot.print_annot_stmt preg "%esp" oc txt targs args end let print_annot_val oc txt args res = diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 18316fb0..d707b2b5 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -276,13 +276,9 @@ Inductive instruction : Type := | Pxoris: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate high *) | Plabel: label -> instruction (**r define a code label *) | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function (pseudo) *) - | Pannot: external_function -> list annot_param -> instruction (**r annotation statement (pseudo) *) + | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement (pseudo) *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) - | Pcfi_rel_offset: int -> instruction (**r .cfi_rel_offset lr debug directive *) - -with annot_param : Type := - | APreg: preg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Pcfi_rel_offset: int -> instruction. (**r .cfi_rel_offset lr debug directive *) (** The pseudo-instructions are the following: @@ -936,20 +932,6 @@ Definition extcall_arguments Definition loc_external_result (sg: signature) : list preg := map 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 := @@ -978,8 +960,8 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) -> - annot_arguments rs m args vargs -> - external_call' ef ge vargs m t v m' -> + eval_annot_args ge rs (rs GPR1) m args vargs -> + external_call ef ge vargs m t v m' -> step (State rs m) t (State (nextinstr rs) m') | exec_step_external: @@ -1031,16 +1013,6 @@ Proof. intros. red in H0; red in H1. eauto. Qed. -Remark annot_arguments_determ: - forall rs m params args1 args2, - annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. -Proof. - unfold annot_arguments. intros. revert params args1 H args2 H0. - induction 1; intros. - inv H0; auto. - inv H1. decEq; eauto. inv H; inv H4. auto. congruence. -Qed. - Lemma semantics_determinate: forall p, determinate (semantics p). Proof. Ltac Equalities := @@ -1059,8 +1031,8 @@ Ltac Equalities := exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. inv H12. - assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. - exploit external_call_determ'. eexact H5. eexact H13. intros [A B]. + assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. @@ -1069,7 +1041,7 @@ Ltac Equalities := red; intros. inv H; simpl. omega. inv H3; eapply external_call_trace_length; eauto. - inv H4; eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. inv H2; eapply external_call_trace_length; eauto. (* initial states *) inv H; inv H0. f_equal. congruence. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index c003bcd1..47895cb1 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -74,7 +74,7 @@ let _m8 = coqint_of_camlint (-8l) (* Handling of annotations *) let expand_annot_val txt targ args res = - emit (Pannot(EF_annot(txt, [AA_arg targ]), List.map (fun r -> APreg r) args)); + emit (Pannot(EF_annot(txt, [targ]), List.map (fun r -> AA_base r) args)); begin match args, res with | [IR src], [IR dst] -> if dst <> src then emit (Pmr(dst, src)) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 2bd69d91..7ee6c770 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -610,14 +610,6 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) Error (msg "Asmgen.transl_store") 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) @@ -658,7 +650,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mbuiltin ef args res => OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) | Mannot ef args => - OK (Pannot ef (map transl_annot_param args) :: k) + OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) | Mlabel lbl => OK (Plabel lbl :: k) | Mgoto lbl => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index c7439c3d..27b32ba1 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -778,13 +778,16 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. 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. + exploit annot_args_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. + erewrite <- sp_val by eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. + exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 70b1feb6..618643b8 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -523,3 +523,18 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) | _ => (Aindexed Int.zero, e:::Enil) end. + +(** ** Arguments of annotations *) + +Nondetfunction annot_arg (e: expr) := + match e with + | Eop (Ointconst n) Enil => AA_int n + | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs + | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + AA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) + | Eload chunk (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs + | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs + | _ => AA_base e + end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 8311b82c..c51b650b 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -999,5 +999,21 @@ Proof. rewrite Int.add_zero. auto. Qed. +Theorem eval_annot_arg: + forall a v, + eval_expr ge sp e m nil a v -> + CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. +Proof. + intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. +- constructor. +- constructor. +- constructor. +- simpl in H5. inv H5. constructor. +- subst v. constructor; auto. +- inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- inv H. InvEval. simpl in H6. inv H6. constructor; auto. +- constructor; auto. +Qed. + End CMCONSTR. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 70aec6c0..7e460f46 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -234,9 +234,12 @@ module Target (System : SYSTEM):TARGET = let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r + (* [preg] is only used for printing annotations. + Use the full register names [rN] and [fN] to avoid + ambiguity with constants. *) let preg oc = function - | IR r -> ireg oc r - | FR r -> freg oc r + | IR r -> fprintf oc "r%s" (int_reg_name r) + | FR r -> fprintf oc "f%s" (float_reg_name r) | _ -> assert false let section oc sec = diff --git a/test/regression/annot1.c b/test/regression/annot1.c index 9bdf14eb..b60f8a64 100644 --- a/test/regression/annot1.c +++ b/test/regression/annot1.c @@ -58,6 +58,42 @@ void k(int arg) C1 + 1, arg, C2 * 2); } +int j(int a) +{ + /* Local variables that are stack-allocated early */ + short b = 0, c = 0; + char d[4]; + *(a ? &b : &c) = 42; + __builtin_annot("j %1 %2 %3 %4", b, c, d[0], d[3]); + return b; +} + +long long ll(long long a) +{ + /* Force spilling */ + long long b = a+1; + long long c = b+1; + long long d = c+1; + long long e = d+1; + long long f = e+1; + long long g = f+1; + long long h = g+1; + long long i = h+1; + long long j = i+1; + long long k = j+1; + long long l = k+1; + long long m = l+1; + long long n = m+1; + long long o = n+1; + long long p = o+1; + long long q = p+1; + long long r = q+1; + long long s = r+1; + long long t = s+1; + __builtin_annot("ll %1 %2 %3 %4 %5 %6 %7 %8 %9 %10 %11 %12 %13 %14 %15 %16 %17 %18 %19 %20", a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t); + return t; +} + int main() { __builtin_annot("calling f"); |