diff options
| author |  Aleksandar Milicevic <unknown> | 2011-08-05 12:03:01 -0700 |
|---|---|---|
| committer | Aleksandar Milicevic <unknown> | 2011-08-05 12:03:01 -0700 |
| commit | ce3354c16952bcc77a6b54745d548f145614589b (patch) | |
| tree | 9b04395ae1e538d5a4fc86deec72bc5091518f9a | |
| parent | daf763dc8abb3b26e06e10ea432e3ec9688fc90e (diff) | |
| parent | 86fd6c60aea290944c89ec76c3d8a5044e88dcac (diff) | |
Merge
45 files changed, 2243 insertions, 2173 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 751d8baa..648d4c9f 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -205,11 +205,8 @@ namespace BytecodeTranslator { /// </summary>
public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
+ string fieldname = MemberHelper.GetMemberSignature(field, NameFormattingOptions.DocumentationId);
fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
- // Need to append something to the name to avoid name clashes with other members (of a different
- // type) that have the same name.
- fieldname += "$field";
Bpl.IToken tok = field.Token();
if (field.IsStatic) {
@@ -227,7 +224,7 @@ namespace BytecodeTranslator { public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
+ string fieldname = MemberHelper.GetMemberSignature(e, NameFormattingOptions.DocumentationId);
fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
Bpl.IToken tok = e.Token();
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index f6903b8a..30def4a2 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -122,7 +122,7 @@ namespace BytecodeTranslator { string fullyQualifiedName = namedTypeDef.ToString();
string xamlForClass = PhoneCodeHelper.instance().getXAMLForPage(fullyQualifiedName);
if (xamlForClass != null) { // if not it is possibly an abstract page
- string uriName = PhoneControlsPlugin.getURIBase(xamlForClass);
+ string uriName = UriHelper.getURIBase(xamlForClass);
Bpl.Constant uriConstant = sink.FindOrCreateConstant(uriName);
PhoneCodeHelper.instance().setBoogieStringPageNameForPageClass(fullyQualifiedName, uriConstant.Name);
}
@@ -223,7 +223,7 @@ namespace BytecodeTranslator { private bool sawCctor = false;
private void CreateStaticConstructor(ITypeDefinition typeDefinition) {
- var typename = TypeHelper.GetTypeName(typeDefinition);
+ var typename = TypeHelper.GetTypeName(typeDefinition, Microsoft.Cci.NameFormattingOptions.DocumentationId);
typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#cctor",
new Bpl.TypeVariableSeq(),
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs index 6be74264..cd71e7cc 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs @@ -10,6 +10,28 @@ using Microsoft.Cci.MutableCodeModel; namespace BytecodeTranslator.Phone {
public static class UriHelper {
/// <summary>
+ /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)
+ /// This method returns a base URI
+ /// </summary>
+ /// <param name="uri"></param>
+ /// <returns></returns>
+ public static string getURIBase(string uri) {
+ // I need to build an absolute URI just to call getComponents() ...
+ Uri mockBaseUri = new Uri("mock://mock/", UriKind.RelativeOrAbsolute);
+ Uri realUri;
+ try {
+ realUri = new Uri(uri, UriKind.Absolute);
+ } catch (UriFormatException) {
+ // uri string is relative
+ realUri = new Uri(mockBaseUri, uri);
+ }
+
+ string str = realUri.GetComponents(UriComponents.Path | UriComponents.StrongAuthority | UriComponents.Scheme, UriFormat.UriEscaped);
+ Uri mockStrippedUri = new Uri(str);
+ return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();
+ }
+
+ /// <summary>
/// checks if argument is locally created URI with static URI target
/// </summary>
/// <param name="arg"></param>
@@ -32,7 +54,7 @@ namespace BytecodeTranslator.Phone { if (staticURITarget == null)
return false;
- uri = staticURITarget.Value as string;
+ uri= staticURITarget.Value as string;
return true;
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs index 4d1f60fb..d79d2c00 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs @@ -31,6 +31,7 @@ namespace BytecodeTranslator.Phone { private IAssemblyReference coreAssemblyRef;
private IAssemblyReference phoneAssembly;
private IAssemblyReference phoneSystemWindowsAssembly;
+ private IAssemblyReference MSPhoneControlsAssembly;
private INamespaceTypeReference appBarIconButtonType;
private INamespaceTypeReference checkBoxType;
private INamespaceTypeReference radioButtonType;
@@ -39,6 +40,7 @@ namespace BytecodeTranslator.Phone { private INamespaceTypeReference toggleButtonType;
private INamespaceTypeReference controlType;
private INamespaceTypeReference uiElementType;
+ private INamespaceTypeReference pivotType;
private CompileTimeConstant trueConstant;
private CompileTimeConstant falseConstant;
@@ -65,6 +67,8 @@ namespace BytecodeTranslator.Phone { return checkBoxType;
} else if (classname == "ApplicationBarIconButton") {
return appBarIconButtonType;
+ } else if (classname == "Pivot") {
+ return pivotType;
} else if (classname == "DummyType") {
return Dummy.Type;
} else {
@@ -87,12 +91,17 @@ namespace BytecodeTranslator.Phone { AssemblyIdentity MSPhoneAssemblyId =
new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+ AssemblyIdentity MSPhoneControlsAssemblyId=
+ new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone.Controls"), "", new Version("7.0.0.0"),
+ new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+
AssemblyIdentity MSPhoneSystemWindowsAssemblyId =
new AssemblyIdentity(host.NameTable.GetNameFor("System.Windows"), coreAssemblyRef.Culture, coreAssemblyRef.Version,
coreAssemblyRef.PublicKeyToken, "");
phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
phoneSystemWindowsAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);
+ MSPhoneControlsAssembly= host.FindAssembly(MSPhoneControlsAssemblyId);
// TODO determine the needed types dynamically
appBarIconButtonType= platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarIconButton");
@@ -103,6 +112,7 @@ namespace BytecodeTranslator.Phone { toggleButtonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Primitives", "ToggleButton");
controlType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Control");
uiElementType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "UIElement");
+ pivotType = platform.CreateReference(MSPhoneControlsAssembly, "Microsoft", "Phone", "Controls", "Pivot");
trueConstant = new CompileTimeConstant() {
Type = platform.SystemBoolean,
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs index f94f0044..2d3533aa 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs @@ -13,6 +13,8 @@ namespace BytecodeTranslator.Phone { private ITypeReference cancelEventArgsType;
private ITypeReference typeTraversed;
private IMethodDefinition methodTraversed;
+ private static HashSet<IMethodDefinition> navCallers= new HashSet<IMethodDefinition>();
+ public static IEnumerable<IMethodDefinition> NavCallers { get { return navCallers; } }
public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed, IMethodDefinition methodTraversed) : base() {
this.host = host;
@@ -29,10 +31,13 @@ namespace BytecodeTranslator.Phone { cancelEventArgsType = platform.CreateReference(assembly, "System", "ComponentModel", "CancelEventArgs");
}
+ public override void Visit(IEnumerable<IAssemblyReference> assemblyReferences) {
+ base.Visit(assemblyReferences);
+ }
+
+
public override void Visit(IMethodDefinition method) {
if (method.IsConstructor && PhoneTypeHelper.isPhoneApplicationClass(typeTraversed, host)) {
- // TODO BUG doing this is generating a fresh variable definition somewhere that the BCT then translates into two different (identical) declarations
- // TODO maybe a bug introduced here or a BCT bug
string mainPageUri = PhoneCodeHelper.instance().PhonePlugin.getMainPageXAML();
SourceMethodBody sourceBody = method.Body as SourceMethodBody;
if (sourceBody != null) {
@@ -41,7 +46,7 @@ namespace BytecodeTranslator.Phone { Assignment uriInitAssign = new Assignment() {
Source = new CompileTimeConstant() {
Type = host.PlatformType.SystemString,
- Value = PhoneControlsPlugin.getURIBase(mainPageUri),
+ Value = UriHelper.getURIBase(mainPageUri),
},
Type = host.PlatformType.SystemString,
Target = new TargetExpression() {
@@ -78,10 +83,13 @@ namespace BytecodeTranslator.Phone { navCallFound = false;
navCallIsStatic = false;
this.Visit(statement);
- if (navCallFound && navCallIsStatic) {
- staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));
- } else if (navCallFound) {
- nonStaticNavStmts.Add(statement);
+ if (navCallFound) {
+ navCallers.Add(methodTraversed);
+ if (navCallIsStatic) {
+ staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));
+ } else {
+ nonStaticNavStmts.Add(statement);
+ }
}
}
@@ -106,6 +114,8 @@ namespace BytecodeTranslator.Phone { UriHelper.isArgumentURILocallyCreatedStaticRoot(expr, host, out target);
if (!isStatic)
target = "--Other non inferrable target--";
+ else
+ target = UriHelper.getURIBase(target);
} catch (InvalidOperationException) {
}
}
@@ -140,11 +150,13 @@ namespace BytecodeTranslator.Phone { string target;
if (isNavigationOnBackKeyPressHandler(methodCall, out target)) {
PhoneCodeHelper.instance().BackKeyPressNavigates = true;
- ICollection<string> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed];
- if (targets == null) {
+ ICollection<string> targets;
+ try {
+ targets= PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed];
+ } catch (KeyNotFoundException) {
targets = new HashSet<string>();
}
- targets.Add(target);
+ targets.Add("\"" + target + "\"");
PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed]= targets;
} else if (isCancelOnBackKeyPressHandler(methodCall)) {
PhoneCodeHelper.instance().BackKeyPressHandlerCancels = true;
@@ -247,7 +259,7 @@ namespace BytecodeTranslator.Phone { Assignment currentURIAssign = new Assignment() {
Source = new CompileTimeConstant() {
Type = host.PlatformType.SystemString,
- Value = PhoneControlsPlugin.getURIBase(entry.Item3),
+ Value = UriHelper.getURIBase(entry.Item3).ToLower(),
},
Type = host.PlatformType.SystemString,
Target = new TargetExpression() {
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 18d735af..231a21cf 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -31,6 +31,9 @@ namespace BytecodeTranslator { [OptionDescription("Break into debugger", ShortForm = "break")]
public bool breakIntoDebugger = false;
+ [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]
+ public bool captureState = false;
+
[OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
public List<string> libpaths = new List<string>();
@@ -165,16 +168,16 @@ namespace BytecodeTranslator { return result;
}
- public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options/*?*/ options, List<Regex> exemptionList, bool whiteList) {
+ public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Contract.Requires(assemblyNames != null);
Contract.Requires(heapFactory != null);
- var libPaths = options == null ? null : options.libpaths;
- var wholeProgram = options == null ? false : options.wholeProgram;
- var/*?*/ stubAssemblies = options == null ? null : options.stub;
- var phoneControlsConfigFile = options == null ? null : options.phoneControls;
- var doPhoneNav = options == null ? false : options.phoneNavigationCode;
- var doPhoneFeedback = options == null ? false : options.phoneFeedbackCode;
+ var libPaths = options.libpaths;
+ var wholeProgram = options.wholeProgram;
+ var/*?*/ stubAssemblies = options.stub;
+ var phoneControlsConfigFile = options.phoneControls;
+ var doPhoneNav = options.phoneNavigationCode;
+ var doPhoneFeedback = options.phoneFeedbackCode;
var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
Host = host;
@@ -247,7 +250,7 @@ namespace BytecodeTranslator { else
traverserFactory = new CLRSemantics();
- Sink sink= new Sink(host, traverserFactory, heapFactory, exemptionList, whiteList);
+ Sink sink= new Sink(host, traverserFactory, heapFactory, options, exemptionList, whiteList);
TranslationHelper.tmpVarCounter = 0;
MetadataTraverser translator;
translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
@@ -324,6 +327,13 @@ namespace BytecodeTranslator { System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);
}
+ if (PhoneCodeHelper.instance().PhoneNavigationToggled) {
+ // TODO integrate into the pipeline and spit out the boogie code
+ foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {
+ System.Console.WriteLine(def.ToString());
+ }
+ }
+
Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");
Prelude.Emit(writer);
sink.TranslatedProgram.Emit(writer);
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index b2c1177e..1427b836 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -27,10 +27,11 @@ namespace BytecodeTranslator { get { return this.factory; }
}
readonly TraverserFactory factory;
+ private readonly Options options;
readonly bool whiteList;
readonly List<Regex> exemptionList;
- public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, List<Regex> exemptionList, bool whiteList) {
+ public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Contract.Requires(host != null);
Contract.Requires(factory != null);
Contract.Requires(heapFactory != null);
@@ -38,6 +39,7 @@ namespace BytecodeTranslator { this.host = host;
this.factory = factory;
var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?
+ this.options = options;
this.exemptionList = exemptionList;
this.whiteList = whiteList;
if (this.TranslatedProgram == null) {
@@ -52,6 +54,8 @@ namespace BytecodeTranslator { }
}
+ public Options Options { get { return this.options; } }
+
public Heap Heap {
get { return this.heap; }
}
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 4c927b3e..015e57ce 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -54,6 +54,8 @@ namespace BytecodeTranslator public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();
private bool contractContext;
internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();
+ private bool captureState;
+ private static int captureStateCounter = 0;
#region Constructors
public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
@@ -61,6 +63,7 @@ namespace BytecodeTranslator this.factory = sink.Factory;
PdbReader = pdbReader;
this.contractContext = contractContext;
+ this.captureState = sink.Options.captureState;
}
#endregion
@@ -108,6 +111,14 @@ namespace BytecodeTranslator public override void Visit(IStatement statement) {
EmitSourceContext(statement);
+ if (this.sink.Options.captureState) {
+ var tok = statement.Token();
+ var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);
+ var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);
+ StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)
+ );
+ }
base.Visit(statement);
}
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index a17165ee..924aba5e 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -42,6 +42,7 @@ namespace BytecodeTranslator { var parameterToken = parameterDefinition.Token();
var typeToken = parameterDefinition.Type.Token();
var parameterName = TranslationHelper.TurnStringIntoValidIdentifier(parameterDefinition.Name.Value);
+ if (String.IsNullOrWhiteSpace(parameterName)) parameterName = "P" + parameterDefinition.Index.ToString();
this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);
if (parameterDefinition.IsByReference) {
@@ -154,6 +155,7 @@ namespace BytecodeTranslator { s = s.Replace('[', '$');
s = s.Replace(']', '$');
s = s.Replace('|', '$');
+ s = s.Replace('+', '$');
s = GetRidOfSurrogateCharacters(s);
return s;
}
diff --git a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py index 37b35746..2071ce21 100644 --- a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py +++ b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py @@ -5,7 +5,7 @@ from xml.dom import minidom from itertools import product
import xml.dom
-CONTROL_NAMES= ["Button", "CheckBox", "RadioButton"]
+CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton", "Pivot"]
CONTAINER_CONTROL_NAMES= ["Canvas", "Grid", "StackPanel"]
# TODO externalize strings, share with C# code
@@ -20,6 +20,8 @@ originalPageVars= [] boogiePageVars= []
boogiePageClasses= []
dummyPageVar= "dummyBoogieStringPageName"
+anonymousControlCount= 0;
+ANONYMOUS_CONTROL_PREFIX= "__BOOGIE_ANONYMOUS_CONTROL_"
def showUsage():
print "PhoneBoogieCodeGenerator -- create boilerplate code for Boogie verification of Phone apps"
@@ -29,7 +31,14 @@ def showUsage(): print "\t--controls <app_control_info_file>: Phone app control info. See PhoneControlsExtractor. Short form: -c"
print "\t--output <code_output_file>: file to write with boilerplate code. Short form: -o\n"
-def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName):
+def isAnonymousControl(control):
+ name= control["bplName"]
+ return name.find(ANONYMOUS_CONTROL_PREFIX) != -1
+
+def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName):
+ global anonymousControlCount
+ global ANONYMOUS_CONTROL_PREFIX
+
newControl={}
newControl["class"]= controlClass
newControl["enabled"]= enabled
@@ -37,6 +46,11 @@ def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickH newControl["clickHandler"]= clickHandler
newControl["checkedHandler"]= checkedHandler
newControl["uncheckedHandler"]= uncheckedHandler
+ newControl["selectionChangedHandler"]= selectionChangedHandler
+ if (bplName == ""):
+ # anonymous control, need a dummy boogie var, but we cannot know how it got initialized
+ bplName= ANONYMOUS_CONTROL_PREFIX + str(anonymousControlCount)
+ anonymousControlCount= anonymousControlCount+1
newControl["bplName"]=bplName
infoMap[controlName]= newControl
@@ -115,7 +129,7 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): for entry in staticControlsMap[originalPageName]["controls"].keys():
controlInfo= staticControlsMap[originalPageName]["controls"][entry]
if controlInfo["bplName"] == "":
- continue
+ continue;
if not ifInitialized:
file.write("\t\tif ($activeControl == " + str(activeControl) + ") {\n")
ifInitialized= True
@@ -139,6 +153,10 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): file.write("\t\t\t\tif ($handlerToActivate == 2) {\n")
file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["uncheckedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
file.write("\t\t\t\t}\n")
+ if not controlInfo["selectionChangedHandler"] == "":
+ file.write("\t\t\t\tif ($handlerToActivate == 3) {\n")
+ file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["selectionChangedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
+ file.write("\t\t\t\t}\n")
file.write("\t\t\t}\n")
file.write("\t\t}\n")
@@ -203,14 +221,14 @@ def buildControlInfo(controlInfoFileName): file = open(controlInfoFileName, "r")
# Info file format is first line containing only the main page, another line with boogie's current navigation variable and then one line per
- # <pageClassName>,<page.xaml file>,<xaml boogie string representation>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<BoogieName>
+ # <pageClassName>,<page.xaml file>,<xaml boogie string representation>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<SelectionChangedValue>,<BoogieName>
mainPageXAML= file.readline().strip()
currentNavigationVariable= file.readline().strip()
mainAppClassname= file.readline().strip()
infoLine= file.readline().strip()
while not infoLine == "":
- pageClass, pageName, pageBoogieStringName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName= infoLine.split(",")
+ pageClass, pageName, pageBoogieStringName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName= infoLine.split(",")
pageInfo={}
pageInfo["class"]=pageClass
try:
@@ -224,7 +242,7 @@ def buildControlInfo(controlInfoFileName): pageControlInfo= pageInfo["controls"]
except KeyError:
pageInfo["controls"]=pageControlInfo
- loadControlInfo(pageControlInfo, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName)
+ loadControlInfo(pageControlInfo, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName)
pageInfo["controls"]= pageControlInfo
staticControlsMap[pageName]=pageInfo
diff --git a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py index 9285d6c8..82090e29 100644 --- a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py +++ b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py @@ -4,7 +4,7 @@ import os from xml.dom import minidom
import xml.dom
-CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton"]
+CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton", "Pivot"]
# 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
@@ -70,6 +70,7 @@ def addDummyControlToMap(pageXAML, parentPage): newControl["Click"] = ""
newControl["Checked"] = ""
newControl["Unchecked"] = ""
+ newControl["SelectionChanged"]= ""
newControl["XAML"]= pageXAML
pageControls.append(newControl)
staticControlsMap[parentPage]= pageControls
@@ -98,6 +99,7 @@ def addControlToMap(pageXAML, parentPage, controlNode): newControl["Click"] = controlNode.getAttribute("Click").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)
newControl["Checked"] = controlNode.getAttribute("Checked").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)
newControl["Unchecked"] = controlNode.getAttribute("Unchecked").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)
+ newControl["SelectionChanged"] = controlNode.getAttribute("SelectionChanged").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)
newControl["XAML"]= pageXAML
pageControls.append(newControl)
staticControlsMap[parentPage]= pageControls
@@ -145,7 +147,7 @@ def outputPhoneControls(outputFileName): outputFile= open(outputFileName, "w")
# Output format is first line containing only the main page, then line containing boogie navigation variable, and then one line per
- # <pageClassName>,<page.xaml file>,<boogie string page name>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>
+ # <pageClassName>,<page.xaml file>,<boogie string page name>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<SelChangedValue>
outputFile.write(mainPageXAML + "\n")
outputFile.write("dummyNavigationVariable_unknown\n")
outputFile.write("dummyMainAppName_unknown\n") # I could possibly deduce it from WMAppManifest.xml, but I'm unsure. Doing it later is safe anyway
@@ -167,10 +169,14 @@ def outputPhoneControls(outputFileName): unchecked= control["Unchecked"]
if (unchecked.find(COMMA_REPLACEMENT) != -1):
unchecked= ""
+ selectionChanged= control["SelectionChanged"]
+ if (selectionChanged.find(COMMA_REPLACEMENT) != -1):
+ selectionChanged= ""
pageXAML= control["XAML"]
# last comma is to account for bpl translation name, that is unknown for now
# boogie string page name is unknown for now
- outputFile.write(page + "," + os.path.basename(pageXAML) + ",dummyBoogieStringPageName," + control["Type"] + "," + control["Name"] + "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + ",\n")
+ outputFile.write(page + "," + os.path.basename(pageXAML) + ",dummyBoogieStringPageName," + control["Type"] + "," + control["Name"] + \
+ "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + "," + selectionChanged + ",\n")
outputFile.close()
diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs index ac2a0b2d..6dfccde6 100644 --- a/BCT/RegressionTests/RegressionTestInput/Class1.cs +++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs @@ -190,5 +190,12 @@ namespace RegressionTestInput { }
}
}
+ public class TestForClassesDifferingOnlyInBeingGeneric {
+ public int x;
+ }
+
+ public class TestForClassesDifferingOnlyInBeingGeneric<T> {
+ public int x;
+ }
}
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index a0f72ae1..59d9be9b 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -492,7 +492,7 @@ procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, -procedure {:extern} System.Console.WriteLine$System.Double43(value$in: Real);
+procedure {:extern} System.Console.WriteLine$System.Double45(value$in: Real);
@@ -504,7 +504,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: d := d$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
- call System.Console.WriteLine$System.Double43(d);
+ call System.Console.WriteLine$System.Double45(d);
if ($Exception != null)
{
return;
@@ -597,7 +597,7 @@ procedure RegressionTestInput.RealNumbers.#ctor6($this: Ref); -procedure {:extern} System.Object.#ctor44($this: Ref);
+procedure {:extern} System.Object.#ctor46($this: Ref);
@@ -606,7 +606,7 @@ implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -617,11 +617,11 @@ implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) -procedure RegressionTestInput.RealNumbers.#cctor();
+procedure T$RegressionTestInput.RealNumbers.#cctor();
-implementation RegressionTestInput.RealNumbers.#cctor()
+implementation T$RegressionTestInput.RealNumbers.#cctor()
{
}
@@ -633,9 +633,9 @@ axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, Sys axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field: Field;
+const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field: Field;
+const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;
procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref);
@@ -647,7 +647,7 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
- $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field, Int2Box(Box2Int(Read($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field))));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
return;
}
@@ -663,9 +663,9 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($t var $localExc: Ref;
var $label: int;
- $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field, Int2Box(0));
- $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field, Int2Box(0));
- call System.Object.#ctor44($this);
+ $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0));
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -676,11 +676,11 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($t -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+procedure T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
{
}
@@ -712,9 +712,9 @@ axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type); axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type);
-const unique RegressionTestInput.S.x$field: Field;
+const unique F$RegressionTestInput.S.x: Field;
-const unique RegressionTestInput.S.b$field: Field;
+const unique F$RegressionTestInput.S.b: Field;
implementation RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref)
{
@@ -729,9 +729,9 @@ implementation RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($re assume $DynamicType($tmp0) == RegressionTestInput.S$type;
s := $tmp0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
- assert Box2Int(Read($Heap, s, RegressionTestInput.S.x$field)) == 0;
+ assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
- assert !Box2Bool(Read($Heap, s, RegressionTestInput.S.b$field));
+ assert !Box2Bool(Read($Heap, s, F$RegressionTestInput.S.b));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
$result := s;
return;
@@ -751,9 +751,9 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes s := s$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
- $Heap := Write($Heap, s, RegressionTestInput.S.x$field, Int2Box(3));
+ $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Box(3));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
- assert Box2Int(Read($Heap, s, RegressionTestInput.S.x$field)) == 3;
+ assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
$result := s;
return;
@@ -770,7 +770,7 @@ implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -781,11 +781,11 @@ implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) -procedure RegressionTestInput.CreateStruct.#cctor();
+procedure T$RegressionTestInput.CreateStruct.#cctor();
-implementation RegressionTestInput.CreateStruct.#cctor()
+implementation T$RegressionTestInput.CreateStruct.#cctor()
{
}
@@ -797,9 +797,9 @@ axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type) axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);
-var RegressionTestInput.ClassWithArrayTypes.s$field: Ref;
+var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;
-const unique RegressionTestInput.ClassWithArrayTypes.a$field: Field;
+const unique F$RegressionTestInput.ClassWithArrayTypes.a: Field;
procedure RegressionTestInput.ClassWithArrayTypes.Main112();
@@ -853,11 +853,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main213() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
call $tmp3 := Alloc();
assume $ArrayLength($tmp3) == 1 * 5;
- RegressionTestInput.ClassWithArrayTypes.s$field := $tmp3;
+ F$RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
- $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0 := Int2Box(2)]];
+ $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
- assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0]) == 2;
+ assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
call $tmp4 := Alloc();
assume $ArrayLength($tmp4) == 1 * 4;
@@ -867,7 +867,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main213() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
assert Box2Int($ArrayContents[t][0]) == 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
- assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0]) == 2;
+ assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
return;
}
@@ -888,12 +888,12 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int3214($thi x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
- $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][x := Int2Box(42)]];
+ $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Box(42)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
- $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][x + 1 := Int2Box(43)]];
+ $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Box(43)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
- _loc0 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field));
- _loc1 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field));
+ _loc0 := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
+ _loc1 := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
return;
@@ -922,7 +922,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array15 if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
{
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
- $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];
+ $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];
}
else
{
@@ -943,8 +943,8 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) var $localExc: Ref;
var $label: int;
- $Heap := Write($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field, Ref2Box(null));
- call System.Object.#ctor44($this);
+ $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null));
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -955,13 +955,52 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) -procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
+procedure T$RegressionTestInput.ClassWithArrayTypes.#cctor();
-implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
+implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor()
+{
+ F$RegressionTestInput.ClassWithArrayTypes.s := null;
+}
+
+
+
+function RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0: Type) : Type;
+
+function Child0(in: Type) : Type;
+
+axiom (forall arg0: Type :: { RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0) } Child0(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0)) == arg0);
+
+const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: Field;
+
+procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor17($this: Ref);
+
+
+
+implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor17($this: Ref)
+{
+ var $localExc: Ref;
+ var $label: int;
+
+ $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x, Int2Box(0));
+ call System.Object.#ctor46($this);
+ if ($Exception != null)
+ {
+ return;
+ }
+
+ return;
+}
+
+
+
+procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor();
+
+
+
+implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor()
{
- RegressionTestInput.ClassWithArrayTypes.s$field := null;
}
@@ -972,11 +1011,11 @@ axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);
-procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -992,11 +1031,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys -procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -1012,11 +1051,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst -procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3220($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3220($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -1032,11 +1071,11 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy -procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3221($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3221($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1050,16 +1089,16 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3 -procedure RegressionTestInput.BitwiseOperations.#ctor21($this: Ref);
+procedure RegressionTestInput.BitwiseOperations.#ctor22($this: Ref);
-implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref)
+implementation RegressionTestInput.BitwiseOperations.#ctor22($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1070,11 +1109,11 @@ implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref) -procedure RegressionTestInput.BitwiseOperations.#cctor();
+procedure T$RegressionTestInput.BitwiseOperations.#cctor();
-implementation RegressionTestInput.BitwiseOperations.#cctor()
+implementation T$RegressionTestInput.BitwiseOperations.#cctor()
{
}
@@ -1096,20 +1135,20 @@ axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type); axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);
-procedure RegressionTestInput.AsyncAttribute.#ctor22($this: Ref);
+procedure RegressionTestInput.AsyncAttribute.#ctor23($this: Ref);
-procedure {:extern} System.Attribute.#ctor45($this: Ref);
+procedure {:extern} System.Attribute.#ctor47($this: Ref);
-implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref)
+implementation RegressionTestInput.AsyncAttribute.#ctor23($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Attribute.#ctor45($this);
+ call System.Attribute.#ctor47($this);
if ($Exception != null)
{
return;
@@ -1120,11 +1159,11 @@ implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref) -procedure RegressionTestInput.AsyncAttribute.#cctor();
+procedure T$RegressionTestInput.AsyncAttribute.#cctor();
-implementation RegressionTestInput.AsyncAttribute.#cctor()
+implementation T$RegressionTestInput.AsyncAttribute.#cctor()
{
}
@@ -1136,11 +1175,11 @@ axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);
-procedure RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int);
+procedure RegressionTestInput.RefParameters.M$System.Int32$24(x$in: int) returns (x$out: int);
-implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int)
+implementation RegressionTestInput.RefParameters.M$System.Int32$24(x$in: int) returns (x$out: int)
{
var $localExc: Ref;
var $label: int;
@@ -1154,16 +1193,16 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) re -procedure RegressionTestInput.RefParameters.#ctor24($this: Ref);
+procedure RegressionTestInput.RefParameters.#ctor25($this: Ref);
-implementation RegressionTestInput.RefParameters.#ctor24($this: Ref)
+implementation RegressionTestInput.RefParameters.#ctor25($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1174,11 +1213,11 @@ implementation RegressionTestInput.RefParameters.#ctor24($this: Ref) -procedure RegressionTestInput.RefParameters.#cctor();
+procedure T$RegressionTestInput.RefParameters.#cctor();
-implementation RegressionTestInput.RefParameters.#cctor()
+implementation T$RegressionTestInput.RefParameters.#cctor()
{
}
@@ -1190,16 +1229,16 @@ axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);
-procedure RegressionTestInput.NestedGeneric.#ctor27($this: Ref);
+procedure RegressionTestInput.NestedGeneric.#ctor28($this: Ref);
-implementation RegressionTestInput.NestedGeneric.#ctor27($this: Ref)
+implementation RegressionTestInput.NestedGeneric.#ctor28($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1216,16 +1255,16 @@ axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);
-procedure RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref);
+procedure RegressionTestInput.NestedGeneric.C.#ctor27($this: Ref);
-implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref)
+implementation RegressionTestInput.NestedGeneric.C.#ctor27($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1238,11 +1277,9 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref) function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;
-function Child0(in: Type) : Type;
-
axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);
-procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int);
+procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3226($this: Ref, x$in: int);
@@ -1250,7 +1287,7 @@ procedure {:extern} System.Activator.CreateInstance``12(T: Type) returns ($resul -implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int)
+implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3226($this: Ref, x$in: int)
{
var x: int;
var CS$0$0000: Box;
@@ -1265,7 +1302,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($thi x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1299,31 +1336,31 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($thi -procedure RegressionTestInput.NestedGeneric.C.G.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.C.G`1.#cctor();
-implementation RegressionTestInput.NestedGeneric.C.G.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.C.G`1.#cctor()
{
}
-procedure RegressionTestInput.NestedGeneric.C.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.C.#cctor();
-implementation RegressionTestInput.NestedGeneric.C.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.C.#cctor()
{
}
-procedure RegressionTestInput.NestedGeneric.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.#cctor();
-implementation RegressionTestInput.NestedGeneric.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.#cctor()
{
}
@@ -1343,8 +1380,47 @@ procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref); implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref)
{
- $Heap := Write($Heap, other, RegressionTestInput.S.x$field, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.S.x$field))));
- $Heap := Write($Heap, other, RegressionTestInput.S.b$field, Bool2Box(Box2Bool(Read($Heap, this, RegressionTestInput.S.b$field))));
+ $Heap := Write($Heap, other, F$RegressionTestInput.S.x, Int2Box(Box2Int(Read($Heap, this, F$RegressionTestInput.S.x))));
+ $Heap := Write($Heap, other, F$RegressionTestInput.S.b, Bool2Box(Box2Bool(Read($Heap, this, F$RegressionTestInput.S.b))));
+}
+
+
+
+const unique RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type: Type;
+
+axiom $Subtype(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+
+axiom $DisjointSubtree(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+
+const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: Field;
+
+procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor29($this: Ref);
+
+
+
+implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor29($this: Ref)
+{
+ var $localExc: Ref;
+ var $label: int;
+
+ $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x, Int2Box(0));
+ call System.Object.#ctor46($this);
+ if ($Exception != null)
+ {
+ return;
+ }
+
+ return;
+}
+
+
+
+procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor();
+
+
+
+implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor()
+{
}
@@ -1355,13 +1431,13 @@ axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type);
-var RegressionTestInput.Class0.StaticInt$field: int;
+var F$RegressionTestInput.Class0.StaticInt: int;
-procedure RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.StaticMethod$System.Int3230(x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.StaticMethod$System.Int3230(x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1375,11 +1451,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) -procedure RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int);
+procedure RegressionTestInput.Class0.M$System.Int3231($this: Ref, x$in: int);
-implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int)
+implementation RegressionTestInput.Class0.M$System.Int3231($this: Ref, x$in: int)
{
var x: int;
var __temp_1: int;
@@ -1401,20 +1477,20 @@ implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int assert (if x == 3 then y <= 8 else false);
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
- RegressionTestInput.Class0.StaticInt$field := y;
+ F$RegressionTestInput.Class0.StaticInt := y;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
- assert y == RegressionTestInput.Class0.StaticInt$field;
+ assert y == F$RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
return;
}
-procedure RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int);
+procedure RegressionTestInput.Class0.M$System.Int32$System.Int3232($this: Ref, x$in: int, y$in: int);
-implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int)
+implementation RegressionTestInput.Class0.M$System.Int32$System.Int3232($this: Ref, x$in: int, y$in: int)
{
var x: int;
var y: int;
@@ -1429,11 +1505,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: R -procedure RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool);
+procedure RegressionTestInput.Class0.M$System.Boolean33($this: Ref, b$in: bool);
-implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool)
+implementation RegressionTestInput.Class0.M$System.Boolean33($this: Ref, b$in: bool)
{
var b: bool;
var $localExc: Ref;
@@ -1446,11 +1522,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: b -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref);
+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class034($this: Ref, c$in: Ref);
-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref)
+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class034($this: Ref, c$in: Ref)
{
var c: Ref;
var $localExc: Ref;
@@ -1463,41 +1539,41 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: -procedure RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int);
+procedure RegressionTestInput.Class0.NonVoid35($this: Ref) returns ($result: int);
-implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int)
+implementation RegressionTestInput.Class0.NonVoid35($this: Ref) returns ($result: int)
{
var $tmp8: int;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
- call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3228(3);
+ call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3230(3);
if ($Exception != null)
{
return;
}
- $result := 3 + RegressionTestInput.Class0.StaticInt$field + $tmp8;
+ $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp8;
return;
}
-procedure RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$36($this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$36($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
var $label: int;
x$out := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
- x$out := 3 + RegressionTestInput.Class0.StaticInt$field;
+ x$out := 3 + F$RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
$result := x$out;
return;
@@ -1505,11 +1581,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x -procedure RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.RefParam$System.Int32$37($this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.RefParam$System.Int32$37($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
var $label: int;
@@ -1518,7 +1594,7 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
x$out := x$out + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
- RegressionTestInput.Class0.StaticInt$field := x$out;
+ F$RegressionTestInput.Class0.StaticInt := x$out;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
$result := x$out;
return;
@@ -1526,11 +1602,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x -procedure RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.AssignToInParam$System.Int3238($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.AssignToInParam$System.Int3238($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1540,7 +1616,7 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
x := x + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
- RegressionTestInput.Class0.StaticInt$field := x;
+ F$RegressionTestInput.Class0.StaticInt := x;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
$result := x;
return;
@@ -1548,11 +1624,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int);
+procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1566,11 +1642,11 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3240($this: Ref, y$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3240($this: Ref, y$in: int) returns ($result: int)
{
var y: int;
var $tmp9: int;
@@ -1579,7 +1655,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: y := y$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this, y);
+ call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this, y);
if ($Exception != null)
{
return;
@@ -1591,16 +1667,16 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: -procedure RegressionTestInput.Class0.#ctor39($this: Ref);
+procedure RegressionTestInput.Class0.#ctor41($this: Ref);
-implementation RegressionTestInput.Class0.#ctor39($this: Ref)
+implementation RegressionTestInput.Class0.#ctor41($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1611,13 +1687,13 @@ implementation RegressionTestInput.Class0.#ctor39($this: Ref) -procedure RegressionTestInput.Class0.#cctor();
+procedure T$RegressionTestInput.Class0.#cctor();
-implementation RegressionTestInput.Class0.#cctor()
+implementation T$RegressionTestInput.Class0.#cctor()
{
- RegressionTestInput.Class0.StaticInt$field := 0;
+ F$RegressionTestInput.Class0.StaticInt := 0;
}
@@ -1628,15 +1704,15 @@ axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);
-var RegressionTestInput.ClassWithBoolTypes.staticB$field: bool;
+var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;
-const unique RegressionTestInput.ClassWithBoolTypes.b$field: Field;
+const unique F$RegressionTestInput.ClassWithBoolTypes.b: Field;
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool);
+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(x$in: int, y$in: int) returns ($result: bool);
-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool)
+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(x$in: int, y$in: int) returns ($result: bool)
{
var x: int;
var y: int;
@@ -1652,32 +1728,32 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool);
+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean43($this: Ref, z$in: bool);
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool)
+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean43($this: Ref, z$in: bool)
{
var z: bool;
var $localExc: Ref;
var $label: int;
z := z$in;
- $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b$field, Bool2Box(false));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
}
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
- $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b$field, Bool2Box(z));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
if (z)
{
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
- RegressionTestInput.ClassWithBoolTypes.staticB$field := z;
+ F$RegressionTestInput.ClassWithBoolTypes.staticB := z;
}
else
{
@@ -1688,18 +1764,18 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($th -procedure RegressionTestInput.ClassWithBoolTypes.Main42();
+procedure RegressionTestInput.ClassWithBoolTypes.Main44();
-implementation RegressionTestInput.ClassWithBoolTypes.Main42()
+implementation RegressionTestInput.ClassWithBoolTypes.Main44()
{
var $tmp10: bool;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
- call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(3, 4);
+ call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(3, 4);
if ($Exception != null)
{
return;
@@ -1711,13 +1787,13 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main42() -procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
+procedure T$RegressionTestInput.ClassWithBoolTypes.#cctor();
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
+implementation T$RegressionTestInput.ClassWithBoolTypes.#cctor()
{
- RegressionTestInput.ClassWithBoolTypes.staticB$field := false;
+ F$RegressionTestInput.ClassWithBoolTypes.staticB := false;
}
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index d2b5950a..d93b6815 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -478,7 +478,7 @@ procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, -procedure {:extern} System.Console.WriteLine$System.Double43(value$in: Real);
+procedure {:extern} System.Console.WriteLine$System.Double45(value$in: Real);
@@ -490,7 +490,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: d := d$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
- call System.Console.WriteLine$System.Double43(d);
+ call System.Console.WriteLine$System.Double45(d);
if ($Exception != null)
{
return;
@@ -583,7 +583,7 @@ procedure RegressionTestInput.RealNumbers.#ctor6($this: Ref); -procedure {:extern} System.Object.#ctor44($this: Ref);
+procedure {:extern} System.Object.#ctor46($this: Ref);
@@ -592,7 +592,7 @@ implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -603,11 +603,11 @@ implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) -procedure RegressionTestInput.RealNumbers.#cctor();
+procedure T$RegressionTestInput.RealNumbers.#cctor();
-implementation RegressionTestInput.RealNumbers.#cctor()
+implementation T$RegressionTestInput.RealNumbers.#cctor()
{
}
@@ -651,7 +651,7 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($t RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0;
RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := 0;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -662,11 +662,11 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($t -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+procedure T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
{
}
@@ -756,7 +756,7 @@ implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -767,11 +767,11 @@ implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) -procedure RegressionTestInput.CreateStruct.#cctor();
+procedure T$RegressionTestInput.CreateStruct.#cctor();
-implementation RegressionTestInput.CreateStruct.#cctor()
+implementation T$RegressionTestInput.CreateStruct.#cctor()
{
}
@@ -930,7 +930,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) var $label: int;
RegressionTestInput.ClassWithArrayTypes.a[$this] := null;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -941,28 +941,67 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) -procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
+procedure T$RegressionTestInput.ClassWithArrayTypes.#cctor();
-implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
+implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor()
{
RegressionTestInput.ClassWithArrayTypes.s := null;
}
+function RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0: Type) : Type;
+
+function Child0(in: Type) : Type;
+
+axiom (forall arg0: Type :: { RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0) } Child0(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0)) == arg0);
+
+var RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int;
+
+procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor17($this: Ref);
+
+
+
+implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor17($this: Ref)
+{
+ var $localExc: Ref;
+ var $label: int;
+
+ RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x[$this] := 0;
+ call System.Object.#ctor46($this);
+ if ($Exception != null)
+ {
+ return;
+ }
+
+ return;
+}
+
+
+
+procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor();
+
+
+
+implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.BitwiseOperations$type: Type;
axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type);
axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);
-procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -978,11 +1017,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys -procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -998,11 +1037,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst -procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3220($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3220($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -1018,11 +1057,11 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy -procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3221($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3221($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1036,16 +1075,16 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3 -procedure RegressionTestInput.BitwiseOperations.#ctor21($this: Ref);
+procedure RegressionTestInput.BitwiseOperations.#ctor22($this: Ref);
-implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref)
+implementation RegressionTestInput.BitwiseOperations.#ctor22($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1056,11 +1095,11 @@ implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref) -procedure RegressionTestInput.BitwiseOperations.#cctor();
+procedure T$RegressionTestInput.BitwiseOperations.#cctor();
-implementation RegressionTestInput.BitwiseOperations.#cctor()
+implementation T$RegressionTestInput.BitwiseOperations.#cctor()
{
}
@@ -1082,20 +1121,20 @@ axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type); axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);
-procedure RegressionTestInput.AsyncAttribute.#ctor22($this: Ref);
+procedure RegressionTestInput.AsyncAttribute.#ctor23($this: Ref);
-procedure {:extern} System.Attribute.#ctor45($this: Ref);
+procedure {:extern} System.Attribute.#ctor47($this: Ref);
-implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref)
+implementation RegressionTestInput.AsyncAttribute.#ctor23($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Attribute.#ctor45($this);
+ call System.Attribute.#ctor47($this);
if ($Exception != null)
{
return;
@@ -1106,11 +1145,11 @@ implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref) -procedure RegressionTestInput.AsyncAttribute.#cctor();
+procedure T$RegressionTestInput.AsyncAttribute.#cctor();
-implementation RegressionTestInput.AsyncAttribute.#cctor()
+implementation T$RegressionTestInput.AsyncAttribute.#cctor()
{
}
@@ -1122,11 +1161,11 @@ axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);
-procedure RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int);
+procedure RegressionTestInput.RefParameters.M$System.Int32$24(x$in: int) returns (x$out: int);
-implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int)
+implementation RegressionTestInput.RefParameters.M$System.Int32$24(x$in: int) returns (x$out: int)
{
var $localExc: Ref;
var $label: int;
@@ -1140,16 +1179,16 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) re -procedure RegressionTestInput.RefParameters.#ctor24($this: Ref);
+procedure RegressionTestInput.RefParameters.#ctor25($this: Ref);
-implementation RegressionTestInput.RefParameters.#ctor24($this: Ref)
+implementation RegressionTestInput.RefParameters.#ctor25($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1160,11 +1199,11 @@ implementation RegressionTestInput.RefParameters.#ctor24($this: Ref) -procedure RegressionTestInput.RefParameters.#cctor();
+procedure T$RegressionTestInput.RefParameters.#cctor();
-implementation RegressionTestInput.RefParameters.#cctor()
+implementation T$RegressionTestInput.RefParameters.#cctor()
{
}
@@ -1176,16 +1215,16 @@ axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);
-procedure RegressionTestInput.NestedGeneric.#ctor27($this: Ref);
+procedure RegressionTestInput.NestedGeneric.#ctor28($this: Ref);
-implementation RegressionTestInput.NestedGeneric.#ctor27($this: Ref)
+implementation RegressionTestInput.NestedGeneric.#ctor28($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1202,16 +1241,16 @@ axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);
-procedure RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref);
+procedure RegressionTestInput.NestedGeneric.C.#ctor27($this: Ref);
-implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref)
+implementation RegressionTestInput.NestedGeneric.C.#ctor27($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1224,11 +1263,9 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref) function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;
-function Child0(in: Type) : Type;
-
axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);
-procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int);
+procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3226($this: Ref, x$in: int);
@@ -1236,7 +1273,7 @@ procedure {:extern} System.Activator.CreateInstance``12(T: Type) returns ($resul -implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int)
+implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3226($this: Ref, x$in: int)
{
var x: int;
var CS$0$0000: Box;
@@ -1251,7 +1288,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($thi x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1285,31 +1322,31 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($thi -procedure RegressionTestInput.NestedGeneric.C.G.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.C.G`1.#cctor();
-implementation RegressionTestInput.NestedGeneric.C.G.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.C.G`1.#cctor()
{
}
-procedure RegressionTestInput.NestedGeneric.C.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.C.#cctor();
-implementation RegressionTestInput.NestedGeneric.C.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.C.#cctor()
{
}
-procedure RegressionTestInput.NestedGeneric.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.#cctor();
-implementation RegressionTestInput.NestedGeneric.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.#cctor()
{
}
@@ -1335,6 +1372,45 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Re +const unique RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type: Type;
+
+axiom $Subtype(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+
+axiom $DisjointSubtree(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+
+var RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int;
+
+procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor29($this: Ref);
+
+
+
+implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor29($this: Ref)
+{
+ var $localExc: Ref;
+ var $label: int;
+
+ RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x[$this] := 0;
+ call System.Object.#ctor46($this);
+ if ($Exception != null)
+ {
+ return;
+ }
+
+ return;
+}
+
+
+
+procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor();
+
+
+
+implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.Class0$type: Type;
axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type);
@@ -1343,11 +1419,11 @@ axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type); var RegressionTestInput.Class0.StaticInt: int;
-procedure RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.StaticMethod$System.Int3230(x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.StaticMethod$System.Int3230(x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1361,11 +1437,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) -procedure RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int);
+procedure RegressionTestInput.Class0.M$System.Int3231($this: Ref, x$in: int);
-implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int)
+implementation RegressionTestInput.Class0.M$System.Int3231($this: Ref, x$in: int)
{
var x: int;
var __temp_1: int;
@@ -1396,11 +1472,11 @@ implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int -procedure RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int);
+procedure RegressionTestInput.Class0.M$System.Int32$System.Int3232($this: Ref, x$in: int, y$in: int);
-implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int)
+implementation RegressionTestInput.Class0.M$System.Int32$System.Int3232($this: Ref, x$in: int, y$in: int)
{
var x: int;
var y: int;
@@ -1415,11 +1491,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: R -procedure RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool);
+procedure RegressionTestInput.Class0.M$System.Boolean33($this: Ref, b$in: bool);
-implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool)
+implementation RegressionTestInput.Class0.M$System.Boolean33($this: Ref, b$in: bool)
{
var b: bool;
var $localExc: Ref;
@@ -1432,11 +1508,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: b -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref);
+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class034($this: Ref, c$in: Ref);
-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref)
+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class034($this: Ref, c$in: Ref)
{
var c: Ref;
var $localExc: Ref;
@@ -1449,18 +1525,18 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: -procedure RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int);
+procedure RegressionTestInput.Class0.NonVoid35($this: Ref) returns ($result: int);
-implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int)
+implementation RegressionTestInput.Class0.NonVoid35($this: Ref) returns ($result: int)
{
var $tmp8: int;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
- call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3228(3);
+ call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3230(3);
if ($Exception != null)
{
return;
@@ -1472,11 +1548,11 @@ implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result -procedure RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$36($this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$36($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
var $label: int;
@@ -1491,11 +1567,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x -procedure RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.RefParam$System.Int32$37($this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.RefParam$System.Int32$37($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
var $label: int;
@@ -1512,11 +1588,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x -procedure RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.AssignToInParam$System.Int3238($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.AssignToInParam$System.Int3238($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1534,11 +1610,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int);
+procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1552,11 +1628,11 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3240($this: Ref, y$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3240($this: Ref, y$in: int) returns ($result: int)
{
var y: int;
var $tmp9: int;
@@ -1565,7 +1641,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: y := y$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this, y);
+ call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this, y);
if ($Exception != null)
{
return;
@@ -1577,16 +1653,16 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: -procedure RegressionTestInput.Class0.#ctor39($this: Ref);
+procedure RegressionTestInput.Class0.#ctor41($this: Ref);
-implementation RegressionTestInput.Class0.#ctor39($this: Ref)
+implementation RegressionTestInput.Class0.#ctor41($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1597,11 +1673,11 @@ implementation RegressionTestInput.Class0.#ctor39($this: Ref) -procedure RegressionTestInput.Class0.#cctor();
+procedure T$RegressionTestInput.Class0.#cctor();
-implementation RegressionTestInput.Class0.#cctor()
+implementation T$RegressionTestInput.Class0.#cctor()
{
RegressionTestInput.Class0.StaticInt := 0;
}
@@ -1618,11 +1694,11 @@ var RegressionTestInput.ClassWithBoolTypes.staticB: bool; var RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool;
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool);
+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(x$in: int, y$in: int) returns ($result: bool);
-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool)
+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(x$in: int, y$in: int) returns ($result: bool)
{
var x: int;
var y: int;
@@ -1638,11 +1714,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool);
+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean43($this: Ref, z$in: bool);
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool)
+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean43($this: Ref, z$in: bool)
{
var z: bool;
var $localExc: Ref;
@@ -1651,7 +1727,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($th z := z$in;
RegressionTestInput.ClassWithBoolTypes.b[$this] := false;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1674,18 +1750,18 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($th -procedure RegressionTestInput.ClassWithBoolTypes.Main42();
+procedure RegressionTestInput.ClassWithBoolTypes.Main44();
-implementation RegressionTestInput.ClassWithBoolTypes.Main42()
+implementation RegressionTestInput.ClassWithBoolTypes.Main44()
{
var $tmp10: bool;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
- call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(3, 4);
+ call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(3, 4);
if ($Exception != null)
{
return;
@@ -1697,11 +1773,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main42() -procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
+procedure T$RegressionTestInput.ClassWithBoolTypes.#cctor();
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
+implementation T$RegressionTestInput.ClassWithBoolTypes.#cctor()
{
RegressionTestInput.ClassWithBoolTypes.staticB := false;
}
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs index e3da57b5..a8b5fdb2 100644 --- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs +++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs @@ -61,7 +61,7 @@ namespace TranslationTest { #endregion
private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {
- BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, null, null, false);
+ BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, new Options(), null, false);
var fileName = Path.ChangeExtension(assemblyName, "bpl");
var s = File.ReadAllText(fileName);
return s;
diff --git a/BCT/TranslationPlugins/PhoneControlsPlugin.cs b/BCT/TranslationPlugins/PhoneControlsPlugin.cs index e539b1b8..daa7c345 100644 --- a/BCT/TranslationPlugins/PhoneControlsPlugin.cs +++ b/BCT/TranslationPlugins/PhoneControlsPlugin.cs @@ -7,7 +7,7 @@ using System.IO; namespace TranslationPlugins {
public enum Visibility { Visible, Collapsed };
- public enum Event { Click, Checked, Unchecked };
+ public enum Event { Click, Checked, Unchecked, SelectionChanged };
public class HandlerSignature {
public static string[] getParameterTypesForHandler(Event controlEvent) {
@@ -15,6 +15,7 @@ namespace TranslationPlugins { case Event.Checked:
case Event.Unchecked:
case Event.Click:
+ case Event.SelectionChanged:
return new string[] { "object", "System.WindowsRoutedventArgs" };
default:
throw new NotImplementedException("Handlers for event: " + controlEvent + " not supported yet");
@@ -94,7 +95,7 @@ namespace TranslationPlugins { public class PhoneControlsPlugin : TranslationPlugin {
// TODO this will probably need a complete rewrite once it is event based, and make it more push than pull
// TODO but it doesn't make sense right now to make it BCT or CCI aware
- private static int CONFIG_LINE_FIELDS= 11;
+ private static int CONFIG_LINE_FIELDS= 12;
private static int PAGE_CLASS_FIELD= 0;
private static int PAGE_XAML_FIELD= 1;
private static int PAGE_BOOGIE_STRING_FIELD = 2;
@@ -105,7 +106,8 @@ namespace TranslationPlugins { private static int CLICK_HANDLER_FIELD= 7;
private static int CHECKED_HANDLER_FIELD= 8;
private static int UNCHECKED_HANDLER_FIELD = 9;
- private static int BPL_NAME_FIELD = 10;
+ private static int SELECTIONCHANGED_HANDLER_FIELD = 10;
+ private static int BPL_NAME_FIELD = 11;
private IDictionary<string, PageStructure> pageStructureInfo;
@@ -125,28 +127,6 @@ namespace TranslationPlugins { return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();
}
- /// <summary>
- /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)
- /// This method returns a base URI
- /// </summary>
- /// <param name="uri"></param>
- /// <returns></returns>
- public static string getURIBase(string uri) {
- // I need to build an absolute URI just to call getComponents() ...
- Uri mockBaseUri = new Uri("mock://mock/", UriKind.RelativeOrAbsolute);
- Uri realUri;
- try {
- realUri = new Uri(uri, UriKind.Absolute);
- } catch (UriFormatException) {
- // uri string is relative
- realUri = new Uri(mockBaseUri, uri);
- }
-
- string str = realUri.GetComponents(UriComponents.Path | UriComponents.StrongAuthority | UriComponents.Scheme, UriFormat.UriEscaped);
- Uri mockStrippedUri = new Uri(str);
- return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();
- }
-
//public static string getFullyQualifiedControlClass(string controlClass) {
// // TODO do an actual API discovery. The problem will be differencing 7.0 apps from 7.1 apps
// return "System.Windows.Controls." + controlClass;
@@ -190,6 +170,7 @@ namespace TranslationPlugins { }
private void setPageAsMainPage(string pageXAML) {
+ pageXAML = pageXAML.ToLower();
int lastDirPos= pageXAML.LastIndexOf('/');
if (lastDirPos != -1)
pageXAML = pageXAML.Substring(lastDirPos+1);
@@ -212,14 +193,15 @@ namespace TranslationPlugins { public void DumpControlStructure(StreamWriter outputStream) {
// maintain same format as input format
- string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;
+ string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler,
+ checkedHandler, uncheckedHandler, selectionChangedHandler, bplName;
outputStream.WriteLine(getMainPageXAML());
outputStream.WriteLine(getBoogieNavigationVariable());
outputStream.WriteLine(getMainAppTypeName());
foreach (KeyValuePair<string, PageStructure> entry in this.pageStructureInfo) {
pageClass = entry.Key;
- pageXAML = entry.Value.PageXAML;
+ pageXAML = entry.Value.PageXAML.ToLower();
pageBoogieStringName = entry.Value.PageBoogieName;
foreach (ControlInfoStructure controlInfo in entry.Value.getAllControlsInfo()) {
controlClass= controlInfo.ClassName;
@@ -253,8 +235,17 @@ namespace TranslationPlugins { } else {
uncheckedHandler = "";
}
+
+ handlers = controlInfo.getHandlers(Event.SelectionChanged);
+ if (handlers.Any()) {
+ selectionChangedHandler= handlers.First().Name;
+ } else {
+ selectionChangedHandler = "";
+ }
bplName = controlInfo.BplName;
- outputStream.WriteLine(pageClass + "," + pageXAML + "," + pageBoogieStringName + "," + controlClass + "," + controlName + "," + enabled + "," + visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + bplName);
+ outputStream.WriteLine(pageClass + "," + pageXAML.ToLower() + "," + pageBoogieStringName + "," + controlClass + "," + controlName + "," + enabled + "," +
+ visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + selectionChangedHandler + "," +
+ bplName);
}
}
}
@@ -276,14 +267,15 @@ namespace TranslationPlugins { // TODO the page.xaml value is saved with no directory information: if two pages exist with same name but different directories it will treat them as the same
// TODO I'm not handling this for now, and I won't be handling relative/absolute URI either for now
- string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;
+ string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler,
+ uncheckedHandler, selectionChangedHandler, bplName;
string configLine = configStream.ReadLine();
string[] inputLine;
PageStructure pageStr;
ControlInfoStructure controlInfoStr;
// first line just states the main page xaml
- string mainPageXAML= configLine.Trim();
+ string mainPageXAML= configLine.Trim().ToLower();
configLine = configStream.ReadLine();
// second line states boogie current nav variable, possibly dummy value
@@ -305,7 +297,7 @@ namespace TranslationPlugins { throw new ArgumentException("Config input line contains wrong number of fields: " + inputLine.Length + ", expected " + CONFIG_LINE_FIELDS);
pageClass = inputLine[PAGE_CLASS_FIELD].Trim();
- pageXAML = inputLine[PAGE_XAML_FIELD].Trim();
+ pageXAML = inputLine[PAGE_XAML_FIELD].Trim().ToLower();
pageBoogieStringName = inputLine[PAGE_BOOGIE_STRING_FIELD].Trim();
controlClass = inputLine[CONTROL_CLASS_FIELD].Trim();
controlName = inputLine[CONTROL_NAME_FIELD].Trim();
@@ -317,6 +309,7 @@ namespace TranslationPlugins { clickHandler = inputLine[CLICK_HANDLER_FIELD].Trim();
checkedHandler = inputLine[CHECKED_HANDLER_FIELD].Trim();
uncheckedHandler = inputLine[UNCHECKED_HANDLER_FIELD].Trim();
+ selectionChangedHandler = inputLine[SELECTIONCHANGED_HANDLER_FIELD].Trim();
bplName = inputLine[BPL_NAME_FIELD].Trim();
try {
@@ -341,6 +334,7 @@ namespace TranslationPlugins { controlInfoStr.setHandler(Event.Click, clickHandler);
controlInfoStr.setHandler(Event.Checked, checkedHandler);
controlInfoStr.setHandler(Event.Unchecked, uncheckedHandler);
+ controlInfoStr.setHandler(Event.SelectionChanged, selectionChangedHandler);
pageStr.setControlInfo(controlName, controlInfoStr);
pageStructureInfo[pageClass] = pageStr;
diff --git a/Chalice/readme.txt b/Chalice/readme.txt index 3f36e1db..37998339 100644 --- a/Chalice/readme.txt +++ b/Chalice/readme.txt @@ -7,3 +7,8 @@ Running Chalice: chalice.bat <file.chalice> [-params] Running the tests for Chalice: see tests/readme.txt
Chalice is built using Simple Build Tool (https://github.com/harrah/xsbt/wiki/Setup)
+
+Note: You might have to increase the stack size of the JVM to avoid a stack
+overflow, for instance by changing scala.bat by adding "-Xss16M" to the
+JAVA_OPTS:
+ if "%_JAVA_OPTS%"=="" set _JAVA_OPTS=-Xmx256M -Xms32M -Xss16M
diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala index 594273cb..e49d12a5 100644 --- a/Chalice/src/main/scala/Chalice.scala +++ b/Chalice/src/main/scala/Chalice.scala @@ -189,7 +189,7 @@ object Chalice { // parse programs
val parser = new Parser();
val parseResults = if (files.isEmpty) {
- println("No input file provided. Use 'chalice /help' for a list of all available command line options. Reading from stdin...")
+ if (!vsMode) println("No input file provided. Use 'chalice /help' for a list of all available command line options. Reading from stdin...")
List(parser.parseStdin)
} else for (file <- files) yield {
parser.parseFile(file)
diff --git a/Chalice/src/main/scala/SmokeTest.scala b/Chalice/src/main/scala/SmokeTest.scala index 9f23d144..f317f24c 100644 --- a/Chalice/src/main/scala/SmokeTest.scala +++ b/Chalice/src/main/scala/SmokeTest.scala @@ -25,7 +25,7 @@ object SmokeTest { var warning: Boolean = false // did this "assert false" generate a warning? (i.e. did it not generate a Boogie error?)
}
/** Serves as a sentinel for the first assert (which should always cause a
- * warning, thus SmokeAssertSentinel.warning = false
+ * warning, thus SmokeAssertSentinel.warning = false)
*/
object SmokeAssertSentinel extends SmokeAssert(-1, NoPosition, "", Set(), null)
diff --git a/Chalice/tests/examples/AssociationList.chalice b/Chalice/tests/examples/AssociationList.chalice index cc3ecfb4..418bcd12 100644 --- a/Chalice/tests/examples/AssociationList.chalice +++ b/Chalice/tests/examples/AssociationList.chalice @@ -1,3 +1,12 @@ +/*
+ Note: This example seems to be completely broken. The failing assertion
+ about locking/unlocking too much causes an inconsistency and all following
+ assertions pass by default.
+ It seems that the specification, in particular the loop invariant in method
+ Add, is wrong. (see also http://boogie.codeplex.com/workitem/10207)
+ -- August 2011, Stefan Heule
+*/
+
class Client {
method Main(d: Data)
requires d != null
diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt index bfff3c60..53d6428f 100644 --- a/Chalice/tests/examples/AssociationList.output.txt +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -1,10 +1,10 @@ Verification of AssociationList.chalice using parameters=""
- 19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu. - 64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop. + 28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for mu. + 73.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop. The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 64.9: The begging of the while-body is unreachable. - 64.9: The statements after the while-loop are unreachable. + 73.9: The begging of the while-body is unreachable. + 73.9: The statements after the while-loop are unreachable. Boogie program verifier finished with 2 errors and 2 smoke test warnings.
diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs index e29a6d4a..698141bb 100644 --- a/Source/AbsInt/AbstractInterpretation.cs +++ b/Source/AbsInt/AbstractInterpretation.cs @@ -153,15 +153,6 @@ namespace Microsoft.Boogie.AbstractInterpretation { return this.lattice.Meet(atReturn, knownAtCallSite);
}
- /*
- private Cci.IGraphNavigator callGraph;
- public Cci.IGraphNavigator CallGraph {
- get {
- return this.callGraph;
- }
- }
- */
-
/// <summary>
/// Compute the invariants for the program using the underlying abstract domain
/// </summary>
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 6b5723c8..e91b47c8 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -39,6 +39,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelpe EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TPTP", "Provers\TPTP\TPTP.csproj", "{A598ED5A-93AD-4125-A555-3921A2F936FA}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.csproj", "{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Checked|.NET = Checked|.NET
@@ -495,6 +497,30 @@ Global {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|x86.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|.NET.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Any CPU.Build.0 = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Release|x86.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.ActiveCfg = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 88d8bdaa..82c864d5 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -429,6 +429,21 @@ namespace Microsoft.Boogie { // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+ if (CommandLineOptions.Clo.ContractInfer) {
+ Houdini.Houdini houdini = new Houdini.Houdini(program, true);
+ Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment) {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
+ errorCount = outcome.ErrorCount;
+ verified = outcome.Verified;
+ inconclusives = outcome.Inconclusives;
+ timeOuts = outcome.TimeOuts;
+ outOfMemories = 0;
+ return PipelineOutcome.Done;
+ }
+
if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
}
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 95078433..52714dc9 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -172,6 +172,10 @@ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
</ProjectReference>
+ <ProjectReference Include="..\Houdini\Houdini.csproj">
+ <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>
+ <Name>Houdini</Name>
+ </ProjectReference>
<ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
<Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 56116601..e1136150 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -299,7 +299,6 @@ namespace Microsoft.Boogie { public int VcsCores = 1;
public bool VcsDumpSplits = false;
- public bool houdiniEnabled = false;
public bool DebugRefuted = false;
public XmlSink XmlRefuted {
@@ -401,7 +400,6 @@ namespace Microsoft.Boogie { Contract.Invariant(cce.NonNullElements(methodsToTranslateMethodQualified, true));
Contract.Invariant(cce.NonNullElements(methodsToTranslateSubstring, true));
Contract.Invariant(Ai != null);
- Contract.Invariant(houdiniFlags != null);
}
[Rep]
@@ -441,13 +439,6 @@ namespace Microsoft.Boogie { }
public AiFlags/*!*/ Ai = new AiFlags();
- public class HoudiniFlags {
- public bool continueAtError = false;
- public bool incremental = false;
- }
-
- public HoudiniFlags/*!*/ houdiniFlags = new HoudiniFlags();
-
[Verify(false)]
private CommandLineOptions() {
// this is just to suppress verification.
@@ -979,8 +970,6 @@ namespace Microsoft.Boogie { case "-contractInfer":
case "/contractInfer":
ContractInfer = true;
- TheProverFactory = ProverFactory.Load("ContractInference");
- ProverName = "ContractInference".ToUpper();
break;
case "-subsumption":
@@ -1367,28 +1356,6 @@ namespace Microsoft.Boogie { }
break;
- case "-Houdini":
- case "/Houdini":
- this.houdiniEnabled = true;
- if (ps.hasColonArgument) {
- if (ps.ConfirmArgumentCount(1)) {
- foreach (char c in cce.NonNull(args[ps.i])) {
- switch (c) {
- case 'c':
- houdiniFlags.continueAtError = true;
- break;
- case 'i':
- houdiniFlags.incremental = true;
- break;
- default:
- ps.Error("Unknown houdini flag: " + c + "\n");
- break;
- }
- }
- }
- }
- break;
-
case "-z3exe":
case "/z3exe":
if (ps.ConfirmArgumentCount(1)) {
@@ -2172,10 +2139,6 @@ namespace Microsoft.Boogie { of every block
/printInstrumented : print Boogie program after it has been
instrumented with invariants
- /Houdini[:<flags>] : perform procedure Houdini
- c = continue when an error found
- i = use incremental queries
- /dbgRefuted : log refuted Houdini candidates to XmlSink
---- Debugging and general tracing options ---------------------------------
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 098dbad2..5e2bc911 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3715,6 +3715,9 @@ namespace Microsoft.Dafny { return UsesSpecFeatures(e.Seq) ||
(e.E0 != null && UsesSpecFeatures(e.E0)) ||
(e.E1 != null && UsesSpecFeatures(e.E1));
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+ return UsesSpecFeatures(e.Array) || e.Indices.Exists(ee => UsesSpecFeatures(ee));
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
return UsesSpecFeatures(e.Seq) ||
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 99df97cd..21336545 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -344,7 +344,6 @@ namespace Graphing { Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null));
}
-
private class PreHeader {
Node/*!*/ myHeader;
[ContractInvariantMethod]
@@ -464,7 +463,7 @@ namespace Graphing { }
}
- internal IEnumerable<Node> Predecessors(Node n) {
+ public IEnumerable<Node> Predecessors(Node n) {
// original A#
//Set<Node> result = Set{ x : x in Nodes, Edge(x,n) };
@@ -472,7 +471,7 @@ namespace Graphing { return predCache[n];
}
- internal IEnumerable<Node> Successors(Node n) {
+ public IEnumerable<Node> Successors(Node n) {
ComputePredSuccCaches();
return succCache[n];
}
diff --git a/Source/Houdini/AssemblyInfo.ssc b/Source/Houdini/AssemblyInfo.ssc deleted file mode 100644 index 6ed99a25..00000000 --- a/Source/Houdini/AssemblyInfo.ssc +++ /dev/null @@ -1,4 +0,0 @@ -using System.Reflection;
-using System.Runtime.CompilerServices;
-
-[assembly: AssemblyKeyFile("..\\InterimKey.snk")]
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs new file mode 100644 index 00000000..437dbc98 --- /dev/null +++ b/Source/Houdini/Checker.cs @@ -0,0 +1,90 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Diagnostics.Contracts;
+using System.Collections.Generic;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.Simplify;
+using Microsoft.Boogie.Z3;
+using System.Collections;
+using System.IO;
+using System.Threading;
+using VC;
+
+namespace Microsoft.Boogie.Houdini {
+ public class HoudiniVCGen : VCGen {
+ private Checker checker;
+ private string descriptiveName;
+ private VCExpr conjecture;
+ private ProverInterface.ErrorHandler handler;
+ CounterexampleCollector collector;
+
+ public VCExpressionGenerator VCExprGenerator {
+ get {
+ return checker.VCExprGen;
+ }
+ }
+
+ public Boogie2VCExprTranslator BooogieExprTranslator {
+ get {
+ DeclFreeProverContext proverContext = (DeclFreeProverContext)checker.TheoremProver.Context;
+ return proverContext.BoogieExprTranslator;
+ }
+ }
+
+ public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile)
+ : base(program, logFilePath, appendLogFile) {
+ descriptiveName = impl.Name;
+ collector = new CounterexampleCollector();
+ collector.OnProgress("HdnVCGen", 0, 0, 0.0);
+ if (CommandLineOptions.Clo.SoundnessSmokeTest) {
+ throw new Exception("HoudiniVCGen does not support Soundness smoke test.");
+ }
+
+ ConvertCFG2DAG(impl, program);
+ ModelViewInfo mvInfo;
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);
+ Hashtable/*<int, Absy!>*/ label2absy;
+ checker = new Checker(this, program, logFilePath, appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);
+ if (!(checker.TheoremProver is Z3ProcessTheoremProver)) {
+ throw new Exception("HdnChecker only works with z3");
+ }
+ conjecture = GenerateVC(impl, null, out label2absy, checker);
+
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
+ handler = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, implName2LazyInliningInfo, checker.TheoremProver.Context, program);
+ }
+ else {
+ handler = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, implName2LazyInliningInfo, checker.TheoremProver.Context, program);
+ }
+ }
+
+ public ProverInterface.Outcome Verify(VCExpr axiom, out List<Counterexample> errors) {
+ collector.examples.Clear();
+ VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);
+ checker.BeginCheck(descriptiveName, vc, handler);
+ WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });
+
+ ProverInterface.Outcome proverOutcome = checker.ReadOutcome();
+ if (proverOutcome == ProverInterface.Outcome.Invalid) {
+ Contract.Assume(collector.examples != null);
+ if (collector.examples.Count == 0) {
+ string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));
+ if (memStr != null)
+ memStr = "?";
+ throw new UnexpectedProverOutputException("Outcome.Errors w/ 0 counter examples. " + memStr + " memory used");
+ }
+ errors = collector.examples;
+ }
+ else {
+ errors = null;
+ }
+ return proverOutcome;
+ }
+
+ }
+}
\ No newline at end of file diff --git a/Source/Houdini/Checker.ssc b/Source/Houdini/Checker.ssc deleted file mode 100644 index 03c2beda..00000000 --- a/Source/Houdini/Checker.ssc +++ /dev/null @@ -1,460 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using Microsoft.Contracts;
-using System.Collections.Generic;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify.AST;
-using VC;
-using Microsoft.Boogie.Z3;
-using Microsoft.AbstractInterpretationFramework;
-using Microsoft.Boogie.AbstractInterpretation;
-using System.Collections;
-using System.Compiler;
-using System.IO;
-using System.Threading;
-
-namespace Microsoft.Boogie.Houdini {
-
- public abstract class HdnCheckerFactory {
- public static HdnChecker! BuildHdnChecker(Checker! checker) {
- if (checker.TheoremProver is Z3ThreadTheoremProver)
- return new HoudiniZ3ApiChecker(checker);
- else if (checker.TheoremProver is Z3ProcessTheoremProver) {
- if (CommandLineOptions.Clo.houdiniFlags.incremental) {
- return new HoudiniZ3CheckerIncr(checker);
- } else {
- return new HoudiniZ3Checker(checker);
- }
- } else
- throw new Exception("HdnChecker only works with z3");
- }
- }
-
- public abstract class HdnChecker {
- public abstract void PrepareCheck(string! _descriptiveName,
- VCExpr! _vc, ProverInterface.ErrorHandler! _handler);
- public abstract void PushAxiom(VCExpr! vc);
- public abstract void Pop();
- public abstract void Check();
- public abstract ProverInterface.Outcome ReadOutcome()
- throws UnexpectedProverOutputException;
- }
-
- public class HoudiniZ3ApiChecker:HdnChecker {
-
- private Z3ThreadTheoremProver! z3prover;
-
- private ProverInterface.ErrorHandler handler;
- private ProverInterface.Outcome outcome;
- private UnexpectedProverOutputException outputExn;
-
- internal HoudiniZ3ApiChecker(Checker! checker)
- requires checker.TheoremProver!=null;
- requires checker.TheoremProver is Z3ThreadTheoremProver;
- {
- this.z3prover = (Z3ThreadTheoremProver)checker.TheoremProver;
- }
-
- public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc, ProverInterface.ErrorHandler! _handler) {
- handler = _handler;
- z3prover.LogComment(_descriptiveName);
- z3prover.PrepareCheck(_descriptiveName,_vc);
- }
-
- public override void PushAxiom(VCExpr! vc) {
- z3prover.PushAxiom(vc);
- }
-
- public override void Pop() {
- z3prover.Pop();
- }
-
- public override void Check() {
- z3prover.BeginPreparedCheck();
- try {
- outcome = z3prover.CheckOutcome((!)handler);
- } catch (UnexpectedProverOutputException e) {
- outputExn = e;
- }
- }
-
- public override ProverInterface.Outcome ReadOutcome()
- throws UnexpectedProverOutputException;
- {
- if (outputExn != null) {
- throw outputExn;
- }
- return outcome;
- }
- }
-
- // version of Z3PTP exposing more of the prover process functionality
- public class Z3ProcessTPExposed : Z3ProcessTheoremProver {
-
- [NotDelayed]
- public Z3ProcessTPExposed (TextWriter/*?*/ logFileWriter, VCExpressionGenerator! gen, DeclFreeProverContext! ctx, int timeout, bool typed)
- throws UnexpectedProverOutputException;
- {
- base(logFileWriter, gen, ctx, timeout, typed, "z3.exe");
- }
-
-
- //MOVED Directly Z3 ProverInterface for now...
- //To introduce this cleanly, need to add a new subproject under Provers
- //and must use the commandline option for that, instead of saying /prover:z3
- //That way, the class is constructed in class Checker the same way
- //all the other provers are constructed
-
- }
-
- public class Z3ExposedFactory : Z3.Factory {
-
- }
-
-
- //Old version
- public class HoudiniZ3Checker:HdnChecker {
- private Stack<VCExpr!>! axioms = new Stack<VCExpr!>();
- private Checker! checker;
- private string descriptiveName;
- private VCExpr conjecture;
- private ProverInterface.ErrorHandler handler;
-
- internal HoudiniZ3Checker(Checker! checker)
- requires checker.TheoremProver!=null;
- requires checker.TheoremProver is Z3ProcessTheoremProver;
- {
- this.checker = checker;
- }
-
- public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc, ProverInterface.ErrorHandler! _handler)
- {
- this.descriptiveName = _descriptiveName;
- this.conjecture = _vc;
- this.handler = _handler;
- }
- public override void PushAxiom(VCExpr! vc) {
- axioms.Push(vc);
- }
- public override void Pop() {
- axioms.Pop();
- }
- private VCExpr! BuildVCAxioms(Stack<VCExpr!>! axioms)
- requires axioms.Count>0;
- {
- VCExpr vc_axioms = null;
- foreach (VCExpr! axiom in axioms) {
- if (vc_axioms==null)
- vc_axioms=axiom;
- else
- vc_axioms = checker.VCExprGen.And(vc_axioms,axiom);
- }
- return (!)vc_axioms;
- }
-
- public override void Check()
- {
- assert (descriptiveName!=null);
- assert (conjecture!=null);
- assert (handler!=null);
- outcome = ProverInterface.Outcome.Undetermined;
-
- VCExpr! vc;
- if (axioms.Count>0) {
- VCExpr vc_axioms = BuildVCAxioms(axioms);
- vc = checker.VCExprGen.Implies(vc_axioms,conjecture);
- } else
- vc = conjecture;
-
- checker.BeginCheck(descriptiveName,vc,handler);
- WaitHandle.WaitAny(new WaitHandle[] {checker.ProverDone});
- }
-
- private ProverInterface.Outcome outcome;
- private UnexpectedProverOutputException outputExn;
-
- public override ProverInterface.Outcome ReadOutcome()
- throws UnexpectedProverOutputException;
- {
- try {
- outcome = checker.ReadOutcome();
- } catch (UnexpectedProverOutputException e) {
- throw e;
- }
- return outcome;
- }
- }
-
- //new version
- public class HoudiniZ3CheckerIncr:HdnChecker {
- private Checker! checker;
- private string descriptiveName;
- private VCExpr conjecture;
- private ProverInterface.ErrorHandler handler;
-
- // Hack to delay the exception throwing (from Push/Pop...) for now
- private UnexpectedProverOutputException delayedExc;
- private Z3ProcessTheoremProver! thmProver;
-
- internal HoudiniZ3CheckerIncr(Checker! checker)
- requires checker.TheoremProver!=null;
- requires checker.TheoremProver is Z3ProcessTheoremProver;
- {
- this.checker = checker;
- this.thmProver = (Z3ProcessTheoremProver!)checker.TheoremProver;
- }
-
- private void delayException(UnexpectedProverOutputException exc) {
- if (delayedExc == null) { delayedExc = exc; }
- }
-
- public override void PrepareCheck(string! _descriptiveName, VCExpr! _vc,
- ProverInterface.ErrorHandler! _handler)
- {
- this.descriptiveName = _descriptiveName;
- this.conjecture = _vc;
- this.handler = _handler;
- this.thmProver.LogComment(_descriptiveName);
- try {
- this.thmProver.PrepareCheck(_descriptiveName,_vc);
- } catch (UnexpectedProverOutputException exc) {
- delayException(exc);
- }
- }
- public override void PushAxiom(VCExpr! vc) {
- string! vcStr = vc.ToString();
- try {
- thmProver.PushAxioms(vcStr);
- } catch (UnexpectedProverOutputException exc) {
- delayException(exc);
- }
- }
- public override void Pop() {
- try {
- thmProver.PopAxioms();
- } catch (UnexpectedProverOutputException exc) {
- delayException(exc);
- }
- }
-
- public override void Check()
- {
- assert (descriptiveName!=null);
- assert (conjecture!=null);
- assert (handler!=null);
- outcome = ProverInterface.Outcome.Undetermined;
-
- VCExpr! vc = checker.VCExprGen.False;
- checker.BeginCheck(descriptiveName,vc,handler);
- WaitHandle.WaitAny(new WaitHandle[] {checker.ProverDone});
- }
-
- private ProverInterface.Outcome outcome;
- private UnexpectedProverOutputException outputExn;
-
- public override ProverInterface.Outcome ReadOutcome()
- throws UnexpectedProverOutputException;
- {
- // HACK
- if (delayedExc != null) {
- UnexpectedProverOutputException temp = delayedExc;
- delayedExc = null;
- throw temp;
- }
- // Normal stuff
- try {
- outcome = checker.ReadOutcome();
- } catch (UnexpectedProverOutputException e) {
- throw e;
- }
- return outcome;
- }
- }
-
- public abstract class HdnVCGenFactory {
- public abstract HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile);
- }
- public class Z3APIHdnVCGenFactory:HdnVCGenFactory {
- public override HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile) {
- return new Z3ApiHdnVCGen(program, logFilePath, appendLogFile);
- }
- }
- public class Z3HdnVCGenFactory:HdnVCGenFactory {
- public override HdnVCGen! BuildVCGen(Program! program, string logFilePath, bool appendLogFile) {
- return new Z3HdnVCGen(program, logFilePath, appendLogFile);
- }
- }
-
- public abstract class HdnVCGen {
- public abstract void PrepareVerification(Implementation! impl, Program! program);
- public abstract void PushAxiom(Axiom! axiom);
- public abstract void Pop();
- public abstract VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)
- throws UnexpectedProverOutputException;
-
- }
-
- public class Z3HdnVCGen: HdnVCGen {
- private Program! program;
- private string logFilePath;
- private bool appendLogFile;
- private Implementation implementation;
- private Axiom axiom;
-
- private ExtVCGen vcgen;
-
- public Z3HdnVCGen(Program! program, string logFilePath, bool appendLogFile) {
- this.program = program;
- this.logFilePath = logFilePath;
- this.appendLogFile= appendLogFile;
- }
-
- public override void PrepareVerification(Implementation! impl, Program! program) {
- this.implementation = impl;
- this.program = program;
- this.vcgen = new ExtVCGen(program,logFilePath,appendLogFile);
- this.vcgen.PrepareVerification(this.implementation,this.program);
- //watch out for > 1 call -- don't want CFG conversion to happen too many times!!!
- }
-
- public override void PushAxiom(Axiom! axiom) {
- assert this.vcgen != null;
- this.axiom=axiom;
- this.vcgen.PushAxiom(this.axiom);
- }
-
- public override void Pop() {
- assert this.vcgen != null;
- this.vcgen.Pop();
- this.axiom = null;
- }
-
- public override VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)
- throws UnexpectedProverOutputException; {
- assert(this.vcgen!=null);
-
- return vcgen.Verify(out errors);
- }
-
- }
-
- public class Z3ApiHdnVCGen: HdnVCGen {
- private ExtVCGen! vcgen;
-
- public Z3ApiHdnVCGen(Program! program, string logFilePath, bool appendLogFile) {
- this.vcgen = new ExtVCGen(program,logFilePath,appendLogFile);
- }
-
- public override void PrepareVerification(Implementation! impl, Program! program) {
- vcgen.PrepareVerification(impl,program);
- }
-
- public override void PushAxiom(Axiom! axiom) {
- vcgen.PushAxiom(axiom);
- }
-
- public override void Pop() {
- vcgen.Pop();
- }
-
- public override VC.VCGen.Outcome Verify(out List<Counterexample!>? errors)
- throws UnexpectedProverOutputException; {
- return vcgen.Verify(out errors);
- }
-
- }
-
-
-
- public class ExtVCGen : VCGen {
-
- private HdnChecker hdnChecker;
- private VCExpressionGenerator gen;
- CounterexampleCollector! collector = new CounterexampleCollector();
-
- public ExtVCGen(Program! program, string logFilePath, bool appendLogFile) {
- base(program,logFilePath,appendLogFile);
- }
-
- public void PrepareVerification(Implementation! impl, Program! program) {
- collector.OnProgress("HdnVCGen", 0, 0, 0.0);
- if (CommandLineOptions.Clo.SoundnessSmokeTest) {
- throw new Exception("HoudiniVCGen does not support Soundness smoke test.");
- }
-
- ConvertCFG2DAG(impl, program);
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program);
- Hashtable/*<int, Absy!>*/! label2absy;
- Checker! checker = new Checker(program, this.logFilePath, this.appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);
- VCExpr! vc = GenerateVC(impl, out label2absy, checker);
-
- ErrorReporter reporter;
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
- reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector);
- } else {
- reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector);
- }
- this.gen = checker.VCExprGen;
- this.hdnChecker = HdnCheckerFactory.BuildHdnChecker(checker);
- this.hdnChecker.PrepareCheck((!) impl.Name, vc, reporter);
- }
-
-
- public void PushAxiom(Axiom! axiom)
- {
- assume (hdnChecker!=null);
- assume (gen!=null);
- VCExpr vc = axiom.Expr.VCView(gen);
- this.hdnChecker.PushAxiom(vc);
- }
- public void Pop() {
- assume (hdnChecker!=null);
- hdnChecker.Pop();
- }
-
- public Outcome Verify(out List<Counterexample!>? errors)
- throws UnexpectedProverOutputException; {
- assume (hdnChecker!=null);
- collector.examples.Clear();
- hdnChecker.Check();
- ProverInterface.Outcome proverOutcome;
- proverOutcome = hdnChecker.ReadOutcome();
- Outcome verifyOutcome = ReadOutcome(proverOutcome);
- if (verifyOutcome == Outcome.Errors) {
- assume (collector.examples!=null);
- if (collector.examples.Count == 0) {
- string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));
- if (memStr != null)
- memStr = "?";
- throw new UnexpectedProverOutputException("Outcome.Errors w/ 0 counter examples. " + memStr + " memory used");
- }
- errors = collector.examples;
- } else {
- errors = null;
- }
- return verifyOutcome;
- }
-
- private Outcome ReadOutcome(ProverInterface.Outcome proverOutcome) {
- switch (proverOutcome) {
- case ProverInterface.Outcome.Valid:
- return Outcome.Correct;
- case ProverInterface.Outcome.Invalid:
- return Outcome.Errors;
- case ProverInterface.Outcome.TimeOut:
- return Outcome.TimedOut;
- case ProverInterface.Outcome.Undetermined:
- return Outcome.Inconclusive;
- default:
- throw new Exception("Unknown Prover Interface outcome while reading outcome.");
- }
- }
-
- }
-
-
-}
\ No newline at end of file diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs new file mode 100644 index 00000000..714ecd3b --- /dev/null +++ b/Source/Houdini/Houdini.cs @@ -0,0 +1,1139 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Diagnostics.Contracts;
+using System.Collections.Generic;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.Simplify;
+using VC;
+using Microsoft.Boogie.Z3;
+using System.Collections;
+using System.IO;
+using Microsoft.AbstractInterpretationFramework;
+using Graphing;
+
+namespace Microsoft.Boogie.Houdini {
+
+ class ReadOnlyDictionary<K, V> {
+ private Dictionary<K, V> dictionary;
+ public ReadOnlyDictionary(Dictionary<K, V> dictionary) {
+ this.dictionary = dictionary;
+ }
+
+ public Dictionary<K, V>.KeyCollection Keys {
+ get { return this.dictionary.Keys; }
+ }
+
+ public bool TryGetValue(K k, out V v) {
+ return this.dictionary.TryGetValue(k, out v);
+ }
+
+ public bool ContainsKey(K k) {
+ return this.dictionary.ContainsKey(k);
+ }
+ }
+
+ public abstract class HoudiniObserver {
+ public virtual void UpdateStart(Program program, int numConstants) { }
+ public virtual void UpdateIteration() { }
+ public virtual void UpdateImplementation(Implementation implementation) { }
+ public virtual void UpdateAssignment(Dictionary<string, bool> assignment) { }
+ public virtual void UpdateOutcome(ProverInterface.Outcome outcome) { }
+ public virtual void UpdateEnqueue(Implementation implementation) { }
+ public virtual void UpdateDequeue() { }
+ public virtual void UpdateConstant(string constantName) { }
+ public virtual void UpdateEnd(bool isNormalEnd) { }
+ public virtual void UpdateFlushStart() { }
+ public virtual void UpdateFlushFinish() { }
+ public virtual void SeeException(string msg) { }
+ }
+
+ public class IterationTimer<K> {
+ private Dictionary<K, List<double>> times;
+
+ public IterationTimer() {
+ times = new Dictionary<K, List<double>>();
+ }
+
+ public void AddTime(K key, double timeMS) {
+ List<double> oldList;
+ times.TryGetValue(key, out oldList);
+ if (oldList == null) {
+ oldList = new List<double>();
+ }
+ else {
+ times.Remove(key);
+ }
+ oldList.Add(timeMS);
+ times.Add(key, oldList);
+ }
+
+ public void PrintTimes(TextWriter wr) {
+ wr.WriteLine("Total procedures: {0}", times.Count);
+ double total = 0;
+ int totalIters = 0;
+ foreach (KeyValuePair<K, List<double>> kv in times) {
+ int curIter = 0;
+ wr.WriteLine("Times for {0}:", kv.Key);
+ foreach (double v in kv.Value) {
+ wr.WriteLine(" ({0})\t{1}ms", curIter, v);
+ total += v;
+ curIter++;
+ }
+ totalIters += curIter;
+ }
+ total = total / 1000.0;
+ wr.WriteLine("Total time: {0} (s)", total);
+ wr.WriteLine("Avg: {0} (s/iter)", total / totalIters);
+ }
+ }
+
+ public class HoudiniTimer : HoudiniObserver {
+ private DateTime startT;
+ private Implementation curImp;
+ private IterationTimer<string> times;
+ private TextWriter wr;
+
+ public HoudiniTimer(TextWriter wr) {
+ this.wr = wr;
+ times = new IterationTimer<string>();
+ }
+ public override void UpdateIteration() {
+ startT = DateTime.Now;
+ }
+ public override void UpdateImplementation(Implementation implementation) {
+ curImp = implementation;
+ }
+ public override void UpdateOutcome(ProverInterface.Outcome o) {
+ Contract.Assert(curImp != null);
+ DateTime endT = DateTime.Now;
+ times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique
+ }
+ public void PrintTimes() {
+ wr.WriteLine("-----------------------------------------");
+ wr.WriteLine("Times for each iteration for each procedure");
+ wr.WriteLine("-----------------------------------------");
+ times.PrintTimes(wr);
+ }
+ }
+
+ public class HoudiniTextReporter : HoudiniObserver {
+ private TextWriter wr;
+ private int currentIteration = -1;
+
+ public HoudiniTextReporter(TextWriter wr) {
+ this.wr = wr;
+ }
+ public override void UpdateStart(Program program, int numConstants) {
+ wr.WriteLine("Houdini started:" + program.ToString() + " #constants: " + numConstants.ToString());
+ currentIteration = -1;
+ wr.Flush();
+ }
+ public override void UpdateIteration() {
+ currentIteration++;
+ wr.WriteLine("---------------------------------------");
+ wr.WriteLine("Houdini iteration #" + currentIteration);
+ wr.Flush();
+ }
+ public override void UpdateImplementation(Implementation implementation) {
+ wr.WriteLine("implementation under analysis :" + implementation.Name);
+ wr.Flush();
+ }
+ public override void UpdateAssignment(Dictionary<string, bool> assignment) {
+ bool firstTime = true;
+ wr.Write("assignment under analysis : axiom (");
+ foreach (KeyValuePair<string, bool> kv in assignment) {
+ if (!firstTime) wr.Write(" && "); else firstTime = false;
+ string valString; // ugliness to get it lower cased
+ if (kv.Value) valString = "true"; else valString = "false";
+ wr.Write(kv.Key + " == " + valString);
+ }
+ wr.WriteLine(");");
+ wr.Flush();
+ }
+ public override void UpdateOutcome(ProverInterface.Outcome outcome) {
+ wr.WriteLine("analysis outcome :" + outcome);
+ wr.Flush();
+ }
+ public override void UpdateEnqueue(Implementation implementation) {
+ wr.WriteLine("worklist enqueue :" + implementation.Name);
+ wr.Flush();
+ }
+ public override void UpdateDequeue() {
+ wr.WriteLine("worklist dequeue");
+ wr.Flush();
+ }
+ public override void UpdateConstant(string constantName) {
+ wr.WriteLine("constant disabled : " + constantName);
+ wr.Flush();
+ }
+ public override void UpdateEnd(bool isNormalEnd) {
+ wr.WriteLine("Houdini ended: " + (isNormalEnd ? "Normal" : "Abnormal"));
+ wr.WriteLine("Number of iterations: " + (this.currentIteration + 1));
+ wr.Flush();
+ }
+ public override void UpdateFlushStart() {
+ wr.WriteLine("***************************************");
+ wr.WriteLine("Flushing remaining implementations");
+ wr.Flush();
+ }
+ public override void UpdateFlushFinish() {
+ wr.WriteLine("***************************************");
+ wr.WriteLine("Flushing finished");
+ wr.Flush();
+ }
+ public override void SeeException(string msg) {
+ wr.WriteLine("Caught exception: " + msg);
+ wr.Flush();
+ }
+
+ }
+
+
+ public abstract class ObservableHoudini {
+ private List<HoudiniObserver> observers = new List<HoudiniObserver>();
+
+ public void AddObserver(HoudiniObserver observer) {
+ if (!observers.Contains(observer))
+ observers.Add(observer);
+ }
+ private delegate void NotifyDelegate(HoudiniObserver observer);
+
+ private void Notify(NotifyDelegate notifyDelegate) {
+ foreach (HoudiniObserver observer in observers) {
+ notifyDelegate(observer);
+ }
+ }
+ protected void NotifyStart(Program program, int numConstants) {
+ NotifyDelegate notifyDelegate = (NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStart(program, numConstants); };
+ Notify(notifyDelegate);
+ }
+ protected void NotifyIteration() {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateIteration(); });
+ }
+ protected void NotifyImplementation(Implementation implementation) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateImplementation(implementation); });
+ }
+ protected void NotifyAssignment(Dictionary<string, bool> assignment) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); });
+ }
+ protected void NotifyOutcome(ProverInterface.Outcome outcome) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); });
+ }
+ protected void NotifyEnqueue(Implementation implementation) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateEnqueue(implementation); });
+ }
+ protected void NotifyDequeue() {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateDequeue(); });
+ }
+ protected void NotifyConstant(string constantName) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateConstant(constantName); });
+ }
+ protected void NotifyEnd(bool isNormalEnd) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateEnd(isNormalEnd); });
+ }
+ protected void NotifyFlushStart() {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateFlushStart(); });
+ }
+ protected void NotifyFlushFinish() {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateFlushFinish(); });
+ }
+
+ protected void NotifyException(string msg) {
+ Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.SeeException(msg); });
+ }
+ }
+
+ public class Houdini : ObservableHoudini {
+ private Program program;
+ private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;
+ private ReadOnlyDictionary<Implementation, HoudiniVCGen> vcgenSessions;
+ private Graph<Implementation> callGraph;
+ private bool continueAtError;
+
+ public Houdini(Program program, bool continueAtError) {
+ this.program = program;
+ this.callGraph = BuildCallGraph();
+ this.continueAtError = continueAtError;
+ this.houdiniConstants = CollectExistentialConstants();
+ this.vcgenSessions = PrepareVCGenSessions();
+ }
+
+ private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions() {
+ HashSet<Implementation> impls = new HashSet<Implementation>();
+ Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if (impl != null) {
+ impls.Add(impl);
+ }
+ }
+ foreach (Implementation impl in impls) {
+ // make a different simplify log file for each function
+ String simplifyLog = null;
+ if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
+ simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
+ }
+ HoudiniVCGen vcgen = new HoudiniVCGen(program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ vcgenSessions.Add(impl, vcgen);
+ }
+ return new ReadOnlyDictionary<Implementation, HoudiniVCGen>(vcgenSessions);
+ }
+
+ private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
+ Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Constant constant = decl as Constant;
+ if (constant != null) {
+ bool result = false;
+ if (constant.CheckBooleanAttribute("existential", ref result)) {
+ if (result == true)
+ existentialConstants.Add(constant.Name, new IdentifierExpr(Token.NoToken, constant));
+ }
+ }
+ }
+ return new ReadOnlyDictionary<string, IdentifierExpr>(existentialConstants);
+ }
+
+ private Graph<Implementation> BuildCallGraph() {
+ Graph<Implementation> callGraph = new Graph<Implementation>();
+ Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ procToImpls[proc] = new HashSet<Implementation>();
+ }
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ callGraph.AddSource(impl);
+ procToImpls[impl.Proc].Add(impl);
+ }
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ foreach (Block b in impl.Blocks) {
+ foreach (Cmd c in b.Cmds) {
+ CallCmd cc = c as CallCmd;
+ if (cc == null) continue;
+ foreach (Implementation callee in procToImpls[cc.Proc]) {
+ callGraph.AddEdge(impl, callee);
+ }
+ }
+ }
+ }
+ return callGraph;
+ }
+
+ private Queue<Implementation> BuildWorkList(Program program) {
+ Queue<Implementation> queue = new Queue<Implementation>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if (impl != null) {
+ queue.Enqueue(impl);
+ }
+ }
+ return queue;
+ }
+
+ private bool MatchCandidate(Expr boogieExpr, out string candidateConstant) {
+ candidateConstant = null;
+ IExpr antecedent;
+ IExpr expr = boogieExpr as IExpr;
+ if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {
+ IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;
+ if (constantFunApp != null && houdiniConstants.ContainsKey(constantFunApp.IdentifierExpr.Name)) {
+ candidateConstant = constantFunApp.IdentifierExpr.Name;
+ return true;
+ }
+ }
+ return false;
+ }
+
+ private VCExpr BuildAxiom(HoudiniVCGen vcgen, Dictionary<string, bool> currentAssignment) {
+ Boogie2VCExprTranslator exprTranslator = vcgen.BooogieExprTranslator;
+ VCExpressionGenerator exprGen = vcgen.VCExprGenerator;
+
+ VCExpr expr = VCExpressionGenerator.True;
+ foreach (KeyValuePair<string, bool> kv in currentAssignment) {
+ IdentifierExpr constantExpr;
+ houdiniConstants.TryGetValue(kv.Key, out constantExpr);
+ Contract.Assume(constantExpr != null);
+ VCExprVar exprVar = exprTranslator.LookupVariable(constantExpr.Decl);
+ if (kv.Value) {
+ expr = exprGen.And(expr, exprVar);
+ }
+ else {
+ expr = exprGen.And(expr, exprGen.Not(exprVar));
+ }
+ }
+ return expr;
+ }
+
+ private Dictionary<string, bool> BuildAssignment(Dictionary<string, IdentifierExpr>.KeyCollection constants) {
+ Dictionary<string, bool> initial = new Dictionary<string, bool>();
+ foreach (string constant in constants)
+ initial.Add(constant, true);
+ return initial;
+ }
+
+ private ProverInterface.Outcome VerifyUsingAxiom(Implementation implementation, VCExpr axiom, out List<Counterexample> errors) {
+ HoudiniVCGen vcgen;
+ vcgenSessions.TryGetValue(implementation, out vcgen);
+ if (vcgen == null)
+ throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
+ ProverInterface.Outcome outcome = TryCatchVerify(vcgen, axiom, out errors);
+ return outcome;
+ }
+
+ // the main procedure that checks a procedure and updates the
+ // assignment and the worklist
+ private ProverInterface.Outcome HoudiniVerifyCurrent(HoudiniState current,
+ Program program,
+ out List<Counterexample> errors,
+ out bool exc) {
+ HoudiniVCGen vcgen;
+ if (current.Implementation == null)
+ throw new Exception("HoudiniVerifyCurrent has null implementation");
+
+ Implementation implementation = current.Implementation;
+ vcgenSessions.TryGetValue(implementation, out vcgen);
+ if (vcgen == null)
+ throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
+
+ ProverInterface.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);
+ return outcome;
+ }
+
+ private ProverInterface.Outcome VerifyCurrent(HoudiniState current,
+ Program program,
+ out List<Counterexample> errors,
+ out bool exc) {
+ HoudiniVCGen vcgen;
+ if (current.Implementation != null) {
+ Implementation implementation = current.Implementation;
+ vcgenSessions.TryGetValue(implementation, out vcgen);
+ if (vcgen == null)
+ throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
+
+ ProverInterface.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);
+ return outcome;
+ }
+ else {
+ throw new Exception("VerifyCurrent has null implementation");
+ }
+ }
+
+ private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List<Counterexample> errors) {
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid:
+ return false;
+ case ProverInterface.Outcome.Invalid:
+ Contract.Assume(errors != null);
+ foreach (Counterexample error in errors) {
+ if (ExtractRefutedAnnotation(error) == null)
+ return true;
+ }
+ return false;
+ default:
+ return true;
+ }
+ }
+
+ // returns true if at least one of the violations is non-candidate
+ private bool AnyNonCandidateViolation(ProverInterface.Outcome outcome, List<Counterexample> errors) {
+ switch (outcome) {
+ case ProverInterface.Outcome.Invalid:
+ Contract.Assert(errors != null);
+ foreach (Counterexample error in errors) {
+ if (ExtractRefutedAnnotation(error) == null)
+ return true;
+ }
+ return false;
+ default:
+ return false;
+ }
+ }
+
+ private List<Counterexample> emptyList = new List<Counterexample>();
+
+ // Record most current Non-Candidate errors found by Boogie, etc.
+ private void UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,
+ Implementation implementation,
+ ProverInterface.Outcome verificationOutcome,
+ List<Counterexample> errors) {
+ string implName = implementation.ToString();
+ houdiniOutcome.implementationOutcomes.Remove(implName);
+ List<Counterexample> nonCandidateErrors = new List<Counterexample>();
+
+ switch (verificationOutcome) {
+ case ProverInterface.Outcome.Invalid:
+ Contract.Assume(errors != null);
+ foreach (Counterexample error in errors) {
+ if (ExtractRefutedAnnotation(error) == null)
+ nonCandidateErrors.Add(error);
+ }
+ break;
+ default:
+ break;
+ }
+ houdiniOutcome.implementationOutcomes.Add(implName, new VCGenOutcome(verificationOutcome, nonCandidateErrors));
+ }
+
+ private void FlushWorkList(HoudiniState current) {
+ this.NotifyFlushStart();
+ HoudiniVCGen vcgen;
+ vcgenSessions.TryGetValue(current.Implementation, out vcgen);
+ VCExpr axiom = BuildAxiom(vcgen, current.Assignment);
+ while (current.WorkList.Count > 0) {
+ this.NotifyIteration();
+
+ current.Implementation = current.WorkList.Peek();
+ this.NotifyImplementation(current.Implementation);
+
+ List<Counterexample> errors;
+ ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+ this.NotifyOutcome(outcome);
+
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+
+ }
+ this.NotifyFlushFinish();
+ }
+
+ private void UpdateAssignment(HoudiniState current, RefutedAnnotation refAnnot) {
+ current.Assignment.Remove(refAnnot.Constant);
+ current.Assignment.Add(refAnnot.Constant, false);
+ this.NotifyConstant(refAnnot.Constant);
+ }
+
+ private void AddToWorkList(HoudiniState current, Implementation imp) {
+ if (!current.WorkList.Contains(imp) && !current.isBlackListed(imp.Name)) {
+ current.WorkList.Enqueue(imp);
+ this.NotifyEnqueue(imp);
+ }
+ }
+
+ private void UpdateWorkList(HoudiniState current,
+ ProverInterface.Outcome outcome,
+ List<Counterexample> errors) {
+ Contract.Assume(current.Implementation != null);
+
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid:
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ break;
+ case ProverInterface.Outcome.Invalid:
+ Contract.Assume(errors != null);
+ bool dequeue = false;
+ foreach (Counterexample error in errors) {
+ RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+ if (refutedAnnotation != null) {
+ foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) { AddToWorkList(current, implementation); }
+ UpdateAssignment(current, refutedAnnotation);
+ }
+ else {
+ dequeue = true; //once one non-houdini error is hit dequeue?!
+ }
+ }
+ if (dequeue) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ }
+ break;
+ case ProverInterface.Outcome.TimeOut:
+ // TODO: reset session instead of blocking timed out funcs?
+ current.addToBlackList(current.Implementation.Name);
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ break;
+ case ProverInterface.Outcome.OutOfMemory:
+ case ProverInterface.Outcome.Undetermined:
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ break;
+ default:
+ throw new Exception("Unknown vcgen outcome");
+ }
+ }
+
+
+ private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) {
+ Contract.Assume(current.Implementation != null);
+ foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) {
+ AddToWorkList(current, implementation);
+ }
+ }
+
+
+ // Updates the worklist and current assignment
+ // @return true if the current function is kept on the queue
+ private bool UpdateAssignmentWorkList(HoudiniState current,
+ ProverInterface.Outcome outcome,
+ List<Counterexample> errors) {
+ Contract.Assume(current.Implementation != null);
+ bool dequeue = true;
+
+ switch (outcome) {
+ case ProverInterface.Outcome.Valid:
+ //yeah, dequeue
+ break;
+ case ProverInterface.Outcome.Invalid:
+ Contract.Assume(errors != null);
+ foreach (Counterexample error in errors) {
+ RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
+ if (refutedAnnotation != null) { // some candidate annotation removed
+ AddRelatedToWorkList(current, refutedAnnotation);
+ UpdateAssignment(current, refutedAnnotation);
+ dequeue = false;
+ }
+ }
+ break;
+
+ case ProverInterface.Outcome.TimeOut:
+ // TODO: reset session instead of blocking timed out funcs?
+ current.addToBlackList(current.Implementation.Name);
+ break;
+ case ProverInterface.Outcome.Undetermined:
+ case ProverInterface.Outcome.OutOfMemory:
+ break;
+ default:
+ throw new Exception("Unknown vcgen outcome");
+ }
+ if (dequeue) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ }
+ return !dequeue;
+ }
+
+ private class HoudiniState {
+ private Queue<Implementation> _workList;
+ private HashSet<string> blackList;
+ private Dictionary<string, bool> _assignment;
+ private Implementation _implementation;
+ private HoudiniOutcome _outcome;
+
+ public HoudiniState(Queue<Implementation> workList, Dictionary<string, bool> currentAssignment) {
+ this._workList = workList;
+ this._assignment = currentAssignment;
+ this._implementation = null;
+ this._outcome = new HoudiniOutcome();
+ this.blackList = new HashSet<string>();
+ }
+
+ public Queue<Implementation> WorkList {
+ get { return this._workList; }
+ }
+ public Dictionary<string, bool> Assignment {
+ get { return this._assignment; }
+ }
+ public Implementation Implementation {
+ get { return this._implementation; }
+ set { this._implementation = value; }
+ }
+ public HoudiniOutcome Outcome {
+ get { return this._outcome; }
+ }
+ public bool isBlackListed(string funcName) {
+ return blackList.Contains(funcName);
+ }
+ public void addToBlackList(string funcName) {
+ blackList.Add(funcName);
+ }
+ }
+
+ private void PrintBadList(string kind, List<string> list) {
+ if (list.Count != 0) {
+ Console.WriteLine("----------------------------------------");
+ Console.WriteLine("Functions: {0}", kind);
+ foreach (string fname in list) {
+ Console.WriteLine("\t{0}", fname);
+ }
+ Console.WriteLine("----------------------------------------");
+ }
+ }
+
+ private void PrintBadOutcomes(List<string> timeouts, List<string> inconc, List<string> errors) {
+ PrintBadList("TimedOut", timeouts);
+ PrintBadList("Inconclusive", inconc);
+ PrintBadList("Errors", errors);
+ }
+
+ public HoudiniOutcome VerifyProgram() {
+ HoudiniOutcome outcome = VerifyProgramSameFuncFirst();
+ PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);
+ return outcome;
+ }
+
+ // Old main loop
+ public HoudiniOutcome VerifyProgramUnorderedWork() {
+ HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
+ this.NotifyStart(program, houdiniConstants.Keys.Count);
+
+
+
+ while (current.WorkList.Count > 0) {
+ System.GC.Collect();
+ this.NotifyIteration();
+
+ HoudiniVCGen vcgen;
+ vcgenSessions.TryGetValue(current.Implementation, out vcgen);
+ VCExpr axiom = BuildAxiom(vcgen, current.Assignment);
+ this.NotifyAssignment(current.Assignment);
+
+ current.Implementation = current.WorkList.Peek();
+ this.NotifyImplementation(current.Implementation);
+
+ List<Counterexample> errors;
+ ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);
+ this.NotifyOutcome(outcome);
+
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+ if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ FlushWorkList(current);
+ }
+ else
+ UpdateWorkList(current, outcome, errors);
+ }
+ this.NotifyEnd(true);
+ current.Outcome.assignment = current.Assignment;
+ return current.Outcome;
+ }
+
+ // New main loop
+ public HoudiniOutcome VerifyProgramSameFuncFirst() {
+ HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
+ this.NotifyStart(program, houdiniConstants.Keys.Count);
+
+ while (current.WorkList.Count > 0) {
+ bool exceptional = false;
+ System.GC.Collect();
+ this.NotifyIteration();
+
+ current.Implementation = current.WorkList.Peek();
+ this.NotifyImplementation(current.Implementation);
+
+ List<Counterexample> errors;
+ ProverInterface.Outcome outcome = VerifyCurrent(current, program, out errors, out exceptional);
+
+ // updates to worklist already done in VerifyCurrent, unless there was an exception
+ if (exceptional) {
+ this.NotifyOutcome(outcome);
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+ if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ FlushWorkList(current);
+ }
+ else {
+ UpdateAssignmentWorkList(current, outcome, errors);
+ }
+ exceptional = false;
+ }
+ }
+ this.NotifyEnd(true);
+ current.Outcome.assignment = current.Assignment;
+ return current.Outcome;
+ }
+
+ //Clean houdini (Based on "Houdini Spec in Boogie" email 10/22/08
+ //Aborts when there is a violation of non-candidate assertion
+ //This can be used in eager mode (continueAfterError) by simply making
+ //all non-candidate annotations as unchecked (free requires/ensures, assumes)
+ public HoudiniOutcome PerformHoudiniInference() {
+ HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
+ this.NotifyStart(program, houdiniConstants.Keys.Count);
+
+ Console.WriteLine("Using the new houdini algorithm\n");
+
+ while (current.WorkList.Count > 0) {
+ bool exceptional = false;
+ System.GC.Collect();
+ this.NotifyIteration();
+
+ current.Implementation = current.WorkList.Peek();
+ this.NotifyImplementation(current.Implementation);
+
+ List<Counterexample> errors;
+ ProverInterface.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional);
+
+ // updates to worklist already done in VerifyCurrent, unless there was an exception
+ if (exceptional) {
+ this.NotifyOutcome(outcome);
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+ if (AnyNonCandidateViolation(outcome, errors)) { //abort
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ FlushWorkList(current);
+ }
+ else { //continue
+ UpdateAssignmentWorkList(current, outcome, errors);
+ }
+ }
+ }
+ this.NotifyEnd(true);
+ current.Outcome.assignment = current.Assignment;
+ return current.Outcome;
+ }
+
+ private List<Implementation> FindImplementationsToEnqueue(RefutedAnnotation refutedAnnotation, Implementation currentImplementation) {
+ List<Implementation> implementations = new List<Implementation>();
+ switch (refutedAnnotation.Kind) {
+ case RefutedAnnotationKind.REQUIRES:
+ foreach (Implementation callee in callGraph.Successors(currentImplementation)) {
+ Contract.Assume(callee.Proc != null);
+ if (callee.Proc.Equals(refutedAnnotation.CalleeProc))
+ implementations.Add(callee);
+ }
+ break;
+ case RefutedAnnotationKind.ENSURES:
+ foreach (Implementation caller in callGraph.Predecessors(currentImplementation))
+ implementations.Add(caller);
+ break;
+ case RefutedAnnotationKind.ASSERT: //the implementation is already in queue
+ break;
+ default:
+ throw new Exception("Unknown Refuted annotation kind:" + refutedAnnotation.Kind);
+ }
+ return implementations;
+ }
+
+ private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT };
+
+ private class RefutedAnnotation {
+ private string _constant;
+ private RefutedAnnotationKind _kind;
+ private Procedure _callee;
+
+ private RefutedAnnotation(string constant, RefutedAnnotationKind kind, Procedure callee) {
+ this._constant = constant;
+ this._kind = kind;
+ this._callee = callee;
+ }
+ public RefutedAnnotationKind Kind {
+ get { return this._kind; }
+ }
+ public string Constant {
+ get { return this._constant; }
+ }
+ public Procedure CalleeProc {
+ get { return this._callee; }
+ }
+ public static RefutedAnnotation BuildRefutedRequires(string constant, Procedure callee) {
+ return new RefutedAnnotation(constant, RefutedAnnotationKind.REQUIRES, callee);
+ }
+ public static RefutedAnnotation BuildRefutedEnsures(string constant) {
+ return new RefutedAnnotation(constant, RefutedAnnotationKind.ENSURES, null);
+ }
+ public static RefutedAnnotation BuildRefutedAssert(string constant) {
+ return new RefutedAnnotation(constant, RefutedAnnotationKind.ASSERT, null);
+ }
+
+ }
+
+ private void PrintRefutedCall(CallCounterexample err, XmlSink xmlOut) {
+ Expr cond = err.FailingRequires.Condition;
+ string houdiniConst;
+ if (MatchCandidate(cond, out houdiniConst)) {
+ xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);
+ }
+ }
+
+ private void PrintRefutedReturn(ReturnCounterexample err, XmlSink xmlOut) {
+ Expr cond = err.FailingEnsures.Condition;
+ string houdiniConst;
+ if (MatchCandidate(cond, out houdiniConst)) {
+ xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);
+ }
+ }
+
+ private void PrintRefutedAssert(AssertCounterexample err, XmlSink xmlOut) {
+ Expr cond = err.FailingAssert.OrigExpr;
+ string houdiniConst;
+ if (MatchCandidate(cond, out houdiniConst)) {
+ xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);
+ }
+ }
+
+
+ private void DebugRefutedCandidates(Implementation curFunc, List<Counterexample> errors) {
+ XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;
+ if (xmlRefuted != null && errors != null) {
+ DateTime start = DateTime.Now;
+ xmlRefuted.WriteStartMethod(curFunc.ToString(), start);
+
+ foreach (Counterexample error in errors) {
+ CallCounterexample ce = error as CallCounterexample;
+ if (ce != null) PrintRefutedCall(ce, xmlRefuted);
+ ReturnCounterexample re = error as ReturnCounterexample;
+ if (re != null) PrintRefutedReturn(re, xmlRefuted);
+ AssertCounterexample ae = error as AssertCounterexample;
+ if (ae != null) PrintRefutedAssert(ae, xmlRefuted);
+ }
+
+ DateTime end = DateTime.Now;
+ xmlRefuted.WriteEndMethod("errors", end, end.Subtract(start));
+ }
+ }
+
+ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {
+ string houdiniConstant;
+ CallCounterexample callCounterexample = error as CallCounterexample;
+ if (callCounterexample != null) {
+ Procedure failingProcedure = callCounterexample.FailingCall.Proc;
+ Requires failingRequires = callCounterexample.FailingRequires;
+ if (MatchCandidate(failingRequires.Condition, out houdiniConstant)) {
+ Contract.Assert(houdiniConstant != null);
+ return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure);
+ }
+ }
+ ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
+ if (returnCounterexample != null) {
+ Ensures failingEnsures = returnCounterexample.FailingEnsures;
+ if (MatchCandidate(failingEnsures.Condition, out houdiniConstant)) {
+ Contract.Assert(houdiniConstant != null);
+ return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant);
+ }
+ }
+ AssertCounterexample assertCounterexample = error as AssertCounterexample;
+ if (assertCounterexample != null) {
+ AssertCmd failingAssert = assertCounterexample.FailingAssert;
+ if (MatchCandidate(failingAssert.OrigExpr, out houdiniConstant)) {
+ Contract.Assert(houdiniConstant != null);
+ return RefutedAnnotation.BuildRefutedAssert(houdiniConstant);
+ }
+ }
+
+ return null;
+ }
+
+ private ProverInterface.Outcome TryCatchVerify(HoudiniVCGen vcgen, VCExpr axiom, out List<Counterexample> errors) {
+ ProverInterface.Outcome outcome;
+ try {
+ outcome = vcgen.Verify(axiom, out errors);
+ }
+ catch (VCGenException e) {
+ Contract.Assume(e != null);
+ errors = null;
+ outcome = ProverInterface.Outcome.Undetermined;
+ }
+ catch (UnexpectedProverOutputException upo) {
+ Contract.Assume(upo != null);
+ errors = null;
+ outcome = ProverInterface.Outcome.Undetermined;
+ }
+ return outcome;
+ }
+
+ //version of TryCatchVerify that spins on the same function
+ //as long as the current assignment is changing
+ private ProverInterface.Outcome TrySpinSameFunc(HoudiniState current,
+ Program program,
+ HoudiniVCGen vcgen,
+ out List<Counterexample> errors,
+ out bool exceptional) {
+ Contract.Assert(current.Implementation != null);
+ ProverInterface.Outcome outcome;
+ errors = null;
+ outcome = ProverInterface.Outcome.Undetermined;
+ try {
+ bool trySameFunc = true;
+ bool pastFirstIter = false; //see if this new loop is even helping
+
+ do {
+ if (pastFirstIter) {
+ System.GC.Collect();
+ this.NotifyIteration();
+ }
+
+ this.vcgenSessions.TryGetValue(current.Implementation, out vcgen);
+ VCExpr currentAx = BuildAxiom(vcgen, current.Assignment);
+ this.NotifyAssignment(current.Assignment);
+
+ outcome = vcgen.Verify(currentAx, out errors);
+ this.NotifyOutcome(outcome);
+
+ DebugRefutedCandidates(current.Implementation, errors);
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+ if (!continueAtError && IsOutcomeNotHoudini(outcome, errors)) {
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ trySameFunc = false;
+ FlushWorkList(current);
+ }
+ else {
+ trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
+ //reset for the next round
+ errors = null;
+ outcome = ProverInterface.Outcome.Undetermined;
+ }
+ pastFirstIter = true;
+ } while (trySameFunc && current.WorkList.Count > 0);
+
+ }
+ catch (VCGenException e) {
+ Contract.Assume(e != null);
+ NotifyException("VCGen");
+ exceptional = true;
+ return outcome;
+ }
+ catch (UnexpectedProverOutputException upo) {
+ Contract.Assume(upo != null);
+ NotifyException("UnexpectedProverOutput");
+ exceptional = true;
+ return outcome;
+ }
+ exceptional = false;
+ return outcome;
+ }
+
+ //Similar to TrySpinSameFunc except no Candidate logic
+ private ProverInterface.Outcome HoudiniVerifyCurrentAux(HoudiniState current,
+ Program program,
+ HoudiniVCGen vcgen,
+ out List<Counterexample> errors,
+ out bool exceptional) {
+ Contract.Assert(current.Implementation != null);
+ ProverInterface.Outcome outcome;
+ errors = null;
+ outcome = ProverInterface.Outcome.Undetermined;
+ try {
+ bool trySameFunc = true;
+ bool pastFirstIter = false; //see if this new loop is even helping
+
+ do {
+ if (pastFirstIter) {
+ System.GC.Collect();
+ this.NotifyIteration();
+ }
+
+ VCExpr currentAx = BuildAxiom(vcgen, current.Assignment);
+ this.NotifyAssignment(current.Assignment);
+
+ //check the VC with the current assignment
+ outcome = vcgen.Verify(currentAx, out errors);
+ this.NotifyOutcome(outcome);
+
+ DebugRefutedCandidates(current.Implementation, errors);
+ UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
+
+ if (AnyNonCandidateViolation(outcome, errors)) { //abort
+ current.WorkList.Dequeue();
+ this.NotifyDequeue();
+ trySameFunc = false;
+ FlushWorkList(current);
+ }
+ else { //continue
+ trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
+ //reset for the next round
+ errors = null;
+ outcome = ProverInterface.Outcome.Undetermined;
+ }
+ pastFirstIter = true;
+ } while (trySameFunc && current.WorkList.Count > 0);
+
+ }
+ catch (VCGenException e) {
+ Contract.Assume(e != null);
+ NotifyException("VCGen");
+ exceptional = true;
+ return outcome;
+ }
+ catch (UnexpectedProverOutputException upo) {
+ Contract.Assume(upo != null);
+ NotifyException("UnexpectedProverOutput");
+ exceptional = true;
+ return outcome;
+ }
+ exceptional = false;
+ return outcome;
+ }
+ }
+
+ public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted }
+
+ public class VCGenOutcome {
+ public ProverInterface.Outcome outcome;
+ public List<Counterexample> errors;
+ public VCGenOutcome(ProverInterface.Outcome outcome, List<Counterexample> errors) {
+ this.outcome = outcome;
+ this.errors = errors;
+ }
+ }
+
+ public class HoudiniOutcome {
+ // final assignment
+ public Dictionary<string, bool> assignment = new Dictionary<string, bool>();
+ // boogie errors
+ public Dictionary<string, VCGenOutcome> implementationOutcomes = new Dictionary<string, VCGenOutcome>();
+ // outcome kind
+ public HoudiniOutcomeKind kind;
+
+ // statistics
+
+ private int CountResults(ProverInterface.Outcome outcome) {
+ int outcomeCount = 0;
+ foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) {
+ if (verifyOutcome.outcome == outcome)
+ outcomeCount++;
+ }
+ return outcomeCount;
+ }
+
+ private List<string> ListOutcomeMatches(ProverInterface.Outcome outcome) {
+ List<string> result = new List<string>();
+ foreach (KeyValuePair<string, VCGenOutcome> kvpair in implementationOutcomes) {
+ if (kvpair.Value.outcome == outcome)
+ result.Add(kvpair.Key);
+ }
+ return result;
+ }
+
+ public int ErrorCount {
+ get {
+ return CountResults(ProverInterface.Outcome.Invalid);
+ }
+ }
+ public int Verified {
+ get {
+ return CountResults(ProverInterface.Outcome.Valid);
+ }
+ }
+ public int Inconclusives {
+ get {
+ return CountResults(ProverInterface.Outcome.Undetermined);
+ }
+ }
+ public int TimeOuts {
+ get {
+ return CountResults(ProverInterface.Outcome.TimeOut);
+ }
+ }
+ public List<string> ListOfTimeouts {
+ get {
+ return ListOutcomeMatches(ProverInterface.Outcome.TimeOut);
+ }
+ }
+ public List<string> ListOfInconclusives {
+ get {
+ return ListOutcomeMatches(ProverInterface.Outcome.Undetermined);
+ }
+ }
+ public List<string> ListOfErrors {
+ get {
+ return ListOutcomeMatches(ProverInterface.Outcome.Invalid);
+ }
+ }
+ }
+
+}
diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj new file mode 100644 index 00000000..bd4e693b --- /dev/null +++ b/Source/Houdini/Houdini.csproj @@ -0,0 +1,105 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>8.0.30703</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Microsoft.Boogie.Houdini</RootNamespace>
+ <AssemblyName>Houdini</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup>
+ <SignAssembly>true</SignAssembly>
+ </PropertyGroup>
+ <PropertyGroup>
+ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Xml.Linq" />
+ <Reference Include="System.Data.DataSetExtensions" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="Checker.cs" />
+ <Compile Include="Houdini.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\AIFramework\AIFramework.csproj">
+ <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
+ <Name>AIFramework</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
+ <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+ <Name>CodeContractsExtender</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Core\Core.csproj">
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Graph\Graph.csproj">
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
+ <Name>Graph</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+ <Name>ParserHelper</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Provers\Simplify\Simplify.csproj">
+ <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
+ <Name>Simplify</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Provers\Z3\Z3.csproj">
+ <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
+ <Name>Z3</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\VCExpr\VCExpr.csproj">
+ <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
+ <Name>VCExpr</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+ <Name>VCGeneration</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <Folder Include="Properties\" />
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/Source/Houdini/Houdini.ssc b/Source/Houdini/Houdini.ssc deleted file mode 100644 index bd8348be..00000000 --- a/Source/Houdini/Houdini.ssc +++ /dev/null @@ -1,1188 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using Microsoft.Contracts;
-using System.Collections.Generic;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify.AST;
-using VC;
-using Microsoft.Boogie.Z3;
-using Microsoft.AbstractInterpretationFramework;
-using Microsoft.Boogie.AbstractInterpretation;
-using System.Collections;
-using System.Compiler;
-using System.IO;
-
-namespace Microsoft.Boogie.Houdini
-{
-
- class ReadOnlyDictionary<K,V> {
- private Dictionary<K,V>! dictionary;
- public ReadOnlyDictionary(Dictionary<K,V>! dictionary) {
- this.dictionary = dictionary;
- }
-
- public Dictionary<K,V>.KeyCollection Keys {
- get { return this.dictionary.Keys; }
- }
-
- public bool TryGetValue(K k, out V? v) {
- return this.dictionary.TryGetValue(k, out v);
- }
-
- public bool ContainsKey(K k) {
- return this.dictionary.ContainsKey(k);
- }
- }
-
- public class CallGraph {
-
- private IGraphNavigator! aiCallGraph;
-
- public CallGraph(IGraphNavigator! aiCallGraph) {
- this.aiCallGraph = aiCallGraph;
- }
-
- public IEnumerable! PreviousNodes(Implementation! n) {
- return (!)this.aiCallGraph.PreviousNodes(n);
- }
- public IEnumerable! NextNodes(Implementation! n) {
- return (!)this.aiCallGraph.NextNodes(n);
- }
-
- }
-
- public abstract class HoudiniObserver {
- public virtual void UpdateStart(Program! program, int numConstants) {}
- public virtual void UpdateIteration() {}
- public virtual void UpdateImplementation(Implementation! implementation) {}
- public virtual void UpdateAssignment(Dictionary<string!,bool>! assignment) {}
- public virtual void UpdateOutcome(VCGen.Outcome outcome) {}
- public virtual void UpdateEnqueue(Implementation! implementation) {}
- public virtual void UpdateDequeue() {}
- public virtual void UpdateConstant(string! constantName) {}
- public virtual void UpdateEnd(bool isNormalEnd) {}
- public virtual void UpdateFlushStart() {}
- public virtual void UpdateFlushFinish() {}
- public virtual void SeeException(string! msg){}
- }
-
- public class IterationTimer <K> {
- private Dictionary<K, List<double>!>! times;
-
- public IterationTimer () {
- times = new Dictionary<K, List<double>!>();
- }
-
- public void AddTime(K key, double timeMS) {
- List<double> oldList;
- times.TryGetValue(key, out oldList);
- if (oldList == null) {
- oldList = new List<double>();
- } else {
- times.Remove(key);
- }
- oldList.Add(timeMS);
- times.Add(key, oldList);
- }
-
- public void PrintTimes(TextWriter! wr) {
- wr.WriteLine ("Total procedures: {0}", times.Count);
- double total = 0;
- int totalIters = 0;
- foreach(KeyValuePair<K, List<double>!> kv in times) {
- int curIter = 0;
- wr.WriteLine("Times for {0}:", kv.Key);
- foreach(double v in kv.Value) {
- wr.WriteLine(" ({0})\t{1}ms", curIter, v);
- total += v;
- curIter++;
- }
- totalIters += curIter;
- }
- total = total / 1000.0;
- wr.WriteLine ("Total time: {0} (s)", total);
- wr.WriteLine ("Avg: {0} (s/iter)", total/totalIters);
- }
- }
-
- public class HoudiniTimer : HoudiniObserver {
- private DateTime startT;
- private Implementation curImp;
- private IterationTimer<string!>! times;
- private TextWriter! wr;
-
- public HoudiniTimer(TextWriter! wr) {
- this.wr = wr;
- times = new IterationTimer<string!>();
- }
- public override void UpdateIteration() {
- startT = DateTime.Now;
- }
- public override void UpdateImplementation(Implementation! implementation){
- curImp = implementation;
- }
- public override void UpdateOutcome (VCGen.Outcome o) {
- assert curImp != null;
- DateTime endT = DateTime.Now;
- times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique
- }
- public void PrintTimes() {
- wr.WriteLine("-----------------------------------------");
- wr.WriteLine("Times for each iteration for each procedure");
- wr.WriteLine("-----------------------------------------");
- times.PrintTimes(wr);
- }
- }
-
- public class HoudiniTextReporter: HoudiniObserver {
- private TextWriter! wr;
- private int currentIteration = -1;
-
- public HoudiniTextReporter(TextWriter! wr) {
- this.wr = wr;
- }
- public override void UpdateStart(Program! program, int numConstants) {
- wr.WriteLine("Houdini started:" + program.ToString() + " #constants: " + numConstants.ToString());
- currentIteration = -1;
- wr.Flush();
- }
- public override void UpdateIteration() {
- currentIteration++;
- wr.WriteLine("---------------------------------------");
- wr.WriteLine("Houdini iteration #" + currentIteration);
- wr.Flush();
- }
- public override void UpdateImplementation(Implementation! implementation){
- wr.WriteLine("implementation under analysis :" + implementation.Name);
- wr.Flush();
- }
- public override void UpdateAssignment(Dictionary<string!,bool>! assignment) {
- bool firstTime = true;
- wr.Write("assignment under analysis : axiom (");
- foreach (KeyValuePair<string!,bool> kv in assignment) {
- if (!firstTime) wr.Write(" && "); else firstTime = false;
- string! valString; // ugliness to get it lower cased
- if (kv.Value) valString = "true"; else valString = "false";
- wr.Write(kv.Key + " == " + valString);
- }
- wr.WriteLine(");");
- wr.Flush();
- }
- public override void UpdateOutcome(VCGen.Outcome outcome) {
- wr.WriteLine("analysis outcome :" + outcome);
- wr.Flush();
- }
- public override void UpdateEnqueue(Implementation! implementation) {
- wr.WriteLine("worklist enqueue :" + implementation.Name);
- wr.Flush();
- }
- public override void UpdateDequeue() {
- wr.WriteLine("worklist dequeue");
- wr.Flush();
- }
- public override void UpdateConstant(string! constantName) {
- wr.WriteLine("constant disabled : " + constantName);
- wr.Flush();
- }
- public override void UpdateEnd(bool isNormalEnd) {
- wr.WriteLine("Houdini ended: " + (isNormalEnd ? "Normal" : "Abnormal"));
- wr.WriteLine("Number of iterations: " + (this.currentIteration+1));
- wr.Flush();
- }
- public override void UpdateFlushStart() {
- wr.WriteLine("***************************************");
- wr.WriteLine("Flushing remaining implementations");
- wr.Flush();
- }
- public override void UpdateFlushFinish() {
- wr.WriteLine("***************************************");
- wr.WriteLine("Flushing finished");
- wr.Flush();
- }
- public override void SeeException(string! msg) {
- wr.WriteLine("Caught exception: " + msg);
- wr.Flush();
- }
-
- }
-
-
- public abstract class ObservableHoudini {
- private List<HoudiniObserver!>! observers= new List<HoudiniObserver!>();
-
- public void AddObserver(HoudiniObserver! observer) {
- if (!observers.Contains(observer))
- observers.Add(observer);
- }
- private delegate void NotifyDelegate(HoudiniObserver! observer);
-
- private void Notify(NotifyDelegate! notifyDelegate) {
- foreach (HoudiniObserver! observer in observers) {
- notifyDelegate(observer);
- }
- }
- protected void NotifyStart(Program! program, int numConstants) {
- NotifyDelegate notifyDelegate = (NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateStart(program, numConstants); };
- Notify(notifyDelegate);
- }
- protected void NotifyIteration() {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateIteration(); });
- }
- protected void NotifyImplementation(Implementation! implementation) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateImplementation(implementation); });
- }
- protected void NotifyAssignment(Dictionary<string!,bool>! assignment) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateAssignment(assignment); });
- }
- protected void NotifyOutcome(VCGen.Outcome outcome) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateOutcome(outcome); });
- }
- protected void NotifyEnqueue(Implementation! implementation){
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateEnqueue(implementation); });
- }
- protected void NotifyDequeue(){
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateDequeue(); });
- }
- protected void NotifyConstant(string! constantName){
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateConstant(constantName); });
- }
- protected void NotifyEnd(bool isNormalEnd) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateEnd(isNormalEnd); });
- }
- protected void NotifyFlushStart() {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateFlushStart(); });
- }
- protected void NotifyFlushFinish() {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.UpdateFlushFinish(); });
- }
-
- protected void NotifyException(string! msg) {
- Notify((NotifyDelegate) delegate (HoudiniObserver! r) { r.SeeException(msg); });
- }
- }
-
- public enum HoudiniProver { Z3, Z3API }
-
- public class Houdini : ObservableHoudini {
-
- private Program! program;
-
- private ReadOnlyDictionary<string!,IdentifierExpr!>! houdiniConstants;
- private ReadOnlyDictionary<Implementation!,HdnVCGen!>! vcgenSessions;
- private CallGraph! callGraph;
- private bool continueAtError;
- private HoudiniProver houdiniProver;
- private HdnVCGenFactory! vcgenFactory;
-
- public Houdini(Program! program, CallGraph! callgraph, bool continueAtError, HoudiniProver houdiniProver) {
- this.program=program;
- this.callGraph = callgraph;
- this.continueAtError = continueAtError;
- this.houdiniProver = houdiniProver;
- HdnVCGenFactory factory;
- switch (this.houdiniProver) {
- case HoudiniProver.Z3:
- factory = new Z3HdnVCGenFactory();
- break;
- case HoudiniProver.Z3API:
- default:
- factory = new Z3APIHdnVCGenFactory();
- break;
- }
- this.vcgenFactory = factory;
- HoudiniHelper helper = new HoudiniHelper(factory);
- this.houdiniConstants = helper.CollectExistentialConstants(program);
- this.vcgenSessions = helper.PrepareVCGenSessions(program);
- }
-
- private Queue<Implementation!>! BuildWorkList(Program! program) {
- Queue<Implementation!>! queue = new Queue<Implementation!>();
- foreach ( Declaration! decl in program.TopLevelDeclarations ) {
- Implementation impl = decl as Implementation;
- if (impl!=null) {
- queue.Enqueue(impl);
- }
- }
- return queue;
- }
-
- private class HoudiniHelper {
- private HdnVCGenFactory! vcgenFactory;
- public HoudiniHelper(HdnVCGenFactory! vcgenFactory) {
- this.vcgenFactory = vcgenFactory;
- }
-
- public ReadOnlyDictionary<Implementation!,HdnVCGen!>! PrepareVCGenSessions(Program! program) {
- Dictionary<Implementation!,HdnVCGen!>! vcgenSessions = new Dictionary<Implementation!,HdnVCGen!>();
-
- foreach ( Declaration! decl in program.TopLevelDeclarations ) {
- Implementation impl = decl as Implementation;
- if (impl!=null) {
- // make a different simplify log file for each function
- String simplifyLog = null;
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
- simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
- }
- HdnVCGen! vcgen = vcgenFactory.BuildVCGen(program, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
- vcgen.PrepareVerification(impl,program);
- vcgenSessions.Add(impl,vcgen);
- }
- }
- return new ReadOnlyDictionary<Implementation!,HdnVCGen!>(vcgenSessions);
- }
-
- public ReadOnlyDictionary<string!,IdentifierExpr!>! CollectExistentialConstants(Program! program) {
- Dictionary<string!,IdentifierExpr!>! existentialConstants = new Dictionary<string!,IdentifierExpr!>();
- foreach ( Declaration! decl in program.TopLevelDeclarations ) {
- Constant constant = decl as Constant;
- if (constant!=null) {
- bool result=false;
- if (constant.CheckBooleanAttribute("existential",ref result)) {
- if (result==true)
- existentialConstants.Add(constant.Name, new IdentifierExpr(Token.NoToken,constant));
- }
- }
- }
- return new ReadOnlyDictionary<string!,IdentifierExpr!>(existentialConstants);
- }
- }
-
- private bool MatchCandidate(Expr boogieExpr, out string candidateConstant) {
- candidateConstant = null;
- IExpr antecedent;
- IExpr expr = boogieExpr as IExpr;
- if (expr!=null && ExprUtil.Match(expr, Prop.Implies, out antecedent)) {
- IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp;
- if ((constantFunApp !=null) && (houdiniConstants.ContainsKey(constantFunApp.IdentifierExpr.Name))) {
- candidateConstant = constantFunApp.IdentifierExpr.Name;
- return true;
- }
- }
- return false;
- }
-
-
- private Axiom! BuildAxiom(Dictionary<string!,bool>! currentAssignment) {
- Expr axiom = null;
- foreach (KeyValuePair<string!,bool> kv in currentAssignment) {
- IdentifierExpr constantExpr;
- houdiniConstants.TryGetValue(kv.Key,out constantExpr);
- assume (constantExpr!=null);
- Expr valueExpr = new LiteralExpr(Token.NoToken, kv.Value);
- Expr constantAssignment = Expr.Binary(Token.NoToken,BinaryOperator.Opcode.Eq,constantExpr,valueExpr);
- if (axiom==null)
- axiom = constantAssignment;
- else
- axiom = Expr.Binary(Token.NoToken,BinaryOperator.Opcode.And,axiom,constantAssignment);
- }
- if (axiom==null)
- axiom = new LiteralExpr(Token.NoToken, true);
- return new Axiom(Token.NoToken,axiom);
- }
-
- private Dictionary<string!,bool>! BuildAssignment(Dictionary<string!,IdentifierExpr!>.KeyCollection! constants) {
- Dictionary<string!,bool>! initial = new Dictionary<string!,bool>();
- foreach (string! constant in constants)
- initial.Add(constant,true);
- return initial;
- }
-
- private VCGen.Outcome VerifyUsingAxiom(Implementation! implementation, Axiom! axiom, out List<Counterexample!>? errors) {
- HdnVCGen vcgen;
- vcgenSessions.TryGetValue(implementation,out vcgen);
- if(vcgen==null)
- throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
- vcgen.PushAxiom(axiom);
- VCGen.Outcome outcome = TryCatchVerify(vcgen, out errors);
- vcgen.Pop();
- return outcome;
- }
-
- // the main procedure that checks a procedure and updates the
- // assignment and the worklist
- private VCGen.Outcome HoudiniVerifyCurrent(HoudiniState! current,
- Program! program,
- out List<Counterexample!>? errors,
- out bool exc) {
- HdnVCGen vcgen;
- if (current.Implementation == null)
- throw new Exception("HoudiniVerifyCurrent has null implementation");
-
- Implementation! implementation = current.Implementation;
- vcgenSessions.TryGetValue(implementation,out vcgen);
- if(vcgen==null)
- throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
-
- VCGen.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);
- return outcome;
- }
-
- private VCGen.Outcome VerifyCurrent(HoudiniState! current,
- Program! program,
- out List<Counterexample!>? errors,
- out bool exc) {
- HdnVCGen vcgen;
- if (current.Implementation != null) {
- Implementation! implementation = current.Implementation;
- vcgenSessions.TryGetValue(implementation,out vcgen);
- if(vcgen==null)
- throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);
-
- VCGen.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);
- return outcome;
- } else {
- throw new Exception("VerifyCurrent has null implementation");
- }
- }
-
- private bool IsOutcomeNotHoudini(VCGen.Outcome outcome, List<Counterexample!>? errors) {
- switch (outcome) {
- case VCGen.Outcome.Correct:
- return false;
- break;
- case VCGen.Outcome.Errors:
- assume (errors!=null);
- foreach (Counterexample error in errors) {
- if (ExtractRefutedAnnotation(error)==null)
- return true;
- }
- return false;
- break;
- case VCGen.Outcome.TimedOut:
- case VCGen.Outcome.Inconclusive:
- default:
- return true;
- break;
- }
- }
-
-
- // returns true if at least one of the violations is non-candidate
- private bool AnyNonCandidateViolation(VCGen.Outcome outcome, List<Counterexample!>? errors) {
- switch (outcome) {
- case VCGen.Outcome.Errors:
- assert (errors!=null);
- foreach (Counterexample error in errors) {
- if (ExtractRefutedAnnotation(error)==null)
- return true;
- }
- return false;
- break;
- case VCGen.Outcome.Correct:
- case VCGen.Outcome.TimedOut:
- case VCGen.Outcome.Inconclusive:
- default:
- return false;
- break;
- }
- }
-
-
- private List<Counterexample!> emptyList = new List<Counterexample!>();
-
- // Record most current Non-Candidate errors found by Boogie, etc.
- private void UpdateHoudiniOutcome(HoudiniOutcome! houdiniOutcome,
- Implementation! implementation,
- VCGen.Outcome verificationOutcome,
- List<Counterexample!>? errors) {
- string! implName = implementation.ToString();
- houdiniOutcome.implementationOutcomes.Remove(implName);
- List<Counterexample!> nonCandidateErrors = new List<Counterexample!>();
-
- switch (verificationOutcome) {
- case VCGen.Outcome.Errors:
- assume (errors!=null);
- foreach (Counterexample! error in errors) {
- if (ExtractRefutedAnnotation(error)==null)
- nonCandidateErrors.Add(error);
- }
- break;
- case VCGen.Outcome.TimedOut:
- case VCGen.Outcome.Correct:
- case VCGen.Outcome.Inconclusive:
- default:
- break;
- }
- houdiniOutcome.implementationOutcomes.Add(implName,
- new VCGenOutcome(verificationOutcome, nonCandidateErrors));
-
- }
-
- private void FlushWorkList(HoudiniState! current) {
- this.NotifyFlushStart();
- Axiom axiom = BuildAxiom(current.Assignment);
- while (current.WorkList.Count>0) {
- this.NotifyIteration();
-
- current.Implementation= current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample!>? errors;
- VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation,axiom,out errors);
- UpdateHoudiniOutcome(current.Outcome,current.Implementation,outcome,errors);
- this.NotifyOutcome(outcome);
-
- current.WorkList.Dequeue();
- this.NotifyDequeue();
-
- }
- this.NotifyFlushFinish();
- }
-
- private void UpdateAssignment(HoudiniState! current, RefutedAnnotation! refAnnot){
- current.Assignment.Remove(refAnnot.Constant);
- current.Assignment.Add(refAnnot.Constant,false);
- this.NotifyConstant(refAnnot.Constant);
- }
-
- private void AddToWorkList(HoudiniState! current, Implementation! imp) {
- if (!current.WorkList.Contains(imp) && !current.isBlackListed(imp.Name)) {
- current.WorkList.Enqueue(imp);
- this.NotifyEnqueue(imp);
- }
- }
-
- private void UpdateWorkList(HoudiniState! current,
- VCGen.Outcome outcome,
- List<Counterexample!>? errors) {
- assume (current.Implementation!=null);
-
- switch (outcome) {
- case VCGen.Outcome.Correct:
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- break;
- case VCGen.Outcome.Errors:
- assume (errors!=null);
- bool dequeue = false;
- foreach (Counterexample! error in errors) {
- RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
- if (refutedAnnotation!=null) {
- foreach (Implementation! implementation in FindImplementationsToEnqueue(refutedAnnotation,current.Implementation))
- { AddToWorkList(current, implementation); }
- UpdateAssignment(current, refutedAnnotation);
- }
- else {
- dequeue = true; //once one non-houdini error is hit dequeue?!
- }
- }
- if (dequeue) {
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- }
- break;
- case VCGen.Outcome.TimedOut:
- // TODO: reset session instead of blocking timed out funcs?
- current.addToBlackList(current.Implementation.Name);
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- break;
- case VCGen.Outcome.OutOfMemory:
- case VCGen.Outcome.Inconclusive:
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- break;
- default:
- throw new Exception("Unknown vcgen outcome");
- }
- }
-
-
- private void AddRelatedToWorkList(HoudiniState! current, RefutedAnnotation! refutedAnnotation) {
- assume (current.Implementation != null);
- foreach (Implementation! implementation in FindImplementationsToEnqueue(refutedAnnotation,current.Implementation)) {
- AddToWorkList(current, implementation);
- }
- }
-
-
- // Updates the worklist and current assignment
- // @return true if the current function is kept on the queue
- private bool UpdateAssignmentWorkList(HoudiniState! current,
- VCGen.Outcome outcome,
- List<Counterexample!>? errors) {
- assume (current.Implementation!=null);
- bool dequeue = true;
-
- switch (outcome) {
- case VCGen.Outcome.Correct:
- //yeah, dequeue
- break;
- case VCGen.Outcome.Errors:
- assume (errors!=null);
- foreach (Counterexample! error in errors) {
- RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
- if (refutedAnnotation!=null) { // some candidate annotation removed
- AddRelatedToWorkList(current, refutedAnnotation);
- UpdateAssignment(current, refutedAnnotation);
- dequeue = false;
- }
- }
- break;
-
- case VCGen.Outcome.TimedOut:
- // TODO: reset session instead of blocking timed out funcs?
- current.addToBlackList(current.Implementation.Name);
- break;
- case VCGen.Outcome.Inconclusive:
- case VCGen.Outcome.OutOfMemory:
- break;
- default:
- throw new Exception("Unknown vcgen outcome");
- }
- if (dequeue) {
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- }
- return !dequeue;
- }
-
-
-
- private class HoudiniState {
- private Queue<Implementation!>! _workList;
- private Set<string!>! blackList;
- private Dictionary<string!,bool>! _assignment;
- private Implementation _implementation;
- private HoudiniOutcome! _outcome;
-
- public HoudiniState(Queue<Implementation!>! workList, Dictionary<string!,bool>! currentAssignment) {
- this._workList = workList;
- this._assignment = currentAssignment;
- this._implementation = null;
- this._outcome = new HoudiniOutcome();
- this.blackList = new Set<string!>();
- }
-
- public Queue<Implementation!>! WorkList {
- get { return this._workList; }
- }
- public Dictionary<string!,bool>! Assignment {
- get { return this._assignment; }
- }
- public Implementation Implementation {
- get { return this._implementation; }
- set { this._implementation = value; }
- }
- public HoudiniOutcome! Outcome {
- get { return this._outcome; }
- }
- public bool isBlackListed(string! funcName) {
- return blackList.Contains(funcName);
- }
- public void addToBlackList(string! funcName) {
- blackList.Add(funcName);
- }
- }
-
- private void PrintBadList(string kind, List<string!>! list) {
- if(list.Count != 0) {
- Console.WriteLine("----------------------------------------");
- Console.WriteLine("Functions: {0}", kind);
- foreach(string! fname in list) {
- Console.WriteLine("\t{0}", fname);
- }
- Console.WriteLine("----------------------------------------");
- }
- }
-
- private void PrintBadOutcomes(List<string!>! timeouts, List<string!>! inconc, List<string!>! errors) {
- PrintBadList("TimedOut", timeouts);
- PrintBadList("Inconclusive", inconc);
- PrintBadList("Errors", errors);
- }
-
- public HoudiniOutcome! VerifyProgram (Program! program) {
- HoudiniOutcome outcome;
- switch (this.houdiniProver) {
- case HoudiniProver.Z3:
- outcome = VerifyProgramSameFuncFirst(program);
- //outcome = PerformHoudiniInference(program);
- break;
- case HoudiniProver.Z3API: // not that stable
- outcome = VerifyProgramUnorderedWork(program);
- break;
- default:
- throw new Exception("Unknown HoudiniProver: " + this.houdiniProver.ToString());
- }
- PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);
- return outcome;
- }
-
- // Old main loop
- public HoudiniOutcome! VerifyProgramUnorderedWork (Program! program) {
- HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment((!)houdiniConstants.Keys));
- this.NotifyStart(program, houdiniConstants.Keys.Count);
-
- while (current.WorkList.Count>0) {
- System.GC.Collect();
- this.NotifyIteration();
-
- Axiom axiom = BuildAxiom(current.Assignment);
- this.NotifyAssignment(current.Assignment);
-
- current.Implementation= current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample!>? errors;
- VCGen.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out errors);
- this.NotifyOutcome(outcome);
-
- UpdateHoudiniOutcome(current.Outcome,current.Implementation,outcome,errors);
- if (IsOutcomeNotHoudini(outcome,errors) && !continueAtError) {
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- FlushWorkList(current);
- } else
- UpdateWorkList(current,outcome,errors);
- }
- this.NotifyEnd(true);
- current.Outcome.assignment = current.Assignment;
- return current.Outcome;
- }
-
- // New main loop
- public HoudiniOutcome! VerifyProgramSameFuncFirst (Program! program) {
- HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment((!)houdiniConstants.Keys));
- this.NotifyStart(program, houdiniConstants.Keys.Count);
-
- while (current.WorkList.Count>0) {
- bool exceptional = false;
- System.GC.Collect();
- this.NotifyIteration();
-
- current.Implementation = current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample!>? errors;
- VCGen.Outcome outcome = VerifyCurrent(current, program, out errors, out exceptional);
-
- // updates to worklist already done in VerifyCurrent, unless there was an exception
- if (exceptional) {
- this.NotifyOutcome(outcome);
- UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
- if (IsOutcomeNotHoudini(outcome,errors) && !continueAtError){
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- FlushWorkList(current);
- } else {
- UpdateAssignmentWorkList(current, outcome, errors);
- }
- exceptional = false;
- }
- }
- this.NotifyEnd(true);
- current.Outcome.assignment = current.Assignment;
- return current.Outcome;
- }
-
- //Clean houdini (Based on "Houdini Spec in Boogie" email 10/22/08
- //Aborts when there is a violation of non-candidate assertion
- //This can be used in eager mode (continueAfterError) by simply making
- //all non-candidate annotations as unchecked (free requires/ensures, assumes)
- public HoudiniOutcome! PerformHoudiniInference(Program! program) {
- HoudiniState current = new HoudiniState(BuildWorkList(program),BuildAssignment((!)houdiniConstants.Keys));
- this.NotifyStart(program, houdiniConstants.Keys.Count);
-
- Console.WriteLine("Using the new houdini algorithm\n");
-
- while (current.WorkList.Count > 0) {
- bool exceptional = false;
- System.GC.Collect();
- this.NotifyIteration();
-
- current.Implementation = current.WorkList.Peek();
- this.NotifyImplementation(current.Implementation);
-
- List<Counterexample!>? errors;
- VCGen.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional);
-
- // updates to worklist already done in VerifyCurrent, unless there was an exception
- if (exceptional) {
- this.NotifyOutcome(outcome);
- UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
- if (AnyNonCandidateViolation(outcome, errors)) { //abort
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- FlushWorkList(current);
- } else { //continue
- UpdateAssignmentWorkList(current, outcome, errors);
- }
- }
- }
- this.NotifyEnd(true);
- current.Outcome.assignment = current.Assignment;
- return current.Outcome;
- }
-
-
- private List<Implementation!>! FindImplementationsToEnqueue(RefutedAnnotation! refutedAnnotation, Implementation! currentImplementation) {
- List<Implementation!>! implementations = new List<Implementation!>();
- switch (refutedAnnotation.Kind) {
- case RefutedAnnotationKind.REQUIRES:
- foreach (Implementation! callee in callGraph.NextNodes(currentImplementation)) {
- assume (callee.Proc!=null);
- if (callee.Proc.Equals(refutedAnnotation.CalleeProc))
- implementations.Add(callee);
- }
- break;
- case RefutedAnnotationKind.ENSURES:
- foreach (Implementation! caller in callGraph.PreviousNodes(currentImplementation))
- implementations.Add(caller);
- break;
- case RefutedAnnotationKind.ASSERT: //the implementation is already in queue
- break;
- default:
- throw new Exception("Unknown Refuted annotation kind:" + refutedAnnotation.Kind);
- break;
- }
- return implementations;
- }
-
- private enum RefutedAnnotationKind { REQUIRES, ENSURES, ASSERT};
-
- private class RefutedAnnotation {
- private string! _constant;
- private RefutedAnnotationKind _kind;
- private Procedure _callee;
-
- private RefutedAnnotation(string! constant, RefutedAnnotationKind kind, Procedure callee) {
- this._constant = constant;
- this._kind = kind;
- this._callee = callee;
- }
- public RefutedAnnotationKind Kind {
- get { return this._kind; }
- }
- public string! Constant {
- get { return this._constant; }
- }
- public Procedure CalleeProc {
- get { return this._callee; }
- }
- public static RefutedAnnotation BuildRefutedRequires(string! constant, Procedure! callee) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.REQUIRES,callee);
- }
- public static RefutedAnnotation BuildRefutedEnsures(string! constant) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.ENSURES, null);
- }
- public static RefutedAnnotation BuildRefutedAssert(string! constant) {
- return new RefutedAnnotation(constant,RefutedAnnotationKind.ASSERT, null);
- }
-
- }
-
- private void PrintRefutedCall(CallCounterexample! err, XmlSink! xmlOut) {
- Expr! cond = err.FailingRequires.Condition;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, err.Trace);
- }
- }
-
- private void PrintRefutedReturn(ReturnCounterexample! err, XmlSink! xmlOut) {
- Expr! cond = err.FailingEnsures.Condition;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, err.Trace);
- }
- }
-
- private void PrintRefutedAssert(AssertCounterexample! err, XmlSink! xmlOut) {
- Expr cond = err.FailingAssert.OrigExpr;
- string houdiniConst;
- if (MatchCandidate(cond, out houdiniConst)) {
- xmlOut.WriteError("postcondition violation", err.FailingAssert.tok, err.FailingAssert.tok, err.Trace);
- }
- }
-
-
- private void DebugRefutedCandidates(Implementation! curFunc, List<Counterexample!> errors) {
- XmlSink xmlRefuted = CommandLineOptions.Clo.XmlRefuted;
- if (xmlRefuted != null && errors != null) {
- DateTime start = DateTime.Now;
- xmlRefuted.WriteStartMethod(curFunc.ToString(), start);
-
- foreach (Counterexample! error in errors) {
- CallCounterexample ce = error as CallCounterexample;
- if (ce != null) PrintRefutedCall(ce, xmlRefuted);
- ReturnCounterexample re = error as ReturnCounterexample;
- if (re != null) PrintRefutedReturn(re, xmlRefuted);
- AssertCounterexample ae = error as AssertCounterexample;
- if (ae != null) PrintRefutedAssert(ae, xmlRefuted);
- }
-
- DateTime end = DateTime.Now;
- xmlRefuted.WriteEndMethod("errors", end, end.Subtract(start));
- }
- }
-
- private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) {
- string houdiniConstant;
- CallCounterexample callCounterexample = error as CallCounterexample;
- if (callCounterexample!=null) {
- Procedure! failingProcedure = (!)callCounterexample.FailingCall.Proc;
- Requires! failingRequires = (!)callCounterexample.FailingRequires;
- if (MatchCandidate(failingRequires.Condition,out houdiniConstant)) {
- assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedRequires(houdiniConstant, failingProcedure);
- }
- }
- ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
- if (returnCounterexample!=null) {
- Ensures failingEnsures =returnCounterexample.FailingEnsures;
- if (MatchCandidate(failingEnsures.Condition,out houdiniConstant)) {
- assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedEnsures(houdiniConstant);
- }
- }
- AssertCounterexample assertCounterexample = error as AssertCounterexample;
- if (assertCounterexample!=null) {
- AssertCmd failingAssert = assertCounterexample.FailingAssert;
- if (MatchCandidate(failingAssert.OrigExpr,out houdiniConstant)) {
- assert (houdiniConstant!=null);
- return RefutedAnnotation.BuildRefutedAssert(houdiniConstant);
- }
- }
-
- return null;
- }
-
- private VCGen.Outcome TryCatchVerify(HdnVCGen! vcgen, out List<Counterexample!>? errors) {
- VCGen.Outcome outcome;
- try {
- outcome = vcgen.Verify(out errors);
- } catch (VCGenException e) {
- assume(e!=null);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- } catch (UnexpectedProverOutputException upo) {
- assume(upo!=null);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- return outcome;
- }
-
- //version of TryCatchVerify that spins on the same function
- //as long as the current assignment is changing
- private VCGen.Outcome TrySpinSameFunc(HoudiniState! current,
- Program! program,
- HdnVCGen! vcgen,
- out List<Counterexample!>? errors,
- out bool exceptional) {
- assert (current.Implementation != null);
- VCGen.Outcome outcome;
- bool pushed = false;
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- try {
- bool trySameFunc = true;
- bool pastFirstIter = false; //see if this new loop is even helping
-
- do {
- if (pastFirstIter) {
- System.GC.Collect();
- this.NotifyIteration();
- }
- Axiom! currentAx = BuildAxiom(current.Assignment);
- this.NotifyAssignment(current.Assignment);
-
- vcgen.PushAxiom(currentAx);
- pushed = true;
- outcome = vcgen.Verify(out errors);
- vcgen.Pop();
- pushed = false;
- this.NotifyOutcome(outcome);
-
- DebugRefutedCandidates(current.Implementation, errors);
- UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
- if (!continueAtError && IsOutcomeNotHoudini(outcome,errors)) {
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- trySameFunc = false;
- FlushWorkList(current);
- } else {
- trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
- //reset for the next round
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- pastFirstIter = true;
- } while (trySameFunc && current.WorkList.Count > 0);
-
- } catch (VCGenException e) {
- assume(e!=null);
- if (pushed){
- vcgen.Pop(); // what if session is dead?
- }
- NotifyException("VCGen");
- exceptional = true;
- return outcome;
- } catch (UnexpectedProverOutputException upo) {
- assume(upo!=null);
- if (pushed){
- vcgen.Pop();
- }
- NotifyException("UnexpectedProverOutput");
- exceptional = true;
- return outcome;
- }
- exceptional = false;
- return outcome;
- }
-
-
-
- //Similar to TrySpinSameFunc except no Candidate logic
- private VCGen.Outcome HoudiniVerifyCurrentAux(HoudiniState! current,
- Program! program,
- HdnVCGen! vcgen,
- out List<Counterexample!>? errors,
- out bool exceptional) {
- assert (current.Implementation != null);
- VCGen.Outcome outcome;
- bool pushed = false;
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- try {
- bool trySameFunc = true;
- bool pastFirstIter = false; //see if this new loop is even helping
-
- do {
- if (pastFirstIter) {
- System.GC.Collect();
- this.NotifyIteration();
- }
-
- Axiom! currentAx = BuildAxiom(current.Assignment);
- this.NotifyAssignment(current.Assignment);
-
- //check the VC with the current assignment
- vcgen.PushAxiom(currentAx);
- pushed = true;
- outcome = vcgen.Verify(out errors);
- vcgen.Pop();
- pushed = false;
- this.NotifyOutcome(outcome);
-
- DebugRefutedCandidates(current.Implementation, errors);
- UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);
-
- if (AnyNonCandidateViolation(outcome, errors)) { //abort
- current.WorkList.Dequeue();
- this.NotifyDequeue();
- trySameFunc = false;
- FlushWorkList(current);
- } else { //continue
- trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);
- //reset for the next round
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- pastFirstIter = true;
- } while (trySameFunc && current.WorkList.Count > 0);
-
- } catch (VCGenException e) {
- assume(e!=null);
- if (pushed){
- vcgen.Pop(); // what if session is dead?
- }
- NotifyException("VCGen");
- exceptional = true;
- return outcome;
- } catch (UnexpectedProverOutputException upo) {
- assume(upo!=null);
- if (pushed){
- vcgen.Pop();
- }
- NotifyException("UnexpectedProverOutput");
- exceptional = true;
- return outcome;
- }
- exceptional = false;
- return outcome;
- }
- }
-
- public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted }
-
- public class VCGenOutcome {
- public VCGen.Outcome outcome;
- public List<Counterexample!> errors;
- public VCGenOutcome(VCGen.Outcome outcome, List<Counterexample!> errors) {
- this.outcome = outcome;
- this.errors = errors;
- }
- }
-
- public class HoudiniOutcome {
- // final assignment
- public Dictionary<string!,bool>! assignment = new Dictionary<string!,bool>();
- // boogie errors
- public Dictionary<string!,VCGenOutcome!>! implementationOutcomes = new Dictionary<string!,VCGenOutcome!>();
- // outcome kind
- public HoudiniOutcomeKind kind;
-
- // statistics
-
- private int CountResults(VCGen.Outcome outcome) {
- int outcomeCount=0;
- foreach (VCGenOutcome! verifyOutcome in implementationOutcomes.Values) {
- if (verifyOutcome.outcome==outcome)
- outcomeCount++;
- }
- return outcomeCount;
- }
-
- private List<string!>! ListOutcomeMatches(VCGen.Outcome outcome) {
- List<string!>! result = new List<string!>();
- foreach (KeyValuePair<string!, VCGenOutcome!> kvpair in implementationOutcomes) {
- if (kvpair.Value.outcome==outcome)
- result.Add(kvpair.Key);
- }
- return result;
- }
-
- public int ErrorCount {
- get {
- return CountResults(VCGen.Outcome.Errors);
- }
- }
- public int Verified {
- get {
- return CountResults(VCGen.Outcome.Correct);
- }
- }
- public int Inconclusives {
- get {
- return CountResults(VCGen.Outcome.Inconclusive);
- }
- }
- public int TimeOuts {
- get {
- return CountResults(VCGen.Outcome.TimedOut);
- }
- }
- public List<string!>! ListOfTimeouts {
- get {
- return ListOutcomeMatches(VCGen.Outcome.TimedOut);
- }
- }
- public List<string!>! ListOfInconclusives {
- get {
- return ListOutcomeMatches(VCGen.Outcome.Inconclusive);
- }
- }
- public List<string!>! ListOfErrors {
- get {
- return ListOutcomeMatches(VCGen.Outcome.Errors);
- }
- }
- }
-
-}
diff --git a/Source/Houdini/Houdini.sscproj b/Source/Houdini/Houdini.sscproj deleted file mode 100644 index 3f68bb91..00000000 --- a/Source/Houdini/Houdini.sscproj +++ /dev/null @@ -1,118 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<VisualStudioProject>
- <XEN ProjectType="Local"
- SchemaVersion="1.0"
- Name="Houdini"
- ProjectGuid="40454b39-4f61-48b2-bde3-e9271b24f469"
- >
- <Build>
- <Settings ApplicationIcon=""
- AssemblyName="Houdini"
- OutputType="Library"
- RootNamespace="Houdini"
- StartupObject=""
- StandardLibraryLocation=""
- TargetPlatform="v2"
- TargetPlatformLocation=""
- >
- <Config Name="Debug"
- AllowUnsafeBlocks="False"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="False"
- ConfigurationOverrideFile=""
- DefineConstants="DEBUG;TRACE"
- DocumentationFile=""
- DebugSymbols="True"
- FileAlignment="4096"
- IncrementalBuild="True"
- Optimize="False"
- OutputPath="bin\debug"
- RegisterForComInterop="False"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="False"
- WarningLevel="4"
- CheckContractAdmissibility="True"
- CheckPurity="False"
- />
- <Config Name="Release"
- AllowUnsafeBlocks="false"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="false"
- ConfigurationOverrideFile=""
- DefineConstants="TRACE"
- DocumentationFile=""
- DebugSymbols="false"
- FileAlignment="4096"
- IncrementalBuild="false"
- Optimize="true"
- OutputPath="bin\release"
- RegisterForComInterop="false"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="false"
- WarningLevel="4"
- CheckContractAdmissibility="True"
- CheckPurity="False"
- />
- </Settings>
- <References>
- <Reference Name="System"
- AssemblyName="System"
- Private="false"
- />
- <Reference Name="System.Data"
- AssemblyName="System.Data"
- Private="false"
- />
- <Reference Name="System.Xml"
- AssemblyName="System.Xml"
- Private="false"
- />
- <Reference Name="Core"
- Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
- Private="true"
- />
- <Reference Name="VCGeneration"
- Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- <Reference Name="Simplify"
- Project="{F75666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- <Reference Name="AIFramework"
- Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
- Private="true"
- />
- <Reference Name="AbsInt"
- Project="{11D06232-2039-4BCA-853B-C596E2A4EDB0}"
- Private="true"
- />
- <Reference Name="System.Compiler.Framework"
- AssemblyName="System.Compiler.Framework"
- Private="false"
- HintPath="../../Binaries/System.Compiler.Framework.dll"
- />
- <Reference Name="Z3"
- Project="{F75666DE-CD56-457C-8782-09BE243450FC}"
- Private="true"
- />
- </References>
- </Build>
- <Files>
- <Include>
- <File RelPath="Houdini.ssc"
- SubType="Code"
- BuildAction="Compile"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="Checker.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="..\version.ssc"
- />
- </Include>
- </Files>
- </XEN>
-</VisualStudioProject>
\ No newline at end of file diff --git a/Source/ModelViewer/BCTProvider.cs b/Source/ModelViewer/BCTProvider.cs new file mode 100644 index 00000000..6574daff --- /dev/null +++ b/Source/ModelViewer/BCTProvider.cs @@ -0,0 +1,203 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace Microsoft.Boogie.ModelViewer.BCT {
+ public class Provider : ILanguageProvider {
+ public static Provider Instance = new Provider();
+ private Provider() { }
+
+ public bool IsMyModel(Model m) {
+ return m.TryGetFunc("Alloc") != null;
+ }
+
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts) {
+ var dm = new BCTModel(m, opts);
+ foreach (var s in m.States) {
+ var sn = new StateNode(dm.states.Count, dm, s);
+ dm.states.Add(sn);
+ }
+ dm.FinishStates();
+ return dm;
+ }
+ }
+
+ class BCTModel : LanguageModel {
+ public readonly Model.Func f_heap_select;
+ public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();
+ public readonly Dictionary<Model.Element, Model.FuncTuple> DatatypeValues = new Dictionary<Model.Element, Model.FuncTuple>();
+ Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();
+ public List<StateNode> states = new List<StateNode>();
+
+ public BCTModel(Model m, ViewOptions opts)
+ : base(m, opts) {
+ f_heap_select = m.MkFunc("[3]", 3);
+ }
+
+ internal void FinishStates() {
+ GenerateSourceLocations(states);
+ }
+
+ public override IEnumerable<IState> States {
+ get { return states; }
+ }
+
+ public string GetUserVariableName(string name) {
+ if (name.StartsWith("$"))
+ return null;
+ var hash = name.IndexOf('#');
+ if (0 < hash)
+ return name.Substring(0, hash);
+ return name;
+ }
+
+ public Model.Element Image(Model.Element elt, Model.Func f) {
+ var r = f.AppWithResult(elt);
+ if (r != null)
+ return r.Args[0];
+ return null;
+ }
+ /*
+ public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt) {
+ List<ElementNode> result = new List<ElementNode>();
+
+ if (elt.Kind != Model.ElementKind.Uninterpreted)
+ return result;
+
+ // Perhaps elt is a known datatype value
+ Model.FuncTuple fnTuple;
+ if (DatatypeValues.TryGetValue(elt, out fnTuple)) {
+ // elt is a datatype value
+ int i = 0;
+ foreach (var arg in fnTuple.Args) {
+ var edgname = new EdgeName(this, i.ToString());
+ result.Add(new FieldNode(state, edgname, arg));
+ i++;
+ }
+ return result;
+ }
+
+ // Perhaps elt is a sequence
+ var seqLen = f_seq_length.AppWithArg(0, elt);
+ if (seqLen != null) {
+ // elt is a sequence
+ foreach (var tpl in f_seq_index.AppsWithArg(0, elt)) {
+ var edgname = new EdgeName(this, "[%0]", tpl.Args[1]);
+ result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));
+ }
+ return result;
+ }
+
+ // Perhaps elt is a set
+ foreach (var tpl in f_set_select.AppsWithArg(0, elt)) {
+ var setElement = tpl.Args[1];
+ var containment = tpl.Result;
+ var edgname = new EdgeName(this, "[%0]", Unbox(setElement));
+ result.Add(new FieldNode(state, edgname, containment));
+ }
+ if (result.Count != 0)
+ return result; // elt is a set
+
+ // It seems elt is an object or array
+ Model.Element[] lengths;
+ if (ArrayLengths.TryGetValue(elt, out lengths)) {
+ int i = 0;
+ foreach (var len in lengths) {
+ var name = lengths.Length == 1 ? "Length" : "Length" + i;
+ var edgname = new EdgeName(this, name);
+ result.Add(new FieldNode(state, edgname, len));
+ i++;
+ }
+ }
+ var heap = state.State.TryGet("$Heap");
+ if (heap != null) {
+ foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) {
+ var field = new FieldName(tpl.Args[2], this);
+ if (field.NameFormat != "alloc") {
+ var edgname = new EdgeName(this, field.NameFormat, field.NameArgs);
+ result.Add(new FieldNode(state, edgname, Unbox(tpl.Result)));
+ }
+ }
+ }
+ return result;
+ }
+ */
+ }
+
+ class StateNode : NamedState {
+ internal readonly BCTModel dm;
+ internal readonly List<VariableNode> vars = new List<VariableNode>();
+ internal readonly int index;
+
+ public StateNode(int i, BCTModel parent, Model.CapturedState s)
+ : base(s, parent) {
+ dm = parent;
+ state = s;
+ index = i;
+
+ SetupVars();
+ }
+
+ void SetupVars() {
+ var names = Util.Empty<string>();
+
+ if (dm.states.Count > 0) {
+ var prev = dm.states.Last();
+ names = prev.vars.Map(v => v.realName);
+ }
+
+ names = names.Concat(state.Variables).Distinct();
+
+ var curVars = state.Variables.ToDictionary(x => x);
+ foreach (var v in names) {
+ if (dm.GetUserVariableName(v) != null) {
+ var val = state.TryGet(v);
+ var vn = new VariableNode(this, v, val);
+ vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);
+ if (curVars.ContainsKey(v))
+ dm.RegisterLocalValue(vn.Name, val);
+ vars.Add(vn);
+ }
+ }
+
+ dm.Flush(Nodes);
+ }
+
+ public override IEnumerable<IDisplayNode> Nodes {
+ get {
+ return vars;
+ }
+ }
+ }
+
+ class ElementNode : DisplayNode {
+ protected StateNode stateNode;
+ protected Model.Element elt;
+ protected BCTModel vm { get { return stateNode.dm; } }
+
+ public ElementNode(StateNode st, EdgeName name, Model.Element elt)
+ : base(st.dm, name, elt) {
+ this.stateNode = st;
+ this.elt = elt;
+ }
+
+ public ElementNode(StateNode st, string name, Model.Element elt)
+ : this(st, new EdgeName(name), elt) { }
+
+ protected override void ComputeChildren() {
+ //children.AddRange(vm.GetExpansion(stateNode, elt));
+ }
+ }
+
+ class VariableNode : ElementNode {
+ public bool updatedHere;
+ public string realName;
+
+ public VariableNode(StateNode par, string realName, Model.Element elt)
+ : base(par, realName, elt) {
+ this.realName = realName;
+ name = new EdgeName(vm.GetUserVariableName(realName));
+ }
+ }
+}
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj index 6262ae2f..3a25e5cc 100644 --- a/Source/ModelViewer/ModelViewer.csproj +++ b/Source/ModelViewer/ModelViewer.csproj @@ -113,6 +113,7 @@ </ItemGroup>
<ItemGroup>
<Compile Include="BaseProvider.cs" />
+ <Compile Include="BCTProvider.cs" />
<Compile Include="DafnyProvider.cs" />
<Compile Include="DataModel.cs" />
<Compile Include="Main.cs">
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index ff106380..87ab590d 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -164,8 +164,8 @@ namespace VC { Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
}
- private Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;
- private GlobalVariable errorVariable;
+ protected Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;
+ protected GlobalVariable errorVariable;
public void GenerateVCsForLazyInlining(Program program) {
Contract.Requires(program != null);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0723bcba..9a8c7541 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -419,50 +419,50 @@ Execution trace: Dafny program verifier finished with 3 verified, 3 errors
-------------------- ResolutionErrors.dfy --------------------
-ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context
-ResolutionErrors.dfy(100,9): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(101,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(105,11): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(106,9): Error: actual out-parameter 0 is required to be a ghost variable
-ResolutionErrors.dfy(113,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(117,23): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(124,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(128,21): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(129,35): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(138,9): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(144,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(185,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(208,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(220,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(224,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(229,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
-ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name
-ResolutionErrors.dfy(46,7): Error: unresolved identifier: F
-ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name
-ResolutionErrors.dfy(47,7): Error: call to instance function requires an instance
-ResolutionErrors.dfy(48,7): Error: unresolved identifier: G
-ResolutionErrors.dfy(50,7): Error: unresolved identifier: M
-ResolutionErrors.dfy(51,7): Error: call to instance method requires an instance
-ResolutionErrors.dfy(52,7): Error: unresolved identifier: N
-ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters
-ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global
-ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
-ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
-ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label
-ResolutionErrors.dfy(252,2): Error: duplicate label
-ResolutionErrors.dfy(278,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(279,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(281,4): Error: a constructor is only allowed to be called when an object is being allocated
-ResolutionErrors.dfy(295,16): Error: arguments must have the same type (got int and DTD_List)
-ResolutionErrors.dfy(296,16): Error: arguments must have the same type (got DTD_List and int)
-ResolutionErrors.dfy(297,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name
+ResolutionErrors.dfy(55,7): Error: unresolved identifier: F
+ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance
+ResolutionErrors.dfy(57,7): Error: unresolved identifier: G
+ResolutionErrors.dfy(59,7): Error: unresolved identifier: M
+ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance
+ResolutionErrors.dfy(61,7): Error: unresolved identifier: N
+ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters
+ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global
+ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
+ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(261,2): Error: duplicate label
+ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated
+ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
44 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index f8adaad5..1b68ad91 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -24,6 +24,15 @@ method ManyIndices<T>(a: array3<T>, b: array<T>, m: int, n: int) var z := b[m, n, m, n]; // error
}
+method SB(b: array2<int>, s: int) returns (x: int, y: int)
+ requires b != null;
+{
+ while
+ {
+ case b[x,y] == s =>
+ }
+}
+
// -------- name resolution
class Global {
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 5ee9f921..2b60b851 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -85,7 +85,7 @@ Dafny program verifier finished with 29 verified, 0 errors -------------------- Rippling.dfy --------------------
-Dafny program verifier finished with 132 verified, 0 errors
+Dafny program verifier finished with 137 verified, 0 errors
-------------------- Celebrity.dfy --------------------
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 0a4d541d..5fd87a6c 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -234,6 +234,13 @@ function sort(xs: List): List case Cons(y, ys) => insort(y, sort(ys))
}
+function reverse(xs: List): List
+{
+ match xs
+ case Nil => Nil
+ case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))
+}
+
// Pair list functions
function zip(a: List, b: List): PList
@@ -554,3 +561,28 @@ ghost method P67() assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));
}
}
+
+// ---------
+
+ghost method Lemma_RevConcat(xs: List, ys: List)
+ ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
+{
+ match (xs) {
+ case Nil =>
+ assert forall ws :: concat(ws, Nil) == ws;
+ case Cons(t, rest) =>
+ Lemma_RevConcat(rest, ys);
+ assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
+ }
+}
+
+ghost method Theorem(xs: List)
+ ensures reverse(reverse(xs)) == xs;
+{
+ match (xs) {
+ case Nil =>
+ case Cons(t, rest) =>
+ Lemma_RevConcat(reverse(rest), Cons(t, Nil));
+ Theorem(rest);
+ }
+}
diff --git a/Test/houdini/houd6.bpl b/Test/houdini/houd6.bpl index 09f2dd0e..820d2d73 100644 --- a/Test/houdini/houd6.bpl +++ b/Test/houdini/houd6.bpl @@ -41,4 +41,4 @@ modifies array; }
// expected outcome: Correct
-// expected assigment: bi->True forall i
\ No newline at end of file +// expected assigment: bi->False forall i
\ No newline at end of file diff --git a/Util/VS2010/Chalice/StartChalice.bat b/Util/VS2010/Chalice/StartChalice.bat index 0e7401e4..e2de0e65 100644 --- a/Util/VS2010/Chalice/StartChalice.bat +++ b/Util/VS2010/Chalice/StartChalice.bat @@ -3,7 +3,7 @@ echo ---------- Starting ------------ < nul >> c:\tmp\coo.out time < nul >> c:\tmp\coo.out
echo. < nul >> c:\tmp\coo.out
-call "c:\Program Files\Scala\bin\scala" -cp c:\boogie\Chalice\bin chalice.Chalice -nologo -vs %* 2>> c:\tmp\coo.out
+call "c:\Program Files\Scala\bin\scala" -cp c:\boogie\Chalice\target\scala-2.8.1.final\classes chalice.Chalice /boogieOpt:nologo /vs %* 2>> c:\tmp\coo.out
time < nul >> c:\tmp\coo.out
echo. < nul >> c:\tmp\coo.out
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 0cd95bbd..df0f22ee 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -352,6 +352,7 @@ namespace Demo | "==>"
| "<==>"
| "#"
+ | "?" // this is not an operator, but a possible character in identifiers
| n
| stringLiteral
;
|