diff options
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 15 |
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); |
