有一些语言支持一个足够强大的类型系统,他们可以在编译时证明代码不会在其边界之外处理数组.我的问题是,如果我们要将这样一种语言编译到JVM中,有没有办法利用这种语言来执行性能,并删除每个数组访问上发生的数组边界检查？
1)我知道最近的JDK支持一些数组绑定检查消除,但是由于我在编译时知道某些调用是安全的,所以我可以更安全地删除.
2)有些人认为这不会影响性能,但最重要的是,特别是在数组/计算等重大应用程序,如科学计算.
关于铸造的同样的问题.我知道某些是某种类型的,但Java不是因为它的有限类型的系统.有没有办法告诉JVM“信任我”,跳过任何支票？
我意识到JVM通常是分布式的,可能没有办法做到这一点,使用这个功能来修改JVM是合理的吗？这是已经完成了吗？
编译一个更有力的类型语言到JVM的沮丧之一,它仍然受到Java限制的阻碍.
解决方法
原则上,如果没有
proof-carrying code(PCC)基础设施,这不能以安全的方式完成. PCC将允许您将安全推理嵌入到类文件中.您的嵌入式证明将在课程加载时检查.如果证明中有缺陷,该课程不加载.
如果JVM允许您删除运行时检查,而不需要正式证明,那么,正如SecurityMatt所言,它将打破Java的原始理念作为一个安全的平台.
JVM使用特殊形式的PCC来对方法中的局部变量进行类型检查.类加载机制使用所有局部变量打字信息来检查其正确性,但在此之后丢弃.但这是JVM中使用的PCC概念的唯一实例.据我所知,JVM没有一般的PCC基础设施.
我曾听说过一个JavaCard平台,它支持一小部分Java.我不知道这是否可以帮助你的问题.
