diff options
| author | Alasdair Armstrong | 2018-03-20 17:57:20 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-03-22 18:58:59 +0000 |
| commit | e33c8546e005fba30ff882b188c86ca03d0917c8 (patch) | |
| tree | cf72fc3066962718d26a76baedd2d11a7be16946 /mips | |
| parent | 0860deb52e55b11e39e3470290e07f861f877483 (diff) | |
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.
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/main.sail | 7 | ||||
| -rw-r--r-- | mips/prelude.sail | 14 |
2 files changed, 15 insertions, 6 deletions
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]) |