This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rGfa689726768b: [dataflow] document flow condition (authored
by sammccall).
Changed prior to commit:
https://reviews.llvm.org/D154969?vs=539086&id=539381#toc
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D154969/new/
https://reviews.llvm.org/D154969
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -22,6 +22,7 @@
#include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Logger.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
@@ -524,16 +525,30 @@
arena().makeEquals(LHS.formula(), RHS.formula()));
}
- /// Returns the token that identifies the flow condition of the environment.
+ /// Returns a boolean variable that identifies the flow condition (FC).
+ ///
+ /// The flow condition is a set of facts that are necessarily true when the
+ /// program reaches the current point, expressed as boolean formulas.
+ /// The flow condition token is equivalent to the AND of these facts.
+ ///
+ /// These may e.g. constrain the value of certain variables. A pointer
+ /// variable may have a consistent modeled PointerValue throughout, but at a
+ /// given point the Environment may tell us that the value must be non-null.
+ ///
+ /// The FC is necessary but not sufficient for this point to be reachable.
+ /// In particular, where the FC token appears in flow conditions of successor
+ /// environments, it means "point X may have been reached", not
+ /// "point X was reached".
Atom getFlowConditionToken() const { return FlowConditionToken; }
- /// Adds `Val` to the set of clauses that constitute the flow condition.
+ /// Record a fact that must be true if this point in the program is reached.
void addToFlowCondition(const Formula &);
/// Deprecated: Use Formula version instead.
void addToFlowCondition(BoolValue &Val);
- /// Returns true if and only if the clauses that constitute the flow
condition
- /// imply that `Val` is true.
+ /// Returns true if the formula is always true when this point is reached.
+ /// Returns false if the formula may be false, or if the flow condition isn't
+ /// sufficiently precise to prove that it is true.
bool flowConditionImplies(const Formula &) const;
/// Deprecated: Use Formula version instead.
bool flowConditionImplies(BoolValue &Val) const;
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -22,6 +22,7 @@
#include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Logger.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
@@ -524,16 +525,30 @@
arena().makeEquals(LHS.formula(), RHS.formula()));
}
- /// Returns the token that identifies the flow condition of the environment.
+ /// Returns a boolean variable that identifies the flow condition (FC).
+ ///
+ /// The flow condition is a set of facts that are necessarily true when the
+ /// program reaches the current point, expressed as boolean formulas.
+ /// The flow condition token is equivalent to the AND of these facts.
+ ///
+ /// These may e.g. constrain the value of certain variables. A pointer
+ /// variable may have a consistent modeled PointerValue throughout, but at a
+ /// given point the Environment may tell us that the value must be non-null.
+ ///
+ /// The FC is necessary but not sufficient for this point to be reachable.
+ /// In particular, where the FC token appears in flow conditions of successor
+ /// environments, it means "point X may have been reached", not
+ /// "point X was reached".
Atom getFlowConditionToken() const { return FlowConditionToken; }
- /// Adds `Val` to the set of clauses that constitute the flow condition.
+ /// Record a fact that must be true if this point in the program is reached.
void addToFlowCondition(const Formula &);
/// Deprecated: Use Formula version instead.
void addToFlowCondition(BoolValue &Val);
- /// Returns true if and only if the clauses that constitute the flow condition
- /// imply that `Val` is true.
+ /// Returns true if the formula is always true when this point is reached.
+ /// Returns false if the formula may be false, or if the flow condition isn't
+ /// sufficiently precise to prove that it is true.
bool flowConditionImplies(const Formula &) const;
/// Deprecated: Use Formula version instead.
bool flowConditionImplies(BoolValue &Val) const;
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
