From bc281cc199c6b80a1ab424e233d93fd9a5b0e882 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Wed, 5 Dec 2018 10:43:25 +0000 Subject: [PATCH 1/3] Symbol consistency between goto programs and symbol table Iterate over all symbols in a goto program and for each one check that it is present in the symbol table as well. Includes a unit test for the check. --- src/goto-programs/goto_function.h | 13 ++++ src/goto-programs/goto_program.cpp | 23 +++++++ unit/Makefile | 1 + .../goto_program_table_consistency.cpp | 67 +++++++++++++++++++ 4 files changed, 104 insertions(+) create mode 100644 unit/goto-programs/goto_program_table_consistency.cpp diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index f9e1d7f99db..a73d538c8fb 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -16,6 +16,7 @@ Date: May 2018 #include +#include #include #include "goto_program.h" @@ -118,6 +119,18 @@ class goto_functiont void validate(const namespacet &ns, const validation_modet vm) const { body.validate(ns, vm); + + find_symbols_sett typetags; + find_type_symbols(type, typetags); + const symbolt *symbol; + for(const auto &identifier : typetags) + { + DATA_CHECK( + vm, + !ns.lookup(identifier, symbol), + id2string(identifier) + " not found"); + } + validate_full_type(type, ns, vm); } }; diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index e718a7b7a68..e34eaa159c9 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -677,6 +678,26 @@ void goto_programt::instructiont::validate( validate_full_expr(guard, ns, vm); const symbolt *table_symbol; + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + !ns.lookup(function, table_symbol), + id2string(function) + " not found", + source_location); + + auto expr_symbol_finder = [&](const exprt &e) { + find_symbols_sett typetags; + find_type_symbols(e.type(), typetags); + find_symbols(e, typetags); + const symbolt *symbol; + for(const auto &identifier : typetags) + { + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + !ns.lookup(identifier, symbol), + id2string(identifier) + " not found", + source_location); + } + }; switch(type) { @@ -708,6 +729,7 @@ void goto_programt::instructiont::validate( targets.empty(), "assert instruction should not have a target", source_location); + std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder); break; case OTHER: break; @@ -772,6 +794,7 @@ void goto_programt::instructiont::validate( code.get_statement() == ID_function_call, "function call instruction should contain a call statement", source_location); + std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder); break; case THROW: break; diff --git a/unit/Makefile b/unit/Makefile index f21996324c9..cc5c68b4839 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,6 +20,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/goto_program_declaration.cpp \ goto-programs/goto_program_function_call.cpp \ goto-programs/goto_program_goto_target.cpp \ + goto-programs/goto_program_table_consistency.cpp \ goto-programs/goto_trace_output.cpp \ goto-symex/ssa_equation.cpp \ interpreter/interpreter.cpp \ diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp new file mode 100644 index 00000000000..3509a408867 --- /dev/null +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -0,0 +1,67 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + Author: Diffblue Ltd. + + \*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of consistent program/table pair", + "[core][goto-programs][validate]") +{ + GIVEN("A program with one assertion") + { + symbol_tablet symbol_table; + const typet type = signedbv_typet(32); + symbolt symbol; + irep_idt symbol_name = "a"; + symbol.name = symbol_name; + symbol_exprt varx(symbol_name, type); + symbolt function_symbol; + irep_idt function_name = "fun"; + function_symbol.name = function_name; + + exprt val10 = from_integer(10, type); + 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.back().function = function_symbol.name; + + symbol_table.insert(function_symbol); + WHEN("Symbol table has the right symbol") + { + symbol.type = type; + symbol_table.insert(symbol); + const namespacet ns(symbol_table); + THEN("The consistency check succeeds") + { + goto_function.validate(ns, validation_modet::INVARIANT); + REQUIRE(true); + } + } + WHEN("Symbol table does not have the symbol") + { + const namespacet ns(symbol_table); + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_function.validate(ns, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +} From a0289a7dbca8919ea7cdc4f9ef03b0bcc469414d Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Wed, 5 Dec 2018 10:44:37 +0000 Subject: [PATCH 2/3] Function type consistency between goto programs and symbol table A simple iteration over goto-functions to check that it's base type is the same as the one stored in the symbol table. Includes a unit test. --- src/goto-programs/goto_functions.h | 9 +++ unit/Makefile | 1 + .../goto_model_function_type_consistency.cpp | 67 +++++++++++++++++++ 3 files changed, 77 insertions(+) create mode 100644 unit/goto-programs/goto_model_function_type_consistency.cpp diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index a5fa9c0094f..f03933466ea 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -127,6 +127,15 @@ class goto_functionst for(const auto &entry : function_map) { const goto_functiont &goto_function = entry.second; + const auto &function_name = entry.first; + + DATA_CHECK( + vm, + goto_function.type == ns.lookup(function_name).type, + id2string(function_name) + " type inconsistency\ngoto program type: " + + goto_function.type.id_string() + + "\nsymbol table type: " + ns.lookup(function_name).type.id_string()); + goto_function.validate(ns, vm); } } diff --git a/unit/Makefile b/unit/Makefile index cc5c68b4839..3f426a4953f 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -15,6 +15,7 @@ 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_model_function_type_consistency.cpp \ goto-programs/goto_program_assume.cpp \ goto-programs/goto_program_dead.cpp \ goto-programs/goto_program_declaration.cpp \ diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp new file mode 100644 index 00000000000..69cc5265819 --- /dev/null +++ b/unit/goto-programs/goto_model_function_type_consistency.cpp @@ -0,0 +1,67 @@ +/*******************************************************************\ + + Module: Unit tests for goto_model::validate + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of consistent program/table pair (function type)", + "[core][goto-programs][validate]") +{ + GIVEN("A model with one function") + { + const typet type1 = signedbv_typet(32); + const typet type2 = signedbv_typet(64); + code_typet fun_type1({}, type1); + code_typet fun_type2({}, type2); + + symbolt function_symbol; + irep_idt function_symbol_name = "foo"; + function_symbol.name = function_symbol_name; + + goto_modelt goto_model; + goto_model.goto_functions.function_map[function_symbol.name] = + goto_functiont(); + goto_model.goto_functions.function_map[function_symbol.name].type = + fun_type1; + + WHEN("Symbol table has the right type") + { + function_symbol.type = fun_type1; + goto_model.symbol_table.insert(function_symbol); + + THEN("The consistency check succeeds") + { + goto_model.validate(validation_modet::INVARIANT); + + REQUIRE(true); + } + } + + WHEN("Symbol table has the wrong type") + { + function_symbol.type = fun_type2; + goto_model.symbol_table.insert(function_symbol); + + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_model.validate(validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +} From 60a833e92779f45500abbd38234cd580b09eb901 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Wed, 5 Dec 2018 10:50:55 +0000 Subject: [PATCH 3/3] Program table symbol type consistency Look up the symbol id in symbol table and call base_type_eq on every symbol expression in guard and code whenever relevant. Includes a unit test. Also fixes unit tests that these new checks brake. --- src/goto-programs/goto_program.cpp | 24 ++++++ unit/Makefile | 1 + unit/goto-programs/goto_program_assume.cpp | 5 ++ unit/goto-programs/goto_program_dead.cpp | 6 ++ .../goto_program_declaration.cpp | 6 ++ .../goto_program_function_call.cpp | 3 +- .../goto_program_goto_target.cpp | 7 ++ ..._program_symbol_type_table_consistency.cpp | 75 +++++++++++++++++++ 8 files changed, 126 insertions(+), 1 deletion(-) create mode 100644 unit/goto-programs/goto_program_symbol_type_table_consistency.cpp diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index e34eaa159c9..fd192b0e3f0 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -699,6 +700,25 @@ void goto_programt::instructiont::validate( } }; + auto ¤t_source_location = source_location; + auto type_finder = + [&ns, vm, &table_symbol, ¤t_source_location](const exprt &e) { + if(e.id() == ID_symbol) + { + const auto &goto_symbol_expr = to_symbol_expr(e); + const auto &goto_id = goto_symbol_expr.get_identifier(); + + if(!ns.lookup(goto_id, table_symbol)) + DATA_CHECK_WITH_DIAGNOSTICS( + vm, + base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns), + id2string(goto_id) + " type inconsistency\n" + + "goto program type: " + goto_symbol_expr.type().id_string() + + "\n" + "symbol table type: " + table_symbol->type.id_string(), + current_source_location); + } + }; + switch(type) { case NO_INSTRUCTION_TYPE: @@ -729,7 +749,9 @@ void goto_programt::instructiont::validate( targets.empty(), "assert instruction should not have a target", source_location); + std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder); + std::for_each(guard.depth_begin(), guard.depth_end(), type_finder); break; case OTHER: break; @@ -794,7 +816,9 @@ void goto_programt::instructiont::validate( code.get_statement() == ID_function_call, "function call instruction should contain a call statement", source_location); + std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder); + std::for_each(code.depth_begin(), code.depth_end(), type_finder); break; case THROW: break; diff --git a/unit/Makefile b/unit/Makefile index 3f426a4953f..d0bfac443b5 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -21,6 +21,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/goto_program_declaration.cpp \ goto-programs/goto_program_function_call.cpp \ goto-programs/goto_program_goto_target.cpp \ + goto-programs/goto_program_symbol_type_table_consistency.cpp \ goto-programs/goto_program_table_consistency.cpp \ goto-programs/goto_trace_output.cpp \ goto-symex/ssa_equation.cpp \ diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp index 20d988f78be..bfe8d82519f 100644 --- a/unit/goto-programs/goto_program_assume.cpp +++ b/unit/goto-programs/goto_program_assume.cpp @@ -19,6 +19,9 @@ SCENARIO( symbol_tablet symbol_table; const typet type1 = signedbv_typet(32); symbolt symbol; + symbolt fun_symbol; + irep_idt fun_name = "foo"; + fun_symbol.name = fun_name; irep_idt symbol_name = "a"; symbol.name = symbol_name; symbol_exprt varx(symbol_name, type1); @@ -31,8 +34,10 @@ SCENARIO( symbol.type = type1; symbol_table.insert(symbol); + symbol_table.insert(fun_symbol); namespacet ns(symbol_table); instructions.back().make_assertion(x_le_10); + instructions.back().function = fun_name; WHEN("Instruction has no targets") { diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp index 0d4f24c1eb6..5ca70a6bdf9 100644 --- a/unit/goto-programs/goto_program_dead.cpp +++ b/unit/goto-programs/goto_program_dead.cpp @@ -19,6 +19,10 @@ SCENARIO( symbol_tablet symbol_table; const signedbv_typet type1(32); + symbolt fun_symbol; + irep_idt fun_name = "foo"; + fun_symbol.name = fun_name; + symbolt var_symbol; irep_idt var_symbol_name = "a"; var_symbol.type = type1; @@ -31,6 +35,8 @@ SCENARIO( code_deadt removal(var_a); instructions.back().make_dead(); instructions.back().code = removal; + instructions.back().function = fun_name; + symbol_table.insert(fun_symbol); WHEN("Removing known symbol") { diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp index a1b111f8d92..73bdf2dbc2e 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -19,6 +19,10 @@ SCENARIO( symbol_tablet symbol_table; const signedbv_typet type1(32); + symbolt fun_symbol; + irep_idt fun_name = "foo"; + fun_symbol.name = fun_name; + symbolt var_symbol; irep_idt var_symbol_name = "a"; var_symbol.type = type1; @@ -30,6 +34,8 @@ SCENARIO( instructions.emplace_back(goto_program_instruction_typet::DECL); code_declt declaration(var_a); instructions.back().make_decl(declaration); + instructions.back().function = fun_name; + symbol_table.insert(fun_symbol); WHEN("Declaring known symbol") { diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index a86fbf0e98f..ab3cf0d6150 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -34,15 +34,16 @@ SCENARIO( symbolt fun_symbol; irep_idt fun_symbol_name = "foo"; fun_symbol.name = fun_symbol_name; + fun_symbol.type = code_type; 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); + instructions.back().function = fun_symbol_name; 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); diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index 53ee02bafee..6dabf0e6e74 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -18,6 +18,10 @@ SCENARIO( { symbol_tablet symbol_table; const typet type1 = signedbv_typet(32); + symbolt fun_symbol; + irep_idt fun_name = "foo"; + fun_symbol.name = fun_name; + symbolt symbol; irep_idt symbol_name = "a"; symbol.name = symbol_name; @@ -29,12 +33,15 @@ SCENARIO( auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_program_instruction_typet::ASSERT); instructions.back().make_assertion(x_le_10); + instructions.back().function = fun_name; instructions.emplace_back(goto_program_instruction_typet::GOTO); instructions.back().make_goto(instructions.begin()); + instructions.back().function = fun_name; symbol.type = type1; symbol_table.insert(symbol); + symbol_table.insert(fun_symbol); namespacet ns(symbol_table); WHEN("Target is a target") diff --git a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp new file mode 100644 index 00000000000..8ec80923125 --- /dev/null +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -0,0 +1,75 @@ +/*******************************************************************\ + + Module: Unit tests for goto_program::validate + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "Validation of consistent program/table pair (type-wise)", + "[core][goto-programs][validate]") +{ + GIVEN("A program with one assertion") + { + symbol_tablet symbol_table; + const typet type1 = signedbv_typet(32); + const typet type2 = signedbv_typet(64); + symbolt symbol; + irep_idt symbol_name = "a"; + symbol.name = symbol_name; + symbol_exprt varx(symbol_name, type1); + symbolt function_symbol; + irep_idt function_name = "fun"; + function_symbol.name = function_name; + + 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.back().function = function_symbol.name; + + symbol_table.insert(function_symbol); + WHEN("Symbol table has the right symbol type") + { + symbol.type = type1; + symbol_table.insert(symbol); + const namespacet ns(symbol_table); + + THEN("The consistency check succeeds") + { + goto_function.validate(ns, validation_modet::INVARIANT); + + REQUIRE(true); + } + } + + WHEN("Symbol table has the wrong symbol type") + { + symbol.type = type2; + symbol_table.insert(symbol); + const namespacet ns(symbol_table); + + THEN("The consistency check fails") + { + bool caught = false; + try + { + goto_function.validate(ns, validation_modet::EXCEPTION); + } + catch(incorrect_goto_program_exceptiont &e) + { + caught = true; + } + REQUIRE(caught); + } + } + } +}