From f73d601390a42a07a575db0c5efd5982471c2f2d Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 8 Jan 2018 16:35:08 +0000 Subject: Add some optional experimental rewrites to help with monomorphisation --- src/monomorphise.ml | 151 ++++++++++++++++++++++++++++++++++++++++++++++++++- src/process_file.ml | 8 ++- src/process_file.mli | 1 + src/sail.ml | 3 + 4 files changed, 159 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 0cbeda49..eef94982 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2460,11 +2460,156 @@ let argset_to_list splits = List.map argelt l end +module MonoRewrites = +struct + +let is_constant_range = function + | E_aux (E_lit _,_), E_aux (E_lit _,_) -> true + | _ -> false + +let is_constant = function + | E_aux (E_lit _,_) -> true + | _ -> false + +let is_constant_vec_typ env typ = + let typ = Env.base_typ_of env typ in + match destruct_vector env typ with + | Some (_,size,_,_) -> + (match nexp_simp size with + | Nexp_aux (Nexp_constant _,_) -> true + | _ -> false) + | _ -> false + +let is_id env id = + let ids = Env.get_overloads (Id_aux (id,Parse_ast.Unknown)) env in + let ids = id :: List.map (fun (Id_aux (id,_)) -> id) ids in + fun (Id_aux (x,_)) -> List.mem x ids + +(* We have to add casts in here with appropriate length information so that the + type checker knows the expected return types. *) -let monomorphise mwords auto debug_analysis splits env defs = +let rewrite_app env typ (id,args) = + let is_append = is_id env (Id "append") in + if is_append id then + let is_subrange = is_id env (Id "vector_subrange") in + let is_slice = is_id env (Id "slice") in + match args with + (* (known-size-vector @ variable-vector) @ variable-vector *) + | [E_aux (E_app (append, + [e1; + E_aux (E_app (subrange1, + [vector1; start1; end1]),_)]),_); + E_aux (E_app (subrange2, + [vector2; start2; end2]),_)] + when is_append append && is_subrange subrange1 && is_subrange subrange2 && + is_constant_vec_typ env (typ_of e1) && + not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> + let (start,size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in + let (_,size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in + let midsize = nminus size size1 in + let midstart = + if is_order_inc order + then nconstant zero_big_int + else nminus midsize (nconstant unit_big_int) in + let midtyp = vector_typ midstart midsize order bittyp in + E_app (append, + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "subrange_subrange_concat", + [vector1; start1; end1; vector2; start2; end2]), + (Unknown,None))),(Unknown,None))]) + + (* variable-range @ variable-range *) + | [E_aux (E_app (subrange1, + [vector1; start1; end1]),_); + E_aux (E_app (subrange2, + [vector2; start2; end2]),_)] + when is_subrange subrange1 && is_subrange subrange2 && + not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> + E_cast (typ, + E_aux (E_app (mk_id "subrange_subrange_concat", + [vector1; start1; end1; vector2; start2; end2]), + (Unknown,None))) + + (* variable-slice @ variable-slice *) + | [E_aux (E_app (slice1, + [vector1; start1; length1]),_); + E_aux (E_app (slice2, + [vector2; start2; length2]),_)] + when is_slice slice1 && is_slice slice2 && + not (is_constant length1 || is_constant length2) -> + E_cast (typ, + E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]),(Unknown,None))) + + | _ -> E_app (id,args) + + else if is_id env (Id "eq_vec") id then + (* variable-range == variable_range *) + let is_subrange = is_id env (Id "vector_subrange") in + match args with + | [E_aux (E_app (subrange1, + [vector1; start1; end1]),_); + E_aux (E_app (subrange2, + [vector2; start2; end2]),_)] + when is_subrange subrange1 && is_subrange subrange2 && + not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> + E_app (mk_id "subrange_subrange_eq", + [vector1; start1; end1; vector2; start2; end2]) + | _ -> E_app (id,args) + + else if is_id env (Id "IsZero") id then + match args with + | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)] + when is_id env (Id "vector_subrange") subrange1 && + not (is_constant_range (start1,end1)) -> + E_app (mk_id "is_zero_subrange", + [vector1; start1; end1]) + | _ -> E_app (id,args) + + else if is_id env (Id "IsOnes") id then + match args with + | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)] + when is_id env (Id "vector_subrange") subrange1 && + not (is_constant_range (start1,end1)) -> + E_app (mk_id "is_ones_subrange", + [vector1; start1; end1]) + | _ -> E_app (id,args) + + else E_app (id,args) + +let rewrite_aux = function + | (E_app (id,args),((_,Some (env,ty,_)) as annot)) -> + E_aux (rewrite_app env ty (id,args),annot) + | exp,annot -> E_aux (exp,annot) + +let mono_rewrite defs = + let open Rewriter in + rewrite_defs_base + { rewriters_base with + rewrite_exp = fun _ -> fold_exp { id_exp_alg with e_aux = rewrite_aux } } + defs +end + +(* TODO: put in a proper mli for this stuff *) +type options = { + auto : bool; + debug_analysis : int; + rewrites : bool +} + +let monomorphise mwords opts splits env defs = + let (defs,env) = + if opts.rewrites then + let defs = MonoRewrites.mono_rewrite defs in + (* TODO: is this necessary? *) + Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs + else (defs,env) + in +(*let _ = Pretty_print.pp_defs stdout defs in*) let new_splits = - if auto - then Analysis.argset_to_list (Analysis.analyse_defs debug_analysis env defs) + if opts.auto + then Analysis.argset_to_list (Analysis.analyse_defs opts.debug_analysis env defs) else [] in let defs = split_defs (new_splits@splits) defs in (* TODO: currently doing this because constant propagation leaves numeric literals as diff --git a/src/process_file.ml b/src/process_file.ml index 83cfd8a3..127a5aee 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -126,9 +126,15 @@ let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.E let opt_ddump_raw_mono_ast = ref false let opt_dmono_analysis = ref 0 let opt_auto_mono = ref false +let opt_mono_rewrites = ref false let monomorphise_ast locs type_env ast = - let ast = Monomorphise.monomorphise (!Pretty_print_lem.opt_mwords) (!opt_auto_mono) (!opt_dmono_analysis) + let open Monomorphise in + let opts = { + auto = !opt_auto_mono; + debug_analysis = !opt_dmono_analysis; + rewrites = !opt_mono_rewrites } in + let ast = monomorphise (!Pretty_print_lem.opt_mwords) opts locs type_env ast in let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in let ienv = Type_check.Env.no_casts Type_check.initial_env in diff --git a/src/process_file.mli b/src/process_file.mli index 88c9b9fb..10510e5c 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -70,6 +70,7 @@ val opt_dno_cast : bool ref val opt_ddump_raw_mono_ast : bool ref val opt_dmono_analysis : int ref val opt_auto_mono : bool ref +val opt_mono_rewrites : bool ref type out_type = | Lem_ast_out diff --git a/src/sail.ml b/src/sail.ml index 9bb7cfcb..1a0f6282 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -132,6 +132,9 @@ let options = Arg.align ([ ( "-auto_mono", Arg.Set opt_auto_mono, " automatically infer how to monomorphise code"); + ( "-mono_rewrites", + Arg.Set Process_file.opt_mono_rewrites, + " turn on rewrites for combining bitvector operations"); ( "-verbose", Arg.Set opt_print_verbose, " (debug) pretty-print the input to standard output"); -- cgit v1.2.3 From 35bfe5b1c08fb045283785c819bf0ec4fe24f1c0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 9 Jan 2018 11:33:04 +0000 Subject: Move reordering in alpha_equivalent before relabelling to give consistent names --- src/type_check.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index dee17fee..a4b4bb39 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1613,11 +1613,11 @@ let rec alpha_equivalent env typ1 typ2 = | Typ_fn (typ1, typ2, eff) -> Typ_fn (relabel typ1, relabel typ2, eff) | Typ_tup typs -> Typ_tup (List.map relabel typs) | Typ_exist (kids, nc, typ) -> + let (kids, _) = kid_order (KidSet.of_list kids) typ in let kids = List.map (fun kid -> (kid, new_kid ())) kids in let nc = List.fold_left (fun nc (kid, nk) -> nc_subst_nexp kid (Nexp_var nk) nc) nc kids in let typ = List.fold_left (fun nc (kid, nk) -> typ_subst_nexp kid (Nexp_var nk) nc) typ kids in let kids = List.map snd kids in - let (kids, _) = kid_order (KidSet.of_list kids) typ in Typ_exist (kids, nc, typ) | Typ_app (id, args) -> Typ_app (id, List.map relabel_arg args) -- cgit v1.2.3 From 8193c028274dccde0d4c972290cf2ca68d74a6eb Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 9 Jan 2018 14:50:32 +0000 Subject: Proper location for no set constraint errors --- src/monomorphise.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index eef94982..9ed5d799 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -221,7 +221,7 @@ let kidset_bigunion = function | h::t -> List.fold_left KidSet.union h t (* TODO: deal with non-set constraints, intersections, etc somehow *) -let extract_set_nc var (NC_aux (_,l) as nc) = +let extract_set_nc l var nc = let rec aux (NC_aux (nc,l)) = let re nc = NC_aux (nc,l) in match nc with @@ -351,7 +351,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) = let find_insts k (insts,nc) = let inst,nc' = if KidSet.mem k vars then - let is,nc' = extract_set_nc k nc in + let is,nc' = extract_set_nc l k nc in Some is,nc' else None,nc in (k,inst)::insts,nc' @@ -1257,7 +1257,7 @@ let split_defs splits defs = | Nexp_var kvar -> let ncs = Env.get_constraints env in let nc = List.fold_left nc_and nc_true ncs in - List.map mk_lit (fst (extract_set_nc kvar nc)) + List.map mk_lit (fst (extract_set_nc l kvar nc)) | _ -> cannot () end | _ -> cannot () -- cgit v1.2.3 From 9c01188e3630b03fd4142e1424250170fa7a65ff Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 9 Jan 2018 16:07:06 +0000 Subject: Tidy up monomorphisation interface --- src/monomorphise.ml | 8 +++---- src/monomorphise.mli | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++++ src/process_file.ml | 7 +++--- 3 files changed, 71 insertions(+), 7 deletions(-) create mode 100644 src/monomorphise.mli (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 9ed5d799..72db4c9d 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2591,14 +2591,14 @@ let mono_rewrite defs = defs end -(* TODO: put in a proper mli for this stuff *) type options = { auto : bool; debug_analysis : int; - rewrites : bool + rewrites : bool; + rewrite_size_parameters : bool } -let monomorphise mwords opts splits env defs = +let monomorphise opts splits env defs = let (defs,env) = if opts.rewrites then let defs = MonoRewrites.mono_rewrite defs in @@ -2615,7 +2615,7 @@ let monomorphise mwords opts splits env defs = (* TODO: currently doing this because constant propagation leaves numeric literals as int, try to avoid this later; also use final env for DEF_spec case above, because the type checker doesn't store the env at that point :( *) - if mwords then + if opts.rewrite_size_parameters then let (defs,env) = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in let defs = AtomToItself.rewrite_size_parameters env defs in defs diff --git a/src/monomorphise.mli b/src/monomorphise.mli new file mode 100644 index 00000000..39b4e244 --- /dev/null +++ b/src/monomorphise.mli @@ -0,0 +1,63 @@ +(**************************************************************************) +(* 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. *) +(**************************************************************************) + +type options = { + auto : bool; (* Analyse ast to find splits for monomorphisation *) + debug_analysis : int; (* Debug output level for the automatic analysis *) + rewrites : bool; (* Experimental rewrites for variable-sized operations *) + rewrite_size_parameters : bool (* Make implicit type parameters explicit for (e.g.) lem *) +} + +val monomorphise : + options -> + ((string * int) * string) list -> (* List of splits from the command line *) + Type_check.Env.t -> + Type_check.tannot Ast.defs -> + Type_check.tannot Ast.defs diff --git a/src/process_file.ml b/src/process_file.ml index 127a5aee..3755a83d 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -133,9 +133,10 @@ let monomorphise_ast locs type_env ast = let opts = { auto = !opt_auto_mono; debug_analysis = !opt_dmono_analysis; - rewrites = !opt_mono_rewrites } in - let ast = monomorphise (!Pretty_print_lem.opt_mwords) opts - locs type_env ast in + rewrites = !opt_mono_rewrites; + rewrite_size_parameters = !Pretty_print_lem.opt_mwords + } in + let ast = monomorphise opts locs type_env ast in let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in let ienv = Type_check.Env.no_casts Type_check.initial_env in Type_check.check ienv ast -- cgit v1.2.3 From c11d9865030a2c147fcb3ea3b1fd0a57d92fc30c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 9 Jan 2018 18:19:14 +0000 Subject: More monomorphisation rewrites for aarch64 --- src/monomorphise.ml | 89 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 89 insertions(+) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 72db4c9d..bfa29e6a 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -2493,6 +2493,7 @@ let rewrite_app env typ (id,args) = if is_append id then let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in + let is_zeros = is_id env (Id "Zeros") in match args with (* (known-size-vector @ variable-vector) @ variable-vector *) | [E_aux (E_app (append, @@ -2518,6 +2519,29 @@ let rewrite_app env typ (id,args) = E_aux (E_app (mk_id "subrange_subrange_concat", [vector1; start1; end1; vector2; start2; end2]), (Unknown,None))),(Unknown,None))]) + | [E_aux (E_app (append, + [e1; + E_aux (E_app (slice1, + [vector1; start1; length1]),_)]),_); + E_aux (E_app (slice2, + [vector2; start2; length2]),_)] + when is_append append && is_slice slice1 && is_slice slice2 && + is_constant_vec_typ env (typ_of e1) && + not (is_constant length1 || is_constant length2) -> + let (start,size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in + let (_,size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in + let midsize = nminus size size1 in + let midstart = + if is_order_inc order + then nconstant zero_big_int + else nminus midsize (nconstant unit_big_int) in + let midtyp = vector_typ midstart midsize order bittyp in + E_app (append, + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]), + (Unknown,None))),(Unknown,None))]) (* variable-range @ variable-range *) | [E_aux (E_app (subrange1, @@ -2542,6 +2566,29 @@ let rewrite_app env typ (id,args) = E_aux (E_app (mk_id "slice_slice_concat", [vector1; start1; length1; vector2; start2; length2]),(Unknown,None))) + | [E_aux (E_app (append1, + [e1; + E_aux (E_app (slice1, [vector1; start1; length1]),_)]),_); + E_aux (E_app (zeros1, [length2]),_)] + when is_append append1 && is_slice slice1 && is_zeros zeros1 && + is_constant_vec_typ env (typ_of e1) && + not (is_constant length1 || is_constant length2) -> + let (start,size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in + let (_,size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in + let midsize = nminus size size1 in + let midstart = + if is_order_inc order + then nconstant zero_big_int + else nminus midsize (nconstant unit_big_int) in + let midtyp = vector_typ midstart midsize order bittyp in + E_cast (typ, + E_aux (E_app (mk_id "append", + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "slice_zeros_concat", + [vector1; start1; length1; length2]),(Unknown,None))),(Unknown,None))]), + (Unknown,None))) + | _ -> E_app (id,args) else if is_id env (Id "eq_vec") id then @@ -2576,6 +2623,48 @@ let rewrite_app env typ (id,args) = [vector1; start1; end1]) | _ -> E_app (id,args) + else if is_id env (Id "Extend") id || is_id env (Id "ZeroExtend") id then + let is_subrange = is_id env (Id "vector_subrange") in + let is_slice = is_id env (Id "slice") in + let is_zeros = is_id env (Id "Zeros") in + match args with + | (E_aux (E_app (append1, + [E_aux (E_app (subrange1, [vector1; start1; end1]), _); + E_aux (E_app (zeros1, [len1]),_)]),_)):: + ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) + when is_subrange subrange1 && is_zeros zeros1 && is_append append1 + -> E_app (mk_id "place_subrange", + [vector1; start1; end1; len1]) + + | (E_aux (E_app (append1, + [E_aux (E_app (slice1, [vector1; start1; length1]), _); + E_aux (E_app (zeros1, [length2]),_)]),_)):: + ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) + when is_slice slice1 && is_zeros zeros1 && is_append append1 + -> E_app (mk_id "place_slice", + [vector1; start1; length1; length2]) + + (* If we've already rewritten to slice_slice_concat, we can just drop the + zero extension because it can do it *) + | (E_aux (E_cast (_, (E_aux (E_app (Id_aux (Id "slice_slice_concat",_), args),_))),_)):: + ([] | [_;E_aux (E_id (Id_aux (Id "unsigned",_)),_)]) + -> E_app (mk_id "slice_slice_concat", args) + + | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] + when is_slice slice1 && not (is_constant length1) -> + E_app (mk_id "zext_slice", [vector1; start1; length1]) + + | _ -> E_app (id,args) + + else if is_id env (Id "SignExtend") id then + let is_slice = is_id env (Id "slice") in + match args with + | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] + when is_slice slice1 && not (is_constant length1) -> + E_app (mk_id "sext_slice", [vector1; start1; length1]) + + | _ -> E_app (id,args) + else E_app (id,args) let rewrite_aux = function -- cgit v1.2.3 From 1d564c59924363e4c045f7dbfda8800c3901c42f Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 10 Jan 2018 15:23:12 +0000 Subject: Fix control dependencies in monomorphisation analysis --- src/monomorphise.ml | 62 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 38 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index bfa29e6a..6cea3f22 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1958,8 +1958,7 @@ let merge rs rs' = { type env = { var_deps : dependencies Bindings.t; - kid_deps : dependencies KBindings.t; - control_deps : dependencies + kid_deps : dependencies KBindings.t } let rec split3 = function @@ -1973,12 +1972,24 @@ let kids_bound_by_pat pat = fst (fold_pat ({ (compute_pat_alg KidSet.empty KidSet.union) with p_var = (fun ((s,p),kid) -> (KidSet.add kid s, P_var (p,kid))) }) pat) +(* Add bound variables from a pattern to the environment with the given dependency. *) + let update_env env deps pat = let bound = bindings_from_pat pat in let var_deps = List.fold_left (fun ds v -> Bindings.add v deps ds) env.var_deps bound in let kbound = kids_bound_by_pat pat in let kid_deps = KidSet.fold (fun v ds -> KBindings.add v deps ds) kbound env.kid_deps in - { env with var_deps = var_deps; kid_deps = kid_deps } + { var_deps = var_deps; kid_deps = kid_deps } + +let assigned_vars_exps es = + List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp)) + IdSet.empty es + +(* For adding control dependencies to mutable variables *) + +let add_dep_to_assigned dep assigns es = + let assigned = assigned_vars_exps es in + Bindings.mapi (fun id d -> if IdSet.mem id assigned then dmerge dep d else d) assigns (* Functions to give dependencies for type variables in nexps, constraints, types and unification variables. For function calls we also supply a list of dependencies for @@ -2041,9 +2052,7 @@ let deps_of_uvar kid_deps arg_deps = function let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let remove_assigns es message = - let assigned = - List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp)) - IdSet.empty es in + let assigned = assigned_vars_exps es in IdSet.fold (fun id asn -> Bindings.add id (Unknown (l, string_of_id id ^ message)) asn) @@ -2054,8 +2063,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let deps, _, rs = split3 (List.map (analyse_exp fn_id env assigns) es) in (deps, assigns, List.fold_left merge empty rs) in - let merge_deps deps = - List.fold_left dmerge env.control_deps deps in + let merge_deps deps = List.fold_left dmerge dempty deps in let deps, assigns, r = match e with | E_block es -> @@ -2074,18 +2082,18 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = | E_id id -> begin match Bindings.find id env.var_deps with - | args -> (dmerge env.control_deps args,assigns,empty) + | args -> (args,assigns,empty) | exception Not_found -> match Bindings.find id assigns with - | args -> (dmerge env.control_deps args,assigns,empty) + | args -> (args,assigns,empty) | exception Not_found -> match Env.lookup_id id (Type_check.env_of_annot (l,annot)) with - | Enum _ | Union _ -> env.control_deps,assigns,empty + | Enum _ | Union _ -> dempty,assigns,empty | Register _ -> Unknown (l, string_of_id id ^ " is a register"),assigns,empty | _ -> Unknown (l, string_of_id id ^ " is not in the environment"),assigns,empty end - | E_lit _ -> (env.control_deps,assigns,empty) + | E_lit _ -> (dempty,assigns,empty) | E_cast (_,e) -> analyse_exp fn_id env assigns e | E_app (id,args) -> let deps, assigns, r = non_det args in @@ -2117,23 +2125,23 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = (merge_deps deps, assigns, r) | E_if (e1,e2,e3) -> let d1,assigns,r1 = analyse_exp fn_id env assigns e1 in - let env' = { env with control_deps = dmerge env.control_deps d1 } in - let d2,a2,r2 = analyse_exp fn_id env' assigns e2 in - let d3,a3,r3 = analyse_exp fn_id env' assigns e3 in - (dmerge d2 d3, dep_bindings_merge a2 a3, merge r1 (merge r2 r3)) + let d2,a2,r2 = analyse_exp fn_id env assigns e2 in + let d3,a3,r3 = analyse_exp fn_id env assigns e3 in + let assigns = add_dep_to_assigned d1 (dep_bindings_merge a2 a3) [e2;e3] in + (dmerge d1 (dmerge d2 d3), assigns, merge r1 (merge r2 r3)) | E_loop (_,e1,e2) -> + (* We remove all of the variables assigned in the loop, so we don't + need to add control dependencies *) let assigns = remove_assigns [e1;e2] " assigned in a loop" in let d1,a1,r1 = analyse_exp fn_id env assigns e1 in - let env' = { env with control_deps = dmerge env.control_deps d1 } in - let d2,a2,r2 = analyse_exp fn_id env' assigns e2 in + let d2,a2,r2 = analyse_exp fn_id env assigns e2 in (dempty, assigns, merge r1 r2) | E_for (var,efrom,eto,eby,ord,body) -> let d1,assigns,r1 = non_det [efrom;eto;eby] in let assigns = remove_assigns [body] " assigned in a loop" in - let d = dmerge env.control_deps (merge_deps d1) in + let d = merge_deps d1 in let loop_kid = mk_kid ("loop_" ^ string_of_id var) in let env' = { env with - control_deps = d; kid_deps = KBindings.add loop_kid d env.kid_deps} in let d2,a2,r2 = analyse_exp fn_id env' assigns body in (dempty, assigns, merge r1 r2) @@ -2167,11 +2175,14 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = match pexp with | Pat_exp (pat,e1) -> let env = update_env env deps pat in - analyse_exp fn_id env assigns e1 + let d,assigns,r = analyse_exp fn_id env assigns e1 in + let assigns = add_dep_to_assigned deps assigns [e1] in + (d,assigns,r) | Pat_when (pat,e1,e2) -> let env = update_env env deps pat in let d1,assigns,r1 = analyse_exp fn_id env assigns e1 in let d2,assigns,r2 = analyse_exp fn_id env assigns e2 in + let assigns = add_dep_to_assigned deps assigns [e1;e2] in (dmerge d1 d2, assigns, merge r1 r2) in let ds,assigns,rs = split3 (List.map analyse_case cases) in @@ -2193,7 +2204,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = | E_exit e | E_throw e -> let _, _, r = analyse_exp fn_id env assigns e in - (Unknown (l,"non-local flow"), Bindings.empty, r) + (dempty, Bindings.empty, r) | E_try (e,cases) -> let deps,_,r = analyse_exp fn_id env assigns e in let assigns = remove_assigns [e] " assigned in try expression" in @@ -2201,11 +2212,14 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = match pexp with | Pat_exp (pat,e1) -> let env = update_env env (Unknown (l,"Exception")) pat in - analyse_exp fn_id env assigns e1 + let d,assigns,r = analyse_exp fn_id env assigns e1 in + let assigns = add_dep_to_assigned deps assigns [e1] in + (d,assigns,r) | Pat_when (pat,e1,e2) -> let env = update_env env (Unknown (l,"Exception")) pat in let d1,assigns,r1 = analyse_exp fn_id env assigns e1 in let d2,assigns,r2 = analyse_exp fn_id env assigns e2 in + let assigns = add_dep_to_assigned deps assigns [e1;e2] in (dmerge d1 d2, assigns, merge r1 r2) in let ds,assigns,rs = split3 (List.map analyse_handler cases) in @@ -2356,7 +2370,7 @@ let initial_env fn_id (TypQ_aux (tq,_)) pat = let _,var_deps,kid_deps = split3 (List.mapi arg pats) in let var_deps = List.fold_left dep_bindings_merge Bindings.empty var_deps in let kid_deps = List.fold_left dep_kbindings_merge kid_quant_deps kid_deps in - { var_deps = var_deps; kid_deps = kid_deps; control_deps = dempty } + { var_deps = var_deps; kid_deps = kid_deps } let print_result r = let _ = print_endline (" splits: " ^ string_of_argset r.split) in -- cgit v1.2.3 From 1603db2cf47b9cca42cfe8aaeedec43b347a5821 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 10 Jan 2018 16:29:39 +0000 Subject: Add an all_split_errors option --- src/monomorphise.ml | 45 ++++++++++++++++++++++++++------------------- src/monomorphise.mli | 9 +++++---- src/process_file.ml | 4 +++- src/process_file.mli | 1 + src/sail.ml | 3 +++ 5 files changed, 38 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 6cea3f22..ce67ecd1 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -784,7 +784,7 @@ let rec assigned_vars_in_lexp (LEXP_aux (le,_)) = IdSet.union (assigned_vars_in_lexp le) (IdSet.union (assigned_vars e1) (assigned_vars e2)) | LEXP_field (le,_) -> assigned_vars_in_lexp le -let split_defs splits defs = +let split_defs continue_anyway splits defs = let split_constructors (Defs defs) = let sc_type_union q (Tu_aux (tu,l) as tua) = match tu with @@ -1196,17 +1196,22 @@ let split_defs splits defs = (* Split a variable pattern into every possible value *) - let split var l annot = + let split var pat_l annot = let v = string_of_id var in - let env = Type_check.env_of_annot (l, annot) in - let typ = Type_check.typ_of_annot (l, annot) in + let env = Type_check.env_of_annot (pat_l, annot) in + let typ = Type_check.typ_of_annot (pat_l, annot) in let typ = Env.expand_synonyms env typ in let Typ_aux (ty,l) = typ in let new_l = Generated l in let renew_id (Id_aux (id,l)) = Id_aux (id,new_l) in - let cannot () = - raise (Reporting_basic.err_general l - ("Cannot split type " ^ string_of_typ typ ^ " for variable " ^ v)) + let cannot msg = + let open Reporting_basic in + let error = + Err_general (pat_l, + ("Cannot split type " ^ string_of_typ typ ^ " for variable " ^ v ^ ": " ^ msg)) + in if continue_anyway + then (print_error error; [P_aux (P_id var,(pat_l,annot)),[]]) + else raise (Fatal_error error) in match ty with | Typ_id (Id_aux (Id "bool",_)) -> @@ -1226,7 +1231,7 @@ let split_defs splits defs = P_aux (P_lit (L_aux (b,new_l)),(l,annot)), [var,E_aux (E_lit (L_aux (b,new_l)),(new_l, annot))]) [L_zero; L_one] - | _ -> cannot ()) + | _ -> cannot ("don't know about type " ^ string_of_id id)) | Typ_app (Id_aux (Id "vector",_), [_;Typ_arg_aux (Typ_arg_nexp len,_);_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> (match len with @@ -1237,15 +1242,13 @@ let split_defs splits defs = P_aux (P_lit lit,(l,annot)), [var,E_aux (E_lit lit,(new_l,annot))]) lits else - raise (Reporting_basic.err_general l - ("Refusing to split vector type of length " ^ string_of_big_int sz ^ - " above limit " ^ string_of_int vector_split_limit ^ - " for variable " ^ v)) + cannot ("Refusing to split vector type of length " ^ string_of_big_int sz ^ + " (above limit " ^ string_of_int vector_split_limit ^ ")") | _ -> - cannot () + cannot ("length not constant, " ^ string_of_nexp len) ) (* set constrained numbers *) - | Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp Nexp_aux (value,_),_)]) -> + | Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (value,_) as nexp),_)]) -> begin let mk_lit i = let lit = L_aux (L_num i,new_l) in @@ -1257,10 +1260,12 @@ let split_defs splits defs = | Nexp_var kvar -> let ncs = Env.get_constraints env in let nc = List.fold_left nc_and nc_true ncs in - List.map mk_lit (fst (extract_set_nc l kvar nc)) - | _ -> cannot () + (match extract_set_nc l kvar nc with + | (is,_) -> List.map mk_lit is + | exception Reporting_basic.Fatal_error (Reporting_basic.Err_general (_,msg)) -> cannot msg) + | _ -> cannot ("unsupport atom nexp " ^ string_of_nexp nexp) end - | _ -> cannot () + | _ -> cannot ("unsupported type " ^ string_of_typ typ) in @@ -2698,7 +2703,8 @@ type options = { auto : bool; debug_analysis : int; rewrites : bool; - rewrite_size_parameters : bool + rewrite_size_parameters : bool; + all_split_errors : bool } let monomorphise opts splits env defs = @@ -2714,7 +2720,8 @@ let monomorphise opts splits env defs = if opts.auto then Analysis.argset_to_list (Analysis.analyse_defs opts.debug_analysis env defs) else [] in - let defs = split_defs (new_splits@splits) defs in + let defs = split_defs opts.all_split_errors (new_splits@splits) defs in + (* TODO: stop if opts.all_split_errors && something went wrong *) (* TODO: currently doing this because constant propagation leaves numeric literals as int, try to avoid this later; also use final env for DEF_spec case above, because the type checker doesn't store the env at that point :( *) diff --git a/src/monomorphise.mli b/src/monomorphise.mli index 39b4e244..8e0c1ede 100644 --- a/src/monomorphise.mli +++ b/src/monomorphise.mli @@ -49,10 +49,11 @@ (**************************************************************************) type options = { - auto : bool; (* Analyse ast to find splits for monomorphisation *) - debug_analysis : int; (* Debug output level for the automatic analysis *) - rewrites : bool; (* Experimental rewrites for variable-sized operations *) - rewrite_size_parameters : bool (* Make implicit type parameters explicit for (e.g.) lem *) + auto : bool; (* Analyse ast to find splits for monomorphisation *) + debug_analysis : int; (* Debug output level for the automatic analysis *) + rewrites : bool; (* Experimental rewrites for variable-sized operations *) + rewrite_size_parameters : bool; (* Make implicit type parameters explicit for (e.g.) lem *) + all_split_errors : bool } val monomorphise : diff --git a/src/process_file.ml b/src/process_file.ml index 3755a83d..9b5cd9da 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -127,6 +127,7 @@ let opt_ddump_raw_mono_ast = ref false let opt_dmono_analysis = ref 0 let opt_auto_mono = ref false let opt_mono_rewrites = ref false +let opt_dall_split_errors = ref false let monomorphise_ast locs type_env ast = let open Monomorphise in @@ -134,7 +135,8 @@ let monomorphise_ast locs type_env ast = auto = !opt_auto_mono; debug_analysis = !opt_dmono_analysis; rewrites = !opt_mono_rewrites; - rewrite_size_parameters = !Pretty_print_lem.opt_mwords + rewrite_size_parameters = !Pretty_print_lem.opt_mwords; + all_split_errors = !opt_dall_split_errors } in let ast = monomorphise opts locs type_env ast in let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in diff --git a/src/process_file.mli b/src/process_file.mli index 10510e5c..53bb9606 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -71,6 +71,7 @@ val opt_ddump_raw_mono_ast : bool ref val opt_dmono_analysis : int ref val opt_auto_mono : bool ref val opt_mono_rewrites : bool ref +val opt_dall_split_errors : bool ref type out_type = | Lem_ast_out diff --git a/src/sail.ml b/src/sail.ml index 1a0f6282..c622b8ee 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -135,6 +135,9 @@ let options = Arg.align ([ ( "-mono_rewrites", Arg.Set Process_file.opt_mono_rewrites, " turn on rewrites for combining bitvector operations"); + ( "-dall_split_errors", + Arg.Set Process_file.opt_dall_split_errors, + " display all case split errors from monomorphisation, rather than one"); ( "-verbose", Arg.Set opt_print_verbose, " (debug) pretty-print the input to standard output"); -- cgit v1.2.3 From 6c3f6b7a8e8d5df984d73c9c12740e652f638f03 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 12 Jan 2018 11:15:56 +0000 Subject: Support constant propagation on casts in monomorphisation --- src/monomorphise.ml | 80 ++++++++++++++++++++++++++++++++++++++++------------- src/type_check.mli | 2 ++ 2 files changed, 63 insertions(+), 19 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index ce67ecd1..5ffe75d4 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -622,29 +622,69 @@ let lit_match = function (* There's no undefined nexp, so replace undefined sizes with a plausible size. 32 is used as a sensible default. *) + +let fabricate_nexp_exist env l typ kids nc typ' = + match kids,nc,Env.expand_synonyms env typ' with + | ([kid],NC_aux (NC_set (kid',i::_),_), + Typ_aux (Typ_app (Id_aux (Id "atom",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_)) + when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 -> + Nexp_aux (Nexp_constant i,Unknown) + | ([kid],NC_aux (NC_true,_), + Typ_aux (Typ_app (Id_aux (Id "atom",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_)) + when Kid.compare kid kid'' = 0 -> + nint 32 + | ([kid],NC_aux (NC_set (kid',i::_),_), + Typ_aux (Typ_app (Id_aux (Id "range",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_); + Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) + when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 && + Kid.compare kid kid''' = 0 -> + Nexp_aux (Nexp_constant i,Unknown) + | ([kid],NC_aux (NC_true,_), + Typ_aux (Typ_app (Id_aux (Id "range",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_); + Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) + when Kid.compare kid kid'' = 0 && + Kid.compare kid kid''' = 0 -> + nint 32 + | _ -> raise (Reporting_basic.err_general l + ("Undefined value at unsupported type " ^ string_of_typ typ)) + let fabricate_nexp l = function | None -> nint 32 | Some (env,typ,_) -> match Type_check.destruct_exist env typ with | None -> nint 32 - | Some (kids,nc,typ') -> - match kids,nc,Env.expand_synonyms env typ' with - | ([kid],NC_aux (NC_set (kid',i::_),_), - Typ_aux (Typ_app (Id_aux (Id "range",_), - [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_); - Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) - when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 && - Kid.compare kid kid''' = 0 -> - Nexp_aux (Nexp_constant i,Unknown) - | ([kid],NC_aux (NC_true,_), - Typ_aux (Typ_app (Id_aux (Id "range",_), - [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_); - Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) - when Kid.compare kid kid'' = 0 && - Kid.compare kid kid''' = 0 -> - nint 32 - | _ -> raise (Reporting_basic.err_general l - ("Undefined value at unsupported type " ^ string_of_typ typ)) + | Some (kids,nc,typ') -> fabricate_nexp_exist env l typ kids nc typ' + +let atom_typ_kid kid = function + | Typ_aux (Typ_app (Id_aux (Id "atom",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_) -> + Kid.compare kid kid' = 0 + | _ -> false + +(* We reduce casts in a few cases, in particular to ensure that where the + type checker has added a ({'n, true. atom('n)}) ex_int(...) cast we can + fill in the 'n. For undefined we fabricate a suitable value for 'n. *) + +let reduce_cast typ exp l annot = + let env = env_of_annot (l,annot) in + let typ' = Env.base_typ_of env typ in + match exp, destruct_exist env typ' with + | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' -> + let nc_env = Env.add_typ_var kid BK_nat env in + let nc_env = Env.add_constraint (nc_eq (nvar kid) (nconstant n)) nc_env in + if prove nc_env nc + then exp + else raise (Reporting_basic.err_unreachable l + ("Constant propagation error: literal " ^ string_of_big_int n ^ + " does not satisfy constraint " ^ string_of_n_constraint nc)) + | E_aux (E_lit (L_aux (L_undef,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' -> + let nexp = fabricate_nexp_exist env Unknown typ [kid] nc typ'' in + E_aux (E_cast (subst_src_typ (KBindings.singleton kid nexp) typ'', exp),(Generated l,None)) + | _ -> E_aux (E_cast (typ,exp),(l,annot)) (* Used for constant propagation in pattern matches *) type 'a matchresult = @@ -886,7 +926,9 @@ let split_defs continue_anyway splits defs = -> exp,assigns | E_cast (t,e') -> let e'',assigns = const_prop_exp substs assigns e' in - re (E_cast (t, e'')) assigns + if is_value e'' && e' <> e'' + then reduce_cast t e'' l annot, assigns + else re (E_cast (t, e'')) assigns | E_app (id,es) -> let es',assigns = non_det_exp_list es in let env = Type_check.env_of_annot (l, annot) in diff --git a/src/type_check.mli b/src/type_check.mli index 92949c85..5066553e 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -105,6 +105,8 @@ module Env : sig (* Get the current set of constraints. *) val get_constraints : t -> n_constraint list + val add_constraint : n_constraint -> t -> t + val get_typ_var : kid -> t -> base_kind_aux val get_typ_vars : t -> base_kind_aux KBindings.t -- cgit v1.2.3 From e227238dfa54ad337afa00648a35e8932d42fd06 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 12 Jan 2018 11:32:30 +0000 Subject: Remove generic comparison --- 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 5ffe75d4..389dacd4 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -926,7 +926,7 @@ let split_defs continue_anyway splits defs = -> exp,assigns | E_cast (t,e') -> let e'',assigns = const_prop_exp substs assigns e' in - if is_value e'' && e' <> e'' + if is_value e'' then reduce_cast t e'' l annot, assigns else re (E_cast (t, e'')) assigns | E_app (id,es) -> -- cgit v1.2.3 From 83538020553691efe472984ee16ebd04eb252f82 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 12 Jan 2018 17:33:56 +0000 Subject: Try to keep types for undefined around during monomorphisation Otherwise the type checker can't figure it out when we substitute --- src/monomorphise.ml | 42 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 40 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 389dacd4..dd0edd64 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -183,6 +183,8 @@ let rec is_value (E_aux (e,(l,annot))) = | E_lit _ -> true | E_tuple es -> List.for_all is_value es | E_app (id,es) -> is_constructor id && List.for_all is_value es + (* We add casts to undefined to keep the type information in the AST *) + | E_cast (typ,E_aux (E_lit (L_aux (L_undef,_)),_)) -> true (* TODO: more? *) | _ -> false @@ -671,6 +673,10 @@ let atom_typ_kid kid = function let reduce_cast typ exp l annot = let env = env_of_annot (l,annot) in + let replace_typ typ = function + | Some (env,_,eff) -> Some (env,typ,eff) + | None -> None + in let typ' = Env.base_typ_of env typ in match exp, destruct_exist env typ' with | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' -> @@ -683,7 +689,14 @@ let reduce_cast typ exp l annot = " does not satisfy constraint " ^ string_of_n_constraint nc)) | E_aux (E_lit (L_aux (L_undef,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' -> let nexp = fabricate_nexp_exist env Unknown typ [kid] nc typ'' in - E_aux (E_cast (subst_src_typ (KBindings.singleton kid nexp) typ'', exp),(Generated l,None)) + let newtyp = subst_src_typ (KBindings.singleton kid nexp) typ'' in + E_aux (E_cast (newtyp, exp), (Generated l,replace_typ newtyp annot)) + | E_aux (E_cast (_, + (E_aux (E_lit (L_aux (L_undef,_)),_) as exp)),_), + Some ([kid],nc,typ'') when atom_typ_kid kid typ'' -> + let nexp = fabricate_nexp_exist env Unknown typ [kid] nc typ'' in + let newtyp = subst_src_typ (KBindings.singleton kid nexp) typ'' in + E_aux (E_cast (newtyp, exp), (Generated l,replace_typ newtyp annot)) | _ -> E_aux (E_cast (typ,exp),(l,annot)) (* Used for constant propagation in pattern matches *) @@ -754,6 +767,8 @@ let try_app (l,ann) (id,args) = else if is_id "ex_int" then match args with | [E_aux (E_lit lit,(l,_))] -> Some (E_aux (E_lit lit,(l,ann))) + | [E_aux (E_cast (_,(E_aux (E_lit (L_aux (L_undef,_)),_) as e)),(l,_))] -> + Some (reduce_cast (typ_of_annot (l,ann)) e l ann) | _ -> None else if is_id "vector_access" || is_id "bitvector_access" then match args with @@ -824,6 +839,14 @@ let rec assigned_vars_in_lexp (LEXP_aux (le,_)) = IdSet.union (assigned_vars_in_lexp le) (IdSet.union (assigned_vars e1) (assigned_vars e2)) | LEXP_field (le,_) -> assigned_vars_in_lexp le +(* Add a cast to undefined so that it retains its type, otherwise it can't be + substituted safely *) +let keep_undef_typ value = + match value with + | E_aux (E_lit (L_aux (L_undef,lann)),eann) -> + E_aux (E_cast (typ_of_annot eann,value),(Generated Unknown,snd eann)) + | _ -> value + let split_defs continue_anyway splits defs = let split_constructors (Defs defs) = let sc_type_union q (Tu_aux (tu,l) as tua) = @@ -1052,7 +1075,7 @@ let split_defs continue_anyway splits defs = match Env.lookup_id id env with | Local (Mutable,_) | Unbound -> if is_value e' - then Bindings.add id e' assigns + then Bindings.add id (keep_undef_typ e') assigns else Bindings.remove id assigns | _ -> assigns end @@ -1224,6 +1247,21 @@ let split_defs continue_anyway splits defs = (Reporting_basic.print_err false true l' "Monomorphisation" "Unexpected kind of pattern for literal"; GiveUp) in findpat_generic checkpat "literal" assigns cases + | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)) -> + let checkpat = function + | P_aux (P_lit (L_aux (lit_p, _)),_) -> DoesNotMatch + | P_aux (P_var (P_aux (P_id id,p_id_annot), kid),_) -> + (* For undefined we fix the type-level size (because there's no good + way to construct an undefined size), but leave the term as undefined + to make the meaning clear. *) + let nexp = fabricate_nexp l annot in + let typ = subst_src_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in + DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,None))], + [kid,nexp]) + | P_aux (_,(l',_)) -> + (Reporting_basic.print_err false true l' "Monomorphisation" + "Unexpected kind of pattern for literal"; GiveUp) + in findpat_generic checkpat "literal" assigns cases | _ -> None and can_match exp = -- cgit v1.2.3