compiler.mlw 8.96 KB
Newer Older
1 2 3 4 5 6


(*Imp to ImpVm compiler *)
(**************************************************************************)
module Compile_aexpr

7 8


9 10 11 12 13 14 15
  use import int.Int
  use import list.List
  use import list.Length
  use import list.Append
  use import imp.Imp
  use import vm.Vm
  use import state.State
16 17
  use import logic.Compiler_logic
  use import specs.VM_arith_instr_spec
18

19 20
  function aexpr_post (a:aexpr) (len:pos) : 'a -> pos -> post =
  \ x p ms ms'.
21 22 23 24 25
    match ms with
     | VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
    end

    lemma aexpr_post_lemma:
26 27
     forall a len, x: 'a, p ms ms'.
      aexpr_post a len x p ms ms' =
28 29 30 31 32
       match ms with
        | VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
       end

    meta rewrite prop aexpr_post_lemma
33 34


35
  let rec compile_aexpr (a : aexpr) :  hl 'a
36
    variant { a }
37
    ensures { result.pre = trivial_pre }
38
    ensures { result.post = aexpr_post a result.code.length }
39
    ensures { hl_correctness result}
40
    = let c = match a with
41 42 43 44 45 46 47
       | Anum n     -> $ iconstf n
       | Avar x     -> $ ivarf x
       | Aadd a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~  $ iaddf ()
       | Asub a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~  $ isubf ()
       | Amul a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~  $ imulf ()
      end in
       let ghost pre = trivial_pre in
Léon Gondelman's avatar
Léon Gondelman committed
48
        let ghost post = aexpr_post a c.wcode.length
49
        in hoare pre c post
50

51 52 53 54 55 56
  let compile_aexpr_natural (a: aexpr) : code
    ensures { forall c p s m.
              codeseq_at c p result ->
              transition_star c
                (VMS  p                                    s  m)
                (VMS (p + length result) (push (aeval m a) s) m) }
57 58
  = let res =  (compile_aexpr a) : hl unit in
   assert { forall p s m. res.pre () p (VMS p s m) };
Léon Gondelman's avatar
Léon Gondelman committed
59
   res.code
60

Léon Gondelman's avatar
Léon Gondelman committed
61 62 63 64 65 66 67 68 69 70 71
end

module Compile_bexpr

  use import int.Int
  use import list.List
  use import list.Length
  use import list.Append
  use import imp.Imp
  use import vm.Vm
  use import state.State
72 73 74
  use import logic.Compiler_logic
  use import specs.VM_arith_instr_spec
  use import specs.VM_bool_instr_spec
Léon Gondelman's avatar
Léon Gondelman committed
75 76
  use import Compile_aexpr

Léon Gondelman's avatar
Léon Gondelman committed
77 78

  function bexpr_post (b:bexpr) (cond: bool) (out_t:pos) (out_f:pos)
79 80
  : 'a -> pos -> post =
    \x p ms ms'. match ms with
Léon Gondelman's avatar
Léon Gondelman committed
81 82 83
      | VMS _ s m -> if beval m b = cond
        then ms' = VMS (p + out_t) s m
        else ms' = VMS (p + out_f) s m
Martin Clochard's avatar
Martin Clochard committed
84
      end
Léon Gondelman's avatar
Léon Gondelman committed
85

86
  meta rewrite_def function bexpr_post
Léon Gondelman's avatar
Léon Gondelman committed
87

88 89
  function exn_bool (b1: bexpr) (cond: bool) : 'a -> pos -> pred =
   \x p ms. match ms with
Léon Gondelman's avatar
Léon Gondelman committed
90 91
            | VMS _ _ m -> beval m b1 = cond end

92
  meta rewrite_def function exn_bool
Léon Gondelman's avatar
Léon Gondelman committed
93 94


95
  let rec compile_bexpr (b : bexpr) (cond: bool) (ofs: pos) :  hl 'a
Léon Gondelman's avatar
Léon Gondelman committed
96 97 98 99 100 101 102
    variant { b }
    ensures { result.pre = trivial_pre }
    ensures { result.post =
              bexpr_post b cond (result.code.length + ofs) result.code.length }
    ensures { hl_correctness result}
    =
    let c = match b with
103 104 105
       | Btrue      -> $ if cond then ibranchf ofs else inil ()
       | Bfalse     -> $ if cond then inil () else ibranchf ofs
       | Bnot b1    -> $ compile_bexpr b1 (not cond) ofs
Léon Gondelman's avatar
Léon Gondelman committed
106
       | Band b1 b2 ->
107 108 109 110
         let c2  = $ compile_bexpr b2 cond ofs % exn_bool b1 False in
          let ofs = if cond then length c2.wcode else ofs + length c2.wcode in
           let c1 = $ compile_bexpr b1 False ofs in
            c1 ~ c2
Léon Gondelman's avatar
Léon Gondelman committed
111 112 113 114 115
       | Beq a1 a2 ->
         $ compile_aexpr a1 ~ $ compile_aexpr a2 ~
         $ if cond then ibeqf ofs else ibnef ofs
       | Ble a1 a2 ->
          $ compile_aexpr a1 ~ $ compile_aexpr a2 ~
116 117
          $ if cond then iblef ofs else ibgtf ofs
      end  in
Léon Gondelman's avatar
Léon Gondelman committed
118 119 120 121
      let ghost pre = trivial_pre in
        let ghost post = bexpr_post b cond (c.wcode.length + ofs) c.wcode.length  in
        hoare pre c post

122 123 124



Léon Gondelman's avatar
Léon Gondelman committed
125 126 127 128 129 130 131
 let compile_bexpr_natural (b: bexpr) (cond: bool) (ofs: pos) : code
    ensures {
     forall c p s m.
       codeseq_at c p result ->
         transition_star c
           (VMS  p s  m)
           (VMS (p + length result + if beval m b = cond then ofs else 0) s m) }
132 133
  = let res =  (compile_bexpr b cond ofs) : hl unit in
   assert { forall p s m. res.pre () p (VMS p s m) };
Léon Gondelman's avatar
Léon Gondelman committed
134 135 136 137
   res.code
end


138 139


Léon Gondelman's avatar
Léon Gondelman committed
140 141
module Compile_com

142
  meta compute_max_steps 65536
Léon Gondelman's avatar
Léon Gondelman committed
143 144 145 146 147 148 149
  use import int.Int
  use import list.List
  use import list.Length
  use import list.Append
  use import imp.Imp
  use import vm.Vm
  use import state.State
150 151 152
  use import logic.Compiler_logic
  use import specs.VM_arith_instr_spec
  use import specs.VM_bool_instr_spec
Léon Gondelman's avatar
Léon Gondelman committed
153 154 155 156
  use import Compile_aexpr
  use import Compile_bexpr


157 158
  function com_pre (cmd: com) : 'a -> pos -> pred =
   \x p ms. match ms with  VMS p' _ m -> p = p' /\ exists m'. ceval m cmd m' end
Léon Gondelman's avatar
Léon Gondelman committed
159 160

  lemma com_pre_lemma:
161
   forall cmd, x:'a, p ms. com_pre cmd x p ms =
Léon Gondelman's avatar
Léon Gondelman committed
162 163 164 165
    match ms with  VMS p' _ m -> p = p' /\ exists m'. ceval m cmd m' end

   meta rewrite prop com_pre_lemma

166 167
  function com_post (cmd: com) (len:pos) : 'a -> pos -> post =
  \x p ms ms'. match ms, ms' with
Léon Gondelman's avatar
Léon Gondelman committed
168 169 170 171 172
              | VMS p s m, VMS p' s' m'  ->
                p' = p + len /\ s' = s /\ ceval m cmd m'
             end

  lemma com_post_lemma:
173
    forall cmd len, x:'a, p ms ms'. com_post cmd len x p ms ms' =
Léon Gondelman's avatar
Léon Gondelman committed
174 175 176 177 178 179 180
     match ms, ms' with
              | VMS p s m, VMS p' s' m'  ->
                p' = p + len /\ s' = s /\ ceval m cmd m'
             end

  meta rewrite prop com_post_lemma

181 182 183 184 185
 function exn_bool_old (b1: bexpr) (cond: bool) : ('a,machine_state) -> pos -> pred =
   \x p ms. match snd x with
            | VMS _ _ m -> beval m b1 = cond end

  meta rewrite_def function exn_bool_old
Léon Gondelman's avatar
Léon Gondelman committed
186 187


188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
  function loop_invariant (c: com) : ('a,machine_state) -> pos -> pred =
  \ x p msi. let ms0 = snd x in
     match ms0, msi with
      | VMS _ s0 m0, VMS pi si mi ->
        pi = p /\ s0 = si /\ exists mf. ceval m0 c mf /\ ceval mi c mf
     end

  meta rewrite_def function loop_invariant


  function loop_post (c : com) (len: pos) : ('a,machine_state) -> pos -> pred =
   \ x p msf. let ms0 = snd x in
     match ms0, msf with
      | VMS _ s0 m0, VMS pf sf mf ->
        pf = p + len /\ s0 = sf /\ ceval m0 c mf
     end

  meta rewrite_def function loop_post

  function loop_variant (c : com) (test: bexpr) : ('a -> pos -> post) =
   \ x p msj msi.
     match msj, msi with
      | VMS pj sj mj, VMS pi si mi ->
       pj = pi /\ sj = si /\ ceval mi c mj /\ beval mi test = True
     end

  meta rewrite_def function loop_variant


217
  let rec compile_com (cmd: com) : hl 'a
Léon Gondelman's avatar
Léon Gondelman committed
218 219 220 221 222 223 224 225 226 227 228 229 230
  variant  { cmd }
  ensures  { result.pre = com_pre cmd }
  ensures  { result.post = com_post cmd result.code.length }
  ensures  { hl_correctness result }
  = let res =
      match cmd with
       | Cskip              -> $ inil ()
       | Cassign x a        -> $ compile_aexpr a  ~ $ isetvarf x
       | Cseq cmd1 cmd2     -> $ compile_com cmd1 ~ $ compile_com cmd2
       | Cif cond cmd1 cmd2 ->
       let code_true   = compile_com cmd1 in
       let code_false  = compile_com cmd2 in
        $ compile_bexpr cond False (code_true.code.length + 1) ~
231 232
        (($ code_true ~ $ ibranchf code_false.code.length) % exn_bool cond False)  ~
        ($ code_false % exn_bool_old cond True)
233 234 235 236 237 238 239 240 241 242 243 244
       | Cwhile test body  ->
          let code_body = compile_com body in
           let body_length = length code_body.code + 1 in
            let code_test = compile_bexpr test False (body_length) in
           let ofs = (length code_test.code + body_length) in
            let wp_while = $ code_test ~
              ($ code_body ~ $ ibranchf (- ofs)) % exn_bool test False in
            let ghost inv  = loop_invariant cmd in
            let ghost var  = loop_variant body test  in
            let ghost post = loop_post cmd ofs in
            let hl_while = hoare inv wp_while (loop_preservation inv var post) in
            $ inil () ~ $ make_loop_hl hl_while inv var post
Léon Gondelman's avatar
Léon Gondelman committed
245 246 247 248
      end
     in
    let ghost pre  = com_pre cmd in
    let ghost post = com_post cmd res.wcode.length  in
249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
    hoare pre res post




 let compile_com_natural (com: com) : code
    ensures {
     forall c p s m m'.
        ceval m com m' ->
         codeseq_at c p result ->
          transition_star c
           (VMS  p s  m)
            (VMS (p + length result) s m') }
  = let res =  compile_com com : hl unit in
   assert { forall p s m m'. ceval m com m' -> res.pre () p (VMS p s m) };
   res.code


 let compile_program (prog : com) : code
   ensures { forall  mi mf: state.
    ceval mi prog mf -> vm_terminates result mi mf }
  = compile_com_natural prog ++ ihalt

Léon Gondelman's avatar
Léon Gondelman committed
272 273


274 275
end

276

277

Léon Gondelman's avatar
Léon Gondelman committed
278 279 280 281 282 283
(*
Local Variables:
compile-command: "why3 ide -L . compiler.mlw"
End:
*)

284

Martin Clochard's avatar
Martin Clochard committed
285
(* *)
286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307

   (*
   (res.wp p post) ms ->
     (exists ms' : machine_state. (post ms')
      /\ contextual_irrelevance res.wcode p ms ms')
  *)

 (*
   (res.wp p post) ms
   exists ms'
   -----------------------------------------------
   (post ms') /\ contextual_irrelevance res.wcode p ms ms')
  *)

 (*condition suffisante ? *)
(* trouver un ms' qui vérifie :
 ((s2.wp (p + s1.wcode.length) post) ms')  /\ contextual_irrelevance res.wcode p ms ms' *)

 (*
   (res.wp p post) ms
   exists ms'
   -----------------------------------------------
Martin Clochard's avatar
Martin Clochard committed
308
   (post ms') /\ contextual_irrelevance res.wcode p ms ms') *)