[PATCH] D128363: [clang][dataflow] Implement functionality for flow condition variable substitution.

weiyi via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Fri Jun 24 06:32:53 PDT 2022


wyt marked 3 inline comments as done.
wyt added a comment.

@xazax.hun

> Could you elaborate on why do we need this?

We are currently working on a pointer nullability analysis here: https://github.com/google/crubit/tree/main/nullability_verification.
One of the things we are trying to do is to check if the flow condition is independent of a variable, done by checking if the formula regardless if the variable is substituted to true or false - requiring `buildAndSubstituteFlowCondition`.

> Why do we care about how flow condition constraints are represented? We should use the solver to ask questions and as far as I understand the solver should work with both representations.

The first approach of representing flow conditions as an atomic boolean token, places the responsibility on the user to handle adding the constraints of the flow condition when checking with the solver. 
The second approach of representing flow conditions as a direct conjunction of its constraints, has performance implications as any boolean values with the flow condition appearing in it may grow in size, and the entire conjunction of the flow condition has to be added repeatedly if the flow condition appears in multiple places.

> Also this function feels like doing two things, building the flow condition from the tokens and doing substitutions. Any reason why those two are not separate functions? Is this for performance reasons?

You'd build the flow condition by passing in an empty substitutions set. Also, just building the flow condition does not see any use currently.



================
Comment at: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp:177
+    auto &Sub = substituteBoolVal(Negation.getSubVal(), SubstitutionsCache);
+    Result = &getOrCreateNegationValue(Sub);
+    break;
----------------
@gribozavr2 
> Could you refactor it into a free function? It does not use 'this', seems like.
We store and retrieve BoolVals in DataflowAnalysisContext. Example as highlighted.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D128363/new/

https://reviews.llvm.org/D128363



More information about the cfe-commits mailing list