Add function inlining pass to improve DSA precision

CMakeLists.txt

@@ -110,6 +110,7 @@ add_library(smackTranslator STATIC
   include/smack/SmackOptions.h
   include/smack/CodifyStaticInits.h
   include/smack/RemoveDeadDefs.h
+  include/smack/SmackFunctionInliner.h
   include/smack/ExtractContracts.h
   include/smack/VerifierCodeMetadata.h
   include/smack/SimplifyLibCalls.h
@@ -137,6 +138,7 @@ add_library(smackTranslator STATIC
   lib/smack/SmackOptions.cpp
   lib/smack/CodifyStaticInits.cpp
   lib/smack/RemoveDeadDefs.cpp
+  lib/smack/SmackFunctionInliner.cpp
   lib/smack/ExtractContracts.cpp
   lib/smack/VerifierCodeMetadata.cpp
   lib/smack/SimplifyLibCalls.cpp

docs/function-inlining.md

@@ -0,0 +1,99 @@
+# SmackFunctionInliner Pass
+
+## Motivation
+
+SMACK uses context-insensitive DSA analysis from sea-dsa. When a function
+takes or returns pointers, the context-insensitive analysis merges the
+points-to nodes at call sites, losing precision. For example, if `alloc()`
+returns a freshly allocated pointer, every caller's returned pointer gets
+merged into a single node — even though each call site is independent.
+
+Inlining these functions before DSA runs eliminates the inter-procedural
+pointer flow, allowing DSA to treat each (formerly separate) call site's
+allocations and pointer operations locally. This improves precision without
+requiring a context-sensitive analysis.
+
+## Design
+
+`SmackFunctionInliner` is an LLVM `ModulePass` that runs in the `llvm2bpl`
+pipeline **before** sea-dsa analysis. It uses LLVM's `InlineFunction` utility
+to inline small functions, with a higher threshold for functions that involve
+pointers.
+
+### Inlining criteria
+
+A function is eligible for inlining if **all** of the following hold:
+
+- It has a definition (not a declaration or intrinsic)
+- It is not variadic
+- Its name does not contain `__SMACK_` or `__VERIFIER_`
+- It is not an entry point (as specified by `--entry-points`)
+- It is not recursive (see below)
+- Its instruction count is within the threshold:
+  - **Pointer-involving** (returns or takes a pointer): <= `--ptr-inline-limit` (default 200)
+  - **Non-pointer**: <= `--inline-limit` (default 50)
+
+The `noinline` attribute (which clang adds to all functions at `-O0`) is
+stripped before inlining, since this pass inlines for analysis precision,
+not as a compiler optimization.
+
+### Recursion detection
+
+The pass builds an LLVM `CallGraph` and uses `scc_iterator` to identify
+strongly connected components (SCCs):
+
+- **Non-trivial SCC** (size > 1): all functions in the SCC are mutually
+  recursive and excluded from inlining.
+- **Trivial SCC** (size 1): the function is checked for a self-call edge.
+  If present, it is directly recursive and excluded.
+
+This prevents infinite inlining of recursive call chains.
+
+### Bottom-up processing
+
+`scc_iterator` yields SCCs in reverse topological order — callees before
+callers. The pass processes functions in this order so that when a caller
+is inlined, its callees have already been inlined into it. For a chain
+`main → foo → bar`, the pass first inlines `bar` into `foo`, then inlines
+`foo` (now containing `bar`'s body) into `main`.
+
+### Iterative fixpoint
+
+The pass repeats until no more inlining occurs. This handles cases where
+inlining changes the call graph (e.g., a function that was above the
+threshold shrinks after dead code is removed, or inlining removes the last
+caller of a function which is then deleted, changing reachability).
+
+After each iteration, functions with no remaining callers are removed
+(excluding entry points and `__SMACK_`/`__VERIFIER_` functions).
+
+## Command-line options
+
+| Option | Type | Default | Description |
+|--------|------|---------|-------------|
+| `--inline-funcs` | bool | true | Enable/disable the pass |
+| `--inline-limit` | unsigned | 50 | Instruction count threshold for non-pointer functions (0 disables) |
+| `--ptr-inline-limit` | unsigned | 200 | Instruction count threshold for pointer-involving functions |
+
+## Pipeline placement
+
+The pass is inserted in `llvm2bpl.cpp` after dead code elimination and
+`RemoveDeadDefs`, but before `seadsa::createRemovePtrToIntPass()` and all
+subsequent DSA-dependent passes:
+
+```
+... createDeadCodeEliminationPass()
+... RemoveDeadDefs()
+>>> SmackFunctionInliner()       ← here
+... createRemovePtrToIntPass()
+... createLowerSwitchPass()
+... createPromoteMemoryToRegisterPass()
+...
+```
+
+## Files
+
+- `include/smack/SmackFunctionInliner.h` — Pass declaration
+- `lib/smack/SmackFunctionInliner.cpp` — Pass implementation
+- `tools/llvm2bpl/llvm2bpl.cpp` — Pipeline integration
+- `CMakeLists.txt` — Build integration

include/smack/SmackFunctionInliner.h

@@ -0,0 +1,32 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+
+#ifndef SMACKFUNCTIONINLINER_H
+#define SMACKFUNCTIONINLINER_H
+
+#include "llvm/IR/Module.h"
+#include "llvm/Pass.h"
+
+#include <set>
+
+namespace smack {
+
+class SmackFunctionInliner : public llvm::ModulePass {
+public:
+  static char ID;
+  SmackFunctionInliner() : llvm::ModulePass(ID) {}
+  virtual bool runOnModule(llvm::Module &M) override;
+
+private:
+  bool shouldInline(llvm::Function &F);
+  bool involvesPointers(llvm::Function &F);
+  unsigned getInstructionCount(llvm::Function &F);
+  void computeRecursiveFunctions(llvm::Module &M);
+
+  std::set<llvm::Function *> recursiveFunctions;
+};
+
+} // namespace smack
+
+#endif // SMACKFUNCTIONINLINER_H

lib/smack/SmackFunctionInliner.cpp

@@ -0,0 +1,212 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+
+#define DEBUG_TYPE "smack-inline"
+
+#include "smack/SmackFunctionInliner.h"
+#include "smack/Debug.h"
+#include "smack/Naming.h"
+#include "smack/SmackOptions.h"
+#include "llvm/ADT/SCCIterator.h"
+#include "llvm/Analysis/CallGraph.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
+#include "llvm/Transforms/Utils/Cloning.h"
+
+#include <vector>
+
+static llvm::cl::opt<bool>
+    InlineFuncs("inline-funcs",
+                llvm::cl::desc("Inline small functions before DSA analysis"),
+                llvm::cl::init(false));
+
+static llvm::cl::opt<unsigned>
+    InlineLimit("inline-limit",
+                llvm::cl::desc("Instruction count threshold for inlining "
+                               "non-pointer functions (0 to disable)"),
+                llvm::cl::init(50));
+
+static llvm::cl::opt<unsigned>
+    PtrInlineLimit("ptr-inline-limit",
+                   llvm::cl::desc("Instruction count threshold for inlining "
+                                  "pointer-involving functions"),
+                   llvm::cl::init(200));
+
+static llvm::cl::list<std::string>
+    NoInlineFuncs("no-inline",
+                  llvm::cl::desc("Functions that should not be inlined"),
+                  llvm::cl::ZeroOrMore);
+
+namespace smack {
+
+using namespace llvm;
+
+bool SmackFunctionInliner::involvesPointers(Function &F) {
+  if (F.getReturnType()->isPointerTy())
+    return true;
+  for (auto &Arg : F.args())
+    if (Arg.getType()->isPointerTy())
+      return true;
+  return false;
+}
+
+unsigned SmackFunctionInliner::getInstructionCount(Function &F) {
+  unsigned count = 0;
+  for (auto &BB : F)
+    count += BB.size();
+  return count;
+}
+
+bool SmackFunctionInliner::shouldInline(Function &F) {
+  if (F.isDeclaration() || F.isIntrinsic())
+    return false;
+
+  if (F.isVarArg())
+    return false;
+
+  auto name = F.getName();
+  if (name.find("__SMACK_") != StringRef::npos)
+    return false;
+  if (name.find("__VERIFIER_") != StringRef::npos)
+    return false;
+  for (const auto &NI : NoInlineFuncs)
+    if (name == NI)
+      return false;
+  if (SmackOptions::isEntryPoint(name))
+    return false;
+
+  if (recursiveFunctions.count(&F))
+    return false;
+
+  unsigned instCount = getInstructionCount(F);
+  if (involvesPointers(F))
+    return instCount <= PtrInlineLimit;
+  return InlineLimit > 0 && instCount <= InlineLimit;
+}
+
+void SmackFunctionInliner::computeRecursiveFunctions(Module &M) {
+  recursiveFunctions.clear();
+  CallGraph CG(M);
+
+  for (auto I = scc_begin(&CG); !I.isAtEnd(); ++I) {
+    const auto &SCC = *I;
+    if (SCC.size() > 1) {
+      // Non-trivial SCC: all functions are mutually recursive
+      for (auto *CGN : SCC)
+        if (Function *F = CGN->getFunction())
+          recursiveFunctions.insert(F);
+    } else {
+      // Single-node SCC: check for direct self-recursion
+      CallGraphNode *CGN = SCC[0];
+      Function *F = CGN->getFunction();
+      if (F) {
+        for (auto &CR : *CGN) {
+          if (CR.second->getFunction() == F) {
+            recursiveFunctions.insert(F);
+            break;
+          }
+        }
+      }
+    }
+  }
+}
+
+bool SmackFunctionInliner::runOnModule(Module &M) {
+  if (!InlineFuncs)
+    return false;
+
+  bool changed = false;
+  bool inlinedAny;
+
+  do {
+    inlinedAny = false;
+
+    // Recompute recursive functions each iteration since inlining
+    // may break cycles.
+    computeRecursiveFunctions(M);
+
+    // Build bottom-up order using the call graph SCCs.
+    // scc_iterator yields SCCs in reverse topological order (callees before
+    // callers), which is exactly the bottom-up order we want.
+    CallGraph CG(M);
+    std::vector<Function *> bottomUp;
+    for (auto I = scc_begin(&CG); !I.isAtEnd(); ++I) {
+      for (auto *CGN : *I)
+        if (Function *F = CGN->getFunction())
+          bottomUp.push_back(F);
+    }
+
+    // Process each function in bottom-up order: inline callees into it.
+    for (Function *F : bottomUp) {
+      if (F->isDeclaration())
+        continue;
+
+      // Collect inlineable call sites within this function.
+      std::vector<CallBase *> callSites;
+      for (auto &BB : *F) {
+        for (auto &I : BB) {
+          auto *CB = dyn_cast<CallBase>(&I);
+          if (!CB)
+            continue;
+
+          Function *Callee = CB->getCalledFunction();
+          if (!Callee)
+            continue;
+
+          if (!shouldInline(*Callee))
+            continue;
+
+          callSites.push_back(CB);
+        }
+      }
+
+      // Inline collected call sites.
+      for (auto *CB : callSites) {
+        Function *Callee = CB->getCalledFunction();
+        if (!Callee)
+          continue;
+
+        // Strip noinline attribute (added by -O0) since we inline for
+        // analysis precision, not as a compiler optimization.
+        Callee->removeFnAttr(Attribute::NoInline);
+
+        InlineFunctionInfo IFI;
+        InlineResult IR = InlineFunction(*CB, IFI);
+        if (IR.isSuccess()) {
+          SDEBUG(errs() << "inlined: " << Callee->getName() << "\n");
+          inlinedAny = true;
+          changed = true;
+        }
+      }
+    }
+
+    // Remove dead functions after inlining.
+    if (inlinedAny) {
+      std::vector<Function *> dead;
+      for (Function &F : M) {
+        if (F.isDeclaration())
+          continue;
+        if (F.use_empty() && !SmackOptions::isEntryPoint(F.getName()) &&
+            F.getName().find("__SMACK_") == StringRef::npos &&
+            F.getName().find("__VERIFIER_") == StringRef::npos) {
+          dead.push_back(&F);
+        }
+      }
+      for (auto *F : dead) {
+        SDEBUG(errs() << "removing fully inlined: " << F->getName() << "\n");
+        F->eraseFromParent();
+      }
+    }
+  } while (inlinedAny);
+
+  return changed;
+}
+
+char SmackFunctionInliner::ID = 0;
+
+static RegisterPass<SmackFunctionInliner>
+    X("smack-inline", "Inline small functions before DSA analysis");
+
+} // namespace smack

share/smack/frontend.py

@@ -109,6 +109,8 @@ def default_clang_compile_command(args, lib=False):
     if VProperty.INTEGER_OVERFLOW in args.check:
         cmd += (['-fsanitize=signed-integer-overflow,shift']
                 if not lib else ['-DSIGNED_INTEGER_OVERFLOW_CHECK'])
+    if args.integer_encoding != 'bit-vector' and not lib:
+        cmd += ['-fsanitize=unsigned-integer-overflow']
     if VProperty.ASSERTIONS not in args.check:
         cmd += ['-DDISABLE_SMACK_ASSERTIONS']
     if args.float:

share/smack/svcomp/utils.py

@@ -14,6 +14,12 @@ def svcomp_frontend(input_file, args):
   # enable static LLVM unroll pass
   args.static_unroll = True
 
+  # enable function inlining before DSA for precision
+  args.inline_funcs = True
+
+  # prevent inlining reach_error so replace_reach_error can find it
+  args.no_inline = getattr(args, 'no_inline', []) + ['reach_error']
+
   # attempt to rewrite bitwise ops into provided models
   args.rewrite_bitwise_ops = True