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