Simplify

goblint · Nov 25, 2023 · 8318ad8 · 8318ad8
1 parent 8db2966
commit 8318ad8
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 34 deletions.
diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml
@@ -1108,34 +1108,16 @@ struct
     in
 
     let set_interval min_i max_i =
-      if Val.is_null v then
-        match idx_maximal size with
-        (* ... and size has no upper limit, add all indexes of interval to may_nulls_set *)
-        | None ->  Nulls.add_interval Possibly (min_i, max_i) nulls
-        | Some max_size ->
-          (* ... add all indexes < maximal size to may_nulls_set *)
-          if Z.equal min_i Z.zero && Z.geq max_i max_size then
-            Nulls.add_all Possibly nulls
-          else 
-            Nulls.add_interval Possibly (min_i, Z.min (Z.pred max_size) max_i) nulls
-      else if Val.is_not_null v then
-        if Z.equal min_i Z.zero && Z.geq max_i min_size then
-          Nulls.remove_all Possibly nulls
-        else
-          Nulls.filter_musts (fun x -> (Z.lt x min_i || Z.gt x max_i) && Z.lt x min_size) min_size nulls
+      (* Update max_i so it is capped at the maximum size *)
+      let max_i = BatOption.map_default (fun x -> Z.min max_i @@ Z.pred x) max_i (idx_maximal size) in
+      if Val.is_not_null v then
+        Nulls.remove_interval Possibly (min_i, max_i) min_size nulls 
       else
-        let nulls = match idx_maximal size with
-          (* ... and size has no upper limit, add all indexes of interval to may_nulls_set *)
-          | None -> Nulls.add_interval Possibly (min_i,max_i) nulls
-          | Some max_size when Z.equal min_i Z.zero && Z.geq max_i max_size ->
-            (* ... add all indexes < maximal size to may_nulls_set *)
-            Nulls.add_all Possibly nulls
-          | Some max_size -> Nulls.add_interval Possibly (min_i, Z.min (Z.pred max_size) max_i) nulls
-        in
-        if Z.equal min_i Z.zero && Z.geq max_i min_size then
-          Nulls.remove_all Possibly nulls
+        let nulls = Nulls.add_interval ~maxfull:(idx_maximal size) Possibly (min_i, max_i) nulls in
+        if Val.is_null v then
+          nulls
         else
-          Nulls.filter_musts (fun x -> (Z.lt x min_i || Z.gt x max_i) && Z.lt x min_size) min_size nulls
+          Nulls.remove_interval Possibly (min_i, max_i) min_size nulls 
     in
 
     (* warn if index is (potentially) out of bounds *)

diff --git a/src/cdomains/nullByteSet.ml b/src/cdomains/nullByteSet.ml
@@ -98,17 +98,30 @@ module MustMaySet = struct
     | Definitely -> (MustSet.add i musts, MaySet.add i mays)
     | Possibly -> (musts, MaySet.add i mays)
 
-  let add_interval mode (l,u) (musts, mays) =
+  let add_interval ?maxfull mode (l,u) (musts, mays) =
     match mode with
     | Definitely -> failwith "todo"
     | Possibly -> 
-      let rec add_indexes i max set =
-        if Z.gt i max then
-          set
+      match maxfull with
+      | Some Some maxfull when Z.equal l Z.zero && Z.geq u maxfull -> 
+        (musts, MaySet.top ())
+      | _ ->
+        let rec add_indexes i max set =
+          if Z.gt i max then
+            set
+          else
+            add_indexes (Z.succ i) max (MaySet.add i set)
+        in
+        (musts, add_indexes l u mays)
+
+  let remove_interval mode (l,u) min_size (musts, mays) =
+    match mode with
+    | Definitely -> failwith "todo"
+    | Possibly ->
+        if Z.equal l Z.zero && Z.geq u min_size then 
+          (MustSet.top (), mays)
         else
-          add_indexes (Z.succ i) max (MaySet.add i set)
-      in
-      (musts, add_indexes l u mays)
+          (MustSet.filter (fun x -> (Z.lt x l || Z.gt x u) && Z.lt x min_size) musts min_size, mays)
 
   let add_all mode (musts, mays) =
     match mode with
@@ -131,4 +144,4 @@ module MustMaySet = struct
   let forget_may (musts, mays) = (musts, MaySet.top ())
   let forget_must (musts, mays) = (MustSet.top (), mays)
   let filter_musts f min_size (musts, mays) = (MustSet.filter f musts min_size, mays)
-end
+end