Support re-normalization of values returned by function calls

Some ABIs leave more flexibility concerning function return values
than CompCert expects.

For example, the x86 ABI says that a function result of type "char" is
returned in register AL, leaving the top 24 bits of register EAX
unspecified, while CompCert expects EAX to contain 32 valid bits,
namely the zero- or sign-extension of the 8-bit result.

This commits adds a general mechanism to insert "re-normalization"
conversions on the results of function calls.  Currently, it only
deals with results of small integer types, and inserts zero- or
sign-extensions if so instructed by a platform-dependent function,
Convention1.return_value_needs_normalization.

The conversions in question are inserted early in the front-end, so
that they can be optimized away in the back-end.

The semantic preservation proof is still conducted against the
CompCert model, where the return values of functions are already
normalized.  What the proof shows is that the extra conversions have
no effect in this case.  In future work we could relax the CompCert model,
allowing functions to return values that are not normalized.

1 files changed, 33 insertions, 4 deletions

diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index ee135dcd..5bd12d00 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -23,6 +23,7 @@
 Require Import Coqlib Maps Errors Integers Floats.
 Require Import AST Linking.
 Require Import Ctypes Cop Clight Cminor Csharpminor.
+Require Import Conventions1.
 
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
@@ -558,6 +559,34 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist)
       typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil
   end.
 
+(** Translate a function call.
+    Depending on the ABI, it may be necessary to normalize the value
+    returned by casting it to the return type of the function.
+    For example, in the x86 ABI, a return value of type "char" is
+    returned in register AL, leaving the top 24 bits of EAX
+    unspecified.  Hence, a cast to type "char" is needed to sign- or
+    zero-extend the returned integer before using it. *)
+
+Definition make_normalization (t: type) (a: expr) :=
+  match t with
+  | Tint IBool _ _ => Eunop Ocast8unsigned a
+  | Tint I8 Signed _ => Eunop Ocast8signed a
+  | Tint I8 Unsigned _ => Eunop Ocast8unsigned a
+  | Tint I16 Signed _ => Eunop Ocast16signed a
+  | Tint I16 Unsigned _ => Eunop Ocast16unsigned a
+  | _ => a
+  end.
+
+Definition make_funcall (x: option ident) (tres: type) (sg: signature)
+                      (fn: expr) (args: list expr): stmt :=
+  match x, return_value_needs_normalization sg.(sig_res) with
+  | Some id, true =>
+      Sseq (Scall x sg fn args)
+           (Sset id (make_normalization tres (Evar id)))
+  | _, _ =>
+      Scall x sg fn args
+  end.
+
 (** * Translation of statements *)
 
 (** [transl_statement nbrk ncnt s] returns a Csharpminor statement
@@ -601,10 +630,10 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
       | fun_case_f args res cconv =>
           do tb <- transl_expr ce b;
           do tcl <- transl_arglist ce cl args;
-          OK(Scall x {| sig_args := typlist_of_arglist cl args;
-                        sig_res  := rettype_of_type res;
-                        sig_cc   := cconv |}
-                   tb tcl)
+          let sg := {| sig_args := typlist_of_arglist cl args;
+                       sig_res  := rettype_of_type res;
+                       sig_cc   := cconv |} in
+          OK (make_funcall x res sg tb tcl)
       | _ => Error(msg "Cshmgen.transl_stmt(call)")
       end
   | Clight.Sbuiltin x ef tyargs bl =>