Enforce that bitvectors have non-negative indices always (#723)

* Enforce that bitvectors have non-negative indices always

This requires some refactoring to the typing context, so now we always
check that unexpanded types are well-formed.

* Fix some more tests

* Use UFNIA logic for CVC4

* Add greater than zero constraints to mono casts

* Make changes to bitvector indexing optional

CHANGELOG.md

@@ -1,6 +1,27 @@
 Changelog
 =========
 
+Sail 0.19
+---------
+
+##### Stricter bitvector type indexing
+
+Stricter indexing for bitvector types. Previous versions of Sail
+treated `bitvector('n)` as uninhabited if `'n < 0`, but otherwise
+permitted such bitvector types in signatures. Now the type
+`bitvector('n)` is only well-formed if `'n >= 0`. This is a breaking
+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
+```
+val foo : forall 'n. bits('n) -> bool
+```
+the `'n` type variable will be inferred as:
+```
+val foo : forall ('n : Nat). bits('n) -> bool
+```
+
 Sail 0.18
 ---------
 

lib/concurrency_interface/read_write.sail

@@ -86,7 +86,7 @@ union Access_kind('arch_ak : Type) = {
 $option -lem_extern_type Mem_read_request
 $option -coq_extern_type Mem_read_request
 struct Mem_read_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
-                        'arch_ak: Type), 'n > 0 = {
+                        'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),
   // There may not always be a virtual address, e.g. when translation is off.
   // Additionally, translate reads don't have a (VA, PA) pair in the
@@ -182,7 +182,7 @@ with
 $option -lem_extern_type Mem_write_request
 $option -coq_extern_type Mem_write_request
 struct Mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
-                         'arch_ak : Type), 'n > 0 = {
+                         'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),
   va : option(bits('vasize)),
   pa : 'pa,

lib/vector.sail

@@ -53,7 +53,7 @@ $endif
 
 $include <flow.sail>
 
-type bits('n : Int) = bitvector('n)
+type bits('n) = bitvector('n)
 
 val eq_bits = pure {
   ocaml: "eq_list",
@@ -129,7 +129,7 @@ function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail
 
 overload operator ^ = {sail_mask}
 
-val bitvector_concat = pure {ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec", _: "append"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = pure {ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec", _: "append"} : forall 'n 'm.
   (bits('n), bits('m)) -> bits('n + 'm)
 
 overload append = {bitvector_concat}
@@ -316,7 +316,7 @@ val slice = pure "slice_inc" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm.
   (bits('m), int('o), int('n)) -> bits('n)
 $endif
 
-val replicate_bits = pure "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm)
+val replicate_bits = pure "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), int('m)) -> bits('n * 'm)
 
 val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n)
 function slice_mask(n,i,l) =

src/bin/sail.ml

@@ -274,6 +274,7 @@ let rec options =
       ("-no_warn", Arg.Clear Reporting.opt_warnings, " do not print warnings");
       ("-all_warnings", Arg.Set Reporting.opt_all_warnings, " print all warning messages");
       ("-strict_var", Arg.Set Type_check.opt_strict_var, " require var expressions for variable declarations");
+      ("-strict_bitvector", Arg.Set Initial_check.opt_strict_bitvector, " require bitvectors to be indexed by naturals");
       ("-plugin", Arg.String (fun plugin -> load_plugin options plugin), "<file> load a Sail plugin");
       ("-just_check", Arg.Set opt_just_check, " terminate immediately after typechecking");
       ("-memo_z3", Arg.Set opt_memo_z3, " memoize calls to z3, improving performance when typechecking repeatedly");

src/lib/ast_util.ml

@@ -788,6 +788,12 @@ let quant_map_items f = function
   | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l)
   | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l)
 
+let quant_fold_map_items f acc = function
+  | TypQ_aux (TypQ_no_forall, l) -> (acc, TypQ_aux (TypQ_no_forall, l))
+  | TypQ_aux (TypQ_tq qis, l) ->
+      let acc, qis = Util.fold_left_map f acc qis in
+      (acc, TypQ_aux (TypQ_tq qis, l))
+
 let is_quant_kopt = function QI_aux (QI_id _, _) -> true | _ -> false
 
 let is_quant_constraint = function QI_aux (QI_constraint _, _) -> true | _ -> false

src/lib/ast_util.mli

@@ -414,6 +414,7 @@ val quant_items : typquant -> quant_item list
 val quant_kopts : typquant -> kinded_id list
 val quant_split : typquant -> kinded_id list * n_constraint list
 val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant
+val quant_fold_map_items : ('acc -> quant_item -> 'acc * quant_item) -> 'acc -> typquant -> 'acc * typquant
 
 val is_quant_kopt : quant_item -> bool
 val is_quant_constraint : quant_item -> bool

src/lib/chunk_ast.ml

@@ -460,7 +460,7 @@ let pop_trailing_comment ?space:(n = 0) comments chunks line_num =
     end
 
 let string_of_kind (K_aux (k, _)) =
-  match k with K_type -> "Type" | K_int -> "Int" | K_order -> "Order" | K_bool -> "Bool"
+  match k with K_type -> "Type" | K_int -> "Int" | K_nat -> "Nat" | K_order -> "Order" | K_bool -> "Bool"
 
 (* Right now, let's just assume we never break up kinded-identifiers *)
 let chunk_of_kopt (KOpt_aux (KOpt_kind (special, vars, kind, _), l)) =

src/lib/constant_propagation.ml

@@ -268,7 +268,7 @@ let const_props target ast =
   let interpreter_istate =
     (* Do not interpret undefined_X functions *)
     let open Interpreter in
-    let undefined_builtin_ids = ids_of_defs Initial_check.undefined_builtin_val_specs in
+    let undefined_builtin_ids = ids_of_defs (Initial_check.undefined_builtin_val_specs ()) in
     let remove_primop id = StringMap.remove (string_of_id id) in
     let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in
     let lstate, gstate = Constant_fold.initial_state ast Type_check.initial_env in

src/lib/constraint.ml

@@ -64,7 +64,7 @@ let cvc4_solver =
   {
     command = "cvc4";
     args = (fun input -> [| "-L"; "smtlib2"; "--tlimit=2000"; input |]);
-    header = "(set-logic QF_UFNIA)\n";
+    header = "(set-logic UFNIA)\n";
     footer = "";
     negative_literals = false;
     uninterpret_power = true;
@@ -243,9 +243,14 @@ let to_smt l abstract vars constr =
   (abstract_decs @ var_decs vars, smt_constr, smt_var, !exponentials)
 
 let sailexp_concrete n =
-  List.init (n + 1) (fun i ->
-      sfun "=" [sfun "sailexp" [Atom (string_of_int i)]; Atom (Big_int.to_string (Big_int.pow_int_positive 2 i))]
-  )
+  sfun "forall"
+    [
+      List [List [Atom "n"; Atom "Int"]];
+      sfun "=>" [sfun ">=" [Atom "n"; Atom "0"]; sfun ">=" [sfun "sailexp" [Atom "n"]; Atom "1"]];
+    ]
+  :: List.init (n + 1) (fun i ->
+         sfun "=" [sfun "sailexp" [Atom (string_of_int i)]; Atom (Big_int.to_string (Big_int.pow_int_positive 2 i))]
+     )
 
 let smtlib_of_constraints ?(get_model = false) l abstract vars extra constr :
     string * (kid -> sexpr * bool) * sexpr list =