Saya ingin membuat fungsi di SPARK_Mode yang menggunakan fungsi intrinsik 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;

Saya ingin menganggap postcondition itu benar karena itu adalah definisi dari jumlah nol tambahan yang tersirat oleh dokumentasi. Namun, saya tidak yakin bagaimana mencapai ini, setelah membaca banyak dokumentasi dan mencoba menggunakan "pragma Asumsi". Saya relatif baru di Ada/SPARK dan saya menggunakan Komunitas GNAT 2020. Adakah yang bisa membantu saya memecahkan masalah ini sehingga gnatprove dapat membuktikan postcondition CTZLL?

4
alfxs 10 Juli 2020, 21:51

1 menjawab

Jawaban Terbaik

Ketika saya merumuskan postcondition (kontrak) __builtin_ctzll menggunakan Shift_Right, saya dapat membuktikan (menggunakan GNAT CE 2020 dan pembuktian level 1) bahwa test.adb bebas dari kesalahan run-time jika itu akan dijalankan.

Catatan: Dokumentasi terkait: Panduan pengguna SPARK, bagian 7.4.5: Menulis Kontrak pada Subprogram yang Diimpor.

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;

keluaran (dari 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

Bagi mereka yang tidak terbiasa dengan __builtin_ctzll: mengembalikan jumlah bit 0 yang tertinggal di x, mulai dari posisi bit paling tidak signifikan. Jika x adalah 0, hasilnya tidak terdefinisi. Lihat juga di sini. Contoh:

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;

keluaran (dari 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
4
DeeDee 11 Juli 2020, 08:52