[pulse] Fixed a bug in AbductiveDomain.leq operator. (#1424)

Summary:
the mapping for computing 'leq' relation in isomorphic graphs was sometimes mixed with opposite mappings due to typos in the code.

Please see [CONTRIBUTING.md](./CONTRIBUTING.md) for how to set up your development environment and run tests.

Pull Request resolved: https://github.com/facebook/infer/pull/1424

Reviewed By: ngorogiannis

Differential Revision: D28118324

Pulled By: jvillard

fbshipit-source-id: 56e813bd1

infer/src/pulse/PulseAbductiveDomain.ml

@@ -112,8 +112,8 @@ let leq ~lhs ~rhs =
      &&
      match
        BaseDomain.isograph_map BaseDomain.empty_mapping
-         ~lhs:(rhs.pre :> BaseDomain.t)
+         ~lhs:(lhs.pre :> BaseDomain.t)
-         ~rhs:(lhs.pre :> BaseDomain.t)
+         ~rhs:(rhs.pre :> BaseDomain.t)
      with
      | NotIsomorphic ->
          false

infer/src/pulse/PulseBaseDomain.ml

@@ -125,7 +125,7 @@ module GraphComparison = struct
             IsomorphicUpTo mapping
         | Some _, None | None, Some _ ->
             NotIsomorphic
-        | Some (edges_rhs, attrs_rhs), Some (edges_lhs, attrs_lhs) ->
+        | Some (edges_lhs, attrs_lhs), Some (edges_rhs, attrs_rhs) ->
             (* continue the comparison recursively on all edges and attributes *)
             if Attributes.equal attrs_rhs attrs_lhs then
               let bindings_lhs = Memory.Edges.bindings edges_lhs in