diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/interpreter.ml | 13 | ||||
| -rw-r--r-- | src/rewrites.ml | 2 | ||||
| -rw-r--r-- | src/value.ml | 7 |
3 files changed, 18 insertions, 4 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index 599a83bf..a95ab8c3 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -338,6 +338,15 @@ let rec build_letchain id lbs (E_aux (_, annot) as exp) = build_letchain id lbs exp | _ :: lbs -> build_letchain id lbs exp +let is_interpreter_extern id env = + let open Type_check in + Env.is_extern id env "interpreter" || Env.is_extern id env "ocaml" + +let get_interpreter_extern id env = + let open Type_check in + try Env.get_extern id env "interpreter" with + | Type_error _ -> Env.get_extern id env "ocaml" + let rec step (E_aux (e_aux, annot) as orig_exp) = let wrap e_aux' = return (E_aux (e_aux', annot)) in match e_aux with @@ -419,9 +428,9 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = step exp >>= fun exp' -> wrap (E_app (id, evaluated @ exp' :: exps)) | [] when Env.is_union_constructor id (env_of_annot annot) -> return (exp_of_value (V_ctor (string_of_id id, List.map value_of_exp evaluated))) - | [] when Env.is_extern id (env_of_annot annot) "interpreter" -> + | [] when is_interpreter_extern id (env_of_annot annot) -> begin - let extern = Env.get_extern id (env_of_annot annot) "interpreter" in + let extern = get_interpreter_extern id (env_of_annot annot) in if extern = "reg_deref" then let regname = List.hd evaluated |> value_of_exp |> coerce_ref in gets >>= fun (_, gstate) -> diff --git a/src/rewrites.ml b/src/rewrites.ml index 19192bab..9a5d8410 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3000,8 +3000,10 @@ let rewrite_defs_ocaml = [ ] let rewrite_defs_interpreter = [ + ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("tuple_vector_assignments", rewrite_tuple_vector_assignments); ("tuple_assignments", rewrite_tuple_assignments); + ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("constraint", rewrite_constraint); ("trivial_sizeof", rewrite_trivial_sizeof); diff --git a/src/value.ml b/src/value.ml index 0b50ee1f..a871c1be 100644 --- a/src/value.ml +++ b/src/value.ml @@ -366,7 +366,10 @@ let value_write_ram = function | _ -> failwith "value write_ram" let value_putchar = function - | [v] -> Sail_lib.putchar (coerce_int v); V_unit + | [v] -> + output_char !print_chan (char_of_int (Big_int.to_int (coerce_int v))); + flush !print_chan; + V_unit | _ -> failwith "value putchar" let value_print_bits = function @@ -384,7 +387,7 @@ let primops = [ ("and_bool", and_bool); ("or_bool", or_bool); ("print_endline", value_print); - ("prerr_endline", value_print); + ("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))); |