SPARK-Ada с использованием GNATProve для принятия постусловия функции G CC Intrinsi c - PullRequest
Новая
       72

SPARK-Ada с использованием GNATProve для принятия постусловия функции G CC Intrinsi c

4 голосов
/ 10 июля 2020

Я хотел бы создать функцию в SPARK_Mode, которая использует GNAT G CC intrinsi c функцию «__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;

Я хотел бы предположить, что постусловие истинно, поскольку оно это определение количества нулей в конце, которое подразумевается в документации. Однако я не уверен, как это сделать, sh прочитав много документации и попытавшись использовать "pragma Assume". Я относительно новичок в Ada / SPARK и использую GNAT Community 2020. Может ли кто-нибудь помочь мне решить эту проблему, чтобы gnatprove смог доказать постусловие CTZLL?

1 Ответ

4 голосов
/ 11 июля 2020

Когда я формулирую постусловие (контракт) __builtin_ctzll с использованием Shift_Right, я могу доказать (используя GNAT CE 2020 и уровень доказательства 1), что test.adb не содержит ошибок времени выполнения, если бы это было run.

Примечание: Связанная документация: руководство пользователя SPARK, раздел 7.4.5: Написание контрактов на импортированные подпрограммы .

intrinsi c .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: возвращает количество завершающих 0-битов в x, начиная с позиции младшего разряда. Если x равен 0, результат не определен. См. Также здесь . Пример:

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