From 3e7d3d6ae503011ec665bc49d6dfd06d0e266b5f Mon Sep 17 00:00:00 2001
From: Kevin Adameit <kevin.adameit@icloud.com>
Date: Fri, 6 Dec 2024 18:42:36 +0100
Subject: [PATCH] Bugfix in Vector rev and Matrix map2i again

---
 src/analyses/apron/affineEqualityAnalysis.apron.ml         | 2 +-
 .../affineEquality/arrayImplementation/arrayMatrix.ml      | 1 +
 .../affineEquality/sparseImplementation/listMatrix.ml      | 7 ++++---
 .../affineEquality/sparseImplementation/sparseVector.ml    | 2 +-
 src/cdomains/apron/affineEqualityDomain.apron.ml           | 2 ++
 5 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/analyses/apron/affineEqualityAnalysis.apron.ml b/src/analyses/apron/affineEqualityAnalysis.apron.ml
index e262b2653b..80d3b32874 100644
--- a/src/analyses/apron/affineEqualityAnalysis.apron.ml
+++ b/src/analyses/apron/affineEqualityAnalysis.apron.ml
@@ -14,7 +14,7 @@ include RelationAnalysis
 
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
-    let module AD = AffineEqualityDomain.D2 (ArrayVector) (ArrayMatrix) in
+    let module AD = AffineEqualityDomain.D2 (SparseVector) (ListMatrix) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml
index 2248b1f414..5e8407d621 100644
--- a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml
+++ b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml
@@ -71,6 +71,7 @@ module ArrayMatrix: AbstractMatrix =
       V.of_array m.(n)
 
     let remove_row m n =
+      let () = Printf.printf "Before remove_row %i of m:\n%s\n" n (show m) in
       let new_matrix = Array.make_matrix (num_rows m - 1) (num_cols m) A.zero in
       if not @@ is_empty new_matrix then
         if n = 0 then
diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
index 87bf5702da..5440c55244 100644
--- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
+++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
@@ -64,6 +64,7 @@ module ListMatrix: AbstractMatrix =
       List.nth m n
 
     let remove_row m n =
+      let () = Printf.printf "Before remove_row %i of m:\n%s\n" n (show m) in
       List.remove_at n m
 
     let get_col m n =
@@ -149,9 +150,9 @@ module ListMatrix: AbstractMatrix =
       let () = Printf.printf "Before map2i m:\n%sv:%s\n" (show m) (V.show v) in
       let rec map2i_min i acc m v =
         match m, v with
-        | [], _ | _, [] -> List.rev acc
-        | row :: rs, value :: vs ->
-          map2i_min (i + 1) (f i row value :: acc) rs vs
+        | [], _  -> List.rev acc
+        | row :: rs, [] -> List.rev_append (row :: acc) rs
+        | row :: rs, value :: vs -> map2i_min (i + 1) (f i row value :: acc) rs vs
       in  
       let () = Printf.printf "After map2i m:\n%s\n" (show (map2i_min 0 [] m (V.to_list v))) in
       map2i_min 0 [] m (V.to_list v)
diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
index 1dd59d1454..a9e5af6fd0 100644
--- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
+++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
@@ -224,7 +224,7 @@ module SparseVector: AbstractVector =
       List.exists2 f (to_list v1) (to_list v2)
 
     let rev v = 
-      let entries' = List.rev @@ List.map (fun (idx, value) -> (v.len - idx, value)) v.entries in 
+      let entries' = List.rev @@ List.map (fun (idx, value) -> (v.len - 1 - idx, value)) v.entries in 
       {entries = entries'; len = v.len}
 
     let map2i f v v' = (* TODO: optimize! *)
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index a08c44b661..7df3ac7edc 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -305,8 +305,10 @@ struct
             (a, b, max)
           else
             (
+              let () = Printf.printf "Before rev col_a: %s col_b: %s\n" (Vector.show col_a) (Vector.show col_b) in
               let col_a = Vector.rev col_a in
               let col_b = Vector.rev col_b in
+              let () = Printf.printf "After rev col_a: %s col_b: %s\n" (Vector.show col_a) (Vector.show col_b) in
               let i = Vector.find2i (<>:) col_a col_b in
               let (x, y) = Vector.nth col_a i, Vector.nth col_b i in
               let r, diff = Vector.length col_a - (i + 1), x -: y  in