Interpreter: don't silently use OCaml externs, only interpreter externs

(Adds 'interpreter' externs as appropriate.)

6 files changed, 69 insertions, 15 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index 61a1ff76..3a1b0927 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -5,19 +5,19 @@ $include <flow.sail>
 
 // ***** Addition *****
 
-val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
+val add_atom = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
   (int('n), int('m)) -> int('n + 'm)
 
-val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int
+val add_int = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int
 
 overload operator + = {add_atom, add_int}
 
 // ***** Subtraction *****
 
-val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
+val sub_atom = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
   (int('n), int('m)) -> int('n - 'm)
 
-val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int
+val sub_int = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int
 
 overload operator - = {sub_atom, sub_int}
 
@@ -29,18 +29,18 @@ val sub_nat = {
 
 // ***** Negation *****
 
-val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n)
+val negate_atom = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n)
 
-val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int
+val negate_int = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int
 
 overload negate = {negate_atom, negate_int}
 
 // ***** Multiplication *****
 
-val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
+val mult_atom = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
   (int('n), int('m)) -> int('n * 'm)
 
-val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int
+val mult_int = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int
 
 overload operator * = {mult_atom, mult_int}
 
@@ -59,6 +59,7 @@ val shr_int = "shr_int" : (int, int) -> int
 val div_int = {
   smt: "div",
   ocaml: "quotient",
+  interpreter: "quotient",
   lem: "integerDiv",
   c: "tdiv_int",
   coq: "Z.quot"
@@ -69,6 +70,7 @@ overload operator / = {div_int}
 val mod_int = {
   smt: "mod",
   ocaml: "modulus",
+  interpreter: "modulus",
   lem: "integerMod",
   c: "tmod_int",
   coq: "Z.rem"
@@ -79,6 +81,7 @@ overload operator % = {mod_int}
 val abs_int = {
   smt : "abs",
   ocaml: "abs_int",
+  interpreter: "abs_int",
   lem: "abs_int",
   coq: "Z.abs"
 } : (int, int) -> int
diff --git a/lib/elf.sail b/lib/elf.sail
index 2d799d4d..6ea5de19 100644
--- a/lib/elf.sail
+++ b/lib/elf.sail
@@ -3,12 +3,14 @@ $define _ELF
 
 val elf_entry = {
   ocaml: "Elf_loader.elf_entry",
+  interpreter: "Elf_loader.elf_entry",
   lem: "elf_entry",
   c: "elf_entry"
 } : unit -> int
 
 val elf_tohost = {
   ocaml: "Elf_loader.elf_tohost",
+  interpreter: "Elf_loader.elf_tohost",
   lem: "elf_tohost",
   c: "elf_tohost"
 } : unit -> int
diff --git a/lib/flow.sail b/lib/flow.sail
index 5ee9a74a..7c6f1ebb 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -21,7 +21,7 @@ val not_bool = {coq: "negb", _: "not"} : bool -> bool
 val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool
 
-val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val eq_atom = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
 val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
@@ -41,9 +41,9 @@ val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom('
 val gt_atom_range = {coq: "gtb_range_r", _: "gt"}     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
 val gteq_atom_range = {coq: "geb_range_r", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
 
-val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
-val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool
-val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool
+val eq_range = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
+val eq_int = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool
+val eq_bool = {ocaml: "eq_bool", interpreter: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool
 
 val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
 function neq_range (x, y) = not_bool(eq_range(x, y))
diff --git a/lib/instr_kinds.sail b/lib/instr_kinds.sail
new file mode 100644
index 00000000..66ef90c6
--- /dev/null
+++ b/lib/instr_kinds.sail
@@ -0,0 +1,28 @@
+union read_kind = {
+  Read_plain : unit,
+  Read_reserve : unit,
+  Read_acquire : unit,
+  Read_exclusive : unit,
+  Read_exclusive_acquire : unit,
+  Read_stream : unit,
+  Read_RISCV_acquire : unit,
+  Read_RISCV_strong_acquire : unit,
+  Read_RISCV_reserved : unit,
+  Read_RISCV_reserved_acquire : unit,
+  Read_RISCV_reserved_strong_acquire : unit,
+  Read_X86_locked : unit
+}
+
+union write_kind = {
+  Write_plain  : unit
+  Write_conditional : unit
+  Write_release : unit
+  Write_exclusive : unit
+  Write_exclusive_release : unit
+  Write_RISCV_release : unit
+  Write_RISCV_strong_release : unit
+  Write_RISCV_conditional : unit
+  Write_RISCV_conditional_release : unit
+  Write_RISCV_conditional_strong_release : unit
+  Write_X86_locked : unit
+}
\ No newline at end of file
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 8abcd218..9ac4d1a5 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -9,6 +9,7 @@ val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool
 
 val eq_bits = {
   ocaml: "eq_list",
+  interpreter: "eq_list",
   lem: "eq_vec",
   c: "eq_bits",
   coq: "eq_vec"
@@ -20,6 +21,7 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -
 
 val vector_length = {
   ocaml: "length",
+  interpreter: "length",
   lem: "length_list",
   c: "length",
   coq: "vec_length"
@@ -39,6 +41,7 @@ val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('
 
 val truncate = {
   ocaml: "vector_truncate",
+  interpreter: "vector_truncate",
   lem: "vector_truncate",
   coq: "vector_truncate",
   c: "sail_truncate"
@@ -50,7 +53,7 @@ function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail
 
 overload operator ^ = {sail_mask}
 
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = {ocaml: "append", interpreter: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 
 overload append = {bitvector_concat}
@@ -60,6 +63,7 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
 
 val bitvector_access = {
   ocaml: "access",
+  interpreter: "access",
   lem: "access_vec_dec",
   coq: "access_vec_dec",
   c: "vector_access"
@@ -67,6 +71,7 @@ val bitvector_access = {
 
 val plain_vector_access = {
   ocaml: "access",
+  interpreter: "access",
   lem: "access_list_dec",
   coq: "vec_access_dec",
   c: "vector_access"
@@ -76,6 +81,7 @@ overload vector_access = {bitvector_access, plain_vector_access}
 
 val bitvector_update = {
   ocaml: "update",
+  interpreter: "update",
   lem: "update_vec_dec",
   coq: "update_vec_dec",
   c: "vector_update"
@@ -83,6 +89,7 @@ val bitvector_update = {
 
 val plain_vector_update = {
   ocaml: "update",
+  interpreter: "update",
   lem: "update_list_dec",
   coq: "vec_update_dec",
   c: "vector_update"
@@ -92,6 +99,7 @@ overload vector_update = {bitvector_update, plain_vector_update}
 
 val add_bits = {
   ocaml: "add_vec",
+  interpreter: "add_vec",
   lem: "add_vec",
   c: "add_bits",
   coq: "add_vec"
@@ -99,6 +107,7 @@ val add_bits = {
 
 val add_bits_int = {
   ocaml: "add_vec_int",
+  interpreter: "add_vec_int",
   lem: "add_vec_int",
   c: "add_bits_int",
   coq: "add_vec_int"
@@ -108,6 +117,7 @@ overload operator + = {add_bits, add_bits_int}
 
 val vector_subrange = {
   ocaml: "subrange",
+  interpreter: "subrange",
   lem: "subrange_vec_dec",
   c: "vector_subrange",
   coq: "subrange_vec_dec"
@@ -116,6 +126,7 @@ val vector_subrange = {
 
 val vector_update_subrange = {
   ocaml: "update_subrange",
+  interpreter: "update_subrange",
   lem: "update_subrange_vec_dec",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_dec"
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index b295c92c..b8e1b91f 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -9,6 +9,7 @@ val "eq_bit" : (bit, bit) -> bool
 
 val eq_bits = {
   ocaml: "eq_list",
+  interpreter: "eq_list",
   lem: "eq_vec",
   c: "eq_bits",
   coq: "eq_vec"
@@ -20,6 +21,7 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -
 
 val vector_length = {
   ocaml: "length",
+  interpreter: "length",
   lem: "length_list",
   c: "length",
   coq: "length_list"
@@ -37,6 +39,7 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
 val truncate = {
   ocaml: "vector_truncate",
+  interpreter: "vector_truncate",
   lem: "vector_truncate",
   coq: "vector_truncate",
   c: "truncate"
@@ -48,7 +51,7 @@ function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_exte
 
 overload operator ^ = {mask}
 
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = {ocaml: "append", interpreter: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 
 overload append = {bitvector_concat}
@@ -58,6 +61,7 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
 
 val bitvector_access = {
   ocaml: "access",
+  interpreter: "access",
   lem: "access_vec_inc",
   coq: "access_vec_inc",
   c: "vector_access"
@@ -65,6 +69,7 @@ val bitvector_access = {
 
 val plain_vector_access = {
   ocaml: "access",
+  interpreter: "access",
   lem: "access_list_inc",
   coq: "access_list_inc",
   c: "vector_access"
@@ -74,6 +79,7 @@ overload vector_access = {bitvector_access, plain_vector_access}
 
 val bitvector_update = {
   ocaml: "update",
+  interpreter: "update",
   lem: "update_vec_inc",
   coq: "update_vec_inc",
   c: "vector_update"
@@ -81,6 +87,7 @@ val bitvector_update = {
 
 val plain_vector_update = {
   ocaml: "update",
+  interpreter: "update",
   lem: "update_list_inc",
   coq: "update_list_inc",
   c: "vector_update"
@@ -90,11 +97,12 @@ overload vector_update = {bitvector_update, plain_vector_update}
 
 val add_bits = {
   ocaml: "add_vec",
+  interpreter: "add_vec",
   c: "add_bits"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_bits_int = {
-  ocaml: "add_vec_int",
+  ocaml: "add_vec_int", interpreter: "add_vec_int",
   c: "add_bits_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
@@ -102,6 +110,7 @@ overload operator + = {add_bits, add_bits_int}
 
 val vector_subrange = {
   ocaml: "subrange",
+  interpreter: "subrange",
   lem: "subrange_vec_inc",
   c: "vector_subrange",
   coq: "subrange_vec_inc"
@@ -110,6 +119,7 @@ val vector_subrange = {
 
 val vector_update_subrange = {
   ocaml: "update_subrange",
+  interpreter: "update_subrange",
   lem: "update_subrange_vec_inc",
   c: "vector_update_subrange",
   coq: "update_subrange_vec_inc"