Move to operations on Nulls

goblint · Nov 26, 2023 · df10ad6 · df10ad6
1 parent 34d2e1c
commit df10ad6
Show file tree

Hide file tree

Showing 2 changed files with 46 additions and 21 deletions.
diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml
@@ -1380,7 +1380,7 @@ struct
         let may_nulls_set_result = 
           let max_size2 = BatOption.default max_dstsize (idx_maximal truncatedsize) in
           (* get may nulls from src string < maximal size of dest *)
-          MaySet.filter ~max_size: max_size2 (Z.gt max_dstsize) may_nulls_set2'
+          MaySet.filter ~max_size:max_size2 (Z.gt max_dstsize) may_nulls_set2'
           (* and keep indexes of dest >= minimal strlen of src *)
           |> MaySet.union (MaySet.filter ~max_size:max_dstsize (Z.leq min_srclen) may_nulls_set1) in
         ((must_nulls_set_result, may_nulls_set_result), dstsize)
@@ -1477,28 +1477,34 @@ struct
        * for all i1, i2 in may_nulls_set1, may_nulls_set2: add i1 + i2 if it is <= strlen(dest) + strlen(src) to new may_nulls_set
        * and keep indexes > minimal strlen(dest) + strlen(src) of may_nulls_set *)
       if Nulls.is_empty Possibly nulls1 || Nulls.is_empty Possibly nulls2 then
-        let (must_nulls_set1, may_nulls_set1) = nulls1 in
-        let (must_nulls_set2', may_nulls_set2') = nulls2' in
-        let may_nulls_set_result =
-          if max_size1_exists then
-            MaySet.filter ~max_size:max_size1 (fun x -> if maxlen1_exists && maxlen2_exists then x <=. (maxlen1 +. maxlen2) else true) may_nulls_set1
-            |> MaySet.elements
-            (* if may_nulls_set2' is top, limit it to max_size1 *)
-            |> BatList.cartesian_product (MaySet.elements (MaySet.filter ~max_size:max_size1 (fun x -> true) may_nulls_set2'))
+        if max_size1_exists then
+          let nulls1_no_must = Nulls.remove_all Possibly nulls1 in
+          let r = 
+            nulls1_no_must
+            (* filter ensures we have the concete representation *)
+            |> Nulls.filter ~max_size:max_size1 (fun x -> if maxlen1_exists && maxlen2_exists then x <=. (maxlen1 +. maxlen2) else true)
+            |> Nulls.elements ~max_size:max_size1 Possibly
+            |> BatList.cartesian_product (Nulls.elements ~max_size:max_size1 Possibly nulls2')
             |> List.map (fun (i1, i2) -> i1 +. i2)
-            |> MaySet.of_list
-            |> MaySet.union (MaySet.filter ~max_size:max_size1 (Z.lt (minlen1 +. minlen2)) may_nulls_set1)
-            |> MaySet.M.filter (Z.gt max_size1) 
-          else if not (MaySet.is_top may_nulls_set1) && not (MaySet.is_top may_nulls_set2') && maxlen1_exists && maxlen2_exists then
-            MaySet.M.filter (fun x -> if maxlen1_exists && maxlen2_exists then x <=. (maxlen1 +. maxlen2) else true) may_nulls_set1
-            |> MaySet.elements
-            |> BatList.cartesian_product (MaySet.elements may_nulls_set2')
+            |> (fun x -> Nulls.add_list Possibly x (Nulls.filter ~max_size:max_size1 (Z.lt (minlen1 +. minlen2)) nulls1_no_must))
+            |> Nulls.filter (Z.gt max_size1)
+          in 
+          (r, size1)
+        else if Nulls.may_can_benefit_from_filter nulls1 && Nulls.may_can_benefit_from_filter nulls2 && maxlen1_exists && maxlen2_exists then
+          let nulls1_no_must = Nulls.remove_all Possibly nulls1 in
+          let r = 
+            nulls1_no_must
+            (* filter ensures we have the concete representation *)
+            |> Nulls.filter (fun x -> x <=. (maxlen1 +. maxlen2))
+            |> Nulls.elements Possibly
+            |> BatList.cartesian_product (Nulls.elements Possibly nulls2')
             |> List.map (fun (i1, i2) -> i1 +. i2)
-            |> MaySet.of_list
-            |> MaySet.union (MaySet.M.filter (Z.lt (minlen1 +. minlen2)) may_nulls_set1)
-          else
-            MaySet.top () in
-        ((MustSet.top (), may_nulls_set_result), size1)
+            |> (fun x -> Nulls.add_list Possibly x (Nulls.filter (Z.lt (minlen1 +. minlen2)) nulls1_no_must))
+          in 
+          (r, size1)
+        else
+          (Nulls.top (), size1)
+
         (* if minimal must null = minimal may null in ar1 and ar2, add them together and keep indexes > strlen(dest) + strlen(src) of ar1 *)
       else if Nulls.min_elem_precise (nulls1) && Nulls.min_elem_precise nulls2' then
         let min_i1 = Nulls.min_elem Definitely nulls1 in

diff --git a/src/cdomains/nullByteSet.ml b/src/cdomains/nullByteSet.ml
@@ -46,6 +46,14 @@ module MaySet = struct
   module M = SetDomain.ToppedSet (IntDomain.BigInt) (struct let topname = "All Null" end)
   include M
 
+  let elements ?max_size may_nulls_set =
+    if M.is_top may_nulls_set then
+      match max_size with
+      | Some max_size -> M.elements @@ MustSet.compute_set max_size
+      | _ -> failwith "top and no max size supplied"
+    else
+      M.elements may_nulls_set
+
   let remove i may_nulls_set max_size =
     if M.is_top may_nulls_set then
       M.remove i (MustSet.compute_set max_size)
@@ -107,6 +115,11 @@ module MustMaySet = struct
     | Definitely -> (MustSet.add i musts, MaySet.add i mays)
     | Possibly -> (musts, MaySet.add i mays)
 
+  let add_list mode l (musts, mays) =
+    match mode with
+    | Definitely -> failwith "todo"
+    | Possibly -> (musts, MaySet.union (MaySet.of_list l) mays)
+
   let add_interval ?maxfull mode (l,u) (musts, mays) =
     match mode with
     | Definitely -> failwith "todo"
@@ -152,6 +165,12 @@ module MustMaySet = struct
     | Definitely -> musts
     | Possibly -> mays
 
+  let elements ?max_size ?min_size mode (musts, mays) =
+    match mode with
+    | Definitely ->failwith "todo"
+    | Possibly -> MaySet.elements ?max_size mays 
+
+
   let precise_singleton i =
     (MustSet.singleton i, MaySet.singleton i)