[quandary] fix widening bug

Summary:
The previous widening operator added stars to the *end* of paths that existed in `next` but not `prev`. This is not enough to ensure termination in the case where the trie is growing both deeper and wider at the same time.

The newly added test demonstrates this issue. In the code, there's an ever-growing path of the form `tmp.prev.next.prev.next...` that wasn't summarized by the previous widening operator. The new widening is much more aggressive: it replaces *any* node present in `next` but not `prev` with a `*` (rather than trying to tack a star onto the end). This fixes the issue.

This issue was causing divergence on tricky doubly-linked list code in prod.

Reviewed By: jeremydubreil

Differential Revision: D5665719

fbshipit-source-id: 1310a92

infer/src/checkers/accessTree.ml

@@ -92,11 +92,11 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct
     make_node base_trace (AccessMap.singleton access (make_normal_leaf trace))
 
   (** find all of the traces in the subtree and join them with [orig_trace] *)
-  let rec join_all_traces orig_trace = function
+  let rec join_all_traces ?(join_traces= TraceDomain.join) orig_trace = function
     | Subtree subtree
      -> let join_all_traces_ orig_trace tree =
           let node_join_traces _ (trace, node) trace_acc =
-            join_all_traces (TraceDomain.join trace_acc trace) node
+            join_all_traces (join_traces trace_acc trace) node
           in
           AccessMap.fold node_join_traces tree orig_trace
         in
@@ -276,21 +276,23 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct
     let f_ acc ap (trace, _) = f acc ap trace in
     fold f_
 
-  (* replace the normal leaves of [node] with starred leaves *)
+  (* try for a bit to reach a fixed point before widening aggressively *)
-  let rec node_add_stars (trace, tree as node) =
+  let joins_before_widen = 3
-    match tree with
-    | Subtree subtree
-     -> if AccessMap.is_empty subtree then make_starred_leaf trace
-        else
-          let subtree' = AccessMap.map node_add_stars subtree in
-          if phys_equal subtree' subtree then node else (trace, Subtree subtree')
-    | Star
-     -> node
 
   let widen ~prev ~next ~num_iters =
     if phys_equal prev next then prev
+    else if Int.( <= ) num_iters joins_before_widen then join prev next
     else
       let trace_widen prev next = TraceDomain.widen ~prev ~next ~num_iters in
+      (* turn [node] into a starred node by vacuuming up its sub-traces *)
+      let node_add_stars (trace, tree as node) =
+        match tree with
+        | Subtree _
+         -> let trace' = join_all_traces ~join_traces:trace_widen trace tree in
+            make_starred_leaf trace'
+        | Star
+         -> node
+      in
       let rec node_widen prev_node_opt next_node_opt =
         match (prev_node_opt, next_node_opt) with
         | Some prev_node, Some next_node

infer/src/unit/accessTreeTests.ml

@@ -337,7 +337,7 @@ let tests =
       let make_x_base_tree trace =
         Domain.BaseMap.singleton x_base (Domain.make_normal_leaf trace)
       in
-      let widen prev next = Domain.widen ~prev ~next ~num_iters:0 in
+      let widen prev next = Domain.widen ~prev ~next ~num_iters:4 in
       (* a bit light on the tests here, since widen is implemented as a simple wrapper of join *)
       (* widening traces works:
          x |-> ("x", empty) \/ x |-> ("y", empty) =
@@ -358,15 +358,13 @@ let tests =
       (* adding stars to a subtree works:
          x |-> ("y", empty) \/
          x |-> ("x" , f |-> ("f", g |-> ("g", empty))) =
-         x |-> (T , f |-> ("f", g |-> ("g", Star)))
+         x |-> (T , f |-> (T, * ))
       *)
-      let xFG_star_tree =
+      let xF_star_tree =
-        let g_subtree = Domain.make_starred_leaf xFG_trace in
+        Domain.AccessMap.singleton f (Domain.make_starred_leaf MockTraceDomain.top)
-        Domain.AccessMap.singleton g g_subtree |> Domain.make_node xF_trace
+        |> Domain.make_node MockTraceDomain.top |> Domain.BaseMap.singleton x_base
-        |> Domain.AccessMap.singleton f |> Domain.make_node MockTraceDomain.top
-        |> Domain.BaseMap.singleton x_base
       in
-      assert_trees_equal (widen x_tree_y_trace xFG_tree) xFG_star_tree ;
+      assert_trees_equal (widen x_tree_y_trace xFG_tree) xF_star_tree ;
       (* widening is not commutative, and is it not join:
          x |-> ("x" , f |-> ("f", g |-> ("g", empty))) \/
          x |-> ("y", empty) =

infer/tests/codetoanalyze/cpp/quandary/basics.cpp

@@ -178,4 +178,21 @@ void atomic_eq(std::atomic<std::chrono::duration<int, std::centi>> x,
   // crash
   x = y;
 }
+struct node {
+  struct node* prev;
+  struct node* next;
+};
+
+// we used to hang on this example before the widening operator was fixed
+void loop_ok() {
+  struct node* init;
+  struct node* tmp;
+
+  while (1) {
+    tmp->next = init;
+    init = tmp;
+    tmp->prev = init;
+  }
+}
+
 }