clang 23.0.0git
DataflowAnalysisContext.cpp
Go to the documentation of this file.
1//===-- DataflowAnalysisContext.cpp -----------------------------*- C++ -*-===//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8//
9// This file defines a DataflowAnalysisContext class that owns objects that
10// encompass the state of a program and stores context that is used during
11// dataflow analysis.
12//
13//===----------------------------------------------------------------------===//
14
16#include "clang/AST/Type.h"
22#include "clang/Basic/LLVM.h"
23#include "llvm/ADT/DenseSet.h"
24#include "llvm/ADT/SetOperations.h"
25#include "llvm/ADT/SetVector.h"
26#include "llvm/Support/CommandLine.h"
27#include "llvm/Support/Debug.h"
28#include "llvm/Support/FileSystem.h"
29#include "llvm/Support/Path.h"
30#include "llvm/Support/raw_ostream.h"
31#include <cassert>
32#include <memory>
33#include <stack>
34#include <string>
35#include <utility>
36#include <vector>
37
38static llvm::cl::opt<std::string> DataflowLog(
39 "dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
40 llvm::cl::desc("Emit log of dataflow analysis. With no arg, writes textual "
41 "log to stderr. With an arg, writes HTML logs under the "
42 "specified directory (one per analyzed function)."));
43
44namespace clang {
45namespace dataflow {
46
47FieldSet DataflowAnalysisContext::computeModeledFields(QualType Type) {
48 // During context-sensitive analysis, a struct may be allocated in one
49 // function, but its field accessed in a function lower in the stack than
50 // the allocation. Since we only collect fields used in the function where
51 // the allocation occurs, we can't apply that filter when performing
52 // context-sensitive analysis. But, this only applies to storage locations,
53 // since field access it not allowed to fail. In contrast, field *values*
54 // don't need this allowance, since the API allows for uninitialized fields.
55 if (Opts.ContextSensitiveOpts)
56 return getObjectFields(Type);
57
58 return llvm::set_intersection(getObjectFields(Type), ModeledFields);
59}
60
62 QualType CanonicalType = Type.getCanonicalType().getUnqualifiedType();
63 std::unique_ptr<FieldSet> &Fields = CachedModeledFields[CanonicalType];
64 if (Fields == nullptr)
65 Fields = std::make_unique<FieldSet>(computeModeledFields(CanonicalType));
66 return *Fields;
67}
68
69void DataflowAnalysisContext::addModeledFields(const FieldSet &Fields) {
70 ModeledFields.set_union(Fields);
71 CachedModeledFields.clear();
72}
73
75 if (!Type.isNull() && Type->isRecordType()) {
76 llvm::DenseMap<const ValueDecl *, StorageLocation *> FieldLocs;
77 for (const FieldDecl *Field : getModeledFields(Type))
78 if (Field->getType()->isReferenceType())
79 FieldLocs.insert({Field, nullptr});
80 else
81 FieldLocs.insert({Field, &createStorageLocation(
82 Field->getType().getNonReferenceType())});
83
85 for (const auto &Entry : getSyntheticFields(Type))
86 SyntheticFields.insert(
87 {Entry.getKey(),
88 &createStorageLocation(Entry.getValue().getNonReferenceType())});
89
90 return createRecordStorageLocation(Type, std::move(FieldLocs),
91 std::move(SyntheticFields));
92 }
94}
95
96// Returns the keys for a given `StringMap`.
97// Can't use `StringSet` as the return type as it doesn't support `operator==`.
98template <typename T>
99static llvm::DenseSet<llvm::StringRef> getKeys(const llvm::StringMap<T> &Map) {
100 return llvm::DenseSet<llvm::StringRef>(llvm::from_range, Map.keys());
101}
102
106 assert(Type->isRecordType());
107 assert(containsSameFields(getModeledFields(Type), FieldLocs));
108 assert(getKeys(getSyntheticFields(Type)) == getKeys(SyntheticFields));
109
110 RecordStorageLocationCreated = true;
111 return arena().create<RecordStorageLocation>(Type, std::move(FieldLocs),
112 std::move(SyntheticFields));
113}
114
117 if (auto *Loc = DeclToLoc.lookup(&D))
118 return *Loc;
120 DeclToLoc[&D] = &Loc;
121 return Loc;
122}
123
126 const Expr &CanonE = ignoreCFGOmittedNodes(E);
127
128 if (auto *Loc = ExprToLoc.lookup(&CanonE))
129 return *Loc;
130 auto &Loc = createStorageLocation(CanonE.getType());
131 ExprToLoc[&CanonE] = &Loc;
132 return Loc;
133}
134
137 auto CanonicalPointeeType =
138 PointeeType.isNull() ? PointeeType : PointeeType.getCanonicalType();
139 auto Res = NullPointerVals.try_emplace(CanonicalPointeeType, nullptr);
140 if (Res.second) {
141 auto &PointeeLoc = createStorageLocation(CanonicalPointeeType);
142 Res.first->second = &arena().create<PointerValue>(PointeeLoc);
143 }
144 return *Res.first->second;
145}
146
148 if (Invariant == nullptr)
149 Invariant = &Constraint;
150 else
151 Invariant = &arena().makeAnd(*Invariant, Constraint);
152}
153
155 Atom Token, const Formula &Constraint) {
156 auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint);
157 if (!Res.second) {
158 Res.first->second =
159 &arena().makeAnd(*Res.first->second, Constraint);
160 }
161}
162
164 Atom ForkToken = arena().makeFlowConditionToken();
165 FlowConditionDeps[ForkToken].insert(Token);
166 addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token));
167 return ForkToken;
168}
169
170Atom
172 Atom SecondToken) {
174 auto &TokenDeps = FlowConditionDeps[Token];
175 TokenDeps.insert(FirstToken);
176 TokenDeps.insert(SecondToken);
178 arena().makeOr(arena().makeAtomRef(FirstToken),
179 arena().makeAtomRef(SecondToken)));
180 return Token;
181}
182
184 llvm::SetVector<const Formula *> Constraints) {
185 return S.solve(Constraints.getArrayRef());
186}
187
189 const Formula &F) {
190 if (F.isLiteral(true))
191 return true;
192
193 // Returns true if and only if truth assignment of the flow condition implies
194 // that `F` is also true. We prove whether or not this property holds by
195 // reducing the problem to satisfiability checking. In other words, we attempt
196 // to show that assuming `F` is false makes the constraints induced by the
197 // flow condition unsatisfiable.
198 llvm::SetVector<const Formula *> Constraints;
199 Constraints.insert(&arena().makeAtomRef(Token));
200 Constraints.insert(&arena().makeNot(F));
201 addTransitiveFlowConditionConstraints(Token, Constraints);
202 return isUnsatisfiable(std::move(Constraints));
203}
204
206 const Formula &F) {
207 if (F.isLiteral(false))
208 return false;
209
210 llvm::SetVector<const Formula *> Constraints;
211 Constraints.insert(&arena().makeAtomRef(Token));
212 Constraints.insert(&F);
213 addTransitiveFlowConditionConstraints(Token, Constraints);
214 return isSatisfiable(std::move(Constraints));
215}
216
218 const Formula &Val2) {
219 llvm::SetVector<const Formula *> Constraints;
220 Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));
221 return isUnsatisfiable(std::move(Constraints));
222}
223
224llvm::DenseSet<Atom> DataflowAnalysisContext::collectDependencies(
225 llvm::DenseSet<Atom> Tokens) const {
226 // Use a worklist algorithm, with `Remaining` holding the worklist and
227 // `Tokens` tracking which atoms have already been added to the worklist.
228 std::vector<Atom> Remaining(Tokens.begin(), Tokens.end());
229 while (!Remaining.empty()) {
230 Atom CurrentToken = Remaining.back();
231 Remaining.pop_back();
232 if (auto DepsIt = FlowConditionDeps.find(CurrentToken);
233 DepsIt != FlowConditionDeps.end())
234 for (Atom A : DepsIt->second)
235 if (Tokens.insert(A).second)
236 Remaining.push_back(A);
237 }
238
239 return Tokens;
240}
241
242void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
243 Atom Token, llvm::SetVector<const Formula *> &Constraints) {
244 llvm::DenseSet<Atom> AddedTokens;
245 std::vector<Atom> Remaining = {Token};
246
247 if (Invariant)
248 Constraints.insert(Invariant);
249 // Define all the flow conditions that might be referenced in constraints.
250 while (!Remaining.empty()) {
251 auto Token = Remaining.back();
252 Remaining.pop_back();
253 if (!AddedTokens.insert(Token).second)
254 continue;
255
256 auto ConstraintsIt = FlowConditionConstraints.find(Token);
257 if (ConstraintsIt == FlowConditionConstraints.end()) {
258 // The flow condition is unconstrained. Just add the atom directly, which
259 // is equivalent to asserting it is true.
260 Constraints.insert(&arena().makeAtomRef(Token));
261 } else {
262 // Bind flow condition token via `iff` to its set of constraints:
263 // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
264 Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
265 *ConstraintsIt->second));
266 }
267
268 if (auto DepsIt = FlowConditionDeps.find(Token);
269 DepsIt != FlowConditionDeps.end())
270 for (Atom A : DepsIt->second)
271 Remaining.push_back(A);
272 }
273}
274
275static void getReferencedAtoms(const Formula &F,
276 llvm::DenseSet<dataflow::Atom> &Refs) {
277 // Avoid recursion to avoid stack overflows from very large formulas.
278 // The shape of the tree structure for very large formulas is such that there
279 // are at most 2 children from any node, but there may be many generations.
280 std::stack<const Formula *> WorkList;
281 WorkList.push(&F);
282
283 while (!WorkList.empty()) {
284 const Formula *Current = WorkList.top();
285 WorkList.pop();
286 switch (Current->kind()) {
287 case Formula::AtomRef:
288 Refs.insert(Current->getAtom());
289 break;
290 case Formula::Literal:
291 break;
292 case Formula::Not:
293 WorkList.push(Current->operands()[0]);
294 break;
295 case Formula::And:
296 case Formula::Or:
297 case Formula::Implies:
298 case Formula::Equal:
299 ArrayRef<const Formula *> Operands = Current->operands();
300 WorkList.push(Operands[0]);
301 WorkList.push(Operands[1]);
302 break;
303 }
304 }
305}
306
308 llvm::DenseSet<dataflow::Atom> TargetTokens) const {
310
311 // Copy `Invariant` even if it is null, to initialize the field.
312 LC.Invariant = Invariant;
313 if (Invariant != nullptr)
314 getReferencedAtoms(*Invariant, TargetTokens);
315
316 llvm::DenseSet<dataflow::Atom> Dependencies =
317 collectDependencies(std::move(TargetTokens));
318
319 for (dataflow::Atom Token : Dependencies) {
320 // Only process the token if it is constrained. Unconstrained tokens don't
321 // have dependencies.
322 const Formula *Constraints = FlowConditionConstraints.lookup(Token);
323 if (Constraints == nullptr)
324 continue;
325 LC.TokenDefs[Token] = Constraints;
326
327 if (auto DepsIt = FlowConditionDeps.find(Token);
328 DepsIt != FlowConditionDeps.end())
329 LC.TokenDeps[Token] = DepsIt->second;
330 }
331
332 return LC;
333}
334
336 Invariant = LC.Invariant;
337 FlowConditionConstraints = std::move(LC.TokenDefs);
338 // TODO: The dependencies in `LC.TokenDeps` can be reconstructed from
339 // `LC.TokenDefs`. Give the caller the option to reconstruct, rather than
340 // providing them directly, to save caller space (memory/disk).
341 FlowConditionDeps = std::move(LC.TokenDeps);
342}
343
344static void printAtomList(const llvm::SmallVector<Atom> &Atoms,
345 llvm::raw_ostream &OS) {
346 OS << "(";
347 for (size_t i = 0; i < Atoms.size(); ++i) {
348 OS << Atoms[i];
349 if (i + 1 < Atoms.size())
350 OS << ", ";
351 }
352 OS << ")\n";
353}
354
356 llvm::raw_ostream &OS) {
357 llvm::SetVector<const Formula *> Constraints;
358 Constraints.insert(&arena().makeAtomRef(Token));
359 addTransitiveFlowConditionConstraints(Token, Constraints);
360
361 OS << "Flow condition token: " << Token << "\n";
363 llvm::SetVector<const Formula *> OriginalConstraints = Constraints;
364 simplifyConstraints(Constraints, arena(), &Info);
365 if (!Constraints.empty()) {
366 OS << "Constraints:\n";
367 for (const auto *Constraint : Constraints) {
368 Constraint->print(OS);
369 OS << "\n";
370 }
371 }
372 if (!Info.TrueAtoms.empty()) {
373 OS << "True atoms: ";
374 printAtomList(Info.TrueAtoms, OS);
375 }
376 if (!Info.FalseAtoms.empty()) {
377 OS << "False atoms: ";
378 printAtomList(Info.FalseAtoms, OS);
379 }
380 if (!Info.EquivalentAtoms.empty()) {
381 OS << "Equivalent atoms:\n";
383 printAtomList(Class, OS);
384 }
385
386 OS << "\nFlow condition constraints before simplification:\n";
387 for (const auto *Constraint : OriginalConstraints) {
388 Constraint->print(OS);
389 OS << "\n";
390 }
391}
392
393const AdornedCFG *
395 // Canonicalize the key:
396 F = F->getDefinition();
397 if (F == nullptr)
398 return nullptr;
399 auto It = FunctionContexts.find(F);
400 if (It != FunctionContexts.end())
401 return &It->second;
402
404 auto ACFG = AdornedCFG::build(*F);
405 // FIXME: Handle errors.
406 assert(ACFG);
407 auto Result = FunctionContexts.insert({F, std::move(*ACFG)});
408 return &Result.first->second;
409 }
410
411 return nullptr;
412}
413
414static std::unique_ptr<Logger> makeLoggerFromCommandLine() {
415 if (DataflowLog.empty())
416 return Logger::textual(llvm::errs());
417
418 llvm::StringRef Dir = DataflowLog;
419 if (auto EC = llvm::sys::fs::create_directories(Dir))
420 llvm::errs() << "Failed to create log dir: " << EC.message() << "\n";
421 // All analysis runs within a process will log to the same directory.
422 // Share a counter so they don't all overwrite each other's 0.html.
423 // (Don't share a logger, it's not threadsafe).
424 static std::atomic<unsigned> Counter = {0};
425 auto StreamFactory =
426 [Dir(Dir.str())]() mutable -> std::unique_ptr<llvm::raw_ostream> {
428 llvm::sys::path::append(File,
429 std::to_string(Counter.fetch_add(1)) + ".html");
430 std::error_code EC;
431 auto OS = std::make_unique<llvm::raw_fd_ostream>(File, EC);
432 if (EC) {
433 llvm::errs() << "Failed to create log " << File << ": " << EC.message()
434 << "\n";
435 return std::make_unique<llvm::raw_null_ostream>();
436 }
437 return OS;
438 };
439 return Logger::html(std::move(StreamFactory));
440}
441
443 Solver &S, std::unique_ptr<Solver> &&OwnedSolver, Options Opts)
444 : S(S), OwnedSolver(std::move(OwnedSolver)), A(std::make_unique<Arena>()),
445 Opts(Opts) {
446 // If the -dataflow-log command-line flag was set, synthesize a logger.
447 // This is ugly but provides a uniform method for ad-hoc debugging dataflow-
448 // based tools.
449 if (Opts.Log == nullptr) {
450 if (DataflowLog.getNumOccurrences() > 0) {
451 LogOwner = makeLoggerFromCommandLine();
452 this->Opts.Log = LogOwner.get();
453 // FIXME: if the flag is given a value, write an HTML log to a file.
454 } else {
455 this->Opts.Log = &Logger::null();
456 }
457 }
458}
459
460DataflowAnalysisContext::~DataflowAnalysisContext() = default;
461
462} // namespace dataflow
463} // namespace clang
static llvm::cl::opt< std::string > DataflowLog("dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional, llvm::cl::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)."))
Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified.
C Language Family Type Representation.
This represents one expression.
Definition Expr.h:112
QualType getType() const
Definition Expr.h:144
Represents a member of a struct/union/class.
Definition Decl.h:3160
Represents a function declaration or definition.
Definition Decl.h:2000
bool doesThisDeclarationHaveABody() const
Returns whether this specific declaration of the function has a body.
Definition Decl.h:2326
FunctionDecl * getDefinition()
Get the definition for this declaration.
Definition Decl.h:2282
A (possibly-)qualified type.
Definition TypeBase.h:937
bool isNull() const
Return true if this QualType doesn't point to a type yet.
Definition TypeBase.h:1004
QualType getNonReferenceType() const
If Type is a reference type (e.g., const int&), returns the type that the reference refers to ("const...
Definition TypeBase.h:8573
QualType getCanonicalType() const
Definition TypeBase.h:8440
Token - This structure provides full information about a lexed token.
Definition Token.h:36
The base class of the type hierarchy.
Definition TypeBase.h:1839
bool isRecordType() const
Definition TypeBase.h:8752
Represent the declaration of a variable (in which case it is an lvalue) a function (in which case it ...
Definition Decl.h:712
QualType getType() const
Definition Decl.h:723
Holds CFG with additional information derived from it that is needed to perform dataflow analysis.
Definition AdornedCFG.h:47
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.
Definition Arena.h:124
const Formula & makeAnd(const Formula &LHS, const Formula &RHS)
Returns a formula for the conjunction of LHS and RHS.
Definition Arena.cpp:41
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,...
Definition Arena.h:36
const AdornedCFG * getAdornedCFG(const FunctionDecl *F)
Returns the AdornedCFG registered for F, if any.
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...
void addFlowConditionConstraint(Atom Token, const Formula &Constraint)
Adds Constraint to the flow condition identified by Token.
Atom forkFlowCondition(Atom Token)
Creates a new flow condition with the same constraints as the flow condition identified by Token and ...
bool equivalentFormulas(const Formula &Val1, const Formula &Val2)
Returns true if Val1 is equivalent to Val2.
StorageLocation & getStableStorageLocation(const ValueDecl &D)
Returns a stable storage location for D.
bool flowConditionImplies(Atom Token, const Formula &F)
Returns true if the constraints of the flow condition identified by Token imply that F is true.
Solver::Result querySolver(llvm::SetVector< const Formula * > Constraints)
Returns the outcome of satisfiability checking on Constraints.
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.
const FieldSet & getModeledFields(QualType Type)
Returns the fields of Type, limited to the set of fields modeled by this context.
PointerValue & getOrCreateNullPointerValue(QualType PointeeType)
Returns a pointer value that represents a null pointer.
void addInvariant(const Formula &Constraint)
Adds Constraint to current and future flow conditions in this context.
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.
SimpleLogicalContext exportLogicalContext(llvm::DenseSet< dataflow::Atom > TargetTokens) const
Export the logical-context portions of AC, limited to the given target flow-condition tokens.
LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token, llvm::raw_ostream &OS=llvm::dbgs())
void initLogicalContext(SimpleLogicalContext LC)
Initializes this context's "logical" components with LC.
RecordStorageLocation & createRecordStorageLocation(QualType Type, RecordStorageLocation::FieldToLoc FieldLocs, RecordStorageLocation::SyntheticFieldMap SyntheticFields)
Creates a RecordStorageLocation for the given type and with the given fields.
ArrayRef< const Formula * > operands() const
Definition Formula.h:82
bool isLiteral(bool b) const
Definition Formula.h:78
Atom getAtom() const
Definition Formula.h:68
@ Equal
True if LHS is false or RHS is true.
Definition Formula.h:64
@ Implies
True if either LHS or RHS is true.
Definition Formula.h:63
@ AtomRef
A reference to an atomic boolean variable.
Definition Formula.h:54
@ Literal
Constant true or false.
Definition Formula.h:56
@ Or
True if LHS and RHS are both true.
Definition Formula.h:62
@ And
True if its only operand is false.
Definition Formula.h:61
Kind kind() const
Definition Formula.h:66
static std::unique_ptr< Logger > textual(llvm::raw_ostream &)
A logger that simply writes messages to the specified ostream in real time.
Definition Logger.cpp:107
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*.
Definition Value.h:170
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)
Atom
Identifies an atomic boolean variable such as "V1".
Definition Formula.h:34
static void printAtomList(const llvm::SmallVector< Atom > &Atoms, llvm::raw_ostream &OS)
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.
Definition ASTOps.cpp:35
FieldSet getObjectFields(QualType Type)
Returns the set of all fields in the type.
Definition ASTOps.cpp:74
static std::unique_ptr< Logger > makeLoggerFromCommandLine()
static llvm::DenseSet< llvm::StringRef > getKeys(const llvm::StringMap< T > &Map)
bool containsSameFields(const FieldSet &Fields, const RecordStorageLocation::FieldToLoc &FieldLocs)
Returns whether Fields and FieldLocs contain the same fields.
Definition ASTOps.cpp:80
llvm::SmallSetVector< const FieldDecl *, 4 > FieldSet
A set of FieldDecl *.
Definition ASTOps.h:42
The JSON file list parser is used to communicate input to InstallAPI.
@ Result
The result type of a method or function.
Definition TypeBase.h:905
@ Invariant
The parameter is invariant: must match exactly.
Definition DeclObjC.h:555
@ Class
The "class" keyword introduces the elaborated-type-specifier.
Definition TypeBase.h:5925
A simple representation of essential elements of the logical context used in environments.
llvm::DenseMap< Atom, const Formula * > TokenDefs
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.