From 3e2fa59262eca836807c884fcb12f1fa67acbe21 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 11 May 2016 08:47:39 -0700 Subject: [PATCH] Reimplement command line options Summary: Reimplement command line options in preparation for uniformly passing options from the top-level infer driver that invokes a build command through the build system to the descendant infer processes. All command line options of all executables are collected into Config, and declared using a new CommandLineOption module that supports maintining backward compatibility with the current command line interface. Very few values representing command line options are mutable now, as they are set once during parsing but are constant thereafter. All ordering dependencies are contained within the implementation of Config, and the implementation of Config is careful to avoid unintended interactions and ordering dependencies between options. Reviewed By: jvillard Differential Revision: D3273345 fbshipit-source-id: 8e8c6fa --- infer/src/IR/cfg.ml | 8 +- infer/src/IR/procname.ml | 6 +- infer/src/IR/sil.ml | 20 +- infer/src/backend/CommandLineOption.ml | 378 ++++++++ infer/src/backend/CommandLineOption.mli | 96 ++ infer/src/backend/DB.ml | 12 +- infer/src/backend/SymOp.ml | 4 +- infer/src/backend/abs.ml | 14 +- infer/src/backend/absarray.ml | 19 +- infer/src/backend/buckets.ml | 8 +- infer/src/backend/callbacks.ml | 2 +- infer/src/backend/clusterMakefile.ml | 8 +- infer/src/backend/config.ml | 1171 +++++++++++++++++------ infer/src/backend/config.mli | 222 +++++ infer/src/backend/dom.ml | 24 +- infer/src/backend/dotty.ml | 7 +- infer/src/backend/errdesc.ml | 132 +-- infer/src/backend/errlog.ml | 8 +- infer/src/backend/exceptions.ml | 4 +- infer/src/backend/inferanalyze.ml | 276 +----- infer/src/backend/inferconfig.ml | 8 +- infer/src/backend/inferprint.ml | 328 ++----- infer/src/backend/interproc.ml | 50 +- infer/src/backend/localise.ml | 2 +- infer/src/backend/logging.ml | 14 +- infer/src/backend/match.ml | 4 +- infer/src/backend/mergeCapture.ml | 8 +- infer/src/backend/mleak_buckets.ml | 118 +-- infer/src/backend/mleak_buckets.mli | 8 +- infer/src/backend/modelBuiltins.ml | 12 +- infer/src/backend/printer.ml | 30 +- infer/src/backend/prop.ml | 6 +- infer/src/backend/propgraph.ml | 2 +- infer/src/backend/prover.ml | 19 +- infer/src/backend/rearrange.ml | 59 +- infer/src/backend/specs.ml | 6 +- infer/src/backend/symExec.ml | 32 +- infer/src/backend/tabulation.ml | 16 +- infer/src/backend/taint.ml | 8 +- infer/src/backend/utils.ml | 285 +----- infer/src/backend/utils.mli | 63 +- infer/src/backend/zipLib.ml | 14 +- infer/src/checkers/codeQuery.ml | 3 +- infer/src/checkers/codeQuery.mli | 2 - infer/src/checkers/registerCheckers.ml | 8 +- infer/src/clang/cArithmetic_trans.ml | 4 +- infer/src/clang/cFrontend.ml | 12 +- infer/src/clang/cFrontend_config.ml | 40 - infer/src/clang/cFrontend_config.mli | 30 - infer/src/clang/cFrontend_decl.ml | 4 +- infer/src/clang/cFrontend_utils.ml | 26 +- infer/src/clang/cFrontend_utils.mli | 4 +- infer/src/clang/cLocation.ml | 12 +- infer/src/clang/cMain.ml | 105 +- infer/src/clang/cMethod_signature.ml | 2 +- infer/src/clang/cMethod_signature.mli | 4 +- infer/src/clang/cMethod_trans.ml | 26 +- infer/src/clang/cTrans.ml | 8 +- infer/src/clang/cTrans_models.mli | 2 +- infer/src/eradicate/eradicateChecks.ml | 2 +- infer/src/eradicate/models.ml | 2 +- infer/src/harness/inhabit.ml | 2 +- infer/src/java/jAnnotation.ml | 2 +- infer/src/java/jClasspath.ml | 9 +- infer/src/java/jClasspath.mli | 2 - infer/src/java/jConfig.ml | 16 - infer/src/java/jFrontend.ml | 6 +- infer/src/java/jMain.ml | 79 +- infer/src/java/jTrans.ml | 19 +- infer/src/java/jTrans.mli | 3 - infer/src/java/jUtils.ml | 2 +- infer/src/llvm/lConfig.ml | 16 - infer/src/llvm/lConfig.mli | 16 - infer/src/llvm/lMain.ml | 41 +- infer/src/llvm/lTrans.ml | 2 +- infer/src/scripts/checkCopyright.ml | 2 +- 76 files changed, 2097 insertions(+), 1927 deletions(-) create mode 100644 infer/src/backend/CommandLineOption.ml create mode 100644 infer/src/backend/CommandLineOption.mli create mode 100644 infer/src/backend/config.mli delete mode 100644 infer/src/llvm/lConfig.ml delete mode 100644 infer/src/llvm/lConfig.mli 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