From 6b1ac652b0168a9352dff8e357a313e75f13bd21 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 28 Nov 2010 03:45:32 +0000 Subject: [PATCH] Maximally precise transfer functions for constant bit propagation. I'm still working on the multiplication like ones. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1030 e59a4935-1847-0410-ae03-e826735625c1 --- src/main/main.cpp | 2 - .../constantBitP/ConstantBitP_Arithmetic.cpp | 391 ++++++++ .../constantBitP/ConstantBitP_Boolean.cpp | 333 +++++++ .../constantBitP/ConstantBitP_Comparison.cpp | 631 ++++++++++++ .../constantBitP/ConstantBitP_Shifting.cpp | 927 ++++++++++++++++++ .../ConstantBitP_TransferFunctions.cpp | 460 +++++++++ .../ConstantBitP_TransferFunctions.h | 82 ++ .../constantBitP/ConstantBitPropagation.cpp | 7 +- 8 files changed, 2828 insertions(+), 5 deletions(-) create mode 100644 src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp create mode 100644 src/simplifier/constantBitP/ConstantBitP_Boolean.cpp create mode 100644 src/simplifier/constantBitP/ConstantBitP_Comparison.cpp create mode 100644 src/simplifier/constantBitP/ConstantBitP_Shifting.cpp create mode 100644 src/simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp create mode 100644 src/simplifier/constantBitP/ConstantBitP_TransferFunctions.h diff --git a/src/main/main.cpp b/src/main/main.cpp index be29b88..76726d7 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -110,10 +110,8 @@ int main(int argc, char ** argv) { helpstring += "-d : check counterexample\n"; -#ifdef WITHCBITP helpstring += "--disable-cbitp : disable constant bit propagation\n"; -#endif helpstring += "--exit-after-CNF : exit after the CNF has been generated\n"; diff --git a/src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp b/src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp new file mode 100644 index 0000000..3ba9843 --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp @@ -0,0 +1,391 @@ +#include "ConstantBitP_TransferFunctions.h" +#include "ConstantBitP_Utility.h" + +// Add, subtract. +// Trevor Hansen. BSD License. + +namespace simplifier +{ +namespace constantBitP +{ + +// Subtract is implemented in terms of plus. +Result bvSubtractBothWays(vector& children, FixedBits& output) +{ + assert(children.size() ==2); + + FixedBits & a = *children[0]; + FixedBits & b = *children[1]; + + assert(a.getWidth() == b.getWidth()); + + const int bitWidth = a.getWidth(); + + FixedBits one(bitWidth, false); + one.fixToZero(); + one.setFixed(0, true); + one.setValue(0, true); + + FixedBits notB(bitWidth, false); + + vector Addargs; + Addargs.push_back(&a); + Addargs.push_back(¬B); + Addargs.push_back(&one); + + bool changed = false; + while (true) // until it fixed points + { + Result result; + FixedBits initialNotB(notB); + FixedBits initialA(a); + FixedBits initialOut(output); + + result = bvNotBothWays(b, notB); + if (CONFLICT == result) + return CONFLICT; + + result = bvAddBothWays(Addargs, output); + if (CONFLICT == result) + return CONFLICT; + + if (FixedBits::equals(initialNotB, notB) && FixedBits::equals(initialA, a) && FixedBits::equals(initialOut, output)) + break; + else + changed = true; + } + + return NOT_IMPLEMENTED; +} + +/////////////// ADDITION> + +const bool add_debug_messages = false; + +// For a given number of children. The maximum size of the carry in for addition. +// +// For five arguments (say). The carry can be as big as 4. But into the second column +// it can be no bigger than 2. +unsigned maximumCarryInForAddition(int numberOfChildren, int index) +{ + assert(numberOfChildren > 1); + assert(index >=0); + + if (0 == index) + return 0; + + + if (numberOfChildren==2) + return 1; // Case that the (index==0) is already handled. + + + unsigned result = 0; + unsigned currIndex = 0; + + while (currIndex < (unsigned)index) + { + result = (result + numberOfChildren) >> 1; + currIndex++; + } + + //cerr << "max carry" << numberOfChildren << " " << index << " " << result << endl; + return result; +} + +// Given the current fixings to a particular column, as well as the range of the columns inflow, +// deduce values. +// index: Column we are working on. +// sum: What the column must sum to. +// inflowMin: Minimum inflow expected, i.e. lowerbound of lower (index-1). + +Result fixIfCanForAddition(vector& children, const int index, const int sum, const int inflowMin, const int inflowMax) +{ + Result result = NO_CHANGE; + + assert(inflowMin <= inflowMax); + assert(inflowMin >=0); + assert(index >=0); + assert(index < children[0]->getWidth()); + + const int maxCarryIn = maximumCarryInForAddition(children.size(), index); + + assert(inflowMax <= maxCarryIn); + assert(sum <= (signed)children.size() + maxCarryIn ); + + if (add_debug_messages) + cerr << "fixIfCanForAddition " << index << " " << sum << endl; + + int unfixed = 0; + int ones = 0; + int zeroes = 0; + for (unsigned i = 0; i < children.size(); i++) + { + if (children[i]->isFixed(index)) + { + if (children[i]->getValue(index)) + ones++; + if (!children[i]->getValue(index)) + zeroes++; + } + else + { + unfixed++; + } + } + + assert(ones >=0 && unfixed >=0 && zeroes >=0); + assert(ones + unfixed + zeroes == (signed)children.size()); + + ones = ones + inflowMin; + + if ((ones == sum) && unfixed > 0) // set em all to false. Already have as many as we need. + { + for (unsigned i = 0; i < children.size(); i++) + { + if (!children[i]->isFixed(index)) + { + children[i]->setFixed(index, true); + children[i]->setValue(index, false); + result = CHANGED; + } + } + } + + int sumUnfixed = unfixed + inflowMax - inflowMin; + zeroes = zeroes + (maxCarryIn - inflowMax); + + assert(ones >=0 && sumUnfixed >=0 && zeroes >=0); + assert(ones+sumUnfixed+zeroes == (signed) children.size()+ maxCarryIn); + + if (sum == (sumUnfixed + ones) && unfixed > 0) // need 'em all fixed to ones. + { + for (unsigned i = 0; i < children.size(); i++) + { + if (!children[i]->isFixed(index)) + { + children[i]->setFixed(index, true); + children[i]->setValue(index, true); + result = CHANGED; + } + } + } + else if (sum > sumUnfixed + ones) + return CONFLICT; + + if (sum < ones) + return CONFLICT; + + return result; +} + +// Count the number of fixed ones, and zeroes. Update the low and high column counts. +// Counts should only be monitonically changed. So this can only be run once. +void initialiseColumnCounts(int columnL[], int columnH[], const int bitWidth, const int numberOfChildren, const vector& children) +{ + // setup the low and highs. + for (int i = 0; i < bitWidth; i++) + { + columnL[i] = 0; + columnH[i] = numberOfChildren; + } + + // Set the column totals. + for (int i = 0; i < bitWidth; i++) + { + for (int j = 0; j < numberOfChildren; j++) + { + if (children[j]->isFixed(i)) + { + if (children[j]->getValue(i)) + columnL[i]++; + else + columnH[i]--; + } + } + } +} + +void printArray(int f[], int width) +{ + for (int i = width - 1; i >= 0; i--) + std::cerr << f[i] << " "; + std::cerr << std::endl; +} + +Result bvAddBothWays(vector& children, FixedBits& output) +{ + Result result = NO_CHANGE; + + const int bitWidth = output.getWidth(); + const int numberOfChildren = children.size(); + + for (int i = 0; i < numberOfChildren; i++) + { + assert(children[i]->getWidth() == bitWidth ); + } + + int columnL[bitWidth]; // minimum "" "" + int columnH[bitWidth]; // maximum number of true partial products. + + initialiseColumnCounts(columnL, columnH, bitWidth, numberOfChildren, children); + + int sumH[bitWidth]; + int sumL[bitWidth]; + sumL[0] = columnL[0]; + sumH[0] = columnH[0]; + + for (unsigned i = /**/1 /**/; i < (unsigned) bitWidth; i++) + { + assert((columnH[i] >= columnL[i]) && (columnL[i] >= 0)); + sumH[i] = columnH[i] + (sumH[i - 1] / 2); + sumL[i] = columnL[i] + (sumL[i - 1] / 2); + } + + // Now the sums counts are all updated. And consistent with each other. + + bool changed = true; + while (changed) + { + changed = false; + + // Make sure each column's sum is consistent with the output. + for (int i = 0; i < bitWidth; i++) + { + if (output.isFixed(i)) + { + int expected = output.getValue(i) ? 1 : 0; + + // output is true. So the maximum and minimum can only be even. + if (sumH[i] % 2 != expected) + { + sumH[i]--; + changed = true; + } + if (sumL[i] % 2 != expected) + { + sumL[i]++; + changed = true; + } + + if (changed && ((sumH[i] < sumL[i]) || (sumL[i] < 0))) + return CONFLICT; + } + } + + // update the column counts to make them consistent to the totals. + for (int i = /**/0 /**/; i < bitWidth; i++) + { + if (sumH[i] < columnH[i]) + { + columnH[i]--; + changed = true; + + if (columnH[i] < columnL[i]) + return CONFLICT; + } + } + + // Go from low to high making each of the sums consistent. + for (int i = /**/1 /**/; i < bitWidth; i++) + { + assert((columnH[i] >= columnL[i]) && (columnL[i] >= 0)); + if (sumH[i] > columnH[i] + (sumH[i - 1] / 2)) + { + sumH[i] = columnH[i] + (sumH[i - 1] / 2); + changed = true; + } + if (sumL[i] < columnL[i] + (sumL[i - 1] / 2)) + { + sumL[i] = columnL[i] + (sumL[i - 1] / 2); + changed = true; + } + + if (changed && (sumH[i] < sumL[i] || sumL[i] < 0)) + return CONFLICT; + + } + + // go from high to low, making each of the sums consistent. + for (int i = /**/bitWidth - 1 /**/; i >= 1; i--) + { + if ((sumH[i] == sumL[i])) + { + stats s = getStats(children, i); + + if (0 == s.unfixed) + { + // amount that the prior column needs to contribute. + int toContribute = (sumH[i] - s.fixedToOne) * 2; + + if (sumH[i - 1] > (toContribute + 1)) + { + changed = true; + sumH[i - 1] = toContribute + 1; // plus one because of rounding down. + } + + if (sumL[i - 1] < toContribute) + { + changed = true; + sumL[i - 1] = toContribute; + } + + if (sumH[i - 1] < sumL[i - 1]) + { + return CONFLICT; + } + } + } + } + + if (add_debug_messages) + { + std::cerr << "bottom" << std::endl; + cerr << "columnL:"; + printArray(columnL, bitWidth); + cerr << "columnH:"; + printArray(columnH, bitWidth); + cerr << "sumL:"; + printArray(sumL, bitWidth); + cerr << "sumH:"; + printArray(sumH, bitWidth); + } + + for (int column = 0; column < bitWidth; column++) + { + if (sumH[column] == sumL[column]) + { + // (1) If the low and high sum is equal. Then the output is know. + bool newResult = (sumH[column] % 2 == 0) ? false : true; + + if (!output.isFixed(column)) + { + output.setFixed(column, true); + output.setValue(column, newResult); + result = CHANGED; + changed = true; + } + else if (output.isFixed(column) && (output.getValue(column) != newResult)) + return CONFLICT; + + // (2) If this column has some unfixed values. Then we may be able to determine them. + Result tempResult; + if (0 == column) + tempResult = fixIfCanForAddition(children, column, sumH[column], 0, 0); + else + tempResult = fixIfCanForAddition(children, column, sumH[column], sumL[column - 1] / 2, sumH[column - 1] / 2); + + if (CONFLICT == tempResult) + return CONFLICT; + + if (CHANGED == tempResult) + changed = true; + + } + + } + } + return NOT_IMPLEMENTED; +} + +} +} diff --git a/src/simplifier/constantBitP/ConstantBitP_Boolean.cpp b/src/simplifier/constantBitP/ConstantBitP_Boolean.cpp new file mode 100644 index 0000000..d513531 --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_Boolean.cpp @@ -0,0 +1,333 @@ +#include "ConstantBitP_TransferFunctions.h" +#include "ConstantBitP_Utility.h" + +// AND, OR, XOR, NOT Transfer functions. +// Trevor Hansen. BSD License. + + + +namespace simplifier +{ +namespace constantBitP +{ + +Result bvXorBothWays(vector& operands, FixedBits& output) +{ + Result result = NO_CHANGE; + const int bitWidth = output.getWidth(); + + for (int i = 0; i < bitWidth; i++) + { + const stats status = getStats(operands, i); + + if (status.unfixed == 0) // if they are all fixed. We know the answer. + { + bool answer = (status.fixedToOne % 2) != 0; + + if (!output.isFixed(i)) + { + output.setFixed(i, true); + output.setValue(i, answer); + result = CHANGED; + } + else if (output.getValue(i) != answer) + return CONFLICT; + } + else if (status.unfixed == 1 && output.isFixed(i)) + { + // If there is just one unfixed, and we have the answer --> We know the value. + bool soFar = ((status.fixedToOne % 2) != 0); + if (soFar != output.getValue(i)) + { // result needs to be flipped. + fixUnfixedTo(operands, i, true); + } + else + fixUnfixedTo(operands, i, false); + result = CHANGED; + } + } + return result; +} + +// if output bit is true. Fix all the operands. +// if all the operands are fixed. Fix the output. +// given 1,1,1,- == 0, fix - to 0. +Result bvAndBothWays(vector& operands, FixedBits& output) +{ + Result result = NO_CHANGE; + const int bitWidth = output.getWidth(); + + for (int i = 0; i < bitWidth; i++) + { + const stats status = getStats(operands, i); + + // output is fixed to one. But an input value is false! + if (output.isFixed(i) && output.getValue(i) && status.fixedToZero > 0) + return CONFLICT; + + // output is fixed to one. But an input value is false! + if (output.isFixed(i) && !output.getValue(i) && status.fixedToZero == 0 + && status.unfixed == 0) + return CONFLICT; + + // output is fixed to one. So all should be one. + if (output.isFixed(i) && output.getValue(i) && status.unfixed > 0) + { + fixUnfixedTo(operands, i, true); + result = CHANGED; + } + + // The output is unfixed. At least one input is false. + if (!output.isFixed(i) && status.fixedToZero > 0) + { + output.setFixed(i, true); + output.setValue(i, false); + result = CHANGED; + } + + // Everything is fixed to one! + if (!output.isFixed(i) && status.fixedToZero == 0 && status.unfixed + == 0) + { + output.setFixed(i, true); + output.setValue(i, true); + result = CHANGED; + } + + // If the output is false, and there is a single unfixed value with everything else true.. + if (output.isFixed(i) && !output.getValue(i) && status.fixedToZero == 0 + && status.unfixed == 1) + { + fixUnfixedTo(operands, i, false); + result = CHANGED; + } + } + return result; +} + +Result bvOrBothWays(vector& children, FixedBits& output) +{ + Result r = NO_CHANGE; + const int numberOfChildren = children.size(); + const int bitWidth = output.getWidth(); + + for (int i = 0; i < bitWidth; i++) + { + bool answerKnown = output.isFixed(i); + bool answer = false; + if (answerKnown) + answer = output.getValue(i); + + int unks = 0; + int ones = 0; + int zeroes = 0; + + for (int j = 0; j < numberOfChildren; j++) + { + assert(output.getWidth() == children[j]->getWidth()); + + if (!children[j]->isFixed(i)) + unks++; + else if (children[j]->getValue(i)) + ones++; + else + zeroes++; + } + + if (ones > 0) // Atleast a single one found! + + { + if (answerKnown && !answer) + return CONFLICT; + + if (!answerKnown) + { + output.setFixed(i, true); + output.setValue(i, true); + r = CHANGED; + } + } + + if (zeroes == numberOfChildren) // all zeroes. + + { + if (answerKnown && answer) + return CONFLICT; + + if (!answerKnown) + { + r = CHANGED; + output.setFixed(i, true); + output.setValue(i, false); + + } + } + + if (answerKnown && !answer) // known false + + { + if (ones > 0) + return CONFLICT; + + // set all the column to false. + + for (int j = 0; j < numberOfChildren; j++) + { + if (!children[j]->isFixed(i)) + { + r = CHANGED; + children[j]->setFixed(i, true); + children[j]->setValue(i, false); + } + } + + } + + if (unks == 1 && answerKnown && answer && (zeroes == (numberOfChildren + - 1))) + { + // A single unknown, everything else is false. The answer is true. So the unknown is true. + + for (int j = 0; j < numberOfChildren; j++) + { + if (!children[j]->isFixed(i)) + { + r = CHANGED; + children[j]->setFixed(i, true); + children[j]->setValue(i, true); + } + } + } + + } + return r; +} + +Result bvNotBothWays(vector& children, FixedBits& result) +{ + return bvNotBothWays(*(children[0]), result); +} + +Result bvImpliesBothWays(vector& children, FixedBits& result) +{ + + FixedBits& a = (*children[0]); + FixedBits& b = (*children[1]); + + assert(a.getWidth() == result.getWidth()); + const int bitWidth = a.getWidth(); + assert (bitWidth == 1); + + Result r = NO_CHANGE; + + int i = 0; + + // (false -> something) is always true. + // (something -> true ) is always true. + if (a.isFixedToZero(i) || b.isFixedToOne(i)) + { + if (!result.isFixed(i)) + { + result.setFixed(i, true); + result.setValue(i, true); + r = CHANGED; + } else if (result.isFixedToZero(i)) + return CONFLICT; + } + + // If the result is false. it must be (true -> false) + if (result.isFixedToZero(i)) + { + if (a.isFixedToZero(i) || b.isFixedToOne(i)) + return CONFLICT; + + if (!a.isFixed(i)) + { + a.setFixed(i, true); + a.setValue(i, true); + r = CHANGED; + } + if (!b.isFixed(i)) + { + b.setFixed(i, true); + b.setValue(i, false); + r = CHANGED; + } + } + + if (result.isFixedToOne(i)) + { + if (a.isFixedToOne(i)) + { + if (!b.isFixed(i)) + { + b.setFixed(i, true); + b.setValue(i, true); + r = CHANGED; + } + else if (b.isFixedToZero(i)) + return CONFLICT; + } + + if (b.isFixedToZero(i)) + { + if (!a.isFixed(i)) + { + a.setFixed(i, true); + a.setValue(i, false); + r = CHANGED; + } + } + } + + if (a.isFixedToOne(i) && b.isFixedToZero(i)) + { + if (result.isFixedToOne(i)) + return CONFLICT; + if (!result.isFixed(i)) + { + result.setFixed(i, true); + result.setValue(i, false); + r = CHANGED; + } + } + + return r; + +} + +Result bvNotBothWays(FixedBits& a, FixedBits& output) +{ + assert(a.getWidth() == output.getWidth()); + const int bitWidth = a.getWidth(); + + Result result = NO_CHANGE; + + for (int i = 0; i < bitWidth; i++) + { + // error if they are the same. + if (a.isFixed(i) && output.isFixed(i) && (a.getValue(i) + == output.getValue(i))) + { + return CONFLICT; + } + + if (a.isFixed(i) && !output.isFixed(i)) + { + output.setFixed(i, true); + output.setValue(i, !a.getValue(i)); + result = CHANGED; + } + + if (output.isFixed(i) && !a.isFixed(i)) + { + a.setFixed(i, true); + a.setValue(i, !output.getValue(i)); + result = CHANGED; + } + } + return result; +} + +} +} diff --git a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp new file mode 100644 index 0000000..4f99030 --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp @@ -0,0 +1,631 @@ +#include "ConstantBitP_TransferFunctions.h" +#include "ConstantBitP_Utility.h" +#include "../../extlib-constbv/constantbv.h" + + +// The signed and unsigned versions of the four comparison operations: > < >= <= + +// Establishes consistency over the intervals of the operations. Then +// increase the minimum value by turning on the highest unfixed bit. +// If that takes us past the other value's maximum. Then that bit +// must be zero. + +// Trevor Hansen. BSD License. + +namespace simplifier +{ +namespace constantBitP +{ + +Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output); +Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output); + +Result bvSignedLessThanBothWays(vector& children, FixedBits& output) +{ + assert(children.size() == 2); + return bvSignedLessThanBothWays(*children[0], *children[1], output); +} + +Result bvSignedGreaterThanBothWays(FixedBits & c0, FixedBits & c1, FixedBits& output) +{ + return bvSignedLessThanBothWays(c1, c0, output); +} + +Result bvSignedGreaterThanBothWays(vector& children, FixedBits& output) +{ + assert(children.size() == 2); + return bvSignedLessThanBothWays(*children[1], *children[0], output); +} + +Result bvSignedLessThanEqualsBothWays(vector& children, FixedBits& output) +{ + assert(children.size() == 2); + return bvSignedLessThanEqualsBothWays(*children[0], *children[1], output); +} + +Result bvSignedGreaterThanEqualsBothWays(FixedBits & c0, FixedBits & c1, FixedBits& output) +{ + return bvSignedLessThanEqualsBothWays(c1, c0, output); +} + +Result bvSignedGreaterThanEqualsBothWays(vector& children, FixedBits& output) +{ + assert(children.size() == 2); + return bvSignedLessThanEqualsBothWays(*children[1], *children[0], output); +} + +///////// UNSIGNED. + +Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output); +Result bvLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output); + +Result bvLessThanBothWays(vector& children, FixedBits& output) +{ + assert(children.size() == 2); + return bvLessThanBothWays(*children[0], *children[1], output); +} + +Result bvGreaterThanBothWays(vector& children, FixedBits& output) +{ + assert(children.size() == 2); + return bvLessThanBothWays(*children[1], *children[0], output); +} + +Result bvGreaterThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output) +{ + return bvLessThanBothWays(c1, c0, output); +} + +Result bvGreaterThanEqualsBothWays(vector& children, FixedBits& result) +{ + assert(children.size() == 2); + return bvLessThanEqualsBothWays(*children[1], *children[0], result); +} + +Result bvGreaterThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output) +{ + return bvLessThanEqualsBothWays(c1, c0, output); +} + +Result bvLessThanEqualsBothWays(vector& children, FixedBits& output) +{ + assert(children.size() == 2); + return bvLessThanEqualsBothWays(*children[0], *children[1], output); +} + +typedef unsigned int* CBV; + +void destroy(CBV a, CBV b, CBV c, CBV d) +{ + CONSTANTBV::BitVector_Destroy(a); + CONSTANTBV::BitVector_Destroy(b); + CONSTANTBV::BitVector_Destroy(c); + CONSTANTBV::BitVector_Destroy(d); +} + +///////// Signed operations. + + + + +Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits& c1, FixedBits& output) +{ + Result r = NO_CHANGE; + + assert(c0.getWidth() == c1.getWidth()); + + CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c1_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + + setSignedMinMax(c0, c0_min, c0_max); + setSignedMinMax(c1, c1_min, c1_max); + + // EG. [0,5] < [6,8]. i.e. max of first is less than min of second. + if (signedCompare(c0_max, c1_min) < 0) + { + if (output.isFixed(0) && !output.getValue(0)) // output is fixed to false. + { + destroy(c0_min, c0_max, c1_min, c1_max); + return CONFLICT; + } + + if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, true); + r = CHANGED; + } + } + + // EG. [3,5] < [0,1]. + if (signedCompare(c0_min, c1_max) >= 0) + { + // min is greater than max. + if (output.isFixed(0) && output.getValue(0)) + { + destroy(c0_min, c0_max, c1_min, c1_max); + return CONFLICT; + } + + if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, false); + r = CHANGED; + } + } + + if (output.isFixed(0) && !output.getValue(0)) + { + FixedBits t(1, true); + t.setFixed(0, true); + t.setValue(0, true); + destroy(c0_min, c0_max, c1_min, c1_max); + return bvSignedGreaterThanEqualsBothWays(c0, c1, t); + } + + const int msb = c0.getWidth() - 1; + + // The signed case. + if (output.isFixed(0) && output.getValue(0)) + { + //////////// MSB + // turn off the sign bit of c0's minimum. + // If that value is greater or equal to c1's max. SEt it. + if (!c0.isFixed(msb)) + { + // turn it on in the minimum. + CONSTANTBV::BitVector_Bit_Off(c0_min, msb); + if (signedCompare(c0_min, c1_max) >= 0) + { + c0.setFixed(msb, true); + c0.setValue(msb, true); + setSignedMinMax(c0, c0_min, c0_max); + r = CHANGED; + } + else + { + CONSTANTBV::BitVector_Bit_On(c0_min, msb); + } + } + + if (!c1.isFixed(msb)) + { + CONSTANTBV::BitVector_Bit_On(c1_max, msb); + if (signedCompare(c1_max, c0_min) <= 0) + { + c1.setFixed(msb, true); + c1.setValue(msb, false); + setSignedMinMax(c1, c1_min, c1_max); + r = CHANGED; + } + else + { + CONSTANTBV::BitVector_Bit_Off(c1_max, msb); + } + } + + ///////////// Bits other than the MSB + + if (output.isFixed(0) && output.getValue(0)) + { + for (int i = c0.getWidth() - 1 - 1; i >= 0; i--) + { + if (!c0.isFixed(i)) + { + // turn it on in the minimum. + CONSTANTBV::BitVector_Bit_On(c0_min, i); + if (signedCompare(c0_min, c1_max) >= 0) + { + c0.setFixed(i, true); + c0.setValue(i, false); + setSignedMinMax(c0, c0_min, c0_max); + r = CHANGED; + } + else + { + CONSTANTBV::BitVector_Bit_Off(c0_min, i); + break; + } + } + } + + for (int i = c1.getWidth() - 1 - 1; i >= 0; i--) + { + if (!c1.isFixed(i)) + { + CONSTANTBV::BitVector_Bit_Off(c1_max, i); + if (signedCompare(c1_max, c0_min) <= 0) + { + c1.setFixed(i, true); + c1.setValue(i, true); + setSignedMinMax(c1, c1_min, c1_max); + r = CHANGED; + } + else + { + CONSTANTBV::BitVector_Bit_On(c1_max, i); + break; + } + } + } + } + } + destroy(c0_min, c0_max, c1_min, c1_max); + return NOT_IMPLEMENTED; +} + +Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output) +{ + Result r = NO_CHANGE; + + assert(c0.getWidth() == c1.getWidth()); + + CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c1_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + + setSignedMinMax(c0, c0_min, c0_max); + setSignedMinMax(c1, c1_min, c1_max); + + if (signedCompare(c0_max, c1_min) <= 0) + { + if (output.isFixed(0) && !output.getValue(0)) + { + destroy(c0_min, c0_max, c1_min, c1_max); + return CONFLICT; + } + + if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, true); + r = CHANGED; + } + } + + if (signedCompare(c0_min, c1_max) > 0) + { + if (output.isFixed(0) && output.getValue(0)) + { + destroy(c0_min, c0_max, c1_min, c1_max); + return CONFLICT; + } + + if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, false); + r = CHANGED; + } + } + + // If true. Reverse and send to the other.. + if (output.isFixed(0) && !output.getValue(0)) + { + FixedBits t(1, true); + t.setFixed(0, true); + t.setValue(0, true); + destroy(c0_min, c0_max, c1_min, c1_max); + return bvSignedGreaterThanBothWays(c0, c1, t); + } + + const int msb = c0.getWidth() - 1; + + if (output.isFixed(0) && output.getValue(0)) + { + //////////// MSB + // turn off the sign bit of c0's minimum. + // If that value is greater or equal to c1's max. SEt it. + if (!c0.isFixed(msb)) + { + // turn it on in the minimum. + CONSTANTBV::BitVector_Bit_Off(c0_min, msb); + if (signedCompare(c0_min, c1_max) > 0) + { + c0.setFixed(msb, true); + c0.setValue(msb, true); + setSignedMinMax(c0, c0_min, c0_max); + r = CHANGED; + } + else + { + CONSTANTBV::BitVector_Bit_On(c0_min, msb); + } + } + + if (!c1.isFixed(msb)) + { + CONSTANTBV::BitVector_Bit_On(c1_max, msb); + if (signedCompare(c1_max, c0_min) < 0) + { + c1.setFixed(msb, true); + c1.setValue(msb, false); + setSignedMinMax(c1, c1_min, c1_max); + r = CHANGED; + } + else + { + CONSTANTBV::BitVector_Bit_Off(c1_max, msb); + } + } + //////////// Others. + + + // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side + // then we know it must be turned off. + for (int i = c0.getWidth() - 1 - 1; i >= 0; i--) + { + if (!c0.isFixed(i)) // bit is variable. + { + // turn it on in the minimum. + CONSTANTBV::BitVector_Bit_On(c0_min, i); + if (signedCompare(c0_min, c1_max) > 0) + { + c0.setFixed(i, true); + c0.setValue(i, false); + setSignedMinMax(c0, c0_min, c0_max); + } + else + { + CONSTANTBV::BitVector_Bit_Off(c0_min, i); + break; + } + } + } + + // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side + // then we know it must be turned off. + for (int i = c0.getWidth() - 1 - 1; i >= 0; i--) + { + if (!c1.isFixed(i)) // bit is variable. + { + // turn it on in the minimum. + CONSTANTBV::BitVector_Bit_Off(c1_max, i); + if (signedCompare(c1_max, c0_min) < 0) + { + c1.setFixed(i, true); + c1.setValue(i, true); + setSignedMinMax(c1, c1_min, c1_max); + } + else + { + CONSTANTBV::BitVector_Bit_On(c1_max, i); + break; + } + } + } + } + + destroy(c0_min, c0_max, c1_min, c1_max); + return NOT_IMPLEMENTED; +} + +///////////////////////// UNSIGNED. + + + + +// UNSIGNED!! +Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output) +{ + Result r = NO_CHANGE; + + assert(c0.getWidth() == c1.getWidth()); + + CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c1_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + + setUnsignedMinMax(c0, c0_min, c0_max); + setUnsignedMinMax(c1, c1_min, c1_max); + + // EG. [0,5] < [6,8]. i.e. max of first is less than min of second. + if (unsignedCompare(c0_max, c1_min) < 0) + { + if (output.isFixed(0) && !output.getValue(0)) // output is fixed to false. + { + destroy(c0_min, c0_max, c1_min, c1_max); + return CONFLICT; + } + + if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, true); + } + } + + // EG. [3,5] < [0,1]. + if (unsignedCompare(c0_min, c1_max) >= 0) + { + // min is greater than max. + if (output.isFixed(0) && output.getValue(0)) + { + destroy(c0_min, c0_max, c1_min, c1_max); + return CONFLICT; + } + + if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, false); + } + } + + // If true. Reverse and send to the other. + if (output.isFixed(0) && !output.getValue(0)) + { + FixedBits t(1, true); + t.setFixed(0, true); + t.setValue(0, true); + destroy(c0_min, c0_max, c1_min, c1_max); + return bvGreaterThanEqualsBothWays(c0, c1, t); + } + + bool changed = false; + + if (output.isFixed(0) && output.getValue(0)) + { + // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side + // then we know it must be turned off. + for (int i = c0.getWidth() - 1; i >= 0; i--) + { + if (!c0.isFixed(i)) // bit is variable. + { + // turn it on in the minimum. + CONSTANTBV::BitVector_Bit_On(c0_min, i); + if (unsignedCompare(c0_min, c1_max) >= 0) + { + c0.setFixed(i, true); + c0.setValue(i, false); + setUnsignedMinMax(c0, c0_min, c0_max); + changed = true; + } + else + { + CONSTANTBV::BitVector_Bit_Off(c0_min, i); + break; + } + } + } + + for (int i = c1.getWidth() - 1; i >= 0; i--) + { + if (!c1.isFixed(i)) // bit is variable. + { + CONSTANTBV::BitVector_Bit_Off(c1_max, i); + if (unsignedCompare(c1_max, c0_min) <= 0) + { + c1.setFixed(i, true); + c1.setValue(i, true); + setUnsignedMinMax(c1, c1_min, c1_max); + changed = true; + } + else + { + CONSTANTBV::BitVector_Bit_On(c1_max, i); + break; + } + } + } + } + + destroy(c0_min, c0_max, c1_min, c1_max); + return NOT_IMPLEMENTED; +} + +Result bvLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output) +{ + Result r = NO_CHANGE; + + assert(c0.getWidth() == c1.getWidth()); + + CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + CBV c1_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true); + + setUnsignedMinMax(c0, c0_min, c0_max); + setUnsignedMinMax(c1, c1_min, c1_max); + + // EG. [0,5] <= [6,8]. i.e. max of first is less than min of second. + if (unsignedCompare(c0_max, c1_min) <= 0) + { + if (output.isFixed(0) && !output.getValue(0)) // output is fixed to false. + { + destroy(c0_min, c0_max, c1_min, c1_max); + return CONFLICT; + } + + if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, true); + } + } + + // EG. [3,5] <= [0,1]. + if (unsignedCompare(c0_min, c1_max) > 0) + { + if (output.isFixed(0) && output.getValue(0)) + { + destroy(c0_min, c0_max, c1_min, c1_max); + return CONFLICT; + } + + if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, false); + } + } + + // If true. Reverse and send to the other.. + if (output.isFixed(0) && !output.getValue(0)) + { + FixedBits t(1, true); + t.setFixed(0, true); + t.setValue(0, true); + destroy(c0_min, c0_max, c1_min, c1_max); + return bvGreaterThanBothWays(c0, c1, t); + } + + // We only deal with the true case in this function. + + if (output.isFixed(0) && output.getValue(0)) + { + // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side + // then we know it must be turned off. + for (int i = c0.getWidth() - 1; i >= 0; i--) + { + if (!c0.isFixed(i)) // bit is variable. + { + // turn it on in the minimum. + CONSTANTBV::BitVector_Bit_On(c0_min, i); + if (unsignedCompare(c0_min, c1_max) > 0) + { + c0.setFixed(i, true); + c0.setValue(i, false); + setUnsignedMinMax(c0, c0_min, c0_max); + } + else + { + CONSTANTBV::BitVector_Bit_Off(c0_min, i); + break; + } + } + } + + // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side + // then we know it must be turned off. + for (int i = c0.getWidth() - 1; i >= 0; i--) + { + if (!c1.isFixed(i)) // bit is variable. + { + // turn it on in the minimum. + CONSTANTBV::BitVector_Bit_Off(c1_max, i); + if (unsignedCompare(c1_max, c0_min) < 0) + { + c1.setFixed(i, true); + c1.setValue(i, true); + setUnsignedMinMax(c1, c1_min, c1_max); + } + else + { + CONSTANTBV::BitVector_Bit_On(c1_max, i); + break; + } + } + } + } + destroy(c0_min, c0_max, c1_min, c1_max); + return NOT_IMPLEMENTED; +} + +} +} diff --git a/src/simplifier/constantBitP/ConstantBitP_Shifting.cpp b/src/simplifier/constantBitP/ConstantBitP_Shifting.cpp new file mode 100644 index 0000000..c9af59c --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_Shifting.cpp @@ -0,0 +1,927 @@ +#include "ConstantBitP_TransferFunctions.h" +#include "ConstantBitP_Utility.h" +#include "../../extlib-constbv/constantbv.h" + +// Left shift, right shift. +// Trevor Hansen. BSD License. + +// smtlib & x86 semantics differ for what happens when a value is shifted by greater +// than the bitWidth. On x86, in 64-bit mode, only the bottom 6 bits of the shift are +// used. In SMTLIB the total value is used. + + +namespace simplifier +{ +namespace constantBitP +{ + +const bool debug_shift = false; + +Result bvRightShiftBothWays(vector& children, FixedBits& output) +{ + Result result = NO_CHANGE; + const unsigned bitWidth = output.getWidth(); + + assert(2 == children.size()); + + FixedBits& op = *children[0]; + FixedBits& shift = *children[1]; + + FixedBits outputReverse(bitWidth,false); + FixedBits opReverse(bitWidth,false); + + // Reverse the output and the input. + for (unsigned i =0; i < bitWidth;i++) + { + if (op.isFixed(i)) + { + opReverse.setFixed(bitWidth-1-i,true); + opReverse.setValue(bitWidth-1-i,op.getValue(i)); + } + + if (output.isFixed(i)) + { + outputReverse.setFixed(bitWidth-1-i,true); + outputReverse.setValue(bitWidth-1-i,output.getValue(i)); + } + } + + vector args; + args.push_back(&opReverse); + args.push_back(&shift); // shift is unmodified. + result = bvLeftShiftBothWays(args, outputReverse); + + if (CONFLICT == result) + return CONFLICT; + + // Now write the reversed values back. + // Reverse the output and the input. + for (unsigned i =0; i < bitWidth;i++) + { + if (opReverse.isFixed(i) && !op.isFixed(bitWidth-1-i)) + { + op.setFixed(bitWidth-1-i,true); + op.setValue(bitWidth-1-i,opReverse.getValue(i)); + } + + if (outputReverse.isFixed(i) && !output.isFixed(bitWidth-1-i)) + { + output.setFixed(bitWidth-1-i,true); + output.setValue(bitWidth-1-i,outputReverse.getValue(i)); + } + } + + return result; +} + +// Converts the array of possible shifts into a set that represents the values. +FixedBits getPossible(unsigned bitWidth, bool possibleShift[], unsigned numberOfPossibleShifts, const FixedBits& shift) +{ + FixedBits v(bitWidth, false); + bool first = true; + for (unsigned i = 0; i < numberOfPossibleShifts - 1; i++) + { + if (possibleShift[i]) + { + if (first) + { + first = false; + for (unsigned j = 0; j < (unsigned) v.getWidth(); j++) + { + v.setFixed(j, true); + if (j < sizeof(unsigned) * 8) + v.setValue(j, 0 != (i & (1 << j))); + else + v.setValue(j, false); + } + } + else + { + // join. + for (unsigned j = 0; j < (unsigned) v.getWidth() && j + < sizeof(unsigned) * 8; j++) + { + if (v.isFixed(j)) + { + // union. + if (v.getValue(j) != (0 != (i & (1 << j)))) + v.setFixed(j, false); + } + } + } + } + } + + unsigned firstShift; + for (firstShift=0; firstShiftbitWidth + // in this function. + if (possibleShift[numberOfPossibleShifts - 1]) + { + FixedBits bitWidthFB = FixedBits::fromUnsignedInt(bitWidth, bitWidth); + FixedBits output(1, true); + output.setFixed(0, true); + output.setValue(0, true); + FixedBits working(shift); + + vector args; + args.push_back(&working); + args.push_back(&bitWidthFB); + + //Write into working anything that can be determined given it's >=bitWidth. + Result r = bvGreaterThanEqualsBothWays(args,output); + assert(CONFLICT != r); + + // Get the union of "working" with the prior union. + for (unsigned i = 0; i < bitWidth; i++) + { + if (!working.isFixed(i) && v.isFixed(i)) + v.setFixed(i, false); + if (working.isFixed(i) && v.isFixed(i) && (working.getValue(i) != v.getValue(i))) + v.setFixed(i, false); + if (firstShift == numberOfPossibleShifts - 1) // no less shifts possible. + { + if (working.isFixed(i)) + { + v.setFixed(i, true); + v.setValue(i, working.getValue(i)); + } + } + } + } + + if (debug_shift) + cerr << "Set of possible shifts:" << v << endl; + + return v; +} + + +unsigned getMaxShiftFromValueViaAlternation(const unsigned bitWidth, const FixedBits& output) +{ + unsigned maxShiftFromValue = UINT_MAX; + + // The shift must be less than the position of the first alternation. + bool foundTrue = false; + bool foundFalse = false; + for (int i = bitWidth - 1; i >= 0; i--) + { + if (output.isFixed(i)) + { + if (output.getValue(i) && foundFalse) + { + maxShiftFromValue = i; + break; + } + if (!output.getValue(i) && foundTrue) + { + maxShiftFromValue = i; + break; + } + if (output.getValue(i)) + foundTrue = true; + else if (!output.getValue(i)) + foundFalse = true; + } + } + + if (maxShiftFromValue != UINT_MAX) + maxShiftFromValue = bitWidth - 2 - maxShiftFromValue; + + return maxShiftFromValue; +} + +Result bvArithmeticRightShiftBothWays(vector& children, FixedBits& output) +{ + const unsigned bitWidth = output.getWidth(); + assert(2== children.size()); + assert(bitWidth > 0); + assert(children[0]->getWidth() == children[1]->getWidth()); + const unsigned MSBIndex = bitWidth-1; + + Result result = NO_CHANGE; + + FixedBits& op = *children[0]; + FixedBits& shift = *children[1]; + + // If the MSB isn't set, create a copy with it set each way and take the meet. + if (!op.isFixed(MSBIndex)) + { + vector children1; + vector children2; + FixedBits op1(op); + FixedBits op2(op); + FixedBits shift1(shift); + FixedBits shift2(shift); + FixedBits output1(output); + FixedBits output2(output); + + children1.push_back(&op1); + children1.push_back(&shift1); + op1.setFixed(MSBIndex, true); + op1.setValue(MSBIndex, true); + + children2.push_back(&op2); + children2.push_back(&shift2); + op2.setFixed(MSBIndex, true); + op2.setValue(MSBIndex, false); + + Result r1 = bvArithmeticRightShiftBothWays(children1, output1); + Result r2 = bvArithmeticRightShiftBothWays(children2, output2); + + if (r1 == CONFLICT && r2 == CONFLICT) + return CONFLICT; + + if (r1 == CONFLICT) + { + op = op2; + shift = shift2; + output = output2; + return r2; + } + + if (r2 == CONFLICT) + { + op = op1; + shift = shift1; + output = output1; + return r1; + } + + op = FixedBits::meet(op1,op2); + shift = FixedBits::meet(shift1,shift2); + output = FixedBits::meet(output1,output2); + return r1; + + } + + assert(op.isFixed(MSBIndex)); + + if (debug_shift) + { + cerr << "=========" << endl; + cerr << op << " >a> "; + cerr << shift; + cerr << " = " << output << endl; + } + + // The topmost number of possible shifts corresponds to all + // the values of shift that shift out everything. + // i.e. possibleShift[bitWidth+1] is the SET of all operations that shift past the end. + const unsigned numberOfPossibleShifts = bitWidth + 1; + bool possibleShift[numberOfPossibleShifts]; + for (unsigned i = 0; i < numberOfPossibleShifts; i++) + possibleShift[i] = false; + + + // If either of the top two bits are fixed they should be equal. + if (op.isFixed(MSBIndex) ^ output.isFixed(MSBIndex)) + { + if (op.isFixed(MSBIndex)) + { + output.setFixed(MSBIndex, true); + output.setValue(MSBIndex, op.getValue(MSBIndex)); + } + + if (output.isFixed(MSBIndex)) + { + op.setFixed(MSBIndex, true); + op.setValue(MSBIndex, output.getValue(MSBIndex)); + } + } + + // Both the MSB of the operand and the output should be fixed now.. + assert(output.isFixed(MSBIndex)); + + unsigned minShiftFromShift, maxShiftFromShift; // The range of the "shift" value. + shift.getUnsignedMinMax(minShiftFromShift, maxShiftFromShift); + + // The shift can't be any bigger than the topmost alternation in the output. + // For example if the output is 0.01000, then the shift can not be bigger than + // 3. + unsigned maxShiftFromOutput = getMaxShiftFromValueViaAlternation(bitWidth, output); + + maxShiftFromShift = std::min(maxShiftFromShift, (unsigned) maxShiftFromOutput); + + if (debug_shift) + { + cerr << "minshift:" << minShiftFromShift << endl; + cerr << "maxshift:" << maxShiftFromShift << endl; + cerr << "total:" << maxShiftFromShift << endl; + } + + + for (unsigned i = minShiftFromShift; i <= std::min(bitWidth, maxShiftFromShift); i++) + { + // if the bit-pattern of 'i' is in the set represented by the 'shift'. + if (shift.unsignedHolds(i)) + possibleShift[i] = true; + } + + // Complication. Given a shift like [.1] possibleShift[2] is now false. + // A shift of 2 isn't possible. But one of three is. + // possibleShift[2] means any shift >=2 is possible. So it needs to be set + // to true. + { + if (maxShiftFromShift >= bitWidth) + possibleShift[bitWidth] = true; + } + + // Now check one-by-one each shifting. + // If we are shifting a zero to where a one is (say), then that shifting isn't possible. + for (unsigned shiftIt = minShiftFromShift; shiftIt < numberOfPossibleShifts; shiftIt++) + { + if (possibleShift[shiftIt]) + { + for (unsigned column = 0; column < bitWidth; column++) + { + // if they are fixed to different values. That's wrong. + if (column + shiftIt <= bitWidth - 1) + { + if (output.isFixed(column) && op.isFixed(column + shiftIt) + && (output.getValue(column) != op.getValue(column + + shiftIt))) + { + possibleShift[shiftIt] = false; + break; + } + } + } + } + } + + int nOfPossibleShifts = 0; + for (unsigned i = 0; i < numberOfPossibleShifts; i++) + { + if (possibleShift[i]) + { + nOfPossibleShifts++; + maxShiftFromShift = i; + if (debug_shift) + { + std::cerr << "Possible Shift:" << i << std::endl; + } + } + } + + if (debug_shift) + { + std::cerr << "Number of possible shifts:" << nOfPossibleShifts << endl; + } + + // If it's empty. It's a conflict. + if (0 == nOfPossibleShifts) + { + return CONFLICT; + } + + // We have a list of all the possible shift amounts. + // We take the union of all the bits that are possible. + FixedBits setOfPossibleShifts = getPossible(bitWidth, possibleShift, numberOfPossibleShifts,shift); + + // Write in any fixed values to the shift. + for (unsigned i = 0; i < bitWidth; i++) + { + if (setOfPossibleShifts.isFixed(i)) + { + if (!shift.isFixed(i)) + { + shift.setFixed(i, true); + shift.setValue(i, setOfPossibleShifts.getValue(i)); + result = CHANGED; + } + else if (shift.isFixed(i) && shift.getValue(i) + != setOfPossibleShifts.getValue(i)) + { + return CONFLICT; + } + } + } + + // If a particular input bit appears in every possible shifting, + // and if that bit is unfixed, + // and if the result it is fixed to the same value in every position. + // Then, that bit must be fixed. + // E.g. [--] << [0-] == [00] + + bool candidates[bitWidth]; + for (unsigned i = 0; i < bitWidth; i++) + { + candidates[i] = !op.isFixed(i); + } + + // candidates: So far: the bits that are unfixed in the operand. + + for (unsigned i = 0; i < numberOfPossibleShifts; i++) + { + if (possibleShift[i]) + { + // If this shift is possible, then some bits will be shifted out. + for (unsigned j = 0; j < i; j++) + candidates[j] = false; + } + } + + // candidates: So far: + the input bits that are unfixed. + // + the input bits that are in every possible fixing. + + // Check all candidates have the same output values. + for (unsigned candidate = 0; candidate < bitWidth; candidate++) + { + bool first = true; + bool setTo = false; // value that's never read. To quieten gcc. + + if (candidates[candidate]) + { + for (unsigned shiftIT = 0; shiftIT < bitWidth; shiftIT++) + { + // If the shift isn't possible continue. + if (!possibleShift[shiftIT]) + continue; + + if (shiftIT > candidate) + continue; + + unsigned idx = candidate - shiftIT; + + if (!output.isFixed(idx)) + { + candidates[candidate] = false; + break; + } + else + { + if (first) + { + first = false; + setTo = output.getValue(idx); + } + else + { + if (setTo != output.getValue(idx)) + { + candidates[candidate] = false; + break; + } + + } + } + } + } + + if (candidates[candidate]) + { + assert(!op.isFixed(candidate)); + op.setFixed(candidate, true); + op.setValue(candidate, setTo); + } + } + + if (debug_shift) + { + cerr << op << " >a> "; + cerr << shift; + cerr << " = " << output << endl; + } + + // Go through each of the possible shifts. If the same value is fixed + // at every location. Then it's fixed too in the result. + // Looping over the output columns. + bool MSBValue = op.getValue(MSBIndex); + + for (unsigned column = 0; column < bitWidth; column++) + { + bool allFixedToSame = true; + bool allFixedTo = false; // value that's never read. To quieten gcc. + bool first = true; + + for (unsigned shiftIt = 0; (shiftIt < numberOfPossibleShifts) + && allFixedToSame; shiftIt++) + { + if (possibleShift[shiftIt]) + { + // Will have shifted in something.. + if (shiftIt > (bitWidth - 1 -column)) + { + if (first) + { + allFixedTo = MSBValue; + first = false; + } + else + { + if (allFixedTo != MSBValue) + { + allFixedToSame = false; + } + } + } + else + { + unsigned index = column + shiftIt; + if (!op.isFixed(index)) + allFixedToSame = false; + else if (first && op.isFixed(index)) + { + first = false; + allFixedTo = op.getValue(index); + } + if (op.isFixed(index) && allFixedTo != op.getValue( + index)) + allFixedToSame = false; + } + } + } + + // If it can be just one possible value. Then we can fix 'em. + if (allFixedToSame) + { + if (output.isFixed(column) && (output.getValue(column) + != allFixedTo)) + { + return CONFLICT; + } + if (!output.isFixed(column)) + { + output.setFixed(column, true); + output.setValue(column, allFixedTo); + result = CHANGED; + } + } + } + return NOT_IMPLEMENTED; +} + +Result bvLeftShiftBothWays(vector& children, FixedBits& output) +{ + const unsigned bitWidth = output.getWidth(); + assert(2== children.size()); + assert(bitWidth > 0); + + Result result = NO_CHANGE; + + FixedBits& op = *children[0]; + FixedBits& shift = *children[1]; + + if (debug_shift) + { + cerr << "op:" << op << endl; + cerr << "shift:" << shift << endl; + cerr << "output:" << output << endl; + } + + // The topmost number of possible shifts corresponds to all + // the values of shift that shift out everything. + // i.e. possibleShift[bitWidth+1] is the SET of all operations that shift past the end. + const unsigned numberOfPossibleShifts = bitWidth + 1; + bool possibleShift[numberOfPossibleShifts]; + for (unsigned i = 0; i < numberOfPossibleShifts; i++) + possibleShift[i] = false; + + unsigned minShift, maxShift; + shift.getUnsignedMinMax(minShift,maxShift); + + // The shift must be less than the position of the first one in the output + int positionOfFirstOne = -1; + for (unsigned i = 0; i < bitWidth; i++) + { + if (output.isFixed(i) && output.getValue(i)) + { + positionOfFirstOne = i; + break; + } + } + + if (positionOfFirstOne >= 0) + { + if ((unsigned) positionOfFirstOne < minShift) + return CONFLICT; + + maxShift = std::min(maxShift, (unsigned) positionOfFirstOne); + } + + for (unsigned i = minShift; i <= std::min(bitWidth, maxShift); i++) + { + // if the bit-pattern of 'i' is in the set represented by the 'shift'. + if (shift.unsignedHolds(i)) + possibleShift[i] = true; + } + + // Complication. Given a shift like [-1]. possibleShift[2] is now false. + // A shift of 2 isn't possible. But one of three is. + // possibleShift[2] means any shift >=2 is possible. So it needs to be set + // to true. + { + if (maxShift >= bitWidth) + possibleShift[bitWidth] = true; + } + + // Now check one-by-one each shifting. + // If we are shifting a zero to where a one is (say), then that shifting isn't possible. + for (unsigned shiftIt = 0; shiftIt < numberOfPossibleShifts; shiftIt++) + { + if (possibleShift[shiftIt]) + { + for (unsigned column = 0; column < bitWidth; column++) + { + if (column < shiftIt) + { + if (output.isFixed(column) && output.getValue(column)) // output is one in the column. That's wrong. + { + possibleShift[shiftIt] = false; + break; + } + } + else + { + // if they are fixed to different values. That's wrong. + if (output.isFixed(column) && op.isFixed(column - shiftIt) && (output.getValue(column) != op.getValue(column - shiftIt))) + { + possibleShift[shiftIt] = false; + break; + } + } + } + } + } + + int nOfPossibleShifts = 0; + int shiftIndex = 0; + for (unsigned i = 0; i < numberOfPossibleShifts; i++) + { + if (possibleShift[i]) + { + nOfPossibleShifts++; + shiftIndex = i; + if (debug_shift) + { + std::cerr << "Possible:" << i << std::endl; + } + } + } + + if (debug_shift) + { + std::cerr << "Number of possible shifts:" << nOfPossibleShifts << endl; + } + + // If it's empty. It's a conflict. + if (0 == nOfPossibleShifts) + return CONFLICT; + + // We have a list of all the possible shift amounts. + // We take the union of all the bits that are possible. + + FixedBits v(bitWidth, false); + bool first = true; + for (unsigned i = 0; i < numberOfPossibleShifts-1; i++) + { + if (possibleShift[i]) + { + if (first) + { + first = false; + for (unsigned j = 0; j < (unsigned) v.getWidth(); j++) + { + v.setFixed(j, true); + if (j < sizeof(unsigned)*8) + v.setValue(j, 0 != (i & (1 << j))); + else + v.setValue(j, false); + } + } + else + { + // join. + for (unsigned j = 0; j < (unsigned) v.getWidth() && j < sizeof(unsigned)*8; j++) + { + if (v.isFixed(j)) + { + // union. + if (v.getValue(j) != (0!=(i & (1 << j)))) + v.setFixed(j, false); + } + } + } + } + } + + // The top most entry of the shift table is special. It means all values of shift + // that fill it completely with zeroes. We take the union of all of the values >bitWidth + // in this function. + if (possibleShift[numberOfPossibleShifts - 1]) + { + FixedBits bitWidthFB = FixedBits::fromUnsignedInt(bitWidth, bitWidth); + FixedBits output(1, true); + output.setFixed(0, true); + output.setValue(0, true); + FixedBits working(shift); + + vector args; + args.push_back(&working); + args.push_back(&bitWidthFB); + + //Write into working anything that can be determined given it's >=bitWidth. + Result r = bvGreaterThanEqualsBothWays(args,output); + assert(CONFLICT != r); + + // Get the union of "working" with the prior union. + for (unsigned i = 0; i < bitWidth; i++) + { + if (!working.isFixed(i) && v.isFixed(i)) + v.setFixed(i, false); + if (working.isFixed(i) && v.isFixed(i) && (working.getValue(i) != v.getValue(i))) + v.setFixed(i, false); + if (first) // no less shifts possible. + { + if (working.isFixed(i)) + { + v.setFixed(i, true); + v.setValue(i, working.getValue(i)); + } + } + } + } + + if (debug_shift) + { + std::cerr << "Shift Amount:" << v << std::endl; + } + + for (unsigned i = 0; i < bitWidth; i++) + { + if (v.isFixed(i)) + { + if (!shift.isFixed(i)) + { + shift.setFixed(i, true); + shift.setValue(i, v.getValue(i)); + result = CHANGED; + } + else if (shift.isFixed(i) && shift.getValue(i) != v.getValue(i)) + return CONFLICT; + } + } + + // If a particular input bit appears in every possible shifting, + // and if that bit is unfixed, + // and if the result it is fixed to the same value in every position. + // Then, that bit must be fixed. + // E.g. [--] << [0-] == [00] + + bool candidates[bitWidth]; + for (unsigned i = 0; i < bitWidth; i++) + { + candidates[i] = !op.isFixed(i); + } + + // candidates: So far: the bits that are unfixed. + + for (unsigned i = 0; i < numberOfPossibleShifts; i++) + { + if (possibleShift[i]) + { + // If this shift is possible, then some bits will be shifted out. + for (unsigned j = 0; j < i; j++) + candidates[bitWidth - 1 - j] = false; + } + } + + // candidates: So far: + the input bits that are unfixed. + // + the input bits that are in every possible fixing. + + // Check all candidates have the same output values. + for (unsigned candidate = 0; candidate < bitWidth; candidate++) + { + bool first = true; + bool setTo = false; // value that's never read. To quieten gcc. + + if (candidates[candidate]) + { + for (unsigned shiftIT = 0; shiftIT < bitWidth; shiftIT++) + { + // If the shift isn't possible continue. + if (!possibleShift[shiftIT]) + continue; + + unsigned idx = candidate + shiftIT; + + if (!output.isFixed(idx)) + { + candidates[candidate] = false; + break; + } + else + { + if (first) + { + first = false; + setTo = output.getValue(idx); + } + else + { + if (setTo != output.getValue(idx)) + { + candidates[candidate] = false; + break; + } + + } + } + } + } + + if (candidates[candidate]) + { + assert(!op.isFixed(candidate)); + op.setFixed(candidate, true); + op.setValue(candidate, setTo); + } + } + + // done. + + // Go through each of the possible shifts. If the same value is fixed + // at every location. Then it's fixed too in the result. + for (unsigned column = 0; column < bitWidth; column++) + { + bool allFixedToSame = true; + bool allFixedTo = false; // value that's never read. To quieten gcc. + bool first = true; + + for (unsigned shiftIt = minShift; (shiftIt < numberOfPossibleShifts) && allFixedToSame; shiftIt++) + { + if (possibleShift[shiftIt]) + { + // Will have shifted in zeroes. + if (shiftIt > column) + { + if (first) + { + allFixedTo = false; + first = false; + } + else + { + if (allFixedTo) + { + allFixedToSame = false; + } + } + } + else + { + unsigned index = column - shiftIt; + if (!op.isFixed(index)) + allFixedToSame = false; + else if (first && op.isFixed(index)) + { + first = false; + allFixedTo = op.getValue(index); + } + if (op.isFixed(index) && allFixedTo != op.getValue(index)) + allFixedToSame = false; + } + } + } + + // If it can be just one possible value. Then we can fix 'em. + if (allFixedToSame) + { + if (output.isFixed(column) && (output.getValue(column) != allFixedTo)) + return CONFLICT; + if (!output.isFixed(column)) + { + output.setFixed(column, true); + output.setValue(column, allFixedTo); + result = CHANGED; + } + } + } + + /* + // If there is only one possible shift value. Then, we can push from the output back. + if (1 == nOfPossibleShifts) + { + for (unsigned i = shiftIndex; i < bitWidth; i++) + { + if (!op.isFixed(i - shiftIndex) && output.isFixed(i)) + { + op.setFixed(i - shiftIndex, true); + op.setValue(i - shiftIndex, output.getValue(i)); + result = CHANGED; + } + } + } +*/ + + return NOT_IMPLEMENTED; +} + +} +} diff --git a/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp b/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp new file mode 100644 index 0000000..6233809 --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp @@ -0,0 +1,460 @@ +#include "ConstantBitP_TransferFunctions.h" +#include "ConstantBitP_Utility.h" + +namespace simplifier +{ +namespace constantBitP +{ + +namespace BEEV +{ +typedef unsigned int * CBV; +} + +// Misc (easy) transfer functions. +// Trevor Hansen. BSD License. + +// if the result is fixed to true. Then fix a==b. +// if the result is fixed to false, there is a single unspecied value, and all the rest are the same. Fix it to the opposite. + +// if a==b then fix the result to true. +// if a!=b then fix the result to false. +Result bvEqualsBothWays(FixedBits& a, FixedBits& b, FixedBits& output) +{ + assert(a.getWidth() == b.getWidth()); + assert(1 == output.getWidth()); + + const int childWidth = a.getWidth(); + + Result r = NO_CHANGE; + + bool allSame = true; + bool definatelyFalse = false; + + for (int i = 0; i < childWidth; i++) + { + // if both fixed + if (a.isFixed(i) && b.isFixed(i)) + { + // And have different values. + if (a.getValue(i) != b.getValue(i)) + { + definatelyFalse = true; + } + else + { + allSame &= true; + continue; + } + } + allSame &= false; + } + + if (definatelyFalse) + { + if (output.isFixed(0) && output.getValue(0)) + { + return CONFLICT; + } + else if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, false); + r = CHANGED; + } + } + else if (allSame) + { + if (output.isFixed(0) && !output.getValue(0)) + { + return CONFLICT; + } + else if (!output.isFixed(0)) + { + output.setFixed(0, true); + output.setValue(0, true); + r = CHANGED; + } + } + + if (output.isFixed(0) && output.getValue(0)) // all should be the same. + { + for (int i = 0; i < childWidth; i++) + { + if (a.isFixed(i) && b.isFixed(i)) + { + if (a.getValue(i) != b.getValue(i)) + { + return CONFLICT; + } + } + else if (a.isFixed(i) != b.isFixed(i)) // both same but only one is fixed. + { + if (a.isFixed(i)) + { + b.setFixed(i, true); + b.setValue(i, a.getValue(i)); + r = CHANGED; + } + else + { + a.setFixed(i, true); + a.setValue(i, b.getValue(i)); + r = CHANGED; + } + } + } + } + + // if the result is fixed to false, there is a single unspecied value, and all the rest are the same. Fix it to the opposite. + if (output.isFixed(0) && !output.getValue(0)) + { + int unknown = 0; + + for (int i = 0; i < childWidth; i++) + { + if (!a.isFixed(i)) + unknown++; + if (!b.isFixed(i)) + unknown++; + else if (a.isFixed(i) && b.isFixed(i) && a.getValue(i) != b.getValue(i)) + { + unknown = 10; // hack, don't do the next loop. + break; + } + } + + if (1 == unknown) + { + for (int i = 0; i < childWidth; i++) + { + if (!a.isFixed(i)) + { + a.setFixed(i, true); + a.setValue(i, !b.getValue(i)); + r = CHANGED; + } + if (!b.isFixed(i)) + { + b.setFixed(i, true); + b.setValue(i, !a.getValue(i)); + r = CHANGED; + } + } + } + } + return r; +} + +Result bvEqualsBothWays(vector& children, FixedBits& result) +{ + return bvEqualsBothWays(*(children[0]), *(children[1]), result); +} + +Result bvZeroExtendBothWays(vector& children, FixedBits& output) +{ + assert(children.size() ==2 ); + // The second argument is a junk size arugment. + + + FixedBits& input = *children[0]; + const int inputBitWidth = input.getWidth(); + const int outputBitWidth = output.getWidth(); + + Result result = makeEqual(input, output, 0, inputBitWidth); + if (CONFLICT == result) + return CONFLICT; + + // Fix all the topmost bits of the output to zero. + for (int i = inputBitWidth; i < outputBitWidth; i++) + { + if (output.isFixed(i) && output.getValue(i)) + return CONFLICT; // set to one. Never right. + else if (!output.isFixed(i)) + { + output.setFixed(i, true); + output.setValue(i, false); + result = CHANGED; + } + } + return result; +} + +Result bvSignExtendBothWays(vector& children, FixedBits& output) +{ + assert(children.size() ==2 ); + // The second argument is a junk size arugment. + + FixedBits& input = *children[0]; + const int inputBitWidth = input.getWidth(); + const int outputBitWidth = output.getWidth(); + assert(inputBitWidth <= outputBitWidth); + + Result result = makeEqual(input, output, 0, inputBitWidth); + if (CONFLICT == result) + return CONFLICT; + + // If any of the topmost bits of the output are fixed. Then they all should be. + // They should all be fixed to the same value. + bool found = false; + bool setTo; + for (int i = inputBitWidth - /**/1 /**/; i < outputBitWidth; i++) + { + if (output.isFixed(i)) + { + setTo = output.getValue(i); + found = true; + break; + } + } + + if (found) + { + for (int i = inputBitWidth - 1; i < outputBitWidth; i++) + { + if (output.isFixed(i) && (output.getValue(i) != setTo)) + return CONFLICT; // if any are set to the wrong value! bad. + else if (!output.isFixed(i)) + { + output.setFixed(i, true); + output.setValue(i, setTo); + result = CHANGED; + } + } + + Result result2 = makeEqual(input, output, 0, inputBitWidth); + if (CONFLICT == result2) + return CONFLICT; + + } + return result; +} + +Result bvExtractBothWays(vector& children, FixedBits& output) +{ + const int numberOfChildren = children.size(); + const int outputBitWidth = output.getWidth(); + + Result result = NO_CHANGE; + + assert(3 == numberOfChildren); + + int top = children[1]->getUnsignedValue(); + int bottom = children[2]->getUnsignedValue(); + + FixedBits& input = *(children[0]); + + assert(top >= bottom); + assert(bottom >=0); + assert(top - bottom + 1 == outputBitWidth); + assert(top < input.getWidth()); + + for (int outputPosition = 0; outputPosition < outputBitWidth; outputPosition++) + { + int inputPosition = outputPosition + bottom; + + if (input.isFixed(inputPosition) && output.isFixed(outputPosition)) + if (input.getValue(inputPosition) ^ output.getValue(outputPosition)) + return CONFLICT; + + if (input.isFixed(inputPosition) ^ output.isFixed(outputPosition)) + { + if (input.isFixed(inputPosition)) + { + output.setFixed(outputPosition, true); + output.setValue(outputPosition, input.getValue(inputPosition)); + result = CHANGED; + } + else + { + input.setFixed(inputPosition, true); + input.setValue(inputPosition, output.getValue(outputPosition)); + result = CHANGED; + } + } + } + + //cerr << "extract[" << top << ":" << bottom << "]" << input << "=" << output<< endl; + + return result; +} + +// UMINUS, is NEG followed by +1 +Result bvUnaryMinusBothWays(vector& children, FixedBits& output) +{ + assert(children.size() == 1); + const int bitWidth = children[0]->getWidth(); + + // If it's only one bit. This will be negative one. + FixedBits one(bitWidth, false); + one.fixToZero(); + one.setFixed(0, true); + one.setValue(0, true); + + FixedBits notted(bitWidth, false); + + vector args; + args.push_back(¬ted); + args.push_back(&one); + + Result result = NO_CHANGE; + while (true) // until it fixed points + { + FixedBits initialNot(notted); + FixedBits initialIn(*children[0]); + FixedBits initialOut(output); + + result = bvNotBothWays(*children[0], notted); + if (CONFLICT == result) + return CONFLICT; + + result = bvAddBothWays(args, output); + if (CONFLICT == result) + return CONFLICT; + + if (FixedBits::equals(initialNot, notted) && FixedBits::equals(initialIn, *children[0]) && FixedBits::equals(initialOut, output)) + break; + } + + return NOT_IMPLEMENTED; // don't set the status properly yet.. +} + +Result bvConcatBothWays(vector& children, FixedBits& output) +{ + Result r = NO_CHANGE; + const int numberOfChildren = children.size(); + int current = 0; + for (int i = numberOfChildren - 1; i >= 0; i--) // least significant is last. + + { + FixedBits& child = *children[i]; + for (int j = 0; j < child.getWidth(); j++) + { + // values are different. Bad. + if (output.isFixed(current) && child.isFixed(j) && (output.getValue(current) != child.getValue(j))) + return CONFLICT; + + if (output.isFixed(current) && !child.isFixed(j)) + { + // only output is fixed. + child.setFixed(j, true); + child.setValue(j, output.getValue(current)); + r = CHANGED; + } + else if (!output.isFixed(current) && child.isFixed(j)) + { + // only input is fixed. + output.setFixed(current, true); + output.setValue(current, child.getValue(j)); + r = CHANGED; + } + current++; + } + } + return r; +} + +// If the guard is fixed, make equal the appropriate input and output. +// If one input can not possibly be the output. Then set the guard to make it the other one. +// If both values are the same. Set the output to that value. +Result bvITEBothWays(vector& children, FixedBits& output) +{ + Result result = NO_CHANGE; + + assert(3 == children.size()); + const int bitWidth = output.getWidth(); + FixedBits& guard = *children[0]; + FixedBits& c1 = *children[1]; + FixedBits& c2 = *children[2]; + + assert(c1.getWidth() == c2.getWidth()); + assert(output.getWidth() == c2.getWidth()); + + if (guard.isFixed(0) && guard.getValue(0)) + { // guard fixed to true. So make (first arg == output) + result = makeEqual(output, c1, 0, bitWidth); + if (CONFLICT == result) + return CONFLICT; + + } + else if (guard.isFixed(0) && !guard.getValue(0)) + { + result = makeEqual(output, c2, 0, bitWidth); + if (CONFLICT == result) + return CONFLICT; + + } + else + { + for (int i = 0; i < bitWidth; i++) + { + if (c1.isFixed(i) && c2.isFixed(i) && (c1.getValue(i) == c2.getValue(i))) + { + + if (output.isFixed(i) && (output.getValue(i) != c1.getValue(i))) + return CONFLICT; + + if (!output.isFixed(i)) + { + output.setFixed(i, true); + output.setValue(i, c1.getValue(i)); + result = CHANGED; + } + } + } + } + + bool changed = false; + if (CHANGED == result) + changed = true; + + for (int i = 0; i < bitWidth; i++) + { + if (output.isFixed(i)) + { + if (c1.isFixed(i) && (c1.getValue(i) != output.getValue(i))) + { + //c1 is fixed to a value that's not the same as the output. + if (!guard.isFixed(0)) + { + guard.setFixed(0, true); + guard.setValue(0, false); + result = bvITEBothWays(children, output); + if (CONFLICT == result) + return CONFLICT; + changed = true; + } + else if (guard.getValue(0)) + return CONFLICT; + } + + if (c2.isFixed(i) && (c2.getValue(i) != output.getValue(i))) + { + //c2 is fixed to a value that's not the same as the output. + if (!guard.isFixed(0)) + { + guard.setFixed(0, true); + guard.setValue(0, true); + result = bvITEBothWays(children, output); + if (CONFLICT == result) + return CONFLICT; + changed = true; + + } + else if (!guard.getValue(0)) + return CONFLICT; + } + } + } + + if (result == CONFLICT) + return CONFLICT; + if (changed) + return CHANGED; + + return result; +} + +} + +} diff --git a/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.h b/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.h new file mode 100644 index 0000000..5053b23 --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.h @@ -0,0 +1,82 @@ +/* + * ConstantBitPropagation_TransferFunctions.h + * + */ +// Trevor Hansen. BSD License. + +#ifndef CONSTANTBITPROPAGATION_TRANSFERFUNCTIONS_H_ +#define CONSTANTBITPROPAGATION_TRANSFERFUNCTIONS_H_ + +#include "ConstantBitPropagation.h" +namespace simplifier +{ +namespace constantBitP +{ +class MultiplicationStats; + +// Multiply is not yet maximally precise. +//!!!!!!! +Result bvMultiplyBothWays(vector& children, FixedBits& output, BEEV::STPMgr* bm, MultiplicationStats* ms = NULL); +Result bvUnsignedDivisionBothWays(vector& children, FixedBits& output, BEEV::STPMgr* bm); +Result bvUnsignedModulusBothWays(vector& children, FixedBits& output, BEEV::STPMgr* bm); +Result bvSignedDivisionBothWays(vector& children, FixedBits& output, BEEV::STPMgr* bm); +Result bvSignedRemainderBothWays(vector& children, FixedBits& output, BEEV::STPMgr* bm); +Result bvSignedModulusBothWays(vector& children, FixedBits& output, BEEV::STPMgr* bm); +//!!!!!!! + + +// BOTH WAY FUNCTIONS..-------MAXIMALLY PRECISE.......... +Result bvEqualsBothWays(vector& children, FixedBits& output); + +Result bvAndBothWays(vector& operands, FixedBits& output); + +Result bvOrBothWays(vector& children, FixedBits& output); +Result bvXorBothWays(vector& children, FixedBits& output); + +Result bvImpliesBothWays(vector& children, FixedBits& result); + +Result bvAddBothWays(vector& children, FixedBits& output); +Result bvSubtractBothWays(vector& children, FixedBits& output); + +Result bvNotBothWays(FixedBits& a, FixedBits& output); +Result bvNotBothWays(vector& children, FixedBits& output); + +Result bvITEBothWays(vector& children, FixedBits& output); + +Result bvExtractBothWays(vector& children, FixedBits& output); + +Result bvConcatBothWays(vector& children, FixedBits& output); + +Result bvSignExtendBothWays(vector& children, FixedBits& output); +Result bvZeroExtendBothWays(vector& children, FixedBits& output); + +Result bvUnaryMinusBothWays(vector& children, FixedBits& output); + +Result bvLeftShiftBothWays(vector& children, FixedBits& output); +Result bvRightShiftBothWays(vector& children, FixedBits& output); +Result bvArithmeticRightShiftBothWays(vector& children, FixedBits& output); + +// FOUR signed operations. +Result bvSignedGreaterThanBothWays(vector& children, FixedBits& output); + +Result bvSignedLessThanBothWays(vector& children, FixedBits& output); + +Result bvSignedLessThanEqualsBothWays(vector& children, FixedBits& output); + +Result bvSignedGreaterThanEqualsBothWays(vector& children, FixedBits& output); + +// FOUR unsigned operations. + +Result bvLessThanBothWays(vector& children, FixedBits& output); +Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output); + +Result bvLessThanEqualsBothWays(vector& children, FixedBits& output); + +Result bvGreaterThanBothWays(vector& children, FixedBits& output); + +Result bvGreaterThanEqualsBothWays(vector& children, FixedBits& output); + +} +} + +#endif /* CONSTANTBITPROPAGATION_TRANSFERFUNCTIONS_H_ */ diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp index b81f023..192aad0 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp +++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp @@ -619,8 +619,6 @@ namespace simplifier assert(!n.isConstant()); -#ifdef WITHCBITP - Result(*transfer)(vector&, FixedBits&); switch (k) @@ -673,6 +671,7 @@ namespace simplifier MAPTFN(ITE,bvITEBothWays) MAPTFN(BVCONCAT, bvConcatBothWays) +#ifdef WITHCBITP case BVMULT: // handled specially later. case BVDIV: case BVMOD: @@ -681,6 +680,7 @@ namespace simplifier case SBVMOD: transfer = NULL; break; +#endif default: { notHandled(k); @@ -690,6 +690,7 @@ namespace simplifier #undef MAPTFN bool mult_like = false; +#ifdef WITHCBITP // safe approximation to no overflow multiplication. if (k == BVMULT) { @@ -725,6 +726,7 @@ namespace simplifier mult_like=true; } else +#endif result = transfer(children, output); if (mult_like && output_mult_like) @@ -734,7 +736,6 @@ namespace simplifier cerr << *children[1] << std::endl; } -#endif return result; } -- 2.47.3