Bugfixes in Vector and more Debug prints

src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml

@@ -39,6 +39,7 @@ module ArrayMatrix: AbstractMatrix =
     let copy m = Timing.wrap "copy" (copy) m
 
     let add_empty_columns m cols =
+      let () = Printf.printf "Before add_empty_columns m:\n%s\n" (show m) in
       let nnc = Array.length cols in
       if is_empty m || nnc = 0 then m else
         let nr, nc = num_rows m, num_cols m in
@@ -50,17 +51,20 @@ module ArrayMatrix: AbstractMatrix =
             m'.(i).(j + !offset) <- m.(i).(j);
           done
         done;
+        let () = Printf.printf "After add_empty_columns m:\n%s\n" (show m') in
         m'
 
     let add_empty_columns m cols = Timing.wrap "add_empty_cols" (add_empty_columns m) cols
 
     let append_row m row  =
+      let () = Printf.printf "Before append_row m:\n%s\n" (show m) in
       let size = num_rows m in
       let new_matrix = Array.make_matrix (size + 1) (num_cols m) A.zero in
       for i = 0 to size - 1 do
         new_matrix.(i) <- m.(i)
       done;
       new_matrix.(size) <- V.to_array row;
+      let () = Printf.printf "After append_row m:\n%s\n" (show new_matrix) in
       new_matrix
 
     let get_row m n =
@@ -84,11 +88,14 @@ module ArrayMatrix: AbstractMatrix =
     let set_col_with m new_col n =
       for i = 0 to num_rows m - 1 do
         m.(i).(n) <- V.nth new_col i
-      done; m
+      done;
+      let () = Printf.printf "After set_col m:\n%s\n" (show m) in
+      m
 
     let set_col_with m new_col n = Timing.wrap "set_col" (set_col_with m new_col) n
 
     let set_col m new_col n =
+      let () = Printf.printf "Before set_col m:\n%s\n" (show m) in
       let copy = copy m in
       set_col_with copy new_col n
 
@@ -341,8 +348,10 @@ module ArrayMatrix: AbstractMatrix =
     *)
 
     let map2 f m v =
+      let () = Printf.printf "Before map2 m:\n%s\n" (show m) in
       let m' = copy m in
       map2_with f m' v;
+      let () = Printf.printf "After map2 m:\n%s\n" (show m') in
       m'
 
     let map2_with f m v = Timing.wrap "map2_with" (map2_with f m) v

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

@@ -39,6 +39,7 @@ module ListMatrix: AbstractMatrix =
       Timing.wrap "copy" (copy) m
 
     let add_empty_columns m cols = 
+      let () = Printf.printf "Before add_empty_columns m:\n%s\n" (show m) in
       let cols = Array.to_list cols in 
       let sorted_cols = List.sort Stdlib.compare cols in
       let rec count_sorted_occ acc cols last count = 
@@ -48,12 +49,15 @@ module ListMatrix: AbstractMatrix =
         | (x :: xs) -> count_sorted_occ ((last, count) :: acc) xs x 1
       in
       let occ_cols = count_sorted_occ [] sorted_cols (-1) 0 in
+      let () = Printf.printf "After add_empty_columns m:\n%s\n" (show (List.map (fun row -> V.insert_zero_at_indices row occ_cols) m)) in
       List.map (fun row -> V.insert_zero_at_indices row occ_cols) m
 
     let add_empty_columns m cols =
       Timing.wrap "add_empty_cols" (add_empty_columns m) cols
 
     let append_row m row  =
+    let () = Printf.printf "Before append_row m:\n%s\n" (show m) in
+    let () = Printf.printf "After append_row m:\n%s\n" (show ( m @ [row])) in
       m @ [row]
 
     let get_row m n =
@@ -69,7 +73,9 @@ module ListMatrix: AbstractMatrix =
       Timing.wrap "get_col" (get_col m) n
 
     let set_col m new_col n = 
+      let () = Printf.printf "Before set_col m:\n%s\n" (show m) in
       (* List.mapi (fun row_idx row -> V.set_nth row n (V.nth new_col row_idx)) m *)
+      let () = Printf.printf "After set_col m:\n%s\n" (show (List.map2 (fun row value -> V.set_nth row n value) m (V.to_list new_col))) in
       List.map2 (fun row value -> V.set_nth row n value) m (V.to_list new_col)
 
     let append_matrices m1 m2  = (* keeps dimensions of first matrix, what if dimensions differ?*)
@@ -263,7 +269,9 @@ module ListMatrix: AbstractMatrix =
       List.find_opt f m
 
     let map2 f m v =
+      let () = Printf.printf "Before map2 we have m:\n%s\n" (show m) in
       let vector_length = V.length v in
+      let () = Printf.printf "After map2 we have m:\n%s\n" (show (List.mapi (fun index row -> if index < vector_length then f row (V.nth v index) else row ) m)) in
       List.mapi (fun index row -> if index < vector_length then f row (V.nth v index) else row ) m
 
 

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -4,6 +4,7 @@ open ConvenienceOps
 
 open BatList
 open BatArray
+open Batteries
 
 module List = BatList
 module Array = BatArray
@@ -20,6 +21,20 @@ module SparseVector: AbstractVector =
 
     let to_vector e l = {entries=e; len=l}
 
+    let to_list v = 
+      let[@tail_mod_cons] rec extend_zero_aux i v' =
+        if i >= v.len then [] else (*can probably be removed*)
+          match v', i with
+          | (xi,xv)::xs, _ -> if xi = i then xv::(extend_zero_aux (i+1) xs) else A.zero ::(extend_zero_aux (i+1) v')
+          | [], j when i < v.len -> A.zero :: (extend_zero_aux (i+1) v')
+          | [], _ -> []
+      in 
+      (extend_zero_aux 0 v.entries)
+
+    let of_list l = 
+      let entries' = List.rev @@ List.fold_lefti (fun acc i x -> if x <> A.zero then (i, x) :: acc else acc) [] l
+      in {entries = entries'; len = List.length l}
+
     let keep_vals v n = 
       let rec keep_vals_vec v n =
         match v with 
@@ -82,7 +97,8 @@ module SparseVector: AbstractVector =
       in
       {entries = add_indices_helper v.entries idx 0; len = v.len + List.length idx}
 
-    let set_nth v n num = 
+    let set_nth v n num = (* TODO: Optimize! *)
+      (*
       if n >= v.len then failwith "Out of bounds" 
       else
         let rev_entries', _ = List.fold_lefti (fun (acc, found) i (idx, value) -> 
@@ -99,6 +115,8 @@ module SparseVector: AbstractVector =
 
           ) ([], false) v.entries in
         {entries = List.rev rev_entries'; len = v.len}
+        *)
+      of_list @@ List.mapi (fun i x -> if i = n then num else x) (to_list v)
 
     let insert_val_at n new_val v = 
       if n > v.len then failwith "n too large" else (* Does this happen? Otherwise we can omit this comparison, here right now to be semantically equivalent *)
@@ -153,17 +171,14 @@ module SparseVector: AbstractVector =
       if v.len <> v'.len then raise (Invalid_argument "Unequal lengths") else 
         (aux acc v.entries v'.entries)
 
-    let apply_with_c f c v =
-      let entries' = List.map (fun (idx, value) -> (idx, f value c)) v.entries in
-      {entries = entries'; len = v.len}
 
     let zero_vec n = 
       {entries = []; len = n}
 
     let is_zero_vec v = (v.entries = [])
 
-    let nth v n = 
-      if n >= v.len then failwith "V.nth out of bounds"
+    let nth v n = (* Note: This exception HAS TO BE THROWN! It is expected by the domain *)
+      if n >= v.len then raise (Invalid_argument "Cannot access vector element (out of bounds)")
       else
         let rec nth v = match v with (* List.assoc would also work, but we use the fact that v is sorted *)
           | [] -> A.zero
@@ -175,24 +190,12 @@ module SparseVector: AbstractVector =
     let length v =
       v.len
 
-    let of_list l = 
-      let entries' = List.rev @@ List.fold_lefti (fun acc i x -> if x <> A.zero then (i, x) :: acc else acc) [] l
-      in {entries = entries'; len = List.length l}
-
-    let to_list v = 
-      let[@tail_mod_cons] rec extend_zero_aux i v' =
-        if i >= v.len then [] else (*can probably be removed*)
-          match v', i with
-          | (xi,xv)::xs, _ -> if xi = i then xv::(extend_zero_aux (i+1) xs) else A.zero ::(extend_zero_aux (i+1) v')
-          | [], j when i < v.len -> A.zero :: (extend_zero_aux (i+1) v')
-          | [], _ -> []
-      in 
-      (extend_zero_aux 0 v.entries)
-
     let map2 f v v' = 
       if v.len <> v'.len then failwith "Unequal vector length" else 
         of_list (List.map2 f (to_list v) (to_list v'))
 
+    let apply_with_c f c v  = (* TODO: optimize! *)
+      of_list @@ List.map (fun value -> f value c) (to_list v)
 
     let findi f v = 
       if f A.zero then  
@@ -246,7 +249,7 @@ module SparseVector: AbstractVector =
       of_list (List.mapi f (to_list v))
 
     let find2i f v v' = (* TODO: optimize! *)
-      failwith "TODO"
+      fst @@ List.findi (fun _ (val1, val2) -> (uncurry f) (val1, val2)) (List.combine (to_list v) (to_list v'))
 
     let to_array v = 
       let vec = Array.make v.len A.zero in 

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -33,11 +33,13 @@ struct
 
 
   let dim_remove (ch: Apron.Dim.change) m ~del =
+    let () = Printf.printf "Before dim_remove m:\n%s" (show m) in
     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 y x) m ch.dim else m in
+      let () = Printf.printf "After dim_remove m':\n%s" (show (remove_zero_rows @@ del_cols 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
@@ -348,6 +350,7 @@ struct
 
   let join a b =
     let res = join a b in
+    let () = Printf.printf "join a: %s b: %s -> %s \n" (show a) (show b) (show res) in
     if M.tracing then M.tracel "join" "join a: %s b: %s -> %s " (show a) (show b) (show res) ;
     res
 
@@ -368,6 +371,7 @@ struct
   let remove_rels_with_var x var env = Timing.wrap "remove_rels_with_var" remove_rels_with_var x var env 
 
   let forget_vars t vars =
+    let () = Printf.printf "forget_vars m:\n%s" (show t) in
     if is_bot t || is_top_env t || vars = [] then
       t
     else
@@ -409,7 +413,8 @@ struct
     in
     (* let assign_uninvertible_rel x var b env = Timing.wrap "assign_uninvertible" (assign_uninvertible_rel x var b) env in *)
     let is_invertible v = Vector.nth v @@ Environment.dim_of_var t.env var <>: Mpqf.zero
-    in let affineEq_vec = get_coeff_vec t texp
+    in let affineEq_vec = get_coeff_vec t texp in
+    let () = Printf.printf "After affineEq_vec m:\n%s\n" (Vector.show (Option.get affineEq_vec))
     in if is_bot t then t else let m = Option.get t.d in
       match affineEq_vec with
       | Some v when is_top_env t -> if is_invertible v then t else assign_uninvertible_rel m var v t.env
@@ -445,20 +450,23 @@ struct
     res
 
   let assign_var_parallel t vv's =
+    let () = Printf.printf "Before assign_var_parallel m:\n%s\n" (show t) in
     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 multi_t = List.fold_left2 (fun t' v_prime (_,v') -> assign_var t' v_prime v') t_primed primed_vars vv's in
+    let () = Printf.printf "After assign_var_parallel multi_t:\n%s\n" (show multi_t) in
     match multi_t.d with
-    | Some m when not @@ is_top_env multi_t -> let () = Printf.printf "Matrix in Domain m:\n%s" (Matrix.show m) in
+    | Some m when not @@ is_top_env multi_t -> let () = Printf.printf "Matrix in Domain m:\n%s\n" (Matrix.show m) in
       let replace_col m x y =
         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 m col_x dim_y
       in
       let m_cp = Matrix.copy m in
       let switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in
+      let () = Printf.printf "Switched Matrix in Domain switched_m:\n%s\n" (Matrix.show switched_m) in
       let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars ~del:true in
       let x = Option.get res.d in
       (match Matrix.normalize x with