search

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
771 stars 137 forks source link

test: fix tests #75

Closed adrianherrera closed 2 years ago

adrianherrera commented 2 years ago

Includes disabling -O2 optimization, because newer LLVM's insert inline assembly which loses symbolic constraints.

aurelf commented 2 years ago

Hi Adiran,

Thanks for the fix. I imagine this will have an important performance impact no? Also the tests fail for the simple backend, did you look into this? Did you check if there was a way to disable the insertion of inline instructions by the newer LLVM ?

adrianherrera commented 2 years ago

Hey @aurelf,

Yeah, I guess it will have a performance impact, but given that this is for the tests it shouldn't impact the performance of deployed code.

I did notice that one test still fails (pointers.c). I haven't dug too deeply into the reasons (yet), but the same test also fails in the master branch.

I have been looking into the inline assembly, and it seems to be due to the same reasons discussed in https://github.com/eurecom-s3/symcc/issues/29. Per this issue, one way to "make the tests work independently of endianness..." would just be to disable optimizations of the tests :) I'll let you decide if this is the most suitable approach.

adrianherrera commented 2 years ago

Hey @aurelf,

So I've rewritten this PR. After muuuuch digging, it turns out that ntohl is replaced with a byteswap macro when optimizations are enabled. Thus, we can just undef this macro if it is defined (ensuring that the actual ntohl function is symbolized).

adrianherrera commented 2 years ago

Actually, I'm going to close this PR because I have a better approach; one that doesn't rely on a hack to the test source :)