Add fresh, assert and assume to WISL, tweak while

wisl/examples/wpst/llen_wpst.wisl

@@ -0,0 +1,33 @@
+function llen(x) {
+    if (x = null) {
+        n := 0
+    } else {
+        t := [x+1];
+        n := llen(t);
+        n := n + 1
+    };
+    return n
+}
+
+function build_list(size) {
+  i := 0;
+  l := null;
+  while (i < size) {
+    n := new(2);
+    [n] := size - i;
+    [n + 1] := l;
+    l := n;
+    i := i + 1
+  };
+  return l
+}
+
+function main() {
+  fresh x;
+  assume (x >= 2);
+  assume (x <= 3);
+  l := build_list(x);
+  size := llen(l);
+  assert (size = 2);
+  return null
+}

wisl/lib/ParserAndCompiler/WLexer.mll

@@ -31,6 +31,7 @@ rule read =
   | "if"     { IF (curr lexbuf) }
   | "else"   { ELSE (curr lexbuf) }
   | "skip"   { SKIP (curr lexbuf) }
+  | "fresh" { FRESH (curr lexbuf) }
   | "new"    { NEW (curr lexbuf) }
   | "free"   { DELETE (curr lexbuf) }
   | "dispose"{ DELETE (curr lexbuf) }
@@ -43,6 +44,7 @@ rule read =
   | "nounfold" { NOUNFOLD (curr lexbuf) }
   | "apply"  { APPLY (curr lexbuf) }
   | "assert" { ASSERT (curr lexbuf) }
+  | "assume" { ASSUME (curr lexbuf) }
   | "with" { WITH (curr lexbuf) }
   | "variant" { VARIANT (curr lexbuf) }
   | "statement" { STATEMENT (curr lexbuf) }

wisl/lib/ParserAndCompiler/WParser.mly

@@ -1,9 +1,9 @@
 %token EOF
 
 (* key words *)
-%token <CodeLoc.t> TRUE FALSE NULL WHILE IF ELSE SKIP NEW DELETE
+%token <CodeLoc.t> TRUE FALSE NULL WHILE IF ELSE SKIP FRESH NEW DELETE
 %token <CodeLoc.t> FUNCTION RETURN PREDICATE LEMMA
-%token <CodeLoc.t> INVARIANT FOLD UNFOLD NOUNFOLD APPLY ASSERT EXIST FORALL
+%token <CodeLoc.t> INVARIANT FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME EXIST FORALL
 %token <CodeLoc.t> STATEMENT WITH VARIANT PROOF
 
 (* punctuation *)
@@ -197,6 +197,11 @@ statement:
       let lend = WExpr.get_loc e in
       let loc = CodeLoc.merge lstart lend in
       WStmt.make bare_stmt loc }
+  | lstart = FRESH; lx = IDENTIFIER
+    { let (lend, x) = lx in
+      let bare_stmt = WStmt.Fresh x in
+      let loc = CodeLoc.merge lstart lend in
+      WStmt.make bare_stmt loc }
   | lx = IDENTIFIER; ASSIGN; NEW; LBRACE; ln = INTEGER; lend = RBRACE
     { let (lstart, x) = lx in
     let (_, i) = ln in
@@ -249,6 +254,20 @@ statement:
     { let bare_stmt = WStmt.Logic lc in
       let loc = CodeLoc.merge lstart lend in
       WStmt.make bare_stmt loc }
+  | lstart = ASSERT; e = expression;
+    {
+      let bare_stmt = WStmt.Assert e in
+      let lend = WExpr.get_loc e in
+      let loc = CodeLoc.merge lstart lend in
+      WStmt.make bare_stmt loc
+    }
+  | lstart = ASSUME; e = expression;
+    {
+      let bare_stmt = WStmt.Assume e in
+      let lend = WExpr.get_loc e in
+      let loc = CodeLoc.merge lstart lend in
+      WStmt.make bare_stmt loc
+    }
 
 
 expr_list:

wisl/lib/ParserAndCompiler/wisl2Gil.ml

@@ -648,19 +648,22 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl =
       let comp_body, new_functions = compile_list sl in
       let comp_body, bodlab = get_or_create_lab comp_body lbody_lab in
       let endlab = gen_str end_lab in
-      let annot_while =
+      let annot =
         WAnnot.make ~origin_id:sid_while ~origin_loc:(CodeLoc.to_location sloc)
           ()
       in
-      let loopcmd = Cmd.GuardedGoto (guard, bodlab, endlab) in
+      let annot_hidden = WAnnot.{ annot with is_hidden = true } in
       let headlabopt = Some looplab in
-      let loopcmd_lab = (annot_while, headlabopt, loopcmd) in
+      let headcmd = Cmd.Skip in
+      let headcmd_lab = (annot_hidden, headlabopt, headcmd) in
+      let loopcmd = Cmd.GuardedGoto (guard, bodlab, endlab) in
+      let loopcmd_lab = (annot, None, loopcmd) in
       let backcmd = Cmd.Goto looplab in
-      let backcmd_lab = (annot_while, None, backcmd) in
+      let backcmd_lab = (annot_hidden, None, backcmd) in
       let endcmd = Cmd.Skip in
-      let endcmd_lab = (annot_while, Some endlab, endcmd) in
+      let endcmd_lab = (annot_hidden, Some endlab, endcmd) in
       let comp_rest, new_functions_2 = compile_list rest in
-      ( cmdle @ [ loopcmd_lab ] @ comp_body
+      ( [ headcmd_lab ] @ cmdle @ [ loopcmd_lab ] @ comp_body
         @ [ backcmd_lab; endcmd_lab ]
         @ comp_rest,
         new_functions @ new_functions_2 )
@@ -681,6 +684,14 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl =
       in
       let comp_rest, new_functions = compile_list rest in
       (cmdle @ [ (annot, None, cmd) ] @ comp_rest, new_functions)
+  (* Fresh s-var *)
+  | { snode = Fresh v; sid; sloc } :: rest ->
+      let cmd = Cmd.Logic (LCmd.FreshSVar v) in
+      let annot =
+        WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc) ()
+      in
+      let comp_rest, new_functions = compile_list rest in
+      ((annot, None, cmd) :: comp_rest, new_functions)
   (* Object Deletion *)
   | { snode = Dispose e; sid; sloc } :: rest ->
       let cmdle, comp_e = compile_expr e in
@@ -863,6 +874,28 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl =
       in
       let comp_rest, new_functions = compile_list rest in
       (cmds_with_annot @ comp_rest, new_functions)
+  | { snode = Assert e; sid; sloc } :: rest ->
+      let annot =
+        WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc) ()
+      in
+      let cmdle, comp_e = compile_expr e in
+      let cmd =
+        let formula = Formula.Eq (comp_e, Expr.bool true) in
+        Cmd.Logic (LCmd.Assert formula)
+      in
+      let comp_rest, new_functions = compile_list rest in
+      (cmdle @ [ (annot, None, cmd) ] @ comp_rest, new_functions)
+  | { snode = Assume e; sid; sloc } :: rest ->
+      let annot =
+        WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc) ()
+      in
+      let cmdle, comp_e = compile_expr e in
+      let cmd =
+        let formula = Formula.Eq (comp_e, Expr.bool true) in
+        Cmd.Logic (LCmd.Assume formula)
+      in
+      let comp_rest, new_functions = compile_list rest in
+      (cmdle @ [ (annot, None, cmd) ] @ comp_rest, new_functions)
 
 let compile_spec
     ?(fname = "main")

wisl/lib/syntax/WStmt.ml

@@ -3,6 +3,7 @@ open VisitorUtils
 type tt =
   | Skip
   | VarAssign of string * WExpr.t
+  | Fresh of string  (** fresh x *)
   | New of string * int
   | Dispose of WExpr.t
   | Lookup of string * WExpr.t (* x := [e] *)
@@ -12,6 +13,8 @@ type tt =
   | While of WExpr.t * t list
   | If of WExpr.t * t list * t list
   | Logic of WLCmd.t
+  | Assert of WExpr.t  (** non-SL assertion *)
+  | Assume of WExpr.t  (** non-SL assumption *)
 
 and t = { sid : int; sloc : CodeLoc.t; snode : tt }
 
@@ -30,6 +33,7 @@ and pp fmt stmt =
   match get stmt with
   | Skip -> Format.fprintf fmt "@[%s@]" "skip"
   | VarAssign (v, e) -> Format.fprintf fmt "@[%s := %a@]" v WExpr.pp e
+  | Fresh v -> Format.fprintf fmt "@[fresh %s@]" v
   | New (v, r) -> Format.fprintf fmt "@[%s := new(%i)@]" v r
   | Dispose e -> Format.fprintf fmt "@[free@ %a@]" WExpr.pp e
   | Lookup (v, e) -> Format.fprintf fmt "@[%s := [%a]@]" v WExpr.pp e
@@ -47,6 +51,8 @@ and pp fmt stmt =
         "@[@[<v 2>if(%a) {@\n%a@]@\n@[<v 2>} else {@\n%a@]@\n}@]" WExpr.pp e
         pp_list s1 pp_list s2
   | Logic lcmd -> Format.fprintf fmt "@[[[ %a ]]@]" WLCmd.pp lcmd
+  | Assert e -> Format.fprintf fmt "@[assert %a@]" WExpr.pp e
+  | Assume e -> Format.fprintf fmt "@[assume %a@]" WExpr.pp e
 
 and pp_head fmt stmt =
   match get stmt with
@@ -87,14 +93,15 @@ let rec get_by_id id stmt =
   let lcmd_getter = WLCmd.get_by_id id in
   let aux s =
     match get s with
-    | Dispose e | Lookup (_, e) | VarAssign (_, e) -> expr_getter e
+    | Dispose e | Lookup (_, e) | VarAssign (_, e) | Assert e | Assume e ->
+        expr_getter e
     | Update (e1, e2) -> expr_getter e1 |>> (expr_getter, e2)
     | FunCall (_, _, el, _) -> expr_list_visitor el
     | While (e, sl) -> expr_getter e |>> (list_visitor, sl)
     | If (e, sl1, sl2) ->
         expr_getter e |>> (list_visitor, sl1) |>> (list_visitor, sl2)
     | Logic lcmd -> lcmd_getter lcmd
-    | New _ | Skip -> `None
+    | Fresh _ | New _ | Skip -> `None
   in
   let self_or_none = if get_id stmt = id then `WStmt stmt else `None in
   self_or_none |>> (aux, stmt)

wisl/lib/syntax/WStmt.mli

@@ -1,6 +1,7 @@
 type tt =
   | Skip
   | VarAssign of string * WExpr.t  (** x := e *)
+  | Fresh of string  (** fresh x *)
   | New of string * int  (** x := new(k) *)
   | Dispose of WExpr.t  (** free(e) *)
   | Lookup of string * WExpr.t  (** x := [e] *)
@@ -10,6 +11,8 @@ type tt =
   | While of WExpr.t * t list  (** while (e) \{ s \} *)
   | If of WExpr.t * t list * t list  (** if (e) \{ s \} else \{ s \} *)
   | Logic of WLCmd.t  (** logic command *)
+  | Assert of WExpr.t  (** non-SL assertion *)
+  | Assume of WExpr.t  (** non-SL assumption *)
 
 and t = { sid : int; sloc : CodeLoc.t; snode : tt }