diff options
| author |  Sam Blackshear <unknown> | 2011-05-24 14:46:12 +0530 |
|---|---|---|
| committer | Sam Blackshear <unknown> | 2011-05-24 14:46:12 +0530 |
| commit | 40e4151cb1072695f1a2aed297206203481cdd66 (patch) | |
| tree | a89f729fd386fd1ede2421faee65c4fc69e428db /BCT | |
| parent | 5cfbcc0fed2cc711ddcd6702ebd821cff95103ab (diff) | |
| parent | 356651d4f4e2d9825f18858603f506332d582ad5 (diff) | |
merge
Diffstat (limited to 'BCT')
| -rw-r--r-- | BCT/BytecodeTranslator/BytecodeTranslator.csproj | 12 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 641 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 71 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 4 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 50 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 93 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 35 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 34 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TraverserFactory.cs | 6 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/WholeProgram.cs | 88 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 589 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 617 |
12 files changed, 1372 insertions, 868 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj index 86fc4a5d..e4575480 100644 --- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj +++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj @@ -32,6 +32,7 @@ <UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
<TargetFrameworkProfile />
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -41,7 +42,7 @@ <DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
<CodeContractsCustomRewriterAssembly>
</CodeContractsCustomRewriterAssembly>
<CodeContractsCustomRewriterClass>
@@ -67,6 +68,15 @@ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
<CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
<CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 29c0033f..08e32248 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -138,6 +138,16 @@ namespace BytecodeTranslator }
public override void Visit(IArrayIndexer arrayIndexer) {
+
+#if EXPERIMENTAL
+ if (!IsAtomicInstance(arrayIndexer.IndexedObject)) {
+ // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.
+ var se = ExpressionSimplifier.Simplify(this.sink, arrayIndexer);
+ this.Visit(se);
+ return;
+ }
+#endif
+
this.Visit(arrayIndexer.IndexedObject);
Bpl.Expr arrayExpr = TranslatedExpressions.Pop();
this.Visit(arrayIndexer.Indices);
@@ -155,6 +165,9 @@ namespace BytecodeTranslator indexExpr = new Bpl.NAryExpr(arrayIndexer.Token(), new Bpl.FunctionCall(f), new Bpl.ExprSeq(indexExprs));
}
+#if EXPERIMENTAL
+ this.TranslatedExpressions.Push(arrayExpr);
+#else
Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(arrayIndexer.Type));
Bpl.Expr selectExpr = sink.Heap.ReadHeap(arrayExpr, indexExpr, AccessType.Array, temp.Type);
this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, selectExpr));
@@ -162,10 +175,22 @@ namespace BytecodeTranslator this.arrayExpr = arrayExpr;
this.indexExpr = indexExpr;
+#endif
}
public override void Visit(ITargetExpression targetExpression)
{
+#if EXPERIMENTAL
+ Contract.Assume(false, "The expression containing this as a subexpression should never allow a call to this routine.");
+
+ if (targetExpression.Instance != null && !IsAtomicInstance(targetExpression.Instance)) {
+ //// Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.
+ var se = ExpressionSimplifier.Simplify(this.sink, targetExpression);
+ this.Visit(se);
+ return;
+ }
+#endif
+
#region ArrayIndexer
IArrayIndexer/*?*/ indexer = targetExpression.Definition as IArrayIndexer;
if (indexer != null)
@@ -252,11 +277,14 @@ namespace BytecodeTranslator public override void Visit(IBoundExpression boundExpression)
{
- //if (boundExpression.Instance != null)
- //{
- // this.Visit(boundExpression.Instance);
- // // TODO: (mschaef) look where it's bound and do something
- //}
+
+ if (boundExpression.Instance != null && !IsAtomicInstance(boundExpression.Instance)) {
+ // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.
+ var se = ExpressionSimplifier.Simplify(this.sink, boundExpression);
+ this.Visit(se);
+ return;
+ }
+
#region Local
ILocalDefinition local = boundExpression.Definition as ILocalDefinition;
if (local != null)
@@ -290,9 +318,9 @@ namespace BytecodeTranslator }
else {
Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
- Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(field.ResolvedField.Type));
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, temp.Type)));
- TranslatedExpressions.Push(temp);
+ var bplType = this.sink.CciTypeToBoogie(field.Type);
+ var e = this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, bplType);
+ this.TranslatedExpressions.Push(e);
}
}
return;
@@ -339,6 +367,14 @@ namespace BytecodeTranslator #endregion
}
+ internal static bool IsAtomicInstance(IExpression expression) {
+ var thisInst = expression as IThisReference;
+ if (thisInst != null) return true;
+ var be = expression as IBoundExpression;
+ if (be == null) return false;
+ return be.Instance == null;
+ }
+
public override void Visit(IPopValue popValue) {
var locExpr = this.StmtTraverser.operandStack.Pop();
this.TranslatedExpressions.Push(locExpr);
@@ -433,102 +469,26 @@ namespace BytecodeTranslator MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None));
}
- #region Translate In and Out Parameters
- var inexpr = new List<Bpl.Expr>();
- var outvars = new List<Bpl.IdentifierExpr>();
-
- #region Create the 'this' argument for the function call
- Bpl.IdentifierExpr thisExpr = null;
- List<Bpl.Variable> locals = null;
- List<IFieldDefinition> args = null;
- Bpl.Expr arrayExpr = null;
- Bpl.Expr indexExpr = null;
- if (!methodCall.IsStaticCall) {
- this.collectStructFields = true;
- this.structFields = new List<IFieldDefinition>();
- this.arrayExpr = null;
- this.indexExpr = null;
- this.Visit(methodCall.ThisArgument);
- this.collectStructFields = false;
- args = this.structFields;
- arrayExpr = this.arrayExpr;
- indexExpr = this.indexExpr;
-
- var e = this.TranslatedExpressions.Pop();
- inexpr.Add(e);
- if (e is Bpl.NAryExpr) {
- e = ((Bpl.NAryExpr)e).Args[0];
- }
- thisExpr = e as Bpl.IdentifierExpr;
- locals = new List<Bpl.Variable>();
- Bpl.Variable x = thisExpr.Decl;
- locals.Add(x);
- for (int i = 0; i < args.Count; i++) {
- Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));
- Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);
- StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, y.TypedIdent.Type)));
- x = y;
- locals.Add(y);
- }
- }
- if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {
- outvars.Add(thisExpr);
- }
- #endregion
+ Bpl.IToken cloc = methodCall.Token();
- Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();
- Dictionary<IParameterDefinition, Bpl.IdentifierExpr> p2eMap = new Dictionary<IParameterDefinition, Bpl.IdentifierExpr>();
- IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
- penum.MoveNext();
- foreach (IExpression exp in methodCall.Arguments) {
- if (penum.Current == null) {
- throw new TranslationException("More arguments than parameters in method call");
- }
- this.Visit(exp);
- Bpl.Expr e = this.TranslatedExpressions.Pop();
- if (penum.Current.Type is IGenericTypeParameter)
- inexpr.Add(sink.Heap.Box(methodCall.Token(), this.sink.CciTypeToBoogie(exp.Type), e));
- else
- inexpr.Add(e);
- if (penum.Current.IsByReference) {
- Bpl.IdentifierExpr unboxed = e as Bpl.IdentifierExpr;
- if (unboxed == null) {
- throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");
- }
- if (penum.Current.Type is IGenericTypeParameter) {
- Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));
- toBoxed[unboxed] = boxed;
- outvars.Add(boxed);
- }
- else {
- outvars.Add(unboxed);
- }
- }
- penum.MoveNext();
- }
- #endregion
+ List<Bpl.Expr> inexpr;
+ List<Bpl.IdentifierExpr> outvars;
+ Bpl.IdentifierExpr thisExpr;
+ List<Bpl.Variable> locals;
+ List<IFieldDefinition> args;
+ Bpl.Expr arrayExpr;
+ Bpl.Expr indexExpr;
+ Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;
+ var proc = TranslateArgumentsAndReturnProcedure(cloc, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out locals, out args, out arrayExpr, out indexExpr, out toBoxed);
- Bpl.IToken cloc = methodCall.Token();
- if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
- Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);
- Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(cloc, v);
- if (resolvedMethod.Type is IGenericTypeParameter) {
- Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));
- toBoxed[unboxed] = boxed;
- outvars.Add(boxed);
- }
- else {
- outvars.Add(unboxed);
- }
- TranslatedExpressions.Push(unboxed);
- }
- var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
string methodname = proc.Name;
-
+ var translateAsFunctionCall = proc is Bpl.Function;
Bpl.QKeyValue attrib = null;
- foreach (var a in resolvedMethod.Attributes) {
- if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
- attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);
+ if (!translateAsFunctionCall) {
+ foreach (var a in resolvedMethod.Attributes) {
+ if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
+ attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);
+ }
}
}
@@ -563,13 +523,24 @@ namespace BytecodeTranslator else {
this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));
}
- }
- else {
- if (attrib != null)
- call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);
- else
- call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
- this.StmtTraverser.StmtBuilder.Add(call);
+ } else {
+ if (translateAsFunctionCall) {
+ var func = proc as Bpl.Function;
+ var exprSeq = new Bpl.ExprSeq();
+ foreach (var e in inexpr) {
+ exprSeq.Add(e);
+ }
+ var callFunction = new Bpl.NAryExpr(cloc, new Bpl.FunctionCall(func), exprSeq);
+ this.TranslatedExpressions.Push(callFunction);
+ return;
+
+ } else {
+ if (attrib != null)
+ call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);
+ else
+ call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ }
}
foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {
@@ -596,6 +567,99 @@ namespace BytecodeTranslator }
}
+ protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable<IExpression> arguments, out List<Bpl.Expr> inexpr, out List<Bpl.IdentifierExpr> outvars, out Bpl.IdentifierExpr thisExpr, out List<Bpl.Variable> locals, out List<IFieldDefinition> args, out Bpl.Expr arrayExpr, out Bpl.Expr indexExpr, out Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed) {
+ inexpr = new List<Bpl.Expr>();
+ outvars = new List<Bpl.IdentifierExpr>();
+
+ #region Create the 'this' argument for the function call
+ thisExpr = null;
+ locals = null;
+ args = null;
+ arrayExpr = null;
+ indexExpr = null;
+ if (thisArg != null) {
+ this.collectStructFields = true;
+ this.structFields = new List<IFieldDefinition>();
+ this.arrayExpr = null;
+ this.indexExpr = null;
+ this.Visit(thisArg);
+ this.collectStructFields = false;
+ args = this.structFields;
+ arrayExpr = this.arrayExpr;
+ indexExpr = this.indexExpr;
+
+ var e = this.TranslatedExpressions.Pop();
+ inexpr.Add(e);
+ if (e is Bpl.NAryExpr) {
+ e = ((Bpl.NAryExpr)e).Args[0];
+ }
+ thisExpr = e as Bpl.IdentifierExpr;
+ locals = new List<Bpl.Variable>();
+ Bpl.Variable x = thisExpr.Decl;
+ locals.Add(x);
+ for (int i = 0; i < args.Count; i++) {
+ Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));
+ Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);
+ StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, y.TypedIdent.Type)));
+ x = y;
+ locals.Add(y);
+ }
+ }
+ if (thisArg != null && methodToCall.ContainingType.ResolvedType.IsStruct) {
+ outvars.Add(thisExpr);
+ }
+ #endregion
+
+ toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();
+ IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
+ penum.MoveNext();
+ foreach (IExpression exp in arguments) {
+ if (penum.Current == null) {
+ throw new TranslationException("More arguments than parameters in method call");
+ }
+ this.Visit(exp);
+ Bpl.Expr e = this.TranslatedExpressions.Pop();
+ if (penum.Current.Type is IGenericTypeParameter)
+ inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(exp.Type), e));
+ else
+ inexpr.Add(e);
+ if (penum.Current.IsByReference) {
+ Bpl.IdentifierExpr unboxed = e as Bpl.IdentifierExpr;
+ if (unboxed == null) {
+ throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");
+ }
+ if (penum.Current.Type is IGenericTypeParameter) {
+ Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));
+ toBoxed[unboxed] = boxed;
+ outvars.Add(boxed);
+ } else {
+ outvars.Add(unboxed);
+ }
+ }
+ penum.MoveNext();
+ }
+
+ var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
+
+ var translateAsFunctionCall = proc is Bpl.Function;
+ if (!translateAsFunctionCall) {
+ if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
+ Bpl.Variable v = this.sink.CreateFreshLocal(resolvedMethod.Type.ResolvedType);
+ Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v);
+ if (resolvedMethod.Type is IGenericTypeParameter) {
+ Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));
+ toBoxed[unboxed] = boxed;
+ outvars.Add(boxed);
+ } else {
+ outvars.Add(unboxed);
+ }
+ TranslatedExpressions.Push(unboxed);
+ }
+ }
+
+ return proc;
+ }
+
#endregion
#region Translate Assignments
@@ -604,6 +668,7 @@ namespace BytecodeTranslator private Bpl.Expr arrayExpr = null;
private Bpl.Expr indexExpr = null;
+#if EXPERIMENTAL
/// <summary>
///
/// </summary>
@@ -612,18 +677,119 @@ namespace BytecodeTranslator public override void Visit(IAssignment assignment) {
Contract.Assert(TranslatedExpressions.Count == 0);
+ var tok = assignment.Token();
+
+ object container = assignment.Target.Definition;
+
+ var/*?*/ local = container as ILocalDefinition;
+ if (local != null) {
+ Contract.Assume(assignment.Target.Instance == null);
+ this.Visit(assignment.Source);
+ var e = this.TranslatedExpressions.Pop();
+ var bplLocal = Bpl.Expr.Ident(this.sink.FindOrCreateLocalVariable(local));
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, bplLocal, e));
+ return;
+ }
+
+ var/*?*/ parameter = container as IParameterDefinition;
+ if (parameter != null) {
+ Contract.Assume(assignment.Target.Instance == null);
+ this.Visit(assignment.Source);
+ var e = this.TranslatedExpressions.Pop();
+ var bplParam = Bpl.Expr.Ident(this.sink.FindParameterVariable(parameter, this.contractContext));
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, bplParam, e));
+ return;
+ }
+
+ var/*?*/ field = container as IFieldReference;
+ if (field != null) {
+ this.Visit(assignment.Source);
+ var e = this.TranslatedExpressions.Pop();
+ var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field));
+ if (assignment.Target.Instance == null) {
+ // static fields are not kept in the heap
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, f, e));
+ } else {
+ if (field.ContainingType.ResolvedType.IsStruct) {
+ //var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);
+ //var s_prime_expr = Bpl.Expr.Ident(s_prime);
+ //var boogieType = sink.CciTypeToBoogie(field.Type);
+ //StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,
+ // field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,
+ // boogieType));
+ UpdateStruct(tok, assignment.Target.Instance, field, e);
+ } else {
+ this.Visit(assignment.Target.Instance);
+ var x = this.TranslatedExpressions.Pop();
+ var boogieType = sink.CciTypeToBoogie(field.Type);
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, x, f, e,
+ field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,
+ boogieType));
+ }
+ }
+ return;
+ }
+
+ var/*?*/ arrayIndexer = container as IArrayIndexer;
+ if (arrayIndexer != null) {
+ this.Visit(assignment.Target.Instance);
+ var x = this.TranslatedExpressions.Pop();
+ this.Visit(arrayIndexer.Indices);
+ var indices_prime = this.TranslatedExpressions.Pop();
+ this.Visit(assignment.Source);
+ var e = this.TranslatedExpressions.Pop();
+ StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, x, indices_prime, e, AccessType.Array, sink.CciTypeToBoogie(arrayIndexer.Type)));
+ return;
+ }
+
+ Contract.Assume(false);
+ }
+
+ private void UpdateStruct(Bpl.IToken tok, IExpression iExpression, IFieldReference field, Bpl.Expr e) {
+ var addrOf = iExpression as IAddressOf;
+ if (addrOf == null) return;
+ var addressableExpression = addrOf.Expression as IAddressableExpression;
+ if (addressableExpression == null) return;
+
+ var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field));
+
+ if (addressableExpression.Instance == null) {
+ var boogieType = sink.CciTypeToBoogie(field.Type);
+ this.Visit(addressableExpression);
+ var def = this.TranslatedExpressions.Pop();
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, def, f, e,
+ AccessType.Struct,
+ boogieType));
+ } else {
+ var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);
+ var s_prime_expr = Bpl.Expr.Ident(s_prime);
+ var boogieType = sink.CciTypeToBoogie(field.Type);
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,
+ AccessType.Struct,
+ boogieType));
+ UpdateStruct(tok, addressableExpression.Instance, addressableExpression.Definition as IFieldReference, s_prime_expr);
+ }
+ }
+
+#else
+
+ public override void Visit(IAssignment assignment) {
+ Contract.Assert(TranslatedExpressions.Count == 0);
+
#region Transform Right Hand Side ...
this.Visit(assignment.Source);
- Bpl.Expr sourceexp = this.TranslatedExpressions.Pop();
+ var sourceexp = this.TranslatedExpressions.Pop();
#endregion
// Simplify the LHS so that all nested dereferences and method calls are broken
// up into separate assignments to locals.
- var blockExpression = AssignmentSimplifier.Simplify(this.sink, assignment.Target);
- foreach (var s in blockExpression.BlockStatement.Statements) {
- this.StmtTraverser.Visit(s);
- }
- var target = blockExpression.Expression as ITargetExpression;
+ //var blockExpression = ExpressionSimplifier.Simplify(this.sink, assignment.Target) as IBlockExpression;
+ //foreach (var s in blockExpression.BlockStatement.Statements) {
+ // this.StmtTraverser.Visit(s);
+ //}
+ //var target = blockExpression.Expression as ITargetExpression;
+
+ var target = assignment.Target;
List<IFieldDefinition> args = null;
Bpl.Expr arrayExpr = null;
@@ -643,8 +809,7 @@ namespace BytecodeTranslator Bpl.IdentifierExpr f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(fieldReference.ResolvedField));
if (target.Instance == null) {
StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(assignment.Token(), f, sourceexp));
- }
- else {
+ } else {
Debug.Assert(args != null);
List<Bpl.Variable> locals = new List<Bpl.Variable>();
Bpl.IdentifierExpr instanceExpr = TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
@@ -715,6 +880,8 @@ namespace BytecodeTranslator return;
}
+#endif
+
#endregion
#region Translate Object Creation
@@ -725,77 +892,35 @@ namespace BytecodeTranslator /// </summary>
public override void Visit(ICreateObjectInstance createObjectInstance)
{
- TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance);
- }
-
- public override void Visit(ICreateArray createArrayInstance)
- {
- TranslateArrayCreation(createArrayInstance);
- }
-
- public override void Visit(ICreateDelegateInstance createDelegateInstance)
- {
- if (createDelegateInstance.Instance == null) {
- TranslatedExpressions.Push(Bpl.Expr.Literal(0));
- }
- else {
- this.Visit(createDelegateInstance.Instance);
- }
-
- TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type, createDelegateInstance);
- }
-
- private void TranslateArrayCreation(IExpression creationAST)
- {
- Bpl.IToken cloc = creationAST.Token();
-
- var a = this.sink.CreateFreshLocal(creationAST.Type);
-
- // First generate an Alloc() call
- this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
-
- TranslatedExpressions.Push(Bpl.Expr.Ident(a));
- }
-
- private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, IExpression creationAST)
- {
+ var ctor = createObjectInstance.MethodToCall;
var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;
- Bpl.IToken token = creationAST.Token();
-
- var a = this.sink.CreateFreshLocal(creationAST.Type);
+ Bpl.IToken token = createObjectInstance.Token();
+
+ var a = this.sink.CreateFreshLocal(createObjectInstance.Type);
// First generate an Alloc() call
this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
// Second, generate the call to the appropriate ctor
- var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
- Bpl.ExprSeq inexpr = new Bpl.ExprSeq();
- inexpr.Add(Bpl.Expr.Ident(a));
- IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
- penum.MoveNext();
- foreach (IExpression exp in arguments) {
- if (penum.Current == null) {
- throw new TranslationException("More Arguments than Parameters in functioncall");
- }
- this.Visit(exp);
- Bpl.Expr e = this.TranslatedExpressions.Pop();
- if (penum.Current.Type is IGenericTypeParameter)
- inexpr.Add(sink.Heap.Box(ctor.Token(), this.sink.CciTypeToBoogie(exp.Type), e));
- else
- inexpr.Add(e);
- penum.MoveNext();
- }
- Bpl.IdentifierExprSeq outvars = new Bpl.IdentifierExprSeq();
+ List<Bpl.Expr> inexpr;
+ List<Bpl.IdentifierExpr> outvars;
+ Bpl.IdentifierExpr thisExpr;
+ List<Bpl.Variable> locals;
+ List<IFieldDefinition> args;
+ Bpl.Expr arrayExpr;
+ Bpl.Expr indexExpr;
+ Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;
+ var proc = TranslateArgumentsAndReturnProcedure(token, ctor, resolvedMethod, null, createObjectInstance.Arguments, out inexpr, out outvars, out thisExpr, out locals, out args, out arrayExpr, out indexExpr, out toBoxed);
this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, proc.Name, inexpr, outvars));
// Generate assumption about the dynamic type of the just allocated object
this.StmtTraverser.StmtBuilder.Add(
- new Bpl.AssumeCmd(token,
+ new Bpl.AssumeCmd(token,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(inexpr[0]),
- Bpl.Expr.Ident(this.sink.FindOrCreateType(creationAST.Type))
+ Bpl.Expr.Ident(this.sink.FindOrCreateType(createObjectInstance.Type))
)
)
);
@@ -803,6 +928,37 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
+ public override void Visit(ICreateArray createArrayInstance)
+ {
+ Bpl.IToken cloc = createArrayInstance.Token();
+ var a = this.sink.CreateFreshLocal(createArrayInstance.Type);
+
+ Debug.Assert(createArrayInstance.Rank > 0);
+ Bpl.Expr lengthExpr = Bpl.Expr.Literal(1);
+ foreach (IExpression expr in createArrayInstance.Sizes) {
+ this.Visit(expr);
+ lengthExpr = Bpl.Expr.Mul(lengthExpr, TranslatedExpressions.Pop());
+ }
+
+ // First generate an Alloc() call
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
+ Bpl.Expr assumeExpr = Bpl.Expr.Eq(new Bpl.NAryExpr(cloc, new Bpl.FunctionCall(this.sink.Heap.ArrayLengthFunction), new Bpl.ExprSeq(Bpl.Expr.Ident(a))), lengthExpr);
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.AssumeCmd(cloc, assumeExpr));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(a));
+ }
+
+ public override void Visit(ICreateDelegateInstance createDelegateInstance)
+ {
+ if (createDelegateInstance.Instance == null) {
+ TranslatedExpressions.Push(Bpl.Expr.Literal(0));
+ }
+ else {
+ this.Visit(createDelegateInstance.Instance);
+ }
+
+ TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type, createDelegateInstance);
+ }
+
private void TranslateDelegateCreation(IMethodReference methodToCall, ITypeReference type, IExpression creationAST)
{
Bpl.IToken cloc = creationAST.Token();
@@ -1134,9 +1290,7 @@ namespace BytecodeTranslator public override void Visit(IVectorLength vectorLength) {
base.Visit(vectorLength.Vector);
var e = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(
- Bpl.Expr.Select(new Bpl.IdentifierExpr(vectorLength.Token(), this.sink.Heap.ArrayLengthVariable), new Bpl.Expr[] { e })
- );
+ TranslatedExpressions.Push(new Bpl.NAryExpr(vectorLength.Token(), new Bpl.FunctionCall(this.sink.Heap.ArrayLengthFunction), new Bpl.ExprSeq(e)));
}
#endregion
@@ -1161,74 +1315,125 @@ namespace BytecodeTranslator }
#endregion
+ public override void Visit(IBlockExpression blockExpression) {
+ this.StmtTraverser.Visit(blockExpression.BlockStatement);
+ this.Visit(blockExpression.Expression);
+ }
+
/// <summary>
/// This is a rewriter so it must be used on a mutable Code Model!!!
/// </summary>
- private class AssignmentSimplifier : CodeRewriter {
+ private class ExpressionSimplifier : CodeRewriter {
Sink sink;
- private List<IStatement> localDeclarations = new List<IStatement>();
- private AssignmentSimplifier(Sink sink)
+ private ExpressionSimplifier(Sink sink)
: base(sink.host) {
this.sink = sink;
}
- public static IBlockExpression Simplify(Sink sink, ITargetExpression targetExpression) {
- var a = new AssignmentSimplifier(sink);
- var leftOverExpression = a.Rewrite(targetExpression);
- return new BlockExpression() {
- BlockStatement = new BlockStatement() { Statements = a.localDeclarations, },
- Expression = leftOverExpression,
- Type = targetExpression.Type,
- };
+ public static IExpression Simplify(Sink sink, IExpression expression) {
+ var a = new ExpressionSimplifier(sink);
+ return a.Rewrite(expression);
}
public override IExpression Rewrite(IBoundExpression boundExpression) {
- if (boundExpression.Instance == null)
- return base.Rewrite(boundExpression); // REVIEW: Maybe just stop the rewriting and return boundExpression?
- var e = base.Rewrite(boundExpression);
- boundExpression = e as IBoundExpression;
- if (boundExpression == null) return e;
+
+ if (ExpressionTraverser.IsAtomicInstance(boundExpression.Instance)) return boundExpression;
+
+ // boundExpression == BE(inst, def), i.e., inst.def
+ // return { loc := e; [assert loc != null;] | BE(BE(null,loc), def) }, i.e., "loc := e; loc.def"
+ // where e is the rewritten inst
+
+ var e = base.Rewrite(boundExpression.Instance);
+
var loc = new LocalDefinition() {
- Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()), // TODO: should make the name unique within the method containing the assignment
+ Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),
Type = boundExpression.Type,
};
- this.localDeclarations.Add(
- new LocalDeclarationStatement() {
- InitialValue = boundExpression,
- LocalVariable = loc,
- }
- );
- return new BoundExpression() {
- Definition = loc,
- Instance = null,
- Type = boundExpression.Type,
+ var locDecl = new LocalDeclarationStatement() {
+ InitialValue = e,
+ LocalVariable = loc,
+ };
+ return new BlockExpression() {
+ BlockStatement = new BlockStatement() {
+ Statements = new List<IStatement> { locDecl },
+ },
+ Expression = new BoundExpression() {
+ Definition = boundExpression.Definition,
+ Instance = new BoundExpression() {
+ Definition = loc,
+ Instance = null,
+ Type = loc.Type,
+ },
+ Type = boundExpression.Type,
+ },
};
+
}
- public override IExpression Rewrite(IMethodCall methodCall) {
+ public override IExpression Rewrite(IArrayIndexer arrayIndexer) {
+ if (ExpressionTraverser.IsAtomicInstance(arrayIndexer.IndexedObject)) return arrayIndexer;
+
+ // arrayIndexer == AI(inst, [index]), i.e., inst[index0, index1,...]
+ // return { loc := e; [assert loc != null;] | AI(BE(null,loc), [index]) }
+ // where e is the rewritten array instance
- var e = base.Rewrite(methodCall); // simplify anything deeper in the tree
- methodCall = e as IMethodCall;
- if (methodCall == null) return e;
+ var e = base.Rewrite(arrayIndexer.IndexedObject);
var loc = new LocalDefinition() {
- Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment
- Type = methodCall.Type,
+ Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),
+ Type = arrayIndexer.Type,
};
- this.localDeclarations.Add(
- new LocalDeclarationStatement() {
- InitialValue = methodCall,
- LocalVariable = loc,
- }
- );
- return new BoundExpression() {
- Definition = loc,
- Instance = null,
- Type = methodCall.Type,
+ var locDecl = new LocalDeclarationStatement() {
+ InitialValue = e,
+ LocalVariable = loc,
};
+ return new BlockExpression() {
+ BlockStatement = new BlockStatement() {
+ Statements = new List<IStatement> { locDecl },
+ },
+ Expression = new ArrayIndexer() {
+ IndexedObject = new BoundExpression() {
+ Definition = loc,
+ Instance = null,
+ Type = loc.Type,
+ },
+ Indices = new List<IExpression>(arrayIndexer.Indices),
+ Type = arrayIndexer.Type,
+ },
+ };
+ }
+
+#if EXPERIMENTAL
+ public override ITargetExpression Rewrite(ITargetExpression targetExpression) {
+ Contract.Assume(false, "The expression containing this as a subexpression should never allow a call to this routine.");
+ return null;
}
+#endif
+
+ //public override IExpression Rewrite(IMethodCall methodCall) {
+
+ // var e = base.Rewrite(methodCall); // simplify anything deeper in the tree
+ // methodCall = e as IMethodCall;
+ // if (methodCall == null) return e;
+
+ // var loc = new LocalDefinition() {
+ // Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment
+ // Type = methodCall.Type,
+ // };
+ // this.localDeclarations.Add(
+ // new LocalDeclarationStatement() {
+ // InitialValue = methodCall,
+ // LocalVariable = loc,
+ // }
+ // );
+ // return new BoundExpression() {
+ // Definition = loc,
+ // Instance = null,
+ // Type = methodCall.Type,
+ // };
+ //}
}
}
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 283a59a3..87d950c4 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -56,6 +56,35 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x ); axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );
axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
+{
+ $result := $TypeOf($DynamicType(this));
+}
+function $TypeOfInv(Ref): Type;
+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
+
+function $ThreadDelegate(Ref) : Ref;
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+{
+ call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
+}
+procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start(this: Ref)
+{
+ call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
+}
+procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
+
";
private Sink sink;
@@ -71,7 +100,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); this.TypeType = new Bpl.CtorType(this.TypeTypeDecl.tok, this.TypeTypeDecl, new Bpl.TypeSeq());
this.RefType = new Bpl.CtorType(this.RefTypeDecl.tok, this.RefTypeDecl, new Bpl.TypeSeq());
this.RealType = new Bpl.CtorType(this.RealTypeDecl.tok, this.RealTypeDecl, new Bpl.TypeSeq());
- }
+ }
return b;
}
@@ -82,6 +111,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
+ fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
Bpl.IToken tok = field.Token();
Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType);
@@ -100,6 +130,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
Bpl.Variable v;
string eventName = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
+ eventName = TranslationHelper.TurnStringIntoValidIdentifier(eventName);
Bpl.IToken tok = e.Token();
Bpl.Type t = this.sink.CciTypeToBoogie(e.Type.ResolvedType);
@@ -108,7 +139,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); v = new Bpl.GlobalVariable(tok, tident);
}
else {
- Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Bpl.Type.Int), t);
+ Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(this.RefType), t);
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, mt);
v = new Bpl.GlobalVariable(tok, tident);
}
@@ -125,11 +156,11 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); /// </param>
public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.Expr f, AccessType accessType, Bpl.Type unboxType) {
if (accessType == AccessType.Struct)
- return Bpl.Expr.Select(o, f);
+ return Unbox(f.tok, unboxType, Bpl.Expr.Select(o, f));
else if (accessType == AccessType.Heap)
return Bpl.Expr.Select(f, o);
else
- return Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f);
+ return Unbox(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f));
}
/// <summary>
@@ -139,11 +170,11 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.Expr f, Bpl.Expr value, AccessType accessType, Bpl.Type boxType) {
Debug.Assert(o != null);
if (accessType == AccessType.Struct)
- return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, value);
+ return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, Box(f.tok, boxType, value));
else if (accessType == AccessType.Heap)
return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)f, o, value);
else
- return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, value)));
+ return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, Box(f.tok, boxType, value))));
}
}
@@ -192,6 +223,33 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x ); axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );
axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
+{
+ $result := $TypeOf($DynamicType(this));
+}
+function $TypeOfInv(Ref): Type;
+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
+
+function $ThreadDelegate(Ref) : Ref;
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+{
+ call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
+}
+procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start(this: Ref)
+{
+ call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
+}
+procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
";
private Sink sink;
@@ -239,6 +297,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x ); public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
Bpl.Variable v;
string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
+ fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
Bpl.IToken tok = e.Token();
if (e.Adder.ResolvedMethod.IsStatic) {
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 6d03ef9f..004d4224 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -68,8 +68,8 @@ namespace BytecodeTranslator { {
[RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Box;")]
public Bpl.Variable ArrayContentsVariable = null;
- [RepresentationFor("$ArrayLength", "var $ArrayLength: [Ref]int;")]
- public Bpl.Variable ArrayLengthVariable = null;
+ [RepresentationFor("$ArrayLength", "function $ArrayLength(Ref): int;")]
+ public Bpl.Function ArrayLengthFunction = null;
public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 58bec27f..75601140 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -30,23 +30,31 @@ namespace BytecodeTranslator { public readonly TraverserFactory factory;
- public readonly PdbReader/*?*/ PdbReader;
+ public readonly IDictionary<IUnit, PdbReader> PdbReaders;
+ public PdbReader/*?*/ PdbReader;
- public MetadataTraverser(Sink sink, PdbReader/*?*/ pdbReader)
+ public MetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)
: base() {
this.sink = sink;
this.factory = sink.Factory;
- this.PdbReader = pdbReader;
+ this.PdbReaders = pdbReaders;
}
#region Overrides
public override void Visit(IModule module) {
+ this.PdbReaders.TryGetValue(module, out this.PdbReader);
base.Visit(module);
}
public override void Visit(IAssembly assembly) {
- base.Visit(assembly);
+ this.PdbReaders.TryGetValue(assembly, out this.PdbReader);
+ this.sink.BeginAssembly(assembly);
+ try {
+ base.Visit(assembly);
+ } finally {
+ this.sink.EndAssembly(assembly);
+ }
}
/// <summary>
@@ -55,6 +63,9 @@ namespace BytecodeTranslator { ///
public override void Visit(ITypeDefinition typeDefinition) {
+ var savedPrivateTypes = this.privateTypes;
+ this.privateTypes = new List<ITypeDefinition>();
+
if (typeDefinition.IsClass) {
bool savedSawCctor = this.sawCctor;
this.sawCctor = false;
@@ -80,7 +91,12 @@ namespace BytecodeTranslator { TypeHelper.GetTypeName(typeDefinition));
throw new NotImplementedException(String.Format("Unknown kind of type definition '{0}'.", TypeHelper.GetTypeName(typeDefinition)));
}
+ this.Visit(typeDefinition.PrivateHelperMembers);
+ foreach (var t in this.privateTypes) {
+ this.Visit(t);
+ }
}
+ List<ITypeDefinition> privateTypes = new List<ITypeDefinition>();
private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) {
Contract.Requires(typeDefinition.IsStruct);
@@ -256,7 +272,11 @@ namespace BytecodeTranslator { #endregion
#region Translate body
- method.Body.Dispatch(stmtTraverser);
+ var helperTypes = stmtTraverser.TranslateMethod(method);
+ if (helperTypes != null) {
+ this.privateTypes.AddRange(helperTypes);
+ }
+ //method.Body.Dispatch(stmtTraverser);
#endregion
#region Create Local Vars For Implementation
@@ -272,6 +292,8 @@ namespace BytecodeTranslator { Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
#endregion
+ var translatedBody = stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken);
+
#region Add implementation to Boogie program
if (proc != null) {
Bpl.Implementation impl =
@@ -281,13 +303,14 @@ namespace BytecodeTranslator { decl.InParams,
decl.OutParams,
vseq,
- stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));
+ translatedBody);
impl.Proc = proc;
this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
} else { // method is translated as a function
- //Bpl.Function func = decl as Bpl.Function;
- //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), new List<Bpl.Block>{ new Bpl.Block(
+ //var func = decl as Bpl.Function;
+ //Contract.Assume(func != null);
+ //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), translatedBody.BigBlocks);
}
#endregion
@@ -366,6 +389,15 @@ namespace BytecodeTranslator { #endregion
+ #region Public API
+ public virtual void TranslateAssemblies(IEnumerable<IUnit> assemblies) {
+ foreach (var a in assemblies) {
+ a.Dispatch(this);
+ }
+ }
+ #endregion
+
+ #region Helpers
private class FindCtorCall : BaseCodeTraverser {
private bool isDeferringCtor = false;
public ITypeReference containingType;
@@ -387,5 +419,7 @@ namespace BytecodeTranslator { base.Visit(methodCall);
}
}
+ #endregion
+
}
}
\ No newline at end of file diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index f42c34d9..50ac68cf 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -25,6 +25,9 @@ namespace BytecodeTranslator { [OptionDescription("The names of the assemblies to use as input", ShortForm = "a")]
public List<string> assemblies = null;
+ [OptionDescription("Break into debugger", ShortForm = "break")]
+ public bool breakIntoDebugger = false;
+
[OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
public List<string> libpaths = new List<string>();
@@ -36,7 +39,7 @@ namespace BytecodeTranslator { public bool wholeProgram = false;
[OptionDescription("Stub assembly", ShortForm = "s")]
- public List<string>/*?*/ stubAssemblies = null;
+ public List<string>/*?*/ stub = null;
}
@@ -47,14 +50,21 @@ namespace BytecodeTranslator { static int Main(string[] args)
{
int result = 0;
+ int errorReturnValue = -1;
#region Parse options
var options = new Options();
options.Parse(args);
+ if (options.HelpRequested) {
+ options.PrintOptions("");
+ return errorReturnValue;
+ }
if (options.HasErrors) {
- if (options.HelpRequested)
- options.PrintOptions("");
- return 1;
+ options.PrintErrorsAndExit(Console.Out);
+ }
+
+ if (options.breakIntoDebugger) {
+ System.Diagnostics.Debugger.Break();
}
#endregion
@@ -81,7 +91,7 @@ namespace BytecodeTranslator { return 1;
}
- result = TranslateAssembly(assemblyNames, heap, options.libpaths, options.wholeProgram, options.stubAssemblies);
+ result = TranslateAssembly(assemblyNames, heap, options.libpaths, options.wholeProgram, options.stub);
} catch (Exception e) { // swallow everything and just return an error code
Console.WriteLine("The byte-code translator failed: {0}", e.Message);
@@ -98,7 +108,9 @@ namespace BytecodeTranslator { var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
Host = host;
- var modules = new List<Tuple<IModule,PdbReader/*?*/>>();
+ var modules = new List<IModule>();
+ var contractExtractors = new Dictionary<IUnit, IContractProvider>();
+ var pdbReaders = new Dictionary<IUnit, PdbReader>();
foreach (var a in assemblyNames) {
var module = host.LoadUnitFrom(a) as IModule;
if (module == null || module == Dummy.Module || module == Dummy.Assembly) {
@@ -112,7 +124,9 @@ namespace BytecodeTranslator { pdbReader = new PdbReader(pdbStream, host);
}
module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;
- modules.Add(Tuple.Create(module, pdbReader));
+ modules.Add(module);
+ contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));
+ pdbReaders.Add(module, pdbReader);
}
if (stubAssemblies != null) {
foreach (var s in stubAssemblies) {
@@ -132,12 +146,21 @@ namespace BytecodeTranslator { var copier = new CodeDeepCopier(host);
var mutableModule = copier.Copy(module);
- var mutator = new ReparentModule(host,
- TypeHelper.GetDefiningUnit(host.PlatformType.SystemObject.ResolvedType),
- mutableModule);
- module = mutator.Rewrite(mutableModule);
+ var mscorlib = TypeHelper.GetDefiningUnit(host.PlatformType.SystemObject.ResolvedType);
+
+ //var mutator = new ReparentModule(host, mscorlib, mutableModule);
+ //module = mutator.Rewrite(mutableModule);
+ //modules.Add(Tuple.Create(module, pdbReader));
+
+ RewriteUnitReferences renamer = new RewriteUnitReferences(host, mutableModule);
+ var mscorlibAssembly = (IAssembly)mscorlib;
+ renamer.targetAssembly = mscorlibAssembly;
+ renamer.originalAssemblyIdentity = mscorlibAssembly.AssemblyIdentity;
+ renamer.RewriteChildren(mutableModule);
+ modules.Add((IModule)mutableModule);
+ contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));
+ pdbReaders.Add(module, pdbReader);
- modules.Add(Tuple.Create(module, pdbReader));
}
}
if (modules.Count == 0) {
@@ -145,7 +168,7 @@ namespace BytecodeTranslator { return -1;
}
- var primaryModule = modules[0].Item1;
+ var primaryModule = modules[0];
TraverserFactory traverserFactory;
if (wholeProgram)
@@ -156,20 +179,8 @@ namespace BytecodeTranslator { var sink = new Sink(host, traverserFactory, heapFactory);
TranslationHelper.tmpVarCounter = 0;
- foreach (var tup in modules) {
-
- var module = tup.Item1;
- var pdbReader = tup.Item2;
-
- IAssembly/*?*/ assembly = null;
- MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, host.GetContractExtractor(module.ModuleIdentity), pdbReader);
- assembly = module as IAssembly;
- if (assembly != null)
- translator.Visit(assembly);
- else
- translator.Visit(module);
-
- }
+ MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
+ translator.TranslateAssemblies(modules);
foreach (ITypeDefinition type in sink.delegateTypeToDelegates.Keys) {
CreateDispatchMethod(sink, type);
@@ -340,6 +351,34 @@ namespace BytecodeTranslator { // Maybe this is a good place to add the procedure to the toplevel declarations
}
}
+
+ private class RewriteUnitReferences : MetadataRewriter {
+ private UnitIdentity sourceUnitIdentity = null;
+ internal IAssembly/*?*/ targetAssembly = null;
+ internal AssemblyIdentity/*?*/ originalAssemblyIdentity = null;
+
+ Dictionary<uint, bool> internedKeys = new Dictionary<uint, bool>();
+
+ public RewriteUnitReferences(IMetadataHost host, Module sourceUnit)
+ : base(host) {
+ this.sourceUnitIdentity = sourceUnit.UnitIdentity;
+ }
+
+ public override IModuleReference Rewrite(IModuleReference moduleReference) {
+ if (this.sourceUnitIdentity.Equals(moduleReference.UnitIdentity)) {
+ return this.targetAssembly;
+ }
+ return base.Rewrite(moduleReference);
+ }
+ public override IAssemblyReference Rewrite(IAssemblyReference assemblyReference) {
+ if (this.sourceUnitIdentity.Equals(assemblyReference.UnitIdentity)) {
+ return this.targetAssembly;
+ }
+ return base.Rewrite(assemblyReference);
+ }
+
+ }
+
}
}
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index b8d8334d..97fd4441 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -118,7 +118,7 @@ namespace BytecodeTranslator { return heap.StructType;
else if (type.IsEnum)
return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer
- else if (type is IGenericTypeParameter)
+ else if (type is IGenericTypeParameter)
return heap.BoxType;
else
return heap.RefType;
@@ -167,7 +167,9 @@ namespace BytecodeTranslator { Bpl.IToken tok = local.Token();
Bpl.Type t = CciTypeToBoogie(local.Type.ResolvedType);
if (!localVarMap.TryGetValue(local, out v)) {
- v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));
+ var name = local.Name.Value;
+ name = TranslationHelper.TurnStringIntoValidIdentifier(name);
+ v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, t));
localVarMap.Add(local, v);
}
return v;
@@ -334,6 +336,7 @@ namespace BytecodeTranslator { ProcedureInfo procAndFormalMap;
var key = method.InternedKey;
+
if (!this.declaredMethods.TryGetValue(key, out procAndFormalMap)) {
string MethodName = TranslationHelper.CreateUniqueMethodName(method);
@@ -375,7 +378,7 @@ namespace BytecodeTranslator { Bpl.Formal selfOut = null;
#region Create 'this' parameter
if (!method.IsStatic) {
- Bpl.Type selfType = CciTypeToBoogie(method.ContainingType);
+ var selfType = CciTypeToBoogie(method.ContainingType);
if (method.ContainingType.ResolvedType.IsStruct) {
//selfType = Heap.StructType;
in_count++;
@@ -470,15 +473,16 @@ namespace BytecodeTranslator { #endregion
+ var tok = method.Token();
Bpl.DeclWithFormals decl;
if (IsPure(method)) {
- var func = new Bpl.Function(method.Token(),
+ var func = new Bpl.Function(tok,
MethodName,
new Bpl.VariableSeq(invars),
this.RetVariable);
decl = func;
} else {
- var proc = new Bpl.Procedure(method.Token(),
+ var proc = new Bpl.Procedure(tok,
MethodName,
new Bpl.TypeVariableSeq(),
new Bpl.VariableSeq(invars),
@@ -488,7 +492,10 @@ namespace BytecodeTranslator { boogiePostcondition);
decl = proc;
}
-
+ if (this.assemblyBeingTranslated != null && !TypeHelper.GetDefiningUnitReference(method.ContainingType).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity)) {
+ var attrib = new Bpl.QKeyValue(tok, "extern", new List<object>(1), null);
+ decl.Attributes = attrib;
+ }
string newName = null;
if (IsStubMethod(method, out newName)) {
@@ -573,7 +580,8 @@ namespace BytecodeTranslator { public ProcedureInfo FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method) {
this.FindOrCreateProcedure(method);
- return this.declaredMethods[method.InternedKey];
+ var key = method.InternedKey;
+ return this.declaredMethods[key];
}
public static IMethodReference Unspecialize(IMethodReference method) {
IMethodReference result = method;
@@ -609,6 +617,10 @@ namespace BytecodeTranslator { t = this.Heap.CreateTypeVariable(type);
this.declaredTypes.Add(key, t);
this.TranslatedProgram.TopLevelDeclarations.Add(t);
+ if (this.assemblyBeingTranslated != null && !TypeHelper.GetDefiningUnitReference(type).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity)) {
+ var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);
+ t.Attributes = attrib;
+ }
}
return t;
}
@@ -634,6 +646,15 @@ namespace BytecodeTranslator { this.localCounter = 0;
}
+ public void BeginAssembly(IAssembly assembly) {
+ this.assemblyBeingTranslated = assembly;
+ }
+
+ public void EndAssembly(IAssembly assembly) {
+ this.assemblyBeingTranslated = null;
+ }
+ private IAssembly/*?*/ assemblyBeingTranslated;
+
public Dictionary<ITypeDefinition, HashSet<IMethodDefinition>> delegateTypeToDelegates = new Dictionary<ITypeDefinition, HashSet<IMethodDefinition>>();
public void AddDelegate(ITypeDefinition type, IMethodDefinition defn)
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 24b4b2ca..d26f540d 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -50,13 +50,37 @@ namespace BytecodeTranslator return etrav.TranslatedExpressions.Pop();
}
+ public ICollection<ITypeDefinition>/*?*/ TranslateMethod(IMethodDefinition method) {
+ var methodBody = method.Body as ISourceMethodBody;
+ if (methodBody == null) return null;
+ var block = methodBody.Block as BlockStatement;
+ // TODO: Error if cast fails?
+
+ ICollection<ITypeDefinition> newTypes = null;
+ if (block != null) {
+ var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);
+ newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);
+ }
+ this.Visit(methodBody);
+ return newTypes;
+ }
+
#endregion
- public override void Visit(IBlockStatement block) {
- Bpl.StmtListBuilder slb = new Bpl.StmtListBuilder();
+ //public override void Visit(ISourceMethodBody methodBody) {
+ // var block = methodBody.Block as BlockStatement;
+ // // TODO: Error if cast fails?
+
+ // if (block != null) {
+ // var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);
+ // var newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);
+ // }
+ // base.Visit(methodBody);
+ //}
- foreach (IStatement st in block.Statements) {
- this.Visit(st);
+ public override void Visit(IBlockStatement block) {
+ foreach (var s in block.Statements) {
+ this.Visit(s);
}
}
@@ -73,7 +97,7 @@ namespace BytecodeTranslator if (this.PdbReader != null) {
var slocs = this.PdbReader.GetClosestPrimarySourceLocationsFor(statement.Locations);
foreach (var sloc in slocs) {
- fileName = sloc.Document.Name.Value;
+ fileName = sloc.Document.Location;
lineNumber = sloc.StartLine;
break;
}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index cdc1c8a3..78c818bd 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -18,9 +18,11 @@ using Bpl = Microsoft.Boogie; namespace BytecodeTranslator {
public abstract class TraverserFactory {
- public virtual MetadataTraverser MakeMetadataTraverser(Sink sink, IContractProvider contractProvider, PdbReader/*?*/ pdbReader)
+ public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,
+ IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
+ IDictionary<IUnit, PdbReader> sourceLocationProviders)
{
- return new MetadataTraverser(sink, pdbReader);
+ return new MetadataTraverser(sink, sourceLocationProviders);
}
public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
return new StatementTraverser(sink, pdbReader, contractContext);
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs index 92154020..dd00768b 100644 --- a/BCT/BytecodeTranslator/WholeProgram.cs +++ b/BCT/BytecodeTranslator/WholeProgram.cs @@ -16,8 +16,7 @@ namespace BytecodeTranslator { class WholeProgram : TraverserFactory {
/// <summary>
- /// Table to be filled by the metadata traverser when it first gets to an assembly.
- /// [TODO: It should be full set of assemblies that are being translated (CUA).]
+ /// Table to be filled by the metadata traverser before visiting any assemblies.
///
/// The table lists the direct supertypes of all type definitions that it encounters during the
/// traversal. (But the table is organized so that subTypes[T] is the list of type definitions
@@ -25,8 +24,10 @@ namespace BytecodeTranslator { /// </summary>
readonly public Dictionary<ITypeReference, List<ITypeReference>> subTypes = new Dictionary<ITypeReference, List<ITypeReference>>();
- public override MetadataTraverser MakeMetadataTraverser(Sink sink, IContractProvider contractProvider, PdbReader pdbReader) {
- return new WholeProgramMetadataSemantics(this, sink, pdbReader);
+ public override MetadataTraverser MakeMetadataTraverser(Sink sink,
+ IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
+ IDictionary<IUnit, PdbReader> pdbReaders) {
+ return new WholeProgramMetadataSemantics(this, sink, pdbReaders);
}
public class WholeProgramMetadataSemantics : MetadataTraverser {
@@ -34,27 +35,23 @@ namespace BytecodeTranslator { readonly WholeProgram parent;
readonly Sink sink;
- /// <summary>
- /// TODO: Need to have this populated before any of the assemblies in the CUA are traversed.
- /// </summary>
- readonly Dictionary<IAssembly, bool> codeUnderAnalysis = new Dictionary<IAssembly, bool>();
+ readonly Dictionary<IUnit, bool> codeUnderAnalysis = new Dictionary<IUnit, bool>();
- public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, PdbReader/*?*/ pdbReader)
- : base(sink, pdbReader) {
+ public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)
+ : base(sink, pdbReaders) {
this.parent = parent;
this.sink = sink;
}
- public override void Visit(IAssembly assembly) {
-
- #region When doing whole-program analysis, traverse the assembly gathering type information
- this.codeUnderAnalysis.Add(assembly, true);
+ public override void TranslateAssemblies(IEnumerable<IUnit> assemblies) {
+ #region traverse all of the units gathering type information
var typeRecorder = new RecordSubtypes(this.parent.subTypes);
- typeRecorder.Visit(assembly);
+ foreach (var a in assemblies) {
+ this.codeUnderAnalysis.Add(a, true);
+ typeRecorder.Visit(a);
+ }
#endregion
-
- base.Visit(assembly);
-
+ base.TranslateAssemblies(assemblies);
}
class RecordSubtypes : BaseMetadataTraverser {
@@ -120,54 +117,18 @@ namespace BytecodeTranslator { return;
}
- #region Translate In Parameters
-
- var inexpr = new List<Bpl.Expr>();
- #region Create the 'this' argument for the function call
- this.Visit(methodCall.ThisArgument);
- inexpr.Add(this.TranslatedExpressions.Pop());
- #endregion
-
- Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();
- IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
- penum.MoveNext();
- foreach (IExpression exp in methodCall.Arguments) {
- if (penum.Current == null) {
- throw new TranslationException("More Arguments than Parameters in functioncall");
- }
- this.Visit(exp);
- Bpl.Expr e = this.TranslatedExpressions.Pop();
-
- p2eMap.Add(penum.Current, e);
- if (!penum.Current.IsOut) {
- inexpr.Add(e);
- }
-
- penum.MoveNext();
- }
- #endregion
-
Bpl.IToken token = methodCall.Token();
- #region Translate Out vars
- var outvars = new List<Bpl.IdentifierExpr>();
+ List<Bpl.Expr> inexpr;
+ List<Bpl.IdentifierExpr> outvars;
+ Bpl.IdentifierExpr thisExpr;
+ List<Bpl.Variable> locals;
+ List<IFieldDefinition> args;
+ Bpl.Expr arrayExpr;
+ Bpl.Expr indexExpr;
+ Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;
+ var proc = TranslateArgumentsAndReturnProcedure(token, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out locals, out args, out arrayExpr, out indexExpr, out toBoxed);
- foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {
- if (kvp.Key.IsByReference) {
- Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;
- if (iexp == null) {
- throw new TranslationException("Trying to pass complex expression as out in functioncall");
- }
- outvars.Add(iexp);
- }
- }
- #endregion
-
- if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
- Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);
- outvars.Add(new Bpl.IdentifierExpr(token, v));
- TranslatedExpressions.Push(new Bpl.IdentifierExpr(token, v));
- }
Bpl.QKeyValue attrib = null;
foreach (var a in resolvedMethod.Attributes) {
@@ -179,7 +140,6 @@ namespace BytecodeTranslator { var elseBranch = new Bpl.StmtListBuilder();
- var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
var methodname = proc.Name;
Bpl.CallCmd call;
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 98d25303..295349c9 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -5,19 +5,16 @@ type Struct = [Field]Box; type HeapType = [Ref,Field]Box;
-function IsGoodHeap(HeapType) : bool;
-
var $Alloc: [Ref]bool;
procedure {:inline 1} Alloc() returns (x: Ref);
modifies $Alloc;
- free ensures x != null;
implementation Alloc() returns (x: Ref)
{
- assume $Alloc[x] == false;
+ assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
}
@@ -29,10 +26,87 @@ axiom Box2Int($DefaultBox) == 0; axiom Box2Bool($DefaultBox) == false;
+axiom Box2Ref($DefaultBox) == null;
+
+axiom Box2Struct($DefaultBox) == $DefaultStruct;
+
axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);
axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);
+axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x);
+
+axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x);
+
+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref);
+
+
+
+implementation System.Object.GetType(this: Ref) returns ($result: Ref)
+{
+ $result := $TypeOf($DynamicType(this));
+}
+
+
+
+function $TypeOfInv(Ref) : Type;
+
+axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t);
+
+function $ThreadDelegate(Ref) : Ref;
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref);
+
+
+
+implementation System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+
+
+
+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref);
+
+
+
+implementation System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+{
+ call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
+}
+
+
+
+procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
+
+
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref);
+
+
+
+implementation System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+
+
+
+procedure {:inline 1} System.Threading.Thread.Start(this: Ref);
+
+
+
+implementation System.Threading.Thread.Start(this: Ref)
+{
+ call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
+}
+
+
+
+procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
+
+
+
procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref);
@@ -190,7 +264,7 @@ implementation DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref) -var $Heap: HeapType where IsGoodHeap($Heap);
+var $Heap: HeapType;
function {:inline true} Read(H: HeapType, o: Ref, f: Field) : Box
{
@@ -204,7 +278,7 @@ function {:inline true} Write(H: HeapType, o: Ref, f: Field, v: Box) : HeapType var $ArrayContents: [Ref][int]Box;
-var $ArrayLength: [Ref]int;
+function $ArrayLength(Ref) : int;
type Field;
@@ -220,6 +294,8 @@ type Type; const unique $DefaultStruct: Struct;
+type Real;
+
function Box2Int(Box) : int;
function Box2Bool(Box) : bool;
@@ -228,6 +304,8 @@ function Box2Struct(Box) : Struct; function Box2Ref(Box) : Ref;
+function Box2Real(Box) : Real;
+
function Int2Box(int) : Box;
function Bool2Box(bool) : Box;
@@ -236,12 +314,23 @@ function Struct2Box(Struct) : Box; function Ref2Box(Ref) : Box;
+function Real2Box(Real) : Box;
+
+function {:inline true} Box2Box(b: Box) : Box
+{
+ b
+}
+
function Struct2Ref(Struct) : Ref;
function Int2Ref(int) : Ref;
function Bool2Ref(bool) : Ref;
+function Int2Real(int, Type, Type) : Real;
+
+function Real2Int(Real, Type, Type) : Real;
+
function $DynamicType(Ref) : Type;
function $TypeOf(Type) : Ref;
@@ -256,6 +345,129 @@ var $Method: [Ref][Ref]int; var $Receiver: [Ref][Ref]Ref;
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref)
+{
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
+ $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref);
+
+
+
+procedure {:extern} System.Object.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref)
+{
+ $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
+ $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0));
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+{
+}
+
+
+
+const unique RegressionTestInput.CreateStruct: Type;
+
+procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box);
+
+
+
+const unique RegressionTestInput.S.x: Field;
+
+const unique RegressionTestInput.S.b: Field;
+
+implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box)
+{
+ var local_0: [Field]Box;
+ var _loc0: int;
+ var _loc1: bool;
+
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
+ local_0 := $DefaultStruct;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
+ _loc0 := local_0;
+ assert Box2Int(_loc0[RegressionTestInput.S.x]) == 0;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
+ _loc1 := local_0;
+ assert !Box2Bool(_loc1[RegressionTestInput.S.b]);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
+ $result := local_0;
+ return;
+}
+
+
+
+procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box);
+
+
+
+implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box)
+{
+ var s: [Field]Box;
+ var _loc0: int;
+
+ s := s$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
+ s := s[RegressionTestInput.S.x := Int2Box(3)];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
+ _loc0 := s;
+ assert Box2Int(_loc0[RegressionTestInput.S.x]) == 3;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
+ $result := s;
+ return;
+}
+
+
+
+procedure RegressionTestInput.CreateStruct.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.CreateStruct.#ctor(this: Ref)
+{
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.CreateStruct.#cctor();
+
+
+
+implementation RegressionTestInput.CreateStruct.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.ClassWithArrayTypes: Type;
var RegressionTestInput.ClassWithArrayTypes.s: Ref;
@@ -278,28 +490,30 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() var $tmp5: int;
var $tmp6: int;
- assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
call $tmp0 := Alloc();
+ assume $ArrayLength($tmp0) == 1 * 5;
local_0 := $tmp0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
$tmp1 := Box2Int($ArrayContents[local_0][0]);
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(2)]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 88} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
$tmp2 := Box2Int($ArrayContents[local_0][0]);
assert $tmp2 == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
call $tmp3 := Alloc();
+ assume $ArrayLength($tmp3) == 1 * 4;
local_1 := $tmp3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
$tmp4 := Box2Int($ArrayContents[local_1][0]);
$ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := Int2Box(1)]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
$tmp5 := Box2Int($ArrayContents[local_1][0]);
assert $tmp5 == 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 94} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
$tmp6 := Box2Int($ArrayContents[local_0][0]);
assert $tmp6 == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
return;
}
@@ -320,28 +534,30 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() var $tmp12: int;
var $tmp13: int;
- assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
call $tmp7 := Alloc();
+ assume $ArrayLength($tmp7) == 1 * 5;
RegressionTestInput.ClassWithArrayTypes.s := $tmp7;
- assert {:sourceFile "Class1.cs"} {:sourceLine 101} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
$tmp8 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);
$ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 102} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
$tmp9 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);
assert $tmp9 == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
call $tmp10 := Alloc();
+ assume $ArrayLength($tmp10) == 1 * 4;
local_0 := $tmp10;
- assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
$tmp11 := Box2Int($ArrayContents[local_0][0]);
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(1)]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
$tmp12 := Box2Int($ArrayContents[local_0][0]);
assert $tmp12 == 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 108} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
$tmp13 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);
assert $tmp13 == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
return;
}
@@ -354,35 +570,23 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: Ref, implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: Ref, x$in: int)
{
var x: int;
- var _loc0: Ref;
- var $tmp14: Ref;
+ var $tmp14: int;
var $tmp15: int;
- var _loc1: Ref;
- var $tmp16: Ref;
+ var $tmp16: int;
var $tmp17: int;
- var $tmp18: Ref;
- var $tmp19: int;
- var $tmp20: Ref;
- var $tmp21: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 114} true;
- $tmp14 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));
- _loc0 := $tmp14;
- $tmp15 := Box2Int($ArrayContents[_loc0][x]);
- $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][x := Int2Box(42)]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 115} true;
- $tmp16 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));
- _loc1 := $tmp16;
- $tmp17 := Box2Int($ArrayContents[_loc1][x + 1]);
- $ArrayContents := $ArrayContents[_loc1 := $ArrayContents[_loc1][x + 1 := Int2Box(43)]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 116} true;
- $tmp18 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));
- $tmp19 := Box2Int($ArrayContents[$tmp18][x + 1]);
- $tmp20 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));
- $tmp21 := Box2Int($ArrayContents[$tmp20][x]);
- assert $tmp19 == $tmp21 + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 117} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
+ $tmp14 := Box2Int($ArrayContents[this][x]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][x := Int2Box(42)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
+ $tmp15 := Box2Int($ArrayContents[this][x + 1]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][x + 1 := Int2Box(43)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
+ $tmp16 := Box2Int($ArrayContents[Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x + 1]);
+ $tmp17 := Box2Int($ArrayContents[Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x]);
+ assert $tmp16 == $tmp17 + 1;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
return;
}
@@ -395,26 +599,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: Ref, xs$in: Ref)
{
var xs: Ref;
- var $tmp22: int;
- var _loc0: Ref;
- var $tmp23: Ref;
- var $tmp24: int;
+ var $tmp18: int;
+ var $tmp19: int;
xs := xs$in;
- if (!(if xs != null then $ArrayLength[xs] <= 0 else true))
+ if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
{
- assert {:sourceFile "Class1.cs"} {:sourceLine 121} true;
- $tmp22 := Box2Int($ArrayContents[xs][0]);
- $tmp23 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));
- _loc0 := $tmp23;
- $tmp24 := Box2Int($ArrayContents[_loc0][0]);
- $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][0 := Int2Box($tmp22)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ $tmp18 := Box2Int($ArrayContents[xs][0]);
+ $tmp19 := Box2Int($ArrayContents[this][0]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][0 := Int2Box($tmp18)]];
}
else
{
}
- assert {:sourceFile "Class1.cs"} {:sourceLine 123} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 123} true;
return;
}
@@ -424,10 +624,6 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref); -procedure System.Object.#ctor(this: Ref);
-
-
-
implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref)
{
$Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null));
@@ -448,6 +644,34 @@ implementation RegressionTestInput.ClassWithArrayTypes.#cctor() +const unique RegressionTestInput.AsyncAttribute: Type;
+
+procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);
+
+
+
+procedure {:extern} System.Attribute.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#ctor(this: Ref)
+{
+ call System.Attribute.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.AsyncAttribute.#cctor();
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.RefParameters: Type;
procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);
@@ -457,9 +681,9 @@ procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns ( implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)
{
x$out := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 156} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;
x$out := x$out + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 157} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 157} true;
return;
}
@@ -487,6 +711,8 @@ implementation RegressionTestInput.RefParameters.#cctor() +const unique RegressionTestInput.S: Type;
+
const unique RegressionTestInput.Class0: Type;
var RegressionTestInput.Class0.StaticInt: int;
@@ -500,7 +726,7 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r var x: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 18} true;
$result := x + 1;
return;
}
@@ -515,22 +741,22 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: Ref, x$in: int) {
var x: int;
var __temp_1: int;
- var $tmp25: int;
+ var $tmp20: int;
var local_0: int;
x := x$in;
- $tmp25 := x;
- assert $tmp25 != 0;
- __temp_1 := 5 / $tmp25;
+ $tmp20 := x;
+ assert $tmp20 != 0;
+ __temp_1 := 5 / $tmp20;
x := 3;
local_0 := __temp_1 + 3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
assert (if x == 3 then local_0 <= 8 else false);
- assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
RegressionTestInput.Class0.StaticInt := local_0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
assert local_0 == RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
return;
}
@@ -547,7 +773,7 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: Ref, x := x$in;
y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 28} true;
return;
}
@@ -562,7 +788,7 @@ implementation RegressionTestInput.Class0.M$System.Boolean(this: Ref, b$in: bool var b: bool;
b := b$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 29} true;
return;
}
@@ -577,7 +803,7 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref var c: Ref;
c := c$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 30} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 30} true;
return;
}
@@ -589,25 +815,26 @@ procedure RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int); implementation RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int)
{
- var $tmp26: int;
+ var $tmp21: int;
- assert {:sourceFile "Class1.cs"} {:sourceLine 34} true;
- call $tmp26 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
- $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp26;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
+ call $tmp21 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
+ $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp21;
return;
}
-procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref, x$in: int) returns (x$out: int, $result: int)
{
- assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
+ x$out := x$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
$result := x$out;
return;
}
@@ -621,11 +848,11 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, x$in: int implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, x$in: int) returns (x$out: int, $result: int)
{
x$out := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 42} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
x$out := x$out + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
RegressionTestInput.Class0.StaticInt := x$out;
- assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
$result := x$out;
return;
}
@@ -641,11 +868,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: Ref var x: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
x := x + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
RegressionTestInput.Class0.StaticInt := x;
- assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
$result := x;
return;
}
@@ -661,7 +888,7 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho var x: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 56} true;
$result := x;
return;
}
@@ -675,12 +902,12 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$i implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$in: int) returns ($result: int)
{
var y: int;
- var $tmp27: int;
+ var $tmp22: int;
y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp27 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
- $result := $tmp27;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
+ call {:async} $tmp22 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp22;
return;
}
@@ -709,53 +936,6 @@ implementation RegressionTestInput.Class0.#cctor() -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref)
-{
- var $tmp28: int;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
- $tmp28 := Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x));
- $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box($tmp28));
- assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref)
-{
- $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
- $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0));
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
-{
-}
-
-
-
const unique RegressionTestInput.ClassWithBoolTypes: Type;
var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
@@ -773,7 +953,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 x := x$in;
y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 70} true;
$result := x < y;
return;
}
@@ -790,14 +970,14 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: z := z$in;
$Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false));
- assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
call System.Object.#ctor(this);
- assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
$Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
if (z)
{
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
RegressionTestInput.ClassWithBoolTypes.staticB := z;
}
else
@@ -815,11 +995,11 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main(); implementation RegressionTestInput.ClassWithBoolTypes.Main()
{
- var $tmp29: bool;
+ var $tmp23: bool;
- assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;
- call $tmp29 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
- assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
+ call $tmp23 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
return;
}
@@ -835,108 +1015,3 @@ implementation RegressionTestInput.ClassWithBoolTypes.#cctor() }
-
-const unique RegressionTestInput.S: Type;
-
-const unique RegressionTestInput.S.x: Field;
-
-const unique RegressionTestInput.S.b: Field;
-
-const unique RegressionTestInput.AsyncAttribute: Type;
-
-procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);
-
-
-
-procedure System.Attribute.#ctor(this: Ref);
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#ctor(this: Ref)
-{
- call System.Attribute.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.AsyncAttribute.#cctor();
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.CreateStruct: Type;
-
-procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box);
-
-
-
-implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box)
-{
- var local_0: [Field]Box;
- var $tmp30: int;
- var $tmp31: bool;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 141} true;
- local_0 := $DefaultStruct;
- assert {:sourceFile "Class1.cs"} {:sourceLine 142} true;
- $tmp30 := Box2Int(local_0[RegressionTestInput.S.x]);
- assert $tmp30 == 0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 143} true;
- $tmp31 := Box2Bool(local_0[RegressionTestInput.S.b]);
- assert !$tmp31;
- assert {:sourceFile "Class1.cs"} {:sourceLine 145} true;
- $result := local_0;
- return;
-}
-
-
-
-procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box);
-
-
-
-implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box)
-{
- var s: [Field]Box;
- var $tmp32: int;
-
- s := s$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 147} true;
- s := s[RegressionTestInput.S.x := Int2Box(3)];
- assert {:sourceFile "Class1.cs"} {:sourceLine 148} true;
- $tmp32 := Box2Int(s[RegressionTestInput.S.x]);
- assert $tmp32 == 3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 150} true;
- $result := s;
- return;
-}
-
-
-
-procedure RegressionTestInput.CreateStruct.#ctor(this: Ref);
-
-
-
-implementation RegressionTestInput.CreateStruct.#ctor(this: Ref)
-{
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.CreateStruct.#cctor();
-
-
-
-implementation RegressionTestInput.CreateStruct.#cctor()
-{
-}
-
-
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 6e450f38..a0ba97d5 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -5,21 +5,18 @@ type Struct = [Field]Box; type HeapType = [Ref,Field]Box;
-var $Heap: HeapType where IsGoodHeap($Heap);
-
-function IsGoodHeap(HeapType) : bool;
+var $Heap: HeapType;
var $Alloc: [Ref]bool;
procedure {:inline 1} Alloc() returns (x: Ref);
modifies $Alloc;
- free ensures x != null;
implementation Alloc() returns (x: Ref)
{
- assume $Alloc[x] == false;
+ assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
}
@@ -31,10 +28,87 @@ axiom Box2Int($DefaultBox) == 0; axiom Box2Bool($DefaultBox) == false;
+axiom Box2Ref($DefaultBox) == null;
+
+axiom Box2Struct($DefaultBox) == $DefaultStruct;
+
axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);
axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);
+axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x);
+
+axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x);
+
+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref);
+
+
+
+implementation System.Object.GetType(this: Ref) returns ($result: Ref)
+{
+ $result := $TypeOf($DynamicType(this));
+}
+
+
+
+function $TypeOfInv(Ref) : Type;
+
+axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t);
+
+function $ThreadDelegate(Ref) : Ref;
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref);
+
+
+
+implementation System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+
+
+
+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref);
+
+
+
+implementation System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+{
+ call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
+}
+
+
+
+procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
+
+
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref);
+
+
+
+implementation System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+
+
+
+procedure {:inline 1} System.Threading.Thread.Start(this: Ref);
+
+
+
+implementation System.Threading.Thread.Start(this: Ref)
+{
+ call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
+}
+
+
+
+procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
+
+
+
procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref);
@@ -194,7 +268,7 @@ implementation DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref) var $ArrayContents: [Ref][int]Box;
-var $ArrayLength: [Ref]int;
+function $ArrayLength(Ref) : int;
type Field;
@@ -210,6 +284,8 @@ type Type; const unique $DefaultStruct: Struct;
+type Real;
+
function Box2Int(Box) : int;
function Box2Bool(Box) : bool;
@@ -218,6 +294,8 @@ function Box2Struct(Box) : Struct; function Box2Ref(Box) : Ref;
+function Box2Real(Box) : Real;
+
function Int2Box(int) : Box;
function Bool2Box(bool) : Box;
@@ -226,12 +304,23 @@ function Struct2Box(Struct) : Box; function Ref2Box(Ref) : Box;
+function Real2Box(Real) : Box;
+
+function {:inline true} Box2Box(b: Box) : Box
+{
+ b
+}
+
function Struct2Ref(Struct) : Ref;
function Int2Ref(int) : Ref;
function Bool2Ref(bool) : Ref;
+function Int2Real(int, Type, Type) : Real;
+
+function Real2Int(Real, Type, Type) : Real;
+
function $DynamicType(Ref) : Type;
function $TypeOf(Type) : Ref;
@@ -246,6 +335,129 @@ var $Method: [Ref][Ref]int; var $Receiver: [Ref][Ref]Ref;
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
+
+var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int;
+
+var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [Ref]int;
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref)
+{
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
+ RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref);
+
+
+
+procedure {:extern} System.Object.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref)
+{
+ RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this] := 0;
+ RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := 0;
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+{
+}
+
+
+
+const unique RegressionTestInput.CreateStruct: Type;
+
+procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box);
+
+
+
+var RegressionTestInput.S.x: [Ref]int;
+
+var RegressionTestInput.S.b: [Ref]bool;
+
+implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box)
+{
+ var local_0: [Field]Box;
+ var _loc0: int;
+ var _loc1: bool;
+
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
+ local_0 := $DefaultStruct;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
+ _loc0 := local_0;
+ assert Box2Int(_loc0[RegressionTestInput.S.x]) == 0;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
+ _loc1 := local_0;
+ assert !Box2Bool(_loc1[RegressionTestInput.S.b]);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
+ $result := local_0;
+ return;
+}
+
+
+
+procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box);
+
+
+
+implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box)
+{
+ var s: [Field]Box;
+ var _loc0: int;
+
+ s := s$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
+ s[RegressionTestInput.S.x] := Int2Box(3);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
+ _loc0 := s;
+ assert Box2Int(_loc0[RegressionTestInput.S.x]) == 3;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
+ $result := s;
+ return;
+}
+
+
+
+procedure RegressionTestInput.CreateStruct.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.CreateStruct.#ctor(this: Ref)
+{
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.CreateStruct.#cctor();
+
+
+
+implementation RegressionTestInput.CreateStruct.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.ClassWithArrayTypes: Type;
var RegressionTestInput.ClassWithArrayTypes.s: Ref;
@@ -268,28 +480,30 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() var $tmp5: int;
var $tmp6: int;
- assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
call $tmp0 := Alloc();
+ assume $ArrayLength($tmp0) == 1 * 5;
local_0 := $tmp0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;
- $tmp1 := $ArrayContents[local_0][0];
- $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 88} true;
- $tmp2 := $ArrayContents[local_0][0];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
+ $tmp1 := Box2Int($ArrayContents[local_0][0]);
+ $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(2)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
+ $tmp2 := Box2Int($ArrayContents[local_0][0]);
assert $tmp2 == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
call $tmp3 := Alloc();
+ assume $ArrayLength($tmp3) == 1 * 4;
local_1 := $tmp3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;
- $tmp4 := $ArrayContents[local_1][0];
- $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;
- $tmp5 := $ArrayContents[local_1][0];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
+ $tmp4 := Box2Int($ArrayContents[local_1][0]);
+ $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := Int2Box(1)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
+ $tmp5 := Box2Int($ArrayContents[local_1][0]);
assert $tmp5 == 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 94} true;
- $tmp6 := $ArrayContents[local_0][0];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
+ $tmp6 := Box2Int($ArrayContents[local_0][0]);
assert $tmp6 == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
return;
}
@@ -310,28 +524,30 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() var $tmp12: int;
var $tmp13: int;
- assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
call $tmp7 := Alloc();
+ assume $ArrayLength($tmp7) == 1 * 5;
RegressionTestInput.ClassWithArrayTypes.s := $tmp7;
- assert {:sourceFile "Class1.cs"} {:sourceLine 101} true;
- $tmp8 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0];
- $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 102} true;
- $tmp9 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
+ $tmp8 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);
+ $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
+ $tmp9 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);
assert $tmp9 == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
call $tmp10 := Alloc();
+ assume $ArrayLength($tmp10) == 1 * 4;
local_0 := $tmp10;
- assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;
- $tmp11 := $ArrayContents[local_0][0];
- $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;
- $tmp12 := $ArrayContents[local_0][0];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
+ $tmp11 := Box2Int($ArrayContents[local_0][0]);
+ $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(1)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
+ $tmp12 := Box2Int($ArrayContents[local_0][0]);
assert $tmp12 == 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 108} true;
- $tmp13 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
+ $tmp13 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);
assert $tmp13 == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
return;
}
@@ -344,35 +560,23 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: Ref, implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: Ref, x$in: int)
{
var x: int;
- var _loc0: Ref;
- var $tmp14: Ref;
+ var $tmp14: int;
var $tmp15: int;
- var _loc1: Ref;
- var $tmp16: Ref;
+ var $tmp16: int;
var $tmp17: int;
- var $tmp18: Ref;
- var $tmp19: int;
- var $tmp20: Ref;
- var $tmp21: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 114} true;
- $tmp14 := RegressionTestInput.ClassWithArrayTypes.a[this];
- _loc0 := $tmp14;
- $tmp15 := $ArrayContents[_loc0][x];
- $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][x := 42]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 115} true;
- $tmp16 := RegressionTestInput.ClassWithArrayTypes.a[this];
- _loc1 := $tmp16;
- $tmp17 := $ArrayContents[_loc1][x + 1];
- $ArrayContents := $ArrayContents[_loc1 := $ArrayContents[_loc1][x + 1 := 43]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 116} true;
- $tmp18 := RegressionTestInput.ClassWithArrayTypes.a[this];
- $tmp19 := $ArrayContents[$tmp18][x + 1];
- $tmp20 := RegressionTestInput.ClassWithArrayTypes.a[this];
- $tmp21 := $ArrayContents[$tmp20][x];
- assert $tmp19 == $tmp21 + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 117} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
+ $tmp14 := Box2Int($ArrayContents[this][x]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][x := Int2Box(42)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
+ $tmp15 := Box2Int($ArrayContents[this][x + 1]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][x + 1 := Int2Box(43)]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
+ $tmp16 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x + 1]);
+ $tmp17 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x]);
+ assert $tmp16 == $tmp17 + 1;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
return;
}
@@ -385,26 +589,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: Ref, xs$in: Ref)
{
var xs: Ref;
- var $tmp22: int;
- var _loc0: Ref;
- var $tmp23: Ref;
- var $tmp24: int;
+ var $tmp18: int;
+ var $tmp19: int;
xs := xs$in;
- if (!(if xs != null then $ArrayLength[xs] <= 0 else true))
+ if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
{
- assert {:sourceFile "Class1.cs"} {:sourceLine 121} true;
- $tmp22 := $ArrayContents[xs][0];
- $tmp23 := RegressionTestInput.ClassWithArrayTypes.a[this];
- _loc0 := $tmp23;
- $tmp24 := $ArrayContents[_loc0][0];
- $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][0 := $tmp22]];
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+ $tmp18 := Box2Int($ArrayContents[xs][0]);
+ $tmp19 := Box2Int($ArrayContents[this][0]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][0 := Int2Box($tmp18)]];
}
else
{
}
- assert {:sourceFile "Class1.cs"} {:sourceLine 123} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 123} true;
return;
}
@@ -414,10 +614,6 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref); -procedure System.Object.#ctor(this: Ref);
-
-
-
implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref)
{
RegressionTestInput.ClassWithArrayTypes.a[this] := null;
@@ -438,6 +634,34 @@ implementation RegressionTestInput.ClassWithArrayTypes.#cctor() +const unique RegressionTestInput.AsyncAttribute: Type;
+
+procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);
+
+
+
+procedure {:extern} System.Attribute.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#ctor(this: Ref)
+{
+ call System.Attribute.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.AsyncAttribute.#cctor();
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.RefParameters: Type;
procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);
@@ -447,9 +671,9 @@ procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns ( implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)
{
x$out := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 156} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;
x$out := x$out + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 157} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 157} true;
return;
}
@@ -477,6 +701,8 @@ implementation RegressionTestInput.RefParameters.#cctor() +const unique RegressionTestInput.S: Type;
+
const unique RegressionTestInput.Class0: Type;
var RegressionTestInput.Class0.StaticInt: int;
@@ -490,7 +716,7 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r var x: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 18} true;
$result := x + 1;
return;
}
@@ -505,22 +731,22 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: Ref, x$in: int) {
var x: int;
var __temp_1: int;
- var $tmp25: int;
+ var $tmp20: int;
var local_0: int;
x := x$in;
- $tmp25 := x;
- assert $tmp25 != 0;
- __temp_1 := 5 / $tmp25;
+ $tmp20 := x;
+ assert $tmp20 != 0;
+ __temp_1 := 5 / $tmp20;
x := 3;
local_0 := __temp_1 + 3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
assert (if x == 3 then local_0 <= 8 else false);
- assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
RegressionTestInput.Class0.StaticInt := local_0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
assert local_0 == RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
return;
}
@@ -537,7 +763,7 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: Ref, x := x$in;
y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 28} true;
return;
}
@@ -552,7 +778,7 @@ implementation RegressionTestInput.Class0.M$System.Boolean(this: Ref, b$in: bool var b: bool;
b := b$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 29} true;
return;
}
@@ -567,7 +793,7 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref var c: Ref;
c := c$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 30} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 30} true;
return;
}
@@ -579,25 +805,26 @@ procedure RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int); implementation RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int)
{
- var $tmp26: int;
+ var $tmp21: int;
- assert {:sourceFile "Class1.cs"} {:sourceLine 34} true;
- call $tmp26 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
- $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp26;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
+ call $tmp21 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
+ $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp21;
return;
}
-procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref, x$in: int) returns (x$out: int, $result: int)
{
- assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
+ x$out := x$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
$result := x$out;
return;
}
@@ -611,11 +838,11 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, x$in: int implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, x$in: int) returns (x$out: int, $result: int)
{
x$out := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 42} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
x$out := x$out + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
RegressionTestInput.Class0.StaticInt := x$out;
- assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
$result := x$out;
return;
}
@@ -631,11 +858,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: Ref var x: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
x := x + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
RegressionTestInput.Class0.StaticInt := x;
- assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
$result := x;
return;
}
@@ -651,7 +878,7 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho var x: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 56} true;
$result := x;
return;
}
@@ -665,12 +892,12 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$i implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$in: int) returns ($result: int)
{
var y: int;
- var $tmp27: int;
+ var $tmp22: int;
y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp27 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
- $result := $tmp27;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
+ call {:async} $tmp22 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp22;
return;
}
@@ -699,53 +926,6 @@ implementation RegressionTestInput.Class0.#cctor() -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
-
-var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int;
-
-var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [Ref]int;
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref)
-{
- var $tmp28: int;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
- $tmp28 := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this];
- RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := $tmp28;
- assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref)
-{
- RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this] := 0;
- RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := 0;
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
-{
-}
-
-
-
const unique RegressionTestInput.ClassWithBoolTypes: Type;
var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
@@ -763,7 +943,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 x := x$in;
y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 70} true;
$result := x < y;
return;
}
@@ -780,14 +960,14 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: z := z$in;
RegressionTestInput.ClassWithBoolTypes.b[this] := false;
- assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
call System.Object.#ctor(this);
- assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
RegressionTestInput.ClassWithBoolTypes.b[this] := z;
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
if (z)
{
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
RegressionTestInput.ClassWithBoolTypes.staticB := z;
}
else
@@ -805,11 +985,11 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main(); implementation RegressionTestInput.ClassWithBoolTypes.Main()
{
- var $tmp29: bool;
+ var $tmp23: bool;
- assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;
- call $tmp29 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
- assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
+ call $tmp23 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
return;
}
@@ -825,108 +1005,3 @@ implementation RegressionTestInput.ClassWithBoolTypes.#cctor() }
-
-const unique RegressionTestInput.S: Type;
-
-var RegressionTestInput.S.x: [Ref]int;
-
-var RegressionTestInput.S.b: [Ref]bool;
-
-const unique RegressionTestInput.AsyncAttribute: Type;
-
-procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);
-
-
-
-procedure System.Attribute.#ctor(this: Ref);
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#ctor(this: Ref)
-{
- call System.Attribute.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.AsyncAttribute.#cctor();
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.CreateStruct: Type;
-
-procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box);
-
-
-
-implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box)
-{
- var local_0: [Field]Box;
- var $tmp30: int;
- var $tmp31: bool;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 141} true;
- local_0 := $DefaultStruct;
- assert {:sourceFile "Class1.cs"} {:sourceLine 142} true;
- $tmp30 := local_0[RegressionTestInput.S.x];
- assert $tmp30 == 0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 143} true;
- $tmp31 := local_0[RegressionTestInput.S.b];
- assert !$tmp31;
- assert {:sourceFile "Class1.cs"} {:sourceLine 145} true;
- $result := local_0;
- return;
-}
-
-
-
-procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box);
-
-
-
-implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box)
-{
- var s: [Field]Box;
- var $tmp32: int;
-
- s := s$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 147} true;
- s[RegressionTestInput.S.x] := 3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 148} true;
- $tmp32 := s[RegressionTestInput.S.x];
- assert $tmp32 == 3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 150} true;
- $result := s;
- return;
-}
-
-
-
-procedure RegressionTestInput.CreateStruct.#ctor(this: Ref);
-
-
-
-implementation RegressionTestInput.CreateStruct.#ctor(this: Ref)
-{
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.CreateStruct.#cctor();
-
-
-
-implementation RegressionTestInput.CreateStruct.#cctor()
-{
-}
-
-
|