From a10a09cec65239af24aa72aa2e05f08359d17a61 Mon Sep 17 00:00:00 2001 From: Hamed Date: Fri, 1 Sep 2017 12:39:40 -0700 Subject: [PATCH] Adding DecomposeOrderResolver --- src/AST/order.cc | 4 +- src/AST/order.h | 3 +- src/ASTAnalyses/ordergraph.cc | 14 +++++-- src/ASTAnalyses/ordergraph.h | 4 +- src/ASTTransform/decomposeordertransform.cc | 3 +- src/Encoders/orderencoding.h | 3 +- src/Makefile | 9 +++-- src/Translator/decomposeorderresolver.cc | 32 ++++++++++++++++ src/Translator/decomposeorderresolver.h | 28 ++++++++++++++ src/Translator/orderresolver.cc | 39 ++++++++++++++++++++ src/Translator/orderresolver.h | 27 ++++++++++++++ src/{Backend => Translator}/sattranslator.cc | 0 src/{Backend => Translator}/sattranslator.h | 0 src/classlist.h | 4 ++ src/mymemory.h | 8 ++-- 15 files changed, 160 insertions(+), 18 deletions(-) create mode 100644 src/Translator/decomposeorderresolver.cc create mode 100644 src/Translator/decomposeorderresolver.h create mode 100644 src/Translator/orderresolver.cc create mode 100644 src/Translator/orderresolver.h rename src/{Backend => Translator}/sattranslator.cc (100%) rename src/{Backend => Translator}/sattranslator.h (100%) diff --git a/src/AST/order.cc b/src/AST/order.cc index d359ee6..908d691 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -10,7 +10,7 @@ Order::Order(OrderType _type, Set *_set) : set(_set), orderPairTable(NULL), graph(NULL), - order(this) + encoding(this) { } @@ -24,7 +24,7 @@ void Order::addOrderConstraint(BooleanOrder *constraint) { } void Order::setOrderEncodingType(OrderEncodingType type) { - order.type = type; + encoding.type = type; } Order *Order::clone(CSolver *solver, CloneMap *map) { diff --git a/src/AST/order.h b/src/AST/order.h index ed82695..65291aa 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -18,7 +18,8 @@ public: OrderGraph *graph; Order *clone(CSolver *solver, CloneMap *map); Vector constraints; - OrderEncoding order; + OrderEncoding encoding; + void setOrderResolver(OrderResolver* _resolver) { encoding.resolver = _resolver;}; void initializeOrderHashtable(); void initializeOrderElementsHashtable(); void addOrderConstraint(BooleanOrder *constraint); diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index fcc9eda..62d4846 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -105,14 +105,17 @@ void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrd } } -OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) { +OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id, bool create) { OrderNode *node = new OrderNode(id); OrderNode *tmp = nodes->get(node); if ( tmp != NULL) { delete node; node = tmp; - } else { + } else if(create) { nodes->add(node); + } else{ + delete node; + return NULL; } return node; } @@ -123,14 +126,17 @@ OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) { return tmp; } -OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) { +OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end, bool create) { OrderEdge *edge = new OrderEdge(begin, end); OrderEdge *tmp = edges->get(edge); if ( tmp != NULL ) { delete edge; edge = tmp; - } else { + } else if (create) { edges->add(edge); + } else { + delete edge; + return NULL; } return edge; } diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h index 5f10c1f..d508d03 100644 --- a/src/ASTAnalyses/ordergraph.h +++ b/src/ASTAnalyses/ordergraph.h @@ -17,8 +17,8 @@ public: ~OrderGraph(); void addOrderConstraintToOrderGraph(BooleanOrder *bOrder); void addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder); - OrderNode *getOrderNodeFromOrderGraph(uint64_t id); - OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end); + OrderNode *getOrderNodeFromOrderGraph(uint64_t id, bool create = true); + OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end, bool create = true); OrderNode *lookupOrderNodeFromOrderGraph(uint64_t id); OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end); void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr); diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index 262497e..6be7bea 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -13,6 +13,7 @@ #include "mutableset.h" #include "ordergraph.h" #include "csolver.h" +#include "decomposeorderresolver.h" DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver) @@ -77,7 +78,7 @@ void DecomposeOrderTransform::doTransform(){ neworder->addOrderConstraint(orderconstraint); } } - + currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) ); uint pcvsize = partialcandidatevec.getSize(); for (uint i = 0; i < pcvsize; i++) { Order *neworder = partialcandidatevec.get(i); diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h index 4d71805..90a97eb 100644 --- a/src/Encoders/orderencoding.h +++ b/src/Encoders/orderencoding.h @@ -11,7 +11,8 @@ typedef enum OrderEncodingType OrderEncodingType; class OrderEncoding { public: OrderEncoding(Order *order); - + + OrderResolver* resolver; OrderEncodingType type; Order *order; CMEMALLOC; diff --git a/src/Makefile b/src/Makefile index 5adb178..e6699e6 100644 --- a/src/Makefile +++ b/src/Makefile @@ -4,16 +4,16 @@ PHONY += directories MKDIR_P = mkdir -p OBJ_DIR = bin -CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) +CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) -C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) +C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) -HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) +HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o) CFLAGS := -Wall -g -O0 -CFLAGS += -IAST -IASTTransform -IASTAnalyses -ICollections -IBackend -I. -IEncoders -ITuner +CFLAGS += -IAST -IASTTransform -IASTAnalyses -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner LDFLAGS := -ldl -lrt -rdynamic SHARED := -shared @@ -34,6 +34,7 @@ ${OBJ_DIR}: ${MKDIR_P} ${OBJ_DIR}/AST ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses ${MKDIR_P} ${OBJ_DIR}/ASTTransform + ${MKDIR_P} ${OBJ_DIR}/Translator ${MKDIR_P} ${OBJ_DIR}/Tuner ${MKDIR_P} ${OBJ_DIR}/Collections ${MKDIR_P} ${OBJ_DIR}/Backend diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc new file mode 100644 index 0000000..49d8855 --- /dev/null +++ b/src/Translator/decomposeorderresolver.cc @@ -0,0 +1,32 @@ + +/* + * File: DecomposeOrderResolver.cc + * Author: hamed + * + * Created on September 1, 2017, 10:36 AM + */ + +#include "decomposeorderresolver.h" +#include "order.h" +#include "ordernode.h" +#include "ordergraph.h" + +DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector& _orders): + OrderResolver(_graph), + orders(_orders.getSize(), _orders.expose()) +{ +} + +DecomposeOrderResolver::~DecomposeOrderResolver() { + delete graph; +} + +HappenedBefore DecomposeOrderResolver::getOrder(OrderNode* from, OrderNode* to){ + ASSERT(from->id == to->id); + // We should ask this query from the suborder .... + Order *suborder = NULL; + suborder = orders.get(from->sccNum); + ASSERT(suborder != NULL); + return suborder->encoding.resolver->resolveOrder(from->id, to->id); +} + diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h new file mode 100644 index 0000000..6a7d735 --- /dev/null +++ b/src/Translator/decomposeorderresolver.h @@ -0,0 +1,28 @@ + +/* + * File: DecomposeOrderResolver.h + * Author: hamed + * + * Created on September 1, 2017, 10:36 AM + */ + +#ifndef DECOMPOSEORDERRESOLVER_H +#define DECOMPOSEORDERRESOLVER_H +#include "classlist.h" +#include "mymemory.h" +#include "structs.h" +#include "orderresolver.h" + +class DecomposeOrderResolver : public OrderResolver{ +public: + DecomposeOrderResolver(OrderGraph* graph, Vector & orders); + virtual ~DecomposeOrderResolver(); +private: + OrderGraph* graph; + Vector orders; + + HappenedBefore getOrder(OrderNode* from, OrderNode* to); +}; + +#endif /* DECOMPOSEORDERRESOLVER_H */ + diff --git a/src/Translator/orderresolver.cc b/src/Translator/orderresolver.cc new file mode 100644 index 0000000..5ed3a5e --- /dev/null +++ b/src/Translator/orderresolver.cc @@ -0,0 +1,39 @@ +#include "orderresolver.h" +#include "ordergraph.h" +#include "ordernode.h" +#include "orderedge.h" + +OrderResolver::OrderResolver(OrderGraph* _graph) + :graph(_graph) +{ +} + +OrderResolver::~OrderResolver(){ + delete graph; +} + +HappenedBefore OrderResolver::resolveOrder(uint64_t first, uint64_t second){ + OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/); + if(from == NULL){ + return SATC_UNORDERED; + } + OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false); + if(from == NULL){ + return SATC_UNORDERED; + } + if (from->sccNum != to->sccNum) { + OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/); + if (edge != NULL && edge->mustPos){ + return SATC_FIRST; + } else if( edge != NULL && edge->mustNeg){ + return SATC_SECOND; + }else { + ASSERT(0); + //It's a case that either there's no edge, or there is an edge + // but we don't know the value! (This case shouldn't happen) + //return from->sccNum < to->sccNum? SATC_FIRST: SATC_SECOND; + } + } else { + return getOrder(from, to); + } +} \ No newline at end of file diff --git a/src/Translator/orderresolver.h b/src/Translator/orderresolver.h new file mode 100644 index 0000000..9f248af --- /dev/null +++ b/src/Translator/orderresolver.h @@ -0,0 +1,27 @@ + +/* + * File: orderresolver.h + * Author: hamed + * + * Created on August 31, 2017, 7:16 PM + */ + +#ifndef ORDERRESOLVER_H +#define ORDERRESOLVER_H +#include "classlist.h" +#include "structs.h" +#include "mymemory.h" + +class OrderResolver { +public: + OrderResolver(OrderGraph* _graph); + HappenedBefore resolveOrder(uint64_t first, uint64_t second); + virtual ~OrderResolver(); + CMEMALLOC; +protected: + OrderGraph* graph; + virtual HappenedBefore getOrder(OrderNode* from, OrderNode* to) = 0; +}; + +#endif /* ORDERRESOLVER_H */ + diff --git a/src/Backend/sattranslator.cc b/src/Translator/sattranslator.cc similarity index 100% rename from src/Backend/sattranslator.cc rename to src/Translator/sattranslator.cc diff --git a/src/Backend/sattranslator.h b/src/Translator/sattranslator.h similarity index 100% rename from src/Backend/sattranslator.h rename to src/Translator/sattranslator.h diff --git a/src/classlist.h b/src/classlist.h index e8ab113..d56a650 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -13,6 +13,7 @@ #include "mymemory.h" #include #include "classes.h" +#include "AST/astnode.h" class BooleanOrder; @@ -59,6 +60,9 @@ class TunableSetting; class TunableDesc; +class OrderResolver; +class DecomposeOrderResolver; + struct IncrementalSolver; typedef struct IncrementalSolver IncrementalSolver; struct TableEntry; diff --git a/src/mymemory.h b/src/mymemory.h index 09ea7cd..8ad874b 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -24,7 +24,8 @@ void ourfree(void *ptr); void * ourcalloc(size_t count, size_t size); void * ourrealloc(void *ptr, size_t size); - */ +*/ + /* void * model_malloc(size_t size); void model_free(void *ptr); void * model_calloc(size_t count, size_t size); @@ -35,11 +36,12 @@ void * model_realloc(void *ptr, size_t size); #define ourfree model_free #define ourrealloc model_realloc #define ourcalloc model_calloc -/* +*/ + static inline void *ourmalloc(size_t size) { return malloc(size); } static inline void ourfree(void *ptr) { free(ptr); } static inline void *ourcalloc(size_t count, size_t size) { return calloc(count, size); } -static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }*/ +static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); } #define CMEMALLOC \ void *operator new(size_t size) { \ -- 2.34.1