Closed tiedaoxiaotubie closed 3 years ago
My question is: since we can not implement symbolic wrapper for all of the functions in libc manually, what will happen if we meet
strlen
during the symbolic execution? I think SymCC won't instrument strlen with symbolic code, so we will lost the constraints inside the strlen.
That's correct: SymCC won't know how the return value of strlen
was obtained, and it will therefore treat it as a concrete value.
Not sure whether my understanding is right, what's other side effect (if any) for the libc functions that don't have symbolic wrapper?
In most cases, there are no negative consequences beyond SymCC losing track of symbolic constraints. One exception from this rule is when a libc function changes memory: if the modified memory cell contained symbolic data before the function call, then SymCC won't know that its symbolic expression doesn't correctly describe the new value, which can lead to incorrect (and likely conflicting) path constraints. In such cases, it makes sense to add wrappers for the offending function(s); see https://github.com/eurecom-s3/symcc/issues/23#issuecomment-696656932 for suggestions how to do so.
Closing as duplicate of #23
Hi, I noticed that there are only
26
symbolic wrapper for libc functions, but there are still many libc functions that also need to provide the symbolic wrapper, for example, thestrlen()
.My question is: since we can not implement symbolic wrapper for all of the functions in libc manually, what will happen if we meet
strlen
during the symbolic execution? I think SymCC won't instrument strlen with symbolic code, so we will lost the constraints inside the strlen.Not sure whether my understanding is right, what's other side effect (if any) for the libc functions that don't have symbolic wrapper?