diff options
| -rw-r--r-- | Source/Core/AbsyQuant.cs | 8 | ||||
| -rw-r--r-- | Source/Core/BoogiePL.atg | 2 | ||||
| -rw-r--r-- | Source/Core/Inline.cs | 39 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 2 | ||||
| -rw-r--r-- | Test/inline/Answer | 40 |
5 files changed, 62 insertions, 29 deletions
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 0f29c9a0..cae8bd92 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -533,6 +533,13 @@ namespace Microsoft.Boogie { return l.asBigNum.ToIntSafe;
return defl;
}
+
+ public override Absy Clone() {
+ List<object> newParams = new List<object>();
+ foreach (object o in Params)
+ newParams.Add(o);
+ return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone());
+ }
}
public class Trigger : Absy {
@@ -546,7 +553,6 @@ namespace Microsoft.Boogie { Contract.Invariant(Pos || Tr.Length == 1);
}
-
public Trigger Next;
public Trigger(IToken tok, bool pos, ExprSeq tr)
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 7519fb4c..645cdee5 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -587,7 +587,7 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl> (.
// here we attach kv only to the Procedure, not its implementation
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
.)
)
(. proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); .)
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index adc7e2f0..c9f6445c 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -388,6 +388,27 @@ namespace Microsoft.Boogie { codeCopier.OldSubst = null;
}
+ private Cmd InlinedRequires(Implementation impl, CallCmd callCmd, Requires req) {
+ Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
+ if (req.Free)
+ reqCopy.Condition = Expr.True;
+ else
+ reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
+ AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
+ a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
+ return a;
+ }
+
+ private Cmd InlinedEnsures(Implementation impl, CallCmd callCmd, Ensures ens) {
+ if (impl.FindExprAttribute("inline") != null && !ens.Free) {
+ Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
+ ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
+ return new AssertEnsuresCmd(ensCopy);
+ }
+ else {
+ return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
+ }
+ }
// result[0] is the entry block
protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {
@@ -418,17 +439,20 @@ namespace Microsoft.Boogie { inCmds.Add(cmd);
}
- // inject non-free requires
+ // inject requires
for (int i = 0; i < proc.Requires.Length; i++) {
Requires/*!*/ req = cce.NonNull(proc.Requires[i]);
+ inCmds.Add(InlinedRequires(impl, callCmd, req));
+ /*
if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {
- Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
+ Requires reqCopy = (Requires)cce.NonNull(req.Clone());
reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
- AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
+ AssertCmd a = new AssertRequiresCmd(callCmd, reqCopy);
Contract.Assert(a != null);
a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
inCmds.Add(a);
}
+ */
}
VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);
@@ -483,16 +507,19 @@ namespace Microsoft.Boogie { // create out block
CmdSeq outCmds = new CmdSeq();
- // inject non-free ensures
+ // inject ensures
for (int i = 0; i < proc.Ensures.Length; i++) {
Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);
+ outCmds.Add(InlinedEnsures(impl, callCmd, ens));
+ /*
if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {
- Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
+ Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());
ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
- AssertCmd/*!*/ a = new AssertEnsuresCmd(ensCopy);
+ AssertCmd a = new AssertEnsuresCmd(ensCopy);
Contract.Assert(a != null);
outCmds.Add(a);
}
+ */
}
// assign out params
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 34f43896..5bfbbfc2 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -503,7 +503,7 @@ private class BvBounds : Expr { }
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
+ Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
} else SynErr(91);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
diff --git a/Test/inline/Answer b/Test/inline/Answer index 2c29ab0b..d7e7edbe 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -32,7 +32,7 @@ procedure {:inline 1} incdec(x: int, y: int) returns (z: int); -implementation incdec(x: int, y: int) returns (z: int)
+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
{
anon0:
@@ -49,7 +49,7 @@ procedure {:inline 1} inc(x: int, i: int) returns (y: int); -implementation inc(x: int, i: int) returns (y: int)
+implementation {:inline 1} inc(x: int, i: int) returns (y: int)
{
anon0:
@@ -65,7 +65,7 @@ procedure {:inline 1} dec(x: int, i: int) returns (y: int); -implementation dec(x: int, i: int) returns (y: int)
+implementation {:inline 1} dec(x: int, i: int) returns (y: int)
{
anon0:
@@ -160,7 +160,7 @@ procedure {:inline 1} incdec(x: int, y: int) returns (z: int); ensures z == x + 1 - y;
-implementation incdec(x: int, y: int) returns (z: int)
+implementation {:inline 1} incdec(x: int, y: int) returns (z: int)
{
var inline$dec$0$x: int;
var inline$dec$0$i: int;
@@ -220,7 +220,7 @@ procedure {:inline 1} increase(i: int) returns (k: int); -implementation increase(i: int) returns (k: int)
+implementation {:inline 1} increase(i: int) returns (k: int)
{
var j: int;
@@ -298,7 +298,7 @@ procedure {:inline 3} recursive(x: int) returns (y: int); -implementation recursive(x: int) returns (y: int)
+implementation {:inline 3} recursive(x: int) returns (y: int)
{
var k: int;
@@ -421,7 +421,7 @@ after inlining procedure calls procedure {:inline 3} recursive(x: int) returns (y: int);
-implementation recursive(x: int) returns (y: int)
+implementation {:inline 3} recursive(x: int) returns (y: int)
{
var k: int;
var inline$recursive$0$k: int;
@@ -560,7 +560,7 @@ procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, fo -implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
{
var i: int;
var b: bool;
@@ -606,7 +606,7 @@ procedure {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool); -implementation check(A: [int]int, i: int, c: int) returns (ret: bool)
+implementation {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool)
{
anon0:
@@ -746,7 +746,7 @@ after inlining procedure calls procedure {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool);
-implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
+implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: int, found: bool)
{
var i: int;
var b: bool;
@@ -866,7 +866,7 @@ procedure {:inline 2} foo(); -implementation foo()
+implementation {:inline 2} foo()
{
anon0:
@@ -882,7 +882,7 @@ procedure {:inline 2} foo1(); -implementation foo1()
+implementation {:inline 2} foo1()
{
anon0:
@@ -898,7 +898,7 @@ procedure {:inline 2} foo2(); -implementation foo2()
+implementation {:inline 2} foo2()
{
anon0:
@@ -914,7 +914,7 @@ procedure {:inline 2} foo3(); -implementation foo3()
+implementation {:inline 2} foo3()
{
anon0:
@@ -947,7 +947,7 @@ procedure {:inline 2} foo(); modifies x;
-implementation foo()
+implementation {:inline 2} foo()
{
var inline$foo$0$x: int;
var inline$foo$1$x: int;
@@ -992,7 +992,7 @@ procedure {:inline 2} foo1(); modifies x;
-implementation foo1()
+implementation {:inline 2} foo1()
{
var inline$foo2$0$x: int;
var inline$foo3$0$x: int;
@@ -1097,7 +1097,7 @@ procedure {:inline 2} foo2(); modifies x;
-implementation foo2()
+implementation {:inline 2} foo2()
{
var inline$foo3$0$x: int;
var inline$foo1$0$x: int;
@@ -1202,7 +1202,7 @@ procedure {:inline 2} foo3(); modifies x;
-implementation foo3()
+implementation {:inline 2} foo3()
{
var inline$foo1$0$x: int;
var inline$foo2$0$x: int;
@@ -1532,7 +1532,7 @@ procedure {:inline 1} foo(); -implementation foo()
+implementation {:inline 1} foo()
{
anon0:
@@ -1605,7 +1605,7 @@ procedure {:inline 1} foo(); modifies g;
-implementation foo()
+implementation {:inline 1} foo()
{
var inline$bar$0$g: int;
|