From 2800c84972e78da7bb6b8e86dc8bc3cfd633f079 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 31 Jan 2017 12:31:55 -0800 Subject: [PATCH] [checkers] don't do expensive access path equality check unless debugging Reviewed By: jeremydubreil Differential Revision: D4489105 fbshipit-source-id: 545e281 --- infer/src/checkers/IdAccessPathMapDomain.ml | 33 ++++++++------------- 1 file changed, 12 insertions(+), 21 deletions(-) diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index 7d9098f23..133513c65 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -18,27 +18,6 @@ include IdMap let pp fmt astate = IdMap.pp ~pp_value:AccessPath.Raw.pp fmt astate -let (<=) ~lhs ~rhs = - if phys_equal lhs rhs - then true - else - try - IdMap.for_all - (fun id lhs_ap -> - let rhs_ap = IdMap.find id rhs in - let eq = AccessPath.Raw.equal lhs_ap rhs_ap in - if not eq && Config.debug_exceptions - then - failwithf "Id %a maps to both %a and %a@." - Var.pp id - AccessPath.Raw.pp lhs_ap - AccessPath.Raw.pp rhs_ap; - eq) - lhs - with Not_found -> false - -(* in principle, could do a join here if the access paths have the same root. but they should - always be equal if we are using the map correctly *) let check_invariant ap1 ap2 = function | Var.ProgramVar pvar when Pvar.is_frontend_tmp pvar -> (* Sawja reuses temporary variables which sometimes breaks this invariant *) @@ -52,6 +31,18 @@ let check_invariant ap1 ap2 = function AccessPath.Raw.pp ap1 AccessPath.Raw.pp ap2 +let (<=) ~lhs ~rhs = + if phys_equal lhs rhs + then true + else + IdMap.for_all + (fun id lhs_ap -> + let rhs_has = IdMap.mem id rhs in + if rhs_has && Config.debug_exceptions + then check_invariant lhs_ap (IdMap.find id rhs) id; + rhs_has) + lhs + let join astate1 astate2 = if phys_equal astate1 astate2 then astate1