[absint] add widening threshold to crash hard in the face of likely divergence

Reviewed By: jeremydubreil

Differential Revision: D5519258

fbshipit-source-id: 8883f49

infer/src/absint/AbstractInterpreter.ml

@@ -96,7 +96,13 @@ struct
         else astate_pre
       in
       if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.pre then (inv_map, work_queue)
-      else update_inv_map widened_pre (old_state.visit_count + 1)
+      else
+        let visit_count' = old_state.visit_count + 1 in
+        if visit_count' > Config.max_widens then
+          failwithf
+            "Exceeded max widening threshold %d while analyzing %a. Please check your widening operator or increase the threshold"
+            Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ;
+        update_inv_map widened_pre visit_count'
     else
       (* first time visiting this node *)
       let visit_count = 1 in

infer/src/base/Config.ml

@@ -189,6 +189,11 @@ let manual_threadsafety = "THREADSAFETY CHECKER OPTIONS"
 (** Maximum level of recursion during the analysis, after which a timeout is generated *)
 let max_recursion = 5
 
+(** Maximum number of widens that can be performed before the analysis will intentionally crash.
+    Used to guard against divergence in the case that someone has implemented a bad widening
+    operator *)
+let max_widens = 10000
+
 (** Flag to tune the level of applying the meet operator for
     preconditions during the footprint analysis:
     0 = do not use the meet

infer/src/base/Config.mli

@@ -153,6 +153,8 @@ val log_dir_name : string
 
 val max_recursion : int
 
+val max_widens : int
+
 val meet_level : int
 
 val models_dir : string