在处理表达式时如何检查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

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

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

但要注意你的变量没有可用的值。

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

Answer 2

这正是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添加一个简单的前置条件，如下所示：

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

然后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

顺便提一下，您建议的代码：

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

不会有两个原因：

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