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

Tracing2 #3504

Draft
wants to merge 16 commits into
base: main
Choose a base branch
from
Draft

Tracing2 #3504

wants to merge 16 commits into from

Conversation

lks9
Copy link
Contributor

@lks9 lks9 commented Aug 5, 2024

Replaces #3491

Related Issue

This pull request addresses #.

Intended Change

This adds functionality to check a single control-flow trace in KeY,
so only one path in the symbolic execution path.

The idea is to record the control flow while running normally.
And then we use the recorded path as a precondition for any
proof obligation.

For experimenting and debugging method contracts and similar,
this might be very useful:

  • We do not need any auxiliary specification (loop invariants, called method contracts, proof scripts).
  • For a method contract KeY could not verify, it might be useful to explore just a single path (debugging of method contracts).

Backgound

I already had a previous approach using JML assume, see
https://github.com/lks9/retroACexampleKeY/

The current implementation uses new taclet rules traceIf, traceIfElse.

Plan

  • Automatic Instrumentation for recording (outside KeY)
  • Trace conversion for use in KeY (use traceAfter(), traceBefore() and traced() predicates)
  • Tracing rules for Exception-Handling
  • Documentation
  • Soundness?

Type of pull request

  • New feature (non-breaking change which adds functionality)
  • There are changes to the taclet rule base

Ensuring quality

TODO:

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
  • I added new test case(s) for new functionality.
  • I have tested the feature as follows: ...
  • I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@lks9 lks9 mentioned this pull request Aug 5, 2024
5 tasks
lks9 added 3 commits August 5, 2024 14:09
* tracing:off for some taclet rules
* renamed displayName for some rules
  (e.g. compound_assignment to assignment_and)
* generalized condition_not_simple to match Expression e1, e2
  (still sound a simplification; needed when tracing)
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.

1 participant