Skip to content

Commit bceccd4

Browse files
kadameitkadameit
committed
Move affeq tests back to subdir and avoid cyclic dependencies with dune file
1 parent 3d1b152 commit bceccd4

File tree

3 files changed

+385
-0
lines changed

3 files changed

+385
-0
lines changed

‎tests/unit/cdomains/affineEqualityDomain/dune‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
; Workaround for workaround for alternative dependencies with unqualified subdirs.
2+
; copy_files causes "dependency cycle that does not involve any files" otherwise
3+
(include_subdirs no)

‎tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.apron.ml‎

Lines changed: 371 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,371 @@
1+
(*
2+
To run this (and all other unit tests), type `dune runtest tests/unit/`.
3+
*)
4+
5+
open Goblint_lib
6+
open OUnit2
7+
open SparseVector
8+
open ListMatrix
9+
10+
module D = SharedFunctions.Mpqf
11+
module Vector = SparseVector (D)
12+
module Matrix = ListMatrix (D) (SparseVector)
13+
include RatOps.ConvenienceOps(D)
14+
15+
(** Shorthands for common functions. *)
16+
let int x = D.of_int x
17+
18+
let frac numerator denominator = D.of_frac numerator denominator
19+
20+
(** Shorthands for common functions. *)
21+
let float x = D.of_float x
22+
23+
let make_matrix_of_2d_list l =
24+
List.fold_left
25+
(fun acc row -> Matrix.append_row acc (Vector.of_list row))
26+
(Matrix.empty ())
27+
l
28+
29+
(** This function runs the equality assertion with the solution after normalizing the matrix. *)
30+
let normalize_and_assert (matrix : Matrix.t) (solution : Matrix.t) =
31+
let get_dimensions m = (Matrix.num_rows m, Matrix.num_cols m) in
32+
let do_dimensions_match (r1, c1) (r2, c2) = r1 = r2 && c1 = c2 in
33+
let matrix_dim = get_dimensions matrix in
34+
let solution_dim = get_dimensions solution in
35+
if not (do_dimensions_match solution_dim matrix_dim) then
36+
failwith
37+
"The matrix to normalize and the solution have different dimensions!"
38+
else
39+
match Matrix.normalize matrix with
40+
| None -> assert_failure "The normalization returned None."
41+
| Some reduced_matrix -> assert_equal reduced_matrix solution
42+
43+
(**
44+
Example from a [Youtube video](https://www.youtube.com/watch?v=TYs4h-AoqyQ)
45+
but extended by a solution vector b = [0;0;25]^T.
46+
*)
47+
let standard_normalize _ =
48+
let width = 5 in
49+
let any_matrix =
50+
Matrix.append_row
51+
(Matrix.append_row
52+
(Matrix.append_row (Matrix.empty ())
53+
(Vector.of_sparse_list width
54+
[ (0, int 2); (2, int 4); (3, int (-1)) ]))
55+
(Vector.of_sparse_list width [ (0, int 2); (1, int 3); (2, int 4) ]))
56+
(Vector.of_sparse_list width
57+
[ (0, int 1); (1, int 1); (2, int 2); (3, int 4); (4, int 25) ])
58+
in
59+
let normalized_matrix =
60+
Matrix.append_row
61+
(Matrix.append_row
62+
(Matrix.append_row (Matrix.empty ())
63+
(Vector.of_sparse_list width [ (0, int 1); (2, int 2); (4, int 3) ]))
64+
(Vector.of_sparse_list width [ (1, int 1); (4, int (-2)) ]))
65+
(Vector.of_sparse_list width [ (3, int 1); (4, int 6) ])
66+
in
67+
normalize_and_assert any_matrix normalized_matrix
68+
69+
(**
70+
Normalization just sorts the matrix, as the rows are already reduced.
71+
*)
72+
let does_just_sort _ =
73+
let width = 7 in
74+
let chaotic_matrix =
75+
Matrix.append_row
76+
(Matrix.append_row
77+
(Matrix.append_row
78+
(Matrix.append_row (Matrix.empty ())
79+
(Vector.of_sparse_list width [ (2, int 1) ]))
80+
(Vector.of_sparse_list width [ (5, int 1) ]))
81+
(Vector.of_sparse_list width [ (0, int 1); (3, int 1) ]))
82+
(Vector.of_sparse_list width [ (1, int 1); (4, int (-3)) ])
83+
in
84+
85+
let sorted_matrix =
86+
Matrix.append_row
87+
(Matrix.append_row
88+
(Matrix.append_row
89+
(Matrix.append_row (Matrix.empty ())
90+
(Vector.of_sparse_list width [ (0, int 1); (3, int 1) ]))
91+
(Vector.of_sparse_list width [ (1, int 1); (4, int (-3)) ]))
92+
(Vector.of_sparse_list width [ (2, int 1) ]))
93+
(Vector.of_sparse_list width [ (5, int 1) ])
94+
in
95+
normalize_and_assert chaotic_matrix sorted_matrix
96+
97+
(**
98+
Normalization should eliminate both linearly dependent rows.
99+
*)
100+
let does_eliminate_dependent_rows _ =
101+
let width = 3 in
102+
let linearly_dependent_rows =
103+
Matrix.append_row
104+
(Matrix.append_row
105+
(Matrix.append_row (Matrix.empty ())
106+
(Vector.of_sparse_list width [ (0, int 1); (2, int 4) ]))
107+
(Vector.of_sparse_list width [ (0, int 2); (2, int 8) ]))
108+
(Vector.of_sparse_list width [ (0, int 3); (2, int 12) ])
109+
in
110+
111+
let minimized_matrix =
112+
Matrix.append_row
113+
(Matrix.append_row
114+
(Matrix.append_row (Matrix.empty ())
115+
(Vector.of_sparse_list width [ (0, int 1); (2, int 4) ]))
116+
(Vector.zero_vec width))
117+
(Vector.zero_vec width)
118+
in
119+
normalize_and_assert linearly_dependent_rows minimized_matrix
120+
121+
let does_handle_floats _ =
122+
let width = 3 in
123+
let any_matrix =
124+
Matrix.append_row
125+
(Matrix.append_row (Matrix.empty ())
126+
(Vector.of_sparse_list width [ (0, float 5.); (2, float (1. /. 2.)) ]))
127+
(Vector.of_sparse_list width
128+
[ (0, float (1. /. 4.)); (1, float 23.); (2, float 2.) ])
129+
in
130+
131+
let normalized_matrix =
132+
Matrix.append_row
133+
(Matrix.append_row (Matrix.empty ())
134+
(Vector.of_sparse_list width [ (0, float 1.); (2, frac 1 10) ]))
135+
(Vector.of_sparse_list width [ (1, float 1.); (2, frac 79 920) ])
136+
in
137+
normalize_and_assert any_matrix normalized_matrix
138+
139+
let does_handle_fractions _ =
140+
let width = 3 in
141+
let any_matrix =
142+
Matrix.append_row
143+
(Matrix.append_row (Matrix.empty ())
144+
(Vector.of_sparse_list width [ (0, frac 5 1); (2, frac 1 2) ]))
145+
(Vector.of_sparse_list width
146+
[ (0, frac 1 4); (1, frac 23 1); (2, frac 2 1) ])
147+
in
148+
149+
let normalized_matrix =
150+
Matrix.append_row
151+
(Matrix.append_row (Matrix.empty ())
152+
(Vector.of_sparse_list width [ (0, frac 1 1); (2, frac 1 10) ]))
153+
(Vector.of_sparse_list width [ (1, frac 1 1); (2, frac 79 920) ])
154+
in
155+
normalize_and_assert any_matrix normalized_matrix
156+
157+
let does_negate_negative _ =
158+
let width = 5 in
159+
let negative_matrix =
160+
Matrix.append_row
161+
(Matrix.append_row (Matrix.empty ())
162+
(Vector.of_sparse_list width [ (0, int (-1)); (3, int (-3)) ]))
163+
(Vector.of_sparse_list width [ (2, int (-1)); (4, int (-5)) ])
164+
in
165+
166+
let negated_matrix =
167+
Matrix.append_row
168+
(Matrix.append_row (Matrix.empty ())
169+
(Vector.of_sparse_list width [ (0, int 1); (3, int 3) ]))
170+
(Vector.of_sparse_list width [ (2, int 1); (4, int 5) ])
171+
in
172+
normalize_and_assert negative_matrix negated_matrix
173+
174+
(**
175+
Normalization is idempotent.
176+
*)
177+
let does_not_change_normalized_matrix _ =
178+
let width = 5 in
179+
let already_normalized =
180+
Matrix.append_row
181+
(Matrix.append_row
182+
(Matrix.append_row (Matrix.empty ())
183+
(Vector.of_sparse_list width [ (0, int 1); (3, int 1) ]))
184+
(Vector.of_sparse_list width [ (1, int 1); (3, int 3) ]))
185+
(Vector.of_sparse_list width [ (2, int 1); (3, int 1) ])
186+
in
187+
normalize_and_assert already_normalized already_normalized
188+
189+
let is_covered_by_simple _ =
190+
let m1 = Matrix.init_with_vec (Vector.of_list [int 1; int 1; int 2; int 10]) in
191+
let m2 = Matrix.append_row
192+
(Matrix.append_row
193+
(Matrix.empty ())
194+
(Vector.of_list [int 1; int 1; int 0; int 6]))
195+
(Vector.of_list [int 0; int 0; int 1; int 2]) in
196+
let result = Matrix.is_covered_by m1 m2 in
197+
assert_bool "Matrix m1 is covered by m2, but was false" result
198+
199+
let is_covered_by_vector_first_row _ =
200+
let m1 = Matrix.init_with_vec (Vector.of_list [int 1; int 2; int 0; int 7]) in
201+
let m2 = Matrix.append_row
202+
(Matrix.append_row
203+
(Matrix.empty ())
204+
(Vector.of_list [int 1; int 2; int 0; int 7]))
205+
(Vector.of_list [int 0; int 0; int 1; int 2]) in
206+
let result = Matrix.is_covered_by m1 m2 in
207+
assert_bool "Matrix m1 is covered by m2, but was false" result
208+
209+
let is_zero_vec_covered _ =
210+
let m1 = Matrix.init_with_vec (Vector.zero_vec 4) in
211+
let m2 = Matrix.append_row
212+
(Matrix.append_row
213+
(Matrix.empty ())
214+
(Vector.of_list [int 1; int 2; int 0; int 7]))
215+
(Vector.of_list [int 0; int 0; int 1; int 2]) in
216+
let result = Matrix.is_covered_by m1 m2 in
217+
assert_bool "Matrix m1 is covered by m2, but was false" result
218+
219+
let is_not_covered _ =
220+
let m1 = Matrix.init_with_vec (Vector.of_list [int 1; int 1; int 2; int 10]) in
221+
let m2 = Matrix.append_row
222+
(Matrix.append_row
223+
(Matrix.empty ())
224+
(Vector.of_list [int 1; int 1; int 0; int 6]))
225+
(Vector.of_list [int 0; int 0; int 1; int 3]) in
226+
let result = Matrix.is_covered_by m2 m1 in
227+
assert_bool "Matrix m1 is not covered by m2, but was true" (not result)
228+
229+
let is_covered_big _ =
230+
let m1 = make_matrix_of_2d_list @@
231+
[[int 1; int 0; int 0; int 0; int 0; int (-1); int 0];
232+
[int 0; int 1; int 0; int 0; int 0; int (-2); int 0];
233+
[int 0; int 0; int 1; (frac (-1) 3); frac 1 3; int 0; frac 1 3]] in
234+
235+
let m2 = make_matrix_of_2d_list @@
236+
[[int 1; int 0; int 0; int 0; int 0; int 0; int 0];
237+
[int 0; int 1; int 0; int 0; int 0; int 0; int 0];
238+
[int 0; int 0; int 1; frac (-1) 3; frac 1 3; int 0; frac 1 3];
239+
[int 0; int 0; int 0; int 0; int 0; int 1; int 0]] in
240+
241+
let result = Matrix.is_covered_by m1 m2 in
242+
assert_bool "Matrix m1 is covered by m2, but was false" (result)
243+
244+
let is_covered_big2 _ =
245+
let m1 = make_matrix_of_2d_list @@
246+
[[int 1; int 0; int 0; int 0; int 0; int 1; int 0]
247+
] in
248+
249+
let m2 = make_matrix_of_2d_list @@
250+
[[int 1; int 0; int 0; int 0; int 0; int 0; int 0];
251+
[int 0; int 1; int 0; int 0; int 0; int 0; int 0];
252+
[int 0; int 0; int 0; int 0; int 0; int 1; int 0]] in
253+
254+
let result = Matrix.is_covered_by m1 m2 in
255+
assert_bool "Matrix m1 is covered by m2, but was false" (result)
256+
(**
257+
Normalization works on an empty matrix.
258+
*)
259+
let normalize_empty _ =
260+
let width = 3 in
261+
let empty_matrix =
262+
Matrix.append_row
263+
(Matrix.append_row
264+
(Matrix.append_row (Matrix.empty ()) (Vector.zero_vec width))
265+
(Vector.zero_vec width))
266+
(Vector.zero_vec width)
267+
in
268+
normalize_and_assert empty_matrix empty_matrix
269+
270+
let normalize_two_columns _ =
271+
let width = 2 in
272+
let two_col_matrix =
273+
Matrix.append_row
274+
(Matrix.append_row (Matrix.empty ())
275+
(Vector.of_sparse_list width [ (0, int 3); (1, int 2) ]))
276+
(Vector.of_sparse_list width [ (0, int 9); (1, int 6) ])
277+
in
278+
let normalized_matrix =
279+
Matrix.append_row
280+
(Matrix.append_row (Matrix.empty ())
281+
(Vector.of_sparse_list width
282+
[ (0, int 1); (1, D.div (int 2) (int 3)) ]))
283+
(Vector.of_sparse_list width [])
284+
in
285+
normalize_and_assert two_col_matrix normalized_matrix
286+
287+
let int_domain_to_rational _ =
288+
let width = 3 in
289+
let int_matrix =
290+
Matrix.append_row
291+
(Matrix.append_row (Matrix.empty ())
292+
(Vector.of_sparse_list width [ (0, int 3); (2, int 1) ]))
293+
(Vector.of_sparse_list width [ (0, int 2); (1, int 1); (2, int 1) ])
294+
in
295+
let normalized_matrix =
296+
Matrix.append_row
297+
(Matrix.append_row (Matrix.empty ())
298+
(Vector.of_sparse_list width
299+
[ (0, int 1); (2, D.div (int 1) (int 3)) ]))
300+
(Vector.of_sparse_list width [ (1, int 1); (2, D.div (int 1) (int 3)) ])
301+
in
302+
normalize_and_assert int_matrix normalized_matrix
303+
304+
305+
let vectorMap2i _ =
306+
let v1 = Vector.of_list [int 0; int 1; int 0; int 2; int 3; int 0; int 4; int 0; int 1] in
307+
let v2 = Vector.of_list [int 4; int 0; int 0; int 0; int 5; int 6; int 0; int 0; int 2] in
308+
let result = Vector.map2i (fun i x y -> (int i) *: (x +: y)) v1 v2 in
309+
let expected = Vector.of_list [int 0; int 1; int 0; int 6; int 32; int 30; int 24; int 0; int 24] in
310+
assert_equal expected result
311+
312+
313+
let vectorMap2i_empty _ =
314+
let v1 = Vector.of_list [] in
315+
let v2 = Vector.of_list [] in
316+
let result = Vector.map2i (fun i x y -> (int i) *: (x +: y)) v1 v2 in
317+
let expected = Vector.of_list [] in
318+
assert_equal expected result
319+
320+
let vectorMap2i_one_zero _ =
321+
let v1 = Vector.of_list [int 0; int 0; int 0; int 0] in
322+
let v2 = Vector.of_list [int 1; int 2; int 3; int 4] in
323+
let result = Vector.map2i (fun i x y -> (int i) *: (x +: y)) v1 v2 in
324+
let expected = Vector.of_list [int 0; int 2; int 6; int 12] in
325+
assert_equal expected result
326+
327+
328+
let vectorMap_zero_preserving_normal _ =
329+
let v1 = Vector.of_list [int 0; int 1; int 2; int 0; int 0; int 4; int 5; int 0; int 0;] in
330+
let result = Vector.map_f_preserves_zero (fun x -> x *: x) v1 in
331+
let expected = Vector.of_list [int 0; int 1; int 4; int 0; int 0; int 16; int 25; int 0; int 0;] in
332+
assert_equal expected result
333+
334+
335+
let get_col_upper_triangular _ =
336+
let m = make_matrix_of_2d_list @@
337+
[[int 1; int 0; int 0; int 0; int 0; int 0; int 0];
338+
[int 0; int 1; int 0; int 0; int 0; int 0; int 0];
339+
[int 0; int 0; int 1; frac (-1) 3; int 0; frac 1 3; int 1]] in
340+
341+
let result = Matrix.get_col_upper_triangular m 5 in
342+
343+
let expected = Vector.of_list [int 0; int 0; frac 1 3] in
344+
345+
assert_equal expected result
346+
347+
let test () =
348+
"SparseMatrixImplementationTest-Apron"
349+
>::: [
350+
"can solve a standard normalization" >:: standard_normalize;
351+
"does sort already reduzed" >:: does_just_sort;
352+
"does eliminate dependent rows" >:: does_eliminate_dependent_rows;
353+
"can handle float domain" >:: does_handle_floats;
354+
"can handle fraction domain" >:: does_handle_fractions;
355+
"does negate negative matrix" >:: does_negate_negative;
356+
"does not change already normalized matrix" >:: does_not_change_normalized_matrix;
357+
"m1 is covered by m2" >:: is_covered_by_simple;
358+
"m1 is covered by m2 with vector in first row" >:: is_covered_by_vector_first_row;
359+
"zero vector is covered by m2" >:: is_zero_vec_covered;
360+
"m1 is not covered by m2" >:: is_not_covered;
361+
"m1 is covered by m2 with big matrix" >:: is_covered_big;
362+
"does not change an empty matrix" >:: normalize_empty;
363+
"can correctly normalize a two column matrix" >:: normalize_two_columns;
364+
"can handle a rational solution" >:: int_domain_to_rational;
365+
"m1 is covered by m2 with big matrix2" >:: is_covered_big2;
366+
"map2i two vectors" >:: vectorMap2i;
367+
"map2i two empty vectors" >:: vectorMap2i_empty;
368+
"map2i one zero vector" >:: vectorMap2i_one_zero;
369+
"map zero preserving normal" >:: vectorMap_zero_preserving_normal;
370+
"get column when matrix in rref" >:: get_col_upper_triangular;
371+
]

‎tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.no-apron.ml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
open OUnit2
2+
3+
(* Note:
4+
There are currently no tests independent of apron.
5+
The .apron tests use apron's Mpqf module as an implementation of RatOps.
6+
There are currently no other RatOps implementations, so this file is empty.
7+
*)
8+
let test () =
9+
"SparseMatrixImplementationTest-No-Apron"
10+
>::: [
11+
]

0 commit comments

Comments
 (0)