Forro: revised syntax (this version used in Boogie tutorial at SBMF 2010)

8 files changed, 68 insertions, 51 deletions

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))

 

 // --------------------