diff options
-rw-r--r-- | cfrontend/Ctypes.v | 56 | ||||
-rw-r--r-- | common/Linking.v | 94 |
2 files changed, 86 insertions, 64 deletions
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 036b768b..bfc5daa9 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -1173,14 +1173,12 @@ Unset Implicit Arguments. (** ** Linking types *) -Instance Linker_types : Linker type := { +Program Instance Linker_types : Linker type := { link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None; linkorder := fun t1 t2 => t1 = t2 }. -Proof. - auto. - intros; congruence. - intros. destruct (type_eq x y); inv H. auto. +Next Obligation. + destruct (type_eq x y); inv H. auto. Defined. Global Opaque Linker_types. @@ -1224,14 +1222,18 @@ Proof. assert (x = y) by eauto. subst y. auto. Qed. -Instance Linker_composite_defs : Linker (list composite_definition) := { +Program Instance Linker_composite_defs : Linker (list composite_definition) := { link := link_composite_defs; linkorder := @List.incl composite_definition }. -Proof. -- intros; apply incl_refl. -- intros; red; intros; eauto. -- intros. apply link_composite_def_inv in H; destruct H as (A & B & C). +Next Obligation. + apply incl_refl. +Defined. +Next Obligation. + red; intros; eauto. +Defined. +Next Obligation. + apply link_composite_def_inv in H; destruct H as (A & B & C). split; red; intros; apply C; auto. Defined. @@ -1406,18 +1408,22 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop := | linkorder_fundef_ext_int: forall f id sg targs tres cc, linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f). -Instance Linker_fundef (F: Type): Linker (fundef F) := { +Program Instance Linker_fundef (F: Type): Linker (fundef F) := { link := link_fundef; linkorder := linkorder_fundef }. -Proof. -- intros; constructor. -- intros. inv H; inv H0; constructor. -- intros x y z EQ. destruct x, y; simpl in EQ. +Next Obligation. + constructor. +Defined. +Next Obligation. + inv H; inv H0; constructor. +Defined. +Next Obligation. + destruct x, y; simpl in H. + discriminate. -+ destruct e; inv EQ. split; constructor. -+ destruct e; inv EQ. split; constructor. -+ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv EQ. ++ destruct e; inv H. split; constructor. ++ destruct e; inv H. split; constructor. ++ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv H. InvBooleans. subst. split; constructor. Defined. @@ -1465,15 +1471,19 @@ Definition linkorder_program {F: Type} (p1 p2: program F) : Prop := linkorder (program_of_program p1) (program_of_program p2) /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co). -Instance Linker_program (F: Type): Linker (program F) := { +Program Instance Linker_program (F: Type): Linker (program F) := { link := link_program; linkorder := linkorder_program }. -Proof. -- intros; split. apply linkorder_refl. auto. -- intros. destruct H, H0. split. eapply linkorder_trans; eauto. +Next Obligation. + split. apply linkorder_refl. auto. +Defined. +Next Obligation. + destruct H, H0. split. eapply linkorder_trans; eauto. intros; auto. -- intros until z. unfold link_program. +Defined. +Next Obligation. + revert H. unfold link_program. destruct (link (program_of_program x) (program_of_program y)) as [p|] eqn:LP; try discriminate. destruct (lift_option (link (prog_types x) (prog_types y))) as [[typs EQ]|EQ]; try discriminate. destruct (link_build_composite_env (prog_types x) (prog_types y) typs diff --git a/common/Linking.v b/common/Linking.v index eaa95462..ec828ea4 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -59,18 +59,22 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop := | linkorder_fundef_refl: forall fd, linkorder_fundef fd fd | linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f). -Instance Linker_fundef (F: Type): Linker (fundef F) := { +Program Instance Linker_fundef (F: Type): Linker (fundef F) := { link := link_fundef; linkorder := linkorder_fundef }. -Proof. -- intros; constructor. -- intros. inv H; inv H0; constructor. -- intros x y z EQ. destruct x, y; simpl in EQ. +Next Obligation. + constructor. +Defined. +Next Obligation. + inv H; inv H0; constructor. +Defined. +Next Obligation. + destruct x, y; simpl in H. + discriminate. -+ destruct e; inv EQ. split; constructor. -+ destruct e; inv EQ. split; constructor. -+ destruct (external_function_eq e e0); inv EQ. split; constructor. ++ destruct e; inv H. split; constructor. ++ destruct e; inv H. split; constructor. ++ destruct (external_function_eq e e0); inv H. split; constructor. Defined. Global Opaque Linker_fundef. @@ -109,16 +113,20 @@ Inductive linkorder_varinit: list init_data -> list init_data -> Prop := il <> nil -> init_data_list_size il = sz -> linkorder_varinit (Init_space sz :: nil) il. -Instance Linker_varinit : Linker (list init_data) := { +Program Instance Linker_varinit : Linker (list init_data) := { link := link_varinit; linkorder := linkorder_varinit }. -Proof. -- intros. constructor. -- intros. inv H; inv H0; constructor; auto. +Next Obligation. + constructor. +Defined. +Next Obligation. + inv H; inv H0; constructor; auto. congruence. simpl. generalize (init_data_list_size_pos z). xomega. -- unfold link_varinit; intros until z. +Defined. +Next Obligation. + revert H; unfold link_varinit. destruct (classify_init x) eqn:Cx, (classify_init y) eqn:Cy; intros E; inv E; try (split; constructor; fail). + destruct (zeq sz (Z.max sz0 0 + 0)); inv H0. split; constructor. congruence. auto. @@ -154,14 +162,18 @@ Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> P linkorder i1 i2 -> linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo). -Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { +Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { link := link_vardef; linkorder := linkorder_vardef }. -Proof. -- intros. destruct x; constructor; apply linkorder_refl. -- intros. inv H; inv H0. constructor; eapply linkorder_trans; eauto. -- unfold link_vardef; intros until z. +Next Obligation. + destruct x; constructor; apply linkorder_refl. +Defined. +Next Obligation. + inv H; inv H0. constructor; eapply linkorder_trans; eauto. +Defined. +Next Obligation. + revert H; unfold link_vardef. destruct x as [f1 i1 r1 v1], y as [f2 i2 r2 v2]; simpl. destruct (link f1 f2) as [f|] eqn:LF; try discriminate. destruct (link i1 i2) as [i|] eqn:LI; try discriminate. @@ -176,15 +188,10 @@ Global Opaque Linker_vardef. (** A trivial linker for the trivial var info [unit]. *) -Instance Linker_unit: Linker unit := { +Program Instance Linker_unit: Linker unit := { link := fun x y => Some tt; linkorder := fun x y => True }. -Proof. -- auto. -- auto. -- auto. -Defined. Global Opaque Linker_unit. @@ -207,18 +214,22 @@ Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V - linkorder v1 v2 -> linkorder_def (Gvar v1) (Gvar v2). -Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { +Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { link := link_def; linkorder := linkorder_def }. -Proof. -- intros. destruct x; constructor; apply linkorder_refl. -- intros. inv H; inv H0; constructor; eapply linkorder_trans; eauto. -- unfold link_def; intros. +Next Obligation. + destruct x; constructor; apply linkorder_refl. +Defined. +Next Obligation. + inv H; inv H0; constructor; eapply linkorder_trans; eauto. +Defined. +Next Obligation. + unfold link_def; intros. destruct x as [f1|v1], y as [f2|v2]; try discriminate. -+ destruct (link f1 f2) as [f|] eqn:L; inv H. apply link_linkorder in L. - split; constructor; tauto. -+ destruct (link v1 v2) as [v|] eqn:L; inv H. apply link_linkorder in L. ++ simpl in H. destruct (link f1 f2) as [f|] eqn:L. inv H. apply link_linkorder in L. + split; constructor; tauto. discriminate. ++ simpl in H; destruct (link v1 v2) as [v|] eqn:L; inv H. apply link_linkorder in L. split; constructor; tauto. Defined. @@ -320,7 +331,7 @@ Qed. End LINKER_PROG. -Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := { +Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := { link := link_prog; linkorder := fun p1 p2 => p1.(prog_main) = p2.(prog_main) @@ -332,18 +343,19 @@ Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program /\ linkorder gd1 gd2 /\ (~In id p2.(prog_public) -> gd2 = gd1) }. -Proof. -- intros; split; auto. split. apply incl_refl. intros. +Next Obligation. + split; auto. split. apply incl_refl. intros. exists gd1; split; auto. split; auto. apply linkorder_refl. - -- intros x y z (A1 & B1 & C1) (A2 & B2 & C2). +Defined. +Next Obligation. split. congruence. split. red; eauto. - intros. exploit C1; eauto. intros (gd2 & P & Q & R). - exploit C2; eauto. intros (gd3 & U & X & Y). + intros. exploit H4; eauto. intros (gd2 & P & Q & R). + exploit H2; eauto. intros (gd3 & U & X & Y). exists gd3. split; auto. split. eapply linkorder_trans; eauto. intros. transitivity gd2. apply Y. auto. apply R. red; intros; elim H0; auto. - -- intros. apply link_prog_inv in H. destruct H as (L1 & L2 & L3). +Defined. +Next Obligation. + apply link_prog_inv in H. destruct H as (L1 & L2 & L3). subst z; simpl. intuition auto. + red; intros; apply in_app_iff; auto. + rewrite prog_defmap_elements, PTree.gcombine, H by auto. |