编译细节和可达性算法

问题描述

| 我是否应该分析图的各个部分的可及性（称为规则）：如果验证了某个布尔条件，则可以到达一个节点。每个节点仅知道其前任节点，节点的类型不同，并且并非所有节点都有待验证的条件。规则放置在文件中。 我进行了规则解析，我选择了（通过使用区分联合）并根据执行流程对节点进行排序。现在，我应该进行一种静态分析，以告知用户在特定条件下某些节点不可访问。该图有多个入口点，但只有一个出口点。 教授告诉我在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 \”块用于选择所有且仅满足给定条件的行。我应该静态地检查这些条件是相互矛盾的。     

解决方法

        没有简单的方法可以解决问题。如果您能够编写始终有效的静态分析工具，那么您还将解决停止问题，这是（证明）不可能的。 我认为F＃编译器目前不进行任何复杂的可达性分析。如果您想仅针对布尔条件和整数（例如您的示例）实施此检查，则可以解析F＃表达式，将其转换为某些逻辑公式，然后使用SMT求解器检查条件是否存在任何值将举行。 要解析源代码，可以使用开源F＃版本，也可以使用F＃引号（如果您只想在显式标记的表达式上运行工具）。使用后者更容易启动。 有关SMT求解器的更多信息，您可以从Microsoft Research签出Z3项目。您也可以自己实现这种工具的简单版本-对于布尔条件（无数字），您可以看一下SAT求解算法。