在处理表达式时如何检查Ada中的潜在溢出？

Question

我对Ada相对较新,并且一直在使用Ada 2005.但是,我觉得这个问题与所有语言相关.

我目前正在使用Codepeer等静态分析工具来解决代码中的潜在漏洞.

我正在讨论的一个问题是如何在分配可能导致变量溢出的表达式之前处理检查.

通过示例可以更好地解释这一点.假设我有一个无符号32位整数类型的变量.我正在为这个变量CheckMeForOverflow分配一个表达式:

CheckMeForOverflow := (Val1 + Val2) * Val3;

我的困境是如何在这种情况下有效地检查溢出 - 这似乎在代码中经常出现.是的,我可以这样做:

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

我的问题是,检查表达式似乎效率低,然后在没有溢出可能的情况下立即分配相同的表达式.

但是,当我在网上看时,这似乎很常见.谁能解释更好的替代方案或解释为什么这是一个不错的选择？我不想把它分散在我的代码中.

我还意识到我可以创建一个更大类型的另一个变量来保存表达式,对新变量进行评估,然后将该变量的值分配给CheckMeForOverflow,但是再次,这将意味着创建一个新变量并将其用于执行一次检查,然后再也不再使用它.这似乎很浪费.

有人可以提供一些见解吗？

非常感谢!

Answer 1

这正是 SPARK 可以帮助解决的问题。它允许您证明在给定计算输入的某些假设的情况下不会出现运行时错误。

如果您从像这个包中这样的简单函数开始No_Overflow：

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;

然后当你在上面运行 SPARK 时，你会得到以下结果：

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

现在，如果您添加一个简单的前提条件，No_Overflow如下所示：

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

然后 SPARK 产生以下结果：

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

您对输入范围的实际先决条件显然取决于您的应用程序。

替代方案是您假设的解决方案，在计算表达式之前在代码中放置大量显式保护，或者通过异常处理捕获运行时错误。与这些方法相比，SPARK 的优势在于，如果您可以提前证明不会出现运行时错误，则无需在构建软件时进行运行时检查。

请注意，前提条件是 Ada 2012 的一项功能。您还可以pragma Assert在整个代码中使用 SPARK 可以利用的功能来进行证明。

有关 SPARK 的更多信息，请参阅此处的教程： https ://learn.adacore.com/courses/intro-to-spark/index.html

要亲自尝试，您可以将上述代码粘贴到此处的示例中： https://learn.adacore.com/courses/intro-to-spark/book/03_Proof_Of_Program_Integrity.html#runtime-errors

顺便说一句，您建议的代码：

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

不起作用有两个原因：

1. Unsigned_Int'Size是表示 所需的位数Unsigned_Int。你可能想要的Unsigned_Int'Last是。
2. ((Val1 + Val2) * Val3)在比较Unsigned_Int'Last完成之前可能会溢出。因此，此时您将生成一个异常，并崩溃或在异常处理程序中处理它。

Answer 2

就我个人而言，我会做这样的事情

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

但请注意，您的变量不能具有可用值。

它比 if 结构更清晰，而且我们不会执行两次计算。