如何解决如何检查 Spark_Ada 中的 Storage_Error
根据 Spark2014 文档,Spark 代码中不允许处理异常。
通过验证,可以排除大多数运行时错误发生在编写的程序中,但不能排除 Storage_Error
之类的异常。
由于 Storage_Error
可能发生在每个过程/函数调用或使用 new
动态分配内存时(如果我错了,请纠正我),因此在代码段中捕获和处理此异常使用 Spark_Mode=off 只会在程序的最高级别(程序的入口点)有效。我真的不喜欢这种方法,因为您几乎失去了对此类异常做出反应的所有可能性。
我想做什么:
假设用过程 Add()
创建一个无界树。在这个过程中,我想检查堆上是否有足够的空间在树内创建一个新节点。
如果有,为节点分配内存并将其添加到树中,否则可以给出一个 out 参数,其中设置了某种标志。
我已经搜索了 Spark UserGuide,但找不到如何处理这种情况的方法,只是程序员必须确保有足够的可用内存,而不是如何做到这一点。
如何在 Spark 中处理这些异常?
解决方法
SPARK 确实无法证明(保证)不存在存储错误,因为这些错误是从程序范围之外引发的。对于失败的堆分配以及堆栈空间耗尽时都是如此。
然而,如下面的示例所示,人们可能会通过在 SPARK 分析中避免分配例程来作弊。分配子程序 New_Integer
具有 SPARK 可用于分析指针的后置条件,但不分析子程序的主体。这允许处理 Storage_Error
。当然,现在必须注意主体确实符合规范:当 Ptr
为真时,null
字段不得为 Valid
。 SPARK 现在只假设这是真的,但不会验证这一点。
注意:使用 GNAT CE 2021 可以证明所有指针取消引用和不存在内存泄漏。但是,在 { 期间实际将 Valid
鉴别器设置为 False
会很好{1}} 并使用像 Free
这样的后置条件。不幸的是,这让 SPARK 抱怨可能的判别检查失败。
更新(2021 年 6 月 3 日)
我根据@YannickMoy 的提示更新了示例(见下文)。 Post => P.Valid = False
现在确保弱指针的 Free
鉴别器在返回时设置为 Valid
。
main.adb
False
test.ads
with Test;
procedure Main with SPARK_Mode is
X : Test.Weak_Int_Ptr := Test.New_Integer (42);
Y : Integer;
begin
-- Dereference.
if X.Valid then
Y := X.Ptr.all;
end if;
-- Free.
Test.Free (X);
end Main;
test.adb
package Test with SPARK_Mode is
type Int_Ptr is access Integer;
-- A weak pointer that may or may not be valid,depending on
-- on whether the allocation succeeded.
type Weak_Int_Ptr (Valid : Boolean := False) is record
case Valid is
when False => null;
when True => Ptr : Int_Ptr;
end case;
end record;
function New_Integer (N : Integer) return Weak_Int_Ptr
with Post => (if New_Integer'Result.Valid then New_Integer'Result.Ptr /= null);
-- Allocates a new integer.
procedure Free (P : in out Weak_Int_Ptr)
with
Pre => not P'Constrained,Post => P.Valid = False;
-- Deallocates an integer if needed.
end Test;
输出(gnatprove)
with Ada.Unchecked_Deallocation;
package body Test with SPARK_Mode is
-----------------
-- New_Integer --
-----------------
function New_Integer (N : Integer) return Weak_Int_Ptr is
pragma SPARK_Mode (Off); -- Refrain body from analysis.
begin
return Weak_Int_Ptr'(Valid => True,Ptr => new Integer'(N));
exception
when Storage_Error =>
return Weak_Int_Ptr'(Valid => False);
end New_Integer;
----------
-- Free --
----------
procedure Free (P : in out Weak_Int_Ptr) is
procedure Local_Free is new Ada.Unchecked_Deallocation
(Object => Integer,Name => Int_Ptr);
begin
if P.Valid then
Local_Free (P.Ptr);
P := Weak_Int_Ptr'(Valid => False);
end if;
end Free;
end Test;
摘要(由 OP 添加)
提供的代码有助于防止 $ gnatprove -Pdefault.gpr -j0 --level=0 --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:5:04: info: absence of memory leak at end of scope proved
main.adb:13:13: info: discriminant check proved
main.adb:13:18: info: pointer dereference check proved
main.adb:17:08: info: precondition proved
test.adb:31:23: info: discriminant check proved
test.adb:32:12: info: discriminant check proved
test.adb:32:12: info: absence of memory leak proved
test.ads:22:16: info: postcondition proved
Summary logged in [...]/gnatprove.out
使用 Storage_Error
关键字进行动态分配。由于 SPARK 已经可以证明无限递归(如评论中所述。参见 here),唯一可能导致 new
的未解决问题是程序在正常执行期间需要更多堆栈比什么可用。然而,这可以通过 GNATstack 等工具在编译时监控和确定(也在评论中提到。参见 here)。
我认为您可以创建自己的存储池 (ARM 13.11 ff) 来支持“new
可以吗?”的附加操作。使其免受并发的影响会更加复杂。
我想你可以让它的 Allocate
吞下异常并返回 null
。无论如何,我认为您必须“在 SPARK 之外”编写这样的程序!
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。