Bugfix in Vector rev and Matrix map2i again

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

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

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)

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! *)

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