Skip to content
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.

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

Clarify usage of history variables in error messages #8456

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from

Conversation

qinheping
Copy link
Collaborator

Resolve: #8453
loop_entry expressions are only supported in loop contracts. old expressions are only supported in function contracts. Using them in expressions in other places such as assertions may lead to conversion error.

Copy link

codecov bot commented Sep 13, 2024

Codecov Report

Attention: Patch coverage is 0% with 7 lines in your changes missing coverage. Please review.

Project coverage is 78.26%. Comparing base (2212cd6) to head (83f5c48).
Report is 26 commits behind head on develop.

Files with missing lines Patch % Lines
src/solvers/smt2/smt2_conv.cpp 0.00% 7 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8456      +/-   ##
===========================================
- Coverage    78.38%   78.26%   -0.13%     
===========================================
  Files         1726     1727       +1     
  Lines       188616   190082    +1466     
  Branches     18295    18526     +231     
===========================================
+ Hits        147855   148773     +918     
- Misses       40761    41309     +548     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@qinheping qinheping force-pushed the issues/8453 branch 2 times, most recently from 19dc6a3 to 698c22c Compare September 16, 2024 01:24
@@ -2476,6 +2476,18 @@ void smt2_convt::convert_expr(const exprt &expr)
out << ')';
}
}
else if(expr.id() == ID_old)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can't we detect this much earlier, e.g., in the C front-end during type checking? We actually already do some such checking, I think we just need to do more of it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can't detect this during type checking as we can't distinguish expressions in loop invariants and in __CPROVER_assert at that stage.

CBMC warned that it would ignore __CPROVER_loop_entry in assertions during prop_conv when using SAT backend. However, when using SMT backend, CBMC would throw exception without notifying that the cause is invalid usage of loop_entry.

This PR patches the case of using SMT backend and clarify the correct usage of loop_entry when exception thrown.

@qinheping
Copy link
Collaborator Author

@tautschnig Any thoughts on this?

@tautschnig
Copy link
Collaborator

I still believe we should identify this problem during parsing or type checking stages, even if it requires much larger changes. For the time being I'll re-assign to solver code owners.

@rod-chapman
Copy link
Collaborator

This problem should be identified and reported in a way that gives the clearest, understandable and actionable error message to the user.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

CBMC crash if CPROVER_loop_entry is used inside an assertion inside a loop
6 participants