]>
Commit | Line | Data |
---|---|---|
3aaedf88 | 1 | /* |
2 | ** forjunk.c | |
3 | */ | |
4 | ||
5 | //#define DEBUGPRINT 1 | |
6 | ||
7 | # include <ctype.h> /* for isdigit */ | |
8 | # include "lclintMacros.nf" | |
9 | # include "basic.h" | |
10 | # include "cgrammar.h" | |
11 | # include "cgrammar_tokens.h" | |
12 | ||
13 | # include "exprChecks.h" | |
3aaedf88 | 14 | # include "exprNodeSList.h" |
15 | ||
3aaedf88 | 16 | # include "exprDataQuite.i" |
17 | ||
84c9ffbf | 18 | /*@access constraint, exprNode @*/ |
19 | ||
20 | /*@access constraintExpr @*/ | |
21 | ||
bb25bea6 | 22 | static bool isInc (/*@observer@*/ constraintExpr c) /*@*/ |
84c9ffbf | 23 | { |
24 | ||
25 | llassert(constraintExpr_isDefined(c) ); | |
26 | if (c->kind == binaryexpr ) | |
27 | { | |
28 | constraintExprBinaryOpKind binOP; | |
29 | constraintExpr t1, t2; | |
30 | t1 = constraintExprData_binaryExprGetExpr1 (c->data); | |
31 | t2 = constraintExprData_binaryExprGetExpr2 (c->data); | |
32 | ||
33 | binOP = constraintExprData_binaryExprGetOp (c->data); | |
34 | if (binOP == PLUS) | |
35 | if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 ) | |
36 | { | |
37 | return TRUE; | |
38 | } | |
39 | } | |
40 | ||
41 | return FALSE; | |
42 | } | |
43 | ||
44 | ||
3aaedf88 | 45 | |
46 | // look for constraints like cexrp = cexrp + 1 | |
84c9ffbf | 47 | static bool incVar (/*@notnull@*/ constraint c) /*@*/ |
3aaedf88 | 48 | { |
49 | constraintExpr t1; | |
50 | if (c->ar != EQ) | |
51 | { | |
52 | return FALSE; | |
53 | } | |
54 | if (! isInc (c->expr ) ) | |
55 | return FALSE; | |
56 | ||
84c9ffbf | 57 | llassert (constraintExpr_isDefined(c->expr) ); |
3aaedf88 | 58 | llassert (c->expr->kind == binaryexpr); |
84c9ffbf | 59 | |
3aaedf88 | 60 | t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data); |
61 | if (constraintExpr_similar (c->lexpr, t1) ) | |
62 | return TRUE; | |
63 | ||
64 | return FALSE; | |
65 | } | |
84c9ffbf | 66 | /*@noaccess constraintExpr @*/ |
3aaedf88 | 67 | |
68 | ||
bb25bea6 | 69 | static bool increments (/*@observer@*/ constraint c, |
70 | /*@observer@*/ constraintExpr var) | |
3aaedf88 | 71 | { |
84c9ffbf | 72 | llassert(constraint_isDefined(c) ); |
73 | ||
74 | if (constraint_isUndefined(c) ) | |
75 | { | |
76 | return FALSE; | |
77 | } | |
78 | ||
3aaedf88 | 79 | llassert (incVar (c)); |
80 | if (constraintExpr_similar (c->lexpr, var) ) | |
81 | return TRUE; | |
82 | else | |
83 | return FALSE; | |
84 | } | |
85 | ||
84c9ffbf | 86 | static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody) |
3aaedf88 | 87 | { |
88 | ||
89 | exprNode init, test, inc, t1, t2; | |
90 | lltok tok; | |
91 | ||
84c9ffbf | 92 | llassert(exprNode_isDefined (forPred) ); |
93 | llassert(exprNode_isDefined (forBody) ); | |
94 | ||
3aaedf88 | 95 | init = exprData_getTripleInit (forPred->edata); |
96 | test = exprData_getTripleTest (forPred->edata); | |
97 | inc = exprData_getTripleInc (forPred->edata); | |
98 | ||
84c9ffbf | 99 | llassert(exprNode_isDefined(test) ); |
100 | ||
101 | if (exprNode_isUndefined(test) ) | |
102 | { | |
103 | return FALSE; | |
104 | } | |
105 | ||
106 | llassert(exprNode_isDefined(inc) ); | |
107 | ||
108 | if (exprNode_isUndefined(inc) ) | |
109 | { | |
110 | return FALSE; | |
111 | } | |
112 | ||
3aaedf88 | 113 | if (test->kind != XPR_PREOP) |
114 | return FALSE; | |
115 | ||
116 | tok = (exprData_getUopTok (test->edata)); | |
117 | if (!lltok_isMult (tok) ) | |
118 | { | |
119 | return FALSE; | |
120 | } | |
121 | ||
122 | //should check preop too | |
123 | if (inc->kind != XPR_POSTOP) | |
124 | { | |
125 | return FALSE; | |
126 | } | |
127 | ||
128 | tok = (exprData_getUopTok (inc->edata)); | |
129 | if (lltok_isInc_Op (tok) ) | |
130 | { | |
131 | t1 = exprData_getUopNode (test->edata); | |
132 | t2 = exprData_getUopNode (inc->edata); | |
84c9ffbf | 133 | llassert(exprNode_isDefined(t2) && exprNode_isDefined(t2) ); |
134 | ||
135 | if (exprNode_isUndefined(t1) || exprNode_isUndefined(t2) ) | |
136 | { | |
137 | return FALSE; | |
138 | } | |
139 | ||
3aaedf88 | 140 | if (sRef_sameName (t1->sref, t2->sref) ) |
141 | { | |
142 | return TRUE; | |
143 | } | |
144 | } | |
145 | return FALSE; | |
146 | } | |
147 | ||
bb25bea6 | 148 | static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c) |
3aaedf88 | 149 | { |
150 | constraintList ret; | |
151 | ||
c3e695ff | 152 | ret = constraintList_makeNew(); |
3aaedf88 | 153 | constraintList_elements (c, el) |
154 | { | |
84c9ffbf | 155 | llassert(constraint_isDefined(el)); |
156 | if ( constraint_isUndefined(el) ) | |
157 | continue; | |
158 | ||
3aaedf88 | 159 | if (el->ar == LT || el->ar == LTE) |
160 | { | |
d46ce6a4 | 161 | constraint temp; |
162 | temp = constraint_copy(el); | |
163 | ||
164 | ret = constraintList_add (ret, temp); | |
3aaedf88 | 165 | } |
166 | } | |
167 | end_constraintList_elements; | |
168 | ||
169 | return ret; | |
170 | } | |
171 | ||
bb25bea6 | 172 | static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c) |
3aaedf88 | 173 | { |
174 | constraintList ret; | |
175 | ||
c3e695ff | 176 | ret = constraintList_makeNew(); |
3aaedf88 | 177 | constraintList_elements (c, el) |
178 | { | |
60eced23 | 179 | llassert (constraint_isDefined (el)); |
180 | ||
3aaedf88 | 181 | if (incVar (el) ) |
182 | { | |
d46ce6a4 | 183 | constraint temp; |
184 | temp = constraint_copy(el); | |
185 | ret = constraintList_add (ret, temp); | |
3aaedf88 | 186 | } |
187 | } | |
188 | end_constraintList_elements; | |
189 | ||
190 | return ret; | |
191 | } | |
192 | ||
bb25bea6 | 193 | static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody) |
3aaedf88 | 194 | { |
195 | ||
196 | exprNode init, test, inc, t1, t2; | |
197 | constraintList ltCon; | |
198 | constraintList incCon; | |
bb25bea6 | 199 | constraintExpr ret; |
3aaedf88 | 200 | |
201 | lltok tok; | |
202 | ||
203 | init = exprData_getTripleInit (forPred->edata); | |
204 | test = exprData_getTripleTest (forPred->edata); | |
205 | inc = exprData_getTripleInc (forPred->edata); | |
206 | ||
84c9ffbf | 207 | llassert(exprNode_isDefined(test) ); |
208 | llassert(exprNode_isDefined(inc) ); | |
3aaedf88 | 209 | |
210 | ltCon = getLessThanConstraints (test->trueEnsuresConstraints); | |
211 | incCon = getIncConstraints (inc->ensuresConstraints); | |
212 | ||
213 | DPRINTF(( message ("getForTimes: ltCon: %s from %s", constraintList_print(ltCon), constraintList_print(test->trueEnsuresConstraints) ) )); | |
214 | ||
215 | DPRINTF(( message ("getForTimes: incCon: %s from %s", constraintList_print(incCon), constraintList_print(inc->ensuresConstraints) ) )); | |
216 | ||
217 | constraintList_elements (ltCon, el) | |
218 | { | |
dc92450f | 219 | constraintList_elements(incCon, el2) |
3aaedf88 | 220 | { |
221 | if ( increments(el2, el->lexpr) ) | |
222 | { | |
223 | DPRINTF(( message ("getForTimes: %s increments %s", constraint_print(el2), constraint_print(el) ) )); | |
bb25bea6 | 224 | ret = constraintExpr_copy (el->expr); |
225 | constraintList_free(ltCon); | |
226 | constraintList_free(incCon); | |
227 | return ret; | |
3aaedf88 | 228 | |
229 | } | |
230 | else | |
231 | DPRINTF(( message ("getForTimes: %s doesn't increment %s", constraint_print(el2), constraint_print(el) ) )); | |
232 | } | |
233 | end_constraintList_elements; | |
234 | } | |
235 | ||
236 | end_constraintList_elements; | |
bb25bea6 | 237 | |
238 | constraintList_free(ltCon); | |
239 | constraintList_free(incCon); | |
3aaedf88 | 240 | |
241 | DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse(forPred), exprNode_unparse(forBody) ) )); | |
242 | if (! canGetForTimes (forPred, forBody) ) | |
243 | { | |
244 | return NULL; | |
245 | } | |
246 | ||
247 | ||
248 | if (test->kind != XPR_PREOP) | |
249 | llassert (FALSE); | |
250 | ||
251 | tok = (exprData_getUopTok (test->edata)); | |
252 | if (!lltok_isMult (tok) ) | |
253 | { | |
254 | llassert ( FALSE ); | |
255 | } | |
256 | ||
257 | //should check preop too | |
258 | if (inc->kind != XPR_POSTOP) | |
259 | { | |
260 | llassert (FALSE ); | |
261 | } | |
262 | ||
263 | tok = (exprData_getUopTok (inc->edata)); | |
264 | if (lltok_isInc_Op (tok) ) | |
265 | { | |
266 | t1 = exprData_getUopNode (test->edata); | |
267 | t2 = exprData_getUopNode (inc->edata); | |
268 | if (sRef_sameName (t1->sref, t2->sref) ) | |
269 | { | |
270 | return (constraintExpr_makeMaxSetExpr (t1) ); | |
271 | } | |
272 | } | |
273 | llassert( FALSE); | |
274 | BADEXIT; | |
275 | } | |
276 | ||
84c9ffbf | 277 | /*@access constraintExpr @*/ |
3aaedf88 | 278 | |
bb25bea6 | 279 | static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) |
3aaedf88 | 280 | { |
281 | constraintExprKind kind; | |
282 | constraintExpr temp; | |
283 | ||
284 | DPRINTF(( message ("Doing constraintExpr_searchAndAdd %s %s %s ", | |
285 | constraintExpr_unparse(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) ); | |
286 | ||
287 | if ( constraintExpr_similar (c, find) ) | |
288 | { | |
3aaedf88 | 289 | |
28bf4b0b | 290 | constraintExpr newExpr; |
bb25bea6 | 291 | |
292 | cstring cPrint; | |
293 | ||
294 | cPrint = constraintExpr_unparse(c); | |
295 | ||
296 | ||
28bf4b0b | 297 | newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy(add) ); |
3aaedf88 | 298 | |
bb25bea6 | 299 | DPRINTF((message ("Replacing %q with %q", |
28bf4b0b | 300 | cPrint, constraintExpr_unparse(newExpr) |
3aaedf88 | 301 | ))); |
28bf4b0b | 302 | return newExpr; |
3aaedf88 | 303 | } |
304 | ||
305 | kind = c->kind; | |
306 | ||
307 | switch (kind) | |
308 | { | |
309 | case term: | |
310 | break; | |
311 | case unaryExpr: | |
312 | temp = constraintExprData_unaryExprGetExpr (c->data); | |
bb25bea6 | 313 | temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add); |
3aaedf88 | 314 | c->data = constraintExprData_unaryExprSetExpr (c->data, temp); |
315 | break; | |
316 | case binaryexpr: | |
317 | ||
318 | temp = constraintExprData_binaryExprGetExpr1 (c->data); | |
bb25bea6 | 319 | temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add); |
3aaedf88 | 320 | c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp); |
321 | ||
322 | temp = constraintExprData_binaryExprGetExpr2 (c->data); | |
bb25bea6 | 323 | temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add); |
3aaedf88 | 324 | c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp); |
325 | break; | |
326 | default: | |
327 | llassert(FALSE); | |
328 | } | |
329 | return c; | |
330 | ||
331 | } | |
332 | ||
84c9ffbf | 333 | /*@noaccess constraintExpr @*/ |
334 | ||
bb25bea6 | 335 | static constraint constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) |
3aaedf88 | 336 | { |
337 | ||
338 | llassert (constraint_search (c, find) ); | |
339 | DPRINTF(( message ("Doing constraint_searchAndAdd %s %s %s ", | |
340 | constraint_print(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) ); | |
341 | ||
342 | c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add); | |
343 | c->expr = constraintExpr_searchAndAdd (c->expr, find, add); | |
344 | ||
345 | c = constraint_simplify (c); | |
346 | c = constraint_simplify (c); | |
347 | ||
348 | return c; | |
349 | ||
350 | } | |
351 | ||
28bf4b0b | 352 | static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list, |
bb25bea6 | 353 | /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) |
3aaedf88 | 354 | { |
355 | constraintList newConstraints; | |
356 | constraintList ret; | |
357 | ||
c3e695ff | 358 | newConstraints = constraintList_makeNew(); |
3aaedf88 | 359 | |
360 | constraintList_elements (list, el) | |
361 | { | |
362 | if (constraint_search (el, find) ) | |
363 | { | |
28bf4b0b | 364 | constraint newExpr; |
365 | newExpr = constraint_copy (el); | |
3aaedf88 | 366 | |
28bf4b0b | 367 | newExpr = constraint_searchAndAdd (newExpr, find, add); |
368 | DPRINTF (( (message ("Adding constraint %s ", constraint_print (newExpr)) ) )); | |
369 | newConstraints = constraintList_add (newConstraints, newExpr); | |
3aaedf88 | 370 | } |
371 | ||
372 | } | |
373 | end_constraintList_elements; | |
374 | ||
4ab867d6 | 375 | ret = constraintList_addListFree (list, newConstraints); |
3aaedf88 | 376 | return ret; |
377 | } | |
378 | ||
bb25bea6 | 379 | static void doAdjust(/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations) |
3aaedf88 | 380 | { |
381 | ||
382 | constraintList_elements (forBody->ensuresConstraints, el) | |
383 | { | |
84c9ffbf | 384 | // look for var = var + 1 |
3aaedf88 | 385 | if (incVar(el) ) |
386 | { | |
387 | DPRINTF((message ("Found inc variable constraint : %s", constraint_print (el) ) )); | |
388 | forBody->requiresConstraints = constraintList_searchAndAdd(forBody->requiresConstraints, el->lexpr, iterations); | |
389 | } | |
390 | } | |
391 | end_constraintList_elements; | |
392 | } | |
393 | ||
28bf4b0b | 394 | void exprNode_forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody) |
3aaedf88 | 395 | { |
84c9ffbf | 396 | exprNode init, test, inc; |
397 | ||
3aaedf88 | 398 | constraintExpr iterations; |
399 | ||
400 | init = exprData_getTripleInit (forPred->edata); | |
401 | test = exprData_getTripleTest (forPred->edata); | |
402 | inc = exprData_getTripleInc (forPred->edata); | |
403 | ||
404 | if (exprNode_isError (test) || exprNode_isError (inc) ) | |
405 | return; | |
406 | ||
407 | iterations = getForTimes (forPred, forBody ); | |
408 | ||
28bf4b0b | 409 | if (constraintExpr_isDefined (iterations) ) |
3aaedf88 | 410 | { |
411 | doAdjust ( e, forPred, forBody, iterations); | |
bb25bea6 | 412 | constraintExpr_free(iterations); |
3aaedf88 | 413 | } |
3aaedf88 | 414 | } |
415 | ||
416 | ||
417 | /* else */ | |
418 | /* { */ | |
419 | /* DPRINTF (("Can't get for time ")); */ | |
420 | /* } */ | |
421 | ||
422 | /* if (exprNode_isError(init) ) */ | |
423 | /* { */ | |
424 | /* return; */ | |
425 | /* } */ | |
426 | ||
427 | /* if (init->kind == XPR_ASSIGN) */ | |
428 | /* { */ | |
429 | /* t1 = exprData_getOpA (init->edata); */ | |
430 | /* t2 = exprData_getOpB (init->edata); */ | |
431 | ||
432 | /* if (! (t1->kind == XPR_VAR) ) */ | |
433 | /* return; */ | |
434 | /* } */ | |
435 | /* else */ | |
436 | /* return; */ | |
437 | ||
438 | /* if (test->kind == XPR_FETCH) */ | |
439 | /* { */ | |
440 | /* t3 = exprData_getPairA (test->edata); */ | |
441 | /* t4 = exprData_getPairB (test->edata); */ | |
442 | ||
443 | /* if (sRef_sameName(t1->sref, t4->sref) ) */ | |
444 | /* { */ | |
445 | /* DPRINTF((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */ | |
446 | /* con = constraint_makeEnsureLteMaxRead(t1, t3); */ | |
447 | /* forPred->ensuresConstraints = constraintList_add(forPred->ensuresConstraints, con); */ | |
448 | /* } */ | |
449 | /* else */ | |
450 | /* { */ | |
451 | /* DPRINTF((message ("Didn't Find a for loop matching heuristic:%s %s and %s differ", exprNode_unparse (forPred), exprNode_unparse(t1), exprNode_unparse(t3) ) )); */ | |
452 | /* } */ | |
453 | /* return; */ | |
454 | /* } */ |