diff options
| -rw-r--r-- | Source/Core/Absy.cs | 9 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 12 | ||||
| -rw-r--r-- | Source/Core/Inline.cs | 136 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 35 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 3 | ||||
| -rw-r--r-- | Test/inline/Answer | 19 | ||||
| -rw-r--r-- | Test/inline/expansion.bpl | 33 | ||||
| -rw-r--r-- | Test/inline/expansion2.bpl | 8 | ||||
| -rw-r--r-- | Test/inline/expansion3.bpl | 12 | ||||
| -rw-r--r-- | Test/inline/expansion4.bpl | 9 | ||||
| -rw-r--r-- | Test/inline/runtest.bat | 2 |
11 files changed, 33 insertions, 245 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 0b40c86e..8f51aac8 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -312,9 +312,6 @@ namespace Microsoft.Boogie { seeker.Visit(d);
}
}
-
- AxiomExpander expander = new AxiomExpander(this, tc);
- expander.CollectExpansions();
}
public void ComputeStronglyConnectedComponents() {
@@ -1796,13 +1793,7 @@ namespace Microsoft.Boogie { // the body is only set if the function is declared with {:inline}
public Expr Body;
- public List<Expansion/*!*/> expansions;
public bool doingExpansion;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(expansions, true));
- }
-
private bool neverTrigger;
private bool neverTriggerComputed;
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index de1fdb00..16b988c9 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1856,14 +1856,6 @@ namespace Microsoft.Boogie { one of them to keep; otherwise, Boogie ignore the :extern declaration
and keeps the other.
- ---- On axioms -------------------------------------------------------------
-
- {:inline true}
- Works on axiom of the form:
- (forall VARS :: f(VARS) = expr(VARS))
- Makes Boogie replace f(VARS) with expr(VARS) everywhere just before
- doing VC generation.
-
---- On implementations and procedures -------------------------------------
{:inline N}
@@ -1897,6 +1889,10 @@ namespace Microsoft.Boogie { {:bvbuiltin ""spec""}
Rewrite the function to built-in prover function symbol 'fn'.
+ {:inline}
+ {:inline true}
+ Expand function according to its definition before going to the prover.
+
{:never_pattern true}
Terms starting with this function symbol will never be
automatically selected as patterns. It does not prevent them
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 802fd390..d9c33bd4 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -601,140 +601,4 @@ namespace Microsoft.Boogie { }
}
} // end class CodeCopier
-
-
- public class AxiomExpander : Duplicator {
- readonly Program/*!*/ program;
- readonly TypecheckingContext/*!*/ tc;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(program != null);
- Contract.Invariant(tc != null);
- }
-
-
- public AxiomExpander(Program prog, TypecheckingContext t) {
- Contract.Requires(t != null);
- Contract.Requires(prog != null);
- program = prog;
- tc = t;
- }
-
- public void CollectExpansions() {
- foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- Axiom ax = decl as Axiom;
- if (ax != null) {
- bool expand = false;
- if (!ax.CheckBooleanAttribute("inline", ref expand)) {
- Error(decl.tok, "{:inline ...} expects either true or false as the argument");
- }
- if (expand) {
- AddExpansion(ax.Expr, ax.FindStringAttribute("ignore"));
- }
- }
- Function f = decl as Function;
- if (f != null && f.Body != null) {
- Variable[]/*!*/ formals = new Variable[f.InParams.Length];
- Contract.Assert(formals != null);
- for (int i = 0; i < formals.Length; ++i)
- formals[i] = f.InParams[i];
- AddExpansion(f, new Expansion(null, f.Body,
- new TypeVariableSeq(f.TypeParameters),
- formals));
- }
- }
- }
-
- void Error(IToken tok, string msg) {
- Contract.Requires(tok != null);
- tc.Error(tok, "expansion: " + msg);
- }
-
- void AddExpansion(Expr axiomBody, string ignore) {
- Contract.Requires(axiomBody != null);
- // it would be sooooooooo much easier with pattern matching
- ForallExpr all = axiomBody as ForallExpr;
- if (all != null) {
- NAryExpr nary = all.Body as NAryExpr;
- BinaryOperator bin = nary == null ? null : nary.Fun as BinaryOperator;
- //System.Console.WriteLine("{0} {1} {2}", nary==null, bin==null, bin==null?0 : bin.Op);
- if (nary != null && bin != null && (bin.Op == BinaryOperator.Opcode.Eq || bin.Op == BinaryOperator.Opcode.Iff)) {
-
- NAryExpr func = nary.Args[0] as NAryExpr;
- //System.Console.WriteLine("{0} {1}", func == null, func == null ? null : func.Fun.GetType());
- while (func != null && func.Fun is TypeCoercion)
- func = func.Args[0] as NAryExpr;
- if (func != null && func.Fun is FunctionCall) {
- Function fn = cce.NonNull((FunctionCall)func.Fun).Func;
- Expansion exp = new Expansion(ignore, cce.NonNull(nary.Args[1]),
- new TypeVariableSeq(),
- new Variable[func.Args.Length]);
- int pos = 0;
- HashSet<Declaration> parms = new HashSet<Declaration>();
- foreach (Expr/*!*/ e in func.Args) {
- Contract.Assert(e != null);
- IdentifierExpr id = e as IdentifierExpr;
- if (id == null) {
- Error(e.tok, "only identifiers supported as function arguments");
- return;
- }
- exp.formals[pos++] = id.Decl;
- if (parms.Contains(id.Decl)) {
- Error(all.tok, "an identifier was used more than once");
- return;
- }
- parms.Add(id.Decl);
- if (!all.Dummies.Has(id.Decl)) {
- Error(all.tok, "identifier was not quantified over");
- return;
- }
- }
- if (func.Args.Length != all.Dummies.Length) {
- Error(all.tok, "more variables quantified over, than used in function");
- return;
- }
-
- HashSet<TypeVariable/*!*/> typeVars = new HashSet<TypeVariable/*!*/>();
- foreach (TypeVariable/*!*/ v in cce.NonNull(func.TypeParameters).FormalTypeParams) {
- Contract.Assert(v != null);
- if (!func.TypeParameters[v].IsVariable) {
- Error(all.tok, "only identifiers supported as type parameters");
- return;
- }
- TypeVariable/*!*/ formal = func.TypeParameters[v].AsVariable;
- Contract.Assert(formal != null);
- exp.TypeParameters.Add(formal);
- if (typeVars.Contains(formal)) {
- Error(all.tok, "an identifier was used more than once");
- return;
- }
- typeVars.Add(formal);
- if (!all.TypeParameters.Has(formal)) {
- Error(all.tok, "identifier was not quantified over");
- return;
- }
- }
- if (((FunctionCall)func.Fun).Func.TypeParameters.Length != all.TypeParameters.Length) {
- Error(all.tok, "more variables quantified over, than used in function");
- return;
- }
- AddExpansion(fn, exp);
- return;
- }
- }
- }
-
- Error(axiomBody.tok, "axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))");
- }
-
- void AddExpansion(Function fn, Expansion x) {
- Contract.Requires(x != null);
- Contract.Requires(fn != null);
- if (fn.expansions == null) {
- fn.expansions = new List<Expansion/*!*/>();
- }
- fn.expansions.Add(x);
- }
- }
} // end namespace
\ No newline at end of file diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 4555f18c..4e9c5c10 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1086,7 +1086,7 @@ namespace Microsoft.Boogie.VCExprAST { return null;
}
- Expansion exp = FindExpansion(app.Func);
+ var exp = app.Func.Body;
if (exp == null)
return null;
@@ -1099,11 +1099,12 @@ namespace Microsoft.Boogie.VCExprAST { // first bind the formals to VCExpr variables, which are later
// substituted with the actual parameters
- for (int i = 0; i < exp.formals.Length; ++i)
- subst[BaseTranslator.BindVariable(cce.NonNull(exp.formals)[i])] = args[i];
+ var inParams = app.Func.InParams;
+ for (int i = 0; i < inParams.Length; ++i)
+ subst[BaseTranslator.BindVariable(inParams[i])] = args[i];
// recursively translate the body of the expansion
- translatedBody = BaseTranslator.Translate(exp.body);
+ translatedBody = BaseTranslator.Translate(exp);
} finally {
BaseTranslator.PopFormalsScope();
BaseTranslator.PopBoundVariableScope();
@@ -1111,32 +1112,12 @@ namespace Microsoft.Boogie.VCExprAST { }
// substitute the formals with the actual parameters in the body
- Contract.Assert(typeArgs.Count == exp.TypeParameters.Length);
+ var tparms = app.Func.TypeParameters;
+ Contract.Assert(typeArgs.Count == tparms.Length);
for (int i = 0; i < typeArgs.Count; ++i)
- subst[exp.TypeParameters[i]] = typeArgs[i];
+ subst[tparms[i]] = typeArgs[i];
SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
return substituter.Mutate(translatedBody, subst);
}
-
- private Expansion FindExpansion(Function func) {
- Contract.Requires(func != null);
- if (func.expansions == null)
- return null;
-
- Expansion exp = null;
- foreach (Expansion e in func.expansions) {
- Contract.Assert(e != null);
- if (e.ignore == null || !GenerationOptions.IsAnyProverCommandSupported(e.ignore)) {
- if (exp == null) {
- exp = e;
- } else {
- System.Console.WriteLine("*** more than one possible expansion for {0}", func);
- return null;
- }
- }
- }
-
- return exp;
- }
}
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index ff691828..1529db01 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -160,8 +160,7 @@ namespace Microsoft.Boogie { Contract.Assert(decl != null);
bool expand = false;
Axiom ax = decl as Axiom;
- decl.CheckBooleanAttribute("inline", ref expand);
- if (!expand && ax != null) {
+ if (ax != null) {
ctx.AddAxiom(ax, null);
}
}
diff --git a/Test/inline/Answer b/Test/inline/Answer index 72ba1170..ae632f79 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1448,26 +1448,15 @@ Execution trace: test5.bpl(34,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
--------------------- expansion.bpl --------------------
-expansion.bpl(29,14): Error: invalid type for argument 0 in application of foo1: bool (expected: int)
-expansion.bpl(13,16): Error: expansion: {:inline ...} expects either true or false as the argument
-expansion.bpl(14,22): Error: expansion: identifier was not quantified over
-expansion.bpl(15,22): Error: expansion: identifier was not quantified over
-expansion.bpl(16,22): Error: expansion: more variables quantified over, than used in function
-expansion.bpl(18,21): Error: expansion: axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))
-expansion.bpl(19,53): Error: expansion: only identifiers supported as function arguments
-expansion.bpl(33,22): Error: expansion: an identifier was used more than once
-8 type checking errors detected in expansion.bpl
-------------------- expansion3.bpl --------------------
*** detected expansion loop on foo3
*** detected expansion loop on foo3
*** detected expansion loop on foo3
-*** more than one possible expansion for x1
-expansion3.bpl(18,3): Error BP5001: This assertion might not hold.
-Execution trace:
- expansion3.bpl(18,3): anon0
-Boogie program verifier finished with 1 verified, 1 error
+Boogie program verifier finished with 1 verified, 0 errors
+-------------------- expansion4.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- Elevator.bpl --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
diff --git a/Test/inline/expansion.bpl b/Test/inline/expansion.bpl deleted file mode 100644 index 41acfb44..00000000 --- a/Test/inline/expansion.bpl +++ /dev/null @@ -1,33 +0,0 @@ -const q : int;
-const p : bool;
-function foo(x:int, y:bool) returns(bool);
-function foo1(x:int, y:bool) returns(bool);
-function foo2(x:int, y:bool) returns(bool);
-function foo3(x:int, y:bool) returns(bool);
-// OK
-axiom {:inline false} (forall x:int, y:bool :: foo(x,p) <==> x > 10 && y);
-axiom {:inline true} (forall x:int, y:bool :: foo1(x,y) == (x > 10 && y));
-axiom {:inline true} (forall x:int, y:bool :: foo2(x,y) == (q > 10 && y));
-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == foo3(x,y));
-// fail
-axiom {:inline 1} (forall x:int, y:bool :: foo(x,y) <==> x > 10 && y);
-axiom {:inline true} (forall x:int, y:bool :: foo(x,p) <==> x > 10 && y);
-axiom {:inline true} (forall y:bool :: foo(q,y) == (q > 10 && y));
-axiom {:inline true} (forall x:int, y:bool, z:int :: foo(x,y) == (q > 10 && y));
-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == (q > 10 && y));
-axiom {:inline true} true;
-axiom {:inline true} (forall y:bool, x:int :: foo3(x,true) == (q > 10 && y));
-
-
-procedure baz1()
-{
- assert foo3(1,true);
-}
-
-procedure baz2()
-{
- assert foo1(true,true);
-}
-
-function foo4(x:int, y:int) returns(bool);
-axiom {:inline true} (forall x:int,z:int :: foo4(x,x) == (x > 0));
diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl index fc14a0eb..b6ed19ed 100644 --- a/Test/inline/expansion2.bpl +++ b/Test/inline/expansion2.bpl @@ -1,7 +1,7 @@ -function xxgz(x:int) returns(bool);
-function xxf1(x:int,y:bool) returns(int);
-axiom {:inline true} (forall x:int :: xxgz(x) <==> x > 0);
-axiom {:inline true} (forall x:int, y:bool :: xxf1(x,y) == x+1);
+function {:inline true} xxgz(x:int) returns(bool)
+ { x > 0 }
+function {:inline true} xxf1(x:int,y:bool) returns(int)
+ { x + 1 }
axiom (forall z:int :: z>12 ==> xxgz(z));
axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0);
diff --git a/Test/inline/expansion3.bpl b/Test/inline/expansion3.bpl index 1fd3d853..2b1f0caa 100644 --- a/Test/inline/expansion3.bpl +++ b/Test/inline/expansion3.bpl @@ -1,5 +1,5 @@ -function foo3(x:int, y:bool) returns(bool);
-axiom {:inline true} (forall y:bool, x:int :: foo3(x,y) == foo3(x,y));
+function {:inline true} foo3(x:int, y:bool) returns(bool)
+ { foo3(x,y) }
axiom foo3(1,false);
@@ -9,11 +9,3 @@ procedure baz1() assume foo3(1,true);
}
-function x1(x:int) returns(bool);
-axiom {:inline true} (forall x:int :: x1(x) <==> x > 0);
-axiom {:inline true} (forall x:int :: x1(x) <==> x >= 1);
-
-procedure bar()
-{
- assert x1(3);
-}
diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl new file mode 100644 index 00000000..be11a391 --- /dev/null +++ b/Test/inline/expansion4.bpl @@ -0,0 +1,9 @@ +function foo(x:int) : int
+ { if x <= 0 then 1 else foo(x - 1) + 2 }
+
+procedure bar()
+{
+ assert foo(0) == 1;
+ assert foo(1) == 3;
+ assert foo(2) == 5;
+}
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index f04b84da..f56d55a0 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -13,7 +13,7 @@ for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do ( %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f
)
-for %%f in (test5.bpl expansion.bpl expansion3.bpl Elevator.bpl) do (
+for %%f in (test5.bpl expansion3.bpl expansion4.bpl Elevator.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
|