diff options
author | 2011-11-15 13:05:51 -0800 | |
---|---|---|
committer | 2011-11-15 13:05:51 -0800 | |
commit | 78160fbd9492cf88e620a859a405fe9a49a09c54 (patch) | |
tree | 5f1571197ea295cd7870935406c808c2bc04ed5c | |
parent | 94fcbefe78e8f7f866e0e6f743fa4b1ab258b296 (diff) | |
parent | b13899eb71d162ca976bfcd6ed774a1c99717372 (diff) |
Merge
22 files changed, 522 insertions, 194 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 8e5170b2..47c68419 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -33,6 +33,27 @@ namespace BytecodeTranslator private bool contractContext;
+ private Bpl.Expr FindOrCreateTypeReferenceInCodeContext(ITypeReference typeReference) {
+ return this.sink.FindOrCreateTypeReference(typeReference, true);
+
+ IGenericTypeParameter gtp = typeReference as IGenericTypeParameter;
+ if (gtp != null) {
+ var selectorName = gtp.Name.Value;
+ selectorName = TranslationHelper.TurnStringIntoValidIdentifier(selectorName);
+ var typeName = TypeHelper.GetTypeName(gtp.DefiningType, NameFormattingOptions.DocumentationId);
+ typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);
+ var funcName = String.Format("{0}#{1}", selectorName, typeName);
+ Bpl.IToken tok = Bpl.Token.NoToken;
+ var identExpr = Bpl.Expr.Ident(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, funcName, this.sink.Heap.TypeType)));
+ var funcCall = new Bpl.FunctionCall(identExpr);
+ var thisArg = new Bpl.IdentifierExpr(tok, this.sink.ThisVariable);
+ var dynType = this.sink.Heap.DynamicType(thisArg);
+ var nary = new Bpl.NAryExpr(Bpl.Token.NoToken, funcCall, new Bpl.ExprSeq(dynType));
+ return nary;
+ }
+ return this.sink.FindOrCreateTypeReference(typeReference);
+ }
+
#region Constructors
///// <summary>
@@ -473,7 +494,7 @@ namespace BytecodeTranslator new Bpl.AssumeCmd(tok,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(locExpr),
- this.sink.FindOrCreateTypeReference(typ)
+ this.FindOrCreateTypeReferenceInCodeContext(typ)
)
)
);
@@ -637,7 +658,7 @@ namespace BytecodeTranslator new Bpl.AssumeCmd(methodCallToken,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(thisExpr),
- this.sink.FindOrCreateTypeReference(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)
+ this.FindOrCreateTypeReferenceInCodeContext(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)
)
)
);
@@ -701,13 +722,13 @@ namespace BytecodeTranslator List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();
Sink.GetConsolidatedTypeArguments(consolidatedTypeArguments, methodToCall.ContainingType);
foreach (ITypeReference typeReference in consolidatedTypeArguments) {
- inexpr.Add(sink.FindOrCreateTypeReference(typeReference));
+ inexpr.Add(this.FindOrCreateTypeReferenceInCodeContext(typeReference));
}
}
IGenericMethodInstanceReference methodInstanceReference = methodToCall as IGenericMethodInstanceReference;
if (methodInstanceReference != null) {
foreach (ITypeReference typeReference in methodInstanceReference.GenericArguments) {
- inexpr.Add(sink.FindOrCreateTypeReference(typeReference));
+ inexpr.Add(this.FindOrCreateTypeReferenceInCodeContext(typeReference));
}
}
@@ -945,7 +966,7 @@ namespace BytecodeTranslator new Bpl.AssumeCmd(token,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(Bpl.Expr.Ident(a)),
- this.sink.FindOrCreateTypeReference(createObjectInstance.Type)
+ this.FindOrCreateTypeReferenceInCodeContext(createObjectInstance.Type)
)
)
);
@@ -953,6 +974,7 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
+
public override void TraverseChildren(ICreateArray createArrayInstance)
{
Bpl.IToken cloc = createArrayInstance.Token();
@@ -1002,13 +1024,13 @@ namespace BytecodeTranslator List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();
Sink.GetConsolidatedTypeArguments(consolidatedTypeArguments, methodToCall.ContainingType);
foreach (ITypeReference typeReference in consolidatedTypeArguments) {
- typeParameterExprs.Add(sink.FindOrCreateTypeReference(typeReference));
+ typeParameterExprs.Add(this.FindOrCreateTypeReferenceInCodeContext(typeReference));
}
}
IGenericMethodInstanceReference methodInstanceReference = methodToCall as IGenericMethodInstanceReference;
if (methodInstanceReference != null) {
foreach (ITypeReference typeReference in methodInstanceReference.GenericArguments) {
- typeParameterExprs.Add(sink.FindOrCreateTypeReference(typeReference));
+ typeParameterExprs.Add(this.FindOrCreateTypeReferenceInCodeContext(typeReference));
}
}
Bpl.Expr typeParameterExpr =
@@ -1448,7 +1470,7 @@ namespace BytecodeTranslator public override void TraverseChildren(ICastIfPossible castIfPossible) {
base.Traverse(castIfPossible.ValueToCast);
var exp = TranslatedExpressions.Pop();
- var e = this.sink.FindOrCreateTypeReference(castIfPossible.TargetType);
+ var e = this.FindOrCreateTypeReferenceInCodeContext(castIfPossible.TargetType);
var callAs = new Bpl.NAryExpr(
castIfPossible.Token(),
new Bpl.FunctionCall(this.sink.Heap.AsFunction),
@@ -1458,7 +1480,7 @@ namespace BytecodeTranslator return;
}
public override void TraverseChildren(ICheckIfInstance checkIfInstance) {
- var e = this.sink.FindOrCreateTypeReference(checkIfInstance.TypeToCheck);
+ var e = this.FindOrCreateTypeReferenceInCodeContext(checkIfInstance.TypeToCheck);
//var callTypeOf = new Bpl.NAryExpr(
// checkIfInstance.Token(),
// new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),
@@ -1644,7 +1666,7 @@ namespace BytecodeTranslator }
public override void TraverseChildren(ITypeOf typeOf) {
- var e = this.sink.FindOrCreateTypeReference(typeOf.TypeToGet);
+ var e = this.FindOrCreateTypeReferenceInCodeContext(typeOf.TypeToGet);
var callTypeOf = new Bpl.NAryExpr(
typeOf.Token(),
new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 4f0e3667..f6dc7ecf 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -125,7 +125,7 @@ namespace BytecodeTranslator { if (typeDefinition.IsClass) {
bool savedSawCctor = this.sawCctor;
this.sawCctor = false;
- sink.FindOrCreateTypeReference(typeDefinition);
+ sink.FindOrDefineType(typeDefinition);
base.TraverseChildren(typeDefinition);
if (!this.sawCctor) {
CreateStaticConstructor(typeDefinition);
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 4af8c9ec..4702d5a0 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -211,7 +211,7 @@ namespace BytecodeTranslator { }
module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;
// The decompiler does not turn calls to Assert/Assume into Code Model nodes
- module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(module);
+ module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(module);
host.RegisterAsLatest(module);
modules.Add(module);
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 50051b0c..957b8c38 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -867,14 +867,14 @@ namespace BytecodeTranslator { /// <paramref name="type"/> in the Bpl program. I.e., its
/// value represents the expression "typeof(type)".
/// </summary>
- public Bpl.Expr FindOrCreateTypeReference(ITypeReference type) {
+ public Bpl.Expr FindOrCreateTypeReference(ITypeReference type, bool codeContext = false) {
var gtir = type as IGenericTypeInstanceReference;
if (gtir != null) {
- var genericType = FindOrDefineType(gtir.GenericType);
+ var genericType = FindOrDefineType(gtir.GenericType.ResolvedType);
var gArgs = new Bpl.ExprSeq();
foreach (var a in gtir.GenericArguments) {
- var a_prime = FindOrCreateTypeReference(a);
+ var a_prime = FindOrCreateTypeReference(a, codeContext);
gArgs.Add(a_prime);
}
var typeExpression = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(genericType), gArgs);
@@ -882,18 +882,24 @@ namespace BytecodeTranslator { IGenericTypeParameter gtp = type as IGenericTypeParameter;
if (gtp != null) {
- var selectorName = gtp.Name.Value;
- selectorName = TranslationHelper.TurnStringIntoValidIdentifier(selectorName);
- var typeName = TypeHelper.GetTypeName(gtp.DefiningType, NameFormattingOptions.DocumentationId);
- typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);
- var funcName = String.Format("{0}#{1}", selectorName, typeName);
- Bpl.IToken tok = Bpl.Token.NoToken;
- var identExpr = Bpl.Expr.Ident(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, funcName, this.Heap.TypeType)));
- var funcCall = new Bpl.FunctionCall(identExpr);
- var thisArg = new Bpl.IdentifierExpr(tok, this.ThisVariable);
- var dynType = this.Heap.DynamicType(thisArg);
- var nary = new Bpl.NAryExpr(Bpl.Token.NoToken, funcCall, new Bpl.ExprSeq(dynType));
- return nary;
+ if (codeContext) {
+ var selectorName = gtp.Name.Value;
+ selectorName = TranslationHelper.TurnStringIntoValidIdentifier(selectorName);
+ var typeName = TypeHelper.GetTypeName(gtp.DefiningType, NameFormattingOptions.DocumentationId);
+ typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);
+ var funcName = String.Format("{0}#{1}", selectorName, typeName);
+ Bpl.IToken tok = Bpl.Token.NoToken;
+ var identExpr = Bpl.Expr.Ident(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, funcName, this.Heap.TypeType)));
+ var funcCall = new Bpl.FunctionCall(identExpr);
+ var thisArg = new Bpl.IdentifierExpr(tok, this.ThisVariable);
+ var dynType = this.Heap.DynamicType(thisArg);
+ var nary = new Bpl.NAryExpr(Bpl.Token.NoToken, funcCall, new Bpl.ExprSeq(dynType));
+ return nary;
+
+ } else {
+ var formal = FindOrDefineTypeParameter(gtp);
+ return Bpl.Expr.Ident(formal);
+ }
}
IGenericMethodParameter gmp = type as IGenericMethodParameter;
@@ -903,6 +909,15 @@ namespace BytecodeTranslator { }
ITypeReference uninstantiatedGenericType = GetUninstantiatedGenericType(type);
+
+ // Corner case: type might be a reference to the uninstantiated generic type.
+ // This happens, e.g., with "typeof(Dictionary<,>)".
+ // In that case, need to create a constant for it (because Boogie doesn't allow
+ // overloading by arity on functions
+ if (type.ResolvedType.IsGeneric && type == uninstantiatedGenericType) {
+ return FindOrDefineTypeConstant(type);
+ }
+
List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();
GetConsolidatedTypeArguments(consolidatedTypeArguments, type);
@@ -912,24 +927,58 @@ namespace BytecodeTranslator { var f2 = this.declaredTypeFunctions[k];
Bpl.ExprSeq args = new Bpl.ExprSeq();
foreach (ITypeReference p in consolidatedTypeArguments) {
- args.Add(FindOrCreateTypeReference(p));
+ args.Add(FindOrCreateTypeReference(p, codeContext));
}
Bpl.Expr naryExpr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f2), args);
return naryExpr;
}
- var f = FindOrDefineType(type);
- // BUGBUG: Generics!
+ var f = FindOrDefineType(type.ResolvedType);
var fCall = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f), new Bpl.ExprSeq());
return fCall;
}
+ /// <summary>
+ /// Constants of type "Type" that represent the uninstantiated type of a generic type.
+ /// E.g. "Dictionary<,>".
+ /// </summary>
+ private Dictionary<uint, Bpl.Constant> declaredTypeConstants = new Dictionary<uint, Bpl.Constant>();
+ private Bpl.Expr FindOrDefineTypeConstant(ITypeReference type) {
+ Bpl.Constant c;
+ var k = type.InternedKey;
+ if (!this.declaredTypeConstants.TryGetValue(k, out c)) {
+ var typeName = TypeHelper.GetTypeName(type);
+ var i = typeName.IndexOf('`');
+ // assume there is just one occurrence
+ if (i != -1) {
+ typeName = typeName.Substring(0, i);
+ }
+ typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);
+ var typedIdent = new Bpl.TypedIdent(Bpl.Token.NoToken, typeName, this.Heap.TypeType);
+ c = new Bpl.Constant(Bpl.Token.NoToken, typedIdent, true);
+ this.declaredTypeConstants.Add(k, c);
+ this.TranslatedProgram.TopLevelDeclarations.Add(c);
+ }
+ return Bpl.Expr.Ident(c);
+ }
+
+ private Dictionary<IGenericParameter, Bpl.Formal> declaredTypeParameters = new Dictionary<IGenericParameter, Bpl.Formal>();
+ public Bpl.Formal FindOrDefineTypeParameter(IGenericParameter genericParameter) {
+ Bpl.Formal formal;
+ if (!this.declaredTypeParameters.TryGetValue(genericParameter, out formal)) {
+ var n = genericParameter.Name.Value;
+ var n2 = TranslationHelper.TurnStringIntoValidIdentifier(n);
+ formal = new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, n2, this.Heap.TypeType), true);
+ }
+ return formal;
+ }
/// <summary>
- /// The Heap has to decide how to represent the type.
- /// All the Sink cares about is adding a declaration for it.
+ /// Every type is represented as a function.
+ /// Non-generic types are nullary functions.
+ /// Generic types are n-ary functions, where n is the number of generic parameters.
/// </summary>
- public Bpl.Function FindOrDefineType(ITypeReference type) {
+ public Bpl.Function FindOrDefineType(ITypeDefinition type) {
Bpl.Function f;
@@ -939,19 +988,30 @@ namespace BytecodeTranslator { var numParameters = ConsolidatedGenericParameterCount(type);
- f = this.Heap.CreateTypeFunction(type, numParameters);
+ //f = this.Heap.CreateTypeFunction(type, numParameters);
+
+ string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);
+ typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
+ var tok = type.Token();
+ var inputs = new Bpl.VariableSeq();
+ foreach (var t in TranslationHelper.ConsolidatedGenericParameters(type)) {
+ var formal = FindOrDefineTypeParameter(t);
+ inputs.Add(formal);
+ }
+ Bpl.Variable output = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "result", this.Heap.TypeType), false);
+ Bpl.Function func = new Bpl.Function(tok, typename, inputs, output);
+ func.Attributes = new Bpl.QKeyValue(Bpl.Token.NoToken, "constructor", new List<object>(1), null);
+ f = func;
+
this.declaredTypeFunctions.Add(key, f);
this.TranslatedProgram.TopLevelDeclarations.Add(f);
- DeclareParents(type.ResolvedType, f);
+ DeclareParents(type, f);
bool isExtern = this.assemblyBeingTranslated != null &&
!TypeHelper.GetDefiningUnitReference(type).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity);
if (isExtern) {
var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);
- if (f.Attributes == null)
- f.Attributes = attrib;
- else
- f.Attributes.AddLast(attrib);
+ f.Attributes.AddLast(attrib);
}
return f;
}
@@ -966,31 +1026,27 @@ namespace BytecodeTranslator { return;
}
private void DeclareSuperType(Bpl.Function typeDefinitionAsBplFunction, ITypeReference superType) {
- var superTypeFunction = FindOrDefineType(superType);
+ var superTypeExpr = FindOrCreateTypeReference(superType);
var numberOfGenericParameters = typeDefinitionAsBplFunction.InParams.Length;
var qvars = new Bpl.VariableSeq();
var exprs = new Bpl.ExprSeq();
- var superTypeArgs = new Bpl.ExprSeq();
for (int i = 0; i < numberOfGenericParameters; i++) {
var t = typeDefinitionAsBplFunction.InParams[i];
qvars.Add(t);
var identForT = Bpl.Expr.Ident(t);
exprs.Add(identForT);
- if (i < superTypeFunction.InParams.Length)
- superTypeArgs.Add(identForT);
}
// G(t,u)
var callToG = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(typeDefinitionAsBplFunction), exprs);
- var callToSuperType = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(superTypeFunction), superTypeArgs);
// Subtype(G(t,u), super)
- Bpl.Expr subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG, callToSuperType));
+ Bpl.Expr subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG, superTypeExpr));
Bpl.Expr disjointSubtree = null;
var isDisjoint = !superType.ResolvedType.IsInterface;
if (isDisjoint) {
// DisjointSubtree(G(t,u), super)
- disjointSubtree = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.DisjointSubtree), new Bpl.ExprSeq(callToG, callToSuperType));
+ disjointSubtree = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.DisjointSubtree), new Bpl.ExprSeq(callToG, superTypeExpr));
}
if (0 < numberOfGenericParameters) {
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 7a9340db..424064ff 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -512,7 +512,7 @@ namespace BytecodeTranslator List<Bpl.Expr> typeReferences = new List<Bpl.Expr>();
this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InCatch));
foreach (ICatchClause catchClause in tryCatchFinallyStatement.CatchClauses) {
- typeReferences.Insert(0, this.sink.FindOrCreateTypeReference(catchClause.ExceptionType));
+ typeReferences.Insert(0, this.sink.FindOrCreateTypeReference(catchClause.ExceptionType, true));
StatementTraverser catchTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);
if (catchClause.ExceptionContainer != Dummy.LocalVariable) {
Bpl.Variable catchClauseVariable = this.sink.FindOrCreateLocalVariable(catchClause.ExceptionContainer);
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 98610297..2862a520 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -126,14 +126,25 @@ namespace BytecodeTranslator { Contract.Requires(typeReference != null);
var typeDefinition = typeReference.ResolvedType;
- var totalParameters = new List<IGenericTypeParameter>(typeDefinition.GenericParameters);
+ var totalParameters = new List<IGenericTypeParameter>();
+ ConsolidatedGenericParameters(typeDefinition, totalParameters);
+ return totalParameters;
+
+ //var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;
+ //while (nestedTypeDefinition != null) {
+ // var containingType = nestedTypeDefinition.ContainingType.ResolvedType;
+ // totalParameters.AddRange(containingType.GenericParameters);
+ // nestedTypeDefinition = containingType as INestedTypeDefinition;
+ //}
+ //totalParameters.AddRange(typeDefinition.GenericParameters);
+ //return totalParameters;
+ }
+ private static void ConsolidatedGenericParameters(ITypeDefinition typeDefinition, List<IGenericTypeParameter> consolidatedParameters){
var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;
- while (nestedTypeDefinition != null) {
- var containingType = nestedTypeDefinition.ContainingType.ResolvedType;
- totalParameters.AddRange(containingType.GenericParameters);
- nestedTypeDefinition = containingType as INestedTypeDefinition;
+ if (nestedTypeDefinition != null){
+ ConsolidatedGenericParameters(nestedTypeDefinition.ContainingTypeDefinition, consolidatedParameters);
}
- return totalParameters;
+ consolidatedParameters.AddRange(typeDefinition.GenericParameters);
}
public static string CreateUniqueMethodName(IMethodReference method) {
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs index e1d2d73a..d9366708 100644 --- a/BCT/BytecodeTranslator/WholeProgram.cs +++ b/BCT/BytecodeTranslator/WholeProgram.cs @@ -165,7 +165,7 @@ namespace BytecodeTranslator { var m = typeMethodPair.Item2;
// guard: is#T($DynamicType(local_variable))
- var typeFunction = this.sink.FindOrDefineType(t);
+ var typeFunction = this.sink.FindOrDefineType(t.ResolvedType);
if (typeFunction == null) {
// BUGBUG!! This just silently skips the branch that would dispatch to t's implementation of the method!
continue;
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 5a1f8dc5..83e6009d 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -389,8 +389,8 @@ namespace Microsoft.Boogie { inline = true;
}
}
- if (inline && CommandLineOptions.Clo.LazyInlining == 0 &&
- CommandLineOptions.Clo.StratifiedInlining == 0) {
+ if ((inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) ||
+ CommandLineOptions.Clo.InlineDepth >= 0) {
foreach (Declaration d in TopLevelDeclarations) {
Implementation impl = d as Implementation;
if (impl != null) {
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 4ffccdc5..7d3fce84 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -143,6 +143,7 @@ namespace Microsoft.Boogie { public int /*(0:3)*/ ErrorTrace = 1;
public bool IntraproceduralInfer = true;
public bool ContractInfer = false;
+ public int InlineDepth = -1;
public bool UseUncheckedContracts = false;
public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
@@ -949,7 +950,10 @@ namespace Microsoft.Boogie { case "/contractInfer":
ContractInfer = true;
break;
-
+ case "-inlineDepth":
+ case "/inlineDepth":
+ ps.GetNumericArgument(ref InlineDepth);
+ break;
case "-subsumption":
case "/subsumption": {
int s = 0;
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index d9c33bd4..adc7e2f0 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -26,6 +26,8 @@ namespace Microsoft.Boogie { protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ inlinedProcLblMap;
+ protected int inlineDepth;
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(codeCopier != null);
@@ -67,6 +69,7 @@ namespace Microsoft.Boogie { protected Inliner(InlineCallback cb) {
inlinedProcLblMap = new Dictionary<string/*!*/, int>();
recursiveProcUnrollMap = new Dictionary<string/*!*/, int>();
+ inlineDepth = CommandLineOptions.Clo.InlineDepth;
codeCopier = new CodeCopier();
inlineCallback = cb;
}
@@ -159,6 +162,8 @@ namespace Microsoft.Boogie { // otherwise, the procedure is not inlined at the call site
protected int GetInlineCount(Implementation impl) {
Contract.Requires(impl != null);
+ Contract.Requires(impl.Proc != null);
+
string/*!*/ procName = impl.Name;
Contract.Assert(procName != null);
int c;
@@ -169,9 +174,7 @@ namespace Microsoft.Boogie { c = -1; // TryGetValue above always overwrites c
impl.CheckIntAttribute("inline", ref c);
// procedure attribute overrides implementation
- if (impl.Proc != null) {
- impl.Proc.CheckIntAttribute("inline", ref c);
- }
+ impl.Proc.CheckIntAttribute("inline", ref c);
recursiveProcUnrollMap[procName] = c;
return c;
@@ -194,9 +197,9 @@ namespace Microsoft.Boogie { }
}
- private List<Block/*!*/>/*!*/ DoInlineBlocks(Stack<Procedure/*!*/>/*!*/ callStack, List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,
- VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies, ref bool inlinedSomething) {
- Contract.Requires(cce.NonNullElements(callStack));
+ private List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,
+ VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies,
+ ref bool inlinedSomething) {
Contract.Requires(cce.NonNullElements(blocks));
Contract.Requires(program != null);
Contract.Requires(newLocalVars != null);
@@ -204,7 +207,6 @@ namespace Microsoft.Boogie { Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
List<Block/*!*/>/*!*/ newBlocks = new List<Block/*!*/>();
-
foreach (Block block in blocks) {
TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd);
CmdSeq cmds = block.Cmds;
@@ -223,14 +225,16 @@ namespace Microsoft.Boogie { } else {
Contract.Assert(callCmd.Proc != null);
Procedure proc = callCmd.Proc;
- int inline = -1;
Implementation impl = FindProcImpl(program, proc);
- if (impl != null) {
- inline = GetInlineCount(impl);
+ if (impl == null) {
+ newCmds.Add(codeCopier.CopyCmd(cmd));
+ continue;
}
+
+ int inline = GetInlineCount(impl);
- if (inline > 0) { // at least one block should exist
+ if (inline > 0 || (inline == -1 && inlineDepth > 0)) { // at least one block should exist
Contract.Assume(impl != null);
Contract.Assert(cce.NonNull(impl.OriginalBlocks).Count > 0);
inlinedSomething = true;
@@ -247,18 +251,24 @@ namespace Microsoft.Boogie { // increment the counter for the procedure to be used in constructing the locals and formals
NextInlinedProcLabel(proc.Name);
- BeginInline(newLocalVars, newModifies, proc, impl);
+ BeginInline(newLocalVars, newModifies, impl);
- List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, proc, impl, nextBlockLabel);
+ List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, impl, nextBlockLabel);
Contract.Assert(cce.NonNullElements(inlinedBlocks));
EndInline();
- recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;
- callStack.Push(cce.NonNull(impl.Proc));
- inlinedBlocks = DoInlineBlocks(callStack, inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);
- callStack.Pop();
- recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;
+ if (inline > 0)
+ recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;
+ else
+ inlineDepth = inlineDepth - 1;
+
+ inlinedBlocks = DoInlineBlocks(inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);
+
+ if (inline > 0)
+ recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;
+ else
+ inlineDepth = inlineDepth + 1;
Block/*!*/ startBlock = inlinedBlocks[0];
Contract.Assert(startBlock != null);
@@ -271,7 +281,7 @@ namespace Microsoft.Boogie { lblCount = nextlblCount;
newCmds = new CmdSeq();
- } else if (inline == 0) {
+ } else if (inline == 0 || (inline == -1 && inlineDepth == 0)) {
inlinedSomething = true;
if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {
// add assert
@@ -304,17 +314,20 @@ namespace Microsoft.Boogie { Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
inlinedProcLblMap.Clear();
recursiveProcUnrollMap.Clear();
+ inlineDepth = CommandLineOptions.Clo.InlineDepth;
inlined = false;
- return DoInlineBlocks(new Stack<Procedure/*!*/>(), blocks, program, newLocalVars, newModifies, ref inlined);
+ return DoInlineBlocks(blocks, program, newLocalVars, newModifies, ref inlined);
}
- protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Procedure proc, Implementation impl) {
+ protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Implementation impl) {
Contract.Requires(impl != null);
- Contract.Requires(proc != null);
+ Contract.Requires(impl.Proc != null);
Contract.Requires(newModifies != null);
Contract.Requires(newLocalVars != null);
+
Hashtable substMap = new Hashtable();
+ Procedure proc = impl.Proc;
foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) {
Contract.Assert(locVar != null);
@@ -377,18 +390,19 @@ namespace Microsoft.Boogie { // result[0] is the entry block
- protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Procedure proc, Implementation impl, string nextBlockLabel) {
+ protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {
Contract.Requires(nextBlockLabel != null);
Contract.Requires(impl != null);
- Contract.Requires(proc != null);
+ Contract.Requires(impl.Proc != null);
Contract.Requires(callCmd != null);
- Contract.Requires(((codeCopier.Subst != null)));
+ Contract.Requires(codeCopier.Subst != null);
- Contract.Requires((codeCopier.OldSubst != null));
+ Contract.Requires(codeCopier.OldSubst != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
List<Block/*!*/>/*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks);
Contract.Assert(implBlocks.Count > 0);
+ Procedure proc = impl.Proc;
string startLabel = implBlocks[0].Label;
List<Block/*!*/>/*!*/ inlinedBlocks = new List<Block/*!*/>();
@@ -407,7 +421,7 @@ namespace Microsoft.Boogie { // inject non-free requires
for (int i = 0; i < proc.Requires.Length; i++) {
Requires/*!*/ req = cce.NonNull(proc.Requires[i]);
- if (!req.Free) {
+ if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {
Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
@@ -472,7 +486,7 @@ namespace Microsoft.Boogie { // inject non-free ensures
for (int i = 0; i < proc.Ensures.Length; i++) {
Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);
- if (!ens.Free) {
+ if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {
Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
AssertCmd/*!*/ a = new AssertEnsuresCmd(ensCopy);
diff --git a/Source/GPUVerify.sln b/Source/GPUVerify.sln index 4fb930ef..a78d449e 100644 --- a/Source/GPUVerify.sln +++ b/Source/GPUVerify.sln @@ -53,26 +53,28 @@ Global z3apidebug|x86 = z3apidebug|x86
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Checked|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.Build.0 = Checked|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Release|Any CPU
{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.Build.0 = Debug|Any CPU
{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|x86
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|x86
{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.Build.0 = Release|Any CPU
{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|x86
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|x86
{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.ActiveCfg = Release|Any CPU
- {E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.Build.0 = Release|Any CPU
{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.Build.0 = Checked|Any CPU
{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 74bdaa5e..b17ca60f 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -261,7 +261,7 @@ namespace GPUVerify verifier.AddCandidateInvariant(wc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
}
- private static Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)
+ protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)
{
Variable ReadOrWriteHasOccurred = ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);
ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;
@@ -355,22 +355,12 @@ namespace GPUVerify AddReadOrWrittenZOffsetIsThreadIdCandidateEnsures(Proc, v, ReadOrWrite, Thread);
}
- protected override void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Proc.Requires.Add(new Requires(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
- }
-
- protected override void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Proc.Ensures.Add(new Ensures(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
- }
-
private void AddReadOrWrittenXOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
{
Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Requires.Add(new Requires(false, expr));
+ verifier.AddCandidateRequires(Proc, expr);
}
}
@@ -379,7 +369,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Requires.Add(new Requires(false, expr));
+ verifier.AddCandidateRequires(Proc, expr);
}
}
@@ -388,7 +378,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Requires.Add(new Requires(false, expr));
+ verifier.AddCandidateRequires(Proc, expr);
}
}
@@ -397,7 +387,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenXOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Ensures.Add(new Ensures(false, expr));
+ verifier.AddCandidateEnsures(Proc, expr);
}
}
@@ -406,7 +396,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenYOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Ensures.Add(new Ensures(false, expr));
+ verifier.AddCandidateEnsures(Proc, expr);
}
}
@@ -415,7 +405,7 @@ namespace GPUVerify Expr expr = ReadOrWrittenZOffsetIsThreadIdExpr(v, ReadOrWrite, Thread);
if (expr != null)
{
- Proc.Ensures.Add(new Ensures(false, expr));
+ verifier.AddCandidateEnsures(Proc, expr);
}
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 25974225..36881f88 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -597,7 +597,7 @@ namespace GPUVerify - private void AddCandidateRequires(Procedure Proc, Expr e)
+ internal void AddCandidateRequires(Procedure Proc, Expr e)
{
Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
@@ -605,7 +605,7 @@ namespace GPUVerify Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
- private void AddCandidateEnsures(Procedure Proc, Expr e)
+ internal void AddCandidateEnsures(Procedure Proc, Expr e)
{
Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 7023a2b3..6956b973 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -61,6 +61,37 @@ <ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
</PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
+ <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|AnyCPU'">
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Release\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ </PropertyGroup>
<ItemGroup>
<Reference Include="System" />
<Reference Include="System.Core" />
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 0f5f8278..237c155e 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -81,10 +81,6 @@ namespace GPUVerify protected abstract void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, string OneOrTwo);
- protected abstract void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo);
-
- protected abstract void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo);
-
public void AddRaceCheckingCandidateInvariants(WhileCmd wc)
{
foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
@@ -154,7 +150,13 @@ namespace GPUVerify failedToFindSecondAccess = false;
}
- AddRaceCheckCalls(verifier.KernelImplementation);
+ foreach (Declaration d in verifier.Program.TopLevelDeclarations)
+ {
+ if (d is Implementation)
+ {
+ AddRaceCheckCalls(d as Implementation);
+ }
+ }
if (failedToFindSecondAccess || !addedLogWrite)
return false;
@@ -447,5 +449,19 @@ namespace GPUVerify }
}
+ private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
+ }
+
+ private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
+ {
+ verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
+ }
+
+ protected abstract Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo);
+
+
+
}
}
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs index 3b1f877e..b3104609 100644 --- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs @@ -567,7 +567,7 @@ namespace GPUVerify verifier.AddCandidateInvariant(wc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
}
- private static Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)
+ protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)
{
int OneOrTwo = Int32.Parse(OneOrTwoString);
Expr expr = null;
@@ -756,7 +756,7 @@ namespace GPUVerify if (expr != null)
{
- Proc.Requires.Add(new Requires(false, expr));
+ verifier.AddCandidateRequires(Proc, expr);
}
}
@@ -766,19 +766,9 @@ namespace GPUVerify if (expr != null)
{
- Proc.Ensures.Add(new Ensures(false, expr));
+ verifier.AddCandidateEnsures(Proc, expr);
}
}
- protected override void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Proc.Requires.Add(new Requires(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
- }
-
- protected override void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
- {
- Proc.Ensures.Add(new Ensures(false, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo)));
- }
-
}
}
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index c725c96a..310a25af 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -680,8 +680,6 @@ namespace Microsoft.Boogie internal System.IO.TextReader rd;
string lastLine = "";
int lineNo;
- bool v1model = false;
- Dictionary<string, Element> partitionMapping = new Dictionary<string, Element>(); // only used when v1model is true
internal List<Model> resModels = new List<Model>();
Model currModel;
@@ -704,8 +702,7 @@ namespace Microsoft.Boogie return f;
}
- List<object> GetFunctionTuple() {
- string newLine = ReadLine();
+ List<object> GetFunctionTuple(string newLine) {
if (newLine == null)
return null;
string line = newLine;
@@ -782,26 +779,15 @@ namespace Microsoft.Boogie return new DatatypeValue(currModel, (string)os[0], args);
}
- Element GetElt(string name)
- {
- Element ret;
-
- if (v1model) {
- if (!partitionMapping.TryGetValue(name, out ret))
- BadModel("undefined partition " + name);
- } else {
- ret = currModel.TryMkElement(name);
- if (ret == null)
- BadModel("invalid element name " + name);
- }
-
+ Element GetElt(string name) {
+ Element ret = currModel.TryMkElement(name);
+ if (ret == null)
+ BadModel("invalid element name " + name);
return ret;
}
void NewModel()
{
- v1model = false;
- partitionMapping.Clear();
lastLine = "";
currModel = new Model();
resModels.Add(currModel);
@@ -822,14 +808,10 @@ namespace Microsoft.Boogie continue;
if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
continue;
- if (line == "partitions:" || line == "function interpretations:") {
- v1model = true;
- continue;
- }
- var words = GetWords(line);
- if (words.Length == 0) continue;
- var lastWord = words[words.Length - 1];
+ var words = GetFunctionTuple(line);
+ if (words.Count == 0) continue;
+ var lastWord = words[words.Count - 1];
if (currModel == null)
BadModel("model begin marker not found");
@@ -853,35 +835,13 @@ namespace Microsoft.Boogie continue;
}
- if (v1model && words[0][0] == '*') {
- var partName = words[0];
- var len = words.Length;
- Element elt;
- if (len >= 3 && words[len - 2] == "->") {
- elt = currModel.TryMkElement(lastWord);
- if (elt == null) BadModel("bad parition value " + lastWord);
- len -= 2;
- } else {
- elt = currModel.MkElement(words[0]);
- }
- partitionMapping.Add(partName, elt);
- for (int i = 1; i < len; ++i) {
- var name = words[i];
- if (i == 1 && name[0] == '{')
- name = name.Substring(1);
- if (i == len - 1 && name.EndsWith("}"))
- name = name.Substring(0, name.Length - 1);
- var cnst = currModel.MkFunc(name, 0);
- cnst.SetConstant(elt);
- }
-
- } else if (words.Length == 3 && words[1] == "->") {
+ if (words.Count == 3 && words[1] is string && ((string) words[1]) == "->") {
Func fn = null;
- var funName = words[0];
+ var funName = (string) words[0];
- if (lastWord == "{") {
+ if (lastWord is string && ((string) lastWord) == "{") {
for ( ; ; ) {
- var tuple = GetFunctionTuple();
+ var tuple = GetFunctionTuple(ReadLine());
if (tuple == null) BadModel("EOF in function table");
if (tuple.Count == 0) continue;
string tuple0 = tuple[0] as string;
diff --git a/Test/inline/Answer b/Test/inline/Answer index ae632f79..2c29ab0b 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1439,6 +1439,197 @@ implementation bar() Boogie program verifier finished with 5 verified, 0 errors
+-------------------- test7.bpl --------------------
+
+var g: int;
+
+procedure main();
+ modifies g;
+
+
+
+implementation main()
+{
+
+ anon0:
+ g := 0;
+ call foo();
+ assert g == 1;
+ return;
+}
+
+
+
+procedure foo();
+ modifies g;
+
+
+
+implementation foo()
+{
+
+ anon0:
+ g := g + 1;
+ return;
+}
+
+
+after inlining procedure calls
+procedure main();
+ modifies g;
+
+
+implementation main()
+{
+ var inline$foo$0$g: int;
+
+ anon0:
+ g := 0;
+ goto inline$foo$0$Entry;
+
+ inline$foo$0$Entry:
+ inline$foo$0$g := g;
+ goto inline$foo$0$anon0;
+
+ inline$foo$0$anon0:
+ g := g + 1;
+ goto inline$foo$0$Return;
+
+ inline$foo$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ assert g == 1;
+ return;
+}
+
+
+
+Boogie program verifier finished with 2 verified, 0 errors
+-------------------- test8.bpl --------------------
+
+var g: int;
+
+procedure main();
+ modifies g;
+
+
+
+implementation main()
+{
+
+ anon0:
+ g := 0;
+ call foo();
+ assert g == 1;
+ return;
+}
+
+
+
+procedure {:inline 1} foo();
+ modifies g;
+
+
+
+implementation foo()
+{
+
+ anon0:
+ call bar();
+ return;
+}
+
+
+
+procedure bar();
+ modifies g;
+
+
+
+implementation bar()
+{
+
+ anon0:
+ g := g + 1;
+ return;
+}
+
+
+after inlining procedure calls
+procedure main();
+ modifies g;
+
+
+implementation main()
+{
+ var inline$foo$0$g: int;
+ var inline$bar$0$g: int;
+
+ anon0:
+ g := 0;
+ goto inline$foo$0$Entry;
+
+ inline$foo$0$Entry:
+ inline$foo$0$g := g;
+ goto inline$foo$0$anon0;
+
+ inline$foo$0$anon0:
+ goto inline$bar$0$Entry;
+
+ inline$bar$0$Entry:
+ inline$bar$0$g := g;
+ goto inline$bar$0$anon0;
+
+ inline$bar$0$anon0:
+ g := g + 1;
+ goto inline$bar$0$Return;
+
+ inline$bar$0$Return:
+ goto inline$foo$0$anon0$1;
+
+ inline$foo$0$anon0$1:
+ goto inline$foo$0$Return;
+
+ inline$foo$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ assert g == 1;
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 1} foo();
+ modifies g;
+
+
+implementation foo()
+{
+ var inline$bar$0$g: int;
+
+ anon0:
+ goto inline$bar$0$Entry;
+
+ inline$bar$0$Entry:
+ inline$bar$0$g := g;
+ goto inline$bar$0$anon0;
+
+ inline$bar$0$anon0:
+ g := g + 1;
+ goto inline$bar$0$Return;
+
+ inline$bar$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+
+Boogie program verifier finished with 3 verified, 0 errors
-------------------- test5.bpl --------------------
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index f56d55a0..3a8b0a9d 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -13,6 +13,11 @@ for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do ( %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f
)
+for %%f in (test7.bpl test8.bpl) do (
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /inline:spec /inlineDepth:1 /print:- /env:0 /printInlined /noinfer %%f
+)
+
for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
diff --git a/Test/inline/test7.bpl b/Test/inline/test7.bpl new file mode 100644 index 00000000..b5c6a4c6 --- /dev/null +++ b/Test/inline/test7.bpl @@ -0,0 +1,15 @@ +var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert g == 1;
+}
+
+procedure foo()
+modifies g;
+{
+ g := g + 1;
+}
\ No newline at end of file diff --git a/Test/inline/test8.bpl b/Test/inline/test8.bpl new file mode 100644 index 00000000..12eab481 --- /dev/null +++ b/Test/inline/test8.bpl @@ -0,0 +1,21 @@ +var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert g == 1;
+}
+
+procedure {:inline 1} foo()
+modifies g;
+{
+ call bar();
+}
+
+procedure bar()
+modifies g;
+{
+ g := g + 1;
+}
\ No newline at end of file diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index e1ff7176..3ecae08a 100644 --- a/_admin/Boogie/aste/summary.log +++ b/_admin/Boogie/aste/summary.log @@ -1,21 +1,21 @@ -# Aste started: 2011-11-01 07:00:10
+# Aste started: 2011-11-12 07:00:04
# Host id: Boogiebox
# Configuration: boogie.cfg
# Task: aste.tasks.boogie.FullBuild
-# [2011-11-01 07:03:36] SpecSharp revision: 979f82b8db6c
-# [2011-11-01 07:03:36] SscBoogie revision: 979f82b8db6c
-# [2011-11-01 07:05:13] Boogie revision: f402d8e0fc1b
-[2011-11-01 07:06:40] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
+# [2011-11-12 07:03:24] SpecSharp revision: 31c83dcaabce
+# [2011-11-12 07:03:24] SscBoogie revision: 31c83dcaabce
+# [2011-11-12 07:05:06] Boogie revision: c4b860ad3af4
+[2011-11-12 07:06:26] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
1>corflags : warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
-[2011-11-01 07:08:09] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
+[2011-11-12 07:07:59] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
- D:\Temp\aste\Boogie\Source\Core\Absy.cs(710,9): warning CS0162: Unreachable code detected
+ D:\Temp\aste\Boogie\Source\Core\Absy.cs(749,9): warning CS0162: Unreachable code detected
D:\Temp\aste\Boogie\Source\Core\OOLongUtil.cs(109,7): warning CS0162: Unreachable code detected
- D:\Temp\aste\Boogie\Source\Core\Absy.cs(679,7): warning CC1036: Detected call to method 'Graphing.Graph`1<Microsoft.Boogie.Block>.TopologicalSort' without [Pure] in contracts of method 'Microsoft.Boogie.Program.GraphFromImpl(Microsoft.Boogie.Implementation)'.
+ D:\Temp\aste\Boogie\Source\Core\Absy.cs(718,7): warning CC1036: Detected call to method 'Graphing.Graph`1<Microsoft.Boogie.Block>.TopologicalSort' without [Pure] in contracts of method 'Microsoft.Boogie.Program.GraphFromImpl(Microsoft.Boogie.Implementation)'.
EXEC : warning CC1079: Type Microsoft.Boogie.Variable implements Microsoft.AbstractInterpretationFramework.IVariable.get_Name by inheriting Microsoft.Boogie.NamedDeclaration.get_Name causing the interface contract to not be checked at runtime. Consider adding a wrapper method.
D:\Temp\aste\Boogie\Source\Core\Parser.cs(111,3): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.
D:\Temp\aste\Boogie\Source\Core\Parser.cs(116,5): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.
@@ -41,5 +41,5 @@ warning CS0162: Unreachable code detected
warning CS0219: The variable 'expand' is assigned but its value is never used
warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.
-[2011-11-01 08:02:30] 0 out of 31 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
-# [2011-11-01 08:02:53] Released nightly of Boogie
+[2011-11-12 08:05:27] 0 out of 31 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
+# [2011-11-12 08:06:33] Released nightly of Boogie
|