source: LTS/Vm.ma @ 3399

Last change on this file since 3399 was 3379, checked in by sacerdot, 6 years ago

Semantics completed.

File size: 3.2 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| Ijmp: nat → instr
10| Ibne: nat → instr
11| Ibge: nat → instr
12| Ihalt: instr
13| Iio: instr
14| Icall: fname → 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
25definition pc: ∀S. vmstate S → nat ≝ λS,s. \snd (\fst s).
26
27inductive vmstep (p: programT) (S: storeT) : vmstate S → vmstate S → Prop :=
28| vmstep_const: ∀c,pc,stk,s,n. fetch c pc = Some … (Iconst n) →
29   vmstep …
30    〈c, pc,     stk,      s〉
31    〈c, 1 + pc, n :: stk, s〉
32| vmstep_var: ∀c,pc,stk,s,x. fetch c pc = Some … (Ivar x) →
33   vmstep …
34    〈c, pc,     stk,              s〉
35    〈c, 1 + pc, get … s x :: stk, s〉
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| vmstep_add: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Iadd →
41   vmstep …
42    〈c, pc,     n2 :: n1 :: stk,  s〉
43    〈c, 1 + pc, (n1 + n2) :: stk, s〉
44| vmstep_sub: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Isub →
45   vmstep …
46    〈c, pc,     n2 :: n1 :: stk,  s〉
47    〈c, 1 + pc, (n1 - n2) :: stk, s〉
48| vmstep_bne: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibne ofs) →
49   let pc' ≝ if eqb n1 n2 then 1 + pc else 1 + pc + ofs in
50   vmstep …
51    〈c, pc,  n2 :: n1 :: stk, s〉
52    〈c, pc', stk,             s〉
53| vmstep_bge: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibge ofs) →
54   let pc' ≝ if ltb n1 n2 then 1 + pc else 1 + pc + ofs in
55   vmstep …
56    〈c, pc,  n2 :: n1 :: stk, s〉
57    〈c, pc', stk,             s〉
58| vmstep_branch: ∀c,pc,stk,s,ofs. fetch c pc = Some … (Ijmp ofs) →
59   let pc' ≝ 1 + pc + ofs in
60   vmstep …
61    〈c,           pc, stk, s〉
62    〈c, 1 + pc + ofs, stk, s〉
63| vmstep_io: ∀c,pc,stk,s. fetch c pc = Some … Iio →
64   vmstep …
65    〈c,     pc, stk, s〉
66    〈c, 1 + pc, stk, s〉.
67
68definition emitterT ≝ nat → nat → option label.
69
70definition vmlstep: ∀p: programT. ∀S: storeT. ∀emit: emitterT.
71 vmstate S → vmstate S → list label → Prop ≝
72λp,S,emitter,s1,s2,ll. ∀l.
73 vmstep p S s1 s2 ∧ ll = [l] ∧ emitter (pc … s1) (pc … s2) = Some … l.
74
75(*
76Definition star_vm (lbl: Type) (c: code (instr_vm lbl)) := star (trans_vm lbl c).
77
78Definition term_vm_lbl (lbl: Type) (c: code (instr_vm lbl)) (s_init s_fin: store) (trace: list lbl) :=
79        exists pc,
80        code_at c pc = Some (Ihalt lbl) /\
81        star_vm lbl c (0, nil, s_init) (pc, nil, s_fin) trace.
82
83Definition term_vm (c: code_vm) (s_init s_fin: store):=
84        exists pc,
85        code_at c pc = Some (Ihalt False) /\
86        star_vm False c (0, nil, s_init) (pc, nil, s_fin) nil.
87
88Definition term_vml (c: code_vml) (s_init s_fin: store) (trace: list label) :=
89        exists pc,
90        code_at c pc = Some (Ihalt label) /\
91        star_vm label c (0, nil, s_init) (pc, nil, s_fin) trace.
92*)
Note: See TracBrowser for help on using the repository browser.