source: src/ASM/Interpret2.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 2.4 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 let s ≝ execute_1 s in
49 match lookup_opt … pc costs with
50 [ None ⇒ ret … 〈E0, s〉
51 | Some cst ⇒ ret … 〈Echarge cst, s〉 ].
52
53axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
54
55definition exec: trans_system io_out io_in ≝
56 mk_trans_system … is_final execute_1_instruction.
57
58definition ASM_fullexec: fullexec io_out io_in ≝
59 mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))).
Note: See TracBrowser for help on using the repository browser.