Lukas tracing

[lks9]

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, traceElse (and the ones without else-branch).

Plan

• Automatic Instrumentation for recording (outside KeY)
• Trace conversion for use in KeY (outside KeY)
• 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)

@unp1

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

[wadoon]

Do you really need to record the trace of the Java program? I guess it would be enough to capture the state of the input parameters (and class etc...) on the method entry. Then, the control flow should be deterministic. (And then you would be on track with our data minimization paper at ISOLA'22).

[lks9]

@wadoon Thank you very much for the literature! Yes, I think that could work, too! I have not read the paper yet but I suppose it is not that easy to capture the state of all input parameters in Java? (For binary programs, something similar is done by the RR debugger, but this debugger is very system dependent and will not work at Java source code level.)

On the other hand, the instrumentation for Java is doable (see https://github.com/ProRunVis/ProRunVis based on the JavaParser). We only need to change the instrumentation that it only records a bit-trace of if/else-decisions (for C, see https://github.com/lks9/src-tracer). At least for the KeY Symposium I will have a working demo of every step, I promise!

What I also find interesting is to look how you achieve data minimization... I think control-flow tracing could also adhere that principle. But I still need to read the paper, thanks!

[lks9]

In the meantime, you could just start KeY with: key.ui/examples/heap/pathValidation/quicksort.key

[wadoon]

I suppose it is not that easy to capture the state of all input parameters in Java?

Relatively easy. For POJO things, you can just use serialization or do it with reflection on your own. Of course, capturing and reproducing external resources (Files, ...) might be impossible.

On the other, what you need is a list of observer functions (path conditions), which evaluate the state of expression on the spot.

For the generation of Java code from JML code, we have functionality in JJBMC upon the jmltoolkit.

If you need to rewrite JML/Java program code I would recommend to look into jmltoolkit.

[mi-ki]

I think the two approaches are somewhat complementary, and I am very much looking forward to the talk at this year's KeY Symposium!
For specific information-flow/fairness use-cases, @samysweb and I thought about extracting something along the lines of path conditions from information-flow proofs in KeY and this trace idea sounds very promising to me in that respect.

[lks9]

Thank you very much for all the feedback! To be honest, I only set-up this DRAFT-PR to run the tests...

I suppose it is not that easy to capture the state of all input parameters in Java?

Relatively easy. For POJO things, you can just use serialization or do it with reflection on your own. Of course, capturing and reproducing external resources (Files, ...) might be impossible.

Well, only that all of this is already possible with the RR debugger!

Three arguments in favor of my approach against the POJO thing with reflection:

First, I think POJO would be to much of a restriction. KeY goes beyond POJO with modular specifications and there are some other approaches (e.g. context aware trace contracts or dependent assertions) that go in the opposite direction, but also beyond POJO.

Second, even with POJO this could be nice as it allows KeY's symbolic execution to follow a single path. What could be an alternative is to capture the inputs and than do that data minimization from your paper on the inputs, if this would be possible. But this needs to be implemented somehow, your original approach works by refactoring the code instead (if I grasped it correctly).

Third, retracing with KeY (or other symbolic execution tools) using recorded input constraints could be slower, because we still need to check for each if/else branching which branch is satisfiable (although we know that only one is satisfiable, because it is deterministic). With this DRAFT-PR, you get non-branching rules for if/else. It is also easier to navigate in KeY's proof tree when there is less branching (I also observed in comparison to my previous approach which used JML assume() instead of single-branch taclet rules).

On the other, what you need is a list of observer functions (path conditions), which evaluate the state of expression on the spot.

For every single if/else, while or for we need additional code (observer functions) to record either a 0 or a 1. But we do not record what is usually called path condition in symbolic execution: Perhaps you see the 0/1 bitstring as some sort of path condition, I suppose that would be somehow correct, but I would not call it that to avoid confusion. There is no (expensive) evaluation needed during recording.

If you need to rewrite JML/Java program code I would recommend to look into jmltoolkit.

Thanks!

[lks9]

Closed because of #3504