编译细节和可达性算法 [英] Compilation details and reachability algorithms

问题描述

我应该分析图的各个部分的可及性(称为规则):如果验证了某个布尔条件，就可以达到一个节点.每个节点仅知道其前任节点，节点的类型不同，并且并非所有节点都有待验证的条件.规则放置在文件中.

Should I make an analysis of reachability of parts of a graph (called rule): a node can be reached if a certain boolean condition is verified. Each node knows only its predecessor, there are different types of nodes and not all nodes have at guard a condition to be verified. The rule is placed in a file.

我对规则进行了解析，我已经选择了(通过使用区分联合)并根据执行流程对节点进行了排序.现在，我应该进行一种静态分析，以告知用户在指定条件下某些节点不可访问.该图有多个入口点，但只有一个出口点.

I made ​the parsing of the rule, I have selected (through the use of discriminated union) and ordered the nodes in accordance with the flow of execution. Now, I should make a kind of static analysis to inform the user that, for specified conditions, some nodes are unreachable. There are multiple entry points to the graph, but only one exit point.

教授告诉我在F#中转换布尔条件，并通过编译对其进行检查.但是我注意到，即使我编写了以下代码，F#编译器也没有向我发出警告:

The professor told me to translate the Boolean conditions in F# and check it through compilation. But I noticed that the F# compiler does not give me a warning even though I have written the following code:

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#中实现起来没有太多复杂的解决方案?还是在编译器中有一个选项可以让我获取有关无法访问的代码的信息?

Is there a better solution and not too much complex to implement in F# to solve this problem? Or is there an option in the compiler that allows me to get information about unreachable code?

这是图表的示例，我必须检查各个分支的可达性. "IN"块用于从数据库中加载列，而"Select"块用于选择所有且仅满足给定条件的行.我应该静态地检查这些条件是否相互矛盾.

This is an example of the graph that I have to check the reachability of the various branches. "IN" blocks are used to load the columns from a database, while "Select" blocks are used to select all and only the rows that meet a given condition. I should check statically that these conditions are mutually contradictory.

推荐答案

没有简单的方法可以解决此问题.如果您能够编写始终有效的静态分析工具，则还可以解决停止问题 (这是不可能的).

There is no easy way to solve the problem. If you were able to write a static analysis tool that always worked, you would also solve the Halting problem and that's (provably) impossible.

我认为F#编译器目前不进行任何复杂的可达性分析.如果要仅针对布尔条件和整数(如您的示例)实施此检查，则可以解析F#表达式，将其转换为某些逻辑公式，然后使用

I don't think the F# compiler does any complex reachability analysis at the moment. If you want to implement this check just for Boolean conditions and Integers (as in your examples), then you could parse the F# expression, translate it to some logical formula and then use SMT solver to check whether there are any values for which the condition will hold.

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

• To parse the source code, you can either use the open-source F# release, or you can use F# quotations (if you just want to run your tool on explicitly marked expressions). Using the later is easier for starting.

有关SMT求解器的更多信息，可以查看

For more information about SMT solvers, you can check out the Z3 project from Microsoft Research. You could also implement a simple version of such tool yourself - for just Boolean conditions (no numbers) you can take a look at SAT solving algorithms.

这篇关于编译细节和可达性算法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！