From 7ab1ab50443374ab6341d97fe933037f1a3cc35d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 16 Jul 2025 15:47:29 -0700 Subject: [PATCH] BMC: looping constraint must consider all inputs The SMV top-level main module does not have explicit inputs or output. This change adds all inputs to the list of variables that are compared when creating the lasso condition. --- .../ebmc/SVA-LTL/lasso1-show-formula.desc | 2 +- regression/smv/LTL/smv_ltlspec_F5.desc | 6 +++--- regression/smv/LTL/smv_ltlspec_F5.smv | 2 +- regression/smv/LTL/smv_ltlspec_F7.desc | 8 +++++++ regression/smv/LTL/smv_ltlspec_F7.smv | 6 ++++++ src/trans-word-level/lasso.cpp | 21 +++---------------- 6 files changed, 22 insertions(+), 23 deletions(-) create mode 100644 regression/smv/LTL/smv_ltlspec_F7.desc create mode 100644 regression/smv/LTL/smv_ltlspec_F7.smv diff --git a/regression/ebmc/SVA-LTL/lasso1-show-formula.desc b/regression/ebmc/SVA-LTL/lasso1-show-formula.desc index 551c72879..79caed9c3 100644 --- a/regression/ebmc/SVA-LTL/lasso1-show-formula.desc +++ b/regression/ebmc/SVA-LTL/lasso1-show-formula.desc @@ -3,6 +3,6 @@ lasso1.sv --bound 1 --show-formula ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) lasso::1-back-to-0 ⇔ \(.*counter@1 = .*counter@0 ∧ .*clock@1 ⇔ .*clock@0\)$ +^\(\d+\) lasso::1-back-to-0 ⇔ \(.*clock@1 ⇔ .*clock@0 ∧ .*counter@1 = .*counter@0\)$ -- -- diff --git a/regression/smv/LTL/smv_ltlspec_F5.desc b/regression/smv/LTL/smv_ltlspec_F5.desc index 952a884b6..6dd404fba 100644 --- a/regression/smv/LTL/smv_ltlspec_F5.desc +++ b/regression/smv/LTL/smv_ltlspec_F5.desc @@ -1,10 +1,10 @@ -KNOWNBUG +CORE smv_ltlspec_F5.smv ---bound 3 --numbered-trace +--bound 1 --numbered-trace ^\[spec1\] F \(!some_input \& X !some_input\): REFUTED$ +^Counterexample with 2 states:$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -The BMC engine gives the wrong answer. diff --git a/regression/smv/LTL/smv_ltlspec_F5.smv b/regression/smv/LTL/smv_ltlspec_F5.smv index dd929f90a..d65f4ea4f 100644 --- a/regression/smv/LTL/smv_ltlspec_F5.smv +++ b/regression/smv/LTL/smv_ltlspec_F5.smv @@ -3,5 +3,5 @@ MODULE main VAR some_input : boolean; -- Expected to fail --- The shortest loop is FALSE, FALSE +-- The shortest loop is FALSE, FALSE or TRUE, TRUE LTLSPEC F (!some_input & X !some_input) diff --git a/regression/smv/LTL/smv_ltlspec_F7.desc b/regression/smv/LTL/smv_ltlspec_F7.desc new file mode 100644 index 000000000..ae735bb83 --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_F7.desc @@ -0,0 +1,8 @@ +CORE +smv_ltlspec_F7.smv +--bound 1 --show-formula +^\(1\) lasso::1-back-to-0 ⇔ \(smv::main::var::some_input@1 = smv::main::var::some_input@0\)$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/LTL/smv_ltlspec_F7.smv b/regression/smv/LTL/smv_ltlspec_F7.smv new file mode 100644 index 000000000..8a9629d7f --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_F7.smv @@ -0,0 +1,6 @@ +MODULE main + +VAR some_input : 1..3; + +-- Expected to fail +LTLSPEC F (some_input >= 2) diff --git a/src/trans-word-level/lasso.cpp b/src/trans-word-level/lasso.cpp index c15e5a64e..b13efb1eb 100644 --- a/src/trans-word-level/lasso.cpp +++ b/src/trans-word-level/lasso.cpp @@ -95,7 +95,7 @@ void lasso_constraints( std::vector variables_to_compare; - // Gather the state variables. + // Gather the state variables, and the inputs. const symbol_tablet &symbol_table = ns.get_symbol_table(); auto lower = symbol_table.symbol_module_map.lower_bound(module_identifier); auto upper = symbol_table.symbol_module_map.upper_bound(module_identifier); @@ -104,26 +104,11 @@ void lasso_constraints( { const symbolt &symbol = ns.lookup(it->second); - if(symbol.is_state_var) + if(symbol.is_state_var || symbol.is_input) variables_to_compare.push_back(symbol.symbol_expr()); } - // gather the top-level inputs - const auto &module_symbol = ns.lookup(module_identifier); - DATA_INVARIANT(module_symbol.type.id() == ID_module, "expected a module"); - const auto &ports = module_symbol.type.find(ID_ports); - - 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(); - variables_to_compare.push_back(std::move(input_symbol)); - } - } - + // Create the constraint for(mp_integer i = 1; i < no_timeframes; ++i) { for(mp_integer k = 0; k < i; ++k)