diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/c_backend.ml | 35 | ||||
| -rw-r--r-- | src/isail.ml | 9 | ||||
| -rw-r--r-- | src/sail.ml | 1 | ||||
| -rw-r--r-- | src/specialize.ml | 39 | ||||
| -rw-r--r-- | src/specialize.mli | 5 |
5 files changed, 56 insertions, 33 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index aff2d49e..47e84446 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -90,8 +90,8 @@ let zencode_id = function (* 2. Converting sail types to C types *) (**************************************************************************) -let max_int64 = Big_int.of_int64 Int64.max_int -let min_int64 = Big_int.of_int64 Int64.min_int +let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) +let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) (** The context type contains two type-checking environments. ctx.local_env contains the closest typechecking @@ -111,6 +111,7 @@ type ctx = recursive_functions : IdSet.t; no_raw : bool; optimize_smt : bool; + iterate_size : bool; } let initial_ctx env = @@ -124,8 +125,17 @@ let initial_ctx env = recursive_functions = IdSet.empty; no_raw = false; optimize_smt = true; + iterate_size = false; } +let rec iterate_size ctx size n m = + if size > 64 then + CT_lint + else if prove __POS__ ctx.local_env (nc_and (nc_lteq (nconstant (min_int size)) n) (nc_lteq m (nconstant (max_int size)))) then + CT_fint size + else + iterate_size ctx (size + 1) n m + (** Convert a sail type into a C-type. This function can be quite slow, because it uses ctx.local_env and SMT to analyse the Sail types and attempts to fit them into the smallest possible C @@ -151,10 +161,15 @@ let rec ctyp_of_typ ctx typ = | Some (kids, constr, n, m) -> match nexp_simp n, nexp_simp m with | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) - when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 -> - CT_fint 64 + when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> + if ctx.iterate_size then + iterate_size ctx 2 (nconstant n) (nconstant m) + else + CT_fint 64 | n, m when ctx.optimize_smt -> - if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then + if ctx.iterate_size then + iterate_size ctx 2 n m + else if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then CT_fint 64 else CT_lint @@ -264,7 +279,7 @@ let hex_char = let literal_to_fragment (L_aux (l_aux, _) as lit) = match l_aux with - | L_num n when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> + | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> Some (F_lit (V_int n), CT_fint 64) | L_hex str when String.length str <= 16 -> let padding = 16 - String.length str in @@ -544,9 +559,9 @@ let analyze_primop' ctx id args typ = | Some (kids, constr, n, m) -> match nexp_simp n, nexp_simp m with | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) - when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 -> + when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64)) - | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) -> + | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) -> AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64)) | _ -> no_change end @@ -717,7 +732,7 @@ let rec chunkify n xs = let rec compile_aval l ctx = function | AV_C_fragment (frag, typ, ctyp) -> let ctyp' = ctyp_of_typ ctx typ in - if not (ctyp_equal ctyp ctyp') then + if not (ctyp_equal ctyp ctyp' || ctx.iterate_size) then raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp')); [], (frag, ctyp_of_typ ctx typ), [] @@ -737,7 +752,7 @@ let rec compile_aval l ctx = function | AV_lit (L_aux (L_string str, _), typ) -> [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), [] - | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> + | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> let gs = gensym () in [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)], (F_id gs, CT_lint), diff --git a/src/isail.ml b/src/isail.ml index 35350291..4c7cf8d6 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -356,15 +356,6 @@ let handle_input' input = ":(c)ommand can be called as either :c or :command." ] in List.iter print_endline commands - | ":poly" -> - let is_kopt = match arg with - | "Int" -> is_int_kopt - | "Type" -> is_typ_kopt - | "Order" -> is_order_kopt - | _ -> failwith "Invalid kind" - in - let ids = Specialize.polymorphic_functions is_kopt !Interactive.ast in - List.iter (fun id -> print_endline (string_of_id id)) (IdSet.elements ids) | ":option" -> begin try diff --git a/src/sail.ml b/src/sail.ml index bd953992..344152a2 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -408,7 +408,6 @@ let main() = 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 ast_c type_envs) in *) - (* let ast_c = Spec_analysis.top_sort_defs ast_c in *) Util.opt_warnings := true; C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c else ()); diff --git a/src/specialize.ml b/src/specialize.ml index 591a415a..19c5df7a 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -59,17 +59,26 @@ let is_typ_ord_arg = function type specialization = { is_polymorphic : kinded_id -> bool; - instantiation_filter : kid -> typ_arg -> bool + instantiation_filter : kid -> typ_arg -> bool; + extern_filter : (string -> string option) -> bool } let typ_ord_specialization = { is_polymorphic = (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt); - instantiation_filter = (fun _ -> is_typ_ord_arg) + instantiation_filter = (fun _ -> is_typ_ord_arg); + extern_filter = (fun _ -> false) } let int_specialization = { is_polymorphic = is_int_kopt; - instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false) + instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false); + extern_filter = (fun externs -> match externs "c" with Some _ -> true | None -> false) + } + +let int_specialization_with_externs = { + is_polymorphic = is_int_kopt; + instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false); + extern_filter = (fun _ -> false) } let rec nexp_simp_typ (Typ_aux (typ_aux, l)) = @@ -105,15 +114,15 @@ let fix_instantiation spec instantiation = for some set of kinded-identifiers, specified by the is_kopt predicate. For example, polymorphic_functions is_int_kopt will return all Int-polymorphic functions. *) -let rec polymorphic_functions is_kopt (Defs defs) = +let rec polymorphic_functions ctx (Defs defs) = match defs with - | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, _, externs), _)) :: defs -> - let is_polymorphic = List.exists is_kopt (quant_kopts typq) in - if is_polymorphic then - IdSet.add id (polymorphic_functions is_kopt (Defs defs)) + | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, externs, _), _)) :: defs -> + let is_polymorphic = List.exists ctx.is_polymorphic (quant_kopts typq) in + if is_polymorphic && not (ctx.extern_filter externs) then + IdSet.add id (polymorphic_functions ctx (Defs defs)) else - polymorphic_functions is_kopt (Defs defs) - | _ :: defs -> polymorphic_functions is_kopt (Defs defs) + polymorphic_functions ctx (Defs defs) + | _ :: defs -> polymorphic_functions ctx (Defs defs) | [] -> IdSet.empty (* When we specialize a function, we need to generate new name. To do @@ -548,7 +557,13 @@ let reorder_typedefs (Defs defs) = Defs (List.rev !tdefs @ others) let specialize_ids spec ids ast = - let ast = List.fold_left (fun ast id -> specialize_id spec id ast) ast (IdSet.elements ids) in + let total = IdSet.cardinal ids in + let _, ast = + List.fold_left + (fun (n, ast) id -> + Util.progress "Specializing " (string_of_id id) n total; (n + 1, specialize_id spec id ast)) + (1, ast) (IdSet.elements ids) + in let ast = reorder_typedefs ast in let ast, _ = Type_error.check Type_check.initial_env ast in let ast = @@ -562,7 +577,7 @@ let rec specialize' n spec ast env = if n = 0 then ast, env else - let ids = polymorphic_functions spec.is_polymorphic ast in + let ids = polymorphic_functions spec ast in if IdSet.is_empty ids then ast, env else diff --git a/src/specialize.mli b/src/specialize.mli index 93dec239..b6299558 100644 --- a/src/specialize.mli +++ b/src/specialize.mli @@ -62,12 +62,15 @@ val typ_ord_specialization : specialization (** (experimental) specialise Int-kinded definitions *) val int_specialization : specialization +(** (experimental) specialise Int-kinded definitions, including externs *) +val int_specialization_with_externs : specialization + (** Returns an IdSet with the function ids that have X-kinded parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first argument specifies what X should be - it should be one of: [is_int_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util], or some combination of those. *) -val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t +val polymorphic_functions : specialization -> 'a defs -> IdSet.t (** specialize returns an AST with all the Order and Type polymorphism removed, as well as the environment produced by type checking that |