1 /********************************************************************
2 * AUTHORS: Vijay Ganesh
3 *
4 * BEGIN DATE: November, 2005
5 *
6 Permission is hereby granted, free of charge, to any person obtaining a copy
7 of this software and associated documentation files (the "Software"), to deal
8 in the Software without restriction, including without limitation the rights
9 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10 copies of the Software, and to permit persons to whom the Software is
11 furnished to do so, subject to the following conditions:
12
13 The above copyright notice and this permission notice shall be included in
14 all copies or substantial portions of the Software.
15
16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
22 THE SOFTWARE.
23 ********************************************************************/
24
25 #include "stp/Printer/printers.h"
26 #include <cassert>
27 namespace printer
28 {
29
30 using std::string;
31 using std::endl;
32 using namespace stp;
33
34 // printer for C code (copied from PL_Print())
35 // TODO: this does not fully implement printing of all of the STP
36 // language - FatalError calls inserted for unimplemented
37 // functionality, e.g.,:
38 // FatalError("C_Print1: printing not implemented for this kind: ",*this);
39
40 // helper function for printing C code (copied from PL_Print1())
41 // if this node is present in the letvar Map, then print the letvar
C_Print1(ostream & os,const ASTNode n,int indentation,bool letize,STPMgr * bm)42 void C_Print1(ostream& os, const ASTNode n, int indentation, bool letize,
43 STPMgr* bm)
44 {
45
46 unsigned int num_bytes;
47 Kind LHSkind, RHSkind;
48
49 // os << spaces(indentation);
50 // os << endl << spaces(indentation);
51 if (!n.IsDefined())
52 {
53 os << "<undefined>";
54 return;
55 }
56
57 // this is to print letvars for shared subterms inside the printing
58 // of "(LET v0 = term1, v1=term1@term2,...
59 if ((bm->NodeLetVarMap1.find(n) != bm->NodeLetVarMap1.end()) && !letize)
60 {
61 C_Print1(os, (bm->NodeLetVarMap1[n]), indentation, letize, bm);
62 return;
63 }
64
65 // this is to print letvars for shared subterms inside the actual
66 // term to be printed
67 if ((bm->NodeLetVarMap.find(n) != bm->NodeLetVarMap.end()) && letize)
68 {
69 C_Print1(os, (bm->NodeLetVarMap[n]), indentation, letize, bm);
70 return;
71 }
72
73 // otherwise print it normally
74 Kind kind = n.GetKind();
75 const ASTVec& c = n.GetChildren();
76 switch (kind)
77 {
78 case BOOLEXTRACT:
79 FatalError("C_Print1: printing not implemented for this kind: ", n);
80 break;
81 case BITVECTOR:
82 FatalError("C_Print1: printing not implemented for this kind: ", n);
83 break;
84 case BOOLEAN:
85 FatalError("C_Print1: printing not implemented for this kind: ", n);
86 break;
87 case FALSE:
88 os << "0";
89 break;
90 case TRUE:
91 os << "1";
92 break;
93 case BVCONST:
94 case SYMBOL:
95 // print in C friendly format:
96 n.nodeprint(os, true);
97 break;
98 case READ:
99 C_Print1(os, c[0], indentation, letize, bm);
100 os << "[";
101 C_Print1(os, c[1], indentation, letize, bm);
102 os << "]";
103 break;
104 case WRITE:
105 os << "(";
106 C_Print1(os, c[0], indentation, letize, bm);
107 os << " WITH [";
108 C_Print1(os, c[1], indentation, letize, bm);
109 os << "] := ";
110 C_Print1(os, c[2], indentation, letize, bm);
111 os << ")";
112 os << endl;
113 break;
114 case BVUMINUS:
115 os << kind << "( ";
116 C_Print1(os, c[0], indentation, letize, bm);
117 os << ")";
118 break;
119 case NOT:
120 os << "!(";
121 C_Print1(os, c[0], indentation, letize, bm);
122 os << ") " << endl;
123 break;
124 case BVNOT:
125 os << " ~(";
126 C_Print1(os, c[0], indentation, letize, bm);
127 os << ")";
128 break;
129 case BVCONCAT:
130 // stopgap for un-implemented features
131 FatalError("C_Print1: printing not implemented for this kind: ", n);
132 break;
133 case BVOR:
134 os << "(";
135 C_Print1(os, c[0], indentation, letize, bm);
136 os << " | ";
137 C_Print1(os, c[1], indentation, letize, bm);
138 os << ")";
139 break;
140 case BVAND:
141 os << "(";
142 C_Print1(os, c[0], indentation, letize, bm);
143 os << " & ";
144 C_Print1(os, c[1], indentation, letize, bm);
145 os << ")";
146 break;
147 case BVEXTRACT:
148 {
149
150 // we only accept indices that are byte-aligned
151 // (e.g., [15:8], [23:16])
152 // and round down to byte indices rather than bit indices
153 unsigned upper = c[1].GetUnsignedConst();
154 unsigned lower = c[2].GetUnsignedConst();
155 assert(upper > lower);
156 assert(lower % 8 == 0);
157 assert((upper + 1) % 8 == 0);
158 num_bytes = (upper - lower + 1) / 8;
159 assert(num_bytes > 0);
160
161 // for multi-byte extraction, use the ADDRESS
162 if (num_bytes > 1)
163 {
164 os << "&";
165 C_Print1(os, c[0], indentation, letize, bm);
166 os << "[" << lower / 8 << "]";
167 }
168 // for single-byte extraction, use the VALUE
169 else
170 {
171 C_Print1(os, c[0], indentation, letize, bm);
172 os << "[" << lower / 8 << "]";
173 }
174
175 break;
176 }
177 case BVLEFTSHIFT:
178 // stopgap for un-implemented features
179 FatalError("C_Print1: printing not implemented for this kind: ", n);
180 break;
181 case BVRIGHTSHIFT:
182 // stopgap for un-implemented features
183 FatalError("C_Print1: printing not implemented for this kind: ", n);
184 break;
185 case BVMULT:
186 case BVSUB:
187 case BVPLUS:
188 case SBVDIV:
189 case SBVREM:
190 case BVDIV:
191 case BVMOD:
192 os << kind << "(";
193 os << n.GetValueWidth();
194 for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend;
195 it++)
196 {
197 os << ", " << endl;
198 C_Print1(os, *it, indentation, letize, bm);
199 }
200 os << ")" << endl;
201 break;
202 case ITE:
203 os << "if (";
204 C_Print1(os, c[0], indentation, letize, bm);
205 os << ")" << endl;
206 os << "{";
207 C_Print1(os, c[1], indentation, letize, bm);
208 os << endl << "} else {";
209 C_Print1(os, c[2], indentation, letize, bm);
210 os << endl << "}";
211 break;
212 case BVLT:
213 // convert to UNSIGNED before doing comparison!
214 os << "((unsigned char)";
215 C_Print1(os, c[0], indentation, letize, bm);
216 os << " < ";
217 os << "(unsigned char)";
218 C_Print1(os, c[1], indentation, letize, bm);
219 os << ")";
220 break;
221 case BVLE:
222 // convert to UNSIGNED before doing comparison!
223 os << "((unsigned char)";
224 C_Print1(os, c[0], indentation, letize, bm);
225 os << " <= ";
226 os << "(unsigned char)";
227 C_Print1(os, c[1], indentation, letize, bm);
228 os << ")";
229 break;
230 case BVGT:
231 // convert to UNSIGNED before doing comparison!
232 os << "((unsigned char)";
233 C_Print1(os, c[0], indentation, letize, bm);
234 os << " > ";
235 os << "(unsigned char)";
236 C_Print1(os, c[1], indentation, letize, bm);
237 os << ")";
238 break;
239 case BVGE:
240 // convert to UNSIGNED before doing comparison!
241 os << "((unsigned char)";
242 C_Print1(os, c[0], indentation, letize, bm);
243 os << " >= ";
244 os << "(unsigned char)";
245 C_Print1(os, c[1], indentation, letize, bm);
246 os << ")";
247 break;
248 case BVXOR:
249 case BVNAND:
250 case BVNOR:
251 case BVXNOR:
252 // stopgap for un-implemented features
253 FatalError("C_Print1: printing not implemented for this kind: ", n);
254 break;
255 case BVSLT:
256 // convert to SIGNED before doing comparison!
257 os << "((signed char)";
258 C_Print1(os, c[0], indentation, letize, bm);
259 os << " < ";
260 os << "(signed char)";
261 C_Print1(os, c[1], indentation, letize, bm);
262 os << ")";
263 break;
264 case BVSLE:
265 // convert to SIGNED before doing comparison!
266 os << "((signed char)";
267 C_Print1(os, c[0], indentation, letize, bm);
268 os << " <= ";
269 os << "(signed char)";
270 C_Print1(os, c[1], indentation, letize, bm);
271 os << ")";
272 break;
273 case BVSGT:
274 // convert to SIGNED before doing comparison!
275 os << "((signed char)";
276 C_Print1(os, c[0], indentation, letize, bm);
277 os << " > ";
278 os << "(signed char)";
279 C_Print1(os, c[1], indentation, letize, bm);
280 os << ")";
281 break;
282 case BVSGE:
283 // convert to SIGNED before doing comparison!
284 os << "((signed char)";
285 C_Print1(os, c[0], indentation, letize, bm);
286 os << " >= ";
287 os << "(signed char)";
288 C_Print1(os, c[1], indentation, letize, bm);
289 os << ")";
290 break;
291 case EQ:
292 // tricky tricky ... if it's a single-byte comparison,
293 // simply do ==, but if it's multi-byte, must do memcmp
294 LHSkind = c[0].GetKind();
295 RHSkind = c[1].GetKind();
296
297 num_bytes = 0;
298
299 // try to figure out whether it's a single-byte or multi-byte
300 // comparison
301 if (LHSkind == BVEXTRACT)
302 {
303 unsigned upper = c[0].GetChildren()[1].GetUnsignedConst();
304 unsigned lower = c[0].GetChildren()[2].GetUnsignedConst();
305 num_bytes = (upper - lower + 1) / 8;
306 }
307 else if (RHSkind == BVEXTRACT)
308 {
309 unsigned upper = c[1].GetChildren()[1].GetUnsignedConst();
310 unsigned lower = c[1].GetChildren()[2].GetUnsignedConst();
311 num_bytes = (upper - lower + 1) / 8;
312 }
313
314 if (num_bytes > 1)
315 {
316 os << "(memcmp(";
317 C_Print1(os, c[0], indentation, letize, bm);
318 os << ", ";
319 C_Print1(os, c[1], indentation, letize, bm);
320 os << ", ";
321 os << num_bytes;
322 os << ") == 0)";
323 }
324 else if (num_bytes == 1)
325 {
326 os << "(";
327 C_Print1(os, c[0], indentation, letize, bm);
328 os << " == ";
329 C_Print1(os, c[1], indentation, letize, bm);
330 os << ")";
331 }
332 else
333 {
334 FatalError("C_Print1: ugh problem in implementing ==");
335 }
336
337 break;
338 case AND:
339 case OR:
340 case NAND:
341 case NOR:
342 case XOR:
343 {
344 os << "(";
345 C_Print1(os, c[0], indentation, letize, bm);
346 ASTVec::const_iterator it = c.begin();
347 ASTVec::const_iterator itend = c.end();
348
349 it++;
350 for (; it != itend; it++)
351 {
352 switch (kind)
353 {
354 case AND:
355 os << " && ";
356 break;
357 case OR:
358 os << " || ";
359 break;
360 case NAND:
361 FatalError("unsupported boolean type in C_Print1");
362 break;
363 case NOR:
364 FatalError("unsupported boolean type in C_Print1");
365 break;
366 case XOR:
367 FatalError("unsupported boolean type in C_Print1");
368 break;
369 default:
370 FatalError("unsupported boolean type in C_Print1");
371 break;
372 }
373 C_Print1(os, *it, indentation, letize, bm);
374 }
375 os << ")";
376 break;
377 }
378 case IFF:
379 // stopgap for un-implemented features
380 FatalError("C_Print1: printing not implemented for this kind: ", n);
381 break;
382 case IMPLIES:
383 // stopgap for un-implemented features
384 FatalError("C_Print1: printing not implemented for this kind: ", n);
385 break;
386 case BVSX:
387 // stopgap for un-implemented features
388 FatalError("C_Print1: printing not implemented for this kind: ", n);
389 break;
390 default:
391 // remember to use LispPrinter here. Otherwise this function will
392 // go into an infinite loop. Recall that "<<" is overloaded to
393 // the lisp printer. FatalError uses lispprinter
394 FatalError("C_Print1: printing not implemented for this kind: ", n);
395 break;
396 }
397 }
398
399 // two pass algorithm:
400 //
401 // 1. In the first pass, letize this Node, N: i.e. if a node
402 // 1. appears more than once in N, then record this fact.
403 //
404 // 2. In the second pass print a "global let" and then print N
405 // 2. as follows: Every occurence of a node occuring more than
406 // 2. once is replaced with the corresponding let variable.
C_Print(ostream & os,const ASTNode n,STPMgr * bm,int indentation)407 ostream& C_Print(ostream& os, const ASTNode n, STPMgr* bm, int indentation)
408 {
409 // Clear the PrintMap
410 bm->PLPrintNodeSet.clear();
411 bm->NodeLetVarMap.clear();
412 bm->NodeLetVarVec.clear();
413 bm->NodeLetVarMap1.clear();
414
415 // pass 1: letize the node
416 n.LetizeNode(bm);
417
418 unsigned int num_bytes = 0;
419
420 // pass 2:
421 //
422 // 2. print all the let variables and their counterpart expressions
423 // 2. as follows (LET var1 = expr1, var2 = expr2, ...
424 //
425 // 3. Then print the Node itself, replacing every occurence of
426 // 3. expr1 with var1, expr2 with var2, ...
427 // os << "(";
428 if (0 < bm->NodeLetVarMap.size())
429 {
430 // ASTNodeMap::iterator it=bm->NodeLetVarMap.begin();
431 // ASTNodeMap::iterator itend=bm->NodeLetVarMap.end();
432 vector<std::pair<ASTNode, ASTNode>>::iterator it =
433 bm->NodeLetVarVec.begin();
434 vector<std::pair<ASTNode, ASTNode>>::iterator itend =
435 bm->NodeLetVarVec.end();
436
437 // start a new block to create new static scope
438 os << "{" << endl;
439
440 for (; it != itend; it++)
441 {
442
443 // see if it's a BVEXTRACT, and if so, whether it's multi-byte
444 if (it->second.GetKind() == BVEXTRACT)
445 {
446 unsigned upper = it->second.GetChildren()[1].GetUnsignedConst();
447 unsigned lower = it->second.GetChildren()[2].GetUnsignedConst();
448 num_bytes = (upper - lower + 1) / 8;
449 assert(num_bytes > 0);
450 }
451
452 // print the let var first
453 if (num_bytes > 1)
454 {
455 // for multi-byte assignment, use 'memcpy' and array notation
456 os << "unsigned char ";
457 C_Print1(os, it->first, indentation, false, bm);
458 os << "[" << num_bytes << "]; ";
459 os << "memcpy(";
460 C_Print1(os, it->first, indentation, false, bm);
461 os << ", ";
462 // print the expr
463 C_Print1(os, it->second, indentation, false, bm);
464 os << ", " << num_bytes << ");";
465 }
466 else
467 {
468 // for single-byte assignment, use '='
469 os << "unsigned char ";
470 C_Print1(os, it->first, indentation, false, bm);
471 os << " = ";
472 // print the expr
473 C_Print1(os, it->second, indentation, false, bm);
474 os << ";" << endl;
475 }
476
477 // update the second map for proper printing of LET
478 bm->NodeLetVarMap1[it->second] = it->first;
479 }
480
481 os << endl << "stp_assert ";
482 C_Print1(os, n, indentation, true, bm);
483
484 os << ";" << endl << "}";
485 }
486 else
487 {
488 os << "stp_assert ";
489 C_Print1(os, n, indentation, false, bm);
490 os << ";";
491 }
492 // os << " )";
493 // os << " ";
494
495 return os;
496 }
497 }
498