From b6da2cfd6722b056c821dad2618d032ced0ac9af Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 5 Mar 2011 01:09:57 +0000 Subject: changes for dealing with delegates --- BCT/BytecodeTranslator/MetadataTraverser.cs | 112 +++++++++++++++++++--------- BCT/BytecodeTranslator/TranslationHelper.cs | 4 +- 2 files changed, 79 insertions(+), 37 deletions(-) diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index ce5bff5b..0cdf2bf0 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -83,55 +83,96 @@ namespace BytecodeTranslator { break; } } - - var procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(invokeMethod, invokeMethod.IsStatic); - var proc = procAndFormalMap.Procedure; - var invars = proc.InParams; - var outvars = proc.OutParams; - - Bpl.IToken token = invokeMethod.Token(); - - this.sink.BeginMethod(); - + try { + var procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(invokeMethod, invokeMethod.IsStatic); + var proc = procAndFormalMap.Procedure; + var invars = proc.InParams; + var outvars = proc.OutParams; + + Bpl.IToken token = invokeMethod.Token(); + + Bpl.Formal method = new Bpl.Formal(token, new Bpl.TypedIdent(token, "method", Bpl.Type.Int), true); + Bpl.Formal receiver = new Bpl.Formal(token, new Bpl.TypedIdent(token, "receiver", Bpl.Type.Int), true); + + Bpl.VariableSeq dispatchProcInvars = new Bpl.VariableSeq(); + dispatchProcInvars.Add(method); + dispatchProcInvars.Add(receiver); + for (int i = 1; i < invars.Length; i++) { + Bpl.Variable f = invars[i]; + dispatchProcInvars.Add(new Bpl.Formal(token, new Bpl.TypedIdent(token, f.Name, f.TypedIdent.Type), true)); + } + Bpl.VariableSeq dispatchProcOutvars = new Bpl.VariableSeq(); + foreach (Bpl.Formal f in outvars) { + dispatchProcOutvars.Add(new Bpl.Formal(token, new Bpl.TypedIdent(token, f.Name, f.TypedIdent.Type), false)); + } - Bpl.LocalVariable method = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "method", Bpl.Type.Int)); - Bpl.LocalVariable receiver = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "receiver", Bpl.Type.Int)); - Bpl.LocalVariable iter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "iter", Bpl.Type.Int)); - Bpl.LocalVariable niter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "niter", Bpl.Type.Int)); - - Bpl.StmtListBuilder implStmtBuilder = new Bpl.StmtListBuilder(); - implStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), this.sink.ReadHead(Bpl.Expr.Ident(invars[0])))); + Bpl.Procedure dispatchProc = + new Bpl.Procedure(token, + "DispatchOne." + proc.Name, + new Bpl.TypeVariableSeq(), + dispatchProcInvars, + dispatchProcOutvars, + new Bpl.RequiresSeq(), + new Bpl.IdentifierExprSeq(), + new Bpl.EnsuresSeq()); + this.sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchProc); - Bpl.StmtListBuilder whileStmtBuilder = new Bpl.StmtListBuilder(); - whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(niter), this.sink.ReadNext(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(iter)))); - whileStmtBuilder.Add(BuildReturnCmd(Bpl.Expr.Eq(Bpl.Expr.Ident(niter), this.sink.ReadHead(Bpl.Expr.Ident(invars[0]))))); - whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(method), this.sink.ReadMethod(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter)))); - whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(receiver), this.sink.ReadReceiver(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter)))); Bpl.IfCmd ifCmd = BuildIfCmd(Bpl.Expr.True, new Bpl.AssumeCmd(token, Bpl.Expr.False), null); - foreach (IMethodDefinition defn in sink.delegateTypeToDelegates[type]) - { + foreach (IMethodDefinition defn in sink.delegateTypeToDelegates[type]) { Bpl.ExprSeq ins = new Bpl.ExprSeq(); Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq(); if (!defn.IsStatic) ins.Add(Bpl.Expr.Ident(receiver)); int index; - for (index = 1; index < invars.Length; index++) - { - ins.Add(Bpl.Expr.Ident(invars[index])); + for (index = 2; index < dispatchProcInvars.Length; index++) { + ins.Add(Bpl.Expr.Ident(dispatchProcInvars[index])); } - for (index = 0; index < outvars.Length; index++) - { - outs.Add(Bpl.Expr.Ident(outvars[index])); + for (index = 0; index < dispatchProcOutvars.Length; index++) { + outs.Add(Bpl.Expr.Ident(dispatchProcOutvars[index])); } Bpl.Constant c = sink.FindOrAddDelegateMethodConstant(defn); - Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(method), Bpl.Expr.Ident(c)); + Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(method), Bpl.Expr.Ident(c)); Bpl.CallCmd callCmd = new Bpl.CallCmd(token, c.Name, ins, outs); ifCmd = BuildIfCmd(bexpr, callCmd, ifCmd); } - whileStmtBuilder.Add(ifCmd); + Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder(); + ifStmtBuilder.Add(ifCmd); + Bpl.Implementation dispatchImpl = + new Bpl.Implementation(token, + dispatchProc.Name, + new Bpl.TypeVariableSeq(), + dispatchProc.InParams, + dispatchProc.OutParams, + new Bpl.VariableSeq(), + ifStmtBuilder.Collect(token) + ); + dispatchImpl.Proc = dispatchProc; + this.sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchImpl); + + Bpl.LocalVariable iter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "iter", Bpl.Type.Int)); + Bpl.LocalVariable niter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "niter", Bpl.Type.Int)); + + Bpl.StmtListBuilder implStmtBuilder = new Bpl.StmtListBuilder(); + implStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), this.sink.ReadHead(Bpl.Expr.Ident(invars[0])))); + + Bpl.StmtListBuilder whileStmtBuilder = new Bpl.StmtListBuilder(); + whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(niter), this.sink.ReadNext(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(iter)))); + whileStmtBuilder.Add(BuildReturnCmd(Bpl.Expr.Eq(Bpl.Expr.Ident(niter), this.sink.ReadHead(Bpl.Expr.Ident(invars[0]))))); + Bpl.ExprSeq inExprs = new Bpl.ExprSeq(); + inExprs.Add(this.sink.ReadMethod(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter))); + inExprs.Add(this.sink.ReadReceiver(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter))); + for (int i = 1; i < invars.Length; i++) { + Bpl.Variable f = invars[i]; + inExprs.Add(Bpl.Expr.Ident(f)); + } + Bpl.IdentifierExprSeq outExprs = new Bpl.IdentifierExprSeq(); + foreach (Bpl.Formal f in outvars) { + outExprs.Add(Bpl.Expr.Ident(f)); + } + whileStmtBuilder.Add(new Bpl.CallCmd(token, dispatchProc.Name, inExprs, outExprs)); whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), Bpl.Expr.Ident(niter))); Bpl.WhileCmd whileCmd = new Bpl.WhileCmd(token, Bpl.Expr.True, new List(), whileStmtBuilder.Collect(token)); @@ -141,12 +182,11 @@ namespace BytecodeTranslator { new Bpl.Implementation(token, proc.Name, new Bpl.TypeVariableSeq(), - proc.InParams, - proc.OutParams, - new Bpl.VariableSeq(iter, niter, method, receiver), + invars, + outvars, + new Bpl.VariableSeq(iter, niter), implStmtBuilder.Collect(token) ); - impl.Proc = proc; this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl); } diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 30e90f8a..f3b7aa58 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -90,6 +90,7 @@ namespace BytecodeTranslator { public static string CreateUniqueMethodName(IMethodReference method) { var containingTypeName = TypeHelper.GetTypeName(method.ContainingType, NameFormattingOptions.None); + /* if (containingTypeName == "Poirot.Poirot") { string name = method.Name.Value; @@ -99,9 +100,10 @@ namespace BytecodeTranslator { return "corral_atomic_end"; else if (name == "CurrentThreadId") return "corral_getThreadID"; - else if (name == "Nondet") + else if (name == "Nondet_int" || name == "Nondet_string") return "poirot_nondet"; } + */ var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId); s = s.Substring(2); s = s.TrimEnd(')'); -- cgit v1.2.3