path: root/cfrontend/Cshmgen.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Translation from Clight to Csharpminor. *)

(** The main transformations performed by this first part are:
- Resolution of all type-dependent behaviours: overloaded operators
   are resolved, address computations for array and struct accesses
   are made explicit, etc.
- Translation of Clight's loops and [switch] statements into
   Csharpminor's simpler control structures.
*)

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.

(** * Csharpminor constructors *)

(** The following functions build Csharpminor expressions that compute
   the value of a C operation.  Most construction functions take
   as arguments
-  Csharpminor subexpressions that compute the values of the
     arguments of the operation;
-  The C types of the arguments of the operation.  These types
     are used to insert the necessary numeric conversions and to
     resolve operation overloading.
   Most of these functions return a [res expr], with [Error]
   denoting a case where the operation is not defined at the given types.
*)

Definition make_intconst (n: int) :=  Econst (Ointconst n).

Definition make_longconst (f: int64) :=  Econst (Olongconst f).

Definition make_floatconst (f: float) :=  Econst (Ofloatconst f).

Definition make_singleconst (f: float32) :=  Econst (Osingleconst f).

Definition make_ptrofsconst (n: Z) :=
  if Archi.ptr64 then make_longconst (Int64.repr n) else make_intconst (Int.repr n).

Definition make_singleoffloat (e: expr) := Eunop Osingleoffloat e.
Definition make_floatofsingle (e: expr) := Eunop Ofloatofsingle e.

Definition make_floatofint (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Ofloatofint e
  | Unsigned => Eunop Ofloatofintu e
  end.

Definition make_singleofint (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Osingleofint e
  | Unsigned => Eunop Osingleofintu e
  end.

Definition make_intoffloat (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Ointoffloat e
  | Unsigned => Eunop Ointuoffloat e
  end.

Definition make_intofsingle (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Ointofsingle e
  | Unsigned => Eunop Ointuofsingle e
  end.

Definition make_longofint (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Olongofint e
  | Unsigned => Eunop Olongofintu e
  end.

Definition make_floatoflong (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Ofloatoflong e
  | Unsigned => Eunop Ofloatoflongu e
  end.

Definition make_singleoflong (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Osingleoflong e
  | Unsigned => Eunop Osingleoflongu e
  end.

Definition make_longoffloat (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Olongoffloat e
  | Unsigned => Eunop Olonguoffloat e
  end.

Definition make_longofsingle (e: expr) (sg: signedness) :=
  match sg with
  | Signed => Eunop Olongofsingle e
  | Unsigned => Eunop Olonguofsingle e
  end.

Definition make_cmpu_ne_zero (e: expr) :=
  match e with
  | Ebinop (Ocmp c) e1 e2 => e
  | Ebinop (Ocmpu c) e1 e2 => e
  | Ebinop (Ocmpf c) e1 e2 => e
  | Ebinop (Ocmpfs c) e1 e2 => e
  | Ebinop (Ocmpl c) e1 e2 => e
  | Ebinop (Ocmplu c) e1 e2 => e
  | _ => Ebinop (Ocmpu Cne) e (make_intconst Int.zero)
  end.

(** Variants of [sizeof] and [alignof] that check that the given type is complete. *)

Definition sizeof (ce: composite_env) (t: type) : res Z :=
  if complete_type ce t
  then OK (Ctypes.sizeof ce t)
  else Error (msg "incomplete type").

Definition alignof (ce: composite_env) (t: type) : res Z :=
  if complete_type ce t
  then OK (Ctypes.alignof ce t)
  else Error (msg "incomplete type").

(** [make_cast from to e] applies to [e] the numeric conversions needed
   to transform a result of type [from] to a result of type [to]. *)

Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) :=
  match sz, si with
  | I8, Signed => Eunop Ocast8signed e
  | I8, Unsigned => Eunop Ocast8unsigned e
  | I16, Signed => Eunop Ocast16signed e
  | I16, Unsigned => Eunop Ocast16unsigned e
  | I32, _ => e
  | IBool, _ => make_cmpu_ne_zero e
  end.

Definition make_cast (from to: type) (e: expr) :=
  match classify_cast from to with
  | cast_case_pointer => OK e
  | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2)
  | cast_case_f2f => OK e
  | cast_case_s2s => OK e
  | cast_case_f2s => OK (make_singleoffloat e)
  | cast_case_s2f => OK (make_floatofsingle e)
  | cast_case_i2f si1 => OK (make_floatofint e si1)
  | cast_case_i2s si1 => OK (make_singleofint e si1)
  | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2)
  | cast_case_s2i sz2 si2 => OK (make_cast_int (make_intofsingle e si2) sz2 si2)
  | cast_case_l2l => OK e
  | cast_case_i2l si1 => OK (make_longofint e si1)
  | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2)
  | cast_case_l2f si1 => OK (make_floatoflong e si1)
  | cast_case_l2s si1 => OK (make_singleoflong e si1)
  | cast_case_f2l si2 => OK (make_longoffloat e si2)
  | cast_case_s2l si2 => OK (make_longofsingle e si2)
  | cast_case_i2bool => OK (make_cmpu_ne_zero e)
  | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero))
  | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero))
  | cast_case_l2bool => OK (Ebinop (Ocmplu Cne) e (make_longconst Int64.zero))
  | cast_case_struct id1 id2 => OK e
  | cast_case_union id1 id2 => OK e
  | cast_case_void => OK e
  | cast_case_default => Error (msg "Cshmgen.make_cast")
  end.

(** [make_boolean e ty] returns a Csharpminor expression that evaluates
   to the boolean value of [e].  *)

Definition make_boolean (e: expr) (ty: type) :=
  match classify_bool ty with
  | bool_case_i => make_cmpu_ne_zero e
  | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
  | bool_case_s => Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero)
  | bool_case_l => Ebinop (Ocmplu Cne) e (make_longconst Int64.zero)
  | bool_default => e   (**r should not happen *)
  end.

(** Unary operators *)

Definition make_notbool (e: expr) (ty: type) :=
  match classify_bool ty with
  | bool_case_i => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero))
  | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero))
  | bool_case_s => OK (Ebinop (Ocmpfs Ceq) e (make_singleconst Float32.zero))
  | bool_case_l => OK (Ebinop (Ocmplu Ceq) e (make_longconst Int64.zero))
  | bool_default => Error (msg "Cshmgen.make_notbool")
  end.

Definition make_neg (e: expr) (ty: type) :=
  match classify_neg ty with
  | neg_case_i _ => OK (Eunop Onegint e)
  | neg_case_f => OK (Eunop Onegf e)
  | neg_case_s => OK (Eunop Onegfs e)
  | neg_case_l _ => OK (Eunop Onegl e)
  | neg_default => Error (msg "Cshmgen.make_neg")
  end.

Definition make_absfloat (e: expr) (ty: type) :=
  match classify_neg ty with
  | neg_case_i sg => OK (Eunop Oabsf (make_floatofint e sg))
  | neg_case_f => OK (Eunop Oabsf e)
  | neg_case_s => OK (Eunop Oabsf (make_floatofsingle e))
  | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg))
  | neg_default => Error (msg "Cshmgen.make_absfloat")
  end.

Definition make_notint (e: expr) (ty: type) :=
  match classify_notint ty with
  | notint_case_i _ => OK (Eunop Onotint e)
  | notint_case_l _ => OK (Eunop Onotl e)
  | notint_default => Error (msg "Cshmgen.make_notint")
  end.

(** Binary operators *)

Definition make_binarith (iop iopu fop sop lop lopu: binary_operation)
                         (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  let c := classify_binarith ty1 ty2 in
  let ty := binarith_type c in
  do e1' <- make_cast ty1 ty e1;
  do e2' <- make_cast ty2 ty e2;
  match c with
  | bin_case_i Signed => OK (Ebinop iop e1' e2')
  | bin_case_i Unsigned => OK (Ebinop iopu e1' e2')
  | bin_case_f => OK (Ebinop fop e1' e2')
  | bin_case_s => OK (Ebinop sop e1' e2')
  | bin_case_l Signed => OK (Ebinop lop e1' e2')
  | bin_case_l Unsigned => OK (Ebinop lopu e1' e2')
  | bin_default => Error (msg "Cshmgen.make_binarith")
  end.

Definition make_add_ptr_int (ce: composite_env) (ty: type) (si: signedness) (e1 e2: expr) :=
  do sz <- sizeof ce ty;
  if Archi.ptr64 then
    let n := make_longconst (Int64.repr sz) in
    OK (Ebinop Oaddl e1 (Ebinop Omull n (make_longofint e2 si)))
  else
    let n := make_intconst (Int.repr sz) in
    OK (Ebinop Oadd e1 (Ebinop Omul n e2)).

Definition make_add_ptr_long (ce: composite_env) (ty: type) (e1 e2: expr) :=
  do sz <- sizeof ce ty;
  if Archi.ptr64 then
    let n := make_longconst (Int64.repr sz) in
    OK (Ebinop Oaddl e1 (Ebinop Omull n e2))
  else
    let n := make_intconst (Int.repr sz) in
    OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))).

Definition make_expect (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  make_binarith (Oexpect AST.Tint) (Oexpect AST.Tint)
                (Oexpect AST.Tfloat) (Oexpect AST.Tsingle)
                (Oexpect AST.Tlong) (Oexpect AST.Tlong) e1 ty1 e2 ty2.

Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_add ty1 ty2 with
  | add_case_pi ty si => make_add_ptr_int ce ty si e1 e2
  | add_case_pl ty => make_add_ptr_long ce ty e1 e2
  | add_case_ip si ty => make_add_ptr_int ce ty si e2 e1
  | add_case_lp ty => make_add_ptr_long ce ty e2 e1
  | add_default => make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2
  end.

Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_sub ty1 ty2 with
  | sub_case_pi ty si =>
      do sz <- sizeof ce ty;
      if Archi.ptr64 then
        let n := make_longconst (Int64.repr sz) in
        OK (Ebinop Osubl e1 (Ebinop Omull n (make_longofint e2 si)))
      else
        let n := make_intconst (Int.repr sz) in
        OK (Ebinop Osub e1 (Ebinop Omul n e2))
  | sub_case_pp ty =>
      do sz <- sizeof ce ty;
      if Archi.ptr64 then
        let n := make_longconst (Int64.repr sz) in
        OK (Ebinop Odivl (Ebinop Osubl e1 e2) n)
      else
        let n := make_intconst (Int.repr sz) in
        OK (Ebinop Odiv (Ebinop Osub e1 e2) n)
  | sub_case_pl ty =>
      do sz <- sizeof ce ty;
      if Archi.ptr64 then
        let n := make_longconst (Int64.repr sz) in
        OK (Ebinop Osubl e1 (Ebinop Omull n e2))
      else
        let n := make_intconst (Int.repr sz) in
        OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
  | sub_default =>
      make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2
  end.

Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  make_binarith Omul Omul Omulf Omulfs Omull Omull e1 ty1 e2 ty2.

Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  make_binarith Odiv Odivu Odivf Odivfs Odivl Odivlu e1 ty1 e2 ty2.

Definition make_binarith_int (iop iopu lop lopu: binary_operation)
                             (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  let c := classify_binarith ty1 ty2 in
  let ty := binarith_type c in
  do e1' <- make_cast ty1 ty e1;
  do e2' <- make_cast ty2 ty e2;
  match c with
  | bin_case_i Signed => OK (Ebinop iop e1' e2')
  | bin_case_i Unsigned => OK (Ebinop iopu e1' e2')
  | bin_case_l Signed => OK (Ebinop lop e1' e2')
  | bin_case_l Unsigned => OK (Ebinop lopu e1' e2')
  | bin_case_f | bin_case_s | bin_default => Error (msg "Cshmgen.make_binarith_int")
  end.

Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  make_binarith_int Omod Omodu Omodl Omodlu e1 ty1 e2 ty2.

Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  make_binarith_int Oand Oand Oandl Oandl e1 ty1 e2 ty2.

Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  make_binarith_int Oor Oor Oorl Oorl e1 ty1 e2 ty2.

Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  make_binarith_int Oxor Oxor Oxorl Oxorl e1 ty1 e2 ty2.

Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_shift ty1 ty2 with
  | shift_case_ii _ => OK (Ebinop Oshl e1 e2)
  | shift_case_li _ => OK (Ebinop Oshll e1 e2)
  | shift_case_il _ => OK (Ebinop Oshl e1 (Eunop Ointoflong e2))
  | shift_case_ll _ => OK (Ebinop Oshll e1 (Eunop Ointoflong e2))
  | shift_default => Error (msg "Cshmgen.make_shl")
  end.

Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_shift ty1 ty2 with
  | shift_case_ii Signed => OK (Ebinop Oshr e1 e2)
  | shift_case_ii Unsigned => OK (Ebinop Oshru e1 e2)
  | shift_case_li Signed => OK (Ebinop Oshrl e1 e2)
  | shift_case_li Unsigned => OK (Ebinop Oshrlu e1 e2)
  | shift_case_il Signed => OK (Ebinop Oshr e1 (Eunop Ointoflong e2))
  | shift_case_il Unsigned => OK (Ebinop Oshru e1 (Eunop Ointoflong e2))
  | shift_case_ll Signed => OK (Ebinop Oshrl e1 (Eunop Ointoflong e2))
  | shift_case_ll Unsigned => OK (Ebinop Oshrlu e1 (Eunop Ointoflong e2))
  | shift_default => Error (msg "Cshmgen.make_shr")
  end.

Definition make_cmp_ptr (c: comparison) (e1 e2: expr) :=
  Ebinop (if Archi.ptr64 then Ocmplu c else Ocmpu c) e1 e2.

Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_cmp ty1 ty2 with
  | cmp_case_pp => OK (make_cmp_ptr c e1 e2)
  | cmp_case_pi si =>
      OK (make_cmp_ptr c e1 (if Archi.ptr64 then make_longofint e2 si else e2))
  | cmp_case_ip si =>
      OK (make_cmp_ptr c (if Archi.ptr64 then make_longofint e1 si else e1) e2)
  | cmp_case_pl =>
      OK (make_cmp_ptr c e1 (if Archi.ptr64 then e2 else Eunop Ointoflong e2))
  | cmp_case_lp =>
      OK (make_cmp_ptr c (if Archi.ptr64 then e1 else Eunop Ointoflong e1) e2)
  | cmp_default =>
      make_binarith
        (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpfs c) (Ocmpl c) (Ocmplu c)
        e1 ty1 e2 ty2
  end.

(** Auxiliary for translating bitfield accesses *)

Definition make_extract_bitfield (sz: intsize) (sg: signedness) (pos width: Z)
                                 (addr: expr) : res expr :=
  if zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz) then
    let amount1 := Int.repr (Int.zwordsize - first_bit sz pos width - width) in
    let amount2 := Int.repr (Int.zwordsize - width) in
    let e1 := Eload (chunk_for_carrier sz) addr in
    let e2 := Ebinop Oshl e1 (make_intconst amount1) in
    let e3 := Ebinop (if intsize_eq sz IBool
                      || signedness_eq sg Unsigned then Oshru else Oshr)
                     e2 (make_intconst amount2) in
    OK e3
  else
    Error(msg "Cshmgen.extract_bitfield").

(** [make_load addr ty_res] loads a value of type [ty_res] from
   the memory location denoted by the Csharpminor expression [addr]
   and the bitfield designator [bf].
   If [ty_res] is an array or function type, returns [addr] instead,
   as consistent with C semantics.
*)

Definition make_load (addr: expr) (ty_res: type) (bf: bitfield) :=
  match bf with
  | Full =>
      match access_mode ty_res with
      | By_value chunk => OK (Eload chunk addr)
      | By_reference => OK addr
      | By_copy => OK addr
      | By_nothing => Error (msg "Cshmgen.make_load")
      end
  | Bits sz sg pos width =>
      make_extract_bitfield sz sg pos width addr
  end.

(** Auxiliary for translating bitfield updates *)

Definition make_store_bitfield (sz: intsize) (sg: signedness) (pos width: Z)
                               (addr val: expr) : res stmt :=
  if zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz) then
    let amount := first_bit sz pos width in
    let mask := Int.shl (Int.repr (two_p width - 1)) (Int.repr amount) in
    let e1 := Eload (chunk_for_carrier sz) addr in
    let e2 := Ebinop Oshl val (make_intconst (Int.repr amount)) in
    let e3 := Ebinop Oor (Ebinop Oand e2 (make_intconst mask))
                         (Ebinop Oand e1 (make_intconst (Int.not mask))) in
    OK (Sstore (chunk_for_carrier sz) addr e3)
  else
    Error(msg "Cshmgen.make_store_bitfield").

(** [make_memcpy dst src ty] returns a [memcpy] builtin appropriate for
  by-copy assignment of a value of Clight type [ty]. *)

Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) :=
  do sz <- sizeof ce ty;
  OK (Sbuiltin None (EF_memcpy sz (Ctypes.alignof_blockcopy ce ty))
                    (dst :: src :: nil)).

(** [make_store addr ty bf rhs] stores the value of the
   Csharpminor expression [rhs] into the memory location denoted by the
   Csharpminor expression [addr].
   [ty] is the type of the memory location and [bf] a bitfield designator. *)

Definition make_store (ce: composite_env) (addr: expr) (ty: type) (bf: bitfield) (rhs: expr) :=
  match bf with
  | Full =>
      match access_mode ty with
      | By_value chunk => OK (Sstore chunk addr rhs)
      | By_copy => make_memcpy ce addr rhs ty
      | _ => Error (msg "Cshmgen.make_store")
      end
  | Bits sz sg pos width =>
      make_store_bitfield sz sg pos width addr rhs
  end.

(** ** Translation of operators *)

Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr :=
  match op with
  | Cop.Onotbool => make_notbool a ta
  | Cop.Onotint => make_notint a ta
  | Cop.Oneg => make_neg a ta
  | Cop.Oabsfloat => make_absfloat a ta
  end.

Definition transl_binop (ce: composite_env)
                        (op: Cop.binary_operation)
                        (a: expr) (ta: type)
                        (b: expr) (tb: type) : res expr :=
  match op with
  | Cop.Oexpect => make_expect a ta b tb
  | Cop.Oadd => make_add ce a ta b tb
  | Cop.Osub => make_sub ce a ta b tb
  | Cop.Omul => make_mul a ta b tb
  | Cop.Odiv => make_div a ta b tb
  | Cop.Omod => make_mod a ta b tb
  | Cop.Oand => make_and a ta b tb
  | Cop.Oor  => make_or a ta b tb
  | Cop.Oxor => make_xor a ta b tb
  | Cop.Oshl => make_shl a ta b tb
  | Cop.Oshr => make_shr a ta b tb
  | Cop.Oeq => make_cmp Ceq a ta b tb
  | Cop.One => make_cmp Cne a ta b tb
  | Cop.Olt => make_cmp Clt a ta b tb
  | Cop.Ogt => make_cmp Cgt a ta b tb
  | Cop.Ole => make_cmp Cle a ta b tb
  | Cop.Oge => make_cmp Cge a ta b tb
  end.

(** ** Translation of field accesses *)

Definition make_field_access (ce: composite_env) (ty: type) (f: ident) (a: expr) : res (expr * bitfield) :=
  do (ofs, bf) <-
    match ty with
    | Tstruct id _ =>
        match ce!id with
        | None => Error (MSG "Undefined struct " :: CTX id :: nil)
        | Some co => field_offset ce f (co_members co)
        end
    | Tunion id _ =>
        match ce!id with
        | None => Error (MSG "Undefined union " :: CTX id :: nil)
        | Some co => union_field_offset ce f (co_members co)
        end
    | _ =>
        Error(msg "Cshmgen.make_field_access")
    end;
  let a' :=
    if Archi.ptr64
    then Ebinop Oaddl a (make_longconst (Int64.repr ofs))
    else Ebinop Oadd a (make_intconst (Int.repr ofs)) in
  OK (a', bf).

(** * Translation of expressions *)

(** [transl_expr a] returns the Csharpminor code that computes the value
   of expression [a]. The computation is performed in the error monad
   (see module [Errors]) to enable error reporting. *)

Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr :=
  match a with
  | Clight.Econst_int n _ =>
      OK(make_intconst n)
  | Clight.Econst_float n _ =>
      OK(make_floatconst n)
  | Clight.Econst_single n _ =>
      OK(make_singleconst n)
  | Clight.Econst_long n _ =>
      OK(make_longconst n)
  | Clight.Evar id ty =>
      make_load (Eaddrof id) ty Full
  | Clight.Etempvar id ty =>
      OK(Evar id)
  | Clight.Ederef b ty =>
      do tb <- transl_expr ce b;
      make_load tb ty Full
  | Clight.Eaddrof b _ =>
      do (tb, bf) <- transl_lvalue ce b;
      match bf with
      | Full => OK tb
      | Bits _ _ _ _ => Error (msg "Cshmgen.transl_expr: addrof bitfield")
      end
  | Clight.Eunop op b _ =>
      do tb <- transl_expr ce b;
      transl_unop op tb (typeof b)
  | Clight.Ebinop op b c _ =>
      do tb <- transl_expr ce b;
      do tc <- transl_expr ce c;
      transl_binop ce op tb (typeof b) tc (typeof c)
  | Clight.Ecast b ty =>
      do tb <- transl_expr ce b;
      make_cast (typeof b) ty tb
  | Clight.Efield b i ty =>
      do tb <- transl_expr ce b;
      do (addr, bf) <- make_field_access ce (typeof b) i tb;
      make_load addr ty bf
  | Clight.Esizeof ty' ty =>
      do sz <- sizeof ce ty'; OK(make_ptrofsconst sz)
  | Clight.Ealignof ty' ty =>
      do al <- alignof ce ty'; OK(make_ptrofsconst al)
  end

(** [transl_lvalue a] returns the Csharpminor code that evaluates
   [a] as a lvalue, that is, code that returns the memory address
   where the value of [a] is stored.  It also returns the bitfield to be
   accessed at this address, if appropriate.
*)

with transl_lvalue (ce: composite_env) (a: Clight.expr) {struct a} : res (expr * bitfield) :=
  match a with
  | Clight.Evar id _ =>
      OK (Eaddrof id, Full)
  | Clight.Ederef b _ =>
      do tb <- transl_expr ce b; OK (tb, Full)
  | Clight.Efield b i ty =>
      do tb <- transl_expr ce b;
      make_field_access ce (typeof b) i tb
  | _ =>
      Error(msg "Cshmgen.transl_lvalue")
  end.

(** [transl_arglist al tyl] returns a list of Csharpminor expressions
   that compute the values of the list [al] of Clight expressions,
   casted to the corresponding types in [tyl].
   Used for function applications. *)

Fixpoint transl_arglist (ce: composite_env) (al: list Clight.expr) (tyl: typelist)
                         {struct al}: res (list expr) :=
  match al, tyl with
  | nil, Tnil => OK nil
  | a1 :: a2, Tcons ty1 ty2 =>
      do ta1 <- transl_expr ce a1;
      do ta1' <- make_cast (typeof a1) ty1 ta1;
      do ta2 <- transl_arglist ce a2 ty2;
      OK (ta1' :: ta2)
  | a1 :: a2, Tnil =>
      (* Tolerance for calls to K&R or variadic functions *)
      do ta1 <- transl_expr ce a1;
      do ta1' <- make_cast (typeof a1) (default_argument_conversion (typeof a1)) ta1;
      do ta2 <- transl_arglist ce a2 Tnil;
      OK (ta1' :: ta2)
  | _, _ =>
      Error(msg "Cshmgen.transl_arglist: arity mismatch")
  end.

(** Compute the argument signature that corresponds to a function application. *)

Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist)
                            {struct al}: list AST.typ :=
  match al, tyl with
  | nil, _ => nil
  | a1 :: a2, Tcons ty1 ty2 =>
      typ_of_type ty1 :: typlist_of_arglist a2 ty2
  | a1 :: a2, Tnil =>
      (* Tolerance for calls to K&R or variadic functions *)
      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
   that performs the same computations as the CabsCoq statement [s].

   If the statement [s] terminates prematurely on a [break] construct,
   the generated Csharpminor statement terminates prematurely on an
   [exit nbrk] construct.

   If the statement [s] terminates prematurely on a [continue]
   construct, the generated Csharpminor statement terminates
   prematurely on an [exit ncnt] construct.

   The general translation for loops is as follows:
<<
loop s1 s2          --->     block {
                               loop {
                                 block { s1 };
                                 // continue in s1 branches here
                                 s2;
                               }
                             }
                             // break in s1 and s2 branches here
*)

Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
                          (s: Clight.statement) {struct s} : res stmt :=
  match s with
  | Clight.Sskip =>
      OK Sskip
  | Clight.Sassign b c =>
      do (tb, bf) <- transl_lvalue ce b;
      do tc <- transl_expr ce c;
      do tc' <- make_cast (typeof c) (typeof b) tc;
      make_store ce tb (typeof b) bf tc'
  | Clight.Sset x b =>
      do tb <- transl_expr ce b;
      OK(Sset x tb)
  | Clight.Scall x b cl =>
      match classify_fun (typeof b) with
      | fun_case_f args res cconv =>
          do tb <- transl_expr ce b;
          do tcl <- transl_arglist ce cl args;
          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 =>
      do tbl <- transl_arglist ce bl tyargs;
      OK(Sbuiltin x ef tbl)
  | Clight.Ssequence s1 s2 =>
      do ts1 <- transl_statement ce tyret nbrk ncnt s1;
      do ts2 <- transl_statement ce tyret nbrk ncnt s2;
      OK (Sseq ts1 ts2)
  | Clight.Sifthenelse e s1 s2 =>
      do te <- transl_expr ce e;
      do ts1 <- transl_statement ce tyret nbrk ncnt s1;
      do ts2 <- transl_statement ce tyret nbrk ncnt s2;
      OK (Sifthenelse (make_boolean te (typeof e)) ts1 ts2)
  | Clight.Sloop s1 s2 =>
      do ts1 <- transl_statement ce tyret 1%nat 0%nat s1;
      do ts2 <- transl_statement ce tyret 0%nat (S ncnt) s2;
      OK (Sblock (Sloop (Sseq (Sblock ts1) ts2)))
  | Clight.Sbreak =>
      OK (Sexit nbrk)
  | Clight.Scontinue =>
      OK (Sexit ncnt)
  | Clight.Sreturn (Some e) =>
      do te <- transl_expr ce e;
      do te' <- make_cast (typeof e) tyret te;
      OK (Sreturn (Some te'))
  | Clight.Sreturn None =>
      OK (Sreturn None)
  | Clight.Sswitch a sl =>
      do ta <- transl_expr ce a;
      do tsl <- transl_lbl_stmt ce tyret 0%nat (S ncnt) sl;
      match classify_switch (typeof a) with
      | switch_case_i => OK (Sblock (Sswitch false ta tsl))
      | switch_case_l => OK (Sblock (Sswitch true ta tsl))
      | switch_default => Error(msg "Cshmgen.transl_stmt(switch)")
      end
  | Clight.Slabel lbl s =>
      do ts <- transl_statement ce tyret nbrk ncnt s;
      OK (Slabel lbl ts)
  | Clight.Sgoto lbl =>
      OK (Sgoto lbl)
  end

with transl_lbl_stmt (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
                     (sl: Clight.labeled_statements)
                     {struct sl}: res lbl_stmt :=
  match sl with
  | Clight.LSnil =>
      OK LSnil
  | Clight.LScons n s sl' =>
      do ts <- transl_statement ce tyret nbrk ncnt s;
      do tsl' <- transl_lbl_stmt ce tyret nbrk ncnt sl';
      OK (LScons n ts tsl')
  end.

(*** Translation of functions *)

Definition transl_var (ce: composite_env) (v: ident * type) :=
  do sz <- sizeof ce (snd v); OK (fst v, sz).

Definition signature_of_function (f: Clight.function) :=
  {| sig_args := map typ_of_type (map snd (Clight.fn_params f));
     sig_res  := rettype_of_type (Clight.fn_return f);
     sig_cc   := Clight.fn_callconv f |}.

Definition transl_function (ce: composite_env) (f: Clight.function) : res function :=
  do tbody <- transl_statement ce f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f);
  do tvars <- mmap (transl_var ce) (Clight.fn_vars f);
  OK (mkfunction
       (signature_of_function f)
       (map fst (Clight.fn_params f))
       tvars
       (map fst (Clight.fn_temps f))
       tbody).

Definition transl_fundef (ce: composite_env) (id: ident) (f: Clight.fundef) : res fundef :=
  match f with
  | Internal g =>
      do tg <- transl_function ce g; OK(AST.Internal tg)
  | External ef args res cconv =>
      if signature_eq (ef_sig ef) (signature_of_type args res cconv)
      then OK(AST.External ef)
      else Error(msg "Cshmgen.transl_fundef: wrong external signature")
  end.

(** ** Translation of programs *)

Definition transl_globvar (id: ident) (ty: type) := OK tt.

Definition transl_program (p: Clight.program) : res program :=
  transform_partial_program2 (transl_fundef p.(prog_comp_env)) transl_globvar p.