Skip to content

Experiment with path- and context-sensitivity for memLeak analysis#1234

Merged
michael-schwarz merged 4 commits intomasterfrom
path_sens_memleak
Nov 9, 2023
Merged

Experiment with path- and context-sensitivity for memLeak analysis#1234
michael-schwarz merged 4 commits intomasterfrom
path_sens_memleak

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented Nov 3, 2023 •
edited
Loading

I'll use this issue to document some of the steps towards coming up with a good config for sv-comp.

Machine Config 
parallel runs:           40
resource limits:
- memory:                3000.0 MB
- time:                  1800 s
- cpu cores:             1
hardware requirements:
- cpu cores:             1
- memory:                3000.0 MB
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    goblint2
os:                      Linux-5.15.0-84-generic-x86_64-with-glibc2.29
cpu:                     Intel Xeon Platinum 8260 CPU @ 2.40GHz
- cores:                 96
- max frequency:         3900.0 MHz
- turbo boost enabled:   True
ram:                     540649.373696 MB
------------------------------------------------------------

Results without any additional path- & context-sensitivity:

Statistics:           3862 Files
  correct:            1082
    correct true:     1082
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:            2780
  Score:              2164 (max: 5857)

Results with full path- & context-sensitivity:

Statistics:           3862 Files
correct:            1104
  correct true:     1104
  correct false:       0
incorrect:             0
  incorrect true:      0
  incorrect false:     0
unknown:            2758
Score:              2208 (max: 5857)

Results with full path- & context-sensitivity & unique count of 5:

Statistics:           3862 Files
correct:            1131
  correct true:     1131
  correct false:       0
incorrect:             0
  incorrect true:      0
  incorrect false:     0
unknown:            2731
Score:              2262 (max: 5857)

Results with full path- & context-sensitivity & unique count of 5 & fix for #1235 :

Statistics:           3862 Files
  correct:            1158
    correct true:     1158
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:            2704
  Score:              2316 (max: 5857)

@michael-schwarz michael-schwarz added this to the SV-COMP 2024 milestone Nov 3, 2023
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Nov 3, 2023

When being fully path- & context-sensitive, we succeed on 22 additional tasks.

results.2023-11-03_13-56-44.table.zip

@michael-schwarz michael-schwarz added sv-comp SV-COMP (analyses, results), witnesses precision labels Nov 3, 2023
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Nov 6, 2023

We get strictly better with each of these config options, so it seems clear we would want them.

results.2023-11-06_10-15-02.zip

@michael-schwarz michael-schwarz mentioned this pull request Nov 6, 2023
Closed
@michael-schwarz michael-schwarz linked an issue Nov 6, 2023 that may be closed by this pull request
Enable a path-sensitive memory leak analysis in autoTune for small programs #1214
Closed
@michael-schwarz michael-schwarz marked this pull request as ready for review November 8, 2023 07:19
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Nov 8, 2023

To facilitate development and get accurate pre-runs, I'd propose merging this now, so we don't have multiple PRs floating around.

@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Nov 8, 2023

Quick question @sim642: I saw you specify svcomp24.json in the artifact. Is this a symlink to svcomp.json for now, or do I need to make these changes also in some other places?

@michael-schwarz michael-schwarz mentioned this pull request Nov 8, 2023
Merged
1 task
@sim642
Copy link
Copy Markdown
Member

sim642 commented Nov 8, 2023

Quick question @sim642: I saw you specify svcomp24.json in the artifact. Is this a symlink to svcomp.json for now, or do I need to make these changes also in some other places?

It's a config I copied and adapted on the svcomp24-dev branch before some of the PRs were merged.

This PR doesn't even change svcomp.json, so it shouldn't matter. Or should the path-sensitivity not be default but only in SV-COMP conf?

@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Nov 8, 2023

Ok, thanks! Are you merging master back into svcomp24-dev regularly then?

Or should the path-sensitivity not be default but only in SV-COMP conf?

No, I think it makes sense to have it path-sensitive by default.

@michael-schwarz michael-schwarz merged commit 03e17b6 into master Nov 9, 2023
@michael-schwarz michael-schwarz deleted the path_sens_memleak branch November 9, 2023 10:21
This was referenced Nov 21, 2023
Open
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 24, 2023
@sim642
[new release] goblint (2.3.0)
34ad5a7 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
@sim642 @nberth
[new release] goblint (2.3.0)
8f8e773 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 approved these changes

Assignees

No one assigned

Labels

precision sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Milestone

SV-COMP 2024

Development

Successfully merging this pull request may close these issues.

Enable a path-sensitive memory leak analysis in autoTune for small programs

2 participants

@michael-schwarz @sim642