source: src/ASM/AbstractStatus.ma @ 2498

Last change on this file since 2498 was 2498, checked in by mckinna, 7 years ago

Refactor:
Typedefs object_code and costlabel_map lifted out from ASMCostsSplit.ma
Dependencies simplified.

File size: 2.0 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Status.ma".
3include "ASM/Fetch.ma".
4include "common/StructuredTraces.ma".
5
6include "basics/lists/listb.ma".
7
8definition ASM_classify00: ∀a. preinstruction a → status_class ≝
9  λa, pre.
10  match pre with
11  [ RET ⇒ cl_return
12  | RETI ⇒ cl_return
13  | JZ _ ⇒ cl_jump
14  | JNZ _ ⇒ cl_jump
15  | JC _ ⇒ cl_jump
16  | JNC _ ⇒ cl_jump
17  | JB _ _ ⇒ cl_jump
18  | JNB _ _ ⇒ cl_jump
19  | JBC _ _ ⇒ cl_jump
20  | CJNE _ _ ⇒ cl_jump
21  | DJNZ _ _ ⇒ cl_jump
22  | _ ⇒ cl_other
23  ].
24
25definition ASM_classify0: instruction → status_class ≝
26  λi.
27  match i with
28   [ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
29   | ACALL _ ⇒ cl_call
30   | LCALL _ ⇒ cl_call
31   | JMP _ ⇒ cl_call
32   | AJMP _ ⇒ cl_other
33   | LJMP _ ⇒ cl_other
34   | SJMP _ ⇒ cl_other
35   | _ ⇒ cl_other
36   ].
37
38definition current_instruction0 ≝
39  λcode_memory: BitVectorTrie Byte 16.
40  λprogram_counter: Word.
41    \fst (\fst (fetch … code_memory program_counter)).
42
43definition current_instruction ≝
44  λcode_memory.
45  λs: Status code_memory.
46    current_instruction0 code_memory (program_counter … s).
47   
48definition current_instruction_label ≝
49  λcode_memory.
50  λcost_labels: costlabel_map.
51  λs: Status code_memory.
52  let pc ≝ program_counter … code_memory s in
53    lookup_opt … pc cost_labels.
54
55definition next_instruction_properly_relates_program_counters ≝
56  λcode_memory.
57  λbefore: Status code_memory.
58  λafter : Status code_memory.
59    let program_counter_before ≝ program_counter ? code_memory before in
60    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
61      program_counter ? code_memory after = program_counter_after.
62
63definition word_deqset: DeqSet ≝
64  mk_DeqSet Word (eq_bv 16) ?.
65  @refl_iff_eq_bv_true
66qed.
67   
68definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
69  λcode_memory.
70  λs: Status code_memory.
71    ASM_classify0 (current_instruction … s).
Note: See TracBrowser for help on using the repository browser.