Skip to content

Statement List: Jump instructions #5054

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

Merged
merged 7 commits into from
May 13, 2021

Conversation

MatWise
Copy link
Contributor

@MatWise MatWise commented Aug 22, 2019

Includes support for the following STL instructions:

  • JU (unconditional jump)
  • JC (conditional jump)
  • JCN (inverted conditional jump)

Since not all label destinations in STL are valid (this can depend on several conditions), it is needed to introduce data structures which track the properties of label and jump locations to the typecheck. See the documentation for details about the whole strategy.

Limitations: This implementation is only a rough concept and will likely be changed in the future. CFGs prove more useful for this task than the current concept, since they allow all parts of the PLC CPU to be modelled implicitly, without exceptions. Currently the state of the CPU needs to be saved as an intermediate result when encountering labels and jumps. So far this has only been realised for logic sequences. Jump instructions in blocks that depend on the accumulator will yield to false results.

  • 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.

@MatWise
Copy link
Contributor Author

MatWise commented Aug 23, 2019

Travis build fails because of known doxygen issue, works locally.

@tautschnig tautschnig force-pushed the feature/statement-list-jumps branch from 8328937 to f9b7df4 Compare May 11, 2021 08:02
@tautschnig tautschnig self-assigned this May 11, 2021
@codecov
Copy link

codecov bot commented May 11, 2021

Codecov Report

Merging #5054 (5656450) into develop (535dc20) will decrease coverage by 0.35%.
The diff coverage is n/a.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5054      +/-   ##
===========================================
- Coverage    75.68%   75.33%   -0.36%     
===========================================
  Files         1447     1447              
  Lines       157837   157988     +151     
===========================================
- Hits        119465   119013     -452     
- Misses       38372    38975     +603     
Impacted Files Coverage Δ
src/ansi-c/c_typecheck_base.cpp 55.92% <0.00%> (-22.32%) ⬇️
src/ansi-c/ansi_c_entry_point.cpp 65.88% <0.00%> (-21.50%) ⬇️
src/util/parse_options.cpp 59.61% <0.00%> (-21.16%) ⬇️
src/ansi-c/literals/convert_character_literal.cpp 53.84% <0.00%> (-17.95%) ⬇️
src/ansi-c/c_typecheck_base.h 86.66% <0.00%> (-13.34%) ⬇️
src/ansi-c/c_typecheck_expr.cpp 61.39% <0.00%> (-13.31%) ⬇️
src/goto-programs/goto_program.cpp 53.39% <0.00%> (-13.22%) ⬇️
src/ansi-c/anonymous_member.cpp 84.61% <0.00%> (-10.26%) ⬇️
src/util/xml.cpp 62.83% <0.00%> (-10.14%) ⬇️
src/util/simplify_expr_floatbv.cpp 86.82% <0.00%> (-9.31%) ⬇️
... and 40 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 8e651e4...5656450. Read the comment docs.

MatWise added 7 commits May 12, 2021 22:01
Changes the accepted format for labels and wraps instructions that have
a label in a code label.
Includes parser support for:
- JU (unconditional jump)
- JC (conditional jump)
- JCN (inverted conditional jump)
Just small formatting changes.
Adds support for the verification of jump instructions. Includes both
conditional and unconditional jumps.

Limitations: This implementation is only a rough concept and will likely
be changed in the future. CFGs prove more useful for this task than the
current concept, since they allow all parts of the PLC CPU to be
modelled implicitly, without exceptions. Currently the state of the CPU
needs to be saved as an intermediate result when encountering labels and
jumps. This is only realised for logic sequences currently. Jump
instructions in blocks that depend on the accumulator will yield to
false results!
Sets the typecheck to the correct state for verifying new blocks or
networks.

Limitations: The accumulator is unaffected by this. It needs to be
investigated whether the accumulator gets reset at all in TIA.
@tautschnig tautschnig force-pushed the feature/statement-list-jumps branch from f9b7df4 to 5656450 Compare May 12, 2021 20:15
@tautschnig tautschnig merged commit d61a8f4 into diffblue:develop May 13, 2021
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.

2 participants