source: src/ASM/AbstractStatus.ma @ 2771

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

WARNING: another big commit, touching many files in ASM/*.ma

This edit
a) prunes many redundant "include"s from ASM/*.ma hierarchy
b) adjusts the use of aliases from ASM/ and elsewhere (big, annoying, hard-to-debug disambiguation errors), from the earlier adjustment to ASM/ASM.ma
c) adds ONE (and once repeated) type annotation to ASM/Interpret.ma

As with the continual failures with Clight/switchRemoval.ma, the (revised) definition of execute_1_preinstruction causes no end of disambiguation thrashing. One type annotation (in the JMP case, to ensure that program_counter calculations actually produce values in Word) is enough to cut that particular Gordian knot. By russell-style reasoning, the annotation then gets repeated later, though in fact in that later instance is redundant...

File size: 2.0 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
36definition current_instruction0 ≝
37  λcode_memory: BitVectorTrie Byte 16.
38  λprogram_counter: Word.
39    \fst (\fst (fetch … code_memory program_counter)).
40
41definition current_instruction ≝
42  λcode_memory.
43  λs: Status code_memory.
44    current_instruction0 code_memory (program_counter … s).
45   
46definition current_instruction_label ≝
47  λcode_memory.
48  λcost_labels: BitVectorTrie costlabel 16.
49  λs: Status code_memory.
50  let pc ≝ program_counter … code_memory s in
51    lookup_opt … pc cost_labels.
52
53definition next_instruction_properly_relates_program_counters ≝
54  λcode_memory.
55  λbefore: Status code_memory.
56  λafter : Status code_memory.
57    let program_counter_before ≝ program_counter ? code_memory before in
58    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
59      program_counter ? code_memory after = program_counter_after.
60
61definition word_deqset: DeqSet ≝
62  mk_DeqSet Word (eq_bv 16) ?.
63  @refl_iff_eq_bv_true
64qed.
65   
66definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
67  λcode_memory.
68  λs: Status code_memory.
69    ASM_classify0 (current_instruction … s).
Note: See TracBrowser for help on using the repository browser.