Require Import Coqlib.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import AST.
Require Import Csyntax.
Require Import Clight.
Require Import Cminor.
Require Import Csharpminor.

Open Local Scope string_scope.
Open Local Scope error_monad_scope.

Operations on C types

Definition chunk_of_type (ty: type): res memory_chunk :=
  match access_mode ty with
  | By_value chunk => OK chunk
  | _ => Error (msg "Cshmgen.chunk_of_type")
  end.


Definition var_kind_of_type (ty: type): res var_kind :=
  match ty with
  | Tint I8 Signed _ => OK(Vscalar Mint8signed)
  | Tint I8 Unsigned _ => OK(Vscalar Mint8unsigned)
  | Tint I16 Signed _ => OK(Vscalar Mint16signed)
  | Tint I16 Unsigned _ => OK(Vscalar Mint16unsigned)
  | Tint I32 _ _ => OK(Vscalar Mint32)
  | Tint IBool _ _ => OK(Vscalar Mint8unsigned)
  | Tfloat F32 _ => OK(Vscalar Mfloat32)
  | Tfloat F64 _ => OK(Vscalar Mfloat64)
  | Tvoid => Error (msg "Cshmgen.var_kind_of_type(void)")
  | Tpointer _ _ => OK(Vscalar Mint32)
  | Tarray _ _ _ => OK(Varray (Csyntax.sizeof ty) (Csyntax.alignof ty))
  | Tfunction _ _ => Error (msg "Cshmgen.var_kind_of_type(function)")
  | Tstruct _ fList _ => OK(Varray (Csyntax.sizeof ty) (Csyntax.alignof ty))
  | Tunion _ fList _ => OK(Varray (Csyntax.sizeof ty) (Csyntax.alignof ty))
  | Tcomp_ptr _ _ => OK(Vscalar Mint32)
end.
  

Csharpminor constructors

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

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

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

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

Definition make_boolean (e: expr) (ty: type) :=
  match ty with
  | Tfloat _ _ => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
  | _ => e
  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)
  | _ => Error (msg "Cshmgen.make_neg")
  end.

Definition make_notbool (e: expr) (ty: type) :=
  match classify_bool ty with
  | bool_case_ip => OK (Eunop Onotbool e)
  | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero))
  | _ => Error (msg "Cshmgen.make_notbool")
  end.

Definition make_notint (e: expr) (ty: type) :=
  Eunop Onotint e.

Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_add ty1 ty2 with
  | add_case_ii _ => OK (Ebinop Oadd e1 e2)
  | add_case_ff => OK (Ebinop Oaddf e1 e2)
  | add_case_if sg => OK (Ebinop Oaddf (make_floatofint e1 sg) e2)
  | add_case_fi sg => OK (Ebinop Oaddf e1 (make_floatofint e2 sg))
  | add_case_pi ty _ =>
      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
      OK (Ebinop Oadd e1 (Ebinop Omul n e2))
  | add_case_ip ty _ =>
      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
      OK (Ebinop Oadd e2 (Ebinop Omul n e1))
  | add_default => Error (msg "Cshmgen.make_add")
  end.

Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_sub ty1 ty2 with
  | sub_case_ii _ => OK (Ebinop Osub e1 e2)
  | sub_case_ff => OK (Ebinop Osubf e1 e2)
  | sub_case_if sg => OK (Ebinop Osubf (make_floatofint e1 sg) e2)
  | sub_case_fi sg => OK (Ebinop Osubf e1 (make_floatofint e2 sg))
  | sub_case_pi ty =>
      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
      OK (Ebinop Osub e1 (Ebinop Omul n e2))
  | sub_case_pp ty =>
      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
      OK (Ebinop Odivu (Ebinop Osub e1 e2) n)
  | sub_default => Error (msg "Cshmgen.make_sub")
  end.

Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_mul ty1 ty2 with
  | mul_case_ii _ => OK (Ebinop Omul e1 e2)
  | mul_case_ff => OK (Ebinop Omulf e1 e2)
  | mul_case_if sg => OK (Ebinop Omulf (make_floatofint e1 sg) e2)
  | mul_case_fi sg => OK (Ebinop Omulf e1 (make_floatofint e2 sg))
  | mul_default => Error (msg "Cshmgen.make_mul")
  end.

Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_div ty1 ty2 with
  | div_case_ii Unsigned => OK (Ebinop Odivu e1 e2)
  | div_case_ii Signed => OK (Ebinop Odiv e1 e2)
  | div_case_ff => OK (Ebinop Odivf e1 e2)
  | div_case_if sg => OK (Ebinop Odivf (make_floatofint e1 sg) e2)
  | div_case_fi sg => OK (Ebinop Odivf e1 (make_floatofint e2 sg))
  | div_default => Error (msg "Cshmgen.make_div")
  end.

Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_binint ty1 ty2 with
  | binint_case_ii Unsigned => OK (Ebinop Omodu e1 e2)
  | binint_case_ii Signed => OK (Ebinop Omod e1 e2)
  | mod_default => Error (msg "Cshmgen.make_mod")
  end.

Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  OK(Ebinop Oand e1 e2).

Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  OK(Ebinop Oor e1 e2).

Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  OK(Ebinop Oxor e1 e2).

Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  OK(Ebinop Oshl e1 e2).

Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_shift ty1 ty2 with
  | shift_case_ii Unsigned => OK (Ebinop Oshru e1 e2)
  | shift_case_ii Signed => OK (Ebinop Oshr e1 e2)
  | shr_default => Error (msg "Cshmgen.make_shr")
  end.

Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
  match classify_cmp ty1 ty2 with
  | cmp_case_ii Signed => OK (Ebinop (Ocmp c) e1 e2)
  | cmp_case_ii Unsigned => OK (Ebinop (Ocmpu c) e1 e2)
  | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2)
  | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2)
  | cmp_case_if sg => OK (Ebinop (Ocmpf c) (make_floatofint e1 sg) e2)
  | cmp_case_fi sg => OK (Ebinop (Ocmpf c) e1 (make_floatofint e2 sg))
  | cmp_default => Error (msg "Cshmgen.make_cmp")
  end.


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, _ => Eunop Oboolval e
  end.

Definition make_cast_float (e: expr) (sz: floatsize) :=
  match sz with
  | F32 => Eunop Osingleoffloat e
  | F64 => e
  end.

Definition make_cast (from to: type) (e: expr) :=
  match classify_cast from to with
  | cast_case_neutral => e
  | cast_case_i2i sz2 si2 => make_cast_int e sz2 si2
  | cast_case_f2f sz2 => make_cast_float e sz2
  | cast_case_i2f si1 sz2 => make_cast_float (make_floatofint e si1) sz2
  | cast_case_f2i sz2 si2 => make_cast_int (make_intoffloat e si2) sz2 si2
  | cast_case_ip2bool => Eunop Oboolval e
  | cast_case_f2bool => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
  | cast_case_struct id1 fld1 id2 fld2 => e
  | cast_case_union id1 fld1 id2 fld2 => e
  | cast_case_void => e
  | cast_case_default => e
  end.


Definition make_load (addr: expr) (ty_res: type) :=
  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.


Definition make_vol_load (dst: ident) (addr: expr) (ty: type) :=
  match (access_mode ty) with
  | By_value chunk => OK (Sbuiltin (Some dst) (EF_vload chunk) (addr :: nil))
  | By_reference => OK (Sset dst addr)
  | By_copy => OK (Sset dst addr)
  | By_nothing => Error (msg "Cshmgen.make_vol_load")
  end.


Definition make_memcpy (dst src: expr) (ty: type) :=
  Sbuiltin None (EF_memcpy (Csyntax.sizeof ty) (Zmin (Csyntax.alignof ty) 4))
                (dst :: src :: nil).


Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
  match access_mode ty with
  | By_value chunk => OK (Sstore chunk addr rhs)
  | By_copy => OK (make_memcpy addr rhs ty)
  | _ => Error (msg "Cshmgen.make_store")
  end.


Definition make_vol_store (addr: expr) (ty: type) (rhs: expr) :=
  match access_mode ty with
  | By_value chunk => OK (Sbuiltin None (EF_vstore chunk) (addr :: rhs :: nil))
  | By_copy => OK (make_memcpy addr rhs ty)
  | _ => Error (msg "Cshmgen.make_store")
  end.

Reading and writing variables

Definition is_variable (e: Clight.expr) : option ident :=
  match e with
  | Clight.Evar id _ => Some id
  | _ => None
  end.


Definition var_get (id: ident) (ty: type) :=
  match access_mode ty with
  | By_value chunk => OK (Evar id)
  | By_reference => OK (Eaddrof id)
  | By_copy => OK (Eaddrof id)
  | _ => Error (MSG "Cshmgen.var_get " :: CTX id :: nil)
  end.


Definition var_set (id: ident) (ty: type) (rhs: expr) :=
  match access_mode ty with
  | By_value chunk => OK (Sassign id rhs)
  | By_copy => OK (make_memcpy (Eaddrof id) rhs ty)
  | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil)
  end.

Translation of operators

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

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

Translation of expressions

Fixpoint transl_expr (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.Evar id ty =>
      var_get id ty
  | Clight.Etempvar id ty =>
      OK(Etempvar id)
  | Clight.Ederef b _ =>
      do tb <- transl_expr b;
      make_load tb (typeof a)
  | Clight.Eaddrof b _ =>
      transl_lvalue b
  | Clight.Eunop op b _ =>
      do tb <- transl_expr b;
      transl_unop op tb (typeof b)
  | Clight.Ebinop op b c _ =>
      do tb <- transl_expr b;
      do tc <- transl_expr c;
      transl_binop op tb (typeof b) tc (typeof c)
  | Clight.Ecast b ty =>
      do tb <- transl_expr b;
      OK (make_cast (typeof b) ty tb)
  | Clight.Econdition b c d ty =>
      do tb <- transl_expr b;
      do tc <- transl_expr c;
      do td <- transl_expr d;
      OK(Econdition (make_boolean tb (typeof b))
                    (make_cast (typeof c) ty tc)
                    (make_cast (typeof d) ty td))
  | Clight.Efield b i ty =>
      match typeof b with
      | Tstruct _ fld _ =>
          do tb <- transl_expr b;
          do ofs <- field_offset i fld;
          make_load
            (Ebinop Oadd tb (make_intconst (Int.repr ofs)))
            ty
      | Tunion _ fld _ =>
          do tb <- transl_expr b;
          make_load tb ty
      | _ =>
          Error(msg "Cshmgen.transl_expr(field)")
      end
  end


with transl_lvalue (a: Clight.expr) {struct a} : res expr :=
  match a with
  | Clight.Evar id _ =>
      OK (Eaddrof id)
  | Clight.Ederef b _ =>
      transl_expr b
  | Clight.Efield b i ty =>
      match typeof b with
      | Tstruct _ fld _ =>
          do tb <- transl_expr b;
          do ofs <- field_offset i fld;
          OK (Ebinop Oadd tb (make_intconst (Int.repr ofs)))
      | Tunion _ fld _ =>
          transl_expr b
      | _ =>
          Error(msg "Cshmgen.transl_lvalue(field)")
      end
  | _ =>
      Error(msg "Cshmgen.transl_lvalue")
  end.


Fixpoint transl_exprlist (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 a1;
      do ta2 <- transl_exprlist a2 ty2;
      OK (make_cast (typeof a1) ty1 ta1 :: ta2)
  | _, _ =>
      Error(msg "Cshmgen.transl_exprlist: arity mismatch")
  end.

Translation of statements

Definition is_constant_bool (e: expr) : option bool :=
  match e with
  | Econst (Ointconst n) => Some (negb (Int.eq n Int.zero))
  | _ => None
  end.

Definition exit_if_false (e: Clight.expr) : res stmt :=
  do te <- transl_expr e;
  match is_constant_bool te with
  | Some true => OK(Sskip)
  | Some false => OK(Sexit 0%nat)
  | None =>
      OK(Sifthenelse
            (make_boolean te (typeof e))
            Sskip
            (Sexit 0%nat))
  end.


Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat)
                          (s: Clight.statement) {struct s} : res stmt :=
  match s with
  | Clight.Sskip =>
      OK Sskip
  | Clight.Sassign b c =>
      if type_is_volatile (typeof b) then
         (do tb <- transl_lvalue b;
          do tc <- transl_expr c;
          make_vol_store tb (typeof b) (make_cast (typeof c) (typeof b) tc))
      else match is_variable b with
      | Some id =>
          do tc <- transl_expr c;
          var_set id (typeof b) (make_cast (typeof c) (typeof b) tc)
      | None =>
          do tb <- transl_lvalue b;
          do tc <- transl_expr c;
          make_store tb (typeof b) (make_cast (typeof c) (typeof b) tc)
      end
  | Clight.Sset x b =>
      do tb <- transl_expr b;
      OK(Sset x tb)
  | Clight.Svolread x b =>
      do tb <- transl_lvalue b;
      make_vol_load x tb (typeof b)
  | Clight.Scall x b cl =>
      match classify_fun (typeof b) with
      | fun_case_f args res =>
          do tb <- transl_expr b;
          do tcl <- transl_exprlist cl args;
          OK(Scall x (signature_of_type args res) tb tcl)
      | _ => Error(msg "Cshmgen.transl_stmt(call)")
      end
  | Clight.Ssequence s1 s2 =>
      do ts1 <- transl_statement tyret nbrk ncnt s1;
      do ts2 <- transl_statement tyret nbrk ncnt s2;
      OK (Sseq ts1 ts2)
  | Clight.Sifthenelse e s1 s2 =>
      do te <- transl_expr e;
      do ts1 <- transl_statement tyret nbrk ncnt s1;
      do ts2 <- transl_statement tyret nbrk ncnt s2;
      OK (Sifthenelse (make_boolean te (typeof e)) ts1 ts2)
  | Clight.Swhile e s1 =>
      do te <- exit_if_false e;
      do ts1 <- transl_statement tyret 1%nat 0%nat s1;
      OK (Sblock (Sloop (Sseq te (Sblock ts1))))
  | Clight.Sdowhile e s1 =>
      do te <- exit_if_false e;
      do ts1 <- transl_statement tyret 1%nat 0%nat s1;
      OK (Sblock (Sloop (Sseq (Sblock ts1) te)))
  | Clight.Sfor' e2 e3 s1 =>
      do te2 <- exit_if_false e2;
      do te3 <- transl_statement tyret 0%nat (S ncnt) e3;
      do ts1 <- transl_statement tyret 1%nat 0%nat s1;
      OK (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))
  | Clight.Sbreak =>
      OK (Sexit nbrk)
  | Clight.Scontinue =>
      OK (Sexit ncnt)
  | Clight.Sreturn (Some e) =>
      do te <- transl_expr e;
      OK (Sreturn (Some (make_cast (typeof e) tyret te)))
  | Clight.Sreturn None =>
      OK (Sreturn None)
  | Clight.Sswitch a sl =>
      do ta <- transl_expr a;
      do tsl <- transl_lbl_stmt tyret 0%nat (S ncnt) sl;
      OK (Sblock (Sswitch ta tsl))
  | Clight.Slabel lbl s =>
      do ts <- transl_statement tyret nbrk ncnt s;
      OK (Slabel lbl ts)
  | Clight.Sgoto lbl =>
      OK (Sgoto lbl)
  end

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


Definition prefix_var_name (id: ident) : errmsg :=
  MSG "In local variable " :: CTX id :: MSG ": " :: nil.

Definition transl_vars (l: list (ident * type)) :=
   AST.map_partial prefix_var_name var_kind_of_type l.

Definition transl_function (f: Clight.function) : res function :=
  do tparams <- transl_vars (Clight.fn_params f);
  do tvars <- transl_vars (Clight.fn_vars f);
  do tbody <- transl_statement f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f);
  OK (mkfunction
       (opttyp_of_type (Clight.fn_return f))
       tparams
       tvars
       (List.map (@fst ident type) f.(Clight.fn_temps))
       tbody).

Definition list_typ_eq:
  forall (l1 l2: list typ), {l1=l2} + {l1<>l2}.

Definition transl_fundef (f: Clight.fundef) : res fundef :=
  match f with
  | Clight.Internal g =>
      do tg <- transl_function g; OK(AST.Internal tg)
  | Clight.External ef args res =>
      if list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist args)
      && opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type res)
      then OK(AST.External ef)
      else Error(msg "Cshmgen.transl_fundef: wrong external signature")
  end.

Translation of programs

Definition transl_globvar (ty: type) := var_kind_of_type ty.

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