[CN-test-gen] Crash when using accesses and --with-static-hack on a static global array

[septract]

Summary

cn test --with-static-hack crashes when applying accesses to a static global array.

Replication

Test file, accesses_test.c:

static int glob_array[32];

void foo(int i) 
/*@
accesses glob_array; 
@*/
{
  ; 
}

Resulting crash:

$ cn test --with-static-hack --output-dir=testgen accesses_test.c
cn: internal error, uncaught exception:
    Failure("map<u64, i32> @ File \"backend/cn/lib/testGeneration/genDistribute.ml\", line 74, characters 74-81")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__TestGeneration__GenDistribute.default_weights.aux in file "backend/cn/lib/testGeneration/genDistribute.ml", line 74, characters 11-83
    Called from Cn__TestGeneration__GenTerms.map_gen_pre in file "backend/cn/lib/testGeneration/genTerms.ml", line 320, characters 29-32
    Called from Cn__TestGeneration__GenTerms.map_gen_pre in file "backend/cn/lib/testGeneration/genTerms.ml", line 330, characters 51-67
    Called from Cn__TestGeneration__GenDistribute.distribute_gen in file "backend/cn/lib/testGeneration/genDistribute.ml", line 107, characters 2-64
    Called from Cn__Option.map in file "backend/cn/lib/option.ml", line 5, characters 36-41
    Called from Cn__TestGeneration__GenDistribute.distribute_gen_def in file "backend/cn/lib/testGeneration/genDistribute.ml", line 113, characters 58-88
    Called from Cn__List.map_snd.(fun) in file "backend/cn/lib/list.ml", line 59, characters 25-28
    Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
    Called from Cn__List.map_snd.(fun) in file "backend/cn/lib/list.ml", line 59, characters 25-28
    Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
    Called from Cn__TestGeneration__SpecTests.compile_generators in file "backend/cn/lib/testGeneration/specTests.ml", line 90, characters 12-43
    Called from Cn__TestGeneration.save_generators in file "backend/cn/lib/testGeneration/testGeneration.ml", line 183, characters 4-134
    Called from Cn__TestGeneration.run in file "backend/cn/lib/testGeneration/testGeneration.ml", line 379, characters 2-62
    Called from Dune__exe__Main.run_tests.(fun) in file "backend/cn/bin/main.ml", line 558, characters 13-194
    
Issues can be made at https://github.com/rems-project/cerberus/issues.
Prefix your issue with "[CN-Test-Gen]". Check that there isn't already one for this error.

For comparison, this example verifies as it should:

$ cn verify accesses_test.c
[1/1]: foo -- pass

CN version: git-3567800c4 [2025-01-14 14:26:12 +0000]

Analysis

• This example is derived from the OpenSUT MKM function policy_add() which accesses the policy_table array (see here).
• The call to cn test uses the --with-static-hack flag. This is a workaround for various issues with the C preprocessor (summarized in Preprocessor and executable specifications #823). Without --with-static-hack CN rejects the example.

cc: @ZippeyKeys12

[septract]

Another anomaly with accesses on global arrays: if we just comment out the accesses clause, cn test will run on the example. I guess what's happening is that CN is ignoring ownership information over such arrays. But then, if we try to call a function which depends on ownership information, the runtime testing will throw an error.

Eg. see the following example:

static int glob_array[32]; 

int access_elem(int* elem) 
/*@
requires 
  take Elem_in = Owned(elem); 
ensures 
  take Elem_out = Owned(elem); 
@*/
{
  int i = *elem; 
  return i; 
}

void client_local(int *my_array, int offset) 
/*@
requires 
  take Arr_in = each (u64 i; i <= 32u64) { Owned(array_shift(my_array, i)) }; 
  0i32 <= offset; offset < 32i32; 
ensures 
  take Arr_out = each (u64 i; i <= 32u64) { Owned(array_shift(my_array, i)) }; 
@*/
{ 
  /*@ extract Owned<int>, (u64) offset; @*/
  int* tmp = &my_array[offset]; 
  access_elem(tmp); 
  return; 
}

void client_glob(int offset) 
/*@
// accesses glob_array; // commented out to make the test generator run 
requires 
  0i32 <= offset; offset < 32i32; 
@*/
{ 
  /*@ extract Owned<int>, (u64) offset; @*/
  int* tmp = &glob_array[offset]; 
  access_elem(tmp); 
  return; 
}