Evaluate any non-trivial switch condition just once

goto-program conversion should not turn switch(E) { case 1:... case 2:
...} into if(E == 1 || E == 2 || ...) for a non-trivial expression E.
Instead, the value of E must be copied into a temporary to avoid
repeated evaluation of E. We would already do this when E had side
effects, but even side-effect-free expression could result in expensive
assertions being generated when those expressions themselves would
trigger them with goto_check.

This change reduces verification time of a proof of
s2n_stuffer_skip_whitespace from several minutes down to seconds.

Author: tautschnig

regression/cbmc/switch9/main.c

@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+
+  if(!p)
+    return 1;
+
+  switch(*p)
+  {
+  case 1:
+  case 2:
+  case 3:
+    return 0;
+  case 4:
+  default:
+    return -1;
+  }
+}

regression/cbmc/switch9/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--pointer-check --malloc-may-fail --malloc-fail-null
+activate-multi-line-match
+^\[main.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*p: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+\[main.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*p: SUCCESS\n.*\[main.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*p: SUCCESS\n
+--
+A pointer check for the switch value should be generated, but there should only
+be one such check.

src/goto-programs/goto_convert.cpp

@@ -1184,6 +1184,27 @@ void goto_convertt::convert_switch(
   goto_programt sideeffects;
   clean_expr(argument, sideeffects, mode);
 
+  // Avoid potential performance penalties caused by evaluating the value
+  // multiple times (as the below chain-of-ifs does) does. "needs_cleaning"
+  // isn't necessarily the right check here, and we may need to introduce a
+  // different way of identifying the class of non-trivial expressions that
+  // warrant introduction of a temporary.
+  if(needs_cleaning(argument))
+  {
+    symbolt &new_symbol = new_tmp_symbol(
+      argument.type(),
+      "switch_value",
+      sideeffects,
+      code.source_location(),
+      mode);
+
+    code_assignt copy_value{
+      new_symbol.symbol_expr(), argument, code.source_location()};
+    convert(copy_value, sideeffects, mode);
+
+    argument = new_symbol.symbol_expr();
+  }
+
   // save break/default/cases targets
   break_switch_targetst old_targets(targets);