constgen.h

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 #ifndef CONSTGEN_H
  11 #define CONSTGEN_H
  12 #include "classlist.h"
  13 #include "stl-model.h"
  14
  15
  16 #ifdef VERBOSE_CONSTRAINTS
  17 #define ADDCONSTRAINT(cn, str) do {Constraint *c=cn; model_print("%s ",str);c->print();model_print("\n");addConstraint(c);} while(0);
  18 #define ADDCONSTRAINT2(cg, cn, str) do {Constraint *c=cn; model_print("%s ",str);c->print();model_print("\n");cg->addConstraint(c);} while(0);
  19
  20 #define ADDGOAL(r, cn, str) do {Constraint *c=cn; model_print("%s ",str);c->print();model_print("\n");addGoal(r, c);} while(0);
  21 #define ADDBRANCHGOAL(r, cn, str) do {Constraint *c=cn; model_print("%s ",str);c->print();model_print("\n");addBranchGoal(r, c);} while(0);
  22 #else
  23
  24 #define ADDCONSTRAINT(cn, store) addConstraint(cn);
  25 #define ADDCONSTRAINT2(cg, cn, store) cg->addConstraint(cn);
  26
  27 #define ADDGOAL(r, cn, store) addGoal(r, cn);
  28 #define ADDBRANCHGOAL(r, cn, store) addBranchGoal(r, cn);
  29 #endif
  30
  31 unsigned int RecPairHash(RecPair *rp);
  32 bool RecPairEquals(RecPair *r1, RecPair *r2);
  33 typedef HashTable<RecPair *, RecPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RecPairHash, RecPairEquals> RecPairTable;
  34
  35 typedef HashTable<EPRecord *, uint, uintptr_t, 0, model_malloc, model_calloc, model_free> RecToIntTable;
  36
  37 #ifdef STATS
  38 struct MC_Stat {
  39         long long time;
  40         int bgoals;
  41         int fgoals;
  42         bool was_incremental;
  43         bool was_sat;
  44         MEMALLOC;
  45 };
  46 #endif
  47
  48 class ConstGen {
  49 public:
  50         ConstGen(MCExecution *e);
  51         ~ConstGen();
  52         bool process();
  53         void reset();
  54         bool canReuseEncoding();
  55         Constraint * getNewVar();
  56         void getArrayNewVars(uint num, Constraint **);
  57         RecordSet * computeConflictSet(EPRecord *store, EPRecord *load, RecordSet *baseset);
  58         RecordSet * getMayReadFromSet(EPRecord *load);
  59         RecordSet * getMayReadFromSetOpt(EPRecord *load);
  60         void addConstraint(Constraint *c);
  61         bool * runSolver();
  62         StoreLoadSet * getStoreLoadSet(EPRecord *op);
  63         Constraint * getOrderConstraint(EPRecord *first, EPRecord *second);
  64         Constraint * getExecutionConstraint(EPRecord *record);
  65         bool isAlwaysExecuted(EPRecord *record);
  66         BranchRecord * getBranchRecord(EPRecord *branch) {return branchtable->get(branch);}
  67         bool getOrder(EPRecord *first, EPRecord *second, bool * satsolution);
  68         void printConstraint(uint value);
  69         void printNegConstraint(uint value);
  70         void achievedGoal(EPRecord *record);
  71 #ifdef STATS
  72         MC_Stat *curr_stat;
  73 #endif
  74
  75         MEMALLOC;
  76 private:
  77         Constraint * getRetValueEncoding(EPRecord *record, uint64_t value);
  78         Constraint * getMemValueEncoding(EPRecord *record, uint64_t value);
  79         bool subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record);
  80
  81         void addBranchGoal(EPRecord *, Constraint *c);
  82         void addGoal(EPRecord *, Constraint *c);
  83         void translateGoals();
  84
  85         /** Methods to print execution graph .*/
  86         void printEventGraph();
  87         void printRecord(EPRecord *record, int file);
  88         void doPrint(EPRecord *record, int file);
  89
  90         /** Methods to traverse execution graph .*/
  91         void traverse(bool initial);
  92         void traverseRecord(EPRecord *record, bool initial);
  93
  94         /** Methods for initially visit records */
  95         void visitRecord(EPRecord *record);
  96         void insertAction(EPRecord *record);
  97         void insertFunction(EPRecord *record);
  98         void insertEquals(EPRecord *record);
  99         void insertBranch(EPRecord *record);
 100         void insertNonLocal(EPRecord *record);
 101         void insertLabel(EPRecord *record);
 102
 103         /** Methods for second pass over records */
 104         void processRecord(EPRecord *record);
 105         void processYield(EPRecord *record);
 106         void processFunction(EPRecord *record);
 107         void processEquals(EPRecord *record);
 108         void processLoopPhi(EPRecord *record);
 109         void processPhi(EPRecord *record);
 110         void processCAS(EPRecord *record);
 111         void processEXC(EPRecord *record);
 112         void processAdd(EPRecord *record);
 113         void processStore(EPRecord *record);
 114         void processBranch(EPRecord *record);
 115         void processLoad(EPRecord *record);
 116         void processAddresses(EPRecord *record);
 117         void recordExecCond(EPRecord *record);
 118         void computeYieldCond(EPRecord *record);
 119
 120         /** TSO Specific methods */
 121 #ifdef TSO
 122         void genTSOTransOrderConstraints();
 123         void insertTSOAction(EPRecord *record);
 124         void processFence(EPRecord *record);
 125 #endif
 126
 127         /** These functions build closed groups of memory operations that
 128                         can store/load from each other. */
 129         void groupMemoryOperations(EPRecord *op);
 130         void mergeSets(StoreLoadSet *to, StoreLoadSet *from);
 131
 132         bool orderThread(EPRecord *first, EPRecord *second);
 133         void createOrderConstraint(EPRecord *r1, EPRecord *r2);
 134         void genTransOrderConstraints();
 135         void genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec, ModelVector<EPRecord *> * t3vec);
 136         void genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec);
 137         void genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec);
 138
 139         /** The hashtable maps an address to the closure set of
 140                         memory operations that may touch that address. */
 141         StoreLoadSetHashTable *storeloadtable;
 142         /** This hashtable maps a load to all of the stores it may read
 143                         from. */
 144         LoadHashTable *loadtable;
 145
 146         MCExecution *execution;
 147         ModelVector<EPRecord *> * workstack;
 148         ModelVector<ModelVector<EPRecord *> *> * threadactions;
 149         RecPairTable *rpt;
 150         uint numconstraints;
 151         ModelVector<Constraint *> * goalset;
 152         ModelVector<EPRecord *> *yieldlist;
 153         Constraint ** goalvararray;
 154         ModelVector<Constraint *> * vars;
 155         BranchTable * branchtable;
 156         FunctionTable *functiontable;
 157         EqualsTable *equalstable;
 158         ScheduleBuilder *schedulebuilder;
 159         RecordSet *nonlocaltrans;
 160         RecordSet *incompleteexploredbranch;
 161         LoadHashTable *execcondtable;
 162         IncrementalSolver *solver;
 163         RecToIntTable *rectoint;
 164         RecToConsTable *yieldtable;
 165 #ifdef STATS
 166         ModelVector<struct MC_Stat *> * stats;
 167 #endif
 168         uint varindex;
 169         int schedule_graph;
 170         bool has_untaken_branches;
 171 };
 172
 173 class RecPair {
 174 public:
 175         RecPair(EPRecord *r1, EPRecord *r2) :
 176                 epr1(r1),
 177                 epr2(r2),
 178                 constraint(NULL) {
 179         }
 180         EPRecord *epr1;
 181         EPRecord *epr2;
 182         Constraint *constraint;
 183         MEMALLOC;
 184 };
 185
 186 #endif