Using \gtid in barrier contracts breaks down and does not verify

[sakehl]

Mostly a reminder to self to fix.

Due to the fact of how barriers are encoded, and the SimplifyNestedQuantifyRelations work

when you write for instance:

  //@ blockDim.y == 1 && blockDim.z == 1 && gridDim.y == 1 && gridDim.z == 1;
__global__ void test(){
  __shared__ int s[blockDim.x];
  int tid = blockIdx.x * blockDim.x + threadIdx.x;
  s[tid] = tid;
  /*@
  requires Perm(&s[/gtid], write);
  requires s[/gtid] == /gtid)
  ensures (\forall* int i; 0 <= i && i < blockDim.x; Perm(&s[i], write \ (blockDim.x)));
  ensures (\forall int i; 0 <= i && i < blockDim.x; s==\gtid);
  @*/
  __syncthreads();
}

breaks down, since it does not infer that blockDim.y == 1 && blockDim.z == 1 && gridDim.y == 1 && gridDim.z == 1 and thus cannot simplify to automatically quantified conditions of the barrier contract.

Additional note, using tid instead of \gtid leads to wonky results in the barrier contract. I'm unsure if it is completely correct, since tid is sort of considered a constant, whilst actually it differs in value in the barrier quantifiers. Have to think more about it.