[CN-exec] Missing instrumentation for ghost arguments at call sites when goto/tag is used

[moratorium08]

If you instrument the following program with Fulminate, and run it,

void f() /*@ requires cn_ghost u64 size; true; @*/ {}

int main() {
    goto t;
t:
    f(/*@ 1u64 @*/);
    return 0;
}

you will get like this:

> cn instrument poc.c --run
poc.c:1:23: warning: experimental keyword 'cn_ghost' (use of experimental features is discouraged)
void f() /*@ requires cn_ghost u64 size; true; @*/ {}
                      ^~~~~~~~
Runtime typechecking of ghost arguments failed
************************************************************
Internal error: no error_msg_info available.

This is because the function call f() is not correctly instrumented; the instrumented main function (poc.exec.c) is going to be like this:

int main() {
  /* EXECUTABLE CN PRECONDITION */
  signed int __cn_ret = 0;
  initialise_ownership_ghost_state();
  initialise_ghost_stack_depth();
  alloc_ghost_array(1);
  initialise_exec_c_locs_mode(0);
  initialise_ownership_stack_mode(0);

    goto t;
t:
    f(/*@ 1u64 @*/);      // <--- this is not instrumented!!
    { __cn_ret = 0; goto __cn_epilogue; }

/* EXECUTABLE CN POSTCONDITION */
__cn_epilogue:

  free_ghost_array();

return __cn_ret;

}

misc

• CN version: 384f4f3

[rbanerjee20]

@dc-mak as we discussed today with @dimecon , this issue exists for all Mucore labels (except loops), not just C labels.

We probably want to collect and pipe through the Mucore expression (as done for LALoops here) for the remaining label cases as follows:

| LAloop_continue _
| LAloop_break _ -> failwith "TODO: similar to existing handling - return Mu.Non_inlined" 
| LAreturn
| LAswitch
| LAcase
| LAdefault
| LAactual_label ->
   failwith "TODO: handle label and collect Mucore expression, as is collected for LALoop"