Error for global symbolic variables are assigned 0

[Himeshi]

In the eval function, all global constants are given an error value of zero. This should be modified such that if the global variable is symbolic, it should be assigned a symbolic error value.

[domainexpert]

@Himeshi I believe the test case is basic/array_test2.c of fp-examples. Looking at the .ll file, there is a global declaration of @arr as follows:

@arr = common global [5 x i32] zeroinitializer, align 16

Here @arr is actually a pointer value, and it is not an input, so I think it should correctly have 0 as its error. However, it seems to me it is the content of @arr such as arr[0], arr[1], and arr[2] that need to have symbolic errors. Looking at array_test2.c this seems to be the expected situation. I think here what is needed is to make

klee_track_error(arr, "arr_error");

initializes the symbolic errors for every element of arr, which is the subject of #25 . Please let me know your thoughts.

[Himeshi]

@domainexpert From our previous discussion at the Friday meetings I thought that we were going keep the implementation of klee_track_error for arrays as it currently is and then add symbolic variables when the error array elements are accessed with getelementptr instruction.

This issue is actually for when a function call is made and the input arguments are binded to it. In this case I think that when the ptr for arr is passed into a function, it's associated error value should be arr_error and not 0, because arr is not just a global constant, but it is symbolic. Thoughts?

[domainexpert]

@Himeshi The approach with getelementptr may work, since (I think) one would always access array elements using getelementptr. One just needs to ensure that subsequent getelementptr with the same index would retrieve the same error expression. In summary, here we have two options:

1. Define the error expression for each element at getelementptr.
2. Define the error expression for each element at call to klee_track_error as I suggested. I have no strong opinion on both, please feel free to select your approach.

I believe we are discussing in the context of basic/array_test2.c of fp-examples. So, in regards to the question on arr_error, I guess first we need to clarify if arr_error:

1. Is the error of the global array pointer value?
2. Is the uniform error of each element of the array?
3. Is the prefix for arr_error0, arr_error1, arr_error2, and so on, which are are distinct errors for each element of the array?

Logically 1 should not be the case, since the global array pointer value should not have input-dependent error.

[Himeshi]

@domainexpert I believe it should be case 3. At the beginning of the program, we may assign the same error to all elements, but as the symbolic execution progresses we cannot assume that all array elements will have the same error and this eliminates case 2.

[domainexpert]

@Himeshi Excellent analysis. I agree.

[domainexpert]

@Himeshi Another way of doing it, given an array arr of fixed size, say 3, we could do:

klee_track_error(&(a[0]), "arr_0_error");
klee_track_error(&(a[1]), "arr_1_error");
klee_track_error(&(a[2]), "arr_2_error");

Just a thought.

[Himeshi]

I'm not sure if that would be a good approach @domainexpert. This function call would have to made for whichever the number of elements in the input array. In the jfdctint program alone it is 64. Also this would require special handling when the array is allocated dynamically.

[domainexpert]

@Himeshi Ok, I'm fine with the current approach.

[domainexpert]

Resolved via #28.