src/expr/pickler.cpp

   1 /*********************                                                        */
   2 /*! \file pickler.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Tim King, Kshitij Bansal
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief This is a "pickler" for expressions
  13  **
  14  ** This is a "pickler" for expressions.  It produces a binary
  15  ** serialization of an expression that can be converted back
  16  ** into an expression in the same or another ExprManager.
  17  **/
  18
  19 #include <iostream>
  20 #include <sstream>
  21 #include <string>
  22
  23 #include "expr/pickler.h"
  24 #include "expr/pickle_data.h"
  25 #include "expr/expr.h"
  26 #include "expr/node.h"
  27 #include "expr/node_manager.h"
  28 #include "expr/node_value.h"
  29 #include "expr/expr_manager_scope.h"
  30 #include "expr/variable_type_map.h"
  31 #include "util/cvc4_assert.h"
  32 #include "expr/kind.h"
  33 #include "expr/metakind.h"
  34 #include "util/output.h"
  35
  36 namespace CVC4 {
  37 namespace expr {
  38 namespace pickle {
  39
  40 class PicklerPrivate {
  41 public:
  42   typedef std::stack<Node> NodeStack;
  43   NodeStack d_stack;
  44
  45   PickleData d_current;
  46
  47   Pickler& d_pickler;
  48
  49   NodeManager* const d_nm;
  50
  51   PicklerPrivate(Pickler& pickler, ExprManager* em) :
  52     d_pickler(pickler),
  53     d_nm(NodeManager::fromExprManager(em)) {
  54   }
  55
  56   bool atDefaultState(){
  57     return d_stack.empty() && d_current.empty();
  58   }
  59
  60   /* Helper functions for toPickle */
  61   void toCaseNode(TNode n) throw(AssertionException, PicklingException);
  62   void toCaseVariable(TNode n) throw(AssertionException, PicklingException);
  63   void toCaseConstant(TNode n);
  64   void toCaseOperator(TNode n) throw(AssertionException, PicklingException);
  65   void toCaseString(Kind k, const std::string& s);
  66
  67   /* Helper functions for toPickle */
  68   Node fromCaseOperator(Kind k, uint32_t nchildren);
  69   Node fromCaseConstant(Kind k, uint32_t nblocks);
  70   std::string fromCaseString(uint32_t nblocks);
  71   Node fromCaseVariable(Kind k);
  72
  73 };/* class PicklerPrivate */
  74
  75 static Block mkBlockBody4Chars(char a, char b, char c, char d) {
  76   Block newBody;
  77   newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d;
  78   return newBody;
  79 }
  80
  81 static char getCharBlockBody(BlockBody body, int i) {
  82   Assert(0 <= i && i <= 3);
  83
  84   switch(i) {
  85   case 0: return (body.d_data & 0xff000000) >> 24;
  86   case 1: return (body.d_data & 0x00ff0000) >> 16;
  87   case 2: return (body.d_data & 0x0000ff00) >> 8;
  88   case 3: return (body.d_data & 0x000000ff);
  89   default:
  90     Unreachable();
  91   }
  92   return '\0';
  93 }
  94
  95 static Block mkBlockBody(unsigned data) {
  96   Block newBody;
  97   newBody.d_body.d_data = data;
  98   return newBody;
  99 }
 100
 101 static Block mkOperatorHeader(Kind k, unsigned numChildren) {
 102   Block newHeader;
 103   newHeader.d_headerOperator.d_kind = k;
 104   newHeader.d_headerOperator.d_nchildren = numChildren;
 105   return newHeader;
 106 }
 107
 108 static Block mkVariableHeader(Kind k) {
 109   Block newHeader;
 110   newHeader.d_header.d_kind = k;
 111   return newHeader;
 112 }
 113
 114 static Block mkConstantHeader(Kind k, unsigned numBlocks) {
 115   Block newHeader;
 116   newHeader.d_headerConstant.d_kind = k;
 117   newHeader.d_headerConstant.d_constblocks = numBlocks;
 118   return newHeader;
 119 }
 120
 121 Pickler::Pickler(ExprManager* em) :
 122   d_private(new PicklerPrivate(*this, em)) {
 123 }
 124
 125 Pickler::~Pickler() {
 126   delete d_private;
 127 }
 128
 129 void Pickler::toPickle(Expr e, Pickle& p)
 130   throw(PicklingException) {
 131   Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm);
 132   Assert(d_private->atDefaultState());
 133
 134   try{
 135     d_private->d_current.swap(*p.d_data);
 136     d_private->toCaseNode(e.getTNode());
 137     d_private->d_current.swap(*p.d_data);
 138   }catch(PicklingException& pe){
 139     d_private->d_current = PickleData();
 140     Assert(d_private->atDefaultState());
 141     throw pe;
 142   }
 143
 144   Assert(d_private->atDefaultState());
 145 }
 146
 147 void PicklerPrivate::toCaseNode(TNode n)
 148   throw(AssertionException, PicklingException) {
 149   Debug("pickler") << "toCaseNode: " << n << std::endl;
 150   Kind k = n.getKind();
 151   kind::MetaKind m = metaKindOf(k);
 152   switch(m) {
 153   case kind::metakind::CONSTANT:
 154     toCaseConstant(n);
 155     break;
 156   case kind::metakind::VARIABLE:
 157     toCaseVariable(n);
 158     break;
 159   case kind::metakind::OPERATOR:
 160   case kind::metakind::PARAMETERIZED:
 161     toCaseOperator(n);
 162     break;
 163   default:
 164     Unhandled(m);
 165   }
 166 }
 167
 168 void PicklerPrivate::toCaseOperator(TNode n)
 169   throw(AssertionException, PicklingException) {
 170   Kind k = n.getKind();
 171   kind::MetaKind m = metaKindOf(k);
 172   Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR);
 173   if(m == kind::metakind::PARAMETERIZED) {
 174     toCaseNode(n.getOperator());
 175   }
 176   for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
 177     toCaseNode(*i);
 178   }
 179   d_current << mkOperatorHeader(k, n.getNumChildren());
 180 }
 181
 182 void PicklerPrivate::toCaseVariable(TNode n)
 183   throw(AssertionException, PicklingException) {
 184   Kind k = n.getKind();
 185   Assert(metaKindOf(k) == kind::metakind::VARIABLE);
 186
 187   const NodeValue* nv = n.d_nv;
 188   uint64_t asInt = reinterpret_cast<uint64_t>(nv);
 189   uint64_t mapped = d_pickler.variableToMap(asInt);
 190
 191   uint32_t firstHalf = mapped >> 32;
 192   uint32_t secondHalf = mapped & 0xffffffff;
 193
 194   d_current << mkVariableHeader(k);
 195   d_current << mkBlockBody(firstHalf);
 196   d_current << mkBlockBody(secondHalf);
 197 }
 198
 199
 200 void PicklerPrivate::toCaseConstant(TNode n) {
 201   Kind k = n.getKind();
 202   Assert(metaKindOf(k) == kind::metakind::CONSTANT);
 203   switch(k) {
 204   case kind::CONST_BOOLEAN:
 205     d_current << mkConstantHeader(k, 1);
 206     d_current << mkBlockBody(n.getConst<bool>());
 207     break;
 208   case kind::CONST_RATIONAL: {
 209     std::string asString;
 210     Assert(k == kind::CONST_RATIONAL);
 211     const Rational& q = n.getConst<Rational>();
 212     asString = q.toString(16);
 213     toCaseString(k, asString);
 214     break;
 215   }
 216   case kind::BITVECTOR_EXTRACT_OP: {
 217     BitVectorExtract bve = n.getConst<BitVectorExtract>();
 218     d_current << mkConstantHeader(k, 2);
 219     d_current << mkBlockBody(bve.high);
 220     d_current << mkBlockBody(bve.low);
 221     break;
 222   }
 223   case kind::CONST_BITVECTOR: {
 224     // irritating: we incorporate the size of the string in with the
 225     // size of this constant, so it appears as one big constant and
 226     // doesn't confuse anybody
 227     BitVector bv = n.getConst<BitVector>();
 228     std::string asString = bv.getValue().toString(16);
 229     d_current << mkConstantHeader(k, 2 + asString.size());
 230     d_current << mkBlockBody(bv.getSize());
 231     toCaseString(k, asString);
 232     break;
 233   }
 234   case  kind::BITVECTOR_SIGN_EXTEND_OP: {
 235     BitVectorSignExtend bvse = n.getConst<BitVectorSignExtend>();
 236     d_current << mkConstantHeader(k, 1);
 237     d_current << mkBlockBody(bvse.signExtendAmount);
 238     break;
 239   }
 240   default:
 241     Unhandled(k);
 242   }
 243 }
 244
 245 void PicklerPrivate::toCaseString(Kind k, const std::string& s) {
 246   d_current << mkConstantHeader(k, s.size());
 247
 248   unsigned size = s.size();
 249   unsigned i;
 250   for(i = 0; i + 4 <= size; i += 4) {
 251     d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]);
 252   }
 253   switch(size % 4) {
 254   case 0: break;
 255   case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break;
 256   case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break;
 257   case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break;
 258   default:
 259     Unreachable();
 260   }
 261
 262 }
 263
 264 void Pickler::debugPickleTest(Expr e) {
 265
 266   //ExprManager *em = e.getExprManager();
 267   //Expr e1 = mkVar("x", makeType());
 268   //return ;
 269
 270   Pickler pickler(e.getExprManager());
 271
 272   Pickle p;
 273   pickler.toPickle(e, p);
 274
 275   uint32_t size = p.d_data->size();
 276   std::string str = p.d_data->toString();
 277
 278   Expr from = pickler.fromPickle(p);
 279   ExprManagerScope ems(e);
 280
 281   Debug("pickle") << "before: " << e << std::endl;
 282   Debug("pickle") << "after: " << from.getNode() << std::endl;
 283   Debug("pickle") << "pickle: (oct) "<< size << " " << str.length() << " " << str << std::endl;
 284
 285   Assert(p.d_data->empty());
 286   Assert(e == from);
 287 }
 288
 289 Expr Pickler::fromPickle(Pickle& p) {
 290   Assert(d_private->atDefaultState());
 291
 292   d_private->d_current.swap(*p.d_data);
 293
 294   while(!d_private->d_current.empty()) {
 295     Block front = d_private->d_current.dequeue();
 296
 297     Kind k = (Kind)front.d_header.d_kind;
 298     kind::MetaKind m = metaKindOf(k);
 299
 300     Node result = Node::null();
 301     switch(m) {
 302     case kind::metakind::VARIABLE:
 303       result = d_private->fromCaseVariable(k);
 304       break;
 305     case kind::metakind::CONSTANT:
 306       result = d_private->fromCaseConstant(k, front.d_headerConstant.d_constblocks);
 307       break;
 308     case kind::metakind::OPERATOR:
 309     case kind::metakind::PARAMETERIZED:
 310       result = d_private->fromCaseOperator(k, front.d_headerOperator.d_nchildren);
 311       break;
 312     default:
 313       Unhandled(m);
 314     }
 315     Assert(result != Node::null());
 316     d_private->d_stack.push(result);
 317   }
 318
 319   Assert(d_private->d_current.empty());
 320   Assert(d_private->d_stack.size() == 1);
 321   Node res = d_private->d_stack.top();
 322   d_private->d_stack.pop();
 323
 324   Assert(d_private->atDefaultState());
 325
 326   return d_private->d_nm->toExpr(res);
 327 }
 328
 329 Node PicklerPrivate::fromCaseVariable(Kind k) {
 330   Assert(metaKindOf(k) == kind::metakind::VARIABLE);
 331
 332   Block firstHalf = d_current.dequeue();
 333   Block secondHalf = d_current.dequeue();
 334
 335   uint64_t asInt = firstHalf.d_body.d_data;
 336   asInt = asInt << 32;
 337   asInt = asInt | (secondHalf.d_body.d_data);
 338
 339   uint64_t mapped = d_pickler.variableFromMap(asInt);
 340
 341   NodeValue* nv = reinterpret_cast<NodeValue*>(mapped);
 342   Node fromNodeValue(nv);
 343
 344   Assert(fromNodeValue.getKind() == k);
 345
 346   return fromNodeValue;
 347 }
 348
 349 Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) {
 350   switch(k) {
 351   case kind::CONST_BOOLEAN: {
 352     Assert(constblocks == 1);
 353     Block val = d_current.dequeue();
 354
 355     bool b= val.d_body.d_data;
 356     return d_nm->mkConst<bool>(b);
 357   }
 358   case kind::CONST_RATIONAL: {
 359     std::string s = fromCaseString(constblocks);
 360     Rational q(s, 16);
 361     return d_nm->mkConst<Rational>(q);
 362   }
 363   case kind::BITVECTOR_EXTRACT_OP: {
 364     Block high = d_current.dequeue();
 365     Block low = d_current.dequeue();
 366     BitVectorExtract bve(high.d_body.d_data, low.d_body.d_data);
 367     return d_nm->mkConst<BitVectorExtract>(bve);
 368   }
 369   case kind::CONST_BITVECTOR: {
 370     unsigned size = d_current.dequeue().d_body.d_data;
 371     Block header CVC4_UNUSED = d_current.dequeue();
 372     Assert(header.d_headerConstant.d_kind == kind::CONST_BITVECTOR);
 373     Assert(header.d_headerConstant.d_constblocks == constblocks - 2);
 374     Integer value(fromCaseString(constblocks - 2));
 375     BitVector bv(size, value);
 376     return d_nm->mkConst(bv);
 377   }
 378   case  kind::BITVECTOR_SIGN_EXTEND_OP: {
 379     Block signExtendAmount = d_current.dequeue();
 380     BitVectorSignExtend bvse(signExtendAmount.d_body.d_data);
 381     return d_nm->mkConst<BitVectorSignExtend>(bvse);
 382   }
 383   default:
 384     Unhandled(k);
 385   }
 386 }
 387
 388 std::string PicklerPrivate::fromCaseString(uint32_t size) {
 389   std::stringstream ss;
 390   unsigned i;
 391   for(i = 0; i + 4 <= size; i += 4) {
 392     Block front = d_current.dequeue();
 393     BlockBody body = front.d_body;
 394
 395     ss << getCharBlockBody(body,0)
 396        << getCharBlockBody(body,1)
 397        << getCharBlockBody(body,2)
 398        << getCharBlockBody(body,3);
 399   }
 400   Assert(i == size - (size%4) );
 401   if(size % 4 != 0) {
 402     Block front = d_current.dequeue();
 403     BlockBody body = front.d_body;
 404     switch(size % 4) {
 405     case 1:
 406       ss << getCharBlockBody(body,0);
 407       break;
 408     case 2:
 409       ss << getCharBlockBody(body,0)
 410          << getCharBlockBody(body,1);
 411       break;
 412     case 3:
 413       ss << getCharBlockBody(body,0)
 414          << getCharBlockBody(body,1)
 415          << getCharBlockBody(body,2);
 416       break;
 417     default:
 418       Unreachable();
 419     }
 420   }
 421   return ss.str();
 422 }
 423
 424 Node PicklerPrivate::fromCaseOperator(Kind k, uint32_t nchildren) {
 425   kind::MetaKind m = metaKindOf(k);
 426   bool parameterized = (m == kind::metakind::PARAMETERIZED);
 427   uint32_t npops = nchildren + (parameterized? 1 : 0);
 428
 429   NodeStack aux;
 430   while(npops > 0) {
 431     Assert(!d_stack.empty());
 432     Node top = d_stack.top();
 433     aux.push(top);
 434     d_stack.pop();
 435     --npops;
 436   }
 437
 438   NodeBuilder<> nb(d_nm, k);
 439   while(!aux.empty()) {
 440     Node top = aux.top();
 441     nb << top;
 442     aux.pop();
 443   }
 444
 445   return nb;
 446 }
 447
 448 Pickle::Pickle() {
 449   d_data = new PickleData();
 450 }
 451
 452 // Just copying the pointer isn't right, we have to copy the
 453 // underlying data.  Otherwise user-level Pickles will delete the data
 454 // twice! (once in each thread)
 455 Pickle::Pickle(const Pickle& p) {
 456   d_data = new PickleData(*p.d_data);
 457 }
 458
 459 Pickle& Pickle::operator = (const Pickle& other) {
 460   if (this != &other) {
 461     delete d_data;
 462     d_data = new PickleData(*other.d_data);
 463   }
 464   return *this;
 465 }
 466
 467
 468 Pickle::~Pickle() {
 469   delete d_data;
 470 }
 471
 472 uint64_t MapPickler::variableFromMap(uint64_t x) const
 473 {
 474   VarMap::const_iterator i = d_fromMap.find(x);
 475   Assert(i != d_fromMap.end());
 476   return i->second;
 477 }
 478
 479 }/* CVC4::expr::pickle namespace */
 480 }/* CVC4::expr namespace */
 481 }/* CVC4 namespace */