From e5e7f36bcd58b4048b35fcaf0ab4ec7a65b80102 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 28 May 2024 03:39:23 -0700 Subject: [PATCH] extract transition_systemt::inputs and ::state_variables This extracts to replicated methods that identify the inputs and the state variables of the transition system. --- src/ebmc/liveness_to_safety.cpp | 17 +------ src/ebmc/random_traces.cpp | 80 +-------------------------------- src/ebmc/transition_system.cpp | 50 +++++++++++++++++++++ src/ebmc/transition_system.h | 3 ++ 4 files changed, 57 insertions(+), 93 deletions(-) diff --git a/src/ebmc/liveness_to_safety.cpp b/src/ebmc/liveness_to_safety.cpp index f4e78722a..fb945dff0 100644 --- a/src/ebmc/liveness_to_safety.cpp +++ b/src/ebmc/liveness_to_safety.cpp @@ -120,23 +120,10 @@ void liveness_to_safetyt::operator()() if(!properties.requires_lasso_constraints()) return; // no - irep_idt module_identifier = transition_system.main_symbol->name; - // gather the state variables - const namespacet ns(transition_system.symbol_table); + state_vars = transition_system.state_variables(); - const auto &symbol_module_map = - transition_system.symbol_table.symbol_module_map; - auto lower = symbol_module_map.lower_bound(module_identifier); - auto upper = symbol_module_map.upper_bound(module_identifier); - - for(auto it = lower; it != upper; it++) - { - const symbolt &symbol = ns.lookup(it->second); - - if(symbol.is_state_var) - state_vars.push_back(symbol.symbol_expr()); - } + const namespacet ns(transition_system.symbol_table); // create 'loop' shadow symbols for the state variables for(auto &symbol_expr : state_vars) diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp index 8def46279..8fd6838d1 100644 --- a/src/ebmc/random_traces.cpp +++ b/src/ebmc/random_traces.cpp @@ -84,8 +84,6 @@ class random_tracest constant_exprt random_value(const typet &); - symbolst inputs() const; - symbolst state_variables() const; symbolst remove_constrained(const symbolst &) const; void @@ -440,80 +438,6 @@ constant_exprt random_tracest::random_value(const typet &type) /*******************************************************************\ -Function: random_tracest::inputs - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -random_tracest::symbolst random_tracest::inputs() const -{ - symbolst inputs; - - const auto &module_symbol = *transition_system.main_symbol; - - if(module_symbol.type.id() != ID_module) - throw ebmc_errort() << "expected a module but got " - << module_symbol.type.id(); - - const auto &ports = module_symbol.type.find(ID_ports); - - // filter out the inputs - for(auto &port : static_cast(ports).operands()) - { - DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol"); - if(port.get_bool(ID_input) && !port.get_bool(ID_output)) - { - symbol_exprt input_symbol(port.get(ID_identifier), port.type()); - input_symbol.add_source_location() = port.source_location(); - inputs.push_back(std::move(input_symbol)); - } - } - - return inputs; -} - -/*******************************************************************\ - -Function: random_tracest::state_variables - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -random_tracest::symbolst random_tracest::state_variables() const -{ - symbolst state_variables; - - const auto &module_symbol = *transition_system.main_symbol; - const namespacet ns(transition_system.symbol_table); - - const auto &symbol_module_map = - transition_system.symbol_table.symbol_module_map; - auto lower = symbol_module_map.lower_bound(module_symbol.name); - auto upper = symbol_module_map.upper_bound(module_symbol.name); - - for(auto it = lower; it != upper; it++) - { - const symbolt &symbol = ns.lookup(it->second); - - if(symbol.is_state_var) - state_variables.push_back(symbol.symbol_expr()); - } - - return state_variables; -} - -/*******************************************************************\ - Function: random_tracest::remove_constrained Inputs: @@ -665,12 +589,12 @@ void random_tracest::operator()( ns, true); - auto inputs = this->inputs(); + auto inputs = transition_system.inputs(); if(inputs.empty()) throw ebmc_errort() << "module does not have inputs"; - auto state_variables = this->state_variables(); + auto state_variables = transition_system.state_variables(); message.statistics() << "Found " << inputs.size() << " input(s) and " << state_variables.size() << " state variable(s)" diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp index 3ebacd496..dcbf8d54b 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -368,3 +368,53 @@ int show_symbol_table( return get_transition_system( cmdline, message_handler, dummy_transition_system); } + +std::vector transition_systemt::state_variables() const +{ + std::vector state_variables; + + const auto &module_symbol = *main_symbol; + const namespacet ns(symbol_table); + + const auto &symbol_module_map = symbol_table.symbol_module_map; + auto lower = symbol_module_map.lower_bound(module_symbol.name); + auto upper = symbol_module_map.upper_bound(module_symbol.name); + + for(auto it = lower; it != upper; it++) + { + const symbolt &symbol = ns.lookup(it->second); + + if(symbol.is_state_var) + state_variables.push_back(symbol.symbol_expr()); + } + + return state_variables; +} + +std::vector transition_systemt::inputs() const +{ + std::vector inputs; + + const auto &module_symbol = *main_symbol; + + DATA_INVARIANT( + module_symbol.type.id() == ID_module, "main_symbol must be module"); + + const auto &ports_irep = module_symbol.type.find(ID_ports); + + // filter out the inputs + auto &ports = static_cast(ports_irep).operands(); + for(auto &port : ports) + { + DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol"); + if(port.get_bool(ID_input) && !port.get_bool(ID_output)) + { + symbol_exprt input_symbol( + to_symbol_expr(port).get_identifier(), port.type()); + input_symbol.add_source_location() = port.source_location(); + inputs.push_back(std::move(input_symbol)); + } + } + + return inputs; +} diff --git a/src/ebmc/transition_system.h b/src/ebmc/transition_system.h index eb7501eb2..a2451632e 100644 --- a/src/ebmc/transition_system.h +++ b/src/ebmc/transition_system.h @@ -29,6 +29,9 @@ class transition_systemt transt trans_expr; // transition system expression void output(std::ostream &) const; + + std::vector state_variables() const; + std::vector inputs() const; }; transition_systemt get_transition_system(const cmdlinet &, message_handlert &);