diff options
Diffstat (limited to 'src/specialize.ml')
| -rw-r--r-- | src/specialize.ml | 57 |
1 files changed, 34 insertions, 23 deletions
diff --git a/src/specialize.ml b/src/specialize.ml index afce4b0f..e2b0075d 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -53,7 +53,7 @@ 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 @@ -62,7 +62,7 @@ let is_typ_ord_arg = function type specialization = { is_polymorphic : kinded_id -> bool; instantiation_filter : kid -> typ_arg -> bool; - extern_filter : (string -> string option) -> bool + extern_filter : (string * string) list -> bool } let typ_ord_specialization = { @@ -73,13 +73,13 @@ let typ_ord_specialization = { let int_specialization = { is_polymorphic = is_int_kopt; - 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) + instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp (Nexp_aux (Nexp_constant _, _)), _) -> true | _ -> false); + extern_filter = (fun externs -> match Ast_util.extern_assoc "c" externs 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); + instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp (Nexp_aux (Nexp_constant _, _)), _) -> true | _ -> false); extern_filter = (fun _ -> false) } @@ -186,7 +186,9 @@ let string_of_instantiation instantiation = | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_gt (n1, n2), _) -> string_of_nexp n1 ^ " > " ^ string_of_nexp n2 | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2 + | NC_aux (NC_bounded_lt (n1, n2), _) -> string_of_nexp n1 ^ " < " ^ string_of_nexp n2 | NC_aux (NC_or (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_and (nc1, nc2), _) -> @@ -391,7 +393,7 @@ let specialize_id_valspec spec instantiations id ast = let kopts, constraints = quant_split typq in let constraints = instantiate_constraints safe_instantiation constraints in let constraints = instantiate_constraints reverse constraints in - let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in + let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt && KBindings.mem (kopt_kid kopt) safe_instantiation)) kopts in let typq = if List.length (typ_frees @ int_frees) = 0 && List.length kopts = 0 then mk_typquant [] @@ -483,18 +485,21 @@ let specialize_id_overloads instantiations id (Defs defs) = valspecs are then re-specialized. This process is iterated until the whole spec is specialized. *) -let initial_calls = IdSet.of_list +let initial_calls = ref (IdSet.of_list [ mk_id "main"; mk_id "__SetConfig"; mk_id "__ListConfig"; mk_id "execute"; mk_id "decode"; mk_id "initialize_registers"; + mk_id "prop"; mk_id "append_64" (* used to construct bitvector literals in C backend *) - ] + ]) + +let add_initial_calls ids = initial_calls := IdSet.union ids !initial_calls -let remove_unused_valspecs ?(initial_calls=initial_calls) env ast = - let calls = ref initial_calls in +let remove_unused_valspecs env ast = + let calls = ref !initial_calls in let vs_ids = val_spec_ids ast in let inspect_exp = function @@ -527,14 +532,6 @@ let remove_unused_valspecs ?(initial_calls=initial_calls) env ast = List.fold_left (fun ast id -> Defs (remove_unused ast id)) ast (IdSet.elements unused) -let slice_defs env (Defs defs) keep_ids = - let keep = function - | DEF_fundef fd -> IdSet.mem (id_of_fundef fd) keep_ids - | _ -> true - in - let defs = List.filter keep defs in - remove_unused_valspecs env (Defs defs) ~initial_calls:keep_ids - let specialize_id spec id ast = let instantiations = instantiations_of spec id ast in let ast = specialize_id_valspec spec instantiations id ast in @@ -560,6 +557,7 @@ let reorder_typedefs (Defs defs) = Defs (List.rev !tdefs @ others) let specialize_ids spec ids ast = + let t = Profile.start () in let total = IdSet.cardinal ids in let _, ast = List.fold_left @@ -578,14 +576,19 @@ let specialize_ids spec ids ast = | 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) + let _, ast = + List.fold_left + (fun (n, ast) id -> + Util.progress "Rewriting " (string_of_id id) n total; + (n + 1, rewrite_polymorphic_calls spec id ast)) + (1, ast) (IdSet.elements ids) in let ast, env = Type_error.check Type_check.initial_env ast in let ast = remove_unused_valspecs env ast in + Profile.finish "specialization pass" t; ast, env -let rec specialize' n spec ast env = +let rec specialize_passes n spec env ast = if n = 0 then ast, env else @@ -594,6 +597,14 @@ let rec specialize' n spec ast env = ast, env else let ast, env = specialize_ids spec ids ast in - specialize' (n - 1) spec ast env + specialize_passes (n - 1) spec env ast + +let specialize = specialize_passes (-1) -let specialize = specialize' (-1) +let () = + let open Interactive in + Action (fun () -> + let ast', env' = specialize typ_ord_specialization !env !ast in + ast := ast'; + env := env' + ) |> register_command ~name:"specialize" ~help:"Specialize Type and Order type variables in the AST" |