diff options
| -rw-r--r-- | editors/sail2-mode.el | 5 | ||||
| -rw-r--r-- | src/c_backend.ml | 83 | ||||
| -rw-r--r-- | src/isail.ml | 13 |
3 files changed, 81 insertions, 20 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index eb3e0fe6..47ce1690 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -16,10 +16,11 @@ "exmem" "undef" "unspec" "nondet" "escape")) (defconst sail2-types - '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits")) + '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits" + "uint64_t" "int64_t" "bv_t" "mpz_t")) (defconst sail2-special - '("_prove" "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif")) + '("_prove" "create" "kill" "convert" "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif")) (defconst sail2-font-lock-keywords `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face) diff --git a/src/c_backend.ml b/src/c_backend.ml index 99e6c522..dc87cfd9 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -744,10 +744,10 @@ let rec ctyp_equal ctyp1 ctyp2 = intermediate language pretty-printer. *) let rec string_of_ctyp = function | CT_mpz -> "mpz_t" - | CT_bv true -> "bv_t<dec>" - | CT_bv false -> "bv_t<inc>" - | CT_uint64 (n, true) -> "uint64_t<" ^ string_of_int n ^ ", dec>" - | CT_uint64 (n, false) -> "uint64_t<" ^ string_of_int n ^ ", int>" + | CT_bv true -> "bv_t(dec)" + | CT_bv false -> "bv_t(inc)" + | CT_uint64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)" + | CT_uint64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)" | CT_int64 -> "int64_t" | CT_bit -> "bit" | CT_unit -> "unit" @@ -756,9 +756,9 @@ let rec string_of_ctyp = function | CT_tup ctyps -> "(" ^ Util.string_of_list ", " string_of_ctyp ctyps ^ ")" | CT_struct (id, _) | CT_enum (id, _) | CT_variant (id, _) -> string_of_id id | CT_string -> "string" - | CT_vector (true, ctyp) -> "vector<dec, " ^ string_of_ctyp ctyp ^ ">" - | CT_vector (false, ctyp) -> "vector<inc, " ^ string_of_ctyp ctyp ^ ">" - | CT_list ctyp -> "list<" ^ string_of_ctyp ctyp ^ ">" + | CT_vector (true, ctyp) -> "vector(dec, " ^ string_of_ctyp ctyp ^ ")" + | CT_vector (false, ctyp) -> "vector(inc, " ^ string_of_ctyp ctyp ^ ")" + | CT_list ctyp -> "list(" ^ string_of_ctyp ctyp ^ ")" (** Convert a sail type into a C-type **) let rec ctyp_of_typ ctx typ = @@ -1129,7 +1129,7 @@ let rec pp_clexp = function let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = match instr with | I_decl (ctyp, id) -> - pp_id id ^^ string " : " ^^ pp_ctyp ctyp + pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp | I_if (cval, then_instrs, else_instrs, ctyp) -> let pp_if_block = function | [] -> string "{}" @@ -1161,13 +1161,12 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args); string ":"; pp_ctyp ctyp2 ] | I_convert (x, ctyp1, y, ctyp2) -> - separate space [ pp_clexp x; string "="; - pp_keyword "convert" ^^ pp_ctyp ctyp2 ^^ parens (pp_id y); - string ":"; pp_ctyp ctyp1 ] + separate space [ pp_clexp x; colon; pp_ctyp ctyp1; string "="; + pp_keyword "convert" ^^ pp_id y; colon; pp_ctyp ctyp2 ] | I_copy (clexp, cval) -> separate space [pp_clexp clexp; string "="; pp_cval cval] | I_clear (ctyp, id) -> - pp_keyword "kill" ^^ parens (pp_ctyp ctyp) ^^ pp_id id + pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp | I_return cval -> pp_keyword "return" ^^ pp_cval cval | I_throw cval -> @@ -1191,12 +1190,13 @@ let pp_ctype_def = function pp_keyword "struct" ^^ pp_id id ^^ string " = " ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) fields) rbrace | CTD_variant (id, ctors) -> - pp_keyword "variant" ^^ pp_id id ^^ string " = " + pp_keyword "union" ^^ pp_id id ^^ string " = " ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) ctors) rbrace let pp_cdef = function | CDEF_spec (id, ctyps, ctyp) -> - pp_keyword "val" ^^ pp_id id ^^ space ^^ parens (separate_map (comma ^^ space) pp_ctyp ctyps) ^^ string " -> " ^^ pp_ctyp ctyp + pp_keyword "val" ^^ pp_id id ^^ string " : " ^^ parens (separate_map (comma ^^ space) pp_ctyp ctyps) ^^ string " -> " ^^ pp_ctyp ctyp + ^^ hardline | CDEF_fundef (id, ret, args, instrs) -> let ret = match ret with | None -> empty @@ -2379,10 +2379,9 @@ let hoist_ctyp = function | _ -> false let hoist_counter = ref 0 - let hoist_id () = - let id = mk_id ("gh#" ^ string_of_int !gensym_counter) in - incr gensym_counter; + let id = mk_id ("gh#" ^ string_of_int !hoist_counter) in + incr hoist_counter; id let hoist_allocations ctx = function @@ -2441,6 +2440,48 @@ let hoist_allocations ctx = function | cdef -> [cdef] +let flat_counter = ref 0 +let flat_id () = + let id = mk_id ("local#" ^ string_of_int !flat_counter) in + incr flat_counter; + id + +let flatten_instrs ctx = + let rec flatten = function + | I_aux (I_decl (ctyp, decl_id), aux) :: instrs -> + let fid = flat_id () in + I_aux (I_decl (ctyp, fid), aux) :: flatten (instrs_rename decl_id fid instrs) + + | I_aux ((I_block block | I_try_block block), _) :: instrs -> + flatten block @ flatten instrs + + | I_aux (I_if (cval, then_instrs, else_instrs, _), _) :: instrs -> + let then_label = label "then_" in + let endif_label = label "endif_" in + [ijump cval then_label] + @ flatten else_instrs + @ [igoto endif_label] + @ [ilabel then_label] + @ flatten then_instrs + @ [ilabel endif_label] + @ flatten instrs + + | I_aux (I_comment _, _) :: instrs -> flatten instrs + + | instr :: instrs -> instr :: flatten instrs + | [] -> [] + in + function + | CDEF_fundef (function_id, heap_return, args, body) -> + flat_counter := 0; + [CDEF_fundef (function_id, heap_return, args, flatten body)] + + | CDEF_let (n, bindings, instrs, cleanup) -> + flat_counter := 0; + [CDEF_let (n, bindings, flatten instrs, flatten cleanup)] + + | cdef -> [cdef] + let concatMap f xs = List.concat (List.map f xs) let optimize ctx cdefs = @@ -3150,6 +3191,14 @@ let sgen_finish = function Printf.sprintf " finish_%s();" (sgen_id id) | _ -> assert false +let bytecode_ast ctx rewrites (Defs defs) = + 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 + let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in + let cdefs = List.concat (List.rev chunks) in + rewrites cdefs + let compile_ast ctx (Defs defs) = try let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in diff --git a/src/isail.ml b/src/isail.ml index ce17561d..94ee6b56 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -263,7 +263,18 @@ let handle_input' input = interactive_ast := ast; interactive_env := env; interactive_state := initial_state !interactive_ast - + | ":bytecode" -> + let open PPrint in + let open C_backend in + let ast = Process_file.rewrite_ast_c !interactive_ast in + let ast, env = Specialize.specialize ast !interactive_env in + let ctx = initial_ctx env in + let byte_ast = bytecode_ast ctx (fun cdefs -> List.concat (List.map (flatten_instrs ctx) cdefs)) ast in + let chan = open_out arg in + Util.opt_colors := false; + Pretty_print_sail.pretty_sail chan (separate_map hardline pp_cdef byte_ast); + Util.opt_colors := true; + close_out chan | ":ast" -> let chan = open_out arg in Pretty_print_sail.pp_defs chan !interactive_ast; |