diff --git a/CHANGELOG b/CHANGELOG index 5eefc0add..963968718 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,6 +1,8 @@ # EBMC 5.4 * BMC: Cadical support with --cadical +* BMC: iterative constraint strengthening is now default; + use --bmc-with-assumptions to re-enable the previous algorithm. # EBMC 5.3 diff --git a/regression/ebmc/assumptions/assume2.bmc-with-assumptions.desc b/regression/ebmc/assumptions/assume2.bmc-with-assumptions.desc new file mode 100644 index 000000000..e6046b824 --- /dev/null +++ b/regression/ebmc/assumptions/assume2.bmc-with-assumptions.desc @@ -0,0 +1,8 @@ +CORE +assume2.sv +--bound 0 --bmc-with-assumptions +^\[main\.a1\] assume always 10 <= main\.a && main\.a <= 100: ASSUMED$ +^\[main\.p1\] always main\.a != 200: PROVED up to bound 0$ +^\[main\.p2\] always main.a != 20: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/ebmc/example4_trace/test.desc b/regression/ebmc/example4_trace/test.desc index e4b14f44f..0d8fbc117 100644 --- a/regression/ebmc/example4_trace/test.desc +++ b/regression/ebmc/example4_trace/test.desc @@ -3,6 +3,6 @@ example4.sv --bound 10 --trace ^\[counter\.assert\.1\] .* PROVED up to bound 10$ ^\[counter\.assert\.2\] .* REFUTED$ -^ counter\.state = 254 \(11111110\)$ +^ counter\.state = \d+ \([01]+\)$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/verilog/functioncall/functioncall2.desc b/regression/verilog/functioncall/functioncall2.desc index ce377110c..b73c415b7 100644 --- a/regression/verilog/functioncall/functioncall2.desc +++ b/regression/verilog/functioncall/functioncall2.desc @@ -3,6 +3,6 @@ functioncall2.v --module main --bound 1 ^EXIT=0$ ^SIGNAL=0$ -^UNSAT: No counterexample found within bound$ +^UNSAT: .*$ -- ^warning: ignoring diff --git a/regression/verilog/functioncall/functioncall3.desc b/regression/verilog/functioncall/functioncall3.desc index effdedbf2..0edd47a6f 100644 --- a/regression/verilog/functioncall/functioncall3.desc +++ b/regression/verilog/functioncall/functioncall3.desc @@ -3,6 +3,6 @@ functioncall3.v --module main --bound 0 ^EXIT=0$ ^SIGNAL=0$ -^UNSAT: No counterexample found within bound$ +^UNSAT: .*$ -- ^warning: ignoring diff --git a/regression/verilog/functioncall/functioncall4.desc b/regression/verilog/functioncall/functioncall4.desc index 2c9db11df..564d66096 100644 --- a/regression/verilog/functioncall/functioncall4.desc +++ b/regression/verilog/functioncall/functioncall4.desc @@ -3,7 +3,7 @@ functioncall4.v --module main --bound 0 ^EXIT=0$ ^SIGNAL=0$ -^UNSAT: No counterexample found within bound$ +^UNSAT: .*$ -- ^warning: ignoring -- diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp index 68f93133a..ebaa553a0 100644 --- a/src/ebmc/bmc.cpp +++ b/src/ebmc/bmc.cpp @@ -17,9 +17,184 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +void bmc_with_assumptions( + std::size_t bound, + const transition_systemt &transition_system, + ebmc_propertiest &properties, + decision_proceduret &solver, + message_handlert &message_handler) +{ + messaget message(message_handler); + const namespacet ns(transition_system.symbol_table); + + // Use assumptions to check the properties separately + + for(auto &property : properties.properties) + { + if(property.is_disabled() || property.is_failure() || property.is_assumed()) + { + continue; + } + + message.status() << "Checking " << property.name << messaget::eom; + + auto assumption = not_exprt{conjunction(property.timeframe_handles)}; + + decision_proceduret::resultt dec_result = solver(assumption); + + switch(dec_result) + { + case decision_proceduret::resultt::D_SATISFIABLE: + if(property.is_exists_path()) + { + property.proved(); + message.result() << "SAT: path found" << messaget::eom; + } + else // universal path property + { + property.refuted(); + message.result() << "SAT: counterexample found" << messaget::eom; + } + + property.witness_trace = compute_trans_trace( + property.timeframe_handles, + solver, + bound + 1, + ns, + transition_system.main_symbol->name); + break; + + case decision_proceduret::resultt::D_UNSATISFIABLE: + if(property.is_exists_path()) + { + message.result() << "UNSAT: No path found within bound" + << messaget::eom; + property.refuted_with_bound(bound); + } + else // universal path property + { + message.result() << "UNSAT: No counterexample found within bound" + << messaget::eom; + property.proved_with_bound(bound); + } + break; + + case decision_proceduret::resultt::D_ERROR: + message.error() << "Error from decision procedure" << messaget::eom; + property.failure(); + break; + + default: + property.failure(); + throw ebmc_errort() << "Unexpected result from decision procedure"; + } + } +} + +/// VMCAI 2009 Query-driven program testing, +/// "iterative constraint strengthening" +void bmc_with_iterative_constraint_strengthening( + std::size_t bound, + const transition_systemt &transition_system, + ebmc_propertiest &properties, + decision_proceduret &solver, + message_handlert &message_handler) +{ + messaget message(message_handler); + const namespacet ns(transition_system.symbol_table); + + auto trace_found = [&solver](const ebmc_propertiest::propertyt &property) + { + for(auto &h : property.timeframe_handles) + if(solver.get(h).is_false()) + return true; + return false; + }; + + while(true) + { + // At least one of the remaining properties + // should be falsified. + exprt::operandst disjuncts; + + for(auto &property : properties.properties) + { + if(property.is_unknown()) + { + for(auto &h : property.timeframe_handles) + disjuncts.push_back(not_exprt{h}); + } + } + + // This constraint is strenthened in each iteration. + solver.set_to_true(disjunction(disjuncts)); + + decision_proceduret::resultt dec_result = solver(); + + switch(dec_result) + { + case decision_proceduret::resultt::D_SATISFIABLE: + // Found a trace for at least one further property with unknown state + message.result() << "SAT: path found" << messaget::eom; + + for(auto &property : properties.properties) + { + if(property.is_unknown() && trace_found(property)) + { + if(property.is_exists_path()) + property.proved(); + else // universal path property + property.refuted(); + + property.witness_trace = compute_trans_trace( + property.timeframe_handles, + solver, + bound + 1, + ns, + transition_system.main_symbol->name); + } + } + break; // next iteration of while loop + + case decision_proceduret::resultt::D_UNSATISFIABLE: + message.result() << "UNSAT: No path found within bound" << messaget::eom; + + for(auto &property : properties.properties) + { + if(property.is_unknown()) + { + if(property.is_exists_path()) + property.refuted_with_bound(bound); + else // universal path property + property.proved_with_bound(bound); + } + } + return; + + case decision_proceduret::resultt::D_ERROR: + for(auto &property : properties.properties) + { + if(property.is_unknown()) + property.failure(); + } + message.error() << "Error from decision procedure" << messaget::eom; + return; + + default: + for(auto &property : properties.properties) + { + if(property.is_unknown()) + property.failure(); + } + throw ebmc_errort() << "Unexpected result from decision procedure"; + } + } +} + void bmc( std::size_t bound, bool convert_only, + bool bmc_with_assumptions, const transition_systemt &transition_system, ebmc_propertiest &properties, const ebmc_solver_factoryt &solver_factory, @@ -76,12 +251,25 @@ void bmc( if(convert_only) { + // At least one property must be violated in at least one + // timeframe. + exprt::operandst disjuncts; + for(const auto &property : properties.properties) { - if(!property.is_disabled()) - solver.set_to_false(conjunction(property.timeframe_handles)); + if(property.is_assumed()) + { + // already added as constraint above + } + else if(!property.is_disabled()) + { + for(auto &h : property.timeframe_handles) + disjuncts.push_back(not_exprt{h}); + } } + solver.set_to_true(disjunction(disjuncts)); + // Call decision_proceduret::dec_solve to finish the conversion // process. (void)solver(); @@ -93,69 +281,15 @@ void bmc( auto sat_start_time = std::chrono::steady_clock::now(); - // Use assumptions to check the properties separately - - for(auto &property : properties.properties) + if(bmc_with_assumptions) { - if( - property.is_disabled() || property.is_failure() || - property.is_assumed()) - { - continue; - } - - message.status() << "Checking " << property.name << messaget::eom; - - auto assumption = not_exprt{conjunction(property.timeframe_handles)}; - - decision_proceduret::resultt dec_result = solver(assumption); - - switch(dec_result) - { - case decision_proceduret::resultt::D_SATISFIABLE: - if(property.is_exists_path()) - { - property.proved(); - message.result() << "SAT: path found" << messaget::eom; - } - else // universal path property - { - property.refuted(); - message.result() << "SAT: counterexample found" << messaget::eom; - } - - property.witness_trace = compute_trans_trace( - property.timeframe_handles, - solver, - bound + 1, - ns, - transition_system.main_symbol->name); - break; - - case decision_proceduret::resultt::D_UNSATISFIABLE: - if(property.is_exists_path()) - { - message.result() << "UNSAT: No path found within bound" - << messaget::eom; - property.refuted_with_bound(bound); - } - else // universal path property - { - message.result() << "UNSAT: No counterexample found within bound" - << messaget::eom; - property.proved_with_bound(bound); - } - break; - - case decision_proceduret::resultt::D_ERROR: - message.error() << "Error from decision procedure" << messaget::eom; - property.failure(); - break; - - default: - property.failure(); - throw ebmc_errort() << "Unexpected result from decision procedure"; - } + ::bmc_with_assumptions( + bound, transition_system, properties, solver, message_handler); + } + else + { + ::bmc_with_iterative_constraint_strengthening( + bound, transition_system, properties, solver, message_handler); } auto sat_stop_time = std::chrono::steady_clock::now(); diff --git a/src/ebmc/bmc.h b/src/ebmc/bmc.h index 33536a67e..1cf51025e 100644 --- a/src/ebmc/bmc.h +++ b/src/ebmc/bmc.h @@ -22,6 +22,7 @@ class transition_systemt; void bmc( std::size_t bound, bool convert_only, + bool bmc_with_assumptions, const transition_systemt &, ebmc_propertiest &, const ebmc_solver_factoryt &, diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index cd3d14c1d..d6abed1e8 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -47,6 +47,7 @@ class ebmc_parse_optionst:public parse_options_baset "(compute-ct)(dot-netlist)(smv-netlist)(vcd):" "(random-traces)(trace-steps):(random-seed):(traces):" "(random-trace)(random-waveform)" + "(bmc-with-assumptions)" "(liveness-to-safety)" "I:D:(preprocess)(systemverilog)(vl2smv-extensions)" "(warn-implicit-nets)", diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index c90b73b4c..9123617d4 100644 --- a/src/ebmc/k_induction.cpp +++ b/src/ebmc/k_induction.cpp @@ -202,7 +202,8 @@ void k_inductiont::induction_base() bmc( k, - false, + false, // convert_only + false, // bmc_with_assumptions transition_system, properties, solver_factory, diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index d0b8373ad..6f645fb4b 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -80,9 +80,12 @@ property_checker_resultt word_level_bmc( if(properties.properties.empty()) throw "no properties"; + bool bmc_with_assumptions = cmdline.isset("bmc-with-assumptions"); + bmc( bound, convert_only, + bmc_with_assumptions, transition_system, properties, solver_factory,