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

strchr fix #4

Closed adrianherrera closed 4 years ago

adrianherrera commented 4 years ago

The second argument to strchr is an int, not a char. The original strchr wrapper was causing "incompatible sort" error messages in z3 because the LHS of the expression was 8 bits and the RHS was 32 bits when calling _sym_get_parameter_expression.

Now all types are the same, however I'm not 100% sure on the fix and what other affects this may have on the shadow memory. Nevertheless, the "incompatible sort" error has disappeared.

sebastianpoeplau commented 4 years ago

Good catch! I suppose my use cases never called strchr with a symbolic character...

Regarding the fix, I think we should convert the parameter's expression to 8 bits instead of creating 32-bit expressions for the rest. It may not be documented well, but shadow memory assumes an 8-bit expression for each byte in memory. (I'll add some documentation to the shadow iterators to make it clear.)

Do I have permission to push to your branch? Then I can take care of the change. Otherwise feel free to do it yourself - it should be a simple matter of wrapping the parameter's expression in a call to _sym_build_trunc.

adrianherrera commented 4 years ago

Ok cool, thanks, I was not aware of this requirement.

Please modify my branch as required.

On Mon, 29 Jun 2020 at 9:40 pm, Sebastian Poeplau notifications@github.com wrote:

Good catch! I suppose my use cases never called strchr with a symbolic character...

Regarding the fix, I think we should convert the parameter's expression to 8 bits instead of creating 32-bit expressions for the rest. It may not be documented well, but shadow memory assumes an 8-bit expression for each byte in memory. (I'll add some documentation to the shadow iterators to make it clear.)

Do I have permission to push to your branch? Then I can take care of the change. Otherwise feel free to do it yourself - it should be a simple matter of wrapping the parameter's expression in a call to _sym_build_trunc.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/eurecom-s3/symcc/pull/4#issuecomment-651059275, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACB2DEUJ2FVGGCVOUZBVZR3RZB4RPANCNFSM4OIH2BDQ .