From ea1898f88e2edcecf3a58923fcd1a5d2b87219a8 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Sat, 6 Nov 2010 19:47:03 +0000 Subject: Introducing Forr?! Forr? is a tiny language that translates to Boogie. The purpose of the language and verifier is to serve as a tutorial example for how to build a verifier on top of Boogie. --- Source/Forro/Ast.fs | 34 +++++++ Source/Forro/BoogieAst.fs | 40 ++++++++ Source/Forro/BoogiePrinter.fs | 112 ++++++++++++++++++++++ Source/Forro/Forro.fsproj | 82 ++++++++++++++++ Source/Forro/Lexer.fsl | 56 +++++++++++ Source/Forro/Main.fs | 52 ++++++++++ Source/Forro/Parser.fsy | 115 ++++++++++++++++++++++ Source/Forro/Printer.fs | 110 +++++++++++++++++++++ Source/Forro/Resolver.fs | 126 +++++++++++++++++++++++++ Source/Forro/Translator.fs | 215 ++++++++++++++++++++++++++++++++++++++++++ 10 files changed, 942 insertions(+) create mode 100644 Source/Forro/Ast.fs create mode 100644 Source/Forro/BoogieAst.fs create mode 100644 Source/Forro/BoogiePrinter.fs create mode 100644 Source/Forro/Forro.fsproj create mode 100644 Source/Forro/Lexer.fsl create mode 100644 Source/Forro/Main.fs create mode 100644 Source/Forro/Parser.fsy create mode 100644 Source/Forro/Printer.fs create mode 100644 Source/Forro/Resolver.fs create mode 100644 Source/Forro/Translator.fs (limited to 'Source/Forro') diff --git a/Source/Forro/Ast.fs b/Source/Forro/Ast.fs new file mode 100644 index 00000000..fa4db8ec --- /dev/null +++ b/Source/Forro/Ast.fs @@ -0,0 +1,34 @@ +namespace Forro + +type Field = Head | Tail | Valid + +type Variable = Var of string + +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 StmtList = + Block of Statement list + +and 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 + +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 new file mode 100644 index 00000000..964f6667 --- /dev/null +++ b/Source/Forro/BoogieAst.fs @@ -0,0 +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 diff --git a/Source/Forro/BoogiePrinter.fs b/Source/Forro/BoogiePrinter.fs new file mode 100644 index 00000000..8f2b37ee --- /dev/null +++ b/Source/Forro/BoogiePrinter.fs @@ -0,0 +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 diff --git a/Source/Forro/Forro.fsproj b/Source/Forro/Forro.fsproj new file mode 100644 index 00000000..531264b3 --- /dev/null +++ b/Source/Forro/Forro.fsproj @@ -0,0 +1,82 @@ + + + + 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 new file mode 100644 index 00000000..b1271536 --- /dev/null +++ b/Source/Forro/Lexer.fsl @@ -0,0 +1,56 @@ +{ +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 { tokenize lexbuf } +// operators +| "==" { EQ } +| "!=" { NEQ } +| "+" { PLUS } +| "-" { MINUS } +| "*" { STAR } +| "<" { LESS } +| "<=" { ATMOST } +| "and" { AND } +| "or" { OR } +| "not" { NOT } +| "old" { OLD } +| "." { DOT } +// misc +| "(" { LPAREN } +| ")" { RPAREN } +| ";" { SEMI } +| ":=" { 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 new file mode 100644 index 00000000..41c45220 --- /dev/null +++ b/Source/Forro/Main.fs @@ -0,0 +1,52 @@ +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 lexbuff = LexBuffer.FromTextReader(f) + // parse + let prog = Parser.start Lexer.tokenize lexbuff + // 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 new file mode 100644 index 00000000..6fa41431 --- /dev/null +++ b/Source/Forro/Parser.fsy @@ -0,0 +1,115 @@ +%{ + +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 PLUS MINUS +%token STAR +%token EQ NEQ LESS ATMOST +%token AND OR +%token OLD LPAREN RPAREN SEMI 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 + REQUIRES Expression ENSURES Expression + DO StmtList END SEMI + { match $2 with outs,id,ins -> Proc(id, StringsToVariables ins, StringsToVariables outs, $4, $6, $8) } + +Signature: + IdList { [], List.head $1, List.tail $1 } + | IdList ASSIGN IdList { $1, List.head $3, List.tail $3 } + +IdList: ID { [$1] } + | ID IdList { $1 :: $2 } + +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: // possibly empty + { [] } + | Expression ExprList { $1::$2 } + +VarList: // nonempty + | ID ASSIGN { [Var($1)] } + | ID VarList { Var($1)::$2 } + +StmtList: + StmtListX { Block($1) } + +StmtListX: + { [] } + | Stmt StmtListX { $1::$2 } + +Stmt: + ID ASSIGN Expression SEMI { Assign(Var($1), $3) } + | ID ASSIGN NEW Expression Expression SEMI { Alloc(Var($1), $4, $5) } + | 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 ExprList RPAREN SEMI { CallStmt([],$2,$4) } + | 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 new file mode 100644 index 00000000..65d515f8 --- /dev/null +++ b/Source/Forro/Printer.fs @@ -0,0 +1,110 @@ +module ForroPrinter + +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 + | 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 + | 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 PrintVars 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 ; printfn ";" + 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 PrintVars outs ; printf " :=" + printf " %s" name + PrintVars 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 new file mode 100644 index 00000000..9844c24b --- /dev/null +++ b/Source/Forro/Resolver.fs @@ -0,0 +1,126 @@ +module Resolver + +open System +open Forro + +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) = + 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 new file mode 100644 index 00000000..77f3c864 --- /dev/null +++ b/Source/Forro/Translator.fs @@ -0,0 +1,215 @@ +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; +var $tail: [int]int; +var $valid: [int]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) + | Or -> BBinary(BOr, MkPred (TrExpr a), Def b) :: (DefL a) + | _ -> 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), 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, locals = FreshLocal locals + let s = [ BAssert (Def hd) ; BAssert (Def tl) ; + 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))], 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) + | 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