diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-02-18 16:57:17 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-02-21 13:29:39 +0100 |
| commit | be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b (patch) | |
| tree | 0d54cce547d12567d7e9e9f2c4d650e5a1b94b39 /common/Values.v | |
| parent | a9eaf4897c825093aba2137ff76e56bfbf1e72d5 (diff) | |
| download | compcert-kvx-be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b.tar.gz compcert-kvx-be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b.zip | |
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.
Diffstat (limited to 'common/Values.v')
| -rw-r--r-- | common/Values.v | 33 |
1 files changed, 32 insertions, 1 deletions
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: |