I would like to create a function in SPARK_Mode that utilizes the GNAT GCC intrinsic function "__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;
I would like to assume the postcondition to be true since it is the definition of the number of trailing zeros which is implied by the documentation. However, I am unsure how to accomplish this, having read much documentation and having tried to use "pragma Assume". I am relatively new to Ada/SPARK and am using GNAT Community 2020. Can someone please help me solve this issue so that gnatprove is able to prove the postcondition of CTZLL?
When I formulate the postcondition (contract) of __builtin_ctzll using Shift_Right, I'm able proof (using GNAT CE 2020 and proof level 1) that test.adb is free of run-time errors if it would be run.
Note: Related documentation: SPARK user's manual, section 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;
output (of 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
For those not familiar with __builtin_ctzll: returns the number of trailing 0-bits in x, starting at the least significant bit position. If x is 0, the result is undefined. See also here. Example:
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;
output (of 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