Closed ercoppa closed 1 year ago
So we're actually lying in that comment in visitSelectInst
:stuck_out_tongue_winking_eye: I agree with your suggested fix. We could additionally check if the expressions for both values are null (i.e., the values are compile-time known, as in foo ? "yes" : "no"
) and skip the creation of the select in that case, which will prevent us from emitting code for subsequent use of the selected value. (It would be short-circuited at runtime, but code that we don't generate is even better than code that we jump over :wink: )
See PR #111
The current implementation of
visitSelectInst
is:The effect is that SymCC may (e.g., depending on the branch bitmap) generate an alternative input. However, the data flow is not propagated: the result of SelectInst would not be symbolic. Hence, the code is not reflecting the comment.
This can be seen in this example (inspired by real-world code):
where
r
will not be symbolic due to the bug. SymCC cannot solve the branch inmain
becauser
is concrete.A possible fix could be to add in the bottom of
visitSelectInst
something like:If this suggested fix is fine, then I can send a PR. Otherwise, let me know how you prefer to revise the fix.