Skip to content

Commit 6d22190

Browse files
martintautschnig
martin
authored and
tautschnig
committed
Annotate missed cases in the transform functions of various domains
There are a number of reasons why instruction types were left out of these case statements : 1. Ignoring this instruction is generally a valid overapproximation. 2. Ignoring this instruction is a valid overapproximation for this domain. 3. The instruction is assumed to not be present due to preceding passes. 4. The instruction should never appear in any valid goto program. 5. The instruction is newer than the analysis code and was forgotten. This patch tries to correctly document which of these apply.
1 parent 5727624 commit 6d22190

9 files changed

+142
-79
lines changed

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 15 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -538,18 +538,24 @@ void custom_bitvector_domaint::transform(
538538

539539
case CATCH:
540540
case THROW:
541+
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
542+
break;
541543
case RETURN:
542-
case ATOMIC_BEGIN:
543-
case ATOMIC_END:
544-
case END_FUNCTION:
545-
case LOCATION:
546-
case START_THREAD:
547-
case END_THREAD:
548-
case SKIP:
549-
case ASSERT:
550-
case ASSUME:
544+
DATA_INVARIANT(false, "Returns must be removed before analysis");
545+
break;
546+
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
547+
case ATOMIC_END: // Ignoring is a valid over-approximation
548+
case END_FUNCTION: // No action required
549+
case LOCATION: // No action required
550+
case START_THREAD: // Require a concurrent analysis at higher level
551+
case END_THREAD: // Require a concurrent analysis at higher level
552+
case SKIP: // No action required
553+
case ASSERT: // No action required
554+
case ASSUME: // Ignoring is a valid over-approximation
555+
break;
551556
case INCOMPLETE_GOTO:
552557
case NO_INSTRUCTION_TYPE:
558+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
553559
break;
554560
}
555561
}

‎src/analyses/escape_analysis.cpp

Lines changed: 18 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -253,21 +253,30 @@ void escape_domaint::transform(
253253
// This is the edge to the call site.
254254
break;
255255

256-
case GOTO:
256+
case GOTO: // Ignoring the guard is a valid over-approximation
257+
break;
257258
case CATCH:
258259
case THROW:
260+
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
261+
break;
259262
case RETURN:
260-
case ATOMIC_BEGIN:
261-
case ATOMIC_END:
262-
case LOCATION:
263-
case START_THREAD:
264-
case END_THREAD:
265-
case ASSERT:
266-
case ASSUME:
267-
case SKIP:
263+
DATA_INVARIANT(false, "Returns must be removed before analysis");
264+
break;
265+
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
266+
case ATOMIC_END: // Ignoring is a valid over-approximation
267+
case LOCATION: // No action required
268+
case START_THREAD: // Require a concurrent analysis at higher level
269+
case END_THREAD: // Require a concurrent analysis at higher level
270+
case ASSERT: // No action required
271+
case ASSUME: // Ignoring is a valid over-approximation
272+
case SKIP: // No action required
273+
break;
268274
case OTHER:
275+
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
276+
break;
269277
case INCOMPLETE_GOTO:
270278
case NO_INSTRUCTION_TYPE:
279+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
271280
break;
272281
}
273282
}

‎src/analyses/global_may_alias.cpp

Lines changed: 20 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -129,23 +129,32 @@ void global_may_alias_domaint::transform(
129129
break;
130130
}
131131

132-
case FUNCTION_CALL:
133-
case GOTO:
132+
case FUNCTION_CALL: // Probably safe
133+
case GOTO: // Ignoring the guard is a valid over-approximation
134+
break;
134135
case CATCH:
135136
case THROW:
137+
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
138+
break;
136139
case RETURN:
137-
case ATOMIC_BEGIN:
138-
case ATOMIC_END:
139-
case LOCATION:
140-
case START_THREAD:
141-
case END_THREAD:
142-
case ASSERT:
143-
case ASSUME:
144-
case SKIP:
145-
case END_FUNCTION:
140+
DATA_INVARIANT(false, "Returns must be removed before analysis");
141+
break;
142+
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
143+
case ATOMIC_END: // Ignoring is a valid over-approximation
144+
case LOCATION: // No action required
145+
case START_THREAD: // Require a concurrent analysis at higher level
146+
case END_THREAD: // Require a concurrent analysis at higher level
147+
case ASSERT: // No action required
148+
case ASSUME: // Ignoring is a valid over-approximation
149+
case SKIP: // No action required
150+
case END_FUNCTION: // No action required
151+
break;
146152
case OTHER:
153+
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
154+
break;
147155
case INCOMPLETE_GOTO:
148156
case NO_INSTRUCTION_TYPE:
157+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
149158
break;
150159
}
151160
}

‎src/analyses/interval_domain.cpp

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -110,18 +110,26 @@ void interval_domaint::transform(
110110

111111
case CATCH:
112112
case THROW:
113+
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
114+
break;
113115
case RETURN:
114-
case ATOMIC_BEGIN:
115-
case ATOMIC_END:
116-
case END_FUNCTION:
117-
case START_THREAD:
118-
case END_THREAD:
119-
case ASSERT:
120-
case LOCATION:
121-
case SKIP:
116+
DATA_INVARIANT(false, "Returns must be removed before analysis");
117+
break;
118+
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
119+
case ATOMIC_END: // Ignoring is a valid over-approximation
120+
case END_FUNCTION: // No action required
121+
case START_THREAD: // Require a concurrent analysis at higher level
122+
case END_THREAD: // Require a concurrent analysis at higher level
123+
case ASSERT: // No action required
124+
case LOCATION: // No action required
125+
case SKIP: // No action required
126+
break;
122127
case OTHER:
128+
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
129+
break;
123130
case INCOMPLETE_GOTO:
124131
case NO_INSTRUCTION_TYPE:
132+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
125133
break;
126134
}
127135
}

‎src/analyses/invariant_set_domain.cpp

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -77,16 +77,19 @@ void invariant_set_domaint::transform(
7777

7878
case CATCH:
7979
case THROW:
80-
case DEAD:
81-
case ATOMIC_BEGIN:
82-
case ATOMIC_END:
83-
case END_FUNCTION:
84-
case LOCATION:
85-
case END_THREAD:
86-
case SKIP:
80+
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
81+
break;
82+
case DEAD: // No action required
83+
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
84+
case ATOMIC_END: // Ignoring is a valid over-approximation
85+
case END_FUNCTION: // No action required
86+
case LOCATION: // No action required
87+
case END_THREAD: // Require a concurrent analysis at higher level
88+
case SKIP: // No action required
89+
break;
8790
case INCOMPLETE_GOTO:
8891
case NO_INSTRUCTION_TYPE:
89-
// do nothing
92+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
9093
break;
9194
}
9295
}

‎src/analyses/local_bitvector_analysis.cpp

Lines changed: 19 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -310,20 +310,29 @@ void local_bitvector_analysist::build()
310310

311311
case CATCH:
312312
case THROW:
313+
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
314+
break;
313315
case RETURN:
314-
case ATOMIC_BEGIN:
315-
case ATOMIC_END:
316-
case LOCATION:
317-
case START_THREAD:
318-
case END_THREAD:
319-
case SKIP:
316+
DATA_INVARIANT(false, "Returns must be removed before analysis");
317+
break;
318+
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
319+
case ATOMIC_END: // Ignoring is a valid over-approximation
320+
case LOCATION: // No action required
321+
case START_THREAD: // Require a concurrent analysis at higher level
322+
case END_THREAD: // Require a concurrent analysis at higher level
323+
case SKIP: // No action required
324+
case ASSERT: // No action required
325+
case ASSUME: // Ignoring is a valid over-approximation
326+
case GOTO: // Ignoring the guard is a valid over-approximation
327+
case END_FUNCTION: // No action required
328+
break;
320329
case OTHER:
321-
case ASSERT:
322-
case ASSUME:
323-
case GOTO:
324-
case END_FUNCTION:
330+
DATA_INVARIANT(
331+
false, "Unclear what is a safe over-approximation of OTHER");
332+
break;
325333
case INCOMPLETE_GOTO:
326334
case NO_INSTRUCTION_TYPE:
335+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
327336
break;
328337
}
329338

‎src/analyses/local_cfg.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,9 +86,12 @@ void local_cfgt::build(const goto_programt &goto_program)
8686
case DECL:
8787
case DEAD:
8888
case ASSIGN:
89+
node.successors.push_back(loc_nr + 1);
90+
break;
91+
8992
case INCOMPLETE_GOTO:
9093
case NO_INSTRUCTION_TYPE:
91-
node.successors.push_back(loc_nr+1);
94+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
9295
break;
9396
}
9497
}

‎src/analyses/local_may_alias.cpp

Lines changed: 19 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -419,20 +419,29 @@ void local_may_aliast::build(const goto_functiont &goto_function)
419419

420420
case CATCH:
421421
case THROW:
422+
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
423+
break;
422424
case RETURN:
423-
case GOTO:
424-
case START_THREAD:
425-
case END_THREAD:
426-
case ATOMIC_BEGIN:
427-
case ATOMIC_END:
428-
case LOCATION:
429-
case SKIP:
430-
case END_FUNCTION:
425+
DATA_INVARIANT(false, "Returns must be removed before analysis");
426+
break;
427+
case GOTO: // Ignoring the guard is a valid over-approximation
428+
case START_THREAD: // Require a concurrent analysis at higher level
429+
case END_THREAD: // Require a concurrent analysis at higher level
430+
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
431+
case ATOMIC_END: // Ignoring is a valid over-approximation
432+
case LOCATION: // No action required
433+
case SKIP: // No action required
434+
case END_FUNCTION: // No action required
435+
case ASSERT: // No action required
436+
case ASSUME: // Ignoring is a valid over-approximation
437+
break;
431438
case OTHER:
432-
case ASSERT:
433-
case ASSUME:
439+
DATA_INVARIANT(
440+
false, "Unclear what is a safe over-approximation of OTHER");
441+
break;
434442
case INCOMPLETE_GOTO:
435443
case NO_INSTRUCTION_TYPE:
444+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
436445
break;
437446
}
438447

‎src/analyses/uncaught_exceptions_analysis.cpp

Lines changed: 20 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -125,23 +125,30 @@ void uncaught_exceptions_domaint::transform(
125125
join(uea.exceptions_map[function_name]);
126126
break;
127127
}
128-
case DECL:
129-
case DEAD:
130-
case ASSIGN:
128+
case DECL: // Safe to ignore in this context
129+
case DEAD: // Safe to ignore in this context
130+
case ASSIGN: // Safe to ignore in this context
131+
break;
131132
case RETURN:
132-
case GOTO:
133-
case ATOMIC_BEGIN:
134-
case ATOMIC_END:
135-
case START_THREAD:
136-
case END_THREAD:
137-
case END_FUNCTION:
138-
case ASSERT:
139-
case ASSUME:
140-
case LOCATION:
141-
case SKIP:
133+
DATA_INVARIANT(false, "Returns must be removed before analysis");
134+
break;
135+
case GOTO: // Ignoring the guard is a valid over-approximation
136+
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
137+
case ATOMIC_END: // Ignoring is a valid over-approximation
138+
case START_THREAD: // Require a concurrent analysis at higher level
139+
case END_THREAD: // Require a concurrent analysis at higher level
140+
case END_FUNCTION: // No action required
141+
case ASSERT: // No action required
142+
case ASSUME: // Ignoring is a valid over-approximation
143+
case LOCATION: // No action required
144+
case SKIP: // No action required
145+
break;
142146
case OTHER:
147+
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
148+
break;
143149
case INCOMPLETE_GOTO:
144150
case NO_INSTRUCTION_TYPE:
151+
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
145152
break;
146153
}
147154
}

0 commit comments

Comments
 (0)