From 6a360137340c86006b4f3a7c6564717299cb1761 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 9 May 2018 20:08:54 +0100
Subject: 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).
---
 src/gen_lib/sail_values.lem | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index a709a8c1..0f384cab 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -45,12 +45,19 @@ let negate_real r = realNegate r
 let abs_real r = realAbs r
 let power_real b e = realPowInteger b e*)
 
+val print_endline : string -> unit
+let print_endline _ = ()
+declare ocaml target_rep function print_endline = `print_endline`
+
 val prerr_endline : string -> unit
 let prerr_endline _ = ()
 declare ocaml target_rep function prerr_endline = `prerr_endline`
 
 val print_int : string -> integer -> unit
-let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+let print_int msg i = print_endline (msg ^ (stringFromInteger i))
+
+val prerr_int : string -> integer -> unit
+let prerr_int msg i = prerr_endline (msg ^ (stringFromInteger i))
 
 val putchar : integer -> unit
 let putchar _ = ()
-- 
cgit v1.2.3