diff options
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 357 |
1 files changed, 215 insertions, 142 deletions
diff --git a/src/value.ml b/src/value.ml index 8f8e651a..69023bc3 100644 --- a/src/value.ml +++ b/src/value.ml @@ -93,6 +93,33 @@ type value = with a direct register read. *) | V_attempted_read of string +let coerce_bit = function + | V_bit b -> b + | _ -> assert false + +let is_bit = function + | V_bit _ -> true + | _ -> false + +let rec string_of_value = function + | V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs) + | V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]" + | V_bool true -> "true" + | V_bool false -> "false" + | V_bit Sail_lib.B0 -> "bitzero" + | V_bit Sail_lib.B1 -> "bitone" + | V_int n -> Big_int.to_string n + | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" + | V_list vals -> "[|" ^ Util.string_of_list ", " string_of_value vals ^ "|]" + | V_unit -> "()" + | V_string str -> "\"" ^ str ^ "\"" + | V_ref str -> "ref " ^ str + | V_real r -> Sail_lib.string_of_real r + | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" + | V_record record -> + "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}" + | V_attempted_read _ -> assert false + let rec eq_value v1 v2 = match v1, v2 with | V_vector v1s, V_vector v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s @@ -111,12 +138,7 @@ let rec eq_value v1 v2 = StringMap.equal eq_value fields1 fields2 | _, _ -> false -let coerce_bit = function - | V_bit b -> b - | _ -> assert false - let coerce_ctor = function - | V_ctor (str, [V_tuple vals]) -> (str, vals) | V_ctor (str, vals) -> (str, vals) | _ -> assert false @@ -148,6 +170,10 @@ let coerce_tuple = function | V_tuple vs -> vs | _ -> assert false +let coerce_list = function + | V_list vs -> vs + | _ -> assert false + let coerce_listlike = function | V_tuple vs -> vs | V_list vs -> vs @@ -260,6 +286,10 @@ let value_append = function | [v1; v2] -> V_vector (coerce_gv v1 @ coerce_gv v2) | _ -> failwith "value append" +let value_append_list = function + | [v1; v2] -> V_list (coerce_list v1 @ coerce_list v2) + | _ -> failwith "value_append_list" + let value_slice = function | [v1; v2; v3] -> V_vector (Sail_lib.slice (coerce_gv v1, coerce_int v2, coerce_int v3)) | _ -> failwith "value slice" @@ -280,6 +310,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" @@ -315,10 +349,22 @@ let value_sub_int = function | [v1; v2] -> V_int (Sail_lib.sub_int (coerce_int v1, coerce_int v2)) | _ -> failwith "value sub" +let value_sub_nat = function + | [v1; v2] -> V_int (Sail_lib.sub_nat (coerce_int v1, coerce_int v2)) + | _ -> failwith "value sub_nat" + 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" @@ -341,7 +387,7 @@ let value_add_vec_int = function let value_sub_vec_int = function | [v1; v2] -> mk_vector (Sail_lib.sub_vec_int (coerce_bv v1, coerce_int v2)) - | _ -> failwith "value add_vec_int" + | _ -> failwith "value sub_vec_int" let value_add_vec = function | [v1; v2] -> mk_vector (Sail_lib.add_vec (coerce_bv v1, coerce_bv v2)) @@ -371,33 +417,10 @@ let value_replicate_bits = function | [v1; v2] -> mk_vector (Sail_lib.replicate_bits (coerce_bv v1, coerce_int v2)) | _ -> failwith "value replicate_bits" -let is_bit = function - | V_bit _ -> true - | _ -> false - let is_ctor = function | V_ctor _ -> true | _ -> false -let rec string_of_value = function - | V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs) - | V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]" - | V_bool true -> "true" - | V_bool false -> "false" - | V_bit Sail_lib.B0 -> "bitzero" - | V_bit Sail_lib.B1 -> "bitone" - | V_int n -> Big_int.to_string n - | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" - | V_list vals -> "[|" ^ Util.string_of_list ", " string_of_value vals ^ "|]" - | V_unit -> "()" - | V_string str -> "\"" ^ str ^ "\"" - | V_ref str -> "ref " ^ str - | V_real r -> Sail_lib.string_of_real r - | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" - | V_record record -> - "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}" - | V_attempted_read _ -> assert false - let value_sign_extend = function | [v1; v2] -> mk_vector (Sail_lib.sign_extend (coerce_bv v1, coerce_int v2)) | _ -> failwith "value sign_extend" @@ -410,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" @@ -418,10 +445,22 @@ 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" +let value_vector_truncateLSB = function + | [v1; v2] -> mk_vector (Sail_lib.vector_truncateLSB (coerce_bv v1, coerce_int v2)) + | _ -> failwith "value vector_truncateLSB" + let value_eq_anything = function | [v1; v2] -> V_bool (eq_value v1 v2) | _ -> failwith "value eq_anything" @@ -444,6 +483,10 @@ let value_undefined_vector = function | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2)) | _ -> failwith "value undefined_vector" +let value_undefined_bitvector = function + | [v] -> V_vector (Sail_lib.undefined_vector (coerce_int v, V_bit (Sail_lib.B0))) + | _ -> failwith "value undefined_bitvector" + let value_read_ram = function | [v1; v2; v3; v4] -> mk_vector (Sail_lib.read_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4)) | _ -> failwith "value read_ram" @@ -521,6 +564,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" @@ -565,116 +616,138 @@ let value_string_append = function | [v1; v2] -> V_string (Sail_lib.string_append (coerce_string v1, coerce_string v2)) | _ -> failwith "value string_append" -let primops = - List.fold_left - (fun r (x, y) -> StringMap.add x y r) - StringMap.empty - [ ("and_bool", and_bool); - ("or_bool", or_bool); - ("print", value_print); - ("prerr", fun vs -> (prerr_string (string_of_value (List.hd vs)); V_unit)); - ("dec_str", fun _ -> V_string "X"); - ("print_endline", value_print_endline); - ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit)); - ("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))); - ("print_bits", value_print_bits); - ("print_int", value_print_int); - ("print_string", value_print_string); - ("prerr_bits", value_print_bits); - ("prerr_int", value_print_int); - ("prerr_string", value_prerr_string); - ("concat_str", value_concat_str); - ("eq_int", value_eq_int); - ("lteq", value_lteq); - ("gteq", value_gteq); - ("lt", value_lt); - ("gt", value_gt); - ("eq_list", value_eq_list); - ("eq_bool", value_eq_bool); - ("eq_string", value_eq_string); - ("string_startswith", value_string_startswith); - ("string_drop", value_string_drop); - ("string_take", value_string_take); - ("string_length", value_string_length); - ("eq_bit", value_eq_bit); - ("eq_anything", value_eq_anything); - ("length", value_length); - ("subrange", value_subrange); - ("access", value_access); - ("update", value_update); - ("update_subrange", value_update_subrange); - ("slice", value_slice); - ("append", value_append); - ("not", value_not); - ("not_vec", value_not_vec); - ("and_vec", value_and_vec); - ("or_vec", value_or_vec); - ("uint", value_uint); - ("sint", value_sint); - ("get_slice_int", value_get_slice_int); - ("set_slice_int", value_set_slice_int); - ("set_slice", value_set_slice); - ("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); - ("div_int", value_quotient); - ("mult_int", value_mult); - ("mult", value_mult); - ("quotient", value_quotient); - ("modulus", value_modulus); - ("negate", value_negate); - ("shr_int", value_shr_int); - ("shl_int", value_shl_int); - ("max_int", value_max_int); - ("min_int", value_min_int); - ("abs_int", value_abs_int); - ("add_vec_int", value_add_vec_int); - ("sub_vec_int", value_sub_vec_int); - ("add_vec", value_add_vec); - ("sub_vec", value_sub_vec); - ("vector_truncate", value_vector_truncate); - ("read_ram", value_read_ram); - ("write_ram", value_write_ram); - ("trace_memory_read", fun _ -> V_unit); - ("trace_memory_write", fun _ -> V_unit); - ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns())); - ("load_raw", value_load_raw); - ("to_real", value_to_real); - ("eq_real", value_eq_real); - ("lt_real", value_lt_real); - ("gt_real", value_gt_real); - ("lteq_real", value_lteq_real); - ("gteq_real", value_gteq_real); - ("add_real", value_add_real); - ("sub_real", value_sub_real); - ("mult_real", value_mult_real); - ("round_up", value_round_up); - ("round_down", value_round_down); - ("quotient_real", value_div_real); - ("abs_real", value_abs_real); - ("div_real", value_div_real); - ("sqrt_real", value_sqrt_real); - ("print_real", value_print_real); - ("random_real", value_random_real); - ("undefined_unit", fun _ -> V_unit); - ("undefined_bit", fun _ -> V_bit Sail_lib.B0); - ("undefined_int", fun _ -> V_int Big_int.zero); - ("undefined_bool", fun _ -> V_bool false); - ("undefined_vector", value_undefined_vector); - ("undefined_string", fun _ -> V_string ""); - ("internal_pick", value_internal_pick); - ("replicate_bits", value_replicate_bits); - ("Elf_loader.elf_entry", fun _ -> V_int (!Elf_loader.opt_elf_entry)); - ("Elf_loader.elf_tohost", fun _ -> V_int (!Elf_loader.opt_elf_tohost)); - ("string_append", value_string_append); - ("string_length", value_string_length); - ("string_startswith", value_string_startswith); - ("string_drop", value_string_drop); - ] +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 = ref + (List.fold_left + (fun r (x, y) -> StringMap.add x y r) + StringMap.empty + [ ("and_bool", and_bool); + ("or_bool", or_bool); + ("print", value_print); + ("prerr", fun vs -> (prerr_string (string_of_value (List.hd vs)); V_unit)); + ("dec_str", fun _ -> V_string "X"); + ("print_endline", value_print_endline); + ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit)); + ("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); + ("prerr_bits", value_print_bits); + ("prerr_int", value_print_int); + ("prerr_string", value_prerr_string); + ("concat_str", value_concat_str); + ("eq_int", value_eq_int); + ("lteq", value_lteq); + ("gteq", value_gteq); + ("lt", value_lt); + ("gt", value_gt); + ("eq_list", value_eq_list); + ("eq_bool", value_eq_bool); + ("eq_string", value_eq_string); + ("string_startswith", value_string_startswith); + ("string_drop", value_string_drop); + ("string_take", value_string_take); + ("string_length", value_string_length); + ("eq_bit", value_eq_bit); + ("eq_anything", value_eq_anything); + ("length", value_length); + ("subrange", value_subrange); + ("access", value_access); + ("update", value_update); + ("update_subrange", value_update_subrange); + ("slice", value_slice); + ("append", value_append); + ("append_list", value_append_list); + ("not", value_not); + ("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); + ("set_slice_int", value_set_slice_int); + ("set_slice", value_set_slice); + ("hex_slice", value_hex_slice); + ("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); + ("shift_bits_right", value_shift_bits_right); + ("add_int", value_add_int); + ("sub_int", value_sub_int); + ("sub_nat", value_sub_nat); + ("div_int", value_quotient); + ("mult_int", value_mult); + ("mult", value_mult); + ("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); + ("min_int", value_min_int); + ("abs_int", value_abs_int); + ("add_vec_int", value_add_vec_int); + ("sub_vec_int", value_sub_vec_int); + ("add_vec", value_add_vec); + ("sub_vec", value_sub_vec); + ("vector_truncate", value_vector_truncate); + ("vector_truncateLSB", value_vector_truncateLSB); + ("read_ram", value_read_ram); + ("write_ram", value_write_ram); + ("trace_memory_read", fun _ -> V_unit); + ("trace_memory_write", fun _ -> V_unit); + ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns())); + ("load_raw", value_load_raw); + ("to_real", value_to_real); + ("eq_real", value_eq_real); + ("lt_real", value_lt_real); + ("gt_real", value_gt_real); + ("lteq_real", value_lteq_real); + ("gteq_real", value_gteq_real); + ("add_real", value_add_real); + ("sub_real", value_sub_real); + ("mult_real", value_mult_real); + ("round_up", value_round_up); + ("round_down", value_round_down); + ("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); + ("print_real", value_print_real); + ("random_real", value_random_real); + ("undefined_unit", fun _ -> V_unit); + ("undefined_bit", fun _ -> V_bit Sail_lib.B0); + ("undefined_int", fun _ -> V_int Big_int.zero); + ("undefined_nat", fun _ -> V_int Big_int.zero); + ("undefined_bool", fun _ -> V_bool false); + ("undefined_bitvector", value_undefined_bitvector); + ("undefined_vector", value_undefined_vector); + ("undefined_string", fun _ -> V_string ""); + ("internal_pick", value_internal_pick); + ("replicate_bits", value_replicate_bits); + ("Elf_loader.elf_entry", fun _ -> V_int (!Elf_loader.opt_elf_entry)); + ("Elf_loader.elf_tohost", fun _ -> V_int (!Elf_loader.opt_elf_tohost)); + ("string_append", value_string_append); + ("string_length", value_string_length); + ("string_startswith", value_string_startswith); + ("string_drop", value_string_drop); + ("skip", fun _ -> V_unit); + ]) + +let add_primop name impl = + primops := StringMap.add name impl !primops |