source: LTS/Vm.ma @ 3378

Last change on this file since 3378 was 3378, checked in by sacerdot, 6 years ago
  • Stuff common to both languages is now in Common.ma
  • object (intermediate) code Vm (in progress)
File size: 3.1 KB
Line 
1include "Common.ma".
2
3inductive instr: Type[0] :=
4| Iconst: nat → instr
5| Ivar: option ident → instr
6| Isetvar: option ident → instr
7| Iadd: instr
8| Isub: instr
9| Ibranch: nat → instr
10| Ibne: label → nat → label → instr
11| Ibge: label → nat → label → instr
12| Ihalt: instr
13| Ilabel: label → instr
14| Icall: fname → label → instr
15| Iret: fname → instr.
16
17definition programT ≝ fname → list instr.
18
19definition fetch: list instr → nat → option instr ≝ λl,n. nth_opt ? n l.
20
21definition stackT: Type[0] ≝ list nat.
22
23definition vmstate ≝ λS:storeT. (list instr) × nat × (stackT × S).
24
25inductive vmstep (p: programT) (S: storeT): vmstate S → vmstate S → option label → Prop :=
26| vmstep_const: ∀c,pc,stk,s,n. fetch c pc = Some … (Iconst n) →
27   vmstep …
28    〈c, pc,     stk,      s〉
29    〈c, 1 + pc, n :: stk, s〉
30    (None …)
31| vmstep_var: ∀c,pc,stk,s,x. fetch c pc = Some … (Ivar x) →
32   vmstep …
33    〈c, pc,     stk,              s〉
34    〈c, 1 + pc, get … s x :: stk, s〉
35    (None …)
36| vmstep_setvar: ∀c,pc,stk,s,x,n. fetch c pc = Some … (Isetvar x) →
37   vmstep …
38    〈c, pc,     n :: stk, s〉
39    〈c, 1 + pc, stk,      set … s x n〉
40    (None …)
41| vmstep_add: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Iadd →
42   vmstep …
43    〈c, pc,     n2 :: n1 :: stk,  s〉
44    〈c, 1 + pc, (n1 + n2) :: stk, s〉
45    (None …)
46| vmstep_sub: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Isub →
47   vmstep …
48    〈c, pc,     n2 :: n1 :: stk,  s〉
49    〈c, 1 + pc, (n1 - n2) :: stk, s〉
50    (None …)
51| vmstep_bne: ∀c,pc,stk,s,l1,ofs,l2,n1,n2. fetch c pc = Some … (Ibne l1 ofs l2) →
52   let pc' ≝ if eqb n1 n2 then 1 + pc else 1 + pc + ofs in
53   let l ≝ if eqb n1 n2 then l2 else l1 in
54   vmstep …
55    〈c, pc,  n2 :: n1 :: stk, s〉
56    〈c, pc', stk,             s〉
57    (Some … l)
58| vmstep_bge: ∀c,pc,stk,s,l1,ofs,l2,n1,n2. fetch c pc = Some … (Ibge l1 ofs l2) →
59   let pc' ≝ if ltb n1 n2 then 1 + pc else 1 + pc + ofs in
60   let l ≝ if ltb n1 n2 then l2 else l1 in
61   vmstep …
62    〈c, pc,  n2 :: n1 :: stk, s〉
63    〈c, pc', stk,             s〉
64    (Some … l).
65| vmstep_branch: ∀c,pc,stk,s,l,ofs. fetch c pc = Some … (Ibranch l ofs) →
66   let pc' ≝ 1 + pc + ofs in
67   trans_vm lbl c (pc, stk, s) (pc', stk, s) None
68| vmstep_label: forall pc stk s l, code_at c pc = Some (Ilabel lbl l)
69                -> trans_vm lbl c (pc,stk,s) (pc+1,stk,s) (Some l).
70
71(*
72Definition star_vm (lbl: Type) (c: code (instr_vm lbl)) := star (trans_vm lbl c).
73
74Definition term_vm_lbl (lbl: Type) (c: code (instr_vm lbl)) (s_init s_fin: store) (trace: list lbl) :=
75        exists pc,
76        code_at c pc = Some (Ihalt lbl) /\
77        star_vm lbl c (0, nil, s_init) (pc, nil, s_fin) trace.
78
79Definition term_vm (c: code_vm) (s_init s_fin: store):=
80        exists pc,
81        code_at c pc = Some (Ihalt False) /\
82        star_vm False c (0, nil, s_init) (pc, nil, s_fin) nil.
83
84Definition term_vml (c: code_vml) (s_init s_fin: store) (trace: list label) :=
85        exists pc,
86        code_at c pc = Some (Ihalt label) /\
87        star_vm label c (0, nil, s_init) (pc, nil, s_fin) trace.
88*)
Note: See TracBrowser for help on using the repository browser.