From 677be047108738c94bb836f95b9db4d052912c5a Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 18 Jul 2018 16:02:21 -0700 Subject: [PATCH] edits --- src/AST/boolean.h | 2 +- src/AST/element.cc | 2 + src/AST/rewriter.cc | 88 +++++++++++++------ .../Polarity/polarityassignment.cc | 19 ++++ src/ASTAnalyses/Polarity/polarityassignment.h | 2 + src/classes.h | 1 + src/csolver.h | 3 +- 7 files changed, 86 insertions(+), 31 deletions(-) diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 207b327..1b5d24d 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -21,7 +21,7 @@ public: virtual bool isFalse() {return boolVal == BV_MUSTBEFALSE;} Polarity polarity; BooleanValue boolVal; - Vector parents; + Vector parents; virtual void updateParents() {} CMEMALLOC; diff --git a/src/AST/element.cc b/src/AST/element.cc index 565187a..9642d9c 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -59,6 +59,8 @@ Element *ElementFunction::clone(CSolver *solver, CloneMap *map) { void ElementFunction::updateParents() { for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this); + if (overflowstatus) + overflowstatus->parents.push(this); } Set *ElementFunction::getRange() { diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index 804d9de..58ef96b 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -2,6 +2,7 @@ #include "boolean.h" #include "csolver.h" #include "polarityassignment.h" +#include "element.h" void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) { if (constraints.contains(bexpr.negate())) { @@ -26,25 +27,41 @@ void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) { uint size = bexpr->parents.getSize(); for (uint i = 0; i < size; i++) { - Boolean *parent = bexpr->parents.get(i); - ASSERT(parent->type == LOGICOP); - BooleanLogic *logicop = (BooleanLogic *) parent; - switch (logicop->op) { - case SATC_AND: - handleANDTrue(logicop, bexpr); - break; - case SATC_IFF: - handleIFFTrue(logicop, bexpr); - break; - case SATC_NOT: - case SATC_OR: - case SATC_XOR: - case SATC_IMPLIES: - ASSERT(0); + ASTNode *parent = bexpr->parents.get(i); + if (parent->type == ELEMFUNCRETURN) { + ElementFunction *ef = (ElementFunction *) parent; + handleFunction(ef, bexpr); + } else { + ASSERT(parent->type == LOGICOP); + BooleanLogic *logicop = (BooleanLogic *) parent; + switch (logicop->op) { + case SATC_AND: + handleANDTrue(logicop, bexpr); + break; + case SATC_IFF: + handleIFFTrue(logicop, bexpr); + break; + case SATC_NOT: + case SATC_OR: + case SATC_XOR: + case SATC_IMPLIES: + ASSERT(0); + } } } } +void CSolver::handleFunction(ElementFunction * ef, BooleanEdge child) { + BooleanEdge childNegate = child.negate(); + elemMap.remove(ef); + if (ef->overflowstatus == child) { + ef->overflowstatus = boolTrue; + } else if (ef->overflowstatus == childNegate) { + ef->overflowstatus = boolFalse; + } + elemMap.put(ef, ef); +} + void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) { //Canonicalize if (oldb.isNegated()) { @@ -74,22 +91,35 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) { BooleanEdge oldbnegated = oldb.negate(); uint size = oldb->parents.getSize(); for (uint i = 0; i < size; i++) { - Boolean *parent = oldb->parents.get(i); - BooleanLogic *logicop = (BooleanLogic *) parent; - boolMap.remove(parent); //could change parent's hash - - uint parentsize = logicop->inputs.getSize(); - for (uint j = 0; j < parentsize; j++) { - BooleanEdge b = logicop->inputs.get(j); - if (b == oldb) { - logicop->inputs.set(j, newb); - newb->parents.push(parent); - } else if (b == oldbnegated) { - logicop->inputs.set(j, newb.negate()); - newb->parents.push(parent); + ASTNode *parent = oldb->parents.get(i); + if (parent->type == ELEMFUNCRETURN) { + ElementFunction *ef = (ElementFunction *) parent; + elemMap.remove(ef); + if (ef->overflowstatus == oldb) { + ef->overflowstatus = newb; + newb->parents.push(ef); + } else if (ef->overflowstatus == oldbnegated) { + ef->overflowstatus = newb.negate(); + newb->parents.push(ef); + } + elemMap.put(ef, ef); + } else { + BooleanLogic *logicop = (BooleanLogic *) parent; + boolMap.remove(logicop); //could change parent's hash + + uint parentsize = logicop->inputs.getSize(); + for (uint j = 0; j < parentsize; j++) { + BooleanEdge b = logicop->inputs.get(j); + if (b == oldb) { + logicop->inputs.set(j, newb); + newb->parents.push(logicop); + } else if (b == oldbnegated) { + logicop->inputs.set(j, newb.negate()); + newb->parents.push(logicop); + } } + boolMap.put(logicop, logicop); } - boolMap.put(parent, parent); } } diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc index ef988dd..dc69a57 100644 --- a/src/ASTAnalyses/Polarity/polarityassignment.cc +++ b/src/ASTAnalyses/Polarity/polarityassignment.cc @@ -59,6 +59,25 @@ void computePredicatePolarity(BooleanPredicate *This) { if (This->undefStatus) { computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE); } + for(uint i=0; i < This->inputs.getSize(); i++) { + Element * e = This->inputs.get(i); + computeElement(e); + } +} + +void computeElement(Element *e) { + if (e->type == ELEMFUNCRETURN) { + ElementFunction *ef = (ElementFunction *) e; + + if (ef->overflowstatus) { + computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE); + } + + for(uint i=0; i < ef->inputs.getSize(); i++) { + Element * echild = ef->inputs.get(i); + computeElement(echild); + } + } } void computeLogicOpPolarity(BooleanLogic *This) { diff --git a/src/ASTAnalyses/Polarity/polarityassignment.h b/src/ASTAnalyses/Polarity/polarityassignment.h index ce5096f..5cf345c 100644 --- a/src/ASTAnalyses/Polarity/polarityassignment.h +++ b/src/ASTAnalyses/Polarity/polarityassignment.h @@ -12,12 +12,14 @@ #include "common.h" #include "ops.h" #include "boolean.h" +#include "element.h" void computePolarities(CSolver *This); bool updatePolarity(Boolean *This, Polarity polarity); void updateEdgePolarity(BooleanEdge dst, BooleanEdge src); void updateEdgePolarity(BooleanEdge dst, Polarity polarity); void updateMustValue(Boolean *This, BooleanValue value); +void computeElement(Element *e); void computePolarity(Boolean *boolean, Polarity polarity); void computePredicatePolarity(BooleanPredicate *This); void computeLogicOpPolarity(BooleanLogic *boolean); diff --git a/src/classes.h b/src/classes.h index db98ab2..58f5a02 100644 --- a/src/classes.h +++ b/src/classes.h @@ -27,6 +27,7 @@ class Transformer; class Set; class BooleanLogic; class Serializer; +class ElementFunction; typedef uint64_t VarType; typedef unsigned int uint; diff --git a/src/csolver.h b/src/csolver.h index b84d324..53e1901 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -175,7 +175,8 @@ public: private: void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child); void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child); - + void handleFunction(ElementFunction * ef, BooleanEdge child); + //These two functions are helpers if the client has a pointer to a //Boolean object that we have since replaced BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize); -- 2.34.1