aboutsummaryrefslogtreecommitdiffstats
path: root/common
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-08-21 11:05:36 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-08-21 11:05:36 +0200
commit54f97d1988f623ba7422e13a504caeb5701ba93c (patch)
treed8dea46837352979490f4ed4516f9649fef41b98 /common
parentb4846ffadfa3fbb73ffa7d9c43e5218adeece8da (diff)
downloadcompcert-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 'common')
-rw-r--r--common/AST.v143
-rw-r--r--common/Events.v464
-rw-r--r--common/PrintAST.ml48
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
+