From bed18114957f4e873e5055b93572a07c10e776fa Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Thu, 27 Oct 2011 19:12:06 -0700 Subject: Boogie: Get rid of {:inline} attributes on axioms --- Source/Core/Absy.cs | 9 --- Source/Core/CommandLineOptions.cs | 12 ++-- Source/Core/Inline.cs | 136 -------------------------------------- 3 files changed, 4 insertions(+), 153 deletions(-) (limited to 'Source/Core') 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 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 parms = new HashSet(); - 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 typeVars = new HashSet(); - 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(); - } - fn.expansions.Add(x); - } - } } // end namespace \ No newline at end of file -- cgit v1.2.3