(** Translation from Csharpminor to Cminor. *)

Require Import Coqlib.
Require Import Maps.
Require Import Sets. 
Require Import AST.
Require Import Integers.
Require Mem.
Require Import Csharpminor.
Require Import Op.
Require Import Cminor.
Require Cmconstr.

(** The main task in translating Csharpminor to Cminor is to explicitly
  stack-allocate local variables whose address is taken: these local
  variables become sub-blocks of the Cminor stack data block for the
  current function.  Taking the address of such a variable becomes
  a [Oaddrstack] operation with the corresponding offset.  Accessing
  or assigning such a variable becomes a load or store operation at
  that address.  Only scalar local variables whose address is never
  taken in the Csharpminor code can be mapped to Cminor local
  variable, since the latter do not reside in memory.  

  Other tasks performed during the translation to Cminor:
- Transformation of Csharpminor's standard set of operators and
  trivial addressing modes to Cminor's processor-dependent operators
  and addressing modes.  This is done using the optimizing Cminor
  constructor functions provided in file [Cmconstr], therefore performing
  instruction selection on the fly.
- 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 Csharpminor.
*)

(** Translation of operators. *)

Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr :=
  match el with
  | Enil =>
      match op with
      | Csharpminor.Ointconst n => Some(Eop (Ointconst n) Enil)
      | Csharpminor.Ofloatconst n => Some(Eop (Ofloatconst n) Enil)
      | _ => None
      end
  | Econs e1 Enil =>
      match op with
      | Csharpminor.Ocast8unsigned => Some(Cmconstr.cast8unsigned e1)
      | Csharpminor.Ocast8signed => Some(Cmconstr.cast8signed e1)
      | Csharpminor.Ocast16unsigned => Some(Cmconstr.cast16unsigned e1)
      | Csharpminor.Ocast16signed => Some(Cmconstr.cast16signed e1)
      | Csharpminor.Onotint => Some(Cmconstr.notint e1)
      | Csharpminor.Onegf => Some(Cmconstr.negfloat e1)
      | Csharpminor.Oabsf => Some(Cmconstr.absfloat e1)
      | Csharpminor.Osingleoffloat => Some(Cmconstr.singleoffloat e1)
      | Csharpminor.Ointoffloat => Some(Cmconstr.intoffloat e1)
      | Csharpminor.Ofloatofint => Some(Cmconstr.floatofint e1)
      | Csharpminor.Ofloatofintu => Some(Cmconstr.floatofintu e1)
      | _ => None
      end
  | Econs e1 (Econs e2 Enil) =>
      match op with
      | Csharpminor.Oadd => Some(Cmconstr.add e1 e2)
      | Csharpminor.Osub => Some(Cmconstr.sub e1 e2)
      | Csharpminor.Omul => Some(Cmconstr.mul e1 e2)
      | Csharpminor.Odiv => Some(Cmconstr.divs e1 e2)
      | Csharpminor.Odivu => Some(Cmconstr.divu e1 e2)
      | Csharpminor.Omod => Some(Cmconstr.mods e1 e2)
      | Csharpminor.Omodu => Some(Cmconstr.modu e1 e2)
      | Csharpminor.Oand => Some(Cmconstr.and e1 e2)
      | Csharpminor.Oor => Some(Cmconstr.or e1 e2)
      | Csharpminor.Oxor => Some(Cmconstr.xor e1 e2)
      | Csharpminor.Oshl => Some(Cmconstr.shl e1 e2)
      | Csharpminor.Oshr => Some(Cmconstr.shr e1 e2)
      | Csharpminor.Oshru => Some(Cmconstr.shru e1 e2)
      | Csharpminor.Oaddf => Some(Cmconstr.addf e1 e2)
      | Csharpminor.Osubf => Some(Cmconstr.subf e1 e2)
      | Csharpminor.Omulf => Some(Cmconstr.mulf e1 e2)
      | Csharpminor.Odivf => Some(Cmconstr.divf e1 e2)
      | Csharpminor.Ocmp c => Some(Cmconstr.cmp c e1 e2)
      | Csharpminor.Ocmpu c => Some(Cmconstr.cmpu c e1 e2)
      | Csharpminor.Ocmpf c => Some(Cmconstr.cmpf c e1 e2)
      | _ => None
      end
  | _ => None
  end.

(** [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 => Cmconstr.cast8signed e
  | Mint8unsigned => Cmconstr.cast8unsigned e
  | Mint16signed => Cmconstr.cast16signed e
  | Mint16unsigned => Cmconstr.cast16unsigned e
  | Mint32 => e
  | Mfloat32 => Cmconstr.singleoffloat e
  | Mfloat64 => e
  end.

Definition make_load (chunk: memory_chunk) (e: expr): expr :=
  Cmconstr.load chunk e.

Definition store_arg (chunk: memory_chunk) (e: expr) : expr :=
  match e with
  | Eop op (Econs e1 Enil) =>
      match op with
      | Ocast8signed =>
          match chunk with Mint8signed => e1 | _ => e end
      | Ocast8unsigned =>
          match chunk with Mint8unsigned => e1 | _ => e end
      | Ocast16signed =>
          match chunk with Mint16signed => e1 | _ => e end
      | Ocast16unsigned =>
          match chunk with Mint16unsigned => e1 | _ => e end
      | Osingleoffloat =>
          match chunk with Mfloat32 => e1 | _ => e end
      | _ => e
      end
  | _ => e
  end.

Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt :=
  Sexpr(Cmconstr.store chunk e1 (store_arg chunk e2)).

Definition make_stackaddr (ofs: Z): expr :=
  Eop (Oaddrstack (Int.repr ofs)) Enil.

Definition make_globaladdr (id: ident): expr :=
  Eop (Oaddrsymbol id Int.zero) Enil.

(** Compile-time information attached to each Csharpminor
  variable: global variables, local variables, function parameters.
  [Var_local] denotes a scalar local variable whose address is not
  taken; it will be translated to a Cminor local variable of the
  same name.  [Var_stack_scalar] and [Var_stack_array] denote
  local variables that are stored as sub-blocks of the Cminor stack
  data block.  [Var_global_scalar] and [Var_global_array] denote
  global variables, stored in the global symbols with the same names. *)

Inductive var_info: Set :=
  | Var_local: memory_chunk -> var_info
  | Var_stack_scalar: memory_chunk -> Z -> var_info
  | Var_stack_array: Z -> var_info
  | Var_global_scalar: memory_chunk -> var_info
  | Var_global_array: var_info.

Definition compilenv := PMap.t var_info.

(** Generation of Cminor code corresponding to accesses to Csharpminor 
  local variables: reads, assignments, and taking the address of. *)

Definition var_get (cenv: compilenv) (id: ident): option expr :=
  match PMap.get id cenv with
  | Var_local chunk =>
      Some(Evar id)
  | Var_stack_scalar chunk ofs =>
      Some(make_load chunk (make_stackaddr ofs))
  | Var_global_scalar chunk =>
      Some(make_load chunk (make_globaladdr id))
  | _ =>
      None
  end.

Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): option stmt :=
  match PMap.get id cenv with
  | Var_local chunk =>
      Some(Sexpr(Eassign id (make_cast chunk rhs)))
  | Var_stack_scalar chunk ofs =>
      Some(make_store chunk (make_stackaddr ofs) rhs)
  | Var_global_scalar chunk =>
      Some(make_store chunk (make_globaladdr id) rhs)
  | _ =>
      None
  end.

Definition var_addr (cenv: compilenv) (id: ident): option expr :=
  match PMap.get id cenv with
  | Var_local chunk => None
  | Var_stack_scalar chunk ofs => Some (make_stackaddr ofs)
  | Var_stack_array ofs => Some (make_stackaddr ofs)
  | _ => Some (make_globaladdr id)
  end.

(** The translation from Csharpminor to Cminor can fail, which we
  encode by returning option types ([None] denotes error).
  Propagation of errors is done in monadic style, using the following
  [bind] monadic composition operator, and a [do] notation inspired
  by Haskell's. *)

Definition bind (A B: Set) (a: option A) (b: A -> option B): option B :=
  match a with
  | None => None
  | Some x => b x
  end.

Notation "'do' X <- A ; B" := (bind _ _ A (fun X => B))
  (at level 200, X ident, A at level 100, B at level 200).

(** Translation of expressions.  All the hard work is done by the
  [make_*] and [var_*] functions defined above. *)

Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr)
                     {struct e}: option expr :=
  match e with
  | Csharpminor.Evar id => var_get cenv id
  | Csharpminor.Eaddrof id => var_addr cenv id
  | Csharpminor.Eop op el =>
      do tel <- transl_exprlist cenv el; make_op op tel
  | Csharpminor.Eload chunk e =>
      do te <- transl_expr cenv e; Some (make_load chunk te)
  | Csharpminor.Ecall sig e el =>
      do te <- transl_expr cenv e;
      do tel <- transl_exprlist cenv el;
      Some (Ecall sig te tel)
  | Csharpminor.Econdition e1 e2 e3 =>
      do te1 <- transl_expr cenv e1;
      do te2 <- transl_expr cenv e2;
      do te3 <- transl_expr cenv e3;
      Some (Cmconstr.conditionalexpr te1 te2 te3)
  | Csharpminor.Elet e1 e2 =>
      do te1 <- transl_expr cenv e1;
      do te2 <- transl_expr cenv e2;
      Some (Elet te1 te2)
  | Csharpminor.Eletvar n =>
      Some (Eletvar n)
  | Csharpminor.Ealloc e =>
      do te <- transl_expr cenv e;
      Some (Ealloc te)
  end

with transl_exprlist (cenv: compilenv) (el: Csharpminor.exprlist)
                     {struct el}: option exprlist :=
  match el with
  | Csharpminor.Enil =>
      Some Enil
  | Csharpminor.Econs e1 e2 =>
      do te1 <- transl_expr cenv e1;
      do te2 <- transl_exprlist cenv e2;
      Some (Econs te1 te2)
  end.

(** Translation of statements.  Entirely straightforward. *)

Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt)
                     {struct s}: option stmt :=
  match s with
  | Csharpminor.Sskip =>
      Some Sskip
  | Csharpminor.Sexpr e =>
      do te <- transl_expr cenv e; Some(Sexpr te)
  | Csharpminor.Sassign id e =>
      do te <- transl_expr cenv e; var_set cenv id te
  | Csharpminor.Sstore chunk e1 e2 =>
      do te1 <- transl_expr cenv e1;
      do te2 <- transl_expr cenv e2;
      Some (make_store chunk te1 te2)
  | Csharpminor.Sseq s1 s2 =>
      do ts1 <- transl_stmt cenv s1;
      do ts2 <- transl_stmt cenv s2;
      Some (Sseq ts1 ts2)
  | Csharpminor.Sifthenelse e s1 s2 =>
      do te <- transl_expr cenv e;
      do ts1 <- transl_stmt cenv s1;
      do ts2 <- transl_stmt cenv s2;
      Some (Cmconstr.ifthenelse te ts1 ts2)
  | Csharpminor.Sloop s =>
      do ts <- transl_stmt cenv s;
      Some (Sloop ts)
  | Csharpminor.Sblock s =>
      do ts <- transl_stmt cenv s;
      Some (Sblock ts)
  | Csharpminor.Sexit n =>
      Some (Sexit n)
  | Csharpminor.Sswitch e cases default =>
      do te <- transl_expr cenv e; Some(Sswitch te cases default)
  | Csharpminor.Sreturn None =>
      Some (Sreturn None)
  | Csharpminor.Sreturn (Some e) =>
      do te <- transl_expr cenv e; Some (Sreturn (Some te))
  end.

(** Computation of the set of variables whose address is taken in
  a piece of Csharpminor code. *)

Module Identset := MakeSet(PTree).

Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t :=
  match e with
  | Csharpminor.Evar id => Identset.empty
  | Csharpminor.Eaddrof id => Identset.add id Identset.empty
  | Csharpminor.Eop op el => addr_taken_exprlist el
  | Csharpminor.Eload chunk e => addr_taken_expr e
  | Csharpminor.Ecall sig e el =>
      Identset.union (addr_taken_expr e) (addr_taken_exprlist el)
  | Csharpminor.Econdition e1 e2 e3 =>
      Identset.union (addr_taken_expr e1) 
        (Identset.union (addr_taken_expr e2) (addr_taken_expr e3))
  | Csharpminor.Elet e1 e2 =>
      Identset.union (addr_taken_expr e1) (addr_taken_expr e2)
  | Csharpminor.Eletvar n => Identset.empty
  | Csharpminor.Ealloc e => addr_taken_expr e
  end

with addr_taken_exprlist (e: Csharpminor.exprlist): Identset.t :=
  match e with
  | Csharpminor.Enil => Identset.empty
  | Csharpminor.Econs e1 e2 =>
      Identset.union (addr_taken_expr e1) (addr_taken_exprlist e2)
  end.

Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t :=
  match s with
  | Csharpminor.Sskip => Identset.empty
  | Csharpminor.Sexpr e => addr_taken_expr e
  | Csharpminor.Sassign id e => addr_taken_expr e
  | Csharpminor.Sstore chunk e1 e2 =>
      Identset.union (addr_taken_expr e1) (addr_taken_expr e2)
  | Csharpminor.Sseq s1 s2 =>
      Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2)
  | Csharpminor.Sifthenelse e s1 s2 =>
      Identset.union (addr_taken_expr e)
        (Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2))
  | Csharpminor.Sloop s => addr_taken_stmt s
  | Csharpminor.Sblock s => addr_taken_stmt s
  | Csharpminor.Sexit n => Identset.empty
  | Csharpminor.Sswitch e cases default => addr_taken_expr e
  | Csharpminor.Sreturn None => Identset.empty
  | Csharpminor.Sreturn (Some e) => addr_taken_expr e
  end.

(** Layout of the Cminor stack data block and construction of the 
  compilation environment.  Csharpminor local variables that are
  arrays or whose address is taken are allocated a slot in the Cminor
  stack data.  While this is not important for correctness, sufficient
  padding is inserted to ensure adequate alignment of addresses. *)

Definition assign_variable
    (atk: Identset.t)
    (id_lv: ident * var_kind)
    (cenv_stacksize: compilenv * Z) : compilenv * Z :=
  let (cenv, stacksize) := cenv_stacksize in
  match id_lv with
  | (id, Varray sz) =>
      let ofs := align stacksize 8 in
      (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz)
  | (id, Vscalar chunk) =>
      if Identset.mem id atk then
        let sz := Mem.size_chunk chunk in
        let ofs := align stacksize sz in
        (PMap.set id (Var_stack_scalar chunk ofs) cenv, ofs + sz)
      else
        (PMap.set id (Var_local chunk) cenv, stacksize)
  end.

Fixpoint assign_variables
    (atk: Identset.t)
    (id_lv_list: list (ident * var_kind))
    (cenv_stacksize: compilenv * Z)
    {struct id_lv_list}: compilenv * Z :=
  match id_lv_list with
  | nil => cenv_stacksize
  | id_lv :: rem =>
      assign_variables atk rem (assign_variable atk id_lv cenv_stacksize)
  end.

Definition build_compilenv
          (globenv: compilenv) (f: Csharpminor.function) : compilenv * Z :=
  assign_variables
    (addr_taken_stmt f.(Csharpminor.fn_body))
    (fn_variables f)
    (globenv, 0).

Definition assign_global_variable
     (ce: compilenv) (info: ident * var_kind * list init_data) : compilenv :=
  match info with
  | (id, Vscalar chunk, _) => PMap.set id (Var_global_scalar chunk) ce
  | (id, Varray _, _) => PMap.set id Var_global_array ce
  end.

Definition build_global_compilenv (p: Csharpminor.program) : compilenv :=
  List.fold_left assign_global_variable 
                 p.(prog_vars) (PMap.init Var_global_array).

(** Function parameters whose address is taken must be stored in their
  stack slots at function entry.  (Cminor passes these parameters in
  local variables.) *)

Fixpoint store_parameters
       (cenv: compilenv) (params: list (ident * memory_chunk))
       {struct params} : stmt :=
  match params with
  | nil => Sskip
  | (id, chunk) :: rem =>
      match PMap.get id cenv with
      | Var_local chunk =>
          Sseq (Sexpr (Eassign id (make_cast chunk (Evar id))))
               (store_parameters cenv rem)
      | Var_stack_scalar chunk ofs =>
          Sseq (make_store chunk (make_stackaddr ofs) (Evar id))
               (store_parameters cenv rem)
      | _ =>
          Sskip (* should never happen *)
      end
  end.

(** Translation of a Csharpminor function.  We must check that the
  required Cminor stack block is no bigger than [Int.max_signed],
  otherwise address computations within the stack block could
  overflow machine arithmetic and lead to incorrect code. *)

Definition transl_function
         (gce: compilenv) (f: Csharpminor.function): option function :=
  let (cenv, stacksize) := build_compilenv gce f in
  if zle stacksize Int.max_signed then
    do tbody <- transl_stmt cenv f.(Csharpminor.fn_body);
       Some (mkfunction
              (Csharpminor.fn_sig f)
              (Csharpminor.fn_params_names f)
              (Csharpminor.fn_vars_names f)
              stacksize
              (Sseq (store_parameters cenv f.(Csharpminor.fn_params)) tbody))
  else None.

Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): option fundef :=
  transf_partial_fundef (transl_function gce) f.

Definition transl_program (p: Csharpminor.program) : option program :=
  let gce := build_global_compilenv p in
  transform_partial_program (transl_fundef gce) (program_of_program p).