summaryrefslogtreecommitdiff
path: root/Source/Forro
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Forro')
-rw-r--r--Source/Forro/Ast.fs76
-rw-r--r--Source/Forro/BoogieAst.fs80
-rw-r--r--Source/Forro/BoogiePrinter.fs224
-rw-r--r--Source/Forro/Forro.fsproj164
-rw-r--r--Source/Forro/Lexer.fsl120
-rw-r--r--Source/Forro/Main.fs114
-rw-r--r--Source/Forro/Parser.fsy244
-rw-r--r--Source/Forro/Printer.fs214
-rw-r--r--Source/Forro/Resolver.fs246
-rw-r--r--Source/Forro/Translator.fs434
10 files changed, 958 insertions, 958 deletions
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 @@
-<?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" />
- <Reference Include="System.Numerics" />
- </ItemGroup>
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
- Other similar extension points exist, see Microsoft.Common.targets.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
+<?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" />
+ <Reference Include="System.Numerics" />
+ </ItemGroup>
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <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
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<char>.LexemeString lexbuf)) }
-| "null" { NULL }
-// identifiers
-| idchar+ { ID (LexBuffer<char>.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<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
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<char>.FromTextReader(f)
- lexbuf.EndPos <- { pos_bol = 0;
- pos_fname=if filename = null then "stdin" else filename;
- pos_cnum=0;
- pos_lnum=1 }
- // parse
- let prog = Parser.start Lexer.tokenize 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<char>.FromTextReader(f)
+ lexbuf.EndPos <- { pos_bol = 0;
+ pos_fname=if filename = null then "stdin" else filename;
+ pos_cnum=0;
+ pos_lnum=1 }
+ // parse
+ let prog = Parser.start Lexer.tokenize 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 <string> ID
-%token <System.Int32> 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 <string> ID
+%token <System.Int32> 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<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
+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<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
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<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)
+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<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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 21:41:36 +0000