From 50897a5a2e62d24899dad210377901d7a3ba446f Mon Sep 17 00:00:00 2001 From: Mike Barnett Date: Sun, 5 Feb 2012 12:34:44 -0800 Subject: Separated the concepts of "boxing" (i.e., CLR boxing of a value type) from the "union" type that is the supertype of all the translated Boogie types. --- BCT/BCT.sln | 32 +++++ BCT/BytecodeTranslator/ExpressionTraverser.cs | 190 ++++++++++++++++++-------- BCT/BytecodeTranslator/Heap.cs | 36 +---- BCT/BytecodeTranslator/HeapFactory.cs | 71 +++++++--- BCT/BytecodeTranslator/Program.cs | 4 +- BCT/BytecodeTranslator/StatementTraverser.cs | 21 +-- BCT/BytecodeTranslator/WholeProgram.cs | 2 +- 7 files changed, 241 insertions(+), 115 deletions(-) (limited to 'BCT') diff --git a/BCT/BCT.sln b/BCT/BCT.sln index c8c132bb..cdd22c63 100644 --- a/BCT/BCT.sln +++ b/BCT/BCT.sln @@ -54,6 +54,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILGarbageCollect", "..\..\C EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ControlAndDataFlowGraph", "..\..\ccicodebox\CodeGenerators\ControlAndDataFlowGraph\ControlAndDataFlowGraph.csproj", "{2596EFB0-87AE-42CE-89EB-84F35D6350D2}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "NewILToCodeModel", "..\..\CCICodeBox\Converters\NewILToCodeModel\NewILToCodeModel.csproj", "{A555D4CB-F16F-4049-A8CF-180B8A05C755}" +EndProject Global GlobalSection(TeamFoundationVersionControl) = preSolution SccNumberOfProjects = 17 @@ -829,6 +831,36 @@ Global {2596EFB0-87AE-42CE-89EB-84F35D6350D2}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU {2596EFB0-87AE-42CE-89EB-84F35D6350D2}.Release|Mixed Platforms.Build.0 = Release|Any CPU {2596EFB0-87AE-42CE-89EB-84F35D6350D2}.Release|x86.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|Any CPU.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|Any CPU.Build.0 = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|Mixed Platforms.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|Mixed Platforms.Build.0 = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|x86.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|Any CPU.Build.0 = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|x86.ActiveCfg = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|Any CPU.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|Any CPU.Build.0 = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|Mixed Platforms.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|Mixed Platforms.Build.0 = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|x86.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|Mixed Platforms.Build.0 = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|x86.ActiveCfg = Debug|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|Mixed Platforms.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|Mixed Platforms.Build.0 = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|x86.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|Any CPU.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|Any CPU.Build.0 = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|x86.ActiveCfg = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index e6e5c414..a9e1f9b0 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -331,22 +331,13 @@ namespace BytecodeTranslator // but the address of it must be a ref, so do the conversion this.Traverse(addressOf.Expression); var e = this.TranslatedExpressions.Pop(); - this.TranslatedExpressions.Push(this.sink.Heap.Unbox(addressOf.Token(), this.sink.Heap.RefType, e)); + this.TranslatedExpressions.Push(this.sink.Heap.FromUnion(addressOf.Token(), this.sink.Heap.RefType, e)); } else { this.Traverse(addressOf.Expression); } } else { this.Traverse(addressOf.Expression); return; - // TODO: Sometimes the value must still be boxed: for anythign that is not going to be represented as a Ref in Boogie! - //this.Traverse(addressOf.Expression); - //var e = this.TranslatedExpressions.Pop(); - - //Bpl.Variable a = this.sink.CreateFreshLocal(addressOf.Type); - //this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a)))); - //this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(Bpl.Token.NoToken, Bpl.Expr.Ident(a), Bpl.Expr.Ident(this.sink.Heap.BoxField), e, AccessType.Heap, boogieT)); - //this.TranslatedExpressions.Push(Bpl.Expr.Ident(a)); - } } #endregion @@ -554,7 +545,7 @@ namespace BytecodeTranslator List inexpr; List outvars; Bpl.IdentifierExpr thisExpr; - Dictionary toBoxed; + Dictionary> toBoxed; var proc = TranslateArgumentsAndReturnProcedure(methodCallToken, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed); string methodname = proc.Name; var translateAsFunctionCall = proc is Bpl.Function; @@ -596,6 +587,7 @@ namespace BytecodeTranslator this.TranslatedExpressions.Push(callFunction); return; } else { + EmitLineDirective(methodCallToken); if (attrib != null) call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars, attrib); else @@ -604,8 +596,20 @@ namespace BytecodeTranslator } } - foreach (KeyValuePair kv in toBoxed) { - this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value))); + foreach (KeyValuePair> kv in toBoxed) { + var lhs = kv.Key; + var tuple = kv.Value; + var rhs = tuple.Item1; + Bpl.Expr fromUnion; + if (tuple.Item2) { + // Since both structs and objects are represented by "Ref", need to make a distinction here. + // Review: Introduce an explicit type "Struct"? + fromUnion = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Struct), new Bpl.ExprSeq(rhs)); + } else { + fromUnion = this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs); + //this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs))); + } + this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion)); } Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef)); @@ -630,6 +634,17 @@ namespace BytecodeTranslator } } + private void EmitLineDirective(Bpl.IToken methodCallToken) { + var sloc = this.StmtTraverser.lastSourceLocation; + if (sloc != null) { + var fileName = sloc.Document.Location; + var lineNumber = sloc.StartLine; + var attrib = new Bpl.QKeyValue(methodCallToken, "sourceLine", new List { Bpl.Expr.Literal((int)lineNumber) }, null); + attrib = new Bpl.QKeyValue(methodCallToken, "sourceFile", new List { fileName }, attrib); + this.StmtTraverser.StmtBuilder.Add(new Bpl.AssertCmd(methodCallToken, Bpl.Expr.True, attrib)); + } + } + private Bpl.CallCmd translateAddRemoveCall(IMethodCall methodCall, IMethodDefinition resolvedMethod, Bpl.IToken methodCallToken, List inexpr, List outvars, Bpl.IdentifierExpr thisExpr, bool isEventAdd) { Bpl.CallCmd call; var mName = resolvedMethod.Name.Value; @@ -670,6 +685,7 @@ namespace BytecodeTranslator this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(thisExpr))); // Second, generate the call to the appropriate ctor + EmitLineDirective(methodCallToken); this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, proc.Name, inexpr, outvars)); // Generate an assumption about the dynamic type of the just allocated object @@ -684,7 +700,7 @@ namespace BytecodeTranslator } // REVIEW: Does "thisExpr" really need to come back as an identifier? Can't it be a general expression? - protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable arguments, out List inexpr, out List outvars, out Bpl.IdentifierExpr thisExpr, out Dictionary toBoxed) { + protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable arguments, out List inexpr, out List outvars, out Bpl.IdentifierExpr thisExpr, out Dictionary> toUnioned) { inexpr = new List(); outvars = new List(); @@ -718,7 +734,7 @@ namespace BytecodeTranslator } #endregion - toBoxed = new Dictionary(); + toUnioned = new Dictionary>(); IEnumerator penum = resolvedMethod.Parameters.GetEnumerator(); penum.MoveNext(); foreach (IExpression exp in arguments) { @@ -755,9 +771,16 @@ namespace BytecodeTranslator e = bplLocal; } - if (currentType is IGenericParameterReference && this.sink.CciTypeToBoogie(currentType) == this.sink.Heap.UnionType) - inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(expressionToTraverse.Type), e)); - else { + if (currentType is IGenericParameterReference && this.sink.CciTypeToBoogie(currentType) == this.sink.Heap.UnionType) { + if (TranslationHelper.IsStruct(expressionToTraverse.Type)) { + // Since both structs and objects are represented by "Ref", need to make a distinction here. + // Review: Introduce an explicit type "Struct"? + var toUnion = new Bpl.NAryExpr(token, new Bpl.FunctionCall(this.sink.Heap.Struct2Union), new Bpl.ExprSeq(e)); + inexpr.Add(toUnion); + } else { + inexpr.Add(sink.Heap.ToUnion(token, this.sink.CciTypeToBoogie(expressionToTraverse.Type), e)); + } + } else { inexpr.Add(e); } if (penum.Current.IsByReference) { @@ -769,7 +792,7 @@ namespace BytecodeTranslator var boogieType = this.sink.CciTypeToBoogie(penum.Current.Type); if (boogieType == this.sink.Heap.UnionType) { Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.UnionType)); - toBoxed[unboxed] = boxed; + toUnioned[unboxed] = Tuple.Create(boxed,false); outvars.Add(boxed); } else { outvars.Add(unboxed); @@ -800,20 +823,20 @@ namespace BytecodeTranslator if (!translateAsFunctionCall) { if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) { Bpl.Variable v = this.sink.CreateFreshLocal(methodToCall.ResolvedMethod.Type.ResolvedType); - Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v); + Bpl.IdentifierExpr unUnioned = new Bpl.IdentifierExpr(token, v); if (resolvedMethod.Type is IGenericParameterReference) { var boogieType = this.sink.CciTypeToBoogie(resolvedMethod.Type); if (boogieType == this.sink.Heap.UnionType) { - Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.UnionType)); - toBoxed[unboxed] = boxed; - outvars.Add(boxed); + Bpl.IdentifierExpr unioned = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.UnionType)); + toUnioned[unUnioned] = Tuple.Create(unioned, TranslationHelper.IsStruct(methodToCall.ResolvedMethod.Type.ResolvedType)); + outvars.Add(unioned); } else { - outvars.Add(unboxed); + outvars.Add(unUnioned); } } else { - outvars.Add(unboxed); + outvars.Add(unUnioned); } - TranslatedExpressions.Push(unboxed); + TranslatedExpressions.Push(unUnioned); } } @@ -882,6 +905,8 @@ namespace BytecodeTranslator } Bpl.Cmd cmd; + EmitLineDirective(tok); + var/*?*/ local = container as ILocalDefinition; if (local != null) { Contract.Assume(instance == null); @@ -1025,9 +1050,12 @@ namespace BytecodeTranslator List inexpr; List outvars; Bpl.IdentifierExpr thisExpr; - Dictionary toBoxed; + Dictionary> toBoxed; var proc = TranslateArgumentsAndReturnProcedure(token, ctor, resolvedMethod, null, createObjectInstance.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed); inexpr.Insert(0, Bpl.Expr.Ident(a)); + + EmitLineDirective(token); + this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, proc.Name, inexpr, outvars)); // Generate an assumption about the dynamic type of the just allocated object @@ -1574,7 +1602,8 @@ namespace BytecodeTranslator this.Traverse(conversion.ValueToConvert); var boogieTypeOfValue = this.sink.CciTypeToBoogie(conversion.ValueToConvert.Type); var boogieTypeToBeConvertedTo = this.sink.CciTypeToBoogie(conversion.TypeAfterConversion); - if (boogieTypeOfValue == boogieTypeToBeConvertedTo) { + if (boogieTypeOfValue == boogieTypeToBeConvertedTo && !TranslationHelper.IsStruct(conversion.ValueToConvert.Type) + && !TranslationHelper.IsStruct(conversion.TypeAfterConversion)) { // then this conversion is a nop, just ignore it return; } @@ -1584,20 +1613,44 @@ namespace BytecodeTranslator var exp = TranslatedExpressions.Pop(); + if (boogieTypeOfValue == this.sink.Heap.UnionType && boogieTypeToBeConvertedTo != this.sink.Heap.RefType) { + var e = this.sink.Heap.FromUnion(tok, boogieTypeToBeConvertedTo, exp); + TranslatedExpressions.Push(e); + return; + } + if (boogieTypeToBeConvertedTo == this.sink.Heap.UnionType) { + Bpl.Expr e; + if (boogieTypeOfValue == this.sink.Heap.RefType) + e = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Union), new Bpl.ExprSeq(exp)); + else + e = this.sink.Heap.ToUnion(tok, boogieTypeOfValue, exp); + TranslatedExpressions.Push(e); + return; + } + + if (boogieTypeToBeConvertedTo == this.sink.Heap.RefType && + TranslationHelper.IsStruct(conversion.TypeAfterConversion) && + boogieTypeOfValue == this.sink.Heap.RefType) { + // REVIEW: This also applies to conversions from one struct type to another! + var e = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Struct), new Bpl.ExprSeq(exp)); + TranslatedExpressions.Push(e); + return; + } + if (boogieTypeToBeConvertedTo == Bpl.Type.Bool) { Bpl.Expr expr; if (boogieTypeOfValue == Bpl.Type.Int) { expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Literal(0)); } else if (boogieTypeOfValue == this.sink.Heap.RefType) { - expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Ident(this.sink.Heap.NullRef)); + expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Bool), new Bpl.ExprSeq(exp)); } else if (boogieTypeOfValue == this.sink.Heap.RealType) { expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Real2Int), new Bpl.ExprSeq(exp)); expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, expr, Bpl.Expr.Literal(0)); } else if (boogieTypeOfValue == this.sink.Heap.UnionType) { - expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Bool), new Bpl.ExprSeq(exp)); + expr = this.sink.Heap.FromUnion(tok, Bpl.Type.Bool, exp); } else { throw new NotImplementedException(msg); @@ -1612,13 +1665,13 @@ namespace BytecodeTranslator expr = new Bpl.NAryExpr(tok, new Bpl.IfThenElse(tok), new Bpl.ExprSeq(exp, Bpl.Expr.Literal(1), Bpl.Expr.Literal(0))); } else if (boogieTypeOfValue == this.sink.Heap.RefType) { - expr = this.sink.Heap.ReadHeap(exp, Bpl.Expr.Ident(this.sink.Heap.BoxField), AccessType.Heap, Bpl.Type.Int); + expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Int), new Bpl.ExprSeq(exp)); } else if (boogieTypeOfValue == this.sink.Heap.RealType) { expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Real2Int), new Bpl.ExprSeq(exp)); } else if (boogieTypeOfValue == this.sink.Heap.UnionType) { - expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Int), new Bpl.ExprSeq(exp)); + expr = this.sink.Heap.FromUnion(Bpl.Token.NoToken, Bpl.Type.Int, exp); } else { throw new NotImplementedException(msg); @@ -1628,9 +1681,32 @@ namespace BytecodeTranslator } if (boogieTypeToBeConvertedTo == this.sink.Heap.RefType) { + // var a = BoxFromXXX(exp); Bpl.Variable a = this.sink.CreateFreshLocal(conversion.TypeAfterConversion); - this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a)))); - this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(Bpl.Token.NoToken, Bpl.Expr.Ident(a), Bpl.Expr.Ident(this.sink.Heap.BoxField), exp, AccessType.Heap, boogieTypeOfValue)); + Bpl.Procedure boxOperator; + if (boogieTypeOfValue == Bpl.Type.Bool) + boxOperator = this.sink.Heap.BoxFromBool; + else if (boogieTypeOfValue == Bpl.Type.Int) + boxOperator = this.sink.Heap.BoxFromInt; + else if (boogieTypeOfValue == this.sink.Heap.RealType) + boxOperator = this.sink.Heap.BoxFromReal; + else if (TranslationHelper.IsStruct(conversion.ValueToConvert.Type)) { + // Boxing a struct implicitly makes a copy of the struct + var typeOfValue = conversion.ValueToConvert.Type; + var proc = this.sink.FindOrCreateProcedureForStructCopy(typeOfValue); + var bplLocal = Bpl.Expr.Ident(this.sink.CreateFreshLocal(typeOfValue)); + var cmd = new Bpl.CallCmd(tok, proc.Name, new List { exp, }, new List { bplLocal, }); + this.StmtTraverser.StmtBuilder.Add(cmd); + exp = bplLocal; + boxOperator = this.sink.Heap.BoxFromStruct; + } else { + if (boogieTypeOfValue != this.sink.Heap.UnionType) + throw new NotImplementedException(msg); + boxOperator = this.sink.Heap.BoxFromUnion; + } + var name = boxOperator.Name; + + this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, name, new Bpl.ExprSeq(exp), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a)))); TranslatedExpressions.Push(Bpl.Expr.Ident(a)); return; } @@ -1645,10 +1721,10 @@ namespace BytecodeTranslator expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Int2Real), new Bpl.ExprSeq(exp)); } else if (boogieTypeOfValue == this.sink.Heap.RefType) { - expr = this.sink.Heap.ReadHeap(exp, Bpl.Expr.Ident(this.sink.Heap.BoxField), AccessType.Heap, this.sink.Heap.RealType); + expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Real), new Bpl.ExprSeq(exp)); } else if (boogieTypeOfValue == this.sink.Heap.UnionType) { - expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Real), new Bpl.ExprSeq(exp)); + expr = this.sink.Heap.FromUnion(tok, this.sink.Heap.RealType, exp); } else { throw new NotImplementedException(msg); @@ -1657,27 +1733,27 @@ namespace BytecodeTranslator return; } - if (boogieTypeToBeConvertedTo == this.sink.Heap.UnionType) { - Bpl.Function func; - if (boogieTypeOfValue == Bpl.Type.Bool) { - func = this.sink.Heap.Bool2Union; - } - else if (boogieTypeOfValue == Bpl.Type.Int) { - func = this.sink.Heap.Int2Union; - } - else if (boogieTypeOfValue == this.sink.Heap.RefType) { - func = this.sink.Heap.Ref2Union; - } - else if (boogieTypeOfValue == this.sink.Heap.RealType) { - func = this.sink.Heap.Real2Union; - } - else { - throw new NotImplementedException(msg); - } - var boxExpr = new Bpl.NAryExpr(conversion.Token(), new Bpl.FunctionCall(func), new Bpl.ExprSeq(exp)); - TranslatedExpressions.Push(boxExpr); - return; - } + //if (boogieTypeToBeConvertedTo == this.sink.Heap.UnionType) { + // Bpl.Function func; + // if (boogieTypeOfValue == Bpl.Type.Bool) { + // func = this.sink.Heap.Bool2Union; + // } + // else if (boogieTypeOfValue == Bpl.Type.Int) { + // func = this.sink.Heap.Int2Union; + // } + // else if (boogieTypeOfValue == this.sink.Heap.RefType) { + // func = this.sink.Heap.Ref2Union; + // } + // else if (boogieTypeOfValue == this.sink.Heap.RealType) { + // func = this.sink.Heap.Real2Union; + // } + // else { + // throw new NotImplementedException(msg); + // } + // var boxExpr = new Bpl.NAryExpr(conversion.Token(), new Bpl.FunctionCall(func), new Bpl.ExprSeq(exp)); + // TranslatedExpressions.Push(boxExpr); + // return; + //} } public override void TraverseChildren(IOnesComplement onesComplement) { diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 0c976bcc..aaed79e4 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -29,15 +29,6 @@ namespace BytecodeTranslator { /// public class SplitFieldsHeap : Heap { - #region "Boxing" as done in the CLR - /// - /// Used to represent "boxing" as it is done in the CLR. - /// - [RepresentationFor("$BoxField", "var $BoxField: [Ref]Box;")] - private Bpl.GlobalVariable boxField = null; - public override Bpl.Variable BoxField { get { return boxField; } } - #endregion - /// /// Prelude text for which access to the ASTs is not needed /// @@ -122,13 +113,10 @@ namespace BytecodeTranslator { if (accessType == AccessType.Struct || accessType == AccessType.Heap) { Bpl.IdentifierExpr field = f as Bpl.IdentifierExpr; Debug.Assert(field != null); - if (field.Decl == this.BoxField) - return Unbox(f.tok, unboxType, Bpl.Expr.Select(field, o)); - else - return Bpl.Expr.Select(field, o); + return Bpl.Expr.Select(field, o); } else - return Unbox(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f)); + return FromUnion(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f)); } /// @@ -140,13 +128,10 @@ namespace BytecodeTranslator { if (accessType == AccessType.Struct || accessType == AccessType.Heap) { Bpl.IdentifierExpr field = f as Bpl.IdentifierExpr; Debug.Assert(field != null); - if (field.Decl == this.BoxField) - return Bpl.Cmd.MapAssign(tok, field, o, Box(tok, boxType, value)); - else - return Bpl.Cmd.MapAssign(tok, field, o, value); + return Bpl.Cmd.MapAssign(tok, field, 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, Box(f.tok, boxType, 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, ToUnion(f.tok, boxType, value)))); } } @@ -159,15 +144,6 @@ namespace BytecodeTranslator { /// public class GeneralHeap : Heap { - #region "Boxing" as done in the CLR - /// - /// Used to represent "boxing" as it is done in the CLR. - /// - [RepresentationFor("$BoxField", "const unique $BoxField: Field;")] - private Bpl.Constant boxField = null; - public override Bpl.Variable BoxField { get { return boxField; } } - #endregion - #region Fields [RepresentationFor("$Heap", "var $Heap: HeapType;", true)] @@ -268,7 +244,7 @@ namespace BytecodeTranslator { callRead = Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f); // wrap it in the right conversion function - var callExpr = Unbox(f.tok, unboxType, callRead); + var callExpr = FromUnion(f.tok, unboxType, callRead); return callExpr; } @@ -281,7 +257,7 @@ namespace BytecodeTranslator { Bpl.IdentifierExpr h; Bpl.NAryExpr callWrite; - var callConversion = Box(f.tok, boxType, value); + var callConversion = ToUnion(f.tok, boxType, value); if (accessType == AccessType.Struct || accessType == AccessType.Heap) { h = Bpl.Expr.Ident(HeapVariable); diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index dc281ad6..f4a04b37 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -73,8 +73,6 @@ namespace BytecodeTranslator { public abstract Bpl.Variable CreateFieldVariable(IFieldReference field); - public abstract Bpl.Variable BoxField { get; } - #region Boogie Types [RepresentationFor("Delegate", "type {:datatype} Delegate;")] @@ -101,7 +99,7 @@ namespace BytecodeTranslator { public Bpl.TypeCtorDecl FieldTypeDecl = null; public Bpl.CtorType FieldType; - [RepresentationFor("Union", "type Union;")] + [RepresentationFor("Union", "type {:datatype} Union;")] public Bpl.TypeCtorDecl UnionTypeDecl = null; public Bpl.CtorType UnionType; @@ -126,38 +124,81 @@ namespace BytecodeTranslator { #endregion + #region CLR Boxing + + [RepresentationFor("$BoxFromBool", "procedure $BoxFromBool(b: bool) returns (r: Ref) free ensures $BoxedValue(r) == Bool2Union(b); { call r := Alloc(); assume $BoxedValue(r) == Bool2Union(b); }")] + public Bpl.Procedure BoxFromBool = null; + + [RepresentationFor("$BoxFromInt", "procedure $BoxFromInt(i: int) returns (r: Ref) free ensures $BoxedValue(r) == Int2Union(i); { call r := Alloc(); assume $BoxedValue(r) == Int2Union(i); }")] + public Bpl.Procedure BoxFromInt = null; + + [RepresentationFor("$BoxFromReal", "procedure $BoxFromReal(r: Real) returns (rf: Ref) free ensures $BoxedValue(rf) == Real2Union(r); { call rf := Alloc(); assume $BoxedValue(rf) == Real2Union(r); }")] + public Bpl.Procedure BoxFromReal = null; + + [RepresentationFor("$BoxFromStruct", "procedure $BoxFromStruct(s: Ref) returns (r: Ref) free ensures $BoxedValue(r) == Struct2Union(s); { call r := Alloc(); assume $BoxedValue(r) == Struct2Union(s); }")] + public Bpl.Procedure BoxFromStruct = null; + + [RepresentationFor("$BoxFromUnion", "procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref) { if (is#Ref2Union(u)) { r := refValue#Ref2Union(u); } else { call r := Alloc(); assume $BoxedValue(r) == u; } }")] + public Bpl.Procedure BoxFromUnion = null; + + [RepresentationFor("$BoxedValue", "function $BoxedValue(r: Ref): Union;")] + public Bpl.Function BoxedValue = null; + + [RepresentationFor("$Unbox2Bool", "function $Unbox2Bool(r: Ref): (bool) { boolValue#Bool2Union($BoxedValue(r)) }")] + public Bpl.Function Unbox2Bool = null; + + [RepresentationFor("$Unbox2Int", "function $Unbox2Int(r: Ref): (int) { intValue#Int2Union($BoxedValue(r)) }")] + public Bpl.Function Unbox2Int = null; + + [RepresentationFor("$Unbox2Real", "function $Unbox2Real(r: Ref): (Real) { realValue#Real2Union($BoxedValue(r)) }")] + public Bpl.Function Unbox2Real = null; + + [RepresentationFor("$Unbox2Struct", "function $Unbox2Struct(r: Ref): (Ref) { structValue#Struct2Union($BoxedValue(r)) }")] + public Bpl.Function Unbox2Struct = null; + + [RepresentationFor("$Unbox2Union", "function $Unbox2Union(r: Ref): (Union) { $BoxedValue(r) }")] + public Bpl.Function Unbox2Union = null; + + #endregion + #region Conversions #region Heap values - [RepresentationFor("Union2Bool", "function Union2Bool(Union): bool;")] + [RepresentationFor("Union2Bool", "function Union2Bool(u: Union): (bool) { boolValue#Bool2Union(u) }")] public Bpl.Function Union2Bool = null; - [RepresentationFor("Union2Int", "function Union2Int(Union): int;")] + [RepresentationFor("Union2Int", "function Union2Int(u: Union): (int) { intValue#Int2Union(u) }")] public Bpl.Function Union2Int = null; - [RepresentationFor("Union2Ref", "function Union2Ref(Union): Ref;")] + [RepresentationFor("Union2Ref", "function Union2Ref(u: Union): (Ref) { refValue#Ref2Union(u) }")] public Bpl.Function Union2Ref = null; - [RepresentationFor("Union2Real", "function Union2Real(Union): Real;")] + [RepresentationFor("Union2Real", "function Union2Real(u: Union): (Real) { realValue#Real2Union(u) }")] public Bpl.Function Union2Real = null; - [RepresentationFor("Bool2Union", "function Bool2Union(bool): Union;")] + [RepresentationFor("Union2Struct", "function Union2Struct(u: Union): (Ref) { structValue#Struct2Union(u) }")] + public Bpl.Function Union2Struct = null; + + [RepresentationFor("Bool2Union", "function {:constructor} Bool2Union(boolValue: bool): Union;")] public Bpl.Function Bool2Union = null; - [RepresentationFor("Int2Union", "function Int2Union(int): Union;")] + [RepresentationFor("Int2Union", "function {:constructor} Int2Union(intValue: int): Union;")] public Bpl.Function Int2Union = null; - [RepresentationFor("Ref2Union", "function Ref2Union(Ref): Union;")] + [RepresentationFor("Ref2Union", "function {:constructor} Ref2Union(refValue: Ref): Union;")] public Bpl.Function Ref2Union = null; - [RepresentationFor("Real2Union", "function Real2Union(Real): Union;")] + [RepresentationFor("Real2Union", "function {:constructor} Real2Union(realValue: Real): Union;")] public Bpl.Function Real2Union = null; + [RepresentationFor("Struct2Union", "function {:constructor} Struct2Union(structValue: Ref): Union;")] + public Bpl.Function Struct2Union = null; + [RepresentationFor("Union2Union", "function {:inline true} Union2Union(u: Union): Union { u }")] public Bpl.Function Union2Union = null; - public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) { + public Bpl.Expr ToUnion(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) { Bpl.Function conversion; if (boogieType == Bpl.Type.Bool) conversion = this.Bool2Union; @@ -180,7 +221,7 @@ namespace BytecodeTranslator { return callConversion; } - public Bpl.Expr Unbox(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) { + public Bpl.Expr FromUnion(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) { Bpl.Function conversion = null; if (boogieType == Bpl.Type.Bool) conversion = this.Union2Bool; @@ -384,10 +425,6 @@ axiom Union2Int($DefaultHeapValue) == 0; axiom Union2Bool($DefaultHeapValue) == false; axiom Union2Ref($DefaultHeapValue) == null; -axiom (forall x: int :: { Int2Union(x) } Union2Int(Int2Union(x)) == x ); -axiom (forall x: bool :: { Bool2Union(x) } Union2Bool(Bool2Union(x)) == x ); -axiom (forall x: Ref :: { Ref2Union(x) } Union2Ref(Ref2Union(x)) == x ); - function $ThreadDelegate(Ref) : Ref; procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref) diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index abbdcc00..8de2f91e 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -566,10 +566,10 @@ namespace BytecodeTranslator { if (rtype == ltype) { // do nothing } else if (ltype == sink.Heap.UnionType) { - rexpr = sink.Heap.Box(Bpl.Token.NoToken, rtype, rexpr); + rexpr = sink.Heap.ToUnion(Bpl.Token.NoToken, rtype, rexpr); } else if (rtype == sink.Heap.UnionType) { - rexpr = sink.Heap.Unbox(Bpl.Token.NoToken, ltype, rexpr); + rexpr = sink.Heap.FromUnion(Bpl.Token.NoToken, ltype, rexpr); } else { System.Diagnostics.Debug.Assert(false); diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index c36608b6..14eee8c6 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -122,6 +122,8 @@ namespace BytecodeTranslator foreach (var sloc in slocs) { fileName = sloc.Document.Location; lineNumber = sloc.StartLine; + + this.parent.lastSourceLocation = sloc; break; } if (fileName != null) { @@ -237,6 +239,7 @@ namespace BytecodeTranslator } private static int counter = 0; + public IPrimarySourceLocation lastSourceLocation; internal int NextUniqueNumber() { return counter++; } @@ -336,14 +339,16 @@ namespace BytecodeTranslator // 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 if (isStruct) { - var defaultValue = new DefaultValue() { - DefaultValueType = typ, - Locations = new List(localDeclarationStatement.Locations), - Type = typ, - }; - var e2 = ExpressionFor(defaultValue); - StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e2)); - if (structCopy) { + if (!structCopy) { + var defaultValue = new DefaultValue() { + DefaultValueType = typ, + Locations = new List(localDeclarationStatement.Locations), + Type = typ, + }; + var e2 = ExpressionFor(defaultValue); + StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e2)); + } else + /*if (structCopy) */{ var proc = this.sink.FindOrCreateProcedureForStructCopy(typ); e = ExpressionFor(initVal); StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, new List { e, }, new List{ boogieLocalExpr, })); diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs index bd297451..73e882e0 100644 --- a/BCT/BytecodeTranslator/WholeProgram.cs +++ b/BCT/BytecodeTranslator/WholeProgram.cs @@ -140,7 +140,7 @@ namespace BytecodeTranslator { List inexpr; List outvars; Bpl.IdentifierExpr thisExpr; - Dictionary toBoxed; + Dictionary> toBoxed; var proc = TranslateArgumentsAndReturnProcedure(token, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed); -- cgit v1.2.3