Explictly define partial order for lattices

lib/analysis/defuse_bool.ml

@@ -22,6 +22,13 @@ module IsZeroLattice = struct
     | _ -> Top
 
   let widening a b = join a b
+
+  let leq a b =
+    match (a, b) with
+    | a, b when equal a b -> true
+    | Bot, _ | _, Top -> true
+    | _, Bot | Top, _ -> false
+    | _ -> false
 end
 
 module IsZeroValueAbstraction = struct

lib/analysis/intra_analysis.ml

@@ -139,6 +139,9 @@ module MapState (V : Lattice) = struct
       let join a b = M.idempotent_union (fun v a b -> V.join a b) a b
       let equal a b = M.reflexive_equal V.equal a b
 
+      let leq a b =
+        M.reflexive_subset_domain_for_all2 (fun _ a b -> V.leq a b) a b
+
       let show m =
         Iter.from_iter (fun f -> M.iter (fun k v -> f (k, v)) m)
         |> Iter.to_string ~sep:", " (fun (k, v) ->

lib/analysis/known_bits.ml

@@ -9,7 +9,7 @@ module IsKnownLattice = struct
   let name = "tnum"
 
   type t = Bot | TNum of { value : Bitvec.t; mask : Bitvec.t } | Top
-  [@@deriving eq]
+  [@@deriving ord, eq]
 
   let tnum v m =
     assert (is_zero (bitand v m));
@@ -39,18 +39,18 @@ module IsKnownLattice = struct
         in
         result "" 0 v m
 
-  let compare a b =
-    if equal a b then 0
+  let leq a b =
+    if equal a b then true
     else
       match (a, b) with
       | TNum { value = av; mask = am }, TNum { value = bv; mask = bm } ->
           if
             (is_zero @@ bitand am (bitnot bm))
             && Bitvec.equal (bitand av (bitnot am)) (bitand bv (bitnot bm))
-          then -1
-          else 1
-      | Bot, _ | _, Top -> -1
-      | _, Bot | Top, _ -> 1
+          then true
+          else false
+      | Bot, _ | _, Top -> true
+      | _, Bot | Top, _ -> false
 
   let bottom = Bot
   let top = Top

lib/analysis/lattice_types.ml

@@ -10,6 +10,7 @@ module type Lattice = sig
   val bottom : t
   val join : t -> t -> t
   val equal : t -> t -> bool
+  val leq : t -> t -> bool
   val widening : t -> t -> t
 end
 
@@ -124,6 +125,14 @@ struct
   let map f a = bind (fun x -> V (f x)) a
   let map2 f a b = bind2 (fun x y -> V (f x y)) a b
   let join a b = match (a, b) with Top, _ -> Top | _, Top -> Top | _ -> Bot
+
+  let leq a b =
+    match (a, b) with
+    | a, b when equal a b -> true
+    | Bot, _ | _, Top -> true
+    | _, Bot | Top, _ -> false
+    | _ -> false
+
   let widening a b = join a b
 end
 

lib/analysis/wrapped_intervals.ml

@@ -24,7 +24,7 @@ module WrappedIntervalsLattice = struct
   let name = "wrappedIntervals"
 
   type t = Top | Interval of { lower : Bitvec.t; upper : Bitvec.t } | Bot
-  [@@deriving eq]
+  [@@deriving ord, eq]
 
   let show l =
     match l with
@@ -78,22 +78,18 @@ module WrappedIntervalsLattice = struct
         size_is_equal upper e;
         ule (sub e lower) (sub upper lower)
 
-  let compare a b =
+  let leq a b =
     match (a, b) with
-    | a, b when equal a b -> 0
-    | Top, _ | _, Bot -> 1
-    | Bot, _ | _, Top -> -1
+    | a, b when equal a b -> true
+    | Bot, _ | _, Top -> true
+    | Top, _ | _, Bot -> false
     | Interval { lower = al; upper = au }, Interval { lower = bl; upper = bu }
       ->
-        if
-          member b al && member b au
-          && ((not (member a bl)) || not (member a bu))
-        then -1
-        else 1
+        member b al && member b au && ((not (member a bl)) || not (member a bu))
 
   let join a b =
-    if compare a b <= 0 then b
-    else if compare b a <= 0 then a
+    if leq a b then b
+    else if leq b a then a
     else
       match (a, b) with
       | Interval { lower = al; upper = au }, Interval { lower = bl; upper = bu }
@@ -146,7 +142,7 @@ module WrappedIntervalsLattice = struct
           match (s, t) with
           | Interval { lower = al; _ }, Interval { lower = bl; _ } ->
               Bitvec.compare al bl
-          | _, _ -> compare s t)
+          | _, _ -> if equal s t then 0 else if leq s t then -1 else 1)
         ints
     in
     let f1 =
@@ -173,7 +169,7 @@ module WrappedIntervalsLattice = struct
         size_is_equal al bl;
         size_is_equal au bu;
         let width = size al in
-        if compare b a <= 0 then a
+        if leq b a then a
         else if Z.geq (cardinality ~width a) (Z.pow (Z.of_int 2) width) then top
         else
           let joined = join a b in
@@ -232,7 +228,7 @@ module WrappedIntervalsLattice = struct
     | Interval { lower; upper } ->
         let width = size lower in
         let np = np ~width in
-        if compare np t <= 0 then
+        if leq np t then
           [ interval lower (smax ~width); interval (smin ~width) upper ]
         else [ t ]
 
@@ -247,7 +243,7 @@ module WrappedIntervalsLattice = struct
     | Interval { lower; upper } ->
         let width = size lower in
         let sp = sp ~width in
-        if compare sp t <= 0 then
+        if leq sp t then
           [ interval lower (umax ~width); interval (umin ~width) upper ]
         else [ t ]
 
@@ -644,7 +640,7 @@ module WrappedIntervalsLatticeOps = struct
           interval (zero ~size:width)
             (concat (zero ~size:k) (ones ~size:(width - k)))
         in
-        if compare (sp ~width) t <= 0 then fallback
+        if leq (sp ~width) t then fallback
         else
           match t with
           | Interval { lower; upper } ->
@@ -661,7 +657,7 @@ module WrappedIntervalsLatticeOps = struct
             (concat (ones ~size:k) (zero ~size:(width - k)))
             (concat (zero ~size:k) (ones ~size:(width - k)))
         in
-        if compare (np ~width) t <= 0 then fallback
+        if leq (np ~width) t then fallback
         else
           match t with
           | Interval { lower; upper } ->
@@ -680,7 +676,7 @@ module WrappedIntervalsLatticeOps = struct
       truncate (lshr ~width t (interval k k)) (hi - lo)
 
   let concat (s, sw) (t, tw) =
-    let t = if compare (sp ~width:tw) t <= 0 then top else t in
+    let t = if leq (sp ~width:tw) t then top else t in
     match (s, t) with
     | Bot, _ | _, Bot -> bottom
     | Top, Top -> top

lib/transforms/may_read_uninit.ml

@@ -25,6 +25,13 @@ module ReadUninit = struct
     | Bot, a -> a
     | Write, Write -> Write
 
+  let leq a b =
+    match (a, b) with
+    | a, b when equal a b -> true
+    | Bot, _ | _, ReadUninit -> true
+    | _, Bot | ReadUninit, _ -> false
+    | _ -> false
+
   let show v = match v with ReadUninit -> "RU" | Bot -> "bot" | Write -> "W"
   let pretty v = Containers_pp.text (show v)
   let widening = join

test/analysis/wrapped_intervals.ml

@@ -37,8 +37,8 @@ let%test_unit "member" =
   assert (member (iv 6 2) 7)
 
 let%test_unit "partial_order" =
-  let ( <= ) a b = compare a b <= 0 in
-  let ( > ) a b = compare a b > 0 in
+  let ( <= ) a b = leq a b in
+  let ( > ) a b = not @@ leq a b in
   let iv a b = interval (Bitvec.of_int ~size:4 a) (Bitvec.of_int ~size:4 b) in
   assert (top <= top);
   assert (bottom <= top);
@@ -176,7 +176,7 @@ let%test "mul2" =
       t
   in
   let concrete = iv ~w:43 0x180fcfd9808 0x180fcfd9808 in
-  compare concrete abstract <= 0
+  leq concrete abstract
 
 let%test "udiv_top_top" =
   let ( = ) = equal in

test/lang/value_soundness.ml

@@ -70,7 +70,7 @@ struct
   let is_sound (_, _, abstract, concrete) =
     let abstract = fst @@ Lazy.force abstract in
     let concrete = fst @@ Lazy.force concrete in
-    V.equal abstract (V.join abstract concrete)
+    V.leq concrete abstract
 
   let suite =
     let open QCheck in