Разобрать длинный двойной из строки - PullRequest
2 голосов
/ 12 ноября 2011

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

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

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

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

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

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

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

Ответы [ 2 ]

2 голосов
/ 18 ноября 2011

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

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

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

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

0 голосов
/ 14 ноября 2011

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

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

...