From f1ec636b83611f9d69e2a4d6ce34413399b73823 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 1 Aug 2018 14:26:12 +0100 Subject: Coq: implicit range conversions for function arguments, debug tracing The new option -dcoq_debug_on takes a list of functions to output tracing on. --- src/pretty_print_coq.ml | 72 ++++++++++++++++++++++++++++++++++++++++--------- src/sail.ml | 3 +++ 2 files changed, 63 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 713cfb34..5e3326bf 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -58,6 +58,7 @@ open Pretty_print_common module StringSet = Set.Make(String) let opt_undef_axioms = ref false +let opt_debug_on : string list ref = ref [] (**************************************************************************** * PPrint-based sail-to-coq pprinter @@ -69,6 +70,7 @@ type context = { kid_id_renames : id KBindings.t; (* tyvar -> argument renames *) bound_nexps : NexpSet.t; build_ex_return : bool; + debug : bool; } let empty_ctxt = { early_ret = false; @@ -76,8 +78,20 @@ let empty_ctxt = { kid_id_renames = KBindings.empty; bound_nexps = NexpSet.empty; build_ex_return = false; + debug = false; } +let debug_depth = ref 0 + +let rec indent n = match n with + | 0 -> "" + | n -> "| " ^ indent (n - 1) + +let debug ctxt m = + if ctxt.debug + then print_endline (indent !debug_depth ^ Lazy.force m) + else () + let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar @@ -763,12 +777,29 @@ let replace_atom_return_type ret_typ = true, Typ_aux (Typ_exist ([kid], nc_gteq (nvar kid) (nconstant Nat_big_num.zero), atom_typ (nvar kid)),Generated l) | _ -> false, ret_typ +let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = + match argty, fnty with + | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp nexp,_)]), + Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_); + Typ_arg_aux(Typ_arg_nexp high,_)]) -> + Type_check.prove env (nc_and (nc_eq nexp low) (nc_eq nexp high)) + | Typ_exist (_, _, Typ_aux (Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp _,_)]), _)), + Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_); + Typ_arg_aux(Typ_arg_nexp high,_)]) -> + Type_check.prove env (nc_eq low high) + | _ -> false let prefix_recordtype = true let report = Reporting_basic.err_unreachable let doc_exp_lem, doc_let_lem = let rec top_exp (ctxt : context) (aexp_needed : bool) (E_aux (e, (l,annot)) as full_exp) = + let top_exp c a e = + let () = debug_depth := !debug_depth + 1 in + let r = top_exp c a e in + let () = debug_depth := !debug_depth - 1 in + r + in let expY = top_exp ctxt true in let expN = top_exp ctxt false in let expV = top_exp ctxt in @@ -984,6 +1015,7 @@ let doc_exp_lem, doc_let_lem = parens (separate_map comma (expV false) args) in if aexp_needed then parens (align epp) else epp else + let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in let call, is_extern = if Env.is_extern f env "coq" then string (Env.get_extern f env "coq"), true @@ -996,33 +1028,44 @@ let doc_exp_lem, doc_let_lem = | _ -> [arg_typ], ret_typ, eff) | _ -> raise (Reporting_basic.err_unreachable l "Function not a function type") in + let inst = + match instantiation_of_without_type full_exp with + | x -> x + (* Not all function applications can be inferred, so try falling back to the + type inferred when we know the target type. + TODO: there are probably some edge cases where this won't pick up a need + to cast. *) + | exception _ -> instantiation_of full_exp + in + let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in + (* Insert existential unpacking of arguments where necessary *) let doc_arg arg typ_from_fn = let arg_pp = expY arg in - let arg_ty = expand_range_type (Env.expand_synonyms (env_of arg) (typ_of arg)) in - let typ_from_fn = expand_range_type (Env.expand_synonyms (env_of arg) typ_from_fn) in + let arg_ty_plain = Env.expand_synonyms (env_of arg) (typ_of arg) in + let arg_ty = expand_range_type arg_ty_plain in + let typ_from_fn_plain = subst_unifiers inst typ_from_fn in + let typ_from_fn_plain = Env.expand_synonyms (env_of arg) typ_from_fn_plain in + let typ_from_fn = expand_range_type typ_from_fn_plain in (* TODO: more sophisticated check *) + let () = + debug ctxt (lazy ("arg type found " ^ string_of_typ arg_ty_plain)); + debug ctxt (lazy ("arg type expected " ^ string_of_typ typ_from_fn_plain)) + in match destruct_exist env arg_ty, destruct_exist env typ_from_fn with | Some _, None -> parens (string "projT1 " ^^ arg_pp) (* Usually existentials have already been built elsewhere, but this is useful for (e.g.) ranges *) | None, Some _ -> parens (string "build_ex " ^^ arg_pp) + | Some _, Some _ when is_range_from_atom (env_of arg) arg_ty_plain typ_from_fn_plain -> + parens (string "to_range " ^^ parens (string "projT1 " ^^ arg_pp)) | _, _ -> arg_pp in let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in + (* Decide whether to unpack an existential result, pack one, or cast. To do this we compare the expected type stored in the checked expression with the inferred type. *) - let inst = - match instantiation_of_without_type full_exp with - | x -> x - (* Not all function applications can be inferred, so try falling back to the - type inferred when we know the target type. - TODO: there are probably some edge cases where this won't pick up a need - to cast. *) - | exception _ -> instantiation_of full_exp - in - let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in let ret_typ_inst = subst_unifiers inst ret_typ in @@ -1033,6 +1076,10 @@ let doc_exp_lem, doc_let_lem = let ret_typ_inst = if is_no_Z_proof_fn env f then ret_typ_inst else snd (replace_atom_return_type ret_typ_inst) in + 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, build_ex, in_typ, out_typ = match ret_typ_inst, ann_typ with | Typ_aux (Typ_exist (_,_,t1),_), Typ_aux (Typ_exist (_,_,t2),_) -> @@ -1639,6 +1686,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = kid_id_renames = kid_to_arg_rename; bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ); build_ex_return = effectful eff && build_ex; + debug = List.mem (string_of_id id) (!opt_debug_on) } in (* Put the constraints after pattern matching so that any type variable that's been replaced by one of the term-level arguments is bound. *) diff --git a/src/sail.ml b/src/sail.ml index e698090e..0b56ab21 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -146,6 +146,9 @@ let options = Arg.align ([ ( "-dcoq_warn_nonex", Arg.Set Rewrites.opt_coq_warn_nonexhaustive, "Generate warnings for non-exhaustive pattern matches in the Coq backend"); + ( "-dcoq_debug_on", + Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f::!Pretty_print_coq.opt_debug_on), + " Produce debug messages for Coq output on given function"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix), " set a custom prefix for generated latex command (default sail)"); -- cgit v1.2.3 From 7dbc1523cdb82bdbfb9fea84b5afcdb4f6e829c2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 17:31:58 +0100 Subject: Coq: proper precedence for constraints (both prop and bool) --- src/pretty_print_coq.ml | 75 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 54 insertions(+), 21 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 5e3326bf..d5925dc0 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -310,37 +310,70 @@ let drop_duplicate_atoms kids ty = | Typ_app _ -> Some full_typ in aux_typ ty -(* TODO: parens *) -let rec doc_nc_prop ctx (NC_aux (nc,_)) = +(* Follows Coq precedence levels *) +let rec doc_nc_prop ctx nc = + let rec l85 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) + | _ -> l80 nc_full + and l80 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) + | _ -> l70 nc_full + and l70 (NC_aux (nc,_) as nc_full) = match nc with | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_set (kid, is) -> (* TODO: is this a good translation? *) + | _ -> l10 nc_full + and l10 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_set (kid, is) -> separate space [string "In"; doc_var_lem ctx kid; brackets (separate (string "; ") (List.map (fun i -> string (Nat_big_num.to_string i)) is))] - | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) - | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) | NC_true -> string "True" | NC_false -> string "False" - -(* TODO: parens *) -let rec doc_nc_exp ctx (NC_aux (nc,_)) = - match nc with - | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)) - | NC_set (kid, is) -> (* TODO: is this a good translation? *) - separate space [string "member_Z_list"; doc_var_lem ctx kid; - brackets (separate (string "; ") - (List.map (fun i -> string (Nat_big_num.to_string i)) is))] - | NC_or (nc1, nc2) -> doc_op (string "||") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2) - | NC_and (nc1, nc2) -> doc_op (string "&&") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2) - | NC_true -> string "true" - | NC_false -> string "false" + | NC_or _ + | NC_and _ + | NC_equal _ + | NC_bounded_ge _ + | NC_bounded_le _ + | NC_not_equal _ -> parens (l85 nc_full) + in l85 nc + +(* Follows Coq precedence levels *) +let doc_nc_exp ctx nc = + let rec l70 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | _ -> l50 nc_full + and l50 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_or (nc1, nc2) -> doc_op (string "||") (l50 nc1) (l40 nc2) + | _ -> l40 nc_full + and l40 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_and (nc1, nc2) -> doc_op (string "&&") (l40 nc1) (l10 nc2) + | _ -> l10 nc_full + and l10 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)) + | NC_set (kid, is) -> + separate space [string "member_Z_list"; doc_var_lem ctx kid; + brackets (separate (string "; ") + (List.map (fun i -> string (Nat_big_num.to_string i)) is))] + | NC_true -> string "true" + | NC_false -> string "false" + | NC_equal _ + | NC_bounded_ge _ + | NC_bounded_le _ + | NC_or _ + | NC_and _ -> parens (l70 nc_full) + in l70 nc let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) = match typ with -- cgit v1.2.3 From d2a01be233f1ea4bed66819096949aa4f56b2695 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 18:15:02 +0100 Subject: Coq: remove type removal holdover from Lem backend, add MIPS lemma --- 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 d5925dc0..93a24f4e 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1311,7 +1311,7 @@ let doc_exp_lem, doc_let_lem = let epp = let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in let middle = - match fst (untyp_pat pat) with + match pat with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_id id,_) -> -- cgit v1.2.3 From 2cb15665392d0b87da9e0c1f43e19267f28c3a82 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 3 Aug 2018 14:52:44 +0100 Subject: Coq: generalise dependent pair handling a little 1. for monadic values (not in a terribly useful way, though) 2. for more types --- src/pretty_print_coq.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 93a24f4e..dff68092 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1133,10 +1133,13 @@ let doc_exp_lem, doc_let_lem = | _ -> false in unpack,build_ex,autocast in - let autocast_id = if effectful eff then "autocast_m" else "autocast" in - let epp = if unpack then string "projT1" ^^ space ^^ parens epp else epp in + let autocast_id, proj_id, build_id = + if effectful eff + then "autocast_m", "projT1_m", "build_ex_m" + else "autocast", "projT1", "build_ex" in + let epp = if unpack then string proj_id ^^ space ^^ parens epp else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in - let epp = if build_ex then string "build_ex" ^^ space ^^ parens epp else epp in + let epp = if build_ex then string build_id ^^ space ^^ parens epp else epp in liftR (if aexp_needed then parens (align epp) else epp) end | E_vector_access (v,e) -> -- cgit v1.2.3 From bcb0bb41b9b0058ec03383cc27ec0ef613511c65 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 3 Aug 2018 16:50:31 +0100 Subject: Fix existential variable problems in monomorphisation One due to using raw types from the type checker in casts without trying to turn them into sane types, the other due to forgetting to use the constraint when trying to simplify sizes in existential types. Both triggered because the type checker now records more specific types. --- src/monomorphise.ml | 99 ++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 68 insertions(+), 31 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index adc4d6d2..e9e2c6b6 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3167,13 +3167,15 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = | None -> r | Some (tenv,typ,_) -> let typ = Env.base_typ_of tenv typ in - let env, typ = + let env, tenv, typ = match destruct_exist tenv typ with - | None -> env, typ + | None -> env, tenv, typ | Some (kids, nc, typ) -> { env with kid_deps = List.fold_left (fun kds kid -> KBindings.add kid deps kds) env.kid_deps kids }, - typ + Env.add_constraint nc + (List.fold_left (fun tenv kid -> Env.add_typ_var l kid BK_int tenv) tenv kids), + typ in if is_bitvector_typ typ then let size,_,_ = vector_typ_args_of typ in @@ -3644,6 +3646,14 @@ let is_constant_vec_typ env typ = let rewrite_app env typ (id,args) = let is_append = is_id env (Id "append") in + let try_cast_to_typ (E_aux (e,_) as exp) = + let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in + match size with + | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp) + | _ -> match solve env size with + | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp) + | None -> e + in if is_append id then let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in @@ -3661,14 +3671,23 @@ let rewrite_app env typ (id,args) = not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in - let midsize = nminus size size1 in - let midtyp = vector_typ midsize order bittyp in - E_app (append, - [e1; - E_aux (E_cast (midtyp, - E_aux (E_app (mk_id "subrange_subrange_concat", - [vector1; start1; end1; vector2; start2; end2]), - (Unknown,empty_tannot))),(Unknown,empty_tannot))]) + let midsize = nminus size size1 in begin + match solve env midsize with + | Some c -> + let midtyp = vector_typ (nconstant c) order bittyp in + E_app (append, + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "subrange_subrange_concat", + [vector1; start1; end1; vector2; start2; end2]), + (Unknown,empty_tannot))),(Unknown,empty_tannot))]) + | _ -> + E_app (append, + [e1; + E_aux (E_app (mk_id "subrange_subrange_concat", + [vector1; start1; end1; vector2; start2; end2]), + (Unknown,empty_tannot))]) + end | [E_aux (E_app (append, [e1; E_aux (E_app (slice1, @@ -3680,14 +3699,23 @@ let rewrite_app env typ (id,args) = not (is_constant length1 || is_constant length2) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in - let midsize = nminus size size1 in - let midtyp = vector_typ midsize order bittyp in - E_app (append, - [e1; - E_aux (E_cast (midtyp, - E_aux (E_app (mk_id "slice_slice_concat", - [vector1; start1; length1; vector2; start2; length2]), - (Unknown,empty_tannot))),(Unknown,empty_tannot))]) + let midsize = nminus size size1 in begin + match solve env midsize with + | Some c -> + let midtyp = vector_typ (nconstant c) order bittyp in + E_app (append, + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]), + (Unknown,empty_tannot))),(Unknown,empty_tannot))]) + | _ -> + E_app (append, + [e1; + E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]), + (Unknown,empty_tannot))]) + end (* variable-range @ variable-range *) | [E_aux (E_app (subrange1, @@ -3696,10 +3724,10 @@ let rewrite_app env typ (id,args) = [vector2; start2; end2]),_)] when is_subrange subrange1 && is_subrange subrange2 && not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> - E_cast (typ, - E_aux (E_app (mk_id "subrange_subrange_concat", - [vector1; start1; end1; vector2; start2; end2]), - (Unknown,empty_tannot))) + try_cast_to_typ + (E_aux (E_app (mk_id "subrange_subrange_concat", + [vector1; start1; end1; vector2; start2; end2]), + (Unknown,empty_tannot))) (* variable-slice @ variable-slice *) | [E_aux (E_app (slice1, @@ -3708,9 +3736,9 @@ let rewrite_app env typ (id,args) = [vector2; start2; length2]),_)] when is_slice slice1 && is_slice slice2 && not (is_constant length1 || is_constant length2) -> - E_cast (typ, - E_aux (E_app (mk_id "slice_slice_concat", - [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) + try_cast_to_typ + (E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) | [E_aux (E_app (append1, [e1; @@ -3721,16 +3749,25 @@ let rewrite_app env typ (id,args) = not (is_constant length1 || is_constant length2) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in - let midsize = nminus size size1 in - let midtyp = vector_typ midsize order bittyp in - E_cast (typ, - E_aux (E_app (mk_id "append", + let midsize = nminus size size1 in begin + match solve env midsize with + | Some c -> + let midtyp = vector_typ (nconstant c) order bittyp in + try_cast_to_typ + (E_aux (E_app (mk_id "append", [e1; E_aux (E_cast (midtyp, E_aux (E_app (mk_id "slice_zeros_concat", [vector1; start1; length1; length2]),(Unknown,empty_tannot))),(Unknown,empty_tannot))]), (Unknown,empty_tannot))) - + | _ -> + try_cast_to_typ + (E_aux (E_app (mk_id "append", + [e1; + E_aux (E_app (mk_id "slice_zeros_concat", + [vector1; start1; length1; length2]),(Unknown,empty_tannot))]), + (Unknown,empty_tannot))) + end | _ -> E_app (id,args) else if is_id env (Id "eq_vec") id then -- cgit v1.2.3 From f9282ab5dec29d7ec99d473d013d32b41a0b8dbc Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 7 Aug 2018 11:02:09 +0100 Subject: Improve cast introduction for Lem Handles mutable variables and conditionals (there are still some corner cases that don't appear in Aarch64 to do). The pretty printer is now back to preferring to use concrete types, but has a special case for casts to print more general types. --- src/monomorphise.ml | 65 ++++++++++++++++++++++++++++++++++++++----------- src/pretty_print_lem.ml | 35 ++++++++++++++------------ 2 files changed, 71 insertions(+), 29 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index e9e2c6b6..ab6d9e2d 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3912,7 +3912,7 @@ let simplify_size_nexp env quant_kids (Nexp_aux (_,l) as 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 function call to change mword 'n to (say) mword ty16, and vice versa. *) -let make_bitvector_cast_fns env quant_kids src_typ target_typ = +let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ = let genunk = Generated Unknown in let fresh = let counter = ref 0 in @@ -3945,7 +3945,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = P_aux (P_id var,(Generated src_l,src_ann)), E_aux (E_cast (tar_typ', - E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), + E_aux (E_app (Id_aux (Id cast_name, genunk), [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))), (genunk, tar_ann)) | _ -> @@ -3971,12 +3971,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = (fun var exp -> let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (one_target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)), - E_aux (E_app (Id_aux (Id "bitvector_cast",genunk), + E_aux (E_app (Id_aux (Id cast_name,genunk), [E_aux (E_id var,(genunk,src_ann))]),(genunk,tar_ann))),(genunk,tar_ann)), exp),(genunk,exp_ann))), (fun (E_aux (_,(exp_l,exp_ann)) as exp) -> E_aux (E_cast (one_target_typ, - E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), [exp]), (Generated exp_l,tar_ann))), + E_aux (E_app (Id_aux (Id cast_name, genunk), [exp]), (Generated exp_l,tar_ann))), (Generated exp_l,tar_ann))) | _ -> (fun var exp -> @@ -3991,12 +3991,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = (* TODO: bound vars *) let make_bitvector_env_casts env quant_kids (kid,i) exp = - let mk_cast var typ exp = (fst (make_bitvector_cast_fns env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in + let mk_cast var typ exp = (fst (make_bitvector_cast_fns "bitvector_cast_in" env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in let locals = Env.get_locals env in 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 env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns env quant_kids typ target_typ)) 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 rec extract_value_from_guard var (E_aux (e,_)) = match e with @@ -4023,6 +4023,12 @@ let fill_in_type env typ = subst_src_typ subst typ (* TODO: top-level patterns *) +(* TODO: proper environment tracking for variables. Currently we pretend that + we can print the type of a variable in the top-level environment, but in + practice they might be below a case split. Note that we'd also need to + provide some way for the Lem pretty printer to know what to use; currently + we just use two names for the cast, bitvector_cast_in and bitvector_cast_out, + to let the pretty printer know whether to use the top-level environment. *) let add_bitvector_casts (Defs defs) = let rewrite_body id quant_kids top_env ret_typ exp = let rewrite_aux (e,ann) = @@ -4039,13 +4045,13 @@ let add_bitvector_casts (Defs defs) = 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 - make_bitvector_cast_exp env quant_kids src_typ result_typ + 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 - make_bitvector_cast_exp env quant_kids src_typ result_typ + 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) | _ -> @@ -4056,15 +4062,46 @@ let add_bitvector_casts (Defs defs) = E_aux (E_case (exp', List.map map_case cases),ann) | _ -> E_aux (e,ann) end + | E_if (e1,e2,e3) -> + let env = env_of_annot ann in + let result_typ = Env.base_typ_of env (typ_of_annot ann) in + let rec extract (E_aux (e,_)) = + match e with + | 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" -> + (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 = "and_bool" -> + extract x @ extract y + | _ -> [] + in + let insts = extract e1 in + let e2' = List.fold_left (fun body inst -> + make_bitvector_env_casts env quant_kids inst body) e2 insts in + let insts = List.fold_left (fun insts (kid,i) -> + KBindings.add kid (nconstant i) insts) KBindings.empty insts in + let src_typ = subst_src_typ insts result_typ in + let e2' = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ e2' in + E_aux (E_if (e1,e2',e3), ann) | E_return e' -> - E_aux (E_return (make_bitvector_cast_exp top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann) - (* TODO: (env_of_annot ann) isn't suitable, because it contains - constraints revealing the case splits involved; needs a more - subtle approach *) + 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 (env_of_annot ann) quant_kids (fill_in_type (env_of e') (typ_of e')) + 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_id id -> begin + let env = env_of_annot ann in + match Env.lookup_id id env with + | Local (Mutable, vtyp) -> + make_bitvector_cast_exp "bitvector_cast_in" top_env quant_kids + (fill_in_type (env_of_annot ann) (typ_of_annot ann)) + vtyp + (E_aux (e,ann)) + | _ -> E_aux (e,ann) + end | _ -> E_aux (e,ann) in let open Rewriter in @@ -4089,7 +4126,7 @@ let add_bitvector_casts (Defs defs) = let body = rewrite_body id quant_kids body_env ret_typ body in (* Also add a cast around the entire function clause body, if necessary *) let body = - make_bitvector_cast_exp fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body + make_bitvector_cast_exp "bitvector_cast_out" fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body in let pexp = construct_pexp (pat,guard,body,annot) in FCL_aux (FCL_Funcl (id,pexp),fcl_ann) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 75284418..bef54f05 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -65,8 +65,9 @@ let opt_mwords = ref false type context = { early_ret : bool; bound_nexps : NexpSet.t; + top_env : Env.t } -let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty } +let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty; top_env = Env.empty } let print_to_from_interp_value = ref false let langlebar = string "<|" @@ -328,10 +329,9 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_arg_order o -> empty in typ', atomic_typ -(* Check for variables in types that would be pretty-printed and are not - bound in the val spec of the function. *) +(* Check for variables in types that would be pretty-printed. *) let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) = - NexpSet.diff (lem_nexps_of_typ typ) ctxt.bound_nexps + lem_nexps_of_typ typ |> NexpSet.exists (fun nexp -> not (is_nexp_constant nexp)) let replace_typ_size ctxt env (Typ_aux (t,a)) = @@ -341,14 +341,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let mk_typ nexp = Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_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 @@ -760,8 +760,12 @@ let doc_exp_lem, doc_let_lem = let env = env_of full_exp in let t = Env.expand_synonyms env (typ_of full_exp) in let eff = effect_of full_exp in - if typ_needs_printed t - then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true) + if typ_needs_printed t then + if Id.compare f (mk_id "bitvector_cast_out") <> 0 + then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true) + (* TODO: coordinate with the code in monomorphise.ml to find the correct + typing environment to use *) + else (align (group (prefix 0 1 epp (doc_tannot_lem ctxt ctxt.top_env (effectful eff) t))), true) else (epp, aexp_needed) in liftR (if aexp_needed then parens (align taepp) else taepp) end @@ -1255,7 +1259,8 @@ let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) = let pat,guard,exp,(l,_) = destruct_pexp pexp in let ctxt = { early_ret = contains_early_return exp; - bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ) } in + bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ); + top_env = env_of_annot annot } in let pats, bind = untuple_args_pat pat in let patspp = separate_map space (doc_pat_lem ctxt true) pats in let _ = match guard with -- cgit v1.2.3 From e9ac694490707b29cf68ca3aefce46331149c003 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 7 Aug 2018 11:13:07 +0100 Subject: Fix propagation of overly-specific types in early_return rewrite --- src/rewrites.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index 5ed174ea..0a8c8156 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4381,6 +4381,8 @@ let rewrite_defs_lem = [ ("sizeof", rewrite_sizeof); ("early_return", rewrite_defs_early_return); ("fix_val_specs", rewrite_fix_val_specs); + (* early_return currently breaks the types *) + ("recheck_defs", recheck_defs); ("remove_blocks", rewrite_defs_remove_blocks); ("letbind_effects", rewrite_defs_letbind_effects); ("remove_e_assign", rewrite_defs_remove_e_assign); -- cgit v1.2.3 From 88fbe39a24a9432a58bc9998130f0b075344ef4c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 7 Aug 2018 14:50:07 +0100 Subject: Lem: print more bitvector types Especially for return expressions, which fixes a test case --- src/pretty_print_lem.ml | 59 ++++++++++++++++++++++++++++--------------------- 1 file changed, 34 insertions(+), 25 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index bef54f05..e9e6befb 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -352,18 +352,21 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = end | _ -> None -let doc_tannot_lem ctxt env eff typ = - let of_typ typ = - let ta = doc_typ_lem typ in - if eff then string " : M " ^^ parens ta - else string " : " ^^ ta - in +let make_printable_type ctxt env typ = if contains_t_pp_var ctxt typ then match replace_typ_size ctxt env typ with - | None -> empty - | Some typ -> of_typ typ - else of_typ typ + | None -> None + | Some typ -> Some typ + else Some typ + +let doc_tannot_lem ctxt env eff typ = + match make_printable_type ctxt env typ with + | None -> empty + | Some typ -> + let ta = doc_typ_lem typ in + if eff then string " : M " ^^ parens ta + else string " : " ^^ ta let doc_lit_lem (L_aux(lit,l)) = match lit with @@ -495,8 +498,9 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with parens (separate comma_sp (List.map2 doc_elem typs pats)) | P_typ(typ,p) -> let doc_p = doc_pat_lem ctxt true p in - if contains_t_pp_var ctxt typ then doc_p - else parens (doc_op colon doc_p (doc_typ_lem typ)) + (match make_printable_type ctxt (env_of_annot (l,annot)) typ with + | None -> doc_p + | Some typ -> parens (doc_op colon doc_p (doc_typ_lem typ))) | P_vector pats -> let ppp = brackets (separate_map semi (doc_pat_lem ctxt true) pats) in if apat_needed then parens ppp else ppp @@ -727,14 +731,16 @@ let doc_exp_lem, doc_let_lem = | [exp] -> let epp = separate space [string "early_return"; expY exp] in let aexp_needed, tepp = - if contains_t_pp_var ctxt (typ_of exp) || - contains_t_pp_var ctxt (typ_of full_exp) then - aexp_needed, epp - else - let tannot = separate space [string "MR"; - doc_atomic_typ_lem false (typ_of full_exp); - doc_atomic_typ_lem false (typ_of exp)] in - true, doc_op colon epp tannot in + match Util.option_bind (make_printable_type ctxt ctxt.top_env) + (Env.get_ret_typ (env_of exp)), + make_printable_type ctxt (env_of full_exp) (typ_of full_exp) with + | Some typ, Some full_typ -> + let tannot = separate space [string "MR"; + doc_atomic_typ_lem false full_typ; + doc_atomic_typ_lem false typ] in + true, doc_op colon epp tannot + | _ -> aexp_needed, epp + in if aexp_needed then parens tepp else tepp | _ -> raise (Reporting_basic.err_unreachable l "Unexpected number of arguments for early_return builtin") @@ -920,12 +926,15 @@ let doc_exp_lem, doc_let_lem = "pretty-printing non-constant sizeof expressions to Lem not supported")) | E_return r -> let ta = - if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r) - then empty - else separate space - [string ": MR"; - parens (doc_typ_lem (typ_of full_exp)); - parens (doc_typ_lem (typ_of r))] in + match Util.option_bind (make_printable_type ctxt ctxt.top_env) (Env.get_ret_typ (env_of full_exp)), + make_printable_type ctxt (env_of r) (typ_of r) with + | Some full_typ, Some r_typ -> + separate space + [string ": MR"; + parens (doc_typ_lem full_typ); + parens (doc_typ_lem r_typ)] + | _ -> empty + in align (parens (string "early_return" ^//^ expV true r ^//^ ta)) | E_constraint _ -> string "true" | E_internal_value _ -> -- cgit v1.2.3 From e3933fd35222995a3b44015aa288fdf34696bc8a Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 7 Aug 2018 15:47:21 +0100 Subject: Revert "Warnings: deal with all the deprecation warnings" One day we will be free from the 4.02.3 menace, but today is not that day. :( This should fix Sail on Jenkins This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414. --- src/latex.ml | 2 +- src/lem_interp/printing_functions.ml | 2 +- src/ocaml_backend.ml | 2 +- src/pretty_print_lem.ml | 2 +- src/process_file.ml | 6 +++--- src/rewriter.ml | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index 39db43db..0520d074 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -126,7 +126,7 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l | Some l -> Printf.sprintf "\\label{%s}" l in let cmd = !opt_prefix_latex ^ prefix ^ cmd in - let lcmd = String.lowercase_ascii cmd in (* lowercase to avoid file names differing only by case *) + let lcmd = String.lowercase cmd in (* lowercase to avoid file names differing only by case *) if StringSet.mem lcmd !commands then latex_command ~label:label dir (cmd ^ "v") no_loc annot else diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index c17e879f..a5cb96ff 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -481,7 +481,7 @@ let rec instr_parms_to_string ps = let pad n s = if String.length s < n then s ^ String.make (n-String.length s) ' ' else s let instruction_to_string (name, parms) = - ((*pad 5*) (String.lowercase_ascii name)) ^ " " ^ instr_parms_to_string parms + ((*pad 5*) (String.lowercase name)) ^ " " ^ instr_parms_to_string parms let print_backtrace_compact printer (IState(stack,_)) = List.iter (fun (e,(env,mem)) -> print_exp printer env mem true e) (compact_stack stack) diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 3e4dc650..236c4222 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -673,7 +673,7 @@ let ocaml_main spec sail_dir = with | End_of_file -> close_in chan; lines := List.rev !lines end; - (("open " ^ String.capitalize_ascii spec ^ ";;\n\n") :: !lines + (("open " ^ String.capitalize spec ^ ";;\n\n") :: !lines @ [ " zinitializze_registers ();"; if !opt_trace_ocaml then " Sail_lib.opt_trace := true;" else " ();"; " Printexc.record_backtrace true;"; diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index e9e6befb..d300f699 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -129,7 +129,7 @@ let doc_id_lem_ctor (Id_aux(i,_)) = | Id("nat") -> string "integer" | Id("Some") -> string "Just" | Id("None") -> string "Nothing" - | Id i -> string (fix_id false (String.capitalize_ascii i)) + | Id i -> string (fix_id false (String.capitalize i)) | DeIid x -> string (Util.zencode_string ("op " ^ x)) let deinfix = function diff --git a/src/process_file.ml b/src/process_file.ml index 5fdd3d24..958720ea 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -271,14 +271,14 @@ let output_lem filename libs defs = operators_module ] @ monad_modules in - let isa_thy_name = String.capitalize_ascii filename ^ "_lemmas" in + let isa_thy_name = String.capitalize filename ^ "_lemmas" in let isa_lemmas = separate hardline [ string ("theory " ^ isa_thy_name); string " imports"; string " Sail.Sail2_values_lemmas"; string " Sail.Sail2_state_lemmas"; - string (" " ^ String.capitalize_ascii filename); + string (" " ^ String.capitalize filename); string "begin"; string ""; State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs; @@ -292,7 +292,7 @@ let output_lem filename libs defs = open_output_with_check_unformatted (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) - (o, base_imports @ (String.capitalize_ascii types_module :: libs)) + (o, base_imports @ (String.capitalize types_module :: libs)) defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; diff --git a/src/rewriter.ml b/src/rewriter.ml index 01ff62b1..6d88730d 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -266,7 +266,7 @@ let vector_string_to_bit_list l lit = | _ -> raise (Reporting_basic.err_unreachable l "hexchar_to_binlist given unrecognized character") in let s_bin = match lit with - | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase_ascii s_hex))) + | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase s_hex))) | L_bin s_bin -> explode s_bin | _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in -- cgit v1.2.3 From 07cb99b638d118a23cc8610c6cffbf5834b0fa87 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 11:17:21 +0100 Subject: Coq: handle nats like ranges, not atoms --- src/pretty_print_coq.ml | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index dff68092..74d10f44 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -152,7 +152,6 @@ let doc_id id = string (string_id id) let doc_id_type (Id_aux(i,_)) = match i with | Id("int") -> string "Z" - | Id("nat") -> string "Z" | Id i -> string (fix_id false i) | DeIid x -> string (Util.zencode_string ("op " ^ x)) @@ -384,6 +383,11 @@ let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) = let var = nvar kid in let nc = nc_and (nc_lteq low var) (nc_lteq var high) in Some (Typ_aux (Typ_exist ([kid], nc, atom_typ var),Parse_ast.Generated l)) + | Typ_id (Id_aux (Id "nat",_)) -> + let kid = mk_kid "n" in + let var = nvar kid in + Some (Typ_aux (Typ_exist ([kid], nc_gteq var (nconstant Nat_big_num.zero), atom_typ var), + Generated l)) | _ -> None let expand_range_type typ = Util.option_default typ (maybe_expand_range_type typ) @@ -428,7 +432,8 @@ let doc_typ, doc_atomic_typ = | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> let tpp = string "register_ref regstate register_value " ^^ typ etyp in if atyp_needed then parens tpp else tpp - | Typ_app(Id_aux (Id "range", _), _) -> + | Typ_app(Id_aux (Id "range", _), _) + | Typ_id (Id_aux (Id "nat", _)) -> (match maybe_expand_range_type ty with | Some typ -> atomic_typ atyp_needed typ | None -> raise (Reporting_basic.err_unreachable l "Bad range type")) @@ -805,9 +810,6 @@ let replace_atom_return_type ret_typ = | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),l) -> let kid = mk_kid "_retval" in (* TODO: collision avoidance *) true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Generated l) - | Typ_aux (Typ_id (Id_aux (Id "nat",_)),l) -> - let kid = mk_kid "_retval" in - true, Typ_aux (Typ_exist ([kid], nc_gteq (nvar kid) (nconstant Nat_big_num.zero), atom_typ (nvar kid)),Generated l) | _ -> false, ret_typ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = @@ -816,10 +818,6 @@ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_); Typ_arg_aux(Typ_arg_nexp high,_)]) -> Type_check.prove env (nc_and (nc_eq nexp low) (nc_eq nexp high)) - | Typ_exist (_, _, Typ_aux (Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp _,_)]), _)), - Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_); - Typ_arg_aux(Typ_arg_nexp high,_)]) -> - Type_check.prove env (nc_eq low high) | _ -> false let prefix_recordtype = true @@ -1618,10 +1616,6 @@ let rec atom_constraint ctxt (pat, typ) = | _ -> Some (bquote ^^ braces (string "ArithFact" ^^ space ^^ parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp))))) - | P_aux (P_id id, _), - Typ_aux (Typ_id (Id_aux (Id "nat",_)),_) -> - Some (bquote ^^ braces (string "ArithFact" ^^ space ^^ - parens (doc_op (string ">=") (doc_id id) (string "0")))) | P_aux (P_typ (_,p),_), _ -> atom_constraint ctxt (p, typ) | _ -> None -- cgit v1.2.3 From 93b8618d2b1c14c58340eae4873632fb4d7c1a20 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 11:17:46 +0100 Subject: Coq: decompose dependent pairs at internal_plet as well as let --- src/pretty_print_coq.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 74d10f44..d55e226b 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1315,9 +1315,11 @@ let doc_exp_lem, doc_let_lem = match pat with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" - | P_aux (P_id id,_) -> + | P_aux (P_id id,_) + when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) -> separate space [string ">>= fun"; doc_id id; bigarrow] - | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) + when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow] -- cgit v1.2.3 From 9368ae447257efea8b0af8725350e195b2bb9731 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 11:18:00 +0100 Subject: Coq: tidy up debugging messages --- src/pretty_print_coq.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index d55e226b..4e2193c1 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1080,8 +1080,8 @@ let doc_exp_lem, doc_let_lem = let typ_from_fn = expand_range_type typ_from_fn_plain in (* TODO: more sophisticated check *) let () = - debug ctxt (lazy ("arg type found " ^ string_of_typ arg_ty_plain)); - debug ctxt (lazy ("arg type expected " ^ string_of_typ typ_from_fn_plain)) + debug ctxt (lazy (" arg type found " ^ string_of_typ arg_ty_plain)); + debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn_plain)) in match destruct_exist env arg_ty, destruct_exist env typ_from_fn with | Some _, None -> parens (string "projT1 " ^^ arg_pp) @@ -1108,8 +1108,8 @@ let doc_exp_lem, doc_let_lem = if is_no_Z_proof_fn env f then ret_typ_inst else snd (replace_atom_return_type ret_typ_inst) in let () = - debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); - debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) + debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); + debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) in let unpack, build_ex, in_typ, out_typ = match ret_typ_inst, ann_typ with -- cgit v1.2.3 From 58f585cfd9b1f5fd7724fdcb71b46179524653ca Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 15:28:38 +0100 Subject: Coq: debugging on top-level lets --- src/pretty_print_coq.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 4e2193c1..90276cb3 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1929,6 +1929,7 @@ let doc_val pat exp = in let env = env_of exp in let typ = expand_range_type (Env.expand_synonyms env (typ_of exp)) in + let ctxt = { empty_ctxt with debug = List.mem (string_of_id id) (!opt_debug_on) } in let id, opt_unpack = match destruct_exist env typ with | None -> id, None @@ -1943,7 +1944,7 @@ let doc_val pat exp = let idpp = doc_id id in let basepp = group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^/^ - doc_exp_lem empty_ctxt false exp ^^ dot) ^^ hardline + doc_exp_lem ctxt false exp ^^ dot) ^^ hardline in match opt_unpack with | None -> basepp ^^ hardline -- cgit v1.2.3 From 3f2205e552d850c5eb128f4763ea0e4016e43ad2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 10 Aug 2018 18:37:24 +0100 Subject: Coq: add some of string library --- src/process_file.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'src') diff --git a/src/process_file.ml b/src/process_file.ml index 958720ea..96029587 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -309,6 +309,7 @@ let output_coq filename libs defs = let base_imports = [ "Sail2_instr_kinds"; "Sail2_values"; + "Sail2_string"; operators_module ] @ monad_modules in -- cgit v1.2.3 From 67b48947300cf4ac5f792dc31436cb241a4c7126 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Sun, 12 Aug 2018 15:23:22 +0100 Subject: Coq: handle enums in binders, make top-level patterns exhaustive --- src/pretty_print_coq.ml | 21 ++++++++++++++++----- src/rewriter.mli | 2 ++ src/rewrites.ml | 36 +++++++++++++++++++++++++++++++++++- 3 files changed, 53 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 90276cb3..d5aa7151 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -105,6 +105,11 @@ let is_number_char c = c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' || c = '6' || c = '7' || c = '8' || c = '9' +let is_enum env id = + match Env.lookup_id id env with + | Enum _ -> true + | _ -> false + let rec fix_id remove_tick name = match name with | "assert" | "lsl" @@ -1316,10 +1321,12 @@ let doc_exp_lem, doc_let_lem = | 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 (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 (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 (pat, typ_of e1); bigarrow] @@ -1373,12 +1380,14 @@ let doc_exp_lem, doc_let_lem = (* 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 (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 (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]) (top_exp ctxt false e) @@ -1730,7 +1739,9 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let exp_typ = Env.expand_synonyms env typ in match p with | P_id id - | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) -> + | P_typ (_,P_aux (P_id id,_)) + when Util.is_none (is_auto_decomposed_exist env exp_typ) && + not (is_enum env id) -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) | _ -> (used_a_pattern := true; diff --git a/src/rewriter.mli b/src/rewriter.mli index 3e582071..da4702b5 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -74,6 +74,8 @@ val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp val rewrite_pat : tannot rewriters -> tannot pat -> tannot pat +val rewrite_pexp : tannot rewriters -> tannot pexp -> tannot pexp + val rewrite_let : tannot rewriters -> tannot letbind -> tannot letbind val rewrite_def : tannot rewriters -> tannot def -> tannot def diff --git a/src/rewrites.ml b/src/rewrites.ml index 0a8c8156..825073b4 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4043,7 +4043,10 @@ let rewrite_defs_realise_mappings (Defs defs) = (* Rewrite to make all pattern matches in Coq output exhaustive. - Assumes that guards, vector patterns, etc have been rewritten already. *) + Assumes that guards, vector patterns, etc have been rewritten already, + and the scattered functions have been merged. + Will add escape effect where a default is needed, so effects will + need recalculated afterwards. *) let opt_coq_warn_nonexhaustive = ref false @@ -4285,6 +4288,37 @@ let rewrite_case (e,ann) = end | _ -> E_aux (e,ann) +let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) = + let id,fcl_ann = + match fcls with + | FCL_aux (FCL_Funcl (id,_),ann) :: _ -> id,ann + | [] -> raise (Reporting_basic.err_unreachable (fst f_ann) + "Empty function") + in + let env = env_of_annot fcl_ann in + let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in + let rps = List.fold_left process_funcl [RP_any] fcls in + let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) -> + FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann)) + fcls in + match rps with + | [] -> FD_aux (FD_function (r,t,e,fcls'),f_ann) + | (example::_) -> + let _ = + if !opt_coq_warn_nonexhaustive + then Reporting_basic.print_err false false + (fst f_ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in + + let l = Parse_ast.Generated Parse_ast.Unknown in + let p = P_aux (P_wild, (l, empty_tannot)) in + let ann' = mk_tannot env (typ_of_annot fcl_ann) (mk_effect [BE_escape]) in + (* TODO: use an expression that specifically indicates a failed pattern match *) + let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in + let default = FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (p,b),(l,empty_tannot))),fcl_ann) in + + FD_aux (FD_function (r,t,e,fcls'@[default]),f_ann) + + let rewrite = let alg = { id_exp_alg with e_aux = rewrite_case } in rewrite_defs_base -- cgit v1.2.3 From 3001c5dbdfbd060500df141d8112af5c1021f347 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 13:52:50 +0100 Subject: Guarded clauses rewrite: variable patterns subsume enums Prevents redundant clauses. --- src/rewrites.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index 825073b4..aee57977 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1084,9 +1084,11 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = | _, P_typ (_,pat2) -> subsumes_pat pat1 pat2 | P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) -> if id1 = id2 then Some [] - else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound && - Env.lookup_id aid2 (env_of_annot annot2) = Unbound - then Some [(id2,id1)] else None + else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound + then if Env.lookup_id aid2 (env_of_annot annot2) = Unbound + then Some [(id2,id1)] + else Some [] + else None | P_id id1, _ -> if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None | P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2 -- cgit v1.2.3 From 616b770c1fef06b9b5322d0dfde729594abd279a Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 16:50:38 +0100 Subject: Coq: drop redundant final wildcard clauses Deals with pattern matches generated from mappings, plus the occasional error. --- src/rewrites.ml | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index aee57977..47c7e923 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4048,7 +4048,15 @@ let rewrite_defs_realise_mappings (Defs defs) = Assumes that guards, vector patterns, etc have been rewritten already, and the scattered functions have been merged. Will add escape effect where a default is needed, so effects will - need recalculated afterwards. *) + need recalculated afterwards. + + Also detects and removes redundant wildcard patterns at the end of the match. + (We could do more, but this is sufficient to deal with the code generated by + the mappings rewrites.) + + Note: if this naive implementation turns out to be too slow or buggy, we + could look at implementing Maranget JFP 17(3), 2007. + *) let opt_coq_warn_nonexhaustive = ref false @@ -4266,12 +4274,38 @@ let process_pexp env = raise (Reporting_basic.err_unreachable l "Guarded pattern should have been rewritten away") +(* We do some minimal redundancy checking to remove bogus wildcard patterns here *) +let check_cases process is_wild loc_of cases = + let rec aux rps acc = function + | [] -> acc, rps + | [p] when is_wild p && match rps with [] -> true | _ -> false -> + let () = Reporting_basic.print_err false false + (loc_of p) "Match checking" "Redundant wildcard clause" in + acc, [] + | h::t -> aux (process rps h) (h::acc) t + in + let cases, rps = aux [RP_any] [] cases in + List.rev cases, rps + +let pexp_is_wild = function + | (Pat_aux (Pat_exp (P_aux (P_wild,_),_),_)) -> true + | _ -> false + +let pexp_loc = function + | (Pat_aux (Pat_exp (P_aux (_,(l,_)),_),_)) -> l + | (Pat_aux (Pat_when (P_aux (_,(l,_)),_,_),_)) -> l + +let funcl_is_wild = function + | (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp_is_wild pexp + +let funcl_loc (FCL_aux (_,(l,_))) = l + let rewrite_case (e,ann) = match e with | E_case (e1,cases) -> begin let env = env_of_annot ann in - let rps = List.fold_left (process_pexp env) [RP_any] cases in + let cases, rps = check_cases (process_pexp env) pexp_is_wild pexp_loc cases in match rps with | [] -> E_aux (E_case (e1,cases),ann) | (example::_) -> @@ -4299,7 +4333,7 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) = in let env = env_of_annot fcl_ann in let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in - let rps = List.fold_left process_funcl [RP_any] fcls in + let fcls, rps = check_cases process_funcl funcl_is_wild funcl_loc fcls in let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) -> FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann)) fcls in -- cgit v1.2.3