From d694038abdd1ea55e4b74099bf2c958e8293f563 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Wed, 27 Sep 2017 07:34:07 -0700 Subject: [PATCH] New test for the tableaux method. Reviewed By: dulmarod Differential Revision: D5862915 fbshipit-source-id: 6c6c4b6 --- infer/lib/linter_rules/linters.al | 4 +- infer/src/clang/ALVar.mli | 2 +- infer/src/clang/cFrontend_checkers_main.ml | 157 ++++++---- infer/src/clang/cFrontend_config.ml | 2 + infer/src/clang/cFrontend_config.mli | 2 + infer/src/clang/cFrontend_errors.ml | 3 +- infer/src/clang/cFrontend_errors.mli | 4 + infer/src/clang/cPredicates.ml | 2 +- infer/src/clang/cPredicates.mli | 2 +- infer/src/clang/cTL.ml | 32 +- infer/src/clang/cTL.mli | 10 +- infer/src/clang/ctl_parser_types.mli | 2 + infer/src/clang/tableaux.ml | 336 +++++++++++++++++++++ infer/src/clang/tableaux.mli | 28 ++ 14 files changed, 502 insertions(+), 84 deletions(-) create mode 100644 infer/src/clang/tableaux.ml create mode 100644 infer/src/clang/tableaux.mli diff --git a/infer/lib/linter_rules/linters.al b/infer/lib/linter_rules/linters.al index fcd208dee..dbc4ddea9 100644 --- a/infer/lib/linter_rules/linters.al +++ b/infer/lib/linter_rules/linters.al @@ -114,11 +114,11 @@ DEFINE-CHECKER REGISTERED_OBSERVER_BEING_DEALLOCATED = { (remove_observer1) HOLDS-EVENTUALLY; - LET eventually_removeObserver = + LET eventually_removeObserver = IN-NODE ObjCImplementationDecl, ObjCProtocolDecl WITH-TRANSITION Any (remove_observer_in_method OR remove_observer_in_method HOLDS-IN-SOME-SUPERCLASS-OF ObjCImplementationDecl) - HOLDS-EVENTUALLY; + HOLDS-EVENTUALLY; SET report_when = WHEN diff --git a/infer/src/clang/ALVar.mli b/infer/src/clang/ALVar.mli index d00e6562a..7dd57a919 100644 --- a/infer/src/clang/ALVar.mli +++ b/infer/src/clang/ALVar.mli @@ -11,7 +11,7 @@ open! IStd type keyword = Doc_url | Message | Mode | Name | Report_when | Severity | Suggestion -type formula_id = Formula_id of string +type formula_id = Formula_id of string [@@deriving compare] (** a regexp and its cached compiled version *) type cached_regexp = {string: string; regexp: Str.regexp Lazy.t} [@@deriving compare] diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index 5b083ce82..b49116aa9 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/infer/src/clang/cFrontend_checkers_main.ml @@ -202,79 +202,118 @@ let get_method_body_opt decl = -> Logging.die InternalError "Should only be called with method, but got %s" (Clang_ast_proj.get_decl_kind_string decl) -let rec do_frontend_checks_stmt (context: CLintersContext.context) stmt = +let call_tableaux cxt an map_active = + if CFrontend_config.tableaux_evaluation then Tableaux.build_valuation an cxt map_active + +let rec do_frontend_checks_stmt (context: CLintersContext.context) + (map_act: Tableaux.context_linter_map) stmt = let open Clang_ast_t in - let do_all_checks_on_stmts context stmt = + let an = Ctl_parser_types.Stmt stmt in + (*L.(debug Linters Medium) + "@\n >>>>>>Visit node %i <<<<<@\n" (Ctl_parser_types.ast_node_pointer an) ; *) + let do_all_checks_on_stmts context map_active stmt = ( match stmt with | DeclStmt (_, _, decl_list) - -> List.iter ~f:(do_frontend_checks_decl context) decl_list + -> List.iter ~f:(do_frontend_checks_decl context map_active) decl_list | BlockExpr (_, _, _, decl) - -> List.iter ~f:(do_frontend_checks_decl context) [decl] + -> List.iter ~f:(do_frontend_checks_decl context map_active) [decl] | _ -> () ) ; - do_frontend_checks_stmt context stmt + do_frontend_checks_stmt context map_active stmt in - CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Stmt stmt) ; - match stmt with - | ObjCAtSynchronizedStmt (_, stmt_list) - -> let stmt_context = {context with CLintersContext.in_synchronized_block= true} in - List.iter ~f:(do_all_checks_on_stmts stmt_context) stmt_list - | IfStmt (_, [stmt1; stmt2; cond_stmt; inside_if_stmt; inside_else_stmt]) - -> (* here we analyze the children of the if stmt with the standard context, - except for inside_if_stmt... *) - List.iter ~f:(do_all_checks_on_stmts context) [stmt1; stmt2; cond_stmt; inside_else_stmt] ; - let inside_if_stmt_context = - {context with CLintersContext.if_context= compute_if_context context cond_stmt} - in - (* ...and here we analyze the stmt inside the if with the context - extended with the condition of the if *) - do_all_checks_on_stmts inside_if_stmt_context inside_if_stmt - | OpaqueValueExpr (_, lstmt, _, opaque_value_expr_info) - -> let stmts = - match opaque_value_expr_info.Clang_ast_t.ovei_source_expr with - | Some stmt - -> lstmt @ [stmt] - | _ - -> lstmt - in - List.iter ~f:(do_all_checks_on_stmts context) stmts - (* given that this has not been translated, looking up for variables *) - (* inside leads to inconsistencies *) - | ObjCAtCatchStmt _ - -> () - | _ - -> let stmts = snd (Clang_ast_proj.get_stmt_tuple stmt) in - List.iter ~f:(do_all_checks_on_stmts context) stmts + CFrontend_errors.invoke_set_of_checkers_on_node context an ; + (* The map should be visited when we enter the node before visiting children *) + let map_active = Tableaux.update_linter_context_map an map_act in + let stmt_context_list = + match stmt with + | ObjCAtSynchronizedStmt (_, stmt_list) + -> [({context with CLintersContext.in_synchronized_block= true}, stmt_list)] + | OpaqueValueExpr (_, lstmt, _, opaque_value_expr_info) -> ( + match opaque_value_expr_info.Clang_ast_t.ovei_source_expr with + | Some stmt + -> [(context, lstmt @ [stmt])] + | _ + -> [(context, lstmt)] ) + | IfStmt (_, [stmt1; stmt2; cond_stmt; inside_if_stmt; inside_else_stmt]) + -> let inside_if_stmt_context = + {context with CLintersContext.if_context= compute_if_context context cond_stmt} + in + (* distinguish between then and else branch as they need different context *) + [ (context, [stmt1; stmt2; cond_stmt; inside_else_stmt]) + ; (inside_if_stmt_context, [inside_if_stmt]) ] + (* given that this has not been translated, looking up for variables *) + (* inside leads to inconsistencies *) + | ObjCAtCatchStmt _ + -> [(context, [])] + | _ + -> [(context, snd (Clang_ast_proj.get_stmt_tuple stmt))] + in + if CFrontend_config.tableaux_evaluation then + (* Unlike in the standard algorithm, nodes reachable via transitions + PointerToDecl are not visited + during the evaluation of the formula. So we need to visit + them diring the general visit of the tree. *) + do_frontend_checks_via_transition context map_active an CTL.PointerToDecl ; + List.iter + ~f:(fun (cxt, stmts) -> + List.iter ~f:(do_all_checks_on_stmts cxt map_active) stmts ; + call_tableaux cxt an map_active) + stmt_context_list + +(* Visit nodes via a transition *) +and do_frontend_checks_via_transition context map_active an trans = + let succs = CTL.next_state_via_transition an trans in + List.iter + ~f:(fun an' -> + (*L.(debug Linters Medium) + "@\n---- Going from %i to %i via transition %a ---- @\n" + (Ctl_parser_types.ast_node_pointer an) (Ctl_parser_types.ast_node_pointer an') + CTL.Debug.pp_transition (Some trans) ;*) + match an' with + | Ctl_parser_types.Decl d + -> do_frontend_checks_decl context map_active d + | Ctl_parser_types.Stmt st + -> do_frontend_checks_stmt context map_active st) + succs -and do_frontend_checks_decl (context: CLintersContext.context) decl = +and do_frontend_checks_decl (context: CLintersContext.context) + (map_act: Tableaux.context_linter_map) decl = let open Clang_ast_t in + let an = Ctl_parser_types.Decl decl in + (* The map should be visited when we enter the node before visiting children *) + let map_active = Tableaux.update_linter_context_map an map_act in match decl with | FunctionDecl _ | CXXMethodDecl _ | CXXConstructorDecl _ | CXXConversionDecl _ | CXXDestructorDecl _ - | ObjCMethodDecl _ | BlockDecl _ - -> ( - let context' = CLintersContext.update_current_method context decl in - CFrontend_errors.invoke_set_of_checkers_on_node context' (Ctl_parser_types.Decl decl) ; - match get_method_body_opt decl with + | ObjCMethodDecl _ + -> let context' = CLintersContext.update_current_method context decl in + CFrontend_errors.invoke_set_of_checkers_on_node context' an ; + (* We need to visit explicitly nodes reachable via Parameters transitions + because they won't be visited during the evaluation of the formula *) + do_frontend_checks_via_transition context' map_active an CTL.Parameters ; + ( match get_method_body_opt decl with | Some stmt - -> do_frontend_checks_stmt context' stmt + -> do_frontend_checks_stmt context' map_active stmt | None - -> () ) + -> () ) ; + call_tableaux context' an map_active | ObjCImplementationDecl (_, _, decls, _, _) | ObjCInterfaceDecl (_, _, decls, _, _) - -> CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Decl decl) ; + -> CFrontend_errors.invoke_set_of_checkers_on_node context an ; let context' = {context with current_objc_class= Some decl} in - List.iter ~f:(do_frontend_checks_decl context') decls + List.iter ~f:(do_frontend_checks_decl context' map_active) decls ; + call_tableaux context' an map_active | _ - -> CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Decl decl) ; - match Clang_ast_proj.get_decl_context_tuple decl with + -> CFrontend_errors.invoke_set_of_checkers_on_node context an ; + ( match Clang_ast_proj.get_decl_context_tuple decl with | Some (decls, _) - -> List.iter ~f:(do_frontend_checks_decl context) decls + -> List.iter ~f:(do_frontend_checks_decl context map_active) decls | None - -> () + -> () ) ; + call_tableaux context an map_active let context_with_ck_set context decl_list = let is_ck = @@ -327,20 +366,20 @@ let do_frontend_checks (trans_unit_ctx: CFrontend_config.translation_unit_contex if Config.print_active_checkers then L.progress "Linting file %a, active linters: @\n%a@\n" SourceFile.pp source_file CFrontend_errors.pp_linters filtered_parsed_linters ; + Tableaux.init_global_nodes_valuation () ; match ast with | Clang_ast_t.TranslationUnitDecl (_, decl_list, _, _) -> let context = context_with_ck_set (CLintersContext.empty trans_unit_ctx) decl_list in - let is_decl_allowed decl = - let decl_info = Clang_ast_proj.get_decl_tuple decl in - CLocation.should_do_frontend_check trans_unit_ctx decl_info.Clang_ast_t.di_source_range - in - let allowed_decls = List.filter ~f:is_decl_allowed decl_list in + let allowed_decls = List.filter ~f:(Tableaux.is_decl_allowed context) decl_list in (* We analyze the top level and then all the allowed declarations *) + let active_map : Tableaux.context_linter_map = Tableaux.init_active_map () in CFrontend_errors.invoke_set_of_checkers_on_node context (Ctl_parser_types.Decl ast) ; - List.iter ~f:(do_frontend_checks_decl context) allowed_decls ; + List.iter ~f:(do_frontend_checks_decl context active_map) allowed_decls ; if LintIssues.exists_issues () then store_issues source_file ; L.(debug Linters Medium) "End linting file %a@\n" SourceFile.pp source_file ; CTL.save_dotty_when_in_debug_mode trans_unit_ctx.CFrontend_config.source_file - | _ - -> (* NOTE: Assumes that an AST always starts with a TranslationUnitDecl *) - assert false + (*if CFrontend_config.tableaux_evaluation then ( + Tableaux.print_table_size () ; + Tableaux.print_global_valuation_map ()) *) + | _ (* NOTE: Assumes that an AST always starts with a TranslationUnitDecl *) + -> assert false diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index 51e1fadf1..3b27cd565 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -174,3 +174,5 @@ let reset_global_state () = global_translation_unit_decls := [] ; log_out := Format.std_formatter ; sil_types_map := Clang_ast_extend.TypePointerMap.empty + +let tableaux_evaluation = false diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index 9df41ee3f..fb424815c 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -174,3 +174,5 @@ val sil_types_map : Typ.desc Clang_ast_extend.TypePointerMap.t ref Populated during frontend execution when new type is found *) val reset_global_state : unit -> unit + +val tableaux_evaluation : bool diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index 5a064c9ff..4cf6549bb 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -478,5 +478,6 @@ let invoke_set_of_checkers_on_node context an = Because depending on the formula it may give an error at line -1 *) () | _ - -> invoke_set_of_parsed_checkers_an !parsed_linters context an ) ; + -> if not CFrontend_config.tableaux_evaluation then + invoke_set_of_parsed_checkers_an !parsed_linters context an ) ; if Config.default_linters then invoke_set_of_hard_coded_checkers_an context an diff --git a/infer/src/clang/cFrontend_errors.mli b/infer/src/clang/cFrontend_errors.mli index 67a2d0f4f..bab0ca7dc 100644 --- a/infer/src/clang/cFrontend_errors.mli +++ b/infer/src/clang/cFrontend_errors.mli @@ -49,3 +49,7 @@ val expand_checkers : macros_map -> paths_map -> CTL.ctl_checker list -> CTL.ctl val create_parsed_linters : string -> CTL.ctl_checker list -> linter list val remove_new_lines : string -> string + +val fill_issue_desc_info_and_log : + CLintersContext.context -> Ctl_parser_types.ast_node -> CIssue.issue_desc -> string option + -> Location.t -> unit diff --git a/infer/src/clang/cPredicates.ml b/infer/src/clang/cPredicates.ml index 5a656d7b0..d47fb9039 100644 --- a/infer/src/clang/cPredicates.ml +++ b/infer/src/clang/cPredicates.ml @@ -131,7 +131,7 @@ let captured_variables_cxx_ref an = | _ -> [] -type t = ALVar.formula_id * (* (name, [param1,...,paramK]) *) ALVar.alexp list +type t = ALVar.formula_id * (* (name, [param1,...,paramK]) *) ALVar.alexp list [@@deriving compare] let pp_predicate fmt (_name, _arglist) = let name = ALVar.formula_id_to_string _name in diff --git a/infer/src/clang/cPredicates.mli b/infer/src/clang/cPredicates.mli index 36a4bd30e..be4f763aa 100644 --- a/infer/src/clang/cPredicates.mli +++ b/infer/src/clang/cPredicates.mli @@ -9,7 +9,7 @@ open! IStd -type t = ALVar.formula_id * ALVar.alexp list +type t = ALVar.formula_id * ALVar.alexp list [@@deriving compare] (* (name, [param1,...,paramK]) *) diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 2d6fedd46..9c07f07b8 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -28,6 +28,7 @@ type transitions = | Cond | PointerToDecl (** stmt to decl *) | Protocol (** decl to decl *) + [@@deriving compare] let is_transition_to_successor trans = match trans with @@ -61,6 +62,9 @@ type t = | EU of transitions option * t * t | EH of ALVar.alexp list * t | ET of ALVar.alexp list * transitions option * t + [@@deriving compare] + +let equal = [%compare.equal : t] let has_transition phi = match phi with @@ -596,34 +600,32 @@ let transition_decl_to_stmt d trs = let temp_res = match (trs, d) with | Body, ObjCMethodDecl (_, _, omdi) - -> omdi.omdi_body + -> [omdi.omdi_body] | Body, FunctionDecl (_, _, _, fdi) | Body, CXXMethodDecl (_, _, _, fdi, _) | Body, CXXConstructorDecl (_, _, _, fdi, _) | Body, CXXConversionDecl (_, _, _, fdi, _) | Body, CXXDestructorDecl (_, _, _, fdi, _) - -> fdi.fdi_body + -> [fdi.fdi_body] | Body, BlockDecl (_, bdi) - -> bdi.bdi_body + -> [bdi.bdi_body] | InitExpr, VarDecl (_, _, _, vdi) - -> vdi.vdi_init_expr + -> [vdi.vdi_init_expr] | InitExpr, ObjCIvarDecl (_, _, _, fldi, _) | InitExpr, FieldDecl (_, _, _, fldi) | InitExpr, ObjCAtDefsFieldDecl (_, _, _, fldi) - -> fldi.fldi_init_expr - | InitExpr, CXXMethodDecl _ - | InitExpr, CXXConstructorDecl _ - | InitExpr, CXXConversionDecl _ - | InitExpr, CXXDestructorDecl _ - -> (* requires extending to lists *) - CFrontend_config.unimplemented - "transition_decl_to_stmt: InitExpr/CXX{Method,Constructor,Conversion,Destructor}" + -> [fldi.fldi_init_expr] + | InitExpr, CXXMethodDecl (_, _, _, _, mdi) + | InitExpr, CXXConstructorDecl (_, _, _, _, mdi) + | InitExpr, CXXConversionDecl (_, _, _, _, mdi) + | InitExpr, CXXDestructorDecl (_, _, _, _, mdi) + -> List.map ~f:(fun ci -> ci.xci_init_expr) mdi.xmdi_cxx_ctor_initializers | InitExpr, EnumConstantDecl (_, _, _, ecdi) - -> ecdi.ecdi_init_expr + -> [ecdi.ecdi_init_expr] | _, _ - -> None + -> [None] in - match temp_res with Some st -> [Stmt st] | _ -> [] + List.fold ~f:(fun l e -> match e with Some st -> Stmt st :: l | _ -> l) temp_res ~init:[] let transition_decl_to_decl_via_super d = let decl_opt_to_ast_node_opt d_opt = match d_opt with Some d' -> [Decl d'] | None -> [] in diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli index 1502f0bf8..c731c3aa5 100644 --- a/infer/src/clang/cTL.mli +++ b/infer/src/clang/cTL.mli @@ -26,7 +26,7 @@ type transitions = | Cond | PointerToDecl (** stmt to decl *) | Protocol (** decl to decl *) - + [@@deriving compare] (* In formulas below prefix "E" means "exists a path" "A" means "for all path" *) @@ -63,9 +63,9 @@ type t = there exists a node defining a super class in the hierarchy of the class defined by the current node (if any) where phi holds *) | ET of ALVar.alexp list * transitions option * t - (** ET[T][l] phi <=> - there exists a descentant an of the current node such that an is of type in set T - making a transition to a node an' via label l, such that in an phi holds. *) + (** ET[T][l] phi <=> there exists a descentant an of the current node such that an is of type in set T + making a transition to a node an' via label l, such that in an phi holds. *) + [@@deriving compare] (* "set" clauses are used for defining mandatory variables that will be used by when reporting issues: eg for defining the condition. @@ -84,6 +84,8 @@ type t = *) +val equal : t -> t -> bool + type clause = | CLet of ALVar.formula_id * ALVar.t list * t (* Let clause: let id = definifion; *) diff --git a/infer/src/clang/ctl_parser_types.mli b/infer/src/clang/ctl_parser_types.mli index c465ae553..2248b435a 100644 --- a/infer/src/clang/ctl_parser_types.mli +++ b/infer/src/clang/ctl_parser_types.mli @@ -21,6 +21,8 @@ val ast_node_type : ast_node -> string val ast_node_kind : ast_node -> string +val ast_node_pointer : ast_node -> int + val ast_node_has_kind : ALVar.alexp list -> ast_node -> bool val ast_node_unique_string_id : ast_node -> string diff --git a/infer/src/clang/tableaux.ml b/infer/src/clang/tableaux.ml new file mode 100644 index 000000000..f4ae8e281 --- /dev/null +++ b/infer/src/clang/tableaux.ml @@ -0,0 +1,336 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd +module L = Logging +module CTLFormulaSet = Caml.Set.Make (CTL) + +module ClosureHashtbl = Caml.Map.Make (struct + type t = CTL.t [@@deriving compare] +end) + +(* This map associates a true/false to a formula in a node to + say if that is a good context where to evaluate the formula or not. + This is an optimization that avoids evaluation formulas where not necessary *) +type context_linter_map = bool ClosureHashtbl.t + +(* This map associate to a formula the set of its subformulae + (is state only formula, linter_condition, list of subformulae of linter_condition) *) +let closure_map : (bool * CTL.t list) ClosureHashtbl.t ref = ref ClosureHashtbl.empty + +type node_valuation_key = int * string [@@deriving compare] + +(* Given a linter and a node, a node valuation is a set of + formulae valid in that node. The formulae are subformulae of the + linter.condition, and therefore their use is to be able to + evaluate the linter condition. *) +module NodesValuationHashtbl = Caml.Map.Make (struct + type t = node_valuation_key [@@deriving compare] +end) + +type node_valuation = CTLFormulaSet.t + +let global_nodes_valuation : node_valuation NodesValuationHashtbl.t ref = + ref NodesValuationHashtbl.empty + +let init_global_nodes_valuation () = + global_nodes_valuation := NodesValuationHashtbl.empty ; + closure_map := ClosureHashtbl.empty + +let print_table_size () = + L.(debug Linters Medium) + "@\n[Size: %i]@\n" + (NodesValuationHashtbl.cardinal !global_nodes_valuation) + +let add_formula_to_valuation k s = + global_nodes_valuation := NodesValuationHashtbl.add k s !global_nodes_valuation + +let get_node_valuation k = + try NodesValuationHashtbl.find k !global_nodes_valuation + with Not_found -> CTLFormulaSet.empty + +let is_decl_allowed lcxt decl = + let decl_info = Clang_ast_proj.get_decl_tuple decl in + CLocation.should_do_frontend_check lcxt.CLintersContext.translation_unit_context + decl_info.Clang_ast_t.di_source_range + +(* true if it's an InNode formulae *) +let is_in_formula phi = match phi with CTL.InNode _ -> true | _ -> false + +(* Map initialized with false for InNode formula and true for others *) +let init_active_map () = + List.fold + ~f:(fun acc_map linter -> + let not_inf = not (is_in_formula linter.CFrontend_errors.condition) in + ClosureHashtbl.add linter.CFrontend_errors.condition not_inf acc_map) + ~init:ClosureHashtbl.empty !CFrontend_errors.parsed_linters + +(* update the context map for formulae of type InNode(tl, phi). When we + pass from a node in the list tl. The idea is that the context map tell us + when we are in a node that is a discendant of a node in tl so that is make + sense to keep evaluation phi. Otherwise we can skip the evaluation of phi and + its subformulae *) +let update_linter_context_map an linter_context_map = + let do_one_linter acc_map linter = + let phi = linter.CFrontend_errors.condition in + match phi with + | CTL.InNode (tl, _) -> ( + try + if ClosureHashtbl.find phi linter_context_map then acc_map + else + let res = Ctl_parser_types.ast_node_has_kind tl an in + (*L.(debug Linters Medium) "@\n Updating linter map for node %i with '%b'" + (Ctl_parser_types.ast_node_pointer an) res; *) + ClosureHashtbl.add phi res acc_map + with Not_found -> + Logging.die InternalError "Every linter condition should have an entry in the map." ) + | _ + -> acc_map + in + List.fold ~f:do_one_linter ~init:linter_context_map !CFrontend_errors.parsed_linters + +(* Takes phi and transform it by an equivalent formula containing +only a minimal set of operators *) +let rec normalize phi = + let open CTL in + match phi with + | True | False | Atomic _ + -> phi + | Implies (phi1, phi2) + -> normalize (Or (Not phi1, phi2)) + | Or (phi1, phi2) + -> let phi1' = normalize phi1 in + let phi2' = normalize phi2 in + Or (phi1', phi2') + | And (phi1, phi2) + -> let phi1' = normalize phi1 in + let phi2' = normalize phi2 in + And (phi1', phi2') + | Not phi1 + -> let phi1' = normalize phi1 in + Not phi1' + | AG (trans, phi1) + -> let phi1' = normalize phi1 in + Not (EF (trans, Not phi1')) + | EX (trans, phi1) + -> let phi1' = normalize phi1 in + EX (trans, phi1') + | EF (trans, phi1) + -> let phi1' = normalize phi1 in + EF (trans, phi1') + | EG (trans, phi1) + -> let phi1' = normalize phi1 in + EG (trans, phi1') + | AX (trans, phi1) + -> let phi1' = normalize phi1 in + Not (EX (trans, Not phi1')) + | AF (trans, phi1) + -> let phi1' = normalize phi1 in + Not (EG (trans, Not phi1')) + | EU (trans, phi1, phi2) + -> let phi1' = normalize phi1 in + let phi2' = normalize phi2 in + EU (trans, phi1', phi2') + | AU (trans, phi1, phi2) + -> let phi1' = normalize phi1 in + let phi2' = normalize phi2 in + Not (Or (EU (trans, Not phi2', Not (Or (phi1', phi2'))), EG (trans, phi2'))) + | EH (cl, phi1) + -> normalize (ET (cl, None, EX (Some Super, EF (Some Super, phi1)))) + | ET (tl, trs, phi1) + -> ( + let phi1' = normalize phi1 in + match trs with + | Some _ + -> EF (None, InNode (tl, EX (trs, phi1'))) + | None + -> EF (None, InNode (tl, phi1')) ) + | InNode (nl, phi1) + -> let phi1' = normalize phi1 in + InNode (nl, phi1') + +(* Given a phi0 build the list of its subformulae including itself. + The order of the list is such that, for any formula phi, its strict subformulae + occur before. The order is important for the evaluation. *) +let formula_closure phi0 = + let open CTL in + let rec do_subformula phi = + match phi with + | True | False | Atomic _ + -> [phi] + | Not phi1 + -> phi :: do_subformula phi1 + | And (phi1, phi2) | Or (phi1, phi2) | EU (_, phi1, phi2) + -> let cl1 = do_subformula phi1 in + let cl2 = do_subformula phi2 in + phi :: (cl1 @ cl2) + | EX (_, phi1) | EF (_, phi1) | EG (_, phi1) | InNode (_, phi1) + -> phi :: do_subformula phi1 + | AG _ | AX _ | AF _ | AU _ | EH _ | ET _ | Implies _ + -> Logging.die InternalError "@\n Failing with formula @\n %a@\n" CTL.Debug.pp_formula phi + in + let cl0 = do_subformula phi0 in + let cl0' = List.rev cl0 in + List.fold + ~f:(fun acc e -> if List.mem acc e ~equal:CTL.equal then acc else acc @ [e]) + ~init:[] cl0' + +(* check if there is a formula phi in the set of valid formula of +a successor *) +let exists_formula_in_successor_nodes an checker trans phi = + (*L.(debug Linters Medium) "@\n Successor nodes of %i: " (Ctl_parser_types.ast_node_pointer an) ;*) + let succs = + match trans with + | Some l + -> (* L.(debug Linters Medium) " (passing by '%a' transition) " CTL.Debug.pp_transition trans ;*) + CTL.next_state_via_transition an l + | None + -> (*L.(debug Linters Medium) " (passing by None) " ;*) + Ctl_parser_types.get_direct_successor_nodes an + in + (*List.iter + ~f:(fun an' -> L.(debug Linters Medium) " [%i] " (Ctl_parser_types.ast_node_pointer an')) + succs ;*) + List.exists + ~f:(fun an' -> + let node_pointer = Ctl_parser_types.ast_node_pointer an' in + let key = (node_pointer, checker) in + let succ_sat_set = get_node_valuation key in + (*print_formula_set succ_sat_set "SUCC_SAT_SET" ;*) + CTLFormulaSet.mem phi succ_sat_set) + succs + +(* Given a node an and a closure cl, returns the subset of valid formulae of + cl in an. The hipothesis is that you have constructed the set of valid formulae +for the successors of the node an *) +let add_valid_formulae an checker lcxt cl = + let open CTL in + (*let name = Ctl_parser_types.ast_node_kind an in + let pointer = Ctl_parser_types.ast_node_pointer an in *) + let add_in_set phi acc_set = + (* L.(debug Linters Medium) + "@\n **** In (%i, %s) ADDING FORMULA **** @\n %a@\n@\n" pointer name CTL.Debug.pp_formula + phi ; *) + CTLFormulaSet.add phi acc_set + in + let is_valid phi acc_set = CTLFormulaSet.mem phi acc_set in + let do_formula acc_set phi = + (* L.(debug Linters Medium) + "@\n In (%i, %s) Dealing with formula @\n %a@\n" pointer name CTL.Debug.pp_formula phi ; + L.(debug Linters Medium) "@\n ---------------------------- @\n" ;*) + match phi with + | True + -> add_in_set phi acc_set + | False + -> acc_set + | Atomic _ + -> if Option.is_some (eval_formula phi an lcxt) then add_in_set phi acc_set else acc_set + | And (phi1, phi2) when is_valid phi1 acc_set && is_valid phi2 acc_set + -> add_in_set phi acc_set + | Or (phi1, phi2) when is_valid phi1 acc_set || is_valid phi2 acc_set + -> add_in_set phi acc_set + | Not phi1 when not (is_valid phi1 acc_set) + -> add_in_set phi acc_set + | InNode (tl, phi1) when Ctl_parser_types.ast_node_has_kind tl an && is_valid phi1 acc_set + -> add_in_set phi acc_set + | EX (trans, phi1) when exists_formula_in_successor_nodes an checker trans phi1 + -> add_in_set phi acc_set + | EF (trans, phi1) + when is_valid phi1 acc_set || exists_formula_in_successor_nodes an checker trans phi + -> add_in_set phi acc_set + | EG (trans, phi1) + when is_valid phi1 acc_set && exists_formula_in_successor_nodes an checker trans phi + -> add_in_set phi acc_set + | EU (trans, phi1, phi2) + when is_valid phi2 acc_set + || is_valid phi1 acc_set && exists_formula_in_successor_nodes an checker trans phi + -> add_in_set phi acc_set + | AG _ | AX _ | AF _ | AU _ | EH _ | ET _ | Implies _ + -> Logging.die InternalError + "@\n We should not have operators AG, AX, AF, AU, EH, ET.\n Failing with formula @\n %a@\n" + CTL.Debug.pp_formula phi + | _ + -> acc_set + in + List.fold ~f:do_formula cl ~init:CTLFormulaSet.empty + +(* true if it's a formulae that does not contain temporal operators + and can be decided in a single node *) +let rec is_state_only_formula phi = + let open CTL in + match phi with + | True | False | Atomic _ + -> (*L.(debug Linters Medium) "@\n ****** FOUND state_only_formula ***** @\n" ;*) true + | Not phi1 + -> is_state_only_formula phi1 + | And (phi1, phi2) | Or (phi1, phi2) | Implies (phi1, phi2) + -> is_state_only_formula phi1 && is_state_only_formula phi2 + | InNode (_, phi1) + -> is_state_only_formula phi1 + | AX _ | EX _ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | EH _ | ET _ + -> false + +(* Report an issue provided that a declaration is allowed + (i.e., it's in the analized file )*) +let report_issue an lcxt linter (*npo_condition*) = + let open Ctl_parser_types in + let open CFrontend_errors in + (*let name = Ctl_parser_types.ast_node_kind an in + let pointer = Ctl_parser_types.ast_node_pointer an in + L.(debug Linters Medium) + "@\n@\n@\n ***** In (%i, %s) Reporting because we found @\n%a@\n@\n@\n@\n" pointer name + CTL.Debug.pp_formula linter.condition ;*) + let loc = CFrontend_checkers.location_from_an lcxt an in + let should_report = match an with Decl dec -> is_decl_allowed lcxt dec | Stmt _ -> true in + if should_report then fill_issue_desc_info_and_log lcxt an linter.issue_desc linter.def_file loc + +let check_linter_map linter_map_contex phi = + try ClosureHashtbl.find phi linter_map_contex + with Not_found -> + Logging.die InternalError "@\n ERROR: linter_map must have an entry for each formula" + +(* skip the evaluation of a InNode because an is not among the set tl *) +let skip_evaluation_InNode_formula an phi = + match phi with + | CTL.InNode (tl, _) when not (Ctl_parser_types.ast_node_has_kind tl an) + -> true + | _ + -> false + +(* Build valuation, i.e. set of valid subformula for a pair (node, checker) *) +let build_valuation an lcxt linter_map_context = + let open CFrontend_errors in + let node_pointer = Ctl_parser_types.ast_node_pointer an in + (*L.(debug Linters Medium) + "@\n@\n ******** Tableaux called for node %i ******** @\n@\n" node_pointer ;*) + let do_one_check linter = + (*transition_set_in_formula := TransitionSet.empty ; + build_transition_set npo_condition ; *) + let normalized_condition = normalize linter.condition in + let is_state_only, cl = + try ClosureHashtbl.find normalized_condition !closure_map + with Not_found -> + let cl' = formula_closure normalized_condition in + let is_state_only = is_state_only_formula normalized_condition in + (*print_closure cl' ; *) + closure_map := ClosureHashtbl.add normalized_condition (is_state_only, cl') !closure_map ; + (is_state_only, cl') + in + if not (is_state_only && skip_evaluation_InNode_formula an normalized_condition) then + let sat_set = add_valid_formulae an linter.issue_desc.id lcxt cl in + (*L.progress " [Set Size: %i] @\n" (CTLFormulaSet.cardinal sat_set);*) + if CTLFormulaSet.mem normalized_condition sat_set then report_issue an lcxt linter ; + add_formula_to_valuation (node_pointer, linter.issue_desc.id) sat_set + in + List.iter + ~f:(fun (linter: linter) -> + if CIssue.should_run_check linter.issue_desc.CIssue.mode + && check_linter_map linter_map_context linter.condition + then do_one_check linter) + !parsed_linters diff --git a/infer/src/clang/tableaux.mli b/infer/src/clang/tableaux.mli new file mode 100644 index 000000000..f0b72f63b --- /dev/null +++ b/infer/src/clang/tableaux.mli @@ -0,0 +1,28 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +module CTLFormulaSet : Caml.Set.S with type elt = CTL.t + +module ClosureHashtbl : Caml.Map.S with type key = CTL.t + +type context_linter_map = bool ClosureHashtbl.t + +val init_global_nodes_valuation : unit -> unit + +val init_active_map : unit -> bool ClosureHashtbl.t + +val update_linter_context_map : + Ctl_parser_types.ast_node -> context_linter_map -> context_linter_map + +val build_valuation : + Ctl_parser_types.ast_node -> CLintersContext.context -> context_linter_map -> unit + +val is_decl_allowed : CLintersContext.context -> Clang_ast_t.decl -> bool + +val print_table_size : unit -> unit