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(&times);
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