diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/monomorphise.ml | 671 | ||||
| -rw-r--r-- | src/process_file.ml | 7 | ||||
| -rw-r--r-- | src/process_file.mli | 4 | ||||
| -rw-r--r-- | src/sail.ml | 12 |
4 files changed, 645 insertions, 49 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index f79c1dc3..74242509 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -11,10 +11,6 @@ let optmap v f = | None -> None | Some v -> Some (f v) -let env_typ_expected l : tannot -> Env.t * typ = function - | None -> raise (Reporting_basic.err_unreachable l "Missing type environment") - | Some (env,ty,_) -> env,ty - 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 *) @@ -392,10 +388,13 @@ let reduce_nexp subst ne = let typ_of_args args = match args with - | [E_aux (_,(l,annot))] -> - snd (env_typ_expected l annot) + | [E_aux (E_tuple args,(_,Some (_,Typ_aux (Typ_exist _,_),_)))] -> + let tys = List.map Type_check.typ_of args in + Typ_aux (Typ_tup tys,Unknown) + | [exp] -> + Type_check.typ_of exp | _ -> - let tys = List.map (fun (E_aux (_,(l,annot))) -> snd (env_typ_expected l annot)) args in + let tys = List.map Type_check.typ_of args in Typ_aux (Typ_tup tys,Unknown) (* Check to see if we need to monomorphise a use of a constructor. Currently @@ -544,7 +543,7 @@ let nexp_subst_exp substs = snd (nexp_subst_fns substs) let bindings_from_pat p = let rec aux_pat (P_aux (p,(l,annot))) = - let env,_ = env_typ_expected l annot in + let env = Type_check.env_of_annot (l, annot) in match p with | P_lit _ | P_wild @@ -664,9 +663,9 @@ let can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases = in findpat_generic checkpat "literal" cases | _ -> None -let can_match (E_aux (_,(l,annot)) as exp0) cases = - let (env,_) = env_typ_expected l annot in - can_match_with_env env exp0 cases +let can_match exp cases = + let env = Type_check.env_of exp in + can_match_with_env env exp cases (* 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 @@ -740,18 +739,6 @@ let try_app (l,ann) (Id_aux (id,_),args) = else None -let try_app_infix (l,ann) (E_aux (e1,ann1)) (Id_aux (id,_)) (E_aux (e2,ann2)) = - let i = match id with Id x -> x | DeIid x -> x in - let new_l = Generated l in - match e1, i, e2 with - | E_lit l1, ("=="|"!="), E_lit l2 -> - let lit b = if b then L_true else L_false in - let lit b = lit (if i = "==" then b else not b) in - (match lit_eq l1 l2 with - | Some b -> Some (E_aux (E_lit (L_aux (lit b,new_l)), (l,ann))) - | None -> None) - | _ -> None - let construct_lit_vector args = let rec aux l = function | [] -> Some (L_aux (L_bin (String.concat "" (List.rev l)),Unknown)) @@ -894,7 +881,7 @@ let split_defs splits defs = let es',assigns = non_det_exp_list es in re (E_nondet es') assigns | E_id id -> - let env,_ = env_typ_expected l annot in + let env = Type_check.env_of_annot (l, annot) in (try match Env.lookup_id id env with | Local (Immutable,_) -> Bindings.find id substs @@ -914,22 +901,13 @@ let split_defs splits defs = re (E_cast (t, e'')) assigns | E_app (id,es) -> let es',assigns = non_det_exp_list es in - let env,_ = env_typ_expected l annot 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 l env (id,es') with - | None -> - (let env,_ = env_typ_expected l annot in - match Env.is_union_constructor id env, refine_constructor refinements l env id es' with - | true, Some exp -> re exp assigns - | _,_ -> re (E_app (id,es')) assigns) + | None -> re (E_app (id,es')) assigns | Some r -> r,assigns) | Some r -> r,assigns) - | E_app_infix (e1,id,e2) -> - let e1',e2',assigns = non_det_exp_2 e1 e2 in - (match try_app_infix (l,annot) e1' id e2' with - | Some exp -> exp,assigns - | None -> re (E_app_infix (e1',id,e2')) assigns) | E_tuple es -> let es',assigns = non_det_exp_list es in re (E_tuple es') assigns @@ -1032,7 +1010,7 @@ let split_defs splits defs = end (* TODO maybe - tuple assignments *) | E_assign (le,e) -> - let env,_ = env_typ_expected l annot in + 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 @@ -1072,11 +1050,13 @@ let split_defs splits defs = re (E_internal_cast (ann,e')) assigns (* TODO: should I substitute or anything here? Is it even used? *) | E_comment_struc e -> re (E_comment_struc e) assigns + + | E_app_infix _ | E_internal_let _ | E_internal_plet _ | E_internal_return _ -> raise (Reporting_basic.err_unreachable l - "Unexpected internal expression encountered in monomorphisation") + ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp)) and const_prop_fexps substs assigns (FES_aux (FES_Fexps (fes,flag), annot)) = FES_aux (FES_Fexps (List.map (const_prop_fexp substs assigns) fes, flag), annot) and const_prop_fexp substs assigns (FE_aux (FE_Fexp (id,e), annot)) = @@ -1146,7 +1126,8 @@ let split_defs splits defs = let split var l annot = let v = string_of_id var in - let env, typ = env_typ_expected l annot in + let env = Type_check.env_of_annot (l, annot) in + let typ = Type_check.typ_of_annot (l, annot) in let typ = Env.expand_synonyms env typ in let Typ_aux (ty,l) = typ in let new_l = Generated l in @@ -1241,8 +1222,6 @@ let split_defs splits defs = optmap (spl p) (fun ps -> List.map (fun (p,sub) -> FP_aux (FP_Fpat (id,p), annot), sub) ps) in - let ipat (i,p) = optmap (spl p) (List.map (fun (p,sub) -> (i,p),sub)) - in match p with | P_lit _ | P_wild @@ -1353,7 +1332,14 @@ let split_defs splits defs = | E_constraint _ -> ea | E_cast (t,e') -> re (E_cast (t, map_exp e')) - | E_app (id,es) -> re (E_app (id,List.map map_exp es)) + | E_app (id,es) -> + let es' = List.map map_exp es in + let env = env_of_annot annot in + begin + match Env.is_union_constructor id env, refine_constructor refinements (fst annot) env id es' with + | true, Some exp -> re exp + | _,_ -> re (E_app (id,es')) + end | E_app_infix (e1,id,e2) -> re (E_app_infix (map_exp e1,id,map_exp e2)) | E_tuple es -> re (E_tuple (List.map map_exp es)) | E_if (e1,e2,e3) -> re (E_if (map_exp e1, map_exp e2, map_exp e3)) @@ -1726,8 +1712,607 @@ let rewrite_size_parameters env (Defs defs) = end -let monomorphise mwords splits defs = - let defs = split_defs splits defs in + +module Analysis = +struct + +type loc = string * int (* filename, line *) + +let string_of_loc (s,l) = s ^ "." ^ string_of_int l + +let id_pair_compare (id,l) (id',l') = + match Id.compare id id' with + | 0 -> compare l l' + | x -> x + +(* Arguments that we might split on *) +module ArgSet = Set.Make (struct + type t = id * loc + let compare = id_pair_compare +end) + +(* Arguments that we should look at in callers *) +module CallerArgSet = Set.Make (struct + type t = id * int + let compare = id_pair_compare +end) + +(* Type variables that we should look at in callers *) +module CallerKidSet = Set.Make (struct + type t = id * kid + let compare (id,kid) (id',kid') = + match Id.compare id id' with + | 0 -> Kid.compare kid kid' + | x -> x +end) + +module FailureSet = Set.Make (struct + type t = Parse_ast.l * string + let compare = compare +end) + +type dependencies = + | Have of ArgSet.t * CallerArgSet.t * CallerKidSet.t + (* args to split inside fn * caller args to split * caller kids that are bitvector parameters *) + | Unknown of Parse_ast.l * string + +let string_of_argset s = + String.concat ", " (List.map (fun (id,l) -> string_of_id id ^ "." ^ string_of_loc l) + (ArgSet.elements s)) + +let string_of_callerset s = + String.concat ", " (List.map (fun (id,arg) -> string_of_id id ^ "." ^ string_of_int arg) + (CallerArgSet.elements s)) + +let string_of_callerkidset s = + String.concat ", " (List.map (fun (id,kid) -> string_of_id id ^ "." ^ string_of_kid kid) + (CallerKidSet.elements s)) + +let string_of_dep = function + | Have (argset,callset,kidset) -> + "Have (" ^ string_of_argset argset ^ "; " ^ string_of_callerset callset ^ "; " ^ + string_of_callerkidset kidset ^ ")" + | Unknown (l,msg) -> "Unknown " ^ msg ^ " at " ^ Reporting_basic.loc_to_string l + +(* Result of analysing the body of a function. The split field gives + the arguments to split based on the body alone, and the failures + field where we couldn't do anything. The other fields are used at + the end for the interprocedural phase. *) + +type result = { + split : ArgSet.t; + failures : FailureSet.t; + (* Dependencies for arguments and type variables of each fn called, so that + if the fn uses one for a bitvector size we can track it back *) + split_on_call : (dependencies list * dependencies KBindings.t) Bindings.t; (* (arguments, kids) per fn *) + split_in_caller : CallerArgSet.t; + kid_in_caller : CallerKidSet.t +} + +let empty = { + split = ArgSet.empty; + failures = FailureSet.empty; + split_on_call = Bindings.empty; + split_in_caller = CallerArgSet.empty; + kid_in_caller = CallerKidSet.empty +} + +let dmerge x y = + match x,y with + | Unknown (l,s), _ -> Unknown (l,s) + | _, Unknown (l,s) -> Unknown (l,s) + | Have (a,c,k), Have (a',c',k') -> + Have (ArgSet.union a a', CallerArgSet.union c c', CallerKidSet.union k k') + +let dempty = Have (ArgSet.empty, CallerArgSet.empty, CallerKidSet.empty) + +let dopt_merge k x y = + match x, y with + | None, _ -> y + | _, None -> x + | Some x, Some y -> Some (dmerge x y) + +let dep_bindings_merge a1 a2 = + Bindings.merge dopt_merge a1 a2 + +let dep_kbindings_merge a1 a2 = + KBindings.merge dopt_merge a1 a2 + +let call_kid_merge k x y = + match x, y with + | None, x -> x + | x, None -> x + | Some d, Some d' -> Some (dmerge d d') + +let call_arg_merge k args args' = + match args, args' with + | None, x -> x + | x, None -> x + | Some (args,kdep), Some (args',kdep') + -> Some (List.map2 dmerge args args', KBindings.merge call_kid_merge kdep kdep') + +let merge rs rs' = { + split = ArgSet.union rs.split rs'.split; + failures = FailureSet.union rs.failures rs'.failures; + split_on_call = Bindings.merge call_arg_merge rs.split_on_call rs'.split_on_call; + split_in_caller = CallerArgSet.union rs.split_in_caller rs'.split_in_caller; + kid_in_caller = CallerKidSet.union rs.kid_in_caller rs'.kid_in_caller +} + +type env = { + var_deps : dependencies Bindings.t; + kid_deps : dependencies KBindings.t; + control_deps : dependencies +} + +let rec split3 = function + | [] -> [],[],[] + | ((h1,h2,h3)::t) -> + let t1,t2,t3 = split3 t in + (h1::t1,h2::t2,h3::t3) + +let kids_bound_by_pat pat = + let open Rewriter in + 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) + +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 } + +(* 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 + arguments so that we can find dependencies for existentially bound sizes. *) + +let deps_of_tyvars kid_deps arg_deps kids = + let check kid deps = + match KBindings.find kid kid_deps with + | deps' -> dmerge deps deps' + | exception Not_found -> + match kid with + | Kid_aux (Var kidstr, l) -> + let unknown = Unknown (l, "Unknown type variable " ^ string_of_kid kid) in + (* Tyvars from existentials in arguments have a special format *) + if String.length kidstr > 5 && String.sub kidstr 0 4 = "'arg" then + try + let i = String.index kidstr '#' in + let n = String.sub kidstr 4 (i-4) in + let arg = int_of_string n in + List.nth arg_deps arg + with Not_found | Failure _ -> unknown + else unknown + in + KidSet.fold check kids dempty + +let deps_of_nexp kid_deps arg_deps nexp = + let kids = nexp_frees nexp in + deps_of_tyvars kid_deps arg_deps kids + +let rec deps_of_nc kid_deps (NC_aux (nc,l)) = + match nc with + | NC_equal (nexp1,nexp2) + | NC_bounded_ge (nexp1,nexp2) + | NC_bounded_le (nexp1,nexp2) + | NC_not_equal (nexp1,nexp2) + -> dmerge (deps_of_nexp kid_deps [] nexp1) (deps_of_nexp kid_deps [] nexp2) + | NC_set (kid,_) -> + (match KBindings.find kid kid_deps with + | deps -> deps + | exception Not_found -> Unknown (l, "Unknown type variable " ^ string_of_kid kid)) + | NC_or (nc1,nc2) + | NC_and (nc1,nc2) + -> dmerge (deps_of_nc kid_deps nc1) (deps_of_nc kid_deps nc2) + | NC_true + | NC_false + -> dempty + +let deps_of_typ kid_deps arg_deps typ = + deps_of_tyvars kid_deps arg_deps (tyvars_of_typ typ) + +let deps_of_uvar kid_deps arg_deps = function + | U_nexp nexp -> deps_of_nexp kid_deps arg_deps nexp + | U_order _ + | U_effect _ -> dempty + | U_typ typ -> deps_of_typ kid_deps arg_deps typ + +(* Takes an environment of dependencies on vars, type vars, and flow control, + and dependencies on mutable variables. The latter are quite conservative, + we currently drop variables assigned inside loops, for example. *) + +let rec analyse_exp 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 + IdSet.fold + (fun id asn -> + Bindings.add id (Unknown (l, string_of_id id ^ message)) asn) + assigned assigns + in + let non_det es = + let assigns = remove_assigns es " assigned in non-deterministic expressions" in + let deps, _, rs = split3 (List.map (analyse_exp 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 deps, assigns, r = + match e with + | E_block es -> + let rec aux assigns = function + | [] -> (dempty, assigns, empty) + | [e] -> analyse_exp env assigns e + | e::es -> + let _, assigns, r' = analyse_exp env assigns e in + let d, assigns, r = aux assigns es in + d, assigns, merge r r' + in + aux assigns es + | E_nondet es -> + let _, assigns, r = non_det es in + (dempty, assigns, r) + | E_id id -> + begin + match Bindings.find id env.var_deps with + | args -> (dmerge env.control_deps args,assigns,empty) + | exception Not_found -> + match Bindings.find id assigns with + | args -> (dmerge env.control_deps 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 + | 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_cast (_,e) -> analyse_exp env assigns e + | E_app (id,args) -> + let deps, assigns, r = non_det args in + let kid_inst = instantiation_of exp in + let kid_deps = KBindings.map (deps_of_uvar env.kid_deps deps) kid_inst in + let r' = { empty with split_on_call = Bindings.singleton id (deps, kid_deps) } in + (merge_deps deps, assigns, merge r r') + | E_tuple es + | E_list es -> + let deps, assigns, r = non_det es in + (merge_deps deps, assigns, r) + | E_if (e1,e2,e3) -> + let d1,assigns,r1 = analyse_exp env assigns e1 in + let env' = { env with control_deps = dmerge env.control_deps d1 } in + let d2,a2,r2 = analyse_exp env' assigns e2 in + let d3,a3,r3 = analyse_exp env' assigns e3 in + (dmerge d2 d3, dep_bindings_merge a2 a3, merge r1 (merge r2 r3)) + | E_loop (_,e1,e2) -> + let assigns = remove_assigns [e1;e2] " assigned in a loop" in + let d1,a1,r1 = analyse_exp env assigns e1 in + let env' = { env with control_deps = dmerge env.control_deps d1 } in + let d2,a2,r2 = analyse_exp 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 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 env' assigns body in + (dempty, assigns, merge r1 r2) + | E_vector es -> + let ds, assigns, r = non_det es in + (merge_deps ds, assigns, r) + | E_vector_access (e1,e2) + | E_vector_append (e1,e2) + | E_cons (e1,e2) -> + let ds, assigns, r = non_det [e1;e2] in + (merge_deps ds, assigns, r) + | E_vector_subrange (e1,e2,e3) + | E_vector_update (e1,e2,e3) -> + let ds, assigns, r = non_det [e1;e2;e3] in + (merge_deps ds, assigns, r) + | E_vector_update_subrange (e1,e2,e3,e4) -> + let ds, assigns, r = non_det [e1;e2;e3;e4] in + (merge_deps ds, assigns, r) + | E_record (FES_aux (FES_Fexps (fexps,_),_)) -> + let es = List.map (function (FE_aux (FE_Fexp (_,e),_)) -> e) fexps in + let ds, assigns, r = non_det es in + (merge_deps ds, assigns, r) + | E_record_update (e,FES_aux (FES_Fexps (fexps,_),_)) -> + let es = List.map (function (FE_aux (FE_Fexp (_,e),_)) -> e) fexps in + let ds, assigns, r = non_det (e::es) in + (merge_deps ds, assigns, r) + | E_field (e,_) -> analyse_exp env assigns e + | E_case (e,cases) -> + let deps,assigns,r = analyse_exp env assigns e in + let analyse_case (Pat_aux (pexp,_)) = + match pexp with + | Pat_exp (pat,e1) -> + let env = update_env env deps pat in + analyse_exp env assigns e1 + | Pat_when (pat,e1,e2) -> + let env = update_env env deps pat in + let d1,assigns,r1 = analyse_exp env assigns e1 in + let d2,assigns,r2 = analyse_exp env assigns e2 in + (dmerge d1 d2, assigns, merge r1 r2) + in + let ds,assigns,rs = split3 (List.map analyse_case cases) in + (merge_deps (deps::ds), + List.fold_left dep_bindings_merge Bindings.empty assigns, + List.fold_left merge r rs) + | E_let (LB_aux (LB_val (pat,e1),_),e2) -> + let d1,assigns,r1 = analyse_exp env assigns e1 in + let env = update_env env d1 pat in + let d2,assigns,r2 = analyse_exp env assigns e2 in + (d2,assigns,merge r1 r2) + | E_assign (lexp,e1) -> + let d1,assigns,r1 = analyse_exp env assigns e1 in + let assigns,r2 = analyse_lexp env assigns d1 lexp in + (dempty, assigns, merge r1 r2) + | E_sizeof nexp -> + (deps_of_nexp env.kid_deps [] nexp, assigns, empty) + | E_return e + | E_exit e + | E_throw e -> + let _, _, r = analyse_exp env assigns e in + (Unknown (l,"non-local flow"), Bindings.empty, r) + | E_try (e,cases) -> + let deps,_,r = analyse_exp env assigns e in + let assigns = remove_assigns [e] " assigned in try expression" in + let analyse_handler (Pat_aux (pexp,_)) = + match pexp with + | Pat_exp (pat,e1) -> + let env = update_env env (Unknown (l,"Exception")) pat in + analyse_exp env assigns e1 + | Pat_when (pat,e1,e2) -> + let env = update_env env (Unknown (l,"Exception")) pat in + let d1,assigns,r1 = analyse_exp env assigns e1 in + let d2,assigns,r2 = analyse_exp env assigns e2 in + (dmerge d1 d2, assigns, merge r1 r2) + in + let ds,assigns,rs = split3 (List.map analyse_handler cases) in + (merge_deps (deps::ds), + List.fold_left dep_bindings_merge Bindings.empty assigns, + List.fold_left merge r rs) + | E_assert (e1,_) -> analyse_exp env assigns e1 + + | E_app_infix _ + | E_internal_cast _ + | E_internal_exp _ + | E_sizeof_internal _ + | E_internal_exp_user _ + | E_comment _ + | E_comment_struc _ + | E_internal_plet _ + | E_internal_return _ + -> raise (Reporting_basic.err_unreachable l + ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp)) + + | E_internal_let (lexp,e1,e2) -> + (* Really we ought to remove the assignment after e2 *) + let d1,assigns,r1 = analyse_exp env assigns e1 in + let assigns,r' = analyse_lexp env assigns d1 lexp in + let d2,assigns,r2 = analyse_exp env assigns e2 in + (dempty, assigns, merge r1 (merge r' r2)) + | E_constraint nc -> + (deps_of_nc env.kid_deps nc, assigns, empty) + in + let r = + (* Check for bitvector types with parametrised sizes *) + match annot with + | None -> r + | Some (tenv,typ,_) -> + (* TODO: existential wrappers *) + let typ = Env.expand_synonyms tenv typ in + if is_bitvector_typ typ then + let _,size,_,_ = vector_typ_args_of typ in + match deps_of_nexp env.kid_deps [] size with + | Have (args,caller,caller_kids) -> + { r with + split = ArgSet.union r.split args; + split_in_caller = CallerArgSet.union r.split_in_caller caller; + kid_in_caller = CallerKidSet.union r.kid_in_caller caller_kids + } + | Unknown (l,msg) -> + { r with + failures = + FailureSet.add (l,"Unable to monomorphise " ^ string_of_nexp size ^ ": " ^ msg) + r.failures } + else + r + in (deps, assigns, r) + + +and analyse_lexp env assigns deps (LEXP_aux (lexp,_)) = + (* TODO: maybe subexps and sublexps should be non-det (and in const_prop_lexp, too?) *) + match lexp with + | LEXP_id id + | LEXP_cast (_,id) -> + Bindings.add id deps assigns, empty + | LEXP_memory (id,es) -> + let _, assigns, r = analyse_exp env assigns (E_aux (E_tuple es,(Unknown,None))) in + assigns, r + | LEXP_tup lexps -> + List.fold_left (fun (assigns,r) lexp -> + let assigns,r' = analyse_lexp env assigns deps lexp + in assigns,merge r r') (assigns,empty) lexps + | LEXP_vector (lexp,e) -> + let _, assigns, r1 = analyse_exp env assigns e in + let assigns, r2 = analyse_lexp env assigns deps lexp in + assigns, merge r1 r2 + | LEXP_vector_range (lexp,e1,e2) -> + let _, assigns, r1 = analyse_exp env assigns e1 in + let _, assigns, r2 = analyse_exp env assigns e2 in + let assigns, r3 = analyse_lexp env assigns deps lexp in + assigns, merge r3 (merge r1 r2) + | LEXP_field (lexp,_) -> analyse_lexp env assigns deps lexp + + +let translate_id (Id_aux (_,l) as id) = + let rec aux l = + match l with + | Range (pos,_) -> id,(pos.Lexing.pos_fname,pos.Lexing.pos_lnum) + | Generated l -> aux l + | _ -> + raise (Reporting_basic.err_general l ("Unable to give location for " ^ string_of_id id)) + in aux l + +let initial_env fn_id (TypQ_aux (tq,_)) pat = + let pats = + match pat with + | P_aux (P_tup pats,_) -> pats + | _ -> [pat] + in + let arg i pat = + let rec aux (P_aux (p,(l,_))) = + let of_list pats = + let ss,vs,ks = split3 (List.map aux pats) in + let s = List.fold_left ArgSet.union ArgSet.empty ss in + let v = List.fold_left dep_bindings_merge Bindings.empty vs in + let k = List.fold_left dep_kbindings_merge KBindings.empty ks in + s,v,k + in + match p with + | P_lit _ + | P_wild + -> ArgSet.empty,Bindings.empty,KBindings.empty + | P_as (pat,id) -> + let s,v,k = aux pat in + let id' = translate_id id in + ArgSet.add id' s, Bindings.add id (Have (ArgSet.singleton id',CallerArgSet.empty,CallerKidSet.empty)) v,k + | P_typ (_,pat) -> aux pat + | P_id id -> + let id' = translate_id id in + let s = ArgSet.singleton id' in + s, Bindings.singleton id (Have (s,CallerArgSet.empty,CallerKidSet.empty)), KBindings.empty + | P_var (pat,kid) -> + let s,v,k = aux pat in + s,v,KBindings.add kid (Have (ArgSet.empty,CallerArgSet.singleton (fn_id,i),CallerKidSet.empty)) k + | P_app (_,pats) -> of_list pats + | P_record (fpats,_) -> of_list (List.map (fun (FP_aux (FP_Fpat (_,p),_)) -> p) fpats) + | P_vector pats + | P_vector_concat pats + | P_tup pats + | P_list pats + -> of_list pats + | P_cons (p1,p2) -> of_list [p1;p2] + in aux pat + in + let quant k = function + | QI_aux (QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_,kid)),_)),_) -> + KBindings.add kid (Have (ArgSet.empty,CallerArgSet.empty,CallerKidSet.singleton (fn_id,kid))) k + | QI_aux (QI_const _,_) -> k + in + let kid_quant_deps = + match tq with + | TypQ_no_forall -> KBindings.empty + | TypQ_tq qs -> List.fold_left quant KBindings.empty qs + in + 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 } + +let print_result r = + let _ = print_endline (" splits: " ^ string_of_argset r.split) in + let print_kbinding kid dep = + let _ = print_endline (" " ^ string_of_kid kid ^ ": " ^ string_of_dep dep) in + () + in + let print_binding id (deps,kdep) = + let _ = print_endline (" " ^ string_of_id id ^ ":") in + let _ = List.iter (fun dep -> print_endline (" " ^ string_of_dep dep)) deps in + let _ = KBindings.iter print_kbinding kdep in + () + in + let _ = print_endline " split_on_call: " in + let _ = Bindings.iter print_binding r.split_on_call in + let _ = print_endline (" split_in_caller: " ^ string_of_callerset r.split_in_caller) in + let _ = print_endline (" kid_in_caller: " ^ string_of_callerkidset r.kid_in_caller) in + () + +let analyse_funcl debug tenv (FCL_aux (FCL_Funcl (id,pat,body),_)) = + let (tq,_) = Env.get_val_spec id tenv in + let aenv = initial_env id tq pat in + let _,_,r = analyse_exp aenv Bindings.empty body in + let _ = + if debug > 2 then + (print_endline (string_of_id id); + print_result r) + else () + in r + +let analyse_def debug env = function + | DEF_fundef (FD_aux (FD_function (_,_,_,funcls),_)) -> + List.fold_left (fun r f -> merge r (analyse_funcl debug env f)) empty funcls + + | _ -> empty + +let analyse_defs debug env (Defs defs) = + let r = List.fold_left (fun r d -> merge r (analyse_def debug env d)) empty defs in + + (* Resolve the interprocedural dependencies *) + + let rec chase_deps = function + | Have (splits, caller_args, caller_kids) -> + let splits,fails = CallerArgSet.fold add_arg caller_args (splits,FailureSet.empty) in + let splits,fails = CallerKidSet.fold add_kid caller_kids (splits,fails) in + splits, fails + | Unknown (l,msg) -> + ArgSet.empty , FailureSet.singleton (l,("Unable to monomorphise dependency: " ^ msg)) + and chase_kid_caller (id,kid) = + match Bindings.find id r.split_on_call with + | (_,kid_deps) -> begin + match KBindings.find kid kid_deps with + | deps -> chase_deps deps + | exception Not_found -> ArgSet.empty,FailureSet.empty + end + | exception Not_found -> ArgSet.empty,FailureSet.empty + and chase_arg_caller (id,i) = + match Bindings.find id r.split_on_call with + | (arg_deps,_) -> chase_deps (List.nth arg_deps i) + | exception Not_found -> ArgSet.empty,FailureSet.empty + and add_arg arg (splits,fails) = + let splits',fails' = chase_arg_caller arg in + ArgSet.union splits splits', FailureSet.union fails fails' + and add_kid k (splits,fails) = + let splits',fails' = chase_kid_caller k in + ArgSet.union splits splits', FailureSet.union fails fails' + in + let _ = if debug > 1 then print_result r else () in + let splits,fails = CallerArgSet.fold add_arg r.split_in_caller (r.split,r.failures) in + let splits,fails = CallerKidSet.fold add_kid r.kid_in_caller (splits,fails) in + let _ = + if debug > 0 then + (print_endline "Final splits:"; + print_endline (string_of_argset splits)) + else () + in + let _ = + if FailureSet.is_empty fails then () else + begin + FailureSet.iter (fun (l,msg) -> Reporting_basic.print_err false false l "Monomorphisation" msg) + fails; + raise (Reporting_basic.err_general Unknown "Unable to monomorphise program") + end + in splits + +let argset_to_list splits = + let l = ArgSet.elements splits in + let argelt (id,(file,loc)) = ((file,loc),string_of_id id) in + List.map argelt l +end + + +let monomorphise mwords auto debug_analysis splits env defs = + let new_splits = + if auto + then Analysis.argset_to_list (Analysis.analyse_defs 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 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/process_file.ml b/src/process_file.ml index 5d362af2..ab18f3ad 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -119,9 +119,12 @@ let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.E (ast, env) let opt_ddump_raw_mono_ast = ref false +let opt_dmono_analysis = ref 0 +let opt_auto_mono = ref false -let monomorphise_ast locs ast = - let ast = Monomorphise.monomorphise (!opt_lem_mwords) locs ast in +let monomorphise_ast locs type_env ast = + let ast = Monomorphise.monomorphise (!opt_lem_mwords) (!opt_auto_mono) (!opt_dmono_analysis) + 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 diff --git a/src/process_file.mli b/src/process_file.mli index 4bf48aec..afde469e 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -43,7 +43,7 @@ val parse_file : string -> Parse_ast.defs val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs val check_ast: unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t -val monomorphise_ast : ((string * int) * string) list -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t +val monomorphise_ast : ((string * int) * string) list -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs @@ -61,6 +61,8 @@ val opt_ddump_tc_ast : bool ref val opt_ddump_rewrite_ast : ((string * int) option) ref 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 type out_type = | Lem_ast_out diff --git a/src/sail.ml b/src/sail.ml index 68dbcdbe..e7e965ba 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -114,6 +114,12 @@ let options = Arg.align ([ ( "-ddump_raw_mono_ast", Arg.Set opt_ddump_raw_mono_ast, " (debug) dump the monomorphised ast before type-checking"); + ( "-dmono_analysis", + Arg.Set_int opt_dmono_analysis, + " (debug) dump information about monomorphisation analysis: 0 silent, 3 max"); + ( "-auto_mono", + Arg.Set opt_auto_mono, + " automatically infer how to monomorphise code"); ( "-verbose", Arg.Set opt_print_verbose, " (debug) pretty-print the input to standard output"); @@ -168,9 +174,9 @@ let main() = let (ast, type_envs) = check_ast ast in let (ast, type_envs) = - match !opt_mono_split with - | [] -> ast, type_envs - | locs -> monomorphise_ast locs ast + match !opt_mono_split, !opt_auto_mono with + | [], false -> ast, type_envs + | locs, _ -> monomorphise_ast locs type_envs ast in let ast = |