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

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 do_the_op1 type_of i j op x = 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 type_of i j k op x y = 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) (type_of j) (type_of k) 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

(* 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 j k prop =
        match L.is_zero j prop, L.is_zero k 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)
                  when Register.equal j k -> L.bind i (L.V (Mem.Value.of_bool true)) 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)
      when Register.equal j k -> L.bind i (L.V (Mem.Value.of_bool false)) prop 
                | _ -> L.rem i prop

let semantics
    (types : sig_type Register.Map.t)
    (graph : statement Label.Map.t)
                (pred_table : Label.Set.t 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 pred prop =
                        L.join (valu pred) prop in
                Label.Set.fold f (Label.Map.find lbl pred_table) L.bottom 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 type_of i j op (L.find j pred_prop)) pred_prop
                        with
                                | Not_found -> L.rem i pred_prop)

    | St_op2 (op,i,Reg j,Reg k,_) when L.mem j pred_prop && L.mem k pred_prop ->
                        let j_val = L.find j pred_prop in
                        let k_val = L.find k pred_prop in
      L.bind i (do_the_op2 type_of i j k op j_val k_val) pred_prop
                | St_op2 (op, i, Reg j, Reg k, _) ->
                        mark_const_op op i j k 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 = RTLabsUtilities.computes_type_map f_def in
                
        let graph = f_def.f_graph in
        
        let pred_table = RTLabsUtilities.compute_predecessors 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) if we have mapped a register to a value, it must be an integer *)
(* 2) we are turning abstract offsets and sizes into integers *)
(* 3) 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 i -> Cst_addrsymbol i
        | _ -> invalid_arg "cst_of_value"

let simpl_imm_op2 op i j k types prop l =
        let f r =
                try
                        Some (L.find_cst r prop)
                with
                        | Not_found -> None in
        let one = Mem.Value.of_int 1 in
        let type_of r = Register.Map.find r types in
        match f j, f k, op with
  | Some (L.V v), _, (Op_add | Op_or | Op_xor ) when Mem.Value.is_false v ->
    St_op1(Op_id, i, k, l)
  | Some (L.V v), _, Op_mul when Mem.Value.equal v one ->
    St_op1(Op_id, i, k, l)
  | _, Some (L.V v), (Op_add | Op_sub | Op_addp | Op_subp | Op_or | Op_xor)
          when Mem.Value.is_false v ->
    St_op1(Op_id, i, j, l)
  | _, Some (L.V v), Op_mul when Mem.Value.equal v one ->
    St_op1(Op_id, i, j, l)
  | Some (L.V v), _, Op_sub when Mem.Value.is_false v ->
                St_op1(Op_negint, i, k, l)
  | Some v, Some u, _ ->
                let a1 = Imm (cst_of_value v, type_of j) in
                let a2 = Imm (cst_of_value u, type_of k) in
                St_op2(op, i, a1, a2, l)
  | Some v, _, _ -> St_op2(op, i, Imm (cst_of_value v, type_of j), Reg k, l)
  | _, Some v, _ -> St_op2(op, i, Reg j, Imm (cst_of_value v, type_of k), l)
        | _ -> St_op2(op, i, Reg j, Reg k, l)

let simpl_imm_load q i j types prop l =
        try
                let v = L.find_cst i prop in
                St_load(q, Imm (cst_of_value v, Register.Map.find i types), j, l)
        with
                | Not_found -> St_load (q, Reg i, j, l)

let simpl_imm_store q i j types prop l =
        let f r =
                try
                    Some (L.find_cst r prop)
                with
                    | Not_found -> None in
        let type_of r = Register.Map.find r types in
        match f i, f j with
                | Some v, Some u ->
            let a1 = Imm (cst_of_value v, type_of i) in
            let a2 = Imm (cst_of_value u, type_of j) in
            St_store(q, a1, a2, l)
                | Some v, _ ->
                        St_store(q, Imm (cst_of_value v, type_of i), Reg j, l)
    | _, Some u ->
      St_store(q, Reg i, Imm (cst_of_value u, type_of j), l)
                | _ -> St_store(q, Reg i, Reg j, 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_statement
    (valu : F.valuation)
                (types: sig_type Register.Map.t)
    (p    : Label.t)
                : statement -> statement = function
  | 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) 
        | (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)
        | St_op2 (op, i, Reg j, Reg k, l) ->
                simpl_imm_op2 op i j k types (valu p) l
  | St_load (q, Reg i, j, l) ->
                simpl_imm_load q i j types (valu p) l
        | St_store (q, Reg i, Reg j, l) ->
                simpl_imm_store q i j types (valu p) l
  | St_op2 _ | St_load _ | St_store _ ->
          assert false (* there should not be any imm argument *)
        | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) ->
                let s = match L.find_cst i (valu p) with
                        | L.V v when Mem.Value.is_false v -> St_skip if_false
                        | L.V _ | L.A _ -> St_skip if_true
                        | _ -> s in s
        | stmt -> stmt

let dom (map : 'a Label.Map.t) : Label.Set.t =
        let add key _ = Label.Set.add key in
        Label.Map.fold add map Label.Set.empty

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 = RTLabsUtilities.computes_type_map f_def in 
        let graph = Label.Map.mapi (transform_statement valu types) f_def.f_graph in
        (* and we eliminate resulting dead code *)
        let graph = RTLabsUtilities.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