30ece3bb1d706803e32d4028aa4bac305737ab8a
[satcheck.git] / eprecord.cc
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 #include "eprecord.h"
11 #include "change.h"
12 #include "model.h"
13 #include "planner.h"
14
15 EPRecord::EPRecord(EventType _event, ExecPoint *_execpoint, EPValue *_branch, uintptr_t _offset, unsigned int _numinputs, uint _len, bool _anyvalue) :
16         valuevector(new ValueVector()),
17         execpoint(_execpoint),
18         completed(NULL),
19         branch(_branch),
20         setarray((IntHashSet **)model_malloc(sizeof(IntHashSet *)*(_numinputs+VC_BASEINDEX))),
21         nextRecord(NULL),
22         childRecord(NULL),
23         philooptable(NULL),
24         offset(_offset),
25         event(_event),
26         jointhread(THREAD_ID_T_NONE),
27         numinputs(_numinputs+VC_BASEINDEX),
28         len(_len),
29         anyvalue(_anyvalue),
30         phi(false),
31         loopphi(false),
32         size(0),
33         func_shares_goalset(false),
34         ptr(NULL)
35 {
36         for(unsigned int i=0;i<numinputs;i++)
37                 setarray[i]=new IntHashSet();
38 }
39
40 EPRecord::~EPRecord() {
41         if (!func_shares_goalset && (completed != NULL))
42                 delete completed;
43         delete valuevector;
44         if (completed != NULL)
45                 delete completed;
46         if (philooptable!=NULL) {
47                 EPRecordIDIterator *rit=philooptable->iterator();
48                 while(rit->hasNext()) {
49                         struct RecordIDPair *val=rit->next();
50                         model_free(val);
51                 }
52                 delete rit;
53                 delete philooptable;
54         }
55         model_free(setarray);
56 }
57
58 const char * eventToStr(EventType event) {
59         switch(event) {
60         case ALLOC:
61                 return "alloc";
62         case LOAD:
63                 return "load";
64         case RMW:
65                 return "rmw";
66         case STORE:
67                 return "store";
68         case BRANCHDIR:
69                 return "br_dir";
70         case MERGE:
71                 return "merge";
72         case FUNCTION:
73                 return "func";
74         case EQUALS:
75                 return "equals";
76         case THREADCREATE:
77                 return "thr_create";
78         case THREADBEGIN:
79                 return "thr_begin";
80         case THREADJOIN:
81                 return "join";
82         case YIELD:
83                 return "yield";
84         case NONLOCALTRANS:
85                 return "nonlocal";
86         case LOOPEXIT:
87                 return "loopexit";
88         case LABEL:
89                 return "label";
90         case LOOPENTER:
91                 return "loopenter";
92         case LOOPSTART:
93                 return "loopstart";
94         case FENCE:
95                 return "fence";
96         default:
97                 return "unknown";
98         }
99 }
100
101 IntHashSet * EPRecord::getReturnValueSet() {
102         switch(event) {
103         case FUNCTION:
104         case EQUALS:
105                 return getSet(VC_FUNCOUTINDEX);
106         case RMW:
107                 return getSet(VC_RMWOUTINDEX);
108         case LOAD:
109                 return getSet(VC_RFINDEX);
110         case ALLOC:
111         case BRANCHDIR:
112         case MERGE:
113         case STORE:
114         case THREADCREATE:
115         case THREADBEGIN:
116         case THREADJOIN:
117         case YIELD:
118         case FENCE:
119         case NONLOCALTRANS:
120         case LOOPEXIT:
121         case LABEL:
122         case LOOPENTER:
123         case LOOPSTART:
124                 ASSERT(false);
125                 return NULL;
126         default:
127                 ASSERT(false);
128                 return NULL;
129         }
130 }
131
132 void EPRecord::print(int f) {
133         if (event==RMW) {
134                 if (op==ADD)
135                         model_dprintf(f, "add");
136                 else if (op==EXC)
137                         model_dprintf(f, "exc");
138                 else
139                         model_dprintf(f, "cas");
140         } else
141                 model_dprintf(f, "%s",eventToStr(event));
142         IntHashSet *i=NULL;
143         switch(event) {
144         case LOAD:
145                 i=setarray[VC_RFINDEX];
146                 break;
147         case STORE:
148                 i=setarray[VC_BASEINDEX];
149                 break;
150         case RMW:
151                 i=setarray[VC_RMWOUTINDEX];
152                 break;
153         case FUNCTION: {
154                 if (!getPhi()) {
155                         CGoalIterator *cit=completed->iterator();
156                         model_dprintf(f, "{");
157                         while(cit->hasNext()) {
158                                 CGoal *goal=cit->next();
159                                 model_dprintf(f,"(");
160                                 for(uint i=0;i<getNumFuncInputs();i++) {
161                                         model_dprintf(f,"%llu ", goal->getValue(i+VC_BASEINDEX));
162                                 }
163                                 model_dprintf(f,"=> %llu)", goal->getOutput());
164                         }
165                         delete cit;
166                 }
167                 break;
168         }
169         default:
170                 ;
171         }
172         if (i!=NULL) {
173                 IntIterator *it=i->iterator();
174                 model_dprintf(f, "{");
175
176                 while(it->hasNext()) {
177                         model_dprintf(f, "%llu ", it->next());
178                 }
179                 model_dprintf(f, "}");
180                 delete it;
181         }
182
183         for(uint i=0;i<numinputs;i++) {
184                 IntIterator *it=setarray[i]->iterator();
185                 model_dprintf(f,"{");
186                 while(it->hasNext()) {
187                         uint64_t v=it->next();
188                         model_dprintf(f,"%llu ", v);
189                 }
190                 model_dprintf(f,"}");
191                 delete it;
192         }
193
194
195         execpoint->print(f);
196 }
197
198 void EPRecord::print() {
199         model_print("%s",eventToStr(event));
200         execpoint->print();
201         model_print(" CR=%p ", this);
202         model_print(" NR=%p", nextRecord);
203 }
204
205 bool EPRecord::hasAddr(const void * addr) {
206         return getSet(VC_ADDRINDEX)->contains((uintptr_t)addr);
207 }
208
209 int EPRecord::getIndex(EPValue *val) {
210         for(unsigned int i=0;i<valuevector->size();i++) {
211                 EPValue *epv=(*valuevector)[i];
212                 if (epv==val)
213                         return i;
214         }
215         return -1;
216 }
217
218 int EPRecord::getIndex(uint64_t val) {
219         for(unsigned int i=0;i<valuevector->size();i++) {
220                 EPValue *epv=(*valuevector)[i];
221                 if (epv->getValue()==val)
222                         return i;
223         }
224         return -1;
225 }
226
227 bool EPRecord::hasValue(uint64_t val) {
228         for(unsigned int i=0;i<valuevector->size();i++) {
229                 EPValue *epv=(*valuevector)[i];
230                 if (epv->getValue()==val)
231                         return true;
232         }
233         return false;
234 }
235
236 bool compatibleStoreLoad(EPRecord *store, EPRecord *load) {
237         return true;
238 }