summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2011-03-05 01:09:57 +0000
committerGravatar qadeer <unknown>2011-03-05 01:09:57 +0000
commitb6da2cfd6722b056c821dad2618d032ced0ac9af (patch)
tree7741b276aba3435e3a2ad1e3014c41b737ec2701
parent8a2dd8d4c29df3db73dd13a5457efbee007dfeac (diff)
changes for dealing with delegates
-rw-r--r--BCT/BytecodeTranslator/MetadataTraverser.cs112
-rw-r--r--BCT/BytecodeTranslator/TranslationHelper.cs4
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<Bpl.PredicateCmd>(), 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(')');