Merge pull request #1389 from diffblue/smv-word-constants

SMV: word constants

Author: kroening

CHANGELOG

@@ -1,3 +1,7 @@
+# EBMC 5.9
+
+* SMV: word constants
+
 # EBMC 5.8
 
 * AIG/netlist engine: fix for conversion of extract bits operator

regression/smv/word/word_constants1.desc

@@ -0,0 +1,7 @@
+CORE
+word_constants1.smv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/smv/word/word_constants1.smv

@@ -0,0 +1,18 @@
+MODULE main
+
+SPEC uwconst(123, 8) = 0d8_123;
+SPEC uwconst(123, 8) = 0ud8_123;
+SPEC uwconst(123, 8) = 0h_7b;
+SPEC uwconst(123, 8) = 0uh_7b;
+SPEC uwconst(123, 8) = 0o8_173;
+SPEC uwconst(123, 8) = 0uo8_173;
+SPEC uwconst(123, 8) = 0b_01111011;
+SPEC uwconst(123, 8) = 0ub_01111011;
+SPEC uwconst(123, 8) = 0b8_1111011;
+SPEC uwconst(123, 8) = 0ub8_1111011;
+
+SPEC swconst(123, 8) = 0sd8_123;
+SPEC swconst(123, 8) = 0sh_7b;
+SPEC swconst(123, 8) = 0so8_173;
+SPEC swconst(123, 8) = 0sb_01111011;
+SPEC swconst(123, 8) = 0sb8_1111011;

src/hw_cbmc_irep_ids.h

@@ -41,6 +41,7 @@ IREP_ID_ONE(smv_union)
 IREP_ID_ONE(smv_unsigned_cast)
 IREP_ID_ONE(smv_uwconst)
 IREP_ID_ONE(smv_word1)
+IREP_ID_ONE(smv_word_constant)
 IREP_ID_ONE(smv_H)
 IREP_ID_ONE(smv_bounded_H)
 IREP_ID_ONE(smv_O)

src/smvlang/parser.y

@@ -320,8 +320,9 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
 
 %token IDENTIFIER_Token   "identifier"
 %token QIDENTIFIER_Token  "quoted identifier"
-%token STRING_Token    "quoted string"
+%token STRING_Token   "quoted string"
 %token NUMBER_Token   "number"
+%token WORD_CONSTANT_Token "word constant"
 
 /* operator precedence, low to high */
 %right IMPLIES_Token
@@ -815,6 +816,7 @@ formula    : basic_expr
 
 constant   : boolean_constant
            | integer_constant
+           | word_constant
            ;
 
 boolean_constant:
@@ -841,6 +843,15 @@ integer_constant:
            }
            ;
 
+word_constant:
+             WORD_CONSTANT_Token
+           {
+             init($$, ID_constant);
+             stack_expr($$).set(ID_value, stack_expr($1).id());
+             stack_expr($$).type() = typet{ID_smv_word_constant};
+           }
+           ;
+
 basic_expr : constant
            | identifier
            {

src/smvlang/scanner.l

@@ -188,6 +188,11 @@ void newlocation(YYSTYPE &x)
                   stack_expr(yysmvlval).id(yytext);
 		  return NUMBER_Token;
 		}
+0[us]?[bBoOdDhH][0-9]*_[0-9a-fA-F][_0-9a-fA-F]* {
+                  newstack(yysmvlval);
+                  stack_expr(yysmvlval).id(yytext);
+		  return WORD_CONSTANT_Token;
+		}
 \"[^\"]*\"      {
                   newstack(yysmvlval);
                   std::string tmp(yytext);

src/smvlang/smv_typecheck.cpp

@@ -90,6 +90,7 @@ class smv_typecheckt:public typecheckt
   void typecheck(smv_parse_treet::modulet::itemt &);
   void typecheck_expr_rec(exprt &, modet);
   void convert_expr_to(exprt &, const typet &dest);
+  exprt convert_word_constant(const constant_exprt &);
 
   smv_parse_treet::modulet *modulep;
 
@@ -582,6 +583,123 @@ void smv_typecheckt::typecheck(exprt &expr, modet mode)
 
 /*******************************************************************\
 
+Function: convert_word_constant
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt smv_typecheckt::convert_word_constant(const constant_exprt &src_expr)
+{
+  auto &src = id2string(src_expr.get_value());
+
+  DATA_INVARIANT(src[0] == '0', "word constant grammar");
+
+  std::size_t index = 1;
+  bool is_signed = false;
+
+  DATA_INVARIANT(index < src.size(), "word constant length");
+
+  switch(src[index])
+  {
+  case 's':
+  case 'S':
+    is_signed = true;
+    index++;
+    break;
+
+  case 'u':
+  case 'U':
+    // this is the default
+    index++;
+    break;
+
+  default:;
+  }
+
+  DATA_INVARIANT(index < src.size(), "word constant length");
+
+  unsigned base;
+  switch(src[index])
+  {
+  case 'd':
+  case 'D':
+    base = 10;
+    break;
+
+  case 'h':
+  case 'H':
+    base = 16;
+    break;
+
+  case 'b':
+  case 'B':
+    base = 2;
+    break;
+
+  case 'o':
+  case 'O':
+    base = 8;
+    break;
+
+  default:
+    DATA_INVARIANT(false, "word constant base");
+  }
+
+  index++;
+
+  DATA_INVARIANT(index < src.size(), "word constant length");
+
+  std::optional<mp_integer> bits = {};
+
+  // optional number of bits
+  if(isdigit(src[index]))
+  {
+    std::string bits_str;
+    for(; index < src.size() && isdigit(src[index]); index++)
+    {
+      bits_str += src[index];
+    }
+
+    bits = string2integer(bits_str);
+  }
+
+  std::string digits;
+  digits.reserve(src.size());
+
+  for(; index < src.size(); index++)
+  {
+    if(src[index] != '_')
+      digits.push_back(src[index]);
+  }
+
+  if(!bits.has_value())
+  {
+    if(base == 10)
+      throw errort{}.with_location(src_expr.source_location())
+        << "decimal word constant without width";
+    else if(base == 2)
+      bits = digits.size();
+    else if(base == 8)
+      bits = digits.size() * 3;
+    else if(base == 16)
+      bits = digits.size() * 4;
+  }
+
+  auto digits_int = string2integer(digits, base);
+
+  auto type =
+    bitvector_typet{is_signed ? ID_signedbv : ID_unsignedbv, bits.value()};
+
+  return from_integer(digits_int, type).with_source_location(src_expr);
+}
+
+/*******************************************************************\
+
 Function: smv_typecheckt::typecheck_expr_rec
 
   Inputs:
@@ -845,6 +963,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     {
       // good as is
     }
+    else if(type.id() == ID_smv_word_constant)
+    {
+      // turn into signedbv/unsignedbv
+      expr = convert_word_constant(to_constant_expr(expr));
+    }
     else
     {
       PRECONDITION(false);