[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Dmitri Gribenko via Phabricator via cfe-commits]

This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rG3b29b8a2aba2: Expose DataflowAnalysisContext.querySolver(). 
(authored by bazuzi, committed by gribozavr).

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -175,6 +175,14 @@
 
   Arena () { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::SetVector Constraints);
+
 private:
   friend class Environment;
 
@@ -204,13 +212,6 @@
   AtomicBoolValue , llvm::SetVector ,
   llvm::DenseSet );
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::SetVector Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::SetVector Constraints) {


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -175,6 +175,14 @@
 
   Arena () { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::SetVector Constraints);
+
 private:
   friend class Environment;
 
@@ -204,13 +212,6 @@
   AtomicBoolValue , llvm::SetVector ,
   llvm::DenseSet );
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::SetVector Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::SetVector Constraints) {
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Samira Bazuzi via Phabricator via cfe-commits]

bazuzi added a comment.

Since the timeline for being able to use this is dependent not only on commits 
but integrates as well, lets go ahead with this then.

Can someone commit it for me when we're ready?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Sam McCall via Phabricator via cfe-commits]

sammccall added a comment.

In D153805#4464487 , @bazuzi wrote:

> It looks like D153485  changes the context 
> for the last few comments significantly. What's the appetite for adding yet 
> another child commit to the chain D153485  
> is in that exposes the solver directly? Instead of committing this and having 
> D153485  make a breaking change to expose 
> the solver directly if that's better in the new context.

Yeah, that's fewer steps but more stuff stacked on top.
I don't feel strongly - happy to make that change later if you'd like to have 
this available now.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Samira Bazuzi via Phabricator via cfe-commits]

bazuzi added a comment.

It looks like D153485  changes the context 
for the last few comments significantly. What's the appetite for adding yet 
another child commit to the chain D153485  is 
in that exposes the solver directly? Instead of committing this and having 
D153485  make a breaking change to expose the 
solver directly if that's better in the new context.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Sam McCall via Phabricator via cfe-commits]

sammccall added a comment.

LG as is, sorry for the noise!




Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+

gribozavr2 wrote:
> sammccall wrote:
> > bazuzi wrote:
> > > bazuzi wrote:
> > > > sammccall wrote:
> > > > > sammccall wrote:
> > > > > > FWIW, I'd probably prefer exposing the solver object itself, having 
> > > > > > all capabilities exposed directly through DataflowAnalysisContext 
> > > > > > gives it this ugly "god object" quality and the places that we want 
> > > > > > to use it really just need arena + solver.
> > > > > this should be ArrayRef now... sorry for the churn
> > > > HEAD says SetVector, so updated to that. Is there another change coming 
> > > > that makes it ArrayRef?
> > > If all capabilities was more than 1 capability and this function didn't 
> > > already exist, I'd me more inclined to agree. But requiring users to 
> > > duplicate the body of this function seems worse to me than forwarding an 
> > > API from a member.
> > > 
> > > I'm noticing as well that the body of this function adds true and !false 
> > > constraints to the provided set, which I hadn't been doing when using a 
> > > solver and for which I can find no documentation indicating that it's 
> > > necessary. Either we should document why that's done and would need to 
> > > expect users to know to do it if we expose the solver only directly, or 
> > > we should remove that from this function.
> > I do think ArrayRef is the right signature here - SetVector is a slightly 
> > messy impl detail.
> > 
> > This would mean an unfortunate copy for now but that will go away, see 
> > D153485 (which is waiting on the Formula patch to land)
> @sammccall 
> While I'd normally agree, querySolver() incorporates the true and false 
> literals into the formula, so it is actually a lot more useful than the raw 
> solver object. Until we have a different representation of boolean literals, 
> I think this patch is the better in terms of API design.
The public APIs for "set of constraints" are ArrayRef (on Solver::solve).
SetVector was how we maintained determinism while deduplicating inside DACtx, 
this function is SetVector specifically because it was private.

Nevertheless, let's go with this change as-is, the alternatives are complicated 
for now.
I'll try to simplify the API a bit once the prereqs are in place.



Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+

sammccall wrote:
> gribozavr2 wrote:
> > sammccall wrote:
> > > bazuzi wrote:
> > > > bazuzi wrote:
> > > > > sammccall wrote:
> > > > > > sammccall wrote:
> > > > > > > FWIW, I'd probably prefer exposing the solver object itself, 
> > > > > > > having all capabilities exposed directly through 
> > > > > > > DataflowAnalysisContext gives it this ugly "god object" quality 
> > > > > > > and the places that we want to use it really just need arena + 
> > > > > > > solver.
> > > > > > this should be ArrayRef now... sorry for the churn
> > > > > HEAD says SetVector, so updated to that. Is there another change 
> > > > > coming that makes it ArrayRef?
> > > > If all capabilities was more than 1 capability and this function didn't 
> > > > already exist, I'd me more inclined to agree. But requiring users to 
> > > > duplicate the body of this function seems worse to me than forwarding 
> > > > an API from a member.
> > > > 
> > > > I'm noticing as well that the body of this function adds true and 
> > > > !false constraints to the provided set, which I hadn't been doing when 
> > > > using a solver and for which I can find no documentation indicating 
> > > > that it's necessary. Either we should document why that's done and 
> > > > would need to expect users to know to do it if we expose the solver 
> > > > only directly, or we should remove that from this function.
> > > I do think ArrayRef is the right signature here - SetVector is a slightly 
> > > messy impl detail.
> > > 
> > > This would mean an unfortunate copy for now but that will go away, see 
> > > D153485 (which is waiting on the Formula patch to land)
> > @sammccall 
> > While I'd normally agree, querySolver() incorporates the true and false 
> > literals into the formula, so it is actually a lot more useful than the raw 
> > solver object. Until we have a different representation of boolean 
> > literals, I think this patch is the better in terms of API design.
> The public APIs for "set of constraints" are ArrayRef (on Solver::solve).
> SetVector was how we maintained determinism while deduplicating inside DACtx, 
> this function is SetVector specifically because it was private.
> 
> Nevertheless, let's go with this change as-is, the alternatives are 
> complicated 

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Dmitri Gribenko via Phabricator via cfe-commits]

gribozavr2 accepted this revision.
gribozavr2 added inline comments.



Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+

sammccall wrote:
> bazuzi wrote:
> > bazuzi wrote:
> > > sammccall wrote:
> > > > sammccall wrote:
> > > > > FWIW, I'd probably prefer exposing the solver object itself, having 
> > > > > all capabilities exposed directly through DataflowAnalysisContext 
> > > > > gives it this ugly "god object" quality and the places that we want 
> > > > > to use it really just need arena + solver.
> > > > this should be ArrayRef now... sorry for the churn
> > > HEAD says SetVector, so updated to that. Is there another change coming 
> > > that makes it ArrayRef?
> > If all capabilities was more than 1 capability and this function didn't 
> > already exist, I'd me more inclined to agree. But requiring users to 
> > duplicate the body of this function seems worse to me than forwarding an 
> > API from a member.
> > 
> > I'm noticing as well that the body of this function adds true and !false 
> > constraints to the provided set, which I hadn't been doing when using a 
> > solver and for which I can find no documentation indicating that it's 
> > necessary. Either we should document why that's done and would need to 
> > expect users to know to do it if we expose the solver only directly, or we 
> > should remove that from this function.
> I do think ArrayRef is the right signature here - SetVector is a slightly 
> messy impl detail.
> 
> This would mean an unfortunate copy for now but that will go away, see 
> D153485 (which is waiting on the Formula patch to land)
@sammccall 
While I'd normally agree, querySolver() incorporates the true and false 
literals into the formula, so it is actually a lot more useful than the raw 
solver object. Until we have a different representation of boolean literals, I 
think this patch is the better in terms of API design.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Samira Bazuzi via Phabricator via cfe-commits]

bazuzi added inline comments.



Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+

sammccall wrote:
> sammccall wrote:
> > FWIW, I'd probably prefer exposing the solver object itself, having all 
> > capabilities exposed directly through DataflowAnalysisContext gives it this 
> > ugly "god object" quality and the places that we want to use it really just 
> > need arena + solver.
> this should be ArrayRef now... sorry for the churn
HEAD says SetVector, so updated to that. Is there another change coming that 
makes it ArrayRef?



Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+

bazuzi wrote:
> sammccall wrote:
> > sammccall wrote:
> > > FWIW, I'd probably prefer exposing the solver object itself, having all 
> > > capabilities exposed directly through DataflowAnalysisContext gives it 
> > > this ugly "god object" quality and the places that we want to use it 
> > > really just need arena + solver.
> > this should be ArrayRef now... sorry for the churn
> HEAD says SetVector, so updated to that. Is there another change coming that 
> makes it ArrayRef?
If all capabilities was more than 1 capability and this function didn't already 
exist, I'd me more inclined to agree. But requiring users to duplicate the body 
of this function seems worse to me than forwarding an API from a member.

I'm noticing as well that the body of this function adds true and !false 
constraints to the provided set, which I hadn't been doing when using a solver 
and for which I can find no documentation indicating that it's necessary. 
Either we should document why that's done and would need to expect users to 
know to do it if we expose the solver only directly, or we should remove that 
from this function.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Sam McCall via Phabricator via cfe-commits]

sammccall added inline comments.



Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+

sammccall wrote:
> sammccall wrote:
> > FWIW, I'd probably prefer exposing the solver object itself, having all 
> > capabilities exposed directly through DataflowAnalysisContext gives it this 
> > ugly "god object" quality and the places that we want to use it really just 
> > need arena + solver.
> this should be ArrayRef now... sorry for the churn
I do think ArrayRef is the right signature here - SetVector is a slightly messy 
impl detail.

This would mean an unfortunate copy for now but that will go away, see D153485 
(which is waiting on the Formula patch to land)


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Samira Bazuzi via Phabricator via cfe-commits]

bazuzi updated this revision to Diff 536293.
bazuzi added a comment.

Rebase on main to pull in change from DenseSet to SetVector.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -175,6 +175,14 @@
 
   Arena () { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::SetVector Constraints);
+
 private:
   friend class Environment;
 
@@ -204,13 +212,6 @@
   AtomicBoolValue , llvm::SetVector ,
   llvm::DenseSet );
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::SetVector Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::SetVector Constraints) {


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -175,6 +175,14 @@
 
   Arena () { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::SetVector Constraints);
+
 private:
   friend class Environment;
 
@@ -204,13 +212,6 @@
   AtomicBoolValue , llvm::SetVector ,
   llvm::DenseSet );
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::SetVector Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::SetVector Constraints) {
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Sam McCall via Phabricator via cfe-commits]

sammccall accepted this revision.
sammccall added a comment.

Thanks!

As discussed offline, I had some concerns about whether there were any cases 
where it was safe to use formulas separate from the FC that might constrain 
them.
But we found some: these are formulas produced by the downstream analysis that 
have known structure.




Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+

FWIW, I'd probably prefer exposing the solver object itself, having all 
capabilities exposed directly through DataflowAnalysisContext gives it this 
ugly "god object" quality and the places that we want to use it really just 
need arena + solver.



Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+

sammccall wrote:
> FWIW, I'd probably prefer exposing the solver object itself, having all 
> capabilities exposed directly through DataflowAnalysisContext gives it this 
> ugly "god object" quality and the places that we want to use it really just 
> need arena + solver.
this should be ArrayRef now... sorry for the churn


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Samira Bazuzi via Phabricator via cfe-commits]

bazuzi updated this revision to Diff 536269.
bazuzi added a comment.

Updated function comment to remove unnecessary repetition and include 
newly-discovered caveat re: flow conditions.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -174,6 +174,14 @@
 
   Arena () { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+
 private:
   friend class Environment;
 
@@ -203,13 +211,6 @@
   AtomicBoolValue , llvm::DenseSet ,
   llvm::DenseSet );
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::DenseSet Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::DenseSet Constraints) {


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -174,6 +174,14 @@
 
   Arena () { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+
 private:
   friend class Environment;
 
@@ -203,13 +211,6 @@
   AtomicBoolValue , llvm::DenseSet ,
   llvm::DenseSet );
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::DenseSet Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::DenseSet Constraints) {
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel accepted this revision.
ymandel added inline comments.
This revision is now accepted and ready to land.



Comment at: 
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:178-181
+  /// Possible outcomes are:
+  /// - `Satisfiable`: A satisfying assignment exists and is returned.
+  /// - `Unsatisfiable`: A satisfying assignment does not exist.
+  /// - `TimedOut`: The search for a satisfying assignment was not completed.

nit: Given that these are options of `Solver::Result`, I think you can just 
delete these lines.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153805

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Samira Bazuzi via Phabricator via cfe-commits]

bazuzi created this revision.
bazuzi added reviewers: ymandel, gribozavr2, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
bazuzi requested review of this revision.
Herald added a project: clang.

This allows for use of the same solver used by the DAC for additional solving 
post-analysis and thus shared use of MaxIterations in WatchedLiteralsSolver.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D153805

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -174,6 +174,13 @@
 
   Arena () { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  /// Possible outcomes are:
+  /// - `Satisfiable`: A satisfying assignment exists and is returned.
+  /// - `Unsatisfiable`: A satisfying assignment does not exist.
+  /// - `TimedOut`: The search for a satisfying assignment was not completed.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+
 private:
   friend class Environment;
 
@@ -203,13 +210,6 @@
   AtomicBoolValue , llvm::DenseSet ,
   llvm::DenseSet );
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::DenseSet Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::DenseSet Constraints) {


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -174,6 +174,13 @@
 
   Arena () { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  /// Possible outcomes are:
+  /// - `Satisfiable`: A satisfying assignment exists and is returned.
+  /// - `Unsatisfiable`: A satisfying assignment does not exist.
+  /// - `TimedOut`: The search for a satisfying assignment was not completed.
+  Solver::Result querySolver(llvm::DenseSet Constraints);
+
 private:
   friend class Environment;
 
@@ -203,13 +210,6 @@
   AtomicBoolValue , llvm::DenseSet ,
   llvm::DenseSet );
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::DenseSet Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::DenseSet Constraints) {
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits