RTS: Add --verbosity flag to C model

This is interpreted as a set of bits that control various bits of output.
Bit 0 is print the PC on every cycle.
(It would probably be useful to standardise a few of these flags across
 all models.  Other candidates are accesses to physical memory, throwing
 SAIL exceptions, current privilege level, ...)

4 files changed, 32 insertions, 3 deletions

diff --git a/aarch64/elfmain.sail b/aarch64/elfmain.sail
index 152f4ed8..a231cf64 100644
--- a/aarch64/elfmain.sail
+++ b/aarch64/elfmain.sail
@@ -198,9 +198,13 @@ val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 val check_cycle_count = { c: "cycle_count" } : unit -> unit
 
 function main() = {
+  let verbosity = __GetVerbosity();
   init();
   while true do {
     fetch_and_execute();
     check_cycle_count();
+    if verbosity[0] == bitone then {
+        print(concat_str("[SAIL] PC=", concat_str(HexStr(UInt(aget_PC())), "\n")));
+    }
   }
 }
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 553fc091..74298e00 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -356,3 +356,5 @@ val __WakeupRequest = {ocaml: "wakeup_request", lem: "wakeup_request", smt: "wak
 
 val __Sleeping = {ocaml: "sleeping", lem: "sleeping", smt: "sleeping", interpreter: "sleeping", c: "sleeping"}: unit -> bool effect {escape, rreg, undef}
 
+val __GetVerbosity = {c: "sail_get_verbosity"}: unit -> bits(64) effect {escape, rreg, undef}
+
diff --git a/lib/rts.c b/lib/rts.c
index 022fb7e3..dd251eea 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -30,6 +30,13 @@ unit sail_exit(unit u)
   return UNIT;
 }
 
+static uint64_t g_verbosity = 0;
+
+mach_bits sail_get_verbosity(const unit u)
+{
+  return g_verbosity;
+}
+
 bool g_sleeping = false;
 
 unit sleep_request(const unit u)
@@ -434,12 +441,13 @@ void get_cycle_count(sail_int *rop, const unit u)
 /* ***** Argument Parsing ***** */
 
 static struct option options[] = {
-  {"elf",        required_argument, 0, 'e'},
-  {"entry",      required_argument, 0, 'n'},
-  {"image",      required_argument, 0, 'i'},
   {"binary",     required_argument, 0, 'b'},
   {"cyclelimit", required_argument, 0, 'l'},
   {"config",     required_argument, 0, 'C'},
+  {"elf",        required_argument, 0, 'e'},
+  {"entry",      required_argument, 0, 'n'},
+  {"image",      required_argument, 0, 'i'},
+  {"verbosity",  required_argument, 0, 'v'},
   {0, 0, 0, 0}
 };
 
@@ -517,6 +525,13 @@ int process_arguments(int argc, char *argv[])
       }
       break;
 
+    case 'v':
+      if (!sscanf(optarg, "0x%" PRIx64, &g_verbosity)) {
+       fprintf(stderr, "Could not parse verbosity flags %s\n", optarg);
+       return -1;
+      }
+      break;
+
     default:
       fprintf(stderr, "Unrecognized option %s\n", optarg);
       return -1;
diff --git a/lib/rts.h b/lib/rts.h
index 95ff72c4..cedb555e 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -21,6 +21,14 @@ unit sail_assert(bool b, sail_string msg);
 unit sail_exit(unit);
 
 /*
+ * sail_get_verbosity reads a 64-bit value that the C runtime allows you to set
+ * on the command line.
+ * The intention is that you can use individual bits to turn on/off different
+ * pieces of debugging output.
+ */
+mach_bits sail_get_verbosity(const unit u);
+
+/*
  * Put processor to sleep until an external device calls wakeup_request().
  */
 unit sleep_request(const unit u);