[CN] Mismatched CN syntax when reasoning about ptr vs. array fields

[septract]

CN requires two different conventions when referring to struct fields, depending on whether the field was declared as a pointer or an array. From a C language perspective, these situations are semantically extremely similar and use the same syntax, so it's v confusing that CN distinguishes them. Ideally CN should allow the same specification form in both cases.

Replication

The following (working) example illustrates the problem:

struct foo {
  int arr[2]; 
  int *ptr; 
}; 

int *access(struct foo *f, int i) 
/*@
requires take F_in = Owned(f); 
ensures 
  take F_out = Owned(f); 
  if (i == 0i32) {
    ptr_eq( return, member_shift(f, arr) ) // <-- Case 1: member_shift()
  } else {
    ptr_eq( return, F_in.ptr ) // <-- Case 2: no member_shift() 
  }; 
@*/
{ 
  if (i == 0) { 
    return f->arr; 
  } else { 
    return f->ptr; 
  }
}

This example is derived from the client_write_buffer function in the OpenSUT MKM code, here.

CN version: git-6d4b48623 [2025-01-02 16:35:14 -0500]

Alternatives that don't work

The version of the specification with member_shift() in both cases doesn't work:

/*@
// Doesn't work: 
requires take F_in = Owned(f); 
ensures 
  take F_out = Owned(f); 
  if (i == 0i32) {
    ptr_eq( return, member_shift(f, arr) ) 
  } else {
    ptr_eq( return, member_shift(f, ptr) ) // <-- use member_shift() in Case 2 instead
  }; 
@*/

CN rejects the proof with the following error:

field_access_bug_2.c:40:5: error: Unprovable constraint
    return f->ptr; 
    ^~~~~~~~~~~~~~ 
Constraint from field_access_bug_2.c:30:3:
  if (i == 0i32) {
  ^~~~~~~~~~~~~~~~ 

The version of the specification with dot-notation in both cases also doesn't work. In fact it crashes CN - see #809.

// Crashes CN:
/*@
requires take F_in = Owned(f); 
ensures 
  take F_out = Owned(f); 
  if (i == 0i32) {
    ptr_eq( return, F_in.arr ) // <-- use dot-notation in Case 1 instead
  } else {
    ptr_eq( return, F_in.ptr )
  }; 
@*/

Analysis

• Ideally, we should be able to write this example using the same syntactic form in both cases. If not, we should at least help the user get this right with a useful error message.
• I guess what is happening is that the abstract value F_in extracted by Owned refers to the pointer in the case of a field declared as a pointer, and to the contents of the array when declared as an array. We want both of these things in different situations for both pointers and arrays, but the current state seems quite confusing.
• Note I filed the crash mentioned above as ticket [CN] Crash when applying ptr_eq to struct array field #809.