DataflowAnalysisContext.cpp Source File (original) (raw)

21#include "llvm/ADT/SetOperations.h"

22#include "llvm/ADT/SetVector.h"

23#include "llvm/Support/CommandLine.h"

24#include "llvm/Support/Debug.h"

25#include "llvm/Support/FileSystem.h"

26#include "llvm/Support/Path.h"

27#include "llvm/Support/raw_ostream.h"

28#include

29#include

30#include

31#include

32#include

35 "dataflow-log", llvm:🆑:Hidden, llvm:🆑:ValueOptional,

36 llvm:🆑:desc("Emit log of dataflow analysis. With no arg, writes textual "

37 "log to stderr. With an arg, writes HTML logs under the "

38 "specified directory (one per analyzed function)."));

41namespace dataflow {

51 if (Opts.ContextSensitiveOpts)

55}

57void DataflowAnalysisContext::addModeledFields(const FieldSet &Fields) {

58 ModeledFields.set_union(Fields);

59}

63 llvm::DenseMap<const ValueDecl *, StorageLocation *> FieldLocs;

65 if (Field->getType()->isReferenceType())

66 FieldLocs.insert({Field, nullptr});

67 else

69 Field->getType().getNonReferenceType())});

73 SyntheticFields.insert(

74 {Entry.getKey(),

78 std::move(SyntheticFields));

79 }

81}

85template

86static llvm::DenseSetllvm::StringRef getKeys(const llvm::StringMap &Map) {

87 return llvm::DenseSetllvm::StringRef(llvm::from_range, Map.keys());

88}

97 RecordStorageLocationCreated = true;

99 std::move(SyntheticFields));

100}

101

104 if (auto *Loc = DeclToLoc.lookup(&D))

105 return *Loc;

107 DeclToLoc[&D] = &Loc;

108 return Loc;

109}

110

114

115 if (auto *Loc = ExprToLoc.lookup(&CanonE))

116 return *Loc;

118 ExprToLoc[&CanonE] = &Loc;

119 return Loc;

120}

121

124 auto CanonicalPointeeType =

126 auto Res = NullPointerVals.try_emplace(CanonicalPointeeType, nullptr);

127 if (Res.second) {

130 }

131 return *Res.first->second;

132}

133

140

143 auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint);

144 if (!Res.second) {

145 Res.first->second =

146 &arena().makeAnd(*Res.first->second, Constraint);

147 }

148}

149

152 FlowConditionDeps[ForkToken].insert(Token);

154 return ForkToken;

155}

156

159 Atom SecondToken) {

161 auto &TokenDeps = FlowConditionDeps[Token];

162 TokenDeps.insert(FirstToken);

163 TokenDeps.insert(SecondToken);

165 arena().makeOr(arena().makeAtomRef(FirstToken),

166 arena().makeAtomRef(SecondToken)));

168}

169

171 llvm::SetVector<const Formula *> Constraints) {

172 return S.solve(Constraints.getArrayRef());

173}

174

178 return true;

179

180

181

182

183

184

185 llvm::SetVector<const Formula *> Constraints;

186 Constraints.insert(&arena().makeAtomRef(Token));

187 Constraints.insert(&arena().makeNot(F));

188 addTransitiveFlowConditionConstraints(Token, Constraints);

189 return isUnsatisfiable(std::move(Constraints));

190}

191

195 return false;

196

197 llvm::SetVector<const Formula *> Constraints;

198 Constraints.insert(&arena().makeAtomRef(Token));

199 Constraints.insert(&F);

200 addTransitiveFlowConditionConstraints(Token, Constraints);

201 return isSatisfiable(std::move(Constraints));

202}

203

206 llvm::SetVector<const Formula *> Constraints;

207 Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));

208 return isUnsatisfiable(std::move(Constraints));

209}

210

211llvm::DenseSet DataflowAnalysisContext::collectDependencies(

212 llvm::DenseSet Tokens) const {

213

214

215 std::vector Remaining(Tokens.begin(), Tokens.end());

216 while (!Remaining.empty()) {

217 Atom CurrentToken = Remaining.back();

218 Remaining.pop_back();

219 if (auto DepsIt = FlowConditionDeps.find(CurrentToken);

220 DepsIt != FlowConditionDeps.end())

221 for (Atom A : DepsIt->second)

222 if (Tokens.insert(A).second)

223 Remaining.push_back(A);

224 }

225

226 return Tokens;

227}

228

229void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(

230 Atom Token, llvm::SetVector<const Formula *> &Constraints) {

231 llvm::DenseSet AddedTokens;

232 std::vector Remaining = {Token};

233

236

237 while (!Remaining.empty()) {

238 auto Token = Remaining.back();

239 Remaining.pop_back();

240 if (!AddedTokens.insert(Token).second)

241 continue;

242

243 auto ConstraintsIt = FlowConditionConstraints.find(Token);

244 if (ConstraintsIt == FlowConditionConstraints.end()) {

245

246

247 Constraints.insert(&arena().makeAtomRef(Token));

248 } else {

249

250

251 Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),

252 *ConstraintsIt->second));

253 }

254

255 if (auto DepsIt = FlowConditionDeps.find(Token);

256 DepsIt != FlowConditionDeps.end())

257 for (Atom A : DepsIt->second)

258 Remaining.push_back(A);

259 }

260}

261

263 llvm::DenseSetdataflow::Atom &Refs) {

264 switch (F.kind()) {

266 Refs.insert(F.getAtom());

267 break;

269 break;

272 break;

280 break;

281 }

282}

283

285 llvm::DenseSetdataflow::Atom TargetTokens) const {

287

288

292

293 llvm::DenseSetdataflow::Atom Dependencies =

294 collectDependencies(std::move(TargetTokens));

295

297

298

299 const Formula *Constraints = FlowConditionConstraints.lookup(Token);

300 if (Constraints == nullptr)

301 continue;

303

304 if (auto DepsIt = FlowConditionDeps.find(Token);

305 DepsIt != FlowConditionDeps.end())

307 }

308

309 return LC;

310}

311

314 FlowConditionConstraints = std::move(LC.TokenDefs);

315

316

317

318 FlowConditionDeps = std::move(LC.TokenDeps);

319}

320

322 llvm::raw_ostream &OS) {

323 OS << "(";

324 for (size_t i = 0; i < Atoms.size(); ++i) {

325 OS << Atoms[i];

326 if (i + 1 < Atoms.size())

327 OS << ", ";

328 }

329 OS << ")\n";

330}

331

333 llvm::raw_ostream &OS) {

334 llvm::SetVector<const Formula *> Constraints;

335 Constraints.insert(&arena().makeAtomRef(Token));

336 addTransitiveFlowConditionConstraints(Token, Constraints);

337

338 OS << "Flow condition token: " << Token << "\n";

340 llvm::SetVector<const Formula *> OriginalConstraints = Constraints;

342 if (!Constraints.empty()) {

343 OS << "Constraints:\n";

344 for (const auto *Constraint : Constraints) {

345 Constraint->print(OS);

346 OS << "\n";

347 }

348 }

350 OS << "True atoms: ";

352 }

354 OS << "False atoms: ";

356 }

358 OS << "Equivalent atoms:\n";

361 }

362

363 OS << "\nFlow condition constraints before simplification:\n";

364 for (const auto *Constraint : OriginalConstraints) {

365 Constraint->print(OS);

366 OS << "\n";

367 }

368}

369

372

374 if (F == nullptr)

375 return nullptr;

376 auto It = FunctionContexts.find(F);

377 if (It != FunctionContexts.end())

378 return &It->second;

379

382

383 assert(ACFG);

384 auto Result = FunctionContexts.insert({F, std::move(*ACFG)});

385 return &Result.first->second;

386 }

387

388 return nullptr;

389}

390

394

396 if (auto EC = llvm::sys::fs::create_directories(Dir))

397 llvm::errs() << "Failed to create log dir: " << EC.message() << "\n";

398

399

400

401 static std::atomic Counter = {0};

402 auto StreamFactory =

403 [Dir(Dir.str())]() mutable -> std::unique_ptrllvm::raw\_ostream {

405 llvm::sys::path::append(File,

406 std::to_string(Counter.fetch_add(1)) + ".html");

407 std::error_code EC;

408 auto OS = std::make_uniquellvm::raw\_fd\_ostream(File, EC);

409 if (EC) {

410 llvm::errs() << "Failed to create log " << File << ": " << EC.message()

411 << "\n";

412 return std::make_uniquellvm::raw\_null\_ostream();

413 }

414 return OS;

415 };

416 return Logger::html(std::move(StreamFactory));

417}

418

420 Solver &S, std::unique_ptr &&OwnedSolver, Options Opts)

421 : S(S), OwnedSolver(std::move(OwnedSolver)), A(std::make_unique()),

422 Opts(Opts) {

423

424

425

426 if (Opts.Log == nullptr) {

427 if (DataflowLog.getNumOccurrences() > 0) {

428 LogOwner = makeLoggerFromCommandLine();

429 this->Opts.Log = LogOwner.get();

430

431 } else {

432 this->Opts.Log = &Logger::null();

433 }

434 }

435}

436

437DataflowAnalysisContext::~DataflowAnalysisContext() = default;

438

439}

440}

static llvm:🆑:opt< std::string > DataflowLog("dataflow-log", llvm:🆑:Hidden, llvm:🆑:ValueOptional, llvm:🆑:desc("Emit log of dataflow analysis. With no arg, writes textual " "log to stderr. With an arg, writes HTML logs under the " "specified directory (one per analyzed function)."))

This represents one expression.

Represents a member of a struct/union/class.

Represents a function declaration or definition.

bool doesThisDeclarationHaveABody() const

Returns whether this specific declaration of the function has a body.

FunctionDecl * getDefinition()

Get the definition for this declaration.

A (possibly-)qualified type.

bool isNull() const

Return true if this QualType doesn't point to a type yet.

QualType getNonReferenceType() const

If Type is a reference type (e.g., const int&), returns the type that the reference refers to ("const...

QualType getCanonicalType() const

Token - This structure provides full information about a lexed token.

The base class of the type hierarchy.

bool isRecordType() const

Represent the declaration of a variable (in which case it is an lvalue) a function (in which case it ...

Holds CFG with additional information derived from it that is needed to perform dataflow analysis.

static llvm::Expected< AdornedCFG > build(const FunctionDecl &Func)

Builds an AdornedCFG from a FunctionDecl.

Atom makeFlowConditionToken()

Creates a fresh flow condition and returns a token that identifies it.

const Formula & makeAnd(const Formula &LHS, const Formula &RHS)

Returns a formula for the conjunction of LHS and RHS.

std::enable_if_t< std::is_base_of< StorageLocation, T >::value, T & > create(Args &&...args)

Creates a T (some subclass of StorageLocation), forwarding args to the constructor,...

const AdornedCFG * getAdornedCFG(const FunctionDecl *F)

Returns the AdornedCFG registered for F, if any.

Definition DataflowAnalysisContext.cpp:371

DataflowAnalysisContext(std::unique_ptr< Solver > S, Options Opts=Options{ std::nullopt, nullptr})

Constructs a dataflow analysis context.

Atom joinFlowConditions(Atom FirstToken, Atom SecondToken)

Creates a new flow condition that represents the disjunction of the flow conditions identified by Fir...

Definition DataflowAnalysisContext.cpp:158

void addFlowConditionConstraint(Atom Token, const Formula &Constraint)

Adds Constraint to the flow condition identified by Token.

Definition DataflowAnalysisContext.cpp:141

Atom forkFlowCondition(Atom Token)

Creates a new flow condition with the same constraints as the flow condition identified by Token and ...

Definition DataflowAnalysisContext.cpp:150

bool equivalentFormulas(const Formula &Val1, const Formula &Val2)

Returns true if Val1 is equivalent to Val2.

Definition DataflowAnalysisContext.cpp:204

StorageLocation & getStableStorageLocation(const ValueDecl &D)

Returns a stable storage location for D.

Definition DataflowAnalysisContext.cpp:103

bool flowConditionImplies(Atom Token, const Formula &F)

Returns true if the constraints of the flow condition identified by Token imply that F is true.

Definition DataflowAnalysisContext.cpp:175

Solver::Result querySolver(llvm::SetVector< const Formula * > Constraints)

Returns the outcome of satisfiability checking on Constraints.

Definition DataflowAnalysisContext.cpp:170

bool flowConditionAllows(Atom Token, const Formula &F)

Returns true if the constraints of the flow condition identified by Token still allow F to be true.

Definition DataflowAnalysisContext.cpp:192

PointerValue & getOrCreateNullPointerValue(QualType PointeeType)

Returns a pointer value that represents a null pointer.

Definition DataflowAnalysisContext.cpp:123

void addInvariant(const Formula &Constraint)

Adds Constraint to current and future flow conditions in this context.

Definition DataflowAnalysisContext.cpp:134

llvm::StringMap< QualType > getSyntheticFields(QualType Type)

Returns the names and types of the synthetic fields for the given record type.

StorageLocation & createStorageLocation(QualType Type)

Returns a new storage location appropriate for Type.

Definition DataflowAnalysisContext.cpp:61

SimpleLogicalContext exportLogicalContext(llvm::DenseSet< dataflow::Atom > TargetTokens) const

Export the logical-context portions of AC, limited to the given target flow-condition tokens.

Definition DataflowAnalysisContext.cpp:284

FieldSet getModeledFields(QualType Type)

Returns the fields of Type, limited to the set of fields modeled by this context.

Definition DataflowAnalysisContext.cpp:43

LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token, llvm::raw_ostream &OS=llvm::dbgs())

Definition DataflowAnalysisContext.cpp:332

void initLogicalContext(SimpleLogicalContext LC)

Initializes this context's "logical" components with LC.

Definition DataflowAnalysisContext.cpp:312

RecordStorageLocation & createRecordStorageLocation(QualType Type, RecordStorageLocation::FieldToLoc FieldLocs, RecordStorageLocation::SyntheticFieldMap SyntheticFields)

Creates a RecordStorageLocation for the given type and with the given fields.

Definition DataflowAnalysisContext.cpp:90

ArrayRef< const Formula * > operands() const

bool isLiteral(bool b) const

@ Equal

True if LHS is false or RHS is true.

@ Implies

True if either LHS or RHS is true.

@ AtomRef

A reference to an atomic boolean variable.

@ Literal

Constant true or false.

@ Or

True if LHS and RHS are both true.

@ And

True if its only operand is false.

static std::unique_ptr< Logger > textual(llvm::raw_ostream &)

A logger that simply writes messages to the specified ostream in real time.

static std::unique_ptr< Logger > html(std::function< std::unique_ptr< llvm::raw_ostream >()>)

A logger that builds an HTML UI to inspect the analysis results.

Models a symbolic pointer. Specifically, any value of type T*.

A storage location for a record (struct, class, or union).

llvm::DenseMap< const ValueDecl *, StorageLocation * > FieldToLoc

llvm::StringMap< StorageLocation * > SyntheticFieldMap

A storage location that is not subdivided further for the purposes of abstract interpretation.

Base class for elements of the local variable store and of the heap.

static void getReferencedAtoms(const Formula &F, llvm::DenseSet< dataflow::Atom > &Refs)

Definition DataflowAnalysisContext.cpp:262

Atom

Identifies an atomic boolean variable such as "V1".

static void printAtomList(const llvm::SmallVector< Atom > &Atoms, llvm::raw_ostream &OS)

Definition DataflowAnalysisContext.cpp:321

void simplifyConstraints(llvm::SetVector< const Formula * > &Constraints, Arena &arena, SimplifyConstraintsInfo *Info=nullptr)

Simplifies a set of constraints (implicitly connected by "and") in a way that does not change satisfi...

const Expr & ignoreCFGOmittedNodes(const Expr &E)

Skip past nodes that the CFG does not emit.

FieldSet getObjectFields(QualType Type)

Returns the set of all fields in the type.

static std::unique_ptr< Logger > makeLoggerFromCommandLine()

Definition DataflowAnalysisContext.cpp:391

static llvm::DenseSet< llvm::StringRef > getKeys(const llvm::StringMap< T > &Map)

Definition DataflowAnalysisContext.cpp:86

bool containsSameFields(const FieldSet &Fields, const RecordStorageLocation::FieldToLoc &FieldLocs)

Returns whether Fields and FieldLocs contain the same fields.

llvm::SmallSetVector< const FieldDecl *, 4 > FieldSet

A set of FieldDecl *.

The JSON file list parser is used to communicate input to InstallAPI.

@ Result

The result type of a method or function.

@ Invariant

The parameter is invariant: must match exactly.

@ Class

The "class" keyword introduces the elaborated-type-specifier.

A simple representation of essential elements of the logical context used in environments.

llvm::DenseMap< Atom, const Formula * > TokenDefs

const Formula * Invariant

llvm::DenseMap< Atom, llvm::DenseSet< Atom > > TokenDeps

Information on the way a set of constraints was simplified.

llvm::SmallVector< Atom > TrueAtoms

Atoms that the original constraints imply must be true.

llvm::SmallVector< llvm::SmallVector< Atom > > EquivalentAtoms

List of equivalence classes of atoms.

llvm::SmallVector< Atom > FalseAtoms

Atoms that the original constraints imply must be false.