Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

1 files changed, 142 insertions, 129 deletions

diff --git a/src/value.ml b/src/value.ml
index 71d9ffe6..3a9a071f 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -369,6 +369,14 @@ let value_mult = function
   | [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2))
   | _ -> failwith "value mult"
 
+let value_tdiv_int = function
+  | [v1; v2] -> V_int (Sail_lib.tdiv_int (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value tdiv_int"
+
+let value_tmod_int = function
+  | [v1; v2] -> V_int (Sail_lib.tmod_int (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value tmod_int"
+
 let value_quotient = function
   | [v1; v2] -> V_int (Sail_lib.quotient (coerce_int v1, coerce_int v2))
   | _ -> failwith "value quotient"
@@ -486,7 +494,7 @@ let value_undefined_vector = function
 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"
@@ -620,131 +628,136 @@ 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)
-    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 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);
+       ("tdiv_int", value_tdiv_int);
+       ("tmod_int", value_tmod_int);
+       ("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