//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Cci;
using Microsoft.Cci.MetadataReader;
using Microsoft.Cci.MutableCodeModel;
using Microsoft.Cci.Contracts;
using Microsoft.Cci.ILToCodeModel;
using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
namespace BytecodeTranslator
{
public class StatementTraverser : BaseCodeTraverser {
public readonly TraverserFactory factory;
readonly Sink sink;
private readonly Bpl.Variable HeapVariable;
public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();
#region Constructors
public StatementTraverser(Sink sink) {
this.sink = sink;
this.factory = sink.Factory;
HeapVariable = sink.HeapVariable;
}
#endregion
#region Helper Methods
Bpl.Expr ExpressionFor(IExpression expression) {
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this);
etrav.Visit(expression);
Contract.Assert(etrav.TranslatedExpressions.Count == 1);
return etrav.TranslatedExpressions.Pop();
}
#endregion
public override void Visit(IBlockStatement block) {
Bpl.StmtListBuilder slb = new Bpl.StmtListBuilder();
foreach (IStatement st in block.Statements) {
this.Visit(st);
}
}
#region Basic Statements
public override void Visit(IAssertStatement assertStatement) {
StmtBuilder.Add(
new Bpl.AssertCmd(assertStatement.Token(), ExpressionFor(assertStatement.Condition))
);
}
public override void Visit(IAssumeStatement assumeStatement) {
StmtBuilder.Add(
new Bpl.AssertCmd(assumeStatement.Token(), ExpressionFor(assumeStatement.Condition))
);
}
///
///
///
/// (mschaef) Works, but still a stub
///
public override void Visit(IConditionalStatement conditionalStatement) {
StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink);
StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink);
ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, null);
condTraverser.Visit(conditionalStatement.Condition);
thenTraverser.Visit(conditionalStatement.TrueBranch);
elseTraverser.Visit(conditionalStatement.FalseBranch);
Bpl.IfCmd ifcmd = new Bpl.IfCmd(conditionalStatement.Token(),
condTraverser.TranslatedExpressions.Pop(),
thenTraverser.StmtBuilder.Collect(conditionalStatement.TrueBranch.Token()),
null,
elseTraverser.StmtBuilder.Collect(conditionalStatement.FalseBranch.Token())
);
StmtBuilder.Add(ifcmd);
}
///
///
///
///
/// TODO: might be wrong for the general case
public override void Visit(IExpressionStatement expressionStatement) {
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this);
etrav.Visit(expressionStatement.Expression);
}
///
///
///
/// (mschaef) Not Implemented
///
public override void Visit(IBreakStatement breakStatement) {
StmtBuilder.Add(new Bpl.BreakCmd(breakStatement.Token(), "I dont know"));
}
///
/// If the local declaration has an initial value, then generate the
/// statement "loc := e" from it. Otherwise ignore it.
///
public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {
if (localDeclarationStatement.InitialValue == null) return;
var loc = this.sink.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);
var tok = localDeclarationStatement.Token();
var e = ExpressionFor(localDeclarationStatement.InitialValue);
StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, loc), e));
return;
}
///
///
///
/// (mschaef) not implemented
///
public override void Visit(IReturnStatement returnStatement) {
Bpl.IToken tok = returnStatement.Token();
if (returnStatement.Expression != null) {
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this);
etrav.Visit(returnStatement.Expression);
if (this.sink.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {
throw new TranslationException(String.Format("{0} returns a value that is not supported by the function", returnStatement.ToString()));
}
StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
new Bpl.IdentifierExpr(tok, this.sink.RetVariable), etrav.TranslatedExpressions.Pop()));
}
StmtBuilder.Add(new Bpl.ReturnCmd(returnStatement.Token()));
}
#endregion
#region Goto and Labels
///
///
///
/// STUB
///
public override void Visit(IGotoStatement gotoStatement) {
String[] target = new String[1] { gotoStatement.TargetStatement.Label.Value };
Bpl.GotoCmd gotocmd = new Microsoft.Boogie.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target));
StmtBuilder.Add(gotocmd);
}
///
///
///
/// (mschaef) not sure if there is more work to do
///
public override void Visit(ILabeledStatement labeledStatement) {
StmtBuilder.AddLabelCmd(labeledStatement.Label.Value);
base.Visit(labeledStatement.Statement);
}
#endregion
#region Looping Statements
public override void Visit(IWhileDoStatement whileDoStatement) {
throw new NotImplementedException("While Statements are not implemented");
}
#endregion
}
}