Missing features and/or potential bugs (willing to fix)

[leventeBajczi]

Hi!

I'm in the process (ftsrg/theta#258) of integrating JavaSMT with our Theta model checker. By doing so, I have discovered some pain points of the integration, which I'd like to both log as a potential issue and discuss in terms of what I can do to help these get resolved. I'm more than happy to try and create a PR about the changes, but wanted to discuss first.

I know that most of these problems are easily solved using some workarounds, but I think there is value in getting them implemented / fixed.

In no particular order the missing features (keep in mind that it is entirely possible that I just missed some :) ):

1. The conversion between Rational and Integer sorts in this direction is given by the .floor() operation, but there is no inverse operation, despite Z3 having a .mkInt2Real, SMT-LIB defining a to_real, etc. I can see some signs of support for this operator (e.g., here), but I see no way of creating this formula otherwise.

2. There is no support for rotating (either left or right) a bitvector. Some solvers (including Z3 and CVC4) have support for these operators, and for others, it can be (expensively) emulated. However, emulating it for supporting solvers is way too big of an overhead.

3. fp.rem is not supported.

4. I see no way of creating array literals, therefore I cannot translate the following assertion: (assert (= 0 (select ((as const (Array Int Int)) 0) 0))).

5. I see no way of creating a floating point literal from a IEEE-754 bit pattern without first creating the bitvector literal, then using the fromIeeeBitvector. Consequently, I also miss a way of retrieving the bit pattern from a floating point literal.

And the (potential) bug:

6. Modulo creates REM operator instead of MOD for bitvectors. See relevant code here. This is potentially dangerous, because (at least) I would think that a .modulo() function will use the bvsmod operator, and not one of the {s,u}rem operators. Consider the following as an example for why this matters:

(declare-fun a () (_ BitVec 2))
(declare-fun b () (_ BitVec 2))

(assert (not (= (bvsmod a b) (bvsrem a b))))

(declare-fun c () (_ BitVec 2))
(declare-fun d () (_ BitVec 2))

(assert (not (= (bvsmod c d) (bvurem c d))))

(check-sat)
(get-model)

There are satisfying assignments to all variables (meaning smod corresponds to neither urem nor srem) , and in those cases, a wrong result would have been created, should the user not look at the internals of JavaSMT. I think this should be changed.

Again, I'm more than happy to provide a fix for these as a PR. However, I would like to get some feedback on the points above, especially regarding which might be a misunderstanding on my part rather than a missing feature / bug. Thanks!

[kfriedberger]

Hi.

This is quite a long issue, so I will answer in smaller parts. See below.

1. The conversion between Rational and Integer sorts in this direction is given by the .floor() operation, but there is no inverse operation, despite Z3 having a .mkInt2Real, SMT-LIB defining a to_real, etc. I can see some signs of support for this operator (e.g., here), but I see no way of creating this formula otherwise.

Integers are a subset of Rationals. Thus, JavaSMT and most SMT solvers (including Z3) allow to use Integers directly without any casting in rational-based operations. We only need to handle very specific cases, where the SMT solver strictly separates Integer and Rational theory and requires explicit user-given conversion.

2. There is no support for rotating (either left or right) a bitvector. Some solvers (including Z3 and CVC4) have support for these operators, and for others, it can be (expensively) emulated. However, emulating it for supporting solvers is way too big of an overhead.

Nobody requested rotation until now. This seems to be useful. We can add rotation to JavaSMT.

3. fp.rem is not supported.

Same here: Nobody requested fp.rem until now. Testing fp.rem for 32bit and 64bit fp-type should be simple. Other fp-types might be complex to be tested.

4. I see no way of creating array literals, therefore I cannot translate the following assertion: (assert (= 0 (select ((as const (Array Int Int)) 0) 0))).

Nobody requested this until now. This is a special case, because most users want to have a "unknown" array as variable/symbol, not as literal. I do not see a problem adding it to JavaSMT's API.

5. I see no way of creating a floating point literal from a IEEE-754 bit pattern without first creating the bitvector literal, then using the fromIeeeBitvector. Consequently, I also miss a way of retrieving the bit pattern from a floating point literal.

In other words: You want to request a new method FloatingPointFormula makeNumber(String bv, FloatingPointType type) where the string is a bitvector-representation of matching length. I see no problem to add such a method.
For retrieval, I am not sure about the use-case. In models, you should get a Java-Float/Double or String anyway. Where and why do you want to access the literal?

6. Modulo creates REM operator instead of MOD for bitvectors. See relevant code here. This is potentially dangerous, because (at least) I would think that a .modulo() function will use the bvsmod operator, and not one of the {s,u}rem operators. Consider the following as an example for why this matters:

(declare-fun a () (_ BitVec 2))
(declare-fun b () (_ BitVec 2))

(assert (not (= (bvsmod a b) (bvsrem a b))))

(declare-fun c () (_ BitVec 2))
(declare-fun d () (_ BitVec 2))

(assert (not (= (bvsmod c d) (bvurem c d))))

(check-sat)
(get-model)

There are satisfying assignments to all variables (meaning smod corresponds to neither urem nor srem) , and in those cases, a wrong result would have been created, should the user not look at the internals of JavaSMT. I think this should be changed.

JavaSMT's history with CPAchecker comes from C-code verification, and it started from Integer-based formulas, where the appropriate choice was to implement modulo as remainder. Perhaps, this was not optimal according to SMTLIB. Changing this method only internally is a breaking API-change that is hard to detect. We will think about it. A possible solution would be to remove (deprecate) the current method and add div/rem as separate methods.

Again, I'm more than happy to provide a fix for these as a PR. However, I would like to get some feedback on the points above, especially regarding which might be a misunderstanding on my part rather than a missing feature / bug.

Feel free to provide one or more PRs, separated by topic, if possible.

Best,
Karlheinz

[leventeBajczi]

Integers are a subset of Rationals. Thus, JavaSMT and most SMT solvers (including Z3) allow to use Integers directly without any casting in rational-based operations. We only need to handle very specific cases, where the SMT solver strictly separates Integer and Rational theory and requires explicit user-given conversion.

That's right, I was blinded by our own implementation that does not allow this.

Nobody requested rotation until now. This seems to be useful. We can add rotation to JavaSMT.

Same here: Nobody requested fp.rem until now. Testing fp.rem for 32bit and 64bit fp-type should be simple. Other fp-types might be complex to be tested.

I'll work on these then.

In other words: You want to request a new method FloatingPointFormula makeNumber(String bv, FloatingPointType type) where the string is a bitvector-representation of matching length. I see no problem to add such a method.
For retrieval, I am not sure about the use-case. In models, you should get a Java-Float/Double or String anyway. Where and why do you want to access the literal?

I need the actual value of the literal for transforming it back into our own representation of floats (for which we use mpfr and the BigFloat library). We need this to perform arbitrary-precision, IEEE-754-conformant calculations inside Theta.

I'll also try and come up with a suggestion on how I'd like this to be implemented in a PR, and then we can discuss there whether you think it's OK.

Thanks for the detailed responses!

[leventeBajczi]

Also,

JavaSMT's history with CPAchecker comes from C-code verification, and it started from Integer-based formulas, where the appropriate choice was to implement modulo as remainder. Perhaps, this was not optimal according to SMTLIB. Changing this method only internally is a breaking API-change that is hard to detect. We will think about it. A possible solution would be to remove (deprecate) the current method and add div/rem as separate methods.

I think that longer term the deprecation way should be preferred. I'll implement this as a suggestion in a PR, and we can continue the discussion there.