python: translation to Why3 abstract syntax

parent aa52f5a8
(********************************************************************)
(* *)
(* 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. *)
(* *)
(********************************************************************)
(* Arbres de syntaxe abstraite de Mini-Python *) open Why3
type ident = string type ident = Ptree.ident
type unop = type unop =
| Uneg (* -e *) | Uneg (* -e *)
...@@ -12,15 +22,16 @@ type binop = ...@@ -12,15 +22,16 @@ type binop =
| Beq | Bneq | Blt | Ble | Bgt | Bge (* == != < <= > >= *) | Beq | Bneq | Blt | Ble | Bgt | Bge (* == != < <= > >= *)
| Band | Bor (* && || *) | Band | Bor (* && || *)
type constant = type expr = {
| Cnone expr_desc: expr_desc;
| Cbool of bool expr_loc : Why3.Loc.position;
| Cstring of string }
| Cint of int (* en Python les entiers sont en réalité de précision
arbitraire; on simplifie ici *)
type expr = and expr_desc =
| Ecst of constant | Enone
| Ebool of bool
| Eint of string
| Estring of string
| Eident of ident | Eident of ident
| Ebinop of binop * expr * expr | Ebinop of binop * expr * expr
| Eunop of unop * expr | Eunop of unop * expr
...@@ -28,12 +39,18 @@ type expr = ...@@ -28,12 +39,18 @@ type expr =
| Elist of expr list | Elist of expr list
| Eget of expr * expr (* e1[e2] *) | Eget of expr * expr (* e1[e2] *)
and stmt = and stmt = {
stmt_desc: stmt_desc;
stmt_loc : Loc.position;
}
and stmt_desc =
| Sif of expr * stmt * stmt | Sif of expr * stmt * stmt
| Sreturn of expr | Sreturn of expr
| Sassign of ident * expr | Sassign of ident * expr
| Sprint of expr | Sprint of expr
| Sblock of stmt list | Sblock of stmt list
| Swhile of expr * Ptree.loop_annotation * stmt
| Sfor of ident * expr * stmt | Sfor of ident * expr * stmt
| Seval of expr | Seval of expr
| Sset of expr * expr * expr (* e1[e2] = e3 *) | Sset of expr * expr * expr (* e1[e2] = e3 *)
......
(********************************************************************)
(* *)
(* 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. *)
(* *)
(********************************************************************)
{ {
open Lexing open Lexing
...@@ -10,12 +20,12 @@ ...@@ -10,12 +20,12 @@
let h = Hashtbl.create 32 in let h = Hashtbl.create 32 in
List.iter (fun (s, tok) -> Hashtbl.add h s tok) List.iter (fun (s, tok) -> Hashtbl.add h s tok)
["def", DEF; "if", IF; "else", ELSE; ["def", DEF; "if", IF; "else", ELSE;
"return", RETURN; "print", PRINT; "return", RETURN; "print", PRINT; "while", WHILE;
"for", FOR; "in", IN; "for", FOR; "in", IN;
"and", AND; "or", OR; "not", NOT; "and", AND; "or", OR; "not", NOT;
"True", CST (Cbool true); "True", TRUE;
"False", CST (Cbool false); "False", FALSE;
"None", CST Cnone;]; "None", NONE;];
fun s -> try Hashtbl.find h s with Not_found -> IDENT s fun s -> try Hashtbl.find h s with Not_found -> IDENT s
let newline lexbuf = let newline lexbuf =
...@@ -72,9 +82,8 @@ rule next_tokens = parse ...@@ -72,9 +82,8 @@ rule next_tokens = parse
| ',' { [COMMA] } | ',' { [COMMA] }
| ':' { [COLON] } | ':' { [COLON] }
| integer as s | integer as s
{ try [CST (Cint (int_of_string s))] { [INTEGER s] }
with _ -> raise (Lexing_error ("constant too large: " ^ s)) } | '"' { [STRING (string lexbuf)] }
| '"' { [CST (Cstring (string lexbuf))] }
| eof { [EOF] } | eof { [EOF] }
| _ as c { raise (Lexing_error ("illegal character: " ^ String.make 1 c)) } | _ as c { raise (Lexing_error ("illegal character: " ^ String.make 1 c)) }
...@@ -104,7 +113,7 @@ and string = parse ...@@ -104,7 +113,7 @@ and string = parse
{ {
let next_token = let next_token =
let tokens = Queue.create () in (* prochains lexèmes à renvoyer *) let tokens = Queue.create () in
fun lb -> fun lb ->
if Queue.is_empty tokens then begin if Queue.is_empty tokens then begin
let l = next_tokens lb in let l = next_tokens lb in
......
(********************************************************************)
(* *)
(* 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. *)
(* *)
(********************************************************************)
open Why3 open Why3
open Mlw_module open Mlw_module
...@@ -7,6 +17,119 @@ open Stdlib ...@@ -7,6 +17,119 @@ open Stdlib
let debug = Debug.register_flag "mini-python" let debug = Debug.register_flag "mini-python"
~desc:"mini-python plugin debug flag" ~desc:"mini-python plugin debug flag"
let mk_id ?(loc=Loc.dummy_position) name =
{ id_str = name; id_lab = []; id_loc = loc }
let mk_expr ?(loc=Loc.dummy_position) d =
{ expr_desc = d; expr_loc = loc }
let mk_unit ~loc =
mk_expr ~loc (Etuple [])
let empty_spec = {
sp_pre = [];
sp_post = [];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
}
type env = {
vars: unit Hstr.t;
}
let infix ~loc s = Qident (mk_id ~loc ("infix " ^ s))
let prefix ~loc s = Qident (mk_id ~loc ("prefix " ^ s))
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 ->
mk_expr ~loc (Econst (Number.ConstInt (Number.int_const_dec s)))
| Py_ast.Estring _s ->
assert false (*TODO*)
| Py_ast.Eident id ->
if not (Hstr.mem env.vars id.id_str) then
Loc.errorm ~loc "unbound variable %s" id.id_str;
mk_expr ~loc (Eidapp (prefix ~loc "!", [mk_expr ~loc (Eident (Qident id))]))
| 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])
| Py_ast.Bdiv -> assert false (*TODO*)
| Py_ast.Bmod -> assert false (*TODO*)
| 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]))
| Py_ast.Ecall (id, el) ->
assert false (*TODO*)
| Py_ast.Elist el ->
assert false
| Py_ast.Eget (e1, e2) ->
assert false (*TODO*)
let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
match d with
| Py_ast.Sblock sl ->
block env loc sl
| Py_ast.Seval e ->
expr env e
| Py_ast.Sprint e ->
mk_expr ~loc (Elet (mk_id ~loc "_", Gnone, expr env e, mk_unit ~loc))
| Py_ast.Sif (e, s1, s2) ->
mk_expr ~loc (Eif (expr env e, stmt env s1, stmt env s2))
| Py_ast.Swhile (e, ann, s) ->
mk_expr ~loc (Ewhile (expr env e, ann, stmt env s))
| Py_ast.Sreturn e ->
assert false (*TODO*)
| Py_ast.Sassign (id, e) ->
let e = expr env e in
if Hstr.mem env.vars id.id_str then
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
block env loc [s]
| Py_ast.Sfor (id, e, s) ->
assert false (*TODO*)
| Py_ast.Sset (e1, e2, e3) ->
assert false (*TODO*)
and block env loc = function
| [] ->
mk_unit ~loc
| { Py_ast.stmt_loc = loc; stmt_desc = Py_ast.Sassign (id, e) } :: sl
when not (Hstr.mem env.vars id.id_str) ->
let e = expr env e in (* check e *before* adding id to environment *)
Hstr.add env.vars id.id_str ();
let e1 = mk_expr ~loc (Eidapp (Qident (mk_id ~loc "ref"), [e])) in
mk_expr ~loc (Elet (id, Gnone, e1, block env loc sl))
| { Py_ast.stmt_loc = loc } as s :: sl ->
mk_expr ~loc (Esequence (stmt env s, block env loc sl))
let translate inc (_dl, s) =
let params = [Loc.dummy_position, None, false, Some (PTtuple [])] in
let env = { vars = Hstr.create 32 } in
let fd = (params, None, stmt env s, empty_spec) in
let main = Dfun (mk_id "main", Gnone, fd) in
inc.new_pdecl Loc.dummy_position main
let read_channel env path file c = let read_channel env path file c =
let lb = Lexing.from_channel c in let lb = Lexing.from_channel c in
Loc.set_file file lb; Loc.set_file file lb;
...@@ -17,12 +140,13 @@ let read_channel env path file c = ...@@ -17,12 +140,13 @@ let read_channel env path file c =
let name = String.capitalize_ascii file in let name = String.capitalize_ascii file in
Debug.dprintf debug "building module %s.@." name; Debug.dprintf debug "building module %s.@." name;
let inc = Mlw_typing.open_file env path in let inc = Mlw_typing.open_file env path in
let id = { id_str = name; id_lab = []; id_loc = Loc.dummy_position } in inc.open_module (mk_id name);
inc.open_module id; let use_import (f, m) =
(* Typing.add_decl id.id_loc *) let q = Qdot (Qident (mk_id f), mk_id m) in
(* (Duse (Qdot (Qident (mk_id "ocaml"), mk_id "OCaml") )); *) let use = {use_theory = q; use_import = Some (true, m) }, None in
(* Typing.close_scope id.id_loc ~import:true; *) inc.use_clone Loc.dummy_position use in
(* List.iter (fun x -> add_decl (loc_of_decl x) x) f; *) List.iter use_import ["int", "Int"; "ref", "Ref"; "seq", "Seq"];
translate inc f;
inc.close_module (); inc.close_module ();
let mm, _ as res = Mlw_typing.close_file () in let mm, _ as res = Mlw_typing.close_file () in
if path = [] && Debug.test_flag debug then begin if path = [] && Debug.test_flag debug then begin
......
(********************************************************************)
(* *)
(* 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. *)
(* *)
(********************************************************************)
%{ %{
open Why3
open Ptree
open Py_ast open Py_ast
let floc s e = Loc.extract (s,e)
let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
let mk_term d s e = { term_desc = d; term_loc = floc s e }
let mk_expr loc d = { expr_desc = d; expr_loc = loc }
let mk_stmt loc d = { stmt_desc = d; stmt_loc = loc }
let variant_union v1 v2 = match v1, v2 with
| _, [] -> v1
| [], _ -> v2
| _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
"multiple `variant' clauses are not allowed"
let empty_annotation =
{ loop_invariant = []; loop_variant = [] }
%} %}
%token <Py_ast.constant> CST %token <string> INTEGER
%token <string> STRING
%token <Py_ast.binop> CMP %token <Py_ast.binop> CMP
%token <string> IDENT %token <string> IDENT
%token DEF IF ELSE RETURN PRINT FOR IN AND OR NOT %token DEF IF ELSE RETURN PRINT WHILE FOR IN AND OR NOT NONE TRUE FALSE
%token EOF %token EOF
%token LP RP LSQ RSQ COMMA EQUAL COLON BEGIN END NEWLINE %token LP RP LSQ RSQ COMMA EQUAL COLON BEGIN END NEWLINE
%token PLUS MINUS TIMES DIV MOD %token PLUS MINUS TIMES DIV MOD
/* annotations */
%token INVARIANT VARIANT
%left OR %left OR
%left AND %left AND
%nonassoc NOT %nonassoc NOT
...@@ -28,7 +60,7 @@ ...@@ -28,7 +60,7 @@
file: file:
| NEWLINE? dl = list(def) b = list(stmt) EOF | NEWLINE? dl = list(def) b = list(stmt) EOF
{ dl, Sblock b } { dl, { stmt_desc = Sblock b; stmt_loc = floc $startpos(b) $endpos(b) } }
; ;
def: def:
...@@ -38,8 +70,21 @@ def: ...@@ -38,8 +70,21 @@ def:
; ;
expr: expr:
| c = CST | d = expr_desc
{ Ecst c } { mk_expr (floc $startpos $endpos) d }
;
expr_desc:
| NONE
{ Enone }
| TRUE
{ Ebool true }
| FALSE
{ Ebool false }
| c = INTEGER
{ Eint c }
| s = STRING
{ Estring s }
| id = ident | id = ident
{ Eident id } { Eident id }
| e1 = expr LSQ e2 = expr RSQ | e1 = expr LSQ e2 = expr RSQ
...@@ -55,28 +100,67 @@ expr: ...@@ -55,28 +100,67 @@ expr:
| LSQ l = separated_list(COMMA, expr) RSQ | LSQ l = separated_list(COMMA, expr) RSQ
{ Elist l } { Elist l }
| LP e = expr RP | LP e = expr RP
{ e } { e.expr_desc }
;
%inline binop:
| PLUS { Badd }
| MINUS { Bsub }
| TIMES { Bmul }
| DIV { Bdiv }
| MOD { Bmod }
| c=CMP { c }
| AND { Band }
| OR { Bor }
;
located(X):
| X { mk_stmt (floc $startpos $endpos) $1 }
; ;
suite: suite: located(suite_desc) { $1 };
suite_desc:
| s = simple_stmt NEWLINE | s = simple_stmt NEWLINE
{ s } { s.stmt_desc }
| NEWLINE BEGIN l = nonempty_list(stmt) END | NEWLINE BEGIN l = nonempty_list(stmt) END
{ Sblock l } { Sblock l }
; ;
stmt: stmt: located(stmt_desc) { $1 };
stmt_desc:
| s = simple_stmt NEWLINE | s = simple_stmt NEWLINE
{ s } { s.stmt_desc }
| IF c = expr COLON s = suite | IF c = expr COLON s = suite
{ Sif (c, s, Sblock []) } { Sif (c, s, mk_stmt (floc $startpos $endpos) (Sblock [])) }
| IF c = expr COLON s1 = suite ELSE COLON s2 = suite | IF c = expr COLON s1 = suite ELSE COLON s2 = suite
{ Sif (c, s1, s2) } { Sif (c, s1, s2) }
| WHILE e = expr COLON s = simple_stmt NEWLINE
{ Swhile (e, empty_annotation, s) }
| WHILE e = expr COLON NEWLINE BEGIN a=loop_annotation l=nonempty_list(stmt) END
{ Swhile (e, a, mk_stmt (floc $startpos(l) $endpos(l)) (Sblock l)) }
| FOR x = ident IN e = expr COLON s = suite | FOR x = ident IN e = expr COLON s = suite
{ Sfor (x, e, s) } { Sfor (x, e, s) }
; ;
simple_stmt: loop_annotation:
| (* epsilon *)
{ empty_annotation }
| invariant loop_annotation
{ let a = $2 in { a with loop_invariant = $1 :: a.loop_invariant } }
| variant loop_annotation
{ let a = $2 in { a with loop_variant = variant_union $1 a.loop_variant } }
invariant:
| INVARIANT i=term { i }
variant:
| VARIANT l=comma_list1(term) { List.map (fun t -> t, None) l }
simple_stmt: located(simple_stmt_desc) { $1 };
simple_stmt_desc:
| RETURN e = expr | RETURN e = expr
{ Sreturn e } { Sreturn e }
| id = ident EQUAL e = expr | id = ident EQUAL e = expr
...@@ -89,19 +173,21 @@ simple_stmt: ...@@ -89,19 +173,21 @@ simple_stmt:
{ Seval e } { Seval e }
; ;
%inline binop:
| PLUS { Badd }
| MINUS { Bsub }
| TIMES { Bmul }
| DIV { Bdiv }
| MOD { Bmod }
| c=CMP { c }
| AND { Band }
| OR { Bor }
;
ident: ident:
id = IDENT { id } id = IDENT { mk_id id $startpos $endpos }
; ;
/* logic */
mk_term(X): d = X { mk_term d $startpos $endpos }
term: t = mk_term(term_) { t }
term_:
| ident { Tident (Qident $1) }
| INTEGER { Tconst (Number.ConstInt ((Number.int_const_dec $1))) }
| TRUE { Ttrue }
| FALSE { Tfalse }
comma_list1(X):
| separated_nonempty_list(COMMA, X) { $1 }
a = 0
b = 1
while b < 100:
print(a)
b = a+b
a = b-a
# Local Variables: # Local Variables:
# compile-command: "make -C ../.. && why3 ide test.py" # compile-command: "make -C ../.. && why3 ide test.py"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment