How to understand the assignment semantic in lab?
- Dominant language
- OCaml
- Stars
- 15.7k
- Forks
- 2.1k
- Avg merge
- 19h 36m
- Merged PRs (30d)
- 13
Description
Please make sure your issue is not addressed in the [FAQ](https://fbinfer.com/docs/support#troubleshooting).
- The version of infer from `infer --version` is Infer version v1.1.0-9d9a3a42b.
- Your operating system and version is Linux DESKTOP-DOL0AJB 5.10.16.3-microsoft-standard-WSL
- The command I ran was `infer -g --resource-leak-lab-only -- javac LeaksAccessPaths.java`.
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](https://github.com/facebook/infer/blob/main/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml#L64):
```ocaml
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.
```java
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;`.
```txt
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.
Contributor guide
Assessment
This issue has not been assessed yet.