Handle BotValue/TopValue in Lattice lifters (closes #1572)

src/domain/lattice.ml

@@ -93,10 +93,10 @@ struct
   include Base
   let leq = equal
   let join x y =
-    if equal x y then x else raise (Unsupported "fake join")
+    if equal x y then x else raise (Unsupported "fake join") (* TODO: TopValue? *)
   let widen = join
   let meet x y =
-    if equal x y then x else raise (Unsupported "fake meet")
+    if equal x y then x else raise (Unsupported "fake meet") (* TODO: BotValue? *)
   let narrow = meet
   include NoBotTop
 
@@ -259,24 +259,36 @@ struct
     | (_, `Top) -> `Top
     | (`Bot, x) -> x
     | (x, `Bot) -> x
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.join x y)
+    | (`Lifted x, `Lifted y) ->
+      try `Lifted (Base.join x y)
+      with TopValue -> `Top
 
   let meet x y =
     match (x,y) with
     | (`Bot, _) -> `Bot
     | (_, `Bot) -> `Bot
     | (`Top, x) -> x
     | (x, `Top) -> x
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.meet x y)
+    | (`Lifted x, `Lifted y) ->
+      try `Lifted (Base.meet x y)
+      with BotValue -> `Bot
 
   let widen x y =
     match (x,y) with
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.widen x y)
+    | (`Lifted x, `Lifted y) ->
+      begin
+        try `Lifted (Base.widen x y)
+        with TopValue -> `Top
+      end
     | _ -> y
 
   let narrow x y =
     match (x,y) with
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (`Lifted x, `Lifted y) ->
+      begin
+        try `Lifted (Base.narrow x y)
+        with BotValue -> `Bot
+      end
     | (_, `Bot) -> `Bot
     | (`Top, y) -> y
     | _ -> x
@@ -315,7 +327,7 @@ struct
     | (x, `Bot) -> x
     | (`Lifted x, `Lifted y) ->
       try `Lifted (Base.join x y)
-      with Uncomparable -> `Top
+      with Uncomparable | TopValue -> `Top
 
   let meet x y =
     match (x,y) with
@@ -325,20 +337,24 @@ struct
     | (x, `Top) -> x
     | (`Lifted x, `Lifted y) ->
       try `Lifted (Base.meet x y)
-      with Uncomparable -> `Bot
+      with Uncomparable | BotValue -> `Bot
 
   let widen x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
-      (try `Lifted (Base.widen x y)
-       with Uncomparable -> `Top)
+      begin
+        try `Lifted (Base.widen x y)
+        with Uncomparable | TopValue -> `Top
+      end
     | _ -> y
 
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
-      (try `Lifted (Base.narrow x y)
-       with Uncomparable -> `Bot)
+      begin
+        try `Lifted (Base.narrow x y)
+        with Uncomparable | BotValue -> `Bot
+      end
     | (_, `Bot) -> `Bot
     | (`Top, y) -> y
     | _ -> x
@@ -378,11 +394,11 @@ struct
     | (x, `Bot) -> x
     | (`Lifted1 x, `Lifted1 y) -> begin
         try `Lifted1 (Base1.join x y)
-        with Unsupported _ -> `Top
+        with Unsupported _ | TopValue -> `Top
       end
     | (`Lifted2 x, `Lifted2 y) -> begin
         try `Lifted2 (Base2.join x y)
-        with Unsupported _ -> `Top
+        with Unsupported _ | TopValue -> `Top
       end
     | _ -> `Top
 
@@ -394,11 +410,11 @@ struct
     | (x, `Top) -> x
     | (`Lifted1 x, `Lifted1 y) -> begin
         try `Lifted1 (Base1.meet x y)
-        with Unsupported _ -> `Bot
+        with Unsupported _ | BotValue -> `Bot
       end
     | (`Lifted2 x, `Lifted2 y) -> begin
         try `Lifted2 (Base2.meet x y)
-        with Unsupported _ -> `Bot
+        with Unsupported _ | BotValue -> `Bot
       end
     | _ -> `Bot
 
@@ -489,7 +505,9 @@ struct
     match (x,y) with
     | (`Bot, _) -> `Bot
     | (_, `Bot) -> `Bot
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.meet x y)
+    | (`Lifted x, `Lifted y) ->
+      try `Lifted (Base.meet x y)
+      with BotValue -> `Bot
 
   let widen x y =
     match (x,y) with
@@ -498,7 +516,11 @@ struct
 
   let narrow x y =
     match (x,y) with
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (`Lifted x, `Lifted y) ->
+      begin
+        try `Lifted (Base.narrow x y)
+        with BotValue -> `Bot
+      end
     | (_, `Bot) -> `Bot
     | _ -> x
 end
@@ -525,7 +547,9 @@ struct
     match (x,y) with
     | (`Top, x) -> `Top
     | (x, `Top) -> `Top
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.join x y)
+    | (`Lifted x, `Lifted y) ->
+      try `Lifted (Base.join x y)
+      with TopValue -> `Top
 
   let meet x y =
     match (x,y) with
@@ -535,7 +559,11 @@ struct
 
   let widen x y =
     match (x,y) with
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.widen x y)
+    | (`Lifted x, `Lifted y) ->
+      begin
+        try `Lifted (Base.widen x y)
+        with TopValue -> `Top
+      end
     | _ -> y
 
   let narrow x y =