Changeset 3379


Ignore:
Timestamp:
Jul 2, 2013, 11:58:06 AM (4 years ago)
Author:
sacerdot
Message:

Semantics completed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3378 r3379  
    77| Iadd: instr
    88| Isub: instr
    9 | Ibranch: nat → instr
    10 | Ibne: label → nat → label → instr
    11 | Ibge: label → nat → label → instr
     9| Ijmp: nat → instr
     10| Ibne: nat → instr
     11| Ibge: nat → instr
    1212| Ihalt: instr
    13 | Ilabel: label → instr
    14 | Icall: fname → label → instr
     13| Iio: instr
     14| Icall: fname → instr
    1515| Iret: fname → instr.
    1616
     
    2323definition vmstate ≝ λS:storeT. (list instr) × nat × (stackT × S).
    2424
    25 inductive vmstep (p: programT) (S: storeT): vmstate S → vmstate S → option label → Prop :=
     25definition pc: ∀S. vmstate S → nat ≝ λS,s. \snd (\fst s).
     26
     27inductive vmstep (p: programT) (S: storeT) : vmstate S → vmstate S → Prop :=
    2628| vmstep_const: ∀c,pc,stk,s,n. fetch c pc = Some … (Iconst n) →
    2729   vmstep …
    2830    〈c, pc,     stk,      s〉
    2931    〈c, 1 + pc, n :: stk, s〉
    30     (None …)
    3132| vmstep_var: ∀c,pc,stk,s,x. fetch c pc = Some … (Ivar x) →
    3233   vmstep …
    3334    〈c, pc,     stk,              s〉
    3435    〈c, 1 + pc, get … s x :: stk, s〉
    35     (None …)
    3636| vmstep_setvar: ∀c,pc,stk,s,x,n. fetch c pc = Some … (Isetvar x) →
    3737   vmstep …
    3838    〈c, pc,     n :: stk, s〉
    3939    〈c, 1 + pc, stk,      set … s x n〉
    40     (None …)
    4140| vmstep_add: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Iadd →
    4241   vmstep …
    4342    〈c, pc,     n2 :: n1 :: stk,  s〉
    4443    〈c, 1 + pc, (n1 + n2) :: stk, s〉
    45     (None …)
    4644| vmstep_sub: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Isub →
    4745   vmstep …
    4846    〈c, pc,     n2 :: n1 :: stk,  s〉
    4947    〈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) →
    5249   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
    5450   vmstep …
    5551    〈c, pc,  n2 :: n1 :: stk, s〉
    5652    〈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) →
    5954   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
    6155   vmstep …
    6256    〈c, pc,  n2 :: n1 :: stk, s〉
    6357    〈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) →
    6659   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
     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.
    7074
    7175(*
Note: See TracChangeset for help on using the changeset viewer.