pascal-lab / Tai-e-assignments

Tai-e assignments for static program analysis
https://tai-e.pascal-lab.net/
GNU Lesser General Public License v3.0
1.01k stars 234 forks source link

Question about A2 (ConstProp) - Shadowed by another constant or NAC ? #16

Open werifu opened 1 year ago

werifu commented 1 year ago

In the test case Assign, analyzing the following code in function Assign.assign():

    void assign() {
        int x = 1, y;
        x = 2;
        x = 3;
        x = 4;
        y = x;
    }

We can get respectively {x=1}, {x=2}, {x=3} and {x=4} , meaning that we still consider x as constant value instead of NAC while its value has been changed.

However, in the test case 'Loop', the following function leads to a failure on OJ:

    void whileNAC() {
        int a, b = 0, c = 0;
        int i = 0;
        while (i < 10) {
            a = b;
            b = c;
            c = 1;
            ++i;
        }
    }

the variable c is expected as NAC while my analyzer regards it as constant 1 in the while loop.

When should a variable become another constant, and when should it become NAC? It confused me a lot, need I do some dead code detection to it? But I think it's not the task of this assignment.

Trust04zh commented 1 year ago

Perhaps it would be easier to understand from the perspective of the variable's value (whether it is a constant) at a specific program point, rather than how it has been changed before this variable.

For the first example, when we focus on the program point after 2:x=3, the value of x can only be a constant 3 (although it was previously 1 or 2). Similarly, when we focus on the program point after 3:x=4, the value of x can only be a constant 4 (although previously ...).

assign()

In the second example, when we focus on the program point after 3:nop, the value of c can be obtained from different values of c from two program points (after 1:c=0 and after 10:c=1, with some statements in between, but these statements do not reassign c, so the value of c will be transfered unchanged), and we get the result of NAC for c by the meet operation. The result that the value of c is NAC will be transfered unchanged to the program point before 10:c=1. However, since the statement 10:c=1 assigns c to 1, the value of c after 10:c=1 is 1. Therefore, at some program points during the loop (but not all), the value of c is indeed 1.

whileNAC

These diagrams were generated using tai-e framework to produce the source code and then rendered using graphviz.