pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

hiding implementation of var

Browse Source 
Reviewed By: jberdine

Differential Revision: D3310210

fbshipit-source-id: 96a498d
master
Sam Blackshear 9 years ago committed by Facebook Github Bot 3
parent fd04004b43
commit cfa7739963
6 changed files with 78 additions and 40 deletions
Show Stats Download Patch File Download Diff File

12
infer/src/backend/preanal.ml
Unescape View File

@ -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

12
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -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

28
infer/src/checkers/copyPropagation.ml
Unescape View File

@ -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

10
infer/src/checkers/liveness.ml
Unescape View File

@ -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

28
infer/src/checkers/var.ml
Unescape View File

@ -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)

28
infer/src/checkers/var.mli
Unescape View File

@ -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
Write Preview
Loading…
Cancel
Save