Changeset 1939 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 14, 2012, 10:37:08 AM (8 years ago)
Author:
mulligan
Message:

Changes to get things to compile and to avoid the dependency circularity between ASM/Interpret.ma and common/StructuredTraces.ma. New file ASM/AbstractStatus.ma factors out the definition (not the implementation!) of an abstract status, which both of the previously mentioned files require.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1938 r1939  
    22include "ASM/StatusProofs.ma".
    33include "ASM/Fetch.ma".
    4 include "common/StructuredTraces.ma".
     4include "ASM/AbstractStatus.ma".
    55
    66definition sign_extension: Byte → Word ≝
     
    120120include alias "arithmetics/nat.ma".
    121121include alias "ASM/BitVectorTrie.ma".
    122 
    123 definition ASM_classify00: ∀a. preinstruction a → status_class ≝
    124   λa, pre.
    125   match pre with
    126   [ RET ⇒ cl_return
    127   | RETI ⇒ cl_return
    128   | JZ _ ⇒ cl_jump
    129   | JNZ _ ⇒ cl_jump
    130   | JC _ ⇒ cl_jump
    131   | JNC _ ⇒ cl_jump
    132   | JB _ _ ⇒ cl_jump
    133   | JNB _ _ ⇒ cl_jump
    134   | JBC _ _ ⇒ cl_jump
    135   | CJNE _ _ ⇒ cl_jump
    136   | DJNZ _ _ ⇒ cl_jump
    137   | _ ⇒ cl_other
    138   ].
    139 
    140 definition ASM_classify0: instruction → status_class ≝
    141   λi.
    142   match i with
    143    [ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
    144    | ACALL _ ⇒ cl_call
    145    | LCALL _ ⇒ cl_call
    146    | JMP _ ⇒ cl_call
    147    | AJMP _ ⇒ cl_other
    148    | LJMP _ ⇒ cl_other
    149    | SJMP _ ⇒ cl_other
    150    | _ ⇒ cl_other
    151    ].
    152 
    153 definition current_instruction0 ≝
    154   λcode_memory: BitVectorTrie Byte 16.
    155   λprogram_counter: Word.
    156     \fst (\fst (fetch … code_memory program_counter)).
    157 
    158 definition current_instruction ≝
    159   λcode_memory.
    160   λs: Status code_memory.
    161     current_instruction0 code_memory (program_counter … s).
    162    
    163 definition current_instruction_label ≝
    164   λcode_memory.
    165   λcost_labels: BitVectorTrie costlabel 16.
    166   λs: Status code_memory.
    167   let pc ≝ program_counter … code_memory s in
    168     lookup_opt … pc cost_labels.
    169 
    170 definition next_instruction_properly_relates_program_counters ≝
    171   λcode_memory.
    172   λbefore: Status code_memory.
    173   λafter : Status code_memory.
    174     let program_counter_before ≝ program_counter ? code_memory before in
    175     let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
    176       program_counter ? code_memory after = program_counter_after.
    177 
    178 definition word_deqset: DeqSet ≝
    179   mk_DeqSet Word (eq_bv 16) ?.
    180   @refl_iff_eq_bv_true
    181 qed.
    182    
    183 definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
    184   λcode_memory.
    185   λs: Status code_memory.
    186     ASM_classify0 (current_instruction … s).
    187122
    188123definition execute_1_preinstruction':
Note: See TracChangeset for help on using the changeset viewer.