Merge pull request diffblue#4148 from diffblue/gcc_switch_case_range

introduce code_gcc_switch_case_ranget

Author: tautschnig

src/ansi-c/c_typecheck_base.h

@@ -136,7 +136,7 @@ class c_typecheck_baset:
   virtual void typecheck_label(code_labelt &code);
   virtual void typecheck_switch_case(code_switch_caset &code);
   virtual void typecheck_gcc_computed_goto(codet &code);
-  virtual void typecheck_gcc_switch_case_range(codet &code);
+  virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &);
   virtual void typecheck_gcc_local_label(codet &code);
   virtual void typecheck_return(codet &code);
   virtual void typecheck_switch(code_switcht &code);

src/ansi-c/c_typecheck_code.cpp

@@ -42,7 +42,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
   else if(statement==ID_switch_case)
     typecheck_switch_case(to_code_switch_case(code));
   else if(statement==ID_gcc_switch_case_range)
-    typecheck_gcc_switch_case_range(code);
+    typecheck_gcc_switch_case_range(to_code_gcc_switch_case_range(code));
   else if(statement==ID_block)
     typecheck_block(to_code_block(code));
   else if(statement==ID_decl_block)
@@ -515,31 +515,23 @@ void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code)
   }
 }
 
-void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
+void c_typecheck_baset::typecheck_gcc_switch_case_range(
+  code_gcc_switch_case_ranget &code)
 {
-  if(code.operands().size()!=3)
-  {
-    error().source_location = code.source_location();
-    error() << "gcc_switch_case_range expected to have three operands"
-            << eom;
-    throw 0;
-  }
-
-  typecheck_code(to_code(code.op2()));
-
   if(!case_is_allowed)
   {
     error().source_location = code.source_location();
     error() << "did not expect `case' here" << eom;
     throw 0;
   }
 
-  typecheck_expr(code.op0());
-  typecheck_expr(code.op1());
-  implicit_typecast(code.op0(), switch_op_type);
-  implicit_typecast(code.op1(), switch_op_type);
-  make_constant(code.op0());
-  make_constant(code.op1());
+  typecheck_expr(code.lower());
+  typecheck_expr(code.upper());
+  implicit_typecast(code.lower(), switch_op_type);
+  implicit_typecast(code.upper(), switch_op_type);
+  make_constant(code.lower());
+  make_constant(code.upper());
+  typecheck_code(code.code());
 }
 
 void c_typecheck_baset::typecheck_gcc_local_label(codet &)

src/cpp/parse.cpp

@@ -7414,20 +7414,18 @@ bool Parser::rStatement(codet &statement)
         if(!rExpression(range_end, false))
           return false;
 
-        statement=codet(ID_gcc_switch_case_range);
-        statement.operands().resize(3);
-        statement.op0()=case_expr;
-        statement.op1()=range_end;
-        set_location(statement, tk1);
-
         if(lex.get_token(tk2)!=':')
           return false;
 
         codet statement2;
         if(!rStatement(statement2))
           return false;
 
-        statement.op2().swap(statement2);
+        code_gcc_switch_case_ranget code(
+          std::move(case_expr), std::move(range_end), std::move(statement2));
+        set_location(code, tk1);
+
+        statement = std::move(code);
       }
       else
       {

src/goto-programs/goto_convert.cpp

@@ -384,17 +384,12 @@ void goto_convertt::convert_switch_case(
 }
 
 void goto_convertt::convert_gcc_switch_case_range(
-  const codet &code,
+  const code_gcc_switch_case_ranget &code,
   goto_programt &dest,
   const irep_idt &mode)
 {
-  INVARIANT_WITH_DIAGNOSTICS(
-    code.operands().size() == 3,
-    "GCC's switch-case-range statement expected to have three operands",
-    code.find_source_location());
-
-  const auto lb = numeric_cast<mp_integer>(code.op0());
-  const auto ub = numeric_cast<mp_integer>(code.op1());
+  const auto lb = numeric_cast<mp_integer>(code.lower());
+  const auto ub = numeric_cast<mp_integer>(code.upper());
 
   INVARIANT_WITH_DIAGNOSTICS(
     lb.has_value() && ub.has_value(),
@@ -409,7 +404,7 @@ void goto_convertt::convert_gcc_switch_case_range(
   }
 
   goto_programt tmp;
-  convert(to_code(code.op2()), tmp, mode);
+  convert(code.code(), tmp, mode);
 
   goto_programt::targett target = tmp.instructions.begin();
   dest.destructive_append(tmp);
@@ -425,7 +420,7 @@ void goto_convertt::convert_gcc_switch_case_range(
   exprt::operandst &case_op_dest = cases_entry->second->second;
 
   for(mp_integer i = *lb; i <= *ub; ++i)
-    case_op_dest.push_back(from_integer(i, code.op0().type()));
+    case_op_dest.push_back(from_integer(i, code.lower().type()));
 }
 
 /// converts 'code' and appends the result to 'dest'
@@ -459,7 +454,8 @@ void goto_convertt::convert(
   else if(statement==ID_switch_case)
     convert_switch_case(to_code_switch_case(code), dest, mode);
   else if(statement==ID_gcc_switch_case_range)
-    convert_gcc_switch_case_range(code, dest, mode);
+    convert_gcc_switch_case_range(
+      to_code_gcc_switch_case_range(code), dest, mode);
   else if(statement==ID_for)
     convert_for(to_code_for(code), dest, mode);
   else if(statement==ID_while)

src/goto-programs/goto_convert_class.h

@@ -283,7 +283,7 @@ class goto_convertt:public messaget
     goto_programt &dest,
     const irep_idt &mode);
   void convert_gcc_switch_case_range(
-    const codet &code,
+    const code_gcc_switch_case_ranget &,
     goto_programt &dest,
     const irep_idt &mode);
   void convert_function_call(

src/util/std_code.h

@@ -1474,6 +1474,92 @@ inline code_switch_caset &to_code_switch_case(codet &code)
   return static_cast<code_switch_caset &>(code);
 }
 
+/// \ref codet representation of a switch-case, i.e.\ a `case` statement
+/// within a `switch`. This is the variant that takes a range,
+/// which is a gcc extension.
+class code_gcc_switch_case_ranget : public codet
+{
+public:
+  code_gcc_switch_case_ranget(exprt _lower, exprt _upper, codet _code)
+    : codet(
+        ID_gcc_switch_case_range,
+        {std::move(_lower), std::move(_upper), std::move(_code)})
+  {
+  }
+
+  /// lower bound of range
+  const exprt &lower() const
+  {
+    return op0();
+  }
+
+  /// lower bound of range
+  exprt &lower()
+  {
+    return op0();
+  }
+
+  /// upper bound of range
+  const exprt &upper() const
+  {
+    return op1();
+  }
+
+  /// upper bound of range
+  exprt &upper()
+  {
+    return op1();
+  }
+
+  /// the statement to be executed when the case applies
+  codet &code()
+  {
+    return static_cast<codet &>(op2());
+  }
+
+  /// the statement to be executed when the case applies
+  const codet &code() const
+  {
+    return static_cast<const codet &>(op2());
+  }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
+};
+
+template <>
+inline bool can_cast_expr<code_gcc_switch_case_ranget>(const exprt &base)
+{
+  return detail::can_cast_code_impl(base, ID_gcc_switch_case_range);
+}
+
+inline void validate_expr(const code_gcc_switch_case_ranget &x)
+{
+  validate_operands(x, 3, "gcc-switch-case-range must have three operands");
+}
+
+inline const code_gcc_switch_case_ranget &
+to_code_gcc_switch_case_range(const codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
+  DATA_INVARIANT(
+    code.operands().size() == 3,
+    "gcc-switch-case-range must have three operands");
+  return static_cast<const code_gcc_switch_case_ranget &>(code);
+}
+
+inline code_gcc_switch_case_ranget &to_code_gcc_switch_case_range(codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
+  DATA_INVARIANT(
+    code.operands().size() == 3,
+    "gcc-switch-case-range must have three operands");
+  return static_cast<code_gcc_switch_case_ranget &>(code);
+}
+
 /// \ref codet representation of a `break` statement (within a `for` or `while`
 /// loop).
 class code_breakt:public codet