Skip to content

Add transformation to instrument a program with asserts & Produce invariants from Apron#157

Merged
michael-schwarz merged 95 commits intomasterfrom
instrument_with_asserts
Apr 1, 2022
Merged

Add transformation to instrument a program with asserts & Produce invariants from Apron#157
michael-schwarz merged 95 commits intomasterfrom
instrument_with_asserts

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented Dec 17, 2020 •
edited
Loading

Instrument a given program with asserts based on the analysis results. Enable with --sets trans.activated[+] assert. Writes the instrumented file into the file specified in trans.output.

Limitations

  • Currently only works for local, top-level variables (i.e. not arrays, structures, ...) of integer type
  • Asserts all local variables after join, ideally one would like to only modify ones that were modified in one of the branches
  • Removes comments from files, if the input program has //UNKNOWN annotations, this will remove them, and they will fail when running Goblint again.

Use Cases

  • To compare precision between runs and/or configurations
  • Theoretically, one could take arbitrary programs (without UB), annotate them, compile and execute. If any of the asserts is violated, this is an unsoundness in Goblint.

This is based on @Fayanzar work submitted for his Master's thesis (extracted from #150)

Fayanzar and others added 24 commits July 31, 2020 09:04
@Fayanzar
Initial IntervalSet implementation.
1020948
@Fayanzar
Fixed addition and added some most essential comments.
c826d50
@Fayanzar
Finally done the IntervalSet domain.
37f0cbb
@Fayanzar
Finally done the IntervalSet domain.
4a4f612
@Fayanzar
Merge branch 'interval_set' of https://github.com/Fayanzar/analyzer i…
fb542a5 
…nto interval_set
@Fayanzar
Initial IntervalSet implementation.
ff18b08
@Fayanzar
Fixed addition and added some most essential comments.
1ceeb58
@Fayanzar
Finally done the IntervalSet domain.
b5fc6e4
@Fayanzar
Some basic stuff with adding assertions after assignments.
aed5615
@Fayanzar
IntervalSet + assert transformation.
dad6f85 
TODO:
- solve looping issue with IntervalSet
- assert memory writes
- remove lots of CIL-created scopes
- do something about asserting the last assignment of the scope
- handle global references
@Fayanzar
Merge branch 'interval_set' of https://github.com/Fayanzar/analyzer i…
724d9cf 
…nto interval_set
@michael-schwarz
intDomain from master
1219f39
@michael-schwarz
Merge branch 'master' into instrument_with_asserts
c2d3d57
@michael-schwarz
Make compile
3bad570
@michael-schwarz
Remove interval set
3f260d3
@michael-schwarz
Remove unused getAllInfo query
b121d88
@michael-schwarz
Cleanup
c5ebdf0
@michael-schwarz
More cleanup
d525581
@michael-schwarz
Cleanup
e5ed366
@michael-schwarz
Cleanup
4d29fc2
@michael-schwarz
Cleanup
03a2228
@michael-schwarz
Add comment
f2e92a4
@michael-schwarz
Merge remote-tracking branch 'origin/master' into instrument_with_ass…
25ebdc8 
…erts
@michael-schwarz
Gitignore: Output folder of assert transformation
eef4aab
@michael-schwarz michael-schwarz mentioned this pull request Dec 17, 2020
Closed
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Dec 21, 2020 •
edited
Loading

Things that remain TODO:

  • Assertions about globals as well
  • Assertions with some offset (not just Cil.NoOffset)
  • Assertions in pieces of code that are unreachable

@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Jan 7, 2021

Possible improvement: Reduce the number of assert(0) inserted into unreachable code.

@michael-schwarz
Recurse for top-level LOr in pullOutCommonConjuncts
01eb533
@michael-schwarz
Simplify combine_conjuncts
3f80db6
@michael-schwarz
Cleanup invariant query
0af69af
@michael-schwarz
Pull out to be consistent with inverse conversions
71de492
@michael-schwarz
Comment waht exactly is Not_found in make_assert
ad28690
@michael-schwarz
Pull Invariant query handling into control
b9f8c92
@michael-schwarz
Change return type of Invariant query
0cb270b
@michael-schwarz
Use specific exception for failed conversions
1e5012d
@michael-schwarz
Asserts: use fresh functions everytime, since we just print the resul…
873c52b 
…ts, it does not matter
@michael-schwarz
More sensible to_cil_varinfo
1c34756
@michael-schwarz
No more mess
2b419b2
@michael-schwarz
Do conversion via linexpr1
e3c1089
@michael-schwarz
Rounding
f0e7aba
@michael-schwarz
Attempt to negate constants to get asserts containing -k*v instead of…
291c2fa 
… +(-k)*v
@michael-schwarz
Add possibility to filter one variable constraints based on Lincons0
d2b5142
@michael-schwarz
Rm unused function
7d7ecbd
@michael-schwarz
Make explicit what is caught
46d76e3
@michael-schwarz michael-schwarz requested a review from sim642 March 31, 2022 07:07
sim642
sim642 reviewed Mar 31, 2022
View reviewed changes
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Apr 1, 2022

I tested with octMPQ, it is still significantly slower than octD (10.075 s vs 3.299 s) and finds the same invariants on the programs I tested with, so octD still seems like the better choice.
(Side remark: I had some trouble getting it to compile with octMPQ, it would not find apron.octMPQ. For some reason opam reinstall apron fixed the issue.)

@michael-schwarz michael-schwarz requested a review from sim642 April 1, 2022 07:46
@michael-schwarz michael-schwarz merged commit e754868 into master Apr 1, 2022
@michael-schwarz michael-schwarz deleted the instrument_with_asserts branch April 1, 2022 09:04
@michael-schwarz michael-schwarz mentioned this pull request May 22, 2022
Closed
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
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

student-job testing

Projects

None yet

Milestone

v2.0.0

Development

Successfully merging this pull request may close these issues.

4 participants

@michael-schwarz @sim642 @vesalvojdani @Fayanzar