return Model.compareEquivalent(Type, *Val1, Env1, *Val2, Env2);
}
+/// Attempts to merge distinct values `Val1` and `Val1` in `Env1` and `Env2`,
+/// respectively, of the same type `Type`. Merging generally produces a single
+/// value that (soundly) approximates the two inputs, although the actual
+/// meaning depends on `Model`.
+static Value *mergeDistinctValues(QualType Type, Value *Val1, Environment &Env1,
+ Value *Val2, const Environment &Env2,
+ Environment::ValueModel &Model) {
+ // Join distinct boolean values preserving information about the constraints
+ // in the respective path conditions. Note: this construction can, in
+ // principle, result in exponential growth in the size of boolean values.
+ // Potential optimizations may be worth considering. For example, represent
+ // the flow condition of each environment using a bool atom and store, in
+ // `DataflowAnalysisContext`, a mapping of bi-conditionals between flow
+ // condition atoms and flow condition constraints. Something like:
+ // \code
+ // FC1 <=> C1 ^ C2
+ // FC2 <=> C2 ^ C3 ^ C4
+ // FC3 <=> (FC1 v FC2) ^ C5
+ // \code
+ // Then, we can track dependencies between flow conditions (e.g. above `FC3`
+ // depends on `FC1` and `FC2`) and modify `flowConditionImplies` to construct
+ // a formula that includes the bi-conditionals for all flow condition atoms in
+ // the transitive set, before invoking the solver.
+ if (auto *Expr1 = dyn_cast<BoolValue>(Val1)) {
+ for (BoolValue *Constraint : Env1.getFlowConditionConstraints()) {
+ Expr1 = &Env1.makeAnd(*Expr1, *Constraint);
+ }
+ auto *Expr2 = cast<BoolValue>(Val2);
+ for (BoolValue *Constraint : Env2.getFlowConditionConstraints()) {
+ Expr2 = &Env1.makeAnd(*Expr2, *Constraint);
+ }
+ return &Env1.makeOr(*Expr1, *Expr2);
+ }
+
+ // FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
+ // returns false to avoid storing unneeded values in `DACtx`.
+ if (Value *MergedVal = Env1.createValue(Type))
+ if (Model.merge(Type, *Val1, Env1, *Val2, Env2, *MergedVal, Env1))
+ return MergedVal;
+
+ return nullptr;
+}
+
/// Initializes a global storage value.
static void initGlobalVar(const VarDecl &D, Environment &Env) {
if (!D.hasGlobalStorage() ||
continue;
}
- // FIXME: Consider destroying `MergedValue` immediately if
- // `ValueModel::merge` returns false to avoid storing unneeded values in
- // `DACtx`.
- if (Value *MergedVal = createValue(Loc->getType()))
- if (Model.merge(Loc->getType(), *Val, *this, *It->second, Other,
- *MergedVal, *this))
- LocToVal.insert({Loc, MergedVal});
+ if (Value *MergedVal = mergeDistinctValues(Loc->getType(), Val, *this,
+ It->second, Other, Model))
+ LocToVal.insert({Loc, MergedVal});
}
if (OldLocToVal.size() != LocToVal.size())
Effect = LatticeJoinEffect::Changed;
using ::testing::IsNull;
using ::testing::NotNull;
using ::testing::Pair;
+using ::testing::SizeIs;
class TransferTest : public ::testing::Test {
protected:
});
}
+TEST_F(TransferTest, CorrelatedBranches) {
+ std::string Code = R"(
+ void target(bool B, bool C) {
+ if (B) {
+ return;
+ }
+ (void)0;
+ /*[[p0]]*/
+ if (C) {
+ B = true;
+ /*[[p1]]*/
+ }
+ if (B) {
+ (void)0;
+ /*[[p2]]*/
+ }
+ }
+ )";
+ runDataflow(
+ Code, [](llvm::ArrayRef<
+ std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+ Results,
+ ASTContext &ASTCtx) {
+ ASSERT_THAT(Results, SizeIs(3));
+
+ const ValueDecl *CDecl = findValueDecl(ASTCtx, "C");
+ ASSERT_THAT(CDecl, NotNull());
+
+ {
+ ASSERT_THAT(Results[2], Pair("p0", _));
+ const Environment &Env = Results[2].second.Env;
+ const ValueDecl *BDecl = findValueDecl(ASTCtx, "B");
+ ASSERT_THAT(BDecl, NotNull());
+ auto &BVal = *cast<BoolValue>(Env.getValue(*BDecl, SkipPast::None));
+
+ EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BVal)));
+ }
+
+ {
+ ASSERT_THAT(Results[1], Pair("p1", _));
+ const Environment &Env = Results[1].second.Env;
+ auto &CVal = *cast<BoolValue>(Env.getValue(*CDecl, SkipPast::None));
+ EXPECT_TRUE(Env.flowConditionImplies(CVal));
+ }
+
+ {
+ ASSERT_THAT(Results[0], Pair("p2", _));
+ const Environment &Env = Results[0].second.Env;
+ auto &CVal = *cast<BoolValue>(Env.getValue(*CDecl, SkipPast::None));
+ EXPECT_TRUE(Env.flowConditionImplies(CVal));
+ }
+ });
+}
+
} // namespace