diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 8762c98c8..d9afe6751 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -101,4 +101,35 @@ module Make (TraceDomain : AbstractDomain.S) = struct Some (join_all_traces trace subtree) | exception Not_found -> None + + let rec access_tree_lteq ((lhs_trace, lhs_tree) as lhs) ((rhs_trace, rhs_tree) as rhs) = + if lhs == rhs + then true + else + TraceDomain.(<=) ~lhs:lhs_trace ~rhs:rhs_trace && + match lhs_tree, rhs_tree with + | Subtree lhs_subtree, Subtree rhs_subtree -> + AccessMap.for_all + (fun k lhs_v -> + try + let rhs_v = AccessMap.find k rhs_subtree in + access_tree_lteq lhs_v rhs_v + with Not_found -> false) + lhs_subtree + | _, Star -> + true + | Star, Subtree _ -> + false + + let (<=) ~lhs ~rhs = + if lhs == rhs + then true + else + BaseMap.for_all + (fun k lhs_v -> + try + let rhs_v = BaseMap.find k rhs in + access_tree_lteq lhs_v rhs_v + with Not_found -> false) + lhs end diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 505989a44..49bf17bbb 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -131,4 +131,58 @@ let tests = assert_traces_eq yFG tree "{ yF }"; assert_trace_not_found yG tree in "get_trace">::get_trace_test_ in - "access_tree_suite">:::[get_trace_test] + + let lteq_test = + let lteq_test_ _ = + let x_base_tree = Domain.BaseMap.singleton x_base Domain.empty_node in + let y_base_tree = Domain.BaseMap.singleton y_base Domain.empty_node in + let x_y_base_tree = Domain.BaseMap.add y_base Domain.empty_node x_base_tree in + let xFG_tree = Domain.BaseMap.singleton x_base x_tree in + + let x_star_tree = Domain.BaseMap.singleton x_base (Domain.make_starred_leaf x_trace) in + let yF_star_tree = Domain.BaseMap.singleton y_base y_tree in + + (* regular tree tests *) + assert_bool "<= equal;" (Domain.(<=) ~lhs:tree ~rhs:tree); + assert_bool "<= bases" (Domain.(<=) ~lhs:x_base_tree ~rhs:x_y_base_tree); + assert_bool "<= regular1" (Domain.(<=) ~lhs:x_base_tree ~rhs:xFG_tree); + assert_bool "<= regular2" (Domain.(<=) ~lhs:xFG_tree ~rhs:tree); + assert_bool "<= regular3" (Domain.(<=) ~lhs:y_base_tree ~rhs:tree); + assert_bool "<= bases negative1" (not (Domain.(<=) ~lhs:x_y_base_tree ~rhs:x_base_tree)); + assert_bool "<= bases negative2" (not (Domain.(<=) ~lhs:x_base_tree ~rhs:y_base_tree)); + assert_bool "<= negative1" (not (Domain.(<=) ~lhs:xFG_tree ~rhs:y_base_tree)); + assert_bool "<= negative2" (not (Domain.(<=) ~lhs:tree ~rhs:xFG_tree)); + + (* star tree tests *) + assert_bool "<= star lhs equal" (Domain.(<=) ~lhs:x_star_tree ~rhs:x_star_tree); + assert_bool "<= star rhs1" (Domain.(<=) ~lhs:x_base_tree ~rhs:x_star_tree); + assert_bool "<= star rhs2" (Domain.(<=) ~lhs:xFG_tree ~rhs:x_star_tree); + assert_bool "<= star rhs3" (Domain.(<=) ~lhs:y_base_tree ~rhs:yF_star_tree); + assert_bool "<= star rhs4" (Domain.(<=) ~lhs:yF_star_tree ~rhs:tree); + assert_bool "<= star lhs negative1" (not (Domain.(<=) ~lhs:x_star_tree ~rhs:x_base_tree)); + assert_bool "<= star lhs negative2" (not (Domain.(<=) ~lhs:x_star_tree ~rhs:xFG_tree)); + assert_bool "<= star lhs negative3" (not (Domain.(<=) ~lhs:yF_star_tree ~rhs:y_base_tree)); + assert_bool "<= star lhs negative4" (not (Domain.(<=) ~lhs:tree ~rhs:yF_star_tree)); + + (* <= tree but not <= trace tests *) + (* same as x_base_tree, but with a trace higher in the traces lattice *) + let x_base_tree_higher_trace = + Domain.BaseMap.singleton x_base (Domain.make_normal_leaf y_trace) in + (* same as x_star_tree, but with a trace incomparable in the traces lattice *) + let x_star_tree_diff_trace = + Domain.BaseMap.singleton x_base (Domain.make_starred_leaf y_trace) in + assert_bool + "(x, {}) <= (x, {y})" + (Domain.(<=) ~lhs:x_base_tree ~rhs:x_base_tree_higher_trace); + assert_bool + "(x, {y}) not <= (x, {})" + (not (Domain.(<=) ~lhs:x_base_tree_higher_trace ~rhs:x_base_tree)); + assert_bool + "(x*, {y})* not <= (x*, {x})" + (not (Domain.(<=) ~lhs:x_star_tree_diff_trace ~rhs:x_star_tree)); + assert_bool + "(x*, {x})* not <= (x*, {y})" + (not (Domain.(<=) ~lhs:x_star_tree ~rhs:x_star_tree_diff_trace)) in + "lteq">::lteq_test_ in + + "access_tree_suite">:::[get_trace_test; lteq_test]