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