Open
Description
The program
type MyBv20 = bv20
method Test() {
var d: MyBv20 := 0;
d := 0 - d; // this is translated correctly into Boogie
d := -d; // this ought to generate the same thing, but generates malformed Boogie
assert d == 0;
}causes a crash:
$ dafny test.dfy
(0,-1): Error: invalid type for argument 0 in application of sub_bv20: int (expected: bv20)
1 type checking errors detected in test__module.bpl
*** Encountered internal translation error - re-running Boogie to get better debug information
test__module.bpl(2895,20): Error: invalid type for argument 0 in application of sub_bv20: int (expected: bv20)
1 type checking errors detected in test__module.bpl
Internally, Dafny rewrites a unary-minus expression -x into 0 - x. But this 0 needs to have the right type. In this example, the 0 should have a bitvector type. Apparently, this is not done correctly. It does work if the input program uses type bv20 instead of the type synonym MyBv20:
method ThisWorks() {
var d: bv20 := 0;
d := 0 - d;
d := -d;
assert d == 0;
}So, I'm guessing the code that assigns the type to the 0 in the rewriting of unary-minus expressions neglects to expand type synonyms before doing the type test. The way to do this properly is to use the .IsBitVectorType property on the type.