如何检查 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。

ma​​in.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 之外”编写这样的程序！