Merge pull request #7403 from tautschnig/cleanup/untimed-trace

GOTO trace: no timestamps for single-threaded programs

Author: tautschnig

src/goto-symex/build_goto_trace.cpp

@@ -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;
@@ -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())

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -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()))

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -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")
     {