diff options
| author | Alasdair Armstrong | 2018-03-19 17:39:42 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-03-19 17:39:42 +0000 |
| commit | b42d5ab44307da291aac1882f8a2bb7bcbdfa900 (patch) | |
| tree | eddf168eca14f33ddd34027b0553302612a679da /riscv | |
| parent | e3e597feb532c71e0db32eb9abbebb9f51314d6d (diff) | |
Fixes to C backend for RISCV-compilation
Can now compile RISCV. Requires some library tweaks before it'll pass any tests,
Also adds hyperlinks to wip latex output
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/main.sail | 10 | ||||
| -rw-r--r-- | riscv/prelude.sail | 2 |
2 files changed, 9 insertions, 3 deletions
diff --git a/riscv/main.sail b/riscv/main.sail index 8e0b0440..b2bda58f 100644 --- a/riscv/main.sail +++ b/riscv/main.sail @@ -1,6 +1,9 @@ val fetch_and_execute : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} -val elf_tohost = "Elf_loader.elf_tohost" : unit -> int +val elf_tohost = { + ocaml: "Elf_loader.elf_tohost", + c: "elf_tohost" +} : unit -> int function fetch_and_execute () = let tohost = __GetSlice_int(64, elf_tohost(), 0) in @@ -42,7 +45,10 @@ function fetch_and_execute () = PC = nextPC } -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, exmem, rmem, rreg, wmv, wreg} diff --git a/riscv/prelude.sail b/riscv/prelude.sail index f6532215..44791217 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -3,7 +3,7 @@ default Order dec type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None : unit, Some : 'a} -val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool |