facebook / infer

A static analyzer for Java, C, C++, and Objective-C
http://fbinfer.com/
MIT License
14.89k stars 2.01k forks source link

How to understand the assignment semantic in lab? #1658

Open Butter934 opened 2 years ago

Butter934 commented 2 years ago

Please make sure your issue is not addressed in the FAQ.

Thank you for making such a powerful tool!

I'm new to Infer and trying to learn Infer by the lab. But I can't understand the handling of assignment statements:

let assign lhs_access_path rhs_access_path held =
  let one_binding access_path count held =
    match
      AccessPath.replace_prefix ~prefix:rhs_access_path ~replace_with:access_path lhs_access_path
    with
    | Some base_access_path ->
        ResourcesHeld.add base_access_path count held
    | None ->
        ResourcesHeld.add access_path count held
  in
  ResourcesHeld.fold one_binding held ResourcesHeld.empty

Why replace every key of the abstract state while lhs_access_path contain rhs_access_path as a prefix? This confused me a lot and cause false negative. Here's my LeaksAccessPaths.java for test.

package codetoanalyze.java.checkers;

import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;

class ClassA{
    public FileInputStream field;
    public ClassA field2;

    ClassA(FileInputStream stream, ClassA x){
    this.field = stream;
    this.field2 = x;
    }
}

public class LeaksAccessPaths {
    void test(ClassA a)throws IOException, FileNotFoundException {
    FileInputStream stream1 = new FileInputStream("file1.txt");
    FileInputStream stream2 = new FileInputStream("file1.txt");
    FileInputStream stream3 = new FileInputStream("file1.txt"); 
    a.field2.field2 = a.field2;
    stream1.close();
    stream2.close();
    stream3.close();
    }
}

I ran infer -g --resource-leak-lab-only -- javac LeaksAccessPaths.java, here's the analyzing result of a.field2.field2 = a.field2;.

PRE STATE:
{ n$0 -> 1, n$3 -> 1, n$6 -> 1 }

INSTR=  a->field2->field2 := a->field2 [line 30]; 

STATE:
{ n$0.field2 -> 1, n$3.field2 -> 1, n$6.field2 -> 1 }

INSTR=  NULLIFY(&a); [line 30]; 

STATE UNCHANGED

INSTR=  EXIT_SCOPE(a); [line 30]; 

STATE:
{ n$0.field2 -> 1, n$3.field2 -> 1, n$6.field2 -> 1 }

and we can see that every key in the map are replaced by something, even the key wasn't mentioned in the statement at all. I would very appreciate it if anyone could help.