Fix #83: pass a clean 32-bit taken value to _sym_push_path_constraint#186
Open
Emad-Mahmodi wants to merge 1 commit into
Open
Fix #83: pass a clean 32-bit taken value to _sym_push_path_constraint#186Emad-Mahmodi wants to merge 1 commit into
Emad-Mahmodi wants to merge 1 commit into
Conversation
Emad-Mahmodi
added a commit
to Emad-Mahmodi/symcc
that referenced
this pull request
Jun 11, 2026
Several runtime functions whose C signature takes an int were declared to the compiler with a 1-bit integer (int1T) -- the same i1-vs-int mismatch as eurecom-s3#83. Affected: _sym_build_float (is_double), _sym_build_int_to_float (is_double, is_signed), _sym_build_float_to_float and _sym_build_bits_to_float (to_double). Declare these parameters as i32 and pass the flags as i32 at the call sites. The remaining i1 parameters correspond to C bool arguments, whose width already matches (clang lowers bool to i1) and where the callee observes only one bit, so they are unaffected. _sym_push_path_constraint is addressed separately in eurecom-s3#186. Behavior-preserving (identical diverging inputs on a float-heavy test).
…constraint The compiler declared the 'taken' parameter of _sym_push_path_constraint as i1, while the runtime defines it as a C int (i32). Conditions lowered via 'xor i1 %c, true' passed the raw i1 with dirty high bits (254/255) to the runtime, which tests 'if (taken)' and mis-handled a not-taken branch as taken, so SymCC failed to generate diverging inputs. Declare 'taken' as i32 and zero-extend the condition at all call sites (branch, select, switch, tryAlternative). Fixes both backends. Adds test/xor_taken.c.
Emad-Mahmodi
force-pushed
the
fix/issue-83-taken-zext
branch
from
0f3acd8 to
944cc84
Compare
Emad-Mahmodi
added a commit
to Emad-Mahmodi/symcc
that referenced
this pull request
Jun 20, 2026
Several runtime functions whose C signature takes an int were declared to the compiler with a 1-bit integer (int1T) -- the same i1-vs-int mismatch as eurecom-s3#83. Affected: _sym_build_float (is_double), _sym_build_int_to_float (is_double, is_signed), _sym_build_float_to_float and _sym_build_bits_to_float (to_double). Declare these parameters as i32 and pass the flags as i32 at the call sites. The remaining i1 parameters correspond to C bool arguments, whose width already matches (clang lowers bool to i1) and where the callee observes only one bit, so they are unaffected. _sym_push_path_constraint is addressed separately in eurecom-s3#186. Behavior-preserving (identical diverging inputs on a float-heavy test).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The compiler declared _sym_push_path_constraint's taken parameter as i1, while the runtime defines it as a C int (i32). Branch conditions produced via logical negation lower to xor i1 %c, true, and passing the raw i1 without zero-extension let uninitialized high bits (observed as 254/255) reach the runtime's if (taken) check, so a not-taken branch was treated as taken and SymCC kept generating the same path instead of a diverging one.
This declares taken as i32 and zero-extends the condition at all four call sites (branch, select, switch, tryAlternative). It fixes both the simple and qsym backends and addresses the root-cause type mismatch. Per @aurelf's request in the issue, test/xor_taken.c exercises the pattern on both backends.
Reproduction (the program reads g_2 then g_927; bytes 1–2 are g_927):
Before: generated input 00 00 00 -> g_927 = 0 (same path; bug)
After: generated input 00 ff 00 -> g_927 = 255 (diverging path; fixed)
ninja check passes on both backends (27/27).