From c0a66dbd49073ff9d19b35eda69427328dd7976d Mon Sep 17 00:00:00 2001 From: Martino Luca Date: Thu, 13 Oct 2016 09:48:20 -0700 Subject: [PATCH] [Infer][CTL] First implementation of a debugging feature for AST checks Summary: During the development/debugging of AST checks, it will be possible to emit dotty graphs with a representation of the evaluation of formulas. The formulas, expressed using the notation of CTL (https://en.wikipedia.org/wiki/Computation_tree_logic) are represented in a graph alongside the current ast-node and their final evaluation result (green for true, red for false) To get the dotty graph, run infer with the `--debug` flag Reviewed By: ddino Differential Revision: D3937787 fbshipit-source-id: 163e17d --- infer/src/base/Config.ml | 2 + infer/src/base/Config.mli | 1 + infer/src/base/Utils.ml | 3 +- infer/src/base/Utils.mli | 2 + infer/src/clang/cFrontend_checkers_main.ml | 5 +- infer/src/clang/cTL.ml | 285 ++++++++++++++++----- infer/src/clang/cTL.mli | 2 + infer/src/clang/predicates.ml | 3 + infer/src/clang/predicates.mli | 2 + 9 files changed, 234 insertions(+), 71 deletions(-) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 18c51bd75..c92769242 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -143,6 +143,8 @@ let inferconfig_file = ".inferconfig" let ivar_attributes = "ivar_attributes" +let lint_dotty_dir_name = "lint_dotty" + let lint_issues_dir_name = "lint_issues" (** letters used in the analysis output *) diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index c445af4e1..2e88206f6 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -85,6 +85,7 @@ val infer_py_argparse_error_exit_code : int val initial_analysis_time : float val ivar_attributes : string val lib_dir : string +val lint_dotty_dir_name : string val lint_issues_dir_name : string val load_average : float val log_analysis_crash : string diff --git a/infer/src/base/Utils.ml b/infer/src/base/Utils.ml index 365db7a5b..d523db6e4 100644 --- a/infer/src/base/Utils.ml +++ b/infer/src/base/Utils.ml @@ -601,11 +601,10 @@ let with_file file ~f = let oc = open_out file in let f () = f oc in let g () = close_out oc in - do_finally f g + do_finally f g |> fst let write_json_to_file destfile json = with_file destfile ~f:(fun oc -> Yojson.Basic.pretty_to_channel oc json) - |> fst let consume_in chan_in = try diff --git a/infer/src/base/Utils.mli b/infer/src/base/Utils.mli index bc10fb7b5..a12ce03ff 100644 --- a/infer/src/base/Utils.mli +++ b/infer/src/base/Utils.mli @@ -280,6 +280,8 @@ val directory_iter : (string -> unit) -> string -> unit val read_optional_json_file : string -> (Yojson.Basic.json, string) result +val with_file : string -> f:(out_channel -> 'a) -> 'a + val write_json_to_file : string -> Yojson.Basic.json -> unit val consume_in : in_channel -> unit diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index 0ca1151c1..4062f9d8f 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/infer/src/clang/cFrontend_checkers_main.ml @@ -126,8 +126,9 @@ let do_frontend_checks trans_unit_ctx ast = IList.iter (do_frontend_checks_decl context) allowed_decls; if (LintIssues.exists_issues ()) then store_issues source_file; - Logging.out "End linting file %s@\n" (DB.source_file_to_string source_file) - | _ -> assert false (* NOTE: Assumes that an AST always starts with a TranslationUnitDecl *) + Logging.out "End linting file %s@\n" (DB.source_file_to_string source_file); + CTL.save_dotty_when_in_debug_mode trans_unit_ctx.CFrontend_config.source_file; + | _ -> assert false (* NOTE: Assumes that an AST alsways starts with a TranslationUnitDecl *) with | Assert_failure (file, line, column) as exn -> Logging.err "Fatal error: exception Assert_failure(%s, %d, %d)@\n%!" file line column; diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 3069869fb..4b64928ed 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -50,6 +50,188 @@ type ast_node = | Stmt of Clang_ast_t.stmt | Decl of Clang_ast_t.decl +module Debug = struct + let pp_transition_decl_to_stmt fmt trans_opt = + let pp_aux fmt trans = match trans with + | Body -> Format.pp_print_string fmt "Body" + | InitExpr -> Format.pp_print_string fmt "InitExpr" in + match trans_opt with + | Some trans -> pp_aux fmt trans + | None -> Format.pp_print_string fmt "None" + + let rec pp_formula fmt phi = + match phi with + | True -> Format.fprintf fmt "True" + | False -> Format.fprintf fmt "False" + | Atomic p -> Predicates.pp_predicate fmt p + | Not phi -> Format.fprintf fmt "NOT(%a)" pp_formula phi + | And (phi1, phi2) -> Format.fprintf fmt "(%a AND %a)" pp_formula phi1 pp_formula phi2 + | Or (phi1, phi2) -> Format.fprintf fmt "(%a OR %a)" pp_formula phi1 pp_formula phi2 + | Implies (phi1, phi2) -> Format.fprintf fmt "(%a ==> %a)" pp_formula phi1 pp_formula phi2 + | AX phi -> Format.fprintf fmt "AX(%a)" pp_formula phi + | EX phi -> Format.fprintf fmt "EX(%a)" pp_formula phi + | AF phi -> Format.fprintf fmt "AF(%a)" pp_formula phi + | EF phi -> Format.fprintf fmt "EF(%a)" pp_formula phi + | AG phi -> Format.fprintf fmt "AG(%a)" pp_formula phi + | EG phi -> Format.fprintf fmt "EG(%a)" pp_formula phi + | AU (phi1, phi2) -> Format.fprintf fmt "A[%a UNTIL %a]" pp_formula phi1 pp_formula phi2 + | EU (phi1, phi2) -> Format.fprintf fmt "E[%a UNTIL %a]" pp_formula phi1 pp_formula phi2 + | EH (arglist, phi) -> Format.fprintf fmt "EH[%a](%a)" + (Utils.pp_comma_seq Format.pp_print_string) arglist + pp_formula phi + | ET (arglist, trans, phi) -> Format.fprintf fmt "ET[%a][%a](%a)" + (Utils.pp_comma_seq Format.pp_print_string) arglist + pp_transition_decl_to_stmt trans + pp_formula phi + + module EvaluationTracker = struct + exception Empty_stack of string + + type eval_result = Eval_undefined | Eval_true | Eval_false + + type content = { + ast_node: ast_node; + phi: t; + eval_result: eval_result; + } + + type node = { + id: int; + content: content; + } + + type tree = Tree of node * (tree list) + + type t = { + next_id: int; + eval_stack: tree Stack.t; + forest: tree list; + } + + let create_content ast_node phi = {ast_node; phi; eval_result = Eval_undefined} + + let create () = {next_id = 0; eval_stack = Stack.create(); forest = []} + + let eval_begin t content = + let node = {id = t.next_id; content} in + let create_subtree root = Tree (root, []) in + let subtree' = create_subtree node in + Stack.push subtree' t.eval_stack; + {t with next_id = t.next_id + 1} + + let eval_end t result = + let eval_result_of_bool = function + | true -> Eval_true + | false -> Eval_false in + if Stack.is_empty t.eval_stack then + raise (Empty_stack "Unbalanced number of eval_begin/eval_end invocations"); + let evaluated_tree = match Stack.pop t.eval_stack with + | Tree ({id = _; content} as node, children) -> + let content' = {content with eval_result = eval_result_of_bool result} in + Tree ({node with content = content'}, children) in + let forest' = + if Stack.is_empty t.eval_stack then evaluated_tree :: t.forest + else + let parent = match Stack.pop t.eval_stack with + Tree (node, children) -> Tree (node, evaluated_tree :: children) in + Stack.push parent t.eval_stack; + t.forest in + {t with forest = forest'} + + module DottyPrinter = struct + let dotty_of_ctl_evaluation t = + let buffer_content buf = + let result = Buffer.contents buf in + Buffer.reset buf; + result in + let dotty_of_tree cluster_id tree = + let get_root tree = match tree with Tree (root, _) -> root in + let get_children tree = match tree with Tree (_, children) -> IList.rev children in + (* shallow: emit dotty about root node and edges to its children *) + let shallow_dotty_of_tree tree = + let root_node = get_root tree in + let children = get_children tree in + let edge child_node = + if root_node.content.ast_node = child_node.content.ast_node then + Printf.sprintf "%d -> %d [style=dotted]" root_node.id child_node.id + else + Printf.sprintf "%d -> %d [style=bold]" root_node.id child_node.id in + let color = + match root_node.content.eval_result with + | Eval_true -> "green" + | Eval_false -> "red" + | _ -> failwith "Tree is not fully evaluated" in + let label = + let string_of_ast_node an = + match an with + | Stmt stmt -> Clang_ast_proj.get_stmt_kind_string stmt + | Decl decl -> Clang_ast_proj.get_decl_kind_string decl in + let smart_string_of_formula phi = + let num_children = IList.length children in + match phi with + | And _ when num_children = 2 -> "(...) AND (...)" + | Or _ when num_children = 2 -> "(...) OR (...)" + | Implies _ when num_children = 2 -> "(...) ==> (...)" + | Not _ -> "NOT(...)" + | _ -> Utils.pp_to_string pp_formula phi in + Format.sprintf "(%d)\\n%s\\n%s" + root_node.id + (Escape.escape_dotty (string_of_ast_node root_node.content.ast_node)) + (Escape.escape_dotty (smart_string_of_formula root_node.content.phi)) in + let edges = + let buf = Buffer.create 16 in + IList.iter + (fun subtree -> Buffer.add_string buf ((edge (get_root subtree)) ^ "\n")) + children; + buffer_content buf in + Printf.sprintf "%d [label=\"%s\" shape=box color=%s]\n%s\n" + root_node.id label color edges in + let rec traverse buf tree = + Buffer.add_string buf (shallow_dotty_of_tree tree); + IList.iter (traverse buf) (get_children tree) in + let buf = Buffer.create 16 in + traverse buf tree; + Printf.sprintf "subgraph cluster_%d {\n%s\n}" cluster_id (buffer_content buf) in + let buf = Buffer.create 16 in + IList.iteri + (fun cluster_id tree -> Buffer.add_string buf ((dotty_of_tree cluster_id tree) ^ "\n")) + (IList.rev t.forest); + Printf.sprintf "digraph CTL_Evaluation {\n%s\n}\n" (buffer_content buf) + end + end +end + +let ctl_evaluation_tracker = match Config.debug_mode with + | true -> Some (ref (Debug.EvaluationTracker.create ())) + | false -> None + +let debug_create_payload ast_node phi = + match ctl_evaluation_tracker with + | Some _ -> Some (Debug.EvaluationTracker.create_content ast_node phi) + | None -> None + +let debug_eval_begin payload = + match ctl_evaluation_tracker, payload with + | Some tracker, Some payload -> + tracker := Debug.EvaluationTracker.eval_begin !tracker payload + | _ -> () + +let debug_eval_end result = + match ctl_evaluation_tracker with + | Some tracker -> + tracker := Debug.EvaluationTracker.eval_end !tracker result + | None -> () + +let save_dotty_when_in_debug_mode source_file = + match ctl_evaluation_tracker with + | Some tracker -> + let dotty_dir = Config.results_dir // Config.lint_dotty_dir_name in + create_dir dotty_dir; + let source_file_basename = Filename.basename (DB.source_file_to_string source_file) in + let file = dotty_dir // (source_file_basename ^ ".dot") in + let dotty = Debug.EvaluationTracker.DottyPrinter.dotty_of_ctl_evaluation !tracker in + with_file file ~f:(fun oc -> output_string oc dotty) + | _ -> () (* Helper functions *) @@ -130,11 +312,10 @@ let eval_Atomic pred_name params an lcxt = such that (st', lcxt) satifies EF phi *) let rec eval_EF_st phi st lcxt = - Logging.out "\n->>>> Evaluating EF in %s\n" - (Clang_ast_proj.get_stmt_kind_string st); let _, succs = Clang_ast_proj.get_stmt_tuple st in - (eval_formula phi (Stmt st) lcxt) || - IList.exists (fun s -> eval_EF phi (Stmt s) lcxt) succs + eval_formula phi (Stmt st) lcxt + || IList.exists (fun s -> eval_EF phi (Stmt s) lcxt) succs + (* dec, lcxt |= EF phi <=> dec, lcxt |= phi or exists dec' in Successors(dec): dec', lcxt |= EF phi @@ -142,9 +323,7 @@ let rec eval_EF_st phi st lcxt = This is as eval_EF_st but for decl. *) and eval_EF_decl phi dec lcxt = - Logging.out "\n->>>> Evaluating EF in %s\n" - (Clang_ast_proj.get_decl_kind_string dec); - (eval_formula phi (Decl dec) lcxt) || + eval_formula phi (Decl dec) lcxt || (match Clang_ast_proj.get_decl_context_tuple dec with | Some (decl_list, _) -> IList.exists (fun d -> eval_EF phi (Decl d) lcxt) decl_list @@ -163,8 +342,6 @@ and eval_EF phi an lcxt = such that (st', lcxt) satifies phi *) and eval_EX_st phi st lcxt = - Logging.out "\n->>>> Evaluating EX in %s\n" - (Clang_ast_proj.get_stmt_kind_string st); let _, succs = Clang_ast_proj.get_stmt_tuple st in IList.exists (fun s -> eval_formula phi (Stmt s) lcxt) succs @@ -173,8 +350,6 @@ and eval_EX_st phi st lcxt = Same as eval_EX_st but for decl. *) and eval_EX_decl phi dec lcxt = - Logging.out "\n->>>> Evaluating EF in %s\n" - (Clang_ast_proj.get_decl_kind_string dec); match Clang_ast_proj.get_decl_context_tuple dec with | Some (decl_list, _) -> IList.exists (fun d -> eval_formula phi (Decl d) lcxt) decl_list @@ -218,14 +393,11 @@ and eval_EH classes phi an lcxt = | Some idi -> (match Ast_utils.get_super_ObjCImplementationDecl idi with | Some (Clang_ast_t.ObjCImplementationDecl(_, _, _, _, idi') as d) -> - eval_formula phi (Decl d) lcxt - || (eval_super (Some idi')) + eval_formula phi (Decl d) lcxt || eval_super (Some idi') | _ -> false) | None -> false in match an with | Decl d when node_has_type classes (Decl d) -> - Logging.out "\n->>>> Evaluating EH in %s\n" - (Clang_ast_proj.get_decl_kind_string d); eval_super (Ast_utils.get_impl_decl_info d) | _ -> false @@ -251,71 +423,50 @@ and eval_ET tl trs phi an lcxt = let _, stmt_list = Clang_ast_proj.get_stmt_tuple st in IList.exists (fun s -> eval phi (Stmt s) lcxt) stmt_list in let do_decl d = - Logging.out "\n->>>> Evaluating ET in %s\n" - (Clang_ast_proj.get_decl_kind_string d); match trs, node_has_type tl (Decl d) with | Some _, true -> - Logging.out "\n ->>>> Declaration is in types and has label"; (match transition_from_decl_to_stmt d trs with - | None -> - Logging.out "\n ->>>> NO transition returned"; - false - | Some st -> - Logging.out "\n ->>>> A transition is returned \n"; - eval_formula phi (Stmt st) lcxt) - | None, true -> - Logging.out "\n ->>>> Declaration has NO transition label\n"; - eval_formula phi (Decl d) lcxt - | _, false -> - Logging.out "\n ->>>> Declaration is NOT in types and _ label\n"; - evaluate_on_subdeclarations d (eval_ET tl trs) in + | None -> false + | Some st -> eval_formula phi (Stmt st) lcxt) + | None, true -> eval_formula phi (Decl d) lcxt + | _, false -> evaluate_on_subdeclarations d (eval_ET tl trs) in let do_stmt st = - Logging.out "\n->>>> Evaluating ET in %s\n" - (Clang_ast_proj.get_stmt_kind_string st); match trs, node_has_type tl (Stmt st) with | Some _, true -> - Logging.out "\n ->>>> Statement is in types and has label"; (match transition_from_stmt_to_decl st trs with - | None -> - Logging.out "\n ->>>> NO transition returned\n"; - false - | Some d -> - Logging.out "\n ->>>> A transition is returned \n"; - eval_formula phi (Decl d) lcxt) - | None, true -> - Logging.out "\n ->>>> Statement has NO transition label\n"; - eval_formula phi (Stmt st) lcxt - | _, false -> - Logging.out "\n ->>>> Declaration is NOT in types and _ label\n"; - evaluate_on_substmt st (eval_ET tl trs) in + | None -> false + | Some d -> eval_formula phi (Decl d) lcxt) + | None, true -> eval_formula phi (Stmt st) lcxt + | _, false -> evaluate_on_substmt st (eval_ET tl trs) in match an with | Decl d -> do_decl d | Stmt BlockExpr(_, _, _, d) -> (* From BlockExpr we jump directly to its BlockDecl *) - Logging.out "\n->>>> BlockExpr evaluated in ET, evaluating its BlockDecl \n"; eval_ET tl trs phi (Decl d) lcxt | Stmt st -> do_stmt st - (* Formulas are evaluated on a AST node an and a linter context lcxt *) and eval_formula f an lcxt = - match f with - | True -> true - | False -> false - | Atomic (name, params) -> eval_Atomic name params an lcxt - | Not f1 -> not (eval_formula f1 an lcxt) - | And (f1, f2) -> (eval_formula f1 an lcxt) && (eval_formula f2 an lcxt) - | Or (f1, f2) -> (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt) - | Implies (f1, f2) -> - not (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt) - | AU (f1, f2) -> eval_AU f1 f2 an lcxt - | EU (f1, f2) -> eval_EU f1 f2 an lcxt - | EF f1 -> eval_EF f1 an lcxt - | AF f1 -> eval_formula (AU (True, f1)) an lcxt - | AG f1 -> eval_formula (Not (EF (Not f1))) an lcxt - | EX f1 -> eval_EX f1 an lcxt - | AX f1 -> eval_formula (Not (EX (Not f1))) an lcxt - | EH (cl, phi) -> eval_EH cl phi an lcxt - | EG f1 -> (* st |= EG f1 <=> st |= f1 /\ EX EG f1 *) - eval_formula (And (f1, EX (EG (f1)))) an lcxt - | ET (tl, sw, phi) -> eval_ET tl sw phi an lcxt + debug_eval_begin (debug_create_payload an f); + let res = match f with + | True -> true + | False -> false + | Atomic (name, params) -> eval_Atomic name params an lcxt + | Not f1 -> not (eval_formula f1 an lcxt) + | And (f1, f2) -> (eval_formula f1 an lcxt) && (eval_formula f2 an lcxt) + | Or (f1, f2) -> (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt) + | Implies (f1, f2) -> + not (eval_formula f1 an lcxt) || (eval_formula f2 an lcxt) + | AU (f1, f2) -> eval_AU f1 f2 an lcxt + | EU (f1, f2) -> eval_EU f1 f2 an lcxt + | EF f1 -> eval_EF f1 an lcxt + | AF f1 -> eval_formula (AU (True, f1)) an lcxt + | AG f1 -> eval_formula (Not (EF (Not f1))) an lcxt + | EX f1 -> eval_EX f1 an lcxt + | AX f1 -> eval_formula (Not (EX (Not f1))) an lcxt + | EH (cl, phi) -> eval_EH cl phi an lcxt + | EG f1 -> (* st |= EG f1 <=> st |= f1 /\ EX EG f1 *) + eval_formula (And (f1, EX (EG (f1)))) an lcxt + | ET (tl, sw, phi) -> eval_ET tl sw phi an lcxt in + debug_eval_end res; + res diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 8a89ad1f3..d8172daa0 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -54,3 +54,5 @@ type ast_node = | Decl of Clang_ast_t.decl val eval_formula : t -> ast_node -> CLintersContext.context -> bool + +val save_dotty_when_in_debug_mode : DB.source_file -> unit diff --git a/infer/src/clang/predicates.ml b/infer/src/clang/predicates.ml index 829a9b381..977c212e6 100644 --- a/infer/src/clang/predicates.ml +++ b/infer/src/clang/predicates.ml @@ -50,6 +50,9 @@ let var_descs_name stmt = type t = string * string list (* (name, [param1,...,paramK]) *) +let pp_predicate fmt (name, arglist) = + Format.fprintf fmt "%s(%a)" name (Utils.pp_comma_seq Format.pp_print_string) arglist + let is_declaration_kind decl s = Clang_ast_proj.get_decl_kind_string decl = s diff --git a/infer/src/clang/predicates.mli b/infer/src/clang/predicates.mli index 7c4468494..b855d0f0d 100644 --- a/infer/src/clang/predicates.mli +++ b/infer/src/clang/predicates.mli @@ -52,3 +52,5 @@ val is_unop_with_kind : Clang_ast_t.stmt -> string -> bool val is_stmt : Clang_ast_t.stmt -> string -> bool val isa : Clang_ast_t.stmt -> string -> bool + +val pp_predicate : Format.formatter -> string * string list -> unit