[domains] gating sanity checks in id -> access path domain

Summary:
These checks were useful when developing Quandary, but do not fire anymore.
`AccessPath.raw_equal` is implicated as one of the top time-consuming functions in Quandary, so gating the assertion that calls it needlessly might save us some time.

Also minor cleanup: made the error messages a bit clearer and added an mli.

Reviewed By: jeremydubreil

Differential Revision: D4323653

fbshipit-source-id: 2a723b5

infer/src/checkers/IdAccessPathMapDomain.ml

@@ -9,8 +9,6 @@
 
 open! IStd
 
-(** mapping of ids to raw access paths. useful for id-normalizing access paths *)
-
 module IdMap = Var.Map
 
 type astate = AccessPath.raw IdMap.t
@@ -31,11 +29,31 @@ let (<=) ~lhs ~rhs =
         (fun id lhs_ap ->
            let rhs_ap = IdMap.find id rhs in
            let eq = AccessPath.equal_raw lhs_ap rhs_ap in
-           assert eq;
+           if not eq && Config.debug_exceptions
+           then
+             failwithf "Id %a maps to both %a and %a@."
+               Var.pp id
+               AccessPath.pp_raw lhs_ap
+               AccessPath.pp_raw 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 *)
+      (* TODO: fix (13370224) *)
+      ()
+  | id ->
+      if not (AccessPath.equal_raw ap1 ap2)
+      then
+        failwithf "Id %a maps to both %a and %a@."
+          Var.pp id
+          AccessPath.pp_raw ap1
+          AccessPath.pp_raw ap2
+
 let join astate1 astate2 =
   if phys_equal astate1 astate2
   then astate1
@@ -43,16 +61,7 @@ let join astate1 astate2 =
     IdMap.merge
       (fun var ap1_opt ap2_opt -> match ap1_opt, ap2_opt with
          | Some ap1, Some ap2 ->
-             (* in principle, could do a join here if the access paths have the same root. but
+             if Config.debug_exceptions then check_invariant ap1 ap2 var;
-                they should always be equal if we are using the map correctly *)
-             let check_invariant () = match var with
-               | Var.ProgramVar pvar when Pvar.is_frontend_tmp pvar ->
-                   (* Sawja reuses temporary variables which sometimes breaks this invariant *)
-                   (* TODO: fix (13370224) *)
-                   ()
-               | _ ->
-                   assert (AccessPath.equal_raw ap1 ap2) in
-             check_invariant ();
              ap1_opt
          | Some _, None -> ap1_opt
          | None, Some _ -> ap2_opt

infer/src/checkers/IdAccessPathMapDomain.mli

@@ -0,0 +1,20 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! IStd
+
+(** mapping of ids to raw access paths. useful for id-normalizing access paths *)
+
+module IdMap = Var.Map
+
+type astate = AccessPath.raw IdMap.t
+
+include (module type of IdMap)
+
+include AbstractDomain.S with type astate := astate