Changeset 3379
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3378 r3379 7 7  Iadd: instr 8 8  Isub: instr 9  I branch: nat → instr10  Ibne: label → nat → label→ instr11  Ibge: label → nat → label→ instr9  Ijmp: nat → instr 10  Ibne: nat → instr 11  Ibge: nat → instr 12 12  Ihalt: instr 13  I label: label →instr14  Icall: fname → label →instr13  Iio: instr 14  Icall: fname → instr 15 15  Iret: fname → instr. 16 16 … … 23 23 definition vmstate ≝ λS:storeT. (list instr) × nat × (stackT × S). 24 24 25 inductive vmstep (p: programT) (S: storeT): vmstate S → vmstate S → option label → Prop := 25 definition pc: ∀S. vmstate S → nat ≝ λS,s. \snd (\fst s). 26 27 inductive vmstep (p: programT) (S: storeT) : vmstate S → vmstate S → Prop := 26 28  vmstep_const: ∀c,pc,stk,s,n. fetch c pc = Some … (Iconst n) → 27 29 vmstep … 28 30 〈c, pc, stk, s〉 29 31 〈c, 1 + pc, n :: stk, s〉 30 (None …)31 32  vmstep_var: ∀c,pc,stk,s,x. fetch c pc = Some … (Ivar x) → 32 33 vmstep … 33 34 〈c, pc, stk, s〉 34 35 〈c, 1 + pc, get … s x :: stk, s〉 35 (None …)36 36  vmstep_setvar: ∀c,pc,stk,s,x,n. fetch c pc = Some … (Isetvar x) → 37 37 vmstep … 38 38 〈c, pc, n :: stk, s〉 39 39 〈c, 1 + pc, stk, set … s x n〉 40 (None …)41 40  vmstep_add: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Iadd → 42 41 vmstep … 43 42 〈c, pc, n2 :: n1 :: stk, s〉 44 43 〈c, 1 + pc, (n1 + n2) :: stk, s〉 45 (None …)46 44  vmstep_sub: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Isub → 47 45 vmstep … 48 46 〈c, pc, n2 :: n1 :: stk, s〉 49 47 〈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) → 48  vmstep_bne: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibne ofs) → 52 49 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 in54 50 vmstep … 55 51 〈c, pc, n2 :: n1 :: stk, s〉 56 52 〈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) → 53  vmstep_bge: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibge ofs) → 59 54 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 in61 55 vmstep … 62 56 〈c, pc, n2 :: n1 :: stk, s〉 63 57 〈c, pc', stk, s〉 64 (Some … l). 65  vmstep_branch: ∀c,pc,stk,s,l,ofs. fetch c pc = Some … (Ibranch l ofs) → 58  vmstep_branch: ∀c,pc,stk,s,ofs. fetch c pc = Some … (Ijmp ofs) → 66 59 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). 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 68 definition emitterT ≝ nat → nat → option label. 69 70 definition 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. 70 74 71 75 (*
Note: See TracChangeset
for help on using the changeset viewer.