Ignore:
Timestamp:
Jun 14, 2012, 11:57:51 AM (7 years 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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/proof.tex

    r2065 r2080  
    8181
    8282\begin{lstlisting}
    83 definition jump_expansion':
    84 $\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (|l|) < 2^16).
    85  option ($\Sigma$sigma:Word → Word $\times$ bool.
    86   $\forall$ppc: Word.$\forall$ppc_ok.
    87    let pc := \fst (sigma ppc) in
    88    let labels := \fst (create_label_cost_map (\snd program)) in
    89    let lookup_labels :=
    90     $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
    91    let instruction :=
    92     \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
    93    let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
    94     And (nat_of_bitvector $\ldots$ ppc $\leq$ |\snd program| →
    95      next_pc = add ? pc (bitvector_of_nat $\ldots$
    96       (instruction_size lookup_labels ($\lambda$x.\fst (sigma x))
    97        ($\lambda$x.\snd (sigma x)) ppc instruction))
    98     )
    99     (Or (nat_of_bitvector $\ldots$ ppc < |\snd program| →
    100      nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
    101     (nat_of_bitvector $\ldots$ ppc = |\snd program| → next_pc = (zero $\ldots$))))
     83definition sigma_policy_specification :=:
     84$\lambda$program: pseudo_assembly_program.
     85$\lambda$sigma: Word → Word.
     86$\lambda$policy: Word → bool.
     87 sigma (zero $\ldots$) = zero $\ldots$ $\wedge$
     88 $\forall$ppc: Word.$\forall$ppc_ok.
     89 let instr_list := \snd program in
     90 let pc ≝ sigma ppc in
     91 let labels := \fst (create_label_cost_map (\snd program)) in
     92 let lookup_labels :=
     93  $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
     94 let instruction :=
     95  \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
     96 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
     97  (nat_of_bitvector $\ldots$ ppc ≤ |instr_list| →
     98   next_pc = add 16 pc (bitvector_of_nat $\ldots$
     99   (instruction_size lookup_labels sigma policy ppc instruction)))
     100  $\wedge$     
     101  ((nat_of_bitvector $\ldots$ ppc < |instr_list| →
     102   nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
     103  $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| → next_pc = (zero $\ldots$))).
    102104\end{lstlisting}
    103105
     
    113115address can be zero (this is the case where the program size is exactly equal
    114116to the amount of memory).
     117
     118And finally, we enforce that the program starts at address 0, i.e.
     119$\sigma(0) = 0$.
Note: See TracChangeset for help on using the changeset viewer.