SMV: implement bit selection operator

This implements the grammar and type checking for SMV's term[high:low]
bit-selection operator.

Author: kroening

CHANGELOG

@@ -1,6 +1,7 @@
 # EBMC 5.9
 
 * SMV: word constants
+* SMV: bit selection operator
 
 # EBMC 5.8
 

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.

regression/smv/word/extractbits1.desc renamed to regression/smv/word/bit_selection2.desc

@@ -1,5 +1,5 @@
 CORE
-shift1.smv
+bit_selection2.smv
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/smv/word/extractbits1.smv renamed to regression/smv/word/bit_selection2.smv

@@ -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/hw_cbmc_irep_ids.h

@@ -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);
 

src/smvlang/expr2smv.cpp

@@ -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);

src/smvlang/expr2smv_class.h

@@ -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); }

src/smvlang/parser.y

@@ -1206,6 +1206,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();
@@ -1626,6 +1682,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());