Changeset 1648 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Jan 18, 2012, 11:01:14 AM (8 years ago)
Author:
mulligan
Message:

new version of utilities/monad.ma with typecheck command comented out

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1620 r1648  
    66include alias "arithmetics/nat.ma".
    77include alias "basics/logic.ma".
     8
     9definition current_instruction0 ≝
     10  λcode_memory: BitVectorTrie Byte 16.
     11  λprogram_counter: Word.
     12    \fst (\fst (fetch … code_memory program_counter)).
     13
     14definition current_instruction ≝
     15  λs: Status.
     16    current_instruction0 (code_memory … s) (program_counter … s).
     17
     18definition ASM_classify0: instruction → status_class ≝
     19  λi: instruction.
     20    match i with
     21     [ RealInstruction pre ⇒
     22       match pre with
     23        [ RET ⇒ cl_return
     24        | JZ _ ⇒ cl_jump
     25        | JNZ _ ⇒ cl_jump
     26        | JC _ ⇒ cl_jump
     27        | JNC _ ⇒ cl_jump
     28        | JB _ _ ⇒ cl_jump
     29        | JNB _ _ ⇒ cl_jump
     30        | JBC _ _ ⇒ cl_jump
     31        | CJNE _ _ ⇒ cl_jump
     32        | DJNZ _ _ ⇒ cl_jump
     33        | _ ⇒ cl_other
     34        ]
     35     | ACALL _ ⇒ cl_call
     36     | LCALL _ ⇒ cl_call
     37     | JMP _ ⇒ cl_call
     38     | AJMP _ ⇒ cl_jump
     39     | LJMP _ ⇒ cl_jump
     40     | SJMP _ ⇒ cl_jump
     41     | _ ⇒ cl_other
     42     ].
     43
     44definition ASM_classify: Status → status_class ≝
     45 λs: Status.
     46   ASM_classify0 (current_instruction s).
    847
    948let rec compute_max_trace_label_label_cost
Note: See TracChangeset for help on using the changeset viewer.