diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 57 | ||||
-rw-r--r-- | common/Events.v | 187 |
2 files changed, 56 insertions, 188 deletions
diff --git a/common/AST.v b/common/AST.v index 415e90e2..0b524eb8 100644 --- a/common/AST.v +++ b/common/AST.v @@ -544,10 +544,65 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := End TRANSF_PARTIAL_FUNDEF. -(** * Arguments and results to builtin functions *) +(** * Register pairs *) Set Contextual Implicit. +(** In some intermediate languages (LTL, Mach), 64-bit integers can be + split into two 32-bit halves and held in a pair of registers. + Syntactically, this is captured by the type [rpair] below. *) + +Inductive rpair (A: Type) : Type := + | One (r: A) + | Twolong (rhi rlo: A). + +Definition typ_rpair (A: Type) (typ_of: A -> typ) (p: rpair A): typ := + match p with + | One r => typ_of r + | Twolong rhi rlo => Tlong + end. + +Definition map_rpair (A B: Type) (f: A -> B) (p: rpair A): rpair B := + match p with + | One r => One (f r) + | Twolong rhi rlo => Twolong (f rhi) (f rlo) + end. + +Definition regs_of_rpair (A: Type) (p: rpair A): list A := + match p with + | One r => r :: nil + | Twolong rhi rlo => rhi :: rlo :: nil + end. + +Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A := + match l with + | nil => nil + | p :: l => regs_of_rpair p ++ regs_of_rpairs l + end. + +Lemma in_regs_of_rpairs: + forall (A: Type) (x: A) p, In x (regs_of_rpair p) -> forall l, In p l -> In x (regs_of_rpairs l). +Proof. + induction l; simpl; intros. auto. apply in_app. destruct H0; auto. subst a. auto. +Qed. + +Lemma in_regs_of_rpairs_inv: + forall (A: Type) (x: A) l, In x (regs_of_rpairs l) -> exists p, In p l /\ In x (regs_of_rpair p). +Proof. + induction l; simpl; intros. contradiction. + rewrite in_app_iff in H; destruct H. + exists a; auto. + apply IHl in H. firstorder auto. +Qed. + +Definition forall_rpair (A: Type) (P: A -> Prop) (p: rpair A): Prop := + match p with + | One r => P r + | Twolong rhi rlo => P rhi /\ P rlo + end. + +(** * Arguments and results to builtin functions *) + Inductive builtin_arg (A: Type) : Type := | BA (x: A) | BA_int (n: int) diff --git a/common/Events.v b/common/Events.v index 040029fb..c94d6d35 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1487,193 +1487,6 @@ Proof. intros. exploit external_call_determ. eexact H. eexact H0. intuition. Qed. -(** Late in the back-end, calling conventions for external calls change: - arguments and results of type [Tlong] are passed as two integers. - We now wrap [external_call] to adapt to this convention. *) - -Fixpoint decode_longs (tyl: list typ) (vl: list val) : list val := - match tyl with - | nil => nil - | Tlong :: tys => - match vl with - | v1 :: v2 :: vs => Val.longofwords v1 v2 :: decode_longs tys vs - | _ => nil - end - | ty :: tys => - match vl with - | v1 :: vs => v1 :: decode_longs tys vs - | _ => nil - end - end. - -Definition encode_long (oty: option typ) (v: val) : list val := - match oty with - | Some Tlong => Val.hiword v :: Val.loword v :: nil - | _ => v :: nil - end. - -Definition proj_sig_res' (s: signature) : list typ := - match s.(sig_res) with - | Some Tlong => Tint :: Tint :: nil - | Some ty => ty :: nil - | None => Tint :: nil - end. - -Inductive external_call' - (ef: external_function) (ge: Senv.t) - (vargs: list val) (m1: mem) (t: trace) (vres: list val) (m2: mem) : Prop := - external_call'_intro: forall v, - external_call ef ge (decode_longs (sig_args (ef_sig ef)) vargs) m1 t v m2 -> - vres = encode_long (sig_res (ef_sig ef)) v -> - external_call' ef ge vargs m1 t vres m2. - -Lemma decode_longs_lessdef: - forall tyl vl1 vl2, Val.lessdef_list vl1 vl2 -> Val.lessdef_list (decode_longs tyl vl1) (decode_longs tyl vl2). -Proof. - induction tyl; simpl; intros. - auto. - destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_lessdef; auto. -Qed. - -Lemma decode_longs_inject: - forall f tyl vl1 vl2, Val.inject_list f vl1 vl2 -> Val.inject_list f (decode_longs tyl vl1) (decode_longs tyl vl2). -Proof. - induction tyl; simpl; intros. - auto. - destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. Qed. - -Lemma encode_long_lessdef: - forall oty v1 v2, Val.lessdef v1 v2 -> Val.lessdef_list (encode_long oty v1) (encode_long oty v2). -Proof. - intros. destruct oty as [[]|]; simpl; auto. - constructor. apply Val.hiword_lessdef; auto. constructor. apply Val.loword_lessdef; auto. auto. -Qed. - -Lemma encode_long_inject: - forall f oty v1 v2, Val.inject f v1 v2 -> Val.inject_list f (encode_long oty v1) (encode_long oty v2). -Proof. - intros. destruct oty as [[]|]; simpl; auto. - constructor. apply Val.hiword_inject; auto. constructor. apply Val.loword_inject; auto. auto. -Qed. - -Lemma encode_long_has_type: - forall v sg, - Val.has_type v (proj_sig_res sg) -> - Val.has_type_list (encode_long (sig_res sg) v) (proj_sig_res' sg). -Proof. - unfold proj_sig_res, proj_sig_res', encode_long; intros. - destruct (sig_res sg) as [[] | ]; simpl; auto. - destruct v; simpl; auto. -Qed. - -Lemma external_call_well_typed': - forall ef ge vargs m1 t vres m2, - external_call' ef ge vargs m1 t vres m2 -> - Val.has_type_list vres (proj_sig_res' (ef_sig ef)). -Proof. - intros. inv H. apply encode_long_has_type. - eapply external_call_well_typed; eauto. -Qed. - -Lemma external_call_symbols_preserved': - forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, - external_call' ef ge1 vargs m1 t vres m2 -> - Senv.equiv ge1 ge2 -> - external_call' ef ge2 vargs m1 t vres m2. -Proof. - intros. inv H. exists v; auto. eapply external_call_symbols_preserved; eauto. -Qed. - -Lemma external_call_valid_block': - forall ef ge vargs m1 t vres m2 b, - external_call' ef ge vargs m1 t vres m2 -> - Mem.valid_block m1 b -> Mem.valid_block m2 b. -Proof. - intros. inv H. eapply external_call_valid_block; eauto. -Qed. - -Lemma external_call_nextblock': - forall ef ge vargs m1 t vres m2, - external_call' ef ge vargs m1 t vres m2 -> - Ple (Mem.nextblock m1) (Mem.nextblock m2). -Proof. - intros. inv H. eapply external_call_nextblock; eauto. -Qed. - -Lemma external_call_mem_extends': - forall ef ge vargs m1 t vres m2 m1' vargs', - external_call' ef ge vargs m1 t vres m2 -> - Mem.extends m1 m1' -> - Val.lessdef_list vargs vargs' -> - exists vres' m2', - external_call' ef ge vargs' m1' t vres' m2' - /\ Val.lessdef_list vres vres' - /\ Mem.extends m2 m2' - /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'. -Proof. - intros. inv H. - exploit external_call_mem_extends; eauto. - eapply decode_longs_lessdef; eauto. - intros (v' & m2' & A & B & C & D). - exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition. - econstructor; eauto. - eapply encode_long_lessdef; eauto. -Qed. - -Lemma external_call_mem_inject': - forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs', - meminj_preserves_globals ge f -> - external_call' ef ge vargs m1 t vres m2 -> - Mem.inject f m1 m1' -> - Val.inject_list f vargs vargs' -> - exists f' vres' m2', - external_call' ef ge vargs' m1' t vres' m2' - /\ Val.inject_list f' vres vres' - /\ Mem.inject f' m2 m2' - /\ Mem.unchanged_on (loc_unmapped f) m1 m2 - /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' - /\ inject_incr f f' - /\ inject_separated f f' m1 m1'. -Proof. - intros. inv H0. - exploit external_call_mem_inject; eauto. - eapply decode_longs_inject; eauto. - intros (f' & v' & m2' & A & B & C & D & E & P & Q). - exists f'; exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition. - econstructor; eauto. - apply encode_long_inject; auto. -Qed. - -Lemma external_call_determ': - forall ef ge vargs m t1 vres1 m1 t2 vres2 m2, - external_call' ef ge vargs m t1 vres1 m1 -> - external_call' ef ge vargs m t2 vres2 m2 -> - match_traces ge t1 t2 /\ (t1 = t2 -> vres1 = vres2 /\ m1 = m2). -Proof. - intros. inv H; inv H0. exploit external_call_determ. eexact H1. eexact H. - intros [A B]. split. auto. intros. destruct B as [C D]; auto. subst. auto. -Qed. - -Lemma external_call_match_traces': - forall ef ge vargs m t1 vres1 m1 t2 vres2 m2, - external_call' ef ge vargs m t1 vres1 m1 -> - external_call' ef ge vargs m t2 vres2 m2 -> - match_traces ge t1 t2. -Proof. - intros. inv H; inv H0. eapply external_call_match_traces; eauto. -Qed. - -Lemma external_call_deterministic': - forall ef ge vargs m t vres1 m1 vres2 m2, - external_call' ef ge vargs m t vres1 m1 -> - external_call' ef ge vargs m t vres2 m2 -> - vres1 = vres2 /\ m1 = m2. -Proof. - intros. inv H; inv H0. - exploit external_call_deterministic. eexact H1. eexact H. intros [A B]. - split; congruence. -Qed. - (** * Evaluation of builtin arguments *) Section EVAL_BUILTIN_ARG. |