SMV: introduce classes for extend, resize, signed, unsigned

src/smvlang/Makefile

@@ -1,4 +1,5 @@
-SRC = smv_language.cpp \
+SRC = smv_expr.cpp \
+      smv_language.cpp \
       smv_parser.cpp \
       smv_typecheck.cpp \
       expr2smv.cpp \

src/smvlang/smv_expr.cpp

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: SMV Expressions
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "smv_expr.h"
+
+#include <util/arith_tools.h>
+#include <util/mathematical_types.h>
+
+smv_resize_exprt::smv_resize_exprt(exprt __op, std::size_t __size, typet __type)
+  : smv_resize_exprt{
+      std::move(__op),
+      from_integer(__size, natural_typet{}),
+      std::move(__type)}
+{
+}
+
+smv_extend_exprt::smv_extend_exprt(exprt __op, std::size_t __size, typet __type)
+  : smv_extend_exprt{
+      std::move(__op),
+      from_integer(__size, natural_typet{}),
+      std::move(__type)}
+{
+}

src/smvlang/smv_expr.h

@@ -0,0 +1,167 @@
+/*******************************************************************\
+
+Module: SMV Expressions
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_EXPR_H
+#define CPROVER_SMV_EXPR_H
+
+#include <util/std_expr.h>
+
+class smv_resize_exprt : public binary_exprt
+{
+public:
+  smv_resize_exprt(exprt __op, constant_exprt __size, typet __type)
+    : binary_exprt{
+        std::move(__op),
+        ID_smv_resize,
+        std::move(__size),
+        std::move(__type)}
+  {
+  }
+
+  smv_resize_exprt(exprt __op, std::size_t __size, typet);
+
+  const exprt &op() const
+  {
+    return op0();
+  }
+
+  exprt &op()
+  {
+    return op0();
+  }
+
+  const constant_exprt &size() const
+  {
+    return static_cast<const constant_exprt &>(op1());
+  }
+
+  constant_exprt &size()
+  {
+    return static_cast<constant_exprt &>(op1());
+  }
+
+protected:
+  using binary_exprt::op0;
+  using binary_exprt::op1;
+};
+
+inline const smv_resize_exprt &to_smv_resize_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_resize);
+  smv_resize_exprt::check(expr);
+  return static_cast<const smv_resize_exprt &>(expr);
+}
+
+inline smv_resize_exprt &to_smv_resize_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_resize);
+  smv_resize_exprt::check(expr);
+  return static_cast<smv_resize_exprt &>(expr);
+}
+
+class smv_extend_exprt : public binary_exprt
+{
+public:
+  smv_extend_exprt(exprt __op, constant_exprt __size, typet __type)
+    : binary_exprt{
+        std::move(__op),
+        ID_smv_extend,
+        std::move(__size),
+        std::move(__type)}
+  {
+  }
+
+  smv_extend_exprt(exprt __op, std::size_t __size, typet);
+
+  const exprt &op() const
+  {
+    return op0();
+  }
+
+  exprt &op()
+  {
+    return op0();
+  }
+
+  const constant_exprt &size() const
+  {
+    return static_cast<const constant_exprt &>(op1());
+  }
+
+  constant_exprt &size()
+  {
+    return static_cast<constant_exprt &>(op1());
+  }
+
+protected:
+  using binary_exprt::op0;
+  using binary_exprt::op1;
+};
+
+inline const smv_extend_exprt &to_smv_extend_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_extend);
+  smv_extend_exprt::check(expr);
+  return static_cast<const smv_extend_exprt &>(expr);
+}
+
+inline smv_extend_exprt &to_smv_extend_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_extend);
+  smv_extend_exprt::check(expr);
+  return static_cast<smv_extend_exprt &>(expr);
+}
+
+class smv_unsigned_cast_exprt : public unary_exprt
+{
+public:
+  smv_unsigned_cast_exprt(exprt __op, typet __type)
+    : unary_exprt{ID_smv_unsigned_cast, std::move(__op), std::move(__type)}
+  {
+  }
+};
+
+inline const smv_unsigned_cast_exprt &
+to_smv_unsigned_cast_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_unsigned_cast);
+  smv_unsigned_cast_exprt::check(expr);
+  return static_cast<const smv_unsigned_cast_exprt &>(expr);
+}
+
+inline smv_unsigned_cast_exprt &to_smv_unsigned_cast_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_unsigned_cast);
+  smv_unsigned_cast_exprt::check(expr);
+  return static_cast<smv_unsigned_cast_exprt &>(expr);
+}
+
+class smv_signed_cast_exprt : public unary_exprt
+{
+public:
+  smv_signed_cast_exprt(exprt __op, typet __type)
+    : unary_exprt{ID_smv_signed_cast, std::move(__op), std::move(__type)}
+  {
+  }
+};
+
+inline const smv_signed_cast_exprt &to_smv_signed_cast_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_signed_cast);
+  smv_signed_cast_exprt::check(expr);
+  return static_cast<const smv_signed_cast_exprt &>(expr);
+}
+
+inline smv_signed_cast_exprt &to_smv_signed_cast_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_signed_cast);
+  smv_signed_cast_exprt::check(expr);
+  return static_cast<smv_signed_cast_exprt &>(expr);
+}
+
+#endif // CPROVER_SMV_EXPR_H

src/smvlang/smv_typecheck.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/typecheck.h>
 
 #include "expr2smv.h"
+#include "smv_expr.h"
 #include "smv_range.h"
 
 #include <algorithm>
@@ -1202,7 +1203,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_unsigned_cast)
   {
     // a reinterpret cast
-    auto &op = to_unary_expr(expr).op();
+    auto &op = to_smv_unsigned_cast_expr(expr).op();
     typecheck_expr_rec(op, mode);
     if(op.type().id() == ID_signedbv)
       expr.type() = unsignedbv_typet{to_signedbv_type(op.type()).get_width()};
@@ -1215,7 +1216,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_signed_cast)
   {
     // a reinterpret cast
-    auto &op = to_unary_expr(expr).op();
+    auto &op = to_smv_signed_cast_expr(expr).op();
     typecheck_expr_rec(op, mode);
     if(op.type().id() == ID_unsignedbv)
       expr.type() = signedbv_typet{to_unsignedbv_type(op.type()).get_width()};
@@ -1248,21 +1249,21 @@ void smv_typecheckt::lower_node(exprt &expr) const
 {
   if(expr.id() == ID_smv_extend)
   {
-    auto &binary = to_binary_expr(expr);
-    expr = typecast_exprt{binary.lhs(), expr.type()};
+    auto &smv_extend = to_smv_extend_expr(expr);
+    expr = typecast_exprt{smv_extend.lhs(), smv_extend.type()};
   }
   else if(expr.id() == ID_smv_resize)
   {
-    auto &binary = to_binary_expr(expr);
-    expr = typecast_exprt{binary.lhs(), expr.type()};
+    auto &smv_resize = to_smv_resize_expr(expr);
+    expr = typecast_exprt{smv_resize.lhs(), smv_resize.type()};
   }
   else if(expr.id() == ID_smv_signed_cast)
   {
-    expr = typecast_exprt{to_unary_expr(expr).op(), expr.type()};
+    expr = typecast_exprt{to_smv_signed_cast_expr(expr).op(), expr.type()};
   }
   else if(expr.id() == ID_smv_unsigned_cast)
   {
-    expr = typecast_exprt{to_unary_expr(expr).op(), expr.type()};
+    expr = typecast_exprt{to_smv_unsigned_cast_expr(expr).op(), expr.type()};
   }
 }