From 3003a6ddbd55776181018371ebc50b7f81de5590 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 24 Jan 2024 17:32:53 +0000 Subject: [PATCH] Allow constant expressions in bitfield widths Previously we looked just for literal constants Fixes issue 431 --- src/lib/ast_util.ml | 20 ++++++ src/lib/ast_util.mli | 2 + src/lib/type_check.ml | 64 ++++++++++--------- test/c/nexp_simp_euclidian.expect | 1 + test/c/nexp_simp_euclidian.sail | 24 +++++++ test/lem/run_tests.py | 8 +++ test/typecheck/pass/bitfield_abs.sail | 9 +++ test/typecheck/pass/bitfield_exponential.sail | 9 +++ test/typecheck/pass/bitfield_mod.sail | 10 +++ 9 files changed, 117 insertions(+), 30 deletions(-) create mode 100644 test/c/nexp_simp_euclidian.expect create mode 100644 test/c/nexp_simp_euclidian.sail create mode 100644 test/typecheck/pass/bitfield_abs.sail create mode 100644 test/typecheck/pass/bitfield_exponential.sail create mode 100644 test/typecheck/pass/bitfield_mod.sail diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index 73ccfef9c..4f157cd30 100644 --- a/src/lib/ast_util.ml +++ b/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 diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index 0392729d9..8dddee4f0 100644 --- a/src/lib/ast_util.mli +++ b/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 diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 618b28665..d89c5be12 100644 --- a/src/lib/type_check.ml +++ b/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 = diff --git a/test/c/nexp_simp_euclidian.expect b/test/c/nexp_simp_euclidian.expect new file mode 100644 index 000000000..9766475a4 --- /dev/null +++ b/test/c/nexp_simp_euclidian.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/nexp_simp_euclidian.sail b/test/c/nexp_simp_euclidian.sail new file mode 100644 index 000000000..a90185e05 --- /dev/null +++ b/test/c/nexp_simp_euclidian.sail @@ -0,0 +1,24 @@ +default Order dec + +$include +$include + +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"); +} diff --git a/test/lem/run_tests.py b/test/lem/run_tests.py index 9f02cd9c5..f661d6f87 100755 --- a/test/lem/run_tests.py +++ b/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()): diff --git a/test/typecheck/pass/bitfield_abs.sail b/test/typecheck/pass/bitfield_abs.sail new file mode 100644 index 000000000..492cbc47b --- /dev/null +++ b/test/typecheck/pass/bitfield_abs.sail @@ -0,0 +1,9 @@ +default Order dec + +$include + +type xlen : Int = abs(-2) + +bitfield foo : bits(xlen) = { + A : 0, +} diff --git a/test/typecheck/pass/bitfield_exponential.sail b/test/typecheck/pass/bitfield_exponential.sail new file mode 100644 index 000000000..d3506365a --- /dev/null +++ b/test/typecheck/pass/bitfield_exponential.sail @@ -0,0 +1,9 @@ +default Order dec + +$include + +type xlen : Int = 2 ^ 2 + +bitfield foo : bits(xlen) = { + A : 0, +} diff --git a/test/typecheck/pass/bitfield_mod.sail b/test/typecheck/pass/bitfield_mod.sail new file mode 100644 index 000000000..690fede29 --- /dev/null +++ b/test/typecheck/pass/bitfield_mod.sail @@ -0,0 +1,10 @@ +default Order dec + +$include +$include + +type xlen : Int = mod(5, 3) + +bitfield foo : bits(xlen) = { + A : 0, +}