diff --git a/dune-project b/dune-project index 895f605a30..c4a627e95f 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,4 @@ -(lang dune 3.7) +(lang dune 3.13) (using dune_site 0.1) (cram enable) (name goblint) diff --git a/goblint.opam b/goblint.opam index 694d7e4c93..06018358ed 100644 --- a/goblint.opam +++ b/goblint.opam @@ -35,7 +35,7 @@ homepage: "https://goblint.in.tum.de" doc: "https://goblint.readthedocs.io/en/latest/" bug-reports: "https://github.com/goblint/analyzer/issues" depends: [ - "dune" {>= "3.7"} + "dune" {>= "3.13"} "ocaml" {>= "4.14"} "goblint-cil" {>= "2.0.5"} "batteries" {>= "3.5.1"} diff --git a/src/analyses/apron/affineEqualityAnalysis.apron.ml b/src/analyses/apron/affineEqualityAnalysis.apron.ml index d4a1e5be2e..c1fc2a51e0 100644 --- a/src/analyses/apron/affineEqualityAnalysis.apron.ml +++ b/src/analyses/apron/affineEqualityAnalysis.apron.ml @@ -4,11 +4,30 @@ open Analyses +open SparseVector +open ListMatrix + +open ArrayVector +open ArrayMatrix + include RelationAnalysis +(* There are two versions of the affeq domain. + 1. Sparse without side effects + 2. Dense Array with side effects + Default: sparse implementation + The array implementation with side effects of the affeq domain is used when the --disable ana.affeq.sparse option is set *) +let get_domain: (module RelationDomain.RD) Lazy.t = + lazy ( + if GobConfig.get_bool "ana.affeq.sparse" then + (module AffineEqualityDomain.D2 (SparseVector) (ListMatrix)) + else + (module AffineEqualityDenseDomain.D2 (ArrayVector) (ArrayMatrix)) + ) + let spec_module: (module MCPSpec) Lazy.t = lazy ( - let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in + let module AD = (val Lazy.force get_domain) in let module Priv = (val RelationPriv.get_priv ()) in let module Spec = struct diff --git a/src/cdomains/vectorMatrix.ml b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml similarity index 64% rename from src/cdomains/vectorMatrix.ml rename to src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml index a3712274ab..84771a0a15 100644 --- a/src/cdomains/vectorMatrix.ml +++ b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml @@ -1,286 +1,50 @@ -(** OCaml implementations of vectors and matrices. *) +open Matrix +open ArrayVector +open RatOps open Batteries -module Array = Batteries.Array -module M = Messages -(* let timing_wrap = Timing.wrap *) -(* Disable timing of VectorMatrix and AffineEqualityDomain. - This is cleaner than a timing functor because the timed functions also call each other. *) -let timing_wrap _ f x = f x +let timing_wrap = Vector.timing_wrap -(** Abstracts the functions of the Mpqf module for rationals from Apron that implements multi-precision rationals. - One could later exchange "Mpqf" with a different module that provides the functions specified by this interface. *) -module type RatOps = +module type ArrayMatrix = sig - type t [@@deriving eq, ord, hash] - val add : t -> t -> t - val sub : t -> t -> t - val mul : t -> t -> t - val div : t -> t -> t - val neg : t -> t - val abs : t -> t - val to_string: t -> string - val of_int: int -> t - val zero: t - val one: t - val get_den: t -> Z.t - val get_num: t -> Z.t -end - -(** It provides more readable infix operators for the functions of RatOps. - It is designed to be included by modules that make use of RatOps's functions. *) -module ConvenienceOps (A: RatOps) = -struct - let ( *: ) = A.mul - let (+:) = A.add - let (-:) = A.sub - let (/:) = A.div - let (=:) x y = A.equal x y - let (<>:) x y = not (A.equal x y) - let (<:) x y = A.compare x y < 0 - let (>:) x y = A.compare x y > 0 - let (<=:) x y = A.compare x y <= 0 - let (>=:) x y = A.compare x y >= 0 - let of_int x = A.of_int x -end - -(** High-level abstraction of a vector. *) -module type Vector = -sig - type num - type t [@@deriving eq, ord, hash] - - val show: t -> string - - val keep_vals: t -> int -> t - - val remove_val: t -> int -> t - - val set_val: t -> int -> num -> t - - val set_val_with: t -> int -> num -> unit - - val insert_val: int -> num -> t -> t - - val apply_with_c: (num -> num -> num) -> num -> t -> t - - val apply_with_c_with: (num -> num -> num) -> num -> t -> unit - - val zero_vec: int -> t - - val nth: t -> int -> num - - val length: t -> int - - val map2: (num -> num -> num) -> t -> t -> t - - val map2_with: (num -> num -> num) -> t -> t -> unit - - val findi: (num -> bool) -> t -> int - - val map: (num -> num) -> t -> t - - val map_with: (num -> num) -> t -> unit - - val compare_length_with: t -> int -> int - - val of_list: num list -> t - - val to_list: t -> num list - - val filteri: (int -> num -> bool) -> t -> t - - val append: t -> t -> t - - val exists: (num -> bool) -> t -> bool - - val rev: t -> t - - val rev_with: t -> unit - - val map2i: (int -> num -> num -> num) -> t -> t -> t - - val map2i_with: (int -> num -> num -> num) -> t -> t -> unit - - val mapi: (int -> num -> num) -> t -> t - - val mapi_with: (int -> num -> num) -> t -> unit - - val find2i: (num -> num -> bool) -> t -> t -> int - - val to_array: t -> num array - - val of_array: num array -> t - - val copy: t -> t -end - -(** Some functions inside have the suffix _with, which means that the function has side effects. *) -module type AbstractVector = - functor (A: RatOps) -> - sig - include Vector with type num:= A.t - end - - -(** High-level abstraction of a matrix. *) -module type Matrix = -sig - type num - type vec - type t [@@deriving eq, ord, hash] - - val empty: unit -> t (* TODO: needs unit? *) - - val is_empty: t -> bool - - val show: t -> string - - val add_empty_columns: t -> int array -> t - - val append_row: t -> vec -> t - - val get_row: t -> int -> vec - - val del_col: t -> int -> t - - val del_cols: t -> int array -> t - - val remove_row: t -> int -> t - + include Matrix val get_col: t -> int -> vec - val append_matrices: t -> t -> t - - val num_rows: t -> int - - val num_cols: t -> int + val set_col_with: t -> vec -> int -> t - val reduce_col: t -> int -> t + val del_col: t -> int -> t val reduce_col_with: t -> int -> unit - val normalize: t -> t Option.t (*Gauss-Jordan Elimination to get matrix in reduced row echelon form (rref) + deletion of zero rows. None matrix has no solution*) - val normalize_with: t -> bool val rref_vec_with: t -> vec -> t Option.t val rref_matrix_with: t -> t -> t Option.t - val find_opt: (vec -> bool) -> t -> vec option - - val map2: (vec -> num -> vec) -> t -> vec -> t - val map2_with: (vec -> num -> vec) -> t -> vec -> unit - val map2i: (int -> vec-> num -> vec) -> t -> vec -> t - val map2i_with: (int -> vec -> num -> vec) -> t -> vec -> unit - val set_col: t -> vec -> int -> t - - val set_col_with: t -> vec -> int -> t - - val init_with_vec: vec -> t - - val remove_zero_rows: t -> t - - val is_covered_by: t -> t -> bool - - val copy: t -> t - + val append_matrices: t -> t -> t end -(** Some functions inside have the suffix _with, which means that the function has side effects. *) -module type AbstractMatrix = - functor (A: RatOps) (V: AbstractVector) -> +(** Some functions inside have the suffix _with, which means that the function is not purely functional. *) +module type ArrayMatrixFunctor = + functor (A: RatOps) (V: ArrayVectorFunctor) -> sig - include Matrix with type vec := V(A).t and type num := A.t - end - - -(** Array-based vector implementation. *) -module ArrayVector: AbstractVector = - functor (A: RatOps) -> - struct - include ConvenienceOps (A) - include Array - type t = A.t array [@@deriving eq, ord, hash] - - let show t = - let t = Array.to_list t in - let rec list_str l = - match l with - | [] -> "]" - | x :: xs -> (A.to_string x) ^" "^(list_str xs) - in - "["^list_str t^"\n" - - let keep_vals v n = - if n >= Array.length v then v else - Array.filteri (fun i x -> i < n) v (* TODO: take? *) - - let compare_length_with v len = - Int.compare (Array.length v) len - - let remove_val v n = - if n >= Array.length v then failwith "n outside of Array range" else - Array.init (Array.length v - 1) (fun i -> if i < n then Array.get v i else Array.get v (i + 1)) (* TODO: remove_at? *) - - let set_val_with v n new_val = - if n >= Array.length v then failwith "n outside of Array range" else - Array.set v n new_val - - let set_val v n new_val = - let copy = copy v in - set_val_with copy n new_val; copy - - let insert_val n new_val v = - if n > Array.length v then failwith "n too large" else - Array.init (Array.length v + 1) (fun i -> if i < n then Array.get v i else if i = n then new_val else Array.get v (i -1)) (* insert? *) - - let apply_with_c f c v = - Array.map (fun x -> f x c) v - - let zero_vec n = Array.make n A.zero - - let nth = Array.get - - let map2i f v1 v2 = - let f' i = uncurry (f i) in - Array.mapi f' (Array.combine v1 v2) (* TODO: iter2i? *) - - let map2i_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f i x y) v1 v2 - - let find2i f v1 v2 = - Array.findi (uncurry f) (Array.combine v1 v2) (* TODO: iter2i? *) - - let to_array v = v - - let of_array v = v - - let apply_with_c_with f c v = Array.modify (fun x -> f x c) v - - let rev_with v = Array.rev_in_place v - - let map_with f v = Array.modify f v - - let map2_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f x y) v1 v2 - - let copy v = Array.copy v - - let mapi_with f v = Array.iteri (fun i x -> v.(i) <- f i x) v + include ArrayMatrix with type vec := V(A).t and type num := A.t end -open Batteries.Array - (** Array-based matrix implementation. It provides a normalization function to reduce a matrix into reduced row echelon form. Operations exploit that the input matrix/matrices are in reduced row echelon form already. *) -module ArrayMatrix: AbstractMatrix = - functor (A: RatOps) (V: AbstractVector) -> +(* The functions that have the suffix _with are not purely functional and affect the program state beyond their return value. + They were used in a previous version of the affineEqualityDomain. + These calls were removed to transition to list-based matrices.*) +module ArrayMatrix: ArrayMatrixFunctor = + functor (A: RatOps) (V: ArrayVectorFunctor) -> struct include ConvenienceOps(A) module V = V(A) @@ -296,6 +60,9 @@ module ArrayMatrix: AbstractMatrix = let num_rows m = Array.length m + let compare_num_rows m1 m2 = + Int.compare (Array.length m1) (Array.length m2) + let is_empty m = (num_rows m = 0) @@ -312,7 +79,7 @@ module ArrayMatrix: AbstractMatrix = 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 - let m' = make_matrix nr (nc + nnc) A.zero in + let m' = Array.make_matrix nr (nc + nnc) A.zero in for i = 0 to nr - 1 do let offset = ref 0 in for j = 0 to nc - 1 do @@ -326,7 +93,7 @@ module ArrayMatrix: AbstractMatrix = let append_row m row = let size = num_rows m in - let new_matrix = make_matrix (size + 1) (num_cols m) A.zero 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; @@ -337,7 +104,7 @@ module ArrayMatrix: AbstractMatrix = V.of_array m.(n) let remove_row m n = - let new_matrix = make_matrix (num_rows m - 1) (num_cols m) A.zero 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 Array.blit m 1 new_matrix 0 (num_rows m - 1) @@ -414,6 +181,7 @@ module ArrayMatrix: AbstractMatrix = let del_cols m cols = timing_wrap "del_cols" (del_cols m) cols + (* This does NOT have the same semantics as map2i_with. While map2i_with can deal with m and v having different lenghts, map2i will raise Invalid_argument in that case*) let map2i f m v = let f' x (i,y) = V.to_array @@ f i (V.of_array x) y in let range_array = Array.init (V.length v) Fun.id in @@ -510,7 +278,7 @@ module ArrayMatrix: AbstractMatrix = let rref_vec_with m v = - (*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.*) + (*This function yields the same result as appending vector v to m, normalizing it and removing zero rows would. However, it is usually faster than performing those ops manually.*) (*m must be in rref form and contain the same num of cols as v*) (*If m is empty then v is simply normalized and returned*) let v = V.to_array v in @@ -608,4 +376,4 @@ module ArrayMatrix: AbstractMatrix = done let map2i_with f m v = timing_wrap "map2i_with" (map2i_with f m) v - end + end \ No newline at end of file diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml new file mode 100644 index 0000000000..59d75a0bfe --- /dev/null +++ b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml @@ -0,0 +1,128 @@ +open Vector +open RatOps + +open Batteries + +module type ArrayVector = +sig + include Vector + val mapi_with: (int -> num -> num) -> t -> unit + + val map_with: (num -> num) -> t -> unit + + val map2_with: (num -> num -> num) -> t -> t -> unit + + val map2i_with: (int -> num -> num -> num) -> t -> t -> unit + + val filteri: (int -> num -> bool) -> t -> t + + val findi: (num -> bool) -> t -> int + + val find2i: (num -> num -> bool) -> t -> t -> int + + val exists: (num -> bool) -> t -> bool + + val set_nth_with: t -> int -> num -> unit + + val insert_val_at: t -> int -> num -> t + + val apply_with_c_with: (num -> num -> num) -> num -> t -> unit + + val rev_with: t -> unit + + val append: t -> t -> t +end + +module type ArrayVectorFunctor = + functor (A: RatOps) -> + sig + include ArrayVector with type num:= A.t + end + +(** Array-based vector implementation. *) +module ArrayVector: ArrayVectorFunctor = + functor (A: RatOps) -> + struct + include ConvenienceOps (A) + include Array + type t = A.t array [@@deriving eq, ord, hash] + + let show t = + let t = Array.to_list t in + let rec list_str l = + match l with + | [] -> "]" + | x :: xs -> (A.to_string x) ^" "^(list_str xs) + in + "["^list_str t^"\n" + + let keep_vals v n = + if n >= Array.length v then v else + Array.filteri (fun i x -> i < n) v (* TODO: take? *) + + let compare_length_with v len = + Int.compare (Array.length v) len + + let remove_nth v n = + if n >= Array.length v then failwith "n outside of Array range" else + Array.init (Array.length v - 1) (fun i -> if i < n then Array.get v i else Array.get v (i + 1)) (* TODO: remove_at? *) + + let set_nth_with v n new_val = + if n >= Array.length v then failwith "n outside of Array range" else + Array.set v n new_val + + let set_nth v n new_val = + let copy = copy v in + set_nth_with copy n new_val; copy + + let insert_val_at v n new_val = + if n > Array.length v then failwith "n too large" else + Array.init (Array.length v + 1) (fun i -> if i < n then Array.get v i else if i = n then new_val else Array.get v (i -1)) (* insert? *) + + let zero_vec n = Array.make n A.zero + + let is_const_vec v = + compare_length_with (filteri (fun i x -> (*Inefficient*) + compare_length_with v (i + 1) > 0 && x <>: A.zero) v) 1 = 0 + + let nth = Array.get + + let map2i f v1 v2 = + let f' i = uncurry (f i) in + Array.mapi f' (Array.combine v1 v2) (* TODO: iter2i? *) + + let map2i_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f i x y) v1 v2 + + let find2i f v1 v2 = + Array.findi (uncurry f) (Array.combine v1 v2) (* TODO: iter2i? *) + + let to_array v = v + + let of_array v = v + + let apply_with_c_with f c v = Array.modify (fun x -> f x c) v + + let rev_with v = Array.rev_in_place v + + let map_with f v = Array.modify f v + + let map2_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f x y) v1 v2 + + let copy v = Array.copy v + + let mapi_with f v = Array.iteri (fun i x -> v.(i) <- f i x) v + + let of_sparse_list col_count ls = + let vec = Array.make col_count A.zero in + List.iter (fun (idx, value) -> vec.(idx) <- value) ls; + vec + + let to_sparse_list v = + let rec aux idx acc = + if idx < 0 then acc + else + let value = v.(idx) in + let acc = if value <> A.zero then (idx, value):: acc else acc in + aux (idx - 1) acc + in aux (length v - 1) [] + end \ No newline at end of file diff --git a/src/cdomains/affineEquality/matrix.ml b/src/cdomains/affineEquality/matrix.ml new file mode 100644 index 0000000000..5460c2a230 --- /dev/null +++ b/src/cdomains/affineEquality/matrix.ml @@ -0,0 +1,49 @@ +(** High-level abstraction of a matrix. *) +module type Matrix = +sig + type num + type vec + type t [@@deriving eq, ord, hash] + + val show: t -> string + + val copy: t -> t + + val empty: unit -> t + + val is_empty: t -> bool + + val num_rows: t -> int + + val compare_num_rows: t -> t -> int + + val num_cols: t -> int + + val init_with_vec: vec -> t + + val append_row: t -> vec -> t + + val get_row: t -> int -> vec + + val remove_row: t -> int -> t + + val remove_zero_rows: t -> t + + val map2: (vec -> num -> vec) -> t -> vec -> t + + val map2i: (int -> vec-> num -> vec) -> t -> vec -> t + + val add_empty_columns: t -> int array -> t + + val set_col: t -> vec -> int -> t + + val del_cols: t -> int array -> t + + val find_opt: (vec -> bool) -> t -> vec option + + val reduce_col: t -> int -> t + + val normalize: t -> t Option.t (* Gauss-Jordan Elimination to get matrix in reduced row echelon form (rref) + deletion of zero rows. None matrix has no solution *) + + val is_covered_by: t -> t -> bool +end \ No newline at end of file diff --git a/src/cdomains/affineEquality/ratOps.ml b/src/cdomains/affineEquality/ratOps.ml new file mode 100644 index 0000000000..35ec136ba6 --- /dev/null +++ b/src/cdomains/affineEquality/ratOps.ml @@ -0,0 +1,35 @@ +(** Abstracts the functions of the Mpqf module for rationals from Apron that implements multi-precision rationals. + One could later exchange "Mpqf" with a different module that provides the functions specified by this interface. *) +module type RatOps = +sig + type t [@@deriving eq, ord, hash] + val add : t -> t -> t + val sub : t -> t -> t + val mul : t -> t -> t + val div : t -> t -> t + val neg : t -> t + val abs : t -> t + val to_string: t -> string + val of_int: int -> t + val zero: t + val one: t + val get_den: t -> Z.t + val get_num: t -> Z.t +end + +(** It provides more readable infix operators for the functions of RatOps. + It is designed to be included by modules that make use of RatOps's functions. *) +module ConvenienceOps (A: RatOps) = +struct + let ( *: ) = A.mul + let (+:) = A.add + let (-:) = A.sub + let (/:) = A.div + let (=:) x y = A.equal x y + let (<>:) x y = not (A.equal x y) + let (<:) x y = A.compare x y < 0 + let (>:) x y = A.compare x y > 0 + let (<=:) x y = A.compare x y <= 0 + let (>=:) x y = A.compare x y >= 0 + let of_int x = A.of_int x +end \ No newline at end of file diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml new file mode 100644 index 0000000000..7fe400140a --- /dev/null +++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml @@ -0,0 +1,376 @@ +open Matrix +open SparseVector +open RatOps + +open Batteries + +let timing_wrap = Vector.timing_wrap + +module type SparseMatrix = +sig + include Matrix + val get_col_upper_triangular: t -> int -> vec + + val swap_rows: t -> int -> int -> t + + val rref_vec: t -> vec -> t Option.t + + val rref_matrix: t -> t -> t Option.t +end + +module type SparseMatrixFunctor = + functor (A: RatOps) (V: SparseVectorFunctor) -> + sig + include SparseMatrix with type vec := V(A).t and type num := A.t + end + +(** Matrix implementation that uses a list of (ideally sparse) vectors representing its rows. + It provides a normalization function to reduce a matrix into reduced row echelon form. + Operations exploit that the input matrix/matrices are in reduced row echelon form already. *) +module ListMatrix: SparseMatrixFunctor = + functor (A: RatOps) (V: SparseVectorFunctor) -> + struct + include ConvenienceOps(A) + module V = V(A) + + type t = V.t list (* List of rows *) + [@@deriving eq, ord, hash] + + let show x = + List.fold_left (^) "" (List.map (fun x -> (V.show x)) x) + + let copy m = m + + let equal m1 m2 = timing_wrap "equal" (equal m1) m2 + + let copy m = + timing_wrap "copy" (copy) m + + let empty () = [] + + let is_empty = List.is_empty + + let num_rows = List.length + + let compare_num_rows = List.compare_lengths + + let num_cols m = + if m = [] then 0 else V.length (List.hd m) + + let init_with_vec v = + [v] + + let append_row m row = + m @ [row] + + let get_row = List.nth + + let remove_row m n = + List.remove_at n m + + let remove_zero_rows m = + List.filter (fun row -> not (V.is_zero_vec row)) m + + 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 map2 f m v = + let vector_length = V.length v in + let vector_entries = V.to_sparse_list v in + let rec map2_helper acc index m v = + match m, v with + | [], _ -> List.rev acc + | row :: rs, [] when index >= vector_length -> List.rev_append acc m + | row :: rs, [] -> map2_helper ((f row A.zero):: acc) (index + 1) rs [] + | row :: rs, (i, value) :: vs -> + if i = index then + map2_helper ((f row value):: acc) (index + 1) rs vs + else + map2_helper ((f row A.zero) :: acc) (index + 1) rs v + in + map2_helper [] 0 m vector_entries + + let map2 f m v = timing_wrap "Matrix.map2" (map2 f m) v + + let map2i f m v = + let vector_length = V.length v in + let vector_entries = V.to_sparse_list v in + let rec map2i_helper acc index m v = + match m, v with + | [], _ -> List.rev acc + | row :: rs, [] when index >= vector_length -> List.rev_append acc m + | row :: rs, [] -> map2i_helper ((f index row A.zero):: acc) (index + 1) rs [] + | row :: rs, (i, value) :: vs -> + if i = index then + map2i_helper ((f index row value):: acc) (index + 1) rs vs + else + map2i_helper ((f index row A.zero) :: acc) (index + 1) rs v + in + map2i_helper [] 0 m vector_entries + + let map2i f m v = timing_wrap "Matrix.map2i" (map2i f m) v + + (** + [add_empty_columns m cols] extends the matrix [m] as specified in [cols]. + @param cols An apron dimchange array as defined here: https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html . + *) + let add_empty_columns m cols = + let cols_list = Array.to_list cols in (* cols should adhere to apron specification as described here: https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html*) + (* This creates a list of tuples, each specifying an index and how many zeros are to be inserted at that index. This is then used for each row *) + let grouped_indices = List.group Int.compare cols_list in + let occ_cols = List.map (fun group -> ((List.hd group, List.length group))) grouped_indices in + List.map (fun row -> V.insert_zero_at_indices row occ_cols (Array.length cols)) m + + let add_empty_columns m cols = + timing_wrap "add_empty_cols" (add_empty_columns m) cols + + (** + [get_col_upper_triangular m n] returns the [n]th column of [m]. [m] must be in upper triangular form. + @param m A matrix in upper triangular form. + *) + let get_col_upper_triangular m n = + let rec helper acc m i = + match m with + | [] -> acc + | row :: xs -> + if i > n then + acc + else + let value = V.nth row n in if value <>: A.zero then helper ((i, value) :: acc) xs (i + 1) else helper acc xs (i + 1) + in V.of_sparse_list (num_rows m) (List.rev @@ helper [] m 0) + + let get_col_upper_triangular m n = timing_wrap "get_col" (get_col_upper_triangular m) n + + let set_col m new_col n = + map2 (fun row value -> V.set_nth row n value) m new_col + + let set_col m new_col n = timing_wrap "set_col" (set_col m) new_col n + + (** + [del_cols m cols] removes columns from [m] as specified by [c]. + @param c An apron dimchange array as defined here: https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html . + *) + let del_cols m cols = + if (Array.length cols) = num_cols m then empty() + else + let cols_list = Array.to_list cols in + List.map (fun row -> V.remove_at_indices row cols_list) m + + let del_cols m cols = timing_wrap "del_cols" (del_cols m) cols + + let find_opt = List.find_opt + + let div_row row value = + V.map_f_preserves_zero (fun a -> a /: value) row + + let sub_scaled_row row1 row2 factor = + V.map2_f_preserves_zero (fun x y -> x -: (factor *: y)) row1 row2 + + (** + [get_pivot_positions m] returns a list of tuples of row index and pivot position (column index) of all rref-pivots of [m]. + @param m A matrix in rref. + *) + let get_pivot_positions m = + List.rev @@ List.fold_lefti ( + fun acc i row -> match V.find_first_non_zero row with + | None -> acc + | Some (pivot_col, _) -> (i, pivot_col, row) :: acc + ) [] m + + let get_pivot_positions m = + timing_wrap "get_pivot_positions" get_pivot_positions m + + (** + [reduce_col m j] reduces the [j]-th column in [m] with the last row that has a non-zero element in this column. + *) + let reduce_col m j = + if is_empty m then m + else + let rec find_pivot idx entries = (* Finds non-zero element in column j and returns pair of row idx and the pivot value *) + match entries with + | [] -> None + | row :: rest -> let value = V.nth row j in + if value =: A.zero then find_pivot (idx - 1) rest else Some (idx, value) + in + match (find_pivot (num_rows m - 1) (List.rev m)) with + | None -> m (* column is already filled with zeroes *) + | Some (row_idx, pivot) -> + let pivot_row = List.nth m row_idx in (* use the pivot row to reduce all entries in column j to zero, then "delete" the pivot row *) + List.mapi (fun idx row -> + if idx = row_idx then + V.zero_vec (num_cols m) + else + let row_value = V.nth row j in + if row_value = A.zero then row + else (let s = row_value /: pivot in + sub_scaled_row row pivot_row s) + ) m + + (** + [normalize m] transforms matrix [m] into reduced row echolon form (rref). + *) + let normalize m = + let col_count = num_cols m in + let cut_front_matrix m row_idx col_idx = + List.filteri_map (fun i row -> if i < row_idx then None else Some (V.starting_from_nth row col_idx)) m + in + let cut_front_matrix m row_idx col_idx = timing_wrap "cut_front_matrix" (cut_front_matrix m row_idx) col_idx in + (* Function for finding first pivot in an extracted part of the matrix (row_idx and col_idx indicate which part of the original matrix) *) + (* The last column represents the constant in the affeq *) + let find_first_pivot m row_idx col_idx = + if col_idx >= col_count then None else + let max_piv_col_idx = num_cols m - 2 in (* col at num_cols - 1 is the constant of the affeq *) + (* Finding pivot by extracting the minimum column index of the first non zero value of each row *) + let (piv_row, piv_col, piv_val) = List.fold_lefti (fun (cur_row, cur_col, cur_val) i row -> + let row_first_non_zero = V.find_first_non_zero row in + match row_first_non_zero with + | None -> (cur_row, cur_col, cur_val) + | Some (idx, value) -> if idx < cur_col then (i, idx, value) else (cur_row, cur_col, cur_val) + ) (num_rows m, max_piv_col_idx + 1, A.zero) m + in + if piv_col = (max_piv_col_idx + 1) then None else Some (row_idx + piv_row, col_idx + piv_col, piv_val) + in + let find_first_pivot m row_idx col_idx = timing_wrap "find_first_pivot" (find_first_pivot m row_idx) col_idx 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 = + match V.find_first_non_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 + in + List.for_all row_is_valid m in + (* Finds the best fitting pivot, moves the respective row at the correct position, and reduces the pivot column afterwards. Continues with next row after that until fully normalized *) + let rec find_piv_and_reduce m m' row_idx col_idx = + if col_idx >= (col_count - 1) then m (* In this case the whole bottom of the matrix starting from row_index has been reduced to Zero, so it is normalized *) + else + match find_first_pivot m' row_idx col_idx with + | None -> m (* No pivot found means already normalized *) + | Some (piv_row_idx, piv_col_idx, piv_val) -> ( + let m = if piv_row_idx <> row_idx then swap_rows m row_idx piv_row_idx else m in + let normalized_m = List.mapi (fun idx row -> if idx = row_idx then div_row row piv_val else row) m in + let piv_row = (List.nth normalized_m row_idx) in + let subtracted_m = List.mapi (fun idx row -> if idx <> row_idx then + let scale = V.nth row piv_col_idx in + sub_scaled_row row piv_row scale else row) normalized_m in + let m' = cut_front_matrix subtracted_m (row_idx + 1) (piv_col_idx + 1) in + find_piv_and_reduce 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' = find_piv_and_reduce m m 0 0 in + if affeq_rows_are_valid m' then Some m' else None + + + let normalize m = timing_wrap "normalize" normalize m + + (** + [reduce_col_with_vec m j v] sets the [j]-th column of [m] to zero by subtracting multiples of [v] from each row. *) + let reduce_col_with_vec m j v = + let pivot_element = V.nth v j in + if pivot_element = A.zero then m + else List.mapi (fun idx row -> + let row_value = V.nth row j in + if row_value =: A.zero then row + else (let s = row_value /: pivot_element in + V.map2_f_preserves_zero (fun x y -> x -: (s *: y)) row v) + ) m + + (** + [insert_v_according_to_piv m v piv_idx pivot_position] inserts vector [v] into [m] such that rref is preserved. + @param m A matrix in rref such that [(r, piv_idx)] is not in [pivot_positions] for all [r]. + @param v A vector such that [v(piv_idx) =: A.one] and [v(c) <>: A.zero] if [(r,c)] is not in [pivot_position] for all [r]. + *) + let insert_v_according_to_piv m v piv_idx pivot_positions = + let reduced_m = reduce_col_with_vec m piv_idx v in + match List.find_opt (fun (row_idx, piv_col, _) -> piv_col > piv_idx) pivot_positions with + | None -> append_row reduced_m v + | Some (row_idx, _, _) -> + let (before, after) = List.split_at row_idx reduced_m in + before @ (v :: after) + + let insert_v_according_to_piv m v piv_idx pivot_positions = + timing_wrap "insert_v_according_to_piv" (insert_v_according_to_piv m v piv_idx) pivot_positions + + (** + [rref_vec m v] yields the same result as appending [v] to [m], then bringing [m] into rref and removing all zero rows. + + {i Faster than appending [v] to [m] and normalizing!} + @param m A matrix in rref. + @param v A vector with number of entries equal to the number of columns of [v]. + *) + let rref_vec m v = + if is_empty m then (* In this case, v is normalized and returned *) + BatOption.map (fun (_, value) -> init_with_vec @@ div_row v value) (V.find_first_non_zero v) + else (* We try to normalize v and check if a contradiction arises. If not, we insert v at the appropriate place in m (depending on the pivot) *) + let pivot_positions = get_pivot_positions m in + (* filtered_pivots are only the pivots which have a non-zero entry in the corresponding column of v. Only those are relevant to subtract from v *) + let filtered_pivots = List.rev @@ fst @@ List.fold_left (fun (res, pivs_tail) (col_idx, value) -> + let pivs_tail = List.drop_while (fun (_, piv_col, _) -> piv_col < col_idx) pivs_tail in (* Skipping until possible match of both cols *) + match pivs_tail with + | [] -> (res, []) + | (row_idx, piv_col, row) :: ps when piv_col = col_idx -> ((row_idx, piv_col, row, value) :: res, ps) + | _ -> (res, pivs_tail) + ) ([], pivot_positions) (V.to_sparse_list v) in + let v_after_elim = List.fold_left (fun acc (row_idx, pivot_position, piv_row, v_at_piv) -> + sub_scaled_row acc piv_row v_at_piv + ) v filtered_pivots in + match V.find_first_non_zero v_after_elim with (* now we check for contradictions and finally insert v *) + | None -> Some m (* v is zero vector and was therefore already covered by m *) + | Some (idx, value) -> + if idx = (num_cols m - 1) then + None + else + let normalized_v = V.map_f_preserves_zero (fun x -> x /: value) v_after_elim in + Some (insert_v_according_to_piv m normalized_v idx pivot_positions) + + let rref_vec m v = timing_wrap "rref_vec" (rref_vec m) v + + (** [rref_matrix m m'] yields the same result as appending [m'] to [m], then bringing the resulting matrix into rref and removing all zero rows. + + {i Faster than appending [m'] to [m] and then normalizing!} + @param m A matrix in rref. + @param m' A matrix in rref. + *) + let rref_matrix m1 m2 = + let big_m, small_m = if compare_num_rows m1 m2 > 0 then m1, m2 else m2, m1 in + fst @@ List.fold_while (fun acc _ -> Option.is_some acc) + (fun acc_big_m small -> rref_vec (Option.get acc_big_m) small ) (Some big_m) small_m + + let rref_matrix m1 m2 = timing_wrap "rref_matrix" (rref_matrix m1) m2 + + (** + [is_coverd_by m m'] returns [true] iff every vector in [m] is a linear combination of vectors in [m']. + @param m A matrix in rref. + @param m' A matrix in rref. + *) + let is_covered_by m1 m2 = + let rec is_linearly_independent_rref v m = + let pivot_opt = V.find_first_non_zero v in + match pivot_opt with + | None -> false (* When we found no pivot, the vector is already A.zero. *) + | Some (pivot_id, pivot) -> + let m' = List.drop_while (fun v2 -> + match V.find_first_non_zero v2 with + | None -> true (* In this case, m2 only has zero rows after that *) + | Some (idx', _) -> idx' < pivot_id + ) m in + match m' with + | [] -> not @@ V.is_zero_vec v + | x::xs -> + let new_v = V.map2_f_preserves_zero (fun v1 v2 -> v1 -: (pivot *: v2)) v x in + is_linearly_independent_rref new_v m' + in + if compare_num_rows m1 m2 > 0 then false else + let rec is_covered_by_helper m1 m2 = + match m1 with + | [] -> true + | v1::vs1 -> + let first_non_zero = V.find_first_non_zero v1 in + match first_non_zero with + | None -> true (* vs1 must also be zero-vectors because of rref *) + | Some (idx, _) -> + let linearly_indep = is_linearly_independent_rref v1 m2 in + if linearly_indep then false else is_covered_by_helper vs1 m2 + in is_covered_by_helper m1 m2 + + let is_covered_by m1 m2 = timing_wrap "is_covered_by" (is_covered_by m1) m2 + + end diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml new file mode 100644 index 0000000000..88879e21de --- /dev/null +++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml @@ -0,0 +1,326 @@ +open Vector +open RatOps + +open Batteries + +module type SparseVector = +sig + include Vector + val is_zero_vec: t -> bool + + val insert_zero_at_indices: t -> (int * int) list -> int -> t + + val remove_at_indices: t -> int list -> t + + (* Returns the part of the vector starting from index n*) + val starting_from_nth : t -> int -> t + + val find_first_non_zero : t -> (int * num) option + + val map_f_preserves_zero: (num -> num) -> t -> t + + val mapi_f_preserves_zero: (int -> num -> num) -> t -> t + + val map2_f_preserves_zero: (num -> num -> num) -> t -> t -> t + + val find2i_f_false_at_zero: (num -> num -> bool) -> t -> t -> int + + val apply_with_c_f_preserves_zero: (num -> num -> num) -> num -> t -> t +end + +module type SparseVectorFunctor = + functor (A: RatOps) -> + sig + include SparseVector with type num:= A.t + end + +module SparseVector: SparseVectorFunctor = + functor (A: RatOps) -> + struct + include ConvenienceOps (A) + + (** Only non-zero [entries] are stored in a list of tuples of (index, value). All values not contained in [entries] are implicitly [A.Zero]. *) + type t = { + entries: (int * A.t) list ; + len: int + }[@@deriving eq, ord, hash] + + let copy v = v + + (** [of_list l] returns a vector constructed from the non-sparse list [l] *) + let of_list l = + let entries = List.filteri_map (fun i x -> if x <> A.zero then Some (i, x) else None) l in + let len = List.length l in + {entries; len} + + (** [of_array a] returns a vector constructed from the non-sparse array [a] *) + let of_array a = + let entries = Array.fold_righti (fun i x acc -> if x <> A.zero then (i, x) :: acc else acc ) a [] in + let len = Array.length a in + {entries; len} + + (** [of_sparse_list len entries] returns a vector of length [len] constructed from the sorted sparse list [entries]. + A sparse list is a list of tuples of the form [(i, value)] which represent that the vector has an entry [value] at index [i]. + All non-specified entries are assumed to be [Zero]. The sparse list has to be sorted by the index [i]. + *) + let of_sparse_list len entries = + {entries; len} + + (** [to_list v] returns a non-sparse list representing the vector v *) + let to_list v = + let rec extend_zero_aux i acc = function + | (index, value) :: xs when index = i -> extend_zero_aux (i + 1) (value :: acc) xs + | ((_:: _) as v) -> extend_zero_aux (i + 1) (A.zero :: acc) v + | [] -> if i < v.len then extend_zero_aux (i + 1) (A.zero :: acc) [] else List.rev acc + in + extend_zero_aux 0 [] v.entries + + let to_array v = + let vec = Array.make v.len A.zero in + List.iter (fun (idx, value) -> vec.(idx) <- value) v.entries; + vec + + let to_sparse_list v = + v.entries + + let show v = + let rec sparse_list_str i l = + if i >= v.len then "]" + else match l with + | [] -> (A.to_string A.zero) ^" "^ (sparse_list_str (i + 1) l) + | (idx, value) :: xs -> + if i = idx then (A.to_string value) ^" "^ sparse_list_str (i + 1) xs + else (A.to_string A.zero) ^" "^ sparse_list_str (i + 1) l + in + "["^(sparse_list_str 0 v.entries)^"\n" + + let length v = + v.len + + let compare_length_with v n = + Int.compare v.len n + + let zero_vec len = + {entries = []; len} + + let is_zero_vec v = (v.entries = []) + + (** + [is_const_vec v] returns true if the v can be interpreted as an expression with one variable and possibly a constant, i.e. x_i + c + *) + let is_const_vec v = + match v.entries with + | [] -> false + | (idx, _) :: (const_idx , _) :: [] when const_idx = (v.len - 1) -> true + | (idx, _)::[] when idx <> v.len -1 -> true + | _ -> false + + (** + [nth v n] returns the [n]-th entry of [v]. + @raise Invalid_argument if [n] is 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 "Index out of bounds") + else + match List.find_opt (fun (idx, _) -> idx >= n) v.entries with + | Some (idx, value) when idx = n -> value + | _ -> A.zero + + (** + [set_nth v n num] returns [v] where the [n]-th entry has been set to [num]. + @raise Invalid_argument if [n] is out of bounds. + *) + let set_nth v n num = + if n >= v.len then raise (Invalid_argument "Index out of bounds") + else + let rec set_nth_helper vec acc = + match vec with + | [] -> if num <>: A.zero then List.rev ((n, num) :: acc) else List.rev acc + | (idx, value) :: xs when n = idx -> if num <>: A.zero then List.rev_append ((idx, num) :: acc) xs else List.rev_append acc xs + | (idx, value) :: xs when n < idx -> if num <>: A.zero then List.rev_append ((n, num) :: acc) vec else List.rev_append acc vec + | x :: xs -> set_nth_helper xs (x :: acc) + in + {v with entries = set_nth_helper v.entries []} + + (** + [insert_zero_at_indices v indices num_zeros] inserts [num_zeros] into [v]. + @param indices A {b sorted} list of tuples where [fst] gives the index of the insert and [snd] the number of zeros that will be inserted. + *) + let insert_zero_at_indices v indices num_zeros = + let rec add_indices_helper vec cur_idx added_count acc = + match vec, cur_idx with + | [], _ -> List.rev acc (* inserting at the end only means changing the dimension *) + | (idx, value) :: xs, [] -> add_indices_helper xs [] added_count ((idx + added_count, value) :: acc) + | (idx, _) :: _, ((i, count) :: ys) when i <= idx -> add_indices_helper vec ys (added_count + count) acc + | (idx, value) :: xs, ((i, count) :: ys) -> add_indices_helper xs cur_idx added_count ((idx + added_count, value) :: acc) + in + {entries = add_indices_helper v.entries indices 0 []; len = v.len + num_zeros} + + (** + [remove_nth v n] returns [v] where the [n]-th entry is removed, decreasing the length of the vector by one. + @raise Invalid_argument if [n] is out of bounds + *) + let remove_nth v n = + if n >= v.len then raise (Invalid_argument "Index out of bounds") + else + let entries = List.filter_map (fun (idx, value) -> + if idx = n then None + else if idx > n + then Some (idx - 1, value) + else Some (idx, value) + ) v.entries in + {entries; len = v.len - 1} + + (** + [remove_at_indices v indices] returns [v] where all entries at the positions specified by [indices] are removed, decreasing its length by the length of [indices]. + @param indices A {b sorted} list of indices + @raise Invalid_argument if [indices] would reach out of bounds for some index. + *) + let remove_at_indices v indices = + let rec remove_indices_helper vec cur_idx deleted_count acc = + match vec, cur_idx with + | [], [] -> List.rev acc + | [], (y :: ys) when deleted_count >= v.len || y >= v.len -> raise (Invalid_argument "Indices out of bounds") + | [], (y :: ys) -> remove_indices_helper [] ys (deleted_count + 1) acc + | (idx, value) :: xs, [] -> remove_indices_helper xs [] deleted_count ((idx - deleted_count, value) :: acc) + | (idx, _) :: xs, (y :: ys) when y = idx -> remove_indices_helper xs ys (deleted_count + 1) acc + | (idx, _) :: xs, (y :: ys) when y < idx -> remove_indices_helper vec ys (deleted_count + 1) acc + | (idx, value) :: xs, (y :: ys) -> remove_indices_helper xs cur_idx deleted_count ((idx - deleted_count, value) :: acc) + in + {entries = remove_indices_helper v.entries indices 0 []; len = v.len - List.length indices} + + (** [keep_vals v n] returns returns a vector only containing the first [n] elements of [v] *) + let keep_vals v n = + if n >= v.len then v else + {entries = List.take_while (fun (idx, _) -> idx < n) v.entries; len=n} + + (** [starting_from_nth v n] returns a vector only containing the elements after the [n]th *) + let starting_from_nth v n = + let entries = List.filter_map (fun (idx, value) -> if idx < n then None else Some (idx - n, value)) v.entries in + {entries; len = v.len - n} + + (** + [find2i_f_false_at_zero f v v'] returns the {b index} of the first pair of entries [e, e'] from [v, v'] where [f e e' = true ]. + + Note that [f] {b must} be such that [f 0 0 = false]! + *) + let find2i_f_false_at_zero f v v' = (*Very welcome to change the name*) + let rec aux v1 v2 = + match v1, v2 with + | [], [] -> raise Not_found + | [], (yidx, yval)::ys -> if f A.zero yval then yidx else aux [] ys + | (xidx, xval) :: xs, [] -> if f xval A.zero then xidx else aux xs [] + | (xidx, xval) :: xs, (yidx, yval) :: ys -> + match xidx - yidx with + | d when d < 0 -> if f xval A.zero then xidx else aux xs v2 + | d when d > 0 -> if f A.zero yval then yidx else aux v1 ys + | _ -> if f xval yval then xidx else aux xs ys + in + if v.len <> v'.len then raise (Invalid_argument "Unequal lengths") else + aux v.entries v'.entries + + (** + [find_first_non_zero v] returns the first entry [e] and its index where [e <>: 0], if such an entry exists. + @return [(idx, e) option] + *) + let find_first_non_zero v = + match v.entries with + | [] -> None + | x :: _ -> Some x + + let find_first_non_zero v = timing_wrap "find_first_non_zero" (find_first_non_zero) v + + (** + [map_f_preserves_zero f v] returns the mapping of [v] specified by [f]. + + Note that [f] {b must} be such that [f 0 = 0]! + + *) + let map_f_preserves_zero f v = (* map for functions f such that f 0 = 0 since f won't be applied to zero values. See also map *) + let entries' = List.filter_map ( + fun (idx, value) -> let new_val = f value in + if new_val = A.zero then None else Some (idx, new_val)) v.entries in + {v with entries = entries'} + + let map_f_preserves_zero f v = timing_wrap "map_f_preserves_zero" (map_f_preserves_zero f) v + + (** + [mapi_f_preserves_zero f v] returns the mapping of [v] specified by [f]. + + Note that [f] {b must} be such that [f i 0 = 0] for any index [i]! + + *) + let mapi_f_preserves_zero f v = + let entries' = List.filter_map ( + fun (idx, value) -> let new_val = f idx value in + if new_val = A.zero then None else Some (idx, new_val)) v.entries in + {v with entries = entries'} + + (** + [map2_f_preserves_zero f v v'] returns the mapping of [v] and [v'] specified by [f]. + + Note that [f] {b must} be such that [f 0 0 = 0]! + + @raise Invalid_argument if [v] and [v'] have unequal lengths + *) + let map2_f_preserves_zero f v v' = + let f_rem_zero acc idx e1 e2 = + let r = f e1 e2 in + if r =: A.zero then acc else (idx, r) :: acc + in + let rec aux acc v1 v2 = + match v1, v2 with + | [], [] -> acc + | [], (yidx, yval) :: ys -> aux (f_rem_zero acc yidx A.zero yval) [] ys + | (xidx, xval) :: xs, [] -> aux (f_rem_zero acc xidx xval A.zero) xs [] + | (xidx, xval) :: xs, (yidx, yval) :: ys -> + match xidx - yidx with + | d when d < 0 -> aux (f_rem_zero acc xidx xval A.zero) xs v2 + | d when d > 0 -> aux (f_rem_zero acc yidx A.zero yval) v1 ys + | _ -> aux (f_rem_zero acc xidx xval yval) xs ys + in + if v.len <> v'.len then raise (Invalid_argument "Unequal lengths") else + {v with entries = List.rev (aux [] v.entries v'.entries)} + + let map2_f_preserves_zero f v1 v2 = timing_wrap "map2_f_preserves_zero" (map2_f_preserves_zero f v1) v2 + + (** + @raise Invalid_argument if [v] and [v'] have unequal lengths + *) + let map2i f v v' = (*might more memory efficient, but definitly not faster (asymptotically)*) + if v.len <> v'.len then raise (Invalid_argument "Unequal lengths") else + let f_rem_zero idx acc e1 e2 = + let r = f idx e1 e2 in + if r =: A.zero then acc else (idx, r) :: acc + in + let rec aux acc vec1 vec2 i = + match vec1, vec2 with + | [], [] when i = v.len -> acc + | [], [] -> aux (f_rem_zero i acc A.zero A.zero) [] [] (i + 1) + | [], (yidx, yval) :: ys when i = yidx -> aux (f_rem_zero i acc A.zero yval) [] ys (i + 1) + | (xidx, xval) :: xs, [] when i = xidx -> aux (f_rem_zero i acc xval A.zero) xs [] (i + 1) + | [], (_, _) :: _ | (_, _) :: _, [] -> aux (f_rem_zero i acc A.zero A.zero) vec1 vec2 (i + 1) (* When one vec is not zero_vec, but has implicit zeroes at front *) + | (xidx, xval)::xs, (yidx, yval)::ys -> + if xidx <> i && yidx <> i then aux (f_rem_zero i acc A.zero A.zero) vec1 vec2 (i+1) (* When both vectors have implicit zeroes at front *) + else + match xidx - yidx with (* Here at least one of the idx is i, which is the smaller one *) + | d when d < 0 -> aux (f_rem_zero i acc xval A.zero) xs vec2 (i + 1) + | d when d > 0 -> aux (f_rem_zero i acc A.zero yval) vec1 ys (i + 1) + | _ -> aux (f_rem_zero i acc xval yval) xs ys (i + 1) + in + {v with entries = List.rev (aux [] v.entries v'.entries 0)} + + (** + [apply_with_c_f_preserves_zero f c v] returns the mapping of [v] and [c] specified by [f]. + + Note that [f] {b must} be such that [f 0 c = 0]! + *) + let apply_with_c_f_preserves_zero f c v = + let entries = List.filter_map (fun (idx, value) -> let new_val = f value c in if new_val =: A.zero then None else Some (idx, new_val)) v.entries in + {entries; len = v.len} + + let rev v = + let entries = List.rev_map (fun (idx, value) -> (v.len - 1 - idx, value)) v.entries in + {entries; len = v.len} + + end diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml new file mode 100644 index 0000000000..32e78f8b5b --- /dev/null +++ b/src/cdomains/affineEquality/vector.ml @@ -0,0 +1,47 @@ +(** High-level abstraction of a vector. *) +module type Vector = +sig + type num + type t [@@deriving eq, ord, hash] + + val show: t -> string + + val copy: t -> t + + val of_list: num list -> t + + val of_array: num array -> t + + val of_sparse_list: int -> (int * num) list -> t + + val to_list: t -> num list + + val to_array: t -> num array + + val to_sparse_list: t -> (int * num) list + + val length: t -> int + + val compare_length_with: t -> int -> int + + val zero_vec: int -> t + + val is_const_vec: t -> bool + + val nth: t -> int -> num + + val set_nth: t -> int -> num -> t + + val remove_nth: t -> int -> t + + val keep_vals: t -> int -> t + + val map2i: (int -> num -> num -> num) -> t -> t -> t + + val rev: t -> t +end + +(*let timing_wrap = Timing.wrap*) +(* Disable timing of the vector and matrix implementations and AffineEqualityDomain as well as SharedFunctions. + This is cleaner than a timing functor because the timed functions also call each other. *) +let timing_wrap _ f x = f x \ No newline at end of file diff --git a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml new file mode 100644 index 0000000000..dc48e805ad --- /dev/null +++ b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml @@ -0,0 +1,607 @@ +(** OCaml implementation of the affine equalities domain. + + @see Karr, M. Affine relationships among variables of a program. *) + +(** There are two versions of the AffineEqualityDomain. + This version here is based on a dense implementation that is not purely functional, thus it uses Matrix and Vector functions marked with "_with". + Abstract states in the newly added domain are represented by structs containing a matrix and an apron environment. + Matrices are modeled as proposed by Karr: Each variable is assigned to a column and each row represents a linear affine relationship that must hold at the corresponding program point. + The apron environment is hereby used to organize the order of columns and variables. *) + +open GoblintCil +open Pretty +module M = Messages +open GobApron + +open ArrayVector +open ArrayMatrix + +open Batteries + +module Mpqf = SharedFunctions.Mpqf + +module AffineEqualityMatrix (Vec: ArrayVectorFunctor) (Mx: ArrayMatrixFunctor) = +struct + include Mx(Mpqf) (Vec) + let dim_add (ch: Apron.Dim.change) m = + Array.modifyi (+) ch.dim; + add_empty_columns m ch.dim + + let dim_add ch m = timing_wrap "dim add" (dim_add ch) m + + + let dim_remove (ch: Apron.Dim.change) m ~del = + 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_with y x; y) m ch.dim else m 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 +end + +(** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars. + Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *) +module VarManagement (Vec: ArrayVectorFunctor) (Mx: ArrayMatrixFunctor)= +struct + module Vector = Vec (Mpqf) + module Matrix = AffineEqualityMatrix (Vec) (Mx) + + let dim_add = Matrix.dim_add + + include SharedFunctions.VarManagementOps(AffineEqualityMatrix (Vec) (Mx)) + include RatOps.ConvenienceOps(Mpqf) + + (** Get the constant from the vector if it is a constant *) + let to_constant_opt v = match Vector.findi ((<>:) Mpqf.zero) v with + | exception Not_found -> Some Mpqf.zero + | i when Vector.compare_length_with v (i + 1) = 0 -> Some (Vector.nth v i) + | _ -> None + + let get_coeff_vec (t: t) texp = + (*Parses a Texpr to obtain a coefficient + const (last entry) vector to repr. an affine relation. + Returns None if the expression is not affine*) + 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 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 + let rec convert_texpr = function + (*If x is a constant, replace it with its const. val. immediately*) + | Cst x -> + let of_union = function + | Coeff.Interval _ -> failwith "Not a constant" + | Scalar Float x -> Mpqf.of_float x + | Scalar Mpqf x -> x + | Scalar Mpfrf x -> Mpfr.to_mpq x + in + Vector.set_nth 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_nth_with v (Environment.dim_of_var t.env x) Mpqf.one; v 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_nth_with zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)); zero_vec_cp + | _ -> entry_only zero_vec_cp + end + | None -> entry_only zero_vec_cp end + | Unop (Neg, e, _, _) -> neg @@ convert_texpr e + | Unop (Cast, e, _, _) -> convert_texpr e (*Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts*) + | Unop (Sqrt, e, _, _) -> raise NotLinear + | Binop (Add, e1, e2, _, _) -> + let v1 = convert_texpr e1 in + let v2 = convert_texpr e2 in + Vector.map2_with (+:) v1 v2; v1 + | Binop (Sub, e1, e2, _, _) -> + let v1 = convert_texpr e1 in + let v2 = convert_texpr e2 in + Vector.map2_with (+:) v1 (neg @@ v2); v1 + | 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 + | _, _ -> raise NotLinear + end + | Binop _ -> raise NotLinear + in + try + Some (convert_texpr texp) + with NotLinear -> None + + let get_coeff_vec t texp = timing_wrap "coeff_vec" (get_coeff_vec t) texp +end + +(** As it is specifically used for the new affine equality domain, it can only provide bounds if the expression contains known constants only and in that case, min and max are the same. *) +module ExpressionBounds (Vc: ArrayVectorFunctor) (Mx: ArrayMatrixFunctor): (SharedFunctions.ConvBounds with type t = VarManagement(Vc) (Mx).t) = +struct + include VarManagement (Vc) (Mx) + + let bound_texpr t texpr = + let texpr = Texpr1.to_expr texpr in + match Option.bind (get_coeff_vec t texpr) to_constant_opt with + | Some c when Mpqf.get_den c = Z.one -> + let int_val = Mpqf.get_num c in + Some int_val, Some int_val + | _ -> None, None + + + let bound_texpr d texpr1 = + let res = bound_texpr d texpr1 in + (if M.tracing then + match res with + | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pretty min GobZ.pretty max + | _ -> () + ); + res + + + let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 +end + +module D(Vc: ArrayVectorFunctor) (Mx: ArrayMatrixFunctor) = +struct + include Printable.Std + include RatOps.ConvenienceOps (Mpqf) + include VarManagement (Vc) (Mx) + + module Bounds = ExpressionBounds (Vc) (Mx) + module V = RelationDomain.V + module Arg = struct + let allow_global = true + end + module Convert = SharedFunctions.Convert (V) (Bounds) (Arg) (SharedFunctions.Tracked) + + + type var = V.t + + let show t = + let conv_to_ints row = + let row = Array.copy @@ Vector.to_array row in + let mpqf_of_z x = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z x in + let lcm = mpqf_of_z @@ Array.fold_left (fun x y -> Z.lcm x (Mpqf.get_den y)) Z.one row in + Array.modify (( *:) lcm) row; + let int_arr = Array.map Mpqf.get_num row in + let div = Array.fold_left Z.gcd int_arr.(0) int_arr in + Array.modify (fun x -> Z.div x div) int_arr; + int_arr + in + let vec_to_constraint arr env = + let vars, _ = Environment.vars env in + let dim_to_str var = + let coeff = arr.(Environment.dim_of_var env var) in + if Z.equal coeff Z.zero then + "" + else + let coeff_str = + if Z.equal coeff Z.one then "+" + else if Z.equal coeff Z.minus_one then "-" + else if Z.lt coeff Z.minus_one then Z.to_string coeff + else Format.asprintf "+%s" (Z.to_string coeff) + in + coeff_str ^ Var.show var + in + let const_to_str vl = + if Z.equal vl Z.zero then + "" + else + let negated = Z.neg vl in + if Z.gt negated Z.zero then "+" ^ Z.to_string negated + else Z.to_string negated + in + let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars) + ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in + if Stdlib.String.starts_with res ~prefix:"+" then + Str.string_after res 1 + else + res + in + match t.d with + | None -> "Bottom Env" + | Some m when Matrix.is_empty m -> "⊤" + | Some m -> + let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env) in + "[|"^ (String.concat "; " constraint_list) ^"|]" + + let pretty () (x:t) = text (show x) + let printXml f x = BatPrintf.fprintf f "\n\n\nmatrix\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (show x)) Environment.printXml x.env + let eval_interval ask = Bounds.bound_texpr + + let name () = "affeq" + + let to_yojson _ = failwith "ToDo Implement in future" + + + let is_bot t = equal t (bot ()) + + let bot_env = {d = None; env = Environment.make [||] [||]} + + let is_bot_env t = t.d = None + + let top () = {d = Some (Matrix.empty ()); env = Environment.make [||] [||]} + + let is_top t = Environment.equal empty_env t.env && GobOption.exists Matrix.is_empty t.d + + let is_top_env t = (not @@ Environment.equal empty_env t.env) && GobOption.exists Matrix.is_empty t.d + + let meet t1 t2 = + let sup_env = Environment.lce t1.env t2.env in + + let t1, t2 = change_d t1 sup_env ~add:true ~del:false, change_d t2 sup_env ~add:true ~del:false in + if is_bot t1 || is_bot t2 then + bot () + else + (* TODO: Why can I be sure that m1 && m2 are all Some here? + Answer: because is_bot checks if t1.d is None and we checked is_bot before. *) + let m1, m2 = Option.get t1.d, Option.get t2.d in + if is_top_env t1 then + {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env} + else if is_top_env t2 then + {d = Some (dim_add (Environment.dimchange t1.env sup_env) m1); env = sup_env} + else + let rref_matr = Matrix.rref_matrix_with (Matrix.copy m1) (Matrix.copy m2) in + if Option.is_none rref_matr then + bot () + else + {d = rref_matr; env = sup_env} + + + let meet t1 t2 = + let res = meet t1 t2 in + if M.tracing then M.tracel "meet" "meet a: %s b: %s -> %s " (show t1) (show t2) (show res) ; + res + + let meet t1 t2 = timing_wrap "meet" (meet t1) t2 + + let leq t1 t2 = + let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *) + if env_comp = -2 || env_comp > 0 then + (* -2: environments are not compatible (a variable has different types in the 2 environements *) + (* -1: if env1 is a subset of env2, (OK) *) + (* 0: if equality, (OK) *) + (* +1: if env1 is a superset of env2, and +2 otherwise (the lce exists and is a strict superset of both) *) + false + else if is_bot t1 || is_top_env t2 then + true + else if is_bot t2 || is_top_env t1 then + false + else + let m1, m2 = Option.get t1.d, Option.get t2.d in + let m1' = if env_comp = 0 then m1 else dim_add (Environment.dimchange t1.env t2.env) m1 in + Matrix.is_covered_by m2 m1' + + let leq a b = timing_wrap "leq" (leq a) b + + let leq t1 t2 = + let res = leq t1 t2 in + if M.tracing then M.tracel "leq" "leq a: %s b: %s -> %b " (show t1) (show t2) res ; + res + + let join a b = + let rec lin_disjunc r s a b = + if s >= Matrix.num_cols a then a else + let case_two a r col_b = + let a_r = Matrix.get_row a r in + Matrix.map2i_with (fun i x y -> if i < r then + Vector.map2_with (fun u j -> u +: y *: j) x a_r; x) a col_b; + Matrix.remove_row a r + in + let case_three a b col_a col_b max = + let col_a, col_b = Vector.copy col_a, Vector.copy col_b in + let col_a, col_b = Vector.keep_vals col_a max, Vector.keep_vals col_b max in + if Vector.equal col_a col_b then + (a, b, max) + else + ( + Vector.rev_with col_a; + Vector.rev_with col_b; + 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 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 + in + Matrix.remove_row (multiply_by_t a a_r) r, Matrix.remove_row (multiply_by_t b b_r) r, (max - 1) + ) + in + let col_a, col_b = Matrix.get_col a s, Matrix.get_col b s in + let nth_zero v i = match Vector.nth v i with + | exception Invalid_argument _ -> Mpqf.zero + | x -> x + in + let a_rs, b_rs = nth_zero col_a r, nth_zero col_b r in + if not (Z.equal (Mpqf.get_den a_rs) Z.one) || not (Z.equal (Mpqf.get_den b_rs) Z.one) then failwith "Matrix not in rref form" else + begin match Int.of_float @@ Mpqf.to_float @@ a_rs, Int.of_float @@ Mpqf.to_float @@ b_rs with (* TODO: is it safe to go through floats? *) + | 1, 1 -> lin_disjunc (r + 1) (s + 1) a b + | 1, 0 -> lin_disjunc r (s + 1) (case_two a r col_b) b + | 0, 1 -> lin_disjunc r (s + 1) a (case_two b r col_a) + | 0, 0 -> let new_a, new_b, new_r = case_three a b col_a col_b r in + lin_disjunc new_r (s + 1) new_a new_b + | _ -> failwith "Matrix not in rref form" end + in + if is_bot a then + b + else if is_bot b then + a + else + match Option.get a.d, Option.get b.d with + | x, y when is_top_env a || is_top_env b -> {d = Some (Matrix.empty ()); env = Environment.lce a.env b.env} + | x, y when (Environment.cmp a.env b.env <> 0) -> + let sup_env = Environment.lce a.env b.env in + let mod_x = dim_add (Environment.dimchange a.env sup_env) x in + let mod_y = dim_add (Environment.dimchange b.env sup_env) y in + {d = Some (lin_disjunc 0 0 (Matrix.copy mod_x) (Matrix.copy mod_y)); env = sup_env} + | x, y when Matrix.equal x y -> {d = Some x; env = a.env} + | x, y -> {d = Some(lin_disjunc 0 0 (Matrix.copy x) (Matrix.copy y)); env = a.env} + + let join a b = timing_wrap "join" (join a) b + + let join a b = + let res = join a b in + if M.tracing then M.tracel "join" "join a: %s b: %s -> %s " (show a) (show b) (show res) ; + res + + let widen a b = + if Environment.equal a.env b.env then + join a b + else + b + + let narrow a b = a + + let pretty_diff () (x, y) = + dprintf "%s: %a not leq %a" (name ()) pretty x pretty y + + let remove_rels_with_var x var env inplace = + let j0 = Environment.dim_of_var env var in + if inplace then + (Matrix.reduce_col_with x j0; x) + else + Matrix.reduce_col x j0 + + let remove_rels_with_var x var env inplace = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) inplace + + let forget_vars t vars = + if is_bot t || is_top_env t || vars = [] then + t + else + let m = Option.get t.d in + let rem_from m = List.fold_left (fun m' x -> remove_rels_with_var m' x t.env true) m vars in + {d = Some (Matrix.remove_zero_rows @@ rem_from (Matrix.copy m)); env = t.env} + + let forget_vars t vars = + let res = forget_vars t vars in + if M.tracing then M.tracel "ops" "forget_vars %s -> %s" (show t) (show res); + res + + let forget_vars t vars = timing_wrap "forget_vars" (forget_vars t) vars + + let assign_texpr (t: VarManagement(Vc)(Mx).t) var texp = + let assign_invertible_rels x var b env = + let j0 = Environment.dim_of_var env var in + let a_j0 = Matrix.get_col x j0 in (*Corresponds to Axj0*) + let b0 = Vector.nth b j0 in + Vector.apply_with_c_with (/:) b0 a_j0; (*Corresponds to Axj0/Bj0*) + let recalc_entries m rd_a = Matrix.map2_with (fun x y -> Vector.map2i_with (fun j z d -> + if j = j0 then y + else if Vector.compare_length_with b (j + 1) > 0 then z -: y *: d + else z +: y *: d) x b; x) m rd_a + in + recalc_entries x a_j0; + if Matrix.normalize_with x then {d = Some x; env = env} else bot () + in + let assign_invertible_rels x var b env = timing_wrap "assign_invertible" (assign_invertible_rels x var b) env in + let assign_uninvertible_rel x var b env = + let b_length = Vector.length b in + Vector.mapi_with (fun i z -> if i < b_length - 1 then Mpqf.neg z else z) b; + Vector.set_nth_with b (Environment.dim_of_var env var) Mpqf.one; + let opt_m = Matrix.rref_vec_with x b in + if Option.is_none opt_m then bot () else + {d = opt_m; env = env} + 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 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 + | Some v -> if is_invertible v then let t' = assign_invertible_rels (Matrix.copy m) var v t.env in {d = t'.d; env = t'.env} + else let new_m = Matrix.remove_zero_rows @@ remove_rels_with_var m var t.env false + in assign_uninvertible_rel new_m var v t.env + | None -> {d = Some (Matrix.remove_zero_rows @@ remove_rels_with_var m var t.env false); env = t.env} + + let assign_texpr t var texp = timing_wrap "assign_texpr" (assign_texpr t var) texp + + let assign_exp ask (t: VarManagement(Vc)(Mx).t) var exp (no_ov: bool Lazy.t) = + let t = if not @@ Environment.mem_var t.env var then add_vars t [var] else t in + (* TODO: Do we need to do a constant folding here? It happens for texpr1_of_cil_exp *) + match Convert.texpr1_expr_of_cil_exp ask t t.env exp no_ov with + | exp -> assign_texpr t var exp + | exception Convert.Unsupported_CilExp _ -> + if is_bot t then t else forget_vars t [var] + + let assign_exp ask t var exp no_ov = + let res = assign_exp ask t var exp no_ov in + if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s" + (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res); + res + + let assign_var (t: VarManagement(Vc)(Mx).t) v v' = + let t = add_vars t [v; v'] in + let texpr1 = Texpr1.of_expr (t.env) (Var v') in + assign_texpr t v (Apron.Texpr1.to_expr texpr1) + + let assign_var t v v' = + let res = assign_var t v v' in + if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res); + res + + let assign_var_parallel t vv's = + 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 + match multi_t.d with + | Some m when not @@ is_top_env multi_t -> + 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_with 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 res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars ~del:true in + let x = Option.get res.d in + if Matrix.normalize_with x then + {d = Some x; env = res.env} + else + bot () + | _ -> t + + let assign_var_parallel t vv's = + let res = assign_var_parallel t vv's in + if M.tracing then M.tracel "ops" "assign_var parallel: %s -> %s " (show t) (show res); + res + + let assign_var_parallel t vv's = timing_wrap "var_parallel" (assign_var_parallel t) vv's + + let assign_var_parallel_with t vv's = + let t' = assign_var_parallel t vv's in + t.d <- t'.d; + t.env <- t'.env + + let assign_var_parallel_with t vv's = + if M.tracing then M.tracel "var_parallel" "assign_var parallel'"; + assign_var_parallel_with t vv's + + let assign_var_parallel' t vs1 vs2 = + let vv's = List.combine vs1 vs2 in + assign_var_parallel t vv's + + let assign_var_parallel' t vv's = + let res = assign_var_parallel' t vv's in + if M.tracing then M.tracel "ops" "assign_var parallel'"; + res + + let substitute_exp ask t var exp no_ov = + let t = if not @@ Environment.mem_var t.env var then add_vars t [var] else t in + let res = assign_exp ask t var exp no_ov in + forget_vars res [var] + + let substitute_exp ask t var exp no_ov = + let res = substitute_exp ask t var exp no_ov in + if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res); + res + + let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov + + (** Assert a constraint expression. + + The overflow is completely handled by the flag "no_ov", + which is set in relationAnalysis.ml via the function no_overflow. + In case of a potential overflow, "no_ov" is set to false + and Convert.tcons1_of_cil_exp will raise the exception Unsupported_CilExp Overflow *) + + let meet_tcons ask t tcons expr = + let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in + let meet_vec e = + (* Flip the sign of the const. val in coeff vec *) + let coeff = Vector.nth e (Vector.length e - 1) in + Vector.set_nth_with e (Vector.length e - 1) (Mpqf.neg coeff); + if is_bot t then + bot () + else + let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in + if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} + + in + match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with + | Some v -> + begin match to_constant_opt v, Tcons1.get_typ tcons with + | Some c, DISEQ -> check_const (=:) c + | Some c, SUP -> check_const (<=:) c + | Some c, EQ -> check_const (<>:) c + | Some c, SUPEQ -> check_const (<:) c + | None, DISEQ + | None, SUP -> + if equal (meet_vec v) t then + bot_env + else + t + | None, EQ -> + let res = meet_vec v in + if is_bot res then + bot_env + else + res + | _ -> t + end + | None -> t + + let meet_tcons t tcons expr = timing_wrap "meet_tcons" (meet_tcons t tcons) expr + + let unify a b = + meet a b + + let unify a b = + let res = unify a b in + if M.tracing then M.tracel "ops" "unify: %s %s -> %s" (show a) (show b) (show res); + res + + let assert_constraint ask d e negate no_ov = + if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" d_exp e (Lazy.force no_ov); + match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with + | tcons1 -> meet_tcons ask d tcons1 e + | exception Convert.Unsupported_CilExp _ -> d + + let assert_constraint ask d e negate no_ov = timing_wrap "assert_constraint" (assert_constraint ask d e negate) no_ov + + let relift t = t + + let invariant t = + let invariant m = + let one_constraint i = + let row = Matrix.get_row m i in + let coeff_vars = List.map (fun x -> Coeff.s_of_mpqf @@ Vector.nth row (Environment.dim_of_var t.env x), x) (vars t) in + let cst = Coeff.s_of_mpqf @@ Vector.nth row (Vector.length row - 1) in + let e1 = Linexpr1.make t.env in + Linexpr1.set_list e1 coeff_vars (Some cst); + Lincons1.make e1 EQ + in + List.init (Matrix.num_rows m) one_constraint + in + BatOption.map_default invariant [] t.d + + let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1 + + let env t = t.env + + type marshal = t + + let marshal t = t + + let unmarshal t = t +end + +module D2(Vc: ArrayVectorFunctor) (Mx: ArrayMatrixFunctor): RelationDomain.RD with type var = Var.t = +struct + module D = D (Vc) (Mx) + module ConvArg = struct + let allow_global = false + end + include SharedFunctions.AssertionModule (D.V) (D) (ConvArg) + include D +end \ No newline at end of file diff --git a/src/cdomains/apron/affineEqualityDenseDomain.no-apron.ml b/src/cdomains/apron/affineEqualityDenseDomain.no-apron.ml new file mode 100644 index 0000000000..5fed2c883c --- /dev/null +++ b/src/cdomains/apron/affineEqualityDenseDomain.no-apron.ml @@ -0,0 +1,5 @@ +(* This domain is empty on purpose. It serves only as an alternative dependency + in cases where the actual domain can't be used because of a missing library. + It was added because we don't want to fully depend on Apron. *) + +let reset_lazy () = () diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 06268130b2..0d20f5ce9d 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -2,24 +2,30 @@ @see Karr, M. Affine relationships among variables of a program. *) -(** Abstract states in the newly added domain are represented by structs containing a matrix and an apron environment. +(** There are two versions of the AffineEqualityDomain. + Unlike the other version, this version here is NOT based on side effects. + Abstract states in the newly added domain are represented by structs containing a matrix and an apron environment. Matrices are modeled as proposed by Karr: Each variable is assigned to a column and each row represents a linear affine relationship that must hold at the corresponding program point. The apron environment is hereby used to organize the order of columns and variables. *) open GoblintCil open Pretty + module M = Messages open GobApron -open VectorMatrix + +open SparseVector +open ListMatrix + +open Batteries module Mpqf = SharedFunctions.Mpqf -module AffineEqualityMatrix (Vec: AbstractVector) (Mx: AbstractMatrix) = +module AffineEqualityMatrix (Vec: SparseVectorFunctor) (Mx: SparseMatrixFunctor) = struct include Mx(Mpqf) (Vec) let dim_add (ch: Apron.Dim.change) m = - Array.modifyi (+) ch.dim; - add_empty_columns m ch.dim + add_empty_columns m ch.dim let dim_add ch m = timing_wrap "dim add" (dim_add ch) m @@ -29,15 +35,15 @@ 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 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 + let dim_remove ch m ~del = timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del end (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars. Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *) -module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)= +module VarManagement (Vec: SparseVectorFunctor) (Mx: SparseMatrixFunctor)= struct module Vector = Vec (Mpqf) module Matrix = AffineEqualityMatrix (Vec) (Mx) @@ -45,23 +51,25 @@ struct let dim_add = Matrix.dim_add include SharedFunctions.VarManagementOps(AffineEqualityMatrix (Vec) (Mx)) - include ConvenienceOps(Mpqf) + include RatOps.ConvenienceOps(Mpqf) (** Get the constant from the vector if it is a constant *) - let to_constant_opt v = match Vector.findi ((<>:) Mpqf.zero) v with - | exception Not_found -> Some Mpqf.zero - | i when Vector.compare_length_with v (i + 1) = 0 -> Some (Vector.nth v i) + + let to_constant_opt v = match Vector.find_first_non_zero v with + | None -> Some Mpqf.zero + | Some (i, value) when i = (Vector.length v) - 1 -> Some value | _ -> None + let to_constant_opt v = timing_wrap "to_constant_opt" (to_constant_opt) v + let get_coeff_vec (t: t) texp = (*Parses a Texpr to obtain a coefficient + const (last entry) vector to repr. an affine relation. Returns None if the expression is not affine*) 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 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 + let neg v = Vector.map_f_preserves_zero Mpqf.neg v in + let is_const_vec = Vector.is_const_vec in let rec convert_texpr = function (*If x is a constant, replace it with its const. val. immediately*) @@ -72,36 +80,35 @@ struct | Scalar Mpqf x -> x | Scalar Mpfrf x -> Mpfr.to_mpq x in - Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x) + Vector.set_nth 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_nth 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 - | _ -> entry_only zero_vec_cp + Vector.set_nth zero_vec ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)) + | _ -> entry_only zero_vec end - | None -> entry_only zero_vec_cp end + | None -> entry_only zero_vec end | Unop (Neg, e, _, _) -> neg @@ convert_texpr e | Unop (Cast, e, _, _) -> convert_texpr e (*Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts*) | Unop (Sqrt, e, _, _) -> raise NotLinear | Binop (Add, e1, e2, _, _) -> let v1 = convert_texpr e1 in let v2 = convert_texpr e2 in - Vector.map2_with (+:) v1 v2; v1 + Vector.map2_f_preserves_zero (+:) 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_f_preserves_zero (+:) 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_f_preserves_zero ( *:) c v1 + | Some c, _ -> Vector.apply_with_c_f_preserves_zero ( *:) c v2 | _, _ -> raise NotLinear end | Binop _ -> raise NotLinear @@ -114,7 +121,7 @@ struct end (** As it is specifically used for the new affine equality domain, it can only provide bounds if the expression contains known constants only and in that case, min and max are the same. *) -module ExpressionBounds (Vc: AbstractVector) (Mx: AbstractMatrix): (SharedFunctions.ConvBounds with type t = VarManagement(Vc) (Mx).t) = +module ExpressionBounds (Vc: SparseVectorFunctor) (Mx: SparseMatrixFunctor): (SharedFunctions.ConvBounds with type t = VarManagement(Vc) (Mx).t) = struct include VarManagement (Vc) (Mx) @@ -140,10 +147,10 @@ struct let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 end -module D(Vc: AbstractVector) (Mx: AbstractMatrix) = +module D(Vc: SparseVectorFunctor) (Mx: SparseMatrixFunctor) = struct include Printable.Std - include ConvenienceOps (Mpqf) + include RatOps.ConvenienceOps (Mpqf) include VarManagement (Vc) (Mx) module Bounds = ExpressionBounds (Vc) (Mx) @@ -192,7 +199,7 @@ struct in let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars) ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in - if String.starts_with res ~prefix:"+" then + if String.starts_with res "+" then Str.string_after res 1 else res @@ -240,11 +247,9 @@ struct else if is_top_env t2 then {d = Some (dim_add (Environment.dimchange t1.env sup_env) m1); env = sup_env} else - let rref_matr = Matrix.rref_matrix_with (Matrix.copy m1) (Matrix.copy m2) in - if Option.is_none rref_matr then - bot () - else - {d = rref_matr; env = sup_env} + match Matrix.rref_matrix m1 m2 with + | None -> bot () + | rref_matr -> {d = rref_matr; env = sup_env} let meet t1 t2 = @@ -283,41 +288,36 @@ struct if s >= Matrix.num_cols a then a else let case_two a r col_b = let a_r = Matrix.get_row a r in - Matrix.map2i_with (fun i x y -> if i < r then - Vector.map2_with (fun u j -> u +: y *: j) x a_r; x) a col_b; + let a = Matrix.map2i (fun i x y -> if i < r then Vector.map2_f_preserves_zero (fun u j -> u +: y *: j) x a_r else x) a col_b; in Matrix.remove_row a r in let case_three a b col_a col_b max = - let col_a, col_b = Vector.copy col_a, Vector.copy col_b in let col_a, col_b = Vector.keep_vals col_a max, Vector.keep_vals col_b max in - if Vector.equal col_a col_b then + let col_diff = Vector.map2_f_preserves_zero (-:) col_a col_b in + if Vector.is_zero_vec col_diff then (a, b, max) else ( - Vector.rev_with col_a; - Vector.rev_with col_b; - let i = Vector.find2i (<>:) col_a col_b in + let col_a = Vector.rev col_a in + let col_b = Vector.rev col_b in + let i = Vector.find2i_f_false_at_zero (<>:) 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 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_f_preserves_zero (fun u j -> u -: (beta *: j)) x t) else x) m col_diff in Matrix.remove_row (multiply_by_t a a_r) r, Matrix.remove_row (multiply_by_t b b_r) r, (max - 1) ) in - let col_a, col_b = Matrix.get_col a s, Matrix.get_col b s in + let col_a, col_b = Matrix.get_col_upper_triangular a s, Matrix.get_col_upper_triangular b s in let nth_zero v i = match Vector.nth v i with | exception Invalid_argument _ -> Mpqf.zero | x -> x in let a_rs, b_rs = nth_zero col_a r, nth_zero col_b r in if not (Z.equal (Mpqf.get_den a_rs) Z.one) || not (Z.equal (Mpqf.get_den b_rs) Z.one) then failwith "Matrix not in rref form" else - begin match Int.of_float @@ Mpqf.to_float @@ a_rs, Int.of_float @@ Mpqf.to_float @@ b_rs with (* TODO: is it safe to go through floats? *) + begin match Z.to_int @@ Mpqf.get_num a_rs, Z.to_int @@ Mpqf.get_num b_rs with | 1, 1 -> lin_disjunc (r + 1) (s + 1) a b | 1, 0 -> lin_disjunc r (s + 1) (case_two a r col_b) b | 0, 1 -> lin_disjunc r (s + 1) a (case_two b r col_a) @@ -336,9 +336,9 @@ struct let sup_env = Environment.lce a.env b.env in let mod_x = dim_add (Environment.dimchange a.env sup_env) x in let mod_y = dim_add (Environment.dimchange b.env sup_env) y in - {d = Some (lin_disjunc 0 0 (Matrix.copy mod_x) (Matrix.copy mod_y)); env = sup_env} + {d = Some (lin_disjunc 0 0 mod_x mod_y); env = sup_env} | x, y when Matrix.equal x y -> {d = Some x; env = a.env} - | x, y -> {d = Some(lin_disjunc 0 0 (Matrix.copy x) (Matrix.copy y)); env = a.env} + | x, y -> {d = Some(lin_disjunc 0 0 x y); env = a.env} let join a b = timing_wrap "join" (join a) b @@ -358,22 +358,18 @@ struct let pretty_diff () (x, y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y - let remove_rels_with_var x var env inplace = - let j0 = Environment.dim_of_var env var in - if inplace then - (Matrix.reduce_col_with x j0; x) - else - Matrix.reduce_col x j0 + let remove_rels_with_var x var env = + let j0 = Environment.dim_of_var env var in Matrix.reduce_col x j0 - let remove_rels_with_var x var env inplace = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) inplace + 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 = if is_bot t || is_top_env t || vars = [] then t else let m = Option.get t.d in - let rem_from m = List.fold_left (fun m' x -> remove_rels_with_var m' x t.env true) m vars in - {d = Some (Matrix.remove_zero_rows @@ rem_from (Matrix.copy m)); env = t.env} + let rem_from m = List.fold_left (fun m' x -> remove_rels_with_var m' x t.env) m vars in + {d = Some (Matrix.remove_zero_rows @@ rem_from m); env = t.env} let forget_vars t vars = let res = forget_vars t vars in @@ -385,36 +381,40 @@ struct let assign_texpr (t: VarManagement(Vc)(Mx).t) var texp = let assign_invertible_rels x var b env = let j0 = Environment.dim_of_var env var in - let a_j0 = Matrix.get_col x j0 in (*Corresponds to Axj0*) + let a_j0 = Matrix.get_col_upper_triangular x j0 in (*Corresponds to Axj0*) let b0 = Vector.nth b j0 in - Vector.apply_with_c_with (/:) b0 a_j0; (*Corresponds to Axj0/Bj0*) - let recalc_entries m rd_a = Matrix.map2_with (fun x y -> Vector.map2i_with (fun j z d -> + let a_j0 = Vector.apply_with_c_f_preserves_zero (/:) b0 a_j0 in (*Corresponds to Axj0/Bj0*) + let recalc_entries m rd_a = Matrix.map2 (fun x y -> Vector.map2i (fun j z d -> if j = j0 then y else if Vector.compare_length_with b (j + 1) > 0 then z -: y *: d - else z +: y *: d) x b; x) m rd_a + else z +: y *: d) x b) m rd_a in - recalc_entries x a_j0; - if Matrix.normalize_with x then {d = Some x; env = env} else bot () + let x = recalc_entries x a_j0 in + match Matrix.normalize x with + | None -> bot () + | some_normalized_matrix -> {d = some_normalized_matrix; env = env} in let assign_invertible_rels x var b env = timing_wrap "assign_invertible" (assign_invertible_rels x var b) env in let assign_uninvertible_rel x var b env = let b_length = Vector.length b in - Vector.mapi_with (fun i z -> if i < b_length - 1 then Mpqf.neg z else z) b; - Vector.set_val_with b (Environment.dim_of_var env var) Mpqf.one; - let opt_m = Matrix.rref_vec_with x b in - if Option.is_none opt_m then bot () else - {d = opt_m; env = env} + let b = Vector.mapi_f_preserves_zero (fun i z -> if i < b_length - 1 then Mpqf.neg z else z) b in + let b = Vector.set_nth b (Environment.dim_of_var env var) Mpqf.one in + match Matrix.rref_vec x b with + | None -> bot () + | some_matrix -> {d = some_matrix; env = env} 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 if is_bot t then t else let m = Option.get t.d in + in let affineEq_vec = get_coeff_vec t texp 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 - | Some v -> if is_invertible v then let t' = assign_invertible_rels (Matrix.copy m) var v t.env in {d = t'.d; env = t'.env} - else let new_m = Matrix.remove_zero_rows @@ remove_rels_with_var m var t.env false + | Some v when is_top_env t -> + if is_invertible v then t else assign_uninvertible_rel m var v t.env + | Some v -> + if is_invertible v then let t' = assign_invertible_rels m var v t.env in {d = t'.d; env = t'.env} + else let new_m = Matrix.remove_zero_rows @@ remove_rels_with_var m var t.env in assign_uninvertible_rel new_m var v t.env - | None -> {d = Some (Matrix.remove_zero_rows @@ remove_rels_with_var m var t.env false); env = t.env} + | None -> {d = Some (Matrix.remove_zero_rows @@ remove_rels_with_var m var t.env); env = t.env} let assign_texpr t var texp = timing_wrap "assign_texpr" (assign_texpr t var) texp @@ -449,20 +449,18 @@ struct 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 match multi_t.d with - | Some m when not @@ is_top_env multi_t -> + | Some m when not @@ is_top_env multi_t -> 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_with m col_x dim_y + let col_x = Matrix.get_col_upper_triangular 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 switched_m = List.fold_left2 replace_col m primed_vars assigned_vars 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 - if Matrix.normalize_with x then - {d = Some x; env = res.env} - else - bot () + (match Matrix.normalize x with + | None -> bot () + | some_matrix -> {d = some_matrix; env = res.env}) | _ -> t let assign_var_parallel t vv's = @@ -514,13 +512,13 @@ struct let meet_vec e = (* Flip the sign of the const. val in coeff vec *) let coeff = Vector.nth e (Vector.length e - 1) in - Vector.set_val_with e (Vector.length e - 1) (Mpqf.neg coeff); + let e = Vector.set_nth e (Vector.length e - 1) (Mpqf.neg coeff) in if is_bot t then bot () else - let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in - if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} - + match Matrix.rref_vec (Option.get t.d) e with + | None -> bot () + | some_matrix -> {d = some_matrix; env = t.env} in match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with | Some v -> @@ -590,7 +588,7 @@ struct let unmarshal t = t end -module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.RD with type var = Var.t = +module D2(Vc: SparseVectorFunctor) (Mx: SparseMatrixFunctor): RelationDomain.RD with type var = Var.t = struct module D = D (Vc) (Mx) module ConvArg = struct diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 6af7030a51..4684d6d02b 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -12,7 +12,6 @@ open GoblintCil open Pretty module M = Messages open GobApron -open VectorMatrix module Mpqf = SharedFunctions.Mpqf @@ -173,7 +172,7 @@ module EqualitiesConjunction = struct let dim_add (ch: Apron.Dim.change) m = modify_variables_in_domain m ch.dim (+) - let dim_add ch m = timing_wrap "dim add" (dim_add ch) m + let dim_add ch m = Timing.wrap "dim add" (dim_add ch) m let dim_remove (ch: Apron.Dim.change) m = if Array.length ch.dim = 0 || is_empty m then @@ -184,7 +183,7 @@ module EqualitiesConjunction = struct let m' = Array.fold_lefti (fun y i x -> forget_variable y (x)) m cpy in (* clear m' from relations concerning ch.dim *) modify_variables_in_domain m' cpy (-)) - let dim_remove ch m = VectorMatrix.timing_wrap "dim remove" (fun m -> dim_remove ch m) m + let dim_remove ch m = Timing.wrap "dim remove" (fun m -> dim_remove ch m) m let dim_remove ch m ~del = let res = dim_remove ch m in if M.tracing then M.tracel "dim_remove" "dim remove at positions [%s] in { %s } -> { %s }" @@ -343,7 +342,7 @@ struct | [(coeff,var,divi)] -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi)) |_ -> None)) - let simplify_to_ref_and_offset t texp = timing_wrap "coeff_vec" (simplify_to_ref_and_offset t) texp + let simplify_to_ref_and_offset t texp = Timing.wrap "coeff_vec" (simplify_to_ref_and_offset t) texp let assign_const t var const divi = match t.d with | None -> t @@ -365,13 +364,13 @@ struct Some res, Some res) | _ -> None, None - let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 + let bound_texpr d texpr1 = Timing.wrap "bounds calculation" (bound_texpr d) texpr1 end module D = struct include Printable.Std - include ConvenienceOps (Mpqf) + include RatOps.ConvenienceOps (Mpqf) include VarManagement module Bounds = ExpressionBounds @@ -456,7 +455,7 @@ struct if M.tracing then M.tracel "meet" "meet a: %s\n U \n b: %s \n -> %s" (show t1) (show t2) (show res) ; res - let meet t1 t2 = timing_wrap "meet" (meet t1) t2 + let meet t1 t2 = Timing.wrap "meet" (meet t1) t2 let leq t1 t2 = let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *) @@ -475,7 +474,7 @@ struct let m1' = if env_comp = 0 then m1 else VarManagement.dim_add (Environment.dimchange t1.env t2.env) m1 in EConj.IntMap.for_all (implies m1') (snd m2) (* even on sparse m2, it suffices to check the non-trivial equalities, still present in sparse m2 *) - let leq a b = timing_wrap "leq" (leq a) b + let leq a b = Timing.wrap "leq" (leq a) b let leq t1 t2 = let res = leq t1 t2 in @@ -551,7 +550,7 @@ struct | Some x, Some y when EConj.equal x y -> {d = Some x; env = a.env} | Some x, Some y -> {d = join_d x y; env = a.env} - let join a b = timing_wrap "join" (join a) b + let join a b = Timing.wrap "join" (join a) b let join a b = let res = join a b in @@ -593,7 +592,7 @@ struct if M.tracing then M.tracel "ops" "forget_vars %s -> %s" (show t) (show res); res - let forget_vars t vars = timing_wrap "forget_vars" (forget_vars t) vars + let forget_vars t vars = Timing.wrap "forget_vars" (forget_vars t) vars (** implemented as described on page 10 in the paper about Fast Interprocedural Linear Two-Variable Equalities in the Section "Abstract Effect of Statements" This makes a copy of the data structure, it doesn't change it in-place. *) @@ -617,7 +616,7 @@ struct end | None -> bot_env - let assign_texpr t var texp = timing_wrap "assign_texpr" (assign_texpr t var) texp + let assign_texpr t var texp = Timing.wrap "assign_texpr" (assign_texpr t var) texp (* no_ov -> no overflow if it's true then there is no overflow @@ -664,7 +663,7 @@ struct if M.tracing then M.tracel "ops" "assign_var parallel: %s -> %s" (show t) (show res); res - let assign_var_parallel t vv's = timing_wrap "var_parallel" (assign_var_parallel t) vv's + let assign_var_parallel t vv's = Timing.wrap "var_parallel" (assign_var_parallel t) vv's let assign_var_parallel_with t vv's = (* TODO: If we are angling for more performance, this might be a good place ot try. `assign_var_parallel_with` is used whenever a function is entered (body), @@ -696,7 +695,7 @@ struct if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res); res - let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov + let substitute_exp ask t var exp no_ov = Timing.wrap "substitution" (substitute_exp ask t var exp) no_ov (** Assert a constraint expression. @@ -751,7 +750,7 @@ struct if M.tracing then M.tracel "meet_tcons" "meet_tcons with expr: %a no_ov:%b" d_exp original_expr (Lazy.force no_ov); meet_tcons ask t tcons original_expr no_ov - let meet_tcons t tcons expr = timing_wrap "meet_tcons" (meet_tcons t tcons) expr + let meet_tcons t tcons expr = Timing.wrap "meet_tcons" (meet_tcons t tcons) expr let unify a b = meet a b @@ -777,7 +776,7 @@ struct | tcons1 -> meet_tcons ask d tcons1 e no_ov | exception Convert.Unsupported_CilExp _ -> d - let assert_constraint ask d e negate no_ov = timing_wrap "assert_constraint" (assert_constraint ask d e negate) no_ov + let assert_constraint ask d e negate no_ov = Timing.wrap "assert_constraint" (assert_constraint ask d e negate) no_ov let relift t = t diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index fd6c578e60..464c10ec74 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -4,8 +4,8 @@ open Batteries open GobApron -module M = Messages +module M = Messages let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) = if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *) @@ -404,7 +404,7 @@ struct in {d = Some (if add then RelDomain.dim_add dim_change m else RelDomain.dim_remove dim_change m ~del:del); env = new_env} - let change_d t new_env ~add ~del = VectorMatrix.timing_wrap "dimension change" (fun del -> change_d t new_env ~add:add ~del:del) del + let change_d t new_env ~add ~del = Vector.timing_wrap "dimension change" (fun del -> change_d t new_env ~add:add ~del:del) del let vars x = Environment.ivars_only x.env @@ -413,18 +413,18 @@ struct let env' = Environment.add_vars t.env vars in change_d t env' ~add:true ~del:false - let add_vars t vars = VectorMatrix.timing_wrap "add_vars" (add_vars t) vars + let add_vars t vars = Vector.timing_wrap "add_vars" (add_vars t) vars let drop_vars t vars ~del = let t = copy t in let env' = Environment.remove_vars t.env vars in change_d t env' ~add:false ~del:del - let drop_vars t vars = VectorMatrix.timing_wrap "drop_vars" (drop_vars t) vars + let drop_vars t vars = Vector.timing_wrap "drop_vars" (drop_vars t) vars let remove_vars t vars = drop_vars t vars ~del:false - let remove_vars t vars = VectorMatrix.timing_wrap "remove_vars" (remove_vars t) vars + let remove_vars t vars = Vector.timing_wrap "remove_vars" (remove_vars t) vars let remove_vars_with t vars = let t' = remove_vars t vars in @@ -435,7 +435,7 @@ struct let env' = Environment.remove_filter t.env f in change_d t env' ~add:false ~del:false - let remove_filter t f = VectorMatrix.timing_wrap "remove_filter" (remove_filter t) f + let remove_filter t f = Vector.timing_wrap "remove_filter" (remove_filter t) f let remove_filter_with t f = let t' = remove_filter t f in @@ -447,14 +447,14 @@ struct let env' = Environment.keep_filter t.env f in change_d t env' ~add:false ~del:false - let keep_filter t f = VectorMatrix.timing_wrap "keep_filter" (keep_filter t) f + let keep_filter t f = Vector.timing_wrap "keep_filter" (keep_filter t) f let keep_vars t vs = let t = copy t in let env' = Environment.keep_vars t.env vs in change_d t env' ~add:false ~del:false - let keep_vars t vs = VectorMatrix.timing_wrap "keep_vars" (keep_vars t) vs + let keep_vars t vs = Vector.timing_wrap "keep_vars" (keep_vars t) vs let mem_var t var = Environment.mem_var t.env var diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 9ce523e6ed..8d4ba6c472 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1218,6 +1218,19 @@ } }, "additionalProperties": false + }, + "affeq": { + "title": "ana.affeq", + "type": "object", + "properties": { + "sparse": { + "title": "ana.affeq.sparse", + "description": "Use sparse implementation of Affine Equality analysis (using lists). If set to false, the dense version is used (using arrays). Default is true (sparse implementation)", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false } }, "additionalProperties": false diff --git a/src/dune b/src/dune index 10996e7ee8..f114a14db7 100644 --- a/src/dune +++ b/src/dune @@ -10,7 +10,7 @@ (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs ; Conditionally compile based on whether apron optional dependency is installed or not. ; Alternative dependencies seem like the only way to optionally depend on optional dependencies. - ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies. + ; See: https://dune.readthedocs.io/en/stable/reference/library-dependencies.html#alternative-dependencies (select gobApron.ml from (apron -> gobApron.apron.ml) (-> gobApron.no-apron.ml) @@ -35,6 +35,10 @@ (apron -> affineEqualityDomain.apron.ml) (-> affineEqualityDomain.no-apron.ml) ) + (select affineEqualityDenseDomain.ml from + (apron -> affineEqualityDenseDomain.apron.ml) + (-> affineEqualityDenseDomain.no-apron.ml) + ) (select linearTwoVarEqualityAnalysis.ml from (apron -> linearTwoVarEqualityAnalysis.apron.ml) (-> linearTwoVarEqualityAnalysis.no-apron.ml) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 415fb21605..e37fa0cae6 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -260,6 +260,7 @@ module ValueDomainQueries = ValueDomainQueries module RelationDomain = RelationDomain module ApronDomain = ApronDomain module AffineEqualityDomain = AffineEqualityDomain +module AffineEqualityDenseDomain = AffineEqualityDenseDomain module LinearTwoVarEqualityDomain = LinearTwoVarEqualityDomain (** {3 Concurrency} *) @@ -433,7 +434,15 @@ module BaseInvariant = BaseInvariant module CommonPriv = CommonPriv module WideningThresholds = WideningThresholds -module VectorMatrix = VectorMatrix +(* There might be a more elegant solution. *) +module Vector = Vector +module Matrix = Matrix +module ArrayVector = ArrayVector +module ArrayMatrix = ArrayMatrix +module SparseVector = SparseVector +module ListMatrix = ListMatrix +module RatOps = RatOps + module SharedFunctions = SharedFunctions module GobApron = GobApron diff --git a/tests/regression/63-affeq/21-function_call.c b/tests/regression/63-affeq/21-function_call.c new file mode 100644 index 0000000000..723b75e14a --- /dev/null +++ b/tests/regression/63-affeq/21-function_call.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none +// This test was added from 77-lin2vareq because it found mistakes in dim_add that weren't detected by the other tests +#include + +int check_equal(int x, int y, int z) { + __goblint_check(x == y); + __goblint_check(z == y); + __goblint_check(x == z); + return 8; +} + +int main(void) { + int x, y, z; + + y = x; + z = y; + + check_equal(x, y, z); + + return 0; +} diff --git a/tests/unit/cdomains/affineEqualityDomain/dune b/tests/unit/cdomains/affineEqualityDomain/dune new file mode 100644 index 0000000000..acf9e69fbf --- /dev/null +++ b/tests/unit/cdomains/affineEqualityDomain/dune @@ -0,0 +1,3 @@ +; Workaround for workaround for alternative dependencies with unqualified subdirs. +; copy_files causes "dependency cycle that does not involve any files" otherwise +(include_subdirs no) \ No newline at end of file diff --git a/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.apron.ml b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.apron.ml new file mode 100644 index 0000000000..6c66655971 --- /dev/null +++ b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.apron.ml @@ -0,0 +1,371 @@ +(* + To run this (and all other unit tests), type `dune runtest tests/unit/`. +*) + +open Goblint_lib +open OUnit2 +open SparseVector +open ListMatrix + +module D = SharedFunctions.Mpqf +module Vector = SparseVector (D) +module Matrix = ListMatrix (D) (SparseVector) +include RatOps.ConvenienceOps(D) + +(** Shorthands for common functions. *) +let int x = D.of_int x + +let frac numerator denominator = D.of_frac numerator denominator + +(** Shorthands for common functions. *) +let float x = D.of_float x + +let make_matrix_of_2d_list l = + List.fold_left + (fun acc row -> Matrix.append_row acc (Vector.of_list row)) + (Matrix.empty ()) + l + +(** This function runs the equality assertion with the solution after normalizing the matrix. *) +let normalize_and_assert (matrix : Matrix.t) (solution : Matrix.t) = + let get_dimensions m = (Matrix.num_rows m, Matrix.num_cols m) in + let do_dimensions_match (r1, c1) (r2, c2) = r1 = r2 && c1 = c2 in + let matrix_dim = get_dimensions matrix in + let solution_dim = get_dimensions solution in + if not (do_dimensions_match solution_dim matrix_dim) then + failwith + "The matrix to normalize and the solution have different dimensions!" + else + match Matrix.normalize matrix with + | None -> assert_failure "The normalization returned None." + | Some reduced_matrix -> assert_equal reduced_matrix solution + +(** + Example from a [Youtube video](https://www.youtube.com/watch?v=TYs4h-AoqyQ) + but extended by a solution vector b = [0;0;25]^T. +*) +let standard_normalize _ = + let width = 5 in + let any_matrix = + Matrix.append_row + (Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width + [ (0, int 2); (2, int 4); (3, int (-1)) ])) + (Vector.of_sparse_list width [ (0, int 2); (1, int 3); (2, int 4) ])) + (Vector.of_sparse_list width + [ (0, int 1); (1, int 1); (2, int 2); (3, int 4); (4, int 25) ]) + in + let normalized_matrix = + Matrix.append_row + (Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int 1); (2, int 2); (4, int 3) ])) + (Vector.of_sparse_list width [ (1, int 1); (4, int (-2)) ])) + (Vector.of_sparse_list width [ (3, int 1); (4, int 6) ]) + in + normalize_and_assert any_matrix normalized_matrix + +(** + Normalization just sorts the matrix, as the rows are already reduced. +*) +let does_just_sort _ = + let width = 7 in + let chaotic_matrix = + Matrix.append_row + (Matrix.append_row + (Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (2, int 1) ])) + (Vector.of_sparse_list width [ (5, int 1) ])) + (Vector.of_sparse_list width [ (0, int 1); (3, int 1) ])) + (Vector.of_sparse_list width [ (1, int 1); (4, int (-3)) ]) + in + + let sorted_matrix = + Matrix.append_row + (Matrix.append_row + (Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int 1); (3, int 1) ])) + (Vector.of_sparse_list width [ (1, int 1); (4, int (-3)) ])) + (Vector.of_sparse_list width [ (2, int 1) ])) + (Vector.of_sparse_list width [ (5, int 1) ]) + in + normalize_and_assert chaotic_matrix sorted_matrix + +(** + Normalization should eliminate both linearly dependent rows. +*) +let does_eliminate_dependent_rows _ = + let width = 3 in + let linearly_dependent_rows = + Matrix.append_row + (Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int 1); (2, int 4) ])) + (Vector.of_sparse_list width [ (0, int 2); (2, int 8) ])) + (Vector.of_sparse_list width [ (0, int 3); (2, int 12) ]) + in + + let minimized_matrix = + Matrix.append_row + (Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int 1); (2, int 4) ])) + (Vector.zero_vec width)) + (Vector.zero_vec width) + in + normalize_and_assert linearly_dependent_rows minimized_matrix + +let does_handle_floats _ = + let width = 3 in + let any_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, float 5.); (2, float (1. /. 2.)) ])) + (Vector.of_sparse_list width + [ (0, float (1. /. 4.)); (1, float 23.); (2, float 2.) ]) + in + + let normalized_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, float 1.); (2, frac 1 10) ])) + (Vector.of_sparse_list width [ (1, float 1.); (2, frac 79 920) ]) + in + normalize_and_assert any_matrix normalized_matrix + +let does_handle_fractions _ = + let width = 3 in + let any_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, frac 5 1); (2, frac 1 2) ])) + (Vector.of_sparse_list width + [ (0, frac 1 4); (1, frac 23 1); (2, frac 2 1) ]) + in + + let normalized_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, frac 1 1); (2, frac 1 10) ])) + (Vector.of_sparse_list width [ (1, frac 1 1); (2, frac 79 920) ]) + in + normalize_and_assert any_matrix normalized_matrix + +let does_negate_negative _ = + let width = 5 in + let negative_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int (-1)); (3, int (-3)) ])) + (Vector.of_sparse_list width [ (2, int (-1)); (4, int (-5)) ]) + in + + let negated_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int 1); (3, int 3) ])) + (Vector.of_sparse_list width [ (2, int 1); (4, int 5) ]) + in + normalize_and_assert negative_matrix negated_matrix + +(** + Normalization is idempotent. +*) +let does_not_change_normalized_matrix _ = + let width = 5 in + let already_normalized = + Matrix.append_row + (Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int 1); (3, int 1) ])) + (Vector.of_sparse_list width [ (1, int 1); (3, int 3) ])) + (Vector.of_sparse_list width [ (2, int 1); (3, int 1) ]) + in + normalize_and_assert already_normalized already_normalized + +let is_covered_by_simple _ = + let m1 = Matrix.init_with_vec (Vector.of_list [int 1; int 1; int 2; int 10]) in + let m2 = Matrix.append_row + (Matrix.append_row + (Matrix.empty ()) + (Vector.of_list [int 1; int 1; int 0; int 6])) + (Vector.of_list [int 0; int 0; int 1; int 2]) in + let result = Matrix.is_covered_by m1 m2 in + assert_bool "Matrix m1 is covered by m2, but was false" result + +let is_covered_by_vector_first_row _ = + let m1 = Matrix.init_with_vec (Vector.of_list [int 1; int 2; int 0; int 7]) in + let m2 = Matrix.append_row + (Matrix.append_row + (Matrix.empty ()) + (Vector.of_list [int 1; int 2; int 0; int 7])) + (Vector.of_list [int 0; int 0; int 1; int 2]) in + let result = Matrix.is_covered_by m1 m2 in + assert_bool "Matrix m1 is covered by m2, but was false" result + +let is_zero_vec_covered _ = + let m1 = Matrix.init_with_vec (Vector.zero_vec 4) in + let m2 = Matrix.append_row + (Matrix.append_row + (Matrix.empty ()) + (Vector.of_list [int 1; int 2; int 0; int 7])) + (Vector.of_list [int 0; int 0; int 1; int 2]) in + let result = Matrix.is_covered_by m1 m2 in + assert_bool "Matrix m1 is covered by m2, but was false" result + +let is_not_covered _ = + let m1 = Matrix.init_with_vec (Vector.of_list [int 1; int 1; int 2; int 10]) in + let m2 = Matrix.append_row + (Matrix.append_row + (Matrix.empty ()) + (Vector.of_list [int 1; int 1; int 0; int 6])) + (Vector.of_list [int 0; int 0; int 1; int 3]) in + let result = Matrix.is_covered_by m2 m1 in + assert_bool "Matrix m1 is not covered by m2, but was true" (not result) + +let is_covered_big _ = + let m1 = make_matrix_of_2d_list @@ + [[int 1; int 0; int 0; int 0; int 0; int (-1); int 0]; + [int 0; int 1; int 0; int 0; int 0; int (-2); int 0]; + [int 0; int 0; int 1; (frac (-1) 3); frac 1 3; int 0; frac 1 3]] in + + let m2 = make_matrix_of_2d_list @@ + [[int 1; int 0; int 0; int 0; int 0; int 0; int 0]; + [int 0; int 1; int 0; int 0; int 0; int 0; int 0]; + [int 0; int 0; int 1; frac (-1) 3; frac 1 3; int 0; frac 1 3]; + [int 0; int 0; int 0; int 0; int 0; int 1; int 0]] in + + let result = Matrix.is_covered_by m1 m2 in + assert_bool "Matrix m1 is covered by m2, but was false" (result) + +let is_covered_big2 _ = + let m1 = make_matrix_of_2d_list @@ + [[int 1; int 0; int 0; int 0; int 0; int 1; int 0] + ] in + + let m2 = make_matrix_of_2d_list @@ + [[int 1; int 0; int 0; int 0; int 0; int 0; int 0]; + [int 0; int 1; int 0; int 0; int 0; int 0; int 0]; + [int 0; int 0; int 0; int 0; int 0; int 1; int 0]] in + + let result = Matrix.is_covered_by m1 m2 in + assert_bool "Matrix m1 is covered by m2, but was false" (result) +(** + Normalization works on an empty matrix. +*) +let normalize_empty _ = + let width = 3 in + let empty_matrix = + Matrix.append_row + (Matrix.append_row + (Matrix.append_row (Matrix.empty ()) (Vector.zero_vec width)) + (Vector.zero_vec width)) + (Vector.zero_vec width) + in + normalize_and_assert empty_matrix empty_matrix + +let normalize_two_columns _ = + let width = 2 in + let two_col_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int 3); (1, int 2) ])) + (Vector.of_sparse_list width [ (0, int 9); (1, int 6) ]) + in + let normalized_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width + [ (0, int 1); (1, D.div (int 2) (int 3)) ])) + (Vector.of_sparse_list width []) + in + normalize_and_assert two_col_matrix normalized_matrix + +let int_domain_to_rational _ = + let width = 3 in + let int_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width [ (0, int 3); (2, int 1) ])) + (Vector.of_sparse_list width [ (0, int 2); (1, int 1); (2, int 1) ]) + in + let normalized_matrix = + Matrix.append_row + (Matrix.append_row (Matrix.empty ()) + (Vector.of_sparse_list width + [ (0, int 1); (2, D.div (int 1) (int 3)) ])) + (Vector.of_sparse_list width [ (1, int 1); (2, D.div (int 1) (int 3)) ]) + in + normalize_and_assert int_matrix normalized_matrix + + +let vectorMap2i _ = + let v1 = Vector.of_list [int 0; int 1; int 0; int 2; int 3; int 0; int 4; int 0; int 1] in + let v2 = Vector.of_list [int 4; int 0; int 0; int 0; int 5; int 6; int 0; int 0; int 2] in + let result = Vector.map2i (fun i x y -> (int i) *: (x +: y)) v1 v2 in + let expected = Vector.of_list [int 0; int 1; int 0; int 6; int 32; int 30; int 24; int 0; int 24] in + assert_equal expected result + + +let vectorMap2i_empty _ = + let v1 = Vector.of_list [] in + let v2 = Vector.of_list [] in + let result = Vector.map2i (fun i x y -> (int i) *: (x +: y)) v1 v2 in + let expected = Vector.of_list [] in + assert_equal expected result + +let vectorMap2i_one_zero _ = + let v1 = Vector.of_list [int 0; int 0; int 0; int 0] in + let v2 = Vector.of_list [int 1; int 2; int 3; int 4] in + let result = Vector.map2i (fun i x y -> (int i) *: (x +: y)) v1 v2 in + let expected = Vector.of_list [int 0; int 2; int 6; int 12] in + assert_equal expected result + + +let vectorMap_zero_preserving_normal _ = + let v1 = Vector.of_list [int 0; int 1; int 2; int 0; int 0; int 4; int 5; int 0; int 0;] in + let result = Vector.map_f_preserves_zero (fun x -> x *: x) v1 in + let expected = Vector.of_list [int 0; int 1; int 4; int 0; int 0; int 16; int 25; int 0; int 0;] in + assert_equal expected result + + +let get_col_upper_triangular _ = + let m = make_matrix_of_2d_list @@ + [[int 1; int 0; int 0; int 0; int 0; int 0; int 0]; + [int 0; int 1; int 0; int 0; int 0; int 0; int 0]; + [int 0; int 0; int 1; frac (-1) 3; int 0; frac 1 3; int 1]] in + + let result = Matrix.get_col_upper_triangular m 5 in + + let expected = Vector.of_list [int 0; int 0; frac 1 3] in + + assert_equal expected result + +let test () = + "SparseMatrixImplementationTest-Apron" + >::: [ + "can solve a standard normalization" >:: standard_normalize; + "does sort already reduzed" >:: does_just_sort; + "does eliminate dependent rows" >:: does_eliminate_dependent_rows; + "can handle float domain" >:: does_handle_floats; + "can handle fraction domain" >:: does_handle_fractions; + "does negate negative matrix" >:: does_negate_negative; + "does not change already normalized matrix" >:: does_not_change_normalized_matrix; + "m1 is covered by m2" >:: is_covered_by_simple; + "m1 is covered by m2 with vector in first row" >:: is_covered_by_vector_first_row; + "zero vector is covered by m2" >:: is_zero_vec_covered; + "m1 is not covered by m2" >:: is_not_covered; + "m1 is covered by m2 with big matrix" >:: is_covered_big; + "does not change an empty matrix" >:: normalize_empty; + "can correctly normalize a two column matrix" >:: normalize_two_columns; + "can handle a rational solution" >:: int_domain_to_rational; + "m1 is covered by m2 with big matrix2" >:: is_covered_big2; + "map2i two vectors" >:: vectorMap2i; + "map2i two empty vectors" >:: vectorMap2i_empty; + "map2i one zero vector" >:: vectorMap2i_one_zero; + "map zero preserving normal" >:: vectorMap_zero_preserving_normal; + "get column when matrix in rref" >:: get_col_upper_triangular; + ] \ No newline at end of file diff --git a/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.no-apron.ml b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.no-apron.ml new file mode 100644 index 0000000000..b50ad787bc --- /dev/null +++ b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.no-apron.ml @@ -0,0 +1,11 @@ +open OUnit2 + +(* Note: + There are currently no tests independent of apron. + The .apron tests use apron's Mpqf module as an implementation of RatOps. + There are currently no other RatOps implementations, so this file is empty. +*) +let test () = + "SparseMatrixImplementationTest-No-Apron" + >::: [ + ] \ No newline at end of file diff --git a/tests/unit/dune b/tests/unit/dune index 07c87e7822..85038e1da6 100644 --- a/tests/unit/dune +++ b/tests/unit/dune @@ -2,7 +2,14 @@ (test (name mainTest) - (libraries ounit2 qcheck-ounit goblint.std goblint.common goblint.lib goblint.constraint goblint.solver goblint.cdomain.value) + (libraries ounit2 qcheck-ounit goblint.std goblint.common goblint.lib goblint.constraint goblint.solver goblint.cdomain.value + ; Conditionally compile based on whether apron optional dependency is installed or not. + ; See: https://dune.readthedocs.io/en/stable/reference/library-dependencies.html#alternative-dependencies + (select sparseMatrixImplementationTest.ml from + (apron -> sparseMatrixImplementationTest.apron.ml) + (-> sparseMatrixImplementationTest.no-apron.ml) + ) + ) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall)) @@ -11,3 +18,9 @@ (flags (:standard -warn-error -A -w -unused-var-strict)) ; https://dune.readthedocs.io/en/stable/faq.html#how-to-make-warnings-non-fatal ) ) + +; Workaround for alternative dependencies with unqualified subdirs. +; See: https://github.com/ocaml/dune/issues/4383#issuecomment-805107435. +; TODO: Remove workaround with dune 3.0, where this should get fixed. +; A dune file with "include_subdirs no" is located in cdomains/affineEqualityDomain to avoid a dependency cycle +(copy_files# cdomains/affineEqualityDomain/sparseImplementation/*.ml) \ No newline at end of file diff --git a/tests/unit/mainTest.ml b/tests/unit/mainTest.ml index 44f1096655..3ab350d0fe 100644 --- a/tests/unit/mainTest.ml +++ b/tests/unit/mainTest.ml @@ -7,6 +7,7 @@ let all_tests = MapDomainTest.test (); SolverTest.test (); LvalTest.test (); + SparseMatrixImplementationTest.test () ; CompilationDatabaseTest.tests; LibraryDslTest.tests; CilfacadeTest.tests;