Changeset 2080 for src/ASM/CPP2012-policy/proof.tex

Timestamp:

06/14/12 11:57:51 (11 months ago)

Author:

boender

Message:

- added references to SDCC and gcc (thanks, Dominic)
- updated sigma policy specification
- changed description of SDCC algorithm to actual SDCC behaviour

Files:

• src/ASM/CPP2012-policy/proof.tex (modified) (2 diffs)

src/ASM/CPP2012-policy/proof.tex

@@ -81 +81 @@
 
 \begin{lstlisting}
-definition jump_expansion':
-$\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (|l|) < 2^16).
- option ($\Sigma$sigma:Word → Word $\times$ bool.
-  $\forall$ppc: Word.$\forall$ppc_ok.
-   let pc := \fst (sigma ppc) in
-   let labels := \fst (create_label_cost_map (\snd program)) in
-   let lookup_labels :=
-    $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
-   let instruction :=
-    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
-   let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
-    And (nat_of_bitvector $\ldots$ ppc $\leq$ |\snd program| →
-     next_pc = add ? pc (bitvector_of_nat $\ldots$
-      (instruction_size lookup_labels ($\lambda$x.\fst (sigma x))
-       ($\lambda$x.\snd (sigma x)) ppc instruction))
-    )
-    (Or (nat_of_bitvector $\ldots$ ppc < |\snd program| →
-     nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
-    (nat_of_bitvector $\ldots$ ppc = |\snd program| → next_pc = (zero $\ldots$)))) 
+definition sigma_policy_specification :=:
+$\lambda$program: pseudo_assembly_program.
+$\lambda$sigma: Word → Word.
+$\lambda$policy: Word → bool.
+ sigma (zero $\ldots$) = zero $\ldots$ $\wedge$
+ $\forall$ppc: Word.$\forall$ppc_ok.
+ let instr_list := \snd program in
+ let pc ≝ sigma ppc in
+ let labels := \fst (create_label_cost_map (\snd program)) in
+ let lookup_labels :=
+  $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
+ let instruction :=
+  \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
+ let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
+  (nat_of_bitvector $\ldots$ ppc ≤ |instr_list| →
+   next_pc = add 16 pc (bitvector_of_nat $\ldots$
+   (instruction_size lookup_labels sigma policy ppc instruction)))
+  $\wedge$     
+  ((nat_of_bitvector $\ldots$ ppc < |instr_list| →
+   nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
+  $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| → next_pc = (zero $\ldots$))).
 \end{lstlisting}
 
@@ -113 +115 @@
 address can be zero (this is the case where the program size is exactly equal
 to the amount of memory).
+
+And finally, we enforce that the program starts at address 0, i.e.
+$\sigma(0) = 0$.