Merge pull request #1728 from goblint/lattice-lift-po

Weaken `Lattice.Lift{,2}Conf` arguments, remove `Lattice.LiftPO`

Author: sim642

src/analyses/mCPRegistry.ml

@@ -381,7 +381,7 @@ struct
 end
 
 module DomVariantLattice0 (DLSpec : DomainListLatticeSpec)
-  : Lattice.S with type t = int * Obj.t
+  : Lattice.PO with type t = int * Obj.t
 =
 struct
   open DLSpec
@@ -403,11 +403,6 @@ struct
 
   let leq    = binop_map' (fun _ (module S : Lattice.S) x y -> S.leq (Obj.obj x) (Obj.obj y))
 
-  let is_top x = false
-  let is_bot x = false
-  let top () = failwith "DomVariantLattice0.top"
-  let bot () = failwith "DomVariantLattice0.bot"
-
   let pretty_diff () (x, y) =
     let f _ (module S : Lattice.S) x y =
       if S.leq (Obj.obj x) (Obj.obj y) then nil

src/cdomain/value/cdomains/intDomain0.ml

@@ -841,7 +841,7 @@ end
 
 module Lift (Base: IkindUnawareS): IkindUnawareS with type t = [ `Bot | `Lifted of Base.t | `Top ] and type int_t = Base.int_t = (* identical to Flat, but does not go to `Top/Bot` if Base raises Unknown/Error *)
 struct
-  include Lattice.LiftPO (struct
+  include Lattice.LiftConf (struct
       include Printable.DefaultConf
       let top_name = "MaxInt"
       let bot_name = "MinInt"

src/domain/lattice.ml

@@ -239,7 +239,7 @@ end
 module Flat = FlatConf (Printable.DefaultConf)
 
 
-module LiftConf (Conf: Printable.LiftConf) (Base: S) =
+module LiftConf (Conf: Printable.LiftConf) (Base: PO) =
 struct
   include Printable.LiftConf (Conf) (Base)
 
@@ -270,7 +270,7 @@ struct
     | (x, `Bot) -> x
     | (`Lifted x, `Lifted y) ->
       try `Lifted (Base.join x y)
-      with TopValue -> `Top
+      with TopValue | Uncomparable -> `Top
 
   let meet x y =
     match (x,y) with
@@ -280,14 +280,14 @@ struct
     | (x, `Top) -> x
     | (`Lifted x, `Lifted y) ->
       try `Lifted (Base.meet x y)
-      with BotValue -> `Bot
+      with BotValue | Uncomparable -> `Bot
 
   let widen x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
       begin
         try `Lifted (Base.widen x y)
-        with TopValue -> `Top
+        with TopValue | Uncomparable -> `Top
       end
     | _ -> y
 
@@ -296,7 +296,7 @@ struct
     | (`Lifted x, `Lifted y) ->
       begin
         try `Lifted (Base.narrow x y)
-        with BotValue -> `Bot
+        with BotValue | Uncomparable -> `Bot
       end
     | (_, `Bot) -> `Bot
     | (`Top, y) -> y
@@ -305,71 +305,7 @@ end
 
 module Lift = LiftConf (Printable.DefaultConf)
 
-module LiftPO (Conf: Printable.LiftConf) (Base: PO) =
-struct
-  include Printable.LiftConf (Conf) (Base)
-
-  let bot () = `Bot
-  let is_bot x = x = `Bot
-  let top () = `Top
-  let is_top x = x = `Top
-
-  let leq x y =
-    match (x,y) with
-    | (_, `Top) -> true
-    | (`Top, _) -> false
-    | (`Bot, _) -> true
-    | (_, `Bot) -> false
-    | (`Lifted x, `Lifted y) -> Base.leq x y
-
-  let pretty_diff () ((x:t),(y:t)): Pretty.doc =
-    match (x,y) with
-    | (`Lifted x, `Lifted y) -> Base.pretty_diff () (x,y)
-    | _ -> if leq x y then Pretty.text "No Changes" else
-        Pretty.dprintf "%a instead of %a" pretty x pretty y
-
-  let join x y =
-    match (x,y) with
-    | (`Top, _) -> `Top
-    | (_, `Top) -> `Top
-    | (`Bot, x) -> x
-    | (x, `Bot) -> x
-    | (`Lifted x, `Lifted y) ->
-      try `Lifted (Base.join x y)
-      with Uncomparable | TopValue -> `Top
-
-  let meet x y =
-    match (x,y) with
-    | (`Bot, _) -> `Bot
-    | (_, `Bot) -> `Bot
-    | (`Top, x) -> x
-    | (x, `Top) -> x
-    | (`Lifted x, `Lifted y) ->
-      try `Lifted (Base.meet x y)
-      with Uncomparable | BotValue -> `Bot
-
-  let widen x y =
-    match (x,y) with
-    | (`Lifted x, `Lifted y) ->
-      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) ->
-      begin
-        try `Lifted (Base.narrow x y)
-        with Uncomparable | BotValue -> `Bot
-      end
-    | (_, `Bot) -> `Bot
-    | (`Top, y) -> y
-    | _ -> x
-end
-
-module Lift2Conf (Conf: Printable.Lift2Conf) (Base1: S) (Base2: S) =
+module Lift2Conf (Conf: Printable.Lift2Conf) (Base1: PO) (Base2: PO) =
 struct
   include Printable.Lift2Conf (Conf) (Base1) (Base2)