python: building lists

modules/python.mlw

@@ -3,35 +3,35 @@ module Python
 
   use import int.Int
   use import ref.Ref
-  use array.Array as A
+  use array.Array
 
   (* Python's lists are actually resizable arrays, but we simplify here *)
-  type list 'a = A.array 'a
+  type list 'a = Array.array 'a
 
   function ([]) (l: list 'a) (i: int) : 'a =
-    A.get l i
+    Array.get l i
 
   function len (l: list 'a) : int =
-    A.length l
+    Array.length l
 
   let len (l: list 'a) : int
     ensures { result = len(l) }
-  = A.length l
+  = Array.length l
 
   let ([]) (l: list 'a) (i: int) : 'a
-    requires { 0 <= i < A.length l }
+    requires { 0 <= i < Array.length l }
     ensures  { result = l[i] }
-  = A.([]) l i
+  = Array.([]) l i
 
   let ([]<-) (l: list 'a) (i: int) (v: 'a) : unit
-    requires { 0 <= i < A.length l }
+    requires { 0 <= i < Array.length l }
     writes   { l }
-    ensures  { l = A.([<-]) (old l) i v }
-  = A.([]<-) l i v
+    ensures  { l = Array.([<-]) (old l) i v }
+  = Array.([]<-) l i v
 
   val range (l u: int) : list int
     requires { l <= u }
-    ensures  { A.length result = u - l }
+    ensures  { Array.length result = u - l }
     ensures  { forall i. l <= i < u -> result[i] = i }
 
   (* Python's division and modulus according are neither Euclidean division,

plugins/python/py_ast.ml

@@ -36,7 +36,8 @@ and expr_desc =
   | Ebinop of binop * expr * expr
   | Eunop of unop * expr
   | Ecall of ident * expr list
-  | Elist of expr list
+  | Elist of expr list   (* [e1, e2, ..., en] *)
+  | Emake of expr * expr (* [e1] * e2 *)
   | Eget of expr * expr  (* e1[e2] *)
 
 and stmt = {
@@ -57,7 +58,7 @@ and stmt_desc =
 
 and block = stmt list
 
-and def = ident * ident list * block
+and def = ident * ident list * Ptree.spec * block
 
 and file = def list * block
 

plugins/python/py_lexer.mll

@@ -33,6 +33,16 @@
       ];
    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;
+      ];
+    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 <-
@@ -68,11 +78,8 @@ rule next_tokens = parse
   | '\n'    { newline lexbuf; update_stack (indentation lexbuf) }
   | (space | comment)+
             { next_tokens lexbuf }
-  | "#@" space* "invariant" space+ { [INVARIANT] }
-  | "#@" space* "variant"   space+ { [VARIANT] }
-  | "#@" space* "assert"    space+ { [ASSERT] }
-  | "#@" space* "assume"    space+ { [ASSUME] }
-  | "#@" space* "check"     space+ { [CHECK] }
+  | "#@" space* (ident as id)
+            { [annotation id] }
   | "#@"    { raise (Lexing_error "expecting an annotation") }
   | ident as id
             { [id_or_kwd id] }

plugins/python/py_main.ml

@@ -36,10 +36,15 @@ 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))]))
+let array_set ~loc a i v =
+  mk_expr ~loc (Eidapp (mixfix ~loc "[]<-", [a; i; v]))
 let constant ~loc s =
   mk_expr ~loc (Econst (Number.ConstInt (Number.int_const_dec s)))
 let len ~loc =
   Qident (mk_id ~loc "len")
+let array_make ~loc n v =
+  mk_expr ~loc (Eidapp (Qdot (Qident (mk_id ~loc "Array"), mk_id ~loc "make"),
+                        [n; v]))
 
 let empty_spec = {
   sp_pre     = [];
@@ -122,8 +127,21 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
     mk_expr ~loc (Eidapp (Qident (mk_id ~loc "not"), [expr env e]))
   | Py_ast.Ecall (id, el) ->
     mk_expr ~loc (Eidapp (Qident id, List.map (expr env) el))
-  | Py_ast.Elist _el ->
-    assert false (*TODO*)
+  | 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))
   | Py_ast.Eget (e1, e2) ->
     mk_expr ~loc (Eidapp (mixfix ~loc "[]", [expr env e1; expr env e2]))
 
@@ -145,8 +163,7 @@ let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
     else
       block env ~loc [s]
   | Py_ast.Sset (e1, e2, e3) ->
-    mk_expr ~loc (Eidapp (mixfix ~loc "[]<-",
-                          [expr env e1; expr env e2; expr env e3]))
+    array_set ~loc (expr env e1) (expr env e2) (expr env e3)
   | Py_ast.Sassert (k, t) ->
     mk_expr ~loc (Eassert (k, deref env t))
   | Py_ast.Swhile (e, ann, s) ->
@@ -192,7 +209,27 @@ and block env ?(loc=Loc.dummy_position) = function
     let sl = block env ~loc sl in
     mk_expr ~loc (Esequence (s, sl))
 
-let translate inc (_dl, s) =
+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 def inc (id, idl, sp, bl) =
+  let env = empty_env in
+  let env = List.fold_left add_var env idl in
+  let param id = id.id_loc, Some id, false, None in
+  let params = List.map param idl in
+  let fd = (params, None, block env bl, spec env sp) in
+  let d = Dfun (id, Gnone, fd) in
+  inc.new_pdecl id.id_loc d
+
+let translate inc (dl, s) =
+  List.iter (def inc) dl;
   let params = [Loc.dummy_position, None, false, Some (PTtuple [])] in
   let env = empty_env in
   let fd = (params, None, block env s, empty_spec) in

plugins/python/py_parser.mly

@@ -20,6 +20,7 @@
 
   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 }
@@ -39,6 +40,23 @@
 
   let get_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
@@ -50,7 +68,7 @@
 %token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL COLON BEGIN END NEWLINE
 %token PLUS MINUS TIMES DIV MOD
 (* annotations *)
-%token INVARIANT VARIANT ASSUME ASSERT CHECK
+%token INVARIANT VARIANT ASSUME ASSERT CHECK REQUIRES ENSURES
 %token ARROW LRARROW FORALL EXISTS DOT THEN LET
 
 (* precedences *)
@@ -80,10 +98,25 @@ file:
 
 def:
 | DEF f = ident LEFTPAR x = separated_list(COMMA, ident) RIGHTPAR
-  COLON s = suite
-    { f, x, s }
+  COLON NEWLINE BEGIN s=spec l=nonempty_list(stmt) END
+    { f, x, s, l }
 ;
 
+spec:
+| (* epsilon *)     { empty_spec }
+| single_spec spec  { spec_union $1 $2 }
+
+single_spec:
+| REQUIRES t=term NEWLINE
+    { { empty_spec with sp_pre = [t] } }
+| ENSURES e=ensures NEWLINE
+    { { empty_spec with sp_post = [floc $startpos(e) $endpos(e), e] } }
+
+ensures:
+| term
+    { let id = mk_id "result" $startpos $endpos in
+      [mk_pat (Pvar id) $startpos $endpos, $1] }
+
 expr:
 | d = expr_desc
    { mk_expr (floc $startpos $endpos) d }
@@ -110,6 +143,10 @@ expr_desc:
     { Eunop (Unot, e1) }
 | e1 = expr o = binop e2 = expr
     { Ebinop (o, e1, e2) }
+| e1 = expr TIMES e2 = expr
+    { match e1.expr_desc with
+      | Elist [e1] -> Emake (e1, e2)
+      | _ -> Ebinop (Bmul, e1, e2) }
 | f = ident LEFTPAR e = separated_list(COMMA, expr) RIGHTPAR
     { Ecall (f, e) }
 | LEFTSQ l = separated_list(COMMA, expr) RIGHTSQ
@@ -121,7 +158,6 @@ expr_desc:
 %inline binop:
 | PLUS  { Badd }
 | MINUS { Bsub }
-| TIMES { Bmul }
 | DIV   { Bdiv }
 | MOD   { Bmod }
 | c=CMP { c    }

plugins/python/test.py

 
+# def swap(a, i, j):
+#   #@ requires 0 <= i < len(a) and 0 <= j < len(a)
+#   t = a[i]
+#   a[i] = a[j]
+#   a[j] = t
+
 a = 0
 b = 1
 while b < 100:
@@ -24,12 +30,17 @@ while i < 10:
   i = i+1
 
 sum = 0
-for x in l:
+for x in [42]*3:
   #@ invariant sum >= 0
   print(x)
   #@ assert x >= 0
   sum = sum+x
 
+foo = [1,2,3]
+#@ assert len(foo)==3
+#@ assert foo[1]==2
+
+
 # Python's division is neither Euclidean division, nor computer division
 #@ assert  4 //  3 ==  1 and  4 %  3 ==  1
 #@ assert -4 //  3 == -2 and -4 %  3 ==  2