Backend support for SMTLib types (particularly bitvectors and floats)

[viper-admin]

Pull request 🔀 created by @marcoeilers on 2019-07-23 17:02
Last updated on 2019-07-29 15:54
Original Bitbucket pull request id: 127

Participants:

• @alexanderjsummers (reviewer)
• @vakaras (reviewer) ✔️
• @marcoeilers
• @mschwerhoff (reviewer)

Source: 071af4a on branch meilers_smt_types
Destination: a384ea0 on branch master

State: OPEN

This PR adds backend support for theories supported by SMTLib (in Silicon’s case) and Boogie (in Carbon’s case) to Viper. In SMTLib, there are a number of such types, but afaik Boogie only supports bitvectors and IEEE floating point numbers.

The PR adds additional nodes to the AST to represent the corresponding types and functions, and there are PRs for Silicon and Carbon that teach the backends how to translate those types and functions. There is no integration with the parser (yet), so those types and functions can be used only by frontends that directly create the AST nodes.

In particular, there are the following additions:

• SMTType(boogieType, smtType): Represents a type with name “boogieType” in Boogie and name “smtType” in SMTLib.
• SMTFunc(name, smtName, type, formalArgs): A function that is called “smtName” in SMTLib and can be referred to inside the Viper Program as “name”. The distinction between internal name and Viper name is helpful because SMTLib overloads function names, e.g. function “bvxor” XORs bitvectors of different lenghts, so one might want to use different function names “bvxor32” and “bvxor16” for bitvectors of length 32 and 16, respectively.
• SMTFuncApp(smtFunc, args): Applications of those functions. Note that SMTFuncs do not have to be defined explicitly in the Viper Program, they are only referred to by SMTFuncApps.
• Factory classes BVFactors(size) and FloatFactory(exp, mant, round) that give convenient access to types and functions for bitvectors of a given size, as well as floats of a certain type (i.e., a given number of bits for the exponent and the significand, and a given rounding mode).

[viper-admin]

@vakaras commented on 2019-07-29 15:00

Outdated location: line 393 of src/main/scala/viper/silver/ast/Expression.scala

Why we need with PossibleTrigger here?

[viper-admin]

@vakaras commented on 2019-07-29 15:03

LGTM

[viper-admin]

@vakaras approved ✔️ the pull request on 2019-07-29 15:03

[viper-admin]

@vakaras commented on 2019-07-29 15:04

Silicon pull request: viperproject/silicon#472

Carbon pull request: viperproject/carbon#345

[viper-admin]

@marcoeilers commented on 2019-07-29 15:46

Outdated location: line 393 of src/main/scala/viper/silver/ast/Expression.scala

Why we need with PossibleTrigger here?

Whoops, copy-paste error, I’ll remove it.

[mschwerhoff]

I'm not overly thrilled about including the Boogie type name as well. How cumbersome would it be if it were left to Carbon (or any other Boogie-based backend) to translate from SMT name to Boogie name?

[marcoeilers]

Boogie just has support specifically for bitvector and float types, so it cannot work with an arbitrary SMT type. So one could do what you suggested, but one would have to look for these two specific kinds of types and then just fail on anything other than those specific types, that would work.
We could also just rename it from SMTType to BackendType or something like that, I agree that it's quite weird that something called SMT type contains something Boogie-related and is pretty-printed using its Boogie name.

[mschwerhoff]

If we allow arbitrary SMT types (or "backend types"), it either way seems unavoidable that backend verifiers would have to perform consistency checks to reject programs with backend types they don't support.

[marcoeilers]

Yes, I agree.

[mschwerhoff]

Is it really the Boogie name we want to use? Seems odd, since the extension is about SMT types.

[marcoeilers]

I figured the Boogie name would be less confusing because SMT type names can look a bit weird. float24e8 just looks more like a type to me than (_ FloatingPoint 8 24). But I don't really have a strong opinion on that.

[mschwerhoff]

I agree, the SMT type name is really no eye candy. Does the parser also expect the Boogie name format?

Maybe we could only use the Boogie type names, and backends (Silicon) would have to map them to SMT, if necessary, potentially with the help of some Silver function.

[marcoeilers]

This is currently only in the AST for frontends to use, there is no support for this on the source level, the parser doesn't know about this.
Actually, because it's currently not accessible from the source level I basically thought it's okay if there is basically no consistency checking from the backends (I wouldn't really want Silicon to have to know exactly which builtin types and functions Z3 or SMTlib contains and supports); anyone who uses this is building a frontend and should really know what they're doing. I added the factory for bitvector and float types and functions so that those are easy to get right.

Use only Boogie names: Yeah sure, we could do that. Then we would lose the option of using types that exists in Z3 but not in Boogie, though.

[mschwerhoff]

If we wanted to merge more or less as-is, we could probably describe the feature as (very) experimental, and see what happens. Or just not document it at all :-)