 Timestamp:
 Jun 13, 2012, 5:54:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r2064 r2065 22 22 iteration of the fixed point computation; and finally, we can prove some 23 23 properties of the fixed point. 24 25 The invariants for the fold function. Note that during the fixed point 26 computation, the $sigma$ functions are implemented as tries, so in order to 27 compute $sigma(i)$, we lookup the value for $i$ in the corresponding trie. 28 29 \begin{lstlisting} 30 (out_of_program_none prefix policy) $\wedge$ 31 (jump_not_in_policy prefix policy) $\wedge$ 32 (policy_increase prefix old_sigma policy) $\wedge$ 33 (policy_compact_unsafe prefix labels policy) $\wedge$ 34 (policy_safe prefix labels added old_sigma policy) $\wedge$ 35 (\fst (bvt_lookup $\ldots$ 36 (bitvector_of_nat ? 0) (\snd policy) $\langle$0,short_jump$\rangle$) = 0) $\wedge$ 37 (\fst policy = \fst (bvt_lookup $\ldots$ 38 (bitvector_of_nat ? (prefix)) (\snd policy) $\langle$0,short_jump$\rangle$)) $\wedge$ 39 (added = 0 → policy_pc_equal prefix old_sigma policy) $\wedge$ 40 (policy_jump_equal prefix old_sigma policy → added = 0) 41 \end{lstlisting} 42 43 These invariants have the following meanings: 44 45 \begin{itemize} 46 \item {\tt out\_of\_program\_none} shows that if we try to lookup a value 47 beyond the program, we will get an empty result; 48 \item {\tt jump\_not\_in\_policy} shows that an instruction that is not a jump 49 will have a {\tt short\_jump} as its associated jump length; 50 \item {\tt policy\_increase} shows that between iterations, jumps either increase (i.e. from {\tt short\_jump} to {\tt medium\_jump} or from {\tt medium\_jump} to {\tt long\_jump}) or remain equal; 51 \item {\tt policy\_compact\_unsafe} shows that the policy is compact (instrucftions directly follow each other and do not overlap); 52 \item {\tt policy\_safe} shows that jumps selected are appropriate for the 53 distance between their position and their target, and the jumps selected are 54 the smallest possible; 55 \item Then there are two properties that fix the values of $\sigma(0)$ and 56 $\sigma(n)$ (with $n$ the size of the program); 57 \item And finally two predicates that link the value of $added$ to reaching 58 of a fixed point. 59 \end{itemize} 60 61 \begin{lstlisting} 62 ($\Sigma$x:bool × (option ppc_pc_map). 63 let $\langle$no_ch,y$\rangle$ := x in 64 match y with 65 [ None ⇒ nec_plus_ultra program old_policy 66  Some p ⇒ (out_of_program_none program p) $\wedge$ 67 (jump_not_in_policy program p) $\wedge$ 68 (policy_increase program old_policy p) $\wedge$ 69 (no_ch = true → policy_compact program labels p) $\wedge$ 70 (\fst (bvt_lookup $\ldots$ 71 (bitvector_of_nat ? 0) (\snd p) $\langle$0,short_jump$\rangle$) = 0) $\wedge$ 72 (\fst p = \fst (bvt_lookup $\ldots$ 73 (bitvector_of_nat ? (program)) (\snd p) $\langle$0,short_jump$\rangle$)) $\wedge$ 74 (no_ch = true $\rightarrow$ policy_pc_equal program old_policy p) $\wedge$ 75 (policy_jump_equal program old_policy p $\rightarrow$ no_ch = true) $\wedge$ 76 (\fst p < 2^16) 77 ]) 78 \end{lstlisting} 24 79 25 80 The main correctness statement, then, is as follows:
Note: See TracChangeset
for help on using the changeset viewer.