1 /********************************************************************
2 * AUTHORS: Vijay Ganesh, Trevor Hansen, Dan Liew
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/AST/AST.h"
26 #include "stp/Simplifier/Simplifier.h"
27 #include "stp/Simplifier/constantBitP/ConstantBitP_TransferFunctions.h"
28 #include "stp/Simplifier/constantBitP/ConstantBitP_Utility.h"
29 #include <set>
30 #include <stdexcept>
31
32 namespace simplifier
33 {
34 namespace constantBitP
35 {
36 using std::endl;
37 using std::pair;
38 using std::set;
39
40 const bool debug_division = false;
41 extern std::ostream& log;
42
43 using stp::STPMgr;
44
45 enum WhatIsOutput
46 {
47 REMAINDER_IS_OUTPUT,
48 QUOTIENT_IS_OUTPUT
49 };
50
51 enum Operation
52 {
53 SIGNED_DIVISION,
54 SIGNED_REMAINDER,
55 SIGNED_MODULUS
56 };
57
58 // For unsigned 3-bit exhaustive, there are 1119 differences for unsigned
59 // division.
60
61 // a/b and a%b. a=bq +r. Where b!=0 implies r<b. Multiplication and addition
62 // don't overflow.
63
64 // returning true = conflict.
65 // Fix value of a to b.
fix(FixedBits & a,const FixedBits & b,const int i)66 bool fix(FixedBits& a, const FixedBits& b, const int i)
67 {
68 if (!b.isFixed(i))
69 return false;
70
71 if (a.isFixed(i) && b.isFixed(i) && (a.getValue(i) ^ b.getValue(i)))
72 return true;
73
74 if (!a.isFixed(i) && b.isFixed(i))
75 {
76 a.setFixed(i, true);
77 a.setValue(i, b.getValue(i));
78 return false;
79 }
80
81 return false;
82 }
83
cbvToFixedBits(stp::CBV low,unsigned width)84 FixedBits cbvToFixedBits(stp::CBV low, unsigned width)
85 {
86 FixedBits lowBits(width, false);
87 for (int i = width - 1; i >= 0; i--)
88 {
89 if (CONSTANTBV::BitVector_bit_test(low, i))
90 {
91 lowBits.setFixed(i, true);
92 lowBits.setValue(i, true);
93 }
94 else
95 {
96 lowBits.setFixed(i, true);
97 lowBits.setValue(i, false);
98 }
99 }
100 return lowBits;
101 }
102
103 // The value "b" is in the range [low,high] inclusive.
104 // Unfortunately it's not idempotent, <....1> [5,6], doesn't completely set it.
fix(FixedBits & b,stp::CBV low,stp::CBV high)105 Result fix(FixedBits& b, stp::CBV low, stp::CBV high)
106 {
107 FixedBits init = b;
108 const int width = b.getWidth();
109
110 FixedBits highBits = cbvToFixedBits(high, width);
111 FixedBits lowBits = cbvToFixedBits(low, width);
112
113 vector<FixedBits*> c;
114 c.push_back(&b);
115 c.push_back(&highBits);
116
117 FixedBits t(1, true);
118 t.setFixed(0, true);
119 t.setValue(0, true);
120 Result result1 = bvLessThanEqualsBothWays(c, t);
121
122 c.clear();
123 c.push_back(&lowBits);
124 c.push_back(&b);
125 Result result2 = bvLessThanEqualsBothWays(c, t);
126
127 Result result = merge(result1, result2);
128 if (result == CONFLICT)
129 return CONFLICT;
130
131 for (int i = width - 1; i >= 0; i--)
132 {
133 if ((CONSTANTBV::BitVector_bit_test(low, i) ==
134 CONSTANTBV::BitVector_bit_test(high, i)))
135 {
136 bool toFix = CONSTANTBV::BitVector_bit_test(low, i);
137 if (b.isFixed(i))
138 {
139 if (b.getValue(i) != toFix)
140 {
141 return CONFLICT;
142 }
143 }
144 else
145 {
146 b.setFixed(i, true);
147 b.setValue(i, toFix);
148 }
149 }
150 else
151 break;
152 }
153
154 if (!FixedBits::equals(init, b))
155 return CHANGED;
156 return NO_CHANGE;
157 }
158
159 Result bvUnsignedQuotientAndRemainder2(vector<FixedBits*>& children,
160 FixedBits& output, STPMgr* bm,
161 WhatIsOutput whatIs);
162
bvUnsignedQuotientAndRemainder(vector<FixedBits * > & children,FixedBits & output,STPMgr * bm,WhatIsOutput whatIs)163 Result bvUnsignedQuotientAndRemainder(vector<FixedBits*>& children,
164 FixedBits& output, STPMgr* bm,
165 WhatIsOutput whatIs)
166 {
167 assert(output.getWidth() == children[0]->getWidth());
168 assert(output.getWidth() == children[1]->getWidth());
169 assert(children.size() == 2);
170
171 if (whatIs != QUOTIENT_IS_OUTPUT)
172 {
173 return bvUnsignedQuotientAndRemainder2(children, output, bm, whatIs);
174 }
175
176 FixedBits& a = *children[0];
177 FixedBits& b = *children[1];
178
179 const unsigned width = a.getWidth();
180
181 stp::CBV minTop = CONSTANTBV::BitVector_Create(width, true);
182 stp::CBV maxTop = CONSTANTBV::BitVector_Create(width, true);
183
184 setUnsignedMinMax(a, minTop, maxTop);
185
186 stp::CBV minBottom = CONSTANTBV::BitVector_Create(width, true);
187 stp::CBV maxBottom = CONSTANTBV::BitVector_Create(width, true);
188
189 setUnsignedMinMax(b, minBottom, maxBottom);
190
191 stp::CBV minQuotient = CONSTANTBV::BitVector_Create(width, true);
192 stp::CBV maxQuotient = CONSTANTBV::BitVector_Create(width, true);
193
194 stp::CBV minRemainder = CONSTANTBV::BitVector_Create(width, true);
195 stp::CBV maxRemainder = CONSTANTBV::BitVector_Create(width, true);
196
197 if (whatIs == QUOTIENT_IS_OUTPUT)
198 {
199 setUnsignedMinMax(output, minQuotient, maxQuotient);
200
201 for (unsigned i = 0; i < width; i++)
202 CONSTANTBV::BitVector_Bit_On(maxRemainder, i);
203 }
204 else
205 {
206 setUnsignedMinMax(output, minRemainder, maxRemainder);
207
208 for (unsigned i = 0; i < width; i++)
209 CONSTANTBV::BitVector_Bit_On(maxQuotient, i);
210 }
211
212 // need to clean up these at end.
213 stp::CBV one = CONSTANTBV::BitVector_Create(width, true);
214 CONSTANTBV::BitVector_increment(one);
215
216 stp::CBV max = CONSTANTBV::BitVector_Create(width, true);
217 CONSTANTBV::BitVector_Fill(max);
218
219 // quotient and remainder.
220 stp::CBV q = CONSTANTBV::BitVector_Create(width, true);
221 stp::CBV r = CONSTANTBV::BitVector_Create(width, true);
222 // misc.
223 stp::CBV copy = CONSTANTBV::BitVector_Create(width, true);
224 stp::CBV copy2 = CONSTANTBV::BitVector_Create(width, true);
225 stp::CBV multR = CONSTANTBV::BitVector_Create(width, true);
226
227 if (debug_division)
228 {
229 log << "--" << endl;
230 log << "initial" << endl;
231 log << "a:[" << *minTop << "," << *maxTop << "]";
232 log << " / b:[" << *minBottom << "," << *maxBottom << "] = ";
233 log << "[" << *minQuotient << "," << *maxQuotient << "]";
234 log << " rem [" << *minRemainder << "," << *maxRemainder << "]";
235 log << endl;
236 }
237
238 // If a bit is changed, then we fixed point again.
239 bool bitEverChanged = false;
240 bool bitJustChanged = true;
241 Result result = NO_CHANGE;
242
243 // We loop. There are 6 cases.
244 while (bitJustChanged)
245 {
246 bitJustChanged = false;
247
248 bool changed = true;
249
250 int iteration = 0;
251 while (changed)
252 {
253 changed = false;
254 CONSTANTBV::ErrCode e;
255
256 // The main loop doesn't work if there is a division by zero possible.
257 // If the minimum bottom is zero, but the minimum quotient is > 111.1111, then in
258 // our semantics of a/0 = 1..1, it can't be zero.
259 if (CONSTANTBV::BitVector_is_empty(minBottom) &&
260 CONSTANTBV::BitVector_Lexicompare(maxQuotient, max) < 0)
261 {
262 CONSTANTBV::BitVector_increment(minBottom);
263 if (CONSTANTBV::BitVector_Lexicompare(minBottom, maxBottom) > 0)
264 {
265 result = CONFLICT;
266 goto end;
267 }
268 }
269
270 if (CONSTANTBV::BitVector_is_empty(minBottom))
271 {
272 goto end; // Possible division by zero. Hard to work with..
273 }
274
275 bool carry_1 = false;
276 CONSTANTBV::BitVector_sub(copy, minTop, minRemainder, &carry_1);
277 if (!carry_1) // Not sure if it goes negative.
278 {
279 e = CONSTANTBV::BitVector_Div_Pos(q, copy, maxBottom, r);
280 assert(e == CONSTANTBV::ErrCode_Ok);
281
282 if (CONSTANTBV::BitVector_Lexicompare(minQuotient, q) < 0)
283 {
284 if (debug_division)
285 {
286 log << "1 minQ) " << *minTop;
287 log << " / " << *maxBottom;
288 log << " = " << *q;
289 log << " r " << *r << endl;
290 }
291
292 // min quotient is bigger. Bring in.
293 CONSTANTBV::BitVector_Copy(minQuotient, q);
294 changed = true;
295 }
296 }
297
298 CONSTANTBV::BitVector_Copy(copy, maxTop);
299 // bool carry_2 = false;
300 // CONSTANTBV::BitVector_sub(copy,maxTop,minRemainder,&carry_2);
301 // assert(!carry_1); // Not sure if it goes negative.
302
303 e = CONSTANTBV::BitVector_Div_Pos(q, copy, minBottom, r);
304 assert(e == CONSTANTBV::ErrCode_Ok);
305
306 if (CONSTANTBV::BitVector_Lexicompare(maxQuotient, q) > 0)
307 {
308 if (debug_division)
309 {
310 log << "2 maxQ) " << *maxTop;
311 log << " / " << *minBottom;
312 log << " = " << *q;
313 log << " r " << *r << endl;
314 }
315
316 CONSTANTBV::BitVector_Copy(maxQuotient,
317 q); // copy the reduced value in.
318 changed = true;
319 }
320
321 CONSTANTBV::BitVector_Copy(copy, maxQuotient);
322 e = CONSTANTBV::BitVector_Mul_Pos(multR, copy, maxBottom, true);
323 bool carry = false;
324 CONSTANTBV::BitVector_sub(copy, maxBottom, one, &carry);
325 CONSTANTBV::BitVector_add(copy2, multR, copy, &carry);
326 CONSTANTBV::BitVector_Copy(multR, copy2);
327 // involved. eek.
328
329 if (e == CONSTANTBV::ErrCode_Ok &&
330 CONSTANTBV::BitVector_Lexicompare(maxTop, multR) > 0)
331 {
332 if (debug_division)
333 {
334 log << "3 maxT) " << *maxQuotient;
335 log << " * " << *maxBottom;
336 log << " = " << *multR << endl;
337 }
338 CONSTANTBV::BitVector_Copy(maxTop, multR);
339 changed = true;
340 }
341
342 CONSTANTBV::BitVector_Copy(copy, minBottom);
343
344 // If this is strict then it seems to be treated as signed, so it is
345 // considered to overflow
346 // if a bit moves into the top of multR.
347 e = CONSTANTBV::BitVector_Mul_Pos(multR, copy, minQuotient, false);
348 // cerr << e << endl;
349
350 if (e == CONSTANTBV::ErrCode_Ok &&
351 CONSTANTBV::BitVector_Lexicompare(minTop, multR) < 0)
352 {
353 if (debug_division)
354 {
355 log << "4 minT) " << *minQuotient;
356 log << " * " << *minBottom;
357 log << " = " << *multR << endl;
358 }
359 CONSTANTBV::BitVector_Copy(minTop, multR);
360 changed = true;
361 }
362
363 if (CONSTANTBV::BitVector_Lexicompare(minQuotient, one) >= 0)
364 {
365 // not going to divide by zero.
366
367 CONSTANTBV::BitVector_Copy(copy, maxTop);
368 e = CONSTANTBV::BitVector_Div_Pos(q, copy, minQuotient, r);
369 assert(e == CONSTANTBV::ErrCode_Ok);
370
371 if (CONSTANTBV::BitVector_Lexicompare(maxBottom, q) > 0)
372 {
373 if (debug_division)
374 {
375 log << "5 maxB) " << *maxTop;
376 log << " / " << *minQuotient;
377 log << " = " << *q;
378 log << " r " << *r << endl;
379 }
380
381 // min quotient is bigger. Bring in.
382 CONSTANTBV::BitVector_Copy(maxBottom, q);
383 changed = true;
384 }
385 }
386
387 // This rule increases the minimum of the bottom.
388 // let a be the min of the top,
389 // let q be the maximum of the quotient,
390 // let b be the min. of the bottom.
391 // then a= bq +r
392 // so a = bq + (b-1) // if the max. of r is one less than b.
393 // so (1+a) / (q+1) = b.
394 // We round the division up.
395 {
396 bool carry = false;
397 CONSTANTBV::BitVector_add(copy, minTop, one, &carry);
398 bool carry2 = false;
399 CONSTANTBV::BitVector_add(copy2, maxQuotient, one, &carry2);
400 if (!carry && !carry2)
401 {
402 e = CONSTANTBV::BitVector_Div_Pos(q, copy, copy2, r);
403 assert(e == CONSTANTBV::ErrCode_Ok);
404 if (CONSTANTBV::BitVector_Lexicompare(q, one) >= 0)
405 {
406 CONSTANTBV::BitVector_add(copy, q, one, &carry);
407 if (!carry && (CONSTANTBV::BitVector_Lexicompare(minBottom, q) < 0))
408 {
409
410 if (debug_division)
411 {
412 log << "6 min_3_B) ";
413 log << "minBottom" << *minBottom << " ";
414 log << "q" << *q << endl;
415 }
416
417 // min quotient is bigger. Bring in.
418 CONSTANTBV::BitVector_Copy(minBottom, q);
419 changed = true;
420 }
421 }
422 }
423 }
424
425 // Don't know why we don't need to check the intervals on the others?
426 if (CONSTANTBV::BitVector_Lexicompare(minQuotient, maxQuotient) > 0)
427 {
428 if (debug_division)
429 {
430 log << "conflict" << endl;
431 log << "a:[" << *minTop << "," << *maxTop << "]";
432 log << " / b:[" << *minBottom << "," << *maxBottom << "] = ";
433 log << "[" << *minQuotient << "," << *maxQuotient << "]";
434 log << endl;
435 }
436
437 result = CONFLICT;
438 goto end;
439 }
440
441 if (debug_division)
442 {
443 log << "intermediate" << endl;
444 log << "a:[" << *minTop << "," << *maxTop << "]";
445 log << " / b:[" << *minBottom << "," << *maxBottom << "] = ";
446 log << "[" << *minQuotient << "," << *maxQuotient << "]";
447 log << endl;
448 }
449 iteration++;
450 // if (iteration==2 && changed)
451 // exit(1);
452 }
453
454 if (debug_division)
455 {
456 log << "final" << endl;
457 log << "a:[" << *minTop << "," << *maxTop << "]";
458 log << " / b:[" << *minBottom << "," << *maxBottom << "] = ";
459 log << "[" << *minQuotient << "," << *maxQuotient << "]";
460 log << endl;
461 }
462
463 {
464 Result r1 = fix(a, minTop, maxTop);
465 if (r1 == CHANGED)
466 r1 = merge(r1, fix(a, minTop, maxTop));
467
468 Result r2 = fix(b, minBottom, maxBottom);
469 if (r2 ==
470 CHANGED) // We call is a second time because it's not idepotent..
471 r2 = merge(r2, fix(b, minBottom, maxBottom));
472
473 Result r3;
474 if (whatIs == QUOTIENT_IS_OUTPUT)
475 {
476 r3 = fix(output, minQuotient, maxQuotient);
477 if (r3 == CHANGED)
478 r3 = merge(r3, fix(output, minQuotient, maxQuotient));
479 }
480 else
481 r3 = fix(output, minRemainder, maxRemainder);
482
483 if (r1 == CONFLICT || r2 == CONFLICT || r3 == CONFLICT)
484 {
485 result = CONFLICT;
486 goto end;
487 }
488 assert(result != CONFLICT);
489
490 if (r1 == CHANGED || r2 == CHANGED || r3 == CHANGED)
491 result = CHANGED;
492 }
493
494 // check that fixing bits hasn't tightened intervals. If it has we need to
495 // resolve.
496 if (result == CHANGED)
497 {
498 bool tightened = false;
499
500 setUnsignedMinMax(output, copy, copy2);
501
502 if (whatIs == QUOTIENT_IS_OUTPUT)
503 {
504 if (CONSTANTBV::BitVector_Lexicompare(minQuotient, copy) < 0 ||
505 CONSTANTBV::BitVector_Lexicompare(maxQuotient, copy2) > 0)
506 tightened = true;
507 }
508 else
509 {
510 if (CONSTANTBV::BitVector_Lexicompare(minRemainder, copy) < 0 ||
511 CONSTANTBV::BitVector_Lexicompare(maxRemainder, copy2) > 0)
512 tightened = true;
513 }
514
515 setUnsignedMinMax(b, copy, copy2);
516 if (CONSTANTBV::BitVector_Lexicompare(minBottom, copy) < 0 ||
517 CONSTANTBV::BitVector_Lexicompare(maxBottom, copy2) > 0)
518 tightened = true;
519
520 setUnsignedMinMax(a, copy, copy2);
521 if (CONSTANTBV::BitVector_Lexicompare(minTop, copy) < 0 ||
522 CONSTANTBV::BitVector_Lexicompare(maxTop, copy2) > 0)
523 tightened = true;
524
525 if (tightened)
526 {
527 setUnsignedMinMax(a, minTop, maxTop);
528 setUnsignedMinMax(b, minBottom, maxBottom);
529 if (whatIs == QUOTIENT_IS_OUTPUT)
530 setUnsignedMinMax(output, minQuotient, maxQuotient);
531 else
532 setUnsignedMinMax(output, minRemainder, maxRemainder);
533
534 bitEverChanged = true;
535 bitJustChanged = true;
536 }
537 }
538 }
539
540 end:
541 // Destroy range variables.
542 CONSTANTBV::BitVector_Destroy(minTop);
543 CONSTANTBV::BitVector_Destroy(maxTop);
544 CONSTANTBV::BitVector_Destroy(minBottom);
545 CONSTANTBV::BitVector_Destroy(maxBottom);
546 CONSTANTBV::BitVector_Destroy(minQuotient);
547 CONSTANTBV::BitVector_Destroy(maxQuotient);
548 CONSTANTBV::BitVector_Destroy(minRemainder);
549 CONSTANTBV::BitVector_Destroy(maxRemainder);
550
551 // Destroy helpers.
552 CONSTANTBV::BitVector_Destroy(copy);
553 CONSTANTBV::BitVector_Destroy(copy2);
554 CONSTANTBV::BitVector_Destroy(multR);
555 CONSTANTBV::BitVector_Destroy(q);
556 CONSTANTBV::BitVector_Destroy(r);
557 CONSTANTBV::BitVector_Destroy(one);
558 CONSTANTBV::BitVector_Destroy(max);
559
560 if (result == CONFLICT)
561 return CONFLICT;
562
563 if (bitEverChanged)
564 return CHANGED;
565 return result;
566 }
567
568 // (a/b) = q
569 // Solving: (a = q * b + r) AND (r < b).
bvUnsignedQuotientAndRemainder2(vector<FixedBits * > & children,FixedBits & output,STPMgr * bm,WhatIsOutput whatIs)570 Result bvUnsignedQuotientAndRemainder2(vector<FixedBits*>& children,
571 FixedBits& output, STPMgr* bm,
572 WhatIsOutput whatIs)
573 {
574 assert(output.getWidth() == children[0]->getWidth());
575 assert(output.getWidth() == children[1]->getWidth());
576 assert(children.size() == 2);
577
578 unsigned int newWidth = 2 * output.getWidth();
579 // Create Widenend copies.
580 FixedBits a(newWidth, false);
581 FixedBits b(newWidth, false);
582
583 FixedBits q(newWidth, false);
584 FixedBits r(newWidth, false);
585
586 // intermediate values.
587 FixedBits times(newWidth, false);
588
589 a.copyIn(*children[0]);
590 b.copyIn(*children[1]);
591
592 assert(!b.containsZero());
593
594 if (whatIs == QUOTIENT_IS_OUTPUT)
595 q.copyIn(output);
596 else if (whatIs == REMAINDER_IS_OUTPUT)
597 r.copyIn(output);
598 else
599 throw std::runtime_error("sdjjfas");
600
601 FixedBits aCopy(newWidth, false);
602 FixedBits bCopy(newWidth, false);
603 FixedBits rCopy(newWidth, false);
604 FixedBits qCopy(newWidth, false);
605
606 // Times and plus must not overflow.
607 for (unsigned i = (unsigned)output.getWidth(); i < newWidth; i++)
608 {
609 // No overflow.
610 times.setFixed(i, true);
611 times.setValue(i, false);
612
613 // Everything is zero extended.
614 a.setFixed(i, true);
615 a.setValue(i, false);
616 b.setFixed(i, true);
617 b.setValue(i, false);
618
619 // Multiplication must not overflow.
620 r.setFixed(i, true);
621 r.setValue(i, false);
622 q.setFixed(i, true);
623 q.setValue(i, false);
624 }
625
626 // True bit.
627 FixedBits trueBit(1, true);
628 trueBit.setFixed(0, true);
629 trueBit.setValue(0, true);
630
631 Result result = NO_CHANGE;
632
633 vector<FixedBits*> addChildren;
634 addChildren.push_back(×);
635 addChildren.push_back(&r);
636
637 vector<FixedBits*> multiplicationChildren;
638 multiplicationChildren.push_back(&q);
639 multiplicationChildren.push_back(&b);
640
641 do
642 {
643 aCopy = a;
644 bCopy = b;
645 rCopy = r;
646 qCopy = q;
647
648 if (debug_division)
649 {
650 log << "p1:" << a << "/" << b << "=" << q << "rem(" << r << ")" << endl;
651 log << "times" << times << endl;
652 }
653
654 result = bvLessThanBothWays(r, b, trueBit); // (r < b)
655 if (result == CONFLICT)
656 return CONFLICT;
657
658 result = bvMultiplyBothWays(multiplicationChildren, times, bm);
659 if (result == CONFLICT)
660 return CONFLICT;
661
662 result = bvAddBothWays(addChildren, a);
663 if (result == CONFLICT)
664 return CONFLICT;
665 } while (!(FixedBits::equals(aCopy, a) && FixedBits::equals(bCopy, b) &&
666 FixedBits::equals(rCopy, r) && FixedBits::equals(qCopy, q)));
667
668 bool conflict = false;
669 for (unsigned i = 0; i < output.getWidth(); i++)
670 {
671 if (whatIs == QUOTIENT_IS_OUTPUT)
672 conflict |= fix(output, q, i);
673 else if (whatIs == REMAINDER_IS_OUTPUT)
674 conflict |= fix(output, r, i);
675 else
676 throw std::runtime_error("sdjjfas");
677
678 conflict |= fix(*children[0], a, i);
679 conflict |= fix(*children[1], b, i);
680 }
681
682 if (debug_division)
683 cerr << endl;
684
685 if (conflict)
686 return CONFLICT;
687
688 return NOT_IMPLEMENTED;
689 }
690
bvUnsignedModulusBothWays(vector<FixedBits * > & children,FixedBits & output,STPMgr * bm)691 Result bvUnsignedModulusBothWays(vector<FixedBits*>& children,
692 FixedBits& output, STPMgr* bm)
693 {
694
695 Result r1 = NO_CHANGE;
696 vector<FixedBits*> v;
697 v.push_back(&output);
698 v.push_back(children[0]);
699 FixedBits truN(1, true);
700 truN.setFixed(0, true);
701 truN.setValue(0, true);
702 r1 = bvLessThanEqualsBothWays(v, truN);
703
704 if (children[1]->containsZero())
705 return r1;
706
707 if (debug_division)
708 log << *(children[0]) << "bvmod" << *(children[1]) << "=" << output << endl;
709
710 Result r =
711 bvUnsignedQuotientAndRemainder(children, output, bm, REMAINDER_IS_OUTPUT);
712
713 // Doesn't even do constant propagation.
714 // <10>bvmod<11>=<-->
715 if (r != CONFLICT && children[0]->isTotallyFixed() &&
716 children[1]->isTotallyFixed() && !output.isTotallyFixed())
717 {
718
719 if (debug_division)
720 {
721 log << "Not even constant prop!" << *(children[0]) << "bvmod"
722 << *(children[1]) << "=" << output << endl;
723 }
724
725 // assert(output.isTotallyFixed());
726 }
727
728 if (r == CONFLICT || r == CHANGED)
729 return r;
730
731 return r1;
732 }
733
bvUnsignedDivisionBothWays(vector<FixedBits * > & children,FixedBits & output,STPMgr * bm)734 Result bvUnsignedDivisionBothWays(vector<FixedBits*>& children,
735 FixedBits& output, STPMgr* bm)
736 {
737 Result r0 = NO_CHANGE;
738
739 if (children[1]->containsZero())
740 return r0; // TODO fix so we learn something if we might be dividing by zero..
741
742 // Enforce that the output must be less than the numerator.
743 for (int i = children[0]->getWidth() - 1; i >= 0; i--)
744 {
745 if (children[0]->isFixedToZero(i))
746 {
747 if (output.isFixedToOne(i))
748 return CONFLICT;
749 else if (!output.isFixed(i))
750 {
751 output.setFixed(i, true);
752 output.setValue(i, false);
753 r0 = CHANGED;
754 }
755 }
756 else
757 {
758 break;
759 }
760 }
761
762 Result r =
763 bvUnsignedQuotientAndRemainder(children, output, bm, QUOTIENT_IS_OUTPUT);
764
765 return merge(r0, r);
766 }
767
canBe(const FixedBits & b,int index,bool value)768 bool canBe(const FixedBits& b, int index, bool value)
769 {
770 if (!b.isFixed(index))
771 return true;
772 else
773 return (!(b.getValue(index) ^ value));
774 }
775
776 // This provides a way to call the process function with fewer arguments.
777 struct Data
778 {
779 FixedBits& tempA;
780 FixedBits& tempB;
781 FixedBits& tempOutput;
782 FixedBits& workingA;
783 FixedBits& workingB;
784 FixedBits& workingOutput;
785 unsigned int signBit;
786
Datasimplifier::constantBitP::Data787 Data(FixedBits& _tempA, FixedBits& _tempB, FixedBits& _tempOutput,
788 FixedBits& _workingA, FixedBits& _workingB, FixedBits& _workingOutput)
789 : tempA(_tempA), tempB(_tempB), tempOutput(_tempOutput),
790 workingA(_workingA), workingB(_workingB), workingOutput(_workingOutput)
791 {
792 signBit = tempOutput.getWidth() - 1;
793 }
794
processsimplifier::constantBitP::Data795 void process(bool& first)
796 {
797 if (first)
798 {
799 workingA = tempA;
800 workingB = tempB;
801 workingOutput = tempOutput;
802 }
803 else
804 {
805 workingA = FixedBits::meet(workingA, tempA);
806 workingB = FixedBits::meet(workingB, tempB);
807 workingOutput = FixedBits::meet(workingOutput, tempOutput);
808 }
809 first = false;
810 }
811
setsimplifier::constantBitP::Data812 void set(const FixedBits& a, const FixedBits& b, const FixedBits& output,
813 bool aTop, bool bTop)
814 {
815 tempA = a;
816 tempB = b;
817 tempOutput = output;
818 tempA.setFixed(signBit, true);
819 tempA.setValue(signBit, aTop);
820
821 tempB.setFixed(signBit, true);
822 tempB.setValue(signBit, bTop);
823 }
824
printsimplifier::constantBitP::Data825 void print()
826 {
827 cerr << "Working: ";
828 cerr << workingA << "/";
829 cerr << workingB << "=";
830 cerr << workingOutput << endl;
831
832 cerr << "Temps: ";
833 cerr << tempA << "/";
834 cerr << tempB << "=";
835 cerr << tempOutput << endl;
836 }
837 };
838
negate(FixedBits & input,FixedBits & output)839 Result negate(FixedBits& input, FixedBits& output)
840 {
841 vector<FixedBits*> negChildren;
842
843 negChildren.push_back(&input);
844 return bvUnaryMinusBothWays(negChildren, output);
845 }
846
847 // This is preposterously complicated. We execute four cases then take the union
848 // of them.
849 //
bvSignedDivisionRemainderBothWays(vector<FixedBits * > & children,FixedBits & output,STPMgr * bm,Result (* tf)(vector<FixedBits * > &,FixedBits &,STPMgr * bm),const Operation op)850 Result bvSignedDivisionRemainderBothWays(vector<FixedBits*>& children,
851 FixedBits& output, STPMgr* bm,
852 Result (*tf)(vector<FixedBits*>&,
853 FixedBits&, STPMgr* bm),
854 const Operation op)
855 {
856 assert(output.getWidth() == children[0]->getWidth());
857 assert(output.getWidth() == children[1]->getWidth());
858 assert(children.size() == 2);
859
860 const FixedBits& a = *children[0];
861 const FixedBits& b = *children[1];
862
863 assert(&a != &b);
864
865 const unsigned int inputWidth = output.getWidth();
866 const unsigned int signBit = output.getWidth() - 1;
867
868 FixedBits workingA(inputWidth, false);
869 FixedBits workingB(inputWidth, false);
870 FixedBits workingOutput(inputWidth, false);
871
872 FixedBits tempA = a;
873 FixedBits tempB = b;
874 FixedBits tempOutput = output;
875
876 vector<FixedBits*> tempChildren;
877 tempChildren.push_back(&tempA);
878 tempChildren.push_back(&tempB);
879 Result r = NO_CHANGE;
880
881 if (b.containsZero())
882 return NO_CHANGE;
883
884 Data data(tempA, tempB, tempOutput, workingA, workingB, workingOutput);
885
886 while (true)
887 {
888 if (debug_division)
889 {
890 cerr << "start:";
891 cerr << a << "/";
892 cerr << b << "=";
893 cerr << output << endl;
894 }
895
896 bool first = true;
897
898 if (canBe(a, signBit, false) && canBe(b, signBit, false))
899 {
900 // (bvudiv s t)
901 r = NO_CHANGE;
902 data.set(a, b, output, false, false);
903
904 r = tf(tempChildren, tempOutput, bm);
905 if (r != CONFLICT)
906 {
907 if (debug_division)
908 cerr << "case A" << endl;
909 data.process(first);
910 }
911 }
912
913 if (canBe(a, signBit, true) && canBe(b, signBit, false))
914 {
915 // (bvneg (bvudiv (bvneg a) b))
916 r = NO_CHANGE;
917 data.set(a, b, output, true, false);
918
919 FixedBits negA(inputWidth, false);
920
921 vector<FixedBits*> negChildren;
922 negChildren.push_back(&negA);
923 r = bvUnaryMinusBothWays(negChildren, tempA); // get NegA
924 // cerr << negA << " " << tempA << endl;
925 assert(r != CONFLICT);
926
927 // modulus: (bvadd (bvneg (bvurem (bvneg s) t)) t)
928 FixedBits wO(inputWidth, false);
929 if (op == SIGNED_MODULUS)
930 {
931 vector<FixedBits*> ch;
932 ch.push_back(&wO);
933 ch.push_back(&tempB);
934 r = bvAddBothWays(ch, tempOutput);
935 assert(r != CONFLICT);
936 }
937 else
938 wO = tempOutput;
939
940 FixedBits negOutput(inputWidth, false);
941 negChildren.clear();
942 negChildren.push_back(&negOutput);
943 r = bvUnaryMinusBothWays(negChildren, wO);
944 assert(r != CONFLICT);
945
946 negChildren.clear();
947 negChildren.push_back(&negA);
948 negChildren.push_back(&tempB);
949
950 r = tf(negChildren, negOutput, bm);
951 if (r != CONFLICT)
952 {
953 negChildren.clear();
954 negChildren.push_back(&wO);
955 r = bvUnaryMinusBothWays(negChildren, negOutput);
956
957 if (r != CONFLICT)
958 {
959 if (op == SIGNED_MODULUS)
960 {
961 vector<FixedBits*> ch;
962 ch.push_back(&wO);
963 ch.push_back(&tempB);
964 r = bvAddBothWays(ch, tempOutput);
965 }
966 else
967 tempOutput = wO;
968
969 if (r != CONFLICT)
970 {
971 negChildren.clear();
972 negChildren.push_back(&tempA);
973 // cerr << negA << " " << tempA << endl;
974 r = bvUnaryMinusBothWays(negChildren, negA);
975 // data.print();
976 if (r != CONFLICT)
977 {
978
979 if (debug_division)
980 cerr << "case B" << endl;
981
982 data.process(first);
983 }
984 }
985 }
986 }
987 }
988
989 if (canBe(a, signBit, false) && canBe(b, signBit, true))
990 {
991 // (bvneg (bvudiv a (bvneg b)))
992 r = NO_CHANGE;
993 data.set(a, b, output, false, true);
994
995 FixedBits negB(inputWidth, false);
996 // FixedBits negA(inputWidth, false);
997
998 vector<FixedBits*> negChildren;
999 negChildren.push_back(&negB);
1000 r = bvUnaryMinusBothWays(negChildren, tempB); // get NegB
1001 assert(r != CONFLICT);
1002
1003 // Create a negated version of the output if necessary. Modulus and
1004 // remainder aren't both negated. Division is.
1005 FixedBits wO(inputWidth, false);
1006 if (op == SIGNED_DIVISION)
1007 {
1008 r = negate(tempOutput, wO);
1009 assert(r != CONFLICT);
1010 }
1011 else if (op == SIGNED_REMAINDER || op == SIGNED_MODULUS)
1012 wO = tempOutput;
1013
1014 // (bvadd (bvurem s (bvneg t)) t)
1015 if (op == SIGNED_MODULUS)
1016 {
1017 FixedBits wTemp(inputWidth, false);
1018 vector<FixedBits*> ch;
1019 ch.push_back(&wTemp);
1020 ch.push_back(&tempB);
1021 r = bvAddBothWays(ch, tempOutput);
1022 assert(r != CONFLICT);
1023 wO = wTemp;
1024 }
1025
1026 negChildren.clear();
1027 negChildren.push_back(&tempA);
1028 negChildren.push_back(&negB);
1029
1030 r = tf(negChildren, wO, bm);
1031 if (r != CONFLICT)
1032 {
1033 FixedBits t(wO.getWidth(), false);
1034 if (op == SIGNED_MODULUS)
1035 {
1036 vector<FixedBits*> ch;
1037 ch.push_back(&wO);
1038 ch.push_back(&tempB);
1039 r = bvAddBothWays(ch, tempOutput);
1040 t = tempOutput;
1041 }
1042 else
1043 t = wO;
1044
1045 if (r != CONFLICT)
1046 {
1047 if (op == SIGNED_DIVISION)
1048 {
1049 r = negate(tempOutput, t);
1050 }
1051 else if (op == SIGNED_REMAINDER || op == SIGNED_MODULUS)
1052 {
1053 tempOutput = t;
1054 }
1055
1056 if (r != CONFLICT)
1057 {
1058 negChildren.clear();
1059 negChildren.push_back(&tempB);
1060 r = bvUnaryMinusBothWays(negChildren, negB);
1061 if (r != CONFLICT)
1062 {
1063 if (debug_division)
1064 cerr << "case C" << endl;
1065
1066 data.process(first);
1067 }
1068 }
1069 }
1070 }
1071 }
1072
1073 if (canBe(a, signBit, true) && canBe(b, signBit, true))
1074 {
1075 // (bvudiv (bvneg a) (bvneg b)))))))
1076 r = NO_CHANGE;
1077 data.set(a, b, output, true, true);
1078
1079 FixedBits negA(inputWidth, false);
1080 FixedBits negB(inputWidth, false);
1081
1082 vector<FixedBits*> negChildren;
1083 negChildren.push_back(&negA);
1084 r = bvUnaryMinusBothWays(negChildren, tempA); // get NegA
1085 assert(r != CONFLICT);
1086
1087 negChildren.clear();
1088 negChildren.push_back(&negB);
1089 r = bvUnaryMinusBothWays(negChildren, tempB); // get NegB
1090 assert(r != CONFLICT);
1091
1092 negChildren.clear();
1093 negChildren.push_back(&negA);
1094 negChildren.push_back(&negB);
1095
1096 FixedBits wO(inputWidth, false);
1097 if (op == SIGNED_REMAINDER || op == SIGNED_MODULUS)
1098 {
1099 r = negate(tempOutput, wO);
1100 assert(r != CONFLICT);
1101 }
1102 else if (op == SIGNED_DIVISION)
1103 wO = tempOutput;
1104
1105 r = tf(negChildren, wO, bm);
1106 if (r != CONFLICT)
1107 {
1108 negChildren.clear();
1109 negChildren.push_back(&tempB);
1110 r = bvUnaryMinusBothWays(negChildren, negB);
1111
1112 if (r != CONFLICT)
1113 {
1114 negChildren.clear();
1115 negChildren.push_back(&tempA);
1116 r = bvUnaryMinusBothWays(negChildren, negA);
1117 // data.print();
1118 if (r != CONFLICT)
1119 {
1120 if (op == SIGNED_REMAINDER || op == SIGNED_MODULUS)
1121 {
1122 r = negate(tempOutput, wO);
1123 }
1124 else if (op == SIGNED_DIVISION)
1125 tempOutput = wO;
1126
1127 if (r != CONFLICT)
1128 {
1129 if (debug_division)
1130 cerr << "case D" << endl;
1131
1132 data.process(first);
1133 }
1134 }
1135 }
1136 }
1137 }
1138
1139 if (first)
1140 return CONFLICT; // All are conflicts.
1141
1142 // The results be subsets of the originals.
1143 assert(FixedBits::in(workingA, *children[0]));
1144 assert(FixedBits::in(workingB, *children[1]));
1145 assert(FixedBits::in(workingOutput, output));
1146
1147 if (FixedBits::equals(a, workingA) && FixedBits::equals(b, workingB) &&
1148 FixedBits::equals(output, workingOutput))
1149 break;
1150 else
1151 {
1152 *children[0] = workingA;
1153 *children[1] = workingB;
1154 output = workingOutput;
1155 }
1156 }
1157
1158 return NOT_IMPLEMENTED;
1159 }
1160
bvSignedModulusBothWays(vector<FixedBits * > & children,FixedBits & output,STPMgr * bm)1161 Result bvSignedModulusBothWays(vector<FixedBits*>& children, FixedBits& output,
1162 STPMgr* bm)
1163 {
1164 /*
1165 (bvsmod s t) abbreviates
1166 (let (?msb_s (extract[|m-1|:|m-1|] s))
1167 (let (?msb_t (extract[|m-1|:|m-1|] t))
1168 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
1169 (bvurem s t)
1170 (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
1171 (bvadd (bvneg (bvurem (bvneg s) t)) t)
1172 (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
1173 (bvadd (bvurem s (bvneg t)) t)
1174 (bvneg (bvurem (bvneg s) (bvneg t)))))))
1175 */
1176
1177 // I think this implements old style (broken) semantics, so avoiding it.
1178 return NO_CHANGE;
1179
1180 if (children[0] == children[1]) // same pointer.
1181 {
1182 return NO_CHANGE;
1183 }
1184
1185 return bvSignedDivisionRemainderBothWays(
1186 children, output, bm, bvUnsignedModulusBothWays, SIGNED_MODULUS);
1187 }
1188
bvSignedRemainderBothWays(vector<FixedBits * > & children,FixedBits & output,STPMgr * bm)1189 Result bvSignedRemainderBothWays(vector<FixedBits*>& children,
1190 FixedBits& output, STPMgr* bm)
1191 {
1192 /*
1193 (bvsrem s t) abbreviates
1194 (let (?msb_s (extract[|m-1|:|m-1|] s))
1195 (let (?msb_t (extract[|m-1|:|m-1|] t))
1196 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
1197 (bvurem s t)
1198 (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
1199 (bvneg (bvurem (bvneg s) t))
1200 (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
1201 (bvurem s (bvneg t)))
1202 (bvneg (bvurem (bvneg s) (bvneg t)))))))
1203 */
1204
1205 if (children[0] == children[1]) // same pointer.
1206 {
1207 return NO_CHANGE;
1208 }
1209
1210 return bvSignedDivisionRemainderBothWays(
1211 children, output, bm, bvUnsignedModulusBothWays, SIGNED_REMAINDER);
1212 }
1213
bvSignedDivisionBothWays(vector<FixedBits * > & children,FixedBits & output,STPMgr * bm)1214 Result bvSignedDivisionBothWays(vector<FixedBits*>& children, FixedBits& output,
1215 STPMgr* bm)
1216 {
1217 /*
1218 * (bvsdiv s t) abbreviates
1219 (let (?msb_s (extract[|m-1|:|m-1|] s))
1220 (let (?msb_t (extract[|m-1|:|m-1|] t))
1221 (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
1222 (bvudiv s t)
1223 (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
1224 (bvneg (bvudiv (bvneg s) t))
1225 (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
1226 (bvneg (bvudiv s (bvneg t)))
1227 (bvudiv (bvneg s) (bvneg t)))))))
1228 *
1229 */
1230
1231 if (children[0] == children[1]) // same pointer.
1232 {
1233 return NO_CHANGE;
1234 }
1235
1236 // unsigned division propagates much better than signed division does!
1237 const int top = children[0]->getWidth();
1238 if ((*children[0])[top - 1] == '0' && (*children[1])[top - 1] == '0')
1239 return bvUnsignedDivisionBothWays(children, output, bm);
1240 else
1241 return bvSignedDivisionRemainderBothWays(
1242 children, output, bm, bvUnsignedDivisionBothWays, SIGNED_DIVISION);
1243 }
1244 }
1245 }
1246