Use sail_lib.lem values in C backend

Rather than just using strings to represent literals, now use value
types from sail_lib.lem to represent them. This allows for expressions
to be evaluated at compile time, which will be useful for future
optimisations involving constant folding and propagation, and allows
the intermediate bytecode to be interpreted using the same lem
builtins that the shallow embedding uses.

To get this to work I had to tweak the build process slightly to allow
ml files to import lem files from gen_lib/. Hopefully this doesn't
break anything!

1 files changed, 99 insertions, 0 deletions

diff --git a/src/value2.lem b/src/value2.lem
new file mode 100644
index 00000000..09d74520
--- /dev/null
+++ b/src/value2.lem
@@ -0,0 +1,99 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open import Pervasives
+open import Assert_extra
+open Map
+
+open import Sail_values
+
+type vl =
+  | V_vector of list vl
+  | V_list of list vl
+  | V_bits of list bitU
+  | V_bit of bitU
+  | V_tuple of list vl
+  | V_bool of bool
+  | V_nondet (* Special nondeterministic boolean *)
+  | V_unit
+  | V_int of integer
+  | V_string of string
+  | V_ctor of string * list vl
+  | V_ctor_kind of string
+  | V_record of list (string * vl)
+  | V_null (* Used for unitialized values and null pointers in C compilation *)
+
+let string_of_value = function
+  | V_bits bs -> show_bitlist bs ^ "ul"
+  | V_int i -> show i ^ "l"
+  | V_bool true -> "true"
+  | V_bool false -> "false"
+  | V_null -> "NULL"
+  | V_unit -> "UNIT"
+  | V_bit B0 -> "0ul"
+  | V_bit B1 -> "1ul"
+  | V_string str -> "\"" ^ str ^ "\""
+  | _ -> failwith "Cannot convert value to string"
+end
+
+let primops extern args =
+  match (extern, args) with
+  | ("and_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 && b2)
+  | ("and_bool", [V_nondet; V_bool false]) -> V_bool false
+  | ("and_bool", [V_bool false; V_nondet]) -> V_bool false
+  | ("and_bool", _) -> V_nondet
+
+  | ("or_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 || b2)
+  | ("or_bool", [V_nondet; V_bool true]) -> V_bool true
+  | ("or_bool", [V_bool true; V_nondet]) -> V_bool true
+  | ("or_bool", _) -> V_nondet
+
+  | _ -> failwith ("Unimplemented primitive operation " ^ extern)
+  end