diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sail_lib.ml | 1 | ||||
| -rw-r--r-- | src/value.ml | 5 |
2 files changed, 6 insertions, 0 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 13ed491b..21d95e64 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -728,6 +728,7 @@ let sign_extend (vec, n) = | B1 :: _ as vec -> replicate_bits ([B1], Big_int.of_int (m - List.length vec)) @ vec let zeros n = replicate_bits ([B0], n) +let ones n = replicate_bits ([B1], n) let shift_bits_right_arith (x, y) = let ybi = uint(y) in 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); |