1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
diff --git a/NEWS b/NEWS
index ba021869b184..a9acb822e95d 100644
--- a/NEWS
+++ b/NEWS
@@ -10,6 +10,9 @@ GNU grep NEWS -*- outline -*-
Character ranges would not work in single-byte character sets other
than C (for example, ISO-8859-1 or KOI8-R). [bug introduced in 2.6]
+ The output of grep was incorrect for whole-word (-w) matches if the
+ patterns included a backreference.
+
** Portability
Avoid a link failure on Solaris 8.
diff --git a/src/dfasearch.c b/src/dfasearch.c
index a43f822aafa0..2dbe6b11bcc4 100644
--- a/src/dfasearch.c
+++ b/src/dfasearch.c
@@ -18,6 +18,57 @@
/* Written August 1992 by Mike Haertel. */
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+void klee_assume(uintptr_t x) {}
+void klee_mark_patch(uint64_t patch_num) {}
+
+bool __klee_runtime = true;
+void
+klee_make_symbolic(void *addr, size_t nbytes, const char *name)
+{
+ __klee_runtime = false;
+}
+
+int
+__choose(const char *switch_id)
+{
+ char *env = getenv(switch_id);
+ if (env == NULL)
+ return 0;
+ int result=atoi(env);
+ return result;
+}
+
+#define MAX_NAME_LENGTH 1000
+#define SYMBOLIC_OUTPUT_PROTO(type, typestr) \
+type \
+angelix_symbolic_output_##type(type expr, char* id) \
+{ \
+ if (!__klee_runtime) \
+ return expr; \
+ static int instance = 0; \
+ char name[MAX_NAME_LENGTH]; \
+ sprintf(name, "out!%s!%d", id, instance++); \
+ type s; \
+ klee_make_symbolic(&s, sizeof(s), name); \
+ klee_assume(s == expr); \
+ return s; \
+}
+SYMBOLIC_OUTPUT_PROTO(int, "int")
+SYMBOLIC_OUTPUT_PROTO(long, "long")
+SYMBOLIC_OUTPUT_PROTO(size_t, "size_t")
+SYMBOLIC_OUTPUT_PROTO(bool, "bool")
+SYMBOLIC_OUTPUT_PROTO(char, "char")
+#undef SYMBOLIC_OUTPUT_PROTO
+
+#define ANGELIX_OUTPUT(type, expr, name) \
+ angelix_symbolic_output_##type((expr), (name))
+
+#define __COMPILE_40
+
#include <config.h>
#include "search.h"
#include "dfa.h"
@@ -357,8 +408,20 @@ EGexecute (char const *buf, size_t size, size_t *match_size,
{
/* Good enough for a non-exact match.
No need to look at further patterns, if any. */
+char __choose2 = __choose("__SWITCH2");
+klee_make_symbolic(&__choose2, sizeof(__choose2), "__choose2");
+if (__choose2 == 0)
+ {
beg = match;
goto success_in_len;
+ }
+#ifdef __COMPILE_40
+else if (__choose2 == 3)
+ {
+ klee_mark_patch(40);
+ goto success;
+ }
+#endif
}
if (match < best_match || (match == best_match && len > best_len))
{
@@ -388,5 +451,6 @@ EGexecute (char const *buf, size_t size, size_t *match_size,
*match_size = len;
ret_val = beg - buf;
out:
+ ANGELIX_OUTPUT(size_t, *match_size, "match_size");
return ret_val;
}
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 02db64c44ab3..59ed67223445 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -16,6 +16,7 @@
TESTS = \
backref.sh \
+ backref-word \
bre.sh \
case-fold-backref \
case-fold-backslash-w \
|
