llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT--> @llvm/pr-subscribers-clang-static-analyzer-1 Author: Balazs Benics (steakhal) <details> <summary>Changes</summary> This is exactly as originally landed in #<!-- -->95128, but now the minimal Z3 version was increased to meet this change in #<!-- -->96682. https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4 --- This change keeps existing behavior, namely that if we hit a Z3 timeout we will accept the report as "satisfiable". This prepares for the commit "Harden safeguards for Z3 query times". https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 (cherry picked from commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab) --- Patch is 27.63 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/97265.diff 12 Files Affected: - (modified) clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h (-23) - (added) clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h (+66) - (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (+4-1) - (modified) clang/lib/StaticAnalyzer/Core/BugReporter.cpp (+22-6) - (modified) clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (-76) - (modified) clang/lib/StaticAnalyzer/Core/CMakeLists.txt (+1) - (added) clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp (+118) - (added) clang/test/Analysis/z3/crosscheck-statistics.c (+33) - (modified) clang/unittests/StaticAnalyzer/CMakeLists.txt (+1) - (added) clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp (+59) - (modified) llvm/include/llvm/Support/SMTAPI.h (+19) - (modified) llvm/lib/Support/Z3Solver.cpp (+96-20) ``````````diff diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h index cc3d93aabafda..f97514955a591 100644 --- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h @@ -597,29 +597,6 @@ class SuppressInlineDefensiveChecksVisitor final : public BugReporterVisitor { PathSensitiveBugReport &BR) override; }; -/// The bug visitor will walk all the nodes in a path and collect all the -/// constraints. When it reaches the root node, will create a refutation -/// manager and check if the constraints are satisfiable -class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor { -private: - /// Holds the constraints in a given path - ConstraintMap Constraints; - -public: - FalsePositiveRefutationBRVisitor(); - - void Profile(llvm::FoldingSetNodeID &ID) const override; - - PathDiagnosticPieceRef VisitNode(const ExplodedNode *N, - BugReporterContext &BRC, - PathSensitiveBugReport &BR) override; - - void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode, - PathSensitiveBugReport &BR) override; - void addConstraints(const ExplodedNode *N, - bool OverwriteConstraintsOnExistingSyms); -}; - /// The visitor detects NoteTags and displays the event notes they contain. class TagVisitor : public BugReporterVisitor { public: diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h new file mode 100644 index 0000000000000..9413fd739f607 --- /dev/null +++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h @@ -0,0 +1,66 @@ +//===- Z3CrosscheckVisitor.h - Crosscheck reports with Z3 -------*- C++ -*-===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// This file defines the visitor and utilities around it for Z3 report +// refutation. +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H +#define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H + +#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h" + +namespace clang::ento { + +/// The bug visitor will walk all the nodes in a path and collect all the +/// constraints. When it reaches the root node, will create a refutation +/// manager and check if the constraints are satisfiable. +class Z3CrosscheckVisitor final : public BugReporterVisitor { +public: + struct Z3Result { + std::optional<bool> IsSAT = std::nullopt; + }; + explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result); + + void Profile(llvm::FoldingSetNodeID &ID) const override; + + PathDiagnosticPieceRef VisitNode(const ExplodedNode *N, + BugReporterContext &BRC, + PathSensitiveBugReport &BR) override; + + void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode, + PathSensitiveBugReport &BR) override; + +private: + void addConstraints(const ExplodedNode *N, + bool OverwriteConstraintsOnExistingSyms); + + /// Holds the constraints in a given path. + ConstraintMap Constraints; + Z3Result &Result; +}; + +/// The oracle will decide if a report should be accepted or rejected based on +/// the results of the Z3 solver. +class Z3CrosscheckOracle { +public: + enum Z3Decision { + AcceptReport, // The report was SAT. + RejectReport, // The report was UNSAT or UNDEF. + }; + + /// Makes a decision for accepting or rejecting the report based on the + /// result of the corresponding Z3 query. + static Z3Decision + interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Query); +}; + +} // namespace clang::ento + +#endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 5116a4c06850d..bf18c353b8508 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -34,7 +34,10 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { public: SMTConstraintManager(clang::ento::ExprEngine *EE, clang::ento::SValBuilder &SB) - : SimpleConstraintManager(EE, SB) {} + : SimpleConstraintManager(EE, SB) { + Solver->setBoolParam("model", true); // Enable model finding + Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/); + } virtual ~SMTConstraintManager() = default; //===------------------------------------------------------------------===// diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp index 14ca507a16d55..c9a7fd0e035c2 100644 --- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp +++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp @@ -35,6 +35,7 @@ #include "clang/StaticAnalyzer/Core/AnalyzerOptions.h" #include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h" #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h" +#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" #include "clang/StaticAnalyzer/Core/Checker.h" #include "clang/StaticAnalyzer/Core/CheckerManager.h" #include "clang/StaticAnalyzer/Core/CheckerRegistryData.h" @@ -86,6 +87,11 @@ STATISTIC(MaxValidBugClassSize, "The maximum number of bug reports in the same equivalence class " "where at least one report is valid (not suppressed)"); +STATISTIC(NumTimesReportPassesZ3, "Number of reports passed Z3"); +STATISTIC(NumTimesReportRefuted, "Number of reports refuted by Z3"); +STATISTIC(NumTimesReportEQClassWasExhausted, + "Number of times all reports of an equivalence class was refuted"); + BugReporterVisitor::~BugReporterVisitor() = default; void BugReporterContext::anchor() {} @@ -2864,21 +2870,31 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport( // If crosscheck is enabled, remove all visitors, add the refutation // visitor and check again R->clearVisitors(); - R->addVisitor<FalsePositiveRefutationBRVisitor>(); + Z3CrosscheckVisitor::Z3Result CrosscheckResult; + R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult); // We don't overwrite the notes inserted by other visitors because the // refutation manager does not add any new note to the path generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC); + switch (Z3CrosscheckOracle::interpretQueryResult(CrosscheckResult)) { + case Z3CrosscheckOracle::RejectReport: + ++NumTimesReportRefuted; + R->markInvalid("Infeasible constraints", /*Data=*/nullptr); + continue; + case Z3CrosscheckOracle::AcceptReport: + ++NumTimesReportPassesZ3; + break; + } } - // Check if the bug is still valid - if (R->isValid()) - return PathDiagnosticBuilder( - std::move(BRC), std::move(BugPath->BugPath), BugPath->Report, - BugPath->ErrorNode, std::move(visitorNotes)); + assert(R->isValid()); + return PathDiagnosticBuilder(std::move(BRC), std::move(BugPath->BugPath), + BugPath->Report, BugPath->ErrorNode, + std::move(visitorNotes)); } } + ++NumTimesReportEQClassWasExhausted; return {}; } diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp index 4ff4f7de425ca..7102bf51a57e8 100644 --- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -3447,82 +3447,6 @@ UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC, return nullptr; } -//===----------------------------------------------------------------------===// -// Implementation of FalsePositiveRefutationBRVisitor. -//===----------------------------------------------------------------------===// - -FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor() - : Constraints(ConstraintMap::Factory().getEmptyMap()) {} - -void FalsePositiveRefutationBRVisitor::finalizeVisitor( - BugReporterContext &BRC, const ExplodedNode *EndPathNode, - PathSensitiveBugReport &BR) { - // Collect new constraints - addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true); - - // Create a refutation manager - llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); - ASTContext &Ctx = BRC.getASTContext(); - - // Add constraints to the solver - for (const auto &I : Constraints) { - const SymbolRef Sym = I.first; - auto RangeIt = I.second.begin(); - - llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( - RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(), - /*InRange=*/true); - while ((++RangeIt) != I.second.end()) { - SMTConstraints = RefutationSolver->mkOr( - SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, - RangeIt->From(), RangeIt->To(), - /*InRange=*/true)); - } - - RefutationSolver->addConstraint(SMTConstraints); - } - - // And check for satisfiability - std::optional<bool> IsSAT = RefutationSolver->check(); - if (!IsSAT) - return; - - if (!*IsSAT) - BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext()); -} - -void FalsePositiveRefutationBRVisitor::addConstraints( - const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) { - // Collect new constraints - ConstraintMap NewCs = getConstraintMap(N->getState()); - ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>(); - - // Add constraints if we don't have them yet - for (auto const &C : NewCs) { - const SymbolRef &Sym = C.first; - if (!Constraints.contains(Sym)) { - // This symbol is new, just add the constraint. - Constraints = CF.add(Constraints, Sym, C.second); - } else if (OverwriteConstraintsOnExistingSyms) { - // Overwrite the associated constraint of the Symbol. - Constraints = CF.remove(Constraints, Sym); - Constraints = CF.add(Constraints, Sym, C.second); - } - } -} - -PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode( - const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) { - addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false); - return nullptr; -} - -void FalsePositiveRefutationBRVisitor::Profile( - llvm::FoldingSetNodeID &ID) const { - static int Tag = 0; - ID.AddPointer(&Tag); -} - //===----------------------------------------------------------------------===// // Implementation of TagVisitor. //===----------------------------------------------------------------------===// diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt index 8672876c0608d..fb9394a519eb7 100644 --- a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt +++ b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt @@ -51,6 +51,7 @@ add_clang_library(clangStaticAnalyzerCore SymbolManager.cpp TextDiagnostics.cpp WorkList.cpp + Z3CrosscheckVisitor.cpp LINK_LIBS clangAST diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp new file mode 100644 index 0000000000000..a7db44ef8ea30 --- /dev/null +++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp @@ -0,0 +1,118 @@ +//===- Z3CrosscheckVisitor.cpp - Crosscheck reports with Z3 -----*- C++ -*-===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// This file declares the visitor and utilities around it for Z3 report +// refutation. +// +//===----------------------------------------------------------------------===// + +#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" +#include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" +#include "llvm/ADT/Statistic.h" +#include "llvm/Support/SMTAPI.h" + +#define DEBUG_TYPE "Z3CrosscheckOracle" + +STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done"); +STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out"); + +STATISTIC(NumTimesZ3QueryAcceptsReport, + "Number of Z3 queries accepting a report"); +STATISTIC(NumTimesZ3QueryRejectReport, + "Number of Z3 queries rejecting a report"); + +using namespace clang; +using namespace ento; + +Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result) + : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {} + +void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC, + const ExplodedNode *EndPathNode, + PathSensitiveBugReport &BR) { + // Collect new constraints + addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true); + + // Create a refutation manager + llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); + RefutationSolver->setBoolParam("model", true); // Enable model finding + RefutationSolver->setUnsignedParam("timeout", 15000); // ms + + ASTContext &Ctx = BRC.getASTContext(); + + // Add constraints to the solver + for (const auto &[Sym, Range] : Constraints) { + auto RangeIt = Range.begin(); + + llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( + RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(), + /*InRange=*/true); + while ((++RangeIt) != Range.end()) { + SMTConstraints = RefutationSolver->mkOr( + SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, + RangeIt->From(), RangeIt->To(), + /*InRange=*/true)); + } + RefutationSolver->addConstraint(SMTConstraints); + } + + // And check for satisfiability + std::optional<bool> IsSAT = RefutationSolver->check(); + Result = Z3Result{IsSAT}; +} + +void Z3CrosscheckVisitor::addConstraints( + const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) { + // Collect new constraints + ConstraintMap NewCs = getConstraintMap(N->getState()); + ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>(); + + // Add constraints if we don't have them yet + for (auto const &[Sym, Range] : NewCs) { + if (!Constraints.contains(Sym)) { + // This symbol is new, just add the constraint. + Constraints = CF.add(Constraints, Sym, Range); + } else if (OverwriteConstraintsOnExistingSyms) { + // Overwrite the associated constraint of the Symbol. + Constraints = CF.remove(Constraints, Sym); + Constraints = CF.add(Constraints, Sym, Range); + } + } +} + +PathDiagnosticPieceRef +Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &, + PathSensitiveBugReport &) { + addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false); + return nullptr; +} + +void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const { + static int Tag = 0; + ID.AddPointer(&Tag); +} + +Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult( + const Z3CrosscheckVisitor::Z3Result &Query) { + ++NumZ3QueriesDone; + + if (!Query.IsSAT.has_value()) { + // For backward compatibility, let's accept the first timeout. + ++NumTimesZ3TimedOut; + return AcceptReport; + } + + if (Query.IsSAT.value()) { + ++NumTimesZ3QueryAcceptsReport; + return AcceptReport; // sat + } + + ++NumTimesZ3QueryRejectReport; + return RejectReport; // unsat +} diff --git a/clang/test/Analysis/z3/crosscheck-statistics.c b/clang/test/Analysis/z3/crosscheck-statistics.c new file mode 100644 index 0000000000000..7192824c5be31 --- /dev/null +++ b/clang/test/Analysis/z3/crosscheck-statistics.c @@ -0,0 +1,33 @@ +// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s \ +// RUN: -analyzer-config crosscheck-with-z3=true \ +// RUN: -analyzer-stats 2>&1 | FileCheck %s + +// REQUIRES: z3 + +// expected-error@1 {{Z3 refutation rate:1/2}} + +int accepting(int n) { + if (n == 4) { + n = n / (n-4); // expected-warning {{Division by zero}} + } + return n; +} + +int rejecting(int n, int x) { + // Let's make the path infeasible. + if (2 < x && x < 5 && x*x == x*x*x) { + // Have the same condition as in 'accepting'. + if (n == 4) { + n = x / (n-4); // no-warning: refuted + } + } + return n; +} + +// CHECK: 1 BugReporter - Number of times all reports of an equivalence class was refuted +// CHECK-NEXT: 1 BugReporter - Number of reports passed Z3 +// CHECK-NEXT: 1 BugReporter - Number of reports refuted by Z3 + +// CHECK: 1 Z3CrosscheckVisitor - Number of Z3 queries accepting a report +// CHECK-NEXT: 1 Z3CrosscheckVisitor - Number of Z3 queries rejecting a report +// CHECK-NEXT: 2 Z3CrosscheckVisitor - Number of Z3 queries done diff --git a/clang/unittests/StaticAnalyzer/CMakeLists.txt b/clang/unittests/StaticAnalyzer/CMakeLists.txt index ff34d5747cc81..dcc557b44fb31 100644 --- a/clang/unittests/StaticAnalyzer/CMakeLists.txt +++ b/clang/unittests/StaticAnalyzer/CMakeLists.txt @@ -21,6 +21,7 @@ add_clang_unittest(StaticAnalysisTests SymbolReaperTest.cpp SValTest.cpp TestReturnValueUnderConstruction.cpp + Z3CrosscheckOracleTest.cpp ) clang_target_link_libraries(StaticAnalysisTests diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp new file mode 100644 index 0000000000000..efad4dd3f03b9 --- /dev/null +++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp @@ -0,0 +1,59 @@ +//===- unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp ----------------===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// + +#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" +#include "gtest/gtest.h" + +using namespace clang; +using namespace ento; + +using Z3Result = Z3CrosscheckVisitor::Z3Result; +using Z3Decision = Z3CrosscheckOracle::Z3Decision; + +static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport; +static constexpr Z3Decision RejectReport = Z3Decision::RejectReport; + +static constexpr std::optional<bool> SAT = true; +static constexpr std::optional<bool> UNSAT = false; +static constexpr std::optional<bool> UNDEF = std::nullopt; + +namespace { + +struct Z3CrosscheckOracleTest : public testing::Test { + Z3Decision interpretQueryResult(const Z3Result &Result) const { + return Z3CrosscheckOracle::interpretQueryResult(Result); + } +}; + +TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) { + ASSERT_EQ(AcceptReport, interpretQueryResult({SAT})); +} + +TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) { + ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT})); + ASSERT_EQ(AcceptReport, interpretQueryResult({SAT})); +} + +TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) { + ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF})); +} + +TEST_F(Z3CrosscheckOracleTest, Accept... [truncated] `````````` </details> https://github.com/llvm/llvm-project/pull/97265 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
