search

boogie-org / boogie

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

Bug in monomorphization #353

Closed wrwg closed 3 years ago

wrwg commented 3 years ago

The BPL file bpl.zip produces the following errors when run by Boogie: 

Prover error: line 22 column 19: invalid datatype declaration, unknown sort 'T@$TypeName'

Prover error: line 22 column 19: invalid datatype declaration, unknown sort 'T@$TypeName'

Prover error: Prover died

...

Command line (after unzipping):

boogie -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -proverOpt:PROVER_PATH=/home/wrwg/bin/z3 -proverOpt:O:smt.QI.EAGER_THRESHOLD=100 -proverOpt:O:smt.QI.LAZY_THRESHOLD=100 -vcsCores:12 output.bpl

The culprit seems to be the application of the generic function function $ForceTrigger<T>(x: T): bool { true }. I have tried to nail this down to a smaller use case but was not able to do so.

@shazqadeer

shazqadeer commented 3 years ago

Please add -monomorphize option to the command line. When I add that option, I get the following output:

Boogie program verifier finished with 5 verified, 0 errors

Regardless, the output you see is not ideal. I will look into providing a better error message.

shazqadeer commented 3 years ago

The root problem is that datatypes and generics do not work together currently. So, if both are used in the same file then monomorphization must be enabled using the flag I mentioned. Monomorphization is turned off by default because currently only generic functions and datatypes are supported; generic procedures and implementations cannot be monomorphized right now.

shazqadeer commented 3 years ago

@wrwg :

I just merged a PR that should provide a better error message if datatypes and generics are combined without using monomorphization.

Boogie also supports a flag -lib which automatically links a collection of useful libraries including finite vectors with native equality. See here for an example. If you use -lib on the command line, -monomorphize is implied.