(**************************************************************************) (* 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 | E_vector es -> List.for_all is_value es | E_record fes -> List.for_all (fun (FE_aux (FE_Fexp (_, e), _)) -> is_value e) fes | 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 (* Also keep casts around records, as type inference fails without *) | E_cast (_, (E_aux (E_record _, _) as e')) -> is_value e' (* 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 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 = let e_aux (e, ann) = match e with | E_lit (L_aux (L_undef, _)) -> (* Add cast to undefined... *) E_aux (E_cast (typ_of_annot ann, E_aux (e, ann)), ann) | E_cast (typ, E_aux (E_cast (_, e), _)) -> (* ... unless there was a cast already *) E_aux (E_cast (typ, e), ann) | _ -> E_aux (e, ann) in let open Rewriter in fold_exp { id_exp_alg with e_aux = e_aux } 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 module StringSet = Set.Make(String) module StringMap = Map.Make(String) let const_props target ast ref_vars = let const_fold exp = (* Constant-fold function applications with constant arguments *) let interpreter_istate = (* Do not interpret undefined_X functions *) let open Interpreter in let undefined_builtin_ids = ids_of_defs Initial_check.undefined_builtin_val_specs in let remove_primop id = StringMap.remove (string_of_id id) in let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in let (lstate, gstate) = Constant_fold.initial_state ast Type_check.initial_env in (lstate, { gstate with primops = remove_undefined_primops gstate.primops }) in try strip_exp exp |> infer_exp (env_of exp) |> Constant_fold.rewrite_exp_once target interpreter_istate |> keep_undef_typ with | _ -> exp in let constants = let add m = function | DEF_val (LB_aux (LB_val (P_aux ((P_id id | P_typ (_,P_aux (P_id id,_))),_), exp),_)) when Constant_fold.is_constant exp -> Bindings.add id exp m | _ -> m in List.fold_left add Bindings.empty ast.defs in let replace_constant (E_aux (e,annot) as exp) = match e with | E_id id -> (match Bindings.find_opt id constants with | Some e -> e | None -> exp) | _ -> exp in let rec const_prop_exp 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 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 substs assigns e1 in let e2',_ = const_prop_exp 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 substs assigns e1 in let e2',_ = const_prop_exp substs assigns e2 in let e3',_ = const_prop_exp 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 substs assigns e1 in let e2',_ = const_prop_exp substs assigns e2 in let e3',_ = const_prop_exp substs assigns e3 in let e4',_ = const_prop_exp substs assigns e4 in e1',e2',e3',e4',assigns in let rewrap e = E_aux (e,(l,annot)) in let re e assigns = rewrap e,assigns in match e with (* TODO: are there more circumstances in which we should get rid of these? *) | E_block [e] -> const_prop_exp substs assigns e | E_block es -> let es',assigns = threaded_map (const_prop_exp substs) assigns es in re (E_block 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 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 const_prop_try_fn env (id, es') (l, annot), 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 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 substs assigns e2 | _ -> const_prop_exp 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 (Operator "==", 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 substs assigns e3 else if is_env_inconsistent (env_of e3) (snd substs) then const_prop_exp substs_true assigns e2 else let e2',assigns2 = const_prop_exp substs_true assigns e2 in let e3',assigns3 = const_prop_exp 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 (Bindings.remove id (fst substs),snd substs) assigns e4 in re (E_for (id,e1',e2',e3',ord,e4')) assigns | E_loop (loop,m,e1,e2) -> let assigns = isubst_minus_set assigns (IdSet.union (assigned_vars e1) (assigned_vars e2)) in let m' = match m with | Measure_aux (Measure_none,_) -> m | Measure_aux (Measure_some exp,l) -> let exp',_ = const_prop_exp substs assigns exp in Measure_aux (Measure_some exp',l) in let e1',_ = const_prop_exp substs assigns e1 in let e2',_ = const_prop_exp substs assigns e2 in re (E_loop (loop,m',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 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 substs assigns e in let fes' = const_prop_fexps substs assigns fes in begin match unaux_exp (fst (uncast_exp e')) with | E_record (fes0) -> let apply_fexp (FE_aux (FE_Fexp (id, e), _)) (FE_aux (FE_Fexp (id', e'), ann)) = if Id.compare id id' = 0 then FE_aux (FE_Fexp (id', e), ann) else FE_aux (FE_Fexp (id', e'), ann) in let update_fields fexp = List.map (apply_fexp fexp) in let fes0' = List.fold_right update_fields fes' fes0 in re (E_record fes0') assigns | _ -> re (E_record_update (e', fes')) assigns end | E_field (e,id) -> let e',assigns = const_prop_exp substs assigns e in begin let is_field (FE_aux (FE_Fexp (id', _), _)) = Id.compare id id' = 0 in match unaux_exp e' with | E_record fes0 when List.exists is_field fes0 -> let (FE_aux (FE_Fexp (_, e), _)) = List.find is_field fes0 in re (unaux_exp e) assigns | _ -> re (E_field (e',id)) assigns end | E_case (e,cases) -> let e',assigns = const_prop_exp substs assigns e in (match can_match 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 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 substs' assigns exp) | E_let (lb,e2) -> begin match lb with | LB_aux (LB_val (p,e), annot) -> let e',assigns = const_prop_exp substs assigns e in let substs' = remove_bound substs p in let plain () = let e2',assigns = const_prop_exp substs' assigns e2 in re (E_let (LB_aux (LB_val (p,e'), annot), e2')) assigns in if is_value e' then match can_match 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 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 substs assigns le in let e',_ = const_prop_exp 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 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 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 substs assigns e in re (E_case (e', List.map (const_prop_pexp substs Bindings.empty) cases)) Bindings.empty | E_return e -> let e',_ = const_prop_exp 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 substs assigns fes = List.map (const_prop_fexp substs assigns) fes and const_prop_fexp substs assigns (FE_aux (FE_Fexp (id,e), annot)) = FE_aux (FE_Fexp (id,fst (const_prop_exp substs assigns e)),annot) and const_prop_pexp substs assigns = function | (Pat_aux (Pat_exp (p,e),l)) -> Pat_aux (Pat_exp (p,fst (const_prop_exp (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 substs' assigns e1 in Pat_aux (Pat_when (p, e1', fst (const_prop_exp substs' assigns e2)),l) and const_prop_lexp 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 substs assigns e)) es)) (* or here *) | LEXP_tup les -> re (LEXP_tup (List.map (fun le -> fst (const_prop_lexp substs assigns le)) les)) | LEXP_vector (le,e) -> re (LEXP_vector (fst (const_prop_lexp substs assigns le), fst (const_prop_exp substs assigns e))) | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (fst (const_prop_lexp substs assigns le), fst (const_prop_exp substs assigns e1), fst (const_prop_exp substs assigns e2))) | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map (fun le -> fst (const_prop_lexp substs assigns le)) les)) | LEXP_field (le,id) -> re (LEXP_field (fst (const_prop_lexp substs assigns le), id)) | LEXP_deref e -> re (LEXP_deref (fst (const_prop_exp substs assigns e))) (* Try to evaluate function calls with constant arguments via (interpreter-based) constant folding. Boolean connectives are special-cased to support short-circuiting when one argument has a suitable value (even if the other one is not constant). Moreover, calls to a __size function (in particular generated by sizeof rewriting) with a known-constant return type are replaced by that constant; e.g., (length(op : bits(32)) : int(32)) becomes 32 even if op is not constant. *) and const_prop_try_fn env (id, args) (l, annot) = let exp_orig = E_aux (E_app (id, args), (l, annot)) in let args = List.map replace_constant args in let exp = E_aux (E_app (id, args), (l, annot)) in let rec is_overload_of f = Env.get_overloads f env |> List.exists (fun id' -> Id.compare id id' = 0 || is_overload_of id') in match (string_of_id id, args) with | "and_bool", ([E_aux (E_lit (L_aux (L_false, _)), _) as e_false; _] | [_; E_aux (E_lit (L_aux (L_false, _)), _) as e_false]) -> e_false | "or_bool", ([E_aux (E_lit (L_aux (L_true, _)), _) as e_true; _] | [_; E_aux (E_lit (L_aux (L_true, _)), _) as e_true]) -> e_true | _, [E_aux (E_vector [], _); e'] | _, [e'; E_aux (E_vector [], _)] when is_overload_of (mk_id "append") -> e' | _, _ when List.for_all Constant_fold.is_constant args -> const_fold exp | _, [arg] when is_overload_of (mk_id "__size") -> (match destruct_atom_nexp env (typ_of exp) with | Some (Nexp_aux (Nexp_constant i, _)) -> E_aux (E_lit (mk_lit (L_num i)), (l, annot)) | _ -> exp_orig) | _ -> exp_orig and can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns = let rec check_exp_pat (E_aux (e,(l,annot)) as exp) (P_aux (p,(l',_)) as pat) = match e, p with | _, P_wild -> DoesMatch ([],[]) | _, P_typ (_,p') -> check_exp_pat exp p' | _, P_id id' when pat_id_is_variable env id' -> let exp_typ = typ_of exp in let pat_typ = typ_of_pat pat in let goals = KidSet.diff (tyvars_of_typ pat_typ) (tyvars_of_typ exp_typ) in let unifiers = try Type_check.unify l env goals pat_typ exp_typ with _ -> KBindings.empty in let is_nexp (k,a) = match a with | A_aux (A_nexp n,_) -> Some (k,n) | _ -> None in let kbindings = Util.map_filter is_nexp (KBindings.bindings unifiers) in DoesMatch ([id',exp],kbindings) | E_tuple es, P_tup ps -> let rec check = function | DoesNotMatch -> fun _ -> DoesNotMatch | GiveUp -> fun _ -> GiveUp | DoesMatch (s,ns) -> fun (e,p) -> match check_exp_pat e p with | DoesMatch (s',ns') -> DoesMatch (s@s', ns@ns') | x -> x in List.fold_left check (DoesMatch ([],[])) (List.combine es ps) | E_id id, _ -> (match Env.lookup_id id env with | Enum _ -> begin match p with | P_id id' | P_app (id',[]) -> if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch | _ -> (Reporting.print_err l' "Monomorphisation" "Unexpected kind of pattern for enumeration"; GiveUp) end | _ -> GiveUp) | E_lit (L_aux (lit_e, lit_l)), P_lit (L_aux (lit_p, _)) -> if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch | E_lit (L_aux (lit_e, lit_l)), 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 | E_lit ((L_aux ((L_bin _ | L_hex _), _) as lit)), P_vector _ -> let mk_bitlit lit = E_aux (E_lit lit, (Generated l, mk_tannot env bit_typ no_effect)) in let lits' = List.map mk_bitlit (vector_string_to_bit_list lit) in check_exp_pat (E_aux (E_vector lits', (l, annot))) pat | E_lit _, _ -> (Reporting.print_err l' "Monomorphisation" "Unexpected kind of pattern for literal"; GiveUp) | E_vector es, P_vector ps when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es -> 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],[]) | _, P_aux (P_wild, _) -> DoesMatch ([],[]) | _ -> 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) | E_vector _, P_lit ((L_aux ((L_bin _ | L_hex _), _) as lit)) -> let mk_bitlit lit = P_aux (P_lit lit, (Generated l, mk_tannot env bit_typ no_effect)) in let lits' = List.map mk_bitlit (vector_string_to_bit_list lit) in check_exp_pat exp (P_aux (P_vector lits', (l, annot))) | E_vector _, _ -> (Reporting.print_err l "Monomorphisation" "Unexpected kind of pattern for vector literal"; GiveUp) | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)), P_lit (L_aux (lit_p, _)) -> DoesNotMatch | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)), 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) | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)), _ -> (Reporting.print_err l' "Monomorphisation" "Unexpected kind of pattern for literal"; GiveUp) | E_record _,_ | E_cast (_, E_aux (E_record _, _)),_ -> DoesNotMatch | _ -> GiveUp in let check_pat = check_exp_pat exp0 in let add_ksubst_synonyms env' ksubst = (* The type checker sometimes automatically generates kid synonyms, e.g. in let 'datasize = ... in ... it binds both 'datasize and '_datasize. If we subsitute one, we also want to substitute the other. In order to find synonyms, we consult the environment after the bind (see findpat_generic below). *) let get_synonyms (kid, nexp) = let rec synonyms_of_nc nc = match unaux_constraint nc with | NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var (kid2), _)) when Kid.compare kid kid1 = 0 -> [(kid2, nexp)] | NC_and _ -> List.concat (List.map synonyms_of_nc (constraint_conj nc)) | _ -> [] in List.concat (List.map synonyms_of_nc (Env.get_constraints env')) in ksubst @ List.concat (List.map get_synonyms ksubst) in let rec findpat_generic description assigns = function | [] -> (Reporting.print_err l "Monomorphisation" ("Failed to find a case for " ^ description); None) | (Pat_aux (Pat_when (p,guard,exp),_))::tl -> begin match check_pat p with | DoesNotMatch -> findpat_generic 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 substs assigns guard in match guard with | E_lit (L_aux (L_true,_)) -> let ksubst = add_ksubst_synonyms (env_of exp) ksubst in Some (exp,vsubst,ksubst) | E_lit (L_aux (L_false,_)) -> findpat_generic description assigns tl | _ -> None end | GiveUp -> None end | (Pat_aux (Pat_exp (p,exp),_))::tl -> match check_pat p with | DoesNotMatch -> findpat_generic description assigns tl | DoesMatch (subst,ksubst) -> let ksubst = add_ksubst_synonyms (env_of exp) ksubst in Some (exp,subst,ksubst) | GiveUp -> None in findpat_generic (string_of_exp exp0) assigns cases and can_match exp = let env = Type_check.env_of exp in can_match_with_env env exp in (const_prop_exp, const_prop_pexp) let const_prop target d r = fst (const_props target d r) let const_prop_pexp target d r = snd (const_props target d r) let referenced_vars exp = let open Rewriter in fst (fold_exp { (compute_exp_alg IdSet.empty IdSet.union) with e_ref = (fun id -> IdSet.singleton id, E_ref id) } exp) (* This is intended to remove impossible cases when a type-level constant has been used to fix a property of the architecture. In particular, the current version of the RISC-V model uses constructs like match (width, sizeof(xlen)) { (BYTE, _) => ... ... (DOUBLE, 64) => ... }; and the type checker will replace the sizeof with the literal 32 or 64. This pass will then remove the DOUBLE case. It would be nice to have the full constant propagation above do this kind of thing too... *) let remove_impossible_int_cases _ = let must_keep_case exp (Pat_aux ((Pat_exp (p,_) | Pat_when (p,_,_)),_)) = let rec aux (E_aux (exp,_)) (P_aux (p,_)) = match exp, p with | E_tuple exps, P_tup ps -> List.for_all2 aux exps ps | E_lit (L_aux (lit,_)), P_lit (L_aux (lit',_)) -> lit_match (lit, lit') | _ -> true in aux exp p in let e_case (exp,cases) = E_case (exp, List.filter (must_keep_case exp) cases) in let e_if (cond, e_then, e_else) = match destruct_atom_bool (env_of cond) (typ_of cond) with | Some nc -> if prove __POS__ (env_of cond) nc then unaux_exp e_then else if prove __POS__ (env_of cond) (nc_not nc) then unaux_exp e_else else E_if (cond, e_then, e_else) | _ -> E_if (cond, e_then, e_else) in let open Rewriter in let rewrite_exp _ = fold_exp { id_exp_alg with e_case = e_case; e_if = e_if } in rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp }