Abstract Execution

This page supplies additional material for the paper “Abstract Execution“, accepted for FM 2019.

Table of Contents

Abstract. We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter analyzes all possible execution paths of a specific program, Abstract Execution analyzes a partially unspecified program by permitting abstract symbols representing unknown contexts. For each abstract symbol, we faithfully represent each possible concrete execution resulting from its substitution with concrete code. There is a wide range of applications of Abstract Execution, especially for verifying relational properties of schematic programs. We implemented Abstract Execution in a deductive verification framework and proved correctness of eight well-known statement-level refactoring rules, including two with loops. For each refactoring we characterize the preconditions that make it semantics-preserving. Most preconditions are not mentioned in the literature.

You can download a preprint of the paper, or download the appendix only.

KeY-AE and Refactoring Models

The archive with additional files for the paper contains a KeY version implementing Abstract Execution as well as all refactoring models (abstract Java programs, KeY problem files and proof scripts for refactorings with loops). There is also a README.md file in which you find information about the file structure and advice on how to start KeY or a test suite running all refactoring equivalence proofs. For running the test suite (of which you find the corresponding Java files in the src/ directory) or starting KeY, you need to have at least Java 8 installed (and ant for building the test project automatically).

You can conveniently load most AE examples with KeY’s “Load Example” dialog. This includes only correctly specified examples, not those for which the proofs do not close. The latter are included as additional soundness validation checks, and for demonstrating the functionality of our type checker for Abstract Placeholder Statement specifications, in the above mentioned archive. For loading an AE example, choose “File > Load Example” and scroll to the “Abstract Execution” folder at the bottom of the examples list. For the examples not including loops, click on the “Play” button at the upper left of the window to start the automatic strategy execution. The loop-based examples come with proof scripts that start automatically. For some examples, we also have finished proofs available which you can reload by choosing “Load Proof” instead of “Load Example”. All examples should “work”, i.e. the proofs close without any further interaction.

Screenshot of the "Load Example" dialog in KeY, with the Remove Control Flag example chosen.
Screenshot of the “Load Example” dialog in KeY, with the Remove Control Flag example chosen.

Proof Statistics

The below table shows some details about the proof statistics mentioned in the paper.

Refactoring TechniqueNodesAuto mode time [ms]#APS
Move Statements to Callers2,8966,6373
Extract Method (with field)2,97411,4873
Extract Method3,02210,7693
Cond.Dupl.Cond.Fragm. (Prefix)3,84512,5264
Cond.Dupl.Cond.Fragm. (Postfix)3,8749,3724
Cond.Dupl.Cond.Fragm. (Try Catch Postfix)4,52712,2554
Cond.Dupl.Cond.Fragm. (Try Catch Postfix, no finally)5,06519,3144
Cond.Dupl.Cond.Fragm. (complex abstract expression)6,96420,0405
Decompose Conditional6,01726,0264
Slide Statements7,28431,9615
Remove Control Flag (Manuall Unrolling)9,00442,1232
Remove Control Flag (Unrolling Inv Rule)9,01232,0132
Replace Exception with Test (Single Variable Rollback)14,25150,6594
Replace Exception with Test (Skolem Locset Rollback)18,68563,6934
Split Loop39,980333,8058

Syntactic Desugaring

The paper mentions some syntactic elements of APS specifications that are not yet implemented in KeY. All those have to be desugared to standard Java DL terms which are declared in the .key problem files. The following table explains how to do so. We plan to implement the syntactic additions in the future such that they directly can be used.

Specification Construct How to Desugar
  • Replace by \dl_localsP
  • Add LocSet localsP; to the \functions { ... } block of the problems file
final(skolemLocSet) (in a declares clause)
  • Replace by \dl_final(\dl_skolemLocSet)
  • Add LocSet skolemLocSet; to the \functions { ... } block of the problems file
  • Replace by \dl_hasTo(loc)
throwsExc(ID), returns(ID)
  • Replace by \dl_throwsExcID / \dl_returnsID
  • Add boolean throwsExcID;, boolean returnsID; to the \functions { ... } block of the problems file
axiom mutex { term1, term2, ..., termN }; (for boolean terms term1, …, termn) Add a premise to the \problem { ... } part of the .key problem file. You can either directly encode the mutex property as a first-order formula, or add a premise mutuallyExclusiveN(term1, term2, ..., termN) -> and add a rule to the problems file using the #mutualExclusionFormulaN (replace the “N” by your particular one). Check the problem file in the resources subdirectory “ConsolidateDuplicateConditionalFragementAsSlideStatementsCorrect” to see an example.

How To Write New Refactoring Models

The archive with additional files for the AE paper contains a skeleton Java and problem definition file in the directory resources/SKELETON/. There are comments in the contained files “problem.key” and “Refactor.java” that provide hints on how to extend the Skeleton to create a new refactoring model. Please use the unsugared syntax described above; examples for this are also contained in the Skeleton. For checking your new example, load the “problem.key” file into KeY and press the “Play” button to start the automatic proof search.

Abstract Execution Taclets

Taclets (“Schematic, Theory-Specific Rules”) are sequent calculus rules declared in a special, domain-specific language tailored in particular to symbolic execution rules. Most rules in KeY are written as taclets. The most complicated ones, like method contract or loop invariant rules, so far have been implemented as Java-only “built-in” rules. Our Abstract Execution taclets, as well as the new loop invariant taclets that we especially implemented for Abstract Execution, are an exception to that rule. We think that writing rules as taclets makes them more transparent and better maintainable; nevertheless, we had to add new features to the taclet language and to implement special variable conditions and term transformers for our AE taclets.

Below, you find the Abstract Execution taclet for Abstract Placeholder Statements within a loop scope and a non-void method.

abstractExecutionNonVoidLoopScope {
    // All Skolem symbols are "fresh for" the abstract program, such that
    // the same program occurring twice directly encodes the same behavior.
    \schemaVar \formula [nonrigid] C;
    \schemaVar \update U;
    \schemaVar \skolemTerm java.lang.Throwable exc \freshFor(#absProg);
    \schemaVar \skolemTerm boolean returns \freshFor(#absProg);
    \schemaVar \skolemTerm any result \freshFor(#absProg);
    \schemaVar \skolemTerm boolean breaks \freshFor(#absProg);
    \schemaVar \skolemTerm boolean continues \freshFor(#absProg);

    \find (\modality{#allmodal}{ .. #absProg ... }\endmodality(post))

    // Check that we're inside a loop scope               
    // Check that we're inside a method frame (otherwise returning makes no sense)
    // Check that we're in a non-void method, extract result variable
    // Surrounding block labels 
    // Surrounding loop labels 
    // Booleans modeling breaks to those labels. Fresh for the abstract program.
    \varcond(\instantiateVarsFresh(#vars, #labels, "breaks", boolean \freshFor(#absProg)))
    \varcond(\instantiateVarsFresh(#vars1, #labels1, "continues", boolean \freshFor(#absProg)))
    // Program variables for modeling irregular termination
    \varcond(\newPV(#exc, "exc", java.lang.Throwable \freshFor(#absProg)))
    \varcond(\newPV(#returns, "returns", boolean \freshFor(#absProg)))
    \varcond(\newPV(#result, "result", \typeof(#v) \freshFor(#absProg)))
    \varcond(\newPV(#breaks, "breaks", boolean \freshFor(#absProg)))
    \varcond(\newPV(#continues, "continues", boolean \freshFor(#absProg)))
    // Parametric Skolem update and path condition initialization.
    // The update receives two location sets as parameters; the first one for its
    // assignable, and the second one for its accessible locations (similar to a
    // normal update, just with sets). The path condition receives as argument the
    // location set of its accessible values, including the exception, returns, 
    // result, breaks and continues flags.
    \varcond(\initializeParametricSkolemUpdate(U, #absProg))
    \varcond(\initializeParametricSkolemPathCondition(C, #absProg))

    // Index variables for foreach loop 
    \varcond(\new(#v1, boolean))
    \replacewith ( 
         {U}{   #exc:=exc || #returns:=returns
             || #result:=#addCast(result,#result)
             || #breaks:=breaks || #continues:=continues}
           (  C 
            & #mutualExclusionFormula5(#returns, #exc, #breaks, #continues, #vars) 
            & #returnSpec(#absProg, #returns)
            & #excSpec(#absProg, #exc)
            & #breaksSpec(#absProg, #breaks)
            & #continuesSpec(#absProg, #continues)
           ) ->
         {U}{   #exc:=exc || #returns:=returns
             || #result:=#addCast(result,#result)
             || #breaks:=breaks || #continues:=continues}
           \modality{#allmodal}{ ..
               if (#returns) {
                   return #result;
               if (#exc != null) {
                   throw #exc;
               if (#continues) {
               if (#breaks) {
               #foreach (#v1, #label in #vars, #labels) { 
                   if (#v1) {
                       break #label;
               #foreach (#v1, #label1 in #vars1, #labels1) { 
                   if (#v1) {
                       continue #label1;
           ... }\endmodality(post))
    \heuristics(abstractExecution, simplify_prog)