(* *********************************************************************)
(*                                                                     *)
(*              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 GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(* Pulling side-effects out of expressions *)

(* Assumes: nothing
   Produces: simplified code *)

open C
open Cutil
open Transform

(* Grammar of simplified expressions:
      e ::= EConst cst
          | ESizeof ty
          | EVar id
          | EUnop pure-unop e
          | EBinop pure-binop e e
          | EConditional e e e
          | ECast ty e

   Grammar of statements produced to reflect side-effects in expressions:
      s ::= Sskip
          | Sdo (EBinop Oassign e e)
          | Sdo (EBinop Oassign e (ECall e e* ))
          | Sdo (Ecall e el)
          | Sseq s s
          | Sif e s s
*)

let rec is_simpl_expr e =
  match e.edesc with
  | EConst cst -> true
  | ESizeof ty -> true
  | EVar id -> true
  | EUnop((Ominus|Oplus|Olognot|Onot|Oderef|Oaddrof), e1) ->
      is_simpl_expr e1
  | EBinop((Oadd|Osub|Omul|Odiv|Omod|Oand|Oor|Oxor|Oshl|Oshr|
            Oeq|One|Olt|Ogt|Ole|Oge|Oindex|Ologand|Ologor), e1, e2, _) ->
      is_simpl_expr e1 && is_simpl_expr e2
  | EConditional(e1, e2, e3) ->
      is_simpl_expr e1 && is_simpl_expr e2 && is_simpl_expr e3
  | ECast(ty, e1) ->
      is_simpl_expr e1
  | _ ->
      false

(* "Destination" of a simplified expression *)

type exp_destination =
  | RHS                  (* evaluate as a r-value *)
  | LHS                  (* evaluate as a l-value *)
  | Drop                 (* drop its value, we only need the side-effects *)
  | Set of exp           (* assign it to the given simplified l.h.s. *)

let voidconst = { nullconst with etyp = TVoid [] }

(* Reads from volatile lvalues are also considered as side-effects if
   [volatilize] is true. *)

let volatilize = ref false

(* [simpl_expr loc env e act] returns a pair [s, e'] of
   a statement that performs the side-effects present in [e] and
   a simplified, side-effect-free expression [e'].
   If [act] is [RHS], [e'] evaluates to the same value as [e].
   If [act] is [LHS], [e'] evaluates to the same location as [e].
   If [act] is [Drop], [e'] is not meaningful and must be ignored.
   If [act] is [Set lhs], [s] also performs an assignment
   equivalent to [lhs = e].  [e'] is not meaningful. *)

let simpl_expr loc env e act =

  (* Temporaries should not be [const] because we assign into them,
     and need not be [volatile] because no one else is writing into them.
     As for [restrict] it doesn't make sense anyway. *)

  let new_temp ty =
    Transform.new_temp (erase_attributes_type env ty) in

  let eboolvalof e =
    { edesc = EBinop(One, e, intconst 0L IInt, TInt(IInt, []));
      etyp = TInt(IInt, []) } in

  let sseq s1 s2 = Cutil.sseq loc s1 s2 in

  let sassign e1 e2 =
    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp}; 
      sloc = loc } in

  let sif e s1 s2 =
    { sdesc = Sif(e, s1, s2); sloc = loc } in

  let is_volatile_read e =
    !volatilize
    && List.mem AVolatile (attributes_of_type env e.etyp)
    && is_lvalue env e in

  let lhs_to_rhs e =
    if is_volatile_read e
    then (let t = new_temp e.etyp in (sassign t e, t))
    else (sskip, e) in

  let finish act s e =
    match act with
    | RHS ->
        if is_volatile_read e
        then (let t = new_temp e.etyp in (sseq s (sassign t e), t))
        else (s, e)
    | LHS ->
        (s, e)
    | Drop -> 
        if is_volatile_read e
        then (let t = new_temp e.etyp in (sseq s (sassign t e), voidconst))
        else (s, voidconst)
    | Set lhs ->
        if is_volatile_read e
        then (let t = new_temp e.etyp in
                 (sseq s (sseq (sassign t e) (sassign lhs t)), voidconst))
        else (sseq s (sassign lhs e), voidconst) in

   let rec simpl e act =
    match e.edesc with

    | EConst cst -> 
        finish act sskip e

    | ESizeof ty -> 
        finish act sskip e

    | EVar id ->
        finish act sskip e

    | EUnop(op, e1) ->

        begin match op with

        | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ ->
            let (s1, e1') = simpl e1 RHS in
            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}

        | Oaddrof ->
            let (s1, e1') = simpl e1 LHS in
            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}

        | Odot _ ->
            let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in
            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}

        | Opreincr | Opredecr ->
            let (s1, e1') = simpl e1 LHS in
            let (s2, e2') = lhs_to_rhs e1' in
            let op' = match op with Opreincr -> Oadd | _ -> Osub in
            let ty = unary_conversion env e.etyp in
            let e3 =
              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
            begin match act with
            | Drop ->
                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
            | _ ->
                let tmp = new_temp e.etyp in
                finish act (sseq s1 (sseq s2 (sseq (sassign tmp e3)
                                                   (sassign e1' tmp))))
                       tmp
            end

        | Opostincr | Opostdecr ->
            let (s1, e1') = simpl e1 LHS in
            let op' = match op with Opostincr -> Oadd | _ -> Osub in
            let ty = unary_conversion env e.etyp in
            begin match act with
            | Drop ->
                let (s2, e2') = lhs_to_rhs e1' in
                let e3 =
                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
            | _ ->
                let tmp = new_temp e.etyp in
                let e3 =
                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in
                finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3))) 
                       tmp
            end

        end

    | EBinop(op, e1, e2, ty) ->

        begin match op with

        | Oadd | Osub | Omul | Odiv | Omod | Oand | Oor | Oxor
        | Oshl | Oshr | Oeq | One | Olt | Ogt | Ole | Oge | Oindex ->
            let (s1, e1') = simpl e1 RHS in
            let (s2, e2') = simpl e2 RHS in
            finish act (sseq s1 s2)
                       {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp}

        | Oassign ->
            if act = Drop && is_simpl_expr e1 then
              simpl e2 (Set e1)
            else begin
              match act with
              | Drop ->
                  let (s1, e1') = simpl e1 LHS in
                  let (s2, e2') = simpl e2 RHS in
                  (sseq s1 (sseq s2 (sassign e1' e2')), voidconst)
              | _ ->
                  let tmp = new_temp e.etyp in
                  let (s1, e1') = simpl e1 LHS in
                  let (s2, e2') = simpl e2 (Set tmp) in
                  finish act (sseq s1 (sseq s2 (sassign e1' tmp)))
                             tmp
            end

        | Oadd_assign | Osub_assign | Omul_assign | Odiv_assign
        | Omod_assign | Oand_assign | Oor_assign  | Oxor_assign
        | Oshl_assign | Oshr_assign ->
            let (s1, e1') = simpl e1 LHS in
            let (s11, e11') = lhs_to_rhs e1' in
            let (s2, e2') = simpl e2 RHS in
            let op' =
              match op with
              | Oadd_assign -> Oadd    | Osub_assign -> Osub
              | Omul_assign -> Omul    | Odiv_assign -> Odiv
              | Omod_assign -> Omod    | Oand_assign -> Oand
              | Oor_assign  -> Oor     | Oxor_assign -> Oxor
              | Oshl_assign -> Oshl    | Oshr_assign -> Oshr
              | _ -> assert false in
            let e3 =
              { edesc = EBinop(op', e11', e2', ty); etyp = ty } in
            begin match act with
            | Drop ->
                (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
            | _ ->
                let tmp = new_temp e.etyp in
                finish act (sseq s1 (sseq s11 (sseq s2
                               (sseq (sassign tmp e3) (sassign e1' tmp)))))
                           tmp
            end

        | Ocomma ->
            let (s1, _) = simpl e1 Drop in
            let (s2, e2') = simpl e2 act in
            (sseq s1 s2, e2')

        | Ologand ->
            let (s1, e1') = simpl e1 RHS in
            if is_simpl_expr e2 then begin
              finish act s1
                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp}
            end else begin
              match act with
              | Drop ->
                  let (s2, _) = simpl e2 Drop in
                  (sseq s1 (sif e1' s2 sskip), voidconst)
              | RHS | LHS ->  (* LHS should not happen *)
                  let (s2, e2') = simpl e2 RHS in
                  let tmp = new_temp e.etyp in
                  (sseq s1 (sif e1' 
                              (sseq s2 (sassign tmp (eboolvalof e2')))
                              (sassign tmp (intconst 0L IInt))),
                   tmp)
              | Set lv ->
                  let (s2, e2') = simpl e2 RHS in
                  (sseq s1 (sif e1' 
                              (sseq s2 (sassign lv (eboolvalof e2')))
                              (sassign lv (intconst 0L IInt))),
                   voidconst)
            end             

        | Ologor ->
            let (s1, e1') = simpl e1 RHS in
            if is_simpl_expr e2 then begin
              finish act s1
                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp}
            end else begin
              match act with
              | Drop ->
                  let (s2, _) = simpl e2 Drop in
                  (sseq s1 (sif e1' sskip s2), voidconst)
              | RHS | LHS ->  (* LHS should not happen *)
                  let (s2, e2') = simpl e2 RHS in
                  let tmp = new_temp e.etyp in
                  (sseq s1 (sif e1' 
                              (sassign tmp (intconst 1L IInt))
                              (sseq s2 (sassign tmp (eboolvalof e2')))),
                   tmp)
              | Set lv ->
                  let (s2, e2') = simpl e2 RHS in
                  (sseq s1 (sif e1' 
                              (sassign lv (intconst 1L IInt))
                              (sseq s2 (sassign lv (eboolvalof e2')))),
                   voidconst)
            end             

        end

    | EConditional(e1, e2, e3) ->
        let (s1, e1') = simpl e1 RHS in
        if is_simpl_expr e2 && is_simpl_expr e3 then begin
          finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp}
        end else begin
          match act with
          | Drop ->
              let (s2, _) = simpl e2 Drop in
              let (s3, _) = simpl e3 Drop in
              (sseq s1 (sif e1' s2 s3), voidconst)
          | RHS | LHS ->  (* LHS should not happen *)
              let tmp = new_temp e.etyp in
              let (s2, _) = simpl e2 (Set tmp) in
              let (s3, _) = simpl e3 (Set tmp) in
              (sseq s1 (sif e1' s2 s3), tmp)
          | Set lv ->
              let (s2, _) = simpl e2 (Set lv) in
              let (s3, _) = simpl e3 (Set lv) in
              (sseq s1 (sif e1' s2 s3), voidconst)
        end

    | ECast(ty, e1) ->
        if is_void_type env ty then begin
          if act <> Drop then
            Errors.warning "%acast to 'void' in a context expecting a value\n"
                           formatloc loc;
            simpl e1 act
        end else begin
          let (s1, e1') = simpl e1 RHS in
          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp}
        end

    | ECall(e1, el) ->
        let (s1, e1') = simpl e1 RHS in
        let (s2, el') = simpl_list el in
        let e2 = { edesc = ECall(e1', el'); etyp = e.etyp } in
        begin match act with
        | Drop ->
            (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst)
        | Set({edesc = EVar _} as lhs) ->
            (* CompCert wants the destination of a call to be a variable,
               not a more complex lhs.  In the latter case, we
               fall through the catch-all case below *)
            (sseq s1 (sseq s2 (sassign lhs e2)), voidconst)
        | _ ->
            let tmp = new_temp e.etyp in
            finish act (sseq s1 (sseq s2 (sassign tmp e2))) tmp
        end

  and simpl_list = function
    | [] -> (sskip, [])
    | e1 :: el ->
        let (s1, e1') = simpl e1 RHS in
        let (s2, el') = simpl_list el in
        (sseq s1 s2, e1' :: el')

  in simpl e act

(* Simplification of an initializer *)

let simpl_initializer loc env i =

  let rec simpl_init = function
  | Init_single e ->
      let (s, e') = simpl_expr loc env e RHS in
      (s, Init_single e)
  | Init_array il ->
      let rec simpl = function
      | [] -> (sskip, [])
      | i1 :: il ->
          let (s1, i1') = simpl_init i1 in
          let (s2, il') = simpl il in
          (sseq loc s1 s2, i1' :: il') in
      let (s, il') = simpl il in
      (s, Init_array il')
  | Init_struct(id, il) ->
      let rec simpl = function
      | [] -> (sskip, [])
      | (f1, i1) :: il ->
          let (s1, i1') = simpl_init i1 in
          let (s2, il') = simpl il in
          (sseq loc s1 s2, (f1, i1') :: il') in
      let (s, il') = simpl il in
      (s, Init_struct(id, il'))
  | Init_union(id, f, i) ->
      let (s, i') = simpl_init i in
      (s, Init_union(id, f, i'))

  in simpl_init i

(* Construct a simplified statement equivalent to [if (e) s1; else s2;].
   Optimizes the case where e contains [&&] or [||] or [?].
   [s1] or [s2] can be duplicated, so use only for small [s1] and [s2]
   that do not define any labels. *)

let rec simpl_if loc env e s1 s2 =
  match e.edesc with
  | EUnop(Olognot, e1) ->
      simpl_if loc env e1 s2 s1
  | EBinop(Ologand, e1, e2, _) ->
      simpl_if loc env e1
        (simpl_if loc env e2 s1 s2)
        s2
  | EBinop(Ologor, e1, e2, _) ->
      simpl_if loc env e1
        s1
        (simpl_if loc env e2 s1 s2)
  | EConditional(e1, e2, e3) ->
      simpl_if loc env e1
        (simpl_if loc env e2 s1 s2)
        (simpl_if loc env e3 s1 s2)
  | _ ->
      let (s, e') = simpl_expr loc env e RHS in
      sseq loc s {sdesc = Sif(e', s1, s2); sloc = loc}

(* Trivial statements for which [simpl_if] is applicable *)

let trivial_stmt s =
  match s.sdesc with
  | Sskip | Scontinue | Sbreak | Sgoto _ -> true
  | _ -> false

(* Construct a simplified statement equivalent to [if (!e) exit; ]. *)

let break_if_false loc env e =
  simpl_if loc env e
           {sdesc = Sskip; sloc = loc}
           {sdesc = Sbreak; sloc = loc}

(* Simplification of a statement *)

let simpl_statement env s =

  let rec simpl_stmt s =
    match s.sdesc with

  | Sskip ->
      s

  | Sdo e ->
      let (s', _) = simpl_expr s.sloc env e Drop in
      s'

  | Sseq(s1, s2) ->
      {sdesc = Sseq(simpl_stmt s1, simpl_stmt s2); sloc = s.sloc}

  | Sif(e, s1, s2) ->
      if trivial_stmt s1 && trivial_stmt s2 then
        simpl_if s.sloc env e (simpl_stmt s1) (simpl_stmt s2)
      else begin
        let (s', e') = simpl_expr s.sloc env e RHS in
        sseq s.sloc s'
          {sdesc = Sif(e', simpl_stmt s1, simpl_stmt s2);
           sloc = s.sloc}
      end

  | Swhile(e, s1) ->
      if is_simpl_expr e then
        {sdesc = Swhile(e, simpl_stmt s1); sloc = s.sloc}
      else
        {sdesc =
           Swhile(intconst 1L IInt,
                  sseq s.sloc (break_if_false s.sloc env e)
                              (simpl_stmt s1));
         sloc = s.sloc}

  | Sdowhile(s1, e) ->
      if is_simpl_expr e then
        {sdesc = Sdowhile(simpl_stmt s1, e); sloc = s.sloc}
      else begin
        let tmp = new_temp (TInt(IInt, [])) in
        let (s', _) = simpl_expr s.sloc env e (Set tmp) in
        let s_init =
          {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp);
                        etyp = tmp.etyp};
           sloc = s.sloc} in
        {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
      end
(*** Alternate translation that unfortunately puts a "break" in the
     "next" part of a "for", something that is not supported
     by Clight semantics, and has unknown behavior in gcc.
        {sdesc =
           Sfor(sskip, 
                intconst 1L IInt,
                break_if_false s.sloc env e,
                simpl_stmt s1);
         sloc = s.sloc}
***)

  | Sfor(s1, e, s2, s3) ->
      if is_simpl_expr e then
        {sdesc = Sfor(simpl_stmt s1,
                      e,
                      simpl_stmt s2,
                      simpl_stmt s3);
         sloc = s.sloc}
      else
        let (s', e') = simpl_expr s.sloc env e RHS in
        {sdesc = Sfor(sseq s.sloc (simpl_stmt s1) s',
                      e',
                      sseq s.sloc (simpl_stmt s2) s',
                      simpl_stmt s3);
         sloc = s.sloc}

  | Sbreak ->
      s
  | Scontinue ->
      s

  | Sswitch(e, s1) ->
      let (s', e') = simpl_expr s.sloc env e RHS in
      sseq s.sloc s' {sdesc = Sswitch(e', simpl_stmt s1); sloc = s.sloc}

  | Slabeled(lbl, s1) ->
      {sdesc = Slabeled(lbl, simpl_stmt s1); sloc = s.sloc}

  | Sgoto lbl ->
      s

  | Sreturn None ->
      s

  | Sreturn (Some e) ->
      let (s', e') = simpl_expr s.sloc env e RHS in
      sseq s.sloc s' {sdesc = Sreturn(Some e'); sloc = s.sloc}

  | Sblock sl ->
      {sdesc = Sblock(simpl_block sl); sloc = s.sloc}

  | Sdecl d -> assert false

  and simpl_block = function
  | [] -> []
  | ({sdesc = Sdecl(sto, id, ty, None)} as s) :: sl ->
      s :: simpl_block sl
  | ({sdesc = Sdecl(sto, id, ty, Some i)} as s) :: sl ->
      let (s', i') = simpl_initializer s.sloc env i in
      let sl' =
           {sdesc = Sdecl(sto, id, ty, Some i'); sloc = s.sloc}
        :: simpl_block sl in
      if s'.sdesc = Sskip then sl' else s' :: sl'
  | s :: sl ->
      simpl_stmt s :: simpl_block sl

  in simpl_stmt s

(* Simplification of a function definition *)

let simpl_fundef env f =
  reset_temps();
  let body' = simpl_statement env f.fd_body in
  let temps = get_temps() in
  { f with fd_locals = f.fd_locals @ temps; fd_body = body' }

(* Entry point *)

let program ?(volatile = false) p =
  volatilize := volatile;
  Transform.program ~fundef:simpl_fundef p