Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove the phone code, as agreed with Mike and Shaz. #5

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Remove the phone code, as agreed with Mike and Shaz. #5

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 2 additions & 52 deletions BCT.sln
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@

Microsoft Visual Studio Solution File, Format Version 12.00
# Visual Studio 2013
VisualStudioVersion = 12.0.21005.1
# Visual Studio 14
VisualStudioVersion = 14.0.25420.1
MinimumVisualStudioVersion = 10.0.40219.1
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BytecodeTranslator", "BytecodeTranslator\BytecodeTranslator.csproj", "{9C8E4D74-0251-479D-ADAC-A9A469977301}"
EndProject
Expand All @@ -28,11 +28,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractExtractor", "..\CCI
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ControlAndDataFlowGraph", "..\CCICodePlex\Ast\Metadata\Sources\ControlAndDataFlowGraph\ControlAndDataFlowGraph.csproj", "{2596EFB0-87AE-42CE-89EB-84F35D6350D2}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILGarbageCollect", "..\CCICodePlex\Ast\Metadata\Samples\ILGarbageCollect\ILGarbageCollect.csproj", "{60CD0C85-1E4A-4068-A4EC-D15B7981A908}"
ProjectSection(ProjectDependencies) = postProject
{6D83F687-ABB5-40B3-915E-CA53DA0EB7F3} = {6D83F687-ABB5-40B3-915E-CA53DA0EB7F3}
EndProjectSection
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILGenerator", "..\CCICodePlex\Ast\Metadata\Sources\ILGenerator\ILGenerator.csproj", "{08156C78-403A-4112-AD81-8646AC51CD2F}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "MetadataHelper", "..\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\MetadataHelper.csproj", "{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}"
Expand Down Expand Up @@ -459,51 +454,6 @@ Global
{2596EFB0-87AE-42CE-89EB-84F35D6350D2}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{2596EFB0-87AE-42CE-89EB-84F35D6350D2}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{2596EFB0-87AE-42CE-89EB-84F35D6350D2}.z3apidebug|x86.ActiveCfg = Debug|Any CPU
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|Any CPU.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|Mixed Platforms.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|Mixed Platforms.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|x86.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|x86.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|Any CPU.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|Mixed Platforms.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|Mixed Platforms.Build.0 = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|x86.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|x86.Build.0 = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|Any CPU.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|Mixed Platforms.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|x86.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|x86.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|Any CPU.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|Mixed Platforms.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|Mixed Platforms.Build.0 = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|x86.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|x86.Build.0 = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|Any CPU.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|Mixed Platforms.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|Mixed Platforms.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|x86.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|x86.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|Any CPU.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|Mixed Platforms.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|Mixed Platforms.Build.0 = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|x86.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|x86.Build.0 = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|Any CPU.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|Mixed Platforms.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|Mixed Platforms.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|x86.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|x86.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|Any CPU.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|Mixed Platforms.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|Mixed Platforms.Build.0 = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|x86.ActiveCfg = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|x86.Build.0 = Release|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|Any CPU.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|Mixed Platforms.Build.0 = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|x86.ActiveCfg = Debug|x86
{60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|x86.Build.0 = Debug|x86
{08156C78-403A-4112-AD81-8646AC51CD2F}.Checked|Any CPU.ActiveCfg = CompilerOnly|Any CPU
{08156C78-403A-4112-AD81-8646AC51CD2F}.Checked|Any CPU.Build.0 = CompilerOnly|Any CPU
{08156C78-403A-4112-AD81-8646AC51CD2F}.Checked|Mixed Platforms.ActiveCfg = CompilerOnly|Any CPU
Expand Down
14 changes: 0 additions & 14 deletions BytecodeTranslator/BytecodeTranslator.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,18 +103,11 @@
</ItemGroup>
<ItemGroup>
<Compile Include="ExceptionAnalysis.cs" />
<Compile Include="TranslationPlugins\PhoneTranslator\PhoneFeedbackPlugin.cs" />
<Compile Include="TranslationPlugins\Translators\BaseTranslator.cs" />
<Compile Include="CLRSemantics.cs" />
<Compile Include="Heap.cs" />
<Compile Include="HeapFactory.cs" />
<Compile Include="MetadataTraverser.cs" />
<Compile Include="Phone\PhoneBackKeyCallbackTraverser.cs" />
<Compile Include="Phone\PhoneCodeHelper.cs" />
<Compile Include="Phone\PhoneControlFeedbackTraverser.cs" />
<Compile Include="Phone\PhoneInitializationTraverser.cs" />
<Compile Include="Phone\PhoneMethodInliningTraverser.cs" />
<Compile Include="Phone\PhoneNavigationTraverser.cs" />
<Compile Include="Prelude.cs" />
<Compile Include="ExpressionTraverser.cs" />
<Compile Include="Sink.cs" />
Expand All @@ -125,10 +118,7 @@
<Compile Include="TranslationPlugins\BytecodeTranslator\BytecodeTranslatorPlugin.cs" />
<Compile Include="TranslationPlugins\ContractAwareTranslator.cs" />
<Compile Include="TranslationPlugins\ITranslationPlugin.cs" />
<Compile Include="TranslationPlugins\PhoneTranslator\PhoneInitializationPlugin.cs" />
<Compile Include="TranslationPlugins\Translator.cs" />
<Compile Include="TranslationPlugins\Translators\PhoneFeedbackTranslator.cs" />
<Compile Include="TranslationPlugins\Translators\PhoneInitializationTranslator.cs" />
<Compile Include="TraverserFactory.cs" />
<Compile Include="WholeProgram.cs" />
</ItemGroup>
Expand All @@ -148,10 +138,6 @@
<Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>
<Name>ParserHelper</Name>
</ProjectReference>
<ProjectReference Include="..\..\CCICodePlex\Ast\Metadata\Samples\ILGarbageCollect\ILGarbageCollect.csproj">
<Project>{60CD0C85-1E4A-4068-A4EC-D15B7981A908}</Project>
<Name>ILGarbageCollect</Name>
</ProjectReference>
<ProjectReference Include="..\..\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\MetadataHelper.csproj">
<Project>{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}</Project>
<Name>MetadataHelper</Name>
Expand Down
1 change: 0 additions & 1 deletion BytecodeTranslator/ExceptionAnalysis.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@
using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
using TranslationPlugins;
using BytecodeTranslator.Phone;


namespace BytecodeTranslator {
Expand Down
139 changes: 45 additions & 94 deletions BytecodeTranslator/ExpressionTraverser.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@
using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
using TranslationPlugins;
using BytecodeTranslator.Phone;


namespace BytecodeTranslator
Expand Down Expand Up @@ -697,79 +696,59 @@ public override void TraverseChildren(IMethodCall methodCall) {
var translateAsFunctionCall = proc is Bpl.Function;
bool isAsync = false;

// this code structure is quite chaotic, and some code needs to be evaluated regardless, hence the try-finally
try {
if (!translateAsFunctionCall) {
foreach (var a in resolvedMethod.Attributes) {
if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
isAsync = true;
}
if (!translateAsFunctionCall) {
foreach (var a in resolvedMethod.Attributes) {
if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
isAsync = true;
}
}
}

var deferringCtorCall = resolvedMethod.IsConstructor && methodCall.ThisArgument is IThisReference;
// REVIEW!! Ask Herman: is the above test enough? The following test is used in FindCtorCall.IsDeferringCtor,
// but it doesn't work when the type is a struct S because then "this" has a type of "&S".
//&& TypeHelper.TypesAreEquivalent(resolvedMethod.ContainingType, methodCall.ThisArgument.Type);
var deferringCtorCall = resolvedMethod.IsConstructor && methodCall.ThisArgument is IThisReference;
// REVIEW!! Ask Herman: is the above test enough? The following test is used in FindCtorCall.IsDeferringCtor,
// but it doesn't work when the type is a struct S because then "this" has a type of "&S".
//&& TypeHelper.TypesAreEquivalent(resolvedMethod.ContainingType, methodCall.ThisArgument.Type);

if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct && !deferringCtorCall) {
handleStructConstructorCall(methodCall, methodCallToken, inexpr, outvars, thisExpr, proc);
return;
}
if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct && !deferringCtorCall) {
handleStructConstructorCall(methodCall, methodCallToken, inexpr, outvars, thisExpr, proc);
return;
}

Bpl.CallCmd call;
bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
if (isEventAdd || isEventRemove) {
call = translateAddRemoveCall(methodCall, resolvedMethod, methodCallToken, inexpr, outvars, thisExpr, isEventAdd);
} else {
if (translateAsFunctionCall) {
var func = proc as Bpl.Function;
var exprSeq = new List<Bpl.Expr>();
foreach (var e in inexpr) {
exprSeq.Add(e);
}
var callFunction = new Bpl.NAryExpr(methodCallToken, new Bpl.FunctionCall(func), exprSeq);
this.TranslatedExpressions.Push(callFunction);
return;
} else {
EmitLineDirective(methodCallToken);
call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars);
call.IsAsync = isAsync;
this.StmtTraverser.StmtBuilder.Add(call);
Bpl.CallCmd call;
bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
if (isEventAdd || isEventRemove) {
call = translateAddRemoveCall(methodCall, resolvedMethod, methodCallToken, inexpr, outvars, thisExpr, isEventAdd);
} else {
if (translateAsFunctionCall) {
var func = proc as Bpl.Function;
var exprSeq = new List<Bpl.Expr>();
foreach (var e in inexpr) {
exprSeq.Add(e);
}
var callFunction = new Bpl.NAryExpr(methodCallToken, new Bpl.FunctionCall(func), exprSeq);
this.TranslatedExpressions.Push(callFunction);
return;
} else {
EmitLineDirective(methodCallToken);
call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars);
call.IsAsync = isAsync;
this.StmtTraverser.StmtBuilder.Add(call);
}
}

foreach (KeyValuePair<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> kv in toBoxed) {
var lhs = kv.Key;
var tuple = kv.Value;
var rhs = tuple.Item1;
Bpl.Expr fromUnion = this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs, tuple.Item2);
this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion));
}

if (this.sink.Options.modelExceptions == 2
|| (this.sink.Options.modelExceptions == 1 && this.sink.MethodThrowsExceptions(resolvedMethod))) {
Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));
this.StmtTraverser.RaiseException(expr);
}
} finally {
// TODO move away phone related code from the translation, it would be better to have 2 or more translation phases
if (PhoneCodeHelper.instance().PhonePlugin != null) {
if (PhoneCodeHelper.instance().PhoneNavigationToggled) {
if (PhoneCodeHelper.instance().isNavigationCall(methodCall)) {
Bpl.AssignCmd assignCmd = PhoneCodeHelper.instance().createBoogieNavigationUpdateCmd(sink);
this.StmtTraverser.StmtBuilder.Add(assignCmd);
}
}
foreach (KeyValuePair<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> kv in toBoxed) {
var lhs = kv.Key;
var tuple = kv.Value;
var rhs = tuple.Item1;
Bpl.Expr fromUnion = this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs, tuple.Item2);
this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion));
}

if (PhoneCodeHelper.instance().PhoneFeedbackToggled) {
if (PhoneCodeHelper.instance().isMethodKnownUIChanger(methodCall)) {
Bpl.AssumeCmd assumeFalse = new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False);
this.StmtTraverser.StmtBuilder.Add(assumeFalse);
}
}
}
if (this.sink.Options.modelExceptions == 2
|| (this.sink.Options.modelExceptions == 1 && this.sink.MethodThrowsExceptions(resolvedMethod))) {
Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));
this.StmtTraverser.RaiseException(expr);
}
}

Expand Down Expand Up @@ -991,35 +970,7 @@ public override void TraverseChildren(IAssignment assignment) {
Contract.Assert(TranslatedExpressions.Count == 0);
var tok = assignment.Token();

bool translationIntercepted= false;
ICompileTimeConstant constant= assignment.Source as ICompileTimeConstant;
// TODO move away phone related code from the translation, it would be better to have 2 or more translation phases
// NAVIGATION TODO maybe this will go away if I can handle it with stubs
if (PhoneCodeHelper.instance().PhonePlugin != null && PhoneCodeHelper.instance().PhoneNavigationToggled) {
IFieldReference target = assignment.Target.Definition as IFieldReference;
if (target != null && target.Name.Value == PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE) {
if (constant != null && constant.Type == sink.host.PlatformType.SystemString && constant.Value != null &&
constant.Value.Equals(PhoneCodeHelper.BOOGIE_DO_HAVOC_CURRENTURI)) {
TranslateHavocCurrentURI();
translationIntercepted = true;
}
StmtTraverser.StmtBuilder.Add(PhoneCodeHelper.instance().getAddNavigationCheck(sink));
}
}

if (!translationIntercepted)
TranslateAssignment(tok, assignment.Target.Definition, assignment.Target.Instance, assignment.Source);
}

/// <summary>
/// Patch, to account for URIs that cannot be tracked because of current dataflow restrictions
/// </summary>
private void TranslateHavocCurrentURI() {
// TODO move away phone related code from the translation, it would be better to have 2 or more translation phases
IMethodReference havocMethod= PhoneCodeHelper.instance().getUriHavocerMethod(sink);
Sink.ProcedureInfo procInfo= sink.FindOrCreateProcedure(havocMethod.ResolvedMethod);
Bpl.CallCmd havocCall = new Bpl.CallCmd(Bpl.Token.NoToken, procInfo.Decl.Name, new List<Bpl.Expr>(), new List<Bpl.IdentifierExpr>());
StmtTraverser.StmtBuilder.Add(havocCall);
TranslateAssignment(tok, assignment.Target.Definition, assignment.Target.Instance, assignment.Source);
}

/// <summary>
Expand Down
Loading