diff --git a/runtime/qsym_backend/Runtime.cpp b/runtime/qsym_backend/Runtime.cpp index 650787bf..174e3101 100644 --- a/runtime/qsym_backend/Runtime.cpp +++ b/runtime/qsym_backend/Runtime.cpp @@ -320,7 +320,7 @@ void _sym_push_path_constraint(SymExpr constraint, int taken, uintptr_t site_id) { if (constraint == nullptr) return; - + taken = taken & 0x1; g_solver->addJcc(allocatedExpressions.at(constraint), taken != 0, site_id); } diff --git a/runtime/simple_backend/Runtime.cpp b/runtime/simple_backend/Runtime.cpp index 53ca28cd..43f409e9 100644 --- a/runtime/simple_backend/Runtime.cpp +++ b/runtime/simple_backend/Runtime.cpp @@ -435,7 +435,7 @@ void _sym_push_path_constraint(Z3_ast constraint, int taken, uintptr_t site_id [[maybe_unused]]) { if (constraint == nullptr) return; - + taken = taken & 0x1; constraint = Z3_simplify(g_context, constraint); Z3_inc_ref(g_context, constraint); diff --git a/test/xor.c b/test/xor.c new file mode 100644 index 00000000..caee203e --- /dev/null +++ b/test/xor.c @@ -0,0 +1,45 @@ +// 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 . + +// RUN: %symcc %s -o %t +// RUN: echo -ne "\x00\x00\x00" | %t 2>&1 | %filecheck %s +// +// Check the case that xor exist before push path constraint + +#include +#include + +struct S0 { + uint16_t f0; +}; + +static int8_t g_2 = 0; +static uint16_t g_927 = 0; + +static int32_t func_1() { + int32_t l_968 = 6; + if (l_968 = !(0 == g_927)) { + struct S0 l_974, l_1047; + if (9 && (l_974.f0 = g_2 > 0 && l_1047.f0) == l_974.f0 <= 1); + } +} +void main () { + read(STDIN_FILENO, &g_2, sizeof(g_2)); + read(STDIN_FILENO, &g_927, sizeof(g_927)); + func_1(); + // SIMPLE: Trying to solve + // SIMPLE: Found diverging input + // QSYM-COUNT-2: SMT + // QSYM: New testcase +} diff --git a/test/xor.test b/test/xor.test new file mode 100644 index 00000000..6bc154fa --- /dev/null +++ b/test/xor.test @@ -0,0 +1,2 @@ +RUN: %symcc %S/xor.c -o %t +RUN: echo -ne "\x00\x00\x00" | %t 2>&1 | %filecheck %S/xor.c \ No newline at end of file