From 706acdfd9e9631537760600872e3106b53aa2c5c Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 26 Jul 2016 10:44:28 -0700 Subject: [PATCH] generalizing get_trace to get_node Reviewed By: mbouaziz Differential Revision: D3614509 fbshipit-source-id: b1dc5dd --- infer/src/checkers/accessTree.ml | 33 +++++++++++++++++------------- infer/src/unit/accessTreeTests.ml | 34 ++++++++++++++++++++++++++++--- 2 files changed, 50 insertions(+), 17 deletions(-) diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index a21c6a772..a9aaac762 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -76,9 +76,9 @@ module Make (TraceDomain : AbstractDomain.S) = struct | Star -> orig_trace - (** retrieve the trace associated with [ap] from [tree] *) - let get_trace ap tree = - let rec accesses_get_trace access_list trace tree = + (** retrieve the trace and subtree associated with [ap] from [tree] *) + let get_node ap tree = + let rec accesses_get_node access_list trace tree = match access_list, tree with | _, Star -> trace, Star @@ -86,22 +86,26 @@ module Make (TraceDomain : AbstractDomain.S) = struct trace, tree | access :: accesses, Subtree subtree -> let access_trace, access_subtree = AccessMap.find access subtree in - accesses_get_trace accesses access_trace access_subtree in - let get_trace_ base accesses tree = + accesses_get_node accesses access_trace access_subtree in + let get_node_ base accesses tree = let base_trace, base_tree = BaseMap.find base tree in - accesses_get_trace accesses base_trace base_tree in + accesses_get_node accesses base_trace base_tree in let base, accesses = AccessPath.extract ap in - match get_trace_ base accesses tree with + match get_node_ base accesses tree with | trace, subtree -> if AccessPath.is_exact ap - then Some trace + then Some (trace, subtree) else (* input query was [ap]*, and [trace] is the trace associated with [ap]. get the traces associated with the children of [ap] in [tree] and join them with [trace] *) - Some (join_all_traces trace subtree) + Some (join_all_traces trace subtree, subtree) | exception Not_found -> None + (** retrieve the trace associated with [ap] from [tree] *) + let get_trace ap tree = + Option.map fst (get_node ap tree) + (* helper for [add_access]. [last_trace] is the trace associated with [tree] in the parent. *) let rec access_tree_add_trace ~last_trace ~seen_array_access ~is_exact trace access_list tree = match access_list, tree with @@ -272,11 +276,12 @@ module Make (TraceDomain : AbstractDomain.S) = struct prev_node_opt in BaseMap.merge (fun _ prev_node next_node -> node_widen prev_node next_node) prev next + let rec pp_node fmt (trace, subtree) = + let pp_subtree fmt = function + | Subtree access_map -> AccessMap.pp ~pp_value:pp_node fmt access_map + | Star -> F.fprintf fmt "*" in + F.fprintf fmt "(%a, %a)" TraceDomain.pp trace pp_subtree subtree + let pp fmt base_tree = - let rec pp_node fmt (trace, subtree) = - let pp_subtree fmt = function - | Subtree access_map -> AccessMap.pp ~pp_value:pp_node fmt access_map - | Star -> F.fprintf fmt "*" in - F.fprintf fmt "(%a, %a)" TraceDomain.pp trace pp_subtree subtree in BaseMap.pp ~pp_value:pp_node fmt base_tree end diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index cb01231b7..91154c1ca 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -104,12 +104,12 @@ let tests = let array_f_trace = MockTraceDomain.singleton "arrayF" in let x_star_trace = MockTraceDomain.of_list ["x"; "xF"; "xFG"] in + let g_subtree = Domain.make_access_node xF_trace g xFG_trace in let x_subtree = - let g_subtree = Domain.make_access_node xF_trace g xFG_trace in Domain.AccessMap.singleton f g_subtree |> Domain.make_node x_trace in + let yF_subtree = Domain.make_starred_leaf yF_trace in let y_subtree = - let yF_subtree = Domain.make_starred_leaf yF_trace in Domain.AccessMap.singleton f yF_subtree |> Domain.make_node y_trace in let z_subtree = Domain.make_starred_leaf z_trace in @@ -146,6 +146,18 @@ let tests = let assert_trace_not_found access_path tree = assert_traces_eq access_path tree no_trace in + let assert_node_equal access_path tree expected_node = + match Domain.get_node access_path tree with + | Some actual_node -> + let pp_diff fmt (actual, expected) = + F.fprintf + fmt + "Expected to retrieve node %a but got %a" + Domain.pp_node expected + Domain.pp_node actual in + assert_equal ~pp_diff expected_node actual_node + | None -> assert false in + let get_trace_test = let get_trace_test_ _ = (* exact access path tests *) @@ -168,7 +180,23 @@ let tests = assert_traces_eq y_star tree "{ y, yF }"; assert_traces_eq yF_star tree "{ yF }"; assert_traces_eq yFG tree "{ yF }"; - assert_trace_not_found yG tree in + assert_trace_not_found yG tree; + + (* get_trace is just (fst get_node), so light tests here *) + (* exact access path tests *) + assert_node_equal z tree z_subtree; + assert_node_equal xF tree g_subtree; + assert_node_equal xFG tree (Domain.make_normal_leaf xFG_trace); + + (* starred tree tests *) + assert_node_equal yFG tree yF_subtree; + + (* starred access path tests *) + let joined_y_subtree = + Domain.AccessMap.singleton f yF_subtree + |> Domain.make_node (MockTraceDomain.join y_trace yF_trace) in + assert_node_equal y_star tree joined_y_subtree in + "get_trace">::get_trace_test_ in let add_trace_test =