编译细节和可达性算法

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

没有简单的方法可以解决这个问题。如果您能够编写一个始终有效的静态分析工具，您还可以解决停止问题 （事实证明）这是不可能的。

我认为 F# 编译器目前不会进行任何复杂的可达性分析。如果您只想针对布尔条件和整数（如示例中所示）实现此检查，那么您可以解析 F# 表达式，将其转换为某种逻辑公式，然后使用 SMT 求解器 检查是否存在满足条件的任何值。

• 要解析源代码，您可以使用开源 F# 版本，也可以使用F# 引号（如果您只想在显式标记的表达式上运行工具）。使用后者更容易启动。

• 有关 SMT 求解器的更多信息，您可以查看 Z3来自微软研究院的项目。您还可以自己实现此类工具的简单版本 - 对于布尔条件（无数字），您可以查看 SAT 求解算法。