Merge pull request #1754 from goblint/dimchange-tidyup

Dimchange tidyup

Author: DrMichaelPetter

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}
@@ -448,22 +446,35 @@ struct
     if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
     res
 
-  let assign_var_parallel t vv's =
+  let assign_var_parallel t vv's =                                (* vv's is a list of pairs of lhs-variables and their rhs-values *)
     let assigned_vars = List.map fst vv's in
-    let t = add_vars t assigned_vars in
-    let primed_vars = List.init (List.length assigned_vars) (fun i -> Var.of_string (Int.to_string i  ^"'")) in (* TODO: we use primed vars in analysis, conflict? *)
-    let t_primed = add_vars t primed_vars in
+    let t = add_vars t assigned_vars in                           (* introduce all lhs-variables to the relation data structure *)
+    let primed_vars = List.init                                   (* create a list with primed variables "i'" for each lhs-variable *)
+        (List.length assigned_vars) 
+        (fun i -> Var.of_string (Int.to_string i  ^"'")) 
+    in (* TODO: we use primed integers as var names, conflict? *)
+    let t_primed = add_vars t primed_vars in                      (* introduce primed variables to the relation data structure *)
+    (* sequence of assignments: i' = snd vv_i : *)
     let multi_t = List.fold_left2 (fun t' v_prime (_,v') -> assign_var t' v_prime v') t_primed primed_vars vv's in
     match multi_t.d with
-    | Some m when not @@ is_top_env multi_t ->
-      let replace_col m x y =
+    | Some m when not @@ is_top_env multi_t ->                    (* SUBSTITUTE assigned_vars/primed_vars via OVERWRITE & ERASE *)
+      let replace_col m x y =                                     (* OVERWRITES column for var_y with column for var_x *)
         let dim_x, dim_y = Environment.dim_of_var multi_t.env x, Environment.dim_of_var multi_t.env y in
         let col_x = Matrix.get_col m dim_x in
         Matrix.set_col_with m col_x dim_y
       in
+      let erase_cols m old_env to_erase =                         (* ERASES (i.e. entries are removed and column collapsed) from m all to_erase-columns *)
+        let m = Matrix.copy m in
+        let new_env = Environment.remove_vars old_env to_erase in
+        let dimchange = Environment.dimchange2 old_env new_env in
+        if Environment.equal old_env new_env then
+          {d = Some m; env = new_env}
+        else
+          { d = Some (Matrix.remove_zero_rows @@ Matrix.del_cols m (Option.get dimchange.remove).dim); 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 switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in (* OVERWRITE columns for assigned_vars with column for primed_vars *)
+      let res = erase_cols switched_m multi_t.env primed_vars in                     (* ERASE column for primed_vars *)
       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}
@@ -442,21 +440,33 @@ struct
     if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
     res
 
-  let assign_var_parallel t vv's =
-    let assigned_vars = List.map fst vv's in
-    let t = add_vars t assigned_vars in
-    let primed_vars = List.init (List.length assigned_vars) (fun i -> Var.of_string (Int.to_string i  ^"'")) in (* TODO: we use primed vars in analysis, conflict? *)
-    let t_primed = add_vars t primed_vars in
+  let assign_var_parallel t vv's =                                (* vv's is a list of pairs of lhs-variables and their rhs-values *)
+    let assigned_vars = List.map fst vv's in 
+    let t = add_vars t assigned_vars in                           (* introduce all lhs-variables to the relation data structure *)
+    let primed_vars = List.init                                   (* create a list with primed variables "i'" for each lhs-variable *)
+        (List.length assigned_vars) 
+        (fun i -> Var.of_string (Int.to_string i  ^"'")) 
+    in (* TODO: we use primed integers as var names, conflict? *)
+    let t_primed = add_vars t primed_vars in                      (* introduce primed variables to the relation data structure *)
+    (* sequence of assignments: i' = snd vv_i : *)
     let multi_t = List.fold_left2 (fun t' v_prime (_,v') -> assign_var t' v_prime v') t_primed primed_vars vv's in
     match multi_t.d with
-    | Some m when not @@ is_top_env multi_t -> 
-      let replace_col m x y =
+    | Some m when not @@ is_top_env multi_t ->                    (* SUBSTITUTE assigned_vars/primed_vars via OVERWRITE & ERASE *)
+      let replace_col m x y =                                     (* OVERWRITES column for var_y with column for var_x *)
         let dim_x, dim_y = Environment.dim_of_var multi_t.env x, Environment.dim_of_var multi_t.env y in
         let col_x = Matrix.get_col_upper_triangular m dim_x in
         Matrix.set_col m col_x dim_y
       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 erase_cols m old_env to_erase =                         (* ERASES (i.e. entries are removed and column collapsed) from m all to_erase-columns *)
+        let new_env = Environment.remove_vars old_env to_erase in
+        let dimchange = Environment.dimchange2 old_env new_env in
+        if Environment.equal old_env new_env then
+          {d = Some m; env = new_env}
+        else
+          { d = Some (Matrix.remove_zero_rows @@ Matrix.del_cols m (BatOption.get dimchange.remove).dim); env = new_env}
+      in
+      let switched_m = List.fold_left2 replace_col m primed_vars assigned_vars in (* OVERWRITE columns for assigned_vars with column for primed_vars *)
+      let res = erase_cols switched_m multi_t.env primed_vars in                  (* ERASE column for primed_vars *)
       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 =