From 7c2e2886b8c76758e078b26737cd28932cb356bf Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Wed, 29 Nov 2023 08:45:06 +0000
Subject: [PATCH] fix #961: input ptrs cannot be stack allocated Add a
 precondition for that. This test is hard to reproduce because it relies on an
 optimization not being done just in target, while done in source.

---
 ir/memory.cpp  | 1 +
 ir/pointer.cpp | 4 ++--
 ir/pointer.h   | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/ir/memory.cpp b/ir/memory.cpp
index 5460d9c2a..1e87fc0ee 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -1313,6 +1313,7 @@ expr Memory::mkInput(const char *name, const ParamAttrs &attrs0) {
   auto bid = p.getShortBid();
 
   state->addAxiom(bid.ule(max_bid));
+  state->addAxiom(!Pointer(*this, max_bid, false).isStackAllocated(false));
 
   AliasSet alias(*this);
   alias.setMayAliasUpTo(false, max_bid);
diff --git a/ir/pointer.cpp b/ir/pointer.cpp
index f4150e0fb..f14565279 100644
--- a/ir/pointer.cpp
+++ b/ir/pointer.cpp
@@ -502,11 +502,11 @@ expr Pointer::getAllocType() const {
                    expr::mkUInt(0, 2));
 }
 
-expr Pointer::isStackAllocated() const {
+expr Pointer::isStackAllocated(bool simplify) const {
   // 1) if a stack object is returned by a callee it's UB
   // 2) if a stack object is given as argument by the caller, we can upgrade it
   //    to a global object, so we can do POR here.
-  if (!has_alloca || isLocal().isFalse())
+  if (simplify && (!has_alloca || isLocal().isFalse()))
     return false;
   return getAllocType() == STACK;
 }
diff --git a/ir/pointer.h b/ir/pointer.h
index d675de3e4..2c82eb74e 100644
--- a/ir/pointer.h
+++ b/ir/pointer.h
@@ -116,7 +116,7 @@ class Pointer {
     CXX_NEW,
   };
   smt::expr getAllocType() const;
-  smt::expr isStackAllocated() const;
+  smt::expr isStackAllocated(bool simplify = true) const;
   smt::expr isHeapAllocated() const;
   smt::expr isNocapture(bool simplify = true) const;
   smt::expr isNoRead() const;