Commit 79b883d0 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre

Merge branch 'python'

parents cfa504ac 1bf178c8
......@@ -212,6 +212,18 @@ pvsbin/
/plugins/tptp/tptp_parser.conflicts
/plugins/parser/dimacs.ml
# /plugins/python/
/plugins/python/py_lexer.ml
/plugins/python/py_parser.ml
/plugins/python/py_parser.mli
/plugins/python/test/
/plugins/python/py_parser.conflicts
/plugins/python/examples/guess/
/plugins/python/examples/mult/
/plugins/python/examples/dicho/
/plugins/python/examples/sort/
/plugins/python/examples/sort++/
# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux
......@@ -284,6 +296,7 @@ pvsbin/
/modules/pqueue/
/modules/mach/array/
/modules/mach/int/
/modules/python/
# Try Why3
/src/trywhy3/trywhy3.byte
......
......@@ -17,6 +17,7 @@ S plugins/parser
S plugins/printer
S plugins/transform
S plugins/tptp
S plugins/python
B src/util
B src/core
......@@ -37,6 +38,7 @@ B plugins/parser
B plugins/printer
B plugins/transform
B plugins/tptp
B plugins/python
B lib/why3
PKG str unix num dynlink @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@
......@@ -374,20 +374,27 @@ endif
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli \
plugins/python/py_lexer.ml \
plugins/python/py_parser.ml plugins/python/py_parser.mli \
plugins/parser/dimacs.ml \
PLUG_PARSER = genequlin dimacs
PLUG_PRINTER =
PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUG_PYTHON = py_ast py_parser py_lexer py_main
PLUGINS = genequlin dimacs tptp
PLUGINS = genequlin dimacs tptp python
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
PYTHONCMO = $(addsuffix .cmo, $(PYTHONMODULES))
PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))
ifeq (@enable_hypothesis_selection@,yes)
PLUG_TRANSFORM += hypothesis_selection
PLUGINS += hypothesis_selection
......@@ -401,13 +408,13 @@ endif
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \
$(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
$(TPTPMODULES)
$(TPTPMODULES) $(PYTHONMODULES)
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGDIRS = parser printer transform tptp
PLUGDIRS = parser printer transform tptp python
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
......@@ -453,6 +460,14 @@ lib/plugins/tptp.cmo: $(TPTPCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/plugins/python.cmxs: $(PYTHONCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/python.cmo: $(PYTHONCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
......
module MapOcc
use import int.Int
use import map.Map
use import map.Occ
lemma occ_exchange :
forall m: map int 'a, l u i j: int, x y z: 'a.
l <= i < u ->
l <= j < u ->
Occ.occ z m[i <- x][j <- y] l u =
Occ.occ z m[i <- y][j <- x] l u
end
module Python
use import int.Int
use import ref.Ref
use array.Array
(* Python's lists are actually resizable arrays, but we simplify here *)
type list 'a = Array.array 'a
function ([]) (l: list 'a) (i: int) : 'a =
Array.get l i
function ([<-]) (l: list 'a) (i: int) (v: 'a) : list 'a =
Array.set l i v
function len (l: list 'a) : int =
Array.length l
let len (l: list 'a) : int
ensures { result = len(l) }
= Array.length l
let ([]) (l: list 'a) (i: int) : 'a
requires { 0 <= i < Array.length l }
ensures { result = l[i] }
= Array.([]) l i
let ([]<-) (l: list 'a) (i: int) (v: 'a) : unit
requires { 0 <= i < Array.length l }
writes { l }
ensures { l = Array.([<-]) (old l) i v }
= Array.([]<-) l i v
val range (l u: int) : list int
requires { l <= u }
ensures { Array.length result = u - l }
ensures { forall i. l <= i < u -> result[i] = i }
(* ad-hoc facts about exchange *)
use MapOcc
function occurrence (v: 'a) (l: list 'a) : int =
MapOcc.Occ.occ v l.Array.elts 0 l.Array.length
(* Python's division and modulus according are neither Euclidean division,
nor computer division, but something else defined in
https://docs.python.org/3/reference/expressions.html *)
use import int.Abs
use int.EuclideanDivision as E
function div (x y: int) : int =
let q = E.div x y in
if y >= 0 then q else if E.mod x y > 0 then q-1 else q
function mod (x y: int) : int =
let r = E.mod x y in
if y >= 0 then r else if r > 0 then r+y else r
lemma div_mod:
forall x y:int. y <> 0 -> x = y * div x y + mod x y
lemma mod_bounds:
forall x y:int. y <> 0 -> 0 <= abs (mod x y) < abs y
lemma mod_sign:
forall x y:int. y <> 0 -> if y < 0 then mod x y <= 0 else mod x y >= 0
let (//) (x y: int) : int
requires { y <> 0 }
ensures { result = div x y }
= div x y
let (%) (x y: int) : int
requires { y <> 0 }
ensures { result = mod x y }
= mod x y
(* random.randint *)
val randint (l u: int) : int
requires { l <= u }
ensures { l <= result <= u }
val input () : int
val int (n: int) : int
ensures { result = n }
exception Break
exception Return int
end
A plugin to verify programs written in a (microscopic) fragment of Python.
Limitations wrt Python:
- types are limited to integers and lists of integers
- a list is not resizable (i.e. it is a mere array)
- a function must return an integer or nothing
from random import randint
n = 42
a = [0] * n
a[0] = randint(0, 100)
i = 1
while i < n:
#@ invariant 1 <= i
#@ invariant forall i1, i2. 0 <= i1 <= i2 < i -> a[i1] <= a[i2]
#@ variant n-i
a[i] = a[i-1] + randint(0, 10)
i = i + 1
#@ assert len(a) == n
#@ assert forall i1, i2. 0 <= i1 <= i2 < len(a) -> a[i1] <= a[i2]
print(a)
v = int(input("quelle valeur cherchez-vous : "))
l = 0
u = n-1
r = -1
while l <= u:
#@ invariant 0 <= l and u < n
#@ invariant r == -1
#@ invariant forall i. 0 <= i < n -> a[i] == v -> l <= i <= u
#@ variant u-l
m = (l + u) // 2
if a[m] < v:
l = m+1
elif a[m] > v:
u = m-1
else:
r = m
break
if r == -1:
#@ assert forall i. 0 <= i < n -> a[i] != v
print("valeur absente")
else:
#@ assert a[r] == v
print("position", r)
from random import randint
m = randint(0, 100)
print("j'ai choisi un nombre entre 0 et 100")
print("vous devez le trouver")
tentatives = 0
while True:
x = int(input("votre choix : "))
tentatives = tentatives + 1
print(x)
if x < 0 or x > 100:
print("j'ai dit entre 0 et 100")
elif x < m:
print("trop petit")
elif x > m:
print("trop grand")
else:
print("bravo !")
print("en", tentatives, "tentatives")
break
print("la multiplication dite russe")
a = int(input("entrez a : "))
b = int(input("entrez b : "))
p = a
q = b
if q < 0:
p = -a
q = -b
#@ assert q >= 0
r = 0
while q > 0:
#@ invariant 0 <= q and r + p * q == a * b
#@ variant q
if q % 2 == 1:
r = r + p
p = p + p
q = q // 2
print("a * b =", r)
#@ assert r == a * b
from random import randint
n = 42
a = [0] * n
### On remplit le tableau "a"
for i in range(0, len(a)):
a[i] = randint(0, 100)
print(a)
### On prend une photo de "a"
photo = [0] * n
k = 0
while k < len(a):
#@ invariant 0 <= k <= len(a)
#@ invariant forall i. 0 <= i < k -> photo[i] == a[i]
#@ variant len(a) - k
photo[k] = a[k]
k = k + 1
#@ assert forall i. 0 <= i < len(a) -> photo[i] == a[i]
### Et maintenant on le trie
m = 1
while m < len(a):
#@ invariant 1 <= m <= len(a)
#@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j]
#@ invariant forall v. occurrence(v, a) == occurrence(v, photo)
#@ variant len(a) - m
x = a[m]
k = m
while k > 0 and a[k-1] > x:
#@ invariant 0 <= k <= m
#@ invariant forall i,j. 0 <= i <= j < k -> a[i] <= a[j]
#@ invariant forall i,j. 0 <= i < k < j <= m -> a[i] <= a[j]
#@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j]
#@ invariant forall j. k < j <= m -> x < a[j]
#@ invariant forall v. occurrence(v, a[k <- x]) == occurrence(v, photo)
#@ variant k
a[k] = a[k-1]
k = k - 1
a[k] = x
m = m + 1
#@ assert forall i,j. 0 <= i <= j < len(a) -> a[i] <= a[j]
#@ assert forall v. occurrence(v, a) == occurrence(v, photo)
print(a)
from random import randint
n = 42
a = [0] * n
### On remplit le tableau "a"
for i in range(0, len(a)):
a[i] = randint(0, 100)
print(a)
### Et maintenant on le trie
m = 1
while m < len(a):
#@ invariant 1 <= m <= len(a)
#@ invariant forall i,j. 0 <= i <= j < m -> a[i] <= a[j]
#@ variant len(a) - m
x = a[m]
k = m
while k > 0 and a[k-1] > x:
#@ invariant 0 <= k <= m
#@ invariant forall i,j. 0 <= i <= j < k -> a[i] <= a[j]
#@ invariant forall i,j. 0 <= i < k < j <= m -> a[i] <= a[j]
#@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j]
#@ invariant forall j. k < j <= m -> x < a[j]
#@ variant k
a[k] = a[k-1]
k = k - 1
a[k] = x
m = m + 1
#@ assert forall i,j. 0 <= i <= j < len(a) -> a[i] <= a[j]
print(a)
(********************************************************************)
(* *)
(* 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
type ident = Ptree.ident
type unop =
| Uneg (* -e *)
| Unot (* not e *)
type binop =
| Badd | Bsub | Bmul | Bdiv | Bmod (* + - * / % *)
| Beq | Bneq | Blt | Ble | Bgt | Bge (* == != < <= > >= *)
| Band | Bor (* && || *)
type expr = {
expr_desc: expr_desc;
expr_loc : Why3.Loc.position;
}
and expr_desc =
| Enone
| Ebool of bool
| Eint of string
| Estring of string
| Eident of ident
| Ebinop of binop * expr * expr
| Eunop of unop * expr
| Ecall of ident * expr list
| Elist of expr list (* [e1, e2, ..., en] *)
| Emake of expr * expr (* [e1] * e2 *)
| Eget of expr * expr (* e1[e2] *)
and stmt = {
stmt_desc: stmt_desc;
stmt_loc : Loc.position;
}
and stmt_desc =
| Sif of expr * block * block
| Sreturn of expr
| Sassign of ident * expr
| Swhile of expr * Ptree.loop_annotation * block
| Sfor of ident * expr * Ptree.invariant * block
| Seval of expr
| Sset of expr * expr * expr (* e1[e2] = e3 *)
| Sassert of Ptree.assertion_kind * Ptree.term
| Sbreak
| Slabel of ident
and block = stmt list
and def = ident * ident list * Ptree.spec * block
and file = def list * block
(********************************************************************)
(* *)
(* 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 Py_ast
open Py_parser
exception Lexing_error of string
let () = Why3.Exn_printer.register (fun fmt exn -> match exn with
| Lexing_error s -> Format.fprintf fmt "syntax error: %s" s
| _ -> raise exn)
let id_or_kwd =
let h = Hashtbl.create 32 in
List.iter (fun (s, tok) -> Hashtbl.add h s tok)
["def", DEF; "if", IF; "else", ELSE; "elif", ELIF;
"return", RETURN; "while", WHILE;
"for", FOR; "in", IN;
"and", AND; "or", OR; "not", NOT;
"True", TRUE; "False", FALSE; "None", NONE;
"from", FROM; "import", IMPORT; "break", BREAK;
(* annotations *)
"forall", FORALL; "exists", EXISTS; "then", THEN; "let", LET;
];
fun s -> try Hashtbl.find h s with Not_found -> IDENT s
let annotation =
let h = Hashtbl.create 32 in
List.iter (fun (s, tok) -> Hashtbl.add h s tok)
["invariant", INVARIANT; "variant", VARIANT;
"assert", ASSERT; "assume", ASSUME; "check", CHECK;
"requires", REQUIRES; "ensures", ENSURES;
"label", LABEL;
];
fun s -> try Hashtbl.find h s with Not_found ->
raise (Lexing_error ("no such annotation '" ^ s ^ "'"))
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let string_buffer = Buffer.create 1024
let stack = ref [0] (* indentation stack *)
let rec unindent n = match !stack with
| m :: _ when m = n -> []
| m :: st when m > n -> stack := st; END :: unindent n
| _ -> raise (Lexing_error "bad indentation")
let update_stack n =
match !stack with
| m :: _ when m < n ->
stack := n :: !stack;
[NEWLINE; BEGIN]
| _ ->
NEWLINE :: unindent n
}
let letter = ['a'-'z' 'A'-'Z']
let digit = ['0'-'9']
let ident = letter (letter | digit | '_')*
let integer = ['0'-'9']+
let space = ' ' | '\t'
let comment = "#" [^'@''\n'] [^'\n']*
rule next_tokens = parse
| '\n' { newline lexbuf; update_stack (indentation lexbuf) }
| (space | comment)+
{ next_tokens lexbuf }
| "#@" space* (ident as id)
{ [annotation id] }
| "#@" { raise (Lexing_error "expecting an annotation") }
| ident as id
{ [id_or_kwd id] }
| '+' { [PLUS] }
| '-' { [MINUS] }
| '*' { [TIMES] }
| "//" { [DIV] }
| '%' { [MOD] }
| '=' { [EQUAL] }
| "==" { [CMP Beq] }
| "!=" { [CMP Bneq] }
| "<" { [CMP Blt] }
| "<=" { [CMP Ble] }
| ">" { [CMP Bgt] }
| ">=" { [CMP Bge] }
| '(' { [LEFTPAR] }
| ')' { [RIGHTPAR] }
| '[' { [LEFTSQ] }
| ']' { [RIGHTSQ] }
| ',' { [COMMA] }
| ':' { [COLON] }
(* logic symbols *)
| "->" { [ARROW] }
| "<-" { [LARROW] }
| "<->" { [LRARROW] }
| "." { [DOT] }
| integer as s
{ [INTEGER s] }
| '"' { [STRING (string lexbuf)] }
| eof { [EOF] }
| _ as c { raise (Lexing_error ("illegal character: " ^ String.make 1 c)) }
(* count the indentation, i.e. the number of space characters from bol *)
and indentation = parse
| (space | comment)* '\n'
(* skip empty lines *)
{ newline lexbuf; indentation lexbuf }
| space* as s
{ String.length s }
and string = parse
| '"'
{ let s = Buffer.contents string_buffer in
Buffer.reset string_buffer;
s }
| "\\n"
{ Buffer.add_char string_buffer '\n';
string lexbuf }
| "\\\""
{ Buffer.add_char string_buffer '"';
string lexbuf }
| _ as c
{ Buffer.add_char string_buffer c;
string lexbuf }
| eof
{ raise (Lexing_error "unterminated string") }
{
let next_token =
let tokens = Queue.create () in
fun lb ->
if Queue.is_empty tokens then begin
let l = next_tokens lb in
List.iter (fun t -> Queue.add t tokens) l
end;
Queue.pop tokens
}
This diff is collapsed.
(********************************************************************)
(* *)
(* 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
let () = Why3.Exn_printer.register (fun fmt exn -> match exn with
| Error -> Format.fprintf fmt "syntax error"
| _ -> raise exn)
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_pat d s e = { pat_desc = d; pat_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 = [] }
let infix s = "infix " ^ s
let prefix s = "prefix " ^ s
let mixfix s = "mixfix " ^ s
let get_op s e = Qident (mk_id (mixfix "[]") s e)
let set_op s e = Qident (mk_id (mixfix "[<-]") s e)
let empty_spec = {
sp_pre = []; sp_post = []; sp_xpost = [];
sp_reads = []; sp_writes = []; sp_variant = [];
sp_checkrw = false; sp_diverge = false;
}
let spec_union s1 s2 = {
sp_pre = s1.sp_pre @ s2.sp_pre;
sp_post = s1.sp_post @ s2.sp_post;
sp_xpost = s1.sp_xpost @ s2.sp_xpost;
sp_reads = s1.sp_reads @ s2.sp_reads;
sp_writes = s1.sp_writes @ s2.sp_writes;
sp_variant = variant_union s1.sp_variant s2.sp_variant;
sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
sp_diverge = s1.sp_diverge || s2.sp_diverge;
}
%}
%token <string> INTEGER