ada - 如何检查 Spark_Ada 中的 Storage_Error

Question

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

通过验证，可以排除大多数运行时错误发生在编写的程序中，但无法排除像 Storage_Error 这样的异常。

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

我想做的事情:

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

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

如何在 Spark 中处理此类异常？

Answer 1

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

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

注意:所有指针取消引用和不存在内存泄漏都可以使用 GNAT CE 2021 来证明。但是，最好将 Valid 鉴别器实际设置为 False 在 Free 期间使用后置条件，例如 Post => P.Valid = False。不幸的是，这使得 SPARK 提示可能的判别检查失败。

更新(2021 年 6 月 3 日)

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

ma​​in.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;

测试.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;

测试.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添加)

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