impl.cpp

#include "generated.h"
#include "clang/Driver/Driver.h"
#include "clang/Frontend/FrontendActions.h"
#include "clang/Lex/MacroArgs.h"
#include "clang/Tooling/CompilationDatabase.h"
#include "clang/Tooling/Tooling.h"
#include <dlfcn.h>
#include <map>
#include <optional>
#include <sstream>
#include <unordered_set>
#include <vector>

using namespace clang;
using namespace clang::tooling;
using rust::Ref;
using rust::RefMut;
using rust::std::rc::Rc;
using rust::std::vec::Vec;
using namespace rust::pal::clang;
namespace ir = rust::pal::ir;
using OptExpr = rust::core::option::Option<Rc<ir::Expr>>;

llvm::StringRef toStringRef(Ref<rust::Str> str) {
  return llvm::StringRef((char const *)str.as_ptr(), str.len());
}

std::string toString(Ref<rust::Str> str) {
  return std::string((char const *)str.as_ptr(), str.len());
}

Ref<rust::Str> toStr(llvm::StringRef const &str) {
  return str_from_parts((uint8_t const *)str.data(), str.size());
}

Ref<rust::Str> toStr(std::string const &str) {
  return str_from_parts((uint8_t const *)str.data(), str.size());
}

// Returns true if `s` contains a `continue` that binds to the enclosing loop,
// i.e. a `continue` that is not nested inside another loop. Nested `for`,
// `while`, and `do-while` loops act as boundaries (their `continue` belongs to
// them), so we do not descend into them. A `switch` does NOT capture `continue`
// in C, so we descend into it (and into `if`, blocks, labels, etc.).
static bool hasTopLevelContinue(const Stmt *s) {
  if (!s)
    return false;
  if (isa<ContinueStmt>(s))
    return true;
  if (isa<ForStmt>(s) || isa<WhileStmt>(s) || isa<DoStmt>(s))
    return false;
  for (const Stmt *child : s->children())
    if (hasTopLevelContinue(child))
      return true;
  return false;
}

// A `break` that would bind to the enclosing do-while. Unlike `continue`, a
// `break` also binds to a `switch`, so a switch is a boundary here and is not
// one above.
static bool hasTopLevelBreak(const Stmt *s) {
  if (!s)
    return false;
  if (isa<BreakStmt>(s))
    return true;
  if (isa<ForStmt>(s) || isa<WhileStmt>(s) || isa<DoStmt>(s) ||
      isa<SwitchStmt>(s))
    return false;
  for (const Stmt *child : s->children())
    if (hasTopLevelBreak(child))
      return true;
  return false;
}

using SnipMap = rust::pal::hauntedc::SnippetMap;
using TargetIntWidths = rust::pal::hauntedc::TargetIntWidths;

template <> struct std::hash<FileID> {
  std::size_t operator()(FileID const &s) const noexcept {
    return s.getHashValue();
  }
};
struct RangeMap {
  RangeMap(RefMut<Ctx> &c) : ctx(c) {}
  RefMut<Ctx> ctx;
  std::unordered_map<FileID, Rc<rust::Str>> files;

  Rc<rust::Str> getFileName(SourceManager &sm, FileID id) {
    if (auto result = files.find(id); result != files.end()) {
      return result->second.clone();
    } else {
      rust::Ref<rust::Str> fn = "<unknown>"_rs;
      if (id.isValid()) {
        if (auto entryRef = sm.getFileEntryRefForID(id)) {
          fn = toStr(entryRef->getName());
        }
      }
      auto res = ctx.intern_str(fn);
      files[id] = res.clone();
      return res;
    }
  }

  Rc<ir::SourceInfo> getExpansionRange(SourceManager &sm, SourceRange range) {
    return mk_original_location(
        getFileName(sm, sm.getFileID(sm.getExpansionLoc(range.getBegin()))),
        sm.getExpansionLineNumber(range.getBegin()),
        sm.getExpansionColumnNumber(range.getBegin()),
        sm.getExpansionLineNumber(range.getEnd()),
        sm.getExpansionColumnNumber(range.getEnd()));
  }
};

class MacroTracker : public PPCallbacks {
public:
  MacroTracker(RangeMap &m, SnipMap &s, CompilerInstance &ci)
      : rangeMap(m), snippets(s), compilerInst(ci) {}
  RangeMap &rangeMap;
  SnipMap &snippets;
  CompilerInstance &compilerInst;

  void MacroExpands(Token const &MacroNameTok, MacroDefinition const &MD,
                    SourceRange Range, MacroArgs const *Args) override {
    auto &sm = compilerInst.getSourceManager();
    auto &langOpts = compilerInst.getLangOpts();
    if (Args) {
      InlineCodeBuilder toks = InlineCodeBuilder::new_();
      unsigned numArgs = Args->getNumMacroArguments();
      for (unsigned i = 0; i < numArgs; ++i) {
        Token const *argTokens = Args->getUnexpArgument(i);
        unsigned numTokens = Args->getArgLength(argTokens);

        for (unsigned j = 0; j < numTokens; ++j) {
          auto &tok = argTokens[j];
          std::string spelling = Lexer::getSpelling(tok, sm, langOpts);

          Rc<ir::SourceInfo> loc;
          SourceLocation tokLoc = sm.getSpellingLoc(tok.getLocation());
          if (auto fileID = sm.getFileID(tokLoc); fileID.isValid()) {
            unsigned beginLine = sm.getSpellingLineNumber(tokLoc);
            unsigned beginChar = sm.getSpellingColumnNumber(tokLoc);
            unsigned endLine = beginLine;
            unsigned endChar = beginChar + spelling.length();
            loc = mk_original_location(rangeMap.getFileName(sm, fileID),
                                       beginLine, beginChar, endLine, endChar);
          } else {
            auto expansionRange = sm.getExpansionRange(
                SourceRange(tok.getLocation(), tok.getEndLoc()));
            unsigned beginLine =
                sm.getExpansionLineNumber(expansionRange.getBegin());
            unsigned beginChar =
                sm.getExpansionColumnNumber(expansionRange.getBegin());
            unsigned endLine =
                sm.getExpansionLineNumber(expansionRange.getEnd());
            unsigned endChar =
                sm.getExpansionColumnNumber(expansionRange.getEnd());
            loc = mk_fallback_sourceinfo(mk_original_location(
                rangeMap.getFileName(sm,
                                     sm.getFileID(expansionRange.getBegin())),
                beginLine, beginChar, endLine, endChar));
          }

          Ref<rust::Str> before = tok.isAtStartOfLine()   ? "\n"_rs
                                  : tok.hasLeadingSpace() ? " "_rs
                                                          : ""_rs;
          toks.push_token(before, std::move(loc), toStr(spelling));
        }
      }
      unsigned ctr = compilerInst.getPreprocessor().getCounterValue();
      toks.insert_into_map(ctr, snippets);
    }
  }
};

Rc<rust::num_bigint::BigInt> toBigInt(llvm::APInt const &n) {
  llvm::SmallString<16> out;
  n.toStringSigned(out);
  return mk_bigint(toStr(out));
}

Rc<rust::num_bigint::BigInt> toBigInt(llvm::APSInt const &n) {
  llvm::SmallString<16> out;
  n.toString(out);
  return mk_bigint(toStr(out));
}

struct AnonNameGen {
  llvm::StringRef base;
  unsigned i = 0;

  AnonNameGen(llvm::StringRef b) : base(b) {}

  std::string next() {
    std::ostringstream out;
    out.write(base.data(), base.size());
    out << "_anon_" << ++i;
    return out.str();
  }
};

class PALConsumer : public ASTConsumer {
public:
  PALConsumer(RefMut<Ctx> c, RangeMap &m, SnipMap &s, CompilerInstance &ci)
      : ctx(c), rangeMap(m), snippets(s), sm(ci.getSourceManager()) {}

  RefMut<Ctx> ctx;
  RangeMap &rangeMap;
  SnipMap &snippets;
  SourceManager &sm;
  ASTContext *astCtx = nullptr;
  std::unordered_set<RecordDecl *>
      alreadyDefined; // guard against recursive structures
  std::unordered_map<RecordDecl *, std::string>
      structNames; // map record decls to generated struct names
  Expr *forLoopIncrement = nullptr;

  // Where a statement expression used as an rvalue may put the statements
  // ahead of its value, or null if there is nowhere to put them.
  //
  // Set only by trStmt, and only for a position that is genuinely a statement
  // context evaluated exactly once: a declaration's initializer, and the
  // right-hand side of an assignment statement. It is cleared again around any
  // operand that C evaluates conditionally -- ?:'s arms, &&'s and ||'s right
  // operand -- where running the statements unconditionally would change the
  // program. See the StmtExpr arm in trRValue.
  Vec<Rc<ir::Stmt>> *hoistTarget = nullptr;

  // Clears hoistTarget for the extent of a conditionally-evaluated operand.
  struct NoHoist {
    Vec<Rc<ir::Stmt>> **slot;
    Vec<Rc<ir::Stmt>> *saved;
    explicit NoHoist(Vec<Rc<ir::Stmt>> **s) : slot(s), saved(*s) {
      *slot = nullptr;
    }
    ~NoHoist() { *slot = saved; }
  };
  // When inside a switch desugaring, break sets this flag instead of mk_break
  Rc<ir::Ident> *switchBreakId = nullptr;

  // The arm a `?:` actually takes, when clang can decide the condition at
  // compile time, or null when it cannot.
  //
  // C evaluates exactly one arm of a conditional, so when the condition is a
  // constant the program IS that arm and nothing else. Translating the whole
  // conditional is not merely wasteful, it is wrong in the way that matters
  // here: the arm that is never taken is often not meant to be compiled at
  // all. Generated RPC-stub headers can wrap every call argument in
  // a test like
  //
  //   (__builtin_classify_type(x) == 12 || __builtin_classify_type(x) == 13)
  //       ? ERROR__Struct_or_union_arguments_not_allowed_in_call()
  //       : (uint64_t)(x)
  //
  // where the error function is declared and deliberately never defined, so
  // that a struct argument fails to link. Once the classify_type calls fold,
  // the condition is `1 == 12 || 1 == 13` and the dead arm is a call to a
  // function PAL has no body for -- which, before this, both introduced an
  // admitted module and made the conditional ill-typed, since the two arms'
  // types agree in C but not after PAL maps a typedef and its underlying type
  // to different F* names ("The branches of a conditional must return the same
  // type: Typedef_uint64_t.ty_uint64_t and UInt64.t").
  //
  // Requiring the condition to be side-effect free is what makes dropping it
  // sound: `f() ? a : b` must still call f. HasSideEffects is asked
  // separately from the evaluation because EvaluateAsBooleanCondition has no
  // equivalent of EvaluateAsInt's SE_NoSideEffects.
  Expr *constantCondArm(const ConditionalOperator *co) {
    bool val = false;
    if (co->getCond()->HasSideEffects(*astCtx) ||
        !co->getCond()->EvaluateAsBooleanCondition(val, *astCtx)) {
      return nullptr;
    }
    return val ? co->getTrueExpr() : co->getFalseExpr();
  }

  // TODO: should probably wait with translation until after parsing

  void Initialize(ASTContext &Context) override {
    astCtx = &Context;
    auto const &TI = Context.getTargetInfo();
    ctx.set_target_int_widths(
        TargetIntWidths(TI.getCharWidth(), TI.getShortWidth(), TI.getIntWidth(),
                        TI.getLongWidth(), TI.getLongLongWidth()));
  }

  virtual bool HandleTopLevelDecl(DeclGroupRef DG) override {
    for (auto D : DG)
      HandleDecl(D);
    return ASTConsumer::HandleTopLevelDecl(DG);
  }

  Rc<ir::Ident> getDeclName(NamedDecl *d) {
    auto loc = mk_fallback_sourceinfo(
        getRange(d->getSourceRange())); // TODO: get range of name token
    return ctx.mk_ident(toStr(d->getName()), std::move(loc));
  }

  // Name to use for a struct/union field. Unnamed fields (e.g. C11 anonymous
  // struct/union members) have no identifier, so we synthesize a stable name
  // from the field's index within its record. The index is deterministic and
  // shared by the field definition and every member access referring to it, so
  // the synthesized names stay consistent across the whole translation.
  std::string fieldNameStr(FieldDecl const *f) {
    if (f->getIdentifier())
      return f->getName().str();
    return "_unnamed" + std::to_string(f->getFieldIndex());
  }

  RecordDecl *recordKey(RecordDecl *decl) {
    return cast<RecordDecl>(decl->getCanonicalDecl());
  }

  Rc<ir::SourceInfo> getRange(SourceRange const &range) {
    return rangeMap.getExpansionRange(sm, range);
  }

  template <typename T>
  void reportUnsupported(SourceRange const &rng, Rc<ir::SourceInfo> const &loc,
                         char const *msg, T const &extra) {
    if (!sm.isInMainFile(sm.getExpansionLoc(rng.getBegin()))) {
      // only complain about unsupported syntax in main file
      return;
    }
    ctx.report_diag(loc.clone(), true, toStr(std::string(msg) + extra));
  }

  // Translate a single struct/union field into the IR, pushing it onto the
  // given builder. Handles plain fields and unsigned bit-fields; rejects
  // signed bit-fields and skips anonymous/zero-width padding bit-fields.
  void addRecordField(DeclBuilder &builder, FieldDecl *f,
                      AnonNameGen *liftStructs, bool inUnion) {
    auto floc = getRange(f->getSourceRange());
    if (f->isBitField()) {
      // Anonymous / zero-width bit-fields are pure padding with no accessible
      // value; drop them entirely.
      if (f->isUnnamedBitField())
        return;
      // Bit-fields are only modeled inside structs; union bit-fields would need
      // the same value-based encoding layered on the union variant model.
      if (inUnion) {
        reportUnsupported(f->getSourceRange(), floc,
                          "unsupported bit-field in union", "");
        return;
      }
      // Only unsigned (and _Bool) bit-fields are modeled. Signed bit-fields
      // would need sign-extension on read and have implementation-defined
      // out-of-range write semantics (C11 6.3.1.3p3), so reject them.
      if (!f->getType()->isUnsignedIntegerType()) {
        reportUnsupported(
            f->getSourceRange(), floc,
            "unsupported signed bit-field (only unsigned bit-fields are "
            "supported)",
            "");
        return;
      }
      unsigned width = f->getBitWidthValue();
      builder.field_bitfield(
          ctx.mk_ident(toStr(fieldNameStr(f)), std::move(floc)),
          trQualType(f->getType(), f->getSourceRange(), liftStructs), width);
      return;
    }
    auto qt = f->getType();
    auto *qtPtr = qt.IgnoreParens().getTypePtr();
    if (auto *iat = dyn_cast<IncompleteArrayType>(qtPtr)) {
      // Flexible array member: `T name[]` as the last field of a struct (C11
      // 6.7.2.1). Clang guarantees it is the last field. Model it inline as an
      // unsized `array_spec T` in the noeq record; a `_refines(...)` clause on
      // the field supplies an optional length refinement.
      if (inUnion) {
        reportUnsupported(f->getSourceRange(), floc,
                          "unsupported flexible array member in union", "");
        return;
      }
      auto elemTy =
          trQualType(iat->getElementType(), f->getSourceRange(), liftStructs);
      builder.field(
          ctx.mk_ident(toStr(fieldNameStr(f)), std::move(floc)),
          trTypeAttrs(f->getAttrs(),
                      mk_flex_array_type(getRange(f->getSourceRange()),
                                         std::move(elemTy))));
    } else if (isa<VariableArrayType>(qtPtr)) {
      reportUnsupported(f->getSourceRange(), floc,
                        "unsupported non-constant-length array field", "");
    } else {
      builder.field(
          ctx.mk_ident(toStr(fieldNameStr(f)), std::move(floc)),
          trTypeAttrs(f->getAttrs(),
                      trQualType(f->getType(), f->getSourceRange(), liftStructs,
                                 findFnProtoTypeLoc(f->getTypeSourceInfo())),
                      f->getType(), f->getSourceRange()));
    }
  }

  void trRecordDecl(Rc<ir::Ident> ident, RecordDecl *decl,
                    AnonNameGen *liftStructs) {
    auto key = recordKey(decl);
    if (!decl->isCompleteDefinition()) {
      if (decl->getTagKind() == TagTypeKind::Struct) {
        auto loc = getRange(decl->getSourceRange());
        ctx.add_struct_decl(std::move(loc), std::move(ident));
      }
      return;
    }
    if (!alreadyDefined.insert(key).second)
      return;
    auto loc = getRange(decl->getSourceRange());
    auto builder = DeclBuilder::new_(loc.clone(), ident.clone());
    if (decl->getTagKind() == TagTypeKind::Struct) {
      builder.refines(trTypeAttrs(decl->getAttrs(),
                                  mk_type_struct(loc.clone(), ident.clone())));
      // Check for struct-level attributes
      if (decl->hasAttrs()) {
        for (auto *attr : decl->getAttrs()) {
          if (auto *ann = dyn_cast<AnnotateAttr>(attr)) {
            if (ann->getAnnotation() == "pal-eager-unfold-predicate" &&
                ann->args_size() == 0) {
              builder.set_eager_unfold_pred();
            }
          }
        }
      }
      // Process nested record declarations (inner structs/unions)
      for (auto *D : decl->decls()) {
        if (auto *inner = dyn_cast<RecordDecl>(D)) {
          if (inner->isCompleteDefinition() && inner->getIdentifier()) {
            auto innerLoc = getRange(inner->getSourceRange());
            auto innerName =
                ctx.mk_ident(toStr(inner->getName()), innerLoc.clone());
            auto innerAnon = AnonNameGen(inner->getName());
            trRecordDecl(std::move(innerName), inner, &innerAnon);
          }
        }
      }
      for (auto f : decl->fields()) {
        addRecordField(builder, f, liftStructs, /*inUnion=*/false);
      }
      ctx.add_struct(std::move(builder));
    } else if (decl->getTagKind() == TagTypeKind::Union) {
      // Process nested record declarations (inner structs/unions)
      for (auto *D : decl->decls()) {
        if (auto *inner = dyn_cast<RecordDecl>(D)) {
          if (inner->isCompleteDefinition() && inner->getIdentifier()) {
            auto innerLoc = getRange(inner->getSourceRange());
            auto innerName =
                ctx.mk_ident(toStr(inner->getName()), innerLoc.clone());
            auto innerAnon = AnonNameGen(inner->getName());
            trRecordDecl(std::move(innerName), inner, &innerAnon);
          }
        }
      }
      for (auto f : decl->fields()) {
        addRecordField(builder, f, liftStructs, /*inUnion=*/true);
      }
      ctx.add_union(std::move(builder));
    } else {
      reportUnsupported(decl->getSourceRange(), loc, "unsupported record kind",
                        "");
    }
  }

  Rc<ir::Type> trFnPtrType(const FunctionProtoType *proto, SourceRange range,
                           Rc<ir::SourceInfo> loc,
                           AnonNameGen *liftStructs = nullptr,
                           FunctionProtoTypeLoc protoLoc = {}) {
    auto args = Vec<Rc<ir::Type>>::new_();
    for (unsigned i = 0; i < proto->getNumParams(); ++i) {
      ParmVarDecl *paramDecl = protoLoc && i < protoLoc.getNumParams()
                                   ? protoLoc.getParam(i)
                                   : nullptr;
      SourceRange paramRange = paramDecl ? paramDecl->getSourceRange() : range;
      auto param = trQualType(
          proto->getParamType(i), paramRange, liftStructs,
          paramDecl ? findFnProtoTypeLoc(paramDecl->getTypeSourceInfo())
                    : FunctionProtoTypeLoc{});
      if (paramDecl) {
        param = trTypeAttrs(paramDecl->getAttrs(), std::move(param),
                            paramDecl->getType(), paramRange);
      }
      args.push(std::move(param));
    }
    auto ret = trQualType(proto->getReturnType(), range, liftStructs);
    return mk_type_fnptr(std::move(loc), std::move(args), std::move(ret));
  }

  FunctionProtoTypeLoc findFnProtoTypeLoc(TypeSourceInfo *typeInfo) {
    if (!typeInfo)
      return {};
    for (TypeLoc typeLoc = typeInfo->getTypeLoc(); typeLoc;
         typeLoc = typeLoc.getNextTypeLoc()) {
      if (auto protoLoc = typeLoc.getAs<FunctionProtoTypeLoc>())
        return protoLoc;
    }
    return {};
  }

  Rc<ir::Type> trQualType(QualType t, SourceRange range,
                          AnonNameGen *liftStructs = nullptr,
                          FunctionProtoTypeLoc protoLoc = {}) {
    t = t.IgnoreParens();
    auto loc = getRange(range);

    if (t.getAsString() == "size_t") {
      return mk_sizet(std::move(loc));
    } else if (auto typeOf = dyn_cast<TypeOfType>(t)) {
      return trQualType(typeOf->desugar(), range, liftStructs);
    } else if (auto typeOfExpr = dyn_cast<TypeOfExprType>(t)) {
      return trQualType(typeOfExpr->desugar(), range, liftStructs);
    } else if (auto tydef = dyn_cast<TypedefType>(t)) {
      auto id = ctx.mk_ident(toStr(tydef->getDecl()->getName()), loc.clone());
      return mk_type_typedef(std::move(loc), std::move(id));
#if LLVM_VERSION_MAJOR < 22
    } else if (auto elab = dyn_cast<ElaboratedType>(t)) {
      return trQualType(elab->desugar(), range, liftStructs);
#endif
    } else if (auto ptr = dyn_cast<PointerType>(t)) {
      // Pointer to a (prototyped) function: `R (*)(A0, A1, ...)`. Modeled as a
      // dedicated function-pointer IR type with the argument types collected in
      // order and tupled on emission.
      if (auto proto = ptr->getPointeeType()->getAs<FunctionProtoType>()) {
        return trFnPtrType(proto, range, loc.clone(), liftStructs, protoLoc);
      }
      return mk_pointer_unknown(
          std::move(loc),
          trQualType(ptr->getPointeeType(), /*TODO*/ range, liftStructs));
    } else if (auto proto = t->getAs<FunctionProtoType>()) {
      // A bare (undecayed) function type reached as a value type — treat the
      // function-to-pointer decay result the same as a function pointer.
      return trFnPtrType(proto, range, std::move(loc), liftStructs, protoLoc);
    } else if (auto adj = dyn_cast<AdjustedType>(t)) {
      return trQualType(adj->getOriginalType(), range, liftStructs, protoLoc);
    } else if (auto cat = dyn_cast<ConstantArrayType>(t)) {
      return mk_fixed_array_type(
          std::move(loc),
          trQualType(cat->getElementType(), /* TODO */ range, liftStructs),
          cat->getSize().getZExtValue());
    } else if (auto arr = dyn_cast<ArrayType>(t)) {
      // VLA or incomplete array — decays to pointer
      return mk_pointer_array(
          std::move(loc),
          trQualType(arr->getElementType(), /* TODO */ range, liftStructs));
    } else if (auto rec = dyn_cast<RecordType>(t)) {
      auto decl = rec->getDecl();
      auto key = recordKey(decl);
      Rc<ir::Ident> name;
      if (auto it = structNames.find(key); it != structNames.end()) {
        name = ctx.mk_ident(toStr(it->second), loc.clone());
      } else if (decl->getIdentifier()) {
        structNames.emplace(key, decl->getName().str());
        name = ctx.mk_ident(toStr(decl->getName()), loc.clone());
      } else if (liftStructs) {
        auto nameStr = liftStructs->next();
        structNames.emplace(key, nameStr);
        name = ctx.mk_ident(toStr(nameStr), loc.clone());
        trRecordDecl(name.clone(), decl, liftStructs);
      } else {
        reportUnsupported(
            range, loc, "unsupported anonymous struct/union outside of typedef",
            "");
        return mk_type_err(std::move(loc));
      }
      switch (decl->getTagKind()) {
      case TagTypeKind::Struct: {
        return mk_type_struct(std::move(loc), std::move(name));
      }
      case TagTypeKind::Union: {
        return mk_type_union(std::move(loc), std::move(name));
      }
      default: {
        reportUnsupported(range, loc, "unsupported record kind", "");
        return mk_type_err(std::move(loc));
      }
      }
    }
    if (t->isVoidType()) {
      return mk_void_type(std::move(loc));
    }
    if (isBoolType(t)) {
      return mk_bool_type(std::move(loc));
    }
    if (t->isSpecificBuiltinType(BuiltinType::Float)) {
      return mk_float_type(std::move(loc), 32);
    }
    if (t->isSpecificBuiltinType(BuiltinType::Double)) {
      return mk_float_type(std::move(loc), 64);
    }
    if (t->isFloatingType()) {
      reportUnsupported(range, loc, "unsupported floating-point type ",
                        t.getAsString());
      return mk_type_err(std::move(loc));
    }
    if (t->isSignedIntegerType() || t->isUnsignedIntegerType()) {
      bool isSigned = t->isSignedIntegerType();
      unsigned width = astCtx->getIntWidth(t);
      return mk_int_type(std::move(loc), isSigned, width);
    }

    reportUnsupported(range, loc, "unsupported type ", t->getTypeClassName());
    return mk_type_err(std::move(loc));
  }

  // `_array`, `_arrayptr` and `_core_ref` reclassify a *pointer*. When the
  // declared type only reaches the pointer through a typedef (e.g.
  // `typedef E* PE;`), the translated type is an opaque type reference and the
  // classification has nothing to attach to. Desugar to the underlying pointer
  // type in that case so the attribute applies to the pointer it names.
  static bool isPointerKindAttr(AnnotateAttr *ann) {
    if (ann->args_size() != 0)
      return false;
    auto name = ann->getAnnotation();
    return name == "pal-array" || name == "pal-arrayptr" ||
           name == "pal-core-ref";
  }

  Rc<ir::Type> desugarPointerTypedef(Rc<ir::Type> &&ty, QualType declQt,
                                     SourceRange declRange) {
    if (declQt.isNull())
      return std::move(ty);
    auto qt = declQt.IgnoreParens();
    auto ptr = qt->getAs<PointerType>();
    if (!ptr || isa<PointerType>(qt.getTypePtr()))
      return std::move(ty);
    return trQualType(astCtx->getPointerType(ptr->getPointeeType()), declRange);
  }

  Rc<ir::Type> trTypeAttrs(AttrVec const &attrs, Rc<ir::Type> &&ty,
                           QualType declQt = QualType(),
                           SourceRange declRange = SourceRange()) {
    for (auto attr : attrs) {
      if (auto ann = dyn_cast<AnnotateAttr>(attr)) {
        if (isPointerKindAttr(ann)) {
          ty = desugarPointerTypedef(std::move(ty), declQt, declRange);
          break;
        }
      }
    }
    bool sawNullable = false;
    std::optional<Rc<ir::SourceInfo>> nullableLoc;
    for (auto it = attrs.rbegin(); it != attrs.rend(); ++it) {
      if (auto ann = dyn_cast<AnnotateAttr>(*it)) {
        auto loc = getRange(ann->getRange());
        if (auto ref = isUnaryAttrOf(ann, "pal-refine")) {
          ty = mk_type_refine(std::move(loc), std::move(ty),
                              std::move(ref.value()));
        } else if (auto ref = isUnaryAttrOf(ann, "pal-refine-always")) {
          ty = mk_type_refine_always(std::move(loc), std::move(ty),
                                     std::move(ref.value()));
        } else if (auto ref = isUnaryAttrOf(ann, "pal-refines")) {
          // `_refines(p)` on a flexible array member: an always-true length
          // refinement (relating the FAM length to a sibling field). Modeled
          // as `RefineAlways`; emit lifts the relation into a `pure` fact in
          // the struct predicate.
          ty = mk_type_refine_always(std::move(loc), std::move(ty),
                                     std::move(ref.value()));
        } else if (auto ref = isUnaryAttrOf(ann, "pal-refine-uninit")) {
          ty = mk_type_refine_uninit(std::move(loc), std::move(ty),
                                     std::move(ref.value()));
        } else if (ann->getAnnotation() == "pal-refine-value" &&
                   ann->args_size() == 2) {
          std::optional<unsigned> binding_ctr, pred_ctr;
          if (auto v0 = ann->args_begin()[0]->getIntegerConstantExpr(*astCtx)) {
            binding_ctr = v0->getZExtValue();
          }
          if (auto v1 = ann->args_begin()[1]->getIntegerConstantExpr(*astCtx)) {
            pred_ctr = v1->getZExtValue();
          }
          if (binding_ctr && pred_ctr) {
            ty = mk_type_refine_value(std::move(loc), std::move(ty),
                                      *binding_ctr, *pred_ctr, snippets);
          }
        } else if (ann->getAnnotation() == "pal-plain" &&
                   ann->args_size() == 0) {
          ty = mk_type_plain(std::move(loc), std::move(ty));
        } else if (ann->getAnnotation() == "pal-nullable" &&
                   ann->args_size() == 0) {
          sawNullable = true;
          if (!nullableLoc)
            nullableLoc = getRange(ann->getRange());
          ty = mk_type_nullable(std::move(loc), std::move(ty));
        } else if (ann->getAnnotation() == "pal-array" &&
                   ann->args_size() == 0) {
          ty = mk_type_array(std::move(loc), std::move(ty));
        } else if (ann->getAnnotation() == "pal-arrayptr" &&
                   ann->args_size() == 0) {
          ty = mk_type_arrayptr(std::move(loc), std::move(ty));
        } else if (ann->getAnnotation() == "pal-core-ref" &&
                   ann->args_size() == 0) {
          ty = mk_type_core_ref(std::move(loc), std::move(ty));
        }
      }
    }
    (void)sawNullable;
    (void)nullableLoc;
    return ty;
  }

  // A `_core_ref` parameter carries no ownership: `core_ref` is an
  // axiomatized address with no `pts_to`, and the predicate generated for it
  // is `emp`. Reading its const qualifier as a borrow would still give it a
  // permission implicit, and an implicit that appears only in `emp` is one no
  // call site can ever solve, so the call does not elaborate. The attribute
  // is nearly always written on a typedef -- it has to be, to land on the
  // pointee of a `void const**` -- so the typedef chain is walked.
  static bool isCoreRefQualType(QualType qt) {
    while (!qt.isNull()) {
      qt = qt.IgnoreParens();
      auto *td = qt->getAs<TypedefType>();
      if (!td)
        return false;
      for (auto *attr : td->getDecl()->getAttrs()) {
        if (auto *ann = dyn_cast<AnnotateAttr>(attr)) {
          if (ann->getAnnotation() == "pal-core-ref" && ann->args_size() == 0)
            return true;
        }
      }
      QualType next = td->getDecl()->getUnderlyingType();
      if (next.getAsOpaquePtr() == qt.getAsOpaquePtr())
        return false;
      qt = next;
    }
    return false;
  }

  bool hasCoreRefAttr(AttrVec const &attrs) {
    for (auto attr : attrs) {
      if (auto ann = dyn_cast<AnnotateAttr>(attr)) {
        if (ann->getAnnotation() == "pal-core-ref" && ann->args_size() == 0)
          return true;
      }
    }
    return false;
  }

  bool hasConsumesAttr(AttrVec const &attrs) {
    for (auto it = attrs.rbegin(); it != attrs.rend(); ++it) {
      if (auto ann = dyn_cast<AnnotateAttr>(*it)) {
        if (ann->getAnnotation() == "pal-consumes" && ann->args_size() == 0) {
          return true;
        }
      }
    }
    return false;
  }

  bool hasOutAttr(AttrVec const &attrs) {
    for (auto it = attrs.rbegin(); it != attrs.rend(); ++it) {
      if (auto ann = dyn_cast<AnnotateAttr>(*it)) {
        if (ann->getAnnotation() == "pal-out" && ann->args_size() == 0) {
          return true;
        }
      }
    }
    return false;
  }

  bool isBoolType(QualType t) {
    return t->isUnsignedIntegerType() && astCtx->getIntWidth(t) == 1;
  }

  Rc<ir::Expr> trLValue(Expr *e) {
    auto loc = getRange(e->getSourceRange());

    if (auto generic = dyn_cast<GenericSelectionExpr>(e)) {
      return trLValue(generic->getResultExpr());
    } else if (auto dre = dyn_cast<DeclRefExpr>(e)) {
      auto id = ctx.mk_ident(toStr(dre->getDecl()->getName()), loc.clone());
      return mk_lvalue_var(std::move(loc), std::move(id));
    } else if (auto p = dyn_cast<ParenExpr>(e)) {
      return trLValue(p->getSubExpr());
    } else if (auto uo = dyn_cast<UnaryOperator>(e)) {
      switch (uo->getOpcode()) {
      case UO_Deref:
        return mk_deref(std::move(loc), trRValue(uo->getSubExpr()));

      default:;
        // continue to error case
      }
    } else if (auto m = dyn_cast<MemberExpr>(e)) {
      auto *md = m->getMemberDecl();
      std::string nameStr;
      if (auto *fd = dyn_cast<FieldDecl>(md))
        nameStr = fieldNameStr(fd);
      else
        nameStr = md->getName().str();
      auto id = ctx.mk_ident(toStr(nameStr), loc.clone());
      auto base = m->isArrow() ? mk_deref(loc.clone(), trRValue(m->getBase()))
                               : trLValue(m->getBase());
      return mk_lvalue_member(std::move(loc), std::move(base), std::move(id));
    } else if (auto sub = dyn_cast<ArraySubscriptExpr>(e)) {
      return mk_index(std::move(loc), trRValue(sub->getBase()),
                      trRValue(sub->getIdx()));
    } else if (auto ic = dyn_cast<ImplicitCastExpr>(e)) {
      if (ic->getCastKind() == CK_NoOp) {
        return trLValue(ic->getSubExpr());
      }
    } else if (isa<CompoundLiteralExpr>(e)) {
      auto hoisted = hoistedCompoundLiterals.find(e->IgnoreParenImpCasts());
      if (hoisted != hoistedCompoundLiterals.end()) {
        auto tmp = ctx.mk_ident(toStr(StringRef(hoisted->second)), loc.clone());
        return mk_lvalue_var(std::move(loc), std::move(tmp));
      }
      // C11 6.5.2.5p4 makes a compound literal an lvalue, so `(T){...}.f` and
      // `&(T){...}` are both legal. The object it names is unnamed and fresh,
      // though, so nothing stored through it can be observed by any later
      // expression -- which means translating it as its own value loses
      // nothing. That is what lets a read like `((T){.f = 0}).f`, the shape a
      // named-constant macro expands to, go through.
      return trRValue(e);
    }

    reportUnsupported(e->getSourceRange(), loc,
                      "unsupported lvalue expression ", e->getStmtClassName());
    return mk_lvalue_err(std::move(loc),
                         trQualType(e->getType(), e->getSourceRange()));
  }

  // C11 6.7.9p21: elements of an aggregate that the initializer list does not
  // reach are initialized as objects with static storage duration, i.e. to
  // zero. Build that zero value for `qt`, so a partial array initializer can be
  // padded out to the array's declared length.
  Rc<ir::Expr> trZeroInit(QualType qt, SourceRange range,
                          Rc<ir::SourceInfo> loc) {
    auto desugared = qt.getDesugaredType(*astCtx);
    if (auto *cat = dyn_cast<ConstantArrayType>(desugared.getTypePtr())) {
      auto elemTy = trQualType(cat->getElementType(), range);
      auto elems = Vec<Rc<ir::Expr>>::new_();
      uint64_t n = cat->getSize().getLimitedValue();
      for (uint64_t i = 0; i < n; ++i)
        elems.push(trZeroInit(cat->getElementType(), range, loc.clone()));
      return mk_array_init(std::move(loc), std::move(elemTy), std::move(elems),
                           false);
    }
    if (auto *rec = dyn_cast<RecordType>(desugared.getTypePtr())) {
      auto *decl = rec->getDecl();
      auto it = structNames.find(recordKey(decl));
      if (it != structNames.end() &&
          decl->getTagKind() == TagTypeKind::Struct) {
        // An empty field list means "every field takes its type's default",
        // which is what emission already does for fields omitted from a
        // designated initializer.
        auto structName = ctx.mk_ident(toStr(it->second), loc.clone());
        return StructInitBuilder::new_(loc.clone(), std::move(structName))
            .build();
      }
      reportUnsupported(range, loc, "unsupported zero initializer for type ",
                        qt.getAsString().c_str());
      return mk_rvalue_err(std::move(loc), trQualType(qt, range));
    }
    if (desugared->isScalarType()) {
      // Covers integers, enums, floating point, booleans and pointers; a null
      // pointer constant is a zero literal of the pointer's type, which is how
      // `isNull` casts are already translated.
      return mk_int_lit(std::move(loc), mk_bigint("0"_rs),
                        trQualType(qt, range));
    }
    reportUnsupported(range, loc, "unsupported zero initializer for type ",
                      qt.getAsString().c_str());
    return mk_rvalue_err(std::move(loc), trQualType(qt, range));
  }

  Rc<ir::Expr> trInitList(InitListExpr *init, SourceRange range,
                          Rc<ir::SourceInfo> loc) {
    auto qt = init->getType().getDesugaredType(*astCtx);
    // Handle array initializer lists
    if (auto *cat = dyn_cast<ConstantArrayType>(qt.getTypePtr())) {
      auto elemTy = trQualType(cat->getElementType(), range);
      auto elems = Vec<Rc<ir::Expr>>::new_();
      unsigned given = init->getNumInits();
      for (unsigned i = 0; i < given; ++i) {
        elems.push(trRValue(init->getInit(i)));
      }
      // An initializer list may be shorter than the array; the array's length
      // comes from its type, not from the list. Pad the tail with the filler
      // Clang recorded, or with zeroes when that filler is the implicit one.
      // Without this the array literal takes the length of the list and the
      // result no longer has the array's type.
      uint64_t declared = cat->getSize().getLimitedValue();
      Expr *filler = init->getArrayFiller();
      for (uint64_t i = given; i < declared; ++i) {
        if (filler && !isa<ImplicitValueInitExpr>(filler))
          elems.push(trRValue(filler));
        else
          elems.push(trZeroInit(cat->getElementType(), range, getRange(range)));
      }
      return mk_array_init(std::move(loc), std::move(elemTy), std::move(elems),
                           false);
    }
    // A braced initializer for a scalar object: C permits `int x = {0}` and
    // `T x = {}`. Code can reach it through typedefs whose definition is a
    // struct on one platform and a plain integer on another. The list holds at
    // most one element, and it initializes the object directly.
    if (qt->isScalarType()) {
      if (init->getNumInits() == 0) {
        return trZeroInit(init->getType(), range, std::move(loc));
      }
      if (init->getNumInits() == 1) {
        return trRValue(init->getInit(0));
      }
      reportUnsupported(range, loc,
                        "initializer list for a scalar type has more than one "
                        "element",
                        "");
      return mk_rvalue_err(std::move(loc), trQualType(init->getType(), range));
    }
    auto *rec = dyn_cast<RecordType>(qt.getTypePtr());
    if (!rec) {
      reportUnsupported(range, loc,
                        "unsupported initializer list for non-record type", "");
      return mk_rvalue_err(std::move(loc), trQualType(init->getType(), range));
    }
    auto *decl = rec->getDecl();
    auto it = structNames.find(recordKey(decl));
    if (it == structNames.end()) {
      reportUnsupported(range, loc, "unknown record in initializer list", "");
      return mk_rvalue_err(std::move(loc), trQualType(init->getType(), range));
    }

    if (decl->getTagKind() == TagTypeKind::Union) {
      if (init->getNumInits() != 1) {
        reportUnsupported(range, loc,
                          "union initializer must have exactly one field", "");
        return mk_rvalue_err(std::move(loc),
                             trQualType(init->getType(), range));
      }
      auto unionName = ctx.mk_ident(toStr(it->second), loc.clone());
      auto *fieldInit = init->getInit(0);
      auto *field = init->getInitializedFieldInUnion();
      auto floc = getRange(fieldInit->getSourceRange());
      auto fieldName =
          ctx.mk_ident(toStr(fieldNameStr(field)), std::move(floc));
      return mk_union_init(std::move(loc), std::move(unionName),
                           std::move(fieldName), trRValue(fieldInit));
    }

    if (decl->getTagKind() != TagTypeKind::Struct) {
      reportUnsupported(range, loc,
                        "unsupported initializer list for non-struct type", "");
      return mk_rvalue_err(std::move(loc), trQualType(init->getType(), range));
    }
    auto structName = ctx.mk_ident(toStr(it->second), loc.clone());
    auto builder = StructInitBuilder::new_(loc.clone(), std::move(structName));
    for (unsigned i = 0; i < init->getNumInits(); ++i) {
      auto *fieldInit = init->getInit(i);
      auto *field = *std::next(decl->field_begin(), i);
      // A flexible array member cannot be initialized in a C compound literal;
      // Clang supplies an implicit (empty) initializer for it. Skip it here so
      // the emitter fills it with its default (a length-0 array).
      if (field->getType()->isIncompleteArrayType())
        continue;
      // A field omitted from a designated initializer (e.g. `{ .initialized =
      // 42 }` leaving other fields unset) is represented by Clang's semantic
      // InitListExpr as an ImplicitValueInitExpr placeholder. Per C11
      // 6.7.9p21, such fields are implicitly zero-initialized, the same as an
      // object of static storage duration. Skip translating the placeholder
      // itself (trRValue has no case for it, so it would otherwise become an
      // error/admit()) and let the emitter fill it with its type's zero/null
      // default, exactly as it does for a field absent entirely from the
      // initializer list.
      if (isa<ImplicitValueInitExpr>(fieldInit))
        continue;
      auto floc = getRange(fieldInit->getSourceRange());
      auto fieldName =
          ctx.mk_ident(toStr(fieldNameStr(field)), std::move(floc));
      builder.field(std::move(fieldName), trRValue(fieldInit));
    }
    return builder.build();
  }

  // Recognize a `sizeof` operand in an allocation size expression. Both
  // spellings are accepted: a type operand (`sizeof(T)`) and an expression
  // operand (`sizeof(*p)`, `sizeof *p`), the latter being the common C idiom
  // `p = malloc(sizeof(*p))`. The operand type is read off with
  // `getTypeOfArgument()`, which covers both. Returns nullptr if `e` is not a
  // `sizeof`.
  static const UnaryExprOrTypeTraitExpr *asSizeof(Expr *e) {
    auto *s = dyn_cast<UnaryExprOrTypeTraitExpr>(e->IgnoreParenImpCasts());
    if (!s || s->getKind() != UETT_SizeOf)
      return nullptr;
    // A VLA operand has no static size, so it does not denote an allocation
    // unit; an incomplete operand type cannot be translated either.
    auto argTy = s->getTypeOfArgument();
    if (argTy->isIncompleteType() || argTy->isDependentType() ||
        argTy->isVariableArrayType())
      return nullptr;
    return s;
  }

  // For a flexible-array-member allocation's trailing size term, return the
  // count operand `n` of `n * sizeof(elem)` or `sizeof(elem) * n` (the
  // non-sizeof multiplicand). Returns nullptr if the term is not a recognized
  // product with a sizeof factor.
  static Expr *flexArrayCountSide(Expr *e) {
    auto *mul = dyn_cast<BinaryOperator>(e->IgnoreParenImpCasts());
    if (!mul || mul->getOpcode() != BO_Mul)
      return nullptr;
    if (asSizeof(mul->getLHS()))
      return mul->getRHS();
    if (asSizeof(mul->getRHS()))
      return mul->getLHS();
    return nullptr;
  }

  // Whether an ignored variadic argument can be dropped without losing a
  // proof obligation: evaluating it must have no side effects, read no memory
  // other than non-volatile locals, and have no undefined behavior.
  bool canOmitVariadicArgument(Expr *e) {
    if (e->HasSideEffects(*astCtx))
      return false;
    return isInertVariadicOperand(e);
  }

  bool isInertVariadicOperand(Expr *e) {
    e = e->IgnoreParenImpCasts();
    if (isa<IntegerLiteral, CharacterLiteral, FloatingLiteral, StringLiteral>(
            e))
      return true;
    if (e->getType()->isIntegerType() && e->isIntegerConstantExpr(*astCtx))
      return true;
    // A conversion between integer types is never undefined.
    if (auto *cast = dyn_cast<ExplicitCastExpr>(e);
        cast && cast->getType()->isIntegerType() &&
        cast->getSubExpr()->getType()->isIntegerType())
      return isInertVariadicOperand(cast->getSubExpr());
    if (auto *op = dyn_cast<UnaryOperator>(e);
        op && op->getOpcode() == UO_Not && op->getType()->isIntegerType())
      return isInertVariadicOperand(op->getSubExpr());
    if (auto *bin = dyn_cast<BinaryOperator>(e)) {
      auto ty = bin->getType();
      bool operands = isInertVariadicOperand(bin->getLHS()) &&
                      isInertVariadicOperand(bin->getRHS());
      switch (bin->getOpcode()) {
      case BO_And:
      case BO_Or:
      case BO_Xor:
        return ty->isIntegerType() && operands;
      // Unsigned arithmetic wraps. Division is excluded: a zero divisor is
      // undefined whatever the type.
      case BO_Add:
      case BO_Sub:
      case BO_Mul:
        return ty->isUnsignedIntegerType() && operands;
      case BO_Shl:
      case BO_Shr: {
        if (!ty->isUnsignedIntegerType() || !operands)
          return false;
        auto amount = bin->getRHS()->getIntegerConstantExpr(*astCtx);
        return amount && amount->isNonNegative() &&
               amount->getZExtValue() < astCtx->getTypeSize(ty);
      }
      default:
        return false;
      }
    }
    bool address = false;
    if (auto *op = dyn_cast<UnaryOperator>(e);
        op && op->getOpcode() == UO_AddrOf) {
      address = true;
      e = op->getSubExpr()->IgnoreParens();
    }
    auto *ref = dyn_cast<DeclRefExpr>(e);
    auto *var = ref ? dyn_cast<VarDecl>(ref->getDecl()) : nullptr;
    if (!var || (!isa<ParmVarDecl>(var) && !var->hasLocalStorage()))
      return false;
    auto ty = var->getType();
    // A local array passed to `...` has decayed to its address.
    return !ty.isVolatileQualified() && !ty->isAtomicType() &&
           (address || ty->isScalarType() || ty->isArrayType());
  }

  Rc<ir::Expr> trRValue(Expr *e) {
    auto loc = getRange(e->getSourceRange());

    if (auto generic = dyn_cast<GenericSelectionExpr>(e)) {
      return trRValue(generic->getResultExpr());
    }

    if (auto ic = dyn_cast<CastExpr>(e)) {
      switch (ic->getCastKind()) {
      case CK_LValueToRValue:
        if (dyn_cast<CompoundLiteralExpr>(
                ic->getSubExpr()->IgnoreParenImpCasts())) {
          return trRValue(ic->getSubExpr());
        }
        return mk_rvalue_lvalue(std::move(loc), trLValue(ic->getSubExpr()));

      case CK_NoOp:
        return trRValue(ic->getSubExpr());
      case CK_FunctionToPointerDecay:
        // `add` used as a value decays to a function pointer; translate the
        // underlying function reference directly (the DeclRefExpr arm below
        // produces a FnRef for a FunctionDecl).
        return trRValue(ic->getSubExpr());
      case CK_ArrayToPointerDecay: {
        auto *subExpr = ic->getSubExpr()->IgnoreParenImpCasts();
        if (dyn_cast<StringLiteral>(subExpr) ||
            dyn_cast<CompoundLiteralExpr>(subExpr)) {
          return trRValue(ic->getSubExpr());
        }
        return mk_rvalue_lvalue(std::move(loc), trLValue(ic->getSubExpr()));
      }
      case CK_PointerToIntegral: {
        auto *target = ic->getType()->getAs<BuiltinType>();
        auto source = ic->getSubExpr()->getType();
        if (target &&
            (target->getKind() == BuiltinType::Long ||
             target->getKind() == BuiltinType::ULong) &&
            source->isPointerType() &&
            !source->getPointeeType()->isFunctionType()) {
          return mk_rvalue_cast(std::move(loc), trRValue(ic->getSubExpr()),
                                trQualType(ic->getType(), e->getSourceRange()));
        }
        reportUnsupported(e->getSourceRange(), loc,
                          "unsupported pointer-to-integer cast",
                          "only object or void pointers to long or unsigned "
                          "long are supported");
        return mk_rvalue_err(std::move(loc),
                             trQualType(e->getType(), e->getSourceRange()));
      }
      case CK_IntegralCast:
      case CK_IntegralToBoolean:
      case CK_PointerToBoolean:
      case CK_FloatingCast:
      case CK_IntegralToFloating:
      case CK_FloatingToIntegral:
      case CK_FloatingToBoolean:
        return mk_rvalue_cast(std::move(loc), trRValue(ic->getSubExpr()),
                              trQualType(ic->getType(), ic->getSourceRange()));

      // Integer -> pointer. Lowered to an ordinary IR cast; the emitter
      // routes it through `core_ref`, PAL's raw-pointer model, and the result
      // carries no ownership.
      //
      // `isNull` is tested first, because a null pointer constant that has
      // already picked up an integral cast -- `(T *)(uintptr_t)0` -- must stay
      // a null pointer rather than become an opaque address.
      //
      // This used to fall through to "unsupported rvalue expression
      // CStyleCastExpr", which is much worse than it sounds: PAL then emits
      // `(admit())` for the whole enclosing expression, so the *rest* of the
      // function's obligations go unchecked too.
      case CK_IntegralToPointer:
        if (isNull(ic)) {
          return mk_int_lit(std::move(loc), mk_bigint("0"_rs),
                            trQualType(ic->getType(), ic->getSourceRange()));
        }
        return mk_rvalue_cast(std::move(loc), trRValue(ic->getSubExpr()),
                              trQualType(ic->getType(), ic->getSourceRange()));

      default:;
        if (isNull(ic)) {
          return mk_int_lit(std::move(loc), mk_bigint("0"_rs),
                            trQualType(ic->getType(), ic->getSourceRange()));
        }

        // Detect (T*) malloc(sizeof(T)) and (T*) malloc(sizeof(T) * n)
        if (auto *call =
                dyn_cast<CallExpr>(ic->getSubExpr()->IgnoreParenImpCasts())) {
          if (auto *callee = call->getDirectCallee()) {
            if (callee->getName() == "malloc" && call->getNumArgs() == 1) {
              auto *arg = call->getArg(0)->IgnoreParenImpCasts();
              // Single element: malloc(sizeof(T)) or malloc(sizeof(*p))
              if (auto *sizeofExpr = asSizeof(arg)) {
                auto allocTy = trQualType(sizeofExpr->getTypeOfArgument(),
                                          sizeofExpr->getSourceRange());
                return mk_malloc(std::move(loc), std::move(allocTy));
              }
              // Flexible array member allocation:
              //   malloc(sizeof(struct foo) + n * sizeof(elem))
              // The trailing-array term is runtime sizing that Pulse models via
              // the inline ghost `array_spec`; translate identically to a plain
              // struct malloc of the header type (dropping the array term).
              if (auto *binOp = dyn_cast<BinaryOperator>(arg)) {
                if (binOp->getOpcode() == BO_Add) {
                  auto structSizeofSide =
                      [&](Expr *e) -> const UnaryExprOrTypeTraitExpr * {
                    auto *s = asSizeof(e);
                    if (s && s->getTypeOfArgument()->isRecordType())
                      return s;
                    return nullptr;
                  };
                  const UnaryExprOrTypeTraitExpr *structSide =
                      structSizeofSide(binOp->getLHS());
                  Expr *arrayTerm = binOp->getRHS();
                  if (!structSide) {
                    structSide = structSizeofSide(binOp->getRHS());
                    arrayTerm = binOp->getLHS();
                  }
                  if (structSide) {
                    auto allocTy = trQualType(structSide->getTypeOfArgument(),
                                              structSide->getSourceRange());
                    // Extract `n` from the trailing array term `n *
                    // sizeof(elem)` or `sizeof(elem) * n`, so the flexible tail
                    // is sized `n`.
                    if (Expr *countSide = flexArrayCountSide(arrayTerm)) {
                      auto countExpr = trRValue(countSide);
                      return mk_malloc_flex(std::move(loc), std::move(allocTy),
                                            std::move(countExpr));
                    }
                    // Unrecognized array term: fall back to an empty flexible
                    // tail (plain struct malloc).
                    return mk_malloc(std::move(loc), std::move(allocTy));
                  }
                }
              }
              // Array: malloc(sizeof(T) * n) or malloc(n * sizeof(T))
              if (auto *binOp = dyn_cast<BinaryOperator>(arg)) {
                if (binOp->getOpcode() == BO_Mul) {
                  const UnaryExprOrTypeTraitExpr *sizeofSide = nullptr;
                  Expr *countSide = nullptr;
                  if (auto *s = asSizeof(binOp->getLHS())) {
                    sizeofSide = s;
                    countSide = binOp->getRHS();
                  } else if (auto *s = asSizeof(binOp->getRHS())) {
                    sizeofSide = s;
                    countSide = binOp->getLHS();
                  }
                  if (sizeofSide && countSide) {
                    auto allocTy = trQualType(sizeofSide->getTypeOfArgument(),
                                              sizeofSide->getSourceRange());
                    auto countExpr = trRValue(countSide);
                    return mk_malloc_array(std::move(loc), std::move(allocTy),
                                           std::move(countExpr));
                  }
                }
              }
            }
            // Detect calloc(n, sizeof(T)) and calloc(1, n * sizeof(T))
            if (callee->getName() == "calloc" && call->getNumArgs() == 2) {
              auto *countArg = call->getArg(0)->IgnoreParenImpCasts();
              auto *sizeArg = call->getArg(1)->IgnoreParenImpCasts();
              if (auto *sizeofExpr = asSizeof(sizeArg)) {
                auto allocTy = trQualType(sizeofExpr->getTypeOfArgument(),
                                          sizeofExpr->getSourceRange());
                // calloc(1, sizeof(T)) → single ref
                if (auto *intLit = dyn_cast<IntegerLiteral>(countArg)) {
                  if (intLit->getValue() == 1) {
                    return mk_calloc(std::move(loc), std::move(allocTy));
                  }
                }
                // calloc(n, sizeof(T)) → array
                auto countExpr = trRValue(countArg);
                return mk_calloc_array(std::move(loc), std::move(allocTy),
                                       std::move(countExpr));
              }
              // Flexible array member allocation:
              //   calloc(1, sizeof(struct foo) + n * sizeof(elem))
              // Zeroing counterpart of the malloc FAM idiom above (mirrors
              // MsQuic's `QuicCidNewNullSource`, which allocates the sized
              // block and zeroes it). Translate to a single zeroed struct
              // allocation of the header type, dropping the runtime array term;
              // the zeroed struct's flexible array starts empty (length 0).
              if (auto *intLit = dyn_cast<IntegerLiteral>(countArg)) {
                if (intLit->getValue() == 1) {
                  if (auto *binOp = dyn_cast<BinaryOperator>(sizeArg)) {
                    if (binOp->getOpcode() == BO_Add) {
                      auto structSizeofSide =
                          [&](Expr *e) -> const UnaryExprOrTypeTraitExpr * {
                        auto *s = asSizeof(e);
                        if (s && s->getTypeOfArgument()->isRecordType())
                          return s;
                        return nullptr;
                      };
                      const UnaryExprOrTypeTraitExpr *structSide =
                          structSizeofSide(binOp->getLHS());
                      Expr *arrayTerm = binOp->getRHS();
                      if (!structSide) {
                        structSide = structSizeofSide(binOp->getRHS());
                        arrayTerm = binOp->getLHS();
                      }
                      if (structSide) {
                        auto allocTy =
                            trQualType(structSide->getTypeOfArgument(),
                                       structSide->getSourceRange());
                        // Extract `n` from the trailing array term so the
                        // zeroed flexible tail is sized `n`.
                        if (Expr *countSide = flexArrayCountSide(arrayTerm)) {
                          auto countExpr = trRValue(countSide);
                          return mk_calloc_flex(std::move(loc),
                                                std::move(allocTy),
                                                std::move(countExpr));
                        }
                        // Unrecognized array term: fall back to an empty
                        // flexible tail (plain zeroed struct calloc).
                        return mk_calloc(std::move(loc), std::move(allocTy));
                      }
                    }
                  }
                }
              }
              // calloc(1, n * sizeof(T)) or calloc(1, sizeof(T) * n) → array
              // (e.g. CXPLAT_ALLOC_NONPAGED(n * sizeof(T), ...) → calloc(1,
              // ...))
              if (auto *intLit = dyn_cast<IntegerLiteral>(countArg)) {
                if (intLit->getValue() == 1) {
                  if (auto *binOp = dyn_cast<BinaryOperator>(sizeArg)) {
                    if (binOp->getOpcode() == BO_Mul) {
                      const UnaryExprOrTypeTraitExpr *sizeofSide = nullptr;
                      Expr *countSide = nullptr;
                      if (auto *s = asSizeof(binOp->getLHS())) {
                        sizeofSide = s;
                        countSide = binOp->getRHS();
                      } else if (auto *s = asSizeof(binOp->getRHS())) {
                        sizeofSide = s;
                        countSide = binOp->getLHS();
                      }
                      if (sizeofSide && countSide) {
                        auto allocTy =
                            trQualType(sizeofSide->getTypeOfArgument(),
                                       sizeofSide->getSourceRange());
                        auto countExpr = trRValue(countSide);
                        return mk_calloc_array(std::move(loc),
                                               std::move(allocTy),
                                               std::move(countExpr));
                      }
                    }
                  }
                }
              }
            }
          }
        }

        // Detect the standard `container_of` idiom, i.e.
        //   (T *)((char *)ptr - offsetof(T, field))
        // as produced by the `_container_of` macro, Linux's `container_of`,
        // MsQuic's `CXPLAT_CONTAINING_RECORD`, etc. The outer `(T *)` cast is a
        // CK_BitCast off a char-pointer subtraction whose right operand is an
        // `OffsetOfExpr` with a single field component. Recover the field
        // pointer, enclosing struct, and field name and build a container
        // projection node. Matching the idiom directly means user code needs no
        // PAL-specific spelling of `container_of`.
        if (ic->getCastKind() == CK_BitCast) {
          if (auto *sub = dyn_cast<BinaryOperator>(
                  ic->getSubExpr()->IgnoreParenImpCasts());
              sub && sub->getOpcode() == BO_Sub) {
            if (auto *ooe = dyn_cast<OffsetOfExpr>(
                    sub->getRHS()->IgnoreParenImpCasts());
                ooe && ooe->getNumComponents() == 1 &&
                ooe->getComponent(0).getKind() == OffsetOfNode::Field) {
              if (auto *field = ooe->getComponent(0).getField()) {
                auto *recordDecl = field->getParent();
                auto structTy = trQualType(astCtx->getRecordType(recordDecl),
                                           ooe->getSourceRange());
                auto fieldId = ctx.mk_ident(toStr(fieldNameStr(field)),
                                            getRange(ooe->getSourceRange()));
                // Strip the `(char *)` cast off the left operand to recover the
                // original field pointer rvalue.
                auto *ptrExpr = sub->getLHS()->IgnoreParenImpCasts();
                if (auto *ptrCast = dyn_cast<CastExpr>(ptrExpr)) {
                  ptrExpr = ptrCast->getSubExpr();
                }
                return mk_container_of(std::move(loc), trRValue(ptrExpr),
                                       std::move(structTy), std::move(fieldId));
              }
            }
          }
        }

        // Detect a cast between a struct pointer and a pointer to one of its
        // transitively-initial members, in either direction. C guarantees a
        // struct pointer round-trips with a pointer to its initial member
        // (C17 6.7.2.1p17): "A pointer to a structure object, suitably
        // converted, points to its initial member ... and vice versa. There
        // may be unnamed padding within a structure object, but not at its
        // beginning." Applying this recursively, a struct pointer is
        // interconvertible with a pointer to the first field of the first
        // field of ... its first field, arbitrarily deep. We recover this
        // chain of initial members and lower a `field -> struct` cast to a
        // nest of per-field container projections (the node `_container_of`
        // produces) and a `struct -> field` cast to a nest of member accesses
        // `&base->f0.f1...`. Both reuse machinery PAL already emits, so
        // nothing downstream changes. A chain of length one reproduces the
        // single-hop first-field cast exactly.
        if (ic->getCastKind() == CK_BitCast) {
          QualType dstTy = ic->getType();
          QualType srcTy = ic->getSubExpr()->getType();
          if (dstTy->isPointerType() && srcTy->isPointerType()) {
            QualType dstPointee = dstTy->getPointeeType();
            QualType srcPointee = srcTy->getPointeeType();

            auto sameType = [&](QualType a, QualType b) {
              return astCtx->hasSameUnqualifiedType(a, b);
            };
            // The non-bitfield first field of a struct pointee, or null.
            auto firstField = [&](QualType pointee) -> FieldDecl * {
              auto *rt = pointee->getAs<RecordType>();
              if (!rt)
                return nullptr;
              auto *rd = rt->getDecl()->getDefinition();
              if (!rd || rd->getTagKind() != TagTypeKind::Struct)
                return nullptr;
              auto it = rd->field_begin();
              if (it == rd->field_end() || it->isBitField())
                return nullptr;
              return *it;
            };
            // The chain of initial members descending from `from` until one
            // has type `target`, e.g. [outer::in, inner::x] for `outer` down
            // to `int`. Empty if `target` is not a transitively-initial member
            // of `from` (a non-struct/bitfield is reached first, or `from`
            // already equals `target`). Depth-capped as a safety net against
            // pathological (e.g. recursive) type graphs.
            auto firstFieldChain =
                [&](QualType from,
                    QualType target) -> std::vector<FieldDecl *> {
              std::vector<FieldDecl *> chain;
              QualType cur = from;
              for (int depth = 0; depth < 32; ++depth) {
                if (sameType(cur, target))
                  return chain;
                FieldDecl *f = firstField(cur);
                if (!f)
                  return {};
                chain.push_back(f);
                if (sameType(f->getType(), target))
                  return chain;
                cur = f->getType();
              }
              return {};
            };

            // (struct S *)p  where p : F *, F transitively-initial member of S.
            auto revChain = firstFieldChain(dstPointee, srcPointee);
            // (F *)s  where s : struct S *, F transitively-initial member of S.
            auto fwdChain = firstFieldChain(srcPointee, dstPointee);

            // At most one direction can match: both would require a cycle in
            // the by-value initial-member graph, impossible as sizes strictly
            // decrease. The `.empty()` guards are defensive.
            if (!revChain.empty() && fwdChain.empty()) {
              // Nest container projections innermost-first: the deepest field
              // (whose parent owns `p`) is applied first.
              auto expr = trRValue(ic->getSubExpr());
              for (auto it = revChain.rbegin(); it != revChain.rend(); ++it) {
                FieldDecl *f = *it;
                auto structTy =
                    trQualType(astCtx->getRecordType(f->getParent()),
                               ic->getSourceRange());
                auto fieldId = ctx.mk_ident(toStr(fieldNameStr(f)),
                                            getRange(ic->getSourceRange()));
                expr = mk_container_of(loc.clone(), std::move(expr),
                                       std::move(structTy), std::move(fieldId));
              }
              return expr;
            }

            if (!fwdChain.empty() && revChain.empty()) {
              // Nest member accesses outermost-first: &(*s).f0.f1...
              auto base = mk_deref(loc.clone(), trRValue(ic->getSubExpr()));
              for (FieldDecl *f : fwdChain) {
                auto fieldId = ctx.mk_ident(toStr(fieldNameStr(f)),
                                            getRange(ic->getSourceRange()));
                base = mk_lvalue_member(loc.clone(), std::move(base),
                                        std::move(fieldId));
              }
              return mk_rvalue_ref(std::move(loc), std::move(base));
            }
          }
        }

        // BitCast (e.g., T* → void*): pass through after malloc/calloc
        // detection. F* functions like memcpy are type-polymorphic.
        if (ic->getCastKind() == CK_BitCast) {
          return trRValue(ic->getSubExpr());
        }

        // continue to error case
      }
    } else if (auto p = dyn_cast<ParenExpr>(e)) {
      return trRValue(p->getSubExpr());
    } else if (auto il = dyn_cast<IntegerLiteral>(e)) {
      if (isBoolType(il->getType())) {
        return mk_bool_lit(std::move(loc), !il->getValue().isZero());
      } else {
        auto ty = trQualType(il->getType(), il->getSourceRange());
        return mk_int_lit(std::move(loc), toBigInt(il->getValue()),
                          std::move(ty));
      }
    } else if (auto fl = dyn_cast<FloatingLiteral>(e)) {
      SmallString<32> value;
      fl->getValue().toString(value);
      auto ty = trQualType(fl->getType(), fl->getSourceRange());
      return mk_float_lit(std::move(loc),
                          ctx.intern_str(toStr(StringRef(value))),
                          std::move(ty));
    } else if (auto cl = dyn_cast<CharacterLiteral>(e)) {
      auto ty = trQualType(cl->getType(), cl->getSourceRange());
      return mk_int_lit(std::move(loc),
                        mk_bigint(toStr(std::to_string(cl->getValue()))),
                        std::move(ty));
    } else if (auto sl = dyn_cast<StringLiteral>(e)) {
      if (sl->getKind() != StringLiteralKind::Ordinary ||
          sl->getCharByteWidth() != 1) {
        reportUnsupported(e->getSourceRange(), loc,
                          "unsupported non-narrow string literal", "");
        return mk_rvalue_err(std::move(loc),
                             trQualType(e->getType(), e->getSourceRange()));
      }
      auto charIsSigned = astCtx->getLangOpts().CharIsSigned;
      auto charWidth = astCtx->getTargetInfo().getCharWidth();
      auto mkCharTy = [&]() {
        return mk_int_type(loc.clone(), charIsSigned, charWidth);
      };
      auto mkCharLit = [&](unsigned char ch) {
        long long value = ch;
        if (charIsSigned && charWidth > 0 &&
            value >= (1LL << (charWidth - 1))) {
          value -= 1LL << charWidth;
        }
        return mk_int_lit(loc.clone(), mk_bigint(toStr(std::to_string(value))),
                          mkCharTy());
      };
      auto elems = Vec<Rc<ir::Expr>>::new_();
      for (unsigned char ch : sl->getBytes()) {
        elems.push(mkCharLit(ch));
      }
      elems.push(mkCharLit(0));
      auto elemTy = mkCharTy();
      return mk_array_init(std::move(loc), std::move(elemTy), std::move(elems),
                           true);
    } else if (auto uo = dyn_cast<UnaryOperator>(e)) {
      switch (uo->getOpcode()) {
      case UO_AddrOf:
        // `&func` where `func` is a function: produce a function reference
        // rather than address-of an lvalue. `&func` and bare `func` (decay)
        // both denote the same function-pointer value.
        if (auto *dre = dyn_cast<DeclRefExpr>(
                uo->getSubExpr()->IgnoreParenImpCasts())) {
          if (auto *fd = dyn_cast<FunctionDecl>(dre->getDecl())) {
            auto id = ctx.mk_ident(toStr(fd->getName()), loc.clone());
            return mk_rvalue_fnref(std::move(loc), std::move(id));
          }
        }
        return mk_rvalue_ref(std::move(loc), trLValue(uo->getSubExpr()));

      case UO_LNot:
        return mk_rvalue_unop(std::move(loc), ir::UnOp::Not(),
                              trRValue(uo->getSubExpr()));

      case UO_Not:
        return mk_rvalue_unop(std::move(loc), ir::UnOp::BitNot(),
                              trRValue(uo->getSubExpr()));

      case UO_Plus:
        return trRValue(uo->getSubExpr());

      case UO_Minus:
        return mk_rvalue_unop(std::move(loc), ir::UnOp::Neg(),
                              trRValue(uo->getSubExpr()));

      case UO_PreInc:
        return mk_pre_incr(std::move(loc), trLValue(uo->getSubExpr()));
      case UO_PostInc:
        return mk_post_incr(std::move(loc), trLValue(uo->getSubExpr()));
      case UO_PreDec:
        return mk_pre_decr(std::move(loc), trLValue(uo->getSubExpr()));
      case UO_PostDec:
        return mk_post_decr(std::move(loc), trLValue(uo->getSubExpr()));

      default:;
        // continue to error case
      }
    } else if (auto *bo = dyn_cast<BinaryOperator>(e)) {
      // `a && b` and `a || b` evaluate `b` only if `a` does not decide the
      // answer, so a statement expression in `b` must not hoist out.
      auto shortCircuit = [&](BinaryOperator *op_e, auto &l, ir::BinOp op) {
        auto lhs = trRValue(op_e->getLHS());
        NoHoist noHoist(&hoistTarget);
        return mk_rvalue_binop(std::move(l), std::move(op), std::move(lhs),
                               trRValue(op_e->getRHS()));
      };
      auto m = [&](ir::BinOp op) {
        return mk_rvalue_binop(std::move(loc), std::move(op),
                               trRValue(bo->getLHS()), trRValue(bo->getRHS()));
      };
      switch (bo->getOpcode()) {
      case clang::BO_Add:
        return m(ir::BinOp::Add());
      case clang::BO_Sub:
        return m(ir::BinOp::Sub());
      case clang::BO_Mul:
        return m(ir::BinOp::Mul());
      case clang::BO_Div:
        return m(ir::BinOp::Div());
      case clang::BO_Rem:
        return m(ir::BinOp::Mod());
      case clang::BO_LAnd:
        return shortCircuit(bo, loc, ir::BinOp::LogAnd());
      case clang::BO_EQ:
        return m(ir::BinOp::Eq());
      case clang::BO_NE: {
        auto loc2 = loc.clone();
        return mk_rvalue_unop(std::move(loc2), ir::UnOp::Not(),
                              m(ir::BinOp::Eq()));
      }
      case clang::BO_LE:
        return m(ir::BinOp::LEq());
      case clang::BO_LT:
        return m(ir::BinOp::Lt());
      case clang::BO_GT:
        return mk_rvalue_binop(std::move(loc), ir::BinOp::Lt(),
                               trRValue(bo->getRHS()), trRValue(bo->getLHS()));
      case clang::BO_GE:
        return mk_rvalue_binop(std::move(loc), ir::BinOp::LEq(),
                               trRValue(bo->getRHS()), trRValue(bo->getLHS()));
      case clang::BO_LOr:
        return shortCircuit(bo, loc, ir::BinOp::LogOr());
      case clang::BO_And:
        return m(ir::BinOp::BitAnd());
      case clang::BO_Or:
        return m(ir::BinOp::BitOr());
      case clang::BO_Xor:
        return m(ir::BinOp::BitXor());
      case clang::BO_Shl:
        return m(ir::BinOp::Shl());
      case clang::BO_Shr:
        return m(ir::BinOp::Shr());

      case clang::BO_Assign:
        return mk_assign_expr(std::move(loc), trLValue(bo->getLHS()),
                              trRValue(bo->getRHS()));

      case clang::BO_AddAssign:
      case clang::BO_SubAssign:
      case clang::BO_MulAssign:
      case clang::BO_DivAssign:
      case clang::BO_RemAssign:
      case clang::BO_ShlAssign:
      case clang::BO_ShrAssign:
      case clang::BO_AndAssign:
      case clang::BO_OrAssign:
      case clang::BO_XorAssign: {
        auto getBinOp = [](BinaryOperatorKind ok) -> ir::BinOp {
          switch (ok) {
          case BO_AddAssign:
            return ir::BinOp::Add();
          case BO_SubAssign:
            return ir::BinOp::Sub();
          case BO_MulAssign:
            return ir::BinOp::Mul();
          case BO_DivAssign:
            return ir::BinOp::Div();
          case BO_RemAssign:
            return ir::BinOp::Mod();
          case BO_ShlAssign:
            return ir::BinOp::Shl();
          case BO_ShrAssign:
            return ir::BinOp::Shr();
          case BO_AndAssign:
            return ir::BinOp::BitAnd();
          case BO_OrAssign:
            return ir::BinOp::BitOr();
          case BO_XorAssign:
            return ir::BinOp::BitXor();
          default:
            __builtin_unreachable();
          }
        };
        auto op = getBinOp(bo->getOpcode());
        auto lhsRval = mk_rvalue_lvalue(loc.clone(), trLValue(bo->getLHS()));
        auto rhs = trRValue(bo->getRHS());
        auto result = mk_rvalue_binop(loc.clone(), std::move(op),
                                      std::move(lhsRval), std::move(rhs));
        return mk_assign_expr(std::move(loc), trLValue(bo->getLHS()),
                              std::move(result));
      }

      case clang::BO_Comma: {
        // The comma operator in rvalue position.
        //
        // `(a, b)` evaluates `a`, discards it, then yields `b`.  PAL's
        // expression IR has nowhere to put `a`: there is no statement
        // sequencing inside an rvalue, and hoisting it out would move it
        // across the surrounding expression's other operands, which C's
        // sequencing rules do not permit in general.
        //
        // So this is translated only when `a` cannot be observed at all --
        // when Clang can tell us it has no side effects.  Then `(a, b)` and
        // `b` are the same program and the arm is a pure simplification.
        //
        // This is not a corner case.  Generated RPC-stub macros can all be
        // of the form
        //
        //   #define f(...) ((void)sizeof(f(__VA_ARGS__)),
        //   (uint64_t)invoke_N(...))
        //
        // where the left operand is a compile-time prototype check whose
        // operand is unevaluated.  Refusing it made every such call site an
        // `admit()`, discarding the surrounding obligations along with
        // it.
        //
        // A left operand that *does* have side effects still reaches the
        // unsupported diagnostic below, deliberately: silently dropping it
        // would change the program.
        if (!bo->getLHS()->HasSideEffects(*astCtx)) {
          return trRValue(bo->getRHS());
        }
        break;
      }

      default:;
        // continue to error case
      }
    } else if (auto *c = dyn_cast<CallExpr>(e)) {
      if (auto fd = c->getDirectCallee()) {
        // Byte-reversal builtins. `Pulse.Lib.C.UInt64.bswap64` is a
        // definition in terms of shifts and masks, not an axiom, so this
        // assumes nothing -- a caller that needs to reason about the result
        // can unfold it. Code reaches this through big-endian hardware
        // descriptors.
        if (fd->getName() == "__builtin_bswap64" && c->getNumArgs() == 1) {
          auto prim =
              ctx.mk_ident(toStr(StringRef("__pal_bswap64")), loc.clone());
          auto primArgs = Vec<Rc<ir::Expr>>::new_();
          primArgs.push(trRValue(c->getArg(0)));
          return mk_rvalue_fncall(std::move(loc), std::move(prim),
                                  std::move(primArgs));
        }
        // GCC/Clang builtins that carry no program meaning.
        //
        // Real code reaches these through likely()/unlikely() and assert();
        // left alone they produce a large share of translation errors, none
        // of which reflect anything about the C program's behaviour.
        //
        //   __builtin_expect(e, c)     is exactly `e`; the second argument is a
        //                              branch-prediction hint with no
        //                              semantics.
        //   __builtin_constant_p(e)    folds to 0. This is the conservative
        //                              answer -- it selects the general,
        //                              non-constant code path, which is the one
        //                              that must be correct for arbitrary
        //                              input.
        StringRef bname = fd->getName();
        if (bname == "__builtin_expect" && c->getNumArgs() == 2) {
          return trRValue(c->getArg(0));
        }
        if (bname == "__builtin_expect_with_probability" &&
            c->getNumArgs() == 3) {
          return trRValue(c->getArg(0));
        }
        if (bname == "__builtin_constant_p" && c->getNumArgs() == 1) {
          return mk_int_lit(std::move(loc), mk_bigint("0"_rs),
                            trQualType(e->getType(), e->getSourceRange()));
        }
        // Any other builtin that answers a question about the *program text*
        // rather than about a value: fold it to the answer clang computed.
        // See the matching fold at the end of trRValue for the rationale; this
        // arm is needed as well because a CallExpr never reaches that fallback
        // -- it translates to a call node, and only a later pass discovers
        // that the callee has no body to call.
        if (fd->getBuiltinID() != 0 &&
            e->getType()->isIntegralOrEnumerationType()) {
          Expr::EvalResult builtinRes;
          if (e->EvaluateAsInt(builtinRes, *astCtx, Expr::SE_NoSideEffects)) {
            SmallString<32> digits;
            builtinRes.Val.getInt().toString(digits, 10, /*Signed=*/true);
            return mk_int_lit(std::move(loc), mk_bigint(toStr(digits.str())),
                              trQualType(e->getType(), e->getSourceRange()));
          }
        }
        // Detect free(ptr)
        if (fd->getName() == "free" && c->getNumArgs() == 1) {
          auto arg = c->getArg(0);
          // Strip implicit void* cast
          if (auto *ic = dyn_cast<ImplicitCastExpr>(arg)) {
            if (ic->getCastKind() == CK_BitCast) {
              arg = ic->getSubExpr();
            }
          }
          return mk_free(std::move(loc), trRValue(arg));
        }
        // Detect memset(ptr, 0, ...). Only a zero fill value is supported:
        // C `memset` writes raw bytes, and the only fill we can faithfully
        // model for arbitrary types is the all-zero one. Two shapes are
        // recognized:
        //   * memset(ptr, 0, sizeof(T))      — zero a single object of type T
        //     (struct, scalar, ...), emitted as a whole-object write of
        //     `zero_default`.
        //   * memset(ptr, 0, sizeof(T) * n)  — zero an array of byte-sized
        //     element type (e.g. uint8_t, char).
        // Non-zero fill values are rejected with a clear diagnostic.
        // A platform's zeroing wrapper is the memset intrinsic under another
        // name and a shorter argument list: `zero_memory(ptr, size)`,
        // `RtlZeroMemory(ptr, size)`, `bzero(ptr, size)`. Declaring it
        // `_memset_zero` routes it through the same recognizer, with the fill
        // value supplied rather than read from the call. Without this the
        // wrapper translates to an uninterpreted stub, which silently makes
        // every postcondition about the zeroed object vacuous.
        bool isMemsetAlias = false;
        for (auto *attr : fd->attrs()) {
          if (auto *ann = dyn_cast<AnnotateAttr>(attr);
              ann && ann->getAnnotation() == "pal-memset-zero" &&
              ann->args_size() == 0) {
            isMemsetAlias = true;
          }
        }
        if (isMemsetAlias && c->getNumArgs() != 2) {
          reportUnsupported(e->getSourceRange(), loc,
                            "a _memset_zero function must take exactly two "
                            "arguments (destination, size); ",
                            fd->getName().str());
          return mk_rvalue_err(std::move(loc),
                               trQualType(c->getType(), c->getSourceRange()));
        }
        if ((fd->getName() == "memset" && c->getNumArgs() == 3) ||
            isMemsetAlias) {
          auto *ptrArg = c->getArg(0);
          // Strip implicit void* cast
          if (auto *ic = dyn_cast<ImplicitCastExpr>(ptrArg)) {
            if (ic->getCastKind() == CK_BitCast) {
              ptrArg = ic->getSubExpr();
            }
          }
          auto *valArg = isMemsetAlias ? nullptr : c->getArg(1);
          auto *sizeArg =
              c->getArg(isMemsetAlias ? 1 : 2)->IgnoreParenImpCasts();
          Expr::EvalResult valRes;
          bool valIsZero =
              isMemsetAlias || (valArg->EvaluateAsInt(valRes, *astCtx) &&
                                valRes.Val.isInt() && valRes.Val.getInt() == 0);
          if (!valIsZero) {
            reportUnsupported(e->getSourceRange(), loc,
                              "memset is only supported with a zero fill value",
                              std::string());
            return mk_rvalue_err(std::move(loc),
                                 trQualType(c->getType(), c->getSourceRange()));
          }
          // Zeroing a single object: memset(ptr, 0, sizeof(T)) where the size
          // is a bare sizeof (no multiplication) whose type matches the
          // pointee of `ptr`. Works for any type with a `has_zero_default`
          // instance (structs, scalars, ...): it is emitted as a whole-object
          // write of `zero_default`.
          if (auto *szof = dyn_cast<UnaryExprOrTypeTraitExpr>(sizeArg)) {
            if (szof->getKind() == UETT_SizeOf) {
              auto objQt = szof->getTypeOfArgument();
              auto pointeeQt = ptrArg->getType()->getPointeeType();
              if (!pointeeQt.isNull() &&
                  astCtx->hasSameUnqualifiedType(objQt, pointeeQt)) {
                auto objTy = trQualType(pointeeQt, szof->getSourceRange());
                return mk_memset_zero(std::move(loc), std::move(objTy),
                                      trRValue(ptrArg));
              }
            }
          }
          // Zeroing a whole array: `f(arr, N)` where `arr` is an array-typed
          // lvalue that decays to the pointer argument and `N` is its size in
          // bytes. The extent lives in the array's own type, so nothing has to
          // be inferred from the way the count was spelled: `sizeof(s->field)`
          // and a literal are both accepted, and both are checked against the
          // type rather than trusted. This is the shape a platform zeroing
          // wrapper takes on a fixed-size trailing `Reserved` member, which
          // `memset(ptr, 0, sizeof(T) * n)` below cannot express because a
          // wrapper taking `void *` has no element type to name.
          {
            auto *destObj = c->getArg(0)->IgnoreParenImpCasts();
            auto destQt = destObj->getType();
            if (const auto *arrTy = astCtx->getAsConstantArrayType(destQt)) {
              auto elemQt = arrTy->getElementType();
              Expr::EvalResult szRes;
              const bool byteSized =
                  !elemQt->isIncompleteType() && !elemQt->isDependentType() &&
                  astCtx->getTypeSizeInChars(elemQt).getQuantity() == 1;
              const auto arrBytes =
                  astCtx->getTypeSizeInChars(destQt).getQuantity();
              if (byteSized && sizeArg->EvaluateAsInt(szRes, *astCtx) &&
                  szRes.Val.isInt() && szRes.Val.getInt() == arrBytes) {
                auto elemTy = trQualType(elemQt, destObj->getSourceRange());
                llvm::SmallString<20> countStr;
                llvm::APInt(64, arrBytes, true).toStringSigned(countStr);
                auto countExpr = mk_int_lit(
                    loc.clone(), mk_bigint(toStr(StringRef(countStr))),
                    trQualType(astCtx->getSizeType(), e->getSourceRange()));
                auto zeroExpr =
                    mk_int_lit(loc.clone(), mk_bigint("0"_rs),
                               trQualType(elemQt, destObj->getSourceRange()));
                return mk_memset(std::move(loc), std::move(elemTy),
                                 trRValue(ptrArg), std::move(zeroExpr),
                                 std::move(countExpr));
              }
            }
          }
          // The array shape below reads the fill value out of the call, which
          // an alias does not carry, and a wrapper taking `void *` cannot name
          // a byte-sized element type anyway. Rejecting it here keeps an
          // unrecognized alias call from falling through to an uninterpreted
          // stub.
          if (isMemsetAlias) {
            reportUnsupported(
                e->getSourceRange(), loc,
                "a _memset_zero call is only supported in the form "
                "f(ptr, sizeof(*ptr)) or f(arr, sizeof(arr)) for a "
                "fixed-size array of a byte-sized element type; ",
                fd->getName().str());
            return mk_rvalue_err(std::move(loc),
                                 trQualType(c->getType(), c->getSourceRange()));
          }
          if (auto *binOp = dyn_cast<BinaryOperator>(sizeArg)) {
            if (binOp->getOpcode() == BO_Mul) {
              auto *lhs = binOp->getLHS()->IgnoreParenImpCasts();
              auto *rhs = binOp->getRHS()->IgnoreParenImpCasts();
              const UnaryExprOrTypeTraitExpr *sizeofSide = nullptr;
              Expr *countSide = nullptr;
              if (auto *s = dyn_cast<UnaryExprOrTypeTraitExpr>(lhs)) {
                if (s->getKind() == UETT_SizeOf && s->isArgumentType()) {
                  sizeofSide = s;
                  countSide = binOp->getRHS();
                }
              }
              if (!sizeofSide) {
                if (auto *s = dyn_cast<UnaryExprOrTypeTraitExpr>(rhs)) {
                  if (s->getKind() == UETT_SizeOf && s->isArgumentType()) {
                    sizeofSide = s;
                    countSide = binOp->getLHS();
                  }
                }
              }
              if (sizeofSide && countSide) {
                auto elemQt = sizeofSide->getArgumentType();
                bool byteSized =
                    !elemQt->isIncompleteType() && !elemQt->isDependentType() &&
                    astCtx->getTypeSizeInChars(elemQt).getQuantity() == 1;
                if (byteSized) {
                  auto elemTy =
                      trQualType(elemQt, sizeofSide->getSourceRange());
                  auto countExpr = trRValue(countSide);
                  return mk_memset(std::move(loc), std::move(elemTy),
                                   trRValue(ptrArg), trRValue(valArg),
                                   std::move(countExpr));
                }
                reportUnsupported(
                    e->getSourceRange(), loc,
                    "memset is only supported on byte-sized element types "
                    "(e.g. uint8_t, char); element type ",
                    elemQt.getAsString());
                return mk_rvalue_err(
                    std::move(loc),
                    trQualType(c->getType(), c->getSourceRange()));
              }
            }
          }
        }
        auto fn = ctx.mk_ident(toStr(fd->getName()),
                               getRange(c->getCallee()->getSourceRange()));
        auto args = Vec<Rc<ir::Expr>>::new_();
        for (unsigned i = 0; i < c->getNumArgs(); ++i) {
          auto *arg = c->getArg(i);
          if (fd->isVariadic() && i >= fd->getNumParams()) {
            if (!canOmitVariadicArgument(arg)) {
              reportUnsupported(
                  arg->getSourceRange(), getRange(arg->getSourceRange()),
                  "unsupported ignored variadic argument: expected a literal, "
                  "a non-volatile local value or address, or wrapping "
                  "integer arithmetic over those",
                  "");
              return mk_rvalue_err(
                  std::move(loc),
                  trQualType(c->getType(), c->getSourceRange()));
            }
            continue;
          }
          args.push(trRValue(arg));
        }
        return mk_rvalue_fncall(std::move(loc), std::move(fn), std::move(args));
      } else {
        // Indirect call through a function-pointer value: `fptr(a, b, ...)`.
        // Clang gives no direct callee; the callee is an rvalue of
        // function-pointer type.
        if (auto *ptr = c->getCallee()->getType()->getAs<PointerType>()) {
          if (auto *proto = ptr->getPointeeType()->getAs<FunctionProtoType>();
              proto && proto->isVariadic()) {
            reportUnsupported(c->getSourceRange(), loc,
                              "indirect variadic calls are not supported", "");
            return mk_rvalue_err(std::move(loc),
                                 trQualType(c->getType(), c->getSourceRange()));
          }
        }
        auto callee = trRValue(c->getCallee());
        auto args = Vec<Rc<ir::Expr>>::new_();
        for (auto arg : c->arguments()) {
          args.push(trRValue(arg));
        }
        return mk_rvalue_fnptr_call(std::move(loc), std::move(callee),
                                    std::move(args));
      }
    } else if (auto *cl = dyn_cast<CompoundLiteralExpr>(e)) {
      auto *init = dyn_cast<InitListExpr>(cl->getInitializer());
      if (!init) {
        reportUnsupported(e->getSourceRange(), loc,
                          "unsupported compound literal without init list", "");
        return mk_rvalue_err(std::move(loc),
                             trQualType(e->getType(), e->getSourceRange()));
      }
      return trInitList(init, e->getSourceRange(), std::move(loc));
    } else if (auto *init = dyn_cast<InitListExpr>(e)) {
      return trInitList(init, e->getSourceRange(), std::move(loc));
    } else if (auto *co = dyn_cast<ConditionalOperator>(e)) {
      if (auto *arm = constantCondArm(co)) {
        return trRValue(arm);
      }
      // The condition is evaluated unconditionally and may hoist; the two arms
      // are not, so a statement expression in either must stay where it is.
      auto cond = trRValue(co->getCond());
      NoHoist noHoist(&hoistTarget);
      return mk_cond(std::move(loc), std::move(cond),
                     trRValue(co->getTrueExpr()), trRValue(co->getFalseExpr()));
    } else if (auto *bco = dyn_cast<BinaryConditionalOperator>(e)) {
      // GNU `a ?: b`: `a` if it is nonzero, else `b`, with `a` evaluated
      // once.
      // TODO: The current encoding will evaluate `b` unconditionally; can be
      // fix by translating to an if-statement?
      if (bco->getFalseExpr()->HasSideEffects(*astCtx)) {
        reportUnsupported(e->getSourceRange(), loc,
                          "GNU ?: with an effectful right operand", "");
        return mk_rvalue_err(std::move(loc),
                             trQualType(e->getType(), e->getSourceRange()));
      }
      return mk_rvalue_binop(std::move(loc), ir::BinOp::Elvis(),
                             trRValue(bco->getCommon()),
                             trRValue(bco->getFalseExpr()));
    } else if (auto *dre = dyn_cast<DeclRefExpr>(e)) {
      if (auto *ecd = dyn_cast<EnumConstantDecl>(dre->getDecl())) {
        const auto val = ecd->getInitVal();
        SmallString<20> valStr;
        val.toString(valStr, 10, val.isSigned());
        return mk_int_lit(std::move(loc), mk_bigint(toStr(StringRef(valStr))),
                          trQualType(e->getType(), e->getSourceRange()));
      }
      // A bare reference to a function (function-to-pointer decay): produce a
      // function reference, identical to `&func`.
      if (auto *fd = dyn_cast<FunctionDecl>(dre->getDecl())) {
        auto id = ctx.mk_ident(toStr(fd->getName()), loc.clone());
        return mk_rvalue_fnref(std::move(loc), std::move(id));
      }
      // Other DeclRefExpr in rvalue context: treat as lvalue read
      return mk_rvalue_lvalue(std::move(loc), trLValue(e));
    } else if (auto *m = dyn_cast<MemberExpr>(e)) {
      // A member of a structure *value* -- `f(x).field`, or a field of a
      // compound literal -- is itself an rvalue in C, so there is no lvalue to
      // project from and trLValue cannot be used. Translate the base as a value
      // and project the field out of it; ExprT::Member is neutral, and emit
      // already renders a value base as a record field selection rather than a
      // reference projection.
      auto *md = m->getMemberDecl();
      std::string nameStr;
      if (auto *fd = dyn_cast<FieldDecl>(md))
        nameStr = fieldNameStr(fd);
      else
        nameStr = md->getName().str();
      auto id = ctx.mk_ident(toStr(nameStr), loc.clone());
      // When the base was hoisted out of the enclosing statement, project from
      // the temporary rather than re-translating the call.
      auto hoisted = hoistedRValues.find(m->getBase()->IgnoreParenImpCasts());
      if (hoisted != hoistedRValues.end()) {
        auto tmp = ctx.mk_ident(toStr(StringRef(hoisted->second)), loc.clone());
        auto tmpRef = mk_lvalue_var(loc.clone(), std::move(tmp));
        return mk_lvalue_member(std::move(loc), std::move(tmpRef),
                                std::move(id));
      }
      auto base = m->isArrow() ? mk_deref(loc.clone(), trRValue(m->getBase()))
                               : trRValue(m->getBase());
      return mk_lvalue_member(std::move(loc), std::move(base), std::move(id));
    } else if (auto *u = dyn_cast<UnaryExprOrTypeTraitExpr>(e)) {
      auto kind = u->getKind();
      if (kind == UETT_SizeOf || kind == UETT_AlignOf ||
          kind == UETT_PreferredAlignOf) {
        auto argTy = u->getTypeOfArgument();
        if (argTy->isIncompleteType() || argTy->isDependentType() ||
            argTy->isVariableArrayType()) {
          reportUnsupported(
              e->getSourceRange(), loc,
              "sizeof/_Alignof on incomplete, dependent, or VLA type ", "");
          return mk_rvalue_err(std::move(loc),
                               trQualType(e->getType(), e->getSourceRange()));
        }
        auto ty = trQualType(argTy, e->getSourceRange());
        if (kind == UETT_SizeOf) {
          return mk_sizeof(std::move(loc), std::move(ty));
        } else {
          return mk_alignof(std::move(loc), std::move(ty));
        }
      }
    } else if (auto *off = dyn_cast<OffsetOfExpr>(e)) {
      // `offsetof(S, m)` is a ground fact about the ABI, in the same way the
      // size of a complete record is, and clang has already computed it. Fold
      // it to its value rather than leaving the whole enclosing function
      // untranslatable. This shares the layout assumption `c_sizeof` makes:
      // the layout being proved against is the one this compiler chooses.
      Expr::EvalResult evalResult;
      if (off->EvaluateAsInt(evalResult, *astCtx)) {
        SmallString<32> digits;
        evalResult.Val.getInt().toString(digits, 10, /*Signed=*/false);
        return mk_int_lit(std::move(loc), mk_bigint(toStr(digits.str())),
                          trQualType(e->getType(), e->getSourceRange()));
      }
      reportUnsupported(e->getSourceRange(), loc,
                        "offsetof whose value is not a constant", "");
      return mk_rvalue_err(std::move(loc),
                           trQualType(e->getType(), e->getSourceRange()));
    }

    // __builtin_choose_expr(c, a, b) is `a` or `b` -- decided by the compiler,
    // not at run time -- and, crucially, the branch not chosen is not even
    // type-checked.  So the choice must be made here rather than translated:
    // the other operand may not be a well-typed expression at all.  Clang has
    // already made it.
    //
    // A ROUND_UP macro can use the builtin to pick a width-appropriate
    // rounding expression from the argument's size.
    if (auto *ce = dyn_cast<ChooseExpr>(e)) {
      return trRValue(ce->getChosenSubExpr());
    }

    // A statement expression whose body reduces to a single expression.
    //
    // `({ e; })` is exactly `e`.  PAL cannot translate the general form --
    // `({ s1; s2; e; })` has statements in it, and an rvalue has nowhere to
    // put them; hoisting them out would move them across the surrounding
    // expression's other operands, which C's sequencing rules do not permit --
    // but the degenerate form is common, because the GNU idiom is how C
    // writes a macro that must not evaluate its argument twice or must not be
    // usable as an lvalue, and many such macros wrap a single expression.
    //
    // Statements are skipped ahead of the final expression only when they
    // cannot affect it: a null statement, and a declaration group consisting
    // entirely of static assertions (which macros use for argument type
    // checking).  A
    // declaration that introduces a variable, or any other statement, still
    // reaches the unsupported diagnostic -- dropping it would change the
    // program, and keeping it is the hoisting problem above.
    //
    // In statement position no restriction is needed; see trStmt.
    if (auto *se = dyn_cast<StmtExpr>(e)) {
      if (auto *comp = dyn_cast<CompoundStmt>(se->getSubStmt())) {
        Expr *value = nullptr;
        bool reducible = comp->size() > 0;
        for (auto *s : comp->body()) {
          if (value != nullptr) {
            // The value-yielding expression must be last.
            reducible = false;
            break;
          }
          if (isa<NullStmt>(s)) {
            continue;
          }
          if (auto *ds = dyn_cast<DeclStmt>(s)) {
            bool allStaticAsserts = true;
            for (auto *d : ds->decls()) {
              if (!isa<StaticAssertDecl>(d)) {
                allStaticAsserts = false;
              }
            }
            if (allStaticAsserts) {
              continue;
            }
            reducible = false;
            break;
          }
          if (auto *sub = dyn_cast<Expr>(s)) {
            value = sub;
            continue;
          }
          reducible = false;
          break;
        }
        if (reducible && value != nullptr) {
          return trRValue(value);
        }
        // Otherwise the body has statements in it. If this position has
        // somewhere to put them -- see hoistTarget -- run them there, ahead of
        // the value.
        //
        // This is the shape most GNU macros actually have: a local bound to
        // the argument so it is evaluated once, a check on it, then the
        // result. A typical ROUND_UP is exactly that, and so is
        // DIV_ROUND_UP.
        //
        // Sound because hoistTarget is set only where the statements'
        // new position and their old one are separated by nothing that C
        // evaluates: a declaration's initializer and an assignment
        // statement's right-hand side have no other operands to cross, and
        // both are evaluated exactly once. Every conditionally-evaluated
        // operand clears it again. What is NOT attempted is hoisting out of
        // an operand with siblings -- `f(g(), ({...}))` -- where the
        // statements would move across `g()`.
        if (hoistTarget != nullptr && comp->size() > 0) {
          auto *last = *(comp->body_end() - 1);
          if (auto *lastValue = dyn_cast<Expr>(last)) {
            for (auto *s : comp->body()) {
              if (s == last) {
                break;
              }
              trStmt(*hoistTarget, s);
            }
            return trRValue(lastValue);
          }
        }
      }
    }

    // Last resort, before giving up: an expression that asks a question about
    // the *program text* rather than about a value, and that clang has already
    // answered.
    //
    // These are the type-level predicates -- __builtin_classify_type,
    // __builtin_types_compatible_p, and their relatives -- which C code uses to
    // select between branches at compile time. Translating such a test
    // faithfully is not merely hard, it is wrong: the branch not taken is
    // typically an error stub that has no definition, so only the folded value
    // describes the program that is actually compiled.
    //
    // Three things make this safe to do here rather than as a general
    // simplification:
    //   * it is reached only where PAL was about to emit `(admit())` for the
    //     whole enclosing expression, so it cannot displace any translation
    //     PAL would otherwise perform, and cannot weaken any obligation --
    //     an admit() discards them all;
    //   * SE_NoSideEffects makes clang decline the fold if evaluating the
    //     expression could do anything observable;
    //   * an integral result type, since that is all mk_int_lit can carry.
    //
    // Generated RPC-stub headers reach this by wrapping every call argument
    // in a CHECK_SCALAR test that rejects struct and union arguments at
    // compile time. See test/classify_type.
    if (e->getType()->isIntegralOrEnumerationType()) {
      Expr::EvalResult constRes;
      if (e->EvaluateAsInt(constRes, *astCtx, Expr::SE_NoSideEffects)) {
        SmallString<32> digits;
        constRes.Val.getInt().toString(digits, 10, /*Signed=*/true);
        return mk_int_lit(std::move(loc), mk_bigint(toStr(digits.str())),
                          trQualType(e->getType(), e->getSourceRange()));
      }
    }

    reportUnsupported(e->getSourceRange(), loc,
                      "unsupported rvalue expression ", e->getStmtClassName());
    return mk_rvalue_err(std::move(loc),
                         trQualType(e->getType(), e->getSourceRange()));
  }

  bool isNull(Expr *e) {
    if (auto *c = dyn_cast<CastExpr>(e)) {
      if (c->getCastKind() == CK_NullToPointer)
        return true;
      return isNull(c->getSubExpr());
    } else if (auto *p = dyn_cast<ParenExpr>(e)) {
      return isNull(p->getSubExpr());
    } else {
      return false;
    }
  }

  Vec<Rc<ir::Stmt>> trStmts(Stmt *stmt) {
    auto stmts = Vec<Rc<ir::Stmt>>::new_();
    if (stmt)
      trStmt(stmts, stmt);
    return stmts;
  }

  /// Structure-valued call results bound ahead of the statement that projects
  /// from them, keyed by the call expression.
  std::map<const Expr *, std::string> hoistedRValues;
  std::map<const Expr *, std::string> hoistedCompoundLiterals;
  int rvalueHoistCounter = 0;

  /// Bind a structure-valued call that a member projection reads from to a
  /// uniquely named local, ahead of the statement that contains it.
  ///
  /// `f(x).field` has no lvalue to project from, so the call's result has to
  /// live somewhere before the field can be read. Pulse will hoist it on its
  /// own, but its hoisted binders are named from a counter that does not
  /// survive leaving a statement, so two of them can end up sharing a name; a
  /// branch-local one then captures a same-named binder introduced before the
  /// branch, and the branch postcondition becomes ill-typed. Naming the
  /// temporary here keeps the names unique by construction and makes the
  /// emitted Pulse say what the C says.
  ///
  /// Only unconditionally evaluated positions are hoisted: moving a call out
  /// of a `?:` arm or the right operand of `&&`/`||` would evaluate it when C
  /// would not.
  void hoistRValueMembers(Vec<Rc<ir::Stmt>> &stmts, Expr *e) {
    if (!e)
      return;
    e = e->IgnoreParens();
    if (auto *co = dyn_cast<ConditionalOperator>(e)) {
      hoistRValueMembers(stmts, co->getCond());
      return;
    }
    if (auto *bo = dyn_cast<BinaryOperator>(e)) {
      if (bo->getOpcode() == BO_LAnd || bo->getOpcode() == BO_LOr) {
        hoistRValueMembers(stmts, bo->getLHS());
        return;
      }
    }
    for (auto *child : e->children()) {
      if (auto *ce = dyn_cast_or_null<Expr>(child)) {
        hoistRValueMembers(stmts, ce);
      }
    }
    auto *m = dyn_cast<MemberExpr>(e);
    if (!m || m->isArrow()) {
      return;
    }
    auto *base = m->getBase()->IgnoreParenImpCasts();
    if (!base->isPRValue() || !isa<CallExpr>(base)) {
      return;
    }
    if (hoistedRValues.count(base)) {
      return;
    }
    auto baseLoc = getRange(base->getSourceRange());
    auto ty = trQualType(base->getType(), base->getSourceRange());
    auto name = "__pal_rvalue_" + std::to_string(rvalueHoistCounter++);
    auto id = ctx.mk_ident(toStr(StringRef(name)), baseLoc.clone());
    auto rval = trRValue(base);
    stmts.push(mk_let_stmt(baseLoc.clone(), std::move(id), std::move(ty),
                           std::move(rval)));
    hoistedRValues[base] = name;
  }

  void hoistAddressedCompoundLiterals(Vec<Rc<ir::Stmt>> &stmts, Expr *e) {
    if (!e)
      return;
    e = e->IgnoreParens();
    if (auto *co = dyn_cast<ConditionalOperator>(e)) {
      hoistAddressedCompoundLiterals(stmts, co->getCond());
      return;
    }
    if (auto *bo = dyn_cast<BinaryOperator>(e)) {
      if (bo->getOpcode() == BO_LAnd || bo->getOpcode() == BO_LOr) {
        hoistAddressedCompoundLiterals(stmts, bo->getLHS());
        return;
      }
    }
    if (auto *uo = dyn_cast<UnaryOperator>(e);
        uo && uo->getOpcode() == UO_AddrOf) {
      auto *base = uo->getSubExpr()->IgnoreParenImpCasts();
      if (auto *cl = dyn_cast<CompoundLiteralExpr>(base)) {
        if (!hoistedCompoundLiterals.count(base)) {
          auto baseLoc = getRange(base->getSourceRange());
          auto ty = trQualType(base->getType(), base->getSourceRange());
          auto name = "__pal_compound_" + std::to_string(rvalueHoistCounter++);
          auto id = ctx.mk_ident(toStr(StringRef(name)), baseLoc.clone());
          stmts.push(mk_var_decl(baseLoc.clone(), id.clone(), ty.clone()));
          stmts.push(mk_assign(baseLoc.clone(),
                               mk_lvalue_var(baseLoc.clone(), id.clone()),
                               trRValue(cl)));
          hoistedCompoundLiterals[base] = name;
        }
        return;
      }
    }
    for (auto *child : e->children()) {
      if (auto *ce = dyn_cast_or_null<Expr>(child)) {
        hoistAddressedCompoundLiterals(stmts, ce);
      }
    }
  }

  rust::Unit trStmt(Vec<Rc<ir::Stmt>> &stmts, Stmt *stmt) {
    auto loc = getRange(stmt->getSourceRange());

    if (auto *e = dyn_cast<Expr>(stmt)) {
      hoistAddressedCompoundLiterals(stmts, e);
      hoistRValueMembers(stmts, e);
    } else if (auto *ret = dyn_cast<ReturnStmt>(stmt)) {
      hoistAddressedCompoundLiterals(stmts, ret->getRetValue());
      hoistRValueMembers(stmts, ret->getRetValue());
    } else if (auto *ifs = dyn_cast<IfStmt>(stmt)) {
      hoistAddressedCompoundLiterals(stmts, ifs->getCond());
      hoistRValueMembers(stmts, ifs->getCond());
    } else if (auto *ds = dyn_cast<DeclStmt>(stmt)) {
      for (auto *d : ds->decls()) {
        if (auto *vd = dyn_cast<VarDecl>(d)) {
          hoistAddressedCompoundLiterals(stmts, vd->getInit());
          hoistRValueMembers(stmts, vd->getInit());
        }
      }
    }

    if (auto *bo = dyn_cast<BinaryOperator>(stmt)) {
      switch (bo->getOpcode()) {
      case clang::BO_Assign:
        return stmts.push(mk_assign(std::move(loc), trLValue(bo->getLHS()),
                                    trRValue(bo->getRHS())));

      case clang::BO_Comma:
        trStmt(stmts, bo->getLHS());
        return trStmt(stmts, bo->getRHS());

      case clang::BO_AddAssign:
      case clang::BO_SubAssign:
      case clang::BO_MulAssign:
      case clang::BO_DivAssign:
      case clang::BO_RemAssign:
      case clang::BO_ShlAssign:
      case clang::BO_ShrAssign:
      case clang::BO_AndAssign:
      case clang::BO_OrAssign:
      case clang::BO_XorAssign: {
        auto getBinOp = [](BinaryOperatorKind ok) -> ir::BinOp {
          switch (ok) {
          case BO_AddAssign:
            return ir::BinOp::Add();
          case BO_SubAssign:
            return ir::BinOp::Sub();
          case BO_MulAssign:
            return ir::BinOp::Mul();
          case BO_DivAssign:
            return ir::BinOp::Div();
          case BO_RemAssign:
            return ir::BinOp::Mod();
          case BO_ShlAssign:
            return ir::BinOp::Shl();
          case BO_ShrAssign:
            return ir::BinOp::Shr();
          case BO_AndAssign:
            return ir::BinOp::BitAnd();
          case BO_OrAssign:
            return ir::BinOp::BitOr();
          case BO_XorAssign:
            return ir::BinOp::BitXor();
          default:
            __builtin_unreachable();
          }
        };
        auto op = getBinOp(bo->getOpcode());
        auto lhsRval = mk_rvalue_lvalue(loc.clone(), trLValue(bo->getLHS()));
        auto rhs = trRValue(bo->getRHS());
        auto result = mk_rvalue_binop(loc.clone(), std::move(op),
                                      std::move(lhsRval), std::move(rhs));
        return stmts.push(mk_assign(std::move(loc), trLValue(bo->getLHS()),
                                    std::move(result)));
      }

      default:;
        // continue to error case
      }
    } else if (auto *uo = dyn_cast<UnaryOperator>(stmt)) {
      auto lhs = trLValue(uo->getSubExpr());
      switch (uo->getOpcode()) {
      case UO_PreInc: {
        auto exprLoc = loc.clone();
        return stmts.push(mk_call(
            std::move(loc), mk_pre_incr(std::move(exprLoc), std::move(lhs))));
      }
      case UO_PostInc: {
        auto exprLoc = loc.clone();
        return stmts.push(mk_call(
            std::move(loc), mk_post_incr(std::move(exprLoc), std::move(lhs))));
      }
      case UO_PreDec: {
        auto exprLoc = loc.clone();
        return stmts.push(mk_call(
            std::move(loc), mk_pre_decr(std::move(exprLoc), std::move(lhs))));
      }
      case UO_PostDec: {
        auto exprLoc = loc.clone();
        return stmts.push(mk_call(
            std::move(loc), mk_post_decr(std::move(exprLoc), std::move(lhs))));
      }
      default:;
        // continue to error case
      }
    } else if (auto *i = dyn_cast<IfStmt>(stmt)) {
      auto thenStmt = i->getThen();
      auto enss = Vec<Rc<ir::Expr>>::new_();
      if (auto attrThen = dyn_cast_or_null<AttributedStmt>(thenStmt)) {
        for (auto attr : attrThen->getAttrs()) {
          if (auto ens = isUnaryAttrOf(attr, "pal-ensures")) {
            enss.push(std::move(ens.value()));
          }
        }
        thenStmt = attrThen->getSubStmt();
      }
      return stmts.push(mk_if(loc.clone(), trRValue(i->getCond()),
                              trStmts(thenStmt), trStmts(i->getElse()),
                              std::move(enss)));
    } else if (auto *w = dyn_cast<WhileStmt>(stmt)) {
      auto body = w->getBody();
      auto invs = Vec<Rc<ir::Expr>>::new_();
      auto reqs = Vec<Rc<ir::Expr>>::new_();
      auto enss = Vec<Rc<ir::Expr>>::new_();
      if (auto attrBody = dyn_cast<AttributedStmt>(body)) {
        for (auto attr : attrBody->getAttrs()) {
          if (auto inv = isUnaryAttrOf(attr, "pal-invariant")) {
            invs.push(std::move(inv.value()));
          } else if (auto req = isUnaryAttrOf(attr, "pal-requires")) {
            reqs.push(std::move(req.value()));
          } else if (auto ens = isUnaryAttrOf(attr, "pal-ensures")) {
            enss.push(std::move(ens.value()));
          }
        }
        body = attrBody->getSubStmt();
      }
      auto savedIncrement = forLoopIncrement;
      forLoopIncrement = nullptr;
      auto bodyStmts = trStmts(body);
      forLoopIncrement = savedIncrement;
      return stmts.push(mk_while(loc.clone(), trRValue(w->getCond()),
                                 std::move(invs), std::move(reqs),
                                 std::move(enss), std::move(bodyStmts)));
    } else if (auto *d = dyn_cast<DoStmt>(stmt)) {
      // Desugar `do { body } while (cond)` into a `while` loop. There are two
      // desugarings, and the presence of a *top-level* `continue` in the body
      // selects between them:
      //
      //   * Clean desugaring (no top-level `continue`):
      //         bool cont = true; bool first = true;
      //         while (cont) { body; first = false; cont = cond; }
      //     Here `cont` (the "continuation" flag) drives the loop: it is forced
      //     true so the body runs at least once (do-while semantics), then the
      //     guard is re-evaluated at the *end* of the body via `cont = cond`.
      //
      //   * Legacy desugaring (a top-level `continue` is present):
      //         bool first = true;
      //         while (first || cond) { first = false; body; }
      //     We cannot use the clean form here: a top-level `continue` would
      //     jump past the trailing `cont = cond` update, so the guard would
      //     never be re-evaluated and the loop could spin forever. The legacy
      //     form keeps the guard `cond` in the `while` condition (re-evaluated
      //     on each iteration, side effects and all) where `continue` cannot
      //     skip it.
      //
      // `hasTopLevelContinue` decides which form to use. It treats a nested
      // for/while/do-while as a boundary (a `continue` inside one binds to that
      // inner loop, not to us) but descends into if/switch/blocks/labels, since
      // a `continue` there does target this do-while.
      //
      // Annotations:
      //   * `_do_while_first(name)` names the first-iteration flag so the user
      //     can mention it in invariants (e.g. `first ==> i < n`).
      //   * `_do_while_cond(name)` names the continuation flag `cont`. This is
      //     needed for impure guards: the auto-linking invariant (below) is
      //     omitted when the guard has side effects, so the user must name
      //     `cont` and supply their own *pure* linking invariant relating it to
      //     program state (e.g. `cont == (s.x < 10)`).

      // Extract annotations and check for _do_while_first / _do_while_cond
      auto body = d->getBody();
      auto invs = Vec<Rc<ir::Expr>>::new_();
      auto reqs = Vec<Rc<ir::Expr>>::new_();
      auto enss = Vec<Rc<ir::Expr>>::new_();
      std::string flagName;
      std::string condName;
      // Whether the user wrote any loop annotation on this do-while. The Vec
      // bridge exposes only new_/push, so emptiness is tracked here rather
      // than queried afterwards.
      bool sawLoopAnnot = false;
      if (auto attrBody = dyn_cast<AttributedStmt>(body)) {
        for (auto attr : attrBody->getAttrs()) {
          if (auto inv = isUnaryAttrOf(attr, "pal-invariant")) {
            invs.push(std::move(inv.value()));
            sawLoopAnnot = true;
          } else if (auto req = isUnaryAttrOf(attr, "pal-requires")) {
            reqs.push(std::move(req.value()));
            sawLoopAnnot = true;
          } else if (auto ens = isUnaryAttrOf(attr, "pal-ensures")) {
            enss.push(std::move(ens.value()));
            sawLoopAnnot = true;
          } else if (auto ann = dyn_cast<AnnotateAttr>(attr)) {
            if (ann->getAnnotation() == "pal-do-while-first" &&
                ann->args_size() == 1) {
              auto *arg = (*ann->args_begin())->IgnoreParenImpCasts();
              if (auto *sl = dyn_cast<StringLiteral>(arg)) {
                flagName = sl->getString().str();
              }
            } else if (ann->getAnnotation() == "pal-do-while-cond" &&
                       ann->args_size() == 1) {
              auto *arg = (*ann->args_begin())->IgnoreParenImpCasts();
              if (auto *sl = dyn_cast<StringLiteral>(arg)) {
                condName = sl->getString().str();
              }
            }
          }
        }
        body = attrBody->getSubStmt();
      }

      // `do { ... } while (0)` is not a loop. It is C's standard idiom for
      // giving a multi-statement macro a single-statement body (C FAQ 10.4),
      // and BUG_ON and assert-style macros are built from it.
      //
      // Desugaring it like any other do-while is semantically correct but
      // destroys the facts it establishes: the body becomes a Pulse `while`,
      // and the *only* thing that survives a loop is its invariant. The
      // auto-generated invariant relates the two loop-control flags and says
      // nothing about program state, so
      //
      //     BUG_ON(i >= n);   // do { if (i >= n) abort(); } while (0)
      //
      // taught the solver nothing about `i` afterwards -- even though
      // _pal_abort ensures `pure False`, so the `if` really does establish
      // `i < n` on the path that continues. Every bounds check written this
      // way was invisible, which for a codebase whose validation idiom *is*
      // BUG_ON means essentially all of its input validation was invisible.
      //
      // When the guard is a constant zero the body runs exactly once, so
      // emitting it straight-line is not an optimisation but the faithful
      // translation. Guarded conservatively:
      //   * a top-level `break` or `continue` in the body targets this
      //     do-while (both exit it, since the guard is false); inlining would
      //     silently re-bind them to an enclosing loop, or to nothing;
      //   * any user annotation means the user is treating this as a loop, so
      //     honour that and take the general path.
      {
        auto condVal = d->getCond()->getIntegerConstantExpr(*astCtx);
        bool isZeroGuard = !d->getCond()->HasSideEffects(*astCtx) &&
                           condVal.has_value() && *condVal == 0;
        if (isZeroGuard && !sawLoopAnnot && flagName.empty() &&
            condName.empty() && !hasTopLevelBreak(body) &&
            !hasTopLevelContinue(body)) {
          return trStmt(stmts, body);
        }
      }

      // First-iteration flag: named by _do_while_first, else auto-generated.
      // Its
      // `_live` invariant is auto-injected only when the name is auto-generated
      // (a user-named flag is expected to be mentioned in the user's
      // invariant).
      bool firstIsAuto = flagName.empty();
      if (firstIsAuto) {
        static int doCounter = 0;
        flagName = "__do_first_" + std::to_string(doCounter++);
      }
      auto firstId = ctx.mk_ident(toStr(flagName), loc.clone());

      // Continuation flag `cont`: named by _do_while_cond, else auto-generated.
      // As with `first`, `_live(cont)` is auto-injected only when the name is
      // auto-generated; a user-named `cont` is expected to appear (with its own
      // `_live`) in the user's invariants.
      bool condIsAuto = condName.empty();
      if (condIsAuto) {
        static int doContCounter = 0;
        condName = "__do_cont_" + std::to_string(doContCounter++);
      }
      auto contId = ctx.mk_ident(toStr(condName), loc.clone());

      if (!hasTopLevelContinue(body)) {
        // Clean desugaring: no top-level `continue`.

        // bool cont; cont = true;
        stmts.push(mk_var_decl(loc.clone(), contId.clone(),
                               mk_bool_type(loc.clone())));
        stmts.push(mk_assign(loc.clone(),
                             mk_lvalue_var(loc.clone(), contId.clone()),
                             mk_bool_lit(loc.clone(), true)));
        // bool first; first = true;
        stmts.push(mk_var_decl(loc.clone(), firstId.clone(),
                               mk_bool_type(loc.clone())));
        stmts.push(mk_assign(loc.clone(),
                             mk_lvalue_var(loc.clone(), firstId.clone()),
                             mk_bool_lit(loc.clone(), true)));

        // while condition: cont
        auto whileCond = mk_rvalue_lvalue(
            loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()));

        // Inject _live(cont) and _live(first) when the respective flag name was
        // auto-generated (a user-named flag carries its own _live).
        if (condIsAuto) {
          invs.push(
              mk_live(loc.clone(), mk_lvalue_var(loc.clone(), contId.clone())));
        }
        if (firstIsAuto) {
          invs.push(mk_live(loc.clone(),
                            mk_lvalue_var(loc.clone(), firstId.clone())));
        }

        // Link the internal `cont` flag back to the loop condition so the body
        // knows `cond` held on re-entry. The guard `while (cont)` alone conveys
        // nothing to the solver about `cond`, yet many bodies rely on it (e.g.
        // a body doing `i = i + 1` needs `i < n` to maintain `i <= n`). We
        // inject:
        //     cont == (first || cond)
        // which, together with the guard `cont == true`, re-supplies exactly
        // the `first || cond` fact the original do-while guard would have
        // provided.
        //
        // This is only sound when `cond` is a *pure* expression: the invariant
        // is a `with_pure` proposition, so an impure guard (e.g. `while (f())`)
        // cannot appear in it. When the guard has side effects we omit the
        // linking invariant entirely (such loops must instead carry a
        // user-written invariant relating program state to the guard's result).
        if (!d->getCond()->HasSideEffects(*astCtx)) {
          auto firstRead = mk_rvalue_lvalue(
              loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone()));
          auto contReadInv = mk_rvalue_lvalue(
              loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()));
          auto firstOrCond =
              mk_rvalue_binop(loc.clone(), ir::BinOp::LogOr(),
                              std::move(firstRead), trRValue(d->getCond()));
          invs.push(mk_rvalue_binop(loc.clone(), ir::BinOp::Eq(),
                                    std::move(contReadInv),
                                    std::move(firstOrCond)));
        }

        // Build body: original_body; first = false; cont = cond;
        auto bodyStmts = Vec<Rc<ir::Stmt>>::new_();
        auto savedIncrement = forLoopIncrement;
        forLoopIncrement = nullptr;
        trStmt(bodyStmts, body);
        forLoopIncrement = savedIncrement;
        bodyStmts.push(mk_assign(loc.clone(),
                                 mk_lvalue_var(loc.clone(), firstId.clone()),
                                 mk_bool_lit(loc.clone(), false)));
        bodyStmts.push(mk_assign(loc.clone(),
                                 mk_lvalue_var(loc.clone(), contId.clone()),
                                 trRValue(d->getCond())));

        return stmts.push(mk_while(std::move(loc), std::move(whileCond),
                                   std::move(invs), std::move(reqs),
                                   std::move(enss), std::move(bodyStmts)));
      }

      // Legacy desugaring: body has a top-level `continue`.
      //
      // The `cont` flag plays no role here (the guard is `first || cond`), but
      // if the user named it via `_do_while_cond(cont)` we still declare and
      // initialize it. That way an invariant / `_live` referencing `cont`
      // resolves to a real, initialized variable and the generated F* file does
      // not break -- even though nothing in this desugaring reads `cont`.
      if (!condIsAuto) {
        stmts.push(mk_var_decl(loc.clone(), contId.clone(),
                               mk_bool_type(loc.clone())));
        stmts.push(mk_assign(loc.clone(),
                             mk_lvalue_var(loc.clone(), contId.clone()),
                             mk_bool_lit(loc.clone(), true)));
      }

      // bool first; first = true;
      stmts.push(
          mk_var_decl(loc.clone(), firstId.clone(), mk_bool_type(loc.clone())));
      stmts.push(mk_assign(loc.clone(),
                           mk_lvalue_var(loc.clone(), firstId.clone()),
                           mk_bool_lit(loc.clone(), true)));

      // while condition: first || cond
      auto flagRead = mk_rvalue_lvalue(
          loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone()));
      auto whileCond =
          mk_rvalue_binop(loc.clone(), ir::BinOp::LogOr(), std::move(flagRead),
                          trRValue(d->getCond()));

      // Add _live(first) to invariants when the name is auto-generated.
      if (firstIsAuto) {
        invs.push(
            mk_live(loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone())));
      }

      // Build body: first = false; original_body;
      auto bodyStmts = Vec<Rc<ir::Stmt>>::new_();
      bodyStmts.push(mk_assign(loc.clone(),
                               mk_lvalue_var(loc.clone(), firstId.clone()),
                               mk_bool_lit(loc.clone(), false)));
      auto savedIncrement = forLoopIncrement;
      forLoopIncrement = nullptr;
      trStmt(bodyStmts, body);
      forLoopIncrement = savedIncrement;

      return stmts.push(mk_while(std::move(loc), std::move(whileCond),
                                 std::move(invs), std::move(reqs),
                                 std::move(enss), std::move(bodyStmts)));
    } else if (auto *sw = dyn_cast<SwitchStmt>(stmt)) {
      // Desugar: switch (scrutinee) { case v1: s1; case v2: s2; default: sd }
      //      --> let scrut = scrutinee;
      //          bool hit = false; bool brk = false;
      //          if (!brk && (hit || scrut == v1)) { hit = true; s1 }
      //          if (!brk && (hit || scrut == v2)) { hit = true; s2 }
      //          if (!brk) { sd }
      // break inside case bodies sets brk = true.

      // Evaluate scrutinee
      auto scrutRval = trRValue(sw->getCond());
      auto scrutTy =
          trQualType(sw->getCond()->getType(), sw->getCond()->getSourceRange());

      // Bind the scrutinee once as an immutable value.
      static int switchCounter = 0;
      auto switchIndex = switchCounter++;
      auto scrutName = "__switch_scrut_" + std::to_string(switchIndex);
      auto scrutId = ctx.mk_ident(toStr(scrutName), loc.clone());
      stmts.push(mk_let_stmt(loc.clone(), scrutId.clone(), scrutTy.clone(),
                             std::move(scrutRval)));

      // Collect cases from the switch body. A switch postcondition is used as
      // the join invariant for every desugared case test.
      auto *body = sw->getBody();
      std::vector<Rc<ir::Expr>> switchEnss;
      if (auto attrBody = dyn_cast<AttributedStmt>(body)) {
        for (auto attr : attrBody->getAttrs()) {
          if (auto ens = isUnaryAttrOf(attr, "pal-ensures")) {
            switchEnss.push_back(std::move(ens.value()));
          }
        }
        body = attrBody->getSubStmt();
      }
      auto *comp = dyn_cast<CompoundStmt>(body);
      if (!comp) {
        reportUnsupported(body->getSourceRange(), loc,
                          "switch body must be a compound statement", "");
        return {};
      }

      auto containsSwitchBreak = [&](auto &self, Stmt *s) -> bool {
        if (dyn_cast<BreakStmt>(s))
          return true;
        if (dyn_cast<SwitchStmt>(s) || dyn_cast<ForStmt>(s) ||
            dyn_cast<WhileStmt>(s) || dyn_cast<DoStmt>(s))
          return false;
        for (auto *child : s->children()) {
          if (child && self(self, child))
            return true;
        }
        return false;
      };
      bool switchCanBreak = false;
      for (auto *child : comp->body())
        switchCanBreak |= containsSwitchBreak(containsSwitchBreak, child);

      // Walk the compound statement collecting case/default groups
      // Clang attaches only the first statement after a label to CaseStmt or
      // DefaultStmt. The remaining statements are siblings in the compound
      // body, but are still controlled by that label in C.
      struct SwitchGroup {
        Stmt *label;
        bool isDefault;
        std::vector<Expr *> caseValues;
        std::vector<Stmt *> body;
      };
      std::vector<SwitchGroup> groups;
      bool seenDefault = false;
      SwitchGroup *currentGroup = nullptr;
      for (auto *child : comp->body()) {
        if (auto *cs = dyn_cast<CaseStmt>(child)) {
          auto childLoc = getRange(child->getSourceRange());
          if (seenDefault) {
            reportUnsupported(cs->getSourceRange(), childLoc,
                              "default must be the last case in switch", "");
            break;
          }

          groups.push_back({child, false, {}, {}});
          currentGroup = &groups.back();
          Stmt *caseBody = child;
          while (auto *innerCs = dyn_cast<CaseStmt>(caseBody)) {
            currentGroup->caseValues.push_back(innerCs->getLHS());
            caseBody = innerCs->getSubStmt();
          }
          if (auto *ds = dyn_cast_or_null<DefaultStmt>(caseBody)) {
            seenDefault = true;
            currentGroup->isDefault = true;
            caseBody = ds->getSubStmt();
          }
          if (caseBody)
            currentGroup->body.push_back(caseBody);
        } else if (auto *ds = dyn_cast<DefaultStmt>(child)) {
          seenDefault = true;
          groups.push_back({child, true, {}, {}});
          currentGroup = &groups.back();
          if (ds->getSubStmt())
            currentGroup->body.push_back(ds->getSubStmt());
        } else if (currentGroup) {
          currentGroup->body.push_back(child);
        } else {
          // Statements before the first label are unreachable in C, but retain
          // the old behavior so malformed inputs still receive diagnostics.
          trStmt(stmts, child);
        }
      }

      // A switch whose cases all end in a direct break has no fall-through.
      // Emit it as one match and omit the terminal breaks.
      bool hasOnlyTerminalBreaks = !groups.empty();
      std::vector<SwitchGroup *> cases;
      SwitchGroup *defaultGroup = nullptr;
      for (auto &group : groups) {
        bool hasTerminalBreak =
            !group.body.empty() && isa<BreakStmt>(group.body.back());
        if (!hasTerminalBreak) {
          hasOnlyTerminalBreaks = false;
          break;
        }

        size_t bodySize = group.body.size() - 1;
        if (group.isDefault) {
          defaultGroup = &group;
        } else {
          cases.push_back(&group);
        }
        for (size_t i = 0; i < bodySize; i++) {
          if (containsSwitchBreak(containsSwitchBreak, group.body[i])) {
            hasOnlyTerminalBreaks = false;
            break;
          }
        }
        if (!hasOnlyTerminalBreaks)
          break;
      }

      if (hasOnlyTerminalBreaks && !cases.empty() && !switchEnss.empty()) {
        auto makeBody = [&](SwitchGroup &group) {
          auto bodyStmts = Vec<Rc<ir::Stmt>>::new_();
          size_t bodySize = group.body.size() - 1;
          for (size_t i = 0; i < bodySize; i++)
            trStmt(bodyStmts, group.body[i]);
          return bodyStmts;
        };

        bool canUseMatch = true;
        for (auto *group : cases) {
          for (auto *caseValue : group->caseValues) {
            Expr::EvalResult result;
            if (!caseValue->EvaluateAsInt(result, *astCtx) ||
                !result.Val.isInt()) {
              canUseMatch = false;
              break;
            }
          }
          if (!canUseMatch)
            break;
        }

        if (canUseMatch) {
          auto matchBranches = Vec<Rc<ir::MatchBranch>>::new_();
          for (auto *group : cases) {
            auto patterns = Vec<Rc<ir::Expr>>::new_();
            for (auto *caseValue : group->caseValues) {
              Expr::EvalResult result;
              bool evaluated = caseValue->EvaluateAsInt(result, *astCtx);
              assert(evaluated && result.Val.isInt());
              patterns.push(mk_int_lit(getRange(caseValue->getSourceRange()),
                                       toBigInt(result.Val.getInt()),
                                       scrutTy.clone()));
            }
            matchBranches.push(
                mk_match_branch(std::move(patterns), makeBody(*group)));
          }

          auto defaultBody = defaultGroup ? makeBody(*defaultGroup)
                                          : Vec<Rc<ir::Stmt>>::new_();
          auto matchEnss = Vec<Rc<ir::Expr>>::new_();
          auto combined = switchEnss.front().clone();
          for (size_t i = 1; i < switchEnss.size(); i++) {
            combined =
                mk_rvalue_binop(loc.clone(), ir::BinOp::LogAnd(),
                                std::move(combined), switchEnss[i].clone());
          }
          matchEnss.push(std::move(combined));
          stmts.push(mk_match(loc.clone(),
                              mk_lvalue_var(loc.clone(), scrutId.clone()),
                              std::move(matchBranches), std::move(defaultBody),
                              std::move(matchEnss)));
          return {};
        }
      }

      // General switches retain explicit hit and break state to model
      // fall-through.
      auto hitName = "__switch_hit_" + std::to_string(switchIndex);
      auto brkName = "__switch_brk_" + std::to_string(switchIndex);
      auto hitId = ctx.mk_ident(toStr(hitName), loc.clone());
      auto brkId = ctx.mk_ident(toStr(brkName), loc.clone());

      stmts.push(
          mk_var_decl(loc.clone(), hitId.clone(), mk_bool_type(loc.clone())));
      stmts.push(mk_assign(loc.clone(),
                           mk_lvalue_var(loc.clone(), hitId.clone()),
                           mk_bool_lit(loc.clone(), false)));
      stmts.push(
          mk_var_decl(loc.clone(), brkId.clone(), mk_bool_type(loc.clone())));
      stmts.push(mk_assign(loc.clone(),
                           mk_lvalue_var(loc.clone(), brkId.clone()),
                           mk_bool_lit(loc.clone(), false)));

      auto savedSwitchBreak = switchBreakId;
      switchBreakId = new Rc<ir::Ident>(brkId.clone());

      auto caseEnss = [&]() {
        auto enss = Vec<Rc<ir::Expr>>::new_();
        if (!switchEnss.empty()) {
          auto combined = switchEnss.front().clone();
          for (size_t i = 1; i < switchEnss.size(); i++) {
            combined =
                mk_rvalue_binop(loc.clone(), ir::BinOp::LogAnd(),
                                std::move(combined), switchEnss[i].clone());
          }
          combined = mk_rvalue_binop(
              loc.clone(), ir::BinOp::LogAnd(), std::move(combined),
              mk_live(loc.clone(), mk_lvalue_var(loc.clone(), hitId.clone())));
          combined = mk_rvalue_binop(
              loc.clone(), ir::BinOp::LogAnd(), std::move(combined),
              mk_live(loc.clone(), mk_lvalue_var(loc.clone(), brkId.clone())));
          enss.push(std::move(combined));
        }
        return enss;
      };

      for (auto &group : groups) {
        auto childLoc = getRange(group.label->getSourceRange());
        if (!group.isDefault) {
          // Build match condition: scrut == v1 || scrut == v2 || ...
          Rc<ir::Expr> matchCond = mk_bool_lit(childLoc.clone(), false);
          for (auto *cv : group.caseValues) {
            auto scrutRead = mk_lvalue_var(childLoc.clone(), scrutId.clone());
            auto caseVal = trRValue(cv->IgnoreParenImpCasts());
            auto eq = mk_rvalue_binop(childLoc.clone(), ir::BinOp::Eq(),
                                      std::move(scrutRead), std::move(caseVal));
            matchCond = mk_rvalue_binop(childLoc.clone(), ir::BinOp::LogOr(),
                                        std::move(matchCond), std::move(eq));
          }

          // Full condition: !brk && (hit || matchCond)
          auto notBrk = mk_rvalue_unop(
              childLoc.clone(), ir::UnOp::Not(),
              mk_rvalue_lvalue(childLoc.clone(),
                               mk_lvalue_var(childLoc.clone(), brkId.clone())));
          auto hitRead = mk_rvalue_lvalue(
              childLoc.clone(), mk_lvalue_var(childLoc.clone(), hitId.clone()));
          auto hitOrMatch =
              mk_rvalue_binop(childLoc.clone(), ir::BinOp::LogOr(),
                              std::move(hitRead), std::move(matchCond));
          auto cond = mk_rvalue_binop(childLoc.clone(), ir::BinOp::LogAnd(),
                                      std::move(notBrk), std::move(hitOrMatch));

          // Body: hit = true; case_stmts
          auto thenStmts = Vec<Rc<ir::Stmt>>::new_();
          thenStmts.push(mk_assign(
              childLoc.clone(), mk_lvalue_var(childLoc.clone(), hitId.clone()),
              mk_bool_lit(childLoc.clone(), true)));
          for (auto *bodyStmt : group.body)
            trStmt(thenStmts, bodyStmt);

          auto elseStmts = Vec<Rc<ir::Stmt>>::new_();
          stmts.push(mk_if(std::move(childLoc), std::move(cond),
                           std::move(thenStmts), std::move(elseStmts),
                           caseEnss()));

        } else {
          if (!switchCanBreak) {
            // With no break belonging to this switch, reaching default means
            // its body runs. Emitting it directly preserves terminating
            // returns without introducing an unnecessary conditional join.
            stmts.push(mk_assign(childLoc.clone(),
                                 mk_lvalue_var(childLoc.clone(), hitId.clone()),
                                 mk_bool_lit(childLoc.clone(), true)));
            for (auto *bodyStmt : group.body)
              trStmt(stmts, bodyStmt);
            continue;
          }
          // Condition: !brk
          auto notBrk = mk_rvalue_unop(
              childLoc.clone(), ir::UnOp::Not(),
              mk_rvalue_lvalue(childLoc.clone(),
                               mk_lvalue_var(childLoc.clone(), brkId.clone())));

          auto thenStmts = Vec<Rc<ir::Stmt>>::new_();
          thenStmts.push(mk_assign(
              childLoc.clone(), mk_lvalue_var(childLoc.clone(), hitId.clone()),
              mk_bool_lit(childLoc.clone(), true)));
          for (auto *bodyStmt : group.body)
            trStmt(thenStmts, bodyStmt);

          auto elseStmts = Vec<Rc<ir::Stmt>>::new_();
          stmts.push(mk_if(std::move(childLoc), std::move(notBrk),
                           std::move(thenStmts), std::move(elseStmts),
                           caseEnss()));
        }
      }

      delete switchBreakId;
      switchBreakId = savedSwitchBreak;
      return {};
    } else if (auto *f = dyn_cast<ForStmt>(stmt)) {
      // Desugar: for (init; cond; incr) body
      //      --> init; while (cond) { body; incr; }
      if (f->getInit())
        trStmt(stmts, f->getInit());

      auto cond = f->getCond() ? trRValue(f->getCond())
                               : mk_bool_lit(loc.clone(), true);

      auto body = f->getBody();
      auto invs = Vec<Rc<ir::Expr>>::new_();
      auto reqs = Vec<Rc<ir::Expr>>::new_();
      auto enss = Vec<Rc<ir::Expr>>::new_();
      if (auto attrBody = dyn_cast<AttributedStmt>(body)) {
        for (auto attr : attrBody->getAttrs()) {
          if (auto inv = isUnaryAttrOf(attr, "pal-invariant")) {
            invs.push(std::move(inv.value()));
          } else if (auto req = isUnaryAttrOf(attr, "pal-requires")) {
            reqs.push(std::move(req.value()));
          } else if (auto ens = isUnaryAttrOf(attr, "pal-ensures")) {
            enss.push(std::move(ens.value()));
          }
        }
        body = attrBody->getSubStmt();
      }

      auto savedIncrement = forLoopIncrement;
      forLoopIncrement = f->getInc();
      auto bodyStmts = trStmts(body);
      if (f->getInc())
        trStmt(bodyStmts, f->getInc());
      forLoopIncrement = savedIncrement;

      return stmts.push(mk_while(loc.clone(), std::move(cond), std::move(invs),
                                 std::move(reqs), std::move(enss),
                                 std::move(bodyStmts)));
    } else if (dyn_cast<BreakStmt>(stmt)) {
      if (switchBreakId) {
        // Inside a switch: set break flag instead of emitting break
        return stmts.push(mk_assign(
            loc.clone(), mk_lvalue_var(loc.clone(), switchBreakId->clone()),
            mk_bool_lit(std::move(loc), true)));
      }
      return stmts.push(mk_break(std::move(loc)));
    } else if (dyn_cast<ContinueStmt>(stmt)) {
      if (forLoopIncrement)
        trStmt(stmts, forLoopIncrement);
      return stmts.push(mk_continue(std::move(loc)));
    } else if (auto *r = dyn_cast<ReturnStmt>(stmt)) {
      if (auto *rv = r->getRetValue()) {
        return stmts.push(mk_return(std::move(loc), trRValue(rv)));
      } else {
        return stmts.push(mk_return_void(std::move(loc)));
      }
    } else if (auto *g = dyn_cast<GotoStmt>(stmt)) {
      auto label = ctx.mk_ident(toStr(g->getLabel()->getName()), loc.clone());
      return stmts.push(mk_goto(std::move(loc), std::move(label)));
    } else if (auto *ls = dyn_cast<LabelStmt>(stmt)) {
      auto label =
          ctx.mk_ident(toStr(llvm::StringRef(ls->getName())), loc.clone());
      auto enss = Vec<Rc<ir::Expr>>::new_();
      auto subStmt = ls->getSubStmt();
      // Clang attaches __attribute__ to the label decl
      auto labelDecl = ls->getDecl();
      if (labelDecl->hasAttrs()) {
        for (auto attr : labelDecl->getAttrs()) {
          if (auto ens = isUnaryAttrOf(attr, "pal-ensures")) {
            enss.push(std::move(ens.value()));
          }
        }
      }
      // Also check if sub-statement is AttributedStmt
      if (auto attrStmt = dyn_cast<AttributedStmt>(subStmt)) {
        for (auto attr : attrStmt->getAttrs()) {
          if (auto ens = isUnaryAttrOf(attr, "pal-ensures")) {
            enss.push(std::move(ens.value()));
          }
        }
        subStmt = attrStmt->getSubStmt();
      }
      stmts.push(mk_label(std::move(loc), std::move(label), std::move(enss)));
      return trStmt(stmts, subStmt);
    } else if (auto *ds = dyn_cast<DeclStmt>(stmt)) {
      for (auto d : ds->decls()) {
        auto dloc = getRange(d->getSourceRange());
        if (auto vd = dyn_cast<VarDecl>(d)) {
          auto id = ctx.mk_ident(toStr(vd->getName()), dloc.clone());
          auto qt = vd->getType();
          if (auto *vat =
                  dyn_cast<VariableArrayType>(qt.IgnoreParens().getTypePtr())) {
            auto elemTy =
                trQualType(vat->getElementType(), vd->getSourceRange());
            auto sizeExpr = trRValue(vat->getSizeExpr());
            stmts.push(mk_decl_stack_array(dloc.clone(), id.clone(),
                                           std::move(elemTy),
                                           std::move(sizeExpr)));
          } else {
            auto ty = trTypeAttrs(
                vd->getAttrs(),
                trQualType(vd->getType(), vd->getSourceRange(), nullptr,
                           findFnProtoTypeLoc(vd->getTypeSourceInfo())),
                vd->getType(), vd->getSourceRange());
            stmts.push(mk_var_decl(dloc.clone(), id.clone(), std::move(ty)));
            if (vd->hasInit()) {
              // The initializer is evaluated exactly once, with nothing else
              // in the expression to cross, so a statement expression in it
              // may put its statements here -- between the declaration and
              // the assignment.
              auto savedHoist = hoistTarget;
              hoistTarget = &stmts;
              auto init = trRValue(vd->getInit());
              hoistTarget = savedHoist;
              stmts.push(mk_assign(dloc.clone(),
                                   mk_lvalue_var(dloc.clone(), id.clone()),
                                   std::move(init)));
            }
          }
        } else if (auto fd = dyn_cast<FunctionDecl>(d); fd && !fd->hasBody()) {
          // C allows declaring a function in block scope: the K&R-era idiom of
          // declaring a library function locally instead of including its
          // header. The declared function is the same entity as one declared
          // at file scope, and the statement itself has no runtime effect, so
          // hoist the declaration out of the body. A body here would be a GNU
          // nested function, which can capture enclosing locals and hence
          // cannot be hoisted; that falls through to the error below.
          HandleDecl(fd);
        } else {
          reportUnsupported(d->getSourceRange(), dloc,
                            "unsupported variable declaration ",
                            d->getDeclKindName());
          stmts.push(mk_stmt_err(dloc.clone()));
        }
      }
      return rust::Unit();
    } else if (auto *p = dyn_cast<ParenExpr>(stmt)) {
      return trStmt(stmts, p->getSubExpr());
    } else if (auto *comp = dyn_cast<CompoundStmt>(stmt)) {
      // TODO: scope
      for (auto stmt : comp->body())
        trStmt(stmts, stmt);
      return rust::Unit();
    } else if (auto *c = dyn_cast<CallExpr>(stmt)) {
      // Intercept __pal_c_assert(expr) — translated from C assert()
      if (auto fd = c->getDirectCallee()) {
        if (fd->getName() == "__pal_c_assert" && c->getNumArgs() == 1) {
          auto val = trRValue(c->getArg(0));
          // Cast to bool — elab will convert to slprop via with_pure
          auto boolVal = mk_rvalue_cast(loc.clone(), std::move(val),
                                        mk_bool_type(loc.clone()));
          // Wrap in if (pal_c_assert_enabled()) to expose
          // side-effect differences when assertions are disabled.
          auto enabledFn = ctx.mk_ident(
              toStr(StringRef("pal_c_assert_enabled")), loc.clone());
          auto enabledArgs = Vec<Rc<ir::Expr>>::new_();
          auto enabledCall = mk_rvalue_fncall(loc.clone(), std::move(enabledFn),
                                              std::move(enabledArgs));
          auto thenStmts = Vec<Rc<ir::Stmt>>::new_();
          thenStmts.push(mk_assert(loc.clone(), std::move(boolVal)));
          auto elseStmts = Vec<Rc<ir::Stmt>>::new_();
          return stmts.push(mk_if(std::move(loc), std::move(enabledCall),
                                  std::move(thenStmts), std::move(elseStmts),
                                  Vec<Rc<ir::Expr>>::new_()));
        }
      }
      return stmts.push(mk_call(std::move(loc), trRValue(c)));
    } else if (auto *se = dyn_cast<StmtExpr>(stmt)) {
      // _assert(p) expands to ({ __attribute__((annotate("pal-assert",
      // ...))) {} })
      // _ghost_stmt(p) expands similarly with "pal-ghost-stmt"
      if (auto *comp = dyn_cast<CompoundStmt>(se->getSubStmt())) {
        for (auto s : comp->body()) {
          if (auto *attr = dyn_cast<AttributedStmt>(s)) {
            for (auto a : attr->getAttrs()) {
              if (auto val = isUnaryAttrOf(a, "pal-assert")) {
                stmts.push(mk_assert(loc.clone(), std::move(val.value())));
                return rust::Unit();
              }
              if (auto ctr = isUnaryAttrCounter(a, "pal-ghost-stmt")) {
                stmts.push(
                    ctx.mk_ghost_stmt(loc.clone(), ctr.value(), snippets));
                return rust::Unit();
              }
            }
          }
        }
      }
      // Any other statement expression, used where its value is discarded.
      //
      // `({ s1; s2; e; });` as a statement is exactly `{ s1; s2; e; }`: the
      // only thing a statement expression adds over a compound statement is
      // that it has a value, and in statement position that value is thrown
      // away.  So this arm is general -- it needs no restriction on the body
      // at all -- and it is where the GNU idiom mostly appears:
      // do-something-and-check macros expanded for their effect.
      //
      // The value-carrying case is handled in trRValue, where it does need a
      // restriction, because an rvalue has nowhere to put s1 and s2.
      return trStmt(stmts, se->getSubStmt());
    } else if (auto *attr = dyn_cast<AttributedStmt>(stmt)) {
      return trStmt(stmts, attr->getSubStmt());
    } else if (auto *cse = dyn_cast<CStyleCastExpr>(stmt)) {
      if (cse->getType()->isVoidType()) {
        // (void)expr — translate the sub-expression as a statement to
        // preserve any side effects (e.g. (void)x++).  Pure no-ops like
        // ((void)0) will naturally produce no IR.
        return trStmt(stmts, cse->getSubExpr());
      }
    } else if (auto *co = dyn_cast<ConditionalOperator>(stmt)) {
      if (auto *arm = constantCondArm(co)) {
        return trStmt(stmts, arm);
      }
      // `c ? a : b;` as a statement: the value is discarded, but a and b may
      // still do something, so this is an if/else -- not a no-op, and not an
      // rvalue, which is why it cannot go through trRValue.
      //
      // C code writes this when both arms are calls, which is how some
      // assert() implementations expand.  Each arm is translated in
      // statement position, so an arm that computes a discarded pure value
      // drops out on its own.
      auto thenStmts = Vec<Rc<ir::Stmt>>::new_();
      trStmt(thenStmts, co->getTrueExpr());
      auto elseStmts = Vec<Rc<ir::Stmt>>::new_();
      trStmt(elseStmts, co->getFalseExpr());
      return stmts.push(mk_if(std::move(loc), trRValue(co->getCond()),
                              std::move(thenStmts), std::move(elseStmts),
                              Vec<Rc<ir::Expr>>::new_()));
    } else if (dyn_cast<NullStmt>(stmt) || dyn_cast<IntegerLiteral>(stmt)) {
      return rust::Unit();
    }

    // An expression evaluated for a value that is then discarded, where
    // computing the value does nothing observable, is a no-op -- so drop it
    // rather than reporting it unsupported.
    //
    // C admits such statements (with a warning), and the GNU statement
    // expression makes them unavoidable: `({ s1; e; });` in statement
    // position *always* ends in one, because `e` is the construct's value and
    // the surrounding statement throws it away.  Without this, the general
    // statement-position arm above could not translate anything.
    //
    // `HasSideEffects` is clang's own answer, and it is conservative: a call,
    // an assignment, an increment, or a volatile read all count, and any of
    // them still reaches the diagnostic below.
    if (auto *ex = dyn_cast<Expr>(stmt)) {
      if (!ex->HasSideEffects(*astCtx)) {
        return rust::Unit();
      }
    }

    reportUnsupported(stmt->getSourceRange(), loc, "unsupported statement ",
                      stmt->getStmtClassName());
    return stmts.push(mk_stmt_err(std::move(loc)));
  }

  std::optional<Rc<ir::Expr>> isUnaryAttrOf(Attr const *attr,
                                            char const *name) {
    if (auto ann = dyn_cast<AnnotateAttr>(attr);
        ann && ann->args_size() == 1 && ann->getAnnotation() == name) {
      if (auto ctrVal = ann->args_begin()[0]->getIntegerConstantExpr(*astCtx)) {
        unsigned ctr = ctrVal->getZExtValue();
        return {ctx.parse_rvalue(getRange(attr->getRange()), ctr, snippets)};
      }
    }
    return {};
  }

  std::optional<unsigned> isUnaryAttrCounter(Attr const *attr,
                                             char const *name) {
    if (auto ann = dyn_cast<AnnotateAttr>(attr);
        ann && ann->args_size() == 1 && ann->getAnnotation() == name) {
      if (auto ctrVal = ann->args_begin()[0]->getIntegerConstantExpr(*astCtx)) {
        return {static_cast<unsigned>(ctrVal->getZExtValue())};
      }
    }
    return {};
  }

  rust::Unit HandleDecl(Decl *D) {
    if (auto *FD = dyn_cast<FunctionDecl>(D)) {
      // Include block
      if (FD->getName().starts_with("__pal_include_anchor")) {
        std::optional<unsigned> code;
        std::string modName;
        for (auto attr : FD->getAttrs()) {
          if (auto ann = dyn_cast<AnnotateAttr>(attr);
              ann && ann->getAnnotation() == "pal-includes" &&
              ann->args_size() == 2) {
            // First arg: string literal for module name
            if (auto strLit = dyn_cast<StringLiteral>(
                    ann->args_begin()[0]->IgnoreParenCasts())) {
              modName = strLit->getString().str();
            }
            // Second arg: __COUNTER__ for snippet index
            if (auto ctrVal =
                    ann->args_begin()[1]->getIntegerConstantExpr(*astCtx)) {
              unsigned ctr = ctrVal->getZExtValue();
              code = ctr;
            }
          }
        }
        auto loc = getRange(D->getSourceRange());
        if (code && !modName.empty()) {
          ctx.add_include(std::move(loc), toStr(modName), *code, snippets);
        } else {
          ctx.report_diag(std::move(loc), true,
                          "internal error: invalid INCLUDES encoding"_rs);
        }
        return {};
      }

      // Let decl block
      if (FD->getName().starts_with("__pal_let_anchor") ||
          FD->getName().starts_with("__pal_let_rec_anchor")) {
        bool is_rec = FD->getName().starts_with("__pal_let_rec_anchor");
        std::optional<unsigned> sig_ctr, body_ctr;
        for (auto attr : FD->getAttrs()) {
          if (auto ann = dyn_cast<AnnotateAttr>(attr);
              ann &&
              (ann->getAnnotation() == "pal-let" ||
               ann->getAnnotation() == "pal-let-rec") &&
              ann->args_size() == 2) {
            if (auto v0 =
                    ann->args_begin()[0]->getIntegerConstantExpr(*astCtx)) {
              sig_ctr = v0->getZExtValue();
            }
            if (auto v1 =
                    ann->args_begin()[1]->getIntegerConstantExpr(*astCtx)) {
              body_ctr = v1->getZExtValue();
            }
          }
        }
        auto loc = getRange(D->getSourceRange());
        if (sig_ctr && body_ctr) {
          ctx.add_let_decl(std::move(loc), is_rec, *sig_ctr, *body_ctr,
                           snippets);
        } else {
          ctx.report_diag(std::move(loc), true,
                          "internal error: invalid _let encoding"_rs);
        }
        return {};
      }

      // Let impure decl block
      if (FD->getName().starts_with("__pal_letimpure_anchor")) {
        std::optional<unsigned> sig_ctr, body_ctr;
        for (auto attr : FD->getAttrs()) {
          if (auto ann = dyn_cast<AnnotateAttr>(attr);
              ann && ann->getAnnotation() == "pal-letimpure" &&
              ann->args_size() == 2) {
            if (auto v0 =
                    ann->args_begin()[0]->getIntegerConstantExpr(*astCtx)) {
              sig_ctr = v0->getZExtValue();
            }
            if (auto v1 =
                    ann->args_begin()[1]->getIntegerConstantExpr(*astCtx)) {
              body_ctr = v1->getZExtValue();
            }
          }
        }
        auto loc = getRange(D->getSourceRange());
        if (sig_ctr && body_ctr) {
          ctx.add_letimpure_decl(std::move(loc), *sig_ctr, *body_ctr, snippets);
        } else {
          ctx.report_diag(std::move(loc), true,
                          "internal error: invalid _letimpure encoding"_rs);
        }
        return {};
      }

      // Type decl block
      if (FD->getName().starts_with("__pal_type_anchor")) {
        std::optional<unsigned> name_ctr, body_ctr;
        for (auto attr : FD->getAttrs()) {
          if (auto ann = dyn_cast<AnnotateAttr>(attr);
              ann && ann->getAnnotation() == "pal-type" &&
              ann->args_size() == 2) {
            if (auto v0 =
                    ann->args_begin()[0]->getIntegerConstantExpr(*astCtx)) {
              name_ctr = v0->getZExtValue();
            }
            if (auto v1 =
                    ann->args_begin()[1]->getIntegerConstantExpr(*astCtx)) {
              body_ctr = v1->getZExtValue();
            }
          }
        }
        auto loc = getRange(D->getSourceRange());
        if (name_ctr && body_ctr) {
          ctx.add_type_decl(std::move(loc), *name_ctr, *body_ctr, snippets);
        } else {
          ctx.report_diag(std::move(loc), true,
                          "internal error: invalid _type encoding"_rs);
        }
        return {};
      }

      // A `_memset_zero` wrapper is an intrinsic, not a function: every call
      // to it is rewritten to a whole-object zeroing, so emitting a module for
      // it would only add an uninterpreted stub that nothing calls. A
      // definition still translates normally -- the marker only claims what
      // calls mean, and a body present in this translation unit is code to be
      // verified like any other.
      {
        bool memsetZero = false;
        for (auto *attr : FD->getAttrs()) {
          if (auto *ann = dyn_cast<AnnotateAttr>(attr);
              ann && ann->getAnnotation() == "pal-memset-zero" &&
              ann->args_size() == 0) {
            memsetZero = true;
          }
        }
        if (memsetZero && !FD->hasBody()) {
          return {};
        }
      }

      // Regular function decl
      auto ident = getDeclName(FD);
      auto builder =
          DeclBuilder::new_(getRange(FD->getSourceRange()), ident.clone());
      for (auto param : FD->parameters()) {
        auto ty = trQualType(param->getType(), param->getSourceRange(), nullptr,
                             findFnProtoTypeLoc(param->getTypeSourceInfo()));
        ty = trTypeAttrs(param->getAttrs(), std::move(ty), param->getType(),
                         param->getSourceRange());
        auto mode = hasConsumesAttr(param->getAttrs())
                        ? ir::ParamMode::Consumed()
                    : hasOutAttr(param->getAttrs())
                        ? ir::ParamMode::Out()
                        : [&]() {
                            auto qt = param->getType().IgnoreParens();
                            if (hasCoreRefAttr(param->getAttrs()) ||
                                isCoreRefQualType(param->getType()))
                              return ir::ParamMode::Regular();
                            // A top-level `const` on a parameter passed by
                            // value says nothing about ownership: the callee
                            // gets its own copy, and the qualifier only
                            // forbids reassigning the local. Reading it as a
                            // borrow gives the parameter a permission
                            // implicit, and for a scalar -- whose ownership
                            // predicate is `emp` -- nothing at the call site
                            // can ever solve it, so the call does not
                            // elaborate. Only an indirection can be borrowed.
                            if (qt.getCanonicalType()->isPointerType() &&
                                qt.getCanonicalType().isConstQualified())
                              return ir::ParamMode::Const();
                            // `getAs` desugars through typedefs, so a
                            // parameter declared with a pointer-to-const
                            // typedef (`PCFOO`) is recognized just
                            // like one that writes `const T *` through.
                            if (auto ptr = qt->getAs<PointerType>()) {
                              if (ptr->getPointeeType()
                                      .getCanonicalType()
                                      .isConstQualified())
                                return ir::ParamMode::Const();
                            }
                            return ir::ParamMode::Regular();
                          }();
        if (param->getDeclName().isIdentifier() &&
            param->getName().size() > 0) {
          builder.arg(ctx.mk_ident(toStr(param->getName()),
                                   getRange(param->getSourceRange())),
                      std::move(ty), std::move(mode));
        } else {
          builder.arg_anon(std::move(ty), std::move(mode));
        }
      }
      builder.return_type(trTypeAttrs(
          FD->getAttrs(),
          trQualType(FD->getReturnType(), FD->getReturnTypeSourceRange()),
          FD->getReturnType(), FD->getReturnTypeSourceRange()));
      for (auto attr : FD->getAttrs()) {
        if (FD->hasBody() && attr->isInherited())
          continue;
        if (auto req = isUnaryAttrOf(attr, "pal-requires")) {
          builder.requires(std::move(req.value()));
        }
        if (auto ens = isUnaryAttrOf(attr, "pal-ensures")) {
          builder.ensures(std::move(ens.value()));
        }
        if (auto dec = isUnaryAttrOf(attr, "pal-decreases")) {
          builder.decreases(std::move(dec.value()));
        }
        if (auto ann = dyn_cast<AnnotateAttr>(attr);
            ann && ann->getAnnotation() == "pal-pure" &&
            ann->args_size() == 0) {
          builder.set_pure();
        }
        if (auto ann = dyn_cast<AnnotateAttr>(attr);
            ann && ann->getAnnotation() == "pal-rec" && ann->args_size() == 0) {
          builder.set_rec();
        }
        if (auto ann = dyn_cast<AnnotateAttr>(attr);
            ann && ann->getAnnotation() == "pal-total" &&
            ann->args_size() == 0) {
          builder.set_total();
        }
        if (auto ctr = isUnaryAttrCounter(attr, "pal-ghost-arg")) {
          ctx.parse_ghost_arg(builder, getRange(attr->getRange()), ctr.value(),
                              snippets);
        }
      }
      if (FD->hasBody()) {
        return ctx.add_fn_defn(std::move(builder), trStmts(FD->getBody()));
      } else {
        return ctx.add_fn_decl(std::move(builder));
      }
    } else if (auto *TD = dyn_cast<TypedefDecl>(D)) {
      auto loc = getRange(TD->getSourceRange());
      auto id = ctx.mk_ident(toStr(TD->getName()), loc.clone());
      auto anon = AnonNameGen(TD->getName());
      auto type =
          trQualType(TD->getUnderlyingType(), TD->getSourceRange(), &anon,
                     findFnProtoTypeLoc(TD->getTypeSourceInfo()));
      type = trTypeAttrs(TD->getAttrs(), std::move(type));
      bool isPointerView = false;
      if (TD->hasAttrs()) {
        for (auto *attr : TD->getAttrs()) {
          if (auto *ann = dyn_cast<AnnotateAttr>(attr)) {
            if (ann->getAnnotation() == "pal-pointer-view" &&
                ann->args_size() == 0) {
              isPointerView = true;
            }
          }
        }
      }
      return ctx.add_typedef(std::move(loc), std::move(id), std::move(type),
                             isPointerView);
    } else if (auto *RD = dyn_cast<RecordDecl>(D)) {
      auto loc = getRange(RD->getSourceRange());
      if (RD->getIdentifier()) {
        auto id = ctx.mk_ident(toStr(RD->getName()), loc.clone());
        auto anon = AnonNameGen(RD->getName());
        trRecordDecl(std::move(id), RD, &anon);
      } else {
        // TODO: forward struct decls
      }
      return {};
    } else if (auto *VD = dyn_cast<VarDecl>(D)) {
      auto loc = getRange(VD->getSourceRange());
      auto id = ctx.mk_ident(toStr(VD->getName()), loc.clone());
      auto ty = trQualType(VD->getType(), VD->getSourceRange(), nullptr,
                           findFnProtoTypeLoc(VD->getTypeSourceInfo()));
      OptExpr init = VD->hasInit() ? OptExpr::Some(trRValue(VD->getInit()))
                                   : OptExpr::None();
      // Purity is immutability, which is a property of the type alone. Whether
      // the value is *known here* is a separate question, answered by `init`
      // and `is_extern` below.
      bool is_pure = VD->getType().isConstQualified();
      // Whether the object is defined in another translation unit. Asked of
      // the whole redeclaration chain in this one, so an `extern` declaration
      // that this file also defines is not external. This is what separates
      // `extern const T g;`, whose value is unknown, from the tentative
      // definition `const T g;`, which is initialized as if by 0 (C17
      // 6.9.2p2); neither carries an initializer. Files that only declare the
      // object report it as external, and `merge` combines that with the file
      // that defines it, if the build has one.
      bool is_extern = VD->hasDefinition(*astCtx) == VarDecl::DeclarationOnly;
      bool opaque_to_smt = false;
      for (auto attr : VD->getAttrs()) {
        if (auto ann = dyn_cast<AnnotateAttr>(attr);
            ann && ann->getAnnotation() == "pal-pure" &&
            ann->args_size() == 0) {
          is_pure = true;
        }
        if (auto ann = dyn_cast<AnnotateAttr>(attr);
            ann && ann->getAnnotation() == "pal-opaque-to-smt" &&
            ann->args_size() == 0) {
          opaque_to_smt = true;
        }
      }
      return ctx.add_global_var(std::move(loc), std::move(id), std::move(ty),
                                std::move(init), is_pure, is_extern,
                                opaque_to_smt,
                                /*is_enum_constant=*/false);
    } else if (auto *ED = dyn_cast<EnumDecl>(D)) {
      // Enum declarations need no IR representation of their own; Clang inlines
      // enumerators as integer literals wherever they appear in a *body*.
      //
      // Contracts are different: they are raw source snippets that PAL parses
      // itself, so Clang never sees those uses and an enumerator there is just
      // an unresolved name. Publish each enumerator as a pure global constant
      // so contracts can name it rather than repeat its value. Enumerators
      // reached through a header are dropped again by the pruner unless a
      // contract actually mentions them.
      for (auto *ecd : ED->enumerators()) {
        auto ecdLoc = getRange(ecd->getSourceRange());
        auto ecdId = ctx.mk_ident(toStr(ecd->getName()), ecdLoc.clone());
        auto ecdQt = ecd->getType();
        if (ecdQt.isNull())
          continue;
        auto ecdTy = trQualType(ecdQt, ecd->getSourceRange());
        const auto val = ecd->getInitVal();
        SmallString<20> valStr;
        val.toString(valStr, 10, val.isSigned());
        auto lit =
            mk_int_lit(ecdLoc.clone(), mk_bigint(toStr(StringRef(valStr))),
                       trQualType(ecdQt, ecd->getSourceRange()));
        ctx.add_global_var(std::move(ecdLoc), std::move(ecdId),
                           std::move(ecdTy), OptExpr::Some(std::move(lit)),
                           /*is_pure=*/true,
                           // An enumerator is defined right here, never in
                           // another translation unit.
                           /*is_extern=*/false,
                           /*opaque_to_smt=*/false,
                           /*is_enum_constant=*/true);
      }
      return {};
    } else if (dyn_cast<EmptyDecl>(D)) {
      return {};
    } else if (dyn_cast<StaticAssertDecl>(D)) {
      // _Static_assert / static_assert — compile-time check already
      // enforced by Clang; no Pulse representation needed.
      return {};
    } else if (dyn_cast<FileScopeAsmDecl>(D)) {
      reportUnsupported(D->getSourceRange(), getRange(D->getSourceRange()),
                        "file-scope assembly is not translated", "");
      return {};
    }

    reportUnsupported(D->getSourceRange(), getRange(D->getSourceRange()),
                      "unsupported declaration ", D->getDeclKindName());
    return {};
  }
};

class PALAction : public SyntaxOnlyAction {
public:
  PALAction(RefMut<Ctx> c, RangeMap &m) : ctx(c), rangeMap(m) {}
  RefMut<Ctx> ctx;
  RangeMap &rangeMap;
  SnipMap snippets = SnipMap::default_();

  bool BeginSourceFileAction(CompilerInstance &CI) override {
    CI.getPreprocessor().addPPCallbacks(
        std::make_unique<MacroTracker>(rangeMap, snippets, CI));
    return SyntaxOnlyAction::BeginSourceFileAction(CI);
  }

  std::unique_ptr<ASTConsumer> CreateASTConsumer(CompilerInstance &CI,
                                                 StringRef InFile) override {
    return std::make_unique<PALConsumer>(ctx, rangeMap, snippets, CI);
  }

  void EndSourceFileAction() override {
    SyntaxOnlyAction::EndSourceFileAction();
  }
};

class PALActionFactory : public FrontendActionFactory {
public:
  PALActionFactory(RefMut<Ctx> c, RangeMap &m) : ctx(c), rangeMap(m) {}

  std::unique_ptr<FrontendAction> create() override {
    return std::make_unique<PALAction>(ctx, rangeMap);
  }

  RefMut<Ctx> ctx;
  RangeMap &rangeMap;
};

class PALDiagnosticConsumer : public DiagnosticConsumer {
public:
  PALDiagnosticConsumer(RefMut<Ctx> c, RangeMap &m) : ctx(c), rangeMap(m) {}
  RefMut<Ctx> ctx;
  RangeMap &rangeMap;

  void HandleDiagnostic(DiagnosticsEngine::Level DiagLevel,
                        const Diagnostic &Info) override {
    if (!Info.hasSourceManager())
      return;
    auto &sm = Info.getSourceManager();

    SourceLocation begin, end;

    if (Info.getNumRanges() > 0) {
      auto range = Info.getRange(0);
      begin = range.getBegin();
      end = range.getEnd();
    } else if (Info.getLocation().isValid()) {
      begin = Info.getLocation();
      end = begin;
    } else {
      return;
    }

    auto file_name =
        rangeMap.getFileName(sm, sm.getFileID(sm.getExpansionLoc(begin)));
    unsigned begin_line = sm.getExpansionLineNumber(begin);
    unsigned begin_col = sm.getExpansionColumnNumber(begin);
    unsigned end_line = sm.getExpansionLineNumber(end);
    unsigned end_col = sm.getExpansionColumnNumber(end);
    if (end_line == 0 || end_col == 0) {
      end_line = begin_line;
      end_col = begin_col;
    }
    llvm::SmallString<0> out;
    Info.FormatDiagnostic(out);
    ctx.report_diag(mk_original_location(std::move(file_name), begin_line,
                                         begin_col, end_line, end_col),
                    DiagLevel >= DiagnosticsEngine::Level::Error, toStr(out));
  }
};

#if LLVM_VERSION_MAJOR < 22
#define GetResourcesPath clang::driver::Driver::GetResourcesPath
#endif

std::string getBinaryForResourcesPath() {
  Dl_info info;
  if (dladdr((void *)static_cast<std::string (*)(StringRef)>(&GetResourcesPath),
             &info)) {
    return info.dli_fname;
  } else {
    return "/usr/bin/clang";
  }
}

std::string getResourcesPath() {
  return GetResourcesPath(getBinaryForResourcesPath());
}

llvm::vfs::Status mkStatus(Ref<rust::pal::vfs::VFSEntry> entry) {
  auto fileName = entry.get_file_name();
  llvm::sys::fs::UniqueID unique(0, (uint64_t)fileName.as_ptr());
  llvm::sys::TimePoint<> time;
  return llvm::vfs::Status(
      toStringRef(fileName), unique, time, 0, 0, entry.get_contents().len(),
      llvm::sys::fs::file_type::regular_file, llvm::sys::fs::perms::all_all);
}

class CtxVFSFile : public llvm::vfs::File {
  Rc<rust::pal::vfs::VFSEntry> entry;

public:
  CtxVFSFile(Rc<rust::pal::vfs::VFSEntry> &&e) : entry(std::move(e)) {}

  llvm::ErrorOr<llvm::vfs::Status> status() override {
    return mkStatus(entry.deref());
  }

  llvm::ErrorOr<std::unique_ptr<llvm::MemoryBuffer>>
  getBuffer(const Twine &Name, int64_t FileSize = -1,
            bool RequiresNullTerminator = true,
            bool IsVolatile = false) override {
    if (!RequiresNullTerminator)
      return llvm::MemoryBuffer::getMemBuffer(
          toStringRef(entry.deref().get_contents()),
          toStringRef(entry.deref().get_file_name()));

    return llvm::MemoryBuffer::getMemBufferCopy(
        toStringRef(entry.deref().get_contents()),
        toStringRef(entry.deref().get_file_name()));
  };

  std::error_code close() override { return {}; }

  llvm::ErrorOr<std::string> getName() override {
    return toString(entry.deref().get_file_name());
  }
};

class CtxVFS : public llvm::vfs::FileSystem {
  RefMut<Ctx> ctx;
  IntrusiveRefCntPtr<llvm::vfs::FileSystem> realFS;

public:
  CtxVFS(RefMut<Ctx> c) : ctx(c), realFS(llvm::vfs::getRealFileSystem()) {}

  static IntrusiveRefCntPtr<llvm::vfs::FileSystem> make(RefMut<Ctx> ctx) {
    return llvm::makeIntrusiveRefCnt<CtxVFS>(ctx);
  }

  llvm::ErrorOr<llvm::vfs::Status> status(const Twine &Path) override {
    auto res = ctx.read_vfs_file(toStr(Path.str()));
    if (!res.is_ok()) {
      // TODO: fallback for directories
      return realFS->status(Path);
    }
    return mkStatus(res.unwrap().deref());
  };

  llvm::ErrorOr<std::unique_ptr<llvm::vfs::File>>
  openFileForRead(const Twine &Path) override {
    auto res = ctx.read_vfs_file(toStr(Path.str()));
    if (!res.is_ok()) {
      return llvm::errc::no_such_file_or_directory;
    }
    return std::make_unique<CtxVFSFile>(res.unwrap());
  }

  llvm::vfs::directory_iterator dir_begin(const Twine &Dir,
                                          std::error_code &EC) override {
    return realFS->dir_begin(Dir, EC);
  }

  std::error_code setCurrentWorkingDirectory(const Twine &Path) override {
    return realFS->setCurrentWorkingDirectory(Path);
  }

  llvm::ErrorOr<std::string> getCurrentWorkingDirectory() const override {
    return realFS->getCurrentWorkingDirectory();
  }

  std::error_code getRealPath(const Twine &Path,
                              SmallVectorImpl<char> &Output) override {
    // TODO: implement using VFS
    return realFS->getRealPath(Path, Output);
  }

  bool exists(const Twine &Path) override {
    auto res = ctx.read_vfs_file(toStr(Path.str()));
    if (res.is_ok())
      return true;

    // TODO: fallback for directories
    return realFS->exists(Path);
  }

  std::error_code isLocal(const Twine &Path, bool &Result) override {
    Result = true;
    return {};
  }

  std::error_code makeAbsolute(SmallVectorImpl<char> &Path) const override {
    // TODO: implement using VFS
    return realFS->makeAbsolute(Path);
  }
};

static void parse_file(RefMut<Ctx> ctx) {
  std::string fileName = toString(ctx.get_input_file_name());
  std::vector<std::string> sourcePathList{fileName};

  std::string compDBErrMsg;
  auto compDB =
      CompilationDatabase::autoDetectFromSource(fileName, compDBErrMsg);
  std::vector<std::string> argsForCompDB;
  if (!compDB) {
    compDB = std::make_unique<FixedCompilationDatabase>(".", argsForCompDB);
  }

  ClangTool Tool(*compDB, sourcePathList,
                 std::make_shared<PCHContainerOperations>(), CtxVFS::make(ctx));

  RangeMap rangeMap(ctx);
  PALDiagnosticConsumer consumer(ctx, rangeMap);
  Tool.setDiagnosticConsumer(&consumer);

  // Tool.appendArgumentsAdjuster(OptionsParser->getArgumentsAdjuster());

  // On macOS, _FORTIFY_SOURCE is set to 2 by default, hence all libc functions
  // will be rewritten into calls the translator does not model.
  Tool.appendArgumentsAdjuster(getInsertArgumentAdjuster(
      {"-DC2PULSE", "-fno-builtin", "-D_FORTIFY_SOURCE=0"},
      ArgumentInsertPosition::BEGIN));
  Tool.appendArgumentsAdjuster(getInsertArgumentAdjuster(
      {"-Wno-unused-but-set-variable", "-Wno-unused-variable"},
      ArgumentInsertPosition::END));
  Tool.appendArgumentsAdjuster(getInsertArgumentAdjuster(
      {"-resource-dir", getResourcesPath()}, ArgumentInsertPosition::BEGIN));

  // Add user-specified include paths and preprocessor definitions.
  //
  // Each adjuster inserts at BEGIN, so applying them in forward order would
  // reverse the user's ordering and make the *last* -I win. Include path order
  // is significant -- it is what lets a caller shadow a project header -- so we
  // walk backwards, leaving the final argv in the order the user gave.
  //
  // Defines are inserted before the include paths are prepended, so they end up
  // after them in argv; -D and -I do not interact, so relative order is
  // immaterial. What matters is that both precede the source file.
  size_t defineCount = ctx.get_define_count();
  for (size_t i = defineCount; i-- > 0;) {
    std::string def = "-D" + toString(ctx.get_define(i));
    Tool.appendArgumentsAdjuster(
        getInsertArgumentAdjuster(def.c_str(), ArgumentInsertPosition::BEGIN));
  }

  size_t includePathCount = ctx.get_include_path_count();
  for (size_t i = includePathCount; i-- > 0;) {
    std::string incPath = "-I" + toString(ctx.get_include_path(i));
    Tool.appendArgumentsAdjuster(getInsertArgumentAdjuster(
        incPath.c_str(), ArgumentInsertPosition::BEGIN));
  }

  PALActionFactory factory(ctx, rangeMap);
  Tool.run(&factory);
}

namespace rust::exported_functions {
Unit parse_file(RefMut<Ctx> ctx) {
  ::parse_file(ctx);
  return {};
}
} // namespace rust::exported_functions