From 3f034334ad2ac8a4e3aa515b09ef21668d0dd743 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 1 Feb 2022 12:34:19 +0000
Subject: [PATCH] goto-symex: print status note and conditional warning for
 self-loops

Unless CBMC is invoked with --no-self-loops-to-assumptions, self-loops
are replaced by assumptions. This commit now introduces a status output
that such replacement is happening, and also a warning when
--unwinding-assertions is set: as the loop is replaced by an assumption,
no unwinding assertions can possible be generated. This behaviour may be
unexpected by the user, and we should therefore let them know what is
going on.

Fixes: #6433
---
 .../self_loops_to_assumptions1/default.desc   |  2 ++
 .../self_loops_to_assumptions1/no-assume.desc |  1 +
 src/goto-symex/symex_goto.cpp                 | 27 ++++++++++++-------
 3 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/regression/cbmc/self_loops_to_assumptions1/default.desc b/regression/cbmc/self_loops_to_assumptions1/default.desc
index a7a038cf94d..5cec41df787 100644
--- a/regression/cbmc/self_loops_to_assumptions1/default.desc
+++ b/regression/cbmc/self_loops_to_assumptions1/default.desc
@@ -1,6 +1,8 @@
 CORE
 main.c
 --unwind 1 --unwinding-assertions
+^replacing self-loop at file main.c line 3 function main by assume\(FALSE\)$
+^no unwinding assertion will be generated for self-loop at file main.c line 3 function main$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/self_loops_to_assumptions1/no-assume.desc b/regression/cbmc/self_loops_to_assumptions1/no-assume.desc
index 519dfddbd15..b75ec34a1bc 100644
--- a/regression/cbmc/self_loops_to_assumptions1/no-assume.desc
+++ b/regression/cbmc/self_loops_to_assumptions1/no-assume.desc
@@ -5,3 +5,4 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
+^replacing self-loop
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index cf0e8431648..8d32b3ba1ac 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -9,11 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Symbolic Execution
 
-#include "goto_symex.h"
-#include "goto_symex_is_constant.h"
-
-#include <algorithm>
-
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
@@ -22,11 +17,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
+#include <langapi/language_util.h>
 #include <pointer-analysis/add_failed_symbols.h>
 #include <pointer-analysis/value_set_dereference.h>
 
+#include "goto_symex.h"
+#include "goto_symex_is_constant.h"
 #include "path_storage.h"
 
+#include <algorithm>
+
 void goto_symext::apply_goto_condition(
   goto_symex_statet &current_state,
   goto_statet &jump_taken_state,
@@ -279,10 +279,19 @@ void goto_symext::symex_goto(statet &state)
     {
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
-      if(new_guard.is_true())
-        symex_assume_l2(state, false_exprt());
-      else
-        symex_assume_l2(state, not_exprt(new_guard));
+      exprt negated_guard = not_exprt{new_guard};
+      do_simplify(negated_guard);
+      log.statistics() << "replacing self-loop at "
+                       << state.source.pc->source_location() << " by assume("
+                       << from_expr(ns, state.source.function_id, negated_guard)
+                       << ")" << messaget::eom;
+      if(symex_config.unwinding_assertions)
+      {
+        log.warning()
+          << "no unwinding assertion will be generated for self-loop at "
+          << state.source.pc->source_location() << messaget::eom;
+      }
+      symex_assume_l2(state, negated_guard);
 
       // next instruction
       symex_transition(state);