How to compute Angelic values?

[ramsey-coding]

Could you please explain how the Angelic values were computed? Also, will the code be made available?

[norhh]

Angelic values are represented as the tuple (pp, t, x, v), where:

• pp is the program point. Examples include START for the start of the program and END, which is just before the return.
• t is a test.
• x is the variable.
• v is a value of the variable.

The program fails the test t under normal execution, but passes t when execution is altered by binding x to v at pp. Consider the example below, which fails for [-2, -3, -4] because max_value is set to 0 at the start:

def find_max_value(numbers):
    max_value = 0
    for num in numbers:
        if num > max_value:
            max_value = num
    return max_value

Consider the following modification at the program point END (all points before exiting the function):

def find_max_value(numbers):
    max_value = 0
    for num in numbers:
        if num > max_value:
            max_value = num
        max_value = -2  # Angelic value
    return max_value

For the function find_max_value, (END, max_value, {INPUT: [-2, -3, -4], OUTPUT: -2}, max_value, -2) is an angelic value. The angelic value for max_value at the END program point can be easily obtained by concolic execution by using the following modification:

def find_max_value(numbers):
    max_value = 0
    for num in numbers:
        if num > max_value:
            max_value = num
        max_value = <SYMBOL>
    return max_value

The above instrumented code can be executed using a symbolic execution engine on the test [-2, -3, -4]. Symbolic execution provides a path condition for satisfying the test, which in this case is = -2. Such equations can be solved using an SMT solver such as Z3 to obtain the angelic values at the END point

Angelic values were previously used in different applications such as Program Repair and Debugging. They obtained angelic values through symbolic execution on C which has a well maintained symbolic execution named KLEE.
Since the infrastructure for symbolic execution is not as advanced in Python as it is in C, we had to obtain the angelic values at the START and END program points by running it on patched code.

All the code used for executing and obtaining the results is available. The notebook that analyzes the data will soon be pushed

[ramsey-coding]

Thank you for your detailed response. While it might be feasible to derive angelic values by triggering functions in simpler unit functions, I'm curious about the practicality of implementing this approach across a full-scale project, especially considering the need for compilation. How realistic is this method in larger, more complex environments? What do you suggest to use for a Java project?

[norhh]

It should be feasible, for example, Angelix, which is program repair tool for C derives angelic values on large projects.
Java has a better environment for symbolic execution with multiple symbolic execution engines which support symbolic execution on large scale projects.

[ramsey-coding]

In the paper, you have mentioned Thus, we extracted angelic values from the correct versions of the programs via instrumentation. Do you share the instrumentation code in the artifact?

[norhh]

Hi @ramsey-coding, yes, it should be in the feature extractor, which is pyr_benchmark_wrangling library, available through pip and github.

[ramsey-coding]

I do not understand though, when you are fixing a bug how do you have access to the correct versions of the programs?

[norhh]

I do not understand though, when you are fixing a bug how do you have access to the correct versions of the programs?

Maniple is intended to study the utility of different facts. It is possible to extract angelic values, but Python does not have a robust symbolic execution engine to obtain these values. Hence, we used the fixed code to generate angelic values. Since this study focuses on the utility of different fact sets, there was no need to implement symbolic execution for Python to obtain angelic values, as using the correct version provides these values. A deployable APR tool (different from a study on fact sets such as maniple) that uses angelic values will need to obtain them through symbolic execution.