[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rG39b9d4f188ca: [clang][dataflow] Add support for a Top value
in boolean formulas. (authored by ymandel).
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -310,6 +311,9 @@
}
// Models an analysis that uses flow conditions.
+//
+// FIXME: Here and below: change class to final and final methods to override,
+// since we're marking them all as final.
class SpecialBoolAnalysis
: public DataflowAnalysis {
public:
@@ -322,7 +326,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +472,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +481,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +520,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type,
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel updated this revision to Diff 467822.
ymandel marked an inline comment as done.
ymandel added a comment.
rebase onto a recent HEAD
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -310,6 +311,9 @@
}
// Models an analysis that uses flow conditions.
+//
+// FIXME: Here and below: change class to final and final methods to override,
+// since we're marking them all as final.
class SpecialBoolAnalysis
: public DataflowAnalysis {
public:
@@ -322,7 +326,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +472,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +481,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +520,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type, const Value , const Environment ,
@@ -538,11 +546,9 @@
if (HasValue1 == HasValue2)
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel marked an inline comment as done.
ymandel added inline comments.
Comment at: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp:69
-TEST(SolverTest, UnitConflict) {
- ConstraintContext Ctx;
gribozavr2 wrote:
> Why delete this test?
That was a mistake. I've added it back
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel updated this revision to Diff 467746.
ymandel marked an inline comment as done.
ymandel added a comment.
Adding back accidentally deleted test
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -310,6 +311,9 @@
}
// Models an analysis that uses flow conditions.
+//
+// FIXME: Here and below: change class to final and final methods to override,
+// since we're marking them all as final.
class SpecialBoolAnalysis
: public DataflowAnalysis {
public:
@@ -322,7 +326,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +472,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +481,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +520,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type, const Value , const Environment ,
@@ -538,11 +546,9 @@
if (HasValue1 == HasValue2)
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
gribozavr2 accepted this revision.
gribozavr2 added inline comments.
Comment at: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp:69
-TEST(SolverTest, UnitConflict) {
- ConstraintContext Ctx;
Why delete this test?
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel updated this revision to Diff 467611.
ymandel added a comment.
fix typos
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -310,6 +311,9 @@
}
// Models an analysis that uses flow conditions.
+//
+// FIXME: Here and below: change class to final and final methods to override,
+// since we're marking them all as final.
class SpecialBoolAnalysis
: public DataflowAnalysis {
public:
@@ -322,7 +326,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +472,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +481,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +520,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type, const Value , const Environment ,
@@ -538,11 +546,9 @@
if (HasValue1 == HasValue2)
MergedVal.setProperty("has_value", *HasValue1);
else
-
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel marked 6 inline comments as done.
ymandel added inline comments.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:527-528
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 || (Prop1 != nullptr && Prop2 != nullptr &&
+ isTop(*Prop1) && isTop(*Prop2));
}
xazax.hun wrote:
> ymandel wrote:
> > xazax.hun wrote:
> > > I feel like this logic is repeated multiple times. I wonder if we should
> > > define an `operator==` for `const BoolValue*`.
> > Agreed. I want to wait until we settle on the representation and then we
> > can consider this operator. But, if we end up with a singleton Top then I
> > think we can hold off.
> We ended up not going with a singleton Top, let's reconsider the overloaded
> operator.
added FIXME.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel updated this revision to Diff 467609.
ymandel added a comment.
Added FIXMEs for noted issues.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -310,6 +311,9 @@
}
// Models an analysis that uses flow conditions.
+//
+// FIXME: Here and below: change class to final and final methods to override,
+// since we're marking them all as final.
class SpecialBoolAnalysis
: public DataflowAnalysis {
public:
@@ -322,7 +326,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +472,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +481,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +520,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type, const Value , const Environment ,
@@ -538,11 +546,9 @@
if (HasValue1 == HasValue2)
MergedVal.setProperty("has_value", *HasValue1);
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
xazax.hun added inline comments.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1192
+ const Environment , const Value ,
+ const Environment ) final {
+// Changes to a sounds approximation, which allows us to test whether we
can
ymandel wrote:
> xazax.hun wrote:
> > Nit: I usually prefer marking whole classes final rather than individual
> > virtual methods, but feel free to leave as is.
> Good point. I was following what's done elsewhere in the file -- I think we
> should update all or nothing. that said, if you mark the class final, then
> what do you do with each method? nothing or `override`?
I prefer override on the methods in that scenario. But I agree that refactoring
changes like this might be better done in a separate NFC commit.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
xazax.hun added inline comments.
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue () {
+return takeOwnership(std::make_unique());
+ }
ymandel wrote:
> xazax.hun wrote:
> > gribozavr2 wrote:
> > > ymandel wrote:
> > > > xazax.hun wrote:
> > > > > gribozavr2 wrote:
> > > > > > Should we be creating a new top every time, or should it be a
> > > > > > singleton like true and false?
> > > > > >
> > > > > > It seems like we explicitly don't care about its identity (or else
> > > > > > it would be isomorphic to AtomicBool).
> > > > > Good point, a singleton Top might actually simplify some parts of the
> > > > > code.
> > > > Good question. That was my initial implementation, but it ran into the
> > > > problem that the solver (in `buildBooleanFormula`) maps each unique (by
> > > > pointer) subexpression into a fresh SAT variable in . If we use a
> > > > singleton Top, we need to modify that algorithm appropriately. I'm open
> > > > to suggestions, though, because of the advantages of a singleton Top.
> > > >
> > > > If we assume that a given `Top` is never actually shared in a boolean
> > > > formula (unlike other subexpressions, which may be shared), then we can
> > > > use a singleton and special case it in `buildBooleanFormula`. I think
> > > > that's a good assumption, but am not sure. Thoughts?
> > > I see. Could you add some direct tests for the SAT solver with formulas
> > > that include Top to check the behavior we care about?
> > >
> > Given the discussion so far, it looks like having a singleton top has its
> > own problems. I'm fine with the current solution for now, let's see if the
> > overall approach works and we will see if this needs any further
> > optimization later. +1 to Dmitry, some unit tests like Top && Top generated
> > multiple times will not yield the same expression could be useful. If
> > someone in the future tries to introduce singleton Top, they will see those
> > tests fail and see why we did not have that in the first place and what
> > problems need to be solved to introduce it.
> I've added a test that direct creation of two Tops results in distinct values
> (by pointer) and inequivalent (per the solver), and some tests relating to
> the solver which will fail if you switch to a singleton Top. I didn't see
> much room for a `Top && Top` test, since that seems redundant with the
> simpler tests. I think the inequivalence tests satisfies Dmitri's concern
> with conjunctions involving Top, but, happy to add more if you disagree.
>
> I should note, though: `Top iff Top` is true when both Tops are identical
> values (pointer equality) but not when they are distinct values. This doesn't
> seem right to me -- I think we should have one answer for `Top iff Top` and I
> think it should be `false`. So, in some sense, even the current scheme
> suffers from the some of the drawbacks of the singleton scheme. I think this
> is ok for now, but it does seem to encourage improvement in further patches.
> I think we should have one answer for Top iff Top and I think it should be
> false.
I'd love to see this as a TODO comment.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:527-528
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 || (Prop1 != nullptr && Prop2 != nullptr &&
+ isTop(*Prop1) && isTop(*Prop2));
}
ymandel wrote:
> xazax.hun wrote:
> > I feel like this logic is repeated multiple times. I wonder if we should
> > define an `operator==` for `const BoolValue*`.
> Agreed. I want to wait until we settle on the representation and then we can
> consider this operator. But, if we end up with a singleton Top then I think
> we can hold off.
We ended up not going with a singleton Top, let's reconsider the overloaded
operator.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel updated this revision to Diff 467589.
ymandel marked an inline comment as done.
ymandel added a comment.
added another test
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -322,7 +323,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +469,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +478,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +517,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type, const Value , const Environment ,
@@ -538,11 +543,9 @@
if (HasValue1 == HasValue2)
MergedVal.setProperty("has_value", *HasValue1);
else
- MergedVal.setProperty("has_value", HasValueTop);
+ MergedVal.setProperty("has_value", MergedEnv.makeTopBoolValue());
return true;
}
-
- BoolValue
};
class WideningTest : public Test {
@@ -561,11 +564,8 @@
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel marked 5 inline comments as done.
ymandel added inline comments.
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue () {
+return takeOwnership(std::make_unique());
+ }
xazax.hun wrote:
> gribozavr2 wrote:
> > ymandel wrote:
> > > xazax.hun wrote:
> > > > gribozavr2 wrote:
> > > > > Should we be creating a new top every time, or should it be a
> > > > > singleton like true and false?
> > > > >
> > > > > It seems like we explicitly don't care about its identity (or else it
> > > > > would be isomorphic to AtomicBool).
> > > > Good point, a singleton Top might actually simplify some parts of the
> > > > code.
> > > Good question. That was my initial implementation, but it ran into the
> > > problem that the solver (in `buildBooleanFormula`) maps each unique (by
> > > pointer) subexpression into a fresh SAT variable in . If we use a
> > > singleton Top, we need to modify that algorithm appropriately. I'm open
> > > to suggestions, though, because of the advantages of a singleton Top.
> > >
> > > If we assume that a given `Top` is never actually shared in a boolean
> > > formula (unlike other subexpressions, which may be shared), then we can
> > > use a singleton and special case it in `buildBooleanFormula`. I think
> > > that's a good assumption, but am not sure. Thoughts?
> > I see. Could you add some direct tests for the SAT solver with formulas
> > that include Top to check the behavior we care about?
> >
> Given the discussion so far, it looks like having a singleton top has its own
> problems. I'm fine with the current solution for now, let's see if the
> overall approach works and we will see if this needs any further optimization
> later. +1 to Dmitry, some unit tests like Top && Top generated multiple times
> will not yield the same expression could be useful. If someone in the future
> tries to introduce singleton Top, they will see those tests fail and see why
> we did not have that in the first place and what problems need to be solved
> to introduce it.
I've added a test that direct creation of two Tops results in distinct values
(by pointer) and inequivalent (per the solver), and some tests relating to the
solver which will fail if you switch to a singleton Top. I didn't see much room
for a `Top && Top` test, since that seems redundant with the simpler tests. I
think the inequivalence tests satisfies Dmitri's concern with conjunctions
involving Top, but, happy to add more if you disagree.
I should note, though: `Top iff Top` is true when both Tops are identical
values (pointer equality) but not when they are distinct values. This doesn't
seem right to me -- I think we should have one answer for `Top iff Top` and I
think it should be `false`. So, in some sense, even the current scheme suffers
from the some of the drawbacks of the singleton scheme. I think this is ok for
now, but it does seem to encourage improvement in further patches.
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:100
+public:
+ explicit TopBoolValue() : BoolValue(Kind::TopBool) {}
+
sgatev wrote:
> `explicit` seems unnecessary.
agreed. looks like a copy-paste error on my part.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1220
+ (void)0;
+ /*[[p2]]*/
+}
sgatev wrote:
> Why do we need to check two code points here and in the test below? It's not
> obvious what the difference between `p1` and `p2` is.
added comments to both tests to explain motivation. The second one is actually
a regression test since my original version had a bug in its handling of
lvalues *not* in rvalue position.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel updated this revision to Diff 467513.
ymandel added a comment.
Add explicit test for creation of multiple tops.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -322,7 +323,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +469,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +478,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +517,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type, const Value , const Environment ,
@@ -538,11 +543,9 @@
if (HasValue1 == HasValue2)
MergedVal.setProperty("has_value", *HasValue1);
else
- MergedVal.setProperty("has_value", HasValueTop);
+ MergedVal.setProperty("has_value", MergedEnv.makeTopBoolValue());
return true;
}
-
- BoolValue
};
class WideningTest : public Test {
@@ -561,11 +564,8 @@
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel updated this revision to Diff 467510.
ymandel marked 6 inline comments as done.
ymandel added a comment.
Address comments.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -322,7 +323,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +469,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +478,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +517,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type, const Value , const Environment ,
@@ -538,11 +543,9 @@
if (HasValue1 == HasValue2)
MergedVal.setProperty("has_value", *HasValue1);
else
- MergedVal.setProperty("has_value", HasValueTop);
+ MergedVal.setProperty("has_value", MergedEnv.makeTopBoolValue());
return true;
}
-
- BoolValue
};
class WideningTest : public Test {
@@ -561,11 +564,8 @@
checkDataflow(
AnalysisInputs(
Code,
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
xazax.hun added inline comments.
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue () {
+return takeOwnership(std::make_unique());
+ }
gribozavr2 wrote:
> ymandel wrote:
> > xazax.hun wrote:
> > > gribozavr2 wrote:
> > > > Should we be creating a new top every time, or should it be a singleton
> > > > like true and false?
> > > >
> > > > It seems like we explicitly don't care about its identity (or else it
> > > > would be isomorphic to AtomicBool).
> > > Good point, a singleton Top might actually simplify some parts of the
> > > code.
> > Good question. That was my initial implementation, but it ran into the
> > problem that the solver (in `buildBooleanFormula`) maps each unique (by
> > pointer) subexpression into a fresh SAT variable in . If we use a singleton
> > Top, we need to modify that algorithm appropriately. I'm open to
> > suggestions, though, because of the advantages of a singleton Top.
> >
> > If we assume that a given `Top` is never actually shared in a boolean
> > formula (unlike other subexpressions, which may be shared), then we can use
> > a singleton and special case it in `buildBooleanFormula`. I think that's a
> > good assumption, but am not sure. Thoughts?
> I see. Could you add some direct tests for the SAT solver with formulas that
> include Top to check the behavior we care about?
>
Given the discussion so far, it looks like having a singleton top has its own
problems. I'm fine with the current solution for now, let's see if the overall
approach works and we will see if this needs any further optimization later. +1
to Dmitry, some unit tests like Top && Top generated multiple times will not
yield the same expression could be useful. If someone in the future tries to
introduce singleton Top, they will see those tests fail and see why we did not
have that in the first place and what problems need to be solved to introduce
it.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
sgatev added inline comments.
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:156
+ TopBoolValue () {
+return takeOwnership(std::make_unique());
Please add a comment.
Comment at: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h:291
+ BoolValue () const {
+return DACtx->createTopBoolValue();
Please add a comment.
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:100
+public:
+ explicit TopBoolValue() : BoolValue(Kind::TopBool) {}
+
`explicit` seems unnecessary.
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:237-238
+ case Value::Kind::TopBool:
+// Nothing more to do. Each `TopBool` instance is mapped to a fresh
+// variable.
+break;
Where? Does that mean that `TopBool` never reaches the solver? I think it'd be
good to clarify.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1220
+ (void)0;
+ /*[[p2]]*/
+}
Why do we need to check two code points here and in the test below? It's not
obvious what the difference between `p1` and `p2` is.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
gribozavr2 accepted this revision.
gribozavr2 added inline comments.
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue () {
+return takeOwnership(std::make_unique());
+ }
ymandel wrote:
> xazax.hun wrote:
> > gribozavr2 wrote:
> > > Should we be creating a new top every time, or should it be a singleton
> > > like true and false?
> > >
> > > It seems like we explicitly don't care about its identity (or else it
> > > would be isomorphic to AtomicBool).
> > Good point, a singleton Top might actually simplify some parts of the code.
> Good question. That was my initial implementation, but it ran into the
> problem that the solver (in `buildBooleanFormula`) maps each unique (by
> pointer) subexpression into a fresh SAT variable in . If we use a singleton
> Top, we need to modify that algorithm appropriately. I'm open to suggestions,
> though, because of the advantages of a singleton Top.
>
> If we assume that a given `Top` is never actually shared in a boolean formula
> (unlike other subexpressions, which may be shared), then we can use a
> singleton and special case it in `buildBooleanFormula`. I think that's a good
> assumption, but am not sure. Thoughts?
I see. Could you add some direct tests for the SAT solver with formulas that
include Top to check the behavior we care about?
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel marked 11 inline comments as done.
ymandel added inline comments.
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:237-238
+ case Value::Kind::Top:
+// Nothing more to do. Each `Top` instance will be mapped to a fresh
+// variable and is thereafter anonymous.
+break;
gribozavr2 wrote:
>
regarding the latter clause -- its freedom *does* affect satisfiability. e.g.`
A || Top` is trivially satisfiable. I'm just going to drop the "and ...".
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:527-528
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 || (Prop1 != nullptr && Prop2 != nullptr &&
+ isTop(*Prop1) && isTop(*Prop2));
}
xazax.hun wrote:
> I feel like this logic is repeated multiple times. I wonder if we should
> define an `operator==` for `const BoolValue*`.
Agreed. I want to wait until we settle on the representation and then we can
consider this operator. But, if we end up with a singleton Top then I think we
can hold off.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1192
+ const Environment , const Value ,
+ const Environment ) final {
+// Changes to a sounds approximation, which allows us to test whether we
can
xazax.hun wrote:
> Nit: I usually prefer marking whole classes final rather than individual
> virtual methods, but feel free to leave as is.
Good point. I was following what's done elsewhere in the file -- I think we
should update all or nothing. that said, if you mark the class final, then what
do you do with each method? nothing or `override`?
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1302-1311
+void target(bool Cond) {
+ bool Foo = makeTop();
+ // Force a new block.
+ if (false) return;
+ (void)0;
+ /*[[p1]]*/
+
gribozavr2 wrote:
> Similarly in tests below.
>
> `if (false)` theoretically could be handled in a special way in future and
> could be folded away during CFG construction.
Sure. I went with a different name since it's playing a very specific role
that's not related to the test in the way that `Cond` is.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1454
+ });
+}
+
gribozavr2 wrote:
> Could you add a variant of this test?
>
> ```
> void target(bool Cond) {
> bool Foo = makeTop();
> // Force a new block.
> if (false) return;
> (void)0;
> /*[[p1]]*/
>
> bool Zab;
> if (Cond) {
> Zab = Foo;
> } else {
> Zab = Foo;
> }
> (void)0;
> if (Zab == Foo) { return; }
> /*[[p2]]*/
> }
> ```
>
> Show the loss of precision by checking that the flow condition for p2 is
> satisfiable.
Added, but there's no loss of precision and so the test demonstrates that. My
initial instinct was that there would be loss, but the guard of `Cond` actually
preserves the precision. The cost is complexity -- Zab is a fresh atomic and
the flow condition encoded enough information to recover its equivalence to
`Foo`. But, it is not _equal_ to `Foo`, which would be nice.
The case where we lose precision is a loop, where the incoming edge doesn't
carry a condition.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel updated this revision to Diff 466124.
ymandel marked an inline comment as done.
ymandel added a comment.
Address (most) comments.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -322,7 +323,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -468,9 +469,8 @@
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +478,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +517,11 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 ||
+ (Prop1 != nullptr && Prop2 != nullptr && isa(Prop1) &&
+isa(Prop2));
}
bool merge(QualType Type, const Value , const Environment ,
@@ -538,11 +543,9 @@
if (HasValue1 == HasValue2)
MergedVal.setProperty("has_value", *HasValue1);
else
- MergedVal.setProperty("has_value", HasValueTop);
+ MergedVal.setProperty("has_value", MergedEnv.makeTopBoolValue());
return true;
}
-
- BoolValue
};
class WideningTest : public Test {
@@ -561,11 +564,8 @@
checkDataflow(
AnalysisInputs(
Code, ast_matchers::hasName("target"),
-[this](ASTContext , Environment ) {
-
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel added a comment.
Thanks for the thorough reviews! Agreed on all points, and will address.
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue () {
+return takeOwnership(std::make_unique());
+ }
xazax.hun wrote:
> gribozavr2 wrote:
> > Should we be creating a new top every time, or should it be a singleton
> > like true and false?
> >
> > It seems like we explicitly don't care about its identity (or else it would
> > be isomorphic to AtomicBool).
> Good point, a singleton Top might actually simplify some parts of the code.
Good question. That was my initial implementation, but it ran into the problem
that the solver (in `buildBooleanFormula`) maps each unique (by pointer)
subexpression into a fresh SAT variable in . If we use a singleton Top, we need
to modify that algorithm appropriately. I'm open to suggestions, though,
because of the advantages of a singleton Top.
If we assume that a given `Top` is never actually shared in a boolean formula
(unlike other subexpressions, which may be shared), then we can use a singleton
and special case it in `buildBooleanFormula`. I think that's a good assumption,
but am not sure. Thoughts?
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:102
+ static bool classof(const Value *Val) { return Val->getKind() == Kind::Top; }
+};
+
gribozavr2 wrote:
> Since TopValue is a BoolValue, can we form say a ConjunctionValue where LHS
> or RHS is Top?
>
> What if we create such a conjunction twice? It seems like such conjunctions
> would incorrectly compare equal, even though each Top will be replaced with a
> unique fresh variable.
>
> Would it make sense to change our factory functions for boolean formulas to
> eagerly open Top?
>
> Then we wouldn't need a recursive walk in unpackValue().
They would only compare equal if we're using a singleton Top. In fact, that's
not quite right because we have no deep equality on formulas. But, the caching
mechanism would generate the same formula, so the point holds. In that case, we
would need to eagerly open the Top, because we would lose any way to
distinguish them. But, with different Top instances, this wouldn't be
necessary. Overall, it seems like "open top as soon as possible without killing
convergence" is probably our best heuristic, so this seems like a win. But, I'm
pretty sure there are places where it will prevent convergence (on its own --
`widen` will still handle it fine I believe).
Avoiding the recursive walk would be nice.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
xazax.hun added inline comments.
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue () {
+return takeOwnership(std::make_unique());
+ }
gribozavr2 wrote:
> Should we be creating a new top every time, or should it be a singleton like
> true and false?
>
> It seems like we explicitly don't care about its identity (or else it would
> be isomorphic to AtomicBool).
Good point, a singleton Top might actually simplify some parts of the code.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
xazax.hun accepted this revision.
xazax.hun added inline comments.
This revision is now accepted and ready to land.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:527-528
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 || (Prop1 != nullptr && Prop2 != nullptr &&
+ isTop(*Prop1) && isTop(*Prop2));
}
I feel like this logic is repeated multiple times. I wonder if we should define
an `operator==` for `const BoolValue*`.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1192
+ const Environment , const Value ,
+ const Environment ) final {
+// Changes to a sounds approximation, which allows us to test whether we
can
Nit: I usually prefer marking whole classes final rather than individual
virtual methods, but feel free to leave as is.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
gribozavr2 added inline comments.
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue () {
+return takeOwnership(std::make_unique());
+ }
Should we be creating a new top every time, or should it be a singleton like
true and false?
It seems like we explicitly don't care about its identity (or else it would be
isomorphic to AtomicBool).
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:97
+/// formulas.
+class TopValue final : public BoolValue {
+public:
Here and throughout the patch: since we might have a top for other kinds of
values, WDYT about renaming this type to TopBoolValue? Similarly createTop ->
createTopBool ?
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:102
+ static bool classof(const Value *Val) { return Val->getKind() == Kind::Top; }
+};
+
Since TopValue is a BoolValue, can we form say a ConjunctionValue where LHS or
RHS is Top?
What if we create such a conjunction twice? It seems like such conjunctions
would incorrectly compare equal, even though each Top will be replaced with a
unique fresh variable.
Would it make sense to change our factory functions for boolean formulas to
eagerly open Top?
Then we wouldn't need a recursive walk in unpackValue().
Comment at: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp:378
+if (Val == It->second || (Val->getKind() == Value::Kind::Top &&
+ It->second->getKind() == Value::Kind::Top)) {
JoinedEnv.LocToVal.insert({Loc, Val});
isa
Comment at: clang/lib/Analysis/FlowSensitive/Transfer.cpp:76
+ case Value::Kind::AtomicBool:
+return V;
+
llvm_unreachable(); because this can't happen, V is a BoolValue.
Comment at: clang/lib/Analysis/FlowSensitive/Transfer.cpp:123-124
+ return
+}
+
+
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:237-238
+ case Value::Kind::Top:
+// Nothing more to do. Each `Top` instance will be mapped to a fresh
+// variable and is thereafter anonymous.
+break;
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:469
+static bool isTop(Value ) { return V.getKind() == Value::Kind::Top; }
+static bool isAtomic(Value ) {
`isa(...)`? and `isa(...)` below?
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:621
+EXPECT_EQ(GetFooValue(Env3)->getProperty("has_value")->getKind(),
+ Value::Kind::Top);
});
`EXPECT_TRUE(isa(...))` ?
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1193
+ const Environment ) final {
+// Changes to a sounds approximation, which allows us to test whether we
can
+// (soundly) converge for some loops.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1220-1221
+
+// void target(bool Foo) {
+void target() {
+ bool Foo = makeTop();
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1292
+ASSERT_THAT(FooVal2, NotNull());
+EXPECT_TRUE(isTop(*FooVal2));
+
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1302-1311
+void target(bool Cond) {
+ bool Foo = makeTop();
+ // Force a new block.
+ if (false) return;
+ (void)0;
+ /*[[p1]]*/
+
Similarly in tests below.
`if (false)` theoretically could be handled in a special way in future and
could be folded away during CFG construction.
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1436-1440
+const ValueDecl *Zab1Decl = findValueDecl(AO.ASTCtx, "Zab1");
+ASSERT_THAT(Zab1Decl, NotNull());
+
+const ValueDecl *Zab2Decl = findValueDecl(AO.ASTCtx, "Zab2");
+ASSERT_THAT(Zab2Decl, NotNull());
Zab1Decl, Zab2Decl are unused apart from the NotNull check (which does not seem
interesting to me).
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1454
+ });
+}
+
Could you add a variant of this test?
```
void target(bool Cond) {
bool Foo = makeTop();
// Force a new block.
if (false) return;
(void)0;
/*[[p1]]*/
bool Zab;
if (Cond) {
Zab = Foo;
} else {
Zab = Foo;
}
(void)0;
if (Zab == Foo) { return; }
/*[[p2]]*/
}
```
Show
[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.
ymandel created this revision.
ymandel added reviewers: xazax.hun, sgatev.
Herald added subscribers: martong, rnkovacs.
Herald added a reviewer: NoQ.
Herald added a project: All.
ymandel requested review of this revision.
Herald added a project: clang.
Currently, our boolean formulas (`BoolValue`) don't form a lattice, since they
have no Top element. This patch adds such an element, thereby "completing" the
built-in model of bools to be a proper semi-lattice. It still has infinite
height, which is its own problem, but that can be solved separately, through
widening and the like.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D135397
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
if (auto *C = dyn_cast(S)) {
if (auto *F = dyn_cast(C->getCalleeDecl())) {
E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -322,7 +323,7 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const auto *S = CS->getStmt();
auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
@@ -465,12 +466,16 @@
});
}
+static bool isTop(Value ) { return V.getKind() == Value::Kind::Top; }
+static bool isAtomic(Value ) {
+ return V.getKind() == Value::Kind::AtomicBool;
+}
+
class OptionalIntAnalysis
: public DataflowAnalysis {
public:
- explicit OptionalIntAnalysis(ASTContext , BoolValue )
- : DataflowAnalysis(Context),
-HasValueTop(HasValueTop) {}
+ explicit OptionalIntAnalysis(ASTContext )
+ : DataflowAnalysis(Context) {}
static NoopLattice initialElement() { return {}; }
@@ -478,22 +483,23 @@
auto CS = Elt->getAs();
if (!CS)
return;
-auto S = CS->getStmt();
+const Stmt *S = CS->getStmt();
auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
+SmallVector Matches = match(
+stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+ cxxOperatorCallExpr(
+ callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl
+ .bind("operator"))),
+*S, getASTContext());
if (const auto *E = selectFirst(
-"call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
- getASTContext( {
+"construct", Matches)) {
auto = *Env.createValue(E->getType());
ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-} else if (const auto *E = selectFirst(
- "call",
- match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
- OptionalIntRecordDecl
- .bind("call"),
- *S, getASTContext( {
+} else if (const auto *E =
+ selectFirst("operator", Matches)) {
assert(E->getNumArgs() > 0);
auto *Object = E->getArg(0);
assert(Object != nullptr);
@@ -516,7 +522,10 @@
Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
return false;
-return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+auto *Prop1 = Val1.getProperty("has_value");
+auto *Prop2 = Val2.getProperty("has_value");
+return Prop1 == Prop2 || (Prop1 != nullptr && Prop2 != nullptr &&
+ isTop(*Prop1) && isTop(*Prop2));
}
bool merge(QualType Type,
