source: src/ASM/Interpret2.ma @ 1975

Last change on this file since 1975 was 1606, checked in by sacerdot, 8 years ago

Porting to last library of Matita.

File size: 2.3 KB
Line 
1include "ASM/Interpret.ma".
2include "common/SmallstepExec.ma".
3include "common/IO.ma".
4
5(* Transition system on the assembly code *)
6
7(*CSC: waiting for Jaap's code to compile or to be splitted from Assembly.ma *)
8axiom policy: pseudo_assembly_program → Type[0].
9(*CSC: problem here: mk_policy should be allowed to fail, but mk_fullexec does
10  not allow make_global to fail too *)
11axiom mk_policy: ∀p:pseudo_assembly_program. policy p.
12
13(*CSC: already implemented in AssemblyProof.ma: move elsewhere *)
14axiom ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat.
15
16definition pseudo_make_global: pseudo_assembly_program → Word → nat × nat ≝
17 λp. ticks_of … (mk_policy p).
18
19definition execute_1_pseudo_instruction_trace:
20 (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus) ≝
21λticks_of,s.
22 let 〈instr,pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory … s)) (program_counter … s) in
23 let s ≝ execute_1_pseudo_instruction ticks_of s in
24 match instr with
25 [ Cost cst ⇒ ret … 〈Echarge cst, s〉
26 | _ ⇒ ret ? 〈E0, s〉 ].
27
28axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int.
29
30definition pseudo_exec: trans_system io_out io_in ≝
31 mk_trans_system … pseudo_is_final execute_1_pseudo_instruction_trace.
32
33definition pseudo_ASM_fullexec: fullexec io_out io_in ≝
34 mk_fullexec … pseudo_exec pseudo_make_global (λp.OK … (initialise_status … p)).
35
36(* Transition system on the object code *)
37
38(*CSC: move this definition elsewhere *)
39definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
40
41definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
42
43definition execute_1_instruction:
44 BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
45λcosts,s.
46 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
47 let 〈instr,pc〉 ≝ instr_pc in
48 match lookup_opt … pc costs with
49 [ None ⇒ ret … 〈E0, s〉
50 | Some cst ⇒ ret … 〈Echarge cst, execute_1 s〉 ].
51
52axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
53
54definition exec: trans_system io_out io_in ≝
55 mk_trans_system … is_final execute_1_instruction.
56
57definition ASM_fullexec: fullexec io_out io_in ≝
58 mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))).
Note: See TracBrowser for help on using the repository browser.