facebook / facebook/infer

How to understand the assignment semantic in lab?

Open
#1,658 0 comments 1 reaction 0 assignees View on GitHub
question
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.