diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 31 |
1 files changed, 27 insertions, 4 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 86f8934a..a2f1286a 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -534,11 +534,34 @@ let to_vec_dec_undef_big len = to_vec_undef_big false len let to_vec_inc_undef = to_vec_inc_undef_big let to_vec_dec_undef = to_vec_dec_undef_big -let exts_int (len, vec) = to_vec_int (get_ord vec) len (signed_int vec) -let extz_int (len, vec) = to_vec_int (get_ord vec) len (unsigned_int vec) +let exts_int (len, vec) = + let barray = get_barray(vec) in + let vlen = Array.length barray in + let arr = + if (vlen < len) then + (* copy most significant bit into new bits *) + Array.append (Array.make (len - vlen) barray.(0)) barray + else + (* truncate to least significant bits *) + Array.sub barray (vlen - len) len in + let inc = get_ord vec in + Vvector(arr, (if inc then 0 else (len - 1)), inc) + +let extz_int (len, vec) = + let barray = get_barray(vec) in + let vlen = Array.length barray in + let arr = + if (vlen < len) then + (* fill new bits with zero *) + Array.append (Array.make (len - vlen) Vzero) barray + else + (* truncate to least significant bits *) + Array.sub barray (vlen - len) len in + let inc = get_ord vec in + Vvector(arr, (if inc then 0 else (len - 1)), inc) -let exts_big (len,vec) = to_vec_big (get_ord vec) len (signed_big vec) -let extz_big (len,vec) = to_vec_big (get_ord vec) len (unsigned_big vec) +let exts_big (len,vec) = exts_int (int_of_big_int len, vec) +let extz_big (len,vec) = extz_int (int_of_big_int len, vec) let exts = exts_big let extz = extz_big |