From 1294ac891a1c885289bbaf17c893fa1ca6ca2766 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 22:10:06 +0530 Subject: [PATCH 1/6] verify: Validate each term that a module's roots share once. --- clang/lib/Verify/Backend/Obligation.cpp | 357 ++++++++++++++++++++---- 1 file changed, 301 insertions(+), 56 deletions(-) diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp index fa36569e16..63cb5ca057 100644 --- a/clang/lib/Verify/Backend/Obligation.cpp +++ b/clang/lib/Verify/Backend/Obligation.cpp @@ -3,7 +3,10 @@ #include "ObligationLowering.h" #include "SpecAxioms.h" #include "llvm/ADT/APInt.h" +#include "llvm/ADT/DenseMap.h" +#include "llvm/ADT/DenseSet.h" #include "llvm/ADT/SmallString.h" +#include "llvm/ADT/StringMap.h" #include "llvm/ADT/StringRef.h" #include "llvm/Support/Error.h" #include @@ -552,7 +555,12 @@ static bool validateSource(const ObligationSource &Source, std::string &Error) { return true; } -static bool validateLogicExpr(const LogicExpr *Expr, std::string &Error) { +static bool +validateLogicExpr(const LogicExpr *Expr, std::string &Error, + llvm::DenseSet *Valid = nullptr); + +static bool validateLogicNode(const LogicExpr *Expr, std::string &Error, + llvm::DenseSet *Valid) { if (!Expr) { Error = "null term in obligation IR"; return false; @@ -585,7 +593,7 @@ static bool validateLogicExpr(const LogicExpr *Expr, std::string &Error) { return false; } for (const auto &Child : Expr->Children) - if (!validateLogicExpr(Child.get(), Error)) + if (!validateLogicExpr(Child.get(), Error, Valid)) return false; auto requireArity = [&](unsigned Minimum, unsigned Maximum) { @@ -990,6 +998,19 @@ static bool validateLogicExpr(const LogicExpr *Expr, std::string &Error) { return false; } +/// With \p Valid, a term in it is not checked again, and a term that passes +/// joins it: the goals of a module share the terms of their assumptions. +static bool validateLogicExpr(const LogicExpr *Expr, std::string &Error, + llvm::DenseSet *Valid) { + if (Valid && Valid->contains(Expr)) + return true; + if (!validateLogicNode(Expr, Error, Valid)) + return false; + if (Valid) + Valid->insert(Expr); + return true; +} + static void collectQuantifierBinders(const LogicExpr *Expr, std::set &Binders) { if (!Expr) @@ -1042,13 +1063,6 @@ static bool validateVariableScopes( return true; } -static bool validateVariableScopes(const LogicExpr *Expr, std::string &Error) { - std::set Binders; - collectQuantifierBinders(Expr, Binders); - std::map FreeVariables; - return validateVariableScopes(Expr, Binders, {}, FreeVariables, Error); -} - static bool validateVariableScopes(const LogicExpr *Expr, std::map &FreeVariables, @@ -1058,6 +1072,181 @@ validateVariableScopes(const LogicExpr *Expr, return validateVariableScopes(Expr, Binders, {}, FreeVariables, Error); } +namespace { +/// The quantifier binders of each term of a module, and the binder names +/// free in it, as interned sets, computed once for each term the module's +/// roots share. Every binder name of the module is registered before a free +/// set is computed, so a free set holds every binder name of its term's root +/// that occurs free in the term. +class BinderSummaries { +public: + explicit BinderSummaries(llvm::ArrayRef Roots) { + for (const LogicExpr *Root : Roots) + bindersOf(Root); + Complete = true; + } + + bool covers(const LogicExpr *Root) const { return Binders.count(Root); } + + std::optional nameId(llvm::StringRef Name) const { + auto It = Names.find(Name); + if (It == Names.end()) + return std::nullopt; + return It->second; + } + + unsigned bindersOf(const LogicExpr *Expr) { + if (!Expr) + return 0; + if (auto It = Binders.find(Expr); It != Binders.end()) + return It->second; + unsigned Set = 0; + if (Expr->K == LogicExpr::Forall || Expr->K == LogicExpr::Exists) + Set = + with(0, Names.try_emplace(Expr->Binder, Names.size()).first->second); + for (const auto &Child : Expr->Children) + Set = unite(Set, bindersOf(Child.get())); + Binders[Expr] = Set; + return Set; + } + + unsigned freeBindersOf(const LogicExpr *Expr) { + assert(Complete && "binder names are registered first"); + if (!Expr) + return 0; + if (auto It = FreeBinders.find(Expr); It != FreeBinders.end()) + return It->second; + unsigned Set = 0; + if (Expr->K == LogicExpr::Var) + if (auto Id = nameId(Expr->Name)) + Set = with(0, *Id); + for (const auto &Child : Expr->Children) + Set = unite(Set, freeBindersOf(Child.get())); + if (Expr->K == LogicExpr::Forall || Expr->K == LogicExpr::Exists) + Set = without(Set, *nameId(Expr->Binder)); + FreeBinders[Expr] = Set; + return Set; + } + + bool contains(unsigned Set, unsigned Name) const { + return std::binary_search(Sets[Set].begin(), Sets[Set].end(), Name); + } + + bool meet(unsigned Left, unsigned Right) const { + for (unsigned Name : Sets[Left]) + if (contains(Right, Name)) + return true; + return false; + } + + unsigned with(unsigned Set, unsigned Name) { + if (contains(Set, Name)) + return Set; + std::vector Members = Sets[Set]; + Members.insert(llvm::lower_bound(Members, Name), Name); + return intern(std::move(Members)); + } + +private: + llvm::StringMap Names; + std::vector> Sets{{}}; + std::map, unsigned> SetIds{{{}, 0}}; + llvm::DenseMap, unsigned> Unions; + llvm::DenseMap Binders; + llvm::DenseMap FreeBinders; + bool Complete = false; + + unsigned intern(std::vector Members) { + auto [It, Inserted] = SetIds.try_emplace(Members, Sets.size()); + if (Inserted) + Sets.push_back(std::move(Members)); + return It->second; + } + + unsigned unite(unsigned Left, unsigned Right) { + if (Left == Right || Right == 0) + return Left; + if (Left == 0) + return Right; + auto Key = std::minmax(Left, Right); + if (auto It = Unions.find(Key); It != Unions.end()) + return It->second; + std::vector Members; + std::set_union(Sets[Left].begin(), Sets[Left].end(), Sets[Right].begin(), + Sets[Right].end(), std::back_inserter(Members)); + unsigned Set = intern(std::move(Members)); + Unions[Key] = Set; + return Set; + } + + unsigned without(unsigned Set, unsigned Name) { + if (!contains(Set, Name)) + return Set; + std::vector Members = Sets[Set]; + Members.erase(llvm::lower_bound(Members, Name)); + return intern(std::move(Members)); + } +}; + +/// validateVariableScopes for the terms of one module against one map of +/// free variables, visiting a shared term once for each set of binders in +/// scope at it. Every check is the reference one's: a visit checks the sort +/// of each bound occurrence and registers each free one, and the summaries +/// decide whether a free variable is named as a binder of its root. A root +/// that fails either is checked again by validateVariableScopes for the +/// reference's error. The visit registered each name new to the map with the +/// sort of its first occurrence in the root, as the reference does, so the +/// reference finds what it would have found without the visit. +class ScopeValidator { +public: + ScopeValidator(BinderSummaries &Summaries, + std::map &FreeVariables) + : Summaries(Summaries), FreeVariables(FreeVariables) {} + + bool validate(const LogicExpr *Root, std::string &Error) { + const bool Covered = Summaries.covers(Root); + if (Covered && visit(Root, 0) && + !Summaries.meet(Summaries.bindersOf(Root), + Summaries.freeBindersOf(Root))) + return true; + const bool Valid = validateVariableScopes(Root, FreeVariables, Error); + assert((!Covered || !Valid) && + "the summaries reject only what the reference rejects"); + return Valid; + } + +private: + BinderSummaries &Summaries; + std::map &FreeVariables; + llvm::DenseSet> Visited; + + bool visit(const LogicExpr *Expr, unsigned Bound) { + if (!Expr) + return false; + if (Expr->K == LogicExpr::Forall || Expr->K == LogicExpr::Exists) + Bound = Summaries.with(Bound, *Summaries.nameId(Expr->Binder)); + if (Visited.contains({Expr, Bound})) + return true; + if (Expr->K == LogicExpr::Var) { + auto Id = Summaries.nameId(Expr->Name); + if (Id && Summaries.contains(Bound, *Id)) { + if (Expr->Sort.Kind != LogicSortKind::MathematicalInteger) + return false; + } else { + auto [It, Inserted] = FreeVariables.emplace(Expr->Name, Expr->Sort); + if (!Inserted && !equivalentVariableSort(It->second, Expr->Sort)) + return false; + } + } + for (const auto &Child : Expr->Children) + if (!visit(Child.get(), Bound)) + return false; + Visited.insert({Expr, Bound}); + return true; + } +}; +} // namespace + static bool canCoerceLogicSort(const LogicSort &Source, const LogicSort &Target) { if (Source.Kind == Target.Kind) @@ -1073,11 +1262,18 @@ static bool canCoerceLogicSort(const LogicSort &Source, static bool validateLogicCalls(const LogicExpr *Expr, const std::map &Functions, - std::string &Error) { + std::string &Error, + llvm::DenseSet *Checked = nullptr); + +static bool +validateLogicCall(const LogicExpr *Expr, + const std::map &Functions, + std::string &Error, + llvm::DenseSet *Checked) { if (!Expr) return false; for (const auto &Child : Expr->Children) - if (!validateLogicCalls(Child.get(), Functions, Error)) + if (!validateLogicCalls(Child.get(), Functions, Error, Checked)) return false; if (Expr->K != LogicExpr::SpecCall) return true; @@ -1104,6 +1300,21 @@ validateLogicCalls(const LogicExpr *Expr, return true; } +/// With \p Checked, as validateLogicExpr with its set. +static bool +validateLogicCalls(const LogicExpr *Expr, + const std::map &Functions, + std::string &Error, + llvm::DenseSet *Checked) { + if (Checked && Checked->contains(Expr)) + return true; + if (!validateLogicCall(Expr, Functions, Error, Checked)) + return false; + if (Checked) + Checked->insert(Expr); + return true; +} + static bool validateDefinitionVariables(const LogicExpr *Expr, const std::map &Parameters, @@ -1132,9 +1343,11 @@ validateDefinitionVariables(const LogicExpr *Expr, return true; } -static void collectRequiredFeatures(const LogicExpr *Expr, - LogicFeatureSet &Features) { - if (!Expr) +/// With \p Seen, the features of a term in it are already in \p Features. +static void +collectRequiredFeatures(const LogicExpr *Expr, LogicFeatureSet &Features, + llvm::DenseSet *Seen = nullptr) { + if (!Expr || (Seen && !Seen->insert(Expr).second)) return; switch (Expr->Sort.Kind) { case LogicSortKind::MathematicalInteger: @@ -1175,7 +1388,7 @@ static void collectRequiredFeatures(const LogicExpr *Expr, if (Expr->K == VCExpr::SpecCall) Features |= logicFeature(LogicFeature::SpecFunctions); for (const auto &Child : Expr->Children) - collectRequiredFeatures(Child.get(), Features); + collectRequiredFeatures(Child.get(), Features, Seen); } class ObligationBuilder { @@ -2347,6 +2560,36 @@ verify::validateObligationModule(const ObligationModule &M) { std::string ValidationError; std::set StableObligationIds; std::map ModuleVariables; + // The goals share the terms of their assumptions, so each check visits a + // shared term once. + llvm::DenseSet WellFormed, CallsChecked, FeaturesSeen; + std::vector Roots; + for (const DiagnosticTraceEvent &Event : M.TraceEvents) { + Roots.push_back(Event.Guard.get()); + for (const DiagnosticTraceValue &Value : Event.Values) + Roots.push_back(Value.Value.get()); + } + Roots.push_back(M.CorrectnessGoal.get()); + Roots.push_back(M.CounterexampleQuery.get()); + for (const Obligation &Item : M.Obligations) { + Roots.push_back(Item.Goal.get()); + Roots.push_back(Item.CounterexampleQuery.get()); + } + for (const auto &Entry : M.LogicFunctions) { + const LogicFunctionDecl &Declaration = Entry.second; + Roots.push_back(Declaration.StepDefinition.get()); + for (const auto &Definition : Declaration.DefinitionLevels) + Roots.push_back(Definition.get()); + for (const auto &Measure : Declaration.Decreases) + Roots.push_back(Measure.get()); + } + BinderSummaries Binders(Roots); + ScopeValidator ModuleScopes(Binders, ModuleVariables); + auto definitionScopes = [&](const LogicExpr *Expr) { + std::map FreeVariables; + return ScopeValidator(Binders, FreeVariables) + .validate(Expr, ValidationError); + }; for (const auto &[InternalName, Variable] : M.DiagnosticVariables) { if (InternalName.empty() || Variable.DisplayName.empty() || containsEmbeddedNul(InternalName) || @@ -2374,49 +2617,46 @@ verify::validateObligationModule(const ObligationModule &M) { if (!validateSource(Event.Source, ValidationError)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); - if (!validateLogicExpr(Event.Guard.get(), ValidationError) || + if (!validateLogicExpr(Event.Guard.get(), ValidationError, &WellFormed) || !validateLogicCalls(Event.Guard.get(), M.LogicFunctions, - ValidationError) || - !validateVariableScopes(Event.Guard.get(), ModuleVariables, - ValidationError) || + ValidationError, &CallsChecked) || + !ModuleScopes.validate(Event.Guard.get(), ValidationError) || Event.Guard->Sort.Kind != LogicSortKind::Bool) return llvm::createStringError( llvm::inconvertibleErrorCode(), "obligation module has invalid diagnostic trace metadata"); for (const DiagnosticTraceValue &Value : Event.Values) if (Value.Label.empty() || containsEmbeddedNul(Value.Label) || - !validateLogicExpr(Value.Value.get(), ValidationError) || + !validateLogicExpr(Value.Value.get(), ValidationError, &WellFormed) || !validateLogicCalls(Value.Value.get(), M.LogicFunctions, - ValidationError) || - !validateVariableScopes(Value.Value.get(), ModuleVariables, - ValidationError)) + ValidationError, &CallsChecked) || + !ModuleScopes.validate(Value.Value.get(), ValidationError)) return llvm::createStringError( llvm::inconvertibleErrorCode(), "obligation module has invalid diagnostic trace value"); } - if (!validateLogicExpr(M.CorrectnessGoal.get(), ValidationError)) + if (!validateLogicExpr(M.CorrectnessGoal.get(), ValidationError, &WellFormed)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (!validateLogicCalls(M.CorrectnessGoal.get(), M.LogicFunctions, - ValidationError)) + ValidationError, &CallsChecked)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); - if (!validateVariableScopes(M.CorrectnessGoal.get(), ModuleVariables, - ValidationError)) + if (!ModuleScopes.validate(M.CorrectnessGoal.get(), ValidationError)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (M.CorrectnessGoal->Sort.Kind != LogicSortKind::Bool) return llvm::createStringError(llvm::inconvertibleErrorCode(), "complete correctness goal is not bool"); - if (!validateLogicExpr(M.CounterexampleQuery.get(), ValidationError)) + if (!validateLogicExpr(M.CounterexampleQuery.get(), ValidationError, + &WellFormed)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (!validateLogicCalls(M.CounterexampleQuery.get(), M.LogicFunctions, - ValidationError)) + ValidationError, &CallsChecked)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); - if (!validateVariableScopes(M.CounterexampleQuery.get(), ModuleVariables, - ValidationError)) + if (!ModuleScopes.validate(M.CounterexampleQuery.get(), ValidationError)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (M.CounterexampleQuery->Sort.Kind != LogicSortKind::Bool) @@ -2428,8 +2668,10 @@ verify::validateObligationModule(const ObligationModule &M) { "complete counterexample query is not the exact negation of its goal"); LogicFeatureSet RequiredFeatures = 0; - collectRequiredFeatures(M.CorrectnessGoal.get(), RequiredFeatures); - collectRequiredFeatures(M.CounterexampleQuery.get(), RequiredFeatures); + collectRequiredFeatures(M.CorrectnessGoal.get(), RequiredFeatures, + &FeaturesSeen); + collectRequiredFeatures(M.CounterexampleQuery.get(), RequiredFeatures, + &FeaturesSeen); std::set ObligationIds; for (const Obligation &Item : M.Obligations) { @@ -2453,28 +2695,28 @@ verify::validateObligationModule(const ObligationModule &M) { return llvm::createStringError( llvm::inconvertibleErrorCode(), "obligation module has an invalid diagnostic trace prefix"); - if (!validateLogicExpr(Item.Goal.get(), ValidationError)) + if (!validateLogicExpr(Item.Goal.get(), ValidationError, &WellFormed)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); - if (!validateLogicCalls(Item.Goal.get(), M.LogicFunctions, ValidationError)) + if (!validateLogicCalls(Item.Goal.get(), M.LogicFunctions, ValidationError, + &CallsChecked)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); - if (!validateVariableScopes(Item.Goal.get(), ModuleVariables, - ValidationError)) + if (!ModuleScopes.validate(Item.Goal.get(), ValidationError)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (Item.Goal->Sort.Kind != LogicSortKind::Bool) return llvm::createStringError(llvm::inconvertibleErrorCode(), "individual correctness goal is not bool"); - if (!validateLogicExpr(Item.CounterexampleQuery.get(), ValidationError)) + if (!validateLogicExpr(Item.CounterexampleQuery.get(), ValidationError, + &WellFormed)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (!validateLogicCalls(Item.CounterexampleQuery.get(), M.LogicFunctions, - ValidationError)) + ValidationError, &CallsChecked)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); - if (!validateVariableScopes(Item.CounterexampleQuery.get(), ModuleVariables, - ValidationError)) + if (!ModuleScopes.validate(Item.CounterexampleQuery.get(), ValidationError)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (Item.CounterexampleQuery->Sort.Kind != LogicSortKind::Bool) @@ -2486,8 +2728,9 @@ verify::validateObligationModule(const ObligationModule &M) { llvm::inconvertibleErrorCode(), "individual counterexample query is not the exact negation of its " "goal"); - collectRequiredFeatures(Item.Goal.get(), RequiredFeatures); - collectRequiredFeatures(Item.CounterexampleQuery.get(), RequiredFeatures); + collectRequiredFeatures(Item.Goal.get(), RequiredFeatures, &FeaturesSeen); + collectRequiredFeatures(Item.CounterexampleQuery.get(), RequiredFeatures, + &FeaturesSeen); } std::unique_ptr CanonicalGoal = buildCompleteGoal(M.Obligations); @@ -2536,7 +2779,8 @@ verify::validateObligationModule(const ObligationModule &M) { logicFeature(LogicFeature::MathematicalIntegers); } if (Declaration.StepDefinition) { - if (!validateLogicExpr(Declaration.StepDefinition.get(), ValidationError)) + if (!validateLogicExpr(Declaration.StepDefinition.get(), ValidationError, + &WellFormed)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (Declaration.StepDefinition->Sort.Kind != @@ -2549,18 +2793,18 @@ verify::validateObligationModule(const ObligationModule &M) { llvm::inconvertibleErrorCode(), "logical function step result sort mismatch"); if (!validateLogicCalls(Declaration.StepDefinition.get(), - M.LogicFunctions, ValidationError) || - !validateVariableScopes(Declaration.StepDefinition.get(), - ValidationError) || + M.LogicFunctions, ValidationError, + &CallsChecked) || + !definitionScopes(Declaration.StepDefinition.get()) || !validateDefinitionVariables(Declaration.StepDefinition.get(), Parameters, {}, ValidationError)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); collectRequiredFeatures(Declaration.StepDefinition.get(), - RequiredFeatures); + RequiredFeatures, &FeaturesSeen); } for (const auto &Definition : Declaration.DefinitionLevels) { - if (!validateLogicExpr(Definition.get(), ValidationError)) + if (!validateLogicExpr(Definition.get(), ValidationError, &WellFormed)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (Definition->Sort.Kind != Declaration.ResultSort.Kind || @@ -2570,19 +2814,20 @@ verify::validateObligationModule(const ObligationModule &M) { llvm::inconvertibleErrorCode(), "logical function definition result sort mismatch"); if (!validateLogicCalls(Definition.get(), M.LogicFunctions, - ValidationError) || - !validateVariableScopes(Definition.get(), ValidationError) || + ValidationError, &CallsChecked) || + !definitionScopes(Definition.get()) || !validateDefinitionVariables(Definition.get(), Parameters, {}, ValidationError)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); - collectRequiredFeatures(Definition.get(), RequiredFeatures); + collectRequiredFeatures(Definition.get(), RequiredFeatures, + &FeaturesSeen); } // A measure only chooses an induction or Lean's termination argument, // so it adds no feature; it must still be an integer over the // parameters. for (const auto &Measure : Declaration.Decreases) { - if (!validateLogicExpr(Measure.get(), ValidationError)) + if (!validateLogicExpr(Measure.get(), ValidationError, &WellFormed)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ValidationError.c_str()); if (Measure->Sort.Kind != LogicSortKind::MathematicalInteger && @@ -2590,9 +2835,9 @@ verify::validateObligationModule(const ObligationModule &M) { return llvm::createStringError( llvm::inconvertibleErrorCode(), "logical function termination measure is not an integer"); - if (!validateLogicCalls(Measure.get(), M.LogicFunctions, - ValidationError) || - !validateVariableScopes(Measure.get(), ValidationError) || + if (!validateLogicCalls(Measure.get(), M.LogicFunctions, ValidationError, + &CallsChecked) || + !definitionScopes(Measure.get()) || !validateDefinitionVariables(Measure.get(), Parameters, {}, ValidationError)) return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", From 105c32490d6843d82651b04454be5ecbf389f810 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 22:10:07 +0530 Subject: [PATCH 2/6] verify: Count a module's nodes from each shared term's count. --- .../lib/Verify/Backend/ObligationSimplify.cpp | 28 +++++++++++++++---- 1 file changed, 22 insertions(+), 6 deletions(-) diff --git a/clang/lib/Verify/Backend/ObligationSimplify.cpp b/clang/lib/Verify/Backend/ObligationSimplify.cpp index 66154f06fe..fc5c03a8d9 100644 --- a/clang/lib/Verify/Backend/ObligationSimplify.cpp +++ b/clang/lib/Verify/Backend/ObligationSimplify.cpp @@ -46,17 +46,33 @@ uint64_t countNodes(const LogicExpr *Expr) { return Count; } +/// countNodes, with the count of each term kept in \p Counts: the goals +/// share the terms of their assumptions. +uint64_t countNodes(const LogicExpr *Expr, + llvm::DenseMap &Counts) { + if (!Expr) + return 0; + if (auto It = Counts.find(Expr); It != Counts.end()) + return It->second; + uint64_t Count = 1; + for (const auto &Child : Expr->Children) + Count += countNodes(Child.get(), Counts); + Counts[Expr] = Count; + return Count; +} + uint64_t countModuleNodes(const ObligationModule &Module) { - uint64_t Count = countNodes(Module.CorrectnessGoal.get()) + - countNodes(Module.CounterexampleQuery.get()); + llvm::DenseMap Counts; + uint64_t Count = countNodes(Module.CorrectnessGoal.get(), Counts) + + countNodes(Module.CounterexampleQuery.get(), Counts); for (const Obligation &Item : Module.Obligations) - Count += countNodes(Item.Goal.get()) + - countNodes(Item.CounterexampleQuery.get()); + Count += countNodes(Item.Goal.get(), Counts) + + countNodes(Item.CounterexampleQuery.get(), Counts); for (const auto &[Identity, Function] : Module.LogicFunctions) { (void)Identity; - Count += countNodes(Function.StepDefinition.get()); + Count += countNodes(Function.StepDefinition.get(), Counts); for (const auto &Definition : Function.DefinitionLevels) - Count += countNodes(Definition.get()); + Count += countNodes(Definition.get(), Counts); } return Count; } From f5d4be64f7026eba54407c36786bf7714e28581e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 22:10:07 +0530 Subject: [PATCH 3/6] test: Validate modules whose roots share terms. --- .../Verify/ObligationValidationTest.cpp | 189 ++++++++++++++++++ 1 file changed, 189 insertions(+) create mode 100644 clang/unittests/Verify/ObligationValidationTest.cpp diff --git a/clang/unittests/Verify/ObligationValidationTest.cpp b/clang/unittests/Verify/ObligationValidationTest.cpp new file mode 100644 index 0000000000..ada7cd35be --- /dev/null +++ b/clang/unittests/Verify/ObligationValidationTest.cpp @@ -0,0 +1,189 @@ +//===- unittests/Verify/ObligationValidationTest.cpp ----------------------===// +// +// Validation of modules whose roots share terms, as built modules do: a +// shared term is checked once, and each root still gets every check. +// +//===----------------------------------------------------------------------===// + +#include "Backend/Obligation.h" +#include "llvm/Support/Error.h" +#include "gtest/gtest.h" +#include + +using namespace clang::verify; + +namespace { + +LogicSort math() { return LogicSort::mathematicalInteger(); } +LogicSort bv32() { return LogicSort::bitVector(32, true); } + +LogicExprRef term(LogicExpr::Kind Kind, LogicSort Sort, + std::vector Children = {}) { + auto E = std::make_unique(Kind); + E->Sort = Sort; + E->Children = std::move(Children); + return LogicExprRef(std::move(E)); +} + +LogicExprRef variable(llvm::StringRef Name, LogicSort Sort) { + auto E = std::make_unique(LogicExpr::Var); + E->Sort = Sort; + E->Name = Name.str(); + return LogicExprRef(std::move(E)); +} + +LogicExprRef zero(LogicSort Sort) { return term(LogicExpr::IntLit, Sort); } + +LogicExprRef equal(LogicExprRef Left, LogicExprRef Right) { + return term(LogicExpr::Eq, LogicSort::boolSort(), {Left, Right}); +} + +LogicExprRef forall(llvm::StringRef Binder, LogicExprRef Body) { + auto E = std::make_unique(LogicExpr::Forall); + E->Sort = LogicSort::boolSort(); + E->Binder = Binder.str(); + E->Children.push_back(Body); + return LogicExprRef(std::move(E)); +} + +std::unique_ptr root(const LogicExprRef &Term) { + return cloneLogicExpr(Term.get()); +} + +std::unique_ptr negation(const LogicExprRef &Term) { + auto E = std::make_unique(LogicExpr::Not); + E->Sort = LogicSort::boolSort(); + E->Children.push_back(Term); + return E; +} + +/// A module with these goals, in order, and a trace event with these values; +/// every root refers to the terms it is given rather than to copies. +ObligationModule module(std::vector Goals, + std::vector TraceValues = {}) { + ObligationModule M; + M.FunctionName = "shared"; + M.FunctionIdentity = "shared"; + LogicExprRef Complete; + for (size_t I = 0; I != Goals.size(); ++I) { + Obligation Item; + Item.Id = "o" + std::to_string(I); + Item.Goal = root(Goals[I]); + Item.CounterexampleQuery = negation(Goals[I]); + M.Obligations.push_back(std::move(Item)); + Complete = Complete ? term(LogicExpr::And, LogicSort::boolSort(), + {Complete, Goals[I]}) + : Goals[I]; + } + M.CorrectnessGoal = root(Complete); + M.CounterexampleQuery = negation(Complete); + if (!TraceValues.empty()) { + DiagnosticTraceEvent Event; + Event.Guard = root(term(LogicExpr::True, LogicSort::boolSort())); + for (const LogicExprRef &Value : TraceValues) + Event.Values.push_back({"value", root(Value)}); + M.TraceEvents.push_back(std::move(Event)); + } + return M; +} + +std::string validationError(const ObligationModule &M) { + auto Features = validateObligationModule(M); + if (Features) + return ""; + return llvm::toString(Features.takeError()); +} + +TEST(ObligationValidation, SharedTermsKeepEveryFeature) { + LogicExprRef X = variable("x", math()); + LogicExprRef Y = variable("y", bv32()); + LogicExprRef Quantified = forall("k", equal(variable("k", math()), X)); + LogicExprRef First = term(LogicExpr::Or, LogicSort::boolSort(), + {Quantified, equal(X, zero(math()))}); + LogicExprRef Second = term(LogicExpr::Or, LogicSort::boolSort(), + {Quantified, equal(Y, zero(bv32()))}); + ObligationModule M = module({First, Second}, {X}); + auto Features = validateObligationModule(M); + ASSERT_TRUE(static_cast(Features)) + << llvm::toString(Features.takeError()); + EXPECT_EQ(*Features, logicFeature(LogicFeature::MathematicalIntegers) | + logicFeature(LogicFeature::BitVectors) | + logicFeature(LogicFeature::Quantifiers)); +} + +// Each shared term is checked once: this goal's terms double at each of 26 +// levels, so a validation that did not share its work would walk 2^26 paths. +TEST(ObligationValidation, SharedTermsAreCheckedOnce) { + LogicExprRef X = variable("x", math()); + LogicExprRef Term = term( + LogicExpr::And, LogicSort::boolSort(), + {forall("k", equal(variable("k", math()), X)), equal(X, zero(math()))}); + for (unsigned Level = 0; Level != 26; ++Level) + Term = term(LogicExpr::And, LogicSort::boolSort(), {Term, Term}); + const auto Start = std::chrono::steady_clock::now(); + EXPECT_EQ(validationError(module({Term}, {Term})), ""); + EXPECT_LT(std::chrono::duration_cast( + std::chrono::steady_clock::now() - Start) + .count(), + 5000); +} + +// The trace value is checked first and has no binder; the goal then binds k +// elsewhere, so the same free k collides with a binder of the goal's root. +TEST(ObligationValidation, BinderOfALaterRootCollidesWithASharedFreeVariable) { + LogicExprRef K = variable("k", math()); + LogicExprRef Goal = + term(LogicExpr::Or, LogicSort::boolSort(), + {forall("k", equal(variable("k", math()), zero(math()))), + equal(K, zero(math()))}); + EXPECT_EQ(validationError(module({Goal}, {equal(K, zero(math()))})), + "quantifier binder collides with a free variable"); +} + +// The same term is bound in the trace value and free in the goal, where its +// sort differs from the variable's. +TEST(ObligationValidation, SharedTermBoundThenFree) { + LogicExprRef K = variable("k", math()); + ObligationModule M = + module({equal(K, zero(math()))}, {forall("k", equal(K, zero(math())))}); + M.DiagnosticVariables["k"] = {"k", bv32(), {}, {}, {}}; + EXPECT_EQ(validationError(M), "logical variable has inconsistent sorts: k"); +} + +// The same machine-integer term is free in the trace value and bound in the +// goal, where a binder must be a mathematical integer. +TEST(ObligationValidation, SharedTermFreeThenBound) { + LogicExprRef K = variable("k", bv32()); + ObligationModule M = + module({forall("k", equal(K, zero(bv32())))}, {equal(K, zero(bv32()))}); + EXPECT_EQ(validationError(M), + "quantifier binder occurrence is not a mathematical integer"); +} + +// An application shared by two goals is checked against the declarations. +TEST(ObligationValidation, SharedApplicationOfNoDeclaration) { + auto Call = std::make_unique(LogicExpr::SpecCall); + Call->Sort = math(); + Call->SpecCallee = "g"; + LogicExprRef Application(std::move(Call)); + LogicExprRef Goal = equal(Application, zero(math())); + EXPECT_EQ(validationError(module({Goal, Goal})), + "logical application has no owned declaration: g"); +} + +// A definition's variables are its parameters, not the module's. +TEST(ObligationValidation, DefinitionsHaveTheirOwnVariables) { + ObligationModule M = module({equal(variable("x", bv32()), zero(bv32()))}); + LogicFunctionDecl F; + F.Identity = "f"; + F.DisplayName = "f"; + F.Parameters.push_back({"x", math()}); + F.ResultSort = math(); + F.DefinitionFuel = 1; + F.StepDefinition = root(variable("x", math())); + F.DefinitionLevels.push_back(root(variable("x", math()))); + M.LogicFunctions["f"] = std::move(F); + EXPECT_EQ(validationError(M), ""); +} + +} // namespace From 671f20a7298a5ea23c495bb4345b8d42a991754d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 22:10:08 +0530 Subject: [PATCH 4/6] test: Build the obligation validation tests. --- clang/unittests/Verify/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/unittests/Verify/CMakeLists.txt b/clang/unittests/Verify/CMakeLists.txt index 7db36a5f79..e6ac816df0 100644 --- a/clang/unittests/Verify/CMakeLists.txt +++ b/clang/unittests/Verify/CMakeLists.txt @@ -8,6 +8,7 @@ add_distinct_clang_unittest(VerifyTests CertifyTest.cpp EncodingParityTest.cpp MachineIntegerEncodingTest.cpp + ObligationValidationTest.cpp CLANG_LIBS clangVerify LINK_LIBS From b2002e586ae004e210a5d84b2475f8a51e22188c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 22:10:08 +0530 Subject: [PATCH 5/6] docs: Describe how validation visits a shared term once. --- docs/ARCHITECTURE.md | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index e26117327c..83be4280d0 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -924,9 +924,43 @@ space and 53 s, verifying it 14.9 GB with eight jobs (`--jobs=8`, more than a 16 GB CI runner holds beside the tests running with it), and lowering `safe_fib.cpp` 4.7 GB and 16 s. They now take 0.43 GB and 10 s, 0.9 GB, and 0.35 GB and 7 s. The goals still repeat their assumptions as trees, so a -traversal that does not memoize (validation, hashing, serialization) still -takes time quadratic in a function's length; hash-consing the terms and -memoizing those traversals would make it linear. +traversal that does not memoize takes time quadratic in a function's length: +hashing and serialization still do. The simplifier's statistics count a +module's nodes as trees, each shared term's count computed once +(`countModuleNodes`). + +**Validation visits a shared term once.** `validateObligationModule` checks +each term of a module as a root (every trace guard and value, the complete +goal and query, each obligation's goal and query, and each definition level, +step, and measure): every node is well formed, every application has a +declaration with its signature, every variable is in scope with one sort, +and it collects the logic features the module needs. Each check keeps, for +the module, the terms it has passed, so a term the goals share is checked +once whichever roots reach it. Form, applications, and features depend on +the term alone. Scope depends on where a term is, and `ScopeValidator` +handles it in two parts: + +- A variable is bound or free by the quantifiers above it, so a term is + visited once for each set of binder names in scope at it (interned, so + a set is a number). A visit checks that a bound occurrence is a + mathematical integer and registers a free one in the map of free + variables, whose sort must agree with every other occurrence. The module's + roots share one map; each definition has its own, since its variables are + its parameters. +- A free variable must not have the name of a binder anywhere in its root. + `BinderSummaries` gives each term, once, the set of binder names it + contains and the set of binder names free in it (as Frama-C's Qed caches + each term's bound and free variables, `bind` and `vars`, and Lean each + `Expr`'s loose bound-variable range), after every binder name of the + module is registered; a root fails where the two sets of the root meet. + +A root that fails either part is checked again by the tree walk that was the +whole check before, which gives the error it always gave, and an assertion +checks that this walk fails too. Validation was 80% of lowering (callgrind, +`safe_fib.cpp`, 20.4 of 25.1 billion instructions); with it and the node +count linear, `--lower-only` takes 1.9 s instead of 10.4 s on `safe_fib.cpp` +and 2.5 s instead of 10.3 s on the ULEB128 case study, within the same +memory and with the same output. Every source-built or replayed module then passes through one fail-closed canonicalization step before hashing or backend dispatch. The pass folds only From c409b91468239e7121ac1b516e2a442149015fb2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 22:10:08 +0530 Subject: [PATCH 6/6] docs: Note the faster lowering in the 0.2.0 release notes. --- website/source/release-notes.rst | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 85891b4f0f..cf678a6cfa 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -471,10 +471,11 @@ every assumption before it as a copy, and the check's query, the function's complete goal, and that goal's query copied them again, so memory grew with the number of checks times the length of what came before them: verifying the ULEB128 case study took 14.9 GB, and lowering it 53 s. Terms now share what -they repeat: the case study verifies within 0.9 GB and lowers in 10 s, and -``safe_fib.cpp`` lowers in 7 s within 0.35 GB instead of 16 s and 4.7 GB. -Verdicts, archives, hashes, and IR dumps are unchanged; a Lean export names a -large subterm that one statement repeats once (:doc:`case-studies/llvm-uleb128`). +they repeat, and the checks of a module visit a shared term once: the case +study verifies within 0.9 GB and lowers in 2.5 s, and ``safe_fib.cpp`` lowers +in 1.9 s within 0.35 GB instead of 16 s and 4.7 GB. Verdicts, archives, hashes, +and IR dumps are unchanged; a Lean export names a large subterm that one +statement repeats once (:doc:`case-studies/llvm-uleb128`). **Errors point at the code.** An error about a construct the verifier does not represent named only the function, as in ``error: pick: unsupported statement: