Changeset 3039 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Mar 29, 2013, 5:45:14 PM (8 years ago)
Author:
tranquil
Message:
  • merged and extended MovSuccessor? and Mov in one instruction (Mov dst

ident offset)

  • JMP now correctly uses ACCDPTR argument
  • LINToASM: ADDRESS now translate to a symbolical Mov (now a preamble

is generated), and globals initialization is fixed accordingly

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r2999 r3039  
    5151(* Move next function in interpret? *)
    5252definition execute_1_pseudo_instruction':
    53  ∀cm. ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
    54  λcm,sigma,policy,status.
     53 ∀cm.(Identifier → Word) → (Identifier → Word) →
     54 ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
     55 λcm,addr_of_label,addr_of_symbol,sigma,policy,status.
    5556  execute_1_pseudo_instruction cm
    56    (ticks_of cm  sigma policy) status ….
     57   (ticks_of cm  sigma policy) addr_of_label addr_of_symbol status ….
    5758cases daemon (*CSC: we need to prove that we remain inside the program
    5859 (code closed), which is impossible in case of function pointers.
     
    6869  | Jmp _ ⇒ cl_other
    6970  | Jnz _ _ _ ⇒ cl_jump
    70   | MovSuccessor _ _ _ ⇒ cl_other
    7171  | Call _ ⇒ cl_call
    72   | Mov _ _ ⇒ cl_other ].
     72  | Mov _ _ _ ⇒ cl_other ].
    7373
    7474definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝
     
    108108
    109109definition ASM_as_call_ident:
    110  ∀prog,sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
     110 ∀prog.(Identifier → Word) → (Identifier → Word) →
     111 ∀sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
    111112
    112  λprog,sigma,policy,s0.
    113   let st ≝ execute_1_pseudo_instruction' prog sigma policy s0 in
     113 λprog,addr_of_label,addr_of_symbol,sigma,policy,s0.
     114  let st ≝ execute_1_pseudo_instruction' prog addr_of_label addr_of_symbol
     115    sigma policy s0 in
    114116  let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? (program_counter … st)) … (code prog) ? in
    115117  match lbl with
     
    122124
    123125definition ASM_abstract_status:
    124  ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
    125   λprog,sigma,policy.
     126 ∀prog:pseudo_assembly_program.
     127  (Identifier → Word) →
     128  (Identifier → Word) →
     129 ∀sigma,policy.abstract_status ≝
     130  λprog,addr_of_label,addr_of_symbol,sigma,policy.
    126131    mk_abstract_status
    127132      (PseudoStatus prog)
    128       (λs1,s2. execute_1_pseudo_instruction' … sigma policy s1 = s2)
     133      (λs1,s2. execute_1_pseudo_instruction' … addr_of_label addr_of_symbol
     134        sigma policy s1 = s2)
    129135      word_deqset
    130136      (program_counter …)
     
    133139      (ASM_next_instruction_properly_relates_program_counters prog)
    134140      (ASM_as_result …)
    135       (ASM_as_call_ident prog sigma policy …)
     141      (ASM_as_call_ident prog addr_of_label addr_of_symbol sigma policy …)
    136142      ?.
    137143 * #st whd in ⊢ (??%? → ?); cases (\fst (fetch_pseudo_instruction ???)) [*]
     
    142148 pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝
    143149 λc,sigma,policy.
     150  let label_map ≝ \fst (create_label_cost_map (code … c)) in
     151  let symbol_map ≝ construct_datalabels (preamble … c) in
     152  let addr_of_label ≝ λx.bitvector_of_nat ? (lookup_def … label_map x 0) in
     153  let addr_of_symbol ≝ λx.lookup_def … symbol_map x (addr_of_label x) in
    144154  mk_preclassified_system_of_abstract_status
    145155   (pseudo_assembly_program × (Word → Word) × (Word → bool))
    146    (ASM_abstract_status c sigma policy)
    147    (λst. return (execute_1_pseudo_instruction' … sigma policy st))
     156   (ASM_abstract_status c addr_of_label addr_of_symbol sigma policy)
     157   (λst. return (execute_1_pseudo_instruction' … addr_of_label addr_of_symbol sigma policy st))
    148158   (initialise_status … c).
Note: See TracChangeset for help on using the changeset viewer.