Случайная генерация C-программ с плавающей точкой - PullRequest
21 голосов
/ 11 декабря 2011

Кто-нибудь знает случайный генератор программ на C, которые включают вычисления с плавающей запятой?

Я ищу что-то, что будет немного похоже на Csmith , за исключением того, что Csmith не делаетгенерировать выражения с плавающей точкой, и что он генерирует тонны других конструкций, что делает его немного сложным для изменения.Генерация последовательных вычислений была бы хорошим началом для моей цели, если бы они включали некоторые вычисления с плавающей точкой.Условные обозначения были бы еще лучше, но мне не понадобились бы циклы, указатели или даже массивы.

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

РЕДАКТИРОВАТЬ: здесь приведен фрагмент сгенерированной Csmith программы, чтобы уточнить, чтоЯ ищу.

...
int64_t *l_374 = &g_189;
int32_t l_375 = (-1L);
int i, j, k;
l_375 &= ((g_106 == ((*l_374) = (&g_324[4] == l_373[0][0][5]))) < 0x80C8L);
return (*g_207);
...

Я также должен уточнить, что, принимая программу Csmith и заменяя, скажем, int64_t на float, можно получить синтаксически правильную программу на C, но это почти наверняка не дастопределенная программа.Я могу проверить, содержит ли замещенная программа неопределенное поведение, но это не дешево, и если мне придется отклонить 99% замещенных программ, потому что они неопределенные, процесс будет слишком медленным, чтобы быть полезным.

Ответы [ 2 ]

3 голосов
/ 22 декабря 2011

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

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

#include <stdio.h>
double x0 = 35945970.47e-83;
double x1 = (973e-37+(5626073.612783921311173024e-76*231.106261545926274055e1*66390306733994e-1*420514.99786508*654374994.1249111e-35*5201.6039804e56)+(2.93604195+33e-50)+(969222843.32046212043603+1734e01)+(0166605914e8+6701040019050623e-23+32591206968562.6e-11+90771798.753788905)+(328e-49/944642906580982081e7));

int main(){
  x0 = (((x1*534425399171e0)*(x1*x0*x0)*(x1*x0*57063248719.703555336277392e-36*x0*472e57*65189741246535e-1)*x1*(x1/22393742341e70)*(x1+x0+x0+x0))-((843193503867271987e3*61.949746266e23*x1*x1*x0)/(x1/x1)));
  x0 = ((x0+x1+x1+x1+x0)-(x0*506680.0005767722e66*396.650621163*70798334426455964.1*x1*305369e14));
  x1 = 660098705340e-21;
  printf("%a\n", x0);
}

Для этой программы gcc и clang (которые на этой платформе генерируют инструкции SSE2) генерируют исполняемые файлы, которые вычисляют одно и то же:

~/genfloat $ gcc t.c ; ./a.out 
0x1.5c5a77a63c1d6p+430
~/genfloat $ clang t.c ; ./a.out 
0x1.5c5a77a63c1d6p+430

Я также собираюсь протестировать статический анализатор, которыйдолжен предсказать все возможные результаты, которые могут быть получены с помощью программы, скомпилированной с инструкциями x87, непредсказуемым образом передавая некоторые промежуточные результаты в ячейки памяти с двойной точностью:

~/genfloat $ frama-c -val -float-hex -all-rounding-modes t.c 
...
      x0 ∈ [0x1.5c5a77a63c1cap430 .. 0x1.5c5a77a63c1e8p430]

Приведенное выше убедительное утверждение требуетбыть проверенным.

1 голос
/ 06 октября 2012

Моя manydl.c программа делает нечто очень похожее (на целые числа). Вы можете легко адаптировать его к вашим потребностям.

Я написал это как крошечный хак, чтобы убедить некоторых людей, в частности Жака Питра , в том, что система Linux может dlopen очень большое количество (более ста тысяч) общих объектов, эта программа генерировать случайный C-код, сфокусированный на целых числах и компиляциях, а затем dlopen -s выполняет их много. Вы можете адаптировать его к потребностям с плавающей запятой. Я спроектировал manydl.c так, чтобы он генерировал случайные, но завершающие программы на Си, чтобы вы могли адаптировать его к плавающему (просто выберите операции, которые заканчиваются и дешевы, как я).

Спроси меня больше во время кофе

(так как мы близкие коллеги)

...