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

@@ -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