caballa
commented
3 years ago I need more time to debug this.
As a general comment, I can see that you don't pass the bitcode of the GMP library. That's OK but it's bad for configuration priming because it cannot currently execute library code. Thus, it will stop with the first creation of a GMP number. If you are interested, you can see here how we compile GMP and provide the bitcode to OCCAM so the configuration priming can be much more effective.
A follow-up question is that if it's also better to add the bitcode of musllvm. From configuration priming perspective, you don't need to because it uses FFI to call system calls.
Specializing yices with configuration priming results in a large reduction of functions. However, when the specialized binary is run, it results in a segmentation fault. The files required to reproduce the problem can be found here. The issue can be reproduced in the following way:
The test solves for an example file (bool_eqs.ys) using the QF_AUFBV logic and compares the result with result from an unspecialized binary. The test fails when the --enable-config-prime flag is provided. However, the test passes when the flag is not provided (i.e. bash build.sh). To see the segmentation fault, run ./yices_occamized_stripped (after running bash build.sh --enable-config-prime).