llvm/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp

//===- 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/AnalyzerOptions.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"
#include "llvm/Support/Timer.h"

#define DEBUG_TYPE …

STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
STATISTIC(NumTimesZ3ExhaustedRLimit,
          "Number of times Z3 query exhausted the rlimit");
STATISTIC(NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,
          "Number of times report equivalenece class was cut because it spent "
          "too much time in Z3");

STATISTIC(NumTimesZ3QueryAcceptsReport,
          "Number of Z3 queries accepting a report");
STATISTIC(NumTimesZ3QueryRejectReport,
          "Number of Z3 queries rejecting a report");
STATISTIC(NumTimesZ3QueryRejectEQClass,
          "Number of times rejecting an report equivalenece class");

usingnamespaceclang;
usingnamespaceento;

Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
                                         const AnalyzerOptions &Opts)
    : … { … }

void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
                                          const ExplodedNode *EndPathNode,
                                          PathSensitiveBugReport &BR) { … }

void Z3CrosscheckVisitor::addConstraints(
    const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) { … }

PathDiagnosticPieceRef
Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
                               PathSensitiveBugReport &) { … }

void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const { … }

Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
    const Z3CrosscheckVisitor::Z3Result &Query) { … }