From c3e16dbdbc66704414efb3c04e1115dcf2d370aa Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Wed, 27 Nov 2019 04:42:31 -0800 Subject: [PATCH] [AL] Remove unused tableaux evaluation Summary: The tableaux evaluation was an experiment and it was turned off because of bad perf. Let's kill it to clear up the code. Reviewed By: jvillard Differential Revision: D18708388 fbshipit-source-id: 099f5a3d3 --- infer/src/al/AL.ml | 77 +++--- infer/src/al/ALIssues.ml | 3 +- infer/src/al/tableaux.ml | 357 --------------------------- infer/src/al/tableaux.mli | 28 --- infer/src/clang/cFrontend_config.ml | 3 - infer/src/clang/cFrontend_config.mli | 2 - 6 files changed, 31 insertions(+), 439 deletions(-) delete mode 100644 infer/src/al/tableaux.ml delete mode 100644 infer/src/al/tableaux.mli diff --git a/infer/src/al/AL.ml b/infer/src/al/AL.ml index bdbf93b2f..7955c74e0 100644 --- a/infer/src/al/AL.ml +++ b/infer/src/al/AL.ml @@ -207,29 +207,23 @@ let compute_if_context (context : CLintersContext.context) stmt = : CLintersContext.if_context ) -let call_tableaux linters cxt an map_active = - if CFrontend_config.tableaux_evaluation then Tableaux.build_valuation linters an cxt map_active - - -let rec do_frontend_checks_stmt linters (context : CLintersContext.context) - (map_act : Tableaux.context_linter_map) stmt = +let rec do_frontend_checks_stmt linters (context : CLintersContext.context) stmt = let open Clang_ast_t in 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 = + let do_all_checks_on_stmts context stmt = ( match stmt with | DeclStmt (_, _, decl_list) -> - List.iter ~f:(do_frontend_checks_decl linters context map_active) decl_list + List.iter ~f:(do_frontend_checks_decl linters context) decl_list | BlockExpr (_, _, _, decl) -> - List.iter ~f:(do_frontend_checks_decl linters context map_active) [decl] + List.iter ~f:(do_frontend_checks_decl linters context) [decl] | _ -> () ) ; - do_frontend_checks_stmt linters context map_active stmt + do_frontend_checks_stmt linters context stmt in ALIssues.invoke_set_of_checkers_on_node linters context an ; (* The map should be visited when we enter the node before visiting children *) - let map_active = Tableaux.update_linter_context_map linters an map_act in let stmt_context_list = match stmt with | ObjCAtSynchronizedStmt (_, stmt_list) -> @@ -262,21 +256,13 @@ let rec do_frontend_checks_stmt linters (context : CLintersContext.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 linters 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 linters cxt an map_active ) + ~f:(fun (cxt, stmts) -> List.iter ~f:(do_all_checks_on_stmts cxt) stmts) stmt_context_list (* Visit nodes via a transition *) -and do_frontend_checks_via_transition linters context map_active an trans = +and do_frontend_checks_via_transition linters context an trans = let succs = CTL.next_state_via_transition an trans in List.iter ~f:(fun an' -> @@ -286,20 +272,18 @@ and do_frontend_checks_via_transition linters context map_active an trans = CTL.Debug.pp_transition (Some trans) ;*) match an' with | Ctl_parser_types.Decl d -> - do_frontend_checks_decl linters context map_active d + do_frontend_checks_decl linters context d | Ctl_parser_types.Stmt st -> - do_frontend_checks_stmt linters context map_active st ) + do_frontend_checks_stmt linters context st ) succs -and do_frontend_checks_decl linters (context : CLintersContext.context) - (map_act : Tableaux.context_linter_map) decl = +and do_frontend_checks_decl linters (context : CLintersContext.context) decl = let open Clang_ast_t in if CAst_utils.is_implicit_decl decl then () (* do not analyze implicit declarations *) else 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 linters an map_act in match decl with | FunctionDecl _ | CXXMethodDecl _ @@ -307,41 +291,36 @@ and do_frontend_checks_decl linters (context : CLintersContext.context) | CXXConversionDecl _ | CXXDestructorDecl _ | BlockDecl _ - | ObjCMethodDecl _ -> + | ObjCMethodDecl _ -> ( let context' = CLintersContext.update_current_method context decl in ALIssues.invoke_set_of_checkers_on_node linters 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 linters context' map_active an CTL.Parameters ; - ( match CAst_utils.get_method_body_opt decl with + do_frontend_checks_via_transition linters context' an CTL.Parameters ; + match CAst_utils.get_method_body_opt decl with | Some stmt -> - do_frontend_checks_stmt linters context' map_active stmt + do_frontend_checks_stmt linters context' stmt | None -> - () ) ; - call_tableaux linters context' an map_active + () ) | ObjCImplementationDecl (_, _, decls, _, _) | ObjCInterfaceDecl (_, _, decls, _, _) -> ALIssues.invoke_set_of_checkers_on_node linters context an ; let context' = {context with current_objc_class= Some decl} in - List.iter ~f:(do_frontend_checks_decl linters context' map_active) decls ; - call_tableaux linters context' an map_active + List.iter ~f:(do_frontend_checks_decl linters context') decls | ObjCCategoryImplDecl (_, _, decls, _, _) | ObjCCategoryDecl (_, _, decls, _, _) -> ALIssues.invoke_set_of_checkers_on_node linters context an ; let context' = {context with current_objc_category= Some decl} in - List.iter ~f:(do_frontend_checks_decl linters context' map_active) decls ; - call_tableaux linters context' an map_active + List.iter ~f:(do_frontend_checks_decl linters context') decls | ObjCProtocolDecl (_, _, decls, _, _) -> ALIssues.invoke_set_of_checkers_on_node linters context an ; let context' = {context with current_objc_protocol= Some decl} in - List.iter ~f:(do_frontend_checks_decl linters context' map_active) decls ; - call_tableaux linters context' an map_active - | _ -> + List.iter ~f:(do_frontend_checks_decl linters context') decls + | _ -> ( ALIssues.invoke_set_of_checkers_on_node linters context an ; - ( match Clang_ast_proj.get_decl_context_tuple decl with + match Clang_ast_proj.get_decl_context_tuple decl with | Some (decls, _) -> - List.iter ~f:(do_frontend_checks_decl linters context map_active) decls + List.iter ~f:(do_frontend_checks_decl linters context) decls | None -> - () ) ; - call_tableaux linters context an map_active + () ) let context_with_ck_set context decl_list = @@ -361,6 +340,12 @@ let linters_files = List.dedup_and_sort ~compare:String.compare (find_linters_files () @ Config.linters_def_file) +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.source_file + decl_info.Clang_ast_t.di_source_range + + let do_frontend_checks (trans_unit_ctx : CFrontend_config.translation_unit_context) ast = ALIssues.issue_log := IssueLog.empty ; L.(debug Capture Quiet) @@ -379,15 +364,13 @@ let do_frontend_checks (trans_unit_ctx : CFrontend_config.translation_unit_conte if Config.print_active_checkers then L.progress "Linting file %a, active linters: @\n%a@\n" SourceFile.pp source_file ALIssues.pp_linters 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 allowed_decls = List.filter ~f:(Tableaux.is_decl_allowed context) decl_list in + let allowed_decls = List.filter ~f:(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 parsed_linters in ALIssues.invoke_set_of_checkers_on_node parsed_linters context (Ctl_parser_types.Decl ast) ; - List.iter ~f:(do_frontend_checks_decl parsed_linters context active_map) allowed_decls ; + List.iter ~f:(do_frontend_checks_decl parsed_linters context) allowed_decls ; IssueLog.store !ALIssues.issue_log ~dir:Config.lint_issues_dir_name ~file: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 diff --git a/infer/src/al/ALIssues.ml b/infer/src/al/ALIssues.ml index 702ce8b5b..c8dd5a8ad 100644 --- a/infer/src/al/ALIssues.ml +++ b/infer/src/al/ALIssues.ml @@ -540,6 +540,5 @@ let invoke_set_of_checkers_on_node parsed_linters context an = Because depending on the formula it may give an error at line -1 *) () | _ -> - if not CFrontend_config.tableaux_evaluation then - invoke_set_of_parsed_checkers_an parsed_linters context an ) ; + 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/al/tableaux.ml b/infer/src/al/tableaux.ml deleted file mode 100644 index 52bf6c56c..000000000 --- a/infer/src/al/tableaux.ml +++ /dev/null @@ -1,357 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd -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 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 Caml.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.source_file - 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 parsed_linters = - List.fold - ~f:(fun acc_map linter -> - let not_inf = not (is_in_formula linter.ALIssues.condition) in - ClosureHashtbl.add linter.ALIssues.condition not_inf acc_map ) - ~init:ClosureHashtbl.empty 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 parsed_linters an linter_context_map = - let do_one_linter acc_map linter = - let phi = linter.ALIssues.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 Caml.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 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') - | InObjCClass (phi1, phi2) -> - let phi1' = normalize phi1 in - let phi2' = normalize phi2 in - InObjCClass (phi1', phi2') - - -(* 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) | InObjCClass (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 - | InObjCClass (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) | InObjCClass (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 ALIssues 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 = ALUtils.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 ~witness:an ~current_node:an linter.issue_desc loc - - -let check_linter_map linter_map_contex phi = - try ClosureHashtbl.find phi linter_map_contex - with Caml.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 parsed_linters an lcxt linter_map_context = - let open ALIssues 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 Caml.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.issue_type.IssueType.unique_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.issue_type.IssueType.unique_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/al/tableaux.mli b/infer/src/al/tableaux.mli deleted file mode 100644 index 35be2357e..000000000 --- a/infer/src/al/tableaux.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -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 : ALIssues.linter list -> bool ClosureHashtbl.t - -val update_linter_context_map : - ALIssues.linter list -> Ctl_parser_types.ast_node -> context_linter_map -> context_linter_map - -val build_valuation : - ALIssues.linter list - -> Ctl_parser_types.ast_node - -> CLintersContext.context - -> context_linter_map - -> unit - -val is_decl_allowed : CLintersContext.context -> Clang_ast_t.decl -> bool diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index e528afbf9..a7f9db0a9 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -138,6 +138,3 @@ let reset_global_state () = sil_types_map := Clang_ast_extend.TypePointerMap.empty ; procedures_attempted := 0 ; procedures_failed := 0 - - -let tableaux_evaluation = false diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index 654ea59c1..6a2971996 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -119,5 +119,3 @@ val get_fresh_block_index : unit -> int val reset_block_counter : unit -> unit val reset_global_state : unit -> unit - -val tableaux_evaluation : bool