From 449e8a54371b0c707bb7e3c5acdb4fd475a016d0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 3 May 2018 11:03:27 +0100 Subject: Work in progress on the coq backend - originally based on the Lem backend - added externs to some of the library files and tests - added wildcard to extern valspecs in parser - added Type_check.get_val_spec_orig to return the valspec with the function's original names for bound type variables Note that most of the tests will fail currently --- src/parser.mly | 12 +- src/pretty_print_coq.ml | 1325 +++++++++++++++++++++++++++++++++++++++++++++++ src/process_file.ml | 26 + src/process_file.mli | 2 + src/sail.ml | 14 + src/state.ml | 79 +++ src/type_check.ml | 7 + src/type_check.mli | 7 +- 8 files changed, 1467 insertions(+), 5 deletions(-) create mode 100644 src/pretty_print_coq.ml (limited to 'src') diff --git a/src/parser.mly b/src/parser.mly index 0846d4bb..3b7a435b 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -61,9 +61,11 @@ let default_opt x = function | None -> x | Some y -> y -let assoc_opt key assocs = +let assoc_opt key (assocs, default) = try Some (List.assoc key assocs) with - | Not_found -> None + | Not_found -> default + +let cons_fst h (t,x) = (h::t,x) let string_of_id = function | Id_aux (Id str, _) -> str @@ -1193,9 +1195,11 @@ let_def: externs: | id Colon String - { [(string_of_id $1, $3)] } + { ([(string_of_id $1, $3)], None) } + | Under Colon String + { ([], Some $3) } | id Colon String Comma externs - { (string_of_id $1, $3) :: $5 } + { cons_fst (string_of_id $1, $3) $5 } val_spec_def: | Doc val_spec_def diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml new file mode 100644 index 00000000..347b691d --- /dev/null +++ b/src/pretty_print_coq.ml @@ -0,0 +1,1325 @@ +(**************************************************************************) +(* 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. *) +(**************************************************************************) + +(* TODO: + | DEF_reg_dec dec -> group (doc_dec_lem dec) + | DEF_fundef fdef -> group (doc_fundef_lem fdef) ^/^ hardline + | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline + + doc_id / doc_id_type with a DeIid ...* + fix_id + doc_quant_item on constraints + type quantifiers in records, unions + update notation for records + register_refs? + should I control the nexps somewhat? + L_real + should P_var produce an "as"? + does doc_pat detuple too much? + Import ListNotations + P_record? + type quantifiers and constraints in definitions + should atom types be specially treated? (probably not in doc_typ, but elsewhere) + ordering of kids in existential types is fragile! + doc_nexp needs precedence fixed (i.e., parens inserted) + doc_exp_lem assignments, foreach (etc), early_return (supress type when it's not ASTable?), + application (do we need to bother printing types so much?), casts (probably ought to print type), + record update + lem/isabelle formatting hacks + move List imports +*) + +open Type_check +open Ast +open Ast_util +open Rewriter +open PPrint +open Pretty_print_common + +(**************************************************************************** + * PPrint-based sail-to-coq pprinter +****************************************************************************) + +type context = { + early_ret : bool; + bound_nexps : NexpSet.t; +} +let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty } + +let langlebar = string "<|" +let ranglebar = string "|>" +let anglebars = enclose langlebar ranglebar +let enclose_record = enclose (string "{| ") (string " |}") +let bigarrow = string "=>" + +let separate_opt s f l = separate s (Util.map_filter f l) + +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 rec fix_id remove_tick name = match name with + | "assert" + | "lsl" + | "lsr" + | "asr" + | "type" + | "fun" + | "function" + | "raise" + | "try" + | "match" + | "with" + | "check" + | "field" + | "LT" + | "GT" + | "EQ" + | "integer" + -> name ^ "'" + | _ -> + if String.contains name '#' then + fix_id remove_tick (String.concat "_" (Util.split_on_char '#' name)) + else if String.contains name '?' then + fix_id remove_tick (String.concat "_pat_" (Util.split_on_char '?' name)) + else if name.[0] = '\'' then + let var = String.sub name 1 (String.length name - 1) in + if remove_tick then var else (var ^ "'") + else if is_number_char(name.[0]) then + ("v" ^ name ^ "'") + else name + +let doc_id (Id_aux(i,_)) = + match i with + | Id i -> string (fix_id false i) + | DeIid x -> + (* add an extra space through empty to avoid a closing-comment + * token in case of x ending with star. *) + parens (separate space [colon; string x; empty]) + +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 -> + (* add an extra space through empty to avoid a closing-comment + * token in case of x ending with star. *) + parens (separate space [colon; string x; empty]) + +let doc_id_ctor (Id_aux(i,_)) = + match i with + | Id i -> string (fix_id false i) + | DeIid x -> + (* add an extra space through empty to avoid a closing-comment + * token in case of x ending with star. *) + separate space [colon; string x; empty] + +let doc_var_lem kid = string (fix_id true (string_of_kid kid)) + +let doc_docstring_lem (l, _) = match l with + | Parse_ast.Documented (str, _) -> string ("(*" ^ str ^ "*)") ^^ hardline + | _ -> empty + +let simple_annot l typ = (Parse_ast.Generated l, Some (Env.empty, typ, no_effect)) +let simple_num l n = E_aux ( + E_lit (L_aux (L_num n, Parse_ast.Generated l)), + simple_annot (Parse_ast.Generated l) + (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l)))) + +let effectful_set = function + | [] -> false + | _ -> true + (*List.exists + (fun (BE_aux (eff,_)) -> + match eff with + | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem + | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet + | BE_escape -> true + | _ -> false)*) + +let effectful (Effect_aux (Effect_set effs, _)) = effectful_set effs + +let is_regtyp (Typ_aux (typ, _)) env = match typ with + | Typ_app(id, _) when string_of_id id = "register" -> true + | _ -> false + +let doc_nexp nexp = + let (Nexp_aux (nexp, l) as full_nexp) = nexp_simp nexp in + match nexp with + | Nexp_constant i -> string (Big_int.to_string i) + | Nexp_var v -> doc_var_lem v + | Nexp_id id -> doc_id id + | Nexp_times (n1, n2) -> separate space [doc_nexp n1; star; doc_nexp n2] + | Nexp_sum (n1, n2) -> separate space [doc_nexp n1; plus; doc_nexp n2] + | Nexp_minus (n1, n2) -> separate space [doc_nexp n1; minus; doc_nexp n2] + | Nexp_exp n -> separate space [string "2"; caret; doc_nexp n] + | Nexp_neg n -> separate space [minus; doc_nexp n] + | _ -> + raise (Reporting_basic.err_unreachable l + ("cannot pretty-print nexp \"" ^ string_of_nexp full_nexp ^ "\"")) + +(* Rewrite mangled names of type variables to the original names *) +let rec orig_nexp (Nexp_aux (nexp, l)) = + let rewrap nexp = Nexp_aux (nexp, l) in + match nexp with + | Nexp_var kid -> rewrap (Nexp_var (orig_kid kid)) + | Nexp_times (n1, n2) -> rewrap (Nexp_times (orig_nexp n1, orig_nexp n2)) + | Nexp_sum (n1, n2) -> rewrap (Nexp_sum (orig_nexp n1, orig_nexp n2)) + | Nexp_minus (n1, n2) -> rewrap (Nexp_minus (orig_nexp n1, orig_nexp n2)) + | Nexp_exp n -> rewrap (Nexp_exp (orig_nexp n)) + | Nexp_neg n -> rewrap (Nexp_neg (orig_nexp n)) + | _ -> rewrap nexp + +(* Returns the set of type variables that will appear in the Lem output, + which may be smaller than those in the Sail type. May need to be + updated with doc_typ_lem *) +let rec lem_nexps_of_typ (Typ_aux (t,_)) = + let trec = lem_nexps_of_typ in + match t with + | Typ_id _ -> NexpSet.empty + | Typ_var kid -> NexpSet.singleton (orig_nexp (nvar kid)) + | Typ_fn (t1,t2,_) -> NexpSet.union (trec t1) (trec t2) + | Typ_tup ts -> + List.fold_left (fun s t -> NexpSet.union s (trec t)) + NexpSet.empty ts + | Typ_app(Id_aux (Id "vector", _), [ + Typ_arg_aux (Typ_arg_nexp m, _); + Typ_arg_aux (Typ_arg_order ord, _); + Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> + let m = nexp_simp m in + if is_bit_typ elem_typ && not (is_nexp_constant m) then + NexpSet.singleton (orig_nexp m) + else trec elem_typ + | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> + trec etyp + | Typ_app(Id_aux (Id "range", _),_) + | Typ_app(Id_aux (Id "implicit", _),_) + | Typ_app(Id_aux (Id "atom", _), _) -> NexpSet.empty + | Typ_app (_,tas) -> + List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg ta)) + NexpSet.empty tas + | Typ_exist (kids,_,t) -> trec t +and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) = + match ta with + | Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp)) + | Typ_arg_typ typ -> lem_nexps_of_typ typ + | Typ_arg_order _ -> NexpSet.empty + +let lem_tyvars_of_typ typ = + NexpSet.fold (fun nexp ks -> KidSet.union ks (tyvars_of_nexp nexp)) + (lem_nexps_of_typ typ) KidSet.empty + +(* When making changes here, check whether they affect lem_tyvars_of_typ *) +let doc_typ, doc_atomic_typ = + (* following the structure of parser for precedence *) + let rec typ ty = fn_typ true ty + and typ' ty = fn_typ false ty + and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with + | Typ_fn(arg,ret,efct) -> + let ret_typ = + if effectful efct + then separate space [string "M"; fn_typ true ret] + else separate space [fn_typ false ret] in + let arg_typs = match arg with + | Typ_aux (Typ_tup typs, _) -> + List.map (app_typ false) typs + | _ -> [tup_typ false arg] in + let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [ret_typ]) in + (* once we have proper excetions we need to know what the exceptions type is *) + if atyp_needed then parens tpp else tpp + | _ -> tup_typ atyp_needed ty + and tup_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with + | Typ_tup typs -> + parens (separate_map (space ^^ star ^^ space) (app_typ false) typs) + | _ -> app_typ atyp_needed ty + and app_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with + | Typ_app(Id_aux (Id "vector", _), [ + Typ_arg_aux (Typ_arg_nexp m, _); + Typ_arg_aux (Typ_arg_order ord, _); + Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> + let tpp = match elem_typ with + | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> + string "mword " ^^ doc_nexp (nexp_simp m) + | _ -> string "list" ^^ space ^^ typ elem_typ in + if atyp_needed then parens tpp else tpp + | 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", _),_) -> + (string "Z") + | Typ_app(Id_aux (Id "implicit", _),_) -> + (string "Z") + | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> + (string "Z") + | Typ_app(id,args) -> + let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in + if atyp_needed then parens tpp else tpp + | _ -> atomic_typ atyp_needed ty + and atomic_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with + | Typ_id (Id_aux (Id "bool",_)) -> string "bool" + | Typ_id (Id_aux (Id "bit",_)) -> string "bitU" + | Typ_id (id) -> + (*if List.exists ((=) (string_of_id id)) regtypes + then string "register" + else*) doc_id_type id + | Typ_var v -> doc_var_lem v + | Typ_app _ | Typ_tup _ | Typ_fn _ -> + (* exhaustiveness matters here to avoid infinite loops + * if we add a new Typ constructor *) + let tpp = typ ty in + if atyp_needed then parens tpp else tpp + | Typ_exist (kids,_,ty) -> + let tpp = typ ty in +tpp (* List.fold_left + (fun tpp kid -> braces (separate space [doc_var_lem kid; colon; string "Z"; ampersand; tpp])) + tpp kids*) + and doc_typ_arg (Typ_arg_aux(t,_)) = match t with + | Typ_arg_typ t -> app_typ true t + | Typ_arg_nexp n -> doc_nexp n + | 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. *) +let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) = + NexpSet.diff (lem_nexps_of_typ typ) ctxt.bound_nexps + |> NexpSet.exists (fun nexp -> not (is_nexp_constant nexp)) + +let replace_typ_size ctxt env (Typ_aux (t,a)) = + match t with + | Typ_app (Id_aux (Id "vector",_) as id, [Typ_arg_aux (Typ_arg_nexp size,_);ord;typ']) -> + begin + let mk_typ nexp = + Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_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 + end + | _ -> None + +let doc_tannot_lem ctxt env eff typ = + let of_typ typ = + let ta = doc_typ typ in + if eff then string " : M " ^^ parens ta + else string " : " ^^ ta + in + 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 + +let doc_lit (L_aux(lit,l)) = + match lit with + | L_unit -> utf8string "tt" + | L_zero -> utf8string "B0" + | L_one -> utf8string "B1" + | L_false -> utf8string "false" + | L_true -> utf8string "true" + | L_num i -> + let ipp = Big_int.to_string i in + utf8string 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 -> + utf8string "(return (failwith \"undefined value of unsupported type\"))" + | L_string s -> utf8string ("\"" ^ s ^ "\"") + | L_real s -> + (* Lem does not support decimal syntax, so we translate a string + of the form "x.y" into the ratio (x * 10^len(y) + y) / 10^len(y). + The OCaml library has a conversion function from strings to floats, but + not from floats to ratios. ZArith's Q library does have the latter, but + using this would require adding a dependency on ZArith to Sail. *) + let parts = Util.split_on_char '.' s in + let (num, denom) = match parts with + | [i] -> (Big_int.of_string i, Big_int.of_int 1) + | [i;f] -> + let denom = Big_int.pow_int_positive 10 (String.length f) in + (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom) + | _ -> + raise (Reporting_basic.Fatal_error + (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in + parens (separate space (List.map string [ + "realFromFrac"; Big_int.to_string num; Big_int.to_string denom])) + +let doc_quant_item delimit (QI_aux (qi,_)) = + match qi with + | QI_id (KOpt_aux (KOpt_none kid,_)) -> + Some (delimit (separate space [doc_var_lem kid; colon; string "Z"])) + | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (kind,_)],_),kid),_)) -> begin + match kind with + | BK_type -> Some (delimit (separate space [doc_var_lem kid; colon; string "Type"])) + | BK_int -> Some (delimit (separate space [doc_var_lem kid; colon; string "Z"])) + | BK_order -> None + end + | QI_id _ -> failwith "Quantifier with multiple kinds" + | QI_const nc -> None (* TODO *) + +let doc_typquant_items delimit (TypQ_aux (tq,_)) = + match tq with + | TypQ_tq qis -> separate_opt space (doc_quant_item delimit) qis + | TypQ_no_forall -> empty + +let doc_typquant (TypQ_aux(tq,_)) typ = match tq with +| TypQ_tq ((_ :: _) as qs) -> + string "forall " ^^ separate_opt space (doc_quant_item parens) qs ^^ string ". " ^^ typ +| _ -> typ + +(* Produce Size type constraints for bitvector sizes when using + machine words. Often these will be unnecessary, but this simple + approach will do for now. *) + +let rec typeclass_nexps (Typ_aux(t,_)) = + match t with + | Typ_id _ + | Typ_var _ + -> NexpSet.empty + | Typ_fn (t1,t2,_) -> NexpSet.union (typeclass_nexps t1) (typeclass_nexps t2) + | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts) + | Typ_app (Id_aux (Id "vector",_), + [Typ_arg_aux (Typ_arg_nexp size_nexp,_); + _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) + | Typ_app (Id_aux (Id "itself",_), + [Typ_arg_aux (Typ_arg_nexp size_nexp,_)]) -> + let size_nexp = nexp_simp size_nexp in + if is_nexp_constant size_nexp then NexpSet.empty else + NexpSet.singleton (orig_nexp size_nexp) + | Typ_app _ -> NexpSet.empty + | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *) + +let doc_typschm quants (TypSchm_aux(TypSchm_ts(tq,t),_)) = + let pt = doc_typ t in + if quants then doc_typquant tq pt else pt + +let is_ctor env id = match Env.lookup_id id env with +| Enum _ -> true +| _ -> false + +(*Note: vector concatenation, literal vectors, indexed vectors, and record should + be removed prior to pp. The latter two have never yet been seen +*) +let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot))) = match p with + | P_app(id, ((_ :: _) as pats)) -> + let ppp = doc_unop (doc_id_ctor id) + (parens (separate_map comma (doc_pat ctxt true) pats)) in + if apat_needed then parens ppp else ppp + | P_app(id, []) -> doc_id_ctor id + | P_lit lit -> doc_lit lit + | P_wild -> underscore + | P_id id -> doc_id id + | P_var(p,_) -> doc_pat ctxt true p + | P_as(p,id) -> parens (separate space [doc_pat ctxt true p; string "as"; doc_id id]) + | P_typ(typ,p) -> + let doc_p = doc_pat ctxt true p in + doc_p + (* Type annotations aren't allowed everywhere in patterns in Coq *) + (*parens (doc_op colon doc_p (doc_typ typ))*) + | P_vector pats -> + let ppp = brackets (separate_map semi (doc_pat ctxt true) pats) in + if apat_needed then parens ppp else ppp + | P_vector_concat pats -> + raise (Reporting_basic.err_unreachable l + "vector concatenation patterns should have been removed before pretty-printing") + | P_tup pats -> + (match pats with + | [p] -> doc_pat ctxt apat_needed p + | _ -> parens (separate_map comma_sp (doc_pat ctxt false) pats)) + | P_list pats -> brackets (separate_map semi (doc_pat ctxt false) pats) + | P_cons (p,p') -> doc_op (string "::") (doc_pat ctxt true p) (doc_pat ctxt true p') + | P_record (_,_) -> empty (* TODO *) + +let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with + | Typ_tup ts -> List.exists typ_needs_printed ts + | Typ_app (Id_aux (Id "itself",_),_) -> true + | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs + | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2 + | Typ_exist (kids,_,t) -> + let visible_kids = KidSet.inter (KidSet.of_list kids) (lem_tyvars_of_typ t) in + typ_needs_printed t && KidSet.is_empty visible_kids + | _ -> false +and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with + | Typ_arg_typ t -> typ_needs_printed t + | _ -> false + +let contains_early_return exp = + let e_app (f, args) = + let rets, args = List.split args in + (List.fold_left (||) (string_of_id f = "early_return") rets, + E_app (f, args)) in + fst (fold_exp + { (Rewriter.compute_exp_alg false (||)) + with e_return = (fun (_, r) -> (true, E_return r)); e_app = e_app } exp) + +let find_e_ids exp = + let e_id id = IdSet.singleton id, E_id id in + fst (fold_exp + { (compute_exp_alg IdSet.empty IdSet.union) with e_id = e_id } exp) + +let typ_id_of (Typ_aux (typ, l)) = match typ with + | Typ_id id -> id + | Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) + when string_of_id register = "register" -> id + | Typ_app (id, _) -> id + | _ -> raise (Reporting_basic.err_unreachable l "failed to get type id") + +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 expY = top_exp ctxt true in + let expN = top_exp ctxt false in + let expV = top_exp ctxt in + let liftR doc = + if ctxt.early_ret && effectful (effect_of full_exp) + then separate space [string "liftR"; parens (doc)] + else doc in + match e with + | E_assign((LEXP_aux(le_act,tannot) as le), e) -> + (* can only be register writes *) + (match le_act (*, t, tag*) with + | LEXP_vector_range (le,e2,e3) -> + (match le with + | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) -> + if is_bit_typ (typ_of_annot fannot) then + raise (report l "indexing a register's (single bit) bitfield not supported") + else + let field_ref = + doc_id (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id id in + liftR ((prefix 2 1) + (string "write_reg_field_range") + (align (doc_lexp_deref_lem ctxt le ^/^ + field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e))) + | _ -> + let deref = doc_lexp_deref_lem ctxt le in + liftR ((prefix 2 1) + (string "write_reg_range") + (align (deref ^/^ expY e2 ^/^ expY e3) ^/^ expY e))) + | LEXP_vector (le,e2) -> + (match le with + | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) -> + if is_bit_typ (typ_of_annot fannot) then + raise (report l "indexing a register's (single bit) bitfield not supported") + else + let field_ref = + doc_id (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id id in + let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot fannot)) then "write_reg_field_bit" else "write_reg_field_pos" in + liftR ((prefix 2 1) + (string call) + (align (doc_lexp_deref_lem ctxt le ^/^ + field_ref ^/^ expY e2 ^/^ expY e))) + | LEXP_aux (_, lannot) -> + let deref = doc_lexp_deref_lem ctxt le in + let call = if is_bitvector_typ (Env.base_typ_of (env_of full_exp) (typ_of_annot lannot)) then "write_reg_bit" else "write_reg_pos" in + liftR ((prefix 2 1) (string call) + (deref ^/^ expY e2 ^/^ expY e)) + ) + | LEXP_field ((LEXP_aux (_, lannot) as le),id) -> + let field_ref = + doc_id (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id id (*^^ + dot ^^ + string "set_field"*) in + liftR ((prefix 2 1) + (string "write_reg_field") + (doc_lexp_deref_lem ctxt le ^^ space ^^ + field_ref ^/^ expY e)) + | LEXP_deref re -> + liftR ((prefix 2 1) (string "write_reg") (expY re ^/^ expY e)) + | _ -> + liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem ctxt le ^/^ expY e))) + | E_vector_append(le,re) -> + raise (Reporting_basic.err_unreachable l + "E_vector_append should have been rewritten before pretty-printing") + | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re) + | E_if(c,t,e) -> + let epp = if_exp ctxt false c t e in + if aexp_needed then parens (align epp) else epp + | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> + raise (report l "E_for should have been rewritten before pretty-printing") + | E_loop _ -> + raise (report l "E_loop should have been rewritten before pretty-printing") + | E_let(leb,e) -> + let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in + if aexp_needed then parens epp else epp + | E_app(f,args) -> + begin match f with + (* temporary hack to make the loop body a function of the temporary variables *) + | Id_aux (Id "None", _) as none -> doc_id_ctor none + | Id_aux (Id "foreach", _) -> + begin + match args with + | [exp1; exp2; exp3; ord_exp; vartuple; body] -> + let loopvar, body = match body with + | E_aux (E_let (LB_aux (LB_val ( + P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body + | E_aux (E_let (LB_aux (LB_val ( + P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body + | E_aux (E_let (LB_aux (LB_val ( + P_aux (P_id id, _), _), _), body), _) -> id, body + | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in + let step = match ord_exp with + | E_aux (E_lit (L_aux (L_false, _)), _) -> + parens (separate space [string "integerNegate"; expY exp3]) + | _ -> expY exp3 + in + let combinator = if effectful (effect_of body) then "foreachM" else "foreach" in + let indices_pp = parens (separate space [string "index_list"; expY exp1; expY exp2; step]) in + let used_vars_body = find_e_ids body in + let body_lambda = + (* Work around indentation issues in Lem when translating + tuple or literal unit patterns to Isabelle *) + match fst (uncast_exp vartuple) with + | E_aux (E_tuple _, _) + when not (IdSet.mem (mk_id "varstup") used_vars_body)-> + separate space [string "fun"; doc_id loopvar; string "varstup"; bigarrow] + ^^ break 1 ^^ + separate space [string "let"; expY vartuple; string ":= varstup in"] + | E_aux (E_lit (L_aux (L_unit, _)), _) + when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> + separate space [string "fun"; doc_id loopvar; string "unit_var"; bigarrow] + | _ -> + separate space [string "fun"; doc_id loopvar; expY vartuple; bigarrow] + in + parens ( + (prefix 2 1) + ((separate space) [string combinator; indices_pp; expY vartuple]) + (parens + (prefix 2 1 (group body_lambda) (expN body)) + ) + ) + | _ -> raise (Reporting_basic.err_unreachable l + "Unexpected number of arguments for loop combinator") + end + | Id_aux (Id (("while" | "until") as combinator), _) -> + begin + match args with + | [cond; varstuple; body] -> + let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in + let csuffix, cond, body = + match effectful (effect_of cond), effectful (effect_of body) with + | false, false -> "", cond, body + | false, true -> "M", return cond, body + | true, false -> "M", cond, return body + | true, true -> "M", cond, body + in + let used_vars_body = find_e_ids body in + let lambda = + (* Work around indentation issues in Lem when translating + tuple or literal unit patterns to Isabelle *) + match fst (uncast_exp varstuple) with + | E_aux (E_tuple _, _) + when not (IdSet.mem (mk_id "varstup") used_vars_body)-> + separate space [string "fun varstup"; bigarrow] ^^ break 1 ^^ + separate space [string "let"; expY varstuple; string ":= varstup in"] + | E_aux (E_lit (L_aux (L_unit, _)), _) + when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> + separate space [string "fun unit_var"; bigarrow] + | _ -> + separate space [string "fun"; expY varstuple; bigarrow] + in + parens ( + (prefix 2 1) + ((separate space) [string (combinator ^ csuffix); expY varstuple]) + ((prefix 0 1) + (parens (prefix 2 1 (group lambda) (expN cond))) + (parens (prefix 2 1 (group lambda) (expN body)))) + ) + | _ -> raise (Reporting_basic.err_unreachable l + "Unexpected number of arguments for loop combinator") + end + | Id_aux (Id "early_return", _) -> + begin + match args with + | [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 false (typ_of full_exp); + doc_atomic_typ false (typ_of exp)] in + true, doc_op colon epp tannot in + if aexp_needed then parens tepp else tepp + | _ -> raise (Reporting_basic.err_unreachable l + "Unexpected number of arguments for early_return builtin") + end + | _ -> + begin match annot with + | Some (env, _, _) when Env.is_union_constructor f env -> + let epp = + match args with + | [] -> doc_id_ctor f + | [arg] -> doc_id_ctor f ^^ space ^^ expV true arg + | _ -> + doc_id_ctor f ^^ space ^^ + parens (separate_map comma (expV false) args) in + if aexp_needed then parens (align epp) else epp + | _ -> + let call, is_extern = match annot with + | Some (env, _, _) when Env.is_extern f env "coq" -> + string (Env.get_extern f env "coq"), true + | _ -> doc_id f, false in + let epp = hang 2 (flow (break 1) (call :: List.map expY args)) in + let (taepp,aexp_needed) = + 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) + else (epp, aexp_needed) in + liftR (if aexp_needed then parens (align taepp) else taepp) + end + end + | E_vector_access (v,e) -> + raise (Reporting_basic.err_unreachable l + "E_vector_access should have been rewritten before pretty-printing") + | E_vector_subrange (v,e1,e2) -> + raise (Reporting_basic.err_unreachable l + "E_vector_subrange should have been rewritten before pretty-printing") + | E_field((E_aux(_,(l,fannot)) as fexp),id) -> + (match fannot with + | Some(env, (Typ_aux (Typ_id tid, _)), _) + | Some(env, (Typ_aux (Typ_app (tid, _), _)), _) + when Env.is_record tid env -> + let fname = + if prefix_recordtype && string_of_id tid <> "regstate" + then (string (string_of_id tid ^ "_")) ^^ doc_id id + else doc_id id in + expY fexp ^^ dot ^^ fname + | _ -> + raise (report l "E_field expression with no register or record type")) + | E_block [] -> string "tt" + | E_block exps -> raise (report l "Blocks should have been removed till now.") + | E_nondet exps -> raise (report l "Nondet blocks not supported.") + | E_id id | E_ref id -> + let env = env_of full_exp in + let typ = typ_of full_exp in + let eff = effect_of full_exp in + let base_typ = Env.base_typ_of env typ in + if has_effect eff BE_rreg then + let epp = separate space [string "read_reg";doc_id (append_id id "_ref")] in + if is_bitvector_typ base_typ + then liftR (parens (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env true base_typ))))) + else liftR epp + else if Env.is_register id env then doc_id (append_id id "_ref") + else if is_ctor env id then doc_id_ctor id + else doc_id id + | E_lit lit -> doc_lit lit + | E_cast(typ,e) -> + expV aexp_needed e + | E_tuple exps -> + parens (align (group (separate_map (comma ^^ break 1) expN exps))) + | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> + let recordtyp = match annot with + | Some (env, Typ_aux (Typ_id tid,_), _) + | Some (env, Typ_aux (Typ_app (tid, _), _), _) -> + (* when Env.is_record tid env -> *) + tid + | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in + let epp = enclose_record (align (separate_map + (semi_sp ^^ break 1) + (doc_fexp ctxt recordtyp) fexps)) in + if aexp_needed then parens epp else epp + | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> + let recordtyp = match annot with + | Some (env, Typ_aux (Typ_id tid,_), _) + | Some (env, Typ_aux (Typ_app (tid, _), _), _) + when Env.is_record tid env -> + tid + | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in + anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) + | E_vector exps -> + let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in + let start, (len, order, etyp) = + if is_vector_typ t then vector_start_index t, vector_typ_args_of t + else raise (Reporting_basic.err_unreachable l + "E_vector of non-vector type") in + let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in + let expspp = + match exps with + | [] -> empty + | e :: es -> + let (expspp,_) = + List.fold_left + (fun (pp,count) e -> + (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^ + expN e), + if count = 20 then 0 else count + 1) + (expN e,0) es in + align (group expspp) in + let epp = brackets expspp in + let (epp,aexp_needed) = + if is_bit_typ etyp then + let bepp = string "vec_of_bits" ^^ space ^^ align epp in + (align (group (prefix 0 1 bepp (doc_tannot_lem ctxt (env_of full_exp) false t))), true) + else (epp,aexp_needed) in + if aexp_needed then parens (align epp) else epp + | E_vector_update(v,e1,e2) -> + raise (Reporting_basic.err_unreachable l + "E_vector_update should have been rewritten before pretty-printing") + | E_vector_update_subrange(v,e1,e2,e3) -> + raise (Reporting_basic.err_unreachable l + "E_vector_update should have been rewritten before pretty-printing") + | E_list exps -> + brackets (separate_map semi (expN) exps) + | E_case(e,pexps) -> + let only_integers e = expY e in + let epp = + group ((separate space [string "match"; only_integers e; string "with"]) ^/^ + (separate_map (break 1) (doc_case ctxt) pexps) ^/^ + (string "end")) in + if aexp_needed then parens (align epp) else align epp + | E_try (e, pexps) -> + if effectful (effect_of e) then + let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in + let epp = + group ((separate space [string try_catch; expY e; string "(function "]) ^/^ + (separate_map (break 1) (doc_case ctxt) pexps) ^/^ + (string "end)")) in + if aexp_needed then parens (align epp) else align epp + else + raise (Reporting_basic.err_todo l "Warning: try-block around pure expression") + | E_throw e -> + let epp = liftR (separate space [string "throw"; expY e]) in + if aexp_needed then parens (align epp) else align epp + | E_exit e -> liftR (separate space [string "exit"; expY e]) + | E_assert (e1,e2) -> + let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in + if aexp_needed then parens (align epp) else align epp + | E_app_infix (e1,id,e2) -> + raise (Reporting_basic.err_unreachable l + "E_app_infix should have been rewritten before pretty-printing") + | E_var(lexp, eq_exp, in_exp) -> + raise (report l "E_vars should have been removed before pretty-printing") + | E_internal_plet (pat,e1,e2) -> + let epp = + let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in + let middle = + match fst (untyp_pat pat) with + | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> + string ">>" + | P_aux (P_tup _, _) + when not (IdSet.mem (mk_id "varstup") (find_e_ids e2)) -> + (* Work around indentation issues in Lem when translating + tuple patterns to Isabelle *) + separate space + [string ">>= fun varstup => let"; + doc_pat ctxt true pat; + string "= varstup in"] + | _ -> + separate space [string ">>= fun"; doc_pat ctxt true pat; bigarrow] + in + infix 0 1 middle (expV b e1) (expN e2) + in + if aexp_needed then parens (align epp) else epp + | E_internal_return (e1) -> + separate space [string "returnm"; expY e1] + | E_sizeof nexp -> + (match nexp_simp nexp with + | Nexp_aux (Nexp_constant i, _) -> doc_lit (L_aux (L_num i, l)) + | _ -> + raise (Reporting_basic.err_unreachable l + "pretty-printing non-constant sizeof expressions to Lem not supported")) + | E_return r -> + let ret_monad = " : MR" in + 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 ret_monad; + parens (doc_typ (typ_of full_exp)); + parens (doc_typ (typ_of r))] in + align (parens (string "early_return" ^//^ expV true r ^//^ ta)) + | E_constraint _ -> string "true" + | E_comment _ | E_comment_struc _ -> empty + | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ + | E_internal_exp_user _ | E_internal_value _ -> + raise (Reporting_basic.err_unreachable l + "unsupported internal expression encountered while pretty-printing") + and if_exp ctxt (elseif : bool) c t e = + let if_pp = string (if elseif then "else if" else "if") in + let else_pp = match e with + | E_aux (E_if (c', t', e'), _) + | E_aux (E_cast (_, E_aux (E_if (c', t', e'), _)), _) -> + if_exp ctxt true c' t' e' + | _ -> prefix 2 1 (string "else") (top_exp ctxt false e) + in + (prefix 2 1 + (soft_surround 2 1 if_pp (top_exp ctxt true c) (string "then")) + (top_exp ctxt false t)) ^^ + break 1 ^^ + else_pp + and let_exp ctxt (LB_aux(lb,_)) = match lb with + | LB_val(pat,e) -> + prefix 2 1 + (separate space [string "let"; squote ^^ doc_pat ctxt true pat; coloneq]) + (top_exp ctxt false e) + + and doc_fexp ctxt recordtyp (FE_aux(FE_Fexp(id,e),_)) = + let fname = + if prefix_recordtype && string_of_id recordtyp <> "regstate" + then (string (string_of_id recordtyp ^ "_")) ^^ doc_id id + else doc_id id in + group (doc_op coloneq fname (top_exp ctxt true e)) + + and doc_case ctxt = function + | Pat_aux(Pat_exp(pat,e),_) -> + group (prefix 3 1 (separate space [pipe; doc_pat ctxt false pat;bigarrow]) + (group (top_exp ctxt false e))) + | Pat_aux(Pat_when(_,_,_),(l,_)) -> + raise (Reporting_basic.err_unreachable l + "guarded pattern expression should have been rewritten before pretty-printing") + + and doc_lexp_deref_lem ctxt ((LEXP_aux(lexp,(l,annot)))) = match lexp with + | LEXP_field (le,id) -> + parens (separate empty [doc_lexp_deref_lem ctxt le;dot;doc_id id]) + | LEXP_id id -> doc_id (append_id id "_ref") + | LEXP_cast (typ,id) -> doc_id (append_id id "_ref") + | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem ctxt) lexps) + | _ -> + raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Unsupported lexp")) + (* expose doc_exp_lem and doc_let *) + in top_exp, let_exp + +let doc_type_union typ_name (Tu_aux(Tu_ty_id(typ,id),_)) = + separate space [doc_id_ctor id; colon; + doc_typ typ; arrow; typ_name] + +let rec doc_range_lem (BF_aux(r,_)) = match r with + | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i)) + | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2)) + | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) + +let doc_typdef (TD_aux(td, (l, annot))) = match td with + | TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) -> + doc_op coloneq + (separate space [string "Definition"; doc_id_type id; doc_typquant_items parens typq]) + (doc_typschm false typschm) ^^ dot + | TD_record(id,nm,typq,fs,_) -> + let fname fid = if prefix_recordtype && string_of_id id <> "regstate" + then concat [doc_id id;string "_";doc_id_type fid;] + else doc_id_type fid in + let f_pp (typ,fid) = + concat [fname fid;space;colon;space;doc_typ typ; semi] in + let rectyp = match typq with + | TypQ_aux (TypQ_tq qs, _) -> + let quant_item = function + | QI_aux (QI_id (KOpt_aux (KOpt_none kid, _)), l) + | QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) -> + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid, l)), l)] + | _ -> [] in + let targs = List.concat (List.map quant_item qs) in + mk_typ (Typ_app (id, targs)) + | TypQ_aux (TypQ_no_forall, _) -> mk_id_typ id in + let fs_doc = group (separate_map (break 1) f_pp fs) in + let doc_update_field (_,fid) = + let idpp = fname fid in + let otherfield (_,fid') = + if Id.compare fid fid' == 0 then empty else + let idpp = fname fid' in + separate space [semi; idpp; string ":="; idpp; string "r"] + in + string "Notation \"{[ r 'with' '" ^^ idpp ^^ string "' := e ]}\" := ({| " ^^ + idpp ^^ string " := e" ^^ concat (List.map otherfield fs) ^^ + space ^^ string "|})." + in + let updates_pp = separate hardline (List.map doc_update_field fs) in + (* let doc_field (ftyp, fid) = + let reftyp = + mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), + [mk_typ_arg (Typ_arg_typ rectyp); + mk_typ_arg (Typ_arg_typ ftyp)])) in + let rfannot = doc_tannot_lem empty_ctxt env false reftyp in + let get, set = + string "rec_val" ^^ dot ^^ fname fid, + anglebars (space ^^ string "rec_val with " ^^ + (doc_op equals (fname fid) (string "v")) ^^ space) in + let base_ftyp = match annot with + | Some (env, _, _) -> Env.base_typ_of env ftyp + | _ -> ftyp in + let (start, is_inc) = + try + let start, (_, ord, _) = vector_start_index base_ftyp, vector_typ_args_of base_ftyp in + match nexp_simp start with + | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord) + | _ -> + raise (Reporting_basic.err_unreachable Parse_ast.Unknown + ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start)) + with + | _ -> (Big_int.zero, true) in + doc_op equals + (concat [string "let "; parens (concat [doc_id id; underscore; doc_id fid; rfannot])]) + (anglebars (concat [space; + doc_op equals (string "field_name") (string_lit (doc_id fid)); semi_sp; + doc_op equals (string "field_start") (string (Big_int.to_string start)); semi_sp; + doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp; + doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; + doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in *) + doc_op coloneq + (separate space [string "Record"; doc_id_type id; doc_typquant_items parens typq]) + ((*doc_typquant_lem typq*) (braces (space ^^ align fs_doc ^^ space))) ^^ + dot ^^ hardline ^^ updates_pp + | TD_variant(id,nm,typq,ar,_) -> + (match id with + | Id_aux ((Id "read_kind"),_) -> empty + | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "barrier_kind"),_) -> empty + | Id_aux ((Id "trans_kind"),_) -> empty + | Id_aux ((Id "instruction_kind"),_) -> empty + (* | Id_aux ((Id "regfp"),_) -> empty + | Id_aux ((Id "niafp"),_) -> empty + | Id_aux ((Id "diafp"),_) -> empty *) + | Id_aux ((Id "option"),_) -> empty + | _ -> + let typ_nm = separate space [doc_id_type id; doc_typquant_items parens typq] in + let ar_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_type_union typ_nm) ar) in + let typ_pp = + (doc_op coloneq) + (concat [string "Inductive"; space; typ_nm]) + ((*doc_typquant_lem typq*) ar_doc) in + typ_pp ^^ dot ^^ hardline ^^ hardline) + | TD_enum(id,nm,enums,_) -> + (match id with + | Id_aux ((Id "read_kind"),_) -> empty + | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "barrier_kind"),_) -> empty + | Id_aux ((Id "trans_kind"),_) -> empty + | Id_aux ((Id "instruction_kind"),_) -> empty + | Id_aux ((Id "regfp"),_) -> empty + | Id_aux ((Id "niafp"),_) -> empty + | Id_aux ((Id "diafp"),_) -> empty + | _ -> + let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_ctor enums) in + let typ_pp = (doc_op coloneq) + (concat [string "Inductive"; space; doc_id_type id;]) + (enums_doc) in + typ_pp ^^ dot ^^ hardline ^^ hardline) + | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices") + +let args_of_typ l env typs = + let arg i typ = + let id = mk_id ("arg" ^ string_of_int i) in + (P_aux (P_id id, (l, Some (env, typ, no_effect))), typ), + E_aux (E_id id, (l, Some (env, typ, no_effect))) in + List.split (List.mapi arg typs) + +let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) = + let env = env_of_annot annot in + let tup_typs = match typ with + | Typ_aux (Typ_tup typs, _) -> Some typs + | _ -> match Env.expand_synonyms env typ with + | Typ_aux (Typ_tup typs, _) -> Some typs + | _ -> None + in + let identity = (fun body -> body) in + match paux, tup_typs with + | P_tup [], _ -> + let annot = (l, Some (Env.empty, unit_typ, no_effect)) in + [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity + | P_tup pats, Some typs -> List.combine pats typs, identity + | P_tup pats, _ -> failwith "Tuple pattern against non-tuple type" + | P_wild, Some typs -> + let wild typ = P_aux (P_wild, (l, Some (env, typ, no_effect))), typ in + List.map wild typs, identity + | P_typ (_, pat), _ -> untuple_args_pat typ pat + | P_as _, Some typs | P_id _, Some typs -> + let argpats, argexps = args_of_typ l env typs in + let argexp = E_aux (E_tuple argexps, annot) in + let bindargs (E_aux (_, bannot) as body) = + E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in + argpats, bindargs + | _, _ -> + [pat,typ], identity + +let doc_rec (Rec_aux(r,_)) = match r with + | Rec_nonrec -> string "Definition" + | Rec_rec -> string "Fixpoint" + +let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with + | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ typ) + +let doc_fun_body ctxt exp = + let doc_exp = doc_exp_lem ctxt false exp in + if ctxt.early_ret + then align (string "catch_early_return" ^//^ parens (doc_exp)) + else doc_exp + +(* Coq doesn't support "as" patterns well in Definition binders, so we push + them over to the r.h.s. of the := *) +let demote_as_pattern i (P_aux (_,p_annot) as pat,typ) = + let open Rewriter in + if fst (fold_pat ({ (compute_pat_alg false (||)) with p_as = (fun ((_,p),id) -> true, P_as (p,id)) }) pat) + then + let id = mk_id ("arg" ^ string_of_int i) in (* TODO: name conflicts *) + (P_aux (P_id id, p_annot),typ), + fun (E_aux (_,e_ann) as e) -> + E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann) + else (pat,typ), fun e -> e + +let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = + let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in + let (arg_typ, ret_typ, eff) = match typ with + | Typ_aux (Typ_fn (arg_typ, ret_typ, eff),_) -> arg_typ, ret_typ, eff + | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type") + in + 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 + let quantspp = doc_typquant_items braces tq in + let pats, bind = untuple_args_pat arg_typ pat in + let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in + let exp = List.fold_left (fun body f -> f body) (bind exp) binds in + let patspp = separate_map space (fun (pat,typ) -> + squote ^^ parens (separate space [doc_pat ctxt true pat; colon; doc_typ typ])) pats in + let retpp = + if effectful eff + then string "M" ^^ space ^^ parens (doc_typ ret_typ) + else doc_typ ret_typ + in + let _ = match guard with + | None -> () + | _ -> + raise (Reporting_basic.err_unreachable l + "guarded pattern expression should have been rewritten before pretty-printing") in + group (prefix 3 1 + (separate space [doc_id id; quantspp; patspp; colon; retpp; coloneq]) + (doc_fun_body ctxt exp ^^ dot)) + +let get_id = function + | [] -> failwith "FD_function with empty list" + | (FCL_aux (FCL_Funcl (id,_),_))::_ -> id + +module StringSet = Set.Make(String) + +(* Strictly speaking, Lem doesn't support multiple clauses for a single function + joined by "and", although it has worked for Isabelle before. However, all + the funcls should have been merged by the merge_funcls rewrite now. *) +let doc_fundef_rhs_lem (FD_aux(FD_function(r, typa, efa, funcls),fannot)) = + separate_map (hardline ^^ string "and ") doc_funcl funcls + +let doc_mutrec_lem = function + | [] -> failwith "DEF_internal_mutrec with empty function list" + | fundefs -> + string "let rec " ^^ + separate_map (hardline ^^ string "and ") doc_fundef_rhs_lem fundefs + +let rec doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),fannot)) = + match fcls with + | [] -> failwith "FD_function with empty function list" + | [FCL_aux (FCL_Funcl(id,_),annot) as funcl] + when not (Env.is_extern id (env_of_annot annot) "coq") -> + (doc_rec r) ^^ space ^^ (doc_funcl funcl) + | [_] -> empty (* extern *) + | _ -> failwith "FD_function with more than one clause" + + + +let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = + match reg with + | DEC_reg(typ,id) -> empty + (* + let env = env_of_annot annot in + let rt = Env.base_typ_of env typ in + if is_vector_typ rt then + let start, (size, order, etyp) = vector_start_index rt, vector_typ_args_of rt in + if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then + let o = if is_order_inc order then "true" else "false" in + (doc_op equals) + (string "let" ^^ space ^^ doc_id id) + (string "Register" ^^ space ^^ + align (separate space [string_lit(doc_id id); + doc_nexp (size); + doc_nexp (start); + string o; + string "[]"])) + ^/^ hardline + else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) + else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) *) + | DEC_alias(id,alspec) -> empty + | DEC_typ_alias(typ,id,alspec) -> empty + +let is_field_accessor regtypes fdef = + let is_field_of regtyp field = + List.exists (fun (tname, (_, _, fields)) -> tname = regtyp && + List.exists (fun (_, fid) -> string_of_id fid = field) fields) regtypes in + match Util.split_on_char '_' (string_of_id (id_of_fundef fdef)) with + | [access; regtyp; field] -> + (access = "get" || access = "set") && is_field_of regtyp field + | _ -> false + +let doc_regtype_fields (tname, (n1, n2, fields)) = + let i1, i2 = match n1, n2 with + | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> i1, i2 + | _ -> raise (Reporting_basic.err_typ Parse_ast.Unknown + ("Non-constant indices in register type " ^ tname)) in + let dir_b = i1 < i2 in + let dir = (if dir_b then "true" else "false") in + let doc_field (fr, fid) = + let i, j = match fr with + | BF_aux (BF_single i, _) -> (i, i) + | BF_aux (BF_range (i, j), _) -> (i, j) + | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown + ("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in + let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in + (* TODO Assumes normalised, decreasing bitvector slices; however, since + start indices or indexing order do not appear in Lem type annotations, + this does not matter. *) + let ftyp = vector_typ (nconstant fsize) dec_ord bit_typ in + let reftyp = + mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), + [mk_typ_arg (Typ_arg_typ (mk_id_typ (mk_id tname))); + mk_typ_arg (Typ_arg_typ ftyp)])) in + let rfannot = doc_tannot_lem empty_ctxt Env.empty false reftyp in + doc_op equals + (concat [string "let "; parens (concat [string tname; underscore; doc_id fid; rfannot])]) + (concat [ + space; langlebar; string " field_name = \"" ^^ doc_id fid ^^ string "\";"; hardline; + space; space; space; string (" field_start = " ^ Big_int.to_string i ^ ";"); hardline; + space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline; + space; space; space; string (" get_field = get_" ^ tname ^ "_" ^ string_of_id fid ^ ";"); hardline; + space; space; space; string (" set_field = set_" ^ tname ^ "_" ^ string_of_id fid ^ " "); ranglebar]) + in + separate_map hardline doc_field fields + +let rec doc_def def = + (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) + match def with + | DEF_spec v_spec -> empty (* Types appear in definitions *) + | DEF_fixity _ -> empty + | DEF_overload _ -> empty + | DEF_type t_def -> group (doc_typdef t_def) ^/^ hardline + | DEF_reg_dec dec -> group (doc_dec_lem dec) + + | DEF_default df -> empty + | DEF_fundef fdef -> group (doc_fundef fdef) ^/^ hardline + | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline + | DEF_val (LB_aux (LB_val (pat, exp), _)) -> + let (id,typpp) = match pat with + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, space ^^ colon ^^ space ^^ doc_typ typ + | P_aux (P_id id, _) -> id, empty + | _ -> failwith "Top-level value definition with complex pattern not supported for Coq yet" + in + group (string "Definition" ^^ space ^^ doc_id id ^^ typpp ^^ space ^^ coloneq ^^ + doc_exp_lem empty_ctxt false exp ^^ dot) ^/^ hardline + | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" + + | DEF_kind _ -> empty + + | DEF_comm (DC_comm s) -> comment (string s) + | DEF_comm (DC_comm_struct d) -> comment (doc_def d) + + +let find_exc_typ defs = + let is_exc_typ_def = function + | DEF_type td -> string_of_id (id_of_type_def td) = "exception" + | _ -> false in + if List.exists is_exc_typ_def defs then "exception" else "unit" + +let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line = + (* let regtypes = find_regtypes d in *) + let state_ids = + State.generate_regstate_defs true defs + |> Initial_check.val_spec_ids + in + let is_state_def = function + | DEF_spec vs -> IdSet.mem (id_of_val_spec vs) state_ids + | DEF_fundef fd -> IdSet.mem (id_of_fundef fd) state_ids + | _ -> false + in + let is_typ_def = function + | DEF_type _ -> true + | _ -> false + in + let exc_typ = find_exc_typ defs in + let typdefs, defs = List.partition is_typ_def defs in + let statedefs, defs = List.partition is_state_def defs in + let register_refs = State.register_refs_coq (State.find_registers defs) in + (print types_file) + (concat + [string "(*" ^^ (string top_line) ^^ string "*)";hardline; + (separate_map hardline) + (fun lib -> separate space [string "Require Import";string lib] ^^ dot) types_modules;hardline; +string "Require Import String."; hardline; + separate empty (List.map doc_def typdefs); hardline; + hardline; + separate empty (List.map doc_def statedefs); hardline; + hardline; + register_refs; hardline; + concat [ + string ("Definition MR a r := monadR register_value a r " ^ exc_typ ^ "."); hardline; + string ("Definition M a := monad register_value a " ^ exc_typ ^ "."); hardline + ] + ]); + (print defs_file) + (concat + [string "(*" ^^ (string top_line) ^^ string "*)";hardline; + (separate_map hardline) + (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline; +string "Require Import List. Import ListNotations."; + hardline; + separate empty (List.map doc_def defs); + hardline]); diff --git a/src/process_file.ml b/src/process_file.ml index a576c16e..4856c20a 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -57,6 +57,7 @@ let opt_lem_mwords = ref false type out_type = | Lem_ast_out | Lem_out of string list + | Coq_out of string list let get_lexbuf f = let in_chan = open_in f in @@ -291,6 +292,28 @@ let output_lem filename libs defs = print ol isa_lemmas; close_output_with_check ext_ol +let output_coq filename libs defs = + let generated_line = generated_line filename in + let types_module = (filename ^ "_types") in + let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in + let operators_module = "Sail_operators_mwords" in + let base_imports = [ + "Sail_instr_kinds"; + "Sail_values"; + 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 + (Pretty_print_coq.pp_defs_coq + (ot, base_imports) + (o, base_imports @ (types_module :: libs)) + defs generated_line); + close_output_with_check ext_ot; + close_output_with_check ext_o + let rec iterate (f : int -> unit) (n : int) : unit = if n = 0 then () else (f n; iterate f (n - 1)) @@ -312,6 +335,8 @@ let output1 libpath out_arg filename defs = end | Lem_out libs -> output_lem f' libs defs + | Coq_out libs -> + output_coq f' libs defs let output libpath out_arg files = List.iter @@ -342,6 +367,7 @@ let rewrite rewriters defs = let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)] let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem +let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml let rewrite_ast_c = rewrite Rewrites.rewrite_defs_c let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter diff --git a/src/process_file.mli b/src/process_file.mli index 2f418ff9..b38b4259 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -56,6 +56,7 @@ val monomorphise_ast : ((string * int) * string) list -> Type_check.Env.t -> Typ val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val rewrite_ast_coq : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_c : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs @@ -81,6 +82,7 @@ val opt_dall_split_errors : bool ref type out_type = | Lem_ast_out | 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*) val output : string -> (* The path to the library *) diff --git a/src/sail.ml b/src/sail.ml index 85719f4d..4d32fb94 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -62,9 +62,11 @@ let opt_print_lem = ref false let opt_print_ocaml = ref false let opt_print_c = ref false let opt_print_latex = ref false +let opt_print_coq = ref false let opt_memo_z3 = ref false let opt_sanity = ref false let opt_libs_lem = ref ([]:string list) +let opt_libs_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) let opt_mono_split = ref ([]:((string * int) * string) list) let opt_process_elf : string option ref = ref None @@ -120,6 +122,12 @@ let options = Arg.align ([ ( "-lem_mwords", Arg.Set Pretty_print_lem.opt_mwords, " use native machine word library for Lem output"); + ( "-coq", + Arg.Set opt_print_coq, + " output a Coq translated version of the input"); + ( "-coq_lib", + Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), + " provide additional library to open in Coq output"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix), " set a custom prefix for generated latex command (default sail)"); @@ -310,6 +318,12 @@ let main() = let ast_lem = rewrite_ast_lem ast_lem in output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem] else ()); + (if !(opt_print_coq) + then + let type_envs, ast_coq = State.add_regstate_defs true type_envs ast in + let ast_coq = rewrite_ast_coq ast_coq in + output "" (Coq_out (!opt_libs_coq)) [out_name,ast_coq] + else ()); (if !(opt_print_latex) then begin diff --git a/src/state.ml b/src/state.ml index 59fb9995..49fa5a99 100644 --- a/src/state.ml +++ b/src/state.ml @@ -306,6 +306,85 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = hardline ^^ hardline ^^ separate_map (hardline ^^ hardline) register_lemmas registers +let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with + | Typ_app _ when is_vector_typ typ && not (is_bitvector_typ typ) -> + let size, ord, etyp = vector_typ_args_of typ in + let size = string_of_nexp (nexp_simp size) in + let is_inc = if is_order_inc ord then "true" else "false" in + let etyp_of, of_etyp = regval_convs_coq etyp in + "(fun v => vector_of_regval " ^ etyp_of ^ " v)", + "(fun v => regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)" + | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) + when string_of_id id = "list" -> + let etyp_of, of_etyp = regval_convs_coq etyp in + "(fun v => list_of_regval " ^ etyp_of ^ " v)", + "(fun v => regval_of_list " ^ of_etyp ^ " v)" + | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) + when string_of_id id = "option" -> + let etyp_of, of_etyp = regval_convs_coq etyp in + "(fun v => option_of_regval " ^ etyp_of ^ " v)", + "(fun v => regval_of_option " ^ of_etyp ^ " v)" + | _ -> + let id = string_of_id (regval_constr_id true typ) in + "(fun v => " ^ id ^ "_of_regval v)", "(fun v => regval_of_" ^ id ^ " v)" + +let register_refs_coq registers = + let generic_convs = + separate_map hardline string [ + "Definition vector_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with"; + " | Regval_vector (_, _, v) => just_list (List.map of_regval v)"; + " | _ => None"; + "end."; + ""; + "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : list a) : register_value := Regval_vector (size, is_inc, List.map regval_of xs)."; + ""; + "Definition list_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with"; + " | Regval_list v => just_list (List.map of_regval v)"; + " | _ => None"; + "end."; + ""; + "Definition regval_of_list {a} (regval_of : a -> register_value) (xs : list a) : register_value := Regval_list (List.map regval_of xs)."; + ""; + "Definition option_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (option a) := match rv with"; + " | Regval_option v => option_map of_regval v"; + " | _ => None"; + "end."; + ""; + "Definition regval_of_option {a} (regval_of : a -> register_value) (v : option a) := Regval_option (option_map regval_of v)."; + ""; + "" + ] + in + let register_ref (typ, id) = + let idd = string (string_of_id id) in + (* let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in *) + let of_regval, regval_of = regval_convs_coq typ in + concat [string "Definition "; idd; string "_ref := {|"; hardline; + string " name := \""; idd; string "\";"; hardline; + string " read_from := (fun s => s.("; idd; string "));"; hardline; + string " write_to := (fun v s => ({[ s with "; idd; string " := v ]}));"; hardline; + string " of_regval := "; string of_regval; string ";"; hardline; + string " regval_of := "; string regval_of; string " |}."; hardline] + in + let refs = separate_map hardline register_ref registers in + let get_set_reg (_, id) = + let idd = string_of_id id in + string (" if string_dec reg_name \"" ^ idd ^ "\" then Some (" ^ idd ^ "_ref.(regval_of) (" ^ idd ^ "_ref.(read_from) s)) else"), + string (" if string_dec reg_name \"" ^ idd ^ "\" then option_map (fun v => " ^ idd ^ "_ref.(write_to) v s) (" ^ idd ^ "_ref.(of_regval) v) else") + in + let getters_setters = + let getters, setters = List.split (List.map get_set_reg registers) in + string "Local Open Scope string." ^^ hardline ^^ + string "Definition get_regval (reg_name : string) (s : regstate) : option register_value :=" ^^ hardline ^^ + separate hardline getters ^^ hardline ^^ + string " None." ^^ hardline ^^ hardline ^^ + string "Definition set_regval (reg_name : string) (v : register_value) (s : regstate) : option regstate :=" ^^ hardline ^^ + separate hardline setters ^^ hardline ^^ + string " None." ^^ hardline ^^ hardline ^^ + string "Definition register_accessors := (get_regval, set_regval)." ^^ hardline ^^ hardline + in + separate hardline [generic_convs; refs; getters_setters] + let generate_regstate_defs mwords defs = (* FIXME We currently don't want to generate undefined_type functions for register state and values. For the Lem backend, this would require diff --git a/src/type_check.ml b/src/type_check.ml index 5c72983a..6f5332cf 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -302,6 +302,7 @@ module Env : sig val update_val_spec : id -> typquant * typ -> t -> t val define_val_spec : id -> t -> t val get_val_spec : id -> t -> typquant * typ + val get_val_spec_orig : id -> t -> typquant * typ val is_union_constructor : id -> t -> bool val add_record : id -> typquant -> (typ * id) list -> t -> t val is_record : id -> t -> bool @@ -717,6 +718,12 @@ end = struct let freshen_bind env bind = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) + let get_val_spec_orig id env = + try + Bindings.find id env.top_val_specs + with + | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) + let get_val_spec id env = try let bind = Bindings.find id env.top_val_specs in diff --git a/src/type_check.mli b/src/type_check.mli index a047db9c..bb52f2aa 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -88,9 +88,14 @@ module Env : sig (** Note: Most get_ functions assume the identifiers exist, and throw type errors if it doesn't. *) - (** get the quantifier and type for a function identifier. *) + (** Get the quantifier and type for a function identifier, freshening + type variables. *) val get_val_spec : id -> t -> typquant * typ + (** Like get_val_spec, except that the original type variables are used. + Useful when processing the body of the function. *) + val get_val_spec_orig : id -> t -> typquant * typ + val update_val_spec : id -> typquant * typ -> t -> t val get_register : id -> t -> typ -- cgit v1.2.3 From bff23103407288070287106cb92b19116ee637c5 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 26 Apr 2018 17:31:58 +0100 Subject: Fix interpreter messages for failing asserts --- src/interpreter.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/interpreter.ml b/src/interpreter.ml index 2b24d66c..87439e83 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -257,7 +257,10 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_loop (Until, exp, body) -> wrap (E_block [body; E_aux (E_if (exp, orig_exp, exp_of_value V_unit), annot)]) | E_assert (exp, msg) when is_true exp -> wrap unit_exp - | E_assert (exp, msg) when is_false exp -> assertion_failed "FIXME" + | E_assert (exp, msg) when is_false exp && is_value msg -> + failwith (coerce_string (value_of_exp msg)) + | E_assert (exp, msg) when is_false exp -> + step msg >>= fun msg' -> wrap (E_assert (exp, msg')) | E_assert (exp, msg) -> step exp >>= fun exp' -> wrap (E_assert (exp', msg)) -- cgit v1.2.3 From 0e79825b9208a947a19b66b1221cdc890d425ec1 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 30 Apr 2018 17:38:33 +0100 Subject: Add typing rule for checking tuples as well as inferring them Removes some patches in ASL parser Allow immutable variables to shadow mutable ones. This is useful for translating ASL. --- src/type_check.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index 6f5332cf..de4c22c3 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2262,6 +2262,9 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | None -> typ_error l "Cannot use return outside a function" in annot_exp (E_return checked_exp) typ + | E_tuple exps, Typ_tup typs when List.length exps = List.length typs -> + let checked_exps = List.map2 (fun exp typ -> crule check_exp env exp typ) exps typs in + annot_exp (E_tuple checked_exps) typ | E_app (f, xs), _ -> let inferred_exp = infer_funapp l env f xs (Some typ) in type_coercion env inferred_exp typ @@ -2455,9 +2458,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) (Reporting_basic.loc_to_string l)) else (); match Env.lookup_id v env with - | Local (Immutable, _) | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, [] - | Local (Mutable, _) | Register _ -> - typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat) + | Local _ | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, [] + | Register _ -> + typ_error l ("Cannot shadow register in pattern " ^ string_of_pat pat) | Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env, [] end | P_var (pat, typ_pat) -> -- cgit v1.2.3 From 3f93ecbc6dbdc315b79de4ee69bf6bc6a6420d57 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 3 May 2018 15:30:55 +0100 Subject: Flow typing and l-expression changes for ASL parser 1. Experiment with allowing some flow typing on mutable variables for translating ASL in a more idiomatic way. I realise after updating some of the test cases that this could have some problematic side effects for lem translation, where mutable variables are translated into monadic code. We'd need to ensure that whatever flow typing happens for mutable variables also works for monadic code, including within transformed loops. If this doesn't work out some of these changes may need to be reverted. 2. Make the type inference for l-expressions a bit smarter. Splits the type checking rules for l-expressions into a inference part and a checking part like the other bi-directional rules. Should not be able to type check slightly more l-expresions, such as nested vector slices that may not have checked previously. The l-expression rules for vector patterns should be simpler now, but they are also more strict about bounds checking. Previously the bounds checks were derived from the corresponding operations that would appear on the RHS (i.e. LEXP_vector would get it's check from vector_access). This meant that the l-expression bounds checks could be weakend by weakening the checks on those operations. Now this is no longer possible, there is a -no_lexp_bounds_check option which turns of bounds checking in l-expressions. Currently this is on for the generated ARM spec, but this should only be temporary. 3. Add a LEXP_vector_concat which mirrors P_vector_concat except in l-expressions. Previously there was a hack that overloaded LEXP_tup for this to translate some ASL patterns, but that was fairly ugly. Adapt the rewriter and other parts of the code to handle this. The rewriter for lexp tuple vector assignments is now a rewriter for vector concat assignments. 4. Include a newly generated version of aarch64_no_vector 5. Update the Ocaml test suite to use builtins in lib/ --- src/ast_util.ml | 11 +- src/initial_check.ml | 60 ++++++----- src/interpreter.ml | 4 + src/parse_ast.ml | 1 + src/pretty_print_sail.ml | 1 + src/rewriter.ml | 11 +- src/rewriter.mli | 3 +- src/rewrites.ml | 32 +++--- src/sail.ml | 3 + src/type_check.ml | 267 ++++++++++++++++++++++++----------------------- src/type_check.mli | 9 +- src/value.ml | 5 + 12 files changed, 228 insertions(+), 179 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 2f2d27d8..f7574b9d 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -449,6 +449,7 @@ and map_lexp_annot_aux f = function | LEXP_memory (id, exps) -> LEXP_memory (id, List.map (map_exp_annot f) exps) | LEXP_cast (typ, id) -> LEXP_cast (typ, id) | LEXP_tup lexps -> LEXP_tup (List.map (map_lexp_annot f) lexps) + | LEXP_vector_concat lexps -> LEXP_vector_concat (List.map (map_lexp_annot f) lexps) | LEXP_vector (lexp, exp) -> LEXP_vector (map_lexp_annot f lexp, map_exp_annot f exp) | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2) | LEXP_field (lexp, id) -> LEXP_field (map_lexp_annot f lexp, id) @@ -645,8 +646,8 @@ let rec string_of_exp (E_aux (exp, _)) = | E_try (exp, cases) -> "try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}" | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp - | E_assign (lexp, bind) -> string_of_lexp lexp ^ " := " ^ string_of_exp bind - | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp + | E_assign (lexp, bind) -> string_of_lexp lexp ^ " = " ^ string_of_exp bind + | E_cast (typ, exp) -> string_of_exp exp ^ " : " ^ string_of_typ typ | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]" | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]" | E_vector_update (v, n, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " = " ^ string_of_exp exp ^ "]" @@ -702,7 +703,7 @@ and string_of_pat (P_aux (pat, l)) = | P_wild -> "_" | P_id v -> string_of_id v | P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_typ_pat tpat - | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat + | P_typ (typ, pat) -> string_of_pat pat ^ " : " ^ string_of_typ typ | P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")" | P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")" | P_cons (pat1, pat2) -> string_of_pat pat1 ^ " :: " ^ string_of_pat pat2 @@ -719,7 +720,9 @@ and string_of_lexp (LEXP_aux (lexp, _)) = | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")" | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]" | LEXP_vector_range (lexp, exp1, exp2) -> - string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ ".." ^ string_of_exp exp2 ^ "]" + string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ " .. " ^ string_of_exp exp2 ^ "]" + | LEXP_vector_concat lexps -> + string_of_list " @ " string_of_lexp lexps | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")" and string_of_letbind (LB_aux (lb, l)) = diff --git a/src/initial_check.ml b/src/initial_check.ml index 62c1af02..1ba1b9e6 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -539,35 +539,45 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) ), (l,())) and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = - LEXP_aux( - (match exp with - | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) - | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp) - | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) -> - LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id) - | Parse_ast.E_tuple(tups) -> + let lexp = match exp with + | Parse_ast.E_id id -> LEXP_id (to_ast_id id) + | Parse_ast.E_deref exp -> LEXP_deref (to_ast_exp k_env def_ord exp) + | Parse_ast.E_cast (typ, Parse_ast.E_aux (Parse_ast.E_id id, l')) -> + LEXP_cast (to_ast_typ k_env def_ord typ, to_ast_id id) + | Parse_ast.E_tuple tups -> let ltups = List.map (to_ast_lexp k_env def_ord) tups in - let is_ok_in_tup (LEXP_aux (le,(l,_))) = + let is_ok_in_tup (LEXP_aux (le, (l, _))) = match le with - | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () + | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_vector_concat _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () | LEXP_memory _ | LEXP_deref _ -> - typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in + typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None + in List.iter is_ok_in_tup ltups; - LEXP_tup(ltups) - | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) -> - (match f with - | Parse_ast.Id(id) -> - (match List.map (to_ast_exp k_env def_ord) args with - | [E_aux(E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory(to_ast_id f',[]) - | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps) - | args -> LEXP_memory(to_ast_id f', args)) - | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None) - | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp) - | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> - LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) - | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env def_ord fexp, to_ast_id id) - | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None) - , (l,())) + LEXP_tup ltups + | Parse_ast.E_app ((Parse_ast.Id_aux (f, l') as f'), args) -> + begin match f with + | Parse_ast.Id(id) -> + (match List.map (to_ast_exp k_env def_ord) args with + | [E_aux (E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory (to_ast_id f', []) + | [E_aux (E_tuple exps,_)] -> LEXP_memory (to_ast_id f', exps) + | args -> LEXP_memory(to_ast_id f', args)) + | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None + end + | Parse_ast.E_vector_append (exp1, exp2) -> + LEXP_vector_concat (to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2) + | Parse_ast.E_vector_access (vexp, exp) -> LEXP_vector (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp) + | Parse_ast.E_vector_subrange (vexp, exp1, exp2) -> + LEXP_vector_range (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) + | Parse_ast.E_field (fexp, id) -> LEXP_field (to_ast_lexp k_env def_ord fexp, to_ast_id id) + | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None + in + LEXP_aux (lexp, (l, ())) + +and to_ast_lexp_vector_concat k_env def_ord (Parse_ast.E_aux (exp_aux, l) as exp) = + match exp_aux with + | Parse_ast.E_vector_append (exp1, exp2) -> + to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2 + | _ -> [to_ast_lexp k_env def_ord exp] and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : unit pexp = match pex with diff --git a/src/interpreter.ml b/src/interpreter.ml index 87439e83..e62fcfc3 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -505,6 +505,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = else puts (lstate, { gstate with boxes = StringMap.add name (value_of_exp exp) gstate.boxes }) >> wrap unit_exp | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment" + | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> failwith "Vector concat assignment" (* let values = coerce_tuple (value_of_exp exp) in wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values)) @@ -556,6 +557,9 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) = | LEXP_tup lexps -> mk_exp (E_tuple (List.map exp_of_lexp lexps)) | LEXP_vector (lexp, exp) -> mk_exp (E_vector_access (exp_of_lexp lexp, exp)) | LEXP_vector_range (lexp, exp1, exp2) -> mk_exp (E_vector_subrange (exp_of_lexp lexp, exp1, exp2)) + | LEXP_vector_concat [] -> failwith "Empty LEXP_vector_concat node in exp_of_lexp" + | LEXP_vector_concat [lexp] -> exp_of_lexp lexp + | LEXP_vector_concat (lexp :: lexps) -> mk_exp (E_vector_append (exp_of_lexp lexp, exp_of_lexp (mk_lexp (LEXP_vector_concat lexps)))) | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id)) and pattern_match env (P_aux (p_aux, _) as pat) value = diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 826d8eb1..55ed57d2 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -517,6 +517,7 @@ lexp_aux = (* lvalue expression, can't occur out of the parser *) | LEXP_mem of id * (exp) list | LEXP_vector of lexp * exp (* vector element *) | LEXP_vector_range of lexp * exp * exp (* subvector *) + | LEXP_vector_concat of lexp list | LEXP_field of lexp * id (* struct field *) and lexp = diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index c0658a83..5a26cb42 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -418,6 +418,7 @@ and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) = | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2]) + | LEXP_vector_concat lexps -> parens (separate_map (string " @ ") doc_lexp lexps) | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) | _ -> parens (doc_lexp lexp) and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace diff --git a/src/rewriter.ml b/src/rewriter.ml index 203e8a58..82e3ab05 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -197,6 +197,8 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with | LEXP_memory (_,es) -> union_eff_exps es | LEXP_tup les -> List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les + | LEXP_vector_concat les -> + List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les | LEXP_vector (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e) | LEXP_vector_range (lexp,e1,e2) -> union_effects (effect_of_lexp lexp) @@ -384,6 +386,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters exp1, rewriters.rewrite_exp rewriters exp2)) + | LEXP_vector_concat lexps -> rewrap (LEXP_vector_concat (List.map (rewriters.rewrite_lexp rewriters) lexps)) | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters lexp,id)) let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = @@ -556,6 +559,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_tup : 'lexp list -> 'lexp_aux ; lEXP_vector : 'lexp * 'exp -> 'lexp_aux ; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux + ; lEXP_vector_concat : 'lexp list -> 'lexp_aux ; lEXP_field : 'lexp * id -> 'lexp_aux ; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp ; fE_Fexp : id * 'exp -> 'fexp_aux @@ -635,7 +639,8 @@ and fold_lexp_aux alg = function | LEXP_vector (lexp,e) -> alg.lEXP_vector (fold_lexp alg lexp, fold_exp alg e) | LEXP_vector_range (lexp,e1,e2) -> alg.lEXP_vector_range (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2) - | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id) + | LEXP_vector_concat les -> alg.lEXP_vector_concat (List.map (fold_lexp alg) les) + | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id) and fold_lexp alg (LEXP_aux (lexp_aux,annot)) = alg.lEXP_aux (fold_lexp_aux alg lexp_aux, annot) and fold_fexp_aux alg (FE_Fexp (id,e)) = alg.fE_Fexp (id, fold_exp alg e) @@ -706,6 +711,7 @@ let id_exp_alg = ; lEXP_tup = (fun tups -> LEXP_tup tups) ; lEXP_vector = (fun (lexp,e2) -> LEXP_vector (lexp,e2)) ; lEXP_vector_range = (fun (lexp,e2,e3) -> LEXP_vector_range (lexp,e2,e3)) + ; lEXP_vector_concat = (fun lexps -> LEXP_vector_concat lexps) ; lEXP_field = (fun (lexp,id) -> LEXP_field (lexp,id)) ; lEXP_aux = (fun (lexp,annot) -> LEXP_aux (lexp,annot)) ; fE_Fexp = (fun (id,e) -> FE_Fexp (id,e)) @@ -813,6 +819,9 @@ let compute_exp_alg bot join = ; lEXP_vector = (fun ((vl,lexp),(v2,e2)) -> (join vl v2, LEXP_vector (lexp,e2))) ; lEXP_vector_range = (fun ((vl,lexp),(v2,e2),(v3,e3)) -> (join_list [vl;v2;v3], LEXP_vector_range (lexp,e2,e3))) + ; lEXP_vector_concat = (fun ls -> + let (vs,ls) = List.split ls in + (join_list vs, LEXP_vector_concat ls)) ; lEXP_field = (fun ((vl,lexp),id) -> (vl, LEXP_field (lexp,id))) ; lEXP_aux = (fun ((vl,lexp),annot) -> (vl, LEXP_aux (lexp,annot))) ; fE_Fexp = (fun (id,(v,e)) -> (v, FE_Fexp (id,e))) diff --git a/src/rewriter.mli b/src/rewriter.mli index f8982d69..ccc1f951 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -155,6 +155,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_tup : 'lexp list -> 'lexp_aux ; lEXP_vector : 'lexp * 'exp -> 'lexp_aux ; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux + ; lEXP_vector_concat : 'lexp list -> 'lexp_aux ; lEXP_field : 'lexp * id -> 'lexp_aux ; lEXP_aux : 'lexp_aux * 'a annot -> 'lexp ; fE_Fexp : id * 'exp -> 'fexp_aux @@ -167,7 +168,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; pat_exp : 'pat * 'exp -> 'pexp_aux ; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux ; pat_aux : 'pexp_aux * 'a annot -> 'pexp - ; lB_val : 'pat * 'exp -> 'letbind_aux + ; lB_val : 'pat * 'exp -> 'letbind_aux ; lB_aux : 'letbind_aux * 'a annot -> 'letbind ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } diff --git a/src/rewrites.ml b/src/rewrites.ml index cfeae1e3..a61f2622 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -127,7 +127,7 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with | LEXP_memory _ | LEXP_deref _ -> false | LEXP_id id | LEXP_cast (_, id) -> id_is_local_var id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps + | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps | LEXP_vector (lexp,_) | LEXP_vector_range (lexp,_,_) | LEXP_field (lexp,_) -> lexp_is_local lexp env @@ -136,7 +136,7 @@ let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with | LEXP_memory _ | LEXP_deref _ -> false | LEXP_id id | LEXP_cast (_, id) -> id_is_unbound id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps + | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps | LEXP_vector (lexp,_) | LEXP_vector_range (lexp,_,_) | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env @@ -281,7 +281,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = scope. *) | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) -> let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in - Some (E_aux (E_app (mk_id "add_range", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect)))) + Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect)))) | _ -> begin match destruct_vector env typ with @@ -293,12 +293,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = let rec split_nexp (Nexp_aux (nexp_aux, l) as nexp) = match nexp_aux with | Nexp_sum (n1, n2) -> - mk_exp (E_app (mk_id "add_range", [split_nexp n1; split_nexp n2])) + mk_exp (E_app (mk_id "add_atom", [split_nexp n1; split_nexp n2])) | Nexp_minus (n1, n2) -> - mk_exp (E_app (mk_id "sub_range", [split_nexp n1; split_nexp n2])) + mk_exp (E_app (mk_id "sub_atom", [split_nexp n1; split_nexp n2])) | Nexp_times (n1, n2) -> - mk_exp (E_app (mk_id "mult_range", [split_nexp n1; split_nexp n2])) - | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_range", [split_nexp nexp])) + mk_exp (E_app (mk_id "mult_atom", [split_nexp n1; split_nexp n2])) + | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_atom", [split_nexp nexp])) | _ -> mk_exp (E_sizeof nexp) in let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) = @@ -487,6 +487,7 @@ let rewrite_sizeof (Defs defs) = ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups')) ; lEXP_vector = (fun ((lexp,lexp'),(e2,e2')) -> (LEXP_vector (lexp,e2), LEXP_vector (lexp',e2'))) ; lEXP_vector_range = (fun ((lexp,lexp'),(e2,e2'),(e3,e3')) -> (LEXP_vector_range (lexp,e2,e3), LEXP_vector_range (lexp',e2',e3'))) + ; lEXP_vector_concat = (fun lexps -> let (lexps,lexps') = List.split lexps in (LEXP_vector_concat lexps, LEXP_vector_concat lexps')) ; lEXP_field = (fun ((lexp,lexp'),id) -> (LEXP_field (lexp,id), LEXP_field (lexp',id))) ; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot))) ; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e'))) @@ -2281,11 +2282,11 @@ let rewrite_simple_types (Defs defs) = let defs = Defs (List.map simple_def defs) in rewrite_defs_base simple_defs defs -let rewrite_tuple_vector_assignments defs = +let rewrite_vector_concat_assignments defs = let assign_tuple e_aux annot = let env = env_of_annot annot in match e_aux with - | E_assign (LEXP_aux (LEXP_tup lexps, lannot), exp) -> + | E_assign (LEXP_aux (LEXP_vector_concat lexps, lannot), exp) -> let typ = Env.base_typ_of env (typ_of exp) in if is_vector_typ typ then (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *) @@ -2518,8 +2519,11 @@ let rewrite_defs_letbind_effects = | LEXP_vector_range (lexp,e1,e2) -> n_lexp lexp (fun lexp -> n_exp_name e1 (fun e1 -> - n_exp_name e2 (fun e2 -> + n_exp_name e2 (fun e2 -> k (fix_eff_lexp (LEXP_aux (LEXP_vector_range (lexp,e1,e2),annot)))))) + | LEXP_vector_concat es -> + n_lexpL es (fun es -> + k (fix_eff_lexp (LEXP_aux (LEXP_vector_concat es,annot)))) | LEXP_field (lexp,id) -> n_lexp lexp (fun lexp -> k (fix_eff_lexp (LEXP_aux (LEXP_field (lexp,id),annot)))) @@ -3198,7 +3202,7 @@ let merge_funcls (Defs defs) = let recheck_defs defs = fst (check initial_env defs) let rewrite_defs_lem = [ - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3233,7 +3237,7 @@ let rewrite_defs_ocaml = [ (* ("undefined", rewrite_undefined); *) ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("pat_lits", rewrite_defs_pat_lits); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3252,7 +3256,7 @@ let rewrite_defs_ocaml = [ let rewrite_defs_c = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("pat_lits", rewrite_defs_pat_lits); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); @@ -3268,7 +3272,7 @@ let rewrite_defs_c = [ let rewrite_defs_interpreter = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); diff --git a/src/sail.ml b/src/sail.ml index 4d32fb94..f459d774 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -157,6 +157,9 @@ let options = Arg.align ([ ( "-enum_casts", Arg.Set Initial_check.opt_enum_casts, " allow enumerations to be automatically casted to numeric range types"); + ( "-no_lexp_bounds_check", + Arg.Set Type_check.opt_no_lexp_bounds_check, + " turn off bounds checking for vector assignments in l-expressions"); ( "-no_effects", Arg.Set Type_check.opt_no_effects, " (experimental) turn off effect checking"); diff --git a/src/type_check.ml b/src/type_check.ml index de4c22c3..65d07859 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -63,6 +63,10 @@ let opt_tc_debug = ref 0 re-writer passes, so it should only be used for debugging. *) let opt_no_effects = ref false +(* opt_no_lexp_bounds_check turns of the bounds checking in vector + assignments in l-expressions *) +let opt_no_lexp_bounds_check = ref false + let depth = ref 0 let rec indent n = match n with @@ -314,6 +318,7 @@ module Env : sig val add_union_id : id -> typquant * typ -> t -> t val add_flow : id -> (typ -> typ) -> t -> t val get_flow : id -> t -> typ -> typ + val remove_flow : id -> t -> t val is_register : id -> t -> bool val get_register : id -> t -> typ val add_register : id -> typ -> t -> t @@ -346,7 +351,7 @@ module Env : sig val add_cast : id -> t -> t val allow_polymorphic_undefineds : t -> t val polymorphic_undefineds : t -> bool - val lookup_id : id -> t -> lvar + val lookup_id : ?raw:bool -> id -> t -> lvar val fresh_kid : ?kid:kid -> t -> kid val expand_synonyms : t -> typ -> typ val canonicalize : t -> typ -> typ @@ -856,10 +861,12 @@ end = struct | Not_found -> fun typ -> typ let add_flow id f env = - begin - typ_print (lazy ("Adding flow constraints for " ^ string_of_id id)); - { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow } - end + typ_print (lazy ("Adding flow constraints for " ^ string_of_id id)); + { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow } + + let remove_flow id env = + typ_print (lazy ("Removing flow constraints for " ^ string_of_id id)); + { env with flow = Bindings.remove id env.flow } let is_register id env = Bindings.mem id env.registers @@ -898,11 +905,11 @@ end = struct let get_locals env = env.locals - let lookup_id id env = + let lookup_id ?raw:(raw=false) id env = try let (mut, typ) = Bindings.find id env.locals in let flow = get_flow id env in - Local (mut, flow typ) + Local (mut, if raw then typ else flow typ) with | Not_found -> begin @@ -943,12 +950,11 @@ end = struct let add_constraint (NC_aux (nc_aux, l) as constr) env = wf_constraint env constr; - begin - typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr)); - match nc_aux with - | NC_true -> env - | _ -> { env with constraints = constr :: env.constraints } - end + match nc_aux with + | NC_true -> env + | _ -> + typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr)); + { env with constraints = constr :: env.constraints } let get_ret_typ env = env.ret_typ @@ -1095,6 +1101,12 @@ let destruct_numeric env typ = Some ([kid], nc_true, nvar kid) | _, _ -> None +let bind_numeric l typ env = + match destruct_numeric env typ with + | Some (kids, nc, nexp) -> + nexp, add_existential kids nc env + | None -> typ_error l ("Expected " ^ string_of_typ typ ^ " to be numeric") + (** Pull an (potentially)-existentially qualified type into the global typing environment **) let bind_existential typ env = @@ -1224,7 +1236,7 @@ let prove_z3' env constr = | Constraint.Unknown -> typ_debug (lazy "unknown"); false let prove_z3 env nc = - typ_print (lazy ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); + typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); prove_z3' env (fun var_of -> Constraint.negate (nc_constraint env var_of nc)) let solve env nexp = @@ -1743,7 +1755,10 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t match destruct_exist env typ1, unwrap_exist env (Env.canonicalize env typ2) with | Some (kids, nc, typ1), _ -> let env = add_existential kids nc env in subtyp l env typ1 typ2 + (* | None, ([], _, typ2) -> + typ_error l (string_of_typ typ1 ^ " < " ^ string_of_typ typ2) *) | None, (kids, nc, typ2) -> + typ_debug (lazy "Subtype check with unification"); let env = add_typ_vars kids env in let kids' = KidSet.elements (KidSet.diff (KidSet.of_list kids) (typ_frees typ2)) in let unifiers, existential_kids, existential_nc = @@ -1913,6 +1928,10 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot) let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) +let lexp_typ_of (LEXP_aux (_, (l, tannot))) = typ_of_annot (l, tannot) + +let lexp_env_of (LEXP_aux (_, (l, tannot))) = env_of_annot (l, tannot) + (* Flow typing *) let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with @@ -2096,7 +2115,7 @@ let rec filter_casts env from_typ to_typ casts = let crule r env exp typ = incr depth; - typ_print (lazy ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ)); + typ_print (lazy (Util.("Check " |> cyan |> clear) ^ string_of_exp exp ^ " <= " ^ string_of_typ typ)); try let checked_exp = r env exp typ in decr depth; checked_exp @@ -2107,7 +2126,7 @@ let irule r env exp = incr depth; try let inferred_exp = r env exp in - typ_print (lazy ("Infer " ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp))); + typ_print (lazy (Util.("Infer " |> blue |> clear) ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp))); decr depth; inferred_exp with @@ -2695,7 +2714,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in annot_assign tlexp checked_exp, env' | LEXP_id v when has_typ v env -> - begin match Env.lookup_id v env with + begin match Env.lookup_id ~raw:true v env with | Local (Mutable, vtyp) | Register vtyp -> let checked_exp = crule check_exp env exp vtyp in let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in @@ -2708,9 +2727,26 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as annot_assign tlexp inferred_exp, env' and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = + typ_print (lazy ("Binding mutable " ^ string_of_lexp lexp ^ " to " ^ string_of_typ typ)); let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in match lexp_aux with + | LEXP_cast (typ_annot, v) -> + begin match Env.lookup_id ~raw:true v env with + | Local (Immutable, _) | Enum _ -> + typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Local (Mutable, vtyp) -> + subtyp l env typ typ_annot; + subtyp l env typ_annot vtyp; + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env + | Register vtyp -> + subtyp l env typ typ_annot; + subtyp l env typ_annot vtyp; + annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env + | Unbound -> + subtyp l env typ typ_annot; + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env + end | LEXP_deref exp -> let inferred_exp = infer_exp env exp in begin match typ_of inferred_exp with @@ -2719,39 +2755,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env | _ -> - typ_error l (string_of_typ typ ^ " must be a ref or register type in (*" ^ string_of_exp exp ^ ")") + typ_error l (string_of_typ typ ^ " must be a ref or register type in " ^ string_of_exp exp ^ ")") end | LEXP_id v -> - begin match Env.lookup_id v env with + begin match Env.lookup_id ~raw:true v env with | Local (Immutable, _) | Enum _ -> typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env + | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env end - | LEXP_cast (typ_annot, v) -> - begin - match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Local (Mutable, vtyp) -> - begin - subtyp l env typ typ_annot; - subtyp l env typ_annot vtyp; - annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env - end - | Register vtyp -> - begin - subtyp l env typ typ_annot; - subtyp l env typ_annot vtyp; - annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env - end - | Unbound -> - begin - subtyp l env typ typ_annot; - annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env - end - end | LEXP_tup lexps -> begin let typ = Env.expand_synonyms env typ in @@ -2766,99 +2779,85 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length" in annot_lexp (LEXP_tup tlexps) typ, env - (* This case is pretty much just for the PSTATE. := vector pattern which is really common in ASL. *) - (* Maybe this code can be made not horrible? *) - | Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 -> - begin - match destruct_vector env typ with - | Some (vec_len, _, _) -> - let bind_bits_tuple lexp (tlexps, env, llen) = - match lexp with - | LEXP_aux (LEXP_id v, _) -> - begin - match Env.lookup_id v env with - | Local (Immutable, _) | Enum _ -> - typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) - | Unbound -> - typ_error l "Unbound variable in vector tuple assignment" - | Local (Mutable, vtyp) | Register vtyp -> - let llen' = match destruct_vector env vtyp with - | Some (llen', _, _) -> llen' - | None -> typ_error l "Variables in vector tuple assignment must be vectors" - in - let tlexp, env = bind_lexp env lexp vtyp in - tlexp :: tlexps, env, nsum llen llen' - end - | LEXP_aux (LEXP_field (LEXP_aux (LEXP_id v, _), fid), _) -> - (* FIXME: will only work for ASL *) - let rec_id = - match Env.lookup_id v env with - | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id - | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") - in - let typq, _, vtyp, _ = Env.get_accessor rec_id fid env in - let llen' = match destruct_vector env vtyp with - | Some (llen', _, _) -> llen' - | None -> typ_error l "Variables in vector tuple assignment must be vectors" - in - let tlexp, env = bind_lexp env lexp vtyp in - tlexp :: tlexps, env, nsum llen llen' - | _ -> typ_error l "bit vector assignment must only contain identifiers" - in - let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nint 0) in - if prove env (nc_eq vec_len lexp_len) - then annot_lexp (LEXP_tup tlexps) typ, env - else typ_error l "Vector and tuple length must be the same in assignment" - | None -> typ_error l ("Malformed vector type " ^ string_of_typ typ) + | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple type " ^ string_of_typ typ) + end + | _ -> + let inferred_lexp = infer_lexp env lexp in + subtyp l env typ (lexp_typ_of inferred_lexp); + inferred_lexp, env + +and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) = + let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in + let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in + match lexp_aux with + | LEXP_id v -> + begin match Env.lookup_id v env with + | Local (Mutable, typ) -> annot_lexp (LEXP_id v) typ + (* Probably need to remove flows here *) + | Register typ -> annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]) + | Local (Immutable, _) | Enum _ -> + typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) + | Unbound -> + typ_error l ("Cannot create a new identifier in this l-expression " ^ string_of_lexp lexp) + end + | LEXP_vector_range (v_lexp, exp1, exp2) -> + begin + let inferred_v_lexp = infer_lexp env v_lexp in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let inferred_exp1 = infer_exp env exp1 in + let inferred_exp2 = infer_exp env exp2 in + let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in + let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in + begin match ord with + | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove env (nc_lteq nexp1 nexp2) -> + let len = nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)) in + annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ) + | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove env (nc_gteq nexp1 nexp2) -> + let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in + annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ) + | _ -> typ_error l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp) end - | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ) + | _ -> typ_error l "Cannot assign slice of non vector type" end - | LEXP_vector_range (LEXP_aux (LEXP_id v, _), exp1, exp2) -> + | LEXP_vector (v_lexp, exp) -> begin - let is_immutable, is_register, vtyp = match Env.lookup_id v env with - | Unbound -> typ_error l "Cannot assign to element of unbound vector" - | Enum _ -> typ_error l "Cannot vector assign to enumeration element" - | Local (Immutable, vtyp) -> true, false, vtyp - | Local (Mutable, vtyp) -> false, false, vtyp - | Register vtyp -> false, true, vtyp - in - let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in - let inferred_exp1, inferred_exp2 = match access with - | E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) -> inferred_exp1, inferred_exp2 - | _ -> assert false - in - match typ_of access with - | _ when not is_immutable && is_register -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env - | _ when not is_immutable -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector_range (annot_lexp (LEXP_id v) vtyp, inferred_exp1, inferred_exp2)) typ, env - | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp) + let inferred_v_lexp = infer_lexp env v_lexp in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let inferred_exp = infer_exp env exp in + let nexp, env = bind_numeric l (typ_of inferred_exp) env in + if !opt_no_lexp_bounds_check || prove env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then + annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ + else + typ_error l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp) + | _ -> typ_error l "Cannot assign vector element of non vector type" end - (* Not sure about this case... can the left lexp be anything other than an identifier? *) - | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) -> + | LEXP_vector_concat [] -> typ_error l "Cannot have empty vector concatenation l-expression" + | LEXP_vector_concat (v_lexp :: v_lexps) -> begin - let is_immutable, is_register, vtyp = match Env.lookup_id v env with - | Unbound -> typ_error l "Cannot assign to element of unbound vector" - | Enum _ -> typ_error l "Cannot vector assign to enumeration element" - | Local (Immutable, vtyp) -> true, false, vtyp - | Local (Mutable, vtyp) -> false, false, vtyp - | Register vtyp -> false, true, vtyp - in - let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in - let inferred_exp = match access with - | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp - | _ -> assert false + let sum_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) = + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 && ord_identical ord first_ord -> + typ_equality l env elem_typ first_elem_typ; + nsum acc len + | _ -> typ_error l "Vector concatentation l-expression must only contain vector types of the same order" in - match typ_of access with - | _ when not is_immutable && is_register -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env - | _ when not is_immutable -> - subtyp l env typ (typ_of access); - annot_lexp (LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp)) typ, env - | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp) + let inferred_v_lexp = infer_lexp env v_lexp in + let inferred_v_lexps = List.map (infer_lexp env) v_lexps in + let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in + let v_typs = List.map (fun lexp -> Env.expand_synonyms env (lexp_typ_of lexp)) inferred_v_lexps in + match v_typ_aux with + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) + when Id.compare id (mk_id "vector") = 0 -> + let len = List.fold_left (sum_lengths ord elem_typ) len v_typs in + annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (vector_typ (nexp_simp len) ord elem_typ) + | _ -> typ_error l ("Vector concatentation l-expression must only contain vector types, found " ^ string_of_typ v_typ) end | LEXP_field (LEXP_aux (LEXP_id v, _), fid) -> (* FIXME: will only work for ASL *) @@ -2868,7 +2867,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") in let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in - annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]), env + annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]) | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp) and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = @@ -2951,7 +2950,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_app (f, xs) -> infer_funapp l env f xs None | E_loop (loop_type, cond, body) -> let checked_cond = crule check_exp env cond bool_typ in - let checked_body = crule check_exp env body unit_typ in + let flows, constrs = infer_flow env checked_cond in + let checked_body = crule check_exp (add_flows true flows env) body unit_typ in annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ | E_for (v, f, t, step, ord, body) -> begin @@ -3485,6 +3485,9 @@ and propagate_lexp_effect_aux = function let p_exp2 = propagate_exp_effect exp2 in LEXP_vector_range (p_lexp, p_exp1, p_exp2), union_effects (collect_effects [p_exp1; p_exp2]) (effect_of_lexp p_lexp) + | LEXP_vector_concat lexps -> + let p_lexps = List.map propagate_lexp_effect lexps in + LEXP_vector_concat p_lexps, collect_effects_lexp p_lexps | LEXP_field (lexp, id) -> let p_lexp = propagate_lexp_effect lexp in LEXP_field (p_lexp, id),effect_of_lexp p_lexp diff --git a/src/type_check.mli b/src/type_check.mli index bb52f2aa..ed240839 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -63,6 +63,10 @@ val opt_tc_debug : int ref re-writer passes, so it should only be used for debugging. *) val opt_no_effects : bool ref +(** [opt_no_lexp_bounds_check] turns of the bounds checking in vector + assignments in l-expressions. *) +val opt_no_lexp_bounds_check : bool ref + (** {2 Type errors} *) type type_error = @@ -148,8 +152,9 @@ module Env : sig (** Lookup id searchs for a specified id in the environment, and returns it's type and what kind of identifier it is, using the lvar type. Returns Unbound if the identifier is unbound, and - won't throw any exceptions. *) - val lookup_id : id -> t -> lvar + won't throw any exceptions. If the raw option is true, then look + up the type without any flow typing modifiers. *) + val lookup_id : ?raw:bool -> id -> t -> lvar val is_union_constructor : id -> t -> bool diff --git a/src/value.ml b/src/value.ml index 4b4f0865..e9a98160 100644 --- a/src/value.ml +++ b/src/value.ml @@ -183,6 +183,10 @@ let value_eq_string = function | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2)) | _ -> failwith "value eq_string" +let value_eq_bit = function + | [v1; v2] -> V_bool (Sail_lib.eq_bit (coerce_bit v1, coerce_bit v2)) + | _ -> failwith "value eq_bit" + let value_length = function | [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int) | _ -> failwith "value length" @@ -417,6 +421,7 @@ let primops = ("eq_list", value_eq_list); ("eq_bool", value_eq_bool); ("eq_string", value_eq_string); + ("eq_bit", value_eq_bit); ("eq_anything", value_eq_anything); ("length", value_length); ("subrange", value_subrange); -- cgit v1.2.3 From bdeaec366f85128a43e302b3e5831f9e2bace33c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 3 May 2018 13:57:38 +0100 Subject: Basic Coq constraints --- src/pretty_print_coq.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 347b691d..5af4f417 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -397,6 +397,22 @@ let doc_lit (L_aux(lit,l)) = parens (separate space (List.map string [ "realFromFrac"; Big_int.to_string num; Big_int.to_string denom])) +(* TODO: parens *) +let rec doc_nc (NC_aux (nc,_)) = + match nc with + | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ne1) (doc_nexp ne2) + | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ne1) (doc_nexp ne2) + | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ne1) (doc_nexp ne2) + | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ne1) (doc_nexp ne2) + | NC_set (kid, is) -> (* TODO: is this a good translation? *) + separate space [string "In"; doc_var_lem 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 nc1) (doc_nc nc2) + | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc nc1) (doc_nc nc2) + | NC_true -> string "True" + | NC_false -> string "False" + let doc_quant_item delimit (QI_aux (qi,_)) = match qi with | QI_id (KOpt_aux (KOpt_none kid,_)) -> @@ -408,7 +424,7 @@ let doc_quant_item delimit (QI_aux (qi,_)) = | BK_order -> None end | QI_id _ -> failwith "Quantifier with multiple kinds" - | QI_const nc -> None (* TODO *) + | QI_const nc -> Some (bquote ^^ braces (string "ArithFact" ^^ parens (doc_nc nc))) let doc_typquant_items delimit (TypQ_aux (tq,_)) = match tq with -- cgit v1.2.3 From 266bf3aee70a7003d0779f81370938b0aa7bce03 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 4 May 2018 10:33:45 +0100 Subject: Rename type vars in Coq backend when they clash with identifiers Add value-only version of compute_{pat,exp}_alg to help Experiment with adding equality constraints between type vars and args in Coq output --- src/pretty_print_coq.ml | 171 +++++++++++++++++++++++++++++++++--------------- src/rewriter.ml | 90 +++++++++++++++++++++++++ src/rewriter.mli | 9 +++ 3 files changed, 219 insertions(+), 51 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 5af4f417..a1133e09 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -74,6 +74,7 @@ record update lem/isabelle formatting hacks move List imports + renaming kids bound in fn bodies as well as top-level funcl pattern *) open Type_check @@ -83,15 +84,22 @@ open Rewriter open PPrint open Pretty_print_common +module StringSet = Set.Make(String) + (**************************************************************************** * PPrint-based sail-to-coq pprinter ****************************************************************************) type context = { early_ret : bool; + kid_renames : kid KBindings.t; bound_nexps : NexpSet.t; } -let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty } +let empty_ctxt = { + early_ret = false; + kid_renames = KBindings.empty; + bound_nexps = NexpSet.empty +} let langlebar = string "<|" let ranglebar = string "|>" @@ -162,7 +170,7 @@ let doc_id_ctor (Id_aux(i,_)) = * token in case of x ending with star. *) separate space [colon; string x; empty] -let doc_var_lem kid = string (fix_id true (string_of_kid kid)) +let doc_var_lem ctx kid = string (fix_id true (string_of_kid (try KBindings.find kid ctx.kid_renames with Not_found -> kid))) let doc_docstring_lem (l, _) = match l with | Parse_ast.Documented (str, _) -> string ("(*" ^ str ^ "*)") ^^ hardline @@ -191,11 +199,11 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with | Typ_app(id, _) when string_of_id id = "register" -> true | _ -> false -let doc_nexp nexp = +let doc_nexp ctx nexp = let (Nexp_aux (nexp, l) as full_nexp) = nexp_simp nexp in match nexp with | Nexp_constant i -> string (Big_int.to_string i) - | Nexp_var v -> doc_var_lem v + | Nexp_var v -> doc_var_lem ctx v | Nexp_id id -> doc_id id | Nexp_times (n1, n2) -> separate space [doc_nexp n1; star; doc_nexp n2] | Nexp_sum (n1, n2) -> separate space [doc_nexp n1; plus; doc_nexp n2] @@ -259,6 +267,7 @@ let lem_tyvars_of_typ typ = (* When making changes here, check whether they affect lem_tyvars_of_typ *) let doc_typ, doc_atomic_typ = + let fns ctx = (* following the structure of parser for precedence *) let rec typ ty = fn_typ true ty and typ' ty = fn_typ false ty @@ -287,7 +296,7 @@ let doc_typ, doc_atomic_typ = Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> let tpp = match elem_typ with | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> - string "mword " ^^ doc_nexp (nexp_simp m) + string "mword " ^^ doc_nexp ctx (nexp_simp m) | _ -> string "list" ^^ space ^^ typ elem_typ in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> @@ -310,7 +319,7 @@ let doc_typ, doc_atomic_typ = (*if List.exists ((=) (string_of_id id)) regtypes then string "register" else*) doc_id_type id - | Typ_var v -> doc_var_lem v + | Typ_var v -> doc_var_lem ctx v | Typ_app _ | Typ_tup _ | Typ_fn _ -> (* exhaustiveness matters here to avoid infinite loops * if we add a new Typ constructor *) @@ -323,9 +332,10 @@ tpp (* List.fold_left tpp kids*) and doc_typ_arg (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ t -> app_typ true t - | Typ_arg_nexp n -> doc_nexp n + | Typ_arg_nexp n -> doc_nexp ctx n | Typ_arg_order o -> empty in typ', atomic_typ + in (fun ctx -> (fst (fns ctx))), (fun ctx -> (snd (fns ctx))) (* Check for variables in types that would be pretty-printed and are not bound in the val spec of the function. *) @@ -353,7 +363,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let doc_tannot_lem ctxt env eff typ = let of_typ typ = - let ta = doc_typ typ in + let ta = doc_typ ctxt typ in if eff then string " : M " ^^ parens ta else string " : " ^^ ta in @@ -398,42 +408,42 @@ let doc_lit (L_aux(lit,l)) = "realFromFrac"; Big_int.to_string num; Big_int.to_string denom])) (* TODO: parens *) -let rec doc_nc (NC_aux (nc,_)) = +let rec doc_nc ctx (NC_aux (nc,_)) = match nc with - | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ne1) (doc_nexp ne2) - | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ne1) (doc_nexp ne2) - | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ne1) (doc_nexp ne2) - | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ne1) (doc_nexp ne2) + | 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? *) - separate space [string "In"; doc_var_lem kid; + 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 nc1) (doc_nc nc2) - | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc nc1) (doc_nc nc2) + | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc ctx nc1) (doc_nc ctx nc2) + | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc ctx nc1) (doc_nc ctx nc2) | NC_true -> string "True" | NC_false -> string "False" -let doc_quant_item delimit (QI_aux (qi,_)) = +let doc_quant_item ctx delimit (QI_aux (qi,_)) = match qi with | QI_id (KOpt_aux (KOpt_none kid,_)) -> - Some (delimit (separate space [doc_var_lem kid; colon; string "Z"])) + Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Z"])) | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (kind,_)],_),kid),_)) -> begin match kind with - | BK_type -> Some (delimit (separate space [doc_var_lem kid; colon; string "Type"])) - | BK_int -> Some (delimit (separate space [doc_var_lem kid; colon; string "Z"])) + | BK_type -> Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Type"])) + | BK_int -> Some (delimit (separate space [doc_var_lem ctx kid; colon; string "Z"])) | BK_order -> None end | QI_id _ -> failwith "Quantifier with multiple kinds" - | QI_const nc -> Some (bquote ^^ braces (string "ArithFact" ^^ parens (doc_nc nc))) + | QI_const nc -> Some (bquote ^^ braces (string "ArithFact" ^^ parens (doc_nc ctx nc))) -let doc_typquant_items delimit (TypQ_aux (tq,_)) = +let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) = match tq with - | TypQ_tq qis -> separate_opt space (doc_quant_item delimit) qis + | TypQ_tq qis -> separate_opt space (doc_quant_item ctx delimit) qis | TypQ_no_forall -> empty -let doc_typquant (TypQ_aux(tq,_)) typ = match tq with +let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with | TypQ_tq ((_ :: _) as qs) -> - string "forall " ^^ separate_opt space (doc_quant_item parens) qs ^^ string ". " ^^ typ + string "forall " ^^ separate_opt space (doc_quant_item ctx parens) qs ^^ string ". " ^^ typ | _ -> typ (* Produce Size type constraints for bitvector sizes when using @@ -458,9 +468,9 @@ let rec typeclass_nexps (Typ_aux(t,_)) = | Typ_app _ -> NexpSet.empty | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *) -let doc_typschm quants (TypSchm_aux(TypSchm_ts(tq,t),_)) = - let pt = doc_typ t in - if quants then doc_typquant tq pt else pt +let doc_typschm ctx quants (TypSchm_aux(TypSchm_ts(tq,t),_)) = + let pt = doc_typ ctx t in + if quants then doc_typquant ctx tq pt else pt let is_ctor env id = match Env.lookup_id id env with | Enum _ -> true @@ -715,8 +725,8 @@ let doc_exp_lem, doc_let_lem = aexp_needed, epp else let tannot = separate space [string "MR"; - doc_atomic_typ false (typ_of full_exp); - doc_atomic_typ false (typ_of exp)] in + doc_atomic_typ ctxt false (typ_of full_exp); + doc_atomic_typ ctxt false (typ_of exp)] in true, doc_op colon epp tannot in if aexp_needed then parens tepp else tepp | _ -> raise (Reporting_basic.err_unreachable l @@ -906,8 +916,8 @@ let doc_exp_lem, doc_let_lem = then empty else separate space [string ret_monad; - parens (doc_typ (typ_of full_exp)); - parens (doc_typ (typ_of r))] in + parens (doc_typ ctxt (typ_of full_exp)); + parens (doc_typ ctxt (typ_of r))] in align (parens (string "early_return" ^//^ expV true r ^//^ ta)) | E_constraint _ -> string "true" | E_comment _ | E_comment_struc _ -> empty @@ -960,9 +970,9 @@ let doc_exp_lem, doc_let_lem = (* expose doc_exp_lem and doc_let *) in top_exp, let_exp -let doc_type_union typ_name (Tu_aux(Tu_ty_id(typ,id),_)) = +let doc_type_union ctxt typ_name (Tu_aux(Tu_ty_id(typ,id),_)) = separate space [doc_id_ctor id; colon; - doc_typ typ; arrow; typ_name] + doc_typ ctxt typ; arrow; typ_name] let rec doc_range_lem (BF_aux(r,_)) = match r with | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i)) @@ -972,14 +982,14 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with let doc_typdef (TD_aux(td, (l, annot))) = match td with | TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) -> doc_op coloneq - (separate space [string "Definition"; doc_id_type id; doc_typquant_items parens typq]) - (doc_typschm false typschm) ^^ dot + (separate space [string "Definition"; doc_id_type id; doc_typquant_items empty_ctxt parens typq]) + (doc_typschm empty_ctxt false typschm) ^^ dot | TD_record(id,nm,typq,fs,_) -> let fname fid = if prefix_recordtype && string_of_id id <> "regstate" then concat [doc_id id;string "_";doc_id_type fid;] else doc_id_type fid in let f_pp (typ,fid) = - concat [fname fid;space;colon;space;doc_typ typ; semi] in + concat [fname fid;space;colon;space;doc_typ empty_ctxt typ; semi] in let rectyp = match typq with | TypQ_aux (TypQ_tq qs, _) -> let quant_item = function @@ -1035,7 +1045,7 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in *) doc_op coloneq - (separate space [string "Record"; doc_id_type id; doc_typquant_items parens typq]) + (separate space [string "Record"; doc_id_type id; doc_typquant_items empty_ctxt parens typq]) ((*doc_typquant_lem typq*) (braces (space ^^ align fs_doc ^^ space))) ^^ dot ^^ hardline ^^ updates_pp | TD_variant(id,nm,typq,ar,_) -> @@ -1050,8 +1060,8 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with | Id_aux ((Id "diafp"),_) -> empty *) | Id_aux ((Id "option"),_) -> empty | _ -> - let typ_nm = separate space [doc_id_type id; doc_typquant_items parens typq] in - let ar_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_type_union typ_nm) ar) in + let typ_nm = separate space [doc_id_type id; doc_typquant_items empty_ctxt parens typq] in + let ar_doc = group (separate_map (break 1 ^^ pipe ^^ space) (doc_type_union empty_ctxt typ_nm) ar) in let typ_pp = (doc_op coloneq) (concat [string "Inductive"; space; typ_nm]) @@ -1114,9 +1124,6 @@ let doc_rec (Rec_aux(r,_)) = match r with | Rec_nonrec -> string "Definition" | Rec_rec -> string "Fixpoint" -let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with - | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ typ) - let doc_fun_body ctxt exp = let doc_exp = doc_exp_lem ctxt false exp in if ctxt.early_ret @@ -1135,26 +1142,90 @@ let demote_as_pattern i (P_aux (_,p_annot) as pat,typ) = E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann) else (pat,typ), fun e -> e +(* Ideally we'd remove the duplication between type variables and atom + arguments, but for now we just add an equality constraint. *) + +let atom_constraint ctxt (pat, typ) = + let typ = Env.base_typ_of (pat_env_of pat) typ in + match pat, typ with + | P_aux (P_id id, _), + Typ_aux (Typ_app (Id_aux (Id "atom",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_) -> + Some (bquote ^^ braces (string "ArithFact" ^^ space ^^ + parens (doc_op equals (doc_id id) (doc_var_lem ctxt kid)))) + | _ -> None + +let all_ids pexp = + let open Rewriter in + fold_pexp ( + { (pure_exp_alg IdSet.empty IdSet.union) with + e_id = (fun id -> IdSet.singleton id); + e_ref = (fun id -> IdSet.singleton id); + e_app = (fun (id,ids) -> + List.fold_left IdSet.union (IdSet.singleton id) ids); + e_app_infix = (fun (ids1,id,ids2) -> + IdSet.add id (IdSet.union ids1 ids2)); + e_for = (fun (id,ids1,ids2,ids3,_,ids4) -> + IdSet.add id (IdSet.union ids1 (IdSet.union ids2 (IdSet.union ids3 ids4)))); + lEXP_id = IdSet.singleton; + lEXP_memory = (fun (id,ids) -> + List.fold_left IdSet.union (IdSet.singleton id) ids); + lEXP_cast = (fun (_,id) -> IdSet.singleton id); + pat_alg = { (pure_pat_alg IdSet.empty IdSet.union) with + p_as = (fun (ids,id) -> IdSet.add id ids); + p_id = IdSet.singleton; + p_app = (fun (id,ids) -> + List.fold_left IdSet.union (IdSet.singleton id) ids); + } + }) pexp + +let tyvars_of_typquant (TypQ_aux (tq,_)) = + match tq with + | TypQ_no_forall -> KidSet.empty + | TypQ_tq qs -> List.fold_left KidSet.union KidSet.empty + (List.map tyvars_of_quant_item qs) + +let mk_kid_renames ids_to_avoid kids = + let map_id = function + | Id_aux (Id i, _) -> Some (fix_id false i) + | Id_aux (DeIid _, _) -> None + in + let ids = StringSet.of_list (Util.map_filter map_id (IdSet.elements ids_to_avoid)) in + let rec check_kid kid (newkids,rebindings) = + let rec check kid1 = + let kid_string = fix_id true (string_of_kid kid1) in + if StringSet.mem kid_string ids + then let kid2 = match kid1 with Kid_aux (Var x,l) -> Kid_aux (Var (x ^ "0"),l) in + check kid2 + else + KidSet.add kid1 newkids, KBindings.add kid kid1 rebindings + in check kid + in snd (KidSet.fold check_kid kids (kids, KBindings.empty)) + let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in let (arg_typ, ret_typ, eff) = match typ with | Typ_aux (Typ_fn (arg_typ, ret_typ, eff),_) -> arg_typ, ret_typ, eff | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type") in + let ids_to_avoid = all_ids pexp in + let kids_used = tyvars_of_typquant tq in let pat,guard,exp,(l,_) = destruct_pexp pexp in let ctxt = { early_ret = contains_early_return exp; + kid_renames = mk_kid_renames ids_to_avoid kids_used; bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ) } in - let quantspp = doc_typquant_items braces tq in + let quantspp = doc_typquant_items ctxt braces tq in let pats, bind = untuple_args_pat arg_typ pat in let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in let exp = List.fold_left (fun body f -> f body) (bind exp) binds in let patspp = separate_map space (fun (pat,typ) -> - squote ^^ parens (separate space [doc_pat ctxt true pat; colon; doc_typ typ])) pats in + squote ^^ parens (separate space [doc_pat ctxt true pat; colon; doc_typ ctxt typ])) pats in + let atom_constr_pp = separate_opt space (atom_constraint ctxt) pats in let retpp = if effectful eff - then string "M" ^^ space ^^ parens (doc_typ ret_typ) - else doc_typ ret_typ + then string "M" ^^ space ^^ parens (doc_typ ctxt ret_typ) + else doc_typ ctxt ret_typ in let _ = match guard with | None -> () @@ -1162,15 +1233,13 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = raise (Reporting_basic.err_unreachable l "guarded pattern expression should have been rewritten before pretty-printing") in group (prefix 3 1 - (separate space [doc_id id; quantspp; patspp; colon; retpp; coloneq]) + (separate space [doc_id id; quantspp; patspp; atom_constr_pp; colon; retpp; coloneq]) (doc_fun_body ctxt exp ^^ dot)) let get_id = function | [] -> failwith "FD_function with empty list" | (FCL_aux (FCL_Funcl (id,_),_))::_ -> id -module StringSet = Set.Make(String) - (* Strictly speaking, Lem doesn't support multiple clauses for a single function joined by "and", although it has worked for Isabelle before. However, all the funcls should have been merged by the merge_funcls rewrite now. *) @@ -1275,7 +1344,7 @@ let rec doc_def def = | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline | DEF_val (LB_aux (LB_val (pat, exp), _)) -> let (id,typpp) = match pat with - | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, space ^^ colon ^^ space ^^ doc_typ typ + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, space ^^ colon ^^ space ^^ doc_typ empty_ctxt typ | P_aux (P_id id, _) -> id, empty | _ -> failwith "Top-level value definition with complex pattern not supported for Coq yet" in diff --git a/src/rewriter.ml b/src/rewriter.ml index 82e3ab05..7d10e570 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -840,3 +840,93 @@ let compute_exp_alg bot join = ; lB_aux = (fun ((vl,lb),annot) -> (vl,LB_aux (lb,annot))) ; pat_alg = compute_pat_alg bot join } + +let pure_pat_alg bot join = + let join_list vs = List.fold_left join bot vs in + { p_lit = (fun lit -> bot) + ; p_wild = bot + ; p_as = (fun (v,id) -> v) + ; p_typ = (fun (typ,v) -> v) + ; p_id = (fun id -> bot) + ; p_var = (fun (v,kid) -> v) + ; p_app = (fun (id,ps) -> join_list ps) + ; p_record = (fun (ps,b) -> join_list ps) + ; p_vector = join_list + ; p_vector_concat = join_list + ; p_tup = join_list + ; p_list = join_list + ; p_cons = (fun (vh,vt) -> join vh vt) + ; p_aux = (fun (v,annot) -> v) + ; fP_aux = (fun (v,annot) -> v) + ; fP_Fpat = (fun (id,v) -> v) + } + +let pure_exp_alg bot join = + let join_list vs = List.fold_left join bot vs in + { e_block = join_list + ; e_nondet = join_list + ; e_id = (fun id -> bot) + ; e_ref = (fun id -> bot) + ; e_lit = (fun lit -> bot) + ; e_cast = (fun (typ,v) -> v) + ; e_app = (fun (id,es) -> join_list es) + ; e_app_infix = (fun (v1,id,v2) -> join v1 v2) + ; e_tuple = join_list + ; e_if = (fun (v1,v2,v3) -> join_list [v1;v2;v3]) + ; e_for = (fun (id,v1,v2,v3,order,v4) -> join_list [v1;v2;v3;v4]) + ; e_loop = (fun (lt, v1, v2) -> join v1 v2) + ; e_vector = join_list + ; e_vector_access = (fun (v1,v2) -> join v1 v2) + ; e_vector_subrange = (fun (v1,v2,v3) -> join_list [v1;v2;v3]) + ; e_vector_update = (fun (v1,v2,v3) -> join_list [v1;v2;v3]) + ; e_vector_update_subrange = (fun (v1,v2,v3,v4) -> join_list [v1;v2;v3;v4]) + ; e_vector_append = (fun (v1,v2) -> join v1 v2) + ; e_list = join_list + ; e_cons = (fun (v1,v2) -> join v1 v2) + ; e_record = (fun vs -> vs) + ; e_record_update = (fun (v1,vf) -> join v1 vf) + ; e_field = (fun (v1,id) -> v1) + ; e_case = (fun (v1,vps) -> join_list (v1::vps)) + ; e_try = (fun (v1,vps) -> join_list (v1::vps)) + ; e_let = (fun (vl,v2) -> join vl v2) + ; e_assign = (fun (vl,v2) -> join vl v2) + ; e_sizeof = (fun nexp -> bot) + ; e_constraint = (fun nc -> bot) + ; e_exit = (fun v1 -> v1) + ; e_throw = (fun v1 -> v1) + ; e_return = (fun v1 -> v1) + ; e_assert = (fun (v1,v2) -> join v1 v2) + ; e_internal_cast = (fun (a,v1) -> v1) + ; e_internal_exp = (fun a -> bot) + ; e_internal_exp_user = (fun (a1,a2) -> bot) + ; e_comment = (fun c -> bot) + ; e_comment_struc = (fun v -> bot) + ; e_internal_let = (fun (vl, v2, v3) -> join_list [vl;v2;v3]) + ; e_internal_plet = (fun (vp, v1, v2) -> join_list [vp;v1;v2]) + ; e_internal_return = (fun v -> v) + ; e_internal_value = (fun v -> bot) + ; e_aux = (fun (v,annot) -> v) + ; lEXP_id = (fun id -> bot) + ; lEXP_deref = (fun v -> v) + ; lEXP_memory = (fun (id,es) -> join_list es) + ; lEXP_cast = (fun (typ,id) -> bot) + ; lEXP_tup = join_list + ; lEXP_vector = (fun (vl,v2) -> join vl v2) + ; lEXP_vector_range = (fun (vl,v2,v3) -> join_list [vl;v2;v3]) + ; lEXP_vector_concat = join_list + ; lEXP_field = (fun (vl,id) -> vl) + ; lEXP_aux = (fun (vl,annot) -> vl) + ; fE_Fexp = (fun (id,v) -> v) + ; fE_aux = (fun (vf,annot) -> vf) + ; fES_Fexps = (fun (vs,b) -> join_list vs) + ; fES_aux = (fun (vf,annot) -> vf) + ; def_val_empty = bot + ; def_val_dec = (fun v -> v) + ; def_val_aux = (fun (v,aux) -> v) + ; pat_exp = (fun (vp,v) -> join vp v) + ; pat_when = (fun (vp,v,v') -> join_list [vp;v;v']) + ; pat_aux = (fun (v,a) -> v) + ; lB_val = (fun (vp,v) -> join vp v) + ; lB_aux = (fun (vl,annot) -> vl) + ; pat_alg = pure_pat_alg bot join + } diff --git a/src/rewriter.mli b/src/rewriter.mli index ccc1f951..cdacf222 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -203,6 +203,15 @@ val compute_exp_alg : 'b -> ('b -> 'b -> 'b) -> ('b * 'a letbind_aux),('b * 'a letbind), ('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) exp_alg +val pure_pat_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b,'b,'b) pat_alg + +val pure_exp_alg : 'b -> ('b -> 'b -> 'b) -> + ('a,'b,'b,'b,'b,'b, + 'b,'b,'b, + 'b,'b,'b,'b, + 'b,'b, + 'b,'b,'b,'b) exp_alg + val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot val add_p_typ : typ -> tannot pat -> tannot pat -- cgit v1.2.3 From 1653f1816406f9b70de66f9b2427df71f1c5a1a2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 4 May 2018 12:00:44 +0100 Subject: Start updating monomorphisation + add additional lexp + update aarch64 mono demo source - still needs support for tyvars from assignments in dependency analysis --- src/monomorphise.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 75b82da2..c743ac61 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -636,6 +636,7 @@ let nexp_subst_fns substs = | LEXP_tup les -> re (LEXP_tup (List.map s_lexp les)) | LEXP_vector (le,e) -> re (LEXP_vector (s_lexp le, s_exp e)) | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (s_lexp le, s_exp e1, s_exp e2)) + | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map s_lexp les)) | LEXP_field (le,id) -> re (LEXP_field (s_lexp le, id)) | LEXP_deref e -> re (LEXP_deref (s_exp e)) in (s_pat,s_exp) @@ -955,7 +956,9 @@ let rec assigned_vars_in_lexp (LEXP_aux (le,_)) = match le with | LEXP_id id | LEXP_cast (_,id) -> IdSet.singleton id - | LEXP_tup lexps -> List.fold_left (fun vs le -> IdSet.union vs (assigned_vars_in_lexp le)) IdSet.empty lexps + | LEXP_tup lexps + | LEXP_vector_concat lexps -> + List.fold_left (fun vs le -> IdSet.union vs (assigned_vars_in_lexp le)) IdSet.empty lexps | LEXP_memory (_,es) -> List.fold_left (fun vs e -> IdSet.union vs (assigned_vars e)) IdSet.empty es | LEXP_vector (le,e) -> IdSet.union (assigned_vars_in_lexp le) (assigned_vars e) | LEXP_vector_range (le,e1,e2) -> @@ -1468,6 +1471,7 @@ let split_defs all_errors splits defs = re (LEXP_vector_range (fst (const_prop_lexp ref_vars substs assigns le), fst (const_prop_exp ref_vars substs assigns e1), fst (const_prop_exp ref_vars substs assigns e2))) + | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map (fun le -> fst (const_prop_lexp ref_vars substs assigns le)) les)) | LEXP_field (le,id) -> re (LEXP_field (fst (const_prop_lexp ref_vars substs assigns le), id)) | LEXP_deref e -> re (LEXP_deref (fst (const_prop_exp ref_vars substs assigns e))) @@ -2014,6 +2018,7 @@ let split_defs all_errors splits defs = | LEXP_tup les -> re (LEXP_tup (List.map map_lexp les)) | LEXP_vector (le,e) -> re (LEXP_vector (map_lexp le, map_exp e)) | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (map_lexp le, map_exp e1, map_exp e2)) + | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map map_lexp les)) | LEXP_field (le,id) -> re (LEXP_field (map_lexp le, id)) | LEXP_deref e -> re (LEXP_deref (map_exp e)) in map_pexp, map_letbind @@ -3120,7 +3125,8 @@ and analyse_lexp fn_id env assigns deps (LEXP_aux (lexp,(l,_))) = | LEXP_memory (id,es) -> let _, assigns, r = analyse_exp fn_id env assigns (E_aux (E_tuple es,(Unknown,None))) in assigns, r - | LEXP_tup lexps -> + | LEXP_tup lexps + | LEXP_vector_concat lexps -> List.fold_left (fun (assigns,r) lexp -> let assigns,r' = analyse_lexp fn_id env assigns deps lexp in assigns,merge r r') (assigns,empty) lexps -- cgit v1.2.3 From 09bfbe239b1b5d8627f84a8115cfaf9f83114ba5 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 4 May 2018 16:12:28 +0100 Subject: Fix mono cast introduction to avoid a checking to inference change Adds return type to pattern so that the original function body is still type checked, rather than switching to type inference which may fail. --- src/monomorphise.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index c743ac61..fcace50f 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3781,7 +3781,7 @@ let make_bitvector_cast_fns env src_typ target_typ = match src_t, tar_t with | Typ_tup typs, Typ_tup typs' -> let ps,es = List.split (List.map2 aux typs typs') in - P_aux (P_tup ps,(Generated src_l, src_ann)), + P_aux (P_typ (src_typ, P_aux (P_tup ps,(Generated src_l, src_ann))),(Generated src_l, src_ann)), E_aux (E_tuple es,(Generated tar_l, tar_ann)) | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp size,_); _; -- cgit v1.2.3 From 664a78f7517ecf93ee1694784819cfa1ee894b80 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 4 May 2018 16:13:06 +0100 Subject: Add support for top-level values to monomorphisation singleton rewrite --- src/monomorphise.ml | 10 ++++++++++ src/rewriter.mli | 4 ++++ 2 files changed, 14 insertions(+) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index fcace50f..0585d9fa 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2359,10 +2359,20 @@ let rewrite_size_parameters env (Defs defs) = | Some exp -> Some (fold_exp { id_exp_alg with e_app = rewrite_e_app } exp) in FCL_aux (FCL_Funcl (id,construct_pexp (pat,guard,body,(pl,None))),(l,None)) in + let rewrite_letbind lb = + let rewrite_e_app (id,args) = + match Bindings.find id fn_sizes with + | to_change,_ -> + let args' = mapat (replace_with_the_value []) to_change args in + E_app (id,args') + | exception Not_found -> E_app (id,args) + in fold_letbind { id_exp_alg with e_app = rewrite_e_app } lb + in let rewrite_def = function | DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) -> (* TODO rewrite tannopt? *) DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,None))) + | DEF_val lb -> DEF_val (rewrite_letbind lb) | DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec -> begin match Bindings.find id fn_sizes with diff --git a/src/rewriter.mli b/src/rewriter.mli index cdacf222..6e9f08c2 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -181,6 +181,10 @@ val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_a 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp +val fold_letbind : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, + 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, + 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a letbind -> 'letbind + val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp -- cgit v1.2.3 From e87d2f43beb17cec230d359189842afc5dfcb3b7 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 4 May 2018 18:52:13 +0100 Subject: Rewrite constant nexps in specs (from Thomas) --- src/rewrites.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index a61f2622..debce3d1 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -241,8 +241,19 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = | (l, None) -> (l, None) in - rewrite_defs_base { - rewriters_base with rewrite_exp = (fun _ -> map_exp_annot rewrite_annot) + let rewrite_def rewriters = function + | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, Some (env, typ, eff)))) -> + let typschm = match typschm with + | TypSchm_aux (TypSchm_ts (tq, typ), l) -> + TypSchm_aux (TypSchm_ts (tq, rewrite_typ env typ), l) + in + let a = rewrite_annot (l, Some (env, typ, eff)) in + DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a)) + | d -> Rewriter.rewrite_def rewriters d + in + + rewrite_defs_base { rewriters_base with + rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); rewrite_def = rewrite_def }, rewrite_typ -- cgit v1.2.3 From 714d62a0ea695081ad16d2cfac0997024eb13de9 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 4 May 2018 18:52:50 +0100 Subject: Fix missing nexp id rewriting --- src/rewrites.ml | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index debce3d1..950b7c5f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -190,16 +190,18 @@ let lookup_equal_kids env = List.fold_left add_nc KBindings.empty (Env.get_constraints env) let lookup_constant_kid env kid = - try - let kids = KBindings.find kid (lookup_equal_kids env) in - let check_nc const nc = match const, nc with - | None, NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant i, _)), _) - when KidSet.mem kid kids -> - Some i - | _, _ -> const - in - List.fold_left check_nc None (Env.get_constraints env) - with Not_found -> None + let kids = + match KBindings.find kid (lookup_equal_kids env) with + | kids -> kids + | exception Not_found -> KidSet.singleton kid + in + let check_nc const nc = match const, nc with + | None, NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant i, _)), _) + when KidSet.mem kid kids -> + Some i + | _, _ -> const + in + List.fold_left check_nc None (Env.get_constraints env) let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with | Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env) -- cgit v1.2.3 From 066ecac9d79769e1a759f8ed1b13b18548aef36c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 4 May 2018 18:53:50 +0100 Subject: Checked that variable names in split_fun rewrites are really variables Otherwise some clauses disappear --- src/rewrites.ml | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/rewrites.ml b/src/rewrites.ml index 950b7c5f..582901dc 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1914,6 +1914,16 @@ let is_funcl_rec (FCL_aux (FCL_Funcl (id, pexp), _)) = E_app_infix (e1, f, e2))) } exp) + +let pat_var (P_aux (paux, a)) = + let env = env_of_annot a in + let is_var id = + not (Env.is_union_constructor id env) && + match Env.lookup_id id env with Enum _ -> false | _ -> true + in match paux with + | (P_as (_, id) | P_id id) when is_var id -> Some id + | _ -> None + (* Split out function clauses for individual union constructor patterns (e.g. AST nodes) into auxiliary functions. Used for the execute function. *) let rewrite_split_fun_constr_pats fun_name (Defs defs) = @@ -1938,10 +1948,10 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) = Bindings.add aux_fun_id (aux_clauses @ [aux_funcl]) aux_funs with Not_found -> let argpats, argexps = List.split (List.mapi - (fun idx (P_aux (paux, a)) -> - let id = match paux with - | P_as (_, id) | P_id id -> id - | _ -> mk_id ("arg" ^ string_of_int idx) + (fun idx (P_aux (_,a) as pat) -> + let id = match pat_var pat with + | Some id -> id + | None -> mk_id ("arg" ^ string_of_int idx) in P_aux (P_id id, a), E_aux (E_id id, a)) args) -- cgit v1.2.3 From faec5d87b9d9690b1c95928d2d932d5d51d94cd4 Mon Sep 17 00:00:00 2001 From: emersion Date: Wed, 9 May 2018 12:30:32 +0100 Subject: Fix Byte_sequence errors due to linksem update --- src/elf_loader.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/elf_loader.ml b/src/elf_loader.ml index 89987647..02ff072b 100644 --- a/src/elf_loader.ml +++ b/src/elf_loader.ml @@ -65,9 +65,9 @@ let rec break n = function | (_ :: _ as xs) -> [Lem_list.take n xs] @ break n (Lem_list.drop n xs) let print_segment seg = - let (Byte_sequence.Sequence bs) = seg.Elf_interpreted_segment.elf64_segment_body in + let bs = seg.Elf_interpreted_segment.elf64_segment_body in prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef"; - List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 bs) + List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 (Byte_sequence.char_list_of_byte_sequence bs)) let read name = let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in @@ -112,7 +112,7 @@ let write_file chan paddr i byte = let load_segment ?writer:(writer=write_sail_lib) seg = let open Elf_interpreted_segment in - let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in + let bs = seg.elf64_segment_body in let paddr = seg.elf64_segment_paddr in let base = seg.elf64_segment_base in let offset = seg.elf64_segment_offset in @@ -121,7 +121,7 @@ let load_segment ?writer:(writer=write_sail_lib) seg = prerr_endline ("Segment base address: " ^ Big_int.to_string base); prerr_endline ("Segment physical address: " ^ Big_int.to_string paddr); print_segment seg; - List.iteri (writer paddr) (List.map int_of_char bs) + List.iteri (writer paddr) (List.map int_of_char (Byte_sequence.char_list_of_byte_sequence bs)) let load_elf ?writer:(writer=write_sail_lib) name = let segments, e_entry, symbol_map = read name in -- cgit v1.2.3 From 9fea45722d58132cc484d9421fb3407286dc4f01 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 4 May 2018 16:18:01 +0100 Subject: Generate initial register state record Filled with default values (e.g., 0) and used to initialise the state monad. There is already code to generate a Sail function "initialize_registers", but this is monadic itself, so it cannot be used to initialise the monad. --- src/state.ml | 131 +++++++++++++++++++++++++++++++++++++++++++---------- src/type_check.mli | 3 ++ 2 files changed, 111 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/state.ml b/src/state.ml index 49fa5a99..5a360456 100644 --- a/src/state.ml +++ b/src/state.ml @@ -60,6 +60,11 @@ open Pretty_print_sail let defs_of_string = ast_of_def_string Ast_util.inc_ord +let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs)) + +let has_default_order defs = + List.exists (function DEF_default (DT_aux (DT_order _, _)) -> true | _ -> false) defs + let find_registers defs = List.fold_left (fun acc def -> @@ -77,18 +82,100 @@ let generate_regstate = function | [] -> ["type regstate = unit"] | registers -> let reg (typ, id) = Printf.sprintf "%s : %s" (string_of_id id) (to_string (doc_typ typ)) in - let initreg (_, id) = Printf.sprintf "%s = undefined" (string_of_id id) in - let regstate = - "struct regstate = { " ^ - (String.concat ", " (List.map reg registers)) ^ - " }" - in - let initstate = - "let initial_regstate : regstate = struct { " ^ - (String.concat ", " (List.map initreg registers)) ^ - " }" - in - regstate :: (if !Initial_check.opt_undefined_gen then [initstate] else []) + ["struct regstate = { " ^ (String.concat ", " (List.map reg registers)) ^ " }"] + +let generate_initial_regstate defs = + let registers = find_registers defs in + if registers = [] then [] else + try + (* Recursively choose a default value for every type in the spec. + vals, constructed below, maps user-defined types to default values. *) + let rec lookup_init_val vals (Typ_aux (typ_aux, _) as typ) = + match typ_aux with + | Typ_id id -> + if string_of_id id = "bool" then "false" else + if string_of_id id = "bit" then "bitzero" else + if string_of_id id = "int" then "0" else + if string_of_id id = "nat" then "0" else + if string_of_id id = "real" then "0" else + if string_of_id id = "string" then "\"\"" else + if string_of_id id = "unit" then "()" else + Bindings.find id vals [] + | Typ_app (id, _) when string_of_id id = "list" -> "[||]" + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]) when string_of_id id = "atom" -> + string_of_nexp nexp + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _); _]) when string_of_id id = "range" -> + string_of_nexp nexp + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ; + Typ_arg_aux (Typ_arg_typ etyp, _)]) + when string_of_id id = "vector" -> + (* Output a list of initial values of the vector elements, or a + literal binary zero value if this is a bitvector and the + environment has a default indexing order (required by the + typechecker for binary and hex literals) *) + let literal_bitvec = is_bit_typ etyp && has_default_order defs in + let init_elem = if literal_bitvec then "0" else lookup_init_val vals etyp in + let rec elems len = + if (Nat_big_num.less_equal len Nat_big_num.zero) then [] else + init_elem :: elems (Nat_big_num.pred len) + in + if literal_bitvec then "0b" ^ (String.concat "" (elems len)) else + "[" ^ (String.concat ", " (elems len)) ^ "]" + | Typ_app (id, args) -> Bindings.find id vals args + | Typ_tup typs -> + "(" ^ (String.concat ", " (List.map (lookup_init_val vals) typs)) ^ ")" + | Typ_exist (_, _, typ) -> lookup_init_val vals typ + | _ -> raise Not_found + in + (* Helper functions to instantiate type arguments *) + let typ_subst_targ kid (Typ_arg_aux (arg, _)) typ = match arg with + | Typ_arg_nexp (Nexp_aux (nexp, _)) -> typ_subst_nexp kid nexp typ + | Typ_arg_typ (Typ_aux (typ', _)) -> typ_subst_typ kid typ' typ + | Typ_arg_order (Ord_aux (ord, _)) -> typ_subst_order kid ord typ + in + let typ_subst_quant_item typ (QI_aux (qi, _)) arg = match qi with + | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) -> + typ_subst_targ kid arg typ + | _ -> typ + in + 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 + | TD_enum (id, _, id1 :: _, _) -> + (* Choose the first value of an enumeration type as default *) + 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 + | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (tq, typ), _)) -> + let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in + Bindings.add id init_val vals + | TD_record (id, _, tq, fields, _) -> + let init_val args = + let init_field (typ, id) = + let typ = typ_subst_typquant tq args typ in + string_of_id id ^ " = " ^ lookup_init_val vals typ + in + "struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }" + in + Bindings.add id init_val vals + | TD_bitfield (id, typ, _) -> + Bindings.add id (fun _ -> lookup_init_val vals typ) vals + | _ -> 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 + in + let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in + ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"] + with + | _ -> [] (* Do not generate an initial register state if anything goes wrong *) let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with | Typ_id id -> id @@ -135,9 +222,8 @@ let generate_regval_typ typs = (String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^ " }"] -let add_regval_conv id typ defs = +let add_regval_conv id typ (Defs defs) = let id = string_of_id id in - let is_defined name = IdSet.mem (mk_id name) (ids_of_defs defs) in let typ_str = to_string (doc_typ typ) in (* Create a function that converts from regval to the target type. *) let from_name = id ^ "_of_regval" in @@ -146,14 +232,14 @@ let add_regval_conv id typ defs = Printf.sprintf "function %s Regval_%s(v) = Some(v)" from_name id; Printf.sprintf "and %s _ = None()" from_name ] in - let from_defs = if is_defined from_name then [] else [from_val; from_function] in + let from_defs = if is_defined defs from_name then [] else [from_val; from_function] in (* Create a function that converts from target type to regval. *) let to_name = "regval_of_" ^ id in let to_val = Printf.sprintf "val %s : %s -> register_value" to_name typ_str in let to_function = Printf.sprintf "function %s v = Regval_%s(v)" to_name id in - let to_defs = if is_defined to_name then [] else [to_val; to_function] in + let to_defs = if is_defined defs to_name then [] else [to_val; to_function] in let cdefs = concat_ast (List.map defs_of_string (from_defs @ to_defs)) in - append_ast defs cdefs + append_ast (Defs defs) cdefs let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with | Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) -> @@ -393,17 +479,16 @@ let generate_regstate_defs mwords defs = let gen_undef = !Initial_check.opt_undefined_gen in Initial_check.opt_undefined_gen := false; let registers = find_registers defs in - let def_ids = ids_of_defs (Defs defs) in - let has_def name = IdSet.mem (mk_id name) def_ids in let regtyps = register_base_types mwords (List.map fst registers) in let option_typ = - if has_def "option" then [] else + if is_defined defs "option" then [] else ["union option ('a : Type) = {None : unit, Some : 'a}"] in - let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in - let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in + let regval_typ = if is_defined defs "register_value" then [] else generate_regval_typ regtyps in + let regstate_typ = if is_defined defs "regstate" then [] else generate_regstate registers in + let initregstate = if is_defined defs "initial_regstate" then [] else generate_initial_regstate defs in let defs = - option_typ @ regval_typ @ regstate_typ + option_typ @ regval_typ @ regstate_typ @ initregstate |> List.map defs_of_string |> concat_ast |> Bindings.fold add_regval_conv regtyps diff --git a/src/type_check.mli b/src/type_check.mli index ed240839..a5d38363 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -283,6 +283,9 @@ val string_of_uvar : uvar -> string val subst_unifiers : uvar KBindings.t -> typ -> typ +val typ_subst_nexp : kid -> nexp_aux -> typ -> typ +val typ_subst_typ : kid -> typ_aux -> typ -> typ +val typ_subst_order : kid -> order_aux -> typ -> typ val typ_subst_kid : kid -> kid -> typ -> typ val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constraint option -- cgit v1.2.3 From c3f3642dfa5647685ae3dea86beeef8abc27f026 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 4 May 2018 17:44:07 +0100 Subject: Support short-circuiting of Boolean expressions in Lem --- src/gen_lib/prompt.lem | 6 +++++ src/pretty_print_lem.ml | 63 +++++++++++++++++++++++-------------------------- src/rewrites.ml | 10 +++++++- 3 files changed, 45 insertions(+), 34 deletions(-) (limited to 'src') diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index de683047..830f2350 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -38,6 +38,12 @@ end declare {isabelle} termination_argument foreachM = automatic +val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e +let and_boolM l r = l >>= (fun l -> if l then r else return false) + +val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e +let or_boolM l r = l >>= (fun l -> if l then return true else r) + val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e let bool_of_bitU_fail = function | B0 -> return false diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index f58c3fa6..f6b2fa87 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -551,10 +551,11 @@ let doc_exp_lem, doc_let_lem = let expY = top_exp ctxt true in let expN = top_exp ctxt false in let expV = top_exp ctxt in + let wrap_parens doc = if aexp_needed then parens (doc) else doc in let liftR doc = if ctxt.early_ret && effectful (effect_of full_exp) - then separate space [string "liftR"; parens (doc)] - else doc in + then wrap_parens (separate space [string "liftR"; parens (doc)]) + else wrap_parens doc in match e with | E_assign((LEXP_aux(le_act,tannot) as le), e) -> (* can only be register writes *) @@ -619,20 +620,21 @@ let doc_exp_lem, doc_let_lem = raise (Reporting_basic.err_unreachable l "E_vector_append should have been rewritten before pretty-printing") | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re) - | E_if(c,t,e) -> - let epp = if_exp ctxt false c t e in - if aexp_needed then parens (align epp) else epp + | E_if(c,t,e) -> wrap_parens (align (if_exp ctxt false c t e)) | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> raise (report l "E_for should have been rewritten before pretty-printing") | E_loop _ -> raise (report l "E_loop should have been rewritten before pretty-printing") | E_let(leb,e) -> - let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in - if aexp_needed then parens epp else epp + wrap_parens (let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e) | E_app(f,args) -> begin match f with - (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_lem_ctor none + | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) + when effectful (effect_of full_exp) -> + let call = doc_id_lem (append_id f "M") in + wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args))) + (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "foreach", _) -> begin match args with @@ -743,7 +745,7 @@ let doc_exp_lem, doc_let_lem = | _ -> doc_id_lem_ctor f ^^ space ^^ parens (separate_map comma (expV false) args) in - if aexp_needed then parens (align epp) else epp + wrap_parens (align epp) | _ -> let call, is_extern = match annot with | Some (env, _, _) when Env.is_extern f env "lem" -> @@ -796,8 +798,7 @@ let doc_exp_lem, doc_let_lem = else if is_ctor env id then doc_id_lem_ctor id else doc_id_lem id | E_lit lit -> doc_lit_lem lit - | E_cast(typ,e) -> - expV aexp_needed e + | E_cast(typ,e) -> expV aexp_needed e | E_tuple exps -> parens (align (group (separate_map (comma ^^ break 1) expN exps))) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> @@ -807,10 +808,9 @@ let doc_exp_lem, doc_let_lem = (* when Env.is_record tid env -> *) tid | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in - let epp = anglebars (space ^^ (align (separate_map - (semi_sp ^^ break 1) - (doc_fexp ctxt recordtyp) fexps)) ^^ space) in - if aexp_needed then parens epp else epp + wrap_parens (anglebars (space ^^ (align (separate_map + (semi_sp ^^ break 1) + (doc_fexp ctxt recordtyp) fexps)) ^^ space)) | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> let recordtyp = match annot with | Some (env, Typ_aux (Typ_id tid,_), _) @@ -829,7 +829,7 @@ let doc_exp_lem, doc_let_lem = let start = match nexp_simp start with | Nexp_aux (Nexp_constant i, _) -> Big_int.to_string i | _ -> if dir then "0" else string_of_int (List.length exps) in - let expspp = + (* let expspp = match exps with | [] -> empty | e :: es -> @@ -840,7 +840,8 @@ let doc_exp_lem, doc_let_lem = expN e), if count = 20 then 0 else count + 1) (expN e,0) es in - align (group expspp) in + align (group expspp) in *) + let expspp = align (group (flow_map (semi ^^ break 0) expN exps)) in let epp = brackets expspp in let (epp,aexp_needed) = if is_bit_typ etyp && !opt_mwords then @@ -858,28 +859,24 @@ let doc_exp_lem, doc_let_lem = brackets (separate_map semi (expN) exps) | E_case(e,pexps) -> let only_integers e = expY e in - let epp = - group ((separate space [string "match"; only_integers e; string "with"]) ^/^ - (separate_map (break 1) (doc_case ctxt) pexps) ^/^ - (string "end")) in - if aexp_needed then parens (align epp) else align epp + wrap_parens + (group ((separate space [string "match"; only_integers e; string "with"]) ^/^ + (separate_map (break 1) (doc_case ctxt) pexps) ^/^ + (string "end"))) | E_try (e, pexps) -> if effectful (effect_of e) then let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in - let epp = - group ((separate space [string try_catch; expY e; string "(function "]) ^/^ - (separate_map (break 1) (doc_case ctxt) pexps) ^/^ - (string "end)")) in - if aexp_needed then parens (align epp) else align epp + wrap_parens + (group ((separate space [string try_catch; expY e; string "(function "]) ^/^ + (separate_map (break 1) (doc_case ctxt) pexps) ^/^ + (string "end)"))) else raise (Reporting_basic.err_todo l "Warning: try-block around pure expression") | E_throw e -> - let epp = liftR (separate space [string "throw"; expY e]) in - if aexp_needed then parens (align epp) else align epp + align (liftR (separate space [string "throw"; expY e])) | E_exit e -> liftR (separate space [string "exit"; expY e]) | E_assert (e1,e2) -> - let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in - if aexp_needed then parens (align epp) else align epp + align (liftR (separate space [string "assert_exp"; expY e1; expY e2])) | E_app_infix (e1,id,e2) -> raise (Reporting_basic.err_unreachable l "E_app_infix should have been rewritten before pretty-printing") @@ -905,9 +902,9 @@ let doc_exp_lem, doc_let_lem = in infix 0 1 middle (expV b e1) (expN e2) in - if aexp_needed then parens (align epp) else epp + wrap_parens (align epp) | E_internal_return (e1) -> - separate space [string "return"; expY e1] + wrap_parens (align (separate space [string "return"; expY e1])) | E_sizeof nexp -> (match nexp_simp nexp with | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem (L_aux (L_num i, l)) diff --git a/src/rewrites.ml b/src/rewrites.ml index 582901dc..e779b059 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2581,6 +2581,14 @@ let rewrite_defs_letbind_effects = | E_cast (typ,exp') -> n_exp_name exp' (fun exp' -> k (rewrap (E_cast (typ,exp')))) + | E_app (op_bool, [l; r]) + when string_of_id op_bool = "and_bool" || string_of_id op_bool = "or_bool" -> + (* Leave effectful operands of Boolean "and"/"or" in place to allow + short-circuiting. *) + let newreturn = effectful l || effectful r in + let l = n_exp_term newreturn l in + let r = n_exp_term newreturn r in + k (rewrap (E_app (op_bool, [l; r]))) | E_app (id,exps) -> n_exp_nameL exps (fun exps -> k (rewrap (E_app (id,exps)))) @@ -2967,7 +2975,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = (* after rewrite_defs_letbind_effects c has no variable updates *) let env = env_of_annot annot in let typ = typ_of e1 in - let eff = union_eff_exps [e1;e2] in + let eff = union_eff_exps [c;e1;e2] in let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats)) | E_case (e1,ps) -> -- cgit v1.2.3 From c6710bb09c1d492b4434f0b3b375750275b4d4b5 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 4 May 2018 17:46:10 +0100 Subject: Run ARM built-in tests for Lem backend (via OCaml) --- src/gen_lib/sail_operators.lem | 12 ++++++++++++ src/gen_lib/sail_operators_bitlists.lem | 17 +++++++++++++++++ src/gen_lib/sail_operators_mwords.lem | 17 +++++++++++++++++ 3 files changed, 46 insertions(+) (limited to 'src') diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index d4275c87..78aab65e 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -223,3 +223,15 @@ let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedInteger val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r) + +val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a +let get_slice_int_bv len n lo = + let hi = lo + len - 1 in + let bs = bools_of_int (hi + 1) n in + of_bools (subrange_list false bs hi lo) + +val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer +let set_slice_int_bv len n lo v = + let hi = lo + len - 1 in + let bs = bits_of_int (hi + 1) n in + maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v))) diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index b0a29b5e..fed293b4 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -35,6 +35,9 @@ let zero_extend bits len = extz_bits len bits val sign_extend : list bitU -> integer -> list bitU let sign_extend bits len = exts_bits len bits +val zeros : integer -> list bitU +let zeros len = repeat [B0] len + val vector_truncate : list bitU -> integer -> list bitU let vector_truncate bs len = extz_bv len bs @@ -289,6 +292,20 @@ let duplicate_oracle b n = val reverse_endianness : list bitU -> list bitU let reverse_endianness v = reverse_endianness_list v +val get_slice_int : integer -> integer -> integer -> list bitU +let get_slice_int = get_slice_int_bv + +val set_slice_int : integer -> integer -> integer -> list bitU -> integer +let set_slice_int = set_slice_int_bv + +val slice : list bitU -> integer -> integer -> list bitU +let slice v lo len = + subrange_vec_dec v (lo + len - 1) lo + +val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU +let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v = + update_subrange_vec_dec out (n + slice_len - 1) n v + val eq_vec : list bitU -> list bitU -> bool val neq_vec : list bitU -> list bitU -> bool val ult_vec : list bitU -> list bitU -> bool diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 8bcc0319..077dfb02 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -76,6 +76,9 @@ let zero_extend w _ = Machine_word.zeroExtend w val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b let sign_extend w _ = Machine_word.signExtend w +val zeros : forall 'a. Size 'a => integer -> mword 'a +let zeros _ = Machine_word.wordFromNatural 0 + val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b let vector_truncate w _ = Machine_word.zeroExtend w @@ -310,6 +313,20 @@ let duplicate b n = maybe_failwith (duplicate_maybe b n) val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v)) +val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a +let get_slice_int = get_slice_int_bv + +val set_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer +let set_slice_int = set_slice_int_bv + +val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b +let slice v lo len = + subrange_vec_dec v (lo + len - 1) lo + +val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a +let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v = + update_subrange_vec_dec out (n + slice_len - 1) n v + val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -- cgit v1.2.3 From b6b46102fc49eae53c27d5d6540d41981c75da0c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 8 May 2018 18:13:03 +0100 Subject: Add more annotations for loop bounds in Lem rewriting Typechecking for-loops failed after the Lem rewriting passes in some cases: if the lower bound for the loop may be greater than the upper bound, the loop variable's type might be empty, and it cannot be initialised. This patch adds a guard "lower <= upper" around the loop body, and removes it again during pretty-printing. --- src/pretty_print_lem.ml | 14 ++++++++------ src/rewrites.ml | 43 +++++++++++++++++++++++++++++++++++-------- 2 files changed, 43 insertions(+), 14 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index f6b2fa87..c181249d 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -640,12 +640,14 @@ let doc_exp_lem, doc_let_lem = match args with | [exp1; exp2; exp3; ord_exp; vartuple; body] -> let loopvar, body = match body with - | E_aux (E_let (LB_aux (LB_val ( - P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body - | E_aux (E_let (LB_aux (LB_val ( - P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body - | E_aux (E_let (LB_aux (LB_val ( - P_aux (P_id id, _), _), _), body), _) -> id, body + | E_aux (E_let (LB_aux (LB_val (_, _), _), + E_aux (E_let (LB_aux (LB_val (_, _), _), + E_aux (E_if (_, + E_aux (E_let (LB_aux (LB_val ( + ((P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _)) + | (P_aux (P_var (P_aux (P_id id, _), _), _)) + | (P_aux (P_id id, _))), _), _), + body), _), _), _)), _)), _) -> id, body | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in let step = match ord_exp with | E_aux (E_lit (L_aux (L_false, _)), _) -> diff --git a/src/rewrites.ml b/src/rewrites.ml index e779b059..b59a248e 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2924,20 +2924,21 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = |> mk_var_exps_pats pl env in let exp4 = rewrite_var_updates (add_vars overwrite exp4 vars) in - let ord_exp, kids, constr, lower, upper = - match destruct_range env (typ_of exp1), destruct_range env (typ_of exp2) with + let ord_exp, kids, constr, lower, upper, lower_exp, upper_exp = + match destruct_numeric env (typ_of exp1), destruct_numeric env (typ_of exp2) with | None, _ | _, None -> raise (Reporting_basic.err_unreachable el "Could not determine loop bounds") - | Some (kids1, constr1, l1, u1), Some (kids2, constr2, l2, u2) -> + | Some (kids1, constr1, n1), Some (kids2, constr2, n2) -> let kids = kids1 @ kids2 in let constr = nc_and constr1 constr2 in - let ord_exp, lower, upper = + let ord_exp, lower, upper, lower_exp, upper_exp = if is_order_inc order - then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, l1, u2) - else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, l2, u1) + then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, n1, n2, exp1, exp2) + else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, n2, n1, exp2, exp1) in - ord_exp, kids, constr, lower, upper + ord_exp, kids, constr, lower, upper, lower_exp, upper_exp in + (* Bind the loop variable in the body, annotated with constraints *) let lvar_kid = mk_kid ("loop_" ^ string_of_id id) in let lvar_nc = nc_and constr (nc_and (nc_lteq lower (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) upper)) in let lvar_typ = mk_typ (Typ_exist (lvar_kid :: kids, lvar_nc, atom_typ (nvar lvar_kid))) in @@ -2946,7 +2947,33 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ)) in let lb = fix_eff_lb (annot_letbind (lvar_pat, exp1) el env lvar_typ) in let body = fix_eff_exp (annot_exp (E_let (lb, exp4)) el env (typ_of exp4)) in - let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; body])) el env (typ_of body)) in + (* If lower > upper, the loop body never gets executed, and the type + checker might not be able to prove that the initial value exp1 + satisfies the constraints on the loop variable. + + Make this explicit by guarding the loop body with lower <= upper. + (for type-checking; the guard is later removed again by the Lem + pretty-printer). This could be implemented with an assertion, but + that would force the loop to be effectful, so we use an if-expression + instead. This code assumes that the loop bounds have (possibly + existential) atom types, and the loop body has type unit. *) + let lower_kid = mk_kid ("loop_" ^ string_of_id id ^ "_lower") in + let lower_pat = P_var (annot_pat P_wild el env (typ_of lower_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var lower_kid)]))) in + let lb_lower = annot_letbind (lower_pat, lower_exp) el env (typ_of lower_exp) in + let upper_kid = mk_kid ("loop_" ^ string_of_id id ^ "_upper") in + let upper_pat = P_var (annot_pat P_wild el env (typ_of upper_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var upper_kid)]))) in + let lb_upper = annot_letbind (upper_pat, upper_exp) el env (typ_of upper_exp) in + let guard = annot_exp (E_constraint (nc_lteq (nvar lower_kid) (nvar upper_kid))) el env bool_typ in + let unit_exp = annot_exp (E_lit (mk_lit L_unit)) el env unit_typ in + let skip_val = tuple_exp (if overwrite then vars else unit_exp :: vars) in + let guarded_body = + fix_eff_exp (annot_exp (E_let (lb_lower, + fix_eff_exp (annot_exp (E_let (lb_upper, + fix_eff_exp (annot_exp (E_if (guard, body, skip_val)) + el env (typ_of exp4)))) + el env (typ_of exp4)))) + el env (typ_of exp4)) in + let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body])) el env (typ_of body)) in Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats)) | E_loop(loop,cond,body) -> let vars, varpats = -- cgit v1.2.3 From 972d349919fc5ebe911604330ea3c80e70fdcfad Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 8 May 2018 18:48:18 +0100 Subject: Add tests for Isabelle->OCaml generation for CHERI and AArch64 --- src/gen_lib/state_monad.lem | 13 +++++++++++++ src/type_check.mli | 2 ++ 2 files changed, 15 insertions(+) (limited to 'src') diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index 8253b800..a2919762 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -265,3 +265,16 @@ let update_reg_field_bit regfield i reg_val bit = let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in regfield.set_field reg_val new_field_value let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*) + +(* TODO Add Show typeclass for value and exception type *) +val show_result : forall 'a 'e. result 'a 'e -> string +let show_result = function + | Value _ -> "Value ()" + | Ex (Failure msg) -> "Failure " ^ msg + | Ex (Throw _) -> "Throw" +end + +val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit +let prerr_results rs = + let _ = Set.map (fun (r, _) -> let _ = prerr_endline (show_result r) in ()) rs in + () diff --git a/src/type_check.mli b/src/type_check.mli index a5d38363..1c0e2f09 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -271,6 +271,8 @@ val destruct_exist : Env.t -> typ -> (kid list * n_constraint * typ) option val destruct_range : Env.t -> typ -> (kid list * n_constraint * nexp * nexp) option +val destruct_numeric : Env.t -> typ -> (kid list * n_constraint * nexp) option + val destruct_vector : Env.t -> typ -> (nexp * order * typ) option type uvar = -- cgit v1.2.3 From c498c8a7f8d448dcefd1692e7562878cc6feb62b Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 9 May 2018 16:51:17 +0100 Subject: Fix printing of hex strings in Lem --- src/gen_lib/sail_values.lem | 1 + 1 file changed, 1 insertion(+) (limited to 'src') diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 2d9eda9c..5c6dc593 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -414,6 +414,7 @@ let rec hexstring_of_bits bs = match bs with | (Just n, Just s) -> Just (n :: s) | _ -> Nothing end + | [] -> Just [] | _ -> Nothing end declare {isabelle} termination_argument hexstring_of_bits = automatic -- cgit v1.2.3 From 0d56f6be9e2e437c570da05b1c8cdc25eb24912c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 9 May 2018 16:55:58 +0100 Subject: Fix an issue with C compilation --- src/c_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index 5cf282f9..23a8c92e 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -1927,7 +1927,7 @@ and compile_block ctx = function let setup, _, call, cleanup = compile_aexp ctx exp in let rest = compile_block ctx exps in let gs = gensym () in - setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup @ rest + iblock (setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup) :: rest (** Compile a sail type definition into a IR one. Most of the actual work of translating the typedefs into C is done by the code -- cgit v1.2.3 From 9efeea3c2179a182feb07c6b4e640674f149331f Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 2 May 2018 10:31:00 +0100 Subject: Add language=sail option in listings command for latex output. This helps with documents containing listings in multiple languages. --- src/latex.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index 01cf55b2..f16dddd8 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -134,7 +134,7 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l)); close_out oc; - string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting{%s/%s_sail.tex}}" dir cmd) + string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s_sail.tex}}" dir cmd) end let latex_command_id ?prefix:(prefix="") dir id no_loc annot = -- cgit v1.2.3