diff options
| -rw-r--r-- | lib/rts.c | 5 | ||||
| -rw-r--r-- | lib/sail.c | 7 | ||||
| -rw-r--r-- | lib/sail.h | 1 | ||||
| -rw-r--r-- | src/c_backend.ml | 43 |
4 files changed, 47 insertions, 9 deletions
@@ -25,7 +25,7 @@ unit sail_exit(unit u) unit sleep_request(const unit u) { fprintf(stderr, "Sail model going to sleep\n"); - exit(EXIT_SUCCESS); + return UNIT; } /* ***** Sail memory builtins ***** */ @@ -176,7 +176,8 @@ unit load_raw(mach_bits addr, const sail_string file) return UNIT; } -void load_image(char *file) { +void load_image(char *file) +{ FILE *fp = fopen(file, "r"); if (!fp) { @@ -360,6 +360,13 @@ mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits op) return mpz_get_ui(*op.bits); } +void CONVERT_OF(sail_bits, mach_bits)(sail_bits *rop, const mach_bits op, const uint64_t len) +{ + rop->len = len; + // use safe_rshift to correctly handle the case when we have a 0-length vector. + mpz_set_ui(*rop->bits, op & safe_rshift(UINT64_MAX, 64 - len)); +} + void UNDEFINED(sail_bits)(sail_bits *rop, const sail_int len, const mach_bits bit) { zeros(rop, len); @@ -176,6 +176,7 @@ void RECREATE_OF(sail_bits, mach_bits)(sail_bits *, const bool direction); mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits); +void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t); void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit); mach_bits UNDEFINED(mach_bits)(const unit); diff --git a/src/c_backend.ml b/src/c_backend.ml index 1a2981e2..ae411654 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -465,12 +465,12 @@ let gensym () = incr gensym_counter; id -let rec split_block = function +let rec split_block l = function | [exp] -> [], exp | exp :: exps -> - let exps, last = split_block exps in + let exps, last = split_block l exps in exp :: exps, last - | [] -> c_error "empty block" + | [] -> c_error ~loc:l "empty block" let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in @@ -525,7 +525,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) | E_block exps -> - let exps, last = split_block exps in + let exps, last = split_block l exps in let aexps = List.map anf exps in let alast = anf last in mk_aexp (AE_block (aexps, alast, typ_of exp)) @@ -1740,6 +1740,18 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup + else if is_stack_ctyp assign_ctyp && not (is_stack_ctyp ctyp) then + let gs = gensym () in + setup @ [ icomment comment; + idecl ctyp gs; + ialloc ctyp gs; + call (CL_id gs); + iconvert (CL_id id) assign_ctyp gs ctyp; + iclear ctyp gs + ], + CT_unit, + (fun clexp -> icopy clexp unit_fragment), + cleanup else failwith comment @@ -2159,7 +2171,7 @@ let rec compile_def ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> c_debug (lazy ("Compiling function " ^ string_of_id id)); 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)); + if string_of_id id = "fetch_and_execute" then prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)) else (); let setup, ctyp, call, cleanup = compile_aexp ctx aexp in c_debug (lazy "Compiled aexp"); let fundef_label = label "fundef_fail_" in @@ -2633,8 +2645,8 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = end | "vector_update_subrange", _ -> Printf.sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp) | "vector_subrange", _ -> Printf.sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp) - | "vector_update", CT_bits64 _ -> "update_uint64_t" - | "vector_update", CT_bits _ -> "update_bv" + | "vector_update", CT_bits64 _ -> "update_mach_bits" + | "vector_update", CT_bits _ -> "update_sail_bits" | "vector_update", _ -> Printf.sprintf "vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) @@ -2697,6 +2709,23 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = i) in separate hardline (List.mapi convert (List.map2 (fun x y -> (x, y)) ctyps1 ctyps2)) + (* If we're converting from a bits type with a known compile time + length, pass it as an extra parameter to the conversion. *) + | I_convert (x, ctyp1, y, (CT_bits64 (n, _) as ctyp2)) -> + if is_stack_ctyp ctyp1 then + string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s, %d);" + (sgen_clexp_pure x) + (sgen_ctyp_name ctyp1) + (sgen_ctyp_name ctyp2) + (sgen_id y) + n) + else + string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s, %d);" + (sgen_ctyp_name ctyp1) + (sgen_ctyp_name ctyp2) + (sgen_clexp x) + (sgen_id y) + n) | I_convert (x, ctyp1, y, ctyp2) -> if is_stack_ctyp ctyp1 then string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s);" |