3 #include "processconcrete.h"
4 #include "processabstract.h"
12 #include "bitreader.h"
13 #include "bitwriter.h"
17 static int concretecheck=0;
18 static int concretetrigger=0;
20 processconcrete::processconcrete(model *m) {
22 bw=new bitwriter(globalmodel,m->gethashtable());
23 br=new bitreader(globalmodel,m->gethashtable());
26 void processconcrete::printstats() {
27 printf("Concretization Rules Checked: %d Triggered: %d\n",concretecheck,concretetrigger);
31 void processconcrete::processrule(Rule *r) {
32 State *st=new State(r,globalmodel->gethashtable());
33 if (st->initializestate(this, globalmodel)) {
36 if (evaluatestatementa(r->getstatementa(),st->env)) {
38 satisfystatementb((CStatementb *)r->getstatementb(),st->env);
41 if (!st->increment(this, globalmodel))
48 processconcrete::~processconcrete() {
52 bool processconcrete::evaluatestatementa(Statementa *sa, Hashtable *env) {
53 switch(sa->gettype()) {
55 return evaluatestatementa(sa->getleft(),env)||evaluatestatementa(sa->getright(),env);
57 return evaluatestatementa(sa->getleft(),env)&&evaluatestatementa(sa->getright(),env);
59 return !evaluatestatementa(sa->getleft(),env);
60 case STATEMENTA_EQUALS: {
61 Element *left=evaluateexpr((CAElementexpr *)sa->getleftee(),env);
62 Element *right=evaluateexpr((CAElementexpr *)sa->getrightee(),env);
63 bool tvalue=left->equals(right);
69 Element *left=evaluateexpr((CAElementexpr *)sa->getleftee(),env);
70 Element *right=evaluateexpr((CAElementexpr *)sa->getrightee(),env);
71 if (!left->isnumber()||
73 printf("Bad lt compare\n");
76 bool tvalue=left->intvalue()<right->intvalue();
86 void processconcrete::satisfystatementb(CStatementb *sb, Hashtable *env) {
87 Element * rvalue=evaluateexpr((CAElementexpr *)sb->getright(),env);
89 if (sb->gettype()==CSTATEMENTB_ARRAYASSIGN)
90 index=evaluateexpr((CAElementexpr *)sb->getleft(),env);
91 Field *field=sb->getfield();
92 Element *src=evaluateexpr(sb->getexpr(),env);
93 bw->writefieldorarray(src,field,index,rvalue);
100 Element * processconcrete::evaluateexpr(Expr *e, Hashtable *env) {
101 switch(e->gettype()) {
103 return new Element((Element *)env->get(e->getlabel()->label()));
105 Element *old=evaluateexpr(e->getexpr(),env);
106 Element *newe=br->readfieldorarray(evaluateexpr(e->getexpr(),env),e->getfield(),NULL);
111 Element *old=evaluateexpr(e->getexpr(),env);
112 char *type=e->getcasttype();
113 structure *st=globalmodel->getstructure(type);
114 Element *newe=new Element(old->getobject(),st);
119 Element *old=evaluateexpr(e->getexpr(),env);
120 Element *index=evaluateexpr(e->getindex(),env);
121 Element *newe=br->readfieldorarray(evaluateexpr(e->getexpr(),env),e->getfield(),index);
129 Element * processconcrete::evaluateexpr(CAElementexpr *ee, Hashtable *env) {
130 switch(ee->gettype()) {
131 case CAELEMENTEXPR_LABEL:
133 return new Element((Element *)env->get(ee->getlabel()->label()));
135 case CAELEMENTEXPR_NULL:
137 return new Element();
139 case CAELEMENTEXPR_SUB:
141 CAElementexpr *left=ee->getleft();
142 CAElementexpr *right=ee->getright();
143 Element *leftval=evaluateexpr(left,env);
144 Element *rightval=evaluateexpr(right,env);
145 Element *diff=new Element(leftval->intvalue()-rightval->intvalue());
146 delete(leftval);delete(rightval);
149 case CAELEMENTEXPR_ADD:
151 CAElementexpr *left=ee->getleft();
152 CAElementexpr *right=ee->getright();
153 Element *leftval=evaluateexpr(left,env);
154 Element *rightval=evaluateexpr(right,env);
155 Element *sum=new Element(leftval->intvalue()+rightval->intvalue());
156 delete(leftval);delete(rightval);
159 case CAELEMENTEXPR_MULT:
161 CAElementexpr *left=ee->getleft();
162 CAElementexpr *right=ee->getright();
163 Element *leftval=evaluateexpr(left,env);
164 Element *rightval=evaluateexpr(right,env);
165 Element *diff=new Element(leftval->intvalue()*rightval->intvalue());
166 delete(leftval);delete(rightval);
169 case CAELEMENTEXPR_DIV:
171 CAElementexpr *left=ee->getleft();
172 CAElementexpr *right=ee->getright();
173 Element *leftval=evaluateexpr(left,env);
174 Element *rightval=evaluateexpr(right,env);
175 Element *diff=new Element(leftval->intvalue()/rightval->intvalue());
176 delete(leftval);delete(rightval);
179 case CAELEMENTEXPR_LIT:
181 Literal *l=ee->getliteral();
182 switch(l->gettype()) {
184 return new Element(l->number());
186 return new Element(copystr(l->token()));
188 return new Element(l->getbool());
190 printf("ERROR with lit type\n");
194 case CAELEMENTEXPR_SIZEOF:
196 Setexpr * setexpr=ee->getsetexpr();
197 switch(setexpr->gettype()) {
199 return new Element(globalmodel->getdomainrelation()->getset(setexpr->getsetlabel()->getname())->getset()->size());
201 Element *key=(Element *)env->get(setexpr->getlabel()->label());
202 WorkSet *ws=globalmodel->getdomainrelation()->getrelation(setexpr->getrelation()->getname())->getrelation()->getset(key);
204 return new Element(0);
206 return new Element(ws->size());
208 case SETEXPR_INVREL: {
209 Element *key=(Element *)env->get(setexpr->getlabel()->label());
210 WorkSet *ws=globalmodel->getdomainrelation()->getrelation(setexpr->getrelation()->getname())->getrelation()->invgetset(key);
212 return new Element(0);
214 return new Element(ws->size());
218 case CAELEMENTEXPR_ELEMENT: {
219 Element *index=evaluateexpr(ee->getleft(),env);
220 int ind=index->intvalue();
223 Setexpr * setexpr=ee->getsetexpr();
224 switch(setexpr->gettype()) {
226 return new Element((Element *)globalmodel->getdomainrelation()->getset(setexpr->getsetlabel()->getname())->getset()->getelement(ind));
228 Element *key=(Element *)env->get(setexpr->getlabel()->label());
229 return new Element((Element *)globalmodel->getdomainrelation()->getrelation(setexpr->getrelation()->getname())->getrelation()->getset(key)->getelement(ind));
231 case SETEXPR_INVREL: {
232 Element *key=(Element *)env->get(setexpr->getlabel()->label());
233 return new Element((Element *)globalmodel->getdomainrelation()->getrelation(setexpr->getrelation()->getname())->getrelation()->invgetset(key)->getelement(ind));
237 case CAELEMENTEXPR_RELATION:
239 Element *e=evaluateexpr(ee->getleft(),env);
240 Element *r=(Element *)globalmodel->getdomainrelation()->getrelation(ee->getrelation()->getname())->getrelation()->getobj(e);
241 return new Element(r);