Resolve derived source expressions by field offset

The n-th LLVM struct element is not the n-th DW_TAG_member, so naming a
field by its ordinal position reported the wrong member whenever the two
orderings diverged: bitfields share a storage unit, clang inserts padding,
and a C++ base class occupies a field without being a member. A store to
'b->after' was recorded as 'b->f2', and 'p->d0' as 'p->d1' -- a wrong name
in a counterexample is worse than no name at all.

Look the member up by the byte offset of the field being indexed instead,
and decline to name a bitfield, a static or artificial member, an ambiguous
match, or a union, where a field index cannot pick a member out.

Fix three more ways a name could describe the wrong object:

  - A pointer value owes a dereference that only the member branch spent,
    so '(*pa)[2]' came out as 'pa[2]', a different address. Spend it in the
    subscript branch too.
  - Subscripting the address of a non-array named 'x[1]' for a scalar x.
    Require the debug type to really be an array.
  - A cast that changes the type no longer describes the same object, so
    neither it nor the stripPointerCastsAndAliases fallback should carry a
    source expression across one.

Consume one DWARF array dimension per subscript, since DWARF folds every
dimension into a single node; multi-dimensional element expressions were
dropped entirely before and now resolve.

Restrict the recorded value to scalars -- vectors reached the recorder
through the vector load and store paths -- and drop the parameter name
shadowing llvm::Value.

Move the test into its own folder pinned to Corral: source expressions are
only rendered into a counterexample by /printDataValues, so @checkout could
never match under Boogie and the c/data job went red. Add regressions for
the bitfield, cast, and array cases; the absence assertions use awk rather
than grep -v, which exits 0 whenever any line differs and so asserts
nothing.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: shaobo-he

include/smack/SmackInstGenerator.h

@@ -12,6 +12,10 @@
 #include <unordered_set>
 #include <vector>
 
+namespace llvm {
+class DIType;
+}
+
 namespace smack {
 
 class Naming;
@@ -57,9 +61,12 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   void rememberSourceExpr(const llvm::Value *v, const SourceExpr &expr);
   const std::vector<SourceExpr> *findSourceExprs(const llvm::Value *v) const;
   std::vector<SourceExpr> sourceLValues(const llvm::Value *pointer) const;
-  void rememberLoadSourceExpr(llvm::LoadInst &i);
+  void rememberLoadSourceExpr(llvm::LoadInst &i,
+                              const std::vector<SourceExpr> &lvalues);
   void rememberGEPSourceExpr(llvm::GetElementPtrInst &i);
   void rememberCastSourceExpr(llvm::CastInst &i);
+  void recordDerivedLValues(const std::vector<SourceExpr> &lvalues,
+                            const llvm::Value *value);
   void recordSourceLValues(const llvm::Value *pointer,
                            const llvm::Value *value);
 

lib/smack/SmackInstGenerator.cpp

@@ -11,11 +11,13 @@
 #include "smack/VectorOperations.h"
 #include "llvm/Analysis/LoopInfo.h"
 #include "llvm/BinaryFormat/Dwarf.h"
+#include "llvm/IR/DataLayout.h"
 #include "llvm/IR/DebugInfo.h"
 #include "llvm/IR/DebugInfoMetadata.h"
 #include "llvm/IR/GetElementPtrTypeIterator.h"
 #include "llvm/IR/InstVisitor.h"
 #include "llvm/Support/GraphWriter.h"
+#include <algorithm>
 #include <sstream>
 
 #include "llvm/Support/raw_ostream.h"
@@ -90,20 +92,71 @@ const DIType *dereferenceDIType(const DIType *T) {
   }
 }
 
-const DIDerivedType *getDIMember(const DIType *T, unsigned index) {
+// The n-th LLVM struct element is not the n-th DW_TAG_member: bitfields share
+// a storage unit, clang inserts padding, and a base class occupies a field
+// without being a member. Matching on the byte offset instead keeps the name
+// tied to the field whose value is actually recorded.
+const DIDerivedType *getDIMemberAtOffset(const DIType *T,
+                                         uint64_t offsetInBits) {
   auto *CT = dyn_cast_or_null<DICompositeType>(stripDIAliases(T));
   if (!CT)
     return nullptr;
 
-  unsigned memberIndex = 0;
+  switch (CT->getTag()) {
+  case dwarf::DW_TAG_structure_type:
+  case dwarf::DW_TAG_class_type:
+    break;
+  default:
+    // Every union member sits at offset zero, so a field index cannot pick one
+    // out; arrays and enumerations have no members to pick at all.
+    return nullptr;
+  }
+
+  const DIDerivedType *found = nullptr;
   for (DINode *N : CT->getElements()) {
     auto *Member = dyn_cast<DIDerivedType>(N);
     if (!Member || Member->getTag() != dwarf::DW_TAG_member)
       continue;
-    if (memberIndex++ == index)
-      return Member;
+    // A static member has no storage in the object, and an artificial one
+    // (a vtable pointer) is not something the source can name.
+    if (Member->isStaticMember() || Member->isArtificial())
+      continue;
+    if (Member->getOffsetInBits() != offsetInBits)
+      continue;
+    // Several bitfields share one storage unit, so the recorded value is not
+    // the value of any single one of them.
+    if (Member->isBitField())
+      return nullptr;
+    if (found)
+      return nullptr;
+    found = Member;
   }
-  return nullptr;
+  return found;
+}
+
+unsigned countDIArrayDims(const DICompositeType *CT) {
+  unsigned dims = 0;
+  for (DINode *N : CT->getElements())
+    if (isa<DISubrange>(N))
+      ++dims;
+  return dims;
+}
+
+// DWARF folds every dimension of a multi-dimensional array into one node, so
+// consuming a subscript may leave the remaining dimensions in place.
+const DIType *stepIntoDIArray(const DIType *T, unsigned &dimsLeft) {
+  auto *CT = dyn_cast_or_null<DICompositeType>(stripDIAliases(T));
+  if (!CT || CT->getTag() != dwarf::DW_TAG_array_type)
+    return nullptr;
+
+  if (dimsLeft == 0)
+    dimsLeft = countDIArrayDims(CT);
+  if (dimsLeft == 0)
+    return nullptr;
+
+  if (--dimsLeft > 0)
+    return T;
+  return stripDIAliases(CT->getBaseType());
 }
 
 std::string sourceIndex(const Value *V) {
@@ -142,8 +195,11 @@ SmackInstGenerator::findSourceExprs(const llvm::Value *V) const {
   if (I != sourceExprs.end())
     return &I->second;
 
+  // Only follow a strip that preserves the pointee type; a bitcast to another
+  // pointee would let the next GEP resolve field indices against the wrong
+  // debug type.
   const Value *Stripped = V->stripPointerCastsAndAliases();
-  if (Stripped != V) {
+  if (Stripped != V && Stripped->getType() == V->getType()) {
     I = sourceExprs.find(Stripped);
     if (I != sourceExprs.end())
       return &I->second;
@@ -178,8 +234,9 @@ SmackInstGenerator::sourceLValues(const llvm::Value *Pointer) const {
   return Results;
 }
 
-void SmackInstGenerator::rememberLoadSourceExpr(llvm::LoadInst &I) {
-  for (const auto &E : sourceLValues(I.getPointerOperand()))
+void SmackInstGenerator::rememberLoadSourceExpr(
+    llvm::LoadInst &I, const std::vector<SourceExpr> &LValues) {
+  for (const auto &E : LValues)
     rememberSourceExpr(&I, {E.name, E.type, false, E.isDerived});
 }
 
@@ -188,34 +245,55 @@ void SmackInstGenerator::rememberGEPSourceExpr(llvm::GetElementPtrInst &I) {
   if (!Bases)
     return;
 
-  for (const auto &Base : *Bases) {
+  // Copy the bases: recording a new expression for this instruction may grow
+  // the map, and we would otherwise be iterating a vector inside it.
+  const std::vector<SourceExpr> Sources = *Bases;
+
+  for (const auto &Base : Sources) {
     std::string Name = Base.name;
     const DIType *DITy = Base.isAddress ? stripDIAliases(Base.type)
                                         : dereferenceDIType(Base.type);
     Type *IRTy = I.getSourceElementType();
-    bool UseArrow = !Base.isAddress;
+    // A pointer value still owes a dereference: the first member access spends
+    // it as '->', and the first subscript spends it as '(*p)[i]'.
+    bool PendingDeref = !Base.isAddress;
     bool Derived = Base.isDerived;
     bool Valid = DITy != nullptr;
+    unsigned Dims = 0;
     unsigned Position = 0;
 
     for (auto Index = I.idx_begin(), End = I.idx_end(); Valid && Index != End;
          ++Index, ++Position) {
       Value *IndexValue = Index->get();
 
       // The first index steps through the pointer operand. A zero index names
-      // the same source object and leaves '.' versus '->' to the first member.
+      // the same source object and leaves the dereference to the next index.
       if (Position == 0) {
         auto *CI = dyn_cast<ConstantInt>(IndexValue);
-        if (!CI || !CI->isZero()) {
-          std::string IndexName = sourceIndex(IndexValue);
-          if (IndexName.empty()) {
+        if (CI && CI->isZero())
+          continue;
+
+        std::string IndexName = sourceIndex(IndexValue);
+        if (IndexName.empty()) {
+          Valid = false;
+          break;
+        }
+
+        if (Base.isAddress) {
+          // Subscripting the address of an object only names an element when
+          // that object is an array; otherwise this is pointer arithmetic
+          // running past it, and 'x[1]' would name something that x is not.
+          const DIType *ElemDITy = stepIntoDIArray(DITy, Dims);
+          if (!ElemDITy) {
             Valid = false;
             break;
           }
-          Name += "[" + IndexName + "]";
-          UseArrow = false;
-          Derived = true;
+          DITy = ElemDITy;
         }
+
+        Name += "[" + IndexName + "]";
+        PendingDeref = false;
+        Derived = true;
         continue;
       }
 
@@ -227,17 +305,22 @@ void SmackInstGenerator::rememberGEPSourceExpr(llvm::GetElementPtrInst &I) {
         }
 
         unsigned Field = CI->getZExtValue();
-        const DIDerivedType *Member = getDIMember(DITy, Field);
+        const DIDerivedType *Member =
+            getDIMemberAtOffset(DITy, I.getModule()
+                                          ->getDataLayout()
+                                          .getStructLayout(ST)
+                                          ->getElementOffsetInBits(Field));
         if (!Member || Member->getName().empty()) {
           Valid = false;
           break;
         }
 
-        Name += (UseArrow ? "->" : ".") + Member->getName().str();
-        UseArrow = false;
+        Name += (PendingDeref ? "->" : ".") + Member->getName().str();
+        PendingDeref = false;
         Derived = true;
         IRTy = ST->getElementType(Field);
         DITy = stripDIAliases(Member->getBaseType());
+        Dims = 0;
         continue;
       }
 
@@ -246,21 +329,27 @@ void SmackInstGenerator::rememberGEPSourceExpr(llvm::GetElementPtrInst &I) {
         Valid = false;
         break;
       }
-      Name += "[" + IndexName + "]";
-      UseArrow = false;
-      Derived = true;
 
-      if (auto *AT = dyn_cast<ArrayType>(IRTy)) {
-        IRTy = AT->getElementType();
-        auto *CT = dyn_cast_or_null<DICompositeType>(stripDIAliases(DITy));
-        DITy = CT ? stripDIAliases(CT->getBaseType()) : nullptr;
-      } else if (auto *VT = dyn_cast<VectorType>(IRTy)) {
-        IRTy = VT->getElementType();
-        auto *CT = dyn_cast_or_null<DICompositeType>(stripDIAliases(DITy));
-        DITy = CT ? stripDIAliases(CT->getBaseType()) : nullptr;
-      } else {
+      Type *ElemIRTy = nullptr;
+      if (auto *AT = dyn_cast<ArrayType>(IRTy))
+        ElemIRTy = AT->getElementType();
+      else if (auto *VT = dyn_cast<FixedVectorType>(IRTy))
+        ElemIRTy = VT->getElementType();
+
+      const DIType *ElemDITy = stepIntoDIArray(DITy, Dims);
+      if (!ElemIRTy || !ElemDITy) {
         Valid = false;
+        break;
       }
+
+      // '*p' subscripted is '(*p)[i]'; 'p[i]' would name a different address.
+      if (PendingDeref)
+        Name = "(*" + Name + ")";
+      Name += "[" + IndexName + "]";
+      PendingDeref = false;
+      Derived = true;
+      IRTy = ElemIRTy;
+      DITy = ElemDITy;
     }
 
     if (Valid)
@@ -269,26 +358,42 @@ void SmackInstGenerator::rememberGEPSourceExpr(llvm::GetElementPtrInst &I) {
 }
 
 void SmackInstGenerator::rememberCastSourceExpr(llvm::CastInst &I) {
+  // A cast that changes the type no longer describes the same source object:
+  // the pointee of a bitcast decides which struct the next GEP resolves its
+  // field indices against, and an integer cast changes the value outright.
+  if (I.getSrcTy() != I.getDestTy())
+    return;
+
   auto *Exprs = findSourceExprs(I.getOperand(0));
   if (!Exprs)
     return;
-  for (const auto &E : *Exprs)
+  const std::vector<SourceExpr> Sources = *Exprs;
+  for (const auto &E : Sources)
     rememberSourceExpr(&I, E);
 }
 
-void SmackInstGenerator::recordSourceLValues(const llvm::Value *Pointer,
-                                             const llvm::Value *Value) {
-  if (!SmackOptions::SourceLocSymbols || Value->getType()->isAggregateType())
+void SmackInstGenerator::recordDerivedLValues(
+    const std::vector<SourceExpr> &LValues, const llvm::Value *V) {
+  // boogie_si_record_* models a single scalar; an aggregate or a vector has no
+  // counterexample value to print.
+  llvm::Type *T = V->getType();
+  if (!SmackOptions::SourceLocSymbols || T->isAggregateType() ||
+      T->isVectorTy() || T->isVoidTy())
     return;
 
   std::set<std::string> Recorded;
-  for (const auto &E : sourceLValues(Pointer)) {
+  for (const auto &E : LValues) {
     if (!E.isDerived || !Recorded.insert(E.name).second)
       continue;
-    emit(recordProcedureCall(Value, {Attr::attr("cexpr", E.name)}));
+    emit(recordProcedureCall(V, {Attr::attr("cexpr", E.name)}));
   }
 }
 
+void SmackInstGenerator::recordSourceLValues(const llvm::Value *Pointer,
+                                             const llvm::Value *V) {
+  recordDerivedLValues(sourceLValues(Pointer), V);
+}
+
 const Stmt *
 SmackInstGenerator::recordProcedureCall(const llvm::Value *V,
                                         std::list<const Attr *> attrs) {
@@ -725,8 +830,9 @@ void SmackInstGenerator::visitLoadInst(llvm::LoadInst &li) {
   }
 
   emit(Stmt::assign(rep->expr(&li), E));
-  rememberLoadSourceExpr(li);
-  recordSourceLValues(P, &li);
+  auto LValues = sourceLValues(P);
+  rememberLoadSourceExpr(li, LValues);
+  recordDerivedLValues(LValues, &li);
 
   if (SmackOptions::MemoryModelDebug) {
     emit(Stmt::call(Naming::REC_MEM_OP, {Expr::id(Naming::MEM_OP_VAL)}));
@@ -1474,7 +1580,6 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
           {llvm::Intrinsic::ctlz, ctlz},
           {llvm::Intrinsic::ctpop, ctpop},
           {llvm::Intrinsic::cttz, cttz},
-          {llvm::Intrinsic::dbg_declare, ignore},
           {llvm::Intrinsic::dbg_label, ignore},
           {llvm::Intrinsic::copysign, copysign},
           {llvm::Intrinsic::expect, identity},

test/c/data/source-expr/config.yml

@@ -0,0 +1,3 @@
+# Recorded source expressions are only rendered into a counterexample by
+# Corral's /printDataValues, so @checkout cannot match under Boogie.
+verifiers: [corral]

test/c/data/source-expr/source_expr_array.c

@@ -0,0 +1,21 @@
+#include "smack.h"
+
+// @expect verified
+// @checkbpl grep -F 'call {:cexpr "(*pa)[2]"} boogie_si_record_i32'
+// @checkbpl awk '/cexpr "pa\[2\]"/ { exit 1 }'
+// @checkbpl awk '/cexpr "x\[1\]"/ { exit 1 }'
+// @checkbpl grep -F 'call {:cexpr "m[1][2]"} boogie_si_record_i32'
+
+// (*pa)[2] and pa[2] are different addresses, and a scalar's address is not an
+// array; both used to be recorded under the wrong name.
+int main(void) {
+  int x = 1;
+  int arr[4];
+  int(*pa)[4] = &arr;
+  int m[3][4];
+
+  (*pa)[2] = 2;
+  m[1][2] = 3;
+  assert((*pa)[2] == 2 && m[1][2] == 3 && x == 1);
+  return 0;
+}

test/c/data/source-expr/source_expr_bitfield.c

@@ -0,0 +1,23 @@
+#include "smack.h"
+
+// @expect verified
+// @checkbpl grep -F 'call {:cexpr "b->after"} boogie_si_record_i32'
+// @checkbpl awk '/cexpr "b->f1"/ { exit 1 }'
+// @checkbpl awk '/cexpr "b->f2"/ { exit 1 }'
+
+// Two bitfields share one LLVM storage unit, so the third member sits at LLVM
+// field index 1 while it is the third DW_TAG_member. Naming it by ordinal
+// position reported it as f2.
+struct bits {
+  unsigned f1 : 3;
+  unsigned f2 : 5;
+  int after;
+};
+
+int main(void) {
+  struct bits s;
+  struct bits *b = &s;
+  b->after = 42;
+  assert(b->after == 42);
+  return 0;
+}