WALA icon indicating copy to clipboard operation
WALA copied to clipboard
verified publisher icon wala

Program Slicing Fails to Identify Unreachable Dead Code with Logical Contradictions

Open bystc opened this issue 2 months ago • 2 comments

Summary

WALA's program slicing tool fails to detect and filter out dead code when the unreachability depends on logical reasoning (e.g., if (a < 0 && a > 100)). This causes the slicer to incorrectly select seed statements from unreachable code paths, producing incorrect slice results.

Expected Behavior

When slicing code containing a logically contradictory condition (e.g., if (a < 0 && a > 100)), the slicer should:

  1. Recognize that the condition is always false through constant propagation and range analysis
  2. Mark the entire if-block as unreachable dead code
  3. Exclude unreachable code from seed statement candidates
  4. When using a method name (e.g., println) as the seed, prefer reachable statements over unreachable ones

Actual Behavior

The slicer:

  1. Does NOT detect the logical contradiction in the condition
  2. Treats the unreachable code as normal code
  3. Selects a println statement from the dead code block as the seed (line 25 instead of line 40)
  4. Produces an incorrect slice containing dead code that will never execute

Steps to Reproduce

1. Test Code

package com.ibm.wala.examples.metamorphic;

public class MT3_DeadCode_AlwaysFalseCondition {
    
    public static void main(String[] args) {
        // Input variables
        int x = args.length > 0 ? Integer.parseInt(args[0]) : 10;
        int y = 20;
        
        // Computation
        int a = x + y;
        int b = compute(x);
        
        // === DEAD CODE: Always-false condition ===
        if (a < 0 && a > 100) {  // Logically impossible: a cannot be both <0 AND >100
            // This code will NEVER execute
            a = a * 1000;
            b = b * 1000;
            int result = a + b;
            System.out.println("Dead: " + result);  
        }
        // === End of dead code ===
        
        // Conditional branch
        if (a > 15) {
            b = b * 2;
        } else {
            b = b + 5;
        }
        
        // Target variable
        int result = a + b;
        
        // Slice seed point - THIS is where we want to slice from
        System.out.println(result);  // Line 40 - INTENDED SEED POINT
        
        // Subsequent unrelated code
        int z = 100;
        int w = z * 2;
    }
    
    private static int compute(int input) {
        int temp = input * 3;
        if (temp > 20) {
            temp = temp - 5;
        }
        return temp;
    }
}

2. Run Slicing

gradle run \
  -PmainClass="com.ibm.wala.examples.drivers.SlicingDriver" \
  --args="-appJar build/libs/myapp.jar \
          -mainClass Lcom/ibm/wala/examples/metamorphic/MT3_DeadCode_AlwaysFalseCondition \
          -targetMethod println \
          -applicationOnly true"

3. Observe Results

> Task :processResources NO-SOURCE
> Task :classes

> Task :run
Analyzing: build/libs/WALA-start-master-0.1.jar
Restricting to entrypoint: Lcom/ibm/wala/examples/metamorphic/MT3_DeadCode_AlwaysFalseCondition
Slice configuration -> data: NO_HEAP, control: FULL
Seed statement: com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: invokevirtual < Application, Ljava/io/PrintStream, println(Ljava/lang/String;)V > 19,21 @70 exception:22 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:25 -> System.out.println("Dead: " + result); (applicationOnly)

Backward slice (size=30, applicationOnly):
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 3 = arraylength 1 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:12 -> int x = args.length > 0 ? Integer.parseInt(args[0]) : 10;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: conditional branch(le, to iindex=9) 3,4 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:12 -> int x = args.length > 0 ? Integer.parseInt(args[0]) : 10;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 6 = arrayload 1[4] @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:12 -> int x = args.length > 0 ? Integer.parseInt(args[0]) : 10;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 8 = invokestatic < Application, Ljava/lang/Integer, parseInt(Ljava/lang/String;)I > 6 @8 exception:7 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:12 -> int x = args.length > 0 ? Integer.parseInt(args[0]) : 10;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: PARAM_CALLER
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: NORMAL_RET_CALLER
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 11 = binaryop(add) 9 , 10 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:16 -> int a = x + y;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 13 = invokestatic < Application, Lcom/ibm/wala/examples/metamorphic/MT3_DeadCode_AlwaysFalseCondition, compute(I)I > 9 @25 exception:12 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:17 -> int b = compute(x);
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: PARAM_CALLER
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: NORMAL_RET_CALLER
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: conditional branch(ge, to iindex=42) 11,4 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:20 -> if (a < 0 && a > 100) { 
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: conditional branch(le, to iindex=42) 11,14 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:20 -> if (a < 0 && a > 100) { 
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 16 = binaryop(mul) 11 , 15 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:22 -> a = a * 1000;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 17 = binaryop(mul) 13 , 15 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:23 -> b = b * 1000;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 18 = binaryop(add) 16 , 17 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:24 -> int result = a + b;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 19 = getstatic < Application, Ljava/lang/System, out, <Application,Ljava/io/PrintStream> > @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:25 -> System.out.println("Dead: " + result);
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: [invokedynamic] 21 = invokestatic < Application, Ljava/lang/invoke/StringConcatFactory, makeConcatWithConstants(I)Ljava/lang/String; > 18 @65 exception:20 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:25 -> System.out.println("Dead: " + result);
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: NORMAL_RET_CALLER
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: invokevirtual < Application, Ljava/io/PrintStream, println(Ljava/lang/String;)V > 19,21 @70 exception:22 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:25 -> System.out.println("Dead: " + result);
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: PHI
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: PARAM_CALLEE
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: METHOD_ENTRY
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.compute(I)I :: 4 = binaryop(mul) 1 , 3 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:48 -> int temp = input * 3;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.compute(I)I :: conditional branch(le, to iindex=11) 4,5 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:49 -> if (temp > 20) {
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.compute(I)I :: 7 = binaryop(sub) 4 , 6 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:50 -> temp = temp - 5;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.compute(I)I :: return 8 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:52 -> return temp;
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.compute(I)I :: PHI
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.compute(I)I :: PARAM_CALLEE
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.compute(I)I :: NORMAL_RET_CALLEE
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.compute(I)I :: METHOD_ENTRY

Forward slice (size=3, applicationOnly):
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: invokevirtual < Application, Ljava/io/PrintStream, println(Ljava/lang/String;)V > 19,21 @70 exception:22 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:25 -> System.out.println("Dead: " + result);
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: EXC_RET_CALLER
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: EXC_RET_CALLEE

Backward thin slice (size=3, applicationOnly):
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: 19 = getstatic < Application, Ljava/lang/System, out, <Application,Ljava/io/PrintStream> > @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:25 -> System.out.println("Dead: " + result);
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: NORMAL_RET_CALLER
  com.ibm.wala.examples.metamorphic.MT3_DeadCode_AlwaysFalseCondition.main([Ljava/lang/String;)V :: invokevirtual < Application, Ljava/io/PrintStream, println(Ljava/lang/String;)V > 19,21 @70 exception:22 @ src\main\java\com\ibm\wala\examples\metamorphic\MT3_DeadCode_AlwaysFalseCondition.java:25 -> System.out.println("Dead: " + result);

WRONG: Selected line 25 (dead code) instead of line 40 (intended seed)

Backward slice includes dead code:

  • Line 20: if (a < 0 && a > 100) {
  • Line 22: a = a * 1000;
  • Line 23: b = b * 1000;
  • Line 24: int result = a + b;
  • Line 25: System.out.println("Dead: " + result);

Comparison with Baseline

Baseline Code: OriginalTest.java (identical except without the dead code block)

public class OriginalTest {
    public static void main(String[] args) {
        int x = args.length > 0 ? Integer.parseInt(args[0]) : 10;
        int y = 20;
        int a = x + y;
        int b = compute(x);
        
        // NO dead code here
        
        if (a > 15) {
            b = b * 2;
        } else {
            b = b + 5;
        }
        
        int result = a + b;
        System.out.println(result);  // Line 29 - SEED POINT
        
        int z = 100;
        int w = z * 2;
    }
    
    private static int compute(int input) {
        int temp = input * 3;
        if (temp > 20) {
            temp = temp - 5;
        }
        return temp;
    }
}

Expected: Since the dead code in MT3 is unreachable, the slicing results for both programs should be identical (they are semantically equivalent).

Actual: The slices are completely different because MT3 incorrectly slices from the dead code.

Attached is the code for calling Wala's slicing function. SlicingDriver.java

Would you like me to submit a PR to fix this issue? I'm willing to contribute if there's guidance on the preferred implementation approach.

bystc avatar Oct 30 '25 08:10 bystc

Thanks for the report @bystc. As you've observed WALA's slicer does not detect the contradiction in your example and eliminate dead code. I feel for cases like this, one might want a separate pass to trim out or mark dead code before running the slicer; I don't recall slicing algorithms that bake in such reasoning. If you're interested in implementing such a dead code detection analysis, and then having a way to pass the results to the slicer, I'd be opening to reviewing a PR and advising on it.

As to the slicer choosing the wrong seed, could you map back to source-level line numbers to ensure you get the desired seed for your use case?

msridhar avatar Oct 30 '25 15:10 msridhar

hi @msridhar Thanks for your reply and suggestions! As a beginner in program slicing, I agree with your thoughts on dead code detection. Currently, I mainly hope to explore more slicing-related scenarios to build up my understanding of the tool. If I encounter other questions or discover new scenarios in the future, I might need to consult you again—thank you very much for being willing to help! Regarding the seed issue, I’ll try mapping back to source-level line numbers to confirm as you suggested. Thanks for the guidance!

bystc avatar Nov 01 '25 08:11 bystc