summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlasdair Armstrong2020-02-06 17:20:39 +0000
committerAlasdair Armstrong2020-02-06 17:21:20 +0000
commit4a72cb8084237161d0bccc66f27d5fb6d24315e0 (patch)
tree04b824a9190795185a24c7c2679c60dd03592d43
parentda1309632d35c910a6d3ae14ad2f5af037fce89e (diff)
Make sure tdiv_int and tmod_int are recognised by sail -i
-rw-r--r--doc/riscv.tex2
-rw-r--r--src/value.ml10
2 files changed, 11 insertions, 1 deletions
diff --git a/doc/riscv.tex b/doc/riscv.tex
index 48008c64..ca2b9dfe 100644
--- a/doc/riscv.tex
+++ b/doc/riscv.tex
@@ -56,7 +56,7 @@ register Xs : vector(32, dec, xlenbits)
\sailval{wX}
\sailfn{wX}
-\sailoverloadVVX
+\sailoverloadUUX
We also give a function \ll{MEMr} for reading memory, this function
just points at a builtin we have defined elsewhere. Note that
diff --git a/src/value.ml b/src/value.ml
index 69023bc3..3a9a071f 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -369,6 +369,14 @@ let value_mult = function
| [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2))
| _ -> failwith "value mult"
+let value_tdiv_int = function
+ | [v1; v2] -> V_int (Sail_lib.tdiv_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value tdiv_int"
+
+let value_tmod_int = function
+ | [v1; v2] -> V_int (Sail_lib.tmod_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value tmod_int"
+
let value_quotient = function
| [v1; v2] -> V_int (Sail_lib.quotient (coerce_int v1, coerce_int v2))
| _ -> failwith "value quotient"
@@ -687,6 +695,8 @@ let primops = ref
("sub_int", value_sub_int);
("sub_nat", value_sub_nat);
("div_int", value_quotient);
+ ("tdiv_int", value_tdiv_int);
+ ("tmod_int", value_tmod_int);
("mult_int", value_mult);
("mult", value_mult);
("quotient", value_quotient);