编译细节和可达性算法

Question

我是否应该对图的各个部分进行可达性分析(称为规则)：如果验证了某个布尔条件，则可以到达一个节点。每个节点只知道它的前身，存在不同类型的节点，并且并不是所有节点都具有要验证的条件。该规则被放在一个文件中。

我让​来解析规则，我选择了(通过使用区分联合)，并根据执行流程对节点进行了排序。现在，我应该进行一种静态分析来通知用户，在指定的条件下，某些节点是无法到达的。图中有多个入口点，但只有一个出口点。

教授告诉我翻译F#中的布尔条件，并通过编译来检查它。但我注意到，即使我编写了以下代码，F#编译器也没有给我一个警告：

let tryCondition cond =
if cond then
    if not cond then "Not reachable"
    else "Reachable"
else "bye"

或

let tryConditionTwo num =
match num with
| x as t when x > 0 -> match t with
                       | y when y < 0 -> "Not reachable"
                       | _ -> "Reachable"
| _ -> "bye"

有没有更好的解决方案，而不是在F#中实现太复杂来解决这个问题？或者，编译器中是否有一个选项可以让我获得有关无法访问的代码的信息？

这是一个图的例子，我必须检查各个分支的可达性。"IN“块用于从数据库加载列，而" select”块用于选择所有行，并且只选择满足给定条件的行。我应该静态地检查这些条件是相互矛盾的。

Answer 1

没有简单的方法来解决这个问题。如果您能够编写一个始终有效的静态分析工具，那么您也可以解决Halting problem问题，而这(可以证明)是不可能的。

我认为F#编译器目前不会做任何复杂的可达性分析。如果您希望仅针对布尔条件和整数实现此检查(如示例中所示)，则可以解析F#表达式，将其转换为某个逻辑公式，然后使用SMT solver检查是否存在该条件适用的任何值。

• 要解析源代码，可以使用open-source F#发行版，也可以使用F# quotations (如果只想在显式标记的表达式上运行工具)。使用后者更容易开始。
• 有关

求解器的更多信息，可以查看微软研究院的Z3 project。您也可以自己实现这种工具的一个简单版本--对于布尔条件(没有数字)，您可以看看SAT solving algorithms.