Как это возможно, в Аде, чтобы иметь ошибку кода из-за присвоения 64-битного числа с плавающей запятой 16-битному целому числу?

Question

Я только что обнаружил этот отчет о причинах отказа ракеты Ariane 5.Согласно отчету, сбой произошел, когда 64-разрядному числу с плавающей запятой было присвоено 16-разрядное целое число.

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

Существует также вопрос, почему не существует обработчика исключений для этого условия, что также является своеобразным,но, возможно, скорее неудача программиста, чем языка - хотя проект Ada, который оставил живой код с потенциальными исключениями, но без обработчика исключений, трудно представить.

Есть идеи?

http://www -users.math.umn.edu / ~ arnold / disasters / ariane5rep.html

Answer 1

Целью кода было управлять ракетой.Что бы сделал обработчик исключений?Играть на похороны, когда ракета разбивается?Когда сработало бы исключение, было бы слишком поздно: не было данных для расчета уравнений управления для фактического управления транспортным средством, начиная с этого момента.

Answer 2

Короче говоря: это не просто проблема программирования, это более сложная проблема

Дефект в Ariane 5 не был вызван ни одной причиной.На протяжении всего процесса разработки и тестирования было много этапов, на которых этот дефект мог быть выявлен.

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

• Система обнаружила и распознала ошибку.К сожалению, спецификация механизма обработки ошибок была непоследовательной и привела к окончательному уничтожению.

• Ошибочный модуль никогда не был должным образом протестирован в новой среде - ни на уровне оборудования, ни на уровне системной интеграции.Поэтому ошибка разработки и реализации не была обнаружена.

См. Diff с правильным кодом:

--- LIRE_DERIVE.ads 000 Tue Jun 04 12:00:00 1996
+++ LIRE_DERIVE.ads Fri Jan 29 13:50:00 2010
@@ -3,10 +3,17 @@
 if L_M_BV_32 > 32767 then
     P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
 elsif L_M_BV_32 < -32768 then
     P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
 else
     P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BV_32));
 end if;

-P_M_DERIVE(T_ALG.E_BH) := 
-  UC_16S_EN_16NS (TDB.T_ENTIER_16S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH)));
+L_M_BH_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH));
+
+if L_M_BH_32 > 32767 then
+    P_M_DERIVE(T_ALG.E_BH) := 16#7FFF#;
+elsif L_M_BH_32 < -32768 then
+    P_M_DERIVE(T_ALG.E_BH) := 16#8000#;
+else
+    P_M_DERIVE(T_ALG.E_BH) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BH_32));
+end if;

---

Более подробная информация:

A) The “Ошибка операнда »произошла из-за неожиданно большого значения ЧД (горизонтального смещения), рассчитанного внутренней функцией на основе значения« горизонтальной скорости », измеренного датчиками на платформе.

Значение ЧД служило индикатором точности позиционирования Платформы.значение ЧД оказалось намного больше, чем ожидалось, поскольку траектория полета Ariane 5 на ранней стадии значительно отличалась от траектории полета Ariane 4 (где этот программный модуль использовался ранее), что привело к значительно более высокой «горизонтальной скорости».».

Последним действием, имевшим фатальные последствия, было прекращение работы процессора.Соответственно вся навигационная система перестала функционировать.Было технически невозможно возобновить ее действия.

B) Однако Ariane 5, в отличие от предыдущей модели, обладал принципиально иной дисциплиной для выполнения предполетных действий - настолько отличающейся, что работа рокового программного модуля после времени запуска вообще не имела смысла,Однако модуль был повторно использован без каких-либо изменений.

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

Это было их очень сознательное решение добавить надлежащую защиту к четырем переменным и оставить три - включая ЧД - незащищенными.Причиной этого решения стало убеждение, что для этих трех переменных возникновение ситуации переполнения в принципе невозможно.

Эта достоверность была подтверждена расчетами, показывающими, что ожидаемый диапазон физических параметров полета, на основании которых определяются значения этих переменных, таков, что не может привести к нежелательной ситуации.И это было правдой - но для траектории, рассчитанной для модели Ariane 4.

И ракета нового поколения Ariane 5 была запущена по совершенно другой траектории, для которой оценки не проводились.Между тем, оно (вместе с высоким начальным ускорением) было таким, что «горизонтальная скорость» превышала расчетную (для Ariane 4) более чем в пять раз.

Защита для всех семи (включая BH) переменных не была предоставлена, поскольку для компьютера IRS была объявлена ​​максимальная рабочая нагрузка в 80%.Разработчики должны были искать способы уменьшить ненужные вычислительные затраты, и они ослабили защиту, где теоретически нежелательная ситуация не могла возникнуть.Когда он возник, такой механизм обработки исключений вступил в действие, который оказался совершенно неадекватным.

Этот механизм включал следующие три основных действия.

• Информация о возникновении чрезвычайной ситуации должна передаваться черезшина к бортовому компьютеру OBC.

• Параллельно она - вместе со всем контекстом - записывалась в перепрограммируемую память EEPROM (которую в ходе исследования можно было восстановить и прочитать ее содержимое).

• Процессор IRS должен был выйти из строя.

Последнее действие оказалось фатальным - именно он произошел в ситуации, которая на самом деле была нормальной (несмотря на исключение программного обеспечения, созданное из-за незащищенного переполнения), что привело к катастрофе.

C) Скорость была представлена ​​в виде 64-разрядного числа с плавающей запятой.Преобразование в 16-разрядное целое число со знаком вызвало переполнение. Текущая скорость Ariane 5 была слишком высока, чтобы представить ее как 16-разрядное целое число. Обработка ошибок была исключена из соображений производительности

(защита для всех семи (включаяПеременные не были предоставлены, поскольку для компьютера IRS была объявлена ​​максимальная рабочая нагрузка в 80%. Разработчикам пришлось искать способы уменьшить ненужные вычислительные затраты, и они ослабили защиту там, где теоретически нежелательная ситуация не могла возникнуть.)

Согласно презентации Жан-Жака Леви (1049 * 1 , 2 ) (которая была частью команды, которая искала источник проблемы), фактический исходный код в Аде, которыйпричиной проблемы было следующее .:

-- Vertical velocity bias as measured by sensor

L_M_BV_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BV) * G_M_INFO_DERIVE(T_ALG.E_BV));

-- Check, if measured vertical velocity bias ban be 
-- converted to a 16 bit int. If so, then convert

if L_M_BV_32 > 32767 then
    P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
elsif L_M_BV_32 < -32768 then
    P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
else
    P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BV_32));
end if;

-- Horizontal velocity bias as measured by sensor -- is converted to a 16 bit int without checking P_M_DERIVE

P_M_DERIVE(T_ALG.E_BH) := UC_16S_EN_16NS (TDB.T_ENTIER_16S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH)));

Последняя строка (показанная здесь в виде двух строк текста) вызвала переполнение, при котором преобразование из 64 битов в 16 битов без знака не защищено.Предыдущий код защищен тестированием перед присвоением, если число слишком велико.

Правильный код был бы:

L_M_BV_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BV) * G_M_INFO_DERIVE(T_ALG.E_BV));

if L_M_BV_32 > 32767 then
    P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
elsif L_M_BV_32 < -32768 then
    P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
else
    P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BV_32));
end if;

L_M_BH_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH));

if L_M_BH_32 > 32767 then
    P_M_DERIVE(T_ALG.E_BH) := 16#7FFF#;
elsif L_M_BH_32 < -32768 then
    P_M_DERIVE(T_ALG.E_BH) := 16#8000#;
else
    P_M_DERIVE(T_ALG.E_BH) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BH_32));
end if;

Другими словами, такая же проверка переполнения должна была присутствовать для горизонтальной части расчета (E_BH), как уже присутствовала длявертикальная часть расчета (E_BV).

'Источник: http://moscova.inria.fr/~levy/talks/10enslongo/enslongo.pdf

(По 2019-01-24 можно найти по адресу: http://para.inria.fr/~levy/talks/10enslongo/enslongo.pdf)

https://habr.com/ru/company/pvs-studio/blog/306748/

https://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%A9%E3%82%B9%E3%82%BF%E3%83%BC%E3%83%9F%E3%83%83%E3%82%B7%E3%83%A7%E3%83%B3

Answer 3

Ответ прост: всегда возможно явное преобразование, и, кажется, это было сделано с помощью кода Ariane 5:

-- Overflow is correctly handled for the vertical component
L_M_BV_32 := TBD.T_ENTIER_16S((1.0 / C_M_LSB_BH) *
                                   G_M_INFO_DERIVE(T_ALG.E_BH));
if L_M_BV_32 > 32767 then
 P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
elseif L_M_BV_32 < -32768 then
 P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
else
 P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TBD.T_ENTIER_16S(L_M_BV_32));
end if;

-- But not for the horizontal one
P_M_DERIVE(T_ALG.E_BH) := UC_16S_EN_16NS(TBD.T_ENTIER_16S
                                   ((1.0 / C_M_LSB_BH) *
                                   G_M_INFO_DERIVE(T_ALG.E_BH));

Здесь функция T_ENTIER_16Sбез сомнения преобразует число с плавающей запятой в 16-битное значение со знаком.Обратите внимание, что «ENTIER» по-французски, так что функция, вероятно, доступна из внутренней библиотеки.

Как обработать явное преобразование с плавающей запятой в целочисленное в Ada, конечно, доступно с вашего любимого сайта Q / A .

---

Для Ады преобразование очень явное;программисты должны подумать о сценарии.Но, возможно, они и думали, что это никогда не должно произойти.Расчет, вероятно, также должен быть производительным;В конце концов, время полета ракеты является существенным.

То, что результат вычисления не требует очень высокой точности, ясно из вертикальных вычислений: оно просто максимизирует значения 16-битногоцелое число со знаком вместо обновления целого числа до 32 бит.Возврат отрицательных значений значений, близких к нулю, - это то, что приводит к сбою - это приведет к слишком сильному искажению вычислений.

Имейте в виду, что максимальное ограничение ограниченного целого значения является мерой с ограничением, которое может работать не во всех случаях.ситуация.«Окончательное решение», используемое для этого проекта, может не работать в вашем проекте.

---

Обратите внимание, что каким-то образом они предположили, что возвращение почти случайного значения сделало большесмысл тогда выбрасывать исключение в функцию T_ENTIER_16S.это возможно из-за соображений производительности;функция может просто скопировать соответствующие биты, сохранив два оператора if для проверки на переполнение / недостаточное заполнение.

Исключения хороши, но они не имеют большого значения для такого рода вычислений во время выполнения.Проблема в том, что ракета зависит от функции, которая должна выполняться правильно.Если этого не произойдет, он потерпит неудачу и рухнет.Единственное время, когда исключение удобно, это когда есть регресс.В противном случае исключения могут просто помочь с анализом ошибки после факта.

---

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

И код в полете - когда утверждения отключены - мог возвращать значения MIN / MAX вместо прямого представления битов.Все лучше, чем возвращать совершенно неожиданные результаты.То есть: если дополнительное тестирование значений не является проблемой в отношении времени выполнения функции.