py_main.ml 14 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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

open Why3
13
open Pmodule
14
open Py_ast
15
open Ptree
16
open Wstdlib
17

18
let debug = Debug.register_flag "python"
19
  ~desc:"mini-python plugin debug flag"
20 21 22 23

(* NO! this will be executed at plugin load, thus
disabling the warning for ALL WHY3 USERS even if they don't
use the python front-end
24
let () = Debug.set_flag Dterm.debug_ignore_unused_var
25
*)
26

27
let mk_id ~loc name =
Andrei Paskevich's avatar
Andrei Paskevich committed
28
  { id_str = name; id_ats = []; id_loc = loc }
29

30 31
let infix  ~loc s = Qident (mk_id ~loc (Ident.op_infix s))
let prefix ~loc s = Qident (mk_id ~loc (Ident.op_prefix s))
32 33
let get_op ~loc   = Qident (mk_id ~loc (Ident.op_get ""))
let set_op ~loc   = Qident (mk_id ~loc (Ident.op_set ""))
34

35
let mk_expr ~loc d =
36
  { expr_desc = d; expr_loc = loc }
37
let mk_term ~loc d =
38
  { term_desc = d; term_loc = loc }
39
let mk_pat ~loc d =
40
  { pat_desc = d; pat_loc = loc }
41 42
let mk_unit ~loc =
  mk_expr ~loc (Etuple [])
43 44
let mk_var ~loc id =
  mk_expr ~loc (Eident (Qident id))
45 46
let mk_tvar ~loc id =
  mk_term ~loc (Tident (Qident id))
47 48 49 50
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))]))
51
let array_set ~loc a i v =
52
  mk_expr ~loc (Eidapp (set_op ~loc, [a; i; v]))
53 54 55 56
let constant ~loc i =
  mk_expr ~loc (Econst (Number.const_of_int i))
let constant_s ~loc s =
  mk_expr ~loc (Econst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s})))
57 58
let len ~loc =
  Qident (mk_id ~loc "len")
59 60
let break ~loc =
  Qident (mk_id ~loc "Break")
61
let break_handler ~loc =
62
  [break ~loc, None, mk_unit ~loc]
63 64 65 66
let return ~loc =
  Qident (mk_id ~loc "Return")
let return_handler ~loc =
  let x = mk_id ~loc "x" in
67
  [return ~loc, Some (mk_pat ~loc (Pvar x)), mk_var ~loc x]
68 69 70
let array_make ~loc n v =
  mk_expr ~loc (Eidapp (Qdot (Qident (mk_id ~loc "Array"), mk_id ~loc "make"),
                        [n; v]))
71 72 73 74 75 76 77

let empty_spec = {
  sp_pre     = [];
  sp_post    = [];
  sp_xpost   = [];
  sp_reads   = [];
  sp_writes  = [];
78
  sp_alias   = [];
79 80 81 82 83 84
  sp_variant = [];
  sp_checkrw = false;
  sp_diverge = false;
}

type env = {
85 86
  vars: ident Mstr.t;
  for_index: int;
87 88
}

89 90 91 92 93 94 95 96 97 98 99 100
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
101

102 103 104 105 106 107
(* 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
108
  Mstr.fold deref env.vars t
109

110
let stmt_of_decl = function Dstmt s -> s | _ -> invalid_arg "not a statement"
111

112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
let rec has_stmt p = function
  | Dstmt s -> p s || begin match s.stmt_desc with
    | Sbreak  | Sreturn _ | Sassign _ | Slabel _
    | Seval _ | Sset _ | Sassert _ | Swhile _ -> false
    | Sif (_, bl1, bl2) -> has_stmtl p bl1 || has_stmtl p bl2
    | Sfor (_, _, _, bl) -> has_stmtl p bl end
  | _ -> false
and has_stmtl p bl = List.exists (has_stmt p) bl

let has_breakl = has_stmtl (fun s -> s.stmt_desc = Sbreak)
let has_returnl = has_stmtl (function { stmt_desc = Sreturn _ } -> true | _ -> false)

let rec expr_has_call id e = match e.Py_ast.expr_desc with
  | Enone | Ebool _ | Eint _ | Estring _ | Py_ast.Eident _ -> false
  | Emake (e1, e2) | Eget (e1, e2) | Ebinop (_, e1, e2) ->
    expr_has_call id e1 || expr_has_call id e2
  | Eunop (_, e1) -> expr_has_call id e1
  | Ecall (f, el) -> id.id_str = f.id_str || List.exists (expr_has_call id) el
  | Elist el -> List.exists (expr_has_call id) el

let rec stmt_has_call id s = match s.stmt_desc with
  | Sbreak | Slabel _ | Sassert _ -> false
  | Sreturn e | Sassign (_, e) | Seval e -> expr_has_call id e
  | Sset (e1, e2, e3) ->
    expr_has_call id e1 || expr_has_call id e2 || expr_has_call id e3
  | Sif (e, s1, s2) -> expr_has_call id e || block_has_call id s1 || block_has_call id s2
138
  | Sfor (_, e, _, s) | Swhile (e, _, _, s) -> expr_has_call id e || block_has_call id s
139
and block_has_call id = has_stmtl (stmt_has_call id)
140

141 142 143 144 145 146
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 ->
147
    constant_s ~loc s
148
  | Py_ast.Estring _s ->
149
    mk_unit ~loc (*FIXME*)
150
  | Py_ast.Eident id ->
151
    if not (Mstr.mem id.id_str env.vars) then
152
      Loc.errorm ~loc "unbound variable %s" id.id_str;
153
    deref_id ~loc id
154 155 156 157
  | Py_ast.Ebinop (op, e1, e2) ->
    let e1 = expr env e1 in
    let e2 = expr env e2 in
    mk_expr ~loc (match op with
158 159
      | Py_ast.Band -> Eand (e1, e2)
      | Py_ast.Bor  -> Eor  (e1, e2)
160 161 162
      | Py_ast.Badd -> Eidapp (infix ~loc "+", [e1; e2])
      | Py_ast.Bsub -> Eidapp (infix ~loc "-", [e1; e2])
      | Py_ast.Bmul -> Eidapp (infix ~loc "*", [e1; e2])
163 164
      | Py_ast.Bdiv -> Eidapp (infix ~loc "//", [e1; e2])
      | Py_ast.Bmod -> Eidapp (infix ~loc "%", [e1; e2])
165 166 167 168 169 170 171 172 173 174 175
      | 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]))
176 177
  | Py_ast.Ecall ({id_str="print"}, el) ->
    let eval res e =
178
      mk_expr ~loc (Elet (mk_id ~loc "_", false, Expr.RKnone, expr env e, res)) in
179
    List.fold_left eval (mk_unit ~loc) el
180 181
  | Py_ast.Ecall (id, el) ->
    mk_expr ~loc (Eidapp (Qident id, List.map (expr env) el))
182 183 184
  | Py_ast.Emake (e1, e2) -> (* [e1]*e2 *)
    array_make ~loc (expr env e2) (expr env e1)
  | Py_ast.Elist [] ->
185
    array_make ~loc (constant ~loc 0) (constant ~loc 0)
186 187
  | Py_ast.Elist el ->
    let n = List.length el in
188
    let n = constant ~loc n in
189
    let id = mk_id ~loc "new array" in
190
    mk_expr ~loc (Elet (id, false, Expr.RKnone, array_make ~loc n (constant ~loc 0),
191 192
    let i = ref (-1) in
    let init seq e =
193
      incr i; let i = constant ~loc !i in
194 195 196
      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))
197
  | Py_ast.Eget (e1, e2) ->
198
    mk_expr ~loc (Eidapp (get_op ~loc, [expr env e1; expr env e2]))
199

200 201 202 203 204 205 206 207 208 209 210 211
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 }

let no_params ~loc = [loc, None, false, Some (PTtuple [])]

212 213 214 215 216
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) ->
217
    mk_expr ~loc (Eif (expr env e, block env ~loc s1, block env ~loc s2))
218 219
  | Py_ast.Sreturn e ->
    mk_expr ~loc (Eraise (return ~loc, Some (expr env e)))
220 221
  | Py_ast.Sassign (id, e) ->
    let e = expr env e in
222
    if Mstr.mem id.id_str env.vars then
223
      let x = let loc = id.id_loc in mk_expr ~loc (Eident (Qident id)) in
224
      mk_expr ~loc (Einfix (x, mk_id ~loc (Ident.op_infix ":="), e))
225
    else
226
      block env ~loc [Dstmt s]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227
  | Py_ast.Sset (e1, e2, e3) ->
228
    array_set ~loc (expr env e1) (expr env e2) (expr env e3)
229 230
  | Py_ast.Sassert (k, t) ->
    mk_expr ~loc (Eassert (k, deref env t))
231 232 233
  | Py_ast.Swhile (e, inv, var, s) ->
    let inv = List.map (deref env) inv in
    let var = List.map (fun (t, o) -> deref env t, o) var in
234
    let loop = mk_expr ~loc
235
      (Ewhile (expr env e, inv, var, block env ~loc s)) in
236
    if has_breakl s then mk_expr ~loc (Ematch (loop, [], break_handler ~loc))
237
    else loop
238 239
  | Py_ast.Sbreak ->
    mk_expr ~loc (Eraise (break ~loc, None))
240 241
  | Py_ast.Slabel _ ->
    mk_unit ~loc (* ignore lonely marks *)
242 243 244
  (* make a special case for
       for id in range(e1, e2):
    *)
245
  | Py_ast.Sfor (id, {Py_ast.expr_desc=Ecall ({id_str="range"}, [e1;e2])},
246 247
                 inv, body) ->
    let inv = List.map (deref env) inv in
248
    let e_to = expr env e2 in
249
    let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [e_to; constant ~loc 1])) in
250 251
    mk_expr ~loc (Efor (id, expr env e1, Expr.To, ub, inv,
    mk_expr ~loc (Elet (id, false, Expr.RKnone, mk_ref ~loc (mk_var ~loc id),
252 253 254 255 256 257 258
    let env = add_var env id in
    block ~loc env body))))
  (* otherwise, translate
       for id in e:
         #@ invariant inv
         body
    to
259
       let l = e in
260
       for i = 0 to len(l)-1 do
261 262 263
         invariant { let id = l[i] in I }
         let id = ref l[i] in
         body
264 265
       done
    *)
266
  | Py_ast.Sfor (id, e, inv, body) ->
267 268
    let i, l, env = for_vars ~loc env in
    let e = expr env e in
269
    mk_expr ~loc (Elet (l, false, Expr.RKnone, e, (* evaluate e only once *)
270
    let lb = constant ~loc 0 in
271
    let lenl = mk_expr ~loc (Eidapp (len ~loc, [mk_var ~loc l])) in
272
    let ub = mk_expr ~loc (Eidapp (infix ~loc "-", [lenl; constant ~loc 1])) in
273 274 275
    let invariant inv =
      let loc = inv.term_loc in
      let li = mk_term ~loc
276
        (Tidapp (get_op ~loc, [mk_tvar ~loc l; mk_tvar ~loc i])) in
277
      mk_term ~loc (Tlet (id, li, deref env inv)) in
278
    mk_expr ~loc (Efor (i, lb, Expr.To, ub, List.map invariant inv,
279
    let li = mk_expr ~loc
280
      (Eidapp (get_op ~loc, [mk_var ~loc l; mk_var ~loc i])) in
281
    mk_expr ~loc (Elet (id, false, Expr.RKnone, mk_ref ~loc li,
282
    let env = add_var env id in
283
    block ~loc env body
284
    ))))))
285

286
and block env ~loc = function
287 288
  | [] ->
    mk_unit ~loc
289
  | Dstmt { stmt_loc = loc; stmt_desc = Slabel id } :: sl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
290
    mk_expr ~loc (Elabel (id, block env ~loc sl))
291
  | Dstmt { Py_ast.stmt_loc = loc; stmt_desc = Py_ast.Sassign (id, e) } :: sl
292
    when not (Mstr.mem id.id_str env.vars) ->
293
    let e = expr env e in (* check e *before* adding id to environment *)
294
    let env = add_var env id in
295
    mk_expr ~loc (Elet (id, false, Expr.RKnone, mk_ref ~loc e, block env ~loc sl))
296
  | Dstmt ({ Py_ast.stmt_loc = loc } as s) :: sl ->
297
    let s = stmt env s in
298
    if sl = [] then s else mk_expr ~loc (Esequence (s, block env ~loc sl))
299
  | Ddef (id, idl, sp, bl) :: sl ->
300 301 302 303 304 305 306 307
    (* f(x1,...,xn): body ==>
      let f x1 ... xn =
        let x1 = ref x1 in ... let xn = ref xn in
        try body with Return x -> x *)
    let env' = List.fold_left add_var empty_env idl in
    let body = block env' ~loc:id.id_loc bl in
    let body = if not (has_returnl bl) then body else
      let loc = id.id_loc in
308
      mk_expr ~loc (Ematch (body, [], return_handler ~loc)) in
309 310 311 312 313 314 315
    let local bl id =
      let loc = id.id_loc in
      let ref = mk_ref ~loc (mk_var ~loc id) in
      mk_expr ~loc (Elet (id, false, Expr.RKnone, ref, bl)) in
    let body = List.fold_left local body idl in
    let param id = id.id_loc, Some id, false, None in
    let params = if idl = [] then no_params ~loc else List.map param idl in
316
    let s = block env ~loc sl in
317 318 319 320 321 322
    let e = if block_has_call id bl then
      Erec ([id, false, Expr.RKnone, params, None, Ity.MaskVisible, sp, body], s)
    else
      let e = Efun (params, None, Ity.MaskVisible, sp, body) in
      Elet (id, false, Expr.RKnone, mk_expr ~loc e, s) in
    mk_expr ~loc e
323 324
  | (Dimport _ | Py_ast.Dlogic _) :: sl ->
    block env ~loc sl
325

326 327 328
let fresh_type_var =
  let r = ref 0 in
  fun loc -> incr r;
Andrei Paskevich's avatar
Andrei Paskevich committed
329
    PTtyvar { id_str = "a" ^ string_of_int !r; id_loc = loc; id_ats = [] }
330 331 332 333

let logic_param id =
  id.id_loc, Some id, false, fresh_type_var id.id_loc

334
let logic = function
335 336 337 338 339 340
  | Py_ast.Dlogic (func, id, idl) ->
    let d = { ld_loc = id.id_loc;
              ld_ident = id;
              ld_params = List.map logic_param idl;
              ld_type = if func then Some (fresh_type_var id.id_loc) else None;
              ld_def = None } in
341
    Typing.add_decl id.id_loc (Dlogic [d])
342
  | _ -> ()
343

344 345 346 347 348 349
let translate ~loc dl =
  List.iter logic dl;
  let bl = block empty_env ~loc dl in
  let fd = Efun (no_params ~loc, None, Ity.MaskVisible, empty_spec, bl) in
  let main = Dlet (mk_id ~loc "main", false, Expr.RKnone, mk_expr ~loc fd) in
  Typing.add_decl loc main
350

351
let read_channel env path file c =
352
  let f = Py_lexer.parse file c in
353 354 355
  Debug.dprintf debug "%s parsed successfully.@." file;
  let file = Filename.basename file in
  let file = Filename.chop_extension file in
356
  let name = Strings.capitalize file in
357
  Debug.dprintf debug "building module %s.@." name;
358 359 360
  Typing.open_file env path;
  let loc = Loc.user_position file 0 0 0 in
  Typing.open_module (mk_id ~loc name);
361
  let use_import (f, m) =
362 363 364 365
    let m = mk_id ~loc m in
    Typing.open_scope loc m;
    Typing.add_decl loc (Ptree.Duse (Qdot (Qident (mk_id ~loc f), m)));
    Typing.close_scope loc ~import:true in
366
  List.iter use_import
367
    ["int", "Int"; "ref", "Refint"; "python", "Python"];
368 369 370
  translate ~loc f;
  Typing.close_module loc;
  let mm = Typing.close_file () in
371 372
  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
373 374
    let print_m _ m = Pmodule.print_module Format.err_formatter m in
    Ident.Mid.iter print_m (Mstr.fold add_m mm Ident.Mid.empty)
375
  end;
376
  mm
377 378 379 380

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