Merge pull request #435 from diffblue/verilog_bit_select

Verilog: use `ID_verilog_bit_select` for bit-select expressions
diffblue · Apr 15, 2024 · 9e68c85 · 9e68c85
2 parents b86b687 + 24658cf
commit 9e68c85
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 32 deletions.
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -42,7 +42,7 @@ IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)
 IREP_ID_ONE(output_register)
 IREP_ID_ONE(inout)
-IREP_ID_ONE(bit_select)
+IREP_ID_ONE(verilog_bit_select)
 IREP_ID_ONE(generate_block)
 IREP_ID_ONE(generate_skip)
 IREP_ID_ONE(generate_if)

diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -129,25 +129,6 @@ inline static void new_symbol(YYSTYPE &dest, YYSTYPE &src)
 
 /*******************************************************************\
 
-Function: extractbit
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-static void extractbit(YYSTYPE &expr, YYSTYPE &identifier, YYSTYPE &part)
-{
-  init(expr, ID_extractbit);
-  mto(expr, identifier);
-  stack_expr(expr).add_to_operands(std::move(to_unary_expr(stack_expr(part)).op()));
-}
-
-/*******************************************************************\
-
 Function: add_as_subtype
 
   Inputs:
@@ -1099,13 +1080,13 @@ port_expression_opt:
 
 port_reference:
 	  port_identifier
-	| port_identifier bit_select  { make_nil($$); /* Not supported */ }
+	| port_identifier constant_bit_select  { make_nil($$); /* Not supported */ }
 	| port_identifier part_select { make_nil($$); /* Not supported */ }
 	;
 
-bit_select:
+constant_bit_select:
 	  '[' expression ']'
-		{ init($$, ID_bit_select); mto($$, $2); }
+		{ $$ = $2; }
 	;
 
 part_select:
@@ -3105,8 +3086,10 @@ hierarchical_identifier_select:
 
 hierarchical_identifier_bit_select_brace:
 	  hierarchical_variable_identifier
-	| hierarchical_identifier_bit_select_brace bit_select
-		{ extractbit($$, $1, $2); }
+	| hierarchical_identifier_bit_select_brace constant_bit_select
+		{ init($$, ID_verilog_bit_select);
+		  mto($$, $1);
+		  mto($$, $2); }
 	;
 
 time_literal: TOK_TIME_LITERAL

diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -1939,7 +1939,7 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
 
 /*******************************************************************\
 
-Function: verilog_typecheck_exprt::convert_extractbit_expr
+Function: verilog_typecheck_exprt::convert_bit_select_expr
 
   Inputs:
 
@@ -1949,8 +1949,11 @@ Function: verilog_typecheck_exprt::convert_extractbit_expr
 
 \*******************************************************************/
 
-exprt verilog_typecheck_exprt::convert_extractbit_expr(extractbit_exprt expr)
+exprt verilog_typecheck_exprt::convert_bit_select_expr(binary_exprt expr)
 {
+  // Verilog's bit select expression may map onto an extractbit
+  // or an array index expression, depending on the type of the first
+  // operand.
   exprt &op0 = expr.op0();
   convert_expr(op0);
 
@@ -1962,7 +1965,7 @@ exprt verilog_typecheck_exprt::convert_extractbit_expr(extractbit_exprt expr)
 
   if(op0.type().id()==ID_array)
   {
-    exprt &op1 = to_extractbit_expr(expr).index();
+    exprt &op1 = expr.op1();
     convert_expr(op1);
     if(op1.type().id() == ID_verilog_real)
     {
@@ -2001,7 +2004,7 @@ exprt verilog_typecheck_exprt::convert_extractbit_expr(extractbit_exprt expr)
         return false_exprt().with_source_location<exprt>(expr);
 
       op1 -= offset;
-      to_extractbit_expr(expr).op1() = from_integer(op1, natural_typet());
+      expr.op1() = from_integer(op1, natural_typet());
     }
     else
     {
@@ -2014,6 +2017,7 @@ exprt verilog_typecheck_exprt::convert_extractbit_expr(extractbit_exprt expr)
     }
 
     expr.type()=bool_typet();
+    expr.id(ID_extractbit);
   }
 
   return std::move(expr);
@@ -2116,8 +2120,8 @@ Function: verilog_typecheck_exprt::convert_binary_expr
 
 exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 {
-  if(expr.id()==ID_extractbit)
-    return convert_extractbit_expr(to_extractbit_expr(expr));
+  if(expr.id() == ID_verilog_bit_select)
+    return convert_bit_select_expr(to_binary_expr(expr));
   else if(expr.id()==ID_replication)
     return convert_replication_expr(to_replication_expr(expr));
   else if(

diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h
@@ -128,7 +128,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   [[nodiscard]] exprt
   convert_system_function(const irep_idt &identifier, function_call_exprt);
   [[nodiscard]] exprt convert_constraint_select_one(exprt);
-  [[nodiscard]] exprt convert_extractbit_expr(extractbit_exprt);
+  [[nodiscard]] exprt convert_bit_select_expr(binary_exprt);
   [[nodiscard]] exprt convert_replication_expr(replication_exprt);
   [[nodiscard]] exprt convert_shl_expr(shl_exprt);
   void implicit_typecast(exprt &, const typet &type);