# Changeset 3341

Ignore:
Timestamp:
Jun 7, 2013, 6:26:15 PM (6 years ago)
Message:
• more notation stuff (still needs work!)
File:
1 edited

### Legend:

Unmodified
 r3338 \begin{align*} \mathrm{sigma\_policy\_specification} \equiv \mathtt{sigma\_policy\_specification} \equiv \lambda program.\lambda sigma.\lambda policy. \notag\\ sigma\ 0 = 0\ \wedge \notag\\ \forall ppc.ppc < |instr\_list| \rightarrow \notag\\ \mathbf{let}\ pc \equiv sigma\ ppc\ \mathbf{in} \notag\\ \mathbf{let}\ instruction \equiv \mathrm{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\ \mathbf{let}\ instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\ \mathbf{let}\ next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\ next\_pc = pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\ (pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\ next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\ (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\ (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\ \mathbf{let}\ instruction' \equiv \mathrm{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\ \mathrm{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\ pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}) \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\ pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}) \end{align*} consisting of the current size of the program and our $\sigma$ function. \begin{lstlisting} definition out_of_program_none := $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. $\forall$i.i < 2^16 $\rightarrow$ (i > |prefix| $\leftrightarrow$ bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?). \end{lstlisting} \begin{align*} \mathtt{out\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\ \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow \mathtt{lookup\_opt}\ i\ sigma = \mathtt{None}) \end{align*} This invariant states that any pseudo-address not yet examined is not present in the lookup trie. \begin{lstlisting} definition not_jump_default := $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. $\forall$i.i < |prefix| $\rightarrow$ ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) $\rightarrow$ \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$) = short_jump. \end{lstlisting} \begin{align*} \mathtt{not\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\ \forall i.i < |prefix| \rightarrow\notag\\ \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\ \mathtt{lookup}\ i\ sigma = \mathtt{short\_jump} \end{align*} This invariant states that when we try to look up the jump length of a value, a short jump. \begin{lstlisting} definition jump_increase := $\lambda$prefix:list labelled_instruction.$\lambda$op:ppc_pc_map.$\lambda$p:ppc_pc_map. $\forall$i.i $\leq$ |prefix| $\rightarrow$ let $\langle$opc,oj$\rangle$ := bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in let $\langle$pc,j$\rangle$ := bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd p) $\langle$0,short_jump$\rangle$ in jmpleq oj j. \end{lstlisting} \begin{align*} \mathtt{jump\_increase} \equiv \lambda pc.\lambda op\lambda p. \forall i.i < |prefix| \rightarrow\notag\\ \mathbf{let}\ oj \equiv \mathtt{lookup}\ i\ op\ \mathbf{in} \notag\\ \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ p\ \mathbf{in} \notag\\ \mathtt{jmpleq}\ oj\ j \end{align*} This invariant states that between iterations (with $op$ being the previous increase. It is needed for proving termination. \clearpage \begin{lstlisting} definition sigma_compact_unsafe := $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map. $\forall$n.n < |program| $\rightarrow$ match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with [ None $\Rightarrow$ False | Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with [ None $\Rightarrow$ False | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in pc1 = pc + instruction_size_jmplen j (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$))) ] ]. \end{lstlisting} \begin{align*} \mathtt{sigma\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.\notag\\ \forall n.n < |prefix| \rightarrow\notag\\ \mathbf{match}\ \mathtt{lookup\_opt}\ n\ sigma\ \mathbf{with}\notag\\ \mathtt{None} \Rightarrow \mathrm{False} \notag\\ \mathtt{Some}\ \langle pc, j \rangle \Rightarrow \mathbf{match}\ \mathtt{lookup\_opt}\ (n+1)\ sigma\ \mathbf{with}\notag\\ \mathtt{None} \Rightarrow \mathrm{False} \notag\\ \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow pc_1 = pc + \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix) \end{align*} This is a temporary formulation of the main property\\ property. \begin{lstlisting} definition sigma_safe := $\lambda$prefix:list labelled_instruction.$\lambda$labels:label_map.$\lambda$added:$\mathbb{N}$. $\lambda$old_sigma:ppc_pc_map.$\lambda$sigma:ppc_pc_map. $\forall$i.i < |prefix| $\rightarrow$ let $\langle$pc,j$\rangle$ := bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in let pc_plus_jmp_length := bitvector_of_nat ?  (\fst (bvt_lookup $\ldots$ (bitvector_of_nat ? (S i)) (\snd sigma) $\langle$0,short_jump$\rangle$)) in let $\langle$label,instr$\rangle$ := nth i ? prefix $\langle$None ?, Comment [ ]$\rangle$ in $\forall$dest.is_jump_to instr dest $\rightarrow$ let paddr := lookup_def $\ldots$ labels dest 0 in let addr := bitvector_of_nat ? (if leb i paddr (* forward jump *) then \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd old_sigma) $\langle$0,short_jump$\rangle$) + added else \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd sigma) $\langle$0,short_jump$\rangle$)) in match j with [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$ \fst (short_jump_cond pc_plus_jmp_length addr) = true | absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true $\wedge$ \fst (short_jump_cond pc_plus_jmp_length addr) = false | long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = false ]. \end{lstlisting} \begin{align*} \mathtt{sigma\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma\notag\\ \forall i.i < |prefix| \rightarrow \notag\\ \mathbf{let}\ instr \equiv \mathtt{nth}\ i\ prefix\ \mathbf{in}\notag\\ \forall dest\_label.\mathtt{is\_jump\_to\_instr}\ dest\_label \rightarrow\notag\\ \mathbf{let}\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in} \notag\\ \mathbf{let}\ \langle j, src, dest \rangle \equiv\notag\\ \mathbf{if}\ paddr\ \leq\ i\ \mathbf{then}\notag\\ \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ sigma\ \mathbf{in} \notag\\ \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ sigma\ \mathbf{in}\notag\\ \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ sigma\ \mathbf{in}\notag\\ \langle j, pc\_plus\_jl, addr \rangle\notag\\ \mathbf{else} \\ \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ sigma\ \mathbf{in} \notag\\ \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ old\_sigma\ \mathbf{in}\notag\\ \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ old\_sigma\ \mathbf{in}\notag\\ \langle j, pc\_plus\_jl, addr \rangle\ \mathbf{in}\notag\\ \mathbf{match}\ j\ \mathbf{with} \notag\\ \mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\ \mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\ \mathrm{long\_jump} \Rightarrow \mathrm{True} \end{align*} This is a more direct safety property: it states that branch instructions are