polyir:可以通过Coq开发的多面体编译技术建模的循环类型的语义

聚IR 这是SCoP语义的参考实现。 此实现对所使用的多面体库的具体实现进行了抽象。 实现必须坚持由布局规范POLYHEDRA 。 在此，每个操作都允许失败（所有操作都返回option ）。 但是，如果操作成功，我们希望结果是正确的。 我们为库选择了一个这样的模型，以说明诸如VPL之类的库，该库使用经定理证明的oracle来验证正确性证书。 这样的库的API总是会返回一个可选值（对于VPL，它是一个imp值），该值可能正确也可能不正确。 通过以“允许失败”的方式构造我们期望的API，我们可以与使用oracles的库进行接口。 另一方面，如果某人确实为多面体操作实现了经过完全验证的库，那么要插入我们的API，他们只需将其结果包装成Some(...)并一天调用即可，因为他们的所有结果都会被正确的。 该项目的目标如下： 提供Polly，PLUTO等使用的SCoPs形式语义的参考概念。据