SPARK-Ada 使用 GNATProve 假设 GCC 内函数的后置条件

Question

我想在 SPARK_Mode 中创建一个使用 GNAT GCC 内部函数“__builtin_ctzll”的函数。

with Interfaces; use Interfaces;
package GCC_Intrinsic with
   SPARK_Mode
is

   function DividesLL (A, B : Unsigned_64) return Boolean is (B mod A = 0) with
      Ghost,
      Pre => A /= 0;

   function CTZLL (X : Unsigned_64) return Natural with
      Pre  => X /= 0,
      Post => CTZLL'Result in 0 .. Unsigned_64'Size - 1
      and then DividesLL (Unsigned_64 (2)**CTZLL'Result, X)
      and then
      (for all Y in CTZLL'Result + 1 .. Unsigned_64'Size - 1 =>
         not DividesLL (Unsigned_64 (2)**Y, X));
   
   pragma Import (Intrinsic, CTZLL, "__builtin_ctzll");

end GCC_Intrinsic;

我想假设后置条件为真，因为它是文档隐含的尾随零数的定义。但是，我不确定如何完成此操作，阅读了大量文档并尝试使用“pragma Assume”。我是 Ada/SPARK 的新手，正在使用 GNAT Community 2020。有人可以帮我解决这个问题，以便 gnatprove 能够证明 CTZLL 的后置条件吗？

Answer 1

当我使用 Shift_Right 制定 __builtin_ctzll 的后置条件（合同）时，我能够证明（使用 GNAT CE 2020 和证明级别 1）test.adb 没有运行-时间错误，如果是运行.

注意：相关文档：SPARK 用户手册，第 7.4.5 节：Writing Contracts on Imported Subprograms.

intrinsic.ads

pragma Assertion_Policy (Check);

with Interfaces; use Interfaces;

package Intrinsic with SPARK_Mode is

   --  Count Trailing Zeros (long long unsigned).
   
   function CTZLL (X : Unsigned_64) return Natural with
     Pre  => X /= 0,       
     Post => CTZLL'Result in 0 .. Unsigned_64'Size - 1 and
             (for all I in 0 .. CTZLL'Result - 1 =>
                (Shift_Right (X, I) and 2#1#) = 2#0#) and 
             (Shift_Right (X, CTZLL'Result) and 2#1#) = 2#1#;

   --  You could also use aspects (Import, Convention, External_Name).
   pragma Import (Intrinsic, CTZLL, "__builtin_ctzll");
   
end Intrinsic;

test.adb

pragma Assertion_Policy (Check);

with Interfaces; use Interfaces;
with Intrinsic;  use Intrinsic;

procedure Test with SPARK_Mode is
begin
   
   --  Absence of Run-Time Errors (AoRTE) for this program can be proven:
   --  Assert_Failure will not be raised at runtime.
   
   pragma Assert (CTZLL ( 1) = 0);
   pragma Assert (CTZLL ( 2) = 1);
   pragma Assert (CTZLL ( 3) = 0);
   pragma Assert (CTZLL ( 4) = 2);
   pragma Assert (CTZLL ( 5) = 0);
   pragma Assert (CTZLL ( 6) = 1);
   pragma Assert (CTZLL ( 7) = 0);
   pragma Assert (CTZLL ( 8) = 3);
   pragma Assert (CTZLL ( 9) = 0);
   pragma Assert (CTZLL (10) = 1);
      
   pragma Assert (CTZLL (2 ** 63    ) = 63);
   pragma Assert (CTZLL (2 ** 64 - 1) =  0);
   
end Test;

输出（gnatprove）

$ gnatprove -P default.gpr -j0 -u test.adb --level=1 --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
test.adb:12:19: info: precondition proved
test.adb:12:19: info: assertion proved
[...]
test.adb:24:19: info: precondition proved
test.adb:24:19: info: assertion proved

对于那些不熟悉 __builtin_ctzll 的人：returns x 中尾随 0 位的数量，从最低有效位开始。如果 x 为 0，则结果未定义。另见 here。示例：

main.adb

with Ada.Text_IO;         use Ada.Text_IO;
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;
with Interfaces;          use Interfaces;
with Intrinsic;           use Intrinsic;

procedure Main is
begin
   for K in 1 .. 10 loop
      Put (K, Width => 3);
      Put (K, Width => 9, Base => 2);
      Put (CTZLL (Unsigned_64 (K)), Width => 4);
      New_Line;
   end loop;
end Main;

输出（Main）

$ ./obj/main
  1     2#1#   0
  2    2#10#   1
  3    2#11#   0
  4   2#100#   2
  5   2#101#   0
  6   2#110#   1
  7   2#111#   0
  8  2#1000#   3
  9  2#1001#   0
 10  2#1010#   1

SPARK-Ada 使用 GNATProve 假设 GCC 内函数的后置条件

SPARK-Ada Using GNATProve to Assume a Postcondition of a GCC Intrinsic Function

ada

spark-ada