From 418de56be635e161de3d0d826f47d927f1876a53 Mon Sep 17 00:00:00 2001
From: Kevin Adameit <kevin.adameit@icloud.com>
Date: Thu, 5 Dec 2024 15:37:17 +0100
Subject: [PATCH] Fixed affeq_rows_are_valid helper for normalize

---
 .../sparseImplementation/listMatrix.ml        | 21 +++++++++----------
 .../sparseImplementation/sparseVector.ml      |  2 +-
 2 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
index f1183dcd95..2e0eda574f 100644
--- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
+++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
@@ -147,15 +147,6 @@ module ListMatrix: AbstractMatrix =
     let swap_rows m j k =
       List.mapi (fun i row -> if i = j then List.nth m k else if i = k then List.nth m j else row) m
 
-    let is_valid_affeq_matrix m = 
-      let col_count = num_cols m in
-      let row_is_invalid row = (* TODO: Vector findi_opt *)
-        match V.findi_val_opt ((<>:) A.zero) row with
-        | Some (idx, _) -> if idx = col_count - 1 then true else false (* If all cofactors of the affeq are zero, but the constant is non-zero, the row is invalid *)
-        | None -> false (* Full zero row is not invalid *)
-      in
-      List.exists row_is_invalid m
-
     let normalize m =
       let col_count = num_cols m in
       let dec_mat_2D (m : t) (row_idx : int) (col_idx : int) : t = 
@@ -174,6 +165,14 @@ module ListMatrix: AbstractMatrix =
           in
           if piv_col = (num_cols m) then None else Some (piv_row, piv_col, piv_val)
       in
+      let affeq_rows_are_valid m = (* Check if the semantics of an rref-affeq matrix are correct *)
+        let col_count = num_cols m in
+        let row_is_valid row = (* TODO: Vector findi_opt *)
+          match V.findi_val_opt ((<>:) A.zero) row with
+          | Some (idx, _) -> if idx < col_count - 1 then true else false (* If all cofactors of the affeq are zero, but the constant is non-zero, the row is invalid *)
+          | None -> true (* Full zero row is valid *)
+        in
+        List.for_all row_is_valid m in
       let rec main_loop m m' row_idx col_idx = 
         if col_idx = (col_count - 2) then m  (* In this case the whole bottom of the matrix starting from row_index is Zero, so it is normalized *)
         else
@@ -188,7 +187,7 @@ module ListMatrix: AbstractMatrix =
               main_loop subtracted_m m' (row_idx + 1) (piv_col_idx + 1)) (* We start at piv_col_idx + 1 because every other col before that is zero at the bottom*)
       in 
       let m' = main_loop m m 0 0 in
-      if is_valid_affeq_matrix m' then Some m' else None (* TODO: We can check this for each row, using the helper function row_is_invalid *)
+      if affeq_rows_are_valid m' then Some m' else None (* TODO: We can check this for each row, using the helper function row_is_invalid *)
 
 
     (*This function yields the same result as appending vector v to m and normalizing it afterwards would. However, it is usually faster than performing those ops manually.*)
@@ -238,7 +237,7 @@ module ListMatrix: AbstractMatrix =
               let linearly_indep = is_linearly_independent_rref v1 m' in 
               if linearly_indep then false else is_covered_by_helper vs1 m'
         in is_covered_by_helper m1 m2
-              
+
     let is_covered_by m1 m2 = Timing.wrap "is_covered_by" (is_covered_by m1) m2
 
     let find_opt f m =
diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
index 7ac1d4c434..3f80cc7d46 100644
--- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
+++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
@@ -191,7 +191,7 @@ module SparseVector: AbstractVector =
       else
         fst @@ List.find (fun (idx, value) -> f value) v.entries (* Here fst is the idx contained in the found tuple *)
 
-    (* Returns optional of (index * value) where f evaluated to true *)
+    (* Returns optional of (index * value) where f value evaluated to true *)
     let findi_val_opt f v =
       let rec find_zero_or_val vec last_col_idx =
             match vec, last_col_idx with