Как проверить возможное переполнение в Аде при работе с выражением?

Я относительно новичок в 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, но опять же, это будет означать создание новой переменной и ее использование только для выполните одну проверку и никогда больше не используйте ее. Это кажется расточительным.

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

Огромное спасибо!

Вы осмотрели сборку? Я надеюсь, что даже скромная оптимизация сохранит результат выражения в регистре, а затем повторно использует его после условного. Таким образом, ты не нужно выполнять дополнительную работу.

Jeff Holt 03.09.2018 17:40

Насколько мне известно, вы можете получить CodePeer только при наличии контракта на поддержку AdaCore. Используй это! они хороши. (Пожалуйста, поправьте меня, если я ошибаюсь насчет CodePeer, я бы определенно хотел его попробовать!)

Simon Wright 03.09.2018 18:02

Я считаю, что есть несколько способов справиться с такими случаями. Например, вы можете использовать переменную большего размера (скажем, uint64), присвоить ей значение, а затем получить if less than max assign calculated value else maximum. Другой вариант (я думаю, лучше и чище) - использовать нетипизированную константу, поскольку константы могут быть максимально точными. Таким образом, у вас получится что-то вроде function Calc (V1, V2, V3) constant exp := (V1 + V2) * V3; begin if exp < max then return exp; else return max; end;.

NeoSer 07.09.2018 16:14

Если ваше выражение переполняется, оно будет переполнено как в условии «if», так и в присваивании, поэтому вы ничего не получите с «if». Кроме того, Unisgned_Int'Size будет небольшим числом, поэтому я подозреваю, что вы имели в виду что-то еще.

Jeffrey R. Carter 15.09.2018 14:37
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
5
4
639
2
Перейти к ответу Данный вопрос помечен как решенный

Ответы 2

Ответ принят как подходящий

Лично я бы сделал что-то вроде этого

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

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

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

И теперь CheckMeForOverflow имеет свое предыдущее значение (может даже быть неинициализированным) без предупреждения. А если проверки отключены?

Simon Wright 04.09.2018 09:05

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

Frédéric Praca 04.09.2018 09:10

О том, что переменная может иметь неправильное значение, поэтому я поставил не могло иметь полезной ценности.

Frédéric Praca 04.09.2018 09:13

Если проверки отключены, код, который на них полагается, ошибочен. Ошибочный код следует исправить.

Jeffrey R. Carter 15.09.2018 14:43

@ JeffreyR.Carter Я снова полностью согласен, но процитирую ARM Нет никакой гарантии, что подавленная проверка действительно удалена; следовательно, прагму Suppress следует использовать только из соображений эффективности.

Frédéric Praca 27.09.2018 11:03

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

Frédéric Praca 27.09.2018 11:06

Именно эту проблему может решить 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;

Тогда СПАРК выдаст следующее:

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

"не сработает по двум причинам", не могу не согласиться! Для меня вопрос был трудным для понимания по этим двум причинам. В конечном итоге он заканчивается либо «Докажи» (SPARK), либо «Закодируй».

LoneWanderer 09.09.2018 19:50

Другие вопросы по теме