Merge branch 'sail2' into systemverilog2

src/bin/repl.ml

@@ -664,9 +664,9 @@ let handle_input istate input =
   | Failure str ->
       print_endline ("Error: " ^ str);
       istate
-  | Type_check.Type_error (env, _, err) ->
+  | Type_check.Type_error (_, err) ->
       print_endline (Type_error.string_of_type_error err);
-      { istate with env }
+      istate
   | Reporting.Fatal_error err ->
       Reporting.print_error ~interactive:true err;
       istate

src/lib/ast_util.ml

@@ -80,7 +80,7 @@ let add_attribute l attr arg (annot : uannot) = { attrs = (l, attr, arg) :: anno
 let remove_attribute attr1 (annot : uannot) = { attrs = List.filter (fun (_, attr2, _) -> attr1 <> attr2) annot.attrs }
 
 let get_attribute attr annot =
-  List.find_opt (fun (l, attr', arg) -> attr = attr') annot.attrs |> Option.map (fun (l, _, arg) -> (l, arg))
+  List.find_opt (fun (_, attr', _) -> attr = attr') annot.attrs |> Option.map (fun (l, _, arg) -> (l, arg))
 
 let get_attributes annot = annot.attrs
 
@@ -98,7 +98,7 @@ let def_annot_map_loc f (annot : def_annot) = { annot with loc = f annot.loc }
 let add_def_attribute l attr arg (annot : def_annot) = { annot with attrs = (l, attr, arg) :: annot.attrs }
 
 let get_def_attribute attr (annot : def_annot) =
-  List.find_opt (fun (l, attr', arg) -> attr = attr') annot.attrs |> Option.map (fun (l, _, arg) -> (l, arg))
+  List.find_opt (fun (_, attr', _) -> attr = attr') annot.attrs |> Option.map (fun (l, _, arg) -> (l, arg))
 
 type mut = Immutable | Mutable
 
@@ -141,9 +141,9 @@ let gen_loc = function Parse_ast.Generated l -> Parse_ast.Generated l | l -> Par
 let rec is_gen_loc = function
   | Parse_ast.Unknown -> false
   | Parse_ast.Unique (_, l) -> is_gen_loc l
-  | Parse_ast.Generated l -> true
+  | Parse_ast.Generated _ -> true
   | Parse_ast.Hint (_, l1, l2) -> is_gen_loc l1 || is_gen_loc l2
-  | Parse_ast.Range (p1, p2) -> false
+  | Parse_ast.Range _ -> false
 
 let mk_id str = Id_aux (Id str, Parse_ast.Unknown)
 
@@ -529,7 +529,7 @@ let arg_nexp ?loc:(l = Parse_ast.Unknown) n = A_aux (A_nexp n, l)
 let arg_typ ?loc:(l = Parse_ast.Unknown) typ = A_aux (A_typ typ, l)
 let arg_bool ?loc:(l = Parse_ast.Unknown) nc = A_aux (A_bool nc, l)
 
-let arg_kopt (KOpt_aux (KOpt_kind (K_aux (k, _), v), l)) =
+let arg_kopt (KOpt_aux (KOpt_kind (K_aux (k, _), v), _)) =
   match k with K_int -> arg_nexp (nvar v) | K_bool -> arg_bool (nc_var v) | K_type -> arg_typ (mk_typ (Typ_var v))
 
 let nc_not nc = mk_nc (NC_app (mk_id "not", [arg_bool nc]))
@@ -590,7 +590,7 @@ let rec insert_subrange ms (n1, n2) =
 
 let insert_subranges ns ms = List.fold_left insert_subrange ns ms
 
-let rec pattern_vector_subranges (P_aux (aux, (l, _))) =
+let rec pattern_vector_subranges (P_aux (aux, _)) =
   match aux with
   | P_vector_subrange (id, n, m) when Big_int.greater n m -> Bindings.singleton id [(n, m)]
   | P_vector_subrange (id, n, m) -> Bindings.singleton id [(m, n)]

src/lib/callgraph.ml

@@ -408,6 +408,11 @@ let filter_ast_extra cuts g ast keep_std =
     | DEF_aux (DEF_register rdec, def_annot) :: defs when NM.mem (Register (id_of_reg_dec rdec)) g ->
         DEF_aux (DEF_register rdec, def_annot) :: filter_ast' g defs
     | DEF_aux (DEF_register _, _) :: defs -> filter_ast' g defs
+    | DEF_aux (DEF_overload (id, overloads), def_annot) :: defs ->
+        let cut_overload overload =
+          NS.mem (Function overload) cuts || NS.mem (Constructor overload) cuts || NS.mem (Overload overload) cuts
+        in
+        DEF_aux (DEF_overload (id, List.filter cut_overload overloads), def_annot) :: filter_ast' g defs
     | DEF_aux (DEF_val vs, def_annot) :: defs when NM.mem (Function (id_of_val_spec vs)) g ->
         DEF_aux (DEF_val vs, def_annot) :: filter_ast' g defs
     | DEF_aux (DEF_val _, _) :: defs -> filter_ast' g defs

src/lib/constant_fold.ml

@@ -209,7 +209,7 @@ let rw_exp fixed target ok not_ok istate =
         try
           ok ();
           Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot)
-        with Type_error (env, l, err) ->
+        with Type_error (l, err) ->
           (* A type error here would be unexpected, so don't ignore it! *)
           Reporting.warn "" l
             ("Type error when folding constants in "

src/lib/frontend.ml

@@ -127,7 +127,7 @@ let rewrite_ast_initial effect_info env =
     [("initial", fun effect_info env ast -> (Rewriter.rewrite_ast ast, effect_info, env))]
 
 let initial_rewrite effect_info type_envs ast =
-  let ast, _, type_envs = rewrite_ast_initial effect_info type_envs ast in
+  let ast, _, _ = rewrite_ast_initial effect_info type_envs ast in
   (* Recheck after descattering so that the internal type environments
      always have complete variant types *)
   Type_error.check Type_check.initial_env (Type_check.strip_ast ast)

src/lib/initial_check.ml

@@ -405,6 +405,8 @@ let rec to_ast_typ_pat ctx (P.ATyp_aux (aux, l)) =
   | P.ATyp_var kid -> TP_aux (TP_var (to_ast_var kid), l)
   | P.ATyp_app (P.Id_aux (P.Id "int", il), typs) ->
       TP_aux (TP_app (Id_aux (Id "atom", il), List.map (to_ast_typ_pat ctx) typs), l)
+  | P.ATyp_app (P.Id_aux (P.Id "bool", il), typs) ->
+      TP_aux (TP_app (Id_aux (Id "atom_bool", il), List.map (to_ast_typ_pat ctx) typs), l)
   | P.ATyp_app (f, typs) -> TP_aux (TP_app (to_ast_id ctx f, List.map (to_ast_typ_pat ctx) typs), l)
   | _ -> raise (Reporting.err_typ l "Unexpected type in type pattern")
 

src/lib/interpreter.ml

@@ -127,7 +127,7 @@ let fallthrough =
     check_case env exc_typ
       (mk_pexp (Pat_exp (mk_pat (P_id (mk_id "exn")), mk_exp (E_throw (mk_exp (E_id (mk_id "exn")))))))
       unit_typ
-  with Type_error (_, l, err) -> Reporting.unreachable l __POS__ (Type_error.string_of_type_error err)
+  with Type_error (l, err) -> Reporting.unreachable l __POS__ (Type_error.string_of_type_error err)
 
 (**************************************************************************)
 (* 1. Interpreter Monad                                                   *)
@@ -864,7 +864,7 @@ let rec eval_frame' = function
 
 let eval_frame frame =
   try eval_frame' frame
-  with Type_check.Type_error (env, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+  with Type_check.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
 let default_effect_interp state eff =
   let lstate, gstate = state in

src/lib/jib_compile.ml

@@ -145,6 +145,7 @@ type ctx = {
   effect_info : Effects.side_effect_info;
   locals : (mut * ctyp) Bindings.t;
   letbinds : int list;
+  letbind_ids : IdSet.t;
   no_raw : bool;
 }
 
@@ -183,6 +184,7 @@ let initial_ctx env effect_info =
     effect_info;
     locals = Bindings.empty;
     letbinds = [];
+    letbind_ids = IdSet.empty;
     no_raw = false;
   }
 
@@ -1383,13 +1385,14 @@ module Make (C : CONFIG) = struct
         ctx compiled_args arg_ctyps
     in
 
+    let known_ids = IdSet.union ctx.letbind_ids (pat_ids pat) in
     let guard_bindings = ref IdSet.empty in
     let guard_instrs =
       match guard with
       | Some guard ->
           let (AE_aux (_, _, l) as guard) = anf guard in
           guard_bindings := aexp_bindings guard;
-          let guard_aexp = C.optimize_anf ctx (no_shadow (pat_ids pat) guard) in
+          let guard_aexp = C.optimize_anf ctx (no_shadow known_ids guard) in
           let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard_aexp in
           let guard_label = label "guard_" in
           let gs = ngensym () in
@@ -1406,7 +1409,7 @@ module Make (C : CONFIG) = struct
     in
 
     (* Optimize and compile the expression to ANF. *)
-    let aexp = C.optimize_anf ctx (no_shadow (IdSet.union (pat_ids pat) !guard_bindings) (anf exp)) in
+    let aexp = C.optimize_anf ctx (no_shadow (IdSet.union known_ids !guard_bindings) (anf exp)) in
 
     let setup, call, cleanup = compile_aexp ctx aexp in
     let destructure, destructure_cleanup =
@@ -1462,7 +1465,7 @@ module Make (C : CONFIG) = struct
     match aux with
     | DEF_register (DEC_aux (DEC_reg (typ, id, None), _)) -> ([CDEF_register (id, ctyp_of_typ ctx typ, [])], ctx)
     | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), _)) ->
-        let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
+        let aexp = C.optimize_anf ctx (no_shadow ctx.letbind_ids (anf exp)) in
         let setup, call, cleanup = compile_aexp ctx aexp in
         let instrs = setup @ [call (CL_id (global id, ctyp_of_typ ctx typ))] @ cleanup in
         let instrs = unique_names instrs in
@@ -1497,7 +1500,7 @@ module Make (C : CONFIG) = struct
         ([CDEF_type tdef], ctx)
     | DEF_let (LB_aux (LB_val (pat, exp), _)) ->
         let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in
-        let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
+        let aexp = C.optimize_anf ctx (no_shadow ctx.letbind_ids (anf exp)) in
         let setup, call, cleanup = compile_aexp ctx aexp in
         let apat = anf_pat ~global:true pat in
         let gs = ngensym () in
@@ -1514,7 +1517,9 @@ module Make (C : CONFIG) = struct
           @ [ilabel end_label]
         in
         let instrs = unique_names instrs in
-        ([CDEF_let (n, bindings, instrs)], { ctx with letbinds = n :: ctx.letbinds })
+        ( [CDEF_let (n, bindings, instrs)],
+          { ctx with letbinds = n :: ctx.letbinds; letbind_ids = IdSet.union (pat_ids pat) ctx.letbind_ids }
+        )
     (* Only DEF_default that matters is default Order, but all order
        polymorphism is specialised by this point. *)
     | DEF_default _ -> ([], ctx)

src/lib/jib_compile.mli

@@ -104,6 +104,7 @@ type ctx = {
   effect_info : Effects.side_effect_info;
   locals : (mut * ctyp) Bindings.t;
   letbinds : int list;
+  letbind_ids : IdSet.t;
   no_raw : bool;
 }
 

src/lib/jib_optimize.ml

@@ -83,7 +83,7 @@ let optimize_unit instrs =
       end
     | instr -> instr
   in
-  let non_pointless_copy (I_aux (aux, annot)) =
+  let non_pointless_copy (I_aux (aux, _)) =
     match aux with I_decl (CT_unit, _) -> false | I_copy (CL_void, _) -> false | _ -> true
   in
   filter_instrs non_pointless_copy (map_instr_list unit_instr instrs)
@@ -92,17 +92,17 @@ let flat_counter = ref 0
 
 let reset_flat_counter () = flat_counter := 0
 
-let flat_id orig_id =
+let flat_id () =
   let id = mk_id ("$" ^ string_of_int !flat_counter) in
   incr flat_counter;
   name id
 
 let rec flatten_instrs = function
   | I_aux (I_decl (ctyp, decl_id), aux) :: instrs ->
-      let fid = flat_id decl_id in
+      let fid = flat_id () in
       I_aux (I_decl (ctyp, fid), aux) :: flatten_instrs (instrs_rename decl_id fid instrs)
   | I_aux (I_init (ctyp, decl_id, cval), aux) :: instrs ->
-      let fid = flat_id decl_id in
+      let fid = flat_id () in
       I_aux (I_init (ctyp, fid, cval), aux) :: flatten_instrs (instrs_rename decl_id fid instrs)
   | I_aux ((I_block block | I_try_block block), _) :: instrs -> flatten_instrs block @ flatten_instrs instrs
   | I_aux (I_if (cval, then_instrs, else_instrs, _), (_, l)) :: instrs ->

src/lib/monomorphise.ml

@@ -3884,7 +3884,7 @@ module BitvectorSizeCasts = struct
             let arg_typ' = subst_unifiers unifiers arg_typ in
             arg_typ'
           end
-        | _ -> typ_error env l ("Malformed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)
+        | _ -> typ_error l ("Malformed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)
       in
 
       (* Push the cast down, including through constructors *)

src/lib/pattern_completeness.ml

@@ -682,7 +682,7 @@ module Make (C : Config) = struct
          (rows_to_list matrix)
       )
 
-  let split_matrix_ctor ctx c ctor ctor_rows matrix =
+  let split_matrix_ctor ctx c ctor_rows matrix =
     let row_indices = List.fold_left (fun set (r, _) -> IntSet.add r set) IntSet.empty ctor_rows in
     let flatten = function
       | GP_app (_, _, gpats) -> GP_tuple gpats
@@ -844,7 +844,7 @@ module Make (C : Config) = struct
                 | Incomplete unmatcheds -> Incomplete unmatcheds
                 | Completeness_unknown -> Completeness_unknown
                 | Complete cinfo ->
-                    let ctor_matrix = split_matrix_ctor ctx i ctor ctor_rows matrix in
+                    let ctor_matrix = split_matrix_ctor ctx i ctor_rows matrix in
                     if row_matrix_empty ctor_matrix then (
                       let width = row_matrix_width l matrix in
                       Incomplete (undefs_except 0 i (mk_exp (E_app (ctor, [mk_lit_exp L_undef]))) width)
@@ -942,7 +942,7 @@ module Make (C : Config) = struct
             | Completeness_unknown -> None
           end
     with (* For now, if any error occurs just report the pattern match is incomplete *)
-    | exn -> None
+    | _ -> None
 
   let is_complete_funcls_wildcarded ?(keyword = "match") l ctx funcls head_exp_typ =
     let destruct_funcl (FCL_aux (FCL_funcl (id, pexp), annot)) = ((id, annot), pexp) in

src/lib/pretty_print_sail.ml

@@ -590,7 +590,7 @@ let doc_rec (Rec_aux (r, _)) =
   | Rec_nonrec | Rec_rec -> empty
   | Rec_measure (pat, exp) -> braces (doc_pat pat ^^ string " => " ^^ doc_exp exp) ^^ space
 
-let doc_fundef (FD_aux (FD_function (r, _, funcls), annot)) =
+let doc_fundef (FD_aux (FD_function (r, _, funcls), _)) =
   match funcls with
   | [] -> failwith "Empty function list"
   | _ ->
@@ -716,7 +716,7 @@ let doc_typdef (TD_aux (td, _)) =
         (separate space [string "bitfield"; doc_id id; colon; doc_typ typ])
         (surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace)
 
-let doc_spec (VS_aux (v, annot)) =
+let doc_spec =
   let doc_extern ext =
     match ext with
     | Some ext ->
@@ -729,8 +729,8 @@ let doc_spec (VS_aux (v, annot)) =
         equals ^^ space ^^ purity ^^ braces (separate (comma ^^ space) docs)
     | None -> empty
   in
-  match v with
-  | VS_val_spec (ts, id, ext) ->
+  function
+  | VS_aux (VS_val_spec (ts, id, ext), _) ->
       string "val" ^^ space ^^ doc_id id ^^ space ^^ doc_extern ext ^^ colon ^^ space ^^ doc_typschm ts
 
 let doc_prec = function Infix -> string "infix" | InfixL -> string "infixl" | InfixR -> string "infixr"
@@ -812,7 +812,7 @@ let rec doc_def_no_hardline ?(comment = false) (DEF_aux (aux, def_annot)) =
   | DEF_fixity (prec, n, id) ->
       fixities := Bindings.add id (prec, Big_int.to_int n) !fixities;
       separate space [doc_prec prec; doc_int n; doc_id id]
-  | DEF_overload ((Id_aux (_, l) as id), ids) ->
+  | DEF_overload (id, ids) ->
       separate space
         [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
 

src/lib/property.ml

@@ -112,7 +112,7 @@ let add_property_guards props ast =
                         )
                     in
                     try Type_check.check_exp (env_of exp) exp' (typ_of exp)
-                    with Type_error (_, l, err) ->
+                    with Type_error (l, err) ->
                       let msg =
                         "\n\
                          Type error when generating guard for a property.\n\

src/lib/rewrites.ml

@@ -2131,7 +2131,7 @@ let rewrite_vector_concat_assignments env defs =
           in
           begin
             try check_exp env full_exp unit_typ
-            with Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+            with Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
           end
         )
         else E_aux (e_aux, annot)
@@ -2158,7 +2158,7 @@ let rewrite_tuple_assignments env defs =
         let let_exp = mk_exp (E_let (mk_letbind pat (strip_exp exp'), block)) in
         begin
           try check_exp env let_exp unit_typ
-          with Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+          with Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
         end
     | _ -> E_aux (e_aux, annot)
   in
@@ -2930,7 +2930,7 @@ let rewrite_ast_pat_string_append env =
         let mapping_inner_typ =
           match Env.get_val_spec (mk_id mapping_prefix_func) env with
           | _, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [A_aux (A_typ typ, _)]), _)), _) -> typ
-          | _ -> typ_error env Parse_ast.Unknown "mapping prefix func without correct function type?"
+          | _ -> typ_error Parse_ast.Unknown "mapping prefix func without correct function type?"
         in
 
         let s_id = fresh_stringappend_id () in
@@ -5121,7 +5121,7 @@ let rewrite effect_info env rewriters ast =
          (1, (ast, effect_info, env))
          rewriters
       )
-  with Type_check.Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+  with Type_check.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
 let () =
   let open Interactive in

src/lib/scattered.ml

@@ -133,7 +133,7 @@ let rec descatter' accumulator funcls mapcls = function
         :: accumulator
       in
       descatter' accumulator funcls mapcls defs
-  | DEF_aux (DEF_scattered (SD_aux (SD_funcl funcl, (l, _))), def_annot) :: 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