From 8fde27014aee9ac5b43e165a3bd0599ecdecc469 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Fri, 28 Jul 2017 15:24:15 -0700
Subject: [PATCH] [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 | 8 +++++++-
 infer/src/base/Config.ml                | 5 +++++
 infer/src/base/Config.mli               | 2 ++
 3 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml
index 941ed7103..255fc1acf 100644
--- a/infer/src/absint/AbstractInterpreter.ml
+++ b/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
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index 511abf24c..f4bf9ce86 100644
--- a/infer/src/base/Config.ml
+++ b/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
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 4a8f350b8..c166fea49 100644
--- a/infer/src/base/Config.mli
+++ b/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