Hi-Lite high integrity showcase and overflow errors

Hi-Lite high integrity showcase and overflow errors

[Georg Bauhaus]

http://www.open-do.org/projects/hi-lite/a-lighter-introduction-to-hi-lite/
introduces AdaCore's new proof tools. This introduction makes me worry
about integrity, pardon me.

I have included the procedure Mult from the example, after correcting
it as suggested by the text. Mult should perform saturating arithmetic.

The high integrity example program fails miserably. (C programmers
should have a good laugh.)

The program compiles without any warnings. It also behaves as
instructed, but not as intended, I suppose. It either terminates
with an overflow check failure, or with a range check failure,
depending on whether GNAT was run in Ada mode (-gnato), or in GNAT mode.

So to ask a provocative question, what is the use of all these tools
if they still lead to programs that overflow so easily?

Or am I just incorrectly assuming thing and X * Y will make the tools
complain fiercely about possible overflow?

Or that this is just an example procedure and the real Mult and Add will
of course use suitable algorithms for testing the feasibility of the
arithmetical operations?


procedure Alicebob is

    type My_Int is range 0 .. 10_000;

    function Mult (X , Y : My_Int) return My_Int is
    begin
       if X * Y < 10_000 then
          return X * Y;
       else
          return 10_000;
       end if;
    end Mult;

begin
    if Mult (1000, 33) /= 10_000 then
       raise Program_Error;
    end if;
end Alicebob;

Re: Hi-Lite high integrity showcase and overflow errors

[Shark8]

	function Mult (X , Y : My_Int) return My_Int is
	begin
	    Return Result : My_Int:= X*Y;

	    -- When the constraint is exceeded we return the last value.
	    exception
		when Constraint_Error =>
		    Return My_Int'Last;
	end Mult;

There you are; that'll work as intended.

Re: Hi-Lite high integrity showcase and overflow errors

[Shark8]

Forgive the multiple posts, but this might be a little bit clearer; I certainly like that the [word] Return is not repeated.


	function Mult (X , Y : My_Int) return My_Int is
	begin
	    Return Result : My_Int do
		Result:= X*Y;

		-- When the constraint is exceeded we return the last value.
		exception
		when Constraint_Error =>
		    Result:= My_Int'Last;
	    End Return;
	end Mult;

Re: Hi-Lite high integrity showcase and overflow errors

[Georg Bauhaus]

On 04.09.12 05:05, Shark8 wrote:

> 	function Mult (X , Y : My_Int) return My_Int is
> 	begin
> 	    Return Result : My_Int do
> 		Result:= X*Y;
>
> 		-- When the constraint is exceeded we return the last value.
> 		exception
> 		when Constraint_Error =>
> 		    Result:= My_Int'Last;
> 	    End Return;
> 	end Mult;
>

Part of the exercise (which also mentions SPARK) is to have
programs that can drop support for exception handling, I should think.
Formally verified etc etc. So, no, this won't fly ;-)

When McJones & Stepanov introduced the idea behind their recent book
Stepanov has McJones put up a slide, titled "Respect the Domain", which
involves the quantity 2*b. The following lines are taken from near
00:41:45 of http://www.youtube.com/watch?v=Ih9gpJga4Vc:

   // Precondition: a ≥ b > 0
   if (a - b >= b) {  //! Not: a >= b + b

He points out that programmers need to work with potentially partial
functions; "+" is not everywhere defined; it can overflow.
We have to guard as in the Precondition, and "therefore, we could
subtract", even when most mathematicians would say this is stupid
(the meaning of the call-out bubble starting with //! above), which
it isn't because b + b might require more bits than are available.

That's much like X op Y in Hi-Lite's Mult/Add conditionals,
isn't it?

Re: Hi-Lite high integrity showcase and overflow errors

[Shark8]

On Tuesday, September 4, 2012 2:30:50 AM UTC-6, Georg Bauhaus wrote:
> On 04.09.12 05:05, Shark8 wrote:

Ah, I see; I'm not currently interested in SPARK but saw the problem in general Ada terms.  Here's the SPARK-safe version:

	function Mult (X , Y : My_Int) return My_Int is
	    Type Mod_X is mod 2**My_Int'Size; -- must be power-of-2 for mod
	    Tmp_X : Mod_X := Mod_X( X );
	    Tmp_Y : Mod_X := Mod_X( Y );
	    Tmp_R : Mod_X := Tmp_X * Tmp_Y;
	    Last  : Constant := Integer(My_Int'Last);
	begin
	    Return Result : My_Int do
		-- We need to check that the result of the modular operation
		-- isn'tin excess of the given constraint; then check if the
		-- result is less than one of the inputs, in either case we
		-- need to return the maximum number... this might be avoided
  		-- by making the mod-type's modular number the same as
		-- My_Int'Last, however as SPARK is mentioned here that may
		-- not be an option as only powers-of-2 are permitted.
		if (integer(tmp_r) > Last) or else (tmp_R < Tmp_X) then
		    Result:= My_Int'Last;
		else
		    Result:= My_Int( tmp_R );
		end if;
	    End Return;
	end Mult;

You have to use modular-types to bypass overflowing-errors, but then there's also the problem of non power-of-2 Last, which I address in the algorithm presented. Another problem is if the My_Int range has non-zero lower-bounds, in which case the "2**My_Int'Size" should be replaced with the proper static expression something like Log(My_Int'Last-My_Int'First), or some other appropriate bounds.

In general Ada I believe you can forgo the range-check by having the type be Mod (My_Int'Last-My_Int'First), with the offset of My_Int'First added/subtracted as necessary for the conversions.

Re: Hi-Lite high integrity showcase and overflow errors

[Florian Weimer]

* Georg Bauhaus:

> Or am I just incorrectly assuming thing and X * Y will make the tools
> complain fiercely about possible overflow?

The base range of My_Int could be sufficiently large so that the
multiplication wouldn't overflow, ever.  In this regard, integer types
aren't very portable.

On your architecture, you might see different behavior if My_Int is
defined like this:

   type My_Int is range 0 .. 40_000;

And the check is performed against 40_000 as well.

Eventually, you'll have to accept that a lot of Ada marketing material
is poorly prepared at best, and downright intellectually dishonest at
worst.  This is rather sad.

Re: Hi-Lite high integrity showcase and overflow errors

[Shark8]

On Tuesday, September 4, 2012 2:21:30 PM UTC-6, Florian Weimer wrote:
> * Georg Bauhaus:
> 
> > Or am I just incorrectly assuming thing and X * Y will make the tools
> > complain fiercely about possible overflow?
> 
> The base range of My_Int could be sufficiently large so that the
> multiplication wouldn't overflow, ever.  In this regard, integer types
> aren't very portable.
> 
> On your architecture, you might see different behavior if My_Int is
> defined like this:
> 
>    type My_Int is range 0 .. 40_000;
> And the check is performed against 40_000 as well.

Right; both checks are needed.

> Eventually, you'll have to accept that a lot of Ada marketing material
> is poorly prepared at best, and downright intellectually dishonest at
> worst.  This is rather sad.

It is. Of course I think it'd be a lot nicer if the material were commented 'like' my presented code (i.e. problem and solution described) -- simply describing what's happening can reveal a lot of problems that you never thought about initially.

Re: Hi-Lite high integrity showcase and overflow errors

[yannick.moy]

On Monday, September 3, 2012 11:56:28 PM UTC+2, Georg Bauhaus wrote:
> http://www.open-do.org/projects/hi-lite/a-lighter-introduction-to-hi-lite/
> introduces AdaCore's new proof tools. This introduction makes me worry
> about integrity, pardon me.

This is a natural concern when considering formal verification technology. As leader of the technical developments of GNATprove, I assure you that we always have it in mind.

And you are right on one thing: the code as presented in the "Light Introduction to Hi-Lite" does not fly. This is confirmed by running GNATprove on your code:

alicebob.adb:8:20: info: range check proved
alicebob.adb:8:20: info: overflow check proved
alicebob.adb:10:18: info: range check proved
alicebob.adb:7:13: overflow check not proved

Indeed, the possible overflow in line 7 (the test in Mult) can be raised at run-time, hence the overflow check failure when compiling with -gnato.

You can check these results by downloading GNATprove at http://www.open-do.org/projects/hi-lite/gnatprove/ and running:

$ gnatprove -P test --mode=prove --report=all

(with a simple test.gpr project file setting the language to Ada 2012)

> The high integrity example program fails miserably. (C programmers 
> should have a good laugh.)

You should take this example for what it is: an introduction to a research project. When I wrote this example, GNATprove did not exist. Instead, I used Frama-C and SPARK (and I have given the corresponding annotations). With these annotations, in particular the logical preconditions that X*Y<10000, then you can prove that Mult is safe, and still call Mult in a context where this precondition is not satisfied. One advantage of the new Ada 2012 executable annotations is that you can execute preconditions, which would catch the problem at the caller site.

Now that a prototype for GNATprove is available, you can check that Mult is indeed not safe as written. You can either add a precondition, or change My_Int definition into:
  subtype My_Int is Integer range 0 .. 10_000; 
With this definition, GNATprove now proves all checks in Mult:

alicebob.adb:8:20: info: range check proved
alicebob.adb:8:20: info: overflow check proved
alicebob.adb:10:18: info: range check proved
alicebob.adb:7:13: info: overflow check proved

I have modified the webpage to use this definition of Mult. Note that this verification is dependent on the base type of Mult, so dependent on the target for which you're doing the verification. That's a choice we have made for this technology, because we want to integrate proving and testing, and that requires knowledge of target features.

> So to ask a provocative question, what is the use of all these tools
> if they still lead to programs that overflow so easily?

They don't.

> Or am I just incorrectly assuming thing and X * Y will make the tools
> complain fiercely about possible overflow?

Not fiercely, but in all cases where it cannot prove that it does not overflow, it will issue an error message, yes.

Re: Hi-Lite high integrity showcase and overflow errors

[yannick.moy]

> Eventually, you'll have to accept that a lot of Ada marketing material
> is poorly prepared at best, 

Please consider this material is an introduction to a research project. We're not talking marketing material for a product. I think that we do a fair amount of efforts to publicize the goals, the discussions and the current state of the Hi-Lite research project. I invite you to subscribe to the public mailing-list where we discuss most of the technical issues in this project if you're interested:

http://lists.forge.open-do.org/mailman/listinfo/hi-lite-discuss

For a demo of what the prototype can currently handle, see the video demo or the User's Guide at:

http://www.open-do.org/projects/hi-lite/gnatprove/

> and downright intellectually dishonest at
> worst.  This is rather sad.

I hope I convinced you this is not the case.

Re: Hi-Lite high integrity showcase and overflow errors

[Georg Bauhaus]

On 05.09.12 11:19, yannick.moy wrote:
> One advantage of the new Ada 2012 executable annotations is that you can execute preconditions, which would catch the problem at the caller site.

Thanks for explaining. I'll assume, though, that for saturating
arithmetic, the caller would not want X op Y < 10_000 to be
checked as a precondition, as this prevents saturation. So the
postconditions are fine.

Re: Hi-Lite high integrity showcase and overflow errors

[Florian Weimer]

* yannick moy:

> Indeed, the possible overflow in line 7 (the test in Mult) can be
> raised at run-time, hence the overflow check failure when compiling
> with -gnato.

There's recent development in this area.

In FSF GCC trunk, there is now an overflow checking mode, enabled with
-gnato3, which causes the original program to behave as expected.  In
this mode, signed integer arithmetic does not result in intermediate
overflows, and comparisons between signed integers yield the
mathemtically defined result.  In some cases, this requires arbitrary
precision arithmetic at run time, but it really helps to avoid
Constraint_Error exceptions.