diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-07-06 15:40:48 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-07-06 15:40:48 -0700 |
| commit | 728dce3c4c11205ee0eabbc5df166eab261d501f (patch) | |
| tree | f8c06033e715ae7265a30e50ffae7c990b317d2a | |
| parent | feafae60495fd982a94d70323452232b7e3dfce4 (diff) | |
| parent | a4f4e0ba9b1a333e8fefdfe292e18abc305edcd2 (diff) | |
Merge
31 files changed, 2341 insertions, 357 deletions
diff --git a/BCT/BCT.sln b/BCT/BCT.sln index c822a0bb..24c51236 100644 --- a/BCT/BCT.sln +++ b/BCT/BCT.sln @@ -42,6 +42,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractExtractor", "..\..\ EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Microsoft.Contracts", "..\..\CCICodePlex\Ast\Metadata\Sources\Microsoft.Contracts\Microsoft.Contracts.csproj", "{B114E5FF-F2A2-4BE7-8AF1-936FC87030F0}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "mscorlibStub", "mscorlibStub\mscorlibStub.csproj", "{962CB683-8B50-4246-854C-E48D74F733B8}"
+EndProject
Global
GlobalSection(TestCaseManagementSettings) = postSolution
CategoryFile = BCT.vsmdi
@@ -247,6 +249,18 @@ Global {B114E5FF-F2A2-4BE7-8AF1-936FC87030F0}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU
{B114E5FF-F2A2-4BE7-8AF1-936FC87030F0}.Release|Any CPU.ActiveCfg = Release|Any CPU
{B114E5FF-F2A2-4BE7-8AF1-936FC87030F0}.Release|Any CPU.Build.0 = Release|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.CompilerOnly|Any CPU.ActiveCfg = Release|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.CompilerOnly|Any CPU.Build.0 = Release|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.FastpathSim|Any CPU.ActiveCfg = Release|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.FastpathSim|Any CPU.Build.0 = Release|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {962CB683-8B50-4246-854C-E48D74F733B8}.Release|Any CPU.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index c187444f..1bbcc198 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -343,7 +343,7 @@ namespace BytecodeTranslator { }
decl.AddAttribute(attrName, args);
}
- } catch (InvalidCastException e) {
+ } catch (InvalidCastException) {
Console.WriteLine("Warning: Cannot translate custom attributes for method\n '{0}':",
MemberHelper.GetMethodSignature(method, NameFormattingOptions.None));
Console.WriteLine(" >>Skipping attributes, continuing with method translation");
diff --git a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py new file mode 100644 index 00000000..4686e574 --- /dev/null +++ b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py @@ -0,0 +1,152 @@ +import sys
+import getopt
+import os
+from xml.dom import minidom
+import xml.dom
+
+CONTROL_NAMES= ["Button", "CheckBox", "RadioButton"]
+
+# TODO maybe a control is enabled but its parent is not, must take this into account
+# TODO a possible solution is to tie the enabled value to that of the parent in the app until it is either overriden
+# TODO (by directly manipulating the control's enabled value) or the parent becomes enabled
+
+CONTAINER_CONTROL_NAMES= ["Canvas", "Grid", "StackPanel"]
+
+staticControlsMap= {}
+
+def showUsage():
+ print "PhoneControlsExtractor -- extract control information from phone application pages"
+ print "Usage:"
+ print "\tPhoneControlsExtractor --pages <application_directory> --output <info_output_file>\n"
+ print "Options:"
+ print "\t--pages <application_directory>: point to location of .xaml files detailing pages. Short form: -p"
+ print "\t--output <info_output_file>: file to write with control info. Short form: -o\n"
+
+def isPageFile(file):
+ # not the best way, find out the actual exceptions
+ try:
+ minidom.parse(file)
+ file.seek(0)
+ return True
+ except Exception:
+ return False
+
+def removeBlankElements(xmlNode):
+ blankNodes= []
+ for child in xmlNode.childNodes:
+ if child.nodeType == xml.dom.Node.TEXT_NODE and child.data.strip() == "":
+ blankNodes.append(child)
+ elif child.hasChildNodes():
+ removeBlankElements(child)
+
+ for node in blankNodes:
+ node.parentNode.removeChild(node)
+ node.unlink()
+
+def getControlNodes(xmlNode):
+ controlNodes= []
+ if (xmlNode.nodeType == xml.dom.Node.ELEMENT_NODE and xmlNode.localName in CONTROL_NAMES):
+ controlNodes.insert(0,xmlNode)
+
+ for child in xmlNode.childNodes:
+ controlNodes= controlNodes + getControlNodes(child)
+
+ return controlNodes
+
+def addControlToMap(parentPage, controlNode):
+ pageControls=[]
+ newControl={}
+ try:
+ pageControls= staticControlsMap[parentPage]
+ except KeyError:
+ pass
+
+ newControl["Type"]= controlNode.localName
+ newControl["Name"]= controlNode.getAttribute("Name")
+ if (controlNode.hasAttribute("IsEnabled")):
+ newControl["IsEnabled"]= controlNode.getAttribute("IsEnabled")
+ else:
+ newControl["IsEnabled"]= "true"
+
+ if (controlNode.hasAttribute("Visibility")):
+ newControl["Visibility"]= controlNode.getAttribute("Visibility")
+ else:
+ newControl["Visibility"]= "Visible"
+
+ # TODO it is possible that more events are of interest, we should add as we discover them in existing applications
+ newControl["Click"] = controlNode.getAttribute("Click")
+ newControl["Checked"] = controlNode.getAttribute("Checked")
+ newControl["Unchecked"] = controlNode.getAttribute("Unchecked")
+ pageControls.append(newControl)
+ staticControlsMap[parentPage]= pageControls
+
+def extractPhoneControlsFromPage(pageFile):
+ # maybe it is not a page file
+ if not isPageFile(pageFile):
+ return
+
+ pageFileXML= minidom.parse(pageFile)
+ removeBlankElements(pageFileXML)
+ controls= getControlNodes(pageFileXML)
+ for control in controls:
+ ownerPage=""
+ parent= control
+ while not parent == None:
+ a=""
+ if parent.localName == "PhoneApplicationPage":
+ ownerPage= parent.getAttribute("x:Class")
+ parent= parent.parentNode
+ addControlToMap(ownerPage, control)
+
+def outputPhoneControls(outputFileName):
+ outputFile= open(outputFileName, "w")
+
+ # Output format is one line per
+ # <pageClassName>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>#
+ for page in staticControlsMap.keys():
+ for control in staticControlsMap[page]:
+ isEnabled= control["IsEnabled"]
+ visibility= control["Visibility"]
+ click= control["Click"]
+ checked= control["Checked"]
+ unchecked= control["Unchecked"]
+ outputFile.write(page + "," + control["Type"] + "," + control["Name"] + "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + "#\n")
+
+ outputFile.close()
+
+def extractPhoneControls(sourceDir):
+ fileList= [os.path.normcase(fileName) for fileName in os.listdir(sourceDir)]
+ fileList= [os.path.join(sourceDir, fileName) for fileName in fileList if os.path.splitext(fileName)[1] == ".xaml"]
+ for fileName in fileList:
+ pageFile= open(fileName, "r")
+ extractPhoneControlsFromPage(pageFile)
+ pageFile.close()
+
+ # TODO dump controls into a config file that can be passed to BCT
+
+def main():
+ pagesDir= ""
+ outputFile= ""
+ try:
+ opts, args= getopt.getopt(sys.argv[1:], "p:o:", ["pages=","output="])
+ except geopt.error, msg:
+ print msg
+ showUsage()
+ sys.exit(2)
+
+ if not len(opts) == 2:
+ print "Missing options"
+ showUsage()
+ sys.exit(2)
+
+ for o, a in opts:
+ if o in ["-p","--pages"]:
+ pagesDir= a
+ if o in ["-o", "--output"]:
+ outputFile= a
+
+ extractPhoneControls(pagesDir)
+ outputPhoneControls(outputFile)
+
+if __name__ == "__main__":
+ main()
\ No newline at end of file diff --git a/Jennisys/Jennisys.sln b/Jennisys/Jennisys.sln index 77ebb8e2..bb45d27c 100644 --- a/Jennisys/Jennisys.sln +++ b/Jennisys/Jennisys.sln @@ -2,17 +2,73 @@ Microsoft Visual Studio Solution File, Format Version 11.00
# Visual Studio 2010
Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Jennisys", "Jennisys\Jennisys.fsproj", "{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}"
+ ProjectSection(ProjectDependencies) = postProject
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} = {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C} = {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}
+ EndProjectSection
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\Source\Model\Model.csproj", "{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ModelViewer", "..\Source\ModelViewer\ModelViewer.csproj", "{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}"
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
+ Checked|Any CPU = Checked|Any CPU
+ Checked|Mixed Platforms = Checked|Mixed Platforms
+ Checked|x86 = Checked|x86
+ Debug|Any CPU = Debug|Any CPU
+ Debug|Mixed Platforms = Debug|Mixed Platforms
Debug|x86 = Debug|x86
+ Release|Any CPU = Release|Any CPU
+ Release|Mixed Platforms = Release|Mixed Platforms
Release|x86 = Release|x86
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|Any CPU.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|Mixed Platforms.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|Mixed Platforms.Build.0 = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|x86.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Checked|x86.Build.0 = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|Any CPU.ActiveCfg = Debug|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|Mixed Platforms.Build.0 = Debug|x86
{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|x86.ActiveCfg = Debug|x86
{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Debug|x86.Build.0 = Debug|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|Any CPU.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|Mixed Platforms.ActiveCfg = Release|x86
+ {F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|Mixed Platforms.Build.0 = Release|x86
{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|x86.ActiveCfg = Release|x86
{F2FF4B3A-2FE8-474A-88DF-6950F7D78908}.Release|x86.Build.0 = Release|x86
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Any CPU.Build.0 = Release|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Release|x86.ActiveCfg = Release|Any CPU
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Any CPU.ActiveCfg = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.ActiveCfg = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.Build.0 = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.ActiveCfg = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.Build.0 = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Any CPU.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.Build.0 = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.Build.0 = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Any CPU.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.Build.0 = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.Build.0 = Release|x86
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs index 5e66f5f2..244b50b4 100644 --- a/Jennisys/Jennisys/Analyzer.fs +++ b/Jennisys/Jennisys/Analyzer.fs @@ -1,134 +1,295 @@ -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 VarsAreDifferent aa bb =
- printf "false"
- List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb
-
-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 rec PrintStmt stmt indent =
- match stmt with
- | Block(stmts) ->
- Indent indent ; printfn "{"
- PrintStmtList stmts (indent + 2)
- Indent indent ; printfn "}"
- | Assign(lhs,rhs) -> Indent indent ; PrintExpr 0 lhs ; printf " := " ; PrintExpr 0 rhs ; printfn ";"
-and PrintStmtList stmts indent =
- stmts |> List.iter (fun s -> PrintStmt s indent)
-
-let GenerateCode methodName signature pre stmts inv assumeInvInitially =
- printfn " method %s()" methodName
- printfn " modifies this;"
- printfn " {"
- if assumeInvInitially then
- // assume invariant
- printf " assume " ; PrintExpr 0 inv ; printfn ";"
- else ()
- // print signature as local variables
- match signature with
- | Sig(ins,outs) ->
- List.concat [ins; outs] |> List.iter (fun vd -> printf " var " ; PrintVarDecl vd ; printfn ";")
- // assume preconditions
- printf " assume " ; PrintExpr 0 pre ; printfn ";"
- // do statements
- stmts |> List.iter (fun s -> PrintStmt s 4)
- // assume invariant
- printf " assume " ; PrintExpr 0 inv ; printfn ";"
- // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible
- printfn " assert false;"
- printfn "}"
-
-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 [aVars; 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: original abstract fields plus two more copies thereof, plus and concrete fields
- 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 " ; VarsAreDifferent aVars0 aVars1 ; printfn ";"
- printf " assume " ; PrintExpr 0 inv0 ; printfn ";"
- printf " assume " ; PrintExpr 0 inv1 ; printfn ";"
- printfn " assert false;" // {:msg "Two abstract states map to the same concrete state"}
- printfn " }"
- // generate code
- members |> List.iter (function
- | Constructor(methodName,signature,pre,stmts) -> GenerateCode methodName signature pre stmts inv false
- | Method(methodName,signature,pre,stmts) -> GenerateCode methodName signature pre stmts inv true
- | _ -> ())
- // the end of the class
- printfn "}"
- | _ -> assert false // unexpected case
-
-let Analyze prog =
- match prog with
- | Program(components) ->
- components |> List.iter AnalyzeComponent
+module Analyzer + +open Ast +open AstUtils +open CodeGen +open DafnyModelUtils +open PipelineUtils +open Options +open Printer +open Resolver +open DafnyPrinter +open Utils + +open Microsoft.Boogie + +let VarsAreDifferent aa bb = + printf "false" + List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb + +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 GenMethodAnalysisCode comp methodName signature pre post assertion = + " method " + methodName + "()" + newline + + " modifies this;" + newline + + " {" + newline + + // print signature as local variables + (match signature with + | Sig(ins,outs) -> + List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf " var %s;" (PrintVarDecl vd)) + newline) "") + + " // assume precondition" + newline + + " assume " + (PrintExpr 0 pre) + ";" + newline + + " // assume invariant and postcondition" + newline + + " assume Valid();" + newline + + " assume " + (PrintExpr 0 post) + ";" + newline + + " // assume user defined invariant again because assuming Valid() doesn't always work" + newline + + (GetInvariantsAsList comp |> PrintSep newline (fun e -> " assume " + (PrintExpr 0 e) + ";")) + newline + + // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible + " // assert false to search for a model satisfying the assumed constraints" + newline + + " assert " + (PrintExpr 0 assertion) + ";" + newline + + " }" + newline + +let MethodAnalysisPrinter onlyForThisCompMethod assertion comp mthd = + match onlyForThisCompMethod with + | (c,m) when c = comp && m = mthd -> + match m with + | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode comp methodName sign pre post assertion) + newline + | _ -> "" + | _ -> "" + +let rec IsArgsOnly args expr = + match expr with + | IdLiteral(id) -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false) + | UnaryExpr(_,e) -> IsArgsOnly args e + | BinaryExpr(_,_,e1,e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) + | Dot(e,_) -> IsArgsOnly args e + | SelectExpr(e1, e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) + | UpdateExpr(e1, e2, e3) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) && (IsArgsOnly args e3) + | SequenceExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true + | SeqLength(e) -> IsArgsOnly args e + | ForallExpr(vars,e) -> IsArgsOnly (List.concat [args; vars]) e + | IntLiteral(_) -> true + | Star -> true + +let rec GetUnifications expr args (heap,env,ctx) = + match expr with + | IntLiteral(_) + | IdLiteral(_) + | Star + | Dot(_) + | SelectExpr(_) // TODO: handle select expr + | UpdateExpr(_) // TODO: handle update expr + | SequenceExpr(_) + | SeqLength(_) + | ForallExpr(_) // TODO: handle forall expr + | UnaryExpr(_) -> Set.empty + | BinaryExpr(strength,op,e0,e1) -> + if op = "=" then + let v0 = Eval e0 (heap,env,ctx) + let v1 = Eval e1 (heap,env,ctx) + let argsOnly0 = IsArgsOnly args e0 + let argsOnly1 = IsArgsOnly args e1 + match v0,argsOnly1,argsOnly0,v1 with + | Some(c0),true,_,_ -> + Logger.DebugLine (" - adding unification " + (PrintConst c0) + " <--> " + (PrintExpr 0 e1)); + Set.ofList [c0, e1] + | _,_,true,Some(c1) -> + Logger.DebugLine (" - adding unification " + (PrintConst c1) + " <--> " + (PrintExpr 0 e0)); + Set.ofList [c1, e0] + | _ -> Logger.TraceLine (" - couldn't unify anything from " + (PrintExpr 0 expr)); + Set.empty + else + GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx)) + +let rec GetArgValueUnifications args env = + match args with + | Var(name,_) :: rest -> + match Map.tryFind (VarConst(name)) env with + | Some(c) -> + Logger.DebugLine (" - adding unification " + (PrintConst c) + " <--> " + name); + Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env) + | None -> failwith ("couldn't find value for argument " + name) + | [] -> Set.empty + +let rec _GetObjRefExpr o (heap,env,ctx) visited = + if Set.contains o visited then + None + else + let newVisited = Set.add o visited + let refName = PrintObjRefName o (env,ctx) + match refName with + | Exact "this" _ -> Some(IdLiteral(refName)) + | _ -> + let rec __fff lst = + match lst with + | ((o,Var(fldName,_)),l) :: rest -> + match _GetObjRefExpr o (heap,env,ctx) newVisited with + | Some(expr) -> Some(Dot(expr, fldName)) + | None -> __fff rest + | [] -> None + let backPointers = heap |> Map.filter (fun (_,_) l -> l = o) |> Map.toList + __fff backPointers + +let GetObjRefExpr o (heap,env,ctx) = + _GetObjRefExpr o (heap,env,ctx) (Set.empty) + +let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) = + match unifs with + | (c,e) :: rest -> + let restHeap,env,ctx = UpdateHeapEnv prog comp mthd rest (heap,env,ctx) + let newHeap = restHeap |> Map.fold (fun acc (o,f) l -> + let value = Resolve l (env,ctx) + if value = c then + let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from this to " + (PrintObjRefName o (env,ctx))) + let fldName = PrintVarName f + let assertionExpr = BinaryEq (Dot(objRefExpr, fldName)) e + // check if the assertion follows and if so update the env + let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr) + Logger.Debug(" - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ") + let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd)) + if ok then + Logger.DebugLine " HOLDS" + // change the value to expression + acc |> Map.add (o,f) (ExprConst(e)) + else + Logger.DebugLine " DOESN'T HOLDS" + // don't change the value + acc |> Map.add (o,f) l + else + // see if it's a list, then try to match its elements + match value with + | SeqConst(clist) -> acc |> Map.add (o,f) l //TODO!! + | _ -> + // leave it as is + acc |> Map.add (o,f) l + ) restHeap + (newHeap,env,ctx) + | [] -> (heap,env,ctx) + +let GeneralizeSolution prog comp mthd (heap,env,ctx) = + match mthd with + | Method(mName,Sig(ins, outs),pre,post,_) -> + let args = List.concat [ins; outs] + match args with + | [] -> (heap,env,ctx) + | _ -> + let unifs = GetUnifications (BinaryAnd pre post) args (heap,env,ctx) + |> Set.union (GetArgValueUnifications args env) + UpdateHeapEnv prog comp mthd (Set.toList unifs) (heap,env,ctx) + | _ -> failwith ("not a method: " + mthd.ToString()) + +// ==================================================================================== +/// Returns whether the code synthesized for the given method can be verified with Dafny +// ==================================================================================== +let VerifySolution prog comp mthd (heap,env,ctx) = + // print the solution to file and try to verify it with Dafny + let solution = Map.empty |> Map.add (comp,mthd) (heap,env,ctx) + let code = PrintImplCode prog solution (fun p -> [comp,mthd]) + CheckDafnyProgram code dafnyVerifySuffix + +// ============================================================================ +/// Attempts to synthesize the initialization code for the given constructor "m"
+///
+/// Returns a (heap,env,ctx) tuple +// ============================================================================ +let AnalyzeConstructor prog comp m = + let methodName = GetMethodName m + // generate Dafny code for analysis first + let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m) FalseLiteral) + Logger.InfoLine (" [*] analyzing constructor " + methodName + (PrintSig (GetMethodSig m)))
+ Logger.Info " - searching for a solution ..." + let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m)) + if models.Count = 0 then + // no models means that the "assert false" was verified, which means that the spec is inconsistent + Logger.WarnLine " !!! SPEC IS INCONSISTENT !!!" + None + else + if models.Count > 1 then + Logger.WarnLine " FAILED " + failwith "internal error (more than one model for a single constructor analysis)" + Logger.InfoLine " OK " + let model = models.[0] + let heap,env,ctx = ReadFieldValuesFromModel model prog comp m + |> GeneralizeSolution prog comp m + if _opt_verifySolutions then + Logger.InfoLine " - verifying synthesized solution ... " + let verified = VerifySolution prog comp m (heap,env,ctx) + Logger.Info " " + if verified then + Logger.InfoLine "~~~ VERIFIED ~~~" + Some(heap,env,ctx) + else + Logger.InfoLine "!!! NOT VERIFIED !!!" + Some(heap,env,ctx) + else + Some(heap,env,ctx) + + +// ============================================================================ +/// Goes through a given list of methods of the given program and attempts to +/// synthesize code for each one of them. +/// +/// Returns a map from (component * method) |--> (heap,env,ctx) +// ============================================================================ +let rec AnalyzeMethods prog members = + match members with + | (comp,m) :: rest -> + match m with + | Method(_,_,_,_,true) -> + let solOpt = AnalyzeConstructor prog comp m + Logger.InfoLine "" + match solOpt with + | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx) + | None -> AnalyzeMethods prog rest + | _ -> AnalyzeMethods prog rest + | [] -> Map.empty + +let Analyze prog = + let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog) + use file = System.IO.File.CreateText(dafnySynthFile) + file.AutoFlush <- true + Logger.InfoLine "Printing synthesized code" + let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze + fprintfn file "%s" synthCode + () + +//let AnalyzeComponent_rustan 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 [aVars; 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 "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp)) +// printfn " {" +// // the fields: original abstract fields plus two more copies thereof, plus and concrete fields +// allVars |> List.iter (function Var(nm,None) -> printfn " var %s;" nm | Var(nm,Some(tp)) -> printfn " var %s: %s;" nm (PrintType tp)) +// // the method +// printfn " method %s_checkInjective() {" name +// printf " assume " ; (VarsAreDifferent aVars0 aVars1) ; printfn ";" +// printfn " assume %s;" (PrintExpr 0 inv0) +// printfn " assume %s;" (PrintExpr 0 inv1) +// printfn " assert false;" // {:msg "Two abstract states map to the same concrete state"} +// printfn " }" +// // generate code +// members |> List.iter (function +// | Constructor(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv false) +// | Method(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv true) +// | _ -> ()) +// // the end of the class +// printfn "}" +// | _ -> assert false // unexpected case
\ No newline at end of file diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs index fa2db0d9..bd66e688 100644 --- a/Jennisys/Jennisys/Ast.fs +++ b/Jennisys/Jennisys/Ast.fs @@ -1,17 +1,26 @@ -namespace Ast
+/// The AST of a Jennisy program
+///
+/// author: Rustan Leino (leino@microsoft.com)
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+
+namespace Ast
+
open System
open System.Numerics
-
type Type =
+ | IntType
+ | BoolType
+ | SetType of Type (* type parameter *)
+ | SeqType of Type (* type parameter *)
| NamedType of string
- | InstantiatedType of string * Type
+ | InstantiatedType of string * Type (* type parameter *)
type VarDecl =
| Var of string * Type option
type Expr =
- | IntLiteral of BigInteger
+ | IntLiteral of int
| IdLiteral of string
| Star
| Dot of Expr * string
@@ -28,16 +37,16 @@ type Stmt = | Assign of Expr * Expr
type Signature =
- | Sig of VarDecl list * VarDecl list
+ | Sig of (* ins *) VarDecl list * (* outs *) VarDecl list
type Member =
| Field of VarDecl
- | Constructor of string * Signature * Expr * Stmt list
- | Method of string * Signature * Expr * Stmt list
+ | Method of (* name *) string * Signature * (* pre *) Expr * (* post *) Expr * (* isConstructor *) bool
+ | Invariant of Expr list
type TopLevelDecl =
| Class of string * string list * Member list
- | Model of string * string list * VarDecl list * Expr list * Expr
+ | Model of string * string list * VarDecl list * (* frame *) Expr list * (* invariant *) Expr
| Code of string * string list
type SyntacticProgram =
@@ -48,3 +57,15 @@ type Component = type Program =
| Program of Component list
+
+type Const =
+ | IntConst of int
+ | BoolConst of bool
+ | SetConst of Set<Const option>
+ | SeqConst of (Const option) list
+ | NullConst
+ | ThisConst of (* loc id *) string * Type option
+ | NewObj of (* loc id *) string * Type option
+ | ExprConst of Expr
+ | VarConst of (* varName *) string
+ | Unresolved of (* loc id *) string
\ No newline at end of file diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs new file mode 100644 index 00000000..442dfe57 --- /dev/null +++ b/Jennisys/Jennisys/AstUtils.fs @@ -0,0 +1,459 @@ +/// Utility functions for manipulating AST elements
+///
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+
+module AstUtils
+
+open Ast
+open Utils
+
+// ------------------------------- Visitor Stuff -------------------------------------------
+
+let rec VisitExpr visitorFunc expr acc =
+ match expr with + | IntLiteral(_) + | IdLiteral(_) + | Star -> acc |> visitorFunc expr + | Dot(e, _) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e + | SelectExpr(e1, e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 + | UpdateExpr(e1, e2, e3) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3 + | SequenceExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc) + | SeqLength(e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e + | ForallExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e + | UnaryExpr(_,e) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e + | BinaryExpr(_,_,e1,e2) -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2
+
+// ------------------------------- End Visitor Stuff -------------------------------------------
+
+exception EvalFailed
+
+let rec EvalSym expr =
+ match expr with + | IntLiteral(n) -> IntConst(n) + | IdLiteral(id) -> VarConst(id) + | Dot(e, str) -> + match EvalSym e with + | VarConst(lhsName) -> VarConst(lhsName + "." + str) + | _ -> ExprConst(expr) + | SeqLength(e) -> + match EvalSym e with + | SeqConst(clist) -> IntConst(List.length clist) + | _ -> ExprConst(expr) + | SequenceExpr(elist) -> + let clist = elist |> List.fold (fun acc e -> EvalSym e :: acc) [] |> List.rev |> Utils.ConvertToOptionList + SeqConst(clist) + | SelectExpr(lst, idx) -> + match EvalSym lst, EvalSym idx with + | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption + | _ -> ExprConst(expr) + | UpdateExpr(lst,idx,v) -> + match EvalSym lst, EvalSym idx, EvalSym v with + | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (Some(c)) clist) + | _ -> ExprConst(expr) + | BinaryExpr(_,op,e1,e2) -> + match op with + | Exact "=" _ -> + match EvalSym e1, EvalSym e2 with + | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) + | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2) + | VarConst(v1), VarConst(v2) -> BoolConst(v1 = v2) + | _ -> ExprConst(expr) + | Exact "!=" _ -> + match EvalSym e1, EvalSym e2 with + | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2)) + | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2)) + | VarConst(v1), VarConst(v2) -> BoolConst(not (v1 = v2)) + | _ -> ExprConst(expr) + | Exact "<" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2)) + | _ -> ExprConst(expr) + | Exact "<=" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2)) + | _ -> ExprConst(expr) + | Exact ">" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2)) + | _ -> ExprConst(expr) + | Exact ">=" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2) + | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2)) + | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2)) + | _ -> ExprConst(expr) + | Exact "in" _ -> + match EvalSym e1, EvalSym e2 with + | _ as c, SetConst(s) -> BoolConst(Set.contains (Some(c)) s) + | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains (Some(c)) s) + | _ -> ExprConst(expr) + | Exact "!in" _ -> + match EvalSym e1, EvalSym e2 with + | _ as c, SetConst(s) -> BoolConst(not (Set.contains (Some(c)) s)) + | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains (Some(c)) s)) + | _ -> ExprConst(expr) + | Exact "+" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) + | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) + | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) + | _ -> ExprConst(expr) + | Exact "-" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) + | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2) + | _ -> ExprConst(expr) + | Exact "*" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2) + | _ -> ExprConst(expr) + | Exact "div" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2) + | _ -> ExprConst(expr) + | Exact "mod" _ -> + match EvalSym e1, EvalSym e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2) + | _ -> ExprConst(expr) + | _ -> ExprConst(expr) + | UnaryExpr(op, e) -> + match op with + | Exact "!" _ -> + match EvalSym e with + | BoolConst(b) -> BoolConst(not b) + | _ -> ExprConst(expr) + | Exact "-" _ -> + match EvalSym e with + | IntConst(n) -> IntConst(-n) + | _ -> ExprConst(expr) + | _ -> ExprConst(expr) + | _ -> ExprConst(expr)
+
+//TODO: stuff might be missing
+let rec EvalToConst expr =
+ match expr with + | IntLiteral(n) -> IntConst(n) + | IdLiteral(id) -> raise EvalFailed //VarConst(id) + | Dot(e, str) -> raise EvalFailed + | SeqLength(e) -> + match EvalToConst e with + | SeqConst(clist) -> IntConst(List.length clist) + | _ -> raise EvalFailed + | SequenceExpr(elist) -> + let clist = elist |> List.fold (fun acc e -> EvalToConst e :: acc) [] |> List.rev |> Utils.ConvertToOptionList + SeqConst(clist) + | SelectExpr(lst, idx) -> + match EvalToConst lst, EvalToConst idx with + | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption + | _ -> raise EvalFailed + | UpdateExpr(lst,idx,v) -> + match EvalToConst lst, EvalToConst idx, EvalToConst v with + | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (Some(c)) clist) + | _ -> raise EvalFailed + | BinaryExpr(_,op,e1,e2) -> + match op with + | Exact "=" _ -> + try + BoolConst(EvalToBool(e1) = EvalToBool(e2)) + with + | EvalFailed -> BoolConst(EvalToInt(e1) = EvalToInt(e2)) + | Exact "!=" _ -> + try + BoolConst(not(EvalToBool(e1) = EvalToBool(e2))) + with + | EvalFailed -> BoolConst(not(EvalToInt e1 = EvalToInt e2)) + | Exact "<" _ -> BoolConst(EvalToInt e1 < EvalToInt e2) //TODO sets, seqs + | Exact "<=" _ -> BoolConst(EvalToInt e1 <= EvalToInt e2) //TODO sets, seqs + | Exact ">" _ -> BoolConst(EvalToInt e1 > EvalToInt e2) //TODO sets, seqs + | Exact ">=" _ -> BoolConst(EvalToInt e1 >= EvalToInt e2) //TODO sets, seqs + | Exact "in" _ -> raise EvalFailed //TODO + | Exact "!in" _ -> raise EvalFailed //TODO + | Exact "+" _ -> + match EvalToConst e1, EvalToConst e2 with + | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) + | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) + | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) + | _ -> raise EvalFailed + | Exact "-" _ -> IntConst(EvalToInt e1 - EvalToInt e2) + | Exact "*" _ -> IntConst(EvalToInt e1 * EvalToInt e2) + | Exact "div" _ -> IntConst(EvalToInt e1 / EvalToInt e2) + | Exact "mod" _ -> IntConst(EvalToInt e1 % EvalToInt e2) + | _ -> raise EvalFailed + | UnaryExpr(op, e) -> + match op with + | Exact "!" _ -> BoolConst(not (EvalToBool e)) + | Exact "-" _ -> IntConst(-(EvalToInt e)) + | _ -> raise EvalFailed + | _ -> raise EvalFailed +and EvalToBool e = + let c = EvalToConst e + match c with + | BoolConst(b) -> b + | _ -> raise EvalFailed +and EvalToInt e = + let c = EvalToConst e + match c with + | IntConst(n) -> n + | _ -> raise EvalFailed + +let rec Const2Expr c =
+ match c with
+ | IntConst(n) -> IntLiteral(n)
+ | BoolConst(b) -> if b then IntLiteral(1) else IntLiteral(0) //?? BoolLiteral(b)
+ | SeqConst(clist) ->
+ let expList = clist |> List.fold (fun acc c -> Const2Expr (Utils.ExtractOption c) :: acc) [] |> List.rev
+ SequenceExpr(expList)
+ | ThisConst(_) -> IdLiteral("this")
+ | VarConst(v) -> IdLiteral(v)
+ | NullConst -> IdLiteral("null")
+ | ExprConst(e) -> e
+ | _ -> failwith "not implemented or not supported"
+
+// =======================================================================
+/// Returns a binary AND of the two given expressions with short-circuiting
+// =======================================================================
+let BinaryAnd (lhs: Expr) (rhs: Expr) =
+ match lhs, rhs with
+ | IdLiteral("true"), _ -> rhs
+ | IdLiteral("false"), _ -> IdLiteral("false")
+ | _, IdLiteral("true") -> lhs
+ | _, IdLiteral("false") -> IdLiteral("false")
+ | _, _ -> BinaryExpr(30, "&&", lhs, rhs)
+
+// =======================================================================
+/// Returns a binary OR of the two given expressions with short-circuiting
+// =======================================================================
+let BinaryOr (lhs: Expr) (rhs: Expr) =
+ match lhs, rhs with
+ | IdLiteral("true"), _ -> IdLiteral("true")
+ | IdLiteral("false"), _ -> rhs
+ | _, IdLiteral("true") -> IdLiteral("true")
+ | _, IdLiteral("false") -> lhs
+ | _, _ -> BinaryExpr(30, "||", lhs, rhs)
+
+// ===================================================================================
+/// Returns a binary IMPLIES of the two given expressions (TODO: with short-circuiting)
+// ===================================================================================
+let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)
+
+// =================================================
+/// Returns a binary NEQ of the two given expressions
+// =================================================
+let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)
+
+// =================================================
+/// Returns a binary EQ of the two given expressions
+// =================================================
+let BinaryEq lhs rhs = BinaryExpr(40, "=", lhs, rhs)
+
+// =====================
+/// Returns TRUE literal
+// =====================
+let TrueLiteral = IdLiteral("true")
+
+// =====================
+/// Returns FALSE literal
+// =====================
+let FalseLiteral = IdLiteral("false")
+
+// ==========================================
+/// Splits "expr" into a list of its conjuncts
+// ========================================== +let rec SplitIntoConjunts expr = + match expr with + | IdLiteral("true") -> [] + | BinaryExpr(_,"&&",e0,e1) -> List.concat [SplitIntoConjunts e0 ; SplitIntoConjunts e1] + | _ -> [expr] + +// ====================================== +/// Applies "f" to each conjunct of "expr" +// ====================================== +let rec ForeachConjunct f expr = + SplitIntoConjunts expr |> List.fold (fun acc e -> acc + (f e)) ""
+
+// --- search functions ---
+
+// =========================================================
+/// Out of all "members" returns only those that are "Field"s
+// ========================================================= +let FilterFieldMembers members = + members |> List.choose (function Field(vd) -> Some(vd) | _ -> None) + +// ============================================================= +/// Out of all "members" returns only those that are constructors +// ============================================================= +let FilterConstructorMembers members = + members |> List.choose (function Method(_,_,_,_, true) as m -> Some(m) | _ -> None) + +// ============================================================= +/// Out of all "members" returns only those that are +/// constructors and have at least one input parameter +// ============================================================= +let FilterConstructorMembersWithParams members = + members |> List.choose (function Method(_,Sig(ins,outs),_,_, true) as m when not (List.isEmpty ins) -> Some(m) | _ -> None) + +// ========================================================== +/// Out of all "members" returns only those that are "Method"s +// ========================================================== +let FilterMethodMembers members = + members |> List.choose (function Method(_,_,_,_,_) as m -> Some(m) | _ -> None) + +// ======================================================================= +/// Returns all members of the program "prog" that pass the filter "filter" +// ======================================================================= +let FilterMembers prog filter = + match prog with + | Program(components) -> + components |> List.fold (fun acc comp -> + match comp with + | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))] + | _ -> acc) []
+
+// =================================
+/// Returns all fields of a component
+// =================================
+let GetAllFields comp =
+ match comp with + | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) -> + let aVars = FilterFieldMembers members + List.concat [aVars ; cVars]
+ | _ -> []
+
+// =================================
+/// Returns class name of a component
+// =================================
+let GetClassName comp =
+ match comp with
+ | Component(Class(name,_,_),_,_) -> name
+ | _ -> failwith ("unrecognized component: " + comp.ToString())
+
+// ========================
+/// Returns name of a method
+// ========================
+let GetMethodName mthd =
+ match mthd with
+ | Method(name,_,_,_,_) -> name
+ | _ -> failwith ("not a method: " + mthd.ToString())
+
+// ===========================================================
+/// Returns full name of a method (= <class_name>.<method_name>
+// ===========================================================
+let GetMethodFullName comp mthd =
+ (GetClassName comp) + "." + (GetMethodName mthd)
+
+// =============================
+/// Returns signature of a method
+// =============================
+let GetMethodSig mthd =
+ match mthd with
+ | Method(_,sgn,_,_,_) -> sgn
+ | _ -> failwith ("not a method: " + mthd.ToString())
+
+// =========================================================
+/// Returns all arguments of a method (both input and output)
+// =========================================================
+let GetMethodArgs mthd =
+ match mthd with
+ | Method(_,Sig(ins, outs),_,_,_) -> List.concat [ins; outs]
+ | _ -> failwith ("not a method: " + mthd.ToString())
+
+// ==============================================================
+/// Returns all invariants of a component as a list of expressions
+// ==============================================================
+let GetInvariantsAsList comp =
+ match comp with
+ | Component(Class(_,_,members), Model(_,_,_,_,inv), _) ->
+ let clsInvs = members |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat
+ List.append (SplitIntoConjunts inv) clsInvs
+ | _ -> failwith ("unexpected kinf of component: %s" + comp.ToString())
+
+// ==================================
+/// Returns all members of a component
+// ==================================
+let GetMembers comp =
+ match comp with
+ | Component(Class(_,_,members),_,_) -> members
+ | _ -> failwith ("unrecognized component: " + comp.ToString())
+
+// ====================================================
+/// Finds a component of a program that has a given name
+// ====================================================
+let FindComponent (prog: Program) clsName =
+ match prog with
+ | Program(comps) -> comps |> List.filter (function Component(Class(name,_,_),_,_) when name = clsName -> true | _ -> false)
+ |> Utils.ListToOption
+
+// ===================================================
+/// Finds a method of a component that has a given name
+// ===================================================
+let FindMethod comp methodName =
+ let x = GetMembers comp
+ let y = x |> FilterMethodMembers
+ let z = y |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)
+ GetMembers comp |> FilterMethodMembers |> List.filter (function Method(name,_,_,_,_) when name = methodName -> true | _ -> false)
+ |> Utils.ListToOption
+
+// ==============================================
+/// Finds a field of a class that has a given name
+// ==============================================
+let FindVar (prog: Program) clsName fldName =
+ let copt = FindComponent prog clsName
+ match copt with
+ | Some(comp) ->
+ GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)
+ |> Utils.ListToOption
+ | None -> None
+
+// ==========================================================
+/// Desugars a given expression so that all list constructors
+/// are expanded into explicit assignments to indexed elements
+// ==========================================================
+let rec Desugar expr =
+ match expr with + | IntLiteral(_) + | IdLiteral(_) + | Star + | Dot(_) + | SelectExpr(_) + | SeqLength(_) -> expr + | UpdateExpr(_) -> expr //TODO + | SequenceExpr(exs) -> expr //TODO + | ForallExpr(v,e) -> ForallExpr(v, Desugar e) + | UnaryExpr(op,e) -> UnaryExpr(op, Desugar e) + | BinaryExpr(p,op,e1,e2) ->
+ let be = BinaryExpr(p, op, Desugar e1, Desugar e2)
+ try
+ match op with
+ | Exact "=" _ ->
+ match EvalSym e1, EvalSym e2 with
+ | VarConst(v), SeqConst(clist)
+ | SeqConst(clist), VarConst(v) ->
+ let rec __fff lst cnt =
+ match lst with
+ | fs :: rest -> BinaryEq (SelectExpr(IdLiteral(v), IntLiteral(cnt))) (Const2Expr (Utils.ExtractOption clist.[cnt])) :: __fff rest (cnt+1)
+ | [] -> []
+ __fff clist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
+ | SeqConst(cl1), SeqConst(cl2) ->
+ let rec __fff lst1 lst2 cnt =
+ match lst1, lst2 with
+ | fs1 :: rest1, fs2 :: rest2 -> BinaryEq (Const2Expr (Utils.ExtractOption cl1.[cnt])) (Const2Expr (Utils.ExtractOption cl2.[cnt])) :: __fff rest1 rest2 (cnt+1)
+ | [], [] -> []
+ | _ -> failwith "Lists are of different sizes"
+ __fff cl1 cl2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be
+ | _ -> be
+ | _ -> be
+ with
+ | EvalFailed as ex -> (* printfn "%s" (ex.StackTrace.ToString()); *) be
+
+
+let rec DesugarLst exprLst =
+ match exprLst with
+ | expr :: rest -> Desugar expr :: DesugarLst rest
+ | [] -> []
+
diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs new file mode 100644 index 00000000..7e61ec7e --- /dev/null +++ b/Jennisys/Jennisys/CodeGen.fs @@ -0,0 +1,160 @@ +module CodeGen
+
+open Ast
+open AstUtils
+open Utils +open Printer
+open Resolver
+open TypeChecker
+open DafnyPrinter
+
+let numLoopUnrolls = 2
+
+let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr =
+ if numUnrolls = 0 then
+ TrueLiteral
+ else
+ BinaryImplies (BinaryNeq fldExpr (IdLiteral("null")))
+ (BinaryAnd (Dot(fldExpr, validFunName))
+ (GetUnrolledFieldValidExpr (Dot(fldExpr, fldName)) fldName validFunName (numUnrolls-1)))
+
+let GetFieldValidExpr fldName validFunName numUnrolls : Expr = + GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls + //BinaryImplies (BinaryNeq (IdLiteral(fldName)) (IdLiteral("null"))) (Dot(IdLiteral(fldName), validFunName)) + +let GetFieldsForValidExpr allFields prog : VarDecl list = + allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true + | _ -> false) + +let GetFieldsValidExprList clsName allFields prog : Expr list = + let fields = GetFieldsForValidExpr allFields prog + fields |> List.map (function Var(name, t) -> + let validFunName, numUnrolls = + match t with + | Some(ty) when clsName = (PrintType ty) -> "Valid_self()", numLoopUnrolls + | _ -> "Valid()", 1 + GetFieldValidExpr name validFunName numUnrolls + ) + +let PrintValidFunctionCode comp prog : string = + let clsName = GetClassName comp + let vars = GetAllFields comp + let allInvs = GetInvariantsAsList comp + let fieldsValid = GetFieldsValidExprList clsName vars prog + let idt = " " + let PrintInvs invs = + invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) [] + |> PrintSep (" &&" + newline) (fun e -> sprintf "%s(%s)" idt (PrintExpr 0 e)) + |> fun s -> if s = "" then (idt + "true") else s + // TODO: don't hardcode decr vars!!! +// let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then +// ["list"] +// else +// [] +// (if List.isEmpty decrVars then "" else sprintf " decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) + + " function Valid_self(): bool" + newline + + " reads *;" + newline + + " {" + newline + + (PrintInvs allInvs) + newline + + " }" + newline + + newline + + " function Valid(): bool" + newline + + " reads *;" + newline + + " {" + newline + + " this.Valid_self() &&" + newline + + (PrintInvs fieldsValid) + newline + + " }" + newline
+
+let PrintDafnyCodeSkeleton prog methodPrinterFunc: string = + match prog with + | Program(components) -> components |> List.fold (fun acc comp -> + match comp with + | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) as comp -> + let aVars = FilterFieldMembers members + let allVars = List.concat [aVars ; cVars]; + let compMethods = FilterConstructorMembers members + // Now print it as a Dafny program + acc + + (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline + + // the fields: original abstract fields plus concrete fields + (sprintf "%s" (PrintFields aVars 2 true)) + newline + + (sprintf "%s" (PrintFields cVars 2 false)) + newline + + // generate the Valid function + (sprintf "%s" (PrintValidFunctionCode comp prog)) + newline + + // call the method printer function on all methods of this component + (compMethods |> List.fold (fun acc m -> acc + (methodPrinterFunc comp m)) "") + + // the end of the class + "}" + newline + newline + | _ -> assert false; "") ""
+
+let PrintAllocNewObjects (heap,env,ctx) indent = + let idt = Indent indent + env |> Map.fold (fun acc l v -> + match v with + | NewObj(_,_) -> acc |> Set.add v + | _ -> acc + ) Set.empty + |> Set.fold (fun acc newObjConst -> + match newObjConst with + | NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline) + | _ -> failwith ("NewObj doesn't have a type: " + newObjConst.ToString()) + ) "" + +let PrintObjRefName o (env,ctx) = + match Resolve o (env,ctx) with + | ThisConst(_,_) -> "this"; + | NewObj(name, _) -> PrintGenSym name + | _ -> failwith ("unresolved object ref: " + o.ToString()) + +let PrintVarAssignments (heap,env,ctx) indent = + let idt = Indent indent + heap |> Map.fold (fun acc (o,f) l -> + let objRef = PrintObjRefName o (env,ctx) + let fldName = PrintVarName f + let value = Resolve l (env,ctx) |> PrintConst + acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline + ) "" + +let PrintHeapCreationCode (heap,env,ctx) indent = + (PrintAllocNewObjects (heap,env,ctx) indent) + + (PrintVarAssignments (heap,env,ctx) indent) + +let GenConstructorCode mthd body = + let validExpr = IdLiteral("Valid()"); + match mthd with + | Method(methodName, sign, pre, post, _) -> + let preExpr = BinaryAnd validExpr pre + let postExpr = BinaryAnd validExpr post + let PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";") + " method " + methodName + (PrintSig sign) + newline + + " modifies this;" + newline + + (PrintPrePost " requires " preExpr) + newline + + (PrintPrePost " ensures " postExpr) + newline + + " {" + newline + + body + + " }" + newline + | _ -> "" + +// NOTE: insert here coto to say which methods to analyze +let GetMethodsToAnalyze prog = + (* exactly one *) +// let c = FindComponent prog "IntList" |> Utils.ExtractOption +// let m = FindMethod c "Sum" |> Utils.ExtractOption +// [c, m] + (* all *) + FilterMembers prog FilterConstructorMembers + (* only with parameters *) +// FilterMembers prog FilterConstructorMembersWithParams + +// solutions: (comp, constructor) |--> (heap, env, ctx) +let PrintImplCode prog solutions methodsToPrintFunc = + let methods = methodsToPrintFunc prog + PrintDafnyCodeSkeleton prog (fun comp mthd -> + if Utils.ListContains (comp,mthd) methods then + let mthdBody = match Map.tryFind (comp,mthd) solutions with + | Some(heap,env,ctx) -> PrintHeapCreationCode (heap,env,ctx) 4 + | _ -> " //unable to synthesize" + newline + (GenConstructorCode mthd mthdBody) + newline + else + "" + )
\ No newline at end of file diff --git a/Jennisys/Jennisys/DafnyModelUtils.fs b/Jennisys/Jennisys/DafnyModelUtils.fs new file mode 100644 index 00000000..6e78dc33 --- /dev/null +++ b/Jennisys/Jennisys/DafnyModelUtils.fs @@ -0,0 +1,250 @@ +module DafnyModelUtils
+
+(*
+ The heap maps objects and fields to locations.
+ heap: Const * VarDecl option |--> Const
+
+ The environment maps locations to values (except that it can also
+ be locations to locations, because not all values are explicitly
+ present in the model.
+ envMap: Const |--> Const
+
+ The context is just a list of equality constraints collected on the way
+ ctx: Set<Set<Const>>, where the inner set contains exactly two constants
+*)
+
+open Ast
+open AstUtils
+open Utils
+
+open Microsoft.Boogie
+
+/// special object ref constant that will hold method argument values
+let argsObjRefConst = Unresolved("*0")
+
+let GetElemFullName (elem: Model.Element) =
+ elem.Names |> Seq.filter (fun ft -> ft.Func.Arity = 0) + |> Seq.choose (fun ft -> Some(ft.Func.Name)) + |> Utils.SeqToOption
+
+let GetElemName (elem: Model.Element) =
+ let fullNameOpt = GetElemFullName elem + match fullNameOpt with + | Some(fullName) -> + let dotIdx = fullName.LastIndexOf(".") + let fldName = fullName.Substring(dotIdx + 1) + let clsName = if dotIdx = -1 then "" else fullName.Substring(0, dotIdx)
+ Some(clsName, fldName)
+ | None -> None
+
+let GetRefName (ref: Model.Element) =
+ match ref with
+ | :? Model.Uninterpreted as uref -> uref.Name
+ | _ -> failwith ("not a ref (Uninterpreted) but: " + ref.GetType().Name)
+
+let ConvertValue (model: Model) (refVal: Model.Element) =
+ match refVal with
+ | :? Model.Number as ival -> IntConst(ival.AsInt())
+ | :? Model.Boolean as bval -> BoolConst(bval.Value)
+ | :? Model.Array as aval -> failwith "reading array values from model not implemented"
+ | :? Model.Uninterpreted as uval -> Unresolved(uval.Name) (* just a symbolic name for now, which we'll hopefully resolve later*)
+ | _ -> failwith ("unexpected model element kind: " + refVal.ToString())
+
+let GetInt (elem: Model.Element) =
+ match elem with
+ | :? Model.Number as ival -> ival.AsInt()
+ | _ -> failwith ("not an int element: " + elem.ToString())
+
+let GetBool (elem: Model.Element) =
+ match elem with
+ | :? Model.Boolean as bval -> bval.Value
+ | _ -> failwith ("not a bool element: " + elem.ToString())
+
+let GetType (e: Model.Element) =
+ let fNameOpt = GetElemFullName e
+ match fNameOpt with
+ | Some(fname) -> match fname with
+ | Exact "intType" _ -> Some(IntType)
+ | Prefix "class." clsName -> Some(NamedType(clsName))
+ | _ -> None
+ | None -> None
+
+let GetLoc (e: Model.Element) =
+ Unresolved(GetRefName e)
+
+let GetSeqFromEnv env key =
+ match Map.find key env with
+ | SeqConst(lst) -> lst
+ | _ as x-> failwith ("not a SeqConst but: " + x.ToString())
+
+let AddConstr c1 c2 ctx =
+ if c1 = c2 then
+ ctx
+ else
+ match c1, c2 with
+ | Unresolved(_), _ | _, Unresolved(_) ->
+ // find partitions
+ let s1Opt = ctx |> Set.filter (fun ss -> Set.contains c1 ss) |> Utils.SetToOption
+ let s2Opt = ctx |> Set.filter (fun ss -> Set.contains c2 ss) |> Utils.SetToOption
+ match s1Opt, s2Opt with
+ // both already exist --> so just merge them
+ | Some(s1), Some(s2) -> ctx |> Set.remove s1 |> Set.remove s2 |> Set.add (Set.union s1 s2)
+ // exactly one already exists --> add to existing
+ | Some(s1), None -> ctx |> Set.remove s1 |> Set.add (Set.add c2 s1)
+ | None, Some(s2) -> ctx |> Set.remove s2 |> Set.add (Set.add c1 s2)
+ // neither exists --> create a new one
+ | None, None -> ctx |> Set.add (Set.ofList [c1; c2])
+ | _ -> failwith ("trying to add an equality constraint between two constants: " + c1.ToString() + ", and " + c2.ToString())
+
+let rec UpdateContext lst1 lst2 ctx =
+ match lst1, lst2 with
+ | fs1 :: rest1, fs2 :: rest2 ->
+ match fs1, fs2 with
+ | Some(c1), Some(c2) -> UpdateContext rest1 rest2 (AddConstr c1 c2 ctx)
+ | _ -> UpdateContext rest1 rest2 ctx
+ | [], [] -> ctx
+ | _ -> failwith "lists are not of the same length"
+
+let UnboxIfNeeded (model: Microsoft.Boogie.Model) (e: Model.Element) =
+ let f_unbox = model.MkFunc("$Unbox", 2)
+ let unboxed = f_unbox.Apps |> Seq.filter (fun ft -> if (GetLoc ft.Args.[1]) = (GetLoc e) then true else false)
+ |> Seq.choose (fun ft -> Some(ft.Result))
+ |> Utils.SeqToOption
+ match unboxed with
+ | Some(e) -> ConvertValue model e
+ | None -> GetLoc e
+
+let ReadHeap (model: Microsoft.Boogie.Model) prog =
+ let f_heap_select = model.MkFunc("[3]", 3) + let values = f_heap_select.Apps + values |> Seq.fold (fun acc ft -> + assert (ft.Args.Length = 3) + let ref = ft.Args.[1] + let fld = ft.Args.[2] + assert (Seq.length fld.Names = 1) + let fldFullName = (Seq.nth 0 fld.Names).Func.Name + let dotIdx = fldFullName.LastIndexOf(".") + let fldName = fldFullName.Substring(dotIdx + 1) + let clsName = if dotIdx = -1 then "" else fldFullName.Substring(0, dotIdx) + let refVal = ft.Result + let refObj = Unresolved(GetRefName ref) + let fldVarOpt = FindVar prog clsName fldName + match fldVarOpt with + | Some(fldVar) -> + let fldType = match fldVar with + | Var(_,t) -> t + let fldVal = ConvertValue model refVal + acc |> Map.add (refObj, fldVar) fldVal + | None -> acc + ) Map.empty
+
+let rec ReadArgValues (model: Microsoft.Boogie.Model) args =
+ match args with
+ | Var(name,_) as v :: rest ->
+ let farg = model.Functions |> Seq.filter (fun f -> f.Arity = 0 && f.Name.StartsWith(name + "#")) |> Utils.SeqToOption
+ match farg with
+ | Some(func) ->
+ let refObj = argsObjRefConst
+ let fldVar = v
+ assert (Seq.length func.Apps = 1)
+ let ft = Seq.head func.Apps
+ let fldVal = ConvertValue model (ft.Result)
+ ReadArgValues model rest |> Map.add (VarConst(name)) fldVal
+ | None -> failwith ("cannot find corresponding function for parameter " + name)
+ | [] -> Map.empty
+
+let rec ReadSeqLen (model: Microsoft.Boogie.Model) (len_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match len_tuples with
+ | ft :: rest ->
+ let len = GetInt ft.Result
+ let emptyList = Utils.GenList len
+ let newMap = envMap |> Map.add (GetLoc ft.Args.[0]) (SeqConst(emptyList))
+ ReadSeqLen model rest (newMap,ctx)
+ | _ -> (envMap,ctx)
+
+let rec ReadSeqIndex (model: Microsoft.Boogie.Model) (idx_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match idx_tuples with
+ | ft :: rest ->
+ let srcLstKey = GetLoc ft.Args.[0]
+ let oldLst = GetSeqFromEnv envMap srcLstKey
+ let idx = GetInt ft.Args.[1]
+ let lstElem = UnboxIfNeeded model ft.Result
+ let newLst = Utils.ListSet idx (Some(lstElem)) oldLst
+ let newCtx = UpdateContext oldLst newLst ctx
+ let newEnv = envMap |> Map.add srcLstKey (SeqConst(newLst))
+ ReadSeqIndex model rest (newEnv,newCtx)
+ | _ -> (envMap,ctx)
+
+let rec ReadSeqBuild (model: Microsoft.Boogie.Model) (bld_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match bld_tuples with
+ | ft :: rest ->
+ let srcLstLoc = GetLoc ft.Args.[0]
+ let dstLstLoc = GetLoc ft.Result
+ let oldLst = GetSeqFromEnv envMap srcLstLoc
+ let idx = GetInt ft.Args.[1]
+ let lstElemVal = UnboxIfNeeded model ft.Args.[2]
+ let dstLst = GetSeqFromEnv envMap dstLstLoc
+ let newLst = Utils.ListBuild oldLst idx (Some(lstElemVal)) dstLst
+ let newCtx = UpdateContext dstLst newLst ctx
+ let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))
+ ReadSeqBuild model rest (newEnv,newCtx)
+ | _ -> (envMap,ctx)
+
+let rec ReadSeqAppend (model: Microsoft.Boogie.Model) (app_tuples: Model.FuncTuple list) (envMap,ctx) =
+ match app_tuples with
+ | ft :: rest ->
+ let srcLst1Loc = GetLoc ft.Args.[0]
+ let srcLst2Loc = GetLoc ft.Args.[1]
+ let dstLstLoc = GetLoc ft.Result
+ let oldLst1 = GetSeqFromEnv envMap srcLst1Loc
+ let oldLst2 = GetSeqFromEnv envMap srcLst2Loc
+ let dstLst = GetSeqFromEnv envMap dstLstLoc
+ let newLst = List.append oldLst1 oldLst2
+ let newCtx = UpdateContext dstLst newLst ctx
+ let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))
+ ReadSeqAppend model rest (newEnv,newCtx)
+ | _ -> (envMap,ctx)
+
+let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
+ let f_seq_len = model.MkFunc("Seq#Length", 1)
+ let f_seq_idx = model.MkFunc("Seq#Index", 2)
+ let f_seq_bld = model.MkFunc("Seq#Build", 4)
+ let f_seq_app = model.MkFunc("Seq#Append", 2)
+ (envMap,ctx) |> ReadSeqLen model (List.ofSeq f_seq_len.Apps)
+ |> ReadSeqIndex model (List.ofSeq f_seq_idx.Apps)
+ |> ReadSeqBuild model (List.ofSeq f_seq_bld.Apps)
+ |> ReadSeqAppend model (List.ofSeq f_seq_app.Apps)
+
+
+let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =
+ (envMap,ctx)
+
+let ReadNull (model: Microsoft.Boogie.Model) (envMap,ctx) =
+ let f_null = model.MkFunc("null", 0)
+ assert (f_null.AppCount = 1)
+ let e = (f_null.Apps |> Seq.nth 0).Result
+ let newEnv = envMap |> Map.add (GetLoc e) NullConst
+ (newEnv,ctx)
+
+let ReadEnv (model: Microsoft.Boogie.Model) =
+ let f_dtype = model.MkFunc("dtype", 1) + let refs = f_dtype.Apps |> Seq.choose (fun ft -> Some(ft.Args.[0]))
+ let envMap = f_dtype.Apps |> Seq.fold (fun acc ft ->
+ let locName = GetRefName ft.Args.[0]
+ let elemName = GetElemFullName ft.Args.[0]
+ let loc = Unresolved(locName)
+ let locType = GetType ft.Result
+ let value = match elemName with
+ | Some(n) when n.StartsWith("this") -> ThisConst(locName.Replace("*", ""), locType)
+ | _ -> NewObj(locName.Replace("*", ""), locType)
+ acc |> Map.add loc value
+ ) Map.empty
+ (envMap, Set.ofList([])) |> ReadNull model
+ |> ReadSeq model
+ |> ReadSet model
+
+let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth = + let heap = ReadHeap model prog + let env0,ctx = ReadEnv model + let env = env0 |> Utils.MapAddAll (ReadArgValues model (GetMethodArgs meth)) + heap,env,ctx
\ No newline at end of file diff --git a/Jennisys/Jennisys/DafnyPrinter.fs b/Jennisys/Jennisys/DafnyPrinter.fs new file mode 100644 index 00000000..87937850 --- /dev/null +++ b/Jennisys/Jennisys/DafnyPrinter.fs @@ -0,0 +1,52 @@ +module DafnyPrinter + +open Ast +open Printer + +let rec PrintType ty = + match ty with + | IntType -> "int" + | BoolType -> "bool" + | NamedType(id) -> id + | SeqType(t) -> sprintf "seq<%s>" (PrintType t) + | SetType(t) -> sprintf "set<%s>" (PrintType t) + | InstantiatedType(id,arg) -> sprintf "%s<%s>" id (PrintType arg) + +let rec PrintExpr ctx expr = + match expr with + | IntLiteral(n) -> sprintf "%O" n + | IdLiteral(id) -> id + | Star -> assert false; "" // I hope this won't happen + | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id + | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e) + | BinaryExpr(strength,op,e0,e1) -> + let op = + match op with + | "=" -> "==" + | "div" -> "/" + | "mod" -> "%" + | _ -> op + let needParens = strength <= ctx + let openParen = if needParens then "(" else "" + let closeParen = if needParens then ")" else "" + sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen + | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) + | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v) + | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0)) + | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e) + | ForallExpr(vv,e) -> + let needParens = true + let openParen = if needParens then "(" else "" + let closeParen = if needParens then ")" else "" + sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen + +let PrintTypeParams typeParams = + match typeParams with + | [] -> "" + | _ -> sprintf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp)) + +let PrintFields vars indent ghost = + let ghostStr = if ghost then "ghost " else "" + vars |> List.fold (fun acc v -> match v with + | Var(nm,None) -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline) + | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""
\ No newline at end of file diff --git a/Jennisys/Jennisys/EnvUtils.fs b/Jennisys/Jennisys/EnvUtils.fs new file mode 100644 index 00000000..0b840311 --- /dev/null +++ b/Jennisys/Jennisys/EnvUtils.fs @@ -0,0 +1,9 @@ +module EnvUtils
+
+open Ast
+
+let GetThisLoc env =
+ Map.findKey (fun k v ->
+ match v with
+ | ThisConst(_) -> true
+ | _ -> false) env
\ No newline at end of file diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs index b248cf67..0337c6a2 100644 --- a/Jennisys/Jennisys/Jennisys.fs +++ b/Jennisys/Jennisys/Jennisys.fs @@ -1,64 +1,67 @@ -// This project type requires the F# PowerPack at http://fsharppowerpack.codeplex.com/releases
-// Learn more about F# at http://fsharp.net
-// Original project template by Jomo Fisher based on work of Brian McNamara, Don Syme and Matt Valerio
-// This posting is provided "AS IS" with no warranties, and confers no rights.
-
-open System
-open System.IO
-open Microsoft.FSharp.Text.Lexing
-
-open Ast
-open Lexer
-open Parser
-open Printer
-open TypeChecker
-open Analyzer
-
-
-let readAndProcess tracing analyzing (filename: string) =
- try
- 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)
- lexbuf.EndPos <- { pos_bol = 0;
- pos_fname=if filename = null then "stdin" else filename;
- pos_cnum=0;
- pos_lnum=1 }
- try
- // parse
- let sprog = Parser.start Lexer.tokenize lexbuf
- // print the given Jennisys program
- if tracing then
- printfn "---------- Given Jennisys program ----------"
- 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
- | ex ->
- let pos = lexbuf.EndPos
- printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
-
- with
- | ex ->
- printfn "Unhandled Exception: %s" ex.Message
-
-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") (analyzing && arg <> "/noAnalysis") filename
- else
- readAndProcess tracing analyzing filename
-
-let args = Environment.GetCommandLineArgs()
-start 1 args false true null
+// This project type requires the F# PowerPack at http://fsharppowerpack.codeplex.com/releases +// Learn more about F# at http://fsharp.net +// Original project template by Jomo Fisher based on work of Brian McNamara, Don Syme and Matt Valerio +// This posting is provided "AS IS" with no warranties, and confers no rights. +module Main + +open System +open System.IO +open Microsoft.FSharp.Text.Lexing + +open Ast +open Lexer +open Parser +open Printer +open TypeChecker +open Analyzer + +let readAndProcess tracing analyzing (filename: string) = + try + 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) + lexbuf.EndPos <- { pos_bol = 0; + pos_fname=if filename = null then "stdin" else filename; + pos_cnum=0; + pos_lnum=1 } + try + // parse + let sprog = Parser.start Lexer.tokenize lexbuf + // print the given Jennisys program + if tracing then + printfn "---------- Given Jennisys program ----------" + printfn "%s" (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 + | ex -> + let pos = lexbuf.EndPos + printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message + + with + | ex -> + printfn "Unhandled Exception: %s" ex.Message + +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") (analyzing && arg <> "/noAnalysis") filename + else + readAndProcess tracing analyzing filename + +let args = Environment.GetCommandLineArgs() +try + start 1 args false true null +with + | Failure(msg) as e -> printfn "WHYYYYYYYYYYYYYYY: %s" msg; printfn "%s" e.StackTrace
\ No newline at end of file diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj index 09e829eb..39ed1aed 100644 --- a/Jennisys/Jennisys/Jennisys.fsproj +++ b/Jennisys/Jennisys/Jennisys.fsproj @@ -23,6 +23,7 @@ <WarningLevel>3</WarningLevel>
<PlatformTarget>x86</PlatformTarget>
<DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
+ <StartArguments>C:\boogie\Jennisys\Jennisys\examples\List3.jen</StartArguments>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
<DebugType>pdbonly</DebugType>
@@ -41,7 +42,11 @@ <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>
</PropertyGroup>
<ItemGroup>
+ <Compile Include="Options.fs" />
+ <Compile Include="Utils.fs" />
+ <Compile Include="PipelineUtils.fs" />
<Compile Include="Ast.fs" />
+ <Compile Include="AstUtils.fs" />
<Compile Include="$(IntermediateOutputPath)\Parser.fs">
<Visible>false</Visible>
<Link>Parser.fs</Link>
@@ -50,6 +55,8 @@ <Visible>false</Visible>
<Link>Lexer.fs</Link>
</Compile>
+ <Compile Include="DafnyModelUtils.fs" />
+ <Compile Include="EnvUtils.fs" />
<FsYacc Include="Parser.fsy">
<OtherFlags>--module Parser</OtherFlags>
</FsYacc>
@@ -57,7 +64,11 @@ <OtherFlags>--unicode</OtherFlags>
</FsLex>
<Compile Include="Printer.fs" />
+ <Compile Include="Logger.fs" />
+ <Compile Include="DafnyPrinter.fs" />
<Compile Include="TypeChecker.fs" />
+ <Compile Include="Resolver.fs" />
+ <Compile Include="CodeGen.fs" />
<Compile Include="Analyzer.fs" />
<Compile Include="Jennisys.fs" />
</ItemGroup>
@@ -71,6 +82,18 @@ <Reference Include="System.Core" />
<Reference Include="System.Numerics" />
</ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\..\Source\ModelViewer\ModelViewer.csproj">
+ <Name>ModelViewer</Name>
+ <Project>{a678c6eb-b329-46a9-bbfc-7585f01acd7c}</Project>
+ <Private>True</Private>
+ </ProjectReference>
+ <ProjectReference Include="..\..\Source\Model\Model.csproj">
+ <Name>Model</Name>
+ <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>
+ <Private>True</Private>
+ </ProjectReference>
+ </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">
diff --git a/Jennisys/Jennisys/Lexer.fsl b/Jennisys/Jennisys/Lexer.fsl index 9a1cc623..91c3239c 100644 --- a/Jennisys/Jennisys/Lexer.fsl +++ b/Jennisys/Jennisys/Lexer.fsl @@ -30,7 +30,13 @@ rule tokenize = parse | "invariant" { INVARIANT }
| "returns" { RETURNS }
| "requires" { REQUIRES }
+| "ensures" { ENSURES }
| "forall" { FORALL }
+// Types
+| "int" { INTTYPE }
+| "bool" { BOOLTYPE }
+| "seq" { SEQTYPE }
+| "set" { SETTYPE }
// Operators
| "." { DOT }
| "+" { PLUS }
@@ -64,7 +70,7 @@ rule tokenize = parse | "::" { COLONCOLON }
| "," { COMMA }
// Numberic constants
-| digit+ { INTEGER (System.Numerics.BigInteger.Parse(lexeme lexbuf)) }
+| digit+ { INTEGER (System.Convert.ToInt32(lexeme lexbuf)) }
// identifiers
| idchar+ { ID (LexBuffer<char>.LexemeString lexbuf) }
// EOF
diff --git a/Jennisys/Jennisys/Logger.fs b/Jennisys/Jennisys/Logger.fs new file mode 100644 index 00000000..bb784ba2 --- /dev/null +++ b/Jennisys/Jennisys/Logger.fs @@ -0,0 +1,39 @@ +/// Simple logging facility
+///
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+
+module Logger
+
+open Printer
+
+let _ALL = 100
+let _TRACE = 90
+let _DEBUG = 70
+let _INFO = 50
+let _WARN = 40
+let _ERROR = 20
+let _NONE = 0
+
+let logLevel = _ALL
+
+let Log level msg =
+ if logLevel >= level then
+ printf "%s" msg
+
+let LogLine level msg =
+ Log level (msg + newline)
+
+let Trace msg = Log _TRACE msg
+let TraceLine msg = LogLine _TRACE msg
+
+let Debug msg = Log _DEBUG msg
+let DebugLine msg = LogLine _DEBUG msg
+
+let Info msg = Log _INFO msg
+let InfoLine msg = LogLine _INFO msg
+
+let Warn msg = Log _WARN msg
+let WarnLine msg = LogLine _WARN msg
+
+let Error msg = Log _ERROR msg
+let ErrorLine msg = LogLine _ERROR msg
\ No newline at end of file diff --git a/Jennisys/Jennisys/Options.fs b/Jennisys/Jennisys/Options.fs new file mode 100644 index 00000000..34a0422b --- /dev/null +++ b/Jennisys/Jennisys/Options.fs @@ -0,0 +1,8 @@ +/// This module is intended to store and handle configuration options
+///
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+
+module Options
+
+/// attempt to verify synthesized code
+let _opt_verifySolutions = true
\ No newline at end of file diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy index e9a0b2c4..21e2c83e 100644 --- a/Jennisys/Jennisys/Parser.fsy +++ b/Jennisys/Jennisys/Parser.fsy @@ -1,11 +1,12 @@ %{
open Ast
+open AstUtils
let rec MyFold ee acc =
match ee with
| [] -> acc
- | x::rest -> BinaryExpr(30,"&&",x, MyFold rest acc)
+ | x::rest -> BinaryAnd (Desugar x) (MyFold rest acc)
%}
@@ -15,7 +16,7 @@ let rec MyFold ee acc = // These are the terminal tokens of the grammar along with the types of
// the data carried by each token:
%token <string> ID
-%token <System.Numerics.BigInteger> INTEGER
+%token <int> INTEGER
%token DOT
%token NOT
%token STAR DIV MOD
@@ -27,7 +28,8 @@ let rec MyFold ee acc = %token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR
%token GETS COLON COLONCOLON COMMA
%token CLASS MODEL CODE
-%token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES FORALL
+%token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL
+%token INTTYPE BOOLTYPE SEQTYPE SETTYPE
%token EOF
// This is the type of the data produced by a successful reduction of the 'start'
@@ -68,7 +70,11 @@ Signature: Pre:
| { IdLiteral "true" }
- | REQUIRES Expr Pre { BinaryExpr(30,"&&", $2, $3) }
+ | REQUIRES Expr Pre { BinaryAnd $2 $3 }
+
+Post:
+ | { IdLiteral "true" }
+ | ENSURES Expr Post { BinaryAnd $2 $3 }
StmtList:
| { [] }
@@ -83,8 +89,9 @@ BlockStmt: Member:
| VAR VarDecl { Field($2) }
- | CONSTRUCTOR ID Signature Pre StmtList { Constructor($2, $3, $4, $5) }
- | METHOD ID Signature Pre StmtList { Method($2, $3, $4, $5) }
+ | CONSTRUCTOR ID Signature Pre Post { Method($2, $3, (Desugar $4), (Desugar $5), true) }
+ | METHOD ID Signature Pre Post { Method($2, $3, (Desugar $4), (Desugar $5), false) }
+ | INVARIANT ExprList { Invariant(DesugarLst $2) }
FrameMembers:
| { [], [], IdLiteral("true") }
@@ -107,8 +114,12 @@ VarDecl: | ID COLON Type { Var($1,Some($3)) }
Type:
- | ID { NamedType($1) }
- | ID LBRACKET Type RBRACKET { InstantiatedType($1, $3) }
+ | INTTYPE { IntType }
+ | BOOLTYPE { BoolType }
+ | ID { NamedType($1) }
+ | SEQTYPE LBRACKET Type RBRACKET { SeqType($3) }
+ | SETTYPE LBRACKET Type RBRACKET { SetType($3) }
+ | ID LBRACKET Type RBRACKET { InstantiatedType($1, $3) }
ExprList:
| { [] }
@@ -128,14 +139,14 @@ Expr20: Expr30:
| Expr40 { $1 }
- | Expr40 AND Expr30and { BinaryExpr(30,"&&",$1,$3) }
- | Expr40 OR Expr30or { BinaryExpr(30,"||",$1,$3) }
+ | Expr40 AND Expr30and { BinaryAnd $1 $3 }
+ | Expr40 OR Expr30or { BinaryOr $1 $3 }
Expr30and:
| Expr40 { $1 }
- | Expr40 AND Expr30and { BinaryExpr(30,"&&",$1,$3) }
+ | Expr40 AND Expr30and { BinaryAnd $1 $3 }
Expr30or:
| Expr40 { $1 }
- | Expr40 AND Expr30or { BinaryExpr(30,"||",$1,$3) }
+ | Expr40 AND Expr30or { BinaryOr $1 $3 }
Expr40:
| Expr50 { $1 }
diff --git a/Jennisys/Jennisys/PipelineUtils.fs b/Jennisys/Jennisys/PipelineUtils.fs new file mode 100644 index 00000000..686452b6 --- /dev/null +++ b/Jennisys/Jennisys/PipelineUtils.fs @@ -0,0 +1,54 @@ +/// Utility functions for executing shell commands and
+/// running Dafny in particular
+///
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+
+module PipelineUtils
+ +let dafnyScratchSuffix = "scratch" +let dafnyVerifySuffix = "verify" +let dafnyUnifSuffix = "unif" +let dafnySynthFile = @"c:\tmp\jennisys-synth.dfy" + +let CreateEmptyModelFile modelFile = + use mfile = System.IO.File.CreateText(modelFile) + fprintf mfile "" + +// ======================================================= +/// Runs Dafny on the given "inputFile" and prints +/// the resulting model to the given "modelFile" +// ======================================================= +let RunDafny inputFile modelFile =
+ CreateEmptyModelFile modelFile
+ async {
+ use proc = new System.Diagnostics.Process()
+ proc.StartInfo.FileName <- @"c:\tmp\StartDafny-jen.bat"
+ proc.StartInfo.Arguments <- "/mv:" + modelFile + " " + inputFile
+ assert proc.Start()
+ proc.WaitForExit()
+ } |> Async.RunSynchronously
+
+// ======================================================= +/// Runs Dafny on the given "dafnyCode" and returns models +// ======================================================= +let RunDafnyProgram dafnyProgram suffix = + let inFileName = @"c:\tmp\jennisys-" + suffix + ".dfy" + let modelFileName = @"c:\tmp\jennisys-" + suffix + ".bvd" + use file = System.IO.File.CreateText(inFileName) + file.AutoFlush <- true + fprintfn file "%s" dafnyProgram + file.Close() + // run Dafny + RunDafny inFileName modelFileName + // read models from the model file + use modelFile = System.IO.File.OpenText(modelFileName) + Microsoft.Boogie.Model.ParseModels modelFile + +// ======================================================= +/// Checks whether the given dafny program verifies +// ======================================================= +let CheckDafnyProgram dafnyProgram suffix = + // TODO: also check whether Dafny produced any other errors (e.g. compilation errors, etc.) + let models = RunDafnyProgram dafnyProgram suffix + // if there are no models, verification was successful + models.Count = 0
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs index 21193c96..eb70acbd 100644 --- a/Jennisys/Jennisys/Printer.fs +++ b/Jennisys/Jennisys/Printer.fs @@ -1,113 +1,136 @@ -module Printer
-
-open Ast
-
-let rec PrintSep sep f list =
- match list with
- | [] -> ()
- | [a] -> f a
- | a :: more -> f a ; printf "%s" sep ; PrintSep sep f more
-
-let rec PrintType ty =
- match ty with
- | NamedType(id) -> printf "%s" id
- | InstantiatedType(id,arg) -> printf "%s[" id ; PrintType arg ; printf "]"
-
-let PrintVarDecl vd =
- match vd with
- | Var(id,None) -> printf "%s" id
- | Var(id,Some(ty)) -> printf "%s: " id ; PrintType ty
-
-let rec PrintExpr ctx expr =
- match expr with
- | IntLiteral(n) -> printf "%O" n
- | IdLiteral(id) -> printf "%s" id
- | Star -> printf "*"
- | Dot(e,id) -> PrintExpr 100 e ; printf ".%s" id
- | UnaryExpr(op,e) -> printf "%s" op ; PrintExpr 90 e
- | BinaryExpr(strength,op,e0,e1) ->
- 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 = ctx <> 0
- if needParens then printf "(" else ()
- printf "forall " ; vv |> PrintSep ", " PrintVarDecl ; printf " :: " ; PrintExpr 0 e
- if needParens then printf ")" else ()
-
-let PrintSig signature =
- match signature with
- | Sig(ins, outs) ->
- printf "("
- ins |> PrintSep ", " PrintVarDecl
- printf ")"
- if outs <> [] then
- printf " returns ("
- outs |> PrintSep ", " PrintVarDecl
- printf ")"
- else ()
-
-let rec ForeachConjunct f expr =
- match expr with
- | IdLiteral("true") -> ()
- | BinaryExpr(_,"&&",e0,e1) -> ForeachConjunct f e0 ; ForeachConjunct f e1
- | _ -> f expr
-
-let rec Indent i =
- if i = 0 then () else printf " " ; Indent (i-1)
-
-let rec PrintStmt stmt indent =
- match stmt with
- | Block(stmts) ->
- Indent indent ; printfn "{"
- PrintStmtList stmts (indent + 2)
- Indent indent ; printfn "}"
- | Assign(lhs,rhs) -> Indent indent ; PrintExpr 0 lhs ; printf " := " ; PrintExpr 0 rhs ; printfn ""
-and PrintStmtList stmts indent =
- stmts |> List.iter (fun s -> PrintStmt s indent)
-
-let PrintRoutine signature pre body =
- PrintSig signature
- printfn ""
- pre |> ForeachConjunct (fun e -> printf " requires " ; PrintExpr 0 e ; printfn "")
- PrintStmtList body 4
-
-let PrintMember m =
- match m with
- | Field(vd) -> printf " var " ; PrintVarDecl vd ; printfn ""
- | Constructor(id,signature,pre,body) -> printf " constructor %s" id ; PrintRoutine signature pre body
- | Method(id,signature,pre,body) -> printf " method %s" id ; PrintRoutine signature pre body
-
-let PrintTopLevelDeclHeader kind id typeParams =
- printf "%s %s" kind id
- match typeParams with
- | [] -> ()
- | _ -> printf "[" ; typeParams |> PrintSep ", " (fun tp -> printf "%s" tp) ; printf "]"
- printfn " {"
-
-let PrintDecl d =
- match d with
- | Class(id,typeParams,members) ->
- PrintTopLevelDeclHeader "class" id typeParams
- List.iter PrintMember members
- printfn "}"
- | Model(id,typeParams,vars,frame,inv) ->
- PrintTopLevelDeclHeader "model" id typeParams
- vars |> List.iter (fun vd -> printf " var " ; PrintVarDecl vd ; printfn "")
- printfn " frame"
- frame |> List.iter (fun fr -> printf " " ; PrintExpr 0 fr ; printfn "")
- printfn " invariant"
- inv |> ForeachConjunct (fun e -> printf " " ; PrintExpr 0 e ; printfn "")
- printfn "}"
- | Code(id,typeParams) ->
- PrintTopLevelDeclHeader "code" id typeParams
- printfn "}"
-
-let Print prog =
- match prog with
- | SProgram(decls) -> List.iter PrintDecl decls
+module Printer + +open Ast +open AstUtils + +let newline = System.Environment.NewLine // "\r\n" + +let PrintGenSym name = + sprintf "gensym%s" name + +let rec PrintSep sep f list = + match list with + | [] -> "" + | [a] -> f a + | a :: more -> (f a) + sep + (PrintSep sep f more) + +let rec PrintType ty = + match ty with + | IntType -> "int" + | BoolType -> "bool" + | NamedType(id) -> id + | SeqType(t) -> sprintf "seq[%s]" (PrintType t) + | SetType(t) -> sprintf "set[%s]" (PrintType t) + | InstantiatedType(id,arg) -> sprintf "%s[%s]" id (PrintType arg) + +let PrintVarDecl vd = + match vd with + | Var(id,None) -> id + | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty) + +let PrintVarName vd = + match vd with + | Var(id,_) -> id + +let rec PrintExpr ctx expr = + match expr with + | IntLiteral(n) -> sprintf "%O" n + | IdLiteral(id) -> id + | Star -> "*" + | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id + | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e) + | BinaryExpr(strength,op,e0,e1) -> + let needParens = strength <= ctx + let openParen = if needParens then "(" else "" + let closeParen = if needParens then ")" else "" + sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen + | SelectExpr(e,i) -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) + | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v) + | SequenceExpr(ee) -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0)) + | SeqLength(e) -> sprintf "|%s|" (PrintExpr 0 e) + | ForallExpr(vv,e) -> + let needParens = ctx <> 0 + let openParen = if needParens then "(" else "" + let closeParen = if needParens then ")" else "" + sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen + +let PrintSig signature = + match signature with + | Sig(ins, outs) -> + let returnClause = + if outs <> [] then sprintf " returns (%s)" (outs |> PrintSep ", " PrintVarDecl) + else "" + sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause + +let rec Indent i = + if i = 0 then "" else " " + (Indent (i-1)) + +let rec PrintStmt stmt indent = + let idt = (Indent indent) + match stmt with + | Block(stmts) -> + idt + "{" + newline + + (PrintStmtList stmts (indent + 2)) + + idt + "}" + newline + | Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline +and PrintStmtList stmts indent = + stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) "" + +let PrintRoutine signature pre body = + let preStr = pre |> ForeachConjunct (fun e -> sprintf " requires %s%s" (PrintExpr 0 e) newline) + sprintf "%s%s%s%s" (PrintSig signature) newline preStr (PrintExpr 0 body) + +let PrintMember m = + match m with + | Field(vd) -> sprintf " var %s%s" (PrintVarDecl vd) newline + | Method(id,signature,pre,body,true) -> sprintf " constructor %s%s" id (PrintRoutine signature pre body) + | Method(id,signature,pre,body,false) -> sprintf " method %s%s" id (PrintRoutine signature pre body) + | Invariant(_) -> "" // invariants are handled separately + +let PrintTopLevelDeclHeader kind id typeParams = + let typeParamStr = + match typeParams with + | [] -> "" + | _ -> sprintf "[%s]" (typeParams |> PrintSep ", " (fun tp -> tp)) + sprintf "%s %s%s {%s" kind id typeParamStr newline + +let PrintDecl d = + match d with + | Class(id,typeParams,members) -> + sprintf "%s%s}%s" (PrintTopLevelDeclHeader "class" id typeParams) + (List.fold (fun acc m -> acc + (PrintMember m)) "" members) + newline + | Model(id,typeParams,vars,frame,inv) -> + (PrintTopLevelDeclHeader "model" id typeParams) + + (vars |> List.fold (fun acc vd -> acc + " var " + (PrintVarDecl vd) + newline) "") + + " frame" + newline + + (frame |> List.fold (fun acc fr -> acc + " " + (PrintExpr 0 fr) + newline) "") + + " invariant" + newline + + (inv |> ForeachConjunct (fun e -> " " + (PrintExpr 0 e) + newline)) + + "}" + newline + | Code(id,typeParams) -> + (PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline + +let Print prog = + match prog with + | SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls + +let rec PrintConst cst = + match cst with + | IntConst(v) -> sprintf "%d" v + | BoolConst(b) -> sprintf "%b" b + | SetConst(cset) -> cset.ToString() //TODO: this won't work + | SeqConst(cseq) -> + let seqCont = cseq |> List.fold (fun acc cOpt -> + let sep = if acc = "" then "" else ", " + match cOpt with + | Some(c) -> acc + sep + (PrintConst c) + | None -> acc + sep + "null" + ) "" + sprintf "[%s]" seqCont + | NullConst -> "null" + | ThisConst(_,_) -> "this" + | NewObj(name,_) -> PrintGenSym name + | ExprConst(e) -> PrintExpr 0 e + | VarConst(name) -> name + | Unresolved(name) -> sprintf "Unresolved(%s)" name
\ No newline at end of file diff --git a/Jennisys/Jennisys/README.txt b/Jennisys/Jennisys/README.txt new file mode 100644 index 00000000..0e52dec9 --- /dev/null +++ b/Jennisys/Jennisys/README.txt @@ -0,0 +1,5 @@ +1. Installation instructions +---------------------------- + + - create c:\tmp folder + - copy the Jennisys\scripts\StartDafny-jen.bat script into c:\tmp diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs new file mode 100644 index 00000000..f1a1f67f --- /dev/null +++ b/Jennisys/Jennisys/Resolver.fs @@ -0,0 +1,78 @@ +module Resolver
+
+open Ast
+open Printer
+open EnvUtils
+
+// resolving values
+
+let rec Resolve cst (env,ctx) =
+ match cst with
+ | Unresolved(_) as u ->
+ // see if it is in the env map first
+ let envVal = Map.tryFind cst env
+ match envVal with
+ | Some(c) -> Resolve c (env,ctx)
+ | None ->
+ // not found in the env map --> check the equality sets
+ let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)
+ |> Utils.SetToOption
+ match eq with
+ | Some(eqSet) ->
+ let cOpt = eqSet |> Set.filter (function Unresolved(_) -> false | _ -> true)
+ |> Utils.SetToOption
+ match cOpt with
+ | Some(c) -> c
+ | _ -> failwith ("failed to resolve " + cst.ToString())
+ | _ -> failwith ("failed to resolve " + cst.ToString())
+ | SeqConst(cseq) ->
+ let resolvedLst = cseq |> List.rev |> List.fold (fun acc cOpt ->
+ match cOpt with
+ | Some(c) -> Some(Resolve c (env,ctx)) :: acc
+ | None -> cOpt :: acc
+ ) []
+ SeqConst(resolvedLst)
+ | SetConst(cset) ->
+ let resolvedSet = cset |> Set.fold (fun acc cOpt ->
+ match cOpt with
+ | Some(c) -> acc |> Set.add (Some(Resolve c (env,ctx)))
+ | None -> acc |> Set.add(cOpt)
+ ) Set.empty
+ SetConst(resolvedSet)
+ | _ -> cst
+
+let rec EvalUnresolved expr (heap,env,ctx) =
+ match expr with + | IntLiteral(n) -> IntConst(n) + | IdLiteral(id) when id = "this" -> GetThisLoc env + | IdLiteral(id) -> EvalUnresolved (Dot(IdLiteral("this"), id)) (heap,env,ctx) + | Dot(e, str) -> + let discr = EvalUnresolved e (heap,env,ctx) + let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList + match h2 with + | ((_,_),x) :: [] -> x + | _ :: _ -> failwithf "can't evaluate expression deterministically: %s.%s resolves to multiple locations." (PrintConst discr) str + | [] -> failwithf "can't find value for %s.%s" (PrintConst discr) str + | SelectExpr(lst, idx) -> + let lstC = Resolve (EvalUnresolved lst (heap,env,ctx)) (env,ctx) + let idxC = EvalUnresolved idx (heap,env,ctx) + match lstC, idxC with + | SeqConst(clist), IntConst(n) -> clist.[n] |> Utils.ExtractOption + | _ -> failwith "can't eval SelectExpr" + | _ -> failwith "NOT IMPLEMENTED YET" //TODO finish this! +// | Star +// | SelectExpr(_) +// | UpdateExpr(_) +// | SequenceExpr(_) +// | SeqLength(_) +// | ForallExpr(_) +// | UnaryExpr(_) +// | BinaryExpr(_) + +// TODO: can this be implemented on top of the existing AstUtils.EvalSym?? We must! +let Eval expr (heap,env,ctx) =
+ try
+ let unresolvedConst = EvalUnresolved expr (heap,env,ctx)
+ Some(Resolve unresolvedConst (env,ctx))
+ with
+ ex -> None
\ No newline at end of file diff --git a/Jennisys/Jennisys/TypeChecker.fs b/Jennisys/Jennisys/TypeChecker.fs index c9e5f308..7414f253 100644 --- a/Jennisys/Jennisys/TypeChecker.fs +++ b/Jennisys/Jennisys/TypeChecker.fs @@ -1,26 +1,39 @@ module TypeChecker
open Ast
+open Printer
open System.Collections.Generic
let GetClass name decls =
- match decls |> List.tryFind (function Class(_,_,_) -> true | _ -> false) with
+ match decls |> List.tryFind (function Class(n,_,_) when n = name -> true | _ -> false) with
| Some(cl) -> cl
| None -> Class(name,[],[])
let GetModel name decls =
- match decls |> List.tryFind (function Model(_,_,_,_,_) -> true | _ -> false) with
+ match decls |> List.tryFind (function Model(n,_,_,_,_) when n = name -> true | _ -> false) with
| Some(m) -> m
| None -> Model(name,[],[],[],IdLiteral("true"))
let GetCode name decls =
- match decls |> List.tryFind (function Code(_,_) -> true | _ -> false) with
+ match decls |> List.tryFind (function Code(n,_) when n = name -> true | _ -> false) with
| Some(c) -> c
| None -> Code(name,[])
+let IsUserType prog tpo =
+ match tpo with
+ | Some(tp) ->
+ let tpname = match tp with
+ | NamedType(tname) -> tname
+ | InstantiatedType(tname, _) -> tname
+ | _ -> ""
+ match prog with
+ | Program(components) -> components |> List.filter (function Component(Class(name,_,_),_,_) when name = tpname -> true
+ | _ -> false) |> List.isEmpty |> not
+ | None -> false
+
let TypeCheck prog =
match prog with
- | SProgram(decls) ->
+ | 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))
diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs new file mode 100644 index 00000000..3cb8fee4 --- /dev/null +++ b/Jennisys/Jennisys/Utils.fs @@ -0,0 +1,173 @@ +/// Various utility functions
+///
+/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
+
+module Utils
+
+// -------------------------------------------
+// ----------- collection util funcs ---------
+// -------------------------------------------
+
+// =====================================
+/// requres: x = Some(a) or failswith msg
+/// ensures: ret = a
+// =====================================
+let ExtractOptionMsg msg x =
+ match x with
+ | Some(a) -> a
+ | None -> failwith msg
+
+// ====================
+/// requres: x = Some(a)
+/// ensures: ret = a
+// ====================
+let ExtractOption x =
+ ExtractOptionMsg "can't extract anything from a None" x
+
+// =============================
+/// requres: List.length lst <= 1
+/// ensures: if |lst| = 0 then
+/// ret = None
+/// else
+/// ret = Some(lst[0])
+// =============================
+let ListToOption lst =
+ if List.length lst > 1 then
+ failwith "given list contains more than one element"
+ if List.isEmpty lst then
+ None
+ else
+ Some(lst.[0])
+
+// =============================================================
+/// ensures: forall i :: 0 <= i < |lst| ==> ret[i] = Some(lst[i])
+// =============================================================
+let rec ConvertToOptionList lst =
+ match lst with
+ | fs :: rest -> Some(fs) :: ConvertToOptionList rest
+ | [] -> []
+
+// =============================
+/// requres: Seq.length seq <= 1
+/// ensures: if |seq| = 0 then
+/// ret = None
+/// else
+/// ret = Some(seq[0])
+// =============================
+let SeqToOption seq =
+ if Seq.length seq > 1 then
+ failwith "given seq contains more than one element"
+ if Seq.isEmpty seq then
+ None
+ else
+ Some(Seq.nth 0 seq)
+
+// =============================
+/// requires: Set.count set <= 1
+/// ensures: if |set| = 0 then
+/// ret = None
+/// else
+/// ret = Some(set[0])
+// =============================
+let SetToOption set =
+ if Set.count set > 1 then
+ failwith "give set contains more than one value"
+ if (Set.isEmpty set) then
+ None
+ else
+ Some(set |> Set.toList |> List.head)
+
+// ===============================================================
+/// requires: n >= 0
+/// ensures: |ret| = n && forall i :: 0 <= i < n ==> ret[i] = None
+// ===============================================================
+let rec GenList n =
+ if n < 0 then
+ failwith "n must be positive"
+ if n = 0 then
+ []
+ else
+ None :: (GenList (n-1))
+
+// ==========================
+/// ensures: ret = elem in lst
+// ==========================
+let ListContains elem lst =
+ lst |> List.exists (fun e -> e = elem)
+
+// ===============================================================
+/// ensures: |ret| = max(|lst| - cnt, 0)
+/// ensures: forall i :: cnt <= i < |lst| ==> ret[i] = lst[i-cnt]
+// ===============================================================
+let rec ListSkip cnt lst =
+ if cnt = 0 then
+ lst
+ else
+ match lst with
+ | fs :: rest -> ListSkip (cnt-1) rest
+ | [] -> []
+
+// ===============================================================
+/// ensures: forall i :: 0 <= i < max(|srcList|, |dstList|) ==>
+/// if i = idx then
+/// ret[i] = v
+/// elif i < |srcList| then
+/// ret[i] = srcList[i]
+/// else
+/// ret[i] = dstList[i]
+// ===============================================================
+let rec ListBuild srcList idx v dstList =
+ match srcList, dstList with
+ | fs1 :: rest1, fs2 :: rest2 -> if idx = 0 then
+ v :: List.concat [rest1 ; ListSkip (List.length rest1) rest2]
+ else
+ fs1 :: ListBuild rest1 (idx-1) v rest2
+ | [], fs2 :: rest2 -> if idx = 0 then
+ v :: rest2
+ else
+ fs2 :: ListBuild [] (idx-1) v rest2
+ | _, [] -> failwith "index out of range"
+
+// =======================================
+/// ensures: forall i :: 0 <= i < |lst| ==>
+/// if i = idx then
+/// ret[i] = v
+/// else
+/// ret[i] = lst[i]
+// =======================================
+let rec ListSet idx v lst =
+ match lst with
+ | fs :: rest -> if idx = 0 then
+ v :: rest
+ else
+ fs :: ListSet (idx-1) v rest
+ | [] -> failwith "index out of range"
+
+// =======================================
+/// ensures: forall k,v ::
+/// if k,v in map2 then
+// k,v in ret
+/// elif k,v in map1 then
+/// k,v in ret
+/// else
+/// k,v !in ret
+// =======================================
+let rec MapAddAll map1 map2 =
+ map2 |> Map.fold (fun acc k v -> acc |> Map.add k v) map1
+
+// -------------------------------------------
+// ------ string active patterns -------------
+// -------------------------------------------
+
+let (|Prefix|_|) (p:string) (s:string) =
+ if s.StartsWith(p) then
+ Some(s.Substring(p.Length))
+ else
+ None
+
+let (|Exact|_|) (p:string) (s:string) =
+ if s = p then
+ Some(s)
+ else
+ None
+
diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen new file mode 100644 index 00000000..184f4947 --- /dev/null +++ b/Jennisys/Jennisys/examples/List.jen @@ -0,0 +1,42 @@ +class List[T] { + var list: seq[T] + + constructor Empty() + ensures list = [] + + constructor Singleton(t: T) + ensures list = [t] +} + +model List[T] { + var root: Node[T] + + frame + root * root.list[*] + + invariant + (root = null) ==> (|list| = 0) + root != null ==> list = root.list +} + +class Node[T] { + var list: seq[T] + + invariant + |list| > 0 + + constructor Init(t: T) + ensures list = [t] +} + +model Node[T] { + var data: T + var next: Node[T] + + frame + data * next + + invariant + next = null <==> list = [data] + next != null ==> list = [data] + next.list +} diff --git a/Jennisys/Jennisys/examples/List2.jen b/Jennisys/Jennisys/examples/List2.jen new file mode 100644 index 00000000..e99cf342 --- /dev/null +++ b/Jennisys/Jennisys/examples/List2.jen @@ -0,0 +1,57 @@ +class IntList { + var list: seq[int] + + constructor Empty() + ensures list = [] + + constructor SingletonTwo() + ensures list = [2] + + constructor OneTwo() + ensures list = [1] + [2] + + constructor Singleton(p: int) + ensures list = [p] + + constructor TwoConsecutive(p: int) + ensures list = [p] + [p+1] + + constructor Double(p: int, q: int) + ensures list = [p] + [q] + + constructor Sum(p: int, q: int) + ensures list = [p + q] +} + +model IntList { + var root: IntNode + + frame + root * root.list[*] + + invariant + root = null <==> |list| = 0 + root != null ==> list = root.list +} + +class IntNode { + var list: seq[int] + + invariant + |list| > 0 + + constructor SingletonZero() + ensures list = [0] +} + +model IntNode { + var data: int + var next: IntNode + + frame + data * next + + invariant + next = null ==> list = [data] + next != null ==> list = [data] + next.list +} diff --git a/Jennisys/Jennisys/examples/List3.jen b/Jennisys/Jennisys/examples/List3.jen new file mode 100644 index 00000000..6bb49eb8 --- /dev/null +++ b/Jennisys/Jennisys/examples/List3.jen @@ -0,0 +1,71 @@ +class IntList { + var list: seq[int] + + constructor Empty() + ensures list = [] + + constructor SingletonTwo() + ensures list = [2] + + constructor OneTwo() + ensures list = [1] + [2] + + constructor Singleton(p: int) + ensures list = [p] + + constructor TwoConsecutive(p: int) + ensures list = [p] + [p+1] + + constructor Double(p: int, q: int) + ensures list = [p] + [q] + + constructor Sum(p: int, q: int) + ensures list = [p + q] +} + +model IntList { + var root: IntNode + + frame + root * root.list[*] + + invariant + root = null ==> |list| = 0 + root != null ==> (|list| = |root.succ| + 1 && + list[0] = root.data && + (forall i:int :: (0 <= i && i < |root.succ|) ==> (root.succ[i] != null && list[i+1] = root.succ[i].data))) +} + +class IntNode { + var succ: seq[IntNode] + var data: int + + constructor Zero() + ensures data = 0 + ensures succ = [] + + constructor OneTwo() + ensures data = 1 + ensures |succ| = 1 && succ[0] != null && succ[0].data = 2 + + constructor Init(p: int) + ensures data = p + + constructor InitInc(p: int) + ensures data = p + 1 + + + invariant + !(null in succ) +} + +model IntNode { + var next: IntNode + + frame + data * next + + invariant + next = null ==> |succ| = 0 + next != null ==> (succ = [next] + next.succ) +} diff --git a/Jennisys/Jennisys/scripts/StartDafny-jen.bat b/Jennisys/Jennisys/scripts/StartDafny-jen.bat new file mode 100644 index 00000000..79d39a38 --- /dev/null +++ b/Jennisys/Jennisys/scripts/StartDafny-jen.bat @@ -0,0 +1,3 @@ +@echo off
+"c:/boogie/Binaries/Dafny.exe" -nologo -compile:0 /print:xxx.bpl -timeLimit:60 %* > c:\tmp\jen-doo.out
+exit 43
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 780e04d9..197a603e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1806,7 +1806,7 @@ namespace Microsoft.Dafny { /// <summary>
/// Resolves the given call statement.
- /// Assumes all LHSs have already been resolved.
+ /// Assumes all LHSs have already been resolved (and checked for mutability).
/// </summary>
void ResolveCallStmt(CallStmt s, bool specContextOnly, Method method, Type receiverType) {
Contract.Requires(s != null);
@@ -1906,27 +1906,41 @@ namespace Microsoft.Dafny { var lhs = s.Lhs[i];
if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {
Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
- } else if (!specContextOnly && (s.IsGhost || callee.Outs[i].IsGhost)) {
- // LHS must denote a ghost
- lhs = lhs.Resolved;
- if (lhs is IdentifierExpr) {
- var ll = (IdentifierExpr)lhs;
- if (!ll.Var.IsGhost) {
- if (ll is AutoGhostIdentifierExpr && ll.Var is VarDecl) {
- // the variable was actually declared in this statement, so auto-declare it as ghost
- ((VarDecl)ll.Var).MakeGhost();
- } else {
- Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
+ } else {
+ var resolvedLhs = lhs.Resolved;
+ if (!specContextOnly && (s.IsGhost || callee.Outs[i].IsGhost)) {
+ // LHS must denote a ghost
+ if (resolvedLhs is IdentifierExpr) {
+ var ll = (IdentifierExpr)resolvedLhs;
+ if (!ll.Var.IsGhost) {
+ if (ll is AutoGhostIdentifierExpr && ll.Var is VarDecl) {
+ // the variable was actually declared in this statement, so auto-declare it as ghost
+ ((VarDecl)ll.Var).MakeGhost();
+ } else {
+ Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
+ }
}
+ } else if (resolvedLhs is FieldSelectExpr) {
+ var ll = (FieldSelectExpr)resolvedLhs;
+ if (!ll.Field.IsGhost) {
+ Error(s, "actual out-parameter {0} is required to be a ghost field", i);
+ }
+ } else {
+ // this is an array update, and arrays are always non-ghost
+ Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
}
- } else if (lhs is FieldSelectExpr) {
- var ll = (FieldSelectExpr)lhs;
- if (!ll.Field.IsGhost) {
- Error(s, "actual out-parameter {0} is required to be a ghost field", i);
+ }
+ // LHS must denote a mutable field.
+ if (resolvedLhs is IdentifierExpr) {
+ var ll = (IdentifierExpr)resolvedLhs;
+ if (!ll.Var.IsMutable) {
+ Error(resolvedLhs, "LHS of assignment must denote a mutable variable");
+ }
+ } else if (resolvedLhs is FieldSelectExpr) {
+ var ll = (FieldSelectExpr)resolvedLhs;
+ if (!ll.Field.IsMutable) {
+ Error(resolvedLhs, "LHS of assignment must denote a mutable field");
}
- } else {
- // this is an array update, and arrays are always non-ghost
- Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
}
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e5621773..a29c64fa 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1103,3 +1103,8 @@ Dafny program verifier finished with 16 verified, 0 errors -------------------- ChainingDisjointTests.dfy --------------------
Dafny program verifier finished with 6 verified, 0 errors
+
+-------------------- CallStmtTests.dfy --------------------
+CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
+2 resolution/type errors detected in CallStmtTests.dfy
diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy new file mode 100644 index 00000000..735efe81 --- /dev/null +++ b/Test/dafny0/CallStmtTests.dfy @@ -0,0 +1,21 @@ +
+method testing1(t: int)
+{
+ t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
+}
+
+method m() returns (r: int)
+{
+ return 3;
+}
+
+method testing2()
+{
+ var v;
+ v := m2(); // error: v needs to be ghost because r is.
+}
+
+method m2() returns (ghost r: int)
+{
+ r := 23;
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 143a0dc5..7aa1b38e 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -19,7 +19,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Termination.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
- ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy) do (
+ ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
+ CallStmtTests.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 %* %%f
|