Function main in main.sail Not Reflected in C_emulator

[KotorinMinami]

In main.sail, the main function contains annotations for the PC (Program Counter) and uses a try...catch module for the correct operation of the simulator.

function main() : unit -> unit = {
  // initialize extensions
  ext_init();

  PC = get_entry_point();
  print_bits("PC = ", PC);

  try {
    init_model();
    sail_end_cycle();
    loop()
  } catch {
    Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
    Error_internal_error() => print("Error: internal error")
  }
}

However, in the riscv_sim.c , we can see that these functionalities implemented in the main function are not correspondingly reflected.

...
step_exception:
  fprintf(stderr, "Sail exception!");
  goto dump_state;
}

Does this lead to redundancy in the code within the main function? Or can we separate these functionalities and reflect them in riscv_sim.c?

[Timmmm]

Yeah I'm not sure anything really uses that main(). Make make interpret, which runs the Sail interpreter? I'm not sure.

The simulator can't use Sail's main() function because it needs to do stuff after each step. I guess you could technically change it so that Sail's main() called a C callback function after every step, but I think inverting the control like that gets pretty awkward.

[Alasdair]

https://github.com/rems-project/isla requires a main function to be written in Sail when executing litmus tests. The sail_end_cycle function is essentially doing what you suggest where it executes a callback that modifies the symbolic execution state as needed after each instruction.

[KotorinMinami]

My idea is : currently, the exception handling in riscv_sim.c is still marked as TODO. However, the implementation in main.sail, based on my understanding (or perhaps I misunderstood?), has fairly decent implementation of some exception handling as defined in our sail specifications within the generated C code.

if (!(have_exception)) goto post_exception_handlers_11095;
  have_exception = false;
  {
    if ((*current_exception).kind != Kind_zError_not_implemented) goto try_11096;
    sail_string zs;
    CREATE(sail_string)(&zs);
    COPY(sail_string)(&zs, (*current_exception).zError_not_implemented);
    zgsz312274 = print_string("Error: Not implemented: ", zs);
    KILL(sail_string)(&zs);
    goto post_exception_handlers_11095;
  }
try_11096: ;
  {
    if ((*current_exception).kind != Kind_zError_internal_error) goto try_11097;
    zgsz312274 = print_endline("Error: internal error");
    goto post_exception_handlers_11095;
  }
try_11097: ;
  have_exception = true;

Perhaps we can take this as the first step towards implementation? Also, it may be awkward to split the step of handling exceptions in the try...catch block