[Interp] Add transaction info to assert_eq error messages

Author: ngernest

protocols/src/diagnostic.rs

@@ -460,6 +460,7 @@ impl DiagnosticHandler {
         expr2_id: &ExprId,
         eval1: &BitVecValue,
         eval2: &BitVecValue,
+        todo_args: &[BitVecValue],
     ) {
         let buffer = &mut self.create_buffer();
 
@@ -470,9 +471,22 @@ impl DiagnosticHandler {
                 fileid1 == fileid2,
                 "Expressions must be in the same file for assertion error"
             );
+            let transaction_call = if todo_args.is_empty() {
+                tr.name.clone()
+            } else {
+                let args_str = todo_args
+                    .iter()
+                    .map(|v| serialize_bitvec(v, false))
+                    .collect::<Vec<_>>()
+                    .join(", ");
+                format!("{}({})", tr.name, args_str)
+            };
             let diagnostic = Diagnostic {
                 title: format!("Error in file {}", fileid1),
-                message: "The two expressions did not evaluate to the same value".to_string(),
+                message: format!(
+                    "The two expressions did not evaluate to the same value (in transaction `{}`)",
+                    transaction_call
+                ),
                 level: Level::Error,
                 locations: self.error_locations(vec![(
                     fileid1,

protocols/src/errors.rs

@@ -643,6 +643,7 @@ impl DiagnosticEmitter {
         error: &ExecutionError,
         transaction: &Transaction,
         symbol_table: &SymbolTable,
+        todo_args: &[BitVecValue],
     ) {
         match error {
             ExecutionError::Evaluation(eval_err) => {
@@ -655,7 +656,13 @@ impl DiagnosticEmitter {
                 Self::emit_symbol_error(handler, symbol_err, transaction, symbol_table);
             }
             ExecutionError::Assertion(assert_err) => {
-                Self::emit_assertion_error(handler, assert_err, transaction, symbol_table);
+                Self::emit_assertion_error(
+                    handler,
+                    assert_err,
+                    transaction,
+                    symbol_table,
+                    todo_args,
+                );
             }
             ExecutionError::MaxStepsReached(_) => {
                 handler.emit_general_message(&format!("{error}"), Level::Error);
@@ -981,6 +988,7 @@ impl DiagnosticEmitter {
         error: &AssertionError,
         transaction: &Transaction,
         _symbol_table: &SymbolTable,
+        todo_args: &[BitVecValue],
     ) {
         match error {
             AssertionError::EqualityFailed {
@@ -989,7 +997,14 @@ impl DiagnosticEmitter {
                 value1,
                 value2,
             } => {
-                handler.emit_diagnostic_assertion(transaction, expr1_id, expr2_id, value1, value2);
+                handler.emit_diagnostic_assertion(
+                    transaction,
+                    expr1_id,
+                    expr2_id,
+                    value1,
+                    value2,
+                    todo_args,
+                );
             }
             AssertionError::DontCareAssertion { stmt_id } => {
                 handler.emit_diagnostic_stmt(

protocols/src/scheduler.rs

@@ -486,7 +486,13 @@ impl<'a> Scheduler<'a> {
                     .expect("Transaction not found in IRs");
                 let (tr, st, _) = self.irs[ir_idx];
 
-                DiagnosticEmitter::emit_execution_error(self.handler, error, tr, st);
+                DiagnosticEmitter::emit_execution_error(
+                    self.handler,
+                    error,
+                    tr,
+                    st,
+                    &self.todos[idx].1,
+                );
             }
         }
     }

protocols/tests/adders/adder_d1/add_multitrace.out

@@ -2,7 +2,7 @@ Trace 0 executed successfully!
 
 ---
 
-error: The two expressions did not evaluate to the same value
+error: The two expressions did not evaluate to the same value (in transaction `add(4, 5, 10)`)
    ┌─ adders/adder_d1/add_d1.prot:14:13
    │
 14 │   assert_eq(s, DUT.s);

protocols/tests/adders/adder_d1/both_threads_fail.out

@@ -1,10 +1,10 @@
-error: The two expressions did not evaluate to the same value
+error: The two expressions did not evaluate to the same value (in transaction `add_fork_early(1, 2, 5)`)
    ┌─ adders/adder_d1/add_d1.prot:26:13
    │
 26 │   assert_eq(s, DUT.s);
    │             ^^^^^^^^ LHS Value: 5, RHS Value: 3
 
-error: The two expressions did not evaluate to the same value
+error: The two expressions did not evaluate to the same value (in transaction `add_fork_early(4, 5, 10)`)
    ┌─ adders/adder_d1/add_d1.prot:26:13
    │
 26 │   assert_eq(s, DUT.s);

protocols/tests/adders/adder_d1/busy_wait_fail.out

@@ -1,4 +1,4 @@
-error: The two expressions did not evaluate to the same value
+error: The two expressions did not evaluate to the same value (in transaction `add_busy_wait(1, 2, 2, 999)`)
    ┌─ adders/adder_d1/busy_wait.prot:21:15
    │
 21 │     assert_eq(s, DUT.s);

protocols/tests/adders/adder_d1/first_fail_second_norun.out

@@ -1,4 +1,4 @@
-error: The two expressions did not evaluate to the same value
+error: The two expressions did not evaluate to the same value (in transaction `add(1, 2, 4)`)
    ┌─ adders/adder_d1/add_d1.prot:14:13
    │
 14 │   assert_eq(s, DUT.s);

protocols/tests/adders/adder_d1/first_thread_fails.out

@@ -1,4 +1,4 @@
-error: The two expressions did not evaluate to the same value
+error: The two expressions did not evaluate to the same value (in transaction `add(1, 2, 4)`)
    ┌─ adders/adder_d1/add_d1.prot:14:13
    │
 14 │   assert_eq(s, DUT.s);

protocols/tests/adders/adder_d1/second_thread_fails.out

@@ -1,4 +1,4 @@
-error: The two expressions did not evaluate to the same value
+error: The two expressions did not evaluate to the same value (in transaction `add(4, 5, 10)`)
    ┌─ adders/adder_d1/add_d1.prot:14:13
    │
 14 │   assert_eq(s, DUT.s);

protocols/tests/brave_new_world/bit_truncation/bit_truncation_fft_bug.out

@@ -1,4 +1,4 @@
-error: The two expressions did not evaluate to the same value
+error: The two expressions did not evaluate to the same value (in transaction `bit_truncation_fft(8386560, 2047)`)
    ┌─ brave_new_world/bit_truncation/bit_truncation_fft.prot:10:15
    │
 10 │     assert_eq(data_out, dut.output_data);