summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-05-16 18:26:45 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-05-16 18:26:45 -0700
commit0d02c233dc44f763911cfe7daeb0cb0c7a2ec624 (patch)
tree983d39575a16d889f791e8c5d1a7e992c8315888
parentc76d588dd2768de8505d3d08f43f3de0b5f84dae (diff)
parent64e7e8a1194e5bb4667253e301720d4aa55a7dd9 (diff)
Merge
Diffstat
-rw-r--r--BCT/BytecodeTranslator/BytecodeTranslator.csproj12
-rw-r--r--BCT/BytecodeTranslator/ExpressionTraverser.cs308
-rw-r--r--BCT/BytecodeTranslator/Heap.cs2
-rw-r--r--BCT/BytecodeTranslator/MetadataTraverser.cs21
-rw-r--r--BCT/BytecodeTranslator/Program.cs65
-rw-r--r--BCT/BytecodeTranslator/Sink.cs35
-rw-r--r--BCT/BytecodeTranslator/StatementTraverser.cs32
-rw-r--r--BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt129
-rw-r--r--BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt129
9 files changed, 524 insertions, 209 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..73a5951a 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);
@@ -604,6 +640,7 @@ namespace BytecodeTranslator
private Bpl.Expr arrayExpr = null;
private Bpl.Expr indexExpr = null;
+#if EXPERIMENTAL
/// <summary>
///
/// </summary>
@@ -612,18 +649,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 +781,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 +852,8 @@ namespace BytecodeTranslator
return;
}
+#endif
+
#endregion
#region Translate Object Creation
@@ -1161,74 +1300,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..f38e0093 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -39,6 +39,7 @@ var $Heap: HeapType;
var $Alloc: [Ref] bool;
procedure {:inline 1} Alloc() returns (x: Ref)
+ free ensures x != null;
modifies $Alloc;
{
assume $Alloc[x] == false && x != null;
@@ -175,6 +176,7 @@ type HeapType = [Ref,Field]Box;
var $Alloc: [Ref] bool;
procedure {:inline 1} Alloc() returns (x: Ref)
+ free ensures x != null;
modifies $Alloc;
{
assume $Alloc[x] == false && x != null;
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 58bec27f..b1be6294 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -46,7 +46,12 @@ namespace BytecodeTranslator {
}
public override void Visit(IAssembly assembly) {
- base.Visit(assembly);
+ this.sink.BeginAssembly(assembly);
+ try {
+ base.Visit(assembly);
+ } finally {
+ this.sink.EndAssembly(assembly);
+ }
}
/// <summary>
@@ -55,6 +60,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 +88,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 +269,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
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index f42c34d9..d04a8783 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);
@@ -132,12 +142,19 @@ 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(Tuple.Create((IModule)mutableModule, pdbReader));
- modules.Add(Tuple.Create(module, pdbReader));
}
}
if (modules.Count == 0) {
@@ -340,6 +357,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..0e13c510 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);
}
}
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 98d25303..5b24fa32 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -5,8 +5,6 @@ type Struct = [Field]Box;
type HeapType = [Ref,Field]Box;
-function IsGoodHeap(HeapType) : bool;
-
var $Alloc: [Ref]bool;
procedure {:inline 1} Alloc() returns (x: Ref);
@@ -17,7 +15,7 @@ procedure {:inline 1} Alloc() returns (x: Ref);
implementation Alloc() returns (x: Ref)
{
- assume $Alloc[x] == false;
+ assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
}
@@ -29,10 +27,18 @@ 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 DelegateAdd(a: Ref, b: Ref) returns (c: Ref);
@@ -190,7 +196,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
{
@@ -220,6 +226,8 @@ type Type;
const unique $DefaultStruct: Struct;
+type Real;
+
function Box2Int(Box) : int;
function Box2Bool(Box) : bool;
@@ -228,6 +236,8 @@ function Box2Struct(Box) : Struct;
function Box2Ref(Box) : Ref;
+function Box2Real(Box) : Real;
+
function Int2Box(int) : Box;
function Bool2Box(bool) : Box;
@@ -236,12 +246,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;
@@ -354,34 +375,22 @@ 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)]];
+ $tmp14 := Box2Int($ArrayContents[this][x]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][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)]];
+ $tmp15 := Box2Int($ArrayContents[this][x + 1]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][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;
+ $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 "Class1.cs"} {:sourceLine 117} true;
return;
}
@@ -395,20 +404,16 @@ 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))
{
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)]];
+ $tmp18 := Box2Int($ArrayContents[xs][0]);
+ $tmp19 := Box2Int($ArrayContents[this][0]);
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][0 := Int2Box($tmp18)]];
}
else
{
@@ -424,7 +429,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref);
-procedure System.Object.#ctor(this: Ref);
+procedure {:extern} System.Object.#ctor(this: Ref);
@@ -515,13 +520,13 @@ 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;
@@ -589,22 +594,23 @@ 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;
+ 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)
{
+ x$out := x$in;
assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
@@ -675,12 +681,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;
+ call {:async} $tmp22 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp22;
return;
}
@@ -721,11 +727,8 @@ 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));
+ $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
return;
}
@@ -815,10 +818,10 @@ 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);
+ call $tmp23 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
return;
}
@@ -848,7 +851,7 @@ procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);
-procedure System.Attribute.#ctor(this: Ref);
+procedure {:extern} System.Attribute.#ctor(this: Ref);
@@ -879,17 +882,17 @@ procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [
implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box)
{
var local_0: [Field]Box;
- var $tmp30: int;
- var $tmp31: bool;
+ var _loc0: int;
+ var _loc1: 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;
+ _loc0 := local_0;
+ assert Box2Int(_loc0[RegressionTestInput.S.x]) == 0;
assert {:sourceFile "Class1.cs"} {:sourceLine 143} true;
- $tmp31 := Box2Bool(local_0[RegressionTestInput.S.b]);
- assert !$tmp31;
+ _loc1 := local_0;
+ assert !Box2Bool(_loc1[RegressionTestInput.S.b]);
assert {:sourceFile "Class1.cs"} {:sourceLine 145} true;
$result := local_0;
return;
@@ -904,14 +907,14 @@ procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInpu
implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box)
{
var s: [Field]Box;
- var $tmp32: int;
+ var _loc0: 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;
+ _loc0 := s;
+ assert Box2Int(_loc0[RegressionTestInput.S.x]) == 3;
assert {:sourceFile "Class1.cs"} {:sourceLine 150} true;
$result := s;
return;
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 6e450f38..163b9153 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -5,9 +5,7 @@ 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;
@@ -19,7 +17,7 @@ procedure {:inline 1} Alloc() returns (x: Ref);
implementation Alloc() returns (x: Ref)
{
- assume $Alloc[x] == false;
+ assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
}
@@ -31,10 +29,18 @@ 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 DelegateAdd(a: Ref, b: Ref) returns (c: Ref);
@@ -210,6 +216,8 @@ type Type;
const unique $DefaultStruct: Struct;
+type Real;
+
function Box2Int(Box) : int;
function Box2Bool(Box) : bool;
@@ -218,6 +226,8 @@ function Box2Struct(Box) : Struct;
function Box2Ref(Box) : Ref;
+function Box2Real(Box) : Real;
+
function Int2Box(int) : Box;
function Bool2Box(bool) : Box;
@@ -226,12 +236,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;
@@ -344,34 +365,22 @@ 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]];
+ $tmp14 := $ArrayContents[this][x];
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][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]];
+ $tmp15 := $ArrayContents[this][x + 1];
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][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;
+ $tmp16 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x + 1];
+ $tmp17 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x];
+ assert $tmp16 == $tmp17 + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 117} true;
return;
}
@@ -385,20 +394,16 @@ 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))
{
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]];
+ $tmp18 := $ArrayContents[xs][0];
+ $tmp19 := $ArrayContents[this][0];
+ $ArrayContents := $ArrayContents[this := $ArrayContents[this][0 := $tmp18]];
}
else
{
@@ -414,7 +419,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref);
-procedure System.Object.#ctor(this: Ref);
+procedure {:extern} System.Object.#ctor(this: Ref);
@@ -505,13 +510,13 @@ 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;
@@ -579,22 +584,23 @@ 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;
+ 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)
{
+ x$out := x$in;
assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
@@ -665,12 +671,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;
+ call {:async} $tmp22 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp22;
return;
}
@@ -711,11 +717,8 @@ 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;
+ RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this];
assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
return;
}
@@ -805,10 +808,10 @@ 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);
+ call $tmp23 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
return;
}
@@ -838,7 +841,7 @@ procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);
-procedure System.Attribute.#ctor(this: Ref);
+procedure {:extern} System.Attribute.#ctor(this: Ref);
@@ -869,17 +872,17 @@ procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [
implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box)
{
var local_0: [Field]Box;
- var $tmp30: int;
- var $tmp31: bool;
+ var _loc0: int;
+ var _loc1: 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;
+ _loc0 := local_0;
+ assert _loc0[RegressionTestInput.S.x] == 0;
assert {:sourceFile "Class1.cs"} {:sourceLine 143} true;
- $tmp31 := local_0[RegressionTestInput.S.b];
- assert !$tmp31;
+ _loc1 := local_0;
+ assert !_loc1[RegressionTestInput.S.b];
assert {:sourceFile "Class1.cs"} {:sourceLine 145} true;
$result := local_0;
return;
@@ -894,14 +897,14 @@ procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInpu
implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box)
{
var s: [Field]Box;
- var $tmp32: int;
+ var _loc0: 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;
+ _loc0 := s;
+ assert _loc0[RegressionTestInput.S.x] == 3;
assert {:sourceFile "Class1.cs"} {:sourceLine 150} true;
$result := s;
return;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 12:47:52 +0000