Well-formedness check for decl and dead instructions
Check that declared/removed symbol is known and the statement is valid.
This commit is contained in:
parent
093310be33
commit
5aa708a987
|
@ -676,6 +676,8 @@ 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:
|
||||
|
@ -713,8 +715,30 @@ 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:
|
||||
break;
|
||||
|
|
|
@ -371,6 +371,19 @@ public:
|
|||
{
|
||||
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<code_declt>(const exprt &base)
|
||||
|
@ -430,6 +443,21 @@ public:
|
|||
{
|
||||
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<code_deadt>(const exprt &base)
|
||||
|
|
|
@ -31,6 +31,10 @@ 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
|
||||
{
|
||||
#ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS
|
||||
|
|
|
@ -15,6 +15,8 @@ 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_dead.cpp \
|
||||
goto-programs/goto_program_declaration.cpp \
|
||||
goto-programs/goto_trace_output.cpp \
|
||||
goto-symex/ssa_equation.cpp \
|
||||
interpreter/interpreter.cpp \
|
||||
|
|
|
@ -0,0 +1,66 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Unit tests for goto_program::validate
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
#include <goto-programs/goto_function.h>
|
||||
#include <testing-utils/catch.hpp>
|
||||
#include <util/arith_tools.h>
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
|
@ -0,0 +1,65 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Unit tests for goto_program::validate
|
||||
|
||||
Author: Diffblue Ltd.
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
#include <goto-programs/goto_function.h>
|
||||
#include <testing-utils/catch.hpp>
|
||||
#include <util/arith_tools.h>
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue