diff options
| -rw-r--r-- | Jennisys/Analyzer.fs | 92 | ||||
| -rw-r--r-- | Jennisys/Ast.fs | 8 | ||||
| -rw-r--r-- | Jennisys/Jennisys.fs | 25 | ||||
| -rw-r--r-- | Jennisys/Jennisys.fsproj | 2 | ||||
| -rw-r--r-- | Jennisys/Parser.fsy | 4 | ||||
| -rw-r--r-- | Jennisys/Printer.fs | 2 | ||||
| -rw-r--r-- | Jennisys/TypeChecker.fs | 26 |
7 files changed, 147 insertions, 12 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs new file mode 100644 index 00000000..9b7e28ca --- /dev/null +++ b/Jennisys/Analyzer.fs @@ -0,0 +1,92 @@ +module Analyzer
+
+open Ast
+open Printer
+
+let rec PrintType ty =
+ match ty with
+ | NamedType(id) -> printf "%s" id
+ | InstantiatedType(id,arg) -> printf "%s<" id ; PrintType arg ; printf ">"
+
+let rec PrintExpr ctx expr =
+ match expr with
+ | IntLiteral(n) -> printf "%O" n
+ | IdLiteral(id) -> printf "%s" id
+ | Star -> assert false // I hope this won't happen
+ | Dot(e,id) -> PrintExpr 100 e ; printf ".%s" id
+ | UnaryExpr(op,e) -> printf "%s" op ; PrintExpr 90 e
+ | BinaryExpr(strength,op,e0,e1) ->
+ let op =
+ match op with
+ | "=" -> "=="
+ | "div" -> "/"
+ | "mod" -> "%"
+ | _ -> op
+ let needParens = strength <= ctx
+ if needParens then printf "(" else ()
+ PrintExpr strength e0 ; printf " %s " op ; PrintExpr strength e1
+ if needParens then printf ")" else ()
+ | SelectExpr(e,i) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf "]"
+ | UpdateExpr(e,i,v) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf " := " ; PrintExpr 0 v ; printf "]"
+ | SequenceExpr(ee) -> printf "[" ; ee |> PrintSep ", " (PrintExpr 0) ; printf "]"
+ | SeqLength(e) -> printf "|" ; PrintExpr 0 e ; printf "|"
+ | ForallExpr(vv,e) ->
+ let needParens = true
+ if needParens then printf "(" else ()
+ printf "forall " ; vv |> PrintSep ", " PrintVarDecl ; printf " :: " ; PrintExpr 0 e
+ if needParens then printf ")" else ()
+
+let Fields members =
+ members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)
+
+let Rename suffix vars =
+ vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))
+
+let ReplaceName substMap nm =
+ match Map.tryFind nm substMap with
+ | Some(Var(name, tp)) -> name
+ | None -> nm
+
+let rec Substitute substMap = function
+ | IdLiteral(s) -> IdLiteral(ReplaceName substMap s)
+ | Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f)
+ | UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e)
+ | BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1)
+ | SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1)
+ | UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2)
+ | SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee)
+ | SeqLength(e) -> SeqLength(Substitute substMap e)
+ | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)
+ | expr -> expr
+
+let AnalyzeComponent c =
+ match c with
+ | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
+ let aVars = Fields members
+ let aVars0 = Rename "0" aVars
+ let aVars1 = Rename "1" aVars
+ let allVars = List.concat [List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars]
+ let inv0 = Substitute (Map.ofList aVars0) inv
+ let inv1 = Substitute (Map.ofList aVars1) inv
+ // Now print it as a Dafny program
+ printf "class %s" name
+ match typeParams with
+ | [] -> ()
+ | _ -> printf "<" ; typeParams |> PrintSep ", " (fun tp -> printf "%s" tp) ; printf ">"
+ printfn " {"
+ // the fields, both abstract and concrete
+ allVars |> List.iter (function Var(nm,None) -> printfn " var %s;" nm | Var(nm,Some(tp)) -> printf " var %s: " nm ; PrintType tp ; printfn ";")
+ // the method
+ printfn " method %s_checkInjective() {" name
+ printf " assume " ; PrintExpr 0 inv0 ; printfn ";"
+ printf " assume " ; PrintExpr 0 inv1 ; printfn ";"
+ printfn " assert false;"
+ printfn " }"
+ // the end of the class
+ printfn "}"
+ | _ -> assert false // unexpected case
+
+let Analyze prog =
+ match prog with
+ | Program(components) ->
+ components |> List.iter AnalyzeComponent
diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs index 2c2610ce..fa2db0d9 100644 --- a/Jennisys/Ast.fs +++ b/Jennisys/Ast.fs @@ -40,5 +40,11 @@ type TopLevelDecl = | Model of string * string list * VarDecl list * Expr list * Expr
| Code of string * string list
+type SyntacticProgram =
+ | SProgram of TopLevelDecl list
+
+type Component =
+ | Component of (*class*)TopLevelDecl * (*model*)TopLevelDecl * (*code*)TopLevelDecl
+
type Program =
- | Program of TopLevelDecl list
+ | Program of Component list
diff --git a/Jennisys/Jennisys.fs b/Jennisys/Jennisys.fs index d266a065..b248cf67 100644 --- a/Jennisys/Jennisys.fs +++ b/Jennisys/Jennisys.fs @@ -11,11 +11,13 @@ open Ast open Lexer
open Parser
open Printer
+open TypeChecker
+open Analyzer
-let readAndProcess tracing (filename: string) =
+let readAndProcess tracing analyzing (filename: string) =
try
- printfn "Jennisys, Copyright (c) 2011, Microsoft."
+ printfn "// Jennisys, Copyright (c) 2011, Microsoft."
// lex
let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
let lexbuf = LexBuffer<char>.FromTextReader(f)
@@ -25,12 +27,19 @@ let readAndProcess tracing (filename: string) = pos_lnum=1 }
try
// parse
- let prog = Parser.start Lexer.tokenize lexbuf
+ let sprog = Parser.start Lexer.tokenize lexbuf
// print the given Jennisys program
if tracing then
printfn "---------- Given Jennisys program ----------"
- Print prog
+ Print sprog
else ()
+ match TypeCheck sprog with
+ | None -> () // errors have already been reported
+ | Some(prog) ->
+ if analyzing then
+ // output a Dafny program with the constraints to be solved
+ Analyze prog
+ else ()
// that's it
if tracing then printfn "----------" else ()
with
@@ -42,14 +51,14 @@ let readAndProcess tracing (filename: string) = | ex ->
printfn "Unhandled Exception: %s" ex.Message
-let rec start n (args: string []) tracing filename =
+let rec start n (args: string []) tracing analyzing 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
+ start (n+1) args (tracing || arg = "/trace") (analyzing && arg <> "/noAnalysis") filename
else
- readAndProcess tracing filename
+ readAndProcess tracing analyzing filename
let args = Environment.GetCommandLineArgs()
-start 1 args false null
+start 1 args false true null
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj index 372b8703..09e829eb 100644 --- a/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys.fsproj @@ -57,6 +57,8 @@ <OtherFlags>--unicode</OtherFlags>
</FsLex>
<Compile Include="Printer.fs" />
+ <Compile Include="TypeChecker.fs" />
+ <Compile Include="Analyzer.fs" />
<Compile Include="Jennisys.fs" />
</ItemGroup>
<ItemGroup>
diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy index 91f7e5d5..e9a0b2c4 100644 --- a/Jennisys/Parser.fsy +++ b/Jennisys/Parser.fsy @@ -32,14 +32,14 @@ let rec MyFold ee acc = // This is the type of the data produced by a successful reduction of the 'start'
// symbol:
-%type < Ast.Program > start
+%type < Ast.SyntacticProgram > 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: TopLevelDecls EOF { Program($1) }
+start: TopLevelDecls EOF { SProgram($1) }
TopLevelDecls:
| { [] }
diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs index eea67588..21193c96 100644 --- a/Jennisys/Printer.fs +++ b/Jennisys/Printer.fs @@ -110,4 +110,4 @@ let PrintDecl d = let Print prog =
match prog with
- | Program(decls) -> List.iter PrintDecl decls
+ | SProgram(decls) -> List.iter PrintDecl decls
diff --git a/Jennisys/TypeChecker.fs b/Jennisys/TypeChecker.fs new file mode 100644 index 00000000..c9e5f308 --- /dev/null +++ b/Jennisys/TypeChecker.fs @@ -0,0 +1,26 @@ +module TypeChecker
+
+open Ast
+open System.Collections.Generic
+
+let GetClass name decls =
+ match decls |> List.tryFind (function Class(_,_,_) -> true | _ -> false) with
+ | Some(cl) -> cl
+ | None -> Class(name,[],[])
+
+let GetModel name decls =
+ match decls |> List.tryFind (function Model(_,_,_,_,_) -> true | _ -> false) with
+ | Some(m) -> m
+ | None -> Model(name,[],[],[],IdLiteral("true"))
+
+let GetCode name decls =
+ match decls |> List.tryFind (function Code(_,_) -> true | _ -> false) with
+ | Some(c) -> c
+ | None -> Code(name,[])
+
+let TypeCheck prog =
+ match prog with
+ | SProgram(decls) ->
+ let componentNames = decls |> List.choose (function Class(name,_,_) -> Some(name) | _ -> None)
+ let clist = componentNames |> List.map (fun name -> Component(GetClass name decls, GetModel name decls, GetCode name decls))
+ Some(Program(clist))
|