diff options
Diffstat (limited to 'BCT/BytecodeTranslator')
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 4 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 210 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 155 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 3 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TraverserFactory.cs | 2 |
5 files changed, 197 insertions, 177 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 14ec1da2..86162129 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -85,8 +85,8 @@ namespace BytecodeTranslator IFieldReference/*?*/ field = addressableExpression.Definition as IFieldReference;
if (field != null)
{
- //TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.ClassTraverser.FindOrCreateFieldVariable(field.ResolvedField)));
- throw new NotImplementedException();
+ TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field.ResolvedField)));
+ return;
}
IArrayIndexer/*?*/ arrayIndexer = addressableExpression.Definition as IArrayIndexer;
if (arrayIndexer != null)
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index c5dae569..9b895fe3 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -29,18 +29,15 @@ namespace BytecodeTranslator { public readonly TraverserFactory factory;
- public readonly IContractProvider ContractProvider;
-
public readonly PdbReader/*?*/ PdbReader;
public Bpl.Variable HeapVariable;
- public MetadataTraverser(Sink sink, IContractProvider cp, PdbReader/*?*/ pdbReader)
+ public MetadataTraverser(Sink sink, PdbReader/*?*/ pdbReader)
: base() {
this.sink = sink;
this.factory = sink.Factory;
- ContractProvider = cp;
this.PdbReader = pdbReader;
}
@@ -244,140 +241,62 @@ namespace BytecodeTranslator { /// </summary>
public override void Visit(IMethodDefinition method) {
- Dictionary<IParameterDefinition, MethodParameter> formalMap = new Dictionary<IParameterDefinition, MethodParameter>();
this.sink.BeginMethod();
- try {
- #region Create in- and out-parameters
-
- int in_count = 0;
- int out_count = 0;
- MethodParameter mp;
- foreach (IParameterDefinition formal in method.Parameters) {
-
- mp = new MethodParameter(formal);
- if (mp.inParameterCopy != null) in_count++;
- if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))
- out_count++;
- formalMap.Add(formal, mp);
- }
- this.sink.FormalMap = formalMap;
-
- #region Look for Returnvalue
+ var proc = this.sink.FindOrCreateProcedure(method, method.IsStatic);
- if (method.Type.TypeCode != PrimitiveTypeCode.Void) {
- Bpl.Type rettype = TranslationHelper.CciTypeToBoogie(method.Type);
- out_count++;
- this.sink.RetVariable = new Bpl.Formal(method.Token(),
- new Bpl.TypedIdent(method.Type.Token(),
- "$result", rettype), false);
- } else {
- this.sink.RetVariable = null;
- }
-
- #endregion
+ try {
- Bpl.Formal/*?*/ self = null;
- #region Create 'this' parameter
- if (!method.IsStatic) {
- in_count++;
- Bpl.Type selftype = Bpl.Type.Int;
- self = new Bpl.Formal(method.Token(),
- new Bpl.TypedIdent(method.Type.Token(),
- "this", selftype), true);
+ if (method.IsAbstract) {
+ throw new NotImplementedException("abstract methods are not yet implemented");
}
- #endregion
-
- Bpl.Variable[] invars = new Bpl.Formal[in_count];
- Bpl.Variable[] outvars = new Bpl.Formal[out_count];
- int i = 0;
- int j = 0;
+ StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader);
- #region Add 'this' parameter as first in parameter
- if (!method.IsStatic)
- invars[i++] = self;
- #endregion
+ #region Add assignements from In-Params to local-Params
- foreach (MethodParameter mparam in formalMap.Values) {
+ foreach (MethodParameter mparam in this.sink.FormalMap.Values) {
if (mparam.inParameterCopy != null) {
- invars[i++] = mparam.inParameterCopy;
- }
- if (mparam.outParameterCopy != null) {
- if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)
- outvars[j++] = mparam.outParameterCopy;
+ Bpl.IToken tok = method.Token();
+ stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
+ new Bpl.IdentifierExpr(tok, mparam.outParameterCopy),
+ new Bpl.IdentifierExpr(tok, mparam.inParameterCopy)));
}
}
- #region add the returnvalue to out if there is one
- if (this.sink.RetVariable != null) outvars[j] = this.sink.RetVariable;
#endregion
- #endregion
-
- #region Check The Method Contracts
- Bpl.RequiresSeq boogiePrecondition = new Bpl.RequiresSeq();
- Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();
- Bpl.IdentifierExprSeq boogieModifies = new Bpl.IdentifierExprSeq();
-
- IMethodContract contract = ContractProvider.GetMethodContractFor(method);
-
- if (contract != null) {
- try {
- foreach (IPrecondition pre in contract.Preconditions) {
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this.sink, null);
- exptravers.Visit(pre.Condition); // TODO
- // Todo: Deal with Descriptions
-
-
- Bpl.Requires req
- = new Bpl.Requires(pre.Token(),
- false, exptravers.TranslatedExpressions.Pop(), "");
- boogiePrecondition.Add(req);
- }
-
- foreach (IPostcondition post in contract.Postconditions) {
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this.sink, null);
-
- exptravers.Visit(post.Condition);
- // Todo: Deal with Descriptions
-
- Bpl.Ensures ens =
- new Bpl.Ensures(post.Token(),
- false, exptravers.TranslatedExpressions.Pop(), "");
- boogiePostcondition.Add(ens);
- }
-
- foreach (IAddressableExpression mod in contract.ModifiedVariables) {
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this.sink, null);
- exptravers.Visit(mod);
-
- Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
+ try {
+ method.Body.Dispatch(stmtTraverser);
+ } catch (TranslationException te) {
+ throw new NotImplementedException("No Errorhandling in Methodvisitor / " + te.ToString());
+ } catch {
+ throw;
+ }
- if (idexp == null) {
- throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));
- }
- boogieModifies.Add(idexp);
- }
- } catch (TranslationException te) {
- throw new NotImplementedException("Cannot Handle Errors in Method Contract: " + te.ToString());
- } catch {
- throw;
- }
+ #region Create Local Vars For Implementation
+ List<Bpl.Variable> vars = new List<Bpl.Variable>();
+ foreach (MethodParameter mparam in this.sink.FormalMap.Values) {
+ if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))
+ vars.Add(mparam.outParameterCopy);
+ }
+ foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {
+ vars.Add(v);
}
+ Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
#endregion
- string MethodName = TranslationHelper.CreateUniqueMethodName(method);
+ Bpl.Implementation impl =
+ new Bpl.Implementation(method.Token(),
+ proc.Name,
+ new Microsoft.Boogie.TypeVariableSeq(),
+ proc.InParams,
+ proc.OutParams,
+ vseq,
+ stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));
- Bpl.Procedure proc = new Bpl.Procedure(method.Token(),
- MethodName, // make it unique!
- new Bpl.TypeVariableSeq(),
- new Bpl.VariableSeq(invars), // in
- new Bpl.VariableSeq(outvars), // out
- boogiePrecondition,
- boogieModifies,
- boogiePostcondition);
+ impl.Proc = proc;
// Don't need an expression translator because there is a limited set of things
// that can appear as arguments to custom attributes
@@ -407,62 +326,11 @@ namespace BytecodeTranslator { args[argIndex++] = o;
}
}
- proc.AddAttribute(attrName, args);
- }
-
- this.sink.TranslatedProgram.TopLevelDeclarations.Add(proc);
-
- if (method.IsAbstract) {
- throw new NotImplementedException("abstract methods are not yet implemented");
- }
-
- StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader);
-
- #region Add assignements from In-Params to local-Params
-
- foreach (MethodParameter mparam in formalMap.Values) {
- if (mparam.inParameterCopy != null) {
- Bpl.IToken tok = method.Token();
- stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
- new Bpl.IdentifierExpr(tok, mparam.outParameterCopy),
- new Bpl.IdentifierExpr(tok, mparam.inParameterCopy)));
- }
- }
-
- #endregion
-
- try {
- method.ResolvedMethod.Body.Dispatch(stmtTraverser);
- } catch (TranslationException te) {
- throw new NotImplementedException("No Errorhandling in Methodvisitor / " + te.ToString());
- } catch {
- throw;
+ impl.AddAttribute(attrName, args);
}
- #region Create Local Vars For Implementation
- List<Bpl.Variable> vars = new List<Bpl.Variable>();
- foreach (MethodParameter mparam in formalMap.Values) {
- if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))
- vars.Add(mparam.outParameterCopy);
- }
- foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {
- vars.Add(v);
- }
-
- Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
- #endregion
-
- Bpl.Implementation impl =
- new Bpl.Implementation(method.Token(),
- MethodName, // make unique
- new Microsoft.Boogie.TypeVariableSeq(),
- new Microsoft.Boogie.VariableSeq(invars),
- new Microsoft.Boogie.VariableSeq(outvars),
- vseq,
- stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));
-
- impl.Proc = proc;
this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
+
} catch (TranslationException te) {
throw new NotImplementedException(te.ToString());
} catch {
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 02df9b32..1fefbe97 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -25,10 +25,12 @@ namespace BytecodeTranslator { get { return this.factory; }
}
readonly TraverserFactory factory;
+ public readonly IContractProvider ContractProvider;
- public Sink(TraverserFactory factory, HeapFactory heapFactory) {
+ public Sink(TraverserFactory factory, HeapFactory heapFactory, IContractProvider contractProvider) {
this.factory = factory;
var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?
+ this.ContractProvider = contractProvider;
if (this.TranslatedProgram == null)
this.TranslatedProgram = new Bpl.Program();
}
@@ -121,13 +123,160 @@ namespace BytecodeTranslator { return v;
}
/// <summary>
- /// The keys to the table are tuples of the containing type (its interned key) and the name of the field. That
- /// should uniquely identify each field.
+ /// The keys to the table are the interned key of the field.
/// </summary>
private Dictionary<uint, Bpl.Variable> declaredFields = new Dictionary<uint, Bpl.Variable>();
+ public Bpl.Procedure FindOrCreateProcedure(IMethodReference method, bool isStatic) {
+ Bpl.Procedure proc;
+ var key = method.InternedKey;
+ if (!this.declaredMethods.TryGetValue(key, out proc)) {
+ #region Create in- and out-parameters
+
+ int in_count = 0;
+ int out_count = 0;
+ MethodParameter mp;
+ var formalMap = new Dictionary<IParameterDefinition, MethodParameter>();
+ foreach (IParameterDefinition formal in method.Parameters) {
+
+ mp = new MethodParameter(formal);
+ if (mp.inParameterCopy != null) in_count++;
+ if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))
+ out_count++;
+ formalMap.Add(formal, mp);
+ }
+ this.FormalMap = formalMap;
+
+ #region Look for Returnvalue
+
+ if (method.Type.TypeCode != PrimitiveTypeCode.Void) {
+ Bpl.Type rettype = TranslationHelper.CciTypeToBoogie(method.Type);
+ out_count++;
+ this.RetVariable = new Bpl.Formal(method.Token(),
+ new Bpl.TypedIdent(method.Type.Token(),
+ "$result", rettype), false);
+ } else {
+ this.RetVariable = null;
+ }
+
+ #endregion
+
+ Bpl.Formal/*?*/ self = null;
+ #region Create 'this' parameter
+ if (!isStatic) {
+ in_count++;
+ Bpl.Type selftype = Bpl.Type.Int;
+ self = new Bpl.Formal(method.Token(),
+ new Bpl.TypedIdent(method.Type.Token(),
+ "this", selftype), true);
+ }
+ #endregion
+
+ Bpl.Variable[] invars = new Bpl.Formal[in_count];
+ Bpl.Variable[] outvars = new Bpl.Formal[out_count];
+
+ int i = 0;
+ int j = 0;
+
+ #region Add 'this' parameter as first in parameter
+ if (!isStatic)
+ invars[i++] = self;
+ #endregion
+
+ foreach (MethodParameter mparam in formalMap.Values) {
+ if (mparam.inParameterCopy != null) {
+ invars[i++] = mparam.inParameterCopy;
+ }
+ if (mparam.outParameterCopy != null) {
+ if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)
+ outvars[j++] = mparam.outParameterCopy;
+ }
+ }
+
+ #region add the returnvalue to out if there is one
+ if (this.RetVariable != null) outvars[j] = this.RetVariable;
+ #endregion
+
+ #endregion
+
+ #region Check The Method Contracts
+ Bpl.RequiresSeq boogiePrecondition = new Bpl.RequiresSeq();
+ Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();
+ Bpl.IdentifierExprSeq boogieModifies = new Bpl.IdentifierExprSeq();
+
+ IMethodContract contract = ContractProvider.GetMethodContractFor(method);
+
+ if (contract != null) {
+ try {
+ foreach (IPrecondition pre in contract.Preconditions) {
+ ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, null);
+ exptravers.Visit(pre.Condition); // TODO
+ // Todo: Deal with Descriptions
+
+
+ Bpl.Requires req
+ = new Bpl.Requires(pre.Token(),
+ false, exptravers.TranslatedExpressions.Pop(), "");
+ boogiePrecondition.Add(req);
+ }
+
+ foreach (IPostcondition post in contract.Postconditions) {
+ ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, null);
+
+ exptravers.Visit(post.Condition);
+ // Todo: Deal with Descriptions
+
+ Bpl.Ensures ens =
+ new Bpl.Ensures(post.Token(),
+ false, exptravers.TranslatedExpressions.Pop(), "");
+ boogiePostcondition.Add(ens);
+ }
+
+ foreach (IAddressableExpression mod in contract.ModifiedVariables) {
+ ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, null);
+ exptravers.Visit(mod);
+
+ Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
+
+ if (idexp == null) {
+ throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));
+ }
+ boogieModifies.Add(idexp);
+ }
+ } catch (TranslationException te) {
+ throw new NotImplementedException("Cannot Handle Errors in Method Contract: " + te.ToString());
+ } catch {
+ throw;
+ }
+ }
+
+ #endregion
+
+ string MethodName = TranslationHelper.CreateUniqueMethodName(method);
+
+ proc = new Bpl.Procedure(method.Token(),
+ MethodName,
+ new Bpl.TypeVariableSeq(),
+ new Bpl.VariableSeq(invars), // in
+ new Bpl.VariableSeq(outvars), // out
+ boogiePrecondition,
+ boogieModifies,
+ boogiePostcondition);
+
+
+ this.TranslatedProgram.TopLevelDeclarations.Add(proc);
+ this.declaredMethods.Add(key, proc);
+ }
+ return proc;
+ }
+ /// <summary>
+ /// The keys to the table are the interned key of the field.
+ /// </summary>
+ private Dictionary<uint, Bpl.Procedure> declaredMethods = new Dictionary<uint, Bpl.Procedure>();
+
public void BeginMethod() {
this.localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();
+ this.FormalMap = new Dictionary<IParameterDefinition, MethodParameter>();
}
public Dictionary<ITypeDefinition, HashSet<Bpl.Constant>> delegateTypeToDelegates =
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 707ab4e5..8667e1a0 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -99,6 +99,9 @@ namespace BytecodeTranslator { s = s.Replace(',', '$');
s = s.TrimEnd(')');
s = s.Replace("[]", "array");
+ s = s.Replace('<', '$');
+ s = s.Replace('>', '$');
+ s = s.Replace(':', '$');
return s;
}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index 6efe04e2..8162af9e 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -20,7 +20,7 @@ namespace BytecodeTranslator { public abstract class TraverserFactory {
public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider, PdbReader/*?*/ pdbReader, HeapFactory heapFactory)
{
- return new MetadataTraverser(new Sink(this, heapFactory), contractProvider, pdbReader);
+ return new MetadataTraverser(new Sink(this, heapFactory, contractProvider), pdbReader);
}
public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader) {
return new StatementTraverser(sink, pdbReader);
|