summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Ally Donaldson <unknown>2015-01-10 11:01:14 +0000
committerGravatar Ally Donaldson <unknown>2015-01-10 11:01:14 +0000
commit7b1b91e940fd8ec7ac60074c843eb08f5715bc91 (patch)
tree724d2b63de4490a0ed2c226cd021adcf85c00776 /Source
parentdfc5ba21c5da1c8c4133b4aa260a90dc1a9404f4 (diff)
Removed unnecessary stage-related attributes from candidate annotations.
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/Absy.cs7
-rw-r--r--Source/Core/VariableDependenceAnalyser.cs4
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs6
-rw-r--r--Source/Houdini/AnnotationDependenceAnalyser.cs5
-rw-r--r--Source/Houdini/StagedHoudini.cs19
5 files changed, 27 insertions, 14 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7622cbdf..2fd442d4 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1287,17 +1287,16 @@ namespace Microsoft.Boogie {
private int invariantGenerationCounter = 0;
- public Constant MakeExistentialBoolean(int StageId) {
+ public Constant MakeExistentialBoolean() {
Constant ExistentialBooleanConstant = new Constant(Token.NoToken, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);
invariantGenerationCounter++;
ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });
- ExistentialBooleanConstant.AddAttribute("stage_id", new object[] { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(StageId)) });
AddTopLevelDeclaration(ExistentialBooleanConstant);
return ExistentialBooleanConstant;
}
- public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null, int StageId = 0) {
- Constant ExistentialBooleanConstant = MakeExistentialBoolean(StageId);
+ public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null) {
+ Constant ExistentialBooleanConstant = MakeExistentialBoolean();
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);
PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));
if (tag != null)
diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs
index 70e33581..ab12a47e 100644
--- a/Source/Core/VariableDependenceAnalyser.cs
+++ b/Source/Core/VariableDependenceAnalyser.cs
@@ -429,7 +429,7 @@ namespace Microsoft.Boogie {
Dictionary<Implementation, Dictionary<Block, HashSet<Block>>> LocalCtrlDeps = new Dictionary<Implementation, Dictionary<Block, HashSet<Block>>>();
// Work out and union together local control dependences
- foreach (var Impl in prog.Implementations) {
+ foreach (var Impl in prog.NonInlinedImplementations()) {
Graph<Block> blockGraph = prog.ProcessLoops(Impl);
LocalCtrlDeps[Impl] = blockGraph.ControlDependence();
foreach (var KeyValue in LocalCtrlDeps[Impl]) {
@@ -440,7 +440,7 @@ namespace Microsoft.Boogie {
Graph<Implementation> callGraph = Program.BuildCallGraph(prog);
// Add inter-procedural control dependence nodes based on calls
- foreach (var Impl in prog.Implementations) {
+ foreach (var Impl in prog.NonInlinedImplementations()) {
foreach (var b in Impl.Blocks) {
foreach (var cmd in b.Cmds.OfType<CallCmd>()) {
var DirectCallee = GetImplementation(cmd.callee);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ae833dbf..90da808a 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1361,10 +1361,8 @@ namespace Microsoft.Boogie
private static PipelineOutcome RunStagedHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
{
Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
- // TODO - pass this in somewhere
-
- Houdini.StagedHoudini houdini = new Houdini.StagedHoudini(program, ProgramFromFile);
- Houdini.HoudiniOutcome outcome = houdini.PerformStagedHoudiniInference();
+ Houdini.StagedHoudini stagedHoudini = new Houdini.StagedHoudini(program, houdiniStats, ProgramFromFile);
+ Houdini.HoudiniOutcome outcome = stagedHoudini.PerformStagedHoudiniInference();
if (CommandLineOptions.Clo.PrintAssignment)
{
diff --git a/Source/Houdini/AnnotationDependenceAnalyser.cs b/Source/Houdini/AnnotationDependenceAnalyser.cs
index fd283f3e..7cb43fbd 100644
--- a/Source/Houdini/AnnotationDependenceAnalyser.cs
+++ b/Source/Houdini/AnnotationDependenceAnalyser.cs
@@ -436,8 +436,9 @@ namespace Microsoft.Boogie.Houdini {
if (NoStages())
{
- // TODO: need to figure out what to do here
- throw new NotImplementedException();
+ var TrivialGraph = new Graph<ScheduledStage>();
+ TrivialGraph.AddSource(new ScheduledStage(0, new HashSet<string>()));
+ return new StagedHoudiniPlan(TrivialGraph);
}
#region Assign annotations to stages at a given level of granularity
diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs
index 49482b3d..f5ddc92a 100644
--- a/Source/Houdini/StagedHoudini.cs
+++ b/Source/Houdini/StagedHoudini.cs
@@ -15,6 +15,7 @@ namespace Microsoft.Boogie.Houdini
{
private Program program;
+ private HoudiniSession.HoudiniStatistics houdiniStats;
private Func<string, Program> ProgramFromFile;
private StagedHoudiniPlan plan;
private List<Houdini>[] houdiniInstances;
@@ -23,8 +24,9 @@ namespace Microsoft.Boogie.Houdini
private const string tempFilename = "__stagedHoudiniTemp.bpl";
- public StagedHoudini(Program program, Func<string, Program> ProgramFromFile) {
+ public StagedHoudini(Program program, HoudiniSession.HoudiniStatistics houdiniStats, Func<string, Program> ProgramFromFile) {
this.program = program;
+ this.houdiniStats = houdiniStats;
this.ProgramFromFile = ProgramFromFile;
this.houdiniInstances = new List<Houdini>[CommandLineOptions.Clo.StagedHoudiniThreads];
for (int i = 0; i < CommandLineOptions.Clo.StagedHoudiniThreads; i++) {
@@ -40,16 +42,29 @@ namespace Microsoft.Boogie.Houdini
if(CommandLineOptions.Clo.DebugStagedHoudini) {
Console.WriteLine("Plan\n====\n");
- Console.WriteLine(this.plan);
+ if(plan == null) {
+ Console.WriteLine("No plan, as there were no stages");
+ } else {
+ Console.WriteLine(this.plan);
+ }
}
EmitProgram("staged.bpl");
}
}
+ private bool NoStages() {
+ return plan == null;
+ }
+
public HoudiniOutcome PerformStagedHoudiniInference()
{
+ if (NoStages()) {
+ Houdini houdini = new Houdini(program, houdiniStats);
+ return houdini.PerformHoudiniInference();
+ }
+
EmitProgram(tempFilename);
#region Prepare the tasks, but do not launch them