From 9b2ab3b80a0c816862b8b6c90e64050b8369a51e Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Wed, 17 Nov 2010 17:31:39 +0000
Subject: Forro: revised syntax (this version used in Boogie tutorial at SBMF
 2010)

---
 Source/Forro/Ast.fs        | 16 ++++++++++------
 Source/Forro/Forro.fsproj  |  1 +
 Source/Forro/Lexer.fsl     |  6 +++++-
 Source/Forro/Main.fs       |  9 +++++++--
 Source/Forro/Parser.fsy    | 33 ++++++++++++++++++++-------------
 Source/Forro/Printer.fs    | 29 +++++++++++++----------------
 Source/Forro/Resolver.fs   |  3 ---
 Source/Forro/Translator.fs | 22 ++++++++++++----------
 8 files changed, 68 insertions(+), 51 deletions(-)

(limited to 'Source/Forro')

diff --git a/Source/Forro/Ast.fs b/Source/Forro/Ast.fs
index fa4db8ec..6c7ba65c 100644
--- a/Source/Forro/Ast.fs
+++ b/Source/Forro/Ast.fs
@@ -1,10 +1,14 @@
-namespace Forro
+module Forro
 
 type Field = Head | Tail | Valid
 
 type Variable = Var of string
 
-type Operator = Eq | Neq | Plus | Minus | Times | Less | AtMost | And | Or
+let VarName v =
+    match v with Var(x) -> x
+
+type Operator = Eq | Neq | Plus | Minus | Times
+              | Less | AtMost | And | Or
 
 type Expression =
     | Constant of int
@@ -15,10 +19,7 @@ type Expression =
     | Select of Expression * Field
     | Old of Expression
 
-type StmtList  =
-    Block of Statement list
-
-and Statement =
+type Statement =
     | Assign of Variable * Expression
     | Update of Expression * Field * Expression
     | Alloc of Variable * Expression * Expression
@@ -27,6 +28,9 @@ and Statement =
     | CallStmt of Variable list * string * Expression list
     | Assert of Expression
 
+and StmtList  =
+    Block of Statement list
+
 type Procedure =
     Proc of string * Variable list * Variable list * Expression * Expression * StmtList
 
diff --git a/Source/Forro/Forro.fsproj b/Source/Forro/Forro.fsproj
index 531264b3..8f6fc223 100644
--- a/Source/Forro/Forro.fsproj
+++ b/Source/Forro/Forro.fsproj
@@ -71,6 +71,7 @@
     <Reference Include="FSharp.Core" />
     <Reference Include="System" />
     <Reference Include="System.Core" />
+    <Reference Include="System.Numerics" />
   </ItemGroup>
   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
        Other similar extension points exist, see Microsoft.Common.targets.
diff --git a/Source/Forro/Lexer.fsl b/Source/Forro/Lexer.fsl
index b1271536..4252af23 100644
--- a/Source/Forro/Lexer.fsl
+++ b/Source/Forro/Lexer.fsl
@@ -14,7 +14,8 @@ let newline = ('\n' | '\r' '\n')
 
 rule tokenize = parse
 | whitespace    { tokenize lexbuf }
-| newline       { tokenize lexbuf }
+| newline       { // lexbuf.EndPos <- lexbuf.EndPos.AsNewLinePos() ; 
+                  tokenize lexbuf }
 // operators
 | "=="          { EQ }
 | "!="          { NEQ }
@@ -31,7 +32,10 @@ rule tokenize = parse
 // misc
 | "("           { LPAREN }
 | ")"           { RPAREN }
+| "{"           { LCURLY }
+| "}"           { RCURLY }
 | ";"           { SEMI }
+| ","           { COMMA }
 | ":="          { ASSIGN }
 // keywords
 | "procedure"   { PROCEDURE }
diff --git a/Source/Forro/Main.fs b/Source/Forro/Main.fs
index 41c45220..3b0f550f 100644
--- a/Source/Forro/Main.fs
+++ b/Source/Forro/Main.fs
@@ -8,6 +8,7 @@ open Resolver
 open Lexer
 open Parser
 open BoogiePrinter
+
 open Translator
 
 let readAndProcess tracing (filename: string) =
@@ -15,9 +16,13 @@ let readAndProcess tracing (filename: string) =
         if tracing then printfn "Forró: version 1.0" else ()
         // lex
         let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
-        let lexbuff = LexBuffer<char>.FromTextReader(f)
+        let lexbuf = LexBuffer<char>.FromTextReader(f)
+        lexbuf.EndPos <- { pos_bol = 0;
+                           pos_fname=if filename = null then "stdin" else filename; 
+                           pos_cnum=0;
+                           pos_lnum=1 }
         // parse
-        let prog = Parser.start Lexer.tokenize lexbuff
+        let prog = Parser.start Lexer.tokenize lexbuf
         // print the given Forró program
         if tracing then
             printfn "---------- Given Forró program ----------"
diff --git a/Source/Forro/Parser.fsy b/Source/Forro/Parser.fsy
index 6fa41431..5c3f8284 100644
--- a/Source/Forro/Parser.fsy
+++ b/Source/Forro/Parser.fsy
@@ -29,7 +29,7 @@ let IdToField id =
 %token STAR
 %token EQ NEQ LESS ATMOST
 %token AND OR
-%token OLD LPAREN RPAREN SEMI ASSIGN
+%token OLD LPAREN RPAREN LCURLY RCURLY SEMI COMMA ASSIGN
 %token PROCEDURE REQUIRES ENSURES DO END
 %token NEW IF THEN ELSE WHILE INVARIANT CALL ASSERT
 %token EOF
@@ -49,17 +49,21 @@ Prog: Proc { [$1] }
     | Prog Proc { $2 :: $1  }
 
 Proc:
-    PROCEDURE Signature
-    REQUIRES Expression ENSURES Expression
+    PROCEDURE Signature ProcedureSpec
     DO StmtList END SEMI
-    { match $2 with outs,id,ins -> Proc(id, StringsToVariables ins, StringsToVariables outs, $4, $6, $8) }
+    { match $2, $3 with (outs,id,ins), (req,ens) -> Proc(id, StringsToVariables ins, StringsToVariables outs, req, ens, $5) }
+
+ProcedureSpec:
+      REQUIRES Expression ENSURES Expression { $2, $4 }
 
 Signature:
-      IdList                  { [], List.head $1, List.tail $1 }
-    | IdList ASSIGN IdList    { $1, List.head $3, List.tail $3 }
+      ID LPAREN IdList RPAREN                { [], $1, $3 }
+    | ID LPAREN RPAREN                       { [], $1, [] }
+    | IdList ASSIGN ID LPAREN IdList RPAREN  { $1, $3, $5 }
+    | IdList ASSIGN ID LPAREN RPAREN         { $1, $3, [] }
 
 IdList: ID      { [$1] }
-    | ID IdList { $1 :: $2 }
+    | ID COMMA IdList { $1 :: $3 }
 
 Expression:
       AtomicExpr { $1 }
@@ -85,13 +89,13 @@ AtomicExpr:
 FieldSelect:
     AtomicExpr DOT ID { $1, IdToField $3 }
 
-ExprList:  // possibly empty
-                          { [] }
-    | Expression ExprList { $1::$2 }
+ExprList:
+    | Expression                { [$1] }
+    | Expression COMMA ExprList { $1::$3 }
 
-VarList:   // nonempty
+VarList:
     | ID ASSIGN        { [Var($1)] }
-    | ID VarList { Var($1)::$2 }
+    | ID COMMA VarList { Var($1)::$3 }
 
 StmtList:
     StmtListX  { Block($1) }
@@ -102,11 +106,14 @@ StmtListX:
 
 Stmt:
       ID ASSIGN Expression SEMI                           { Assign(Var($1), $3) }
-    | ID ASSIGN NEW Expression Expression SEMI            { Alloc(Var($1), $4, $5) }
+    | ID ASSIGN NEW LPAREN Expression COMMA
+                    Expression RPAREN SEMI                { Alloc(Var($1), $5, $7) }
     | FieldSelect ASSIGN Expression SEMI                  { match $1 with e,f -> Update(e, f, $3) }
     | IF Expression THEN StmtList ELSE StmtList END SEMI  { IfStmt($2,$4,$6) }
     | WHILE Expression Invariants DO StmtList END SEMI    { WhileStmt($2,$3,$5) }
+    | CALL ID LPAREN RPAREN SEMI                          { CallStmt([],$2,[]) }
     | CALL ID LPAREN ExprList RPAREN SEMI                 { CallStmt([],$2,$4) }
+    | CALL VarList ID LPAREN RPAREN SEMI                  { CallStmt($2,$3,[]) }
     | CALL VarList ID LPAREN ExprList RPAREN SEMI         { CallStmt($2,$3,$5) }
     | ASSERT Expression SEMI                              { Assert($2) }
 
diff --git a/Source/Forro/Printer.fs b/Source/Forro/Printer.fs
index 65d515f8..2a9eac84 100644
--- a/Source/Forro/Printer.fs
+++ b/Source/Forro/Printer.fs
@@ -3,11 +3,6 @@
 open System
 open Forro
 
-let rec PrintVars xs =
-    match xs with
-    | [] -> ()
-    | Var(x)::rest -> printf " %s" x ; PrintVars rest
-
 let PrintField f =
     printf "."
     match f with
@@ -51,7 +46,7 @@ let rec PrintStmt indent s =
     match s with
     | Assign(Var(x), e) -> printf "%s" x ; printf " := " ; PrintExpr e true
     | Update(obj,f,rhs) -> PrintExpr obj false ; PrintField f ; printf " := " ; PrintExpr rhs true
-    | Alloc(Var(x),hd,tl) -> printf "%s" x ; printf " := new " ; PrintExpr hd false ; printf " " ; PrintExpr tl false
+    | Alloc(Var(x),hd,tl) -> printf "%s" x ; printf " := new (" ; PrintExpr hd false ; printf ", " ; PrintExpr tl false ; printf ")"
     | IfStmt(guard,thn,els) ->
         printf "if " ; PrintExpr guard true ; printfn " then"
         PrintStmtList ind thn
@@ -65,14 +60,15 @@ let rec PrintStmt indent s =
         PrintStmtList ind body
         Indent indent ; printf "end"
     | CallStmt(outs,id,ins) ->
-        printf "call"
-        if outs.IsEmpty then () else PrintVars outs ; printf " :="
+        printf "call "
+        if outs.IsEmpty then () else
+            ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" outs) ; printf " :="
         printf " %s" id
         printf "("
-        ignore (List.fold (fun sep e -> printf "%s" sep ; PrintExpr e false ; " ") "" ins)
-        printf ");"
+        ignore (List.fold (fun sep e -> printf "%s" sep ; PrintExpr e false ; ", ") "" ins)
+        printf ")"
     | Assert(e) ->
-        printf "assert " ; PrintExpr e ; printfn ";"
+        printf "assert " ; PrintExpr e true
     printfn ";"
 
 and PrintStmtList indent slist =
@@ -83,11 +79,12 @@ let PrintProc p =
     match p with
     | Proc(name, ins, outs, req, ens, body) ->
         // signature
-        printf "procedure"
-        if outs.IsEmpty then () else PrintVars outs ; printf " :="
-        printf " %s" name
-        PrintVars ins
-        printfn ""
+        printf "procedure "
+        if outs.IsEmpty then () else
+            ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" outs) ; printf " :="
+        printf " %s(" name
+        ignore (List.fold (fun sep v -> printf "%s%s" sep (VarName v) ; ", ") "" ins)
+        printfn ")"
         // specification
         printf "  requires "
         PrintExpr req true
diff --git a/Source/Forro/Resolver.fs b/Source/Forro/Resolver.fs
index 9844c24b..f227a5ca 100644
--- a/Source/Forro/Resolver.fs
+++ b/Source/Forro/Resolver.fs
@@ -8,9 +8,6 @@ exception ResolutionError of string
 let ResolutionError(s: string) =
     raise (ResolutionError s)
 
-let VarName v =
-    match v with Var(x) -> x
-
 type VarKind = InParam | OutParam | Local
 
 type Context(procedures: Collections.Generic.IDictionary<string,Procedure>) =
diff --git a/Source/Forro/Translator.fs b/Source/Forro/Translator.fs
index 77f3c864..4e7be216 100644
--- a/Source/Forro/Translator.fs
+++ b/Source/Forro/Translator.fs
@@ -20,9 +20,9 @@ let rec Flatten a =
 let Prelude =
     @"// Forro
 
-var $head: [int]int;
+var $head: [int]int;  // int -> int
 var $tail: [int]int;
-var $valid: [int]bool;
+var $valid: [int]bool;  // array int of bool
 
 const null: int;
 
@@ -91,8 +91,8 @@ let rec DefL expr =
     | Not(e) -> DefL e
     | Binary(op,a,b) ->
         match op with
-        | And -> BBinary(BOr, BNot(MkPred (TrExpr a)), Def b) :: (DefL a)
-        | Or -> BBinary(BOr, MkPred (TrExpr a), Def b) :: (DefL a)
+        | And -> BBinary(BOr, BNot(MkPred (TrExpr a)), Def b) :: (DefL a)   // (Def a) && ((TrExpr a) ==> (Def b))
+        | Or -> BBinary(BOr, MkPred (TrExpr a), Def b) :: (DefL a)  // (Def a) && (!(TrExpr a) ==> (Def b))
         | _ -> Append (DefL b) (DefL a)
     | Select(e,f) ->
         let def = DefL e
@@ -114,7 +114,7 @@ let FreshLocal locals =
     match locals with
     | LB(n, vars) ->
         let name = "nw$" + n.ToString()
-        (BIdentifier(name), LB(n+1, BVar(name, BInt)::vars))
+        (BIdentifier(name), name, LB(n+1, BVar(name, BInt)::vars))
 
 let rec TrStmt stmt locals =
     match stmt with
@@ -130,8 +130,9 @@ let rec TrStmt stmt locals =
                   AssumeGoodState ]
         (s, locals)
     | Alloc(v,hd,tl) ->
-        let nw, locals = FreshLocal locals
+        let nw, name, locals = FreshLocal locals
         let s = [ BAssert (Def hd) ; BAssert (Def tl) ;
+                  BHavoc [name] ;
                   BAssume(BNot(BSelect("$valid", nw))) ;
                   BAssume(BBinary(BEq, BSelect("$head", nw), TrExpr hd)) ;
                   BAssume(BBinary(BEq, BSelect("$tail", nw), TrExpr tl)) ;
@@ -151,13 +152,13 @@ let rec TrStmt stmt locals =
         let s, locals = TrStmtList body locals
         match s with
         | BBlock(slist) ->
-            ([BWhileStmt(MkPred (TrExpr guard), List.rev ii, BBlock(AssumeGoodState::slist))], locals)
+            ([BWhileStmt(MkPred (TrExpr guard), List.rev ii, BBlock(AssumeGoodState::slist)) ; AssumeGoodState], locals)
     | CallStmt(outs,id,ins) ->
         let check = List.map (fun e -> BAssert (Def e)) ins
         let ins = List.map (fun e -> TrExpr e) ins
         let outs = List.map (fun p -> VarName p) outs
-        let s = BCallStmt(outs, id + "#Proc", ins)::check
-        (AssumeGoodState :: List.rev s, locals)
+        let s = BCallStmt(outs, id + "#Proc", ins)
+        (Append check [s ; AssumeGoodState ], locals)
     | Assert(e) ->
         ([ BAssert (Def e) ; BAssert (MkPred (TrExpr e)) ], locals)
 
@@ -190,7 +191,8 @@ let TrProc proc vars =
         let b, locals = TrStmtList body (LB(0,locals))
         match b, locals with
         | BBlock(slist), LB(n, vars) ->
-            BProc(id + "#Proc", bIns, bOuts, pre, AllFields, post, List.rev vars, BBlock(AssumeGoodState::slist))
+            BProc(id + "#Proc", bIns, bOuts, pre, AllFields, post,
+               List.rev vars, BBlock(AssumeGoodState::slist))
 
 // --------------------
 
-- 
cgit v1.2.3