infer_clone/infer/src/checkers/IdAccessPathMapDomain.ml

(*
 * Copyright (c) 2016 - present Facebook, Inc.
 * 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
module IdMap = Var.Map
module L = Logging

type astate = AccessPath.t IdMap.t

include IdMap

let pp fmt astate = IdMap.pp ~pp_value:AccessPath.pp fmt astate

let check_invariant ap1 ap2 = function
  | Var.ProgramVar pvar when Pvar.is_ssa_frontend_tmp pvar ->
      (* Sawja reuses temporary variables which sometimes breaks this invariant *)
      ()
  | id ->
      if not (AccessPath.equal ap1 ap2) then
        L.(die InternalError)
          "Id %a maps to both %a and %a" Var.pp id AccessPath.pp ap1 AccessPath.pp ap2


let ( <= ) ~lhs ~rhs =
  if phys_equal lhs rhs then true
  else
    IdMap.for_all
      (fun id lhs_ap ->
        let rhs_has = IdMap.mem id rhs in
        if rhs_has && Config.debug_exceptions then check_invariant lhs_ap (IdMap.find id rhs) id ;
        rhs_has )
      lhs


let join astate1 astate2 =
  if phys_equal astate1 astate2 then astate1
  else
    IdMap.merge
      (fun var ap1_opt ap2_opt ->
        match (ap1_opt, ap2_opt) with
        | Some ap1, Some ap2 ->
            if Config.debug_exceptions then check_invariant ap1 ap2 var ;
            ap1_opt
        | Some _, None ->
            ap1_opt
        | None, Some _ ->
            ap2_opt
        | None, None ->
            None )
      astate1 astate2


let widen ~prev ~next ~num_iters:_ = join prev next