diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 3f68ac130..1e6c75eee 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -73,12 +73,23 @@ module Node = struct | UnaryOperator [@@deriving compare] + type prune_node_kind = + | PruneNodeKind_ExceptionHandler + | PruneNodeKind_FalseBranch + | PruneNodeKind_InBound + | PruneNodeKind_IsInstance + | PruneNodeKind_MethodBody + | PruneNodeKind_NotNull + | PruneNodeKind_TrueBranch + [@@deriving compare] + type nodekind = | Start_node | Exit_node | Stmt_node of stmt_nodekind | Join_node - | Prune_node of bool * Sil.if_kind * string (** (true/false branch, if_kind, comment) *) + | Prune_node of bool * Sil.if_kind * prune_node_kind + (** (true/false branch, if_kind, comment) *) | Skip_node of string [@@deriving compare] @@ -309,14 +320,31 @@ module Node = struct let d_instrs ~highlight (node : t) = L.d_pp_with_pe ~color:Green (pp_instrs ~highlight) node + let string_of_prune_node_kind = function + | PruneNodeKind_ExceptionHandler -> + "exception handler" + | PruneNodeKind_FalseBranch -> + "false Branch" + | PruneNodeKind_InBound -> + "In bound" + | PruneNodeKind_IsInstance -> + "Is instance" + | PruneNodeKind_MethodBody -> + "method_body" + | PruneNodeKind_NotNull -> + "Not null" + | PruneNodeKind_TrueBranch -> + "true Branch" + + (** Return a description of the cfg node *) let get_description pe node = let str_kind = match get_kind node with | Stmt_node _ -> "Instructions" - | Prune_node (_, _, descr) -> - "Conditional " ^ descr + | Prune_node (_, _, prune_node_kind) -> + "Conditional " ^ string_of_prune_node_kind prune_node_kind | Exit_node -> "Exit" | Skip_node _ -> diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 1ef6d787f..309490ff7 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -69,13 +69,23 @@ module Node : sig | ThrowNPE | UnaryOperator + type prune_node_kind = + | PruneNodeKind_ExceptionHandler + | PruneNodeKind_FalseBranch + | PruneNodeKind_InBound + | PruneNodeKind_IsInstance + | PruneNodeKind_MethodBody + | PruneNodeKind_NotNull + | PruneNodeKind_TrueBranch + (** kind of cfg node *) type nodekind = | Start_node | Exit_node | Stmt_node of stmt_nodekind | Join_node - | Prune_node of bool * Sil.if_kind * string (** (true/false branch, if_kind, comment) *) + | Prune_node of bool * Sil.if_kind * prune_node_kind + (** (true/false branch, if_kind, comment) *) | Skip_node of string [@@deriving compare] diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 24947856f..c01a7be92 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -29,7 +29,10 @@ let source_range_of_stmt stmt = module Nodes = struct - let prune_kind b if_kind = Procdesc.Node.Prune_node (b, if_kind, string_of_bool b ^ " Branch") + let prune_kind b if_kind = + Procdesc.Node.Prune_node + (b, if_kind, if b then PruneNodeKind_TrueBranch else PruneNodeKind_FalseBranch) + let is_true_prune_node n = match Procdesc.Node.get_kind n with diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 90c18fa40..5dd8a8e64 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -919,8 +919,12 @@ let instruction (context : JContext.t) pc instr : translation = let sil_test_true = Exp.UnOp (Unop.LNot, sil_test_false, None) in let sil_instrs_true = Sil.Prune (sil_test_true, loc, true, Sil.Ik_if) in let sil_instrs_false = Sil.Prune (sil_test_false, loc, false, Sil.Ik_if) in - let node_kind_true = Procdesc.Node.Prune_node (true, Sil.Ik_if, "method_body") in - let node_kind_false = Procdesc.Node.Prune_node (false, Sil.Ik_if, "method_body") in + let node_kind_true = + Procdesc.Node.Prune_node (true, Sil.Ik_if, PruneNodeKind_MethodBody) + in + let node_kind_false = + Procdesc.Node.Prune_node (false, Sil.Ik_if, PruneNodeKind_MethodBody) + in let prune_node_true = create_node node_kind_true (instrs1 @ instrs2 @ [sil_instrs_true]) and prune_node_false = create_node node_kind_false (instrs1 @ instrs2 @ [sil_instrs_false]) @@ -1054,7 +1058,7 @@ let instruction (context : JContext.t) pc instr : translation = let not_null_node = let sil_not_null = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in let sil_prune_not_null = Sil.Prune (sil_not_null, loc, true, Sil.Ik_if) - and not_null_kind = Procdesc.Node.Prune_node (true, Sil.Ik_if, "Not null") in + and not_null_kind = Procdesc.Node.Prune_node (true, Sil.Ik_if, PruneNodeKind_NotNull) in create_node not_null_kind (instrs @ [sil_prune_not_null]) in let throw_npe_node = @@ -1095,7 +1099,9 @@ let instruction (context : JContext.t) pc instr : translation = (instrs, sil_array_expr, sil_length_expr, sil_index_expr) in let in_bound_node = - let in_bound_node_kind = Procdesc.Node.Prune_node (true, Sil.Ik_if, "In bound") in + let in_bound_node_kind = + Procdesc.Node.Prune_node (true, Sil.Ik_if, PruneNodeKind_InBound) + in let sil_assume_in_bound = let sil_in_bound = let sil_positive_index = @@ -1159,7 +1165,9 @@ let instruction (context : JContext.t) pc instr : translation = let is_instance_node = let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Exp.zero) in let asssume_instance_of = Sil.Prune (check_is_false, loc, true, Sil.Ik_if) - and instance_of_kind = Procdesc.Node.Prune_node (true, Sil.Ik_if, "Is instance") in + and instance_of_kind = + Procdesc.Node.Prune_node (true, Sil.Ik_if, PruneNodeKind_IsInstance) + in create_node instance_of_kind (instrs @ [call; asssume_instance_of]) and throw_cast_exception_node = let check_is_true = Exp.BinOp (Binop.Ne, res_ex, Exp.one) in diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index f4cf01643..ff158774a 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -24,7 +24,6 @@ let create_handler_table impl = let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handler_table = let catch_block_table = Hashtbl.create 1 in - let exn_message = "exception handler" in let procdesc = context.procdesc in let create_node loc node_kind instrs = Procdesc.create_node procdesc loc node_kind instrs in let ret_var = Procdesc.get_ret_var procdesc in @@ -102,8 +101,12 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle let instr_rethrow_exn = Sil.Store (Exp.Lvar ret_var, ret_type, Exp.Exn (Exp.Var id_exn_val), loc) in - let node_kind_true = Procdesc.Node.Prune_node (true, if_kind, exn_message) in - let node_kind_false = Procdesc.Node.Prune_node (false, if_kind, exn_message) in + let node_kind_true = + Procdesc.Node.Prune_node (true, if_kind, PruneNodeKind_ExceptionHandler) + in + let node_kind_false = + Procdesc.Node.Prune_node (false, if_kind, PruneNodeKind_ExceptionHandler) + in let node_true = let instrs_true = [instr_call_instanceof; instr_prune_true; instr_set_catch_var] in create_node loc node_kind_true instrs_true diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index d4739bd50..fdcb0c173 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -167,7 +167,12 @@ struct let mk_prune_nodes_for_cond cond_exp if_kind = let mk_prune_node cond_exp if_kind true_branch = let prune_instr = Sil.Prune (cond_exp, dummy_loc, true_branch, if_kind) in - create_node (Procdesc.Node.Prune_node (true_branch, if_kind, "")) [prune_instr] + create_node + (Procdesc.Node.Prune_node + ( true_branch + , if_kind + , if true_branch then PruneNodeKind_TrueBranch else PruneNodeKind_FalseBranch )) + [prune_instr] in let true_prune_node = mk_prune_node cond_exp if_kind true in let false_prune_node =