Remove unnecessary lval domain special cases (closes #998)

goblint · Apr 3, 2023 · cc0a40d · cc0a40d
1 parent 1985b99
commit cc0a40d
Showing 1 changed file with 3 additions and 15 deletions.
diff --git 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 *)