Блог

Мне нужно разобрать литералы с плавающей запятой в коде C, используя OCaml.

Тип float в OCaml 64-разрядный. У меня есть строка литерала, ее числовое значение, округленное до 64 бит, и его вид (float, double или long double).

Проблема заключается в литералах с числовым значением больше 64 бит:

1. длинные двойные литералы
2. литералы с плавающей запятой с ‘f’-суффиксом, для которых возникали бы ошибки двойного округления, если бы у них не было суффикса.

Модуль произвольной точности OCaml может анализировать рациональные числа из строк типа «123/123», но не «123.123», «123e123», «0x1.23p-1», как они могли бы появиться в C.

Справочная информация: Я выполняю анализ значений программ на C, используя CIL.

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

Я написал свой ответ в форме сообщения в блоге

Подводя итог некоторым пунктам здесь: вы могли бы использовать интерфейс strtold() и strtof() из OCaml. В первом случае вам нужно было бы подумать о том, как вы собираетесь сохранить полученный результат, поскольку в вашей архитектуре хоста есть только точка, которая long double больше double , чем в вашей хост-системе. Остается проблема, заключающаяся в том, что эти функции содержат ошибки в одной из наиболее широко используемых библиотек C. Очень немного глючит, но глючит именно для тех примеров, которые будут интересны, если вы делаете это для изучения двойного округления.

Другой способ — написать свою собственную функцию, начиная с другого поста в блоге, на который вы ссылаетесь.

Наконец, фраза «Даже для правильного получения плавающих значений с одинарной точностью требуется, чтобы я анализировал литералы со значениями больше 64 бит», которую вы используете в комментариях, все еще является странным способом выразить это. Промежуточные форматы, в которых вы можете проанализировать представление числа с плавающей запятой одинарной точности, прежде чем округлять его до одинарной точности, должны быть без потерь, иначе произойдет двойное округление. Двойное округление может быть более или менее сложным для отображения в зависимости от точности промежуточного формата с потерями, но использование 80-битных или 128-битных двоичных форматов с плавающей запятой не устранит проблему, просто сделает ее более тонкой. В простом алгоритме, который я рекомендую, промежуточный формат представляет собой дробь из двух целых чисел с многозначностью.

Я не вижу вопроса в этом вопросе 🙂

Предполагая, что вам нужен анализатор ocaml для «C float literals» — ответ таков — напишите его самостоятельно, это не очень сложно, и у вас будет строгий контроль над деталями реализации и тем, что на самом деле означает «C float literal».