Abstract Execution

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

Table of Contents

• KeY-AE and Refactoring Models
• Proof Statistics
• Syntactic Desugaring
• How To Write New Refactoring Models
• Abstract Execution Taclets

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.

• Download Preprint
• Download Appendix
• Download KeY and Supplementary Files

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.

Proof Statistics

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

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.

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               
    \varcond(\prefixContainsElement("LoopScopeBlock"))
    // Check that we're inside a method frame (otherwise returning makes no sense)
    \varcond(\prefixContainsElement("MethodFrame"))
    
    // Check that we're in a non-void method, extract result variable
    \varcond(\storeResultVarIn(#v))
    \varcond(\isDefined(#v))
    
    // Surrounding block labels 
    \varcond(\storeContextLabelsIn(#labels))
    // Surrounding loop labels 
    \varcond(\storeContextLoopLabelsIn(#labels1))
    // 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))
    \varcond(\newLabel(#label))
    
    \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) {
                   continue;
               }
               if (#breaks) {
                   break;
               }
               #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)
};