diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sail_lib.ml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 3cd8e18c..f0ea7fb4 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -506,8 +506,18 @@ let sign_extend (vec, n) = | [] -> replicate_bits ([B0], Big_int.of_int (m - List.length vec)) @ vec | B1 :: _ as vec -> replicate_bits ([B1], Big_int.of_int (m - List.length vec)) @ vec -(* FIXME *) -let shift_bits_right (x, y) = x -let shift_bits_left (x, y) = x +let shift_bits_right (x, y) = + let ybi = uint(y) in + let yi = Big_int.to_int ybi in + let zeros = replicate_bits ([B0], ybi) in + let rbits = zeros @ x in + take (List.length x) rbits + +let shift_bits_left (x, y) = + let ybi = uint(y) in + let yi = Big_int.to_int ybi in + let zeros = replicate_bits ([B0], ybi) in + let rbits = x @ zeros in + drop yi rbits let speculate_conditional_success () = true |