Disable timeouts during model analysis

Reviewed By: sblackshear, cristianoc

Differential Revision: D4317600

fbshipit-source-id: 815c462

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 ();

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

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

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 *)
+      (* disable timeouts when analyzing models *)
-      long_symops_timeout, long_seconds_timeout
+      (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 = None then symops_per_iteration := symops_timeout ;
-  if !symops_per_iteration = 0 then symops_per_iteration := symops_timeout ;
+  if !seconds_per_iteration = None then seconds_per_iteration := seconds_timeout ;
 
   match !analyzer with
   | Some Checkers -> checkers := true

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

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 &&
+  (match !timeout_symops with
-     !gs.alarm_active
+   | Some symops when !gs.symop_count > symops && !gs.alarm_active ->
-  then raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count));
+       raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count))
+   | _ -> ()
+  );
   check_wallclock_alarm ()
 
 (** Reset the counter *)

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

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(...)]