3 * File: deserializer.cc
6 * Created on September 7, 2017, 6:08 PM
9 #include "deserializer.h"
13 #include "predicate.h"
16 #include "mutableset.h"
18 #define READBUFFERSIZE 16384
20 Deserializer::Deserializer(const char *file, InterpreterType itype) :
21 buffer((char *) ourmalloc(READBUFFERSIZE)),
24 buffercap(READBUFFERSIZE),
27 filedesc = open(file, O_RDONLY);
32 if (itype != SATUNE) {
33 solver->setInterpreter(itype);
37 Deserializer::~Deserializer() {
38 if (-1 == close(filedesc)) {
44 ssize_t Deserializer::myread(void *__buf, size_t bytestoread) {
45 char *out = (char * ) __buf;
46 size_t totalbytesread = 0;
48 if (bufferbytes != 0) {
49 uint bytestocopy = (bufferbytes > bytestoread) ? bytestoread : bufferbytes;
50 memcpy(out, &buffer[bufferindex], bytestocopy);
52 bufferbytes -= bytestocopy;
53 bufferindex += bytestocopy;
54 totalbytesread += bytestocopy;
55 //update request pointers
57 bytestoread -= bytestocopy;
59 ssize_t bytesread = read (filedesc, buffer, buffercap);
61 bufferbytes = bytesread;
64 } else if (bytesread < 0) {
69 return totalbytesread;
72 CSolver *Deserializer::deserialize() {
74 while (myread(&nodeType, sizeof(ASTNodeType) ) > 0) {
77 deserializeBooleanEdge();
80 deserializeBooleanVar();
83 deserializeBooleanConst();
86 deserializeBooleanOrder();
95 deserializeBooleanLogic();
98 deserializeBooleanPredicate();
101 deserializePredicateTable();
104 deserializePredicateOperator();
110 deserializeElementSet();
113 deserializeElementConst();
116 deserializeElementFunction();
119 deserializeFunctionOperator();
122 deserializeFunctionTable();
131 void Deserializer::deserializeBooleanEdge() {
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);
140 myread(&isTopLevel, sizeof(bool));
142 solver->addConstraint(isNegated ? res.negate() : res);
146 void Deserializer::deserializeBooleanVar() {
148 myread(&b, sizeof(BooleanVar *));
150 myread(&vtype, sizeof(VarType));
151 map.put(b, solver->getBooleanVar(vtype).getBoolean());
154 void Deserializer::deserializeBooleanConst() {
156 myread(&b, sizeof(BooleanVar *));
158 myread(&istrue, sizeof(bool));
159 map.put(b, istrue ? solver->getBooleanTrue().getBoolean() :
160 solver->getBooleanFalse().getBoolean());
163 void Deserializer::deserializeBooleanOrder() {
164 BooleanOrder *bo_ptr;
165 myread(&bo_ptr, sizeof(BooleanOrder *));
167 myread(&order, sizeof(Order *));
168 ASSERT(map.contains(order));
169 order = (Order *) map.get(order);
171 myread(&first, sizeof(uint64_t));
173 myread(&second, sizeof(uint64_t));
174 map.put(bo_ptr, solver->orderConstraint(order, first, second).getBoolean());
177 void Deserializer::deserializeOrder() {
179 myread(&o_ptr, sizeof(Order *));
181 myread(&type, sizeof(OrderType));
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));
189 void Deserializer::deserializeSet() {
191 myread(&s_ptr, sizeof(Set *));
193 myread(&type, sizeof(VarType));
195 myread(&isRange, sizeof(bool));
197 myread(&isMutable, sizeof(bool));
200 myread(&low, sizeof(uint64_t));
202 myread(&high, sizeof(uint64_t));
203 map.put(s_ptr, new Set(type, low, high));
207 set = new MutableSet(type);
210 myread(&size, sizeof(uint));
211 Vector<uint64_t> members;
212 for (uint i = 0; i < size; i++) {
214 myread(&mem, sizeof(uint64_t));
216 ((MutableSet *) set)->addElementMSet(mem);
222 set = solver->createSet(type, members.expose(), size);
228 void Deserializer::deserializeBooleanLogic() {
229 BooleanLogic *bl_ptr;
230 myread(&bl_ptr, sizeof(BooleanLogic *));
232 myread(&op, sizeof(LogicOp));
234 myread(&size, sizeof(uint));
235 Vector<BooleanEdge> members;
236 for (uint i = 0; i < size; i++) {
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 );
246 map.put(bl_ptr, solver->applyLogicalOperation(op, members.expose(), size).getBoolean());
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);
257 myread(&size, sizeof(uint));
258 Vector<Element *> members;
259 for (uint i = 0; i < size; i++) {
261 myread(&input, sizeof(Element *));
262 ASSERT(map.contains(input));
263 input = (Element *) map.get(input);
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;
280 map.put(bp_ptr, solver->applyPredicateTable(predicate, members.expose(), size, undefStatus).getBoolean());
283 void Deserializer::deserializePredicateTable() {
284 PredicateTable *pt_ptr;
285 myread(&pt_ptr, sizeof(PredicateTable *));
287 myread(&table, sizeof(Table *));
288 ASSERT(map.contains(table));
289 table = (Table *) map.get(table);
290 UndefinedBehavior undefinedbehavior;
291 myread(&undefinedbehavior, sizeof(UndefinedBehavior));
293 map.put(pt_ptr, solver->createPredicateTable(table, undefinedbehavior));
296 void Deserializer::deserializePredicateOperator() {
297 PredicateOperator *po_ptr;
298 myread(&po_ptr, sizeof(PredicateOperator *));
300 myread(&op, sizeof(CompOp));
302 map.put(po_ptr, solver->createPredicateOperator(op));
305 void Deserializer::deserializeTable() {
307 myread(&t_ptr, sizeof(Table *));
309 myread(&range, sizeof(Set *));
311 ASSERT(map.contains(range));
312 range = (Set *) map.get(range);
314 Table *table = solver->createTable(range);
316 myread(&size, sizeof(uint));
317 for (uint i = 0; i < size; i++) {
319 myread(&output, sizeof(uint64_t));
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);
328 map.put(t_ptr, table);
332 void Deserializer::deserializeElementSet() {
333 bool anyValue = false;
334 myread(&anyValue, sizeof(bool));
336 myread(&es_ptr, sizeof(ElementSet *));
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);
346 void Deserializer::deserializeElementConst() {
347 bool anyValue = false;
348 myread(&anyValue, sizeof(bool));
350 myread(&es_ptr, sizeof(ElementSet *));
352 myread(&type, sizeof(VarType));
354 myread(&value, sizeof(uint64_t));
355 Element *newEl = solver->getElementConst(type, value);
356 newEl->anyValue = anyValue;
357 map.put(es_ptr, newEl);
360 void Deserializer::deserializeElementFunction() {
361 bool anyValue = false;
362 myread(&anyValue, sizeof(bool));
363 ElementFunction *ef_ptr;
364 myread(&ef_ptr, sizeof(ElementFunction *));
366 myread(&function, sizeof(Function *));
367 ASSERT(map.contains(function));
368 function = (Function *) map.get(function);
370 myread(&size, sizeof(uint));
371 Vector<Element *> members;
372 for (uint i = 0; i < size; i++) {
374 myread(&input, sizeof(Element *));
375 ASSERT(map.contains(input));
376 input = (Element *) map.get(input);
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);
394 void Deserializer::deserializeFunctionOperator() {
395 FunctionOperator *fo_ptr;
396 myread(&fo_ptr, sizeof(FunctionOperator *));
398 myread(&op, sizeof(ArithOp));
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));
408 void Deserializer::deserializeFunctionTable() {
409 FunctionTable *ft_ptr;
410 myread(&ft_ptr, sizeof(FunctionTable *));
412 myread(&table, sizeof(Table *));
413 ASSERT(map.contains(table));
414 table = (Table *) map.get(table);
415 UndefinedBehavior undefinedbehavior;
416 myread(&undefinedbehavior, sizeof(UndefinedBehavior));
418 map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));