diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 9c058515e..4798a852f 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -150,16 +150,16 @@ module NullifyTransferFunctions = struct let exec_instr ((active_defs, to_nullify) as astate) _ = function | Sil.Letderef (lhs_id, _, _, _) -> - VarDomain.add (Var.LogicalVar lhs_id) active_defs, to_nullify + VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify | Sil.Call (lhs_ids, _, _, _, _) -> let active_defs' = IList.fold_left - (fun acc id -> VarDomain.add (Var.LogicalVar id) acc) + (fun acc id -> VarDomain.add (Var.of_id id) acc) active_defs lhs_ids in active_defs', to_nullify | Sil.Set (Sil.Lvar lhs_pvar, _, _, _) -> - VarDomain.add (Var.ProgramVar lhs_pvar) active_defs, to_nullify + VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify | Sil.Set _ | Prune _ | Declare_locals _ | Stackop _ | Remove_temps _ | Abstract _ -> astate @@ -214,11 +214,11 @@ let add_nullify_instrs tenv _ pdesc = | Some (_, to_nullify) -> let pvars_to_nullify, ids_to_remove = Var.Set.fold - (fun var (pvars_acc, ids_acc) -> match var with + (fun var (pvars_acc, ids_acc) -> match Var.to_exp var with (* we nullify all address taken variables at the end of the procedure *) - | ProgramVar pvar when not (AddressTaken.Domain.mem pvar address_taken_vars) -> + | Sil.Lvar pvar when not (AddressTaken.Domain.mem pvar address_taken_vars) -> pvar :: pvars_acc, ids_acc - | LogicalVar id -> + | Sil.Var id -> pvars_acc, id :: ids_acc | _ -> pvars_acc, ids_acc) to_nullify diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 246bfcd21..f467f2cfb 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -317,8 +317,8 @@ module TransferFunctions = struct | _ -> false let is_tracking_exp astate = function - | Sil.Var id -> Domain.is_tracked_var (Var.LogicalVar id) astate - | Sil.Lvar pvar -> Domain.is_tracked_var (Var.ProgramVar pvar) astate + | Sil.Var id -> Domain.is_tracked_var (Var.of_id id) astate + | Sil.Lvar pvar -> Domain.is_tracked_var (Var.of_pvar pvar) astate | _ -> false let prunes_tracking_var astate = function @@ -334,7 +334,7 @@ module TransferFunctions = struct let exec_instr astate { ProcData.pdesc; tenv; } = function | Sil.Call ([id], Const (Cfun callee_pname), _, _, _) when is_unlikely callee_pname -> - Domain.add_tracking_var (Var.LogicalVar id) astate + Domain.add_tracking_var (Var.of_id id) astate | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) -> (* Run the analysis of callee_pname if not already analyzed *) ignore (Summary.read_summary pdesc callee_pname); @@ -350,12 +350,12 @@ module TransferFunctions = struct |> add_allocations | Sil.Letderef (id, exp, _, _) when is_tracking_exp astate exp -> - Domain.add_tracking_var (Var.LogicalVar id) astate + Domain.add_tracking_var (Var.of_id id) astate | Sil.Set (Sil.Lvar pvar, _, exp, _) when is_tracking_exp astate exp -> - Domain.add_tracking_var (Var.ProgramVar pvar) astate + Domain.add_tracking_var (Var.of_pvar pvar) astate | Sil.Set (Sil.Lvar pvar, _, _, _) -> - Domain.remove_tracking_var (Var.ProgramVar pvar) astate + Domain.remove_tracking_var (Var.of_pvar pvar) astate | Sil.Prune (exp, _, _, _) when prunes_tracking_var astate exp -> Domain.stop_tracking astate diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index 6b326a2e2..eb53f2ee7 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -27,7 +27,7 @@ module Domain = struct else Var.Map.for_all (fun k v -> - try Var.var_equal v (Var.Map.find k lhs) + try Var.equal v (Var.Map.find k lhs) with Not_found -> false) rhs @@ -37,7 +37,7 @@ module Domain = struct else let keep_if_same _ v1_opt v2_opt = match v1_opt, v2_opt with | Some v1, Some v2 -> - if Var.var_equal v1 v2 then Some v1 else None + if Var.equal v1 v2 then Some v1 else None | _ -> None in Var.Map.merge keep_if_same astate1 astate2 @@ -45,21 +45,21 @@ module Domain = struct join prev next let pp fmt astate = - let pp_value = Var.pp_var in + let pp_value = Var.pp in Var.Map.pp ~pp_value fmt astate let gen var1 var2 astate = (* don't add tautological copies *) - if Var.var_equal var1 var2 + if Var.equal var1 var2 then astate else Var.Map.add var1 var2 astate let kill_copies_with_var var astate = let do_kill lhs_var rhs_var astate_acc = - if Var.var_equal var lhs_var + if Var.equal var lhs_var then astate_acc (* kill copies vith [var] on lhs *) else - if Var.var_equal var rhs_var + if Var.equal var rhs_var then (* delete [var] = [rhs_var] copy, but add [lhs_var] = M(rhs_var) copy*) try Var.Map.add lhs_var (Var.Map.find rhs_var astate) astate_acc with Not_found -> astate_acc @@ -70,9 +70,9 @@ module Domain = struct (* kill the previous binding for [lhs_var], and add a new [lhs_var] -> [rhs_var] binding *) let kill_then_gen lhs_var rhs_var astate = let already_has_binding lhs_var rhs_var astate = - try Var.var_equal rhs_var (Var.Map.find lhs_var astate) + try Var.equal rhs_var (Var.Map.find lhs_var astate) with Not_found -> false in - if Var.var_equal lhs_var rhs_var || already_has_binding lhs_var rhs_var astate + if Var.equal lhs_var rhs_var || already_has_binding lhs_var rhs_var astate then astate (* already have this binding; no need to kill or gen *) else kill_copies_with_var lhs_var astate @@ -88,15 +88,15 @@ module TransferFunctions = struct let exec_instr astate _ = function | Sil.Letderef (lhs_id, Sil.Lvar rhs_pvar, _, _) when not (Pvar.is_global rhs_pvar) -> - Domain.gen (LogicalVar lhs_id) (ProgramVar rhs_pvar) astate + Domain.gen (Var.of_id lhs_id) (Var.of_pvar rhs_pvar) astate | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Var rhs_id, _) when not (Pvar.is_global lhs_pvar) -> - Domain.kill_then_gen (ProgramVar lhs_pvar) (LogicalVar rhs_id) astate + Domain.kill_then_gen (Var.of_pvar lhs_pvar) (Var.of_id rhs_id) astate | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Lvar rhs_pvar, _) when not (Pvar.is_global lhs_pvar || Pvar.is_global rhs_pvar) -> - Domain.kill_then_gen (ProgramVar lhs_pvar) (ProgramVar rhs_pvar) astate + Domain.kill_then_gen (Var.of_pvar lhs_pvar) (Var.of_pvar rhs_pvar) astate | Sil.Set (Sil.Lvar lhs_pvar, _, _, _) -> (* non-copy assignment (or assignment to global); can only kill *) - Domain.kill_copies_with_var (ProgramVar lhs_pvar) astate + Domain.kill_copies_with_var (Var.of_pvar lhs_pvar) astate | Sil.Letderef _ (* lhs = *rhs where rhs isn't a pvar (or is a global). in any case, not a copy *) (* note: since logical vars can't be reassigned, don't need to kill bindings for lhs id *) @@ -105,9 +105,9 @@ module TransferFunctions = struct astate | Sil.Call (ret_ids, _, actuals, _, _) -> let kill_ret_ids astate_acc id = - Domain.kill_copies_with_var (LogicalVar id) astate_acc in + Domain.kill_copies_with_var (Var.of_id id) astate_acc in let kill_actuals_by_ref astate_acc = function - | (Sil.Lvar pvar, Sil.Tptr _) -> Domain.kill_copies_with_var (ProgramVar pvar) astate_acc + | (Sil.Lvar pvar, Sil.Tptr _) -> Domain.kill_copies_with_var (Var.of_pvar pvar) astate_acc | _ -> astate_acc in let astate' = IList.fold_left kill_ret_ids astate ret_ids in if !Config.curr_language = Config.Java diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 11d86a3dc..6ebc9b68e 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -29,18 +29,18 @@ module TransferFunctions = struct let exp_add_live exp astate = let (ids, pvars) = Sil.exp_get_vars exp in let astate' = - IList.fold_left (fun astate_acc id -> Domain.add (LogicalVar id) astate_acc) astate ids in - IList.fold_left (fun astate_acc pvar -> Domain.add (ProgramVar pvar) astate_acc) astate' pvars + IList.fold_left (fun astate_acc id -> Domain.add (Var.of_id id) astate_acc) astate ids in + IList.fold_left (fun astate_acc pvar -> Domain.add (Var.of_pvar pvar) astate_acc) astate' pvars let exec_instr astate _ = function | Sil.Letderef (lhs_id, rhs_exp, _, _) -> - Domain.remove (LogicalVar lhs_id) astate + Domain.remove (Var.of_id lhs_id) astate |> exp_add_live rhs_exp | Sil.Set (Lvar lhs_pvar, _, rhs_exp, _) -> let astate' = if Pvar.is_global lhs_pvar then astate (* never kill globals *) - else Domain.remove (ProgramVar lhs_pvar) astate in + else Domain.remove (Var.of_pvar lhs_pvar) astate in exp_add_live rhs_exp astate' | Sil.Set (lhs_exp, _, rhs_exp, _) -> exp_add_live lhs_exp astate @@ -49,7 +49,7 @@ module TransferFunctions = struct exp_add_live exp astate | Sil.Call (ret_ids, call_exp, params, _, _) -> IList.fold_right - (fun ret_id astate_acc -> Domain.remove (LogicalVar ret_id) astate_acc) + (fun ret_id astate_acc -> Domain.remove (Var.of_id ret_id) astate_acc) ret_ids astate |> exp_add_live call_exp diff --git a/infer/src/checkers/var.ml b/infer/src/checkers/var.ml index c8a46484d..2ec7754fb 100644 --- a/infer/src/checkers/var.ml +++ b/infer/src/checkers/var.ml @@ -9,7 +9,7 @@ open! Utils -(** single abstraction for all the kinds of variables in SIL *) +(** Single abstraction for all the kinds of variables in SIL *) type var = | ProgramVar of Pvar.t @@ -17,27 +17,37 @@ type var = type t = var -let var_compare v1 v2 = match v1, v2 with +let of_id id = + LogicalVar id + +let of_pvar pvar = + ProgramVar pvar + +let to_exp = function + | ProgramVar pvar -> Sil.Lvar pvar + | LogicalVar id -> Sil.Var id + +let compare v1 v2 = match v1, v2 with | ProgramVar pv1, ProgramVar pv2 -> Pvar.compare pv1 pv2 | LogicalVar sv1, LogicalVar sv2 -> Ident.compare sv1 sv2 | ProgramVar _, _ -> 1 | LogicalVar _, _ -> -1 -let var_equal v1 v2 = - var_compare v1 v2 = 0 +let equal v1 v2 = + compare v1 v2 = 0 -let pp_var fmt = function +let pp fmt = function | ProgramVar pv -> (Pvar.pp pe_text) fmt pv | LogicalVar id -> (Ident.pp pe_text) fmt id module Map = PrettyPrintable.MakePPMap(struct type t = var - let compare = var_compare - let pp_key = pp_var + let compare = compare + let pp_key = pp end) module Set = PrettyPrintable.MakePPSet(struct type t = var - let compare = var_compare - let pp_element = pp_var + let compare = compare + let pp_element = pp end) diff --git a/infer/src/checkers/var.mli b/infer/src/checkers/var.mli new file mode 100644 index 000000000..b41cf6e8b --- /dev/null +++ b/infer/src/checkers/var.mli @@ -0,0 +1,28 @@ +(* + * 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. + *) + +(** Single abstraction for all the kinds of variables in SIL *) + +type t + +val of_id : Ident.t -> t + +val of_pvar : Pvar.t -> t + +val to_exp : t -> Sil.exp + +val equal : t -> t -> bool + +val compare : t -> t -> int + +val pp : Format.formatter -> t -> unit + +module Map : PrettyPrintable.PPMap with type key = t + +module Set : PrettyPrintable.PPSet with type elt = t