diff options
| author |  rustanleino <unknown> | 2010-11-06 19:47:03 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-11-06 19:47:03 +0000 |
| commit | ea1898f88e2edcecf3a58923fcd1a5d2b87219a8 (patch) | |
| tree | 82944147dd136bf68b4cb2f8e40d440c6705d42e | |
| parent | 8d1dd0f01a78bf29aa98832317d8fc951ed15075 (diff) | |
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.
| -rw-r--r-- | Source/Forro.sln | 20 | ||||
| -rw-r--r-- | Source/Forro/Ast.fs | 34 | ||||
| -rw-r--r-- | Source/Forro/BoogieAst.fs | 40 | ||||
| -rw-r--r-- | Source/Forro/BoogiePrinter.fs | 112 | ||||
| -rw-r--r-- | Source/Forro/Forro.fsproj | 82 | ||||
| -rw-r--r-- | Source/Forro/Lexer.fsl | 56 | ||||
| -rw-r--r-- | Source/Forro/Main.fs | 52 | ||||
| -rw-r--r-- | Source/Forro/Parser.fsy | 115 | ||||
| -rw-r--r-- | Source/Forro/Printer.fs | 110 | ||||
| -rw-r--r-- | Source/Forro/Resolver.fs | 126 | ||||
| -rw-r--r-- | Source/Forro/Translator.fs | 215 | ||||
| -rw-r--r-- | Test/forro/prog0.forro | 39 |
12 files changed, 1001 insertions, 0 deletions
diff --git a/Source/Forro.sln b/Source/Forro.sln new file mode 100644 index 00000000..39e50152 --- /dev/null +++ b/Source/Forro.sln @@ -0,0 +1,20 @@ +
+Microsoft Visual Studio Solution File, Format Version 11.00
+# Visual Studio 2010
+Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Forro", "Forro\Forro.fsproj", "{C75E47A0-E88D-4035-9EBF-F6647AF92B79}"
+EndProject
+Global
+ GlobalSection(SolutionConfigurationPlatforms) = preSolution
+ Debug|x86 = Debug|x86
+ Release|x86 = Release|x86
+ EndGlobalSection
+ GlobalSection(ProjectConfigurationPlatforms) = postSolution
+ {C75E47A0-E88D-4035-9EBF-F6647AF92B79}.Debug|x86.ActiveCfg = Debug|x86
+ {C75E47A0-E88D-4035-9EBF-F6647AF92B79}.Debug|x86.Build.0 = Debug|x86
+ {C75E47A0-E88D-4035-9EBF-F6647AF92B79}.Release|x86.ActiveCfg = Release|x86
+ {C75E47A0-E88D-4035-9EBF-F6647AF92B79}.Release|x86.Build.0 = Release|x86
+ EndGlobalSection
+ GlobalSection(SolutionProperties) = preSolution
+ HideSolutionNode = FALSE
+ EndGlobalSection
+EndGlobal
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 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">x86</Platform>
+ <ProductVersion>8.0.30703</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{c75e47a0-e88d-4035-9ebf-f6647af92b79}</ProjectGuid>
+ <OutputType>Exe</OutputType>
+ <RootNamespace>Language</RootNamespace>
+ <AssemblyName>Forro</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ <Name>Language</Name>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <Tailcalls>false</Tailcalls>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <WarningLevel>3</WarningLevel>
+ <PlatformTarget>x86</PlatformTarget>
+ <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <Tailcalls>true</Tailcalls>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <WarningLevel>3</WarningLevel>
+ <PlatformTarget>x86</PlatformTarget>
+ <DocumentationFile>bin\Release\Language.XML</DocumentationFile>
+ </PropertyGroup>
+ <Import Project="$(MSBuildExtensionsPath32)\..\Microsoft F#\v4.0\Microsoft.FSharp.Targets" />
+ <Import Project="$(MSBuildExtensionsPath32)\..\FSharpPowerPack-2.0.0.0\bin\FSharp.PowerPack.targets" />
+ <PropertyGroup>
+ <FsLexOutputFolder>$(IntermediateOutputPath)</FsLexOutputFolder>
+ <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>
+ </PropertyGroup>
+ <ItemGroup>
+ <Compile Include="Ast.fs" />
+ <Compile Include="$(IntermediateOutputPath)\Parser.fs">
+ <Visible>false</Visible>
+ <Link>Parser.fs</Link>
+ </Compile>
+ <Compile Include="$(IntermediateOutputPath)\Lexer.fs">
+ <Visible>false</Visible>
+ <Link>Lexer.fs</Link>
+ </Compile>
+ <FsYacc Include="Parser.fsy">
+ <OtherFlags>--module Parser</OtherFlags>
+ </FsYacc>
+ <FsLex Include="Lexer.fsl">
+ <OtherFlags>--unicode</OtherFlags>
+ </FsLex>
+ <Compile Include="Printer.fs" />
+ <Compile Include="Resolver.fs" />
+ <Compile Include="BoogieAst.fs" />
+ <Compile Include="BoogiePrinter.fs" />
+ <Compile Include="Translator.fs" />
+ <Compile Include="Main.fs" />
+ </ItemGroup>
+ <ItemGroup>
+ <Reference Include="FSharp.PowerPack">
+ <HintPath>C:\Program Files\FSharpPowerPack-1.9.9.9\bin\FSharp.PowerPack.dll</HintPath>
+ </Reference>
+ <Reference Include="mscorlib" />
+ <Reference Include="FSharp.Core" />
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ </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.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ 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<char>.LexemeString lexbuf)) }
+| "null" { NULL }
+// identifiers
+| idchar+ { ID (LexBuffer<char>.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<char>.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 <string> ID
+%token <System.Int32> 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<string,Procedure>) =
+ let mutable locals = null
+ let mutable ProcName = ""
+ member c.Procedures = procedures
+ member c.StartNewProcedure procName =
+ ProcName <- procName
+ locals <- new Collections.Generic.Dictionary<string,VarKind>()
+ 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<string,Variable>()
+ 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<string,VarKind>) =
+ 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<string,VarKind>) ->
+ let name = ProcedureName proc
+ (TrSpec proc vars, TrProc proc vars)
+
+let Translate (rprog: (Procedure * Dictionary<string,VarKind>) list) =
+ let procs = List.fold (fun list -> fun (p,q) -> p::q::list) [] (List.map TrProcedure rprog)
+ BProg(Prelude, procs)
diff --git a/Test/forro/prog0.forro b/Test/forro/prog0.forro new file mode 100644 index 00000000..87dbbd01 --- /dev/null +++ b/Test/forro/prog0.forro @@ -0,0 +1,39 @@ +procedure a b c := P x y z
+ requires 10
+ ensures 20
+do
+ if 30 then else end;
+ if 31 then else end;
+ while x < z
+ invariant x <= z
+ invariant b.valid and 1
+ do
+ k := x + 1;
+ end;
+ (x+5).head := c.tail;
+ a := new 17 18;
+ assert a != null;
+ m := k + a + null;
+ c := m;
+ call Q(x y y);
+ if x then
+ call a c b := P(a b c);
+ else
+ call R();
+ end;
+end;
+
+
+procedure Q x y z
+ requires 10
+ ensures 20
+do
+ if 40 then else end;
+end;
+
+
+procedure R
+ requires 10
+ ensures 20
+do
+end;
|