cloud9_root/src/third_party/stp/src/simplifier/simplifier.cpp
// If both of the children are sign extended. Makes this node sign extended too.
If both of the children are sign extended. Makes this node sign extended too.
If both of the children are sign extended . Makes this node sign extended too .
ASTNode
  Simplifier::pullUpBVSX(ASTNode output)
  {
    assert(output.GetChildren().size() ==2);
    assert(output[0].GetKind() == BVSX);
    assert(output[1].GetKind() == BVSX);
    const Kind k = output.GetKind();
    assert(BVMULT == k || SBVDIV == k || BVPLUS ==k);
    const int inputValueWidth = output.GetValueWidth();
    int lengthA = output.GetChildren()[0][0].GetValueWidth();
    int lengthB = output.GetChildren()[1][0].GetValueWidth();
    int maxLength;
    if (BVMULT == output.GetKind())
      maxLength = lengthA + lengthB;
    else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind())
      maxLength = std::max(lengthA, lengthB) + 1;
    else
      FatalError("Unexpected.");
    if (maxLength < output.GetValueWidth())
      {
        ASTNode newA = nf->CreateTerm(BVEXTRACT, maxLength, output.GetChildren()[0],
            _bm->CreateBVConst(32, maxLength - 1), _bm->CreateZeroConst(32));
        newA = SimplifyTerm(newA);
        ASTNode newB = nf->CreateTerm(BVEXTRACT, maxLength, output.GetChildren()[1],
            _bm->CreateBVConst(32, maxLength - 1), _bm->CreateZeroConst(32));
        newB = SimplifyTerm(newB);
        ASTNode mult = nf->CreateTerm(output.GetKind(), maxLength, newA, newB);
        output = nf->CreateTerm(BVSX, inputValueWidth, mult, _bm->CreateBVConst(32, inputValueWidth));
      }
    return output;
  }
ASTNode Simplifier :: pullUpBVSX ( ASTNode output ) { assert ( output . GetChildren ( ) . size ( ) == 2 ) ; assert ( output [ 0 ] . GetKind ( ) == BVSX ) ; assert ( output [ 1 ] . GetKind ( ) == BVSX ) ; const Kind k = output . GetKind ( ) ; assert ( BVMULT == k || SBVDIV == k || BVPLUS == k ) ; const int inputValueWidth = output . GetValueWidth ( ) ; int lengthA = output . GetChildren ( ) [ 0 ] [ 0 ] . GetValueWidth ( ) ; int lengthB = output . GetChildren ( ) [ 1 ] [ 0 ] . GetValueWidth ( ) ; int maxLength ; if ( BVMULT == output . GetKind ( ) ) maxLength = lengthA + lengthB ; else if ( BVPLUS == output . GetKind ( ) || SBVDIV == output . GetKind ( ) ) maxLength = std :: max ( lengthA , lengthB ) + 1 ; else FatalError ( " " ) ; if ( maxLength < output . GetValueWidth ( ) ) { ASTNode newA = nf -> CreateTerm ( BVEXTRACT , maxLength , output . GetChildren ( ) [ 0 ] , _bm -> CreateBVConst ( 32 , maxLength - 1 ) , _bm -> CreateZeroConst ( 32 ) ) ; newA = SimplifyTerm ( newA ) ; ASTNode newB = nf -> CreateTerm ( BVEXTRACT , maxLength , output . GetChildren ( ) [ 1 ] , _bm -> CreateBVConst ( 32 , maxLength - 1 ) , _bm -> CreateZeroConst ( 32 ) ) ; newB = SimplifyTerm ( newB ) ; ASTNode mult = nf -> CreateTerm ( output . GetKind ( ) , maxLength , newA , newB ) ; output = nf -> CreateTerm ( BVSX , inputValueWidth , mult , _bm -> CreateBVConst ( 32 , inputValueWidth ) ) ; } return output ; }
If both of the children are sign extended.
If both of the children are sign extended .