diff --git a/language/sail.ott b/language/sail.ott index c93e4be67..3eec12f7c 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -726,7 +726,7 @@ default_spec :: 'DT_' ::= scattered_def :: 'SD_' ::= {{ com scattered function and union type definitions }} {{ aux _ annot }} {{ auxparam 'a }} - | scattered function rec_opt tannot_opt effect_opt id :: :: function + | scattered function id : tannot_opt effect_opt :: :: function {{ texlong }} {{ com scattered function definition header }} | function clause funcl :: :: funcl diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index 489c30bd2..749cd101e 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -991,7 +991,7 @@ and map_valspec_annot f = function VS_aux (vs_aux, annot) -> VS_aux (vs_aux, f a and map_scattered_annot f = function SD_aux (sd_aux, annot) -> SD_aux (map_scattered_annot_aux f sd_aux, f annot) and map_scattered_annot_aux f = function - | SD_function (rec_opt, tannot_opt, name) -> SD_function (map_recopt_annot f rec_opt, tannot_opt, name) + | SD_function (name, tannot_opt) -> SD_function (name, tannot_opt) | SD_funcl fcl -> SD_funcl (map_funcl_annot f fcl) | SD_variant (id, typq) -> SD_variant (id, typq) | SD_unioncl (id, tu) -> SD_unioncl (id, tu) @@ -1425,7 +1425,7 @@ let id_of_dec_spec (DEC_aux (DEC_reg (_, id, _), _)) = id let id_of_scattered (SD_aux (sdef, _)) = match sdef with - | SD_function (_, _, id) + | SD_function (id, _) | SD_funcl (FCL_aux (FCL_funcl (id, _), _)) | SD_end id | SD_variant (id, _) diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml index 6e66e15e5..e6e374916 100644 --- a/src/lib/chunk_ast.ml +++ b/src/lib/chunk_ast.ml @@ -1137,7 +1137,7 @@ let chunk_default_typing_spec comments chunks (DT_aux (DT_order (kind, typ), l)) chunk_atyp comments chunks typ; Queue.push (Spacer (true, 1)) chunks -let chunk_fundef comments chunks (FD_aux (FD_function (rec_opt, tannot_opt, _, funcls), l)) = +let chunk_fundef comments chunks (FD_aux (FD_function (rec_opt, tannot_opt, funcls), l)) = pop_comments comments chunks l; let fn_id = match funcls with @@ -1276,7 +1276,7 @@ let chunk_scattered comments chunks (SD_aux (aux, l)) = (Function { id; clause = true; rec_opt = None; typq_opt = None; return_typ_opt = None; funcls = [funcl_chunks] }) chunks | SD_end id -> build_def chunks [chunk_keyword "end"; chunk_id id comments] - | SD_function (_, _, _, id) -> build_def chunks [chunk_keyword "scattered function"; chunk_id id comments] + | SD_function (id, _) -> build_def chunks [chunk_keyword "scattered function"; chunk_id id comments] | _ -> Reporting.unreachable l __POS__ "unhandled scattered def" let def_spacer (_, e) (s, _) = match (e, s) with Some l_e, Some l_s -> if l_s > l_e + 1 then 1 else 0 | _, _ -> 1 diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index 1eeb8c49a..088053d53 100644 --- a/src/lib/initial_check.ml +++ b/src/lib/initial_check.ml @@ -733,10 +733,10 @@ module KindInference = struct let* case = infer_case ctx case in wrap (P.FCL_funcl (id, case)) - let infer_fundef ctx (P.FD_aux (P.FD_function (rec_opt, tannot_opt, effects, funcls), l)) = + let infer_fundef ctx (P.FD_aux (P.FD_function (rec_opt, tannot_opt, funcls), l)) = let* tannot_opt = infer_tannot_opt ctx tannot_opt in let* funcls = mapM (infer_funcl ctx) funcls in - return (P.FD_aux (P.FD_function (rec_opt, tannot_opt, effects, funcls), l)) + return (P.FD_aux (P.FD_function (rec_opt, tannot_opt, funcls), l)) let rec infer_constructor ctx (P.Tu_aux (aux, l)) = let wrap aux = return (P.Tu_aux (aux, l)) in @@ -1761,7 +1761,7 @@ let to_ast_impl_funcls ctx (P.FCL_aux (fcl, l) : P.funcl) : uannot funcl list = | _ -> raise (Reporting.err_general l "Attributes or documentation comment not permitted here") let to_ast_fundef ctx fdef = - let P.FD_aux (P.FD_function (rec_opt, tannot_opt, _, funcls), l), kenv = + let P.FD_aux (P.FD_function (rec_opt, tannot_opt, funcls), l), kenv = KindInference.infer_fundef ctx fdef KindInference.initial_env in let tannot_opt, ctx = ConvertType.to_ast_tannot_opt kenv ctx tannot_opt in @@ -1837,9 +1837,10 @@ let to_ast_dec ctx (P.DEC_aux (regdec, l)) = let to_ast_scattered ctx (P.SD_aux (aux, l)) = let extra_def, aux, ctx = match aux with - | P.SD_function (rec_opt, tannot_opt, _, id) -> + | P.SD_function (id, tannot_opt) -> + let id = to_ast_id ctx id in let tannot_opt, _ = to_ast_tannot_opt ctx tannot_opt in - (None, SD_function (to_ast_rec ctx rec_opt, tannot_opt, to_ast_id ctx id), ctx) + (None, SD_function (id, tannot_opt), ctx) | P.SD_funcl funcl -> (None, SD_funcl (to_ast_funcl None [] ctx funcl), ctx) | P.SD_variant (id, parse_typq) -> let id = to_ast_id ctx id in @@ -1904,15 +1905,6 @@ let to_ast_loop_measure ctx = function | P.Loop (P.While, exp) -> (While, map_exp_annot (fun (l, _) -> (l, ())) @@ to_ast_exp ctx exp) | P.Loop (P.Until, exp) -> (Until, map_exp_annot (fun (l, _) -> (l, ())) @@ to_ast_exp ctx exp) -(* Annotations on some scattered constructs will not be preserved after de-scattering, so warn about this *) -let check_annotation (DEF_aux (aux, def_annot)) = - if Option.is_some def_annot.doc_comment || not (Util.list_empty def_annot.attrs) then ( - match aux with - | DEF_scattered (SD_aux ((SD_function _ | SD_mapping _ | SD_end _), _)) -> - Reporting.warn "" def_annot.loc "Documentation comments and attributes will not be preserved on this definition" - | _ -> () - ) - let pragma_arg_loc pragma arg_left_trim l = let open Lexing in Reporting.map_loc_range @@ -2038,7 +2030,6 @@ let to_ast ctx (P.Defs files) = List.fold_left (fun (defs, ctx) def -> let new_defs, ctx = to_ast_def None [] None ctx def in - List.iter check_annotation new_defs; (new_defs @ defs, ctx) ) ([], ctx) defs diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index a538bb533..64f162482 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -772,37 +772,42 @@ module Make (C : CONFIG) = struct let ctyp = ctyp_of_typ ctx typ in let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in let compile_case case_match_id case_return_id (apat, guard, body) = - let trivial_guard = - match guard with - | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _) - | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _) -> - true - | _ -> false - in - let pre_destructure, destructure, destructure_cleanup, ctx = - compile_match ctx apat cval (fun l b -> icopy l (CL_id (case_match_id, CT_bool)) (V_call (Bnot, [b]))) - in - let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in - let body_setup, body_call, body_cleanup = compile_aexp ctx body in - [iinit l CT_bool case_match_id (V_lit (VL_bool true, CT_bool)); idecl l ctyp case_return_id] - @ pre_destructure @ destructure - @ ( if not trivial_guard then ( - let gs = ngensym () in - guard_setup - @ [idecl l CT_bool gs; guard_call (CL_id (gs, CT_bool))] - @ guard_cleanup - @ [ - iif l - (V_call (Bnot, [V_id (gs, CT_bool)])) - (destructure_cleanup @ [icopy l (CL_id (case_match_id, CT_bool)) (V_lit (VL_bool false, CT_bool))]) - [] CT_unit; - ] + if is_dead_aexp body then [] + else ( + let trivial_guard = + match guard with + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _) + | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _) -> + true + | _ -> false + in + let pre_destructure, destructure, destructure_cleanup, ctx = + compile_match ctx apat cval (fun l b -> icopy l (CL_id (case_match_id, CT_bool)) (V_call (Bnot, [b]))) + in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + [iinit l CT_bool case_match_id (V_lit (VL_bool true, CT_bool)); idecl l ctyp case_return_id] + @ pre_destructure @ destructure + @ ( if not trivial_guard then ( + let gs = ngensym () in + guard_setup + @ [idecl l CT_bool gs; guard_call (CL_id (gs, CT_bool))] + @ guard_cleanup + @ [ + iif l + (V_call (Bnot, [V_id (gs, CT_bool)])) + (destructure_cleanup + @ [icopy l (CL_id (case_match_id, CT_bool)) (V_lit (VL_bool false, CT_bool))] + ) + [] CT_unit; + ] + ) + else [] ) - else [] - ) - @ body_setup - @ [body_call (CL_id (case_return_id, ctyp))] - @ body_cleanup @ destructure_cleanup + @ body_setup + @ [body_call (CL_id (case_return_id, ctyp))] + @ body_cleanup @ destructure_cleanup + ) in let case_ids, cases = List.map diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index 6d4fe318c..bd74d7e2f 100644 --- a/src/lib/parse_ast.ml +++ b/src/lib/parse_ast.ml @@ -375,7 +375,7 @@ type outcome_spec_aux = (* outcome declaration *) type outcome_spec = OV_aux of outcome_spec_aux * l type fundef_aux = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effect_opt * funcl list + | FD_function of rec_opt * tannot_opt * funcl list type type_def_aux = (* Type definition body *) @@ -395,7 +395,7 @@ type dec_spec_aux = (* Register declarations *) type scattered_def_aux = (* Function and type union definitions that can be spread across a file. Each one must end in $_$ *) - | SD_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_function of id * tannot_opt (* scattered function definition header *) | SD_funcl of funcl (* scattered function definition clause *) | SD_enum of id (* scattered enumeration definition header *) | SD_enumcl of id * id (* scattered enumeration member clause *) diff --git a/src/lib/parser.mly b/src/lib/parser.mly index 20282f324..96a9dde21 100644 --- a/src/lib/parser.mly +++ b/src/lib/parser.mly @@ -148,7 +148,6 @@ let mk_typqn = TypQ_aux (TypQ_no_forall, Unknown) let mk_tannotn = Typ_annot_opt_aux (Typ_annot_opt_none, Unknown) let mk_tannot typq typ n m = Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), loc n m) -let mk_eannotn = Effect_opt_aux (Effect_opt_none,Unknown) let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m) @@ -1077,7 +1076,7 @@ rec_measure: fun_def: | Function_ rec_measure? funcls - { let funcls, tannot = $3 in mk_fun (FD_function (default_opt mk_recn $2, tannot, mk_eannotn, funcls)) $startpos $endpos } + { let funcls, tannot = $3 in mk_fun (FD_function (default_opt mk_recn $2, tannot, funcls)) $startpos $endpos } fun_def_list: | fun_def @@ -1259,9 +1258,9 @@ scattered_def: | Scattered Union id typaram { mk_sd (SD_variant($3, $4)) $startpos $endpos } | Scattered Union id - { mk_sd (SD_variant($3, mk_typqn)) $startpos $endpos } + { mk_sd (SD_variant ($3, mk_typqn)) $startpos $endpos } | Scattered Function_ id - { mk_sd (SD_function(mk_recn, mk_tannotn, mk_eannotn, $3)) $startpos $endpos } + { mk_sd (SD_function ($3, mk_tannotn)) $startpos $endpos } | Scattered Mapping id { mk_sd (SD_mapping ($3, mk_tannotn)) $startpos $endpos } | Scattered Mapping id Colon funcl_typ diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index 7b1066912..88c4fe2ad 100644 --- a/src/lib/pretty_print_sail.ml +++ b/src/lib/pretty_print_sail.ml @@ -795,7 +795,7 @@ module Printer (Config : PRINT_CONFIG) = struct let doc_scattered (SD_aux (sd_aux, _)) = match sd_aux with - | SD_function (_, _, id) -> string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id + | SD_function (id, _) -> string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id | SD_funcl funcl -> string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl | SD_end id -> string "end" ^^ space ^^ doc_id id | SD_variant (id, TypQ_aux (TypQ_no_forall, _)) -> diff --git a/src/lib/scattered.ml b/src/lib/scattered.ml index 0ccfc21b6..daa9737f7 100644 --- a/src/lib/scattered.ml +++ b/src/lib/scattered.ml @@ -95,10 +95,12 @@ let patch_funcl_loc def_annot (FCL_aux (aux, (_, tannot))) = let patch_mapcl_annot def_annot (MCL_aux (aux, (_, tannot))) = MCL_aux (aux, (Type_check.strip_def_annot def_annot, tannot)) -let rec descatter' accumulator funcls mapcls = function +let rec descatter' annots accumulator funcls mapcls = function (* For scattered functions we collect all the seperate function clauses until we find the last one, then we turn that function clause into a DEF_fundef containing all the clauses. *) + | DEF_aux (DEF_scattered (SD_aux (SD_function (id, _), _)), def_annot) :: defs -> + descatter' (Bindings.add id def_annot annots) accumulator funcls mapcls defs | DEF_aux (DEF_scattered (SD_aux (SD_funcl funcl, (l, tannot))), def_annot) :: defs when last_scattered_funcl (funcl_id funcl) defs -> let funcl = patch_funcl_loc def_annot funcl in @@ -110,43 +112,46 @@ let rec descatter' accumulator funcls mapcls = function let clauses, update_attr = Type_check.(check_funcls_complete l (env_of_tannot tannot) clauses (typ_of_tannot tannot)) in + let def_annot = + Option.value ~default:(mk_def_annot (gen_loc l) def_annot.env) (Bindings.find_opt (funcl_id funcl) annots) + in let accumulator = DEF_aux ( DEF_fundef (FD_aux (FD_function (fake_rec_opt l, no_tannot_opt l, clauses), (gen_loc l, tannot))), - update_attr (mk_def_annot (gen_loc l) def_annot.env) + update_attr def_annot ) :: accumulator in - descatter' accumulator funcls mapcls defs + descatter' annots accumulator funcls mapcls defs | DEF_aux (DEF_scattered (SD_aux (SD_funcl funcl, _)), def_annot) :: defs -> let id = funcl_id funcl in let funcl = patch_funcl_loc def_annot funcl in begin match Bindings.find_opt id funcls with - | Some clauses -> descatter' accumulator (Bindings.add id (funcl :: clauses) funcls) mapcls defs - | None -> descatter' accumulator (Bindings.add id [funcl] funcls) mapcls defs + | Some clauses -> descatter' annots accumulator (Bindings.add id (funcl :: clauses) funcls) mapcls defs + | None -> descatter' annots accumulator (Bindings.add id [funcl] funcls) mapcls defs end (* Scattered mappings are handled the same way as scattered functions *) + | DEF_aux (DEF_scattered (SD_aux (SD_mapping (id, _), _)), def_annot) :: defs -> + descatter' (Bindings.add id def_annot annots) accumulator funcls mapcls defs | DEF_aux (DEF_scattered (SD_aux (SD_mapcl (id, mapcl), (l, tannot))), def_annot) :: defs when last_scattered_mapcl id defs -> let mapcl = patch_mapcl_annot def_annot mapcl in let clauses = match Bindings.find_opt id mapcls with Some clauses -> List.rev (mapcl :: clauses) | None -> [mapcl] in + let def_annot = Option.value ~default:(mk_def_annot (gen_loc l) def_annot.env) (Bindings.find_opt id annots) in let accumulator = - DEF_aux - ( DEF_mapdef (MD_aux (MD_mapping (id, no_tannot_opt l, clauses), (gen_loc l, tannot))), - mk_def_annot (gen_loc l) def_annot.env - ) + DEF_aux (DEF_mapdef (MD_aux (MD_mapping (id, no_tannot_opt l, clauses), (gen_loc l, tannot))), def_annot) :: accumulator in - descatter' accumulator funcls mapcls defs + descatter' annots accumulator funcls mapcls defs | DEF_aux (DEF_scattered (SD_aux (SD_mapcl (id, mapcl), _)), def_annot) :: defs -> let mapcl = patch_mapcl_annot def_annot mapcl in begin match Bindings.find_opt id mapcls with - | Some clauses -> descatter' accumulator funcls (Bindings.add id (mapcl :: clauses) mapcls) defs - | None -> descatter' accumulator funcls (Bindings.add id [mapcl] mapcls) defs + | Some clauses -> descatter' annots accumulator funcls (Bindings.add id (mapcl :: clauses) mapcls) defs + | None -> descatter' annots accumulator funcls (Bindings.add id [mapcl] mapcls) defs end (* For scattered unions, when we find a union declaration we immediately grab all the future clauses and turn it into a @@ -164,7 +169,7 @@ let rec descatter' accumulator funcls mapcls = function :: records @ accumulator in - descatter' accumulator funcls mapcls (filter_union_clauses id defs) + descatter' annots accumulator funcls mapcls (filter_union_clauses id defs) end (* Therefore we should never see SD_unioncl... *) | DEF_aux (DEF_scattered (SD_aux (SD_unioncl _, (l, _))), _) :: _ -> @@ -184,9 +189,9 @@ let rec descatter' accumulator funcls mapcls = function DEF_aux (DEF_type (TD_aux (TD_enum (id, members, false), (gen_loc l, Type_check.empty_tannot))), def_annot) :: accumulator in - descatter' accumulator funcls mapcls (filter_enum_clauses id defs) + descatter' annots accumulator funcls mapcls (filter_enum_clauses id defs) end - | def :: defs -> descatter' (def :: accumulator) funcls mapcls defs + | def :: defs -> descatter' annots (def :: accumulator) funcls mapcls defs | [] -> List.rev accumulator -let descatter ast = { ast with defs = descatter' [] Bindings.empty Bindings.empty ast.defs } +let descatter ast = { ast with defs = descatter' Bindings.empty [] Bindings.empty Bindings.empty ast.defs } diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index f80c2f9f4..d9339b4a7 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -2570,12 +2570,12 @@ and check_case env pat_typ pexp typ = (* AA: Not sure if we still need this *) | exception (Type_error _ as typ_exn) -> ( match pat with - | P_aux (P_lit lit, _) -> + | P_aux (P_lit lit, (l, _)) -> let guard' = mk_exp (E_app_infix (mk_exp (E_id (mk_id "p#")), mk_id "==", mk_exp (E_lit lit))) in let guard = match guard with None -> guard' | Some guard -> mk_exp (E_app_infix (guard, mk_id "&", guard')) in - check_case env pat_typ (Pat_aux (Pat_when (mk_pat (P_id (mk_id "p#")), guard, case), annot)) typ + check_case env pat_typ (Pat_aux (Pat_when (mk_pat ~loc:l (P_id (mk_id "p#")), guard, case), annot)) typ | _ -> raise typ_exn ) @@ -2868,7 +2868,7 @@ and bind_pat env (P_aux (pat_aux, (l, uannot)) as pat) typ = let guard = locate (fun _ -> l) (mk_exp (E_app_infix (mk_exp (E_id var), mk_id "==", mk_exp (E_lit lit)))) in - let typed_pat, env, guards = bind_pat env (mk_pat (P_id var)) typ in + let typed_pat, env, guards = bind_pat env (mk_pat ~loc:l (P_id var)) typ in (typed_pat, env, guard :: guards) | _ -> raise typ_exn ) @@ -4248,7 +4248,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, uannot)) as mp | Local (Immutable, _) | Unbound _ -> begin match Env.lookup_id v other_env with | Local (Immutable, typ) -> - bind_mpat allow_unknown other_env env (mk_mpat (MP_typ (mk_mpat (MP_id v), typ))) typ + bind_mpat allow_unknown other_env env (mk_mpat ~loc:l (MP_typ (mk_mpat ~loc:l (MP_id v), typ))) typ | Unbound _ -> if allow_unknown then (annot_mpat (MP_id v) unknown_typ, env, []) else @@ -4934,7 +4934,14 @@ let rec check_typedef : Env.t -> env def_annot -> uannot type_def -> typed_def l and check_scattered : Env.t -> env def_annot -> uannot scattered_def -> typed_def list * Env.t = fun env def_annot (SD_aux (sdef, (l, uannot))) -> match sdef with - | SD_function (_, _, id) | SD_mapping (id, _) -> ([], Env.add_scattered_id id env) + | SD_function (id, tannot_opt) -> + ( [DEF_aux (DEF_scattered (SD_aux (SD_function (id, tannot_opt), (l, empty_tannot))), def_annot)], + Env.add_scattered_id id env + ) + | SD_mapping (id, tannot_opt) -> + ( [DEF_aux (DEF_scattered (SD_aux (SD_mapping (id, tannot_opt), (l, empty_tannot))), def_annot)], + Env.add_scattered_id id env + ) | SD_end id -> if not (Env.is_scattered_id id env) then typ_error l (string_of_id id ^ " is not a scattered definition, so it cannot be ended") diff --git a/test/typecheck/fail/issue775.expect b/test/typecheck/fail/issue775.expect new file mode 100644 index 000000000..55fd55354 --- /dev/null +++ b/test/typecheck/fail/issue775.expect @@ -0,0 +1,5 @@ +Type error: +fail/issue775.sail:12.49-51: +12 |mapping clause encdec = UTYPE(imm, rd) <-> imm @ rd @ 0b0010111 +  | ^^ +  | Expected bitvector type, got regidx diff --git a/test/typecheck/fail/issue775.sail b/test/typecheck/fail/issue775.sail new file mode 100644 index 000000000..71a1c99c1 --- /dev/null +++ b/test/typecheck/fail/issue775.sail @@ -0,0 +1,12 @@ +default Order dec +$include + +struct regidx = { regidx : bits(5) } + +scattered union ast + +val encdec : ast <-> bits(32) +scattered mapping encdec + +union clause ast = UTYPE : (bits(20), regidx) +mapping clause encdec = UTYPE(imm, rd) <-> imm @ rd @ 0b0010111