From 4827dd4bbbdbaf85e1995d589b6b92d6b1831b38 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 6 Feb 2024 11:44:31 +0000
Subject: [PATCH] Goto crossing scopes: fix scope tree entry of conditions

We must convert the condition of an if/then/else first to make sure any
declarations produced by converting the condition have a suitable
scope-tree node. Previously, gotos in either branch of the if-then-else
were led to believe that declarations resulting from condition were not
yet in scope. The feature from #8091 would, thus, result in a spurious
loop back to the declaration to put it in scope before following the
goto edge.
---
 .../cbmc/declaration-goto/no-duplicate-decl.c    | 16 ++++++++++++++++
 .../cbmc/declaration-goto/no-duplicate-decl.desc | 11 +++++++++++
 regression/validate-trace-xml-schema/check.py    |  1 +
 src/goto-programs/goto_convert.cpp               |  6 +++---
 4 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc/declaration-goto/no-duplicate-decl.c
 create mode 100644 regression/cbmc/declaration-goto/no-duplicate-decl.desc

diff --git a/regression/cbmc/declaration-goto/no-duplicate-decl.c b/regression/cbmc/declaration-goto/no-duplicate-decl.c
new file mode 100644
index 000000000000..d8c3f66ada27
--- /dev/null
+++ b/regression/cbmc/declaration-goto/no-duplicate-decl.c
@@ -0,0 +1,16 @@
+int foo()
+{
+  return 1;
+}
+
+int main()
+{
+  if(foo())
+    goto out;
+
+  return 1;
+
+out:
+  __CPROVER_assert(0, "false");
+  return 0;
+}
diff --git a/regression/cbmc/declaration-goto/no-duplicate-decl.desc b/regression/cbmc/declaration-goto/no-duplicate-decl.desc
new file mode 100644
index 000000000000..ca0f21bf6ca9
--- /dev/null
+++ b/regression/cbmc/declaration-goto/no-duplicate-decl.desc
@@ -0,0 +1,11 @@
+CORE
+no-duplicate-decl.c
+--show-goto-functions
+^[[:space:]]*DECL main::\$tmp::return_value_foo
+^EXIT=0$
+^SIGNAL=0$
+--
+^[[:space:]]*DECL going_to::out
+^[[:space:]]*\d+: DECL main::\$tmp::return_value_foo
+--
+Test that no loop back to the declaration is generated.
diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py
index 1ee1c781abd7..e148b3bbd83f 100644
--- a/regression/validate-trace-xml-schema/check.py
+++ b/regression/validate-trace-xml-schema/check.py
@@ -23,6 +23,7 @@
     ['xml-interface1', 'test_wrong_flag.desc'],
     # these want --show-goto-functions instead of producing a trace
     ['integer-assignments1', 'integer-typecheck.desc'],
+    ['declaration-goto', 'no-duplicate-decl.desc'],
     ['destructors', 'compound_literal.desc'],
     ['destructors', 'enter_lexical_block.desc'],
     ['enum_is_in_range', 'enum_test3-simplified.desc'],
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index f7725df31369..71c3365beb6e 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -1617,6 +1617,9 @@ void goto_convertt::convert_ifthenelse(
     return convert_ifthenelse(new_if0, dest, mode);
   }
 
+  exprt tmp_guard = code.cond();
+  clean_expr(tmp_guard, dest, mode);
+
   // convert 'then'-branch
   goto_programt tmp_then;
   convert(code.then_case(), tmp_then, mode);
@@ -1636,9 +1639,6 @@ void goto_convertt::convert_ifthenelse(
                           : code.else_case().source_location();
   }
 
-  exprt tmp_guard=code.cond();
-  clean_expr(tmp_guard, dest, mode);
-
   generate_ifthenelse(
     tmp_guard,
     source_location,