ensure function globals are not zero sized

ir/memory.cpp

@@ -2010,7 +2010,7 @@ void Memory::mkLocalDisjAddrAxioms(const expr &allocated, const expr &short_bid,
 pair<expr, expr>
 Memory::alloc(const expr *size, uint64_t align, BlockKind blockKind,
               const expr &precond, const expr &nonnull,
-              optional<unsigned> bidopt, unsigned *bid_out) {
+              optional<unsigned> bidopt, unsigned *bid_out, bool is_function) {
   assert(!memory_unused());
 
   // Produce a local block if blockKind is heap or stack.
@@ -2068,6 +2068,8 @@ Memory::alloc(const expr *size, uint64_t align, BlockKind blockKind,
     // support for 0-sized arrays like [0 x i8], which are arbitrarily sized
     if (size)
       state->addAxiom(p.blockSize() == size_zext);
+    if (is_function)
+      state->addAxiom(p.blockSize() != 0);
     state->addAxiom(p.isBlockAligned(align, true));
     state->addAxiom(p.getAllocType() == alloc_ty);
 

ir/memory.h

@@ -303,7 +303,8 @@ class Memory {
   std::pair<smt::expr, smt::expr> alloc(const smt::expr *size, uint64_t align,
       BlockKind blockKind, const smt::expr &precond = true,
       const smt::expr &nonnull = false,
-      std::optional<unsigned> bid = std::nullopt, unsigned *bid_out = nullptr);
+      std::optional<unsigned> bid = std::nullopt, unsigned *bid_out = nullptr,
+      bool is_function = false);
 
   // Start lifetime of a local block.
   void startLifetime(const smt::expr &ptr_local);

ir/value.cpp

@@ -89,11 +89,15 @@ void GlobalVariable::print(ostream &os) const {
     os << '?';
   else
     os << allocsize;
-  os << " bytes, align " << align;
+  os << " bytes";
+  if (is_function)
+    os << ", exec";
+  os << ", align " << align;
 }
 
 static expr get_global(State &s, const string &name, const expr *size,
-                       unsigned align, bool isconst, unsigned &bid) {
+                       unsigned align, bool isconst, bool is_function,
+                       unsigned &bid) {
   expr ptr;
   bool allocated;
   auto blkkind = isconst ? Memory::CONSTGLOBAL : Memory::GLOBAL;
@@ -102,14 +106,15 @@ static expr get_global(State &s, const string &name, const expr *size,
     if (!allocated) {
       // Use the same block id that is used by src
       assert(!s.isSource());
-      ptr = s.getMemory().alloc(size, align, blkkind, true, true, bid).first;
+      ptr = s.getMemory().alloc(size, align, blkkind, true, true, bid, nullptr,
+                                is_function).first;
       s.markGlobalAsAllocated(name);
     } else {
       ptr = Pointer(s.getMemory(), bid, false).release();
     }
   } else {
     ptr = s.getMemory().alloc(size, align, blkkind, true, true, nullopt,
-                              &bid).first;
+                              &bid, is_function).first;
     s.addGlobalVarBid(name, bid);
   }
   return ptr;
@@ -119,7 +124,7 @@ StateValue GlobalVariable::toSMT(State &s) const {
   unsigned bid;
   expr size = expr::mkUInt(allocsize, bits_size_t);
   return { get_global(s, getName(), arbitrary_size ? nullptr : &size, align,
-                      isconst, bid),
+                      isconst, is_function, bid),
            true };
 }
 
@@ -223,7 +228,7 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
     unsigned bid;
     expr size = expr::mkUInt(attrs.blockSize, bits_size_t);
     val = Pointer(s.getMemory(),
-                  get_global(s, smt_name, &size, attrs.align, false, bid))
+                  get_global(s, smt_name, &size, attrs.align, false, false,bid))
           .setAttrs(attrs)
           .setIsBasedOnArg()
           .release();

ir/value.h

@@ -86,11 +86,13 @@ class GlobalVariable final : public Value {
   unsigned align;
   bool isconst;
   bool arbitrary_size;
+  bool is_function;
 public:
   GlobalVariable(Type &type, std::string &&name, uint64_t allocsize,
-                 unsigned align, bool isconst, bool arbitrary_size) :
+                 unsigned align, bool isconst, bool arbitrary_size,
+                 bool is_function = false) :
     Value(type, std::move(name)), allocsize(allocsize), align(align),
-    isconst(isconst), arbitrary_size(arbitrary_size) {}
+    isconst(isconst), arbitrary_size(arbitrary_size), is_function(is_function) {}
   uint64_t size() const { return allocsize; }
   bool isArbitrarySize() const { return arbitrary_size; }
   unsigned getAlignment() const { return align; }

llvm_util/utils.cpp

@@ -384,7 +384,7 @@ Value* get_operand(llvm::Value *v,
   if (auto fn = dyn_cast<llvm::Function>(v)) {
     auto val = make_unique<GlobalVariable>(
       *ty, '@' + fn->getName().str(), 0,
-      fn->getAlign().value_or(llvm::Align(8)).value(), true, true);
+      fn->getAlign().value_or(llvm::Align(8)).value(), true, true, true);
     auto gvar = val.get();
     current_fn->addConstant(std::move(val));