CONTRACTS: Add goto-level loop-contract annotation #7788
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
qinheping
requested review from
tautschnig,
feliperodri,
remi-delmas-3000,
martin-cs,
peterschrammel and
kroening
as code owners
qinheping
force-pushed
the
features/goto-level-loop-contracts
branch
from
9eb93d8 to
69d05d1
Compare
qinheping
requested review from
jimgrundy,
TGWDB and
NlightNFotis
as code owners
qinheping
force-pushed
the
features/goto-level-loop-contracts
branch
from
69d05d1 to
22ad623
Compare
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #7788 +/- ##
===========================================
+ Coverage 78.58% 78.65% +0.07%
===========================================
Files 1693 1699 +6
Lines 193381 193857 +476
===========================================
+ Hits 151962 152477 +515
+ Misses 41419 41380 -39
☔ View full report in Codecov by Sentry. |
qinheping
force-pushed
the
features/goto-level-loop-contracts
branch
from
22ad623 to
47bccae
Compare
feliperodri
added
aws
qinheping
force-pushed
the
features/goto-level-loop-contracts
branch
5 times, most recently
from
8286ec0 to
188d439
Compare
tautschnig
reviewed
Jul 7, 2023
| @@ -0,0 +1,9 @@ | |||
| CORE gcc-only | |||
There was a problem hiding this comment.
Could you elaborate as to why this test is GCC-specific?
There was a problem hiding this comment.
We use void pointer in this benchmark. Typechecking void pointer will trigger the error https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/c_typecheck_expr.cpp#L4152 under VISUAL_STUDIO.
There was a problem hiding this comment.
Can we just use a char pointer instead?
There was a problem hiding this comment.
Actually, using char pointers will lead to a bug of DFCC.
156: File: D:\a\cbmc\cbmc\src\goto-instrument\contracts\dynamic-frames\dfcc_instrument.cpp:330 function: dfcc_instrumentt::instrument_function
156: Condition: Precondition
156: Reason: found != goto_model.goto_functions.function_map.end()
156: << EXTRA DIAGNOSTICS >>
156: Function '_errno' must exist in the model.
156: << END EXTRA DIAGNOSTICS >>
There is a function _errno in the symbol table but not in the function map. I will keep this test as gcc-only and open an issue to track this bug.
qinheping
force-pushed
the
features/goto-level-loop-contracts
branch
4 times, most recently
from
d84e62d to
84d83cc
Compare
tautschnig
approved these changes
Jul 11, 2023
qinheping
force-pushed
the
features/goto-level-loop-contracts
branch
2 times, most recently
from
ea4d440 to
d7f4ba1
Compare
qinheping
force-pushed
the
features/goto-level-loop-contracts
branch
from
d7f4ba1 to
6cc179a
Compare
This commit allows us to parse and annotate loop contracts from JSON files to GOTO models.
We first parse the JSON file to get the configuration.
Function configurations consist of function id (regex) and a list of loop-contract configurations.
Loop-contract configurations consist of:
Loop number of the loop we are annotating to.
Loop invariants as strings.
(optional) Loop assigns as strings.
(optional) Loop decreases as strings.
(optional) A symbol map that map symbol names in the loop contracts strings to their name in the symbol table of the goto model.
Loop contracts mangling consists of four steps.
Construct a fake function with a fake loop that contains the loop contracts for parsing the contracts.
Parse the fake function and extract the contracts as exprt.
Substitute symbols in the extracted exprt with the symbols in the symbol table of the goto model according to the symbol map provided by the user.
Typecheck all contract exprt.
Annotate all contract exprt to the corresponding loop.
qinheping
force-pushed
the
features/goto-level-loop-contracts
branch
from
6cc179a to
b543536
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR allows us to parse and annotate loop contracts from JSON files to GOTO models.
We first parse the JSON file to get the configuration.
Loop contracts mangling consists of four steps.