Allow the use of pointers to things that are not a reference type

[superaxander]

Currently you can only take the address of a struct in the C and C++ frontends. By converting variables to pointers whenever you take their address you can do the same for non-reference types.

This is a draft PR because I'm still working on it. While it is currently at a state where I'm not breaking anything and simple (nonsense) examples like this verify:

struct A {
    int a;
    int b;
    int *c;
};


//@ ensures \result == 10;
int main() {
    struct A a;

    a.a = 2;

    struct A* b = &a;
    b->a = 5;
    b->b = 5;
    b->c = &a.a;
    return a.a + a.b;
}

I am unsure where the limits are here. Additionally I still need to fix the locations because you cannot write the necessary loop invariants to preserve access to your local which was transformed to a pointer.

[sakehl]

Ow interesting, I've thought a lot about this as well.

structs and fields of structs should work easily indeed, since they are translated to refs in viper already.

More interesting are cases like:

 //@ context x!= NULL && \pointer_length(x) == 1 && Perm(x, write);
 //@ ensures *x == \old(*x)+1;
void f(int* x){
  x++;
}

void main(){
  int x = 5;
  f(&x);
  //@ assert x == 6;
}

What I've been thinking is maybe adding additional annotations when declaring a var, such that we actually consider it a memory location for which we have can specify permissions, since it seems like an overhead of the encoding to encode every basic type as a memory location.

So maybe something like:

/*@ ref @*/ int x;

or something.

Probably @pieter-bos has some ideas here too.

[sakehl]

Looking at the code, you make a variable a pointer, whenever address of is used of that variable. Which is nice.

I wonder how that works with parallel blocks and for loops. Do you then need to also add for those variables permissions, that they are not NULL and have pointer_length of 1?

Anyway, nice work!

[superaxander]

Yeah so what I've done for now is simply detect which variables and fields get their address taken and "upgrade" those to pointers automatically. I'm not sure if there are cases where this could not be detected and such an annotation would be needed. I was trying some stuff out in VeriFast and it seems to take a similar approach of implicitly upgrading variables to pointers.

For example in this program you can use == to reason about the value of a in the loop invariant:

int main()
    //@ requires true;
    //@ ensures result == 10;
{
    int a = 15;    
    int x = 0;
    while (x < 1)
    	//@ invariant x >= 0 && x <= 1 &*& a == ((x == 1) ? 10 : 15);
    {
    	a = 10;
    	x += 1;
    }
    return a;
}

But if I add a line ìnt *b = &a anywhere in this function then I have to rewrite the invariant to look like this:

x >= 0 && x <= 1 &*& a |-> ((x == 1) ? 10 : 15);

And removing the int *b = &a will require you to also switch back to ==.

[superaxander]

Looking at the code, you make a variable a pointer, whenever address of is used of that variable. Which is nice.

I wonder how that works with parallel blocks and for loops. Do you then need to also add for those variables permissions, that they are not NULL and have pointer_length of 1?

Anyway, nice work!

Yes that is the reason why this a draft PR currently. Things break when you have loops and currently there is no way to write the necessary loop invariant to say that you keep access to the pointer after the loop, but that is probably just a mistake I made in the location transformation.

[superaxander]

Right now the following program can be verified:

struct A {
    int a;
    int b;
};
struct B {
    struct A a;
};
//@ ensures \result == 10;
int main() {
    struct B b;

    b.a.a = 2;

    struct A* a = &b.a;

    int *c = &a->a;
    int *d = &a->b;

    //@ loop_invariant Perm(a, write);
    //@ loop_invariant Perm(&a->a, write);
    //@ loop_invariant Perm(&a->b, write);
    //@ loop_invariant c == &a->a;
    //@ loop_invariant d == &a->b;
    //@ loop_invariant \pointer(&a->a, 1, write);
    //@ loop_invariant \pointer(&a->b, 1, write);
    //@ loop_invariant *c == 5 ==> *d == 5;
    while (*c != 5) {
        *c = 5;
        *d = 5;
    }

    return a->a + a->b;
}

To get this to work I had initialise the inner struct whenever the outer struct is initialised since otherwise you don't have permission to access the inner struct. (I guess that was just an open issue with structs currently?)

I also added a bit of a hack

vercors/src/rewrite/vct/rewrite/VariableToPointer.scala

Lines 110 to 112 in 5386e50

	case PointerLocation(AddrOf(Deref(obj, Ref(f)))) /* if addressedSet.contains(f) always true */ => FieldLocation[Post](dispatch(obj), fieldMap.ref(f))
	case PointerLocation(AddrOf(DerefHeapVariable(Ref(v)))) /* if addressedSet.contains(v) always true */ => HeapVariableLocation[Post](heapVariableMap.ref(v))
	case PointerLocation(AddrOf(local@Local(_))) => throw UnsupportedAddrOf(local)

Which gets rid of an initial AddrOf in a PointerLocation so that you can actually refer to the implicit pointer and say something about its permissions.

[superaxander]

An additional note about this:

To get this to work I had initialise the inner struct whenever the outer struct is initialised since otherwise you don't have permission to access the inner struct. (I guess that was just an open issue with structs currently?)

I currently implemented this by simply initialising any classes contained in the class when we encounter a NewObject/Instantiate statement/expression. That would be a problem if it happened to Java classes since they should of course have null fields by default. However, the new expressions in Java and PVL are translated to ConstructorInvocations so we do not have this problem. But maybe to avoid confusion this default initialising behaviour should be implemented in LangCToCol and LangCPPToCol instead.

[sakehl]

An additional note about this:

To get this to work I had initialise the inner struct whenever the outer struct is initialised since otherwise you don't have permission to access the inner struct. (I guess that was just an open issue with structs currently?)

I currently implemented this by simply initialising any classes contained in the class when we encounter a NewObject/Instantiate statement/expression. That would be a problem if it happened to Java classes since they should of course have null fields by default. However, the new expressions in Java and PVL are translated to ConstructorInvocations so we do not have this problem. But maybe to avoid confusion this default initialising behaviour should be implemented in LangCToCol and LangCPPToCol instead.

Tbh: what should really happen is that we give Struct it's own internal type and declerations.

I hacked in struct to be similar to a class, just to get something working. But really they are different beast, where structs are really 'values' and classes are references.

So we should have a TStruct as Type, and Struct[G] as decleration together with StructDeclaration etc in Node.scala

[superaxander]

Superseded by #1159