diff --git a/infer/src/backend/timeout.ml b/infer/src/backend/timeout.ml index 6cae7c8ac..007360d9b 100644 --- a/infer/src/backend/timeout.ml +++ b/infer/src/backend/timeout.ml @@ -114,7 +114,7 @@ let resume_previous_timeout () = let exe_timeout f x = let suspend_existing_timeout_and_start_new_one () = suspend_existing_timeout ~keep_symop_total:true; - set_alarm (SymOp.get_timeout_seconds ()); + Option.iter (SymOp.get_timeout_seconds ()) ~f:set_alarm; SymOp.set_alarm () in try suspend_existing_timeout_and_start_new_one (); diff --git a/infer/src/base/CommandLineOption.ml b/infer/src/base/CommandLineOption.ml index c014f855c..e28212c8d 100644 --- a/infer/src/base/CommandLineOption.ml +++ b/infer/src/base/CommandLineOption.ml @@ -317,6 +317,11 @@ let mk_int ~default ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = ~decode_json:(string_json_decoder ~long) ~mk_spec:(fun set -> Arg.String set) +let mk_int_opt ?default ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = + let default_to_string = function Some f -> string_of_int f | None -> "" in + let f s = Some (int_of_string s) in + mk_option ~deprecated ~long ?short ~default ~default_to_string ~f ?exes ~meta doc + let mk_float ~default ?(deprecated=[]) ~long ?short ?exes ?(meta="") doc = mk ~deprecated ~long ?short ~default ?exes ~meta doc ~default_to_string:string_of_float diff --git a/infer/src/base/CommandLineOption.mli b/infer/src/base/CommandLineOption.mli index af623ba04..462655e9d 100644 --- a/infer/src/base/CommandLineOption.mli +++ b/infer/src/base/CommandLineOption.mli @@ -64,6 +64,8 @@ val mk_bool_group : val mk_int : default:int -> int ref t +val mk_int_opt : ?default:int -> int option ref t + val mk_float : default:float -> float ref t val mk_float_opt : ?default:float -> float option ref t diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 3598174bf..1fa4916fe 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1045,7 +1045,7 @@ and save_results = ~meta:"file.iar" "Save analysis results to Infer Analysis Results file file.iar" and seconds_per_iteration = - CLOpt.mk_float ~deprecated:["seconds_per_iteration"] ~long:"seconds-per-iteration" ~default:0. + CLOpt.mk_float_opt ~deprecated:["seconds_per_iteration"] ~long:"seconds-per-iteration" ~meta:"float" "Set the number of seconds per iteration (see --iterations)" and skip_analysis_in_path = @@ -1135,7 +1135,7 @@ and svg = "Generate .dot and .svg files from specs" and symops_per_iteration = - CLOpt.mk_int ~deprecated:["symops_per_iteration"] ~long:"symops-per-iteration" ~default:0 + CLOpt.mk_int_opt ~deprecated:["symops_per_iteration"] ~long:"symops-per-iteration" ~meta:"int" "Set the number of symbolic operations per iteration (see --iterations)" and test_filtering = @@ -1295,16 +1295,14 @@ let post_parsing_initialization () = 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 !models_mode then - (* use longer timeouts when analyzing models *) - long_symops_timeout, long_seconds_timeout + (* disable timeouts when analyzing models *) + (None, None) else - default_symops_timeout, default_seconds_timeout + (Some default_symops_timeout, Some 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 ; + if !symops_per_iteration = None then symops_per_iteration := symops_timeout ; + if !seconds_per_iteration = None then seconds_per_iteration := seconds_timeout ; match !analyzer with | Some Checkers -> checkers := true diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 8a959eb4f..c27837724 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -238,7 +238,7 @@ 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 seconds_per_iteration : float option val show_buckets : bool val show_progress_bar : bool val skip_analysis_in_path : string list @@ -252,7 +252,7 @@ val stats_mode : bool val subtype_multirange : bool val suppress_warnings_out : string option val svg : bool -val symops_per_iteration : int +val symops_per_iteration : int option val test : bool val test_filtering : bool val testing_mode : bool diff --git a/infer/src/base/SymOp.ml b/infer/src/base/SymOp.ml index 695f25bc4..02ba49ccd 100644 --- a/infer/src/base/SymOp.ml +++ b/infer/src/base/SymOp.ml @@ -58,10 +58,14 @@ 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 + (Option.map Config.seconds_per_iteration + ~f:(fun sec -> sec *. (float_of_int Config.iterations))) (** Timeout in SymOps *) -let timeout_symops = ref (Config.symops_per_iteration * Config.iterations) +let timeout_symops = + ref (Option.map Config.symops_per_iteration ~f:(fun symops -> symops * Config.iterations)) let get_timeout_seconds () = !timeout_seconds @@ -155,9 +159,11 @@ let reset_total () = let pay () = !gs.symop_count <- !gs.symop_count + 1; !gs.symop_total := !(!gs.symop_total) + 1; - if !gs.symop_count > !timeout_symops && - !gs.alarm_active - then raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count)); + (match !timeout_symops with + | Some symops when !gs.symop_count > symops && !gs.alarm_active -> + raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count)) + | _ -> () + ); check_wallclock_alarm () (** Reset the counter *) diff --git a/infer/src/base/SymOp.mli b/infer/src/base/SymOp.mli index 4c31011a0..5caa41502 100644 --- a/infer/src/base/SymOp.mli +++ b/infer/src/base/SymOp.mli @@ -22,7 +22,7 @@ val check_wallclock_alarm : unit -> unit val get_remaining_wallclock_time : unit -> float (** Timeout in seconds for each function *) -val get_timeout_seconds : unit -> float +val get_timeout_seconds : unit -> float option (** Return the total number of symop's since the beginning *) val get_total : unit -> int diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 1b09959cd..ee2670a41 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -142,8 +142,6 @@ codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getTwoIntegers codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getTwoIntegersWithOneCheck(Integer,Integer), 11, RETURN_VALUE_IGNORED, [start of procedure getTwoIntegersWithOneCheck(...),Taking true branch,Taking true branch] codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.putIntegerTwiceThenGetTwice(HashMap), 6, RETURN_VALUE_IGNORED, [start of procedure putIntegerTwiceThenGetTwice(...)] codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.putIntegerTwiceThenGetTwice(HashMap), 7, RETURN_VALUE_IGNORED, [start of procedure putIntegerTwiceThenGetTwice(...)] -codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.putIntegerTwiceThenGetTwice(HashMap), 12, RETURN_VALUE_IGNORED, [start of procedure putIntegerTwiceThenGetTwice(...)] -codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.putIntegerTwiceThenGetTwice(HashMap), 13, RETURN_VALUE_IGNORED, [start of procedure putIntegerTwiceThenGetTwice(...)] codetoanalyze/java/infer/IntegerExample.java, void IntegerExample.testIntegerEqualsBad(), 6, NULL_DEREFERENCE, [start of procedure testIntegerEqualsBad(),Taking true branch] codetoanalyze/java/infer/InvokeDynamic.java, int InvokeDynamic.lambda$npeInLambdaBad$1(String,String), 1, NULL_DEREFERENCE, [start of procedure lambda$npeInLambdaBad$1(...)] codetoanalyze/java/infer/InvokeDynamic.java, void InvokeDynamic.invokeDynamicThenNpeBad(List), 5, NULL_DEREFERENCE, [start of procedure invokeDynamicThenNpeBad(...)]