Add support for Strings and Rationals to the Princess backend #391
Conversation
Please apply 'ant format-diff' before commiting, or the extended version 'ant format-source'.
Scala is not upwards and not downwards compatible. The upcoming Ostrich library is only available for Scala 2.12, so we downgrade Scala for Princess.
This is an initial step and the usage is still unclear. This is not tested.
… theory and arrays. Princess intenally converts all real-arrays to int-arrays and thus there is some casting and quantification in SMT.
Princess needs non-rational UF arguments to be explicitly casted to rational.
… rationals (f.ex "1/3 <= y"). This extends the workaround we already use for terms to equations as Princess seems to have a bug when it comes to evaluating rational terms" This reverts commit 3b7229a
…variable by zero returns an integer term
…ese were temporarily disabled due to a bug that has now been fixed. See uuverifiers/princess#11
…. The problem here is that Princess introduces quantifiers when rationals are used, not that arrays can't be combined with rational numbers.
…upport division by zero, but it currently seems to be broken for rationals (at least with the way we're using them)
…incess to crash when non-linear terms are used" This reverts commit 3bc04a8.
| <orderEntry type="module-library"> | ||
| <library> | ||
| <CLASSES> | ||
| <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/ostrich_2.13.jar!/" /> |
There was a problem hiding this comment.
I guess the org.sat4j.core.jar and the ostrich-ecma2020-parser_2.13.jar are only called from these 2 new Jars?
There was a problem hiding this comment.
Yes, those are both dependencies of ostrich_2.13.jar and we never call them directly. Here is the section from the Ostrich ivy.xml:
<dependencies>
<dependency org="org.scala-lang" name="scala-library" rev="2.13.8" force="true" conf="compile->compile(*),master(*);runtime->runtime(*)"/>
<dependency org="io.github.uuverifiers" name="ostrich-ecma2020-parser_2.13" rev="1.3" force="true" conf="compile->compile(*),master(*);runtime->runtime(*)"/>
<dependency org="io.github.uuverifiers" name="princess_2.13" rev="2023-06-19" force="true" conf="compile->compile(*),master(*);runtime->runtime(*)"/>
<dependency org="org.sat4j" name="org.sat4j.core" rev="2.3.1" force="true" conf="compile->compile(*),master(*);runtime->runtime(*)"/>
<dependency org="org.scalacheck" name="scalacheck_2.13" rev="1.14.0" force="true" conf="test->runtime(*),master(*)"/>
<dependency org="dk.brics.automaton" name="automaton" rev="1.11-8" force="true" conf="compile->compile(*),master(*);runtime->runtime(*)"/>
</dependencies>
In fact we may want to remove automaton.jar as well as it is just another dependency?
| .withMessage("Solver %s does not support floor operation", solverToUse()) | ||
| .that(solverToUse()) | ||
| .isNotEqualTo(Solvers.OPENSMT); | ||
| requireRationalFloor(); |
There was a problem hiding this comment.
I guess checking once here is enough ;D
There was a problem hiding this comment.
Yes, it should be fixed now :)
| requireArrays(); | ||
| requireIntegers(); | ||
|
|
||
| IntegerFormula _i = imgr.makeVariable("i"); |
There was a problem hiding this comment.
_i is not a valid variable name according to our style guide.
There was a problem hiding this comment.
These variable names seem to be used for the entire class, though. Should I just rename all the variables, or would it be better to handle this somewhere else?
|
|
||
| @Override | ||
| protected IExpression floor(IExpression number) { | ||
| throw new AssertionError("floor is not supported in Princess"); |
There was a problem hiding this comment.
This looks like a UnsupportedOperationException.
|
|
||
| IExpression result = PrincessEnvironment.rationalTheory.mul((ITerm) number1, (ITerm) number2); | ||
|
|
||
| if (result instanceof IIntLit && ((IIntLit) result).value().equals(IdealInt.apply(0))) { |
There was a problem hiding this comment.
A comment for explaining this line would be nice.
| } else if (pTerm instanceof IFormula) { | ||
| return creator.getBoolType(); | ||
| } else { | ||
| // TODO: Do we need more cases? |
There was a problem hiding this comment.
It would be good to look into this before merging.
| IExpression evaluation = evaluate(formula); | ||
| if (evaluation == null) { | ||
| // fallback: try to simplify the query and evaluate again. | ||
| evaluation = evaluate(creator.getEnv().simplify(formula)); |
There was a problem hiding this comment.
What happens when simplify() is called for rationals?
There was a problem hiding this comment.
I've given it a try now, and unfortunately simplify() doesn't seem to solve the issue. The entire code here is meant to work around uuverifiers/princess#7 and uuverifiers/princess#8 in Princess and we might be able to simplify it again once these bugs have been closed.
| @@ -508,32 +540,69 @@ private static String getName(IExpression var) { | |||
| } | |||
|
|
|||
| static FormulaType<?> getFormulaType(IExpression pFormula) { | |||
| // TODO: We could use Sort.sortof() here, but it sometimes returns `integer` even though the | |||
There was a problem hiding this comment.
We should extract this into an issue so that we don't forget.
There was a problem hiding this comment.
I've opened a new Princess issue for this: uuverifiers/princess#16
| static Seq<ITerm> toITermSeq(IExpression... exprs) { | ||
| return toITermSeq(Arrays.asList(exprs)); | ||
| } | ||
|
|
||
| IExpression simplify(IExpression f) { | ||
| // TODO this method is not tested, check it! |
There was a problem hiding this comment.
Native solver tests seem appropriate considering there is some assumptions that we put on the behavior of the solver.
There was a problem hiding this comment.
Do you mean simplify here?
| new OstrichStringTheory( | ||
| toSeq(new ArrayList<>()), | ||
| new OFlags( | ||
| OFlags.$lessinit$greater$default$1(), |
There was a problem hiding this comment.
A comment explaining these would be nice.
There was a problem hiding this comment.
I've added the arguments and their default values by copying the description from Ostrich.
Thanks!
No, unforunately not. Ostrich does include a script to run it directly from the command line, however, internally this will still just call Princess. From our perspective it's probably best to see Ostrich as the String Theory module of Princess. |
…trich to the latest release
…FormulaManager, rather than an AssertionError
…sing bracket in PrincessStringFormulaManager
…String when trying to parse a \u{...} character with 5 digits. Such escape sequences are valid in SMTLIB, but can't be supported by us for Princess as we are restricted to the BMP in UTF16. We also added a test for this special case.
We're now evaluating formulas directly on the stack as there are several issues in Princess that block us from using the partial model with rational numbers. Once those issues have been resolved we can revert this change and move back to using the partial model.
… would unregister themselves from the prover while being closed by it.
Hello everyone,
the goal of this pull request is to add two more theories for strings and rational numbers to the Princess backend. It is a continuation of the work that went into #257. Some of the issues that blocked us from merging it back then have since been resolved, and at least the rational formula manager is actually starting to look pretty good now. Here is a comparison between Princess and some other solvers when running BMC on the
ReachSafety-Floatstask with optioncpa.predicate.encodeFloatAs=RATIONALset to test the rational formula manager:It's a bit harder to evaluate how well the String manager is working now. The Ostrich team has been very helpful and they quickly fixed a couple of bugs that we've reported. However, since CPAchecker doesn't use String theory there is no easy way of trying it out.
Linked issues:
Princess (Rationals)
Ostrich (Strings)
I've added (partial) workarounds for the two Princess issues, but some work may still be needed. For Ostrich the biggest limitation is that the solver can only handle constraints where (at least) one of the sides is a singleton (= constant) string. Something like "a str.<= b" where both
aandbare variables is already impossible. This is a known issue and they're planning a redesign for the solver that will allow it to handle such constraints. In the mean time we might want to add some additional error messages to make sure that the user knows why their program is failing.