Profile cover photo
Profile photo
Iago Abal
Computer Engineer, Formal Methods Advocate, and Functional Programmer
Computer Engineer, Formal Methods Advocate, and Functional Programmer
About
Iago's posts

Our paper "Effective Bug Finding in C Programs with Shape-and-Effect Abstractions" that describes the ideas behind the #EBA bug finder, just got #accepted in #VMCAI 2017! Big #thanks to my co-authors for the good work! And thanks to the anonymous reviewers for their time and comments too.

Post has attachment
Finally, I have written a README.md for EBA so that others can give it a try. If you run into problems, please open an issue or let me know somehow.

At some point I should make a release and create an OPAM package...

Post has attachment
What is a #falsepositive for a #bugfinding tool? This post links to a patch removing a piece of dead code, but the source of this fix is a double-lock bug report by #EBA.

Ideally we want to analyze all the execution paths starting from the entry point of a program. But there are often way too many execution paths in a program, and that approach only works for quite small ones. To scale up we analyze functions locally, without regard to its calling context. So we find bugs like this one, that in practice never happen.

On the other hand, it was a ticking bomb, waiting for someone to use it in a different way and trigger the deadlock. I'm happy it got fixed, and I personally do consider it a bug. At usual, classifications are #fuzzy, there is a whole range from 100% bugs to 0% bugs.



Post has attachment
Jokes apart, it's kind of ridiculous to refer to highly-qualified people who work 40+ hours a week, and carry out most of the research as " #students ". Often it's just a way to justify low wages and lack of legal working rights. If a private company would put "students" to work full-time for a period of 3+ years, without a proper job contract, that would most definitely be illegal.

Post has attachment
A compilation of 26 historical (single thread) double lock #bugs in #Linux. #EBA finds 22 of those.

Post has attachment
Insightful comment according to Slashdot crowd:

"University professors are under constant pressure to come up with something interesting to show they are a world class expert in their field. And grad students who do most of the grunt work are under pressure to prove themselves as well. So this is yet another impractical technique."

Post has attachment
Nice tool for testing command line applications.

For instance, I'm starting to use tests like

  $ cp -r "$TESTDIR"/linux .

  $ eba -L linux/cmt_speech.i 2>/dev/null | grep -A 2 "Double lock"
  Double lock (*) (glob)
  first at drivers/hsi/clients/cmt_speech.c:443
  second at drivers/hsi/clients/cmt_speech.c:407

to check that my changes to #EBA don't make it miss any previously detected bug.

Post has attachment
Another double spin_lock fixed in a #Linux #driver thanks to #EBA!

Post has attachment
#EBA reported an spurious double-lock bug here, because from the context of `data_xfer' nothing indicates that `&acdev->host->lock' and `qc->ap->lock' are the same lock. Anyways, EBA still pointed out a situation that it's confusing for humans as well, and that deserved a cleanup patch.

Post has attachment
Second bug-fix submitted thanks to #EBA !
Wait while more posts are being loaded