中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第7章 程序验证 ProgramVerification Necula 02 Finish Verification Condition Generation Simple Prover for FOL

Finish Verification Condition Generation Simple Prover for FOL CS294-8 Lecture 10 Prof.Necula CS 294-8 Lecture 10 1

Prof. Necula CS 294-8 Lecture 10 1 Finish Verification Condition Generation Simple Prover for FOL CS 294-8 Lecture 10

Not Quite Weakest Preconditions Recall what we are trying to do: false → frue Pre(s,B) strong ↑1 weak weakest A precondition:WP(s,B) verification condition:VC(s,B) We shall construct a verification condition:VC(s,B) The loops are annotated with loop invariants VC is guaranteed stronger than WP But hopefully still weaker than A:A>VC(s,B)WP(s,B) Prof.Necula CS 294-8 Lecture 10 2

Prof. Necula CS 294-8 Lecture 10 2 Not Quite Weakest Preconditions • Recall what we are trying to do: false  true strong weak Pre(s, B) weakest A precondition: WP(s, B) verification condition: VC(s, B) • We shall construct a verification condition: VC(s, B) – The loops are annotated with loop invariants ! – VC is guaranteed stronger than WP – But hopefully still weaker than A: A  VC(s, B)  WP(s, B)

Verification Condition Generation Computed in a manner similar to WP 。 Except the rule for while: VC(whiler E do s,B)= IA(X1Xn.I→(E→VC(s,I)AE→B)) I holds I is preserved in B holds when the on entry an arbitrary iteration loop terminates I is the loop invariant (provided externally) X1,...Xn are all the variables modified in s The V is similar to the V in mathematical induction: P(O)An∈N.P(n)→P(n+1) Prof.Necula CS 294-8 Lecture 10 3

Prof. Necula CS 294-8 Lecture 10 3 Verification Condition Generation • Computed in a manner similar to WP • Except the rule for while: VC(whileI E do s, B) = I  (x1…xn . I  (E  VC(s, I)   E  B) ) • I is the loop invariant (provided externally) • x1 , …, xn are all the variables modified in s • The  is similar to the  in mathematical induction: P(0) n  N. P(n)  P(n+1) I holds on entry I is preserved in an arbitrary iteration B holds when the loop terminates

Forward Verification Condition Generation Traditionally VC is computed backwards Works well for structured code o But it can be computed in a forward direction Works even for low-level languages (e.g.,assembly language) Uses symbolic evaluation(important technique #2) Has broad applications in program analysis e.g.the PREfix tools works this way Prof.Necula CS 294-8 Lecture 10 4

Prof. Necula CS 294-8 Lecture 10 4 Forward Verification Condition Generation • Traditionally VC is computed backwards – Works well for structured code • But it can be computed in a forward direction – Works even for low-level languages (e.g., assembly language) – Uses symbolic evaluation (important technique #2) – Has broad applications in program analysis • e.g. the PREfix tools works this way

Symbolic Evaluation Consider the language: x:=E I f()I if E goto L goto LL:return I inv E The "inv E"instruction is an annotation Says that boolean expression E holds at that point Notation:Ik is the instruction at address k Prof.Necula CS 294-8 Lecture 10 5

Prof. Necula CS 294-8 Lecture 10 5 Symbolic Evaluation • Consider the language: x := E | f() | if E goto L | goto L | L: | return | inv E • The “inv E” instruction is an annotation – Says that boolean expression E holds at that point • Notation: Ik is the instruction at address k

Symbolic Evaluation.The State. We set up a symbolic evaluation state: ∑：VarU{u}→SymbolicExpressions (X) the symbolic value of x in state X[x:=E]=a new state in which x's value is E We shall use states also as substitutions: ∑(E)-obtained from E by replacing×with(x) Prof.Necula CS 294-8 Lecture 10 6

Prof. Necula CS 294-8 Lecture 10 6 Symbolic Evaluation. The State. • We set up a symbolic evaluation state: S : Var  { m } → SymbolicExpressions S(x) = the symbolic value of x in state S S[x:=E] = a new state in which x’s value is E We shall use states also as substitutions: S(E) - obtained from E by replacing x with S(x)

Symbolic Evaluation.The Invariants. The symbolic evaluator keeps track of the encountered invariants Inv c{1...n} ·Ifk∈Inv then Ik is an invariant instruction that we have already executed Basic idea:execute an inv instruction only twice: The first time it is encountered And one more time around an arbitrary iteration Prof.Necula CS 294-8 Lecture 10 7

Prof. Necula CS 294-8 Lecture 10 7 Symbolic Evaluation. The Invariants. • The symbolic evaluator keeps track of the encountered invariants Inv  {1…n} • If k  Inv then – Ik is an invariant instruction that we have already executed • Basic idea: execute an inv instruction only twice: – The first time it is encountered – And one more time around an arbitrary iteration

Symbolic Evaluation.Rules. Define a VC function as an interpreter: VC:1..n x SymbolicState x InvariantState>Predicate VCL,Σ，Inv) if Ik=goto L E=VC(L,Σ，Inv)A -E三VCk+1,Σ，Inm) if Ik=if E goto L VC(k+1,[x:=(E)],Inv) ifIk=×=E VC(k,Σ，In= ∑(Post current)) if Ik=return Σ(Pre)N a1am.'(Postf)→VC(k+1,,Inv） (where y1,..Ym are modified by f) if Ik=f() and a1,..am are fresh parameters and '=[y1:=a1,...ym :am] Prof.Necula CS 294-8 Lecture 10 8

Prof. Necula CS 294-8 Lecture 10 8 Symbolic Evaluation. Rules. • Define a VC function as an interpreter: VC : 1..n  SymbolicState  InvariantState → Predicate VC(k, S, Inv) = VC(L, S, Inv) if Ik = goto L E  VC(L, S, Inv)   E  VC(k+1, S, Inv) if Ik = if E goto L VC(k+1, S[x:=S(E)], Inv) if Ik = x := E S(Postcurrent) if Ik = return S(Pref )   a1 ..am.S’(Postf )  VC(k+1, S’, Inv) (where y1 , …, ym are modified by f) and a1 , …, am are fresh parameters and S’ = S[y1 := a1 , …, ym := am] if Ik = f()

Symbolic Evaluation.Invariants. Two cases when seeing an invariant instruction: 1.We see the invariant for the first time Ik inv E. kg Inv Let fy1,...,ym}=the variables that could be modified on a path from the invariant back to itself Let a1....,am fresh new symbolic parameters VC(k,∑，Inv)= Σ(E)A∀a1.am.'(E)→VC(k+1,,InvU{k) with >'>[y1 :a1,...,Ym :am] Prof.Necula CS 294-8 Lecture 10 9

Prof. Necula CS 294-8 Lecture 10 9 Symbolic Evaluation. Invariants. Two cases when seeing an invariant instruction: 1. We see the invariant for the first time – Ik = inv E. – k  Inv – Let {y1 , …, ym} = the variables that could be modified on a path from the invariant back to itself – Let a1 , …, am fresh new symbolic parameters VC(k, S, Inv) = S(E)  a1…am. S’(E)  VC(k+1, S’, Inv  {k}) with S’ = S[y1 := a1 , …, ym := am]

Symbolic Evaluation.Invariants. 2.We see the invariant for the second time Ik=inv E ke Inv VC(k,∑，Inm)=(E) Some tools take a more simplistic approach Do not require invariants Iterate through the loop a fixed number of times PREfix (iterates 2 times),versions of ESC (Compaq SRC) Sacrifice completeness for usability Prof.Necula CS 294-8 Lecture 10 10

Prof. Necula CS 294-8 Lecture 10 10 Symbolic Evaluation. Invariants. 2. We see the invariant for the second time – Ik = inv E – k  Inv VC(k, S, Inv) = S(E) • Some tools take a more simplistic approach – Do not require invariants – Iterate through the loop a fixed number of times – PREfix (iterates 2 times), versions of ESC (Compaq SRC) – Sacrifice completeness for usability