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

Fix assert false in Paths.

Browse Source 
Reviewed By: akotulski

Differential Revision: D2585594

fb-gh-sync-id: a4ec077
master
Cristiano Calcagno 9 years ago committed by facebook-github-bot-1
parent 6a922ff597
commit 56ccb6b198
5 changed files with 126 additions and 89 deletions
Show Stats Download Patch File Download Diff File

11
infer/src/backend/buckets.ml
Unescape View File

@ -35,11 +35,12 @@ let check_nested_loop path pos_opt =
incr trace_length; incr trace_length;
(* L.d_strln ("level " ^ string_of_int level ^ " (Cfg.Node.get_id node) " ^ string_of_int nid); *) (* L.d_strln ("level " ^ string_of_int level ^ " (Cfg.Node.get_id node) " ^ string_of_int nid); *)
() in () in
let f level p session exn_opt = let f level p session exn_opt = match Paths.Path.curr_node p with
let node = Paths.Path.curr_node p in | Some node ->
do_any_node level node; do_any_node level node;
if level = 0 then do_node_caller node; if level = 0 then do_node_caller node
() in | None ->
() in
Paths.Path.iter_longest_sequence f pos_opt path; Paths.Path.iter_longest_sequence f pos_opt path;
in_nested_loop () in_nested_loop ()

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

@ -138,22 +138,26 @@ let path_set_checkout_todo (node: Cfg.node) : Paths.PathSet.t =
(* =============== START: Print a complete path in a dotty file =============== *) (* =============== START: Print a complete path in a dotty file =============== *)
let pp_path_dotty f path = let pp_path_dotty f path =
let get_node_id_from_path p =
let node = Paths.Path.curr_node p in
Cfg.Node.get_id node in
let count = ref 0 in let count = ref 0 in
let prev_n_id = ref 0 in let prev_n_id = ref 0 in
let curr_n_id = ref 0 in let curr_n_id = ref 0 in
prev_n_id:=- 1; prev_n_id:=- 1;
let g level p session exn_opt = let get_node_id_from_path p = match Paths.Path.curr_node p with
let curr_node = Paths.Path.curr_node p in | Some node ->
let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in Cfg.Node.get_id node
let plist = Paths.PathSet.filter_path p curr_path_set in | None ->
incr count; !curr_n_id in
curr_n_id:= (get_node_id_from_path p); let g level p session exn_opt = match Paths.Path.curr_node p with
Dotty.pp_dotty_prop_list_in_path f plist !prev_n_id !curr_n_id; | Some curr_node ->
L.out "@.Path #%d: %a@." !count Paths.Path.pp p; let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in
prev_n_id:=!curr_n_id in let plist = Paths.PathSet.filter_path p curr_path_set in
incr count;
curr_n_id := get_node_id_from_path p;
Dotty.pp_dotty_prop_list_in_path f plist !prev_n_id !curr_n_id;
L.out "@.Path #%d: %a@." !count Paths.Path.pp p;
prev_n_id:=!curr_n_id
| None ->
() in
L.out "@.@.Printing Path: %a to file error_path.dot@." Paths.Path.pp path; L.out "@.@.Printing Path: %a to file error_path.dot@." Paths.Path.pp path;
Dotty.reset_proposition_counter (); Dotty.reset_proposition_counter ();
Dotty.reset_dotty_spec_counter (); Dotty.reset_dotty_spec_counter ();
@ -335,18 +339,20 @@ let reset_prop_metrics () =
let d_path (path, pos_opt) = let d_path (path, pos_opt) =
let step = ref 0 in let step = ref 0 in
let prop_last_step = ref Prop.prop_emp in (* if the last step had a singleton prop, store it here *) let prop_last_step = ref Prop.prop_emp in (* if the last step had a singleton prop, store it here *)
let f level p session exn_opt = let f level p session exn_opt = match Paths.Path.curr_node p with
let curr_node = Paths.Path.curr_node p in | Some curr_node ->
let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in
let plist = Paths.PathSet.filter_path p curr_path_set in let plist = Paths.PathSet.filter_path p curr_path_set in
incr step; incr step;
(* Propset.pp_proplist_dotty_file ("path" ^ (string_of_int !count) ^ ".dot") plist; *) (* Propset.pp_proplist_dotty_file ("path" ^ (string_of_int !count) ^ ".dot") plist; *)
L.d_strln ("Path Step #" ^ string_of_int !step ^ L.d_strln ("Path Step #" ^ string_of_int !step ^
" node " ^ string_of_int (Cfg.Node.get_id curr_node) ^ " node " ^ string_of_int (Cfg.Node.get_id curr_node) ^
" session " ^ string_of_int session ^ ":"); " session " ^ string_of_int session ^ ":");
Propset.d !prop_last_step (Propset.from_proplist plist); L.d_ln (); Propset.d !prop_last_step (Propset.from_proplist plist); L.d_ln ();
Cfg.Node.d_instrs true None curr_node; L.d_ln (); L.d_ln (); Cfg.Node.d_instrs true None curr_node; L.d_ln (); L.d_ln ();
prop_last_step := (match plist with | [prop] -> prop | _ -> Prop.prop_emp) in prop_last_step := (match plist with | [prop] -> prop | _ -> Prop.prop_emp)
| None ->
() in
L.d_str "Path: "; Paths.Path.d_stats path; L.d_ln (); L.d_str "Path: "; Paths.Path.d_stats path; L.d_ln ();
Paths.Path.d path; L.d_ln (); Paths.Path.d path; L.d_ln ();
(* pp_complete_path_dotty_file path; *) (* pp_complete_path_dotty_file path; *)

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

@ -35,7 +35,7 @@ module Path : sig
val create_loc_trace : t -> Sil.path_pos option -> Errlog.loc_trace val create_loc_trace : t -> Sil.path_pos option -> Errlog.loc_trace
(** return the current node of the path *) (** return the current node of the path *)
val curr_node : t -> Cfg.node val curr_node : t -> Cfg.node option
(** dump a path *) (** dump a path *)
val d : t -> unit val d : t -> unit
@ -115,10 +115,11 @@ end = struct
stats.linear_num <- - 1.0 stats.linear_num <- - 1.0
let rec curr_node = function let rec curr_node = function
| Pstart (node, _) -> node | Pstart (node, _) -> Some node
| Pnode (node, _, _, _, _, _) -> node | Pnode (node, _, _, _, _, _) -> Some node
| Pcall(p1, _, _, _) -> curr_node p1 | Pcall(p1, _, _, _) -> curr_node p1
| Pjoin _ -> assert false | Pjoin _ ->
None
let exname_opt_compare eo1 eo2 = match eo1, eo2 with let exname_opt_compare eo1 eo2 = match eo1, eo2 with
| None, None -> 0 | None, None -> 0
@ -306,8 +307,10 @@ end = struct
| Some pos -> Sil.path_pos_equal (get_path_pos node) pos in | Some pos -> Sil.path_pos_equal (get_path_pos node) pos in
let path_pos_at_path p = let path_pos_at_path p =
try try
let node = curr_node p in match curr_node p with
pos_opt <> None && filter node | Some node ->
pos_opt <> None && filter node
| None -> false
with exn when exn_not_timeout exn -> false in with exn when exn_not_timeout exn -> false in
let position_seen = ref false in let position_seen = ref false in
let inverse_sequence = let inverse_sequence =
@ -333,12 +336,17 @@ end = struct
(** return the node visited most, and number of visits, in the longest linear sequence *) (** return the node visited most, and number of visits, in the longest linear sequence *)
let repetitions path = let repetitions path =
let map = ref NodeMap.empty in let map = ref NodeMap.empty in
let add_node node = let add_node = function
try | Some node ->
let n = NodeMap.find node !map in begin
map := NodeMap.add node (n + 1) !map try
with Not_found -> let n = NodeMap.find node !map in
map := NodeMap.add node 1 !map in map := NodeMap.add node (n + 1) !map
with Not_found ->
map := NodeMap.add node 1 !map
end
| None ->
() in
iter_longest_sequence (fun level p s exn_opt -> add_node (curr_node p)) None path; iter_longest_sequence (fun level p s exn_opt -> add_node (curr_node p)) None path;
let max_rep_node = ref (Cfg.Node.dummy ()) in let max_rep_node = ref (Cfg.Node.dummy ()) in
let max_rep_num = ref 0 in let max_rep_num = ref 0 in
@ -423,51 +431,69 @@ end = struct
Errlog.lt_description = descr; Errlog.lt_description = descr;
Errlog.lt_node_tags = node_tags } in Errlog.lt_node_tags = node_tags } in
let g level path session exn_opt = let g level path session exn_opt =
let curr_node = curr_node path in match curr_node path with
let curr_loc = Cfg.Node.get_loc curr_node in | Some curr_node ->
match Cfg.Node.get_kind curr_node with begin
| Cfg.Node.Join_node -> () (* omit join nodes from error traces *) let curr_loc = Cfg.Node.get_loc curr_node in
| Cfg.Node.Start_node pdesc -> match Cfg.Node.get_kind curr_node with
let pname = Cfg.Procdesc.get_proc_name pdesc in | Cfg.Node.Join_node -> () (* omit join nodes from error traces *)
let name = Procname.to_string pname in | Cfg.Node.Start_node pdesc ->
let name_id = Procname.to_filename pname in let pname = Cfg.Procdesc.get_proc_name pdesc in
let descr = "start of procedure " ^ (Procname.to_simplified_string pname) in let name = Procname.to_string pname in
let node_tags = [(Io_infer.Xml.tag_kind,"procedure_start"); (Io_infer.Xml.tag_name, name); (Io_infer.Xml.tag_name_id, name_id)] in let name_id = Procname.to_filename pname in
trace := mk_trace_elem level curr_loc descr node_tags :: !trace let descr = "start of procedure " ^ (Procname.to_simplified_string pname) in
| Cfg.Node.Prune_node (is_true_branch, if_kind, _) -> let node_tags =
let descr = match is_true_branch, if_kind with [(Io_infer.Xml.tag_kind,"procedure_start");
| true, Sil.Ik_if -> "Taking true branch" (Io_infer.Xml.tag_name, name);
| false, Sil.Ik_if -> "Taking false branch" (Io_infer.Xml.tag_name_id, name_id)] in
| true, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) -> "Loop condition is true. Entering loop body" trace := mk_trace_elem level curr_loc descr node_tags :: !trace
| false, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) -> "Loop condition is false. Leaving loop" | Cfg.Node.Prune_node (is_true_branch, if_kind, _) ->
| true, Sil.Ik_switch -> "Switch condition is true. Entering switch case" let descr = match is_true_branch, if_kind with
| false, Sil.Ik_switch -> "Switch condition is false. Skipping switch case" | true, Sil.Ik_if -> "Taking true branch"
| true, (Sil.Ik_bexp | Sil.Ik_land_lor) -> "Condition is true" | false, Sil.Ik_if -> "Taking false branch"
| false, (Sil.Ik_bexp | Sil.Ik_land_lor) -> "Condition is false" in | true, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) ->
let node_tags = [(Io_infer.Xml.tag_kind,"condition"); (Io_infer.Xml.tag_branch, if is_true_branch then "true" else "false")] in "Loop condition is true. Entering loop body"
trace := mk_trace_elem level curr_loc descr node_tags :: !trace | false, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) ->
| Cfg.Node.Exit_node pdesc -> "Loop condition is false. Leaving loop"
let pname = Cfg.Procdesc.get_proc_name pdesc in | true, Sil.Ik_switch -> "Switch condition is true. Entering switch case"
let descr = "return from a call to " ^ (Procname.to_string pname) in | false, Sil.Ik_switch -> "Switch condition is false. Skipping switch case"
let name = Procname.to_string pname in | true, (Sil.Ik_bexp | Sil.Ik_land_lor) -> "Condition is true"
let name_id = Procname.to_filename pname in | false, (Sil.Ik_bexp | Sil.Ik_land_lor) -> "Condition is false" in
let node_tags = [(Io_infer.Xml.tag_kind,"procedure_end"); (Io_infer.Xml.tag_name, name); (Io_infer.Xml.tag_name_id, name_id)] in let node_tags =
trace := mk_trace_elem level curr_loc descr node_tags :: !trace [(Io_infer.Xml.tag_kind,"condition");
| _ -> (Io_infer.Xml.tag_branch, if is_true_branch then "true" else "false")] in
let descr, node_tags = trace := mk_trace_elem level curr_loc descr node_tags :: !trace
match exn_opt with | Cfg.Node.Exit_node pdesc ->
| None -> "", [] let pname = Cfg.Procdesc.get_proc_name pdesc in
| Some exn_name -> let descr = "return from a call to " ^ (Procname.to_string pname) in
let exn_str = Mangled.to_string exn_name in let name = Procname.to_string pname in
if exn_str = "" let name_id = Procname.to_filename pname in
then "exception", [(Io_infer.Xml.tag_kind,"exception")] let node_tags =
else "exception " ^ exn_str, [(Io_infer.Xml.tag_kind,"exception"); (Io_infer.Xml.tag_name, exn_str)] in [(Io_infer.Xml.tag_kind,"procedure_end");
let descr = (Io_infer.Xml.tag_name, name);
match get_description path with (Io_infer.Xml.tag_name_id, name_id)] in
| Some path_descr -> trace := mk_trace_elem level curr_loc descr node_tags :: !trace
if String.length descr > 0 then descr^" "^path_descr else path_descr | _ ->
| None -> descr in let descr, node_tags =
trace := mk_trace_elem level curr_loc descr node_tags :: !trace in match exn_opt with
| None -> "", []
| Some exn_name ->
let exn_str = Mangled.to_string exn_name in
if exn_str = ""
then "exception", [(Io_infer.Xml.tag_kind,"exception")]
else
"exception " ^ exn_str,
[(Io_infer.Xml.tag_kind,"exception");
(Io_infer.Xml.tag_name, exn_str)] in
let descr =
match get_description path with
| Some path_descr ->
if String.length descr > 0 then descr^" "^path_descr else path_descr
| None -> descr in
trace := mk_trace_elem level curr_loc descr node_tags :: !trace
end
| None ->
() in
iter_longest_sequence g pos_opt path; iter_longest_sequence g pos_opt path;
let compare lt1 lt2 = let compare lt1 lt2 =
let n = int_compare lt1.Errlog.lt_level lt2.Errlog.lt_level in let n = int_compare lt1.Errlog.lt_level lt2.Errlog.lt_level in

2
infer/src/backend/paths.mli
Unescape View File

@ -31,7 +31,7 @@ module Path : sig
val create_loc_trace : t -> Sil.path_pos option -> Errlog.loc_trace val create_loc_trace : t -> Sil.path_pos option -> Errlog.loc_trace
(** return the current node of the path *) (** return the current node of the path *)
val curr_node : t -> Cfg.node val curr_node : t -> Cfg.node option
(** dump a path *) (** dump a path *)
val d : t -> unit val d : t -> unit

8
infer/src/backend/symExec.ml
Unescape View File

@ -826,8 +826,12 @@ let normalize_params pdesc prop actual_params =
let prop, args = IList.fold_left norm_arg (prop, []) actual_params in let prop, args = IList.fold_left norm_arg (prop, []) actual_params in
(prop, IList.rev args) (prop, IList.rev args)
let do_error_checks node instr pname pdesc = let do_error_checks node_opt instr pname pdesc = match node_opt with
if !Config.curr_language = Config.Java then PrintfArgs.check_printf_args_ok node instr pname pdesc | Some node ->
if !Config.curr_language = Config.Java then
PrintfArgs.check_printf_args_ok node instr pname pdesc
| None ->
()
(** Execute [instr] with a symbolic heap [prop].*) (** Execute [instr] with a symbolic heap [prop].*)
let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path

Write Preview
Loading…
Cancel
Save