1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
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.
13 #include "constraint.h"
14 #include "storeloadset.h"
16 #include "execpoint.h"
18 LoadRF::LoadRF(EPRecord *_load, ConstGen *cg) : load(_load) {
19 RecordSet *mrfSet=cg->getMayReadFromSet(load);
20 uint numstores=mrfSet->getSize();
21 numvars=NUMBITS(numstores-1);
22 vars=(Constraint **)model_malloc(numvars*sizeof(Constraint *));
23 cg->getArrayNewVars(numvars, vars);
30 void LoadRF::genConstraints(ConstGen *cg) {
32 RecordSet *mrfSet=cg->getMayReadFromSet(load);
33 StoreLoadSet * sls=cg->getStoreLoadSet(load);
34 uint numvalvars=sls->getNumValVars();
35 uint numaddrvars=sls->getNumAddrVars();
36 Constraint ** loadvalvars=(load->getType()==RMW)?sls->getRMWRValVars(cg, load):sls->getValVars(cg, load);
37 Constraint ** loadaddrvars=sls->getAddrVars(cg, load);
39 RecordIterator *sri=mrfSet->iterator();
40 while(sri->hasNext()) {
41 EPRecord *store=sri->next();
42 Constraint ** storevalvars=sls->getValVars(cg, store);
45 Constraint *rfconst=(numvars==0)?&ctrue:generateConstraint(numvars, vars, storeindex);
46 //if we read from a store, it should happen before us
48 Constraint *storebeforeload;
49 if (store->getEP()->get_tid()==load->getEP()->get_tid()) {
50 if (store->getEP()->compare(load->getEP())==CR_AFTER) {
51 storebeforeload=&ctrue;
53 storebeforeload=&cfalse;
55 storebeforeload=cg->getOrderConstraint(store, load);
57 Constraint * storebeforeload=cg->getOrderConstraint(store, load);
59 //if we read from a store, we should have the same value
60 Constraint *storevalmatch=generateEquivConstraint(numvalvars, loadvalvars, storevalvars);
61 //if we read from a store, it must have been executed
62 Constraint *storeexecuted=cg->getExecutionConstraint(store);
66 //if we read from a store, we should have the same address
67 Constraint ** storeaddrvars=sls->getAddrVars(cg, store);
68 Constraint * storeaddressmatch=generateEquivConstraint(numaddrvars, loadaddrvars, storeaddrvars);
69 Constraint *array[] = {storebeforeload, storevalmatch, storeexecuted, storeaddressmatch};
72 ADDCONSTRAINT2(cg, new Constraint(IMPLIES, rfconst, new Constraint(AND, 4, array)), "storeaddressmatch");
75 //Also need to make sure that we don't have conflicting stores
76 //ordered between the load and store
78 RecordSet *conflictSet=cg->computeConflictSet(store, load, mrfSet);
79 RecordIterator *sit=conflictSet!=NULL?conflictSet->iterator():mrfSet->iterator();
81 while(sit->hasNext()) {
82 EPRecord *conflictstore=sit->next();
83 Constraint ** confstoreaddrvars=sls->getAddrVars(cg, conflictstore);
84 Constraint * storebeforeconflict=cg->getOrderConstraint(store, conflictstore);
85 if (storebeforeconflict->isFalse())
87 Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
88 if (conflictbeforeload->isFalse()) {
89 storebeforeconflict->freerec();
93 rfconst=generateConstraint(numvars, vars, storeindex);
94 Constraint *array[]={storebeforeconflict,
97 cg->getExecutionConstraint(conflictstore)};
98 Constraint *confstore=new Constraint(IMPLIES,
99 new Constraint(AND, 4, array),
100 generateEquivConstraint(numaddrvars, loadaddrvars, confstoreaddrvars)->negate());
102 ADDCONSTRAINT2(cg, confstore, "confstore");
105 if (conflictSet != NULL)
112 Constraint *mustrf=generateLTConstraint(cg, numvars, vars, storeindex);
113 Constraint *validrf=new Constraint(IMPLIES, cg->getExecutionConstraint(load), mustrf);
114 ADDCONSTRAINT2(cg, validrf, "validrf");