2

根据 Spark2014 文档，不允许在 Spark 代码中处理异常。

通过验证，可以排除大多数运行时错误发生在编写的程序内部，但Storage_Error不能排除诸如此类的异常。

由于Storage_Error可能发生在每个过程/函数调用或使用动态分配内存时new（如果我错了，请纠正我），因此在 Spark_Mode=off 的代码段中捕获和处理此异常仅在最高级别有效程序（程序的入口点）。我真的不喜欢这种方法，因为您几乎失去了对这种异常做出反应的所有可能性。

我想做的事：

假设用一个过程创建一个无界树Add()。在这个过程中，我想检查堆上是否有足够的空间，以便在树内创建一个新节点。如果有，为节点分配内存并将其添加到树中，否则可以给出一个 out 参数，其中设置了某种标志。

我已经通过 Spark UserGuide 进行了搜索，但无法找到一种应该如何处理的方法，只是程序员必须确保有足够的可用内存，而不是如何做到这一点。

如何在 Spark 中处理这些异常？

4

2 回答 2

4

SPARK 确实不能证明（保证）不存在存储错误，因为这些错误是从程序范围之外引发的。对于失败的堆分配以及堆栈空间耗尽时都是如此。

但是，可以通过避免 SPARK 分析中的分配例程来作弊，如下面的示例所示。分配子程序New_Integer具有 SPARK 可以用来分析指针的后置条件，但子程序的主体被禁止分析。这允许Storage_Error处理 a 。当然，现在必须注意主体确实符合规范：该Ptr字段不能是nullwhenValid为真。SPARK 现在只假设这是真的，但不会验证这一点。

注意：可以使用 GNAT CE 2021 证明所有指针取消引用和不存在内存泄漏。但是，将Valid鉴别器实际设置为FalseduringFree并使用类似Post => P.Valid = False. 不幸的是，这使得 SPARK 抱怨可能的判别检查失败。

更新（2021 年 6 月 3 日）

我根据@YannickMoy 的提示更新了示例（见下文）。Free现在确保弱指针的Valid鉴别器设置为False返回。

主文件

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;

测试广告

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;

测试.adb

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;

输出（gnatprove）

$ 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

摘要（由OP添加）

提供的代码有助于防止Storage_Error使用new关键字进行动态分配。由于 SPARK 已经可以证明无限递归（如评论中所述。请参见此处），唯一可能导致 , 的未解决问题是Storage_Error在正常执行期间需要比可用堆栈更多的程序。然而，这可以通过 GNATstack 等工具在编译时进行监控和确定（在评论中也提到。请参见此处）。

于 2021-06-02T17:35:35.857 回答
1

我认为您可以创建自己的存储池（ARM 13.11 ff）来支持“可以吗？”的附加操作new。使其免受并发的影响会更加复杂。

我想你可以让它Allocate吞下异常并返回null。无论如何，我认为你必须在“SPARK 之外”编写这样的东西！

于 2021-06-02T17:22:19.627 回答