From 58e34c0128d4bb08e2306ab1952c6caa0f46bb21 Mon Sep 17 00:00:00 2001 From: Havercake Date: Tue, 10 Dec 2024 15:45:56 +0100 Subject: [PATCH 1/5] Normalize tests for empty matrix, two column matrix and a normalized matrix with rationals --- .../sparseMatrixImplementationTest.ml | 54 ++++++++++++++++++- 1 file changed, 53 insertions(+), 1 deletion(-) diff --git a/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml index 9f8a63b83c..edd4d51261 100644 --- a/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml +++ b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml @@ -183,6 +183,54 @@ let does_not_change_normalized_matrix _ = in normalize_and_assert already_normalized already_normalized +(** + 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 tests = "SparseMatrixImplementationTest" >::: [ @@ -193,7 +241,11 @@ let tests = (*"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; + "does not change already normalized matrix" + >:: does_not_change_normalized_matrix; + "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; ] let () = run_test_tt_main tests From 9f7cec947dee59627c44b1ed1dc5d2658f9f66a6 Mon Sep 17 00:00:00 2001 From: Havercake Date: Tue, 10 Dec 2024 15:48:07 +0100 Subject: [PATCH 2/5] Added a newline --- .../sparseImplementation/sparseMatrixImplementationTest.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml index edd4d51261..7d3ffb48d8 100644 --- a/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml +++ b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml @@ -241,8 +241,7 @@ let tests = (*"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; + "does not change already normalized matrix" >:: does_not_change_normalized_matrix; "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; From 6673aae4635b3e63765b6a9eabfc5161c174075f Mon Sep 17 00:00:00 2001 From: Havercake Date: Tue, 10 Dec 2024 15:50:23 +0100 Subject: [PATCH 3/5] Changed the assert failure text for when the normalization fails --- .../sparseImplementation/sparseMatrixImplementationTest.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml index 7d3ffb48d8..08318ec9bc 100644 --- a/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml +++ b/tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml @@ -33,8 +33,7 @@ let normalize_and_assert (matrix : Matrix.t) (solution : Matrix.t) = "The matrix to normalize and the solution have different dimensions!" else match Matrix.normalize matrix with - | None -> - assert_failure "The matrix is normalizable but was not normalized!" + | None -> assert_failure "The normalization returned None." | Some reduced_matrix -> assert_equal reduced_matrix solution (** From 79f890a9ac0488921c69dbe4eb35af2433bfa59d Mon Sep 17 00:00:00 2001 From: Havercake Date: Tue, 10 Dec 2024 15:53:51 +0100 Subject: [PATCH 4/5] Added some comments on the test setup --- tests/unit/mainTest.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/unit/mainTest.ml b/tests/unit/mainTest.ml index 4fd65f6736..b8be9ef8f0 100644 --- a/tests/unit/mainTest.ml +++ b/tests/unit/mainTest.ml @@ -14,10 +14,12 @@ let all_tests = (* etc *) "domaintest" >::: QCheck_ounit.to_ounit2_test_list Maindomaintest.all_testsuite; IntOpsTest.tests; + (* SparseMatrixImplementationTest.tests; *) (* Uncomment this to add the sparse matrix tests to all tests *) ] let subset_tests = "" >::: [SparseMatrixImplementationTest.tests] let () = print_string "\027[0;1munit: \027[0;0;00m"; - run_test_tt_main subset_tests + run_test_tt_main subset_tests (* Remove this and uncomment the line below to run all tests.*) + (* run_test_tt_main all_tests *) From 4b34fda53588d5bb64ee8e5dbaf5b3782bb915e1 Mon Sep 17 00:00:00 2001 From: Havercake Date: Tue, 10 Dec 2024 15:54:03 +0100 Subject: [PATCH 5/5] Added some comments on the test setup --- tests/unit/mainTest.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/unit/mainTest.ml b/tests/unit/mainTest.ml index b8be9ef8f0..9527679fe7 100644 --- a/tests/unit/mainTest.ml +++ b/tests/unit/mainTest.ml @@ -22,4 +22,4 @@ let subset_tests = "" >::: [SparseMatrixImplementationTest.tests] let () = print_string "\027[0;1munit: \027[0;0;00m"; run_test_tt_main subset_tests (* Remove this and uncomment the line below to run all tests.*) - (* run_test_tt_main all_tests *) +(* run_test_tt_main all_tests *)