Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Feature Request] Allow Field Constraints in Member Predicates for Enhanced Flexibility in Class Queries #17990

Open
cradiator opened this issue Nov 14, 2024 · 0 comments
Labels
question Further information is requested

Comments

@cradiator
Copy link

Feature Request

Summary

Allow Field to be constrained within member predicates, not just in characteristic predicates within a class.

Context

In writing a ControlFlowReach class that mimics the dataflow interface, I'd like to define a status field that can be calculated in subclasses according to the source node and then used across member predicates like isSource, isSink, and isBarrier. However, the current limitation requiring Field to be constrained only within characteristic predicates prevents this.

Example Code

Here’s my ControlFlowReach class:

abstract class ControlFlowReach extends string {
  bindingset[this]
  ControlFlowReach() { any() }

  predicate reaches(ControlFlowNode src, ControlFlowNode snk) {
    isSource(src) and isSink(snk) and reach_internal(src, snk)
  }

  abstract predicate isSource(ControlFlowNode node);
  abstract predicate isSink(ControlFlowNode node);
  predicate isBarrier(ControlFlowNode node) { none() }

  private predicate reach_internal(ControlFlowNode current, ControlFlowNode sink) {
    not isBarrier(current) and
    (current = sink or reach_internal(current.getASuccessor(), sink))
  }
}

In the subclass SomeFlow, I define status to calculate a value based on the source node, which I then want to use in isSink and isBarrier.

class SomeFlow extends ControlFlowReach {
  Expr status;

  SomeFlow() {
    this = "SomeFlow"
  }

  predicate isSource(ControlFlowNode node) {
    // condition on node
    and status = <value_based_on_node>
  }

  predicate isSink(ControlFlowNode node) {
    // uses status
  }
}

Issue

Based on the current design, even with isSource(src) and isSink(snk) in reaches(), the status field in isSink and isSource seems to take different values. The documentation notes that fields must be constrained in characteristic predicates and not in member predicates, but it’s unclear why this limitation exists.

Questions

  1. Why must fields be constrained only in characteristic predicates and not in member predicates?
  2. Why does status appear to have different values in isSink and isSource, even though they are called in reaches() under the condition isSource(src) and isSink(snk)?
  3. Could this feature be added in the future, allowing fields to be constrained in member predicates for greater flexibility?

Thank you for considering this request.

@cradiator cradiator added the question Further information is requested label Nov 14, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
question Further information is requested
Projects
None yet
Development

No branches or pull requests

1 participant