Update CHANGELOG and fix some warnings

CHANGELOG.md

@@ -13,7 +13,7 @@ permitted such bitvector types in signatures. Now the type
 change, as some previously permitted definitions are now rejected
 without additional constraints. However Sail has a new kind `Nat`
 which allows it to infer these `>= 0` constraints when explicit type
-variables are ommited, so in a function signature
+variables are omitted, so in a function signature
 ```
 val foo : forall 'n. bits('n) -> bool
 ```
@@ -22,6 +22,14 @@ the `'n` type variable will be inferred as:
 val foo : forall ('n : Nat). bits('n) -> bool
 ```
 
+##### Removed support for compressed ELF binaries
+
+As a convenience feature, the Sail C runtime allowed transparently
+loading compressed ELF files directly by using `gzopen`. However, it
+is easy to just manually decompress such files before passing them to
+the runtime, so we have decided to remove this feature in favour
+of fewer build-time dependencies for the Sail C runtime.
+
 Sail 0.18
 ---------
 

src/bin/sail.ml

@@ -153,7 +153,6 @@ let load_plugin opts plugin =
   with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)
 
 let parse_instantiation inst =
-  let open Ast in
   let open Ast_util in
   let open Lexing in
   match String.split_on_char '=' inst with

src/bin/sail_options.ml

@@ -49,7 +49,4 @@
 
 open Libsail
 
-open Ast
-open Ast_util
-
 let opt_instantiations : (Ast.kind_aux -> Ast.typ_arg) Ast_util.Bindings.t ref = ref Ast_util.Bindings.empty

src/gen_lib/sail2_values.lem

@@ -755,7 +755,7 @@ val count_leading_zeros_bv : forall 'a. Bitvector 'a => 'a -> integer
 let count_leading_zeros_bv v = count_leading_zero_bits (bits_of v)
 
 val count_trailing_zero_bits : list bitU -> integer
-let rec count_trailing_zero_bits v = count_leading_zeros_bv (List.reverse v)
+let count_trailing_zero_bits v = count_leading_zeros_bv (List.reverse v)
 
 val count_trailing_zeros_bv : forall 'a. Bitvector 'a => 'a -> integer
 let count_trailing_zeros_bv v = count_trailing_zero_bits (bits_of v)

src/lib/bitfield.ml

@@ -51,14 +51,8 @@ open Ast
 open Ast_defs
 open Ast_util
 
-let constant_bitvector_typ size = bitvector_typ (nconstant size)
 let fun_typschm arg_typs ret_typ = mk_typschm (mk_typquant []) (function_typ arg_typs ret_typ)
 
-let index_of_nexp nexp =
-  match int_of_nexp_opt (nexp_simp nexp) with
-  | Some i -> i
-  | None -> raise (Reporting.err_typ (nexp_loc nexp) "non-constant bitfield index")
-
 let mk_sizeof_exp i = mk_exp (E_sizeof i)
 let mk_id_exp id = mk_exp (E_id id)
 let mk_id_pat id = mk_pat (P_id id)

src/lib/jib_compile.ml

@@ -1980,8 +1980,6 @@ module Make (C : CONFIG) = struct
     if IdSet.is_empty (IdSet.diff polymorphic_functions unreachable_polymorphic_functions) then (cdefs, ctx)
     else specialize_functions ~specialized_calls ctx cdefs
 
-  let is_struct id = function CT_struct (id', _) -> Id.compare id id' = 0 | _ -> false
-
   class contains_struct_visitor id found =
     object
       inherit empty_jib_visitor

src/lib/jib_util.ml

@@ -1064,21 +1064,6 @@ let rec instr_ctyps (I_aux (instr, aux)) =
 
 and instrs_ctyps instrs = List.fold_left CTSet.union CTSet.empty (List.map instr_ctyps instrs)
 
-let rec instr_ctyps_exist pred (I_aux (instr, aux)) =
-  match instr with
-  | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) | I_undefined ctyp -> pred ctyp
-  | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> pred ctyp || pred (cval_ctyp cval)
-  | I_if (cval, instrs1, instrs2, ctyp) ->
-      pred (cval_ctyp cval) || instrs_ctyps_exist pred instrs1 || instrs_ctyps_exist pred instrs2 || pred ctyp
-  | I_funcall (creturn, _, (_, ctyps), cvals) ->
-      pred (creturn_ctyp creturn) || List.exists pred ctyps || Util.map_exists pred cval_ctyp cvals
-  | I_copy (clexp, cval) -> pred (clexp_ctyp clexp) || pred (cval_ctyp cval)
-  | I_block instrs | I_try_block instrs -> instrs_ctyps_exist pred instrs
-  | I_throw cval | I_jump (cval, _) | I_return cval -> pred (cval_ctyp cval)
-  | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_exit _ | I_end _ -> false
-
-and instrs_ctyps_exist pred instrs = List.exists (instr_ctyps_exist pred) instrs
-
 let ctype_def_ctyps = function
   | CTD_enum _ | CTD_abstract _ -> []
   | CTD_struct (_, fields) -> List.map snd fields

src/lib/jib_visitor.ml

@@ -189,8 +189,8 @@ let rec visit_instr vis outer_instr =
     | I_aux (I_jump (cval, label), aux) ->
         let cval' = visit_cval vis cval in
         if cval == cval' then no_change else I_aux (I_jump (cval', label), aux)
-    | I_aux (I_goto _, aux) -> no_change
-    | I_aux (I_label _, aux) -> no_change
+    | I_aux (I_goto _, _) -> no_change
+    | I_aux (I_label _, _) -> no_change
     | I_aux (I_funcall (creturn, extern, (id, ctyps), cvals), aux) ->
         let creturn' = visit_creturn vis creturn in
         let id' = visit_id vis id in
@@ -209,12 +209,12 @@ let rec visit_instr vis outer_instr =
     | I_aux (I_undefined ctyp, aux) ->
         let ctyp' = visit_ctyp vis ctyp in
         if ctyp == ctyp' then no_change else I_aux (I_undefined ctyp', aux)
-    | I_aux (I_exit _, aux) -> no_change
+    | I_aux (I_exit _, _) -> no_change
     | I_aux (I_end name, aux) ->
         let name' = visit_name vis name in
         if name == name' then no_change else I_aux (I_end name', aux)
-    | I_aux (I_comment _, aux) -> no_change
-    | I_aux (I_raw _, aux) -> no_change
+    | I_aux (I_comment _, _) -> no_change
+    | I_aux (I_raw _, _) -> no_change
     | I_aux (I_return cval, aux) ->
         let cval' = visit_cval vis cval in
         if cval == cval' then no_change else I_aux (I_return cval', aux)

src/lib/smt_gen.ml

@@ -49,11 +49,6 @@ open Jib
 open Jib_util
 open Smt_exp
 
-let zencode_uid (id, ctyps) =
-  match ctyps with
-  | [] -> Util.zencode_string (string_of_id id)
-  | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps)
-
 (* Generate SMT definitions in a writer monad that keeps tracks of any
    overflow checks needed. *)
 

src/lib/smt_gen.mli

@@ -177,8 +177,6 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) : sig
 
   val wf_lbits : Smt_exp.smt_exp -> Smt_exp.smt_exp
 
-  val builtin_vector_update : cval -> cval -> cval -> ctyp -> Smt_exp.smt_exp check_writer
-
   (** Create an SMT expression that converts an expression of the jib
       type [from] into an SMT expression for the jib type [into]. Note
       that this function assumes that the input is of the correct

src/lib/type_env.ml

@@ -330,14 +330,6 @@ let lookup_typ_var v tv_info = match KBindings.find_opt v tv_info.vars with Some
 
 let is_shadowed v tv_info = match KBindings.find_opt v tv_info.shadows with Some _ -> true | None -> false
 
-let k_counter = ref 0
-let k_name () =
-  let kid = mk_kid ("k#" ^ string_of_int !k_counter) in
-  incr k_counter;
-  kid
-
-let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (k_name ())) kinds)
-
 let builtin_typs =
   let k_counter = ref 0 in
   let k_name () =

src/lib/util.ml

@@ -134,36 +134,6 @@ struct
   let put_state s _ = ((), s)
 end
 
-module Duplicate (S : Set.S) = struct
-  type dups = No_dups of S.t | Has_dups of S.elt
-
-  let duplicates (x : S.elt list) : dups =
-    let rec f x acc =
-      match x with [] -> No_dups acc | s :: rest -> if S.mem s acc then Has_dups s else f rest (S.add s acc)
-    in
-    f x S.empty
-end
-
-let remove_duplicates l =
-  let l' = List.sort Stdlib.compare l in
-  let rec aux acc l =
-    match (acc, l) with
-    | _, [] -> List.rev acc
-    | [], x :: xs -> aux [x] xs
-    | y :: ys, x :: xs -> if x = y then aux (y :: ys) xs else aux (x :: y :: ys) xs
-  in
-  aux [] l'
-
-let remove_dups compare eq l =
-  let l' = List.sort compare l in
-  let rec aux acc l =
-    match (acc, l) with
-    | _, [] -> List.rev acc
-    | [], x :: xs -> aux [x] xs
-    | y :: ys, x :: xs -> if eq x y then aux (y :: ys) xs else aux (x :: y :: ys) xs
-  in
-  aux [] l'
-
 let lex_ord_list comparison xs ys =
   let rec lex_lists xs ys =
     match (xs, ys) with

src/lib/util.mli

@@ -80,19 +80,6 @@ module State_monad : functor
   val mapM : ('a -> 'b monad) -> 'a list -> 'b list monad
 end
 
-(** Mixed useful things *)
-module Duplicate (S : Set.S) : sig
-  type dups = No_dups of S.t | Has_dups of S.elt
-  val duplicates : S.elt list -> dups
-end
-
-(** [remove_duplicates l] removes duplicate elements from
-    the list l. As a side-effect, the list might be reordered. *)
-val remove_duplicates : 'a list -> 'a list
-
-(** [remove_dups compare eq l] as remove_duplicates but with parameterised comparison and equality *)
-val remove_dups : ('a -> 'a -> int) -> ('a -> 'a -> bool) -> 'a list -> 'a list
-
 (** Lift a comparison order to the lexical order on lists *)
 val lex_ord_list : ('a -> 'a -> int) -> 'a list -> 'a list -> int
 

src/lib/value.ml

@@ -461,7 +461,7 @@ let value_undefined_vector = function
   | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2))
   | _ -> failwith "value undefined_vector"
 
-let value_undefined_range = function [v1; v2] -> v1 | _ -> failwith "value undefined_range"
+let value_undefined_range = function [v; _] -> v | _ -> failwith "value undefined_range"
 
 let value_undefined_list = function [_] -> V_list [] | _ -> failwith "value undefined_list"
 

src/lib/visitor.ml

@@ -114,7 +114,7 @@ type 'a visit_action =
 
 (*** Define the visiting engine ****)
 (* visit all the nodes in an tree *)
-let rec do_visit (vis : 'v) (action : 'a visit_action) (children : 'v -> 'a -> 'a) (node : 'a) : 'a =
+let do_visit (vis : 'v) (action : 'a visit_action) (children : 'v -> 'a -> 'a) (node : 'a) : 'a =
   match action with
   | SkipChildren -> node
   | ChangeTo node' -> node'

src/sail_sv_backend/sv_optimize.ml

@@ -637,6 +637,7 @@ module RemoveUnusedVariables = struct
         List.iter (smt_uses stack uses) input_connections;
         List.iter (place_uses ~output:true stack uses) output_connections
     | SVD_always_comb stmt -> statement_uses stack uses stmt
+    | SVD_initial stmt -> statement_uses stack uses stmt
     | SVD_always_ff stmt ->
         add_use ~raw:true ~read:true (name (mk_id "clk")) stack uses;
         statement_uses stack uses stmt