summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/Inline.cs52
-rw-r--r--Source/Houdini/AbstractHoudini.cs2
-rw-r--r--Source/Houdini/Houdini.cs109
3 files changed, 115 insertions, 48 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 9af18158..47582868 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -35,6 +35,8 @@ namespace Microsoft.Boogie {
protected List<IdentifierExpr>/*!*/ newModifies;
+ protected string prefix;
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(program != null);
@@ -72,7 +74,7 @@ namespace Microsoft.Boogie {
currentId = 0;
inlinedProcLblMap.Add(procName, currentId);
}
- return "inline$" + procName + "$" + currentId;
+ return prefix + procName + "$" + currentId;
}
protected string GetProcVarName(string procName, string formalName) {
@@ -93,12 +95,58 @@ namespace Microsoft.Boogie {
this.inlineCallback = cb;
this.newLocalVars = new List<Variable>();
this.newModifies = new List<IdentifierExpr>();
+ this.prefix = "inline$";
+ }
+
+ protected static void ComputeInlinerPrefix(Implementation impl, Inliner inliner)
+ {
+ foreach (var v in impl.InParams)
+ {
+ if (!v.Name.StartsWith(inliner.prefix)) continue;
+ for (int i = inliner.prefix.Length; i < v.Name.Length; i++)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ if (v.Name[i] != '$') break;
+ }
+ if (inliner.prefix == v.Name)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ }
+ }
+ foreach (var v in impl.OutParams)
+ {
+ if (!v.Name.StartsWith(inliner.prefix)) continue;
+ for (int i = inliner.prefix.Length; i < v.Name.Length; i++)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ if (v.Name[i] != '$') break;
+ }
+ if (inliner.prefix == v.Name)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ }
+ }
+ foreach (var v in impl.LocVars)
+ {
+ if (!v.Name.StartsWith(inliner.prefix)) continue;
+ for (int i = inliner.prefix.Length; i < v.Name.Length; i++)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ if (v.Name[i] != '$') break;
+ }
+ if (inliner.prefix == v.Name)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ }
+ }
}
protected static void ProcessImplementation(Implementation impl, Inliner inliner) {
Contract.Requires(impl != null);
Contract.Requires(impl.Proc != null);
+ ComputeInlinerPrefix(impl, inliner);
+
inliner.newLocalVars.AddRange(impl.LocVars);
inliner.newModifies.AddRange(impl.Proc.Modifies);
@@ -466,7 +514,7 @@ namespace Microsoft.Boogie {
}
private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) {
- if (QKeyValue.FindBoolAttribute(ens.Attributes, "assume")) {
+ if (QKeyValue.FindBoolAttribute(ens.Attributes, "HoudiniAssume")) {
return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
} else if (ens.Free) {
return new AssumeCmd(ens.tok, Expr.True);
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 716456ea..49273f94 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -2412,7 +2412,7 @@ namespace Microsoft.Boogie.Houdini {
QKeyValue.FindStringAttribute(ens.Attributes, "post") == null)
.Iter(ens => nensures.Add(ens));
foreach (Ensures en in nensures)
- en.Attributes = removeAttr("assume", en.Attributes);
+ en.Attributes = removeAttr("HoudiniAssume", en.Attributes);
proc.Ensures = nensures;
}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 7dfa1bc7..d8adf7d3 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -294,10 +294,11 @@ namespace Microsoft.Boogie.Houdini {
}
public class InlineEnsuresVisitor : ReadOnlyVisitor {
- public override Ensures VisitEnsures(Ensures ensures) {
- ensures.Attributes = new QKeyValue(Token.NoToken, "assume", new List<object>(), ensures.Attributes);
- return base.VisitEnsures(ensures);
- }
+ public override Ensures VisitEnsures(Ensures ensures)
+ {
+ ensures.Attributes = new QKeyValue(Token.NoToken, "HoudiniAssume", new List<object>(), ensures.Attributes);
+ return base.VisitEnsures(ensures);
+ }
}
public class Houdini : ObservableHoudini {
@@ -325,54 +326,72 @@ namespace Microsoft.Boogie.Houdini {
Initialize(program, stats);
}
- protected void Initialize(Program program, HoudiniSession.HoudiniStatistics stats) {
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Collecting existential constants...");
- this.houdiniConstants = CollectExistentialConstants();
+ protected void Initialize(Program program, HoudiniSession.HoudiniStatistics stats)
+ {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Collecting existential constants...");
+ this.houdiniConstants = CollectExistentialConstants();
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Building call graph...");
- this.callGraph = Program.BuildCallGraph(program);
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Building call graph...");
+ this.callGraph = Program.BuildCallGraph(program);
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
- if (CommandLineOptions.Clo.HoudiniUseCrossDependencies) {
- if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
- this.crossDependencies = new CrossDependencies(this.houdiniConstants);
- this.crossDependencies.Visit(program);
- }
+ if (CommandLineOptions.Clo.HoudiniUseCrossDependencies)
+ {
+ if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
+ this.crossDependencies = new CrossDependencies(this.houdiniConstants);
+ this.crossDependencies.Visit(program);
+ }
- Inline();
+ Inline();
+ /*
+ {
+ int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ CommandLineOptions.Clo.PrintUnstructured = 1;
+ using (TokenTextWriter stream = new TokenTextWriter("houdini_inline.bpl"))
+ {
+ program.Emit(stream);
+ }
+ CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
+ */
- this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
- this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, taskID: GetTaskID());
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
+ this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, taskID: GetTaskID());
- vcgenFailures = new HashSet<Implementation>();
- Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Beginning VC generation for Houdini...");
- foreach (Implementation impl in callGraph.Nodes) {
- try {
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Generating VC for {0}", impl.Name);
- HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: GetTaskID());
- houdiniSessions.Add(impl, session);
- } catch (VCGenException) {
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("VC generation failed");
- vcgenFailures.Add(impl);
+ vcgenFailures = new HashSet<Implementation>();
+ Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Beginning VC generation for Houdini...");
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ try
+ {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Generating VC for {0}", impl.Name);
+ HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: GetTaskID());
+ houdiniSessions.Add(impl, session);
+ }
+ catch (VCGenException)
+ {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("VC generation failed");
+ vcgenFailures.Add(impl);
+ }
}
- }
- this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
+ this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
- if (CommandLineOptions.Clo.ExplainHoudini) {
- // Print results of ExplainHoudini to a dotty file
- explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
- explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
- foreach (var constant in houdiniConstants)
- explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
- explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
- }
+ if (CommandLineOptions.Clo.ExplainHoudini)
+ {
+ // Print results of ExplainHoudini to a dotty file
+ explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
+ explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
+ foreach (var constant in houdiniConstants)
+ explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
+ explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
+ }
}
protected void Inline() {
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 23:29:20 +0000