From fa89f816b55a578c98f31c7accdc2cd4a38a3542 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Fri, 8 Sep 2017 22:23:40 -0700 Subject: [PATCH] edits --- src/AST/asthash.cc | 4 +- src/AST/element.cc | 4 +- src/AST/element.h | 4 +- src/ASTAnalyses/Encoding/encodinggraph.cc | 87 +++++++++++++++++++---- src/ASTAnalyses/Encoding/encodinggraph.h | 28 ++++++-- src/Backend/satencoder.cc | 2 +- src/Backend/satfuncopencoder.cc | 4 +- src/Backend/satfunctableencoder.cc | 8 +-- src/Collections/structs.h | 2 +- 9 files changed, 110 insertions(+), 33 deletions(-) diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc index 827f9e1..bc58431 100644 --- a/src/AST/asthash.cc +++ b/src/AST/asthash.cc @@ -104,7 +104,7 @@ uint hashElement(Element *e) { } case ELEMFUNCRETURN: { ElementFunction *ef = (ElementFunction *) e; - return ((uint)(uintptr_t) ef->function) ^ + return ((uint)(uintptr_t) ef->getFunction()) ^ ((uint)(uintptr_t) ef->overflowstatus) ^ hashArray(&ef->inputs); } @@ -127,7 +127,7 @@ bool compareElement(Element *e1, Element *e2) { case ELEMFUNCRETURN: { ElementFunction *ef1 = (ElementFunction *) e1; ElementFunction *ef2 = (ElementFunction *) e2; - return (ef1->function == ef2->function) && + return (ef1->getFunction() == ef2->getFunction()) && (ef1->overflowstatus == ef2->overflowstatus) && compareArray(&ef1->inputs, &ef2->inputs); } diff --git a/src/AST/element.cc b/src/AST/element.cc index 05f6cef..ca42290 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -23,10 +23,10 @@ ElementSet::ElementSet(ASTNodeType _type, Set *s) : ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, BooleanEdge _overflowstatus) : Element(ELEMFUNCRETURN), - function(_function), inputs(array, numArrays), overflowstatus(_overflowstatus), - functionencoding(this) { + functionencoding(this), + function(_function) { } ElementConst::ElementConst(uint64_t _value, Set *_set) : diff --git a/src/AST/element.h b/src/AST/element.h index 076e831..db1cbfb 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -43,14 +43,16 @@ public: class ElementFunction : public Element { public: ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus); - Function *function; Array inputs; BooleanEdge overflowstatus; FunctionEncoding functionencoding; Element *clone(CSolver *solver, CloneMap *map); Set * getRange(); void updateParents(); + Function * getFunction() {return function;} CMEMALLOC; + private: + Function *function; }; static inline ElementEncoding *getElementEncoding(Element *e) { diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc index e337e56..9c0a29e 100644 --- a/src/ASTAnalyses/Encoding/encodinggraph.cc +++ b/src/ASTAnalyses/Encoding/encodinggraph.cc @@ -1,6 +1,7 @@ #include "encodinggraph.h" #include "iterator.h" #include "element.h" +#include "function.h" EncodingGraph::EncodingGraph(CSolver * _solver) : solver(_solver) { @@ -8,30 +9,86 @@ EncodingGraph::EncodingGraph(CSolver * _solver) : } -EncodingNode * EncodingGraph::getNode(Element * element) { - return NULL; -} - void EncodingGraph::buildGraph() { ElementIterator it(solver); while(it.hasNext()) { Element * e = it.next(); - processElement(e); + switch(e->type) { + case ELEMSET: + case ELEMFUNCRETURN: + processElement(e); + break; + case ELEMCONST: + break; + default: + ASSERT(0); + } } } void EncodingGraph::processElement(Element *e) { - switch(e->type) { - case ELEMSET: { - break; - } - case ELEMFUNCRETURN: { - break; + uint size=e->parents.getSize(); + for(uint i=0;iparents.get(i); + switch(n->type) { + case PREDICATEOP: + processPredicate((BooleanPredicate *)n); + break; + case ELEMFUNCRETURN: + processFunction((ElementFunction *)n); + break; + default: + ASSERT(0); + } } - case ELEMCONST: { - break; +} + +void EncodingGraph::processFunction(ElementFunction *ef) { + Function *f=ef->getFunction(); + if (f->type==OPERATORFUNC) { + FunctionOperator *fo=(FunctionOperator*)f; + ArithOp op=fo->op; } - default: - ASSERT(0); +} + +void EncodingGraph::processPredicate(BooleanPredicate *b) { + +} + +EncodingNode * EncodingGraph::createNode(Element *e) { + Set *s = e->getRange(); + EncodingNode *n = encodingMap.get(s); + if (n == NULL) { + n = new EncodingNode(s); + encodingMap.put(s, n); } + n->addElement(e); + return n; +} + +void EncodingNode::addElement(Element *e) { + elements.add(e); +} + +EncodingEdge::EncodingEdge(EncodingNode *_l, EncodingNode *_r) : + left(_l), + right(_r), + dst(NULL) +{ +} + +EncodingEdge::EncodingEdge(EncodingNode *_left, EncodingNode *_right, EncodingNode *_dst) : + left(_left), + right(_right), + dst(_dst) +{ +} + +uint hashEncodingEdge(EncodingEdge *edge) { + uintptr_t hash=(((uintptr_t) edge->left) >> 2) ^ (((uintptr_t)edge->right) >> 4) ^ (((uintptr_t)edge->dst) >> 6); + return (uint) hash; +} + +bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2) { + return e1->left == e2->left && e1->right == e2->right && e1->dst == e2->dst; } diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h index 452a034..adb467c 100644 --- a/src/ASTAnalyses/Encoding/encodinggraph.h +++ b/src/ASTAnalyses/Encoding/encodinggraph.h @@ -3,33 +3,51 @@ #include "classlist.h" #include "structs.h" +uint hashEncodingEdge(EncodingEdge *edge); +bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2); + +typedef Hashtable HashtableEdge; + class EncodingGraph { public: EncodingGraph(CSolver * solver); - EncodingNode * getNode(Element * element); void buildGraph(); CMEMALLOC; private: CSolver * solver; - HashTableEncoding encodingMap; + HashtableEncoding encodingMap; + HashtableEdge edgeMap; void processElement(Element *e); + void processFunction(ElementFunction *f); + void processPredicate(BooleanPredicate *b); + EncodingNode * createNode(Element *e); }; class EncodingNode { public: - + EncodingNode(Set *_s); + void addElement(Element *e); CMEMALLOC; private: - + Set *s; + HashsetElement elements; }; class EncodingEdge { public: - + EncodingEdge(EncodingNode *_l, EncodingNode *_r); + EncodingEdge(EncodingNode *_l, EncodingNode *_r, EncodingNode *_d); CMEMALLOC; private: + EncodingNode *left; + EncodingNode *right; + EncodingNode *dst; + friend uint hashEncodingEdge(EncodingEdge *edge); + friend bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2); + }; + #endif diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 4020ad6..1fe98ce 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -151,7 +151,7 @@ void SATEncoder::encodeElementSATEncoder(Element *element) { } void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) { - switch (function->function->type) { + switch (function->getFunction()->type) { case TABLEFUNC: encodeTableElementFunctionSATEncoder(function); break; diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index bfd4ea6..7e6a67d 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -88,7 +88,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) #ifdef TRACE_DEBUG model_print("Operator Function ...\n"); #endif - FunctionOperator *function = (FunctionOperator *) func->function; + FunctionOperator *function = (FunctionOperator *) func->getFunction(); uint numDomains = func->inputs.getSize(); /* Call base encoders for children */ @@ -115,7 +115,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) Edge carray[numDomains + 1]; uint64_t result = function->applyFunctionOperator(numDomains, vals); - bool isInRange = ((FunctionOperator *)func->function)->isInRangeFunction(result); + bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result); bool needClause = isInRange; if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) { needClause = true; diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index c8d53d1..961d810 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -177,10 +177,10 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint } void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) { - UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior; + UndefinedBehavior undefStatus = ((FunctionTable *) func->getFunction())->undefBehavior; ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED); Array *elements = &func->inputs; - Table *table = ((FunctionTable *) (func->function))->table; + Table *table = ((FunctionTable *) (func->getFunction()))->table; uint size = table->getSize(); Edge constraints[size]; SetIteratorTableEntry *iterator = table->getEntries(); @@ -220,7 +220,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc #ifdef TRACE_DEBUG model_print("Enumeration Table functions ...\n"); #endif - ASSERT(elemFunc->function->type == TABLEFUNC); + ASSERT(elemFunc->getFunction()->type == TABLEFUNC); //First encode children Array *elements = &elemFunc->inputs; for (uint i = 0; i < elements->getSize(); i++) { @@ -228,7 +228,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc encodeElementSATEncoder(elem); } - FunctionTable *function = (FunctionTable *)elemFunc->function; + FunctionTable *function = (FunctionTable *)elemFunc->getFunction(); switch (function->undefBehavior) { case SATC_IGNOREBEHAVIOR: case SATC_FLAGFORCEUNDEFINED: diff --git a/src/Collections/structs.h b/src/Collections/structs.h index e6f451e..6ee69ab 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -32,7 +32,7 @@ typedef Hashtable CloneMap; -typedef Hashtable HashTableEncoding; +typedef Hashtable HashtableEncoding; typedef SetIterator SetIteratorTableEntry; typedef SetIterator SetIteratorOrderEdge; -- 2.34.1