import csharp

/** "Naive" def-use implementation. */
predicate defReaches(AssignableDefinition def, LocalScopeVariable v, ControlFlow::Node cfn) {
  def.getTarget() = v and cfn = def.getAControlFlowNode().getASuccessor()
  or
  exists(ControlFlow::Node mid | defReaches(def, v, mid) |
    not mid =
      any(AssignableDefinition ad | ad.getTarget() = v and ad.isCertain()).getAControlFlowNode() and
    cfn = mid.getASuccessor()
  )
}

predicate defUsePair(AssignableDefinition def, AssignableRead read) {
  exists(Assignable a |
    defReaches(def, a, read.getAControlFlowNode()) and
    read.getTarget() = a
  )
}

private LocalScopeVariableRead getAReachableUncertainRead(AssignableDefinition def) {
  exists(Ssa::Definition ssaDef |
    def = ssaDef.getAnUltimateDefinition().(Ssa::ExplicitDefinition).getADefinition()
  |
    result = ssaDef.getARead()
  )
}

from AssignableDefinition def, LocalScopeVariableRead read, string s
where
  read = getAReachableUncertainRead(def) and
  not defUsePair(def, read) and
  s = "not a def/use pair"
  or
  defUsePair(def, read) and
  not read = getAReachableUncertainRead(def) and
  s = "missing def/use pair"
select def, read, s