How to check for potential overflow in Ada when dealing with expression?

user_10310957 0
Viewed 1042

I am relatively new to Ada and have been using Ada 2005. However, I feel like this question is pertinent to all languages.

I am currently using static analysis tools such as Codepeer to address potential vulnerabilities in my code.

One problem I'm debating is how to handle checks before assigning an expression that may cause overflow to a variable.

This can be explained better with an example. Let's say I have a variable of type unsigned 32-bit integer. I am assigning an expression to this variable CheckMeForOverflow:

CheckMeForOverflow := (Val1 + Val2) * Val3;

My dilemma is how to efficiently check for overflow in cases such as this - which would seem to appear quite often in code. Yes, I could do this:

if ((Val1 + Val2) * Val3) < Unsigned_Int'Size then
    CheckMeForOverflow := (Val1 + Val2) * Val3;
end if;

My issue with this is that this seems inefficient to check the expression and then immediately assign that same expression if there is no potential for overflow.

However, when I look online, this seems to be pretty common. Could anyone explain better alternatives or explain why this is a good choice? I don't want this scattered throughout my code.

I also realize I could make another variable of a bigger type to hold the expression, do the evaluation against the new variable, and then assign that variable's value to CheckMeForOverflow, but then again, that would mean making a new variable and using it just to perform a single check and then never using it again. This seems wasteful.

Could someone please provide some insight?

Thanks so much!

codepeer ada
2 Answers

Personally I would do something like this

begin
   CheckMeForOverflow := (Val1 + Val2) * Val3;
exception
   when constraint_error =>
                 null; --  or log that it overflowed
end;

But take care that your variable couldn't have a usable value.

It's clearer than an if construct and we don't perform the calculation twice.

user_16770890

This is exactly the problem SPARK can help solve. It allows you to prove you won't have runtime errors given certain assumptions about the inputs to your calculations.

If you start with a simple function like No_Overflow in this package:

with Interfaces; use Interfaces;

package Show_Runtime_Errors is

   type Unsigned_Int is range 0 .. 2**32 - 1;
   function No_Overflow (Val1, Val2, Val3 : Unsigned_Int) return Unsigned_Int;

end Show_Runtime_Errors;


package body Show_Runtime_Errors is

   function No_Overflow (Val1, Val2, Val3 : Unsigned_Int) return Unsigned_Int is
      Result : constant Unsigned_Int := (Val1 + Val2) * Val3;
   begin
      return Result;
   end No_Overflow;

end Show_Runtime_Errors;

Then when you run SPARK on it, you get the following:

Proving...
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
show_runtime_errors.adb:4:55: medium: range check might fail (e.g. when Result = 10)
show_runtime_errors.adb:4:55: medium: overflow check might fail (e.g. when
   Result = 9223372039002259450 and Val1 = 4 and Val2 = 2147483646 and
   Val3 = 4294967293)
gnatprove: unproved check messages considered as errors
exit status: 1

Now if you add a simple precondition to No_Overflow like this:

function No_Overflow (Val1, Val2, Val3 : Unsigned_Int) return Unsigned_Int with
   Pre => Val1 < 2**15 and Val2 < 2**15 and Val3 < 2**16;

Then SPARK produces the following:

Proving...
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
Success!

Your actual preconditions on the ranges of the inputs will obviously depend on your application.

The alternatives are the solution you are assuming where you put lots of explicit guards in your code before the expression is evaluated, or to catch runtime errors via exception handling. The advantage of SPARK over these approaches is that you do not need to build your software with runtime checks if you can prove ahead of time there will be no runtime errors.

Note that preconditions are a feature of Ada 2012. You can also use pragma Assert throughout your code which SPARK can take advantage of for doing proofs.

For more on SPARK there is a tutorial here: https://learn.adacore.com/courses/intro-to-spark/index.html

To try it yourself, you can paste the above code in the example here: https://learn.adacore.com/courses/intro-to-spark/book/03_Proof_Of_Program_Integrity.html#runtime-errors

Incidentally, the code you suggested:

if ((Val1 + Val2) * Val3) < Unsigned_Int'Size then
    CheckMeForOverflow := (Val1 + Val2) * Val3;
end if;

won't work for two reasons:

  1. Unsigned_Int'Size is the number of bits needed to represent Unsigned_Int. You likely wanted Unsigned_Int'Last instead.
  2. ((Val1 + Val2) * Val3) can overflow before the comparison to Unsigned_Int'Last is even done. Thus you will generate an exception at this point and either crash or handle it in an exception handler.
user_1898780
Related