From 713199ac2aa8ba9057aa88900b65287333e5c91a Mon Sep 17 00:00:00 2001 From: Yoonseok Ko Date: Tue, 4 May 2021 02:59:21 -0700 Subject: [PATCH] [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 | 4 ++-- infer/src/pulse/PulseBaseDomain.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 78e99a40b..183dd1825 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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) - ~rhs:(lhs.pre :> BaseDomain.t) + ~lhs:(lhs.pre :> BaseDomain.t) + ~rhs:(rhs.pre :> BaseDomain.t) with | NotIsomorphic -> false diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index dcf529be4..191a418d9 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/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