1 #include "boolector.h"
2
3 #include <ctype.h>
4 #include <stdarg.h>
5 #include <stdio.h>
6 #include <stdlib.h>
7 #include <string.h>
8
9 static void
die(const char * fmt,...)10 die (const char *fmt, ...)
11 {
12 va_list ap;
13 va_start (ap, fmt);
14 fprintf (stderr, "*** memcpy: ");
15 vfprintf (stderr, fmt, ap);
16 va_end (ap);
17 fputc ('\n', stderr);
18 exit (1);
19 }
20
21 static int
isint(const char * str)22 isint (const char *str)
23 {
24 char ch;
25
26 if ((ch = *str++) == '-') ch = *str++;
27
28 if (!isdigit (ch)) return 0;
29
30 while (isdigit ((ch = *str++)))
31 ;
32
33 return !ch;
34 }
35
36 int
main(int argc,char ** argv)37 main (int argc, char **argv)
38 {
39 BoolectorNode *src, *dst, *eos, *eod, *p, *q, *tmp, *n, *j, *zero, *one;
40 BoolectorNode *mem, *assumption, *alternative, *cmp, *root, *v;
41 int i, len, havelen, overlapping, signed_size_t;
42 BoolectorNode *old, *new;
43 BoolectorSort isort, esort, asort;
44 Btor *btor;
45
46 len = 0;
47 havelen = 0;
48 overlapping = 0;
49 signed_size_t = 0;
50
51 for (i = 1; i < argc; i++)
52 {
53 if (!strcmp (argv[i], "-h"))
54 {
55 fprintf (stderr, "usage: memcpy [-h][-o][-s] <len>\n");
56 fprintf (stderr, "\n");
57 fprintf (stderr, " -h print this command line option summary\n");
58 fprintf (stderr, " -o allow 'src' and 'dst' to overlap\n");
59 fprintf (stderr, " -s assume 'size_t' to be signed\n");
60 exit (1);
61 }
62 else if (!strcmp (argv[i], "-o"))
63 {
64 overlapping = 1;
65 }
66 else if (!strcmp (argv[i], "-s"))
67 {
68 signed_size_t = 1;
69 }
70 else if (argv[i][0] == '-')
71 die ("invalid command line option '%s'", argv[i]);
72 else if (!isint (argv[i]))
73 die ("expected integer but got '%s'", argv[i]);
74 else if (havelen)
75 die ("multiple integer arguments");
76 else
77 {
78 havelen = 1;
79 len = atoi (argv[i]);
80 }
81 }
82
83 if (!havelen) die ("length argument missing");
84
85 if (len < 0 && !signed_size_t)
86 die ("negative <len> while 'size_t' is unsigned (try '-s')");
87
88 btor = boolector_new ();
89 boolector_set_opt (btor, BTOR_OPT_REWRITE_LEVEL, 0);
90
91 isort = boolector_bitvec_sort (btor, 32);
92 esort = boolector_bitvec_sort (btor, 8);
93 asort = boolector_array_sort (btor, isort, esort);
94 mem = boolector_array (btor, asort, "mem");
95
96 src = boolector_var (btor, isort, "src");
97 dst = boolector_var (btor, isort, "dst");
98
99 n = boolector_unsigned_int (btor, len, isort);
100
101 j = boolector_var (btor, isort, "j");
102
103 zero = boolector_zero (btor, isort);
104 one = boolector_one (btor, isort);
105
106 eos = boolector_add (btor, src, n);
107 eod = boolector_add (btor, dst, n);
108
109 cmp = boolector_ulte (btor, src, eos);
110 assumption = cmp;
111
112 cmp = boolector_ulte (btor, dst, eod);
113 tmp = boolector_and (btor, assumption, cmp);
114 boolector_release (btor, assumption);
115 boolector_release (btor, cmp);
116 assumption = tmp;
117
118 if (!overlapping)
119 {
120 cmp = boolector_ulte (btor, eos, dst);
121 alternative = cmp;
122
123 cmp = boolector_ulte (btor, eod, src);
124 tmp = boolector_or (btor, alternative, cmp);
125 boolector_release (btor, alternative);
126 boolector_release (btor, cmp);
127 alternative = tmp;
128
129 tmp = boolector_and (btor, assumption, alternative);
130 boolector_release (btor, assumption);
131 boolector_release (btor, alternative);
132 assumption = tmp;
133 }
134
135 if (signed_size_t)
136 {
137 cmp = boolector_slte (btor, zero, j);
138 tmp = boolector_and (btor, assumption, cmp);
139 boolector_release (btor, assumption);
140 boolector_release (btor, cmp);
141 assumption = tmp;
142 }
143
144 if (signed_size_t)
145 cmp = boolector_slt (btor, j, n);
146 else
147 cmp = boolector_ult (btor, j, n);
148
149 tmp = boolector_and (btor, assumption, cmp);
150 boolector_release (btor, assumption);
151 boolector_release (btor, cmp);
152 assumption = tmp;
153
154 p = boolector_add (btor, src, j);
155 old = boolector_read (btor, mem, p);
156 boolector_release (btor, p);
157
158 p = boolector_copy (btor, src);
159 q = boolector_copy (btor, dst);
160
161 for (i = 0; i < len; i++)
162 {
163 v = boolector_read (btor, mem, p);
164 tmp = boolector_write (btor, mem, q, v);
165 boolector_release (btor, mem);
166 boolector_release (btor, v);
167 mem = tmp;
168
169 tmp = boolector_add (btor, p, one);
170 boolector_release (btor, p);
171 p = tmp;
172
173 tmp = boolector_add (btor, q, one);
174 boolector_release (btor, q);
175 q = tmp;
176 }
177
178 boolector_release (btor, q);
179 q = boolector_add (btor, dst, j);
180 new = boolector_read (btor, mem, q);
181
182 cmp = boolector_ne (btor, old, new);
183
184 root = boolector_and (btor, assumption, cmp);
185 boolector_release (btor, assumption);
186 boolector_release (btor, cmp);
187
188 boolector_dump_btor_node (btor, stdout, root);
189
190 boolector_release (btor, root);
191 boolector_release (btor, p);
192 boolector_release (btor, q);
193 boolector_release (btor, old);
194 boolector_release (btor, new);
195 boolector_release (btor, eos);
196 boolector_release (btor, eod);
197 boolector_release (btor, one);
198 boolector_release (btor, zero);
199 boolector_release (btor, j);
200 boolector_release (btor, n);
201 boolector_release (btor, dst);
202 boolector_release (btor, src);
203 boolector_release (btor, mem);
204 boolector_release_sort (btor, isort);
205 boolector_release_sort (btor, esort);
206 boolector_release_sort (btor, asort);
207 boolector_delete (btor);
208
209 return 0;
210 }
211