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
776 stars 135 forks source link

fseek fix #9

Closed borzacchiello closed 4 years ago

borzacchiello commented 4 years ago

Hi, It seems that the fseek function model has a bug. If the "offset" argument is symbolic and "whence == SEEK_SET", the function set the return expression to be equals to the expression in "offset", possibly causing "incompatible sort" error message further during execution, since fseek should return an int, and not a long. Now the functions always return a concrete value and concretizes the expression in offset.

Please review my commit, and let me know if I am wrong. Thanks, Luca

sebastianpoeplau commented 4 years ago

Hi @borzacchiello,

Thanks for the fix! I think I mistakenly assumed that fseek would return the current offset (like lseek). I agree that we shouldn't set the return value to the expression for offset, and adding the call to tryAlternative makes sense as well. The only concern I have is that we somehow need to set inputOffset (i.e., the global variable representing the current offset in the input file). Setting it to the result of the fseek call, as we currently do, is certainly wrong - maybe we should call ftell after successful fseek to get the current offset. Do you want to add it, or should I?

Cheers, Seb

borzacchiello commented 4 years ago

Ups, you're right. I just modified the commit as you suggested. Feel free to modify it if something is missing/wrong!

sebastianpoeplau commented 4 years ago

Perfect, thank you!