diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 143 | ||||
-rw-r--r-- | common/Events.v | 464 | ||||
-rw-r--r-- | common/PrintAST.ml | 48 |
3 files changed, 297 insertions, 358 deletions
diff --git a/common/AST.v b/common/AST.v index 387eb6b2..1f393c72 100644 --- a/common/AST.v +++ b/common/AST.v @@ -560,12 +560,6 @@ Inductive external_function : Type := (** A volatile store operation. If the adress given as first argument points within a volatile global variable, generate an event. Otherwise, produce no event and behave like a regular memory store. *) - | EF_vload_global (chunk: memory_chunk) (id: ident) (ofs: int) - (** A volatile load operation from a global variable. - Specialized version of [EF_vload]. *) - | EF_vstore_global (chunk: memory_chunk) (id: ident) (ofs: int) - (** A volatile store operation in a global variable. - Specialized version of [EF_vstore]. *) | EF_malloc (** Dynamic memory allocation. Takes the requested size in bytes as argument; returns a pointer to a fresh block of the given size. @@ -585,12 +579,16 @@ Inductive external_function : Type := (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string). + | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string) (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic preservation theorem. Generated only if [-finline-asm] is given. *) + | EF_debug (kind: positive) (text: ident) (targs: list typ). + (** Transport debugging information from the front-end to the generated + assembly. Takes zero, one or several arguments like [EF_annot]. + Unlike [EF_annot], produces no observable event. *) (** The type signature of an external function. *) @@ -600,14 +598,13 @@ Definition ef_sig (ef: external_function): signature := | EF_builtin name sg => sg | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default - | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) cc_default - | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None cc_default | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default | EF_annot text targs => mksignature targs None cc_default | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default | EF_inline_asm text sg clob => sg + | EF_debug kind text targs => mksignature targs None cc_default end. (** Whether an external function should be inlined by the compiler. *) @@ -618,14 +615,13 @@ Definition ef_inline (ef: external_function) : bool := | EF_builtin name sg => true | EF_vload chunk => true | EF_vstore chunk => true - | EF_vload_global chunk id ofs => true - | EF_vstore_global chunk id ofs => true | EF_malloc => false | EF_free => false | EF_memcpy sz al => true | EF_annot text targs => true | EF_annot_val text targ => true | EF_inline_asm text sg clob => true + | EF_debug kind text targs => true end. (** Whether an external function must reload its arguments. *) @@ -633,6 +629,7 @@ Definition ef_inline (ef: external_function) : bool := Definition ef_reloads (ef: external_function) : bool := match ef with | EF_annot text targs => false + | EF_debug kind text targs => false | _ => true end. @@ -640,22 +637,12 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. + generalize ident_eq signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. auto. apply list_eq_dec. apply String.string_dec. Defined. Global Opaque external_function_eq. -(** Global variables referenced by an external function *) - -Definition globals_external (ef: external_function) : list ident := - match ef with - | EF_vload_global _ id _ => id :: nil - | EF_vstore_global _ id _ => id :: nil - | _ => nil - end. - (** Function definitions are the union of internal and external functions. *) Inductive fundef (F: Type): Type := @@ -690,55 +677,95 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := End TRANSF_PARTIAL_FUNDEF. -(** * Arguments to annotations *) +(** * Arguments and results to builtin functions *) Set Contextual Implicit. -Inductive annot_arg (A: Type) : Type := - | AA_base (x: A) - | AA_int (n: int) - | AA_long (n: int64) - | AA_float (f: float) - | AA_single (f: float32) - | AA_loadstack (chunk: memory_chunk) (ofs: int) - | AA_addrstack (ofs: int) - | AA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) - | AA_addrglobal (id: ident) (ofs: int) - | AA_longofwords (hi lo: annot_arg A). - -Fixpoint globals_of_annot_arg (A: Type) (a: annot_arg A) : list ident := +Inductive builtin_arg (A: Type) : Type := + | BA (x: A) + | BA_int (n: int) + | BA_long (n: int64) + | BA_float (f: float) + | BA_single (f: float32) + | BA_loadstack (chunk: memory_chunk) (ofs: int) + | BA_addrstack (ofs: int) + | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) + | BA_addrglobal (id: ident) (ofs: int) + | BA_longofwords (hi lo: builtin_arg A). + +Inductive builtin_res (A: Type) : Type := + | BR (x: A) + | BR_none + | BR_longofwords (hi lo: builtin_res A). + +Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident := match a with - | AA_loadglobal chunk id ofs => id :: nil - | AA_addrglobal id ofs => id :: nil - | AA_longofwords hi lo => globals_of_annot_arg hi ++ globals_of_annot_arg lo + | BA_loadglobal chunk id ofs => id :: nil + | BA_addrglobal id ofs => id :: nil + | BA_longofwords hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo | _ => nil end. -Definition globals_of_annot_args (A: Type) (al: list (annot_arg A)) : list ident := - List.fold_right (fun a l => globals_of_annot_arg a ++ l) nil al. +Definition globals_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list ident := + List.fold_right (fun a l => globals_of_builtin_arg a ++ l) nil al. -Fixpoint params_of_annot_arg (A: Type) (a: annot_arg A) : list A := +Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A := match a with - | AA_base x => x :: nil - | AA_longofwords hi lo => params_of_annot_arg hi ++ params_of_annot_arg lo + | BA x => x :: nil + | BA_longofwords hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo | _ => nil end. -Definition params_of_annot_args (A: Type) (al: list (annot_arg A)) : list A := - List.fold_right (fun a l => params_of_annot_arg a ++ l) nil al. +Definition params_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list A := + List.fold_right (fun a l => params_of_builtin_arg a ++ l) nil al. -Fixpoint map_annot_arg (A B: Type) (f: A -> B) (a: annot_arg A) : annot_arg B := +Fixpoint params_of_builtin_res (A: Type) (a: builtin_res A) : list A := match a with - | AA_base x => AA_base (f x) - | AA_int n => AA_int n - | AA_long n => AA_long n - | AA_float n => AA_float n - | AA_single n => AA_single n - | AA_loadstack chunk ofs => AA_loadstack chunk ofs - | AA_addrstack ofs => AA_addrstack ofs - | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs - | AA_addrglobal id ofs => AA_addrglobal id ofs - | AA_longofwords hi lo => - AA_longofwords (map_annot_arg f hi) (map_annot_arg f lo) + | BR x => x :: nil + | BR_none => nil + | BR_longofwords hi lo => params_of_builtin_res hi ++ params_of_builtin_res lo end. +Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_arg B := + match a with + | BA x => BA (f x) + | 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 (map_builtin_arg f hi) (map_builtin_arg f lo) + end. + +Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B := + match a with + | BR x => BR (f x) + | BR_none => BR_none + | BR_longofwords hi lo => + BR_longofwords (map_builtin_res f hi) (map_builtin_res f lo) + end. + +(** Which kinds of builtin arguments are supported by which external function. *) + +Inductive builtin_arg_constraint : Type := + | OK_default + | OK_const + | OK_addrstack + | OK_addrglobal + | OK_addrany + | OK_all. + +Definition builtin_arg_ok + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match ba, c with + | (BA _ | BA_longofwords _ _), _ => true + | (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true + | BA_addrstack _, (OK_addrstack | OK_addrany) => true + | BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true + | _, OK_all => true + | _, _ => false + end. diff --git a/common/Events.v b/common/Events.v index 78162fff..ab418ba5 100644 --- a/common/Events.v +++ b/common/Events.v @@ -606,8 +606,7 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := f b1 = None -> f' b1 = Some(b2, delta) -> ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2. -Record extcall_properties (sem: extcall_sem) - (sg: signature) (free_globals: list ident) : Prop := +Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := mk_extcall_properties { (** The return value of an external call must agree with its signature. *) @@ -664,9 +663,6 @@ Record extcall_properties (sem: extcall_sem) ec_mem_inject: forall ge1 ge2 vargs m1 t vres m2 f m1' vargs', symbols_inject f ge1 ge2 -> - (forall id b1, - In id free_globals -> Senv.find_symbol ge1 id = Some b1 -> - exists b2, f b1 = Some(b2, 0) /\ Senv.find_symbol ge2 id = Some b2) -> sem ge1 vargs m1 t vres m2 -> Mem.inject f m1 m1' -> Val.inject_list f vargs vargs' -> @@ -769,37 +765,36 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default) - nil. + (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) - unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. +- unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. eapply Mem.load_type; eauto. (* symbols *) - inv H2. constructor. eapply volatile_load_preserved; eauto. +- inv H2. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) - inv H; auto. +- inv H; auto. (* max perms *) - inv H; auto. +- inv H; auto. (* readonly *) - inv H. apply Mem.unchanged_on_refl. +- inv H. apply Mem.unchanged_on_refl. (* mem extends *) - inv H. inv H1. inv H6. inv H4. +- inv H. inv H1. inv H6. inv H4. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. constructor; auto. (* mem injects *) - inv H1. inv H3. inv H8. inversion H6; subst. +- inv H0. inv H2. inv H7. inversion H5; subst. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. constructor; auto. red; intros. congruence. (* trace length *) - inv H; inv H0; simpl; omega. +- inv H; inv H0; simpl; omega. (* receptive *) - inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. +- inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. exists v2; exists m1; constructor; auto. (* determ *) - inv H; inv H0. inv H1; inv H7; try congruence. +- inv H; inv H0. inv H1; inv H7; try congruence. assert (id = id0) by (eapply Senv.find_symbol_injective; eauto). subst id0. split. constructor. eapply eventval_match_valid; eauto. @@ -811,64 +806,6 @@ Proof. split. constructor. intuition congruence. Qed. -Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) (ge: Senv.t): - list val -> mem -> trace -> val -> mem -> Prop := - | volatile_load_global_sem_intro: forall b t v m, - Senv.find_symbol ge id = Some b -> - volatile_load ge chunk m b ofs t v -> - volatile_load_global_sem chunk id ofs ge nil m t v m. - -Remark volatile_load_global_charact: - forall chunk id ofs ge vargs m t vres m', - volatile_load_global_sem chunk id ofs ge vargs m t vres m' <-> - exists b, Senv.find_symbol ge id = Some b /\ volatile_load_sem chunk ge (Vptr b ofs :: vargs) m t vres m'. -Proof. - intros; split. - intros. inv H. exists b; split; auto. constructor; auto. - intros [b [P Q]]. inv Q. econstructor; eauto. -Qed. - -Lemma volatile_load_global_ok: - forall chunk id ofs, - extcall_properties (volatile_load_global_sem chunk id ofs) - (mksignature nil (Some (type_of_chunk chunk)) cc_default) - (id :: nil). -Proof. - intros; constructor; intros. -(* well typed *) - unfold proj_sig_res; simpl. inv H. inv H1. apply Val.load_result_type. - eapply Mem.load_type; eauto. -(* symbols *) - inv H2. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. -(* valid blocks *) - inv H; auto. -(* max perm *) - inv H; auto. -(* readonly *) - inv H. apply Mem.unchanged_on_refl. -(* extends *) - inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. - exists v'; exists m1'; intuition. econstructor; eauto. -(* inject *) - inv H1. inv H3. - exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). - assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). - econstructor; eauto. rewrite Int.add_zero; auto. - exploit volatile_load_inject; eauto. intros [v' [A B]]. - exists f; exists v'; exists m1'; intuition. econstructor; eauto. - red; intros; congruence. -(* trace length *) - inv H; inv H1; simpl; omega. -(* receptive *) - inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. - exists v2; exists m1; econstructor; eauto. -(* determ *) - rewrite volatile_load_global_charact in *. - destruct H as [b1 [A1 B1]]. destruct H0 as [b2 [A2 B2]]. - rewrite A1 in A2; inv A2. - eapply ec_determ. eapply volatile_load_ok. eauto. eauto. -Qed. - (** ** Semantics of volatile stores *) Inductive volatile_store_sem (chunk: memory_chunk) (ge: Senv.t): @@ -981,99 +918,40 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default) - nil. + (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) - unfold proj_sig_res; simpl. inv H; constructor. +- unfold proj_sig_res; simpl. inv H; constructor. (* symbols preserved *) - inv H2. constructor. eapply volatile_store_preserved; eauto. +- inv H2. constructor. eapply volatile_store_preserved; eauto. (* valid block *) - inv H. inv H1. auto. eauto with mem. +- inv H. inv H1. auto. eauto with mem. (* perms *) - inv H. inv H2. auto. eauto with mem. +- inv H. inv H2. auto. eauto with mem. (* readonly *) - inv H. eapply volatile_store_readonly; eauto. +- inv H. eapply volatile_store_readonly; eauto. (* mem extends*) - inv H. inv H1. inv H6. inv H7. inv H4. +- inv H. inv H1. inv H6. inv H7. inv H4. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. exists Vundef; exists m2'; intuition. constructor; auto. (* mem inject *) - inv H1. inv H3. inv H8. inv H9. inversion H6; subst. +- inv H0. inv H2. inv H7. inv H8. inversion H5; subst. exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]]. exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence. (* trace length *) - inv H; inv H0; simpl; omega. +- inv H; inv H0; simpl; omega. (* receptive *) - assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. +- assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. subst t2; exists vres1; exists m1; auto. (* determ *) - inv H; inv H0. inv H1; inv H8; try congruence. +- inv H; inv H0. inv H1; inv H8; try congruence. assert (id = id0) by (eapply Senv.find_symbol_injective; eauto). subst id0. assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0. split. constructor. auto. split. constructor. intuition congruence. Qed. -Inductive volatile_store_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) (ge: Senv.t): - list val -> mem -> trace -> val -> mem -> Prop := - | volatile_store_global_sem_intro: forall b m1 v t m2, - Senv.find_symbol ge id = Some b -> - volatile_store ge chunk m1 b ofs v t m2 -> - volatile_store_global_sem chunk id ofs ge (v :: nil) m1 t Vundef m2. - -Remark volatile_store_global_charact: - forall chunk id ofs ge vargs m t vres m', - volatile_store_global_sem chunk id ofs ge vargs m t vres m' <-> - exists b, Senv.find_symbol ge id = Some b /\ volatile_store_sem chunk ge (Vptr b ofs :: vargs) m t vres m'. -Proof. - intros; split. - intros. inv H; exists b; split; auto; econstructor; eauto. - intros [b [P Q]]. inv Q. econstructor; eauto. -Qed. - -Lemma volatile_store_global_ok: - forall chunk id ofs, - extcall_properties (volatile_store_global_sem chunk id ofs) - (mksignature (type_of_chunk chunk :: nil) None cc_default) - (id :: nil). -Proof. - intros; constructor; intros. -(* well typed *) - unfold proj_sig_res; simpl. inv H; constructor. -(* symbols preserved *) - inv H2. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. -(* valid block *) - inv H. inv H2. auto. eauto with mem. -(* perms *) - inv H. inv H3. auto. eauto with mem. -(* readonly *) - inv H. eapply volatile_store_readonly; eauto. -(* mem extends*) - rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. - exploit ec_mem_extends. eapply volatile_store_ok. eexact Q. eauto. eauto. - intros [vres' [m2' [A [B [C D]]]]]. - exists vres'; exists m2'; intuition. rewrite volatile_store_global_charact. exists b; auto. -(* mem inject *) - rewrite volatile_store_global_charact in H1. destruct H1 as [b [P Q]]. - exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). - assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. - exploit ec_mem_inject. eapply volatile_store_ok. eauto. intuition. eexact Q. eauto. constructor. eauto. eauto. - intros [f' [vres' [m2' [A [B [C [D [E G]]]]]]]]. - exists f'; exists vres'; exists m2'; intuition. - rewrite volatile_store_global_charact. exists b2; auto. -(* trace length *) - inv H. inv H1; simpl; omega. -(* receptive *) - assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. subst t2. - exists vres1; exists m1; congruence. -(* determ *) - rewrite volatile_store_global_charact in *. - destruct H as [b1 [A1 B1]]. destruct H0 as [b2 [A2 B2]]. rewrite A1 in A2; inv A2. - eapply ec_determ. eapply volatile_store_ok. eauto. eauto. -Qed. - (** ** Semantics of dynamic memory allocation (malloc) *) Inductive extcall_malloc_sem (ge: Senv.t): @@ -1085,8 +963,7 @@ Inductive extcall_malloc_sem (ge: Senv.t): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint) cc_default) - nil. + (mksignature (Tint :: nil) (Some Tint) cc_default). Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m n m' b m'', @@ -1104,19 +981,19 @@ Proof. constructor; intros. (* well typed *) - inv H. unfold proj_sig_res; simpl. auto. +- inv H. unfold proj_sig_res; simpl. auto. (* symbols preserved *) - inv H2; econstructor; eauto. +- inv H2; econstructor; eauto. (* valid block *) - inv H. eauto with mem. +- inv H. eauto with mem. (* perms *) - inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto. +- inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto. rewrite dec_eq_false. auto. apply Mem.valid_not_valid_diff with m1; eauto with mem. (* readonly *) - inv H. eapply UNCHANGED; eauto. +- inv H. eapply UNCHANGED; eauto. (* mem extends *) - inv H. inv H1. inv H5. inv H7. +- inv H. inv H1. inv H5. inv H7. exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. intros [m3' [A B]]. exploit Mem.store_within_extends. eexact B. eauto. @@ -1126,7 +1003,7 @@ Proof. econstructor; eauto. eapply UNCHANGED; eauto. (* mem injects *) - inv H1. inv H3. inv H7. inv H9. +- inv H0. inv H2. inv H6. inv H8. exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. @@ -1138,15 +1015,15 @@ Proof. eapply UNCHANGED; eauto. eapply UNCHANGED; eauto. red; intros. destruct (eq_block b1 b). - subst b1. rewrite C in H3. inv H3. eauto with mem. - rewrite D in H3 by auto. congruence. + subst b1. rewrite C in H2. inv H2. eauto with mem. + rewrite D in H2 by auto. congruence. (* trace length *) - inv H; simpl; omega. +- inv H; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. +- assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. (* determ *) - inv H; inv H0. split. constructor. intuition congruence. +- inv H; inv H0. split. constructor. intuition congruence. Qed. (** ** Semantics of dynamic memory deallocation (free) *) @@ -1161,25 +1038,24 @@ Inductive extcall_free_sem (ge: Senv.t): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None cc_default) - nil. + (mksignature (Tint :: nil) None cc_default). Proof. constructor; intros. (* well typed *) - inv H. unfold proj_sig_res. simpl. auto. +- inv H. unfold proj_sig_res. simpl. auto. (* symbols preserved *) - inv H2; econstructor; eauto. +- inv H2; econstructor; eauto. (* valid block *) - inv H. eauto with mem. +- inv H. eauto with mem. (* perms *) - inv H. eapply Mem.perm_free_3; eauto. +- inv H. eapply Mem.perm_free_3; eauto. (* readonly *) - inv H. eapply Mem.free_unchanged_on; eauto. +- inv H. eapply Mem.free_unchanged_on; eauto. intros. red; intros. elim H3. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm; eauto. (* mem extends *) - inv H. inv H1. inv H8. inv H6. +- inv H. inv H1. inv H8. inv H6. exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B. exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]]. exists Vundef; exists m2'; intuition. @@ -1191,13 +1067,13 @@ Proof. eapply Mem.free_range_perm. eexact H4. eauto. } tauto. (* mem inject *) - inv H1. inv H3. inv H8. inv H10. +- inv H0. inv H2. inv H7. inv H9. exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable). eapply Mem.free_range_perm; eauto. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. - apply H1. instantiate (1 := lo). omega. + apply H0. instantiate (1 := lo). omega. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. @@ -1209,18 +1085,18 @@ Proof. split. auto. split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence. split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. - intros. red; intros. eelim H8; eauto. + intros. red; intros. eelim H7; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply H1. omega. + apply H0. omega. split. auto. red; intros. congruence. (* trace length *) - inv H; simpl; omega. +- inv H; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. +- assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. (* determ *) - inv H; inv H0. split. constructor. intuition congruence. +- inv H; inv H0. split. constructor. intuition congruence. Qed. (** ** Semantics of [memcpy] operations. *) @@ -1241,8 +1117,7 @@ Inductive extcall_memcpy_sem (sz al: Z) (ge: Senv.t): Lemma extcall_memcpy_ok: forall sz al, extcall_properties (extcall_memcpy_sem sz al) - (mksignature (Tint :: Tint :: nil) None cc_default) - nil. + (mksignature (Tint :: Tint :: nil) None cc_default). Proof. intros. constructor. - (* return type *) @@ -1274,7 +1149,7 @@ Proof. erewrite list_forall2_length; eauto. tauto. - (* injections *) - intros. inv H1. inv H3. inv H15. inv H16. inv H12. inv H13. + intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. destruct (zeq sz 0). + (* special case sz = 0 *) assert (bytes = nil). @@ -1325,7 +1200,7 @@ Proof. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. congruence. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. - eelim H3; eauto. + eelim H2; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. eapply Mem.storebytes_range_perm; eauto. erewrite list_forall2_length; eauto. @@ -1353,39 +1228,38 @@ Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t): Lemma extcall_annot_ok: forall text targs, extcall_properties (extcall_annot_sem text targs) - (mksignature targs None cc_default) - nil. + (mksignature targs None cc_default). Proof. intros; constructor; intros. (* well typed *) - inv H. simpl. auto. +- inv H. simpl. auto. (* symbols *) - inv H2. econstructor; eauto. +- inv H2. econstructor; eauto. eapply eventval_list_match_preserved; eauto. (* valid blocks *) - inv H; auto. +- inv H; auto. (* perms *) - inv H; auto. +- inv H; auto. (* readonly *) - inv H. apply Mem.unchanged_on_refl. +- inv H. apply Mem.unchanged_on_refl. (* mem extends *) - inv H. +- inv H. exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. (* mem injects *) - inv H1. +- inv H0. exists f; exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. red; intros; congruence. (* trace length *) - inv H; simpl; omega. +- inv H; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. +- assert (t1 = t2). inv H; inv H0; auto. exists vres1; exists m1; congruence. (* determ *) - inv H; inv H0. +- inv H; inv H0. assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0. split. constructor. auto. Qed. @@ -1399,43 +1273,81 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (ge: Senv.t): Lemma extcall_annot_val_ok: forall text targ, extcall_properties (extcall_annot_val_sem text targ) - (mksignature (targ :: nil) (Some targ) cc_default) - nil. + (mksignature (targ :: nil) (Some targ) cc_default). Proof. intros; constructor; intros. (* well typed *) - inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. +- inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. (* symbols *) - inv H2. econstructor; eauto. +- inv H2. econstructor; eauto. eapply eventval_match_preserved; eauto. (* valid blocks *) - inv H; auto. +- inv H; auto. (* perms *) - inv H; auto. +- inv H; auto. (* readonly *) - inv H. apply Mem.unchanged_on_refl. +- inv H. apply Mem.unchanged_on_refl. (* mem extends *) - inv H. inv H1. inv H6. +- inv H. inv H1. inv H6. exists v2; exists m1'; intuition. econstructor; eauto. eapply eventval_match_lessdef; eauto. (* mem inject *) - inv H1. inv H3. inv H8. +- inv H0. inv H2. inv H7. exists f; exists v'; exists m1'; intuition. econstructor; eauto. eapply eventval_match_inject; eauto. red; intros; congruence. (* trace length *) - inv H; simpl; omega. +- inv H; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. +- assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. (* determ *) - inv H; inv H0. +- inv H; inv H0. assert (arg = arg0). eapply eventval_match_determ_2; eauto. subst arg0. split. constructor. auto. Qed. +Inductive extcall_debug_sem (ge: Senv.t): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_debug_sem_intro: forall vargs m, + extcall_debug_sem ge vargs m E0 Vundef m. + +Lemma extcall_debug_ok: + forall targs, + extcall_properties extcall_debug_sem + (mksignature targs None cc_default). +Proof. + intros; constructor; intros. +(* well typed *) +- inv H. simpl. auto. +(* symbols *) +- inv H2. econstructor; eauto. +(* valid blocks *) +- inv H; auto. +(* perms *) +- inv H; auto. +(* readonly *) +- inv H. apply Mem.unchanged_on_refl. +(* mem extends *) +- inv H. + exists Vundef; exists m1'; intuition. + econstructor; eauto. +(* mem injects *) +- inv H0. + exists f; exists Vundef; exists m1'; intuition. + econstructor; eauto. + red; intros; congruence. +(* trace length *) +- inv H; simpl; omega. +(* receptive *) +- inv H; inv H0. exists Vundef, m1; constructor. +(* determ *) +- inv H; inv H0. + split. constructor. auto. +Qed. + (** ** Semantics of external functions. *) (** For functions defined outside the program ([EF_external] and [EF_builtin]), @@ -1445,14 +1357,14 @@ Qed. Parameter external_functions_sem: ident -> signature -> extcall_sem. Axiom external_functions_properties: - forall id sg, extcall_properties (external_functions_sem id sg) sg nil. + forall id sg, extcall_properties (external_functions_sem id sg) sg. (** We treat inline assembly similarly. *) Parameter inline_assembly_sem: ident -> signature -> extcall_sem. Axiom inline_assembly_properties: - forall id sg, extcall_properties (inline_assembly_sem id sg) sg nil. + forall id sg, extcall_properties (inline_assembly_sem id sg) sg. (** ** Combined semantics of external calls *) @@ -1473,33 +1385,31 @@ Definition external_call (ef: external_function): extcall_sem := | EF_builtin name sg => external_functions_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk - | EF_vload_global chunk id ofs => volatile_load_global_sem chunk id ofs - | EF_vstore_global chunk id ofs => volatile_store_global_sem chunk id ofs | EF_malloc => extcall_malloc_sem | EF_free => extcall_free_sem | EF_memcpy sz al => extcall_memcpy_sem sz al | EF_annot txt targs => extcall_annot_sem txt targs | EF_annot_val txt targ => extcall_annot_val_sem txt targ | EF_inline_asm txt sg clb => inline_assembly_sem txt sg + | EF_debug kind txt targs => extcall_debug_sem end. Theorem external_call_spec: forall ef, - extcall_properties (external_call ef) (ef_sig ef) (globals_external ef). + extcall_properties (external_call ef) (ef_sig ef). Proof. - intros. unfold external_call, ef_sig, globals_external; destruct ef. + intros. unfold external_call, ef_sig; destruct ef. apply external_functions_properties. apply external_functions_properties. apply volatile_load_ok. apply volatile_store_ok. - apply volatile_load_global_ok. - apply volatile_store_global_ok. apply extcall_malloc_ok. apply extcall_free_ok. apply extcall_memcpy_ok. apply extcall_annot_ok. apply extcall_annot_val_ok. apply inline_assembly_properties. + apply extcall_debug_ok. Qed. Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). @@ -1563,7 +1473,7 @@ Lemma external_call_mem_inject: /\ inject_separated f f' m1 m1'. Proof. intros. destruct H as (A & B & C). eapply external_call_mem_inject_gen with (ge1 := ge); eauto. -- repeat split; intros. + repeat split; intros. + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto. + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto. + simpl in H3. exists b1; split; eauto. @@ -1572,7 +1482,6 @@ Proof. * exploit B; eauto. intros EQ; rewrite EQ in H; inv H. rewrite V1; auto. * destruct (Genv.find_var_info ge b2) as [gv2|] eqn:V2; auto. exploit C; eauto. intros EQ; subst b2. congruence. -- intros. exists b1; split; auto. apply A with id; auto. Qed. (** Corollaries of [external_call_determ]. *) @@ -1648,8 +1557,7 @@ Lemma decode_longs_inject: Proof. induction tyl; simpl; intros. auto. - destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. -Qed. + 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). @@ -1785,9 +1693,9 @@ Proof. split; congruence. Qed. -(** * Evaluation of annotation arguments *) +(** * Evaluation of builtin arguments *) -Section EVAL_ANNOT_ARG. +Section EVAL_BUILTIN_ARG. Variable A: Type. Variable ge: Senv.t. @@ -1795,54 +1703,54 @@ Variable e: A -> val. Variable sp: val. Variable m: mem. -Inductive eval_annot_arg: annot_arg A -> val -> Prop := - | eval_AA_base: forall x, - eval_annot_arg (AA_base x) (e x) - | eval_AA_int: forall n, - eval_annot_arg (AA_int n) (Vint n) - | eval_AA_long: forall n, - eval_annot_arg (AA_long n) (Vlong n) - | eval_AA_float: forall n, - eval_annot_arg (AA_float n) (Vfloat n) - | eval_AA_single: forall n, - eval_annot_arg (AA_single n) (Vsingle n) - | eval_AA_loadstack: forall chunk ofs v, +Inductive eval_builtin_arg: builtin_arg A -> val -> Prop := + | eval_BA: forall x, + eval_builtin_arg (BA x) (e x) + | 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 (Senv.symbol_address ge id ofs) = Some v -> - eval_annot_arg (AA_loadglobal chunk id ofs) v - | eval_AA_addrglobal: forall id ofs, - eval_annot_arg (AA_addrglobal id ofs) (Senv.symbol_address ge id ofs) - | eval_AA_longofwords: forall hi lo vhi vlo, - eval_annot_arg hi vhi -> eval_annot_arg lo vlo -> - eval_annot_arg (AA_longofwords hi lo) (Val.longofwords vhi vlo). + eval_builtin_arg (BA_loadglobal chunk id ofs) v + | eval_BA_addrglobal: forall id ofs, + eval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address ge id ofs) + | eval_BA_longofwords: forall hi lo vhi vlo, + eval_builtin_arg hi vhi -> eval_builtin_arg lo vlo -> + eval_builtin_arg (BA_longofwords hi lo) (Val.longofwords vhi vlo). -Definition eval_annot_args (al: list (annot_arg A)) (vl: list val) : Prop := - list_forall2 eval_annot_arg al vl. +Definition eval_builtin_args (al: list (builtin_arg A)) (vl: list val) : Prop := + list_forall2 eval_builtin_arg al vl. -Lemma eval_annot_arg_determ: - forall a v, eval_annot_arg a v -> forall v', eval_annot_arg a v' -> v' = v. +Lemma eval_builtin_arg_determ: + forall a v, eval_builtin_arg a v -> forall v', eval_builtin_arg a v' -> v' = v. Proof. induction 1; intros v' EV; inv EV; try congruence. f_equal; eauto. Qed. -Lemma eval_annot_args_determ: - forall al vl, eval_annot_args al vl -> forall vl', eval_annot_args al vl' -> vl' = vl. +Lemma eval_builtin_args_determ: + forall al vl, eval_builtin_args al vl -> forall vl', eval_builtin_args al vl' -> vl' = vl. Proof. - induction 1; intros v' EV; inv EV; f_equal; eauto using eval_annot_arg_determ. + induction 1; intros v' EV; inv EV; f_equal; eauto using eval_builtin_arg_determ. Qed. -End EVAL_ANNOT_ARG. +End EVAL_BUILTIN_ARG. -Hint Constructors eval_annot_arg: aarg. +Hint Constructors eval_builtin_arg: barg. (** Invariance by change of global environment. *) -Section EVAL_ANNOT_ARG_PRESERVED. +Section EVAL_BUILTIN_ARG_PRESERVED. Variables A F1 V1 F2 V2: Type. Variable ge1: Genv.t F1 V1. @@ -1854,25 +1762,25 @@ Variable m: mem. Hypothesis symbols_preserved: forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. -Lemma eval_annot_arg_preserved: - forall a v, eval_annot_arg ge1 e sp m a v -> eval_annot_arg ge2 e sp m a v. +Lemma eval_builtin_arg_preserved: + forall a v, eval_builtin_arg ge1 e sp m a v -> eval_builtin_arg ge2 e sp m a v. Proof. assert (EQ: forall id ofs, Senv.symbol_address ge2 id ofs = Senv.symbol_address ge1 id ofs). { unfold Senv.symbol_address; simpl; intros. rewrite symbols_preserved; auto. } - induction 1; eauto with aarg. rewrite <- EQ in H; eauto with aarg. rewrite <- EQ; eauto with aarg. + induction 1; eauto with barg. rewrite <- EQ in H; eauto with barg. rewrite <- EQ; eauto with barg. Qed. -Lemma eval_annot_args_preserved: - forall al vl, eval_annot_args ge1 e sp m al vl -> eval_annot_args ge2 e sp m al vl. +Lemma eval_builtin_args_preserved: + forall al vl, eval_builtin_args ge1 e sp m al vl -> eval_builtin_args ge2 e sp m al vl. Proof. - induction 1; constructor; auto; eapply eval_annot_arg_preserved; eauto. + induction 1; constructor; auto; eapply eval_builtin_arg_preserved; eauto. Qed. -End EVAL_ANNOT_ARG_PRESERVED. +End EVAL_BUILTIN_ARG_PRESERVED. (** Compatibility with the "is less defined than" relation. *) -Section EVAL_ANNOT_ARG_LESSDEF. +Section EVAL_BUILTIN_ARG_LESSDEF. Variable A: Type. Variable ge: Senv.t. @@ -1883,35 +1791,35 @@ Variables m1 m2: mem. Hypothesis env_lessdef: forall x, Val.lessdef (e1 x) (e2 x). Hypothesis mem_extends: Mem.extends m1 m2. -Lemma eval_annot_arg_lessdef: - forall a v1, eval_annot_arg ge e1 sp m1 a v1 -> - exists v2, eval_annot_arg ge e2 sp m2 a v2 /\ Val.lessdef v1 v2. +Lemma eval_builtin_arg_lessdef: + forall a v1, eval_builtin_arg ge e1 sp m1 a v1 -> + exists v2, eval_builtin_arg ge e2 sp m2 a v2 /\ Val.lessdef v1 v2. Proof. induction 1. -- exists (e2 x); auto with aarg. -- econstructor; eauto with aarg. -- econstructor; eauto with aarg. -- econstructor; eauto with aarg. -- econstructor; eauto with aarg. -- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. -- econstructor; eauto with aarg. -- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. -- econstructor; eauto with aarg. -- destruct IHeval_annot_arg1 as (vhi' & P & Q). - destruct IHeval_annot_arg2 as (vlo' & R & S). - econstructor; split; eauto with aarg. apply Val.longofwords_lessdef; auto. -Qed. - -Lemma eval_annot_args_lessdef: - forall al vl1, eval_annot_args ge e1 sp m1 al vl1 -> - exists vl2, eval_annot_args ge e2 sp m2 al vl2 /\ Val.lessdef_list vl1 vl2. +- exists (e2 x); auto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with barg. +- econstructor; eauto with barg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with barg. +- econstructor; eauto with barg. +- destruct IHeval_builtin_arg1 as (vhi' & P & Q). + destruct IHeval_builtin_arg2 as (vlo' & R & S). + econstructor; split; eauto with barg. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma eval_builtin_args_lessdef: + forall al vl1, eval_builtin_args ge e1 sp m1 al vl1 -> + exists vl2, eval_builtin_args ge e2 sp m2 al vl2 /\ Val.lessdef_list vl1 vl2. Proof. induction 1. - econstructor; split. constructor. auto. -- exploit eval_annot_arg_lessdef; eauto. intros (v1' & P & Q). +- exploit eval_builtin_arg_lessdef; eauto. intros (v1' & P & Q). destruct IHlist_forall2 as (vl' & U & V). exists (v1'::vl'); split; constructor; auto. Qed. -End EVAL_ANNOT_ARG_LESSDEF. +End EVAL_BUILTIN_ARG_LESSDEF. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 76305d02..5f1db76b 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -41,12 +41,6 @@ let name_of_external = function | EF_builtin(name, sg) -> sprintf "builtin %S" (extern_atom name) | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk) | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk) - | EF_vload_global(chunk, id, ofs) -> - sprintf "volatile load %s global %S %ld" - (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) - | EF_vstore_global(chunk, id, ofs) -> - sprintf "volatile store %s global %S %ld" - (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) | EF_malloc -> "malloc" | EF_free -> "free" | EF_memcpy(sz, al) -> @@ -54,28 +48,38 @@ let name_of_external = function | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (extern_atom text) + | EF_debug(kind, text, targs) -> + sprintf "debug%d %S" (P.to_int kind) (extern_atom text) -let rec print_annot_arg px oc = function - | AA_base x -> px oc x - | AA_int n -> fprintf oc "int %ld" (camlint_of_coqint n) - | AA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n) - | AA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n) - | AA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n) - | AA_loadstack(chunk, ofs) -> +let rec print_builtin_arg px oc = function + | BA x -> px oc x + | BA_int n -> fprintf oc "int %ld" (camlint_of_coqint n) + | BA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n) + | BA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n) + | BA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n) + | BA_loadstack(chunk, ofs) -> fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs) - | AA_addrstack(ofs) -> + | BA_addrstack(ofs) -> fprintf oc "sp + %ld" (camlint_of_coqint ofs) - | AA_loadglobal(chunk, id, ofs) -> + | BA_loadglobal(chunk, id, ofs) -> fprintf oc "%s[&%s + %ld]" (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) - | AA_addrglobal(id, ofs) -> + | BA_addrglobal(id, ofs) -> fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs) - | AA_longofwords(hi, lo) -> - fprintf oc "longofwords(%a, %a)" - (print_annot_arg px) hi (print_annot_arg px) lo + | BA_longofwords(hi, lo) -> + fprintf oc "long(%a, %a)" + (print_builtin_arg px) hi (print_builtin_arg px) lo -let rec print_annot_args px oc = function +let rec print_builtin_args px oc = function | [] -> () - | [a] -> print_annot_arg px oc a + | [a] -> print_builtin_arg px oc a | a1 :: al -> - fprintf oc "%a, %a" (print_annot_arg px) a1 (print_annot_args px) al + fprintf oc "%a, %a" (print_builtin_arg px) a1 (print_builtin_args px) al + +let rec print_builtin_res px oc = function + | BR x -> px oc x + | BR_none -> fprintf oc "_" + | BR_longofwords(hi, lo) -> + fprintf oc "long(%a, %a)" + (print_builtin_res px) hi (print_builtin_res px) lo + |