diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-21 11:05:36 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-21 11:05:36 +0200 |
| commit | 54f97d1988f623ba7422e13a504caeb5701ba93c (patch) | |
| tree | d8dea46837352979490f4ed4516f9649fef41b98 /backend | |
| parent | b4846ffadfa3fbb73ffa7d9c43e5218adeece8da (diff) | |
| download | compcert-kvx-54f97d1988f623ba7422e13a504caeb5701ba93c.tar.gz compcert-kvx-54f97d1988f623ba7422e13a504caeb5701ba93c.zip | |
Refactoring of builtins and annotations in the back-end.
Before, the back-end languages had distinct instructions
- Iannot for annotations, taking structured expressions (annot_arg)
as arguments, and producing no results'
- Ibuiltin for other builtins, using simple pseudoregs/locations/registers
as arguments and results.
This branch enriches Ibuiltin instructions so that they take structured
expressions (builtin_arg and builtin_res) as arguments and results.
This way,
- Annotations fit the general pattern of builtin functions,
so Iannot instructions are removed.
- EF_vload_global and EF_vstore_global become useless, as the
same optimization can be achieved by EF_vload/vstore taking
a structured argument of the "address of global" kind.
- Better code can be generated for builtin_memcpy between stack locations,
or volatile accesses to stack locations.
Finally, this commit also introduces a new kind of external function,
EF_debug, which is like EF_annot but produces no observable events.
It will be used later to transport debug info through the back-end,
without preventing optimizations.
Diffstat (limited to 'backend')
51 files changed, 1718 insertions, 1472 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 37b79a1a..5499c1c5 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -93,12 +93,10 @@ Inductive block_shape: Type := (mv1: moves) (ros': mreg + ident) (mv2: moves) (s: node) | BStailcall (sg: signature) (ros: reg + ident) (args: list reg) (mv1: moves) (ros': mreg + ident) - | BSbuiltin (ef: external_function) (args: list reg) (res: reg) - (mv1: moves) (args': list mreg) (res': list mreg) + | BSbuiltin (ef: external_function) + (args: list (builtin_arg reg)) (res: builtin_res reg) + (mv1: moves) (args': list (builtin_arg loc)) (res': builtin_res mreg) (mv2: moves) (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) @@ -280,14 +278,6 @@ Definition pair_instr_block Some(BSbuiltin ef args res mv1 args' res' mv2 s) | _ => None end - | Iannot ef args s => - match b with - | Lannot ef' args' :: b1 => - assertion (external_function_eq ef ef'); - assertion (check_succ s b1); - Some(BSannot ef args args' s) - | _ => None - end | Icond cond args s1 s2 => let (mv1, b1) := extract_moves nil b in match b1 with @@ -699,54 +689,86 @@ 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. *) +(** [add_equations_builtin_arg] adds the needed equations for arguments + to builtin functions. *) -Fixpoint add_equations_annot_arg (env: regenv) (arg: annot_arg reg) (arg': annot_arg loc) (e: eqs) : option eqs := +Fixpoint add_equations_builtin_arg + (env: regenv) (arg: builtin_arg reg) (arg': builtin_arg loc) (e: eqs) : option eqs := match arg, arg' with - | AA_base r, AA_base l => + | BA r, BA l => Some (add_equation (Eq Full r l) e) - | AA_base r, AA_longofwords (AA_base lhi) (AA_base llo) => + | BA r, BA_longofwords (BA lhi) (BA 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' => + | BA_int n, BA_int n' => assertion (Int.eq_dec n n'); Some e - | AA_long n, AA_long n' => + | BA_long n, BA_long n' => assertion (Int64.eq_dec n n'); Some e - | AA_float f, AA_float f' => + | BA_float f, BA_float f' => assertion (Float.eq_dec f f'); Some e - | AA_single f, AA_single f' => + | BA_single f, BA_single f' => assertion (Float32.eq_dec f f'); Some e - | AA_loadstack chunk ofs, AA_loadstack chunk' ofs' => + | BA_loadstack chunk ofs, BA_loadstack chunk' ofs' => assertion (chunk_eq chunk chunk'); assertion (Int.eq_dec ofs ofs'); Some e - | AA_addrstack ofs, AA_addrstack ofs' => + | BA_addrstack ofs, BA_addrstack ofs' => assertion (Int.eq_dec ofs ofs'); Some e - | AA_loadglobal chunk id ofs, AA_loadglobal chunk' id' ofs' => + | BA_loadglobal chunk id ofs, BA_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' => + | BA_addrglobal id ofs, BA_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 + | BA_longofwords hi lo, BA_longofwords hi' lo' => + do e1 <- add_equations_builtin_arg env hi hi' e; + add_equations_builtin_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 := +Fixpoint add_equations_builtin_args + (env: regenv) (args: list (builtin_arg reg)) + (args': list (builtin_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 + do e1 <- add_equations_builtin_arg env a1 a1' e; + add_equations_builtin_args env al al' e1 + | _, _ => None + end. + +(** For [EF_debug] builtins, some arguments can be removed. *) + +Fixpoint add_equations_debug_args + (env: regenv) (args: list (builtin_arg reg)) + (args': list (builtin_arg loc)) (e: eqs) : option eqs := + match args, args' with + | _, nil => Some e + | a1 :: al, a1' :: al' => + match add_equations_builtin_arg env a1 a1' e with + | None => add_equations_debug_args env al args' e + | Some e1 => add_equations_debug_args env al al' e1 + end + | _, _ => None + end. + +(** Checking of the result of a builtin *) + +Definition remove_equations_builtin_res + (env: regenv) (res: builtin_res reg) (res': builtin_res mreg) (e: eqs) : option eqs := + match res, res' with + | BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e) + | BR r, BR_longofwords (BR rhi) (BR rlo) => + assertion (typ_eq (env r) Tlong); + if mreg_eq rhi rlo then None else + Some (remove_equation (Eq Low r (R rlo)) + (remove_equation (Eq High r (R rhi)) e)) + | BR_none, BR_none => Some e | _, _ => None end. @@ -972,16 +994,18 @@ Definition transfer_aux (f: RTL.function) (env: regenv) track_moves env mv1 e2 | BSbuiltin ef args res mv1 args' res' mv2 s => do e1 <- track_moves env mv2 e; - let args' := map R args' in - let res' := map R res' in - do e2 <- remove_equations_res res (sig_res (ef_sig ef)) res' e1; - assertion (reg_unconstrained res e2); - assertion (forallb (fun l => loc_unconstrained l e2) res'); + do e2 <- remove_equations_builtin_res env res res' e1; + assertion (forallb (fun r => reg_unconstrained r e2) + (params_of_builtin_res res)); + assertion (forallb (fun mr => loc_unconstrained (R mr) e2) + (params_of_builtin_res res')); assertion (can_undef (destroyed_by_builtin ef) e2); - do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2; + do e3 <- + match ef with + | EF_debug _ _ _ => add_equations_debug_args env args args' e2 + | _ => add_equations_builtin_args env args args' e2 + end; track_moves env mv1 e3 - | 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; @@ -1152,7 +1176,6 @@ 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 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 875d4929..57adf102 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -165,10 +165,6 @@ 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 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) @@ -318,10 +314,8 @@ Proof. (* tailcall *) destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. econstructor; eauto. (* builtin *) - destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. + destruct b1; MonadInv. destruct i; MonadInv; UseParsingLemmas. econstructor; eauto. -(* annot *) - destruct b; MonadInv. destruct i; MonadInv. UseParsingLemmas. constructor. (* cond *) destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. econstructor; eauto. (* jumptable *) @@ -1347,9 +1341,9 @@ Proof. rewrite Int64.hi_ofwords, Int64.lo_ofwords; auto. Qed. -Lemma add_equations_annot_arg_satisf: +Lemma add_equations_builtin_arg_satisf: forall env rs ls arg arg' e e', - add_equations_annot_arg env arg arg' e = Some e' -> + add_equations_builtin_arg env arg arg' e = Some e' -> satisf rs ls e' -> satisf rs ls e. Proof. induction arg; destruct arg'; simpl; intros; MonadInv; eauto. @@ -1357,65 +1351,171 @@ Proof. destruct arg'1; MonadInv. destruct arg'2; MonadInv. eauto using add_equation_satisf. Qed. -Lemma add_equations_annot_arg_lessdef: +Lemma add_equations_builtin_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 -> + eval_builtin_arg ge (fun r => rs#r) sp m arg v -> forall e e' arg', - add_equations_annot_arg env arg arg' e = Some e' -> + add_equations_builtin_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'. + exists v', eval_builtin_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. + exists (ls x0); auto with barg. - 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. + exists (Val.longofwords (ls x0) (ls x1)); split; auto with barg. 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. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- exploit IHeval_builtin_arg1; eauto. eapply add_equations_builtin_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. + exploit IHeval_builtin_arg2; eauto. intros (v2 & C & D). + exists (Val.longofwords v1 v2); split; auto with barg. apply Val.longofwords_lessdef; auto. Qed. -Lemma add_equations_annot_args_satisf: +Lemma add_equations_builtin_args_satisf: forall env rs ls arg arg' e e', - add_equations_annot_args env arg arg' e = Some e' -> + add_equations_builtin_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. + induction arg; destruct arg'; simpl; intros; MonadInv; eauto using add_equations_builtin_arg_satisf. Qed. -Lemma add_equations_annot_args_lessdef: +Lemma add_equations_builtin_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 -> + eval_builtin_args ge (fun r => rs#r) sp m arg vl -> forall arg' e e', - add_equations_annot_args env arg arg' e = Some e' -> + add_equations_builtin_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'. + exists vl', eval_builtin_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). + exploit add_equations_builtin_arg_lessdef; eauto. + eapply add_equations_builtin_args_satisf; eauto. intros (v1' & C & D). + exploit (@eval_builtin_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F). exists (v1'' :: vl'); split; constructor; auto. eapply Val.lessdef_trans; eauto. Qed. +Lemma add_equations_debug_args_satisf: + forall env rs ls arg arg' e e', + add_equations_debug_args env arg arg' e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction arg; destruct arg'; simpl; intros; MonadInv; auto. + destruct (add_equations_builtin_arg env a b e) as [e1|] eqn:A; + eauto using add_equations_builtin_arg_satisf. +Qed. + +Lemma add_equations_debug_args_eval: + forall env (ge: RTL.genv) sp rs ls m tm arg vl, + eval_builtin_args ge (fun r => rs#r) sp m arg vl -> + forall arg' e e', + add_equations_debug_args env arg arg' e = Some e' -> + satisf rs ls e' -> + wt_regset env rs -> + Mem.extends m tm -> + exists vl', eval_builtin_args ge ls sp tm arg' vl'. +Proof. + induction 1; simpl; intros; destruct arg'; MonadInv. +- exists (@nil val); constructor. +- exists (@nil val); constructor. +- destruct (add_equations_builtin_arg env a1 b e) as [e1|] eqn:A. ++ exploit IHlist_forall2; eauto. intros (vl' & B). + exploit add_equations_builtin_arg_lessdef; eauto. + eapply add_equations_debug_args_satisf; eauto. intros (v1' & C & D). + exploit (@eval_builtin_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F). + exists (v1'' :: vl'); constructor; auto. ++ eauto. +Qed. + +Lemma add_equations_builtin_eval: + forall ef env args args' e1 e2 m1 m1' rs ls (ge: RTL.genv) sp vargs t vres m2, + wt_regset env rs -> + match ef with + | EF_debug _ _ _ => add_equations_debug_args env args args' e1 + | _ => add_equations_builtin_args env args args' e1 + end = Some e2 -> + Mem.extends m1 m1' -> + satisf rs ls e2 -> + eval_builtin_args ge (fun r => rs # r) sp m1 args vargs -> + external_call ef ge vargs m1 t vres m2 -> + satisf rs ls e1 /\ + exists vargs' vres' m2', + eval_builtin_args ge ls sp m1' args' vargs' + /\ external_call ef ge vargs' m1' t vres' m2' + /\ Val.lessdef vres vres' + /\ Mem.extends m2 m2'. +Proof. + intros. + assert (DEFAULT: add_equations_builtin_args env args args' e1 = Some e2 -> + satisf rs ls e1 /\ + exists vargs' vres' m2', + eval_builtin_args ge ls sp m1' args' vargs' + /\ external_call ef ge vargs' m1' t vres' m2' + /\ Val.lessdef vres vres' + /\ Mem.extends m2 m2'). + { + intros. split. eapply add_equations_builtin_args_satisf; eauto. + exploit add_equations_builtin_args_lessdef; eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros (vres' & m2' & C & D & E & F). + exists vargs', vres', m2'; auto. + } + destruct ef; auto. + split. eapply add_equations_debug_args_satisf; eauto. + exploit add_equations_debug_args_eval; eauto. + intros (vargs' & A). + simpl in H4; inv H4. + exists vargs', Vundef, m1'. intuition auto. simpl. constructor. +Qed. + +Lemma parallel_set_builtin_res_satisf: + forall env res res' e0 e1 rs ls v v', + remove_equations_builtin_res env res res' e0 = Some e1 -> + forallb (fun r => reg_unconstrained r e1) (params_of_builtin_res res) = true -> + forallb (fun mr => loc_unconstrained (R mr) e1) (params_of_builtin_res res') = true -> + satisf rs ls e1 -> + Val.lessdef v v' -> + satisf (regmap_setres res v rs) (Locmap.setres res' v' ls) e0. +Proof. + intros. rewrite forallb_forall in *. + destruct res, res'; simpl in *; inv H. +- apply parallel_assignment_satisf with (k := Full); auto. + unfold reg_loc_unconstrained. rewrite H0 by auto. rewrite H1 by auto. auto. +- destruct res'1; try discriminate. destruct res'2; try discriminate. + rename x0 into hi; rename x1 into lo. MonadInv. destruct (mreg_eq hi lo); inv H5. + set (e' := remove_equation {| ekind := High; ereg := x; eloc := R hi |} e0) in *. + set (e'' := remove_equation {| ekind := Low; ereg := x; eloc := R lo |} e') in *. + simpl in *. red; intros. + destruct (OrderedEquation.eq_dec q (Eq Low x (R lo))). + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. apply Val.loword_lessdef; auto. + destruct (OrderedEquation.eq_dec q (Eq High x (R hi))). + subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; auto). + rewrite Locmap.gss. apply Val.hiword_lessdef; auto. + assert (EqSet.In q e''). + { unfold e'', e', remove_equation; simpl; ESD.fsetdec. } + rewrite Regmap.gso. rewrite ! Locmap.gso. auto. + eapply loc_unconstrained_sound; eauto. + eapply loc_unconstrained_sound; eauto. + eapply reg_unconstrained_sound; eauto. +- auto. +Qed. + (** * Properties of the dataflow analysis *) Lemma analyze_successors: @@ -2071,29 +2171,22 @@ Proof. rewrite SIG. inv WTI. rewrite <- H6. apply wt_regset_list; auto. (* builtin *) -- assert (WTRS': wt_regset env (rs#res <- v)) by (eapply wt_exec_Ibuiltin; eauto). - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit external_call_mem_extends; eauto. - eapply add_equations_args_lessdef; eauto. - inv WTI. rewrite <- H4. apply wt_regset_list; auto. - intros [v' [m'' [F [G [J K]]]]]. - assert (E: map ls1 (map R args') = reglist ls1 args'). - { unfold reglist. rewrite list_map_compose. auto. } - rewrite E in F. clear E. - set (vl' := encode_long (sig_res (ef_sig ef)) v'). - set (ls2 := Locmap.setlist (map R res') vl' (undef_regs (destroyed_by_builtin ef) ls1)). - assert (satisf (rs#res <- v) ls2 e0). - { eapply parallel_assignment_satisf_2; eauto. - eapply can_undef_satisf; eauto. - eapply add_equations_args_satisf; eauto. } +- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit add_equations_builtin_eval; eauto. + intros (C & vargs' & vres' & m'' & D & E & F & G). + assert (WTRS': wt_regset env (regmap_setres res vres rs)) by (eapply wt_exec_Ibuiltin; eauto). + set (ls2 := Locmap.setres res' vres' (undef_regs (destroyed_by_builtin ef) ls1)). + assert (satisf (regmap_setres res vres rs) ls2 e0). + { eapply parallel_set_builtin_res_satisf; eauto. + eapply can_undef_satisf; eauto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. econstructor; split. eapply plus_left. econstructor; eauto. eapply star_trans. eexact A1. - eapply star_left. econstructor. - econstructor. unfold reglist. eapply external_call_symbols_preserved; eauto. + eapply star_left. econstructor. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved. eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - instantiate (1 := vl'); auto. instantiate (1 := ls2); auto. eapply star_right. eexact A3. econstructor. @@ -2101,23 +2194,6 @@ Proof. exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. econstructor; eauto. - -(* annot *) -- 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_two. econstructor. - 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. - constructor. eauto. traceEq. - exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply add_equations_annot_args_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. (* cond *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index ba7fa3a6..0533d561 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -356,29 +356,55 @@ Proof. eapply extcall_args_match; eauto. Qed. -(** Translation of arguments to annotations. *) +(** Translation of arguments and results to builtins. *) -Remark annot_arg_match: +Remark builtin_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. + eval_builtin_arg ge (fun r => rs (preg_of r)) sp m a v -> + eval_builtin_arg ge rs sp m (map_builtin_arg preg_of a) v. Proof. - induction 1; simpl; eauto with aarg. + induction 1; simpl; eauto with barg. Qed. -Lemma annot_args_match: +Lemma builtin_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' + forall al vl, eval_builtin_args ge ms sp m al vl -> + exists vl', eval_builtin_args ge rs sp m' (map (map_builtin_arg preg_of) al) vl' /\ Val.lessdef_list vl vl'. Proof. induction 3; intros; simpl. exists (@nil val); split; constructor. - exploit (@eval_annot_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto. + exploit (@eval_builtin_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. apply annot_arg_match; auto. + exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto. +Qed. + +Lemma agree_set_res: + forall res ms sp rs v v', + agree ms sp rs -> + Val.lessdef v v' -> + agree (Mach.set_res res v ms) sp (Asm.set_res (map_builtin_res preg_of res) v' rs). +Proof. + induction res; simpl; intros. +- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto. + intros. apply Pregmap.gso; auto. +- auto. +- apply IHres2. apply IHres1. auto. + apply Val.hiword_lessdef; auto. + apply Val.loword_lessdef; auto. +Qed. + +Lemma set_res_other: + forall r res v rs, + data_preg r = false -> + set_res (map_builtin_res preg_of res) v rs r = rs r. +Proof. + induction res; simpl; intros. +- apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate. +- auto. +- rewrite IHres2, IHres1; auto. Qed. (** * Correspondence between Mach code and Asm code *) diff --git a/backend/Bounds.v b/backend/Bounds.v index 04c1328d..beb29965 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -67,9 +67,8 @@ Definition instr_within_bounds (i: instruction) := | Lload chunk addr args dst => mreg_within_bounds dst | Lcall sig ros => size_arguments sig <= bound_outgoing b | Lbuiltin ef args res => - 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) (params_of_annot_args args) -> slot_within_bounds sl ofs ty + (forall r, In r (params_of_builtin_res res) \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r) + /\ (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_args args) -> slot_within_bounds sl ofs ty) | _ => True end. @@ -101,8 +100,7 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lbuiltin ef args res => res ++ destroyed_by_builtin ef - | Lannot ef args => nil + | Lbuiltin ef args res => params_of_builtin_res res ++ destroyed_by_builtin ef | Llabel lbl => nil | Lgoto lbl => nil | Lcond cond args lbl => nil @@ -121,7 +119,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 (params_of_annot_args args) + | Lbuiltin ef args res => slots_of_locs (params_of_builtin_args args) | _ => nil end. @@ -351,8 +349,8 @@ Proof. (* call *) eapply size_arguments_bound; eauto. (* builtin *) + split; intros. apply H1. apply in_or_app; auto. -(* annot *) apply H0. rewrite slots_of_locs_charact; auto. Qed. diff --git a/backend/CMparser.mly b/backend/CMparser.mly index f62e05d4..b48a486e 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -42,12 +42,6 @@ let mkef sg toks = EF_vload c | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] -> EF_vstore c - | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c; - EFT_tok "global"; EFT_string s; EFT_int n] -> - EF_vload_global(c, intern_string s, coqint_of_camlint n) - | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c; - EFT_tok "global"; EFT_string s; EFT_int n] -> - EF_vstore_global(c, intern_string s, coqint_of_camlint n) | [EFT_tok "malloc"] -> EF_malloc | [EFT_tok "free"] -> diff --git a/backend/CSE.v b/backend/CSE.v index c0efa941..ebeb921e 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -228,6 +228,12 @@ Definition set_unknown (n: numbering) (rd: reg) := num_reg := PTree.remove rd n.(num_reg); num_val := forget_reg n rd |}. +Definition set_res_unknown (n: numbering) (res: builtin_res reg) := + match res with + | BR r => set_unknown n r + | _ => n + end. + (** [kill_equations pred n] remove all equations satisfying predicate [pred]. *) Fixpoint kill_eqs (pred: rhs -> bool) (eqs: list equation) : list equation := @@ -307,16 +313,15 @@ Definition add_store_result (app: VA.t) (n: numbering) (chunk: memory_chunk) (ad num_val := n2.(num_val) |} else n. -(** [kill_loads_after_storebyte app n dst sz] removes all equations +(** [kill_loads_after_storebyte n dst sz] removes all equations involving loads that could be invalidated by a store of [sz] bytes starting at address [dst]. Loads that are disjoint from this store-bytes are preserved. Equations involving memory-dependent operators are also removed. *) Definition kill_loads_after_storebytes - (app: VA.t) (n: numbering) (dst: reg) (sz: Z) := - let p := aaddr app dst in - kill_equations (filter_after_store app n p sz) n. + (app: VA.t) (n: numbering) (dst: aptr) (sz: Z) := + kill_equations (filter_after_store app n dst sz) n. (** [add_memcpy app n1 n2 rsrc rdst sz] adds equations to [n2] that represent the effect of a [memcpy] block copy operation of [sz] bytes @@ -355,8 +360,8 @@ Fixpoint add_memcpy_eqs (src sz delta: Z) (eqs1 eqs2: list equation) := end end. -Definition add_memcpy (app: VA.t) (n1 n2: numbering) (rsrc rdst: reg) (sz: Z) := - match aaddr app rsrc, aaddr app rdst with +Definition add_memcpy (n1 n2: numbering) (asrc adst: aptr) (sz: Z) := + match asrc, adst with | Stk src, Stk dst => {| num_next := n2.(num_next); num_eqs := add_memcpy_eqs (Int.unsigned src) sz @@ -478,22 +483,22 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb match ef with | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ => empty_numbering - | EF_builtin _ _ | EF_vstore _ | EF_vstore_global _ _ _ => - set_unknown (kill_all_loads before) res + | EF_builtin _ _ | EF_vstore _ => + set_res_unknown (kill_all_loads before) res | EF_memcpy sz al => match args with - | rdst :: rsrc :: nil => + | dst :: src :: nil => let app := approx!!pc in - let n := kill_loads_after_storebytes app before rdst sz in - set_unknown (add_memcpy app before n rsrc rdst sz) res + let adst := aaddr_arg app dst in + let asrc := aaddr_arg app src in + let n := kill_loads_after_storebytes app before adst sz in + set_res_unknown (add_memcpy before n asrc adst sz) res | _ => empty_numbering end - | EF_vload _ | EF_vload_global _ _ _ | EF_annot _ _ | EF_annot_val _ _ => - set_unknown before res + | EF_vload _ | EF_annot _ _ | EF_annot_val _ _ | EF_debug _ _ _ => + set_res_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 c24fa69b..70f9bfc7 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -419,6 +419,14 @@ Proof. rewrite Regmap.gso; eauto with cse. Qed. +Lemma set_res_unknown_holds: + forall valu ge sp rs m n r v, + numbering_holds valu ge sp rs m n -> + numbering_holds valu ge sp (regmap_setres r v rs) m (set_res_unknown n r). +Proof. + intros. destruct r; simpl; auto. apply set_unknown_holds; auto. +Qed. + Lemma kill_eqs_charact: forall pred l strict r eqs, In (Eq l strict r) (kill_eqs pred eqs) -> @@ -533,7 +541,7 @@ Qed. Lemma kill_loads_after_storebytes_holds: forall valu ge sp rs m n dst b ofs bytes m' bc approx ae am sz, numbering_holds valu ge (Vptr sp Int.zero) rs m n -> - rs#dst = Vptr b ofs -> + pmatch bc b ofs dst -> Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> genv_match bc ge -> bc sp = BCstack -> @@ -556,7 +564,7 @@ Proof. eapply pdisjoint_sound. eauto. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. - unfold aaddr. apply match_aptr_of_aval. rewrite <- H0. apply H4. + auto. Qed. Lemma load_memcpy: @@ -675,33 +683,25 @@ Proof. Qed. Lemma add_memcpy_holds: - forall m bsrc osrc sz bytes bdst odst m' valu ge sp rs n1 n2 bc approx ae am rsrc rdst, + forall m bsrc osrc sz bytes bdst odst m' valu ge sp rs n1 n2 bc asrc adst, Mem.loadbytes m bsrc (Int.unsigned osrc) sz = Some bytes -> Mem.storebytes m bdst (Int.unsigned odst) bytes = Some m' -> numbering_holds valu ge (Vptr sp Int.zero) rs m n1 -> numbering_holds valu ge (Vptr sp Int.zero) rs m' n2 -> - genv_match bc ge -> + pmatch bc bsrc osrc asrc -> + pmatch bc bdst odst adst -> bc sp = BCstack -> - ematch bc rs ae -> - approx = VA.State ae am -> - rs#rsrc = Vptr bsrc osrc -> - rs#rdst = Vptr bdst odst -> Ple (num_next n1) (num_next n2) -> - numbering_holds valu ge (Vptr sp Int.zero) rs m' (add_memcpy approx n1 n2 rsrc rdst sz). + numbering_holds valu ge (Vptr sp Int.zero) rs m' (add_memcpy n1 n2 asrc adst sz). Proof. intros. unfold add_memcpy. - destruct (aaddr approx rsrc) eqn:ASRC; auto. - destruct (aaddr approx rdst) eqn:ADST; auto. - assert (A: forall r b o i, - rs#r = Vptr b o -> aaddr approx r = Stk i -> b = sp /\ i = o). + destruct asrc; auto; destruct adst; auto. + assert (A: forall b o i, pmatch bc b o (Stk i) -> b = sp /\ i = o). { - intros until i. unfold aaddr; subst approx. intros. - specialize (H5 r). rewrite H6 in H5. apply match_aptr_of_aval in H5. - rewrite H10 in H5. inv H5. split; auto. eapply bc_stack; eauto. + intros. inv H7. split; auto. eapply bc_stack; eauto. } - exploit (A rsrc); eauto. intros [P Q]. - exploit (A rdst); eauto. intros [U V]. - subst bsrc ofs bdst ofs0. + apply A in H3; destruct H3. subst bsrc ofs. + apply A in H4; destruct H4. subst bdst ofs0. constructor; simpl; intros; eauto with cse. - constructor; simpl; eauto with cse. intros. exploit add_memcpy_eqs_charact; eauto. intros [X | (e0 & X & Y)]. @@ -1102,62 +1102,51 @@ Proof. apply regs_lessdef_regs; auto. - (* Ibuiltin *) + exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. + intros (vargs' & A & B). exploit external_call_mem_extends; eauto. - instantiate (1 := rs'##args). apply regs_lessdef_regs; auto. intros (v' & m1' & P & Q & R & S). econstructor; split. - eapply exec_Ibuiltin; eauto. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_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. destruct SAT as [valu NH]. - assert (CASE1: exists valu, numbering_holds valu ge sp (rs#res <- v) m' empty_numbering). + assert (CASE1: exists valu, numbering_holds valu ge sp (regmap_setres res vres rs) m' empty_numbering). { exists valu; apply empty_numbering_holds. } - assert (CASE2: m' = m -> exists valu, numbering_holds valu ge sp (rs#res <- v) m' (set_unknown approx#pc res)). - { intros. rewrite H1. exists valu. apply set_unknown_holds; auto. } - assert (CASE3: exists valu, numbering_holds valu ge sp (rs#res <- v) m' - (set_unknown (kill_all_loads approx#pc) res)). - { exists valu. apply set_unknown_holds. eapply kill_all_loads_hold; eauto. } + assert (CASE2: m' = m -> exists valu, numbering_holds valu ge sp (regmap_setres res vres rs) m' (set_res_unknown approx#pc res)). + { intros. subst m'. exists valu. apply set_res_unknown_holds; auto. } + assert (CASE3: exists valu, numbering_holds valu ge sp (regmap_setres res vres rs) m' + (set_res_unknown (kill_all_loads approx#pc) res)). + { exists valu. apply set_res_unknown_holds. eapply kill_all_loads_hold; eauto. } destruct ef. + apply CASE1. + apply CASE3. - + apply CASE2; inv H0; auto. + + apply CASE2; inv H1; auto. + apply CASE3. - + apply CASE2; inv H0; auto. - + apply CASE3; auto. + apply CASE1. + apply CASE1. - + destruct args as [ | rdst args]; auto. - destruct args as [ | rsrc args]; auto. - destruct args; auto. - simpl in H0. inv H0. - exists valu. - apply set_unknown_holds. - inv SOUND. eapply add_memcpy_holds; eauto. + + inv H0; auto. inv H3; auto. inv H4; auto. + simpl in H1. inv H1. + exists valu. + apply set_res_unknown_holds. + inv SOUND. unfold vanalyze, rm; rewrite AN. + assert (pmatch bc bsrc osrc (aaddr_arg (VA.State ae am) a0)) + by (eapply aaddr_arg_sound_1; eauto). + assert (pmatch bc bdst odst (aaddr_arg (VA.State ae am) a1)) + by (eapply aaddr_arg_sound_1; eauto). + eapply add_memcpy_holds; eauto. eapply kill_loads_after_storebytes_holds; eauto. eapply Mem.loadbytes_length; eauto. simpl. apply Ple_refl. - + apply CASE2; inv H0; auto. - + apply CASE2; inv H0; auto. + + apply CASE2; inv H1; auto. + + apply CASE2; inv H1; auto. + 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. + + apply CASE2; inv H1; auto. +* apply set_res_lessdef; auto. - (* Icond *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index d48a0553..1e93dd7a 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -291,15 +291,11 @@ Proof. econstructor; eauto. (* Lbuiltin *) left; econstructor; split. - econstructor; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - econstructor; eauto with coqlib. -(* Lannot *) - left; econstructor; split. - econstructor; eauto. - eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + econstructor. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eauto. econstructor; eauto with coqlib. (* Llabel *) case_eq (Labelset.mem lbl (labels_branched_to (fn_code f))); intros. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 668eb808..ad1cbd14 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -78,8 +78,7 @@ Inductive stmt : Type := | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt | 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 + | Sbuiltin : builtin_res ident -> external_function -> list (builtin_arg expr) -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -249,34 +248,42 @@ 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, +Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop := + | eval_BA: 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, + eval_builtin_arg (BA a) v + | eval_BA_int: forall n, + eval_builtin_arg (BA_int n) (Vint n) + | eval_BA_long: forall n, + eval_builtin_arg (BA_long n) (Vlong n) + | eval_BA_float: forall n, + eval_builtin_arg (BA_float n) (Vfloat n) + | eval_BA_single: forall n, + eval_builtin_arg (BA_single n) (Vsingle n) + | eval_BA_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, + eval_builtin_arg (BA_loadstack chunk ofs) v + | eval_BA_addrstack: forall ofs, + eval_builtin_arg (BA_addrstack ofs) (Val.add sp (Vint ofs)) + | eval_BA_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_builtin_arg (BA_loadglobal chunk id ofs) v + | eval_BA_addrglobal: forall id ofs, + eval_builtin_arg (BA_addrglobal id ofs) (Genv.symbol_address ge id ofs) + | eval_BA_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). + eval_builtin_arg (BA_longofwords (BA a1) (BA a2)) (Val.longofwords v1 v2). End EVAL_EXPR. +(** Update local environment with the result of a builtin. *) + +Definition set_builtin_res (res: builtin_res ident) (v: val) (e: env) : env := + match res with + | BR id => PTree.set id v e + | _ => e + end. + (** Pop continuation until a call or stop *) Fixpoint call_cont (k: cont) : cont := @@ -364,18 +371,11 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) m') - | step_builtin: forall f optid ef al k sp e m vl t v m', - eval_exprlist sp e m nil al vl -> - external_call ef ge vl m t v m' -> - 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 -> + | step_builtin: forall f res ef al k sp e m vl t v m', + list_forall2 (eval_builtin_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 (State f (Sbuiltin res ef al) k sp e m) + t (State f Sskip k sp (set_builtin_res res v e) m') | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) diff --git a/backend/Constprop.v b/backend/Constprop.v index ce56ff62..3a238b95 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -20,6 +20,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Op. +Require Machregs. Require Import Registers. Require Import RTL. Require Import Lattice. @@ -102,39 +103,58 @@ 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) (a: annot_arg reg) := +Fixpoint builtin_arg_reduction (ae: AE.t) (a: builtin_arg reg) := match a with - | AA_base r => + | BA 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 + | I n => BA_int n + | L n => BA_long n + | F n => if Compopts.generate_float_constants tt then BA_float n else a + | FS n => if Compopts.generate_float_constants tt then BA_single n else a | _ => a end - | 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' + | BA_longofwords hi lo => + match builtin_arg_reduction ae hi, builtin_arg_reduction ae lo with + | BA_int nhi, BA_int nlo => BA_long (Int64.ofwords nhi nlo) + | hi', lo' => BA_longofwords hi' lo' end | _ => a end. -Function builtin_strength_reduction - (ae: AE.t) (ef: external_function) (args: list reg) := - match ef, args with - | EF_vload chunk, r1 :: nil => - match areg ae r1 with - | Ptr(Gl symb n1) => (EF_vload_global chunk symb n1, nil) - | _ => (ef, args) - end - | EF_vstore chunk, r1 :: r2 :: nil => - match areg ae r1 with - | Ptr(Gl symb n1) => (EF_vstore_global chunk symb n1, r2 :: nil) - | _ => (ef, args) +Definition builtin_arg_strength_reduction + (ae: AE.t) (a: builtin_arg reg) (c: builtin_arg_constraint) := + let a' := builtin_arg_reduction ae a in + if builtin_arg_ok a' c then a' else a. + +Fixpoint builtin_args_strength_reduction + (ae: AE.t) (al: list (builtin_arg reg)) (cl: list builtin_arg_constraint) := + match al with + | nil => nil + | a :: al => + builtin_arg_strength_reduction ae a (List.hd OK_default cl) + :: builtin_args_strength_reduction ae al (List.tl cl) + end. + +(** For debug annotations, add constant values to the original info + instead of replacing it. *) + +Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) := + match al with + | nil => nil + | a :: al => + let a' := builtin_arg_reduction ae a in + let al' := a :: debug_strength_reduction ae al in + match a' with + | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al' + | _ => al' end - | _, _ => - (ef, args) + end. + +Definition builtin_strength_reduction + (ae: AE.t) (ef: external_function) (al: list (builtin_arg reg)) := + match ef with + | EF_debug _ _ _ => debug_strength_reduction ae al + | _ => builtin_args_strength_reduction ae al (Machregs.builtin_constraints ef) end. Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) @@ -174,10 +194,7 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) | Itailcall sig ros args => Itailcall sig (transf_ros ae ros) args | 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 + Ibuiltin ef (builtin_strength_reduction ae ef args) res 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 30bdd674..d9005f5e 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -93,24 +93,6 @@ Proof. intros. destruct f; reflexivity. Qed. -Definition regs_lessdef (rs1 rs2: regset) : Prop := - forall r, Val.lessdef (rs1#r) (rs2#r). - -Lemma regs_lessdef_regs: - forall rs1 rs2, regs_lessdef rs1 rs2 -> - forall rl, Val.lessdef_list rs1##rl rs2##rl. -Proof. - induction rl; constructor; auto. -Qed. - -Lemma set_reg_lessdef: - forall r v1 v2 rs1 rs2, - Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2). -Proof. - intros; red; intros. repeat rewrite Regmap.gsspec. - destruct (peq r0 r); auto. -Qed. - Lemma init_regs_lessdef: forall rl vl1 vl2, Val.lessdef_list vl1 vl2 -> @@ -211,54 +193,79 @@ Proof. unfold successor; intros. apply match_successor_rec. Qed. -Lemma annot_strength_reduction_correct: +Lemma builtin_arg_reduction_correct: 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. + eval_builtin_arg ge (fun r => rs#r) sp m a v -> + eval_builtin_arg ge (fun r => rs#r) sp m (builtin_arg_reduction ae a) v. Proof. - induction 2; simpl; eauto with aarg. + induction 2; simpl; eauto with barg. - 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. +- destruct (builtin_arg_reduction ae hi); auto with barg. + destruct (builtin_arg_reduction ae lo); auto with barg. + inv IHeval_builtin_arg1; inv IHeval_builtin_arg2. constructor. Qed. -Lemma annot_strength_reduction_correct_2: +Lemma builtin_arg_strength_reduction_correct: + forall bc sp m rs ae a v c, + ematch bc rs ae -> + eval_builtin_arg ge (fun r => rs#r) sp m a v -> + eval_builtin_arg ge (fun r => rs#r) sp m (builtin_arg_strength_reduction ae a c) v. +Proof. + intros. unfold builtin_arg_strength_reduction. + destruct (builtin_arg_ok (builtin_arg_reduction ae a) c). + eapply builtin_arg_reduction_correct; eauto. + auto. +Qed. + +Lemma builtin_args_strength_reduction_correct: 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. + eval_builtin_args ge (fun r => rs#r) sp m al vl -> + forall cl, + eval_builtin_args ge (fun r => rs#r) sp m (builtin_args_strength_reduction ae al cl) vl. Proof. - induction 2; simpl; constructor; auto. eapply annot_strength_reduction_correct; eauto. + induction 2; simpl; constructor. + eapply builtin_arg_strength_reduction_correct; eauto. + apply IHlist_forall2. +Qed. + +Lemma debug_strength_reduction_correct: + forall bc sp m rs ae, ematch bc rs ae -> + forall al vl, + eval_builtin_args ge (fun r => rs#r) sp m al vl -> + exists vl', eval_builtin_args ge (fun r => rs#r) sp m (debug_strength_reduction ae al) vl'. +Proof. + induction 2; simpl. +- exists (@nil val); constructor. +- destruct IHlist_forall2 as (vl' & A). + destruct (builtin_arg_reduction ae a1); repeat (eauto; econstructor). Qed. Lemma builtin_strength_reduction_correct: - forall bc ae rs ef args m t vres m', - genv_match bc ge -> + forall sp bc ae rs ef args vargs m t vres m', 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'. + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + exists vargs', + eval_builtin_args ge (fun r => rs#r) sp m (builtin_strength_reduction ae ef args) vargs' + /\ external_call ef ge vargs' m t vres m'. Proof. - 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 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 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. + intros. + assert (DEFAULT: forall cl, + exists vargs', + eval_builtin_args ge (fun r => rs#r) sp m (builtin_args_strength_reduction ae args cl) vargs' + /\ external_call ef ge vargs' m t vres m'). + { exists vargs; split; auto. eapply builtin_args_strength_reduction_correct; eauto. } + unfold builtin_strength_reduction. + destruct ef; auto. + exploit debug_strength_reduction_correct; eauto. intros (vargs' & P). + exists vargs'; split; auto. + inv H1; constructor. Qed. (** The proof of semantic preservation is a simulation argument @@ -478,36 +485,21 @@ Proof. apply regs_lessdef_regs; auto. (* Ibuiltin *) - rename pc'0 into pc. + rename pc'0 into pc. clear MATCH. TransfInstr; intros. Opaque builtin_strength_reduction. - exploit builtin_strength_reduction_correct; eauto. - TransfInstr. - destruct (builtin_strength_reduction ae ef args) as [ef' args']. - intros P Q. - exploit external_call_mem_extends; eauto. - instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto. + exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q). + exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). + apply REGS. eauto. eexact P. + intros (vargs'' & U & V). + exploit external_call_mem_extends; eauto. intros [v' [m2' [A [B [C D]]]]]. left; econstructor; econstructor; split. - eapply exec_Ibuiltin. eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - 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 exec_Ibuiltin; eauto. + eapply eval_builtin_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. + apply set_res_lessdef; auto. (* Icond, preserved *) rename pc' into pc. TransfInstr. diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 9a8f85d2..32bc26fb 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -70,41 +70,54 @@ 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 := +Fixpoint transfer_builtin_arg (nv: nval) (na: NA.t) (a: builtin_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 + | BA r => (add_need r nv ne, nm) + | BA_int _ | BA_long _ | BA_float _ | BA_single _ + | BA_addrstack _ | BA_addrglobal _ _ => (ne, nm) + | BA_loadstack chunk ofs => (ne, nmem_add nm (Stk ofs) (size_chunk chunk)) + | BA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk)) + | BA_longofwords hi lo => + transfer_builtin_arg All (transfer_builtin_arg All na hi) lo end. -Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) (res: reg) +Definition transfer_builtin_args (na: NA.t) (al: list (builtin_arg reg)) : NA.t := + List.fold_left (transfer_builtin_arg All) al na. + +Definition kill_builtin_res (res: builtin_res reg) (ne: NE.t) : NE.t := + match res with + | BR r => kill r ne + | _ => ne + end. + +Function transfer_builtin (app: VA.t) (ef: external_function) + (args: list (builtin_arg reg)) (res: builtin_res reg) (ne: NE.t) (nm: nmem) : NA.t := match ef, args with | EF_vload chunk, a1::nil => - (add_needs_all args (kill res ne), - nmem_add nm (aaddr app a1) (size_chunk chunk)) - | EF_vload_global chunk id ofs, nil => - (add_needs_all args (kill res ne), - nmem_add nm (Gl id ofs) (size_chunk chunk)) + transfer_builtin_arg All + (kill_builtin_res res ne, + nmem_add nm (aaddr_arg app a1) (size_chunk chunk)) + a1 | EF_vstore chunk, a1::a2::nil => - (add_need_all a1 (add_need a2 (store_argument chunk) (kill res ne)), nm) - | EF_vstore_global chunk id ofs, a1::nil => - (add_need a1 (store_argument chunk) (kill res ne), nm) + transfer_builtin_arg All + (transfer_builtin_arg (store_argument chunk) + (kill_builtin_res res ne, nm) a2) + a1 | EF_memcpy sz al, dst::src::nil => - if nmem_contains nm (aaddr app dst) sz then - (add_needs_all args (kill res ne), - nmem_add (nmem_remove nm (aaddr app dst) sz) (aaddr app src) sz) + if nmem_contains nm (aaddr_arg app dst) sz then + transfer_builtin_args + (kill_builtin_res res ne, + nmem_add (nmem_remove nm (aaddr_arg app dst) sz) (aaddr_arg app src) sz) + args else (ne, nm) - | EF_annot txt targs, _ => - (add_needs_all args (kill res ne), nm) - | EF_annot_val txt targ, _ => - (add_needs_all args (kill res ne), nm) + | (EF_annot _ _ | EF_annot_val _ _), _ => + transfer_builtin_args (kill_builtin_res res ne, nm) args + | EF_debug _ _ _, _ => + (kill_builtin_res res ne, nm) | _, _ => - (add_needs_all args (kill res ne), nmem_all) + transfer_builtin_args (kill_builtin_res res ne, nmem_all) args end. Definition transfer (f: function) (approx: PMap.t VA.t) @@ -139,8 +152,6 @@ 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) => @@ -187,7 +198,7 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t) then instr else Inop s | Ibuiltin (EF_memcpy sz al) (dst :: src :: nil) res s => - if nmem_contains (snd an!!pc) (aaddr approx!!pc dst) sz + if nmem_contains (snd an!!pc) (aaddr_arg approx!!pc dst) sz then instr else Inop s | _ => diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index b998c631..a45869d7 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -262,6 +262,16 @@ Proof. simpl. eapply ma_nextblock; eauto. Qed. +Lemma magree_valid_access: + forall m1 m2 (P: locset) chunk b ofs p, + magree m1 m2 P -> + Mem.valid_access m1 chunk b ofs p -> + Mem.valid_access m2 chunk b ofs p. +Proof. + intros. destruct H0; split; auto. + red; intros. eapply ma_perm; eauto. +Qed. + (** * Properties of the need environment *) Lemma add_need_all_eagree: @@ -547,33 +557,43 @@ Proof. eapply magree_monotone; eauto. intros; apply B; auto. Qed. -(** Annotation arguments *) +(** Builtin arguments and results *) -Lemma transfer_annot_arg_sound: +Lemma eagree_set_res: + forall e1 e2 v1 v2 res ne, + Val.lessdef v1 v2 -> + eagree e1 e2 (kill_builtin_res res ne) -> + eagree (regmap_setres res v1 e1) (regmap_setres res v2 e2) ne. +Proof. + intros. destruct res; simpl in *; auto. + apply eagree_update; eauto. apply vagree_lessdef; auto. +Qed. + +Lemma transfer_builtin_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) -> + eval_builtin_arg ge (fun r => e#r) (Vptr sp Int.zero) m a v -> + forall nv ne1 nm1 ne2 nm2, + transfer_builtin_arg nv (ne1, nm1) a = (ne2, nm2) -> eagree e e' ne2 -> magree m m' (nlive ge sp nm2) -> genv_match bc ge -> bc sp = BCstack -> exists v', - eval_annot_arg ge (fun r => e'#r) (Vptr sp Int.zero) m' a v' - /\ Val.lessdef v v' + eval_builtin_arg ge (fun r => e'#r) (Vptr sp Int.zero) m' a v' + /\ vagree v v' nv /\ eagree e e' ne1 /\ magree m m' (nlive ge sp nm1). Proof. 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. +- exists (Vint n); intuition auto. constructor. apply vagree_same. +- exists (Vlong n); intuition auto. constructor. apply vagree_same. +- exists (Vfloat n); intuition auto. constructor. apply vagree_same. +- exists (Vsingle n); intuition auto. constructor. apply vagree_same. - 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. + exists v'; intuition auto. constructor; auto. apply vagree_lessdef; 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. @@ -583,40 +603,80 @@ Proof. intros (v' & A & B). exists v'; intuition auto. constructor. simpl. unfold Senv.symbol_address; simpl; rewrite FS; auto. + apply vagree_lessdef; 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). +- destruct (transfer_builtin_arg All (ne1, nm1) hi) as [ne' nm'] eqn:TR. + exploit IHeval_builtin_arg2; eauto. intros (vlo' & A & B & C & D). + exploit IHeval_builtin_arg1; eauto. intros (vhi' & P & Q & R & S). exists (Val.longofwords vhi' vlo'); intuition auto. constructor; auto. - apply Val.longofwords_lessdef; auto. + apply vagree_lessdef. + apply Val.longofwords_lessdef; apply lessdef_vagree; auto. Qed. -Lemma transfer_annot_args_sound: +Lemma transfer_builtin_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 -> + eval_builtin_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) -> + transfer_builtin_args (ne1, nm1) al = (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' + eval_builtin_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. +Local Opaque transfer_builtin_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. +- destruct (transfer_builtin_arg All (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). + exploit transfer_builtin_arg_sound; eauto. intros (v1' & A2 & B2 & C2 & D2). exists (v1' :: vs'); intuition auto. constructor; auto. Qed. +Lemma can_eval_builtin_arg: + forall sp e m e' m' P, + magree m m' P -> + forall a v, + eval_builtin_arg ge (fun r => e#r) (Vptr sp Int.zero) m a v -> + exists v', eval_builtin_arg tge (fun r => e'#r) (Vptr sp Int.zero) m' a v'. +Proof. + intros until P; intros MA. + assert (LD: forall chunk addr v, + Mem.loadv chunk m addr = Some v -> + exists v', Mem.loadv chunk m' addr = Some v'). + { + intros. destruct addr; simpl in H; try discriminate. + eapply Mem.valid_access_load. eapply magree_valid_access; eauto. + eapply Mem.load_valid_access; eauto. } + induction 1; try (econstructor; now constructor). +- exploit LD; eauto. intros (v' & A). exists v'; constructor; auto. +- exploit LD; eauto. intros (v' & A). exists v'; constructor. + unfold Senv.symbol_address, Senv.find_symbol. rewrite symbols_preserved. assumption. +- destruct IHeval_builtin_arg1 as (v1' & A1). + destruct IHeval_builtin_arg2 as (v2' & A2). + exists (Val.longofwords v1' v2'); constructor; auto. +Qed. + +Lemma can_eval_builtin_args: + forall sp e m e' m' P, + magree m m' P -> + forall al vl, + eval_builtin_args ge (fun r => e#r) (Vptr sp Int.zero) m al vl -> + exists vl', eval_builtin_args tge (fun r => e'#r) (Vptr sp Int.zero) m' al vl'. +Proof. + induction 2. +- exists (@nil val); constructor. +- exploit can_eval_builtin_arg; eauto. intros (v' & A). + destruct IHlist_forall2 as (vl' & B). + exists (v' :: vl'); constructor; eauto. +Qed. + (** Properties of volatile memory accesses *) Lemma transf_volatile_store: @@ -821,168 +881,166 @@ Ltac UseTransfer := functional induction (transfer_builtin (vanalyze rm f)#pc ef args res ne nm); simpl in *; intros. + (* volatile load *) - assert (LD: Val.lessdef rs#a1 te#a1) by eauto 2 with na. - inv H0. rewrite <- H1 in LD; inv LD. - assert (X: exists tv, volatile_load ge chunk tm b ofs t tv /\ Val.lessdef v tv). + inv H0. inv H6. rename b1 into v1. + destruct (transfer_builtin_arg All + (kill_builtin_res res ne, + nmem_add nm (aaddr_arg (vanalyze rm f) # pc a1) + (size_chunk chunk)) a1) as (ne1, nm1) eqn: TR. + inversion SS; subst. exploit transfer_builtin_arg_sound; eauto. + intros (tv1 & A & B & C & D). + inv H1. simpl in B. inv B. + assert (X: exists tvres, volatile_load ge chunk tm b ofs t tvres /\ Val.lessdef vres tvres). { inv H2. - * exists (Val.load_result chunk v0); split; auto. constructor; auto. + * exists (Val.load_result chunk v); split; auto. constructor; auto. * exploit magree_load; eauto. - exploit aaddr_sound; eauto. intros (bc & A & B & C). + exploit aaddr_arg_sound_1; eauto. rewrite <- AN. intros. intros. eapply nlive_add; eassumption. intros (tv & P & Q). exists tv; split; auto. constructor; auto. } - destruct X as (tv & A & B). + destruct X as (tvres & P & Q). econstructor; split. eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. + constructor. eauto. constructor. eapply external_call_symbols_preserved. - simpl. rewrite <- H4. constructor. eauto. + constructor. simpl. eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. - eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. -+ (* volatile global load *) - inv H0. - assert (X: exists tv, volatile_load ge chunk tm b ofs t tv /\ Val.lessdef v tv). - { - inv H2. - * exists (Val.load_result chunk v0); split; auto. constructor; auto. - * exploit magree_load; eauto. - inv SS. intros. eapply nlive_add; eauto. constructor. apply GE. auto. - intros (tv & P & Q). - exists tv; split; auto. constructor; auto. - } - destruct X as (tv & A & B). - econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved. - simpl. econstructor; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. + apply eagree_set_res; auto. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. + (* volatile store *) - exploit transf_volatile_store. eauto. - instantiate (1 := te#a1). eauto 3 with na. - instantiate (1 := te#a2). eauto 3 with na. - eauto. - intros (EQ & tm' & A & B). subst v. + inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2. + destruct (transfer_builtin_arg (store_argument chunk) + (kill_builtin_res res ne, nm) a2) as (ne2, nm2) eqn: TR2. + destruct (transfer_builtin_arg All (ne2, nm2) a1) as (ne1, nm1) eqn: TR1. + inversion SS; subst. + exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto. + intros (tv1 & A1 & B1 & C1 & D1). + exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto. + intros (tv2 & A2 & B2 & C2 & D2). + exploit transf_volatile_store; eauto. + intros (EQ & tm' & P & Q). subst vres. econstructor; split. eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. + constructor. eauto. constructor. eauto. constructor. eapply external_call_symbols_preserved. simpl; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 3 with na. -+ (* volatile global store *) - rewrite volatile_store_global_charact in H0. destruct H0 as (b & P & Q). - exploit transf_volatile_store. eauto. eauto. - instantiate (1 := te#a1). eauto 2 with na. - eauto. - intros (EQ & tm' & A & B). subst v. - econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved. simpl. - rewrite volatile_store_global_charact. exists b; split; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. + apply eagree_set_res; auto. + (* memcpy *) rewrite e1 in TI. - inv H0. - set (adst := aaddr (vanalyze rm f) # pc dst) in *. - set (asrc := aaddr (vanalyze rm f) # pc src) in *. - exploit magree_loadbytes. eauto. eauto. - exploit aaddr_sound. eauto. symmetry; eexact H2. - intros (bc & A & B & C). - intros. eapply nlive_add; eassumption. + inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2. + set (adst := aaddr_arg (vanalyze rm f) # pc dst) in *. + set (asrc := aaddr_arg (vanalyze rm f) # pc src) in *. + destruct (transfer_builtin_arg All + (kill_builtin_res res ne, + nmem_add (nmem_remove nm adst sz) asrc sz) dst) + as (ne2, nm2) eqn: TR2. + destruct (transfer_builtin_arg All (ne2, nm2) src) as (ne1, nm1) eqn: TR1. + inversion SS; subst. + exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto. + intros (tv1 & A1 & B1 & C1 & D1). + exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto. + intros (tv2 & A2 & B2 & C2 & D2). + inv H1. + exploit magree_loadbytes. eauto. eauto. + intros. eapply nlive_add; eauto. + unfold asrc, vanalyze, rm; rewrite AN; eapply aaddr_arg_sound_1; eauto. intros (tbytes & P & Q). exploit magree_storebytes_parallel. - eapply magree_monotone. eexact MEM. + eapply magree_monotone. eexact D2. instantiate (1 := nlive ge sp0 (nmem_remove nm adst sz)). intros. apply incl_nmem_add; auto. eauto. - instantiate (1 := nlive ge sp0 nm). - exploit aaddr_sound. eauto. symmetry; eexact H1. - intros (bc & A & B & C). - intros. eapply nlive_remove; eauto. - erewrite Mem.loadbytes_length in H10 by eauto. - rewrite nat_of_Z_eq in H10 by omega. auto. + instantiate (1 := nlive ge sp0 nm). + intros. eapply nlive_remove; eauto. + unfold adst, vanalyze, rm; rewrite AN; eapply aaddr_arg_sound_1; eauto. + erewrite Mem.loadbytes_length in H1 by eauto. + rewrite nat_of_Z_eq in H1 by omega. auto. eauto. intros (tm' & A & B). - assert (LD1: Val.lessdef rs#src te#src) by eauto 3 with na. rewrite <- H2 in LD1. - assert (LD2: Val.lessdef rs#dst te#dst) by eauto 3 with na. rewrite <- H1 in LD2. econstructor; split. eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. + constructor. eauto. constructor. eauto. constructor. eapply external_call_symbols_preserved. simpl. - inv LD1. inv LD2. econstructor; eauto. + simpl in B1; inv B1. simpl in B2; inv B2. econstructor; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 3 with na. + apply eagree_set_res; auto. + (* memcpy eliminated *) - rewrite e1 in TI. inv H0. - set (adst := aaddr (vanalyze rm f) # pc dst) in *. - set (asrc := aaddr (vanalyze rm f) # pc src) in *. + rewrite e1 in TI. + inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2. + set (adst := aaddr_arg (vanalyze rm f) # pc dst) in *. + set (asrc := aaddr_arg (vanalyze rm f) # pc src) in *. + inv H1. econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. - apply eagree_set_undef; auto. + destruct res; auto. apply eagree_set_undef; auto. eapply magree_storebytes_left; eauto. - exploit aaddr_sound. eauto. symmetry; eexact H1. + exploit aaddr_arg_sound. eauto. eauto. intros (bc & A & B & C). intros. eapply nlive_contains; eauto. erewrite Mem.loadbytes_length in H0 by eauto. rewrite nat_of_Z_eq in H0 by omega. auto. + (* annot *) - inv H0. + destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. + inversion SS; subst. + exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). + inv H1. econstructor; split. - eapply exec_Ibuiltin; eauto. + eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved. simpl; constructor. eapply eventval_list_match_lessdef; eauto 2 with na. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. -+ (* annot val *) - inv H0. destruct _x; inv H1. destruct _x; inv H4. + apply eagree_set_res; auto. ++ (* annot val *) + destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. + inversion SS; subst. + exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). + inv H1. inv B. inv H6. econstructor; split. eapply exec_Ibuiltin; eauto. + apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved. simpl; constructor. eapply eventval_match_lessdef; eauto 2 with na. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 3 with na. + apply eagree_set_res; auto. ++ (* debug *) + inv H1. + exploit can_eval_builtin_args; eauto. intros (vargs' & A). + econstructor; split. + eapply exec_Ibuiltin; eauto. constructor. + eapply match_succ_states; eauto. simpl; auto. + apply eagree_set_res; auto. + (* all other builtins *) assert ((fn_code tf)!pc = Some(Ibuiltin _x _x0 res pc')). { destruct _x; auto. destruct _x0; auto. destruct _x0; auto. destruct _x0; auto. contradiction. } - clear y TI. + clear y TI. + destruct (transfer_builtin_args (kill_builtin_res res ne, nmem_all) _x0) as (ne1, nm1) eqn:TR. + inversion SS; subst. + exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). exploit external_call_mem_extends; eauto 2 with na. eapply magree_extends; eauto. intros. apply nlive_all. - intros (v' & tm' & A & B & C & D & E). + intros (v' & tm' & P & Q & R & S & T). econstructor; split. - eapply exec_Ibuiltin; eauto. + eapply exec_Ibuiltin; eauto. + apply eval_builtin_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_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 3 with na. + apply eagree_set_res; auto. 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 4f17d59c..98436bf5 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -203,15 +203,21 @@ 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 := +Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_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) + | BA x => BA (sreg ctx x) + | BA_loadstack chunk ofs => BA_loadstack chunk (Int.add ofs (Int.repr ctx.(dstk))) + | BA_addrstack ofs => BA_addrstack (Int.add ofs (Int.repr ctx.(dstk))) + | BA_longofwords hi lo => BA_longofwords (sbuiltinarg ctx hi) (sbuiltinarg ctx lo) | _ => a end. +Definition sbuiltinres (ctx: context) (a: builtin_res reg) : builtin_res reg := + match a with + | BR x => BR (sreg ctx x) + | _ => BR_none + end. + (** The initial context, used to copy the CFG of a toplevel function. *) Definition initcontext (dpc dreg nreg: positive) (sz: Z) := @@ -390,10 +396,7 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit := end | 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)) + (Ibuiltin ef (map (sbuiltinarg ctx) args) (sbuiltinres ctx res) (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 993e0b34..c7cc8d8a 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -400,25 +400,25 @@ Proof. eapply function_ptr_translated; eauto. Qed. -(** Translation of annotation arguments. *) +(** Translation of builtin arguments. *) -Lemma tr_annot_arg: +Lemma tr_builtin_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' + eval_builtin_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v -> + exists v', eval_builtin_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sbuiltinarg 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. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. - 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. @@ -429,30 +429,30 @@ Proof. 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. + exists v'; eauto with barg. - 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. +- destruct IHeval_builtin_arg1 as (v1 & A1 & B1). + destruct IHeval_builtin_arg2 as (v2 & A2 & B2). + econstructor; split. eauto with barg. apply Val.longofwords_inject; auto. Qed. -Lemma tr_annot_args: +Lemma tr_builtin_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' + eval_builtin_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl -> + exists vl', eval_builtin_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sbuiltinarg ctx) al) vl' /\ Val.inject_list F vl vl'. Proof. induction 5; simpl. - exists (@nil val); split; constructor. -- exploit tr_annot_arg; eauto. intros (v1' & A & B). +- exploit tr_builtin_arg; eauto. intros (v1' & A & B). destruct IHlist_forall2 as (vl' & C & D). exists (v1' :: vl'); split; constructor; auto. Qed. @@ -663,6 +663,15 @@ Proof. intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. xomega. Qed. +Lemma match_stacks_inside_set_res: + forall F m m' stk stk' f' ctx sp' rs' res v, + match_stacks_inside F m m' stk stk' f' ctx sp' rs' -> + match_stacks_inside F m m' stk stk' f' ctx sp' (regmap_setres (sbuiltinres ctx res) v rs'). +Proof. + intros. destruct res; simpl; auto. + apply match_stacks_inside_set_reg; auto. +Qed. + (** Preservation by a memory store *) Lemma match_stacks_inside_store: @@ -1064,46 +1073,23 @@ Proof. (* builtin *) exploit tr_funbody_inv; eauto. intros TR; inv TR. - exploit external_call_mem_inject; eauto. - eapply match_stacks_inside_globals; eauto. - instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. - intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]]. - left; econstructor; split. - eapply plus_one. eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - econstructor. - eapply match_stacks_inside_set_reg. - 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_set_reg. eapply agree_regs_incr; eauto. auto. auto. - apply J; 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. - -(* 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 tr_builtin_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 plus_one. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor. + eapply match_stacks_inside_set_res. 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. + auto. + destruct res; simpl; [apply agree_set_reg;auto|idtac|idtac]; 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. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index f7e6c317..161e2a6e 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -313,12 +313,9 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop := context_stack_tailcall ctx f ctx' -> tr_instr ctx pc (Itailcall sg (inr _ id) args) c | tr_builtin: forall ctx pc c ef args res s, - Ple res ctx.(mreg) -> - c!(spc ctx pc) = Some (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) -> + match res with BR r => Ple r ctx.(mreg) | _ => True end -> + c!(spc ctx pc) = Some (Ibuiltin ef (map (sbuiltinarg ctx) args) (sbuiltinres 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 @@ -554,6 +551,8 @@ Proof. red; simpl. subst s2; simpl in *; xomega. red; auto. +(* builtin *) + eapply tr_builtin; eauto. destruct b; eauto. (* return *) destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. (* inlined *) diff --git a/backend/LTL.v b/backend/LTL.v index 8c2749a7..67fb0197 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -44,8 +44,7 @@ Inductive instruction: Type := | Lstore (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) | 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 (annot_arg loc)) + | Lbuiltin (ef: external_function) (args: list (builtin_arg loc)) (res: builtin_res mreg) | Lbranch (s: node) | Lcond (cond: condition) (args: list mreg) (s1 s2: node) | Ljumptable (arg: mreg) (tbl: list node) @@ -239,16 +238,12 @@ Inductive step: state -> trace -> state -> Prop := Mem.free m sp 0 f.(fn_stacksize) = Some m' -> step (Block s f (Vptr sp Int.zero) (Ltailcall sig ros :: bb) rs m) E0 (Callstate s fd rs' m') - | exec_Lbuiltin: forall s f sp ef args res bb rs m t vl rs' m', - external_call' ef ge (reglist rs args) m t vl m' -> - rs' = Locmap.setlist (map R res) vl (undef_regs (destroyed_by_builtin ef) rs) -> + | exec_Lbuiltin: forall s f sp ef args res bb rs m vargs t vres rs' m', + eval_builtin_args ge rs sp m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = Locmap.setres res vres (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 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, step (Block s f sp (Lbranch pc :: bb) rs m) E0 (State s f sp pc rs m) diff --git a/backend/Linear.v b/backend/Linear.v index 5d1fc0d8..8c91a809 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -41,8 +41,7 @@ Inductive instruction: Type := | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction - | Lbuiltin: external_function -> list mreg -> list mreg -> instruction - | Lannot: external_function -> list (annot_arg loc) -> instruction + | Lbuiltin: external_function -> list (builtin_arg loc) -> builtin_res mreg -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -198,17 +197,12 @@ Inductive step: state -> trace -> state -> Prop := step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m) E0 (Callstate s f' rs' m') | exec_Lbuiltin: - forall s f sp rs m ef args res b t vl rs' m', - external_call' ef ge (reglist rs args) m t vl m' -> - rs' = Locmap.setlist (map R res) vl (undef_regs (destroyed_by_builtin ef) rs) -> + forall s f sp rs m ef args res b vargs t vres rs' m', + eval_builtin_args ge rs sp m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = Locmap.setres res vres (undef_regs (destroyed_by_builtin ef) rs) -> 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 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: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) diff --git a/backend/Linearize.v b/backend/Linearize.v index b1102e23..78cdd743 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -187,8 +187,6 @@ Fixpoint linearize_block (b: LTL.bblock) (k: code) : code := Ltailcall sig ros :: k | LTL.Lbuiltin ef args res :: b' => Lbuiltin ef args res :: linearize_block b' k - | LTL.Lannot ef args :: b' => - Lannot ef args :: linearize_block b' k | LTL.Lbranch s :: b' => add_branch s k | LTL.Lcond cond args s1 s2 :: b' => diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 08bcd3f3..dc4d11ea 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -644,14 +644,7 @@ Proof. (* Lbuiltin *) left; econstructor; split. simpl. apply plus_one. eapply exec_Lbuiltin; eauto. - eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - econstructor; eauto. - - (* Lannot *) - left; econstructor; split. simpl. - apply plus_one. eapply exec_Lannot; eauto. - eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply eval_builtin_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 c093b62d..2c8de98e 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -55,6 +55,13 @@ Definition loc_valid (l: loc) : bool := | S _ _ _ => false end. +Fixpoint wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool := + match res with + | BR r => subtype ty (mreg_type r) + | BR_none => true + | BR_longofwords hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo + end. + Definition wt_instr (i: instruction) : bool := match i with | Lgetstack sl ofs ty r => @@ -74,9 +81,8 @@ Definition wt_instr (i: instruction) : bool := | Ltailcall sg ros => zeq (size_arguments sg) 0 | Lbuiltin ef args res => - subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res) - | Lannot ef args => - forallb loc_valid (params_of_annot_args args) + wt_builtin_res (proj_sig_res (ef_sig ef)) res + && forallb loc_valid (params_of_builtin_args args) | _ => true end. @@ -161,6 +167,20 @@ Proof. destruct H. apply IHvl; auto. apply wt_setreg; auto. Qed. +Lemma wt_setres: + forall res ty v rs, + wt_builtin_res ty res = true -> + Val.has_type v ty -> + wt_locset rs -> + wt_locset (Locmap.setres res v rs). +Proof. + induction res; simpl; intros. +- apply wt_setreg; auto. eapply Val.has_subtype; eauto. +- auto. +- InvBooleans. eapply IHres2; eauto. destruct v; exact I. + eapply IHres1; eauto. destruct v; exact I. +Qed. + Lemma wt_find_label: forall f lbl c, wt_function f = true -> @@ -291,12 +311,8 @@ Proof. - (* builtin *) simpl in *; InvBooleans. econstructor; eauto. - apply wt_setlist. - eapply Val.has_subtype_list; eauto. eapply external_call_well_typed'; eauto. + eapply wt_setres; eauto. eapply external_call_well_typed; eauto. apply wt_undef_regs; auto. -- (* annot *) - simpl in *; InvBooleans. - econstructor; eauto. - (* label *) simpl in *. econstructor; eauto. - (* goto *) @@ -362,10 +378,10 @@ Proof. intros. inv H. simpl in WTC; InvBooleans. auto. 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) (params_of_annot_args args) = true. +Lemma wt_state_builtin: + forall s f sp ef args res c rs m, + wt_state (State s f sp (Lbuiltin ef args res :: c) rs m) -> + forallb (loc_valid f) (params_of_builtin_args args) = true. Proof. intros. inv H. simpl in WTC; InvBooleans. auto. Qed. diff --git a/backend/Liveness.v b/backend/Liveness.v index ce1a798a..b8a5f965 100644 --- a/backend/Liveness.v +++ b/backend/Liveness.v @@ -92,9 +92,8 @@ Definition transfer | Itailcall sig ros args => 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 + reg_list_live (params_of_builtin_args args) + (reg_list_dead (params_of_builtin_res res) after) | Icond cond args ifso ifnot => reg_list_live args after | Ijumptable arg tbl => diff --git a/backend/Locations.v b/backend/Locations.v index 5674b93a..4ec24a14 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -377,6 +377,14 @@ Module Locmap. destruct vl; auto. destruct H. rewrite IHll; auto. apply gso; auto. apply Loc.diff_sym; auto. Qed. + Fixpoint setres (res: builtin_res mreg) (v: val) (m: t) : t := + match res with + | BR r => set (R r) v m + | BR_none => m + | BR_longofwords hi lo => + setres lo (Val.loword v) (setres hi (Val.hiword v) m) + end. + End Locmap. (** * Total ordering over locations *) diff --git a/backend/Mach.v b/backend/Mach.v index fe00d42d..08fe7c0a 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -60,8 +60,7 @@ Inductive instruction: Type := | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction - | Mbuiltin: external_function -> list mreg -> list mreg -> instruction - | Mannot: external_function -> list (annot_arg mreg) -> instruction + | Mbuiltin: external_function -> list (builtin_arg mreg) -> builtin_res mreg -> instruction | Mlabel: label -> instruction | Mgoto: label -> instruction | Mcond: condition -> list mreg -> label -> instruction @@ -163,6 +162,13 @@ Fixpoint set_regs (rl: list mreg) (vl: list val) (rs: regset) : regset := | _, _ => rs end. +Fixpoint set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset := + match res with + | BR r => Regmap.set r v rs + | BR_none => rs + | BR_longofwords hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + end. + Definition is_label (lbl: label) (instr: instruction) : bool := match instr with | Mlabel lbl' => if peq lbl lbl' then true else false @@ -328,17 +334,12 @@ Inductive step: state -> trace -> state -> Prop := step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) E0 (Callstate s f' rs m') | exec_Mbuiltin: - forall s f sp rs m ef args res b t vl rs' m', - external_call' ef ge rs##args m t vl m' -> - rs' = set_regs res vl (undef_regs (destroyed_by_builtin ef) rs) -> + forall s f sp rs m ef args res b vargs t vres rs' m', + eval_builtin_args ge rs sp m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = set_res res vres (undef_regs (destroyed_by_builtin ef) rs) -> step (State s f sp (Mbuiltin ef args res :: b) rs m) t (State s f sp b rs' m') - | exec_Mannot: - forall s f sp rs m ef args b vargs 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: forall s fb f sp lbl c rs m c', Genv.find_funct_ptr ge fb = Some (Internal f) -> diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index b54188ca..63fb6bb2 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -219,30 +219,30 @@ let print_file_line_d2 oc pref file line = let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" 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) -> + | BA x -> print_preg oc x + | BA_int n -> fprintf oc "%ld" (camlint_of_coqint n) + | BA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) + | BA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) + | BA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) + | BA_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 -> + | BA_addrstack ofs -> fprintf oc "(%s + %ld)" sp_reg_name (camlint_of_coqint ofs) - | AA_loadglobal(chunk, id, ofs) -> + | BA_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) -> + | BA_addrglobal(id, ofs) -> fprintf oc "(\"%s\" + %ld)" (extern_atom id) (camlint_of_coqint ofs) - | AA_longofwords(hi, lo) -> + | BA_longofwords(hi, lo) -> fprintf oc "(%a * 0x100000000 + %a)" (print_annot print_preg sp_reg_name) hi (print_annot print_preg sp_reg_name) lo @@ -267,7 +267,7 @@ let print_annot_stmt print_preg sp_reg_name oc txt tys args = let print_annot_val print_preg oc txt args = print_annot_text print_preg "<internal error>" oc txt - (List.map (fun r -> AA_base r) args) + (List.map (fun r -> BA r) args) (** Inline assembly *) diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 27936f9b..0f78bc58 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -79,10 +79,9 @@ let print_instruction pp succ = function fprintf pp "tailcall %a" ros fn | Lbuiltin(ef, args, res) -> fprintf pp "%a = %s(%a)" - mregs res (name_of_external ef) mregs args - | Lannot(ef, args) -> - fprintf pp "%s(%a)\n" - (name_of_external ef) (print_annot_args loc) args + (print_builtin_res mreg) res + (name_of_external ef) + (print_builtin_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 8484a5c3..0ce2e87b 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -67,10 +67,9 @@ let print_instruction pp i = fprintf pp "\ttailcall %a\n" ros fn | Mbuiltin(ef, args, res) -> 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) (print_annot_args reg) args + (print_builtin_res reg) res + (name_of_external ef) + (print_builtin_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 ce2275cf..78ce1816 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -72,11 +72,9 @@ let print_instruction pp (pc, i) = ros fn regs args | Ibuiltin(ef, args, res, s) -> 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_builtin_res reg) res + (name_of_external ef) + (print_builtin_args reg) args; print_succ pp s (pc - 1) | Icond(cond, args, s1, s2) -> fprintf pp "if (%a) goto %d else goto %d\n" diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index b9813db0..bb67dc96 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -101,10 +101,9 @@ let print_instruction pp succ = function fprintf pp "tailcall %a(%a)" ros fn vars args | Xbuiltin(ef, args, res) -> fprintf pp "%a = %s(%a)" - vars res (name_of_external ef) vars args - | Xannot(ef, args) -> - fprintf pp "%s(%a)" - (name_of_external ef) (print_annot_args var) args + (print_builtin_res var) res + (name_of_external ef) + (print_builtin_args var) args | Xbranch s -> print_succ pp s succ | Xcond(cond, args, s1, s2) -> diff --git a/backend/RTL.v b/backend/RTL.v index 83761c42..56a5efeb 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -70,13 +70,10 @@ Inductive instruction: Type := | Itailcall: signature -> reg + ident -> list reg -> instruction (** [Itailcall sig fn args] performs a function invocation in tail-call position. *) - | Ibuiltin: external_function -> list reg -> reg -> node -> instruction + | Ibuiltin: external_function -> list (builtin_arg reg) -> builtin_res reg -> node -> instruction (** [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 @@ -253,19 +250,12 @@ Inductive step: state -> trace -> state -> Prop := step (State s f (Vptr stk Int.zero) pc rs m) E0 (Callstate s fd rs##args m') | exec_Ibuiltin: - forall s f sp pc rs m ef args res pc' t v m', + forall s f sp pc rs m ef args res pc' vargs t vres m', (fn_code f)!pc = Some(Ibuiltin ef args res pc') -> - 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 -> + eval_builtin_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') + t (State s f sp pc' (regmap_setres res vres 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) -> @@ -367,16 +357,13 @@ Proof. intros. subst. inv H0. exists s1; auto. inversion H; subst; auto. 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. + exists (State s0 f sp pc' (regmap_setres res vres2 rs) m2). eapply exec_Ibuiltin; 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 *) @@ -411,7 +398,6 @@ 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 @@ -432,8 +418,7 @@ Definition instr_uses (i: instruction) : list reg := | Icall sig (inr id) args res s => args | 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 + | Ibuiltin ef args res s => params_of_builtin_args args | Icond cond args ifso ifnot => args | Ijumptable arg tbl => arg :: nil | Ireturn None => nil @@ -450,8 +435,8 @@ Definition instr_defs (i: instruction) : option reg := | Istore chunk addr args src s => None | 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 + | Ibuiltin ef args res s => + match res with BR r => Some r | _ => None end | Icond cond args ifso ifnot => None | Ijumptable arg tbl => None | Ireturn optarg => None @@ -492,8 +477,9 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := | Icall sig (inr id) args res s => fold_left Pmax args (Pmax res m) | 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 + | Ibuiltin ef args res s => + fold_left Pmax (params_of_builtin_args args) + (fold_left Pmax (params_of_builtin_res res) m) | Icond cond args ifso ifnot => fold_left Pmax args m | Ijumptable arg tbl => Pmax arg m | Ireturn None => m @@ -513,7 +499,7 @@ Proof. { induction l; simpl; intros. auto. apply IHl. xomega. } - destruct i; simpl; try (destruct s0); try (apply X); try xomega. + destruct i; simpl; try (destruct s0); repeat (apply X); try xomega. destruct o; xomega. Qed. @@ -527,7 +513,7 @@ Proof. - apply X. xomega. - apply X. xomega. - destruct s0; apply X; xomega. -- apply X. xomega. +- destruct b; inv H1. apply X. simpl. xomega. Qed. Remark max_reg_instr_uses: diff --git a/backend/RTLgen.v b/backend/RTLgen.v index b1c36513..45ad8e19 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -381,6 +381,47 @@ Definition add_move (rs rd: reg) (nd: node) : mon node := then ret nd else add_instr (Iop Omove (rs::nil) rd nd). +(** Translation of arguments and results of builtins. *) + +Definition exprlist_of_expr_list (l: list expr) : exprlist := + List.fold_right Econs Enil l. + +Fixpoint convert_builtin_arg {A: Type} (a: builtin_arg expr) (rl: list A) : builtin_arg A * list A := + match a with + | BA a => + match rl with + | r :: rs => (BA r, rs) + | nil => (BA_int Int.zero, nil) (**r never happens *) + end + | BA_int n => (BA_int n, rl) + | BA_long n => (BA_long n, rl) + | BA_float n => (BA_float n, rl) + | BA_single n => (BA_single n, rl) + | BA_loadstack chunk ofs => (BA_loadstack chunk ofs, rl) + | BA_addrstack ofs => (BA_addrstack ofs, rl) + | BA_loadglobal chunk id ofs => (BA_loadglobal chunk id ofs, rl) + | BA_addrglobal id ofs => (BA_addrglobal id ofs, rl) + | BA_longofwords hi lo => + let (hi', rl1) := convert_builtin_arg hi rl in + let (lo', rl2) := convert_builtin_arg lo rl1 in + (BA_longofwords hi' lo', rl2) + end. + +Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list A) : list (builtin_arg A) := + match al with + | nil => nil + | a1 :: al => + let (a1', rl1) := convert_builtin_arg a1 rl in + a1' :: convert_builtin_args al rl1 + end. + +Definition convert_builtin_res (map: mapping) (r: builtin_res ident) : mon (builtin_res reg) := + match r with + | BR id => do r <- find_var map id; ret (BR r) + | BR_none => ret BR_none + | _ => error (Errors.msg "RTLgen: bad builtin_res") + end. + (** Translation of an expression. [transl_expr map a rd nd] enriches the current CFG with the RTL instructions necessary to compute the value of CminorSel expression [a], leave its result @@ -413,7 +454,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) do r <- find_letvar map n; add_move r rd nd | Ebuiltin ef al => do rl <- alloc_regs map al; - do no <- add_instr (Ibuiltin ef rl rd nd); + do no <- add_instr (Ibuiltin ef (List.map (@BA reg) rl) (BR rd) nd); transl_exprlist map al rl no | Eexternal id sg al => do rl <- alloc_regs map al; @@ -455,39 +496,6 @@ 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 := @@ -586,15 +594,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do rargs <- alloc_regs map cl; do n1 <- add_instr (Itailcall sig (inr _ id) rargs); transl_exprlist map cl rargs n1 - | Sbuiltin optid ef al => - do rargs <- alloc_regs map al; - 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 + | Sbuiltin res ef args => + let al := exprlist_of_expr_list (params_of_builtin_args args) in do rargs <- alloc_regs map al; - do n1 <- add_instr (Iannot ef (convert_annot_args args rargs) nd); + let args' := convert_builtin_args args rargs in + do res' <- convert_builtin_res map res; + do n1 <- add_instr (Ibuiltin ef args' res' nd); transl_exprlist map al rargs n1 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 40bb5c41..e3373bf9 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -12,6 +12,7 @@ open Datatypes open Camlcoq +open AST open Switch open CminorSel @@ -48,6 +49,10 @@ and size_condexpr = function | CElet(a, c) -> size_expr a + size_condexpr c +let size_exprlist al = List.fold_right (fun a s -> size_expr a + s) al 0 + +let size_builtin_args al = size_exprlist (params_of_builtin_args al) + let rec size_exitexpr = function | XEexit n -> 0 | XEjumptable(arg, tbl) -> 2 + size_expr arg @@ -72,8 +77,8 @@ let rec size_stmt = function 3 + size_eos eos + size_exprs args + length_exprs args | Stailcall(sg, eos, args) -> 3 + size_eos eos + size_exprs args + length_exprs args - | Sbuiltin(optid, ef, args) -> 1 + size_exprs args - | Sannot(txt, args) -> 0 + | Sbuiltin(_, (EF_annot _ | EF_debug _), _) -> 0 + | Sbuiltin(optid, ef, args) -> 1 + size_builtin_args args | Sseq(s1, s2) -> size_stmt s1 + size_stmt s2 | Sifthenelse(ce, s1, s2) -> size_condexpr ce + max (size_stmt s1) (size_stmt s2) diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 02460f67..559ab3a2 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -220,6 +220,22 @@ Proof. Qed. Hint Resolve match_env_update_dest: rtlg. +(** A variant of [match_env_update_var] corresponding to the assignment + of the result of a builtin. *) + +Lemma match_env_update_res: + forall map res v e le tres tv rs, + Val.lessdef v tv -> + map_wf map -> + tr_builtin_res map res tres -> + match_env map e le rs -> + match_env map (set_builtin_res res v e) le (regmap_setres tres tv rs). +Proof. + intros. inv H1; simpl. +- eapply match_env_update_var; eauto. +- auto. +Qed. + (** Matching and [let]-bound variables. *) Lemma match_env_bind_letvar: @@ -677,6 +693,15 @@ Proof. auto. Qed. +Remark eval_builtin_args_trivial: + forall (ge: RTL.genv) (rs: regset) sp m rl, + eval_builtin_args ge (fun r => rs#r) sp m (List.map (@BA reg) rl) rs##rl. +Proof. + induction rl; simpl. +- constructor. +- constructor; auto. constructor. +Qed. + Lemma transl_expr_Ebuiltin_correct: forall le ef al vl v, eval_exprlist ge sp e m le al vl -> @@ -691,7 +716,9 @@ Proof. exists (rs1#rd <- v'); exists tm2. (* Exec *) split. eapply star_right. eexact EX1. + change (rs1#rd <- v') with (regmap_setres (BR rd) v' rs1). eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_trivial. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. reflexivity. @@ -972,7 +999,7 @@ Proof. auto. Qed. -(** Annotation arguments. *) +(** Builtin arguments. *) Lemma eval_exprlist_append: forall le al1 vl1 al2 vl2, @@ -985,54 +1012,54 @@ Proof. - simpl. constructor; eauto. Qed. -Lemma invert_eval_annot_arg: +Lemma invert_eval_builtin_arg: forall a v, - eval_annot_arg ge sp e m a v -> + eval_builtin_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')). + eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_builtin_arg a)) vl + /\ Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v + /\ (forall vl', convert_builtin_arg a (vl ++ vl') = (fst (convert_builtin_arg a vl), vl')). Proof. - induction 1; simpl; econstructor; intuition eauto with evalexpr aarg. + induction 1; simpl; econstructor; intuition eauto with evalexpr barg. constructor. constructor. repeat constructor. Qed. -Lemma invert_eval_annot_args: +Lemma invert_eval_builtin_args: forall al vl, - list_forall2 (eval_annot_arg ge sp e m) al vl -> + list_forall2 (eval_builtin_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. + eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_builtin_args al)) vl' + /\ Events.eval_builtin_args ge (fun v => v) sp m (convert_builtin_args al vl') vl. Proof. induction 1; simpl. - exists (@nil val); split; constructor. -- exploit invert_eval_annot_arg; eauto. intros (vl1 & A & B & C). +- exploit invert_eval_builtin_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: +Lemma transl_eval_builtin_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 -> + Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v -> exists v', - Events.eval_annot_arg ge (fun r => rs#r) sp m (fst (convert_annot_arg a rl)) v' + Events.eval_builtin_arg ge (fun r => rs#r) sp m (fst (convert_builtin_arg a rl)) v' /\ Val.lessdef v v' - /\ Val.lessdef_list (snd (convert_annot_arg a vl)) rs##(snd (convert_annot_arg a rl)). + /\ Val.lessdef_list (snd (convert_builtin_arg a vl)) rs##(snd (convert_builtin_arg a rl)). Proof. induction a; simpl; intros until v; intros LD EV; - try (now (inv EV; econstructor; eauto with aarg)). + try (now (inv EV; econstructor; eauto with barg)). - destruct rl; simpl in LD; inv LD; inv EV; simpl. - econstructor; eauto with aarg. + econstructor; eauto with barg. 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 *. +- destruct (convert_builtin_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *. + destruct (convert_builtin_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *. + destruct (convert_builtin_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *. + destruct (convert_builtin_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). @@ -1042,164 +1069,25 @@ Proof. split; auto. apply Val.longofwords_lessdef; auto. Qed. -Lemma transl_eval_annot_args: +Lemma transl_eval_builtin_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 -> + Events.eval_builtin_args ge (fun v => v) sp m (convert_builtin_args al vl1) vl -> exists vl', - Events.eval_annot_args ge (fun r => rs#r) sp m (convert_annot_args al rl) vl' + Events.eval_builtin_args ge (fun r => rs#r) sp m (convert_builtin_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 *. +- destruct (convert_builtin_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. + exploit transl_eval_builtin_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 *. + destruct (convert_builtin_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 *) @@ -1520,36 +1408,24 @@ Proof. (* builtin *) inv TS. + exploit invert_eval_builtin_args; eauto. intros (vparams & P & Q). exploit transl_exprlist_correct; eauto. intros [rs' [tm' [E [F [G [J K]]]]]]. - edestruct external_call_mem_extends as [tv [tm'' [A [B [C D]]]]]; eauto. - econstructor; split. - left. eapply plus_right. eexact E. - eapply exec_Ibuiltin. eauto. - eapply external_call_symbols_preserved. eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - traceEq. - 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. + exploit transl_eval_builtin_args; eauto. intros (vargs' & U & V). - exploit (@eval_annot_args_lessdef _ ge (fun r => rs'#r) (fun r => rs'#r)); eauto. + exploit (@eval_builtin_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 exec_Ibuiltin. eauto. + eapply eval_builtin_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. + eapply match_env_update_res; eauto. (* seq *) inv TS. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 1ca9faa0..41b5016f 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -727,7 +727,7 @@ Inductive tr_expr (c: code): tr_expr c map pr (Eletvar n) ns nd rd dst | tr_Ebuiltin: forall map pr ef al ns nd rd dst n1 rl, tr_exprlist c map pr al ns n1 rl -> - c!n1 = Some (Ibuiltin ef rl rd nd) -> + c!n1 = Some (Ibuiltin ef (List.map (@BA reg) rl) (BR rd) nd) -> reg_map_ok map rd dst -> ~In rd pr -> tr_expr c map pr (Ebuiltin ef al) ns nd rd dst | tr_Eexternal: forall map pr id sg al ns nd rd dst n1 rl, @@ -807,6 +807,15 @@ Inductive tr_exitexpr (c: code): tr_exitexpr c (add_letvar map r) b n1 nexits -> tr_exitexpr c map (XElet a b) ns nexits. +(** Auxiliary for the compilation of [builtin] statements. *) + +Inductive tr_builtin_res: mapping -> builtin_res ident -> builtin_res reg -> Prop := + | tr_builtin_res_var: forall map id r, + map.(map_vars)!id = Some r -> + tr_builtin_res map (BR id) (BR r) + | tr_builtin_res_none: forall map, + tr_builtin_res map BR_none BR_none. + (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c], starting at node [ns], contains instructions that perform the Cminor statement [stmt]. These instructions branch to node [ncont] if @@ -849,15 +858,11 @@ Inductive tr_stmt (c: code) (map: mapping): tr_exprlist c map nil cl ns n2 rargs -> c!n2 = Some (Itailcall sig (inr _ id) rargs) -> tr_stmt c map (Stailcall sig (inr _ id) cl) ns nd nexits ngoto nret rret - | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 rargs, - tr_exprlist c map nil al ns n1 rargs -> - 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_Sbuiltin: forall res ef args ns nd nexits ngoto nret rret res' n1 rargs, + tr_exprlist c map nil (exprlist_of_expr_list (params_of_builtin_args args)) ns n1 rargs -> + c!n1 = Some (Ibuiltin ef (convert_builtin_args args rargs) res' nd) -> + tr_builtin_res map res res' -> + tr_stmt c map (Sbuiltin res ef args) 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 -> @@ -1208,6 +1213,17 @@ Proof. apply add_letvar_valid; eauto with rtlg. Qed. +Lemma convert_builtin_res_charact: + forall map res s res' s' INCR + (TR: convert_builtin_res map res s = OK res' s' INCR) + (WF: map_valid map s), + tr_builtin_res map res res'. +Proof. + destruct res; simpl; intros; monadInv TR. +- constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto. +- constructor. +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) @@ -1260,10 +1276,7 @@ Proof. (* Sbuiltin *) 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. + eapply convert_builtin_res_charact; eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 8961fc0b..8635ed53 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -65,18 +65,24 @@ 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 := +Definition type_of_builtin_arg (a: builtin_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 + | BA r => env r + | BA_int _ => Tint + | BA_long _ => Tlong + | BA_float _ => Tfloat + | BA_single _ => Tsingle + | BA_loadstack chunk ofs => type_of_chunk chunk + | BA_addrstack ofs => Tint + | BA_loadglobal chunk id ofs => type_of_chunk chunk + | BA_addrglobal id ofs => Tint + | BA_longofwords hi lo => Tlong + end. + +Definition type_of_builtin_res (r: builtin_res reg) : typ := + match r with + | BR r => env r + | _ => Tint end. Inductive wt_instr : instruction -> Prop := @@ -124,15 +130,10 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Itailcall sig ros args) | wt_Ibuiltin: forall ef args res s, - map env args = (ef_sig ef).(sig_args) -> - env res = proj_sig_res (ef_sig ef) -> + map type_of_builtin_arg args = (ef_sig ef).(sig_args) -> + type_of_builtin_res 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 -> @@ -233,27 +234,33 @@ Definition is_move (op: operation) : bool := 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 := +Definition type_builtin_arg (e: S.typenv) (a: builtin_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 + | BA r => S.set e r ty + | BA_int _ => type_expect e ty Tint + | BA_long _ => type_expect e ty Tlong + | BA_float _ => type_expect e ty Tfloat + | BA_single _ => type_expect e ty Tsingle + | BA_loadstack chunk ofs => type_expect e ty (type_of_chunk chunk) + | BA_addrstack ofs => type_expect e ty Tint + | BA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk) + | BA_addrglobal id ofs => type_expect e ty Tint + | BA_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 := +Fixpoint type_builtin_args (e: S.typenv) (al: list (builtin_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 + do e1 <- type_builtin_arg e a1 ty1; type_builtin_args e1 al tyl | _, _ => - Error (msg "annotation arity mismatch") + Error (msg "builtin arity mismatch") + end. + +Definition type_builtin_res (e: S.typenv) (a: builtin_res reg) (ty: typ) : res S.typenv := + match a with + | BR r => S.set e r ty + | _ => type_expect e ty Tint end. Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := @@ -294,11 +301,8 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := | Ibuiltin ef args res s => let sig := ef_sig ef in 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)) + do e1 <- type_builtin_args e args sig.(sig_args); + type_builtin_res e1 res (proj_sig_res sig) | Icond cond args s1 s2 => do x1 <- check_successor s1; do x2 <- check_successor s2; @@ -394,41 +398,57 @@ 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. +Lemma type_builtin_arg_incr: + forall e a ty e' te, type_builtin_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. + unfold type_builtin_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. +Lemma type_builtin_args_incr: + forall a ty e e' te, type_builtin_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. + monadInv H. eapply type_builtin_arg_incr; eauto. +Qed. + +Lemma type_builtin_res_incr: + forall e a ty e' te, type_builtin_res e a ty = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + unfold type_builtin_res; intros; destruct a; inv H; eauto with ty. Qed. -Hint Resolve type_annot_args_incr: ty. +Hint Resolve type_builtin_args_incr type_builtin_res_incr: ty. -Lemma type_annot_arg_sound: +Lemma type_builtin_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. + type_builtin_arg e a ty = OK e' -> S.satisf te e' -> type_of_builtin_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: +Lemma type_builtin_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. + type_builtin_args e al tyl = OK e' -> S.satisf te e' -> List.map (type_of_builtin_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. + eapply type_builtin_arg_sound; eauto with ty. eauto. Qed. +Lemma type_builtin_res_sound: + forall e a ty e' te, + type_builtin_res e a ty = OK e' -> S.satisf te e' -> type_of_builtin_res te a = ty. +Proof. + intros. destruct a; simpl in *. + eapply S.set_sound; eauto. + symmetry; eapply type_expect_sound; eauto. + symmetry; eapply type_expect_sound; 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. @@ -497,12 +517,8 @@ Proof. apply tailcall_is_possible_correct; auto. - (* builtin *) constructor. - 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. + eapply type_builtin_args_sound; eauto with ty. + eapply type_builtin_res_sound; eauto. eauto with ty. - (* cond *) constructor. @@ -590,27 +606,38 @@ Proof. unfold type_expect; intros. rewrite dec_eq_true; auto. Qed. -Lemma type_annot_arg_complete: +Lemma type_builtin_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'. + exists e', type_builtin_arg e a (type_of_builtin_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: +Lemma type_builtin_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'. + exists e', type_builtin_args e al (List.map (type_of_builtin_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 (type_builtin_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_builtin_res_complete: + forall te a e, + S.satisf te e -> + exists e', type_builtin_res e a (type_of_builtin_res te a) = OK e' /\ S.satisf te e'. +Proof. + intros. destruct a; simpl. + apply S.set_complete; auto. + exists e; auto. + exists e; auto. +Qed. + Lemma type_instr_complete: forall te e i, S.satisf te e -> @@ -662,15 +689,12 @@ Proof. exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl. intros; apply H3; auto. - (* builtin *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. - 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. + exploit type_builtin_args_complete; eauto. instantiate (1 := args). intros [e1 [A B]]. + exploit type_builtin_res_complete; eauto. instantiate (1 := res). intros [e2 [C D]]. + exists e2; split; auto. + rewrite check_successor_complete by auto. simpl. + rewrite <- H0; rewrite A; simpl. + rewrite <- H1; auto. - (* cond *) exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. exists e1; split; auto. @@ -772,6 +796,15 @@ Proof. split. apply H. apply IHrl. Qed. +Lemma wt_regset_setres: + forall env rs v res, + wt_regset env rs -> + Val.has_type v (type_of_builtin_res env res) -> + wt_regset env (regmap_setres res v rs). +Proof. + intros. destruct res; simpl in *; auto. apply wt_regset_assign; auto. +Qed. + Lemma wt_init_regs: forall env rl args, Val.has_type_list args (List.map env rl) -> @@ -812,11 +845,11 @@ Lemma wt_exec_Ibuiltin: wt_instr f env (Ibuiltin ef args res s) -> external_call ef ge vargs m t vres m' -> wt_regset env rs -> - wt_regset env (rs#res <- vres). + wt_regset env (regmap_setres res vres rs). Proof. intros. inv H. - eapply wt_regset_assign; eauto. - rewrite H7; eapply external_call_well_typed; eauto. + eapply wt_regset_setres; eauto. + rewrite H7. eapply external_call_well_typed; eauto. Qed. Lemma wt_instr_at: @@ -914,8 +947,6 @@ 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 aa4efc53..b901076e 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -114,24 +114,60 @@ 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 -> +let rec convert_builtin_arg tyenv = function + | BA 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)) + | Tlong -> BA_longofwords(BA(V(r, Tint)), BA(V(twin_reg r, Tint))) + | ty -> BA(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) - + | BA_int n -> BA_int n + | BA_long n -> BA_long n + | BA_float n -> BA_float n + | BA_single n -> BA_single n + | BA_loadstack(chunk, ofs) -> BA_loadstack(chunk, ofs) + | BA_addrstack(ofs) -> BA_addrstack(ofs) + | BA_loadglobal(chunk, id, ofs) -> BA_loadglobal(chunk, id, ofs) + | BA_addrglobal(id, ofs) -> BA_addrglobal(id, ofs) + | BA_longofwords(hi, lo) -> + BA_longofwords(convert_builtin_arg tyenv hi, convert_builtin_arg tyenv lo) + +let convert_builtin_res tyenv = function + | BR r -> + begin match tyenv r with + | Tlong -> BR_longofwords(BR(V(r, Tint)), BR(V(twin_reg r, Tint))) + | ty -> BR(V(r, ty)) + end + | BR_none -> BR_none + | BR_longofwords _ -> assert false + +let rec constrain_builtin_arg a cl = + match a, cl with + | BA x, None :: cl' -> (a, cl') + | BA x, Some mr :: cl' -> (BA (L(R mr)), cl') + | BA_longofwords(hi, lo), _ -> + let (hi', cl1) = constrain_builtin_arg hi cl in + let (lo', cl2) = constrain_builtin_arg lo cl1 in + (BA_longofwords(hi', lo'), cl2) + | _, _ -> (a, cl) + +let rec constrain_builtin_args al cl = + match al with + | [] -> ([], cl) + | a :: al -> + let (a', cl1) = constrain_builtin_arg a cl in + let (al', cl2) = constrain_builtin_args al cl1 in + (a' :: al', cl2) + +let rec constrain_builtin_res a cl = + match a, cl with + | BR x, None :: cl' -> (a, cl') + | BR x, Some mr :: cl' -> (BR (L(R mr)), cl') + | BR_longofwords(hi, lo), _ -> + let (hi', cl1) = constrain_builtin_res hi cl in + let (lo', cl2) = constrain_builtin_res lo cl1 in + (BR_longofwords(hi', lo'), cl2) + | _, _ -> (a, cl) + (* 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. @@ -206,12 +242,14 @@ let block_of_RTL_instr funsig tyenv = function [Xtailcall(sg, sum_left_map (vreg tyenv) ros, args')] | RTL.Ibuiltin(ef, args, res, s) -> let (cargs, cres) = mregs_for_builtin ef in - let args1 = expand_regs tyenv args and res1 = expand_regs tyenv [res] in - 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] + let args1 = List.map (convert_builtin_arg tyenv) args + and res1 = convert_builtin_res tyenv res in + let (args2, _) = constrain_builtin_args args1 cargs + and (res2, _) = constrain_builtin_res res1 cres in + movelist (params_of_builtin_args args1) (params_of_builtin_args args2) + (Xbuiltin(ef, args2, res2) :: + movelist (params_of_builtin_res res2) (params_of_builtin_res res1) + [Xbranch s]) | RTL.Icond(cond, args, s1, s2) -> [Xcond(cond, vregs tyenv args, s1, s2)] | RTL.Ijumptable(arg, tbl) -> @@ -249,14 +287,24 @@ let function_of_RTL_function f tyenv = 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 = + +let rec vset_addarg a after = match a with - | AA_base v -> VSet.add v after - | AA_longofwords(hi, lo) -> vset_addannot hi (vset_addannot lo after) + | BA v -> VSet.add v after + | BA_longofwords(hi, lo) -> vset_addarg hi (vset_addarg lo after) | _ -> after +let vset_addargs al after = List.fold_right vset_addarg al after + +let rec vset_removeres r after = + match r with + | BR v -> VSet.remove v after + | BR_none -> after + | BR_longofwords(hi, lo) -> vset_removeres hi (vset_removeres lo after) + let live_before instr after = match instr with | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) -> @@ -279,10 +327,10 @@ let live_before instr after = vset_addlist args (vset_addros ros (vset_removelist res after)) | Xtailcall(sg, ros, args) -> vset_addlist args (vset_addros ros VSet.empty) + | Xbuiltin(EF_debug _, args, res) -> + vset_removeres res after | Xbuiltin(ef, args, res) -> - vset_addlist args (vset_removelist res after) - | Xannot(ef, args) -> - List.fold_right vset_addannot args after + vset_addargs args (vset_removeres res after) | Xbranch s -> after | Xcond(cond, args, s1, s2) -> @@ -330,6 +378,7 @@ let pair_block_live blk after = (**************** Dead code elimination **********************) (* Eliminate pure instructions whose results are not used later. *) +(* Also: remove dead registers from debug annotations. *) let rec dce_parmove srcs dsts after = match srcs, dsts with @@ -341,6 +390,12 @@ let rec dce_parmove srcs dsts after = else (srcs', dsts') | _, _ -> assert false +let rec keep_builtin_arg after = function + | BA v -> VSet.mem v after + | BA_longofwords(hi, lo) -> + keep_builtin_arg after hi && keep_builtin_arg after lo + | _ -> true + let dce_instr instr after k = match instr with | Xmove(src, dst) -> @@ -361,6 +416,9 @@ let dce_instr instr after k = if VSet.mem dst after then instr :: k else k + | Xbuiltin(EF_debug _ as ef, args, res) -> + let across = vset_removeres res after in + Xbuiltin(ef, List.filter (keep_builtin_arg across) args, res) :: k | _ -> instr :: k @@ -455,17 +513,20 @@ let spill_costs f = charge_ros 10 vos | Xbuiltin(ef, args, res) -> begin match ef with - | EF_vstore _ | EF_vstore_global _ | EF_memcpy _ -> + | EF_annot _ | EF_debug _ -> + () + | EF_vstore _ | EF_memcpy _ -> (* result is not used but should not be spilled *) - charge_list 10 1 args; charge_list max_int 0 res + charge_list 10 1 (params_of_builtin_args args); + charge_list max_int 0 (params_of_builtin_res res) | EF_annot_val _ -> (* like a move *) - charge_list 1 1 args; charge_list 1 1 res + charge_list 1 1 (params_of_builtin_args args); + charge_list 1 1 (params_of_builtin_res res) | _ -> - charge_list 10 1 args; charge_list 10 1 res + charge_list 10 1 (params_of_builtin_args args); + charge_list 10 1 (params_of_builtin_res res) end - | Xannot(ef, args) -> - () | Xbranch _ -> () | Xcond(cond, args, _, _) -> charge_list 10 1 args @@ -575,28 +636,28 @@ let add_interfs_instr g instr live = () | Xbuiltin(ef, args, res) -> (* Interferences with live across *) - let across = vset_removelist res live in - List.iter (add_interfs_live g across) res; + let across = vset_removeres res live in + let vres = params_of_builtin_res res in + List.iter (add_interfs_live g across) vres; (* All results must be pairwise different *) - add_interfs_pairwise g res; + add_interfs_pairwise g vres; add_interfs_destroyed g across (destroyed_by_builtin ef); begin match ef, args, res with - | EF_annot_val _, [arg], [res] -> + | EF_annot_val _, [BA arg], BR res -> (* like a move *) IRC.add_pref g arg res | EF_inline_asm(txt, sg, clob), _, _ -> + let vargs = params_of_builtin_args args in (* clobbered regs interfere with res and args for GCC compatibility *) List.iter (fun c -> match Machregs.register_by_name c with | None -> () | Some mr -> - add_interfs_list_mreg g args mr; - if sg.sig_res <> None then add_interfs_list_mreg g res mr) + add_interfs_list_mreg g vargs mr; + add_interfs_list_mreg g vres mr) clob | _ -> () end - | Xannot(ef, args) -> - () | Xbranch s -> () | Xcond(cond, args, s1, s2) -> @@ -671,10 +732,11 @@ let tospill_instr alloc instr ts = addros_tospill alloc vos ts | Xtailcall(sg, vos, args) -> addros_tospill alloc vos ts - | Xbuiltin(ef, args, res) -> - addlist_tospill alloc args (addlist_tospill alloc res ts) - | Xannot(ef, args) -> + | Xbuiltin((EF_annot _ | EF_debug _), _, _) -> ts + | Xbuiltin(ef, args, res) -> + addlist_tospill alloc (params_of_builtin_args args) + (addlist_tospill alloc (params_of_builtin_res res) ts) | Xbranch s -> ts | Xcond(cond, args, s1, s2) -> @@ -734,6 +796,23 @@ let rec reload_vars tospill eqs vl = let (ts, cs, eqs2) = reload_vars tospill eqs1 vs in (t1 :: ts, c1 @ cs, eqs2) +let rec reload_arg tospill eqs = function + | BA v -> + let (t, c1, eqs1) = reload_var tospill eqs v in + (BA t, c1, eqs1) + | BA_longofwords(hi, lo) -> + let (hi', c1, eqs1) = reload_arg tospill eqs hi in + let (lo', c2, eqs2) = reload_arg tospill eqs1 lo in + (BA_longofwords(hi', lo'), c1 @ c2, eqs2) + | a -> (a, [], eqs) + +let rec reload_args tospill eqs = function + | [] -> ([], [], eqs) + | a1 :: al -> + let (t1, c1, eqs1) = reload_arg tospill eqs a1 in + let (tl, cl, eqs2) = reload_args tospill eqs1 al in + (t1 :: tl, c1 @ cl, eqs2) + let save_var tospill eqs v = if not (VSet.mem v tospill) then (v, [], kill v eqs) @@ -742,13 +821,16 @@ let save_var tospill eqs v = (t, [Xspill(t, v)], add v t (kill v eqs)) end -let rec save_vars tospill eqs vl = - match vl with - | [] -> ([], [], eqs) - | v1 :: vs -> - let (t1, c1, eqs1) = save_var tospill eqs v1 in - let (ts, cs, eqs2) = save_vars tospill eqs1 vs in - (t1 :: ts, c1 @ cs, eqs2) +let rec save_res tospill eqs = function + | BR v -> + let (t, c1, eqs1) = save_var tospill eqs v in + (BR t, c1, eqs1) + | BR_none -> + (BR_none, [], eqs) + | BR_longofwords(hi, lo) -> + let (hi', c1, eqs1) = save_res tospill eqs hi in + let (lo', c2, eqs2) = save_res tospill eqs1 lo in + (BR_longofwords(hi', lo'), c1 @ c2, eqs2) (* Trimming equations when we have too many or when they are too old. The goal is to limit the live range of unspillable temporaries. @@ -833,12 +915,12 @@ let spill_instr tospill eqs instr = (c1 @ [Xtailcall(sg, Coq_inl v', args)], []) | Xtailcall(sg, Coq_inr id, args) -> ([instr], []) + | Xbuiltin((EF_annot _ | EF_debug _), args, res) -> + ([instr], eqs) | Xbuiltin(ef, args, res) -> - let (args', c1, eqs1) = reload_vars tospill eqs args in - let (res', c2, eqs2) = save_vars tospill eqs1 res in + let (args', c1, eqs1) = reload_args tospill eqs args in + let (res', c2, eqs2) = save_res 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) -> @@ -977,9 +1059,8 @@ let transl_instr alloc instr k = | Xtailcall(sg, vos, args) -> LTL.Ltailcall(sg, mros_of alloc vos) :: [] | Xbuiltin(ef, args, res) -> - 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 + LTL.Lbuiltin(ef, List.map (AST.map_builtin_arg alloc) args, + AST.map_builtin_res (mreg_of alloc) res) :: k | Xbranch s -> LTL.Lbranch s :: [] | Xcond(cond, args, s1, s2) -> diff --git a/backend/Registers.v b/backend/Registers.v index 47e10fa4..20532e8c 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -22,6 +22,7 @@ Require Import AST. Require Import Maps. Require Import Ordered. Require FSetAVL. +Require Import Values. Definition reg: Type := positive. @@ -53,10 +54,45 @@ Definition regmap_optset | Some r => Regmap.set r v rs end. +Definition regmap_setres + (A: Type) (res: builtin_res reg) (v: A) (rs: Regmap.t A) : Regmap.t A := + match res with + | BR r => Regmap.set r v rs + | _ => rs + end. + Notation "a # b" := (Regmap.get b a) (at level 1). Notation "a ## b" := (List.map (fun r => Regmap.get r a) b) (at level 1). Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level). +(** Pointwise "less defined than" relation between register maps. *) + +Definition regs_lessdef (rs1 rs2: Regmap.t val) : Prop := + forall r, Val.lessdef (rs1#r) (rs2#r). + +Lemma regs_lessdef_regs: + forall rs1 rs2, regs_lessdef rs1 rs2 -> + forall rl, Val.lessdef_list rs1##rl rs2##rl. +Proof. + induction rl; constructor; auto. +Qed. + +Lemma set_reg_lessdef: + forall r v1 v2 rs1 rs2, + Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2). +Proof. + intros; red; intros. repeat rewrite Regmap.gsspec. + destruct (peq r0 r); auto. +Qed. + +Lemma set_res_lessdef: + forall res v1 v2 rs1 rs2, + Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> + regs_lessdef (regmap_setres res v1 rs1) (regmap_setres res v2 rs2). +Proof. + intros. destruct res; simpl; auto. apply set_reg_lessdef; auto. +Qed. + (** Sets of registers *) Module Regset := FSetAVL.Make(OrderedPositive). diff --git a/backend/Renumber.v b/backend/Renumber.v index 634fe56a..0a2c2f12 100644 --- a/backend/Renumber.v +++ b/backend/Renumber.v @@ -48,7 +48,6 @@ 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 09faa131..33d6aafa 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -198,13 +198,7 @@ Proof. (* builtin *) econstructor; split. eapply exec_Ibuiltin; eauto. - 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 eval_builtin_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. diff --git a/backend/Selection.v b/backend/Selection.v index ae9da0a7..2e631ad2 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -34,6 +34,7 @@ Require Import CminorSel. Require Import SelectOp. Require Import SelectDiv. Require Import SelectLong. +Require Machregs. Local Open Scope cminorsel_scope. Local Open Scope error_monad_scope. @@ -203,21 +204,27 @@ 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 +(** Builtin arguments and results *) + +Definition sel_builtin_arg + (e: Cminor.expr) (c: builtin_arg_constraint): AST.builtin_arg expr := + let e' := sel_expr e in + let ba := builtin_arg e' in + if builtin_arg_ok ba c then ba else BA e'. + +Fixpoint sel_builtin_args + (el: list Cminor.expr) + (cl: list builtin_arg_constraint): list (AST.builtin_arg expr) := + match el with + | nil => nil + | e :: el => + sel_builtin_arg e (List.hd OK_default cl) :: sel_builtin_args el (List.tl cl) 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) +Definition sel_builtin_res (optid: option ident) : builtin_res ident := + match optid with + | None => BR_none + | Some id => BR id end. (** Conversion of Cminor [switch] statements to decision trees. *) @@ -277,12 +284,13 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := OK (match classify_call ge fn with | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) - | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args) + | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)) end) | Cminor.Sbuiltin optid ef args => - OK (if builtin_is_annot ef optid - then Sannot ef (List.map sel_annot_arg args) - else Sbuiltin optid ef (sel_exprlist args)) + OK (Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args (Machregs.builtin_constraints ef))) | 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 d7b1e675..1d2f2b3a 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -598,45 +598,47 @@ Proof. exists (v1' :: vl'); split; auto. constructor; eauto. Qed. -Lemma sel_annot_arg_correct: - forall sp e e' m m', +Lemma sel_builtin_arg_correct: + forall sp e e' m m' a v c, 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' + CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) 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: + intros. unfold sel_builtin_arg. + exploit sel_expr_correct; eauto. intros (v1 & A & B). + exists v1; split; auto. + destruct (builtin_arg_ok (builtin_arg (sel_expr a)) c). + apply eval_builtin_arg; eauto. + constructor; auto. +Qed. + +Lemma sel_builtin_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 -> + forall cl, exists vl', - list_forall2 (CminorSel.eval_annot_arg tge sp e' m') - (List.map sel_annot_arg al) + list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') + (sel_builtin_args al cl) vl' /\ Val.lessdef_list vl vl'. Proof. - induction 3; simpl. + induction 3; intros; 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. +- exploit sel_builtin_arg_correct; eauto. intros (v1' & A & B). + edestruct IHeval_exprlist as (vl' & C & D). + exists (v1' :: vl'); split; auto. constructor; eauto. +Qed. + +Lemma sel_builtin_res_correct: + forall oid v e v' e', + env_lessdef e e' -> Val.lessdef v v' -> + env_lessdef (set_optvar oid v e) (set_builtin_res (sel_builtin_res oid) v' e'). +Proof. + intros. destruct oid; simpl; auto. apply set_var_lessdef; auto. Qed. (** Semantic preservation for functions and statements. *) @@ -687,10 +689,10 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (LDA: Val.lessdef_list args args') (LDE: env_lessdef e e') (ME: Mem.extends m m') - (EA: eval_exprlist tge sp e' m' nil al args'), + (EA: list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') al args'), match_states (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) - (State f' (Sbuiltin optid ef al) k' sp e' m') + (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m') | match_builtin_2: forall v v' optid f sp e k m f' e' m' k' (TF: sel_function ge f = OK f') (MC: match_cont k k') @@ -699,7 +701,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (ME: Mem.extends m m'), match_states (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m) - (State f' Sskip k' sp (set_optvar optid v' e') m'). + (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m'). Remark call_cont_commut: forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k'). @@ -724,8 +726,6 @@ 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] | ]; @@ -790,11 +790,11 @@ Proof. eapply eval_store; eauto. constructor; auto. - (* Scall *) - exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit classify_call_correct; eauto. destruct (classify_call ge a) as [ | id | ef]. + (* indirect *) exploit sel_expr_correct; eauto. intros [vf' [A B]]. + exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit functions_translated; eauto. intros (fd' & U & V). left; econstructor; split. econstructor; eauto. econstructor; eauto. @@ -802,6 +802,7 @@ Proof. constructor; auto. constructor; auto. + (* direct *) intros [b [U V]]. + exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit functions_translated; eauto. intros (fd' & X & Y). left; econstructor; split. econstructor; eauto. @@ -809,7 +810,8 @@ Proof. apply sig_function_translated; auto. constructor; auto. constructor; auto. + (* turned into Sbuiltin *) - intros EQ. subst fd. + intros EQ. subst fd. + exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]]. right; split. simpl. omega. split. auto. econstructor; eauto. - (* Stailcall *) @@ -827,32 +829,13 @@ 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 sel_builtin_args_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. apply set_optvar_lessdef; auto. + constructor; auto. apply sel_builtin_res_correct; auto. - (* Seq *) left; econstructor; split. constructor. constructor; auto. constructor; auto. @@ -942,8 +925,8 @@ Proof. econstructor. constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* return of an external call turned into a Sbuiltin *) - right; split. simpl; omega. split. auto. constructor; auto. - destruct optid; simpl; auto. apply set_var_lessdef; auto. + right; split. simpl; omega. split. auto. constructor; auto. + apply sel_builtin_res_correct; auto. Qed. Lemma sel_initial_states: diff --git a/backend/Splitting.ml b/backend/Splitting.ml index 53600c98..97b26a50 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -162,9 +162,8 @@ let ren_instr f maps pc i = | Itailcall(sg, ros, args) -> 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) + Ibuiltin(ef, List.map (AST.map_builtin_arg (ren_reg before)) args, + AST.map_builtin_res (ren_reg after) res, 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 21cf6b73..caf0ae59 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -128,26 +128,26 @@ Definition transl_op (fe: frame_env) (op: operation) := Definition transl_addr (fe: frame_env) (addr: addressing) := shift_stack_addressing (Int.repr fe.(fe_stack_data)) addr. -(** Translation of an annotation argument. *) +(** Translation of a builtin argument. *) -Fixpoint transl_annot_arg (fe: frame_env) (a: annot_arg loc) : annot_arg mreg := +Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_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) + | BA (R r) => BA r + | BA (S Local ofs ty) => + BA_loadstack (chunk_of_type ty) (Int.repr (offset_of_index fe (FI_local ofs ty))) + | BA (S _ _ _) => BA_int Int.zero (**r never happens *) + | BA_int n => BA_int n + | BA_long n => BA_long n + | BA_float n => BA_float n + | BA_single n => BA_single n + | BA_loadstack chunk ofs => + BA_loadstack chunk (Int.add ofs (Int.repr fe.(fe_stack_data))) + | BA_addrstack ofs => + BA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data))) + | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs + | BA_addrglobal id ofs => BA_addrglobal id ofs + | BA_longofwords hi lo => + BA_longofwords (transl_builtin_arg fe hi) (transl_builtin_arg fe lo) end. (** Translation of a Linear instruction. Prepends the corresponding @@ -192,9 +192,7 @@ Definition transl_instr restore_callee_save fe (Mtailcall sig ros :: k) | Lbuiltin ef args dst => - Mbuiltin ef args dst :: k - | Lannot ef args => - Mannot ef (map (transl_annot_arg fe) args) :: k + Mbuiltin ef (map (transl_builtin_arg fe) args) dst :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 7f41512e..dce49432 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -734,6 +734,20 @@ Proof. apply IHrl; auto. apply agree_regs_set_reg; auto. Qed. +Lemma agree_regs_set_res: + forall j res v v' ls rs, + agree_regs j ls rs -> + Val.inject j v v' -> + agree_regs j (Locmap.setres res v ls) (set_res res v' rs). +Proof. + induction res; simpl; intros. +- apply agree_regs_set_reg; auto. +- auto. +- apply IHres2. apply IHres1. auto. + apply Val.hiword_inject; auto. + apply Val.loword_inject; auto. +Qed. + Lemma agree_regs_exten: forall j ls rs ls' rs', agree_regs j ls rs -> @@ -811,6 +825,18 @@ Proof. eapply agree_frame_set_reg; eauto. Qed. +Lemma agree_frame_set_res: + forall j ls0 m sp m' sp' parent ra res v ls, + agree_frame j ls ls0 m sp m' sp' parent ra -> + (forall r, In r (params_of_builtin_res res) -> mreg_within_bounds b r) -> + agree_frame j (Locmap.setres res v ls) ls0 m sp m' sp' parent ra. +Proof. + induction res; simpl; intros. +- eapply agree_frame_set_reg; eauto. +- auto. +- apply IHres2; auto using in_or_app. +Qed. + Lemma agree_frame_undef_regs: forall j ls0 m sp m' sp' parent ra regs ls, agree_frame j ls ls0 m sp m' sp' parent ra -> @@ -2375,9 +2401,9 @@ Qed. End EXTERNAL_ARGUMENTS. -(** Preservation of the arguments to an annotation. *) +(** Preservation of the arguments to a builtin. *) -Section ANNOT_ARGUMENTS. +Section BUILTIN_ARGUMENTS. Variable f: Linear.function. Let b := function_bounds f. @@ -2395,67 +2421,67 @@ Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent retaddr. Hypothesis MINJ: Mem.inject j m m'. Hypothesis GINJ: meminj_preserves_globals ge j. -Lemma transl_annot_arg_correct: +Lemma transl_builtin_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) -> + eval_builtin_arg ge ls (Vptr sp Int.zero) m a v -> + (forall l, In l (params_of_builtin_arg a) -> loc_valid f l = true) -> + (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_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' + eval_builtin_arg ge rs (Vptr sp' Int.zero) m' (transl_builtin_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. + + exists (rs r); auto with barg. + 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. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. - 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. +- econstructor; split; eauto with barg. 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. + exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with barg. +- econstructor; split; eauto with barg. 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. +- destruct IHeval_builtin_arg1 as (v1 & A1 & B1); auto using in_or_app. + destruct IHeval_builtin_arg2 as (v2 & A2 & B2); auto using in_or_app. + exists (Val.longofwords v1 v2); split; auto with barg. apply Val.longofwords_inject; auto. Qed. -Lemma transl_annot_args_correct: +Lemma transl_builtin_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) -> + eval_builtin_args ge ls (Vptr sp Int.zero) m al vl -> + (forall l, In l (params_of_builtin_args al) -> loc_valid f l = true) -> + (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_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' + eval_builtin_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_builtin_arg fe) al) vl' /\ Val.inject_list 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 transl_builtin_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. +End BUILTIN_ARGUMENTS. (** The proof of semantic preservation relies on simulation diagrams of the following form: @@ -2712,47 +2738,26 @@ Proof. apply zero_size_arguments_tailcall_possible. eapply wt_state_tailcall; eauto. - (* Lbuiltin *) - exploit external_call_mem_inject'; eauto. - eapply match_stacks_preserves_globals; eauto. - eapply agree_reglist; eauto. - intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]]. - econstructor; split. - apply plus_one. econstructor; eauto. - eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - econstructor; eauto with coqlib. - inversion H; inversion A; subst. - 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. - apply agree_regs_set_regs; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto. - apply agree_frame_set_regs; auto. apply agree_frame_undef_regs; auto. - 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 agree_valid_mach; eauto. - -- (* Lannot *) - exploit transl_annot_args_correct; eauto. + destruct BOUND as [BND1 BND2]. + exploit transl_builtin_args_correct; eauto. eapply match_stacks_preserves_globals; eauto. - rewrite <- forallb_forall. eapply wt_state_annot; eauto. + rewrite <- forallb_forall. eapply wt_state_builtin; eauto. intros [vargs' [P Q]]. exploit external_call_mem_inject; eauto. eapply match_stacks_preserves_globals; eauto. intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]]. econstructor; split. apply plus_one. econstructor; eauto. - eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. + eapply eval_builtin_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. 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. + apply agree_regs_set_res; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto. eapply agree_frame_inject_incr; eauto. + apply agree_frame_set_res; auto. apply agree_frame_undef_regs; auto. apply agree_frame_extcall_invariant with m m'0; auto. eapply external_call_valid_block; eauto. intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index bd9b227f..1c25d244 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -199,33 +199,15 @@ Qed. relation between values and between memory states. We need to extend it pointwise to register states. *) -Definition regset_lessdef (rs rs': regset) : Prop := - forall r, Val.lessdef (rs#r) (rs'#r). - -Lemma regset_get_list: - forall rs rs' l, - regset_lessdef rs rs' -> Val.lessdef_list (rs##l) (rs'##l). -Proof. - induction l; simpl; intros; constructor; auto. -Qed. - -Lemma regset_set: - forall rs rs' v v' r, - regset_lessdef rs rs' -> Val.lessdef v v' -> - regset_lessdef (rs#r <- v) (rs'#r <- v'). -Proof. - intros; red; intros. repeat rewrite PMap.gsspec. destruct (peq r0 r); auto. -Qed. - -Lemma regset_init_regs: +Lemma regs_lessdef_init_regs: forall params vl vl', Val.lessdef_list vl vl' -> - regset_lessdef (init_regs vl params) (init_regs vl' params). + regs_lessdef (init_regs vl params) (init_regs vl' params). Proof. induction params; intros. simpl. red; intros. rewrite Regmap.gi. constructor. simpl. inv H. red; intros. rewrite Regmap.gi. constructor. - apply regset_set. auto. auto. + apply set_reg_lessdef. auto. auto. Qed. (** * Proof of semantic preservation *) @@ -278,7 +260,7 @@ Qed. Lemma find_function_translated: forall ros rs rs' f, find_function ge ros rs = Some f -> - regset_lessdef rs rs' -> + regs_lessdef rs rs' -> find_function tge ros rs' = Some (transf_fundef f). Proof. intros until f; destruct ros; simpl. @@ -331,7 +313,7 @@ Inductive match_stackframes: list stackframe -> list stackframe -> Prop := match_stackframes nil nil | match_stackframes_normal: forall stk stk' res sp pc rs rs' f, match_stackframes stk stk' -> - regset_lessdef rs rs' -> + regs_lessdef rs rs' -> match_stackframes (Stackframe res f (Vptr sp Int.zero) pc rs :: stk) (Stackframe res (transf_function f) (Vptr sp Int.zero) pc rs' :: stk') @@ -352,7 +334,7 @@ Inductive match_states: state -> state -> Prop := | match_states_normal: forall s sp pc rs m s' rs' m' f (STACKS: match_stackframes s s') - (RLD: regset_lessdef rs rs') + (RLD: regs_lessdef rs rs') (MLD: Mem.extends m m'), match_states (State s f (Vptr sp Int.zero) pc rs m) (State s' (transf_function f) (Vptr sp Int.zero) pc rs' m') @@ -437,13 +419,13 @@ Proof. (* op *) TransfInstr. - assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. exploit eval_operation_lessdef; eauto. intros [v' [EVAL' VLD]]. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'); split. eapply exec_Iop; eauto. rewrite <- EVAL'. apply eval_operation_preserved. exact symbols_preserved. - econstructor; eauto. apply regset_set; auto. + econstructor; eauto. apply set_reg_lessdef; auto. (* eliminated move *) rewrite H1 in H. clear H1. inv H. right. split. simpl. omega. split. auto. @@ -451,7 +433,7 @@ Proof. (* load *) TransfInstr. - assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. exploit eval_addressing_lessdef; eauto. intros [a' [ADDR' ALD]]. exploit Mem.loadv_extends; eauto. @@ -459,11 +441,11 @@ Proof. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split. eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. apply eval_addressing_preserved. exact symbols_preserved. eauto. - econstructor; eauto. apply regset_set; auto. + econstructor; eauto. apply set_reg_lessdef; auto. (* store *) TransfInstr. - assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. exploit eval_addressing_lessdef; eauto. intros [a' [ADDR' ALD]]. exploit Mem.storev_extends. 2: eexact H1. eauto. eauto. apply RLD. @@ -484,14 +466,14 @@ Proof. destruct X as [m'' FREE]. left. exists (Callstate s' (transf_fundef fd) (rs'##args) m''); split. eapply exec_Itailcall; eauto. apply sig_preserved. - constructor. eapply match_stackframes_tail; eauto. apply regset_get_list; auto. + constructor. eapply match_stackframes_tail; eauto. apply regs_lessdef_regs; auto. eapply Mem.free_right_extends; eauto. rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction. (* call that remains a call *) left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Int.zero) pc' rs' :: s') (transf_fundef fd) (rs'##args) m'); split. eapply exec_Icall; eauto. apply sig_preserved. - constructor. constructor; auto. apply regset_get_list; auto. auto. + constructor. constructor; auto. apply regs_lessdef_regs; auto. auto. (* tailcall *) exploit find_function_translated; eauto. intro FIND'. @@ -500,37 +482,26 @@ Proof. left. exists (Callstate s' (transf_fundef fd) (rs'##args) m'1); split. eapply exec_Itailcall; eauto. apply sig_preserved. rewrite stacksize_preserved; auto. - constructor. auto. apply regset_get_list; auto. auto. + constructor. auto. apply regs_lessdef_regs; auto. auto. (* builtin *) TransfInstr. - assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. - 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'#res <- v') m'1); split. - eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved; eauto. - 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. + exploit (@eval_builtin_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. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (regmap_setres res v' rs') m'1); split. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_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. + econstructor; eauto. apply set_res_lessdef; auto. (* cond *) TransfInstr. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split. eapply exec_Icond; eauto. - apply eval_condition_lessdef with (rs##args) m; auto. apply regset_get_list; auto. + apply eval_condition_lessdef with (rs##args) m; auto. apply regs_lessdef_regs; auto. constructor; auto. (* jumptable *) @@ -576,7 +547,7 @@ Proof. left. econstructor; split. simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto. rewrite EQ2. rewrite EQ3. constructor; auto. - apply regset_init_regs. auto. + apply regs_lessdef_init_regs. auto. (* external call *) exploit external_call_mem_extends; eauto. @@ -592,7 +563,7 @@ Proof. (* synchronous return in both programs *) left. econstructor; split. apply exec_return. - constructor; auto. apply regset_set; auto. + constructor; auto. apply set_reg_lessdef; auto. (* return instr in source program, eliminated because of tailcall *) right. split. unfold measure. simpl length. change (S (length s) * (niter + 2))%nat diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 52318ede..e9e4856e 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -339,14 +339,8 @@ Proof. (* Lbuiltin *) left; simpl; econstructor; split. eapply exec_Lbuiltin; eauto. - eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - econstructor; eauto. - (* Lannot *) - left; simpl; econstructor; split. - eapply exec_Lannot; eauto. - eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. + eapply eval_builtin_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 400c19d9..8725c9af 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -59,8 +59,7 @@ Definition ref_instruction (i: instruction) : list ident := | Icall _ (inr id) _ _ _ => id :: nil | Itailcall _ (inl r) _ => nil | Itailcall _ (inr id) _ => id :: nil - | Ibuiltin ef _ _ _ => globals_external ef - | Iannot _ args _ => globals_of_annot_args args + | Ibuiltin _ args _ _ => globals_of_builtin_args args | Icond cond _ _ _ => nil | Ijumptable _ _ => nil | Ireturn _ => nil @@ -87,7 +86,7 @@ Definition add_ref_definition (pm: prog_map) (id: ident) (w: workset): workset : match pm!id with | None => w | Some (Gfun (Internal f)) => add_ref_function f w - | Some (Gfun (External ef)) => addlist_workset (globals_external ef) w + | Some (Gfun (External ef)) => w | Some (Gvar gv) => add_ref_globvar gv w end. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 85e7a360..4d7547f0 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -111,7 +111,7 @@ Proof. unfold add_ref_definition; intros. destruct (pm!id) as [[[] | ? ] | ]. apply add_ref_function_incl. - apply addlist_workset_incl. + apply workset_incl_refl. apply add_ref_globvar_incl. apply workset_incl_refl. Qed. @@ -165,7 +165,7 @@ Proof. Qed. Definition ref_fundef (fd: fundef) (id: ident) : Prop := - match fd with Internal f => ref_function f id | External ef => In id (globals_external ef) end. + match fd with Internal f => ref_function f id | External ef => False end. Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop := match gd with @@ -179,7 +179,7 @@ Lemma seen_add_ref_definition: Proof. unfold add_ref_definition; intros. rewrite H. red in H0; destruct gd as [[f|ef]|gv]. apply seen_add_ref_function; auto. - apply seen_addlist_workset; auto. + contradiction. destruct H0 as (ofs & IN). unfold add_ref_globvar. assert (forall l (w: workset), @@ -580,6 +580,14 @@ Proof. intros; red; intros. rewrite ! Regmap.gsspec. destruct (peq r0 r); auto. Qed. +Lemma set_res_inject: + forall f rs rs' res v v', + regset_inject f rs rs' -> Val.inject f v v' -> + regset_inject f (regmap_setres res v rs) (regmap_setres res v' rs'). +Proof. + intros. destruct res; auto. apply set_reg_inject; auto. +Qed. + Lemma regset_inject_incr: forall f f' rs rs', regset_inject f rs rs' -> inject_incr f f' -> regset_inject f' rs rs'. Proof. @@ -704,7 +712,6 @@ Lemma external_call_inject: forall ef vargs m1 t vres m2 f m1' vargs', meminj_preserves_globals f -> external_call ef ge vargs m1 t vres m2 -> - (forall id, In id (globals_external ef) -> kept id) -> Mem.inject f m1 m1' -> Val.inject_list f vargs vargs' -> exists f', exists vres', exists m2', @@ -717,9 +724,7 @@ Lemma external_call_inject: /\ inject_separated f f' m1 m1'. Proof. intros. eapply external_call_mem_inject_gen; eauto. -- apply globals_symbols_inject; auto. -- intros. exploit symbols_inject_2; eauto. - intros (b' & A & B); exists b'; auto. + apply globals_symbols_inject; auto. Qed. Lemma find_function_inject: @@ -741,60 +746,60 @@ Proof. auto. Qed. -Lemma eval_annot_arg_inject: +Lemma eval_builtin_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 -> + eval_builtin_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) -> + (forall id, In id (globals_of_builtin_arg a) -> kept id) -> exists v', - eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' a v' + eval_builtin_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. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. - 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. + intros (v' & A & B). exists v'; auto with barg. +- econstructor; split; eauto with barg. 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. + exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with barg. +- econstructor; split; eauto with barg. 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. +- destruct IHeval_builtin_arg1 as (v1' & A1 & B1); eauto using in_or_app. + destruct IHeval_builtin_arg2 as (v2' & A2 & B2); eauto using in_or_app. + exists (Val.longofwords v1' v2'); split; auto with barg. apply Val.longofwords_inject; auto. Qed. -Lemma eval_annot_args_inject: +Lemma eval_builtin_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 -> + eval_builtin_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) -> + (forall id, In id (globals_of_builtin_args al) -> kept id) -> exists vl', - eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl' + eval_builtin_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl' /\ Val.inject_list 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). + exploit eval_builtin_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. @@ -888,39 +893,22 @@ Proof. apply regs_inject; auto. - (* builtin *) - exploit external_call_inject; eauto. - eapply match_stacks_preserves_globals; eauto. - intros. apply KEPT. red. econstructor; econstructor; eauto. - apply regs_inject; eauto. - intros (j' & tv & tm' & A & B & C & D & E & F & G). - econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply match_states_regular with (j := j'); eauto. - apply match_stacks_incr with j; auto. - intros. exploit G; eauto. intros [P Q]. - 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 set_reg_inject; auto. apply regset_inject_incr with j; auto. - -- (* annot *) - exploit eval_annot_args_inject; eauto. + exploit eval_builtin_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 exec_Ibuiltin; 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. + apply set_res_inject; auto. apply regset_inject_incr with j; auto. - (* cond *) assert (C: eval_condition cond trs##args tm = Some b). diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index c559aa25..3b0e7133 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -35,6 +35,11 @@ Definition areg (ae: aenv) (r: reg) : aval := AE.get r ae. Definition aregs (ae: aenv) (rl: list reg) : list aval := List.map (areg ae) rl. +(** Analysis of function calls. We treat specially the case where + neither the arguments nor the global variables point within the + stack frame of the current function. In this case, no pointer + within the stack frame escapes during the call. *) + Definition mafter_public_call : amem := mtop. Definition mafter_private_call (am_before: amem) : amem := @@ -43,53 +48,78 @@ Definition mafter_private_call (am_before: amem) : amem := am_nonstack := Nonstack; am_top := plub (ab_summary (am_stack am_before)) Nonstack |}. -Definition transfer_call (ae: aenv) (am: amem) (args: list reg) (res: reg) := +Definition analyze_call (am: amem) (aargs: list aval) := if pincl am.(am_nonstack) Nonstack - && forallb (fun r => vpincl (areg ae r) Nonstack) args - then - VA.State (AE.set res (Ifptr Nonstack) ae) (mafter_private_call am) - else - VA.State (AE.set res Vtop ae) mafter_public_call. - -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_val (av: aval) - | Builtin_default. - -Definition classify_builtin (ef: external_function) (args: list reg) (ae: aenv) := - match ef, args with - | EF_vload chunk, a1::nil => Builtin_vload chunk (areg ae a1) - | EF_vload_global chunk id ofs, nil => Builtin_vload chunk (Ptr (Gl id ofs)) - | 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_val _ _, a1::nil => Builtin_annot_val (areg ae a1) - | _, _ => Builtin_default + && forallb (fun av => vpincl av Nonstack) aargs + then (Ifptr Nonstack, mafter_private_call am) + else (Vtop, mafter_public_call). + +Definition transfer_call (ae: aenv) (am: amem) (args: list reg) (res: reg) := + let (av, am') := analyze_call am (aregs ae args) in + VA.State (AE.set res av ae) am'. + +(** Analysis of builtins. *) + +Fixpoint abuiltin_arg (ae: aenv) (am: amem) (rm: romem) (ba: builtin_arg reg) : aval := + match ba with + | BA r => areg ae r + | BA_int n => I n + | BA_long n => L n + | BA_float n => F n + | BA_single n => FS n + | BA_loadstack chunk ofs => loadv chunk rm am (Ptr (Stk ofs)) + | BA_addrstack ofs => Ptr (Stk ofs) + | BA_loadglobal chunk id ofs => loadv chunk rm am (Ptr (Gl id ofs)) + | BA_addrglobal id ofs => Ptr (Gl id ofs) + | BA_longofwords hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo) end. -Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_function) (args: list reg) (res: reg) := - match classify_builtin ef args ae with - | Builtin_vload chunk aaddr => +Definition set_builtin_res (br: builtin_res reg) (av: aval) (ae: aenv) : aenv := + match br with + | BR r => AE.set r av ae + | _ => ae + end. + +Definition transfer_builtin_default + (ae: aenv) (am: amem) (rm: romem) + (args: list (builtin_arg reg)) (res: builtin_res reg) := + let (av, am') := analyze_call am (map (abuiltin_arg ae am rm) args) in + VA.State (set_builtin_res res av ae) am'. + +Definition transfer_builtin + (ae: aenv) (am: amem) (rm: romem) (ef: external_function) + (args: list (builtin_arg reg)) (res: builtin_res reg) := + match ef, args with + | EF_vload chunk, addr :: nil => + let aaddr := abuiltin_arg ae am rm addr in let a := if va_strict tt then vlub (loadv chunk rm am aaddr) (vnormalize chunk (Ifptr Glob)) else vnormalize chunk Vtop in - VA.State (AE.set res a ae) am - | Builtin_vstore chunk aaddr av => + VA.State (set_builtin_res res a ae) am + | EF_vstore chunk, addr :: v :: nil => + let aaddr := abuiltin_arg ae am rm addr in + let av := abuiltin_arg ae am rm v in let am' := storev chunk am aaddr av in - VA.State (AE.set res ntop ae) (mlub am am') - | Builtin_memcpy sz al adst asrc => + VA.State (set_builtin_res res ntop ae) (mlub am am') + | EF_memcpy sz al, dst :: src :: nil => + let adst := abuiltin_arg ae am rm dst in + let asrc := abuiltin_arg ae am rm src in 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 ntop ae) am' - | Builtin_annot_val av => - VA.State (AE.set res av ae) am - | Builtin_default => - transfer_call ae am args res + VA.State (set_builtin_res res ntop ae) am' + | (EF_annot _ _ | EF_debug _ _ _), _ => + VA.State (set_builtin_res res ntop ae) am + | EF_annot_val _ _, v :: nil => + let av := abuiltin_arg ae am rm v in + VA.State (set_builtin_res res av ae) am + | _, _ => + transfer_builtin_default ae am rm args res end. +(** The transfer function for one instruction. Given the abstract state + "before" the instruction, computes the abstract state "after". *) + Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) : VA.t := match f.(fn_code)!pc with | None => @@ -111,8 +141,6 @@ 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) => @@ -121,6 +149,9 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) : VA.Bot end. +(** A wrapper on [transfer] that removes information associated with + dead registers, so as to reduce the sizes of abstract states. *) + Definition transfer' (f: function) (lastuses: PTree.t (list reg)) (rm: romem) (pc: node) (before: VA.t) : VA.t := match before with @@ -138,6 +169,8 @@ Definition transfer' (f: function) (lastuses: PTree.t (list reg)) (rm: romem) end end. +(** The forward dataflow analysis. *) + Module DS := Dataflow_Solver(VA)(NodeSetForward). Definition mfunction_entry := @@ -285,50 +318,65 @@ Proof. split. eapply ematch_ge; eauto. eauto. Qed. -(** Classification of builtin functions *) +(** ** Analysis of registers and builtin arguments *) -Lemma classify_builtin_sound: - forall bc e ae ef (ge: genv) args m t res m', - ematch bc e ae -> +Lemma areg_sound: + forall bc e ae r, ematch bc e ae -> vmatch bc (e#r) (areg ae r). +Proof. + intros. apply H. +Qed. + +Lemma aregs_sound: + forall bc e ae rl, ematch bc e ae -> list_forall2 (vmatch bc) (e##rl) (aregs ae rl). +Proof. + induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto. +Qed. + +Hint Resolve areg_sound aregs_sound: va. + +Lemma abuiltin_arg_sound: + forall bc ge rs sp m ae rm am, + ematch bc rs ae -> + romatch bc m rm -> + mmatch bc m am -> genv_match bc ge -> - external_call ef ge e##args m t res m' -> - match classify_builtin ef args ae with - | Builtin_vload chunk aaddr => - exists addr, - volatile_load_sem chunk ge (addr::nil) m t res m' /\ vmatch bc addr aaddr - | Builtin_vstore chunk aaddr av => - exists addr v, - volatile_store_sem chunk ge (addr::v::nil) m t res m' - /\ vmatch bc addr aaddr /\ vmatch bc v av - | Builtin_memcpy sz al adst asrc => - 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_val av => m' = m /\ vmatch bc res av - | Builtin_default => True - end. + bc sp = BCstack -> + forall a v, + eval_builtin_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v -> + vmatch bc v (abuiltin_arg ae am rm a). +Proof. + intros until am; intros EM RM MM GM SP. + induction 1; simpl; eauto with va. +- eapply loadv_sound; eauto. simpl. rewrite Int.add_zero_l. auto with va. +- simpl. rewrite Int.add_zero_l. auto with va. +- eapply loadv_sound; eauto. apply symbol_address_sound; auto. +- apply symbol_address_sound; auto. +Qed. + +Lemma abuiltin_args_sound: + forall bc ge rs sp m ae rm am, + ematch bc rs ae -> + romatch bc m rm -> + mmatch bc m am -> + genv_match bc ge -> + bc sp = BCstack -> + forall al vl, + eval_builtin_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl -> + list_forall2 (vmatch bc) vl (map (abuiltin_arg ae am rm) al). +Proof. + intros until am; intros EM RM MM GM SP. + induction 1; simpl. +- constructor. +- constructor; auto. eapply abuiltin_arg_sound; eauto. +Qed. + +Lemma set_builtin_res_sound: + forall bc rs ae v av res, + ematch bc rs ae -> + vmatch bc v av -> + ematch bc (regmap_setres res v rs) (set_builtin_res res av ae). Proof. - intros. unfold classify_builtin; destruct ef; auto. -- (* vload *) - destruct args; auto. destruct args; auto. - exists (e#p); split; eauto. -- (* vstore *) - destruct args; auto. destruct args; auto. destruct args; auto. - exists (e#p), (e#p0); eauto. -- (* vload global *) - destruct args; auto. simpl in H1. - rewrite volatile_load_global_charact in H1. destruct H1 as (b & A & B). - exists (Vptr b ofs); split; auto. constructor. constructor. eapply H0; eauto. -- (* vstore global *) - destruct args; auto. destruct args; auto. simpl in H1. - rewrite volatile_store_global_charact in H1. destruct H1 as (b & A & B). - exists (Vptr b ofs), (e#p); split; auto. split; eauto. constructor. constructor. eapply H0; eauto. -- (* memcpy *) - destruct args; auto. destruct args; auto. destruct args; auto. - exists (e#p), (e#p0); eauto. -- (* annot val *) - destruct args; auto. destruct args; auto. - simpl in H1. inv H1. eauto. + intros. destruct res; simpl; auto. apply ematch_update; auto. Qed. (** ** Constructing block classifications *) @@ -981,6 +1029,17 @@ Proof. apply UNCH1; auto. intros; red. unfold inj_of_bc; rewrite H0; auto. Qed. +Remark list_forall2_in_l: + forall (A B: Type) (P: A -> B -> Prop) x1 l1 l2, + list_forall2 P l1 l2 -> In x1 l1 -> exists x2, In x2 l2 /\ P x1 x2. +Proof. + induction 1; simpl; intros. +- contradiction. +- destruct H1. + + subst. exists b1; auto. + + exploit IHlist_forall2; eauto. intros (x2 & U & V). exists x2; auto. +Qed. + (** ** Semantic invariant *) Section SOUNDNESS. @@ -1170,20 +1229,6 @@ Proof. econstructor; eauto. Qed. -Lemma areg_sound: - forall bc e ae r, ematch bc e ae -> vmatch bc (e#r) (areg ae r). -Proof. - intros. apply H. -Qed. - -Lemma aregs_sound: - forall bc e ae rl, ematch bc e ae -> list_forall2 (vmatch bc) (e##rl) (aregs ae rl). -Proof. - induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto. -Qed. - -Hint Resolve areg_sound aregs_sound: va. - Theorem sound_step: forall st t st', RTL.step ge st t st' -> sound_state st -> sound_state st'. Proof. @@ -1215,9 +1260,9 @@ Proof. - (* call *) assert (TR: transfer f rm pc ae am = transfer_call ae am args res). { unfold transfer; rewrite H; auto. } - unfold transfer_call in TR. + unfold transfer_call, analyze_call in TR. destruct (pincl (am_nonstack am) Nonstack && - forallb (fun r : reg => vpincl (areg ae r) Nonstack) args) eqn:NOLEAK. + forallb (fun av => vpincl av Nonstack) (aregs ae args)) eqn:NOLEAK. + (* private call *) InvBooleans. exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC. @@ -1230,7 +1275,9 @@ Proof. eapply mmatch_stack; eauto. * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v. apply D with (areg ae r). - rewrite forallb_forall in H2. apply vpincl_ge. apply H2; auto. auto with va. + rewrite forallb_forall in H2. apply vpincl_ge. + apply H2. apply in_map; auto. + auto with va. + (* public call *) exploit analyze_successor; eauto. simpl; eauto. rewrite TR. intros SUCC. exploit anonymize_stack; eauto. intros (bc' & A & B & C & D & E & F & G). @@ -1259,61 +1306,24 @@ Proof. assert (SPVALID: Plt sp0 (Mem.nextblock m)) by (eapply mmatch_below; eauto with va). assert (TR: transfer f rm pc ae am = transfer_builtin ae am rm ef args res). { unfold transfer; rewrite H; auto. } - unfold transfer_builtin in TR. - exploit classify_builtin_sound; eauto. destruct (classify_builtin ef args ae). -+ (* volatile load *) - intros (addr & VLOAD & VADDR). inv VLOAD. - eapply sound_succ_state; eauto. simpl; auto. - apply ematch_update; auto. - inv H2. - * (* true volatile access *) - assert (V: vmatch bc v0 (Ifptr Glob)). - { inv H4; simpl in *; constructor. econstructor. eapply GE; eauto. } - destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. - apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor. - * (* normal memory access *) - exploit loadv_sound; eauto. simpl; eauto. intros V. - destruct (va_strict tt). - apply vmatch_lub_l. auto. - eapply vnormalize_cast; eauto. eapply vmatch_top; eauto. -+ (* volatile store *) - intros (addr & src & VSTORE & VADDR & VSRC). inv VSTORE. inv H7. - * (* true volatile access *) - eapply sound_succ_state; eauto. simpl; auto. - apply ematch_update; auto. constructor. - apply mmatch_lub_l; auto. - * (* normal memory access *) - eapply sound_succ_state; eauto. simpl; auto. - apply ematch_update; auto. constructor. - apply mmatch_lub_r. eapply storev_sound; eauto. auto. - eapply romatch_store; eauto. - eapply sound_stack_storev; eauto. simpl; eauto. -+ (* memcpy *) - intros (dst & src & MEMCPY & VDST & VSRC). inv MEMCPY. - eapply sound_succ_state; eauto. simpl; auto. - apply ematch_update; auto. constructor. - eapply storebytes_sound; eauto. - apply match_aptr_of_aval; auto. - eapply Mem.loadbytes_length; eauto. - intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. - eapply romatch_storebytes; eauto. - eapply sound_stack_storebytes; eauto. -+ (* annot val *) - intros (A & B); subst. - eapply sound_succ_state; eauto. simpl; auto. - apply ematch_update; auto. -+ (* general case *) - intros _. - unfold transfer_call in TR. + (* The default case *) + assert (DEFAULT: + transfer f rm pc ae am = transfer_builtin_default ae am rm args res -> + sound_state + (State s f (Vptr sp0 Int.zero) pc' (regmap_setres res vres rs) m')). + { unfold transfer_builtin_default, analyze_call; intros TR'. + set (aargs := map (abuiltin_arg ae am rm) args) in *. + assert (ARGS: list_forall2 (vmatch bc) vargs aargs) by (eapply abuiltin_args_sound; eauto). destruct (pincl (am_nonstack am) Nonstack && - forallb (fun r : reg => vpincl (areg ae r) Nonstack) args) eqn:NOLEAK. + forallb (fun av => vpincl av Nonstack) aargs) + eqn: NOLEAK. * (* private builtin call *) - InvBooleans. rewrite forallb_forall in H2. + InvBooleans. rewrite forallb_forall in H3. exploit hide_stack; eauto. apply pincl_ge; auto. intros (bc1 & A & B & C & D & E & F & G). exploit external_call_match; eauto. - intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v0. - eapply D; eauto with va. apply vpincl_ge. apply H2; auto. + intros. exploit list_forall2_in_l; eauto. intros (av & U & V). + eapply D; eauto with va. apply vpincl_ge. apply H3; auto. intros (bc2 & J & K & L & M & N & O & P & Q). exploit (return_from_private_call bc bc2); eauto. eapply mmatch_below; eauto. @@ -1324,7 +1334,7 @@ Proof. eapply external_call_nextblock; eauto. intros (bc3 & U & V & W & X & Y & Z & AA). eapply sound_succ_state with (bc := bc3); eauto. simpl; auto. - apply ematch_update; auto. + apply set_builtin_res_sound; auto. apply sound_stack_exten with bc. apply sound_stack_inv with m. auto. intros. apply Q. red. eapply Plt_trans; eauto. @@ -1334,7 +1344,7 @@ Proof. exploit anonymize_stack; eauto. intros (bc1 & A & B & C & D & E & F & G). exploit external_call_match; eauto. - intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v0. eapply D; eauto with va. + intros. exploit list_forall2_in_l; eauto. intros (av & U & V). eapply D; eauto with va. intros (bc2 & J & K & L & M & N & O & P & Q). exploit (return_from_public_call bc bc2); eauto. eapply mmatch_below; eauto. @@ -1343,17 +1353,66 @@ Proof. eapply external_call_nextblock; eauto. intros (bc3 & U & V & W & X & Y & Z & AA). eapply sound_succ_state with (bc := bc3); eauto. simpl; auto. - apply ematch_update; auto. + apply set_builtin_res_sound; auto. apply sound_stack_exten with bc. apply sound_stack_inv with m. auto. intros. apply Q. red. eapply Plt_trans; eauto. rewrite C; auto. exact AA. - -- (* annot *) - destruct ef; try contradiction. inv H2. + } + unfold transfer_builtin in TR. + destruct ef; auto. ++ (* volatile load *) + inv H0; auto. inv H3; auto. inv H1. + exploit abuiltin_arg_sound; eauto. intros VM1. + eapply sound_succ_state; eauto. simpl; auto. + apply set_builtin_res_sound; auto. + inv H3. + * (* true volatile access *) + assert (V: vmatch bc v (Ifptr Glob)). + { inv H4; simpl in *; constructor. econstructor. eapply GE; eauto. } + destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. + apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor. + * (* normal memory access *) + exploit loadv_sound; eauto. simpl; eauto. intros V. + destruct (va_strict tt). + apply vmatch_lub_l. auto. + eapply vnormalize_cast; eauto. eapply vmatch_top; eauto. ++ (* volatile store *) + inv H0; auto. inv H3; auto. inv H4; auto. inv H1. + exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H0. intros VM1. + exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H2. intros VM2. + inv H9. + * (* true volatile access *) + eapply sound_succ_state; eauto. simpl; auto. + apply set_builtin_res_sound; auto. constructor. + apply mmatch_lub_l; auto. + * (* normal memory access *) + eapply sound_succ_state; eauto. simpl; auto. + apply set_builtin_res_sound; auto. constructor. + apply mmatch_lub_r. eapply storev_sound; eauto. auto. + eapply romatch_store; eauto. + eapply sound_stack_storev; eauto. simpl; eauto. ++ (* memcpy *) + inv H0; auto. inv H3; auto. inv H4; auto. inv H1. + exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H0. intros VM1. + exploit abuiltin_arg_sound. eauto. eauto. eauto. eauto. eauto. eexact H2. intros VM2. eapply sound_succ_state; eauto. simpl; auto. - unfold transfer; rewrite H; eauto. + apply set_builtin_res_sound; auto. constructor. + eapply storebytes_sound; eauto. + apply match_aptr_of_aval; auto. + eapply Mem.loadbytes_length; eauto. + intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. + eapply romatch_storebytes; eauto. + eapply sound_stack_storebytes; eauto. ++ (* annot *) + inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. ++ (* annot val *) + inv H0; auto. inv H3; auto. inv H1. + eapply sound_succ_state; eauto. simpl; auto. + apply set_builtin_res_sound; auto. eapply abuiltin_arg_sound; eauto. ++ (* debug *) + inv H1. eapply sound_succ_state; eauto. simpl; auto. apply set_builtin_res_sound; auto. constructor. - (* cond *) eapply sound_succ_state; eauto. @@ -1830,7 +1889,46 @@ Proof. eapply eval_static_addressing_sound; eauto with va. Qed. +(** This is a less precise version of [abuiltin_arg], where memory + contents are not taken into account. *) - +Definition aaddr_arg (a: VA.t) (ba: builtin_arg reg) : aptr := + match a with + | VA.Bot => Pbot + | VA.State ae am => + match ba with + | BA r => aptr_of_aval (AE.get r ae) + | BA_addrstack ofs => Stk ofs + | BA_addrglobal id ofs => Gl id ofs + | _ => Ptop + end + end. +Lemma aaddr_arg_sound_1: + forall bc rs ae m rm am ge sp a b ofs, + ematch bc rs ae -> + romatch bc m rm -> + mmatch bc m am -> + genv_match bc ge -> + bc sp = BCstack -> + eval_builtin_arg ge (fun r : positive => rs # r) (Vptr sp Int.zero) m a (Vptr b ofs) -> + pmatch bc b ofs (aaddr_arg (VA.State ae am) a). +Proof. + intros. + apply pmatch_ge with (aptr_of_aval (abuiltin_arg ae am rm a)). + simpl. destruct a; try (apply pge_top); simpl; apply pge_refl. + apply match_aptr_of_aval. eapply abuiltin_arg_sound; eauto. +Qed. +Lemma aaddr_arg_sound: + forall prog s f sp pc e m a b ofs, + sound_state prog (State s f (Vptr sp Int.zero) pc e m) -> + eval_builtin_arg (Genv.globalenv prog) (fun r => e#r) (Vptr sp Int.zero) m a (Vptr b ofs) -> + exists bc, + pmatch bc b ofs (aaddr_arg (analyze (romem_for_program prog) f)!!pc a) + /\ genv_match bc (Genv.globalenv prog) + /\ bc sp = BCstack. +Proof. + intros. inv H. rewrite AN. exists bc; split; auto. + eapply aaddr_arg_sound_1; eauto. +Qed. diff --git a/backend/XTL.ml b/backend/XTL.ml index 0e5ce0c4..e05b90d1 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -34,8 +34,7 @@ type instruction = | Xstore of memory_chunk * addressing * var list * var | 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 + | Xbuiltin of external_function * var builtin_arg list * var builtin_res | Xbranch of node | Xcond of condition * var list * node * node | Xjumptable of var * node list @@ -125,10 +124,22 @@ 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 = +let rec type_builtin_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 + | BA v -> set_var_type v ty + | BA_longofwords(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint + | _ -> () + +let rec type_builtin_args al tyl = + match al, tyl with + | [], [] -> () + | a :: al, ty :: tyl -> type_builtin_arg a ty; type_builtin_args al tyl + | _, _ -> raise Type_error + +let rec type_builtin_res a ty = + match a with + | BR v -> set_var_type v ty + | BR_longofwords(a1, a2) -> type_builtin_res a1 Tint; type_builtin_res a2 Tint | _ -> () let type_instr = function @@ -158,13 +169,8 @@ let type_instr = function () | Xbuiltin(ef, args, res) -> 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 + type_builtin_args args sg.sig_args; + type_builtin_res res (proj_sig_res sg) | Xbranch s -> () | Xcond(cond, args, s1, s2) -> diff --git a/backend/XTL.mli b/backend/XTL.mli index 9794565c..6bdcc8c6 100644 --- a/backend/XTL.mli +++ b/backend/XTL.mli @@ -35,8 +35,7 @@ type instruction = | Xstore of memory_chunk * addressing * var list * var | 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 + | Xbuiltin of external_function * var builtin_arg list * var builtin_res | Xbranch of node | Xcond of condition * var list * node * node | Xjumptable of var * node list |