From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Source/Forro/Ast.fs | 76 ++++---- Source/Forro/BoogieAst.fs | 80 ++++---- Source/Forro/BoogiePrinter.fs | 224 +++++++++++----------- Source/Forro/Forro.fsproj | 164 ++++++++-------- Source/Forro/Lexer.fsl | 120 ++++++------ Source/Forro/Main.fs | 114 +++++------ Source/Forro/Parser.fsy | 244 ++++++++++++------------ Source/Forro/Printer.fs | 214 ++++++++++----------- Source/Forro/Resolver.fs | 246 ++++++++++++------------ Source/Forro/Translator.fs | 434 +++++++++++++++++++++--------------------- 10 files changed, 958 insertions(+), 958 deletions(-) (limited to 'Source/Forro') diff --git a/Source/Forro/Ast.fs b/Source/Forro/Ast.fs index 6c7ba65c..779beefb 100644 --- a/Source/Forro/Ast.fs +++ b/Source/Forro/Ast.fs @@ -1,38 +1,38 @@ -module Forro - -type Field = Head | Tail | Valid - -type Variable = Var of string - -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 - | Null - | Identifier of Variable - | Not of Expression - | Binary of Operator * Expression * Expression - | Select of Expression * Field - | Old of Expression - -type Statement = - | Assign of Variable * Expression - | Update of Expression * Field * Expression - | Alloc of Variable * Expression * Expression - | IfStmt of Expression * StmtList * StmtList - | WhileStmt of Expression * Expression list * StmtList - | 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 - -type Program = - Prog of Procedure list +module Forro + +type Field = Head | Tail | Valid + +type Variable = Var of string + +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 + | Null + | Identifier of Variable + | Not of Expression + | Binary of Operator * Expression * Expression + | Select of Expression * Field + | Old of Expression + +type Statement = + | Assign of Variable * Expression + | Update of Expression * Field * Expression + | Alloc of Variable * Expression * Expression + | IfStmt of Expression * StmtList * StmtList + | WhileStmt of Expression * Expression list * StmtList + | 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 + +type Program = + Prog of Procedure list diff --git a/Source/Forro/BoogieAst.fs b/Source/Forro/BoogieAst.fs index 964f6667..7c1819da 100644 --- a/Source/Forro/BoogieAst.fs +++ b/Source/Forro/BoogieAst.fs @@ -1,40 +1,40 @@ -namespace BoogieAst - -type BType = BInt | BBool - -type BOperator = BEq | BNeq | BPlus | BMinus | BTimes | BLess | BAtMost | BAnd | BOr - -type BExpression = - | BConstant of int - | BFalse - | BTrue - | BNull - | BIdentifier of string - | BNot of BExpression - | BBinary of BOperator * BExpression * BExpression - | BSelect of string * BExpression - | BToPred of BExpression // BToPred(e) == (e != 0) - | BToTerm of BExpression // BToTerm(e) == (if e then 1 else 0) - | BOld of BExpression - | BFunc of string * BExpression list - -type BStmtList = - BBlock of Statement list - -and Statement = - | BAssign of string * BExpression - | BUpdate of string * BExpression * BExpression - | BHavoc of string list - | BAssert of BExpression - | BAssume of BExpression - | BIfStmt of BExpression * BStmtList * BStmtList - | BWhileStmt of BExpression * BExpression list * BStmtList - | BCallStmt of string list * string * BExpression list - -type BVarDecl = BVar of string * BType - -type BProcedure = - BProc of string * BVarDecl list * BVarDecl list * BExpression * string list * BExpression * BVarDecl list * BStmtList - -type BProgram = - BProg of string * BProcedure list +namespace BoogieAst + +type BType = BInt | BBool + +type BOperator = BEq | BNeq | BPlus | BMinus | BTimes | BLess | BAtMost | BAnd | BOr + +type BExpression = + | BConstant of int + | BFalse + | BTrue + | BNull + | BIdentifier of string + | BNot of BExpression + | BBinary of BOperator * BExpression * BExpression + | BSelect of string * BExpression + | BToPred of BExpression // BToPred(e) == (e != 0) + | BToTerm of BExpression // BToTerm(e) == (if e then 1 else 0) + | BOld of BExpression + | BFunc of string * BExpression list + +type BStmtList = + BBlock of Statement list + +and Statement = + | BAssign of string * BExpression + | BUpdate of string * BExpression * BExpression + | BHavoc of string list + | BAssert of BExpression + | BAssume of BExpression + | BIfStmt of BExpression * BStmtList * BStmtList + | BWhileStmt of BExpression * BExpression list * BStmtList + | BCallStmt of string list * string * BExpression list + +type BVarDecl = BVar of string * BType + +type BProcedure = + BProc of string * BVarDecl list * BVarDecl list * BExpression * string list * BExpression * BVarDecl list * BStmtList + +type BProgram = + BProg of string * BProcedure list diff --git a/Source/Forro/BoogiePrinter.fs b/Source/Forro/BoogiePrinter.fs index 8f2b37ee..e9497ab5 100644 --- a/Source/Forro/BoogiePrinter.fs +++ b/Source/Forro/BoogiePrinter.fs @@ -1,112 +1,112 @@ -module BoogiePrinter - -open ForroPrinter // to get Indent -open BoogieAst - -let PrintWithSep Pr sep list = - ignore (List.fold (fun sp e -> printf "%s" sp ; Pr e ; sep) "" list) - -let TypeName t = - match t with - | BInt -> "int" - | BBool -> "bool" - -let PrVarType v = - match v with - | BVar(name,t) -> - printf "%s: %s" name (TypeName t) - -let PrintOp op = - printf " " - match op with - | BEq -> printf "==" - | BNeq -> printf "!=" - | BPlus -> printf "+" - | BMinus -> printf "-" - | BTimes -> printf "*" - | BLess -> printf "<" - | BAtMost -> printf "<=" - | BAnd -> printf "&&" - | BOr -> printf "||" - printf " " - -let rec PrintExpr e = - match e with - | BConstant(x) -> printf "%d" x - | BFalse -> printf "false" - | BTrue -> printf "true" - | BNull -> printf "null" - | BIdentifier(id) -> printf "%s" id - | BNot(e) -> printf "!(" ; PrintExpr e ; printf ")" - | BBinary(op,e0,e1) -> printf "(" ; PrintExpr e0 ; PrintOp op ; PrintExpr e1 ; printf ")" - | BSelect(var,e) -> printf "%s[" var ; PrintExpr e ; printf "]" - | BToPred(e) -> printf "(" ; PrintExpr e ; printf " != 0)" - | BToTerm(e) -> printf "(if " ; PrintExpr e ; printf " then 1 else 0)" - | BOld(e) -> printf "old(" ; PrintExpr e ; printf ")" - | BFunc(id,args) -> printf "%s(" id ; PrintWithSep PrintExpr ", " args ; printf ")" - -let rec PrintStmt indent stmt = - Indent indent - let ind = indent + 2 - match stmt with - | BAssign(id,e) -> printf "%s := " id ; PrintExpr e ; printfn ";" - | BUpdate(id,obj,rhs) -> printf "%s[" id ; PrintExpr obj ; printf "] := " ; PrintExpr rhs ; printfn ";" - | BHavoc(ids) -> printf "havoc " ; PrintWithSep (printf "%s") ", " ids ; printfn ";" - | BAssert(e) -> printf "assert " ; PrintExpr e ; printfn ";" - | BAssume(e) -> printf "assume " ; PrintExpr e ; printfn ";" - | BIfStmt(e,thn,els) -> - printf "if (" ; PrintExpr e ; printfn ") {" - PrintStmtList ind thn - Indent indent - printfn "} else {" - PrintStmtList ind els - Indent indent - printfn "}" - | BWhileStmt(e, invs, body) -> - printf "while (" ; PrintExpr e ; printfn ")" - List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv ; printfn ";") invs - Indent indent - printfn "{" - PrintStmtList ind body - Indent indent - printfn "}" - | BCallStmt(outs, id, ins) -> - printf "call " - if outs.IsEmpty then () else PrintWithSep (fun p -> printf "%s" p) ", " outs ; printf " := " - printf "%s(" id - PrintWithSep PrintExpr ", " ins - printfn ");" - -and PrintStmtList indent stmts = - match stmts with - | BBlock(slist) -> List.iter (fun s -> PrintStmt indent s) slist - -let BPrintProc proc = - match proc with - | BProc(name, ins, outs, req, frame, ens, locals, body) -> - printfn "" - printf "procedure %s(" name - PrintWithSep PrVarType ", " ins - printf ") returns (" - PrintWithSep PrVarType ", " outs - printfn ")" - printf " requires " - PrintExpr req - printfn ";" - printf " modifies " - PrintWithSep (printf "%s") ", " frame - printfn ";" - printf " ensures " - PrintExpr ens - printfn ";" - printfn "{" - List.iter (fun local -> printf " var " ; PrVarType local ; printfn ";") locals - if locals.IsEmpty then () else printfn "" - PrintStmtList 2 body - printfn "}" - -let BPrint (prog: BProgram) = - match prog with - | BProg(prelude, procs) -> - printfn "%s" prelude - List.iter BPrintProc procs +module BoogiePrinter + +open ForroPrinter // to get Indent +open BoogieAst + +let PrintWithSep Pr sep list = + ignore (List.fold (fun sp e -> printf "%s" sp ; Pr e ; sep) "" list) + +let TypeName t = + match t with + | BInt -> "int" + | BBool -> "bool" + +let PrVarType v = + match v with + | BVar(name,t) -> + printf "%s: %s" name (TypeName t) + +let PrintOp op = + printf " " + match op with + | BEq -> printf "==" + | BNeq -> printf "!=" + | BPlus -> printf "+" + | BMinus -> printf "-" + | BTimes -> printf "*" + | BLess -> printf "<" + | BAtMost -> printf "<=" + | BAnd -> printf "&&" + | BOr -> printf "||" + printf " " + +let rec PrintExpr e = + match e with + | BConstant(x) -> printf "%d" x + | BFalse -> printf "false" + | BTrue -> printf "true" + | BNull -> printf "null" + | BIdentifier(id) -> printf "%s" id + | BNot(e) -> printf "!(" ; PrintExpr e ; printf ")" + | BBinary(op,e0,e1) -> printf "(" ; PrintExpr e0 ; PrintOp op ; PrintExpr e1 ; printf ")" + | BSelect(var,e) -> printf "%s[" var ; PrintExpr e ; printf "]" + | BToPred(e) -> printf "(" ; PrintExpr e ; printf " != 0)" + | BToTerm(e) -> printf "(if " ; PrintExpr e ; printf " then 1 else 0)" + | BOld(e) -> printf "old(" ; PrintExpr e ; printf ")" + | BFunc(id,args) -> printf "%s(" id ; PrintWithSep PrintExpr ", " args ; printf ")" + +let rec PrintStmt indent stmt = + Indent indent + let ind = indent + 2 + match stmt with + | BAssign(id,e) -> printf "%s := " id ; PrintExpr e ; printfn ";" + | BUpdate(id,obj,rhs) -> printf "%s[" id ; PrintExpr obj ; printf "] := " ; PrintExpr rhs ; printfn ";" + | BHavoc(ids) -> printf "havoc " ; PrintWithSep (printf "%s") ", " ids ; printfn ";" + | BAssert(e) -> printf "assert " ; PrintExpr e ; printfn ";" + | BAssume(e) -> printf "assume " ; PrintExpr e ; printfn ";" + | BIfStmt(e,thn,els) -> + printf "if (" ; PrintExpr e ; printfn ") {" + PrintStmtList ind thn + Indent indent + printfn "} else {" + PrintStmtList ind els + Indent indent + printfn "}" + | BWhileStmt(e, invs, body) -> + printf "while (" ; PrintExpr e ; printfn ")" + List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv ; printfn ";") invs + Indent indent + printfn "{" + PrintStmtList ind body + Indent indent + printfn "}" + | BCallStmt(outs, id, ins) -> + printf "call " + if outs.IsEmpty then () else PrintWithSep (fun p -> printf "%s" p) ", " outs ; printf " := " + printf "%s(" id + PrintWithSep PrintExpr ", " ins + printfn ");" + +and PrintStmtList indent stmts = + match stmts with + | BBlock(slist) -> List.iter (fun s -> PrintStmt indent s) slist + +let BPrintProc proc = + match proc with + | BProc(name, ins, outs, req, frame, ens, locals, body) -> + printfn "" + printf "procedure %s(" name + PrintWithSep PrVarType ", " ins + printf ") returns (" + PrintWithSep PrVarType ", " outs + printfn ")" + printf " requires " + PrintExpr req + printfn ";" + printf " modifies " + PrintWithSep (printf "%s") ", " frame + printfn ";" + printf " ensures " + PrintExpr ens + printfn ";" + printfn "{" + List.iter (fun local -> printf " var " ; PrVarType local ; printfn ";") locals + if locals.IsEmpty then () else printfn "" + PrintStmtList 2 body + printfn "}" + +let BPrint (prog: BProgram) = + match prog with + | BProg(prelude, procs) -> + printfn "%s" prelude + List.iter BPrintProc procs diff --git a/Source/Forro/Forro.fsproj b/Source/Forro/Forro.fsproj index 8f6fc223..161d79db 100644 --- a/Source/Forro/Forro.fsproj +++ b/Source/Forro/Forro.fsproj @@ -1,83 +1,83 @@ - - - - Debug - x86 - 8.0.30703 - 2.0 - {c75e47a0-e88d-4035-9ebf-f6647af92b79} - Exe - Language - Forro - v4.0 - Client - Language - - - true - full - false - false - bin\Debug\ - DEBUG;TRACE - 3 - x86 - bin\Debug\Language.XML - - - pdbonly - true - true - bin\Release\ - TRACE - 3 - x86 - bin\Release\Language.XML - - - - - $(IntermediateOutputPath) - $(IntermediateOutputPath) - - - - - false - Parser.fs - - - false - Lexer.fs - - - --module Parser - - - --unicode - - - - - - - - - - - C:\Program Files\FSharpPowerPack-1.9.9.9\bin\FSharp.PowerPack.dll - - - - - - - - + + + + Debug + x86 + 8.0.30703 + 2.0 + {c75e47a0-e88d-4035-9ebf-f6647af92b79} + Exe + Language + Forro + v4.0 + Client + Language + + + true + full + false + false + bin\Debug\ + DEBUG;TRACE + 3 + x86 + bin\Debug\Language.XML + + + pdbonly + true + true + bin\Release\ + TRACE + 3 + x86 + bin\Release\Language.XML + + + + + $(IntermediateOutputPath) + $(IntermediateOutputPath) + + + + + false + Parser.fs + + + false + Lexer.fs + + + --module Parser + + + --unicode + + + + + + + + + + + C:\Program Files\FSharpPowerPack-1.9.9.9\bin\FSharp.PowerPack.dll + + + + + + + + \ No newline at end of file diff --git a/Source/Forro/Lexer.fsl b/Source/Forro/Lexer.fsl index 4252af23..5f69df7c 100644 --- a/Source/Forro/Lexer.fsl +++ b/Source/Forro/Lexer.fsl @@ -1,60 +1,60 @@ -{ -module Lexer -open System -open Parser -open Microsoft.FSharp.Text.Lexing -} - -// These are some regular expression definitions -let digit = ['0'-'9'] -let nondigit = [ 'a'-'z' 'A'-'Z' '_' ] -let idchar = (nondigit | digit) -let whitespace = [' ' '\t' ] -let newline = ('\n' | '\r' '\n') - -rule tokenize = parse -| whitespace { tokenize lexbuf } -| newline { // lexbuf.EndPos <- lexbuf.EndPos.AsNewLinePos() ; - tokenize lexbuf } -// operators -| "==" { EQ } -| "!=" { NEQ } -| "+" { PLUS } -| "-" { MINUS } -| "*" { STAR } -| "<" { LESS } -| "<=" { ATMOST } -| "and" { AND } -| "or" { OR } -| "not" { NOT } -| "old" { OLD } -| "." { DOT } -// misc -| "(" { LPAREN } -| ")" { RPAREN } -| "{" { LCURLY } -| "}" { RCURLY } -| ";" { SEMI } -| "," { COMMA } -| ":=" { ASSIGN } -// keywords -| "procedure" { PROCEDURE } -| "requires" { REQUIRES } -| "ensures" { ENSURES } -| "do" { DO } -| "end" { END } -| "new" { NEW } -| "if" { IF } -| "then" { THEN } -| "else" { ELSE } -| "while" { WHILE } -| "invariant" { INVARIANT } -| "call" { CALL } -| "assert" { ASSERT } -// literals -| ['-']?digit+ { INT32 (Int32.Parse(LexBuffer.LexemeString lexbuf)) } -| "null" { NULL } -// identifiers -| idchar+ { ID (LexBuffer.LexemeString lexbuf) } -// EOF -| eof { EOF } +{ +module Lexer +open System +open Parser +open Microsoft.FSharp.Text.Lexing +} + +// These are some regular expression definitions +let digit = ['0'-'9'] +let nondigit = [ 'a'-'z' 'A'-'Z' '_' ] +let idchar = (nondigit | digit) +let whitespace = [' ' '\t' ] +let newline = ('\n' | '\r' '\n') + +rule tokenize = parse +| whitespace { tokenize lexbuf } +| newline { // lexbuf.EndPos <- lexbuf.EndPos.AsNewLinePos() ; + tokenize lexbuf } +// operators +| "==" { EQ } +| "!=" { NEQ } +| "+" { PLUS } +| "-" { MINUS } +| "*" { STAR } +| "<" { LESS } +| "<=" { ATMOST } +| "and" { AND } +| "or" { OR } +| "not" { NOT } +| "old" { OLD } +| "." { DOT } +// misc +| "(" { LPAREN } +| ")" { RPAREN } +| "{" { LCURLY } +| "}" { RCURLY } +| ";" { SEMI } +| "," { COMMA } +| ":=" { ASSIGN } +// keywords +| "procedure" { PROCEDURE } +| "requires" { REQUIRES } +| "ensures" { ENSURES } +| "do" { DO } +| "end" { END } +| "new" { NEW } +| "if" { IF } +| "then" { THEN } +| "else" { ELSE } +| "while" { WHILE } +| "invariant" { INVARIANT } +| "call" { CALL } +| "assert" { ASSERT } +// literals +| ['-']?digit+ { INT32 (Int32.Parse(LexBuffer.LexemeString lexbuf)) } +| "null" { NULL } +// identifiers +| idchar+ { ID (LexBuffer.LexemeString lexbuf) } +// EOF +| eof { EOF } diff --git a/Source/Forro/Main.fs b/Source/Forro/Main.fs index 3b0f550f..07d1a12e 100644 --- a/Source/Forro/Main.fs +++ b/Source/Forro/Main.fs @@ -1,57 +1,57 @@ -open System -open Microsoft.FSharp.Text.Lexing - -open System.IO - -open ForroPrinter -open Resolver -open Lexer -open Parser -open BoogiePrinter - -open Translator - -let readAndProcess tracing (filename: string) = - try - if tracing then printfn "Forró: version 1.0" else () - // lex - let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader - let lexbuf = LexBuffer.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 lexbuf - // print the given Forró program - if tracing then - printfn "---------- Given Forró program ----------" - Print prog - else () - // make sure the program is legal - let rprog = Resolve prog - // translate into Boogie - let bprog = Translate rprog - // print the Boogie program - if tracing then printfn "---------- Resulting Boogie program ----------" else () - BPrint bprog - // that's it - if tracing then printfn "----------" ; printfn "Done" else () - - with - | ResolutionError(msg) -> - printfn "Resolution error: %s" msg - | ex -> - printfn "Unhandled Exception: %s" ex.Message - -let rec start n (args: string []) tracing filename = - if n < args.Length then - let arg = args.[n] - if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else () - let filename = if arg.StartsWith "/" then filename else arg - start (n+1) args (tracing || arg = "/trace") filename - else - readAndProcess tracing filename - -let args = Environment.GetCommandLineArgs() -start 1 args false null +open System +open Microsoft.FSharp.Text.Lexing + +open System.IO + +open ForroPrinter +open Resolver +open Lexer +open Parser +open BoogiePrinter + +open Translator + +let readAndProcess tracing (filename: string) = + try + if tracing then printfn "Forró: version 1.0" else () + // lex + let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader + let lexbuf = LexBuffer.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 lexbuf + // print the given Forró program + if tracing then + printfn "---------- Given Forró program ----------" + Print prog + else () + // make sure the program is legal + let rprog = Resolve prog + // translate into Boogie + let bprog = Translate rprog + // print the Boogie program + if tracing then printfn "---------- Resulting Boogie program ----------" else () + BPrint bprog + // that's it + if tracing then printfn "----------" ; printfn "Done" else () + + with + | ResolutionError(msg) -> + printfn "Resolution error: %s" msg + | ex -> + printfn "Unhandled Exception: %s" ex.Message + +let rec start n (args: string []) tracing filename = + if n < args.Length then + let arg = args.[n] + if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else () + let filename = if arg.StartsWith "/" then filename else arg + start (n+1) args (tracing || arg = "/trace") filename + else + readAndProcess tracing filename + +let args = Environment.GetCommandLineArgs() +start 1 args false null diff --git a/Source/Forro/Parser.fsy b/Source/Forro/Parser.fsy index 5dbb8a4c..af64d267 100644 --- a/Source/Forro/Parser.fsy +++ b/Source/Forro/Parser.fsy @@ -1,122 +1,122 @@ -%{ - -open Forro - -exception ParseError of string - -let StringsToVariables ss = [ for s in ss -> Var(s) ] - -let IdToField id = - match id with - | "head" -> Field.Head - | "tail" -> Field.Tail - | "valid" -> Field.Valid - | _ -> raise (ParseError ("illegal field selector: '" + id + "' (legal selectors are 'head', 'tail', and 'valid')")) - -%} - -// The start token becomes a parser function in the compiled code: -%start start - -// These are the terminal tokens of the grammar along with the types of -// the data carried by each token: -%token ID -%token INT32 -%token NULL -%token DOT -%token NOT -%token STAR -%token PLUS MINUS -%token EQ NEQ LESS ATMOST -%token AND OR -%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 - -// This is the type of the data produced by a successful reduction of the 'start' -// symbol: -%type < Forro.Program > start - -%% - -// These are the rules of the grammar along with the F# code of the -// actions executed as rules are reduced. In this case the actions -// produce data using F# data construction terms. -start: Prog EOF { Prog(List.rev($1)) } - -Prog: Proc { [$1] } - | Prog Proc { $2 :: $1 } - -Proc: - PROCEDURE Signature ProcedureSpec - DO StmtList END SEMI - { 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: - 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 COMMA IdList { $1 :: $3 } - -Expression: - AtomicExpr { $1 } - | NOT Expression { Not($2) } - | Expression PLUS Expression { Binary(Operator.Plus, $1, $3) } - | Expression MINUS Expression { Binary(Operator.Minus, $1, $3) } - | Expression STAR Expression { Binary(Operator.Times, $1, $3) } - | Expression EQ Expression { Binary(Operator.Eq, $1, $3) } - | Expression NEQ Expression { Binary(Operator.Neq, $1, $3) } - | Expression LESS Expression { Binary(Operator.Less, $1, $3) } - | Expression ATMOST Expression { Binary(Operator.AtMost, $1, $3) } - | Expression AND Expression { Binary(Operator.And, $1, $3) } - | Expression OR Expression { Binary(Operator.Or, $1, $3) } - -AtomicExpr: - INT32 { Constant($1) } - | NULL { Null } - | ID { Identifier(Var($1)) } - | OLD LPAREN Expression RPAREN { Old($3) } - | LPAREN Expression RPAREN { $2 } - | FieldSelect { match $1 with e,f -> Select(e,f) } - -FieldSelect: - AtomicExpr DOT ID { $1, IdToField $3 } - -ExprList: - | Expression { [$1] } - | Expression COMMA ExprList { $1::$3 } - -VarList: - | ID ASSIGN { [Var($1)] } - | ID COMMA VarList { Var($1)::$3 } - -StmtList: - StmtListX { Block($1) } - -StmtListX: - { [] } - | Stmt StmtListX { $1::$2 } - -Stmt: - ID ASSIGN Expression SEMI { Assign(Var($1), $3) } - | 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) } - -Invariants: - { [] } - | INVARIANT Expression Invariants { $2::$3 } +%{ + +open Forro + +exception ParseError of string + +let StringsToVariables ss = [ for s in ss -> Var(s) ] + +let IdToField id = + match id with + | "head" -> Field.Head + | "tail" -> Field.Tail + | "valid" -> Field.Valid + | _ -> raise (ParseError ("illegal field selector: '" + id + "' (legal selectors are 'head', 'tail', and 'valid')")) + +%} + +// The start token becomes a parser function in the compiled code: +%start start + +// These are the terminal tokens of the grammar along with the types of +// the data carried by each token: +%token ID +%token INT32 +%token NULL +%token DOT +%token NOT +%token STAR +%token PLUS MINUS +%token EQ NEQ LESS ATMOST +%token AND OR +%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 + +// This is the type of the data produced by a successful reduction of the 'start' +// symbol: +%type < Forro.Program > start + +%% + +// These are the rules of the grammar along with the F# code of the +// actions executed as rules are reduced. In this case the actions +// produce data using F# data construction terms. +start: Prog EOF { Prog(List.rev($1)) } + +Prog: Proc { [$1] } + | Prog Proc { $2 :: $1 } + +Proc: + PROCEDURE Signature ProcedureSpec + DO StmtList END SEMI + { 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: + 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 COMMA IdList { $1 :: $3 } + +Expression: + AtomicExpr { $1 } + | NOT Expression { Not($2) } + | Expression PLUS Expression { Binary(Operator.Plus, $1, $3) } + | Expression MINUS Expression { Binary(Operator.Minus, $1, $3) } + | Expression STAR Expression { Binary(Operator.Times, $1, $3) } + | Expression EQ Expression { Binary(Operator.Eq, $1, $3) } + | Expression NEQ Expression { Binary(Operator.Neq, $1, $3) } + | Expression LESS Expression { Binary(Operator.Less, $1, $3) } + | Expression ATMOST Expression { Binary(Operator.AtMost, $1, $3) } + | Expression AND Expression { Binary(Operator.And, $1, $3) } + | Expression OR Expression { Binary(Operator.Or, $1, $3) } + +AtomicExpr: + INT32 { Constant($1) } + | NULL { Null } + | ID { Identifier(Var($1)) } + | OLD LPAREN Expression RPAREN { Old($3) } + | LPAREN Expression RPAREN { $2 } + | FieldSelect { match $1 with e,f -> Select(e,f) } + +FieldSelect: + AtomicExpr DOT ID { $1, IdToField $3 } + +ExprList: + | Expression { [$1] } + | Expression COMMA ExprList { $1::$3 } + +VarList: + | ID ASSIGN { [Var($1)] } + | ID COMMA VarList { Var($1)::$3 } + +StmtList: + StmtListX { Block($1) } + +StmtListX: + { [] } + | Stmt StmtListX { $1::$2 } + +Stmt: + ID ASSIGN Expression SEMI { Assign(Var($1), $3) } + | 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) } + +Invariants: + { [] } + | INVARIANT Expression Invariants { $2::$3 } diff --git a/Source/Forro/Printer.fs b/Source/Forro/Printer.fs index 2a9eac84..d168e094 100644 --- a/Source/Forro/Printer.fs +++ b/Source/Forro/Printer.fs @@ -1,107 +1,107 @@ -module ForroPrinter - -open System -open Forro - -let PrintField f = - printf "." - match f with - | Head -> printf "head" - | Tail -> printf "tail" - | Valid -> printf "valid" - -let PrintOp op = - printf " " - match op with - | Eq -> printf "==" - | Neq -> printf "!=" - | Plus -> printf "+" - | Minus -> printf "-" - | Times -> printf "*" - | Less -> printf "<" - | AtMost -> printf "<=" - | And -> printf "and" - | Or -> printf "or" - printf " " - -let rec PrintExpr e outermost = - match e with - | Constant(x) -> printf "%i" x - | Null -> printf "null" - | Identifier(Var(x)) -> printf "%s" x - | Not(e) -> printf "not(" ; PrintExpr e true ; printf ")" - | Binary(op,a,b) -> - if outermost then () else printf "(" - PrintExpr a false ; PrintOp op ; PrintExpr b false - if outermost then () else printf ")" - | Select(e,f) -> PrintExpr e false ; PrintField f - | Old(e) -> printf "old(" ; PrintExpr e true ; printf ")" - -let rec Indent n = - if n = 0 then () else printf " " ; Indent (n-1) - -let rec PrintStmt indent s = - Indent indent - let ind = indent + 2 - 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 ; printf ")" - | IfStmt(guard,thn,els) -> - printf "if " ; PrintExpr guard true ; printfn " then" - PrintStmtList ind thn - Indent indent ; printfn "else" - PrintStmtList ind els - Indent indent ; printf "end" - | WhileStmt(guard,invs,body) -> - printf "while " ; PrintExpr guard true ; printfn "" - List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv true ; printfn "") invs - Indent indent ; printfn "do" - PrintStmtList ind body - Indent indent ; printf "end" - | CallStmt(outs,id,ins) -> - 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 ")" - | Assert(e) -> - printf "assert " ; PrintExpr e true - printfn ";" - -and PrintStmtList indent slist = - match slist with - | Block(ss) -> List.iter (fun s -> PrintStmt indent s) ss - -let PrintProc p = - match p with - | Proc(name, ins, outs, req, ens, body) -> - // signature - 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 - printfn "" - printf " ensures " - PrintExpr ens true - printfn "" - // body - printfn "do" - PrintStmtList 2 body - printfn "end;" - -let rec PrintProcs ps = - match ps with - | [] -> () - | p::rest -> PrintProc p ; PrintProcs rest - -let Print prog = - match prog with - | Prog(procs) -> PrintProcs procs +module ForroPrinter + +open System +open Forro + +let PrintField f = + printf "." + match f with + | Head -> printf "head" + | Tail -> printf "tail" + | Valid -> printf "valid" + +let PrintOp op = + printf " " + match op with + | Eq -> printf "==" + | Neq -> printf "!=" + | Plus -> printf "+" + | Minus -> printf "-" + | Times -> printf "*" + | Less -> printf "<" + | AtMost -> printf "<=" + | And -> printf "and" + | Or -> printf "or" + printf " " + +let rec PrintExpr e outermost = + match e with + | Constant(x) -> printf "%i" x + | Null -> printf "null" + | Identifier(Var(x)) -> printf "%s" x + | Not(e) -> printf "not(" ; PrintExpr e true ; printf ")" + | Binary(op,a,b) -> + if outermost then () else printf "(" + PrintExpr a false ; PrintOp op ; PrintExpr b false + if outermost then () else printf ")" + | Select(e,f) -> PrintExpr e false ; PrintField f + | Old(e) -> printf "old(" ; PrintExpr e true ; printf ")" + +let rec Indent n = + if n = 0 then () else printf " " ; Indent (n-1) + +let rec PrintStmt indent s = + Indent indent + let ind = indent + 2 + 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 ; printf ")" + | IfStmt(guard,thn,els) -> + printf "if " ; PrintExpr guard true ; printfn " then" + PrintStmtList ind thn + Indent indent ; printfn "else" + PrintStmtList ind els + Indent indent ; printf "end" + | WhileStmt(guard,invs,body) -> + printf "while " ; PrintExpr guard true ; printfn "" + List.iter (fun inv -> Indent ind ; printf "invariant " ; PrintExpr inv true ; printfn "") invs + Indent indent ; printfn "do" + PrintStmtList ind body + Indent indent ; printf "end" + | CallStmt(outs,id,ins) -> + 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 ")" + | Assert(e) -> + printf "assert " ; PrintExpr e true + printfn ";" + +and PrintStmtList indent slist = + match slist with + | Block(ss) -> List.iter (fun s -> PrintStmt indent s) ss + +let PrintProc p = + match p with + | Proc(name, ins, outs, req, ens, body) -> + // signature + 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 + printfn "" + printf " ensures " + PrintExpr ens true + printfn "" + // body + printfn "do" + PrintStmtList 2 body + printfn "end;" + +let rec PrintProcs ps = + match ps with + | [] -> () + | p::rest -> PrintProc p ; PrintProcs rest + +let Print prog = + match prog with + | Prog(procs) -> PrintProcs procs diff --git a/Source/Forro/Resolver.fs b/Source/Forro/Resolver.fs index f227a5ca..9209f640 100644 --- a/Source/Forro/Resolver.fs +++ b/Source/Forro/Resolver.fs @@ -1,123 +1,123 @@ -module Resolver - -open System -open Forro - -exception ResolutionError of string - -let ResolutionError(s: string) = - raise (ResolutionError s) - -type VarKind = InParam | OutParam | Local - -type Context(procedures: Collections.Generic.IDictionary) = - let mutable locals = null - let mutable ProcName = "" - member c.Procedures = procedures - member c.StartNewProcedure procName = - ProcName <- procName - locals <- new Collections.Generic.Dictionary() - member c.AddLocal v kind = - let name = VarName v - if locals.ContainsKey name then ResolutionError ("duplicate variable '" + name + "' in procedure '" + ProcName + "'") else () - locals.Add(name, kind) - member c.HasLocal v = - locals.ContainsKey (VarName v) - member c.IncludeAssignmentTarget v = - let name = VarName v - if locals.ContainsKey name then - let kind = locals.Item name - if kind = VarKind.InParam then ResolutionError ("variable '"+ name + "' is an in-parameter, which cannot be used as an assignment target") else () - else - locals.Add(name, VarKind.Local) - member v.GetLocals = locals - -let rec ResolveExpr (ctx: Context) expr twoState specContext = - match expr with - | Constant(x) -> () - | Null -> () - | Identifier(v) -> - if ctx.HasLocal v then () else ResolutionError ("undefined variable: " + VarName v) - | Not(e) -> ResolveExpr ctx e twoState specContext - | Binary(op,a,b) -> - ResolveExpr ctx a twoState specContext - ResolveExpr ctx b twoState specContext - | Select(e,f) -> - ResolveExpr ctx e twoState specContext - match f with - | Valid -> if specContext then () else ResolutionError "valid can only be used in specification contexts" - | _ -> () - | Old(e) -> - if twoState then () else ResolutionError "old expressions can only be used in two-state contexts" - ResolveExpr ctx e twoState specContext - -let rec ResolveStmt ctx s = - match s with - | Assign(v, e) -> - ResolveExpr ctx e false false - ctx.IncludeAssignmentTarget v - | Update(obj,f,rhs) -> - ResolveExpr ctx obj false false - match f with - | Valid -> ResolutionError "valid can only be used in specification contexts (in particular, it cannot be assigned to)" - | _ -> () - ResolveExpr ctx rhs false false - | Alloc(v,hd,tl) -> - ResolveExpr ctx hd false false - ResolveExpr ctx tl false false - ctx.IncludeAssignmentTarget v - | IfStmt(guard,thn,els) -> - ResolveExpr ctx guard false false - ResolveStmtList ctx thn - ResolveStmtList ctx els - | WhileStmt(guard,invs,body) -> - ResolveExpr ctx guard false false - List.iter (fun inv -> ResolveExpr ctx inv true true) invs - ResolveStmtList ctx body - | CallStmt(outs,name,ins) -> - if ctx.Procedures.ContainsKey name then () else ResolutionError ("call to undefined procedure: " + name) - match ctx.Procedures.Item name with - | Proc(_,fIns,fOuts,_,_,_) -> - if fIns.Length = ins.Length then () else ResolutionError ("call to " + name + " has wrong number of in-parameters (got " + ins.Length.ToString() + ", expected " + fIns.Length.ToString() + ")") - if fOuts.Length = outs.Length then () else ResolutionError ("call to " + name + " has wrong number of out-parameters (got " + outs.Length.ToString() + ", expected " + fOuts.Length.ToString() + ")") - List.iter (fun e -> ResolveExpr ctx e false false) ins - let outnames = new Collections.Generic.Dictionary() - List.iter (fun v -> - ctx.IncludeAssignmentTarget v - let name = VarName v - if outnames.ContainsKey name then ResolutionError ("an actual out-parameter is allowed only once for a call: " + name) else () - outnames.Add(name, v) - ) outs - | Assert(e) -> - ResolveExpr ctx e true true - -and ResolveStmtList ctx slist = - match slist with - | Block(ss) -> List.iter (fun s -> ResolveStmt ctx s) ss - -let ProcedureName p = - match p with Proc(id,_,_,_,_,_) -> id - -let ResolveProc (ctx: Context) p = - match p with - | Proc(name, ins, outs, req, ens, body) -> - // look up 'name' in ctx.Procedures, report an error if it is not 'p' - let q = ctx.Procedures.Item name - if p <> q then ResolutionError ("duplicate procedure: " + name) else () - ctx.StartNewProcedure name - // look for duplicates in ins+outs - List.iter (fun v -> ctx.AddLocal v VarKind.InParam) ins - List.iter (fun v -> ctx.AddLocal v VarKind.OutParam) outs - // resolve specification - ResolveExpr ctx req false true - ResolveExpr ctx ens true true - // resolve body - ResolveStmtList ctx body - ctx.GetLocals - -let Resolve prog = - match prog with - | Prog(procs) -> - let procedures = dict [ for p in procs -> ProcedureName p, p ] - let ctx = Context(procedures) - List.map (fun p -> p, ResolveProc ctx p) procs +module Resolver + +open System +open Forro + +exception ResolutionError of string + +let ResolutionError(s: string) = + raise (ResolutionError s) + +type VarKind = InParam | OutParam | Local + +type Context(procedures: Collections.Generic.IDictionary) = + let mutable locals = null + let mutable ProcName = "" + member c.Procedures = procedures + member c.StartNewProcedure procName = + ProcName <- procName + locals <- new Collections.Generic.Dictionary() + member c.AddLocal v kind = + let name = VarName v + if locals.ContainsKey name then ResolutionError ("duplicate variable '" + name + "' in procedure '" + ProcName + "'") else () + locals.Add(name, kind) + member c.HasLocal v = + locals.ContainsKey (VarName v) + member c.IncludeAssignmentTarget v = + let name = VarName v + if locals.ContainsKey name then + let kind = locals.Item name + if kind = VarKind.InParam then ResolutionError ("variable '"+ name + "' is an in-parameter, which cannot be used as an assignment target") else () + else + locals.Add(name, VarKind.Local) + member v.GetLocals = locals + +let rec ResolveExpr (ctx: Context) expr twoState specContext = + match expr with + | Constant(x) -> () + | Null -> () + | Identifier(v) -> + if ctx.HasLocal v then () else ResolutionError ("undefined variable: " + VarName v) + | Not(e) -> ResolveExpr ctx e twoState specContext + | Binary(op,a,b) -> + ResolveExpr ctx a twoState specContext + ResolveExpr ctx b twoState specContext + | Select(e,f) -> + ResolveExpr ctx e twoState specContext + match f with + | Valid -> if specContext then () else ResolutionError "valid can only be used in specification contexts" + | _ -> () + | Old(e) -> + if twoState then () else ResolutionError "old expressions can only be used in two-state contexts" + ResolveExpr ctx e twoState specContext + +let rec ResolveStmt ctx s = + match s with + | Assign(v, e) -> + ResolveExpr ctx e false false + ctx.IncludeAssignmentTarget v + | Update(obj,f,rhs) -> + ResolveExpr ctx obj false false + match f with + | Valid -> ResolutionError "valid can only be used in specification contexts (in particular, it cannot be assigned to)" + | _ -> () + ResolveExpr ctx rhs false false + | Alloc(v,hd,tl) -> + ResolveExpr ctx hd false false + ResolveExpr ctx tl false false + ctx.IncludeAssignmentTarget v + | IfStmt(guard,thn,els) -> + ResolveExpr ctx guard false false + ResolveStmtList ctx thn + ResolveStmtList ctx els + | WhileStmt(guard,invs,body) -> + ResolveExpr ctx guard false false + List.iter (fun inv -> ResolveExpr ctx inv true true) invs + ResolveStmtList ctx body + | CallStmt(outs,name,ins) -> + if ctx.Procedures.ContainsKey name then () else ResolutionError ("call to undefined procedure: " + name) + match ctx.Procedures.Item name with + | Proc(_,fIns,fOuts,_,_,_) -> + if fIns.Length = ins.Length then () else ResolutionError ("call to " + name + " has wrong number of in-parameters (got " + ins.Length.ToString() + ", expected " + fIns.Length.ToString() + ")") + if fOuts.Length = outs.Length then () else ResolutionError ("call to " + name + " has wrong number of out-parameters (got " + outs.Length.ToString() + ", expected " + fOuts.Length.ToString() + ")") + List.iter (fun e -> ResolveExpr ctx e false false) ins + let outnames = new Collections.Generic.Dictionary() + List.iter (fun v -> + ctx.IncludeAssignmentTarget v + let name = VarName v + if outnames.ContainsKey name then ResolutionError ("an actual out-parameter is allowed only once for a call: " + name) else () + outnames.Add(name, v) + ) outs + | Assert(e) -> + ResolveExpr ctx e true true + +and ResolveStmtList ctx slist = + match slist with + | Block(ss) -> List.iter (fun s -> ResolveStmt ctx s) ss + +let ProcedureName p = + match p with Proc(id,_,_,_,_,_) -> id + +let ResolveProc (ctx: Context) p = + match p with + | Proc(name, ins, outs, req, ens, body) -> + // look up 'name' in ctx.Procedures, report an error if it is not 'p' + let q = ctx.Procedures.Item name + if p <> q then ResolutionError ("duplicate procedure: " + name) else () + ctx.StartNewProcedure name + // look for duplicates in ins+outs + List.iter (fun v -> ctx.AddLocal v VarKind.InParam) ins + List.iter (fun v -> ctx.AddLocal v VarKind.OutParam) outs + // resolve specification + ResolveExpr ctx req false true + ResolveExpr ctx ens true true + // resolve body + ResolveStmtList ctx body + ctx.GetLocals + +let Resolve prog = + match prog with + | Prog(procs) -> + let procedures = dict [ for p in procs -> ProcedureName p, p ] + let ctx = Context(procedures) + List.map (fun p -> p, ResolveProc ctx p) procs diff --git a/Source/Forro/Translator.fs b/Source/Forro/Translator.fs index 4e7be216..db771c96 100644 --- a/Source/Forro/Translator.fs +++ b/Source/Forro/Translator.fs @@ -1,217 +1,217 @@ -module Translator - -open Forro -open BoogieAst -open Resolver -open System.Collections.Generic - -let rec Append a b = - match a with - | [] -> b - | hd::tl -> hd::(Append tl b) - -let rec Flatten a = - match a with - | [] -> [] - | list::rest -> Append list (Flatten rest) - -// ---------- Prelude ---------- - -let Prelude = - @"// Forro - -var $head: [int]int; // int -> int -var $tail: [int]int; -var $valid: [int]bool; // array int of bool - -const null: int; - -function GoodState([int]int, [int]int, [int]bool): bool; - -axiom (forall hd, tl: [int]int, valid: [int]bool :: - { GoodState(hd, tl, valid) } - GoodState(hd, tl, valid) ==> !valid[null]); -" - -// ---------- Translate Expressions ---------- - -let TrField f = - match f with - | Head -> "$head" - | Tail -> "$tail" - | Valid -> "$valid" - -let AllFields = ["$head" ; "$tail" ; "$valid"] - -let MkPred term = - match term with - | BToTerm(p) -> p - | _ -> BToPred(term) - -let MkTerm pred = - match pred with - | BToPred(e) -> e - | _ -> BToTerm(pred) - -let rec TrExpr expr = - match expr with - | Constant(x) -> BConstant x - | Null -> BNull - | Identifier(Var(x)) -> BIdentifier(x) - | Not(e) -> BNot(TrExpr e) - | Binary(op,a,b) -> - let a = TrExpr a - let b = TrExpr b - match op with - | Eq -> MkTerm(BBinary(BEq,a,b)) - | Neq -> MkTerm(BBinary(BNeq,a,b)) - | Plus -> BBinary(BPlus,a,b) - | Minus -> BBinary(BMinus,a,b) - | Times -> BBinary(BTimes,a,b) - | Less -> MkTerm(BBinary(BLess,a,b)) - | AtMost -> MkTerm(BBinary(BAtMost,a,b)) - | And -> MkTerm(BBinary(BAnd, MkPred a, MkPred b)) - | Or -> MkTerm(BBinary(BOr, MkPred a, MkPred b)) - | Select(e,f) -> - let r = BSelect(TrField f, TrExpr e) - if f = Field.Valid then MkTerm(r) else r - | Old(e) -> BOld(TrExpr e) - -let rec ListToConjunction list = - match list with - | [] -> BTrue - | [P] -> P - | hd::tl -> BBinary(BAnd, hd, ListToConjunction tl) - -let rec DefL expr = - match expr with - | Constant(x) -> [] - | Null -> [] - | Identifier(Var(x)) -> [] - | Not(e) -> DefL e - | Binary(op,a,b) -> - match op with - | 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 - if f = Field.Valid then def // it is always okay to ask about .valid - else BSelect("$valid", TrExpr e) :: def - | Old(e) -> List.map BOld (DefL e) - -and Def expr = - ListToConjunction (List.rev (DefL expr)) - -let AssumeGoodState = - BAssume (BFunc("GoodState", List.map BIdentifier AllFields)) - -// ---------- Translate Statements ---------- - -type LocalBookkeeping = LB of int * BVarDecl list - -let FreshLocal locals = - match locals with - | LB(n, vars) -> - let name = "nw$" + n.ToString() - (BIdentifier(name), name, LB(n+1, BVar(name, BInt)::vars)) - -let rec TrStmt stmt locals = - match stmt with - | Assign(v,e) -> - let s = [ BAssert (Def e) ; - BAssign(VarName v, TrExpr e) ] - (s, locals) - | Update(obj,f,rhs) -> - let o = TrExpr obj - let s = [ BAssert(Def obj) ; BAssert (Def rhs) ; - BAssert(BSelect("$valid", o)) ; - BUpdate(TrField f, o, if f = Field.Valid then MkPred(TrExpr rhs) else TrExpr rhs) ; - AssumeGoodState ] - (s, locals) - | Alloc(v,hd,tl) -> - 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)) ; - BUpdate("$valid", nw, BTrue) ; - AssumeGoodState ; - BAssign(VarName v, nw) ] - (s, locals) - | IfStmt(guard,thn,els) -> - let check = BAssert(Def guard) - let thn, locals = TrStmtList thn locals - let els, locals = TrStmtList els locals - let s = BIfStmt(MkPred (TrExpr guard), thn, els) - ([check ; s], locals) - | WhileStmt(guard,invs,body) -> - let ii = [Def guard] - let ii = List.fold (fun ii -> fun inv -> (MkPred (TrExpr inv))::(Def inv)::ii) ii invs - let s, locals = TrStmtList body locals - match s with - | BBlock(slist) -> - ([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) - (Append check [s ; AssumeGoodState ], locals) - | Assert(e) -> - ([ BAssert (Def e) ; BAssert (MkPred (TrExpr e)) ], locals) - -and TrStmtList slist locals = - match slist with - | Block([]) -> (BBlock [], locals) - | Block(s::rest) -> - let s,locals = TrStmt s locals - let rest,locals = TrStmtList (Block rest) locals - match rest with - | BBlock(slist) -> (BBlock(Append s slist), locals) - -// ---------- Translate Procedure Body ---------- - -let TrSignature ins outs = - let bIns = List.map (fun v -> BVar(VarName v, BInt)) ins - let bOuts = List.map (fun v -> BVar(VarName v, BInt)) outs - (bIns, bOuts) - -let LocalDecls (vars: Dictionary) = - Flatten [ for kv in vars -> if kv.Value = VarKind.Local then [BVar(kv.Key, BInt)] else [] ] - -let TrProc proc vars = - match proc with - | Proc(id, ins, outs, req, ens, body) -> - let bIns, bOuts = TrSignature ins outs - let pre = MkPred (TrExpr req) - let post = MkPred (TrExpr ens) - let locals = LocalDecls 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)) - -// -------------------- - -let TrSpec proc vars = - match proc with - | Proc(id, ins, outs, req, ens, body) -> - let bIns, bOuts = TrSignature ins outs - let b = [ AssumeGoodState ; - BAssert (Def req) ; BAssume (MkPred (TrExpr req)) ; - BHavoc AllFields ; AssumeGoodState ; - BAssert (Def ens) ] - BProc(id + "#WellFormedSpec", bIns, bOuts, BTrue, AllFields, BTrue, [], BBlock(b)) - -let TrProcedure rproc = - match rproc with - | proc, (vars: Dictionary) -> - let name = ProcedureName proc - (TrSpec proc vars, TrProc proc vars) - -let Translate (rprog: (Procedure * Dictionary) list) = - let procs = List.fold (fun list -> fun (p,q) -> p::q::list) [] (List.map TrProcedure rprog) - BProg(Prelude, procs) +module Translator + +open Forro +open BoogieAst +open Resolver +open System.Collections.Generic + +let rec Append a b = + match a with + | [] -> b + | hd::tl -> hd::(Append tl b) + +let rec Flatten a = + match a with + | [] -> [] + | list::rest -> Append list (Flatten rest) + +// ---------- Prelude ---------- + +let Prelude = + @"// Forro + +var $head: [int]int; // int -> int +var $tail: [int]int; +var $valid: [int]bool; // array int of bool + +const null: int; + +function GoodState([int]int, [int]int, [int]bool): bool; + +axiom (forall hd, tl: [int]int, valid: [int]bool :: + { GoodState(hd, tl, valid) } + GoodState(hd, tl, valid) ==> !valid[null]); +" + +// ---------- Translate Expressions ---------- + +let TrField f = + match f with + | Head -> "$head" + | Tail -> "$tail" + | Valid -> "$valid" + +let AllFields = ["$head" ; "$tail" ; "$valid"] + +let MkPred term = + match term with + | BToTerm(p) -> p + | _ -> BToPred(term) + +let MkTerm pred = + match pred with + | BToPred(e) -> e + | _ -> BToTerm(pred) + +let rec TrExpr expr = + match expr with + | Constant(x) -> BConstant x + | Null -> BNull + | Identifier(Var(x)) -> BIdentifier(x) + | Not(e) -> BNot(TrExpr e) + | Binary(op,a,b) -> + let a = TrExpr a + let b = TrExpr b + match op with + | Eq -> MkTerm(BBinary(BEq,a,b)) + | Neq -> MkTerm(BBinary(BNeq,a,b)) + | Plus -> BBinary(BPlus,a,b) + | Minus -> BBinary(BMinus,a,b) + | Times -> BBinary(BTimes,a,b) + | Less -> MkTerm(BBinary(BLess,a,b)) + | AtMost -> MkTerm(BBinary(BAtMost,a,b)) + | And -> MkTerm(BBinary(BAnd, MkPred a, MkPred b)) + | Or -> MkTerm(BBinary(BOr, MkPred a, MkPred b)) + | Select(e,f) -> + let r = BSelect(TrField f, TrExpr e) + if f = Field.Valid then MkTerm(r) else r + | Old(e) -> BOld(TrExpr e) + +let rec ListToConjunction list = + match list with + | [] -> BTrue + | [P] -> P + | hd::tl -> BBinary(BAnd, hd, ListToConjunction tl) + +let rec DefL expr = + match expr with + | Constant(x) -> [] + | Null -> [] + | Identifier(Var(x)) -> [] + | Not(e) -> DefL e + | Binary(op,a,b) -> + match op with + | 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 + if f = Field.Valid then def // it is always okay to ask about .valid + else BSelect("$valid", TrExpr e) :: def + | Old(e) -> List.map BOld (DefL e) + +and Def expr = + ListToConjunction (List.rev (DefL expr)) + +let AssumeGoodState = + BAssume (BFunc("GoodState", List.map BIdentifier AllFields)) + +// ---------- Translate Statements ---------- + +type LocalBookkeeping = LB of int * BVarDecl list + +let FreshLocal locals = + match locals with + | LB(n, vars) -> + let name = "nw$" + n.ToString() + (BIdentifier(name), name, LB(n+1, BVar(name, BInt)::vars)) + +let rec TrStmt stmt locals = + match stmt with + | Assign(v,e) -> + let s = [ BAssert (Def e) ; + BAssign(VarName v, TrExpr e) ] + (s, locals) + | Update(obj,f,rhs) -> + let o = TrExpr obj + let s = [ BAssert(Def obj) ; BAssert (Def rhs) ; + BAssert(BSelect("$valid", o)) ; + BUpdate(TrField f, o, if f = Field.Valid then MkPred(TrExpr rhs) else TrExpr rhs) ; + AssumeGoodState ] + (s, locals) + | Alloc(v,hd,tl) -> + 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)) ; + BUpdate("$valid", nw, BTrue) ; + AssumeGoodState ; + BAssign(VarName v, nw) ] + (s, locals) + | IfStmt(guard,thn,els) -> + let check = BAssert(Def guard) + let thn, locals = TrStmtList thn locals + let els, locals = TrStmtList els locals + let s = BIfStmt(MkPred (TrExpr guard), thn, els) + ([check ; s], locals) + | WhileStmt(guard,invs,body) -> + let ii = [Def guard] + let ii = List.fold (fun ii -> fun inv -> (MkPred (TrExpr inv))::(Def inv)::ii) ii invs + let s, locals = TrStmtList body locals + match s with + | BBlock(slist) -> + ([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) + (Append check [s ; AssumeGoodState ], locals) + | Assert(e) -> + ([ BAssert (Def e) ; BAssert (MkPred (TrExpr e)) ], locals) + +and TrStmtList slist locals = + match slist with + | Block([]) -> (BBlock [], locals) + | Block(s::rest) -> + let s,locals = TrStmt s locals + let rest,locals = TrStmtList (Block rest) locals + match rest with + | BBlock(slist) -> (BBlock(Append s slist), locals) + +// ---------- Translate Procedure Body ---------- + +let TrSignature ins outs = + let bIns = List.map (fun v -> BVar(VarName v, BInt)) ins + let bOuts = List.map (fun v -> BVar(VarName v, BInt)) outs + (bIns, bOuts) + +let LocalDecls (vars: Dictionary) = + Flatten [ for kv in vars -> if kv.Value = VarKind.Local then [BVar(kv.Key, BInt)] else [] ] + +let TrProc proc vars = + match proc with + | Proc(id, ins, outs, req, ens, body) -> + let bIns, bOuts = TrSignature ins outs + let pre = MkPred (TrExpr req) + let post = MkPred (TrExpr ens) + let locals = LocalDecls 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)) + +// -------------------- + +let TrSpec proc vars = + match proc with + | Proc(id, ins, outs, req, ens, body) -> + let bIns, bOuts = TrSignature ins outs + let b = [ AssumeGoodState ; + BAssert (Def req) ; BAssume (MkPred (TrExpr req)) ; + BHavoc AllFields ; AssumeGoodState ; + BAssert (Def ens) ] + BProc(id + "#WellFormedSpec", bIns, bOuts, BTrue, AllFields, BTrue, [], BBlock(b)) + +let TrProcedure rproc = + match rproc with + | proc, (vars: Dictionary) -> + let name = ProcedureName proc + (TrSpec proc vars, TrProc proc vars) + +let Translate (rprog: (Procedure * Dictionary) list) = + let procs = List.fold (fun list -> fun (p,q) -> p::q::list) [] (List.map TrProcedure rprog) + BProg(Prelude, procs) -- cgit v1.2.3