eurecom-s3 / symcc

SymCC: efficient compiler-based symbolic execution
http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
GNU General Public License v3.0
781 stars 137 forks source link

compiler: add supporting passes #76

Closed adrianherrera closed 1 year ago

adrianherrera commented 3 years ago

The PR introduces a number of LLVM passes into the symbolize process.

The ExpandAsm pass exploits LLVM's target lowering and its ability to expand inline assembly into explicit LLVM code.

Importantly, this expansion includes lifting bswap instructions to the bswap intrinsic, which can be symbolized with symcc. This fixes issue #29 and does away with the hacks made in PR #75 (in an attempt to get the tests to pass).

We also run the LLVM scalarizer and loweratomics passes. The former removes most vector instructions and the latter removes atomic instructions. These instructions are currently unsupported by symcc.

aurelf commented 2 years ago

Hi @adrianherrera, thanks for the PR! Sorry for the late answer to it... Could you :

sebastianpoeplau commented 1 year ago

@adrianherrera sorry for getting back to this so terribly late. We haven't had a lot of resources to work on SymCC, so I'm only now finding time to go through the open pull requests...

I really like the idea of adding LLVM passes that support SymCC! The first commit, adding the scalarizer and atomics lowering, should be no problem to add; I will cherry-pick it and merge immediately if the tests pass. The second commit, lifting inline assembly, makes a lot of sense too, but I'm a bit worried that it's a lot of code for a small feature: pass registration is really noisy (not your fault at all, it's what LLVM does), lifting is only supported for x86 and ARM, and it only handles byte swapping. If you don't mind, I'll change the code a bit:

aurelf commented 1 year ago

Hi, that's interesting, thanks both for the work on the features. I really like the lifter feature, however, it seem to work for simple inline assembly, are there any drawbacks to it ? If so shall we make this optional provide a warning about it?

sebastianpoeplau commented 1 year ago

I really like the lifter feature, however, it seem to work for simple inline assembly, are there any drawbacks to it ? If so shall we make this optional provide a warning about it?

I don't see any drawbacks :thinking: It won't work all the time, but when it works the result is better than what we had before.

aurelf commented 1 year ago

I really like the lifter feature, however, it seem to work for simple inline assembly, are there any drawbacks to it ? If so shall we make this optional provide a warning about it?

I don't see any drawbacks thinking It won't work all the time, but when it works the result is better than what we had before.

OK, great thanks !

adrianherrera commented 1 year ago

Awesome, thanks for fixing the PR! Recently we have been working with Trail of Bits and their Remvill/Anvill lifting tools to lift more complicated inline assembly code constructs. Hopefully, we'll soon be able to share this if you're interested.

sebastianpoeplau commented 1 year ago

Sounds very nice! :blush: I'm definitely interested.