Tracing instrumentation for C backend

9 files changed, 264 insertions, 15 deletions

diff --git a/lib/sail.h b/lib/sail.h
index 319db18d..a2f2f456 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -163,6 +163,11 @@ void concat_str(sail_string *stro, const sail_string str1, const sail_string str
 void undefined_string(sail_string *str, const unit u) {
 }
 
+unit print(const sail_string str) {
+  printf("%s", str);
+  return UNIT;
+}
+
 unit print_endline(const sail_string str) {
   printf("%s\n", str);
   return UNIT;
@@ -173,6 +178,11 @@ unit print_string(const sail_string str1, const sail_string str2) {
   return UNIT;
 }
 
+unit prerr(const sail_string str) {
+  fprintf(stderr, "%s", str);
+  return UNIT;
+}
+
 unit prerr_endline(const sail_string str) {
   fprintf(stderr, "%s\n", str);
   return UNIT;
@@ -185,6 +195,13 @@ unit print_int(const sail_string str, const mpz_t op) {
   return UNIT;
 }
 
+unit prerr_int(const sail_string str, const mpz_t op) {
+  fputs(str, stderr);
+  mpz_out_str(stderr, 10, op);
+  fputs("\n", stderr);
+  return UNIT;
+}
+
 unit print_int64(const sail_string str, const int64_t op) {
   printf("%s%" PRId64 "\n", str, op);
   return UNIT;
@@ -192,7 +209,8 @@ unit print_int64(const sail_string str, const int64_t op) {
 
 unit sail_putchar(const mpz_t op) {
   char c = (char) mpz_get_ui(op);
-  putchar(c);
+  printf("%c", c);
+  fflush(stdout);
   return UNIT;
 }
 
@@ -936,8 +954,6 @@ void init_real_of_sail_string(real *rop, const sail_string op) {
 
 #endif
 
-#endif
-
 /* ***** Sail memory builtins ***** */
 
 /* We organise memory available to the sail model into a linked list
@@ -954,7 +970,7 @@ struct block {
 struct block *sail_memory = NULL;
 
 /* Must be one less than a power of two. */
-uint64_t MASK = 0xFFFFul;
+uint64_t MASK = 0xFFFFFFul;
 
 // All sail vectors are at least 64-bits, but only the bottom 8 bits
 // are used in the second argument.
@@ -979,10 +995,11 @@ void write_mem(uint64_t address, uint64_t byte)
   /* If we couldn't find a block matching the mask, allocate a new
      one, write the byte, and put it at the front of the block
      list. */
+  fprintf(stderr, "[Sail] Allocating new block 0x%" PRIx64 "\n", mask);
   struct block *new_block = malloc(sizeof(struct block));
   new_block->block_id = mask;
   new_block->mem = calloc(MASK + 1, sizeof(uint8_t));
-  new_block->mem[offset] = byte;
+  new_block->mem[offset] = (uint8_t) byte;
   new_block->next = sail_memory;
   sail_memory = new_block;
 }
@@ -1002,7 +1019,7 @@ uint64_t read_mem(uint64_t address)
     }
   }
 
-  return 0;
+  return 0x58;
 }
 
 void kill_mem()
@@ -1040,7 +1057,7 @@ unit write_ram(const mpz_t addr_size,     // Either 32 or 64
     byte = mpz_get_ui(buf) & 0xFF;
     write_mem(addr + i, byte);
 
-    // Then shift buf 8 bits right, and increment addr.
+    // Then shift buf 8 bits right.
     mpz_fdiv_q_2exp(buf, buf, 8);
   }
 
@@ -1072,6 +1089,7 @@ void read_ram(bv_t *data,
 }
 
 unit load_raw(uint64_t addr, const sail_string file) {
+  fprintf(stderr, "[Sail] Loading %s from 0x%" PRIx64 " to ", file, addr);
   FILE *fp = fopen(file, "r");
 
   uint64_t byte;
@@ -1080,6 +1098,8 @@ unit load_raw(uint64_t addr, const sail_string file) {
     addr++;
   }
 
+  fprintf(stderr, "0x%" PRIx64 "\n", addr - 1);
+
   return UNIT;
 }
 
@@ -1117,16 +1137,131 @@ void load_image(char *file) {
   fclose(fp);
 }
 
-void load_instr(uint64_t addr, uint32_t instr) {
-  write_mem(addr    , instr       & 0xFF);
-  write_mem(addr + 1, instr >> 8  & 0xFF);
-  write_mem(addr + 2, instr >> 16 & 0xFF);
-  write_mem(addr + 3, instr >> 24 & 0xFF);
+// ***** Setup and cleanup functions for library code *****
+
+static int64_t g_trace_depth;
+static bool g_trace_enabled;
+
+/*
+ * Bind these functions in Sail to enable and disable tracing:
+ *
+ * val "enable_tracing" : unit -> unit
+ * val "disable_tracing" : unit -> unit
+ *
+ * Compile with sail -c -c_trace.
+ */
+unit enable_tracing(const unit u)
+{
+  g_trace_depth = 0;
+  g_trace_enabled = true;
+  return UNIT;
+}
+
+unit disable_tracing(const unit u)
+{
+  g_trace_depth = 0;
+  g_trace_enabled = false;
+  return UNIT;
+}
+
+void trace_bv_t(const bv_t op)
+{
+  if (g_trace_enabled) {
+    if (op.len % 4 == 0) {
+      fputs("0x", stderr);
+      mpz_t buf;
+      mpz_init_set(buf, *op.bits);
+
+      char *hex = malloc((op.len / 4) * sizeof(char));
+
+      for (int i = 0; i < op.len / 4; ++i) {
+	char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30);
+	hex[i] = (c < 0x3A) ? c : c + 0x7;
+	mpz_fdiv_q_2exp(buf, buf, 4);
+      }
+
+      for (int i = op.len / 4; i > 0; --i) {
+	fputc(hex[i - 1], stderr);
+      }
+
+      free(hex);
+      mpz_clear(buf);
+    } else {
+      fputs("0b", stderr);
+      for (int i = op.len; i > 0; --i) {
+	fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stderr);
+      }
+    }
+  }
+}
+
+void trace_uint64_t(const uint64_t x) {
+  if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x);
+}
+
+void trace_sail_string(const sail_string str) {
+  if (g_trace_enabled) fprintf(stderr, "\"%s\"", str);
+}
+
+void trace_unit(const unit u) {
+  if (g_trace_enabled) fputs("()", stderr);
+}
+
+void trace_mpz_t(const mpz_t op) {
+  if (g_trace_enabled) mpz_out_str(stderr, 10, op);
+}
+
+void trace_bool(const bool b) {
+  if (g_trace_enabled) {
+    if (b) {
+      fprintf(stderr, "true");
+    } else {
+      fprintf(stderr, "false");
+    }
+  }
+}
+
+void trace_unknown(void) {
+  if (g_trace_enabled) fputs("?", stderr);
+}
+
+void trace_argsep(void) {
+  if (g_trace_enabled) fputs(", ", stderr);
+}
+
+void trace_argend(void) {
+  if (g_trace_enabled) fputs(")\n", stderr);
+}
+
+void trace_retend(void) {
+  if (g_trace_enabled) fputs("\n", stderr);
+}
+
+void trace_start(char *name)
+{
+  if (g_trace_enabled) {
+    fprintf(stderr, "[TRACE] ");
+    for (int64_t i = 0; i < g_trace_depth; ++i) {
+      fprintf(stderr, "%s", "|   ");
+    }
+    fprintf(stderr, "%s(", name);
+  }
+}
+
+void trace_end(void)
+{
+  if (g_trace_enabled) {
+    fprintf(stderr, "[TRACE] ");
+    for (int64_t i = 0; i < g_trace_depth; ++i) {
+      fprintf(stderr, "%s", "|   ");
+    }
+  }
 }
 
 // ***** Setup and cleanup functions for library code *****
 
 void setup_library(void) {
+  disable_tracing(UNIT);
   mpf_set_default_prec(FLOAT_PRECISION);
   mpz_init(sail_lib_tmp1);
   mpz_init(sail_lib_tmp2);
@@ -1137,3 +1272,5 @@ void cleanup_library(void) {
   mpz_clear(sail_lib_tmp2);
   kill_mem();
 }
+
+#endif
diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml
index 9b063404..0902877a 100644
--- a/riscv/platform_impl.ml
+++ b/riscv/platform_impl.ml
@@ -152,7 +152,7 @@ let rec term_read () =
   let buf = Bytes.make 1 '\000' in
   let nbytes = Unix.read Unix.stdin buf 0 1 in
   (* todo: handle nbytes == 0 *)
-  buf.[0]
+  Bytes.get buf 0
 
 (*
 let save_string_to_file s fname =
diff --git a/src/bitfield.ml b/src/bitfield.ml
index 161908cd..afdd5baf 100644
--- a/src/bitfield.ml
+++ b/src/bitfield.ml
@@ -83,6 +83,22 @@ let rec translate_indices hi lo =
   else
     (hi / 64, hi mod 64, 0) :: translate_indices (hi - (hi mod 64 + 1)) lo
 
+let constructor name order start stop =
+  let indices = translate_indices start stop in
+  let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
+  let constructor_val = Printf.sprintf "val Mk_%s : %s -> %s" name (bitvec size order) name in
+  let body (chunk, hi, lo) =
+    Printf.sprintf "%s_chunk_%i = v[%i .. %i]"
+                   name chunk ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop)
+  in
+  let constructor_function = String.concat "\n"
+    [ Printf.sprintf "function Mk_%s v = struct {" name;
+      Printf.sprintf "  %s" (Util.string_of_list ",\n  " body indices);
+                     "}"
+    ]
+  in
+  combine [ast_of_def_string order constructor_val; ast_of_def_string order constructor_function]
+
 (* For every index range, create a getter and setter *)
 let index_range_getter name field order start stop =
   let indices = translate_indices start stop in
@@ -149,4 +165,4 @@ let field_accessor name order (id, ir) = index_range_accessor name (string_of_id
 let macro id size order ranges =
   let name = string_of_id id in
   let ranges = (mk_id "bits", BF_aux (BF_range (Big_int.of_int (size - 1), Big_int.of_int 0), Parse_ast.Unknown)) :: ranges in
-  combine ([newtype name size order] @ List.map (field_accessor name order) ranges)
+  combine ([newtype name size order; constructor name order (size - 1) 0] @ List.map (field_accessor name order) ranges)
diff --git a/src/c_backend.ml b/src/c_backend.ml
index e088b5e5..96cd9ed7 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -59,6 +59,7 @@ module Big_int = Nat_big_num
 
 let c_verbosity = ref 1
 let opt_ddump_flow_graphs = ref false
+let opt_trace = ref false
 
 (* Optimization flags *)
 let optimize_primops = ref false
@@ -990,8 +991,10 @@ let analyze_primop' ctx env l id args typ =
   | "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] ->
      AE_val (AV_C_fragment (F_op (v1, "&", v2), typ))
 
+            (*
   | "not_bits", [AV_C_fragment (v, _)] ->
      AE_val (AV_C_fragment (F_unary ("~", v), typ))
+             *)
 
   | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] ->
      let len = F_op (f, "-", F_op (t, "-", v_one)) in
@@ -3231,6 +3234,59 @@ let sgen_finish = function
      Printf.sprintf "  finish_%s();" (sgen_id id)
   | _ -> assert false
 
+let instrument_tracing ctx =
+  let module StringSet = Set.Make(String) in
+  let traceable = StringSet.of_list ["uint64_t"; "sail_string"; "bv_t"; "mpz_t"; "unit"; "bool"] in
+  let rec instrument = function
+    | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs ->
+       let trace_start =
+         iraw (Printf.sprintf "trace_start(\"%s\");" (String.escaped (string_of_id id)))
+       in
+       let trace_arg cval =
+         let ctyp_name = sgen_ctyp_name (cval_ctyp cval) in
+         if StringSet.mem ctyp_name traceable then
+           iraw (Printf.sprintf "trace_%s(%s);" ctyp_name (sgen_cval cval))
+         else
+           iraw "trace_unknown();"
+       in
+       let rec trace_args = function
+         | [] -> []
+         | [cval] -> [trace_arg cval]
+         | cval :: cvals ->
+            trace_arg cval :: iraw "trace_argsep();" :: trace_args cvals
+       in
+       let trace_end = iraw "trace_end();" in
+       let trace_ret =
+         let ctyp_name = sgen_ctyp_name ctyp in
+         if StringSet.mem ctyp_name traceable then
+           iraw (Printf.sprintf "trace_%s(%s);" (sgen_ctyp_name ctyp) (sgen_clexp_pure clexp))
+         else
+           iraw "trace_unknown();"
+       in
+       [trace_start;
+        iraw "g_trace_depth++;"]
+       @ trace_args args
+       @ [iraw "trace_argend();";
+          instr;
+          iraw "g_trace_depth--;";
+          trace_end;
+          trace_ret;
+          iraw "trace_retend();"]
+       @ instrument instrs
+
+    | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (instrument block), aux) :: instrument instrs
+    | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (instrument block), aux) :: instrument instrs
+    | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
+       I_aux (I_if (cval, instrument then_instrs, instrument else_instrs, ctyp), aux) :: instrument instrs
+
+    | instr :: instrs -> instr :: instrument instrs
+    | [] -> []
+  in
+  function
+  | CDEF_fundef (function_id, heap_return, args, body) ->
+     CDEF_fundef (function_id, heap_return, args, instrument body)
+  | cdef -> cdef
+
 let bytecode_ast ctx rewrites (Defs defs) =
   let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in
   let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in
@@ -3258,7 +3314,7 @@ let compile_ast ctx (Defs defs) =
     let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
     let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
     let cdefs = List.concat (List.rev chunks) in
-    let cdefs = optimize ctx cdefs in
+    let cdefs = List.map (instrument_tracing ctx) (optimize ctx cdefs) in
     let docs = List.map (codegen_def ctx) cdefs in
 
     let preamble = separate hardline
diff --git a/src/sail.ml b/src/sail.ml
index 36b4efd8..86c00254 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -119,6 +119,9 @@ let options = Arg.align ([
   ( "-Oconstant_fold",
     Arg.Set Constant_fold.optimize_constant_fold,
     " Apply constant folding optimizations");
+  ( "-c_trace",
+    Arg.Set C_backend.opt_trace,
+    " Instrument C ouput with tracing");
   ( "-lem_ast",
     Arg.Set opt_print_lem_ast,
     " output a Lem AST representation of the input");
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 89056347..31b975df 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -575,6 +575,10 @@ let real_of_string str =
 (* Not a very good sqrt implementation *)
 let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *)
 
+let print str = Pervasives.print_string str
+
+let prerr str = Pervasives.prerr_string str
+
 let print_int (str, x) =
   print_endline (str ^ Big_int.to_string x)
 
diff --git a/src/value.ml b/src/value.ml
index 8ee219b7..41b52720 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -491,6 +491,9 @@ let primops =
     StringMap.empty
     [ ("and_bool", and_bool);
       ("or_bool", or_bool);
+      ("print", value_print);
+      ("prerr", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
+      ("dec_str", fun _ -> V_string "X");
       ("print_endline", value_print);
       ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit));
       ("putchar", value_putchar);
diff --git a/test/c/read_write_ram.expect b/test/c/read_write_ram.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/read_write_ram.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/read_write_ram.sail b/test/c/read_write_ram.sail
new file mode 100644
index 00000000..751d15b5
--- /dev/null
+++ b/test/c/read_write_ram.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+$include <string.sail>
+$include <exception_basic.sail>
+
+val write_ram = "write_ram" : forall 'n 'm.
+  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmem}
+
+val read_ram = "read_ram" : forall 'n 'm.
+  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val main : unit -> unit effect {escape, wmem, rmem}
+
+function main() = {
+  write_ram(64, 4, 64^0x0, 64^0x8000_0000, 0x01020304);
+  let data = read_ram(64, 4, 64^0x0, 64^0x8000_0000);
+  assert(data == 0x01020304);
+  let data = read_ram(64, 3, 64^0x0, 64^0x8000_0001);
+  assert(data == 0x010203);
+  let data = read_ram(64, 3, 64^0x0, 64^0x8000_0000);
+  assert(data == 0x020304);
+  write_ram(64, 4, 64^0x0, 64^0x7fff_ffff, 0xA1B2C3D4);
+  let data = read_ram(64, 3, 64^0x0, 64^0x8000_0000);
+  assert(data == 0xA1B2C3);
+  print_endline("ok");
+}
\ No newline at end of file