search

boogie-org / boogie

Boogie
http://research.microsoft.com/en-us/projects/boogie/
MIT License
510 stars 112 forks source link

Unexpected prover response getting model when using cvc4 #370

Closed kbansal closed 3 years ago

kbansal commented 3 years ago

Symptom: Error message "Prover error: Unexpected prover response getting model" when using -proverOpt:SOLVER=cvc4

Issue:I have narrowed down the issue, and I believe the issue is in https://github.com/boogie-org/boogie/blob/master/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs#L1737 (boogie expects cvc4 get-model output to start as (model ...) but output is just (() (define-fun ...)) (in particular, resp.Name is just "")

Additional info: The latest version of CVC4 (v1.8), get-model output does start with (model....). This only seems to happen with the prerelease version 1.9 of cvc4. That said, I looked into SMTLIB standard and it seems that this is CVC4 becoming more SMTLIB compliant, as the standard doesn't have 'model' in the output. So the fix should be on Boogie side to support SMTLIB compliant output.

Boogie file to reproduce issue: output_cvc4.bpl.zip

Full command to reproduce:

boogie -trace -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -monomorphize -proverOpt:SOLVER=cvc4 -proc '$TestArithmetic_div_by_zero_u64_incorrect$verify' output_cvc4.bpl

Versions: CVC4 version 1.9-prerelease [git master aac53f51] Boogie program verifier version 2.8.29.0

kbansal commented 3 years ago

I don't have a build environment working (I tried installing dotnet core for Mac, and building using instructions in the README, but that only generates a BoogieDriver.dll, not the binary).

In any case, here is the patch (renamed to txt for uploading) that I wanted to test out and think should fix the issue. 0001-Fix-for-getting-model-when-using-cvc4.patch.txt

shazqadeer commented 3 years ago

@kbansal : I have the same problem on my Mac that only BoogieDriver.dll is generated. There is an easy workaround. See the following script I wrote:

#!/bin/sh

/Users/shaz/.dotnet/dotnet /Users/shaz/Source/boogie/Source/BoogieDriver/bin/Debug/netcoreapp3.1/BoogieDriver.dll "$@"

The composition of the dotnet binary and BoogieDriver.dll acts as the executable binary.

shazqadeer commented 3 years ago

The patch looks fine to me. Please put up a PR.

kbansal commented 3 years ago

Thanks for the tip about running on Mac, that worked.

Now that I have boogie running, I conclude that even though the above patch is needed; it is not sufficient for getting boogie to complete without error on the boogie file in question.

I have dug into it a little bit, and I will add some more details in another comment after creating the requested PR.

kbansal commented 3 years ago

With the patch above, though it will fix model parsing for some boogie files; it is not sufficient for the one mentioned in this bug (output_cvc4.bpl.zip).

The new boogie error is "Prover error: Unexpected value: $Error".

It is being generated in here: https://github.com/boogie-org/boogie/blob/ed0a67f967c9db3b66d6fb40f243a8d0b56888ee/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs#L1518

With some additional logging, I concluded the issue is that the DataTypes dictionary of SMTErrorModelConverter is actually empty. I do not know why. But that is why it doesn't go down the datatypes handling and thus fails to parse $Error.

The CVC4 model output part that it was trying to parse and fails is the following:

(define-fun |Select_[$int]$Value| ((BOUND_VARIABLE_5658 |T@[Int]$Value|) (BOUND_VARIABLE_5659 Int)) T@$Value $Error)

I won't have time to look into this further, but hopefully this is helpful!

shazqadeer commented 3 years ago

Yes, your feedback is helpful. I will dig further.