diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index f9eecb2238f..e718a7b7a68 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -676,15 +676,38 @@ void goto_programt::instructiont::validate( validate_full_code(code, ns, vm); validate_full_expr(guard, ns, vm); + const symbolt *table_symbol; + switch(type) { case NO_INSTRUCTION_TYPE: break; case GOTO: + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + has_target(), + "goto instruction expects at least one target", + source_location); + // get_target checks that targets.size()==1 + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + get_target()->is_target() && get_target()->target_number != 0, + "goto target has to be a target", + source_location); break; case ASSUME: + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + targets.empty(), + "assume instruction should not have a target", + source_location); break; case ASSERT: + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + targets.empty(), + "assert instruction should not have a target", + source_location); break; case OTHER: break; @@ -703,6 +726,11 @@ void goto_programt::instructiont::validate( case ATOMIC_END: break; case RETURN: + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + code.get_statement() == ID_return, + "return instruction should contain a return statement", + source_location); break; case ASSIGN: DATA_CHECK( @@ -713,10 +741,37 @@ void goto_programt::instructiont::validate( vm, targets.empty(), "assign instruction should not have a target"); break; case DECL: + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + code.get_statement() == ID_decl, + "declaration instructions should contain a declaration statement", + source_location); + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + !ns.lookup(to_code_decl(code).get_identifier(), table_symbol), + "declared symbols should be known", + id2string(to_code_decl(code).get_identifier()), + source_location); break; case DEAD: + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + code.get_statement() == ID_dead, + "dead instructions should contain a dead statement", + source_location); + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + !ns.lookup(to_code_dead(code).get_identifier(), table_symbol), + "removed symbols should be known", + id2string(to_code_dead(code).get_identifier()), + source_location); break; case FUNCTION_CALL: + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + code.get_statement() == ID_function_call, + "function call instruction should contain a call statement", + source_location); break; case THROW: break; diff --git a/src/util/std_code.h b/src/util/std_code.h index a3c73fae594..0a877a2a399 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -371,6 +371,19 @@ class code_declt:public codet { return symbol().get_identifier(); } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, code.operands().size() == 1, "declaration must have one operand"); + DATA_CHECK( + vm, + code.op0().id() == ID_symbol, + "declaring a non-symbol: " + + id2string(to_symbol_expr(code.op0()).get_identifier())); + } }; template<> inline bool can_cast_expr(const exprt &base) @@ -430,6 +443,21 @@ class code_deadt:public codet { return symbol().get_identifier(); } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, + code.operands().size() == 1, + "removal (code_deadt) must have one operand"); + DATA_CHECK( + vm, + code.op0().id() == ID_symbol, + "removing a non-symbol: " + + id2string(to_symbol_expr(code.op0()).get_identifier()) + "from scope"); + } }; template<> inline bool can_cast_expr(const exprt &base) @@ -510,6 +538,11 @@ inline code_assumet &to_code_assume(codet &code) return static_cast(code); } +inline void validate_expr(const code_assumet &x) +{ + validate_operands(x, 1, "assume must have one operand"); +} + /// A non-fatal assertion, which checks a condition then permits execution to /// continue. class code_assertt:public codet @@ -557,6 +590,11 @@ inline code_assertt &to_code_assert(codet &code) return static_cast(code); } +inline void validate_expr(const code_assertt &x) +{ + validate_operands(x, 1, "assert must have one operand"); +} + /// Create a fatal assertion, which checks a condition and then halts if it does /// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`. /// @@ -1046,6 +1084,51 @@ class code_function_callt:public codet { return op2().operands(); } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, + code.operands().size() == 3, + "function calls must have three operands:\n1) expression to store the " + "returned values\n2) the function being called\n3) the vector of " + "arguments"); + } + + static void validate( + const codet &code, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + check(code, vm); + + if(code.op0().id() == ID_nil) + DATA_CHECK( + vm, + to_code_type(code.op1().type()).return_type().id() == ID_empty, + "void function should not return value"); + else + DATA_CHECK( + vm, + base_type_eq( + code.op0().type(), to_code_type(code.op1().type()).return_type(), ns), + "function returns expression of wrong type"); + } + + static void validate_full( + const codet &code, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + for(const exprt &op : code.operands()) + { + validate_full_expr(op, ns, vm); + } + + validate(code, ns, vm); + } }; template<> inline bool can_cast_expr(const exprt &base) @@ -1068,6 +1151,11 @@ inline code_function_callt &to_code_function_call(codet &code) return static_cast(code); } +inline void validate_expr(const code_function_callt &x) +{ + validate_operands(x, 3, "function calls must have three operands"); +} + /// \ref codet representation of a "return from a function" statement. class code_returnt:public codet { @@ -1099,6 +1187,13 @@ class code_returnt:public codet return false; // backwards compatibility return return_value().is_not_nil(); } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand"); + } }; template<> inline bool can_cast_expr(const exprt &base) @@ -1121,6 +1216,11 @@ inline code_returnt &to_code_return(codet &code) return static_cast(code); } +inline void validate_expr(const code_returnt &x) +{ + validate_operands(x, 1, "return must have one operand"); +} + /// \ref codet representation of a label for branch targets. class code_labelt:public codet { diff --git a/src/util/validate_code.cpp b/src/util/validate_code.cpp index 9123ad6680d..9fcfc73b504 100644 --- a/src/util/validate_code.cpp +++ b/src/util/validate_code.cpp @@ -31,6 +31,18 @@ void call_on_code(const codet &code, Args &&... args) { CALL_ON_CODE(code_declt); } + else if(code.get_statement() == ID_dead) + { + CALL_ON_CODE(code_deadt); + } + else if(code.get_statement() == ID_function_call) + { + CALL_ON_CODE(code_function_callt); + } + else if(code.get_statement() == ID_return) + { + CALL_ON_CODE(code_returnt); + } else { #ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS diff --git a/unit/Makefile b/unit/Makefile index bc325db5c0f..f21996324c9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -15,6 +15,11 @@ SRC += analyses/ai/ai.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ compound_block_locations.cpp \ + goto-programs/goto_program_assume.cpp \ + goto-programs/goto_program_dead.cpp \ + goto-programs/goto_program_declaration.cpp \ + goto-programs/goto_program_function_call.cpp \ + goto-programs/goto_program_goto_target.cpp \ goto-programs/goto_trace_output.cpp \ goto-symex/ssa_equation.cpp \ interpreter/interpreter.cpp \ diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp new file mode 100644 index 00000000000..20d988f78be --- /dev/null +++ b/unit/goto-programs/goto_program_assume.cpp @@ -0,0 +1,64 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + + \*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of well-formed assert/assume codes", + "[core][goto-programs][validate]") +{ + GIVEN("A program with one assumption") + { + symbol_tablet symbol_table; + const typet type1 = signedbv_typet(32); + symbolt symbol; + irep_idt symbol_name = "a"; + symbol.name = symbol_name; + symbol_exprt varx(symbol_name, type1); + exprt val10 = from_integer(10, type1); + binary_relation_exprt x_le_10(varx, ID_le, val10); + + goto_functiont goto_function; + auto &instructions = goto_function.body.instructions; + instructions.emplace_back(goto_program_instruction_typet::ASSUME); + + symbol.type = type1; + symbol_table.insert(symbol); + namespacet ns(symbol_table); + instructions.back().make_assertion(x_le_10); + + WHEN("Instruction has no targets") + { + THEN("The consistency check succeeds") + { + goto_function.body.validate(ns, validation_modet::INVARIANT); + REQUIRE(true); + } + } + + WHEN("Instruction has a target") + { + instructions.back().targets.push_back(instructions.begin()); + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_function.body.validate(ns, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +} diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp new file mode 100644 index 00000000000..0d4f24c1eb6 --- /dev/null +++ b/unit/goto-programs/goto_program_dead.cpp @@ -0,0 +1,66 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + + \*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of well-formed symbol removing codes", + "[core][goto-programs][validate]") +{ + GIVEN("A program with one symbol removal") + { + symbol_tablet symbol_table; + const signedbv_typet type1(32); + + symbolt var_symbol; + irep_idt var_symbol_name = "a"; + var_symbol.type = type1; + var_symbol.name = var_symbol_name; + symbol_exprt var_a(var_symbol_name, type1); + + goto_functiont goto_function; + auto &instructions = goto_function.body.instructions; + instructions.emplace_back(goto_program_instruction_typet::DEAD); + code_deadt removal(var_a); + instructions.back().make_dead(); + instructions.back().code = removal; + + WHEN("Removing known symbol") + { + symbol_table.insert(var_symbol); + const namespacet ns(symbol_table); + + THEN("The consistency check succeeds") + { + goto_function.body.validate(ns, validation_modet::INVARIANT); + REQUIRE(true); + } + } + + WHEN("Removing unknown symbol") + { + const namespacet ns(symbol_table); + + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_function.body.validate(ns, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +} diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp new file mode 100644 index 00000000000..a1b111f8d92 --- /dev/null +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -0,0 +1,65 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + + \*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of well-formed declaration codes", + "[core][goto-programs][validate]") +{ + GIVEN("A program with one declaration") + { + symbol_tablet symbol_table; + const signedbv_typet type1(32); + + symbolt var_symbol; + irep_idt var_symbol_name = "a"; + var_symbol.type = type1; + var_symbol.name = var_symbol_name; + symbol_exprt var_a(var_symbol_name, type1); + + goto_functiont goto_function; + auto &instructions = goto_function.body.instructions; + instructions.emplace_back(goto_program_instruction_typet::DECL); + code_declt declaration(var_a); + instructions.back().make_decl(declaration); + + WHEN("Declaring known symbol") + { + symbol_table.insert(var_symbol); + const namespacet ns(symbol_table); + + THEN("The consistency check succeeds") + { + goto_function.body.validate(ns, validation_modet::INVARIANT); + REQUIRE(true); + } + } + + WHEN("Declaring unknown symbol") + { + const namespacet ns(symbol_table); + + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_function.body.validate(ns, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +} diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp new file mode 100644 index 00000000000..a86fbf0e98f --- /dev/null +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -0,0 +1,84 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + + \*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of well-formed function call codes", + "[core][goto-programs][validate]") +{ + GIVEN("A program with one function call") + { + symbol_tablet symbol_table; + const signedbv_typet type1(32); + const signedbv_typet type2(64); + const code_typet code_type({}, type1); + + symbolt var_symbol; + irep_idt var_symbol_name = "a"; + var_symbol.name = var_symbol_name; + symbol_exprt var_a(var_symbol_name, type1); + + symbolt var_symbol2; + irep_idt var_symbol_name2 = "b"; + var_symbol2.name = var_symbol_name2; + symbol_exprt var_b(var_symbol_name2, type2); + + symbolt fun_symbol; + irep_idt fun_symbol_name = "foo"; + fun_symbol.name = fun_symbol_name; + symbol_exprt fun_foo(fun_symbol_name, code_type); + + goto_functiont goto_function; + auto &instructions = goto_function.body.instructions; + instructions.emplace_back(goto_program_instruction_typet::FUNCTION_CALL); + + var_symbol.type = type1; + var_symbol2.type = type2; + fun_symbol.type = type1; + symbol_table.insert(var_symbol); + symbol_table.insert(var_symbol2); + symbol_table.insert(fun_symbol); + namespacet ns(symbol_table); + + WHEN("Return type matches") + { + code_function_callt function_call(var_a, fun_foo, {}); + instructions.back().make_function_call(function_call); + REQUIRE(instructions.back().code.get_statement() == ID_function_call); + + THEN("The consistency check succeeds") + { + goto_function.body.validate(ns, validation_modet::INVARIANT); + REQUIRE(true); + } + } + + WHEN("Return type differs from function type") + { + code_function_callt function_call(var_b, fun_foo, {}); + instructions.back().make_function_call(function_call); + + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_function.body.validate(ns, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +} diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp new file mode 100644 index 00000000000..53ee02bafee --- /dev/null +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -0,0 +1,67 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + + \*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of well-formed goto codes", + "[core][goto-programs][validate]") +{ + GIVEN("A program with one assertion") + { + symbol_tablet symbol_table; + const typet type1 = signedbv_typet(32); + symbolt symbol; + irep_idt symbol_name = "a"; + symbol.name = symbol_name; + symbol_exprt varx(symbol_name, type1); + exprt val10 = from_integer(10, type1); + binary_relation_exprt x_le_10(varx, ID_le, val10); + + goto_functiont goto_function; + auto &instructions = goto_function.body.instructions; + instructions.emplace_back(goto_program_instruction_typet::ASSERT); + instructions.back().make_assertion(x_le_10); + + instructions.emplace_back(goto_program_instruction_typet::GOTO); + instructions.back().make_goto(instructions.begin()); + + symbol.type = type1; + symbol_table.insert(symbol); + namespacet ns(symbol_table); + + WHEN("Target is a target") + { + instructions.front().target_number = 1; + THEN("The consistency check succeeds") + { + goto_function.body.validate(ns, validation_modet::INVARIANT); + REQUIRE(true); + } + } + + WHEN("Target is not a target") + { + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_function.body.validate(ns, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +}