Changeset 3341
 Timestamp:
 Jun 7, 2013, 6:26:15 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r3338 r3341 6 6 7 7 \begin{align*} 8 \math rm{sigma\_policy\_specification} \equiv8 \mathtt{sigma\_policy\_specification} \equiv 9 9 \lambda program.\lambda sigma.\lambda policy. \notag\\ 10 10 sigma\ 0 = 0\ \wedge \notag\\ … … 12 12 \forall ppc.ppc < instr\_list \rightarrow \notag\\ 13 13 \mathbf{let}\ pc \equiv sigma\ ppc\ \mathbf{in} \notag\\ 14 \mathbf{let}\ instruction \equiv \math rm{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\14 \mathbf{let}\ instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\ 15 15 \mathbf{let}\ next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\ 16 next\_pc = pc + \math rm{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\17 (pc + \math rm{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\16 next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\ 17 (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\ 18 18 (\forall ppc'.ppc' < instr\_list \rightarrow ppc < ppc' \rightarrow \notag\\ 19 \mathbf{let}\ instruction' \equiv \math rm{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\20 \math rm{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\21 pc + \math rm{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})19 \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\ 20 \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\ 21 pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}) 22 22 \end{align*} 23 23 … … 70 70 consisting of the current size of the program and our $\sigma$ function. 71 71 72 \begin{lstlisting} 73 definition out_of_program_none := 74 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. 75 $\forall$i.i < 2^16 $\rightarrow$ (i > prefix $\leftrightarrow$ 76 bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?). 77 \end{lstlisting} 72 \begin{align*} 73 \mathtt{out\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\ 74 \forall i.i < 2^{16} \rightarrow (i > prefix \leftrightarrow 75 \mathtt{lookup\_opt}\ i\ sigma = \mathtt{None}) 76 \end{align*} 78 77 79 78 This invariant states that any pseudoaddress not yet examined is not 80 79 present in the lookup trie. 81 80 82 \begin{lstlisting} 83 definition not_jump_default := 84 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. 85 $\forall$i.i < prefix $\rightarrow$ 86 ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) $\rightarrow$ 87 \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) 88 $\langle$0,short_jump$\rangle$) = short_jump. 89 \end{lstlisting} 81 \begin{align*} 82 \mathtt{not\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\ 83 \forall i.i < prefix \rightarrow\notag\\ 84 \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\ 85 \mathtt{lookup}\ i\ sigma = \mathtt{short\_jump} 86 \end{align*} 90 87 91 88 This invariant states that when we try to look up the jump length of a … … 93 90 value, a short jump. 94 91 95 \begin{lstlisting} 96 definition jump_increase := 97 $\lambda$prefix:list labelled_instruction.$\lambda$op:ppc_pc_map.$\lambda$p:ppc_pc_map. 98 $\forall$i.i $\leq$ prefix $\rightarrow$ 99 let $\langle$opc,oj$\rangle$ := 100 bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in 101 let $\langle$pc,j$\rangle$ := 102 bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd p) $\langle$0,short_jump$\rangle$ in 103 jmpleq oj j. 104 \end{lstlisting} 92 \begin{align*} 93 \mathtt{jump\_increase} \equiv \lambda pc.\lambda op\lambda p. 94 \forall i.i < prefix \rightarrow\notag\\ 95 \mathbf{let}\ oj \equiv \mathtt{lookup}\ i\ op\ \mathbf{in} \notag\\ 96 \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ p\ \mathbf{in} \notag\\ 97 \mathtt{jmpleq}\ oj\ j 98 \end{align*} 105 99 106 100 This invariant states that between iterations (with $op$ being the previous … … 108 102 increase. It is needed for proving termination. 109 103 110 \clearpage 111 \begin{lstlisting} 112 definition sigma_compact_unsafe := 113 $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map. 114 $\forall$n.n < program $\rightarrow$ 115 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with 116 [ None $\Rightarrow$ False 117  Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in 118 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with 119 [ None $\Rightarrow$ False 120  Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in 121 pc1 = pc + instruction_size_jmplen j 122 (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$))) 123 ] 124 ]. 125 \end{lstlisting} 104 \begin{align*} 105 \mathtt{sigma\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.\notag\\ 106 \forall n.n < prefix \rightarrow\notag\\ 107 \mathbf{match}\ \mathtt{lookup\_opt}\ n\ sigma\ \mathbf{with}\notag\\ 108 \mathtt{None} \Rightarrow \mathrm{False} \notag\\ 109 \mathtt{Some}\ \langle pc, j \rangle \Rightarrow 110 \mathbf{match}\ \mathtt{lookup\_opt}\ (n+1)\ sigma\ \mathbf{with}\notag\\ 111 \mathtt{None} \Rightarrow \mathrm{False} \notag\\ 112 \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow 113 pc_1 = pc + \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix) 114 \end{align*} 126 115 127 116 This is a temporary formulation of the main property\\ … … 135 124 property. 136 125 137 \begin{lstlisting} 138 definition sigma_safe := 139 $\lambda$prefix:list labelled_instruction.$\lambda$labels:label_map.$\lambda$added:$\mathbb{N}$. 140 $\lambda$old_sigma:ppc_pc_map.$\lambda$sigma:ppc_pc_map. 141 $\forall$i.i < prefix $\rightarrow$ let $\langle$pc,j$\rangle$ := 142 bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in 143 let pc_plus_jmp_length := bitvector_of_nat ? (\fst (bvt_lookup $\ldots$ 144 (bitvector_of_nat ? (S i)) (\snd sigma) $\langle$0,short_jump$\rangle$)) in 145 let $\langle$label,instr$\rangle$ := nth i ? prefix $\langle$None ?, Comment [ ]$\rangle$ in 146 $\forall$dest.is_jump_to instr dest $\rightarrow$ 147 let paddr := lookup_def $\ldots$ labels dest 0 in 148 let addr := bitvector_of_nat ? (if leb i paddr (* forward jump *) 149 then \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd old_sigma) 150 $\langle$0,short_jump$\rangle$) + added 151 else \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd sigma) 152 $\langle$0,short_jump$\rangle$)) in 153 match j with 154 [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$ 155 \fst (short_jump_cond pc_plus_jmp_length addr) = true 156  absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$ 157 \fst (absolute_jump_cond pc_plus_jmp_length addr) = true $\wedge$ 158 \fst (short_jump_cond pc_plus_jmp_length addr) = false 159  long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false 160 $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = false 161 ]. 162 \end{lstlisting} 126 \begin{align*} 127 \mathtt{sigma\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma\notag\\ 128 \forall i.i < prefix \rightarrow \notag\\ 129 \mathbf{let}\ instr \equiv \mathtt{nth}\ i\ prefix\ \mathbf{in}\notag\\ 130 \forall dest\_label.\mathtt{is\_jump\_to\_instr}\ dest\_label \rightarrow\notag\\ 131 \mathbf{let}\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in} \notag\\ 132 \mathbf{let}\ \langle j, src, dest \rangle \equiv\notag\\ 133 \mathbf{if}\ paddr\ \leq\ i\ \mathbf{then}\notag\\ 134 \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ sigma\ \mathbf{in} \notag\\ 135 \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ sigma\ \mathbf{in}\notag\\ 136 \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ sigma\ \mathbf{in}\notag\\ 137 \langle j, pc\_plus\_jl, addr \rangle\notag\\ 138 \mathbf{else} \\ 139 \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ sigma\ \mathbf{in} \notag\\ 140 \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ old\_sigma\ \mathbf{in}\notag\\ 141 \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ old\_sigma\ \mathbf{in}\notag\\ 142 \langle j, pc\_plus\_jl, addr \rangle\ \mathbf{in}\notag\\ 143 \mathbf{match}\ j\ \mathbf{with} \notag\\ 144 \mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\ 145 \mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\ 146 \mathrm{long\_jump} \Rightarrow \mathrm{True} 147 \end{align*} 163 148 164 149 This is a more direct safety property: it states that branch instructions are
Note: See TracChangeset
for help on using the changeset viewer.