diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 1 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/isail.ml | 16 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 4 | ||||
| -rw-r--r-- | src/rewrites.ml | 4 | ||||
| -rw-r--r-- | src/specialize.ml | 86 | ||||
| -rw-r--r-- | src/type_check.ml | 50 |
7 files changed, 144 insertions, 18 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index fdd20050..074376a9 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -267,6 +267,7 @@ let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown) let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown) let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown) let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown) +let napp id args = Nexp_aux (Nexp_app (id, args), Parse_ast.Unknown) let nc_set kid nums = mk_nc (NC_set (kid, nums)) let nc_int_set kid ints = mk_nc (NC_set (kid, List.map Big_int.of_int ints)) diff --git a/src/ast_util.mli b/src/ast_util.mli index 69bd5a52..ec12d44b 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -127,6 +127,7 @@ val nsum : nexp -> nexp -> nexp val ntimes : nexp -> nexp -> nexp val npow2 : nexp -> nexp val nvar : kid -> nexp +val napp : id -> nexp list -> nexp val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *) (* Numeric constraint builders *) diff --git a/src/isail.ml b/src/isail.ml index 31e62fb5..629bf35a 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -250,6 +250,22 @@ let handle_input' input = ":(c)ommand can be called as either :c or :command." ] in List.iter print_endline commands + | ":poly" -> + let is_kopt = match arg with + | "Int" -> is_nat_kopt + | "Type" -> is_typ_kopt + | "Order" -> is_order_kopt + | _ -> failwith "Invalid kind" + in + let ids = Specialize.polymorphic_functions is_kopt !interactive_ast in + List.iter (fun id -> print_endline (string_of_id id)) (IdSet.elements ids) + | ":ins" -> + let id = mk_id arg in + let instantiations = Specialize.instantiations_of id !interactive_ast in + let print_instantiation i = + print_endline (Util.string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ Type_check.string_of_uvar uvar) (KBindings.bindings i)) + in + List.iter print_instantiation instantiations | ":output" -> let chan = open_out arg in Value.output_redirect chan diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 887b15a0..43be7a00 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -74,6 +74,10 @@ let rec doc_nexp = let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) = match n_aux with | Nexp_constant c -> string (Big_int.to_string c) + | Nexp_app (id, nexps) -> string (string_of_nexp nexp) + (* This segfaults??!!!! + doc_id id ^^ (parens (separate_map (comma ^^ space) doc_nexp nexps)) + *) | Nexp_id id -> doc_id id | Nexp_var kid -> doc_kid kid | _ -> parens (nexp0 nexp) diff --git a/src/rewrites.ml b/src/rewrites.ml index e14ced08..e4ac71cd 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -515,8 +515,8 @@ let rewrite_sizeof (Defs defs) = let (params_map, defs) = List.fold_left rewrite_sizeof_def (Bindings.empty, []) defs in let defs = List.map (rewrite_sizeof_valspec params_map) defs in - Defs defs -(* fst (check initial_env (Defs defs)) *) + (* Defs defs *) + fst (check initial_env (Defs defs)) let rewrite_defs_remove_assert defs = let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with diff --git a/src/specialize.ml b/src/specialize.ml new file mode 100644 index 00000000..881881f4 --- /dev/null +++ b/src/specialize.ml @@ -0,0 +1,86 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Rewriter + +(* Returns an IdSet with the function ids that have X-kinded + parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first + argument specifies what X should be - it should be one of: + is_nat_kopt, is_order_kopt, or is_type_kopt from Ast_util. +*) +let rec polymorphic_functions is_kopt (Defs defs) = + match defs with + | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, _, externs), _)) :: defs -> + let is_type_polymorphic = List.exists is_kopt (quant_kopts typq) in + if is_type_polymorphic then + IdSet.add id (polymorphic_functions is_kopt (Defs defs)) + else + polymorphic_functions is_kopt (Defs defs) + | _ :: defs -> polymorphic_functions is_kopt (Defs defs) + | [] -> IdSet.empty + +(* Returns a list of all the instantiations of a function id in an + ast. *) +let rec instantiations_of id ast = + let instantiations = ref [] in + + let inspect_exp = function + | E_aux (E_app (id', _), _) as exp when Id.compare id id' = 0 -> + instantiations := Type_check.instantiation_of exp :: !instantiations; + exp + | exp -> exp + in + + let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in + let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast in + + !instantiations diff --git a/src/type_check.ml b/src/type_check.ml index 3353daf4..30334783 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -343,6 +343,7 @@ module Env : sig val base_typ_of : t -> typ -> typ val add_smt_op : id -> string -> t -> t val get_smt_op : id -> t -> string + val have_smt_op : id -> t -> bool (* Well formedness-checks *) val wf_typ : ?exs:KidSet.t -> t -> typ -> unit val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit @@ -466,6 +467,9 @@ end = struct try Bindings.find id env.smt_ops with | Not_found -> first_smt_op (get_overloads id env) + let have_smt_op id env = + try ignore(get_smt_op id env); true with Type_error _ -> false + let rec infer_kind env id = if Bindings.mem id builtin_typs then Bindings.find id builtin_typs @@ -1336,15 +1340,27 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne else if KidSet.is_empty (nexp_frees n1a) then unify_nexps l env goals n1b (nminus nexp2 n1a) - else unify_error l ("Both sides of Nat expression " ^ string_of_nexp nexp1 + else unify_error l ("Both sides of Int expression " ^ string_of_nexp nexp1 ^ " contain free type variables so it cannot be unified with " ^ string_of_nexp nexp2) | Nexp_minus (n1a, n1b) -> if KidSet.is_empty (nexp_frees n1b) then unify_nexps l env goals n1a (nsum nexp2 n1b) - else unify_error l ("Cannot unify minus Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) + else unify_error l ("Cannot unify minus Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) | Nexp_times (n1a, n1b) -> - if KidSet.is_empty (nexp_frees n1a) - then + (* If we have SMT operations div and mod, then we can use the + property that + + mod(m, C) = 0 && C != 0 --> (C * n = m <--> n = m / C) + + to help us unify multiplications. *) + if Env.have_smt_op (mk_id "div") env && Env.have_smt_op (mk_id "mod") env then + let valid n c = prove env (nc_eq (napp (mk_id "mod") [n; c]) (nint 0)) && prove env (nc_neq c (nint 0)) in + if KidSet.is_empty (nexp_frees n1b) && valid nexp2 n1b then + unify_nexps l env goals n1a (napp (mk_id "div") [nexp2; n1b]) + else if KidSet.is_empty (nexp_frees n1a) && valid nexp2 n1a then + unify_nexps l env goals n1b (napp (mk_id "div") [nexp2; n1a]) + else unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) + else if KidSet.is_empty (nexp_frees n1a) then begin match nexp_aux2 with | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1a, n2a), Parse_ast.Unknown)) -> @@ -1354,20 +1370,19 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne match n1a with | Nexp_aux (Nexp_constant c1,_) when Big_int.equal (Big_int.modulus c2 c1) Big_int.zero -> unify_nexps l env goals n1b (mk_nexp (Nexp_constant (Big_int.div c2 c1))) - | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) + | _ -> unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) end - | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) + | _ -> unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) end - else if KidSet.is_empty (nexp_frees n1b) - then + else if KidSet.is_empty (nexp_frees n1b) then begin match nexp_aux2 with | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1b, n2b), Parse_ast.Unknown)) -> unify_nexps l env goals n1a n2a - | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) + | _ -> unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) end - else unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) - | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) + else unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) + | _ -> unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) let string_of_uvar = function | U_nexp n -> string_of_nexp n @@ -1415,6 +1430,9 @@ let merge_unifiers l kid uvar1 uvar2 = | None, None -> None let rec unify l env typ1 typ2 = + let typ1 = Env.expand_synonyms env typ1 in + let typ2 = Env.expand_synonyms env typ2 in + typ_print ("Unify " ^ string_of_typ typ1 ^ " with " ^ string_of_typ typ2); let goals = KidSet.inter (KidSet.diff (typ_frees typ1) (typ_frees typ2)) (typ_frees typ1) in let rec unify_typ l (Typ_aux (typ1_aux, _) as typ1) (Typ_aux (typ2_aux, _) as typ2) = @@ -1991,13 +2009,13 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | ((E_aux (E_assert (constr_exp, assert_msg), _) as exp) :: exps) -> let constr_exp = crule check_exp env constr_exp bool_typ in let checked_msg = crule check_exp env assert_msg string_typ in - let cexp, env = match assert_constraint env constr_exp with + let env = match assert_constraint env constr_exp with | Some nc -> typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert"); - annot_exp (E_constraint nc) bool_typ, Env.add_constraint nc env - | None -> - constr_exp, env in - let texp = annot_exp_effect (E_assert (cexp, checked_msg)) unit_typ (mk_effect [BE_escape]) in + Env.add_constraint nc env + | None -> env + in + let texp = annot_exp_effect (E_assert (constr_exp, checked_msg)) unit_typ (mk_effect [BE_escape]) in texp :: check_block l env exps typ | (exp :: exps) -> let texp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in |