diff options
Diffstat (limited to 'src/expr/pickler.cpp')
-rw-r--r-- | src/expr/pickler.cpp | 477 |
1 files changed, 477 insertions, 0 deletions
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp new file mode 100644 index 000000000..f09c552d1 --- /dev/null +++ b/src/expr/pickler.cpp @@ -0,0 +1,477 @@ +/********************* */ +/*! \file pickler.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a "pickler" for expressions + ** + ** This is a "pickler" for expressions. It produces a binary + ** serialization of an expression that can be converted back + ** into an expression in the same or another ExprManager. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/pickler.h" +#include "expr/pickle_data.h" +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/node_value.h" +#include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" +#include "util/Assert.h" +#include "expr/kind.h" +#include "expr/metakind.h" +#include "util/output.h" + +namespace CVC4 { +namespace expr { +namespace pickle { + +class PicklerPrivate { +public: + typedef std::stack<Node> NodeStack; + NodeStack d_stack; + + PickleData d_current; + + Pickler& d_pickler; + + NodeManager* const d_nm; + + PicklerPrivate(Pickler& pickler, ExprManager* em) : + d_pickler(pickler), + d_nm(NodeManager::fromExprManager(em)) { + } + + bool atDefaultState(){ + return d_stack.empty() && d_current.empty(); + } + + /* Helper functions for toPickle */ + void toCaseNode(TNode n) throw(AssertionException, PicklingException); + void toCaseVariable(TNode n) throw(AssertionException, PicklingException); + void toCaseConstant(TNode n); + void toCaseOperator(TNode n) throw(AssertionException, PicklingException); + void toCaseString(Kind k, const std::string& s); + + /* Helper functions for toPickle */ + Node fromCaseOperator(Kind k, uint32_t nchildren); + Node fromCaseConstant(Kind k, uint32_t nblocks); + std::string fromCaseString(uint32_t nblocks); + Node fromCaseVariable(Kind k); + +};/* class PicklerPrivate */ + +static Block mkBlockBody4Chars(char a, char b, char c, char d) { + Block newBody; + newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d; + return newBody; +} + +static char getCharBlockBody(BlockBody body, int i) { + Assert(0 <= i && i <= 3); + + switch(i) { + case 0: return (body.d_data & 0xff000000) >> 24; + case 1: return (body.d_data & 0x00ff0000) >> 16; + case 2: return (body.d_data & 0x0000ff00) >> 8; + case 3: return (body.d_data & 0x000000ff); + default: + Unreachable(); + } + return '\0'; +} + +static Block mkBlockBody(unsigned data) { + Block newBody; + newBody.d_body.d_data = data; + return newBody; +} + +static Block mkOperatorHeader(Kind k, unsigned numChildren) { + Block newHeader; + newHeader.d_headerOperator.d_kind = k; + newHeader.d_headerOperator.d_nchildren = numChildren; + return newHeader; +} + +static Block mkVariableHeader(Kind k) { + Block newHeader; + newHeader.d_header.d_kind = k; + return newHeader; +} + +static Block mkConstantHeader(Kind k, unsigned numBlocks) { + Block newHeader; + newHeader.d_headerConstant.d_kind = k; + newHeader.d_headerConstant.d_constblocks = numBlocks; + return newHeader; +} + +Pickler::Pickler(ExprManager* em) : + d_private(new PicklerPrivate(*this, em)) { +} + +Pickler::~Pickler() { + delete d_private; +} + +void Pickler::toPickle(Expr e, Pickle& p) + throw(AssertionException, PicklingException) { + Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm); + Assert(d_private->atDefaultState()); + + try{ + d_private->d_current.swap(*p.d_data); + d_private->toCaseNode(e.getTNode()); + d_private->d_current.swap(*p.d_data); + }catch(PicklingException& pe){ + d_private->d_current = PickleData(); + Assert(d_private->atDefaultState()); + throw pe; + } + + Assert(d_private->atDefaultState()); +} + +void PicklerPrivate::toCaseNode(TNode n) + throw(AssertionException, PicklingException) { + Debug("pickler") << "toCaseNode: " << n << std::endl; + Kind k = n.getKind(); + kind::MetaKind m = metaKindOf(k); + switch(m) { + case kind::metakind::CONSTANT: + toCaseConstant(n); + break; + case kind::metakind::VARIABLE: + toCaseVariable(n); + break; + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + toCaseOperator(n); + break; + default: + Unhandled(m); + } +} + +void PicklerPrivate::toCaseOperator(TNode n) + throw(AssertionException, PicklingException) { + Kind k = n.getKind(); + kind::MetaKind m = metaKindOf(k); + Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR); + if(m == kind::metakind::PARAMETERIZED) { + toCaseNode(n.getOperator()); + } + for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { + toCaseNode(*i); + } + d_current << mkOperatorHeader(k, n.getNumChildren()); +} + +void PicklerPrivate::toCaseVariable(TNode n) + throw(AssertionException, PicklingException) { + Kind k = n.getKind(); + Assert(metaKindOf(k) == kind::metakind::VARIABLE); + + const NodeValue* nv = n.d_nv; + uint64_t asInt = reinterpret_cast<uint64_t>(nv); + uint64_t mapped = d_pickler.variableToMap(asInt); + + uint32_t firstHalf = mapped >> 32; + uint32_t secondHalf = mapped & 0xffffffff; + + d_current << mkVariableHeader(k); + d_current << mkBlockBody(firstHalf); + d_current << mkBlockBody(secondHalf); +} + + +void PicklerPrivate::toCaseConstant(TNode n) { + Kind k = n.getKind(); + Assert(metaKindOf(k) == kind::metakind::CONSTANT); + switch(k) { + case kind::CONST_BOOLEAN: + d_current << mkConstantHeader(k, 1); + d_current << mkBlockBody(n.getConst<bool>()); + break; + case kind::CONST_INTEGER: + case kind::CONST_RATIONAL: { + std::string asString; + if(k == kind::CONST_INTEGER) { + const Integer& i = n.getConst<Integer>(); + asString = i.toString(16); + } else { + Assert(k == kind::CONST_RATIONAL); + const Rational& q = n.getConst<Rational>(); + asString = q.toString(16); + } + toCaseString(k, asString); + break; + } + case kind::BITVECTOR_EXTRACT_OP: { + BitVectorExtract bve = n.getConst<BitVectorExtract>(); + d_current << mkConstantHeader(k, 2); + d_current << mkBlockBody(bve.high); + d_current << mkBlockBody(bve.low); + break; + } + case kind::CONST_BITVECTOR: { + // irritating: we incorporate the size of the string in with the + // size of this constant, so it appears as one big constant and + // doesn't confuse anybody + BitVector bv = n.getConst<BitVector>(); + std::string asString = bv.getValue().toString(16); + d_current << mkConstantHeader(k, 2 + asString.size()); + d_current << mkBlockBody(bv.getSize()); + toCaseString(k, asString); + break; + } + default: + Unhandled(k); + } +} + +void PicklerPrivate::toCaseString(Kind k, const std::string& s) { + d_current << mkConstantHeader(k, s.size()); + + unsigned size = s.size(); + unsigned i; + for(i = 0; i + 4 <= size; i += 4) { + d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]); + } + switch(size % 4) { + case 0: break; + case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break; + case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break; + case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break; + default: + Unreachable(); + } + +} + +void Pickler::debugPickleTest(Expr e) { + + //ExprManager *em = e.getExprManager(); + //Expr e1 = mkVar("x", makeType()); + //return ; + + Pickler pickler(e.getExprManager()); + + Pickle p; + pickler.toPickle(e, p); + + uint32_t size = p.d_data->size(); + std::string str = p.d_data->toString(); + + Expr from = pickler.fromPickle(p); + ExprManagerScope ems(e); + + Debug("pickle") << "before: " << e << std::endl; + Debug("pickle") << "after: " << from.getNode() << std::endl; + Debug("pickle") << "pickle: (oct) "<< size << " " << str.length() << " " << str << std::endl; + + Assert(p.d_data->empty()); + Assert(e == from); +} + +Expr Pickler::fromPickle(Pickle& p) { + Assert(d_private->atDefaultState()); + + d_private->d_current.swap(*p.d_data); + + while(!d_private->d_current.empty()) { + Block front = d_private->d_current.dequeue(); + + Kind k = (Kind)front.d_header.d_kind; + kind::MetaKind m = metaKindOf(k); + + Node result = Node::null(); + switch(m) { + case kind::metakind::VARIABLE: + result = d_private->fromCaseVariable(k); + break; + case kind::metakind::CONSTANT: + result = d_private->fromCaseConstant(k, front.d_headerConstant.d_constblocks); + break; + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + result = d_private->fromCaseOperator(k, front.d_headerOperator.d_nchildren); + break; + default: + Unhandled(m); + } + Assert(result != Node::null()); + d_private->d_stack.push(result); + } + + Assert(d_private->d_current.empty()); + Assert(d_private->d_stack.size() == 1); + Node res = d_private->d_stack.top(); + d_private->d_stack.pop(); + + Assert(d_private->atDefaultState()); + + return d_private->d_nm->toExpr(res); +} + +Node PicklerPrivate::fromCaseVariable(Kind k) { + Assert(metaKindOf(k) == kind::metakind::VARIABLE); + + Block firstHalf = d_current.dequeue(); + Block secondHalf = d_current.dequeue(); + + uint64_t asInt = firstHalf.d_body.d_data; + asInt = asInt << 32; + asInt = asInt | (secondHalf.d_body.d_data); + + uint64_t mapped = d_pickler.variableFromMap(asInt); + + NodeValue* nv = reinterpret_cast<NodeValue*>(mapped); + Node fromNodeValue(nv); + + Assert(fromNodeValue.getKind() == k); + + return fromNodeValue; +} + +Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) { + switch(k) { + case kind::CONST_BOOLEAN: { + Assert(constblocks == 1); + Block val = d_current.dequeue(); + + bool b= val.d_body.d_data; + return d_nm->mkConst<bool>(b); + } + case kind::CONST_INTEGER: + case kind::CONST_RATIONAL: { + std::string s = fromCaseString(constblocks); + if(k == kind::CONST_INTEGER) { + Integer i(s, 16); + return d_nm->mkConst<Integer>(i); + } else { + Rational q(s, 16); + return d_nm->mkConst<Rational>(q); + } + } + case kind::BITVECTOR_EXTRACT_OP: { + Block high = d_current.dequeue(); + Block low = d_current.dequeue(); + BitVectorExtract bve(high.d_body.d_data, low.d_body.d_data); + return d_nm->mkConst<BitVectorExtract>(bve); + } + case kind::CONST_BITVECTOR: { + unsigned size = d_current.dequeue().d_body.d_data; + Block header CVC4_UNUSED = d_current.dequeue(); + Assert(header.d_headerConstant.d_kind == kind::CONST_BITVECTOR); + Assert(header.d_headerConstant.d_constblocks == constblocks - 2); + Integer value(fromCaseString(constblocks - 2)); + BitVector bv(size, value); + return d_nm->mkConst(bv); + } + default: + Unhandled(k); + } +} + +std::string PicklerPrivate::fromCaseString(uint32_t size) { + std::stringstream ss; + unsigned i; + for(i = 0; i + 4 <= size; i += 4) { + Block front = d_current.dequeue(); + BlockBody body = front.d_body; + + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1) + << getCharBlockBody(body,2) + << getCharBlockBody(body,3); + } + Assert(i == size - (size%4) ); + if(size % 4 != 0) { + Block front = d_current.dequeue(); + BlockBody body = front.d_body; + switch(size % 4) { + case 1: + ss << getCharBlockBody(body,0); + break; + case 2: + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1); + break; + case 3: + ss << getCharBlockBody(body,0) + << getCharBlockBody(body,1) + << getCharBlockBody(body,2); + break; + default: + Unreachable(); + } + } + return ss.str(); +} + +Node PicklerPrivate::fromCaseOperator(Kind k, uint32_t nchildren) { + kind::MetaKind m = metaKindOf(k); + bool parameterized = (m == kind::metakind::PARAMETERIZED); + uint32_t npops = nchildren + (parameterized? 1 : 0); + + NodeStack aux; + while(npops > 0) { + Assert(!d_stack.empty()); + Node top = d_stack.top(); + aux.push(top); + d_stack.pop(); + --npops; + } + + NodeBuilder<> nb(d_nm, k); + while(!aux.empty()) { + Node top = aux.top(); + nb << top; + aux.pop(); + } + + return nb; +} + +Pickle::Pickle() { + d_data = new PickleData(); +} + +// Just copying the pointer isn't right, we have to copy the +// underlying data. Otherwise user-level Pickles will delete the data +// twice! (once in each thread) +Pickle::Pickle(const Pickle& p) { + d_data = new PickleData(*p.d_data); +} + +Pickle& Pickle::operator = (const Pickle& other) { + if (this != &other) { + delete d_data; + d_data = new PickleData(*other.d_data); + } + return *this; +} + + +Pickle::~Pickle() { + delete d_data; +} + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ |