diff options
-rw-r--r-- | .hgignore | 2 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 29 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 46 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 34 | ||||
-rw-r--r-- | BCT/RegressionTests/RegressionTestInput/Class1.cs | 12 |
5 files changed, 121 insertions, 2 deletions
@@ -4,7 +4,7 @@ syntax: regexp ^(Source|BCT|Jennisys)/.*\.(user|suo|cache)$
^Source/(Core|Dafny)/(Parser|Scanner).cs.old$
^Binaries/.*\.(dll|pdb|exe|manifest|config)$
-^.*(bin|obj)/([^/]*/)?(Debug|Release)/.*$
+^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked)/.*$
^Binaries/BytecodeTranslator$
^BCT/Binaries/.*$
Test/([^/]*)/Output
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 4e04c104..53e4ccce 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -624,6 +624,35 @@ namespace BytecodeTranslator public override void Visit(IAssignment assignment) {
Contract.Assert(TranslatedExpressions.Count == 0);
+ #region Special case for s := default(S) when S is a struct
+
+ // The C# source "s = new S()" when S is a struct is compiled
+ // into an "initobj" instruction. That is decompiled into the
+ // assignment: "s = DefaultValue(S)".
+ // We translate it as a call to a pseduo-ctor that is created for S:
+ // "s := S.#default_ctor()".
+
+ if (assignment.Target.Type.ResolvedType.IsStruct &&
+ assignment.Target.Type.TypeCode == PrimitiveTypeCode.NotPrimitive &&
+ assignment.Source is IDefaultValue) {
+
+ this.Visit(assignment.Target);
+ var s = this.TranslatedExpressions.Pop();
+
+ var structType = assignment.Target.Type;
+ Bpl.IToken tok = assignment.Token();
+ var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(structType);
+ string methodname = proc.Name;
+ var inexpr = new List<Bpl.Expr>();
+ var outvars = new List<Bpl.IdentifierExpr>();
+ outvars.Add((Bpl.IdentifierExpr)s);
+ var call = new Bpl.CallCmd(tok, methodname, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+
+ return;
+ }
+ #endregion
+
#region Transform Right Hand Side ...
this.Visit(assignment.Source);
Bpl.Expr sourceexp = this.TranslatedExpressions.Pop();
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index bbcc81f5..9482573f 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -73,6 +73,7 @@ namespace BytecodeTranslator { return; // enums just are translated as ints
} else if (typeDefinition.IsStruct) {
sink.FindOrCreateType(typeDefinition);
+ CreateDefaultStructConstructor(typeDefinition);
base.Visit(typeDefinition);
} else {
Console.WriteLine("Unknown kind of type definition '{0}' was found",
@@ -81,6 +82,49 @@ namespace BytecodeTranslator { }
}
+ private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) {
+ Contract.Requires(typeDefinition.IsStruct);
+
+ var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typeDefinition);
+
+ var stmtBuilder = new Bpl.StmtListBuilder();
+
+ foreach (var f in typeDefinition.Fields) {
+ Bpl.Expr e;
+ var bplType = this.sink.CciTypeToBoogie(f.Type);
+ if (bplType == Bpl.Type.Int) {
+ e = Bpl.Expr.Literal(0);
+ e.Type = Bpl.Type.Int;
+ } else if (bplType == Bpl.Type.Bool) {
+ e = Bpl.Expr.False;
+ e.Type = Bpl.Type.Bool;
+ } else {
+ throw new NotImplementedException("Don't know how to translate type");
+ }
+
+ var fExp = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f));
+ var o = Bpl.Expr.Ident(proc.OutParams[0]);
+ var c = this.sink.Heap.WriteHeap(Bpl.Token.NoToken, o, fExp, e, true);
+ stmtBuilder.Add(c);
+ }
+
+ var attrib = new Bpl.QKeyValue(typeDefinition.Token(), "inline", new List<object>(1), null); // TODO: Need to have it be {:inine 1} (and not just {:inline})?
+ Bpl.Implementation impl =
+ new Bpl.Implementation(Bpl.Token.NoToken,
+ proc.Name,
+ new Bpl.TypeVariableSeq(),
+ proc.InParams,
+ proc.OutParams,
+ new Bpl.VariableSeq(),
+ stmtBuilder.Collect(Bpl.Token.NoToken),
+ attrib,
+ new Bpl.Errors()
+ );
+
+ impl.Proc = (Bpl.Procedure) proc; // TODO: get rid of cast
+ this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
+ }
+
private bool sawCctor = false;
private void CreateStaticConstructor(ITypeDefinition typeDefinition) {
@@ -290,7 +334,7 @@ namespace BytecodeTranslator { foreach (var f in method.ContainingTypeDefinition.Fields) {
if (f.IsStatic == method.IsStatic) {
var a = new Assignment() {
- Source = new DefaultValue() { Type = f.Type, },
+ Source = new DefaultValue() { DefaultValueType = f.Type, Type = f.Type, },
Target = new TargetExpression() { Definition = f, Instance = method.IsConstructor ? thisExp : null, Type = f.Type },
Type = f.Type,
};
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 9c20f96a..6e3909ab 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -415,6 +415,40 @@ namespace BytecodeTranslator { return procAndFormalMap.Decl;
}
+ /// <summary>
+ /// Struct "creation" (source code that looks like "new S()" for a struct type S) is modeled
+ /// by a call to the nullary "ctor" that initializes all of the structs fields to zero-
+ /// equivalent values. Note that the generated procedure has no contract. So if the struct
+ /// is defined in an assembly that is not being translated, then its behavior is unspecified.
+ /// </summary>
+ /// <param name="structType">A type reference to the value type for which the ctor should be returned.</param>
+ /// <returns>A nullary procedure that returns an initialized value of type <paramref name="structType"/>.</returns>
+ public Bpl.DeclWithFormals FindOrCreateProcedureForDefaultStructCtor(ITypeReference structType) {
+ Contract.Requires(structType.IsValueType);
+
+ ProcedureInfo procAndFormalMap;
+ var key = structType.InternedKey;
+ if (!this.declaredMethods.TryGetValue(key, out procAndFormalMap)) {
+ var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));
+ var tok = structType.Token();
+ var selfType = new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);
+ var selfOut = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), false);
+ var outvars = new Bpl.Formal[]{ selfOut };
+ var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#default_ctor",
+ new Bpl.TypeVariableSeq(),
+ new Bpl.VariableSeq(), // in
+ new Bpl.VariableSeq(outvars),
+ new Bpl.RequiresSeq(),
+ new Bpl.IdentifierExprSeq(), // modifies
+ new Bpl.EnsuresSeq()
+ );
+ this.TranslatedProgram.TopLevelDeclarations.Add(proc);
+ procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>(), this.RetVariable);
+ this.declaredMethods.Add(key, procAndFormalMap);
+ }
+ return procAndFormalMap.Decl;
+ }
+
// TODO: Fix test to return true iff method is marked with the "real" [Pure] attribute
// also, should it return true for properties and all of the other things the tools
// consider pure?
diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs index f2918aa7..b5fa3582 100644 --- a/BCT/RegressionTests/RegressionTestInput/Class1.cs +++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs @@ -130,4 +130,16 @@ namespace RegressionTestInput { this.y = this.x;
}
}
+
+ public struct S {
+ int x;
+ bool b;
+ }
+
+ public class CreateStruct {
+ public S Create() {
+ return new S();
+ }
+ }
+
}
|