[CN] Crash when applying ptr_eq to struct array field

[septract]

Applying ptr_eq to a struct array field makes CN crash. This example is derived from the OpenSUT MKM target code (see here).

Replication

Crashing code, field_access_bug_1.c:

struct foo {
  int arr[1]; 
}; 

int *access_crash(struct foo *f) 
/*@
requires take F_in = Owned(f); 
ensures 
  ptr_eq( return, F_in.arr ); 
@*/
{ 
  return f->arr; 
}

Crash trace:

$ cn verify field_access_bug_1.c
cn: internal error, uncaught exception:
    Failure("eq_: type mismatch: return : pointer, F_in.arr : map<u64, i32>")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__IndexTerms.eq_ in file "backend/cn/lib/indexTerms.ml", line 555, characters 4-82
    Called from Cn__Builtins.ptr_eq_def.(fun) in file "backend/cn/lib/builtins.ml", line 153, characters 21-63
    Called from Cn__Builtins.mk_arg2.(fun) in file "backend/cn/lib/builtins.ml", line 28, characters 52-64
    Called from Cn__Builtins.apply_builtin_funs in file "backend/cn/lib/builtins.ml", line 219, characters 13-24
    Called from Cn__Compile.EffectfulTranslation.translate_cn_expr.trans in file "backend/cn/lib/compile.ml", line 860, characters 28-71
    Called from Cn__Compile.EffectfulTranslation.translate_cn_expr in file "backend/cn/lib/compile.ml" (inlined), line 1036, characters 4-14
    Called from Cn__Compile.EffectfulTranslation.translate_cn_assrt in file "backend/cn/lib/compile.ml", line 1190, characters 15-53
    Called from Cn__Compile.make_lrt_generic.(fun) in file "backend/cn/lib/compile.ml", line 1479, characters 24-65
    Called from Cn__Compile.make_lrt in file "backend/cn/lib/compile.ml", line 1486, characters 24-53
    Called from Cn__Compile.make_rt in file "backend/cn/lib/compile.ml", line 1516, characters 4-79
    Called from Cn__Core_to_mucore.normalise_fun_map_decl.(fun) in file "backend/cn/lib/core_to_mucore.ml", line 1319, characters 15-204
    Called from Cn__Core_to_mucore.make_largs.aux in file "backend/cn/lib/core_to_mucore.ml", line 906, characters 15-25
    Called from Cn__Core_to_mucore.make_largs.aux in file "backend/cn/lib/core_to_mucore.ml", line 890, characters 17-38
    Called from Cn__Core_to_mucore.make_function_args.aux in file "backend/cn/lib/core_to_mucore.ml", line 992, characters 17-86
    Called from Cn__Core_to_mucore.make_function_args.aux in file "backend/cn/lib/core_to_mucore.ml", line 988, characters 8-89
    Called from Cn__Core_to_mucore.normalise_fun_map_decl in file "backend/cn/lib/core_to_mucore.ml", line 1307, characters 9-1023
    Called from Cn__Core_to_mucore.normalise_fun_map.(fun) in file "backend/cn/lib/core_to_mucore.ml", line 1398, characters 12-282
    Called from Pmap.fold in file "pmap.ml", line 156, characters 15-38
    Called from Cn__Core_to_mucore.normalise_fun_map in file "backend/cn/lib/core_to_mucore.ml", line 1394, characters 4-925
    Called from Cn__Core_to_mucore.normalise_file in file "backend/cn/lib/core_to_mucore.ml", line 1561, characters 4-221
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 164, characters 8-134
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 182, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

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

Analysis

• I don't think use of ptr_eq is type-correct, but it's an obvious thing for the user to write and it shouldn't crash CN as a whole.
• Broader question: what's the correct way to write this kind of pointer access property? Right now, we have to use member_shift specifically for this case, which is hard to intuit.