From 3e6e76a2b2da1cd2b07b35ebc5a74b84b0f70778 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 22 Aug 2017 10:04:07 -0700 Subject: [PATCH] [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 | 26 ++++++++++--------- infer/src/unit/accessTreeTests.ml | 14 +++++----- .../codetoanalyze/cpp/quandary/basics.cpp | 17 ++++++++++++ 3 files changed, 37 insertions(+), 20 deletions(-) diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 8a66d79a7..99c8d8a24 100644 --- a/infer/src/checkers/accessTree.ml +++ b/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 *) - let rec node_add_stars (trace, tree as node) = - 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 + (* try for a bit to reach a fixed point before widening aggressively *) + let joins_before_widen = 3 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 diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 7caec3ae8..322f6f088 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/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 g_subtree = Domain.make_starred_leaf xFG_trace in - Domain.AccessMap.singleton g g_subtree |> Domain.make_node xF_trace - |> Domain.AccessMap.singleton f |> Domain.make_node MockTraceDomain.top - |> Domain.BaseMap.singleton x_base + let xF_star_tree = + Domain.AccessMap.singleton f (Domain.make_starred_leaf MockTraceDomain.top) + |> 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) = diff --git a/infer/tests/codetoanalyze/cpp/quandary/basics.cpp b/infer/tests/codetoanalyze/cpp/quandary/basics.cpp index 7dd6f2380..5e91b61d3 100644 --- a/infer/tests/codetoanalyze/cpp/quandary/basics.cpp +++ b/infer/tests/codetoanalyze/cpp/quandary/basics.cpp @@ -178,4 +178,21 @@ void atomic_eq(std::atomic> 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; + } +} + }