Merge pull request #994 from diffblue/smv-word-type

kroening · web-flow · commit f22a2c14c370 · 2025-03-15T17:39:07.000-07:00
SMV: word types
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/bitwise1.desc b/regression/smv/word/bitwise1.desc
@@ -0,0 +1,14 @@
+CORE
+bitwise1.smv
+
+^\[.*\] !0ud8_123 = 0ud8_132: PROVED$
+^\[.*\] !0sd8_123 = -0sd8_124: PROVED$
+^\[.*\] \(0ud8_123 \& 0ud8_7\) = 0ud8_3: PROVED$
+^\[.*\] \(0ud8_123 \| 0ud8_7\) = 0ud8_127: PROVED$
+^\[.*\] \(0ud8_123 xor 0ud8_7\) = 0ud8_124: PROVED$
+^\[.*\] \(0ud8_123 xnor 0ud8_7\) = 0ud8_131: PROVED$
+^\[.*\] \(0ud8_123 <-> 0ud8_7\) = 0ud8_131: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/bitwise1.smv b/regression/smv/word/bitwise1.smv
@@ -0,0 +1,23 @@
+MODULE main
+
+-- negation
+SPEC !uwconst(123, 8) = uwconst(132, 8)
+SPEC !swconst(123, 8) = swconst(-124, 8)
+
+-- and
+SPEC (uwconst(123, 8) & uwconst(7, 8)) = uwconst(3, 8)
+
+-- or
+SPEC (uwconst(123, 8) | uwconst(7, 8)) = uwconst(127, 8)
+
+-- xor
+SPEC (uwconst(123, 8) xor uwconst(7, 8)) = uwconst(124, 8)
+
+-- xnor
+SPEC (uwconst(123, 8) xnor uwconst(7, 8)) = uwconst(131, 8)
+
+-- implication
+--SPEC (uwconst(123, 8) -> uwconst(7, 8)) = uwconst(135, 8)
+
+-- iff
+SPEC (uwconst(123, 8) <-> uwconst(7, 8)) = uwconst(131, 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/extend1.desc b/regression/smv/word/extend1.desc
@@ -0,0 +1,7 @@
+KNOWNBUG
+extend1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/extend1.smv b/regression/smv/word/extend1.smv
@@ -0,0 +1,4 @@
+MODULE main
+
+SPEC extend(uwconst(1, 1), 7) = uwconst(1, 8)
+SPEC extend(swconst(-1, 1), 7) = swconst(-1, 8)
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/resize1.desc b/regression/smv/word/resize1.desc
@@ -0,0 +1,7 @@
+KNOWNBUG
+resize1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/resize1.smv b/regression/smv/word/resize1.smv
@@ -0,0 +1,4 @@
+MODULE main
+
+SPEC resize(uwconst(1, 1), 8) = uwconst(1, 8)
+SPEC resize(swconst(123, 1), 1) = swconst(-1, 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/regression/smv/word/signed1.desc b/regression/smv/word/signed1.desc
@@ -0,0 +1,7 @@
+KNOWNBUG
+signed1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/signed1.smv b/regression/smv/word/signed1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+SPEC signed(uwconst(1, 1)) = swconst(-1, 1)
diff --git a/regression/smv/word/sizeof1.desc b/regression/smv/word/sizeof1.desc
@@ -0,0 +1,7 @@
+CORE
+sizeof1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/sizeof1.smv b/regression/smv/word/sizeof1.smv
@@ -0,0 +1,4 @@
+MODULE main
+
+SPEC sizeof(uwconst(0, 1)) = 1
+SPEC sizeof(swconst(123, 8)) = 8
diff --git a/regression/smv/word/unsigned1.desc b/regression/smv/word/unsigned1.desc
@@ -0,0 +1,7 @@
+KNOWNBUG
+unsigned1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/word/unsigned1.smv b/regression/smv/word/unsigned1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+SPEC unsigned(swconst(-1, 1)) = uwconst(1, 1)
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -17,12 +17,20 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(smv_bitimplies)
+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);
 
@@ -611,20 +624,25 @@ bool expr2smvt::convert(
     return convert_unary(
       to_not_expr(src), dest, "!", precedence = precedencet::NOT);
 
-  else if(src.id()==ID_and)
+  else if(src.id() == ID_and || src.id() == ID_bitand)
     return convert_binary(src, dest, "&", precedence = precedencet::AND);
 
-  else if(src.id()==ID_or)
+  else if(src.id() == ID_or || src.id() == ID_bitor)
     return convert_binary(src, dest, "|", precedence = precedencet::OR);
 
-  else if(src.id()==ID_implies)
+  else if(src.id() == ID_implies || src.id() == ID_smv_bitimplies)
     return convert_binary(src, dest, "->", precedence = precedencet::IMPLIES);
 
-  else if(src.id() == ID_xor)
+  else if(src.id() == ID_xor || src.id() == ID_bitxor)
     return convert_binary(src, dest, "xor", precedence = precedencet::OR);
 
-  else if(src.id() == ID_xnor)
-    return convert_binary(src, dest, "xnor", precedence = precedencet::OR);
+  else if(src.id() == ID_xnor || src.id() == ID_bitxnor)
+  {
+    if(src.get_bool(ID_C_smv_iff))
+      return convert_binary(src, dest, "<->", precedence = precedencet::IFF);
+    else
+      return convert_binary(src, dest, "xnor", precedence = precedencet::OR);
+  }
 
   else if(
     src.id() == ID_AG || src.id() == ID_EG || src.id() == ID_AF ||
@@ -716,7 +734,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 +754,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 +874,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
diff --git a/src/smvlang/scanner.l b/src/smvlang/scanner.l
diff --git a/src/smvlang/smv_range.h b/src/smvlang/smv_range.h
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
