From 4c3d68142ca387c0cac5da85a6d3710455a5efe2 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 11 Apr 2011 19:46:44 -0700 Subject: Jennisys: First cut of injectivity analysis --- Jennisys/Jennisys/Analyzer.fs | 92 +++++++++++++++++++++++++++++++++++++++ Jennisys/Jennisys/Ast.fs | 8 +++- Jennisys/Jennisys/Jennisys.fs | 25 +++++++---- Jennisys/Jennisys/Jennisys.fsproj | 2 + Jennisys/Jennisys/Parser.fsy | 4 +- Jennisys/Jennisys/Printer.fs | 2 +- Jennisys/Jennisys/TypeChecker.fs | 26 +++++++++++ 7 files changed, 147 insertions(+), 12 deletions(-) create mode 100644 Jennisys/Jennisys/Analyzer.fs create mode 100644 Jennisys/Jennisys/TypeChecker.fs (limited to 'Jennisys') diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs new file mode 100644 index 00000000..9b7e28ca --- /dev/null +++ b/Jennisys/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/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs index 2c2610ce..fa2db0d9 100644 --- a/Jennisys/Jennisys/Ast.fs +++ b/Jennisys/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/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs index d266a065..b248cf67 100644 --- a/Jennisys/Jennisys/Jennisys.fs +++ b/Jennisys/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.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/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj index 372b8703..09e829eb 100644 --- a/Jennisys/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys/Jennisys.fsproj @@ -57,6 +57,8 @@ --unicode + + diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy index 91f7e5d5..e9a0b2c4 100644 --- a/Jennisys/Jennisys/Parser.fsy +++ b/Jennisys/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/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs index eea67588..21193c96 100644 --- a/Jennisys/Jennisys/Printer.fs +++ b/Jennisys/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/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs new file mode 100644 index 00000000..c9e5f308 --- /dev/null +++ b/Jennisys/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)) -- cgit v1.2.3