Various fixes

- Preserve some mapping locations better

- Preserve documentation comments and attributes on scattered mappings
  and functions

- Fix an issue with dead match branches when the eager_control_flow option
  was used in Jib compilation

- Simplify Parse_ast representation of SD_mapping and SD_function

- Re-order Ast.SD_function arguments to match surface syntax

Author: Alasdair

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

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, _)

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

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

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

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 *)

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

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, _)) ->

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 }

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")

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

test/typecheck/fail/issue775.sail

@@ -0,0 +1,12 @@
+default Order dec
+$include <prelude.sail>
+
+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