summaryrefslogtreecommitdiff
path: root/src/value.ml
diff options
context:
space:
mode:
authorRobert Norton2019-05-30 14:45:00 +0100
committerRobert Norton2019-05-30 14:45:49 +0100
commit308207df86f824501efec740532f45e617da1a2e (patch)
tree58dbafded5abf3777aa98054a06237b02dbab6f2 /src/value.ml
parent101065d9c2c7f0d84f352019f157db9b1498a31a (diff)
Implement ones builtin in sail_lib and add to interpreter. However currently this is implemented in lib/vector_dec.sail as sail function that calls not_vec on sail_zeros.
Diffstat (limited to 'src/value.ml')
-rw-r--r--src/value.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml
index e44ebda8..c509c81f 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -433,6 +433,10 @@ let value_zeros = function
| [v] -> mk_vector (Sail_lib.zeros (coerce_int v))
| _ -> failwith "value zeros"
+let value_ones = function
+ | [v] -> mk_vector (Sail_lib.ones (coerce_int v))
+ | _ -> failwith "value ones"
+
let value_shiftl = function
| [v1; v2] -> mk_vector (Sail_lib.shiftl (coerce_bv v1, coerce_int v2))
| _ -> failwith "value shiftl"
@@ -670,6 +674,7 @@ let primops =
("zero_extend", value_zero_extend);
("sign_extend", value_sign_extend);
("zeros", value_zeros);
+ ("ones", value_ones);
("shiftr", value_shiftr);
("shiftl", value_shiftl);
("shift_bits_left", value_shift_bits_left);