source: src/ASM/AbstractStatus.ma

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

Removed redundant defn of current_instruction0,
which only appears in redundnant normalization steps in ASMCosts.ma

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