# Presentation: 037069

## Proving Correctness for  Pointer Programs in a Verifying Compiler

- Gregory Kulczycki and Amrinder Singh, Virginia Tech

## Verifying Compiler

- Editor

- Compiler

- Component
- Library

- Verifier

- Spec

- Body

- Math
- Unit

## Verifier Architecture

- Spec

- VC
- Generator

- Body

- Automated
- Prover

- Proof
- Assistant

- Math Units

- Component
- Specs

- Proof of
- theorems

- Proof of
- correctness

- Obligations

## A Scalable Verifying Compiler

- Reasoning should be modular
- Assertions should be kept as simple as possible
- Problem: Pointers and aliasing complicate reasoning

## Benefits of Our Approach

- Pointers do not need special proof rules
- Typical components do not rely on indirection

## Library components

- Map

- List

- Pointer

- Custom components

- Array

## RESOLVE Verification System

- Language designed with full “heavyweight” verification as a goal
- Incorporates alias-avoidance; uses swapping paradigm
- Simple value semantics
- Program state = defined variables + their values
- Frame property = calls can only effect:
- Explicit parameters
- Global variables listed in “updates” clause

## Pointer Component

- Reason about pointers the same way you reason about other types
- Pointers are implemented differently
- Relocate(p, q) ==> pointer copy (no call)
- Pointers can be given special syntax, but it must map to unsugared code
- q --> p^next ==> Redirect_to_Target(q, p);

## Pointer Component Spec

**Concept** Location_Linking_Template (**type** Info);
-     **Defines** Location: Set;
-     **Defines** Void: Location;
-     **Var** Target: Location  Location;
-     **Var** Contents: Location  Info;
-     **Type** **Family** Position **is** **modeled** **by** Location;
-         **exemplar** P;
-         **initialization ensures** P = Void;

## System of Linked Locations

- 

- 

- 

- 

- 

- 

- 

- P,Q

- R

- S,T

- V

- W

## System of Linked Locations

- P = Q
- Target(W) = R
- L: Location, Target(P) = L **and** Contents(L) = 

- 

- 

- 

- 

- 

- 

- 

- P,Q

- R

- S,T

- V

- W

## Relocate

**Operation** Relocate(**updates** P: Position;
- 			 **preserves** Q: Position);
-      **ensures** P = Q;

- P

- Q

- P,Q

## Relocate_to_Target

**Operation** Relocate_to_Target(**updates** P: Position;
**	****	****	****	****        ****preserves** Q: Position);
-     **requires** Q ≠ Void;
-     **ensures** P = Target(Q);

- P

- Q

- P

- Q

## Redirect_Link

**Operation** Redirect_Link(**preserves** P, Q: Position);
-     **updates** Target;
-     **requires** P ≠ Void;
-     **ensures** Target(P) = Q **and**
-          L: Location, **if** L ≠ P **then** Target(L) = #Target(L);

- P

- Q

- P

- Q

## Redirect_to_Target

**Operation** Redirect_to_Target(**preserves** P, Q: Position);
-     **updates** Target;
-     **requires** P ≠ Void **and** Q ≠ Void;
-     **ensures** Target(P) = #Target(Q) **and**
-         L: Location, **if** L ≠ P **then** Target(L) = #Target(L);

- P

- Q

- P

- Q

## Transfer Specification

**Operation** Transfer(**preserves** P, Q: Position);
-     **updates** Target;
-     **requires** P ≠ Void **and** Q ≠ Void **and**
-                    Target(Q) ≠ Void;
-     **ensures** _x0001_
-         _x0001_Target(P) = #Target(Q) **and**
-         Target(Q) = #Target(#Target(Q)) **and**
-         Target(#Target(Q)) = #Target(P) **and**
-         L: Location,
-             **if** L ≠ P **and** L ≠ Q **and** L ≠ #Target(Q)
-             **then** Target(L) = #Target(L);

## Effect of Transfer(P, Q)

- P

- Q

**Operation** Transfer(**preserves** P, Q: Position);
**updates** Target;
**requires**
- P ≠ Void **and**
- Q ≠ Void **and**
- Target(Q) ≠ Void;
**ensures** _x0001_
-  L: Location, Target(L) =
-   #Target(Q)                **if** L = P
-   #Target(#Target(Q)) **if** L = Q
-   #Target(P)                **if** L = #Target(Q)
-   #Target(L)                **otherwise**;

## Effect of Transfer(P, Q)

- P

- Q

- P

- Q

**Operation** Transfer(**preserves** P, Q: Position);
**updates** Target;
**requires**
- P ≠ Void **and**
- Q ≠ Void **and**
- Target(Q) ≠ Void;
**ensures** _x0001_
-  L: Location, Target(L) =
-   #Target(Q)                **if** L = P
-   #Target(#Target(Q)) **if** L = Q
-   #Target(P)                **if** L = #Target(Q)
-   #Target(L)                **otherwise**;

## Transfer Implementation

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

## Trace of Transfer

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

- P

- Q

## Trace of Transfer

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

- P

- Q

- S

- R,

## Trace of Transfer

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

- P

- Q

- R

- S

## Trace of Transfer

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

- P

- Q

- R

- S

## Trace of Transfer

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

- P

- Q

- R

- S

## Trace of Transfer

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

- P

- Q

- R

- S

## Trace of Transfer

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

- P

- Q

- S

- R

## List Component Specification

**Concept** List_Template (**type** Entry);
-     **Type** **Family** List **is** **modeled** **by**
-             ( Prec: Str(Entry)  Rem: Str(Entry) );
-         **exemplar** S;
-         **initialization ensures** S.Prec =  **and** S.Rem = ;

- L =    
- S =  1, 2   3, 4 
- T =  A, B   

## Insert Operation

**Operation** Insert(**clears** E: Entry, **updates** S: List);
-     **ensures** S.Prec = #S.Prec **and**
-                    S.Rem = #E o #S.Rem **and**
-                    E = Entry.**Init**;

- S =  1, 2   3, 4  **and** E = 6

## Insert Operation

**Operation** Insert(**clears** E: Entry, **updates** S: List);
-     **ensures** S.Prec = #S.Prec **and**
-                    S.Rem = #E o #S.Rem **and**
-                    E = Entry.**Init**;

- S =  1, 2   3, 4  **and** E = 6

- S =  1, 2   6, 3, 4  **and** E = 0

## Remove Operation

**Operation** Remove(**replaces** E: Entry, **updates** S: List);
-     **requires** S.Rem ≠ ;
-     **ensures** S.Prec = #S.Prec **and**
-                    S.Rem = ALL_BUT_FIRST(#S.Rem) **and**
-                    E = FIRST(#S.Rem);

- S =  1, 2   3, 4  **and** E = 6

## Remove Operation

**Operation** Remove(**replaces** E: Entry, **updates** S: List);
-     **requires** S.Rem ≠ ;
-     **ensures** S.Prec = #S.Prec **and**
-                    S.Rem = ALL_BUT_FIRST(#S.Rem) **and**
-                    E = FIRST(#S.Rem);

- S =  1, 2   3, 4  **and** E = 6

- S =  1, 2   4  **and** E = 3

## List Transfer Operation

**Operation** Transfer(**updates** S, T: List);
-     **requires** T.Rem ≠ ;
-     **ensures** S.Prec = #S.Prec **and**
-                    S.Rem = FIRST(#T.Rem) o #S.Rem **and**
-                    T.Prec = #T.Prec **and**
-                    T.Rem = ALL_BUT_FIRST(#T.Rem);

- S =  1   3, 4  **and**
- T =  2   6, 7 

## List Transfer Operation

**Operation** Transfer(**updates** S, T: List);
-     **requires** T.Rem ≠ ;
-     **ensures** S.Prec = #S.Prec **and**
-                    S.Rem = FIRST(#T.Rem) o #S.Rem **and**
-                    T.Prec = #T.Prec **and**
-                    T.Rem = ALL_BUT_FIRST(#T.Rem);

- S =  1   3, 4  **and**
- T =  2   6, 7 

- S =  1   6, 3, 4  **and**
- T =  2   7 

## Pointer Code vs. List Code

**Procedure** Transfer(P, Q: Position);
-     **Var** R, S: Position;
-     Relocate_to_Target(R, P);
-     Relocate_to_Target(S, Q);
-     Redirect_to_Target(Q, S);
-     Redirect_Link(P, S);
-     Redirect_Link(S, R);
**end** Transfer;

**Procedure** Transfer(S, T: List);
-     **Var** E: Entry;
-     Remove(E, T);
-     Insert(E, S);
**end** Transfer;

- Note: Model for List does not involve pointers; swapping paradigm eliminates the need to reason about pointers / aliasing / heaps at higher levels of abstraction

## Pointer VC’s vs List VC’s

- _P __≠__ Void __**and**__ Q __≠__ Void __**and**__ Target(Q) __≠__ Void_
- P ≠ Void
- _P __≠__ Void __**and**__ Q __≠__ Void __**and**__ Target(Q) __≠__ Void_
- Q ≠ Void
- _P __≠__ Void __**and**__ Q __≠__ Void __**and**__ Target(Q) __≠__ Void_
- Q ≠ Void **and** Target(Q) ≠ Void
- P ≠ Void **and** Q ≠ Void **and** Target(Q) ≠ Void **and**
- ?Target(Q) = Target(Target(Q)) **and**
- ___L: Location, __**if**__ L __≠__ Q __**then**__ ?Target(L) = Target(L)_
- P ≠ Void
- P ≠ Void **and** Q ≠ Void **and** Target(Q) ≠ Void **and**
- ?Target(Q) = Target(Target(Q)) **and**
- L: Location, **if** L ≠ Q **then** ?Target(L) = Target(L) **and**
- ??Target(P) = ?Target(Target(Q)) **and**
- ___L: Location, __**if**__ L __≠__ P __**then**__ ??Target(L) = ?Target(L)_
- Target(Q) ≠ Void
- P ≠ Void **and** Q ≠ Void **and** Target(Q) ≠ Void **and**
- ?Target(Q) = Target(Target(Q)) **and**
- L: Location, **if** L ≠ Q **then** ?Target(L) = Target(L) **and**
- ??Target(P) = ?Target(Target(Q)) **and**
- L: Location, **if** L ≠ P **then** ??Target(L) = ?Target(L) **and**
- ???Target(Target(Q)) = Target(P) **and**
- __x0001_____L: Location, __**if**__ L __≠__ Target(P) __**then**__ ???Target(L) = ??Target(L)_
- ???Target(P) = Target(Q) **and**
- ???Target(Q) = Target(Target(Q)) **and**
- ???Target(Target(Q)) = Target(P) **and**
- L: Location, (L ≠ P **and** L ≠ Q **and** L ≠ Target(Target(Q))
-     **implies** ???Target(L) = ??Target(L)

- _T.Rem __≠__ empty_string_
- T.Rem ≠ empty_string
- T.Rem ≠ empty_string **and**
- ?T.Prec = T.Prec **and** T.Rem = <E> o ?T.Rem **and**
- _?S.Prec = S.Prec __**and**__ ?S.Rem = <E> o S.Rem           _
- ?S.Prec = S.Prec **and** ?T.Prec = T.Prec **and**
- Rev(T.Rem) o S.Rem = Rev(?T.Rem) o ?S.Rem **and**
- |?S.Rem| = |S.Rem| + 1

## Library components

- Map

- List

- Pointer

- Custom components

- Array

## Verification Condition (VC) Generation

- Symbolic Reasoning Table

- Modified Symbolic Reasoning

- Verification Conditions

## Symbolic Reasoning Table

| State | Facts | Obligations |
| --- | --- | --- |
| 0 | P0 ≠ Void and Q0 ≠ Void and Target0(Q0) ≠ Void and R0 = Void and S0 = Void | P0 ≠ Void |
| Relocate_to_Target(R, P); |  |  |
| 1 | R1 = Target1(P1) and ... | Q1 ≠ Void |
| Relocate_to_Target(S, Q); |  |  |
| 2 | S0 = Target2(Q2) and ... | Q2 ≠ Void and S2 ≠ Void |
| Redirect_to_Target(Q, S); |  |  |
| 3 | Target3(Q3) = Target2(S3) andL: Location, if L ≠ Q3 then Target3(L) = Target2(L) and ... | P3 ≠ Void |
| Redirect_Link(P, S); |  |  |
| 4 | Target4(P4) = S4 and L: Location, if L ≠ P4 then Target4(L) = Target3(L) and ... | S4 ≠ Void |
| Redirect_Link(S, R); |  |  |
| 5 | Target5(S5) = R5 and L: Location, if L ≠ S5 then Target5(L) = Target4(L) and ... | Target5(P5) = Target0(Q5) and Target5(Q5) = Target0(Target0(Q5)) and Target5(Target0(Q5)) = Target0(P5) and L: Location, if L ≠ P5 and L ≠ Q5 and L ≠ Target0(Q5) then Target5(L) = Target0(L) |

## Symbolic Reasoning Table

| State | Facts | Obligations |
| --- | --- | --- |
| 0 | P0 ≠ Void and Q0 ≠ Void and Target0(Q0) ≠ Void and R0 = Void and S0 = Void | P0 ≠ Void |
| Relocate_to_Target(R, P); |  |  |
| 1 | R1 = Target1(P1) and ... | Q1 ≠ Void |
| Relocate_to_Target(S, Q); |  |  |
| 2 | S0 = Target2(Q2) and ... | Q2 ≠ Void and S2 ≠ Void |
| Redirect_to_Target(Q, S); |  |  |
| 3 | Target3(Q3) = Target2(S3) andL: Location, if L ≠ Q3 then Target3(L) = Target2(L) and ... | P3 ≠ Void |
| Redirect_Link(P, S); |  |  |
| 4 | Target4(P4) = S4 and L: Location, if L ≠ P4 then Target4(L) = Target3(L) and ... | S4 ≠ Void |
| Redirect_Link(S, R); |  |  |
| 5 | Target5(S5) = R5 and L: Location, if L ≠ S5 then Target5(L) = Target4(L) and ... | Target5(P5) = Target0(Q5) and Target5(Q5) = Target0(Target0(Q5)) and Target5(Target0(Q5)) = Target0(P5) and L: Location, if L ≠ P5 and L ≠ Q5 and L ≠ Target0(Q5) then Target5(L) = Target0(L) |

- From *requires* clause of Transfer operation

- From *ensures* clause of Transfer operation

## Symbolic Reasoning Table

| State | Facts | Obligations |
| --- | --- | --- |
| 0 | P0 ≠ Void and Q0 ≠ Void and Target0(Q0) ≠ Void and R0 = Void and S0 = Void | P0 ≠ Void |
| Relocate_to_Target(R, P); |  |  |
| 1 | R1 = Target1(P1) and ... | Q1 ≠ Void |
| Relocate_to_Target(S, Q); |  |  |
| 2 | S0 = Target2(Q2) and ... | Q2 ≠ Void and S2 ≠ Void |
| Redirect_to_Target(Q, S); |  |  |
| 3 | Target3(Q3) = Target2(S3) andL: Location, if L ≠ Q3 then Target3(L) = Target2(L) and ... | P3 ≠ Void |
| Redirect_Link(P, S); |  |  |
| 4 | Target4(P4) = S4 and L: Location, if L ≠ P4 then Target4(L) = Target3(L) and ... | S4 ≠ Void |
| Redirect_Link(S, R); |  |  |
| 5 | Target5(S5) = R5 and L: Location, if L ≠ S5 then Target5(L) = Target4(L) and ... | Target5(P5) = Target0(Q5) and Target5(Q5) = Target0(Target0(Q5)) and Target5(Target0(Q5)) = Target0(P5) and L: Location, if L ≠ P5 and L ≠ Q5 and L ≠ Target0(Q5) then Target5(L) = Target0(L) |

- From the *ensures*
- clauses of the
- previous statement

- From the *requires*
- clauses of the
- following statement

## Symbolic Reasoning Table

| State | Facts | Obligations |
| --- | --- | --- |
| 0 | P0 ≠ Void and Q0 ≠ Void and Target0(Q0) ≠ Void and R0 = Void and S0 = Void | P0 ≠ Void |
| Relocate_to_Target(R, P); |  |  |
| 1 | R1 = Target1(P1) and ... | Q1 ≠ Void |
| Relocate_to_Target(S, Q); |  |  |
| 2 | S0 = Target2(Q2) and ... | Q2 ≠ Void and S2 ≠ Void |
| Redirect_to_Target(Q, S); |  |  |
| 3 | Target3(Q3) = Target2(S3) andL: Location, if L ≠ Q3 then Target3(L) = Target2(L) and ... | P3 ≠ Void |
| Redirect_Link(P, S); |  |  |
| 4 | Target4(P4) = S4 and L: Location, if L ≠ P4 then Target4(L) = Target3(L) and ... | S4 ≠ Void |
| Redirect_Link(S, R); |  |  |
| 5 | Target5(S5) = R5 and L: Location, if L ≠ S5 then Target5(L) = Target4(L) and ... | Target5(P5) = Target0(Q5) and Target5(Q5) = Target0(Target0(Q5)) and Target5(Target0(Q5)) = Target0(P5) and L: Location, if L ≠ P5 and L ≠ Q5 and L ≠ Target0(Q5) then Target5(L) = Target0(L) |

**Operation** Redirect_Link(
-         **preserves** P: Position,
-         **preserves** Q: Position
-     );
-     **updates** Target;
-     **requires** P ≠ Void;
-     **ensures** _x0001__x0001_
-        Target(P) = Q **and**
-         L: Location,
-         **if** L ≠ P
-         **then** Target(L) =
-                 #Target(L);

*Currently defined variables:*
- P, Q, R, S, Target, Contents

## Symbolic Reasoning Table

| State | Facts | Obligations |
| --- | --- | --- |
| 0 | P0 ≠ Void and Q0 ≠ Void and Target0(Q0) ≠ Void and R0 = Void and S0 = Void | P0 ≠ Void |
| Relocate_to_Target(R, P); |  |  |
| 1 | R1 = Target1(P1) and ... | Q1 ≠ Void |
| Relocate_to_Target(S, Q); |  |  |
| 2 | S0 = Target2(Q2) and ... | Q2 ≠ Void and S2 ≠ Void |
| Redirect_to_Target(Q, S); |  |  |
| 3 | Target3(Q3) = Target2(S3) andL: Location, if L ≠ Q3 then Target3(L) = Target2(L) and ... | P3 ≠ Void |
| Redirect_Link(P, S); |  |  |
| 4 | Target4(P4) = S4 and L: Location, if L ≠ P4 then Target4(L) = Target3(L) and ... | S4 ≠ Void |
| Redirect_Link(S, R); |  |  |
| 5 | Target5(S5) = R5 and L: Location, if L ≠ S5 then Target5(L) = Target4(L) and ... | Target5(P5) = Target0(Q5) and Target5(Q5) = Target0(Target0(Q5)) and Target5(Target0(Q5)) = Target0(P5) and L: Location, if L ≠ P5 and L ≠ Q5 and L ≠ Target0(Q5) then Target5(L) = Target0(L) |

- To prove an obligation, you may use the facts from the same state and all previous states

## Proving an Obligation

- P0 ≠ Void **and** Q0 ≠ Void **and** Target0(Q0) ≠ Void **and**
- R0 = Void **and** S0 = Void
- R1 = Target1(P1) **and** P1 = P0 **and** Q1 = Q0 **and**
- S1 = S0 **and** Target1 = Target0 **and** Contents1 = Contents0
- S2 = Target2(Q2) **and** P2 = P1 **and** Q2 = Q1 **and**
- R2 = R1 **and** Target2 = Target1 **and** Contents2 = Contents1
- Target3(Q3) = Target2(S) **and**
- L: Location, **if** L ≠ Q3 **then** Target3(L) = Target2(L) **and**
- P3 = P2 **and** Q3 = Q2 **and** R3 = R2 **and** S3 = S2
**and** Contents3 = Contents2
- Target4(P4) = Target3(S4) **and**
- L: Location, **if** L ≠ P4 **then** Target4(L) = Target3(L) **and**
- P4 = P3 **and** Q4 = Q3 **and** R4 = R3 **and** S4 = S3
**and** Contents4 = Contents3

- Facts 0 – 4

- S4 ≠ Void

- Obligation 4

## Proving an Obligation

- P ≠ Void **and** Q ≠ Void **and** Target(Q) ≠ Void
- ?Target(Q) = Target(Target(Q)) **and**
- L: Location, **if** L ≠ Q **then** ?Target(L) = Target(L)
- ??Target(P) = ?Target(Target(Q)) **and**
- L: Location, **if** L ≠ P **then** ??Target(L) = ?Target(L)

- Target(Q) ≠ Void

- Facts in state 4

- Obligation 4

## Verification Condition

- P ≠ Void
- Q ≠ Void
- Target(Q) ≠ Void
- ?Target(Q) = Target(Target(Q))
- L: Location, **if** L ≠ Q **then** ?Target(L) = Target(L)
- ??Target(P) = ?Target(Target(Q))
- ___L: Location, __**if**__ L __≠__ P __**then**__ ??Target(L) = ?Target(L)_
- Target(Q) ≠ Void

## Summary

- RESOLVE reasoning -- Avoids aliasing at higher levels of abstraction; pointers treated same as other components
- OO Logics -- Variables are references to objects into a heap; frame property indicates which parts of the heap can change
- Separation Logic -- Introduces new operator (*) and proof rules that help restrict reasoning to relevant parts of the heap
- Full Functional Verification of Linked Data Structures -- Karen Zee, et al. MIT (PLDI 2008)

## Questions

-  www.cs.clemson.edu/~resolve

## Hoare-Style Proof Rules

- code; **Confirm** pre[x/a, y/b] **and**
-     ?a,?b: T, **if** post[x/?a, y/?b, #x/a, #y/b],
_**    **__**then**__ Q[a__/__?a, b__/__?b];                                    _
- code; p(a, b); **Confirm** Q;

- Apply rules in reverse order to “reduce” your assertive program to a single mathematical assertion
- Application of procedure call rule introduces universally quantified variables

## Proving an Obligation

- P ≠ Void **and** Q ≠ Void **and** Target(Q) ≠ Void **and**
- R = Target(P) **and** S = Target(Q)
- ?Target(Q) = Target(S) **and**
- L: Location, **if** L ≠ Q **then** ?Target(L) = Target(L)
- ??Target(P) = ?Target(S) **and**
- L: Location, **if** L ≠ P **then** ??Target(L) = ?Target(L)

- Facts in state 4

- S ≠ Void

- Obligation 4