##### Document Text Contents

Page 59

must be reflected in the observable locations of the loop body. The result of this phase is a

symbolic execution tree as illustrated in Figure 2.11.

Phase 2. We synthesize the target program q and used variable set use from qi and usei

by applying the rules in a leave-to-root manner. One starts with a leaf node and generates

the program within its sequential block first, e.g., bl

3

, bl

4

, bl

5

, bl

6

in Figure 2.11. These

are combined by rules corresponding to statements that contain a sequential block, such as

loopInvariant (containing bl

3

and bl

4

). One continues with the generalized sequential block

containing the compound statements, e.g., GSB(bl

2

), and so on, until the root is reached. Note

that the order of processing the sequential blocks matters, for instance, the program for the

sequential block bl

4

must be generated before that for bl

3

, because the observable locations in

node n

3

depend on the used variable set of bl

4

according to the loopInvariant rule.

We explain some of the rules in details.

emptyBox

�=)[email protected](obs, _)�,�

�=)U [ _ « _ ]@(obs, obs)�,�

The emptyBox rule is the starting point of program transformation in each sequential block.

The location set use is set to obs, which is the direct result of Lemma 4.

assignment

�=)U {l := r}[! « ! ]@(obs, use)�,�

�=)U [ l= r;! « l= r;! ]@(obs, use� {l}[ {r})�,� if l 2 use

�=)U [ l= r;! « ! ]@(obs, use)�,� otherwise

!

In the assignment rule, the use set contains all program variables on which a read access might

occur in the remaining program before being overwritten. In the first case, when the left side

l of the assignment is among those variables, we have to update the use set by removing the

newly assigned program variable l and adding the variable r which is read by the assignment.

The second case makes use of the knowledge that the value of l is not accessed in the remaining

program and skips the generation of the assignment.

ifElse

�,U b=)U [ p;! « p;! ]@(obs, use

p;!)�,�

�,U¬b=)U [ q;! « q;! ]@(obs, use

q;!)�,�

�=)U [ if (b) {p} else {q} ! «

if (b) {p;!} else {q;!} ]@(obs, use

p;! [ useq;! [ {b})�,�

(with b boolean variable)

49

Page 60

On encountering a conditional statement, symbolic execution splits into two branches, namely

the then branch and else branch. The generation of the conditional statement will result in

a conditional. The guard is the same as used in the original program, the then branch is the

generated version of the source then branch continued with the rest of the program after the

conditional, and the else branch is analogous to the then branch.

Note that the statements following the conditional statement are symbolically executed on

both branches. This leads to duplicated code in the generated program, and, potentially to

code size duplication at each occurrence of a conditional statement. One note in advance: code

duplication can be avoided when applying a similar technique as presented later in connection

with the loop translation rule. However, it is noteworthy that the application of this rule might

have also advantages: as discussed in Chapter 3, symbolic execution and partial evaluation can

be interleaved resulting in (considerably) smaller execution traces. Interleaving symbolic execu-

tion and partial evaluation is orthogonal to the approach presented here and can be combined

easily. In several cases this can lead to different and drastically specialized and therefore smaller

versions of the remainder program ! and !. The use set is extended canonically by joining the

use sets of the different branches and the guard variable.

loopInvariant

�=)U inv,�

�,UVmod(b^ inv) =)UVmod

[ p « p ]@(use

1

[ {b}, use

2

)inv,�

�,UVmod(¬b^ inv) =)UVmod[! « ! ]@(obs, use1)�,�

�=)U [ while(b){p}! « while(b){p}! ]@(obs, use

1

[ use

2

[ {b})�,�

On the logical side the loop invariant rule is as expected and has three premises. Here we are

interested in compilation of the analyzed program rather than proving its correctness. There-

fore, it is sufficient to use true as a trivial invariant or to use any automatically obtainable

invariant. In this case the first premise (init) ensuring that the loop invariant is initially valid

contributes nothing to the program compilation process and is ignored from here onward (if

true is used as invariant then it holds trivially).

Two things are of importance: the third premise (use case) executes only the program fol-

lowing the loop. Furthermore, this code fragment is not executed by any of the other branches

and, hence, we avoid unnecessary code duplication. The second observation is that variables

read by the program in the third premise may be assigned in the loop body, but not read in the

loop body. Obviously, we have to prevent that the assignment rule discards those assignments

when compiling the loop body. Therefore, in the obs for the second premise (preserves), we

must include the used variables of the use case premise and, for similar reasons, the program

variable(s) read by the loop guard. In practice this is achieved by first executing the use case

50

Page 117

[Mey86] Bertrand Meyer. Design by contract. Technical Report TR-EI-12/CO, pages 1–50,

1986.

[Mey92] Bertrand Meyer. Applying “design by contract”. IEEE Computer, 25(10):40–51,

October 1992.

[Mey00] Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, 2000.

[Mos05] Wojciech Mostowski. Formalisation and verification of Java Card security properties

in dynamic logic. In Maura Cerioli, editor, Proc. Fundamental Approaches to Software

Engineering (FASE), Edinburgh, volume 3442 of LNCS, pages 357–371. Springer,

April 2005.

[MP67] John Mccarthy and James Painter. Correctness of a compiler for arithmetic expres-

sions. In Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia

in Applied Mathematics, pages 33–41. American Mathematical Society, 1967.

[MPH00] Jörg Meyer and Arnd Poetzsch-Heffter. An architecture for interactive program

provers. In TACAS, pages 63–77, 2000.

[MW72] Robin Milner and Richard Weyhrauch. Proving compiler correctness in a mecha-

nized logic. In Proc. 7th Annual Machine Intelligence Workshop, volume 7 of Machine

Intelligence, pages 51–72. Edinburgh University Press, 1972.

[Mye04] Glenford J. Myers. Art of Software Testing. John Wiley & Sons, second edition, 2004.

[NPW02] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof

Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

[Plo04] Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr.

Program., 60-61:17–139, 2004.

[Pra76] Vaughan R. Pratt. Semantical considerations on floyd-hoare logic. In FOCS, pages

109–121, 1976.

[PV04] Corina S. Pasareanu and Willem Visser. Verification of Java programs using symbolic

execution and invariant generation. In Susanne Graf and Laurent Mounier, editors,

Proc. Model Checking Software, 11th International SPIN Workshop, Barcelona, Spain,

volume 2989 of LNCS, pages 164–181. Springer, 2004.

[Rey02] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In

LICS, pages 55–74, 2002.

[Rüm06] Philipp Rümmer. Sequential, parallel, and quantified updates of first-order struc-

tures. In Miki Hermann and Andrei Voronkov, editors, Proc. Logic for Programming,

107

must be reflected in the observable locations of the loop body. The result of this phase is a

symbolic execution tree as illustrated in Figure 2.11.

Phase 2. We synthesize the target program q and used variable set use from qi and usei

by applying the rules in a leave-to-root manner. One starts with a leaf node and generates

the program within its sequential block first, e.g., bl

3

, bl

4

, bl

5

, bl

6

in Figure 2.11. These

are combined by rules corresponding to statements that contain a sequential block, such as

loopInvariant (containing bl

3

and bl

4

). One continues with the generalized sequential block

containing the compound statements, e.g., GSB(bl

2

), and so on, until the root is reached. Note

that the order of processing the sequential blocks matters, for instance, the program for the

sequential block bl

4

must be generated before that for bl

3

, because the observable locations in

node n

3

depend on the used variable set of bl

4

according to the loopInvariant rule.

We explain some of the rules in details.

emptyBox

�=)[email protected](obs, _)�,�

�=)U [ _ « _ ]@(obs, obs)�,�

The emptyBox rule is the starting point of program transformation in each sequential block.

The location set use is set to obs, which is the direct result of Lemma 4.

assignment

�=)U {l := r}[! « ! ]@(obs, use)�,�

�=)U [ l= r;! « l= r;! ]@(obs, use� {l}[ {r})�,� if l 2 use

�=)U [ l= r;! « ! ]@(obs, use)�,� otherwise

!

In the assignment rule, the use set contains all program variables on which a read access might

occur in the remaining program before being overwritten. In the first case, when the left side

l of the assignment is among those variables, we have to update the use set by removing the

newly assigned program variable l and adding the variable r which is read by the assignment.

The second case makes use of the knowledge that the value of l is not accessed in the remaining

program and skips the generation of the assignment.

ifElse

�,U b=)U [ p;! « p;! ]@(obs, use

p;!)�,�

�,U¬b=)U [ q;! « q;! ]@(obs, use

q;!)�,�

�=)U [ if (b) {p} else {q} ! «

if (b) {p;!} else {q;!} ]@(obs, use

p;! [ useq;! [ {b})�,�

(with b boolean variable)

49

Page 60

On encountering a conditional statement, symbolic execution splits into two branches, namely

the then branch and else branch. The generation of the conditional statement will result in

a conditional. The guard is the same as used in the original program, the then branch is the

generated version of the source then branch continued with the rest of the program after the

conditional, and the else branch is analogous to the then branch.

Note that the statements following the conditional statement are symbolically executed on

both branches. This leads to duplicated code in the generated program, and, potentially to

code size duplication at each occurrence of a conditional statement. One note in advance: code

duplication can be avoided when applying a similar technique as presented later in connection

with the loop translation rule. However, it is noteworthy that the application of this rule might

have also advantages: as discussed in Chapter 3, symbolic execution and partial evaluation can

be interleaved resulting in (considerably) smaller execution traces. Interleaving symbolic execu-

tion and partial evaluation is orthogonal to the approach presented here and can be combined

easily. In several cases this can lead to different and drastically specialized and therefore smaller

versions of the remainder program ! and !. The use set is extended canonically by joining the

use sets of the different branches and the guard variable.

loopInvariant

�=)U inv,�

�,UVmod(b^ inv) =)UVmod

[ p « p ]@(use

1

[ {b}, use

2

)inv,�

�,UVmod(¬b^ inv) =)UVmod[! « ! ]@(obs, use1)�,�

�=)U [ while(b){p}! « while(b){p}! ]@(obs, use

1

[ use

2

[ {b})�,�

On the logical side the loop invariant rule is as expected and has three premises. Here we are

interested in compilation of the analyzed program rather than proving its correctness. There-

fore, it is sufficient to use true as a trivial invariant or to use any automatically obtainable

invariant. In this case the first premise (init) ensuring that the loop invariant is initially valid

contributes nothing to the program compilation process and is ignored from here onward (if

true is used as invariant then it holds trivially).

Two things are of importance: the third premise (use case) executes only the program fol-

lowing the loop. Furthermore, this code fragment is not executed by any of the other branches

and, hence, we avoid unnecessary code duplication. The second observation is that variables

read by the program in the third premise may be assigned in the loop body, but not read in the

loop body. Obviously, we have to prevent that the assignment rule discards those assignments

when compiling the loop body. Therefore, in the obs for the second premise (preserves), we

must include the used variables of the use case premise and, for similar reasons, the program

variable(s) read by the loop guard. In practice this is achieved by first executing the use case

50

Page 117

[Mey86] Bertrand Meyer. Design by contract. Technical Report TR-EI-12/CO, pages 1–50,

1986.

[Mey92] Bertrand Meyer. Applying “design by contract”. IEEE Computer, 25(10):40–51,

October 1992.

[Mey00] Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, 2000.

[Mos05] Wojciech Mostowski. Formalisation and verification of Java Card security properties

in dynamic logic. In Maura Cerioli, editor, Proc. Fundamental Approaches to Software

Engineering (FASE), Edinburgh, volume 3442 of LNCS, pages 357–371. Springer,

April 2005.

[MP67] John Mccarthy and James Painter. Correctness of a compiler for arithmetic expres-

sions. In Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia

in Applied Mathematics, pages 33–41. American Mathematical Society, 1967.

[MPH00] Jörg Meyer and Arnd Poetzsch-Heffter. An architecture for interactive program

provers. In TACAS, pages 63–77, 2000.

[MW72] Robin Milner and Richard Weyhrauch. Proving compiler correctness in a mecha-

nized logic. In Proc. 7th Annual Machine Intelligence Workshop, volume 7 of Machine

Intelligence, pages 51–72. Edinburgh University Press, 1972.

[Mye04] Glenford J. Myers. Art of Software Testing. John Wiley & Sons, second edition, 2004.

[NPW02] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof

Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

[Plo04] Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr.

Program., 60-61:17–139, 2004.

[Pra76] Vaughan R. Pratt. Semantical considerations on floyd-hoare logic. In FOCS, pages

109–121, 1976.

[PV04] Corina S. Pasareanu and Willem Visser. Verification of Java programs using symbolic

execution and invariant generation. In Susanne Graf and Laurent Mounier, editors,

Proc. Model Checking Software, 11th International SPIN Workshop, Barcelona, Spain,

volume 2989 of LNCS, pages 164–181. Springer, 2004.

[Rey02] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In

LICS, pages 55–74, 2002.

[Rüm06] Philipp Rümmer. Sequential, parallel, and quantified updates of first-order struc-

tures. In Miki Hermann and Andrei Voronkov, editors, Proc. Logic for Programming,

107