diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml deleted file mode 100644 index 0b57d0e94..000000000 --- a/infer/src/checkers/codeQuery.ml +++ /dev/null @@ -1,218 +0,0 @@ -(* - * Copyright (c) 2013 - 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! Utils - -(** Module for code queries. *) - -module L = Logging -module F = Format - -let verbose = false - -let parse_query s = - let buf = Lexing.from_string s in - try - match CodequeryParser.query CodequeryLexer.token buf with - | None -> - L.stdout "empty rule@."; - assert false - | Some query -> - if verbose then L.stdout "%a@." CodeQueryAst.pp_query query; - query - with - | Parsing.Parse_error -> - let lexbuf = Bytes.to_string buf.Lexing.lex_buffer in - L.stdout "@.parsing stops on line %d: \n\n%s@." !CodequeryLexer.line_number lexbuf; - assert false - -let query_ast = - lazy (match Config.code_query with None -> parse_query "x(y)" | Some s -> parse_query s) - -module Err = struct - (** Update the summary with stats from the checker. *) - let update_summary proc_name proc_desc = - let old_summ = Specs.get_summary_unsafe "codeQuery" proc_name in - let nodes = IList.map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in - let specs = - let spec = - { Specs.pre = Specs.Jprop.Prop (1, Prop.prop_emp); - posts = []; - visited = Specs.Visitedset.empty - } in - [(Specs.spec_normalize spec)] in - let new_summ = { old_summ with - Specs.attributes = - { old_summ.Specs.attributes with - ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc }; - nodes = nodes; - payload = - { old_summ.Specs.payload with - Specs.preposts = Some specs; } - } in - Specs.add_summary proc_name new_summ - - let add_error_to_spec proc_name s node loc = - Checkers.ST.pname_add proc_name "codequery" "active"; (* force creation of .specs files *) - State.set_node node; - let exn = Exceptions.Codequery (Localise.verbatim_desc s) in - Reporting.log_error proc_name ~loc: (Some loc) exn -end - -(** Matcher for rules. *) -module Match = struct - type value = - | Vfun of Procname.t - | Vval of Exp.t - - let pp_value fmt = function - | Vval e -> F.fprintf fmt "%a" (Sil.pp_exp pe_text) e - | Vfun pn -> F.fprintf fmt "%s" (Procname.to_string pn) - - let value_equal v1 v2 = match v1, v2 with - | Vval e1, Vval e2 -> Exp.equal e1 e2 - | Vval _, _ -> false - | _, Vval _ -> false - | Vfun pn1, Vfun pn2 -> Procname.equal pn1 pn2 - - let init_env () = Hashtbl.create 1 - - let env_copy env = Hashtbl.copy env - - let env_add env id value = - try - let value' = Hashtbl.find env id in - value_equal value value' - with Not_found -> - Hashtbl.add env id value; - true - let pp_env fmt env = - let pp_item id value = - F.fprintf fmt "%s=%a " id pp_value value in - Hashtbl.iter pp_item env - - let exp_match env ae value = match ae, value with - | CodeQueryAst.Null, Vval e -> Exp.equal e Exp.zero - | CodeQueryAst.Null, _ -> false - | CodeQueryAst.ConstString s, (Vfun pn) -> string_contains s (Procname.to_string pn) - | CodeQueryAst.ConstString _, _ -> false - | CodeQueryAst.Ident id, x -> - env_add env id x - - let rec exp_list_match env ael vl = match ael, vl with - | [], [] -> true - | [], _:: _ -> false - | _:: _, [] -> false - | ae:: ael', v:: vl' -> - if exp_match env ae v then exp_list_match env ael' vl' - else false - - let opt_match match_elem env x_opt y = match x_opt with - | None -> true - | Some x -> match_elem env x y - - let binop_match op1 op2 = match op1, op2 with - | Binop.Eq, "==" -> true - | Binop.Ne, "!=" -> true - | _ -> false - - let rec cond_match env idenv cond (ae1, op, ae2) = match cond with - | Exp.BinOp (bop, _e1, _e2) -> - let e1 = Idenv.expand_expr idenv _e1 in - let e2 = Idenv.expand_expr idenv _e2 in - binop_match bop op && exp_match env ae1 (Vval e1) && exp_match env ae2 (Vval e2) - | Exp.UnOp (Unop.LNot, (Exp.BinOp (Binop.Eq, e1, e2)), _) -> - cond_match env idenv (Exp.BinOp (Binop.Ne, e1, e2)) (ae1, op, ae2) - | Exp.UnOp (Unop.LNot, (Exp.BinOp (Binop.Ne, e1, e2)), _) -> - cond_match env idenv (Exp.BinOp (Binop.Eq, e1, e2)) (ae1, op, ae2) - | _ -> false - - (** Iterate over the instructions of the linearly succ nodes. *) - let rec iter_succ_nodes node iter = - match Cfg.Node.get_succs node with - | [node'] -> - let instrs = Cfg.Node.get_instrs node in - IList.iter (fun instr -> iter (node', instr)) instrs; - iter_succ_nodes node' iter - | [] -> () - | _:: _ -> () - - let linereader = Printer.LineReader.create () - - let print_action env action proc_name node loc = match action with - | CodeQueryAst.Noaction -> - L.stdout "%a@." pp_env env - | CodeQueryAst.Source source_range_opt -> - let x, y = match source_range_opt with - | None -> 10, 10 - | Some (x, y) -> x, y in - L.stdout "%a@." (Checkers.PP.pp_loc_range linereader x y) loc - | CodeQueryAst.Error s_opt -> - let err_name = match s_opt with - | None -> "codequery" - | Some s -> s in - Err.add_error_to_spec proc_name err_name node loc - - let rec match_query show env idenv caller_pn (rule, action) proc_name node instr = - match rule, instr with - | CodeQueryAst.Call (ae1, ae2), Sil.Call (_, Exp.Const (Const.Cfun pn), _, loc, _) -> - if exp_match env ae1 (Vfun caller_pn) && exp_match env ae2 (Vfun pn) then - begin - if show then print_action env action proc_name node loc; - true - end - else false - | CodeQueryAst.Call _, _ -> false - | CodeQueryAst.MethodCall (ae1, ae2, ael_opt), - Sil.Call (_, Exp.Const (Const.Cfun pn), (_e1, _) :: params, - loc, { CallFlags.cf_virtual = true }) -> - let e1 = Idenv.expand_expr idenv _e1 in - let vl = IList.map (function _e, _ -> Vval (Idenv.expand_expr idenv _e)) params in - if exp_match env ae1 (Vval e1) && exp_match env ae2 (Vfun pn) && opt_match exp_list_match env ael_opt vl then - begin - if show then print_action env action proc_name node loc; - true - end - else false - | CodeQueryAst.MethodCall _, _ -> false - | CodeQueryAst.If (ae1, op, ae2, body_rule), Sil.Prune (cond, loc, true_branch, _) -> - if true_branch && cond_match env idenv cond (ae1, op, ae2) then - begin - let found = ref false in - let iter (_, instr') = - let env' = env_copy env in - if not !found - && match_query false env' idenv caller_pn (body_rule, action) proc_name node instr' - then found := true in - iter_succ_nodes node iter; - let line_contains_null () = - match Printer.LineReader.from_loc linereader loc with - | None -> false - | Some s -> string_contains "null" s in - if !found && line_contains_null () (* TODO: this replaces lack of typing where null and 0 and false are the same *) then - begin - L.stdout "conditional %a@." (Sil.pp_exp pe_text) cond; - print_action env action proc_name node loc - end; - !found - end - else false - | CodeQueryAst.If _, _ -> false - -end - -let code_query_callback { Callbacks.proc_desc; idenv; proc_name } = - let do_instr node instr = - let env = Match.init_env () in - let _found = - Match.match_query true env idenv proc_name (Lazy.force query_ast) proc_name node instr in - () in - if verbose then L.stdout "code_query_callback on %a@." Procname.pp proc_name; - Cfg.Procdesc.iter_instrs do_instr proc_desc; - Err.update_summary proc_name proc_desc diff --git a/infer/src/checkers/codeQuery.mli b/infer/src/checkers/codeQuery.mli deleted file mode 100644 index f7a2a3540..000000000 --- a/infer/src/checkers/codeQuery.mli +++ /dev/null @@ -1,14 +0,0 @@ -(* - * Copyright (c) 2013 - 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! Utils - -(** Module for code queries. *) - -val code_query_callback : Callbacks.proc_callback_t diff --git a/infer/src/checkers/codeQueryAst.ml b/infer/src/checkers/codeQueryAst.ml deleted file mode 100644 index 44e8c7eb8..000000000 --- a/infer/src/checkers/codeQueryAst.ml +++ /dev/null @@ -1,57 +0,0 @@ -(* - * Copyright (c) 2013 - 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! Utils - -(** Abstract synyax tree for code queries. *) - -module L = Logging -module F = Format - -type expr = - | Null - | Ident of string - | ConstString of string - -type rule = - | Call of expr * expr - | MethodCall of expr * expr * (expr list option) - | If of expr * string * expr * rule - -type action = - | Noaction - | Source of (int * int) option (* (x,y) represents x lines before and y lines after the source location *) - | Error of string option (* print an error *) - -type query = - rule * action - -let pp_action fmt = function - | Noaction -> () - | Source None -> F.fprintf fmt "@source" - | Source (Some(x, y)) -> F.fprintf fmt "@source(%d,%d)" x y - | Error None -> F.fprintf fmt "@error" - | Error (Some s) -> F.fprintf fmt "@error(%s)" s - -let pp_expr fmt = function - | Null -> F.fprintf fmt "null" - | Ident s -> F.fprintf fmt "%s" s - | ConstString s -> F.fprintf fmt "%s" s - -let pp_expr_list_option fmt = function - | None -> F.fprintf fmt "*" - | Some el -> pp_comma_seq pp_expr fmt el - -let rec pp_rule fmt = function - | Call (ae1, ae2) -> F.fprintf fmt "%a(%a)" pp_expr ae1 pp_expr ae2 - | MethodCall (ae1, ae2, elo) -> F.fprintf fmt "%a.%a(%a)" pp_expr ae1 pp_expr ae2 pp_expr_list_option elo - | If (ae1, s, ae2, rule) -> F.fprintf fmt "if(%a %s %a) ... %a" pp_expr ae1 s pp_expr ae2 pp_rule rule - -let pp_query fmt (rule, action) = - F.fprintf fmt "%a; %a" pp_rule rule pp_action action diff --git a/infer/src/checkers/codequeryLexer.mll b/infer/src/checkers/codequeryLexer.mll deleted file mode 100644 index 1db3c1224..000000000 --- a/infer/src/checkers/codequeryLexer.mll +++ /dev/null @@ -1,80 +0,0 @@ -(* - * Copyright (c) 2013 - 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 CodequeryParser - -let line_number = ref 1 -let parentheses = ref 0 - -let parsed_tokens = Buffer.create 1 -let log lexbuf = Buffer.add_char parsed_tokens ' '; Buffer.add_string parsed_tokens (Lexing.lexeme lexbuf) -let reset_log () = Buffer.reset parsed_tokens -let get_log () = Buffer.contents parsed_tokens - -} - -let lowerletter = ['a'-'z'] -let upperletter = ['A'-'Z'] - -let underscore = '_' -let minus = '-' -let letter = lowerletter | upperletter - -let digit = ['0'-'9'] -let number = digit* | digit+ '.' digit* | digit* '.' digit+ - -let identifier = (letter | underscore) (letter | underscore | digit)* - -let const_string_digit = letter | underscore | digit | ' ' | '.' | ',' | '(' | ')' | '[' | ']' -let const_string = '{' const_string_digit* '}' - -let single_quote = '\'' - -let space = [' ' '\t'] -let newline = '\n' - -rule token = parse - | space { log lexbuf; token lexbuf } - | newline { log lexbuf; incr line_number; token lexbuf } - | '.' { log lexbuf; DOT } - | ';' { log lexbuf; SEMICOLON } - | ':' { log lexbuf; COLON } - | ',' { log lexbuf; COMMA } - | '`' { log lexbuf; REV_QUOTE } - | '\'' { log lexbuf; SINGLE_QUOTE } - | '\"' { log lexbuf; DOUBLE_QUOTE } - | '%' { log lexbuf; PERCENT } - | '&' { log lexbuf; AMPERSAND } - | '!' { log lexbuf; EXCLAMATION } - | '=' { log lexbuf; EQUAL } - | "==" { log lexbuf; EQUALEQUAL } - | "!=" { log lexbuf; EXCLAMATIONEQUAL } - | '-' { log lexbuf; MINUS } - | '+' { log lexbuf; PLUS } - | '<' { log lexbuf; LEFT_CHEVRON } - | '>' { log lexbuf; RIGHT_CHEVRON } - | '(' { log lexbuf; incr parentheses; LEFT_PARENTHESIS } - | ')' { log lexbuf; decr parentheses; RIGHT_PARENTHESIS } - | '[' { log lexbuf; LEFT_SQBRACKET } - | ']' { log lexbuf; RIGHT_SQBRACKET } - | '*' { log lexbuf; STAR } - | '|' { log lexbuf; PIPE } - | '/' { log lexbuf; SLASH } - | '\\' { log lexbuf; BACKSLASH } - | "if" { log lexbuf; IF } - | "..." { log lexbuf; DOTDOTDOT } - | "@source" { log lexbuf; SOURCE } - | "@error" { log lexbuf; ERROR } - | number as n { log lexbuf; NUMBER n } - | identifier as s { log lexbuf; IDENT (s) } - | const_string as s { log lexbuf; CONST_STRING (String.sub s 1 (String.length s - 2)) } - | eof { EOF } - diff --git a/infer/src/checkers/codequeryParser.mly b/infer/src/checkers/codequeryParser.mly deleted file mode 100644 index 12a0faea9..000000000 --- a/infer/src/checkers/codequeryParser.mly +++ /dev/null @@ -1,81 +0,0 @@ -/* - * Copyright (c) 2013 - 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. - */ - -%{ - -%} - -%token DOT SEMICOLON COLON COMMA SINGLE_QUOTE DOUBLE_QUOTE REV_QUOTE -%token PERCENT AMPERSAND EXCLAMATION EQUAL MINUS PLUS EQUALEQUAL EXCLAMATIONEQUAL -%token LEFT_CHEVRON RIGHT_CHEVRON LEFT_PARENTHESIS RIGHT_PARENTHESIS LEFT_SQBRACKET RIGHT_SQBRACKET -%token STAR PIPE SLASH BACKSLASH -%token IF DOTDOTDOT SOURCE ERROR - -%token HEXA -%token NUMBER -%token IDENT -%token CONST_STRING -%token ATTRIBUTE - -%token EOF - -%start query -%type query - -%% - -ident: - | IDENT { $1 } -; - -expr: - | ident { if $1 = "null" then CodeQueryAst.Null else CodeQueryAst.Ident $1 } - | CONST_STRING { CodeQueryAst.ConstString $1 } -; - -condition: - | expr EQUALEQUAL expr { ($1, "==", $3) } - | expr EXCLAMATIONEQUAL expr { ($1, "!=", $3) } -; - -param_element: - | expr { $1 } -; - -param_element_list_nonempty: - | param_element { [$1] } - | param_element COMMA param_element_list_nonempty { $1 :: $3 } -; -param_element_list: - | { [] } - | param_element_list_nonempty { $1 } -; - -call_params: - | STAR { None } - | param_element_list { Some $1 } -; - -rule: - | expr LEFT_PARENTHESIS expr RIGHT_PARENTHESIS { CodeQueryAst.Call ($1, $3) } - | expr DOT expr LEFT_PARENTHESIS call_params RIGHT_PARENTHESIS { CodeQueryAst.MethodCall($1, $3, $5) } - | IF LEFT_PARENTHESIS condition RIGHT_PARENTHESIS DOTDOTDOT rule { let x, y, z = $3 in CodeQueryAst.If (x, y, z, $6) } -; - -action: - | { CodeQueryAst.Noaction } - | SOURCE SEMICOLON { CodeQueryAst.Source None } - | SOURCE LEFT_PARENTHESIS NUMBER COMMA NUMBER RIGHT_PARENTHESIS SEMICOLON { CodeQueryAst.Source (Some (int_of_string $3, int_of_string $5)) } - | ERROR SEMICOLON { CodeQueryAst.Error None } - | ERROR LEFT_PARENTHESIS ident RIGHT_PARENTHESIS SEMICOLON { CodeQueryAst.Error (Some $3) } - -query: - | rule SEMICOLON action { Some ($1,$3) } - | EOF { None } -; diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index e469562ae..671ce1b76 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -33,7 +33,6 @@ let active_procedure_checkers () = SqlChecker.callback_sql, false; Eradicate.callback_eradicate, Config.eradicate; BoundedCallTree.checker, Config.crashcontext; - CodeQuery.code_query_callback, Config.code_query <> None; Checkers.callback_check_field_access, false; ImmutableChecker.callback_check_immutable_cast, checkers_enabled; RepeatedCallsChecker.callback_check_repeated_calls, checkers_enabled;