[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

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

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

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

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

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)
+        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 *)
+        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;

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) ||
+  eval_formula phi (Stmt st) lcxt
-  IList.exists (fun s -> eval_EF phi (Stmt s) lcxt) succs
+  || 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"
+  eval_formula phi (Decl dec) lcxt ||
-    (Clang_ast_proj.get_decl_kind_string dec);
-  (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_formula phi (Decl d) lcxt || eval_super (Some idi')
-             || (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,55 +423,32 @@ 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 ->
+         | None -> false
-             Logging.out "\n   ->>>> NO transition returned";
+         | Some st -> eval_formula phi (Stmt st) lcxt)
-             false
+    | None, true -> eval_formula phi (Decl d) lcxt
-         | Some st ->
+    | _, false -> evaluate_on_subdeclarations d (eval_ET tl trs) in
-             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
   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 ->
+         | None -> false
-             Logging.out "\n   ->>>> NO transition  returned\n";
+         | Some d -> eval_formula phi (Decl d) lcxt)
-             false
+    | None, true -> eval_formula phi (Stmt st) lcxt
-         | Some d ->
+    | _, false -> evaluate_on_substmt st (eval_ET tl trs) in
-             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
   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
+  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
@@ -318,4 +467,6 @@ and eval_formula f 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
+    | ET (tl, sw, phi) -> eval_ET tl sw phi an lcxt in
+  debug_eval_end res;
+  res

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

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
 

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