From d225547fc49807961967181b8661a35fe4de8ed3 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 6 Jun 2019 17:29:22 +0100 Subject: Add an option to pre-compile the axiomatic model for SMT --- src/rewrites.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'src/rewrites.ml') diff --git a/src/rewrites.ml b/src/rewrites.ml index c94e2f57..4ea52c4d 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5023,7 +5023,6 @@ let rewrites_target tgt = | "c" -> rewrites_c | "ir" -> rewrites_c @ [("properties", [])] | "smt" -> rewrites_c @ [("properties", [])] - | "smtfuzz" -> rewrites_c @ [("properties", [])] | "sail" -> [] | "latex" -> [] | "interpreter" -> rewrites_interpreter -- cgit v1.2.3 From 3eadd260f7382f98eb7dcbd706a3ed3e910167eb Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 10 Jun 2019 17:53:58 +0100 Subject: Add well-formedness check for type schemes in valspecs. Fixes #47. Also adjust the nexp substitution so that the error message points to a useful location, and replace the empty environment with the initial environment in a few functions that do type checking to ensure that the prover is set up (which may be needed for the wf check). --- src/rewrites.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/rewrites.ml') diff --git a/src/rewrites.ml b/src/rewrites.ml index 4ea52c4d..e3864a7f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1440,7 +1440,7 @@ let rewrite_defs_exp_lift_assign env defs = rewrite_defs_base write_reg_ref (vector_access (GPR, i)) exp *) let rewrite_register_ref_writes (Defs defs) = - let (Defs write_reg_spec) = fst (Type_error.check Env.empty (Defs (List.map gen_vs + let (Defs write_reg_spec) = fst (Type_error.check initial_env (Defs (List.map gen_vs [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")]))) in let lexp_ref_exp (LEXP_aux (_, annot) as lexp) = try @@ -1630,7 +1630,7 @@ let rewrite_defs_early_return env (Defs defs) = FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, List.map (rewrite_funcl_early_return rewriters) funcls), a) in - let (Defs early_ret_spec) = fst (Type_error.check Env.empty (Defs [gen_vs + let (Defs early_ret_spec) = fst (Type_error.check initial_env (Defs [gen_vs ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in rewrite_defs_base @@ -3771,7 +3771,7 @@ let rewrite_defs_remove_superfluous_returns env = let rewrite_defs_remove_e_assign env (Defs defs) = - let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs + let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars"); ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); -- cgit v1.2.3 From d61140c5a922d8781356aa874a2fe2a7a36ed0ee Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 12 Jun 2019 17:15:10 +0100 Subject: Handle partial matches in guarded pattern rewrite Add a fallthrough case that fails to potentially partial pattern matches. This also helps to preserve any guard in the final match case, which might be needed for flow typing (see the discussion on issue #51). TODO: Merge with the MakeExhaustive rewrite, which currently does not support guarded patterns. --- src/rewrites.ml | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) (limited to 'src/rewrites.ml') diff --git a/src/rewrites.ml b/src/rewrites.ml index e3864a7f..7bfea9b0 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -873,7 +873,7 @@ let case_exp e t cs = strategy to ours: group *mutually exclusive* clauses, and try to merge them into a pattern match first instead of an if-then-else cascade. *) -let rewrite_guarded_clauses l cs = +let rewrite_guarded_clauses l env typ cs = let rec group fallthrough clauses = let add_clause (pat,cls,annot) c = (pat,cls @ [c],annot) in let rec group_aux current acc = (function @@ -934,7 +934,18 @@ let rewrite_guarded_clauses l cs = | [] -> raise (Reporting.err_unreachable l __POS__ "if_exp given empty list in rewrite_guarded_clauses")) in - group [] cs + let is_complete = Pattern_completeness.is_complete (Env.pattern_completeness_ctx env) (List.map construct_pexp cs) in + let fallthrough = + if not is_complete then + let p = P_aux (P_wild, (Parse_ast.Generated l, empty_tannot)) in + let msg = "Pattern match failure at " ^ Reporting.short_loc_to_string l in + let a = mk_exp (E_assert (mk_lit_exp L_false, mk_lit_exp (L_string msg))) in + let b = mk_exp (E_exit (mk_lit_exp L_unit)) in + let (E_aux (_, (_, ann)) as e) = check_exp env (mk_exp (E_block [a; b])) typ in + [(p,None,e,(Parse_ast.Generated l,ann))] + else [] + in + group [] (cs @ fallthrough) let bitwise_and_exp exp1 exp2 = let (E_aux (_,(l,_))) = exp1 in @@ -1316,7 +1327,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = (pat, None, rewrite_rec body, annot) | Pat_aux (Pat_when (pat, guard, body), annot) -> (pat, Some (rewrite_rec guard), rewrite_rec body, annot) in - let clauses = rewrite_guarded_clauses l (List.map clause ps) in + let clauses = rewrite_guarded_clauses l (env_of full_exp) (typ_of full_exp) (List.map clause ps) in let e = rewrite_rec e in if (effectful e) then let (E_aux (_,(el,eannot))) = e in @@ -1334,7 +1345,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = (pat, None, rewrite_rec body, annot) | Pat_aux (Pat_when (pat, guard, body), annot) -> (pat, Some (rewrite_rec guard), rewrite_rec body, annot) in - let clauses = rewrite_guarded_clauses l (List.map clause ps) in + let clauses = rewrite_guarded_clauses l (env_of full_exp) (typ_of full_exp) (List.map clause ps) in let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in let ps = List.map pexp clauses in fix_eff_exp (annot_exp (E_try (e,ps)) l (env_of full_exp) (typ_of full_exp)) @@ -1342,12 +1353,12 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fdannot))) = let funcls = match funcls with - | (FCL_aux (FCL_Funcl(id,_),_) :: _) -> + | (FCL_aux (FCL_Funcl(id,_), fclannot) :: _) -> let clause (FCL_aux (FCL_Funcl(_,pexp),annot)) = let pat,guard,exp,_ = destruct_pexp pexp in let exp = rewriters.rewrite_exp rewriters exp in (pat,guard,exp,annot) in - let cs = rewrite_guarded_clauses l (List.map clause funcls) in + let cs = rewrite_guarded_clauses l (env_of_annot fclannot) (typ_of_annot fclannot) (List.map clause funcls) in List.map (fun (pat,exp,annot) -> FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,empty_tannot))),annot)) cs | _ -> funcls (* TODO is the empty list possible here? *) in -- cgit v1.2.3 From 5de71f5be6e729184e122cf26bcb9a8ed0a40416 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 13 Jun 2019 21:38:42 +0100 Subject: Fix some bugs in Lem rewriter A missing type annotation in rewrite_guarded_clauses caused a crash in some cases. Also fix an effect propagation bug in rewrite_letbind_effects. --- src/rewrites.ml | 46 ++++++++++++++++++++++++++++------------------ 1 file changed, 28 insertions(+), 18 deletions(-) (limited to 'src/rewrites.ml') diff --git a/src/rewrites.ml b/src/rewrites.ml index 7bfea9b0..c9eece20 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -873,7 +873,7 @@ let case_exp e t cs = strategy to ours: group *mutually exclusive* clauses, and try to merge them into a pattern match first instead of an if-then-else cascade. *) -let rewrite_guarded_clauses l env typ cs = +let rewrite_guarded_clauses l env pat_typ typ cs = let rec group fallthrough clauses = let add_clause (pat,cls,annot) c = (pat,cls @ [c],annot) in let rec group_aux current acc = (function @@ -937,12 +937,12 @@ let rewrite_guarded_clauses l env typ cs = let is_complete = Pattern_completeness.is_complete (Env.pattern_completeness_ctx env) (List.map construct_pexp cs) in let fallthrough = if not is_complete then - let p = P_aux (P_wild, (Parse_ast.Generated l, empty_tannot)) in + let p = P_aux (P_wild, (gen_loc l, mk_tannot env pat_typ no_effect)) in let msg = "Pattern match failure at " ^ Reporting.short_loc_to_string l in - let a = mk_exp (E_assert (mk_lit_exp L_false, mk_lit_exp (L_string msg))) in - let b = mk_exp (E_exit (mk_lit_exp L_unit)) in - let (E_aux (_, (_, ann)) as e) = check_exp env (mk_exp (E_block [a; b])) typ in - [(p,None,e,(Parse_ast.Generated l,ann))] + let a = mk_exp ~loc:(gen_loc l) (E_assert (mk_lit_exp L_false, mk_lit_exp (L_string msg))) in + let b = mk_exp ~loc:(gen_loc l) (E_exit (mk_lit_exp L_unit)) in + let (E_aux (_, (_, ann)) as e) = check_exp env (mk_exp ~loc:(gen_loc l) (E_block [a; b])) typ in + [(p,None,e,(gen_loc l,ann))] else [] in group [] (cs @ fallthrough) @@ -1327,7 +1327,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = (pat, None, rewrite_rec body, annot) | Pat_aux (Pat_when (pat, guard, body), annot) -> (pat, Some (rewrite_rec guard), rewrite_rec body, annot) in - let clauses = rewrite_guarded_clauses l (env_of full_exp) (typ_of full_exp) (List.map clause ps) in + let clauses = rewrite_guarded_clauses l (env_of full_exp) (typ_of e) (typ_of full_exp) (List.map clause ps) in let e = rewrite_rec e in if (effectful e) then let (E_aux (_,(el,eannot))) = e in @@ -1345,7 +1345,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = (pat, None, rewrite_rec body, annot) | Pat_aux (Pat_when (pat, guard, body), annot) -> (pat, Some (rewrite_rec guard), rewrite_rec body, annot) in - let clauses = rewrite_guarded_clauses l (env_of full_exp) (typ_of full_exp) (List.map clause ps) in + let clauses = rewrite_guarded_clauses l (env_of full_exp) (typ_of e) (typ_of full_exp) (List.map clause ps) in let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in let ps = List.map pexp clauses in fix_eff_exp (annot_exp (E_try (e,ps)) l (env_of full_exp) (typ_of full_exp)) @@ -1353,12 +1353,21 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fdannot))) = let funcls = match funcls with - | (FCL_aux (FCL_Funcl(id,_), fclannot) :: _) -> + | (FCL_aux (FCL_Funcl(id,pexp), fclannot) :: _) -> let clause (FCL_aux (FCL_Funcl(_,pexp),annot)) = let pat,guard,exp,_ = destruct_pexp pexp in let exp = rewriters.rewrite_exp rewriters exp in (pat,guard,exp,annot) in - let cs = rewrite_guarded_clauses l (env_of_annot fclannot) (typ_of_annot fclannot) (List.map clause funcls) in + let pexp_pat_typ, pexp_ret_typ = + let pat, _, exp, _ = destruct_pexp pexp in + (typ_of_pat pat, typ_of exp) + in + let pat_typ, ret_typ = match Env.get_val_spec_orig id (env_of_annot fclannot) with + | (tq, Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _)) -> (arg_typ, ret_typ) + | (tq, Typ_aux (Typ_fn (arg_typs, ret_typ, _), _)) -> (tuple_typ arg_typs, ret_typ) + | _ -> (pexp_pat_typ, pexp_ret_typ) | exception _ -> (pexp_pat_typ, pexp_ret_typ) + in + let cs = rewrite_guarded_clauses l (env_of_annot fclannot) pat_typ ret_typ (List.map clause funcls) in List.map (fun (pat,exp,annot) -> FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,empty_tannot))),annot)) cs | _ -> funcls (* TODO is the empty list possible here? *) in @@ -1881,10 +1890,9 @@ let rewrite_fix_val_specs env (Defs defs) = Rec_aux (Rec_rec, Parse_ast.Unknown) | _ -> recopt in - let tannotopt = match tannotopt, funcls with - | Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), l), - FCL_aux (FCL_Funcl (_, Pat_aux ((Pat_exp (_, exp) | Pat_when (_, _, exp)), _)), _) :: _ -> - Typ_annot_opt_aux (Typ_annot_opt_some (typq, Env.expand_synonyms (env_of exp) typ), l) + let tannotopt = match tannotopt with + | Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), l) -> + Typ_annot_opt_aux (Typ_annot_opt_none, l) | _ -> tannotopt in (val_specs, FD_aux (FD_function (recopt, tannotopt, effopt, funcls), a)) in @@ -2468,7 +2476,8 @@ let rewrite_defs_letbind_effects env = rewrap (E_var (lexp,exp1,n_exp exp2 k)))) | E_internal_return exp1 -> n_exp_name exp1 (fun exp1 -> - k (if effectful (propagate_exp_effect exp1) then exp1 else rewrap (E_internal_return exp1))) + let exp1 = fix_eff_exp (propagate_exp_effect exp1) in + k (if effectful exp1 then exp1 else rewrap (E_internal_return exp1))) | E_internal_value v -> k (rewrap (E_internal_value v)) | E_return exp' -> @@ -3637,7 +3646,8 @@ let remove_reference_types exp = let rewrite_defs_remove_superfluous_letbinds env = let e_aux (exp,annot) = match exp with - | E_let (LB_aux (LB_val (pat, exp1), _), exp2) -> + | E_let (LB_aux (LB_val (pat, exp1), _), exp2) + | E_internal_plet (pat, exp1, exp2) -> begin match untyp_pat pat, uncast_exp exp1, uncast_exp exp2 with (* 'let x = EXP1 in x' can be replaced with 'EXP1' *) | (P_aux (P_id id, _), _), _, (E_aux (E_id id', _), _) @@ -3649,7 +3659,7 @@ let rewrite_defs_remove_superfluous_letbinds env = (* "let x = EXP1 in return x" can be replaced with 'return (EXP1)', at least when EXP1 is 'small' enough *) | (P_aux (P_id id, _), _), _, (E_aux (E_internal_return (E_aux (E_id id', _)), _), _) - when Id.compare id id' = 0 && small exp1 -> + when Id.compare id id' = 0 && small exp1 && not (effectful exp1) -> let (E_aux (_,e1annot)) = exp1 in E_aux (E_internal_return (exp1),e1annot) | _ -> E_aux (exp,annot) @@ -3746,7 +3756,7 @@ let rewrite_defs_remove_superfluous_returns env = when lit = lit' -> add_opt_cast ptyp etyp a exp1 | (P_aux (P_wild,pannot), ptyp), - (E_aux (E_internal_return (E_aux (E_lit (L_aux (L_unit,_)),_)), a), etyp) + (E_aux ((E_internal_return (E_aux (E_lit (L_aux (L_unit,_)),_)) | E_lit (L_aux (L_unit,_))), a), etyp) when is_unit_typ (typ_of exp1) -> add_opt_cast ptyp etyp a exp1 | (P_aux (P_id id,_), ptyp), -- cgit v1.2.3 From 6048e329c1d88a5d91498c9431e9e9282d170afe Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 18 Jun 2019 20:40:53 +0100 Subject: Fix handling of E_internal_plet in rewrite --- src/rewrites.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'src/rewrites.ml') diff --git a/src/rewrites.ml b/src/rewrites.ml index c9eece20..64cfe48b 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3662,19 +3662,19 @@ let rewrite_defs_remove_superfluous_letbinds env = when Id.compare id id' = 0 && small exp1 && not (effectful exp1) -> let (E_aux (_,e1annot)) = exp1 in E_aux (E_internal_return (exp1),e1annot) + | _, (E_aux (E_throw e, a), _), _ -> E_aux (E_throw e, a) + | (pat, _), (E_aux (E_assert (c, msg), a) as assert_exp, _), _ -> + begin match typ_of c with + | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _) + when prove __POS__ (env_of c) (nc_not nc) -> + (* Drop rest of block after an 'assert(false)' *) + let exit_exp = E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) in + E_aux (E_internal_plet (pat, assert_exp, exit_exp), annot) + | _ -> + E_aux (exp, annot) + end | _ -> E_aux (exp,annot) end - | E_internal_plet (_, E_aux (E_throw e, a), _) -> E_aux (E_throw e, a) - | E_internal_plet (pat, (E_aux (E_assert (c, msg), a) as assert_exp), _) -> - begin match typ_of c with - | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _) - when prove __POS__ (env_of c) (nc_not nc) -> - (* Drop rest of block after an 'assert(false)' *) - let exit_exp = E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) in - E_aux (E_internal_plet (pat, assert_exp, exit_exp), annot) - | _ -> - E_aux (exp, annot) - end | _ -> E_aux (exp,annot) in let alg = { id_exp_alg with e_aux = e_aux } in -- cgit v1.2.3 From 62f7179d0d160439f87d80bc591bddf50bb295fb Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 18 Jun 2019 17:06:53 +0100 Subject: Rewriting improvements for monomorphic aarch64_small - allow disjoint_pat to be used on patterns that have just been introduced by the rewrite without rechecking - don't rebuild the matched expression in the generated fallthrough case (or any wildcard fall-through) - it may be dead code and generate badly typed Lem - update the type environment passed to rewrites whenever type checking is performed; stale information broke some rewrites --- src/rewrites.ml | 53 ++++++++++++++++++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 19 deletions(-) (limited to 'src/rewrites.ml') diff --git a/src/rewrites.ml b/src/rewrites.ml index 64cfe48b..becf2a88 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -771,23 +771,23 @@ and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_) (* A simple check for pattern disjointness; used for optimisation in the guarded pattern rewrite step *) -let rec disjoint_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = +let rec disjoint_pat env (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = match p1, p2 with - | P_as (pat1, _), _ -> disjoint_pat pat1 pat2 - | _, P_as (pat2, _) -> disjoint_pat pat1 pat2 - | P_typ (_, pat1), _ -> disjoint_pat pat1 pat2 - | _, P_typ (_, pat2) -> disjoint_pat pat1 pat2 - | P_var (pat1, _), _ -> disjoint_pat pat1 pat2 - | _, P_var (pat2, _) -> disjoint_pat pat1 pat2 - | P_id id, _ when id_is_unbound id (env_of_annot annot1) -> false - | _, P_id id when id_is_unbound id (env_of_annot annot2) -> false + | P_as (pat1, _), _ -> disjoint_pat env pat1 pat2 + | _, P_as (pat2, _) -> disjoint_pat env pat1 pat2 + | P_typ (_, pat1), _ -> disjoint_pat env pat1 pat2 + | _, P_typ (_, pat2) -> disjoint_pat env pat1 pat2 + | P_var (pat1, _), _ -> disjoint_pat env pat1 pat2 + | _, P_var (pat2, _) -> disjoint_pat env pat1 pat2 + | P_id id, _ when id_is_unbound id env -> false + | _, P_id id when id_is_unbound id env -> false | P_id id1, P_id id2 -> Id.compare id1 id2 <> 0 | P_app (id1, args1), P_app (id2, args2) -> - Id.compare id1 id2 <> 0 || List.exists2 disjoint_pat args1 args2 + Id.compare id1 id2 <> 0 || List.exists2 (disjoint_pat env) args1 args2 | P_vector pats1, P_vector pats2 | P_tup pats1, P_tup pats2 | P_list pats1, P_list pats2 -> - List.exists2 disjoint_pat pats1 pats2 + List.exists2 (disjoint_pat env) pats1 pats2 | _ -> false let equiv_pats pat1 pat2 = @@ -846,6 +846,8 @@ let case_exp e t cs = let env = env_of e in let annot = (get_loc_exp e, Some (env_of e, t, no_effect)) in match cs with + | [(P_aux (P_wild, _), body, _)] -> + fix_eff_exp body | [(P_aux (P_id id, pannot) as pat, body, _)] -> fix_eff_exp (annot_exp (E_let (LB_aux (LB_val (pat, e), pannot), body)) l env t) | _ -> @@ -889,10 +891,12 @@ let rewrite_guarded_clauses l env pat_typ typ cs = let c' = (pat',guard',body',annot) in group_aux (add_clause current c') acc cs | None -> - let pat = remove_wildcards "g__" pat in + let pat = match cs with _::_ -> remove_wildcards "g__" pat | _ -> pat in group_aux (pat,[c],annot) (acc @ [current]) cs) | [] -> acc @ [current]) in let groups = match clauses with + | [(pat,guard,body,annot) as c] -> + [(pat, [c], annot)] | ((pat,guard,body,annot) as c) :: cs -> group_aux (remove_wildcards "g__" pat, [c], annot) [] cs | _ -> @@ -924,7 +928,7 @@ let rewrite_guarded_clauses l env pat_typ typ cs = (* For singleton clauses with a guard, use fallthrough clauses if the guard is not satisfied, but only those fallthrough clauses that are not disjoint with the current pattern *) - let overlapping_clause (pat, _, _) = not (disjoint_pat current_pat pat) in + let overlapping_clause (pat, _, _) = not (disjoint_pat env current_pat pat) in let fallthrough = List.filter overlapping_clause fallthrough in (match guard, fallthrough with | Some exp, _ :: _ -> @@ -4679,11 +4683,11 @@ let rewrite_loops_with_escape_effect env defs = in rewrite_defs_base { rewriters_base with rewrite_exp } defs -let recheck_defs env defs = fst (Type_error.check initial_env defs) +let recheck_defs env defs = Type_error.check initial_env defs let recheck_defs_without_effects env defs = let old = !opt_no_effects in let () = opt_no_effects := true in - let result,_ = Type_error.check initial_env defs in + let result = Type_error.check initial_env defs in let () = opt_no_effects := old in result @@ -4783,12 +4787,20 @@ let if_mono f env defs = | [], false -> defs | _, _ -> f env defs +let if_mono_env f env defs = + match !opt_mono_split, !opt_auto_mono with + | [], false -> defs, env + | _, _ -> f env defs + (* Also turn mwords stages on when we're just trying out mono *) let if_mwords f env defs = if !Pretty_print_lem.opt_mwords then f env defs else if_mono f env defs +let if_mwords_env f env defs = + if !Pretty_print_lem.opt_mwords then f env defs else if_mono_env f env defs type rewriter = | Basic_rewriter of (Env.t -> tannot defs -> tannot defs) + | Checking_rewriter of (Env.t -> tannot defs -> tannot defs * Env.t) | Bool_rewriter of (bool -> rewriter) | String_rewriter of (string -> rewriter) | Literal_rewriter of ((lit -> bool) -> rewriter) @@ -4812,6 +4824,8 @@ let instantiate_rewrite rewriter args = match rewriter, arg with | Basic_rewriter rw, If_mono_arg -> Basic_rewriter (if_mono rw) | Basic_rewriter rw, If_mwords_arg -> Basic_rewriter (if_mwords rw) + | Checking_rewriter rw, If_mono_arg -> Checking_rewriter (if_mono_env rw) + | Checking_rewriter rw, If_mwords_arg -> Checking_rewriter (if_mwords_env rw) | Bool_rewriter rw, Bool_arg b -> rw b | String_rewriter rw, String_arg str -> rw str | Literal_rewriter rw, Literal_arg selector -> rw (selector_function selector) @@ -4819,14 +4833,15 @@ let instantiate_rewrite rewriter args = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Invalid rewrite argument") in match List.fold_left instantiate rewriter args with - | Basic_rewriter rw -> rw + | Basic_rewriter rw -> fun env defs -> rw env defs, env + | Checking_rewriter rw -> rw | _ -> raise (Reporting.err_general Parse_ast.Unknown "Rewrite not fully instantiated") let all_rewrites = [ ("no_effect_check", Basic_rewriter (fun _ defs -> opt_no_effects := true; defs)); - ("recheck_defs", Basic_rewriter recheck_defs); - ("recheck_defs_without_effects", Basic_rewriter recheck_defs_without_effects); + ("recheck_defs", Checking_rewriter recheck_defs); + ("recheck_defs_without_effects", Checking_rewriter recheck_defs_without_effects); ("optimize_recheck_defs", Basic_rewriter (fun _ -> Optimize.recheck)); ("realise_mappings", Basic_rewriter rewrite_defs_realise_mappings); ("remove_mapping_valspecs", Basic_rewriter remove_mapping_valspecs); @@ -5083,5 +5098,5 @@ let rewrite_check_annot = rewrite_pat = (fun _ -> check_pat) } let rewrite_defs_check = [ - ("check_annotations", fun _ -> rewrite_check_annot); + ("check_annotations", fun env defs -> rewrite_check_annot defs, env); ] -- cgit v1.2.3 From 01177094d660286ebe8c83c68d1e8890e29d154c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 11 Jul 2019 14:21:25 +0100 Subject: Make sure constant folding won't fold external definitions that also have sail definitions Definitions can be made external on a per-backend basis, so we need to make sure constant folding doesn't inline external functions that have sail definitions for backends other than the ones we are currently targetting --- src/rewrites.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'src/rewrites.ml') diff --git a/src/rewrites.ml b/src/rewrites.ml index becf2a88..d396e18b 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4772,9 +4772,10 @@ let opt_auto_mono = ref false let opt_dall_split_errors = ref false let opt_dmono_continue = ref false -let monomorphise env defs = +let monomorphise target env defs = let open Monomorphise in monomorphise + target { auto = !opt_auto_mono; debug_analysis = !opt_dmono_analysis; all_split_errors = !opt_dall_split_errors; @@ -4850,12 +4851,12 @@ let all_rewrites = [ ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns); ("mono_rewrites", Basic_rewriter mono_rewrites); ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps); - ("monomorphise", Basic_rewriter monomorphise); + ("monomorphise", String_rewriter (fun target -> Basic_rewriter (monomorphise target))); ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); ("add_bitvector_casts", Basic_rewriter (fun _ -> Monomorphise.add_bitvector_casts)); ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); ("remove_impossible_int_cases", Basic_rewriter Constant_propagation.remove_impossible_int_cases); - ("const_prop_mutrec", Basic_rewriter Constant_propagation_mutrec.rewrite_defs); + ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_defs target))); ("make_cases_exhaustive", Basic_rewriter MakeExhaustive.rewrite); ("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b))); ("vector_string_pats_to_bit_list", Basic_rewriter rewrite_defs_vector_string_pats_to_bit_list); @@ -4887,7 +4888,7 @@ let all_rewrites = [ ("simple_types", Basic_rewriter rewrite_simple_types); ("overload_cast", Basic_rewriter rewrite_overload_cast); ("top_sort_defs", Basic_rewriter (fun _ -> top_sort_defs)); - ("constant_fold", Basic_rewriter (fun _ -> Constant_fold.rewrite_constant_function_calls)); + ("constant_fold", String_rewriter (fun target -> Basic_rewriter (fun _ -> Constant_fold.rewrite_constant_function_calls target))); ("split", String_rewriter (fun str -> Basic_rewriter (rewrite_split_fun_ctor_pats str))); ("properties", Basic_rewriter (fun _ -> Property.rewrite)); ] @@ -4902,7 +4903,7 @@ let rewrites_lem = [ ("recheck_defs", [If_mono_arg]); ("undefined", [Bool_arg false]); ("toplevel_nexps", [If_mono_arg]); - ("monomorphise", [If_mono_arg]); + ("monomorphise", [String_arg "lem"; If_mono_arg]); ("recheck_defs", [If_mwords_arg]); ("add_bitvector_casts", [If_mwords_arg]); ("atoms_to_singletons", [If_mono_arg]); @@ -4925,7 +4926,7 @@ let rewrites_lem = [ ("split", [String_arg "execute"]); ("recheck_defs", []); ("top_sort_defs", []); - ("const_prop_mutrec", []); + ("const_prop_mutrec", [String_arg "lem"]); ("vector_string_pats_to_bit_list", []); ("exp_lift_assign", []); ("early_return", []); @@ -5021,7 +5022,7 @@ let rewrites_c = [ ("mono_rewrites", [If_mono_arg]); ("recheck_defs", [If_mono_arg]); ("toplevel_nexps", [If_mono_arg]); - ("monomorphise", [If_mono_arg]); + ("monomorphise", [String_arg "c"; If_mono_arg]); ("atoms_to_singletons", [If_mono_arg]); ("recheck_defs", [If_mono_arg]); ("undefined", [Bool_arg false]); @@ -5036,7 +5037,7 @@ let rewrites_c = [ ("exp_lift_assign", []); ("merge_function_clauses", []); ("optimize_recheck_defs", []); - ("constant_fold", []) + ("constant_fold", [String_arg "c"]) ] let rewrites_interpreter = [ -- cgit v1.2.3