diff --git a/infer/.merlin b/infer/.merlin index a235f84b9..911615581 100644 --- a/infer/.merlin +++ b/infer/.merlin @@ -1,5 +1,6 @@ S src/** B _build/infer/** +PKG ANSITerminal PKG atdgen PKG core PKG ctypes diff --git a/infer/src/Makefile b/infer/src/Makefile index d2ae966a0..ab6e141b4 100644 --- a/infer/src/Makefile +++ b/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 diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 9c77151a1..58847c99c 100644 --- a/infer/src/clang/cTL.ml +++ b/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 - | Tree ({id = _; content} as node, children) -> + let evaluated_tree, eval_node, ast_node_to_display = match Stack.pop_exn t.eval_stack with + | 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'} diff --git a/opam b/opam index 0d9b7d543..53264195c 100644 --- a/opam +++ b/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" diff --git a/scripts/toplevel_init b/scripts/toplevel_init index c307c8174..774686dea 100644 --- a/scripts/toplevel_init +++ b/scripts/toplevel_init @@ -7,6 +7,7 @@ #require "sawja";; #require "atdgen";; #require "xmlm";; +#require "ANSITerminal";; (* load infer code *) #load "externstubslib.cma";;