From 3581e59e0ecbdf07cd460104bcc907b0d146562f Mon Sep 17 00:00:00 2001 From: Hamed Date: Mon, 28 Aug 2017 22:16:01 -0700 Subject: [PATCH] OOP representation of Transforms --- src/ASTTransform/analyzer.cc | 73 +++++++++++ src/ASTTransform/analyzer.h | 16 +++ src/ASTTransform/decomposeordertransform.cc | 90 +++++++++++++ src/ASTTransform/decomposeordertransform.h | 29 +++++ src/ASTTransform/integerencoding.cc | 49 +++++++ src/ASTTransform/integerencoding.h | 30 +++++ src/ASTTransform/orderdecompose.cc | 135 -------------------- src/ASTTransform/orderdecompose.h | 23 ---- src/ASTTransform/pass.cc | 14 ++ src/ASTTransform/pass.h | 31 +++++ src/ASTTransform/transform.cc | 36 +----- src/ASTTransform/transform.h | 16 ++- src/classlist.h | 2 + src/csolver.cc | 2 +- 14 files changed, 348 insertions(+), 198 deletions(-) create mode 100644 src/ASTTransform/analyzer.cc create mode 100644 src/ASTTransform/analyzer.h create mode 100644 src/ASTTransform/decomposeordertransform.cc create mode 100644 src/ASTTransform/decomposeordertransform.h create mode 100644 src/ASTTransform/integerencoding.cc create mode 100644 src/ASTTransform/integerencoding.h delete mode 100644 src/ASTTransform/orderdecompose.cc delete mode 100644 src/ASTTransform/orderdecompose.h create mode 100644 src/ASTTransform/pass.cc create mode 100644 src/ASTTransform/pass.h diff --git a/src/ASTTransform/analyzer.cc b/src/ASTTransform/analyzer.cc new file mode 100644 index 0000000..fb8fc33 --- /dev/null +++ b/src/ASTTransform/analyzer.cc @@ -0,0 +1,73 @@ +#include "analyzer.h" +#include "common.h" +#include "order.h" +#include "boolean.h" +#include "ordergraph.h" +#include "ordernode.h" +#include "rewriter.h" +#include "orderedge.h" +#include "mutableset.h" +#include "ops.h" +#include "csolver.h" +#include "orderencoder.h" +#include "tunable.h" +#include "transform.h" +#include "element.h" +#include "integerencoding.h" +#include "decomposeordertransform.h" + +void orderAnalysis(CSolver *This) { + Vector *orders = This->getOrders(); + uint size = orders->getSize(); + for (uint i = 0; i < size; i++) { + Order *order = orders->get(i); + DecomposeOrderTransform* decompose = new DecomposeOrderTransform(This, order, DECOMPOSEORDER, &onoff); + if (!decompose->canExecuteTransform()) + continue; + + OrderGraph *graph = buildOrderGraph(order); + if (order->type == PARTIAL) { + //Required to do SCC analysis for partial order graphs. It + //makes sure we don't incorrectly optimize graphs with negative + //polarity edges + completePartialOrderGraph(graph); + } + + + bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff); + + if (mustReachGlobal) + reachMustAnalysis(This, graph, false); + + bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff); + + if (mustReachLocal) { + //This pair of analysis is also optional + if (order->type == PARTIAL) { + localMustAnalysisPartial(This, graph); + } else { + localMustAnalysisTotal(This, graph); + } + } + + bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff); + + if (mustReachPrune) + removeMustBeTrueNodes(This, graph); + + //This is needed for splitorder + computeStronglyConnectedComponentGraph(graph); + decompose->doTransform(); + delete decompose; + delete graph; + + + IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order, ORDERINTEGERENCODING, &offon); + if(!integerEncoding->canExecuteTransform()) + continue; + integerEncoding->doTransform(); + delete integerEncoding; + } +} + + diff --git a/src/ASTTransform/analyzer.h b/src/ASTTransform/analyzer.h new file mode 100644 index 0000000..453e7dc --- /dev/null +++ b/src/ASTTransform/analyzer.h @@ -0,0 +1,16 @@ +/* + * File: analyzer.h + * Author: hamed + * + * Created on August 24, 2017, 5:33 PM + */ + +#ifndef ORDERDECOMPOSE_H +#define ORDERDECOMPOSE_H +#include "classlist.h" +#include "structs.h" + +void orderAnalysis(CSolver *This); + +#endif/* ORDERDECOMPOSE_H */ + diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc new file mode 100644 index 0000000..6df2639 --- /dev/null +++ b/src/ASTTransform/decomposeordertransform.cc @@ -0,0 +1,90 @@ +/* + * File: ordertransform.cc + * Author: hamed + * + * Created on August 28, 2017, 10:35 AM + */ + +#include "decomposeordertransform.h" +#include "order.h" +#include "orderedge.h" +#include "ordernode.h" +#include "boolean.h" +#include "mutableset.h" +#include "ordergraph.h" +#include "csolver.h" + + +DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver, Order* _order, Tunables _tunable, TunableDesc* _desc) + :Transform(_solver, _tunable, _desc), + order(_order) +{ +} + +DecomposeOrderTransform::~DecomposeOrderTransform() { +} + +bool DecomposeOrderTransform::canExecuteTransform(){ + return canExecutePass(solver, order->type); +} + +void DecomposeOrderTransform::doTransform(){ + Vector ordervec; + Vector partialcandidatevec; + uint size = order->constraints.getSize(); + for (uint i = 0; i < size; i++) { + BooleanOrder *orderconstraint = order->constraints.get(i); + OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first); + OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second); + model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum); + if (from->sccNum != to->sccNum) { + OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to); + if (edge->polPos) { + solver->replaceBooleanWithTrue(orderconstraint); + } else if (edge->polNeg) { + solver->replaceBooleanWithFalse(orderconstraint); + } else { + //This case should only be possible if constraint isn't in AST + ASSERT(0); + } + } else { + //Build new order and change constraint's order + Order *neworder = NULL; + if (ordervec.getSize() > from->sccNum) + neworder = ordervec.get(from->sccNum); + if (neworder == NULL) { + MutableSet *set = solver->createMutableSet(order->set->type); + neworder = solver->createOrder(order->type, set); + ordervec.setExpand(from->sccNum, neworder); + if (order->type == PARTIAL) + partialcandidatevec.setExpand(from->sccNum, neworder); + else + partialcandidatevec.setExpand(from->sccNum, NULL); + } + if (from->status != ADDEDTOSET) { + from->status = ADDEDTOSET; + ((MutableSet *)neworder->set)->addElementMSet(from->id); + } + if (to->status != ADDEDTOSET) { + to->status = ADDEDTOSET; + ((MutableSet *)neworder->set)->addElementMSet(to->id); + } + if (order->type == PARTIAL) { + OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to); + if (edge->polNeg) + partialcandidatevec.setExpand(from->sccNum, NULL); + } + orderconstraint->order = neworder; + neworder->addOrderConstraint(orderconstraint); + } + } + + uint pcvsize = partialcandidatevec.getSize(); + for (uint i = 0; i < pcvsize; i++) { + Order *neworder = partialcandidatevec.get(i); + if (neworder != NULL) { + neworder->type = TOTAL; + model_print("i=%u\t", i); + } + } +} diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h new file mode 100644 index 0000000..25aea89 --- /dev/null +++ b/src/ASTTransform/decomposeordertransform.h @@ -0,0 +1,29 @@ +/* + * File: ordertransform.h + * Author: hamed + * + * Created on August 28, 2017, 10:35 AM + */ + +#ifndef ORDERTRANSFORM_H +#define ORDERTRANSFORM_H +#include "classlist.h" +#include "transform.h" + + +class DecomposeOrderTransform : public Transform { +public: + DecomposeOrderTransform(CSolver* _solver, Order* order, Tunables _tunable, TunableDesc* _desc); + virtual ~DecomposeOrderTransform(); + void doTransform(); + void setOrderGraph(OrderGraph* _graph){ + graph = _graph; + } + bool canExecuteTransform(); +private: + Order* order; + OrderGraph* graph; +}; + +#endif /* ORDERTRANSFORM_H */ + diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc new file mode 100644 index 0000000..b4b0f99 --- /dev/null +++ b/src/ASTTransform/integerencoding.cc @@ -0,0 +1,49 @@ + +#include "integerencoding.h" +#include "set.h" +#include "order.h" +#include "satencoder.h" +#include "csolver.h" +#include "integerencodingrecord.h" + +HashTableOrderIntegerEncoding* IntegerEncodingTransform::orderIntegerEncoding = new HashTableOrderIntegerEncoding(); + +IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver, Order* _order, Tunables _tunable, TunableDesc* _desc) + :Transform(_solver, _tunable, _desc), + order(_order) + +{ +} + +IntegerEncodingTransform::~IntegerEncodingTransform(){ +} + +bool IntegerEncodingTransform::canExecuteTransform(){ + return canExecutePass(solver, order->type); +} + +void IntegerEncodingTransform::doTransform(){ + if (!orderIntegerEncoding->contains(order)) { + orderIntegerEncoding->put(order, new IntegerEncodingRecord( + solver->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1))); + } + uint size = order->constraints.getSize(); + for(uint i=0; iconstraints.get(i)); + } +} + + +void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) { + IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order); + //getting two elements and using LT predicate ... + Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first); + Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second); + Set *sarray[] = {ierec->set, ierec->set}; + Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2); + Element *parray[] = {elem1, elem2}; + Boolean *boolean = solver->applyPredicate(predicate, parray, 2); + solver->addConstraint(boolean); + solver->replaceBooleanWithBoolean(boolOrder, boolean); +} + diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h new file mode 100644 index 0000000..61e1512 --- /dev/null +++ b/src/ASTTransform/integerencoding.h @@ -0,0 +1,30 @@ +/* + * File: integerencoding.h + * Author: hamed + * + * Created on August 27, 2017, 4:36 PM + */ + +#ifndef INTEGERENCODING_H +#define INTEGERENCODING_H +#include "classlist.h" +#include "transform.h" +#include "order.h" + +class IntegerEncodingTransform : public Transform{ +public: + IntegerEncodingTransform(CSolver* solver, Order* order, Tunables _tunable, TunableDesc* _desc); + void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder); + void doTransform(); + bool canExecuteTransform(); + ~IntegerEncodingTransform(); +private: + Order* order; + // In future we can use a singleton class instead of static variable for keeping data that needed + // for translating back result + static HashTableOrderIntegerEncoding* orderIntegerEncoding; +}; + + +#endif /* INTEGERENCODING_H */ + diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc deleted file mode 100644 index ccac62b..0000000 --- a/src/ASTTransform/orderdecompose.cc +++ /dev/null @@ -1,135 +0,0 @@ -#include "orderdecompose.h" -#include "common.h" -#include "order.h" -#include "boolean.h" -#include "ordergraph.h" -#include "ordernode.h" -#include "rewriter.h" -#include "orderedge.h" -#include "mutableset.h" -#include "ops.h" -#include "csolver.h" -#include "orderencoder.h" -#include "tunable.h" -#include "transform.h" -#include "element.h" - -void orderAnalysis(CSolver *This) { - Transform* transform = new Transform(); - Vector *orders = This->getOrders(); - uint size = orders->getSize(); - for (uint i = 0; i < size; i++) { - Order *order = orders->get(i); - bool doDecompose = GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff); - if (!doDecompose) - continue; - - OrderGraph *graph = buildOrderGraph(order); - if (order->type == PARTIAL) { - //Required to do SCC analysis for partial order graphs. It - //makes sure we don't incorrectly optimize graphs with negative - //polarity edges - completePartialOrderGraph(graph); - } - - - bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff); - - if (mustReachGlobal) - reachMustAnalysis(This, graph, false); - - bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff); - - if (mustReachLocal) { - //This pair of analysis is also optional - if (order->type == PARTIAL) { - localMustAnalysisPartial(This, graph); - } else { - localMustAnalysisTotal(This, graph); - } - } - - bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff); - - if (mustReachPrune) - removeMustBeTrueNodes(This, graph); - - //This is needed for splitorder - computeStronglyConnectedComponentGraph(graph); - decomposeOrder(This, order, graph); - delete graph; - - - bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon ); - if(!doIntegerEncoding) - continue; - uint size = order->constraints.getSize(); - for(uint i=0; iorderIntegerEncodingSATEncoder(This, order->constraints.get(i)); - } - - } - delete transform; -} - -void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { - Vector ordervec; - Vector partialcandidatevec; - uint size = order->constraints.getSize(); - for (uint i = 0; i < size; i++) { - BooleanOrder *orderconstraint = order->constraints.get(i); - OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first); - OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second); - model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum); - if (from->sccNum != to->sccNum) { - OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to); - if (edge->polPos) { - This->replaceBooleanWithTrue(orderconstraint); - } else if (edge->polNeg) { - This->replaceBooleanWithFalse(orderconstraint); - } else { - //This case should only be possible if constraint isn't in AST - ASSERT(0); - } - } else { - //Build new order and change constraint's order - Order *neworder = NULL; - if (ordervec.getSize() > from->sccNum) - neworder = ordervec.get(from->sccNum); - if (neworder == NULL) { - MutableSet *set = This->createMutableSet(order->set->type); - neworder = This->createOrder(order->type, set); - ordervec.setExpand(from->sccNum, neworder); - if (order->type == PARTIAL) - partialcandidatevec.setExpand(from->sccNum, neworder); - else - partialcandidatevec.setExpand(from->sccNum, NULL); - } - if (from->status != ADDEDTOSET) { - from->status = ADDEDTOSET; - ((MutableSet *)neworder->set)->addElementMSet(from->id); - } - if (to->status != ADDEDTOSET) { - to->status = ADDEDTOSET; - ((MutableSet *)neworder->set)->addElementMSet(to->id); - } - if (order->type == PARTIAL) { - OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to); - if (edge->polNeg) - partialcandidatevec.setExpand(from->sccNum, NULL); - } - orderconstraint->order = neworder; - neworder->addOrderConstraint(orderconstraint); - } - } - - uint pcvsize = partialcandidatevec.getSize(); - for (uint i = 0; i < pcvsize; i++) { - Order *neworder = partialcandidatevec.get(i); - if (neworder != NULL) { - neworder->type = TOTAL; - model_print("i=%u\t", i); - } - } -} - diff --git a/src/ASTTransform/orderdecompose.h b/src/ASTTransform/orderdecompose.h deleted file mode 100644 index 85a5481..0000000 --- a/src/ASTTransform/orderdecompose.h +++ /dev/null @@ -1,23 +0,0 @@ -/* - * To change this license header, choose License Headers in Project Properties. - * To change this template file, choose Tools | Templates - * and open the template in the editor. - */ - -/* - * File: orderdecompose.h - * Author: hamed - * - * Created on August 24, 2017, 5:33 PM - */ - -#ifndef ORDERDECOMPOSE_H -#define ORDERDECOMPOSE_H -#include "classlist.h" -#include "structs.h" - -void orderAnalysis(CSolver *This); -void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph); - -#endif/* ORDERDECOMPOSE_H */ - diff --git a/src/ASTTransform/pass.cc b/src/ASTTransform/pass.cc new file mode 100644 index 0000000..b774ceb --- /dev/null +++ b/src/ASTTransform/pass.cc @@ -0,0 +1,14 @@ +#include "pass.h" +#include "tunable.h" +#include "csolver.h" + +Pass::Pass(Tunables _tunable, TunableDesc* _desc): + tunable(_tunable), + tunableDesc(_desc) +{ + +} + +Pass::~Pass(){ + +} diff --git a/src/ASTTransform/pass.h b/src/ASTTransform/pass.h new file mode 100644 index 0000000..2d5c84e --- /dev/null +++ b/src/ASTTransform/pass.h @@ -0,0 +1,31 @@ +/* + * File: pass.h + * Author: hamed + * + * Created on August 28, 2017, 6:23 PM + */ + +#ifndef PASS_H +#define PASS_H +#include "classlist.h" +#include "mymemory.h" +#include "structs.h" +#include "tunable.h" +#include "csolver.h" + +class Pass{ +public: + Pass(Tunables _tunable, TunableDesc* _desc); + virtual ~Pass(); + virtual inline bool canExecutePass(CSolver* This, uint type=0){ + return GETVARTUNABLE(This->getTuner(), type, tunable, tunableDesc); + } + MEMALLOC; +protected: + Tunables tunable; + TunableDesc* tunableDesc; +}; + + +#endif /* PASS_H */ + diff --git a/src/ASTTransform/transform.cc b/src/ASTTransform/transform.cc index 312b450..d28980e 100644 --- a/src/ASTTransform/transform.cc +++ b/src/ASTTransform/transform.cc @@ -1,9 +1,3 @@ -/* - * To change this license header, choose License Headers in Project Properties. - * To change this template file, choose Tools | Templates - * and open the template in the editor. - */ - /* * File: transform.cc * Author: hamed @@ -12,34 +6,12 @@ */ #include "transform.h" -#include "set.h" -#include "order.h" -#include "satencoder.h" -#include "csolver.h" -#include "integerencodingrecord.h" - -Transform::Transform() { - orderIntegerEncoding = new HashTableOrderIntegerEncoding; -} -void Transform:: orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder) { - Order *order = boolOrder->order; - if (!orderIntegerEncoding->contains(order)) { - orderIntegerEncoding->put(order, new IntegerEncodingRecord( - This->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1))); - } - IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order); - //getting two elements and using LT predicate ... - Element *elem1 = ierec->getOrderIntegerElement(This, boolOrder->first); - Element *elem2 = ierec->getOrderIntegerElement(This, boolOrder->second); - Set *sarray[] = {ierec->set, ierec->set}; - Predicate *predicate = This->createPredicateOperator(LT, sarray, 2); - Element *parray[] = {elem1, elem2}; - Boolean *boolean = This->applyPredicate(predicate, parray, 2); - This->addConstraint(boolean); - This->replaceBooleanWithBoolean(boolOrder, boolean); +Transform::Transform(CSolver* _solver, Tunables _tunable, TunableDesc* _desc): + Pass(_tunable, _desc) +{ + solver = _solver; } Transform::~Transform(){ - delete orderIntegerEncoding; } diff --git a/src/ASTTransform/transform.h b/src/ASTTransform/transform.h index 44b431a..65d8119 100644 --- a/src/ASTTransform/transform.h +++ b/src/ASTTransform/transform.h @@ -11,15 +11,17 @@ #include "classlist.h" #include "mymemory.h" #include "structs.h" +#include "pass.h" -class Transform { +class Transform : public Pass{ public: - Transform(); - ~Transform(); - void orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder); - MEMALLOC; -private: - HashTableOrderIntegerEncoding* orderIntegerEncoding; + Transform(CSolver* _solver,Tunables _tunable, TunableDesc* _desc); + virtual ~Transform(); + virtual bool canExecuteTransform() = 0; + virtual void doTransform() = 0; +protected: + // Need solver for translating back the result ... + CSolver* solver; }; #endif /* TRANSFORM_H */ diff --git a/src/classlist.h b/src/classlist.h index 4b19649..e032cd5 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -54,6 +54,8 @@ class OrderGraph; class OrderNode; class OrderEdge; +class Pass; +class Transform; struct IncrementalSolver; typedef struct IncrementalSolver IncrementalSolver; diff --git a/src/csolver.cc b/src/csolver.cc index d825df5..814a140 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -11,7 +11,7 @@ #include "sattranslator.h" #include "tunable.h" #include "polarityassignment.h" -#include "orderdecompose.h" +#include "analyzer.h" CSolver::CSolver() : unsat(false) { tuner = new Tuner(); -- 2.34.1