Non-Apron relational domain dimchange tidyup

src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml

@@ -137,18 +137,18 @@ module ArrayMatrix: ArrayMatrixFunctor =
     let reduce_col_with m j =
       if not @@ is_empty m then
         (let r = ref (-1) in
-         for i' = 0 to num_rows m - 1 do
-           let rev_i' = num_rows m - i' - 1 in
-           if !r < 0 && m.(rev_i').(j) <>: A.zero then r := rev_i';
-           if !r <> rev_i' then
-             let g = m.(rev_i').(j) in
+         for i' = 0 to num_rows m - 1 do                            (* i' runs through all row indices *)
+           let rev_i' = num_rows m - i' - 1 in                      (* rev_i' runs through all row indices in reverse order *)
+           if !r < 0 && m.(rev_i').(j) <>: A.zero then r := rev_i'; (* if we found the j-column (non-zero element), store its row index in r *)
+           if !r <> rev_i' then                                     (* exclude the non-zero element's row from the transformation *)
+             let g = m.(rev_i').(j) in                              (* only act if rev_i'/j element is non-zero*)
              if g <>: A.zero then
-               let s = g /: m.(!r).(j) in
-               for j' = 0 to num_cols m - 1 do
+               let s = g /: m.(!r).(j) in                           (* determine the kill factor*)
+               for j' = 0 to num_cols m - 1 do                      (* kill the rev_i' element, eintrailing a modification of the rest columns*)
                  m.(rev_i').(j') <- m.(rev_i').(j') -: s *: m.(!r).(j')
                done
          done;
-         if !r >= 0 then Array.fill m.(!r) 0 (num_cols m) A.zero)
+         if !r >= 0 then Array.fill m.(!r) 0 (num_cols m) A.zero)   (* kill row r *)
 
     let reduce_col_with m j  = timing_wrap "reduce_col_with" (reduce_col_with m) j
     let reduce_col m j =
@@ -165,16 +165,16 @@ module ArrayMatrix: ArrayMatrixFunctor =
 
     let del_cols m cols =
       let n_c = Array.length cols in
-      if n_c = 0 || is_empty m then m
+      if n_c = 0 || is_empty m then m                           (* if #toberemoved=0, return m *)
       else
         let m_r, m_c = num_rows m, num_cols m in
-        if m_c = n_c then empty () else
-          let m' = Array.make_matrix m_r (m_c - n_c) A.zero in
-          for i = 0 to m_r - 1 do
-            let offset = ref 0 in
-            for j = 0 to (m_c - n_c) - 1 do
+        if m_c = n_c then empty () else                         (* if #cols = #toberemoved, return empty *)
+          let m' = Array.make_matrix m_r (m_c - n_c) A.zero in  (* else alloc smaller array m' *)
+          for i = 0 to m_r - 1 do                               (* i iterates rows of m' *)
+            let offset = ref 0 in                               (* offset keeps track of coloffset *)
+            for j = 0 to (m_c - n_c) - 1 do                     (* j iterates cols of m' *)
               while  !offset < n_c &&  !offset + j = cols.(!offset) do incr offset done;
-              m'.(i).(j) <- m.(i).(j + !offset);
+              m'.(i).(j) <- m.(i).(j + !offset);                (* copy m to m' *)
             done
           done;
           m'

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

@@ -186,17 +186,16 @@ module ListMatrix: SparseMatrixFunctor =
     let reduce_col m j = 
       if is_empty m then m 
       else
-        let rec find_pivot idx entries = (* Finds non-zero element in column j and returns pair of row idx and the pivot value *)
+        let rec find_pivot idx entries = (* Finds non-zero element in column j and returns pair of row idx, the pivot value and the row *)
           match entries with
           | [] -> None
           | row :: rest -> let value = V.nth row j in 
-            if value =: A.zero then find_pivot (idx - 1) rest else Some (idx, value)
+            if value =: A.zero then find_pivot (idx - 1) rest else Some (idx, value, row)
         in
         match (find_pivot (num_rows m - 1) (List.rev m)) with
         | None -> m (* column is already filled with zeroes *)
-        | Some (row_idx, pivot) -> 
-          let pivot_row = List.nth m row_idx in (* use the pivot row to reduce all entries in column j to zero, then "delete" the pivot row *)
-          List.mapi (fun idx row ->
+        | Some (row_idx, pivot,pivot_row) -> 
+          List.mapi (fun idx row ->  (* use the pivot row to reduce all entries in column j to zero, then "delete" the pivot row *)
               if idx = row_idx then 
                 V.zero_vec (num_cols m)
               else

src/cdomains/apron/affineEqualityDenseDomain.apron.ml

@@ -30,15 +30,14 @@ struct
   let dim_add ch m = timing_wrap "dim add" (dim_add ch) m
 
 
-  let dim_remove (ch: Apron.Dim.change) m ~del =
+  let dim_remove (ch: Apron.Dim.change) m =
     if Array.length ch.dim = 0 || is_empty m then
       m
     else (
-      Array.modifyi (+) ch.dim;
-      let m' = if not del then let m = copy m in Array.fold_left (fun y x -> reduce_col_with y x; y) m ch.dim else m in
+      let m' = let m = copy m in Array.fold_left (fun y x -> reduce_col_with y x; y) m ch.dim in
       remove_zero_rows @@ del_cols m' ch.dim)
 
-  let dim_remove ch m ~del = timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del
+  let dim_remove ch m = timing_wrap "dim remove" (dim_remove ch) m
 end
 
 (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
@@ -234,12 +233,11 @@ struct
   let meet t1 t2 =
     let sup_env = Environment.lce t1.env t2.env in
 
-    let t1, t2 = change_d t1 sup_env ~add:true ~del:false, change_d t2 sup_env ~add:true ~del:false in
+    let t1, t2 = dimchange2_add t1 sup_env, dimchange2_add t2 sup_env in
     if is_bot t1 || is_bot t2 then
       bot ()
     else
-      (* TODO: Why can I be sure that m1 && m2 are all Some here?
-         Answer: because is_bot checks if t1.d is None and we checked is_bot before. *)
+      (* Option.get, because is_bot checks if t1.d is None and we checked is_bot before. *)
       let m1, m2 = Option.get t1.d, Option.get t2.d in
       if is_top_env t1 then
         {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env}
@@ -461,9 +459,24 @@ struct
         let col_x = Matrix.get_col m dim_x in
         Matrix.set_col_with m col_x dim_y
       in
+      let dropvars m oldenv vars =
+        let dropcols (ch:Apron.Dim.change) m = 
+          if Matrix.is_empty m then (* might be empty when assigned_vars/primed_vars are empty *)
+            m
+          else
+            Matrix.remove_zero_rows @@ Matrix.del_cols m ch.dim
+        in
+        let m = Matrix.copy m in
+        let new_env = Environment.remove_vars oldenv vars in
+        let dimchange = Environment.dimchange2 oldenv new_env in
+        if Environment.equal oldenv new_env then
+          {d = Some m; env = new_env}
+        else
+          { d = Some (dropcols (Option.get dimchange.remove) m); env=new_env}
+      in
       let m_cp = Matrix.copy m in
       let switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in
-      let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars ~del:true in
+      let res = dropvars switched_m multi_t.env primed_vars in
       let x = Option.get res.d in
       if Matrix.normalize_with x then
         {d = Some x; env = res.env}

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -30,15 +30,14 @@ struct
   let dim_add ch m = timing_wrap "dim add" (dim_add ch) m
 
 
-  let dim_remove (ch: Apron.Dim.change) m ~del =
+  let dim_remove (ch: Apron.Dim.change) m =
     if Array.length ch.dim = 0 || is_empty m then
       m
     else (
-      Array.modifyi (+) ch.dim;
-      let m' = if not del then Array.fold_left (fun y x -> reduce_col y x) m ch.dim else m in
+      let m' = Array.fold_left (fun y x -> reduce_col y x) m ch.dim in
       remove_zero_rows @@ del_cols m' ch.dim)
 
-  let dim_remove ch m ~del = timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del
+  let dim_remove ch m = timing_wrap "dim remove" (dim_remove ch) m 
 end
 
 (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
@@ -235,12 +234,11 @@ struct
   let meet t1 t2 =
     let sup_env = Environment.lce t1.env t2.env in
 
-    let t1, t2 = change_d t1 sup_env ~add:true ~del:false, change_d t2 sup_env ~add:true ~del:false in
+    let t1, t2 = dimchange2_add t1 sup_env, dimchange2_add t2 sup_env in
     if is_bot t1 || is_bot t2 then
       bot ()
     else
-      (* TODO: Why can I be sure that m1 && m2 are all Some here?
-         Answer: because is_bot checks if t1.d is None and we checked is_bot before. *)
+      (* Option.get, because is_bot checks if t1.d is None and we checked is_bot before. *)
       let m1, m2 = Option.get t1.d, Option.get t2.d in
       if is_top_env t1 then
         {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env}
@@ -455,8 +453,23 @@ struct
         let col_x = Matrix.get_col_upper_triangular m dim_x in
         Matrix.set_col m col_x dim_y
       in
+      let dropvars m oldenv vars = 
+        let dropcols (ch:Apron.Dim.change) m = 
+          if Matrix.is_empty m then (* might be empty when assigned_vars/primed_vars are empty *)
+            m
+          else
+            Matrix.remove_zero_rows @@ Matrix.del_cols m ch.dim
+        in
+        let m = Matrix.copy m in
+        let new_env = Environment.remove_vars oldenv vars in
+        let dimchange = Environment.dimchange2 oldenv new_env in
+        if Environment.equal oldenv new_env then
+          {d = Some m; env = new_env}
+        else
+          { d = Some (dropcols (BatOption.get dimchange.remove) m); env=new_env}
+      in
       let switched_m = List.fold_left2 replace_col m primed_vars assigned_vars in
-      let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars ~del:true in
+      let res = dropvars switched_m multi_t.env primed_vars in
       let x = Option.get res.d in
       (match Matrix.normalize x with 
        | None -> bot ()

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

@@ -178,14 +178,12 @@ module EqualitiesConjunction = struct
     if Array.length ch.dim = 0 || is_empty m then
       m
     else (
-      let cpy = Array.copy ch.dim in
-      Array.modifyi (+) cpy; (* this is a hack to restore the original https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html remove_dimensions semantics for dim_remove *)
-      let m' = Array.fold_lefti (fun y i x -> forget_variable y (x)) m cpy in  (* clear m' from relations concerning ch.dim *)
-      modify_variables_in_domain m' cpy (-))
+      let m' = Array.fold_lefti (fun y i x -> forget_variable y (x)) m ch.dim in  (* clear m' from relations concerning ch.dim *)
+      modify_variables_in_domain m' ch.dim (-))
 
   let dim_remove ch m = Timing.wrap "dim remove" (fun m -> dim_remove ch m) m
 
-  let dim_remove ch m ~del = let res = dim_remove ch m in if M.tracing then
+  let dim_remove ch m = let res = dim_remove ch m in if M.tracing then
       M.tracel "dim_remove" "dim remove at positions [%s] in { %s } -> { %s }"
         (Array.fold_right (fun i str -> (string_of_int i) ^ ", " ^ str)  ch.dim "")
         (show (snd m))
@@ -443,8 +441,8 @@ struct
 
   let meet t1 t2 =
     let sup_env = Environment.lce t1.env t2.env in
-    let t1 = change_d t1 sup_env ~add:true ~del:false in
-    let t2 = change_d t2 sup_env ~add:true ~del:false in
+    let t1 = dimchange2_add t1 sup_env in
+    let t2 = dimchange2_add t2 sup_env in
     match t1.d, t2.d with
     | Some d1', Some d2' ->
       EConj.IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd d2') t1 (* even on sparse d2, this will chose the relevant conjs to meet with*)
@@ -655,7 +653,7 @@ struct
     match multi_t.d with
     | Some arr when not @@ is_top multi_t ->
       let switched_arr = List.fold_left2 (fun multi_t assigned_var primed_var-> assign_var multi_t assigned_var primed_var) multi_t assigned_vars primed_vars in
-      drop_vars switched_arr primed_vars ~del:true
+      remove_vars switched_arr primed_vars
     | _ -> t
 
   let assign_var_parallel t vv's =

src/cdomains/apron/sharedFunctions.apron.ml

@@ -373,8 +373,10 @@ sig
 
   (** is_empty is true, if the domain representation has a dimension size of zero *)
   val is_empty : t -> bool
+  (** interpret dimension addition in change2.add semantics, see https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html*)
   val dim_add : Apron.Dim.change -> t -> t
-  val dim_remove : Apron.Dim.change -> t -> del:bool-> t
+  (** interpret dimension removal in change2.remove semantics, see https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html*)
+  val dim_remove : Apron.Dim.change -> t -> t
 end
 
 (* Shared operations for the management of the Matrix or Array representations of the domains,
@@ -399,47 +401,45 @@ struct
 
   let copy t = {t with d = Option.map RelDomain.copy t.d}
 
-  let change_d t new_env ~add ~del =
+  let dimchange2_add t new_env =
     if Environment.equal t.env new_env then
       t
     else
       match t.d with
       | None -> bot_env
       | Some m ->
-        let dim_change = (* using Environment.dimchange with swapped parameters is not the originally inteded way for APRON dimchanges if keeping to the spec;
-                            instead, we should make use of Environment.dimchange2, which explicitely provides different format for diff arrays for adding and removing.
-                            We here however produce add_dimension format in both cases.
-                            Weirdly, affineEqualities needs an overhaul of its dim_add and dim_remove before this can be migrated to APRON standard, since it internally
-                            ironically converts from add_dimensions format into remove_dimensions format in both cases;
-                            lin2var already has the correct implementation that can handle the respective diff arrays,
-                            but as a stopgap transforms add_dimensions into remove_dimension format itself for the dim_remove case to be compatible to change_d
-                         *)
-          if add then
-            Environment.dimchange t.env new_env
-          else
-            Environment.dimchange new_env t.env
-        in
-        {d = Some (if add then RelDomain.dim_add dim_change m else RelDomain.dim_remove dim_change m ~del:del); env = new_env}
+        let dim_change2 = Environment.dimchange2 t.env new_env in
+        {
+          d = Some (RelDomain.dim_add (Option.get dim_change2.add) m );
+          env = new_env
+        }
 
-  let change_d t new_env ~add ~del = Vector.timing_wrap "dimension change" (fun del -> change_d t new_env ~add:add ~del:del) del
+  let dimchange2_remove t new_env =
+    if Environment.equal t.env new_env then
+      t
+    else
+      match t.d with
+      | None -> bot_env
+      | Some m ->
+        let dim_change2 = Environment.dimchange2 t.env new_env in
+        {
+          d = Some (RelDomain.dim_remove (Option.get dim_change2.remove) m);
+          env = new_env
+        }
 
   let vars x = Environment.ivars_only x.env
 
   let add_vars t vars =
     let t = copy t in
     let env' = Environment.add_vars t.env vars in
-    change_d t env' ~add:true ~del:false
+    dimchange2_add t env'
 
   let add_vars t vars = Vector.timing_wrap "add_vars" (add_vars t) vars
 
-  let drop_vars t vars ~del =
-    let t = copy t in
+  let remove_vars t vars =
+    let t = copy t in 
     let env' = Environment.remove_vars t.env vars in
-    change_d t env' ~add:false ~del:del
-
-  let drop_vars t vars = Vector.timing_wrap "drop_vars" (drop_vars t) vars
-
-  let remove_vars t vars = drop_vars t vars ~del:false
+    dimchange2_remove t env'
 
   let remove_vars t vars = Vector.timing_wrap "remove_vars" (remove_vars t) vars
 
@@ -450,7 +450,7 @@ struct
 
   let remove_filter t f =
     let env' = Environment.remove_filter t.env f in
-    change_d t env' ~add:false ~del:false
+    dimchange2_remove t env'
 
   let remove_filter t f = Vector.timing_wrap "remove_filter" (remove_filter t) f
 
@@ -462,14 +462,14 @@ struct
   let keep_filter t f =
     let t = copy t in
     let env' = Environment.keep_filter t.env f in
-    change_d t env' ~add:false ~del:false
+    dimchange2_remove t env'
 
   let keep_filter t f = Vector.timing_wrap "keep_filter" (keep_filter t) f
 
   let keep_vars t vs =
     let t = copy t in
     let env' = Environment.keep_vars t.env vs in
-    change_d t env' ~add:false ~del:false
+    dimchange2_remove t env'
 
   let keep_vars t vs = Vector.timing_wrap "keep_vars" (keep_vars t) vs