src/Serialize/deserializer.cc

   1
   2 /*
   3  * File:   deserializer.cc
   4  * Author: hamed
   5  *
   6  * Created on September 7, 2017, 6:08 PM
   7  */
   8
   9 #include "deserializer.h"
  10 #include "csolver.h"
  11 #include "unistd.h"
  12 #include "fcntl.h"
  13 #include "predicate.h"
  14 #include "table.h"
  15 #include "element.h"
  16 #include "mutableset.h"
  17
  18 #define READBUFFERSIZE 16384
  19
  20 Deserializer::Deserializer(const char *file, InterpreterType itype) :
  21         buffer((char *) ourmalloc(READBUFFERSIZE)),
  22         bufferindex(0),
  23         bufferbytes(0),
  24         buffercap(READBUFFERSIZE),
  25         solver(new CSolver())
  26 {
  27         filedesc = open(file, O_RDONLY);
  28
  29         if (filedesc < 0) {
  30                 exit(-1);
  31         }
  32         if(itype != SATUNE){
  33                 solver->setInterpreter(itype);
  34         }
  35 }
  36
  37 Deserializer::~Deserializer() {
  38         if (-1 == close(filedesc)) {
  39                 exit(-1);
  40         }
  41         ourfree(buffer);
  42 }
  43
  44 ssize_t Deserializer::myread(void *__buf, size_t bytestoread) {
  45         char *out = (char * ) __buf;
  46         size_t totalbytesread = 0;
  47         while (bytestoread) {
  48                 if (bufferbytes != 0) {
  49                         uint bytestocopy = (bufferbytes > bytestoread) ? bytestoread : bufferbytes;
  50                         memcpy(out, &buffer[bufferindex], bytestocopy);
  51                         //update local buffer
  52                         bufferbytes -= bytestocopy;
  53                         bufferindex += bytestocopy;
  54                         totalbytesread += bytestocopy;
  55                         //update request pointers
  56                         out += bytestocopy;
  57                         bytestoread -= bytestocopy;
  58                 } else {
  59                         ssize_t bytesread = read (filedesc, buffer, buffercap);
  60                         bufferindex = 0;
  61                         bufferbytes = bytesread;
  62                         if (bytesread == 0) {
  63                                 break;
  64                         } else if (bytesread < 0) {
  65                                 exit(-1);
  66                         }
  67                 }
  68         }
  69         return totalbytesread;
  70 }
  71
  72 CSolver *Deserializer::deserialize() {
  73         ASTNodeType nodeType;
  74         while (myread(&nodeType, sizeof(ASTNodeType) ) > 0) {
  75                 switch (nodeType) {
  76                 case BOOLEANEDGE:
  77                         deserializeBooleanEdge();
  78                         break;
  79                 case BOOLEANVAR:
  80                         deserializeBooleanVar();
  81                         break;
  82                 case BOOLCONST:
  83                         deserializeBooleanConst();
  84                         break;
  85                 case ORDERCONST:
  86                         deserializeBooleanOrder();
  87                         break;
  88                 case ORDERTYPE:
  89                         deserializeOrder();
  90                         break;
  91                 case SETTYPE:
  92                         deserializeSet();
  93                         break;
  94                 case LOGICOP:
  95                         deserializeBooleanLogic();
  96                         break;
  97                 case PREDICATEOP:
  98                         deserializeBooleanPredicate();
  99                         break;
 100                 case PREDTABLETYPE:
 101                         deserializePredicateTable();
 102                         break;
 103                 case PREDOPERTYPE:
 104                         deserializePredicateOperator();
 105                         break;
 106                 case TABLETYPE:
 107                         deserializeTable();
 108                         break;
 109                 case ELEMSET:
 110                         deserializeElementSet();
 111                         break;
 112                 case ELEMCONST:
 113                         deserializeElementConst();
 114                         break;
 115                 case ELEMFUNCRETURN:
 116                         deserializeElementFunction();
 117                         break;
 118                 case FUNCOPTYPE:
 119                         deserializeFunctionOperator();
 120                         break;
 121                 case FUNCTABLETYPE:
 122                         deserializeFunctionTable();
 123                         break;
 124                 default:
 125                         ASSERT(0);
 126                 }
 127         }
 128         return solver;
 129 }
 130
 131 void Deserializer::deserializeBooleanEdge() {
 132         Boolean *b_ptr;
 133         myread(&b_ptr, sizeof(Boolean *));
 134         BooleanEdge tmp(b_ptr);
 135         bool isNegated = tmp.isNegated();
 136         ASSERT(map.contains(tmp.getBoolean()));
 137         b_ptr = (Boolean *) map.get(tmp.getBoolean());
 138         BooleanEdge res(b_ptr);
 139         bool isTopLevel;
 140         myread(&isTopLevel, sizeof(bool));
 141         if (isTopLevel) {
 142                 solver->addConstraint(isNegated ? res.negate() : res);
 143         }
 144 }
 145
 146 void Deserializer::deserializeBooleanVar() {
 147         BooleanVar *b;
 148         myread(&b, sizeof(BooleanVar *));
 149         VarType vtype;
 150         myread(&vtype, sizeof(VarType));
 151         map.put(b, solver->getBooleanVar(vtype).getBoolean());
 152 }
 153
 154 void Deserializer::deserializeBooleanConst() {
 155         BooleanVar *b;
 156         myread(&b, sizeof(BooleanVar *));
 157         bool istrue;
 158         myread(&istrue, sizeof(bool));
 159         map.put(b, istrue ? solver->getBooleanTrue().getBoolean() :
 160                                         solver->getBooleanFalse().getBoolean());
 161 }
 162
 163 void Deserializer::deserializeBooleanOrder() {
 164         BooleanOrder *bo_ptr;
 165         myread(&bo_ptr, sizeof(BooleanOrder *));
 166         Order *order;
 167         myread(&order, sizeof(Order *));
 168         ASSERT(map.contains(order));
 169         order  = (Order *) map.get(order);
 170         uint64_t first;
 171         myread(&first, sizeof(uint64_t));
 172         uint64_t second;
 173         myread(&second, sizeof(uint64_t));
 174         map.put(bo_ptr, solver->orderConstraint(order, first, second).getBoolean());
 175 }
 176
 177 void Deserializer::deserializeOrder() {
 178         Order *o_ptr;
 179         myread(&o_ptr, sizeof(Order *));
 180         OrderType type;
 181         myread(&type, sizeof(OrderType));
 182         Set *set_ptr;
 183         myread(&set_ptr, sizeof(Set *));
 184         ASSERT(map.contains(set_ptr));
 185         Set *set  = (Set *) map.get(set_ptr);
 186         map.put(o_ptr, solver->createOrder(type, set));
 187 }
 188
 189 void Deserializer::deserializeSet() {
 190         Set *s_ptr;
 191         myread(&s_ptr, sizeof(Set *));
 192         VarType type;
 193         myread(&type, sizeof(VarType));
 194         bool isRange;
 195         myread(&isRange, sizeof(bool));
 196         bool isMutable;
 197         myread(&isMutable, sizeof(bool));
 198         if (isRange) {
 199                 uint64_t low;
 200                 myread(&low, sizeof(uint64_t));
 201                 uint64_t high;
 202                 myread(&high, sizeof(uint64_t));
 203                 map.put(s_ptr, new Set(type, low, high));
 204         } else {
 205                 Set *set = NULL;
 206                 if (isMutable) {
 207                         set = new MutableSet(type);
 208                 }
 209                 uint size;
 210                 myread(&size, sizeof(uint));
 211                 Vector<uint64_t> members;
 212                 for (uint i = 0; i < size; i++) {
 213                         uint64_t mem;
 214                         myread(&mem, sizeof(uint64_t));
 215                         if (isMutable) {
 216                                 ((MutableSet *) set)->addElementMSet(mem);
 217                         } else {
 218                                 members.push(mem);
 219                         }
 220                 }
 221                 if (!isMutable) {
 222                         set = solver->createSet(type, members.expose(), size);
 223                 }
 224                 map.put(s_ptr, set);
 225         }
 226 }
 227
 228 void Deserializer::deserializeBooleanLogic() {
 229         BooleanLogic *bl_ptr;
 230         myread(&bl_ptr, sizeof(BooleanLogic *));
 231         LogicOp op;
 232         myread(&op, sizeof(LogicOp));
 233         uint size;
 234         myread(&size, sizeof(uint));
 235         Vector<BooleanEdge> members;
 236         for (uint i = 0; i < size; i++) {
 237                 Boolean *member;
 238                 myread(&member, sizeof(Boolean *));
 239                 BooleanEdge tmp(member);
 240                 bool isNegated = tmp.isNegated();
 241                 ASSERT(map.contains(tmp.getBoolean()));
 242                 member = (Boolean *) map.get(tmp.getBoolean());
 243                 BooleanEdge res(member);
 244                 members.push( isNegated ? res.negate() : res );
 245         }
 246         map.put(bl_ptr, solver->applyLogicalOperation(op, members.expose(), size).getBoolean());
 247 }
 248
 249 void Deserializer::deserializeBooleanPredicate() {
 250         BooleanPredicate *bp_ptr;
 251         myread(&bp_ptr, sizeof(BooleanPredicate *));
 252         Predicate *predicate;
 253         myread(&predicate, sizeof(Predicate *));
 254         ASSERT(map.contains(predicate));
 255         predicate = (Predicate *) map.get(predicate);
 256         uint size;
 257         myread(&size, sizeof(uint));
 258         Vector<Element *> members;
 259         for (uint i = 0; i < size; i++) {
 260                 Element *input;
 261                 myread(&input, sizeof(Element *));
 262                 ASSERT(map.contains(input));
 263                 input = (Element *) map.get(input);
 264                 members.push(input);
 265         }
 266
 267         Boolean *stat_ptr;
 268         myread(&stat_ptr, sizeof(Boolean *));
 269         BooleanEdge undefStatus;
 270         if (stat_ptr != NULL) {
 271                 BooleanEdge tmp(stat_ptr);
 272                 bool isNegated = tmp.isNegated();
 273                 ASSERT(map.contains(tmp.getBoolean()));
 274                 stat_ptr = (Boolean *) map.get(tmp.getBoolean());
 275                 BooleanEdge res(stat_ptr);
 276                 undefStatus = isNegated ? res.negate() : res;
 277         } else {
 278                 undefStatus = NULL;
 279         }
 280         map.put(bp_ptr, solver->applyPredicateTable(predicate, members.expose(), size, undefStatus).getBoolean());
 281 }
 282
 283 void Deserializer::deserializePredicateTable() {
 284         PredicateTable *pt_ptr;
 285         myread(&pt_ptr, sizeof(PredicateTable *));
 286         Table *table;
 287         myread(&table, sizeof(Table *));
 288         ASSERT(map.contains(table));
 289         table = (Table *) map.get(table);
 290         UndefinedBehavior undefinedbehavior;
 291         myread(&undefinedbehavior, sizeof(UndefinedBehavior));
 292
 293         map.put(pt_ptr, solver->createPredicateTable(table, undefinedbehavior));
 294 }
 295
 296 void Deserializer::deserializePredicateOperator() {
 297         PredicateOperator *po_ptr;
 298         myread(&po_ptr, sizeof(PredicateOperator *));
 299         CompOp op;
 300         myread(&op, sizeof(CompOp));
 301
 302         map.put(po_ptr, solver->createPredicateOperator(op));
 303 }
 304
 305 void Deserializer::deserializeTable() {
 306         Table *t_ptr;
 307         myread(&t_ptr, sizeof(Table *));
 308         Set *range;
 309         myread(&range, sizeof(Set *));
 310         if (range != NULL) {
 311                 ASSERT(map.contains(range));
 312                 range = (Set *) map.get(range);
 313         }
 314         Table *table = solver->createTable(range);
 315         uint size;
 316         myread(&size, sizeof(uint));
 317         for (uint i = 0; i < size; i++) {
 318                 uint64_t output;
 319                 myread(&output, sizeof(uint64_t));
 320                 uint inputSize;
 321                 myread(&inputSize, sizeof(uint));
 322                 Vector<uint64_t> inputs;
 323                 inputs.setSize(inputSize);
 324                 myread(inputs.expose(), sizeof(uint64_t) * inputSize);
 325                 table->addNewTableEntry(inputs.expose(), inputSize, output);
 326         }
 327
 328         map.put(t_ptr, table);
 329 }
 330
 331
 332 void Deserializer::deserializeElementSet() {
 333         bool anyValue = false;
 334         myread(&anyValue, sizeof(bool));
 335         ElementSet *es_ptr;
 336         myread(&es_ptr, sizeof(ElementSet *));
 337         Set *set;
 338         myread(&set, sizeof(Set *));
 339         ASSERT(map.contains(set));
 340         set  = (Set *) map.get(set);
 341         Element *newEl = solver->getElementVar(set);
 342         newEl->anyValue = anyValue;
 343         map.put(es_ptr, newEl);
 344 }
 345
 346 void Deserializer::deserializeElementConst() {
 347         bool anyValue = false;
 348         myread(&anyValue, sizeof(bool));
 349         ElementSet *es_ptr;
 350         myread(&es_ptr, sizeof(ElementSet *));
 351         VarType type;
 352         myread(&type, sizeof(VarType));
 353         uint64_t value;
 354         myread(&value, sizeof(uint64_t));
 355         Element *newEl = solver->getElementConst(type, value);
 356         newEl->anyValue = anyValue;
 357         map.put(es_ptr, newEl);
 358 }
 359
 360 void Deserializer::deserializeElementFunction() {
 361         bool anyValue = false;
 362         myread(&anyValue, sizeof(bool));
 363         ElementFunction *ef_ptr;
 364         myread(&ef_ptr, sizeof(ElementFunction *));
 365         Function *function;
 366         myread(&function, sizeof(Function *));
 367         ASSERT(map.contains(function));
 368         function = (Function *) map.get(function);
 369         uint size;
 370         myread(&size, sizeof(uint));
 371         Vector<Element *> members;
 372         for (uint i = 0; i < size; i++) {
 373                 Element *input;
 374                 myread(&input, sizeof(Element *));
 375                 ASSERT(map.contains(input));
 376                 input = (Element *) map.get(input);
 377                 members.push(input);
 378         }
 379
 380         Boolean *overflowstatus;
 381         myread(&overflowstatus, sizeof(Boolean *));
 382         BooleanEdge tmp(overflowstatus);
 383         bool isNegated = tmp.isNegated();
 384         ASSERT(map.contains(tmp.getBoolean()));
 385         overflowstatus = (Boolean *) map.get(tmp.getBoolean());
 386         BooleanEdge res(overflowstatus);
 387         BooleanEdge undefStatus = isNegated ? res.negate() : res;
 388         Element *newEl = solver->applyFunction(function, members.expose(), size, undefStatus);
 389         newEl->anyValue = anyValue;
 390         map.put(ef_ptr, newEl);
 391 }
 392
 393
 394 void Deserializer::deserializeFunctionOperator() {
 395         FunctionOperator *fo_ptr;
 396         myread(&fo_ptr, sizeof(FunctionOperator *));
 397         ArithOp op;
 398         myread(&op, sizeof(ArithOp));
 399         Set *range;
 400         myread(&range, sizeof(Set *));
 401         ASSERT(map.contains(range));
 402         range = (Set *) map.get(range);
 403         OverFlowBehavior overflowbehavior;
 404         myread(&overflowbehavior, sizeof(OverFlowBehavior));
 405         map.put(fo_ptr, solver->createFunctionOperator(op, range, overflowbehavior));
 406 }
 407
 408 void Deserializer::deserializeFunctionTable() {
 409         FunctionTable *ft_ptr;
 410         myread(&ft_ptr, sizeof(FunctionTable *));
 411         Table *table;
 412         myread(&table, sizeof(Table *));
 413         ASSERT(map.contains(table));
 414         table = (Table *) map.get(table);
 415         UndefinedBehavior undefinedbehavior;
 416         myread(&undefinedbehavior, sizeof(UndefinedBehavior));
 417
 418         map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));
 419 }