From 944cc842fe3785dfe5733ee918d1e047d8646797 Mon Sep 17 00:00:00 2001 From: Emad-Mahmodi Date: Wed, 10 Jun 2026 09:31:23 +0330 Subject: [PATCH] Fix #83: pass a clean 32-bit taken value to _sym_push_path_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. --- compiler/Runtime.cpp | 4 ++-- compiler/Symbolizer.cpp | 18 ++++++++++++---- test/xor_taken.c | 47 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 63 insertions(+), 6 deletions(-) create mode 100644 test/xor_taken.c diff --git a/compiler/Runtime.cpp b/compiler/Runtime.cpp index 454819c7..0e384ced 100644 --- a/compiler/Runtime.cpp +++ b/compiler/Runtime.cpp @@ -72,8 +72,8 @@ Runtime::Runtime(Module &M) { buildConcat = import(M, "_sym_concat_helper", ptrT, ptrT, ptrT); // doesn't follow naming convention for historic reasons - pushPathConstraint = - import(M, "_sym_push_path_constraint", voidT, ptrT, int1T, intPtrType); + pushPathConstraint = import(M, "_sym_push_path_constraint", voidT, ptrT, + IRB.getInt32Ty(), intPtrType); // Overflow arithmetic buildAddOverflow = diff --git a/compiler/Symbolizer.cpp b/compiler/Symbolizer.cpp index fc9053ed..c5f5b91d 100644 --- a/compiler/Symbolizer.cpp +++ b/compiler/Symbolizer.cpp @@ -441,9 +441,13 @@ void Symbolizer::visitSelectInst(SelectInst &I) { // expression over from the chosen argument. IRBuilder<> IRB(&I); + // Zero-extend the i1 condition to a 32-bit value matching the runtime's + // `int taken` parameter, so that no uninitialized high bits of the i1 + // register can reach the runtime (see issue #83). + auto *taken = IRB.CreateZExt(I.getCondition(), IRB.getInt32Ty()); auto runtimeCall = buildRuntimeCall(IRB, runtime.pushPathConstraint, {{I.getCondition(), true}, - {I.getCondition(), false}, + {taken, false}, {getTargetPreferredInt(&I), false}}); registerSymbolicComputation(runtimeCall); if (getSymbolicExpression(I.getTrueValue()) || @@ -491,9 +495,13 @@ void Symbolizer::visitBranchInst(BranchInst &I) { return; IRBuilder<> IRB(&I); + // Zero-extend the i1 condition to a 32-bit value matching the runtime's + // `int taken` parameter, so that no uninitialized high bits of the i1 + // register can reach the runtime (see issue #83). + auto *taken = IRB.CreateZExt(I.getCondition(), IRB.getInt32Ty()); auto runtimeCall = buildRuntimeCall(IRB, runtime.pushPathConstraint, {{I.getCondition(), true}, - {I.getCondition(), false}, + {taken, false}, {getTargetPreferredInt(&I), false}}); registerSymbolicComputation(runtimeCall); } @@ -923,11 +931,13 @@ void Symbolizer::visitSwitchInst(SwitchInst &I) { IRB.SetInsertPoint(constraintBlock); for (auto &caseHandle : I.cases()) { auto *caseTaken = IRB.CreateICmpEQ(condition, caseHandle.getCaseValue()); + // Zero-extend to match the runtime's `int taken` parameter (issue #83). + auto *caseTakenInt = IRB.CreateZExt(caseTaken, IRB.getInt32Ty()); auto *caseConstraint = IRB.CreateCall( runtime.comparisonHandlers[CmpInst::ICMP_EQ], {conditionExpr, createValueExpression(caseHandle.getCaseValue(), IRB)}); IRB.CreateCall(runtime.pushPathConstraint, - {caseConstraint, caseTaken, getTargetPreferredInt(&I)}); + {caseConstraint, caseTakenInt, getTargetPreferredInt(&I)}); } } @@ -1099,7 +1109,7 @@ void Symbolizer::tryAlternative(IRBuilder<> &IRB, Value *V) { {destExpr, concreteDestExpr}); auto *pushAssertion = IRB.CreateCall( runtime.pushPathConstraint, - {destAssertion, IRB.getInt1(true), getTargetPreferredInt(V)}); + {destAssertion, IRB.getInt32(1), getTargetPreferredInt(V)}); registerSymbolicComputation(SymbolicComputation( concreteDestExpr, pushAssertion, {Input(V, 0, destAssertion)})); } diff --git a/test/xor_taken.c b/test/xor_taken.c new file mode 100644 index 00000000..87053926 --- /dev/null +++ b/test/xor_taken.c @@ -0,0 +1,47 @@ +// This file is part of SymCC. +// +// SymCC is free software: you can redistribute it and/or modify it under the +// terms of the GNU General Public License as published by the Free Software +// Foundation, either version 3 of the License, or (at your option) any later +// version. +// +// SymCC is distributed in the hope that it will be useful, but WITHOUT ANY +// WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR +// A PARTICULAR PURPOSE. See the GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License along with +// SymCC. If not, see . + +// Regression test for issue #83: SymCC failed to generate diverging inputs when +// a branch condition is produced through a logical negation. Clang lowers +// "!(0 == x)" to "xor i1 %cond, true", and the i1 result was passed to the +// runtime's _sym_push_path_constraint() as the "taken" argument with +// uninitialized high bits (observed as 254/255), so a not-taken branch was +// mis-recorded as taken and the solver explored the wrong direction. +// +// RUN: %symcc -O2 %s -o %t +// RUN: echo -ne "\x00\x00" | %t 2>&1 | %filecheck %s +#include +#include +#include + +int main(void) { + uint16_t x = 0; + if (read(STDIN_FILENO, &x, sizeof(x)) != sizeof(x)) { + fprintf(stderr, "Failed to read input\n"); + return -1; + } + + // "!(0 == x)" is lowered to an xor-based negation feeding the branch. + // With the seed x == 0 the branch is NOT taken, so a correct SymCC must + // push the path constraint and solve it for the other direction (x != 0). + // SIMPLE: Trying to solve + // QSYM: SMT + int taken = !(0 == x); + if (taken) + fprintf(stderr, "taken\n"); + else + fprintf(stderr, "not taken\n"); + // ANY: not taken + return 0; +}