From e354f4e24b49420fcbaa1426af3d6c763862d5a5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 30 Sep 2022 11:54:25 +0000
Subject: [PATCH] Fix goto-symex' auto-objects feature

The included test also demonstrates how to use it.
---
 regression/cbmc/auto_objects1/main.c    | 13 +++++++++++++
 regression/cbmc/auto_objects1/test.desc |  8 ++++++++
 src/goto-symex/auto_objects.cpp         |  9 ++++++---
 src/goto-symex/symex_dereference.cpp    |  7 +++----
 4 files changed, 30 insertions(+), 7 deletions(-)
 create mode 100644 regression/cbmc/auto_objects1/main.c
 create mode 100644 regression/cbmc/auto_objects1/test.desc

diff --git a/regression/cbmc/auto_objects1/main.c b/regression/cbmc/auto_objects1/main.c
new file mode 100644
index 00000000000..a35bc5087e3
--- /dev/null
+++ b/regression/cbmc/auto_objects1/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  int *auto_object_source1;
+#pragma CPROVER check push
+#pragma CPROVER check disable "pointer"
+  if(auto_object_source1 != 0)
+    int dummy = *auto_object_source1; // triggers creating an auto object
+#pragma CPROVER check pop
+  if(auto_object_source1 != 0 && *auto_object_source1 == 42) // uses auto object
+  {
+    __CPROVER_assert(*auto_object_source1 == 42, "42");
+  }
+}
diff --git a/regression/cbmc/auto_objects1/test.desc b/regression/cbmc/auto_objects1/test.desc
new file mode 100644
index 00000000000..8c69678ac8f
--- /dev/null
+++ b/regression/cbmc/auto_objects1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
index ed5683dbd68..b2dfa4574a9 100644
--- a/src/goto-symex/auto_objects.cpp
+++ b/src/goto-symex/auto_objects.cpp
@@ -83,11 +83,14 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
       {
         const symbolt &symbol = ns.lookup(obj_identifier);
 
-        if(symbol.base_name.starts_with("symex::auto_object"))
+        if(
+          symbol.base_name.starts_with("symex::auto_object") ||
+          symbol.base_name.starts_with("auto_object"))
         {
           // done already?
-          if(!state.get_level2().current_names.has_key(
-               ssa_expr.get_identifier()))
+          auto l2_index =
+            state.get_level2().current_names.find(ssa_expr.get_identifier());
+          if(!l2_index.has_value() || l2_index->get().second == 1)
           {
             initialize_auto_object(e, state);
           }
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index f4beccfb669..c02d57b7983 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -320,6 +320,9 @@ void goto_symext::dereference_rec(
 
     tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), false);
 
+    // this may yield a new auto-object
+    trigger_auto_object(tmp1, state);
+
     // we need to set up some elaborate call-backs
     symex_dereference_statet symex_dereference_state(state, ns);
 
@@ -336,10 +339,6 @@ void goto_symext::dereference_rec(
       dereference.dereference(tmp1, symex_config.show_points_to_sets);
     // std::cout << "**** " << format(tmp2) << '\n';
 
-
-    // this may yield a new auto-object
-    trigger_auto_object(tmp2, state);
-
     // Check various conditions for when we should try to cache the expression.
     // 1. Caching dereferences must be enabled.
     // 2. Do not cache inside LHS of writes.