Как проверить наличие потенциального переполнения в Ada при работе с выражением? - PullRequest
Новая
       11

Как проверить наличие потенциального переполнения в Ada при работе с выражением?

0 голосов
/ 03 сентября 2018

Я относительно новичок в Аде и использую Аду 2005. Однако я чувствую, что этот вопрос относится ко всем языкам.

В настоящее время я использую инструменты статического анализа, такие как Codepeer, для устранения потенциальных уязвимостей в моем коде.

Одна проблема, которую я обсуждаю, заключается в том, как обрабатывать проверки перед назначением выражения, которое может вызвать переполнение переменной.

Это лучше объяснить на примере. Допустим, у меня есть переменная типа unsigned 32-bit integer. Я назначаю выражение для этой переменной CheckMeForOverflow: 

CheckMeForOverflow := (Val1 + Val2) * Val3;

Моя дилемма заключается в том, как эффективно проверять переполнение в таких случаях, как это, что, по-видимому, довольно часто встречается в коде. Да, я мог бы сделать это: 

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

Моя проблема с этим заключается в том, что кажется неэффективным проверять выражение, а затем немедленно назначать это же выражение, если нет возможности переполнения.

Однако, когда я смотрю в Интернете, это кажется довольно распространенным явлением. Может ли кто-нибудь объяснить лучшие альтернативы или объяснить, почему это хороший выбор? Я не хочу, чтобы это разбросано по всему коду.

Я также понимаю, что мог бы создать другую переменную большего типа для хранения выражения, выполнить сравнение с новой переменной, а затем присвоить значение этой переменной CheckMeForOverflow, но, опять же, это означало бы создание новой переменной и использование это просто выполнить одну проверку, а затем никогда не использовать ее снова. Это кажется расточительным.

Может ли кто-нибудь дать какое-то понимание?

Большое спасибо!

Ответы [ 2 ]

0 голосов
/ 09 сентября 2018

Это именно та проблема, которую 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. Таким образом, вы сгенерируете исключение на этом этапе и либо аварийно завершите работу, либо обработаете его в обработчике исключений.
0 голосов
/ 03 сентября 2018

Лично я бы сделал что-то подобное 

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

Но позаботьтесь о том, чтобы ваша переменная не могла иметь полезного значения.

Это понятнее, чем конструкция if, и мы не выполняем вычисления дважды.

...