From 54f97d1988f623ba7422e13a504caeb5701ba93c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 21 Aug 2015 11:05:36 +0200 Subject: 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. --- backend/ValueAnalysis.v | 404 ++++++++++++++++++++++++++++++------------------ 1 file changed, 251 insertions(+), 153 deletions(-) (limited to 'backend/ValueAnalysis.v') 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. -- cgit