2011-12-10 16 views
21

Có ai biết một trình tạo ngẫu nhiên các chương trình C bao gồm tính toán dấu phẩy động không?Tạo ngẫu nhiên các chương trình C với dấu phẩy động

Tôi đang tìm kiếm thứ gì đó giống như Csmith, ngoại trừ Csmith không tạo biểu thức dấu phẩy động và nó tạo ra rất nhiều cấu trúc khác, làm cho nó hơi khó sửa đổi. Tạo tính toán tuần tự sẽ là một khởi đầu tốt cho mục đích của tôi miễn là chúng bao gồm một số điểm nổi. Điều kiện sẽ tốt hơn, nhưng tôi sẽ không cần vòng lặp, con trỏ, hoặc thậm chí mảng.

Vì rất nhiều ngôn ngữ sử dụng cú pháp giống C, máy phát điện như vậy có thể không phải cụ thể cho C. Ngay cả khi nó cụ thể cho ngôn ngữ C khác, tôi có thể xử lý văn bản chương trình đã tạo ngôn ngữ đó vào một chương trình C.

EDIT: đây là đoạn trích của chương trình do Csmith tạo để làm rõ những gì tôi đang tìm kiếm.

... 
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); 
... 

Tôi cũng nên làm rõ rằng trong khi tham gia một chương trình Csmith và thay thế, chẳng hạn, int64_t với float có thể đưa ra một chương trình C đúng cú pháp, nó sẽ gần như chắc chắn không đưa ra một chương trình xác định. Tôi có thể kiểm tra xem một chương trình thay thế có chứa hành vi không xác định, nhưng điều này không phải là rẻ, và nếu tôi phải từ chối 99% các chương trình thay thế vì chúng không được xác định, quá trình sẽ quá chậm để có ích.

+1

Tôi hoàn toàn thiếu ngủ ngay bây giờ, vì vậy xin lỗi nếu điều này là ngu ngốc, nhưng tôi đang đọc quyền này? Bạn muốn tạo ngẫu nhiên các chương trình C? Xa ra! Tốt cho bạn! Tại sao? : P – TheIronKnuckle

+1

@TheIronKnuckle Đối với "thử nghiệm vi sai": biên dịch một chương trình * được định nghĩa ngẫu nhiên * C với hai trình biên dịch khác nhau và nếu chương trình cho kết quả khác nhau, bạn đã tìm thấy lỗi trong một trong các trình biên dịch. http://www.linux-mips.org/pub/linux/mips/people/macro/DEC/DTJ/DTJT08/DTJT08PF.PDF –

+1

@TheIronKnuckle Vâng, nó phức tạp hơn một chút với dấu phẩy động, vì nổi -point là underspecified trong C99, và hai trình biên dịch cả hai sẽ được chính xác và cho kết quả khác nhau trong sự hiện diện của dấu phẩy động. Đây là lý do tại sao tính năng này không được bao gồm trong Csmith. Nhưng tôi vẫn nghĩ rằng tôi có thể sử dụng các chương trình điểm nổi ngẫu nhiên cho mục đích của mình. –

Trả lời

3

Tôi đã bắt đầu trên floating-point fuzzer nhỏ. Nó bây giờ không có chút gì, nhưng bạn phải bắt đầu với một cái gì đó.

Dưới đây là một ví dụ về sử dụng để so sánh các trình biên dịch tạo hướng dẫn SSE2, mà tôi cho rằng không có lý do gì để tạo ra kết quả khác nhau:

#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); 
} 

Đối với chương trình này, gccclang (mà trên nền tảng này tạo hướng dẫn SSE2) tạo các tệp thực thi tính toán cùng một điều:

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

Tôi cũng dự định thử nghiệm một trình phân tích tĩnh được cho là dự đoán tất cả các kết quả có thể có được với chương trình biên soạn với các lệnh x87, làm tràn một số kết quả trung gian đến các địa điểm bộ nhớ tăng gấp đôi độ chính xác trong một thời trang không thể đoán trước:

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

Trên đây là một tuyên bố mạnh mẽ rằng cần phải được kiểm tra.

1

Chương trình manydl.c của tôi đang hoạt động tương tự (trên số nguyên). Bạn có thể điều chỉnh nó khá dễ dàng theo nhu cầu của bạn.

Tôi đã viết rằng như một hack nhỏ để thuyết phục một số người, đặc biệt là Jacques Pitrat, rằng một hệ thống Linux có thể dlopen một lô rất lớn (hơn trăm nghìn) đối tượng dùng chung, chương trình tạo ngẫu nhiên mã C-tập trung vào số nguyên - và biên dịch và dlopen -s rồi thực thi rất nhiều. Bạn có thể thích nghi nó với nhu cầu điểm nổi. Tôi thiết kế của tôi manydl.c để nó tạo ra ngẫu nhiên nhưng kết thúc chương trình C, vì vậy bạn có thể thích ứng với nó để nổi (chỉ cần chọn các hoạt động được chấm dứt và giá rẻ, như tôi đã làm).

Ask me nhiều lúc cà phê

(vì chúng tôi là đồng nghiệp đóng)

Các vấn đề liên quan