Allow constant expressions in bitfield widths

Previously we looked just for literal constants

Fixes issue 431

src/lib/ast_util.ml

@@ -375,6 +375,17 @@ and nexp_simp_aux = function
       | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (Big_int.div c1 c2)
       | _, _ -> Nexp_app (id, [n1; n2])
     end
+  | Nexp_app ((Id_aux (Id "mod", _) as id), [n1; n2]) -> begin
+      let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in
+      let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in
+      match (n1_simp, n2_simp) with
+      | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (Big_int.modulus c1 c2)
+      | _, _ -> Nexp_app (id, [n1; n2])
+    end
+  | Nexp_app ((Id_aux (Id "abs", _) as id), [n]) -> begin
+      let n = nexp_simp n in
+      match n with Nexp_aux (Nexp_constant c, _) -> Nexp_constant (Big_int.abs c) | _ -> Nexp_app (id, [n])
+    end
   | Nexp_exp nexp ->
       let nexp = nexp_simp nexp in
       begin
@@ -386,6 +397,15 @@ and nexp_simp_aux = function
       end
   | nexp -> nexp
 
+let rec get_nexp_constant (Nexp_aux (n, _)) =
+  match nexp_simp_aux n with
+  | Nexp_constant c -> Some c
+  (* nexp_simp does not always expand large existentials *)
+  | Nexp_exp e -> begin
+      match get_nexp_constant e with Some c -> Some (Big_int.pow_int_positive 2 (Big_int.to_int c)) | None -> None
+    end
+  | _ -> None
+
 let rec constraint_simp (NC_aux (nc_aux, l)) =
   let nc_aux =
     match nc_aux with

src/lib/ast_util.mli

@@ -257,6 +257,8 @@ val is_bitvector_typ : typ -> bool
 val nexp_simp : nexp -> nexp
 val constraint_simp : n_constraint -> n_constraint
 
+val get_nexp_constant : nexp -> Big_int.num option
+
 (** If a constraint is a conjunction, return a list of all the top-level conjuncts *)
 val constraint_conj : n_constraint -> n_constraint list
 

src/lib/type_check.ml

@@ -4387,36 +4387,40 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list
       begin
         match typ with
         (* The type of a bitfield must be a constant-width bitvector *)
-        | Typ_aux (Typ_app (v, [A_aux (A_nexp (Nexp_aux (Nexp_constant size, _)), _)]), _)
-          when string_of_id v = "bitvector" ->
-            let rec expand_range_synonyms = function
-              | BF_aux (BF_single nexp, l) -> BF_aux (BF_single (Env.expand_nexp_synonyms env nexp), l)
-              | BF_aux (BF_range (nexp1, nexp2), l) ->
-                  let nexp1 = Env.expand_nexp_synonyms env nexp1 in
-                  let nexp2 = Env.expand_nexp_synonyms env nexp2 in
-                  BF_aux (BF_range (nexp1, nexp2), l)
-              | BF_aux (BF_concat (r1, r2), l) ->
-                  BF_aux (BF_concat (expand_range_synonyms r1, expand_range_synonyms r2), l)
-            in
-            let record_tdef = TD_record (id, mk_typquant [], [(typ, mk_id "bits")], false) in
-            let ranges =
-              List.map (fun (f, r) -> (f, expand_range_synonyms r)) ranges |> List.to_seq |> Bindings.of_seq
-            in
-            let def_annot = add_def_attribute l "bitfield" (Big_int.to_string size) def_annot in
-            let defs =
-              DEF_aux (DEF_type (TD_aux (record_tdef, (l, empty_uannot))), def_annot)
-              :: Bitfield.macro id size (Env.get_default_order env) ranges
-            in
-            let defs, env =
-              try check_defs env defs
-              with Type_error (inner_l, err) ->
-                typ_raise l (Err_inner (Err_other "Error while checking bitfield", inner_l, "Bitfield error", None, err))
-            in
-            let env = Env.add_bitfield id typ ranges env in
-            if !opt_no_bitfield_expansion then
-              ([DEF_aux (DEF_type (TD_aux (unexpanded, (l, empty_tannot))), def_annot)], env)
-            else (defs, env)
-        | _ -> typ_error l "Underlying bitfield type must be a constant-width bitvector"
+        | Typ_aux (Typ_app (v, [A_aux (A_nexp nexp, _)]), _) when string_of_id v = "bitvector" -> begin
+            match get_nexp_constant nexp with
+            | Some size ->
+                let rec expand_range_synonyms = function
+                  | BF_aux (BF_single nexp, l) -> BF_aux (BF_single (Env.expand_nexp_synonyms env nexp), l)
+                  | BF_aux (BF_range (nexp1, nexp2), l) ->
+                      let nexp1 = Env.expand_nexp_synonyms env nexp1 in
+                      let nexp2 = Env.expand_nexp_synonyms env nexp2 in
+                      BF_aux (BF_range (nexp1, nexp2), l)
+                  | BF_aux (BF_concat (r1, r2), l) ->
+                      BF_aux (BF_concat (expand_range_synonyms r1, expand_range_synonyms r2), l)
+                in
+                let record_tdef = TD_record (id, mk_typquant [], [(typ, mk_id "bits")], false) in
+                let ranges =
+                  List.map (fun (f, r) -> (f, expand_range_synonyms r)) ranges |> List.to_seq |> Bindings.of_seq
+                in
+                let def_annot = add_def_attribute l "bitfield" (Big_int.to_string size) def_annot in
+                let defs =
+                  DEF_aux (DEF_type (TD_aux (record_tdef, (l, empty_uannot))), def_annot)
+                  :: Bitfield.macro id size (Env.get_default_order env) ranges
+                in
+                let defs, env =
+                  try check_defs env defs
+                  with Type_error (inner_l, err) ->
+                    typ_raise l
+                      (Err_inner (Err_other "Error while checking bitfield", inner_l, "Bitfield error", None, err))
+                in
+                let env = Env.add_bitfield id typ ranges env in
+                if !opt_no_bitfield_expansion then
+                  ([DEF_aux (DEF_type (TD_aux (unexpanded, (l, empty_tannot))), def_annot)], env)
+                else (defs, env)
+            | None -> typ_error l ("Bitvector width " ^ string_of_nexp nexp ^ " for bitfield must be constant")
+          end
+        | typ -> typ_error l ("Underlying bitfield type " ^ string_of_typ typ ^ " must be a constant-width bitvector")
       end
 
 and check_scattered : Env.t -> def_annot -> uannot scattered_def -> tannot def list * Env.t =

test/c/nexp_simp_euclidian.expect

@@ -0,0 +1 @@
+ok

test/c/nexp_simp_euclidian.sail

@@ -0,0 +1,24 @@
+default Order dec
+
+$include <prelude.sail>
+$include <smt.sail>
+
+type test_div : Int = div(-3, -2)
+
+bitfield b : bits(test_div) = {
+  F : 1 .. 0
+}
+
+register R : b
+
+val main : unit -> unit
+
+function main() = {
+  _prove(constraint(div(-3, -2) == 2));
+  let 'len = length(R.bits);
+  _prove(constraint('len == 2));
+  assert(ediv_int(-3, -2) == 2);
+  assert(tdiv_int(-3, -2) == 1);
+  assert(fdiv_int(-3, -2) == 1);
+  print_endline("ok");
+}

test/lem/run_tests.py

@@ -5,6 +5,8 @@
 import sys
 import hashlib
 
+from shutil import which
+
 mydir = os.path.dirname(__file__)
 os.chdir(mydir)
 sys.path.insert(0, os.path.realpath('..'))
@@ -44,12 +46,18 @@
     'concurrency_interface_dec',
     'concurrency_interface_inc',
     'wf_register_type',
+    'bitfield_exponential',
+    'bitfield_abs',
+    'bitfield_mod',
 }
 
 print('Sail is {}'.format(sail))
 print('Sail dir is {}'.format(sail_dir))
 
 def test_lem(name, opts, skip_list):
+    if which('cvc4') is None:
+        skip_tests.add('type_pow_zero')
+        skip_tests_mwords.add('type_pow_zero')
     banner('Testing Lem {}'.format(name))
     results = Results(name)
     for filenames in chunks(os.listdir(test_dir), parallel()):

test/typecheck/pass/bitfield_abs.sail

@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen : Int = abs(-2)
+
+bitfield foo : bits(xlen) = {
+  A : 0,
+}

test/typecheck/pass/bitfield_exponential.sail

@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen : Int = 2 ^ 2
+
+bitfield foo : bits(xlen) = {
+  A : 0,
+}

test/typecheck/pass/bitfield_mod.sail

@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+$include <smt.sail>
+
+type xlen : Int = mod(5, 3)
+
+bitfield foo : bits(xlen) = {
+  A : 0,
+}