1fa0612f6e
When both arms of an if-statement prove the same variable non-null (via M22 null-check inference or M23 address-of marking), the summary encoder's `mergeBindings` now intersects the two branches' nonNullVars sets and marks the survivors in the post-if env. Mirrors the same logic already present in security_walker.cpp::walkIf so summary mode and the main walker stay in parity. Added tests/unit/test_summary_encoder_phi_nonnull.cpp covering the rename-pair address-of case. Pre-fix the test FAILs; post-fix PASSes. 44/44 still green. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
83 lines
2.8 KiB
C++
83 lines
2.8 KiB
C++
// M28 phi-join: verify that non-null facts proven in BOTH arms of an
|
|
// if-statement survive the phi-merge in the summary encoder.
|
|
//
|
|
// security_walker.cpp already does this intersection in its walkIf;
|
|
// this test pins the same behavior for `summary_encoder::mergeBindings`
|
|
// so the two code paths stay in parity.
|
|
|
|
#include <clang/AST/Decl.h>
|
|
#include <clang/Frontend/ASTUnit.h>
|
|
#include <clang/Tooling/Tooling.h>
|
|
|
|
#include <catch2/catch_test_macros.hpp>
|
|
#include <memory>
|
|
#include <string>
|
|
|
|
#include "fold/symbolic/summary_encoder.hpp"
|
|
|
|
namespace {
|
|
|
|
std::unique_ptr<clang::ASTUnit> parse(const std::string& code, const std::string& file) {
|
|
return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, file);
|
|
}
|
|
|
|
const clang::FunctionDecl* findFunction(clang::ASTUnit& unit, const std::string& name) {
|
|
auto& ctx = unit.getASTContext();
|
|
for (auto* decl : ctx.getTranslationUnitDecl()->decls()) {
|
|
auto* fd = clang::dyn_cast<clang::FunctionDecl>(decl);
|
|
if (!fd || !fd->hasBody())
|
|
continue;
|
|
if (fd->getQualifiedNameAsString() == name)
|
|
return fd;
|
|
}
|
|
return nullptr;
|
|
}
|
|
|
|
const clang::VarDecl* findGlobalVar(clang::ASTUnit& unit, const std::string& name) {
|
|
auto& ctx = unit.getASTContext();
|
|
for (auto* decl : ctx.getTranslationUnitDecl()->decls()) {
|
|
auto* vd = clang::dyn_cast<clang::VarDecl>(decl);
|
|
if (!vd || !vd->hasGlobalStorage())
|
|
continue;
|
|
if (vd->getNameAsString() == name)
|
|
return vd;
|
|
}
|
|
return nullptr;
|
|
}
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("M28: non-null facts intersected at phi-join survive in summary env",
|
|
"[summary][phi][m28]") {
|
|
// `f` takes only int params (summarizeFunction rejects pointer params via
|
|
// isModeledType), but its body null-checks a global pointer `g_a` in both
|
|
// arms of an if/else. Without M28 in the summary encoder, the post-if env
|
|
// loses the non-null mark; with M28, it retains it (the intersection of
|
|
// both arms' nonNullVars is non-empty).
|
|
auto unit = parse(R"(
|
|
int x;
|
|
int y;
|
|
int* g_p;
|
|
int f(int cond) {
|
|
if (cond) {
|
|
g_p = &x; // M23: address-of marks g_p non-null in then_env
|
|
} else {
|
|
g_p = &y; // M23: address-of marks g_p non-null in else_env
|
|
}
|
|
// Post-if: both branches mark g_p non-null. M28 should retain.
|
|
return 0;
|
|
}
|
|
)",
|
|
"m28.cpp");
|
|
REQUIRE(unit);
|
|
|
|
const auto* fd = findFunction(*unit, "f");
|
|
REQUIRE(fd != nullptr);
|
|
|
|
auto summary = fold::summarizeFunction(fd, unit->getASTContext());
|
|
REQUIRE(summary);
|
|
|
|
const clang::VarDecl* g_p = findGlobalVar(*unit, "g_p");
|
|
REQUIRE(g_p != nullptr);
|
|
REQUIRE(summary->env.isDefinitelyNonNull(g_p));
|
|
}
|