From 423b732cb4e184c47b59449fa6512e83d71616ba Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Mon, 29 Oct 2018 05:13:59 -0700
Subject: [PATCH] [inferbo] Fix condition of narrowing termination

Summary:
It terminates narrowing when new and old states are not comparable.
Since current narrowing does not use meet operations guaranteeing
termination of narrowing, it tries to terminate narrowing more
conservatively.

Reviewed By: mbouaziz

Differential Revision: D12815419

fbshipit-source-id: e8b45199e
---
 infer/src/absint/AbstractInterpreter.ml            |  5 +++++
 .../tests/codetoanalyze/c/bufferoverrun/issues.exp |  1 +
 .../codetoanalyze/c/bufferoverrun/while_loop.c     | 14 ++++++++++++++
 3 files changed, 20 insertions(+)

diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml
index 81009fb99..f84d04a2d 100644
--- a/infer/src/absint/AbstractInterpreter.ml
+++ b/infer/src/absint/AbstractInterpreter.ml
@@ -204,6 +204,11 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
           || Domain.( <= ) ~lhs:old_state.State.pre ~rhs:new_pre
         else Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre
       then (inv_map, ReachedFixPoint)
+      else if is_narrowing && not (Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre) then (
+        L.(debug Analysis Verbose)
+          "Terminate narrowing because old and new states are not comparable at %a:%a@."
+          Typ.Procname.pp (Procdesc.get_proc_name pdesc) Node.pp_id node_id ;
+        (inv_map, ReachedFixPoint) )
       else
         let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in
         update_inv_map new_pre ~visit_count:visit_count'
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
index 439d90f4a..e3e56c06f 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
@@ -186,4 +186,5 @@ codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_with_else_bad
 codetoanalyze/c/bufferoverrun/unreachable.c, infinite_loop_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/unreachable.c, never_loops_bad, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/unreachable.c, unreachable_statement_exit_bad, 1, UNREACHABLE_CODE, no_bucket, ERROR, []
+codetoanalyze/c/bufferoverrun/while_loop.c, diverge_on_narrowing, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c
index 8dd76f5a0..ae5a98443 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c
@@ -13,3 +13,17 @@ void while_loop() {
   while (*(a + i) && i < 10) /* BUG */
     a[i++] = 1; /* SAFE */
 }
+
+struct S {
+  struct S* f;
+};
+
+void dummy_func(struct S* x) {}
+
+void diverge_on_narrowing() {
+  struct S* x;
+  while (1) {
+    dummy_func(0);
+    x = x->f;
+  }
+}