36afe0b81f030112102e0f7a07e2ae1c9e69c09f
[satcheck.git] / mcexecution.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 "mcexecution.h"
11 #include "mcschedule.h"
12 #include "planner.h"
13 #include <stdarg.h>
14 #include "cgoal.h"
15 #include "change.h"
16 #include "mcutil.h"
17 #include "model.h"
18 #include <fcntl.h>
19 #include <unistd.h>
20 #include <string.h>
21 #include "constgen.h"
22
23 MCExecution_snapshot::MCExecution_snapshot() :
24         next_thread_id(0)
25 {
26 }
27
28 MCExecution_snapshot::~MCExecution_snapshot() {
29 }
30
31
32 MCExecution::MCExecution() :
33         EPTable(new EPHashTable()),
34         EPValueTable(new EPValueHashTable()),
35         memtable(new MemHashTable()),
36         storetable(new StoreLoadHashTable()),
37         loadtable(new StoreLoadHashTable()),
38         EPList(new SnapVector<EPValue *>()),
39         ThreadList(new SnapVector<Thread *>()),
40         ExecPointList(new SnapVector<ExecPoint *>()),
41         CurrBranchList(new SnapVector<EPValue *>()),
42         currexecpoint(NULL),
43         scheduler(new MCScheduler(this)),
44         planner(new Planner(this)),
45         snap_fields(new MCExecution_snapshot()),
46         curr_thread(NULL),
47         currbranch(NULL),
48         eprecorddep(new EPRecordDepHashTable()),
49         revrecorddep(new RevDepHashTable()),
50         alwaysexecuted(new ModelVector<EPRecord *>()),
51         lastloopexit(new ModelVector<EPRecord *>()),
52         joinvec(new ModelVector<EPRecord *>()),
53         sharedgoals(new ModelVector<CGoalSet *>()),
54         sharedfuncrecords(new ModelVector<RecordSet *>()),
55         currid(MCID_INIT),
56         schedule_graph(0)
57 {
58         EPList->push_back(NULL);//avoid using MCID of 0
59 #ifdef TSO
60         storebuffer = new SnapVector<SnapList<EPValue *> *>();
61 #endif
62 }
63
64 MCExecution::~MCExecution() {
65         reset();
66         delete EPTable;
67         delete EPValueTable;
68         delete memtable;
69         delete EPList;
70         delete ThreadList;
71         delete ExecPointList;
72         delete scheduler;
73         delete snap_fields;
74         delete eprecorddep;
75         delete revrecorddep;
76         delete joinvec;
77         delete alwaysexecuted;
78         delete lastloopexit;
79 #ifdef TSO
80         for(uint i=0;i<storebuffer->size();i++) {
81                 SnapList<EPValue *> *list=(*storebuffer)[i];
82                 if (list != NULL)
83                         delete list;
84         }
85         delete storebuffer;
86 #endif
87         for(uint i=0;i<sharedgoals->size();i++) {
88                 CGoalSet *c=(*sharedgoals)[i];
89                 if (c != NULL)
90                         delete c;
91         }
92         delete sharedgoals;
93         for(uint i=0;i<sharedfuncrecords->size();i++) {
94                 RecordSet *rs=(*sharedfuncrecords)[i];
95                 if (rs != NULL)
96                         delete rs;
97         }
98         delete sharedfuncrecords;
99 }
100
101 /** @brief Resets MCExecution object for next execution. */
102
103 void MCExecution::reset() {
104         currid=MCID_INIT;
105         currbranch=NULL;
106         alwaysexecuted->clear();
107 }
108
109 void MCExecution::dumpExecution() {
110         char buffer[128];
111         sprintf(buffer, "exec%u.dot",schedule_graph);
112         schedule_graph++;
113         int file=open(buffer,O_WRONLY|O_TRUNC|O_CREAT, S_IRWXU);
114         dprintf(file, "digraph execution {\n");
115         EPRecord *last=NULL;
116         for(uint i=0;i<EPList->size();i++) {
117                 EPValue *epv=(*EPList)[i];
118                 if (epv==NULL)
119                         continue;
120                 EPRecord *record=epv->getRecord();
121                 dprintf(file, "%lu[label=\"",(uintptr_t)record);
122                 record->print(file);
123                 dprintf(file, "\"];\n");
124                 if (last!=NULL)
125                         dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record);
126                 last=record;
127         }
128         dprintf(file, "}\n");
129         close(file);
130 }
131
132 /** @brief Records the MCID and returns the next MCID */
133
134 MCID MCExecution::loadMCID(MCID maddr, uintptr_t offset) {
135         scheduler->check_preempt();
136         id_addr=maddr;
137         id_addr_offset=offset;
138         return id_retval=getNextMCID();
139 }
140
141 /** @brief Records the address and value MCIDs. */
142
143 void MCExecution::storeMCID(MCID maddr, uintptr_t offset, MCID val) {
144 #ifndef TSO
145         scheduler->check_preempt();
146 #endif
147         id_addr=maddr;
148         id_addr_offset=offset;
149         id_value=val;
150 }
151
152 /** @brief Records MCIDs for a RMW. */
153
154 MCID MCExecution::nextRMW(MCID maddr, uintptr_t offset, MCID oldval, MCID valarg) {
155         scheduler->check_preempt();
156         id_addr=maddr;
157         id_addr_offset=offset;
158         id_oldvalue=oldval;
159         id_value=valarg;
160         id_retval=getNextMCID();
161         return id_retval;
162 }
163
164 uint64_t dormwaction(enum atomicop op, void *addr, uint len, uint64_t currval, uint64_t oldval, uint64_t valarg, uint64_t *newval) {
165         uint64_t retval;
166         uint64_t memval;
167         switch(op) {
168         case ADD:
169                 retval=currval;
170                 memval=currval+valarg;
171                 break;
172         case CAS:
173                 retval=currval;
174                 if (currval==oldval) {
175                         memval=valarg;
176                 } else {
177                         memval=currval;
178                 }
179                 break;
180         case EXC:
181                 retval=currval;
182                 memval=valarg;
183                 break;
184         default:
185                 ASSERT(false);
186                 return -1;
187         }
188
189         *newval=memval&getmask(len);
190
191         if (op==ADD || (op==CAS && (currval==oldval)) || (op == EXC)) {
192                 switch(len) {
193                 case 1:
194                         *((uint8_t *)addr)=*newval;
195                         break;
196                 case 2:
197                         *((uint16_t *)addr)=*newval;
198                         break;
199                 case 4:
200                         *((uint32_t *)addr)=*newval;
201                         break;
202                 case 8:
203                         *((uint64_t *)addr)=*newval;
204                         break;
205                 }
206         }
207         return retval;
208 }
209
210 /** @brief Implement atomic RMW. */
211 uint64_t MCExecution::rmw(enum atomicop op, void *addr, uint len, uint64_t currval, uint64_t oldval, uint64_t valarg) {
212         uint64_t newval;
213         uint64_t retval=dormwaction(op, addr, len, currval, oldval, valarg, &newval);
214         if (DBG_ENABLED()) {
215                 model_print("RMW %p oldval=%lu valarg=%lu retval=%lu", addr, oldval, valarg, retval);
216                 currexecpoint->print();
217                 model_print("\n");
218         }
219
220         int num_mcids=(op==ADD)?1:2;
221         EPRecord * record=getOrCreateCurrRecord(RMW, NULL, id_addr_offset, VC_RMWOUTINDEX-VC_RFINDEX, len, false);
222         record->setRMW(op);
223
224         recordRMWChange(record, addr, valarg, oldval, newval);
225         addLoadTable(addr, record);
226         addStoreTable(addr, record);
227         EPValue * epvalue=getEPValue(record, NULL, addr, retval, len);
228         MCID vcrf=memtable->get(addr);
229         MCID mcids[]={id_value, id_oldvalue};
230         recordContext(epvalue, vcrf, id_addr, num_mcids, mcids);
231         ASSERT(EPList->size()==id_retval);
232         EPList->push_back(epvalue);
233         memtable->put(addr, id_retval);
234         currexecpoint->incrementTop();
235         return retval;
236 }
237
238 /** @brief Gets an EPRecord for the current execution point.  */
239
240 EPRecord * MCExecution::getOrCreateCurrRecord(EventType et, bool * isNew, uintptr_t offset,  unsigned int numinputs, uint len, bool br_anyvalue) {
241         EPRecord *record=EPTable->get(currexecpoint);
242         if (isNew!=NULL)
243                 *isNew=(record==NULL);
244         if (record==NULL) {
245                 ExecPoint * ep=new ExecPoint(currexecpoint);
246                 record=new EPRecord(et, ep, currbranch, offset, numinputs, len, br_anyvalue);
247                 if (et==THREADJOIN) {
248                         joinvec->push_back(record);
249                 }
250                 EPTable->put(ep, record);
251         } else {
252                 ASSERT(record->getOffset()==offset);
253         }
254         if (currbranch==NULL) {
255                 uint tid=id_to_int(currexecpoint->get_tid());
256                 if (alwaysexecuted->size()<=tid) {
257                         alwaysexecuted->resize(tid+1);
258                 }
259                 if ((*alwaysexecuted)[tid]!=NULL && et != LABEL && et != LOOPSTART)
260                         (*alwaysexecuted)[tid]->setNextRecord(record);
261                 (*alwaysexecuted)[tid]=record;
262         } else {
263                 if (currbranch->firstrecord==NULL)
264                         currbranch->firstrecord=record;
265                 if (currbranch->lastrecord!=NULL && et != LABEL && et != LOOPSTART)
266                         currbranch->lastrecord->setNextRecord(record);
267                 currbranch->lastrecord=record;
268         }
269
270         return record;
271 }
272
273 /** @brief Gets an EPValue for the current record and value. */
274
275 EPValue * MCExecution::getEPValue(EPRecord * record, bool * isNew,  const void *addr, uint64_t val, int len) {
276         ExecPoint * ep=record->getEP();
277         EPValue * epvalue=new EPValue(ep, record, addr, val,len);
278         EPValue * curr=EPValueTable->get(epvalue);
279         if (curr!=NULL) {
280                 if (isNew!=NULL)
281                         *isNew=false;
282                 delete epvalue;
283         } else {
284                 if (isNew!=NULL)
285                         *isNew=true;
286                 EPValueTable->put(epvalue, epvalue);
287                 record->addEPValue(epvalue);
288                 curr=epvalue;
289         }
290         return curr;
291 }
292
293 /** @brief Lookup EPRecord for the MCID. */
294
295 EPRecord * MCExecution::getEPRecord(MCID id) {
296         return (*EPList)[id]->getRecord();
297 }
298
299 /** @brief Lookup EPValue for the MCID. */
300
301 EPValue * MCExecution::getEPValue(MCID id) {
302         return (*EPList)[id];
303 }
304
305 #ifdef TSO
306 bool MCExecution::isEmptyStoreBuffer(thread_id_t tid) {
307         SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
308         return list->empty();
309 }
310                 
311 void MCExecution::doStore(thread_id_t tid) {
312         SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
313         EPValue * epval=list->front();
314         list->pop_front();
315         if (DBG_ENABLED()) {
316                 model_print("tid = %lu: ", tid);
317         }
318         doStore(epval);
319 }
320
321 void MCExecution::doStore(EPValue *epval) {
322         const void *addr=epval->getAddr();
323         uint64_t val=epval->getValue();
324         int len=epval->getLen();
325         if (DBG_ENABLED()) {
326                 model_print("flushing %d bytes *(%p) = %lu", len, addr, val);
327                 currexecpoint->print();
328                 model_print("\n");
329         }       
330         switch(len) {
331         case 1:
332                 (*(uint8_t *)addr) = (uint8_t)val;
333                 break;
334         case 2:
335                 (*(uint16_t *)addr) = (uint16_t)val;
336                 break;
337         case 4:
338                 (*(uint32_t *)addr) = (uint32_t)val;
339                 break;
340         case 8:
341                 (*(uint64_t *)addr) = (uint64_t)val;
342                 break;
343         }
344 }
345
346 void MCExecution::fence() {
347         scheduler->check_preempt();
348         getOrCreateCurrRecord(FENCE, NULL, 0, 0, 8, false);
349         currexecpoint->incrementTop();
350         uint tid=id_to_int(currexecpoint->get_tid());
351         SnapList<EPValue *> * list=(*storebuffer)[tid];
352         while(!list->empty()) {
353                 EPValue * epval=list->front();
354                 list->pop_front();
355                 doStore(epval);
356         }
357 }
358 #endif
359
360 /** @brief EPValue is the corresponding epvalue object.
361                 For loads rf is the store we read from.
362                 For loads or stores, addr is the MCID for the provided address.
363                 numids is the number of MCID's we take in.
364                 We then list that number of MCIDs for everything we depend on.
365 */
366
367 void MCExecution::recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids) {
368         EPRecord *currrecord=epv->getRecord();
369
370         for(int i=0;i<numids;i++) {
371                 MCID id=mcids[i];
372                 if (id != MCID_NODEP) {
373                         EPRecord * epi=getEPRecord(id);
374                         addRecordDepTable(epi,currrecord, VC_BASEINDEX+i);
375                 }
376         }
377         if (rf != MCID_NODEP) {
378                 EPRecord *eprf=getEPRecord(rf);
379                 addRecordDepTable(eprf,currrecord, VC_RFINDEX);
380         }
381         if (addr != MCID_NODEP) {
382                 EPRecord *epaddr=getEPRecord(addr);
383                 addRecordDepTable(epaddr,currrecord, VC_ADDRINDEX);
384         }
385 }
386
387 /** @brief Processes a store. */
388
389 void MCExecution::store(void *addr, uint64_t val, int len) {
390 #ifndef TSO
391         switch(len) {
392         case 1:
393                 (*(uint8_t *)addr) = (uint8_t)val;
394                 break;
395         case 2:
396                 (*(uint16_t *)addr) = (uint16_t)val;
397                 break;
398         case 4:
399                 (*(uint32_t *)addr) = (uint32_t)val;
400                 break;
401         case 8:
402                 (*(uint64_t *)addr) = (uint64_t)val;
403                 break;
404         }
405 #endif
406         
407         if (DBG_ENABLED()) {
408                 model_print("STORE *%p=%lu ", addr, val);
409                 currexecpoint->print();
410                 model_print("\n");
411         }
412         EPRecord * record=getOrCreateCurrRecord(STORE, NULL, id_addr_offset, 1, len, false);
413         recordStoreChange(record, addr, val);
414         addStoreTable(addr, record);
415         EPValue * epvalue=getEPValue(record, NULL, addr, val, len);
416 #ifdef TSO
417         uint tid=id_to_int(currexecpoint->get_tid());
418         (*storebuffer)[tid]->push_back(epvalue);
419 #endif
420         MCID mcids[]={id_value};
421         recordContext(epvalue, MCID_NODEP, id_addr, 1, mcids);
422         MCID stmcid=getNextMCID();
423         ASSERT(stmcid==EPList->size());
424         EPList->push_back(epvalue);
425         memtable->put(addr, stmcid);
426         currexecpoint->incrementTop();
427 }
428
429 void MCExecution::recordFunctionChange(EPRecord *function, uint64_t val) {
430         if (function->getSet(VC_FUNCOUTINDEX)->add(val))
431                 planner->addChange(new MCChange(function, val, VC_FUNCOUTINDEX));
432 }
433
434 void MCExecution::recordRMWChange(EPRecord *rmw, const void *addr, uint64_t valarg, uint64_t oldval, uint64_t newval) {
435         if (!rmw->hasAddr(addr)) {
436                 rmw->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
437                 planner->addChange(new MCChange(rmw, (uint64_t)addr, VC_ADDRINDEX));
438         }
439         rmw->getSet(VC_BASEINDEX)->add(valarg);
440         if (rmw->getOp()==CAS)
441                 rmw->getSet(VC_OLDVALCASINDEX)->add(oldval);
442         if (!rmw->getSet(VC_RMWOUTINDEX)->contains(newval)) {
443                 rmw->getSet(VC_RMWOUTINDEX)->add(newval);
444                 planner->addChange(new MCChange(rmw, newval, VC_RMWOUTINDEX));
445         }
446 }
447
448 void MCExecution::recordLoadChange(EPRecord *load, const void *addr) {
449         if (!load->hasAddr(addr)) {
450                 load->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
451                 planner->addChange(new MCChange(load, (uint64_t)addr, VC_ADDRINDEX));
452         }
453 }
454
455 void MCExecution::recordStoreChange(EPRecord *store, const void *addr, uint64_t val) {
456         if (!store->hasAddr(addr)) {
457                 store->getSet(VC_ADDRINDEX)->add((uint64_t)addr);
458                 planner->addChange(new MCChange(store, (uint64_t)addr, VC_ADDRINDEX));
459         }
460         if (!store->hasValue(val)) {
461                 store->getSet(VC_BASEINDEX)->add(val);
462                 planner->addChange(new MCChange(store, val, VC_BASEINDEX));
463         }
464 }
465
466 /** @brief Processes a load. */
467
468 uint64_t MCExecution::load(const void *addr, int len) {
469 #ifdef TSO
470         uint64_t val=0;
471         bool found=false;
472         uint tid=id_to_int(currexecpoint->get_tid());
473         SnapList<EPValue *> *list=(*storebuffer)[tid];
474         for(SnapList<EPValue *>::reverse_iterator it=list->rbegin(); it != list->rend(); it++) {
475                 EPValue *epval=*it;
476                 const void *epaddr=epval->getAddr();
477                 if (epaddr == addr) {
478                         val = epval->getValue();
479                         found = true;
480                         break;
481                 }
482         }
483         if (!found) {
484                 switch(len) {
485                 case 1:
486                         val=*(uint8_t *) addr;
487                         break;
488                 case 2:
489                         val=*(uint16_t *) addr;
490                         break;
491                 case 4:
492                         val=*(uint32_t *) addr;
493                         break;
494                 case 8:
495                         val=*(uint64_t *) addr;
496                         break;
497                 }
498         }
499 #else
500         uint64_t val=0;
501         switch(len) {
502         case 1:
503                 val=*(uint8_t *) addr;
504                 break;
505         case 2:
506                 val=*(uint16_t *) addr;
507                 break;
508         case 4:
509                 val=*(uint32_t *) addr;
510                 break;
511         case 8:
512                 val=*(uint64_t *) addr;
513                 break;
514         }
515 #endif
516         
517         if (DBG_ENABLED()) {
518                 model_print("%lu(mid=%u)=LOAD %p ", val, id_retval, addr);
519                 currexecpoint->print();
520                 model_print("\n");
521         }
522         ASSERT(id_addr==MCID_NODEP || (getEPValue(id_addr)->getValue()+id_addr_offset)==((uint64_t)addr));
523         EPRecord * record=getOrCreateCurrRecord(LOAD, NULL, id_addr_offset, 0, len, false);
524         recordLoadChange(record, addr);
525         addLoadTable(addr, record);
526         EPValue * epvalue=getEPValue(record, NULL, addr, val, len);
527         MCID vcrf=memtable->get(addr);
528         recordContext(epvalue, vcrf, id_addr, 0, NULL);
529         ASSERT(EPList->size()==id_retval);
530         EPList->push_back(epvalue);
531         currexecpoint->incrementTop();
532         return val;
533 }
534
535 /** @brief Processes a branch. */
536
537 MCID MCExecution::branchDir(MCID dirid, int direction, int numdirs, bool anyvalue) {
538         if (DBG_ENABLED()) {
539                 model_print("BRANCH dir=%u mid=%u", direction, dirid);
540                 currexecpoint->print();
541                 model_print("\n");
542         }
543         EPRecord * record=getOrCreateCurrRecord(BRANCHDIR, NULL, 0, 1, numdirs, anyvalue);
544         bool isNew;
545         EPValue * epvalue=getEPValue(record, &isNew, NULL, direction, 32);
546         if (isNew) {
547 #ifdef PRINT_ACHIEVED_GOALS
548                 model_print("Achieved Goal: BRANCH dir=%u mid=%u", direction, dirid);
549                 currexecpoint->print();model_print("\n");
550 #endif
551 #ifdef STATS
552                 planner->getConstGen()->curr_stat->bgoals++;
553 #endif
554                 planner->getConstGen()->achievedGoal(record);
555                 scheduler->setNewFlag();
556         }
557         //record that we took a branch
558         currbranch=epvalue;
559         currbranch->lastrecord=NULL;
560         MCID mcids[]={dirid};
561         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
562         MCID brmcid=getNextMCID();
563         ASSERT(EPList->size()==brmcid);
564         EPList->push_back(epvalue);
565         //push the direction of the branch
566         currexecpoint->push(EP_BRANCH,direction);
567         //push the statement counter for the branch
568         currexecpoint->push(EP_COUNTER,0);
569
570         return brmcid;
571 }
572
573 /** @brief Processes a merge with a previous branch.  mcid gives the
574                 branch we merged. */
575
576 void MCExecution::merge(MCID mcid) {
577         EPValue * epvalue=getEPValue(mcid);
578         ExecPoint *ep=epvalue->getEP();
579         //rollback current branch
580         currbranch=EPTable->get(ep)->getBranch();
581         int orig_length=ep->getSize();
582         int curr_length=currexecpoint->getSize();
583         for(int i=0;i<curr_length-orig_length;i++)
584                 currexecpoint->pop();
585         //increment top
586         currexecpoint->incrementTop();  
587         //now we can create the merge point
588         if (DBG_ENABLED()) {
589                 model_print("MERGE mid=%u", mcid);
590                 currexecpoint->print();
591                 model_print("\n");
592         }
593         getOrCreateCurrRecord(MERGE, NULL, 0, 0, 8, false);
594         currexecpoint->incrementTop();
595 }
596
597 /** @brief Phi function. */
598 MCID MCExecution::phi(MCID input) {
599         EPRecord * record=getOrCreateCurrRecord(FUNCTION, NULL, 0, 1, 8, false);
600         record->setPhi();
601         EPValue *epinput=getEPValue(input);
602         EPValue * epvalue=getEPValue(record, NULL, NULL, epinput->getValue(), 8);
603
604         MCID mcids[]={input};
605         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
606         
607         MCID fnmcid=getNextMCID();
608         ASSERT(EPList->size()==fnmcid);
609         EPList->push_back(epvalue);
610         currexecpoint->incrementTop();
611
612         return fnmcid;
613 }
614
615 /** @brief Phi function for loops. */
616 MCID MCExecution::loop_phi(MCID input) {
617         EPRecord * record=getOrCreateCurrRecord(FUNCTION, NULL, 0, 1, 8, false);
618         record->setLoopPhi();
619         EPValue *epinput=getEPValue(input);
620         EPValue * epvalue=getEPValue(record, NULL, NULL, epinput->getValue(), 8);
621
622         MCID mcids[]={input};
623         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
624
625         uint tid=id_to_int(currexecpoint->get_tid());
626         EPRecord *exitrec=(*lastloopexit)[tid];
627
628         EPRecordIDSet *phiset=record->getPhiLoopTable();
629         struct RecordIDPair rip={exitrec,getEPRecord(input)};
630         if (!phiset->contains(&rip)) {
631                 struct RecordIDPair *p=(struct RecordIDPair *)model_malloc(sizeof(struct RecordIDPair));
632                 *p=rip;
633                 phiset->add(p);
634         }
635         
636         MCID fnmcid=getNextMCID();
637         ASSERT(EPList->size()==fnmcid);
638         EPList->push_back(epvalue);
639         currexecpoint->incrementTop();
640
641         return fnmcid;
642 }
643
644 uint64_t MCExecution::equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, MCID *retval) {
645         uint64_t eq=(val1==val2);
646         bool isNew=false;
647         int len=8;
648         EPRecord * record=getOrCreateCurrRecord(EQUALS, &isNew, 0, 2, len, false);
649         EPValue * epvalue=getEPValue(record, NULL, NULL, eq, len);
650         getEPValue(record, NULL, NULL, 1-eq, len);
651         MCID mcids[]={op1, op2};
652         recordContext(epvalue, MCID_NODEP, MCID_NODEP, 2, mcids);
653         if (isNew) {
654                 recordFunctionChange(record, 0);
655                 recordFunctionChange(record, 1);
656         }
657         MCID eqmcid=getNextMCID();
658         ASSERT(EPList->size()==eqmcid);
659         EPList->push_back(epvalue);
660         currexecpoint->incrementTop();
661         *retval=eqmcid;
662         return eq;
663 }
664
665 /** @brief Processes an uninterpretted function. */
666
667 MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint numids, MCID *mcids) {
668         bool isNew=false;
669         EPRecord * record=getOrCreateCurrRecord(FUNCTION, &isNew, 0, numids, len, false);
670         if (isNew) {
671                 if (functionidentifier == 0)
672                         record->setCompletedGoal(new CGoalSet(), false);
673                 else {
674                         if (sharedgoals->size()<=functionidentifier) {
675                                 sharedgoals->resize(functionidentifier+1);
676                                 sharedfuncrecords->resize(functionidentifier+1);
677                         }
678                         if ((*sharedgoals)[functionidentifier]==NULL) {
679                                 (*sharedgoals)[functionidentifier]=new CGoalSet();
680                                 (*sharedfuncrecords)[functionidentifier]=new RecordSet();
681                         }
682                         record->setCompletedGoal((*sharedgoals)[functionidentifier], true);
683                         (*sharedfuncrecords)[functionidentifier]->add(record);
684
685                         for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
686                                 EPRecord *input=getEPRecord(mcids[i-VC_BASEINDEX]);
687                                 IntIterator *inputit=input->getReturnValueSet()->iterator();
688                                 IntHashSet *recinputset=record->getSet(i);
689                                 while(inputit->hasNext()) {
690                                         uint64_t inputval=inputit->next();
691                                         recinputset->add(inputval);
692                                 }
693                                 delete inputit;
694                         }
695
696                         CGoalIterator *cit=(*sharedgoals)[functionidentifier]->iterator();
697                         while(cit->hasNext()) {
698                                 CGoal *goal=cit->next();
699                                 evalGoal(record, goal);
700                         }
701                         delete cit;
702                 }
703         }
704         val=val&getmask(len);
705         EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
706         recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
707         
708         uint64_t valarray[numids+VC_BASEINDEX];
709         for(uint i=0;i<VC_BASEINDEX;i++) {
710                 valarray[i]=0;
711         }
712         for(uint i=VC_BASEINDEX;i<(numids+VC_BASEINDEX);i++) {
713                 valarray[i]=getEPValue(mcids[i-VC_BASEINDEX])->getValue();
714         }
715
716         MCID fnmcid=getNextMCID();
717         ASSERT(EPList->size()==fnmcid);
718         EPList->push_back(epvalue);
719         currexecpoint->incrementTop();
720
721         CGoal *goal=new CGoal(numids+VC_BASEINDEX, valarray);
722         if (record->completedGoalSet()->contains(goal)) {
723                 delete goal;
724         } else {
725                 scheduler->setNewFlag();
726                 planner->getConstGen()->achievedGoal(record);
727 #ifdef PRINT_ACHIEVED_GOALS
728                 model_print("Achieved goal:");goal->print();model_print("\n");
729 #endif
730 #ifdef STATS
731                 planner->getConstGen()->curr_stat->fgoals++;
732 #endif
733                 goal->setOutput(val);
734                 record->completedGoalSet()->add(goal);
735                 recordFunctionChange(record, val);
736                 if (functionidentifier != 0) {
737                         RecordIterator *rit=(*sharedfuncrecords)[functionidentifier]->iterator();
738                         while(rit->hasNext()) {
739                                 EPRecord *func=rit->next();
740                                 if (func == record)
741                                         continue;
742                                 evalGoal(func, goal);
743                         }
744                         delete rit;
745                 }
746         }
747         
748         return fnmcid;
749 }
750
751 void MCExecution::evalGoal(EPRecord *record, CGoal *goal) {
752         for(uint i=VC_BASEINDEX;i<goal->getNum();i++) {
753                 uint64_t input=goal->getValue(i);
754                 if (!record->getSet(i)->contains(input))
755                         return;
756         }
757         //Have all input, propagate output
758         recordFunctionChange(record, goal->getOutput());
759 }
760
761 /** @brief Returns the next thread id. */
762
763 thread_id_t MCExecution::get_next_tid() {
764         return int_to_id(snap_fields->next_thread_id++);
765 }
766
767 /** @brief Registers a new thread */
768
769 void MCExecution::add_thread(Thread *t) {
770         ThreadList->push_back(t);
771         ExecPoint * ep=new ExecPoint(4, t->get_id());
772         ep->push(EP_COUNTER,0);
773         ExecPointList->push_back(ep);
774         CurrBranchList->push_back(NULL);
775 #ifdef TSO
776         storebuffer->push_back(new SnapList<EPValue *>());
777 #endif
778 }
779
780 /** @brief Records currently executing thread. */
781
782 void MCExecution::set_current_thread(Thread *t) {
783         if (curr_thread) {
784                 uint oldtid=id_to_int(curr_thread->get_id());
785                 (*CurrBranchList)[oldtid]=currbranch;
786         }
787         curr_thread=t;
788         currexecpoint=(t==NULL)?NULL:(*ExecPointList)[id_to_int(t->get_id())];
789         currbranch=(t==NULL)?NULL:(*CurrBranchList)[id_to_int(t->get_id())];
790 }
791
792 void MCExecution::threadStart(EPRecord *parent) {
793         EPRecord *threadstart=getOrCreateCurrRecord(THREADBEGIN, NULL, 0, 0, 8, false);
794         if (parent!=NULL) {
795                 parent->setChildRecord(threadstart);
796         }
797         currexecpoint->incrementTop();
798 }
799
800 /** @brief Create a new thread. */
801
802 void MCExecution::threadCreate(thrd_t *t, thrd_start_t start, void *arg) {
803         EPRecord *threadstart=getOrCreateCurrRecord(THREADCREATE, NULL, 0, 0, 8, false);
804         currexecpoint->incrementTop();
805         Thread *th = new Thread(get_next_tid(), t, start, arg, curr_thread, threadstart);
806         add_thread(th);
807 }
808
809 /** @brief Joins with a thread. */
810
811 void MCExecution::threadJoin(Thread *blocking) {
812         while(true) {
813                 if (blocking->is_complete()) {
814                         EPRecord *join=getOrCreateCurrRecord(THREADJOIN, NULL, 0, 0, 8, false);
815                         currexecpoint->incrementTop();
816                         join->setJoinThread(blocking->get_id());
817                         return;
818                 }
819                 get_current_thread()->set_waiting(blocking);
820                 scheduler->check_preempt();
821                 get_current_thread()->set_waiting(NULL);
822         }
823 }
824
825 /** @brief Finishes a thread. */
826
827 void MCExecution::threadFinish() {
828         Thread *th = get_current_thread();
829         /* Wake up any joining threads */
830         for (unsigned int i = 0; i < get_num_threads(); i++) {
831                 Thread *waiting = get_thread(int_to_id(i));
832                 if (waiting->waiting_on() == th) {
833                         waiting->set_waiting(NULL);
834                 }
835         }
836         th->complete();
837         scheduler->check_preempt();
838 }
839
840 /** @brief Thread yield. */
841
842 void MCExecution::threadYield() {
843         getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
844         currexecpoint->incrementTop();
845 }
846
847 /** @brief Thread yield. */
848
849 void * MCExecution::alloc(size_t size) {
850         bool isNew;
851         EPRecord *record=getOrCreateCurrRecord(ALLOC, &isNew, 0, 0, 8, false);
852         currexecpoint->incrementTop();
853         if (isNew) {
854                 size_t allocsize=((size<<1)+7)&~((size_t)(7));
855                 record->setSize(allocsize);
856                 void *ptr=real_user_malloc(size);
857                 record->setPtr(ptr);
858                 return ptr;
859         } else {
860                 if (size>record->getSize()) {
861                         model_print("Allocation size changed too much\n");
862                         exit(-1);
863                 }
864                 void *ptr=record->getPtr();
865                 return ptr;
866         }
867 }
868
869 /** @brief Record enter loop. */
870
871 void MCExecution::enterLoop() {
872         EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
873         
874         //push the loop iteration counter
875         currexecpoint->push(EP_LOOP,0);
876         //push the curr iteration statement counter
877         currexecpoint->push(EP_COUNTER,0);
878         EPRecord * lpstartrecord=getOrCreateCurrRecord(LOOPSTART, NULL, 0, 0, 8, false);
879         record->setChildRecord(lpstartrecord);
880         
881         currexecpoint->incrementTop();
882         if (DBG_ENABLED()) {
883                 model_print("ENLOOP ");
884                 currexecpoint->print();
885                 model_print("\n");
886         }
887 }
888
889 /** @brief Record exit loop. */
890
891 void MCExecution::exitLoop() {
892         ExecPointType type;
893         EPRecord *breakstate=NULL;
894
895         /* Record last statement */
896         uint tid=id_to_int(currexecpoint->get_tid());
897         
898         if (!currexecpoint->directInLoop()) {
899                 breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
900                 currexecpoint->incrementTop();
901         } else {
902                 breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
903                 currexecpoint->incrementTop();
904         }
905         
906         /* Get Last Record */
907         EPRecord *lastrecord=(currbranch==NULL)?(*alwaysexecuted)[tid]:currbranch->lastrecord;
908         
909         /* Remember last record as loop exit for this execution.  */
910         if (lastloopexit->size()<=tid) {
911                 lastloopexit->resize(tid+1);
912         }
913         (*lastloopexit)[tid]=lastrecord;
914
915         do {
916                 type=currexecpoint->getType();
917                 currexecpoint->pop();
918                 if (type==EP_BRANCH) {
919                         //we crossed a branch, fix currbranch
920                         EPRecord *branch=currbranch->getRecord();
921                         currbranch=branch->getBranch();
922                 }
923         } while(type!=EP_LOOP);
924
925         if (DBG_ENABLED()) {
926                 model_print("EXLOOP ");
927                 currexecpoint->print();
928                 model_print("\n");
929         }
930         EPRecord *loopenter=EPTable->get(currexecpoint);
931         currexecpoint->incrementTop();
932         EPRecord *labelrec=getOrCreateCurrRecord(LABEL, NULL, 0, 0, 8, false);
933         if (loopenter->getNextRecord()==NULL) {
934                 loopenter->setNextRecord(labelrec);
935         }
936         breakstate->setNextRecord(labelrec);
937         currexecpoint->incrementTop();
938 }
939
940 /** @brief Record next loop iteration. */
941 void MCExecution::loopIterate() {
942         currexecpoint->pop();
943         //increment the iteration counter
944         currexecpoint->incrementTop();
945         currexecpoint->push(EP_COUNTER,0);
946 }
947
948 /** @brief Helper function to add new item to a StoreLoadHashTable */
949
950 void addTable(StoreLoadHashTable *table, const void *addr, EPRecord *record) {
951         RecordSet * rset=table->get(addr);
952         if (rset==NULL) {
953                 rset=new RecordSet();
954                 table->put(addr, rset);
955         }
956         rset->add(record);
957 }
958
959 /** @brief Update mapping from address to stores to that address. */
960
961 void MCExecution::addStoreTable(const void *addr, EPRecord *record) {
962         addTable(storetable, addr, record);
963 }
964
965 /** @brief Update mapping from address to loads from that address. */
966
967 void MCExecution::addLoadTable(const void *addr, EPRecord *record) {
968         addTable(loadtable, addr, record);
969 }
970
971 /** @brief Update mapping from address to loads from that address. */
972
973 RecordSet * MCExecution::getLoadTable(const void *addr) {
974         return loadtable->get(addr);
975 }
976
977 /** @brief Update mapping from address to stores to that address. */
978
979 RecordSet * MCExecution::getStoreTable(const void *addr) {
980         return storetable->get(addr);
981 }
982
983 /** @brief Registers that component index of deprecord depends on record. */
984
985 void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsigned int index) {
986         EPRecordSet *set=eprecorddep->get(record);
987         if (set==NULL) {
988                 set=new EPRecordSet();
989                 eprecorddep->put(record, set);
990         }
991         struct RecordIntPair pair={deprecord, index};
992
993         if (!set->contains(&pair)) {
994                 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));             
995                 *p=pair;
996                 set->add(p);
997         }
998
999         if (!revrecorddep->contains(&pair)) {
1000                 struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));             
1001                 *p=pair;
1002                 revrecorddep->put(p, new ModelVector<EPRecord *>());
1003         }
1004         
1005         ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
1006         for(uint i=0;i<recvec->size();i++) {
1007                 if ((*recvec)[i]==record)
1008                         return;
1009         }
1010         recvec->push_back(record);
1011 }
1012
1013 ModelVector<EPRecord *> * MCExecution::getRevDependences(EPRecord *record, uint index) {
1014         struct RecordIntPair pair={record, index};
1015         return revrecorddep->get(&pair);
1016 }