Fix #83: pass a clean 32-bit taken value to _sym_push_path_constraint

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 =

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)}));
   }

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 <https://www.gnu.org/licenses/>.
+
+// 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 <stdint.h>
+#include <stdio.h>
+#include <unistd.h>
+
+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;
+}