source: LTS/StaticAnalysis.ma @ 3418

Last change on this file since 3418 was 3381, checked in by sacerdot, 6 years ago

Pen&paper style hypotheses and statements for the static-dynamic simulation.

File size: 5.1 KB
Line 
1include "Common.ma".
2
3inductive classification: Type[0] ≝
4   sequential: classification
5 | conditional: nat → classification
6 | call: ident → classification
7 | ret: classification.
8
9record object_code_def: Type[1] ≝
10 { status: Type[0]
11 ; trans: status → status
12 ; max: nat
13 ; pc: status → nat
14 ; succ: nat → nat
15 ; labelled: nat → nat → bool
16 ; classify: nat → classification
17 ; classification_ok1:
18    ∀s. classify (pc s) = sequential → pc (trans s) = succ (pc s)
19 ; code_closed:
20    ∀pc. pc < max → classify pc = sequential → succ pc < max
21   (* serve per jmp e call??? *)
22 }.
23
24record abelian_monoid: Type[1] ≝
25 { carrier :> Type[0]
26 ; op: carrier → carrier → carrier
27 ; e: carrier
28 ; neutral: ∀x. op … x e = x
29 ; associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)
30 ; commutative: ∀x,y. op … x y = op … y x
31 }.
32
33instr_cost: nat → M
34
35k: n:nat → pc:nat → M ≝
36 match n with
37 [ O ⇒ whatever
38 | S n' ⇒
39    match classify pc with
40    [ seq ⇒
41       if labelelled pc (succ pc) then
42        instr_cost pc
43       else
44        instr_cost pc + k n' (succ pc)
45    | call ⇒
46       if postlabelled pc then
47        instr_cost pc
48       else
49        instr_cost pc + k n' (succ pc)
50    | _ ⇒ instr_cost pc
51    ]]
52
53theorem strong:
54 ∀τ: so -pm→ sn. τ finisce con label o return →
55  Σ_(pc → pc' ∈ τ) instr_cost pc =
56  k max (pc s0) + Σ_(pc -L→ pc' ∈ τ senza l'ultima) K max pc'.
57
58definition x ≤ y ≝ ∃z. op x z = y.
59
60theorem weak:
61 ∀τ: so -pm→ sn. τ estendibile fino a trovare una label o una ret.
62  Σ_(pc → pc' ∈ τ) instr_cost pc ≤
63  k max (pc s0) + Σ_(pc -L→ pc' ∈ τ senza l'ultima se finisce con label o return labelled) K max pc'.
64
65theorem superweak:
66 come strong o weak, ma
67   1. tutte le call sono postlabelled
68   2. il monoide non e' abeliano
69
70===================================================
71
72record cost_monoid ≝ λ nat →
73
74let rec cost_from (pc: nat):
75
76inductive instr: Type[0] :=
77| Iconst: nat → instr
78| Ivar: option ident → instr
79| Isetvar: option ident → instr
80| Iadd: instr
81| Isub: instr
82| Ijmp: nat → instr
83| Ibne: nat → instr
84| Ibge: nat → instr
85| Ihalt: instr
86| Iio: instr
87| Icall: fname → instr
88| Iret: fname → instr.
89
90definition programT ≝ fname → list instr.
91
92definition fetch: list instr → nat → option instr ≝ λl,n. nth_opt ? n l.
93
94definition stackT: Type[0] ≝ list nat.
95
96definition vmstate ≝ λS:storeT. (list instr) × nat × (stackT × S).
97
98definition pc: ∀S. vmstate S → nat ≝ λS,s. \snd (\fst s).
99
100inductive vmstep (p: programT) (S: storeT) : vmstate S → vmstate S → Prop :=
101| vmstep_const: ∀c,pc,stk,s,n. fetch c pc = Some … (Iconst n) →
102   vmstep …
103    〈c, pc,     stk,      s〉
104    〈c, 1 + pc, n :: stk, s〉
105| vmstep_var: ∀c,pc,stk,s,x. fetch c pc = Some … (Ivar x) →
106   vmstep …
107    〈c, pc,     stk,              s〉
108    〈c, 1 + pc, get … s x :: stk, s〉
109| vmstep_setvar: ∀c,pc,stk,s,x,n. fetch c pc = Some … (Isetvar x) →
110   vmstep …
111    〈c, pc,     n :: stk, s〉
112    〈c, 1 + pc, stk,      set … s x n〉
113| vmstep_add: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Iadd →
114   vmstep …
115    〈c, pc,     n2 :: n1 :: stk,  s〉
116    〈c, 1 + pc, (n1 + n2) :: stk, s〉
117| vmstep_sub: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Isub →
118   vmstep …
119    〈c, pc,     n2 :: n1 :: stk,  s〉
120    〈c, 1 + pc, (n1 - n2) :: stk, s〉
121| vmstep_bne: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibne ofs) →
122   let pc' ≝ if eqb n1 n2 then 1 + pc else 1 + pc + ofs in
123   vmstep …
124    〈c, pc,  n2 :: n1 :: stk, s〉
125    〈c, pc', stk,             s〉
126| vmstep_bge: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibge ofs) →
127   let pc' ≝ if ltb n1 n2 then 1 + pc else 1 + pc + ofs in
128   vmstep …
129    〈c, pc,  n2 :: n1 :: stk, s〉
130    〈c, pc', stk,             s〉
131| vmstep_branch: ∀c,pc,stk,s,ofs. fetch c pc = Some … (Ijmp ofs) →
132   let pc' ≝ 1 + pc + ofs in
133   vmstep …
134    〈c,           pc, stk, s〉
135    〈c, 1 + pc + ofs, stk, s〉
136| vmstep_io: ∀c,pc,stk,s. fetch c pc = Some … Iio →
137   vmstep …
138    〈c,     pc, stk, s〉
139    〈c, 1 + pc, stk, s〉.
140
141definition emitterT ≝ nat → nat → option label.
142
143definition vmlstep: ∀p: programT. ∀S: storeT. ∀emit: emitterT.
144 vmstate S → vmstate S → list label → Prop ≝
145λp,S,emitter,s1,s2,ll. ∀l.
146 vmstep p S s1 s2 ∧ ll = [l] ∧ emitter (pc … s1) (pc … s2) = Some … l.
147
148(*
149Definition star_vm (lbl: Type) (c: code (instr_vm lbl)) := star (trans_vm lbl c).
150
151Definition term_vm_lbl (lbl: Type) (c: code (instr_vm lbl)) (s_init s_fin: store) (trace: list lbl) :=
152        exists pc,
153        code_at c pc = Some (Ihalt lbl) /\
154        star_vm lbl c (0, nil, s_init) (pc, nil, s_fin) trace.
155
156Definition term_vm (c: code_vm) (s_init s_fin: store):=
157        exists pc,
158        code_at c pc = Some (Ihalt False) /\
159        star_vm False c (0, nil, s_init) (pc, nil, s_fin) nil.
160
161Definition term_vml (c: code_vml) (s_init s_fin: store) (trace: list label) :=
162        exists pc,
163        code_at c pc = Some (Ihalt label) /\
164        star_vm label c (0, nil, s_init) (pc, nil, s_fin) trace.
165*)
Note: See TracBrowser for help on using the repository browser.