From edc2be164fcf53c333796e55b93f94bf6c9ed152 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 22 Jun 2018 19:03:02 +0100
Subject: Simplify treating of undefined_bool in Lem library

Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state.  The previous behaviour can be
implemented as Sail code, if desired.

Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
---
 mips/mips_extras.lem | 1 -
 1 file changed, 1 deletion(-)

(limited to 'mips/mips_extras.lem')

diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 2e07586c..86e78586 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -90,7 +90,6 @@ let shift_bits_right_arith v n =
   maybe_fail "shift_bits_right_arith" r
 
 (* Use constants for undefined values for now *)
-let internal_pick vs = return (head vs)
 let undefined_string () = return ""
 let undefined_unit () = return ()
 let undefined_int () = return (0:ii)
-- 
cgit v1.2.3


From 63fccf3902edbeb7816e6c419b0cbdcfea423cb9 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 10 Jul 2018 22:39:23 +0100
Subject: Update CHERI code extraction from Isabelle

Also use zero-initialised memory.  Apparently some tests access unitialised
memory, and the default behaviour of the Lem shallow embedding is to fail in
this case.
---
 mips/mips_extras.lem | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'mips/mips_extras.lem')

diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 86e78586..4edb0066 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -111,7 +111,12 @@ val elf_entry : unit -> integer
 let elf_entry () = 0
 declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`
 
-let print_bits msg bs = prerr_endline (msg ^ (string_of_bv bs))
+let print_bits msg bs = print_endline (msg ^ (string_of_bv bs))
+let prerr_bits msg bs = prerr_endline (msg ^ (string_of_bv bs))
+
+val prerr_string : string -> unit
+let prerr_string _ = ()
+declare ocaml target_rep function prerr_string = `Pervasives.prerr_string`
 
 val get_time_ns : unit -> integer
 let get_time_ns () = 0
-- 
cgit v1.2.3