From 7d06797fc12bea25e294a776c87a53f88bb87031 Mon Sep 17 00:00:00 2001 From: Mike Barnett Date: Sun, 29 May 2011 15:07:01 -0700 Subject: Removed the method DefaultValue from the sink: if a default value of a type is desired, then the CCI nodes must be created and an expression/statement traverser used to translate it. --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 27 +++++++- BCT/BytecodeTranslator/MetadataTraverser.cs | 80 ++++++++++++++++------ BCT/BytecodeTranslator/Sink.cs | 26 +------ BCT/BytecodeTranslator/StatementTraverser.cs | 2 +- BCT/BytecodeTranslator/TranslationHelper.cs | 4 ++ .../TranslationTest/GeneralHeapInput.txt | 2 - .../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(); 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 { lit }; var attrib = new Bpl.QKeyValue(typeDefinition.Token(), "inline", args, null); // TODO: Need to have it be {:inine 1} (and not just {:inline})? + + List vars = new List(); + 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(); + 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 vars = new List(); + 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); - } /// 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); } -- cgit v1.2.3