Include function and parameter in `convert_function` error messages #6426

adpaco-aws · 2021-11-01T19:47:25Z

Include the name of the function and parameter causing DATA_INVARIANT to fail in the error messages. This saves time spent in debugging which function and parameter are problematic.

Fixes a couple of mistakes I spotted in the section titles in COMPILING.md.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

TGWDB · 2021-11-02T09:43:52Z

src/goto-programs/goto_convert_functions.cpp

+  const size_t ERROR_MSG_LEN = 512;
+  char parameter_error_message[ERROR_MSG_LEN];
  // we have a body, make sure all parameter names are valid
  for(const auto &p : f.parameter_identifiers)
  {
-    DATA_INVARIANT(!p.empty(), "parameter identifier should not be empty");
+    if (p.empty())
+    {
+      snprintf(parameter_error_message,
+               ERROR_MSG_LEN - 1,
+               "parameter identifier should not be empty\n"
+               "function: %s\n"
+               "parameter: %s",
+               identifier.c_str(),
+               p.c_str());
+    }
+    DATA_INVARIANT(!p.empty(), parameter_error_message);
+
+    if (!symbol_table.has_symbol(p))
+    {
+      snprintf(parameter_error_message,
+               ERROR_MSG_LEN - 1,
+               "parameter identifier must be a known symbol\n"
+               "function: %s\n"
+               "parameter: %s",
+               identifier.c_str(),
+               p.c_str());
+    }
    DATA_INVARIANT(
      symbol_table.has_symbol(p),
-      "parameter identifier must be a known symbol");
+      parameter_error_message);


I'm not sure that defining and constructing all of this outside the invariant is the right choice. There is also DATA_INVARIANT_WITH_DIAGNOSTICS that handles other arguments beyond the message.

Yes; what @TGWDB says.

codecov · 2021-11-02T10:37:29Z

Codecov Report

Merging #6426 (3078d8a) into develop (57ee7ac) will decrease coverage by 0.03%.
The diff coverage is 100.00%.

❗ Current head 3078d8a differs from pull request most recent head 21680ba. Consider uploading reports for the commit 21680ba to get more accurate results

@@             Coverage Diff             @@
##           develop    #6426      +/-   ##
===========================================
- Coverage    76.04%   76.01%   -0.04%     
===========================================
  Files         1546     1527      -19     
  Lines       165541   164465    -1076     
===========================================
- Hits        125882   125013     -869     
+ Misses       39659    39452     -207

Impacted Files	Coverage Δ
src/goto-programs/goto_convert_functions.cpp	`100.00% <100.00%> (ø)`
...rc/solvers/smt2_incremental/smt_solver_process.cpp	`25.00% <0.00%> (-49.08%)`	⬇️
src/solvers/smt2_incremental/smt_solver_process.h	`66.66% <0.00%> (-33.34%)`	⬇️
src/util/pointer_predicates.cpp	`71.60% <0.00%> (-21.95%)`	⬇️
unit/solvers/smt2/smt2irep.cpp	`83.09% <0.00%> (-16.91%)`	⬇️
...ncremental/smt2_incremental_decision_procedure.cpp	`78.43% <0.00%> (-11.26%)`	⬇️
src/util/piped_process.cpp	`76.92% <0.00%> (-3.85%)`	⬇️
src/goto-symex/symex_function_call.cpp	`93.18% <0.00%> (-2.28%)`	⬇️
src/goto-symex/ssa_step.cpp	`79.31% <0.00%> (-2.07%)`	⬇️
src/goto-checker/solver_factory.cpp	`76.49% <0.00%> (-1.39%)`	⬇️
... and 71 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update faaf50e...21680ba. Read the comment docs.

adpaco-aws · 2021-11-02T20:32:02Z

Hi @TGWDB , thanks for your suggestion!

I have changed the code to use DATA_INVARIANT_WITH_DIAGNOSTICS and print a similar message. Let me know if you see any other issues.

martin-cs

Yes; looks good.

Please forgive the pedantry but in future it would be easier if this was two separate PRs. That way each PR does / fixes one thing. I realise this is hassle.

kroening · 2021-11-11T16:02:42Z

src/goto-programs/goto_convert_functions.cpp

+      identifier,
+      "parameter:",
+      p);
+


That doesn't make sense: when the message is triggered, p is empty. Thus, why log it?

Right. Removed p from this case.

tautschnig

@adpaco-aws Could you please squash the three commits pertaining to the diagnostic message into a single one?

adpaco-aws · 2021-12-01T14:13:46Z

@tautschnig just squashed them and rebased against develop, let me know if you see any issues.

adpaco-aws requested review from chrisr-diffblue, kroening, peterschrammel and tautschnig as code owners November 1, 2021 19:47

TGWDB reviewed Nov 2, 2021

View reviewed changes

adpaco-aws force-pushed the debug-convert-function branch from 6063df6 to 5506b3d Compare November 2, 2021 20:28

adpaco-aws force-pushed the debug-convert-function branch from 5506b3d to c11b5cd Compare November 3, 2021 12:04

adpaco-aws requested a review from TGWDB November 3, 2021 12:05

martin-cs approved these changes Nov 3, 2021

View reviewed changes

TGWDB approved these changes Nov 4, 2021

View reviewed changes

kroening reviewed Nov 11, 2021

View reviewed changes

adpaco-aws requested a review from kroening November 18, 2021 16:46

tautschnig approved these changes Dec 1, 2021

View reviewed changes

tautschnig assigned adpaco-aws Dec 1, 2021

adpaco-aws added 2 commits December 1, 2021 14:10

Print function & parameter in convert_function errors

6a58ed9

Fix section titles in COMPILING.md

21680ba

adpaco-aws force-pushed the debug-convert-function branch from 3078d8a to 21680ba Compare December 1, 2021 14:11

adpaco-aws removed their assignment Dec 1, 2021

tautschnig merged commit 7eceeb5 into diffblue:develop Dec 1, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Include function and parameter in `convert_function` error messages #6426

Include function and parameter in `convert_function` error messages #6426

Uh oh!

adpaco-aws commented Nov 1, 2021

Uh oh!

TGWDB Nov 2, 2021

Uh oh!

martin-cs Nov 3, 2021

Uh oh!

codecov bot commented Nov 2, 2021 •

edited

Loading

Uh oh!

adpaco-aws commented Nov 2, 2021

Uh oh!

martin-cs left a comment

Uh oh!

kroening Nov 11, 2021

Uh oh!

adpaco-aws Nov 11, 2021

Uh oh!

tautschnig left a comment

Uh oh!

adpaco-aws commented Dec 1, 2021

Uh oh!

Uh oh!

Include function and parameter in convert_function error messages #6426

Include function and parameter in convert_function error messages #6426

Uh oh!

Conversation

adpaco-aws commented Nov 1, 2021

Uh oh!

TGWDB Nov 2, 2021

Choose a reason for hiding this comment

Uh oh!

martin-cs Nov 3, 2021

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Nov 2, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

adpaco-aws commented Nov 2, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

kroening Nov 11, 2021

Choose a reason for hiding this comment

Uh oh!

adpaco-aws Nov 11, 2021

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

adpaco-aws commented Dec 1, 2021

Uh oh!

Uh oh!

Include function and parameter in `convert_function` error messages #6426

Include function and parameter in `convert_function` error messages #6426

codecov bot commented Nov 2, 2021 •

edited

Loading