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/Memdata.v | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) (limited to 'common/Memdata.v') 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. *) -- cgit