SMV: bool, count, toint, word1

kroening · kroening · commit 87dc0e6f0ae1 · 2025-07-05T15:15:17.000+01:00
This adds the NuSMV operators bool, count, toint, word to the SMV frontend.
diff --git a/CHANGELOG b/CHANGELOG
@@ -6,6 +6,7 @@
 * SystemVerilog: fix for #-# and #=# for empty matches
 * SystemVerilog: fix for |-> and |=> for empty matches
 * LTL/SVA to Buechi with --buechi
+* SMV: bool, count, toint, word1
 
 # EBMC 5.6
 
diff --git a/regression/smv/expressions/smv_bool1.desc b/regression/smv/expressions/smv_bool1.desc
@@ -0,0 +1,11 @@
+CORE
+smv_bool1.smv
+
+^\[.*\] !bool\(0\): PROVED .*$
+^\[.*\] bool\(1\): PROVED .*$
+^\[.*\] bool\(2\): PROVED .*$
+^\[.*\] !bool\(0ud1_0\): PROVED .*$
+^\[.*\] bool\(0ud1_1\): PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/smv/expressions/smv_bool1.smv b/regression/smv/expressions/smv_bool1.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+CTLSPEC !bool(0)
+CTLSPEC bool(1)
+CTLSPEC bool(2)
+CTLSPEC !bool(uwconst(0, 1))
+CTLSPEC bool(uwconst(1, 1))
diff --git a/regression/smv/expressions/smv_count1.desc b/regression/smv/expressions/smv_count1.desc
@@ -0,0 +1,12 @@
+CORE
+smv_count1.smv
+
+^\[.*\] count\(FALSE\) = 0: PROVED .*$
+^\[.*\] count\(TRUE\) = 1: PROVED .*$
+^\[.*\] count\(FALSE, TRUE\) = 1: PROVED .*$
+^\[.*\] count\(TRUE, FALSE\) = 1: PROVED .*$
+^\[.*\] count\(TRUE, TRUE, TRUE\) = 3: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/expressions/smv_count1.smv b/regression/smv/expressions/smv_count1.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+CTLSPEC count(FALSE) = 0
+CTLSPEC count(TRUE) = 1
+CTLSPEC count(FALSE, TRUE) = 1
+CTLSPEC count(TRUE, FALSE) = 1
+CTLSPEC count(TRUE, TRUE, TRUE) = 3
diff --git a/regression/smv/expressions/smv_toint1.desc b/regression/smv/expressions/smv_toint1.desc
@@ -0,0 +1,14 @@
+KNOWNBUG
+smv_toint1.smv
+
+^\[.*\] toint\(0\) = 0: PROVED .*$
+^\[.*\] toint\(1\) = 1: PROVED .*$
+^\[.*\] toint\(FALSE\) = 0: PROVED .*$
+^\[.*\] toint\(TRUE\) = 1: PROVED .*$
+^\[.*\] toint\(0ud8_1\) = 1: PROVED .*$
+^\[.*\] toint\(-0sd8_1\) = -1: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Missing typecasts.
diff --git a/regression/smv/expressions/smv_toint1.smv b/regression/smv/expressions/smv_toint1.smv
@@ -0,0 +1,8 @@
+MODULE main
+
+CTLSPEC toint(0) = 0
+CTLSPEC toint(1) = 1
+CTLSPEC toint(FALSE) = 0
+CTLSPEC toint(TRUE) = 1
+CTLSPEC toint(uwconst(1, 8)) = 1
+CTLSPEC toint(swconst(-1, 8)) = -1
diff --git a/regression/smv/expressions/smv_word1.desc b/regression/smv/expressions/smv_word1.desc
@@ -0,0 +1,9 @@
+CORE
+smv_word1.smv
+
+^\[.*\] word1\(FALSE\) = 0ud1_0: PROVED .*$
+^\[.*\] word1\(TRUE\) = 0ud1_1: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/expressions/smv_word1.smv b/regression/smv/expressions/smv_word1.smv
@@ -0,0 +1,4 @@
+MODULE main
+
+CTLSPEC word1(FALSE) = uwconst(0, 1)
+CTLSPEC word1(TRUE) = uwconst(1, 1)
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -18,11 +18,14 @@ IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
 IREP_ID_ONE(smv_bitimplies)
+IREP_ID_ONE(smv_bool)
+IREP_ID_ONE(smv_count)
 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_toint)
 IREP_ID_ONE(smv_set)
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)
@@ -32,6 +35,7 @@ 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_word1)
 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
@@ -831,6 +831,18 @@ 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_smv_bool)
+    return convert_function_application("bool", src);
+
+  else if(src.id() == ID_smv_count)
+    return convert_function_application("count", src);
+
+  else if(src.id() == ID_smv_toint)
+    return convert_function_application("toint", src);
+
+  else if(src.id() == ID_smv_word1)
+    return convert_function_application("word1", src);
+
   else if(src.id() == ID_typecast)
   {
     return convert_typecast(to_typecast_expr(src));
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
@@ -94,6 +94,12 @@ Function: init
    stack_expr(x_result).add_to_operands(std::move(lhs), std::move(rhs));
  }
 
+static void unary(YYSTYPE &result, const irep_idt &id, YYSTYPE &op)
+{
+  init(result, id);
+  mto(result, op);
+}
+
 /*******************************************************************\
 
 Function: j_binary
@@ -234,6 +240,7 @@ static void new_module(YYSTYPE &module)
 %token xor_Token	"xor"
 %token xnor_Token	"xnor"
 %token self_Token	"self"
+%token toint_Token	"toint"
 %token TRUE_Token	"TRUE"
 %token FALSE_Token	"FALSE"
 %token count_Token	"count"
@@ -706,11 +713,15 @@ term       : constant
            | 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); }
+           | "word1" '(' term ')'     { unary($$, ID_smv_word1, $3); }
+           | "bool" '(' term ')'      { unary($$, ID_smv_bool, $3); }
+           | "toint" '(' term ')'     { unary($$, ID_smv_toint, $3); }
+           | "count" '(' term_list ')' { $$=$3; stack_expr($$).id(ID_smv_count); }
            | swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); }
            | uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); }
-           | signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); }
-           | unsigned_Token '(' term ')' { init($$, ID_smv_unsigned_cast); mto($$, $3); }
-           | sizeof_Token '(' term ')' { init($$, ID_smv_sizeof); mto($$, $3); }
+           | signed_Token '(' term ')' { unary($$, ID_smv_signed_cast, $3); }
+           | unsigned_Token '(' term ')' { unary($$, ID_smv_unsigned_cast, $3); }
+           | sizeof_Token '(' term ')' { unary($$, ID_smv_sizeof, $3); }
            | extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
            | resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
            | term union_Token term    { binary($$, $1, ID_smv_union, $3); }
@@ -791,6 +802,11 @@ set_body_expr:
            | set_body_expr ',' formula { $$=$1; mto($$, $3); }
            ;
 
+term_list:
+             term { init($$); mto($$, $1); }
+           | term_list ',' term { $$=$1; mto($$, $3); }
+           ;
+
 identifier : IDENTIFIER_Token
            | QIDENTIFIER_Token
            {
diff --git a/src/smvlang/scanner.l b/src/smvlang/scanner.l
@@ -121,6 +121,7 @@ void newlocation(YYSTYPE &x)
 "extend"	token(extend_Token);
 "resize"	token(resize_Token);
 "sizeof"	token(sizeof_Token);
+"toint"		token(toint_Token);
 "uwconst"	token(uwconst_Token);
 "swconst"	token(swconst_Token);
 
diff --git a/src/smvlang/smv_expr.h b/src/smvlang/smv_expr.h
@@ -11,6 +11,29 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include <util/std_expr.h>
 
+class smv_bool_exprt : public unary_exprt
+{
+public:
+  smv_bool_exprt(exprt __op, typet __type)
+    : unary_exprt{ID_smv_bool, std::move(__op), std::move(__type)}
+  {
+  }
+};
+
+inline const smv_bool_exprt &to_smv_bool_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_bool);
+  smv_bool_exprt::check(expr);
+  return static_cast<const smv_bool_exprt &>(expr);
+}
+
+inline smv_bool_exprt &to_smv_bool_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_bool);
+  smv_bool_exprt::check(expr);
+  return static_cast<smv_bool_exprt &>(expr);
+}
+
 class smv_resize_exprt : public binary_exprt
 {
 public:
@@ -164,4 +187,50 @@ inline smv_signed_cast_exprt &to_smv_signed_cast_expr(exprt &expr)
   return static_cast<smv_signed_cast_exprt &>(expr);
 }
 
+class smv_toint_exprt : public unary_exprt
+{
+public:
+  smv_toint_exprt(exprt __op, typet __type)
+    : unary_exprt{ID_smv_toint, std::move(__op), std::move(__type)}
+  {
+  }
+};
+
+inline const smv_toint_exprt &to_smv_toint_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_toint);
+  smv_toint_exprt::check(expr);
+  return static_cast<const smv_toint_exprt &>(expr);
+}
+
+inline smv_toint_exprt &to_smv_toint_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_toint);
+  smv_toint_exprt::check(expr);
+  return static_cast<smv_toint_exprt &>(expr);
+}
+
+class smv_word1_exprt : public unary_exprt
+{
+public:
+  smv_word1_exprt(exprt __op, typet __type)
+    : unary_exprt{ID_smv_word1, std::move(__op), std::move(__type)}
+  {
+  }
+};
+
+inline const smv_word1_exprt &to_smv_word1_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_word1);
+  smv_word1_exprt::check(expr);
+  return static_cast<const smv_word1_exprt &>(expr);
+}
+
+inline smv_word1_exprt &to_smv_word1_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_word1);
+  smv_word1_exprt::check(expr);
+  return static_cast<smv_word1_exprt &>(expr);
+}
+
 #endif // CPROVER_SMV_EXPR_H
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
@@ -1091,6 +1091,65 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     expr =
       from_integer(value, type).with_source_location(expr.source_location());
   }
+  else if(expr.id() == ID_smv_bool)
+  {
+    auto &op = to_unary_expr(expr).op();
+    typecheck_expr_rec(op, mode);
+    if(
+      op.type().id() == ID_bool || op.type().id() == ID_unsignedbv ||
+      op.type().id() == ID_signedbv || op.type().id() == ID_range)
+    {
+      // ok
+    }
+    else
+      throw errort().with_location(expr.source_location())
+        << "bool expects boolean, integer or word";
+
+    expr.type() = bool_typet{};
+  }
+  else if(expr.id() == ID_smv_count)
+  {
+    auto &multi_ary_expr = to_multi_ary_expr(expr);
+    for(auto &op : multi_ary_expr.operands())
+    {
+      typecheck_expr_rec(op, mode);
+      if(op.type().id() != ID_bool)
+        throw errort().with_location(op.source_location())
+          << "count expects boolean arguments";
+    }
+    expr.type() = range_typet{0, multi_ary_expr.operands().size()};
+  }
+  else if(expr.id() == ID_smv_toint)
+  {
+    auto &op = to_unary_expr(expr).op();
+    typecheck_expr_rec(op, mode);
+    if(op.type().id() == ID_bool)
+    {
+      expr.type() = range_typet{0, 1};
+    }
+    else if(op.type().id() == ID_unsignedbv || op.type().id() == ID_signedbv)
+    {
+      auto &op_type = to_integer_bitvector_type(op.type());
+      expr.type() = range_typet{op_type.smallest(), op_type.largest()};
+    }
+    else if(op.type().id() == ID_range)
+    {
+      // leave as is
+      expr.type() = op.type();
+    }
+    else
+      throw errort().with_location(expr.source_location())
+        << "toint expects boolean, integer or word";
+  }
+  else if(expr.id() == ID_smv_word1)
+  {
+    auto &op = to_unary_expr(expr).op();
+    typecheck_expr_rec(op, mode);
+    if(op.type().id() != ID_bool)
+      throw errort().with_location(op.source_location())
+        << "word1 expects boolean argument";
+    expr.type() = unsignedbv_typet{1};
+  }
   else if(
     expr.id() == ID_shr || expr.id() == ID_shl || expr.id() == ID_lshr ||
     expr.id() == ID_ashr)
@@ -1289,7 +1348,42 @@ Function: smv_typecheckt::lower_node
 
 void smv_typecheckt::lower_node(exprt &expr) const
 {
-  if(expr.id() == ID_smv_extend)
+  if(expr.id() == ID_smv_bool)
+  {
+    // turn into equality
+    auto &op = to_smv_bool_expr(expr).op();
+    if(op.type().id() == ID_bool)
+      expr = op;
+    else if(op.type().id() == ID_range)
+    {
+      auto &range = to_range_type(op.type());
+      if(range.includes(0))
+        expr = notequal_exprt{op, to_range_type(op.type()).zero_expr()};
+      else
+        expr = true_exprt{};
+    }
+    else if(op.type().id() == ID_unsignedbv)
+    {
+      expr = notequal_exprt{op, to_unsignedbv_type(op.type()).zero_expr()};
+    }
+    else
+      PRECONDITION(false);
+  }
+  else if(expr.id() == ID_smv_count)
+  {
+    // turn into sum
+    exprt::operandst addends;
+
+    addends.reserve(expr.operands().size());
+    auto zero = from_integer(0, expr.type());
+    auto one = from_integer(1, expr.type());
+
+    for(auto &op : expr.operands())
+      addends.push_back(if_exprt{op, one, zero});
+
+    expr = plus_exprt{std::move(addends), expr.type()};
+  }
+  else if(expr.id() == ID_smv_extend)
   {
     auto &smv_extend = to_smv_extend_expr(expr);
     expr = typecast_exprt{smv_extend.lhs(), smv_extend.type()};
@@ -1334,6 +1428,18 @@ void smv_typecheckt::lower_node(exprt &expr) const
         lhs.type() == rhs.type(), "lhs/rhs of in must have same type");
     }
   }
+  else if(expr.id() == ID_smv_toint)
+  {
+    auto &op = to_smv_toint_expr(expr).op();
+    expr = typecast_exprt{op, expr.type()};
+  }
+  else if(expr.id() == ID_smv_word1)
+  {
+    auto &op = to_smv_word1_expr(expr).op();
+    auto zero = from_integer(0, expr.type());
+    auto one = from_integer(1, expr.type());
+    expr = if_exprt{op, std::move(one), std::move(zero)};
+  }
 }
 
 /*******************************************************************\
