From 6f5ca6750410601235f75072fcfe379df86e28b2 Mon Sep 17 00:00:00 2001
From: ret2dir <742991625@qq.com>
Date: Mon, 20 Sep 2021 19:30:35 +0800
Subject: [PATCH 1/2] PR for xor problem
---
runtime/qsym_backend/Runtime.cpp | 2 +-
runtime/simple_backend/Runtime.cpp | 2 +-
test/xor.c | 41 ++++++++++++++++++++++++++++++
test/xor.test | 2 ++
4 files changed, 45 insertions(+), 2 deletions(-)
create mode 100644 test/xor.c
create mode 100644 test/xor.test
diff --git a/runtime/qsym_backend/Runtime.cpp b/runtime/qsym_backend/Runtime.cpp
index 68b093bd..d305821d 100644
--- a/runtime/qsym_backend/Runtime.cpp
+++ b/runtime/qsym_backend/Runtime.cpp
@@ -285,7 +285,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 d7ef5f20..c329f019 100644
--- a/runtime/simple_backend/Runtime.cpp
+++ b/runtime/simple_backend/Runtime.cpp
@@ -417,7 +417,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..902c54c7
--- /dev/null
+++ b/test/xor.c
@@ -0,0 +1,41 @@
+// 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();
+}
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
From 48fec8337bf2fcec44267d461663d7cc6b9db82e Mon Sep 17 00:00:00 2001
From: ret2dir <742991625@qq.com>
Date: Fri, 24 Sep 2021 15:14:17 +0800
Subject: [PATCH 2/2] fix xor filecheck comments
---
test/xor.c | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/test/xor.c b/test/xor.c
index 902c54c7..caee203e 100644
--- a/test/xor.c
+++ b/test/xor.c
@@ -38,4 +38,8 @@ 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
}