diff --git a/infer/src/IR/cfg.ml b/infer/src/IR/cfg.ml index 5af42b370..b3792c894 100644 --- a/infer/src/IR/cfg.ml +++ b/infer/src/IR/cfg.ml @@ -136,7 +136,7 @@ module Node = struct let old_pdesc = Procname.Hash.find old_procs pname in let changed = (* in continue_capture mode keep the old changed bit *) - (!Config.continue_capture && old_pdesc.pd_attributes.ProcAttributes.changed) || + (Config.continue_capture && old_pdesc.pd_attributes.ProcAttributes.changed) || not (pdescs_eq old_pdesc new_pdesc) in new_pdesc.pd_attributes.changed <- changed with Not_found -> () in @@ -937,13 +937,13 @@ let remove_abducted_retvars p = let remove_locals (curr_f : Procdesc.t) p = let names_of_locals = IList.map (get_name_of_local curr_f) (Procdesc.get_locals curr_f) in let names_of_locals' = match !Config.curr_language with - | Config.C_CPP -> (* in ObjC to deal with block we need to remove static locals *) + | Config.Clang -> (* in ObjC to deal with block we need to remove static locals *) let names_of_static_locals = get_name_of_objc_static_locals curr_f p in let names_of_block_locals = get_name_of_objc_block_locals p in names_of_block_locals @ names_of_locals @ names_of_static_locals | _ -> names_of_locals in let removed, p' = Prop.deallocate_stack_vars p names_of_locals' in - (removed, if !Config.angelic_execution then remove_abducted_retvars p' else p') + (removed, if Config.angelic_execution then remove_abducted_retvars p' else p') let remove_formals (curr_f : Procdesc.t) p = let pname = Procdesc.get_proc_name curr_f in @@ -1158,7 +1158,7 @@ let inline_java_synthetic_methods cfg = let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg : cfg) = inline_java_synthetic_methods cfg; if save_sources then save_source_files cfg; - if !Config.incremental_procs then + if Config.incremental_procs then begin match load_cfg_from_file filename with | Some old_cfg -> Node.mark_unchanged_pdescs cfg old_cfg diff --git a/infer/src/IR/procname.ml b/infer/src/IR/procname.ml index 7bd6dccbb..2e2dc2c14 100644 --- a/infer/src/IR/procname.ml +++ b/infer/src/IR/procname.ml @@ -255,11 +255,11 @@ let get_method = function (** Return the language of the procedure. *) let get_language = function | ObjC_Cpp _ -> - Config.C_CPP + Config.Clang | C _ -> - Config.C_CPP + Config.Clang | Block _ -> - Config.C_CPP + Config.Clang | Java _ -> Config.Java diff --git a/infer/src/IR/sil.ml b/infer/src/IR/sil.ml index 2702f2d46..d71296158 100644 --- a/infer/src/IR/sil.ml +++ b/infer/src/IR/sil.ml @@ -238,7 +238,7 @@ module Subtype = struct | NORMAL -> "" let pp f (t, flag) = - if !Config.print_types then + if Config.print_types then match t with | Exact -> F.fprintf f "%s" (flag_to_string flag) @@ -428,7 +428,7 @@ module Subtype = struct and in case return the updated subtype [st1] *) let case_analysis (c1, st1) (c2, st2) f is_interface = let f = check_subtype f in - if (!Config.subtype_multirange) then + if Config.subtype_multirange then get_subtypes (c1, st1) (c2, st2) f is_interface else case_analysis_basic (c1, st1) (c2, st2) f @@ -1662,7 +1662,7 @@ module HpredSet = Set.Make (** Begin change color if using diff printing, return updated printenv and change status *) let color_pre_wrapper pe f x = - if !Config.print_using_diff && pe.pe_kind != PP_TEXT then begin + if Config.print_using_diff && pe.pe_kind != PP_TEXT then begin let color = pe.pe_cmap_norm (Obj.repr x) in if color != pe.pe_color then begin (if pe.pe_kind == PP_HTML then Io_infer.Html.pp_start_color else Latex.pp_color) f color; @@ -1681,7 +1681,7 @@ let color_post_wrapper changed pe f = (** Print a sequence with difference mode if enabled. *) let pp_seq_diff pp pe0 f = - if not !Config.print_using_diff + if not Config.print_using_diff then pp_comma_seq pp f else let rec doit = function @@ -1780,7 +1780,7 @@ let ptr_kind_string = function | Pk_objc_autoreleasing -> "__autoreleasing *" let java () = !Config.curr_language = Config.Java -let eradicate_java () = !Config.eradicate && java () +let eradicate_java () = Config.eradicate && java () (** convert a dexp to a string *) let rec dexp_to_string = function @@ -1878,7 +1878,7 @@ and attribute_to_string pe = function | Racquire, Rlock -> "LOCKED" | Rrelease, Rlock -> "UNLOCKED" in let str_vpath = - if !Config.trace_error + if Config.trace_error then pp_to_string (pp_vpath pe) ra.ra_vpath else "" in name ^ (str_binop pe Lt) ^ Procname.to_string ra.ra_pname ^ ":" ^ @@ -1927,7 +1927,7 @@ and pp_const pe f = function (** Pretty print a type. Do nothing by default. *) and pp_typ pe f te = - if !Config.print_types then pp_typ_full pe f te else () + if Config.print_types then pp_typ_full pe f te else () and pp_struct_typ pe pp_base f struct_typ = match struct_typ.struct_name with | Some name when false -> @@ -2004,7 +2004,7 @@ and _pp_exp pe0 pp_t f e0 = | Const c -> F.fprintf f "%a" (pp_const pe) c | Cast (typ, e) -> F.fprintf f "(%a)%a" pp_t typ pp_exp e | UnOp (op, e, _) -> F.fprintf f "%s%a" (str_unop op) pp_exp e - | BinOp (op, Const c, e2) when !Config.smt_output -> print_binop_stm_output (Const c) op e2 + | BinOp (op, Const c, e2) when Config.smt_output -> print_binop_stm_output (Const c) op e2 | BinOp (op, e1, e2) -> F.fprintf f "(%a %s %a)" pp_exp e1 (str_binop pe op) pp_exp e2 | Lvar pv -> Pvar.pp pe f pv | Lfield (e, fld, _) -> F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld @@ -2569,7 +2569,7 @@ let pp_inst pe f inst = F.fprintf f "%s%s%s" (str_binop pe Lt) str (str_binop pe Gt) let pp_inst_if_trace pe f inst = - if !Config.trace_error then pp_inst pe f inst + if Config.trace_error then pp_inst pe f inst (** pretty print a strexp with an optional predicate env *) let rec pp_sexp_env pe0 envo f se = @@ -3779,7 +3779,7 @@ let exp_add_offsets exp offsets = (** Convert all the lseg's in sigma to nonempty lsegs. *) let sigma_to_sigma_ne sigma : (atom list * hpred list) list = - if !Config.nelseg then + if Config.nelseg then let f eqs_sigma_list hpred = match hpred with | Hpointsto _ | Hlseg(Lseg_NE, _, _, _, _) | Hdllseg(Lseg_NE, _, _, _, _, _, _) -> let g (eqs, sigma) = (eqs, hpred:: sigma) in diff --git a/infer/src/backend/CommandLineOption.ml b/infer/src/backend/CommandLineOption.ml new file mode 100644 index 000000000..9170853b7 --- /dev/null +++ b/infer/src/backend/CommandLineOption.ml @@ -0,0 +1,378 @@ +(* + * Copyright (c) 2016 - 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. + *) + +(** Definition and parsing of command line arguments *) + +open! Utils + +module F = Format + + +(* Each command line option may appear in the --help list of any executable, these tags are used to + specify which executables for which an option will be documented. *) +type exe = A | C | J | L | P | T + +let current_exe = + match Filename.basename Sys.executable_name with + | "InferAnalyze" -> A + | "InferClang" -> C + | "InferJava" -> J + | "InferLLVM" -> L + | "InferPrint" -> P + | _ -> T + + +type desc = { long: string; short: string; meta: string; doc: string; spec: Arg.spec } + +let dashdash long = + match long with + | "" | "--" -> long + | _ -> "--" ^ long + +let short_meta {short; meta; spec} = + String.concat " " + ((if short = "" then [] else ["| -" ^ short]) @ + (match spec with + | Arg.Symbol (symbols, _) -> + ["{ " ^ (String.concat " | " symbols) ^ " }" ^ meta] + | _ -> + if meta = "" then [] else ["<" ^ meta ^ ">"])) + +let left_length long short_meta = + (String.length (dashdash long)) + (String.length short_meta) + +let max_left_length limit current ({long; spec} as desc) = + let short_meta = + match spec with + | Arg.Symbol _ -> short_meta {desc with spec = Arg.Unit (fun () -> ())} + | _ -> short_meta desc in + let length = left_length long short_meta in + if length > limit then current else max current length + +let xdesc {long; short; spec; doc} = + let key long short = + match long, short with + | "", "" -> "" + | "--", _ -> "--" + | "", _ -> "-" ^ short + | _ -> "--" ^ long + in + let xspec long spec = + match spec with + (* translate Symbol to String for better formatting of --help messages *) + | Arg.Symbol (symbols, action) -> + Arg.String (fun arg -> + if IList.mem ( = ) arg symbols then + action arg + else + raise (Arg.Bad (F.sprintf "wrong argument '%s'; option '%s' expects one of: %s" + arg (dashdash long) (String.concat " | " symbols))) + ) + | _ -> + spec + in + (key long short, xspec long spec, doc) + +let pad_and_xform left_width desc = + match desc with + | {doc = ""} -> + xdesc desc + | {long; doc} -> + let short_meta = short_meta desc in + let gap = left_width - (left_length long short_meta) in + if gap < 0 then + xdesc {desc with doc = short_meta ^ "\n" ^ (String.make (4 + left_width) ' ') ^ doc} + else + xdesc {desc with doc = short_meta ^ (String.make (gap + 1) ' ') ^ doc} + +let align ?(limit=max_int) desc_list = + let left_width = IList.fold_left (max_left_length limit) 0 desc_list in + (IList.map (pad_and_xform left_width) desc_list) + + +let check_no_duplicates desc_list = + let rec check_for_duplicates_ = function + | [] | [_] -> + true + | (x, _, _) :: (y, _, _) :: _ when x <> "" && x = y -> + failwith ("Multiple definitions of command line option: " ^ x) + | _ :: tl -> + check_for_duplicates_ tl + in + check_for_duplicates_ (IList.sort (fun (x, _, _) (y, _, _) -> String.compare x y) desc_list) + + +let full_desc_list = ref [] + +let exe_desc_lists = [(A, ref []); (C, ref []); (J, ref []); (L, ref []); (P, ref []); (T, ref [])] + +(* add desc to all desc_lists for the purposes of parsing, include desc in --help only for exes *) +let add exes desc = + full_desc_list := desc :: !full_desc_list ; + IList.iter (fun (exe, desc_list) -> + let desc = + if IList.mem ( = ) exe exes then + desc + else + {desc with meta = ""; doc = ""} in + desc_list := desc :: !desc_list + ) exe_desc_lists + +let mk ?(deprecated=[]) ?(exes=[]) + ~long ?(short="") ~default ~meta doc ~default_to_string ~mk_setter ~mk_spec = + let variable = ref default in + let closure = mk_setter variable in + let setter str = + try closure str + with _ -> raise (Arg.Bad ("bad value " ^ str ^ " for flag " ^ long)) in + let spec = mk_spec setter in + let doc = + let default_string = default_to_string default in + if default_string = "" then doc + else doc ^ " (default: " ^ default_string ^ ")" in + let desc = {long; short; meta; doc; spec} in + (* add desc for long option, with documentation (which includes any short option) for exes *) + add exes desc ; + (* add desc for short option only for parsing, without documentation *) + if short <> "" then + add [] {desc with long = ""; meta = ""; doc = ""} ; + (* add desc for deprecated options only for parsing, without documentation *) + IList.iter (fun deprecated -> + add [] {desc with long = ""; short = deprecated; meta = ""; doc = ""} + ) deprecated ; + variable + +type 'a t = + ?deprecated:string list -> long:Arg.key -> ?short:Arg.key -> + ?exes:exe list -> ?meta:string -> Arg.doc -> + 'a + +let mk_set var value ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + let setter () = var := value in + ignore( + mk ~deprecated ~long ?short ~default:() ?exes ~meta doc + ~default_to_string:(fun () -> "") + ~mk_setter:(fun _ _ -> setter ()) + ~mk_spec:(fun _ -> Arg.Unit setter) ) + +let mk_option ?(default=None) ?(default_to_string=fun _ -> "") ~f + ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + mk ~deprecated ~long ?short ~default ?exes ~meta doc + ~default_to_string + ~mk_setter:(fun var str -> var := f str) + ~mk_spec:(fun set -> Arg.String set) + +let mk_bool ?(deprecated_no=[]) ?(default=false) ?(f=fun b -> b) + ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + let nolong = + let len = String.length long in + if len > 3 && String.sub long 0 3 = "no-" then + String.sub long 3 (len - 3) + else + "no-" ^ long + and noshort = + Option.map (fun short -> + let len = String.length short in + if len > 1 && String.sub short 0 1 = "n" then + String.sub short 1 (len - 1) + else + "n" ^ short + ) short + in + let doc nolong = + match noshort with + | Some noshort -> doc ^ " (Conversely: --" ^ nolong ^ " | -" ^ noshort ^ ")" + | None -> doc ^ " (Conversely: --" ^ nolong ^ ")" + in + let doc, nodoc = + if not default then + ("Activates: " ^ doc nolong, "") + else + ("", "Deactivates: " ^ doc long) in + let default_to_string _ = "" in + let mk_spec set = Arg.Unit (fun () -> set "") in + let var = + mk ~long ?short ~deprecated ~default ?exes + ~meta doc ~default_to_string ~mk_setter:(fun var _ -> var := f true) ~mk_spec in + ignore( + mk ~long:nolong ?short:noshort ~deprecated:deprecated_no ~default:(not default) ?exes + ~meta nodoc ~default_to_string ~mk_setter:(fun _ _ -> var := f false) ~mk_spec ); + var + +let mk_bool_group ?(deprecated_no=[]) ?(default=false) + ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc children = + let f b = + IList.iter (fun child -> child := b) children ; + b + in + mk_bool ~deprecated ~deprecated_no ~default ~long ?short ~f ?exes ~meta doc + +let mk_int ~default ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + mk ~deprecated ~long ?short ~default ?exes ~meta doc + ~default_to_string:string_of_int + ~mk_setter:(fun var str -> var := (int_of_string str)) + ~mk_spec:(fun set -> Arg.String set) + +let mk_float ~default ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + mk ~deprecated ~long ?short ~default ?exes ~meta doc + ~default_to_string:string_of_float + ~mk_setter:(fun var str -> var := (float_of_string str)) + ~mk_spec:(fun set -> Arg.String set) + +let mk_string ~default ?(f=fun s -> s) ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + mk ~deprecated ~long ?short ~default ?exes ~meta doc + ~default_to_string:(fun s -> s) + ~mk_setter:(fun var str -> var := f str) + ~mk_spec:(fun set -> Arg.String set) + +let mk_string_opt ?default ?(f=fun s -> s) ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + let default_to_string = function Some s -> s | None -> "" in + let f s = Some (f s) in + mk_option ~deprecated ~long ?short ~default ~default_to_string ~f ?exes ~meta doc + +let mk_string_list ?(default=[]) ?(f=fun s -> s) + ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + mk ~deprecated ~long ?short ~default ?exes ~meta doc + ~default_to_string:(String.concat ", ") + ~mk_setter:(fun var str -> var := (f str) :: !var) + ~mk_spec:(fun set -> Arg.String set) + +let mk_symbol ~default ~symbols ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + let strings = IList.map fst symbols in + let sym_to_str = IList.map (fun (x,y) -> (y,x)) symbols in + let of_string str = IList.assoc string_equal str symbols in + let to_string sym = IList.assoc ( = ) sym sym_to_str in + mk ~deprecated ~long ?short ~default ?exes ~meta doc + ~default_to_string:(fun s -> to_string s) + ~mk_setter:(fun var str -> var := of_string str) + ~mk_spec:(fun set -> Arg.Symbol (strings, set)) + +let mk_symbol_opt ~symbols ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + let strings = IList.map fst symbols in + let of_string str = IList.assoc string_equal str symbols in + mk ~deprecated ~long ?short ~default:None ?exes ~meta doc + ~default_to_string:(fun _ -> "") + ~mk_setter:(fun var str -> var := Some (of_string str)) + ~mk_spec:(fun set -> Arg.Symbol (strings, set)) + +let mk_symbol_seq ?(default=[]) ~symbols ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + let strings = IList.map fst symbols in + let sym_to_str = IList.map (fun (x,y) -> (y,x)) symbols in + let of_string str = IList.assoc string_equal str symbols in + let to_string sym = IList.assoc ( = ) sym sym_to_str in + mk ~deprecated ~long ?short ~default ?exes ~meta:(" ,-separated sequence" ^ meta) doc + ~default_to_string:(fun syms -> String.concat " " (IList.map to_string syms)) + ~mk_setter:(fun var str_seq -> var := IList.map of_string (Str.split (Str.regexp ",") str_seq)) + ~mk_spec:(fun set -> Arg.Symbol (strings, set)) + +let anon_fun = ref (fun arg -> raise (Arg.Bad ("unexpected anonymous argument: " ^ arg))) + +let mk_anon () = + let anon = ref [] in + anon_fun := (fun arg -> anon := arg :: !anon) ; + anon + + + +(** [sep_char] is used to separate elements of argv when encoded into environment variables *) +let sep_char = '^' + +let encode_argv_to_env argv = + String.concat (String.make 1 sep_char) + (IList.filter (fun arg -> + not (String.contains arg sep_char) + || ( + F.eprintf "Ignoring unsupported option containing '%c' character: %s@\n" sep_char arg ; + false + ) + ) argv) + +let decode_env_to_argv env = + Str.split (Str.regexp_string (String.make 1 sep_char)) env + +let prepend_to_argv args = + let cl_args = match Array.to_list Sys.argv with _ :: tl -> tl | [] -> [] in + (Sys.executable_name, args @ cl_args) + +(** [prefix_before_rest (prefix @ ["--" :: rest])] is [prefix] where "--" is not in [prefix]. *) +let prefix_before_rest args = + let rec prefix_before_rest_ rev_keep = function + | [] | "--" :: _ -> IList.rev rev_keep + | keep :: args -> prefix_before_rest_ (keep :: rev_keep) args in + prefix_before_rest_ [] args + + +let parse env_var exe_usage = + let curr_speclist = ref [] + and full_speclist = ref [] + in + let usage_msg = exe_usage current_exe + in + let curr_usage status = + Arg.usage !curr_speclist usage_msg ; + exit status + and full_usage status = + Arg.usage !full_speclist usage_msg ; + exit status + in + let help_desc_list = + [ { long = "help"; short = ""; meta = ""; spec = Arg.Unit (fun () -> curr_usage 0); + doc = "Display this list of options" } + ; { long = "help-full"; short = ""; meta = ""; spec = Arg.Unit (fun () -> full_usage 0); + doc = "Display the full list of options, including internal and experimental options" } + ] in + let section heading speclist = + let norm k = + let len = String.length k in + if len > 3 && String.sub k 0 3 = "no-" then String.sub k 3 (len - 3) else k in + let compare_specs {long = x} {long = y} = + match x, y with + | "--", "--" -> 0 + | "--", _ -> 1 + | _, "--" -> -1 + | _ -> String.compare (norm x) (norm y) in + let sort speclist = IList.sort compare_specs speclist in + let add_heading speclist = + match heading with + | Some heading -> + let doc = "\n " ^ heading ^ "\n" in + { doc; long = ""; short = ""; meta = ""; spec = Arg.Unit (fun () -> ()) } :: speclist + | None -> + speclist in + let suppress_help speclist = + ("-help", Arg.Unit (fun () -> raise (Arg.Bad "unknown option '-help'")), "") :: speclist in + suppress_help (align ~limit:32 (add_heading (sort speclist))) + in + let curr_desc_list = IList.assoc ( = ) current_exe exe_desc_lists + in + (* curr_speclist includes args for current exe with docs, and all other args without docs, so + that all args can be parsed, but --help and parse failures only show external args for + current exe *) + curr_speclist := (section None (help_desc_list @ !curr_desc_list)) + ; + assert( check_no_duplicates !curr_speclist ) + ; + full_speclist := (section None (help_desc_list @ !full_desc_list)) + ; + let env_args = decode_env_to_argv (try Unix.getenv env_var with Not_found -> "") in + (* begin transitional support for INFERCLANG_ARGS *) + let c_args = + Str.split (Str.regexp_string (String.make 1 ':')) + (try Unix.getenv "INFERCLANG_ARGS" with Not_found -> "") in + let env_args = c_args @ env_args in + (* end transitional support for INFERCLANG_ARGS *) + let exe_name, env_cl_args = prepend_to_argv env_args in + Unix.putenv env_var (encode_argv_to_env (prefix_before_rest env_cl_args)) ; + (try + Arg.parse_argv (Array.of_list (exe_name :: env_cl_args)) !curr_speclist !anon_fun usage_msg + with + | Arg.Bad usage_msg -> Pervasives.prerr_string usage_msg; exit 2 + | Arg.Help usage_msg -> Pervasives.print_string usage_msg; exit 0 + ); + curr_usage diff --git a/infer/src/backend/CommandLineOption.mli b/infer/src/backend/CommandLineOption.mli new file mode 100644 index 000000000..10dfcc0b8 --- /dev/null +++ b/infer/src/backend/CommandLineOption.mli @@ -0,0 +1,96 @@ +(* + * Copyright (c) 2016 - 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. + *) + +(** Definition and parsing of command line arguments *) + +open! Utils + +type exe = A | C | J | L | P | T + +val current_exe : exe + +(** The [mk_*] functions declare command line options, while [parse] parses then according to the + declared options. + + The arguments of the declaration functions are largely treated uniformly: + - [long] declares the option [--long] + - [short] declares the option [-short] as an alias + - [deprecated] declares the option [-key] as an alias, for each [key] in [deprecated] + - [default] specifies the default value + - [default_to_string] is used to document the default value + - [f] specifies a transformation to be performed on the parsed value before setting the config + variable + - [symbols] is an association list sometimes used in place of [f] + - [exes] declares that the option should be included in the external documentation (--help) for + each [exe] in [exes], otherwise it appears only in --help-full + - [meta] is a meta-variable naming the parsed value for documentation purposes + - a documentation string +*) +type 'a t = + ?deprecated:string list -> long:string -> ?short:string -> + ?exes:exe list -> ?meta:string -> string -> + 'a + +(** [mk_set variable value] defines a command line option which sets [variable] to [value]. *) +val mk_set : 'a ref -> 'a -> unit t + +val mk_option : + ?default:'a option -> ?default_to_string:('a option -> string) -> f:(string -> 'a option) -> + 'a option ref t + +(** [mk_bool long short doc] defines a [bool ref] set by the command line flag [--long] (and + [-short]), and cleared by the flag [--no-long] (and [-nshort]). If [long] already has a "no-", + or [short] nas an "n", prefix, then the existing prefixes will instead be removed. The default + value is [false] unless overridden by [~default:true]. The [doc] string will be prefixed with + either "Activates:" or "Deactivates:", so should be phrased accordingly. *) +val mk_bool : ?deprecated_no:string list -> ?default:bool -> ?f:(bool -> bool) -> bool ref t + +(** [mk_bool_group children] behaves as [mk_bool] with the addition that all the [children] are also + set. A child can be unset by including "--no-child" later in the arguments. *) +val mk_bool_group : ?deprecated_no:string list -> ?default:bool -> (bool ref list -> bool ref) t + +val mk_int : default:int -> int ref t + +val mk_float : default:float -> float ref t + +val mk_string : default:string -> ?f:(string -> string) -> string ref t + +val mk_string_opt : ?default:string -> ?f:(string -> string) -> string option ref t + +(** [mk_string_list] defines a [string list ref], initialized to [[]] unless overridden by + [~default]. Each argument of an occurrence of the option will be prepended to the list, so the + final value will be in the reverse order they appeared on the command line. *) +val mk_string_list : + ?default:string list -> ?f:(string -> string) -> string list ref t + +(** [mk_symbol long symbols] defines a command line flag [--long ] where [(,_)] is + an element of [symbols]. *) +val mk_symbol : default:'a -> symbols:(string * 'a) list -> 'a ref t + +(** [mk_symbol_opt] is similar to [mk_symbol] but defaults to [None]. *) +val mk_symbol_opt : symbols:(string * 'a) list -> 'a option ref t + +(** [mk_symbol_seq long symbols] defines a command line flag [--long ] where + [] is a comma-separated sequence of []s such that [(,_)] is an + element of [symbols]. *) +val mk_symbol_seq : ?default:'a list -> symbols:(string * 'a) list -> 'a list ref t + +(** [mk_anon ()] defines a [string list ref] of the anonymous command line arguments, in the reverse + order they appeared on the command line. *) +val mk_anon : + unit -> + string list ref + +(** [parse env_var exe_usage] parses command line arguments as specified by preceding calls to the + [mk_*] functions, and returns a function that prints the usage message and help text then exits. + The decoded value of environment variable [env_var] is prepended to [Sys.argv] before parsing. + Therefore arguments passed on the command line supercede those specified in the environment + variable. WARNING: If an argument appears both in the environment variable and on the command + line, it will be interpreted twice. *) +val parse : string -> (exe -> Arg.usage_msg) -> (int -> 'a) diff --git a/infer/src/backend/DB.ml b/infer/src/backend/DB.ml index f77c4fb08..9da1f910f 100644 --- a/infer/src/backend/DB.ml +++ b/infer/src/backend/DB.ml @@ -71,8 +71,8 @@ let source_file_to_string fname = exception No_project_root let project_root () = - match !Config.project_root with - | None -> L.err "No -project_root option passed@."; raise No_project_root + match Config.project_root with + | None -> L.err "No --project-root option passed@."; raise No_project_root | Some path -> path (* Checking if the path exists may be needed only in some cases, hence the flag check_exists *) @@ -122,10 +122,10 @@ let source_dir_get_internal_file source_dir extension = Filename.concat source_dir fname let captured_dir () = - Filename.concat !Config.results_dir Config.captured_dir_name + Filename.concat Config.results_dir Config.captured_dir_name let sources_dir () = - Filename.concat !Config.results_dir Config.sources_dir_name + Filename.concat Config.results_dir Config.sources_dir_name (** get the source directory corresponding to a source file *) let source_dir_from_source_file source_file = @@ -295,7 +295,7 @@ module Results_dir = struct (** convert a path to a filename *) let path_to_filename pk path = let base = match pk with - | Abs_root -> !Config.results_dir + | Abs_root -> Config.results_dir | Abs_source_dir -> let dir = source_dir_from_source_file !current_source in source_dir_to_string dir @@ -307,7 +307,7 @@ module Results_dir = struct (** initialize the results directory *) let init () = - create_dir !Config.results_dir; + create_dir Config.results_dir; create_dir (specs_dir ()); create_dir (path_to_filename Abs_root [Config.attributes_dir_name]); create_dir (path_to_filename Abs_root [Config.sources_dir_name]); diff --git a/infer/src/backend/SymOp.ml b/infer/src/backend/SymOp.ml index ec60c0669..243a22b02 100644 --- a/infer/src/backend/SymOp.ml +++ b/infer/src/backend/SymOp.ml @@ -38,10 +38,10 @@ let pp_failure_kind fmt = function (** Count the number of symbolic operations *) (** Timeout in seconds for each function *) -let timeout_seconds = ref (!Config.seconds_per_iteration *. (float_of_int !Config.iterations)) +let timeout_seconds = ref (Config.seconds_per_iteration *. (float_of_int Config.iterations)) (** Timeout in SymOps *) -let timeout_symops = ref (!Config.symops_per_iteration * !Config.iterations) +let timeout_symops = ref (Config.symops_per_iteration * Config.iterations) let get_timeout_seconds () = !timeout_seconds diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 27532043d..dee8f48eb 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -211,7 +211,7 @@ let mk_rule_lsls_ls k1 k2 impl_ok1 impl_ok2 para = r_condition = condition } let mk_rules_for_sll (para : Sil.hpara) : rule list = - if not !Config.nelseg then + if not Config.nelseg then begin let pts_pts = mk_rule_ptspts_ls true true para in let pts_pels = mk_rule_ptsls_ls Sil.Lseg_PE true false para in @@ -384,7 +384,7 @@ let mk_rule_dlldll_dll k1 k2 impl_ok1 impl_ok2 para = r_condition = condition } let mk_rules_for_dll (para : Sil.hpara_dll) : rule list = - if not !Config.nelseg then + if not Config.nelseg then begin let pts_pts = mk_rule_ptspts_dll true true para in let pts_pedll = mk_rule_ptsdll_dll Sil.Lseg_PE true false para in @@ -1026,7 +1026,7 @@ let check_observer_is_unsubscribed_deallocation prop e = match Prop.get_observer_attribute prop e with | Some Sil.Aobserver -> (match pvar_opt with - | Some pvar when !Config.nsnotification_center_checker_backend -> + | Some pvar when Config.nsnotification_center_checker_backend -> L.d_strln (" ERROR: Object " ^ (Pvar.to_string pvar) ^ " is being deallocated while still registered in a notification center"); let desc = Localise.desc_registered_observer_being_deallocated pvar loc in @@ -1109,8 +1109,8 @@ let check_junk ?original_prop pname tenv prop = match resource with | Sil.Rmemory Sil.Mobjc -> should_raise_objc_leak hpred | Sil.Rmemory Sil.Mnew | Sil.Rmemory Sil.Mnew_array - when !Config.curr_language = Config.C_CPP -> - Mleak_buckets.should_raise_cpp_leak () + when !Config.curr_language = Config.Clang -> + Mleak_buckets.should_raise_cpp_leak | _ -> None in let exn_retain_cycle cycle = let cycle_dotty = get_retain_cycle_dotty original_prop cycle in @@ -1137,7 +1137,7 @@ let check_junk ?original_prop pname tenv prop = ignore_cycle, exn_retain_cycle cycle | Some _, Sil.Rmemory Sil.Mobjc | Some _, Sil.Rmemory Sil.Mnew - | Some _, Sil.Rmemory Sil.Mnew_array when !Config.curr_language = Config.C_CPP -> + | Some _, Sil.Rmemory Sil.Mnew_array when !Config.curr_language = Config.Clang -> ml_bucket_opt = None, exn_leak | Some _, Sil.Rmemory _ -> !Config.curr_language = Config.Java, exn_leak | Some _, Sil.Rignore -> true, exn_leak @@ -1160,7 +1160,7 @@ let check_junk ?original_prop pname tenv prop = (* None attribute only reported if it's the first one *) IList.mem attr_opt_equal alloc_attribute !leaks_reported in let ignore_leak = - !Config.allowleak || ignore_resource || is_undefined || already_reported () in + !Config.allow_leak || ignore_resource || is_undefined || already_reported () in let report_and_continue = !Config.curr_language = Config.Java || !Config.footprint in let report_leak () = diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index c30602375..904a90bf6 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -321,7 +321,7 @@ let generic_strexp_abstract try let matched, footprint_part, matchings_cur_fp' = match_select_next matchings_cur_fp in let n = IList.length (snd matchings_cur_fp') + 1 in - if !Config.trace_absarray then (L.d_strln ("Num of fp candidates " ^ (string_of_int n))); + if Config.trace_absarray then (L.d_strln ("Num of fp candidates " ^ (string_of_int n))); let strexp_data = StrexpMatch.get_data matched in let p1, changed = do_abstract footprint_part p0 strexp_data in if changed then (p1, true) @@ -331,7 +331,8 @@ let generic_strexp_abstract let rec find_then_abstract bound p0 = if bound = 0 then p0 else begin - if !Config.trace_absarray then (L.d_strln ("Applying " ^ abstraction_name ^ " to"); Prop.d_prop p0; L.d_ln (); L.d_ln ()); + if Config.trace_absarray then + (L.d_strln ("Applying " ^ abstraction_name ^ " to"); Prop.d_prop p0; L.d_ln (); L.d_ln ()); let matchings_cur_fp = find_strexp_to_abstract p0 in let p1, changed = match_abstract p0 matchings_cur_fp in if changed then find_then_abstract (bound - 1) p1 else p0 @@ -443,19 +444,21 @@ let strexp_can_abstract ((_, se, typ) : StrexpMatch.strexp_data) : bool = (** This function abstracts a strexp *) let strexp_do_abstract footprint_part p ((path, se_in, _) : StrexpMatch.strexp_data) : Prop.normal Prop.t * bool = - if !Config.trace_absarray && footprint_part then (L.d_str "strexp_do_abstract (footprint)"; L.d_ln ()); - if !Config.trace_absarray && not footprint_part then (L.d_str "strexp_do_abstract (nonfootprint)"; L.d_ln ()); + if Config.trace_absarray && footprint_part then + (L.d_str "strexp_do_abstract (footprint)"; L.d_ln ()); + if Config.trace_absarray && not footprint_part then + (L.d_str "strexp_do_abstract (nonfootprint)"; L.d_ln ()); let prune_and_blur d_keys keep blur path keep_keys blur_keys = let p2, changed2 = - if !Config.trace_absarray then (L.d_str "keep "; d_keys keep_keys; L.d_ln ()); + if Config.trace_absarray then (L.d_str "keep "; d_keys keep_keys; L.d_ln ()); keep p path keep_keys in let p3, changed3 = if blur_keys == [] then (p2, false) else begin - if !Config.trace_absarray then (L.d_str "blur "; d_keys blur_keys; L.d_ln ()); + if Config.trace_absarray then (L.d_str "blur "; d_keys blur_keys; L.d_ln ()); blur p2 path blur_keys end in - if !Config.trace_absarray then (L.d_strln "Returns"; Prop.d_prop p3; L.d_ln (); L.d_ln ()); + if Config.trace_absarray then (L.d_strln "Returns"; Prop.d_prop p3; L.d_ln (); L.d_ln ()); (p3, changed2 || changed3) in let prune_and_blur_indices = prune_and_blur Sil.d_exp_list keep_only_indices blur_array_indices in @@ -484,7 +487,7 @@ let strexp_do_abstract let keep_ksel = IList.filter should_keep ksel in let keep_keys = IList.map fst keep_ksel in let keep_keys' = if keep_keys == [] then default_keys else keep_keys in - if !Config.trace_absarray then (L.d_str "keep "; d_keys keep_keys'; L.d_ln ()); + if Config.trace_absarray then (L.d_str "keep "; d_keys keep_keys'; L.d_ln ()); abstract keep_keys' [] in let do_array_reexecution esel = (* array case re-execution: remove and blur constant and primed indices *) diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml index dad15c60d..36293d8f9 100644 --- a/infer/src/backend/buckets.ml +++ b/infer/src/backend/buckets.ml @@ -24,12 +24,14 @@ let check_nested_loop path pos_opt = let loop_visits_log = ref [] in let in_nested_loop () = match !loop_visits_log with | true :: true :: _ -> - if !verbose then L.d_strln "in nested loop"; + if verbose then L.d_strln "in nested loop"; true (* last two loop visits were entering loops *) | _ -> false in let do_node_caller node = match Cfg.Node.get_kind node with | Cfg.Node.Prune_node (b, (Sil.Ik_dowhile | Sil.Ik_for | Sil.Ik_while), _) -> - (* if !verbose then L.d_strln ((if b then "enter" else "exit") ^ " node " ^ (string_of_int (Cfg.Node.get_id node))); *) + (* if verbose then *) + (* L.d_strln ((if b then "enter" else "exit") ^ " node " *) + (* ^ (string_of_int (Cfg.Node.get_id node))); *) loop_visits_log := b :: !loop_visits_log | _ -> () in let do_any_node _level _node = @@ -129,7 +131,7 @@ let check_access access_opt de_opt = let classify_access desc access_opt de_opt is_nullable = let default_bucket = if is_nullable then Localise.BucketLevel.b1 else Localise.BucketLevel.b5 in - let show_in_message = !Config.show_buckets in + let show_in_message = Config.show_buckets in match check_access access_opt de_opt with | None -> Localise.error_desc_set_bucket desc default_bucket show_in_message | Some bucket -> Localise.error_desc_set_bucket desc bucket show_in_message diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 0b4c96ddb..0feb3d766 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -54,7 +54,7 @@ let get_procedure_definition exe_env proc_name = (idenv, tenv, proc_name, proc_desc, language)) (Exe_env.get_proc_desc exe_env proc_name) -let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.C_CPP +let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.Clang (** Invoke all registered procedure callbacks on the given procedure. *) let iterate_procedure_callbacks exe_env caller_pname = diff --git a/infer/src/backend/clusterMakefile.ml b/infer/src/backend/clusterMakefile.ml index 5bcee503f..65ebe89de 100644 --- a/infer/src/backend/clusterMakefile.ml +++ b/infer/src/backend/clusterMakefile.ml @@ -34,14 +34,14 @@ let cluster_should_be_analyzed cluster = let modified = DB.file_was_updated_after_start (DB.filename_from_string fname) in if modified && - !Config.developer_mode + Config.developer_mode then L.stdout "Modified: %s@." fname; modified in begin match in_ondemand_config with | Some b -> (* ondemand config file is specified *) b - | None when !Config.reactive_mode -> + | None when Config.reactive_mode -> check_modified () | None -> true @@ -53,7 +53,7 @@ let pp_prolog fmt clusters = Sys.executable_name (Escape.escape_map (fun c -> if c = '#' then Some "\\#" else None) - !Config.results_dir); + Config.results_dir); F.fprintf fmt "CLUSTERS="; IList.iteri @@ -64,7 +64,7 @@ let pp_prolog fmt clusters = F.fprintf fmt "@.@.default: test@.@.all: test@.@."; F.fprintf fmt "test: $(CLUSTERS)@."; - if !Config.show_progress_bar then F.fprintf fmt "\techo \"\"@." + if Config.show_progress_bar then F.fprintf fmt "\techo \"\"@." let pp_epilog fmt () = F.fprintf fmt "@.clean:@.\trm -f $(CLUSTERS)@." diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index a1c776233..243bbcd70 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -8,457 +8,1010 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -module F = Format;; +open! Utils -(* Initialization *) +(** Configuration values: either constant, determined at compile time, or set at startup + time by system calls, environment variables, or command line options *) -F.set_margin 100 +module CLOpt = CommandLineOption +module F = Format -let set_minor_heap_size nMb = (* increase the minor heap size to speed up gc *) - let ctrl = Gc.get () in - let oneMb = 1048576 in - let new_size = max ctrl.Gc.minor_heap_size (nMb * oneMb) - in Gc.set { ctrl with Gc.minor_heap_size = new_size };; -set_minor_heap_size 1 +type language = Clang | Java -let from_env_variable var_name = - try - let _ = Sys.getenv var_name in true - with Not_found -> false +let string_of_language = function + | Java -> "Java" + | Clang -> "C_CPP" -let get_env_variable var_name = - try - let v = Sys.getenv var_name in - if v = "" then None else Some v - with Not_found -> None +type clang_lang = C | CPP | OBJC | OBJCPP + +type os_type = Unix | Win32 | Cygwin + +type zip_library = { + zip_filename: string; + zip_channel: Zip.in_file Lazy.t; + models: bool; +} + + +(** Constant configuration values *) + +(** If true, a precondition with e.g. index 3 in an array does not require the caller to + have index 3 too this mimics what happens with direct access to the array without a + procedure call, where the index is simply materialized if not there *) +let allow_missing_index_in_proc_call = true + +let anonymous_block_num_sep = "______" + +let anonymous_block_prefix = "__objc_anonymous_block_" + +let assign = "<\"Assign\">" let attributes_dir_name = "attributes" -let captured_dir_name = "captured" -let sources_dir_name = "sources" -let specs_dir_name = "specs" -let perf_stats_prefix = "perf_stats" + let backend_stats_dir_name = "backend_stats" -let frontend_stats_dir_name = "frontend_stats" -let reporting_stats_dir_name = "reporting_stats" + +(** If true, a procedure call succeeds even when there is a bound error this mimics what + happens with a direct array access where an error is produced and the analysis + continues *) +let bound_error_allowed_in_procedure_call = true + +let captured_dir_name = "captured" + +let default_failure_name = "ASSERTION_FAILURE" let default_in_zip_results_dir = "infer" -let default_buck_out = "buck-out" +(** Dotty output filename **) +let dotty_output = "icfg.dot" -let proc_stats_filename = "proc_stats.json" +(** If true, filter out errors in low likelyhood buckets, and only show then in developer + mode *) +let filter_buckets = false + +let frontend_stats_dir_name = "frontend_stats" let global_tenv_filename = "global.tenv" -let specs_files_suffix = ".specs" +(** If true, treat calls to no-arg getters as idempotent w.r.t non-nullness *) +let idempotent_getters = true + +(** If true, changes to code are checked at the procedure level; if false, at the file + level *) +let incremental_procs = true (** Name of the infer configuration file *) let inferconfig_file = ".inferconfig" -let inferconfig_home : string option ref = ref None +let ivar_attributes = "ivar_attributes" -let suppress_warnings_annotations : string option ref = ref None +(** Maximum level of recursion during the analysis, after which a timeout is generated *) +let max_recursion = 5 -(** List of paths to the directories containing specs for library functions. *) -let specs_library = ref [] +(** Flag to tune the level of applying the meet operator for + preconditions during the footprint analysis: + 0 = do not use the meet + 1 = use the meet to generate new preconditions *) +let meet_level = 1 -(** path to lib/specs to retrieve the default models *) -let models_dir = - let bin_dir = Filename.dirname Sys.executable_name in - let lib_dir = Filename.concat (Filename.concat bin_dir Filename.parent_dir_name) "lib" in - let lib_specs_dir = Filename.concat lib_dir specs_dir_name in - lib_specs_dir +let nsnotification_center_checker_backend = false -let string_crc_hex32 s = - Digest.to_hex (Digest.string s) +(** If true, it deals with messages (method calls) in objective-c using the objective-c + typical semantics. That is: if the receiver is nil then the method is nop and it + returns 0. When the flag is false we deal with messages as standard method / function + calls *) +let objc_method_call_semantics = true -let infer_cache : string option ref = ref None +let perf_stats_prefix = "perf_stats" -module JarCache = -struct +let proc_stats_filename = "proc_stats.json" - let mkdir s = - try - Unix.mkdir s 0o700; - true - with Unix.Unix_error _ -> false +let property_attributes = "property_attributes" - let extract_specs dest_dir jarfile = - let zip_channel = Zip.open_in jarfile in - let entries = Zip.entries zip_channel in - let extract_entry entry = - let dest_file = Filename.concat dest_dir (Filename.basename entry.Zip.filename) in - if Filename.check_suffix entry.Zip.filename specs_files_suffix - then Zip.copy_entry_to_file zip_channel entry dest_file in - List.iter extract_entry entries; - Zip.close_in zip_channel +(** If true, sanity-check inferred preconditions against Nullable annotations and report + inconsistencies *) +let report_nullable_inconsistency = true - let handle_jar jarfile = - match !infer_cache with - | Some cache_dir -> - let basename = Filename.basename jarfile in - let key = basename ^ string_crc_hex32 jarfile in - let key_dir = Filename.concat cache_dir key in +let reporting_stats_dir_name = "reporting_stats" - if (mkdir key_dir) - then extract_specs key_dir jarfile; +(** If true, compact summaries before saving *) +let save_compact_summaries = true - specs_library := !specs_library @ [key_dir] - | None -> () -end +(** If true, save the execution time in summaries. This makes the analysis + nondeterministic. *) +let save_time_in_summaries = false -type zip_library = { - zip_filename: string; - zip_channel: Zip.in_file Lazy.t; - models: bool; -} +(** If true enables printing proposition compatible for the SMT project *) +let smt_output = false -let zip_filename zip_library = - zip_library.zip_filename +let source_file_extentions = [".java"; ".m"; ".mm"; ".c"; ".cc"; ".cpp"; ".h"] -let zip_channel zip_library = - Lazy.force zip_library.zip_channel +let sources_dir_name = "sources" -let is_models zip_library = - zip_library.models +let specs_dir_name = "specs" -(** list of the zip files to search for specs files *) -let zip_libraries : zip_library list ref = ref [] -let zip_models : zip_library list ref = ref [] +let specs_files_suffix = ".specs" -let use_jar_cache = from_env_variable "INFER_USE_JAR_CACHE" +let start_filename = ".start" -let add_zip_library zip_filename = - if !infer_cache != None && use_jar_cache then - JarCache.handle_jar zip_filename - else - (* The order matters, the jar files should be added following the order *) - (* specs files should be searched in them *) - let zip_library = { - zip_filename = zip_filename; - zip_channel = lazy (Zip.open_in zip_filename); - models = false - } in - zip_libraries := zip_library :: !zip_libraries +(** If true performs taint analysis *) +let taint_analysis = true -let add_models zip_filename = - let zip_library = { - zip_filename = zip_filename; - zip_channel = lazy (Zip.open_in zip_filename); - models = true - } in - zip_models := zip_library :: !zip_models +(** Enable detailed tracing information during array abstraction *) +let trace_absarray = false -let get_zip_libraries () = - (IList.rev !zip_models) @ (IList.rev !zip_libraries) +(** If true, optimize based on locality using reachability *) +let undo_join = true -let project_root : string option ref = ref None +let unsafe_unret = "<\"Unsafe_unretained\">" -(** FLAGS AND GLOBAL VARIABLES *) +let weak = "<\"Weak\">" + + +(** Compile time configuration values *) + +let version_string = + "Infer version " + ^ Version.versionString + ^ "\nCopyright 2009 - present Facebook. All Rights Reserved.\n" + + +(** System call configuration values *) + +(** Initial time of the analysis, i.e. when this module is loaded, gotten from + Unix.time *) +let initial_analysis_time = Unix.time () + +(** Path to lib/specs to retrieve the default models *) +let models_dir = + let bin_dir = Filename.dirname Sys.executable_name in + let lib_dir = Filename.concat (Filename.concat bin_dir Filename.parent_dir_name) "lib" in + let lib_specs_dir = Filename.concat lib_dir specs_dir_name in + lib_specs_dir + +let os_type = match Sys.os_type with + | "Win32" -> Win32 + | "Cygwin" -> Cygwin + | _ -> Unix + + +(** Command Line options *) + +(** The references representing the command line options are defined in a single + simultaneous let...and...and... binding in order to allow the type-checker to catch + uses of one reference in code for another. This avoids being sensitive to + initialization-order and unintended dependence on the order in which options appear on + the command line. For cases where order-dependence is desired, the interacting options + can be defined together sharing a reference. See debug and specs_library below for two + different examples. *) + +let anon_args = + CLOpt.mk_anon () (** Flag for abstracting fields of structs 0 = no 1 = forget some fields during matching (and so lseg abstraction) *) -let abs_struct = ref 1 +and abs_struct = + CLOpt.mk_int ~deprecated:["absstruct"] ~long:"abs-struct" ~default:1 + ~meta:"int" "Specify abstraction level for fields of structs" (** Flag for abstracting numerical values 0 = no abstraction. 1 = evaluate all expressions abstractly. 2 = 1 + abstract constant integer values during join. *) -let abs_val_default = 2 -let abs_val = - ref abs_val_default - -let reset_abs_val () = - abs_val := abs_val_default - -(** if true, completely ignore the possibility that errors can be caused by unknown procedures - * during the symbolic execution phase *) -let angelic_execution = ref true +and abs_val = + CLOpt.mk_int ~deprecated:["absval"] ~long:"abs-val" ~default:2 + ~meta:"int" "Specify abstraction level for expressions" (** Flag for forgetting memory leak false = no true = forget leaked memory cells during abstraction *) -let allowleak = ref false +and allow_leak = + CLOpt.mk_bool ~deprecated:["leak"] ~long:"allow-leak" + "Forget leaks during abstraction" -(** Flag for ignoring arrays and pointer arithmetic. - 0 = treats both features soundly. - 1 = assumes that the size of every array is infinite. - 2 = assumes that all heap dereferences via array indexing and pointer arithmetic are correct. -*) -let array_level = ref 0 +(** Whether specs can be cleaned up before starting analysis *) +and allow_specs_cleanup = + CLOpt.mk_bool ~deprecated:["allow_specs_cleanup"] ~long:"allow-specs-cleanup" + "Allow to remove existing specs before running analysis when it's not incremental" (** Check whether to report Analysis_stops message in user mode *) -let analysis_stops = ref false - -type os_type = Unix | Win32 | Cygwin +and analysis_stops = + CLOpt.mk_bool ~deprecated:["analysis_stops"] ~long:"analysis-stops" + "Issue a warning when the analysis stops" -let os_type = match Sys.os_type with - | "Win32" -> Win32 - | "Cygwin" -> Cygwin - | _ -> Unix - -(** default path of the project results directory *) -let default_results_dir = - Filename.concat (Sys.getcwd ()) "infer-out" - -(** If true shows internal exceptions*) -let developer_mode = ref false - -(** flag: dotty output filename **) -let dotty_output = ref "icfg.dot" +(** Setup the analyzer in order to filter out errors for this analyzer only *) +and analyzer = + CLOpt.mk_symbol_opt ~deprecated:["analyzer"] ~long:"analyzer" + "Specify the analyzer for the path filtering" + ~symbols:Utils.string_to_analyzer -(** command line option to activate the eradicate checker. *) -let eradicate = ref false - -(** should the checkers be run? *) -let checkers_enabled () = not !eradicate +(** if true, completely ignore the possibility that errors can be caused by unknown procedures + during the symbolic execution phase *) +and angelic_execution = + CLOpt.mk_bool ~deprecated:["angelic_execution"] ~long:"angelic-execution" ~default:true + "Angelic execution, where the analysis ignores errors caused by unknown procedure calls" -(** flag for reactive mode: - the analysis starts from the files captured since the "infer" command started *) -let reactive_mode = ref false +(** Flag for ignoring arrays and pointer arithmetic. + 0 = treats both features soundly. + 1 = assumes that the size of every array is infinite. + 2 = assumes that all heap dereferences via array indexing and pointer arithmetic are correct. +*) +and array_level = + CLOpt.mk_int ~deprecated:["arraylevel"] ~long:"array-level" ~default:0 + ~meta:"int" "Level of treating the array indexing and pointer arithmetic" + +and ast_file = + CLOpt.mk_string_opt ~long:"ast-file" ~short:"ast" + ~meta:"file" "AST file for the translation" + +(** Outfile to save bugs stats in csv format *) +and bugs_csv = + CLOpt.mk_option ~deprecated:["bugs"] ~long:"bugs-csv" ~f:create_outfile + ~meta:"bugs.csv" "Create file bugs.csv containing a list of bugs in CSV format" + +(** Outfile to save bugs stats in json format *) +and bugs_json = + CLOpt.mk_option ~deprecated:["bugs_json"] ~long:"bugs-json" ~f:create_outfile + ~meta:"bugs.json" "Create file bugs.json containing a list of bugs in JSON format" + +(** Outfile to save bugs stats in txt format *) +and bugs_txt = + CLOpt.mk_option ~deprecated:["bugs_txt"] ~long:"bugs-txt" ~f:create_outfile + ~meta:"bugs.txt" "Create file bugs.txt containing a list of bugs in TXT format" + +(** Outfile to save bugs stats in xml format *) +and bugs_xml = + CLOpt.mk_option ~deprecated:["bugs_xml"] ~long:"bugs-xml" ~f:create_outfile + ~meta:"bugs.xml" "Create file bugs.xml containing a list of bugs in XML format" + +(** Outfile to save call stats in csv format *) +and calls_csv = + CLOpt.mk_option ~deprecated:["calls"] ~long:"calls-csv" ~f:create_outfile + ~meta:"calls.csv" "Write individual calls in csv format to calls.csv" + +(* Default is objc, since it's the default for clang (at least in Mac OS) *) +and clang_lang = + CLOpt.mk_symbol ~long:"clang-lang" ~short:"x" ~default:OBJC + "Specify language for clang frontend" + ~symbols:[("c", C); ("objective-c", OBJC); ("c++", CPP); ("objective-c++", OBJCPP)] + +and _ = + CLOpt.mk_string_opt ~deprecated:["classpath"] ~long:"classpath" + ~meta:"path" "Specify where to find user class files and annotation processors" + +and _ = + CLOpt.mk_string_opt ~deprecated:["class_source_map"] ~long:"class-source-map" + ~meta:"file" "path to class -> source map in JSON format" + +(** optional command-line name of the .cluster file *) +and cluster = + CLOpt.mk_string_opt ~deprecated:["cluster"] ~long:"cluster" + ~meta:"file" "Specify a .cluster file to be analyzed" + +and code_query = + CLOpt.mk_string_opt ~deprecated:["codequery"] ~long:"code-query" + ~meta:"query" "Execute the code query" (** Continue the capture for reactive mode: If a procedure was changed beforehand, keep the changed marking. *) -let continue_capture = ref false - -(** Merge the captured results directories specified in the dependency file *) -let merge = ref false +and continue = + CLOpt.mk_bool ~deprecated:["continue"] ~long:"continue" + "Continue the capture for the reactive analysis,\ + increasing the changed files/procedures." + +and curr_language = + let var = ref Clang in + CLOpt.mk_set var Java ~deprecated:["java"] ~long:"java" "Set language to Java" ; + var + +and cxx_experimental = + CLOpt.mk_bool ~deprecated:["cxx-experimental"] ~long:"cxx-experimental" + "Analyze C++ methods, still experimental" + +and debug, print_types, write_dotty = + (** flag: if true print full type info *) + let print_types = + CLOpt.mk_bool ~deprecated:["print_types"] ~long:"print-types" + ~default:(CLOpt.current_exe = CLOpt.C) + "Print types in symbolic heaps" + (** flag: if true write dot files in db dir*) + and write_dotty = + CLOpt.mk_bool ~deprecated:["dotty"] ~long:"write-dotty" + "Produce dotty files in the results directory" + in + let debug = + CLOpt.mk_bool_group ~deprecated:["debug"] ~long:"debug" ~short:"g" + "Debug mode (also sets --print-types and --write-dotty)" + [print_types; write_dotty] + in + (debug, print_types, write_dotty) + +(* The classes in the given jar file will be translated. No sources needed *) +and dependencies = + CLOpt.mk_bool ~deprecated:["dependencies"] ~long:"dependencies" + "Translate all the dependencies during the capture" -(** Flag for footprint discovery mode *) -let footprint = ref true - -(** Set in the middle of forcing delayed prints *) -let forcing_delayed_prints = ref false - -(** If true, treat calls to no-arg getters as idempotent w.r.t non-nullness *) -let idempotent_getters = ref true +(** If true shows internal exceptions*) +and developer_mode = + CLOpt.mk_bool ~deprecated:["developer_mode"] ~long:"developer-mode" + ~default:(CLOpt.current_exe = CLOpt.P) + "Reserved" -(** if true, changes to code are checked at the procedure level; if false, at the file level *) -let incremental_procs = ref true +(** if true, print cfg nodes in the dot file that are not defined in that file *) +and dotty_cfg_libs = + CLOpt.mk_bool ~deprecated:["dotty_no_cfg_libs"] ~long:"dotty-cfg-libs" ~default:true + "Prints the cfg of the code coming from the libraries" -(** if active, join x+j and x+k for constants j and k *) -let join_plus = ref true +(** command line option to activate the eradicate checker. *) +and eradicate, checkers = + (** command line option: if true, run the analysis in checker mode *) + let checkers = + CLOpt.mk_bool ~deprecated:["checkers"] ~long:"checkers" + "Run only the checkers instead of the full analysis" + in + let eradicate = + CLOpt.mk_bool_group ~deprecated:["eradicate"] ~long:"eradicate" + "Activate the eradicate checker for java annotations (also sets --checkers)" + [checkers] + in + (eradicate, checkers) + +and err_file = + CLOpt.mk_string ~deprecated:["err_file"] ~long:"err-file" ~default:"" + ~exes:CLOpt.[A] ~meta:"file" "use file for the err channel" + +(* Generate harness for Android code *) +and harness = + CLOpt.mk_bool ~deprecated:["harness"] ~long:"harness" + "Create Android lifecycle harness" + +and headers = + CLOpt.mk_bool ~deprecated:["headers"] ~deprecated_no:["no_headers"] ~long:"headers" + "Translate code in header files" + +and infer_cache = + CLOpt.mk_string_opt ~deprecated:["infer_cache"] ~long:"infer-cache" + ~f:filename_to_absolute + ~meta:"dir" "Select a directory to contain the infer cache" + +and inferconfig_home = + CLOpt.mk_string_opt ~deprecated:["inferconfig_home"] ~long:"inferconfig-home" + ~exes:CLOpt.[A] ~meta:"dir" "Path to the .inferconfig file" + +(** Set the timeout values in seconds and symops, computed as a multiple of the integer + parameter *) +and iterations = + CLOpt.mk_int ~deprecated:["iterations"] ~long:"iterations" ~default:1 + ~meta:"int" + "Specify the maximum number of operations for each function, expressed as a multiple \ + of symbolic operations" (** Flag to tune the final information-loss check used by the join 0 = use the most aggressive join for preconditions 1 = use the least aggressive join for preconditions *) -let join_cond = ref 1 +and join_cond = + CLOpt.mk_int ~deprecated:["join_cond"] ~long:"join-cond" ~default:1 + ~meta:"int" "Set the strength of the final information-loss check used by the join" -(** Flag for turning on the transformation that - null is assigned to a program variable when it becomes dead. - **) -let liveness = ref true +(** Outfile to save the latex report *) +and latex = + CLOpt.mk_option ~deprecated:["latex"] ~long:"latex" ~f:create_outfile + ~meta:"file.tex" "Print latex report to file.tex" -(** if true, give static procs a long name filename::procname *) -let long_static_proc_names = ref false +(** name of the file to load analysis results from *) +and load_results = + CLOpt.mk_string_opt ~deprecated:["load_results"] ~long:"load-results" + ~meta:"file.iar" "Load analysis results from Infer Analysis Results file file.iar" -(** Number of lines of code in original file *) -let nLOC = ref 0 +(** name of the makefile to create with clusters and dependencies *) +and makefile = + CLOpt.mk_string ~deprecated:["makefile"] ~long:"makefile" ~default:"" + ~exes:CLOpt.[A] ~meta:"file" "create a makefile to perform the analysis" -(** Maximum level of recursion during the analysis, after which a timeout is generated *) -let max_recursion = ref 5 - -(** Flag to tune the level of applying the meet operator for - preconditions during the footprint analysis. - 0 = do not use the meet. - 1 = use the meet to generate new preconditions. -*) -let meet_level = ref 1 +(** Merge the captured results directories specified in the dependency file *) +and merge = + CLOpt.mk_bool ~deprecated:["merge"] ~long:"merge" + "Merge the captured results directories specified in the dependency file" + +(** List of obj memory leak buckets to be checked in Objective-C/C++ *) +and ml_buckets = + CLOpt.mk_symbol_seq ~deprecated:["ml_buckets"] ~long:"ml-buckets" ~default:[`MLeak_cf] + "Specify the memory leak buckets to be checked: \ + 'cf' checks leaks from Core Foundation, \ + 'arc' from code compiled in ARC mode, \ + 'narc' from code not compiled in ARC mode, \ + 'cpp' from C++ code" + ~symbols:[ + ("all", `MLeak_all); + ("cf", `MLeak_cf); + ("arc", `MLeak_arc); + ("narc", `MLeak_no_arc); + ("cpp", `MLeak_cpp); + ("unknown_origin", `MLeak_unknown)] + +and models_file = + CLOpt.mk_string_opt ~deprecated:["models"] ~long:"models" + ~exes:CLOpt.[A;J] ~meta:"zip file" "add a zip file containing the models" + +and models_mode = + CLOpt.mk_bool ~deprecated:["models_mode"] ~long:"models-mode" + "Mode for computing the models" + +and modified_targets = + CLOpt.mk_string_opt ~deprecated:["modified_targets"] ~long:"modified-targets" + ~meta:"file" "Read the file of buck targets modified since the last analysis" (** Monitor the size of the props, and print every time the current max is exceeded *) -let monitor_prop_size = ref false +and monitor_prop_size = + CLOpt.mk_bool ~deprecated:["monitor_prop_size"] ~long:"monitor-prop-size" + "Monitor size of props" (** Flag for using the nonempty lseg only **) -let nelseg = ref false +and nelseg = + CLOpt.mk_bool ~deprecated:["nelseg"] ~long:"nelseg" + "Use only nonempty lsegs" -(** Flag to activate nonstop mode: the analysis continues after in encounters errors *) -let nonstop = ref false +(** true if the current objective-c source file is compiled with automatic reference counting + (ARC) *) +and objc_arc = + CLOpt.mk_bool ~deprecated:["fobjc-arc"] ~long:"objc-arc" + "Translate with Objective-C Automatic Reference Counting (ARC)" + +and objc_memory_model = + CLOpt.mk_bool ~deprecated:["objcm"] ~long:"objc-memory-model" + "Use ObjC memory model" (** if true, skip the re-execution phase *) -let only_footprint = ref false +and only_footprint = + CLOpt.mk_bool ~deprecated:["only_footprint"] ~long:"only-footprint" + "Skip the re-execution phase" -(** if true, user simple pretty printing *) -let pp_simple = ref true +and optimistic_cast = + CLOpt.mk_bool ~deprecated:["optimistic_cast"] ~long:"optimistic-cast" + "Allow cast of undefined values" + +and out_file = + CLOpt.mk_string ~deprecated:["out_file"] ~long:"out-file" ~default:"" + ~exes:CLOpt.[A] ~meta:"file" "use file for the out channel" + +and margin = + CLOpt.mk_int ~deprecated:["set_pp_margin"] ~long:"margin" ~default:100 + ~meta:"int" "Set right margin for the pretty printing functions" + +(** command line flag: if true, print stats about preconditions to standard output *) +and precondition_stats = + CLOpt.mk_bool ~deprecated:["precondition_stats"] ~long:"precondition-stats" + "Print stats about preconditions to standard output" -(** flag: if true print full type info *) -let print_types = ref false +(** if true, show buckets in textual description of errors *) +and print_buckets = + CLOpt.mk_bool ~deprecated:["print_buckets"] ~long:"print-buckets" + "Add buckets to issue descriptions, useful when developing infer" + +and print_builtins = + CLOpt.mk_bool ~deprecated:["print_builtins"] ~long:"print-builtins" + "Print the builtin functions and exit" (** if true, acrtivate color printing by diff'ing w.r.t. previous prop *) -let print_using_diff = ref true +and print_using_diff = + CLOpt.mk_bool ~deprecated_no:["noprintdiff"] ~long:"print-using-diff" ~default:true + "Highlighting diff w.r.t. previous prop in printing" + +(** Outfile to save procedures stats in csv format *) +and procs_csv = + CLOpt.mk_option ~deprecated:["procs"] ~long:"procs-csv" ~f:create_outfile + ~meta:"procs.csv" "Create file procs.csv containing statistics for each procedure in CSV format" + +(** Outfile to save procedures stats in xml format *) +and procs_xml = + CLOpt.mk_option ~deprecated:["procs_xml"] ~long:"procs-xml" ~f:create_outfile + ~meta:"procs.xml" "Create file procs.xml containing statistics for each procedure in XML format" + +and progress_bar = + CLOpt.mk_bool ~deprecated_no:["no_progress_bar"] ~long:"progress-bar" ~short:"pb" ~default:true + "Show a progress bar" + +and project_root = + CLOpt.mk_string_opt ~deprecated:["project_root"] ~long:"project-root" ~short:"pr" + ?default:(if CLOpt.(current_exe = P) then Some (Sys.getcwd ()) else None) + ~f:filename_to_absolute + ~exes:CLOpt.[A;C;J;L;P] ~meta:"dir" "Specify the root directory of the project" + +(** command line flag: if true, do not print the spec to standard output *) +and quiet = + CLOpt.mk_bool ~long:"quiet" ~short:"q" + "Do not print specs on standard output" -(** path of the project results directory *) -let results_dir = ref default_results_dir +(** flag for reactive mode: + the analysis starts from the files captured since the "infer" command started *) +and reactive = + CLOpt.mk_bool ~deprecated:["reactive"] ~long:"reactive" + "Reactive propagation mode starting analysis from changed files" + +(** Outfile to save the analysis report *) +and report = + CLOpt.mk_option ~deprecated:["report"] ~long:"report" ~f:create_outfile + ~meta:"report_file" "Create file report_file containing a report of the analysis results" + +(** If true then include Infer source code locations in json reports *) +and reports_include_ml_loc = + CLOpt.mk_bool ~deprecated:["with_infer_src_loc"] ~long:"reports-include-ml-loc" + "Include the location (in the Infer source code) from where reports are generated" + +and results_dir = + CLOpt.mk_string ~deprecated:["results_dir"] ~long:"results-dir" + ~default:(Filename.concat (Sys.getcwd ()) "infer-out") + ~exes:CLOpt.[A;C;J;L;P] ~meta:"dir" "Specify the project results directory" + +(** name of the file to load save results to *) +and save_results = + CLOpt.mk_string_opt ~deprecated:["save_results"] ~long:"save-results" + ~meta:"file.iar" "Save analysis results to Infer Analysis Results file file.iar" + +(** number of seconds to multiply by the number of iterations, after which there is a timeout *) +and seconds_per_iteration = + CLOpt.mk_float ~deprecated:["seconds_per_iteration"] ~long:"seconds-per-iteration" ~default:0. + ~meta:"float" "Set the number of seconds per iteration" + +and source_file = + CLOpt.mk_string_opt ~long:"source-file" ~short:"c" ~meta:"file" "File to translate" + +(** command-line option to print the location of the copy of a source file *) +and source_file_copy = + CLOpt.mk_string_opt ~deprecated:["source_file_copy"] ~long:"source-file-copy" + ~meta:"source_file" "Print the path of the copy of source_file in the results directory" (** Flag to tune the level of abstracting the postconditions of specs discovered by the footprint analysis. 0 = nothing special. 1 = filter out redundant posts implied by other posts. *) -let spec_abs_level = ref 1 +and spec_abs_level = + CLOpt.mk_int ~deprecated:["spec_abs_level"] ~long:"spec-abs-level" ~default:1 + ~meta:"int" "Set the level of abstracting the postconditions of discovered specs" + +(** List of paths to the directories containing specs for library functions. *) +and specs_library = + let specs_library = + CLOpt.mk_string_list ~long:"specs-library" ~short:"lib" ~f:filename_to_absolute + ~exes:CLOpt.[A] ~meta:"dir" + "add dir to the list of directories to be searched for spec files" in + let _ = + (* Given a filename with a list of paths, convert it into a list of string iff they are + absolute *) + let read_specs_dir_list_file fname = + let validate_path path = + if Filename.is_relative path then + failwith ("Failing because path " ^ path ^ " is not absolute") in + match read_file fname with + | Some pathlist -> + IList.iter validate_path pathlist; + pathlist + | None -> failwith ("cannot read file " ^ fname) + in + CLOpt.mk_string ~deprecated:["specs-dir-list-file"] ~long:"specs-library-index" + ~default:"" + ~f:(fun file -> specs_library := (read_specs_dir_list_file file) @ !specs_library; "") + ~exes:CLOpt.[A] ~meta:"file" + "add the newline-separated directories listed in to the list of directories to be \ + searched for spec files" in + specs_library + +(** If active, enable special treatment of static final fields. *) +and static_final = + CLOpt.mk_bool ~deprecated_no:["no-static_final"] ~long:"static-final" ~default:true + "Special treatment for static final fields" + +and stats = + CLOpt.mk_bool ~deprecated:["stats"] ~long:"stats" "Enables stats mode" + +(** Flag to activate nonstop mode: the analysis continues after in encounters errors *) +and no_stop = + CLOpt.mk_bool ~deprecated:["nonstop"] ~long:"no-stop" + "Nonstop mode: the analysis continues after finding errors. \ + With this option the analysis can become less precise." + +and subtype_multirange = + CLOpt.mk_bool ~deprecated:["subtype_multirange"] ~long:"subtype-multirange" ~default:true + "Use the multirange subtyping domain" + +and suppress_warnings_out = + CLOpt.mk_string_opt ~deprecated:["suppress_warnings_out"] ~long:"suppress-warnings-annotations" + ~exes:CLOpt.[J] ~meta:"path" "Path to list of collected @SuppressWarnings annotations" + +(** command line flag: if true, produce a svg file *) +and svg = + CLOpt.mk_bool ~deprecated:["svg"] ~long:"svg" + "Generate .dot and .svg" + +(** number of symops to multiply by the number of iterations, after which there is a timeout *) +and symops_per_iteration = + CLOpt.mk_int ~deprecated:["symops_per_iteration"] ~long:"symops-per-iteration" ~default:0 + ~meta:"int" "Set the number of symbolic operations per iteration" (** Flag for test mode *) -let test = ref true +and test = + CLOpt.mk_bool ~deprecated_no:["notest"] ~long:"test" ~default:true + "Test mode" -(** Flag set to enable detailed tracing informatin during error explanation *) -let trace_error = ref false +(** command line option to test the filtering based on .inferconfig *) +and test_filtering = + CLOpt.mk_bool ~deprecated:["test_filtering"] ~long:"test-filtering" + "List all the files Infer can report on (should be call at the root of the project)" -(** Flag set to enable detailed tracing information during re-arrangement *) -let trace_rearrange = ref false +and testing_mode = + CLOpt.mk_bool ~deprecated:["testing_mode"] ~long:"testing-mode" + "Mode for testing, where no headers are translated, and dot files are created" + +(** Flag set to enable detailed tracing informatin during error explanation *) +and trace_error = + CLOpt.mk_bool ~deprecated:["trace_error"] ~long:"trace-error" + "Turn on tracing of error explanation" (** Flag set to enable detailed tracing information during join *) -let trace_join = ref false +and trace_join = + CLOpt.mk_bool ~deprecated:["trace_join"] ~long:"trace-join" + "Turn on tracing of join" + +(** Flag set to enable detailed tracing information during re-arrangement *) +and trace_rearrange = + CLOpt.mk_bool ~deprecated:["trace_rearrange"] ~long:"trace-rearrange" + "Turn on tracing of rearrangement" -(** Flag set to enable detailed tracing information during array abstraction *) -let trace_absarray = ref false +(** if true, generate preconditions for runtime exceptions in Java and report errors for the public + methods having preconditions to throw runtime exceptions *) +and tracing = + CLOpt.mk_bool ~deprecated:["tracing"] ~long:"tracing" + "Report error traces for runtime exceptions (Only for Java)" (** Consider the size of types during analysis, e.g. cannot use an int pointer to write to a char *) -let type_size = ref false +and type_size = + CLOpt.mk_bool ~deprecated:["type_size"] ~long:"type-size" + "Consider the size of types during analysis" -(** if true, compact summaries before saving *) -let save_compact_summaries = ref true +(** command line flag: if true, produce unit test for each spec *) +and unit_test = + CLOpt.mk_bool ~deprecated:["unit_test"] ~long:"unit-test" + "Print unit test code" -(** If true, save the execution time in summaries. - This makes the analysis nondeterministic. *) -let save_time_in_summaries = ref false +and verbose_out = + CLOpt.mk_string ~deprecated:["verbose_out"] ~long:"verbose-out" ~default:"" + ~exes:CLOpt.[J] ~meta:"file" "Set the path to the javac verbose output" -(** flag: if true enables printing proposition compatible for the SMT project *) -let smt_output = ref false +and version = + CLOpt.mk_bool ~deprecated:["version"] ~long:"version" + ~exes:CLOpt.[A;C;J;L;P] "Print version information and exit" -(** flag: if true performs taint analysis *) -let taint_analysis = ref true +and version_json = + CLOpt.mk_bool ~deprecated:["version_json"] ~long:"version-json" + "Print version json formatted" -(** Flag for turning on the optimization based on locality - 0 = no - 1 = based on reachability -*) -let undo_join = ref true +(** command line flag: if true, print whole seconds only *) +and whole_seconds = + CLOpt.mk_bool ~deprecated:["whole_seconds"] ~long:"whole-seconds" + "Print whole seconds only" (** visit mode for the worklist: 0 depth - fist visit 1 bias towards exit node 2 least visited first *) -let worklist_mode = ref 0 - -(** flag: if true write dot files in db dir*) -let write_dotty = ref false +and worklist_mode = + let var = ref 0 in + CLOpt.mk_set var 2 ~long:"coverage" ~exes:CLOpt.[A] + "analysis mode to maximize coverage (can take longer)" ; + CLOpt.mk_set var 1 ~long:"exit-node-bias" ~deprecated:["exit_node_bias"] + "nodes nearest the exit node are analyzed first" ; + CLOpt.mk_set var 2 ~long:"visits-bias" ~deprecated:["visits_bias"] + "nodes visited fewer times are analyzed first" ; + var (** flag: if true write html files in db dir *) -let write_html = ref false +and write_html = + CLOpt.mk_bool ~deprecated:["html"] ~long:"write-html" + "Produce hmtl output in the results directory" -let subtype_multirange = ref true +(** command line flag: if true, export specs to xml files *) +and xml_specs = + CLOpt.mk_bool ~deprecated:["xml"] ~long:"xml-specs" + "Export specs into XML files file1.xml ... filen.xml" -let optimistic_cast = ref false +(** list of the zip files to search for specs files *) +and zip_libraries : zip_library list ref = ref [] -(** if true, filter out errors in low likelyhood buckets, and only show then in developer mode *) -let filter_buckets = ref false +and zip_specs_library = + CLOpt.mk_string_list ~long:"zip-specs-library" ~short:"ziplib" ~f:filename_to_absolute + ~exes:CLOpt.[A] ~meta:"zip file" "add a zip file containing library spec files" -(** if true, show buckets in textual description of errors *) -let show_buckets = ref false -(** if true, show memory leak buckets in textual description of errors *) -let show_ml_buckets = ref false +(** Global variables *) -(** if true, print cfg nodes in the dot file that are not defined in that file *) -let dotty_cfg_libs = ref true +let set_reference_and_call_function reference value f x = + let saved = !reference in + let restore () = + reference := saved in + try + reference := value; + let res = f x in + restore (); + res + with + | exn -> + restore (); + raise exn -(** if true, it deals with messages (method calls) in objective-c using the objective-c - typical semantics. That is: if the receiver is nil then the method is nop and it returns 0. - When the flag is false we deal with messages as standard method / function calls *) -let objc_method_call_semantics = ref true +(** Flag for footprint discovery mode *) +let footprint = ref true -(** if true, generate preconditions for runtime exceptions in Java and report errors for the public - methods having preconditions to throw runtime exceptions *) -let report_runtime_exceptions = ref false +let run_in_footprint_mode f x = + set_reference_and_call_function footprint true f x -(** if true, sanity-check inferred preconditions against Nullable annotations and report - inconsistencies *) -let report_nullable_inconsistency = ref true +let run_in_re_execution_mode f x = + set_reference_and_call_function footprint false f x -(** true if the current objective-c source file is compiled with automatic reference counting (ARC) *) -let arc_mode = ref false +(** Set in the middle of forcing delayed prints *) +let forcing_delayed_prints = ref false -let objc_memory_model_on = ref false +(** Number of lines of code in original file *) +let nLOC = ref 0 -let report_custom_error = from_env_variable "INFER_REPORT_CUSTOM_ERROR" -let default_failure_name = "ASSERTION_FAILURE" +(** if true, user simple pretty printing *) +let pp_simple = ref true -let analyze_models = from_env_variable "INFER_ANALYZE_MODELS" +let reset_abs_val = + let abs_val_default = !abs_val in + fun () -> + abs_val := abs_val_default -(** initial time of the analysis, i.e. when this module is loaded, gotten from Unix.time *) -let initial_analysis_time = Unix.time () +let run_with_abs_val_equal_zero f x = + set_reference_and_call_function abs_val 0 f x -let symops_timeout, seconds_timeout = - let default_symops_timeout = 333 in - let default_seconds_timeout = 10.0 in - let long_symops_timeout = 1000 in - let long_seconds_timeout = 30.0 in - if analyze_models then - (* use longer timeouts when analyzing models *) - long_symops_timeout, long_seconds_timeout - else - default_symops_timeout, default_seconds_timeout -(** number of symops to multiply by the number of iterations, after which there is a timeout *) -let symops_per_iteration = ref symops_timeout +(** Configuration values specified by environment variables *) -(** number of seconds to multiply by the number of iterations, after which there is a timeout *) -let seconds_per_iteration = ref seconds_timeout +let from_env_variable var_name = + try + let _ = Sys.getenv var_name in true + with Not_found -> false -(** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *) -let iterations = ref 1 +let get_env_variable var_name = + try + let v = Sys.getenv var_name in + if v = "" then None else Some v + with Not_found -> None -(** experimental: dynamic dispatch for interface calls only in Java. off by default because of the - cost *) -let sound_dynamic_dispatch = from_env_variable "INFER_SOUND_DYNAMIC_DISPATCH" +let analyze_models = from_env_variable "INFER_ANALYZE_MODELS" (** experimental: handle dynamic dispatch by following the JVM semantics and creating during the symbolic excution procedure descriptions using the types information found in the abstract state *) let lazy_dynamic_dispatch = from_env_variable "INFER_LAZY_DYNAMIC_DISPATCH" -module Experiment = struct - - (** if true, a precondition with e.g. index 3 in an array does not require the caller to have index 3 too - this mimics what happens with direct access to the array without a procedure call, where the index is simply materialized if not there *) - let allow_missing_index_in_proc_call = ref true - - (** if true, a procedure call succeeds even when there is a bound error - this mimics what happens with a direct array access where an error is produced and the analysis continues *) - let bound_error_allowed_in_procedure_call = ref true - -end - -let source_file_extentions = [".java"; ".m"; ".mm"; ".c"; ".cc"; ".cpp"; ".h"] - -let anonymous_block_prefix = "__objc_anonymous_block_" - -let anonymous_block_num_sep = "______" - -let property_attributes = "property_attributes" - -let ivar_attributes = "ivar_attributes" - -let unsafe_unret = "<\"Unsafe_unretained\">" - -let weak = "<\"Weak\">" - -let assign = "<\"Assign\">" - -let start_filename = ".start" - -(** Programming language. *) -type language = C_CPP | Java +let report_custom_error = from_env_variable "INFER_REPORT_CUSTOM_ERROR" -(** current language *) -let curr_language = ref C_CPP +(** experimental: dynamic dispatch for interface calls only in Java. off by default because of the + cost *) +let sound_dynamic_dispatch = from_env_variable "INFER_SOUND_DYNAMIC_DISPATCH" -let string_of_language = function - | Java -> "Java" - | C_CPP -> "C_CPP" +let use_jar_cache = from_env_variable "INFER_USE_JAR_CACHE" -let show_progress_bar = ref true -let nsnotification_center_checker_backend = ref false +(** Parse Command Line Args *) + +let exe_usage (exe : CLOpt.exe) = + match exe with + | A -> + version_string ^ "\ + Usage: InferAnalyze [options]\n\ + Analyze the files captured in the project results directory, \ + which can be specified with the --results-dir option." + | C -> + "\nUsage: InferClang -c C Files -ast AST Files --results-dir [options] \n" + | J -> + "Usage: InferJava -d compilation_dir -sources filename\n" + | L -> + "Usage: InferLLVM -c [options]\n" + | P -> + "Usage: InferPrint [options] name1.specs ... namen.specs\n\ + Read, convert, and print .specs files. \ + To process all the .specs in the current directory, pass . as only parameter \ + To process all the .specs in the results directory, use option --results-dir \ + Each spec is printed to standard output unless option -q is used." + | T -> + version_string + +let post_parsing_initialization () = + F.set_margin !margin ; + + if !version then ( + F.fprintf F.std_formatter "%s@." version_string ; + exit 0 + ); + if !version_json then ( + F.fprintf F.std_formatter "%s@." Version.versionJson ; + exit 0 + ); + + let set_minor_heap_size nMb = (* increase the minor heap size to speed up gc *) + let ctrl = Gc.get () in + let oneMb = 1048576 in + let new_size = max ctrl.Gc.minor_heap_size (nMb * oneMb) + in Gc.set { ctrl with Gc.minor_heap_size = new_size } + in + set_minor_heap_size 1 ; + + let symops_timeout, seconds_timeout = + let default_symops_timeout = 333 in + let default_seconds_timeout = 10.0 in + let long_symops_timeout = 1000 in + let long_seconds_timeout = 30.0 in + if analyze_models then + (* use longer timeouts when analyzing models *) + long_symops_timeout, long_seconds_timeout + else + default_symops_timeout, default_seconds_timeout + in + if !seconds_per_iteration = 0. then seconds_per_iteration := seconds_timeout ; + if !symops_per_iteration = 0 then symops_per_iteration := symops_timeout ; + + let add_zip_library zip_filename = + match !infer_cache with + | Some cache_dir when use_jar_cache -> + let mkdir s = + try + Unix.mkdir s 0o700; + true + with Unix.Unix_error _ -> false + in + let extract_specs dest_dir zip_filename = + let zip_channel = Zip.open_in zip_filename in + let entries = Zip.entries zip_channel in + let extract_entry entry = + let dest_file = Filename.concat dest_dir (Filename.basename entry.Zip.filename) in + if Filename.check_suffix entry.Zip.filename specs_files_suffix + then Zip.copy_entry_to_file zip_channel entry dest_file in + IList.iter extract_entry entries; + Zip.close_in zip_channel + in + let basename = Filename.basename zip_filename in + let key = basename ^ string_crc_hex32 zip_filename in + let key_dir = Filename.concat cache_dir key in + if (mkdir key_dir) + then extract_specs key_dir zip_filename; + specs_library := !specs_library @ [key_dir] + | _ -> + (* The order matters, the jar files should be added following the order specs files should + be searched in them *) + let zip_library = { + zip_filename = zip_filename; + zip_channel = lazy (Zip.open_in zip_filename); + models = false + } in + zip_libraries := zip_library :: !zip_libraries + in + IList.iter add_zip_library (IList.rev !zip_specs_library) ; + + let zip_models = ref [] in + let add_models zip_filename = + let zip_library = { + zip_filename = zip_filename; + zip_channel = lazy (Zip.open_in zip_filename); + models = true + } in + zip_models := zip_library :: !zip_models + in + (match !models_file with + | Some file -> add_models (filename_to_absolute file) + | None -> ()); + + zip_libraries := IList.rev_append !zip_models (IList.rev !zip_libraries) + + +let parse_args_and_return_usage_exit = + let usage_exit = CLOpt.parse "INFER_ARGS" exe_usage in + if !debug || !developer_mode then + prerr_endline + ((Filename.basename Sys.executable_name) ^ " got args " + ^ (try Unix.getenv "INFER_ARGS" with Not_found -> "")) ; + post_parsing_initialization () ; + usage_exit + +let print_usage_exit () = + parse_args_and_return_usage_exit 1 + + +(** Freeze initialized configuration values *) + +let anon_args = !anon_args +and abs_struct = !abs_struct +and allow_specs_cleanup = !allow_specs_cleanup +and analysis_stops = !analysis_stops +and analyzer = !analyzer +and angelic_execution = !angelic_execution +and arc_mode = objc_arc +and array_level = !array_level +and ast_file = !ast_file +and bugs_csv = !bugs_csv +and bugs_json = !bugs_json +and bugs_txt = !bugs_txt +and bugs_xml = !bugs_xml +and calls_csv = !calls_csv +and checkers = !checkers +(** should the checkers be run? *) +and checkers_enabled = not !eradicate +and clang_lang = !clang_lang +and cluster_cmdline = !cluster +and code_query = !code_query +and continue_capture = !continue +and create_harness = !harness +and cxx_experimental = !cxx_experimental +and debug_mode = !debug +and dependency_mode = !dependencies +and developer_mode = !developer_mode +and dotty_cfg_libs = !dotty_cfg_libs +and eradicate = !eradicate +and err_file_cmdline = !err_file +and infer_cache = !infer_cache +and inferconfig_home = !inferconfig_home +and iterations = !iterations +and javac_verbose_out = !verbose_out +and join_cond = !join_cond +and latex = !latex +and load_analysis_results = !load_results +and makefile_cmdline = !makefile +and merge = !merge +and ml_buckets = !ml_buckets +and models_file = !models_file +and models_mode = !models_mode +and modified_targets = !modified_targets +and monitor_prop_size = !monitor_prop_size +and nelseg = !nelseg +and no_static_final = not !static_final +and no_translate_libs = not !headers +and nonstop = !no_stop +and objc_memory_model_on = !objc_memory_model +and only_footprint = !only_footprint +and optimistic_cast = !optimistic_cast +and out_file_cmdline = !out_file +and precondition_stats = !precondition_stats +and print_builtins = !print_builtins +and print_types = !print_types +and print_using_diff = !print_using_diff +and procs_csv = !procs_csv +and procs_xml = !procs_xml +and project_root = !project_root +and quiet = !quiet +and reactive_mode = !reactive +and report = !report +and report_runtime_exceptions = !tracing +and reports_include_ml_loc = !reports_include_ml_loc +and results_dir = !results_dir +and save_analysis_results = !save_results +and seconds_per_iteration = !seconds_per_iteration +and show_buckets = !print_buckets +and show_progress_bar = !progress_bar +and source_file = !source_file +and source_file_copy = !source_file_copy +and spec_abs_level = !spec_abs_level +and specs_library = !specs_library +and stats_mode = !stats +and subtype_multirange = !subtype_multirange +and suppress_warnings_annotations = !suppress_warnings_out +and svg = !svg +and symops_per_iteration = !symops_per_iteration +and test = !test +and test_filtering = !test_filtering +and testing_mode = !testing_mode +and trace_error = !trace_error +and trace_join = !trace_join +and trace_rearrange = !trace_rearrange +and type_size = !type_size +and unit_test = !unit_test +and whole_seconds = !whole_seconds +and worklist_mode = !worklist_mode +and write_dotty = !write_dotty +and write_html = !write_html +and xml_specs = !xml_specs +and zip_libraries = !zip_libraries diff --git a/infer/src/backend/config.mli b/infer/src/backend/config.mli new file mode 100644 index 000000000..d2e6be075 --- /dev/null +++ b/infer/src/backend/config.mli @@ -0,0 +1,222 @@ +(* + * Copyright (c) 2009 - 2013 Monoidics ltd. + * 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 + +(** Configuration values: either constant, determined at compile time, or set at startup + time by system calls, environment variables, or command line options *) + + +type language = Clang | Java + +val string_of_language : language -> string + +type clang_lang = C | CPP | OBJC | OBJCPP + +type os_type = Unix | Win32 | Cygwin + +type zip_library = { + zip_filename : string; + zip_channel : Zip.in_file Lazy.t; + models : bool; +} + + +(** Configuration values *) + +val allow_missing_index_in_proc_call : bool +val anonymous_block_num_sep : string +val anonymous_block_prefix : string +val assign : string +val attributes_dir_name : string +val backend_stats_dir_name : string +val bound_error_allowed_in_procedure_call : bool +val captured_dir_name : string +val default_failure_name : string +val default_in_zip_results_dir : string +val dotty_output : string +val filter_buckets : bool +val frontend_stats_dir_name : string +val global_tenv_filename : string +val idempotent_getters : bool +val incremental_procs : bool +val inferconfig_file : string +val initial_analysis_time : float +val ivar_attributes : string +val max_recursion : int +val meet_level : int +val models_dir : string +val nsnotification_center_checker_backend : bool +val objc_method_call_semantics : bool +val os_type : os_type +val perf_stats_prefix : string +val proc_stats_filename : string +val property_attributes : string +val report_nullable_inconsistency : bool +val reporting_stats_dir_name : string +val save_compact_summaries : bool +val save_time_in_summaries : bool +val smt_output : bool +val source_file_extentions : string list +val sources_dir_name : string +val specs_dir_name : string +val specs_files_suffix : string +val start_filename : string +val taint_analysis : bool +val trace_absarray : bool +val undo_join : bool +val unsafe_unret : string +val weak : string + + +(** Configuration values specified by environment variables *) + +val from_env_variable : string -> bool +val get_env_variable : string -> string option + +val analyze_models : bool +val lazy_dynamic_dispatch : bool +val report_custom_error : bool +val sound_dynamic_dispatch : bool + + +(** Configuration values specified by command-line options *) + +val anon_args : string list +val abs_struct : int +val allow_specs_cleanup : bool +val analysis_stops : bool +val analyzer : analyzer option +val angelic_execution : bool +val array_level : int +val ast_file : string option +val bugs_csv : outfile option +val bugs_json : outfile option +val bugs_txt : outfile option +val bugs_xml : outfile option +val calls_csv : outfile option +val checkers : bool +val checkers_enabled : bool +val clang_lang : clang_lang +val cluster_cmdline : string option +val code_query : string option +val continue_capture : bool +val create_harness : bool +val cxx_experimental : bool +val debug_mode : bool +val dependency_mode : bool +val developer_mode : bool +val dotty_cfg_libs : bool +val eradicate : bool +val err_file_cmdline : string +val infer_cache : string option +val inferconfig_home : string option +val iterations : int +val javac_verbose_out : string +val join_cond : int +val latex : outfile option +val load_analysis_results : string option +val makefile_cmdline : string +val merge : bool +val ml_buckets : + [ `MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown ] list +val models_file : string option +val models_mode : bool +val modified_targets : string option +val monitor_prop_size : bool +val nelseg : bool +val no_static_final : bool +val no_translate_libs : bool +val nonstop : bool +val objc_memory_model_on : bool +val only_footprint : bool +val optimistic_cast : bool +val out_file_cmdline : string +val precondition_stats : bool +val print_builtins : bool +val print_types : bool +val print_using_diff : bool +val procs_csv : outfile option +val procs_xml : outfile option +val project_root : string option +val quiet : bool +val reactive_mode : bool +val report : outfile option +val report_runtime_exceptions : bool +val reports_include_ml_loc : bool +val results_dir : string +val save_analysis_results : string option +val seconds_per_iteration : float +val show_buckets : bool +val show_progress_bar : bool +val source_file : string option +val source_file_copy : string option +val spec_abs_level : int +val specs_library : string list +val stats_mode : bool +val subtype_multirange : bool +val suppress_warnings_annotations : string option +val svg : bool +val symops_per_iteration : int +val test : bool +val test_filtering : bool +val testing_mode : bool +val trace_error : bool +val trace_join : bool +val trace_rearrange : bool +val type_size : bool +val unit_test : bool +val whole_seconds : bool +val worklist_mode : int +val write_dotty : bool +val write_html : bool +val xml_specs : bool +val zip_libraries : zip_library list + + +(** Global variables *) + +(** [set_reference_and_call_function ref val f x] calls f x with ref set to val. + Restore the initial value also in case of exception. *) +val set_reference_and_call_function : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c + +val footprint : bool ref + +(** Call f x with footprint set to true. + Restore the initial value of footprint also in case of exception. *) +val run_in_footprint_mode : ('a -> 'b) -> 'a -> 'b + +(** Call f x with footprint set to false. + Restore the initial value of footprint also in case of exception. *) +val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b + +val forcing_delayed_prints : bool ref +val nLOC : int ref +val pp_simple : bool ref + + +(** Global variables with initial values specified by command-line options *) + +val abs_val : int ref + +val reset_abs_val : unit -> unit + +(** Call f x with abs_val set to zero. + Restore the initial value also in case of exception. *) +val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b + +val allow_leak : bool ref +val arc_mode : bool ref +val curr_language : language ref + + +(** Command Line Interface Documentation *) + +val print_usage_exit : unit -> 'a diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 2d257b593..18a0c3094 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -254,7 +254,7 @@ module CheckJoinPre : InfoLossCheckerSig = struct | Sil.Lvar _ -> false | Sil.Var id when Ident.is_normal id -> IList.length es >= 1 | Sil.Var _ -> - if !Config.join_cond = 0 then + if Config.join_cond = 0 then IList.exists (Sil.exp_equal Sil.exp_zero) es else if Dangling.check side e then begin @@ -689,7 +689,7 @@ end = struct let get_other_atoms side atom_in = let build_other_atoms construct side e = - if !Config.trace_join then (L.d_str "build_other_atoms: "; Sil.d_exp e; L.d_ln ()); + if Config.trace_join then (L.d_str "build_other_atoms: "; Sil.d_exp e; L.d_ln ()); let others1 = get_others_direct_or_induced side e in let others2 = match others1 with None -> get_others_deep side e | Some _ -> others1 in match others2 with @@ -697,7 +697,7 @@ end = struct | Some (e_res, e_op) -> let a_res = construct e_res in let a_op = construct e_op in - if !Config.trace_join then begin + if Config.trace_join then begin L.d_str "build_other_atoms (successful) "; Sil.d_atom a_res; L.d_str ", "; Sil.d_atom a_op; L.d_ln () end; @@ -1392,7 +1392,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma) try let todo_curr = Todo.pop () in let e1, e2, e = todo_curr in - if !Config.trace_join then begin + if Config.trace_join then begin L.d_strln ".... sigma_partial_join' ...."; L.d_str "TODO: "; Sil.d_exp e1; L.d_str ","; Sil.d_exp e2; L.d_str ","; Sil.d_exp e; L.d_ln (); L.d_strln "SIGMA1 ="; Prop.d_sigma sigma1_in; L.d_ln (); @@ -1407,7 +1407,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma) | Some (Sil.Hlseg (k, _, _, _, _) as lseg), None | Some (Sil.Hdllseg (k, _, _, _, _, _, _) as lseg), None -> - if (not !Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then + if (not Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then let sigma_acc' = join_list_and_non Lhs e lseg e1 e2 :: sigma_acc in sigma_partial_join' mode sigma_acc' sigma1 sigma2 else @@ -1415,7 +1415,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma) | None, Some (Sil.Hlseg (k, _, _, _, _) as lseg) | None, Some (Sil.Hdllseg (k, _, _, _, _, _, _) as lseg) -> - if (not !Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then + if (not Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then let sigma_acc' = join_list_and_non Rhs e lseg e2 e1 :: sigma_acc in sigma_partial_join' mode sigma_acc' sigma1 sigma2 else @@ -1643,21 +1643,23 @@ let pi_partial_join mode | Sil.Aneq _ -> false | e -> Prop.atom_is_inequality e in begin - if !Config.trace_join then begin + if Config.trace_join then begin L.d_str "pi1: "; Prop.d_pi pi1; L.d_ln (); L.d_str "pi2: "; Prop.d_pi pi2; L.d_ln () end; let atom_list1 = let p2 = Prop.normalize ep2 in IList.fold_left (handle_atom_with_widening Lhs p2 pi2) [] pi1 in - if !Config.trace_join then (L.d_str "atom_list1: "; Prop.d_pi atom_list1; L.d_ln ()); + if Config.trace_join then (L.d_str "atom_list1: "; Prop.d_pi atom_list1; L.d_ln ()); let atom_list_combined = let p1 = Prop.normalize ep1 in IList.fold_left (handle_atom_with_widening Rhs p1 pi1) atom_list1 pi2 in - if !Config.trace_join then (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ()); + if Config.trace_join then + (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ()); let atom_list_filtered = IList.filter filter_atom atom_list_combined in - if !Config.trace_join then (L.d_str "atom_list_filtered: "; Prop.d_pi atom_list_filtered; L.d_ln ()); + if Config.trace_join then + (L.d_str "atom_list_filtered: "; Prop.d_pi atom_list_filtered; L.d_ln ()); let atom_list_res = IList.rev atom_list_filtered in atom_list_res @@ -2001,7 +2003,7 @@ let proplist_meet_generate plist = let propset_meet_generate_pre pset = let plist = Propset.to_proplist pset in - if !Config.meet_level = 0 then plist + if Config.meet_level = 0 then plist else let pset1 = proplist_meet_generate plist in let pset_new = Propset.diff pset1 pset in diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 6195035f9..53c77b581 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -1007,7 +1007,7 @@ let pp_cfgnode fmt (n: Cfg.Node.t) = let print_icfg fmt cfg = let print_node node = let loc = Cfg.Node.get_loc node in - if (!Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file !DB.current_source) then + if (Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file !DB.current_source) then F.fprintf fmt "%a\n" pp_cfgnode node in IList.iter print_node (Cfg.Node.get_all_nodes cfg) @@ -1019,7 +1019,10 @@ let print_edges fmt edges = IList.iter print_edge edges let print_icfg_dotty cfg (extra_edges : (Cfg.Node.t * Cfg.Node.t) list) = - let chan = open_out (DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [!Config.dotty_output])) in + let chan = + open_out + (DB.filename_to_string + (DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [Config.dotty_output])) in let fmt = Format.formatter_of_out_channel chan in F.fprintf fmt "digraph iCFG {\n"; print_icfg fmt cfg; diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 1f34a43cd..ee88c28f4 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -127,7 +127,7 @@ let find_normal_variable_funcall true | _ -> false in ignore (IList.exists find_declaration node_instrs); - if !verbose && !res == None + if verbose && !res == None then (L.d_str ("find_normal_variable_funcall could not find " ^ @@ -235,7 +235,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp let node_instrs = Cfg.Node.get_instrs node in let find_declaration = function | Sil.Letderef (id0, e, _, _) when Ident.equal id id0 -> - if !verbose + if verbose then (L.d_str "find_normal_variable_letderef defining "; Sil.d_exp e; L.d_ln ()); @@ -243,7 +243,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp true | Sil.Call ([id0], Sil.Const (Sil.Cfun pn), (e, _):: _, _, _) when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") -> - if !verbose + if verbose then (L.d_str "find_normal_variable_letderef cast on "; Sil.d_exp e; L.d_ln ()); @@ -251,7 +251,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp true | Sil.Call ([id0], (Sil.Const (Sil.Cfun pname) as fun_exp), args, loc, call_flags) when Ident.equal id id0 -> - if !verbose + if verbose then (L.d_str "find_normal_variable_letderef function call "; Sil.d_exp fun_exp; L.d_ln ()); @@ -269,7 +269,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp true | _ -> false in ignore (IList.exists find_declaration node_instrs); - if !verbose && !res == None + if verbose && !res == None then (L.d_str ("find_normal_variable_letderef could not find " ^ @@ -287,20 +287,20 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = let seen = Sil.ExpSet.add e _seen in match Prop.exp_normalize_noabs Sil.sub_empty e with | Sil.Const c -> - if !verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ()); Some (Sil.Dderef (Sil.Dconst c)) | Sil.BinOp(Sil.PlusPI, e1, e2) -> - if !verbose then (L.d_str "exp_lv_dexp: (e1 +PI e2) "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_lv_dexp: (e1 +PI e2) "; Sil.d_exp e; L.d_ln ()); (match _exp_lv_dexp seen node e1, _exp_rv_dexp seen node e2 with | Some de1, Some de2 -> Some (Sil.Dbinop(Sil.PlusPI, de1, de2)) | _ -> None) | Sil.Var id when Ident.is_normal id -> - if !verbose then (L.d_str "exp_lv_dexp: normal var "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_lv_dexp: normal var "; Sil.d_exp e; L.d_ln ()); (match _find_normal_variable_letderef seen node id with | None -> None | Some de -> Some (Sil.Dderef de)) | Sil.Lvar pvar -> - if !verbose then (L.d_str "exp_lv_dexp: program var "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_lv_dexp: program var "; Sil.d_exp e; L.d_ln ()); if pvar_is_frontend_tmp pvar then begin match find_program_variable_assignment node pvar with @@ -322,7 +322,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = end else Some (Sil.Dpvar pvar) | Sil.Lfield (Sil.Var id, f, _) when Ident.is_normal id -> - if !verbose then + if verbose then begin L.d_str "exp_lv_dexp: Lfield with var "; Sil.d_exp (Sil.Var id); @@ -333,7 +333,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = | None -> None | Some de -> Some (Sil.Darrow (de, f))) | Sil.Lfield (e1, f, _) -> - if !verbose then + if verbose then begin L.d_str "exp_lv_dexp: Lfield "; Sil.d_exp e1; @@ -344,7 +344,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = | None -> None | Some de -> Some (Sil.Ddot (de, f))) | Sil.Lindex (e1, e2) -> - if !verbose then + if verbose then begin L.d_str "exp_lv_dexp: Lindex "; Sil.d_exp e1; @@ -359,7 +359,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = Some (Sil.Darray (de1, Sil.Dunknown)) | Some de1, Some de2 -> Some (Sil.Darray (de1, de2))) | _ -> - if !verbose then (L.d_str "exp_lv_dexp: no match for "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_lv_dexp: no match for "; Sil.d_exp e; L.d_ln ()); None (** describe rvalue [e] as a dexp *) @@ -370,18 +370,18 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = let seen = Sil.ExpSet.add e _seen in match e with | Sil.Const c -> - if !verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ()); Some (Sil.Dconst c) | Sil.Lvar pv -> - if !verbose then (L.d_str "exp_rv_dexp: program var "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_rv_dexp: program var "; Sil.d_exp e; L.d_ln ()); if pvar_is_frontend_tmp pv then _exp_lv_dexp _seen (* avoid spurious cycle detection *) node e else Some (Sil.Dpvaraddr pv) | Sil.Var id when Ident.is_normal id -> - if !verbose then (L.d_str "exp_rv_dexp: normal var "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_rv_dexp: normal var "; Sil.d_exp e; L.d_ln ()); _find_normal_variable_letderef seen node id | Sil.Lfield (e1, f, _) -> - if !verbose then + if verbose then begin L.d_str "exp_rv_dexp: Lfield "; Sil.d_exp e1; @@ -392,7 +392,7 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = | None -> None | Some de -> Some (Sil.Ddot(de, f))) | Sil.Lindex (e1, e2) -> - if !verbose then + if verbose then begin L.d_str "exp_rv_dexp: Lindex "; Sil.d_exp e1; @@ -404,23 +404,23 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = | None, _ | _, None -> None | Some de1, Some de2 -> Some (Sil.Darray(de1, de2))) | Sil.BinOp (op, e1, e2) -> - if !verbose then (L.d_str "exp_rv_dexp: BinOp "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_rv_dexp: BinOp "; Sil.d_exp e; L.d_ln ()); (match _exp_rv_dexp seen node e1, _exp_rv_dexp seen node e2 with | None, _ | _, None -> None | Some de1, Some de2 -> Some (Sil.Dbinop (op, de1, de2))) | Sil.UnOp (op, e1, _) -> - if !verbose then (L.d_str "exp_rv_dexp: UnOp "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_rv_dexp: UnOp "; Sil.d_exp e; L.d_ln ()); (match _exp_rv_dexp seen node e1 with | None -> None | Some de1 -> Some (Sil.Dunop (op, de1))) | Sil.Cast (_, e1) -> - if !verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ()); _exp_rv_dexp seen node e1 | Sil.Sizeof (typ, sub) -> - if !verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ()); Some (Sil.Dsizeof (typ, sub)) | _ -> - if !verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ()); None let find_normal_variable_letderef = _find_normal_variable_letderef Sil.ExpSet.empty @@ -536,10 +536,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = | _ -> false in let value_str = match instro with | None -> - if !verbose then (L.d_str "explain_leak: no current instruction"; L.d_ln ()); + if verbose then (L.d_str "explain_leak: no current instruction"; L.d_ln ()); value_str_from_pvars_vpath [] vpath | Some (Sil.Nullify (pvar, _)) when check_pvar pvar -> - if !verbose + if verbose then (L.d_str "explain_leak: current instruction is Nullify for pvar "; Pvar.d pvar; L.d_ln ()); @@ -547,10 +547,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = | None -> None | Some de -> Some (Sil.dexp_to_string de)) | Some (Sil.Abstract _) -> - if !verbose then (L.d_str "explain_leak: current instruction is Abstract"; L.d_ln ()); + if verbose then (L.d_str "explain_leak: current instruction is Abstract"; L.d_ln ()); let get_nullify = function | Sil.Nullify (pvar, _) when check_pvar pvar -> - if !verbose + if verbose then (L.d_str "explain_leak: found nullify before Abstract for pvar "; Pvar.d pvar; L.d_ln ()); @@ -561,7 +561,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = IList.filter (fun pvar -> not (pvar_is_frontend_tmp pvar)) nullify_pvars in value_str_from_pvars_vpath nullify_pvars_notmp vpath | Some (Sil.Set (lexp, _, _, _)) when vpath = None -> - if !verbose + if verbose then (L.d_str "explain_leak: current instruction Set for "; Sil.d_exp lexp; L.d_ln ()); @@ -569,7 +569,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = | Some dexp -> Some (Sil.dexp_to_string dexp) | None -> None) | Some instr -> - if !verbose + if verbose then (L.d_str "explain_leak: case not matched in instr "; Sil.d_instr instr; L.d_ln()); @@ -584,13 +584,13 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = (* we don't know it's been allocated, but it's coming from list abstraction and we have a name *) Exceptions.Exn_user, bucket - else Exceptions.Exn_developer, Some (Mleak_buckets.ml_bucket_unknown_origin ()) in + else Exceptions.Exn_developer, Some Mleak_buckets.ml_bucket_unknown_origin in exn_cat, Localise.desc_leak hpred_typ_opt value_str resource_opt res_action_opt loc bucket (** find the dexp, if any, where the given value is stored also return the type of the value if found *) let vpath_find prop _exp : Sil.dexp option * Sil.typ option = - if !verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ()); + if verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ()); let rec find sigma_acc sigma_todo exp = let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with | Sil.Eexp (e, _) when Sil.exp_equal exp e -> @@ -613,7 +613,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option = | None, _ -> () | Some de, typo -> res := Some (Sil.Darrow (de, f)), typo) | lexp -> - if !verbose + if verbose then (L.d_str "vpath_find do_fse: no match on Eexp "; Sil.d_exp lexp; L.d_ln ())) @@ -632,7 +632,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option = | None, typo -> None, typo | Some de, typo -> Some (Sil.Dderef de), typo) | lexp -> - if !verbose + if verbose then (L.d_str "vpath_find do_sexp: no match on Eexp "; Sil.d_exp lexp; L.d_ln ()); @@ -665,7 +665,7 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option = | Some de, typo -> Some de, typo | None, _ -> find (hpred:: sigma_acc) sigma_todo' exp) in let res = find [] (Prop.get_sigma prop) _exp in - if !verbose then begin + if verbose then begin match res with | None, _ -> L.d_str "vpath_find: cannot find "; Sil.d_exp _exp; L.d_ln () | Some de, typo -> L.d_str "vpath_find: found "; L.d_str (Sil.dexp_to_string de); L.d_str " : "; @@ -683,7 +683,7 @@ let explain_dexp_access prop dexp is_nullable = | None -> None | Some (Sil.Eexp (_, inst)) -> Some inst | Some se -> - if !verbose then (L.d_str "sexpo_to_inst: can't find inst "; Sil.d_sexp se; L.d_ln()); + if verbose then (L.d_str "sexpo_to_inst: can't find inst "; Sil.d_sexp se; L.d_ln()); None in let find_ptsto (e : Sil.exp) : Sil.strexp option = let res = ref None in @@ -695,7 +695,7 @@ let explain_dexp_access prop dexp is_nullable = !res in let rec lookup_fld fsel f = match fsel with | [] -> - if !verbose + if verbose then (L.d_strln ("lookup_fld: can't find field " ^ Ident.fieldname_to_string f)); None @@ -704,7 +704,7 @@ let explain_dexp_access prop dexp is_nullable = else lookup_fld fsel' f in let rec lookup_esel esel e = match esel with | [] -> - if !verbose then (L.d_str "lookup_esel: can't find index "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "lookup_esel: can't find index "; Sil.d_exp e; L.d_ln ()); None | (e1, se):: esel' -> if Sil.exp_equal e1 e then Some se @@ -718,7 +718,7 @@ let explain_dexp_access prop dexp is_nullable = | Some Sil.Earray (_, esel, _), Some Sil.Eexp (e, _) -> lookup_esel esel e | Some se1, Some se2 -> - if !verbose + if verbose then (L.d_str "lookup: case not matched on Darray "; Sil.d_sexp se1; L.d_str " "; Sil.d_sexp se2; L.d_ln()); @@ -729,7 +729,7 @@ let explain_dexp_access prop dexp is_nullable = | Some Sil.Estruct (fsel, _) -> lookup_fld fsel f | Some _ -> - if !verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ()); + if verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ()); None) | Sil.Ddot (de1, f) -> (match lookup de1 with @@ -737,10 +737,10 @@ let explain_dexp_access prop dexp is_nullable = | Some Sil.Estruct (fsel, _) -> lookup_fld fsel f | Some _ -> - if !verbose then (L.d_str "lookup: case not matched on Ddot "; L.d_ln ()); + if verbose then (L.d_str "lookup: case not matched on Ddot "; L.d_ln ()); None) | Sil.Dpvar pvar -> - if !verbose then (L.d_str "lookup: found Dpvar "; L.d_ln ()); + if verbose then (L.d_str "lookup: found Dpvar "; L.d_ln ()); (find_ptsto (Sil.Lvar pvar)) | Sil.Dderef de -> (match lookup de with @@ -748,24 +748,24 @@ let explain_dexp_access prop dexp is_nullable = | Some (Sil.Eexp (e, _)) -> find_ptsto e | Some _ -> None) | (Sil.Dbinop(Sil.PlusPI, Sil.Dpvar _, Sil.Dconst _) as de) -> - if !verbose then (L.d_strln ("lookup: case )pvar + constant) " ^ Sil.dexp_to_string de)); + if verbose then (L.d_strln ("lookup: case )pvar + constant) " ^ Sil.dexp_to_string de)); None | Sil.Dfcall (Sil.Dconst c, _, loc, _) -> - if !verbose then (L.d_strln "lookup: found Dfcall "); + if verbose then (L.d_strln "lookup: found Dfcall "); (match c with | Sil.Cfun _ -> (* Treat function as an update *) Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Location.line)) | _ -> None) | Sil.Dretcall (Sil.Dconst (Sil.Cfun pname as c ) , _, loc, _ ) when method_of_pointer_wrapper pname -> - if !verbose then (L.d_strln "lookup: found Dretcall "); + if verbose then (L.d_strln "lookup: found Dretcall "); Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_pointer_wrapper_call loc.Location.line)) | de -> - if !verbose then (L.d_strln ("lookup: unknown case not matched " ^ Sil.dexp_to_string de)); + if verbose then (L.d_strln ("lookup: unknown case not matched " ^ Sil.dexp_to_string de)); None in let access_opt = match sexpo_to_inst (lookup dexp) with | None -> - if !verbose + if verbose then (L.d_strln ("explain_dexp_access: cannot find inst of " ^ Sil.dexp_to_string dexp)); None @@ -780,7 +780,7 @@ let explain_dexp_access prop dexp is_nullable = | Some Sil.Ialloc when !Config.curr_language = Config.Java -> Some Localise.Initialized_automatically | Some inst -> - if !verbose + if verbose then (L.d_strln ("explain_dexp_access: inst is not an update " ^ @@ -830,7 +830,7 @@ let create_dereference_desc | _ -> access_opt in let desc = Localise.dereference_string deref_str value_str access_opt' loc in let desc = - if !Config.curr_language = Config.C_CPP && not is_premature_nil then + if !Config.curr_language = Config.Clang && not is_premature_nil then match de_opt with | Some (Sil.Dpvar pvar) | Some (Sil.Dpvaraddr pvar) -> @@ -855,60 +855,60 @@ let _explain_access deref_str prop loc = let rec find_outermost_dereference node e = match e with | Sil.Const _ -> - if !verbose then (L.d_str "find_outermost_dereference: constant "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "find_outermost_dereference: constant "; Sil.d_exp e; L.d_ln ()); exp_lv_dexp node e | Sil.Var id when Ident.is_normal id -> (* look up the normal variable declaration *) - if !verbose + if verbose then (L.d_str "find_outermost_dereference: normal var "; Sil.d_exp e; L.d_ln ()); find_normal_variable_letderef node id | Sil.Lfield (e', _, _) -> - if !verbose then (L.d_str "find_outermost_dereference: Lfield "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "find_outermost_dereference: Lfield "; Sil.d_exp e; L.d_ln ()); find_outermost_dereference node e' | Sil.Lindex(e', _) -> - if !verbose then (L.d_str "find_outermost_dereference: Lindex "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "find_outermost_dereference: Lindex "; Sil.d_exp e; L.d_ln ()); find_outermost_dereference node e' | Sil.Lvar _ -> - if !verbose then (L.d_str "find_outermost_dereference: Lvar "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "find_outermost_dereference: Lvar "; Sil.d_exp e; L.d_ln ()); exp_lv_dexp node e | Sil.BinOp(Sil.PlusPI, Sil.Lvar _, _) -> - if !verbose + if verbose then (L.d_str "find_outermost_dereference: Lvar+index "; Sil.d_exp e; L.d_ln ()); exp_lv_dexp node e | Sil.Cast (_, e') -> - if !verbose then (L.d_str "find_outermost_dereference: cast "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "find_outermost_dereference: cast "; Sil.d_exp e; L.d_ln ()); find_outermost_dereference node e' | Sil.BinOp(Sil.PtrFld, _, e') -> - if !verbose then (L.d_str "find_outermost_dereference: PtrFld "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "find_outermost_dereference: PtrFld "; Sil.d_exp e; L.d_ln ()); find_outermost_dereference node e' | _ -> - if !verbose + if verbose then (L.d_str "find_outermost_dereference: no match for "; Sil.d_exp e; L.d_ln ()); None in let find_exp_dereferenced () = match State.get_instr () with | Some Sil.Set (e, _, _, _) -> - if !verbose then (L.d_str "explain_dereference Sil.Set "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "explain_dereference Sil.Set "; Sil.d_exp e; L.d_ln ()); Some e | Some Sil.Letderef (_, e, _, _) -> - if !verbose then (L.d_str "explain_dereference Sil.Leteref "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "explain_dereference Sil.Leteref "; Sil.d_exp e; L.d_ln ()); Some e | Some Sil.Call (_, Sil.Const (Sil.Cfun fn), [(e, _)], _, _) when Procname.to_string fn = "free" -> - if !verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ()); Some e | Some Sil.Call (_, (Sil.Var _ as e), _, _, _) -> - if !verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ()); + if verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ()); Some e | _ -> None in let node = State.get_node () in match find_exp_dereferenced () with | None -> - if !verbose then L.d_strln "_explain_access: find_exp_dereferenced returned None"; + if verbose then L.d_strln "_explain_access: find_exp_dereferenced returned None"; Localise.no_desc | Some e -> L.d_strln "Finding deref'd exp"; @@ -1015,7 +1015,7 @@ let explain_dereference_as_caller_expression find 1 formal_params in match find_with_exp spec_pre exp with | Some (pv, pvar_off) -> - if !verbose then L.d_strln ("pvar: " ^ (Pvar.to_string pv)); + if verbose then L.d_strln ("pvar: " ^ (Pvar.to_string pv)); let pv_name = Pvar.get_name pv in if Pvar.is_global pv then @@ -1023,14 +1023,14 @@ let explain_dereference_as_caller_expression create_dereference_desc ~use_buckets dexp deref_str actual_pre loc else if Pvar.is_callee pv then let position = find_formal_param_number pv_name in - if !verbose then L.d_strln ("parameter number: " ^ string_of_int position); + if verbose then L.d_strln ("parameter number: " ^ string_of_int position); explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off else if Prop.has_dangling_uninit_attribute spec_pre exp then Localise.desc_uninitialized_dangling_pointer_deref deref_str (Pvar.to_string pv) loc else Localise.no_desc | None -> - if !verbose + if verbose then (L.d_str "explain_dereference_as_caller_expression "; Sil.d_exp exp; L.d_str ": cannot explain None "; L.d_ln ()); Localise.no_desc @@ -1141,7 +1141,7 @@ let explain_null_test_after_dereference exp node line loc = | None -> Localise.no_desc let _warning loc fmt fmt_string = - if !Config.developer_mode then + if Config.developer_mode then begin F.fprintf fmt "%s:%d: Warning: " (DB.source_file_to_string !DB.current_source) loc.Location.line; diff --git a/infer/src/backend/errlog.ml b/infer/src/backend/errlog.ml index 515f26222..f0ca191e6 100644 --- a/infer/src/backend/errlog.ml +++ b/infer/src/backend/errlog.ml @@ -175,17 +175,17 @@ let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn = | Some ekind -> ekind | _ -> _ekind in let hide_java_loc_zero = (* hide java errors at location zero unless in -developer_mode *) - !Config.developer_mode = false && + Config.developer_mode = false && !Config.curr_language = Config.Java && loc.Location.line = 0 in let hide_memory_error = match Localise.error_desc_get_bucket desc with - | Some bucket when bucket = (Mleak_buckets.ml_bucket_unknown_origin ()) -> - not (Mleak_buckets.should_raise_leak_unknown_origin ()) + | Some bucket when bucket = Mleak_buckets.ml_bucket_unknown_origin -> + not Mleak_buckets.should_raise_leak_unknown_origin | _ -> false in let log_it = visibility == Exceptions.Exn_user || - (!Config.developer_mode && visibility == Exceptions.Exn_developer) in + (Config.developer_mode && visibility == Exceptions.Exn_developer) in if log_it && not hide_java_loc_zero && not hide_memory_error then begin let added = add_issue err_log diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml index 93fcda3c1..08b6e3449 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -88,7 +88,7 @@ exception Wrong_argument_number of L.ml_loc (** Turn an exception into a descriptive string, error description, location in ml source, and category *) let recognize_exception exn = let filter_out_bucket desc = - !Config.filter_buckets && + Config.filter_buckets && match Localise.error_desc_get_bucket desc with | None -> false | Some bucket -> bucket <> Localise.BucketLevel.b1 in @@ -101,7 +101,7 @@ let recognize_exception exn = (Localise.context_leak, desc, None, Exn_user, High, None, Nocat) | Analysis_stops (desc, ml_loc_opt) -> - let visibility = if !Config.analysis_stops then Exn_user else Exn_developer in + let visibility = if Config.analysis_stops then Exn_user else Exn_developer in (Localise.analysis_stops, desc, ml_loc_opt, visibility, Medium, None, Nocat) | Array_of_pointsto ml_loc -> (Localise.from_string "Array_of_pointsto", diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 2f9802db4..7e580fdc1 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -15,233 +15,13 @@ open! Utils module L = Logging module F = Format -(** command line option: if true, run the analysis in checker mode *) -let checkers = ref false - -(** command line option: name of the makefile to create with clusters and dependencies *) -let makefile_cmdline = ref "" - -(** optional command-line name of the .cluster file *) -let cluster_cmdline = ref None - -(** value of -out_file command-line *) -let out_file_cmdline = ref "" - -(** value of -err_file command-line *) -let err_file_cmdline = ref "" - -(** List of obj memory leak buckets to be checked in Objective-C/C++ *) -let ml_buckets_arg = ref "cf" - -(** Whether specs can be cleaned up before starting analysis *) -let allow_specs_cleanup = ref false - -let version_string () = - "Infer version " - ^ Version.versionString - ^ "\nCopyright 2009 - present Facebook. All Rights Reserved.\n" - -let print_version () = - F.fprintf F.std_formatter "%s@." (version_string ()); - exit 0 - -let print_version_json () = - F.fprintf F.std_formatter "%s@." Version.versionJson; - exit 0 - -let arg_desc = - let base_arg = - let desc = - base_arg_desc @ - [ - "-err_file", - Arg.Set_string err_file_cmdline, - Some "file", - "use file for the err channel" - ; - "-iterations", - Arg.Set_int Config.iterations, - Some "n", - "set the max number of operations for each function, \ - expressed as a multiple of symbolic operations (default n=1)" - ; - "-nonstop", - Arg.Set Config.nonstop, - None, - "activate the nonstop mode: the analysis continues after finding errors. \ - With this option the analysis can become less precise." - ; - "-out_file", - Arg.Set_string out_file_cmdline, - Some "file", - "use file for the out channel" - ; - "-print_builtins", - Arg.Unit Builtin.print_and_exit, - None, - "print the builtin functions and exit" - ; - "-reactive", - Arg.Unit (fun () -> Config.reactive_mode := true), - None, - "analyze in reactive propagation mode starting from changed files" - ; - "-continue", - Arg.Set Config.continue_capture, - None, - "continue the capture for the reactive analysis,\ - increasing the changed files/procedures." - ; - (* TODO: merge with the -project_root option *) - "-java", - Arg.Unit (fun () -> Config.curr_language := Config.Java), - None, - "Set language to Java" - ; - "-version", - Arg.Unit print_version, - None, - "print version information and exit" - ; - "-version_json", - Arg.Unit print_version_json, - None, - "print version json formatted" - ; - "-objcm", - Arg.Set Config.objc_memory_model_on, - None, - "Use ObjC memory model" - ; - "-no_progress_bar", - Arg.Unit (fun () -> Config.show_progress_bar := false), - None, - "Do not show a progress bar" - ; - "-ml_buckets", - Arg.Set_string ml_buckets_arg, - Some "ml_buckets", - "memory leak buckets to be checked, separated by commas. \ - The possible buckets are cf (Core Foundation), arc, narc (No arc), cpp, unknown_origin" - ; - ] in - Arg.create_options_desc false "Analysis Options" desc in - let reserved_arg = - let desc = - reserved_arg_desc @ - [ - "-allow_specs_cleanup", - Arg.Unit (fun () -> allow_specs_cleanup := true), - None, - "Allow to remove existing specs before running analysis when it's not incremental" - ; - "-analysis_stops", - Arg.Set Config.analysis_stops, - None, - "issue a warning when the analysis stops" - ; - "-angelic_execution", - Arg.Set Config.angelic_execution, - None, - "activate angelic execution: \ - The analysis ignores errors caused by unknown procedure calls." - ; - "-checkers", - Arg.Unit (fun () -> checkers := true), - None, - " run only the checkers instead of the full analysis" - ; - "-cluster", - Arg.String (fun s -> cluster_cmdline := Some s), - Some "fname", - "specify a .cluster file to be analyzed" - ; - "-codequery", - Arg.String (fun s -> CodeQuery.query := Some s), - Some "query", - " execute the code query" - ; - "-eradicate", - Arg.Unit (fun () -> - Config.eradicate := true; - checkers := true), - None, - " activate the eradicate checker for java annotations" - ; - "-merge", - Arg.Set Config.merge, - None, - "merge the captured results directories specified in the dependency file" - ; - "-makefile", - Arg.Set_string makefile_cmdline, - Some "file", - "create a makefile to perform the analysis" - ; - "-modified_targets", - Arg.String (fun file -> MergeCapture.modified_file file), - Some "file", - "read the file of buck targets modified since the last analysis" - ; - "-optimistic_cast", - Arg.Set Config.optimistic_cast, - None, - "allow cast of undefined values" - ; - "-print_buckets", - Arg.Unit (fun() -> Config.show_buckets := true; Config.show_ml_buckets := true), - None, - "Add buckets to issue descriptions, useful when developing infer" - ; - "-seconds_per_iteration", - Arg.Set_float Config.seconds_per_iteration, - Some "n", - "set the number of seconds per iteration (default n=30)" - ; - "-subtype_multirange", - Arg.Set Config.subtype_multirange, - None, - "use the multirange subtyping domain" - ; - "-symops_per_iteration", - Arg.Set_int Config.symops_per_iteration, - Some "n", - "set the number of symbolic operations per iteration (default n=" - ^ (string_of_int !Config.symops_per_iteration) ^ ")" - ; - "-tracing", - Arg.Unit (fun () -> Config.report_runtime_exceptions := true), - None, - "Report error traces for runtime exceptions (Only for Java)" - ; - "-type_size", - Arg.Set Config.type_size, - None, - "consider the size of types during analysis" - ; - ] in - Arg.create_options_desc false - "Reserved Options: Experimental features, use with caution!" desc in - base_arg @ reserved_arg - -let usage = - (version_string ()) ^ "\ - Usage: InferAnalyze [options]\n\ - Analyze the files captured in the project results directory, \ - which can be specified with the -results_dir option." - -let print_usage_exit () = - Arg.usage arg_desc usage; - exit(1) - -let () = (* parse command-line arguments *) - let f _ = - () (* ignore anonymous arguments *) in - Arg.parse "INFER_ARGS" arg_desc f usage; - if not (Sys.file_exists !Config.results_dir) then +let () = + if Config.print_builtins then Builtin.print_and_exit () ; + (match Config.modified_targets with Some file -> MergeCapture.modified_file file | None -> ()) ; + if not (Sys.file_exists Config.results_dir) then begin - L.err "ERROR: results directory %s does not exist@.@." !Config.results_dir; - print_usage_exit () + L.err "ERROR: results directory %s does not exist@.@." Config.results_dir; + Config.print_usage_exit () end let analyze_exe_env exe_env = @@ -250,7 +30,7 @@ let analyze_exe_env exe_env = Specs.clear_spec_tbl (); Random.self_init (); let line_reader = Printer.LineReader.create () in - if !checkers then + if Config.checkers then begin (** run the checkers only *) let call_graph = Exe_env.get_cg exe_env in @@ -299,7 +79,7 @@ let close_output_file = function | Some (_, cout) -> close_out cout let setup_logging () = - if !Config.developer_mode then + if Config.developer_mode then let log_dir_name = "log" in let analyzer_out_name = "analyzer_out" in let analyzer_err_name = "analyzer_err" in @@ -308,18 +88,18 @@ let setup_logging () = (DB.Results_dir.path_to_filename DB.Results_dir.Abs_root [log_dir_name]) in DB.create_dir log_dir; let analyzer_out_file = - if !out_file_cmdline = "" then Filename.concat log_dir analyzer_out_name - else !out_file_cmdline in + if Config.out_file_cmdline = "" then Filename.concat log_dir analyzer_out_name + else Config.out_file_cmdline in let analyzer_err_file = - if !err_file_cmdline = "" then Filename.concat log_dir analyzer_err_name - else !err_file_cmdline in + if Config.err_file_cmdline = "" then Filename.concat log_dir analyzer_err_name + else Config.err_file_cmdline in let analyzer_out_of = open_output_file Logging.set_out_formatter analyzer_out_file in let analyzer_err_of = open_output_file Logging.set_err_formatter analyzer_err_file in analyzer_out_of, analyzer_err_of else None, None let teardown_logging analyzer_out_of analyzer_err_of = - if !Config.developer_mode then + if Config.developer_mode then begin L.flush_streams (); close_output_file analyzer_out_of; @@ -337,11 +117,11 @@ let output_json_makefile_stats clusters = ("procedures", `Int num_procs); ("lines", `Int num_lines) ] in (* write stats file to disk, intentionally overwriting old file if it already exists *) - let f = open_out (Filename.concat !Config.results_dir Config.proc_stats_filename) in + let f = open_out (Filename.concat Config.results_dir Config.proc_stats_filename) in Yojson.Basic.pretty_to_channel f file_stats let print_prolog () = - match !cluster_cmdline with + match Config.cluster_cmdline with | None -> L.stdout "Starting analysis (Infer version %s)@." Version.versionString; | Some clname -> L.stdout "Cluster %s@." clname @@ -354,45 +134,43 @@ let process_cluster_cmdline fname = analyze_cluster (nr - 1) cluster let register_perf_stats_report () = - let stats_dir = Filename.concat !Config.results_dir Config.backend_stats_dir_name in - let cluster = match !cluster_cmdline with Some cl -> "_" ^ (Filename.basename cl) | None -> "" in - let stats_file = Filename.concat stats_dir (Config.perf_stats_prefix ^ cluster ^ ".json") in - DB.create_dir !Config.results_dir ; + let stats_dir = Filename.concat Config.results_dir Config.backend_stats_dir_name in + let cluster = match Config.cluster_cmdline with Some cl -> "_" ^ cl | None -> "" in + let stats_base = Config.perf_stats_prefix ^ "_" ^ (Filename.basename cluster) ^ ".json" in + let stats_file = Filename.concat stats_dir stats_base in + DB.create_dir Config.results_dir ; DB.create_dir stats_dir ; PerfStats.register_report_at_exit stats_file let () = register_perf_stats_report () ; - if !Config.developer_mode then + if Config.developer_mode then Printexc.record_backtrace true; print_prolog (); RegisterCheckers.register (); - if !allow_specs_cleanup = true && !cluster_cmdline = None then + if Config.allow_specs_cleanup = true && Config.cluster_cmdline = None then DB.Results_dir.clean_specs_dir (); let analyzer_out_of, analyzer_err_of = setup_logging () in - if !Config.curr_language = Config.C_CPP - then Mleak_buckets.init_buckets !ml_buckets_arg; - let finish_logging () = teardown_logging analyzer_out_of analyzer_err_of in - match !cluster_cmdline with + match Config.cluster_cmdline with | Some fname -> process_cluster_cmdline fname; finish_logging () | None -> - if !Config.merge then MergeCapture.merge_captured_targets (); + if Config.merge then MergeCapture.merge_captured_targets (); let clusters = DB.find_source_dirs () in L.err "Found %d source files in %s@." - (IList.length clusters) !Config.results_dir; + (IList.length clusters) Config.results_dir; - if !makefile_cmdline <> "" + if Config.makefile_cmdline <> "" then - ClusterMakefile.create_cluster_makefile clusters !makefile_cmdline + ClusterMakefile.create_cluster_makefile clusters Config.makefile_cmdline else begin IList.iteri diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml index 2f10952de..5f24fc67f 100644 --- a/infer/src/backend/inferconfig.ml +++ b/infer/src/backend/inferconfig.ml @@ -338,9 +338,9 @@ let disabled_checks_by_default = [ ] let inferconfig () = - match !Config.inferconfig_home with - | Some dir -> Filename.concat dir Config.inferconfig_file - | None -> Config.inferconfig_file + match Config.inferconfig_home, Config.project_root with + | Some dir, _ | _, Some dir -> Filename.concat dir Config.inferconfig_file + | None, None -> Config.inferconfig_file let load_filters analyzer = let inferconfig_file = inferconfig () in @@ -386,7 +386,6 @@ let filters_from_inferconfig inferconfig : filters = (* Create filters based on .inferconfig *) (* The environment varialble NO_PATH_FILTERING disables path filtering. *) let create_filters analyzer = - Config.project_root := Some (Sys.getcwd ()); if Config.from_env_variable "NO_PATH_FILTERING" then do_not_filter else match load_filters (Utils.string_of_analyzer analyzer) with @@ -420,7 +419,6 @@ let is_checker_enabled checker_name = (* are of the form: path/to/file.java -> {infer, eradicate} meaning that analysis results will *) (* be reported on path/to/file.java both for infer and for eradicate *) let test () = - Config.project_root := Some (Sys.getcwd ()); let filters = IList.map (fun analyzer -> (analyzer, create_filters analyzer)) analyzers in let matching_analyzers path = diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index 04219d8c1..b4d68309c 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -14,69 +14,8 @@ module L = Logging module F = Format open Jsonbug_j -(** Outfile to save the latex report *) -let latex = ref None - -(** command line flag: if true, print whole seconds only *) -let whole_seconds = ref false - -(** Outfile to save bugs stats in csv format *) -let bugs_csv = ref None - -(** Outfile to save bugs stats in JSON format *) -let bugs_json = ref None - -(** Outfile to save bugs stats in txt format *) -let bugs_txt = ref None - -(** Outfile to save bugs stats in xml format *) -let bugs_xml = ref None - -(** Outfile to save procedures stats in csv format *) -let procs_csv = ref None - -(** Outfile to save procedures stats in xml format *) -let procs_xml = ref None - -(** Outfile to save call stats in csv format *) -let calls_csv = ref None - -(** Outfile to save the analysis report *) -let report = ref None - -(** command line flag: if true, produce a svg file *) -let svg = ref false - -(** command line flag: if true, export specs to xml files *) -let xml_specs = ref false - -(** command line flag: if true, produce unit test for each spec *) -let unit_test = ref false - -(** command line flag: if true, do not print the spec to standard output *) -let quiet = ref false - -(** command line flag: if true, print stats about preconditions to standard output *) -let precondition_stats = ref false - -(** name of the file to load analysis results from *) -let load_analysis_results = ref None - -(** If true then include Infer source code locations in json reports *) -let reports_include_ml_loc = ref false - -(** name of the file to load save results to *) -let save_analysis_results = ref None - -(** command-line option to print the location of the copy of a source file *) let source_file_copy = ref None -(** command line option to test the filtering based on .inferconfig *) -let test_filtering = ref false - -(** Setup the analyzer in order to filter out errors for this analyzer only *) -let analyzer = ref None - let handle_source_file_copy_option () = match !source_file_copy with | None -> () | Some source_file -> @@ -88,157 +27,9 @@ let canonic_path_from_string s = if s = Filename.dir_sep then s else Filename.concat (Filename.dirname s) (Filename.basename s) ^ Filename.dir_sep -let arg_desc = - let base_arg = - let desc = - [ - "-bugs", - Arg.String (fun s -> bugs_csv := create_outfile s), - Some "bugs.csv", - "create file bugs.csv containing a list of bugs in CSV format" - ; - "-bugs_json", - Arg.String (fun s -> bugs_json := create_outfile s), - Some "bugs.json", - "create file bugs.json containing a list of bugs in JSON format" - ; - "-bugs_txt", - Arg.String (fun s -> bugs_txt := create_outfile s), - Some "bugs.txt", - "create file bugs.txt containing a list of bugs in text format" - ; - "-bugs_xml", - Arg.String (fun s -> bugs_xml := create_outfile s), - Some "bugs.xml", - "create file bugs.xml containing a list of bugs in XML format" - ; - "-calls", - Arg.String (fun s -> calls_csv := create_outfile s), - Some "calls.csv", - "write individual calls in csv format to file.csv" - ; - "-load_results", - Arg.String (fun s -> load_analysis_results := Some s), - Some "file.iar", - "load analysis results from Infer Analysis Results file file.iar" - ; - "-procs", - Arg.String (fun s -> procs_csv := create_outfile s), - Some "procs.csv", - "create file procs.csv containing statistics for each procedure in CSV format" - ; - "-procs_xml", - Arg.String (fun s -> procs_xml := create_outfile s), - Some "procs.xml", - "create file procs.xml containing statistics for each procedure in XML format" - ; - "-results_dir", - Arg.String (fun s -> Config.results_dir := s), - Some "dir", - "read all the .specs files in the results dir" - ; - "-lib", - Arg.String (fun s -> - Config.specs_library := filename_to_absolute s :: !Config.specs_library), - Some "dir", - "add dir to the list of directories to be searched for spec files" - ; - "-q", - Arg.Set quiet, - None, - "quiet: do not print specs on standard output" - ; - "-save_results", - Arg.String (fun s -> save_analysis_results := Some s), - Some "file.iar", - "save analysis results to Infer Analysis Results file file.iar" - ; - "-unit_test", - Arg.Set unit_test, - None, - "print unit test code" - ; - "-xml", - Arg.Set xml_specs, - None, - "export specs into XML files file1.xml ... filen.xml" - ; - "-test_filtering", - Arg.Set test_filtering, - None, - "list all the files Infer can report on (should be call at the root of the procject, \ - where .inferconfig lives)." - ; - "-analyzer", - Arg.String (fun s -> analyzer := Some (Utils.analyzer_of_string s)), - Some "analyzer", - "setup the analyzer for the path filtering" - ; - "-inferconfig_home", - Arg.String (fun s -> Config.inferconfig_home := Some s), - Some "dir", - "Path to the .inferconfig file" - ; - "-with_infer_src_loc", - Arg.Set reports_include_ml_loc, - None, - "include the location (in the Infer source code) from where reports are generated" - ; - ] in - Arg.create_options_desc false "Options" desc in - let reserved_arg = - let desc = - [ - "-latex", - Arg.String (fun s -> latex := create_outfile s), - Some "file.tex", - "print latex report to file.tex" - ; - "-print_types", - Arg.Set Config.print_types, - None, - "print types in symbolic heaps" - ; - "-precondition_stats", - Arg.Set precondition_stats, - None, - "print stats about preconditions to standard output" - ; - "-report", - Arg.String (fun s -> report := create_outfile s), - Some "report_file", - "create file report_file containing a report of the analysis results" - ; - "-source_file_copy", - Arg.String (fun s -> source_file_copy := Some (DB.abs_source_file_from_path s)), - Some "source_file", - "print the path of the copy of source_file in the results directory" - ; - "-svg", - Arg.Set svg, - None, - "generate .dot and .svg" - ; - "-whole_seconds", - Arg.Set whole_seconds, - None, - "print whole seconds only" - ; - ] in - Arg.create_options_desc false "Reserved Options" desc in - base_arg @ reserved_arg - -let usage = - "Usage: InferPrint [options] name1.specs ... namen.specs\n\ - Read, convert, and print .specs files. \ - To process all the .specs in the current directory, pass . as only parameter \ - To process all the .specs in the results directory, use option -results_dir \ - Each spec is printed to standard output unless option -q is used." - let print_usage_exit err_s = L.err "Load Error: %s@.@." err_s; - Arg.usage arg_desc usage; - exit(1) + Config.print_usage_exit () (** return the list of the .specs files in the results dir and libs, if they're defined *) let load_specfiles () = @@ -250,7 +41,7 @@ let load_specfiles () = IList.filter is_specs_file all_filepaths in let specs_dirs = let result_specs_dir = DB.filename_to_string (DB.Results_dir.specs_dir ()) in - result_specs_dir :: !Config.specs_library in + result_specs_dir :: Config.specs_library in IList.flatten (IList.map specs_files_in_dir specs_dirs) (** Create and initialize latex file *) @@ -265,7 +56,7 @@ let write_summary_latex fmt summary = let proc_name = Specs.get_proc_name summary in Latex.pp_section fmt ("Analysis of function " ^ (Latex.convert_string (Procname.to_string proc_name))); - F.fprintf fmt "@[%a@]" (Specs.pp_summary (pe_latex Black) !whole_seconds) summary + F.fprintf fmt "@[%a@]" (Specs.pp_summary (pe_latex Black) Config.whole_seconds) summary let error_desc_to_csv_string error_desc = let pp fmt () = F.fprintf fmt "%a" Localise.pp_error_desc error_desc in @@ -591,7 +382,7 @@ module BugsJson = struct let file = DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in let json_ml_loc = match ml_loc_opt with - | Some (file, lnum, cnum, enum) when !reports_include_ml_loc -> + | Some (file, lnum, cnum, enum) when Config.reports_include_ml_loc -> Some Jsonbug_j.{ file; lnum; cnum; enum; } | _ -> None in let bug = { @@ -969,30 +760,30 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna let base = DB.chop_extension (DB.filename_from_string fname) in let pp_simple_saved = !Config.pp_simple in Config.pp_simple := true; - if !quiet then () + if Config.quiet then () else L.out "Procedure: %a@\n%a@." - Procname.pp proc_name (Specs.pp_summary pe_text !whole_seconds) summary; + Procname.pp proc_name (Specs.pp_summary pe_text Config.whole_seconds) summary; let error_filter error_desc error_name = let always_report () = Localise.error_desc_extract_tag_value error_desc "always_report" = "true" in - (!Config.write_html || not (Localise.equal error_name Localise.skip_function)) && + (Config.write_html || not (Localise.equal error_name Localise.skip_function)) && (filters.Inferconfig.path_filter summary.Specs.attributes.ProcAttributes.loc.Location.file || always_report ()) && filters.Inferconfig.error_filter error_name && filters.Inferconfig.proc_filter proc_name in - do_outf procs_csv (fun outf -> ProcsCsv.pp_summary top_proc_set outf.fmt summary); - do_outf calls_csv (fun outf -> CallsCsv.pp_calls outf.fmt summary); - do_outf procs_xml (fun outf -> ProcsXml.pp_proc top_proc_set outf.fmt summary); - do_outf bugs_csv (fun outf -> BugsCsv.pp_bugs error_filter outf.fmt summary); - do_outf bugs_json (fun outf -> BugsJson.pp_bugs error_filter outf.fmt summary); - do_outf bugs_txt (fun outf -> BugsTxt.pp_bugs error_filter outf.fmt summary); - do_outf bugs_xml (fun outf -> BugsXml.pp_bugs error_filter linereader outf.fmt summary); - do_outf report (fun _ -> Stats.process_summary error_filter summary linereader stats); - if !precondition_stats then PreconditionStats.do_summary proc_name summary; - if !unit_test then UnitTest.print_unit_test proc_name summary; + do_outf Config.procs_csv (fun outf -> ProcsCsv.pp_summary top_proc_set outf.fmt summary); + do_outf Config.calls_csv (fun outf -> CallsCsv.pp_calls outf.fmt summary); + do_outf Config.procs_xml (fun outf -> ProcsXml.pp_proc top_proc_set outf.fmt summary); + do_outf Config.bugs_csv (fun outf -> BugsCsv.pp_bugs error_filter outf.fmt summary); + do_outf Config.bugs_json (fun outf -> BugsJson.pp_bugs error_filter outf.fmt summary); + do_outf Config.bugs_txt (fun outf -> BugsTxt.pp_bugs error_filter outf.fmt summary); + do_outf Config.bugs_xml (fun outf -> BugsXml.pp_bugs error_filter linereader outf.fmt summary); + do_outf Config.report (fun _ -> Stats.process_summary error_filter summary linereader stats); + if Config.precondition_stats then PreconditionStats.do_summary proc_name summary; + if Config.unit_test then UnitTest.print_unit_test proc_name summary; Config.pp_simple := pp_simple_saved; - do_outf latex (fun outf -> write_summary_latex outf.fmt summary); - if !svg then begin + do_outf Config.latex (fun outf -> write_summary_latex outf.fmt summary); + if Config.svg then begin let specs = Specs.get_specs_from_payload summary in let dot_file = DB.filename_add_suffix base ".dot" in let svg_file = DB.filename_add_suffix base ".svg" in @@ -1008,14 +799,14 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna "\" >\"" ^ (DB.filename_to_string svg_file) ^"\"")) end; - if !xml_specs then begin + if Config.xml_specs then begin let xml_file = DB.filename_add_suffix base ".xml" in let specs = Specs.get_specs_from_payload summary in if not (DB.file_exists xml_file) || DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time xml_file then begin - let xml_out = ref (create_outfile (DB.filename_to_string xml_file)) in + let xml_out = create_outfile (DB.filename_to_string xml_file) in do_outf xml_out (fun outf -> Dotty.print_specs_xml (Specs.get_signature summary) @@ -1029,26 +820,28 @@ module AnalysisResults = struct type t = (string * Specs.summary) list let spec_files_from_cmdline = - (* parse command-line arguments, and find spec files specified there *) - let args = ref [] in - let f arg = - if not (Filename.check_suffix arg Config.specs_files_suffix) && arg <> "." - then print_usage_exit "arguments must be .specs files" - else args := arg::!args in - Arg.parse "INFERPRINT_ARGS" arg_desc f usage; - if !test_filtering then + (* find spec files specified by command-line arguments *) + IList.iter (fun arg -> + if not (Filename.check_suffix arg Config.specs_files_suffix) && arg <> "." + then print_usage_exit "arguments must be .specs files" + ) Config.anon_args ; + (match Config.source_file_copy with + | Some s -> source_file_copy := Some (DB.abs_source_file_from_path s) + | None -> () + ); + if Config.test_filtering then begin Inferconfig.test (); exit(0) end; - IList.append (if !args = ["."] then begin + IList.append (if Config.anon_args = ["."] then begin let arr = Sys.readdir "." in let all_files = Array.to_list arr in IList.filter (fun fname -> (Filename.check_suffix fname Config.specs_files_suffix)) all_files end - else !args) (load_specfiles ()) + else Config.anon_args) (load_specfiles ()) (** apply [f] to [arg] with the gc compaction disabled during the execution *) let apply_without_gc f arg = @@ -1113,10 +906,10 @@ module AnalysisResults = struct let get_summary_iterator () = let iterator_of_summary_list r = fun f -> IList.iter f r in - match !load_analysis_results with + match Config.load_analysis_results with | None -> begin - match !save_analysis_results with + match Config.save_analysis_results with | None -> iterator_of_spec_files () | Some s -> @@ -1139,54 +932,53 @@ end let compute_top_procedures = ref false let register_perf_stats_report () = - let stats_dir = Filename.concat !Config.results_dir Config.reporting_stats_dir_name in + let stats_dir = Filename.concat Config.results_dir Config.reporting_stats_dir_name in let stats_file = Filename.concat stats_dir (Config.perf_stats_prefix ^ ".json") in - DB.create_dir !Config.results_dir ; + DB.create_dir Config.results_dir ; DB.create_dir stats_dir ; PerfStats.register_report_at_exit stats_file let () = register_perf_stats_report () ; - Config.developer_mode := true; - Config.print_using_diff := true; handle_source_file_copy_option (); let iterate_summaries = AnalysisResults.get_summary_iterator () in let filters = - match !analyzer with + match Config.analyzer with | None -> Inferconfig.do_not_filter | Some analyzer -> Inferconfig.create_filters analyzer in let pdflatex fname = ignore (Sys.command ("pdflatex " ^ fname)) in - do_outf latex (fun outf -> begin_latex_file outf.fmt); - do_outf procs_csv (fun outf -> ProcsCsv.pp_header outf.fmt ()); - do_outf procs_xml (fun outf -> ProcsXml.pp_procs_open outf.fmt ()); - do_outf calls_csv (fun outf -> CallsCsv.pp_header outf.fmt ()); - do_outf bugs_csv (fun outf -> BugsCsv.pp_header outf.fmt ()); - do_outf bugs_json (fun outf -> BugsJson.pp_json_open outf.fmt ()); - do_outf bugs_xml (fun outf -> BugsXml.pp_bugs_open outf.fmt ()); - do_outf report (fun outf -> Report.pp_header outf.fmt ()); + do_outf Config.latex (fun outf -> begin_latex_file outf.fmt); + do_outf Config.procs_csv (fun outf -> ProcsCsv.pp_header outf.fmt ()); + do_outf Config.procs_xml (fun outf -> ProcsXml.pp_procs_open outf.fmt ()); + do_outf Config.calls_csv (fun outf -> CallsCsv.pp_header outf.fmt ()); + do_outf Config.bugs_csv (fun outf -> BugsCsv.pp_header outf.fmt ()); + do_outf Config.bugs_json (fun outf -> BugsJson.pp_json_open outf.fmt ()); + do_outf Config.bugs_xml (fun outf -> BugsXml.pp_bugs_open outf.fmt ()); + do_outf Config.report (fun outf -> Report.pp_header outf.fmt ()); let top_proc = TopProcedures.create () in - if !compute_top_procedures && (!procs_csv != None || !procs_xml != None) + if !compute_top_procedures && (Config.procs_csv != None || Config.procs_xml != None) then iterate_summaries (TopProcedures.process_summary top_proc); let top_proc_set = TopProcedures.top_set top_proc in let linereader = Printer.LineReader.create () in let stats = Stats.create () in iterate_summaries (process_summary filters linereader stats top_proc_set); - if !unit_test then UnitTest.print_unit_test_main (); - do_outf procs_csv close_outf; - do_outf procs_xml (fun outf -> ProcsXml.pp_procs_close outf.fmt (); close_outf outf); - do_outf bugs_csv close_outf; - do_outf bugs_json (fun outf -> BugsJson.pp_json_close outf.fmt (); close_outf outf); - do_outf bugs_json close_outf; - do_outf calls_csv close_outf; - do_outf bugs_txt close_outf; - do_outf bugs_xml (fun outf -> BugsXml.pp_bugs_close outf.fmt (); close_outf outf); - do_outf latex (fun outf -> + if Config.unit_test then UnitTest.print_unit_test_main (); + do_outf Config.procs_csv close_outf; + do_outf Config.procs_xml (fun outf -> ProcsXml.pp_procs_close outf.fmt (); close_outf outf); + do_outf Config.bugs_csv close_outf; + do_outf Config.bugs_json (fun outf -> BugsJson.pp_json_close outf.fmt (); close_outf outf); + do_outf Config.bugs_json close_outf; + do_outf Config.calls_csv close_outf; + do_outf Config.bugs_txt close_outf; + do_outf Config.bugs_xml (fun outf -> BugsXml.pp_bugs_close outf.fmt (); close_outf outf); + do_outf Config.latex (fun outf -> Latex.pp_end outf.fmt (); close_outf outf; pdflatex outf.fname; let pdf_name = (Filename.chop_extension outf.fname) ^ ".pdf" in ignore (Sys.command ("open " ^ pdf_name))); - do_outf report (fun outf -> F.fprintf outf.fmt "%a@?" Report.pp_stats stats; close_outf outf); - if !precondition_stats then PreconditionStats.pp_stats () + do_outf Config.report + (fun outf -> F.fprintf outf.fmt "%a@?" Report.pp_stats stats; close_outf outf); + if Config.precondition_stats then PreconditionStats.pp_stats () diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 54465cdde..75149df31 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -48,7 +48,7 @@ module NodeVisitSet = if n <> 0 then n else compare_distance_to_exit x1 x2 let compare x1 x2 = if !Config.footprint then - match !Config.worklist_mode with + match Config.worklist_mode with | 0 -> compare_ids x1.node x2.node | 1 -> compare_distance_to_exit x1 x2 | _ -> compare_number_of_visits x1 x2 @@ -167,7 +167,7 @@ let path_set_checkout_todo (wl : Worklist.t) (node: Cfg.node) : Paths.PathSet.t let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t = if !Config.footprint then - run_in_re_execution_mode + Config.run_in_re_execution_mode (Abs.lifted_abstract pname tenv) pset else @@ -179,7 +179,7 @@ let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.Path else Some (Abs.abstract pname tenv p) in if !Config.footprint then - run_in_re_execution_mode + Config.run_in_re_execution_mode (Paths.PathSet.map_option abs_option) pathset else @@ -189,13 +189,13 @@ let do_join_pre plist = Dom.proplist_collapse_pre plist let do_join_post pname tenv (pset: Paths.PathSet.t) = - if !Config.spec_abs_level <= 0 then + if Config.spec_abs_level <= 0 then Dom.pathset_collapse pset else Dom.pathset_collapse (Dom.pathset_collapse_impl pname tenv pset) let do_meet_pre pset = - if !Config.meet_level > 0 then + if Config.meet_level > 0 then Dom.propset_meet_generate_pre pset else Propset.to_proplist pset @@ -206,7 +206,7 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list = let collect_do_abstract_one tenv prop = if !Config.footprint then - run_in_re_execution_mode + Config.run_in_re_execution_mode (Abs.abstract_no_symop tenv) prop else @@ -325,7 +325,7 @@ let check_prop_size p _ = (* Check prop size and filter out possible unabstracted lists *) let check_prop_size edgeset_todo = - if !Config.monitor_prop_size then Paths.PathSet.iter check_prop_size edgeset_todo + if Config.monitor_prop_size then Paths.PathSet.iter check_prop_size edgeset_todo let reset_prop_metrics () = prop_max_size := (0, Prop.prop_emp); @@ -436,7 +436,7 @@ let check_assignement_guard node = let check_guard n = IList.for_all check_instr (Cfg.Node.get_instrs n) in IList.for_all check_guard succs in - if !Config.curr_language = Config.C_CPP && + if !Config.curr_language = Config.Clang && succs_are_all_prune_nodes () && succs_same_loc_as_node () && succs_have_simple_guards () then @@ -566,7 +566,7 @@ let forward_tabulate tenv wl = exe_iter (fun prop path cnt num_paths -> try - let prop = if !Config.taint_analysis then + let prop = if Config.taint_analysis then let tainted_params = Taint.tainted_params proc_name in Tabulation.add_param_taint proc_name formal_params prop tainted_params else prop in @@ -581,7 +581,7 @@ let forward_tabulate tenv wl = with | exn when Exceptions.handle_exception exn && !Config.footprint -> handle_exn curr_node exn; - if !Config.nonstop then + if Config.nonstop then propagate_nodes_divergence tenv proc_desc (Paths.PathSet.from_renamed_list [(prop, path)]) succ_nodes exn_nodes wl; @@ -794,7 +794,7 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr let sigma_new_formals = let do_formal (pv, typ) = let texp = match !Config.curr_language with - | Config.C_CPP -> Sil.Sizeof (typ, Sil.Subtype.exact) + | Config.Clang -> Sil.Sizeof (typ, Sil.Subtype.exact) | Config.Java -> Sil.Sizeof (typ, Sil.Subtype.subtypes) in Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in IList.map do_formal new_formals in @@ -937,7 +937,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) let check_recursion_level () = let summary = Specs.get_summary_unsafe "check_recursion_level" pname in let recursion_level = Specs.get_timestamp summary in - if recursion_level > !Config.max_recursion then + if recursion_level > Config.max_recursion then begin L.err "Reached maximum level of recursion, raising a Timeout@."; raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level)) @@ -1017,7 +1017,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) (pp_intra_stats wl pdesc) proc_name outcome; speco in - if !Config.undo_join then + if Config.undo_join then ignore (Specs.Jprop.filter filter candidate_preconditions) else ignore (IList.map filter candidate_preconditions) in @@ -1031,7 +1031,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [(Procname.to_filename proc_name)] in - if !Config.write_dotty then + if Config.write_dotty then Dotty.pp_speclist_dotty_file filename specs; L.out "@.@.================================================"; L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Procname.pp proc_name; @@ -1273,9 +1273,9 @@ let analyze_proc exe_env proc_desc : Specs.summary = let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in let updated_summary = update_summary prev_summary specs phase proc_name elapsed res in - if !Config.curr_language == Config.C_CPP && Config.report_custom_error then + if !Config.curr_language == Config.Clang && Config.report_custom_error then report_custom_errors updated_summary; - if !Config.curr_language == Config.Java && !Config.report_runtime_exceptions then + if !Config.curr_language == Config.Java && Config.report_runtime_exceptions then report_runtime_exceptions tenv proc_desc updated_summary; updated_summary @@ -1284,7 +1284,7 @@ let transition_footprint_re_exe proc_name joined_pres = L.out "Transition %a from footprint to re-exe@." Procname.pp proc_name; let summary = Specs.get_summary_unsafe "transition_footprint_re_exe" proc_name in let summary' = - if !Config.only_footprint then + if Config.only_footprint then { summary with Specs.phase = Specs.RE_EXECUTION; } @@ -1316,7 +1316,7 @@ let perform_transition exe_env tenv proc_name = let transition () = (* disable exceptions for leaks and protect against any other errors *) let joined_pres = - let allowleak = !Config.allowleak in + let allow_leak = !Config.allow_leak in (* apply the start node to f, and do nothing in case of exception *) let apply_start_node f = try @@ -1328,14 +1328,14 @@ let perform_transition exe_env tenv proc_name = with exn when SymOp.exn_not_failure exn -> () in apply_start_node (do_before_node 0); try - Config.allowleak := true; + Config.allow_leak := true; let res = collect_preconditions tenv proc_name in - Config.allowleak := allowleak; + Config.allow_leak := allow_leak; apply_start_node do_after_node; res with exn when SymOp.exn_not_failure exn -> apply_start_node do_after_node; - Config.allowleak := allowleak; + Config.allow_leak := allow_leak; L.err "Error in collect_preconditions for %a@." Procname.pp proc_name; let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in let err_str = "exception raised " ^ (Localise.to_string err_name) in @@ -1357,7 +1357,7 @@ let interprocedural_algorithm exe_env : unit = match Exe_env.get_proc_desc exe_env proc_name with | Some proc_desc -> let reactive_changed = - if !Config.reactive_mode + if Config.reactive_mode then (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.changed else true in if @@ -1417,13 +1417,13 @@ let do_analysis exe_env = let proc_name = Cfg.Procdesc.get_proc_name proc_desc in let tenv = Exe_env.get_tenv exe_env proc_name in let summaryfp = - run_in_footprint_mode (analyze_proc exe_env) proc_desc in + Config.run_in_footprint_mode (analyze_proc exe_env) proc_desc in Specs.add_summary proc_name summaryfp; perform_transition exe_env tenv proc_name; let summaryre = - run_in_re_execution_mode (analyze_proc exe_env) proc_desc in + Config.run_in_re_execution_mode (analyze_proc exe_env) proc_desc in Specs.add_summary proc_name summaryre in { Ondemand.analyze_ondemand; @@ -1538,7 +1538,7 @@ let print_stats_cfg proc_shadowed cfg = (** Print the stats for all the files in the exe_env *) let print_stats exe_env = - if !Config.developer_mode then + if Config.developer_mode then Exe_env.iter_files (fun fname cfg -> let proc_shadowed proc_desc = diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index b3dad541f..1dd14ee39 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -680,7 +680,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc [("is not " ^ rxxx ^ " after " ^ _line tags loc)] in let bucket_str = match bucket_opt with - | Some bucket when !Config.show_ml_buckets -> bucket + | Some bucket when Config.show_buckets -> bucket | _ -> "" in { no_desc with descriptions = bucket_str :: xxx_allocated_to @ by_call_to @ is_not_rxxx_after; tags = !tags } diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index e1b5ef6de..44125cd35 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -83,7 +83,7 @@ let set_err_formatter fmt = (** Flush the current streams *) let flush_streams () = - if !Config.developer_mode then + if Config.developer_mode then begin F.fprintf !current_out_formatter "@?"; F.fprintf !current_err_formatter "@?" @@ -91,8 +91,8 @@ let flush_streams () = (** extend the current print log *) let add_print_action pact = - if !Config.write_html then delayed_actions := pact :: !delayed_actions - else if not !Config.test then !printer_hook !current_out_formatter pact + if Config.write_html then delayed_actions := pact :: !delayed_actions + else if not Config.test then !printer_hook !current_out_formatter pact (** reset the delayed print actions *) let reset_delayed_prints () = @@ -110,7 +110,7 @@ let do_print fmt fmt_string = F.fprintf fmt fmt_string let do_print_in_developer_mode fmt fmt_string = - if !Config.developer_mode then + if Config.developer_mode then F.fprintf fmt fmt_string else F.ifprintf fmt fmt_string @@ -143,7 +143,7 @@ let pp_ml_loc fmt ml_loc = F.fprintf fmt "%s" (ml_loc_to_string ml_loc) let pp_ml_loc_opt fmt ml_loc_opt = - if !Config.developer_mode then match ml_loc_opt with + if Config.developer_mode then match ml_loc_opt with | None -> () | Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc @@ -197,7 +197,7 @@ let d_decrease_indent (indent: int) = add_print_action (PTdecrease_indent, Obj.repr indent) let log_progress_simple text = - if !Config.show_progress_bar then + if Config.show_progress_bar then F.fprintf Format.err_formatter "%s@?" text let log_progress_file () = @@ -207,7 +207,7 @@ let log_progress_procedure () = log_progress_simple "." let log_progress_timeout_event failure_kind = - if !Config.developer_mode then + if Config.developer_mode then begin match failure_kind with | SymOp.FKtimeout -> diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index 6f3306f9f..3b8b4b688 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -114,7 +114,7 @@ and fsel_match fsel1 sub vars fsel2 = | [], [] -> Some (sub, vars) | [], _ -> None | _, [] -> - if (!Config.abs_struct <= 0) then None + if (Config.abs_struct <= 0) then None else Some (sub, vars) (* This can lead to great information loss *) | (fld1, se1') :: fsel1', (fld2, se2') :: fsel2' -> let n = Sil.fld_compare fld1 fld2 in @@ -123,7 +123,7 @@ and fsel_match fsel1 sub vars fsel2 = | None -> None | Some (sub', vars') -> fsel_match fsel1' sub' vars' fsel2' end - else if (n < 0 && !Config.abs_struct > 0) then + else if (n < 0 && Config.abs_struct > 0) then fsel_match fsel1' sub vars fsel2 (* This can lead to great information loss *) else None diff --git a/infer/src/backend/mergeCapture.ml b/infer/src/backend/mergeCapture.ml index b6d0c88be..3df32fa83 100644 --- a/infer/src/backend/mergeCapture.ml +++ b/infer/src/backend/mergeCapture.ml @@ -19,13 +19,13 @@ module F = Format let check_timestamp_of_symlinks = true let buck_out () = - match !Config.project_root with + match Config.project_root with | Some root -> Filename.concat root "buck-out" | None -> - Filename.concat (Filename.dirname !Config.results_dir) "buck-out" + Filename.concat (Filename.dirname Config.results_dir) "buck-out" -let infer_deps () = Filename.concat !Config.results_dir "infer-deps.txt" +let infer_deps () = Filename.concat Config.results_dir "infer-deps.txt" let modified_targets = ref StringSet.empty @@ -147,7 +147,7 @@ let should_link ~target ~target_results_dir ~stats infer_out_src infer_out_dst = and to determine whether the destination has never been copied. In both cases, perform the link. *) let process_merge_file deps_file = - let infer_out_dst = !Config.results_dir in + let infer_out_dst = Config.results_dir in let stats = empty_stats () in let process_line line = match Str.split_delim (Str.regexp (Str.quote "\t")) line with diff --git a/infer/src/backend/mleak_buckets.ml b/infer/src/backend/mleak_buckets.ml index be70c58d1..75e866d08 100644 --- a/infer/src/backend/mleak_buckets.ml +++ b/infer/src/backend/mleak_buckets.ml @@ -14,103 +14,80 @@ open! Utils let objc_arc_flag = "objc_arc" -let bucket_delimiter = "," - -type mleak_bucket = - | MLeak_cf - | MLeak_arc - | MLeak_no_arc - | MLeak_cpp - | MLeak_unknown - -let ml_buckets = ref [] - -let bucket_from_string bucket_s = - match bucket_s with - | "cf" -> MLeak_cf - | "arc" -> MLeak_arc - | "narc" -> MLeak_no_arc - | "cpp" -> MLeak_cpp - | "unknown_origin" -> MLeak_unknown - | _ -> assert false - let bucket_to_message bucket = match bucket with - | MLeak_cf -> "[CF]" - | MLeak_arc -> "[ARC]" - | MLeak_no_arc -> "[NO ARC]" - | MLeak_cpp -> "[CPP]" - | MLeak_unknown -> "[UNKNOWN ORIGIN]" + | `MLeak_cf -> "[CF]" + | `MLeak_arc -> "[ARC]" + | `MLeak_no_arc -> "[NO ARC]" + | `MLeak_cpp -> "[CPP]" + | `MLeak_unknown -> "[UNKNOWN ORIGIN]" let mleak_bucket_compare b1 b2 = match b1, b2 with - | MLeak_cf, MLeak_cf -> 0 - | MLeak_cf, _ -> -1 - | _, MLeak_cf -> 1 - | MLeak_arc, MLeak_arc -> 0 - | MLeak_arc, _ -> -1 - | _, MLeak_arc -> 1 - | MLeak_no_arc, MLeak_no_arc -> 0 - | MLeak_no_arc, _ -> -1 - | _, MLeak_no_arc -> 1 - | MLeak_unknown, MLeak_unknown -> 0 - | MLeak_unknown, _ -> -1 - | _, MLeak_unknown -> 1 - | MLeak_cpp, MLeak_cpp -> 0 + | `MLeak_all, `MLeak_all -> 0 + | `MLeak_all, _ -> -1 + | _, `MLeak_all -> 1 + | `MLeak_cf, `MLeak_cf -> 0 + | `MLeak_cf, _ -> -1 + | _, `MLeak_cf -> 1 + | `MLeak_arc, `MLeak_arc -> 0 + | `MLeak_arc, _ -> -1 + | _, `MLeak_arc -> 1 + | `MLeak_no_arc, `MLeak_no_arc -> 0 + | `MLeak_no_arc, _ -> -1 + | _, `MLeak_no_arc -> 1 + | `MLeak_unknown, `MLeak_unknown -> 0 + | `MLeak_unknown, _ -> -1 + | _, `MLeak_unknown -> 1 + | `MLeak_cpp, `MLeak_cpp -> 0 let mleak_bucket_eq b1 b2 = mleak_bucket_compare b1 b2 = 0 -let init_buckets ml_buckets_arg = - let buckets = - Str.split (Str.regexp bucket_delimiter) ml_buckets_arg in - let buckets = - match buckets with - | ["all"] -> [] - | _ -> IList.map bucket_from_string buckets in - ml_buckets := buckets +let contains_all = + IList.mem mleak_bucket_eq `MLeak_all Config.ml_buckets -let contains_cf ml_buckets = - IList.mem mleak_bucket_eq MLeak_cf ml_buckets +let contains_cf = + IList.mem mleak_bucket_eq `MLeak_cf Config.ml_buckets -let contains_arc ml_buckets = - IList.mem mleak_bucket_eq MLeak_arc ml_buckets +let contains_arc = + IList.mem mleak_bucket_eq `MLeak_arc Config.ml_buckets -let contains_narc ml_buckets = - IList.mem mleak_bucket_eq MLeak_no_arc ml_buckets +let contains_narc = + IList.mem mleak_bucket_eq `MLeak_no_arc Config.ml_buckets -let contains_cpp ml_buckets = - IList.mem mleak_bucket_eq MLeak_cpp ml_buckets +let contains_cpp = + IList.mem mleak_bucket_eq `MLeak_cpp Config.ml_buckets -let contains_unknown_origin ml_buckets = - IList.mem mleak_bucket_eq MLeak_unknown ml_buckets +let contains_unknown_origin = + IList.mem mleak_bucket_eq `MLeak_unknown Config.ml_buckets let should_raise_leak_cf typ = - if contains_cf !ml_buckets then + if contains_cf then Objc_models.is_core_lib_type typ else false let should_raise_leak_arc () = - if contains_arc !ml_buckets then + if contains_arc then !Config.arc_mode else false let should_raise_leak_no_arc () = - if contains_narc !ml_buckets then + if contains_narc then not (!Config.arc_mode) else false -let should_raise_leak_unknown_origin () = - contains_unknown_origin !ml_buckets +let should_raise_leak_unknown_origin = + contains_unknown_origin -let ml_bucket_unknown_origin () = - bucket_to_message MLeak_unknown +let ml_bucket_unknown_origin = + bucket_to_message `MLeak_unknown (* Returns whether a memory leak should be raised for a C++ object.*) (* If ml_buckets contains cpp, then check leaks from C++ objects. *) -let should_raise_cpp_leak () = - if contains_cpp !ml_buckets then - Some (bucket_to_message MLeak_cpp) +let should_raise_cpp_leak = + if contains_cpp then + Some (bucket_to_message `MLeak_cpp) else None (* Returns whether a memory leak should be raised. *) @@ -118,11 +95,10 @@ let should_raise_cpp_leak () = (* If arc is passed, check leaks from code that compiles with arc*) (* If no arc is passed check the leaks from code that compiles without arc *) let should_raise_objc_leak typ = - if IList.length !ml_buckets = 0 then Some "" - else - if should_raise_leak_cf typ then Some (bucket_to_message MLeak_cf) - else if should_raise_leak_arc () then Some (bucket_to_message MLeak_arc) - else if should_raise_leak_no_arc () then Some (bucket_to_message MLeak_no_arc) + if Config.ml_buckets = [] || contains_all then Some "" + else if should_raise_leak_cf typ then Some (bucket_to_message `MLeak_cf) + else if should_raise_leak_arc () then Some (bucket_to_message `MLeak_arc) + else if should_raise_leak_no_arc () then Some (bucket_to_message `MLeak_no_arc) else None (* diff --git a/infer/src/backend/mleak_buckets.mli b/infer/src/backend/mleak_buckets.mli index 8f28e3169..7ef8bf020 100644 --- a/infer/src/backend/mleak_buckets.mli +++ b/infer/src/backend/mleak_buckets.mli @@ -13,8 +13,6 @@ open! Utils val objc_arc_flag : string -val init_buckets : string -> unit - (* Returns whether a memory leak should be raised. *) (* If cf is passed, then check leaks from Core Foundation. *) (* If arc is passed, check leaks from code that compiles with arc*) @@ -23,8 +21,8 @@ val should_raise_objc_leak : Sil.typ -> string option (* Returns whether a memory leak should be raised for a C++ object.*) (* If ml_buckets contains cpp, then check leaks from C++ objects. *) -val should_raise_cpp_leak : unit -> string option +val should_raise_cpp_leak : string option -val should_raise_leak_unknown_origin : unit -> bool +val should_raise_leak_unknown_origin : bool -val ml_bucket_unknown_origin : unit -> string +val ml_bucket_unknown_origin : string diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index a47cee20e..e2e24685c 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -140,7 +140,7 @@ let execute___print_value { Builtin.pdesc; prop_; path; args; } let is_undefined_opt prop n_lexp = let is_undef = Option.is_some (Prop.get_undef_attribute prop n_lexp) in - is_undef && (!Config.angelic_execution || !Config.optimistic_cast) + is_undef && (Config.angelic_execution || Config.optimistic_cast) (** Creates an object in the heap with a given type, when the object is not known to be null or when it doesn't appear already in the heap. *) @@ -512,7 +512,7 @@ let execute___objc_retain_impl let execute___objc_retain builtin_args : Builtin.ret_typ = - if !Config.objc_memory_model_on then + if Config.objc_memory_model_on then execute___objc_retain_impl builtin_args else execute___no_op builtin_args.Builtin.prop_ builtin_args.Builtin.path @@ -531,7 +531,7 @@ let execute___objc_release_impl let execute___objc_release builtin_args : Builtin.ret_typ = - if !Config.objc_memory_model_on then + if Config.objc_memory_model_on then execute___objc_release_impl builtin_args else execute___no_op builtin_args.Builtin.prop_ builtin_args.Builtin.path @@ -547,7 +547,7 @@ let execute___set_autorelease_attribute | [(lexp, _)], _ -> let pname = Cfg.Procdesc.get_proc_name pdesc in let prop = return_result lexp prop_ ret_ids in - if !Config.objc_memory_model_on then + if Config.objc_memory_model_on then let n_lexp, prop = check_arith_norm_exp pname lexp prop in let prop' = Prop.add_or_replace_exp_attribute prop n_lexp Sil.Aautorelease in [(prop', path)] @@ -558,7 +558,7 @@ let execute___set_autorelease_attribute let execute___release_autorelease_pool ({ Builtin.prop_; path; } as builtin_args) : Builtin.ret_typ = - if !Config.objc_memory_model_on then + if Config.objc_memory_model_on then let autoreleased_objects = Prop.get_atoms_with_attribute Sil.Aautorelease prop_ in let prop_without_attribute = Prop.remove_attribute Sil.Aautorelease prop_ in let call_release res exp = @@ -725,7 +725,7 @@ let _execute_free_nonzero mk pdesc tenv instr prop lexp typ loc = IList.rev prop_list end with Rearrange.ARRAY_ACCESS -> - if (!Config.array_level = 0) then assert false + if (Config.array_level = 0) then assert false else begin L.d_strln ".... Array containing allocated heap cells ...."; L.d_str " Instr: "; Sil.d_instr instr; L.d_ln (); diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 987844ea6..a6cda35cf 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -167,7 +167,7 @@ end (** Execute the delayed print actions *) let force_delayed_print fmt = let pe_default = - if !Config.write_html then pe_html Black else pe_text in + if Config.write_html then pe_html Black else pe_text in function | (L.PTatom, a) -> let (a: Sil.atom) = Obj.obj a in @@ -191,7 +191,7 @@ let force_delayed_print fmt = F.fprintf fmt "%s@[" !s | (L.PTinstr, i) -> let (i: Sil.instr) = Obj.obj i in - if !Config.write_html + if Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green @@ -201,7 +201,7 @@ let force_delayed_print fmt = Sil.pp_instr pe_text fmt i | (L.PTinstr_list, il) -> let (il: Sil.instr list) = Obj.obj il in - if !Config.write_html + if Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green @@ -220,7 +220,7 @@ let force_delayed_print fmt = Location.pp fmt loc | (L.PTnode_instrs, b_n) -> let (b: bool), (io: Sil.instr option), (n: Cfg.node) = Obj.obj b_n in - if !Config.write_html + if Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green @@ -271,14 +271,14 @@ let force_delayed_print fmt = | (L.PTspec, spec) -> let (spec: Prop.normal Specs.spec) = Obj.obj spec in Specs.pp_spec - (if !Config.write_html then pe_html Blue else pe_text) + (if Config.write_html then pe_html Blue else pe_text) None fmt spec | (L.PTstr, s) -> let (s: string) = Obj.obj s in F.fprintf fmt "%s" s | (L.PTstr_color, s) -> let (s: string), (c: color) = Obj.obj s in - if !Config.write_html + if Config.write_html then F.fprintf fmt "%a%s%a" Io_infer.Html.pp_start_color c @@ -291,7 +291,7 @@ let force_delayed_print fmt = F.fprintf fmt "%s@\n" s | (L.PTstrln_color, s) -> let (s: string), (c: color) = Obj.obj s in - if !Config.write_html + if Config.write_html then F.fprintf fmt "%a%s%a@\n" Io_infer.Html.pp_start_color c @@ -313,7 +313,7 @@ let force_delayed_print fmt = (pp_seq (Sil.pp_typ pe_default)) fmt tl | (L.PTerror, s) -> let (s: string) = Obj.obj s in - if !Config.write_html + if Config.write_html then F.fprintf fmt "%aERROR: %s%a" Io_infer.Html.pp_start_color Red @@ -323,7 +323,7 @@ let force_delayed_print fmt = F.fprintf fmt "ERROR: %s" s | (L.PTwarning, s) -> let (s: string) = Obj.obj s in - if !Config.write_html + if Config.write_html then F.fprintf fmt "%aWARNING: %s%a" Io_infer.Html.pp_start_color Orange @@ -333,7 +333,7 @@ let force_delayed_print fmt = F.fprintf fmt "WARNING: %s" s | (L.PTinfo, s) -> let (s: string) = Obj.obj s in - if !Config.write_html + if Config.write_html then F.fprintf fmt "%aINFO: %s%a" Io_infer.Html.pp_start_color Blue @@ -377,14 +377,14 @@ let start_session node (loc: Location.t) proc_name session = Io_infer.Html.pp_start_color Black let node_start_session node loc proc_name session = - if !Config.write_html then + if Config.write_html then start_session node loc proc_name session (** Finish a session, and perform delayed print actions if required *) let node_finish_session node = - if !Config.test == false then force_delayed_prints () + if Config.test == false then force_delayed_prints () else L.reset_delayed_prints (); - if !Config.write_html then begin + if Config.write_html then begin F.fprintf !curr_html_formatter "%a" Io_infer.Html.pp_end_color (); NodesHtml.finish_node (Cfg.Node.get_id node :> int) @@ -393,7 +393,7 @@ let node_finish_session node = (** Write html file for the procedure. The boolean indicates whether to print whole seconds only *) let write_proc_html whole_seconds pdesc = - if !Config.write_html then + if Config.write_html then begin let pname = Cfg.Procdesc.get_proc_name pdesc in let nodes = IList.sort Cfg.Node.compare (Cfg.Procdesc.get_nodes pdesc) in @@ -561,7 +561,7 @@ let write_html_file linereader filename cfg = (** Create filename.ext.html for each file in the exe_env. *) let write_all_html_files linereader exe_env = - if !Config.write_html then + if Config.write_html then Exe_env.iter_files (fun _ cfg -> let source_files_in_cfg = diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 8f57c6793..f759869bb 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -153,12 +153,12 @@ let pp_sub_entry pe0 f entry = (** Pretty print a substitution as a list of (ident,exp) pairs *) let pp_subl pe = - if !Config.smt_output then pp_semicolon_seq pe (pp_sub_entry pe) + if Config.smt_output then pp_semicolon_seq pe (pp_sub_entry pe) else pp_semicolon_seq_oneline pe (pp_sub_entry pe) (** Pretty print a pi. *) let pp_pi pe = - if !Config.smt_output then pp_semicolon_seq pe (Sil.pp_atom pe) + if Config.smt_output then pp_semicolon_seq pe (Sil.pp_atom pe) else pp_semicolon_seq_oneline pe (Sil.pp_atom pe) (** Dump a pi. *) @@ -1395,7 +1395,7 @@ let footprint_normalize prop = sigma_fav_add fav nsigma; fav in (* TODO (t4893479): make this check less angelic *) - if Sil.fav_exists fp_vars Ident.is_normal && not !Config.angelic_execution then + if Sil.fav_exists fp_vars Ident.is_normal && not Config.angelic_execution then begin L.d_strln "footprint part contains normal variables"; d_pi npi; L.d_ln (); diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index 1e64c3e83..d78a3d5d8 100644 --- a/infer/src/backend/propgraph.ml +++ b/infer/src/backend/propgraph.ml @@ -205,7 +205,7 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist = if extract_stack then Prop.replace_sigma (base_stack @ Prop.get_sigma prop) prop else Prop.expose prop in let update_pe_diff (prop: Prop.normal Prop.t) : printenv = - if !Config.print_using_diff then + if Config.print_using_diff then let diff = compute_diff Blue (from_prop base_prop) (from_prop prop) in let cmap_norm = diff_get_colormap false diff in let cmap_foot = diff_get_colormap true diff in diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index a27e58644..7dc3cde07 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -709,7 +709,7 @@ let get_smt_key a p = let check_atom prop a0 = let a = Prop.atom_normalize_prop prop a0 in let prop_no_fp = Prop.replace_sigma_footprint [] (Prop.replace_pi_footprint [] prop) in - if !Config.smt_output then begin + if Config.smt_output then begin let key = get_smt_key a prop_no_fp in let key_filename = DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [(key ^ ".cns")] in @@ -823,11 +823,11 @@ let check_inconsistency_base prop = let is_java_this pvar = !Config.curr_language = Config.Java && Pvar.is_this pvar in let is_objc_instance_self pvar = - !Config.curr_language = Config.C_CPP && + !Config.curr_language = Config.Clang && Pvar.get_name pvar = Mangled.from_string "self" && procedure_attr.ProcAttributes.is_objc_instance_method in let is_cpp_this pvar = - !Config.curr_language = Config.C_CPP && Pvar.is_this pvar && + !Config.curr_language = Config.Clang && Pvar.is_this pvar && procedure_attr.ProcAttributes.is_cpp_instance_method in let do_hpred = function | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) -> @@ -1255,7 +1255,7 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs else None in let index_missing_opt = if index_missing != [] && - (!Config.Experiment.allow_missing_index_in_proc_call || !Config.footprint) + (Config.allow_missing_index_in_proc_call || !Config.footprint) then Some (Sil.Earray (size1, index_missing, inst1)) else None in subs'', index_frame_opt, index_missing_opt @@ -1600,7 +1600,7 @@ end let cast_exception tenv texp1 texp2 e1 subs = let _ = match texp1, texp2 with | Sil.Sizeof (t1, _), Sil.Sizeof (t2, st2) -> - if !Config.developer_mode || + if Config.developer_mode || (Sil.Subtype.is_cast st2 && not (Subtyping_check.check_subtype tenv t1 t2)) then ProverState.checks := Class_cast_check (texp1, texp2, e1) :: !ProverState.checks @@ -1679,7 +1679,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing = (** pre-process implication between a non-array and an array: the non-array is turned into an array of size given by its type only active in type_size mode *) let sexp_imply_preprocess se1 texp1 se2 = match se1, texp1, se2 with - | Sil.Eexp (_, inst), Sil.Sizeof _, Sil.Earray _ when !Config.type_size -> + | Sil.Eexp (_, inst), Sil.Sizeof _, Sil.Earray _ when Config.type_size -> let se1' = Sil.Earray (texp1, [(Sil.exp_zero, se1)], inst) in L.d_strln_color Orange "sexp_imply_preprocess"; L.d_str " se1: "; Sil.d_sexp se1; L.d_ln (); L.d_str " se1': "; Sil.d_sexp se1'; L.d_ln (); se1' @@ -1934,7 +1934,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * let sexp = let index = Sil.exp_int (Sil.Int.of_int (String.length s)) in match !Config.curr_language with - | Config.C_CPP -> + | Config.Clang -> Sil.Earray (size, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none) | Config.Java -> let mk_fld_sexp s = @@ -1945,7 +1945,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * Sil.Estruct (IList.map mk_fld_sexp fields, Sil.inst_none) in let const_string_texp = match !Config.curr_language with - | Config.C_CPP -> Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size), Sil.Subtype.exact) + | Config.Clang -> Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size), Sil.Subtype.exact) | Config.Java -> let object_type = Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in @@ -2088,7 +2088,8 @@ let check_array_bounds (sub1, sub2) prop = let check_failed atom = ProverState.checks := Bounds_check :: !ProverState.checks; L.d_str_color Red "bounds_check failed: provable atom: "; Sil.d_atom atom; L.d_ln(); - if (not !Config.Experiment.bound_error_allowed_in_procedure_call) then raise (IMPL_EXC ("bounds check", (sub1, sub2), EXC_FALSE)) in + if (not Config.bound_error_allowed_in_procedure_call) then + raise (IMPL_EXC ("bounds check", (sub1, sub2), EXC_FALSE)) in let fail_if_le e' e'' = let lt_ineq = Prop.mk_inequality (Sil.BinOp(Sil.Le, e', e'')) in if check_atom prop lt_ineq then check_failed lt_ineq in diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 8c4e9dadd..a2975ffb9 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -76,7 +76,7 @@ let check_bad_index pname p size index loc = (** Perform bounds checking *) let bounds_check pname prop size e = - if !Config.trace_rearrange then + if Config.trace_rearrange then begin L.d_str "Bounds check index:"; Sil.d_exp e; L.d_str " size: "; Sil.d_exp size; @@ -86,7 +86,7 @@ let bounds_check pname prop size e = let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp t (off: Sil.offset list) inst : Sil.atom list * Sil.strexp * Sil.typ = - if !Config.trace_rearrange then + if Config.trace_rearrange then begin L.d_increase_indent 1; L.d_strln "entering create_struct_values"; @@ -167,7 +167,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp L.d_str "create_struct_values type:"; Sil.d_typ_full t; L.d_str " off: "; Sil.d_offset_list off; L.d_ln(); assert false in - if !Config.trace_rearrange then + if Config.trace_rearrange then begin let _, se, _ = res in L.d_strln "exiting create_struct_values, returning"; @@ -246,7 +246,7 @@ let rec _strexp_extend_values let size = match se with | Sil.Eexp (_, Sil.Ialloc) -> Sil.exp_one (* if allocated explicitly, we know size is 1 *) | _ -> - if !Config.type_size then Sil.exp_one (* Sil.Sizeof (typ, Sil.Subtype.exact) *) + if Config.type_size then Sil.exp_one (* Sil.Sizeof (typ, Sil.Subtype.exact) *) else Sil.exp_get_undefined false in let se_new = Sil.Earray(size, [(Sil.exp_zero, se)], inst) in @@ -379,8 +379,10 @@ let strexp_extend_values if footprint_part then off', IList.map (fun (id, e) -> Prop.mk_eq (Sil.Var id) e) eqs else off, [] in - if !Config.trace_rearrange then (L.d_str "entering strexp_extend_values se: "; Sil.d_sexp se; L.d_str " typ: "; - Sil.d_typ_full typ; L.d_str " off': "; Sil.d_offset_list off'; L.d_strln (if footprint_part then " FP" else " RE")); + if Config.trace_rearrange then + (L.d_str "entering strexp_extend_values se: "; Sil.d_sexp se; L.d_str " typ: "; + Sil.d_typ_full typ; L.d_str " off': "; Sil.d_offset_list off'; + L.d_strln (if footprint_part then " FP" else " RE")); let atoms_se_typ_list = _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se typ off' inst in @@ -389,7 +391,7 @@ let strexp_extend_values let check_neg_atom atom = Prover.check_atom Prop.prop_emp (neg_atom atom) in let check_not_inconsistent (atoms, _, _) = not (IList.exists check_neg_atom atoms) in IList.filter check_not_inconsistent atoms_se_typ_list in - if !Config.trace_rearrange then L.d_strln "exiting strexp_extend_values"; + if Config.trace_rearrange then L.d_strln "exiting strexp_extend_values"; let st = match te with | Sil.Sizeof(_, st) -> st | _ -> Sil.Subtype.exact in @@ -408,9 +410,9 @@ let mk_ptsto_exp_footprint then begin (* in angelic mode, purposely ignore dangling pointer warnings during the footprint phase -- we * will fix them during the re - execution phase *) - if not (!Config.angelic_execution && !Config.footprint) then + if not (Config.angelic_execution && !Config.footprint) then begin - if !Config.developer_mode then + if Config.developer_mode then L.err "!!!! Footprint Error, Bad Root : %a !!!! @\n" (Sil.pp_exp pe_text) lexp; let deref_str = Localise.deref_str_dangling None in let err_desc = @@ -422,7 +424,7 @@ let mk_ptsto_exp_footprint end; let off_foot, eqs = laundry_offset_for_footprint max_stamp off in let st = match !Config.curr_language with - | Config.C_CPP -> Sil.Subtype.exact + | Config.Clang -> Sil.Subtype.exact | Config.Java -> Sil.Subtype.subtypes in let create_ptsto footprint_part off0 = match root, off0, typ with | Sil.Lvar pvar, [], Sil.Tfun _ -> @@ -477,7 +479,8 @@ let fav_max_stamp fav = [lexp] -- field splitting model. It also materializes all indices accessed in lexp. *) let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = - if !Config.trace_rearrange then (L.d_str "entering prop_iter_extend_ptsto lexp: "; Sil.d_exp lexp; L.d_ln ()); + if Config.trace_rearrange then + (L.d_str "entering prop_iter_extend_ptsto lexp: "; Sil.d_exp lexp; L.d_ln ()); let offset = Sil.exp_get_offsets lexp in let max_stamp = fav_max_stamp (Prop.prop_iter_fav iter) in let max_stamp_val = !max_stamp in @@ -507,7 +510,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = let iter' = IList.fold_left (Prop.prop_iter_add_atom !Config.footprint) iter atoms in Prop.prop_iter_update_current iter' (Sil.Hpointsto (e, se, te)) in let do_extend e se te = - if !Config.trace_rearrange then begin + if Config.trace_rearrange then begin L.d_strln "entering do_extend"; L.d_str "e: "; Sil.d_exp e; L.d_str " se : "; Sil.d_sexp se; L.d_str " te: "; Sil.d_texp_full te; L.d_ln (); L.d_ln () @@ -618,12 +621,12 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst = exception ARRAY_ACCESS let rearrange_arith lexp prop = - if !Config.trace_rearrange then begin + if Config.trace_rearrange then begin L.d_strln "entering rearrange_arith"; L.d_str "lexp: "; Sil.d_exp lexp; L.d_ln (); L.d_str "prop: "; L.d_ln (); Prop.d_prop prop; L.d_ln (); L.d_ln () end; - if (!Config.array_level >= 2) then raise ARRAY_ACCESS + if (Config.array_level >= 2) then raise ARRAY_ACCESS else let root = Sil.root_of_lexp lexp in if Prover.check_allocatedness prop root then @@ -638,7 +641,7 @@ let pp_rearrangement_error message prop lexp = (** do re-arrangment for an iter whose current element is a pointsto *) let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = - if !Config.trace_rearrange then begin + if Config.trace_rearrange then begin L.d_increase_indent 1; L.d_strln "entering iter_rearrange_ptsto"; L.d_str "lexp: "; Sil.d_exp lexp; L.d_ln (); @@ -677,7 +680,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = | _ -> [iter] end in begin - if !Config.trace_rearrange then begin + if Config.trace_rearrange then begin L.d_strln "exiting iter_rearrange_ptsto, returning results"; Prop.d_proplist_with_typ (IList.map Prop.prop_iter_to_prop res); L.d_decrease_indent 1; @@ -688,7 +691,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = (** do re-arrangment for an iter whose current element is a nonempty listseg *) let iter_rearrange_ne_lseg recurse_on_iters iter para e1 e2 elist = - if (!Config.nelseg) then + if Config.nelseg then let iter_inductive_case = let n' = Sil.Var (Ident.create_fresh Ident.kprimed) in let (_, para_inst1) = Sil.hpara_instantiate para e1 n' elist in @@ -848,7 +851,7 @@ let rec iter_rearrange inst: (Sil.offset list) Prop.prop_iter list = let typ = match Sil.exp_get_offsets lexp with | Sil.Off_fld (f, ((Sil.Tstruct _) as struct_typ)) :: _ -> (* access through field: get the struct type from the field *) - if !Config.trace_rearrange then begin + if Config.trace_rearrange then begin L.d_increase_indent 1; L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Ident.fieldname_to_string f); L.d_str " type from instruction: "; Sil.d_typ_full typ_from_instr; L.d_ln(); @@ -859,7 +862,7 @@ let rec iter_rearrange struct_typ | _ -> typ_from_instr in - if !Config.trace_rearrange then begin + if Config.trace_rearrange then begin L.d_increase_indent 1; L.d_strln "entering iter_rearrange"; L.d_str "lexp: "; Sil.d_exp lexp; L.d_ln (); @@ -869,11 +872,11 @@ let rec iter_rearrange L.d_ln (); L.d_ln () end; let default_case_iter (iter': unit Prop.prop_iter) = - if !Config.trace_rearrange then L.d_strln "entering default_case_iter"; + if Config.trace_rearrange then L.d_strln "entering default_case_iter"; if !Config.footprint then prop_iter_add_hpred_footprint pname tenv prop iter' (lexp, typ) inst else - if (!Config.array_level >= 1 && not !Config.footprint && Sil.exp_pointer_arith lexp) + if (Config.array_level >= 1 && not !Config.footprint && Sil.exp_pointer_arith lexp) then rearrange_arith lexp prop else begin pp_rearrangement_error "cannot find predicate with root" prop lexp; @@ -906,7 +909,7 @@ let rec iter_rearrange | Some iter -> match Prop.prop_iter_current iter with | (Sil.Hpointsto (_, _, texp), off) -> - if !Config.type_size then check_type_size pname prop texp off typ_from_instr; + if Config.type_size then check_type_size pname prop texp off typ_from_instr; iter_rearrange_ptsto pname tenv prop iter lexp inst | (Sil.Hlseg (Sil.Lseg_NE, para, e1, e2, elist), _) -> iter_rearrange_ne_lseg recurse_on_iters iter para e1 e2 elist @@ -926,7 +929,7 @@ let rec iter_rearrange | Some _, _ -> iter_rearrange_pe_dllseg_first recurse_on_iters default_case_iter iter para_dll e1 e2 e3 e4 elist | _, Some _ -> iter_rearrange_pe_dllseg_last recurse_on_iters default_case_iter iter para_dll e1 e2 e3 e4 elist end in - if !Config.trace_rearrange then begin + if Config.trace_rearrange then begin L.d_strln "exiting iter_rearrange, returning results"; Prop.d_proplist_with_typ (IList.map Prop.prop_iter_to_prop res); L.d_decrease_indent 1; @@ -983,7 +986,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = let is_deref_of_nullable = let is_definitely_non_null exp prop = Prover.check_disequal prop exp Sil.exp_zero in - !Config.report_nullable_inconsistency && not (is_definitely_non_null root prop) + Config.report_nullable_inconsistency && not (is_definitely_non_null root prop) && is_only_pt_by_nullable_fld_or_param root in let relevant_attributes_getters = [ Prop.get_resource_attribute; @@ -1026,7 +1029,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = let err_desc = Errdesc.explain_dereference deref_str prop (State.get_loc ()) in raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__)) | Some (Sil.Aundef (s, _, undef_loc, _)) -> - if !Config.angelic_execution then () + if Config.angelic_execution then () else let deref_str = Localise.deref_str_undef (s, undef_loc) in let err_desc = Errdesc.explain_dereference deref_str prop loc in @@ -1071,7 +1074,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc = Some (Sil.Lfield(e'', fn, t)), true (* the block dereferences is a field of an object*) | Some (_, e) -> Some e, false | _ -> None, false in - if (!Config.curr_language = Config.C_CPP) && + if (!Config.curr_language = Config.Clang) && fun_exp_may_be_null () && not (is_fun_exp_captured_var ()) then begin @@ -1085,7 +1088,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc = | _ -> err_desc_nobuckets) in let err_desc = Localise.error_desc_set_bucket - err_desc_nobuckets' Localise.BucketLevel.b1 !Config.show_buckets in + err_desc_nobuckets' Localise.BucketLevel.b1 Config.show_buckets in if is_field_deref then raise (Exceptions.Field_not_null_checked @@ -1099,7 +1102,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc = either is a local or it's a modified param *) let err_desc = Localise.error_desc_set_bucket - err_desc_nobuckets Localise.BucketLevel.b1 !Config.show_buckets in + err_desc_nobuckets Localise.BucketLevel.b1 Config.show_buckets in raise (Exceptions.Null_dereference (err_desc, __POS__)) end diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index ff48a0678..76ef59f6b 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -519,7 +519,7 @@ let res_dir_specs_filename pname = let specs_library_filenames pname = IList.map (fun specs_dir -> DB.filename_from_string (Filename.concat specs_dir (specs_filename pname))) - !Config.specs_library + Config.specs_library (** paths to the .specs file for the given procedure in the models folder *) let specs_models_filename pname = @@ -540,10 +540,10 @@ let store_summary pname (summ: summary) = } | None -> payload in let summ1 = { summ with payload = process_payload summ.payload } in - let summ2 = if !Config.save_compact_summaries + let summ2 = if Config.save_compact_summaries then summary_compact (Sil.create_sharing_env ()) summ1 else summ1 in - let summ3 = if !Config.save_time_in_summaries + let summ3 = if Config.save_time_in_summaries then summ2 else { summ2 with diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 1f079bd8d..943d464c6 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -387,7 +387,7 @@ let call_should_be_skipped callee_pname summary = (* skip abstract methods *) || summary.Specs.attributes.ProcAttributes.is_abstract (* treat calls with no specs as skip functions in angelic mode *) - || (!Config.angelic_execution && Specs.get_specs_from_payload summary == []) + || (Config.angelic_execution && Specs.get_specs_from_payload summary == []) (** In case of constant string dereference, return the result immediately *) let check_constant_string_dereference lexp = @@ -828,7 +828,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_ let add_tainted_post ret_exp callee_pname prop = Prop.add_or_replace_exp_attribute prop ret_exp (Sil.Ataint callee_pname) in - if !Config.angelic_execution && not (is_rec_call callee_pname) then + if Config.angelic_execution && not (is_rec_call callee_pname) then (* introduce a fresh program variable to allow abduction on the return value *) let abducted_ret_pv = Pvar.mk_abducted_ret callee_pname callee_loc in (* prevent introducing multiple abducted retvals for a single call site in a loop *) @@ -842,7 +842,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_ (* bind return id to the abducted value pointed to by the pvar we introduced *) bind_exp_to_abducted_val ret_exp abducted_ret_pv prop in let prop'' = add_ret_non_null ret_exp typ prop' in - if !Config.taint_analysis && Taint.returns_tainted callee_pname None then + if Config.taint_analysis && Taint.returns_tainted callee_pname None then add_tainted_post ret_exp { Sil.taint_source = callee_pname; taint_kind = Unknown } prop'' else prop'' else add_ret_non_null ret_exp typ prop @@ -886,7 +886,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ Prop.add_or_replace_exp_attribute prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit) else prop' in let prop''' = - if !Config.taint_analysis + if Config.taint_analysis then add_taint prop'' id rhs_exp pname tenv else prop'' in prop''' :: acc in @@ -917,7 +917,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ else callee_opt in IList.fold_left fold_undef_pname None (Prop.get_exp_attributes prop exp) in let prop' = - if !Config.angelic_execution then + if Config.angelic_execution then (* when we try to deref an undefined value, add it to the footprint *) match exp_get_undef_attr n_rhs_exp' with | Some (Sil.Aundef (callee_pname, ret_annots, callee_loc, _)) -> @@ -930,7 +930,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ Rearrange.rearrange ~report_deref_errors pdesc tenv n_rhs_exp' typ prop' loc in IList.rev (IList.fold_left (execute_letderef_ pdesc tenv id loc) [] iter_list) with Rearrange.ARRAY_ACCESS -> - if (!Config.array_level = 0) then assert false + if (Config.array_level = 0) then assert false else let undef = Sil.exp_get_undefined false in [Prop.conjoin_eq (Sil.Var id) undef prop_] @@ -969,7 +969,7 @@ let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in IList.rev (IList.fold_left (execute_set_ pdesc tenv n_rhs_exp) [] iter_list) with Rearrange.ARRAY_ACCESS -> - if (!Config.array_level = 0) then assert false + if (Config.array_level = 0) then assert false else [prop_] (** Execute [instr] with a symbolic heap [prop].*) @@ -1034,7 +1034,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path (* in comparisons, nil is translated as (void * ) 0 rather than 0 *) let is_comparison_to_nil = function | Sil.Cast ((Sil.Tptr (Sil.Tvoid, _)), exp) -> - !Config.curr_language = Config.C_CPP && Sil.exp_is_zero exp + !Config.curr_language = Config.Clang && Sil.exp_is_zero exp | _ -> false in match Prop.exp_normalize_prop Prop.prop_emp cond with | Sil.Const (Sil.Cint i) when report_condition_always_true_false i -> @@ -1065,7 +1065,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let exn = Exceptions.Bad_pointer_comparison (desc, __POS__) in Reporting.log_warning current_pname exn | _ -> () in - if not !Config.report_runtime_exceptions then + if not Config.report_runtime_exceptions then check_already_dereferenced current_pname cond prop__; check_condition_always_true_false (); let n_cond, prop = check_arith_norm_exp current_pname cond prop__ in @@ -1145,7 +1145,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let ret_typ_opt = Option.map Cfg.Procdesc.get_ret_type callee_pdesc_opt in let sentinel_result = - if !Config.curr_language = Config.C_CPP then + if !Config.curr_language = Config.Clang then check_variadic_sentinel_if_present (call_args prop_r callee_pname actual_params ret_ids loc) else [(prop_r, path)] in @@ -1244,7 +1244,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path IList.map (Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_initial) (IList.map add_None ptl) in - run_in_re_execution_mode (* no footprint vars for locals *) + Config.run_in_re_execution_mode (* no footprint vars for locals *) sigma_locals () in let sigma' = Prop.get_sigma prop_ @ sigma_locals in let prop' = Prop.normalize (Prop.replace_sigma sigma' prop_) in @@ -1283,7 +1283,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call | hpred -> hpred) (Prop.get_sigma prop) in Prop.normalize (Prop.replace_sigma sigma' prop) in - if !Config.angelic_execution then + if Config.angelic_execution then let add_actual_by_ref_to_footprint prop (actual, actual_typ) = match actual with | Sil.Lvar actual_pv -> @@ -1391,7 +1391,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots IList.fold_left do_attribute p (Prop.get_exp_attributes p e) in IList.fold_left do_exp prop actual_pars in let add_tainted_pre prop actuals caller_pname callee_pname = - if !Config.taint_analysis then + if Config.taint_analysis then match Taint.accepts_sensitive_params callee_pname None with | [] -> prop | param_nums -> @@ -1587,7 +1587,7 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= act (* In case we call an objc instance method we add and extra spec *) (* were the receiver is null and the semantics of the call is nop*) let callee_attrs = Specs.get_attributes summary in - if (!Config.curr_language <> Config.Java) && !Config.objc_method_call_semantics && + if (!Config.curr_language <> Config.Java) && Config.objc_method_call_semantics && (Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then handle_objc_method_call actual_pars actual_params pre tenv ret_ids pdesc callee_pname loc path (Tabulation.exe_function_call callee_attrs) @@ -1646,7 +1646,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa L.d_str "Instruction "; Sil.d_instr instr; L.d_ln (); let prop', fav_normal = pre_process_prop prop in let res_list = - run_with_abs_val_equal_zero (* no exp abstraction during sym exe *) + Config.run_with_abs_val_equal_zero (* no exp abstraction during sym exe *) (fun () -> sym_exec tenv pdesc instr prop' path) () in let res_list_nojunk = @@ -1663,7 +1663,7 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa Paths.PathSet.from_renamed_list results with exn when Exceptions.handle_exception exn && !Config.footprint -> handle_exn exn; (* calls State.mark_instr_fail *) - if !Config.nonstop + if Config.nonstop then (* in nonstop mode treat the instruction as skip *) (Paths.PathSet.from_renamed_list [(prop, path)]) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 989d6ac87..9678bc592 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -336,7 +336,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = match deref_err_list with | [] -> None | deref_err :: _ -> - if !Config.angelic_execution then + if Config.angelic_execution then (* In angelic mode, prefer to report Deref_null over other kinds of deref errors. this * makes sure we report a NULL_DEREFERENCE instead of a less interesting PRECONDITION_NOT_MET @@ -554,7 +554,7 @@ let prop_footprint_add_pi_sigma_starfld_sigma let fav = Prop.sigma_fav [hpred] in (* TODO (t4893479): make this check less angelic *) if Sil.fav_exists fav - (fun id -> not (Ident.is_footprint id) && not !Config.angelic_execution) + (fun id -> not (Ident.is_footprint id) && not Config.angelic_execution) then begin L.d_warning "found hpred with non-footprint variable, dropping the spec"; L.d_ln (); Sil.d_hpred hpred; L.d_ln (); @@ -824,7 +824,7 @@ let add_param_taint proc_name formal_params prop param_nums = (* add Auntaint attribute to a callee_pname precondition *) let mk_pre pre formal_params callee_pname callee_attrs = - if !Config.taint_analysis then + if Config.taint_analysis then add_tainting_att_param_list (Prop.normalize pre) (Taint.accepts_sensitive_params callee_pname (Some callee_attrs)) @@ -902,10 +902,10 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts = IList.map taint_retval posts else posts in let posts' = - if !Config.idempotent_getters && !Config.curr_language = Config.Java + if Config.idempotent_getters && !Config.curr_language = Config.Java then mk_getter_idempotent posts else posts in - if !Config.taint_analysis then mk_retval_tainted posts' else posts' + if Config.taint_analysis then mk_retval_tainted posts' else posts' | _ -> posts (** Check if actual_pre * missing_footprint |- false *) @@ -1025,7 +1025,7 @@ let exe_spec Reporting.log_warning caller_pname exn in let do_split () = let missing_pi' = - if !Config.taint_analysis then + if Config.taint_analysis then do_taint_check caller_pname callee_pname actual_pre missing_pi sub2 else missing_pi in process_splitting @@ -1054,7 +1054,7 @@ let exe_spec IList.iter log_check_exn checks; let subbed_pre = (Prop.prop_sub sub1 actual_pre) in match check_dereferences callee_pname subbed_pre sub2 spec_pre formal_params with - | Some (Deref_undef _, _) when !Config.angelic_execution -> + | Some (Deref_undef _, _) when Config.angelic_execution -> let split = do_split () in report_valid_res split | Some (deref_error, desc) -> @@ -1249,7 +1249,7 @@ let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc result IList.length (Procname.java_get_parameters pn_java) = 0 | _ -> false in - (!Config.idempotent_getters && + (Config.idempotent_getters && !Config.curr_language = Config.Java && is_likely_getter callee_pname) || returns_nullable ret_annot in diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index 29855310d..be08d9e7e 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -154,7 +154,7 @@ let sinks = [ ret_type = "void"; params = []; is_static = false; - language = Config.C_CPP + language = Config.Clang }, [1]); (* it's instance method *) ] @ FbTaint.sinks @@ -166,7 +166,7 @@ let functions_with_tainted_params = [ ret_type = "BOOL"; params = []; is_static = false; (* it's instance method *) - language = Config.C_CPP + language = Config.Clang }, [2]); (* actual specs *) @@ -180,7 +180,7 @@ let functions_with_tainted_params = [ ret_type = "BOOL"; params = []; is_static = false; (* it's instance method *) - language = Config.C_CPP + language = Config.Clang }, [2]); ] @ FbTaint.functions_with_tainted_params @@ -203,7 +203,7 @@ let objc_method_to_procname objc_method = let method_str_to_pname method_str = match method_str.language with - | Config.C_CPP -> + | Config.Clang -> objc_method_to_procname method_str | Config.Java -> java_method_to_procname method_str diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 798796563..61cd6f1c9 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -362,8 +362,8 @@ let create_outfile fname = None (** operate on an outfile reference if it is not None *) -let do_outf outf_ref f = - match !outf_ref with +let do_outf outf_opt f = + match outf_opt with | None -> () | Some outf -> f outf @@ -464,238 +464,6 @@ let filename_to_relative root fname = remainder -(* Type of command-line arguments before processing *) -type arg_list = (string * Arg.spec * string option * string) list - -let arg_desc_filter options_to_keep = - IList.filter (function (option_name, _, _, _) -> IList.mem string_equal option_name options_to_keep) - -(* Given a filename with a list of paths, convert it into a list of string iff they are absolute *) -let read_specs_dir_list_file fname = - let validate_path path = - if Filename.is_relative path then - failwith ("Failing because path " ^ path ^ " is not absolute") in - match read_file fname with - | Some pathlist -> - IList.iter validate_path pathlist; - pathlist - | None -> failwith ("cannot read file " ^ fname) - -let base_arg_desc = - [ - "-results_dir", - Arg.String (fun s -> Config.results_dir := s), - Some "dir", - "set the project results directory (default dir=" ^ Config.default_results_dir ^ ")"; - - "-coverage", - Arg.Unit (fun () -> Config.worklist_mode:= 2), - None, - "analysis mode to maximize coverage (can take longer)"; - - "-lib", - Arg.String (fun s -> Config.specs_library := filename_to_absolute s :: !Config.specs_library), - Some "dir", - "add dir to the list of directories to be searched for spec files"; - - "-specs-dir-list-file", - Arg.String (fun s -> Config.specs_library := (read_specs_dir_list_file s) @ !Config.specs_library), - Some "file", - "add the newline-separated directories listed in to the list of directories to \ - be searched for spec files"; - - "-models", - Arg.String (fun s -> Config.add_models (filename_to_absolute s)), - Some "zip file", - "add a zip file containing the models"; - - "-ziplib", - Arg.String (fun s -> Config.add_zip_library (filename_to_absolute s)), - Some "zip file", - "add a zip file containing library spec files"; - - "-project_root", - Arg.String (fun s -> Config.project_root := Some (filename_to_absolute s)), - Some "dir", - "root directory of the project"; - - "-infer_cache", - Arg.String (fun s -> Config.infer_cache := Some (filename_to_absolute s)), - Some "dir", - "Select a directory to contain the infer cache"; - - "-inferconfig_home", - Arg.String (fun s -> Config.inferconfig_home := Some s), - Some "dir", - "Path to the .inferconfig file"; - ] - -let reserved_arg_desc = - [ - "-absstruct", - Arg.Set_int Config.abs_struct, - Some "n", - "abstraction level for fields of structs (default n = 1)" - ; - "-absval", - Arg.Set_int Config.abs_val, - Some "n", - "abstraction level for expressions (default n = 2)"; - "-arraylevel", - Arg.Set_int Config.array_level, - Some "n", - "the level of treating the array indexing and pointer arithmetic (default n = 0)" - ; - "-developer_mode", - Arg.Set Config.developer_mode, - None, - "reserved" - ; - "-dotty", - Arg.Set Config.write_dotty, - None, - "produce dotty files in the results directory"; - "-exit_node_bias", - Arg.Unit (fun () -> Config.worklist_mode:= 1), - None, - "nodes nearest the exit node are analyzed first"; - "-html", - Arg.Set Config.write_html, - None, - "produce hmtl output in the results directory" - ; - "-join_cond", - Arg.Set_int Config.join_cond, - Some "n", - "set the strength of the final information-loss check used by the join (default n=1)" - ; - "-leak", - Arg.Set Config.allowleak, - None, - "forget leaks during abstraction" - ; - "-monitor_prop_size", - Arg.Set Config.monitor_prop_size, - None, - "monitor size of props" - ; - "-nelseg", - Arg.Set Config.nelseg, - None, - "use only nonempty lsegs" - ; - "-noliveness", - Arg.Clear Config.liveness, - None, - "turn the dead program variable elimination off" - ; - "-noprintdiff", - Arg.Clear Config.print_using_diff, - None, - "turn off highlighting diff w.r.t. previous prop in printing" - ; - "-notest", - Arg.Clear Config.test, - None, - "turn test mode off" - ; - "-only_footprint", - Arg.Set Config.only_footprint, - None, - "skip the re-execution phase" - ; - "-print_types", - Arg.Set Config.print_types, - None, - "print types in symbolic heaps" - ; - "-set_pp_margin", - Arg.Int (fun i -> F.set_margin i), - Some "n", - "set right margin for the pretty printing functions" - ; - "-spec_abs_level", - Arg.Set_int Config.spec_abs_level, - Some "n", - "set the level of abstracting the postconditions of discovered specs (default n=1)" - ; - "-trace_error", - Arg.Set Config.trace_error, - None, - "turn on tracing of error explanation" - ; - "-trace_join", - Arg.Set Config.trace_join, - None, - "turn on tracing of join" - ; - "-trace_rearrange", - Arg.Set Config.trace_rearrange, - None, - "turn on tracing of rearrangement" - ; - "-visits_bias", - Arg.Unit (fun () -> Config.worklist_mode:= 2), - None, - "nodes visited fewer times are analyzed first" - ; - ] - - -module Arg = struct - - include Arg - - (** Custom version of Arg.aling so that keywords are on one line and documentation is on the next *) - let align arg_desc = - let do_arg (key, spec, doc) = - let first_space = - try - let index = String.index doc ' ' in - if String.get doc index = '=' then 0 else index - with Not_found -> 0 in - let len = String.length doc in - let doc1 = String.sub doc 0 first_space in - let doc2 = String.sub doc first_space (len - first_space) in - if len = 0 then (key, spec, doc) - else (key, spec, doc1 ^ "\n " ^ doc2) in - IList.map do_arg arg_desc - - type aligned = (key * spec * doc) - - (** Create a group of sorted command-line arguments *) - let create_options_desc double_minus title unsorted_desc = - let handle_double_minus (opname, spec, param_opt, text) = match param_opt with - | None -> - if double_minus then ("-"^opname, spec, " " ^ text) - else (opname, spec, " " ^ text) - | Some param -> - if double_minus then ("-"^opname, spec, "=" ^ param ^ " " ^ text) - else (opname, spec, param ^ " " ^ text) in - let unsorted_desc' = IList.map handle_double_minus unsorted_desc in - let dlist = - ("", Arg.Unit (fun () -> ()), " \n " ^ title ^ "\n") :: - IList.sort (fun (x, _, _) (y, _, _) -> Pervasives.compare x y) unsorted_desc' in - align dlist - - let env_to_argv env = - Str.split (Str.regexp ":") env - - let prepend_to_argv args = - let cl_args = match Array.to_list Sys.argv with _ :: tl -> tl | [] -> [] in - Sys.executable_name :: args @ cl_args - - let parse env_var spec anon usage = - let env_args = env_to_argv (try Unix.getenv env_var with Not_found -> "") in - let env_cl_args = prepend_to_argv env_args in - try - Arg.parse_argv (Array.of_list env_cl_args) spec anon usage - with - | Bad usage -> Pervasives.prerr_string usage; exit 2; - | Help usage -> Pervasives.print_string usage; exit 0; - -end - (** flags for a procedure *) type proc_flags = (string, string) Hashtbl.t @@ -767,26 +535,24 @@ let directory_iter f path = type analyzer = Infer | Eradicate | Checkers | Tracing -let analyzers = [Infer; Eradicate; Checkers; Tracing] +let string_to_analyzer = + [("infer", Infer); ("eradicate", Eradicate); ("checkers", Checkers); ("tracing", Tracing)] + +let analyzers = IList.map snd string_to_analyzer -let string_of_analyzer = function - | Infer -> "infer" - | Eradicate -> "eradicate" - | Checkers -> "checkers" - | Tracing -> "tracing" +let string_of_analyzer = + let analyzer_to_string = IList.map (fun (a,n) -> (n,a)) string_to_analyzer in + fun analyzer -> + IList.assoc ( = ) analyzer analyzer_to_string exception Unknown_analyzer -let analyzer_of_string = function - | "infer" -> Infer - | "eradicate" -> Eradicate - | "checkers" -> Checkers - | "tracing" -> Tracing - | _ -> raise Unknown_analyzer +let analyzer_of_string name = + try IList.assoc string_equal name string_to_analyzer + with Not_found -> raise Unknown_analyzer -let string_crc_hex32 = - Config.string_crc_hex32 (* implemented in Config to avoid circularities *) +let string_crc_hex32 s = Digest.to_hex (Digest.string s) let string_append_crc_cutoff ?(cutoff=100) ?(key="") name = let name_up_to_cutoff = @@ -797,26 +563,3 @@ let string_append_crc_cutoff ?(cutoff=100) ?(key="") name = let name_for_crc = name ^ key in string_crc_hex32 name_for_crc in name_up_to_cutoff ^ "." ^ crc_str - -let set_reference_and_call_function reference value f x = - let saved = !reference in - let restore () = - reference := saved in - try - reference := value; - let res = f x in - restore (); - res - with - | exn -> - restore (); - raise exn - -let run_in_re_execution_mode f x = - set_reference_and_call_function Config.footprint false f x - -let run_in_footprint_mode f x = - set_reference_and_call_function Config.footprint true f x - -let run_with_abs_val_equal_zero f x = - set_reference_and_call_function Config.abs_val 0 f x diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index 3ebe4fb5a..89751b565 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -148,36 +148,6 @@ val pp_current_time : Format.formatter -> unit -> unit (** Print the time in seconds elapsed since the beginning of the execution of the current command. *) val pp_elapsed_time : Format.formatter -> unit -> unit - -module Arg : sig - include module type of Arg with type spec = Arg.spec - - (** type of aligned commend-line options *) - type aligned = private (key * spec * doc) - - val align : (key * spec * doc) list -> aligned list - - (** [parse env_var arg_desc anon_fun usage_msg] prepends the decoded value of environment variable - [env_var] to [Sys.argv] and then parses the result using the standard [Arg.parse]. Therefore - arguments passed on the command line supercede those specified in the environment variable. - WARNING: If an argument appears both in the environment variable and on the command line, it - will be interpreted twice. *) - val parse : string -> aligned list -> anon_fun -> usage_msg -> unit - - val usage : aligned list -> usage_msg -> unit - - (** [create_options_desc double_minus unsorted_desc title] creates a group of sorted command-line arguments. - [double_minus] is a booleand indicating whether the [-- option = nn] format or [- option n] format is to be used. - [title] is the title of this group of options. - It expects a list [opname, desc, param_opt, text] where - [opname] is the name of the option - [desc] is the Arg.spec - [param_opt] is the optional parameter to [opname] - [text] is the description of the option *) - val create_options_desc : bool -> string -> (string * Arg.spec * string option * string) list -> aligned list - -end - (** Compute a 32-character hexadecimal crc using the Digest module *) val string_crc_hex32 : string -> string @@ -229,23 +199,11 @@ type outfile = val create_outfile : string -> outfile option (** operate on an outfile reference if it is not None *) -val do_outf : outfile option ref -> (outfile -> unit) -> unit +val do_outf : outfile option -> (outfile -> unit) -> unit (** close an outfile *) val close_outf : outfile -> unit -(* Type of command-line arguments before processing *) -type arg_list = (string * Arg.spec * string option * string) list - -(* Filter arguments by name, i.e. keep those whose name appears in the name list *) -val arg_desc_filter : string list -> arg_list -> arg_list - -(** Basic command-line arguments *) -val base_arg_desc : arg_list - -(** Reserved command-line arguments *) -val reserved_arg_desc : arg_list - (** flags for a procedure *) type proc_flags = (string, string) Hashtbl.t @@ -282,25 +240,12 @@ val directory_iter : (string -> unit) -> string -> unit (** Various kind of analyzers *) type analyzer = Infer | Eradicate | Checkers | Tracing +(** Association list of analyzers and their names *) +val string_to_analyzer : (string * analyzer) list + (** List of analyzers *) val analyzers: analyzer list val string_of_analyzer: analyzer -> string val analyzer_of_string: string -> analyzer - -(** Call f x with Config.abs_val set to zero. - Restore the initial value also in case of exception. *) -val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b - -(** Call f x with Config.footprint set to true. - Restore the initial value of footprint also in case of exception. *) -val run_in_footprint_mode : ('a -> 'b) -> 'a -> 'b - -(** Call f x with Config.footprint set to false. - Restore the initial value of footprint also in case of exception. *) -val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b - -(** [set_reference_and_call_function ref val f x] calls f x with ref set to val. - Restore the initial value also in case of exception. *) -val set_reference_and_call_function : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c diff --git a/infer/src/backend/zipLib.ml b/infer/src/backend/zipLib.ml index 04abafdda..4753d69fb 100644 --- a/infer/src/backend/zipLib.ml +++ b/infer/src/backend/zipLib.ml @@ -24,33 +24,33 @@ let load_from_cache serializer zip_path cache_dir zip_library = if not (Sys.file_exists to_path) then begin DB.create_path (Filename.dirname to_path); - let zip_channel = Config.zip_channel zip_library in + let lazy zip_channel = zip_library.Config.zip_channel in let entry = Zip.find_entry zip_channel zip_path in Zip.copy_entry_to_file zip_channel entry to_path end; DB.filename_from_string to_path in match deserialize (extract absolute_path) with - | Some data when Config.is_models zip_library -> Some (data, DB.Models) + | Some data when zip_library.Config.models -> Some (data, DB.Models) | Some data -> Some (data, DB.Spec_lib) | None -> None | exception Not_found -> None let load_from_zip serializer zip_path zip_library = - let zip_channel = Config.zip_channel zip_library in + let lazy zip_channel = zip_library.Config.zip_channel in let deserialize = Serialization.from_string serializer in match deserialize (Zip.read_entry zip_channel (Zip.find_entry zip_channel zip_path)) with - | Some data when Config.is_models zip_library -> Some (data, DB.Models) + | Some data when zip_library.Config.models -> Some (data, DB.Models) | Some data -> Some (data, DB.Spec_lib) | None -> None | exception Not_found -> None let load_data serializer path zip_library = let zip_path = Filename.concat Config.default_in_zip_results_dir path in - match !Config.infer_cache with + match Config.infer_cache with | None -> load_from_zip serializer zip_path zip_library | Some infer_cache -> - let cache_dir = get_cache_dir infer_cache (Config.zip_filename zip_library) in + let cache_dir = get_cache_dir infer_cache zip_library.Config.zip_filename in load_from_cache serializer zip_path cache_dir zip_library (* Search path in the list of zip libraries and use a cache directory to save already @@ -62,4 +62,4 @@ let load serializer path = let opt = load_data serializer path zip_library in if Option.is_some opt then opt else loop other_libraries in - loop (Config.get_zip_libraries ()) + loop Config.zip_libraries diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml index 8e472c9f1..8f4ea1401 100644 --- a/infer/src/checkers/codeQuery.ml +++ b/infer/src/checkers/codeQuery.ml @@ -15,7 +15,6 @@ module L = Logging module F = Format let verbose = false -let query = ref None let parse_query s = let buf = Lexing.from_string s in @@ -34,7 +33,7 @@ let parse_query s = assert false let query_ast = - lazy (match !query with None -> parse_query "x(y)" | Some s -> parse_query s) + 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. *) diff --git a/infer/src/checkers/codeQuery.mli b/infer/src/checkers/codeQuery.mli index 137d20427..f7a2a3540 100644 --- a/infer/src/checkers/codeQuery.mli +++ b/infer/src/checkers/codeQuery.mli @@ -12,5 +12,3 @@ open! Utils (** Module for code queries. *) val code_query_callback : Callbacks.proc_callback_t - -val query : string option ref diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 3d7870c37..c7be732b7 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -16,7 +16,7 @@ module F = Format (** Flags to activate checkers. *) let active_procedure_checkers () = - let checkers_enabled = Config.checkers_enabled () in + let checkers_enabled = Config.checkers_enabled in let java_checkers = let l = @@ -31,8 +31,8 @@ let active_procedure_checkers () = Dataflow.callback_test_dataflow, false; FragmentRetainsViewChecker.callback_fragment_retains_view, checkers_enabled; SqlChecker.callback_sql, false; - Eradicate.callback_eradicate, !Config.eradicate; - CodeQuery.code_query_callback, !CodeQuery.query <> None; + Eradicate.callback_eradicate, Config.eradicate; + 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; @@ -46,7 +46,7 @@ let active_procedure_checkers () = Checkers.callback_print_c_method_calls, false; CheckDeadCode.callback_check_dead_code, checkers_enabled; ] in - IList.map (fun (x, y) -> (x, y, Some Config.C_CPP)) l in + IList.map (fun (x, y) -> (x, y, Some Config.Clang)) l in java_checkers @ c_cpp_checkers diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 84012d4f7..aa4cc66c6 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -150,7 +150,7 @@ let unary_operation_instruction uoi e typ loc = let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in - let exp = if General_utils.is_cpp_translation !CFrontend_config.language then + let exp = if General_utils.is_cpp_translation Config.clang_lang then e else e_plus_1 in @@ -164,7 +164,7 @@ let unary_operation_instruction uoi e typ loc = let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in - let exp = if General_utils.is_cpp_translation !CFrontend_config.language then + let exp = if General_utils.is_cpp_translation Config.clang_lang then e else e_minus_1 in diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index 342f56656..6c40c0dd8 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -34,16 +34,16 @@ let compute_icfg tenv ast = | _ -> assert false (* NOTE: Assumes that an AST alsways starts with a TranslationUnitDecl *) let register_perf_stats_report source_file = - let stats_dir = Filename.concat !Config.results_dir Config.frontend_stats_dir_name in + let stats_dir = Filename.concat Config.results_dir Config.frontend_stats_dir_name in let abbrev_source_file = DB.source_file_encoding source_file in let stats_file = Config.perf_stats_prefix ^ "_" ^ abbrev_source_file ^ ".json" in - DB.create_dir !Config.results_dir ; + DB.create_dir Config.results_dir ; DB.create_dir stats_dir ; PerfStats.register_report_at_exit (Filename.concat stats_dir stats_file) let init_global_state source_file = register_perf_stats_report source_file ; - Config.curr_language := Config.C_CPP; + Config.curr_language := Config.Clang; DB.current_source := source_file; DB.Results_dir.init (); Ident.NameGenerator.reset (); @@ -74,8 +74,8 @@ let do_source_file source_file ast = (*Printing.print_procedures cfg; *) General_utils.sort_fields_tenv tenv; Tenv.store_to_file tenv_file tenv; - if !CFrontend_config.stats_mode then Cfg.check_cfg_connectedness cfg; - if !CFrontend_config.stats_mode - || !CFrontend_config.debug_mode || !CFrontend_config.testing_mode then + if Config.stats_mode then Cfg.check_cfg_connectedness cfg; + if Config.stats_mode + || Config.debug_mode || Config.testing_mode then (Dotty.print_icfg_dotty cfg []; Cg.save_call_graph_dotty None Specs.get_specs call_graph) diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index b0dd95ae6..d851fcd21 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -11,12 +11,6 @@ open! Utils (** Module that contains constants and variables used in the frontend *) -let no_translate_libs = ref true - -let testing_mode = ref false - -let cxx_experimental = ref false - let array_with_objects_count_m = "arrayWithObjects:count:" let object_at_indexed_subscript_m = "objectAtIndexedSubscript:" @@ -49,46 +43,12 @@ let free = "free" let static = "static" -let source_file : string option ref = ref None - -let ast_file : string option ref = ref None - let json = ref "" let pointer_decl_index = ref Clang_ast_main.PointerMap.empty let pointer_stmt_index = ref Clang_ast_main.PointerMap.empty -let debug_mode = ref false - -let stats_mode = ref false - -let models_mode = ref false - -type lang = - | C - | CPP - | OBJC - | OBJCPP - -let language = ref OBJC (* Default is objc, since it's the default for clang (at least in Mac OS) *) - -let lang_from_string lang_string = - let lang = - if lang_string = "c" then C - else if lang_string = "objective-c" then OBJC - else if lang_string = "c++" then CPP - else if lang_string = "objective-c++" then OBJCPP - else assert false in - language := lang - -let lang_to_string lang = - match lang with - | C -> "c" - | OBJC -> "objective-c" - | CPP -> "c++" - | OBJCPP -> "objective-c++" - let emtpy_name_category ="EMPTY_NAME_CATEGORY_FOR_" let objc_object = "objc_object" diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index 06a0ec274..3d4da1bd4 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -13,36 +13,6 @@ open! Utils val global_translation_unit_decls : Clang_ast_t.decl list ref -(** arguments of InferClang *) - -val debug_mode : bool ref - -val stats_mode : bool ref - -val models_mode : bool ref - -val source_file : string option ref - -type lang = - | C - | CPP - | OBJC - | OBJCPP - -val lang_from_string : string -> unit - -val lang_to_string : lang -> string - -val language : lang ref - -val ast_file : string option ref - -val no_translate_libs : bool ref - -val testing_mode : bool ref - -val cxx_experimental : bool ref - (** constants *) val json : string ref diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index e1b1d00fb..6508223d9 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -27,7 +27,7 @@ module CFrontend_decl_funct(T: CModule_type.CTranslation) : CFrontend_decl = struct let model_exists procname = - Specs.summary_exists_in_models procname && not !CFrontend_config.models_mode + Specs.summary_exists_in_models procname && not Config.models_mode (* Translates the method/function's body into nodes of the cfg. *) let add_method tenv cg cfg class_decl_opt procname body has_return_param is_objc_method @@ -189,7 +189,7 @@ struct | Some (ClassTemplateSpecializationDecl _ as d) -> let class_name = CTypes_decl.get_record_name d in let curr_class = CContext.ContextCls(class_name, None, []) in - if !CFrontend_config.cxx_experimental then + if Config.cxx_experimental then process_methods tenv cg cfg curr_class [dec] | Some dec -> Printing.log_stats "Methods of %s skipped\n" (Ast_utils.string_of_decl dec) diff --git a/infer/src/clang/cFrontend_utils.ml b/infer/src/clang/cFrontend_utils.ml index 6836ada7d..6e5ccb3d5 100644 --- a/infer/src/clang/cFrontend_utils.ml +++ b/infer/src/clang/cFrontend_utils.ml @@ -18,11 +18,11 @@ module F = Format module Printing = struct let log_out fmt = - let pp = if !CFrontend_config.debug_mode then Format.fprintf else Format.ifprintf in + let pp = if Config.debug_mode then Format.fprintf else Format.ifprintf in pp Format.std_formatter fmt let log_err fmt = - let pp = if !CFrontend_config.debug_mode then Format.fprintf else Format.ifprintf in + let pp = if Config.debug_mode then Format.fprintf else Format.ifprintf in pp Format.err_formatter fmt @@ -36,7 +36,7 @@ struct let log_stats fmt = let pp = - if !CFrontend_config.stats_mode || !CFrontend_config.debug_mode + if Config.stats_mode || Config.debug_mode then Format.fprintf else Format.ifprintf in pp Format.std_formatter fmt @@ -405,13 +405,13 @@ struct | _ -> false let is_objc () = - match !CFrontend_config.language with - | CFrontend_config.OBJC -> true + match Config.clang_lang with + | Config.OBJC -> true | _ -> false let is_objcpp () = - match !CFrontend_config.language with - | CFrontend_config.OBJCPP -> true + match Config.clang_lang with + | Config.OBJCPP -> true | _ -> false (* @@ -569,7 +569,7 @@ struct let get_rel_file_path file_opt = match file_opt with | Some file -> - (match !Config.project_root with + (match Config.project_root with | Some root -> DB.source_file_to_rel_path (DB.rel_source_file_from_abs_path root file) | None -> file) @@ -587,8 +587,8 @@ struct | None -> "" in let type_string = match language with - | CFrontend_config.CPP - | CFrontend_config.OBJCPP -> Ast_utils.string_of_type_ptr tp + | Config.CPP + | Config.OBJCPP -> Ast_utils.string_of_type_ptr tp | _ -> "" in (* remove __restrict from type name to avoid mismatches. Clang allows to declare function*) (* with __restrict parameters and then define it without (it mostly applies to models).*) @@ -644,10 +644,6 @@ struct | None -> Pvar.mk (Mangled.from_string name_string) procname let is_cpp_translation language = - language = CFrontend_config.CPP || language = CFrontend_config.OBJCPP + language = Config.CPP || language = Config.OBJCPP end - - - - diff --git a/infer/src/clang/cFrontend_utils.mli b/infer/src/clang/cFrontend_utils.mli index 0b9723303..6103d97c8 100644 --- a/infer/src/clang/cFrontend_utils.mli +++ b/infer/src/clang/cFrontend_utils.mli @@ -197,7 +197,7 @@ sig val mk_procname_from_objc_method : string -> string -> Procname.objc_method_kind -> Procname.t val mk_procname_from_function : string -> (Clang_ast_t.decl_info * Clang_ast_t.function_decl_info) - option -> Clang_ast_t.type_ptr -> CFrontend_config.lang -> Procname.t + option -> Clang_ast_t.type_ptr -> Config.clang_lang -> Procname.t val mk_procname_from_cpp_method : string -> string -> Clang_ast_t.type_ptr -> Procname.t @@ -208,6 +208,6 @@ sig val mk_sil_var : Clang_ast_t.named_decl_info -> var_info option -> Procname.t -> Procname.t -> Pvar.t - val is_cpp_translation : CFrontend_config.lang -> bool + val is_cpp_translation : Config.clang_lang -> bool end diff --git a/infer/src/clang/cLocation.ml b/infer/src/clang/cLocation.ml index 8a7a2622c..375144c38 100644 --- a/infer/src/clang/cLocation.ml +++ b/infer/src/clang/cLocation.ml @@ -24,7 +24,7 @@ let source_file_from_path path = "ERROR: Path %s is relative. Please pass an absolute path in the -c argument.@." path; exit 1); - match !Config.project_root with + match Config.project_root with | Some root -> (try DB.rel_source_file_from_abs_path root path @@ -77,7 +77,7 @@ let clang_to_sil_location clang_loc procdesc_opt = Location.{line; col; file; nLOC} let file_in_project file = - match !Config.project_root with + match Config.project_root with | Some root -> let file_in_project = string_is_prefix root file in let paths = Lazy.force Inferconfig.skip_translation_headers in @@ -96,7 +96,7 @@ let should_do_frontend_check (loc_start, _) = let equal_current_source file = DB.source_file_equal (source_file_from_path file) !DB.current_source in equal_current_source file || - (file_in_project file && not !CFrontend_config.testing_mode) + (file_in_project file && not Config.testing_mode) (* We translate by default the instructions in the current file.*) (* In C++ development, we also translate the headers that are part *) @@ -126,11 +126,11 @@ let should_translate (loc_start, loc_end) decl_trans_context = || map_file_of equal_current_source loc_end || map_file_of equal_current_source loc_start || file_in_models - || (!CFrontend_config.cxx_experimental && decl_trans_context = `Translation && file_in_project - && not (!CFrontend_config.testing_mode)) + || (Config.cxx_experimental && decl_trans_context = `Translation && file_in_project + && not Config.testing_mode) let should_translate_lib source_range decl_trans_context = - not !CFrontend_config.no_translate_libs + not Config.no_translate_libs || should_translate source_range decl_trans_context let get_sil_location_from_range source_range prefer_first = diff --git a/infer/src/clang/cMain.ml b/infer/src/clang/cMain.ml index bc21b7a92..1043a2e00 100644 --- a/infer/src/clang/cMain.ml +++ b/infer/src/clang/cMain.ml @@ -17,91 +17,6 @@ module L = Logging open CFrontend_utils -let arg_desc = - let desc = - (Utils.arg_desc_filter ["-results_dir"] base_arg_desc) @ - [ - "-c", - Arg.String (fun cfile -> CFrontend_config.source_file := Some cfile), - Some "cfile", - "C File to translate" - ; - "-x", - Arg.String (fun lang -> CFrontend_config.lang_from_string lang), - Some "cfile", - "Language (c, objective-c, c++, objc-++)" - ; - "-ast", - Arg.String (fun file -> CFrontend_config.ast_file := Some file), - Some "file", - "AST file for the translation" - ; - "-dotty_no_cfg_libs", - Arg.Unit (fun _ -> Config.dotty_cfg_libs := false), - None, - "Prints the cfg of the code coming from the libraries" - ; - "-no_headers", - Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := true), - None, - "Do not translate code in header files (default)" - ; - "-headers", - Arg.Unit (fun _ -> CFrontend_config.no_translate_libs := false), - None, - "Translate code in header files" - ; - "-testing_mode", - Arg.Unit (fun _ -> CFrontend_config.testing_mode := true), - None, - "Mode for testing, where no headers are translated, \ - and dot files are created" - ; - "-debug", - Arg.Unit (fun _ -> CFrontend_config.debug_mode := true), - None, - "Enables debug mode" - ; - "-stats", - Arg.Unit (fun _ -> CFrontend_config.stats_mode := true), - None, - "Enables stats mode" - ; - "-project_root", - Arg.String (fun s -> - Config.project_root := Some (Utils.filename_to_absolute s)), - Some "dir", - "Toot directory of the project" - ; - "-fobjc-arc", - Arg.Unit (fun _ -> Config.arc_mode := true), - None, - "Translate with Objective-C Automatic Reference Counting (ARC)" - ; - "-models_mode", - Arg.Unit (fun _ -> CFrontend_config.models_mode := true), - None, - "Mode for computing the models" - ; - "-cxx-experimental", - Arg.Unit (fun _ -> CFrontend_config.cxx_experimental := true), - None, - "Analyze C++ methods, still experimental" - ; - "-inferconfig_home", - Arg.String (fun s -> Config.inferconfig_home := Some s), - Some "dir", - "Path to the .inferconfig file"; - ] in - Arg.create_options_desc false "Parsing Options" desc - -let usage = - "\nUsage: InferClang -c C Files -ast AST Files -results_dir [options] \n" - -let print_usage_exit () = - Arg.usage arg_desc usage; - exit(1) - let buffer_len = 16384 (* This function reads the json file in fname, validates it, and encoded in the AST data structure*) @@ -141,9 +56,6 @@ let do_run source_path ast_path = CFrontend_config.json := ast_filename; CLocation.check_source_file source_path; let source_file = CLocation.source_file_from_path source_path in - (match !Config.inferconfig_home with - | Some _ -> () - | None -> Config.inferconfig_home := !Config.project_root); Printf.printf "Start translation of AST from %s\n" !CFrontend_config.json; CFrontend.do_source_file source_file ast_decl; Printf.printf "End translation AST file %s... OK!\n" !CFrontend_config.json; @@ -155,14 +67,9 @@ let do_run source_path ast_path = raise exc let () = - Arg.parse "INFERCLANG_ARGS" arg_desc (fun _ -> ()) usage ; - Config.print_types := true; - if Option.is_none !CFrontend_config.source_file then - (Printing.log_err "Incorrect command line arguments\n"; - print_usage_exit ()) - else - match !CFrontend_config.source_file with - | Some path -> - do_run path !CFrontend_config.ast_file - | None -> - assert false + match Config.source_file with + | Some path -> + do_run path Config.ast_file + | None -> + Printing.log_err "Incorrect command line arguments\n"; + Config.print_usage_exit () diff --git a/infer/src/clang/cMethod_signature.ml b/infer/src/clang/cMethod_signature.ml index dec40ebea..7e53a34ad 100644 --- a/infer/src/clang/cMethod_signature.ml +++ b/infer/src/clang/cMethod_signature.ml @@ -20,7 +20,7 @@ type method_signature = { loc : Clang_ast_t.source_range; is_instance : bool; is_cpp_virtual : bool; - language : CFrontend_config.lang; + language : Config.clang_lang; pointer_to_parent : Clang_ast_t.pointer option; pointer_to_property_opt : Clang_ast_t.pointer option; (* If set then method is a getter/setter *) return_param_typ : Sil.typ option; diff --git a/infer/src/clang/cMethod_signature.mli b/infer/src/clang/cMethod_signature.mli index ced30bdcf..4026099ac 100644 --- a/infer/src/clang/cMethod_signature.mli +++ b/infer/src/clang/cMethod_signature.mli @@ -31,7 +31,7 @@ val ms_is_instance : method_signature -> bool val ms_is_cpp_virtual : method_signature -> bool -val ms_get_lang : method_signature -> CFrontend_config.lang +val ms_get_lang : method_signature -> Config.clang_lang val ms_get_pointer_to_parent : method_signature -> Clang_ast_t.pointer option @@ -45,7 +45,7 @@ val ms_is_setter : method_signature -> bool val make_ms : Procname.t -> (string * Clang_ast_t.type_ptr) list -> Clang_ast_t.type_ptr -> Clang_ast_t.attribute list -> Clang_ast_t.source_range -> bool -> ?is_cpp_virtual:bool - -> CFrontend_config.lang -> Clang_ast_t.pointer option -> Clang_ast_t.pointer option + -> Config.clang_lang -> Clang_ast_t.pointer option -> Clang_ast_t.pointer option -> Sil.typ option -> method_signature val replace_name_ms : method_signature -> Procname.t -> method_signature diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 001bc4ba5..eefffea4e 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -29,7 +29,7 @@ type method_call_type = | MCStatic type function_method_decl_info = - | Func_decl_info of Clang_ast_t.function_decl_info * Clang_ast_t.type_ptr * CFrontend_config.lang + | Func_decl_info of Clang_ast_t.function_decl_info * Clang_ast_t.type_ptr * Config.clang_lang | Cpp_Meth_decl_info of Clang_ast_t.function_decl_info * Clang_ast_t.cxx_method_decl_info * string * Clang_ast_t.type_ptr | ObjC_Meth_decl_info of Clang_ast_t.obj_c_method_decl_info * string | Block_decl_info of Clang_ast_t.block_decl_info * Clang_ast_t.type_ptr * CContext.t @@ -92,9 +92,9 @@ let get_param_decls function_method_decl_info = let get_language function_method_decl_info = match function_method_decl_info with | Func_decl_info (_, _, language) -> language - | Cpp_Meth_decl_info _ -> CFrontend_config.CPP - | ObjC_Meth_decl_info _ -> CFrontend_config.OBJC - | Block_decl_info _ -> CFrontend_config.OBJC + | Cpp_Meth_decl_info _ -> Config.CPP + | ObjC_Meth_decl_info _ -> Config.OBJC + | Block_decl_info _ -> Config.OBJC let is_cpp_virtual function_method_decl_info = match function_method_decl_info with @@ -155,7 +155,7 @@ let method_signature_of_decl tenv meth_decl block_data_opt = match meth_decl, block_data_opt with | FunctionDecl (decl_info, name_info, tp, fdi), _ -> let name = Ast_utils.get_qualified_name name_info in - let language = !CFrontend_config.language in + let language = Config.clang_lang in let func_decl = Func_decl_info (fdi, tp, language) in let function_info = Some (decl_info, fdi) in let procname = General_utils.mk_procname_from_function name function_info tp language in @@ -306,9 +306,9 @@ let get_formal_parameters tenv ms = | (name, raw_type):: pl' -> let should_add_pointer name ms = let is_objc_self = name = CFrontend_config.self && - CMethod_signature.ms_get_lang ms = CFrontend_config.OBJC in + CMethod_signature.ms_get_lang ms = Config.OBJC in let is_cxx_this = name = CFrontend_config.this && - CMethod_signature.ms_get_lang ms = CFrontend_config.CPP in + CMethod_signature.ms_get_lang ms = Config.CPP in (is_objc_self && CMethod_signature.ms_is_instance ms) || is_cxx_this in let tp = if should_add_pointer name ms then (Ast_expressions.create_pointer_type raw_type) @@ -366,7 +366,7 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let method_annotation = sil_method_annotation_of_args (CMethod_signature.ms_get_args ms) in let is_cpp_inst_method = CMethod_signature.ms_is_instance ms - && CMethod_signature.ms_get_lang ms = CFrontend_config.CPP in + && CMethod_signature.ms_get_lang ms = Config.CPP in let create_new_procdesc () = let formals = get_formal_parameters tenv ms in let captured_str = @@ -381,7 +381,7 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let captured' = IList.map (fun (var, t) -> (Pvar.get_name var, t)) captured in let procdesc = let proc_attributes = - { (ProcAttributes.default proc_name Config.C_CPP) with + { (ProcAttributes.default proc_name Config.Clang) with ProcAttributes.captured = captured'; ProcAttributes.objc_accessor = get_objc_property_accessor tenv ms; formals; @@ -419,7 +419,7 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt = | None -> Sil.Tvoid, []) in let loc = Location.dummy in let proc_attributes = - { (ProcAttributes.default proc_name Config.C_CPP) with + { (ProcAttributes.default proc_name Config.Clang) with ProcAttributes.formals; is_objc_instance_method = is_objc_inst_method; loc; @@ -439,7 +439,7 @@ let create_procdesc_with_pointer context pointer class_name_opt name tp = | Some class_name -> General_utils.mk_procname_from_cpp_method class_name name tp | None -> - General_utils.mk_procname_from_function name None tp !CFrontend_config.language in + General_utils.mk_procname_from_function name None tp Config.clang_lang in create_external_procdesc context.cfg callee_name false None; callee_name @@ -449,7 +449,7 @@ let get_method_for_frontend_checks cfg cg loc = match Cfg.Procdesc.find_from_name cfg proc_name with | Some pdesc -> pdesc | None -> - let attrs = { (ProcAttributes.default proc_name Config.C_CPP) with + let attrs = { (ProcAttributes.default proc_name Config.Clang) with is_defined = true; loc = loc; } in @@ -465,7 +465,7 @@ let get_method_for_frontend_checks cfg cg loc = let add_default_method_for_class class_name decl_info = let loc = CLocation.get_sil_location_from_range decl_info.Clang_ast_t.di_source_range true in let proc_name = Procname.get_default_objc_class_method class_name in - let attrs = { (ProcAttributes.default proc_name Config.C_CPP) with loc = loc; } in + let attrs = { (ProcAttributes.default proc_name Config.Clang) with loc = loc; } in AttributesTable.store_attributes attrs let get_procname_from_cpp_lambda context dec = diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index e2c018ddf..b2154c077 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -58,7 +58,7 @@ struct | Procname.ObjC_Cpp objc_cpp -> let class_name = Procname.objc_cpp_get_class_name objc_cpp in CTrans_models.get_predefined_model_method_signature class_name selector - General_utils.mk_procname_from_objc_method CFrontend_config.OBJC + General_utils.mk_procname_from_objc_method Config.OBJC | _ -> None in match predefined_ms_opt, ms_opt with @@ -458,8 +458,8 @@ struct (* As e.g. in fun_ptr = foo; *) let non_mangled_func_name = if name = CFrontend_config.malloc && - (!CFrontend_config.language = CFrontend_config.OBJC || - !CFrontend_config.language = CFrontend_config.OBJCPP) then + (Config.clang_lang = Config.OBJC || + Config.clang_lang = Config.OBJCPP) then ModelBuiltins.malloc_no_fail else Procname.from_string_c_fun name in let is_builtin = Builtin.is_registered non_mangled_func_name in @@ -771,7 +771,7 @@ struct if (is_binary_assign_op binary_operator_info) (* assignment operator result is lvalue in CPP, rvalue in C, *) (* hence the difference *) - && (not (General_utils.is_cpp_translation !CFrontend_config.language)) + && (not (General_utils.is_cpp_translation Config.clang_lang)) && ((not creating_node) || (is_return_temp trans_state.continuation)) then ( (* We are in this case when an assignment is inside *) (* another operator that creates a node. Eg. another *) diff --git a/infer/src/clang/cTrans_models.mli b/infer/src/clang/cTrans_models.mli index d4232a9c2..62a05b1df 100644 --- a/infer/src/clang/cTrans_models.mli +++ b/infer/src/clang/cTrans_models.mli @@ -29,6 +29,6 @@ val is_toll_free_bridging : Procname.t option -> bool val get_predefined_model_method_signature : string -> string -> (string -> string -> Procname.objc_method_kind -> Procname.t) -> - CFrontend_config.lang -> CMethod_signature.method_signature option + Config.clang_lang -> CMethod_signature.method_signature option val is_dispatch_function_name : string -> (string * int) option diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index c856d29e4..749322a8e 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/infer/src/eradicate/eradicateChecks.ml @@ -46,7 +46,7 @@ let get_field_annotation fn typ = let ia' = (* TODO (t4968422) eliminate not !Config.eradicate check by marking fields as nullified *) (* outside of Eradicate in some other way *) - if (Models.Inference.enabled || not !Config.eradicate) + if (Models.Inference.enabled || not Config.eradicate) && Models.Inference.field_is_marked fn then Annotations.mk_ia Annotations.Nullable ia else ia in diff --git a/infer/src/eradicate/models.ml b/infer/src/eradicate/models.ml index 0ad355299..ecf7c4384 100644 --- a/infer/src/eradicate/models.ml +++ b/infer/src/eradicate/models.ml @@ -21,7 +21,7 @@ let use_models = true module Inference = struct let enabled = false - let get_dir () = Filename.concat !Config.results_dir "eradicate" + let get_dir () = Filename.concat Config.results_dir "eradicate" let field_get_dir_fname fn = let fname = Ident.fieldname_to_string fn in diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 1e2bba5b2..3ebedfdb2 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -209,7 +209,7 @@ let create_dummy_harness_file harness_name = let write_harness_to_file harness_instrs harness_file = let harness_file = let harness_file_name = DB.source_file_to_string harness_file in - ref (create_outfile harness_file_name) in + create_outfile harness_file_name in let pp_harness fmt = IList.iter (fun instr -> Format.fprintf fmt "%a\n" (Sil.pp_instr pe_text) instr) harness_instrs in do_outf harness_file (fun outf -> diff --git a/infer/src/java/jAnnotation.ml b/infer/src/java/jAnnotation.ml index 98ac50217..dfd60fc24 100644 --- a/infer/src/java/jAnnotation.ml +++ b/infer/src/java/jAnnotation.ml @@ -17,7 +17,7 @@ let is_suppress_warnings_annotated = let matcher = lazy (let default_matcher = fun _ -> false in - match !Config.suppress_warnings_annotations with + match Config.suppress_warnings_annotations with | Some f -> (try let m = Inferconfig.SuppressWarningsMatcher.load_matcher f in diff --git a/infer/src/java/jClasspath.ml b/infer/src/java/jClasspath.ml index fca35f050..944073a1e 100644 --- a/infer/src/java/jClasspath.ml +++ b/infer/src/java/jClasspath.ml @@ -16,11 +16,6 @@ module L = Logging let models_specs_filenames = ref StringSet.empty -let javac_verbose_out = ref "" - -let set_verbose_out path = - javac_verbose_out := path - let models_jar = ref "" @@ -81,7 +76,7 @@ let java_source_file_from_path path = if Filename.is_relative path then failwith "Expect absolute path for java source files" else - match !Config.project_root with + match Config.project_root with | None -> DB.abs_source_file_from_path path | Some project_root -> DB.rel_source_file_from_abs_path project_root path @@ -161,7 +156,7 @@ let add_source_file path map = let load_sources_and_classes () = - let file_in = open_in !javac_verbose_out in + let file_in = open_in Config.javac_verbose_out in let class_filename_re = Str.regexp "\\[wrote RegularFileObject\\[\\(.*\\)\\]\\]" in diff --git a/infer/src/java/jClasspath.mli b/infer/src/java/jClasspath.mli index e1a73d12a..407beb2c8 100644 --- a/infer/src/java/jClasspath.mli +++ b/infer/src/java/jClasspath.mli @@ -25,8 +25,6 @@ val add_models : string -> unit (** Check if there is a model for the given procname *) val is_model : Procname.t -> bool -val set_verbose_out: string -> unit - (** create a source file from an absolute path. Source files are relative if the project root is specified and absolute otherwise *) val java_source_file_from_path : string -> DB.source_file diff --git a/infer/src/java/jConfig.ml b/infer/src/java/jConfig.ml index 23fb64e96..26380c04f 100644 --- a/infer/src/java/jConfig.ml +++ b/infer/src/java/jConfig.ml @@ -118,21 +118,11 @@ let class_code cl = "L"^cl let errors_db_file = "errors.db" let main_errors_file = "Java_frontend.errors" -let classpath : string option ref = ref None - -let class_source_map : string option ref = ref None - (** {2 Flags } *) (* the Sawja representation of the Java Bytecode will be printed *) let html_mode = ref false -(* debug information will be printed *) -let debug_mode = ref false - -(* The classes in the given jar file will be translated. No sources needed *) -let dependency_mode = ref false - (* The dynamic dispatch will be handled partially statically *) let static_dispatch = ref false @@ -142,9 +132,3 @@ let init_count = ref 0 let normalize_string s = let rexp = Str.regexp_string "$" in Str.global_replace rexp "_" s - -(* Translate the safety checks doen by the JVM *) -let translate_checks = ref false - -(* Generate harness for Android code *) -let create_harness = ref false diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index 959d3f816..bf57971fd 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -78,7 +78,7 @@ let add_cmethod never_null_matcher program icfg node cm is_static = let tenv = icfg.JContext.tenv in let cn, ms = JBasics.cms_split cm.Javalib.cm_class_method_signature in let is_clinit = JBasics.ms_equal ms JBasics.clinit_signature in - if !JTrans.no_static_final = false + if Config.no_static_final = false && is_clinit && not (JTransStaticField.has_static_final_fields node) then JUtils.log "\t\tskipping class initializer: %s@." (JBasics.ms_name ms) @@ -96,7 +96,7 @@ let add_cmethod never_null_matcher program icfg node cm is_static = | None -> assert false in let impl = JTrans.get_implementation cm in let instrs, meth_kind = - if is_clinit && not !JTrans.no_static_final then + if is_clinit && not Config.no_static_final then let instrs = JTransStaticField.static_field_init node cn (JBir.code impl) in (instrs, JContext.Init) else (JBir.code impl), JContext.Normal in @@ -126,7 +126,7 @@ let add_amethod program icfg am is_static = let path_of_cached_classname cn = - let root_path = Filename.concat !Config.results_dir "classnames" in + let root_path = Filename.concat Config.results_dir "classnames" in let package_path = IList.fold_left Filename.concat root_path (JBasics.cn_package cn) in Filename.concat package_path ((JBasics.cn_simple_name cn)^".java") diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index 9503f6083..ceb04d10e 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -14,73 +14,8 @@ open Javalib_pack module L = Logging -let arg_desc = - let options_to_keep = ["-results_dir"; "-project_root"] in - let desc = - (arg_desc_filter options_to_keep base_arg_desc) @ - [ - "-classpath", - Arg.String (fun classpath -> JConfig.classpath := Some classpath), - None, - "set the classpath" - ; - "-class_source_map", - Arg.String (fun filename -> JConfig.class_source_map := Some filename), - None, - "path to class -> source map in JSON format" - ; - "-models", - Arg.String (fun filename -> JClasspath.add_models filename), - Some "paths", - "set the path to the jar containing the models" - ; - "-debug", - Arg.Unit (fun () -> JConfig.debug_mode := true), - None, - "write extra translation information" - ; - "-dependencies", - Arg.Unit (fun _ -> JConfig.dependency_mode := true), - None, - "translate all the dependencies during the capture" - ; - "-no-static_final", - Arg.Unit (fun () -> JTrans.no_static_final := true), - None, - "no special treatment for static final fields" - ; - "-tracing", - Arg.Unit (fun () -> JConfig.translate_checks := true), - None, - "Translate JVM checks" - ; - "-harness", - Arg.Unit (fun () -> JConfig.create_harness := true), - None, - "Create Android lifecycle harness" - ; - "-verbose_out", - Arg.String (fun path -> JClasspath.set_verbose_out path), - None, - "Set the path to the javac verbose output" - ; - "-suppress_warnings_out", - Arg.String (fun s -> Config.suppress_warnings_annotations := Some s), - Some "Path", - "Path to list of collected @SuppressWarnings annotations" - ; - ] in - Arg.create_options_desc false "Parsing Options" desc - -let usage = - "Usage: InferJava -d compilation_dir -sources filename\n" - -let print_usage_exit () = - Arg.usage arg_desc usage; - exit(1) - let () = - Arg.parse "INFERJAVA_ARGS" arg_desc (fun _ -> ()) usage; + (match Config.models_file with Some file -> JClasspath.add_models file | None -> ()); if Config.analyze_models && !JClasspath.models_jar <> "" then failwith "Not expecting model file when analyzing the models"; if not Config.analyze_models && !JClasspath.models_jar = "" then @@ -88,10 +23,10 @@ let () = let register_perf_stats_report source_file = - let stats_dir = Filename.concat !Config.results_dir Config.frontend_stats_dir_name in + let stats_dir = Filename.concat Config.results_dir Config.frontend_stats_dir_name in let abbrev_source_file = DB.source_file_encoding source_file in let stats_file = Config.perf_stats_prefix ^ "_" ^ abbrev_source_file ^ ".json" in - DB.create_dir !Config.results_dir ; + DB.create_dir Config.results_dir ; DB.create_dir stats_dir ; PerfStats.register_report_at_exit (Filename.concat stats_dir stats_file) @@ -115,14 +50,12 @@ let store_icfg tenv cg cfg program = begin let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in - if !JConfig.create_harness then Harness.create_harness cfg cg tenv; + if Config.create_harness then Harness.create_harness cfg cg tenv; Preanal.doit ~f_translate_typ:(Some f_translate_typ) cfg cg tenv; Cg.store_to_file cg_file cg; Cfg.store_cfg_to_file cfg_file true cfg; - if !JConfig.debug_mode then + if Config.debug_mode then begin - Config.write_dotty := true; - Config.print_types := true; Dotty.print_icfg_dotty cfg []; Cg.save_call_graph_dotty None Specs.get_specs cg end @@ -224,7 +157,7 @@ let do_all_files classpath sources classes = translate_source_file basename (Some package, source_file) source_file) source_files) sources; - if !JConfig.dependency_mode then + if Config.dependency_mode then capture_libs never_null_matcher linereader program tenv; save_tenv tenv; JClasspath.cleanup program; diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 88c1550af..bbea0bb10 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -255,8 +255,6 @@ let update_init_loc cn ms loc_start = try ignore(JBasics.ClassMap.find cn !init_loc_map) with Not_found -> init_loc_map := (JBasics.ClassMap.add cn loc_start !init_loc_map) -let no_static_final = ref false - (** Creates a procedure description. *) let create_local_procdesc program linereader cfg tenv node m = let cn, ms = JBasics.cms_split (Javalib.get_class_method_signature m) in @@ -264,7 +262,7 @@ let create_local_procdesc program linereader cfg tenv node m = if JBasics.ms_equal ms JBasics.clinit_signature then JContext.Init else JContext.Normal in if not ( - !no_static_final = false && + Config.no_static_final = false && meth_kind = JContext.Init && not (JTransStaticField.has_static_final_fields node)) then @@ -394,7 +392,7 @@ let rec get_method_procdesc program cfg tenv cn ms kind = | Created status -> status let use_static_final_fields context = - (not !no_static_final) && (JContext.get_meth_kind context) <> JContext.Init + (not Config.no_static_final) && (JContext.get_meth_kind context) <> JContext.Init let builtin_new = Sil.Const (Sil.Cfun ModelBuiltins.__new) @@ -570,7 +568,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_ | I_Special -> false | _ -> true in match sil_obj_expr with - | Sil.Var _ when is_non_constructor_call && not !JConfig.translate_checks -> + | Sil.Var _ when is_non_constructor_call && not Config.report_runtime_exceptions -> let obj_typ_no_ptr = match sil_obj_type with | Sil.Tptr (typ, _) -> typ @@ -992,7 +990,8 @@ let rec instruction context pc instr : translation = Cg.add_edge cg caller_procname callee_procname; Instr call_node - | JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks && is_this expr -> + | JBir.Check (JBir.CheckNullPointer expr) + when Config.report_runtime_exceptions && is_this expr -> (* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *) let (instrs, sil_expr, _) = expression context pc expr in let this_not_null_node = @@ -1000,7 +999,7 @@ let rec instruction context pc instr : translation = (Cfg.Node.Stmt_node "this not null") (instrs @ [assume_not_null loc sil_expr]) in Instr this_not_null_node - | JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks -> + | JBir.Check (JBir.CheckNullPointer expr) when Config.report_runtime_exceptions -> let (instrs, sil_expr, _) = expression context pc expr in let not_null_node = let sil_not_null = Sil.BinOp (Sil.Ne, sil_expr, Sil.exp_null) in @@ -1028,8 +1027,8 @@ let rec instruction context pc instr : translation = create_node npe_kind npe_instrs in Prune (not_null_node, throw_npe_node) - | JBir.Check (JBir.CheckArrayBound (array_expr, index_expr)) when !JConfig.translate_checks -> - + | JBir.Check (JBir.CheckArrayBound (array_expr, index_expr)) + when Config.report_runtime_exceptions -> let instrs, _, sil_length_expr, sil_index_expr = let array_instrs, sil_array_expr, _ = expression context pc array_expr @@ -1084,7 +1083,7 @@ let rec instruction context pc instr : translation = Prune (in_bound_node, throw_out_of_bound_node) - | JBir.Check (JBir.CheckCast (expr, object_type)) when !JConfig.translate_checks -> + | JBir.Check (JBir.CheckCast (expr, object_type)) when Config.report_runtime_exceptions -> let sil_type = JTransType.expr_type context expr and instrs, sil_expr, _ = expression context pc expr and ret_id = Ident.create_fresh Ident.knormal diff --git a/infer/src/java/jTrans.mli b/infer/src/java/jTrans.mli index 76ecd7500..c564bd139 100644 --- a/infer/src/java/jTrans.mli +++ b/infer/src/java/jTrans.mli @@ -13,9 +13,6 @@ open! Utils open Javalib_pack open Sawja_pack -(** If active, disable special treatment of static final fields. *) -val no_static_final : bool ref - (** Data structure for storing the results of the translation of an instruction. *) type translation = | Skip diff --git a/infer/src/java/jUtils.ml b/infer/src/java/jUtils.ml index 53a277c65..d72dd56f1 100644 --- a/infer/src/java/jUtils.ml +++ b/infer/src/java/jUtils.ml @@ -12,7 +12,7 @@ open! Utils let rec log fmt = - if !JConfig.debug_mode then + if Config.debug_mode then Logging.stdout fmt else Obj.magic log diff --git a/infer/src/llvm/lConfig.ml b/infer/src/llvm/lConfig.ml deleted file mode 100644 index a89bdbc8f..000000000 --- a/infer/src/llvm/lConfig.ml +++ /dev/null @@ -1,16 +0,0 @@ -(* - * Copyright (c) 2015 - 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 - -(** arguments for InferLLVM *) - -let debug_mode = ref false - -let source_filename : string option ref = ref None diff --git a/infer/src/llvm/lConfig.mli b/infer/src/llvm/lConfig.mli deleted file mode 100644 index 1a8b3c1e5..000000000 --- a/infer/src/llvm/lConfig.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* - * Copyright (c) 2015 - 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 - -(** arguments for InferLLVM *) - -val debug_mode : bool ref - -val source_filename : string option ref diff --git a/infer/src/llvm/lMain.ml b/infer/src/llvm/lMain.ml index dbf9c158b..96fa4e1ca 100644 --- a/infer/src/llvm/lMain.ml +++ b/infer/src/llvm/lMain.ml @@ -9,41 +9,17 @@ open! Utils -let arg_desc = - let options_to_keep = ["-results_dir"; "-project_root"] in - let desc = - arg_desc_filter options_to_keep base_arg_desc @ - [ - "-c", - Arg.String (fun cfile -> LConfig.source_filename := Some cfile), - Some "cfile", - "C/C++ file being translated" - ; - "-debug", - Arg.Unit (fun _ -> LConfig.debug_mode := true), - None, - "Enables debug mode" - ; - ] in - Arg.create_options_desc false "Parsing Options" desc - -let usage = "Usage: InferLLVM -c [options]\n" - -let print_usage_exit () = - Arg.usage arg_desc usage; - exit(1) - let register_perf_stats_report source_file = - let stats_dir = Filename.concat !Config.results_dir Config.frontend_stats_dir_name in + let stats_dir = Filename.concat Config.results_dir Config.frontend_stats_dir_name in let abbrev_source_file = DB.source_file_encoding source_file in let stats_file = Config.perf_stats_prefix ^ "_" ^ abbrev_source_file ^ ".json" in - DB.create_dir !Config.results_dir ; + DB.create_dir Config.results_dir ; DB.create_dir stats_dir ; PerfStats.register_report_at_exit (Filename.concat stats_dir stats_file) let init_global_state source_filename = - Config.curr_language := Config.C_CPP; - begin match !Config.project_root with + Config.curr_language := Config.Clang; + begin match Config.project_root with | None -> DB.current_source := DB.abs_source_file_from_path source_filename | Some project_root -> DB.current_source := DB.rel_source_file_from_abs_path project_root @@ -62,10 +38,8 @@ let store_icfg tenv cg cfg = Preanal.doit cfg cg tenv; Cg.store_to_file cg_file cg; Cfg.store_cfg_to_file cfg_file true cfg; - if !LConfig.debug_mode then + if Config.debug_mode then begin - Config.write_dotty := true; - Config.print_types := true; Dotty.print_icfg_dotty cfg []; Cg.save_call_graph_dotty None Specs.get_specs cg end @@ -76,9 +50,8 @@ let store_tenv tenv = Tenv.store_to_file tenv_filename tenv let () = - Arg.parse "INFERLLVM_ARGS" arg_desc (fun _ -> ()) usage; - begin match !LConfig.source_filename with - | None -> print_usage_exit () + begin match Config.source_file with + | None -> Config.print_usage_exit () | Some source_filename -> init_global_state source_filename end; let lexbuf = Lexing.from_channel stdin in diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index f457561c4..336205238 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -130,7 +130,7 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) | None -> Sil.Tvoid | Some ret_tp -> trans_typ ret_tp in let (proc_attrs : ProcAttributes.t) = - { (ProcAttributes.default proc_name Config.C_CPP) with + { (ProcAttributes.default proc_name Config.Clang) with ProcAttributes.formals = IList.map (fun (tp, name) -> (Mangled.from_string name, trans_typ tp)) params; is_defined = true; (** is defined and not just declared *) diff --git a/infer/src/scripts/checkCopyright.ml b/infer/src/scripts/checkCopyright.ml index c4595346a..2a1cce033 100644 --- a/infer/src/scripts/checkCopyright.ml +++ b/infer/src/scripts/checkCopyright.ml @@ -277,6 +277,6 @@ let () = let to_check = ref [] in let add_file_to_check fname = to_check := fname :: !to_check in - Arg.parse "CHECKCOPYRIGHT_ARGS" (Arg.align speclist) add_file_to_check usage_msg; + Arg.parse (Arg.align speclist) add_file_to_check usage_msg; IList.iter check_copyright (IList.rev !to_check); exit 0