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/Simplifier/constantBitP/ConstantBitP_TransferFunctions.h"
26 #include "stp/Simplifier/constantBitP/ConstantBitP_Utility.h"
27 // FIXME: External library
28 #include "extlib-constbv/constantbv.h"
29
30 // Left shift, right shift.
31 // Trevor Hansen. BSD License.
32
33 // smtlib & x86 semantics differ for what happens when a value is shifted by
34 // greater
35 // than the bitWidth. On x86, in 64-bit mode, only the bottom 6 bits of the
36 // shift are
37 // used. In SMTLIB the total value is used.
38
39 namespace simplifier
40 {
41 namespace constantBitP
42 {
43
44 const bool debug_shift = false;
45
bvRightShiftBothWays(vector<FixedBits * > & children,FixedBits & output)46 Result bvRightShiftBothWays(vector<FixedBits*>& children, FixedBits& output)
47 {
48 Result result = NO_CHANGE;
49 const unsigned bitWidth = output.getWidth();
50
51 assert(2 == children.size());
52
53 FixedBits& op = *children[0];
54 FixedBits& shift = *children[1];
55
56 FixedBits outputReverse(bitWidth, false);
57 FixedBits opReverse(bitWidth, false);
58
59 // Reverse the output and the input.
60 for (unsigned i = 0; i < bitWidth; i++)
61 {
62 if (op.isFixed(i))
63 {
64 opReverse.setFixed(bitWidth - 1 - i, true);
65 opReverse.setValue(bitWidth - 1 - i, op.getValue(i));
66 }
67
68 if (output.isFixed(i))
69 {
70 outputReverse.setFixed(bitWidth - 1 - i, true);
71 outputReverse.setValue(bitWidth - 1 - i, output.getValue(i));
72 }
73 }
74
75 vector<FixedBits*> args;
76 args.push_back(&opReverse);
77 args.push_back(&shift); // shift is unmodified.
78 result = bvLeftShiftBothWays(args, outputReverse);
79
80 if (CONFLICT == result)
81 return CONFLICT;
82
83 // Now write the reversed values back.
84 // Reverse the output and the input.
85 for (unsigned i = 0; i < bitWidth; i++)
86 {
87 if (opReverse.isFixed(i) && !op.isFixed(bitWidth - 1 - i))
88 {
89 op.setFixed(bitWidth - 1 - i, true);
90 op.setValue(bitWidth - 1 - i, opReverse.getValue(i));
91 }
92
93 if (outputReverse.isFixed(i) && !output.isFixed(bitWidth - 1 - i))
94 {
95 output.setFixed(bitWidth - 1 - i, true);
96 output.setValue(bitWidth - 1 - i, outputReverse.getValue(i));
97 }
98 }
99
100 return result;
101 }
102
103 // Converts the array of possible shifts into a set that represents the values.
getPossible(unsigned bitWidth,bool possibleShift[],unsigned numberOfPossibleShifts,const FixedBits & shift)104 FixedBits getPossible(unsigned bitWidth, bool possibleShift[],
105 unsigned numberOfPossibleShifts, const FixedBits& shift)
106 {
107 FixedBits v(bitWidth, false);
108 bool first = true;
109 for (unsigned i = 0; i < numberOfPossibleShifts - 1; i++)
110 {
111 if (possibleShift[i])
112 {
113 if (first)
114 {
115 first = false;
116 for (unsigned j = 0; j < (unsigned)v.getWidth(); j++)
117 {
118 v.setFixed(j, true);
119 if (j < sizeof(unsigned) * 8)
120 v.setValue(j, 0 != (i & (1 << j)));
121 else
122 v.setValue(j, false);
123 }
124 }
125 else
126 {
127 // join.
128 for (unsigned j = 0;
129 j < (unsigned)v.getWidth() && j < sizeof(unsigned) * 8; j++)
130 {
131 if (v.isFixed(j))
132 {
133 // union.
134 if (v.getValue(j) != (0 != (i & (1 << j))))
135 v.setFixed(j, false);
136 }
137 }
138 }
139 }
140 }
141
142 unsigned firstShift;
143 for (firstShift = 0; firstShift < numberOfPossibleShifts; firstShift++)
144 if (possibleShift[firstShift])
145 break;
146
147 // The top most entry of the shift table is special. It means all values of
148 // shift
149 // that fill it completely with zeroes /ones. We take the union of all of the
150 // values >bitWidth
151 // in this function.
152 if (possibleShift[numberOfPossibleShifts - 1])
153 {
154 FixedBits bitWidthFB = FixedBits::fromUnsignedInt(bitWidth, bitWidth);
155 FixedBits output(1, true);
156 output.setFixed(0, true);
157 output.setValue(0, true);
158 FixedBits working(shift);
159
160 vector<FixedBits*> args;
161 args.push_back(&working);
162 args.push_back(&bitWidthFB);
163
164 // Write into working anything that can be determined given it's >=bitWidth.
165 Result r = bvGreaterThanEqualsBothWays(args, output);
166 assert(CONFLICT != r);
167
168 // Get the union of "working" with the prior union.
169 for (unsigned i = 0; i < bitWidth; i++)
170 {
171 if (!working.isFixed(i) && v.isFixed(i))
172 v.setFixed(i, false);
173 if (working.isFixed(i) && v.isFixed(i) &&
174 (working.getValue(i) != v.getValue(i)))
175 v.setFixed(i, false);
176 if (firstShift == numberOfPossibleShifts - 1) // no less shifts possible.
177 {
178 if (working.isFixed(i))
179 {
180 v.setFixed(i, true);
181 v.setValue(i, working.getValue(i));
182 }
183 }
184 }
185 }
186
187 if (debug_shift)
188 cerr << "Set of possible shifts:" << v << endl;
189
190 return v;
191 }
192
getMaxShiftFromValueViaAlternation(const unsigned bitWidth,const FixedBits & output)193 unsigned getMaxShiftFromValueViaAlternation(const unsigned bitWidth,
194 const FixedBits& output)
195 {
196 unsigned maxShiftFromValue = UINT_MAX;
197
198 // The shift must be less than the position of the first alternation.
199 bool foundTrue = false;
200 bool foundFalse = false;
201 for (int i = bitWidth - 1; i >= 0; i--)
202 {
203 if (output.isFixed(i))
204 {
205 if (output.getValue(i) && foundFalse)
206 {
207 maxShiftFromValue = i;
208 break;
209 }
210 if (!output.getValue(i) && foundTrue)
211 {
212 maxShiftFromValue = i;
213 break;
214 }
215 if (output.getValue(i))
216 foundTrue = true;
217 else if (!output.getValue(i))
218 foundFalse = true;
219 }
220 }
221
222 if (maxShiftFromValue != UINT_MAX)
223 maxShiftFromValue = bitWidth - 2 - maxShiftFromValue;
224
225 return maxShiftFromValue;
226 }
227
bvArithmeticRightShiftBothWays(vector<FixedBits * > & children,FixedBits & output)228 Result bvArithmeticRightShiftBothWays(vector<FixedBits*>& children,
229 FixedBits& output)
230 {
231 const unsigned bitWidth = output.getWidth();
232 assert(2 == children.size());
233 assert(bitWidth > 0);
234 assert(children[0]->getWidth() == children[1]->getWidth());
235 const unsigned MSBIndex = bitWidth - 1;
236
237 FixedBits& op = *children[0];
238 FixedBits& shift = *children[1];
239
240 // If the MSB isn't set, create a copy with it set each way and take the meet.
241 if (!op.isFixed(MSBIndex))
242 {
243 vector<FixedBits*> children1;
244 vector<FixedBits*> children2;
245 FixedBits op1(op);
246 FixedBits op2(op);
247 FixedBits shift1(shift);
248 FixedBits shift2(shift);
249 FixedBits output1(output);
250 FixedBits output2(output);
251
252 children1.push_back(&op1);
253 children1.push_back(&shift1);
254 op1.setFixed(MSBIndex, true);
255 op1.setValue(MSBIndex, true);
256
257 children2.push_back(&op2);
258 children2.push_back(&shift2);
259 op2.setFixed(MSBIndex, true);
260 op2.setValue(MSBIndex, false);
261
262 Result r1 = bvArithmeticRightShiftBothWays(children1, output1);
263 Result r2 = bvArithmeticRightShiftBothWays(children2, output2);
264
265 if (r1 == CONFLICT && r2 == CONFLICT)
266 return CONFLICT;
267
268 if (r1 == CONFLICT)
269 {
270 op = op2;
271 shift = shift2;
272 output = output2;
273 return r2;
274 }
275
276 if (r2 == CONFLICT)
277 {
278 op = op1;
279 shift = shift1;
280 output = output1;
281 return r1;
282 }
283
284 op = FixedBits::meet(op1, op2);
285 shift = FixedBits::meet(shift1, shift2);
286 output = FixedBits::meet(output1, output2);
287 return r1;
288 }
289
290 assert(op.isFixed(MSBIndex));
291
292 if (debug_shift)
293 {
294 cerr << "=========" << endl;
295 cerr << op << " >a> ";
296 cerr << shift;
297 cerr << " = " << output << endl;
298 }
299
300 // The topmost number of possible shifts corresponds to all
301 // the values of shift that shift out everything.
302 // i.e. possibleShift[bitWidth+1] is the SET of all operations that shift past
303 // the end.
304 const unsigned numberOfPossibleShifts = bitWidth + 1;
305 bool* possibleShift = (bool*)alloca(sizeof(bool) * numberOfPossibleShifts);
306 for (unsigned i = 0; i < numberOfPossibleShifts; i++)
307 possibleShift[i] = false;
308
309 // If either of the top two bits are fixed they should be equal.
310 if (op.isFixed(MSBIndex) ^ output.isFixed(MSBIndex))
311 {
312 if (op.isFixed(MSBIndex))
313 {
314 output.setFixed(MSBIndex, true);
315 output.setValue(MSBIndex, op.getValue(MSBIndex));
316 }
317
318 if (output.isFixed(MSBIndex))
319 {
320 op.setFixed(MSBIndex, true);
321 op.setValue(MSBIndex, output.getValue(MSBIndex));
322 }
323 }
324
325 // Both the MSB of the operand and the output should be fixed now..
326 assert(output.isFixed(MSBIndex));
327
328 unsigned minShiftFromShift,
329 maxShiftFromShift; // The range of the "shift" value.
330 shift.getUnsignedMinMax(minShiftFromShift, maxShiftFromShift);
331
332 // The shift can't be any bigger than the topmost alternation in the output.
333 // For example if the output is 0.01000, then the shift can not be bigger than
334 // 3.
335 unsigned maxShiftFromOutput =
336 getMaxShiftFromValueViaAlternation(bitWidth, output);
337
338 maxShiftFromShift = std::min(maxShiftFromShift, (unsigned)maxShiftFromOutput);
339
340 if (debug_shift)
341 {
342 cerr << "minshift:" << minShiftFromShift << endl;
343 cerr << "maxshift:" << maxShiftFromShift << endl;
344 cerr << "total:" << maxShiftFromShift << endl;
345 }
346
347 for (unsigned i = minShiftFromShift;
348 i <= std::min(bitWidth, maxShiftFromShift); i++)
349 {
350 // if the bit-pattern of 'i' is in the set represented by the 'shift'.
351 if (shift.unsignedHolds(i))
352 possibleShift[i] = true;
353 }
354
355 // Complication. Given a shift like [.1] possibleShift[2] is now false.
356 // A shift of 2 isn't possible. But one of three is.
357 // possibleShift[2] means any shift >=2 is possible. So it needs to be set
358 // to true.
359 {
360 if (maxShiftFromShift >= bitWidth)
361 possibleShift[bitWidth] = true;
362 }
363
364 // Now check one-by-one each shifting.
365 // If we are shifting a zero to where a one is (say), then that shifting isn't
366 // possible.
367 for (unsigned shiftIt = minShiftFromShift; shiftIt < numberOfPossibleShifts;
368 shiftIt++)
369 {
370 if (possibleShift[shiftIt])
371 {
372 for (unsigned column = 0; column < bitWidth; column++)
373 {
374 // if they are fixed to different values. That's wrong.
375 if (column + shiftIt <= bitWidth - 1)
376 {
377 if (output.isFixed(column) && op.isFixed(column + shiftIt) &&
378 (output.getValue(column) != op.getValue(column + shiftIt)))
379 {
380 possibleShift[shiftIt] = false;
381 break;
382 }
383 }
384 }
385 }
386 }
387
388 int nOfPossibleShifts = 0;
389 for (unsigned i = 0; i < numberOfPossibleShifts; i++)
390 {
391 if (possibleShift[i])
392 {
393 nOfPossibleShifts++;
394 maxShiftFromShift = i;
395 if (debug_shift)
396 {
397 std::cerr << "Possible Shift:" << i << std::endl;
398 }
399 }
400 }
401
402 if (debug_shift)
403 {
404 std::cerr << "Number of possible shifts:" << nOfPossibleShifts << endl;
405 }
406
407 // If it's empty. It's a conflict.
408 if (0 == nOfPossibleShifts)
409 {
410 return CONFLICT;
411 }
412
413 // We have a list of all the possible shift amounts.
414 // We take the union of all the bits that are possible.
415 FixedBits setOfPossibleShifts =
416 getPossible(bitWidth, possibleShift, numberOfPossibleShifts, shift);
417
418 // Write in any fixed values to the shift.
419 for (unsigned i = 0; i < bitWidth; i++)
420 {
421 if (setOfPossibleShifts.isFixed(i))
422 {
423 if (!shift.isFixed(i))
424 {
425 shift.setFixed(i, true);
426 shift.setValue(i, setOfPossibleShifts.getValue(i));
427 }
428 else if (shift.isFixed(i) &&
429 shift.getValue(i) != setOfPossibleShifts.getValue(i))
430 {
431 return CONFLICT;
432 }
433 }
434 }
435
436 // If a particular input bit appears in every possible shifting,
437 // and if that bit is unfixed,
438 // and if the result it is fixed to the same value in every position.
439 // Then, that bit must be fixed.
440 // E.g. [--] << [0-] == [00]
441
442 bool* candidates = (bool*)alloca(sizeof(bool) * bitWidth);
443 for (unsigned i = 0; i < bitWidth; i++)
444 {
445 candidates[i] = !op.isFixed(i);
446 }
447
448 // candidates: So far: the bits that are unfixed in the operand.
449
450 for (unsigned i = 0; i < numberOfPossibleShifts; i++)
451 {
452 if (possibleShift[i])
453 {
454 // If this shift is possible, then some bits will be shifted out.
455 for (unsigned j = 0; j < i; j++)
456 candidates[j] = false;
457 }
458 }
459
460 // candidates: So far: + the input bits that are unfixed.
461 // + the input bits that are in every possible fixing.
462
463 // Check all candidates have the same output values.
464 for (unsigned candidate = 0; candidate < bitWidth; candidate++)
465 {
466 bool setTo = false; // value that's never read. To quieten gcc.
467
468 if (candidates[candidate])
469 {
470 bool first = true;
471 for (unsigned shiftIT = 0; shiftIT < bitWidth; shiftIT++)
472 {
473 // If the shift isn't possible continue.
474 if (!possibleShift[shiftIT])
475 continue;
476
477 if (shiftIT > candidate)
478 continue;
479
480 unsigned idx = candidate - shiftIT;
481
482 if (!output.isFixed(idx))
483 {
484 candidates[candidate] = false;
485 break;
486 }
487 else
488 {
489 if (first)
490 {
491 first = false;
492 setTo = output.getValue(idx);
493 }
494 else
495 {
496 if (setTo != output.getValue(idx))
497 {
498 candidates[candidate] = false;
499 break;
500 }
501 }
502 }
503 }
504 }
505
506 if (candidates[candidate])
507 {
508 assert(!op.isFixed(candidate));
509 op.setFixed(candidate, true);
510 op.setValue(candidate, setTo);
511 }
512 }
513
514 if (debug_shift)
515 {
516 cerr << op << " >a> ";
517 cerr << shift;
518 cerr << " = " << output << endl;
519 }
520
521 // Go through each of the possible shifts. If the same value is fixed
522 // at every location. Then it's fixed too in the result.
523 // Looping over the output columns.
524 bool MSBValue = op.getValue(MSBIndex);
525
526 for (unsigned column = 0; column < bitWidth; column++)
527 {
528 bool allFixedToSame = true;
529 bool allFixedTo = false; // value that's never read. To quieten gcc.
530 bool first = true;
531
532 for (unsigned shiftIt = 0;
533 (shiftIt < numberOfPossibleShifts) && allFixedToSame; shiftIt++)
534 {
535 if (possibleShift[shiftIt])
536 {
537 // Will have shifted in something..
538 if (shiftIt > (bitWidth - 1 - column))
539 {
540 if (first)
541 {
542 allFixedTo = MSBValue;
543 first = false;
544 }
545 else
546 {
547 if (allFixedTo != MSBValue)
548 {
549 allFixedToSame = false;
550 }
551 }
552 }
553 else
554 {
555 unsigned index = column + shiftIt;
556 if (!op.isFixed(index))
557 allFixedToSame = false;
558 else if (first && op.isFixed(index))
559 {
560 first = false;
561 allFixedTo = op.getValue(index);
562 }
563 if (op.isFixed(index) && allFixedTo != op.getValue(index))
564 allFixedToSame = false;
565 }
566 }
567 }
568
569 // If it can be just one possible value. Then we can fix 'em.
570 if (allFixedToSame)
571 {
572 if (output.isFixed(column) && (output.getValue(column) != allFixedTo))
573 {
574 return CONFLICT;
575 }
576 if (!output.isFixed(column))
577 {
578 output.setFixed(column, true);
579 output.setValue(column, allFixedTo);
580 }
581 }
582 }
583 return NOT_IMPLEMENTED;
584 }
585
bvLeftShiftBothWays(vector<FixedBits * > & children,FixedBits & output)586 Result bvLeftShiftBothWays(vector<FixedBits*>& children, FixedBits& output)
587 {
588 const unsigned bitWidth = output.getWidth();
589 assert(2 == children.size());
590 assert(bitWidth > 0);
591
592 FixedBits& op = *children[0];
593 FixedBits& shift = *children[1];
594
595 if (debug_shift)
596 {
597 cerr << "op:" << op << endl;
598 cerr << "shift:" << shift << endl;
599 cerr << "output:" << output << endl;
600 }
601
602 // The topmost number of possible shifts corresponds to all
603 // the values of shift that shift out everything.
604 // i.e. possibleShift[bitWidth+1] is the SET of all operations that shift past
605 // the end.
606 const unsigned numberOfPossibleShifts = bitWidth + 1;
607 bool* possibleShift = (bool*)alloca(sizeof(bool) * numberOfPossibleShifts);
608 for (unsigned i = 0; i < numberOfPossibleShifts; i++)
609 possibleShift[i] = false;
610
611 unsigned minShift, maxShift;
612 shift.getUnsignedMinMax(minShift, maxShift);
613
614 // The shift must be less than the position of the first one in the output
615 int positionOfFirstOne = -1;
616 for (unsigned i = 0; i < bitWidth; i++)
617 {
618 if (output.isFixed(i) && output.getValue(i))
619 {
620 positionOfFirstOne = i;
621 break;
622 }
623 }
624
625 if (positionOfFirstOne >= 0)
626 {
627 if ((unsigned)positionOfFirstOne < minShift)
628 return CONFLICT;
629
630 maxShift = std::min(maxShift, (unsigned)positionOfFirstOne);
631 }
632
633 for (unsigned i = minShift; i <= std::min(bitWidth, maxShift); i++)
634 {
635 // if the bit-pattern of 'i' is in the set represented by the 'shift'.
636 if (shift.unsignedHolds(i))
637 possibleShift[i] = true;
638 }
639
640 // Complication. Given a shift like [-1]. possibleShift[2] is now false.
641 // A shift of 2 isn't possible. But one of three is.
642 // possibleShift[2] means any shift >=2 is possible. So it needs to be set
643 // to true.
644 {
645 if (maxShift >= bitWidth)
646 possibleShift[bitWidth] = true;
647 }
648
649 // Now check one-by-one each shifting.
650 // If we are shifting a zero to where a one is (say), then that shifting isn't
651 // possible.
652 for (unsigned shiftIt = 0; shiftIt < numberOfPossibleShifts; shiftIt++)
653 {
654 if (possibleShift[shiftIt])
655 {
656 for (unsigned column = 0; column < bitWidth; column++)
657 {
658 if (column < shiftIt)
659 {
660 if (output.isFixed(column) &&
661 output.getValue(
662 column)) // output is one in the column. That's wrong.
663 {
664 possibleShift[shiftIt] = false;
665 break;
666 }
667 }
668 else
669 {
670 // if they are fixed to different values. That's wrong.
671 if (output.isFixed(column) && op.isFixed(column - shiftIt) &&
672 (output.getValue(column) != op.getValue(column - shiftIt)))
673 {
674 possibleShift[shiftIt] = false;
675 break;
676 }
677 }
678 }
679 }
680 }
681
682 int nOfPossibleShifts = 0;
683 for (unsigned i = 0; i < numberOfPossibleShifts; i++)
684 {
685 if (possibleShift[i])
686 {
687 nOfPossibleShifts++;
688 if (debug_shift)
689 {
690 std::cerr << "Possible:" << i << std::endl;
691 }
692 }
693 }
694
695 if (debug_shift)
696 {
697 std::cerr << "Number of possible shifts:" << nOfPossibleShifts << endl;
698 }
699
700 // If it's empty. It's a conflict.
701 if (0 == nOfPossibleShifts)
702 return CONFLICT;
703
704 // We have a list of all the possible shift amounts.
705 // We take the union of all the bits that are possible.
706
707 FixedBits v(bitWidth, false);
708 bool first = true;
709 for (unsigned i = 0; i < numberOfPossibleShifts - 1; i++)
710 {
711 if (possibleShift[i])
712 {
713 if (first)
714 {
715 first = false;
716 for (unsigned j = 0; j < (unsigned)v.getWidth(); j++)
717 {
718 v.setFixed(j, true);
719 if (j < sizeof(unsigned) * 8)
720 v.setValue(j, 0 != (i & (1 << j)));
721 else
722 v.setValue(j, false);
723 }
724 }
725 else
726 {
727 // join.
728 for (unsigned j = 0;
729 j < (unsigned)v.getWidth() && j < sizeof(unsigned) * 8; j++)
730 {
731 if (v.isFixed(j))
732 {
733 // union.
734 if (v.getValue(j) != (0 != (i & (1 << j))))
735 v.setFixed(j, false);
736 }
737 }
738 }
739 }
740 }
741
742 // The top most entry of the shift table is special. It means all values of
743 // shift
744 // that fill it completely with zeroes. We take the union of all of the values
745 // >bitWidth
746 // in this function.
747 if (possibleShift[numberOfPossibleShifts - 1])
748 {
749 FixedBits bitWidthFB = FixedBits::fromUnsignedInt(bitWidth, bitWidth);
750 FixedBits output(1, true);
751 output.setFixed(0, true);
752 output.setValue(0, true);
753 FixedBits working(shift);
754
755 vector<FixedBits*> args;
756 args.push_back(&working);
757 args.push_back(&bitWidthFB);
758
759 // Write into working anything that can be determined given it's >=bitWidth.
760 Result r = bvGreaterThanEqualsBothWays(args, output);
761 assert(CONFLICT != r);
762
763 // Get the union of "working" with the prior union.
764 for (unsigned i = 0; i < bitWidth; i++)
765 {
766 if (!working.isFixed(i) && v.isFixed(i))
767 v.setFixed(i, false);
768 if (working.isFixed(i) && v.isFixed(i) &&
769 (working.getValue(i) != v.getValue(i)))
770 v.setFixed(i, false);
771 if (first) // no less shifts possible.
772 {
773 if (working.isFixed(i))
774 {
775 v.setFixed(i, true);
776 v.setValue(i, working.getValue(i));
777 }
778 }
779 }
780 }
781
782 if (debug_shift)
783 {
784 std::cerr << "Shift Amount:" << v << std::endl;
785 }
786
787 for (unsigned i = 0; i < bitWidth; i++)
788 {
789 if (v.isFixed(i))
790 {
791 if (!shift.isFixed(i))
792 {
793 shift.setFixed(i, true);
794 shift.setValue(i, v.getValue(i));
795 }
796 else if (shift.isFixed(i) && shift.getValue(i) != v.getValue(i))
797 return CONFLICT;
798 }
799 }
800
801 // If a particular input bit appears in every possible shifting,
802 // and if that bit is unfixed,
803 // and if the result it is fixed to the same value in every position.
804 // Then, that bit must be fixed.
805 // E.g. [--] << [0-] == [00]
806
807 bool* candidates = (bool*)alloca(sizeof(bool) * bitWidth);
808 for (unsigned i = 0; i < bitWidth; i++)
809 {
810 candidates[i] = !op.isFixed(i);
811 }
812
813 // candidates: So far: the bits that are unfixed.
814
815 for (unsigned i = 0; i < numberOfPossibleShifts; i++)
816 {
817 if (possibleShift[i])
818 {
819 // If this shift is possible, then some bits will be shifted out.
820 for (unsigned j = 0; j < i; j++)
821 candidates[bitWidth - 1 - j] = false;
822 }
823 }
824
825 // candidates: So far: + the input bits that are unfixed.
826 // + the input bits that are in every possible fixing.
827
828 // Check all candidates have the same output values.
829 for (unsigned candidate = 0; candidate < bitWidth; candidate++)
830 {
831 bool first = true;
832 bool setTo = false; // value that's never read. To quieten gcc.
833
834 if (candidates[candidate])
835 {
836 for (unsigned shiftIT = 0; shiftIT < bitWidth; shiftIT++)
837 {
838 // If the shift isn't possible continue.
839 if (!possibleShift[shiftIT])
840 continue;
841
842 unsigned idx = candidate + shiftIT;
843
844 if (!output.isFixed(idx))
845 {
846 candidates[candidate] = false;
847 break;
848 }
849 else
850 {
851 if (first)
852 {
853 first = false;
854 setTo = output.getValue(idx);
855 }
856 else
857 {
858 if (setTo != output.getValue(idx))
859 {
860 candidates[candidate] = false;
861 break;
862 }
863 }
864 }
865 }
866 }
867
868 if (candidates[candidate])
869 {
870 assert(!op.isFixed(candidate));
871 op.setFixed(candidate, true);
872 op.setValue(candidate, setTo);
873 }
874 }
875
876 // done.
877
878 // Go through each of the possible shifts. If the same value is fixed
879 // at every location. Then it's fixed too in the result.
880 for (unsigned column = 0; column < bitWidth; column++)
881 {
882 bool allFixedToSame = true;
883 bool allFixedTo = false; // value that's never read. To quieten gcc.
884 bool first = true;
885
886 for (unsigned shiftIt = minShift;
887 (shiftIt < numberOfPossibleShifts) && allFixedToSame; shiftIt++)
888 {
889 if (possibleShift[shiftIt])
890 {
891 // Will have shifted in zeroes.
892 if (shiftIt > column)
893 {
894 if (first)
895 {
896 allFixedTo = false;
897 first = false;
898 }
899 else
900 {
901 if (allFixedTo)
902 {
903 allFixedToSame = false;
904 }
905 }
906 }
907 else
908 {
909 unsigned index = column - shiftIt;
910 if (!op.isFixed(index))
911 allFixedToSame = false;
912 else if (first && op.isFixed(index))
913 {
914 first = false;
915 allFixedTo = op.getValue(index);
916 }
917 if (op.isFixed(index) && allFixedTo != op.getValue(index))
918 allFixedToSame = false;
919 }
920 }
921 }
922
923 // If it can be just one possible value. Then we can fix 'em.
924 if (allFixedToSame)
925 {
926 if (output.isFixed(column) && (output.getValue(column) != allFixedTo))
927 return CONFLICT;
928 if (!output.isFixed(column))
929 {
930 output.setFixed(column, true);
931 output.setValue(column, allFixedTo);
932 }
933 }
934 }
935
936 /*
937 // If there is only one possible shift value. Then, we can push from the
938 output back.
939 if (1 == nOfPossibleShifts)
940 {
941 for (unsigned i = shiftIndex; i < bitWidth; i++)
942 {
943 if (!op.isFixed(i - shiftIndex) && output.isFixed(i))
944 {
945 op.setFixed(i - shiftIndex, true);
946 op.setValue(i - shiftIndex, output.getValue(i));
947 result = CHANGED;
948 }
949 }
950 }
951 */
952
953 return NOT_IMPLEMENTED;
954 }
955 }
956 }
957