Skip to content

Commit b9adc75

Browse files
tautschnigtautschnig
committed
Check some assumptions about goto programs before starting an analysis
The current set of checks is certainly very incomplete, but at least provides some entry points for adding further tests.
1 parent c674ce7 commit b9adc75

12 files changed

+282
-2
lines changed

‎src/cbmc/cbmc_parse_options.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -672,6 +672,12 @@ int cbmc_parse_optionst::get_goto_program(
672672

673673
goto_convert(symbol_table, goto_functions, ui_message_handler);
674674

675+
if(goto_functions.check_internal_invariants(*this))
676+
{
677+
error() << "GOTO program violates internal invariants" << eom;
678+
return 6;
679+
}
680+
675681
if(process_goto_program(options, goto_functions))
676682
return 6;
677683

‎src/clobber/clobber_parse_options.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,12 @@ int clobber_parse_optionst::doit()
127127
if(get_goto_program(options, goto_functions))
128128
return 6;
129129

130+
if(goto_functions.check_internal_invariants(*this))
131+
{
132+
error() << "GOTO program violates internal invariants" << eom;
133+
return 6;
134+
}
135+
130136
label_properties(goto_functions);
131137

132138
if(cmdline.isset("show-properties"))

‎src/goto-cc/compile.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,12 @@ bool compilet::doit()
129129
return true;
130130
}
131131

132+
if(compiled_functions.check_internal_invariants(*this))
133+
{
134+
error() << "GOTO program violates internal invariants" << eom;
135+
return true;
136+
}
137+
132138
return
133139
warning_is_fatal &&
134140
get_message_handler().get_message_count(messaget::M_WARNING)!=

‎src/goto-diff/goto_diff_parse_options.cpp

+12
Original file line numberDiff line numberDiff line change
@@ -278,6 +278,18 @@ int goto_diff_parse_optionst::doit()
278278
if(get_goto_program_ret!=-1)
279279
return get_goto_program_ret;
280280

281+
if(goto_model1.goto_functions.check_internal_invariants(*this))
282+
{
283+
error() << "GOTO program violates internal invariants" << eom;
284+
return 6;
285+
}
286+
287+
if(goto_model2.goto_functions.check_internal_invariants(*this))
288+
{
289+
error() << "GOTO program violates internal invariants" << eom;
290+
return 6;
291+
}
292+
281293
if(cmdline.isset("show-goto-functions"))
282294
{
283295
show_goto_functions(goto_model1, get_ui());

‎src/goto-instrument/goto_instrument_parse_options.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -868,6 +868,12 @@ void goto_instrument_parse_optionst::get_goto_program()
868868

869869
config.set(cmdline);
870870
config.set_from_symbol_table(symbol_table);
871+
872+
if(goto_functions.check_internal_invariants(*this))
873+
{
874+
error() << "GOTO program violates internal invariants" << eom;
875+
throw 0;
876+
}
871877
}
872878

873879
void goto_instrument_parse_optionst::instrument_goto_program()

‎src/goto-programs/goto_functions.cpp

+13
Original file line numberDiff line numberDiff line change
@@ -30,3 +30,16 @@ void get_local_identifiers(
3030
dest.insert(identifier);
3131
}
3232
}
33+
34+
/// Ensure that all functions satisfy all assumptions about
35+
/// consistent goto programs.
36+
/// \param msg Message output
37+
/// \return True, iff at least one invariant is violated
38+
bool goto_functionst::check_internal_invariants(messaget &msg) const
39+
{
40+
forall_goto_functions(it, *this)
41+
if(it->second.body.check_internal_invariants(msg))
42+
return true;
43+
44+
return false;
45+
}

‎src/goto-programs/goto_functions.h

+2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,8 @@ class goto_functionst:public goto_functions_templatet<goto_programt>
4343
goto_functions_templatet::operator=(std::move(other));
4444
return *this;
4545
}
46+
47+
bool check_internal_invariants(messaget &msg) const;
4648
};
4749

4850
#define Forall_goto_functions(it, functions) \

‎src/goto-programs/goto_program.cpp

+127
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <ostream>
1515

16+
#include <util/message.h>
1617
#include <util/std_expr.h>
1718

1819
#include <langapi/language_util.h>
@@ -483,3 +484,129 @@ std::string as_string(
483484

484485
return "";
485486
}
487+
488+
/// Ensure the current goto_programt satisfies all assumptions
489+
/// about consistent goto programs.
490+
/// \param msg Message output
491+
/// \return True, iff at least one invariant is violated
492+
bool goto_programt::check_internal_invariants(messaget &msg) const
493+
{
494+
if(empty())
495+
return false;
496+
497+
unsigned prev_loc_number=0;
498+
bool prev_loc_number_set=false;
499+
500+
forall_goto_program_instructions(it, *this)
501+
{
502+
const goto_programt::instructiont &ins=*it;
503+
504+
if(ins.check_internal_invariants(msg))
505+
return true;
506+
507+
if(prev_loc_number_set &&
508+
ins.location_number<=prev_loc_number)
509+
{
510+
msg.error().source_location=ins.source_location;
511+
msg.error() << "location number not strictly increasing"
512+
<< messaget::eom;
513+
return true;
514+
}
515+
else if(!prev_loc_number_set)
516+
{
517+
prev_loc_number=ins.location_number;
518+
prev_loc_number_set=true;
519+
}
520+
521+
switch(ins.type)
522+
{
523+
case GOTO:
524+
case ASSUME:
525+
case ASSERT:
526+
if(ins.guard.type()!=bool_typet())
527+
{
528+
msg.error().source_location=ins.source_location;
529+
msg.error() << ins.type << " has non-Boolean guard"
530+
<< messaget::eom;
531+
return true;
532+
}
533+
break;
534+
case OTHER:
535+
case SKIP:
536+
case LOCATION:
537+
case END_FUNCTION:
538+
case START_THREAD:
539+
case END_THREAD:
540+
case ATOMIC_BEGIN:
541+
case ATOMIC_END:
542+
case RETURN:
543+
break;
544+
case ASSIGN:
545+
if(ins.code.get_statement()!=ID_assign)
546+
{
547+
msg.error().source_location=ins.source_location;
548+
msg.error() << ins.type << " instruction has code "
549+
<< ins.code.get_statement()
550+
<< messaget::eom;
551+
return true;
552+
}
553+
return false;
554+
case DECL:
555+
if(ins.code.get_statement()!=ID_decl)
556+
{
557+
msg.error().source_location=ins.source_location;
558+
msg.error() << ins.type << " instruction has code "
559+
<< ins.code.get_statement()
560+
<< messaget::eom;
561+
return true;
562+
}
563+
else if(to_code_decl(ins.code).symbol().id()!=ID_symbol)
564+
{
565+
msg.error().source_location=ins.source_location;
566+
msg.error() << "declaration operand is not a symbol"
567+
<< messaget::eom;
568+
return true;
569+
}
570+
break;
571+
case DEAD:
572+
if(ins.code.get_statement()!=ID_dead)
573+
{
574+
msg.error().source_location=ins.source_location;
575+
msg.error() << ins.type << " instruction has code "
576+
<< ins.code.get_statement()
577+
<< messaget::eom;
578+
return true;
579+
}
580+
break;
581+
case FUNCTION_CALL:
582+
if(ins.code.get_statement()!=ID_function_call)
583+
{
584+
msg.error().source_location=ins.source_location;
585+
msg.error() << ins.type << " instruction has code "
586+
<< ins.code.get_statement()
587+
<< messaget::eom;
588+
return true;
589+
}
590+
break;
591+
case THROW:
592+
case CATCH:
593+
break;
594+
case NO_INSTRUCTION_TYPE:
595+
msg.error().source_location=ins.source_location;
596+
msg.error() << ins.type << " not permitted"
597+
<< messaget::eom;
598+
return true;
599+
}
600+
}
601+
602+
// the last instruction must be END_FUNCTION
603+
if(!get_end_function()->is_end_function())
604+
{
605+
msg.error().source_location=get_end_function()->source_location;
606+
msg.error() << "end of function is of type "
607+
<< get_end_function()->type << messaget::eom;
608+
return true;
609+
}
610+
611+
return false;
612+
}

‎src/goto-programs/goto_program.h

+2
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,8 @@ class goto_programt:public goto_program_templatet<codet, exprt>
6464
// get the variables in decl statements
6565
typedef std::set<irep_idt> decl_identifierst;
6666
void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
67+
68+
bool check_internal_invariants(messaget &msg) const;
6769
};
6870

6971
#define forall_goto_program_instructions(it, program) \

‎src/goto-programs/goto_program_template.h

+90-2
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
2121
#include <sstream>
2222
#include <string>
2323

24+
#include <util/invariant.h>
25+
#include <util/message.h>
2426
#include <util/namespace.h>
2527
#include <util/symbol_table.h>
2628
#include <util/source_location.h>
@@ -262,6 +264,84 @@ class goto_program_templatet
262264
instruction_id_builder << type;
263265
return instruction_id_builder.str();
264266
}
267+
268+
/// Ensure the current instruction satisfies all assumptions
269+
/// within consistent goto programs.
270+
/// \param msg Message output
271+
/// \return True, iff at least one invariant is violated
272+
bool check_internal_invariants(messaget &msg) const
273+
{
274+
if(function.empty())
275+
{
276+
msg.error().source_location=source_location;
277+
msg.error() << "instruction has no function name"
278+
<< messaget::eom;
279+
return true;
280+
}
281+
282+
switch(type)
283+
{
284+
case GOTO:
285+
case ASSUME:
286+
case ASSERT:
287+
if(code!=irept() && code.is_not_nil())
288+
{
289+
msg.error().source_location=source_location;
290+
msg.error() << type << " has non-nil code\n"
291+
<< code.pretty() << messaget::eom;
292+
return true;
293+
}
294+
else if(guard.is_nil() || guard==irept())
295+
{
296+
msg.error().source_location=source_location;
297+
msg.error() << type << " has nil guard"
298+
<< messaget::eom;
299+
return true;
300+
}
301+
return false;
302+
case OTHER:
303+
return false;
304+
case SKIP:
305+
case LOCATION:
306+
case END_FUNCTION:
307+
if(code!=irept() && code.is_not_nil())
308+
{
309+
msg.error().source_location=source_location;
310+
msg.error() << type << " has non-nil code\n"
311+
<< code.pretty() << messaget::eom;
312+
return true;
313+
}
314+
return false;
315+
case START_THREAD:
316+
return false;
317+
case END_THREAD:
318+
return false;
319+
case ATOMIC_BEGIN:
320+
return false;
321+
case ATOMIC_END:
322+
return false;
323+
case RETURN:
324+
return false;
325+
case ASSIGN:
326+
case DECL:
327+
case DEAD:
328+
case FUNCTION_CALL:
329+
if(code==irept() || code.is_nil())
330+
{
331+
msg.error().source_location=source_location;
332+
msg.error() << type << " has nil code"
333+
<< messaget::eom;
334+
return true;
335+
}
336+
return false;
337+
case THROW:
338+
return false;
339+
case CATCH:
340+
return false;
341+
default:
342+
return true;
343+
}
344+
}
265345
};
266346

267347
typedef std::list<instructiont> instructionst;
@@ -466,9 +546,17 @@ class goto_program_templatet
466546

467547
targett get_end_function()
468548
{
469-
assert(!instructions.empty());
549+
PRECONDITION(!instructions.empty());
550+
const auto end_function=std::prev(instructions.end());
551+
DATA_INVARIANT(end_function->is_end_function(), "invalid end_function");
552+
return end_function;
553+
}
554+
555+
const_targett get_end_function() const
556+
{
557+
PRECONDITION(!instructions.empty());
470558
const auto end_function=std::prev(instructions.end());
471-
assert(end_function->is_end_function());
559+
DATA_INVARIANT(end_function->is_end_function(), "invalid end_function");
472560
return end_function;
473561
}
474562

‎src/musketeer/musketeer_parse_options.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,12 @@ void goto_fence_inserter_parse_optionst::get_goto_program(
141141
throw 0;
142142

143143
config.set_from_symbol_table(symbol_table);
144+
145+
if(goto_functions.check_internal_invariants(*this))
146+
{
147+
error() << "GOTO program violates internal invariants" << eom;
148+
throw 0;
149+
}
144150
}
145151

146152
void goto_fence_inserter_parse_optionst::instrument_goto_program(

‎src/symex/symex_parse_options.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,12 @@ int symex_parse_optionst::doit()
138138
if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
139139
return 6;
140140

141+
if(goto_model.goto_functions.check_internal_invariants(*this))
142+
{
143+
error() << "GOTO program violates internal invariants" << eom;
144+
return 6;
145+
}
146+
141147
if(process_goto_program(options))
142148
return 6;
143149

0 commit comments

Comments
 (0)