From 0e8b9c8ca6925a1da647180e15102ff87c15a5f7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 9 Oct 2025 12:46:19 -0700 Subject: [PATCH] SMV: implement bit selection operator This implements the grammar and type checking for SMV's term[high:low] bit-selection operator. --- CHANGELOG | 1 + regression/smv/word/bit_selection1.desc | 5 +- ...{extractbits1.desc => bit_selection2.desc} | 2 +- .../{extractbits1.smv => bit_selection2.smv} | 0 src/hw_cbmc_irep_ids.h | 1 + src/smvlang/expr2smv.cpp | 38 +++++++++++ src/smvlang/expr2smv_class.h | 2 + src/smvlang/parser.y | 1 + src/smvlang/smv_typecheck.cpp | 63 +++++++++++++++++++ 9 files changed, 110 insertions(+), 3 deletions(-) rename regression/smv/word/{extractbits1.desc => bit_selection2.desc} (71%) rename regression/smv/word/{extractbits1.smv => bit_selection2.smv} (100%) diff --git a/CHANGELOG b/CHANGELOG index 414302293..85747cb7a 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,6 +1,7 @@ # EBMC 5.9 * SMV: word constants +* SMV: bit selection operator # EBMC 5.8 diff --git a/regression/smv/word/bit_selection1.desc b/regression/smv/word/bit_selection1.desc index bdd3f163a..c54891e14 100644 --- a/regression/smv/word/bit_selection1.desc +++ b/regression/smv/word/bit_selection1.desc @@ -1,9 +1,10 @@ -KNOWNBUG +CORE bit_selection1.smv --bound 0 +^\[.*\] -0sd7_39\[4:1\] = 0ud4_12: PROVED .*$ +^\[.*\] 0ud3_5\[0:0\] = 0ud1_1: PROVED .*$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -- -This fails to parse. diff --git a/regression/smv/word/extractbits1.desc b/regression/smv/word/bit_selection2.desc similarity index 71% rename from regression/smv/word/extractbits1.desc rename to regression/smv/word/bit_selection2.desc index 106946ec4..7a3395fcf 100644 --- a/regression/smv/word/extractbits1.desc +++ b/regression/smv/word/bit_selection2.desc @@ -1,5 +1,5 @@ CORE -shift1.smv +bit_selection2.smv ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/smv/word/extractbits1.smv b/regression/smv/word/bit_selection2.smv similarity index 100% rename from regression/smv/word/extractbits1.smv rename to regression/smv/word/bit_selection2.smv diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index fcfca60c2..0f791bad8 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -19,6 +19,7 @@ IREP_ID_ONE(G) IREP_ID_ONE(X) IREP_ID_ONE(smv_abs) IREP_ID_ONE(smv_bitimplies) +IREP_ID_ONE(smv_bit_selection) IREP_ID_ONE(smv_bool) IREP_ID_ONE(smv_count) IREP_ID_ONE(smv_enumeration) diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index c03be94e8..f9791f342 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -544,6 +544,41 @@ expr2smvt::resultt expr2smvt::convert_extractbits(const extractbits_exprt &expr) /*******************************************************************\ +Function: expr2smvt::convert_smv_bit_select + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +expr2smvt::resultt +expr2smvt::convert_smv_bit_selection(const ternary_exprt &expr) +{ + const precedencet precedence = precedencet::INDEX; + auto op_rec = convert_rec(expr.op0()); + + std::string dest; + + if(precedence >= op_rec.p) + dest += '('; + dest += op_rec.s; + if(precedence >= op_rec.p) + dest += ')'; + + dest += '['; + dest += convert_rec(expr.op1()).s; + dest += ':'; + dest += convert_rec(expr.op2()).s; + dest += ']'; + + return {precedence, std::move(dest)}; +} + +/*******************************************************************\ + Function: expr2smvt::convert_if Inputs: @@ -907,6 +942,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src) else if(src.id() == ID_extractbits) return convert_extractbits(to_extractbits_expr(src)); + else if(src.id() == ID_smv_bit_selection) + return convert_smv_bit_selection(to_ternary_expr(src)); + else if(src.id() == ID_smv_extend) return convert_function_application("extend", src); diff --git a/src/smvlang/expr2smv_class.h b/src/smvlang/expr2smv_class.h index 73e5ce6f3..7ee44c563 100644 --- a/src/smvlang/expr2smv_class.h +++ b/src/smvlang/expr2smv_class.h @@ -114,6 +114,8 @@ class expr2smvt resultt convert_extractbits(const extractbits_exprt &); + resultt convert_smv_bit_selection(const ternary_exprt &); + resultt convert_index(const index_exprt &, precedencet); resultt convert_if(const if_exprt &, precedencet); diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index d876587d1..3d6e40852 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -899,6 +899,7 @@ basic_expr : constant | basic_expr GTGT_Token basic_expr { binary($$, $1, ID_shr, $3); } | basic_expr LTLT_Token basic_expr { binary($$, $1, ID_shl, $3); } | basic_expr '[' basic_expr ']' { binary($$, $1, ID_index, $3); } + | basic_expr '[' basic_expr ':' basic_expr ']' { init($$, ID_smv_bit_selection); mto($$, $1); mto($$, $3); mto($$, $5); } | basic_expr COLONCOLON_Token basic_expr { binary($$, $1, ID_concatenation, $3); } | "word1" '(' basic_expr ')' { unary($$, ID_smv_word1, $3); } | "bool" '(' basic_expr ')' { unary($$, ID_smv_bool, $3); } diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 7312d9796..d9f26040c 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1203,6 +1203,62 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode) << "abs expects integer"; } } + else if(expr.id() == ID_smv_bit_selection) // word[high:low] + { + auto &op = to_ternary_expr(expr).op0(); + + typecheck_expr_rec(op, mode); + + if(op.type().id() != ID_unsignedbv && op.type().id() != ID_signedbv) + { + throw errort().with_location(op.source_location()) + << "bit selection expects word"; + } + + auto &high = to_ternary_expr(expr).op1(); + + typecheck_expr_rec(high, OTHER); + + // high must be an integer constant + if(high.type().id() != ID_range && high.type().id() != ID_natural) + { + throw errort().with_location(expr.find_source_location()) + << "bit-select high must be integer, but got " + << to_string(high.type()); + } + + if(high.id() != ID_constant) + throw errort().with_location(expr.find_source_location()) + << "bit-select high must be constant"; + + auto high_int = numeric_cast_v(to_constant_expr(high)); + + auto &low = to_ternary_expr(expr).op2(); + + typecheck_expr_rec(low, OTHER); + + // low must be an integer constant + if(low.type().id() != ID_range && low.type().id() != ID_natural) + { + throw errort().with_location(expr.find_source_location()) + << "bit-select low must be integer, but got " << to_string(low.type()); + } + + if(low.id() != ID_constant) + throw errort().with_location(expr.find_source_location()) + << "bit-select low must be constant"; + + auto low_int = numeric_cast_v(to_constant_expr(low)); + + if(low_int > high_int) + throw errort().with_location(expr.find_source_location()) + << "bit-select high must not be smaller than low"; + + auto width = numeric_cast_v(high_int - low_int + 1); + + // always unsigned, even if op is signed + expr.type() = unsignedbv_typet{width}; + } else if(expr.id() == ID_smv_bool) { auto &op = to_unary_expr(expr).op(); @@ -1623,6 +1679,13 @@ void smv_typecheckt::lower_node(exprt &expr) const auto &implies = to_smv_bitimplies_expr(expr); expr = bitor_exprt{bitnot_exprt{implies.op0()}, implies.op1()}; } + else if(expr.id() == ID_smv_bit_selection) + { + // we'll lower to extractbits + auto &bit_selection = to_ternary_expr(expr); + expr = extractbits_exprt{ + bit_selection.op0(), bit_selection.op2(), bit_selection.type()}; + } // lower the type lower(expr.type());