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

opacify the type of node ids

Browse Source 
Summary:Make node ids be `private int` to make sure we don't mix them with random
integers from other sources.

Reviewed By: sblackshear, cristianoc

Differential Revision: D3179670

fb-gh-sync-id: 4bcf4f0
fbshipit-source-id: 4bcf4f0
master
Jules Villard 9 years ago committed by Facebook Github Bot 1
parent ac6ef1d9f6
commit 70c8494625
17 changed files with 86 additions and 73 deletions
Show Stats Download Patch File Download Diff File

7
infer/src/IR/cfg.ml
Unescape View File

@ -17,6 +17,8 @@ module F = Format
(* =============== START of module Node =============== *)
module Node = struct
type id = int
type nodekind =
| Start_node of proc_desc
| Exit_node of proc_desc
@ -27,7 +29,7 @@ module Node = struct
and t = { (** a node *)
(** unique id of the node *)
nd_id : int;
nd_id : id;
(** distance to the exit node *)
mutable nd_dist_exit : int option;
@ -204,6 +206,9 @@ module Node = struct
(** Get the unique id of the node *)
let get_id node = node.nd_id
(** compare node ids *)
let id_compare = int_compare
let get_succs node = node.nd_succs
type node = t

7
infer/src/IR/cfg.mli
Unescape View File

@ -127,6 +127,8 @@ end
module Node : sig
type t = node (** type of nodes *)
type id = private int
(** kind of cfg node *)
type nodekind =
| Start_node of Procdesc.t
@ -192,7 +194,10 @@ module Node : sig
val get_exn : t -> t list
(** Get the unique id of the node *)
val get_id : t -> int
val get_id : t -> id
(** compare node ids *)
val id_compare : id -> id -> int
(** Get the source location of the node *)
val get_loc : t -> Location.t

9
infer/src/backend/dotty.ml
Unescape View File

@ -924,7 +924,7 @@ let pp_proplist_parsed2dotty_file filename plist =
(* channel. You have to compute an interprocedural cfg first *)
let pp_cfgnodename fmt (n : Cfg.Node.t) =
F.fprintf fmt "%d" (Cfg.Node.get_id n)
F.fprintf fmt "%d" (Cfg.Node.get_id n :> int)
let pp_etlist fmt etl =
IList.iter (fun (id, ty) ->
@ -962,7 +962,7 @@ let pp_cfgnodelabel fmt (n : Cfg.Node.t) =
let pp_instrs fmt instrs =
IList.iter (fun i -> F.fprintf fmt " %s\\n " (instr_string i)) instrs in
let instrs = Cfg.Node.get_instrs n in
F.fprintf fmt "%d: %a \\n %a" (Cfg.Node.get_id n) pp_label n pp_instrs instrs
F.fprintf fmt "%d: %a \\n %a" (Cfg.Node.get_id n :> int) pp_label n pp_instrs instrs
let pp_cfgnodeshape fmt (n: Cfg.Node.t) =
match Cfg.Node.get_kind n with
@ -987,7 +987,10 @@ let pp_cfgnode fmt (n: Cfg.Node.t) =
| Cfg.Node.Exit_node _ when is_exn = true -> (* don't print exception edges to the exit node *)
()
| _ ->
F.fprintf fmt "\n\t %d -> %d %s;" (Cfg.Node.get_id n1) (Cfg.Node.get_id n2) color in
F.fprintf fmt "\n\t %d -> %d %s;"
(Cfg.Node.get_id n1 :> int)
(Cfg.Node.get_id n2 :> int)
color in
IList.iter (fun n' -> print_edge n n' false) (Cfg.Node.get_succs n);
IList.iter (fun n' -> print_edge n n' true) (Cfg.Node.get_exn n)

4
infer/src/backend/errdesc.ml
Unescape View File

@ -115,7 +115,7 @@ let find_normal_variable_funcall
("find_normal_variable_funcall could not find " ^
Ident.to_string id ^
" in node " ^
string_of_int (Cfg.Node.get_id node));
string_of_int (Cfg.Node.get_id node :> int));
L.d_ln ());
!res
@ -257,7 +257,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
("find_normal_variable_letderef could not find " ^
Ident.to_string id ^
" in node " ^
string_of_int (Cfg.Node.get_id node));
string_of_int (Cfg.Node.get_id node :> int));
L.d_ln ());
!res

28
infer/src/backend/interproc.ml
Unescape View File

@ -58,15 +58,12 @@ module NodeVisitSet =
(** Table for the results of the join operation on nodes. *)
module Join_table : sig
type t
type node_id = int
val add : t -> node_id -> Paths.PathSet.t -> unit
val add : t -> Cfg.Node.id -> Paths.PathSet.t -> unit
val create : unit -> t
val find : t -> node_id -> Paths.PathSet.t
val find : t -> Cfg.Node.id -> Paths.PathSet.t
end = struct
type t = (int, Paths.PathSet.t) Hashtbl.t
type node_id = int
type t = (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t
let create () : t =
Hashtbl.create 11
@ -83,14 +80,12 @@ end
module Worklist = struct
module NodeMap = Map.Make(Cfg.Node)
type node_id = int
type t = {
join_table : Join_table.t; (** Table of join results *)
path_set_todo : (node_id, Paths.PathSet.t) Hashtbl.t; (** Pathset todo *)
path_set_visited : (node_id, Paths.PathSet.t) Hashtbl.t; (** Pathset visited *)
path_set_todo : (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t; (** Pathset todo *)
path_set_visited : (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t; (** Pathset visited *)
mutable todo_set : NodeVisitSet.t; (** Set of nodes still to do, with visit count *)
mutable visit_map : node_id NodeMap.t; (** Map from nodes done to visit count *)
mutable visit_map : int NodeMap.t; (** Map from nodes done to visit count *)
}
let create () = {
@ -132,7 +127,8 @@ let path_set_create_worklist pdesc =
Cfg.Procdesc.compute_distance_to_exit_node pdesc;
Worklist.create ()
let htable_retrieve (htable : (int, Paths.PathSet.t) Hashtbl.t) (key : int) : Paths.PathSet.t =
let htable_retrieve (htable : (Cfg.Node.id, Paths.PathSet.t) Hashtbl.t) (key : Cfg.Node.id)
: Paths.PathSet.t =
try
Hashtbl.find htable key
with Not_found ->
@ -344,7 +340,7 @@ let do_before_node session node =
State.set_node node;
State.set_session session;
L.reset_delayed_prints ();
Printer.node_start_session node loc proc_name session
Printer.node_start_session node loc proc_name (session :> int)
let do_after_node node =
Printer.node_finish_session node
@ -493,9 +489,9 @@ let mark_visited summary node =
let stats = summary.Specs.stats in
if !Config.footprint
then
stats.Specs.nodes_visited_fp <- IntSet.add node_id stats.Specs.nodes_visited_fp
stats.Specs.nodes_visited_fp <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_fp
else
stats.Specs.nodes_visited_re <- IntSet.add node_id stats.Specs.nodes_visited_re
stats.Specs.nodes_visited_re <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_re
let forward_tabulate tenv wl =
let handled_some_exception = ref false in
@ -549,7 +545,7 @@ let forward_tabulate tenv wl =
handled_some_exception := false;
check_prop_size pathset_todo;
L.d_strln ("**** " ^ (log_string proc_name) ^ " " ^
"Node: " ^ string_of_int curr_node_id ^ ", " ^
"Node: " ^ string_of_int (curr_node_id :> int) ^ ", " ^
"Procedure: " ^ Procname.to_string proc_name ^ ", " ^
"Session: " ^ string_of_int session ^ ", " ^
"Todo: " ^ string_of_int (Paths.PathSet.size pathset_todo) ^ " ****");

13
infer/src/backend/paths.ml
Unescape View File

@ -271,7 +271,7 @@ end = struct
let get_path_pos node =
let pn = Cfg.Procdesc.get_proc_name (Cfg.Node.get_proc_desc node) in
let n_id = Cfg.Node.get_id node in
(pn, n_id)
(pn, (n_id :> int))
let contains_position path pos =
let found = ref false in
@ -291,10 +291,13 @@ end = struct
| Pstart _ -> f level path session prev_exn_opt
| Pnode (_, exn_opt, session', p, _, _) ->
let next_exn_opt = if prev_exn_opt <> None then None else exn_opt in (* no two consecutive exceptions *)
doit level session' p next_exn_opt;
doit level (session' :> int) p next_exn_opt;
f level path session prev_exn_opt
| Pjoin (p1, p2, _) ->
if (Invariant.get_stats p1).max_length >= (Invariant.get_stats p2).max_length then doit level session p1 prev_exn_opt else doit level session p2 prev_exn_opt
if (Invariant.get_stats p1).max_length >= (Invariant.get_stats p2).max_length then
doit level session p1 prev_exn_opt
else
doit level session p2 prev_exn_opt
| Pcall (p1, _, p2, _) ->
let next_exn_opt = None in (* exn must already be inside the call *)
doit level session p1 next_exn_opt;
@ -367,7 +370,7 @@ end = struct
"linear paths: " ^ string_of_float (Invariant.get_stats path).linear_num ^
" max length: " ^ string_of_int (Invariant.get_stats path).max_length ^
" has repetitions: " ^ string_of_int repetitions ^
" of node " ^ (string_of_int (Cfg.Node.get_id node)) in
" of node " ^ (string_of_int (Cfg.Node.get_id node :> int)) in
Invariant.reset_stats path;
str
@ -411,7 +414,7 @@ end = struct
| Pstart (node, _) ->
F.fprintf fmt "n%a" Cfg.Node.pp node
| Pnode (node, _, session, path, _, _) ->
F.fprintf fmt "%a(s%d).n%a" (doit (n - 1)) path session Cfg.Node.pp node
F.fprintf fmt "%a(s%d).n%a" (doit (n - 1)) path (session :> int) Cfg.Node.pp node
| Pjoin (path1, path2, _) ->
F.fprintf fmt "(%a + %a)" (doit (n - 1)) path1 (doit (n - 1)) path2
| Pcall (path1, _, path2, _) ->

50
infer/src/backend/printer.ml
Unescape View File

@ -86,9 +86,9 @@ let node_is_visited node =
| Some summary ->
let stats = summary.Specs.stats in
let is_visited_fp =
IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_fp in
IntSet.mem (Cfg.Node.get_id node :> int) stats.Specs.nodes_visited_fp in
let is_visited_re =
IntSet.mem (Cfg.Node.get_id node) stats.Specs.nodes_visited_re in
IntSet.mem (Cfg.Node.get_id node :> int) stats.Specs.nodes_visited_re in
is_visited_fp, is_visited_re
(** Return true if the node was visited during analysis *)
@ -130,24 +130,24 @@ end = struct
F.fprintf fmt "<br>PREDS:@\n";
IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] ""
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node))
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node))
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node))
(is_visited node) false fmt (Cfg.Node.get_id node)) preds;
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list)
(is_visited node) false fmt (Cfg.Node.get_id node :> int)) preds;
F.fprintf fmt "<br>SUCCS: @\n";
IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] ""
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node))
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node))
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node))
(is_visited node) false fmt (Cfg.Node.get_id node)) succs;
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list)
(is_visited node) false fmt (Cfg.Node.get_id node :> int)) succs;
F.fprintf fmt "<br>EXN: @\n";
IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] ""
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node))
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node))
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node))
(is_visited node) false fmt (Cfg.Node.get_id node)) exn;
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list)
(is_visited node) false fmt (Cfg.Node.get_id node :> int)) exn;
F.fprintf fmt "<br>@\n";
F.pp_print_flush fmt ();
true
@ -360,7 +360,7 @@ let force_delayed_prints () =
let start_session node (loc: Location.t) proc_name session =
let node_id = Cfg.Node.get_id node in
(if NodesHtml.start_node
node_id loc proc_name
(node_id :> int) loc proc_name
(Cfg.Node.get_preds node)
(Cfg.Node.get_succs node)
(Cfg.Node.get_exn node)
@ -372,7 +372,7 @@ let start_session node (loc: Location.t) proc_name session =
F.fprintf !curr_html_formatter "%a%a"
Io_infer.Html.pp_hline ()
(Io_infer.Html.pp_session_link ~with_name: true [".."])
(node_id, session, loc.Location.line);
((node_id :> int), session, loc.Location.line);
F.fprintf !curr_html_formatter "<LISTING>%a"
Io_infer.Html.pp_start_color Black
@ -387,7 +387,7 @@ let node_finish_session node =
if !Config.write_html then begin
F.fprintf !curr_html_formatter "</LISTING>%a"
Io_infer.Html.pp_end_color ();
NodesHtml.finish_node (Cfg.Node.get_id node)
NodesHtml.finish_node (Cfg.Node.get_id node :> int)
end
(** Write html file for the procedure.
@ -409,10 +409,10 @@ let write_proc_html whole_seconds pdesc =
(fun n ->
Io_infer.Html.pp_node_link []
(Cfg.Node.get_description (pe_html Black) n)
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n))
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n))
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n))
(is_visited n) false fmt (Cfg.Node.get_id n))
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list)
(is_visited n) false fmt (Cfg.Node.get_id n :> int))
nodes;
(match Specs.get_summary pname with
| None ->
@ -512,13 +512,13 @@ let write_html_file linereader filename cfg =
Io_infer.Html.pp_node_link
[fname_encoding]
(Cfg.Node.get_description (pe_html Black) n)
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n))
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n))
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n))
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list)
(is_visited n)
isproof
fmt
(Cfg.Node.get_id n))
(Cfg.Node.get_id n :> int))
nodes_at_linenum;
IList.iter
(fun n ->

4
infer/src/backend/reporting.ml
Unescape View File

@ -37,10 +37,10 @@ let log_issue_from_errlog
| None -> State.get_loc ()
| Some loc -> loc in
let node_id = match node_id with
| None -> State.get_node_id_key ()
| None -> (State.get_node_id_key () :> int * int)
| Some node_id -> node_id in
let session = match session with
| None -> State.get_session ()
| None -> (State.get_session () :> int)
| Some session -> session in
let ltr = match ltr with
| None -> State.get_loc_trace ()

6
infer/src/backend/specs.ml
Unescape View File

@ -143,8 +143,8 @@ end
module Visitedset =
Set.Make (struct
type t = int * int list
let compare (node_id1, _) (node_id2, _) = int_compare node_id1 node_id2
type t = Cfg.Node.id * int list
let compare (node_id1, _) (node_id2, _) = Cfg.Node.id_compare node_id1 node_id2
end)
let visited_str vis =
@ -324,7 +324,7 @@ type payload =
type summary =
{ dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *)
nodes: int list; (** ids of cfg nodes of the procedure *)
nodes: Cfg.Node.id list; (** ids of cfg nodes of the procedure *)
phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *)
payload: payload; (** payload containing the result of some analysis *)
sessions: int ref; (** Session number: how many nodes went trough symbolic execution *)

6
infer/src/backend/specs.mli
Unescape View File

@ -61,7 +61,7 @@ module Jprop : sig
end
(** set of visited nodes: node id and list of lines of all the instructions *)
module Visitedset : Set.S with type elt = int * int list
module Visitedset : Set.S with type elt = Cfg.Node.id * int list
(** convert a Visitedset to a string *)
val visited_str : Visitedset.t -> string
@ -137,7 +137,7 @@ type payload =
(** Procedure summary *)
type summary =
{ dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *)
nodes: int list; (** ids of cfg nodes of the procedure *)
nodes: Cfg.Node.id list; (** ids of cfg nodes of the procedure *)
phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *)
payload: payload; (** payload containing the result of some analysis *)
sessions: int ref; (** Session number: how many nodes went trough symbolic execution *)
@ -220,7 +220,7 @@ val is_inactive : Procname.t -> bool
Do nothing if a summary exists already. *)
val init_summary :
(Procname.t list * (** depend list *)
int list * (** nodes *)
Cfg.Node.id list * (** nodes *)
proc_flags * (** procedure flags *)
(Procname.t * Location.t) list * (** calls *)
(Cg.in_out_calls option) * (** in and out calls *)

7
infer/src/backend/state.ml
Unescape View File

@ -277,7 +277,7 @@ let get_path_pos () =
| Some (_, _, pdesc) -> Cfg.Procdesc.get_proc_name pdesc
| None -> Procname.from_string_c_fun "unknown_procedure" in
let nid = get_node_id () in
(pname, nid)
(pname, (nid :> int))
let mark_execution_start node =
let fs = get_failure_stats node in
@ -298,11 +298,12 @@ let mark_instr_ok () =
let mark_instr_fail pre_opt exn =
let loc = get_loc () in
let key = get_node_id_key () in
let key = (get_node_id_key () :> int * int) in
let session = get_session () in
let loc_trace = get_loc_trace () in
let fs = get_failure_stats (get_node ()) in
if fs.first_failure = None then fs.first_failure <- Some (loc, key, session, loc_trace, pre_opt, exn);
if fs.first_failure = None then
fs.first_failure <- Some (loc, key, (session :> int), loc_trace, pre_opt, exn);
fs.instr_fail <- fs.instr_fail + 1
type log_issue =

4
infer/src/backend/state.mli
Unescape View File

@ -45,10 +45,10 @@ val get_loc_trace : unit -> Errlog.loc_trace
val get_node : unit -> Cfg.Node.t
(** Get id of last node seen in symbolic execution *)
val get_node_id : unit -> int
val get_node_id : unit -> Cfg.Node.id
(** Get id and key of last node seen in symbolic execution *)
val get_node_id_key : unit -> int * int
val get_node_id_key : unit -> Cfg.Node.id * int
(** return the normalized precondition extracted form the last prop seen, if any
the abstraction function is a parameter to get around module dependencies *)

2
infer/src/checkers/checkDeadCode.ml
Unescape View File

@ -78,7 +78,7 @@ let check_final_state proc_name proc_desc final_s =
IList.filter (fun n -> not (Cfg.NodeSet.mem n (State.get_visited final_s))) proc_nodes in
let do_node n =
let loc = Cfg.Node.get_loc n in
let description = Format.sprintf "Node not visited: %d" (Cfg.Node.get_id n) in
let description = Format.sprintf "Node not visited: %d" (Cfg.Node.get_id n :> int) in
let report = match Cfg.Node.get_kind n with
| Cfg.Node.Join_node -> false
| k when k = Cfg.Node.exn_sink_kind -> false

2
infer/src/checkers/checkTraceCallSequence.ml
Unescape View File

@ -303,7 +303,7 @@ end
(** State transformation for a cfg node. *)
let do_node pn pd idenv _ node (s : State.t) : (State.t list) * (State.t list) =
if verbose then L.stderr "N:%d S:%s@." (Cfg.Node.get_id node) (State.to_string s);
if verbose then L.stderr "N:%d S:%s@." (Cfg.Node.get_id node :> int) (State.to_string s);
let curr_state = ref s in

2
infer/src/checkers/constantPropagation.ml
Unescape View File

@ -112,7 +112,7 @@ module ConstantFlow = Dataflow.MakeDF(struct
if verbose then
begin
L.stdout "Node %i:" (Cfg.Node.get_id node);
L.stdout "Node %i:" (Cfg.Node.get_id node :> int);
L.stdout "%a" pp constants;
IList.iter
(fun instr -> L.stdout "%a@." (Sil.pp_instr pe_text) instr)

6
infer/src/checkers/procCfg.ml
Unescape View File

@ -48,7 +48,7 @@ end
module Forward : Wrapper with type node = Cfg.node = struct
type t = Cfg.Procdesc.t
type node = Cfg.node
type node_id = int
type node_id = Cfg.Node.id
let node_id = Cfg.Node.get_id
let succs _ n = Cfg.Node.get_succs n
@ -63,10 +63,10 @@ module Forward : Wrapper with type node = Cfg.node = struct
let from_pdesc pdesc = pdesc
let node_id_compare = int_compare
let node_id_compare = Cfg.Node.id_compare
let pp_node = Cfg.Node.pp
let pp_node_id fmt n = F.fprintf fmt "%d" n
let pp_node_id fmt (n : Cfg.Node.id) = F.fprintf fmt "%d" (n :> int)
end

2
infer/src/clang/cTrans.ml
Unescape View File

@ -1153,7 +1153,7 @@ struct
let var_typ = add_reference_if_glvalue typ expr_info in
let join_node = create_node (Cfg.Node.Join_node) [] [] sil_loc context in
Cfg.Node.set_succs_exn cfg join_node succ_nodes [];
let pvar = mk_temp_var (Cfg.Node.get_id join_node) in
let pvar = mk_temp_var (Cfg.Node.get_id join_node :> int) in
let continuation' = mk_cond_continuation trans_state.continuation in
let trans_state' = { trans_state with continuation = continuation'; succ_nodes = [] } in
let res_trans_cond = exec_with_priority_exception trans_state' cond cond_trans in

Write Preview
Loading…
Cancel
Save