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

[dot] move "dot" render of biabduction specs

Browse Source 
Summary:
This allows us to move the CFG rendering to IR/.

The parts of that file concerning CFGs and those concerning Biabduction
specs were entirely disjoint, it turns out, so that was easy.

Reviewed By: jberdine

Differential Revision: D18573924

fbshipit-source-id: 0a5ab6478
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent 8b959be727
commit 8289c7e7c7
10 changed files with 173 additions and 171 deletions
Show Stats Download Patch File Download Diff File

137
infer/src/IR/DotCfg.ml
Unescape View File

@ -0,0 +1,137 @@
(*
* Copyright (c) 2009-2013, Monoidics ltd.
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
module F = Format
let pp_cfgnodename pname fmt (n : Procdesc.Node.t) =
F.fprintf fmt "\"%s_%d\""
(Escape.escape_dotty (Typ.Procname.to_filename pname))
(Procdesc.Node.get_id n :> int)
let pp_etlist fmt etl =
List.iter etl ~f:(fun (id, typ) ->
Format.fprintf fmt " %a:%a" Mangled.pp id (Typ.pp_full Pp.text) typ )
let pp_var_list fmt etl =
List.iter etl ~f:(fun (id, ty) ->
Format.fprintf fmt " %a:%a" Mangled.pp id (Typ.pp_full Pp.text) ty )
let pp_local_list fmt etl = List.iter ~f:(Procdesc.pp_local fmt) etl
let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) =
let pp_label fmt n =
match Procdesc.Node.get_kind n with
| Start_node ->
let pname = Procdesc.Node.get_proc_name n in
let pname_string = Escape.escape_dotty (Typ.Procname.to_string pname) in
let attributes = Procdesc.get_attributes pdesc in
Format.fprintf fmt "Start %s\\nFormals: %a\\nLocals: %a" pname_string pp_etlist
(Procdesc.get_formals pdesc) pp_local_list (Procdesc.get_locals pdesc) ;
if not (List.is_empty (Procdesc.get_captured pdesc)) then
Format.fprintf fmt "\\nCaptured: %a" pp_var_list (Procdesc.get_captured pdesc) ;
let method_annotation = attributes.ProcAttributes.method_annotation in
if not (Annot.Method.is_empty method_annotation) then
Format.fprintf fmt "\\nAnnotation: %a" (Annot.Method.pp pname_string) method_annotation
| Exit_node ->
let pname = Procdesc.Node.get_proc_name n in
Format.fprintf fmt "Exit %s" (Escape.escape_dotty (Typ.Procname.to_string pname))
| Join_node ->
Format.pp_print_char fmt '+'
| Prune_node (is_true_branch, if_kind, _) ->
Format.fprintf fmt "Prune (%b branch, %s)" is_true_branch (Sil.if_kind_to_string if_kind)
| Stmt_node s ->
Format.fprintf fmt " %a" Procdesc.Node.pp_stmt s
| Skip_node s ->
Format.fprintf fmt "Skip %s" s
in
let instr_string i =
let pp f = Sil.pp_instr ~print_types:false Pp.text f i in
let str = F.asprintf "%t" pp in
Escape.escape_dotty str
in
let pp_instrs fmt instrs =
Instrs.iter ~f:(fun i -> F.fprintf fmt " %s\\n " (instr_string i)) instrs
in
let instrs = Procdesc.Node.get_instrs n in
F.fprintf fmt "%d: %a \\n %a" (Procdesc.Node.get_id n :> int) pp_label n pp_instrs instrs
let pp_cfgnodeshape fmt (n : Procdesc.Node.t) =
match Procdesc.Node.get_kind n with
| Start_node | Exit_node ->
F.pp_print_string fmt "color=yellow style=filled"
| Prune_node _ ->
F.fprintf fmt "shape=\"invhouse\""
| Skip_node _ ->
F.fprintf fmt "color=\"gray\""
| Stmt_node _ ->
F.fprintf fmt "shape=\"box\""
| _ ->
()
let pp_cfgnode pdesc fmt (n : Procdesc.Node.t) =
let pname = Procdesc.get_proc_name pdesc in
F.fprintf fmt "%a [label=\"%a\" %a]@\n\t@\n" (pp_cfgnodename pname) n (pp_cfgnodelabel pdesc) n
pp_cfgnodeshape n ;
let print_edge n1 n2 is_exn =
let color = if is_exn then "[color=\"red\" ]" else "" in
match Procdesc.Node.get_kind n2 with
| Exit_node when is_exn ->
(* don't print exception edges to the exit node *)
()
| _ ->
F.fprintf fmt "@\n\t %a -> %a %s;" (pp_cfgnodename pname) n1 (pp_cfgnodename pname) n2 color
in
List.iter ~f:(fun n' -> print_edge n n' false) (Procdesc.Node.get_succs n) ;
List.iter ~f:(fun n' -> print_edge n n' true) (Procdesc.Node.get_exn n)
(** Print the flowgraphs in [cfg]. Nodes are printed only if (a) their location is [source] or
(b) [Config.dotty_cfg_libs] is set. This triggers preanalysis. *)
let print_icfg source fmt cfg =
let print_node pdesc node =
let loc = Procdesc.Node.get_loc node in
if Config.dotty_cfg_libs || SourceFile.equal loc.Location.file source then
F.fprintf fmt "%a@\n" (pp_cfgnode pdesc) node
in
let print_pdesc pdesc =
Procdesc.get_nodes pdesc
|> List.sort ~compare:Procdesc.Node.compare
|> List.iter ~f:(fun node -> print_node pdesc node)
in
Cfg.iter_sorted cfg ~f:(fun pdesc -> print_pdesc pdesc)
let write_icfg_dotty_to_file source cfg fname =
let chan = Out_channel.create fname in
let fmt = Format.formatter_of_out_channel chan in
(* avoid phabricator thinking this file was generated by substituting substring with %s *)
F.fprintf fmt "@[/* %@%s */@\ndigraph cfg {@\n" "generated" ;
print_icfg source fmt cfg ;
F.fprintf fmt "}@]@." ;
Out_channel.close chan
let emit source cfg =
let fname =
match Config.icfg_dotty_outfile with
| Some file ->
file
| None when Config.frontend_tests ->
SourceFile.to_abs_path source ^ ".test.dot"
| None ->
DB.filename_to_string
(DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source)
[Config.dotty_output])
in
write_icfg_dotty_to_file source cfg fname

12
infer/src/IR/DotCfg.mli
Unescape View File

@ -0,0 +1,12 @@
(*
* Copyright (c) 2009-2013, Monoidics ltd.
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
val emit : SourceFile.t -> Cfg.t -> unit
(** emit the given {!Cfg.t} in the "dot" format to a file determined by {!Config} values *)

2
infer/src/backend/InferAnalyze.ml
Unescape View File

@ -25,7 +25,7 @@ let analyze_target : SchedulerTypes.target Tasks.doer =
L.task_progress SourceFile.pp source_file ~f:(fun () -> L.task_progress SourceFile.pp source_file ~f:(fun () ->
Ondemand.analyze_file exe_env source_file ; Ondemand.analyze_file exe_env source_file ;
if Topl.is_active () && Config.debug_mode then if Topl.is_active () && Config.debug_mode then
Dotty.print_icfg_dotty (Topl.sourcefile ()) (Topl.cfg ()) ; DotCfg.emit (Topl.sourcefile ()) (Topl.cfg ()) ;
if Config.write_html then Printer.write_all_html_files source_file ) if Config.write_html then Printer.write_all_html_files source_file )
in in
(* In call-graph scheduling, log progress every [per_procedure_logging_granularity] procedures. (* In call-graph scheduling, log progress every [per_procedure_logging_granularity] procedures.

21
infer/src/backend/dotty.mli
Unescape View File

@ -1,21 +0,0 @@
(*
* Copyright (c) 2009-2013, Monoidics ltd.
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
(** Pretty printing functions in dot format. *)
(** {2 Contol-Flow Graph} *)
val print_icfg_dotty : SourceFile.t -> Cfg.t -> unit
(** Print the cfg *)
(** {2 Specs} *)
val pp_speclist_dotty_file : DB.filename -> Prop.normal BiabductionSummary.spec list -> unit
(** Dotty printing for specs *)

150
infer/src/backend/dotty.ml → infer/src/biabduction/DotBiabduction.ml
Unescape View File

@ -10,8 +10,6 @@ open! IStd
module L = Logging module L = Logging
module F = Format module F = Format
(** {1 Dotty} *)
(* When false it prints only the retain cycle part of a prop. (* When false it prints only the retain cycle part of a prop.
When true it prints the full property (maybe useful for debug) *) When true it prints the full property (maybe useful for debug) *)
let print_full_prop = ref false let print_full_prop = ref false
@ -82,8 +80,7 @@ let fields_structs = ref []
let struct_exp_nodes = ref [] let struct_exp_nodes = ref []
(* general unique counter to assign a different number to boxex, *) (** general unique counter to assign a different number to boxes, clusters, subgraphs, etc. *)
(* clusters,subgraphs etc. *)
let dotty_state_count = ref 0 let dotty_state_count = ref 0
let spec_counter = ref 0 let spec_counter = ref 0
@ -1025,7 +1022,6 @@ and pp_dotty f kind (prop_ : Prop.normal Prop.t) cycle =
~f:(fun node -> if node_in_cycle cycle node then dotty_pp_state f pe cycle node) ~f:(fun node -> if node_in_cycle cycle node then dotty_pp_state f pe cycle node)
all_nodes ; all_nodes ;
List.iter ~f:(dotty_pp_link f) links ; List.iter ~f:(dotty_pp_link f) links ;
(* F.fprintf f "@\n } @\n"; *)
F.fprintf f "@\n } @\n" F.fprintf f "@\n } @\n"
@ -1054,142 +1050,6 @@ let pp_dotty_one_spec f pre posts =
F.fprintf f "@\n } @\n" F.fprintf f "@\n } @\n"
(********** START of Print interprocedural cfgs in dotty format *)
(********** Print control flow graph (in dot form) for fundec to channel. You have to compute an
interprocedural cfg first. *)
let pp_cfgnodename pname fmt (n : Procdesc.Node.t) =
F.fprintf fmt "\"%s_%d\""
(Escape.escape_dotty (Typ.Procname.to_filename pname))
(Procdesc.Node.get_id n :> int)
let pp_etlist fmt etl =
List.iter
~f:(fun (id, typ) -> Format.fprintf fmt " %a:%a" Mangled.pp id (Typ.pp_full Pp.text) typ)
etl
let pp_var_list fmt etl =
List.iter
~f:(fun (id, ty) -> Format.fprintf fmt " %a:%a" Mangled.pp id (Typ.pp_full Pp.text) ty)
etl
let pp_local_list fmt etl = List.iter ~f:(Procdesc.pp_local fmt) etl
let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) =
let pp_label fmt n =
match Procdesc.Node.get_kind n with
| Procdesc.Node.Start_node ->
let pname = Procdesc.Node.get_proc_name n in
let pname_string = Escape.escape_dotty (Typ.Procname.to_string pname) in
let attributes = Procdesc.get_attributes pdesc in
Format.fprintf fmt "Start %s\\nFormals: %a\\nLocals: %a" pname_string pp_etlist
(Procdesc.get_formals pdesc) pp_local_list (Procdesc.get_locals pdesc) ;
if not (List.is_empty (Procdesc.get_captured pdesc)) then
Format.fprintf fmt "\\nCaptured: %a" pp_var_list (Procdesc.get_captured pdesc) ;
let method_annotation = attributes.ProcAttributes.method_annotation in
if not (Annot.Method.is_empty method_annotation) then
Format.fprintf fmt "\\nAnnotation: %a" (Annot.Method.pp pname_string) method_annotation
| Procdesc.Node.Exit_node ->
let pname = Procdesc.Node.get_proc_name n in
Format.fprintf fmt "Exit %s" (Escape.escape_dotty (Typ.Procname.to_string pname))
| Procdesc.Node.Join_node ->
Format.pp_print_char fmt '+'
| Procdesc.Node.Prune_node (is_true_branch, if_kind, _) ->
Format.fprintf fmt "Prune (%b branch, %s)" is_true_branch (Sil.if_kind_to_string if_kind)
| Procdesc.Node.Stmt_node s ->
Format.fprintf fmt " %a" Procdesc.Node.pp_stmt s
| Procdesc.Node.Skip_node s ->
Format.fprintf fmt "Skip %s" s
in
let instr_string i =
let pp f = Sil.pp_instr ~print_types:false Pp.text f i in
let str = F.asprintf "%t" pp in
Escape.escape_dotty str
in
let pp_instrs fmt instrs =
Instrs.iter ~f:(fun i -> F.fprintf fmt " %s\\n " (instr_string i)) instrs
in
let instrs = Procdesc.Node.get_instrs n in
F.fprintf fmt "%d: %a \\n %a" (Procdesc.Node.get_id n :> int) pp_label n pp_instrs instrs
let pp_cfgnodeshape fmt (n : Procdesc.Node.t) =
match Procdesc.Node.get_kind n with
| Procdesc.Node.Start_node | Procdesc.Node.Exit_node ->
F.pp_print_string fmt "color=yellow style=filled"
| Procdesc.Node.Prune_node _ ->
F.fprintf fmt "shape=\"invhouse\""
| Procdesc.Node.Skip_node _ ->
F.fprintf fmt "color=\"gray\""
| Procdesc.Node.Stmt_node _ ->
F.fprintf fmt "shape=\"box\""
| _ ->
()
let pp_cfgnode pdesc fmt (n : Procdesc.Node.t) =
let pname = Procdesc.get_proc_name pdesc in
F.fprintf fmt "%a [label=\"%a\" %a]@\n\t@\n" (pp_cfgnodename pname) n (pp_cfgnodelabel pdesc) n
pp_cfgnodeshape n ;
let print_edge n1 n2 is_exn =
let color = if is_exn then "[color=\"red\" ]" else "" in
match Procdesc.Node.get_kind n2 with
| Procdesc.Node.Exit_node when is_exn ->
(* don't print exception edges to the exit node *)
()
| _ ->
F.fprintf fmt "@\n\t %a -> %a %s;" (pp_cfgnodename pname) n1 (pp_cfgnodename pname) n2 color
in
List.iter ~f:(fun n' -> print_edge n n' false) (Procdesc.Node.get_succs n) ;
List.iter ~f:(fun n' -> print_edge n n' true) (Procdesc.Node.get_exn n)
(** Print the flowgraphs in [cfg]. Nodes are printed only if (a) their location is [source] or
(b) [Config.dotty_cfg_libs] is set. This triggers preanalysis. *)
let print_icfg source fmt cfg =
let print_node pdesc node =
let loc = Procdesc.Node.get_loc node in
if Config.dotty_cfg_libs || SourceFile.equal loc.Location.file source then
F.fprintf fmt "%a@\n" (pp_cfgnode pdesc) node
in
let print_pdesc pdesc =
Procdesc.get_nodes pdesc
|> List.sort ~compare:Procdesc.Node.compare
|> List.iter ~f:(fun node -> print_node pdesc node)
in
Cfg.iter_sorted cfg ~f:(fun pdesc -> print_pdesc pdesc)
let write_icfg_dotty_to_file source cfg fname =
let chan = Out_channel.create fname in
let fmt = Format.formatter_of_out_channel chan in
(* avoid phabricator thinking this file was generated by substituting substring with %s *)
F.fprintf fmt "@[/* %@%s */@\ndigraph cfg {@\n" "generated" ;
print_icfg source fmt cfg ;
F.fprintf fmt "}@]@." ;
Out_channel.close chan
let print_icfg_dotty source cfg =
let fname =
match Config.icfg_dotty_outfile with
| Some file ->
file
| None when Config.frontend_tests ->
SourceFile.to_abs_path source ^ ".test.dot"
| None ->
DB.filename_to_string
(DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source)
[Config.dotty_output])
in
write_icfg_dotty_to_file source cfg fname
(********** END of Printing dotty files ***********)
(** Dotty printing for specs *) (** Dotty printing for specs *)
let pp_speclist_dotty f (splist : Prop.normal BiabductionSummary.spec list) = let pp_speclist_dotty f (splist : Prop.normal BiabductionSummary.spec list) =
reset_proposition_counter () ; reset_proposition_counter () ;
@ -1207,11 +1067,13 @@ let pp_speclist_dotty f (splist : Prop.normal BiabductionSummary.spec list) =
let pp_speclist_to_file (filename : DB.filename) spec_list = let pp_speclist_to_file (filename : DB.filename) spec_list =
let outc = Out_channel.create (DB.filename_to_string (DB.filename_add_suffix filename ".dot")) in let outc =
Out_channel.create (DB.filename_to_string (DB.filename_add_suffix filename ".biabd.dot"))
in
let fmt = F.formatter_of_out_channel outc in let fmt = F.formatter_of_out_channel outc in
let () = F.fprintf fmt "#### Dotty version: ####@\n%a@\n@\n" pp_speclist_dotty spec_list in let () = F.fprintf fmt "@[#### Dotty version: ####@\n%a@\n@\n@]@." pp_speclist_dotty spec_list in
Out_channel.close outc Out_channel.close outc
let pp_speclist_dotty_file (filename : DB.filename) spec_list = let emit_specs_to_file filename spec_list =
try pp_speclist_to_file filename spec_list with exn when SymOp.exn_not_failure exn -> () try pp_speclist_to_file filename spec_list with exn when SymOp.exn_not_failure exn -> ()

12
infer/src/biabduction/DotBiabduction.mli
Unescape View File

@ -0,0 +1,12 @@
(*
* Copyright (c) 2009-2013, Monoidics ltd.
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
val emit_specs_to_file : DB.filename -> Prop.normal BiabductionSummary.spec list -> unit
(** emit specs in the "dot" format to the specified file *)

2
infer/src/biabduction/interproc.ml
Unescape View File

@ -899,7 +899,7 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf
DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source) DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source)
[Typ.Procname.to_filename pname] [Typ.Procname.to_filename pname]
in in
if Config.write_dotty then Dotty.pp_speclist_dotty_file filename specs ; if Config.write_dotty then DotBiabduction.emit_specs_to_file filename specs ;
(specs, BiabductionSummary.RE_EXECUTION) (specs, BiabductionSummary.RE_EXECUTION)
in in
(go, get_results) (go, get_results)

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

@ -61,7 +61,7 @@ let do_source_file (translation_unit_context : CFrontend_config.translation_unit
if if
Config.debug_mode || Config.testing_mode || Config.frontend_tests Config.debug_mode || Config.testing_mode || Config.frontend_tests
|| Option.is_some Config.icfg_dotty_outfile || Option.is_some Config.icfg_dotty_outfile
then Dotty.print_icfg_dotty source_file cfg ; then DotCfg.emit source_file cfg ;
L.(debug Capture Verbose) "Stored on disk:@[<v>%a@]@." Cfg.pp_proc_signatures cfg ; L.(debug Capture Verbose) "Stored on disk:@[<v>%a@]@." Cfg.pp_proc_signatures cfg ;
let procedures_translated_summary = let procedures_translated_summary =
EventLogger.ProceduresTranslatedSummary EventLogger.ProceduresTranslatedSummary

4
infer/src/infer.ml
Unescape View File

@ -189,8 +189,8 @@ let () =
List.iter proc_names ~f:(fun proc_name -> List.iter proc_names ~f:(fun proc_name ->
Procdesc.load proc_name Procdesc.load proc_name
|> Option.iter ~f:(fun cfg -> Typ.Procname.Hash.add cfgs proc_name cfg) ) ; |> Option.iter ~f:(fun cfg -> Typ.Procname.Hash.add cfgs proc_name cfg) ) ;
(* emit the dotty file in captured/... *) (* emit the dot file in captured/... *)
Dotty.print_icfg_dotty source_file cfgs ) ; DotCfg.emit source_file cfgs ) ;
L.result "CFGs written in %s/*/%s@." Config.captured_dir Config.dotty_output ) L.result "CFGs written in %s/*/%s@." Config.captured_dir Config.dotty_output )
| false, false -> | false, false ->
let if_some key opt args = let if_some key opt args =

2
infer/src/java/jMain.ml
Unescape View File

@ -22,7 +22,7 @@ let init_global_state source_file =
let store_icfg tenv source_file cfg = let store_icfg tenv source_file cfg =
Typ.Procname.Hash.iter (fun _ pdesc -> Preanal.do_preanalysis pdesc tenv) cfg ; Typ.Procname.Hash.iter (fun _ pdesc -> Preanal.do_preanalysis pdesc tenv) cfg ;
SourceFiles.add source_file cfg Tenv.Global None ; SourceFiles.add source_file cfg Tenv.Global None ;
if Config.debug_mode || Config.frontend_tests then Dotty.print_icfg_dotty source_file cfg ; if Config.debug_mode || Config.frontend_tests then DotCfg.emit source_file cfg ;
() ()

Write Preview
Loading…
Cancel
Save