C: Tweaks to RISC-V to get compiling to C

Revert a change to string_of_bits because it broke all the RISC-V
tests in OCaml. string_of_int (int_of_string x) is not valid because x may not
fit within an integer.

6 files changed, 57 insertions, 57 deletions

diff --git a/Makefile b/Makefile
index b5f518d..80b3ebf 100644
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,8 @@ SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail ris
 PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
-C_WARNINGS ?= -Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
+C_WARNINGS ?=
+#-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
 C_SRCS = riscv_prelude.c riscv_platform.c
 
 export SAIL_DIR
diff --git a/prelude.sail b/prelude.sail
index 6b2e13f..5d418aa 100644
--- a/prelude.sail
+++ b/prelude.sail
@@ -1,5 +1,7 @@
 default Order dec
 
+$include <flow.sail>
+
 type bits ('n : Int) = vector('n, dec, bit)
 union option ('a : Type) = {None : unit, Some : 'a}
 
@@ -144,8 +146,17 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything}
 
+val vector_subrange = {
+  ocaml: "subrange",
+  lem: "subrange_vec_dec",
+  c: "vector_subrange",
+  coq: "subrange_vec_dec"
+} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1)
+/*
 val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
   (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+*/
 
 val bitvector_access = {c: "bitvector_access", ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
   (bits('n), atom('m)) -> bit
@@ -183,14 +194,6 @@ val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n)
 
 overload ~ = {not_bool, not_vec}
 
-val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-function neq_atom (x, y) = not_bool(eq_atom(x, y))
-
-val neq_int = {lem: "neq"} : (int, int) -> bool
-
-function neq_int (x, y) = not_bool(eq_int(x, y))
-
 val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_vec (x, y) = not_bool(eq_vec(x, y))
@@ -199,27 +202,15 @@ val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, '
 
 function neq_anything (x, y) = not_bool(x == y)
 
-overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
-
-val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
-
-val builtin_and_vec = {c: "and_bits", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val and_vec = {lem: "and_vec", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-function and_vec (xs, ys) = builtin_and_vec(xs, ys)
-
-overload operator & = {and_bool, and_vec}
-
-val or_bool = {coq: "orb", _:"or_bool"} : (bool, bool) -> bool
+overload operator != = {neq_vec, neq_anything}
 
-val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val or_vec = {lem: "or_vec", coq: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+overload operator & = {and_vec}
 
-function or_vec (xs, ys) = builtin_or_vec(xs, ys)
+val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-overload operator | = {or_bool, or_vec}
+overload operator | = {or_vec}
 
 val unsigned = {ocaml: "uint", lem: "uint", coq: "uint", c: "sail_unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
@@ -276,16 +267,16 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
 
 val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val int_power = {ocaml: "int_power", lem: "pow", coq: "pow"} : (int, int) -> int
+val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
 
 val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real
 
 overload operator ^ = {xor_vec, int_power, real_power, concat_str}
 
-val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p.
+val add_range = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
-val add_int = {ocaml: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
+val add_int = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
 
 val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -295,12 +286,12 @@ val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real
 
 overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
 
-val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
+val sub_range = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
-val sub_int = {ocaml: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
+val sub_int = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
 val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
-               lem: "integerMinus", coq: "sub_nat"}
+	       lem: "integerMinus", coq: "sub_nat", c: "sub_nat"}
             : (nat, nat) -> nat
 
 val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -372,10 +363,10 @@ val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
 
 overload operator / = {quotient_nat, quotient, quotient_real}
 
-val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int
-val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int
+val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
 
-val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int
+val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int
 
 overload operator % = {modulus}
 
@@ -385,13 +376,13 @@ val shl_int = "shl_int" : (int, int) -> int
 
 val shr_int = "shr_int" : (int, int) -> int
 
-val min_nat = {ocaml: "min_int", lem: "min"} : (nat, nat) -> nat
+val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
 
-val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min"} : (int, int) -> int
+val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int
 
-val max_nat = {ocaml: "max_int", lem: "max"} : (nat, nat) -> nat
+val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
 
-val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max"} : (int, int) -> int
+val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int
 
 overload min = {min_nat, min_int}
 
@@ -522,7 +513,7 @@ function vector64 n = __raw_GetSlice_int(64, n, 0)
 val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
 function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
 
-val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.
diff --git a/riscv_mem.sail b/riscv_mem.sail
index 7268e9c..6c34134 100644
--- a/riscv_mem.sail
+++ b/riscv_mem.sail
@@ -58,17 +58,17 @@ function mem_read (addr, width, aq, rl, res) = {
   }
 }
 
-val MEMea = {ocaml: "memea", lem: "MEMea"} : forall 'n.
+val MEMea = {lem: "MEMea", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_release = {ocaml: "memea", lem: "MEMea_release"} : forall 'n.
+val MEMea_release = {lem: "MEMea_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_strong_release = {ocaml: "memea", lem: "MEMea_strong_release"} : forall 'n.
+val MEMea_strong_release = {lem: "MEMea_strong_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional = {ocaml: "memea", lem: "MEMea_conditional"} : forall 'n.
+val MEMea_conditional = {lem: "MEMea_conditional", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release"} : forall 'n.
+val MEMea_conditional_release = {lem: "MEMea_conditional_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n.
+val MEMea_conditional_strong_release = {lem: "MEMea_conditional_strong_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
 
 val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
@@ -136,13 +136,13 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
   }
 }
 
-val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr}
-val MEM_fence_r_rw  = {ocaml: "skip", lem: "MEM_fence_r_rw"}  : unit -> unit effect {barr}
-val MEM_fence_r_r   = {ocaml: "skip", lem: "MEM_fence_r_r"}   : unit -> unit effect {barr}
-val MEM_fence_rw_w  = {ocaml: "skip", lem: "MEM_fence_rw_w"}  : unit -> unit effect {barr}
-val MEM_fence_w_w   = {ocaml: "skip", lem: "MEM_fence_w_w"}   : unit -> unit effect {barr}
-val MEM_fence_w_rw  = {ocaml: "skip", lem: "MEM_fence_w_rw"}  : unit -> unit effect {barr}
-val MEM_fence_rw_r  = {ocaml: "skip", lem: "MEM_fence_rw_r"}  : unit -> unit effect {barr}
-val MEM_fence_r_w   = {ocaml: "skip", lem: "MEM_fence_r_w"}   : unit -> unit effect {barr}
-val MEM_fence_w_r   = {ocaml: "skip", lem: "MEM_fence_w_r"}   : unit -> unit effect {barr}
-val MEM_fence_i     = {ocaml: "skip", lem: "MEM_fence_i"}     : unit -> unit effect {barr}
+val MEM_fence_rw_rw = {lem: "MEM_fence_rw_rw", _: "skip"} : unit -> unit effect {barr}
+val MEM_fence_r_rw  = {lem: "MEM_fence_r_rw", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_r_r   = {lem: "MEM_fence_r_r", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_rw_w  = {lem: "MEM_fence_rw_w", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_w_w   = {lem: "MEM_fence_w_w", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_w_rw  = {lem: "MEM_fence_w_rw", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_rw_r  = {lem: "MEM_fence_rw_r", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_r_w   = {lem: "MEM_fence_r_w", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_w_r   = {lem: "MEM_fence_w_r", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_i     = {lem: "MEM_fence_i", _: "skip"}     : unit -> unit effect {barr}
diff --git a/riscv_platform.c b/riscv_platform.c
index 2ad3d3c..d21824a 100644
--- a/riscv_platform.c
+++ b/riscv_platform.c
@@ -46,3 +46,8 @@ void plat_insns_per_tick(sail_int *rop, unit u)
 
 mach_bits plat_htif_tohost(unit u)
 { return 0; }
+
+unit memea(mach_bits len, sail_int n)
+{
+  return UNIT;
+}
diff --git a/riscv_platform.h b/riscv_platform.h
index 2d63dca..4401ad4 100644
--- a/riscv_platform.h
+++ b/riscv_platform.h
@@ -22,3 +22,6 @@ void plat_insns_per_tick(sail_int *rop, unit);
 
 unit plat_term_write(mach_bits);
 mach_bits plat_htif_tohost(unit);
+
+unit memea(mach_bits, sail_int);
+
diff --git a/riscv_sys.sail b/riscv_sys.sail
index 94643ec..59bff60 100644
--- a/riscv_sys.sail
+++ b/riscv_sys.sail
@@ -765,7 +765,7 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
 
 val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
 
-val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success"} : xlenbits -> bool effect {exmem}
+val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success", c: "match_reservation"} : xlenbits -> bool effect {exmem}
 
 val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit