From 5298e209f0ae12e51f3050888e18ad9be09543e4 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 31 Oct 2018 14:56:19 +0000 Subject: Improve error messages for unsolved function quantifiers For example, for a function like ``` val aget_X : forall 'n, 0 <= 'n <= 31. int('n) -> bits(64) function test(n : int) -> unit = { let y = aget_X(n); () } ``` we get the message > Could not resolve quantifiers for aget_X (0 <= 'ex7# & 'ex7# <= 31) > > Try adding named type variables for n : atom('ex7#) > > The property (0 <= n & n <= 31) must hold which suggests adding a name for the type variable 'ex7#, and gives the property in terms of the variable n. If we give n a type variable name: ``` val test : int -> unit function test(n as 'N) = { let y = aget_X(n); () } ``` It will suggest a constraint involving the type variable name > Could not resolve quantifiers for aget_X (0 <= 'ex6# & 'ex6# <= 31) > > Try adding the constraint (0 <= 'N & 'N <= 31) --- src/anf.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src/anf.ml') diff --git a/src/anf.ml b/src/anf.ml index 0f98caff..2e7b6b65 100644 --- a/src/anf.ml +++ b/src/anf.ml @@ -458,17 +458,17 @@ let rec split_block l = function let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in match p_aux with - | P_id id when global -> mk_apat (AP_global (id, pat_typ_of pat)) - | P_id id -> mk_apat (AP_id (id, pat_typ_of pat)) - | P_wild -> mk_apat (AP_wild (pat_typ_of pat)) + | P_id id when global -> mk_apat (AP_global (id, typ_of_pat pat)) + | P_id id -> mk_apat (AP_id (id, typ_of_pat pat)) + | P_wild -> mk_apat (AP_wild (typ_of_pat pat)) | P_tup pats -> mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)) - | P_app (id, [subpat]) -> mk_apat (AP_app (id, anf_pat ~global:global subpat, pat_typ_of pat)) - | P_app (id, pats) -> mk_apat (AP_app (id, mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)), pat_typ_of pat)) + | P_app (id, [subpat]) -> mk_apat (AP_app (id, anf_pat ~global:global subpat, typ_of_pat pat)) + | P_app (id, pats) -> mk_apat (AP_app (id, mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)), typ_of_pat pat)) | P_typ (_, pat) -> anf_pat ~global:global pat | P_var (pat, _) -> anf_pat ~global:global pat | P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat)) - | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (pat_typ_of pat))) - | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (pat_typ_of pat)) + | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (typ_of_pat pat))) + | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (typ_of_pat pat)) | _ -> anf_error ~loc:(fst annot) ("Could not convert pattern to ANF: " ^ string_of_pat pat) let rec apat_globals (AP_aux (aux, _, _)) = -- cgit v1.2.3 From 001e28b487c8a4cb2a25519a3acc8ac8c1aaabf5 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 31 Oct 2018 15:43:56 +0000 Subject: Rename Reporting_basic to Reporting There is no Reporting_complex, so it's not clear what the basic is intended to signify anyway. Add a GitHub issue link to any err_unreachable errors (as they are all bugs) --- src/anf.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/anf.ml') diff --git a/src/anf.ml b/src/anf.ml index 2e7b6b65..4b22b9ad 100644 --- a/src/anf.ml +++ b/src/anf.ml @@ -58,7 +58,7 @@ open PPrint module Big_int = Nat_big_num let anf_error ?loc:(l=Parse_ast.Unknown) message = - raise (Reporting_basic.err_general l ("\nANF translation: " ^ message)) + raise (Reporting.err_general l ("\nANF translation: " ^ message)) (**************************************************************************) (* 1. Conversion to A-normal form (ANF) *) @@ -510,7 +510,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) | E_block [] -> - Util.warn (Reporting_basic.loc_to_string l + Util.warn (Reporting.loc_to_string l ^ "\n\nTranslating empty block (possibly assigning to an uninitialized variable at the end of a block?)"); mk_aexp (ae_lit (L_aux (L_unit, l)) (typ_of exp)) | E_block exps -> -- cgit v1.2.3 From 4b8f3092b2c9767b916535ad73e045262d60d987 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 19 Nov 2018 17:14:19 +0000 Subject: Don't re-check AST repeatedly in exp_lift_assign re-write This was _really_ slow - about 50secs for ARM. If this changes causes breakages we should fix them in some other way. Also using Reporting.err_unreachable in ANF translation, and fix slice optimization when creating slices larger than 64-bits in C translation --- src/anf.ml | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) (limited to 'src/anf.ml') diff --git a/src/anf.ml b/src/anf.ml index 4b22b9ad..50f3ccba 100644 --- a/src/anf.ml +++ b/src/anf.ml @@ -57,9 +57,6 @@ open PPrint module Big_int = Nat_big_num -let anf_error ?loc:(l=Parse_ast.Unknown) message = - raise (Reporting.err_general l ("\nANF translation: " ^ message)) - (**************************************************************************) (* 1. Conversion to A-normal form (ANF) *) (**************************************************************************) @@ -453,7 +450,8 @@ let rec split_block l = function | exp :: exps -> let exps, last = split_block l exps in exp :: exps, last - | [] -> anf_error ~loc:l "empty block" + | [] -> + raise (Reporting.err_unreachable l __POS__ "empty block found when converting to ANF") let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in @@ -469,7 +467,9 @@ let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = | P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat)) | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (typ_of_pat pat))) | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (typ_of_pat pat)) - | _ -> anf_error ~loc:(fst annot) ("Could not convert pattern to ANF: " ^ string_of_pat pat) + | _ -> + raise (Reporting.err_unreachable (fst annot) __POS__ + ("Could not convert pattern to ANF: " ^ string_of_pat pat)) let rec apat_globals (AP_aux (aux, _, _)) = match aux with @@ -529,7 +529,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = mk_aexp (AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp)) | E_assign (lexp, _) -> - failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") + raise (Reporting.err_unreachable l __POS__ + ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")) | E_loop (loop_typ, cond, exp) -> let acond = anf cond in @@ -665,7 +666,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = mk_aexp (AE_let (Mutable, id, lvar_typ lvar, anf binding, anf body, typ_of exp)) | E_var (lexp, _, _) -> - failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") + raise (Reporting.err_unreachable l __POS__ + ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")) | E_let (LB_aux (LB_val (pat, binding), _), body) -> anf (E_aux (E_case (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, empty_tannot))]), exp_annot)) @@ -690,19 +692,19 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ -> (* Should be re-written by type checker *) - failwith "encountered raw vector operation when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered raw vector operation when converting to ANF") | E_internal_value _ -> (* Interpreter specific *) - failwith "encountered E_internal_value when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered E_internal_value when converting to ANF") | E_sizeof _ | E_constraint _ -> (* Sizeof nodes removed by sizeof rewriting pass *) - failwith "encountered E_sizeof or E_constraint node when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered E_sizeof or E_constraint node when converting to ANF") | E_nondet _ -> (* We don't compile E_nondet nodes *) - failwith "encountered E_nondet node when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered E_nondet node when converting to ANF") | E_internal_return _ | E_internal_plet _ -> - failwith "encountered unexpected internal node when converting to ANF" + raise (Reporting.err_unreachable l __POS__ "encountered unexpected internal node when converting to ANF") -- cgit v1.2.3 From ea177d95766789b0500317f12fe0939d1508e19c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 23 Nov 2018 17:55:54 +0000 Subject: C backend improvements - Propagate types more accurately to improve optimization on ANF representation. - Add a generic optimization pass to remove redundant variables that simply alias other variables. - Modify Sail interactive mode, so it can compile a specification with the :compile command, view generated intermediate representation via the :ir command, and step-through the IR with :exec (although this is very incomplete) - Introduce a third bitvector representation, between fast fixed-precision bitvectors, and variable length large bitvectors. The bitvector types are now from most efficient to least * CT_fbits for fixed precision, 64-bit or less bitvectors * CT_sbits for 64-bit or less, variable length bitvectors * CT_lbits for arbitrary variable length bitvectors - Support for generating C code using CT_sbits is currently incomplete, it just exists in the intermediate representation right now. - Include ctyp in AV_C_fragment, so we don't have to recompute it --- src/anf.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/anf.ml') diff --git a/src/anf.ml b/src/anf.ml index 50f3ccba..1f93e00f 100644 --- a/src/anf.ml +++ b/src/anf.ml @@ -127,7 +127,7 @@ and 'a aval = | AV_list of ('a aval) list * 'a | AV_vector of ('a aval) list * 'a | AV_record of ('a aval) Bindings.t * 'a - | AV_C_fragment of fragment * 'a + | AV_C_fragment of fragment * 'a * ctyp (* Renaming variables in ANF expressions *) @@ -183,7 +183,7 @@ let rec aval_rename from_id to_id = function | AV_list (avals, typ) -> AV_list (List.map (aval_rename from_id to_id) avals, typ) | AV_vector (avals, typ) -> AV_vector (List.map (aval_rename from_id to_id) avals, typ) | AV_record (avals, typ) -> AV_record (Bindings.map (aval_rename from_id to_id) avals, typ) - | AV_C_fragment (fragment, typ) -> AV_C_fragment (frag_rename from_id to_id fragment, typ) + | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename from_id to_id fragment, typ, ctyp) let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = let recur = aexp_rename from_id to_id in @@ -423,7 +423,8 @@ and pp_aval = function | AV_id (id, lvar) -> pp_lvar lvar (pp_id id) | AV_tuple avals -> parens (separate_map (comma ^^ space) pp_aval avals) | AV_ref (id, lvar) -> string "ref" ^^ space ^^ pp_lvar lvar (pp_id id) - | AV_C_fragment (frag, typ) -> pp_annot typ (string (string_of_fragment frag |> Util.cyan |> Util.clear)) + | AV_C_fragment (frag, typ, ctyp) -> + pp_annot typ (string ("(" ^ string_of_ctyp ctyp ^ ")" ^ string_of_fragment frag |> Util.cyan |> Util.clear)) | AV_vector (avals, typ) -> pp_annot typ (string "[" ^^ separate_map (comma ^^ space) pp_aval avals ^^ string "]") | AV_list (avals, typ) -> -- cgit v1.2.3 From df3ea2e6da387ead7cba1e27632768e563696502 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 4 Dec 2018 14:53:23 +0000 Subject: Remove FES_Fexps constructor This makes dealing with records and field expressions in Sail much nicer because the constructors are no longer stacked together like matryoshka dolls with unnecessary layers. Previously to get the fields of a record it would be either E_aux (E_record (FES_aux (FES_Fexps (fexps, _), _)), _) but now it is simply: E_aux (E_record fexps, _) --- src/anf.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/anf.ml') diff --git a/src/anf.ml b/src/anf.ml index 1f93e00f..915ab738 100644 --- a/src/anf.ml +++ b/src/anf.ml @@ -569,7 +569,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let aval, wrap = to_aval (anf field_exp) in wrap (mk_aexp (AE_field (aval, id, typ_of exp))) - | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record_update (exp, fexps) -> let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = let aval, wrap = to_aval (anf exp) in (id, aval), wrap @@ -679,7 +679,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in wrap (mk_aexp (AE_val (AV_tuple (List.map fst avals)))) - | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record fexps -> let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = let aval, wrap = to_aval (anf exp) in (id, aval), wrap -- cgit v1.2.3