infer_clone/infer/src/bufferoverrun/bufferOverrunSemantics.ml

(*
 * Copyright (c) 2016 - present
 *
 * Programming Research Laboratory (ROPAS)
 * Seoul National University, Korea
 * All rights reserved.
 *
 * This source code is licensed under the BSD style license found in the
 * LICENSE file in the root directory of this source tree. An additional grant
 * of patent rights can be found in the PATENTS file in the same directory.
 *)

open! IStd
open AbsLoc

module F = Format
module L = Logging
module Domain = BufferOverrunDomain
open Domain

module Make (CFG : ProcCfg.S) =
struct
  exception Not_implemented

  let eval_const : Const.t -> Val.t
    = function
    | Const.Cint intlit -> (try Val.of_int (IntLit.to_int intlit) with _ -> Val.top_itv)
    | Const.Cfloat f -> f |> int_of_float |> Val.of_int
    | _ -> Val.top_itv       (* TODO *)

  let sizeof_ikind : Typ.ikind -> int
    = function
    | Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> 1
    | Typ.IInt | Typ.IUInt -> 4
    | Typ.IShort | Typ.IUShort -> 2
    | Typ.ILong | Typ.IULong -> 4
    | Typ.ILongLong | Typ.IULongLong -> 8
    | Typ.I128 | Typ.IU128 -> 16

  let sizeof_fkind : Typ.fkind -> int
    = function
    | Typ.FFloat -> 4
    | Typ.FDouble | Typ.FLongDouble -> 8

  (* NOTE: assume 32bit machine *)
  let rec sizeof (typ : Typ.t) : int =
    match typ.desc with
    | Typ.Tint ikind -> sizeof_ikind ikind
    | Typ.Tfloat fkind -> sizeof_fkind fkind
    | Typ.Tvoid -> 1
    | Typ.Tptr (_, _) -> 4
    | Typ.Tstruct _ -> 4        (* TODO *)
    | Typ.Tarray (_, Some length, Some stride) -> IntLit.to_int stride * IntLit.to_int length
    | Typ.Tarray (typ, Some length, None) -> sizeof typ * IntLit.to_int length
    | _ -> 4

  let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool
    = fun e1 e2 m ->
      match e1, e2 with
      | Exp.Var x1, Exp.Var x2 ->
        (match Mem.find_alias x1 m, Mem.find_alias x2 m with
        | Some x1', Some x2' -> Pvar.equal x1' x2'
        | _, _ -> false)
      | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) ->
        Unop.equal uop1 uop2 && must_alias e1' e2' m
      | Exp.BinOp (bop1, e11, e12), Exp.BinOp (bop2, e21, e22) ->
        Binop.equal bop1 bop2
        && must_alias e11 e21 m
        && must_alias e12 e22 m
      | Exp.Exn t1, Exp.Exn t2 -> must_alias t1 t2 m
      | Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2
      | Exp.Cast (t1, e1'), Exp.Cast (t2, e2') ->
        Typ.equal t1 t2 && must_alias e1' e2' m
      | Exp.Lvar x1, Exp.Lvar x2 ->
        Pvar.equal x1 x2
      | Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) ->
        must_alias e1 e2 m && Fieldname.equal fld1 fld2
      | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) ->
        must_alias e11 e21 m && must_alias e12 e22 m
      | Exp.Sizeof {nbytes=Some nbytes1}, Exp.Sizeof {nbytes=Some nbytes2} ->
        Int.equal nbytes1 nbytes2
      | Exp.Sizeof {typ=t1; dynamic_length=dynlen1; subtype=subt1},
        Exp.Sizeof {typ=t2; dynamic_length=dynlen2; subtype=subt2} ->
        Typ.equal t1 t2
        && must_alias_opt dynlen1 dynlen2 m
        && Int.equal (Subtype.compare subt1 subt2) 0
      | _, _ -> false

    and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool
      = fun e1_opt e2_opt m ->
        match e1_opt, e2_opt with
        | Some e1, Some e2 -> must_alias e1 e2 m
        | None, None -> true
        | _, _ -> false

  let comp_rev : Binop.t -> Binop.t
    = function
    | Binop.Lt -> Binop.Gt
    | Binop.Gt -> Binop.Lt
    | Binop.Le -> Binop.Ge
    | Binop.Ge -> Binop.Le
    | Binop.Eq -> Binop.Eq
    | Binop.Ne -> Binop.Ne
    | _ -> assert (false)

  let comp_not : Binop.t -> Binop.t
    = function
    | Binop.Lt -> Binop.Ge
    | Binop.Gt -> Binop.Le
    | Binop.Le -> Binop.Gt
    | Binop.Ge -> Binop.Lt
    | Binop.Eq -> Binop.Ne
    | Binop.Ne -> Binop.Eq
    | _ -> assert (false)

  let rec must_alias_cmp : Exp.t -> Mem.astate -> bool
    = fun e m ->
      match e with
      | Exp.BinOp (Binop.Lt, e1, e2)
      | Exp.BinOp (Binop.Gt, e1, e2)
      | Exp.BinOp (Binop.Ne, e1, e2) -> must_alias e1 e2 m
      | Exp.BinOp (Binop.LAnd, e1, e2) ->
        must_alias_cmp e1 m || must_alias_cmp e2 m
      | Exp.BinOp (Binop.LOr, e1, e2) ->
        must_alias_cmp e1 m && must_alias_cmp e2 m
      | Exp.UnOp (Unop.LNot, Exp.UnOp (Unop.LNot, e1, _), _) ->
        must_alias_cmp e1 m
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) ->
        must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
        let e1' = Exp.UnOp (Unop.LNot, e1, t) in
        let e2' = Exp.UnOp (Unop.LNot, e2, t) in
        must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LAnd, e1, e2), t) ->
        let e1' = Exp.UnOp (Unop.LNot, e1, t) in
        let e2' = Exp.UnOp (Unop.LNot, e2, t) in
        must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m
      | _ -> false

  let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t
    = fun exp mem loc ->
      if must_alias_cmp exp mem then Val.of_int 0 else
        match exp with
        | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem
        | Exp.Lvar pvar ->
          let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in
          let arr = Mem.find_stack_set ploc mem in
          ploc |> Val.of_pow_loc |> Val.join arr
        | Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc
        | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc
        | Exp.Const c -> eval_const c
        | Exp.Cast (_, e) -> eval e mem loc
        | Exp.Lfield (e, fn, _) ->
          eval e mem loc
          |> Val.get_array_locs
          |> Fn.flip PowLoc.append_field fn
          |> Val.of_pow_loc
        | Exp.Lindex (e1, _) ->
          let arr = eval e1 mem loc |> Val.get_array_blk in (* must have array blk *)
          (* let idx = eval e2 mem loc in *)
          let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in
          (* if nested array, add the array blk *)
          let arr = Mem.find_heap_set ploc mem in
          Val.join (Val.of_pow_loc ploc) arr
        | Exp.Sizeof {nbytes=Some size} -> Val.of_int size
        | Exp.Sizeof {typ; nbytes=None} -> Val.of_int (sizeof typ)
        | Exp.Exn _
        | Exp.Closure _ -> Val.top_itv

    and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t
      = fun unop e mem loc ->
        let v = eval e mem loc in
        match unop with
        | Unop.Neg -> Val.neg v
        | Unop.BNot -> Val.unknown_bit v
        | Unop.LNot -> Val.lnot v

      and eval_binop
        : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t
        = fun binop e1 e2 mem loc ->
          let v1 = eval e1 mem loc in
          let v2 = eval e2 mem loc in
          match binop with
          | Binop.PlusA ->
            Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2)
          | Binop.PlusPI -> Val.plus_pi v1 v2
          | Binop.MinusA ->
            Val.joins
              [ Val.minus v1 v2
              ; Val.minus_pi v1 v2
              ; Val.minus_pp v1 v2 ]
          | Binop.MinusPI -> Val.minus_pi v1 v2
          | Binop.MinusPP -> Val.minus_pp v1 v2
          | Binop.Mult -> Val.mult v1 v2
          | Binop.Div -> Val.div v1 v2
          | Binop.Mod -> Val.mod_sem v1 v2
          | Binop.Shiftlt -> Val.shiftlt v1 v2
          | Binop.Shiftrt -> Val.shiftrt v1 v2
          | Binop.Lt -> Val.lt_sem v1 v2
          | Binop.Gt -> Val.gt_sem v1 v2
          | Binop.Le -> Val.le_sem v1 v2
          | Binop.Ge -> Val.ge_sem v1 v2
          | Binop.Eq -> Val.eq_sem v1 v2
          | Binop.Ne -> Val.ne_sem v1 v2
          | Binop.BAnd
          | Binop.BXor
          | Binop.BOr -> Val.unknown_bit v1
          | Binop.LAnd -> Val.land_sem v1 v2
          | Binop.LOr -> Val.lor_sem v1 v2
          | Binop.PtrFld -> raise Not_implemented

  let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string
    = fun proc_name node inst_num dimension ->
      let proc_name = Typ.Procname.to_string proc_name in
      let node_num = CFG.hash node |> string_of_int in
      let inst_num = string_of_int inst_num in
      let dimension = string_of_int dimension in
      (proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension)
      |> Allocsite.make

  let eval_array_alloc
    : Typ.Procname.t -> CFG.node -> Typ.t -> ?stride:int -> Itv.t -> Itv.t -> int -> int -> Val.t
    = fun pdesc node typ ?stride:stride0 offset size inst_num dimension ->
      let allocsite = get_allocsite pdesc node inst_num dimension in
      let int_stride = match stride0 with
        | None -> sizeof typ
        | Some stride -> stride in
      let stride = Itv.of_int int_stride in
      ArrayBlk.make allocsite offset size stride
      |> Val.of_array_blk

  let prune_unop : Exp.t -> Mem.astate -> Mem.astate
    = fun e mem ->
      match e with
      | Exp.Var x ->
        (match Mem.find_alias x mem with
        | Some x' ->
          let lv = Loc.of_pvar x' in
          let v = Mem.find_heap lv mem in
          let v' = Val.prune_zero v in
          Mem.update_mem (PowLoc.singleton lv) v' mem
        | None -> mem)
      | Exp.UnOp (Unop.LNot, Exp.Var x, _) ->
        (match Mem.find_alias x mem with
        | Some x' ->
          let lv = Loc.of_pvar x' in
          let v = Mem.find_heap lv mem in
          let itv_v =
            if Itv.is_bot (Val.get_itv v) then Itv.bot else
              Val.get_itv Val.zero
          in
          let v' = Val.modify_itv itv_v v in
          Mem.update_mem (PowLoc.singleton lv) v' mem
        | None -> mem)
      | _ -> mem

  let prune_binop_left : Exp.t -> Location.t -> Mem.astate -> Mem.astate
    = fun e loc mem ->
      match e with
      | Exp.BinOp (Binop.Lt as comp, Exp.Var x, e')
      | Exp.BinOp (Binop.Gt as comp, Exp.Var x, e')
      | Exp.BinOp (Binop.Le as comp, Exp.Var x, e')
      | Exp.BinOp (Binop.Ge as comp, Exp.Var x, e') ->
        (match Mem.find_alias x mem with
        | Some x' ->
          let lv = Loc.of_pvar x' in
          let v = Mem.find_heap lv mem in
          let v' = Val.prune_comp comp v (eval e' mem loc) in
          Mem.update_mem (PowLoc.singleton lv) v' mem
        | None -> mem)
      | Exp.BinOp (Binop.Eq, Exp.Var x, e') ->
        (match Mem.find_alias x mem with
        | Some x' ->
          let lv = Loc.of_pvar x' in
          let v = Mem.find_heap lv mem in
          let v' = Val.prune_eq v (eval e' mem loc) in
          Mem.update_mem (PowLoc.singleton lv) v' mem
        | None -> mem)
      | Exp.BinOp (Binop.Ne, Exp.Var x, e') ->
        (match Mem.find_alias x mem with
        | Some x' ->
          let lv = Loc.of_pvar x' in
          let v = Mem.find_heap lv mem in
          let v' = Val.prune_ne v (eval e' mem loc) in
          Mem.update_mem (PowLoc.singleton lv) v' mem
        | None -> mem)
      | _ -> mem

  let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate
    = fun e loc mem ->
      match e with
      | Exp.BinOp (Binop.Lt as c, e', Exp.Var x)
      | Exp.BinOp (Binop.Gt as c, e', Exp.Var x)
      | Exp.BinOp (Binop.Le as c, e', Exp.Var x)
      | Exp.BinOp (Binop.Ge as c, e', Exp.Var x)
      | Exp.BinOp (Binop.Eq as c, e', Exp.Var x)
      | Exp.BinOp (Binop.Ne as c, e', Exp.Var x) ->
        prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem
      | _ -> mem

  let is_unreachable_constant : Exp.t -> Location.t -> Mem.astate -> bool
    = fun e loc m ->
      Val.(<=) ~lhs:(eval e m loc) ~rhs:(Val.of_int 0)

  let prune_unreachable : Exp.t -> Location.t -> Mem.astate -> Mem.astate
    = fun e loc mem ->
      if is_unreachable_constant e loc mem then Mem.bot else mem

  let rec prune : Exp.t -> Location.t -> Mem.astate -> Mem.astate
    = fun e loc mem ->
      let mem =
        mem
        |> prune_unreachable e loc
        |> prune_unop e
        |> prune_binop_left e loc
        |> prune_binop_right e loc
      in
      match e with
      | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
        prune e loc mem
      | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
        prune (Exp.UnOp (Unop.LNot, e, None)) loc mem
      | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> prune (Exp.Var x) loc mem
      | Exp.BinOp (Binop.LAnd, e1, e2) ->
        mem |> prune e1 loc |> prune e2 loc
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
        mem
        |> prune (Exp.UnOp (Unop.LNot, e1, t)) loc
        |> prune (Exp.UnOp (Unop.LNot, e2, t)) loc
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq as c, e1, e2), _)
      | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) ->
        prune (Exp.BinOp (comp_not c, e1, e2)) loc mem
      | _ -> mem

  let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list
    = fun pdesc ->
      let proc_name = Procdesc.get_proc_name pdesc in
      Procdesc.get_formals pdesc
      |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))

  let get_matching_pairs
    : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate
      -> (Itv.Bound.t * Itv.Bound.t) list
    = fun tenv formal actual typ caller_mem callee_mem ->
      let get_itv v = Val.get_itv v in
      let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in
      let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in
      let get_field_name (fn, _, _) = fn in
      let deref_field v fn mem =
        Mem.find_heap_set (PowLoc.append_field (Val.get_array_locs v) fn) mem
      in
      let deref_ptr v mem = Mem.find_heap_set (Val.get_array_locs v) mem in
      let add_pair_itv itv1 itv2 l =
        let open Itv in
        if itv1 <> bot && itv1 <> top && itv2 <> bot then
          (lb itv1, lb itv2) :: (ub itv1, ub itv2) :: l
        else if itv1 <> bot && itv1 <> top && Itv.eq itv2 bot then
          (lb itv1, Bound.Bot) :: (ub itv1, Bound.Bot) :: l
        else
          l
      in
      let add_pair_val v1 v2 pairs =
        pairs
        |> add_pair_itv (get_itv v1) (get_itv v2)
        |> add_pair_itv (get_offset v1) (get_offset v2)
        |> add_pair_itv (get_size v1) (get_size v2)
      in
      let add_pair_field v1 v2 pairs fn =
        let v1' = deref_field v1 fn callee_mem in
        let v2' = deref_field v2 fn caller_mem in
        add_pair_val v1' v2' pairs
      in
      let add_pair_ptr typ v1 v2 pairs =
        match typ.Typ.desc with
        | Typ.Tptr ({desc=Tstruct typename}, _) ->
          (match Tenv.lookup tenv typename with
          | Some str ->
            let fns = List.map ~f:get_field_name str.Typ.Struct.fields in
            List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns
          | _ -> pairs)
        | Typ.Tptr (_ ,_) ->
          let v1' = deref_ptr v1 callee_mem in
          let v2' = deref_ptr v2 caller_mem in
          add_pair_val v1' v2' pairs
        | _ -> pairs
      in
      [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual

  let subst_map_of_pairs
    : (Itv.Bound.t * Itv.Bound.t) list -> Itv.Bound.t Itv.SubstMap.t
    = fun pairs ->
      let add_pair map (formal, actual) =
        match formal with
        | Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 ->
          let (symbol, coeff) = Itv.SymLinear.choose se1 in
          if Int.equal coeff 1
          then Itv.SubstMap.add symbol actual map
          else assert false
        | _ -> assert false
      in
      List.fold ~f:add_pair ~init:Itv.SubstMap.empty pairs

  let rec list_fold2_def
    : default:Val.t -> f:('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> init:'b -> 'b
    = fun ~default ~f xs ys ~init:acc ->
      match xs, ys with
      | [], _ -> acc
      | x :: xs', [] -> list_fold2_def ~default ~f xs' ys ~init:(f x default acc)
      | [x], _ :: _ -> f x (List.fold ~f:Val.join ~init:Val.bot ys) acc
      | x :: xs', y :: ys' -> list_fold2_def ~default ~f xs' ys' ~init:(f x y acc)

  let get_subst_map
    : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate
      -> Location.t -> Itv.Bound.t Itv.SubstMap.t
    = fun tenv callee_pdesc params caller_mem callee_entry_mem loc ->
      let add_pair (formal, typ) actual l =
        let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in
        let new_matching =
          get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem
        in
        List.rev_append new_matching l
      in
      let formals = get_formals callee_pdesc in
      let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem loc) params in
      list_fold2_def ~default:Val.top_itv ~f:add_pair formals actuals ~init:[]
      |> subst_map_of_pairs
end