From baed6162b5f823a44fd1045c18714d4973d151e9 Mon Sep 17 00:00:00 2001 From: Jon French Date: Mon, 25 Feb 2019 13:12:24 +0000 Subject: OCaml backend: omit function definitions for externs --- src/ocaml_backend.ml | 124 +++++++++++++++++++++++++++------------------------ 1 file changed, 65 insertions(+), 59 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 894d028f..a5f0653b 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -456,70 +456,76 @@ let ocaml_funcls ctx = function | [] -> failwith "Ocaml: empty function" | [FCL_aux (FCL_Funcl (id, pexp),_)] -> - let arg_typs, ret_typ = - match Bindings.find id ctx.val_specs with - | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ) - | _ -> failwith "Found val spec which was not a function!" - in - (* Any remaining type variables after simple_typ rewrite should - indicate Type-polymorphism. If we have it, we need to generate - explicit type signatures with universal quantification. *) - let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in - let pat_sym = gensym () in - let pat, exp = - match pexp with - | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp - | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported" - in - let annot_pat = - let pat = + if Bindings.mem id ctx.externs + then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline + else + let arg_typs, ret_typ = + match Bindings.find id ctx.val_specs with + | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ) + | _ -> failwith "Found val spec which was not a function!" + in + (* Any remaining type variables after simple_typ rewrite should + ind icate Type-polymorphism. If we have it, we need to generate + explic it type signatures with universal quantification. *) + let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in + let pat_sym = gensym () in + let pat, exp = + match pexp with + | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp + | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported" + in + let annot_pat = + let pat = + if KidSet.is_empty kids then + parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))) + else + ocaml_pat ctx pat + in + if !opt_trace_ocaml + then parens (separate space [pat; string "as"; pat_sym]) + else pat + in + let call_header = function_header () in + let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in + let call = if KidSet.is_empty kids then - parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))) + separate space [call_header; zencode ctx id; + annot_pat; colon; ocaml_typ ctx ret_typ; equals; + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] + ^//^ ocaml_exp ctx exp + ^^ rparen else - ocaml_pat ctx pat + separate space [call_header; zencode ctx id; colon; + separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot; + ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals; + string "fun"; annot_pat; string "->"; + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] + ^//^ ocaml_exp ctx exp + ^^ rparen in - if !opt_trace_ocaml - then parens (separate space [pat; string "as"; pat_sym]) - else pat - in - let call_header = function_header () in - let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in - let call = - if KidSet.is_empty kids then - separate space [call_header; zencode ctx id; - annot_pat; colon; ocaml_typ ctx ret_typ; equals; - sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] - ^//^ ocaml_exp ctx exp - ^^ rparen - else - separate space [call_header; zencode ctx id; colon; - separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot; - ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals; - string "fun"; annot_pat; string "->"; - sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] - ^//^ ocaml_exp ctx exp - ^^ rparen - in - ocaml_funcl call string_of_arg string_of_ret + ocaml_funcl call string_of_arg string_of_ret | funcls -> let id = funcls_id funcls in - let arg_typs, ret_typ = - match Bindings.find id ctx.val_specs with - | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ) - | _ -> failwith "Found val spec which was not a function!" - in - let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in - if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else (); - let pat_sym = gensym () in - let call_header = function_header () in - let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in - let call = - separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals; - sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] - ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls) - ^^ rparen - in - ocaml_funcl call string_of_arg string_of_ret + if Bindings.mem id ctx.externs + then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline + else + let arg_typs, ret_typ = + match Bindings.find id ctx.val_specs with + | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ) + | _ -> failwith "Found val spec which was not a function!" + in + let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in + if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else (); + let pat_sym = gensym () in + let call_header = function_header () in + let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in + let call = + separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals; + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] + ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls) + ^^ rparen + in + ocaml_funcl call string_of_arg string_of_ret let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) = ocaml_funcls ctx funcls -- cgit v1.2.3 From 7fc5222ef8daa887eab8a7d178a459c0c84d45f6 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 25 Feb 2019 14:53:57 +0000 Subject: Fix some builtins, and make mod_int return natural --- src/value.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src') diff --git a/src/value.ml b/src/value.ml index 729b3974..8f8e651a 100644 --- a/src/value.ml +++ b/src/value.ml @@ -331,6 +331,10 @@ let value_modulus = function | [v1; v2] -> V_int (Sail_lib.modulus (coerce_int v1, coerce_int v2)) | _ -> failwith "value modulus" +let value_abs_int = function + | [v] -> V_int (Big_int.abs (coerce_int v)) + | _ -> failwith "value abs_int" + let value_add_vec_int = function | [v1; v2] -> mk_vector (Sail_lib.add_vec_int (coerce_bv v1, coerce_int v2)) | _ -> failwith "value add_vec_int" @@ -630,6 +634,7 @@ let primops = ("shl_int", value_shl_int); ("max_int", value_max_int); ("min_int", value_min_int); + ("abs_int", value_abs_int); ("add_vec_int", value_add_vec_int); ("sub_vec_int", value_sub_vec_int); ("add_vec", value_add_vec); -- cgit v1.2.3 From 24223bee0e379a18db010c8b50b1b52110876caf Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 25 Feb 2019 17:20:52 +0000 Subject: Allow int-specialization for non-externs only Add a flag in C backend ctx that allows us to generate arbitrary precision signed integer types, rather than just int64 --- src/c_backend.ml | 35 +++++++++++++++++++++++++---------- src/isail.ml | 9 --------- src/sail.ml | 1 - src/specialize.ml | 39 +++++++++++++++++++++++++++------------ src/specialize.mli | 5 ++++- 5 files changed, 56 insertions(+), 33 deletions(-) (limited to 'src') 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 -- cgit v1.2.3 From 8985e0ffc1b23ef5039383d99bdf46da10a131c1 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 25 Feb 2019 18:37:39 +0000 Subject: Monomorphisation: fix check for effects in constant propagation The old check used the wrong part of the AST. It would stop when it reached the actual effect, anyway, but this should improve performance. --- src/monomorphise.ml | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 92a0ae01..784929e1 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -199,10 +199,9 @@ let rec is_value (E_aux (e,(l,annot))) = (* TODO: more? *) | _ -> false -let is_pure (Effect_opt_aux (e,_)) = +let is_pure e = match e with - | Effect_opt_none -> true - | Effect_opt_effect (Effect_aux (Effect_set [],_)) -> true + | Effect_aux (Effect_set [],_) -> true | _ -> false let rec list_extract f = function @@ -1507,14 +1506,19 @@ let split_defs all_errors splits defs = if not (List.for_all is_value args) then None else + let (tq,typ) = Env.get_val_spec_orig id env in + let eff = match typ with + | Typ_aux (Typ_fn (_,_,eff),_) -> Some eff + | _ -> None + in let Defs ds = defs in - match list_extract (function + match eff, list_extract (function | (DEF_fundef (FD_aux (FD_function (_,_,eff,((FCL_aux (FCL_Funcl (id',_),_))::_ as fcls)),_))) - -> if Id.compare id id' = 0 then Some (eff,fcls) else None + -> if Id.compare id id' = 0 then Some fcls else None | _ -> None) ds with - | None -> None - | Some (eff,_) when not (is_pure eff) -> None - | Some (_,fcls) -> + | None,_ | _,None -> None + | Some eff,_ when not (is_pure eff) -> None + | Some _,Some fcls -> let arg = match args with | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,empty_tannot)) | [e] -> e -- cgit v1.2.3 From 87140e97e3c1b2b1713a4458f8f5e622625c0683 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 26 Feb 2019 17:25:55 +0000 Subject: Make -o option work as usual with C compilation --- src/c_backend.ml | 6 +++--- src/c_backend.mli | 2 +- src/sail.ml | 8 +++++--- src/specialize.mli | 2 ++ 4 files changed, 11 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index 47e84446..05b09b65 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -3499,7 +3499,7 @@ let smt_trace ctx = | cdef -> cdef -let compile_ast ctx c_includes (Defs defs) = +let compile_ast ctx output_chan c_includes (Defs defs) = try c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Identifying recursive functions")); let recursive_functions = Spec_analysis.top_sort_defs (Defs defs) |> get_recursive_functions in @@ -3622,7 +3622,7 @@ let compile_ast ctx c_includes (Defs defs) = ^^ model_init ^^ hlhl ^^ model_fini ^^ hlhl ^^ model_default_main ^^ hlhl - ^^ model_main) - |> print_endline + ^^ model_main ^^ hardline) + |> output_string output_chan with Type_error (_, l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err) diff --git a/src/c_backend.mli b/src/c_backend.mli index 10bf9f40..a11ac7f5 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -89,7 +89,7 @@ val initial_ctx : Env.t -> ctx val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list -val compile_ast : ctx -> string list -> tannot Ast.defs -> unit +val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit val bytecode_ast : ctx -> (cdef list -> cdef list) -> tannot Ast.defs -> cdef list diff --git a/src/sail.ml b/src/sail.ml index 344152a2..49abd3bd 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -407,9 +407,11 @@ 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 ast_c type_envs) in *) + (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs 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) (!opt_includes_c) ast_c + C_backend.compile_ast (C_backend.initial_ctx type_envs) output_chan (!opt_includes_c) ast_c; + close_out output_chan else ()); (if !(opt_print_cgen) then Cgen_backend.output type_envs ast @@ -435,7 +437,7 @@ let main() = begin try if not (Sys.is_directory latex_dir) then begin - prerr_endline ("Failure: latex output directory exists but is not a directory: " ^ latex_dir); + prerr_endline ("Failure: latex output location exists and is not a directory: " ^ latex_dir); exit 1 end with Sys_error(_) -> Unix.mkdir latex_dir 0o755 diff --git a/src/specialize.mli b/src/specialize.mli index b6299558..6ec8c2aa 100644 --- a/src/specialize.mli +++ b/src/specialize.mli @@ -79,6 +79,8 @@ val polymorphic_functions : specialization -> 'a defs -> IdSet.t which case specialize returns the AST unmodified. *) val specialize : specialization -> tannot defs -> Env.t -> tannot defs * Env.t +(** specialize' n performs at most n specialization passes. Useful for + int_specialization which is not guaranteed to terminate. *) val specialize' : int -> specialization -> tannot defs -> Env.t -> tannot defs * Env.t (** return all instantiations of a function id, with the -- cgit v1.2.3 From b118c78ba85320ef2d6632bc2a6ee4f0907e5d23 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 27 Feb 2019 19:24:05 +0000 Subject: Tweaks to C compilation to make it more usable for embedding into other programs Can now set a prefix for generated C functions with -c_prefix so -c_prefix sail_ would give sail_execute_CGetPerm over zexecute_CGetPerm. We still have to use our standard name-mangling scheme to avoid possible collisions within the name. Can build C that doesn't expect the standard runtime, which leaves operations like read_memory, write_memory etc to be stubbed in by another C program including the generated Sail. Things like letbindings are still an issue because we rely on a very small runtime to initialize global letbindings and similar. -c_separate_execute splits the execute function apart in the generated C --- src/c_backend.ml | 53 +++++++++++++++++++++++++++++++++-------------------- src/c_backend.mli | 2 ++ src/rewrites.ml | 6 ++++++ src/rewrites.mli | 1 + src/sail.ml | 11 ++++++++++- 5 files changed, 52 insertions(+), 21 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index 05b09b65..a656a097 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -61,6 +61,7 @@ open Anf module Big_int = Nat_big_num let c_verbosity = ref 0 + let opt_debug_flow_graphs = ref false let opt_debug_function = ref "" let opt_trace = ref false @@ -68,6 +69,8 @@ let opt_smt_trace = ref false let opt_static = ref false let opt_no_main = ref false let opt_memo_cache = ref false +let opt_no_rts = ref false +let opt_prefix = ref "z" (* Optimization flags *) let optimize_primops = ref false @@ -956,8 +959,7 @@ let compile_funcall l ctx id args typ = ifuncall clexp id setup_args else let gs = gensym () in - iblock [icomment "copy call"; - idecl ret_ctyp gs; + iblock [idecl ret_ctyp gs; ifuncall (CL_id (gs, ret_ctyp)) id setup_args; icopy l clexp (F_id gs, ret_ctyp); iclear ret_ctyp gs] @@ -2420,7 +2422,8 @@ let optimize ctx cdefs = |> (if !optimize_alias then concatMap unique_names else nothing) |> (if !optimize_alias then concatMap (remove_alias ctx) else nothing) |> (if !optimize_alias then concatMap (combine_variables ctx) else nothing) - |> (if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing) + (* We need the runtime to initialize hoisted allocations *) + |> (if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations ctx) else nothing) |> (if !optimize_hoist_allocations && !optimize_experimental then concatMap (hoist_alias ctx) else nothing) (**************************************************************************) @@ -2430,6 +2433,12 @@ let optimize ctx cdefs = let sgen_id id = Util.zencode_string (string_of_id id) let codegen_id id = string (sgen_id id) +let sgen_function_id id = + let str = Util.zencode_string (string_of_id id) in + !opt_prefix ^ String.sub str 1 (String.length str - 1) + +let codegen_function_id id = string (sgen_function_id id) + let rec sgen_ctyp = function | CT_unit -> "unit" | CT_bit -> "fbits" @@ -2585,7 +2594,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = else if extern then string_of_id f else - sgen_id f + sgen_function_id f in let fname = match fname, ctyp with @@ -2858,7 +2867,7 @@ let codegen_type_def ctx = function in Printf.sprintf "%s op" (sgen_ctyp ctyp), empty, empty in - string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_id ctor_id) (sgen_id id) ctor_args) ^^ hardline + string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_function_id ctor_id) (sgen_id id) ctor_args) ^^ hardline ^^ surround 2 0 lbrace (tuple ^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline @@ -3009,7 +3018,7 @@ let codegen_list_set id ctyp = let codegen_cons id ctyp = let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in - string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) + string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) ^^ string (Printf.sprintf " *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id)) ^^ (if is_stack_ctyp ctyp then string " (*rop)->hd = x;\n" @@ -3174,9 +3183,9 @@ let codegen_def' ctx = function if Env.is_extern id ctx.tc_env "c" then empty else if is_stack_ctyp ret_ctyp then - string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) else - string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_function_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) | CDEF_fundef (id, ret_arg, args, instrs) as def -> if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else (); @@ -3217,11 +3226,11 @@ let codegen_def' ctx = function | None -> assert (is_stack_ctyp ret_ctyp); (if !opt_static then string "static " else empty) - ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline + ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string args) ^^ hardline | Some gs -> assert (not (is_stack_ctyp ret_ctyp)); (if !opt_static then string "static " else empty) - ^^ string "void" ^^ space ^^ codegen_id id + ^^ string "void" ^^ space ^^ codegen_function_id id ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) ^^ hardline in @@ -3235,7 +3244,7 @@ let codegen_def' ctx = function | CDEF_startup (id, instrs) -> let static = if !opt_static then "static " else "" in - let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_id id)) in + let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_function_id id)) in separate_map hardline codegen_decl instrs ^^ twice hardline ^^ startup_header ^^ hardline @@ -3245,7 +3254,7 @@ let codegen_def' ctx = function | CDEF_finish (id, instrs) -> let static = if !opt_static then "static " else "" in - let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_id id)) in + let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_function_id id)) in separate_map hardline codegen_decl (List.filter is_decl instrs) ^^ twice hardline ^^ finish_header ^^ hardline @@ -3536,9 +3545,10 @@ let compile_ast ctx output_chan c_includes (Defs defs) = let docs = List.map (codegen_def ctx) cdefs in let preamble = separate hardline - ([ string "#include \"sail.h\""; - string "#include \"rts.h\""; - string "#include \"elf.h\"" ] + ([ string "#include \"sail.h\"" ] + @ (if !opt_no_rts then [] else + [ string "#include \"rts.h\""; + string "#include \"elf.h\"" ]) @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes)) in @@ -3582,7 +3592,7 @@ let compile_ast ctx output_chan c_includes (Defs defs) = @ fst exn_boilerplate @ startup cdefs @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs) - @ (if regs = [] then [] else [ " zinitializze_registers(UNIT);" ]) + @ (if regs = [] then [] else [ Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "initialize_registers")) ]) @ letbind_initializers @ [ "}" ] )) in @@ -3603,7 +3613,7 @@ let compile_ast ctx output_chan c_includes (Defs defs) = "{"; " model_init();"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; - " zmain(UNIT);"; + Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main")); " model_fini();"; " return EXIT_SUCCESS;"; "}" ] ) @@ -3619,9 +3629,12 @@ let compile_ast ctx output_chan c_includes (Defs defs) = let hlhl = hardline ^^ hardline in Pretty_print_sail.to_string (preamble ^^ hlhl ^^ separate hlhl docs ^^ hlhl - ^^ model_init ^^ hlhl - ^^ model_fini ^^ hlhl - ^^ model_default_main ^^ hlhl + ^^ (if not !opt_no_rts then + model_init ^^ hlhl + ^^ model_fini ^^ hlhl + ^^ model_default_main ^^ hlhl + else + empty) ^^ model_main ^^ hardline) |> output_string output_chan with diff --git a/src/c_backend.mli b/src/c_backend.mli index a11ac7f5..e6cc783c 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -59,6 +59,8 @@ val opt_trace : bool ref val opt_smt_trace : bool ref val opt_static : bool ref val opt_no_main : bool ref +val opt_no_rts : bool ref +val opt_prefix : string ref (** [opt_memo_cache] will store the compiled function definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the diff --git a/src/rewrites.ml b/src/rewrites.ml index f14d423c..d8cb5a5d 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5170,6 +5170,11 @@ let rewrite_defs_ocaml = [ (* ("separate_numbs", rewrite_defs_separate_numbs) *) ] +let opt_separate_execute = ref false + +let if_separate f env defs = + if !opt_separate_execute then f env defs else defs + let rewrite_defs_c = [ ("no_effect_check", (fun _ defs -> opt_no_effects := true; defs)); @@ -5196,6 +5201,7 @@ let rewrite_defs_c = [ ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); + ("split_execute", if_separate (rewrite_split_fun_constr_pats "execute")); ("exp_lift_assign", rewrite_defs_exp_lift_assign); ("merge_function_clauses", merge_funcls); ("recheck_defs", fun _ -> Optimize.recheck) diff --git a/src/rewrites.mli b/src/rewrites.mli index cea227a5..811d52e8 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -59,6 +59,7 @@ val opt_dmono_analysis : int ref val opt_auto_mono : bool ref val opt_dall_split_errors : bool ref val opt_dmono_continue : bool ref +val opt_separate_execute : bool ref (* Generate a fresh id with the given prefix *) val fresh_id : string -> l -> id diff --git a/src/sail.ml b/src/sail.ml index 49abd3bd..0450c0ca 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -123,7 +123,7 @@ let options = Arg.align ([ " pretty print the input to LaTeX"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix := prefix), - " set a custom prefix for generated LaTeX macro command (default sail)"); + " set a custom prefix for generated LaTeX macro command (default sail)"); ( "-latex_full_valspecs", Arg.Clear Latex.opt_simple_val, " print full valspecs in LaTeX output"); @@ -136,6 +136,15 @@ let options = Arg.align ([ ( "-c_no_main", Arg.Set C_backend.opt_no_main, " do not generate the main() function" ); + ( "-c_no_rts", + Arg.Set C_backend.opt_no_rts, + " do not include the Sail runtime" ); + ( "-c_separate_execute", + Arg.Set Rewrites.opt_separate_execute, + " separate execute scattered function into multiple functions"); + ( "-c_prefix", + Arg.String (fun prefix -> C_backend.opt_prefix := prefix), + " prefix generated C functions" ); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an ELF file so that it can be executed by compiled C code"); -- cgit v1.2.3 From 9fd08144367f0b3a08bd5fd3e973ede900a9c72d Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Wed, 27 Feb 2019 19:03:27 -0800 Subject: Provide more access to the ELF symbols in the OCaml ELF-loader. --- src/elf_loader.ml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/elf_loader.ml b/src/elf_loader.ml index 2f63087f..d6016c8b 100644 --- a/src/elf_loader.ml +++ b/src/elf_loader.ml @@ -47,9 +47,10 @@ let opt_elf_threads = ref 1 let opt_elf_entry = ref Big_int.zero let opt_elf_tohost = ref Big_int.zero -(* the type of elf last loaded *) +(* the type of elf last loaded, and its symbol map *) type elf_class = ELF_Class_64 | ELF_Class_32 let opt_elf_class = ref ELF_Class_64 (* default *) +let opt_symbol_map = ref ([] : Elf_file.global_symbol_init_info) type word8 = int @@ -144,6 +145,7 @@ let load_segment ?writer:(writer=write_sail_lib) bs paddr base offset size memsz let load_elf ?writer:(writer=write_sail_lib) name = let segments, e_entry, symbol_map = read name in opt_elf_entry := e_entry; + opt_symbol_map := symbol_map; (if List.mem_assoc "tohost" symbol_map then let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in opt_elf_tohost := tohost_addr); @@ -181,3 +183,12 @@ let elf_entry () = !opt_elf_entry let elf_tohost () = !opt_elf_tohost (* Used to check last loaded elf class. *) let elf_class () = !opt_elf_class +(* Lookup the address for a symbol *) +let elf_symbol symbol = + if List.mem_assoc symbol !opt_symbol_map then + let (_, _, addr, _, _) = List.assoc symbol !opt_symbol_map in + Some addr + else None +(* Get all symbols *) +let elf_symbols () = + !opt_symbol_map -- cgit v1.2.3 From fb362fcb5671b6f008794d0a7db31b1f2685e413 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 28 Feb 2019 16:28:56 +0000 Subject: Allow user-specified state to be passed through generated C For example: sail -c_extra_params "CPUMIPSState *env" -c_extra_args env would pass a QEMU MIPS cpu state to every non-builtin function call. Also add documentation for each C compilation option in C_backend.mli --- src/c_backend.ml | 27 ++++++++++++++++++++------- src/c_backend.mli | 49 +++++++++++++++++++++++++++++++++++++++++++------ src/sail.ml | 6 ++++++ 3 files changed, 69 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index a656a097..ab388223 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -71,6 +71,18 @@ let opt_no_main = ref false let opt_memo_cache = ref false let opt_no_rts = ref false let opt_prefix = ref "z" +let opt_extra_params = ref None +let opt_extra_arguments = ref None + +let extra_params () = + match !opt_extra_params with + | Some str -> str ^ ", " + | _ -> "" + +let extra_arguments is_extern = + match !opt_extra_arguments with + | Some str when not is_extern -> str ^ ", " + | _ -> "" (* Optimization flags *) let optimize_primops = ref false @@ -2588,6 +2600,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | I_funcall (x, extern, f, args) -> let c_args = Util.string_of_list ", " sgen_cval args in let ctyp = clexp_ctyp x in + let is_extern = Env.is_extern f ctx.tc_env "c" || extern in let fname = if Env.is_extern f ctx.tc_env "c" then Env.get_extern f ctx.tc_env "c" @@ -2649,9 +2662,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = string (Printf.sprintf " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args) else if is_stack_ctyp ctyp then - string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) + string (Printf.sprintf " %s = %s(%s%s);" (sgen_clexp_pure x) fname (extra_arguments is_extern) c_args) else - string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) + string (Printf.sprintf " %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp x) c_args) | I_clear (ctyp, id) when is_stack_ctyp ctyp -> empty @@ -2867,7 +2880,7 @@ let codegen_type_def ctx = function in Printf.sprintf "%s op" (sgen_ctyp ctyp), empty, empty in - string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_function_id ctor_id) (sgen_id id) ctor_args) ^^ hardline + string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_id ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline ^^ surround 2 0 lbrace (tuple ^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline @@ -3183,9 +3196,9 @@ let codegen_def' ctx = function if Env.is_extern id ctx.tc_env "c" then empty else if is_stack_ctyp ret_ctyp then - string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) else - string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_function_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) | CDEF_fundef (id, ret_arg, args, instrs) as def -> if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else (); @@ -3226,12 +3239,12 @@ let codegen_def' ctx = function | None -> assert (is_stack_ctyp ret_ctyp); (if !opt_static then string "static " else empty) - ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string args) ^^ hardline + ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline | Some gs -> assert (not (is_stack_ctyp ret_ctyp)); (if !opt_static then string "static " else empty) ^^ string "void" ^^ space ^^ codegen_function_id id - ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) + ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) ^^ hardline in function_header diff --git a/src/c_backend.mli b/src/c_backend.mli index e6cc783c..3b26acdf 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -53,18 +53,54 @@ open Type_check (** Global compilation options *) +(** Output a dataflow graph for each generated function in Graphviz + (dot) format. *) val opt_debug_flow_graphs : bool ref + +(** Print the ANF and IR representations of a specific function. *) val opt_debug_function : string ref + +(** Instrument generated code to output a trace. opt_smt_trace is WIP + but intended to enable generating traces suitable for concolic + execution with SMT. *) val opt_trace : bool ref val opt_smt_trace : bool ref + +(** Define generated functions as static *) val opt_static : bool ref + +(** Do not generate a main function *) val opt_no_main : bool ref + +(** (WIP) Do not include rts.h (the runtime), and do not generate code + that requires any setup or teardown routines to be run by a runtime + before executing any instruction semantics. *) val opt_no_rts : bool ref + +(** Ordinarily we use plain z-encoding to name-mangle generated Sail + identifiers into a form suitable for C. If opt_prefix is set, then + the "z" which is added on the front of each generated C function + will be replaced by opt_prefix. E.g. opt_prefix := "sail_" would + give sail_my_function rather than zmy_function. *) val opt_prefix : string ref -(** [opt_memo_cache] will store the compiled function definitions in - file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the - original function to be compiled. Enabled using the -memo +(** opt_extra_params and opt_extra_arguments allow additional state to + be threaded through the generated C code by adding an additional + parameter to each function type, and then giving an extra argument + to each function call. For example we could have + + opt_extra_params := Some "CPUMIPSState *env" + opt_extra_arguments := Some "env" + + and every generated function will take a pointer to a QEMU MIPS + processor state, and each function will be passed the env argument + when it is called. *) +val opt_extra_params : string option ref +val opt_extra_arguments : string option ref + +(** (WIP) [opt_memo_cache] will store the compiled function + definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum + of the original function to be compiled. Enabled using the -memo flag. Uses Marshal so it's quite picky about the exact version of the Sail version. This cache can obviously become stale if the C backend changes - it'll load an old version compiled without said @@ -82,13 +118,14 @@ val optimize_experimental : bool ref (** The compilation context. *) type ctx -(** Convert a typ to a IR ctyp *) -val ctyp_of_typ : ctx -> Ast.typ -> ctyp - (** Create a context from a typechecking environment. This environment should be the environment returned by typechecking the full AST. *) val initial_ctx : Env.t -> ctx +(** Convert a typ to a IR ctyp *) +val ctyp_of_typ : ctx -> Ast.typ -> ctyp + + val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit diff --git a/src/sail.ml b/src/sail.ml index 0450c0ca..949663d4 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -145,6 +145,12 @@ let options = Arg.align ([ ( "-c_prefix", Arg.String (fun prefix -> C_backend.opt_prefix := prefix), " prefix generated C functions" ); + ( "-c_extra_params", + Arg.String (fun params -> C_backend.opt_extra_params := Some params), + " generate C functions with additional parameters" ); + ( "-c_extra_args", + Arg.String (fun args -> C_backend.opt_extra_arguments := Some args), + " supply extra argument to every generated C function call" ); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an ELF file so that it can be executed by compiled C code"); -- cgit v1.2.3 From 2fd45fa939ddae7cdb31ee0495e622e6e6a6235f Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 20 Feb 2019 09:55:19 +0000 Subject: Coq: some work on bool simplification This introduces some simplification of informative booleans, but tries too hard to eliminate all of the existentials resulting in difficulties in and/or trees. --- src/pretty_print_coq.ml | 213 ++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 172 insertions(+), 41 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 430eb40d..c4983597 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -350,6 +350,14 @@ match nc1, nc2 with | _, NC_aux (NC_true,_) -> nc1 | _,_ -> nc_and nc1 nc2 +let nice_imp nc1 nc2 = +match nc1, nc2 with +| NC_aux (NC_true,_), _ -> nc2 +| _, NC_aux (NC_true,_) -> nc2 +| NC_aux (NC_false,l), _ -> NC_aux (NC_true,l) +| _, NC_aux (NC_false,_) -> nc_not nc1 +| _,_ -> nc_or (nc_not nc1) nc2 + let nice_iff nc1 nc2 = match nc1, nc2 with | NC_aux (NC_true,_), _ -> nc2 @@ -370,30 +378,151 @@ let doc_nc_fn id = | "not" -> string "negb" | s -> string s -type ex_atom_bool = ExBool_simple | ExBool_val of bool | ExBool_complex +let merge_bool_count = KBindings.union (fun _ m n -> Some (m+n)) -let non_trivial_ex_atom_bool l kopts nc atom_nc = - let vars = KOptSet.union (kopts_of_constraint nc) (kopts_of_constraint atom_nc) in - let exists = KOptSet.of_list kopts in - if KOptSet.subset vars exists then - let kenv = List.fold_left (fun kenv kopt -> KBindings.add (kopt_kid kopt) (unaux_kind (kopt_kind kopt)) kenv) KBindings.empty kopts in - match Constraint.call_smt l kenv (nc_and nc atom_nc), - Constraint.call_smt l kenv (nc_and nc (nc_not atom_nc)) with - | Sat, Sat -> ExBool_simple - | Sat, Unsat -> ExBool_val true - | Unsat, Sat -> ExBool_val false - | _ -> ExBool_complex - else ExBool_complex - -type ex_kind = ExNone | ExBool | ExGeneral +let rec count_bool_vars (NC_aux (nc,_)) = + let count_arg (A_aux (arg,_)) = + match arg with + | A_bool nc -> count_bool_vars nc + | A_nexp _ | A_typ _ | A_order _ -> KBindings.empty + in + match nc with + | NC_or (nc1,nc2) + | NC_and (nc1,nc2) + -> merge_bool_count (count_bool_vars nc1) (count_bool_vars nc2) + | NC_var kid -> KBindings.singleton kid 1 + | NC_equal _ | NC_bounded_ge _ | NC_bounded_le _ | NC_not_equal _ + | NC_set _ | NC_true | NC_false + -> KBindings.empty + | NC_app (_,args) -> + List.fold_left merge_bool_count KBindings.empty (List.map count_arg args) + +type prop_dir = Implied_by | Implies | Iff + +type atom_bool_prop = + Bool_boring +| Bool_complex of prop_dir * kinded_id list * n_constraint * n_constraint + +let simplify_atom_bool l kopts nc atom_nc = +prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); + let counter = ref 0 in + let is_bound kid = List.exists (fun kopt -> Kid.compare kid (kopt_kid kopt) == 0) kopts in + let bool_vars = merge_bool_count (count_bool_vars nc) (count_bool_vars atom_nc) in + let lin_bool_vars = KBindings.filter (fun kid n -> is_bound kid && n = 1) bool_vars in + let rec simplify (NC_aux (nc,l) as nc_full) = + let is_ex_var news (NC_aux (nc,_)) = + match nc with + | NC_var kid when KBindings.mem kid lin_bool_vars -> Some kid + | NC_var kid when KidSet.mem kid news -> Some kid + | _ -> None + in + let replace kills vars = + let v = mk_kid ("simp#" ^ string_of_int !counter) in + let kills = KidSet.union kills (KidSet.of_list vars) in + counter := !counter + 1; + KidSet.singleton v, kills, NC_aux (NC_var v,l) + in + match nc with + | NC_or (nc1,nc2) -> begin + let new1, kill1, nc1 = simplify nc1 in + let new2, kill2, nc2 = simplify nc2 in + let news, kills = KidSet.union new1 new2, KidSet.union kill1 kill2 in + match is_ex_var news nc1, is_ex_var news nc2 with + | Some kid1, Some kid2 -> replace kills [kid1;kid2] + | _ -> news, kills, NC_aux (NC_or (nc1,nc2),l) + end + | NC_and (nc1,nc2) -> begin + let new1, kill1, nc1 = simplify nc1 in + let new2, kill2, nc2 = simplify nc2 in + let news, kills = KidSet.union new1 new2, KidSet.union kill1 kill2 in + match is_ex_var news nc1, is_ex_var news nc2 with + | Some kid1, Some kid2 -> replace kills [kid1;kid2] + | _ -> news, kills, NC_aux (NC_and (nc1,nc2),l) + end + | NC_app (Id_aux (Id "not",_) as id,[A_aux (A_bool nc1,al)]) -> begin + let new1, kill1, nc1 = simplify nc1 in + match is_ex_var new1 nc1 with + | Some kid -> replace kill1 [kid] + | None -> new1, kill1, NC_aux (NC_app (id,[A_aux (A_bool nc1,al)]),l) + end + (* We don't currently recurse into general uses of NC_app, but the + "boring" cases we really want to get rid of won't contain + those. *) + | _ -> KidSet.empty, KidSet.empty, nc_full + in + let new_nc, kill_nc, nc = simplify nc in + let new_atom, kill_atom, atom_nc = simplify atom_nc in + let new_kids = KidSet.union new_nc new_atom in + let kill_kids = KidSet.union kill_nc kill_atom in + let rec strip_implied (NC_aux (nc,l) as nc_full) = + match nc with + | NC_var kid when KBindings.mem kid lin_bool_vars -> None + | NC_var kid when KidSet.mem kid new_kids -> None + | NC_and (nc1,nc2) -> begin + match strip_implied nc1, strip_implied nc2 with + | Some nc1, Some nc2 -> Some (NC_aux (NC_and (nc1,nc2),l)) + | Some nc, None + | None, Some nc -> Some nc + | None, None -> None + end + | NC_or (nc1,nc2) -> begin + match strip_implied nc1, strip_implied nc2 with + | Some nc1, Some nc2 -> Some (NC_aux (NC_or (nc1,nc2),l)) + | _ -> None + end + | _ -> Some nc_full + in + let rec strip_implies (NC_aux (nc,l) as nc_full) = + match nc with + | NC_var kid when KBindings.mem kid lin_bool_vars -> None + | NC_var kid when KidSet.mem kid new_kids -> None + | NC_and (nc1,nc2) -> begin + match strip_implied nc1, strip_implied nc2 with + | Some nc1, Some nc2 -> Some (NC_aux (NC_and (nc1,nc2),l)) + | _ -> None + end + | NC_or (nc1,nc2) -> begin + match strip_implied nc1, strip_implied nc2 with + | Some nc1, Some nc2 -> Some (NC_aux (NC_or (nc1,nc2),l)) + | Some nc, None + | None, Some nc -> Some nc + | None, None -> None + end + | _ -> Some nc_full + in + let strip_implied (NC_aux (_,l) as nc) = + Util.option_default (NC_aux (NC_true,l)) (strip_implied nc) + in + let strip_implies (NC_aux (_,l) as nc) = + Util.option_default (NC_aux (NC_true,l)) (strip_implies nc) + in + let kopts = + List.map (fun kid -> mk_kopt K_bool kid) (KidSet.elements new_kids) @ + List.filter (fun kopt -> not (KidSet.mem (kopt_kid kopt) kill_kids)) kopts + in +prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); + match atom_nc with + | NC_aux (NC_var kid,_) when KBindings.mem kid lin_bool_vars -> Bool_boring + | NC_aux (NC_var kid,_) when KidSet.mem kid new_kids -> Bool_boring + | NC_aux (NC_and (NC_aux (NC_var kid,_),nc'),_) when KBindings.mem kid lin_bool_vars -> + Bool_complex (Implies, kopts, nc, strip_implied nc') + | NC_aux (NC_and (nc',NC_aux (NC_var kid,_)),_) when KBindings.mem kid lin_bool_vars -> + Bool_complex (Implies, kopts, nc, strip_implied nc') + | NC_aux (NC_or (NC_aux (NC_var kid,_),nc'),_) when KBindings.mem kid lin_bool_vars -> + Bool_complex (Implied_by, kopts, nc, strip_implies nc') + | NC_aux (NC_or (nc',NC_aux (NC_var kid,_)),_) when KBindings.mem kid lin_bool_vars -> + Bool_complex (Implied_by, kopts, nc, strip_implies nc') + | _ -> Bool_complex (Iff, kopts, nc, atom_nc) + + +type ex_kind = ExNone | ExGeneral let classify_ex_type (Typ_aux (t,l) as t0) = match t with | Typ_exist (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) as t1)) -> begin - match non_trivial_ex_atom_bool l kopts nc atom_nc with - | ExBool_simple -> ExNone, t1 - | ExBool_val _ -> ExBool, t1 - | ExBool_complex -> ExGeneral, t1 + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> ExNone, t1 + | Bool_complex _ -> ExGeneral, t1 end | Typ_exist (_,_,t1) -> ExGeneral,t1 | _ -> ExNone,t0 @@ -505,12 +634,15 @@ let rec doc_typ_fns ctx = ampersand; doc_arithfact ctx ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc]) | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> begin - match non_trivial_ex_atom_bool l kopts nc atom_nc with - | ExBool_simple -> string "bool" - | ExBool_val t -> string "Bool(" ^^ if t then string "True)" else string "False)" - | ExBool_complex -> + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> string "bool" + | Bool_complex (dir,kopts,nc,atom_nc) -> let var = mk_kid "_bool" in (* TODO collision avoid *) - let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in + let nc = nice_and + (match dir with + | Implies -> nice_imp (nc_var var) atom_nc + | Implied_by -> nice_imp atom_nc (nc_var var) + | Iff -> nice_iff (nc_var var) atom_nc) nc in braces (separate space [doc_var ctx var; colon; string "bool"; ampersand; @@ -816,9 +948,9 @@ let is_ctor env id = match Env.lookup_id id env with let is_auto_decomposed_exist env typ = let typ = expand_range_type typ in - match destruct_exist_plain (Env.expand_synonyms env typ) with - | Some (_, _, typ') -> Some typ' - | _ -> None + match classify_ex_type (Env.expand_synonyms env typ) with + | ExGeneral, typ' -> Some typ' + | ExNone, _ -> None (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen @@ -828,6 +960,7 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty let typ = Env.expand_synonyms env typ in match exists_as_pairs, is_auto_decomposed_exist env typ with | true, Some typ' -> +prerr_endline ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ'); let pat_pp = doc_pat ctxt true true (pat, typ') in let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in if apat_needed then parens pat_pp else pat_pp @@ -1068,10 +1201,9 @@ let doc_exp, doc_let = match destruct_exist_plain typ with | None -> epp | Some (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l)) -> begin - match non_trivial_ex_atom_bool l kopts nc atom_nc with - | ExBool_simple -> epp - | ExBool_val t -> wrap_parens (string "build_Bool" ^/^ epp) - | ExBool_complex -> wrap_parens (string "build_ex" ^/^ epp) + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> epp + | Bool_complex _ -> wrap_parens (string "build_ex" ^/^ epp) end | Some _ -> wrap_parens (string "build_ex" ^/^ epp) @@ -1088,10 +1220,9 @@ let doc_exp, doc_let = let build_ex, out_typ = match destruct_exist_plain typ' with | Some (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l) as t)) -> begin - match non_trivial_ex_atom_bool l kopts nc atom_nc with - | ExBool_simple -> None, t - | ExBool_val _ -> Some "build_Bool", t - | ExBool_complex -> Some "build_ex", t + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> None, t + | Bool_complex _ -> Some "build_ex", t end | Some (_,_,t) -> Some "build_ex", t | None -> None, typ' @@ -1204,7 +1335,11 @@ let doc_exp, doc_let = | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> let call = doc_id (append_id f "M") in - wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args))) + let epp = hang 2 (flow (break 1) (call :: List.map expY args)) in + let epp = match is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp) with + | Some _ -> string "build_ex" ^^ space ^^ parens epp + | None -> epp + in wrap_parens epp (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_ctor none | Id_aux (Id "foreach#", _) -> @@ -1574,7 +1709,6 @@ let doc_exp, doc_let = | ExNone, ExNone -> epp else match cast_ex with | ExGeneral -> string "build_ex" ^^ space ^^ epp - | ExBool -> string "build_Bool" ^^ space ^^ epp | ExNone -> epp in let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in @@ -1582,11 +1716,9 @@ let doc_exp, doc_let = if effects then match cast_ex, outer_ex with | ExGeneral, ExNone -> string "projT1_m" ^^ space ^^ parens epp - | ExBool, ExNone -> string "projBool_m" ^^ space ^^ parens epp | _ -> epp else match cast_ex with | ExGeneral -> string "projT1" ^^ space ^^ parens epp - | ExBool -> string "projBool" ^^ space ^^ parens epp | ExNone -> epp in let epp = @@ -1759,7 +1891,7 @@ let doc_exp, doc_let = let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) full_typ) with | ExGeneral, _ -> squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) - | (ExBool | ExNone), _ -> + | ExNone, _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) in separate space [string ">>= fun"; binder; bigarrow] | _ -> @@ -2244,7 +2376,6 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = let build_ex, ret_typ = replace_atom_return_type ret_typ in let build_ex = match classify_ex_type (Env.expand_synonyms env (expand_range_type ret_typ)) with | ExGeneral, _ -> Some "build_ex" - | ExBool, _ -> Some "build_Bool" | ExNone, _ -> build_ex in let ids_to_avoid = all_ids pexp in -- cgit v1.2.3 From 78281d7e30a4d59f499895fae2960248d936eaf9 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 20 Feb 2019 11:47:46 +0000 Subject: Coq: strip informative bools back to more uniform types Also make pretty printing more keen on line breaking --- src/pretty_print_coq.ml | 106 +++++++++++++++--------------------------------- 1 file changed, 32 insertions(+), 74 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index c4983597..3d2e238d 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -401,7 +401,7 @@ type prop_dir = Implied_by | Implies | Iff type atom_bool_prop = Bool_boring -| Bool_complex of prop_dir * kinded_id list * n_constraint * n_constraint +| Bool_complex of kinded_id list * n_constraint * n_constraint let simplify_atom_bool l kopts nc atom_nc = prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); @@ -454,48 +454,6 @@ prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_o let new_atom, kill_atom, atom_nc = simplify atom_nc in let new_kids = KidSet.union new_nc new_atom in let kill_kids = KidSet.union kill_nc kill_atom in - let rec strip_implied (NC_aux (nc,l) as nc_full) = - match nc with - | NC_var kid when KBindings.mem kid lin_bool_vars -> None - | NC_var kid when KidSet.mem kid new_kids -> None - | NC_and (nc1,nc2) -> begin - match strip_implied nc1, strip_implied nc2 with - | Some nc1, Some nc2 -> Some (NC_aux (NC_and (nc1,nc2),l)) - | Some nc, None - | None, Some nc -> Some nc - | None, None -> None - end - | NC_or (nc1,nc2) -> begin - match strip_implied nc1, strip_implied nc2 with - | Some nc1, Some nc2 -> Some (NC_aux (NC_or (nc1,nc2),l)) - | _ -> None - end - | _ -> Some nc_full - in - let rec strip_implies (NC_aux (nc,l) as nc_full) = - match nc with - | NC_var kid when KBindings.mem kid lin_bool_vars -> None - | NC_var kid when KidSet.mem kid new_kids -> None - | NC_and (nc1,nc2) -> begin - match strip_implied nc1, strip_implied nc2 with - | Some nc1, Some nc2 -> Some (NC_aux (NC_and (nc1,nc2),l)) - | _ -> None - end - | NC_or (nc1,nc2) -> begin - match strip_implied nc1, strip_implied nc2 with - | Some nc1, Some nc2 -> Some (NC_aux (NC_or (nc1,nc2),l)) - | Some nc, None - | None, Some nc -> Some nc - | None, None -> None - end - | _ -> Some nc_full - in - let strip_implied (NC_aux (_,l) as nc) = - Util.option_default (NC_aux (NC_true,l)) (strip_implied nc) - in - let strip_implies (NC_aux (_,l) as nc) = - Util.option_default (NC_aux (NC_true,l)) (strip_implies nc) - in let kopts = List.map (fun kid -> mk_kopt K_bool kid) (KidSet.elements new_kids) @ List.filter (fun kopt -> not (KidSet.mem (kopt_kid kopt) kill_kids)) kopts @@ -504,15 +462,7 @@ prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_o match atom_nc with | NC_aux (NC_var kid,_) when KBindings.mem kid lin_bool_vars -> Bool_boring | NC_aux (NC_var kid,_) when KidSet.mem kid new_kids -> Bool_boring - | NC_aux (NC_and (NC_aux (NC_var kid,_),nc'),_) when KBindings.mem kid lin_bool_vars -> - Bool_complex (Implies, kopts, nc, strip_implied nc') - | NC_aux (NC_and (nc',NC_aux (NC_var kid,_)),_) when KBindings.mem kid lin_bool_vars -> - Bool_complex (Implies, kopts, nc, strip_implied nc') - | NC_aux (NC_or (NC_aux (NC_var kid,_),nc'),_) when KBindings.mem kid lin_bool_vars -> - Bool_complex (Implied_by, kopts, nc, strip_implies nc') - | NC_aux (NC_or (nc',NC_aux (NC_var kid,_)),_) when KBindings.mem kid lin_bool_vars -> - Bool_complex (Implied_by, kopts, nc, strip_implies nc') - | _ -> Bool_complex (Iff, kopts, nc, atom_nc) + | _ -> Bool_complex (kopts, nc, atom_nc) type ex_kind = ExNone | ExGeneral @@ -571,9 +521,13 @@ let rec doc_typ_fns ctx = | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) -> (string "Z") | Typ_app(Id_aux (Id "atom_bool", _), [_]) -> string "bool" - | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool nc,_)]) -> - let tpp = string "Bool" ^^ space ^^ doc_nc_prop ~top:false ctx nc in - if atyp_needed then parens tpp else tpp + | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool atom_nc,_)]) -> + let var = mk_kid "_bool" in (* TODO collision avoid *) + let nc = nice_iff (nc_var var) atom_nc in + braces (separate space + [doc_var ctx var; colon; string "bool"; + ampersand; + doc_arithfact ctx nc]) | Typ_app(id,args) -> let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in if atyp_needed then parens tpp else tpp @@ -636,13 +590,9 @@ let rec doc_typ_fns ctx = | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> begin match simplify_atom_bool l kopts nc atom_nc with | Bool_boring -> string "bool" - | Bool_complex (dir,kopts,nc,atom_nc) -> + | Bool_complex (kopts,nc,atom_nc) -> let var = mk_kid "_bool" in (* TODO collision avoid *) - let nc = nice_and - (match dir with - | Implies -> nice_imp (nc_var var) atom_nc - | Implied_by -> nice_imp atom_nc (nc_var var) - | Iff -> nice_iff (nc_var var) atom_nc) nc in + let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in braces (separate space [doc_var ctx var; colon; string "bool"; ampersand; @@ -1150,7 +1100,7 @@ let replace_atom_return_type ret_typ = (* For informative booleans tweak the type name so that doc_typ knows that the constraint should be output. *) | Typ_aux (Typ_app (Id_aux (Id "atom_bool",il), ([A_aux (A_bool _,_)] as args)),l) -> - Some "build_Bool", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l) + Some "build_ex", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l) | _ -> None, ret_typ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = @@ -1246,7 +1196,7 @@ let doc_exp, doc_let = else exp_pp in match build_ex with | Some s -> - let exp_pp = string s ^^ space ^^ exp_pp in + let exp_pp = string s ^/^ exp_pp in if want_parens then parens exp_pp else exp_pp | None -> exp_pp in aux @@ -1335,9 +1285,17 @@ let doc_exp, doc_let = | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> let call = doc_id (append_id f "M") in - let epp = hang 2 (flow (break 1) (call :: List.map expY args)) in + let doc_arg exp = + let epp = expY exp in + match is_auto_decomposed_exist (env_of exp) (typ_of exp) with + | Some _ -> + let proj = if effectful (effect_of exp) then "projT1_m" else "projT1" in + parens (string proj ^/^ epp) + | None -> epp + in + let epp = hang 2 (flow (break 1) (call :: List.map doc_arg args)) in let epp = match is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp) with - | Some _ -> string "build_ex" ^^ space ^^ parens epp + | Some _ -> string "build_ex_m" ^/^ parens epp | None -> epp in wrap_parens epp (* temporary hack to make the loop body a function of the temporary variables *) @@ -1610,12 +1568,12 @@ let doc_exp, doc_let = if effectful eff then "autocast_m", "projT1_m" else "autocast", "projT1" in - let epp = if unpack && not (effectful eff) then string proj_id ^^ space ^^ parens epp else epp in - let epp = if projbool && not (effectful eff) then string "projBool" ^^ space ^^ parens epp else epp in + let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in + let epp = if projbool && not (effectful eff) then string "projT1" ^/^ parens epp else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in let epp = if effectful eff && packeff && not unpack - then string "build_ex_m" ^^ space ^^ parens epp + then string "build_ex_m" ^^ break 1 ^^ parens epp else epp in liftR (if aexp_needed then parens (align epp) else epp) @@ -1701,24 +1659,24 @@ let doc_exp, doc_let = otherwise derive the new type from the old one. *) if alpha_equivalent env inner_typ cast_typ then epp - else string "derive_m" ^^ space ^^ epp + else string "derive_m" ^/^ epp | ExGeneral, ExNone -> - string "projT1_m" ^^ space ^^ epp + string "projT1_m" ^/^ epp | ExNone, ExGeneral -> - string "build_ex_m" ^^ space ^^ epp + string "build_ex_m" ^/^ epp | ExNone, ExNone -> epp else match cast_ex with - | ExGeneral -> string "build_ex" ^^ space ^^ epp + | ExGeneral -> string "build_ex" ^/^ epp | ExNone -> epp in let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in let epp = if effects then match cast_ex, outer_ex with - | ExGeneral, ExNone -> string "projT1_m" ^^ space ^^ parens epp + | ExGeneral, ExNone -> string "projT1_m" ^/^ parens epp | _ -> epp else match cast_ex with - | ExGeneral -> string "projT1" ^^ space ^^ parens epp + | ExGeneral -> string "projT1" ^/^ parens epp | ExNone -> epp in let epp = -- cgit v1.2.3 From a49a5087d0a2aa25f87bf17a1baa71a29e260b72 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 20 Feb 2019 13:47:10 +0000 Subject: Coq: merge tyvars with corresponding variables --- src/pretty_print_coq.ml | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 3d2e238d..1f37ada5 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1278,7 +1278,35 @@ let doc_exp, doc_let = | E_loop _ -> raise (report l __POS__ "E_loop should have been rewritten before pretty-printing") | E_let(leb,e) -> - let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in + (* TODO: move the context update out of here and use for other binders, too *) + let pat = match leb with LB_aux (LB_val (p,_),_) -> p in + let old_env = env_of_annot (l,annot) in + let new_env = env_of e in + let is_new_binding id = + match Env.lookup_id ~raw:true id old_env with + | Unbound -> true + | _ -> false + in + let new_ids = IdSet.filter is_new_binding (pat_ids pat) in + let merge_new_kids id m = + let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in + debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ )); + match destruct_numeric typ with + | Some ([],_,Nexp_aux (Nexp_var kid,_)) -> + begin try + let _ = Env.get_typ_var kid old_env in + debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); + m + with _ -> + debug ctxt (lazy (" adding tyvar mapping " ^ string_of_kid kid ^ " to " ^ string_of_id id)); + KBindings.add kid id m + end + | _ -> + debug ctxt (lazy (" not suitable type")); + m + in + let new_ctxt = { ctxt with kid_id_renames = IdSet.fold merge_new_kids new_ids ctxt.kid_id_renames } in + let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ top_exp new_ctxt false e in if aexp_needed then parens epp else epp | E_app(f,args) -> begin match f with -- cgit v1.2.3 From 0bb1456fccfd3914b4ec7a714f3479f665711790 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 21 Feb 2019 14:39:34 +0000 Subject: Turn off some debugging messages --- src/pretty_print_coq.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 1f37ada5..c4e4e1c1 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -404,7 +404,7 @@ type atom_bool_prop = | Bool_complex of kinded_id list * n_constraint * n_constraint let simplify_atom_bool l kopts nc atom_nc = -prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); +(*prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc);*) let counter = ref 0 in let is_bound kid = List.exists (fun kopt -> Kid.compare kid (kopt_kid kopt) == 0) kopts in let bool_vars = merge_bool_count (count_bool_vars nc) (count_bool_vars atom_nc) in @@ -458,7 +458,7 @@ prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_o List.map (fun kid -> mk_kopt K_bool kid) (KidSet.elements new_kids) @ List.filter (fun kopt -> not (KidSet.mem (kopt_kid kopt) kill_kids)) kopts in -prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); +(*prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc);*) match atom_nc with | NC_aux (NC_var kid,_) when KBindings.mem kid lin_bool_vars -> Bool_boring | NC_aux (NC_var kid,_) when KidSet.mem kid new_kids -> Bool_boring @@ -910,7 +910,7 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty let typ = Env.expand_synonyms env typ in match exists_as_pairs, is_auto_decomposed_exist env typ with | true, Some typ' -> -prerr_endline ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ'); +(*prerr_endline ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ');*) let pat_pp = doc_pat ctxt true true (pat, typ') in let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in if apat_needed then parens pat_pp else pat_pp -- cgit v1.2.3 From 9e0a49a8aa56affa8018e5978616fc01521c50dc Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 21 Feb 2019 15:13:58 +0000 Subject: Coq: update tyvar merge information at other binders --- src/pretty_print_coq.ml | 72 +++++++++++++++++++++++++------------------------ 1 file changed, 37 insertions(+), 35 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index c4e4e1c1..2da2b024 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1125,6 +1125,32 @@ let is_prefix s s' = String.length s' >= l && String.sub s' 0 l = s +let merge_new_tyvars ctxt old_env pat new_env = + let is_new_binding id = + match Env.lookup_id ~raw:true id old_env with + | Unbound -> true + | _ -> false + in + let new_ids = IdSet.filter is_new_binding (pat_ids pat) in + let merge_new_kids id m = + let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in + debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ )); + match destruct_numeric typ with + | Some ([],_,Nexp_aux (Nexp_var kid,_)) -> + begin try + let _ = Env.get_typ_var kid old_env in + debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); + m + with _ -> + debug ctxt (lazy (" adding tyvar mapping " ^ string_of_kid kid ^ " to " ^ string_of_id id)); + KBindings.add kid id m + end + | _ -> + debug ctxt (lazy (" not suitable type")); + m + in + { ctxt with kid_id_renames = IdSet.fold merge_new_kids new_ids ctxt.kid_id_renames } + let prefix_recordtype = true let report = Reporting.err_unreachable let doc_exp, doc_let = @@ -1278,34 +1304,8 @@ let doc_exp, doc_let = | E_loop _ -> raise (report l __POS__ "E_loop should have been rewritten before pretty-printing") | E_let(leb,e) -> - (* TODO: move the context update out of here and use for other binders, too *) let pat = match leb with LB_aux (LB_val (p,_),_) -> p in - let old_env = env_of_annot (l,annot) in - let new_env = env_of e in - let is_new_binding id = - match Env.lookup_id ~raw:true id old_env with - | Unbound -> true - | _ -> false - in - let new_ids = IdSet.filter is_new_binding (pat_ids pat) in - let merge_new_kids id m = - let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in - debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ )); - match destruct_numeric typ with - | Some ([],_,Nexp_aux (Nexp_var kid,_)) -> - begin try - let _ = Env.get_typ_var kid old_env in - debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); - m - with _ -> - debug ctxt (lazy (" adding tyvar mapping " ^ string_of_kid kid ^ " to " ^ string_of_id id)); - KBindings.add kid id m - end - | _ -> - debug ctxt (lazy (" not suitable type")); - m - in - let new_ctxt = { ctxt with kid_id_renames = IdSet.fold merge_new_kids new_ids ctxt.kid_id_renames } in + let new_ctxt = merge_new_tyvars ctxt (env_of_annot (l,annot)) pat (env_of e) in let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ top_exp new_ctxt false e in if aexp_needed then parens epp else epp | E_app(f,args) -> @@ -1794,7 +1794,7 @@ let doc_exp, doc_let = let only_integers e = expY e in let epp = group ((separate space [string "match"; only_integers e; string "with"]) ^/^ - (separate_map (break 1) (doc_case ctxt (typ_of e)) pexps) ^/^ + (separate_map (break 1) (doc_case ctxt (env_of_annot (l,annot)) (typ_of e)) pexps) ^/^ (string "end")) in if aexp_needed then parens (align epp) else align epp | E_try (e, pexps) -> @@ -1803,7 +1803,7 @@ let doc_exp, doc_let = let epp = (* TODO capture avoidance for __catch_val *) group ((separate space [string try_catch; expY e; string "(fun __catch_val => match __catch_val with "]) ^/^ - (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^ + (separate_map (break 1) (doc_case ctxt (env_of_annot (l,annot)) exc_typ) pexps) ^/^ (string "end)")) in if aexp_needed then parens (align epp) else align epp else @@ -1826,11 +1826,12 @@ let doc_exp, doc_let = debug ctxt (lazy ("Internal plet, pattern " ^ string_of_pat pat)); debug ctxt (lazy (" type of e1 " ^ string_of_typ (typ_of e1))) in + let new_ctxt = merge_new_tyvars ctxt (env_of_annot (l,annot)) pat (env_of e2) in match pat, e1, e2 with | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)), (E_aux (E_assert (assert_e1,assert_e2),_)), _ -> let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in - let epp = infix 0 1 (string ">>= fun _ =>") epp (expN e2) in + let epp = infix 0 1 (string ">>= fun _ =>") epp (top_exp new_ctxt false e2) in if aexp_needed then parens (align epp) else align epp (* Special case because we don't handle variables with nested existentials well yet. TODO: check that id1 is not used in e2' *) @@ -1854,7 +1855,7 @@ let doc_exp, doc_let = separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] in - infix 0 1 middle e1_pp (expN e2') + infix 0 1 middle e1_pp (top_exp new_ctxt false e2') | _ -> let epp = let middle = @@ -1883,7 +1884,7 @@ let doc_exp, doc_let = | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow] in - infix 0 1 middle (expY e1) (expN e2) + infix 0 1 middle (expY e1) (top_exp new_ctxt false e2) in if aexp_needed then parens (align epp) else epp end @@ -1975,10 +1976,11 @@ let doc_exp, doc_let = else doc_id id in group (doc_op coloneq fname (top_exp ctxt true e)) - and doc_case ctxt typ = function + and doc_case ctxt old_env typ = function | Pat_aux(Pat_exp(pat,e),_) -> - group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow]) - (group (top_exp ctxt false e))) + let new_ctxt = merge_new_tyvars ctxt old_env pat (env_of e) in + group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow]) + (group (top_exp new_ctxt false e))) | Pat_aux(Pat_when(_,_,_),(l,_)) -> raise (Reporting.err_unreachable l __POS__ "guarded pattern expression should have been rewritten before pretty-printing") -- cgit v1.2.3 From 143ae2d39ede6bef3e39e2ec4d407ddfdd281a0c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 22 Feb 2019 12:22:06 +0000 Subject: Coq: more for informative booleans Make internal_plet produce annotations (with code to replace unusable type variables) Add mappings for bool kids at bindings Add version of and_bool that proves a property --- src/pretty_print_coq.ml | 76 +++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 68 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 2da2b024..1079d68e 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -477,6 +477,43 @@ let classify_ex_type (Typ_aux (t,l) as t0) = | Typ_exist (_,_,t1) -> ExGeneral,t1 | _ -> ExNone,t0 +(* The AST doesn't generally have enough type annotations for the booleans, + so we attempt to add some (for internal_plet at the moment). This + function helps by checking that the type variables that appear can be + printed for Coq, and attempts to replace them if not. *) +(* TODO: actually check the substitution applies *somewhere* *) +let clean_typ ctxt env typ = + let kids = tyvars_of_typ typ in + let is_equal kid kid' = + prove __POS__ env (nc_eq (nvar kid) (nvar kid')) + in + let check kid subst = + if KidSet.mem kid ctxt.bound_nvars || + KBindings.mem kid ctxt.kid_renames || + KBindings.mem kid ctxt.kid_id_renames + then subst + else + match KidSet.find_first_opt (is_equal kid) ctxt.bound_nvars with + | Some kid' -> KBindings.add kid kid' subst + | None -> + match KBindings.find_first_opt (is_equal kid) ctxt.kid_renames with + | Some (kid',_) -> KBindings.add kid kid' subst + | None -> + match KBindings.find_first_opt (is_equal kid) ctxt.kid_id_renames with + | Some (kid',_) -> KBindings.add kid kid' subst + | None -> + raise Not_found + in + try + let subst = KidSet.fold check kids KBindings.empty in + (* TODO: this is an awful way to do the subsitution! *) + let typ = KBindings.fold (fun kid kid' typ -> subst_kid typ_subst kid kid' typ) subst typ in + Some typ + with Not_found -> + debug ctxt (lazy ("Failed to clean type " ^ string_of_typ typ ^ " under constraints " ^ + Util.string_of_list ", " string_of_n_constraint (Env.get_constraints env))); + None + (* When making changes here, check whether they affect coq_nvars_of_typ *) let rec doc_typ_fns ctx = (* following the structure of parser for precedence *) @@ -1135,8 +1172,9 @@ let merge_new_tyvars ctxt old_env pat new_env = let merge_new_kids id m = let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ )); - match destruct_numeric typ with - | Some ([],_,Nexp_aux (Nexp_var kid,_)) -> + match destruct_numeric typ, destruct_atom_bool new_env typ with + | Some ([],_,Nexp_aux (Nexp_var kid,_)), _ + | _, Some (NC_aux (NC_var kid,_)) -> begin try let _ = Env.get_typ_var kid old_env in debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); @@ -1312,20 +1350,22 @@ let doc_exp, doc_let = begin match f with | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> - let call = doc_id (append_id f "M") in + let informative = Util.is_some (is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp)) in + let suffix = if informative then "MP" else "M" in + let call = doc_id (append_id f suffix) in let doc_arg exp = let epp = expY exp in match is_auto_decomposed_exist (env_of exp) (typ_of exp) with | Some _ -> + if informative then epp else let proj = if effectful (effect_of exp) then "projT1_m" else "projT1" in parens (string proj ^/^ epp) - | None -> epp + | None -> + if informative then parens (string "build_trivial_ex" ^/^ epp) + else epp in let epp = hang 2 (flow (break 1) (call :: List.map doc_arg args)) in - let epp = match is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp) with - | Some _ -> string "build_ex_m" ^/^ parens epp - | None -> epp - in wrap_parens epp + wrap_parens epp (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_ctor none | Id_aux (Id "foreach#", _) -> @@ -1881,6 +1921,26 @@ let doc_exp, doc_let = | ExNone, _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) in separate space [string ">>= fun"; binder; bigarrow] + | P_aux (P_id id,_) -> + let typ = typ_of e1 in + let plain_binder = squote ^^ doc_pat ctxt true true (pat, typ_of e1) in + let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) typ) with + | ExGeneral, (Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) as typ') -> + begin match clean_typ ctxt (env_of_pat pat) typ with + | Some typ' -> + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ']) + | None -> plain_binder end + | ExNone, typ' -> begin + match typ' with + | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) -> + begin match clean_typ ctxt (env_of_pat pat) typ with + | Some typ' -> + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ']) + | None -> plain_binder end + | _ -> plain_binder + end + | _ -> plain_binder + in separate space [string ">>= fun"; binder; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow] in -- cgit v1.2.3 From f86ce3508a9909032d1168091989b65a796314a6 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 28 Feb 2019 16:47:00 +0000 Subject: Coq: Clean up rich boolean handling in backend Now generates something vaguely sensible for RISC-V, although the solver needs a little work. Adds type annotations around effectful, rich and/or expressions. --- src/pretty_print_coq.ml | 230 ++++++++++++++++++++++-------------------------- 1 file changed, 104 insertions(+), 126 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 1079d68e..5dfeb7ba 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -467,52 +467,36 @@ let simplify_atom_bool l kopts nc atom_nc = type ex_kind = ExNone | ExGeneral -let classify_ex_type (Typ_aux (t,l) as t0) = +(* Should a Sail type be turned into a dependent pair in Coq? + Optionally takes a variable that we're binding (to avoid trivial cases where + the type is exactly the boolean we're binding), and whether to turn bools + with interesting type-expressions into dependent pairs. *) +let classify_ex_type ctxt env ?binding ?(rawbools=false) (Typ_aux (t,l) as t0) = + let is_binding kid = + match binding, KBindings.find_opt kid ctxt.kid_id_renames with + | Some id, Some id' when Id.compare id id' == 0 -> true + | _ -> false + in + let simplify_atom_bool l kopts nc atom_nc = + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> Bool_boring + | Bool_complex (_,_,NC_aux (NC_var kid,_)) when is_binding kid -> Bool_boring + | Bool_complex (x,y,z) -> Bool_complex (x,y,z) + in match t with - | Typ_exist (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) as t1)) -> begin + | Typ_exist (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_)) -> begin match simplify_atom_bool l kopts nc atom_nc with - | Bool_boring -> ExNone, t1 - | Bool_complex _ -> ExGeneral, t1 + | Bool_boring -> ExNone, [], bool_typ + | Bool_complex _ -> ExGeneral, [], bool_typ end - | Typ_exist (_,_,t1) -> ExGeneral,t1 - | _ -> ExNone,t0 - -(* The AST doesn't generally have enough type annotations for the booleans, - so we attempt to add some (for internal_plet at the moment). This - function helps by checking that the type variables that appear can be - printed for Coq, and attempts to replace them if not. *) -(* TODO: actually check the substitution applies *somewhere* *) -let clean_typ ctxt env typ = - let kids = tyvars_of_typ typ in - let is_equal kid kid' = - prove __POS__ env (nc_eq (nvar kid) (nvar kid')) - in - let check kid subst = - if KidSet.mem kid ctxt.bound_nvars || - KBindings.mem kid ctxt.kid_renames || - KBindings.mem kid ctxt.kid_id_renames - then subst - else - match KidSet.find_first_opt (is_equal kid) ctxt.bound_nvars with - | Some kid' -> KBindings.add kid kid' subst - | None -> - match KBindings.find_first_opt (is_equal kid) ctxt.kid_renames with - | Some (kid',_) -> KBindings.add kid kid' subst - | None -> - match KBindings.find_first_opt (is_equal kid) ctxt.kid_id_renames with - | Some (kid',_) -> KBindings.add kid kid' subst - | None -> - raise Not_found - in - try - let subst = KidSet.fold check kids KBindings.empty in - (* TODO: this is an awful way to do the subsitution! *) - let typ = KBindings.fold (fun kid kid' typ -> subst_kid typ_subst kid kid' typ) subst typ in - Some typ - with Not_found -> - debug ctxt (lazy ("Failed to clean type " ^ string_of_typ typ ^ " under constraints " ^ - Util.string_of_list ", " string_of_n_constraint (Env.get_constraints env))); - None + | Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]) -> begin + match rawbools, simplify_atom_bool l [] nc_true atom_nc with + | false, _ -> ExNone, [], bool_typ + | _,Bool_boring -> ExNone, [], bool_typ + | _,Bool_complex _ -> ExGeneral, [], bool_typ + end + | Typ_exist (kopts,_,t1) -> ExGeneral,kopts,t1 + | _ -> ExNone,[],t0 (* When making changes here, check whether they affect coq_nvars_of_typ *) let rec doc_typ_fns ctx = @@ -557,14 +541,17 @@ let rec doc_typ_fns ctx = (string "Z") | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) -> (string "Z") - | Typ_app(Id_aux (Id "atom_bool", _), [_]) -> string "bool" - | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool atom_nc,_)]) -> - let var = mk_kid "_bool" in (* TODO collision avoid *) - let nc = nice_iff (nc_var var) atom_nc in - braces (separate space - [doc_var ctx var; colon; string "bool"; - ampersand; - doc_arithfact ctx nc]) + | Typ_app(Id_aux (Id "atom_bool", _), [A_aux (A_bool atom_nc,_)]) -> + begin match simplify_atom_bool l [] nc_true atom_nc with + | Bool_boring -> string "bool" + | Bool_complex (_,_,atom_nc) -> (* simplify won't introduce new kopts *) + let var = mk_kid "_bool" in (* TODO collision avoid *) + let nc = nice_iff (nc_var var) atom_nc in + braces (separate space + [doc_var ctx var; colon; string "bool"; + ampersand; + doc_arithfact ctx nc]) + end | Typ_app(id,args) -> let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in if atyp_needed then parens tpp else tpp @@ -933,11 +920,11 @@ let is_ctor env id = match Env.lookup_id id env with | Enum _ -> true | _ -> false -let is_auto_decomposed_exist env typ = +let is_auto_decomposed_exist ctxt env ?(rawbools=false) typ = let typ = expand_range_type typ in - match classify_ex_type (Env.expand_synonyms env typ) with - | ExGeneral, typ' -> Some typ' - | ExNone, _ -> None + match classify_ex_type ctxt env ~rawbools (Env.expand_synonyms env typ) with + | ExGeneral, kopts, typ' -> Some (kopts, typ') + | ExNone, _, _ -> None (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen @@ -945,10 +932,11 @@ let is_auto_decomposed_exist env typ = let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, typ) = let env = env_of_annot (l,annot) in let typ = Env.expand_synonyms env typ in - match exists_as_pairs, is_auto_decomposed_exist env typ with - | true, Some typ' -> -(*prerr_endline ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ');*) - let pat_pp = doc_pat ctxt true true (pat, typ') in + match exists_as_pairs, is_auto_decomposed_exist ctxt env typ with + | true, Some (kopts,typ') -> + debug ctxt (lazy ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ')); + let ctxt' = { ctxt with bound_nvars = List.fold_left (fun s kopt -> KidSet.add (kopt_kid kopt) s) ctxt.bound_nvars kopts } in + let pat_pp = doc_pat ctxt' true true (pat, typ') in let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in if apat_needed then parens pat_pp else pat_pp | _ -> @@ -1134,10 +1122,8 @@ let replace_atom_return_type ret_typ = | Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp nexp,_)]),l) -> let kid = mk_kid "_retval" in (* TODO: collision avoidance *) Some "build_ex", Typ_aux (Typ_exist ([mk_kopt K_int kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Parse_ast.Generated l) - (* For informative booleans tweak the type name so that doc_typ knows that the - constraint should be output. *) | Typ_aux (Typ_app (Id_aux (Id "atom_bool",il), ([A_aux (A_bool _,_)] as args)),l) -> - Some "build_ex", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l) + Some "build_ex", ret_typ | _ -> None, ret_typ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = @@ -1222,7 +1208,7 @@ let doc_exp, doc_let = | Some _ -> wrap_parens (string "build_ex" ^/^ epp) in - let rec construct_dep_pairs env = + let construct_dep_pairs ?(rawbools=false) env = let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) = match e,t with | E_tuple exps, Typ_tup typs @@ -1231,15 +1217,11 @@ let doc_exp, doc_let = parens (separate (string ", ") (List.map2 (aux false) exps typs)) | _ -> let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in + debug ctxt (lazy ("Constructing " ^ string_of_exp exp ^ " at type " ^ string_of_typ typ)); let build_ex, out_typ = - match destruct_exist_plain typ' with - | Some (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l) as t)) -> begin - match simplify_atom_bool l kopts nc atom_nc with - | Bool_boring -> None, t - | Bool_complex _ -> Some "build_ex", t - end - | Some (_,_,t) -> Some "build_ex", t - | None -> None, typ' + match classify_ex_type ctxt (env_of exp) ~rawbools typ' with + | ExNone, _, _ -> None, typ' + | ExGeneral, _, typ' -> Some "build_ex", typ' in let in_typ = expand_range_type (Env.expand_synonyms (env_of exp) (typ_of exp)) in let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in @@ -1350,14 +1332,14 @@ let doc_exp, doc_let = begin match f with | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> - let informative = Util.is_some (is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp)) in + let informative = Util.is_some (is_auto_decomposed_exist ctxt (env_of full_exp) (general_typ_of full_exp)) in let suffix = if informative then "MP" else "M" in let call = doc_id (append_id f suffix) in let doc_arg exp = let epp = expY exp in - match is_auto_decomposed_exist (env_of exp) (typ_of exp) with + match is_auto_decomposed_exist ctxt (env_of exp) ~rawbools:true (general_typ_of exp) with | Some _ -> - if informative then epp else + if informative then parens (epp ^^ doc_tannot ctxt (env_of exp) true (general_typ_of exp)) else let proj = if effectful (effect_of exp) then "projT1_m" else "projT1" in parens (string proj ^/^ epp) | None -> @@ -1365,6 +1347,7 @@ let doc_exp, doc_let = else epp in let epp = hang 2 (flow (break 1) (call :: List.map doc_arg args)) in + let epp = if informative then epp ^^ doc_tannot ctxt (env_of full_exp) true (general_typ_of full_exp) else epp in wrap_parens epp (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_ctor none @@ -1596,21 +1579,22 @@ let doc_exp, doc_let = let ret_typ_inst = subst_unifiers inst ret_typ in - let packeff,unpack,autocast,projbool = + let packeff,unpack,autocast = let ann_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in let ann_typ = expand_range_type ann_typ in let ret_typ_inst = expand_range_type (Env.expand_synonyms env ret_typ_inst) in let ret_typ_inst = if is_no_proof_fn env f then ret_typ_inst else snd (replace_atom_return_type ret_typ_inst) in - let () = + let () = debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) in let unpack, in_typ = - match ret_typ_inst with - | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1 - | t1 -> false,t1 + if is_no_proof_fn env f then false, ret_typ_inst else + match classify_ex_type ctxt env ~rawbools:true ret_typ_inst with + | ExGeneral, _, t1 -> true,t1 + | ExNone, _, t1 -> false,t1 in let pack,out_typ = match ann_typ with @@ -1625,19 +1609,13 @@ let doc_exp, doc_let = Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) -> not (similar_nexps ctxt env n1 n2) | _ -> false - in - let projbool = - match in_typ with - | Typ_aux (Typ_app (Id_aux (Id "atom#bool",_),_),_) -> true - | _ -> false - in pack,unpack,autocast,projbool + in pack,unpack,autocast in let autocast_id, proj_id = if effectful eff then "autocast_m", "projT1_m" else "autocast", "projT1" in let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in - let epp = if projbool && not (effectful eff) then string "projT1" ^/^ parens epp else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in let epp = if effectful eff && packeff && not unpack @@ -1706,9 +1684,9 @@ let doc_exp, doc_let = debug ctxt (lazy (" on expr of type " ^ string_of_typ inner_typ)); debug ctxt (lazy (" where type expected is " ^ string_of_typ outer_typ)) in - let outer_ex,outer_typ' = classify_ex_type outer_typ in - let cast_ex,cast_typ' = classify_ex_type cast_typ in - let inner_ex,inner_typ' = classify_ex_type inner_typ in + let outer_ex,_,outer_typ' = classify_ex_type ctxt env outer_typ in + let cast_ex,_,cast_typ' = classify_ex_type ctxt env ~rawbools:true cast_typ in + let inner_ex,_,inner_typ' = classify_ex_type ctxt env inner_typ in let autocast = (* Avoid using helper functions which simplify the nexps *) is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' && @@ -1886,11 +1864,11 @@ let doc_exp, doc_let = let middle = match pat' with | P_aux (P_id id,_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) (typ_of e1)) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) typ) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] @@ -1899,44 +1877,39 @@ let doc_exp, doc_let = | _ -> let epp = let middle = + let env1 = env_of e1 in match pat with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_id id,_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) (typ_of e1)) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) typ) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) | P_aux (P_typ (typ, P_aux (P_var (P_aux (P_id id,_),_),_)),_) | P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_) - when not (is_enum (env_of e1) id) -> + when not (is_enum env1 id) -> let full_typ = (expand_range_type typ) in - let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) full_typ) with - | ExGeneral, _ -> + let binder = match classify_ex_type ctxt env1 (Env.expand_synonyms env1 full_typ) with + | ExGeneral, _, _ -> squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) - | ExNone, _ -> + | ExNone, _, _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) in separate space [string ">>= fun"; binder; bigarrow] | P_aux (P_id id,_) -> let typ = typ_of e1 in let plain_binder = squote ^^ doc_pat ctxt true true (pat, typ_of e1) in - let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) typ) with - | ExGeneral, (Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) as typ') -> - begin match clean_typ ctxt (env_of_pat pat) typ with - | Some typ' -> - squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ']) - | None -> plain_binder end - | ExNone, typ' -> begin + let binder = match classify_ex_type ctxt env1 ~binding:id (Env.expand_synonyms env1 typ) with + | ExGeneral, _, (Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) as typ') -> + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) + | ExNone, _, typ' -> begin match typ' with | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) -> - begin match clean_typ ctxt (env_of_pat pat) typ with - | Some typ' -> - squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ']) - | None -> plain_binder end + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) | _ -> plain_binder end | _ -> plain_binder @@ -1958,7 +1931,7 @@ let doc_exp, doc_let = in let valpp = let env = env_of e1 in - construct_dep_pairs env true e1 ret_typ + construct_dep_pairs env true e1 ret_typ ~rawbools:true in wrap_parens (align (separate space [string "returnm"; valpp])) | E_sizeof nexp -> @@ -2009,13 +1982,13 @@ let doc_exp, doc_let = (* Prefer simple lets over patterns, because I've found Coq can struggle to work out return types otherwise *) | LB_val(P_aux (P_id id,_),e) - when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) (typ_of e)) && not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; coloneq]) (top_exp ctxt false e) | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e) - when Util.is_none (is_auto_decomposed_exist (env_of e) typ) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) typ) && not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq]) @@ -2298,7 +2271,7 @@ let pat_is_plain_binder env (P_aux (p,_)) = let demote_all_patterns env i (P_aux (p,p_annot) as pat,typ) = match pat_is_plain_binder env pat with | Some id -> - if Util.is_none (is_auto_decomposed_exist env typ) + if Util.is_none (is_auto_decomposed_exist empty_ctxt env typ) then (pat,typ), fun e -> e else (P_aux (P_id id, p_annot),typ), @@ -2421,11 +2394,6 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = | Typ_aux (Typ_fn (arg_typs, ret_typ, eff),_) -> arg_typs, ret_typ, eff | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type") in - let build_ex, ret_typ = replace_atom_return_type ret_typ in - let build_ex = match classify_ex_type (Env.expand_synonyms env (expand_range_type ret_typ)) with - | ExGeneral, _ -> Some "build_ex" - | ExNone, _ -> build_ex - in let ids_to_avoid = all_ids pexp in let bound_kids = tyvars_of_typquant tq in let pat,guard,exp,(l,_) = destruct_pexp pexp in @@ -2447,15 +2415,23 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = | Rec_aux (Rec_measure _,_) -> true, IdSet.singleton id | _ -> false, IdSet.empty in - let ctxt = + let ctxt0 = { early_ret = contains_early_return exp; kid_renames = mk_kid_renames ids_to_avoid kids_used; kid_id_renames = kid_to_arg_rename; bound_nvars = bound_kids; - build_at_return = if effectful eff then build_ex else None; + build_at_return = None; (* filled in below *) recursive_ids = recursive_ids; debug = List.mem (string_of_id id) (!opt_debug_on) } in + let build_ex, ret_typ = replace_atom_return_type ret_typ in + let build_ex = match classify_ex_type ctxt0 env (Env.expand_synonyms env (expand_range_type ret_typ)) with + | ExGeneral, _, _ -> Some "build_ex" + | ExNone, _, _ -> build_ex + in + let ctxt = { ctxt0 with + build_at_return = if effectful eff then build_ex else None; + } in let () = debug ctxt (lazy ("Function " ^ string_of_id id)); debug ctxt (lazy (" return type " ^ string_of_typ ret_typ)); @@ -2478,19 +2454,21 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ)) in match pat_is_plain_binder env pat with - | Some id -> - if Util.is_none (is_auto_decomposed_exist env exp_typ) then - parens (separate space [doc_id id; colon; doc_typ ctxt typ]) - else begin + | Some id -> begin + match classify_ex_type ctxt env ~binding:id exp_typ with + | ExNone, _, typ' -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ']) + | ExGeneral, _, _ -> let full_typ = (expand_range_type exp_typ) in match destruct_exist_plain (Env.expand_synonyms env full_typ) with | Some ([kopt], NC_aux (NC_true,_), - Typ_aux (Typ_app (Id_aux (Id "atom",_), + Typ_aux (Typ_app (Id_aux (Id ("atom" | "atom_bool" as tyname),_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_)) when Kid.compare (kopt_kid kopt) kid == 0 -> - parens (separate space [doc_id id; colon; string "Z"]) + let coqty = if tyname = "atom" then "Z" else "bool" in + parens (separate space [doc_id id; colon; string coqty]) | Some ([kopt], nc, - Typ_aux (Typ_app (Id_aux (Id "atom",_), + Typ_aux (Typ_app (Id_aux (Id ("atom" | "atom_bool"),_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_)) when Kid.compare (kopt_kid kopt) kid == 0 && not is_measured -> (used_a_pattern := true; -- cgit v1.2.3 From 7503075ef8e9a3698b7bd9c8033ae36a2d0776b9 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 28 Feb 2019 17:54:06 +0000 Subject: Handle implicits in destruct_atom_nexp --- src/type_check.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index 8de4a904..b058d514 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1793,7 +1793,7 @@ and ambiguous_nexp_vars (Nexp_aux (aux, _)) = let destruct_atom_nexp env typ = match Env.expand_synonyms env typ with | Typ_aux (Typ_app (f, [A_aux (A_nexp n, _)]), _) - when string_of_id f = "atom" -> Some n + when string_of_id f = "atom" || string_of_id f = "implicit" -> Some n | Typ_aux (Typ_app (f, [A_aux (A_nexp n, _); A_aux (A_nexp m, _)]), _) when string_of_id f = "range" && nexp_identical n m -> Some n | _ -> None -- cgit v1.2.3 From dfb2ca35204870809730a0feb0ba98c1f45f57ac Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 10:39:37 +0000 Subject: Coq: make iff `iff` Also drop unused implication function --- src/pretty_print_coq.ml | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 5dfeb7ba..d205e46b 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -350,21 +350,14 @@ match nc1, nc2 with | _, NC_aux (NC_true,_) -> nc1 | _,_ -> nc_and nc1 nc2 -let nice_imp nc1 nc2 = -match nc1, nc2 with -| NC_aux (NC_true,_), _ -> nc2 -| _, NC_aux (NC_true,_) -> nc2 -| NC_aux (NC_false,l), _ -> NC_aux (NC_true,l) -| _, NC_aux (NC_false,_) -> nc_not nc1 -| _,_ -> nc_or (nc_not nc1) nc2 - let nice_iff nc1 nc2 = match nc1, nc2 with | NC_aux (NC_true,_), _ -> nc2 | _, NC_aux (NC_true,_) -> nc1 | NC_aux (NC_false,_), _ -> nc_not nc2 | _, NC_aux (NC_false,_) -> nc_not nc1 -| _,_ -> nc_or (nc_and nc1 nc2) (nc_and (nc_not nc1) (nc_not nc2)) + (* TODO: replace this hacky iff with a proper NC_ constructor *) +| _,_ -> mk_nc (NC_app (mk_id "iff",[arg_bool nc1; arg_bool nc2])) (* n_constraint functions are currently just Z3 functions *) let doc_nc_fn_prop id = -- cgit v1.2.3 From 2e835b683c23aa4a63a9d5dac7628b0953be5f24 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 12:14:45 +0000 Subject: Coq tidying: remove old definition, complete a pattern match --- src/pretty_print_coq.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index d205e46b..d323d639 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -390,8 +390,6 @@ let rec count_bool_vars (NC_aux (nc,_)) = | NC_app (_,args) -> List.fold_left merge_bool_count KBindings.empty (List.map count_arg args) -type prop_dir = Implied_by | Implies | Iff - type atom_bool_prop = Bool_boring | Bool_complex of kinded_id list * n_constraint * n_constraint @@ -2746,6 +2744,9 @@ let rec doc_def unimplemented generic_eq_types def = | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings" | DEF_pragma _ -> empty + | DEF_measure (id,_,_) -> unreachable (id_loc id) __POS__ + ("Termination measure for " ^ string_of_id id ^ + " should have been rewritten before backend") let find_exc_typ defs = let is_exc_typ_def = function -- cgit v1.2.3 From 6091ce6ef24cb8ab8b65f528f28109dd15b8cb54 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 15:28:56 +0000 Subject: Fill in some edge cases in monomorphisation --- src/monomorphise.ml | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 784929e1..f0472385 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -344,6 +344,7 @@ and inst_src_typ_arg insts (A_aux (ta,l) as tyarg) = match ta with | A_nexp _ | A_order _ + | A_bool _ -> insts, tyarg | A_typ typ -> let insts', typ' = inst_src_type insts typ in @@ -364,6 +365,7 @@ and contains_exist_arg (A_aux (arg,_)) = match arg with | A_nexp _ | A_order _ + | A_bool _ -> false | A_typ typ -> contains_exist typ @@ -2085,19 +2087,26 @@ let split_defs all_errors splits defs = | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map map_lexp les)) | LEXP_field (le,id) -> re (LEXP_field (map_lexp le, id)) | LEXP_deref e -> re (LEXP_deref (map_exp e)) - in map_pexp, map_letbind - in + in map_exp, map_pexp, map_letbind + in + let map_exp r = let (f,_,_) = map_fns r in f in + let map_pexp r = let (_,f,_) = map_fns r in f in + let map_letbind r = let (_,_,f) = map_fns r in f in + let map_exp exp = + let ref_vars = referenced_vars exp in + map_exp ref_vars exp + in let map_pexp top_pexp = (* Construct the set of referenced variables so that we don't accidentally make false assumptions about them during constant propagation. Note that we assume there aren't any in the guard. *) let (_,_,body,_) = destruct_pexp top_pexp in let ref_vars = referenced_vars body in - fst (map_fns ref_vars) top_pexp + map_pexp ref_vars top_pexp in let map_letbind (LB_aux (LB_val (_,e),_) as lb) = let ref_vars = referenced_vars e in - snd (map_fns ref_vars) lb + map_letbind ref_vars lb in let map_funcl (FCL_aux (FCL_Funcl (id,pexp),annot)) = @@ -2128,6 +2137,7 @@ let split_defs all_errors splits defs = | DEF_mapdef (MD_aux (_, (l, _))) -> Reporting.unreachable l __POS__ "mappings should be gone by now" | DEF_val lb -> [DEF_val (map_letbind lb)] | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd) + | DEF_measure (id,pat,exp) -> [DEF_measure (id,pat,map_exp exp)] in Defs (List.concat (List.map map_def defs)) in @@ -2210,6 +2220,7 @@ and sizes_of_typarg (A_aux (ta,_)) = match ta with A_nexp _ | A_order _ + | A_bool _ -> KidSet.empty | A_typ typ -> sizes_of_typ typ @@ -4380,7 +4391,9 @@ let replace_nexp_in_typ env typ orig new_nexp = | A_typ typ -> let f, typ = aux typ in f, A_aux (A_typ typ,l) - | A_order _ -> false, typ_arg + | A_order _ + | A_bool _ + -> false, typ_arg in aux typ let fresh_nexp_kid nexp = -- cgit v1.2.3 From a8da14a23cd8dfdd5fcc527b930ed553d376d18f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Mar 2019 15:45:46 +0000 Subject: Make Sail more flexible with existentials in union types Issues came up with Christophers translation of hand-written ARM into Sail2 where we were being overly pedantic about the exact position of existential quantifiers in constructors with multiple arguments. This commit generalises unify_typ and type_coercion_unify to be more flexible and support this. Should think at some point if unify_typ can be generalised further. This fix should fix the decode side of things, but may be some issues with the executes that still need looking into when existentials and multiple argument constructors are mixed. --- src/type_check.ml | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index b058d514..a2612794 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1304,6 +1304,15 @@ let bind_existential l name typ env = | Some (kids, nc, typ) -> typ, add_existential l kids nc env | None -> typ, env +let bind_tuple_existentials l name (Typ_aux (aux, annot) as typ) env = + match aux with + | Typ_tup typs -> + let typs, env = + List.fold_right (fun typ (typs, env) -> let typ, env = bind_existential l name typ env in typ :: typs, env) typs ([], env) + in + Typ_aux (Typ_tup typs, annot), env + | _ -> typ, env + let destruct_range env typ = let kopts, constr, (Typ_aux (typ_aux, _)) = Util.option_default ([], nc_true, typ) (destruct_exist (Env.expand_synonyms env typ)) @@ -1567,6 +1576,8 @@ let merge_uvars l unifiers1 unifiers2 = KBindings.merge (merge_unifiers l) unifiers1 unifiers2 let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as typ2) = + typ_debug (lazy (Util.("Unify type " |> magenta |> clear) ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2 + ^ " goals " ^ string_of_list ", " string_of_kid (KidSet.elements goals))); match aux1, aux2 with | Typ_internal_unknown, _ | _, Typ_internal_unknown when Env.allow_unknowns env -> @@ -1577,7 +1588,14 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as | Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]), Typ_app (atom, [A_aux (A_nexp m, _)]) when string_of_id range = "range" && string_of_id atom = "atom" -> - merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m) + let n1, n2 = nexp_simp n1, nexp_simp n2 in + begin match n1, n2 with + | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) -> + if prove __POS__ env (nc_and (nc_lteq n1 m) (nc_lteq m n2)) then KBindings.empty + else unify_error l (string_of_typ typ1 ^ " is not contained within " ^ string_of_typ typ1) + | _, _ -> + merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m) + end | Typ_app (id1, args1), Typ_app (id2, args2) when List.length args1 = List.length args2 && Id.compare id1 id2 = 0 -> List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ_arg l env goals) args1 args2) @@ -2932,6 +2950,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ = try typ_debug (lazy ("Coercing unification: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ)); let atyp, env = bind_existential l None (typ_of annotated_exp) env in + let atyp, env = bind_tuple_existentials l None atyp env in annotated_exp, unify l env (KidSet.diff goals (ambiguous_vars typ)) typ atyp, env with | Unification_error (_, m) when Env.allow_casts env -> -- cgit v1.2.3 From d9db6da6d031effbf820de406f06c4ee973939a5 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Mar 2019 16:29:28 +0000 Subject: Fix bug with naturals in quantified constructors --- src/type_check.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index a2612794..1afd9765 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1585,6 +1585,10 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as | Typ_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_typ typ2) + | Typ_id nat, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id nat = "nat" -> + if prove __POS__ env (nc_gteq n (nint 0)) then KBindings.empty + else unify_error l (string_of_typ typ2 ^ " must be a natural number") + | Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]), Typ_app (atom, [A_aux (A_nexp m, _)]) when string_of_id range = "range" && string_of_id atom = "atom" -> -- cgit v1.2.3 From 3e2cd8de57d4bc865f6b8299dd4e5689b5e8b875 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Mar 2019 16:38:03 +0000 Subject: Add a test case for previous commit Also make unifying int against int('n) work as expected for constructor applications. --- src/type_check.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index 1afd9765..de1c1ae1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1585,6 +1585,9 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as | Typ_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_typ typ2) + (* We need special cases for unifying range(n, m), nat, and int vs atom('n) *) + | Typ_id int, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id int = "int" -> KBindings.empty + | Typ_id nat, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id nat = "nat" -> if prove __POS__ env (nc_gteq n (nint 0)) then KBindings.empty else unify_error l (string_of_typ typ2 ^ " must be a natural number") -- cgit v1.2.3 From a3558b92aa7395b2c841c737d867bbe02c848e03 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 18:19:27 +0000 Subject: Coq: some library compatibility changes --- src/pretty_print_coq.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index d323d639..42780012 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1096,7 +1096,7 @@ let condition_produces_constraint exp = dependent pair with a proof that the result is the expected integer. This is redundant for basic arithmetic functions and functions which we unfold in the constraint solver. *) -let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"; "length"; +let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "Z.rem"; "length_mword"; "length"; "negb"; "andb"; "orb"; "Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"] -- cgit v1.2.3 From a60c223bb5592b8f7b2c1756c6ed0b9920c332a6 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Mar 2019 18:13:32 +0000 Subject: Add some tricky test cases for quantified Sail AST types Fixes some bugs found by doing this --- src/type_check.ml | 33 +++++++++++++++++++++++++++------ 1 file changed, 27 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index de1c1ae1..02339842 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -251,6 +251,25 @@ and strip_kinded_id_aux = function and strip_kind = function | K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown) +let rec typ_constraints (Typ_aux (typ_aux, l)) = + match typ_aux with + | Typ_internal_unknown -> [] + | Typ_id v -> [] + | Typ_var kid -> [] + | Typ_tup typs -> List.concat (List.map typ_constraints typs) + | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args) + | Typ_exist (kids, nc, typ) -> typ_constraints typ + | Typ_fn (arg_typs, ret_typ, _) -> + List.concat (List.map typ_constraints arg_typs) @ typ_constraints ret_typ + | Typ_bidir (typ1, typ2) -> + typ_constraints typ1 @ typ_constraints typ2 +and typ_arg_nexps (A_aux (typ_arg_aux, l)) = + match typ_arg_aux with + | A_nexp n -> [] + | A_typ typ -> typ_constraints typ + | A_bool nc -> [nc] + | A_order ord -> [] + let rec typ_nexps (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_internal_unknown -> [] @@ -2036,7 +2055,7 @@ let rec subtyp l env typ1 typ2 = let env = add_existential l kopts nc env in subtyp l env typ1 typ2 | None, Some (kopts, nc, typ2) -> typ_debug (lazy "Subtype check with unification"); - let typ1 = canonicalize env typ1 in + let typ1, env = bind_existential l None (canonicalize env typ1) env in let env = add_typ_vars l kopts env in let kids' = KidSet.elements (KidSet.diff (KidSet.of_list (List.map kopt_kid kopts)) (tyvars_of_typ typ2)) in if not (kids' = []) then typ_error env l "Universally quantified constraint generated" else (); @@ -3266,13 +3285,15 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _) | TP_wild, _ -> env | TP_var kid, _ -> begin - match typ_nexps typ with - | [nexp] -> + match typ_nexps typ, typ_constraints typ with + | [nexp], [] -> Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l (mk_kopt K_int kid) env) - | [] -> + | [], [nc] -> + Env.add_constraint (nc_and (nc_or (nc_not nc) (nc_var kid)) (nc_or nc (nc_not (nc_var kid)))) (Env.add_typ_var l (mk_kopt K_bool kid) env) + | [], [] -> typ_error env l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to") - | nexps -> - typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric expressions. Cannot bind " ^ string_of_kid kid) + | _, _ -> + typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric or boolean expressions. Cannot bind " ^ string_of_kid kid) end | TP_app (f1, tpats), Typ_app (f2, typs) when Id.compare f1 f2 = 0 -> List.fold_left2 bind_typ_pat_arg env tpats typs -- cgit v1.2.3 From 7584f2303718ef7d345a4ab32ed0ae1344be8816 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Mar 2019 13:43:29 +0000 Subject: WIP: Start working on being able to slice single instructions out of specs --- src/ast_util.mli | 1 + src/graph.ml | 21 +++++- src/graph.mli | 4 +- src/slice.ml | 194 +++++++++++++++++++++++++++++++++++++++++++++++++++++ src/type_check.ml | 30 ++++++--- src/type_check.mli | 4 +- 6 files changed, 240 insertions(+), 14 deletions(-) create mode 100644 src/slice.ml (limited to 'src') diff --git a/src/ast_util.mli b/src/ast_util.mli index 823fcebb..0c42d9d3 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -403,6 +403,7 @@ val ids_of_def : 'a def -> IdSet.t val ids_of_defs : 'a defs -> IdSet.t val pat_ids : 'a pat -> IdSet.t + val subst : id -> 'a exp -> 'a exp -> 'a exp val hex_to_bin : string -> string diff --git a/src/graph.ml b/src/graph.ml index 2fc09014..e3af0b97 100644 --- a/src/graph.ml +++ b/src/graph.ml @@ -88,6 +88,8 @@ module type S = (** Topologically sort a graph. Throws Not_a_DAG if the graph is not directed acyclic. *) val topsort : graph -> node list + + val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit end module Make(Ord: OrderedType) = struct @@ -152,7 +154,9 @@ module Make(Ord: OrderedType) = struct let prune roots cuts cg = let rs = reachable roots cuts cg in - fix_leaves (NM.filter (fun fn _ -> NS.mem fn rs) cg) + let cg = NM.filter (fun fn _ -> NS.mem fn rs) cg in + let cg = NM.mapi (fun fn children -> if NS.mem fn cuts then NS.empty else children) cg in + fix_leaves cg let remove_self_loops cg = NM.mapi (fun fn callees -> NS.remove fn callees) cg @@ -206,4 +210,19 @@ module Make(Ord: OrderedType) = struct in topsort' (); !list + let make_dot node_color edge_color string_of_node out_chan graph = + Util.opt_colors := false; + let to_string node = String.escaped (string_of_node node) in + output_string out_chan "digraph DEPS {\n"; + let make_node from_node = + output_string out_chan (Printf.sprintf " \"%s\" [fillcolor=%s;style=filled];\n" (to_string from_node) (node_color from_node)) + in + let make_line from_node to_node = + output_string out_chan (Printf.sprintf " \"%s\" -> \"%s\" [color=%s];\n" (to_string from_node) (to_string to_node) (edge_color from_node to_node)) + in + NM.bindings graph |> List.iter (fun (from_node, _) -> make_node from_node); + NM.bindings graph |> List.iter (fun (from_node, to_nodes) -> NS.iter (make_line from_node) to_nodes); + output_string out_chan "}\n"; + Util.opt_colors := true; + end diff --git a/src/graph.mli b/src/graph.mli index 11ea63dc..09b78304 100644 --- a/src/graph.mli +++ b/src/graph.mli @@ -90,9 +90,11 @@ module type S = (** Topologically sort a graph. Throws Not_a_DAG if the graph is not directed acyclic. *) val topsort : graph -> node list + + val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit end module Make(Ord: OrderedType) : S with type node = Ord.t and type node_set = Set.Make(Ord).t - and type graph = Set.Make(Ord).t Map.Make(Ord).t + and type graph = Set.Make(Ord).t Map.Make(Ord).t diff --git a/src/slice.ml b/src/slice.ml new file mode 100644 index 00000000..cbf8ee5d --- /dev/null +++ b/src/slice.ml @@ -0,0 +1,194 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Rewriter + +type node = + (* In the graph we have a node Register that represents the actual + register, but functions get only get transitive dependencies on + that through Register_read, Register_write, and Register_ref + nodes. *) + | Register of id + | Function of id + | Letbind of id + | Type of id + | Overload of id + +let node_id = function + | Register id -> id + | Function id -> id + | Letbind id -> id + | Type id -> id + | Overload id -> id + +let node_kind = function + | Register _ -> 0 + | Function _ -> 1 + | Letbind _ -> 3 + | Type _ -> 4 + | Overload _ -> 5 + +module Node = struct + type t = node + let compare n1 n2 = + let lex_ord c1 c2 = if c1 = 0 then c2 else c1 in + lex_ord (compare (node_kind n1) (node_kind n2)) (Id.compare (node_id n1) (node_id n2)) +end + +let node_color cuts = + let module NodeSet = Set.Make(Node) in + function + | node when NodeSet.mem node cuts -> "red" + | Register _ -> "lightpink" + | Function _ -> "white" + | Letbind _ -> "yellow" + | Type _ -> "springgreen" + | Overload _ -> "peachpuff" + +let node_string n = node_id n |> string_of_id |> String.escaped + +let edge_color from_node to_node = "black" + +let builtins = + let open Type_check in + IdSet.of_list (List.map fst (Bindings.bindings Env.builtin_typs)) + +let typ_ids typ = + let rec typ_ids (Typ_aux (aux, _)) = + match aux with + | Typ_var _ | Typ_internal_unknown -> IdSet.empty + | Typ_id id -> IdSet.singleton id + | Typ_app (id, typs) -> + IdSet.add id (List.fold_left IdSet.union IdSet.empty (List.map typ_arg_ids typs)) + | Typ_fn (typs, typ, _) -> + IdSet.union (typ_ids typ) (List.fold_left IdSet.union IdSet.empty (List.map typ_ids typs)) + | Typ_bidir (typ1, typ2) -> + IdSet.union (typ_ids typ1) (typ_ids typ2) + | Typ_tup typs -> + List.fold_left IdSet.union IdSet.empty (List.map typ_ids typs) + | Typ_exist (_, _, typ) -> typ_ids typ + and typ_arg_ids (A_aux (aux, _)) = + match aux with + | A_typ typ -> typ_ids typ + | _ -> IdSet.empty + in + IdSet.diff (typ_ids typ) builtins + +let add_def_to_graph graph def = + let open Type_check in + let module G = Graph.Make(Node) in + let graph = ref graph in + + let scan_exp self e_aux annot = + let env = env_of_annot annot in + begin match e_aux with + | E_id id -> + begin match Env.lookup_id id env with + | Register _ -> graph := G.add_edge self (Register id) !graph + | _ -> + if IdSet.mem id (Env.get_toplevel_lets env) then + graph := G.add_edge self (Letbind id) !graph + else () + end + | E_app (id, _) -> + graph := G.add_edge self (Function id) !graph + | E_ref id -> + graph := G.add_edge self (Register id) !graph + | E_cast (typ, _) -> + IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ) + | _ -> () + end; + E_aux (e_aux, annot) + in + let rw_exp self = { id_exp_alg with e_aux = (fun (e_aux, annot) -> scan_exp self e_aux annot) } in + + let rewriters self = + { rewriters_base with + rewrite_exp = (fun _ -> fold_exp (rw_exp self)); + rewrite_let = (fun _ -> fold_letbind (rw_exp self)); + } + in + + begin match def with + | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _, _), _)) -> + graph := G.add_edges (Function id) [] !graph; + IdSet.iter (fun typ_id -> graph := G.add_edge (Function id) (Type typ_id) !graph) (typ_ids typ) + | DEF_fundef fdef -> + let id = id_of_fundef fdef in + graph := G.add_edges (Function id) [] !graph; + ignore (rewrite_fun (rewriters (Function id)) fdef) + | DEF_val (LB_aux (LB_val (pat, exp), _) as lb) -> + let ids = pat_ids pat in + IdSet.iter (fun id -> graph := G.add_edges (Letbind id) [] !graph) ids; + IdSet.iter (fun id -> ignore (rewrite_let (rewriters (Letbind id)) lb)) ids + | _ -> () + end; + !graph + +let rec graph_of_ast (Defs defs) = + let module G = Graph.Make(Node) in + + match defs with + | def :: defs -> + let g = graph_of_ast (Defs defs) in + add_def_to_graph g def + + | [] -> G.empty + +let dot_of_ast ast = + let module G = Graph.Make(Node) in + let module NodeSet = Set.Make(Node) in + let g = graph_of_ast ast in + let roots = NodeSet.of_list (List.map (fun str -> Function (mk_id str)) ["execute_CGetPerm"; "execute_CSeal"]) in + let cuts = NodeSet.of_list (List.map (fun str -> Function (mk_id str)) ["readCapReg"; "writeCapReg"; "rGPR"; "wGPR"; "SignalException"]) in + let g = G.prune roots cuts g in + G.make_dot (node_color cuts) edge_color node_string stdout g diff --git a/src/type_check.ml b/src/type_check.ml index 02339842..5bc3cc2d 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -105,6 +105,7 @@ type env = { top_val_specs : (typquant * typ) Bindings.t; defined_val_specs : IdSet.t; locals : (mut * typ) Bindings.t; + top_letbinds : IdSet.t; union_ids : (typquant * typ) Bindings.t; registers : (effect * effect * typ) Bindings.t; variants : (typquant * type_union list) Bindings.t; @@ -409,6 +410,8 @@ module Env : sig val get_accessor : id -> id -> t -> typquant * typ * typ * effect val add_local : id -> mut * typ -> t -> t val get_locals : t -> (mut * typ) Bindings.t + val add_toplevel_lets : IdSet.t -> t -> t + val get_toplevel_lets : t -> IdSet.t val add_variant : id -> typquant * type_union list -> t -> t val add_scattered_variant : id -> typquant -> t -> t val add_variant_clause : id -> type_union -> t -> t @@ -488,6 +491,7 @@ end = struct { top_val_specs = Bindings.empty; defined_val_specs = IdSet.empty; locals = Bindings.empty; + top_letbinds = IdSet.empty; union_ids = Bindings.empty; registers = Bindings.empty; variants = Bindings.empty; @@ -1059,15 +1063,19 @@ end = struct | Mutable -> "ref<" ^ string_of_typ typ ^ ">" let add_local id mtyp env = - begin - if not env.allow_bindings then typ_error env (id_loc id) "Bindings are not allowed in this context" else (); - wf_typ env (snd mtyp); - if Bindings.mem id env.top_val_specs then - typ_error env (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name") - else (); - typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp)); - { env with locals = Bindings.add id mtyp env.locals } - end + if not env.allow_bindings then typ_error env (id_loc id) "Bindings are not allowed in this context" else (); + wf_typ env (snd mtyp); + if Bindings.mem id env.top_val_specs then + typ_error env (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name") + else (); + typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp)); + { env with locals = Bindings.add id mtyp env.locals; + top_letbinds = IdSet.remove id env.top_letbinds } + + let add_toplevel_lets ids env = + { env with top_letbinds = IdSet.union ids env.top_letbinds } + + let get_toplevel_lets env = env.top_letbinds let add_variant id variant env = typ_print (lazy (adding ^ "variant " ^ string_of_id id)); @@ -4560,14 +4568,14 @@ let check_letdef orig_env (LB_aux (letbind, (l, _))) = let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) typ_annot in if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects) then - [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], env + [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], Env.add_toplevel_lets (pat_ids tpat) env else typ_error env l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind)) | LB_val (pat, bind) -> let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) (typ_of inferred_bind) in if (BESet.is_empty (effect_set (effect_of inferred_bind)) || !opt_no_effects) then - [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env + [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], Env.add_toplevel_lets (pat_ids tpat) env else typ_error env l ("Top-level definition with effects " ^ string_of_effect (effect_of inferred_bind)) end diff --git a/src/type_check.mli b/src/type_check.mli index cfdfa2c6..15110b37 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -171,6 +171,8 @@ module Env : sig up the type without any flow typing modifiers. *) val lookup_id : ?raw:bool -> id -> t -> typ lvar + val get_toplevel_lets : t -> IdSet.t + val is_union_constructor : id -> t -> bool (** Check if the id is both a constructor, and the only constructor of that @@ -189,7 +191,7 @@ module Env : sig val expand_constraint_synonyms : t -> n_constraint -> n_constraint val expand_nexp_synonyms : t -> nexp -> nexp - + val expand_synonyms : t -> typ -> typ (** Expand type synonyms and remove register annotations (i.e. register -> t)) *) -- cgit v1.2.3 From 9ed89583d52ccff151fb75424975f2ac4e627a1b Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 4 Mar 2019 14:14:17 +0000 Subject: Add location to warning in pattern completeness check --- src/pattern_completeness.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml index 514eb5c0..79fc93ee 100644 --- a/src/pattern_completeness.ml +++ b/src/pattern_completeness.ml @@ -89,7 +89,7 @@ let is_wild = function | GP_wild -> true | _ -> false -let rec generalize ctx (P_aux (p_aux, _) as pat) = +let rec generalize ctx (P_aux (p_aux, (l, _)) as pat) = match p_aux with | P_lit (L_aux (L_unit, _)) -> (* Unit pattern always matches on unit, so generalize to wildcard *) @@ -105,7 +105,8 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) = match ctx.lookup_id id with | Unbound -> GP_wild | Local (Immutable, _) -> GP_wild - | Register _ | Local (Mutable, _) -> Util.warn "Matching on register or mutable variable"; GP_wild + | Register _ | Local (Mutable, _) -> + Util.warn ("Matching on register or mutable variable at " ^ Reporting.loc_to_string l); GP_wild | Enum _ -> GP_app (Bindings.singleton id GP_wild) end | P_var (pat, _) -> generalize ctx pat -- cgit v1.2.3