summaryrefslogtreecommitdiff
path: root/src/value.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/value.ml')
-rw-r--r--src/value.ml15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml
index 2f8144b9..4b4f0865 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -340,6 +340,18 @@ let value_zero_extend = function
| [v1; v2] -> mk_vector (Sail_lib.zero_extend (coerce_bv v1, coerce_int v2))
| _ -> failwith "value zero_extend"
+let value_zeros = function
+ | [v] -> mk_vector (Sail_lib.zeros (coerce_int v))
+ | _ -> failwith "value zeros"
+
+let value_shiftl = function
+ | [v1; v2] -> mk_vector (Sail_lib.shiftl (coerce_bv v1, coerce_int v2))
+ | _ -> failwith "value shiftl"
+
+let value_shiftr = function
+ | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2))
+ | _ -> failwith "value shiftr"
+
let eq_value v1 v2 = string_of_value v1 = string_of_value v2
let value_eq_anything = function
@@ -425,6 +437,9 @@ let primops =
("hex_slice", value_hex_slice);
("zero_extend", value_zero_extend);
("sign_extend", value_sign_extend);
+ ("zeros", value_zeros);
+ ("shiftr", value_shiftr);
+ ("shiftl", value_shiftl);
("add_int", value_add_int);
("sub_int", value_sub_int);
("mult", value_mult);