diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/c_backend.ml | 47 | ||||
| -rw-r--r-- | src/sail.ml | 11 | ||||
| -rw-r--r-- | src/specialize.ml | 11 |
3 files changed, 68 insertions, 1 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index ab388223..d14b5391 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -174,6 +174,7 @@ let rec ctyp_of_typ ctx typ = begin match destruct_range Env.empty typ with | None -> assert false (* Checked if range type in guard *) | Some (kids, constr, n, m) -> + let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env } in match nexp_simp n, nexp_simp m with | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> @@ -483,6 +484,38 @@ let analyze_primop' ctx id args typ = | _ -> no_change end + | "zero_extend", [AV_C_fragment (v1, _, CT_fbits _); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (v1, typ, CT_fbits (Big_int.to_int n, true))) + | _ -> no_change + end + + | "zero_extend", [AV_C_fragment (v1, _, CT_sbits _); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_call ("fast_zero_extend", [v1; v_int (Big_int.to_int n)]), typ, CT_fbits (Big_int.to_int n, true))) + | _ -> no_change + end + + | "sign_extend", [AV_C_fragment (v1, _, CT_fbits (n, _)); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant m, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal m (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_call ("fast_sign_extend", [v1; v_int n; v_int (Big_int.to_int m)]) , typ, CT_fbits (Big_int.to_int m, true))) + | _ -> no_change + end + + | "sign_extend", [AV_C_fragment (v1, _, CT_sbits _); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant m, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal m (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_call ("fast_sign_extend2", [v1; v_int (Big_int.to_int m)]) , typ, CT_fbits (Big_int.to_int m, true))) + | _ -> no_change + end + | "gteq", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> AE_val (AV_C_fragment (F_op (v1, ">=", v2), typ, CT_bool)) @@ -568,6 +601,14 @@ let analyze_primop' ctx id args typ = | _ -> no_change end + | "sail_signed", [AV_C_fragment (frag, vtyp, _)] -> + begin match destruct_vector ctx.tc_env vtyp with + | Some (Nexp_aux (Nexp_constant n, _), _, _) + when Big_int.less_equal n (Big_int.of_int 64) && is_stack_typ ctx typ -> + AE_val (AV_C_fragment (F_call ("fast_signed", [frag; v_int (Big_int.to_int n)]), typ, ctyp_of_typ ctx typ)) + | _ -> no_change + end + | "add_int", [AV_C_fragment (op1, _, _); AV_C_fragment (op2, _, _)] -> begin match destruct_range Env.empty typ with | None -> no_change @@ -592,6 +633,12 @@ let analyze_primop' ctx id args typ = | _ -> no_change end + | "vector_update_subrange", [AV_C_fragment (xs, _, CT_fbits (n, true)); + AV_C_fragment (hi, _, CT_fint 64); + AV_C_fragment (lo, _, CT_fint 64); + AV_C_fragment (ys, _, CT_fbits (m, true))] -> + AE_val (AV_C_fragment (F_call ("fast_update_subrange", [xs; hi; lo; ys]), typ, CT_fbits (n, true))) + | "undefined_bool", _ -> AE_val (AV_C_fragment (F_lit (V_bool false), typ, CT_bool)) diff --git a/src/sail.ml b/src/sail.ml index 2a15f26e..eb81a0ee 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -67,6 +67,7 @@ let opt_print_cgen = ref false let opt_memo_z3 = ref false let opt_sanity = ref false let opt_includes_c = ref ([]:string list) +let opt_specialize_c = ref false let opt_libs_lem = ref ([]:string list) let opt_libs_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) @@ -151,6 +152,9 @@ let options = Arg.align ([ ( "-c_extra_args", Arg.String (fun args -> C_backend.opt_extra_arguments := Some args), "<arguments> supply extra argument to every generated C function call" ); + ( "-c_specialize", + Arg.Set opt_specialize_c, + " specialize integer arguments in C output"); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an ELF file so that it can be executed by compiled C code"); @@ -422,7 +426,12 @@ let main() = then let ast_c = rewrite_ast_c type_envs ast in let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in - (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *) + let ast_c, type_envs = + if !opt_specialize_c then + Specialize.(specialize' 2 int_specialization ast_c type_envs) + else + ast_c, type_envs + in let output_chan = match !opt_file_out with Some f -> open_out (f ^ ".c") | None -> stdout in Util.opt_warnings := true; C_backend.compile_ast (C_backend.initial_ctx type_envs) output_chan (!opt_includes_c) ast_c; diff --git a/src/specialize.ml b/src/specialize.ml index 19c5df7a..a487fc2f 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -52,6 +52,8 @@ open Ast open Ast_util open Rewriter +let opt_ddump_spec_ast = ref None + let is_typ_ord_arg = function | A_aux (A_typ _, _) -> true | A_aux (A_order _, _) -> true @@ -565,6 +567,15 @@ let specialize_ids spec ids ast = (1, ast) (IdSet.elements ids) in let ast = reorder_typedefs ast in + begin match !opt_ddump_spec_ast with + | Some (f, i) -> + let filename = f ^ "_spec_" ^ string_of_int i ^ ".sail" in + let out_chan = open_out filename in + Pretty_print_sail.pp_defs out_chan ast; + close_out out_chan; + opt_ddump_spec_ast := Some (f, i + 1) + | None -> () + end; let ast, _ = Type_error.check Type_check.initial_env ast in let ast = List.fold_left (fun ast id -> rewrite_polymorphic_calls spec id ast) ast (IdSet.elements ids) |