[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

@@ -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'

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]

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;
+  }
+}