From e33c8546e005fba30ff882b188c86ca03d0917c8 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 20 Mar 2018 17:57:20 +0000
Subject: Fix C compilation for CHERI and MIPS

First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.

Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.

Finally support for vector literals that are non-bitvectors has been
added.
---
 mips/main.sail    |  7 +++++--
 mips/prelude.sail | 14 ++++++++++----
 2 files changed, 15 insertions(+), 6 deletions(-)

(limited to 'mips')

diff --git a/mips/main.sail b/mips/main.sail
index 2df5c0f8..e3ffa262 100644
--- a/mips/main.sail
+++ b/mips/main.sail
@@ -9,7 +9,7 @@ function fetch_and_execute () = {
     branchPending = 0b0;
     nextPC = if inBranchDelay then delayedPC else PC + 4;
     cp2_next_pc();
-    
+
     print_bits("PC: ", PC);
     try {
       let pc_pa = TranslatePC(PC);
@@ -36,7 +36,10 @@ function fetch_and_execute () = {
   skip_wmvt();
 }
 
-val elf_entry = "Elf_loader.elf_entry" : unit -> int
+val elf_entry = {
+  ocaml: "Elf_loader.elf_entry",
+  c: "elf_entry"
+} : unit -> int
 
 val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt}
 
diff --git a/mips/prelude.sail b/mips/prelude.sail
index 05e4cfe0..5a7f1351 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -3,6 +3,8 @@ default Order dec
 type bits ('n : Int) = vector('n, dec, bit)
 union option ('a : Type) = {None : unit, Some : 'a}
 
+val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool
+
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 
 val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool
@@ -117,8 +119,10 @@ val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) ->
 
 val cast cast_unit_vec : bit -> bits(1)
 
-function cast_unit_vec bitzero = 0b0
-and cast_unit_vec bitone = 0b1
+function cast_unit_vec b = match b {
+  bitzero => 0b0,
+  bitone => 0b1
+}
 
 val print = "prerr_endline" : string -> unit
 
@@ -345,8 +349,10 @@ val cast bool_to_bits : bool -> bits(1)
 function bool_to_bits x = if x then 0b1 else 0b0
 
 val cast bit_to_bool : bit -> bool
-function bit_to_bool bitone  = true
-and      bit_to_bool bitzero = false
+function bit_to_bool b = match b {
+  bitone => true,
+  bitzero => false
+}
 
 val cast bits_to_bool : bits(1) -> bool
 function bits_to_bool x = bit_to_bool(x[0])
-- 
cgit v1.2.3