Updates for sail-arm release

We want to ensure that no_devices.sail and devices.sail have the same
effect footprint, because with a snapshot-type release in sail-arm, we
can't rebuild the spec with asl_to_sail every time we switch from
running elf binaries to booting OS's. This commit allows registers to
have arbitrary effects, so registers that are really representing
memory-mapped devices don't have to have the wmem/rmem effect.

19 files changed, 114 insertions, 42 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 14f3346a..c0e9fe02 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -957,7 +957,7 @@ let id_of_val_spec (VS_aux (VS_val_spec (_, id, _, _), _)) = id
 
 let id_of_dec_spec (DEC_aux (ds_aux, _)) =
   match ds_aux with
-  | DEC_reg (_, id) -> id
+  | DEC_reg (_, _, _, id) -> id
   | DEC_config (id, _, _) -> id
   | DEC_alias (id, _) -> id
   | DEC_typ_alias (_, id, _) -> id
@@ -966,7 +966,7 @@ let ids_of_def = function
   | DEF_type td -> IdSet.singleton (id_of_type_def td)
   | DEF_fundef fd -> IdSet.singleton (id_of_fundef fd)
   | DEF_val (LB_aux (LB_val (pat, _), _)) -> pat_ids pat
-  | DEF_reg_dec (DEC_aux (DEC_reg (_, id), _)) -> IdSet.singleton id
+  | DEF_reg_dec (DEC_aux (DEC_reg (_, _, _, id), _)) -> IdSet.singleton id
   | DEF_spec vs -> IdSet.singleton (id_of_val_spec vs)
   | DEF_internal_mutrec fds -> IdSet.of_list (List.map id_of_fundef fds)
   | _ -> IdSet.empty
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 458a5c45..6e21dab6 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1623,8 +1623,8 @@ let fix_destructure fail_label = function
 let letdef_count = ref 0
 
 (** Compile a Sail toplevel definition into an IR definition **)
-let rec compile_def ctx = function
-  | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) ->
+let rec compile_def n total ctx = function
+  | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) ->
      [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx
   | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
      let aexp = analyze_functions ctx analyze_primop (c_literals ctx (no_shadow IdSet.empty (anf exp))) in
@@ -1645,6 +1645,8 @@ let rec compile_def ctx = function
 
   | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) ->
      c_debug (lazy ("Compiling function " ^ string_of_id id));
+     Util.progress "Compiling " (string_of_id id) n total;
+
      (* Find the function's type. *)
      let quant, Typ_aux (fn_typ, _) =
        try Env.get_val_spec id ctx.local_env
@@ -1763,7 +1765,7 @@ let rec compile_def ctx = function
 
   | DEF_internal_mutrec fundefs ->
      let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in
-     List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs
+     List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def n total ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs
 
   | def ->
      c_error ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def def))
@@ -3321,7 +3323,10 @@ let bytecode_ast ctx rewrites (Defs defs) =
   let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in
 
   let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
-  let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
+  let total = List.length defs in
+  let _, chunks, ctx =
+    List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs
+  in
   let cdefs = List.concat (List.rev chunks) in
   rewrites cdefs
 
@@ -3362,8 +3367,13 @@ let compile_ast ctx c_includes (Defs defs) =
     let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in
     let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in
     let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
-    let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in
+
+    let total = List.length defs in
+    let _, chunks, ctx =
+      List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs
+    in
     let cdefs = List.concat (List.rev chunks) in
+
     let cdefs, ctx = specialize_variants ctx [] cdefs in
     let cdefs = sort_ctype_defs cdefs in
     let cdefs = optimize ctx cdefs in
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 99dd5f34..30b8bc96 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -642,8 +642,8 @@ let to_ast_alias_spec ctx (P.E_aux(e, l)) =
 
 let to_ast_dec ctx (P.DEC_aux(regdec,l)) =
   DEC_aux((match regdec with
-           | P.DEC_reg (typ, id) ->
-              DEC_reg (to_ast_typ ctx typ, to_ast_id id)
+           | P.DEC_reg (reffect, weffect, typ, id) ->
+              DEC_reg (to_ast_effects reffect, to_ast_effects weffect, to_ast_typ ctx typ, to_ast_id id)
            | P.DEC_config (id, typ, exp) ->
               DEC_config (to_ast_id id, to_ast_typ ctx typ, to_ast_exp ctx exp)
            | P.DEC_alias (id,e) ->
@@ -932,7 +932,7 @@ let generate_undefineds vs_ids (Defs defs) =
   Defs (undefined_builtins @ undefined_defs defs)
 
 let rec get_registers = function
-  | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) :: defs -> (typ, id) :: get_registers defs
+  | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) :: defs -> (typ, id) :: get_registers defs
   | _ :: defs -> get_registers defs
   | [] -> []
 
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 7f5f49e0..75887b4e 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -393,7 +393,7 @@ let initial_value_for id inits =
 
 let ocaml_dec_spec ctx (DEC_aux (reg, _)) =
   match reg with
-  | DEC_reg (typ, id) ->
+  | DEC_reg (_, _, typ, id) ->
      separate space [string "let"; zencode ctx id; colon;
                      parens (ocaml_typ ctx typ); string "ref"; equals;
                      string "ref"; parens (ocaml_exp ctx (initial_value_for id ctx.register_inits))]
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 00da5afb..cbd2a8c5 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -445,7 +445,7 @@ val_spec_aux =  (* Value type specification *)
 
 type 
 dec_spec_aux =  (* Register declarations *)
-   DEC_reg of atyp * id
+   DEC_reg of atyp * atyp * atyp * id
  | DEC_config of id * atyp * exp
  | DEC_alias of id * exp
  | DEC_typ_alias of atyp * id * exp
diff --git a/src/parser.mly b/src/parser.mly
index 3b42d498..68720048 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1362,7 +1362,11 @@ val_spec_def:
 
 register_def:
   | Register id Colon typ
-    { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
+    { let rreg = mk_typ (ATyp_set [mk_effect BE_rreg $startpos($1) $endpos($1)]) $startpos($1) $endpos($1) in
+      let wreg = mk_typ (ATyp_set [mk_effect BE_wreg $startpos($1) $endpos($1)]) $startpos($1) $endpos($1) in
+      mk_reg_dec (DEC_reg (rreg, wreg, $4, $2)) $startpos $endpos }
+  | Register effect_set effect_set id Colon typ
+    { mk_reg_dec (DEC_reg ($2, $3, $6, $4)) $startpos $endpos }
   | Register Configuration id Colon typ Eq exp
     { mk_reg_dec (DEC_config ($3, $5, $7)) $startpos $endpos }
 
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index a8631886..5a122557 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2203,7 +2203,7 @@ let rec doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),fannot)) =
 
 let doc_dec (DEC_aux (reg, ((l, _) as annot))) =
   match reg with
-  | DEC_reg(typ,id) -> empty
+  | DEC_reg(_,_,typ,id) -> empty
      (*
        let env = env_of_annot annot in
        let rt = Env.base_typ_of env typ in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 6c0c3272..0a1b38f9 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1336,7 +1336,7 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) =
 
 let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
   match reg with
-  | DEC_reg(typ,id) -> empty
+  | DEC_reg(_,_,typ,id) -> empty
      (* if !opt_sequential then empty
      else
        let env = env_of_annot annot in
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 75a7e4f9..becdccc0 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -119,6 +119,12 @@ let rec doc_nexp =
   in
   nexp0
 
+let doc_effect (Effect_aux (aux, _)) =
+  match aux with
+  | Effect_set [] -> string "pure"
+  | Effect_set effs ->
+     braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs))
+
 let rec doc_nc nc =
   let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in
   let rec atomic_nc (NC_aux (nc_aux, _) as nc) =
@@ -570,7 +576,10 @@ let doc_mapdef (MD_aux (MD_mapping (id, typa, mapcls), _)) =
 
 let doc_dec (DEC_aux (reg,_)) =
   match reg with
-  | DEC_reg (typ, id) -> separate space [string "register"; doc_id id; colon; doc_typ typ]
+  | DEC_reg (Effect_aux (Effect_set [BE_aux (BE_rreg, _)], _), Effect_aux (Effect_set [BE_aux (BE_wreg, _)], _), typ, id) ->
+     separate space [string "register"; doc_id id; colon; doc_typ typ]
+  | DEC_reg (reffect, weffect, typ, id) ->
+     separate space [string "register"; doc_effect reffect; doc_effect weffect; doc_id id; colon; doc_typ typ]
   | DEC_config (id, typ, exp) -> separate space [string "register configuration"; doc_id id; colon; doc_typ typ; equals; doc_exp exp]
   | DEC_alias(id,alspec) -> string "ALIAS"
   | DEC_typ_alias(typ,id,alspec) -> string "ALIAS"
diff --git a/src/process_file.ml b/src/process_file.ml
index 12f2b7c0..785d7a18 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -365,7 +365,7 @@ let output libpath out_arg files =
       output1 libpath out_arg f defs)
     files
 
-let rewrite_step defs (name, rewriter) =
+let rewrite_step n total defs (name, rewriter) =
   let t = Profile.start () in
   let defs = rewriter defs in
   Profile.finish ("rewrite " ^ name) t;
@@ -380,10 +380,12 @@ let rewrite_step defs (name, rewriter) =
         opt_ddump_rewrite_ast := Some (f, i + 1)
       end
     | _ -> () in
+  Util.progress "Rewrite " name n total;
   defs
 
 let rewrite rewriters defs =
-  try List.fold_left rewrite_step defs rewriters with
+  let total = List.length rewriters in
+  try snd (List.fold_left (fun (n, defs) rw -> n + 1, rewrite_step n total defs rw) (1, defs) rewriters) with
   | Type_check.Type_error (_, l, err) ->
      raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 39b437f4..03c0e074 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -366,11 +366,20 @@ let rewrite_def rewriters d = match d with
   | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewriter")
 
 let rewrite_defs_base rewriters (Defs defs) =
+  let rec rewrite = function
+    | [] -> []
+    | d :: ds ->
+       let d = rewriters.rewrite_def rewriters d in
+       d :: rewrite ds
+  in
+  Defs (rewrite defs)
+
+let rewrite_defs_base_progress prefix rewriters (Defs defs) =
   let total = List.length defs in
   let rec rewrite n = function
     | [] -> []
     | d :: ds ->
-       if !Profile.opt_profile then Util.progress n total else ();
+       Util.progress (prefix ^ " ") (string_of_int n ^ "/" ^ string_of_int total) n total;
        let d = rewriters.rewrite_def rewriters d in
        d :: rewrite (n + 1) ds
   in
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 9da94a99..53b892d4 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -70,6 +70,9 @@ val rewrite_defs : tannot defs -> tannot defs
 
 val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs
 
+(* Same as rewrite_defs base but display a progress bar when verbosity >= 1 *)
+val rewrite_defs_base_progress : string -> tannot rewriters -> tannot defs -> tannot defs
+
 val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp
 
 val rewrite_pat : tannot rewriters -> tannot pat -> tannot pat
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 88ea5304..be02a63f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2339,7 +2339,7 @@ let rewrite_type_def_typs rw_typ rw_typquant (TD_aux (td, annot)) =
 (* FIXME: other reg_dec types *)
 let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) =
   match ds with
-  | DEC_reg (typ, id) -> DEC_aux (DEC_reg (rw_typ typ, id), annot)
+  | DEC_reg (reffect, weffect, typ, id) -> DEC_aux (DEC_reg (reffect, weffect, rw_typ typ, id), annot)
   | DEC_config (id, typ, exp) -> DEC_aux (DEC_config (id, rw_typ typ, exp), annot)
   | _ -> assert false
 
diff --git a/src/sail.ml b/src/sail.ml
index 7bf7d135..8d095451 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -224,8 +224,8 @@ let options = Arg.align ([
     Arg.Set Rewrites.opt_dmono_continue,
     " continue despite monomorphisation errors");
   ( "-verbose",
-    Arg.Set opt_print_verbose,
-    " (debug) pretty-print the input to standard output");
+    Arg.Int (fun verbosity -> Util.opt_verbosity := verbosity),
+    " produce verbose output");
   ( "-ddump_tc_ast",
     Arg.Set opt_ddump_tc_ast,
     " (debug) dump the typechecked ast to stdout");
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index c7b93dbe..e57b1988 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -463,7 +463,7 @@ let fv_of_rd consider_var (DEC_aux (d, annot)) =
   let open Type_check in
   let env = env_of_annot annot in
   match d with
-  | DEC_reg(t, id) ->
+  | DEC_reg(_, _, t, id) ->
      let t' = Env.expand_synonyms env t in
      init_env (string_of_id id),
      Nameset.union (fv_of_typ consider_var mt mt t) (fv_of_typ consider_var mt mt t')
diff --git a/src/state.ml b/src/state.ml
index 63a07c0e..fb065440 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -69,7 +69,7 @@ let find_registers defs =
   List.fold_left
     (fun acc def ->
       match def with
-      | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), (_, tannot))) ->
+      | DEF_reg_dec (DEC_aux(DEC_reg (_, _, typ, id), (_, tannot))) ->
          let env = match destruct_tannot tannot with
            | Some (env, _, _) -> env
            | _ -> Env.empty
diff --git a/src/type_check.ml b/src/type_check.ml
index 4ed234f2..7746ffee 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1511,10 +1511,21 @@ and unify_constraint l env goals (NC_aux (aux1, _) as nc1) (NC_aux (aux2, _) as
   typ_debug (lazy (Util.("Unify constraint " |> magenta |> clear) ^ string_of_n_constraint nc1 ^ " and " ^ string_of_n_constraint nc2));
   match aux1, aux2 with
   | NC_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_bool nc2)
+  | NC_var v, NC_var v' when Kid.compare v v' = 0 -> KBindings.empty
   | NC_and (nc1a, nc2a), NC_and (nc1b, nc2b) | NC_or (nc1a, nc2a), NC_or (nc1b, nc2b) ->
      merge_uvars l (unify_constraint l env goals nc1a nc1b) (unify_constraint l env goals nc2a nc2b)
   | NC_app (f1, args1), NC_app (f2, args2) when Id.compare f1 f2 = 0 && List.length args1 = List.length args2 ->
      List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ_arg l env goals) args1 args2)
+  | NC_equal (n1a, n2a), NC_equal (n1b, n2b) ->
+     merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b)
+  | NC_not_equal (n1a, n2a), NC_equal (n1b, n2b) ->
+     merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b)
+  | NC_bounded_ge (n1a, n2a), NC_equal (n1b, n2b) ->
+     merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b)
+  | NC_bounded_le (n1a, n2a), NC_equal (n1b, n2b) ->
+     merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b)
+  | NC_true, NC_true -> KBindings.empty
+  | NC_false, NC_false -> KBindings.empty
   | _, _ -> unify_error l ("Could not unify constraints " ^ string_of_n_constraint nc1 ^ " and " ^ string_of_n_constraint nc2)
 
 and unify_order l goals (Ord_aux (aux1, _) as ord1) (Ord_aux (aux2, _) as ord2) =
@@ -4557,9 +4568,9 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   | DEF_spec vs -> check_val_spec env vs
   | DEF_default default -> check_default env default
   | DEF_overload (id, ids) -> [DEF_overload (id, ids)], Env.add_overloads id ids env
-  | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, _))) ->
-     let env = Env.add_register id (mk_effect [BE_rreg]) (mk_effect [BE_wreg]) typ env in
-     [DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, mk_expected_tannot env typ no_effect (Some typ))))], env
+  | DEF_reg_dec (DEC_aux (DEC_reg (reffect, weffect, typ, id), (l, _))) ->
+     let env = Env.add_register id reffect weffect typ env in
+     [DEF_reg_dec (DEC_aux (DEC_reg (reffect, weffect, typ, id), (l, mk_expected_tannot env typ no_effect (Some typ))))], env
   | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), (l, _))) ->
      let checked_exp = crule check_exp env (strip_exp exp) typ in
      let env = Env.add_register id no_effect (mk_effect [BE_config]) typ env in
@@ -4569,14 +4580,18 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
   | DEF_scattered sdef -> check_scattered env sdef
 
-and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
-  fun env (Defs defs) ->
+and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t =
+  fun n total env defs ->
   match defs with
-  | [] -> (Defs []), env
+  | [] -> Defs [], env
   | def :: defs ->
+     Util.progress "Type check " (string_of_int n ^ "/" ^ string_of_int total) n total;
      let (def, env) = check_def env def in
-     let (Defs defs, env) = check env (Defs defs) in
-     (Defs (def @ defs)), env
+     let Defs defs, env = check_defs (n + 1) total env defs in
+     Defs (def @ defs), env
+
+and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+  fun env (Defs defs) -> let total = List.length defs in check_defs 1 total env defs
 
 let initial_env =
   Env.empty
diff --git a/src/util.ml b/src/util.ml
index f9603f8e..0ff00df1 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -96,6 +96,7 @@
 
 let opt_warnings = ref true
 let opt_colors = ref true
+let opt_verbosity = ref 0
 
 let rec last = function
   | [x] -> x
@@ -466,13 +467,31 @@ let log_line str line msg =
 
 let header str n = "\n" ^ str ^ "\n" ^ String.make (String.length str - 9 * n) '='
 
-let progress n total =
-  let len = truncate ((float n /. float total) *. 50.0) in
-  let percent = truncate ((float n /. float total) *. 100.0) in
-  let str = "[" ^ String.make len '=' ^ String.make (50 - len) ' ' ^ "] " ^ string_of_int percent ^ "%" in
-  prerr_string str;
-  if n = total then
-    prerr_char '\n'
+let verbose_endline level str =
+  if level >= !opt_verbosity then
+    prerr_endline str
   else
-    prerr_string ("\x1B[" ^ string_of_int (String.length str) ^ "D");
-  flush stderr
+    ()
+
+let progress prefix msg n total =
+  if !opt_verbosity > 0 then
+    let len = truncate ((float n /. float total) *. 50.0) in
+    let percent = truncate ((float n /. float total) *. 100.0) in
+    let msg =
+      if String.length msg <= 20 then
+        msg ^ ")" ^ String.make (20 - String.length msg) ' '
+      else
+        String.sub msg 0 17 ^ "...)"
+    in
+    let str = prefix ^ "[" ^ String.make len '=' ^ String.make (50 - len) ' ' ^ "] "
+              ^ string_of_int percent ^ "%"
+              ^ " (" ^ msg
+    in
+    prerr_string str;
+    if n = total then
+      prerr_char '\n'
+    else
+      prerr_string ("\x1B[" ^ string_of_int (String.length str) ^ "D");
+    flush stderr
+  else
+    ()
diff --git a/src/util.mli b/src/util.mli
index 591cf47b..51504941 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -53,6 +53,7 @@ val last : 'a list -> 'a
 
 val opt_warnings : bool ref
 val opt_colors : bool ref
+val opt_verbosity : int ref
 
 val butlast : 'a list -> 'a list
 
@@ -264,4 +265,4 @@ val file_encode_string : string -> string
 val log_line : string -> int -> string -> string
 val header : string -> int -> string
 
-val progress : int -> int -> unit
+val progress : string -> string -> int -> int -> unit