From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 18 Feb 2020 16:57:17 +0100 Subject: Refine the type of function results in AST.signature Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions. --- common/AST.v | 79 ++++++++++++++++++++++++++++++++++++++++-------------- common/Builtins.v | 2 +- common/Builtins0.v | 64 +++++++++++++++++++++---------------------- common/Events.v | 45 +++++++++++++++++++------------ common/Memdata.v | 24 ++++++++++------- common/Memory.v | 9 +++++++ common/Memtype.v | 5 ++++ common/PrintAST.ml | 8 ++++++ common/Values.v | 33 ++++++++++++++++++++++- 9 files changed, 189 insertions(+), 80 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index a91138c9..fcbf0b34 100644 --- a/common/AST.v +++ b/common/AST.v @@ -45,9 +45,6 @@ Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}. Proof. decide equality. Defined. Global Opaque typ_eq. -Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2} - := option_eq typ_eq. - Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} := list_eq_dec typ_eq. @@ -91,10 +88,34 @@ Fixpoint subtype_list (tyl1 tyl2: list typ) : bool := | _, _ => false end. +(** To describe the values returned by functions, we use the more precise + types below. *) + +Inductive rettype : Type := + | Tret (t: typ) (**r like type [t] *) + | Tint8signed (**r 8-bit signed integer *) + | Tint8unsigned (**r 8-bit unsigned integer *) + | Tint16signed (**r 16-bit signed integer *) + | Tint16unsigned (**r 16-bit unsigned integer *) + | Tvoid. (**r no value returned *) + +Coercion Tret: typ >-> rettype. + +Lemma rettype_eq: forall (t1 t2: rettype), {t1=t2} + {t1<>t2}. +Proof. generalize typ_eq; decide equality. Defined. +Global Opaque rettype_eq. + +Fixpoint proj_rettype (r: rettype) : typ := + match r with + | Tret t => t + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => Tint + | Tvoid => Tint + end. + (** Additionally, function definitions and function calls are annotated by function signatures indicating: - the number and types of arguments; -- the type of the returned value, if any; +- the type of the returned value; - additional information on which calling convention to use. These signatures are used in particular to determine appropriate @@ -117,24 +138,20 @@ Global Opaque calling_convention_eq. Record signature : Type := mksignature { sig_args: list typ; - sig_res: option typ; + sig_res: rettype; sig_cc: calling_convention }. -Definition proj_sig_res (s: signature) : typ := - match s.(sig_res) with - | None => Tint - | Some t => t - end. +Definition proj_sig_res (s: signature) : typ := proj_rettype s.(sig_res). Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. Proof. - generalize opt_typ_eq, list_typ_eq, calling_convention_eq; decide equality. + generalize rettype_eq, list_typ_eq, calling_convention_eq; decide equality. Defined. Global Opaque signature_eq. Definition signature_main := - {| sig_args := nil; sig_res := Some Tint; sig_cc := cc_default |}. + {| sig_args := nil; sig_res := 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 @@ -177,6 +194,28 @@ Definition type_of_chunk (c: memory_chunk) : typ := Lemma type_of_Mptr: type_of_chunk Mptr = Tptr. Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed. +(** Same, as a return type. *) + +Definition rettype_of_chunk (c: memory_chunk) : rettype := + match c with + | Mint8signed => Tint8signed + | Mint8unsigned => Tint8unsigned + | Mint16signed => Tint16signed + | Mint16unsigned => Tint16unsigned + | Mint32 => Tint + | Mint64 => Tlong + | Mfloat32 => Tsingle + | Mfloat64 => Tfloat + | Many32 => Tany32 + | Many64 => Tany64 + end. + +Lemma proj_rettype_of_chunk: + forall chunk, proj_rettype (rettype_of_chunk chunk) = type_of_chunk chunk. +Proof. + destruct chunk; auto. +Qed. + (** The chunk that is appropriate to store and reload a value of the given type, without losing information. *) @@ -477,15 +516,15 @@ Definition ef_sig (ef: external_function): signature := | EF_external name sg => sg | EF_builtin name sg => sg | EF_runtime name sg => sg - | EF_vload chunk => mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default - | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default - | EF_malloc => mksignature (Tptr :: nil) (Some Tptr) cc_default - | EF_free => mksignature (Tptr :: nil) None cc_default - | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) None cc_default - | EF_annot kind text targs => mksignature targs None cc_default - | EF_annot_val kind text targ => mksignature (targ :: nil) (Some targ) cc_default + | EF_vload chunk => mksignature (Tptr :: nil) (rettype_of_chunk chunk) cc_default + | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default + | EF_malloc => mksignature (Tptr :: nil) Tptr cc_default + | EF_free => mksignature (Tptr :: nil) Tvoid cc_default + | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) Tvoid cc_default + | EF_annot kind text targs => mksignature targs Tvoid cc_default + | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default | EF_inline_asm text sg clob => sg - | EF_debug kind text targs => mksignature targs None cc_default + | EF_debug kind text targs => mksignature targs Tvoid cc_default end. (** Whether an external function should be inlined by the compiler. *) diff --git a/common/Builtins.v b/common/Builtins.v index c9097e86..476b541e 100644 --- a/common/Builtins.v +++ b/common/Builtins.v @@ -29,7 +29,7 @@ Definition builtin_function_sig (b: builtin_function) : signature := | BI_platform b => platform_builtin_sig b end. -Definition builtin_function_sem (b: builtin_function) : builtin_sem (proj_sig_res (builtin_function_sig b)) := +Definition builtin_function_sem (b: builtin_function) : builtin_sem (sig_res (builtin_function_sig b)) := match b with | BI_standard b => standard_builtin_sem b | BI_platform b => platform_builtin_sem b diff --git a/common/Builtins0.v b/common/Builtins0.v index b78006dd..8da98314 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -26,8 +26,8 @@ Require Import AST Integers Floats Values Memdata. appropriate for the target. *) -Definition val_opt_has_type (ov: option val) (t: typ) : Prop := - match ov with Some v => Val.has_type v t | None => True end. +Definition val_opt_has_rettype (ov: option val) (t: rettype) : Prop := + match ov with Some v => Val.has_rettype v t | None => True end. Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop := match ov, ov' with @@ -42,10 +42,10 @@ Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop := and be compatible with value injections. *) -Record builtin_sem (tret: typ) : Type := mkbuiltin { +Record builtin_sem (tret: rettype) : Type := mkbuiltin { bs_sem :> list val -> option val; bs_well_typed: forall vl, - val_opt_has_type (bs_sem vl) tret; + val_opt_has_rettype (bs_sem vl) tret; bs_inject: forall j vl vl', Val.inject_list j vl vl' -> val_opt_inject j (bs_sem vl) (bs_sem vl') }. @@ -60,8 +60,8 @@ Record builtin_sem (tret: typ) : Type := mkbuiltin { Local Unset Program Cases. Program Definition mkbuiltin_v1t - (tret: typ) (f: val -> val) - (WT: forall v1, Val.has_type (f v1) tret) + (tret: rettype) (f: val -> val) + (WT: forall v1, Val.has_rettype (f v1) tret) (INJ: forall j v1 v1', Val.inject j v1 v1' -> Val.inject j (f v1) (f v1')) := mkbuiltin tret (fun vl => match vl with v1 :: nil => Some (f v1) | _ => None end) _ _. Next Obligation. @@ -72,8 +72,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v2t - (tret: typ) (f: val -> val -> val) - (WT: forall v1 v2, Val.has_type (f v1 v2) tret) + (tret: rettype) (f: val -> val -> val) + (WT: forall v1 v2, Val.has_rettype (f v1 v2) tret) (INJ: forall j v1 v1' v2 v2', Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j (f v1 v2) (f v1' v2')) := @@ -86,8 +86,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v3t - (tret: typ) (f: val -> val -> val -> val) - (WT: forall v1 v2 v3, Val.has_type (f v1 v2 v3) tret) + (tret: rettype) (f: val -> val -> val -> val) + (WT: forall v1 v2 v3, Val.has_rettype (f v1 v2 v3) tret) (INJ: forall j v1 v1' v2 v2' v3 v3', Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j v3 v3' -> Val.inject j (f v1 v2 v3) (f v1' v2' v3')) := @@ -100,8 +100,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v1p - (tret: typ) (f: val -> option val) - (WT: forall v1, val_opt_has_type (f v1) tret) + (tret: rettype) (f: val -> option val) + (WT: forall v1, val_opt_has_rettype (f v1) tret) (INJ: forall j v1 v1', Val.inject j v1 v1' -> val_opt_inject j (f v1) (f v1')) := mkbuiltin tret (fun vl => match vl with v1 :: nil => f v1 | _ => None end) _ _. @@ -113,8 +113,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v2p - (tret: typ) (f: val -> val -> option val) - (WT: forall v1 v2, val_opt_has_type (f v1 v2) tret) + (tret: rettype) (f: val -> val -> option val) + (WT: forall v1 v2, val_opt_has_rettype (f v1 v2) tret) (INJ: forall j v1 v1' v2 v2', Val.inject j v1 v1' -> Val.inject j v2 v2' -> val_opt_inject j (f v1 v2) (f v1' v2')) := @@ -171,7 +171,7 @@ Proof. destruct t; intros; constructor. Qed. -Lemma inj_num_opt_wt: forall t x, val_opt_has_type (option_map (inj_num t) x) t. +Lemma inj_num_opt_wt: forall t x, val_opt_has_rettype (option_map (inj_num t) x) t. Proof. intros. destruct x; simpl. apply inj_num_wt. auto. Qed. @@ -200,13 +200,13 @@ Proof. Qed. Lemma proj_num_opt_wt: - forall tres t k0 k1 v, + forall (tres: typ) t k0 k1 v, k0 = None \/ k0 = Some Vundef -> - (forall x, val_opt_has_type (k1 x) tres) -> - val_opt_has_type (proj_num t k0 v k1) tres. + (forall x, val_opt_has_rettype (k1 x) tres) -> + val_opt_has_rettype (proj_num t k0 v k1) tres. Proof. intros. - assert (val_opt_has_type k0 tres). { destruct H; subst k0; exact I. } + assert (val_opt_has_rettype k0 tres). { destruct H; subst k0; exact I. } destruct t; simpl; destruct v; auto. Qed. @@ -393,33 +393,33 @@ Definition standard_builtin_table : list (string * standard_builtin) := Definition standard_builtin_sig (b: standard_builtin) : signature := match b with | BI_select t => - mksignature (Tint :: t :: t :: nil) (Some t) cc_default + mksignature (Tint :: t :: t :: nil) t cc_default | BI_fabs | BI_fsqrt => - mksignature (Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: nil) Tfloat cc_default | BI_negl => - mksignature (Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: nil) Tlong cc_default | BI_addl | BI_subl | BI_i64_umulh| BI_i64_smulh | BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod => - mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: Tlong :: nil) Tlong cc_default | BI_mull => - mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default + mksignature (Tint :: Tint :: nil) Tlong cc_default | BI_i32_bswap => - mksignature (Tint :: nil) (Some Tint) cc_default + mksignature (Tint :: nil) Tint cc_default | BI_i64_bswap => - mksignature (Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: nil) Tlong cc_default | BI_i16_bswap => - mksignature (Tint :: nil) (Some Tint) cc_default + mksignature (Tint :: nil) Tint cc_default | BI_i64_shl | BI_i64_shr | BI_i64_sar => - mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default + mksignature (Tlong :: Tint :: nil) Tlong cc_default | BI_i64_dtos | BI_i64_dtou => - mksignature (Tfloat :: nil) (Some Tlong) cc_default + mksignature (Tfloat :: nil) Tlong cc_default | BI_i64_stod | BI_i64_utod => - mksignature (Tlong :: nil) (Some Tfloat) cc_default + mksignature (Tlong :: nil) Tfloat cc_default | BI_i64_stof | BI_i64_utof => - mksignature (Tlong :: nil) (Some Tsingle) cc_default + mksignature (Tlong :: nil) Tsingle cc_default end. -Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (proj_sig_res (standard_builtin_sig b)) := +Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig_res (standard_builtin_sig b)) := match b with | BI_select t => mkbuiltin t diff --git a/common/Events.v b/common/Events.v index 3fb84f49..10e0c232 100644 --- a/common/Events.v +++ b/common/Events.v @@ -623,7 +623,7 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := ec_well_typed: forall ge vargs m1 t vres m2, sem ge vargs m1 t vres m2 -> - Val.has_type vres (proj_sig_res sg); + Val.has_rettype vres sg.(sig_res); (** The semantics is invariant under change of global environment that preserves symbols. *) ec_symbols_preserved: @@ -771,12 +771,12 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default). + (mksignature (Tptr :: nil) (rettype_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. - eapply Mem.load_type; eauto. +- inv H. inv H0. apply Val.load_result_rettype. + eapply Mem.load_rettype; eauto. (* symbols *) - inv H0. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) @@ -922,7 +922,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -967,7 +967,7 @@ Inductive extcall_malloc_sem (ge: Senv.t): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tptr :: nil) (Some Tptr) cc_default). + (mksignature (Tptr :: nil) Tptr cc_default). Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m lo hi v m' b m'', @@ -984,7 +984,7 @@ Proof. } constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res, Tptr; simpl. destruct Archi.ptr64; auto. +- inv H. simpl. unfold Tptr; destruct Archi.ptr64; auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) @@ -1053,11 +1053,11 @@ Inductive extcall_free_sem (ge: Senv.t): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tptr :: nil) None cc_default). + (mksignature (Tptr :: nil) Tvoid cc_default). Proof. constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res. simpl. auto. +- inv H. simpl. auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) @@ -1147,11 +1147,11 @@ 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 (Tptr :: Tptr :: nil) None cc_default). + (mksignature (Tptr :: Tptr :: nil) Tvoid cc_default). Proof. intros. constructor. - (* return type *) - intros. inv H. constructor. + intros. inv H. exact I. - (* change of globalenv *) intros. inv H0. econstructor; eauto. - (* valid blocks *) @@ -1258,7 +1258,7 @@ Inductive extcall_annot_sem (text: string) (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). + (mksignature targs Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1303,11 +1303,11 @@ Inductive extcall_annot_val_sem (text: string) (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). + (mksignature (targ :: nil) targ cc_default). Proof. intros; constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. +- inv H. eapply eventval_match_type; eauto. (* symbols *) - destruct H as (A & B & C). inv H0. econstructor; eauto. eapply eventval_match_preserved; eauto. @@ -1347,7 +1347,7 @@ Inductive extcall_debug_sem (ge: Senv.t): Lemma extcall_debug_ok: forall targs, extcall_properties extcall_debug_sem - (mksignature targs None cc_default). + (mksignature targs Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1396,7 +1396,8 @@ Proof. intros. set (bsem := builtin_function_sem bf). constructor; intros. (* well typed *) - inv H. - specialize (bs_well_typed _ bsem vargs). unfold val_opt_has_type, bsem; rewrite H0. + specialize (bs_well_typed _ bsem vargs). + unfold val_opt_has_rettype, bsem; rewrite H0. auto. (* symbols *) - inv H0. econstructor; eauto. @@ -1516,7 +1517,7 @@ Proof. apply extcall_debug_ok. Qed. -Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). +Definition external_call_well_typed_gen ef := ec_well_typed (external_call_spec ef). Definition external_call_symbols_preserved ef := ec_symbols_preserved (external_call_spec ef). Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef). Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef). @@ -1527,6 +1528,16 @@ Definition external_call_trace_length ef := ec_trace_length (external_call_spec Definition external_call_receptive ef := ec_receptive (external_call_spec ef). Definition external_call_determ ef := ec_determ (external_call_spec ef). +(** Corollary of [external_call_well_typed_gen]. *) + +Lemma external_call_well_typed: + forall ef ge vargs m1 t vres m2, + external_call ef ge vargs m1 t vres m2 -> + Val.has_type vres (proj_sig_res (ef_sig ef)). +Proof. + intros. apply Val.has_proj_rettype. eapply external_call_well_typed_gen; eauto. +Qed. + (** Corollary of [external_call_valid_block]. *) Lemma external_call_nextblock: diff --git a/common/Memdata.v b/common/Memdata.v index 7144d72c..f3016efe 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -547,18 +547,26 @@ Proof. destruct v1; auto. Qed. -Lemma decode_val_type: +Lemma decode_val_rettype: forall chunk cl, - Val.has_type (decode_val chunk cl) (type_of_chunk chunk). + Val.has_rettype (decode_val chunk cl) (rettype_of_chunk chunk). Proof. intros. unfold decode_val. destruct (proj_bytes cl). - destruct chunk; simpl; auto. -Local Opaque Val.load_result. +- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto. +- Local Opaque Val.load_result. destruct chunk; simpl; (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)). Qed. +Lemma decode_val_type: + forall chunk cl, + Val.has_type (decode_val chunk cl) (type_of_chunk chunk). +Proof. + intros. rewrite <- proj_rettype_of_chunk. + apply Val.has_proj_rettype. apply decode_val_rettype. +Qed. + Lemma encode_val_int8_signed_unsigned: forall v, encode_val Mint8signed v = encode_val Mint8unsigned v. Proof. @@ -607,11 +615,9 @@ Lemma decode_val_cast: | _ => True end. Proof. - unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. + intros. + assert (A: Val.has_rettype v (rettype_of_chunk chunk)) by apply decode_val_rettype. + destruct chunk; auto; simpl in A; destruct v; try contradiction; simpl; congruence. Qed. (** Pointers cannot be forged. *) diff --git a/common/Memory.v b/common/Memory.v index b68a5049..9f9934c2 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -682,6 +682,15 @@ Proof. apply decode_val_type. Qed. +Theorem load_rettype: + forall m chunk b ofs v, + load chunk m b ofs = Some v -> + Val.has_rettype v (rettype_of_chunk chunk). +Proof. + intros. exploit load_result; eauto; intros. rewrite H0. + apply decode_val_rettype. +Qed. + Theorem load_cast: forall m chunk b ofs v, load chunk m b ofs = Some v -> diff --git a/common/Memtype.v b/common/Memtype.v index 53775d8b..ca9c6f1f 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -300,6 +300,11 @@ Axiom load_type: load chunk m b ofs = Some v -> Val.has_type v (type_of_chunk chunk). +Axiom load_rettype: + forall m chunk b ofs v, + load chunk m b ofs = Some v -> + Val.has_rettype v (rettype_of_chunk chunk). + (** For a small integer or float type, the value returned by [load] is invariant under the corresponding cast. *) Axiom load_cast: diff --git a/common/PrintAST.ml b/common/PrintAST.ml index e477957a..cf3a17d5 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -27,6 +27,14 @@ let name_of_type = function | Tany32 -> "any32" | Tany64 -> "any64" +let name_of_rettype = function + | Tret t -> name_of_type t + | Tvoid -> "void" + | Tint8signed -> "int8s" + | Tint8unsigned -> "int8u" + | Tint16signed -> "int16s" + | Tint16unsigned -> "int16u" + let name_of_chunk = function | Mint8signed -> "int8s" | Mint8unsigned -> "int8u" diff --git a/common/Values.v b/common/Values.v index de317734..68a2054b 100644 --- a/common/Values.v +++ b/common/Values.v @@ -149,6 +149,23 @@ Proof. auto. Defined. +Definition has_rettype (v: val) (r: rettype) : Prop := + match r, v with + | Tret t, _ => has_type v t + | Tint8signed, Vint n => n = Int.sign_ext 8 n + | Tint8unsigned, Vint n => n = Int.zero_ext 8 n + | Tint16signed, Vint n => n = Int.sign_ext 16 n + | Tint16unsigned, Vint n => n = Int.zero_ext 16 n + | _, Vundef => True + | _, _ => False + end. + +Lemma has_proj_rettype: forall v r, + has_rettype v r -> has_type v (proj_rettype r). +Proof. + destruct r; simpl; intros; auto; destruct v; try contradiction; exact I. +Qed. + (** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. Other values are neither true nor false. *) @@ -1003,10 +1020,24 @@ Definition load_result (chunk: memory_chunk) (v: val) := | _, _ => Vundef end. +Lemma load_result_rettype: + forall chunk v, has_rettype (load_result chunk v) (rettype_of_chunk chunk). +Proof. + intros. unfold has_rettype; destruct chunk; destruct v; simpl; auto. +- rewrite Int.sign_ext_idem by omega; auto. +- rewrite Int.zero_ext_idem by omega; auto. +- rewrite Int.sign_ext_idem by omega; auto. +- rewrite Int.zero_ext_idem by omega; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +Qed. + Lemma load_result_type: forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk). Proof. - intros. unfold has_type; destruct chunk; destruct v; simpl; auto; destruct Archi.ptr64 eqn:SF; simpl; auto. + intros. rewrite <- proj_rettype_of_chunk. apply has_proj_rettype. + apply load_result_rettype. Qed. Lemma load_result_same: -- cgit