The soundness tests can be improved by checking the entire store of the analysis against the store of the concrete interpreter, similar to what we already do for the precision benchmarks. This has the following advantages over the current setup of the soundness tests:
we can test the soundness of more values (all values in the store), rather than just those that are currently reported manually by the concrete interpreter.
we can test the soundness property more rigorously; currently for some data types we don't actually properly check for subsumption.
Both these improvements should make it less probable to miss soundness bugs in the benchmarks.
To avoid code duplication, it Is probably advised to factor our the code in the precision benchmarks that transforms values of different analyses and the concrete interpreter to the same base domain, and then reuse this code for the soundness tests as well.
The soundness tests can be improved by checking the entire store of the analysis against the store of the concrete interpreter, similar to what we already do for the precision benchmarks. This has the following advantages over the current setup of the soundness tests:
Both these improvements should make it less probable to miss soundness bugs in the benchmarks.
To avoid code duplication, it Is probably advised to factor our the code in the precision benchmarks that transforms values of different analyses and the concrete interpreter to the same base domain, and then reuse this code for the soundness tests as well.