SMV: word types

kroening · kroening · commit 90ef6c44755b · 2025-03-14T17:58:00.000-07:00
This adds support for NuSMV's signed and unsigned word types, mapped to
signedbv/unsignedbv.
diff --git a/CHANGELOG b/CHANGELOG
@@ -3,6 +3,7 @@
 * SystemVerilog: typedefs from package scopes
 * SystemVerilog: assignment patterns with keys for structs
 * SMV: LTL V operator, xnor operator
+* SMV: word types and operators
 
 # EBMC 5.5
 
diff --git a/regression/smv/word/basic1.desc b/regression/smv/word/basic1.desc
@@ -0,0 +1,9 @@
+CORE
+basic1.smv
+--bound 0 --trace
+^  s1 = 0sd8_123 \(01111011\)$
+^  u1 = 0ud8_123 \(01111011\)$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/basic1.smv b/regression/smv/word/basic1.smv
@@ -0,0 +1,11 @@
+MODULE main
+
+VAR u1 : word[8];
+
+ASSIGN u1 := uwconst(123, 8);
+
+VAR s1 : signed word[8];
+
+ASSIGN s1 := swconst(123, 8);
+
+SPEC FALSE
diff --git a/regression/smv/word/basic2.desc b/regression/smv/word/basic2.desc
@@ -0,0 +1,8 @@
+CORE
+basic2.smv
+--bdd
+^\[live\] G F counter = 0ud8_10: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/basic2.smv b/regression/smv/word/basic2.smv
@@ -0,0 +1,8 @@
+MODULE main
+
+VAR counter : word[8];
+
+ASSIGN init(counter) := uwconst(0, 8);
+ASSIGN next(counter) := counter + uwconst(1, 8);
+
+LTLSPEC NAME live := G F counter = uwconst(10, 8)
diff --git a/regression/smv/word/concat1.desc b/regression/smv/word/concat1.desc
@@ -0,0 +1,10 @@
+CORE
+concat1.smv
+
+^\[.*\] 0ud8_123 :: 0ud8_1 = 0ud16_31489: PROVED$
+^\[.*\] 0sd8_123 :: 0sd8_1 = 0ud16_31489: PROVED$
+^\[.*\] 0sd8_123 :: 0ud8_1 = 0ud16_31489: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/concat1.smv b/regression/smv/word/concat1.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+SPEC uwconst(123, 8) :: uwconst(1, 8) = uwconst(31489, 16)
+
+-- concatenation is unsigned
+SPEC swconst(123, 8) :: swconst(1, 8) = uwconst(31489, 16)
+SPEC swconst(123, 8) :: uwconst(1, 8) = uwconst(31489, 16)
diff --git a/regression/smv/word/extractbits1.desc b/regression/smv/word/extractbits1.desc
@@ -0,0 +1,7 @@
+CORE
+shift1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/extractbits1.smv b/regression/smv/word/extractbits1.smv
@@ -0,0 +1,8 @@
+MODULE main
+
+SPEC uwconst(123, 8)[0:0] = uwconst(1, 1)
+SPEC uwconst(123, 8)[7:7] = uwconst(0, 1)
+
+-- always unsigned
+SPEC swconst(123, 8)[0:0] = uwconst(1, 1)
+SPEC swconst(123, 8)[7:7] = uwconst(0, 1)
diff --git a/regression/smv/word/shift1.desc b/regression/smv/word/shift1.desc
@@ -0,0 +1,19 @@
+CORE
+shift1.smv
+
+^\[.*\] 0ud8_123 >> 0 = 0ud8_123: PROVED$
+^\[.*\] 0ud8_123 >> 1 = 0ud8_61: PROVED$
+^\[.*\] 0ud8_123 >> 8 = 0ud8_0: PROVED$
+^\[.*\] 0ud8_123 << 0 = 0ud8_123: PROVED$
+^\[.*\] 0ud8_123 << 1 = 0ud8_246: PROVED$
+^\[.*\] 0ud8_123 << 2 = 0ud8_236: PROVED$
+^\[.*\] 0sd8_123 >> 0 = 0sd8_123: PROVED$
+^\[.*\] 0sd8_123 >> 1 = 0sd8_61: PROVED$
+^\[.*\] 0sd8_123 >> 8 = 0sd8_0: PROVED$
+^\[.*\] 0sd8_123 << 0 = 0sd8_123: PROVED$
+^\[.*\] 0sd8_123 << 1 = -0sd8_10: PROVED$
+^\[.*\] 0sd8_123 << 2 = -0sd8_20: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/shift1.smv b/regression/smv/word/shift1.smv
@@ -0,0 +1,15 @@
+MODULE main
+
+SPEC uwconst(123, 8) >> 0 = uwconst(123, 8)
+SPEC uwconst(123, 8) >> 1 = uwconst(61, 8)
+SPEC uwconst(123, 8) >> 8 = uwconst(0, 8)
+SPEC uwconst(123, 8) << 0 = uwconst(123, 8)
+SPEC uwconst(123, 8) << 1 = uwconst(246, 8)
+SPEC uwconst(123, 8) << 2 = uwconst(236, 8)
+
+SPEC swconst(123, 8) >> 0 = swconst(123, 8)
+SPEC swconst(123, 8) >> 1 = swconst(61, 8)
+SPEC swconst(123, 8) >> 8 = swconst(0, 8)
+SPEC swconst(123, 8) << 0 = swconst(123, 8)
+SPEC swconst(123, 8) << 1 = swconst(-10, 8)
+SPEC swconst(123, 8) << 2 = swconst(-20, 8)
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -17,12 +17,19 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(smv_extend)
 IREP_ID_ONE(smv_next)
 IREP_ID_ONE(smv_iff)
 IREP_ID_TWO(C_smv_iff, "#smv_iff")
+IREP_ID_ONE(smv_resize)
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)
+IREP_ID_ONE(smv_signed_cast)
+IREP_ID_ONE(smv_sizeof)
+IREP_ID_ONE(smv_swconst)
 IREP_ID_ONE(smv_union)
+IREP_ID_ONE(smv_unsigned_cast)
+IREP_ID_ONE(smv_uwconst)
 IREP_ID_ONE(smv_H)
 IREP_ID_ONE(smv_bounded_H)
 IREP_ID_ONE(smv_O)
diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
@@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "expr2smv.h"
 
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/lispexpr.h>
 #include <util/lispirep.h>
 #include <util/namespace.h>
@@ -114,7 +116,7 @@ class expr2smvt
     precedencet &precedence);
 
   bool convert_constant(
-    const exprt &src,
+    const constant_exprt &,
     std::string &dest,
     precedencet &precedence);
 
@@ -508,14 +510,13 @@ Function: expr2smvt::convert_constant
 \*******************************************************************/
 
 bool expr2smvt::convert_constant(
-  const exprt &src,
+  const constant_exprt &src,
   std::string &dest,
   precedencet &precedence)
 {
   precedence = precedencet::MAX;
 
-  const typet &type=src.type();
-  const std::string &value=src.get_string(ID_value);
+  const typet &type = src.type();
 
   if(type.id()==ID_bool)
   {
@@ -528,7 +529,19 @@ bool expr2smvt::convert_constant(
           type.id()==ID_natural ||
           type.id()==ID_range ||
           type.id()==ID_enumeration)
-    dest=value;
+  {
+    dest = id2string(src.get_value());
+  }
+  else if(type.id() == ID_signedbv || type.id() == ID_unsignedbv)
+  {
+    auto value_int = numeric_cast_v<mp_integer>(src);
+    auto value_abs = value_int < 0 ? -value_int : value_int;
+    auto minus = value_int < 0 ? "-" : "";
+    auto sign_specifier = type.id() == ID_signedbv ? 's' : 'u';
+    auto word_width = to_bitvector_type(type).width();
+    dest = minus + std::string("0") + sign_specifier + 'd' +
+           std::to_string(word_width) + '_' + integer2string(value_abs);
+  }
   else
     return convert_norep(src, dest, precedence);
 
@@ -716,7 +729,7 @@ bool expr2smvt::convert(
     return convert_next_symbol(src, dest, precedence);
 
   else if(src.id()==ID_constant)
-    return convert_constant(src, dest, precedence);
+    return convert_constant(to_constant_expr(src), dest, precedence);
 
   else if(src.id()=="smv_nondet_choice")
     return convert_nondet_choice(src, dest, precedence);
@@ -736,6 +749,24 @@ bool expr2smvt::convert(
   else if(src.id()==ID_cond)
     return convert_cond(src, dest);
 
+  else if(src.id() == ID_concatenation)
+  {
+    return convert_binary(
+      to_binary_expr(src), dest, "::", precedence = precedencet::CONCAT);
+  }
+
+  else if(src.id() == ID_shl)
+  {
+    return convert_binary(
+      to_binary_expr(src), dest, "<<", precedence = precedencet::SHIFT);
+  }
+
+  else if(src.id() == ID_lshr || src.id() == ID_ashr)
+  {
+    return convert_binary(
+      to_binary_expr(src), dest, ">>", precedence = precedencet::SHIFT);
+  }
+
   else // no SMV language expression for internal representation 
     return convert_norep(src, dest, precedence);
 
@@ -838,6 +869,16 @@ bool type2smv(const typet &type, std::string &code, const namespacet &ns)
       code+=')';
     }
   }
+  else if(type.id() == ID_signedbv)
+  {
+    code =
+      "signed word[" + std::to_string(to_signedbv_type(type).width()) + ']';
+  }
+  else if(type.id() == ID_unsignedbv)
+  {
+    code =
+      "unsigned word[" + std::to_string(to_unsignedbv_type(type).width()) + ']';
+  }
   else
     return true;
 
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
@@ -264,6 +264,8 @@ static void new_module(YYSTYPE &module)
 %token LT_Token       "<"
 %token GT_Token       ">"
 %token NOTEQUAL_Token "!="
+%token LTLT_Token     "<<"
+%token GTGT_Token     ">>"
 
 %token INC_Token
 %token DEC_Token
@@ -289,8 +291,10 @@ static void new_module(YYSTYPE &module)
 %left  union_Token
 %left  IN_Token NOTIN_Token
 %left  mod_Token /* Precedence from CMU SMV, different from NuSMV */
+%left  LTLT_Token GTGT_Token
 %left  PLUS_Token MINUS_Token
 %left  TIMES_Token DIVIDE_Token
+%left  COLONCOLON_Token
 %left  UMINUS           /* supplies precedence for unary minus */
 %left  DOT_Token
 
@@ -476,6 +480,21 @@ simple_type_specifier:
              stack_type($$).add_subtype()=stack_type($6);
            }
            | boolean_Token { init($$, ID_bool); }
+           | word_Token '[' NUMBER_Token ']'
+           {
+             init($$, ID_unsignedbv);
+             stack_type($$).set(ID_width, stack_expr($3).id());
+           }
+           | signed_Token word_Token '[' NUMBER_Token ']'
+           {
+             init($$, ID_signedbv);
+             stack_type($$).set(ID_width, stack_expr($4).id());
+           }
+           | unsigned_Token word_Token '[' NUMBER_Token ']'
+           {
+             init($$, ID_unsignedbv);
+             stack_type($$).set(ID_width, stack_expr($4).id());
+           }
            | '{' enum_list '}' { $$=$2; }
            | NUMBER_Token DOTDOT_Token NUMBER_Token
            {
@@ -669,6 +688,9 @@ term       : variable_name
            | MINUS_Token term %prec UMINUS
                                       { init($$, ID_unary_minus); mto($$, $2); }
            | 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 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); }
            | term PLUS_Token term     { binary($$, $1, ID_plus, $3); }
@@ -680,6 +702,23 @@ term       : variable_name
            | term OR_Token term       { j_binary($$, $1, ID_or, $3); }
            | term AND_Token term      { j_binary($$, $1, ID_and, $3); }
            | NOT_Token term           { init($$, ID_not); mto($$, $2); }
+           | term EQUAL_Token    term { binary($$, $1, ID_equal, $3); }
+           | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
+           | term LT_Token       term { binary($$, $1, ID_lt, $3); }
+           | term LE_Token       term { binary($$, $1, ID_le, $3); }
+           | term GT_Token       term { binary($$, $1, ID_gt, $3); }
+           | term GE_Token       term { binary($$, $1, ID_ge, $3); }
+           | term union_Token    term { binary($$, $1, ID_smv_union, $3); }
+           | term IN_Token       term { binary($$, $1, ID_smv_setin, $3); }
+           | term NOTIN_Token    term { binary($$, $1, ID_smv_setnotin, $3); }
+           | extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
+           | resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
+           | signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); }
+           | sizeof_Token '(' term ')' { init($$, ID_smv_sizeof); mto($$, $3); }
+           | swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); }
+           | unsigned_Token '(' term ')' { init($$, ID_smv_unsigned_cast); mto($$, $3); }
+           | uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); }
+           /* CTL */
            | AX_Token  term           { init($$, ID_AX);  mto($$, $2); }
            | AF_Token  term           { init($$, ID_AF);  mto($$, $2); }
            | AG_Token  term           { init($$, ID_AG);  mto($$, $2); }
@@ -690,21 +729,13 @@ term       : variable_name
            | A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5); }
            | E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5); }
            | E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5); }
+           /* LTL */
            | F_Token  term            { init($$, ID_F);  mto($$, $2); }
            | G_Token  term            { init($$, ID_G);  mto($$, $2); }
            | X_Token  term            { init($$, ID_X);  mto($$, $2); }
            | term U_Token term        { binary($$, $1, ID_U, $3); }
            | term R_Token term        { binary($$, $1, ID_R, $3); }
            | term V_Token term        { binary($$, $1, ID_R, $3); }
-           | term EQUAL_Token    term { binary($$, $1, ID_equal, $3); }
-           | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
-           | term LT_Token       term { binary($$, $1, ID_lt, $3); }
-           | term LE_Token       term { binary($$, $1, ID_le, $3); }
-           | term GT_Token       term { binary($$, $1, ID_gt, $3); }
-           | term GE_Token       term { binary($$, $1, ID_ge, $3); }
-           | term union_Token    term { binary($$, $1, ID_smv_union, $3); }
-           | term IN_Token       term { binary($$, $1, ID_smv_setin, $3); }
-           | term NOTIN_Token    term { binary($$, $1, ID_smv_setnotin, $3); }
            /* LTL PAST */
            | Y_Token term             { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); }
            | Z_Token term             { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); }
diff --git a/src/smvlang/scanner.l b/src/smvlang/scanner.l
@@ -203,6 +203,8 @@ void newlocation(YYSTYPE &x)
 "|"		return OR_Token;
 "&"		return AND_Token;
 "->"		return IMPLIES_Token;
+">>"		return GTGT_Token;
+"<<"		return LTLT_Token;
 "<->"		return EQUIV_Token;
 "="		return EQUAL_Token;
 "<="		return LE_Token;
@@ -213,6 +215,7 @@ void newlocation(YYSTYPE &x)
 ":="		return BECOMES_Token;
 "."		return DOT_Token;
 ".."		return DOTDOT_Token;
+"::"		return COLONCOLON_Token;
 
 .		return yytext[0];
 
diff --git a/src/smvlang/smv_range.h b/src/smvlang/smv_range.h
@@ -73,6 +73,12 @@ class smv_ranget
     return {from - other.from, to - other.to};
   }
 
+  // unary minus
+  smv_ranget operator-() const
+  {
+    return {-to, -from};
+  }
+
   smv_ranget operator*(const smv_ranget &other) const
   {
     mp_integer p1 = from * other.from;
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
