Eliminating polymorphism in Boogie

[shazqadeer]

The implementation of polymorphism in Boogie is complex because it introduces quantifiers and encodes all types into a single type. This complexity discourages Boogie users from exploiting this potentially useful feature. At the same time, the existing implementation is inadequate for fully encoding source-level polymorphism of a language such as Dafny. It is time to revisit the feature, potentially eliminate the current implementation, and start afresh. I am creating this issue so any users of could voice their concerns.

@RustanLeino : Thoughts? If you know of other users of Boogie polymorphism, please inform them that we are considering dropping support for this feature.

[mueller55]

Dear Shaz, I am not sure I fully understand your post. Are you suggesting to find a different encoding of polymorphic types or are you proposing to drop polymorphism from the Boogie type system altogether (possibly going back to an "any" type like in the initial version of Boogie)?

[shazqadeer]

I was being vague in the initial post. Thanks for the response and the suggestion to sharpen the discussion.

I would like to remove the "polymorphic map" feature entirely. This feature is much more complex than the rest of polymorphic Boogie, which is based on parametric polymorphism found in other languages. The polymorphic map feature was added to address a specific use case: encoding the heap of an object-oriented language. However, this feature was not enough to address the encoding needs of Dafny and more encoding had to be done on top of it. In summary, this feature is complex, narrow, and inadequate.

I am unsure about what to do about the other polymorphic features in Boogie. The current situation is untenable because even the translation of a Boogie program that does not use type parameters introduces quantifiers in the verification condition. To avoid quantifiers for a non-generic Boogie program, the user has to use the command-line flag /typeEncoding:m, a poorly-understood hack implemented by me many years ago. There is also another related mysterious flag /monomorphize whose purpose is unclear to me.

Overall, the Boogie community should try to answer the following questions:

• Does polymorphic Boogie aid the development of verifiers for polymorphic source languages? Based on the experience so far, the answer does not appear to be Yes. @RustanLeino informs me that he had to do a ton of work in the Dafny verifier to encode its polymorphic features in spite of the availability of polymorphic features in Boogie. He observed that even if all polymorphic features in Boogie were dropped, he could address the gap in the Dafny implementation with a modest amount of work. This is rather surprising and might indicate that source-level polymorphism interacts with other language features which makes it difficult to directly use Boogie-level polymorphic features.

• Does polymorphic Boogie aid users who model directly in Boogie? Although Boogie is primarily an Intermediate Verification Language, I find it useful to model directly in Boogie to understand a particular verification problem without the overhead of compiling from a source language. For example, the Civl verifier is implemented directly atop Boogie (using attributes) without any source language.

If the answer to either question above is Yes, then we should answer the following question:

• How do we translate polymorphic Boogie to verification conditions in a way that adds complexity in a predictable manner? An example of unpredictable complexity is that addition of polymorphism causes even translation of non-generic Boogie programs to get more complex.

[alexanderjsummers]

Hi Shaz and all,

Thanks a lot for raising the topic and explaining in so much detail. Sorry that I'm a bit late to the party, but I'm hopefully getting up to speed now that I'm back online.

In short, my opinion is that I'd really like polymorphism to stay in Boogie in some form. I have basically two reasons, which correspond to your two questions in your last post.

Firstly, we use Boogie's polymorphism for one of the two main verification pathways in Viper. We have two verifiers for Viper programs: one performs symbolic execution and interacts directly with Z3; the other translates Viper programs to Boogie programs and verifies them with the standard Boogie verifier.

In the Boogie-based verifier, we use polymorphic features for the following (I'm assuming types with parameters are included in the discussion, as well as explicit quantification over types):

1. Modelling language features which naturally have type specialisations (in particular, field types). So the Boogie types modelling Viper fields have a type parameter corresponding to the translation of the field's type.
2. Simulating refinement/union types. We actually use a second type parameter for what we call fields in our Boogie encoding, so that heaps can be a single map with a uniform type, even though conceptually these maps store several kinds of information all at once (values of Viper fields, information about predicate instances, etc.); effectively, we simulate a union type using a second type parameter which selects the kind of field involved.
3. On heap types and similar maps themselves. Given the setup described, our heap representations quantify over two type parameters. Furthermore, some field types are such that program heaps or similar maps can be stored there as values. We have a similar situation for several other maps used in our encoding (in Viper parlance, we track the resources held in the program in different maps from the one representing the actual heap.
4. Modelling built-in mathematical types which are themselves polymorphic (Viper builds in sets, sequences and multisets using axioms similar to Dafny's; these are all polymorphic types at the Boogie level).
5. (a bit similar to the previous, but more-complex) Encoding user-defined types: Viper allows so-called "domains" to be declared in a program, effectively defining a new uninterpreted type concerning which uninterpreted functions and axioms can also be declared. These domain declarations can have type parameters, and instantiation of these types is implicit (as in Boogie); one just uses the instantiated type (which in some cases might be another type parameter if the usage is inside a domain declaration), and the correct instantiation is found.

I think point 5 is the hardest to work around, in the sense that I'm not even sure what one would do as an alternative. In fact, in our symbolic execution verifier we have exactly this issue: since we interact directly with Z3 we don't have the luxury of Boogie's polymorphic types for handling type instantiations. Instead, we've attempted to pre-instantiate the polymorphic types in the input Viper program, using a heuristic approach which we believed to be complete in practice, but have since found to create issues in certain examples, which are then hard to debug (e.g. this issue). Of course, it ought somehow to be possible to lift/generalise the approach that Boogie currently uses to the Viper level, but that would seem a shame to have to do.

For the other points (particularly 1-3) above, I'm pretty sure there would be workarounds that would make our encoding a lot more verbose. My recollection from developing/working on these encodings is that particularly the places where we used Boogie's polymorphic features were quite prone to trivial mistakes (e.g. by me), and that Boogie's type checker called us out on these. I'm a bit afraid that those mistakes would in some cases become subtle verification errors instead (although I haven't thought the alternatives through fully yet), and if so that would certainly be scary.

As a less important remark, we have also considered trying out exchanging alternative heap/map representations in our Boogie encoding (cf. Böhme and Moskal's quite old paper); it's currently quite straightforward (if a little tedious) to go between situations in which we use several related maps with slightly different signatures or one map to rule them all with a signature coerced to subsume them (using extra type parameters to simulate unions, as in point 2), and vice versa. I don't think this would be the case any more without polymorphism (effectively one would be forced into the more verbose many-maps representation, or else forced to have less actually type checking performed by using a more-coarse type encoding (which I think will lead to subtle bugs).

So far we didn't encounter any limitations with respect to what we wanted to encoding in Boogie (perhaps some things would be more natural with (tagged) union types, but considering how much indirect modelling is already done, it doesn't really seem warranted). I'd be interested to understand what limitations were hit when trying to reuse these features for Dafny, but for Viper (which is still an intermediate language with quite simple types), Boogie's polymorphism is currently a great fit.

Finally (this is the top-level "Secondly"!), I've used Boogie for teaching (as the middle of the toolchain used in this course). In particular, I use it for teaching how to model program verification constructs, and to head towards the kind of verification we do by modelling program heaps of various kinds. I use polymorphism in simplified ways of all of the points above, I think, and it makes the code extremely clear to read and teach. If this weren't possible any more, I'm not sure what I'd use instead; Viper doesn't have maps built in (and builds in a heap, so simulating a heap with maps seems a bit strange); I guess I could use Dafny directly, but for teaching the role of an intermediate verification language in this toolchain, it seems a strange choice.

Well, that got kind of long, but hopefully it helps the discussion. As a potential remark in the other direction, I do often observe that slow examples we debug with the Axiom Profiler tend to have tons of instantiations of type-related Boogie-generated axioms. But I wasn't yet able to persuade myself that this was the actual cause of performance issues in any of the debugged examples (they all had non-trivial other axioms which were instantiated a lot, and seem to contribute more more-relevant terms to the e-graph).

[alexanderjsummers]

I realise I didn't answer your last question. I'd be very happy to brainstorm on this together sometime if it would be useful! Just as a basic question, is there a reason why current Boogie couldn't simply omit various internally-generated axioms when the input program doesn't make use of polymorphic features?

[zvonimir]

Kind of related to this, Boogie has a PolymorphismChecker (see https://github.com/boogie-org/boogie/blob/master/Source/ExecutionEngine/ExecutionEngine.cs#L359) that gets invoked on every program. If the checker concludes that the program is monomorphic, then it automatically sets type encoding to be monomorphic under the hood (https://github.com/boogie-org/boogie/blob/master/Source/ExecutionEngine/ExecutionEngine.cs#L737).

So I would say that setting /typeEncoding:m is not needed for monomorphic programs since it is going to be set automatically by Boogie anyways. We should probably document this somewhere.

This was probably done so that Boogie does not introduce auxiliary axioms related to polymorphism when they are not needed, meaning then the input program is monomorphic.

[shazqadeer]

@alexanderjsummers:

Just as a basic question, is there a reason why current Boogie couldn't simply omit various internally-generated axioms when the input program doesn't make use of polymorphic features?

@zvonimir is working on a PR #234 that will clean up the menagerie of command-line options related to monomorphic type encoding. Once this PR lands, the issue of monomorphic Boogie will be settled. If the input program is monomorphic, then automatically no type encoding will
be done.

Question: Boogie currently supports polymorphic maps such as the following:
type HeapType = [Field a]a;
Do you use polymorphic maps in any of your toolchains? I am not certain of the answer from reading your post.

[shazqadeer]

If we keep the support for polymorphic features in Boogie, is there any interest in an encoding that compiles away the polymorphic features via code duplication? On one hand, such an encoding is likely to be simpler since it continues to use the native types supported by solvers. On the other hand, code duplication will result in many more verification conditions being generated.

[zvonimir]

Just to be clear, polymorphic maps will work even after the pull request gets merged in (I did not change that part), but not with the theory of arrays (/useArrayTheory flag). That functionality wasn't working reliably even in the current Boogie version.

@alexanderjsummers I think it would be a good to add a few small Viper-generated regressions into the Boogie repo that contain most, if not all, of the Boogie features and flags you rely on. That would guard against someone breaking the features you guys use. Just my 2 cents.

[gauravpartha]

@shazqadeer

Do you use polymorphic maps in any of your toolchains? I am not certain of the answer from reading your post.

I guess I can speak for @alexanderjsummers (I am also part of the Viper team). Yes, we do. For example, we have the following type for the heap:

type Field A B;
type HeapType = <A, B> [Ref, Field A B]B;

This is not the only place where we use polymorphic maps.

@zvonimir That's a good point, thanks! I'll make a pull request.

[shazqadeer]

Boogie (master branch) now supports monomorphization of functions, procedures, and implementations. You can take a look at the folder Test/monomorphize and file Test/inst/vector_generic.bpl for examples. You can also see the monomorphized program for yourself by using the option /printInstrumented.

The current implementation supports polymorphic axioms in a limited way but I can generalize it to handle all polymorphic axioms in which all quantifiers in the negative normal formal of the axiom are universal. I don't know how to handle polymorphic type parameters in any other situation.

Finally, I made an attempt to understand polymorphic maps. I am attaching a file with an initial attempt to monomorphize a simple program manually. Since I am unsure of the semantics, what I am doing there is an educated guess which I would love for you folks to confirm or refute.

Original program:

type Ref;
var Heap: HeapType;
const null: Ref;
type Field A B;
type NormalField;
type HeapType = <A, B> [Ref, Field A B]B;
const $b: Field NormalField bool;
const $i: Field NormalField int;
const $R: Field NormalField Ref;

procedure A(h: HeapType)
returns (h': HeapType)
{
    var r: Ref;
    h' := h;
    h'[r, $R] := r;
}

procedure B(h: HeapType)
returns (h': HeapType)
{
    var r: Ref;
    var b: bool;
    h' := h;
    h'[r, $b] := b;
    call h' := A(h');
}

Monomorphized program:

type HeapType_NormalField_Ref = [Ref, Field NormalField Ref]Ref;
procedure A_mono(h_NormalField_Ref: HeapType_NormalField_Ref)
returns (h'_NormalField_Ref: HeapType_NormalField_Ref)
{
    var r: Ref;
    h'_NormalField_Ref := h_NormalField_Ref;
    h'_NormalField_Ref[r, $R] := r;
}

type HeapType_NormalField_bool = [Ref, Field NormalField bool]bool;
procedure B_mono(h_NormalField_Ref: HeapType_NormalField_Ref, h_NormalField_bool: HeapType_NormalField_bool)
returns (h'_NormalField_Ref: HeapType_NormalField_Ref, h'_NormalField_bool: HeapType_NormalField_bool)
{
    var r: Ref;
    var b: bool;
    h'_NormalField_bool := h_NormalField_bool;
    h'_NormalField_bool[r, $b] := b;
    call h'_NormalField_Ref := A_mono(h'_NormalField_Ref);
}

[gauravpartha]

The final call in the monomorphized version does not make sense to me in general. In this particular program it seems ok, because procedure A only accesses field $R$. In general, A could also access field $b$ (or there could be a function that takes HeapType as input) and then this particular monomorphization approach would be incorrect.

Since you wrote that you are unsure about the polymorphic map semantics, here is a partial view of how I understand polymorphic maps based on the Boogie polymorphism paper by Leino and Rümmer, which might be helpful or someone can correct me on my view.

Boogie essentially desugars polymorphic maps to type constructors and polymorphic functions (there may be Z3 specific things going on too). So, the original program could be rewritten to the following map-free program (where the select and store axioms have been omitted):

type Ref;
type Field _ _;
type NormalField;

type HeapType_abs;
function select_HeapType_abs<A,B>(arg0: HeapType_abs, arg1: Ref, arg2: Field A B) : B;
function store_HeapType_abs<A,B>(arg0: HeapType_abs, arg1: Ref, arg2: Field A B, arg3: B) : HeapType_abs;
/** select and store axioms omitted */

const $b: Field NormalField bool;
const $i: Field NormalField int;
const $R: Field NormalField Ref;

procedure A(h: HeapType_abs) returns (h': HeapType_abs)
{
  var r: Ref;

    h' := h;
    h' := store_HeapType_abs(h', r, $R, r);
}

procedure B(h: HeapType_abs) returns (h': HeapType_abs)
{
  var r: Ref;
  var b: bool;

    h' := h;
    h' := store_HeapType_abs(h', r, $b, b);
    call h' := A(h');
}

The transformation is not always completely trivial. In particular, if there are two "related maps" such as <A>[int]A and <A>[bool]A, then, in general, they should not be represented by two separate type constructors. The reason is that there could be a quantifier forall <T> m : <A>[T]A :: ... and one would like to capture that if T is int, then <A>[T]A is the same type as <A>[int]A.
The solution is then to instead define a type constructor with a single argument arg representing maps <A>[arg]A, which in the above instances can be instantiated with int, bool, and T, respectively (the Boogie polymorphism paper by Leino and Rümmer provides the details).
In general, one would also desugar type HeapType = <A, B> [Ref, Field A B]B to a type constructor with a single argument that would be instantiated with Ref. This "problem" persists if one keeps type quantification and removes polymorphic maps as the paper shows.

The above example does not expose the full power of Boogie's maps.

For example, assume there is an additional field

const $heap_field: Field NormalField Heap

Now a heap can store heaps (one could argue that semantically speaking such a declaration does not change the meaning of the map but that is another discussion). Someone mentioned to me at some point that Chalice used something like this in its Boogie encoding. In Viper, we use the following field type

Field SomeType (<A, B> [Ref, Field A B]bool)

That means we also store polymorphic maps in heaps, but these maps themselves only store booleans.

A more contrived example is the following program (written by @alexanderjsummers), which models the Barber paradox:

procedure BarberParadox()
{
  var m : <S>[S]bool;  
  
  assume (forall x : <T>[T]bool :: {m[x]} m[x] <==> !x[x]);
  assert m[m] ==> !m[m]; 
  assert false;
}

Here, maps are "truly impredicative": a map can take itself as input and is thus, defined in terms of itself. I do not know of a Boogie front-end that makes use of such "truly impredicative" maps.

I would be interested in investigating what maps make sense for Boogie users.

[shazqadeer]

@gauravpartha : I am interested in exploiting monomorphization inside Boogie so that tools such as Dafny, Viper, MoveProver, etc. can retain modeling producitivity without compromising prover efficiency. Polymorphic maps and type quantification are two features I have not yet addressed in my monomorphization work. If you would like to collaborate in this work, I am certainly happy to have a discussion. I can be reached at [email protected].

[shazqadeer]

The goal of monomorphic encoding was achieved without eliminating any polymorphic features. Closing this discussion.