Fixes to get ARM u-boot working in Sail.

Also fixes to C backend for compiling MIPS spec to C

- Fix an issue with const correctness in internal_vector_update
  functions generated by C backend

- Add builtins for MIPS to sail.h

- Fix an issue where reg_deref didn't work when called on pointers to
  large bitvectors, i.e. vectors containing references to large
  bitfields as in the MIPS TLB code

- Various bug fixes and changes for running U-boot on ARM model,
  including for interpreter and OCaml compilation.

- Fix memory leak issues and incorrect shadowing for foreach loops

- Update C header file. Fixes memory leak in memory read/write
  builtins.

- Add aux constructor to ANF representation to hold environment
  information.

- Fix undefined behavior caused by optimisation left shifting uint64_t
  vectors 64 or more times. Unfortunately there's more issues because
  the same happens for X >> 64 right shifts. It would make sense for
  this to be zero, because that would guarantee the property that ((X
  >> n) >> m) == (X >> (n + m)) but we probably need to do (X >> (n -
  1) >> 1) in the optimisation to ensure that we don't cause
  UB. Shifting by 63 and then by 1 is well-defined, but shifting by 64
  in one go isn't according to the C standard. This issue with
  right-shifts only occurs for zero-length vectors, so it's not a huge
  deal, but it's still annoying.

- Add versions of print_bits and print_int that print to
  stderr. Follows OCaml convention of print/prerr. Should make things
  more explicit. Different backends had different ideas about where
  print should output to, not every backend needs to have this
  (e.g. theorem prover backends don't need to print) but having both
  stderr and stdout seperate and clear is useful for executable models
  (UART needs to be stdout, debug messages should be stderr).

1 files changed, 3 insertions, 0 deletions

diff --git a/src/util.ml b/src/util.ml
index 471b0c4c..b54c13d4 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -442,3 +442,6 @@ let warn str =
   if !opt_warnings then
     prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str)
   else ()
+
+let log_line str line msg =
+  "\n[" ^ (str ^ ":" ^ string_of_int line |> blue |> clear) ^ "] " ^ msg