SMV: bit selection operator

This adds the [ : ] bit selection operator to the SMV frontend.

Author: kroening

src/smvlang/expr2smv.cpp

@@ -184,6 +184,32 @@ expr2smvt::resultt expr2smvt::convert_binary_associative(
 
 /*******************************************************************\
 
+Function: expr2smvt::convert_extractbits
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2smvt::resultt expr2smvt::convert_extractbits(const extractbits_exprt &expr)
+{
+  // we can do constant indices only
+  if(!expr.index().is_constant())
+    return convert_norep(expr);
+
+  auto op_rec = convert_rec(expr.src());
+  auto high_s = integer2string(
+    numeric_cast_v<mp_integer>(to_constant_expr(expr.index())) +
+    to_bitvector_type(expr.type()).width() - 1);
+  auto low_s = convert_rec(expr.index()).s;
+  return {precedencet::INDEX, op_rec.s + '[' + high_s + ':' + low_s + ']'};
+}
+
+/*******************************************************************\
+
 Function: expr2smvt::convert_function_application
 
   Inputs:
@@ -712,6 +738,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
   else if(src.id() == ID_smv_unsigned_cast)
     return convert_function_application("unsigned", src);
 
+  else if(src.id() == ID_extractbits)
+    return convert_extractbits(to_extractbits_expr(src));
+
   else if(src.id() == ID_typecast)
   {
     return convert_rec(to_typecast_expr(src).op());

src/smvlang/expr2smv_class.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_SMV_EXPR2SMV_CLASS_H
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -123,6 +124,8 @@ class expr2smvt
 
   resultt convert_cond(const exprt &);
 
+  resultt convert_extractbits(const extractbits_exprt &);
+
   resultt
   convert_function_application(const std::string &symbol, const exprt &);
 

src/smvlang/parser.y

@@ -297,6 +297,7 @@ static void new_module(YYSTYPE &module)
 %left  COLONCOLON_Token
 %left  UMINUS           /* supplies precedence for unary minus */
 %left  DOT_Token
+%nonassoc '['
 
 %%
 
@@ -690,6 +691,8 @@ term       : variable_name
            | 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 '[' NUMBER_Token ',' NUMBER_Token ']' // bit selection
+                                      { init($$, ID_extractbits); mto($$, $1); mto($$, $3); mto($$, $5); }
            | term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); }
            | term TIMES_Token term    { binary($$, $1, ID_mult, $3); }
            | term DIVIDE_Token term   { binary($$, $1, ID_div, $3); }