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

Question

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?

You can’t prove the postcondition (`gnatprove` would need to see into the intrinsic code). What you can do is write a postcondition that will enable you to prove that code using `CTZLL` is OK; and use other means to demonstrate to your satisfaction that `CTZLL` does in fact behave like the contract says. — Simon Wright, Jul 10 '20 at 22:49

DeeDee · Accepted Answer · 2020-07-11T08:52:11.490

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

Your latest changes to the postcondition take on board my comment *which doesn’t seem to have been posted*. Is this thought transference?! (I may have just forgotten to post it!) — Simon Wright, Jul 11 '20 at 12:35
Is there any way to just assume to postcondition to be true in order to prove another function that uses CTZLL? I'm not sure how to approach this. For example, the binary GCD algorithm uses CTZLL in order to greatly improve performance. — , Jul 11 '20 at 14:34
@alfxs As @Simon Wright already mentioned in its comment to the original question, `gnatprove` cannot proof a postcondition to hold for an imported subprogram and therefore *assumes* that the postcondition will hold if the precondition holds (in this case, the functional relation between `X` and the result of `CTZLL` will hold iff `X /= 0`). Whether the contract (in this case the relation) is either accurate enough, or formulated in a way useful for `gnatprove` to prove other conditions in the algorithm of which `CTZLL` is part, depends on the conditions to be verified in the algorithm. — DeeDee, Jul 11 '20 at 15:02
@alfxs Since you mention the GCD algorithm: there's a nice blog post available that discusses an approach to proof the functional behavior of the GCD algorithm using SPARK: [Proving the Ghost Common Divisor (GCD)](https://blog.adacore.com/gnatprove-tips-and-tricks-proving-the-ghost-common-denominator-gcd). You might've already found it, but I thought I mention it for completeness. The code is available in GNAT CE 2020 (GNAT Studio > Help > SPARK > Examples > gcd). — DeeDee, Jul 11 '20 at 15:12

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

1 Answers1