specs.mlw 7.91 KB
Newer Older
Martin Clochard's avatar
Martin Clochard committed
1
2
3

module VM_instr_spec

Martin Clochard's avatar
Martin Clochard committed
4
5
  meta compute_max_steps 0x10000

6
7
8
9
10
11
12
  use import int.Int
  use import list.List
  use import list.Length
  use import vm.Vm
  use import state.State
  use import logic.Compiler_logic

Martin Clochard's avatar
Martin Clochard committed
13
  function ifun_post (f:machine_state -> machine_state) : post 'a =
14
    fun _ _ ms ms' -> ms' = f ms
Martin Clochard's avatar
Martin Clochard committed
15
  meta rewrite_def function ifun_post
Martin Clochard's avatar
Martin Clochard committed
16

Martin Clochard's avatar
Martin Clochard committed
17
18
  (* General specification builder for determinstic machine
     instructions. *)
19
  let ifunf (ghost pre:pre {'a}) (code_f:code)
Martin Clochard's avatar
Martin Clochard committed
20
21
22
    (ghost f:machine_state -> machine_state) : hl 'a
    requires { forall c p. codeseq_at c p code_f ->
        forall x ms. pre x p ms -> transition c ms (f ms) }
23
24
25
    ensures { result.pre --> pre }
    ensures { result.post --> ifun_post f }
    ensures { result.code --> code_f }
26
  = { pre = pre; code = code_f; post = ifun_post f }
Martin Clochard's avatar
Martin Clochard committed
27
28
29

  (* Iconst spec *)
  function iconst_post (n:int) : post 'a =
30
    fun _ p ms ms' -> forall s m. ms  = VMS p s m -> ms' = VMS (p+1) (push n s) m
31
32
  meta rewrite_def function iconst_post

Martin Clochard's avatar
Martin Clochard committed
33
  function iconst_fun (n:int) : machine_state -> machine_state =
34
    fun ms -> let (VMS p s m) = ms in VMS (p+1) (push n s) m
Martin Clochard's avatar
Martin Clochard committed
35
36
  meta rewrite_def function iconst_fun

37
  let iconstf (n: int) : hl 'a
38
39
40
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> iconst_post n }
    ensures { result.code.length --> 1 }
41
  = hoare trivial_pre ($ ifunf trivial_pre n.iconst n.iconst_fun) n.iconst_post
Martin Clochard's avatar
Martin Clochard committed
42
43
44

  (* Ivar spec *)
  function ivar_post (x:id) : post 'a =
45
    fun _ p ms ms' -> forall s m. ms = VMS p s m -> ms' = VMS (p+1) (push m[x] s) m
Martin Clochard's avatar
Martin Clochard committed
46
  meta rewrite_def function ivar_post
Martin Clochard's avatar
Martin Clochard committed
47

Martin Clochard's avatar
Martin Clochard committed
48
  function ivar_fun (x:id) : machine_state -> machine_state =
49
    fun ms -> let (VMS p s m) = ms in VMS (p+1) (push m[x] s) m
Martin Clochard's avatar
Martin Clochard committed
50
51
52
  meta rewrite_def function ivar_fun

  let ivarf (x: id) : hl 'a
53
54
55
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ivar_post x }
    ensures { result.code.length --> 1 }
56
  = hoare trivial_pre ($ ifunf trivial_pre x.ivar x.ivar_fun) x.ivar_post
Martin Clochard's avatar
Martin Clochard committed
57

Martin Clochard's avatar
Martin Clochard committed
58
59
  (* Binary arithmetic operators specification (Iadd, Isub, Imul)
     via a generic builder. *)
60
61
  type binop = int -> int -> int

Martin Clochard's avatar
Martin Clochard committed
62
  constant ibinop_pre : pre 'a =
63
    fun _ p ms -> exists n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m
64
65
  meta rewrite_def function ibinop_pre

Martin Clochard's avatar
Martin Clochard committed
66
  function ibinop_post (op : binop) : post 'a =
67
   fun _ p ms ms' -> forall n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m ->
Martin Clochard's avatar
Martin Clochard committed
68
     ms' = VMS (p+1) (push (op n1 n2) s) m
69
70
  meta rewrite_def function ibinop_post

Martin Clochard's avatar
Martin Clochard committed
71
  function ibinop_fun (op:binop) : machine_state -> machine_state =
72
    fun ms -> match ms with
Martin Clochard's avatar
Martin Clochard committed
73
74
75
76
77
78
79
80
81
      | VMS p (Cons n2 (Cons n1 s)) m -> VMS (p+1) (push (op n1 n2) s) m
      | _ -> ms
      end
  meta rewrite_def function ibinop_fun

  let create_binop (code_b:code) (ghost op:binop) : hl 'a
    requires { forall c p. codeseq_at c p code_b ->
      forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
 	                                 (VMS (p+1) (push (op n1 n2) s) m) }
82
83
84
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post op }
    ensures { result.code.length --> code_b.length }
85
  = hoare ibinop_pre ($ ifunf ibinop_pre code_b op.ibinop_fun) op.ibinop_post
86

87
  constant plus : binop = fun x y -> x + y
88
89
  meta rewrite_def function plus

90
  constant sub : binop = fun x y -> x - y
91
92
  meta rewrite_def function sub

93
  constant mul : binop = fun x y -> x * y
94
95
96
  meta rewrite_def function mul

  let iaddf () : hl 'a
97
98
99
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post plus }
    ensures { result.code.length --> 1 }
100
  = create_binop iadd plus
101
102

  let isubf () : hl 'a
103
104
105
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post sub }
    ensures { result.code.length --> 1 }
106
  = create_binop isub sub
107
108

  let imulf () : hl 'a
109
110
111
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> ibinop_post mul }
    ensures { result.code.length --> 1 }
112
  = create_binop imul mul
113

Martin Clochard's avatar
Martin Clochard committed
114
  (* Inil spec *)
Martin Clochard's avatar
Martin Clochard committed
115
  function inil_post : post 'a =
116
    fun _ _ ms ms' -> ms = ms'
117
118
119
  meta rewrite_def function inil_post

  let inil () : hl 'a
120
121
122
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> inil_post }
    ensures { result.code.length --> 0 }
123
  = { pre = trivial_pre; code = Nil; post = inil_post }
124

Martin Clochard's avatar
Martin Clochard committed
125
  (* Ibranch specification *)
Martin Clochard's avatar
Martin Clochard committed
126
  function ibranch_post (ofs: ofs) : post 'a =
127
    fun _ p ms ms' -> forall s m. ms = VMS p s m -> ms' = VMS (p + 1 + ofs) s m
128
129
  meta rewrite_def function ibranch_post

Martin Clochard's avatar
Martin Clochard committed
130
  function ibranch_fun (ofs:ofs) : machine_state -> machine_state =
131
    fun ms -> let (VMS p s m) = ms in VMS (p+1+ofs) s m
Martin Clochard's avatar
Martin Clochard committed
132
133
  meta rewrite_def function ibranch_fun

Martin Clochard's avatar
Martin Clochard committed
134
  let ibranchf (ofs:ofs) : hl 'a
135
136
137
    ensures { result.pre --> trivial_pre }
    ensures { result.post --> ibranch_post ofs }
    ensures { result.code.length --> 1 }
138
139
  = let cf = $ ifunf trivial_pre (ibranch ofs) (ibranch_fun ofs) in
    hoare trivial_pre cf (ibranch_post ofs)
140

Martin Clochard's avatar
Martin Clochard committed
141
  (* Conditional jump specification via a generic builder. *)
142
143
  type cond = int -> int -> bool

Martin Clochard's avatar
Martin Clochard committed
144
  function icjump_post (cond:cond) (ofs:ofs) : post 'a =
145
    fun _ p ms ms' -> forall n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m ->
Martin Clochard's avatar
Martin Clochard committed
146
      (cond n1 n2 -> ms' = VMS (p + ofs + 1) s m) /\
147
      (not cond n1 n2 -> ms' = VMS (p+1) s m)
Martin Clochard's avatar
Martin Clochard committed
148
  meta rewrite_def function icjump_post
149

Martin Clochard's avatar
Martin Clochard committed
150
  function icjump_fun (cond:cond) (ofs:ofs) : machine_state -> machine_state =
151
    fun ms -> match ms with
Martin Clochard's avatar
Martin Clochard committed
152
153
154
155
      | VMS p (Cons n2 (Cons n1 s)) m ->
        if cond n1 n2 then VMS (p+ofs+1) s m else VMS (p+1) s m
      | _ -> ms
      end
Martin Clochard's avatar
Martin Clochard committed
156
  meta rewrite_def function icjump_fun
Martin Clochard's avatar
Martin Clochard committed
157

Martin Clochard's avatar
Martin Clochard committed
158
  let create_cjump (code_cd:code) (ghost cond:cond) (ghost ofs:ofs) : hl 'a
Martin Clochard's avatar
Martin Clochard committed
159
160
161
    requires { forall c p1 n1 n2 s m. codeseq_at c p1 code_cd ->
      let p2 = (if cond n1 n2 then p1 + ofs + 1 else p1 + 1) in
      transition c (VMS p1 (push n2 (push n1 s)) m) (VMS p2 s m) }
162
163
164
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post cond ofs }
    ensures { result.code.length --> code_cd.length }
165
166
  = let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in
    hoare ibinop_pre c (icjump_post cond ofs)
167

Martin Clochard's avatar
Martin Clochard committed
168
  (*  binary Boolean operators specification (Ibeq, Ibne, Ible, Ibgt) *)
169
  constant beq : cond = fun x y -> x = y
170
  meta rewrite_def function beq
171

172
  constant bne : cond = fun x y -> x <> y
173
  meta rewrite_def function bne
174

175
  constant ble : cond = fun x y -> x <= y
176
  meta rewrite_def function ble
177

178
  constant bgt : cond = fun x y -> x > y
179
  meta rewrite_def function bgt
180

Martin Clochard's avatar
Martin Clochard committed
181
  let ibeqf (ofs:ofs) : hl 'a
182
183
184
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post beq ofs }
    ensures { result.code.length --> 1 }
185
  = create_cjump (ibeq ofs) beq ofs
186

Martin Clochard's avatar
Martin Clochard committed
187
  let ibnef (ofs:ofs) : hl 'a
188
189
190
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post bne ofs }
    ensures { result.code.length --> 1 }
191
  = create_cjump (ibne ofs) bne ofs
192

Martin Clochard's avatar
Martin Clochard committed
193
  let iblef (ofs:ofs) : hl 'a
194
195
196
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post ble ofs }
    ensures { result.code.length --> 1 }
197
  = create_cjump (ible ofs) ble ofs
198

Martin Clochard's avatar
Martin Clochard committed
199
  let ibgtf (ofs:ofs) : hl 'a
200
201
202
    ensures { result.pre --> ibinop_pre }
    ensures { result.post --> icjump_post bgt ofs }
    ensures { result.code.length --> 1 }
203
  = create_cjump (ibgt ofs) bgt ofs
204

Martin Clochard's avatar
Martin Clochard committed
205
  (* Isetvar specification *)
Martin Clochard's avatar
Martin Clochard committed
206
  constant isetvar_pre : pre 'a =
207
    fun _ p ms -> exists n s m. ms = VMS p (push n s) m
Martin Clochard's avatar
Martin Clochard committed
208
  meta rewrite_def function isetvar_pre
209

Martin Clochard's avatar
Martin Clochard committed
210
  function isetvar_post (x:id) : post 'a =
211
    fun _ p ms ms' -> forall s n m.
Martin Clochard's avatar
Martin Clochard committed
212
213
      ms = VMS p (push n s) m -> ms' = VMS (p+1) s m[x <- n]
  meta rewrite_def function isetvar_post
214

Martin Clochard's avatar
Martin Clochard committed
215
  function isetvar_fun (x:id) : machine_state -> machine_state =
216
    fun ms -> match ms with
Martin Clochard's avatar
Martin Clochard committed
217
218
219
      | VMS p (Cons n s) m -> VMS (p+1) s m[x <- n]
      | _ -> ms
      end
Martin Clochard's avatar
Martin Clochard committed
220
  meta rewrite_def function isetvar_fun
221

Martin Clochard's avatar
Martin Clochard committed
222
  let isetvarf (x: id) : hl 'a
223
224
225
    ensures { result.pre --> isetvar_pre }
    ensures { result.post --> isetvar_post x }
    ensures { result.code.length --> 1 }
226
227
  = let c = $ ifunf isetvar_pre (isetvar x) (isetvar_fun x) in
    hoare isetvar_pre c (isetvar_post x)
228
229

end