Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

py_main.ml 11.8 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13

open Why3
open Mlw_module
14
open Py_ast
15 16 17
open Ptree
open Stdlib

18
let debug = Debug.register_flag "python"
19
  ~desc:"mini-python plugin debug flag"
20
let () = Debug.set_flag Dterm.debug_ignore_unused_var
21

22 23 24
let mk_id ?(loc=Loc.dummy_position) name =
  { id_str = name; id_lab = []; id_loc = loc }

25 26 27 28
let infix  ~loc s = Qident (mk_id ~loc ("infix "  ^ s))
let prefix ~loc s = Qident (mk_id ~loc ("prefix " ^ s))
let mixfix ~loc s = Qident (mk_id ~loc ("mixfix " ^ s))

29 30
let mk_expr ?(loc=Loc.dummy_position) d =
  { expr_desc = d; expr_loc = loc }
31 32
let mk_term ?(loc=Loc.dummy_position) d =
  { term_desc = d; term_loc = loc }
33 34
let mk_pat ?(loc=Loc.dummy_position) d =
  { pat_desc = d; pat_loc = loc }
35 36
let mk_unit ~loc =
  mk_expr ~loc (Etuple [])
37 38
let mk_var ~loc id =
  mk_expr ~loc (Eident (Qident id))
39 40
let mk_tvar ~loc id =
  mk_term ~loc (Tident (Qident id))
41 42 43 44
let mk_ref ~loc e =
  mk_expr ~loc (Eidapp (Qident (mk_id ~loc "ref"), [e]))
let deref_id ~loc id =
  mk_expr ~loc (Eidapp (prefix ~loc "!", [mk_expr ~loc (Eident (Qident id))]))
45 46
let array_set ~loc a i v =
  mk_expr ~loc (Eidapp (mixfix ~loc "[]<-", [a; i; v]))
47 48 49 50
let constant ~loc s =
  mk_expr ~loc (Econst (Number.ConstInt (Number.int_const_dec s)))
let len ~loc =
  Qident (mk_id ~loc "len")
51 52
let break ~loc =
  Qident (mk_id ~loc "Break")
53
let break_handler ~loc =
54
  [break ~loc, None, mk_unit ~loc]
55 56 57 58 59
let return ~loc =
  Qident (mk_id ~loc "Return")
let return_handler ~loc =
  let x = mk_id ~loc "x" in
  [return ~loc, Some (mk_pat ~loc (Pvar x)), mk_var ~loc x]
60 61 62
let array_make ~loc n v =
  mk_expr ~loc (Eidapp (Qdot (Qident (mk_id ~loc "Array"), mk_id ~loc "make"),
                        [n; v]))
63 64 65 66 67 68 69 70 71 72 73 74 75

let empty_spec = {
  sp_pre     = [];
  sp_post    = [];
  sp_xpost   = [];
  sp_reads   = [];
  sp_writes  = [];
  sp_variant = [];
  sp_checkrw = false;
  sp_diverge = false;
}

type env = {
76 77
  vars: ident Mstr.t;
  for_index: int;
78 79
}

80 81 82 83 84 85 86 87 88 89 90 91
let empty_env =
  { vars = Mstr.empty;
    for_index = 0; }

let add_var env id =
  { env with vars = Mstr.add id.id_str id env.vars }

let for_vars ~loc env =
  let i = env.for_index in
  let env = { env with for_index = i + 1 } in
  let i = string_of_int env.for_index in
  mk_id ~loc ("for index " ^ i ), mk_id ~loc ("for list " ^ i), env
92

93 94 95 96 97 98
(* dereference all variables from the environment *)
let deref env t =
  let deref _ ({id_loc=loc} as id) t =
    let tid = mk_term ~loc (Tident (Qident id)) in
    let tid = mk_term ~loc (Tidapp (prefix ~loc "!", [tid])) in
    mk_term ~loc:t.term_loc (Tlet (id, tid, t)) in
99
  Mstr.fold deref env.vars t
100 101 102 103 104

let loop_annotation env a =
  { loop_invariant = List.map (deref env) a.loop_invariant;
    loop_variant   = List.map (fun (t, o) -> deref env t, o) a.loop_variant }

105 106 107
let add_loop_invariant i a =
  { a with loop_invariant = i :: a.loop_invariant }

108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
let rec has_break s = match s.stmt_desc with
  | Sbreak -> true
  | Sreturn _ | Sassign _ | Slabel _
  | Seval _ | Sset _ | Sassert _ | Swhile _ -> false
  | Sif (_, bl1, bl2) -> has_breakl bl1 || has_breakl bl2
  | Sfor (_, _, _, bl) -> has_breakl bl
and has_breakl bl = List.exists has_break bl

let rec has_return s = match s.stmt_desc with
  | Sreturn _ -> true
  | Sbreak | Sassign _ | Slabel _
  | Seval _ | Sset _ | Sassert _ -> false
  | Sif (_, bl1, bl2) -> has_returnl bl1 || has_returnl bl2
  | Swhile (_, _, bl) | Sfor (_, _, _, bl) -> has_returnl bl
and has_returnl bl = List.exists has_return bl
123

124 125 126 127 128 129
let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
  | Py_ast.Enone ->
    mk_unit ~loc
  | Py_ast.Ebool b ->
    mk_expr ~loc (if b then Etrue else Efalse)
  | Py_ast.Eint s ->
130
    constant ~loc s
131
  | Py_ast.Estring _s ->
132
    mk_unit ~loc (*FIXME*)
133
  | Py_ast.Eident id ->
134
    if not (Mstr.mem id.id_str env.vars) then
135
      Loc.errorm ~loc "unbound variable %s" id.id_str;
136
    deref_id ~loc id
137 138 139 140 141 142 143 144 145
  | Py_ast.Ebinop (op, e1, e2) ->
    let e1 = expr env e1 in
    let e2 = expr env e2 in
    mk_expr ~loc (match op with
      | Py_ast.Band -> Elazy (e1, LazyAnd, e2)
      | Py_ast.Bor  -> Elazy (e1, LazyOr,  e2)
      | Py_ast.Badd -> Eidapp (infix ~loc "+", [e1; e2])
      | Py_ast.Bsub -> Eidapp (infix ~loc "-", [e1; e2])
      | Py_ast.Bmul -> Eidapp (infix ~loc "*", [e1; e2])
146 147
      | Py_ast.Bdiv -> Eidapp (Qident (mk_id ~loc "div"), [e1; e2])
      | Py_ast.Bmod -> Eidapp (Qident (mk_id ~loc "mod"), [e1; e2])
148 149 150 151 152 153 154 155 156 157 158
      | Py_ast.Beq  -> Eidapp (infix ~loc "=", [e1; e2])
      | Py_ast.Bneq -> Eidapp (infix ~loc "<>", [e1; e2])
      | Py_ast.Blt  -> Eidapp (infix ~loc "<", [e1; e2])
      | Py_ast.Ble  -> Eidapp (infix ~loc "<=", [e1; e2])
      | Py_ast.Bgt  -> Eidapp (infix ~loc ">", [e1; e2])
      | Py_ast.Bge  -> Eidapp (infix ~loc ">=", [e1; e2])
    )
  | Py_ast.Eunop (Py_ast.Uneg, e) ->
    mk_expr ~loc (Eidapp (prefix ~loc "-", [expr env e]))
  | Py_ast.Eunop (Py_ast.Unot, e) ->
    mk_expr ~loc (Eidapp (Qident (mk_id ~loc "not"), [expr env e]))
159 160 161 162
  | Py_ast.Ecall ({id_str="print"}, el) ->
    let eval res e =
      mk_expr ~loc (Elet (mk_id ~loc "_", Gnone, expr env e, res)) in
    List.fold_left eval (mk_unit ~loc) el
163 164
  | Py_ast.Ecall (id, el) ->
    mk_expr ~loc (Eidapp (Qident id, List.map (expr env) el))
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
  | Py_ast.Emake (e1, e2) -> (* [e1]*e2 *)
    array_make ~loc (expr env e2) (expr env e1)
  | Py_ast.Elist [] ->
    array_make ~loc (constant ~loc "0") (constant ~loc "0")
  | Py_ast.Elist el ->
    let n = List.length el in
    let n = constant ~loc (string_of_int n) in
    let id = mk_id ~loc "new array" in
    mk_expr ~loc (Elet (id, Gnone, array_make ~loc n (constant ~loc "0"),
    let i = ref (-1) in
    let init seq e =
      incr i; let i = constant ~loc (string_of_int !i) in
      let assign = array_set ~loc (mk_var ~loc id) i (expr env e) in
      mk_expr ~loc (Esequence (assign, seq)) in
    List.fold_left init (mk_var ~loc id) el))
180 181
  | Py_ast.Eget (e1, e2) ->
    mk_expr ~loc (Eidapp (mixfix ~loc "[]", [expr env e1; expr env e2]))
182 183 184 185 186 187

let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
  match d with
  | Py_ast.Seval e ->
    expr env e
  | Py_ast.Sif (e, s1, s2) ->
188
    mk_expr ~loc (Eif (expr env e, block env ~loc s1, block env ~loc s2))
189 190
  | Py_ast.Sreturn e ->
    mk_expr ~loc (Eraise (return ~loc, Some (expr env e)))
191 192
  | Py_ast.Sassign (id, e) ->
    let e = expr env e in
193
    if Mstr.mem id.id_str env.vars then
194 195 196
      let x = let loc = id.id_loc in mk_expr ~loc (Eident (Qident id)) in
      mk_expr ~loc (Einfix (x, mk_id ~loc "infix :=", e))
    else
197
      block env ~loc [s]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198
  | Py_ast.Sset (e1, e2, e3) ->
199
    array_set ~loc (expr env e1) (expr env e2) (expr env e3)
200 201
  | Py_ast.Sassert (k, t) ->
    mk_expr ~loc (Eassert (k, deref env t))
202
  | Py_ast.Swhile (e, ann, s) ->
203 204
    let loop = mk_expr ~loc
      (Ewhile (expr env e, loop_annotation env ann, block env ~loc s)) in
205 206
    if has_breakl s then mk_expr ~loc (Etry (loop, break_handler ~loc))
    else loop
207 208
  | Py_ast.Sbreak ->
    mk_expr ~loc (Eraise (break ~loc, None))
209 210
  | Py_ast.Slabel _ ->
    mk_unit ~loc (* ignore lonely marks *)
211 212 213 214 215 216
  | Py_ast.Sfor (id, e, inv, body) ->
    (* for x in e:
         s

    is translated to

217
       let l = e in
218 219 220 221
       for i = 0 to len(l)-1 do
         user invariants
         let x = l[i] in
         s
222 223 224 225 226
       done
    *)
    let i, l, env = for_vars ~loc env in
    let e = expr env e in
    mk_expr ~loc (Elet (l, Gnone, e, (* evaluate e only once *)
227
    let lb = constant ~loc "0" in
228
    let lenl = mk_expr ~loc (Eidapp (len ~loc, [mk_var ~loc l])) in
229
    let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [lenl;constant ~loc "1"])) in
230 231 232 233 234 235
    let invariant inv =
      let loc = inv.term_loc in
      let li = mk_term ~loc
        (Tidapp (mixfix ~loc "[]", [mk_tvar ~loc l; mk_tvar ~loc i])) in
      mk_term ~loc (Tlet (id, li, deref env inv)) in
    mk_expr ~loc (Efor (i, lb, To, ub, List.map invariant inv,
236
    let li = mk_expr ~loc
237
      (Eidapp (mixfix ~loc "[]", [mk_var ~loc l; mk_var ~loc i])) in
238
    mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc li,
239 240 241
    let env = add_var env id in
    block env body
    ))))))
242

243
and block env ?(loc=Loc.dummy_position) = function
244 245
  | [] ->
    mk_unit ~loc
246 247
  | { stmt_loc = loc; stmt_desc = Slabel id } :: sl ->
    mk_expr ~loc (Emark (id, block env ~loc sl))
248
  | { Py_ast.stmt_loc = loc; stmt_desc = Py_ast.Sassign (id, e) } :: sl
249
    when not (Mstr.mem id.id_str env.vars) ->
250
    let e = expr env e in (* check e *before* adding id to environment *)
251 252
    let env = add_var env id in
    mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc e, block env ~loc sl))
253
  | { Py_ast.stmt_loc = loc } as s :: sl ->
254
    let s = stmt env s in
255
    if sl = [] then s else mk_expr ~loc (Esequence (s, block env ~loc sl))
256

257 258 259 260 261 262 263 264 265 266
let post env (loc, l) =
  loc, List.map (fun (pat, t) -> pat, deref env t) l

let spec env sp =
  assert (sp.sp_xpost = [] && sp.sp_reads = [] && sp.sp_writes = []
    && sp.sp_variant = []);
  { sp with
    sp_pre = List.map (deref env) sp.sp_pre;
    sp_post = List.map (post env) sp.sp_post }

267 268 269 270 271
(* f(x1,...,xn): body

   let f x1 ... xn =
     let x1 = ref x1 in ... let xn = ref xn in
     try body with Return x -> x *)
272
let def inc (id, idl, sp, bl) =
273
  let loc = id.id_loc in
274 275
  let env = empty_env in
  let env = List.fold_left add_var env idl in
276 277 278
  let body = block env bl in
  let body = if has_returnl bl then
      mk_expr ~loc (Etry (body, return_handler ~loc)) else body in
279 280 281
  let local bl id =
    let loc = id.id_loc in
    mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc (mk_var ~loc id), bl)) in
282 283 284 285
  let body = List.fold_left local body idl in
  let param id = id.id_loc, Some id, false, None in
  let params = List.map param idl in
  let fd = (params, None, body, sp) in
286 287 288 289 290
  let d = Dfun (id, Gnone, fd) in
  inc.new_pdecl id.id_loc d

let translate inc (dl, s) =
  List.iter (def inc) dl;
291
  let params = [Loc.dummy_position, None, false, Some (PTtuple [])] in
292
  let env = empty_env in
293
  let fd = (params, None, block env s, empty_spec) in
294 295 296
  let main = Dfun (mk_id "main", Gnone, fd) in
  inc.new_pdecl Loc.dummy_position main

297 298 299 300 301 302 303
let read_channel env path file c =
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
  let f = Loc.with_location (Py_parser.file Py_lexer.next_token) lb in
  Debug.dprintf debug "%s parsed successfully.@." file;
  let file = Filename.basename file in
  let file = Filename.chop_extension file in
304
  let name = String.capitalize file in
305 306
  Debug.dprintf debug "building module %s.@." name;
  let inc = Mlw_typing.open_file env path in
307 308 309 310 311
  inc.open_module (mk_id name);
  let use_import (f, m) =
    let q = Qdot (Qident (mk_id f), mk_id m) in
    let use = {use_theory = q; use_import = Some (true, m) }, None in
    inc.use_clone  Loc.dummy_position use in
312
  List.iter use_import
313
    ["int", "Int"; "ref", "Refint"; "python", "Python"];
314
  translate inc f;
315 316 317 318 319 320 321 322 323 324 325 326 327 328 329
  inc.close_module ();
  let mm, _ as res = Mlw_typing.close_file () in
  if path = [] && Debug.test_flag debug then begin
    let add_m _ m modm = Ident.Mid.add m.mod_theory.Theory.th_name m modm in
    let modm = Mstr.fold add_m mm Ident.Mid.empty in
    let print_m _ m = Format.eprintf
      "@[<hov 2>module %a@\n%a@]@\nend@\n@." Pretty.print_th m.mod_theory
      (Pp.print_list Pp.newline2 Mlw_pretty.print_pdecl) m.mod_decls in
    Ident.Mid.iter print_m modm
  end;
  res

let () =
  Env.register_format mlw_language "python" ["py"] read_channel
    ~desc:"mini-Python format"