[CTL] Initial version of a step-by-step debugger for CTL formulas

Summary:
This debugger stops the execution of CTL during the evaluation of formulas, then shows useful info about the current state:
- Which formula is being evaluated
- In which part of the AST is such formula being evaluated
- Line number of the source file
- Whether a CTL-Transition will take place or not
- Node-ID that can be related to the dotty file containing the evaluation graph (the one in infer-out/lint_dotty/)

The AST is shown with coloured nodes, where each colour has the following meaning:
- [Default terminal colour], Bold: The node is being evaluated
- Green, Bold: The formula returned true on the current node
- Red, Bold: The formula returned false on the current node

Reviewed By: ddino

Differential Revision: D4834451

fbshipit-source-id: c9aa970

infer/.merlin

@@ -1,5 +1,6 @@
 S src/**
 B _build/infer/**
+PKG ANSITerminal
 PKG atdgen
 PKG core
 PKG ctypes

infer/src/Makefile

@@ -41,7 +41,7 @@ OCAMLBUILD_OPTIONS = \
   -tag-line "<*{clang/clang_ast_*,backend/jsonbug_*,checkers/stacktree_*,ffi/gen/*}>: warn(-27-32-34-35-39)" \
   -tag-line "<*/{,*/}*.{ml,re}{,i}>: package(ppx_compare)" \
   -tag thread \
-  -pkgs atdgen,core,ctypes.stubs,extlib,oUnit,str,unix,xmlm,yojson,zip
+  -pkgs ANSITerminal,atdgen,core,ctypes.stubs,extlib,oUnit,str,unix,xmlm,yojson,zip
 
 ifeq ($(ENABLE_OCAML_BINANNOT),yes)
 OCAMLBUILD_OPTIONS += -cflags -bin-annot

infer/src/clang/cTL.ml

@@ -48,6 +48,14 @@ type t = (* A ctl formula *)
   | ET of ALVar.alexp list * transitions option * t
   | ETX of ALVar.alexp list * transitions option * t
 
+let has_transition phi = match phi with
+  | True | False | Atomic _ | Not _ | And (_, _)
+  | Or (_, _) | Implies (_, _) | InNode (_, _)
+  | AX _ | AF _ | AG _ | AU (_, _) | EH (_, _) -> false
+  | EX (trans_opt, _) | EF (trans_opt, _)
+  | EG (trans_opt, _) | EU (trans_opt, _, _)
+  | ET (_, trans_opt, _) | ETX (_, trans_opt, _) -> Option.is_some trans_opt
+
 (* "set" clauses are used for defining mandatory variables that will be used
    by when reporting issues: eg for defining the condition.
 
@@ -141,6 +149,51 @@ module Debug = struct
                                       pp_transition trans
                                       pp_formula phi
 
+  let pp_ast ~ast_node_to_highlight ?(prettifier=Fn.id) fmt root =
+    let pp_node_info fmt an = match an with
+      | Stmt (ObjCMessageExpr (_, _, _, {omei_selector})) ->
+          Format.fprintf fmt "selector: \"%s\"" omei_selector
+      | _ -> Format.ifprintf fmt "" in
+    let rec pp_children pp_node wrapper fmt level nodes =
+      match nodes with
+      | [] -> ()
+      | node :: nodes ->
+          pp_node fmt (wrapper node) level "|-";
+          pp_children pp_node wrapper fmt level nodes in
+    let rec pp_ast_aux fmt root level prefix =
+      let get_node_name (an: ast_node) =
+        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 should_highlight = match root, ast_node_to_highlight with
+        | Stmt r, Stmt n -> phys_equal r n
+        | Decl r, Decl n -> phys_equal r n
+        | _ -> false in
+      let node_name =
+        let node_name = get_node_name root in
+        if should_highlight then prettifier node_name else node_name in
+      let spaces = String.make (level*(String.length prefix)) ' ' in
+      let next_level = level + 1 in
+      Format.fprintf fmt "%s%s%s %a@\n" spaces prefix node_name pp_node_info root;
+      (match root with
+       | Stmt (DeclStmt (_, _, decls)) -> pp_decls fmt next_level decls
+       | Stmt stmt ->
+           let _, stmts = Clang_ast_proj.get_stmt_tuple stmt in
+           pp_stmts fmt next_level stmts
+       | Decl (VarDecl (_, _, _, {vdi_init_expr})) ->
+           pp_stmts fmt next_level (Option.to_list vdi_init_expr)
+       | Decl decl ->
+           let decls =
+             Clang_ast_proj.get_decl_context_tuple decl |>
+             Option.map ~f:(fun (decls, _) -> decls) |>
+             Option.value ~default:[] in
+           pp_decls fmt next_level decls)
+    and pp_stmts fmt level stmts =
+      pp_children pp_ast_aux (fun n -> Stmt n) fmt level stmts
+    and pp_decls fmt level decls =
+      pp_children pp_ast_aux (fun n -> Decl n) fmt level decls in
+    pp_ast_aux fmt root 0 ""
+
   module EvaluationTracker = struct
     exception Empty_stack of string
 
@@ -153,29 +206,103 @@ module Debug = struct
       eval_result: eval_result;
     }
 
-    type node = {
+    type eval_node = {
       id: int;
       content: content;
     }
 
-    type tree = Tree of node * (tree list)
+    type tree = Tree of eval_node * (tree list)
+
+    type ast_node_to_display =
+      (* the node can be used to describe further sub calls in the evaluation stack *)
+      | Carry_forward of ast_node
+      (* the node cannot be further used to describe sub calls in the evaluation stack *)
+      | Last_occurrence of ast_node
 
     type t = {
       next_id: int;
-      eval_stack: tree Stack.t;
+      eval_stack: (tree * ast_node_to_display) Stack.t;
       forest: tree list;
+      debugger_active: bool;
     }
 
     let create_content ast_node phi lcxt =
       {ast_node; phi; eval_result = Eval_undefined; lcxt = lcxt; }
 
-    let create () = {next_id = 0; eval_stack = Stack.create(); forest = [] }
+    let create () = {
+      next_id = 0;
+      eval_stack = Stack.create();
+      forest = [];
+      debugger_active = false;
+    }
+
+    let explain t ~eval_node ~ast_node_to_display =
+      if t.debugger_active then
+        let line_number an =
+          let line_of_source_range (sr: Clang_ast_t.source_range) =
+            let loc_info, _ = sr in
+            loc_info.sl_line in
+          match an with
+          | Stmt stmt ->
+              let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in
+              line_of_source_range stmt_info.si_source_range
+          | Decl decl ->
+              let decl_info = Clang_ast_proj.get_decl_tuple decl in
+              line_of_source_range decl_info.di_source_range in
+        let highlight_style = match eval_node.content.eval_result with
+          | Eval_undefined -> ANSITerminal.[Bold]
+          | Eval_true -> ANSITerminal.[Bold; green]
+          | Eval_false -> ANSITerminal.[Bold; red] in
+        let ast_node_to_highlight = eval_node.content.ast_node in
+        let ast_root, is_last_occurrence = match ast_node_to_display with
+          | Carry_forward n -> n, false
+          | Last_occurrence n -> n, true in
+        let ast_str =
+          Format.asprintf "%a"
+            (pp_ast ~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s"))
+            ast_root in
+        Logging.out "\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s\n"
+          eval_node.id
+          (Stack.length t.eval_stack)
+          (Option.value_map
+             ~default:"Unknown" ~f:string_of_int (line_number ast_node_to_highlight));
+        let is_eval_result_undefined = match eval_node.content.eval_result with
+          | Eval_undefined -> true
+          | _ -> false in
+        if is_last_occurrence && is_eval_result_undefined then
+          Logging.out "From this step, a transition to a different part of the AST may follow.\n";
+        let phi_str = Format.asprintf "%a" pp_formula eval_node.content.phi in
+        Logging.out "CTL Formula: %s\n\n" phi_str;
+        Logging.out "%s\n" ast_str;
+        let quit_token = "q" in
+        Logging.out "Press Enter to continue or type %s to quit... @?" quit_token;
+        match read_line () |> String.lowercase with
+        | s when String.equal s quit_token -> exit 0
+        | _ ->
+            (* Remove the line at the bottom of terminal with the debug instructions *)
+            ANSITerminal.(
+              (* move one line up, as current line is the one generated by pressing enter *)
+              move_cursor 0 (-1);
+              move_bol (); (* move to the beginning of the line *)
+              erase Below; (* erase what follows the cursor's position *)
+            )
 
     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 t.eval_stack subtree';
+      let ast_node_from_previous_call =
+        match Stack.top t.eval_stack with
+        | Some (_, Last_occurrence _) -> content.ast_node
+        | Some (_, Carry_forward an) -> an
+        | None -> content.ast_node in
+      let ast_node_to_display =
+        if has_transition content.phi then Last_occurrence ast_node_from_previous_call
+        else Carry_forward ast_node_from_previous_call in
+      Stack.push t.eval_stack (subtree', ast_node_to_display);
+      explain t
+        ~eval_node:node
+        ~ast_node_to_display;
       {t with next_id = t.next_id + 1}
 
     let eval_end t result =
@@ -184,15 +311,21 @@ module Debug = struct
         | 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_exn t.eval_stack with
+      let evaluated_tree, eval_node, ast_node_to_display = match Stack.pop_exn t.eval_stack with
-        | Tree ({id = _; content} as node, children) ->
+        | Tree ({id = _; content} as eval_node, children), ast_node_to_display ->
             let content' = {content with eval_result = eval_result_of_bool result} in
-            Tree ({node with content = content'}, children) in
+            let eval_node' = {eval_node with content = content'} in
+            Tree (eval_node', children),
+            eval_node',
+            ast_node_to_display in
+      explain t
+        ~eval_node
+        ~ast_node_to_display;
       let forest' =
         if Stack.is_empty t.eval_stack then evaluated_tree :: t.forest
         else
           let parent = match Stack.pop_exn t.eval_stack with
-              Tree (node, children) -> Tree (node, evaluated_tree :: children) in
+              Tree (node, children), ntd -> Tree (node, evaluated_tree :: children), ntd in
           Stack.push t.eval_stack parent;
           t.forest in
       {t with forest = forest'}

opam

@@ -26,6 +26,7 @@ remove: [
 ]
 ocaml-version: [ >= "4.02.1" ]
 depends: [
+  "ANSITerminal" {>="0.7"}
   "atdgen" {>="1.6.0"}
   "core" {>="113.33.03"}
   "conf-autoconf"

scripts/toplevel_init

@@ -7,6 +7,7 @@
 #require "sawja";;
 #require "atdgen";;
 #require "xmlm";;
+#require "ANSITerminal";;
 
 (* load infer code *)
 #load "externstubslib.cma";;