Unique specifier for types leading to using different fields in the backend #1219
Conversation
|
Nice! You should know that @superaxander (and sometimes me) are working on some proposed silicon changes that address similar concerns, although we've focused on singleton heap chunks (i.e. plain permission without quantification), but I don't see a strong reason why e.g. the proposed chunk ordering heuristics would not improve things. Maybe we should have a look at some slow array examples again with our recently gained knowledge. |
|
Yes this would be quite useful. Ideally there'd be a way we could give Viper a better view of which fields may alias and which may not instead of simply relying on the name of the field. For example I want to be able to say the field int_1 and int_2 never alias but both of them may alias with int_3 which would drastically reduce the amount of heap chunks viper has to consider when dealing with a pointer to a field int_1 or int_2. (additionally during state consolidation Viper will take every combination of two heap chunks with the same field name to attempt to prove that they do or don't alias, this generates an exponential amount of proof goals) Your example of wanting to specify that the two fields are unique is basically the exact thing I've been working on for the past two weeks with my by-value classes. Because I'm encoding structs as ADTs with pointers inside of them we have for a struct: struct A {
int a;
int b;
}That we know that As for specifying a ghost type of e.g. void pointers I have also been thinking about that since this kind of pattern occurs everywhere in LLVM. (all pointers are untyped in LLVM) My idea so far was to extend the notion of permission to being "permission to access as if it were a certain type". For example: //@ requires Perm(a, write, int)
void foo(void *a) {
int b = *((int *) a)
}You could then call this function with many different kinds of values which can all be treated as int pointers: struct A a;
a.a = 5;
// A pointer to a value "struct A" can be treated as an int pointer
foo(&a);
// This is already an int pointer
foo(&a.b); |
|
So this is almost ready to merge. Adding /@ unique_field @/ should be relatively straightforward, but since I'm on a bit of deadline towards the end of my PhD I don't want to add it in at the moment. Three question, specifically for @superaxander
|
|
Note: I had to run the build action again on GiHub, since the first time it said "Out of heap memory" or something similar. The same I indicated on the VerCors chat a few days ago.
Maybe we need to increase the value of "-Xmx2G" to "-Xmx4G"? in ".mill-jvm-opts" |
True
You can now take a pointer to anything you can take a pointer to in C, so heap variables, locals, and struct fields. For locals we turn their type into a pointer type whenever you tried to take their address, for fields they are always pointers, and for heap variables I currently do the same things as for locals but I'm looking at changing that in #1317. (I want to make everything a pointer unless we can determine we can lower it to a normal value because no one takes the address. This is actually how locals that store a struct value already work) The final way you can get a pointer is by casting an integer to a pointer, but I think casting in general, other than the identity, should probably just be disallowed for unique pointers. |
|
Ok I think I got everything covered now. Everything we discussed above I've fixed now, and there are test present for those things. I've updated the original PR description to reflect precisely what is changed. The test seem to be passing. So if something wants to review this we can merge this? If there is anything I can help with, I'm happy to, since 3000 LoC is quite big. @superaxander or @bobismijnnaam how should we proceed? |
|
No I meant #1232 notice the small but important difference between these two: public class MyClass {
//@ decreases;
private int f() {
//@ decreases;
while (true) {}
return 5;
}
}public class MyClass {
//@ decreases;
private int f()
while (true) {}
return 5;
}
}The first one is harder to fix, since we get a single "decrease" clause from Viper as what was the reason. And I did not know how to redirect blame towards it (the current code). In other words this code: https://github.com/utwente-fmt/vercors/blob/1e37de3ebfa7b5f4a85c1c26b025b1b634529385/src/viper/viper/api/backend/SilverBackend.scala#L303C1-L306C68 does not work, since |
|
#1133 was just a very different kind of beast. You have to check that the post-condition of a call only has a self reference towards the call, if the call also has an decrease clause. Thus a program analyses that checks this should be added. |
Right for this one it's simply that invariant is not set for the decreases nodes. It's just a matter of changing these lines: vercors/src/viper/viper/api/transform/ColToSilver.scala Lines 297 to 311 in 1e37de3 To set the info to |
Apply comment alexander
|
Thanks works now! |
PR Description
Having many arrays in scope at the same time leads to poor performance in Silicon, to the point where it is not possible to verify files with many arrays present. A workaround is to use different fields for different arrays if you are sure the arrays will never overlap.
With this pull request, I add the ability to do this, by marking the type of an array as unique, indicating that it does not overlap with other arrays. In the backend, this will generate different types of fields for each array.
If you indicate that a type is unique with respect to another type, it is like a 'promise' that the function/program you are written uses the type like they are separate memory entries. Types with different uniqueness can never be assigned to each other, never be compared, etc. I.e. there is no coercion between them. Although, we make an exception with function calls, see below for an explanation.
Important: unique<1> is not fundamentally different from unique<2>. It is just the easiest way to indicate that two types are not of the same uniqueness. The actual numbers do not really matter. The same with the difference between
int *andunique<1> int*.In the frontend it looks like this
In the generated viper file we would like to have the following fields and permissions:
The above works as intended.
Pointer structs fields
Since many of my examples I wanted to verify, contained structs with pointer fields, I wanted to make this work as well.
Here I indicated that field
xsofstruct vechas an unique type. Thus, it is stored in fieldint2in Viper.Function coercions
There are probably a lot of (library) functions, which do not contain unique types. To rewrite them all such that they work for a specific uniqueness type is unfeasible. Especially since there is not fundamental difference between the types
unique<1> int*,unique<2> int*orint *, only that these types should not interact in the program.Therefor, we make sure that the following programs works:
Internally, there are created two abstract copies of
h. We have the originalh(int* x)which function body is checked w.r.t. its contract.Then we make the copies
h(unique<1> int* x)andh(unique<2> int* x). Both are created without body, since its body is already checked in the original.When is a function coercion correct.
What we want to prevent is that we can switch between pointer types (memory types) of different uniqueness after a function call. So for instance:
should never be allowed.
So I have the following rule for when I do allow function coercion's:
hhas typeunique<A> x*somewhere in its function. And a copy of this function would requireunique<B> x*. Then any other instance ofunique<A> x*which is in the function should also be coerced towardsunique<B> b*.NB: Instead of
unique<A> x*orunique<B> x*,x*is also valid (no unique modifier).This does mean that we can end up with the following which we allow:
The copies of function h have type signature
int h(/*@ unique<1> @*/ int* x, /*@ unique<1> @*/ int* y)andint h(/*@ unique<2> @*/ int* x, /*@ unique<2> @*/ int* y). This is fine. Since different uniqueness types only set restrictions on how the function can use those pointers. So we already checked that h treats these pointers as being stored in different memory. That they are actually stored in the same memory, just loosens the restriction, but does not matter.To check if all pointer types are correctly coerced, we do a scan of the following of a type signature:
Additionally, any type can contain pointers. E.g.
union<int *, void *> orseq<int *>or more importantly:struct v {int *x}andstruct w {struct v s}`. So we traverse each type to check what pointers it contains.Const type qualifier
The unique type is a type qualifier, it was easy to add the
consttype qualifier as well. I also had some ideas to add const pointers, pointer which elements cannot be changed. Since these kind of pointers could be modeled using sequence.Thus the following example verifies:
And internally uses sequences for x0 and x1.
Any coercion from regular pointer towards constant pointer I disallow at the moment. Mostly since I think you need to take an arbitrary read permission to cast from
int *towardsconst int*, and I'm not sure how to model that. Also, if this coercion/cast happens likeconst int* const_xs = (int * xs) xsyou want to return the taken read permission wheneverconst_xsis no longer in scope. (or when you call a function which hasconst int*as parameter, you want to return the taken read permission after the function call).Also things like
const int x = 0is now possible, which will error when you try to dox =1later on, because ofconst-ness.Possible extensions