From 42a3176882564c92acdb6fe745a3fcfa749f7b2d Mon Sep 17 00:00:00 2001 From: Kihong Heo Date: Fri, 16 Dec 2016 11:43:49 -0800 Subject: [PATCH] Fix the widening operator of the Map functor Summary: This commit avoids using the join operator for the widening of the Map functor in ```abstractDomain.ml``` and ensures termination when ```ValueDomain``` is infinite by using ```ValueDomain.widen```. Closes https://github.com/facebook/infer/pull/535 Differential Revision: D4319797 Pulled By: sblackshear fbshipit-source-id: 16f15e4 --- infer/src/checkers/abstractDomain.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml index 50733b6a6..dfff8107f 100644 --- a/infer/src/checkers/abstractDomain.ml +++ b/infer/src/checkers/abstractDomain.ml @@ -156,8 +156,17 @@ module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct astate1 astate2 - let widen ~prev ~next ~num_iters:_ = - join prev next + let widen ~prev ~next ~num_iters = + if phys_equal prev next + then prev + else + M.merge + (fun _ v1_opt v2_opt -> match v1_opt, v2_opt with + | Some v1, Some v2 -> Some (ValueDomain.widen ~prev:v1 ~next:v2 ~num_iters) + | Some v, _ | _, Some v -> Some v + | None, None -> None) + prev + next let pp fmt astate = M.pp ~pp_value:ValueDomain.pp fmt astate