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.

3 files changed, 15 insertions, 17 deletions

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 704b0aba..ce88778c 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -852,7 +852,7 @@ let expand_instruction instr =
       if variadic then begin
         emit (Pmflr GPR0);
         emit (Pbl(intern_string "__compcert_va_saveregs",
-                  {sig_args = []; sig_res = None; sig_cc = cc_default}));
+                  {sig_args = []; sig_res = Tvoid; sig_cc = cc_default}));
         emit (Pmtlr GPR0)
       end;
       current_function_stacksize := sz;
diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v
index f6e643d2..53c83d7e 100644
--- a/powerpc/Builtins1.v
+++ b/powerpc/Builtins1.v
@@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
   match b with end.
 
-Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
   match b with end.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 1de55c1a..7c1b2750 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -117,18 +117,16 @@ Definition dummy_float_reg := F0.   (**r Used in [Coloring]. *)
   We treat a function without result as a function with one integer result. *)
 
 Definition loc_result_32 (s: signature) : rpair mreg :=
-  match s.(sig_res) with
-  | None => One R3
-  | Some (Tint | Tany32) => One R3
-  | Some (Tfloat | Tsingle | Tany64) => One F1
-  | Some Tlong => Twolong R3 R4
+  match proj_sig_res s with
+  | Tint | Tany32 => One R3
+  | Tfloat | Tsingle | Tany64 => One F1
+  | Tlong => Twolong R3 R4
   end.
 
 Definition loc_result_64 (s: signature) : rpair mreg :=
-  match s.(sig_res) with
-  | None => One R3
-  | Some (Tint | Tlong | Tany32 | Tany64) => One R3
-  | Some (Tfloat | Tsingle) => One F1
+  match proj_sig_res s with
+  | Tint | Tlong | Tany32 | Tany64 => One R3
+  | Tfloat | Tsingle => One F1
   end.
 
 Definition loc_result :=
@@ -140,8 +138,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, loc_result_32, loc_result_64, mreg_type.
-  destruct Archi.ptr64 eqn:?; destruct (sig_res sig) as [[]|]; destruct Archi.ppc64; simpl; auto.
+  intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type.
+  destruct Archi.ptr64 eqn:?; destruct (proj_sig_res sig); destruct Archi.ppc64; simpl; auto.
 Qed.
 
 (** The result locations are caller-save registers *)
@@ -151,7 +149,7 @@ Lemma loc_result_caller_save:
   forall_rpair (fun r => is_callee_save r = false) (loc_result s).
 Proof.
   intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save;
-  destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto.
+  destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto.
 Qed.
 
 (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -161,13 +159,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, loc_result_32, loc_result_64, mreg_type;
-  destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; destruct Archi.ppc64; simpl; auto.
+  destruct Archi.ptr64; destruct (proj_sig_res sg); destruct Archi.ppc64; simpl; auto.
   split; auto. congruence.
   split; auto. congruence.
 Qed.
@@ -177,7 +175,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, loc_result_32, loc_result_64.
+  intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res.
   destruct Archi.ptr64; rewrite H; auto.
 Qed.