From cc0a40d4ec4b4defcc3f4340433d2c287c4e01fd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 3 Apr 2023 17:56:57 +0300
Subject: [PATCH] Remove unnecessary lval domain special cases (closes #998)

---
 src/cdomains/lval.ml | 18 +++---------------
 1 file changed, 3 insertions(+), 15 deletions(-)

diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml
index ce80b799e3..d90fc3658d 100644
--- a/src/cdomains/lval.ml
+++ b/src/cdomains/lval.ml
@@ -42,8 +42,6 @@ struct
   let rec equal x y =
     match x, y with
     | `NoOffset , `NoOffset -> true
-    | `NoOffset, x
-    | x, `NoOffset -> cmp_zero_offset x = `MustZero (* cannot derive due to this special case, special cases not used for AddressDomain any more due to splitting *)
     | `Field (f1,o1), `Field (f2,o2) when CilType.Fieldinfo.equal f1 f2 -> equal o1 o2
     | `Index (i1,o1), `Index (i2,o2) when Idx.equal i1 i2 -> equal o1 o2
     | _ -> false
@@ -63,11 +61,10 @@ struct
   let pretty_diff () (x,y) =
     dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
 
-  let rec hash = function (* special cases not used for AddressDomain any more due to splitting *)
+  let rec hash = function
     | `NoOffset -> 1
-    | `Field (f,o) when not (is_first_field f) -> Hashtbl.hash f.fname * hash o + 13
-    | `Field (_,o) (* zero offsets need to yield the same hash as `NoOffset! *)
-    | `Index (_,o) -> hash o (* index might become top during fp -> might be zero offset *)
+    | `Field (f,o) -> Hashtbl.hash f.fname * hash o + 13
+    | `Index (_,o) -> hash o
   let name () = "Offset"
 
   let from_offset x = x
@@ -87,8 +84,6 @@ struct
 
   let rec compare o1 o2 = match o1, o2 with
     | `NoOffset, `NoOffset -> 0
-    | `NoOffset, x
-    | x, `NoOffset when cmp_zero_offset x = `MustZero -> 0 (* cannot derive due to this special case, special cases not used for AddressDomain any more due to splitting *)
     | `Field (f1,o1), `Field (f2,o2) ->
       let c = CilType.Fieldinfo.compare f1 f2 in
       if c=0 then compare o1 o2 else c
@@ -114,8 +109,6 @@ struct
   let rec leq x y =
     match x, y with
     | `NoOffset, `NoOffset -> true
-    | `NoOffset, x -> cmp_zero_offset x <> `MustNonzero (* special case not used for AddressDomain any more due to splitting *)
-    | x, `NoOffset -> cmp_zero_offset x = `MustZero (* special case not used for AddressDomain any more due to splitting *)
     | `Index (i1,o1), `Index (i2,o2) when Idx.leq i1 i2 -> leq o1 o2
     | `Field (f1,o1), `Field (f2,o2) when CilType.Fieldinfo.equal f1 f2 -> leq o1 o2
     | _ -> false
@@ -124,11 +117,6 @@ struct
     let op = match cop with `Join -> Idx.join | `Meet -> Idx.meet | `Widen -> Idx.widen | `Narrow -> Idx.narrow in
     match x, y with
     | `NoOffset, `NoOffset -> `NoOffset
-    | `NoOffset, x
-    | x, `NoOffset -> (match cop, cmp_zero_offset x with (* special cases not used for AddressDomain any more due to splitting *)
-      | (`Join | `Widen), (`MustZero | `MayZero) -> x
-      | (`Meet | `Narrow), (`MustZero | `MayZero) -> `NoOffset
-      | _ -> raise Lattice.Uncomparable)
     | `Field (x1,y1), `Field (x2,y2) when CilType.Fieldinfo.equal x1 x2 -> `Field (x1, merge cop y1 y2)
     | `Index (x1,y1), `Index (x2,y2) -> `Index (op x1 x2, merge cop y1 y2)
     | _ -> raise Lattice.Uncomparable (* special case not used for AddressDomain any more due to splitting *)