[PATCH] D154969: [dataflow] document flow condition

[Sam McCall via Phabricator via cfe-commits]

sammccall created this revision.
sammccall added a reviewer: ymandel.
Herald added subscribers: martong, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
sammccall requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

There's some documentation of this concept at
https://clang.llvm.org/docs/DataFlowAnalysisIntro.html
but it would be nice to have it closer to the code.

I also was laboring under an obvious but wrong mental model that
the flow condition token represented "execution reached this point",
I'd like to explicitly call that out as wrong.


Repository:
  rG LLVM Github Monorepo

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.
+  ///
+  /// 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;


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D154969.539086.patch
Type: text/x-patch
Size: 2515 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230711/38c479c4/attachment-0001.bin>