diff options
| -rw-r--r-- | Source/Core/Inline.cs | 75 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 24 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 59 | ||||
| -rw-r--r-- | Test/houdini/test10.bpl.expect | 14 |
4 files changed, 38 insertions, 134 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index fe61a765..d6707f1f 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -69,21 +69,14 @@ namespace Microsoft.Boogie { protected string GetInlinedProcLabel(string procName) {
Contract.Requires(procName != null);
Contract.Ensures(Contract.Result<string>() != null);
- int currentId;
- if (!inlinedProcLblMap.TryGetValue(procName, out currentId)) {
- currentId = 0;
- inlinedProcLblMap.Add(procName, currentId);
- }
- return prefix + procName + "$" + currentId;
+ return prefix + procName + "$" + inlinedProcLblMap[procName];
}
protected string GetProcVarName(string procName, string formalName) {
Contract.Requires(formalName != null);
Contract.Requires(procName != null);
Contract.Ensures(Contract.Result<string>() != null);
- string/*!*/ prefix = GetInlinedProcLabel(procName);
- Contract.Assert(prefix != null);
- return prefix + "$" + formalName;
+ return GetInlinedProcLabel(procName) + "$" + formalName;
}
public Inliner(Program program, InlineCallback cb, int inlineDepth) {
@@ -95,59 +88,51 @@ namespace Microsoft.Boogie { this.inlineCallback = cb;
this.newLocalVars = new List<Variable>();
this.newModifies = new List<IdentifierExpr>();
- this.prefix = "inline$";
+ this.prefix = null;
}
// This method updates inliner.prefix so that prepending it to any string is guaranteed
// not to create a conflict with any of the in/out/local variables of impl
- protected static void ComputeInlinerPrefix(Implementation impl, Inliner inliner)
+ protected void ComputePrefix(Program program, Implementation impl)
{
+ this.prefix = "inline$";
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 + "$";
- }
+ DistinguishPrefix(v);
}
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 + "$";
- }
+ DistinguishPrefix(v);
}
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 + "$";
- }
+ DistinguishPrefix(v);
+ }
+ foreach (var v in program.GlobalVariables())
+ {
+ DistinguishPrefix(v);
+ }
+ }
+
+ private void DistinguishPrefix(Variable v)
+ {
+ if (!v.Name.StartsWith(prefix)) return;
+ for (int i = prefix.Length; i < v.Name.Length; i++)
+ {
+ prefix = prefix + "$";
+ if (v.Name[i] != '$') break;
+ }
+ if (prefix == v.Name)
+ {
+ prefix = prefix + "$";
}
}
- protected static void ProcessImplementation(Implementation impl, Inliner inliner) {
+ protected static void ProcessImplementation(Program program, Implementation impl, Inliner inliner) {
Contract.Requires(impl != null);
Contract.Requires(impl.Proc != null);
- ComputeInlinerPrefix(impl, inliner);
+ inliner.ComputePrefix(program, impl);
inliner.newLocalVars.AddRange(impl.LocVars);
inliner.newModifies.AddRange(impl.Proc.Modifies);
@@ -179,14 +164,14 @@ namespace Microsoft.Boogie { Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Requires(impl.Proc != null);
- ProcessImplementation(impl, new Inliner(program, null, CommandLineOptions.Clo.InlineDepth));
+ ProcessImplementation(program, impl, new Inliner(program, null, CommandLineOptions.Clo.InlineDepth));
}
public static void ProcessImplementation(Program program, Implementation impl) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Requires(impl.Proc != null);
- ProcessImplementation(impl, new Inliner(program, null, -1));
+ ProcessImplementation(program, impl, new Inliner(program, null, -1));
}
protected void EmitImpl(Implementation impl) {
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 31b38e8a..d4466ca5 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -698,18 +698,6 @@ namespace Microsoft.Boogie.Houdini { foreach (Implementation impl in callGraph.Nodes)
{
- InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
- inlineRequiresVisitor.Visit(impl);
- }
-
- foreach (Implementation impl in callGraph.Nodes)
- {
- FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
- freeRequiresVisitor.Visit(impl);
- }
-
- foreach (Implementation impl in callGraph.Nodes)
- {
InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
inlineEnsuresVisitor.Visit(impl);
}
@@ -2513,18 +2501,6 @@ namespace Microsoft.Boogie.Houdini { foreach (Implementation impl in callGraph.Nodes)
{
- InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
- inlineRequiresVisitor.Visit(impl);
- }
-
- foreach (Implementation impl in callGraph.Nodes)
- {
- FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
- freeRequiresVisitor.Visit(impl);
- }
-
- foreach (Implementation impl in callGraph.Nodes)
- {
InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
inlineEnsuresVisitor.Visit(impl);
}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 6bb2d4db..e91d0528 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -246,53 +246,6 @@ namespace Microsoft.Boogie.Houdini { }
}
- public class InlineRequiresVisitor : StandardVisitor {
- public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
- List<Cmd> newCmdSeq = new List<Cmd>();
- for (int i = 0, n = cmdSeq.Count; i < n; i++) {
- Cmd cmd = cmdSeq[i];
- CallCmd callCmd = cmd as CallCmd;
- if (callCmd != null) {
- newCmdSeq.AddRange(InlineRequiresForCallCmd(callCmd));
- }
- else {
- newCmdSeq.Add((Cmd)this.Visit(cmd));
- }
- }
- return newCmdSeq;
- }
- private List<Cmd> InlineRequiresForCallCmd(CallCmd node) {
- Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
- for (int i = 0; i < node.Proc.InParams.Count; i++) {
- substMap.Add(node.Proc.InParams[i], node.Ins[i]);
- }
- Substitution substitution = Substituter.SubstitutionFromHashtable(substMap);
- List<Cmd> cmds = new List<Cmd>();
- foreach (Requires requires in node.Proc.Requires) {
- if (requires.Free) continue;
- Requires requiresCopy = new Requires(false, Substituter.Apply(substitution, requires.Condition));
- cmds.Add(new AssertRequiresCmd(node, requiresCopy));
- }
- cmds.Add(node);
- return cmds;
- }
- }
-
- public class FreeRequiresVisitor : StandardVisitor {
- public override Requires VisitRequires(Requires requires) {
- if (requires.Free)
- return base.VisitRequires(requires);
- else
- return new Requires(true, requires.Condition);
- }
-
- public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {
- node.Requires = base.VisitRequires(node.Requires);
- node.Expr = this.VisitExpr(node.Expr);
- return node;
- }
- }
-
public class InlineEnsuresVisitor : ReadOnlyVisitor {
public override Ensures VisitEnsures(Ensures ensures)
{
@@ -398,20 +351,10 @@ namespace Microsoft.Boogie.Houdini { }
protected void Inline() {
- if (CommandLineOptions.Clo.InlineDepth < 0)
+ if (CommandLineOptions.Clo.InlineDepth <= 0)
return;
foreach (Implementation impl in callGraph.Nodes) {
- InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
- inlineRequiresVisitor.Visit(impl);
- }
-
- foreach (Implementation impl in callGraph.Nodes) {
- FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
- freeRequiresVisitor.Visit(impl);
- }
-
- foreach (Implementation impl in callGraph.Nodes) {
InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
inlineEnsuresVisitor.Visit(impl);
}
diff --git a/Test/houdini/test10.bpl.expect b/Test/houdini/test10.bpl.expect index f6adc2b7..d6c787d1 100644 --- a/Test/houdini/test10.bpl.expect +++ b/Test/houdini/test10.bpl.expect @@ -1,7 +1,7 @@ -Assignment computed by Houdini: -b1 = True -b2 = True -b3 = True -b4 = True - -Boogie program verifier finished with 5 verified, 0 errors +Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = False
+b4 = True
+
+Boogie program verifier finished with 5 verified, 0 errors
|