From 52d7e3c8d58945a295a1f4231bd78ebede0b98f9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 8 Dec 2021 20:27:31 +0000
Subject: [PATCH] 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.
---
 regression/cbmc/switch9/main.c     | 20 ++++++++++++++++++++
 regression/cbmc/switch9/test.desc  | 14 ++++++++++++++
 src/goto-programs/goto_convert.cpp | 21 +++++++++++++++++++++
 3 files changed, 55 insertions(+)
 create mode 100644 regression/cbmc/switch9/main.c
 create mode 100644 regression/cbmc/switch9/test.desc

diff --git a/regression/cbmc/switch9/main.c b/regression/cbmc/switch9/main.c
new file mode 100644
index 00000000000..704ea990272
--- /dev/null
+++ b/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;
+  }
+}
diff --git a/regression/cbmc/switch9/test.desc b/regression/cbmc/switch9/test.desc
new file mode 100644
index 00000000000..8438cf07aac
--- /dev/null
+++ b/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.
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index d5ccf182cd9..cfc331a76d0 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/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). "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);