source: Deliverables/D2.2/8051/src/RTLabs/constPropagation.ml @ 1580

open RTLabs

let error_prefix = "RTLabs to RTL"
let error = Error.global_error error_prefix

let error_int () = error "int16 and int32 not supported."
let error_float () = error "float not supported."
let error_shift () = error "Shift operations not supported."


(* The analysis uses the lattice of maps from registers to values with a top *)
(* element which indicates the register is known not to be constant. *)
(* The lattice's join operation is pointwise join, where pointwise bottom is *)
(* represented by the absence of a binding in the map. *)

module Mem = Driver.RTLabsMemory

module L  = struct

  (* bottom will be when the map is undefined, so we do not need it explicitly*)
  type t =
    | T
    | V of Mem.Value.t
    | S (* stack: could add offset *)
    | A of AST.ident (* address symbol *)

  type property =
      t Register.FlexMap.t

  let bottom : property =
    Register.FlexMap.empty

  let join_t x y = match x, y with
    | V v1, V v2 when Mem.Value.equal v1 v2 -> V v1
    | S, S -> S
    | A i, A j when i = j -> A i
    | _ -> T

  let join : property -> property -> property =
    let choose i b1 b2 = match b1, b2 with
      | Some v, Some v' -> Some (join_t v v')
      | Some v, None | None, Some v -> Some v
      | _ -> None in
    Register.FlexMap.merge choose

  let bind = Register.FlexMap.add

  let find = Register.FlexMap.find

  let rem = Register.FlexMap.remove

  let mem = Register.FlexMap.mem

  let is_cst i p =
    try
      match find i p with
        | T -> false
        | _ -> true
    with
      | Not_found -> false

  let find_cst i p =
    match find i p with
      | T -> raise Not_found
      | v -> v

  let is_top i p =
    try
      match find i p with
        | T -> true
        | _ -> false
    with
      | Not_found -> false

  let is_zero i p =
    try
      match find i p with
        | V v -> Mem.Value.is_false v
        | _ -> false
    with
      | Not_found -> false

  let equal : property -> property -> bool =
    Register.FlexMap.equal (fun x y -> match x, y with
      | T, T | S, S -> true
      | V v1, V v2 -> Mem.Value.equal v1 v2
      | A i, A j -> i = j
      | _ -> false)

  let is_maximal _ = false

  let print = function
    | T -> "T"
    | V v -> Mem.Value.to_string v
    | S -> "STACK"
    | A i -> "*" ^ i

end

module F = Fix.Make (Label.ImpMap) (L)

module Eval = CminorInterpret.Eval_op (Mem)
(* evaluation happens in RTLabs memory model ... *)

module MemTarget = Memory.Make (Driver.TargetArch)
(* ... but for sizeof and offsets, which rely on the target memory model *)

open AST

let ext_fun_of_sign = function
  | Signed -> Mem.Value.sign_ext
  | Unsigned -> Mem.Value.zero_ext

let cast_to_std t v = match t with
  | Sig_int (size, sign) -> (ext_fun_of_sign sign) v size Mem.int_size
  | Sig_float _ -> error_float ()
  | Sig_offset | Sig_ptr -> v

let cst t = function
  | Cst_int i -> L.V (cast_to_std t (Mem.Value.of_int i))
  | Cst_offset off -> L.V (Mem.Value.of_int (MemTarget.concrete_offset off))
  | Cst_sizeof t' ->
    L.V (cast_to_std t (Mem.Value.of_int (MemTarget.concrete_size t')))
  | Cst_stack -> L.S
  | Cst_addrsymbol i -> L.A i
  | _ -> assert false (* won't call in these cases *)

let arg_type type_of = function
  | Reg r -> type_of r
  | Imm (_, t) -> t

let find_arg a prop = match a with
  | Reg r -> L.find r prop
  | Imm (k, t) -> cst t k

let do_the_op1
    (op : op1)
    (type_of : Register.t -> sig_type)
    (prop : F.property)
    (i : Register.t)
    (j : Register.t)
    : L.t =
  let x = L.find j prop in
  match op, x with
  | _, L.V v -> L.V (Eval.op1 (type_of i) (type_of j) op v)
  | Op_id, _ -> x
  | _ -> L.T

let do_the_op2
    (op : op2)
    (type_of : Register.t -> sig_type)
    (prop : F.property)
    (i : Register.t)
    (a : argument)
    (b : argument)
    : L.t =
  let x = find_arg a prop in
  let y = find_arg b prop in
  match x, y, op with
  (* consider a constant division by 0 as not constant *)
  | L.V _, L.V v2, (Op_div | Op_divu | Op_mod | Op_modu)
    when Mem.Value.is_false v2 -> L.T
  | L.V v1, L.V v2, _ ->
    L.V (Eval.op2
           (type_of i)
           (arg_type type_of a)
           (arg_type type_of b) op v1 v2)
  (* ops with stack and address symbols are not considered constant, unless *)
  (* clearly so *)
  | x, L.V v, (Op_addp | Op_subp) when Mem.Value.is_false v -> x
  | _ -> L.T

let is_zero_arg a prop = match a with
  | Reg r -> L.is_zero r prop
  | Imm (Cst_int i, _) -> i = 0
  | _ -> false

(* this is used to mark some results of a bin op as constant even if its *)
(* operands are not both constant *)
let mark_const_op op i a b prop =
  match is_zero_arg a prop, is_zero_arg b prop, op with
    | true, _, (Op_mul | Op_div | Op_divu | Op_mod | Op_modu | Op_and |
        Op_shl | Op_shr | Op_shru | Op_cmpu Cmp_gt)
    | _, true, (Op_mul | Op_and | Op_cmpu Cmp_lt) ->
      L.bind i (L.V Mem.Value.zero) prop
    | true, _, Op_cmpu Cmp_le
    | _, true, Op_cmpu Cmp_ge -> L.bind i (L.V (Mem.Value.of_bool true)) prop
    | _, _, (Op_cmp Cmp_eq | Op_cmpu Cmp_eq | Op_cmpp Cmp_eq) ->
      (match a, b with
        | Reg j, Reg k when Register.equal j k ->
          L.bind i (L.V (Mem.Value.of_bool true)) prop
        | _ -> L.rem i prop)
    | _, _, (Op_cmp Cmp_ne | Op_cmp Cmp_gt | Op_cmp Cmp_lt |
             Op_cmpu Cmp_ne | Op_cmpu Cmp_gt | Op_cmpu Cmp_lt |
             Op_cmpp Cmp_ne | Op_cmpp Cmp_gt | Op_cmpp Cmp_lt |
             Op_xor) ->
      (match a, b with
        | Reg j, Reg k when Register.equal j k ->
          L.bind i (L.V (Mem.Value.of_bool false)) prop
        | _ -> L.rem i prop)
    | _ -> L.rem i prop

let is_cst_arg prop = function
  | Reg r -> L.mem r prop
  | Imm _ -> true

let semantics
    (types : sig_type Register.Map.t)
    (graph : statement Label.Map.t)
    (pred_table : Label.t list Label.Map.t)
    (lbl : Label.t)
    (valu : F.valuation)
    : F.property =
  let pred_prop = (* the situation at the entry of the statement (in [valu]) *)
    let f prop pred =
      L.join (valu pred) prop in
    List.fold_left f L.bottom (Label.Map.find lbl pred_table) in
  let type_of r = Register.Map.find r types in
  match Label.Map.find lbl graph with
    | St_cst (_, Cst_float _, _) -> error_float ()
    | St_cst (i, k, _) -> L.bind i (cst (type_of i) k) pred_prop
    | St_op1 (op, i, j, _) ->
      (try
         L.bind i (do_the_op1 op type_of pred_prop i j) pred_prop
       with
         | Not_found -> L.rem i pred_prop)
    | St_op2 (op, i, a, b, _)
      when is_cst_arg pred_prop a && is_cst_arg pred_prop b ->
      L.bind i (do_the_op2 op type_of pred_prop i a b) pred_prop
    | St_op2 (op, i, a, b, _) ->
      mark_const_op op i a b pred_prop
    | St_load (_, _, i, _)
    | St_call_id (_, _, Some i, _, _)
    | St_call_ptr (_, _, Some i, _, _) -> L.rem i pred_prop
    | _ -> pred_prop

let analyze
    (f_def : internal_function)
    : F.valuation =
  (* extract types of registers from the definition *)
  let types = RTLabsGraph.compute_type_map f_def in

  let graph = f_def.f_graph in
  let pred_table =
    let module U = GraphUtilities.Util(RTLabsGraph) in
    U.compute_predecessor_lists graph in

  F.lfp (semantics types graph pred_table)

(* now that the info for constants can be gathered, let's put that to use *)

(* this will be used to turn values back into constants. Notice: *)
(* 1) we are turning abstract offsets and sizes into integers *)
(* 2) this shares the problem with AST constants of representability *)
(*    with ocaml 31 bits integers *)
let cst_of_value = function
  | L.V v -> Cst_int (Mem.Value.to_int v)
  | L.S -> Cst_stack
  | L.A a -> Cst_addrsymbol a
  | _ -> invalid_arg "cst_of_value"

let arg_from_reg prop types r =
  try
    Imm (cst_of_value (L.find_cst r prop), Register.Map.find r types)
  with
    | Not_found -> Reg r

let arg_from_arg prop types = function
  | Reg i -> arg_from_reg prop types i
  | _ as a -> a

let args_from_args prop types =
  List.map (arg_from_arg prop types)

let copy i a l = match a with
  | Reg j -> St_op1 (Op_id, i, j, l)
  | _ -> assert false (* should already have been substituted *)

let negate i a l = match a with
  | Reg j -> St_op1 (Op_negint, i, j, l)
  | _ -> assert false (* should already have been substituted *)

let simpl_imm_op2 op i j k types prop l =
  let f = function
    | Imm _ -> None
    | Reg r ->
      try
        Some (L.find_cst r prop)
      with
        | Not_found -> None in
  let one = Mem.Value.of_int 1 in
  match f j, f k, op with
    | Some (L.V v), _, (Op_add | Op_addp | Op_or | Op_xor )
      when Mem.Value.is_false v ->
      copy i k l
    | Some (L.V v), _, Op_mul when Mem.Value.equal v one ->
      copy i j l
    | _, Some (L.V v), (Op_add | Op_sub | Op_addp | Op_subp | Op_or | Op_xor)
      when Mem.Value.is_false v ->
      copy i j l
    | _, Some (L.V v), (Op_mul | Op_div)  when Mem.Value.equal v one ->
      copy i j l
    | Some (L.V v), _, Op_sub when Mem.Value.is_false v ->
      negate i j l
    | _ ->
      St_op2(op, i, arg_from_arg prop types j, arg_from_arg prop types k, l)

(* we transform statements according to the valuation found out by analyze *)
(* We also turn branchings into redirections if the guard is constant. *)
let transform
    (valu : F.valuation)
    (types: sig_type Register.Map.t)
    (p    : Label.t)
    (stmt : statement) : statement list * Label.t list option =
  match stmt with
    | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) ->
      (* we are sure valu has a binding for i, we change the abstract
         quantities into actual integers *)
      ([St_cst (i, cst_of_value (L.find_cst i (valu p)), next)] , None)
    | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) ->
      ([St_cst (i, cst_of_value (L.find_cst i (valu p)), next)], None)
    | St_op2 (op, i, a, b, l) ->
      ([simpl_imm_op2 op i a b types (valu p) l], None)
    | St_load (q, a, j, l) ->
      ([St_load(q, arg_from_arg (valu p) types a, j, l)], None)
    | St_store (q, a, b, l) ->
      ([St_store (q, arg_from_arg (valu p) types a,
                arg_from_arg (valu p) types b, l)], None)
    | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) ->
      (match L.find_cst i (valu p) with
        | L.V v when Mem.Value.is_false v -> ([], Some [if_false])
        | L.V _ | L.A _ -> ([], Some [if_true])
        | _ -> ([s], Some [if_true ; if_false]))
    | St_return (Some a) ->
      ([St_return (Some (arg_from_arg (valu p) types a))], None)
    | St_call_id (f, args, ret, sg, l) ->
      ([St_call_id (f, args_from_args (valu p) types args, ret, sg, l)], None)
    | St_call_ptr (f, args, ret, sg, l) ->
      ([St_call_ptr (f, args_from_args (valu p) types args, ret, sg, l)], None)
    | St_tailcall_id (f, args, sg) ->
      ([St_tailcall_id (f, args_from_args (valu p) types args, sg)], None)
    | St_tailcall_ptr (f, args, sg) ->
      ([St_tailcall_ptr (f, args_from_args (valu p) types args, sg)], None)
    | stmt -> ([stmt], None)

let transform_int_function
    (f_def  : internal_function)
    : internal_function =
  let valu = analyze f_def in
        (* we transform the graph according to the analysis *)
  let types = RTLabsGraph.compute_type_map f_def in
  let module U = GraphUtilities.Util(RTLabsGraph) in
  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in
  let trans =  transform valu types in
  let fresh () = Label.Gen.fresh f_def.f_luniverse in
  let graph = T.translate_pure_with_redirects fresh trans f_def.f_graph in
  let graph = U.dead_code_elim graph f_def.f_entry in
  {f_def with f_graph = graph}

let transform_function = function
  | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
  | f -> f

let trans = Languages.RTLabs, function
  | Languages.AstRTLabs p ->
    Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
  | _ -> assert false