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
 119         /** TSO Specific methods */
 120 #ifdef TSO
 121         void genTSOTransOrderConstraints();
 122         void insertTSOAction(EPRecord *record);
 123         void processFence(EPRecord *record);
 124 #endif
 125
 126         /** These functions build closed groups of memory operations that
 127                         can store/load from each other. */
 128         void groupMemoryOperations(EPRecord *op);
 129         void mergeSets(StoreLoadSet *to, StoreLoadSet *from);
 130
 131         bool orderThread(EPRecord *first, EPRecord *second);
 132         void createOrderConstraint(EPRecord *r1, EPRecord *r2);
 133         void genTransOrderConstraints();
 134         void genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec, ModelVector<EPRecord *> * t3vec);
 135         void genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec);
 136         void genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec);
 137
 138         /** The hashtable maps an address to the closure set of
 139                         memory operations that may touch that address. */
 140         StoreLoadSetHashTable *storeloadtable;
 141         /** This hashtable maps a load to all of the stores it may read
 142                         from. */
 143         LoadHashTable *loadtable;
 144
 145         MCExecution *execution;
 146         ModelVector<EPRecord *> * workstack;
 147         ModelVector<ModelVector<EPRecord *> *> * threadactions;
 148         RecPairTable *rpt;
 149         uint numconstraints;
 150         ModelVector<Constraint *> * goalset;
 151         Constraint ** goalvararray;
 152         ModelVector<Constraint *> * vars;
 153         BranchTable * branchtable;
 154         FunctionTable *functiontable;
 155         EqualsTable *equalstable;
 156         ScheduleBuilder *schedulebuilder;
 157         RecordSet *nonlocaltrans;
 158         LoadHashTable *execcondtable;
 159         IncrementalSolver *solver;
 160         RecToIntTable *rectoint;
 161 #ifdef STATS
 162         ModelVector<struct MC_Stat *> * stats;
 163 #endif
 164         uint varindex;
 165         int schedule_graph;
 166         bool has_untaken_branches;
 167 };
 168
 169 class RecPair {
 170  public:
 171  RecPair(EPRecord *r1, EPRecord *r2) :
 172         epr1(r1),
 173         epr2(r2),
 174         constraint(NULL) {
 175         }
 176         EPRecord *epr1;
 177         EPRecord *epr2;
 178         Constraint *constraint;
 179         MEMALLOC;
 180 };
 181
 182 #endif