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

问题描述

我应该对图的部分（称为规则）的可达性进行分析：如果某个布尔条件得到验证，则可以到达一个节点。每个节点只知道它的前任，有不同类型的节点，并不是所有的节点都有一个需要检验的条件。该规则放置在一个文件中。

我对规则进行了解析，我选择了（通过使用区别联合）并根据执行流程对节点进行了排序。现在，我应该做一种静态分析来通知用户，对于指定的情况，有些节点是不可访问的。图中有多个入口点，但只有一个出口点。

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

  let tryCondition cond = 
如果cond则
如果不是cond那么不可到达
 else可达
其他再见
  

或

  let tryConditionTwo num = 
 match num with 
 |当x>时x为t。 0  - >与
 |匹配t当y  | _  - > 可达
 | _  - > bye
  

是否有更好的解决方案，并且在F＃中解决此问题时不会太复杂？或者在编译器中有一个选项允许我获取有关无法访问的代码的信息？

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

规则图的一个例子

解决方案

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

我认为F＃编译器目前没有做任何复杂的可达性分析。如果你想仅为布尔条件和整数（如你的例子）实现这个检查，那么你可以解析F＃表达式，将它转换成一些逻辑公式，然后使用 SMT求解器来检查条件是否有任何值。

$ b $为解析源代码，您可以使用开源F＃发行版，或者您可以使用F＃语句（如果您只想在明确标记的表达式上运行您的工具）。使用后者更容易启动。


• 有关SMT解算器的更多信息，可以查看 Z3项目。你也可以自己实现一个简单版本的工具 - 只需布尔条件（无数字），你可以看看 SAT求解算法。

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.

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"

or

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

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?

Edit: 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.

An example of rule graph

解决方案

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.

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.

• 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.

• 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.

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