diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/c_backend.ml | 515 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 9 | ||||
| -rw-r--r-- | src/interpreter.ml | 39 | ||||
| -rw-r--r-- | src/isail.ml | 7 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 4 | ||||
| -rw-r--r-- | src/sail_lib.ml | 42 | ||||
| -rw-r--r-- | src/specialize.ml | 15 | ||||
| -rw-r--r-- | src/type_check.ml | 2 | ||||
| -rw-r--r-- | src/util.ml | 3 | ||||
| -rw-r--r-- | src/util.mli | 2 | ||||
| -rw-r--r-- | src/value.ml | 95 |
11 files changed, 519 insertions, 214 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index 23a8c92e..1371ad7d 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -67,7 +67,7 @@ let optimize_struct_updates = ref false let optimize_enum_undefined = ref false let c_debug str = - if !c_verbosity > 0 then prerr_endline str else () + if !c_verbosity > 0 then prerr_endline (Lazy.force str) else () let c_error ?loc:(l=Parse_ast.Unknown) message = raise (Reporting_basic.err_general l ("\nC backend: " ^ message)) @@ -111,6 +111,7 @@ let rec string_of_fragment ?zencode:(zencode=true) = function op ^ string_of_fragment' ~zencode:zencode f | F_have_exception -> "have_exception" | F_current_exception -> "(*current_exception)" + | F_raw raw -> raw and string_of_fragment' ?zencode:(zencode=true) f = match f with | F_op _ | F_unary _ -> "(" ^ string_of_fragment ~zencode:zencode f ^ ")" @@ -132,21 +133,22 @@ and string_of_fragment' ?zencode:(zencode=true) f = while/until loops). The aexp datatype represents these expressions, while aval represents the trivial values. - The X_aux construct in ast.ml isn't used here, but the typing - information is collapsed into the aexp and aval types. The - convention is that the type of an aexp is given by last argument to - a constructor. It is omitted where it is obvious - for example all - for loops have unit as their type. If some constituent part of the - aexp has an annotation, the it refers to the previous argument, so - in + The convention is that the type of an aexp is given by last + argument to a constructor. It is omitted where it is obvious - for + example all for loops have unit as their type. If some constituent + part of the aexp has an annotation, the it refers to the previous + argument, so in AE_let (id, typ1, _, body, typ2) typ1 is the type of the bound identifer, whereas typ2 is the type of the whole let expression (and therefore also the body). - See Flanagan et al's 'The Essence of Compiling with Continuations' *) -type aexp = + See Flanagan et al's 'The Essence of Compiling with Continuations' + *) +type aexp = AE_aux of aexp_aux * Env.t * l + +and aexp_aux = | AE_val of aval | AE_app of id * aval list * typ | AE_cast of aexp * typ @@ -191,7 +193,7 @@ let rec frag_rename from_id to_id = function | F_id id when Id.compare id from_id = 0 -> F_id to_id | F_id id -> F_id id | F_ref id when Id.compare id from_id = 0 -> F_ref to_id - | F_ref id -> F_id id + | F_ref id -> F_ref id | F_lit v -> F_lit v | F_have_exception -> F_have_exception | F_current_exception -> F_current_exception @@ -199,6 +201,7 @@ let rec frag_rename from_id to_id = function | F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2) | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f) | F_field (f, field) -> F_field (frag_rename from_id to_id f, field) + | F_raw raw -> F_raw raw let rec apat_bindings = function | AP_tup apats -> List.fold_left IdSet.union IdSet.empty (List.map apat_bindings apats) @@ -231,28 +234,30 @@ let rec aval_rename from_id to_id = function | AV_record (avals, typ) -> AV_record (Bindings.map (aval_rename from_id to_id) avals, typ) | AV_C_fragment (fragment, typ) -> AV_C_fragment (frag_rename from_id to_id fragment, typ) -let rec aexp_rename from_id to_id aexp = +let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = let recur = aexp_rename from_id to_id in - match aexp with - | AE_val aval -> AE_val (aval_rename from_id to_id aval) - | AE_app (id, avals, typ) -> AE_app (id, List.map (aval_rename from_id to_id) avals, typ) - | AE_cast (aexp, typ) -> AE_cast (recur aexp, typ) - | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (id, typ1, aexp1, aexp2, typ2) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, recur aexp1, recur aexp2, typ2) - | AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ) - | AE_return (aval, typ) -> AE_return (aval_rename from_id to_id aval, typ) - | AE_throw (aval, typ) -> AE_throw (aval_rename from_id to_id aval, typ) - | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval_rename from_id to_id aval, recur then_aexp, recur else_aexp, typ) - | AE_field (aval, id, typ) -> AE_field (aval_rename from_id to_id aval, id, typ) - | AE_case (aval, apexps, typ) -> AE_case (aval_rename from_id to_id aval, List.map (apexp_rename from_id to_id) apexps, typ) - | AE_try (aexp, apexps, typ) -> AE_try (aexp_rename from_id to_id aexp, List.map (apexp_rename from_id to_id) apexps, typ) - | AE_record_update (aval, avals, typ) -> AE_record_update (aval_rename from_id to_id aval, Bindings.map (aval_rename from_id to_id) avals, typ) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when Id.compare from_id to_id = 0 -> AE_for (id, aexp1, aexp2, aexp3, order, aexp4) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> AE_for (id, recur aexp1, recur aexp2, recur aexp3, order, recur aexp4) - | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, recur aexp1, recur aexp2) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval_rename from_id to_id aval, recur aexp) + let aexp = match aexp with + | AE_val aval -> AE_val (aval_rename from_id to_id aval) + | AE_app (id, avals, typ) -> AE_app (id, List.map (aval_rename from_id to_id) avals, typ) + | AE_cast (aexp, typ) -> AE_cast (recur aexp, typ) + | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp) + | AE_let (id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (id, typ1, aexp1, aexp2, typ2) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, recur aexp1, recur aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ) + | AE_return (aval, typ) -> AE_return (aval_rename from_id to_id aval, typ) + | AE_throw (aval, typ) -> AE_throw (aval_rename from_id to_id aval, typ) + | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval_rename from_id to_id aval, recur then_aexp, recur else_aexp, typ) + | AE_field (aval, id, typ) -> AE_field (aval_rename from_id to_id aval, id, typ) + | AE_case (aval, apexps, typ) -> AE_case (aval_rename from_id to_id aval, List.map (apexp_rename from_id to_id) apexps, typ) + | AE_try (aexp, apexps, typ) -> AE_try (aexp_rename from_id to_id aexp, List.map (apexp_rename from_id to_id) apexps, typ) + | AE_record_update (aval, avals, typ) -> AE_record_update (aval_rename from_id to_id aval, Bindings.map (aval_rename from_id to_id) avals, typ) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when Id.compare from_id to_id = 0 -> AE_for (id, aexp1, aexp2, aexp3, order, aexp4) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> AE_for (id, recur aexp1, recur aexp2, recur aexp3, order, recur aexp4) + | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, recur aexp1, recur aexp2) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval_rename from_id to_id aval, recur aexp) + in + AE_aux (aexp, env, l) and apexp_rename from_id to_id (apat, aexp1, aexp2) = if IdSet.mem from_id (apat_bindings apat) then @@ -267,32 +272,41 @@ let new_shadow id = incr shadow_counter; shadow_id -let rec no_shadow ids aexp = - match aexp with - | AE_val aval -> AE_val aval - | AE_app (id, avals, typ) -> AE_app (id, avals, typ) - | AE_cast (aexp, typ) -> AE_cast (no_shadow ids aexp, typ) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, no_shadow ids aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) when IdSet.mem id ids -> - let shadow_id = new_shadow id in - let aexp1 = no_shadow ids aexp1 in - let ids = IdSet.add shadow_id ids in - AE_let (shadow_id, typ1, aexp1, no_shadow ids (aexp_rename id shadow_id aexp2), typ2) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> - AE_let (id, typ1, no_shadow ids aexp1, no_shadow (IdSet.add id ids) aexp2, typ2) - | AE_block (aexps, aexp, typ) -> AE_block (List.map (no_shadow ids) aexps, no_shadow ids aexp, typ) - | AE_return (aval, typ) -> AE_return (aval, typ) - | AE_throw (aval, typ) -> AE_throw (aval, typ) - | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval, no_shadow ids then_aexp, no_shadow ids else_aexp, typ) - | AE_field (aval, id, typ) -> AE_field (aval, id, typ) - | AE_case (aval, apexps, typ) -> AE_case (aval, List.map (no_shadow_apexp ids) apexps, typ) - | AE_try (aexp, apexps, typ) -> AE_try (no_shadow ids aexp, List.map (no_shadow_apexp ids) apexps, typ) - | AE_record_update (aval, avals, typ) -> AE_record_update (aval, avals, typ) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> - let ids = IdSet.add id ids in - AE_for (id, no_shadow ids aexp1, no_shadow ids aexp2, no_shadow ids aexp3, order, no_shadow ids aexp4) - | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, no_shadow ids aexp1, no_shadow ids aexp2) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, no_shadow ids aexp) +let rec no_shadow ids (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_val aval -> AE_val aval + | AE_app (id, avals, typ) -> AE_app (id, avals, typ) + | AE_cast (aexp, typ) -> AE_cast (no_shadow ids aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, no_shadow ids aexp) + | AE_let (id, typ1, aexp1, aexp2, typ2) when IdSet.mem id ids -> + let shadow_id = new_shadow id in + let aexp1 = no_shadow ids aexp1 in + let ids = IdSet.add shadow_id ids in + AE_let (shadow_id, typ1, aexp1, no_shadow ids (aexp_rename id shadow_id aexp2), typ2) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> + AE_let (id, typ1, no_shadow ids aexp1, no_shadow (IdSet.add id ids) aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (no_shadow ids) aexps, no_shadow ids aexp, typ) + | AE_return (aval, typ) -> AE_return (aval, typ) + | AE_throw (aval, typ) -> AE_throw (aval, typ) + | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval, no_shadow ids then_aexp, no_shadow ids else_aexp, typ) + | AE_field (aval, id, typ) -> AE_field (aval, id, typ) + | AE_case (aval, apexps, typ) -> AE_case (aval, List.map (no_shadow_apexp ids) apexps, typ) + | AE_try (aexp, apexps, typ) -> AE_try (no_shadow ids aexp, List.map (no_shadow_apexp ids) apexps, typ) + | AE_record_update (aval, avals, typ) -> AE_record_update (aval, avals, typ) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when IdSet.mem id ids -> + let shadow_id = new_shadow id in + let aexp1 = no_shadow ids aexp1 in + let aexp2 = no_shadow ids aexp2 in + let aexp3 = no_shadow ids aexp3 in + let ids = IdSet.add shadow_id ids in + AE_for (shadow_id, aexp1, aexp2, aexp3, order, no_shadow ids (aexp_rename id shadow_id aexp4)) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + let ids = IdSet.add id ids in + AE_for (id, no_shadow ids aexp1, no_shadow ids aexp2, no_shadow ids aexp3, order, no_shadow ids aexp4) + | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, no_shadow ids aexp1, no_shadow ids aexp2) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, no_shadow ids aexp) + in + AE_aux (aexp, env, l) and no_shadow_apexp ids (apat, aexp1, aexp2) = let shadows = IdSet.inter (apat_bindings apat) ids in @@ -303,49 +317,55 @@ and no_shadow_apexp ids (apat, aexp1, aexp2) = (rename_apat apat, no_shadow ids (rename aexp1), no_shadow ids (rename aexp2)) (* Map over all the avals in an aexp. *) -let rec map_aval f = function - | AE_val v -> AE_val (f v) - | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_aval f aexp) - | AE_app (id, vs, typ) -> AE_app (id, List.map f vs, typ) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> - AE_let (id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) - | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ) - | AE_return (aval, typ) -> AE_return (f aval, typ) - | AE_throw (aval, typ) -> AE_throw (f aval, typ) - | AE_if (aval, aexp1, aexp2, typ2) -> - AE_if (f aval, map_aval f aexp1, map_aval f aexp2, typ2) - | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_aval f aexp1, map_aval f aexp2) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> - AE_for (id, map_aval f aexp1, map_aval f aexp2, map_aval f aexp3, order, map_aval f aexp4) - | AE_record_update (aval, updates, typ) -> - AE_record_update (f aval, Bindings.map f updates, typ) - | AE_field (aval, field, typ) -> - AE_field (f aval, field, typ) - | AE_case (aval, cases, typ) -> - AE_case (f aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) - | AE_try (aexp, cases, typ) -> - AE_try (map_aval f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f aval, map_aval f aexp) +let rec map_aval f (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_val v -> AE_val (f v) + | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_aval f aexp) + | AE_app (id, vs, typ) -> AE_app (id, List.map f vs, typ) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> + AE_let (id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ) + | AE_return (aval, typ) -> AE_return (f aval, typ) + | AE_throw (aval, typ) -> AE_throw (f aval, typ) + | AE_if (aval, aexp1, aexp2, typ2) -> + AE_if (f aval, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_aval f aexp1, map_aval f aexp2) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + AE_for (id, map_aval f aexp1, map_aval f aexp2, map_aval f aexp3, order, map_aval f aexp4) + | AE_record_update (aval, updates, typ) -> + AE_record_update (f aval, Bindings.map f updates, typ) + | AE_field (aval, field, typ) -> + AE_field (f aval, field, typ) + | AE_case (aval, cases, typ) -> + AE_case (f aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) + | AE_try (aexp, cases, typ) -> + AE_try (map_aval f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f aval, map_aval f aexp) + in + AE_aux (aexp, env, l) (* Map over all the functions in an aexp. *) -let rec map_functions f = function - | AE_app (id, vs, typ) -> f id vs typ - | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2) - | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) - | AE_if (aval, aexp1, aexp2, typ) -> - AE_if (aval, map_functions f aexp1, map_functions f aexp2, typ) - | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_functions f aexp1, map_functions f aexp2) - | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> - AE_for (id, map_functions f aexp1, map_functions f aexp2, map_functions f aexp3, order, map_functions f aexp4) - | AE_case (aval, cases, typ) -> - AE_case (aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) - | AE_try (aexp, cases, typ) -> - AE_try (map_functions f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) - | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v +let rec map_functions f (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_app (id, vs, typ) -> f id vs typ + | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp) + | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) + | AE_if (aval, aexp1, aexp2, typ) -> + AE_if (aval, map_functions f aexp1, map_functions f aexp2, typ) + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_functions f aexp1, map_functions f aexp2) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + AE_for (id, map_functions f aexp1, map_functions f aexp2, map_functions f aexp3, order, map_functions f aexp4) + | AE_case (aval, cases, typ) -> + AE_case (aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) + | AE_try (aexp, cases, typ) -> + AE_try (map_functions f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) + | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v + in + AE_aux (aexp, env, l) (* For debugging we provide a pretty printer for ANF expressions. *) @@ -372,7 +392,8 @@ let pp_order = function | Ord_aux (Ord_dec, _) -> string "dec" | _ -> assert false (* Order types have been specialised, so no polymorphism in C backend. *) -let rec pp_aexp = function +let rec pp_aexp (AE_aux (aexp, _, _)) = + match aexp with | AE_val v -> pp_aval v | AE_cast (aexp, typ) -> pp_annot typ (string "$" ^^ pp_aexp aexp) @@ -387,7 +408,7 @@ let rec pp_aexp = function | AE_let (id, id_typ, binding, body, typ) -> group begin match binding with - | AE_let _ -> + | AE_aux (AE_let _, _, _) -> (pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="]) ^^ hardline ^^ nest 2 (pp_aexp binding)) ^^ hardline ^^ string "in" ^^ space ^^ pp_aexp body @@ -502,12 +523,16 @@ let rec apat_globals = function | AP_app (_, apat) -> apat_globals apat | AP_cons (hd_apat, tl_apat) -> apat_globals hd_apat @ apat_globals tl_apat -let rec anf (E_aux (e_aux, exp_annot) as exp) = - let to_aval = function +let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = + let mk_aexp aexp = AE_aux (aexp, env_of_annot exp_annot, l) in + + let to_aval (AE_aux (aexp_aux, env, l) as aexp) = + let mk_aexp aexp = AE_aux (aexp, env, l) in + match aexp_aux with | AE_val v -> (v, fun x -> x) - | AE_short_circuit (_, _, _) as aexp -> + | AE_short_circuit (_, _, _) -> let id = gensym () in - (AV_id (id, Local (Immutable, bool_typ)), fun x -> AE_let (id, bool_typ, aexp, x, typ_of exp)) + (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp (AE_let (id, bool_typ, aexp, x, typ_of exp))) | AE_app (_, _, typ) | AE_let (_, _, _, _, typ) | AE_return (_, typ) @@ -517,31 +542,30 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | AE_field (_, _, typ) | AE_case (_, _, typ) | AE_try (_, _, typ) - | AE_record_update (_, _, typ) - as aexp -> + | AE_record_update (_, _, typ) -> let id = gensym () in - (AV_id (id, Local (Immutable, typ)), fun x -> AE_let (id, typ, aexp, x, typ_of exp)) - | AE_assign _ | AE_block _ | AE_for _ | AE_loop _ as aexp -> + (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (id, typ, aexp, x, typ_of exp))) + | AE_assign _ | AE_block _ | AE_for _ | AE_loop _ -> let id = gensym () in - (AV_id (id, Local (Immutable, unit_typ)), fun x -> AE_let (id, unit_typ, aexp, x, typ_of exp)) + (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (id, unit_typ, aexp, x, typ_of exp))) in match e_aux with - | E_lit lit -> ae_lit lit (typ_of exp) + | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) | E_block exps -> let exps, last = split_block exps in let aexps = List.map anf exps in let alast = anf last in - AE_block (aexps, alast, typ_of exp) + mk_aexp (AE_block (aexps, alast, typ_of exp)) | E_assign (LEXP_aux (LEXP_deref dexp, _), exp) -> let gs = gensym () in - AE_let (gs, typ_of dexp, anf dexp, AE_assign (gs, typ_of dexp, anf exp), unit_typ) + mk_aexp (AE_let (gs, typ_of dexp, anf dexp, mk_aexp (AE_assign (gs, typ_of dexp, anf exp)), unit_typ)) | E_assign (LEXP_aux (LEXP_id id, _), exp) - | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> + | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> let aexp = anf exp in - AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp) + mk_aexp (AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp)) | E_assign (lexp, _) -> failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") @@ -549,17 +573,17 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | E_loop (loop_typ, cond, exp) -> let acond = anf cond in let aexp = anf exp in - AE_loop (loop_typ, acond, aexp) + mk_aexp (AE_loop (loop_typ, acond, aexp)) | E_for (id, exp1, exp2, exp3, order, body) -> let aexp1, aexp2, aexp3, abody = anf exp1, anf exp2, anf exp3, anf body in - AE_for (id, aexp1, aexp2, aexp3, order, abody) + mk_aexp (AE_for (id, aexp1, aexp2, aexp3, order, abody)) | E_if (cond, then_exp, else_exp) -> let cond_val, wrap = to_aval (anf cond) in let then_aexp = anf then_exp in let else_aexp = anf else_exp in - wrap (AE_if (cond_val, then_aexp, else_aexp, typ_of then_exp)) + wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of then_exp))) | E_app_infix (x, Id_aux (Id op, l), y) -> anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot)) @@ -570,85 +594,85 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (AE_val (AV_vector (List.map fst avals, typ_of exp))) + wrap (mk_aexp (AE_val (AV_vector (List.map fst avals, typ_of exp)))) | E_list exps -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (AE_val (AV_list (List.map fst avals, typ_of exp))) + wrap (mk_aexp (AE_val (AV_list (List.map fst avals, typ_of exp)))) | E_field (field_exp, id) -> let aval, wrap = to_aval (anf field_exp) in - wrap (AE_field (aval, id, typ_of exp)) + wrap (mk_aexp (AE_field (aval, id, typ_of exp))) | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> - let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = - let aval, wrap = to_aval (anf exp) in - (id, aval), wrap - in - let aval, exp_wrap = to_aval (anf exp) in - let fexps = List.map anf_fexp fexps in - let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in - let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in - exp_wrap (wrap (AE_record_update (aval, record, typ_of exp))) + let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = + let aval, wrap = to_aval (anf exp) in + (id, aval), wrap + in + let aval, exp_wrap = to_aval (anf exp) in + let fexps = List.map anf_fexp fexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in + let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in + exp_wrap (wrap (mk_aexp (AE_record_update (aval, record, typ_of exp)))) | E_app (id, [exp1; exp2]) when string_of_id id = "and_bool" -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap = to_aval aexp1 in - wrap (AE_short_circuit (SC_and, aval1, aexp2)) + wrap (mk_aexp (AE_short_circuit (SC_and, aval1, aexp2))) | E_app (id, [exp1; exp2]) when string_of_id id = "or_bool" -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap = to_aval aexp1 in - wrap (AE_short_circuit (SC_or, aval1, aexp2)) + wrap (mk_aexp (AE_short_circuit (SC_or, aval1, aexp2))) | E_app (id, exps) -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (AE_app (id, List.map fst avals, typ_of exp)) + wrap (mk_aexp (AE_app (id, List.map fst avals, typ_of exp))) | E_throw exn_exp -> let aexp = anf exn_exp in let aval, wrap = to_aval aexp in - wrap (AE_throw (aval, typ_of exp)) + wrap (mk_aexp (AE_throw (aval, typ_of exp))) | E_exit exp -> let aexp = anf exp in let aval, wrap = to_aval aexp in - wrap (AE_app (mk_id "sail_exit", [aval], unit_typ)) + wrap (mk_aexp (AE_app (mk_id "sail_exit", [aval], unit_typ))) | E_return ret_exp -> let aexp = anf ret_exp in let aval, wrap = to_aval aexp in - wrap (AE_return (aval, typ_of exp)) + wrap (mk_aexp (AE_return (aval, typ_of exp))) | E_assert (exp1, exp2) -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (AE_app (mk_id "sail_assert", [aval1; aval2], unit_typ))) + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_assert", [aval1; aval2], unit_typ)))) | E_cons (exp1, exp2) -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (AE_app (mk_id "cons", [aval1; aval2], unit_typ))) + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "cons", [aval1; aval2], unit_typ)))) | E_id id -> let lvar = Env.lookup_id id (env_of exp) in begin match lvar with - | _ -> AE_val (AV_id (id, lvar)) + | _ -> mk_aexp (AE_val (AV_id (id, lvar))) end | E_ref id -> let lvar = Env.lookup_id id (env_of exp) in - AE_val (AV_ref (id, lvar)) + mk_aexp (AE_val (AV_ref (id, lvar))) | E_case (match_exp, pexps) -> let match_aval, match_wrap = to_aval (anf match_exp) in @@ -657,9 +681,9 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | Pat_when (pat, guard, body) -> (anf_pat pat, anf guard, anf body) | Pat_exp (pat, body) -> - (anf_pat pat, AE_val (AV_lit (mk_lit (L_true), bool_typ)), anf body) + (anf_pat pat, mk_aexp (AE_val (AV_lit (mk_lit (L_true), bool_typ))), anf body) in - match_wrap (AE_case (match_aval, List.map anf_pexp pexps, typ_of exp)) + match_wrap (mk_aexp (AE_case (match_aval, List.map anf_pexp pexps, typ_of exp))) | E_try (match_exp, pexps) -> let match_aexp = anf match_exp in @@ -668,16 +692,16 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = | Pat_when (pat, guard, body) -> (anf_pat pat, anf guard, anf body) | Pat_exp (pat, body) -> - (anf_pat pat, AE_val (AV_lit (mk_lit (L_true), bool_typ)), anf body) + (anf_pat pat, mk_aexp (AE_val (AV_lit (mk_lit (L_true), bool_typ))), anf body) in - AE_try (match_aexp, List.map anf_pexp pexps, typ_of exp) + mk_aexp (AE_try (match_aexp, List.map anf_pexp pexps, typ_of exp)) | E_var (LEXP_aux (LEXP_id id, _), binding, body) - | E_var (LEXP_aux (LEXP_cast (_, id), _), binding, body) - | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> + | E_var (LEXP_aux (LEXP_cast (_, id), _), binding, body) + | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> let env = env_of body in let lvar = Env.lookup_id id env in - AE_let (id, lvar_typ lvar, anf binding, anf body, typ_of exp) + mk_aexp (AE_let (id, lvar_typ lvar, anf binding, anf body, typ_of exp)) | E_var (lexp, _, _) -> failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") @@ -689,7 +713,7 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (AE_val (AV_tuple (List.map fst avals))) + wrap (mk_aexp (AE_val (AV_tuple (List.map fst avals)))) | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = @@ -699,9 +723,9 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let fexps = List.map anf_fexp fexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in - wrap (AE_val (AV_record (record, typ_of exp))) + wrap (mk_aexp (AE_val (AV_record (record, typ_of exp)))) - | E_cast (typ, exp) -> AE_cast (anf exp, typ) + | E_cast (typ, exp) -> mk_aexp (AE_cast (anf exp, typ)) | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ -> (* Should be re-written by type checker *) @@ -738,7 +762,8 @@ type ctx = enums : IdSet.t Bindings.t; variants : (ctyp Bindings.t) Bindings.t; tc_env : Env.t; - letbinds : int list + letbinds : int list; + recursive_functions : IdSet.t } let initial_ctx env = @@ -746,7 +771,8 @@ let initial_ctx env = enums = Bindings.empty; variants = Bindings.empty; tc_env = env; - letbinds = [] + letbinds = []; + recursive_functions = IdSet.empty } let rec ctyp_equal ctyp1 ctyp2 = @@ -971,6 +997,7 @@ let analyze_primop' ctx id args typ = (* prerr_endline ("Analysing: " ^ string_of_typ typ ^ " " ^ extern ^ Pretty_print_sail.to_string (separate_map (string ", ") pp_aval args)); *) let v_one = F_lit (V_int (Big_int.of_int 1)) in + let v_int n = F_lit (V_int (Big_int.of_int n)) in match extern, args with | "eq_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> @@ -978,7 +1005,7 @@ let analyze_primop' ctx id args typ = | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] -> let len = F_op (f, "-", F_op (t, "-", v_one)) in - AE_val (AV_C_fragment (F_op (F_op (F_op (v_one, "<<", len), "-", v_one), "&", F_op (vec, ">>", t)), typ)) + AE_val (AV_C_fragment (F_op (F_op (F_raw "UINT64_MAX", ">>", F_op (v_int 64, "-", len)), "&", F_op (vec, ">>", t)), typ)) | "vector_access", [AV_C_fragment (vec, _); AV_C_fragment (n, _)] -> AE_val (AV_C_fragment (F_op (v_one, "&", F_op (vec, ">>", n)), typ)) @@ -987,7 +1014,7 @@ let analyze_primop' ctx id args typ = AE_val (AV_C_fragment (F_op (a, "==", b), typ)) | "slice", [AV_C_fragment (vec, _); AV_C_fragment (start, _); AV_C_fragment (len, _)] -> - AE_val (AV_C_fragment (F_op (F_op (F_op (v_one, "<<", len), "-", v_one), "&", F_op (vec, ">>", start)), typ)) + AE_val (AV_C_fragment (F_op (F_op (F_raw "UINT64_MAX", ">>", F_op (v_int 64, "-", len)), "&", F_op (vec, ">>", start)), typ)) | "undefined_bit", _ -> AE_val (AV_C_fragment (F_lit (V_bit Sail_values.B0), typ)) @@ -1544,7 +1571,6 @@ let compile_funcall ctx id args typ = (List.rev !setup, final_ctyp, call, !cleanup) let rec compile_match ctx apat cval case_label = - prerr_endline ("Compiling match " ^ Pretty_print_sail.to_string (pp_apat apat) ^ " cval " ^ Pretty_print_sail.to_string (pp_cval cval)); match apat, cval with | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], @@ -1620,7 +1646,8 @@ let label str = incr label_counter; str -let rec compile_aexp ctx = function +let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = + match aexp_aux with | AE_let (id, _, binding, body, typ) -> let setup, ctyp, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = @@ -1658,8 +1685,8 @@ let rec compile_aexp ctx = function let finish_match_label = label "finish_match_" in let compile_case (apat, guard, body) = let trivial_guard = match guard with - | AE_val (AV_lit (L_aux (L_true, _), _)) - | AE_val (AV_C_fragment (F_lit (V_bool true), _)) -> true + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) + | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _)), _, _) -> true | _ -> false in let case_label = label "case_" in @@ -1697,8 +1724,8 @@ let rec compile_aexp ctx = function let handled_exception_label = label "handled_exception_" in let compile_case (apat, guard, body) = let trivial_guard = match guard with - | AE_val (AV_lit (L_aux (L_true, _), _)) - | AE_val (AV_C_fragment (F_lit (V_bool true), _)) -> true + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) + | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _)), _, _) -> true | _ -> false in let try_label = label "try_" in @@ -1733,13 +1760,31 @@ let rec compile_aexp ctx = function let if_ctyp = ctyp_of_typ ctx if_typ in let compile_branch aexp = let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - fun clexp -> setup @ [call clexp] @ cleanup + if ctyp_equal if_ctyp ctyp then + fun clexp -> setup @ [call clexp] @ cleanup + else if is_stack_ctyp ctyp then + fun clexp -> + let gs = gensym() in + setup + @ [idecl ctyp gs; + call (CL_id gs); + iconvert clexp if_ctyp gs ctyp] + @ cleanup + else + fun clexp -> + let gs = gensym () in + setup + @ [idecl ctyp gs; + ialloc ctyp gs; + call (CL_id gs); + iconvert clexp if_ctyp gs ctyp; + iclear ctyp gs] + @ cleanup in - let setup, ctyp, call, cleanup = compile_aexp ctx (AE_val aval) in - let gs = gensym () in - setup @ [idecl ctyp gs; call (CL_id gs)], + let setup, cval, cleanup = compile_aval ctx aval in + setup, if_ctyp, - (fun clexp -> iif (F_id gs, ctyp) + (fun clexp -> iif cval (compile_branch then_aexp clexp) (compile_branch else_aexp clexp) if_ctyp), @@ -1792,7 +1837,7 @@ let rec compile_aexp ctx = function (* This is a faster assignment rule for updating fields of a struct. Turned on by !optimize_struct_updates. *) - | AE_assign (id, assign_typ, AE_record_update (AV_id (rid, _), fields, typ)) + | AE_assign (id, assign_typ, AE_aux (AE_record_update (AV_id (rid, _), fields, typ), _, _)) when Id.compare id rid = 0 && !optimize_struct_updates -> let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in @@ -1869,7 +1914,7 @@ let rec compile_aexp ctx = function let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in let unit_gs = gensym () in - let loop_test = (F_unary ("!", F_id gs), CT_bool) in + let loop_test = (F_id gs, CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (body_setup @@ -1888,9 +1933,28 @@ let rec compile_aexp ctx = function | AE_cast (aexp, typ) -> compile_aexp ctx aexp | AE_return (aval, typ) -> + let fn_return_ctyp = match Env.get_ret_typ env with + | Some typ -> ctyp_of_typ ctx typ + | None -> c_error ~loc:l "No function return type found when compiling return statement" + in (* Cleanup info will be re-added by fix_early_return *) let return_setup, cval, _ = compile_aval ctx aval in - return_setup @ [ireturn cval], + let creturn = + if ctyp_equal fn_return_ctyp (cval_ctyp cval) then + [ireturn cval] + else if is_stack_ctyp (cval_ctyp cval) && not (is_stack_ctyp fn_return_ctyp) then + let gs1 = gensym () in + let gs2 = gensym () in + [idecl (cval_ctyp cval) gs1; + icopy (CL_id gs1) cval; + idecl fn_return_ctyp gs2; + ialloc fn_return_ctyp gs2; + iconvert (CL_id gs2) fn_return_ctyp gs1 (cval_ctyp cval); + ireturn (F_id gs2, fn_return_ctyp)] + else + c_error ~loc:l "Can only do return type conversion from stack to heap" + in + return_setup @ creturn, ctyp_of_typ ctx typ, (fun clexp -> icomment "unreachable after return"), [] @@ -1911,10 +1975,62 @@ let rec compile_aexp ctx = function (fun clexp -> icopy clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), cleanup - | AE_for _ -> - [], + | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) -> + (* This is a bit of a hack, we force loop_var to be CT_int64 by + forcing it's type to be a known nexp that will map to + CT_int64. *) + let make_small = function + | AV_id (id, Local (Immutable, typ)) when Id.compare id loop_var = 0 -> AV_id (id, Local (Immutable, atom_typ (nint 0))) + | aval -> aval + in + let body = map_aval make_small body in + + let is_inc = match ord with + | Ord_inc -> true + | Ord_dec -> false + | Ord_var _ -> c_error "Polymorphic loop direction in C backend" + in + + (* Loop variables *) + let from_setup, from_ctyp, from_call, from_cleanup = compile_aexp ctx loop_from in + let from_gs = gensym () in + let to_setup, to_ctyp, to_call, to_cleanup = compile_aexp ctx loop_to in + let to_gs = gensym () in + let step_setup, step_ctyp, step_call, step_cleanup = compile_aexp ctx loop_step in + let step_gs = gensym () in + let variable_init gs setup ctyp call cleanup = + [idecl CT_int64 gs; + if is_stack_ctyp ctyp then + iblock (setup @ [call (CL_id gs)] @ cleanup) + else + let gs' = gensym () in + iblock (setup + @ [idecl ctyp gs'; ialloc ctyp gs'; call (CL_id gs'); iconvert (CL_id gs) CT_int64 gs' ctyp; iclear ctyp gs'] + @ cleanup)] + in + + let loop_start_label = label "for_start_" in + let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in + let body_gs = gensym () in + + variable_init from_gs from_setup from_ctyp from_call from_cleanup + @ variable_init to_gs to_setup to_ctyp to_call to_cleanup + @ variable_init step_gs step_setup step_ctyp step_call step_cleanup + @ [iblock ([idecl CT_int64 loop_var; + icopy (CL_id loop_var) (F_id from_gs, CT_int64); + ilabel loop_start_label; + idecl CT_unit body_gs; + iblock (body_setup + @ [body_call (CL_id body_gs)] + @ body_cleanup + @ if is_inc then + [icopy (CL_id loop_var) (F_op (F_id loop_var, "+", F_id step_gs), CT_int64); + ijump (F_op (F_id loop_var, "<=", F_id to_gs), CT_bool) loop_start_label] + else + [icopy (CL_id loop_var) (F_op (F_id loop_var, "-", F_id step_gs), CT_int64); + ijump (F_op (F_id loop_var, ">=", F_id to_gs), CT_bool) loop_start_label])])], CT_unit, - (fun clexp -> icomment "for loop"), + (fun clexp -> icopy clexp unit_fragment), [] (* @@ -2008,7 +2124,7 @@ let fix_early_return ret ctx instrs = | instrs, [] -> instrs | before, I_aux (I_block instrs, _) :: after -> before - @ [iblock (rewrite_return (generate_cleanup (historic @ before)) instrs)] + @ [iblock (rewrite_return (historic @ before) instrs)] @ rewrite_return (historic @ before) after | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> let historic = historic @ before in @@ -2045,7 +2161,7 @@ let fix_early_stack_return ctx instrs = | instrs, [] -> instrs | before, I_aux (I_block instrs, _) :: after -> before - @ [iblock (rewrite_return (generate_cleanup (historic @ before)) instrs)] + @ [iblock (rewrite_return (historic @ before) instrs)] @ rewrite_return (historic @ before) after | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> let historic = historic @ before in @@ -2053,9 +2169,8 @@ let fix_early_stack_return ctx instrs = @ [iif cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp] @ rewrite_return historic after | before, (I_aux (I_return cval, _) as ret) :: after -> - let cleanup_label = label "cleanup_" in - let end_cleanup_label = label "end_cleanup_" in before + @ [icomment "early return cleanup"] @ generate_cleanup (historic @ before) @ [ret] (* There could be jumps into here *) @@ -2080,7 +2195,7 @@ let fix_exception_block ctx instrs = | instrs, [] -> instrs | before, I_aux (I_block instrs, _) :: after -> before - @ [iblock (rewrite_exception (generate_cleanup (historic @ before)) instrs)] + @ [iblock (rewrite_exception (historic @ before) instrs)] @ rewrite_exception (historic @ before) after | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> let historic = historic @ before in @@ -2177,7 +2292,7 @@ let rec compile_def ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in - prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)); + (* prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)); *) let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let fundef_label = label "fundef_fail_" in let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in @@ -2334,6 +2449,7 @@ let rec fragment_deps = function | F_op (frag1, _, frag2) -> NS.union (fragment_deps frag1) (fragment_deps frag2) | F_current_exception -> NS.empty | F_have_exception -> NS.empty + | F_raw _ -> NS.empty let cval_deps = function (frag, _) -> fragment_deps frag @@ -2513,6 +2629,10 @@ let hoist_id () = id let hoist_allocations ctx = function + | CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id ctx.recursive_functions -> + c_debug (lazy (Printf.sprintf "skipping recursive function %s" (string_of_id function_id))); + [cdef] + | CDEF_fundef (function_id, heap_return, args, body) -> let decls = ref [] in let cleanups = ref [] in @@ -2615,7 +2735,13 @@ let concatMap f xs = List.concat (List.map f xs) let optimize ctx cdefs = let nothing cdefs = cdefs in cdefs - |> if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing + |> if !optimize_hoist_allocations then + begin + c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Hoisting allocations")); + concatMap (hoist_allocations ctx) + end + else + nothing (**************************************************************************) (* 7. Code generation *) @@ -2760,7 +2886,12 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = | "undefined_vector", _ -> Printf.sprintf "undefined_vector_%s" (sgen_ctyp_name ctyp) | fname, _ -> fname in - if is_stack_ctyp ctyp then + if fname = "reg_deref" then + if is_stack_ctyp ctyp then + string (Printf.sprintf " %s = *(%s);" (sgen_clexp_pure x) c_args) + else + string (Printf.sprintf " set_%s(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args) + else if is_stack_ctyp ctyp then string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) else string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) @@ -2786,7 +2917,10 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = special conversion code-generator for full generality *) | I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 -> let convert i (ctyp1, ctyp2) = - if ctyp_equal ctyp1 ctyp2 then string " /* no change */" + if ctyp_equal ctyp1 ctyp2 then + string (Printf.sprintf " %s.ztup%i = %s.ztup%i;" (sgen_clexp_pure x) i (sgen_id y) i) + else if ctyp_equal ctyp1 ctyp2 then + c_error "heap tuple type conversion" else if is_stack_ctyp ctyp1 then string (Printf.sprintf " %s.ztup%i = convert_%s_of_%s(%s.ztup%i);" (sgen_clexp_pure x) @@ -3172,7 +3306,7 @@ let codegen_vector ctx (direction, ctyp) = ^^ string "}" in let internal_vector_update = - string (Printf.sprintf "void internal_vector_update_%s(%s *rop, %s op, const int64_t n, const %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + string (Printf.sprintf "void internal_vector_update_%s(%s *rop, %s op, const int64_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) ^^ string (if is_stack_ctyp ctyp then " rop->data[n] = elem;\n" else @@ -3285,9 +3419,11 @@ let codegen_def' ctx = function instrs in function_header + (* ^^ string (Printf.sprintf "{ fprintf(stderr, \"%s \"); " (string_of_id id)) *) ^^ string "{" ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline ^^ string "}" + (* ^^ string "}" *) | CDEF_type ctype_def -> codegen_type_def ctx ctype_def @@ -3341,7 +3477,7 @@ let codegen_def ctx def = let lists = List.map (fun ctyp -> codegen_list ctx (unlist ctyp)) lists in let vectors = List.filter is_ct_vector (cdef_ctyps ctx def) in let vectors = List.map (fun ctyp -> codegen_vector ctx (unvector ctyp)) vectors in - prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); + (* prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); *) concat tups ^^ concat lists ^^ concat vectors @@ -3373,8 +3509,21 @@ let bytecode_ast ctx rewrites (Defs defs) = let cdefs = List.concat (List.rev chunks) in rewrites cdefs +let rec get_recursive_functions (Defs defs) = + match defs with + | DEF_internal_mutrec fundefs :: defs -> + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + | _ :: defs -> get_recursive_functions (Defs defs) + | [] -> IdSet.empty + + let compile_ast ctx (Defs defs) = try + c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Identifying recursive functions")); + let recursive_functions = Spec_analysis.top_sort_defs (Defs defs) |> get_recursive_functions in + let ctx = { ctx with recursive_functions = recursive_functions } in + c_debug (lazy (Util.string_of_list ", " string_of_id (IdSet.elements recursive_functions))); + let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in let ctx = { ctx with tc_env = snd (check ctx.tc_env (Defs [assert_vs; exit_vs])) } in @@ -3444,4 +3593,4 @@ let compile_ast ctx (Defs defs) = Pretty_print_sail.to_string (preamble ^^ hlhl ^^ separate hlhl docs ^^ hlhl ^^ postamble) |> print_endline with - Type_error (l, err) -> prerr_endline ("Unexpected type error when compiling to C:\n" ^ string_of_type_error err) + Type_error (l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ string_of_type_error err) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index a709a8c1..0f384cab 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -45,12 +45,19 @@ let negate_real r = realNegate r let abs_real r = realAbs r let power_real b e = realPowInteger b e*) +val print_endline : string -> unit +let print_endline _ = () +declare ocaml target_rep function print_endline = `print_endline` + val prerr_endline : string -> unit let prerr_endline _ = () declare ocaml target_rep function prerr_endline = `prerr_endline` val print_int : string -> integer -> unit -let print_int msg i = prerr_endline (msg ^ (stringFromInteger i)) +let print_int msg i = print_endline (msg ^ (stringFromInteger i)) + +val prerr_int : string -> integer -> unit +let prerr_int msg i = prerr_endline (msg ^ (stringFromInteger i)) val putchar : integer -> unit let putchar _ = () diff --git a/src/interpreter.ml b/src/interpreter.ml index e62fcfc3..03fd8496 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -109,6 +109,14 @@ let value_of_lit (L_aux (l_aux, _)) = Util.string_to_list str |> List.map (fun c -> V_bit (Sail_lib.bin_char c)) |> (fun v -> V_vector v) + | L_real str -> + begin match Util.split_on_char '.' str with + | [whole; frac] -> + let whole = Rational.of_int (int_of_string whole) in + let frac = Rational.div (Rational.of_int (int_of_string frac)) (Rational.of_int (Util.power 10 (String.length frac))) in + V_real (Rational.add whole frac) + | _ -> failwith "could not parse real literal" + end | _ -> failwith "Unimplemented value_of_lit" (* TODO *) let is_value = function @@ -254,7 +262,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = step exp >>= fun exp' -> wrap (E_if (exp', then_exp, else_exp)) | E_loop (While, exp, body) -> wrap (E_if (exp, E_aux (E_block [body; orig_exp], annot), exp_of_value V_unit)) - | E_loop (Until, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, orig_exp, exp_of_value V_unit), annot)]) + | E_loop (Until, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, exp_of_value V_unit, orig_exp), annot)]) | E_assert (exp, msg) when is_true exp -> wrap unit_exp | E_assert (exp, msg) when is_false exp && is_value msg -> @@ -524,11 +532,22 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let v_from = value_of_exp exp_from in let v_to = value_of_exp exp_to in let v_step = value_of_exp exp_step in - begin match value_gt [v_from; v_to] with - | V_bool true -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) - | V_bool false -> - wrap (E_block [subst id v_from body; E_aux (E_for (id, exp_of_value (value_add_int [v_from; v_step]), exp_to, exp_step, ord, body), annot)]) - | _ -> assert false + begin match ord with + | Ord_aux (Ord_inc, _) -> + begin match value_gt [v_from; v_to] with + | V_bool true -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) + | V_bool false -> + wrap (E_block [subst id v_from body; E_aux (E_for (id, exp_of_value (value_add_int [v_from; v_step]), exp_to, exp_step, ord, body), annot)]) + | _ -> assert false + end + | Ord_aux (Ord_dec, _) -> + begin match value_lt [v_from; v_to] with + | V_bool true -> wrap (E_lit (L_aux (L_unit, Parse_ast.Unknown))) + | V_bool false -> + wrap (E_block [subst id v_from body; E_aux (E_for (id, exp_of_value (value_sub_int [v_from; v_step]), exp_to, exp_step, ord, body), annot)]) + | _ -> assert false + end + | Ord_aux (Ord_var _, _) -> failwith "Polymorphic order in foreach" end | E_for (id, exp_from, exp_to, exp_step, ord, body) when is_value exp_to && is_value exp_step -> step exp_from >>= fun exp_from' -> wrap (E_for (id, exp_from', exp_to, exp_step, ord, body)) @@ -616,7 +635,7 @@ let stack_state (_, lstate, _) = lstate type frame = | Done of state * value - | Step of string * state * (Type_check.tannot exp) monad * (string * lstate * (value -> (Type_check.tannot exp) monad)) list + | Step of string Lazy.t * state * (Type_check.tannot exp) monad * (string Lazy.t * lstate * (value -> (Type_check.tannot exp) monad)) list | Break of frame let rec eval_frame' ast = function @@ -629,17 +648,17 @@ let rec eval_frame' ast = function (* print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear); *) Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack') | Pure exp', _ -> - let out' = Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp') in + let out' = lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp')) in Step (out', state, step exp', stack) | Yield (Call(id, vals, cont)), _ when string_of_id id = "break" -> let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in let body = exp_of_fundef (get_fundef id ast) arg in - Break (Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)) + Break (Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)) | Yield (Call(id, vals, cont)), _ -> (* print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); *) let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in let body = exp_of_fundef (get_fundef id ast) arg in - Step ("", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack) + Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack) | Yield (Gets cont), _ -> eval_frame' ast (Step (out, state, cont state, stack)) | Yield (Puts (state', cont)), _ -> diff --git a/src/isail.ml b/src/isail.ml index 5cd23f83..0bfb06e2 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -110,8 +110,8 @@ let print_program () = | Normal -> () | Evaluation (Step (out, _, _, stack)) -> let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in - List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep); - print_endline out + List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline (Lazy.force code); print_endline sep); + print_endline (Lazy.force out) | Evaluation (Done (_, v)) -> print_endline (Value.string_of_value v |> Util.green |> Util.clear) | Evaluation _ -> () @@ -135,6 +135,7 @@ let rec run () = end let rec run_steps n = + print_endline ("step " ^ string_of_int n); match !current_mode with | _ when n <= 0 -> () | Normal -> () @@ -320,7 +321,7 @@ let handle_input' input = (* An expression in normal mode is type checked, then puts us in evaluation mode. *) let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord str) in - current_mode := Evaluation (eval_frame !interactive_ast (Step ("", !interactive_state, return exp, []))); + current_mode := Evaluation (eval_frame !interactive_ast (Step (lazy "", !interactive_state, return exp, []))); print_program () | Empty -> () end diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index a13d7b4b..1feb6513 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -248,8 +248,8 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = (ocaml_atomic_exp ctx body ^^ semi) ^/^ separate space [string "if"; ocaml_atomic_exp ctx cond; - string "then loop ()"; - string "else ()"] + string "then ()"; + string "else loop ()"] in (string "let rec loop () =" ^//^ loop_body) ^/^ string "in" diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 28784ce1..082df4c1 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -510,8 +510,8 @@ let gteq_real (x, y) = Rational.geq x y let to_real x = Rational.of_int (Big_int.to_int x) (* FIXME *) let negate_real x = Rational.neg x -let round_down x = failwith "round_down" (* Num.big_int_of_num (Num.floor_num x) *) -let round_up x = failwith "round_up" (* Num.big_int_of_num (Num.ceiling_num x) *) +let round_down x = Rational.floor x (* Num.big_int_of_num (Num.floor_num x) *) +let round_up x = Rational.ceiling x (* Num.big_int_of_num (Num.ceiling_num x) *) let quotient_real (x, y) = Rational.div x y let mult_real (x, y) = Rational.mul x y (* Num.mult_num x y *) let real_power (x, y) = failwith "real_power" (* Num.power_num x (Num.num_of_big_int y) *) @@ -541,26 +541,33 @@ let rec pow x = function | n -> x * pow x (n - 1) let real_of_string str = - let rat_of_string sr = Rational.of_int (int_of_string str) in - try - let point = String.index str '.' in - let whole = Rational.of_int (int_of_string (String.sub str 0 point)) in - let frac_str = String.sub str (point + 1) (String.length str - (point + 1)) in - let frac = Rational.div (rat_of_string frac_str) (Rational.of_int (pow 10 (String.length frac_str))) in - Rational.add whole frac - with - | Not_found -> Rational.of_int (int_of_string str) + match String.split_on_char '.' str with + | [whole; frac] -> + let whole = Rational.of_int (int_of_string whole) in + let frac = Rational.div (Rational.of_int (int_of_string frac)) (Rational.of_int (pow 10 (String.length frac))) in + Rational.add whole frac + | [whole] -> Rational.of_int (int_of_string str) + | _ -> failwith "invalid real literal" (* Not a very good sqrt implementation *) let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *) let print_int (str, x) = + print_endline (str ^ Big_int.to_string x) + +let prerr_int (str, x) = prerr_endline (str ^ Big_int.to_string x) let print_bits (str, xs) = + print_endline (str ^ string_of_bits xs) + +let prerr_bits (str, xs) = prerr_endline (str ^ string_of_bits xs) let print_string(str, msg) = + print_endline (str ^ msg) + +let prerr_string(str, msg) = prerr_endline (str ^ msg) let reg_deref r = !r @@ -641,3 +648,16 @@ let trace_memory_write (_, _, _) = () let trace_memory_read (_, _, _) = () let sleep_request () = () + +let load_raw (paddr, file) = + let i = ref 0 in + let paddr = uint paddr in + let in_chan = open_in file in + try + while true do + let byte = input_char in_chan |> Char.code in + wram (Big_int.add paddr (Big_int.of_int !i)) byte; + incr i + done + with + | End_of_file -> () diff --git a/src/specialize.ml b/src/specialize.ml index 191ee3be..465c5398 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -335,12 +335,13 @@ let specialize_id_fundef instantiations id ast = let spec_id = id_of_instantiation id instantiation in if IdSet.mem spec_id !spec_ids then [] else begin + prerr_endline ("specialised fundef " ^ string_of_id id ^ " to " ^ string_of_id spec_id); spec_ids := IdSet.add spec_id !spec_ids; [DEF_fundef (rename_fundef spec_id fundef)] end in let fundefs = List.map specialize_fundef instantiations |> List.concat in - append_ast pre_ast (append_ast (Defs fundefs) post_ast) + append_ast pre_ast (append_ast (Defs (DEF_fundef fundef :: fundefs)) post_ast) | Some _ -> assert false (* unreachable *) let specialize_id_overloads instantiations id (Defs defs) = @@ -380,8 +381,11 @@ let remove_unused_valspecs env ast = let rec remove_unused (Defs defs) id = match defs with - | def :: defs when is_fundef id def -> remove_unused (Defs defs) id + | def :: defs when is_fundef id def -> + prerr_endline ("Removing fundef: " ^ string_of_id id); + remove_unused (Defs defs) id | def :: defs when is_valspec id def -> + prerr_endline ("Removing valspec: " ^ string_of_id id); remove_unused (Defs defs) id | DEF_overload (overload_id, overloads) :: defs -> begin @@ -396,7 +400,9 @@ let remove_unused_valspecs env ast = List.fold_left (fun ast id -> Defs (remove_unused ast id)) ast (IdSet.elements unused) let specialize_id id ast = + prerr_endline ("specialising: " ^ string_of_id id); let instantiations = instantiations_of id ast in + List.iter (fun i -> prerr_endline (string_of_instantiation i)) instantiations; let ast = specialize_id_valspec instantiations id ast in let ast = specialize_id_fundef instantiations id ast in @@ -424,7 +430,9 @@ let specialize_ids ids ast = let ast = List.fold_left (fun ast id -> specialize_id id ast) ast (IdSet.elements ids) in let ast = reorder_typedefs ast in let ast, _ = Type_check.check Type_check.initial_env ast in - let ast = List.fold_left (fun ast id -> rewrite_polymorphic_calls id ast) ast (IdSet.elements ids) in + let ast = + List.fold_left (fun ast id -> rewrite_polymorphic_calls id ast) ast (IdSet.elements ids) + in let ast, env = Type_check.check Type_check.initial_env ast in let ast = remove_unused_valspecs env ast in ast, env @@ -522,6 +530,7 @@ let specialize_variants ((Defs defs) as ast) env = Type_check.check Type_check.initial_env ast let rec specialize ast env = + prerr_endline (Util.log_line __MODULE__ __LINE__ "Performing specialisation pass"); let ids = polymorphic_functions (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt) ast in if IdSet.is_empty ids then specialize_variants ast env diff --git a/src/type_check.ml b/src/type_check.ml index f6717ea4..e32a9532 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -593,7 +593,7 @@ end = struct let complex_nexps = ref KBindings.empty in let simplify_nexp (Nexp_aux (nexp_aux, l) as nexp) = match nexp_aux with - | Nexp_var _ | Nexp_constant _ -> nexp + | Nexp_constant _ -> nexp (* Check this ? *) | _ -> let kid = Kid_aux (Var ("'c#" ^ string_of_int !counter), l) in complex_nexps := KBindings.add kid nexp !complex_nexps; diff --git a/src/util.ml b/src/util.ml index 471b0c4c..b54c13d4 100644 --- a/src/util.ml +++ b/src/util.ml @@ -442,3 +442,6 @@ let warn str = if !opt_warnings then prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str) else () + +let log_line str line msg = + "\n[" ^ (str ^ ":" ^ string_of_int line |> blue |> clear) ^ "] " ^ msg diff --git a/src/util.mli b/src/util.mli index 7a20a6dd..bb7aa70d 100644 --- a/src/util.mli +++ b/src/util.mli @@ -252,3 +252,5 @@ val warn : string -> unit val zencode_string : string -> string val zencode_upper_string : string -> string + +val log_line : string -> int -> string -> string diff --git a/src/value.ml b/src/value.ml index e9a98160..7972c692 100644 --- a/src/value.ml +++ b/src/value.ml @@ -73,6 +73,7 @@ type value = | V_vector of value list | V_list of value list | V_int of Big_int.num + | V_real of Rational.t | V_bool of bool | V_bit of Sail_lib.bit | V_tuple of value list @@ -128,6 +129,10 @@ let coerce_int = function | V_int i -> i | _ -> assert false +let coerce_real = function + | V_real r -> r + | _ -> assert false + let coerce_cons = function | V_list (v :: vs) -> Some (v, vs) | V_list [] -> None @@ -266,6 +271,10 @@ let value_sub_int = function | [v1; v2] -> V_int (Sail_lib.sub_int (coerce_int v1, coerce_int v2)) | _ -> failwith "value sub" +let value_negate = function + | [v1] -> V_int (Sail_lib.negate (coerce_int v1)) + | _ -> failwith "value negate" + let value_mult = function | [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2)) | _ -> failwith "value mult" @@ -282,6 +291,10 @@ let value_add_vec_int = function | [v1; v2] -> mk_vector (Sail_lib.add_vec_int (coerce_bv v1, coerce_int v2)) | _ -> failwith "value add_vec_int" +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" + let value_add_vec = function | [v1; v2] -> mk_vector (Sail_lib.add_vec (coerce_bv v1, coerce_bv v2)) | _ -> failwith "value add_vec" @@ -332,6 +345,7 @@ let rec string_of_value = function | V_unit -> "()" | V_string str -> "\"" ^ str ^ "\"" | V_ref str -> "ref " ^ str + | V_real r -> "REAL" (* No Rational.to_string *) | 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) ^ "}" @@ -385,6 +399,10 @@ let value_write_ram = function V_unit | _ -> failwith "value write_ram" +let value_load_raw = function + | [v1; v2] -> Sail_lib.load_raw (coerce_bv v1, coerce_string v2) ; V_unit + | _ -> failwith "value load_raw" + let value_putchar = function | [v] -> output_char !print_chan (char_of_int (Big_int.to_int (coerce_int v))); @@ -400,6 +418,62 @@ let value_print_int = function | [msg; n] -> output_endline (coerce_string msg ^ string_of_value n); V_unit | _ -> failwith "value print_int" +let value_print_string = function + | [msg; str] -> output_endline (coerce_string msg ^ coerce_string str); V_unit + | _ -> failwith "value print_string" + +let value_prerr_bits = function + | [msg; bits] -> prerr_endline (coerce_string msg ^ string_of_value bits); V_unit + | _ -> failwith "value prerr_bits" + +let value_prerr_int = function + | [msg; n] -> prerr_endline (coerce_string msg ^ string_of_value n); V_unit + | _ -> failwith "value prerr_int" + +let value_prerr_string = function + | [msg; str] -> output_endline (coerce_string msg ^ coerce_string str); V_unit + | _ -> failwith "value print_string" + +let value_concat_str = function + | [v1; v2] -> V_string (Sail_lib.concat_str (coerce_string v1, coerce_string v2)) + | _ -> failwith "value concat_str" + +let value_to_real = function + | [v] -> V_real (Sail_lib.to_real (coerce_int v)) + | _ -> failwith "value to_real" + +let value_quotient_real = function + | [v1; v2] -> V_real (Sail_lib.quotient_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value quotient_real" + +let value_round_up = function + | [v] -> V_int (Sail_lib.round_up (coerce_real v)) + | _ -> failwith "value round_up" + +let value_round_down = function + | [v] -> V_int (Sail_lib.round_down (coerce_real v)) + | _ -> failwith "value round_down" + +let value_eq_real = function + | [v1; v2] -> V_bool (Sail_lib.eq_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value eq_real" + +let value_lt_real = function + | [v1; v2] -> V_bool (Sail_lib.lt_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value lt_real" + +let value_gt_real = function + | [v1; v2] -> V_bool (Sail_lib.gt_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value gt_real" + +let value_lteq_real = function + | [v1; v2] -> V_bool (Sail_lib.lteq_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value lteq_real" + +let value_gteq_real = function + | [v1; v2] -> V_bool (Sail_lib.gteq_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value gteq_real" + let primops = List.fold_left (fun r (x, y) -> StringMap.add x y r) @@ -413,6 +487,11 @@ let primops = ("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); @@ -447,18 +526,34 @@ let primops = ("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); ("add_vec_int", value_add_vec_int); + ("sub_vec_int", value_sub_vec_int); ("add_vec", value_add_vec); ("sub_vec", value_sub_vec); ("read_ram", value_read_ram); ("write_ram", value_write_ram); + ("trace_memory_read", fun _ -> V_unit); + ("trace_memory_write", fun _ -> V_unit); + ("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_lt_real); + ("gteq_real", value_gt_real); + ("round_up", value_round_up); + ("round_down", value_round_down); + ("quotient_real", value_quotient_real); ("undefined_unit", fun _ -> V_unit); ("undefined_bit", fun _ -> V_bit Sail_lib.B0); ("undefined_int", fun _ -> V_int Big_int.zero); |