diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/AST.v | 50 | ||||
| -rw-r--r-- | common/Events.v | 20 |
2 files changed, 44 insertions, 26 deletions
diff --git a/common/AST.v b/common/AST.v index 1b1e872..5eee291 100644 --- a/common/AST.v +++ b/common/AST.v @@ -83,14 +83,26 @@ Fixpoint subtype_list (tyl1 tyl2: list typ) : bool := end. (** Additionally, function definitions and function calls are annotated - by function signatures indicating the number and types of arguments, - as well as the type of the returned value if any. These signatures - are used in particular to determine appropriate calling conventions - for the function. *) + by function signatures indicating: +- the number and types of arguments; +- the type of the returned value, if any; +- additional information on which calling convention to use. + +These signatures are used in particular to determine appropriate +calling conventions for the function. *) + +Record calling_convention : Type := mkcallconv { + cc_vararg: bool; + cc_structret: bool +}. + +Definition cc_default := + {| cc_vararg := false; cc_structret := false |}. Record signature : Type := mksignature { sig_args: list typ; - sig_res: option typ + sig_res: option typ; + sig_cc: calling_convention }. Definition proj_sig_res (s: signature) : typ := @@ -100,9 +112,15 @@ Definition proj_sig_res (s: signature) : typ := end. Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. -Proof. generalize opt_typ_eq, list_typ_eq; intros; decide equality. Defined. +Proof. + generalize opt_typ_eq, list_typ_eq; intros; decide equality. + generalize bool_dec; intros. decide equality. +Defined. Global Opaque signature_eq. +Definition signature_main := + {| sig_args := nil; sig_res := Some Tint; sig_cc := cc_default |}. + (** Memory accesses (load and store instructions) are annotated by a ``memory chunk'' indicating the type, size and signedness of the chunk of memory being accessed. *) @@ -570,16 +588,16 @@ Definition ef_sig (ef: external_function): signature := match ef with | EF_external name sg => sg | EF_builtin name sg => sg - | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) - | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None - | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) - | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None - | EF_malloc => mksignature (Tint :: nil) (Some Tint) - | EF_free => mksignature (Tint :: nil) None - | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None - | EF_annot text targs => mksignature (annot_args_typ targs) None - | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) - | EF_inline_asm text => mksignature nil None + | 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 (annot_args_typ targs) None cc_default + | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default + | EF_inline_asm text => mksignature nil None cc_default end. (** Whether an external function should be inlined by the compiler. *) diff --git a/common/Events.v b/common/Events.v index 24c03dc..cf57650 100644 --- a/common/Events.v +++ b/common/Events.v @@ -764,7 +764,7 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk))). + (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -826,7 +826,7 @@ 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))). + (mksignature nil (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -967,7 +967,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None). + (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1022,7 +1022,7 @@ 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). + (mksignature (type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1070,7 +1070,7 @@ Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint)). + (mksignature (Tint :: nil) (Some Tint) cc_default). Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m n m' b m'', @@ -1145,7 +1145,7 @@ Inductive extcall_free_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None). + (mksignature (Tint :: nil) None cc_default). Proof. constructor; intros. (* well typed *) @@ -1241,7 +1241,7 @@ Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val - Lemma extcall_memcpy_ok: forall sz al, - extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None). + extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None cc_default). Proof. intros. constructor. (* return type *) @@ -1337,7 +1337,7 @@ Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (g Lemma extcall_annot_ok: forall text targs, - extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None). + extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1381,7 +1381,7 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv. Lemma extcall_annot_val_ok: forall text targ, - extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ)). + extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1433,7 +1433,7 @@ Axiom external_functions_properties: Parameter inline_assembly_sem: ident -> extcall_sem. Axiom inline_assembly_properties: - forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None). + forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default). (** ** Combined semantics of external calls *) |