PR for xor problem (issue #83)

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

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

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

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