diff options
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 27 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 80 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 26 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 4 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 2 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 2 |
7 files changed, 89 insertions, 54 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 4456c860..0925bc7c 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -350,7 +350,8 @@ namespace BytecodeTranslator var typ = defaultValue.Type;
- if (typ.IsValueType && typ.TypeCode == PrimitiveTypeCode.NotPrimitive) {
+ #region Struct
+ if (TranslationHelper.IsStruct(typ)) {
// then it is a struct and gets special treatment
// translate it as if it were a call to the nullary ctor for the struct type
// (which doesn't actually exist, but gets generated for each struct type
@@ -383,8 +384,28 @@ namespace BytecodeTranslator this.TranslatedExpressions.Push(locExpr);
return;
}
+ #endregion
- TranslatedExpressions.Push(this.sink.DefaultValue(typ));
+ Bpl.Expr e;
+ var bplType = this.sink.CciTypeToBoogie(typ);
+ if (bplType == Bpl.Type.Int) {
+ var lit = Bpl.Expr.Literal(0);
+ lit.Type = Bpl.Type.Int;
+ e = lit;
+ } else if (bplType == Bpl.Type.Bool) {
+ var lit = Bpl.Expr.False;
+ lit.Type = Bpl.Type.Bool;
+ e = lit;
+ } else if (bplType == this.sink.Heap.RefType) {
+ e = Bpl.Expr.Ident(this.sink.Heap.NullRef);
+ } else if (bplType == this.sink.Heap.BoxType) {
+ e = Bpl.Expr.Ident(this.sink.Heap.DefaultBox);
+ } else {
+ throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(typ)));
+ }
+
+ TranslatedExpressions.Push(e);
+ return;
}
#endregion
@@ -614,7 +635,7 @@ namespace BytecodeTranslator Contract.Assert(TranslatedExpressions.Count == 0);
var typ = source.Type;
- var structCopy = typ.IsValueType && typ.TypeCode == PrimitiveTypeCode.NotPrimitive && !(source is IDefaultValue);
+ var structCopy = TranslationHelper.IsStruct(typ) && !(source is IDefaultValue);
// then a struct value of type S is being assigned: "lhs := s"
// model this as the statement "call lhs := S..#copy_ctor(s)" that does the bit-wise copying
Bpl.DeclWithFormals proc = null;
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 5c78298b..2458d27c 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -104,29 +104,47 @@ namespace BytecodeTranslator { var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typeDefinition);
- var stmtBuilder = new Bpl.StmtListBuilder();
+ this.sink.BeginMethod();
+ var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
+ var stmts = new List<IStatement>();
foreach (var f in typeDefinition.Fields) {
- var e = this.sink.DefaultValue(f.Type);
- var fExp = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f));
- var o = Bpl.Expr.Ident(proc.InParams[0]);
- var boogieType = sink.CciTypeToBoogie(f.Type);
- var c = this.sink.Heap.WriteHeap(Bpl.Token.NoToken, o, fExp, e, AccessType.Struct, boogieType);
- stmtBuilder.Add(c);
+ if (f.IsStatic) continue;
+ var s = new ExpressionStatement() {
+ Expression = new Assignment() {
+ Source = new DefaultValue() { DefaultValueType = f.Type, Type = f.Type, },
+ Target = new TargetExpression() {
+ Definition = f,
+ Instance = new ThisReference() { Type = typeDefinition, },
+ Type = f.Type,
+ },
+ Type = f.Type,
+ },
+ };
}
+ stmtTranslator.Visit(stmts);
+ var translatedStatements = stmtTranslator.StmtBuilder.Collect(Bpl.Token.NoToken);
+
var lit = Bpl.Expr.Literal(1);
lit.Type = Bpl.Type.Int;
var args = new List<object> { lit };
var attrib = new Bpl.QKeyValue(typeDefinition.Token(), "inline", args, null); // TODO: Need to have it be {:inine 1} (and not just {:inline})?
+
+ List<Bpl.Variable> vars = new List<Bpl.Variable>();
+ foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {
+ vars.Add(v);
+ }
+ Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
+
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),
+ vseq,
+ translatedStatements,
attrib,
new Bpl.Errors()
);
@@ -143,6 +161,7 @@ namespace BytecodeTranslator { var stmtBuilder = new Bpl.StmtListBuilder();
foreach (var f in typeDefinition.Fields) {
+ if (f.IsStatic) continue;
var boogieType = sink.CciTypeToBoogie(f.Type);
var fExp = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f));
var e = this.sink.Heap.ReadHeap(Bpl.Expr.Ident(proc.InParams[0]), fExp, AccessType.Struct, boogieType);
@@ -187,32 +206,49 @@ namespace BytecodeTranslator { this.sink.TranslatedProgram.TopLevelDeclarations.Add(proc);
- var stmtBuilder = new Bpl.StmtListBuilder();
+ this.sink.BeginMethod();
+
+ var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
+ var stmts = new List<IStatement>();
+
foreach (var f in typeDefinition.Fields) {
- if (f.IsStatic) {
-
- var e = this.sink.DefaultValue(f.Type);
- stmtBuilder.Add(
- TranslationHelper.BuildAssignCmd(
- Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f)),
- e
- ));
- }
+ if (!f.IsStatic) continue;
+ stmts.Add(
+ new ExpressionStatement() {
+ Expression = new Assignment() {
+ Source = new DefaultValue() { DefaultValueType = f.Type, Type = f.Type, },
+ Target = new TargetExpression() {
+ Definition = f,
+ Instance = null,
+ Type = f.Type,
+ },
+ Type = f.Type,
+ }
+ });
}
+
+ stmtTranslator.Visit(stmts);
+ var translatedStatements = stmtTranslator.StmtBuilder.Collect(Bpl.Token.NoToken);
+
+ List<Bpl.Variable> vars = new List<Bpl.Variable>();
+ foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {
+ vars.Add(v);
+ }
+ Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
+
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)
+ vseq,
+ translatedStatements
);
impl.Proc = proc;
this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
-
}
/// <summary>
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 7e6ddcff..093233cb 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -85,28 +85,6 @@ namespace BytecodeTranslator { public readonly Bpl.Program TranslatedProgram;
- public Bpl.Expr DefaultValue(ITypeReference type) {
- var bplType = CciTypeToBoogie(type);
- if (bplType == Bpl.Type.Int) {
- var lit = Bpl.Expr.Literal(0);
- lit.Type = Bpl.Type.Int;
- return lit;
- } else if (bplType == Bpl.Type.Bool) {
- var lit = Bpl.Expr.False;
- lit.Type = Bpl.Type.Bool;
- return lit;
- } else if (type.ResolvedType.IsStruct) {
- return Bpl.Expr.Ident(this.Heap.DefaultStruct);
- } else if (bplType == this.Heap.RefType) {
- return Bpl.Expr.Ident(this.Heap.NullRef);
- }
- else if (bplType == this.Heap.BoxType) {
- return Bpl.Expr.Ident(this.Heap.DefaultBox);
- } else {
- throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(type)));
- }
- }
-
public Bpl.Type CciTypeToBoogie(ITypeReference type) {
if (TypeHelper.TypesAreEquivalent(type, type.PlatformType.SystemBoolean))
return Bpl.Type.Bool;
@@ -478,11 +456,11 @@ namespace BytecodeTranslator { for (int p1index = 0; p1index < method.ParameterCount; p1index++) {
var p1 = paramList[p1index];
if (p1.IsByReference) continue;
- if (!(p1.Type.IsValueType && p1.Type.TypeCode == PrimitiveTypeCode.NotPrimitive)) continue;
+ if (!TranslationHelper.IsStruct(p1.Type)) continue;
for (int p2index = p1index + 1; p2index < method.ParameterCount; p2index++) {
var p2 = paramList[p2index];
if (p2.IsByReference) continue;
- if (!(p2.Type.IsValueType && p2.Type.TypeCode == PrimitiveTypeCode.NotPrimitive)) continue;
+ if (!TranslationHelper.IsStruct(p2.Type)) continue;
if (!TypeHelper.TypesAreEquivalent(p1.Type, p2.Type)) continue;
var req = new Bpl.Requires(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq,
Bpl.Expr.Ident(formalMap[p1].inParameterCopy), Bpl.Expr.Ident(formalMap[p2].inParameterCopy)));
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index afe6a959..f03894a2 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -183,7 +183,7 @@ namespace BytecodeTranslator var e = ExpressionFor(initVal);
var typ = initVal.Type;
- var structCopy = typ.IsValueType && typ.TypeCode == PrimitiveTypeCode.NotPrimitive && !(initVal is IDefaultValue);
+ var structCopy = TranslationHelper.IsStruct(typ) && !(initVal is IDefaultValue);
// then a struct value of type S is being assigned: "lhs := s"
// model this as the statement "call lhs := S..#copy_ctor(s)" that does the bit-wise copying
Bpl.DeclWithFormals proc = null;
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 54ed1700..fde776f9 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -122,6 +122,10 @@ namespace BytecodeTranslator { return s;
}
+ public static bool IsStruct(ITypeReference typ) {
+ return typ.IsValueType && !typ.IsEnum && typ.TypeCode == PrimitiveTypeCode.NotPrimitive;
+ }
+
#region Temp Stuff that must be replaced as soon as there is real code to deal with this
public static Bpl.Variable TempThisVar() {
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 93f3a127..98583054 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -685,8 +685,6 @@ implementation RegressionTestInput.RefParameters.#cctor() implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)
{
- $Heap := Write($Heap, this, RegressionTestInput.S.x, Int2Box(0));
- $Heap := Write($Heap, this, RegressionTestInput.S.b, Bool2Box(false));
}
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 48d2c942..c292fb90 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -675,8 +675,6 @@ implementation RegressionTestInput.RefParameters.#cctor() implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)
{
- this[RegressionTestInput.S.x] := Int2Box(0);
- this[RegressionTestInput.S.b] := Bool2Box(false);
}
|