diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 7 | ||||
| -rw-r--r-- | Source/Core/VariableDependenceAnalyser.cs | 4 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 6 | ||||
| -rw-r--r-- | Source/Houdini/AnnotationDependenceAnalyser.cs | 5 | ||||
| -rw-r--r-- | Source/Houdini/StagedHoudini.cs | 19 |
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
|