programs: added a for loop, with Ocaml semantics and builtin WP rule

bench/programs/good/for.mlw

+
+(* for loop with invariant *)
+let test () =
+  let x = ref 0 in
+  for i = 1 to 10 do
+    invariant { !x = i-1 }
+    x := !x + 1
+  done;
+  assert { !x = 10 }
+
+(* we don't even enter *)
+let test2 () =
+  let x = ref 0 in
+  for i = 2 to 1 do
+    x := 1
+  done;
+  assert { !x = 0 }
+
+exception E
+
+(* the body raises an exception (for sure)
+   subtle: the invariant is required *)
+let test3 () =
+  { }
+  for i = 1 to 10 do invariant { i >= 2 -> false }
+    raise E
+  done
+  { false } | E -> { true }
+
+(* the body may raise an exception *)
+let test4 x =
+  { }
+  try
+    for i = 0 to 10 do
+      invariant { x < 0 or x >= i }
+      if i = x then raise E
+    done;
+    False
+  with E ->
+    True
+  end
+  { result=True <-> 0 <= x <= 10 }
+
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../../.. bench/programs/good/for"
+End: 
+*)

share/emacs/why.el

@@ -29,7 +29,7 @@
    '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
    '("{\\([^}]*\\)}" . font-lock-type-face)
    `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
-   `(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face)
+   `(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face)
    ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
    )
   "Minimal highlighting for Why mode")

src/programs/pgm_env.ml

@@ -56,6 +56,9 @@ type env = {
   ls_orb  : lsymbol;
   ls_notb : lsymbol;
   ls_unit : lsymbol;
+  ls_gt   : lsymbol;
+  ls_le   : lsymbol;
+  ls_add  : lsymbol;
 }
 
 
@@ -149,6 +152,9 @@ let empty_env uc = {
   ls_orb   = find_ls uc ["orb"];
   ls_notb  = find_ls uc ["notb"];
   ls_unit  = find_ls uc ["Tuple0"];
+  ls_gt    = find_ls uc ["infix >"];
+  ls_le    = find_ls uc ["infix <="];
+  ls_add   = find_ls uc ["infix +"];
 }    
 
 let make_arrow_type env tyl ty =

src/programs/pgm_env.mli

@@ -56,6 +56,9 @@ type env = private {
   ls_orb  : lsymbol;
   ls_notb : lsymbol;
   ls_unit : lsymbol;
+  ls_gt   : lsymbol;
+  ls_le   : lsymbol;
+  ls_add  : lsymbol;
 }
 
 val empty_env : theory_uc -> env

src/programs/pgm_lexer.mll

@@ -68,6 +68,7 @@
 	"reads", READS;
 	"rec", REC;
 	"then", THEN;
+	"to", TO;
 	"try", TRY;
 	"type", TYPE;
 	"variant", VARIANT;

src/programs/pgm_parser.mly

@@ -120,7 +120,7 @@
 %token EXCEPTION FOR
 %token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT OF PARAMETER
 %token RAISE RAISES READS REC 
-%token THEN TRY TYPE VARIANT WHILE WITH WRITES
+%token THEN TO TRY TYPE VARIANT WHILE WITH WRITES
 
 /* symbols */
 
@@ -317,6 +317,8 @@ expr:
 		     mk_expr (Eif ($2, $5,
 				   mk_expr (Eraise (exit_exn (), None)))))),
 	   [exit_exn (), None, mk_expr Eskip])) }
+| FOR lident EQUAL expr TO expr DO loop_invariant expr DONE
+   { mk_expr (Efor ($2, $4, $6, $8, $9)) }
 | ABSURD
    { mk_expr Eabsurd }
 | expr COLON pure_type

src/programs/pgm_ptree.ml

@@ -88,6 +88,7 @@ and expr_desc =
   | Eabsurd
   | Eraise of ident * expr option
   | Etry of expr * (ident * ident option * expr) list
+  | Efor of ident * expr * expr * lexpr option * expr
   (* annotations *)
   | Eassert of assertion_kind * lexpr
   | Elabel of ident * expr

src/programs/pgm_ttree.ml

@@ -90,6 +90,7 @@ and dexpr_desc =
   | DEabsurd 
   | DEraise of Term.lsymbol * dexpr option
   | DEtry of dexpr * (Term.lsymbol * string option * dexpr) list
+  | DEfor of ident * dexpr * dexpr * Denv.dfmla option * dexpr
 
   | DEassert of assertion_kind * Denv.dfmla
   | DElabel of string * dexpr
@@ -148,6 +149,8 @@ and iexpr_desc =
   | IEabsurd
   | IEraise of Term.lsymbol * iexpr option
   | IEtry of iexpr * (Term.lsymbol * Term.vsymbol option * iexpr) list
+  | IEfor of 
+      Term.vsymbol * Term.vsymbol * Term.vsymbol * Term.fmla option * iexpr
 
   | IEassert of assertion_kind * Term.fmla
   | IElabel of label * iexpr
@@ -183,6 +186,8 @@ and expr_desc =
   | Eabsurd
   | Eraise of Term.lsymbol * expr option
   | Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
+  | Efor of 
+      Term.vsymbol * Term.vsymbol * Term.vsymbol * Term.fmla option * expr
 
   | Eassert of assertion_kind * Term.fmla
   | Elabel of label * expr

src/programs/pgm_typing.ml

@@ -61,6 +61,7 @@ let id_result = "result"
 let dty_app (ts, tyl) = assert (ts.ts_def = None); Tyapp (ts, tyl)
 
 let dty_bool gl = dty_app (gl.ts_bool, [])
+let dty_int _gl = dty_app (Ty.ts_int, [])
 let dty_unit gl = dty_app (gl.ts_unit, [])
 let dty_label gl = dty_app (gl.ts_label, [])
 
@@ -361,13 +362,13 @@ and dexpr_desc env loc = function
   | Pgm_ptree.Eloop (a, e1) ->
       let e1 = dexpr env e1 in
       expected_type e1 (dty_unit env.env);
-      DEloop (dloop_annotation env a, e1), (dty_unit env.env)
+      DEloop (dloop_annotation env a, e1), dty_unit env.env
   | Pgm_ptree.Elazy (op, e1, e2) ->
       let e1 = dexpr env e1 in
       expected_type e1 (dty_bool env.env);
       let e2 = dexpr env e2 in
       expected_type e2 (dty_bool env.env);
-      DElazy (op, e1, e2), (dty_bool env.env)
+      DElazy (op, e1, e2), dty_bool env.env
   | Pgm_ptree.Ematch (e1, bl) ->
       let e1 = dexpr env e1 in
       let ty1 = e1.dexpr_type in
@@ -383,7 +384,7 @@ and dexpr_desc env loc = function
       let bl = List.map branch bl in
       DEmatch (e1, bl), ty
   | Pgm_ptree.Eskip ->
-      DElogic env.env.ls_unit, (dty_unit env.env)
+      DElogic env.env.ls_unit, dty_unit env.env
   | Pgm_ptree.Eabsurd ->
       DEabsurd, create_type_var loc
   | Pgm_ptree.Eraise (id, e) ->
@@ -426,6 +427,16 @@ and dexpr_desc env loc = function
 	(ls, x, h)
       in
       DEtry (e1, List.map handler hl), e1.dexpr_type
+  | Pgm_ptree.Efor (x, e1, e2, inv, e3) ->
+      let e1 = dexpr env e1 in
+      expected_type e1 (dty_int env.env);
+      let e2 = dexpr env e2 in
+      expected_type e2 (dty_int env.env);
+      let env = add_local env x.id (DTpure (dty_int env.env)) in
+      let inv = option_map (dfmla env.denv) inv in
+      let e3 = dexpr env e3 in
+      expected_type e3 (dty_unit env.env);
+      DEfor (x, e1, e2, inv, e3), dty_unit env.env
 
   | Pgm_ptree.Eassert (k, le) ->
       DEassert (k, dfmla env.denv le), dty_unit env.env
@@ -701,6 +712,18 @@ and iexpr_desc gl env loc ty = function
 	(ls, x, iexpr gl env h)
       in
       IEtry (iexpr gl env e, List.map handler hl)
+  | DEfor (x, e1, e2, inv, e3) ->
+      let e1 = iexpr gl env e1 in
+      let e2 = iexpr gl env e2 in
+      let vx = create_vsymbol (id_user x.id x.id_loc) e1.iexpr_type in
+      let env = Mstr.add x.id vx env in
+      let inv = option_map (Denv.fmla env) inv in
+      let e3 = iexpr gl env e3 in
+      let v1 = create_vsymbol (id_user "for_start" loc) e1.iexpr_type in
+      let v2 = create_vsymbol (id_user "for_end" loc)   e2.iexpr_type in
+      IElet (v1, e1, mk_iexpr loc ty (
+      IElet (v2, e2, mk_iexpr loc ty (
+      IEfor (vx, v1, v2, inv, e3)))))
 
   | DEassert (k, f) ->
       let f = Denv.fmla env f in
@@ -857,7 +880,7 @@ let rec is_pure_expr e =
   | Elet (_, e1, e2) -> is_pure_expr e1 && is_pure_expr e2
   | Elabel (_, e1) -> is_pure_expr e1
   | Eany c -> E.no_side_effect c.c_effect
-  | Eassert _ | Etry _ | Eraise _ | Ematch _ 
+  | Eassert _ | Etry _ | Efor _ | Eraise _ | Ematch _ 
   | Eloop _ | Eletrec _ | Efun _ 
   | Eglobal _ | Eabsurd -> false (* TODO: improve *)
 
@@ -1042,6 +1065,14 @@ and expr_desc gl env loc ty = function
 	List.fold_left (fun e (_,_,h) -> E.union e h.expr_effect) ef hl 
       in
       Etry (e1, hl), tpure ty, ef
+  | IEfor (x, v1, v2, inv, e3) ->
+      let env = add_local x (tpure v1.vs_ty) env in
+      let e3 = expr gl env e3 in
+      let ef = match inv with
+	| Some f -> fmla_effect gl e3.expr_effect f 
+	| None -> e3.expr_effect
+      in
+      Efor (x, v1, v2, inv, e3), type_v_unit gl, ef
 
   | IEassert (k, f) ->
       let ef = fmla_effect gl E.empty f in
@@ -1111,7 +1142,11 @@ and letrec gl env dl = (* : env * recfun list *)
   let m, dl = fixpoint m0 in
   make_env m, dl
 
-(* freshness analysis *)
+(* freshness analysis
+
+   checks that values of type 'a ref are only freshly allocated
+   term:bool indicates if we are in terminal position in the expression
+   (to allow functions to return fresh references) *)
 
 let rec fresh_expr gl ~term locals e = match e.expr_desc with
   | Elocal vs when is_reference_type gl vs.vs_ty 
@@ -1144,6 +1179,8 @@ let rec fresh_expr gl ~term locals e = match e.expr_desc with
   | Etry (e1, hl) ->
       fresh_expr gl ~term:false locals e1;
       List.iter (fun (_, _, e2) -> fresh_expr gl ~term locals e2) hl
+  | Efor (_, _, _, _, e3) ->
+      fresh_expr gl ~term:false locals e3
 
   | Elabel (_, e) ->
       fresh_expr gl ~term locals e

src/programs/pgm_wp.ml

@@ -312,6 +312,7 @@ and wp_desc env e q = match e.expr_desc with
 		 (quantify env e.expr_effect (wp_implies i we)))
 	in
 	w
+  (* optimization for the particular case let _ = y in e *)
   | Ematch (_, [{pat_node = Pwild}, e]) ->
       wp_expr env e (filter_post e.expr_effect q)
   | Ematch (x, bl) ->
@@ -353,7 +354,36 @@ and wp_desc env e q = match e.expr_desc with
       let q1 = saturate_post e1.expr_effect (fst q) q in
       let q1 = filter_post e1.expr_effect (make_post q1) in
       wp_expr env e1 q1
-
+  | Efor (x, v1, v2, inv, e1) ->
+      (* wp(for x = v1 to v2 do inv { I(x) } e1, Q, R) =
+             v1 > v2  -> Q
+         and v1 <= v2 ->     I(v1)
+                         and forall S. forall i. v1 <= i <= v2 -> 
+                                                 I(i) -> wp(e1, I(i+1), R)
+	                               and I(v2+1) -> Q                    *)
+      let (res, q1), _ = q in
+      let v1_gt_v2 = f_app env.ls_gt [t_var v1; t_var v2] in
+      let v1_le_v2 = f_app env.ls_le [t_var v1; t_var v2] in
+      let inv = match inv with Some inv -> inv | None -> f_true in
+      let wp1 = 
+	let xp1 = t_app env.ls_add [t_var x; t_int_const "1"] ty_int in
+	let post = f_subst (subst1 x xp1) inv in
+	let q1 = saturate_post e1.expr_effect (res, post) q in
+	wp_expr env e1 q1
+      in
+      let f = wp_and ~sym:true
+	(f_subst (subst1 x (t_var v1)) inv)
+	(quantify env e.expr_effect
+	   (wp_and ~sym:true
+	      (wp_forall env x
+	         (wp_implies (wp_and (f_app env.ls_le [t_var v1; t_var x])
+			             (f_app env.ls_le [t_var x;  t_var v2])) 
+                 (wp_implies inv wp1))) 
+	      (let sv2 = t_app env.ls_add [t_var v2; t_int_const "1"] ty_int in
+	       wp_implies (f_subst (subst1 x sv2) inv) q1)))
+      in
+      wp_and ~sym:true (wp_implies v1_gt_v2 q1) (wp_implies v1_le_v2 f)
+      
   | Eassert (Pgm_ptree.Aassert, f) ->
       let (_, q), _ = q in
       wp_and f q

tests/test-pgm-jcf.mlw

-{
 
-type purse = ref int
+(* for loop with invariant *)
+let test () =
+  let x = ref 0 in
+  for i = 1 to 10 do
+    invariant { !x = i-1 }
+    x := !x + 1
+  done;
+  assert { !x = 10 }
 
-}
+(* we don't even enter *)
+let test2 () =
+  let x = ref 0 in
+  for i = 2 to 1 do
+    x := 1
+  done;
+  assert { !x = 0 }
 
-parameter new_purse : unit -> purse
+exception E
 
-let purse_init (balance: purse) (amount: int): unit =
-{ amount >= 0 } 
-    balance := amount
-{ !balance = amount}
+(* the body raises an exception (for sure)
+   subtle: the invariant is required *)
+let test3 () =
+  { }
+  for i = 1 to 10 do invariant { i >= 2 -> false }
+    raise E
+  done
+  { false } | E -> { true }
 
-let test () : int =
-{ true }
-  let p1 = new_purse() in
-  purse_init p1 150;
-  let p2 = new_purse() in
-  !p2
-{ result = 150 }
+(* the body may raise an exception *)
+let test4 x =
+  { }
+  try
+    for i = 0 to 10 do
+      invariant { x < 0 or x >= i }
+      if i = x then raise E
+    done;
+    False
+  with E ->
+    True
+  end
+  { result=True <-> 0 <= x <= 10 }
+  
 
 (*
 Local Variables: