From 72476fbb1208600b2ff9bdd3bb417f89c6bb48d6 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 28 Nov 2023 21:36:52 +0100
Subject: [PATCH] Simplify

---
 src/cdomains/arrayDomain.ml | 16 +++++++---------
 src/cdomains/nullByteSet.ml | 28 ++++++++++++++++------------
 2 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml
index a7b139a740..37d28fc206 100644
--- a/src/cdomains/arrayDomain.ml
+++ b/src/cdomains/arrayDomain.ml
@@ -1260,13 +1260,6 @@ struct
           set
         else
           add_indexes (Z.succ i) max (MaySet.add i set) in
-      let update_must_indexes min_must_null must_nulls_set =
-        if min_must_null =. Z.zero then
-          MustSet.bot ()
-        else
-          (* if strlen < n, every byte starting from min_must_null is surely also transformed to null *)
-          add_indexes min_must_null n must_nulls_set
-          |> MustSet.M.filter (Z.gt n) in
       let update_may_indexes min_may_null may_nulls_set =
         if min_may_null =. Z.zero then
           MaySet.top ()
@@ -1311,7 +1304,7 @@ struct
           Nulls.add_all Possibly nulls
          else
           let (must, mays) = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in
-          (must, mays |> MaySet.M.filter (Z.gt n))  (* TODO: this makes little sense *)
+          (must, mays |> MaySet.M.filter (fun x -> x <. n))  (* TODO: this makes little sense *)
        else
          let min_must_null = Nulls.min_elem Definitely nulls in
          let min_may_null = Nulls.min_elem Possibly nulls in
@@ -1319,7 +1312,12 @@ struct
          warn_no_null min_must_null true min_may_null;
          (* if min_must_null = min_may_null, remove indexes >= n and add all indexes from minimal must/may null to n - 1 in the sets *)
          if min_must_null =. min_may_null then
-           (update_must_indexes min_must_null must_nulls_set, update_may_indexes min_may_null may_nulls_set)
+          (if min_must_null =. Z.zero then
+            Nulls.full_set ()
+          else
+            let nulls = Nulls.add_interval Definitely (min_must_null, Z.pred n) nulls in
+            let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in
+            Nulls.filter (fun x -> x <. n) nulls)
          else
            (MustSet.top (), update_may_indexes min_may_null may_nulls_set)
       in
diff --git a/src/cdomains/nullByteSet.ml b/src/cdomains/nullByteSet.ml
index a7f889ee5a..38fe5cbda9 100644
--- a/src/cdomains/nullByteSet.ml
+++ b/src/cdomains/nullByteSet.ml
@@ -84,6 +84,8 @@ module MustMaySet = struct
 
   let empty () = (MustSet.top (), MaySet.bot ())
 
+  let full_set () = (MustSet.bot (), MaySet.top ())
+
   let is_empty mode (musts, mays) =
     match mode with
     | Definitely -> MaySet.is_empty mays
@@ -123,21 +125,23 @@ module MustMaySet = struct
     | Possibly -> (musts, MaySet.union (MaySet.of_list l) 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
+      else
+        add_indexes (Z.succ i) max (MaySet.add i set)
+    in
+    let mays =
       match maxfull with
       | Some Some maxfull when Z.equal l Z.zero && Z.geq u maxfull -> 
-        (musts, MaySet.top ())
+        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)
-
+        add_indexes l u mays
+    in
+    match mode with
+    | Definitely -> (add_indexes l u musts, mays)
+    | Possibly -> (musts, mays)
+    
   let remove_interval mode (l,u) min_size (musts, mays) =
     match mode with
     | Definitely -> failwith "todo"