Bitvector Expressions are a second class citizen in Boogie and this needs to change

Nov 27, 2014 at 8:08 PM

Bitvector support really feel like a hack in Boogie
  • You have to declare bitvector functions yourself in Boogie programs. This is annoying and I don't see a good reason for this restriction. I think the bitvector functions should all be implicitly declared and be documented.
  • The form that bitvectors need to be declared in painful to use. E.g.
function {:bvbuiltin "bvadd"} BV32_ADD(bv32, bv32) : bv32;
This form is not documented ("This is Boogie2" shows a different syntax which is wrong) and once the program is parsed, working with these NAryExpr is incredibly annoying to work with. I have to look for a string attribute on the Function attached to the FunctionCall attached to the NAryExpr to figure out what the function is.

I'd like to propose we do the following.
  1. Add the relevant bitvector operator Opcodes to BinaryOperator and UnaryOperator.
  2. Teach the Boogie parser when it sees a function with the {:bvbuiltin} attribute to throw it away and instead add an entry to a "string" -> "opcode" map that will be used later on during Expression construction by the parser to create an NAryExpr with the correct operator. We obviously we need to teach the type checking methods how to handle these new operators. I'm not entirely sure how "resolving" would work now. I think this would mean you would need to declare bitvector functions before you use them in a Boogie program.
The result of this would be that Boogie programs would not need to change but the in memory representation of the bitvector functions would be much more sane.
  1. Introduce implicit names for the bitvector functions so they do not need to be declared in a Boogie program. We would also emit warning messages if the "bvbuiltin" attribute was found in the function but we will still treat calls to that function as the intended bitvector operator.
  2. Drop support for using explicit bitvector functions entirely by having the parser emit an error if the "bvbuiltin" attribute is used. This would be a long term goal and would probably require a slow transition.
Nov 27, 2014 at 9:03 PM
I really like this proposal.