From ac945514d59d91e51a63149b39b472421e59e299 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Sat, 29 Dec 2018 14:00:40 +0000 Subject: Add separate termination_measure declarations --- src/initial_check.ml | 2 ++ src/lexer.mll | 1 + src/parse_ast.ml | 1 + src/parser.mly | 4 +++- src/pretty_print_sail.ml | 3 +++ src/rewriter.ml | 1 + src/rewrites.ml | 31 +++++++++++++++++++++++++++++++ src/type_check.ml | 21 ++++++++++++++++++--- 8 files changed, 60 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/initial_check.ml b/src/initial_check.ml index 17b4b515..78314363 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -743,6 +743,8 @@ let to_ast_def ctx def : unit def ctx_out = | P.DEF_scattered sdef -> let sdef, ctx = to_ast_scattered ctx sdef in DEF_scattered sdef, ctx + | P.DEF_measure (id, pat, exp) -> + DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp), ctx let rec remove_mutrec = function | [] -> [] diff --git a/src/lexer.mll b/src/lexer.mll index 57580e7a..1d48b82b 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -182,6 +182,7 @@ let kw_table = ("nondet", (fun x -> Nondet)); ("escape", (fun x -> Escape)); ("configuration", (fun _ -> Configuration)); + ("termination_measure", (fun _ -> TerminationMeasure)); ] diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 65b11373..20a0f48a 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -531,6 +531,7 @@ def = (* Top-level definition *) | DEF_spec of val_spec (* top-level type constraint *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) + | DEF_measure of id * pat * exp (* separate termination measure declaration *) | DEF_reg_dec of dec_spec (* register declaration *) | DEF_pragma of string * string * l | DEF_internal_mutrec of fundef list diff --git a/src/parser.mly b/src/parser.mly index 66902953..3ad0931a 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -183,7 +183,7 @@ let rec desugar_rchain chain s e = %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Constant Constraint Throw Try Catch Exit Bitfield %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token Repeat Until While Do Mutual Var Ref Configuration +%token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure %nonassoc Then %nonassoc Else @@ -1430,6 +1430,8 @@ def: { DEF_internal_mutrec $3 } | Pragma { DEF_pragma (fst $1, snd $1, loc $startpos $endpos) } + | TerminationMeasure id pat Eq exp + { DEF_measure ($2, $3, $5) } defs_list: | def diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 345312f7..d5758303 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -662,6 +662,9 @@ let rec doc_def def = group (match def with ^^ hardline ^^ string "}" | DEF_reg_dec dec -> doc_dec dec | DEF_scattered sdef -> doc_scattered sdef + | DEF_measure (id,pat,exp) -> + string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_pat pat ^^ + space ^^ equals ^/^ doc_exp exp | DEF_pragma (pragma, arg, l) -> string ("$" ^ pragma ^ " " ^ arg) | DEF_fixity (prec, n, id) -> diff --git a/src/rewriter.ml b/src/rewriter.ml index a70f6fab..21310b91 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -364,6 +364,7 @@ let rewrite_def rewriters d = match d with | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind) | DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l) | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter") + | DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp) let rewrite_defs_base rewriters (Defs defs) = let rec rewrite ds = match ds with diff --git a/src/rewrites.ml b/src/rewrites.ml index 0ad4c56e..8d53ea54 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4763,6 +4763,35 @@ let minimise_recursive_functions (Defs defs) = | d -> d in Defs (List.map rewrite_def defs) +let move_termination_measures (Defs defs) = + let scan_for id defs = + let rec aux = function + | [] -> None + | (DEF_measure (id',pat,exp))::t -> + if Id.compare id id' == 0 then Some (pat,exp) else aux t + | (DEF_fundef (FD_aux (FD_function (_,_,_,FCL_aux (FCL_Funcl (id',_),_)::_),_)))::_ + | (DEF_spec (VS_aux (VS_val_spec (_,id',_,_),_))::_) + when Id.compare id id' == 0 -> None + | _::t -> aux t + in aux defs + in + let rec aux acc = function + | [] -> List.rev acc + | (DEF_fundef (FD_aux (FD_function (r,ty,e,fs),(l,f_ann))) as d)::t -> begin + let id = match fs with + | [] -> assert false (* TODO *) + | (FCL_aux (FCL_Funcl (id,_),_))::_ -> id + in + match scan_for id t with + | None -> aux (d::acc) t + | Some (pat,exp) -> + let r = Rec_aux (Rec_measure (pat,exp), Generated l) in + aux (DEF_fundef (FD_aux (FD_function (r,ty,e,fs),(l,f_ann)))::acc) t + end + | (DEF_measure _)::t -> aux acc t + | h::t -> aux (h::acc) t + in Defs (aux [] defs) + (* Make recursive functions with a measure use the measure as an explicit recursion limit, enforced by an assertion. *) let rewrite_explicit_measure (Defs defs) = @@ -4881,6 +4910,7 @@ let rewrite_explicit_measure (Defs defs) = | [wpat] -> wpat | _ -> P_aux (P_tup wpats,(loc,empty_tannot)) in + let measure_exp = E_aux (E_cast (int_typ, measure_exp),(loc,empty_tannot)) in let wbody = E_aux (E_app (rec_id id,wexps@[measure_exp]),(loc,empty_tannot)) in let wrapper = FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (wpat,wbody),(loc,empty_tannot))),(loc,empty_tannot)) @@ -5008,6 +5038,7 @@ let rewrite_defs_coq = [ ("toplevel_string_append", rewrite_defs_toplevel_string_append); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); + ("move_termination_measures", move_termination_measures); ("rewrite_undefined", rewrite_undefined_if_gen true); ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list); ("remove_not_pats", rewrite_defs_not_pats); diff --git a/src/type_check.ml b/src/type_check.ml index 53d87a05..ee80296f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4158,6 +4158,22 @@ let check_tannotopt env typq ret_typ = function then () else typ_error l (string_of_bind (typq, ret_typ) ^ " and " ^ string_of_bind (annot_typq, annot_ret_typ) ^ " do not match between function and val spec") +let check_termination_measure env arg_typs pat exp = + let typ = match arg_typs with [x] -> x | _ -> Typ_aux (Typ_tup arg_typs,Unknown) in + let tpat, env = bind_pat_no_guard env (strip_pat pat) typ in + let texp = check_exp env (strip_exp exp) int_typ in + tpat, texp + +let check_termination_measure_decl env (id, pat, exp) = + let quant, typ = Env.get_val_spec id env in + let arg_typs, l = match typ with + | Typ_aux (Typ_fn (arg_typs, _ ,_),l) -> arg_typs,l + | _ -> typ_error (id_loc id) "Function val spec is not a function type" + in + let env = add_typquant l quant env in + let tpat, texp = check_termination_measure env arg_typs pat exp in + DEF_measure (id, tpat, texp) + let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, _)) as fd_aux) = let id = match (List.fold_right @@ -4190,9 +4206,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) | Rec_aux (Rec_nonrec, l) -> Rec_aux (Rec_nonrec, l) | Rec_aux (Rec_rec, l) -> Rec_aux (Rec_rec, l) | Rec_aux (Rec_measure (measure_p, measure_e), l) -> - let typ = match vtyp_args with [x] -> x | _ -> Typ_aux (Typ_tup vtyp_args,Unknown) in - let tpat, env = bind_pat_no_guard funcl_env (strip_pat measure_p) typ in - let texp = check_exp env (strip_exp measure_e) int_typ in + let tpat, texp = check_termination_measure funcl_env vtyp_args measure_p measure_e in Rec_aux (Rec_measure (tpat, texp), l) in let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in @@ -4439,6 +4453,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err () | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err () | DEF_scattered sdef -> check_scattered env sdef + | DEF_measure (id, pat, exp) -> [check_termination_measure_decl env (id, pat, exp)], env and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = fun env (Defs defs) -> -- cgit v1.2.3 From 771f041a48f611a4869a7a19fa39672581b5ba9a Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Sat, 29 Dec 2018 14:59:09 +0000 Subject: Coq: ensure that recursive functions compute --- 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 09c6cafc..08844eb5 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1296,7 +1296,7 @@ let doc_exp, doc_let = [parens (string "_limit_reduces _acc")] else match f with | Id_aux (Id x,_) when is_prefix "#rec#" x -> - main_call @ [parens (string "Zwf_well_founded _ _")] + main_call @ [parens (string "Zwf_guarded _")] | _ -> main_call in hang 2 (flow (break 1) all) in -- cgit v1.2.3 From 269fdb0ed57814f3fbb41b206a67a3cc7bafc810 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Sun, 30 Dec 2018 14:06:20 +0000 Subject: Sort dependencies of termination measures properly --- src/rewrites.ml | 2 +- src/spec_analysis.ml | 15 ++++++++++++--- 2 files changed, 13 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index 8d53ea54..afbba659 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5038,7 +5038,6 @@ let rewrite_defs_coq = [ ("toplevel_string_append", rewrite_defs_toplevel_string_append); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); - ("move_termination_measures", move_termination_measures); ("rewrite_undefined", rewrite_undefined_if_gen true); ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list); ("remove_not_pats", rewrite_defs_not_pats); @@ -5060,6 +5059,7 @@ let rewrite_defs_coq = [ ("exp_lift_assign", rewrite_defs_exp_lift_assign); (* ("constraint", rewrite_constraint); *) (* ("remove_assert", rewrite_defs_remove_assert); *) + ("move_termination_measures", move_termination_measures); ("top_sort_defs", top_sort_defs); ("trivial_sizeof", rewrite_trivial_sizeof); ("sizeof", rewrite_sizeof); diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 940fbfe5..398f20b5 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -356,9 +356,10 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_) | [] -> failwith "fv_of_fun fell off the end looking for the function name" | FCL_aux(FCL_Funcl(id,_),_)::_ -> string_of_id id in let base_bounds = match rec_opt with - (* Current Sail does not have syntax for declaring functions as recursive, + (* Current Sail does not require syntax for declaring functions as recursive, and type checker does not check whether functions are recursive, so - just always add a self-dependency of functions on themselves + just always add a self-dependency of functions on themselves, as well as + adding dependencies from any specified termination measure further below | Rec_aux(Ast.Rec_rec,_) -> init_env fun_name | _ -> mt*) | _ -> init_env fun_name in @@ -369,6 +370,13 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_) bound, fv_of_typ consider_var bound mt typ | Typ_annot_opt_aux(Typ_annot_opt_none, _) -> base_bounds, mt in + let ns_measure = match rec_opt with + | Rec_aux(Rec_measure (pat,exp),_) -> + let pat_bs,pat_ns = pat_bindings consider_var base_bounds mt pat in + let _, exp_ns,_ = fv_of_exp consider_var pat_bs pat_ns Nameset.empty exp in + exp_ns + | _ -> mt + in let ns = List.fold_right (fun (FCL_aux(FCL_Funcl(_,pexp),_)) ns -> match pexp with | Pat_aux(Pat_exp (pat,exp),_) -> @@ -383,7 +391,7 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_) ) funcls mt in let ns_vs = init_env ("val:" ^ (string_of_id (id_of_fundef fd))) in (* let _ = Printf.eprintf "Function %s uses %s\n" fun_name (set_to_string (Nameset.union ns ns_r)) in *) - init_env fun_name, Nameset.union ns_vs (Nameset.union ns ns_r) + init_env fun_name, Nameset.union ns_vs (Nameset.union ns (Nameset.union ns_r ns_measure)) let fv_of_vspec consider_var (VS_aux(vspec,_)) = match vspec with | VS_val_spec(ts,id,_,_) -> @@ -499,6 +507,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef | DEF_reg_dec rdec -> fv_of_rd consider_var rdec | DEF_pragma _ -> mt,mt + | DEF_measure _ -> mt,mt (* currently removed beforehand *) let group_defs consider_scatter_as_one (Ast.Defs defs) = List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs -- cgit v1.2.3 From dccff374cc4ff0d2ac9737a1abd1907118af6456 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 31 Dec 2018 11:01:54 +0000 Subject: Coq: move function clause merging to keep measure argument intact --- src/rewrites.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index afbba659..3cd89b89 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5065,6 +5065,9 @@ let rewrite_defs_coq = [ ("sizeof", rewrite_sizeof); ("early_return", rewrite_defs_early_return); ("make_cases_exhaustive", MakeExhaustive.rewrite); + (* merge funcls before adding the measure argument so that it doesn't + disappear into an internal pattern match *) + ("merge function clauses", merge_funcls); ("rewrite_explicit_measure", rewrite_explicit_measure); ("recheck_defs_without_effects", recheck_defs_without_effects); ("fix_val_specs", rewrite_fix_val_specs); @@ -5074,7 +5077,6 @@ let rewrite_defs_coq = [ ("internal_lets", rewrite_defs_internal_lets); ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds); ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns); - ("merge function clauses", merge_funcls); ("recheck_defs", recheck_defs) ] -- cgit v1.2.3 From 534e02c863b5a571c6d8bd65cf72a4ce92fe4701 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 31 Dec 2018 19:58:32 +0000 Subject: Last rewrite reordering needs more typechecking --- src/rewrites.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index 3cd89b89..7ccff222 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5064,10 +5064,11 @@ let rewrite_defs_coq = [ ("trivial_sizeof", rewrite_trivial_sizeof); ("sizeof", rewrite_sizeof); ("early_return", rewrite_defs_early_return); - ("make_cases_exhaustive", MakeExhaustive.rewrite); (* merge funcls before adding the measure argument so that it doesn't disappear into an internal pattern match *) ("merge function clauses", merge_funcls); + ("recheck_defs", recheck_defs); + ("make_cases_exhaustive", MakeExhaustive.rewrite); ("rewrite_explicit_measure", rewrite_explicit_measure); ("recheck_defs_without_effects", recheck_defs_without_effects); ("fix_val_specs", rewrite_fix_val_specs); -- cgit v1.2.3 From 5aa29f88c1e31bb9435929f86325f499dccf6d50 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 2 Jan 2019 20:22:35 +0000 Subject: Coq: tweak recently introduced type check to ignore effects --- src/rewrites.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index 7ccff222..8894f2c8 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4835,8 +4835,8 @@ let rewrite_explicit_measure (Defs defs) = | exception Not_found -> [vs] in (* Add extra argument and assertion to each funcl, and rewrite recursive calls *) - let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),ann) as fcl) = - let loc = Parse_ast.Generated (fst ann) in + let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann) as fcl) = + let loc = Parse_ast.Generated (fst fcl_ann) in let P_aux (pat,pann),guard,body,ann = destruct_pexp pexp in let extra_pat = P_aux (P_id limit,(loc,empty_tannot)) in let pat = match pat with @@ -4868,7 +4868,7 @@ let rewrite_explicit_measure (Defs defs) = } body in let body = E_aux (E_block [assert_exp; body],(loc,empty_tannot)) in - FCL_aux (FCL_Funcl (rec_id id, construct_pexp (P_aux (pat,pann),guard,body,ann)),ann) + FCL_aux (FCL_Funcl (rec_id id, construct_pexp (P_aux (pat,pann),guard,body,ann)),fcl_ann) in let rewrite_function (FD_aux (FD_function (r,t,e,fcls),ann) as fd) = let loc = Parse_ast.Generated (fst ann) in @@ -5067,7 +5067,7 @@ let rewrite_defs_coq = [ (* merge funcls before adding the measure argument so that it doesn't disappear into an internal pattern match *) ("merge function clauses", merge_funcls); - ("recheck_defs", recheck_defs); + ("recheck_defs_without_effects", recheck_defs_without_effects); ("make_cases_exhaustive", MakeExhaustive.rewrite); ("rewrite_explicit_measure", rewrite_explicit_measure); ("recheck_defs_without_effects", recheck_defs_without_effects); -- cgit v1.2.3 From 7d33d9c1837149d31df06b803ed4dbf2ce4053ca Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 9 Jan 2019 11:02:13 +0000 Subject: Coq: add parens around negative integer literals --- 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 08844eb5..5cf17056 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -585,8 +585,9 @@ let doc_lit (L_aux(lit,l)) = | L_false -> utf8string "false" | L_true -> utf8string "true" | L_num i -> - let ipp = Big_int.to_string i in - utf8string ipp + let s = Big_int.to_string i in + let ipp = utf8string s in + if Big_int.less i Big_int.zero then parens ipp else ipp | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> -- cgit v1.2.3 From 1c80d84c47faef38149e87e000c6721f6aa6245e Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 9 Jan 2019 13:43:16 +0000 Subject: Coq: the division used in smt.sail should be Euclidean --- src/pretty_print_coq.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 5cf17056..20db317b 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -239,9 +239,9 @@ let doc_nexp ctx ?(skip_vars=KidSet.empty) nexp = and app (Nexp_aux (n,l) as nexp) = match n with | Nexp_app (Id_aux (Id "div",_), [n1;n2]) - -> separate space [string "Z.quot"; atomic n1; atomic n2] + -> separate space [string "ZEuclid.div"; atomic n1; atomic n2] | Nexp_app (Id_aux (Id "mod",_), [n1;n2]) - -> separate space [string "Z.rem"; atomic n1; atomic n2] + -> separate space [string "ZEuclid.modulo"; atomic n1; atomic n2] | Nexp_app (Id_aux (Id "abs_atom",_), [n1]) -> separate space [string "Z.abs"; atomic n1] | _ -> atomic nexp -- cgit v1.2.3 From a5e2b3b7411f630b6d2337402330e13862b5666a Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Mon, 14 Jan 2019 17:35:43 -0800 Subject: Add options for output directories for the lem and coq backends. --- src/process_file.ml | 48 ++++++++++++++++++++++++++++-------------------- src/process_file.mli | 3 +++ src/sail.ml | 6 ++++++ 3 files changed, 37 insertions(+), 20 deletions(-) (limited to 'src') diff --git a/src/process_file.ml b/src/process_file.ml index ca013077..38e60ff8 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -51,6 +51,9 @@ open PPrint open Pretty_print_common +let opt_lem_output_dir = ref None +let opt_coq_output_dir = ref None + type out_type = | Lem_out of string list | Coq_out of string list @@ -254,19 +257,24 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno (ast, env) -let open_output_with_check file_name = +let open_output_with_check opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in let o' = Format.formatter_of_out_channel o in - (o', (o, temp_file_name, file_name)) + (o', (o, temp_file_name, opt_dir, file_name)) -let open_output_with_check_unformatted file_name = +let open_output_with_check_unformatted opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in - (o, temp_file_name, file_name) + (o, temp_file_name, opt_dir, file_name) let always_replace_files = ref true -let close_output_with_check (o, temp_file_name, file_name) = +let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let _ = close_out o in + let file_name = match opt_dir with + | None -> file_name + | Some dir -> if Sys.file_exists dir then () + else Unix.mkdir dir 0o775; + Filename.concat dir file_name in let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in let _ = if (not do_replace) then Sys.remove temp_file_name else Util.move_file temp_file_name file_name in @@ -275,7 +283,7 @@ let close_output_with_check (o, temp_file_name, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f -let output_lem filename libs defs = +let output_lem opt_dir filename libs defs = let generated_line = generated_line filename in (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = (filename ^ "_types") in @@ -308,22 +316,22 @@ let output_lem filename libs defs = string "end" ] ^^ hardline in - let ((ot,_, _) as ext_ot) = - open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (filename ^ ".lem") in + let ((ot,_,_,_) as ext_ot) = + open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".lem") in + let ((o,_,_,_) as ext_o) = + open_output_with_check_unformatted opt_dir (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; - let ((ol, _, _) as ext_ol) = - open_output_with_check_unformatted (isa_thy_name ^ ".thy") in + let ((ol,_,_,_) as ext_ol) = + open_output_with_check_unformatted opt_dir (isa_thy_name ^ ".thy") in print ol isa_lemmas; close_output_with_check ext_ol -let output_coq filename libs defs = +let output_coq opt_dir filename libs defs = let generated_line = generated_line filename in let types_module = (filename ^ "_types") in let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_state"] in @@ -336,10 +344,10 @@ let output_coq filename libs defs = operators_module ] @ monad_modules in - let ((ot,_, _) as ext_ot) = - open_output_with_check_unformatted (filename ^ "_types" ^ ".v") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (filename ^ ".v") in + let ((ot,_,_,_) as ext_ot) = + open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in + let ((o,_,_,_) as ext_o) = + open_output_with_check_unformatted opt_dir (filename ^ ".v") in (Pretty_print_coq.pp_defs_coq (ot, base_imports) (o, base_imports @ (types_module :: libs)) @@ -355,9 +363,9 @@ let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem f' libs defs + output_lem !opt_lem_output_dir f' libs defs | Coq_out libs -> - output_coq f' libs defs + output_coq !opt_coq_output_dir f' libs defs let output libpath out_arg files = List.iter @@ -374,7 +382,7 @@ let rewrite_step defs (name, rewriter) = begin let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in (* output "" Lem_ast_out [filename, defs]; *) - let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in + let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted None filename in Pretty_print_sail.pp_defs ot defs; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) diff --git a/src/process_file.mli b/src/process_file.mli index 1d4d629a..2c4973bc 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -71,6 +71,9 @@ val opt_ddump_tc_ast : bool ref val opt_ddump_rewrite_ast : ((string * int) option) ref val opt_dno_cast : bool ref +val opt_lem_output_dir : (string option) ref +val opt_coq_output_dir : (string option) ref + type out_type = | Lem_out of string list (* If present, the strings are files to open in the lem backend*) | Coq_out of string list (* If present, the strings are files to open in the coq backend*) diff --git a/src/sail.ml b/src/sail.ml index 59190d15..3e89f39d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -150,6 +150,9 @@ let options = Arg.align ([ ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); + ( "-lem_output_dir", + Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), + " set a custom directory to output generated Lem"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), " provide additional library to open in Lem output"); @@ -162,6 +165,9 @@ let options = Arg.align ([ ( "-coq", Arg.Set opt_print_coq, " output a Coq translated version of the input"); + ( "-coq_output_dir", + Arg.String (fun dir -> Process_file.opt_coq_output_dir := Some dir), + " set a custom directory to output generated Coq"); ( "-coq_lib", Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), " provide additional library to open in Coq output"); -- cgit v1.2.3 From bb231219ff3d2d498d6f23f71ec1966dd58a304c Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Wed, 16 Jan 2019 15:15:40 -0800 Subject: Latex: handle underscores when generating latex names. --- src/latex.ml | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index 2f578f2c..56ba29ef 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -102,8 +102,7 @@ type id_category = | FunclNum of int | FunclApp of string -let replace_numbers str = - let replacements = +let number_replacements = [ ("0", "Zero"); ("1", "One"); ("2", "Two"); @@ -114,16 +113,27 @@ let replace_numbers str = ("7", "Seven"); ("8", "Eight"); ("9", "Nine") ] - in + +(* add to this as needed *) +let other_replacements = + [ ("_", "Underscore") ] + +let char_replace str replacements = List.fold_left (fun str (from, into) -> Str.global_replace (Str.regexp_string from) into str) str replacements +let replace_numbers str = + char_replace str number_replacements + +let replace_others str = + char_replace str other_replacements + let category_name = function | Function -> "fn" | Val -> "val" | Overload -> "overload" | FunclNum n -> "fcl" ^ unique_postfix n | FunclCtor (id, n) -> - let str = replace_numbers (Util.zencode_string (string_of_id id)) in + let str = replace_others (replace_numbers (Util.zencode_string (string_of_id id))) in "fcl" ^ String.sub str 1 (String.length str - 1) ^ unique_postfix n | FunclApp str -> "fcl" ^ str @@ -162,8 +172,8 @@ let latex_id id = (* If we have any other weird symbols in the id, remove them using Util.zencode_string (removing the z prefix) *) let str = Util.zencode_string str in let str = String.sub str 1 (String.length str - 1) in - (* Latex only allows letters in identifiers, so replace all numbers *) - let str = replace_numbers str in + (* Latex only allows letters in identifiers, so replace all numbers and other characters *) + let str = replace_others (replace_numbers str) in let generated = state.generated_names |> Bindings.bindings |> List.map snd |> StringSet.of_list in -- cgit v1.2.3 From 3797f0a21c142b37c6ce0728f60b231f2230c4f0 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 21 Jan 2019 14:25:56 +0000 Subject: Fix a bug with type-checking and latex generation We should maybe just make the -latex option behavior the default to avoid this kind of thing --- src/type_check.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index ee80296f..b3c691fb 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4272,14 +4272,18 @@ let check_val_spec env (VS_aux (vs, (l, _))) = typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); let env = Env.add_extern id ext_opt env in let env = if is_cast then Env.add_cast id env else env in + let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in + (* !opt_expand_valspec controls whether the actual valspec in + the AST is expanded, the val_spec type stored in the + environment is always expanded and uses typq' and typ' *) let typq, typ = if !opt_expand_valspec then - expand_bind_synonyms ts_l env (typq, typ) + (typq', typ') else (typq, typ) in let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in - (vs, id, typq, typ, env) + (vs, id, typq', typ', env) in let eff = match typ with -- cgit v1.2.3 From d2d7321afb0112142966c44a8dc4719851f20035 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 21 Jan 2019 16:19:20 +0000 Subject: Fix some issues with latex generation so manual builds again since riscv is no longer in this repository, and we use the RISC-V duopod as an example, you need to build as: make RISCV=directory manual.pdf if directory is not equal to ../../sail-riscv (which is where it would be if sail and sail-riscv are checked out in the same respository together) --- src/latex.ml | 55 +++++++++++++++++++++++++++++++++++++++---------------- src/sail.ml | 3 +++ 2 files changed, 42 insertions(+), 16 deletions(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index 56ba29ef..71e0ba54 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -57,6 +57,7 @@ module StringSet = Set.Make(String);; let opt_prefix = ref "sail" let opt_directory = ref "sail_latex" +let opt_simple_val = ref true let rec unique_postfix n = if n < 0 then @@ -97,10 +98,11 @@ let rec unique_postfix n = type id_category = | Function | Val - | Overload + | Overload of int | FunclCtor of id * int | FunclNum of int | FunclApp of string + | Type let number_replacements = [ ("0", "Zero"); @@ -130,7 +132,8 @@ let replace_others str = let category_name = function | Function -> "fn" | Val -> "val" - | Overload -> "overload" + | Type -> "type" + | Overload n -> "overload" ^ unique_postfix n | FunclNum n -> "fcl" ^ unique_postfix n | FunclCtor (id, n) -> let str = replace_others (replace_numbers (Util.zencode_string (string_of_id id))) in @@ -144,7 +147,8 @@ let category_name_val = function let category_name_simple = function | Function -> "fn" | Val -> "val" - | Overload -> "overload" + | Type -> "type" + | Overload n -> "overload" | FunclNum _ -> "fcl" | FunclCtor (_, _) -> "fcl" | FunclApp _ -> "fcl" @@ -300,10 +304,10 @@ let latex_loc no_loc l = let commands = ref StringSet.empty -let doc_spec_simple (VS_val_spec(ts,id,ext,is_cast)) = - Pretty_print_sail.doc_id id ^^ space - ^^ colon ^^ space - ^^ Pretty_print_sail.doc_typschm ~simple:true ts +let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) = + Pretty_print_sail.doc_id id ^^ space + ^^ colon ^^ space + ^^ Pretty_print_sail.doc_typschm ~simple:true ts let rec latex_command cat id no_loc ((l, _) as annot) = state.this <- Some id; @@ -319,7 +323,7 @@ let rec latex_command cat id no_loc ((l, _) as annot) = output_string chan (Pretty_print_sail.to_string doc); close_out chan; - ksprintf string "\\newcommand{\\sail%s%s}{\\phantomsection%s\\saildoc%s{" (category_name cat) (latex_id id) labelling (category_name_simple cat) + ksprintf string "\\newcommand{\\%s%s%s}{\\phantomsection%s\\saildoc%s{" !opt_prefix (category_name cat) (latex_id id) labelling (category_name_simple cat) ^^ docstring l ^^ string "}{" ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file) @@ -391,30 +395,47 @@ let process_pragma l command = Util.warn (Printf.sprintf "Bad latex pragma %s" (Reporting.loc_to_string l)); None +let tdef_id = function + | TD_abbrev (id, _, _) -> id + | TD_record (id, _, _, _, _) -> id + | TD_variant (id, _, _, _, _) -> id + | TD_enum (id, _, _, _) -> id + | TD_bitfield (id, _, _) -> id + let defs (Defs defs) = reset_state state; + let overload_counter = ref 0 in + let valspecs = ref IdSet.empty in let fundefs = ref IdSet.empty in + let typedefs = ref IdSet.empty in let latex_def def = match def with - | DEF_overload (id, ids) -> None - (* + | DEF_overload (id, ids) -> let doc = string (Printf.sprintf "overload %s = {%s}" (string_of_id id) (Util.string_of_list ", " string_of_id ids)) in - Some (latex_command Overload id doc (id_loc id, None)) - *) + incr overload_counter; + Some (latex_command (Overload !overload_counter) id doc (id_loc id, None)) - | DEF_spec (VS_aux (VS_val_spec (_, id, _, _) as vs, annot)) as def -> + | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), annot) as vs) as def -> valspecs := IdSet.add id !valspecs; - Some (latex_command Val id (doc_spec_simple vs) annot) + if !opt_simple_val then + Some (latex_command Val id (doc_spec_simple vs) annot) + else + Some (latex_command Val id (Pretty_print_sail.doc_spec ~comment:false vs) annot) | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), annot)) as def -> fundefs := IdSet.add id !fundefs; Some (latex_command Function id (Pretty_print_sail.doc_def def) annot) + | DEF_type (TD_aux (tdef, annot)) as def -> + let id = tdef_id tdef in + typedefs := IdSet.add id !typedefs; + Some (latex_command Type id (Pretty_print_sail.doc_def def) annot) + | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) as def -> Some (latex_funcls def funcls) @@ -442,7 +463,7 @@ let defs (Defs defs) = identifiers then outputs the correct mangled command. *) let id_command cat ids = sprintf "\\newcommand{\\%s%s}[1]{\n " !opt_prefix (category_name cat) - ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\sail%s%s}{}" (string_of_id id) (category_name cat) (latex_id id)) + ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s%s%s}{}" (string_of_id id) !opt_prefix (category_name cat) (latex_id id)) (IdSet.elements ids) ^ "}" |> string @@ -459,5 +480,7 @@ let defs (Defs defs) = ^^ separate (twice hardline) [id_command Val !valspecs; ref_command Val !valspecs; id_command Function !fundefs; - ref_command Function !fundefs] + ref_command Function !fundefs; + id_command Type !typedefs; + ref_command Type !typedefs] ^^ hardline diff --git a/src/sail.ml b/src/sail.ml index 3e89f39d..a5cac041 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -112,6 +112,9 @@ let options = Arg.align ([ ( "-latex", Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ], " pretty print the input to latex"); + ( "-latex_full_valspecs", + Arg.Clear Latex.opt_simple_val, + " print full valspecs in latex output latex"); ( "-c", Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); -- cgit v1.2.3 From d34329753b1e8faa32a7c95ac085733555c16749 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 18:37:24 +0000 Subject: Add output directory option for generated Isabelle auxiliary theories --- src/process_file.ml | 11 ++++++----- src/process_file.mli | 1 + src/sail.ml | 3 +++ 3 files changed, 10 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/process_file.ml b/src/process_file.ml index 38e60ff8..094b0ecb 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -52,6 +52,7 @@ open PPrint open Pretty_print_common let opt_lem_output_dir = ref None +let opt_isa_output_dir = ref None let opt_coq_output_dir = ref None type out_type = @@ -283,7 +284,7 @@ let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f -let output_lem opt_dir filename libs defs = +let output_lem filename libs defs = let generated_line = generated_line filename in (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = (filename ^ "_types") in @@ -317,9 +318,9 @@ let output_lem opt_dir filename libs defs = ] ^^ hardline in let ((ot,_,_,_) as ext_ot) = - open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".lem") in + open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in let ((o,_,_,_) as ext_o) = - open_output_with_check_unformatted opt_dir (filename ^ ".lem") in + open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) @@ -327,7 +328,7 @@ let output_lem opt_dir filename libs defs = close_output_with_check ext_ot; close_output_with_check ext_o; let ((ol,_,_,_) as ext_ol) = - open_output_with_check_unformatted opt_dir (isa_thy_name ^ ".thy") in + open_output_with_check_unformatted !opt_isa_output_dir (isa_thy_name ^ ".thy") in print ol isa_lemmas; close_output_with_check ext_ol @@ -363,7 +364,7 @@ let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem !opt_lem_output_dir f' libs defs + output_lem f' libs defs | Coq_out libs -> output_coq !opt_coq_output_dir f' libs defs diff --git a/src/process_file.mli b/src/process_file.mli index 2c4973bc..e209c829 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -72,6 +72,7 @@ val opt_ddump_rewrite_ast : ((string * int) option) ref val opt_dno_cast : bool ref val opt_lem_output_dir : (string option) ref +val opt_isa_output_dir : (string option) ref val opt_coq_output_dir : (string option) ref type out_type = diff --git a/src/sail.ml b/src/sail.ml index a5cac041..920542bc 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -156,6 +156,9 @@ let options = Arg.align ([ ( "-lem_output_dir", Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), " set a custom directory to output generated Lem"); + ( "-isa_output_dir", + Arg.String (fun dir -> Process_file.opt_isa_output_dir := Some dir), + " set a custom directory to output generated Isabelle auxiliary theories"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), " provide additional library to open in Lem output"); -- cgit v1.2.3 From 2c81fff611c458fe04b2de2045247bdc77f8f80a Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 21 Jan 2019 19:02:46 +0000 Subject: Update manual snapshot and add basic sail -latex documentation --- src/type_check.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index b3c691fb..1b6efa46 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1243,7 +1243,7 @@ let prove_z3 env (NC_aux (_, l) as nc) = | Constraint.Sat -> typ_debug (lazy "sat"); false | Constraint.Unknown -> typ_debug (lazy "unknown"); false -let solve env (Nexp_aux (_, l) as nexp) = +let solve env (Nexp_aux (_, l) as nexp) = typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_nexp nexp ^ " = ?")); match nexp with @@ -1255,6 +1255,8 @@ let solve env (Nexp_aux (_, l) as nexp) = let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in Constraint.solve_z3 l vars constr (mk_kid "solve#") + + let prove env nc = typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); let (NC_aux (nc_aux, _) as nc) = Env.expand_constraint_synonyms env nc in -- cgit v1.2.3 From 63a3cdcd18972cdc2b6fa24d6a2deb5cae7549cc Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 22 Jan 2019 03:08:46 +0000 Subject: Make sure we optimize constrained union constructors --- src/c_backend.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index 65702764..f02cdb9c 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -1399,9 +1399,11 @@ let compile_type_def ctx (TD_aux (type_def, _)) = CTD_struct (id, Bindings.bindings ctors), { ctx with records = Bindings.add id ctors ctx.records } - | TD_variant (id, _, _, tus, _) -> + | TD_variant (id, _, typq, tus, _) -> let compile_tu = function - | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id + | Tu_aux (Tu_ty_id (typ, id), _) -> + let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in + ctyp_of_typ ctx typ, id in let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in CTD_variant (id, Bindings.bindings ctus), -- cgit v1.2.3 From 8c457ba46217978c1845ae9d6ebb0970e9b30cb9 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 22 Jan 2019 13:22:30 +0000 Subject: Make sure there is an ocaml representation for optimized memory read for RISC-V --- src/sail_lib.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src') diff --git a/src/sail_lib.ml b/src/sail_lib.ml index c0bf80fa..d1a21b73 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -508,6 +508,13 @@ let read_ram (addr_size, data_size, hex_ram, addr) = Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes; !vector +let fast_read_ram (data_size, addr) = + let addr = uint addr in + let bytes = read_mem_bytes addr (Big_int.to_int data_size) in + let vector = ref [] in + Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes; + !vector + let tag_ram = (ref Mem.empty : (bool Mem.t) ref);; let write_tag_bool (addr, tag) = -- cgit v1.2.3 From 8258b81bf1485e3133fb4351413ed1f554717f43 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 22 Jan 2019 18:04:16 +0000 Subject: Add a pragma for unrolling recursive functions For example in RISC-V for the translation table walk: $optimize unroll 2 val walk32 ... function walk32 ... would create two extra copies of the walk_32 function, walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2 being recursive. Currently we only support the case where we have $optimize unroll, directly followed by a valspec, then a function, but this should be generalised in future. This optimization nearly doubles the performance of RISC-V It is implemented using a new Optimize.recheck rewrite that replaces the ordinary recheck_defs pass. It uses a new typechecker check_with_envs function that allows re-writes to utilise intermediate typechecking environments to minimize the amount of AST checking that occurs, for performance reasons. Note that older Sail versions including the current OPAM release will complain about the optimize pragma, so this cannot be used until they become up to date with this change. --- src/ast_util.ml | 9 +++-- src/ast_util.mli | 2 ++ src/c_backend.ml | 3 ++ src/optimize.ml | 100 +++++++++++++++++++++++++++++++++++++++++++++++++++++ src/rewrites.ml | 2 +- src/type_check.ml | 8 +++++ src/type_check.mli | 4 +++ 7 files changed, 124 insertions(+), 4 deletions(-) create mode 100644 src/optimize.ml (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index a771291e..6fce9a2a 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -128,7 +128,7 @@ let mk_val_spec vs_aux = let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k - + let is_nat_kopt = function | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true | _ -> false @@ -165,7 +165,7 @@ module Kind = struct | K_type, _ -> 1 | _, K_type -> -1 | K_order, _ -> 1 | _, K_order -> -1 end - + module KOpt = struct type t = kinded_id let compare kopt1 kopt2 = @@ -1289,6 +1289,9 @@ let is_fundef id = function | DEF_fundef (FD_aux (FD_function (_, _, _, FCL_aux (FCL_Funcl (id', _), _) :: _), _)) when Id.compare id' id = 0 -> true | _ -> false +let rename_valspec id (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) = + VS_aux (VS_val_spec (typschm, id, externs, is_cast), annot) + let rename_funcl id (FCL_aux (FCL_Funcl (_, pexp), annot)) = FCL_aux (FCL_Funcl (id, pexp), annot) let rename_fundef id (FD_aux (FD_function (ropt, topt, eopt, funcls), annot)) = @@ -1425,7 +1428,7 @@ let locate_id f (Id_aux (name, l)) = Id_aux (name, f l) let locate_kid f (Kid_aux (name, l)) = Kid_aux (name, f l) let locate_kind f (K_aux (kind, l)) = K_aux (kind, f l) - + let locate_kinded_id f (KOpt_aux (KOpt_kind (k, kid), l)) = KOpt_aux (KOpt_kind (locate_kind f k, locate_kid f kid), f l) diff --git a/src/ast_util.mli b/src/ast_util.mli index ca3a9598..f741704a 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -372,6 +372,8 @@ val is_valspec : id -> 'a def -> bool val is_fundef : id -> 'a def -> bool +val rename_valspec : id -> 'a val_spec -> 'a val_spec + val rename_fundef : id -> 'a fundef -> 'a fundef val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option diff --git a/src/c_backend.ml b/src/c_backend.ml index f02cdb9c..7cda4668 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -1763,6 +1763,9 @@ let rec compile_def ctx = function (* Only the parser and sail pretty printer care about this. *) | DEF_fixity _ -> [], ctx + (* We just ignore any pragmas we don't want to deal with. *) + | DEF_pragma _ -> [], ctx + | DEF_internal_mutrec fundefs -> let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs diff --git a/src/optimize.ml b/src/optimize.ml new file mode 100644 index 00000000..a372abf4 --- /dev/null +++ b/src/optimize.ml @@ -0,0 +1,100 @@ +(**************************************************************************) +(* 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 + +let recheck (Defs defs) = + let defs = Type_check.check_with_envs Type_check.initial_env defs in + + let rec find_optimizations = function + | ([DEF_pragma ("optimize", pragma, p_l)], env) + :: ([DEF_spec vs as def1], _) + :: ([DEF_fundef fdef as def2], _) + :: defs -> + let id = id_of_val_spec vs in + let args = Str.split (Str.regexp " +") (String.trim pragma) in + begin match args with + | ["unroll"; n]-> + let n = int_of_string n in + + let rw_app subst (fn, args) = + if Id.compare id fn = 0 then E_app (subst, args) else E_app (fn, args) + in + let rw_exp subst = { id_exp_alg with e_app = rw_app subst } in + let rw_defs subst = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp subst)) } in + + let specs = ref [def1] in + let bodies = ref [rewrite_def (rw_defs (append_id id "_unroll_1")) def2] in + + for i = 1 to n do + let current_id = append_id id ("_unroll_" ^ string_of_int i) in + let next_id = if i = n then current_id else append_id id ("_unroll_" ^ string_of_int (i + 1)) in + (* Create a valspec for the new unrolled function *) + specs := !specs @ [DEF_spec (rename_valspec current_id vs)]; + (* Then duplicate it's function body and make it call the next unrolled function *) + bodies := !bodies @ [rewrite_def (rw_defs next_id) (DEF_fundef (rename_fundef current_id fdef))] + done; + + !specs @ !bodies @ find_optimizations defs + + | _ -> + Util.warn ("Unrecognised optimize pragma in this context: " ^ pragma); + def1 :: def2 :: find_optimizations defs + end + + | (defs, _) :: defs' -> + defs @ find_optimizations defs' + + | [] -> [] + in + + Defs (find_optimizations defs) diff --git a/src/rewrites.ml b/src/rewrites.ml index 8894f2c8..382f9c8f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5129,7 +5129,7 @@ let rewrite_defs_c = [ ("trivial_sizeof", rewrite_trivial_sizeof); ("sizeof", rewrite_sizeof); ("merge_function_clauses", merge_funcls); - ("recheck_defs", recheck_defs) + ("recheck_defs", Optimize.recheck) ] let rewrite_defs_interpreter = [ diff --git a/src/type_check.ml b/src/type_check.ml index 1b6efa46..712b9944 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4470,6 +4470,14 @@ and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = let (Defs defs, env) = check env (Defs defs) in (Defs (def @ defs)), env +and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list = + fun env defs -> + match defs with + | [] -> [] + | def :: defs -> + let def, env = check_def env def in + (def, env) :: check_with_envs env defs + let initial_env = Env.empty |> Env.add_prover prove diff --git a/src/type_check.mli b/src/type_check.mli index 81682606..6a0f0410 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -411,5 +411,9 @@ Some invariants that will hold of a fully checked AST are: Type_error.check *) val check : Env.t -> 'a defs -> tannot defs * Env.t +(** The same as [check], but exposes the intermediate type-checking + environments so we don't have to always re-check the entire AST *) +val check_with_envs : Env.t -> 'a def list -> (tannot def list * Env.t) list + (** The initial type checking environment *) val initial_env : Env.t -- cgit v1.2.3 From c1e0bc6530bcc18d2c3798894b58855ed1231719 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 25 Jan 2019 15:47:41 +0000 Subject: Fix solution finding using SMT by looking for the right variable --- src/constraint.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/constraint.ml b/src/constraint.ml index 7ead0cc8..b7e3cb47 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -131,16 +131,17 @@ let to_smt l vars constr = | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") in - var_decs l vars, smt_constraint constr + var_decs l vars, smt_constraint constr, smt_var -let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string = - let variables, problem = to_smt l vars constr in +let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string * (kid -> sexpr) = + let variables, problem, var_map = to_smt l vars constr in "(push)\n" ^ variables ^ "\n" ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; problem]) ^ "\n(assert constraint)\n(check-sat)" ^ (if get_model then "\n(get-model)" else "") - ^ "\n(pop)" + ^ "\n(pop)", + var_map type smt_result = Unknown | Sat | Unsat @@ -183,7 +184,7 @@ let save_digests () = let call_z3' l vars constraints : smt_result = let problems = [constraints] in - let z3_file = smtlib_of_constraints l vars constraints in + let z3_file, _ = smtlib_of_constraints l vars constraints in (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) @@ -230,9 +231,11 @@ let call_z3 l vars constraints = result let rec solve_z3 l vars constraints var = - let z3_file = smtlib_of_constraints ~get_model:true l vars constraints in + let z3_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in + let z3_var = pp_sexpr (smt_var var) in - (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) + (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); + prerr_endline ("Solving for " ^ z3_var); *) let rec input_all chan = try @@ -250,7 +253,7 @@ let rec solve_z3 l vars constraints var = let z3_output = String.concat " " (input_all z3_chan) in let _ = Unix.close_process_in z3_chan in Sys.remove input_file; - let regexp = {|(define-fun v|} ^ Util.zencode_string (string_of_kid var) ^ {| () Int[ ]+\([0-9]+\))|} in + let regexp = {|(define-fun |} ^ z3_var ^ {| () Int[ ]+\([0-9]+\))|} in try let _ = Str.search_forward (Str.regexp regexp) z3_output 0 in let result = Big_int.of_string (Str.matched_group 1 z3_output) in -- cgit v1.2.3 From e3266e1ce5463d57f3d35c89dc811348f76c9e41 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 25 Jan 2019 15:48:57 +0000 Subject: Monomorphisation: update a built-in name --- src/monomorphise.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4bb1876c..76a48cd7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3418,7 +3418,7 @@ let rec sets_from_assert e = match e with | E_app (Id_aux (Id "or_bool",_),[e1;e2]) -> aux e1 @ aux e2 - | E_app (Id_aux (Id "eq_atom",_), + | E_app (Id_aux (Id "eq_int",_), [E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); E_aux (E_lit (L_aux (L_num i,_)),_)]) -> (check_kid kid; [i]) @@ -4034,7 +4034,7 @@ let rec extract_value_from_guard var (E_aux (e,_)) = match e with | E_app (op, ([E_aux (E_id var',_); E_aux (E_lit (L_aux (L_num i,_)),_)] | [E_aux (E_lit (L_aux (L_num i,_)),_); E_aux (E_id var',_)])) - when string_of_id op = "eq_atom" && Id.compare var var' == 0 -> + when string_of_id op = "eq_int" && Id.compare var var' == 0 -> Some i | E_app (op, [e1;e2]) when string_of_id op = "and_bool" -> (match extract_value_from_guard var e1 with @@ -4047,7 +4047,8 @@ let fill_in_type env typ = let subst = KidSet.fold (fun kid subst -> match Env.get_typ_var kid env with | K_type - | K_order -> subst + | K_order + | K_bool -> subst | K_int -> (match solve env (nvar kid) with | None -> subst @@ -4102,7 +4103,7 @@ let add_bitvector_casts (Defs defs) = | E_app (op, ([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] | [y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)])) - when string_of_id op = "eq_atom" -> + when string_of_id op = "eq_int" -> (match destruct_atom_nexp (env_of y) (typ_of y) with | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)] | _ -> []) -- cgit v1.2.3 From b826df25ee3ec624483b8486af211e6d1e965589 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 28 Jan 2019 21:21:16 +0000 Subject: Lem: Be more careful about nexps occurring in the function signature Don't ask Z3 to simplify them, as flow typing might lead to different results in different if-branches, for example, leading to type errors in Lem. --- src/pretty_print_lem.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 5c67f93a..c0af581a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -349,14 +349,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let mk_typ nexp = Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) in - match Type_check.solve env size with - | Some n -> mk_typ (nconstant n) - | None -> - let is_equal nexp = - prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) - in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with - | nexp -> mk_typ nexp - | exception Not_found -> None + let is_equal nexp = + prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) + in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with + | nexp -> mk_typ nexp + | exception Not_found -> + match Type_check.solve env size with + | Some n -> mk_typ (nconstant n) + | None -> None end | _ -> None -- cgit v1.2.3 From 60164a9a221ed6566f1067100dbea2ec828b47d2 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 29 Jan 2019 16:50:05 +0000 Subject: Improve generation of initial register state Define initial values for record types once instead of repeating them in the initial register state. --- src/state.ml | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/state.ml b/src/state.ml index c9a47b06..fe1cebe7 100644 --- a/src/state.ml +++ b/src/state.ml @@ -135,20 +135,20 @@ let generate_initial_regstate defs = let typ_subst_typquant tq args typ = List.fold_left2 typ_subst_quant_item typ (quant_items tq) args in - let add_typ_init_val vals = function + let add_typ_init_val (defs', vals) = function | TD_enum (id, _, id1 :: _, _) -> (* Choose the first value of an enumeration type as default *) - Bindings.add id (fun _ -> string_of_id id1) vals + (defs', Bindings.add id (fun _ -> string_of_id id1) vals) | TD_variant (id, _, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) -> (* Choose the first variant of a union type as default *) let init_val args = let typ1 = typ_subst_typquant tq args typ1 in string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")" in - Bindings.add id init_val vals + (defs', Bindings.add id init_val vals) | TD_abbrev (id, tq, A_aux (A_typ typ, _)) -> let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in - Bindings.add id init_val vals + (defs', Bindings.add id init_val vals) | TD_record (id, _, tq, fields, _) -> let init_val args = let init_field (typ, id) = @@ -157,16 +157,21 @@ let generate_initial_regstate defs = in "struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }" in - Bindings.add id init_val vals + let def_name = "initial_" ^ string_of_id id in + if quant_items tq = [] && not (is_defined defs def_name) then + (defs' @ ["let " ^ def_name ^ " : " ^ string_of_id id ^ " = " ^ init_val []], + Bindings.add id (fun _ -> def_name) vals) + else (defs', Bindings.add id init_val vals) | TD_bitfield (id, typ, _) -> - Bindings.add id (fun _ -> lookup_init_val vals typ) vals - | _ -> vals + (defs', Bindings.add id (fun _ -> lookup_init_val vals typ) vals) + | _ -> (defs', vals) in - let init_vals = List.fold_left (fun vals def -> match def with - | DEF_type (TD_aux (td, _)) -> add_typ_init_val vals td - | _ -> vals) Bindings.empty defs + let (init_defs, init_vals) = List.fold_left (fun inits def -> match def with + | DEF_type (TD_aux (td, _)) -> add_typ_init_val inits td + | _ -> inits) ([], Bindings.empty) defs in let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in + init_defs @ ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"] with | _ -> [] (* Do not generate an initial register state if anything goes wrong *) -- cgit v1.2.3 From 20334e0f8d1115bf7f70226f5020df180d5d7f89 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 29 Jan 2019 16:54:36 +0000 Subject: Support case splitting on variables as well as sizeof in cast introduction --- src/monomorphise.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 76a48cd7..666abe86 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -4107,6 +4107,13 @@ let add_bitvector_casts (Defs defs) = (match destruct_atom_nexp (env_of y) (typ_of y) with | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)] | _ -> []) + | E_app (op,[x;y]) + when string_of_id op = "eq_int" -> + (match destruct_atom_nexp (env_of x) (typ_of x), destruct_atom_nexp (env_of y) (typ_of y) with + | Some (Nexp_aux (Nexp_var kid,_)), Some (Nexp_aux (Nexp_constant i,_)) + | Some (Nexp_aux (Nexp_constant i,_)), Some (Nexp_aux (Nexp_var kid,_)) + -> [(kid,i)] + | _ -> []) | E_app (op, [x;y]) when string_of_id op = "and_bool" -> extract x @ extract y | _ -> [] -- cgit v1.2.3 From 57ee80b836440110b933350a3646ca5059badda0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 31 Jan 2019 10:59:46 +0000 Subject: Add missing cases to constraint comparison --- src/ast_util.ml | 141 ++++++++++++++++++++++++++++++-------------------------- 1 file changed, 76 insertions(+), 65 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 6fce9a2a..d45dd307 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -984,77 +984,88 @@ let lex_ord f g x1 x2 y1 y2 = | 0 -> g y1 y2 | n -> n +let rec nc_compare (NC_aux (nc1,_)) (NC_aux (nc2,_)) = + match nc1, nc2 with + | NC_equal (n1,n2), NC_equal (n3,n4) + | NC_bounded_ge (n1,n2), NC_bounded_ge (n3,n4) + | NC_bounded_le (n1,n2), NC_bounded_le (n3,n4) + | NC_not_equal (n1,n2), NC_not_equal (n3,n4) + -> lex_ord Nexp.compare Nexp.compare n1 n3 n2 n4 + | NC_set (k1,s1), NC_set (k2,s2) -> + lex_ord Kid.compare (Util.compare_list Nat_big_num.compare) k1 k2 s1 s2 + | NC_or (nc1,nc2), NC_or (nc3,nc4) + | NC_and (nc1,nc2), NC_and (nc3,nc4) + -> lex_ord nc_compare nc_compare nc1 nc3 nc2 nc4 + | NC_app (f1,args1), NC_app (f2,args2) + -> lex_ord Id.compare (Util.compare_list typ_arg_compare) f1 f2 args1 args2 + | NC_var v1, NC_var v2 + -> Kid.compare v1 v2 + | NC_true, NC_true + | NC_false, NC_false + -> 0 + | NC_equal _, _ -> -1 | _, NC_equal _ -> 1 + | NC_bounded_ge _, _ -> -1 | _, NC_bounded_ge _ -> 1 + | NC_bounded_le _, _ -> -1 | _, NC_bounded_le _ -> 1 + | NC_not_equal _, _ -> -1 | _, NC_not_equal _ -> 1 + | NC_set _, _ -> -1 | _, NC_set _ -> 1 + | NC_or _, _ -> -1 | _, NC_or _ -> 1 + | NC_and _, _ -> -1 | _, NC_and _ -> 1 + | NC_app _, _ -> -1 | _, NC_app _ -> 1 + | NC_var _, _ -> -1 | _, NC_var _ -> 1 + | NC_true, _ -> -1 | _, NC_true -> 1 + +and typ_compare (Typ_aux (t1,_)) (Typ_aux (t2,_)) = + match t1,t2 with + | Typ_internal_unknown, Typ_internal_unknown -> 0 + | Typ_id id1, Typ_id id2 -> Id.compare id1 id2 + | Typ_var kid1, Typ_var kid2 -> Kid.compare kid1 kid2 + | Typ_fn (ts1,t2,e1), Typ_fn (ts3,t4,e2) -> + (match Util.compare_list typ_compare ts1 ts3 with + | 0 -> (match typ_compare t2 t4 with + | 0 -> effect_compare e1 e2 + | n -> n) + | n -> n) + | Typ_bidir (t1,t2), Typ_bidir (t3,t4) -> + (match typ_compare t1 t3 with + | 0 -> typ_compare t2 t3 + | n -> n) + | Typ_tup ts1, Typ_tup ts2 -> Util.compare_list typ_compare ts1 ts2 + | Typ_exist (ks1,nc1,t1), Typ_exist (ks2,nc2,t2) -> + (match Util.compare_list KOpt.compare ks1 ks2 with + | 0 -> (match nc_compare nc1 nc2 with + | 0 -> typ_compare t1 t2 + | n -> n) + | n -> n) + | Typ_app (id1,ts1), Typ_app (id2,ts2) -> + (match Id.compare id1 id2 with + | 0 -> Util.compare_list typ_arg_compare ts1 ts2 + | n -> n) + | Typ_internal_unknown, _ -> -1 | _, Typ_internal_unknown -> 1 + | Typ_id _, _ -> -1 | _, Typ_id _ -> 1 + | Typ_var _, _ -> -1 | _, Typ_var _ -> 1 + | Typ_fn _, _ -> -1 | _, Typ_fn _ -> 1 + | Typ_bidir _, _ -> -1 | _, Typ_bidir _ -> 1 + | Typ_tup _, _ -> -1 | _, Typ_tup _ -> 1 + | Typ_exist _, _ -> -1 | _, Typ_exist _ -> 1 + +and typ_arg_compare (A_aux (ta1,_)) (A_aux (ta2,_)) = + match ta1, ta2 with + | A_nexp n1, A_nexp n2 -> Nexp.compare n1 n2 + | A_typ t1, A_typ t2 -> typ_compare t1 t2 + | A_order o1, A_order o2 -> order_compare o1 o2 + | A_bool nc1, A_bool nc2 -> nc_compare nc1 nc2 + | A_nexp _, _ -> -1 | _, A_nexp _ -> 1 + | A_typ _, _ -> -1 | _, A_typ _ -> 1 + | A_order _, _ -> -1 | _, A_order _ -> 1 + module NC = struct type t = n_constraint - let rec compare (NC_aux (nc1,_)) (NC_aux (nc2,_)) = - match nc1, nc2 with - | NC_equal (n1,n2), NC_equal (n3,n4) - | NC_bounded_ge (n1,n2), NC_bounded_ge (n3,n4) - | NC_bounded_le (n1,n2), NC_bounded_le (n3,n4) - | NC_not_equal (n1,n2), NC_not_equal (n3,n4) - -> lex_ord Nexp.compare Nexp.compare n1 n3 n2 n4 - | NC_set (k1,s1), NC_set (k2,s2) -> - lex_ord Kid.compare (Util.compare_list Nat_big_num.compare) k1 k2 s1 s2 - | NC_or (nc1,nc2), NC_or (nc3,nc4) - | NC_and (nc1,nc2), NC_and (nc3,nc4) - -> lex_ord compare compare nc1 nc3 nc2 nc4 - | NC_true, NC_true - | NC_false, NC_false - -> 0 - | NC_equal _, _ -> -1 | _, NC_equal _ -> 1 - | NC_bounded_ge _, _ -> -1 | _, NC_bounded_ge _ -> 1 - | NC_bounded_le _, _ -> -1 | _, NC_bounded_le _ -> 1 - | NC_not_equal _, _ -> -1 | _, NC_not_equal _ -> 1 - | NC_set _, _ -> -1 | _, NC_set _ -> 1 - | NC_or _, _ -> -1 | _, NC_or _ -> 1 - | NC_and _, _ -> -1 | _, NC_and _ -> 1 - | NC_true, _ -> -1 | _, NC_true -> 1 + let compare = nc_compare end module Typ = struct type t = typ - let rec compare (Typ_aux (t1,_)) (Typ_aux (t2,_)) = - match t1,t2 with - | Typ_internal_unknown, Typ_internal_unknown -> 0 - | Typ_id id1, Typ_id id2 -> Id.compare id1 id2 - | Typ_var kid1, Typ_var kid2 -> Kid.compare kid1 kid2 - | Typ_fn (ts1,t2,e1), Typ_fn (ts3,t4,e2) -> - (match Util.compare_list compare ts1 ts3 with - | 0 -> (match compare t2 t4 with - | 0 -> effect_compare e1 e2 - | n -> n) - | n -> n) - | Typ_bidir (t1,t2), Typ_bidir (t3,t4) -> - (match compare t1 t3 with - | 0 -> compare t2 t3 - | n -> n) - | Typ_tup ts1, Typ_tup ts2 -> Util.compare_list compare ts1 ts2 - | Typ_exist (ks1,nc1,t1), Typ_exist (ks2,nc2,t2) -> - (match Util.compare_list KOpt.compare ks1 ks2 with - | 0 -> (match NC.compare nc1 nc2 with - | 0 -> compare t1 t2 - | n -> n) - | n -> n) - | Typ_app (id1,ts1), Typ_app (id2,ts2) -> - (match Id.compare id1 id2 with - | 0 -> Util.compare_list arg_compare ts1 ts2 - | n -> n) - | Typ_internal_unknown, _ -> -1 | _, Typ_internal_unknown -> 1 - | Typ_id _, _ -> -1 | _, Typ_id _ -> 1 - | Typ_var _, _ -> -1 | _, Typ_var _ -> 1 - | Typ_fn _, _ -> -1 | _, Typ_fn _ -> 1 - | Typ_bidir _, _ -> -1 | _, Typ_bidir _ -> 1 - | Typ_tup _, _ -> -1 | _, Typ_tup _ -> 1 - | Typ_exist _, _ -> -1 | _, Typ_exist _ -> 1 - and arg_compare (A_aux (ta1,_)) (A_aux (ta2,_)) = - match ta1, ta2 with - | A_nexp n1, A_nexp n2 -> Nexp.compare n1 n2 - | A_typ t1, A_typ t2 -> compare t1 t2 - | A_order o1, A_order o2 -> order_compare o1 o2 - | A_bool nc1, A_bool nc2 -> NC.compare nc1 nc2 - | A_nexp _, _ -> -1 | _, A_nexp _ -> 1 - | A_typ _, _ -> -1 | _, A_typ _ -> 1 - | A_order _, _ -> -1 | _, A_order _ -> 1 + let compare = typ_compare end module TypMap = Map.Make(Typ) -- cgit v1.2.3 From e62896cecd575134a85def6815fe552f3154ea01 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 31 Jan 2019 11:14:52 +0000 Subject: Monomorphisation: improve cast insertion and nexp rewriting on variants It now pushes casts into lets and constructor applications, and so supports the case needed for RISC-V. --- src/monomorphise.ml | 85 +++++++++++++++++++++++++++++++++++++++++++++-------- src/type_check.mli | 2 ++ 2 files changed, 74 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 666abe86..84025595 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3969,7 +3969,8 @@ let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ = [A_aux (A_nexp size',l_size'); t_ord; A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_) as t_bit]) -> begin match simplify_size_nexp env quant_kids size, simplify_size_nexp env quant_kids size' with - | Some size, Some size' when Nexp.compare size size' <> 0 -> + | Some size, Some size' -> + if Nexp.compare size size' <> 0 then let var = fresh () in let tar_typ' = Typ_aux (Typ_app (t_id, [A_aux (A_nexp size',l_size');t_ord;t_bit]), tar_l) in @@ -3980,6 +3981,10 @@ let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ = E_aux (E_app (Id_aux (Id cast_name, genunk), [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))), (genunk, tar_ann)) + else + let var = fresh () in + P_aux (P_id var,(Generated src_l,src_ann)), + E_aux (E_id var,(Generated src_l,tar_ann)) | _ -> let var = fresh () in P_aux (P_id var,(Generated src_l,src_ann)), @@ -4028,7 +4033,44 @@ let make_bitvector_env_casts env quant_kids (kid,i) exp = Bindings.fold (fun var (mut,typ) exp -> if mut = Immutable then mk_cast var typ exp else exp) locals exp -let make_bitvector_cast_exp cast_name env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns cast_name env quant_kids typ target_typ)) exp +let make_bitvector_cast_exp cast_name cast_env quant_kids typ target_typ exp = + let infer_arg_typ env f l typ = + let (typq, ctor_typ) = Env.get_union_id f env in + let quants = quant_items typq in + match Env.expand_synonyms env ctor_typ with + | Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) -> + begin + let goals = quant_kopts typq |> List.map kopt_kid |> KidSet.of_list in + let unifiers = unify l env goals ret_typ typ in + let arg_typ' = subst_unifiers unifiers arg_typ in + arg_typ' + end + | _ -> typ_error l ("Malformed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ) + + in + (* Push the cast down, including through constructors *) + let rec aux exp (typ, target_typ) = + let exp_env = env_of exp in + match exp with + | E_aux (E_let (lb,exp'),ann) -> + E_aux (E_let (lb,aux exp' (typ, target_typ)),ann) + | E_aux (E_tuple exps,(l,ann)) -> begin + match Env.expand_synonyms exp_env typ, Env.expand_synonyms exp_env target_typ with + | Typ_aux (Typ_tup src_typs,_), Typ_aux (Typ_tup tgt_typs,_) -> + E_aux (E_tuple (List.map2 aux exps (List.combine src_typs tgt_typs)),(l,ann)) + | _ -> raise (Reporting.err_unreachable l __POS__ + ("Attempted to insert cast on tuple on non-tuple type: " ^ + string_of_typ typ ^ " to " ^ string_of_typ target_typ)) + end + | E_aux (E_app (f,args),(l,ann)) when Env.is_union_constructor f (env_of exp) -> + let arg = match args with [arg] -> arg | _ -> E_aux (E_tuple args, (l,empty_tannot)) in + let src_arg_typ = infer_arg_typ (env_of exp) f l typ in + let tgt_arg_typ = infer_arg_typ (env_of exp) f l target_typ in + E_aux (E_app (f,[aux arg (src_arg_typ, tgt_arg_typ)]),(l,ann)) + | _ -> + (snd (make_bitvector_cast_fns cast_name cast_env quant_kids typ target_typ)) exp + in + aux exp (typ, target_typ) let rec extract_value_from_guard var (E_aux (e,_)) = match e with @@ -4077,13 +4119,14 @@ let add_bitvector_casts (Defs defs) = let pat,guard,body,ann = destruct_pexp pexp in let body = match pat, guard with | P_aux (P_lit (L_aux (L_num i,_)),_), _ -> - let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in + (* We used to just substitute kid, but fill_in_type also catches other kids defined by it *) + let src_typ = fill_in_type (Env.add_constraint (nc_eq (nvar kid) (nconstant i)) env) result_typ in make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ (make_bitvector_env_casts env quant_kids (kid,i) body) | P_aux (P_id var,_), Some guard -> (match extract_value_from_guard var guard with | Some i -> - let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in + let src_typ = fill_in_type (Env.add_constraint (nc_eq (nvar kid) (nconstant i)) env) result_typ in make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ (make_bitvector_env_casts env quant_kids (kid,i) body) | None -> body) @@ -4251,14 +4294,13 @@ let rewrite_toplevel_nexps (Defs defs) = let nexp_map, typ = rewrite_typ_in_spec env nexp_map typ in (nexp_map, typ::t)) typs (nexp_map,[]) in nexp_map, Typ_aux (Typ_tup typs,ann) - | _ -> - let typ' = Env.base_typ_of env typ_full in + | _ when is_number typ_full || is_bitvector_typ typ_full -> begin let nexp_opt = - match destruct_atom_nexp env typ' with + match destruct_atom_nexp env typ_full with | Some nexp -> Some nexp | None -> - if is_bitvector_typ typ' then - let (size,_,_) = vector_typ_args_of typ' in + if is_bitvector_typ typ_full then + let (size,_,_) = vector_typ_args_of typ_full in Some size else None in match nexp_opt with @@ -4274,10 +4316,27 @@ let rewrite_toplevel_nexps (Defs defs) = (kid, nexp)::nexp_map, kid in let new_nexp = nvar kid in - (* Try to avoid expanding the original type *) - let changed, typ = replace_nexp_in_typ env typ_full nexp new_nexp in - if changed then nexp_map, typ - else nexp_map, snd (replace_nexp_in_typ env typ' nexp new_nexp) + nexp_map, snd (replace_nexp_in_typ env typ_full nexp new_nexp) + end + | _ -> + let typ' = Env.base_typ_of env typ_full in + if Typ.compare typ_full typ' == 0 then + match t with + | Typ_app (f,args) -> + let in_arg nexp_map (A_aux (arg,l) as arg_full) = + match arg with + | A_typ typ -> + let nexp_map, typ' = rewrite_typ_in_spec env nexp_map typ in + nexp_map, A_aux (A_typ typ',l) + | A_bool _ | A_nexp _ | A_order _ -> nexp_map, arg_full + in + let nexp_map, args = + List.fold_right (fun arg (nexp_map,args) -> + let nexp_map, arg = in_arg nexp_map arg in + (nexp_map, arg::args)) args (nexp_map,[]) + in nexp_map, Typ_aux (Typ_app (f,args),ann) + | _ -> nexp_map, typ_full + else rewrite_typ_in_spec env nexp_map typ' in let rewrite_valspec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tqs,typ),ts_l),id,ext_opt,is_cast),ann)) = match tqs with diff --git a/src/type_check.mli b/src/type_check.mli index 6a0f0410..ce5324d1 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -202,6 +202,8 @@ module Env : sig val pattern_completeness_ctx : t -> Pattern_completeness.ctx val builtin_typs : typquant Bindings.t + + val get_union_id : id -> t -> typquant * typ end (** Push all the type variables and constraints from a typquant into -- cgit v1.2.3 From 5010b667b59bbe0fbb13747a1d2409a2b859cd7a Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 31 Jan 2019 15:24:38 +0000 Subject: Make cast insertion handle more complex nexps and pushing casts into blocks # Conflicts: # src/monomorphise.ml --- src/monomorphise.ml | 48 ++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 38 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 84025595..20c4e386 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3930,16 +3930,39 @@ end module BitvectorSizeCasts = struct -let simplify_size_nexp env quant_kids (Nexp_aux (_,l) as nexp) = - match solve env nexp with - | Some n -> Some (nconstant n) - | None -> - let is_equal kid = - prove env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) - in - match List.find is_equal quant_kids with - | kid -> Some (Nexp_aux (Nexp_var kid,Generated l)) - | exception Not_found -> None +let simplify_size_nexp env quant_kids nexp = + let rec aux (Nexp_aux (ne,l) as nexp) = + match solve env nexp with + | Some n -> Some (nconstant n) + | None -> + let is_equal kid = + prove env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + in + match List.find is_equal quant_kids with + | kid -> Some (Nexp_aux (Nexp_var kid,Generated l)) + | exception Not_found -> + (* Normally rewriting of complex nexps in function signatures will + produce a simple constant or variable above, but occasionally it's + useful to work when that rewriting hasn't been applied. In + particular, that rewriting isn't fully working with RISC-V at the + moment. *) + let re f = function + | Some n1, Some n2 -> Some (Nexp_aux (f n1 n2,l)) + | _ -> None + in + match ne with + | Nexp_times(n1,n2) -> + re (fun n1 n2 -> Nexp_times(n1,n2)) (aux n1, aux n2) + | Nexp_sum(n1,n2) -> + re (fun n1 n2 -> Nexp_sum(n1,n2)) (aux n1, aux n2) + | Nexp_minus(n1,n2) -> + re (fun n1 n2 -> Nexp_times(n1,n2)) (aux n1, aux n2) + | Nexp_exp n -> + Util.option_map (fun n -> Nexp_aux (Nexp_exp n,l)) (aux n) + | Nexp_neg n -> + Util.option_map (fun n -> Nexp_aux (Nexp_neg n,l)) (aux n) + | _ -> None + in aux nexp (* These functions add cast functions across case splits, so that when a bitvector size becomes known in sail, the generated Lem code contains a @@ -4054,6 +4077,11 @@ let make_bitvector_cast_exp cast_name cast_env quant_kids typ target_typ exp = match exp with | E_aux (E_let (lb,exp'),ann) -> E_aux (E_let (lb,aux exp' (typ, target_typ)),ann) + | E_aux (E_block exps,ann) -> + let exps' = match List.rev exps with + | [] -> [] + | final::l -> aux final (typ, target_typ)::l + in E_aux (E_block (List.rev exps'),ann) | E_aux (E_tuple exps,(l,ann)) -> begin match Env.expand_synonyms exp_env typ, Env.expand_synonyms exp_env target_typ with | Typ_aux (Typ_tup src_typs,_), Typ_aux (Typ_tup tgt_typs,_) -> -- cgit v1.2.3 From 88dda99529fd0e151c932ab1bf22b3c101dd8309 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 31 Jan 2019 15:20:25 +0000 Subject: Drop type annotations in top-level nexp rewriting in favour of valspecs otherwise the valspec rewriting will be inconsistent with the type annotation. Note that the type checker will have introduced valspecs where necessary. --- src/monomorphise.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 20c4e386..0a26c8b0 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -4432,7 +4432,11 @@ let rewrite_toplevel_nexps (Defs defs) = | DEF_spec vs -> (match rewrite_valspec vs with | None -> spec_map, def | Some (id, nexp_map, vs) -> Bindings.add id nexp_map spec_map, DEF_spec vs) - | DEF_fundef (FD_aux (FD_function (recopt,tann,eff,funcls),ann)) -> + | DEF_fundef (FD_aux (FD_function (recopt,_,eff,funcls),ann)) -> + (* Type annotations on function definitions will have been turned into + valspecs by type checking, so it should be safe to drop them rather + than updating them. *) + let tann = Typ_annot_opt_aux (Typ_annot_opt_none,Generated Unknown) in spec_map, DEF_fundef (FD_aux (FD_function (recopt,tann,eff,List.map (rewrite_funcl spec_map) funcls),ann)) | _ -> spec_map, def -- cgit v1.2.3 From 116f55b569d68602e8c1f04622100a37e68e91c6 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 31 Jan 2019 17:00:11 +0000 Subject: Turn on cast insertion for -lem_mwords and revert b826df25 now that cast insertion can handle RISC-V Also inserts specs for casts in they're not present --- src/monomorphise.ml | 26 +++++++++++++++++++++++++- src/pretty_print_lem.ml | 16 ++++++++-------- src/rewrites.ml | 10 +++++++--- 3 files changed, 40 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 0a26c8b0..ccaceec7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3964,6 +3964,13 @@ let simplify_size_nexp env quant_kids nexp = | _ -> None in aux nexp +let specs_required = ref IdSet.empty +let check_for_spec env name = + let id = mk_id name in + match Env.get_val_spec id env with + | _ -> () + | exception _ -> specs_required := IdSet.add id !specs_required + (* These functions add cast functions across case splits, so that when a bitvector size becomes known in sail, the generated Lem code contains a function call to change mword 'n to (say) mword ty16, and vice versa. *) @@ -4023,6 +4030,7 @@ let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ = let pat, e' = aux src_typ' target_typ' in match !at_least_one with | Some one_target_typ -> begin + check_for_spec env cast_name; let src_ann = mk_tannot env src_typ no_effect in let tar_ann = mk_tannot env target_typ no_effect in match src_typ' with @@ -4246,7 +4254,23 @@ let add_bitvector_casts (Defs defs) = | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),fd_ann)) -> DEF_fundef (FD_aux (FD_function (r,t,e,List.map rewrite_funcl fcls),fd_ann)) | d -> d - in Defs (List.map rewrite_def defs) + in + specs_required := IdSet.empty; + let defs = List.map rewrite_def defs in + let l = Generated Unknown in + let Defs cast_specs,_ = + (* TODO: use default/relevant order *) + let kid = mk_kid "n" in + let bitsn = vector_typ (nvar kid) dec_ord bit_typ in + let ts = mk_typschm (mk_typquant [mk_qi_id K_int kid]) + (function_typ [bitsn] bitsn no_effect) in + let extfn _ = Some "zeroExtend" in + let mkfn name = + mk_val_spec (VS_val_spec (ts,name,extfn,false)) + in + let defs = List.map mkfn (IdSet.elements !specs_required) in + check Env.empty (Defs defs) + in Defs (cast_specs @ defs) end let replace_nexp_in_typ env typ orig new_nexp = diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c0af581a..5c67f93a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -349,14 +349,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let mk_typ nexp = Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) in - let is_equal nexp = - prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) - in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with - | nexp -> mk_typ nexp - | exception Not_found -> - match Type_check.solve env size with - | Some n -> mk_typ (nconstant n) - | None -> None + match Type_check.solve env size with + | Some n -> mk_typ (nconstant n) + | None -> + let is_equal nexp = + prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) + in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with + | nexp -> mk_typ nexp + | exception Not_found -> None end | _ -> None diff --git a/src/rewrites.ml b/src/rewrites.ml index 382f9c8f..4ea953cf 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4981,6 +4981,10 @@ let if_mono f defs = | [], false -> defs | _, _ -> f defs +(* Also turn mwords stages on when we're just trying out mono *) +let if_mwords f defs = + if !Pretty_print_lem.opt_mwords then f defs else if_mono f defs + let rewrite_defs_lem = [ ("realise_mappings", rewrite_defs_realise_mappings); ("remove_mapping_valspecs", remove_mapping_valspecs); @@ -4991,10 +4995,10 @@ let rewrite_defs_lem = [ ("recheck_defs", if_mono recheck_defs); ("rewrite_toplevel_nexps", if_mono rewrite_toplevel_nexps); ("monomorphise", if_mono monomorphise); - ("recheck_defs", if_mono recheck_defs); - ("add_bitvector_casts", if_mono Monomorphise.add_bitvector_casts); + ("recheck_defs", if_mwords recheck_defs); + ("add_bitvector_casts", if_mwords Monomorphise.add_bitvector_casts); ("rewrite_atoms_to_singletons", if_mono Monomorphise.rewrite_atoms_to_singletons); - ("recheck_defs", if_mono recheck_defs); + ("recheck_defs", if_mwords recheck_defs); ("rewrite_undefined", rewrite_undefined_if_gen false); ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list); ("remove_not_pats", rewrite_defs_not_pats); -- cgit v1.2.3 From e1d33221ea068b452b3862c4dcc5a2794ffc7236 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 31 Jan 2019 17:55:36 +0000 Subject: Fix an unnecessary cast insertion on assignments --- src/monomorphise.ml | 14 ++++++++++---- src/type_check.mli | 2 ++ 2 files changed, 12 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index ccaceec7..dd0f7afd 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -4207,10 +4207,16 @@ let add_bitvector_casts (Defs defs) = E_aux (E_if (e1,e2',e3), ann) | E_return e' -> E_aux (E_return (make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann) - | E_assign (LEXP_aux (lexp,lexp_annot),e') -> - E_aux (E_assign (LEXP_aux (lexp,lexp_annot), - make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) - (typ_of_annot lexp_annot) e'),ann) + | E_assign (LEXP_aux (_,lexp_annot) as lexp,e') -> begin + (* The type in the lexp_annot might come from e' rather than being the + type of the storage, so ask the type checker what it really is. *) + match infer_lexp (env_of_annot lexp_annot) (strip_lexp lexp) with + | LEXP_aux (_,lexp_annot') -> + E_aux (E_assign (lexp, + make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) + (typ_of_annot lexp_annot') e'),ann) + | exception _ -> E_aux (e,ann) + end | E_id id -> begin let env = env_of_annot ann in match Env.lookup_id id env with diff --git a/src/type_check.mli b/src/type_check.mli index ce5324d1..f417c65d 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -297,6 +297,8 @@ val infer_exp : Env.t -> unit exp -> tannot exp val infer_pat : Env.t -> unit pat -> tannot pat * Env.t * unit exp list +val infer_lexp : Env.t -> unit lexp -> tannot lexp + val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t -- cgit v1.2.3