diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 06268130b2..aa64b7f741 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -29,7 +29,7 @@ struct 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' = 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 remove_zero_rows @@ del_cols m' ch.dim) let dim_remove ch m ~del = VectorMatrix.timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del @@ -59,7 +59,7 @@ struct let open Apron.Texpr1 in let exception NotLinear in let zero_vec = Vector.zero_vec @@ Environment.size t.env + 1 in - let neg v = Vector.map_with Mpqf.neg v; v in + let neg v = Vector.map Mpqf.neg v in let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*) Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0 in @@ -75,13 +75,13 @@ struct Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x) | Var x -> let zero_vec_cp = Vector.copy zero_vec in - let entry_only v = Vector.set_val_with v (Environment.dim_of_var t.env x) Mpqf.one; v in + let entry_only v = Vector.set_val v (Environment.dim_of_var t.env x) Mpqf.one in begin match t.d with | Some m -> let row = Matrix.find_opt (fun r -> Vector.nth r (Environment.dim_of_var t.env x) =: Mpqf.one) m in begin match row with | Some v when is_const_vec v -> - Vector.set_val_with zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)); zero_vec_cp + Vector.set_val zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)) | _ -> entry_only zero_vec_cp end | None -> entry_only zero_vec_cp end @@ -91,17 +91,17 @@ struct | Binop (Add, e1, e2, _, _) -> let v1 = convert_texpr e1 in let v2 = convert_texpr e2 in - Vector.map2_with (+:) v1 v2; v1 + Vector.map2 (+:) v1 v2 | Binop (Sub, e1, e2, _, _) -> let v1 = convert_texpr e1 in let v2 = convert_texpr e2 in - Vector.map2_with (+:) v1 (neg @@ v2); v1 + Vector.map2 (+:) v1 (neg @@ v2) | Binop (Mul, e1, e2, _, _) -> let v1 = convert_texpr e1 in let v2 = convert_texpr e2 in begin match to_constant_opt v1, to_constant_opt v2 with - | _, Some c -> Vector.apply_with_c_with ( *:) c v1; v1 - | Some c, _ -> Vector.apply_with_c_with ( *:) c v2; v2 + | _, Some c -> Vector.apply_with_c ( *:) c v1 + | Some c, _ -> Vector.apply_with_c ( *:) c v2 | _, _ -> raise NotLinear end | Binop _ -> raise NotLinear @@ -294,18 +294,17 @@ struct (a, b, max) else ( - Vector.rev_with col_a; - Vector.rev_with col_b; + let col_a = Vector.rev col_a in + let col_b = Vector.rev 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 let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in - Vector.map2_with (-:) col_a col_b; - Vector.rev_with col_a; + let col_a = Vector.map2 (-:) col_a col_b in + let col_a = Vector.rev col_a in let multiply_by_t m t = - Matrix.map2i_with (fun i' x c -> if i' <= max then (let beta = c /: diff in - Vector.map2_with (fun u j -> u -: (beta *: j)) x t); x) m col_a; - m + Matrix.map2i (fun i' x c -> if i' <= max then (let beta = c /: diff in Vector.map2 (fun u j -> u -: (beta *: j)) x t) else x) m col_a; + in Matrix.remove_row (multiply_by_t a a_r) r, Matrix.remove_row (multiply_by_t b b_r) r, (max - 1) ) diff --git a/src/cdomains/vectorMatrix.ml b/src/cdomains/vectorMatrix.ml index 885c73ab90..3da2707fe2 100644 --- a/src/cdomains/vectorMatrix.ml +++ b/src/cdomains/vectorMatrix.ml @@ -83,6 +83,8 @@ sig val map_with: (num -> num) -> t -> unit + val map: (num -> num) -> t -> t + val compare_length_with: t -> int -> int val of_list: num list -> t @@ -99,6 +101,8 @@ sig val rev_with: t -> unit + val rev: t -> t + val map2i: (int -> num -> num -> num) -> t -> t -> t val map2i_with: (int -> num -> num -> num) -> t -> t -> unit @@ -107,6 +111,8 @@ sig val mapi_with: (int -> num -> num) -> t -> unit + val mapi: (int -> num -> num) -> t -> t + val find2i: (num -> num -> bool) -> t -> t -> int val to_array: t -> num array @@ -180,6 +186,8 @@ sig val map2_with: (vec -> num -> vec) -> t -> vec -> unit + val map2: (vec -> num -> vec) -> t -> vec -> t + val map2i: (int -> vec-> num -> vec) -> t -> vec -> t val map2i_with: (int -> vec -> num -> vec) -> t -> vec -> unit @@ -270,14 +278,26 @@ module ArrayVector: AbstractVector = let rev_with v = Array.rev_in_place v + let rev v = Array.rev v + let map_with f v = Array.modify f v + let map f v = Array.map f v + let map2_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f x y) v1 v2 + let map2 f v1 v2 = + let copy_v1 = copy v1 in + map2_with f copy_v1 v2; copy_v1 + let copy v = Array.copy v let mapi_with f v = Array.iteri (fun i x -> v.(i) <- f i x) v + let mapi f v = + let copy = copy v in + mapi_with f copy; copy + let of_sparse_list ls col_count = let vec = Array.make col_count A.zero in List.iter (fun (idx, value) -> vec.(idx) <- value) ls; @@ -788,8 +808,8 @@ module SparseMatrix: AbstractMatrix = let is_empty m = num_rows m = 0 - (*This should be different if the implimentation is sound*) - (*m.column_count = 0*) + (*This should be different if the implimentation is sound*) + (*m.column_count = 0*) let num_cols m = m.column_count @@ -807,14 +827,14 @@ module SparseMatrix: AbstractMatrix = match cols with | x::xs -> if x < idx - then - let (h,t) = list_of_all_before_index idx xs in - (x::h, t) - else ([],x::xs) + then + let (h,t) = list_of_all_before_index idx xs in + (x::h, t) + else ([],x::xs) | [] -> ([],[]) in (*This could easily be abstracted into the above functions, but its nice to have - it here for readability and debugging*) + it here for readability and debugging*) let rec make_empty_entries_for_idxs idxs = match idxs with | x::xs -> (x, emptyT)::(make_empty_entries_for_idxs xs) @@ -872,7 +892,18 @@ module SparseMatrix: AbstractMatrix = 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 = - failwith "TODO" + let rec set_col_in_row row value = + match row with + | [] -> if value =: A.zero then [] else [(n, value)] + | (col_idx, v)::cs when col_idx > n -> if value =: A.zero then (col_idx, v)::cs else (n, value)::(col_idx, v)::cs + | (col_idx, v)::cs when col_idx = n -> if value =: A.zero then cs else (n, value)::cs + | (col_idx, v)::cs -> (col_idx, v)::(set_col_in_row cs value) + in + let new_entries = List.mapi (fun row_idx row -> + let value = V.nth new_col row_idx in + set_col_in_row row value + ) m.entries in + {entries = new_entries; column_count = m.column_count} let append_matrices m1 m2 = failwith "TODO"