]>
Commit | Line | Data |
---|---|---|
4cccc6ad | 1 | /* |
2 | ** constraintList.c | |
3 | */ | |
4 | ||
5 | # include <ctype.h> /* for isdigit */ | |
6 | # include "lclintMacros.nf" | |
7 | # include "basic.h" | |
8 | # include "cgrammar.h" | |
9 | # include "cgrammar_tokens.h" | |
10 | ||
11 | # include "exprChecks.h" | |
12 | # include "aliasChecks.h" | |
13 | # include "exprNodeSList.h" | |
14 | # include "exprData.i" | |
15 | ||
16 | /*@i33*/ | |
17 | /*@-fcnuse*/ | |
18 | /*@-assignexpose*/ | |
19 | ||
361091cc | 20 | /*@notnull@*/ |
21 | /*@special@*/ constraint constraint_makeNew (void) | |
22 | /*@post:isnull result->term, result->expr, result->constrType@*/ | |
23 | /*@defines result->ar, result->post@*/; | |
24 | ||
4cccc6ad | 25 | constraint constraint_copy (constraint c) |
26 | { | |
27 | constraint ret; | |
28 | ret = constraint_makeNew(); | |
361091cc | 29 | ret->lexpr = c->lexpr; |
4cccc6ad | 30 | ret->ar = c->ar; |
361091cc | 31 | ret->expr = c->expr; |
4cccc6ad | 32 | ret->post = c->post; |
33 | return ret; | |
34 | } | |
35 | ||
36 | bool constraint_resolve (/*@unused@*/ constraint c) | |
37 | { | |
38 | return FALSE; | |
39 | } | |
40 | ||
41 | /*@notnull@*/ | |
42 | /*@special@*/ constraint constraint_makeNew (void) | |
361091cc | 43 | /*@post:isnull result->term, result->expr, result->constrType@*/ |
4cccc6ad | 44 | /*@defines result->ar, result->post@*/ |
45 | { | |
46 | constraint ret; | |
47 | ret = dmalloc(sizeof (*ret) ); | |
361091cc | 48 | ret->lexpr = NULL; |
49 | ret->expr = NULL; | |
4cccc6ad | 50 | ret->ar = LT; |
51 | ret->post = FALSE; | |
52 | /*@i23*/return ret; | |
53 | } | |
54 | /*@-czechfcns@*/ | |
361091cc | 55 | constraintExpr constraintExpr_alloc () |
56 | { | |
57 | constraintExpr ret; | |
58 | ret = dmalloc (sizeof (*ret) ); | |
59 | ret->term = NULL; | |
60 | ret->expr = NULL; | |
61 | ret->op = PLUS; | |
62 | return ret; | |
63 | } | |
4cccc6ad | 64 | |
361091cc | 65 | constraintExpr constraintExpr_copy (constraintExpr expr) |
4cccc6ad | 66 | { |
361091cc | 67 | constraintExpr ret; |
68 | ret = constraintExpr_alloc(); | |
69 | ret->term = constraintTerm_copy(expr->term); | |
70 | ret->op = expr->op; | |
71 | if (expr->expr != NULL) | |
72 | { | |
73 | ret->expr = constraintExpr_copy (expr->expr); | |
74 | } | |
75 | else | |
76 | { | |
77 | ret->expr = NULL; | |
78 | } | |
4cccc6ad | 79 | |
361091cc | 80 | } |
81 | ||
82 | constraintExpr constraintExpr_makeMaxSetExpr (exprNode expr) | |
83 | { | |
84 | constraintExpr ret; | |
85 | ret = constraintExpr_alloc(); | |
86 | ret->term = constraintTerm_makeMaxSetexpr(expr); | |
4cccc6ad | 87 | return ret; |
88 | } | |
89 | ||
361091cc | 90 | constraintExpr constraintExpr_makeMaxReadExpr (exprNode expr) |
4cccc6ad | 91 | { |
361091cc | 92 | constraintExpr ret; |
93 | ret = constraintExpr_alloc(); | |
94 | ret->term = constraintTerm_makeMaxReadexpr(expr); | |
4cccc6ad | 95 | return ret; |
96 | } | |
97 | ||
361091cc | 98 | constraintExpr constraintExpr_makeMinSetExpr (exprNode expr) |
99 | { | |
100 | constraintExpr ret; | |
101 | ret = constraintExpr_alloc(); | |
102 | ret->term = constraintTerm_makeMinSetexpr(expr); | |
103 | return ret; | |
104 | } | |
4cccc6ad | 105 | |
361091cc | 106 | constraintExpr constraintExpr_makeMinReadExpr (exprNode expr) |
4cccc6ad | 107 | { |
361091cc | 108 | constraintExpr ret; |
109 | ret = constraintExpr_alloc(); | |
110 | ret->term = constraintTerm_makeMinReadexpr(expr); | |
4cccc6ad | 111 | return ret; |
112 | } | |
4cccc6ad | 113 | |
361091cc | 114 | constraintExpr constraintExpr_makeValueExpr (exprNode expr) |
4cccc6ad | 115 | { |
116 | constraintExpr ret; | |
361091cc | 117 | ret = constraintExpr_alloc(); |
118 | ret->term = constraintTerm_makeValueexpr(expr); | |
4cccc6ad | 119 | return ret; |
120 | } | |
121 | ||
122 | ||
361091cc | 123 | constraintExpr makeConstraintExprIntlit (int i) |
4cccc6ad | 124 | { |
125 | constraintExpr ret; | |
126 | ret = dmalloc (sizeof (*ret) ); | |
361091cc | 127 | ret->term = constraintTerm_makeIntLitValue(i); |
128 | ret->expr = NULL; | |
4cccc6ad | 129 | ret->op = PLUS; |
130 | /*@i1*/ return ret; | |
131 | } | |
132 | ||
4cccc6ad | 133 | |
361091cc | 134 | constraintExpr constraintExpr_makeValueInt (int i) |
135 | { | |
136 | return makeConstraintExprIntlit(i); | |
4cccc6ad | 137 | } |
138 | ||
139 | constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) | |
140 | { | |
141 | constraint ret = constraint_makeNew(); | |
142 | constraintTerm term; | |
361091cc | 143 | |
144 | ret->lexpr =constraintExpr_makeMaxSetExpr(po); | |
4cccc6ad | 145 | ret->ar = GTE; |
361091cc | 146 | ret->expr = constraintExpr_makeValueExpr (ind); |
4cccc6ad | 147 | /*@i1*/return ret; |
148 | } | |
361091cc | 149 | |
150 | constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind) | |
151 | { | |
152 | constraint ret = constraint_makeNew(); | |
153 | // constraintTerm term; | |
154 | po = exprNode_fakeCopy(po); | |
155 | ind = exprNode_fakeCopy(ind); | |
156 | ret->lexpr = constraintExpr_makeMaxReadExpr(po); | |
157 | ret->ar = GTE; | |
158 | ret->expr = constraintExpr_makeValueExpr (ind); | |
159 | return ret; | |
160 | } | |
4cccc6ad | 161 | |
361091cc | 162 | constraint constraint_makeWriteSafeInt (exprNode po, int ind) |
4cccc6ad | 163 | { |
164 | constraint ret = constraint_makeNew(); | |
165 | constraintTerm term; | |
361091cc | 166 | |
167 | ret->lexpr =constraintExpr_makeMaxSetExpr(po); | |
4cccc6ad | 168 | ret->ar = GTE; |
361091cc | 169 | ret->expr = constraintExpr_makeValueInt (ind); |
170 | /*@i1*/return ret; | |
4cccc6ad | 171 | } |
361091cc | 172 | |
173 | constraint constraint_makeReadSafeInt ( exprNode po, int ind) | |
174 | { | |
175 | constraint ret = constraint_makeNew(); | |
4cccc6ad | 176 | |
361091cc | 177 | po = exprNode_fakeCopy(po); |
178 | ||
179 | ret->lexpr = constraintExpr_makeMaxReadExpr(po); | |
180 | ret->ar = GTE; | |
181 | ret->expr = constraintExpr_makeValueInt (ind); | |
182 | return ret; | |
183 | } | |
4cccc6ad | 184 | |
361091cc | 185 | constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint) |
4cccc6ad | 186 | { |
187 | constraint ret = constraint_makeNew(); | |
188 | constraintTerm term; | |
189 | ||
361091cc | 190 | e1 = exprNode_fakeCopy (e1); |
4cccc6ad | 191 | t2 = exprNode_fakeCopy (t2); |
192 | ||
361091cc | 193 | ret = constraint_makeReadSafeExprNode(e1, t2); |
194 | if (ret->lexpr->term->loc != NULL) | |
195 | fileloc_free(ret->lexpr->term->loc); | |
4cccc6ad | 196 | |
361091cc | 197 | ret->lexpr->term->loc = fileloc_copy (sequencePoint); |
4cccc6ad | 198 | ret->post = TRUE; |
361091cc | 199 | |
200 | fileloc_incColumn (ret->lexpr->term->loc); | |
201 | return ret; | |
4cccc6ad | 202 | } |
203 | ||
361091cc | 204 | |
4cccc6ad | 205 | constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint) |
206 | { | |
207 | constraint ret = constraint_makeNew(); | |
208 | constraintTerm term; | |
361091cc | 209 | po = exprNode_fakeCopy(po); |
210 | ind = exprNode_fakeCopy(ind); | |
4cccc6ad | 211 | |
361091cc | 212 | ret->lexpr = constraintExpr_makeMinReadExpr(po); |
4cccc6ad | 213 | ret->ar = LTE; |
361091cc | 214 | ret->expr = constraintExpr_makeValueExpr (ind); |
4cccc6ad | 215 | ret->post = TRUE; |
361091cc | 216 | |
217 | if (ret->lexpr->term->loc != NULL) | |
218 | fileloc_free(ret->lexpr->term->loc); | |
4cccc6ad | 219 | |
361091cc | 220 | ret->lexpr->term->loc = fileloc_copy (sequencePoint); |
4cccc6ad | 221 | /*make this refer to element after preconditions */ |
361091cc | 222 | fileloc_incColumn (ret->lexpr->term->loc); |
4cccc6ad | 223 | /*@i1*/ return ret; |
224 | } | |
225 | ||
361091cc | 226 | constraintExpr makeMaxSetPostOpInc (exprNode e) |
4cccc6ad | 227 | { |
228 | constraintExpr ret; | |
361091cc | 229 | ret = constraintExpr_makeValueExpr (e); |
230 | ret->term = constraintTerm_makeMaxSetexpr (e); | |
231 | ret->op = MINUS; | |
232 | ret->expr = makeConstraintExprIntlit (1); | |
4cccc6ad | 233 | return ret; |
234 | } | |
235 | ||
361091cc | 236 | constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint) |
4cccc6ad | 237 | { |
238 | constraint ret = constraint_makeNew(); | |
239 | //constraintTerm term; | |
240 | exprNode t2; | |
361091cc | 241 | e = exprNode_fakeCopy(e); |
242 | ret->lexpr = constraintExpr_makeMaxSetExpr(e); | |
4cccc6ad | 243 | ret->ar = EQ; |
244 | ret->post = TRUE; | |
361091cc | 245 | ret->expr = makeMaxSetPostOpInc(e); |
4cccc6ad | 246 | |
361091cc | 247 | fileloc_incColumn ( ret->lexpr->term->loc); |
248 | fileloc_incColumn ( ret->lexpr->term->loc); | |
249 | return ret; | |
4cccc6ad | 250 | } |
251 | ||
361091cc | 252 | constraintExpr makeMaxReadPostOpInc (exprNode e) |
4cccc6ad | 253 | { |
361091cc | 254 | constraintExpr ret; |
255 | ret = constraintExpr_makeValueExpr (e); | |
256 | ret->term = constraintTerm_makeMaxReadexpr (e); | |
257 | ret->op = MINUS; | |
258 | ret->expr = makeConstraintExprIntlit (1); | |
259 | return ret; | |
4cccc6ad | 260 | } |
361091cc | 261 | |
262 | constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint) | |
4cccc6ad | 263 | { |
361091cc | 264 | constraint ret = constraint_makeNew(); |
265 | //constraintTerm term; | |
266 | exprNode t2; | |
267 | e = exprNode_fakeCopy(e); | |
268 | ret->lexpr = constraintExpr_makeMaxReadExpr(e); | |
269 | ret->ar = EQ; | |
270 | ret->post = TRUE; | |
271 | ret->expr = makeMaxReadPostOpInc(e); | |
4cccc6ad | 272 | |
361091cc | 273 | fileloc_incColumn ( ret->lexpr->term->loc); |
274 | fileloc_incColumn ( ret->lexpr->term->loc); | |
275 | return ret; | |
4cccc6ad | 276 | } |
277 | ||
361091cc | 278 | |
279 | cstring arithType_print (arithType ar) | |
4cccc6ad | 280 | { |
361091cc | 281 | cstring st = cstring_undefined; |
4cccc6ad | 282 | switch (ar) |
283 | { | |
284 | case LT: | |
361091cc | 285 | st = cstring_makeLiteral (" < "); |
286 | break; | |
4cccc6ad | 287 | case LTE: |
361091cc | 288 | st = cstring_makeLiteral (" <= "); |
289 | break; | |
4cccc6ad | 290 | case GT: |
361091cc | 291 | st = cstring_makeLiteral (" > "); |
292 | break; | |
4cccc6ad | 293 | case GTE: |
361091cc | 294 | st = cstring_makeLiteral (" >= "); |
295 | break; | |
4cccc6ad | 296 | case EQ: |
361091cc | 297 | st = cstring_makeLiteral (" == "); |
298 | break; | |
4cccc6ad | 299 | case NONNEGATIVE: |
361091cc | 300 | st = cstring_makeLiteral (" NONNEGATIVE "); |
301 | break; | |
4cccc6ad | 302 | case POSITIVE: |
361091cc | 303 | st = cstring_makeLiteral (" POSITIVE "); |
304 | break; | |
4cccc6ad | 305 | default: |
306 | llassert(FALSE); | |
361091cc | 307 | break; |
4cccc6ad | 308 | } |
361091cc | 309 | return st; |
4cccc6ad | 310 | } |
311 | ||
361091cc | 312 | cstring constraintExpr_print (constraintExpr ex) |
4cccc6ad | 313 | { |
361091cc | 314 | cstring st; |
315 | cstring opStr; | |
4cccc6ad | 316 | llassert (ex != NULL); |
361091cc | 317 | |
318 | st = message ("%s", | |
319 | constraintTerm_print (ex->term)); | |
320 | ||
321 | if (ex->expr != NULL) | |
4cccc6ad | 322 | { |
323 | if (ex->op == PLUS) | |
324 | { | |
361091cc | 325 | opStr = cstring_makeLiteral (" + "); |
4cccc6ad | 326 | } |
327 | else | |
328 | { | |
361091cc | 329 | opStr = cstring_makeLiteral (" - "); |
4cccc6ad | 330 | } |
361091cc | 331 | st = message ("%s %s %s", st, opStr, constraintExpr_print (ex->expr) ); |
4cccc6ad | 332 | } |
361091cc | 333 | return st; |
4cccc6ad | 334 | } |
335 | ||
336 | ||
361091cc | 337 | cstring constraint_print (constraint c) |
4cccc6ad | 338 | { |
361091cc | 339 | cstring st = cstring_undefined; |
340 | cstring type = cstring_undefined; | |
341 | llassert (c); | |
4cccc6ad | 342 | if (c->post) |
343 | { | |
361091cc | 344 | type = cstring_makeLiteral ("Ensures: "); |
4cccc6ad | 345 | } |
346 | else | |
347 | { | |
361091cc | 348 | type = cstring_makeLiteral ("Requires: "); |
4cccc6ad | 349 | } |
361091cc | 350 | st = message ("%s: %s %s %s", |
351 | type, | |
352 | constraintExpr_print (c->lexpr), | |
353 | arithType_print(c->ar), | |
354 | constraintExpr_print(c->expr) | |
355 | ); | |
356 | return st; | |
4cccc6ad | 357 | } |
358 | ||
359 | /*@=fcnuse*/ | |
360 | /*@=assignexpose*/ | |
361 | /*@=czechfcns@*/ |