From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
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.
---
 riscV/Conventions1.v | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

(limited to 'riscV/Conventions1.v')

diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index df7ddfd2..09cbbb44 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -115,11 +115,10 @@ Definition is_float_reg (r: mreg) :=
   with one integer result. *)
 
 Definition loc_result (s: signature) : rpair mreg :=
-  match s.(sig_res) with
-  | None => One R10
-  | Some (Tint | Tany32) => One R10
-  | Some (Tfloat | Tsingle | Tany64) => One F10
-  | Some Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10
+  match proj_sig_res s with
+  | Tint | Tany32 => One R10
+  | Tfloat | Tsingle | Tany64 => One F10
+  | Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10
   end.
 
 (** The result registers have types compatible with that given in the signature. *)
@@ -128,8 +127,8 @@ Lemma loc_result_type:
   forall sig,
   subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
 Proof.
-  intros. unfold proj_sig_res, loc_result, mreg_type;
-  destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto.
+  intros. unfold loc_result, mreg_type;
+  destruct (proj_sig_res sig); auto; destruct Archi.ptr64; auto.
 Qed.
 
 (** The result locations are caller-save registers *)
@@ -139,7 +138,7 @@ Lemma loc_result_caller_save:
   forall_rpair (fun r => is_callee_save r = false) (loc_result s).
 Proof.
   intros. unfold loc_result, is_callee_save;
-  destruct (sig_res s) as [[]|]; simpl; auto; destruct Archi.ptr64; simpl; auto.
+  destruct (proj_sig_res s); simpl; auto; destruct Archi.ptr64; simpl; auto.
 Qed.
 
 (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -149,13 +148,13 @@ Lemma loc_result_pair:
   match loc_result sg with
   | One _ => True
   | Twolong r1 r2 =>
-       r1 <> r2 /\ sg.(sig_res) = Some Tlong
+       r1 <> r2 /\ proj_sig_res sg = Tlong
     /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true 
     /\ Archi.ptr64 = false
   end.
 Proof.
   intros.
-  unfold loc_result; destruct (sig_res sg) as [[]|]; auto.
+  unfold loc_result; destruct (proj_sig_res sg); auto.
   unfold mreg_type; destruct Archi.ptr64; auto.
   split; auto. congruence.
 Qed.
@@ -165,7 +164,7 @@ Qed.
 Lemma loc_result_exten:
   forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
 Proof.
-  intros. unfold loc_result. rewrite H; auto.  
+  intros. unfold loc_result, proj_sig_res. rewrite H; auto.  
 Qed.
 
 (** ** Location of function arguments *)
-- 
cgit