Merge pull request #5724 from tautschnig/switch-range

GCC switch range: don't enumerate elements

Author: tautschnig

regression/cbmc/gcc_switch_case_range1/main.c

@@ -1,3 +1,5 @@
+#include <limits.h>
+
 int main()
 {
   int x;
@@ -18,9 +20,12 @@ int main()
 #endif
     __CPROVER_assert(0, "... works");
     break;
-  case 13:
+  case 14:
     __CPROVER_assert(0, "13 works");
     break;
+  case 15 ... INT_MAX:
+    __CPROVER_assert(0, "large range works");
+    break;
   default:
     __CPROVER_assert(0, "default works");
     break;

regression/cbmc/gcc_switch_case_range1/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 4 of 4 failed
+^\*\* 5 of 5 failed
 --
 ^warning: ignoring

src/goto-programs/goto_convert.cpp

@@ -416,10 +416,10 @@ void goto_convertt::convert_gcc_switch_case_range(
       targets.cases_map.insert({target, --targets.cases.end()}).first;
   }
 
-  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.lower().type()));
+  // create a skeleton for case_guard
+  cases_entry->second->second.push_back(
+    and_exprt{binary_relation_exprt{code.lower(), ID_le, nil_exprt{}},
+              binary_relation_exprt{nil_exprt{}, ID_le, code.upper()}});
 }
 
 /// converts 'code' and appends the result to 'dest'
@@ -1100,18 +1100,27 @@ exprt goto_convertt::case_guard(
 {
   PRECONDITION(!case_op.empty());
 
-  if(case_op.size() == 1)
-    return equal_exprt(value, case_op.at(0));
-  else
-  {
-    exprt::operandst disjuncts;
-    disjuncts.reserve(case_op.size());
+  exprt::operandst disjuncts;
+  disjuncts.reserve(case_op.size());
 
-    for(const auto &op : case_op)
+  for(const auto &op : case_op)
+  {
+    // could be a skeleton generated by convert_gcc_switch_case_range
+    if(op.id() == ID_and)
+    {
+      const binary_exprt &and_expr = to_binary_expr(op);
+      PRECONDITION(to_binary_expr(and_expr.op0()).op1().is_nil());
+      PRECONDITION(to_binary_expr(and_expr.op1()).op0().is_nil());
+      binary_exprt skeleton = and_expr;
+      to_binary_expr(skeleton.op0()).op1() = value;
+      to_binary_expr(skeleton.op1()).op0() = value;
+      disjuncts.push_back(skeleton);
+    }
+    else
       disjuncts.push_back(equal_exprt(value, op));
-
-    return disjunction(disjuncts);
   }
+
+  return disjunction(disjuncts);
 }
 
 void goto_convertt::convert_switch(