SMV: implement bit selection operator

regression/smv/word/bit_selection1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+bit_selection1.smv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This fails to parse.

regression/smv/word/bit_selection1.smv

@@ -0,0 +1,5 @@
+MODULE main
+
+-- From the NuSMV manual
+SPEC 0sb7_1011001[4:1] = 0ub4_1100
+SPEC 0ub3_101[0:0] = 0ub1_1

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)

src/smvlang/parser.y

@@ -821,6 +821,7 @@ term       : constant
            | term mod_Token term      { binary($$, $1, ID_mod, $3); }
            | term GTGT_Token term     { binary($$, $1, ID_shr, $3); }
            | term LTLT_Token term     { binary($$, $1, ID_shl, $3); }
+           | term '[' term ':' term ']' { init($$, ID_smv_bit_selection); mto($$, $1); mto($$, $3); mto($$, $5); }
            | term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); }
            | "word1" '(' term ')'     { unary($$, ID_smv_word1, $3); }
            | "bool" '(' term ')'      { unary($$, ID_smv_bool, $3); }

src/smvlang/smv_typecheck.cpp

@@ -1066,6 +1066,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<mp_integer>(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<mp_integer>(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<std::size_t>(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();