Merge of the nonstrict-ops branch:

- Most RTL operators now evaluate to Some Vundef instead of None
  when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 225 insertions, 80 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index c293efbe..3a8b8575 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -20,12 +20,13 @@ Require Import Maps.
 Require Import Ordered.
 Require Import AST.
 Require Import Integers.
+Require Import Floats.
 Require Import Memdata.
 Require Import Csharpminor.
 Require Import Cminor.
 
-Open Local Scope string_scope.
-Open Local Scope error_monad_scope.
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
 
 (** The main task in translating Csharpminor to Cminor is to explicitly
   stack-allocate local variables whose address is taken: these local
@@ -37,17 +38,17 @@ Open Local Scope error_monad_scope.
   taken in the Csharpminor code can be mapped to Cminor local
   variable, since the latter do not reside in memory.  
 
-  Another task performed during the translation to Cminor is the
-  insertion of truncation, zero- and sign-extension operations when
-  assigning to a Csharpminor local variable of ``small'' type
-  (e.g. [Mfloat32] or [Mint8signed]).  This is necessary to preserve
-  the ``normalize at assignment-time'' semantics of Clight and Csharpminor.
+  Another task performed during the translation to Cminor is to eliminate
+  redundant casts to small numerical types (8- and 16-bit integers,
+  single-precision floats).  
 
   Finally, the Clight-like [switch] construct of Csharpminor
   is transformed into the simpler, lower-level [switch] construct
   of Cminor.
 *)
 
+(** * Handling of variables *)
+
 Definition for_var (id: ident) : ident := xO id.
 Definition for_temp (id: ident) : ident := xI id.
 
@@ -69,41 +70,46 @@ Inductive var_info: Type :=
 
 Definition compilenv := PMap.t var_info.
 
-(*****
-(** [make_cast chunk e] returns a Cminor expression that normalizes
-  the value of Cminor expression [e] as prescribed by the memory chunk
-  [chunk].  For instance, 8-bit sign extension is performed if
-  [chunk] is [Mint8signed]. *)
-
-Definition make_cast (chunk: memory_chunk) (e: expr): expr :=
-  match chunk with
-  | Mint8signed => Eunop Ocast8signed e
-  | Mint8unsigned => Eunop Ocast8unsigned e
-  | Mint16signed => Eunop Ocast16signed e
-  | Mint16unsigned => Eunop Ocast16unsigned e
-  | Mint32 => e
-  | Mfloat32 => Eunop Osingleoffloat e
-  | Mfloat64 => e
-  end.
-**********)
+(** * Helper functions for code generation *)
 
 (** When the translation of an expression is stored in memory,
-  a cast at the toplevel of the expression can be redundant
+  one or several casts at the toplevel of the expression can be redundant
   with that implicitly performed by the memory store.
   [store_arg] detects this case and strips away the redundant cast. *)
 
-Definition store_arg (chunk: memory_chunk) (e: expr) : expr :=
+Function uncast_int8 (e: expr) : expr :=
+  match e with
+  | Eunop (Ocast8unsigned|Ocast8signed|Ocast16unsigned|Ocast16signed) e1 =>
+      uncast_int8 e1
+  | Ebinop Oand e1 (Econst (Ointconst n)) =>
+      if Int.eq (Int.and n (Int.repr 255)) (Int.repr 255)
+      then uncast_int8 e1
+      else e
+  | _ => e
+  end.
+
+Function uncast_int16 (e: expr) : expr :=
   match e with
-  | Eunop Ocast8signed e1 =>
-      match chunk with Mint8signed => e1 | _ => e end
-  | Eunop Ocast8unsigned e1 =>
-      match chunk with Mint8unsigned => e1 | _ => e end
-  | Eunop Ocast16signed e1 =>
-      match chunk with Mint16signed => e1 | _ => e end
-  | Eunop Ocast16unsigned e1 =>
-      match chunk with Mint16unsigned => e1 | _ => e end
-  | Eunop Osingleoffloat e1 =>
-      match chunk with Mfloat32 => e1 | _ => e end
+  | Eunop (Ocast16unsigned|Ocast16signed) e1 =>
+      uncast_int16 e1
+  | Ebinop Oand e1 (Econst (Ointconst n)) =>
+      if Int.eq (Int.and n (Int.repr 65535)) (Int.repr 65535)
+      then uncast_int16 e1
+      else e
+  | _ => e
+  end.
+
+Function uncast_float32 (e: expr) : expr :=
+  match e with
+  | Eunop Osingleoffloat e1 => uncast_float32 e1
+  | _ => e
+  end.
+
+Function store_arg (chunk: memory_chunk) (e: expr) : expr :=
+  match chunk with
+  | Mint8signed | Mint8unsigned => uncast_int8 e
+  | Mint16signed | Mint16unsigned => uncast_int16 e
+  | Mfloat32 => uncast_float32 e
   | _ => e
   end.
 
@@ -116,16 +122,148 @@ Definition make_stackaddr (ofs: Z): expr :=
 Definition make_globaladdr (id: ident): expr :=
   Econst (Oaddrsymbol id Int.zero).
 
+Definition make_unop (op: unary_operation) (e: expr): expr :=
+  match op with
+  | Ocast8unsigned => Eunop Ocast8unsigned (uncast_int8 e)
+  | Ocast8signed => Eunop Ocast8signed (uncast_int8 e)
+  | Ocast16unsigned => Eunop Ocast16unsigned (uncast_int16 e)
+  | Ocast16signed => Eunop Ocast16signed (uncast_int16 e)
+  | Osingleoffloat => Eunop Osingleoffloat (uncast_float32 e)
+  | _ => Eunop op e
+  end.
+
+(** * Optimization of casts *)
+
+(** To remove redundant casts, we perform a modest static analysis
+  on the values of expressions, classifying them into the following
+  ranges. *)
+
+Inductive approx : Type :=
+  | Any                   (**r any value *)
+  | Int7                  (**r [[0,127]] *)
+  | Int8s                 (**r [[-128,127]] *)
+  | Int8u                 (**r [[0,255]] *)
+  | Int15                 (**r [[0,32767]] *)
+  | Int16s                (**r [[-32768,32767]] *)
+  | Int16u                (**r [[0,65535]] *)
+  | Float32.               (**r single-precision float *)
+
+Module Approx.
+
+Definition bge (x y: approx) : bool :=
+  match x, y with
+  | Any, _ => true
+  | Int7, Int7 => true
+  | Int8s, (Int7 | Int8s) => true
+  | Int8u, (Int7 | Int8u) => true
+  | Int15, (Int7 | Int8u | Int15) => true
+  | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => true
+  | Int16u, (Int7 | Int8u | Int15 | Int16u) => true
+  | Float32, Float32 => true
+  | _, _ => false
+  end.
+
+Definition lub (x y: approx) : approx :=
+  match x, y with
+  | Int7, Int7 => Int7
+  | Int7, Int8u => Int8u
+  | Int7, Int8s => Int8s
+  | Int7, Int15 => Int15
+  | Int7, Int16u => Int16u
+  | Int7, Int16s => Int16s
+  | Int8u, (Int7|Int8u) => Int8u
+  | Int8u, Int15 => Int15
+  | Int8u, Int16u => Int16u
+  | Int8u, Int16s => Int16s
+  | Int8s, (Int7|Int8s) => Int8s
+  | Int8s, (Int15|Int16s) => Int16s
+  | Int15, (Int7|Int8u|Int15) => Int15
+  | Int15, Int16u => Int16u
+  | Int15, (Int8s|Int16s) => Int16s
+  | Int16u, (Int7|Int8u|Int15|Int16u) => Int16u
+  | Int16s, (Int7|Int8u|Int8s|Int15|Int16s) => Int16s
+  | Float32, Float32 => Float32
+  | _, _ => Any
+  end.
+
+Definition of_int (n: int) :=
+  if Int.eq_dec n (Int.zero_ext 7 n) then Int7
+  else if Int.eq_dec n (Int.zero_ext 8 n) then Int8u
+  else if Int.eq_dec n (Int.sign_ext 8 n) then Int8s
+  else if Int.eq_dec n (Int.zero_ext 15 n) then Int15
+  else if Int.eq_dec n (Int.zero_ext 16 n) then Int16u
+  else if Int.eq_dec n (Int.sign_ext 16 n) then Int16s
+  else Any.
+
+Definition of_float (n: float) :=
+  if Float.eq_dec n (Float.singleoffloat n) then Float32 else Any.
+
+Definition of_chunk (chunk: memory_chunk) :=
+  match chunk with
+  | Mint8signed => Int8s
+  | Mint8unsigned => Int8u
+  | Mint16signed => Int16s
+  | Mint16unsigned => Int16u
+  | Mint32 => Any
+  | Mfloat32 => Float32
+  | Mfloat64 => Any
+  end.
+
+Definition unop (op: unary_operation) (a: approx) :=
+  match op with
+  | Ocast8unsigned => Int8u
+  | Ocast8signed => Int8s
+  | Ocast16unsigned => Int16u
+  | Ocast16signed => Int16s
+  | Osingleoffloat => Float32
+  | Onotbool => Int7
+  | _ => Any
+  end.
+
+Definition unop_is_redundant (op: unary_operation) (a: approx) :=
+  match op with
+  | Ocast8unsigned => bge Int8u a
+  | Ocast8signed => bge Int8s a
+  | Ocast16unsigned => bge Int16u a
+  | Ocast16signed => bge Int16s a
+  | Osingleoffloat => bge Float32 a
+  | _ => false
+  end.
+
+Definition bitwise_and (a1 a2: approx) :=
+  if bge Int8u a1 || bge Int8u a2 then Int8u
+  else if bge Int16u a1 || bge Int16u a2 then Int16u
+  else Any.
+
+Definition bitwise_or (a1 a2: approx) :=
+  if bge Int8u a1 && bge Int8u a2 then Int8u
+  else if bge Int16u a1 && bge Int16u a2 then Int16u
+  else Any.
+
+Definition binop (op: binary_operation) (a1 a2: approx) :=
+  match op with
+  | Oand => bitwise_and a1 a2
+  | Oor | Oxor => bitwise_or a1 a2
+  | Ocmp _ => Int7
+  | Ocmpu _ => Int7
+  | Ocmpf _ => Int7
+  | _ => Any
+  end.
+
+End Approx.
+
+(** * Translation of expressions and statements. *)
+
 (** Generation of a Cminor expression for reading a Csharpminor variable. *)
 
-Definition var_get (cenv: compilenv) (id: ident): res expr :=
+Definition var_get (cenv: compilenv) (id: ident): res (expr * approx) :=
   match PMap.get id cenv with
   | Var_local chunk =>
-      OK(Evar (for_var id))
+      OK(Evar (for_var id), Approx.of_chunk chunk)
   | Var_stack_scalar chunk ofs =>
-      OK(Eload chunk (make_stackaddr ofs))
+      OK(Eload chunk (make_stackaddr ofs), Approx.of_chunk chunk)
   | Var_global_scalar chunk =>
-      OK(Eload chunk (make_globaladdr id))
+      OK(Eload chunk (make_globaladdr id), Approx.of_chunk chunk)
   | _ =>
       Error(msg "Cminorgen.var_get")
   end.
@@ -133,12 +271,12 @@ Definition var_get (cenv: compilenv) (id: ident): res expr :=
 (** Generation of a Cminor expression for taking the address of
   a Csharpminor variable. *)
 
-Definition var_addr (cenv: compilenv) (id: ident): res expr :=
+Definition var_addr (cenv: compilenv) (id: ident): res (expr * approx) :=
   match PMap.get id cenv with
   | Var_local chunk => Error(msg "Cminorgen.var_addr")
-  | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs)
-  | Var_stack_array ofs => OK (make_stackaddr ofs)
-  | _ => OK (make_globaladdr id)
+  | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs, Any)
+  | Var_stack_array ofs => OK (make_stackaddr ofs, Any)
+  | _ => OK (make_globaladdr id, Any)
   end.
 
 (** Generation of a Cminor statement performing an assignment to
@@ -175,38 +313,46 @@ Definition var_set_self (cenv: compilenv) (id: ident) (ty: typ) (k: stmt): res s
 
 (** Translation of constants. *)
 
-Definition transl_constant (cst: Csharpminor.constant): constant :=
+Definition transl_constant (cst: Csharpminor.constant): (constant * approx) :=
   match cst with
-  | Csharpminor.Ointconst n => Ointconst n
-  | Csharpminor.Ofloatconst n => Ofloatconst n
+  | Csharpminor.Ointconst n =>
+      (Ointconst n, Approx.of_int n)
+  | Csharpminor.Ofloatconst n =>
+      (Ofloatconst n, Approx.of_float n)
   end.
 
-(** Translation of expressions.  All the hard work is done by the
-  [make_*] and [var_*] functions defined above. *)
+(** Translation of expressions.  Return both a Cminor expression and
+  a compile-time approximation of the value of the original
+  C#minor expression, which is used to remove redundant casts. *)
 
 Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr)
-                     {struct e}: res expr :=
+                     {struct e}: res (expr * approx) :=
   match e with
-  | Csharpminor.Evar id => var_get cenv id
-  | Csharpminor.Etempvar id => OK (Evar (for_temp id))
-  | Csharpminor.Eaddrof id => var_addr cenv id
+  | Csharpminor.Evar id =>
+      var_get cenv id
+  | Csharpminor.Etempvar id =>
+      OK (Evar (for_temp id), Any)
+  | Csharpminor.Eaddrof id =>
+      var_addr cenv id
   | Csharpminor.Econst cst =>
-      OK (Econst (transl_constant cst))
+      let (tcst, a) := transl_constant cst in OK (Econst tcst, a)
   | Csharpminor.Eunop op e1 =>
-      do te1 <- transl_expr cenv e1;
-      OK (Eunop op te1)
+      do (te1, a1)  <- transl_expr cenv e1;
+      if Approx.unop_is_redundant op a1
+      then OK (te1, a1)
+      else OK (make_unop op te1, Approx.unop op a1)
   | Csharpminor.Ebinop op e1 e2 =>
-      do te1 <- transl_expr cenv e1;
-      do te2 <- transl_expr cenv e2;
-      OK (Ebinop op te1 te2)
+      do (te1, a1) <- transl_expr cenv e1;
+      do (te2, a2) <- transl_expr cenv e2;
+      OK (Ebinop op te1 te2, Approx.binop op a1 a2)
   | Csharpminor.Eload chunk e =>
-      do te <- transl_expr cenv e;
-      OK (Eload chunk te)
+      do (te, a) <- transl_expr cenv e;
+      OK (Eload chunk te, Approx.of_chunk chunk)
   | Csharpminor.Econdition e1 e2 e3 =>
-      do te1 <- transl_expr cenv e1;
-      do te2 <- transl_expr cenv e2;
-      do te3 <- transl_expr cenv e3;
-      OK (Econdition te1 te2 te3)
+      do (te1, a1) <- transl_expr cenv e1;
+      do (te2, a2) <- transl_expr cenv e2;
+      do (te3, a3) <- transl_expr cenv e3;
+      OK (Econdition te1 te2 te3, Approx.lub a2 a3)
   end.
 
 Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr)
@@ -215,7 +361,7 @@ Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr)
   | nil =>
       OK nil
   | e1 :: e2 =>
-      do te1 <- transl_expr cenv e1;
+      do (te1, a1) <- transl_expr cenv e1;
       do te2 <- transl_exprlist cenv e2;
       OK (te1 :: te2)
   end.
@@ -261,12 +407,7 @@ Fixpoint switch_env (ls: lbl_stmt) (e: exit_env) {struct ls}: exit_env :=
   end.
 
 (** Translation of statements.  The nonobvious part is
-  the translation of [switch] statements, outlined above. 
-  Also note the additional type checks on arguments to calls and returns.
-  These checks should always succeed for C#minor code generated from
-  well-typed Clight code, but are necessary for the correctness proof
-  to go through.
-*)
+  the translation of [switch] statements, outlined above. *)
 
 Definition typ_of_opttyp (ot: option typ) :=
   match ot with None => Tint | Some t => t end.
@@ -278,17 +419,17 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv)
   | Csharpminor.Sskip =>
       OK Sskip
   | Csharpminor.Sassign id e =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       var_set cenv id te
   | Csharpminor.Sset id e =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       OK (Sassign (for_temp id) te)
   | Csharpminor.Sstore chunk e1 e2 =>
-      do te1 <- transl_expr cenv e1;
-      do te2 <- transl_expr cenv e2;
+      do (te1, a1) <- transl_expr cenv e1;
+      do (te2, a2) <- transl_expr cenv e2;
       OK (make_store chunk te1 te2)
   | Csharpminor.Scall optid sig e el =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       do tel <- transl_exprlist cenv el;
       OK (Scall (option_map for_temp optid) sig te tel)
   | Csharpminor.Sseq s1 s2 =>
@@ -296,7 +437,7 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv)
       do ts2 <- transl_stmt ret cenv xenv s2;
       OK (Sseq ts1 ts2)
   | Csharpminor.Sifthenelse e s1 s2 =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       do ts1 <- transl_stmt ret cenv xenv s1;
       do ts2 <- transl_stmt ret cenv xenv s2;
       OK (Sifthenelse te ts1 ts2)
@@ -311,12 +452,12 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv)
   | Csharpminor.Sswitch e ls =>
       let cases := switch_table ls O in
       let default := length cases in
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       transl_lblstmt ret cenv (switch_env ls xenv) ls (Sswitch te cases default)
   | Csharpminor.Sreturn None =>
       OK (Sreturn None)
   | Csharpminor.Sreturn (Some e) =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       OK (Sreturn (Some te))
   | Csharpminor.Slabel lbl s =>
       do ts <- transl_stmt ret cenv xenv s; OK (Slabel lbl ts)
@@ -336,6 +477,8 @@ with transl_lblstmt (ret: option typ) (cenv: compilenv)
       transl_lblstmt ret cenv (List.tail xenv) ls' (Sseq (Sblock body) ts)
   end.
 
+(** * Stack layout *)
+
 (** Computation of the set of variables whose address is taken in
   a piece of Csharpminor code. *)
 
@@ -455,6 +598,8 @@ Definition build_global_compilenv (p: Csharpminor.program) : compilenv :=
   List.fold_left assign_global_variable 
                  p.(prog_vars) (PMap.init Var_global_array).
 
+(** * Translation of functions *)
+
 (** Function parameters whose address is taken must be stored in their
   stack slots at function entry.  (Cminor passes these parameters in
   local variables.) *)