Immut instead of const

[sakehl]

• The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc.

PR description

I think I made a mistake when introducing a sequence encoding for const pointers. Const pointers are references to which you cannot write towards that reference. However other parts of the program might have a reference towards that pointer, to which it eventually can write again. This is not possible with the current encoding to sequences, since once it is turned to a sequence, it cannot be turned back.

For example

int f(const int * xs) {
  .... // Code which passes xs as a reference to another thread which is started, but is not guaranteed to terminate before 
     // this function terminates 
  return xs[0];
}

main(){
  int* xs = malloc(sizeof(int)*1);
  xs[0] = 1;
  int x = f(xs); // Coerce xs to const pointer and back
  xs[0] = x*x; // But this is wrong, since we also passed xs as a reference to some thread somewhere.
}

Would never be possible with the current encoding. And is I think some use case we want to support.

So I think the better name is an immutable pointer. I.e. a pointer, after which its contents are initialized, are guaranteed to never change again.

So for this we introduce an extra annotation named immutable which captures this. This really is to old encoding for const pointers, so mostly this PR is renaming everything.

To get the old behaviour for const pointers write this now instead: const /*@immutable*/ int* xs`.

Note: I think it is possible to have a better encoding for const pointers: you still make the underlying pointer block a sequence, but this sequence is saved in a field in Viper, so you need permission for this complete sequence. This means you do permission bookkeeping for the complete pointer block, which is still cheaper since its not a permission qualifier.
This fixes the given example above, since if we give the permission of const int* xs to some other thread that does not finish, we do not allow the const pointer to be coerced back to a normal pointer when calling f in main. We can only safely coerce back, if we have the permission.

[superaxander]

Oh btw Edoardo and I are working on proving that all the VerCors ADTs are consistent and we found that the const_pointer one isn't. I.e. writing p = const_pointer_of([1,2,3],4) would lead to inconsistencies since by the first axiom you have that const_pointer_offset(p) < 3 and by the second axiom you have that const_pointer_offset(p) = 4. Now you wouldn't be able to write it as a user, so it'd probably be fine, but it'd be better if there was an implication in the second axiom which requires the offset to be in range. (This is also something that needs to be fixed for the block ADT)