(**************************************************************************) (* 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 Spec_analysis open Type_check (* COULD DO: dead code is only eliminated at if expressions, but we could also cut out impossible case branches and code after assertions. *) (* Constant propogation. Takes maps of immutable/mutable variables to subsitute. The substs argument also contains the current type-level kid refinements so that we can check for dead code. Extremely conservative about evaluation order of assignments in subexpressions, dropping assignments rather than committing to any particular order *) let kbindings_from_list = List.fold_left (fun s (v,i) -> KBindings.add v i s) KBindings.empty let bindings_from_list = List.fold_left (fun s (v,i) -> Bindings.add v i s) Bindings.empty (* union was introduced in 4.03.0, a bit too recently *) let bindings_union s1 s2 = Bindings.merge (fun _ x y -> match x,y with | _, (Some x) -> Some x | (Some x), _ -> Some x | _, _ -> None) s1 s2 let kbindings_union s1 s2 = KBindings.merge (fun _ x y -> match x,y with | _, (Some x) -> Some x | (Some x), _ -> Some x | _, _ -> None) s1 s2 let rec list_extract f = function | [] -> None | h::t -> match f h with None -> list_extract f t | Some v -> Some v let is_pure e = match e with | Effect_aux (Effect_set [],_) -> true | _ -> false let remove_bound (substs,ksubsts) pat = let bound = bindings_from_pat pat in List.fold_left (fun sub v -> Bindings.remove v sub) substs bound, ksubsts let rec is_value (E_aux (e,(l,annot))) = let is_constructor id = match destruct_tannot annot with | None -> (Reporting.print_err l "Monomorphisation" ("Missing type information for identifier " ^ string_of_id id); false) (* Be conservative if we have no info *) | Some (env,_,_) -> Env.is_union_constructor id env || (match Env.lookup_id id env with | Enum _ -> true | Unbound | Local _ | Register _ -> false) in match e with | E_id id -> is_constructor id | 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 let isubst_minus_set subst set = IdSet.fold Bindings.remove set subst let threaded_map f state l = let l',state' = List.fold_left (fun (tl,state) element -> let (el',state') = f state element in (el'::tl,state')) ([],state) l in List.rev l',state' (* Attempt simple pattern matches *) let lit_match = function | (L_zero | L_false), (L_zero | L_false) -> true | (L_one | L_true ), (L_one | L_true ) -> true | L_num i1, L_num i2 -> Big_int.equal i1 i2 | l1,l2 -> l1 = l2 (* 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",_), [A_aux (A_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",_), [A_aux (A_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",_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_); A_aux (A_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",_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_); A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) when Kid.compare kid kid'' = 0 && Kid.compare kid kid''' = 0 -> nint 32 | ([], _, typ) -> nint 32 | (kids, nc, typ) -> raise (Reporting.err_general l ("Undefined value at unsupported type " ^ string_of_typ typ ^ " with " ^ Util.string_of_list ", " string_of_kid kids)) let fabricate_nexp l tannot = match destruct_tannot tannot with | None -> nint 32 | Some (env,typ,_) -> match Type_check.destruct_exist (Type_check.Env.expand_synonyms env typ) with | None -> nint 32 (* TODO: check this *) | Some (kopts,nc,typ') -> fabricate_nexp_exist env l typ (List.map kopt_kid kopts) nc typ' let atom_typ_kid kid = function | Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_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.expand_synonyms env typ') with | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' -> let nc_env = Env.add_typ_var l kopt env in let nc_env = Env.add_constraint (nc_eq (nvar (kopt_kid kopt)) (nconstant n)) nc_env in if prove __POS__ nc_env nc then exp else raise (Reporting.err_unreachable l __POS__ ("Constant propagation error: literal " ^ Big_int.to_string n ^ " does not satisfy constraint " ^ string_of_n_constraint nc)) | E_aux (E_lit (L_aux (L_undef,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' -> let nexp = fabricate_nexp_exist env Unknown typ [kopt_kid kopt] nc typ'' in let newtyp = subst_kids_typ (KBindings.singleton (kopt_kid kopt) 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 ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' -> let nexp = fabricate_nexp_exist env Unknown typ [kopt_kid kopt] nc typ'' in let newtyp = subst_kids_typ (KBindings.singleton (kopt_kid kopt) 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 *) type 'a matchresult = | DoesMatch of 'a | DoesNotMatch | GiveUp (* Remove top-level casts from an expression. Useful when we need to look at subexpressions to reduce something, but could break type-checking if we used it everywhere. *) let rec drop_casts = function | E_aux (E_cast (_,e),_) -> drop_casts e | exp -> exp let int_of_str_lit = function | L_hex hex -> Big_int.of_string ("0x" ^ hex) | L_bin bin -> Big_int.of_string ("0b" ^ bin) | _ -> assert false let bits_of_lit = function | L_bin bin -> bin | L_hex hex -> hex_to_bin hex | _ -> assert false let slice_lit (L_aux (lit,ll)) i len (Ord_aux (ord,_)) = let i = Big_int.to_int i in let len = Big_int.to_int len in let bin = bits_of_lit lit in match match ord with | Ord_inc -> Some i | Ord_dec -> Some (String.length bin - i - len) | Ord_var _ -> None with | None -> None | Some i -> Some (L_aux (L_bin (String.sub bin i len),Generated ll)) let concat_vec lit1 lit2 = let bits1 = bits_of_lit lit1 in let bits2 = bits_of_lit lit2 in L_bin (bits1 ^ bits2) let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) = match l1,l2 with | (L_zero|L_false), (L_zero|L_false) | (L_one |L_true ), (L_one |L_true) -> Some true | (L_hex _| L_bin _), (L_hex _|L_bin _) -> Some (Big_int.equal (int_of_str_lit l1) (int_of_str_lit l2)) | L_undef, _ | _, L_undef -> None | L_num i1, L_num i2 -> Some (Big_int.equal i1 i2) | _ -> Some (l1 = l2) let try_app (l,ann) (id,args) = let new_l = Parse_ast.Generated l in let env = env_of_annot (l,ann) in let get_overloads f = List.map string_of_id (Env.get_overloads (Id_aux (Id f, Parse_ast.Unknown)) env @ Env.get_overloads (Id_aux (DeIid f, Parse_ast.Unknown)) env) in let is_id f = List.mem (string_of_id id) (f :: get_overloads f) in if is_id "==" || is_id "!=" then match args with | [E_aux (E_lit l1,_); E_aux (E_lit l2,_)] -> let lit b = if b then L_true else L_false in let lit b = lit (if is_id "==" then b else not b) in (match lit_eq l1 l2 with | None -> None | Some b -> Some (E_aux (E_lit (L_aux (lit b,new_l)),(l,ann)))) | _ -> None else if is_id "cast_bit_bool" then match args with | [E_aux (E_lit L_aux (L_zero,_),_)] -> Some (E_aux (E_lit (L_aux (L_false,new_l)),(l,ann))) | [E_aux (E_lit L_aux (L_one ,_),_)] -> Some (E_aux (E_lit (L_aux (L_true ,new_l)),(l,ann))) | _ -> None else if is_id "UInt" || is_id "unsigned" then match args with | [E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit,_), _)] -> Some (E_aux (E_lit (L_aux (L_num (int_of_str_lit lit),new_l)),(l,ann))) | _ -> None else if is_id "slice" then match args with | [E_aux (E_lit (L_aux ((L_hex _| L_bin _),_) as lit), annot); E_aux (E_lit L_aux (L_num i,_), _); E_aux (E_lit L_aux (L_num len,_), _)] -> (match Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) with | Typ_aux (Typ_app (_,[_;A_aux (A_order ord,_);_]),_) -> (match slice_lit lit i len ord with | Some lit' -> Some (E_aux (E_lit lit',(l,ann))) | None -> None) | _ -> None) | _ -> None else if is_id "bitvector_concat" then match args with | [E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit1,_), _); E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit2,_), _)] -> Some (E_aux (E_lit (L_aux (concat_vec lit1 lit2,new_l)),(l,ann))) | _ -> None else if is_id "shl_int" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.shift_left i (Big_int.to_int j)),new_l)),(l,ann))) | _ -> None else if is_id "mult_atom" || is_id "mult_int" || is_id "mult_range" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.mul i j),new_l)),(l,ann))) | _ -> None else if is_id "quotient_nat" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.div i j),new_l)),(l,ann))) | _ -> None else if is_id "add_atom" || is_id "add_int" || is_id "add_range" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.add i j),new_l)),(l,ann))) | _ -> None else if is_id "negate_range" then match args with | [E_aux (E_lit L_aux (L_num i,_),_)] -> Some (E_aux (E_lit (L_aux (L_num (Big_int.negate i),new_l)),(l,ann))) | _ -> None 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 | [E_aux (E_lit L_aux ((L_hex _ | L_bin _) as lit,_),_); E_aux (E_lit L_aux (L_num i,_),_)] -> let v = int_of_str_lit lit in let b = Big_int.bitwise_and (Big_int.shift_right v (Big_int.to_int i)) (Big_int.of_int 1) in let lit' = if Big_int.equal b (Big_int.of_int 1) then L_one else L_zero in Some (E_aux (E_lit (L_aux (lit',new_l)),(l,ann))) | _ -> None else None let construct_lit_vector args = let rec aux l = function | [] -> Some (L_aux (L_bin (String.concat "" (List.rev l)),Unknown)) | E_aux (E_lit (L_aux ((L_zero | L_one) as lit,_)),_)::t -> aux ((if lit = L_zero then "0" else "1")::l) t | _ -> None in aux [] args (* 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 (* Check whether the current environment with the given kid assignments is inconsistent (and hence whether the code is dead) *) let is_env_inconsistent env ksubsts = let env = KBindings.fold (fun k nexp env -> Env.add_constraint (nc_eq (nvar k) nexp) env) ksubsts env in prove __POS__ env nc_false let const_prop defs = let rec const_prop_exp ref_vars substs assigns ((E_aux (e,(l,annot))) as exp) = (* Functions to treat lists and tuples of subexpressions as possibly non-deterministic: that is, we stop making any assumptions about variables that are assigned to in any of the subexpressions *) let non_det_exp_list es = let assigned_in = List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp)) IdSet.empty es in let assigns = isubst_minus_set assigns assigned_in in let es' = List.map (fun e -> fst (const_prop_exp ref_vars substs assigns e)) es in es',assigns in let non_det_exp_2 e1 e2 = let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in let assigns = isubst_minus_set assigns assigned_in_e12 in let e1',_ = const_prop_exp ref_vars substs assigns e1 in let e2',_ = const_prop_exp ref_vars substs assigns e2 in e1',e2',assigns in let non_det_exp_3 e1 e2 e3 = let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in let assigned_in_e123 = IdSet.union assigned_in_e12 (assigned_vars e3) in let assigns = isubst_minus_set assigns assigned_in_e123 in let e1',_ = const_prop_exp ref_vars substs assigns e1 in let e2',_ = const_prop_exp ref_vars substs assigns e2 in let e3',_ = const_prop_exp ref_vars substs assigns e3 in e1',e2',e3',assigns in let non_det_exp_4 e1 e2 e3 e4 = let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in let assigned_in_e123 = IdSet.union assigned_in_e12 (assigned_vars e3) in let assigned_in_e1234 = IdSet.union assigned_in_e123 (assigned_vars e4) in let assigns = isubst_minus_set assigns assigned_in_e1234 in let e1',_ = const_prop_exp ref_vars substs assigns e1 in let e2',_ = const_prop_exp ref_vars substs assigns e2 in let e3',_ = const_prop_exp ref_vars substs assigns e3 in let e4',_ = const_prop_exp ref_vars substs assigns e4 in e1',e2',e3',e4',assigns in let re e assigns = E_aux (e,(l,annot)),assigns in match e with (* TODO: are there more circumstances in which we should get rid of these? *) | E_block [e] -> const_prop_exp ref_vars substs assigns e | E_block es -> let es',assigns = threaded_map (const_prop_exp ref_vars substs) assigns es in re (E_block es') assigns | E_nondet es -> let es',assigns = non_det_exp_list es in re (E_nondet es') assigns | E_id id -> let env = Type_check.env_of_annot (l, annot) in (try match Env.lookup_id id env with | Local (Immutable,_) -> Bindings.find id (fst substs) | Local (Mutable,_) -> Bindings.find id assigns | _ -> exp with Not_found -> exp),assigns | E_lit _ | E_sizeof _ | E_constraint _ -> exp,assigns | E_cast (t,e') -> let e'',assigns = const_prop_exp ref_vars substs assigns e' in if is_value 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 (match try_app (l,annot) (id,es') with | None -> (match const_prop_try_fn ref_vars l env (id,es') with | None -> re (E_app (id,es')) assigns | Some r -> r,assigns) | Some r -> r,assigns) | E_tuple es -> let es',assigns = non_det_exp_list es in re (E_tuple es') assigns | E_if (e1,e2,e3) -> let e1',assigns = const_prop_exp ref_vars substs assigns e1 in let e1_no_casts = drop_casts e1' in (match e1_no_casts with | E_aux (E_lit (L_aux ((L_true|L_false) as lit ,_)),_) -> (match lit with | L_true -> const_prop_exp ref_vars substs assigns e2 | _ -> const_prop_exp ref_vars substs assigns e3) | _ -> (* If the guard is an equality check, propagate the value. *) let env1 = env_of e1_no_casts in let is_equal id = List.exists (fun id' -> Id.compare id id' == 0) (Env.get_overloads (Id_aux (DeIid "==", Parse_ast.Unknown)) env1) in let substs_true = match e1_no_casts with | E_aux (E_app (id, [E_aux (E_id var,_); vl]),_) | E_aux (E_app (id, [vl; E_aux (E_id var,_)]),_) when is_equal id -> if is_value vl then (match Env.lookup_id var env1 with | Local (Immutable,_) -> Bindings.add var vl (fst substs),snd substs | _ -> substs) else substs | _ -> substs in (* Discard impossible branches *) if is_env_inconsistent (env_of e2) (snd substs) then const_prop_exp ref_vars substs assigns e3 else if is_env_inconsistent (env_of e3) (snd substs) then const_prop_exp ref_vars substs_true assigns e2 else let e2',assigns2 = const_prop_exp ref_vars substs_true assigns e2 in let e3',assigns3 = const_prop_exp ref_vars substs assigns e3 in let assigns = isubst_minus_set assigns (assigned_vars e2) in let assigns = isubst_minus_set assigns (assigned_vars e3) in re (E_if (e1',e2',e3')) assigns) | E_for (id,e1,e2,e3,ord,e4) -> (* Treat e1, e2 and e3 (from, to and by) as a non-det tuple *) let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in let assigns = isubst_minus_set assigns (assigned_vars e4) in let e4',_ = const_prop_exp ref_vars (Bindings.remove id (fst substs),snd substs) assigns e4 in re (E_for (id,e1',e2',e3',ord,e4')) assigns | E_loop (loop,e1,e2) -> let assigns = isubst_minus_set assigns (IdSet.union (assigned_vars e1) (assigned_vars e2)) in let e1',_ = const_prop_exp ref_vars substs assigns e1 in let e2',_ = const_prop_exp ref_vars substs assigns e2 in re (E_loop (loop,e1',e2')) assigns | E_vector es -> let es',assigns = non_det_exp_list es in begin match construct_lit_vector es' with | None -> re (E_vector es') assigns | Some lit -> re (E_lit lit) assigns end | E_vector_access (e1,e2) -> let e1',e2',assigns = non_det_exp_2 e1 e2 in re (E_vector_access (e1',e2')) assigns | E_vector_subrange (e1,e2,e3) -> let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in re (E_vector_subrange (e1',e2',e3')) assigns | E_vector_update (e1,e2,e3) -> let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in re (E_vector_update (e1',e2',e3')) assigns | E_vector_update_subrange (e1,e2,e3,e4) -> let e1',e2',e3',e4',assigns = non_det_exp_4 e1 e2 e3 e4 in re (E_vector_update_subrange (e1',e2',e3',e4')) assigns | E_vector_append (e1,e2) -> let e1',e2',assigns = non_det_exp_2 e1 e2 in re (E_vector_append (e1',e2')) assigns | E_list es -> let es',assigns = non_det_exp_list es in re (E_list es') assigns | E_cons (e1,e2) -> let e1',e2',assigns = non_det_exp_2 e1 e2 in re (E_cons (e1',e2')) assigns | E_record fes -> let assigned_in_fes = assigned_vars_in_fexps fes in let assigns = isubst_minus_set assigns assigned_in_fes in re (E_record (const_prop_fexps ref_vars substs assigns fes)) assigns | E_record_update (e,fes) -> let assigned_in = IdSet.union (assigned_vars_in_fexps fes) (assigned_vars e) in let assigns = isubst_minus_set assigns assigned_in in let e',_ = const_prop_exp ref_vars substs assigns e in re (E_record_update (e', const_prop_fexps ref_vars substs assigns fes)) assigns | E_field (e,id) -> let e',assigns = const_prop_exp ref_vars substs assigns e in re (E_field (e',id)) assigns | E_case (e,cases) -> let e',assigns = const_prop_exp ref_vars substs assigns e in (match can_match ref_vars e' cases substs assigns with | None -> let assigned_in = List.fold_left (fun vs pe -> IdSet.union vs (assigned_vars_in_pexp pe)) IdSet.empty cases in let assigns' = isubst_minus_set assigns assigned_in in re (E_case (e', List.map (const_prop_pexp ref_vars substs assigns) cases)) assigns' | Some (E_aux (_,(_,annot')) as exp,newbindings,kbindings) -> let exp = nexp_subst_exp (kbindings_from_list kbindings) exp in let newbindings_env = bindings_from_list newbindings in let substs' = bindings_union (fst substs) newbindings_env, snd substs in const_prop_exp ref_vars substs' assigns exp) | E_let (lb,e2) -> begin match lb with | LB_aux (LB_val (p,e), annot) -> let e',assigns = const_prop_exp ref_vars substs assigns e in let substs' = remove_bound substs p in let plain () = let e2',assigns = const_prop_exp ref_vars substs' assigns e2 in re (E_let (LB_aux (LB_val (p,e'), annot), e2')) assigns in if is_value e' && not (is_value e) then match can_match ref_vars e' [Pat_aux (Pat_exp (p,e2),(Unknown,empty_tannot))] substs assigns with | None -> plain () | Some (e'',bindings,kbindings) -> let e'' = nexp_subst_exp (kbindings_from_list kbindings) e'' in let bindings = bindings_from_list bindings in let substs'' = bindings_union (fst substs') bindings, snd substs' in const_prop_exp ref_vars substs'' assigns e'' else plain () end (* TODO maybe - tuple assignments *) | E_assign (le,e) -> let env = Type_check.env_of_annot (l, annot) in let assigned_in = IdSet.union (assigned_vars_in_lexp le) (assigned_vars e) in let assigns = isubst_minus_set assigns assigned_in in let le',idopt = const_prop_lexp ref_vars substs assigns le in let e',_ = const_prop_exp ref_vars substs assigns e in let assigns = match idopt with | Some id -> begin match Env.lookup_id id env with | Local (Mutable,_) | Unbound -> if is_value e' && not (IdSet.mem id ref_vars) then Bindings.add id (keep_undef_typ e') assigns else Bindings.remove id assigns | _ -> assigns end | None -> assigns in re (E_assign (le', e')) assigns | E_exit e -> let e',_ = const_prop_exp ref_vars substs assigns e in re (E_exit e') Bindings.empty | E_ref id -> re (E_ref id) Bindings.empty | E_throw e -> let e',_ = const_prop_exp ref_vars substs assigns e in re (E_throw e') Bindings.empty | E_try (e,cases) -> (* TODO: try and preserve *any* assignment info *) let e',_ = const_prop_exp ref_vars substs assigns e in re (E_case (e', List.map (const_prop_pexp ref_vars substs Bindings.empty) cases)) Bindings.empty | E_return e -> let e',_ = const_prop_exp ref_vars substs assigns e in re (E_return e') Bindings.empty | E_assert (e1,e2) -> let e1',e2',assigns = non_det_exp_2 e1 e2 in re (E_assert (e1',e2')) assigns | E_app_infix _ | E_var _ | E_internal_plet _ | E_internal_return _ | E_internal_value _ -> raise (Reporting.err_unreachable l __POS__ ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp)) and const_prop_fexps ref_vars substs assigns fes = List.map (const_prop_fexp ref_vars substs assigns) fes and const_prop_fexp ref_vars substs assigns (FE_aux (FE_Fexp (id,e), annot)) = FE_aux (FE_Fexp (id,fst (const_prop_exp ref_vars substs assigns e)),annot) and const_prop_pexp ref_vars substs assigns = function | (Pat_aux (Pat_exp (p,e),l)) -> Pat_aux (Pat_exp (p,fst (const_prop_exp ref_vars (remove_bound substs p) assigns e)),l) | (Pat_aux (Pat_when (p,e1,e2),l)) -> let substs' = remove_bound substs p in let e1',assigns = const_prop_exp ref_vars substs' assigns e1 in Pat_aux (Pat_when (p, e1', fst (const_prop_exp ref_vars substs' assigns e2)),l) and const_prop_lexp ref_vars substs assigns ((LEXP_aux (e,annot)) as le) = let re e = LEXP_aux (e,annot), None in match e with | LEXP_id id (* shouldn't end up substituting here *) | LEXP_cast (_,id) -> le, Some id | LEXP_memory (id,es) -> re (LEXP_memory (id,List.map (fun e -> fst (const_prop_exp ref_vars substs assigns e)) es)) (* or here *) | LEXP_tup les -> re (LEXP_tup (List.map (fun le -> fst (const_prop_lexp ref_vars substs assigns le)) les)) | LEXP_vector (le,e) -> re (LEXP_vector (fst (const_prop_lexp ref_vars substs assigns le), fst (const_prop_exp ref_vars substs assigns e))) | LEXP_vector_range (le,e1,e2) -> 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))) (* Reduce a function when 1. all arguments are values, 2. the function is pure, 3. the result is a value (and 4. the function is not scattered, but that's not terribly important) to try and keep execution time and the results managable. *) and const_prop_try_fn ref_vars l env (id,args) = if not (List.for_all is_value args) then None else let (tq,typ) = Env.get_val_spec_orig id env in let eff = match typ with | Typ_aux (Typ_fn (_,_,eff),_) -> Some eff | _ -> None in let Defs ds = defs in match eff, list_extract (function | (DEF_fundef (FD_aux (FD_function (_,_,eff,((FCL_aux (FCL_Funcl (id',_),_))::_ as fcls)),_))) -> if Id.compare id id' = 0 then Some fcls else None | _ -> None) ds with | None,_ | _,None -> None | Some eff,_ when not (is_pure eff) -> None | Some _,Some fcls -> let arg = match args with | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,empty_tannot)) | [e] -> e | _ -> E_aux (E_tuple args,(Generated l,empty_tannot)) in let cases = List.map (function | FCL_aux (FCL_Funcl (_,pexp), ann) -> pexp) fcls in match can_match_with_env ref_vars env arg cases (Bindings.empty,KBindings.empty) Bindings.empty with | Some (exp,bindings,kbindings) -> let substs = bindings_from_list bindings, kbindings_from_list kbindings in let result,_ = const_prop_exp ref_vars substs Bindings.empty exp in let result = match result with | E_aux (E_return e,_) -> e | _ -> result in if is_value result then Some result else None | None -> None and can_match_with_env ref_vars env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns = let rec findpat_generic check_pat description assigns = function | [] -> (Reporting.print_err l "Monomorphisation" ("Failed to find a case for " ^ description); None) | [Pat_aux (Pat_exp (P_aux (P_wild,_),exp),_)] -> Some (exp,[],[]) | (Pat_aux (Pat_exp (P_aux (P_typ (_,p),_),exp),ann))::tl -> findpat_generic check_pat description assigns ((Pat_aux (Pat_exp (p,exp),ann))::tl) | (Pat_aux (Pat_exp (P_aux (P_id id',_),exp),_))::tlx when pat_id_is_variable env id' -> Some (exp, [(id', exp0)], []) | (Pat_aux (Pat_when (P_aux (P_id id',_),guard,exp),_))::tl when pat_id_is_variable env id' -> begin let substs = Bindings.add id' exp0 substs, ksubsts in let (E_aux (guard,_)),assigns = const_prop_exp ref_vars substs assigns guard in match guard with | E_lit (L_aux (L_true,_)) -> Some (exp,[(id',exp0)],[]) | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl | _ -> None end | (Pat_aux (Pat_when (p,guard,exp),_))::tl -> begin match check_pat p with | DoesNotMatch -> findpat_generic check_pat description assigns tl | DoesMatch (vsubst,ksubst) -> begin let guard = nexp_subst_exp (kbindings_from_list ksubst) guard in let substs = bindings_union substs (bindings_from_list vsubst), kbindings_union ksubsts (kbindings_from_list ksubst) in let (E_aux (guard,_)),assigns = const_prop_exp ref_vars substs assigns guard in match guard with | E_lit (L_aux (L_true,_)) -> Some (exp,vsubst,ksubst) | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl | _ -> None end | GiveUp -> None end | (Pat_aux (Pat_exp (p,exp),_))::tl -> match check_pat p with | DoesNotMatch -> findpat_generic check_pat description assigns tl | DoesMatch (subst,ksubst) -> Some (exp,subst,ksubst) | GiveUp -> None in match e with | E_id id -> (match Env.lookup_id id env with | Enum _ -> let checkpat = function | P_aux (P_id id',_) | P_aux (P_app (id',[]),_) -> if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch | P_aux (_,(l',_)) -> (Reporting.print_err l' "Monomorphisation" "Unexpected kind of pattern for enumeration"; GiveUp) in findpat_generic checkpat (string_of_id id) assigns cases | _ -> None) | E_lit (L_aux (lit_e, lit_l)) -> let checkpat = function | P_aux (P_lit (L_aux (lit_p, _)),_) -> if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) -> begin match lit_e with | L_num i -> DoesMatch ([id, E_aux (e,(l,annot))], [kid,Nexp_aux (Nexp_constant i,Unknown)]) (* 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. *) | L_undef -> let nexp = fabricate_nexp l annot in let typ = subst_kids_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))], [kid,nexp]) | _ -> (Reporting.print_err lit_l "Monomorphisation" "Unexpected kind of literal for var match"; GiveUp) end | P_aux (_,(l',_)) -> (Reporting.print_err l' "Monomorphisation" "Unexpected kind of pattern for literal"; GiveUp) in findpat_generic checkpat "literal" assigns cases | E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es -> let checkpat = function | P_aux (P_vector ps,_) -> let matches = List.map2 (fun e p -> match e, p with | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) -> if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var -> DoesMatch ([var, e],[]) | _ -> GiveUp) es ps in let final = List.fold_left (fun acc m -> match acc, m with | _, GiveUp -> GiveUp | GiveUp, _ -> GiveUp | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub') | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in (match final with | GiveUp -> (Reporting.print_err l "Monomorphisation" "Unexpected kind of pattern for vector literal"; GiveUp) | _ -> final) | _ -> (Reporting.print_err l "Monomorphisation" "Unexpected kind of pattern for vector literal"; GiveUp) in findpat_generic checkpat "vector 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), TP_aux (TP_var 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 kids = equal_kids (env_of_annot p_id_annot) kid in let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in let typ = subst_kids_typ ksubst (typ_of_annot p_id_annot) in DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))], KBindings.bindings ksubst) | P_aux (_,(l',_)) -> (Reporting.print_err l' "Monomorphisation" "Unexpected kind of pattern for literal"; GiveUp) in findpat_generic checkpat "literal" assigns cases | _ -> None and can_match ref_vars exp = let env = Type_check.env_of exp in can_match_with_env ref_vars env exp in const_prop_exp