diff options
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 43 |
1 files changed, 42 insertions, 1 deletions
diff --git a/src/value.ml b/src/value.ml index d1b945a7..279d3aba 100644 --- a/src/value.ml +++ b/src/value.ml @@ -302,6 +302,10 @@ let value_or_vec = function | [v1; v2] -> mk_vector (Sail_lib.or_vec (coerce_bv v1, coerce_bv v2)) | _ -> failwith "value not_vec" +let value_xor_vec = function + | [v1; v2] -> mk_vector (Sail_lib.xor_vec (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value xor_vec" + let value_uint = function | [v] -> V_int (Sail_lib.uint (coerce_bv v)) | _ -> failwith "value uint" @@ -341,6 +345,14 @@ let value_negate = function | [v1] -> V_int (Sail_lib.negate (coerce_int v1)) | _ -> failwith "value negate" +let value_pow2 = function + | [v1] -> V_int (Sail_lib.pow2 (coerce_int v1)) + | _ -> failwith "value pow2" + +let value_int_power = function + | [v1; v2] -> V_int (Sail_lib.int_power (coerce_int v1, coerce_int v2)) + | _ -> failwith "value int_power" + let value_mult = function | [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2)) | _ -> failwith "value mult" @@ -417,6 +429,14 @@ let value_shiftr = function | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2)) | _ -> failwith "value shiftr" +let value_shift_bits_left = function + | [v1; v2] -> mk_vector (Sail_lib.shift_bits_left (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value shift_bits_left" + +let value_shift_bits_right = function + | [v1; v2] -> mk_vector (Sail_lib.shift_bits_right (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value shift_bits_right" + let value_vector_truncate = function | [v1; v2] -> mk_vector (Sail_lib.vector_truncate (coerce_bv v1, coerce_int v2)) | _ -> failwith "value vector_truncate" @@ -520,6 +540,14 @@ let value_round_down = function | [v] -> V_int (Sail_lib.round_down (coerce_real v)) | _ -> failwith "value round_down" +let value_quot_round_zero = function + | [v1; v2] -> V_int (Sail_lib.quot_round_zero (coerce_int v1, coerce_int v2)) + | _ -> failwith "value quot_round_zero" + +let value_rem_round_zero = function + | [v1; v2] -> V_int (Sail_lib.rem_round_zero (coerce_int v1, coerce_int v2)) + | _ -> failwith "value rem_round_zero" + let value_add_real = function | [v1; v2] -> V_real (Sail_lib.add_real (coerce_real v1, coerce_real v2)) | _ -> failwith "value add_real" @@ -564,6 +592,10 @@ let value_string_append = function | [v1; v2] -> V_string (Sail_lib.string_append (coerce_string v1, coerce_string v2)) | _ -> failwith "value string_append" +let value_decimal_string_of_bits = function + | [v] -> V_string (Sail_lib.decimal_string_of_bits (coerce_bv v)) + | _ -> failwith "value decimal_string_of_bits" + let primops = List.fold_left (fun r (x, y) -> StringMap.add x y r) @@ -578,6 +610,7 @@ let primops = ("putchar", value_putchar); ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs))); ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs))); + ("decimal_string_of_bits", value_decimal_string_of_bits); ("print_bits", value_print_bits); ("print_int", value_print_int); ("print_string", value_print_string); @@ -610,6 +643,7 @@ let primops = ("not_vec", value_not_vec); ("and_vec", value_and_vec); ("or_vec", value_or_vec); + ("xor_vec", value_xor_vec); ("uint", value_uint); ("sint", value_sint); ("get_slice_int", value_get_slice_int); @@ -621,6 +655,8 @@ let primops = ("zeros", value_zeros); ("shiftr", value_shiftr); ("shiftl", value_shiftl); + ("shift_bits_left", value_shift_bits_left); + ("shift_bits_right", value_shift_bits_right); ("add_int", value_add_int); ("sub_int", value_sub_int); ("div_int", value_quotient); @@ -629,6 +665,8 @@ let primops = ("quotient", value_quotient); ("modulus", value_modulus); ("negate", value_negate); + ("pow2", value_pow2); + ("int_power", value_int_power); ("shr_int", value_shr_int); ("shl_int", value_shl_int); ("max_int", value_max_int); @@ -656,7 +694,9 @@ let primops = ("mult_real", value_mult_real); ("round_up", value_round_up); ("round_down", value_round_down); - ("quotient_real", value_div_real); + ("quot_round_zero", value_quot_round_zero); + ("rem_round_zero", value_rem_round_zero); + ("quotient_real", value_quotient_real); ("abs_real", value_abs_real); ("div_real", value_div_real); ("sqrt_real", value_sqrt_real); @@ -676,4 +716,5 @@ let primops = ("string_length", value_string_length); ("string_startswith", value_string_startswith); ("string_drop", value_string_drop); + ("skip", fun _ -> V_unit); ] |