如何在 Spark_Ada 中检查 Storage_Error

Question

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

经过验证，大部分运行时的错误都可以排除在编写的程序内部，但不能排除像Storage_Error这样的异常。

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

我想做的事情：

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

我已经搜索过 Spark 用户指南，但无法找到如何处理这个问题的方法，只是程序员必须确保有足够的可用内存，但不知道如何做到这一点.

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

Answer 1

我认为您可以创建自己的存储池 (ARM 13.11 ff) 来支持额外的操作“new 可以吗？”。使其免受并发攻击会更加复杂。

我想你可以让它 Allocate 吞下异常和 return null。不管怎样，我认为你必须在“SPARK 之外”编写这样的程序！

Answer 2

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

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

注意：可以使用 GNAT CE 2021 证明所有指针取消引用和不存在内存泄漏。但是，实际上将 Valid 鉴别器设置为 [=20 会很好=] 在 Free 期间使用像 Post => P.Valid = False 这样的后置条件。不幸的是，这使得 SPARK 抱怨可能的判别检查失败。

更新（2021 年 6 月 3 日）

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

main.adb

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.ads

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;

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 已经可以证明无限递归（如评论中所述。请参阅 here), the only open issue that can result in a Storage_Error, would be a program that needs more stack during normal execution than what is available. This however can be monitored and also determined at compile time by tools like GNATstack (also mentioned in the comments. see here）。

如何在 Spark_Ada 中检查 Storage_Error

How to check for Storage_Error in Spark_Ada

ada

spark-ada