Add support for arrays with multiple indices in the Princess model

[daniel-raffler]

Hello everyone,
Princess fails ModelTest.testGetArrays3 with an exception:

java.lang.IllegalArgumentException: unhandled model value store(const(const(0)), 3, store(const(124), 1, 123)) of type class ap.parser.IFunApp
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.convertValue(PrincessFormulaCreator.java:250)
	at org.sosy_lab.java_smt.solvers.princess.PrincessFormulaCreator.convertValue(PrincessFormulaCreator.java:80)
	at org.sosy_lab.java_smt.solvers.princess.PrincessModel.getAssignmentsFromArraySelect(PrincessModel.java:221)
	at org.sosy_lab.java_smt.solvers.princess.PrincessModel.getAssignments(PrincessModel.java:156)
	at org.sosy_lab.java_smt.solvers.princess.PrincessModel.asList(PrincessModel.java:88)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.asList(CachingModel.java:40)
	at org.sosy_lab.java_smt.api.Model.iterator(Model.java:55)
	at org.sosy_lab.java_smt.test.ModelTest.testModelIterator(ModelTest.java:1623)

The problem is on our side as the backend for Princess does not support array with more than one index while creating the model. We should add this missing feature. While we're at it we may also want to look into moving (part) of the conversion into an abstract class. The algorithm is always the same and we currently implement it for several solvers separately

[daniel-raffler]

I've added some tests here and it turns out that model generation for array values is broken in most solvers:

• Princess, Z3 and Yices2 may crash if multiple indices are used
• Z3 often misses a mapping as it simplifies (store array idx val) to (const val) if there are no other mappings (and we can't handle default values)
• CVC4 and CVC5 return Store terms as values
• Bitwuzla doesn't generate any assignments

Since this affects so many solvers I've tried to come up with a generic solution in this branch. The idea is to replace solver specific code for generating the model with a generic implementation that uses a visitor to collect values for all free variables in the assignments. This works quite well so far, however, there are two failing tests: testQuantifiedUF and testQuantifiedUF2. Both tests are quite similar, and they create a constraint f(var) = value where var is an (existentially) quantified variable. The expected outcome is that the model will contain a mapping f(2) = 1 where 2 is the value for the quantified variable

Unfortunately this won't work with the visitor-based approach as quantified variables are substituted before they are visited (and even if they weren't I'm not sure it's a good idea to ask the solver to evaluate bound variables). I've tried to fix this by ignoring bound variables while building the model and changed the tests to expect no mappings for them. However, I'm not sure if this is the right way to solve the problem..

@baierd, @kfriedberger
What's you opinion on this?

[baierd]

@daniel-raffler first of all: thank you for noticing and working/thinking about this!
I am rather tight on time currently and will only be able to look at this and other current developments in 2-3 weeks. So i leave this to Karlheinz in the meantime. Sorry about that.

We found some new exceptions for the current JavaSMT version in CPAchecker here: https://gitlab.com/sosy-lab/software/cpachecker/-/merge_requests/335#note_2792975025
These might be related to this issue. If not, please inform me or open a new issue for them.

[daniel-raffler]

@daniel-raffler first of all: thank you for noticing and working/thinking about this! I am rather tight on time currently and will only be able to look at this and other current developments in 2-3 weeks. So i leave this to Karlheinz in the meantime. Sorry about that.

Sure, no hurry!

We found some new exceptions for the current JavaSMT version in CPAchecker here: https://gitlab.com/sosy-lab/software/cpachecker/-/merge_requests/335#note_2792975025

Do you mean these tasks here?

Unfortunately the logs are not included in the zip file, but I'm getting the exception you mentioned when running

bin/cpachecker --no-output-files --option cpa.predicate.memoryAllocationsAlwaysSucceed=true --predicateAnalysis --option cpa.predicate.encodeFloatAs=INTEGER --option cpa.predicate.encodeBitvectorAs=INTEGER --option solver.solver=princess test/programs/benchmarks/array-fpi/s1iff.c

These might be related to this issue. If not, please inform me or open a new issue for them.

This looks like it could be a bug in Princess. I've tried running the task with #528 and that seems to take care of the issue. However, we may still want to look into it and report the problem to the Princess developers

[baierd]

Yes those are the correct exceptions.

My bad, here are the relevant logs for Princess: princess-logs-selection.zip

It looks like we should move the discussion about this into a dedicated issue. Would you be so kind and open a new one?

[daniel-raffler]

Yes those are the correct exceptions.

My bad, here are the relevant logs for Princess: princess-logs-selection.zip

It looks like we should move the discussion about this into a dedicated issue. Would you be so kind and open a new one?

Thanks! I've opened a new issue here