Sparsification of Affine Equality Matrix #1625
Conversation
sim642
added
in progress
performance
charlotte-brandt
force-pushed
the
master
branch
from
6b07930 to
f931125
Compare
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
…goblint_lib.ml; Reintroduced Timing.wrap;
|
Thanks for updating the description! |
tests/unit/cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.ml
Outdated
Show resolved
Hide resolved
| open ListMatrix | ||
| open ConvenienceOps | ||
|
|
||
| module D = SharedFunctions.Mpqf |
There was a problem hiding this comment.
The "locked" CI job for PRs does not check this, but manually running "unlocked" on your branch should do this: also run tests without the optional Apron dependency installed.
SharedFunctions is one of those modules that's empty without Apron, so I suspect a lot of this would fail to even compile in that case.
You could also try locally uninstalling apron and seeing if everything compiles and all tests pass.
There was a problem hiding this comment.
We added a .no-apron test file. It currently doesn't test anything because there currently is no RatOps implementation other than Mpqf, but now it does compile without Apron.
There was a problem hiding this comment.
However, we ran into an issue with cyclic dependencies when specifying the alternative dependencies for dune, so the tests are located tests/unit but not deeper in the hierarchy.
We tried adding
(copy_files# cdomains/affineEqualityDomain/sparseImplementation/sparseMatrixImplementationTest.*.ml)
to the testing dune file as suggested in this issue, but got the error
Error: Dependency cycle between:
Computing directory contents of _build/default/tests/unit
-> { dir =
In_build_dir
"default/tests/unit/cdomains/affineEqualityDomain/sparseImplementation"
; predicate = Glob (Glob "sparseMatrixImplementationTest.*.ml")
; only_generated_files = false
}
-> Computing directory contents of _build/default/tests/unit
| 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 |
There was a problem hiding this comment.
Why is this in vector.ml if there's also sparseVector.ml for which this seems to be the interface?
Or even further, why isn't this just in sparseVector.mli?
(Same with ArrayVector interface above.)
There was a problem hiding this comment.
We had issues creating .mli files because of the functors that replace num with RatOps which were in the original implementation. We thought it would be nice to have all the vector interfaces in one place but if you think it is better for each file to include its interface we can also move module type SparseVector and SparseVectorFunctor to sparseVector.ml (and the same for the other interfaces).
There was a problem hiding this comment.
I think it's cleaner if vector.ml defines the general abstract interface and sparseVector.ml and arrayVector.ml are independent implementations of it.
Not having vectorFunctor.ml and matrixFunctor.ml just for some interfaces would also reduce the number of top-level modules involved.
There was a problem hiding this comment.
Okay, I changed this. The interfaces as well as the functors are now in their respective files.
src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
Outdated
Show resolved
Hide resolved
| 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 |
There was a problem hiding this comment.
Same thing here as with SparseVector in vector.ml.
| (* To use the original affineEqualityDomain implementation uncomment this and the AD_Array. | ||
| Then replace AD with AD_Array in the functor application. | ||
| open ArrayVector | ||
| open ArrayMatrix *) |
There was a problem hiding this comment.
This is very hard-coded and manual. It should be easy to just make an option for this (if not register two separate analyses with separate names, but that might be too much).
This pull request contributes a sparsification of the
AffineEqualityMatrix(affeq) and is based on the domain of @MartinWehking from this PR.Following restructuring of the modules is introduced:
We added a second
AffineEqualityDomainwhich exploits the sparsity of the affine equality matrices based on this observation by @DrMichaelPetter. ASparseMatrixFunctorandSparseVectorFunctor(as well asArrayMatrixFunctorandArrayVectorFunctor) were added for this purpose and replaced the generalAbstractMatrixandAbstractVector. TheAffineEqualityDomainis now implemented without relying on side effects.The old
AffineEqualityDomainusing arrays was renamed toAffineEqualityDomainSideEffectswhich usesArrayMatrixFunctorandArrayVectorFunctor.No new analysis was added to switch between versions. A description for how to switch between both implementations is provided in the
affineEqualityAnalysisfile.The implementation of sparse matrix works as follows:
The sparse matrix is implemented in the
ListMatrixmodule. Itstype tis a list ofsparseVectorsrepresenting the matrix' rows.sparseVectoris implemented as an ordered list of tuples (index, value) for all non-zero entries.Some functions are implemented for zero-preserving functions only. A function is zero-preserving iff it has a fixpoint at zero. These functions are implemented to gain performance when being used on
sparseVectors.This implementation is part of an assignment for the course Automated Bug Hunting and Beyond at TUM in the winter term 2024/25.