source: src/ASM/AbstractStatus.ma @ 1939

Last change on this file since 1939 was 1939, checked in by mulligan, 8 years ago

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 size: 2.5 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Status.ma".
3include "ASM/Fetch.ma".
4
5include "basics/lists/listb.ma".
6
7inductive status_class: Type[0] ≝
8  | cl_return: status_class
9  | cl_jump: status_class
10  | cl_call: status_class
11  | cl_other: status_class.
12
13definition ASM_classify00: ∀a. preinstruction a → status_class ≝
14  λa, pre.
15  match pre with
16  [ RET ⇒ cl_return
17  | RETI ⇒ cl_return
18  | JZ _ ⇒ cl_jump
19  | JNZ _ ⇒ cl_jump
20  | JC _ ⇒ cl_jump
21  | JNC _ ⇒ cl_jump
22  | JB _ _ ⇒ cl_jump
23  | JNB _ _ ⇒ cl_jump
24  | JBC _ _ ⇒ cl_jump
25  | CJNE _ _ ⇒ cl_jump
26  | DJNZ _ _ ⇒ cl_jump
27  | _ ⇒ cl_other
28  ].
29
30definition ASM_classify0: instruction → status_class ≝
31  λi.
32  match i with
33   [ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
34   | ACALL _ ⇒ cl_call
35   | LCALL _ ⇒ cl_call
36   | JMP _ ⇒ cl_call
37   | AJMP _ ⇒ cl_other
38   | LJMP _ ⇒ cl_other
39   | SJMP _ ⇒ cl_other
40   | _ ⇒ cl_other
41   ].
42
43definition current_instruction0 ≝
44  λcode_memory: BitVectorTrie Byte 16.
45  λprogram_counter: Word.
46    \fst (\fst (fetch … code_memory program_counter)).
47
48definition current_instruction ≝
49  λcode_memory.
50  λs: Status code_memory.
51    current_instruction0 code_memory (program_counter … s).
52   
53definition current_instruction_label ≝
54  λcode_memory.
55  λcost_labels: BitVectorTrie costlabel 16.
56  λs: Status code_memory.
57  let pc ≝ program_counter … code_memory s in
58    lookup_opt … pc cost_labels.
59
60definition next_instruction_properly_relates_program_counters ≝
61  λcode_memory.
62  λbefore: Status code_memory.
63  λafter : Status code_memory.
64    let program_counter_before ≝ program_counter ? code_memory before in
65    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
66      program_counter ? code_memory after = program_counter_after.
67
68definition word_deqset: DeqSet ≝
69  mk_DeqSet Word (eq_bv 16) ?.
70  @refl_iff_eq_bv_true
71qed.
72   
73definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
74  λcode_memory.
75  λs: Status code_memory.
76    ASM_classify0 (current_instruction … s).
77
78record abstract_status : Type[1] ≝
79{
80    as_status :> Type[0]
81  ; as_execute : as_status → as_status → Prop
82  ; as_pc : DeqSet
83  ; as_pc_of : as_status → as_pc
84  ; as_classifier : as_status → status_class → Prop
85  ; as_label : as_status → option costlabel
86  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
87  ; as_final: as_status → Prop
88}.
Note: See TracBrowser for help on using the repository browser.