Skip to content

GOTO trace: no timestamps for single-threaded programs #7403

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jan 12, 2023
Merged

GOTO trace: no timestamps for single-threaded programs #7403

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions src/goto-symex/build_goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,6 +220,7 @@ void build_goto_trace(
time_mapt time_map;

mp_integer current_time=0;
const bool has_threads = target.has_threads();

ssa_step_iteratort last_step_to_keep = target.SSA_steps.end();
bool last_step_was_kept = false;
Expand Down Expand Up @@ -258,6 +259,9 @@ void build_goto_trace(
else if(it->is_shared_read() || it->is_shared_write() ||
it->is_atomic_end())
{
if(!has_threads)
continue;

mp_integer time_before=current_time;

if(it->is_shared_read() || it->is_shared_write())
Expand Down
18 changes: 4 additions & 14 deletions src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -477,20 +477,10 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
}();
if(!descriptor)
{
if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr))
{
// Note this case is currently expected to be encountered during trace
// generation for -
// * Steps which were removed via --slice-formula.
// * Getting concurrency clock values.
// The below implementation which returns the given expression was chosen
// based on the implementation of `smt2_convt::get` in the non-incremental
// smt2 decision procedure.
log.warning()
<< "`get` attempted for unknown symbol, with identifier - \n"
<< symbol_expr->get_identifier() << messaget::eom;
return expr;
}
INVARIANT_WITH_DIAGNOSTICS(
!can_cast_expr<symbol_exprt>(expr),
"symbol expressions must have a known value",
irep_pretty_diagnosticst{expr});
return build_expr_based_on_getting_operands(expr, *this);
}
if(const auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))
Expand Down
21 changes: 7 additions & 14 deletions unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -505,25 +505,18 @@ TEST_CASE(
test.sent_commands ==
std::vector<smt_commandt>{smt_get_value_commandt{foo_term}});
}
SECTION("Get value of non-set symbol")
SECTION("Invariant violation due to non-set symbol")
{
// smt2_incremental_decision_proceduret is used this way when cbmc is
// invoked with the combination of `--trace` and `--slice-formula`.
test.sent_commands.clear();
const exprt bar =
make_test_symbol("bar", signedbv_typet{16}).symbol_expr();
REQUIRE(test.procedure.get(bar) == bar);
REQUIRE(test.sent_commands.empty());
}
SECTION("Get value of type less symbol back")
{
// smt2_incremental_decision_proceduret is used this way as part of
// building the goto trace, to get the partial order concurrency clock
// values.
test.sent_commands.clear();
const symbol_exprt baz = symbol_exprt::typeless("baz");
REQUIRE(test.procedure.get(baz) == baz);
REQUIRE(test.sent_commands.empty());
cbmc_invariants_should_throwt invariants_throw;
REQUIRE_THROWS_MATCHES(
test.procedure.get(bar),
invariant_failedt,
invariant_failure_containing(
"symbol expressions must have a known value"));
}
SECTION("Get value of trivially solved expression")
{
Expand Down