Merge pull request #1306 from diffblue/smv-extractbits

SMV: conversion for extractbits operator

Author: tautschnig

regression/ebmc/smv-word-level/verilog4.desc

@@ -0,0 +1,7 @@
+CORE
+verilog4.sv
+--smv-word-level
+^LTLSPEC X X extend\(main\.x\[31:1\], 1\) = unsigned\(0sd32_1\)$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-word-level/verilog4.sv

@@ -0,0 +1,12 @@
+module main(input clk);
+
+  reg [31:0] x;
+
+  initial x = 0;
+
+  always @(posedge clk)
+    x = x + 1;
+
+  initial assert property (nexttime[2] x[31:1] == 1);
+
+endmodule

src/smvlang/expr2smv.cpp

@@ -479,6 +479,52 @@ expr2smvt::convert_index(const index_exprt &src, precedencet precedence)
 
 /*******************************************************************\
 
+Function: expr2smvt::convert_extractbits
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2smvt::resultt expr2smvt::convert_extractbits(const extractbits_exprt &expr)
+{
+  const precedencet precedence = precedencet::INDEX;
+  auto op_rec = convert_rec(expr.src());
+
+  std::string dest;
+
+  if(precedence >= op_rec.p)
+    dest += '(';
+  dest += op_rec.s;
+  if(precedence >= op_rec.p)
+    dest += ')';
+
+  dest += '[';
+
+  // We can only do constant indices.
+  if(expr.index().is_constant())
+  {
+    auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(expr.index()));
+    auto width = to_unsignedbv_type(expr.type()).get_width();
+    dest += integer2string(index_int + width - 1);
+    dest += ':';
+    dest += integer2string(index_int);
+  }
+  else
+  {
+    dest += "?:?";
+  }
+
+  dest += ']';
+
+  return {precedence, std::move(dest)};
+}
+
+/*******************************************************************\
+
 Function: expr2smvt::convert_if
 
   Inputs:
@@ -825,6 +871,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
     return convert_binary(to_binary_expr(src), ">>", precedencet::SHIFT);
   }
 
+  else if(src.id() == ID_extractbits)
+    return convert_extractbits(to_extractbits_expr(src));
+
   else if(src.id() == ID_smv_extend)
     return convert_function_application("extend", src);
 

src/smvlang/expr2smv_class.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_SMV_EXPR2SMV_CLASS_H
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -111,6 +112,8 @@ class expr2smvt
   resultt
   convert_unary(const unary_exprt &, const std::string &symbol, precedencet);
 
+  resultt convert_extractbits(const extractbits_exprt &);
+
   resultt convert_index(const index_exprt &, precedencet);
 
   resultt convert_if(const if_exprt &, precedencet);