Spacer: error "query failed: Uninterpreted 'mod' in <null>

[leonardoalt]

smt2 file:
https://gist.github.com/leonardoalt/ab12713eb249dadb86f7bb1441705e59

@agurfinkel we once talked about cex not working super well when using nonlinear arithmetic, but this didn't happen before (this happened now on a regression test).

$ z3 mod.smt2 
(error "query failed: Uninterpreted 'mod' in <null>:
summary_0_function_g__19_20_0(#2,#1,#0) :- 
 block_2_g_18_20_0(#11,#1,#0,#3),
 (>= (:var 0) 0),
 (<= (:var 0)
    115792089237316195423570985008687907853269984665640564039457584007913129639935),
 (= (:var 4) (:var 0)),
 (= (:var 5) 1),
 (let ((a!1 (mod (+ (:var 4) (:var 5))
                (+ (- 0 0)
                   115792089237316195423570985008687907853269984665640564039457584007913129639935
                   1))))
(let ((a!2 (ite (> (+ (:var 4) (:var 5))
                   115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!1
                (ite (< (+ (:var 4) (:var 5)) 0) a!1 (+ (:var 4) (:var 5))))))
  (= (:var 6) a!2))),
 (= (:var 7) (:var 6)),
 (= (:var 8) (:var 7)),
 (= (:var 9) 0),
 (= (:var 10) (> (:var 8) (:var 9))),
 (= (:var 2) (:var 11)),
 (= (:var 3) 0).
")
unknown

[agurfinkel]

Spacer does not deal properly with uninterpreted functions. Non-linear mod is treated as UF. This used to "work". But recent fuzzing required being more aggressive at excluding benchmarks that include potentially unsupported features.

In your case, the mod seems interpreted. Let me check with @NikolajBjorner on best course of action.

@NikolajBjorner : the error message is wrong. I think the check does not simplify the argument to mod. We can add a method like is_value_expr that checks that an expression simplifies to a value. But I am not sure how best to do this since it probably needs to be theory specific (e.g., is_arith_value_expr)

[leonardoalt]

Thanks!

It still happens though, with both mod and div.
Here are two samples:

mod: https://gist.github.com/leonardoalt/a9951c60f44ec4e059c623f8530c4ba5
div: https://gist.github.com/leonardoalt/79f72a45c69b1a901149ab7b757e5402

[NikolajBjorner]

They have occurrences where the second argument to mod/div is a variable.
The Horn clause solvers are not well behaved then because of the way they handle interpretations to uninterpreted functions. Instead of giving potentially unsound results, the filter bails out.
It is generally annoying, but deeply ingrained.
Perhaps a way is to declare a default semantics to these functions,
such as mod(x, 0) = 0 for every x. This is available for hardware operations
(division/rem/mod). It is still a bit of a support issue to get right.

[leonardoalt]

@NikolajBjorner would it make sense to reopen the issue to track that?

[agurfinkel]

@NikolajBjorner this, and maybe other protections, for supported features seems too harsh for current users. In SeaHorn case, for example, it is assumed that for every mod(x, y), y is non-zero, although it might be hard to prove locally. It seems that we also disallow the usual local protections using terms such as if (y != 0) then mod(x, y) else 0.

An alternative is to allow arbitrary signature on entry, but make fp.validate=true be the default. The option checks the result at the end and returns unknown if the result does not validate.

We can even require fp.validate=true only in the case that the input does not pass some rule validation logic.

What do you think?

[NikolajBjorner]

You could remove this check from rule_properties and add validation
when the solver is invoked from the horn tactic.
This Horn tactic is the entry point in Z3 where the contract is to be sound, that is,
compatible with SMTLIB2 semantics.

[leonardoalt]

@NikolajBjorner you mentioned above that They have occurrences where the second argument to mod/div is a variable. (regarding the examples that I posted).
What if that's the case, but the second argument has an equality to a constant, is there a way I could make that work together?
Such as:

(and (div x y) (= y 2))

[agurfinkel]

Hey @leonardoalt , this is on my plate as per discussion above. Are you using spacer through the horn tactic? If you use it directly, I believe this check is by-passed. (i.e., via Fixedpoint interface).

The source of the problem is that the decision is made syntactically. There will always be a possibility that after some more pre-processing offending terms will disappear.

What I want to do is to add an optional validation of the solution before it is returned to the user. The logic will then be instead of "if there is an offending term return unknown" into "if there is an offending term run validation before returning to the user".

The hope is to start working on this in the next few weeks. But this has been a low priority for me since I don't know of many users of CHC with non-linear div constraints except for the fuzzers. It will always be better if you can fix it at the encoding level (i.e., substitute y for 2 before sending it to z3, especially if you have some domain specific knowledge of when and how to do it.)

[leonardoalt]

@agurfinkel that sounds good, thanks!
I'm using it directly via the fixedpoint class. I find the API to be easier to construct the model of the program that way.

Right, that makes sense. I'll try to substitute the terms before the query. For me the nonlinear cases are not too important, since they're too hard anyway. My current use cases include division by 2 for binary search, for example.

[agurfinkel]

The more simplification you do before you go to the solver, the more robust your results will be. For example, current pre-processing rules should eliminate y, but (I think) the rule check happens before this pre-processing step.

[leonardoalt]

Ok. I think a fairly easy way for me to do that is to run the SMT solver on the constraints of a block (Horn rule) that contains a division, before adding the rule.

[markusscherer]

Hello @agurfinkel!

Since you where wondering how many people are using CHC with non-linear div constraints I wanted to provide another data point: we are using them in our static analysis framework HoRSt, but it seems that for most real world cases, we can get rid of them by doing some pre-processing.

[leonardoalt]

FYI I've replaced div and mod operations by a multiplication + extra constraints, has worked well so far with Spacer.
Please feel free to close the issue.

[markusscherer]

While discussing @wert310's recent pull request (#5821) he and I had the idea that this issue could be solved in a similar manner (basically we could allow div and mod in cases that are somehow "guarded" (either in the correct ite branch or with and and or). Would a pull request with additional syntactical checks be welcome or is solution mentioned here still planned?

As a side note: If one was sure that all div and mod applications are properly guarded, would running z3 with a patched out syntactical check be sound?

[agurfinkel]

Yes, as long as there are no uninterpreted functions, spacer will be sound. In fact, in our applications that is exactly what we do -- ensure that all div and mod are guarded. However, fuzzing exposed that simply leaving those operators unprotected is not a good solution.