From fcb7b8dff4fb0ae308d900b7e53bfba56850cdfd Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 14 Dec 2017 16:02:18 +0000 Subject: Fix all compiler warning except in lem pretty printer and monomorphisation --- Makefile | 2 +- src/pretty_print_common.ml | 46 +++++---------------------------------------- src/pretty_print_lem_ast.ml | 35 +++++++++------------------------- src/pretty_print_sail.ml | 40 +++++++++------------------------------ src/rewriter.ml | 27 +++++++------------------- src/rewriter.mli | 1 + src/rewrites.ml | 44 ++++++++++++++++++++++++++----------------- src/spec_analysis.ml | 4 ++++ 8 files changed, 63 insertions(+), 136 deletions(-) diff --git a/Makefile b/Makefile index b84e0d22..fe7206f7 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ all: sail sail: - $(MAKE) -C src + $(MAKE) -C src sail ln -f -s src/sail.native sail isail: diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index 98efa4ce..254af4d7 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -102,6 +102,8 @@ let doc_effect (BE_aux (e,_)) = | BE_wmem -> "wmem" | BE_wmv -> "wmv" | BE_wmvt -> "wmvt" + | BE_lset -> "lset" + | BE_lret -> "lret" | BE_eamem -> "eamem" | BE_exmem -> "exmem" | BE_barr -> "barr" @@ -133,51 +135,12 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = | Typ_tup typs -> parens (separate_map comma_sp app_typ typs) | _ -> app_typ ty and app_typ ((Typ_aux (t, _)) as ty) = match t with - (*TODO Need to un bid-endian-ify this here, since both can transform to the shorthand, especially with <: and :> *) - (* Special case simple vectors to improve legibility - * XXX we assume big-endian here, as usual *) -(* - | Typ_app(Id_aux (Id "vector", _), [ - Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); - Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _); - Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_inc, _)), _); - Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> - (doc_id id) ^^ (brackets (if n = 0 then doc_int m else doc_op colon (doc_int n) (doc_int (n+m-1)))) - | Typ_app(Id_aux (Id "vector", _), [ - Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); - Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _); - Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); - Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> - (doc_id id) ^^ (brackets (if n = m-1 then doc_int m else doc_op colon (doc_int n) (doc_int (m+1 -n)))) - | Typ_app(Id_aux (Id "vector", _), [ - Typ_arg_aux(Typ_arg_nexp - (Nexp_aux(Nexp_minus (Nexp_aux(Nexp_constant n, _), - Nexp_aux(Nexp_constant 1, _)),_)),_); - Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _); - Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); - Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> - (doc_id id) ^^ (brackets (if n = m then doc_int m else doc_op colon (doc_int m) (doc_int (n-1)))) - | Typ_app(Id_aux (Id "vector", _), [ - Typ_arg_aux(Typ_arg_nexp - (Nexp_aux(Nexp_minus (n', Nexp_aux((Nexp_constant 1), _)),_) as n_n),_); - Typ_arg_aux(Typ_arg_nexp m_nexp, _); - Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); - Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> - (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n))) - | Typ_app(Id_aux (Id "vector", _), [ - Typ_arg_aux(Typ_arg_nexp - (Nexp_aux(Nexp_sum (n', Nexp_aux((Nexp_constant -1), _)),_) as n_n),_); - Typ_arg_aux(Typ_arg_nexp m_nexp, _); - Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); - Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> - (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n))) - *) | Typ_app(Id_aux (Id "range", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); Typ_arg_aux(Typ_arg_nexp m, _);]) -> (squarebars (if Big_int.equal n Big_int.zero then nexp m else doc_op colon (doc_int n) (nexp m))) | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> - (squarecolons (nexp n)) + (squarecolons (nexp n)) | Typ_app(id,args) -> (* trailing space to avoid >> token in case of nested app types *) (doc_id id) ^^ (angles (separate_map comma_sp doc_typ_arg args)) ^^ space @@ -185,7 +148,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = and atomic_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_id id -> doc_id id | Typ_var v -> doc_var v - | Typ_app _ | Typ_tup _ | Typ_fn _ -> + | Typ_app _ | Typ_tup _ | Typ_fn _ | Typ_exist _ -> (* exhaustiveness matters here to avoid infinite loops * if we add a new Typ constructor *) group (parens (typ ty)) @@ -219,6 +182,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_var v -> doc_var v | Nexp_id i -> braces (doc_id i) + | Nexp_app (op, args) -> doc_id op ^^ parens (separate_map (comma ^^ space) nexp args) | Nexp_constant i -> if Big_int.less i Big_int.zero then parens(doc_int i) else doc_int i | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _-> group (parens (nexp ne)) diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 110c0b31..bcf997d4 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -150,6 +150,7 @@ and pp_format_nexp_lem (Nexp_aux(n,l)) = (match n with | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")" | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")" + | Nexp_app(op,args) -> "(Nexp_app [" ^ Util.string_of_list ", " pp_format_nexp_lem args ^ "])" | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum Big_int.to_string i) ^ ")" | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")" @@ -406,6 +407,9 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) = | E_case(exp,pexps) -> fprintf ppf "@[<0>(E_aux (E_case %a [%a]) (%a, %a))@]" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot + | E_try(exp,pexps) -> + fprintf ppf "@[<0>(E_aux (E_try %a [%a]) (%a, %a))@]" + pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (E_let %a %a) (%a, %a))@]" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (E_assign %a %a) (%a, %a))@]" @@ -416,30 +420,12 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) = fprintf ppf "@[<0>(E_aux (E_constraint %a) (%a, %a))@]" pp_lem_nexp_constraint nc pp_lem_l l pp_annot annot | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot + | E_throw exp -> + fprintf ppf "@[<0>(E_aux (E_throw %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot | E_return exp -> fprintf ppf "@[<0>(E_aux (E_return %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot | E_assert(c,msg) -> fprintf ppf "@[<0>(E_aux (E_assert %a %a) (%a, %a))@]" pp_lem_exp c pp_lem_exp msg pp_lem_l l pp_annot annot - (* - | E_internal_exp ((l, Base((_,t),_,_,_,_,bindings))) -> - (*TODO use bindings where appropriate*) - (match t.t with - | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) - | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> - (match r.nexp with - | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" - kwd (lemnum string_of_int (Big_int.to_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) - | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]" - kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) - | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length")) - | Tapp("implicit",[TA_nexp r]) -> - (match r.nexp with - | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" - kwd (lemnum string_of_int (Big_int.to_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) - | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]" - kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) - | _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const")) - | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given non-vector or implicit")*) | E_comment _ | E_comment_struc _ -> fprintf ppf "@[(E_aux (E_lit (L_aux L_unit %a)) (%a,%a))@]" pp_lem_l l pp_lem_l l pp_annot annot | E_internal_cast _ | E_internal_exp _ -> @@ -455,6 +441,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) = | E_internal_plet (pat,exp1,exp2) -> fprintf ppf "@[<0>(E_aux (E_internal_plet %a %a %a) (%a, %a))@]" pp_lem_pat pat pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_l l pp_annot annot + | E_internal_value _ -> raise (Reporting_basic.err_unreachable l "Found internal_value") in print_e ppf e @@ -500,12 +487,8 @@ let pp_lem_default ppf (DT_aux(df,l)) = (* FIXME *) let pp_lem_spec ppf (VS_aux(v,(l,annot))) = - let print_spec ppf v = - match v with - | VS_val_spec(ts,id,ext_opt,is_cast) -> - (* FIXME: None *) - fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) None pp_bool_lem is_cast - | _ -> failwith "Invalid valspec" + let print_spec ppf (VS_val_spec(ts, id, ext_opt, is_cast)) = + fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) None pp_bool_lem is_cast in fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 8302c32d..b7cd3761 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -347,27 +347,6 @@ let doc_exp, doc_let = | E_app_infix(l,op,r) -> failwith ("unexpected app_infix operator " ^ (pp_format_id op)) (* doc_op (doc_id op) (exp l) (exp r) *) - | E_comment s -> comment (string s) - | E_comment_struc e -> comment (exp e) - (* - | E_internal_exp((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings, and other params*) - (match t.t with - | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) - | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> - (match r.nexp with - | Nvar v -> utf8string v - | Nconst bi -> utf8string (Big_int.Big_int.to_string bi) - | _ -> raise (Reporting_basic.err_unreachable l - ("Internal exp given vector without known length, instead given " ^ n_to_string r))) - | Tapp("implicit",[TA_nexp r]) -> - (match r.nexp with - | Nconst bi -> utf8string (Big_int.Big_int.to_string bi) - | Nvar v -> utf8string v - | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const")) - | _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t))) - | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away")) - | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false - *) | E_internal_return exp1 -> separate space [string "internal_return"; exp exp1] | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr) @@ -415,16 +394,14 @@ let doc_default (DT_aux(df,_)) = match df with | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id] | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord] -let doc_spec (VS_aux(v,_)) = match v with - | VS_val_spec(ts,id,ext_opt,is_cast) -> - let cast_pp = if is_cast then [string "cast"] else [] in - (* This sail syntax only supports a single extern name, so just use the ocaml version *) - let extern_kwd_pp, id_pp = match ext_opt "ocaml" with - | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext))) - | None -> [], doc_id id - in - separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp]) - | _ -> failwith "Invalid valspec" +let doc_spec (VS_aux (VS_val_spec (ts, id, ext_opt, is_cast), _)) = + let cast_pp = if is_cast then [string "cast"] else [] in + (* This sail syntax only supports a single extern name, so just use the ocaml version *) + let extern_kwd_pp, id_pp = match ext_opt "ocaml" with + | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext))) + | None -> [], doc_id id + in + separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp]) let doc_namescm (Name_sect_aux(ns,_)) = match ns with | Name_sect_none -> empty @@ -555,6 +532,7 @@ let rec doc_def def = group (match def with | DEF_comm (DC_comm s) -> comment (string s) | DEF_comm (DC_comm_struct d) -> comment (doc_def d) | DEF_fixity _ -> empty + | DEF_internal_mutrec _ -> failwith "Cannot print internal mutrec" ) ^^ hardline let doc_defs (Defs(defs)) = diff --git a/src/rewriter.ml b/src/rewriter.ml index 468b3a84..a639dd3f 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -130,11 +130,11 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with | E_record_update(e,fexps) -> union_effects (effect_of e) (effect_of_fexps fexps) | E_field (e,_) -> effect_of e - | E_case (e,pexps) -> + | E_case (e,pexps) | E_try (e,pexps) -> List.fold_left union_effects (effect_of e) (List.map effect_of_pexp pexps) | E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e) | E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e) - | E_exit e -> union_effects eff (effect_of e) + | E_exit e | E_throw e -> union_effects eff (effect_of e) | E_return e -> union_effects eff (effect_of e) | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect | E_assert (c,m) -> union_effects eff (union_eff_exps [c; m]) @@ -147,6 +147,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with (union_effects (effect_of e1) (effect_of e2)) | E_internal_plet (_,e1,e2) -> union_effects (effect_of e1) (effect_of e2) | E_internal_return e1 -> effect_of e1 + | E_internal_value v -> no_effect in E_aux (e, (l, Some (env, typ, effsum))) | None -> @@ -205,24 +206,6 @@ let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with | None -> LB_aux (lb, (l, None)) -let effectful_effs = function - | Effect_aux (Effect_set effs, _) -> - List.exists - (fun (BE_aux (be,_)) -> - match be with - | BE_nondet | BE_unspec | BE_undef | BE_lset -> false - | _ -> true - ) effs - | _ -> true - -let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux)) -let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp)) - -(* let id_to_string (Id_aux(id,l)) = - match id with - | Id(s) -> s - | DeIid(s) -> s *) - let explode s = let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in exp (String.length s - 1) [] @@ -526,6 +509,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_internal_let : 'lexp * 'exp * 'exp -> 'exp_aux ; e_internal_plet : 'pat * 'exp * 'exp -> 'exp_aux ; e_internal_return : 'exp -> 'exp_aux + ; e_internal_value : Value.value -> 'exp_aux ; e_aux : 'exp_aux * 'a annot -> 'exp ; lEXP_id : id -> 'lexp_aux ; lEXP_memory : id * 'exp list -> 'lexp_aux @@ -600,6 +584,7 @@ let rec fold_exp_aux alg = function | E_internal_plet (pat,e1,e2) -> alg.e_internal_plet (fold_pat alg.pat_alg pat, fold_exp alg e1, fold_exp alg e2) | E_internal_return e -> alg.e_internal_return (fold_exp alg e) + | E_internal_value v -> alg.e_internal_value v and fold_exp alg (E_aux (exp_aux,annot)) = alg.e_aux (fold_exp_aux alg exp_aux, annot) and fold_lexp_aux alg = function | LEXP_id id -> alg.lEXP_id id @@ -670,6 +655,7 @@ let id_exp_alg = ; e_internal_let = (fun (lexp, e2, e3) -> E_internal_let (lexp,e2,e3)) ; e_internal_plet = (fun (pat, e1, e2) -> E_internal_plet (pat,e1,e2)) ; e_internal_return = (fun e -> E_internal_return e) + ; e_internal_value = (fun v -> E_internal_value v) ; e_aux = (fun (e,annot) -> E_aux (e,annot)) ; lEXP_id = (fun id -> LEXP_id id) ; lEXP_memory = (fun (id,es) -> LEXP_memory (id,es)) @@ -771,6 +757,7 @@ let compute_exp_alg bot join = ; e_internal_plet = (fun ((vp,pat), (v1,e1), (v2,e2)) -> (join_list [vp;v1;v2], E_internal_plet (pat,e1,e2))) ; e_internal_return = (fun (v,e) -> (v, E_internal_return e)) + ; e_internal_value = (fun v -> (bot, E_internal_value v)) ; e_aux = (fun ((v,e),annot) -> (v, E_aux (e,annot))) ; lEXP_id = (fun id -> (bot, LEXP_id id)) ; lEXP_memory = (fun (id,es) -> split_join (fun es -> LEXP_memory (id,es)) es) diff --git a/src/rewriter.mli b/src/rewriter.mli index 09dddb95..faa6a81a 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -145,6 +145,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_internal_let : 'lexp * 'exp * 'exp -> 'exp_aux ; e_internal_plet : 'pat * 'exp * 'exp -> 'exp_aux ; e_internal_return : 'exp -> 'exp_aux + ; e_internal_value : Value.value -> 'exp_aux ; e_aux : 'exp_aux * 'a annot -> 'exp ; lEXP_id : id -> 'lexp_aux ; lEXP_memory : id * 'exp list -> 'lexp_aux diff --git a/src/rewrites.ml b/src/rewrites.ml index 2b5df2a2..8c0526fe 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -102,7 +102,6 @@ let effectful_effs = function | BE_nondet | BE_unspec | BE_undef | BE_lset -> false | _ -> true ) effs - | _ -> true let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux)) let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp)) @@ -366,6 +365,7 @@ let rewrite_sizeof (Defs defs) = ; e_internal_let = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_internal_let (lexp,e2,e3), E_internal_let (lexp',e2',e3'))) ; e_internal_plet = (fun (pat, (e1,e1'), (e2,e2')) -> (E_internal_plet (pat,e1,e2), E_internal_plet (pat,e1',e2'))) ; e_internal_return = (fun (e,e') -> (E_internal_return e, E_internal_return e')) + ; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v)) ; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot))) ; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id)) ; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es'))) @@ -942,6 +942,7 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) = | P_wild -> raise (Reporting_basic.err_unreachable l "pat_to_exp given wildcard pattern") | P_as (pat,id) -> rewrap (E_id id) + | P_var (pat, _) -> pat_to_exp pat | P_typ (_,pat) -> pat_to_exp pat | P_id id -> rewrap (E_id id) | P_app (id,pats) -> rewrap (E_app (id, List.map pat_to_exp pats)) @@ -1030,7 +1031,7 @@ let bitwise_and_exp exp1 exp2 = let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with | P_lit _ | P_wild | P_id _ -> false -| P_as (pat,_) | P_typ (_,pat) -> contains_bitvector_pat pat +| P_as (pat,_) | P_typ (_,pat) | P_var (pat,_) -> contains_bitvector_pat pat | P_vector _ | P_vector_concat _ -> let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in is_bitvector_typ typ @@ -1333,7 +1334,7 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd (pat,guard,exp,annot) in let cs = rewrite_guarded_clauses l (List.map clause funcls) in List.map (fun (pat,exp,annot) -> - FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Unknown,None))),annot)) cs + FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,None))),annot)) cs | _ -> funcls (* TODO is the empty list possible here? *) in FD_aux (FD_function(r,t,e,funcls),(l,fdannot)) @@ -1765,6 +1766,7 @@ let rewrite_fix_val_specs (Defs defs) = let args_t' = rewrite_typ_nexp_ids (env_of exp) (pat_typ_of pat) in let ret_t' = rewrite_typ_nexp_ids (env_of exp) (typ_of exp) in (tq, Typ_aux (Typ_fn (args_t', ret_t', eff'), a)), eff' + | _ -> assert false (* find_vs must return a function type *) in let annot = add_effect_annot annot eff in (Bindings.add id vs val_specs, @@ -2288,7 +2290,7 @@ let rewrite_defs_letbind_effects = let exp3 = n_exp_term newreturn exp3 in k (rewrap (E_if (exp1,exp2,exp3)))) | E_for (id,start,stop,by,dir,body) -> - n_exp_name start (fun start -> + n_exp_name start (fun start -> n_exp_name stop (fun stop -> n_exp_name by (fun by -> let body = n_exp_term (effectful body) body in @@ -2305,19 +2307,19 @@ let rewrite_defs_letbind_effects = n_exp_name exp2 (fun exp2 -> k (rewrap (E_vector_access (exp1,exp2))))) | E_vector_subrange (exp1,exp2,exp3) -> - n_exp_name exp1 (fun exp1 -> - n_exp_name exp2 (fun exp2 -> + n_exp_name exp1 (fun exp1 -> + n_exp_name exp2 (fun exp2 -> n_exp_name exp3 (fun exp3 -> k (rewrap (E_vector_subrange (exp1,exp2,exp3)))))) | E_vector_update (exp1,exp2,exp3) -> - n_exp_name exp1 (fun exp1 -> - n_exp_name exp2 (fun exp2 -> + n_exp_name exp1 (fun exp1 -> + n_exp_name exp2 (fun exp2 -> n_exp_name exp3 (fun exp3 -> k (rewrap (E_vector_update (exp1,exp2,exp3)))))) | E_vector_update_subrange (exp1,exp2,exp3,exp4) -> - n_exp_name exp1 (fun exp1 -> - n_exp_name exp2 (fun exp2 -> - n_exp_name exp3 (fun exp3 -> + n_exp_name exp1 (fun exp1 -> + n_exp_name exp2 (fun exp2 -> + n_exp_name exp3 (fun exp3 -> n_exp_name exp4 (fun exp4 -> k (rewrap (E_vector_update_subrange (exp1,exp2,exp3,exp4))))))) | E_vector_append (exp1,exp2) -> @@ -2327,14 +2329,14 @@ let rewrite_defs_letbind_effects = | E_list exps -> n_exp_nameL exps (fun exps -> k (rewrap (E_list exps))) - | E_cons (exp1,exp2) -> + | E_cons (exp1,exp2) -> n_exp_name exp1 (fun exp1 -> n_exp_name exp2 (fun exp2 -> k (rewrap (E_cons (exp1,exp2))))) | E_record fexps -> n_fexps fexps (fun fexps -> k (rewrap (E_record fexps))) - | E_record_update (exp1,fexps) -> + | E_record_update (exp1,fexps) -> n_exp_name exp1 (fun exp1 -> n_fexps fexps (fun fexps -> k (rewrap (E_record_update (exp1,fexps))))) @@ -2343,11 +2345,16 @@ let rewrite_defs_letbind_effects = k (rewrap (E_field (exp1,id)))) | E_case (exp1,pexps) -> let newreturn = List.exists effectful_pexp pexps in - n_exp_name exp1 (fun exp1 -> + n_exp_name exp1 (fun exp1 -> n_pexpL newreturn pexps (fun pexps -> k (rewrap (E_case (exp1,pexps))))) + | E_try (exp1,pexps) -> + let newreturn = List.exists effectful_pexp pexps in + n_exp_name exp1 (fun exp1 -> + n_pexpL newreturn pexps (fun pexps -> + k (rewrap (E_try (exp1,pexps))))) | E_let (lb,body) -> - n_lb lb (fun lb -> + n_lb lb (fun lb -> rewrap (E_let (lb,n_exp body k))) | E_sizeof nexp -> k (rewrap (E_sizeof nexp)) @@ -2360,6 +2367,7 @@ let rewrite_defs_letbind_effects = n_exp_name exp1 (fun exp1 -> k (rewrap (E_assign (lexp,exp1))))) | E_exit exp' -> k (E_aux (E_exit (n_exp_term (effectful exp') exp'),annot)) + | E_throw exp' -> k (E_aux (E_throw (n_exp_term (effectful exp') exp'),annot)) | E_assert (exp1,exp2) -> n_exp_name exp1 (fun exp1 -> n_exp_name exp2 (fun exp2 -> @@ -2376,11 +2384,13 @@ let rewrite_defs_letbind_effects = | E_internal_return exp1 -> n_exp_name exp1 (fun exp1 -> k (rewrap (E_internal_return exp1))) + | E_internal_value v -> + k (rewrap (E_internal_value v)) | E_comment str -> - k (rewrap (E_comment str)) + k (rewrap (E_comment str)) | E_comment_struc exp' -> n_exp exp' (fun exp' -> - k (rewrap (E_comment_struc exp'))) + k (rewrap (E_comment_struc exp'))) | E_return exp' -> n_exp_name exp' (fun exp' -> k (rewrap (E_return exp'))) diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 7386e9fa..81296027 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -577,6 +577,10 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function | DEF_fixity _ -> mt,mt | DEF_overload (id,ids) -> init_env (string_of_id id), List.fold_left (fun ns id -> Nameset.add (string_of_id id) ns) mt ids | DEF_default def -> mt,mt + | DEF_internal_mutrec fdefs -> + let fvs = List.map (fv_of_fun consider_var) fdefs in + List.fold_left Nameset.union Nameset.empty (List.map fst fvs), + List.fold_left Nameset.union Nameset.empty (List.map snd fvs) | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef | DEF_reg_dec rdec -> fv_of_rd consider_var rdec | DEF_comm _ -> mt,mt -- cgit v1.2.3