diff options
| -rw-r--r-- | Source/Core/Duplicator.ssc | 42 | ||||
| -rw-r--r-- | Source/Core/Inline.ssc | 209 | ||||
| -rw-r--r-- | Test/inline/Answer | 15 | ||||
| -rw-r--r-- | Test/inline/test5.bpl | 36 |
4 files changed, 109 insertions, 193 deletions
diff --git a/Source/Core/Duplicator.ssc b/Source/Core/Duplicator.ssc index f3330739..08577400 100644 --- a/Source/Core/Duplicator.ssc +++ b/Source/Core/Duplicator.ssc @@ -29,7 +29,7 @@ namespace Microsoft.Boogie AssignCmd clone = (AssignCmd)node.Clone();
clone.Lhss = new List<AssignLhs!>(clone.Lhss);
clone.Rhss = new List<Expr!>(clone.Rhss);
- return base.VisitAssignCmd (clone);
+ return base.VisitAssignCmd(clone);
}
public override Cmd! VisitAssumeCmd(AssumeCmd! node)
{
@@ -67,10 +67,16 @@ namespace Microsoft.Boogie }
public override Cmd! VisitCallCmd(CallCmd! node)
{
- CallCmd! newNode = (CallCmd)node.Clone();
- newNode.Ins = new List<Expr> (node.Ins);
- newNode.Outs = new List<IdentifierExpr> (node.Outs);
- return base.VisitCallCmd (node);
+ CallCmd! clone = (CallCmd)node.Clone();
+ clone.Ins = new List<Expr>(clone.Ins);
+ clone.Outs = new List<IdentifierExpr>(clone.Outs);
+ return base.VisitCallCmd(clone);
+ }
+ public override Cmd! VisitCallForallCmd(CallForallCmd! node)
+ {
+ CallForallCmd! clone = (CallForallCmd)node.Clone();
+ clone.Ins = new List<Expr>(clone.Ins);
+ return base.VisitCallForallCmd(clone);
}
public override Choice! VisitChoice(Choice! node)
{
@@ -159,7 +165,9 @@ namespace Microsoft.Boogie }
public override AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)
{
- return base.VisitMapAssignLhs ((MapAssignLhs)node.Clone());
+ MapAssignLhs clone = (MapAssignLhs)node.Clone();
+ clone.Indexes = new List<Expr!>(clone.Indexes);
+ return base.VisitMapAssignLhs(clone);
}
public override MapType! VisitMapType(MapType! node)
{
@@ -285,6 +293,16 @@ namespace Microsoft.Boogie }
/// <summary>
+ /// Apply a substitution to a command. Any variables not in domain(subst)
+ /// is not changed. The substitutions applies within the "old", but the "old"
+ /// expression remains.
+ /// </summary>
+ public static Cmd! Apply(Substitution! subst, Cmd! cmd)
+ {
+ return (Cmd) new NormalSubstituter(subst).Visit(cmd);
+ }
+
+ /// <summary>
/// Apply a substitution to an expression replacing "old" expressions.
/// Outside "old" expressions, the substitution "always" is applied; any variable not in
/// domain(always) is not changed. Inside "old" expressions, apply map "oldExpr" to
@@ -296,6 +314,18 @@ namespace Microsoft.Boogie return (Expr) new ReplacingOldSubstituter(always, forold).Visit(expr);
}
+ /// <summary>
+ /// Apply a substitution to a command replacing "old" expressions.
+ /// Outside "old" expressions, the substitution "always" is applied; any variable not in
+ /// domain(always) is not changed. Inside "old" expressions, apply map "oldExpr" to
+ /// variables in domain(oldExpr), apply map "always" to variables in
+ /// domain(always)-domain(oldExpr), and leave variable unchanged otherwise.
+ /// </summary>
+ public static Cmd! ApplyReplacingOldExprs(Substitution! always, Substitution! forold, Cmd! cmd)
+ {
+ return (Cmd) new ReplacingOldSubstituter(always, forold).Visit(cmd);
+ }
+
private sealed class NormalSubstituter : Duplicator
{
private readonly Substitution! subst;
diff --git a/Source/Core/Inline.ssc b/Source/Core/Inline.ssc index 931c35eb..5c9d18fb 100644 --- a/Source/Core/Inline.ssc +++ b/Source/Core/Inline.ssc @@ -386,19 +386,19 @@ namespace Microsoft.Boogie { }
codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap);
- codeCopier.SubstForOld = Substituter.SubstitutionFromHashtable(substMapOld);
+ codeCopier.OldSubst = Substituter.SubstitutionFromHashtable(substMapOld);
}
protected void EndInline() {
codeCopier.Subst = null;
- codeCopier.SubstForOld = null;
+ codeCopier.OldSubst = null;
}
// result[0] is the entry block
protected List<Block!>! CreateInlinedBlocks(CallCmd! callCmd, Procedure! proc, Implementation! impl, string! nextBlockLabel)
requires (codeCopier.Subst != null);
- requires (codeCopier.SubstForOld != null);
+ requires (codeCopier.OldSubst != null);
{
List<Block!>! implBlocks = (!)impl.OriginalBlocks;
@@ -461,7 +461,7 @@ namespace Microsoft.Boogie { foreach (IdentifierExpr! mie in proc.Modifies)
{
Variable! mvar = (!) mie.Decl;
- AssignCmd assign = Cmd.SimpleAssign(impl.tok, (IdentifierExpr) (!) codeCopier.SubstForOld(mvar), mie);
+ AssignCmd assign = Cmd.SimpleAssign(impl.tok, (IdentifierExpr) (!) codeCopier.OldSubst(mvar), mie);
inCmds.Add(assign);
}
@@ -562,176 +562,29 @@ namespace Microsoft.Boogie { public class CodeCopier
{
-
- private DefaultDuplicator! dupl;
-
- private sealed class DefaultDuplicator : Duplicator
- {
- public Substitution subst;
- public Substitution oldSubst;
- private bool insideOldExpr = false;
- public DefaultDuplicator(Substitution subst, Substitution oldSubst) {
- this.subst = subst;
- this.oldSubst = oldSubst;
- base();
- }
- public override Cmd! VisitAssumeCmd(AssumeCmd! node)
- {
- return new AssumeCmd(node.tok, VisitExpr(node.Expr));
- }
- public override Cmd! VisitAssertCmd(AssertCmd! node)
- {
- return new AssertCmd(node.tok, VisitExpr(node.Expr));
- }
- public override Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
- {
- return new AssertRequiresCmd((CallCmd)VisitCallCmd(node.Call), VisitRequires(node.Requires));
- }
- public override Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
- {
- return new AssertEnsuresCmd(VisitEnsures(node.Ensures));
- }
-
- public override Cmd! VisitCallCmd(CallCmd! node)
- {
- List<Expr>! newIns = new List<Expr> ();
- List<IdentifierExpr>! newOuts = new List<IdentifierExpr> ();
- foreach (Expr e in node.Ins)
- newIns.Add(e == null ? null : this.VisitExpr(e));
- foreach (IdentifierExpr e in node.Outs)
- newOuts.Add(e == null ? null : (IdentifierExpr)this.VisitIdentifierExpr(e));
+ public Substitution Subst;
+ public Substitution OldSubst;
- CallCmd! newCmd = new CallCmd(node.tok, ((!)node.Proc).Name, newIns, newOuts);
- newCmd.Proc = node.Proc;
- return newCmd;
- }
- public override Expr! VisitIdentifierExpr(IdentifierExpr! node)
- {
- Expr e = null;
- if(insideOldExpr && oldSubst != null) {
- e = oldSubst((!)node.Decl);
- }
- if(e == null) {
- if(subst != null) {
- e = subst((!)node.Decl);
- return e == null ? base.VisitIdentifierExpr(node) : e;
- } else {
- return base.VisitIdentifierExpr(node);
- }
- }
- return e;
- }
- public override Expr! VisitOldExpr(OldExpr! node)
- {
- if(this.oldSubst != null) {
- bool previouslyInOld = insideOldExpr;
- insideOldExpr = true;
- Expr! e = (Expr!)this.Visit(node.Expr);
- insideOldExpr = previouslyInOld;
- return e;
- } else {
- return base.VisitOldExpr(node);
- }
- }
- }
-
public CodeCopier(Hashtable! substMap) {
- this.dupl = new DefaultDuplicator(Substituter.SubstitutionFromHashtable(substMap), null);
+ Subst = Substituter.SubstitutionFromHashtable(substMap);
}
public CodeCopier(Hashtable! substMap, Hashtable! oldSubstMap) {
- this.dupl = new DefaultDuplicator(Substituter.SubstitutionFromHashtable(substMap), Substituter.SubstitutionFromHashtable(oldSubstMap));
+ Subst = Substituter.SubstitutionFromHashtable(substMap);
+ OldSubst = Substituter.SubstitutionFromHashtable(oldSubstMap);
}
public CodeCopier() {
- this.dupl = new DefaultDuplicator(null, null);
- }
-
- public Substitution Subst {
- set {
- this.dupl.subst = value;
- }
- get {
- return this.dupl.subst;
- }
- }
-
- public Substitution SubstForOld {
- set {
- this.dupl.oldSubst = value;
- }
- get {
- return this.dupl.oldSubst;
- }
- }
-
- public Duplicator! Dupl {
- get {
- return this.dupl;
- }
- }
-
- public List<Block!>! CopyBlocks(List<Block!>! blocks) {
-
- List<Block!>! newBlocks = new List<Block!>();
-
- foreach(Block block in blocks) {
- Block newBlock = CopyBlock(block);
- newBlocks.Add(newBlock);
- }
-
- return newBlocks;
- }
-
- public List<Block!>! CopyBlocks(List<Block!>! blocks, string! prefix) {
-
- List<Block!>! newBlocks = new List<Block!>();
-
- foreach(Block block in blocks) {
- Block newBlock = CopyBlock(block, prefix);
- newBlocks.Add(newBlock);
- }
-
- return newBlocks;
- }
-
-
- #region CopyBlock
- public Block! CopyBlock(Block! block) {
-
- assert(block.TransferCmd != null);
- Block newBlock = new Block(block.tok, block.Label, CopyCmdSeq(block.Cmds), CopyTransferCmd(block.TransferCmd));
-
- return newBlock;
-
}
- public Block! CopyBlock(Block! block, string! prefix) {
-
- assert(block.TransferCmd != null);
- Block newBlock = new Block(block.tok, prefix + "$" + block.Label, CopyCmdSeq(block.Cmds), CopyTransferCmd(block.TransferCmd));
-
- return newBlock;
-
- }
- #endregion
-
- #region CopyCmdSeq
public CmdSeq! CopyCmdSeq(CmdSeq! cmds) {
-
CmdSeq newCmds = new CmdSeq();
-
- for (int i = 0; i < cmds.Length; ++i) {
- newCmds.Add(CopyCmd(cmds[i]));
+ foreach (Cmd! cmd in cmds) {
+ newCmds.Add(CopyCmd(cmd));
}
-
return newCmds;
-
}
- #endregion
-
- #region CopyTransferCmd
public TransferCmd! CopyTransferCmd(TransferCmd! cmd) {
TransferCmd transferCmd;
GotoCmd gotocmd = cmd as GotoCmd;
@@ -746,39 +599,25 @@ namespace Microsoft.Boogie { return transferCmd;
}
- public TransferCmd! CopyTransferCmd(TransferCmd! cmd, string! prefix) {
- TransferCmd transferCmd;
- GotoCmd gotocmd = cmd as GotoCmd;
- if(gotocmd != null) {
- assert(gotocmd.labelNames != null);
- StringSeq labels = new StringSeq();
- foreach(string label in gotocmd.labelNames) {
- labels.Add(prefix + "$" + label);
- }
- transferCmd = new GotoCmd(cmd.tok, labels);
+ public Cmd! CopyCmd(Cmd! cmd) {
+ if (Subst == null) {
+ return cmd;
+ } else if (OldSubst == null) {
+ return Substituter.Apply(Subst, cmd);
} else {
- transferCmd = new ReturnCmd(cmd.tok);
+ return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, cmd);
}
- return transferCmd;
}
- #endregion
-
-
- #region CopyCmd
- public Cmd! CopyCmd(Cmd! cmd) {
- Cmd newCmd = (Cmd) Dupl.Visit(cmd);
- return newCmd;
- }
- #endregion
-
- #region CopyExpr
public Expr! CopyExpr(Expr! expr) {
- Expr newExpr = (Expr) Dupl.Visit(expr);
- return newExpr;
+ if (Subst == null) {
+ return expr;
+ } else if (OldSubst == null) {
+ return Substituter.Apply(Subst, expr);
+ } else {
+ return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, expr);
+ }
}
- #endregion
-
} // end class CodeCopier
diff --git a/Test/inline/Answer b/Test/inline/Answer index 62d9b677..43ec6740 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -881,8 +881,19 @@ Execution trace: Boogie program verifier finished with 0 verified, 4 errors
-------------------- test5.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
+test5.bpl(37,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ test5.bpl(34,10): anon0
+ test5.bpl(25,23): inline$P$0$Entry
+ test5.bpl(28,10): inline$P$0$anon0
+ test5.bpl(25,23): inline$P$0$Return
+ test5.bpl(34,10): anon0$1
+ test5.bpl(25,23): inline$P$1$Entry
+ test5.bpl(28,10): inline$P$1$anon0
+ test5.bpl(25,23): inline$P$1$Return
+ test5.bpl(34,10): anon0$2
+
+Boogie program verifier finished with 3 verified, 1 error
-------------------- test6.bpl --------------------
test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
test6.bpl(15,22): Error: the inlined procedure is recursive, call stack: foo2 -> foo3 -> foo1 -> foo2
diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl index 0132f60a..629cb04c 100644 --- a/Test/inline/test5.bpl +++ b/Test/inline/test5.bpl @@ -18,3 +18,39 @@ procedure bar() assert x == 5;
}
+// -------------------------------------------------
+
+var Mem : [int]int;
+
+procedure {:inline 1} P(x:int)
+ modifies Mem;
+{
+ Mem[x] := 1;
+}
+
+procedure mainA()
+ modifies Mem;
+{
+ Mem[1] := 0;
+ call P(0);
+ call P(1);
+ assert Mem[1] == 0; // error
+}
+
+procedure mainB()
+ modifies Mem;
+{
+ Mem[1] := 0;
+ call P(0);
+ call P(1);
+ assert Mem[1] == 1; // good
+}
+
+procedure mainC()
+ modifies Mem;
+{
+ Mem[1] := 0;
+ call P(0);
+ call P(1);
+ assert Mem[1] == 1; // good
+}
|