Add special function handler to print error expression

[Himeshi]

Add the special function handler "klee_print_error_expr" to print the error expression of a symbolic variable.

[domainexpert]

@Himeshi Would you please send me / paste here the example code for which you want this API to work?

[Himeshi]

@domainexpert An example program is attached. add_test.pdf

[domainexpert]

@Himeshi One is supposed to be able to obtain the same information via the already-implemented klee_bound_error interface, where the error expression will be stored in klee-out/test000001.precision_error, but in the current version, there seems to be a bug such that 0 is stored as the error expression. I think it may be best to resolve this bug instead.

[domainexpert]

@Himeshi If you agree this is to be handled as a bug of klee_bound_error, then we need to open an issue.

[Himeshi]

@domainexpert what is the functionality of klee_bound_error? If it was to obtain the error expression for a variable then it certainly can be moved to it. However right now klee_bound_error doesn't print the error expression for the output. This is probably because it considers the last instruction to obtain the error expression and the last instruction may not be something that has to do with the output of the program. For the attached program it doesn't produce anything because the last instruction (before the ret) is %10 = sext i32 %9 to i64, !dbg !136. add_test.pdf

It would also be good to have a mechanism to obtain the error expression of intermediary variables for future work. But I'll leave it to you decide if we should consolidate these functionalities into klee_bound_error.

[domainexpert]

@Himeshi So here you are mentioning there are two issues:

1. klee_bound_error() does not print the error expression for the output.
2. There is a need to obtain the error expression of intermediary variables.

Actually, klee_bound_error() allows you to specify the variable that you want to output the error expression of, either it is a variable in the middle of the execution, or a variable at the end of an execution. So, it has been implemented to cover both features.

I have also noticed you put header comments in the C file to record how you ran it. You can actually simply copy the example into basic directory of fp-examples and, modify KLEE_HOME in basic/Makefile, and simply run:

make add_test.klee

So, to answer No. 1, I did that and I discovered that klee_bound_error() does output the error expression into the file I mentioned:

cat add_test.klee/test000001.precision_error 
Line 22 of /home/dcsandr/software/fp-examples/basic/add_test.c (main): __error__22505728 == (0) && (__error__22505728 <= 1.300000e+00) && (__error__22505728 >= -1.300000e+00)

However, here, the error expression (0) is not what you might have expected, and this is the part that needs fixing.

To answer your question No. 2, you can try to run mat_mul.c again in the basic folder of fp-analysis. After setting up the appropriate value for KLEE_HOME in basic/Makefile, please do the following:

make mat_mul.klee

As you can see, the klee_bound_error() call in mat_mul.c is not located at the end of the program, but instead it is located within a loop body! Let's take a look at the output error expressions:

cat mat_mul.klee/test000001.precision_error 

Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15901568 == (((((((aError0 + bError0) * 999285817) / 3879440356) * 3879440356) + ((aError1 + bError1) * 999285817)) / 583758877)) && (__error__15901568 <= 1.000000e-02) && (__error__15901568 >= -1.000000e-02)

------------------------
Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15904752 == (((((((aError0 + bError0_1) * 999285817) / 3879440356) * 3879440356) + ((aError1 + bError1_1) * 999285817)) / 583758877)) && (__error__15904752 <= 1.000000e-02) && (__error__15904752 >= -1.000000e-02)

------------------------
Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15907872 == (((((((aError0 + bError0_2) * 999285817) / 3879440356) * 3879440356) + ((aError1 + bError1_2) * 999285817)) / 583758877)) && (__error__15907872 <= 1.000000e-02) && (__error__15907872 >= -1.000000e-02)

------------------------
Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15911584 == (((((((aError0_1 + bError0_3) * 999285817) / 3879440356) * 3879440356) + ((aError1_1 + bError1_3) * 999285817)) / 583758877)) && (__error__15911584 <= 1.000000e-02) && (__error__15911584 >= -1.000000e-02)

------------------------
Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15912208 == (((((((aError0_1 + bError0_4) * 999285817) / 3879440356) * 3879440356) + ((aError1_1 + bError1_4) * 999285817)) / 583758877)) && (__error__15912208 <= 1.000000e-02) && (__error__15912208 >= -1.000000e-02)

------------------------
Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15923072 == (((((((aError0_1 + bError0_5) * 999285817) / 3879440356) * 3879440356) + ((aError1_1 + bError1_5) * 999285817)) / 583758877)) && (__error__15923072 <= 1.000000e-02) && (__error__15923072 >= -1.000000e-02)

------------------------
Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15926080 == (((((((aError0_2 + bError0_6) * 999285817) / 3879440356) * 3879440356) + ((aError1_2 + bError1_6) * 999285817)) / 583758877)) && (__error__15926080 <= 1.000000e-02) && (__error__15926080 >= -1.000000e-02)

------------------------
Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15927968 == (((((((aError0_2 + bError0_7) * 999285817) / 3879440356) * 3879440356) + ((aError1_2 + bError1_7) * 999285817)) / 583758877)) && (__error__15927968 <= 1.000000e-02) && (__error__15927968 >= -1.000000e-02)

------------------------
Line 25 of /home/dcsandr/software/fp-examples/basic/mat_mul.c (main): __error__15913792 == (((((((aError0_2 + bError0_8) * 999285817) / 3879440356) * 3879440356) + ((aError1_2 + bError1_8) * 999285817)) / 583758877)) && (__error__15913792 <= 1.000000e-02) && (__error__15913792 >= -1.000000e-02)

As you can see, the error expression at each iteration gets printed. I believe this not only answer your question No. 2, but it also demonstrates that klee_bound_error() does not print only the last error expression, but the error expressions of all the visitation of klee_bound_error() along the path.

I hope the above sheds light on the status of the current implementation.

[domainexpert]

@Himeshi Thank you so much for the hard work. Thanks to you, we have identified issues with the implementation, particularly #26. Closing this PR now.