python: more annotations

modules/python.mlw

@@ -30,4 +30,9 @@ module Python
     ensures  { S.length !result = u - l }
     ensures  { forall i. l <= i < u -> result[i] = i }
 
+  (* TODO: specify division and modulus according to
+     https://docs.python.org/3/reference/expressions.html *)
+  function div int int : int
+  function mod int int : int
+
 end

plugins/python/py_ast.ml

@@ -50,10 +50,10 @@ and stmt_desc =
   | Sassign of ident * expr
   | Sprint of expr
   | Swhile of expr * Ptree.loop_annotation * block
-  | Sfor of ident * expr * block
+  | Sfor of ident * expr *  Ptree.loop_annotation * block
   | Seval of expr
   | Sset of expr * expr * expr (* e1[e2] = e3 *)
-  | Sassert of Ptree.term
+  | Sassert of Ptree.assertion_kind * Ptree.term
 
 and block = stmt list
 

plugins/python/py_lexer.mll

@@ -16,6 +16,10 @@
 
   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)
@@ -67,12 +71,15 @@ rule next_tokens = parse
   | "##" space* "invariant" space+ { [INVARIANT] }
   | "##" space* "variant"   space+ { [VARIANT] }
   | "##" space* "assert"    space+ { [ASSERT] }
+  | "##" space* "assume"    space+ { [ASSUME] }
+  | "##" space* "check"     space+ { [CHECK] }
+  | "##"    { raise (Lexing_error "expecting an annotation") }
   | ident as id
             { [id_or_kwd id] }
   | '+'     { [PLUS] }
   | '-'     { [MINUS] }
   | '*'     { [TIMES] }
-  | '/'     { [DIV] }
+  | "//"    { [DIV] }
   | '%'     { [MOD] }
   | '='     { [EQUAL] }
   | "=="    { [CMP Beq] }

plugins/python/py_main.ml

@@ -80,8 +80,8 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
       | 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.Bdiv -> Eidapp (Qident (mk_id ~loc "div"), [e1; e2])
+      | Py_ast.Bmod -> Eidapp (Qident (mk_id ~loc "mod"), [e1; e2])
       | Py_ast.Beq  -> Eidapp (infix ~loc "=", [e1; e2])
       | Py_ast.Bneq -> Eidapp (infix ~loc "<>", [e1; e2])
       | Py_ast.Blt  -> Eidapp (infix ~loc "<", [e1; e2])
@@ -120,13 +120,13 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
       mk_expr ~loc (Einfix (x, mk_id ~loc "infix :=", e))
     else
       block env ~loc [s]
-  | Py_ast.Sfor (_id, _e, _s) ->
+  | Py_ast.Sfor (_id, _e, _a, _s) ->
     assert false (*TODO*)
   | Py_ast.Sset (e1, e2, e3) ->
     mk_expr ~loc (Eidapp (mixfix ~loc "[]<-",
                           [expr env e1; expr env e2; expr env e3]))
-  | Py_ast.Sassert t ->
-    mk_expr ~loc (Eassert (Aassert, deref env t))
+  | Py_ast.Sassert (k, t) ->
+    mk_expr ~loc (Eassert (k, deref env t))
 
 and block env ?(loc=Loc.dummy_position) = function
   | [] ->

plugins/python/py_parser.mly

@@ -14,6 +14,10 @@
   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_term d s e = { term_desc = d; term_loc = floc s e }
@@ -46,7 +50,7 @@
 %token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL COLON BEGIN END NEWLINE
 %token PLUS MINUS TIMES DIV MOD
 (* annotations *)
-%token INVARIANT VARIANT ASSERT
+%token INVARIANT VARIANT ASSUME ASSERT CHECK
 %token ARROW LRARROW FORALL EXISTS DOT THEN LET
 
 (* precedences *)
@@ -145,14 +149,18 @@ stmt_desc:
     { Sif (c, s, []) }
 | IF c = expr COLON s1 = suite ELSE COLON s2 = suite
     { 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, l) }
-| FOR x = ident IN e = expr COLON s = suite
-    { Sfor (x, e, s) }
+| WHILE e = expr COLON b=loop_body
+    { let a, l = b in Swhile (e, a, l) }
+| FOR x = ident IN e = expr COLON b=loop_body
+    { let a, l = b in Sfor (x, e, a, l) }
 ;
 
+loop_body:
+| s = simple_stmt NEWLINE
+  { empty_annotation, [s] }
+| NEWLINE BEGIN a=loop_annotation l=nonempty_list(stmt) END
+  { a, l }
+
 loop_annotation:
 | (* epsilon *)
     { empty_annotation }
@@ -178,12 +186,17 @@ simple_stmt_desc:
     { Sset (e1, e2, e3) }
 | PRINT e = expr
     { Sprint e }
-| ASSERT t = term
-    { Sassert t }
+| k=assertion_kind t = term
+    { Sassert (k, t) }
 | e = expr
     { Seval e }
 ;
 
+assertion_kind:
+| ASSERT  { Aassert }
+| ASSUME  { Aassume }
+| CHECK   { Acheck }
+
 ident:
   id = IDENT { mk_id id $startpos $endpos }
 ;

plugins/python/test.py

@@ -9,6 +9,8 @@ while b < 100:
   b = a+b
   ## assert b >= 1
   a = b-a
+
+# lists
 l = range(0, 10)
 ## assert forall i. 0 <= i < 10 -> l[i] >= 0
 l[2] = 42
@@ -21,6 +23,15 @@ while i < 10:
   l[i] = 0
   i = i+1
 
+# arithmetic
+# Python's division is *Euclidean* division
+q = -4 // 3
+## assert q == -2
+r = -4 % 3
+## assert r == 2
+## assert 4 // -3 == -2
+## assert 4 % -3 == -2
+
 # Local Variables:
 # compile-command: "make -C ../.. && why3 ide test.py"
 # End: