From ed83becd12d7079e6ce2853fbebace20b1e7df5a Mon Sep 17 00:00:00 2001 From: boehmes Date: Thu, 27 Sep 2012 17:13:40 +0200 Subject: Removed AIFramework from Boogie -- use native trivial or native interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped. --- Source/AbsInt/AbsInt.csproj | 7 - Source/AbsInt/AbstractInterpretation.cs | 916 ----------------------------- Source/AbsInt/ExprFactories.cs | 275 --------- Source/AbsInt/LoopInvariantsOnDemand.cs | 84 --- Source/AbsInt/NativeLattice.cs | 20 +- Source/Boogie.sln | 27 - Source/BoogieDriver/BoogieDriver.cs | 11 +- Source/BoogieDriver/BoogieDriver.csproj | 4 - Source/Core/Absy.cs | 202 +------ Source/Core/AbsyCmd.cs | 14 - Source/Core/AbsyExpr.cs | 613 +------------------ Source/Core/AbsyQuant.cs | 242 -------- Source/Core/AbsyType.cs | 1 - Source/Core/BoogiePL.atg | 2 - Source/Core/CommandLineOptions.cs | 44 -- Source/Core/Core.csproj | 4 - Source/Core/Parser.cs | 2 - Source/Core/StandardVisitor.cs | 5 - Source/DafnyDriver/DafnyDriver.cs | 4 - Source/Houdini/Houdini.cs | 18 +- Source/Houdini/Houdini.csproj | 4 - Source/Provers/SMTLib/SMTLib.csproj | 4 - Source/Provers/Z3api/Z3api.csproj | 4 - Source/VCExpr/Boogie2VCExpr.cs | 9 - Source/VCExpr/VCExpr.csproj | 4 - Source/VCGeneration/ConditionGeneration.cs | 1 - Source/VCGeneration/DoomCheck.cs | 1 - Source/VCGeneration/DoomErrorHandler.cs | 1 - Source/VCGeneration/DoomedLoopUnrolling.cs | 1 - Source/VCGeneration/DoomedStrategy.cs | 1 - Source/VCGeneration/HasseDiagram.cs | 1 - Source/VCGeneration/StratifiedVC.cs | 1 - Source/VCGeneration/VC.cs | 1 - Source/VCGeneration/VCDoomed.cs | 1 - Source/VCGeneration/VCGeneration.csproj | 438 +++++++------- Test/aitest0/Answer | 28 +- Test/aitest0/runtest.bat | 2 +- Test/aitest1/Answer | 67 ++- Test/aitest1/runtest.bat | 4 +- Test/aitest9/runtest.bat | 2 +- 40 files changed, 317 insertions(+), 2753 deletions(-) delete mode 100644 Source/AbsInt/AbstractInterpretation.cs delete mode 100644 Source/AbsInt/ExprFactories.cs delete mode 100644 Source/AbsInt/LoopInvariantsOnDemand.cs diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj index 9ccd0ffe..7e421eb1 100644 --- a/Source/AbsInt/AbsInt.csproj +++ b/Source/AbsInt/AbsInt.csproj @@ -212,20 +212,13 @@ - - - - - {39B0658D-C955-41C5-9A43-48C97A1EF5FD} - AIFramework - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} Basetypes diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs deleted file mode 100644 index d69c624a..00000000 --- a/Source/AbsInt/AbstractInterpretation.cs +++ /dev/null @@ -1,916 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- - -namespace Microsoft.Boogie.AbstractInterpretation { - using System; - using System.Collections; - using System.Collections.Generic; - using System.Diagnostics; - using System.Diagnostics.Contracts; - using Microsoft.Boogie; - using System.Linq; - using AI = Microsoft.AbstractInterpretationFramework; - - - /// - /// Defines invariant propagation methods over ASTs for an abstract interpretation policy. - /// - public class AbstractionEngine { - private AI.Lattice lattice; - private Queue procWorkItems; //PM: changed to generic queue - private Queue/**/ callReturnWorkItems; - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(lattice != null); - Contract.Invariant(procWorkItems != null); - Contract.Invariant(callReturnWorkItems != null); - } - - - private class ProcedureWorkItem { - [Rep] // KRML: this doesn't seem like the right designation to me; but I'm not sure what is - public Procedure Proc; - - public int Index; // pre state is Impl.Summary[Index] - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Proc != null); - Contract.Invariant(0 <= Index && Index < Proc.Summary.Count); - Contract.Invariant(log != null); - } - - public ProcedureWorkItem([Captured] Procedure p, AI.Lattice.Element v, AI.Lattice lattice) { - Contract.Requires(p != null); - Contract.Requires(v != null); - Contract.Requires(lattice != null); - - Contract.Ensures(p == Proc); - this.Proc = p; - p.Summary.Add(new ProcedureSummaryEntry(lattice, v)); - this.Index = p.Summary.Count - 1; - // KRML: axioms are now in place: assume 0 <= Index && Index < Proc.Summary.Count; //PM: Should not be necessary once axioms for pure methods are there - } - } - - private readonly static AI.Logger log = new AI.Logger("Engine"); - - - public AbstractionEngine(AI.Lattice lattice) { - Contract.Requires(lattice != null); - Contract.Assume(cce.IsExposable(log)); //PM: One would need static class invariants to prove this property - cce.BeginExpose(log); - log.Enabled = AI.Lattice.LogSwitch; - cce.EndExpose(); - this.lattice = lattice; - this.procWorkItems = new Queue(); - this.callReturnWorkItems = new Queue(); - } - - public static Dictionary ComputeProcImplMap(Program program) { - Contract.Requires(program != null); - // Since implementations call procedures (impl. signatures) - // rather than directly calling other implementations, we first - // need to compute which implementations implement which - // procedures and remember which implementations call which - // procedures. - - return program - .TopLevelDeclarations - .Where(d => d is Implementation).Select(i => (Implementation)i) - .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc); - - } - - public AI.Lattice.Element ApplyProcedureSummary(CallCmd call, Implementation caller, AI.Lattice.Element knownAtCallSite, CallSite callSite) { - Contract.Requires(call.Proc != null); - Contract.Requires(call != null); - Contract.Requires(caller != null); - Contract.Requires(knownAtCallSite != null); - Contract.Requires(callSite != null); - - Contract.Ensures(Contract.Result() != null); - Procedure proc = call.Proc;//Precondition required that call.Proc !=null, therefore no assert necessarry. - - // NOTE: Here, we count on the fact that an implementation's variables - // are distinct from an implementation's procedure's variables. So, even for - // a recursive implementation, we're free to use the implementation's - // procedure's input parameters as though they were temporary local variables. - // - // Hence, in the program - // procedure Foo (i:int); implementation Foo (i':int) { ...call Foo(i'+1)... } - // we can treat the recursive call as - // i:=i'+1; call Foo(i); - // where the notation i' means a variable with the same (string) name as i, - // but a different identity. - - AI.Lattice.Element relevantToCall = knownAtCallSite; //Precondition of the method implies that this can never be null, therefore no need for an assert. - for (int i = 0; i < proc.InParams.Length; i++) { - // "Assign" the actual expressions to the corresponding formal variables. - Contract.Assume(proc.InParams[i] != null); //PM: this can be fixed once VariableSeq is replaced by List; - Contract.Assume(call.Ins[i] != null); //PM: this can be fixed once VariableSeq is replaced by List; - Expr equality = Expr.Eq(Expr.Ident(cce.NonNull(proc.InParams[i])), cce.NonNull(call.Ins[i])); - relevantToCall = lattice.Constrain(relevantToCall, equality.IExpr); - } - foreach (Variable var in caller.LocVars) { - Contract.Assert(var != null); - relevantToCall = this.lattice.Eliminate(relevantToCall, var); - } - - ProcedureSummary summary = proc.Summary; - Contract.Assert(summary != null); - ProcedureSummaryEntry applicableEntry = null; - - for (int i = 0; i < summary.Count; i++) { - ProcedureSummaryEntry current = cce.NonNull(summary[i]); - - if (lattice.Equivalent(current.OnEntry, relevantToCall)) { - applicableEntry = current; - break; - } - } - - // Not found in current map, so add new entry. - if (applicableEntry == null) { - ProcedureWorkItem newWorkItem = new ProcedureWorkItem(proc, relevantToCall, lattice); - Contract.Assert(newWorkItem != null); - this.procWorkItems.Enqueue(newWorkItem); - applicableEntry = cce.NonNull(proc.Summary[newWorkItem.Index]); - } - applicableEntry.ReturnPoints.Add(callSite); - - - AI.Lattice.Element atReturn = applicableEntry.OnExit; - - for (int i = 0; i < call.Outs.Count; i++) { - atReturn = this.lattice.Rename(atReturn, cce.NonNull(call.Proc.OutParams[i]), cce.NonNull(cce.NonNull(call.Outs[i]).Decl)); - knownAtCallSite = this.lattice.Eliminate(knownAtCallSite, cce.NonNull(cce.NonNull(call.Outs[i]).Decl)); - } - - return this.lattice.Meet(atReturn, knownAtCallSite); - } - - /// - /// Compute the invariants for the program using the underlying abstract domain - /// - public void ComputeProgramInvariants(Program program) { - Contract.Requires(program != null); - - Dictionary procedureImplementations = ComputeProcImplMap(program); - //the line above, ergo there is no need for - //an assert after this statement to maintain - //the non-null type. - AI.Lattice.Element initialElement = this.lattice.Top; - Contract.Assert(initialElement != null); - // Gather all the axioms to create the initial lattice element - // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain - - foreach (Declaration decl in program.TopLevelDeclarations) { - Axiom ax = decl as Axiom; - if (ax != null) { - initialElement = this.lattice.Constrain(initialElement, ax.Expr.IExpr); - } - } - - // propagate over all procedures... - foreach (Declaration decl in program.TopLevelDeclarations) { - Procedure proc = decl as Procedure; - if (proc != null) { - this.procWorkItems.Enqueue(new ProcedureWorkItem(proc, initialElement, this.lattice)); - } - } - - // analyze all the procedures... - while (this.procWorkItems.Count + this.callReturnWorkItems.Count > 0) { - while (this.procWorkItems.Count > 0) { - ProcedureWorkItem workItem = this.procWorkItems.Dequeue(); - - ProcedureSummaryEntry summaryEntry = cce.NonNull(workItem.Proc.Summary[workItem.Index]); - if (!procedureImplementations.ContainsKey(workItem.Proc)) { - // This procedure has no given implementations. We therefore treat the procedure - // according to its specification only. - - if (!CommandLineOptions.Clo.IntraproceduralInfer) { - AI.Lattice.Element post = summaryEntry.OnEntry; - // BUGBUG. Here, we should process "post" according to the requires, modifies, ensures - // specification of the procedure, including any OLD expressions in the postcondition. - AI.Lattice.Element atReturn = post; - - if (!this.lattice.LowerThan(atReturn, summaryEntry.OnExit)) { - // If the results of this analysis are strictly worse than - // what we previous knew for the same input assumptions, - // update the summary and re-do the call sites. - - summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn); - - foreach (CallSite callSite in summaryEntry.ReturnPoints) { - this.callReturnWorkItems.Enqueue(callSite); - } - } - } - } else { - // There are implementations, so do inference based on those implementations - - if (!CommandLineOptions.Clo.IntraproceduralInfer) { - summaryEntry.OnExit = lattice.Bottom; - } - - // For each implementation in the procedure... - foreach (Implementation impl in cce.NonNull(procedureImplementations[workItem.Proc])) { - // process each procedure implementation by recursively processing the first (entry) block... - cce.NonNull(impl.Blocks[0]).Lattice = lattice; - ComputeBlockInvariants(impl, cce.NonNull(impl.Blocks[0]), summaryEntry.OnEntry, summaryEntry); - AdjustProcedureSummary(impl, summaryEntry); - } - } - } - - - while (this.callReturnWorkItems.Count > 0) { - CallSite callSite = cce.NonNull((CallSite)this.callReturnWorkItems.Dequeue()); - - PropagateStartingAtStatement(callSite.Impl, callSite.Block, callSite.Statement, callSite.KnownBeforeCall, callSite.SummaryEntry); - AdjustProcedureSummary(callSite.Impl, callSite.SummaryEntry); - } - - } // both queues - - } - - void AdjustProcedureSummary(Implementation impl, ProcedureSummaryEntry summaryEntry) { - Contract.Requires(impl != null); - Contract.Requires(summaryEntry != null); - if (CommandLineOptions.Clo.IntraproceduralInfer) { - return; // no summary to adjust - } - - // compute the procedure invariant by joining all terminal block invariants... - AI.Lattice.Element post = lattice.Bottom; - foreach (Block block in impl.Blocks) { - if (block.TransferCmd is ReturnCmd) { - // note: if program control cannot reach this block, then postValue will be null - if (block.PostInvariant != null) { - post = (AI.Lattice.Element)lattice.Join(post, block.PostInvariant); - } - } - } - - AI.Lattice.Element atReturn = post; - foreach (Variable var in impl.LocVars) { - Contract.Assert(var != null); - atReturn = this.lattice.Eliminate(atReturn, var); - } - foreach (Variable var in impl.InParams) { - Contract.Assert(var != null); - atReturn = this.lattice.Eliminate(atReturn, var); - } - - if (!this.lattice.LowerThan(atReturn, summaryEntry.OnExit)) { - // If the results of this analysis are strictly worse than - // what we previous knew for the same input assumptions, - // update the summary and re-do the call sites. - - summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn); - - foreach (CallSite callSite in summaryEntry.ReturnPoints) { - Contract.Assert(callSite != null); - this.callReturnWorkItems.Enqueue(callSite); - } - } - } - - private static int freshVarId = 0; - private static Variable FreshVar(Boogie.Type ty) { - Contract.Requires(ty != null); - Contract.Ensures(Contract.Result() != null); - - Variable fresh = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "fresh" + freshVarId, ty)); - freshVarId++; - return fresh; - } - - private delegate CallSite/*!*/ MarkCallSite(AI.Lattice.Element/*!*/ currentValue); - - /// - /// Given a basic block, it propagates the abstract state at the entry point through the exit point of the block - /// The implementation that owns the block - /// The from where we propagate - /// - /// The initial value - /// - private void PropagateStartingAtStatement(Implementation/*!*/ impl, Block/*!*/ block, int statementIndex, AI.Lattice.Element/*!*/ currentValue, - ProcedureSummaryEntry/*!*/ summaryEntry) { - Contract.Requires(impl != null); - Contract.Requires(block != null); - Contract.Requires(currentValue != null); - Contract.Requires(summaryEntry != null); - Contract.Assume(cce.IsPeerConsistent(log)); - log.DbgMsg(string.Format("{0}:", block.Label)); - log.DbgMsgIndent(); - - #region Apply the abstract transition relation to the statements in the block - for (int cmdIndex = statementIndex; cmdIndex < block.Cmds.Length; cmdIndex++) { - Cmd cmd = cce.NonNull(block.Cmds[cmdIndex]); // Fetch the command - currentValue = Step(cmd, currentValue, impl, // Apply the transition function - delegate(AI.Lattice.Element cv) { - Contract.Requires(cv != null); - return new CallSite(impl, block, cmdIndex, cv, summaryEntry); - } - ); - } - - block.PostInvariant = currentValue; // The invariant at the exit point of the block is that of the last statement - - log.DbgMsg(string.Format("pre {0}", cce.NonNull(block.PreInvariant).ToString())); - log.DbgMsg(string.Format("post {0}", (block.PostInvariant).ToString())); - log.DbgMsgUnindent(); - #endregion - #region Propagate the post-condition to the successor nodes - GotoCmd @goto = block.TransferCmd as GotoCmd; - if (@goto != null) { - // labelTargets is non-null after calling Resolve in a prior phase. - Contract.Assume(@goto.labelTargets != null); - - // For all the successors of this block, propagate the abstract state - foreach (Block succ in @goto.labelTargets) { - Contract.Assert(succ != null); - if (impl.Blocks.Contains(succ)) { - succ.Lattice = block.Lattice; // The lattice is the same - // Propagate the post-abstract state of this block to the successor - ComputeBlockInvariants(impl, succ, block.PostInvariant, summaryEntry); - } - } - } - #endregion - } - - /// - /// The abstract transition relation. - /// - private AI.Lattice.Element Step(Cmd cmd, AI.Lattice.Element pre, Implementation impl, MarkCallSite/*?*/ callSiteMarker) { - Contract.Requires(cmd != null); - Contract.Requires(pre != null); - Contract.Requires(impl != null); - Contract.Ensures(Contract.Result() != null); - - Contract.Assume(cce.IsPeerConsistent(log)); - log.DbgMsg(string.Format("{0}", cmd)); - log.DbgMsgIndent(); - - AI.Lattice.Element currentValue = pre;//Nonnullability was a precondition - - // Case split... - #region AssignCmd - if (cmd is AssignCmd) { // parallel assignment - // we first eliminate map assignments - AssignCmd assmt = cce.NonNull((AssignCmd)cmd).AsSimpleAssignCmd; - //PM: Assume variables have been resolved - Contract.Assume(Contract.ForAll(assmt.Lhss, lhs => lhs.DeepAssignedVariable != null));//TODO: Check my work, please, Mike. - - List!*/> freshLhs = new List(); - foreach (AssignLhs lhs in assmt.Lhss) { - Contract.Assert(lhs != null); - freshLhs.Add(Expr.Ident(FreshVar(cce.NonNull(lhs.DeepAssignedVariable) - .TypedIdent.Type))); - } - - for (int i = 0; i < freshLhs.Count; ++i) - currentValue = - this.lattice.Constrain(currentValue, - Expr.Eq(freshLhs[i], assmt.Rhss[i]).IExpr); - foreach (AssignLhs lhs in assmt.Lhss) { - Contract.Assert(lhs != null); - currentValue = - this.lattice.Eliminate(currentValue, cce.NonNull(lhs.DeepAssignedVariable)); - } - for (int i = 0; i < freshLhs.Count; ++i) - currentValue = - this.lattice.Rename(currentValue, cce.NonNull(freshLhs[i].Decl), - cce.NonNull(assmt.Lhss[i].DeepAssignedVariable)); - } - - /* - if (cmd is SimpleAssignCmd) - { - SimpleAssignCmd! assmt = (SimpleAssignCmd)cmd; - assume assmt.Lhs.Decl != null; //PM: Assume variables have been resolved - Variable! dest = assmt.Lhs.Decl; - Variable! fresh = FreshVar(dest.TypedIdent.Type); - IdentifierExpr newLhs = Expr.Ident(fresh); - Expr equality = Expr.Eq(newLhs, assmt.Rhs); - - currentValue = this.lattice.Constrain(currentValue, equality.IExpr); - currentValue = this.lattice.Eliminate(currentValue, dest); - currentValue = this.lattice.Rename(currentValue, fresh, dest); - } - #endregion - #region ArrayAssignCmd - else if (cmd is ArrayAssignCmd) - { - ArrayAssignCmd assmt = (ArrayAssignCmd)cmd; - - assume assmt.Array.Type != null; //PM: assume that type checker has run - ArrayType! arrayType = (ArrayType)assmt.Array.Type; - - Variable newHeapVar = FreshVar(arrayType); - IdentifierExpr newHeap = Expr.Ident(newHeapVar); - IdentifierExpr oldHeap = assmt.Array; - assume oldHeap.Decl != null; //PM: assume that variable has been resolved - - // For now, we only know how to handle heaps - if (arrayType.IndexType0.IsRef && arrayType.IndexType1 != null && arrayType.IndexType1.IsName) - { - //PM: The following assertion follows from a nontrivial invariant of ArrayAssignCmd, - //PM: which we do not have yet. Therefore, we put in an assume fo now. - assume assmt.Index1 != null; - assert assmt.Index1 != null; - // heap succession predicate - Expr heapsucc = Expr.HeapSucc(oldHeap, newHeap, assmt.Index0, assmt.Index1); - - currentValue = this.lattice.Constrain(currentValue, heapsucc.IExpr); - - } - else - { - // TODO: We can do this case as well if the heap succession array can handle non-heap arrays - } - // new select expression - IndexedExpr newLhs = new IndexedExpr(Token.NoToken, newHeap, assmt.Index0, assmt.Index1); - Expr equality = Expr.Eq(newLhs, assmt.Rhs); - - currentValue = this.lattice.Constrain(currentValue, equality.IExpr); - currentValue = this.lattice.Eliminate(currentValue, oldHeap.Decl); - currentValue = this.lattice.Rename(currentValue, newHeapVar, oldHeap.Decl); - - - } */ - #endregion - #region Havoc - else if (cmd is HavocCmd) { - HavocCmd havoc = (HavocCmd)cmd; - foreach (IdentifierExpr id in havoc.Vars) { - Contract.Assert(id != null); - currentValue = this.lattice.Eliminate(currentValue, cce.NonNull(id.Decl)); - } - } - #endregion - #region PredicateCmd - else if (cmd is PredicateCmd) { - //System.Console.WriteLine("Abstract State BEFORE " + ((PredicateCmd) cmd).Expr + " : " +this.lattice.ToPredicate(currentValue)); - - Expr embeddedExpr = cce.NonNull((PredicateCmd)cmd).Expr; - List!*/> conjuncts = flatConjunction(embeddedExpr); // Handle "assume P && Q" as if it was "assume P; assume Q" - Contract.Assert(conjuncts != null); - foreach (Expr c in conjuncts) { - Contract.Assert(c != null); - currentValue = this.lattice.Constrain(currentValue, c.IExpr); - } - - //System.Console.WriteLine("Abstract State AFTER assert/assume "+ this.lattice.ToPredicate(currentValue)); - } - #endregion - #region CallCmd - else if (cmd is CallCmd) { - CallCmd call = (CallCmd)cmd; - - if (!CommandLineOptions.Clo.IntraproceduralInfer) { - // Interprocedural analysis - - if (callSiteMarker == null) { - throw new System.InvalidOperationException("INTERNAL ERROR: Context does not allow CallCmd."); - } - - CallSite here = callSiteMarker(currentValue); - currentValue = ApplyProcedureSummary(call, impl, currentValue, here); - } else { - // Intraprocedural analysis - - StateCmd statecmd = call.Desugaring as StateCmd; - if (statecmd != null) { - // Iterate the abstract transition on all the commands in the desugaring of the call - foreach (Cmd callDesug in statecmd.Cmds) { - Contract.Assert(callDesug != null); - currentValue = Step(callDesug, currentValue, impl, null); - } - - // Now, project out the local variables - foreach (Variable local in statecmd.Locals) { - Contract.Assert(local != null); - currentValue = this.lattice.Eliminate(currentValue, local); - } - } else - throw new System.InvalidOperationException("INTERNAL ERROR: CallCmd does not desugar to StateCmd."); - } - } - #endregion - #region CommentCmd - else if (cmd is CommentCmd) { - // skip - } - #endregion - else if (cmd is SugaredCmd) { - // other sugared commands are treated like their desugaring - SugaredCmd sugar = (SugaredCmd)cmd; - Cmd desugaring = sugar.Desugaring; - if (desugaring is StateCmd) { - StateCmd statecmd = (StateCmd)desugaring; - // Iterate the abstract transition on all the commands in the desugaring of the call - foreach (Cmd callDesug in statecmd.Cmds) { - Contract.Assert(callDesug != null); - currentValue = Step(callDesug, currentValue, impl, null); - } - // Now, project out the local variables - foreach (Variable local in statecmd.Locals) { - Contract.Assert(local != null); - currentValue = this.lattice.Eliminate(currentValue, local); - } - } else { - currentValue = Step(desugaring, currentValue, impl, null); - } - } else { - Contract.Assert(false); // unknown command - throw new cce.UnreachableException(); - } - - log.DbgMsgUnindent(); - - return currentValue; - } - - /// - /// Flatten an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R] - /// - private List!*/> flatConjunction(Expr embeddedExpr) { - Contract.Requires(embeddedExpr != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - var retValue = new List(); - NAryExpr e = embeddedExpr as NAryExpr; - if (e != null && e.Fun.FunctionName.CompareTo("&&") == 0) { // if it is a conjunction - foreach (Expr arg in e.Args) { - Contract.Assert(arg != null); - var newConjuncts = flatConjunction(arg); - retValue.AddRange(newConjuncts); - } - } else { - retValue.Add(embeddedExpr); - } - return retValue; - } - - /// - /// Compute the invariants for a basic block - /// The implementation the block belongs to - /// The block for which we compute the invariants - /// The "init" abstract state for the block - /// - private void ComputeBlockInvariants(Implementation impl, Block block, AI.Lattice.Element incomingValue, ProcedureSummaryEntry summaryEntry) { - Contract.Requires(impl != null); - Contract.Requires(block != null); - Contract.Requires(incomingValue != null); - Contract.Requires(summaryEntry != null); - if (block.PreInvariant == null) // block has not yet been processed - { - Contract.Assert(block.PostInvariant == null); - - // To a first approximation the block is unreachable - block.PreInvariant = this.lattice.Bottom; - block.PostInvariant = this.lattice.Bottom; - } - - Contract.Assert(block.PreInvariant != null); - Contract.Assert(block.PostInvariant != null); - - #region Check if we have reached a postfixpoint - - if (lattice.LowerThan(incomingValue, block.PreInvariant)) { - // We have reached a post-fixpoint, so we are done... -#if DEBUG_PRINT - System.Console.WriteLine("@@ Compared for block {0}:", block.Label); - System.Console.WriteLine("@@ {0}", lattice.ToPredicate(incomingValue)); - System.Console.WriteLine("@@ {0}", lattice.ToPredicate(block.PreInvariant)); - System.Console.WriteLine("@@ result = True"); - System.Console.WriteLine("@@ end Compare"); -#endif - return; - } -#if DEBUG_PRINT - // Compute the free variables in incoming and block.PreInvariant - FreeVariablesVisitor freeVarsVisitorForA = new FreeVariablesVisitor(); - FreeVariablesVisitor freeVarsVisitorForB = new FreeVariablesVisitor(); - - lattice.ToPredicate(incomingValue).DoVisit(freeVarsVisitorForA); - lattice.ToPredicate(block.PreInvariant).DoVisit(freeVarsVisitorForB); - - List! freeVarsOfA = freeVarsVisitorForA.FreeVariables; - List! freeVarsOfB = freeVarsVisitorForB.FreeVariables; - - System.Console.WriteLine("@@ Compared for block {0}:", block.Label); - System.Console.WriteLine("@@ Incoming: {0}", lattice.ToPredicate((!) incomingValue)); - System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfA)); - System.Console.WriteLine("@@ Previous: {0}", lattice.ToPredicate(block.PreInvariant)); - System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfB)); - System.Console.WriteLine("@@ result = False"); - System.Console.WriteLine("@@ end Compare"); - string operation = ""; -#endif - #endregion - #region If it is not the case, then join or widen the incoming abstract state with the previous one - if (block.widenBlock) // If the considered block is the entry point of a loop - { - if (block.iterations <= CommandLineOptions.Clo.StepsBeforeWidening + 1) { -#if DEBUG_PRINT - operation = "join"; -#endif - block.PreInvariant = (AI.Lattice.Element)lattice.Join(block.PreInvariant, incomingValue); - } else { -#if DEBUG_PRINT - operation = "widening"; -#endif - - // The default is to have have a widening that perform a (approximation of) the closure of the operands, so to improve the precision - // block.PreInvariant = WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue); - block.PreInvariant = (AI.Lattice.Element)lattice.Widen(block.PreInvariant, incomingValue); - } - block.iterations++; - } else { -#if DEBUG_PRINT - operation = "join"; -#endif - block.PreInvariant = (AI.Lattice.Element)lattice.Join(block.PreInvariant, incomingValue); - } - -#if DEBUG_PRINT - System.Console.WriteLine("@@ {0} for block {1}:", operation, block.Label); - System.Console.WriteLine("@@ {0}", lattice.ToPredicate(block.PreInvariant)); - System.Console.WriteLine("@@ end"); -#endif - #endregion - #region Propagate the entry abstract state through the method - PropagateStartingAtStatement(impl, block, 0, cce.NonNull(block.PreInvariant.Clone()), summaryEntry); - #endregion - } - -#if DEBUG_PRINT - private string! ToString(List! vars) - { - string s = ""; - - foreach(AI.IVariable! v in vars) - { - s += v.Name +" "; - } - return s; - } -#endif - - } // class - - - /// - /// Defines a class for building the abstract domain according to the parameters switch - /// - public class AbstractDomainBuilder { - - private AbstractDomainBuilder() { /* do nothing */ - } - - /// - /// Return a fresh instance of the abstract domain of intervals - /// - static public AbstractAlgebra BuildIntervalsAbstractDomain() { - Contract.Ensures(Contract.Result() != null); - - AI.IPropExprFactory propfactory = new BoogiePropFactory(); - AI.ILinearExprFactory linearfactory = new BoogieLinearFactory(); - AI.IValueExprFactory valuefactory = new BoogieValueFactory(); - IComparer variableComparer = new VariableComparer(); - - AbstractAlgebra retAlgebra; - AI.Lattice intervals = new AI.VariableMapLattice(propfactory, valuefactory, new AI.IntervalLattice(linearfactory), variableComparer); - Contract.Assert(intervals != null); - retAlgebra = new AbstractAlgebra(intervals, propfactory, linearfactory, null, valuefactory, null, variableComparer); - - return retAlgebra; - } - - /// - /// Return a fresh abstract domain, according to the parameters specified by the command line - /// - static public AbstractAlgebra BuildAbstractDomain() { - Contract.Ensures(Contract.Result() != null); - - AbstractAlgebra retAlgebra; - - AI.Lattice returnLattice; - - AI.IPropExprFactory propfactory = new BoogiePropFactory(); - AI.ILinearExprFactory linearfactory = new BoogieLinearFactory(); - AI.IIntExprFactory intfactory = new BoogieIntFactory(); - AI.IValueExprFactory valuefactory = new BoogieValueFactory(); - AI.INullnessFactory nullfactory = new BoogieNullnessFactory(); - IComparer variableComparer = new VariableComparer(); - - AI.MultiLattice multilattice = new AI.MultiLattice(propfactory, valuefactory); - - if (CommandLineOptions.Clo.Ai.Intervals) // Intervals - { - multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory, - new AI.IntervalLattice(linearfactory), - variableComparer)); - } - if (CommandLineOptions.Clo.Ai.Constant) // Constant propagation - - { - multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory, - new AI.ConstantLattice(intfactory), - variableComparer)); - } - if (CommandLineOptions.Clo.Ai.DynamicType) // Class types - { - BoogieTypeFactory typeFactory = new BoogieTypeFactory(); - multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory, - new AI.DynamicTypeLattice(typeFactory, propfactory), - variableComparer)); - } - if (CommandLineOptions.Clo.Ai.Nullness) // Nullness - { - multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory, - new AI.NullnessLattice(nullfactory), - variableComparer)); - } - if (CommandLineOptions.Clo.Ai.Polyhedra) // Polyhedra - { - multilattice.AddLattice(new AI.PolyhedraLattice(linearfactory, propfactory)); - } - - - returnLattice = multilattice; - if (CommandLineOptions.Clo.Ai.DebugStatistics) { - returnLattice = new AI.StatisticsLattice(returnLattice); - } - - returnLattice.Validate(); - - retAlgebra = new AbstractAlgebra(returnLattice, propfactory, linearfactory, intfactory, valuefactory, nullfactory, - variableComparer); - - return retAlgebra; - - } - } - - /// - /// An Abstract Algebra is a tuple made of a Lattice and several factories - /// - public class AbstractAlgebra { - [Peer] - private AI.Lattice lattice; - [Peer] - private AI.IPropExprFactory propFactory; - [Peer] - private AI.ILinearExprFactory linearFactory; - [Peer] - private AI.IIntExprFactory intFactory; - [Peer] - private AI.IValueExprFactory valueFactory; - [Peer] - private AI.INullnessFactory nullFactory; - [Peer] - private IComparer variableComparer; - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(lattice != null); - } - - public AI.Lattice Lattice { - get { - Contract.Ensures(Contract.Result() != null); - - return lattice; - } - } - - public AI.IPropExprFactory PropositionFactory { - get { - return this.propFactory; - } - } - - public AI.ILinearExprFactory LinearExprFactory { - get { - return this.linearFactory; - } - } - - public AI.IIntExprFactory IntExprFactory { - get { - return this.intFactory; - } - } - - public AI.IValueExprFactory ValueFactory { - get { - return this.valueFactory; - } - } - - public AI.INullnessFactory NullFactory { - get { - return this.nullFactory; - } - } - - public IComparer VariableComparer { - get { - return this.variableComparer; - } - } - - [Captured] - public AbstractAlgebra(AI.Lattice lattice, - AI.IPropExprFactory propFactory, - AI.ILinearExprFactory linearFactory, - AI.IIntExprFactory intFactory, - AI.IValueExprFactory valueFactory, - AI.INullnessFactory nullFactory, - IComparer variableComparer) { - Contract.Requires(propFactory == null || cce.Owner.Same(lattice, propFactory));//TODO: Owner is Microsoft.Contracts (mscorlib.Contracts).Owner - Contract.Requires(linearFactory == null || cce.Owner.Same(lattice, linearFactory)); - Contract.Requires(intFactory == null || cce.Owner.Same(lattice, intFactory)); - Contract.Requires(valueFactory == null || cce.Owner.Same(lattice, valueFactory)); - Contract.Requires(nullFactory == null || cce.Owner.Same(lattice, nullFactory)); - Contract.Requires(variableComparer == null || cce.Owner.Same(lattice, variableComparer)); - // ensures Owner.Same(this, lattice); // KRML: - - Contract.Requires(lattice != null); - this.lattice = lattice; - - this.propFactory = propFactory; - this.linearFactory = linearFactory; - this.intFactory = intFactory; - this.valueFactory = valueFactory; - this.nullFactory = nullFactory; - this.variableComparer = variableComparer; - } - - } - - public class AbstractInterpretation { - /// - /// Run the abstract interpretation. - /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn - /// - public static void RunAbstractInterpretation(Program program) { - Contract.Requires(program != null); - Helpers.ExtraTraceInformation("Starting abstract interpretation"); - - if (CommandLineOptions.Clo.UseAbstractInterpretation) { - DateTime start = new DateTime(); // to please compiler's definite assignment rules - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine(); - Console.WriteLine("Running abstract interpretation..."); - start = DateTime.UtcNow; - } - - WidenPoints.Compute(program); - - if (CommandLineOptions.Clo.Ai.AnySet) // if there is some user defined domain we override the default (= intervals) - { - AI.Lattice lattice = AbstractDomainBuilder.BuildAbstractDomain().Lattice; - ApplyAbstractInterpretation(program, lattice); - - if (CommandLineOptions.Clo.Ai.DebugStatistics) { - Console.Error.WriteLine(lattice); - } - } else // Otherwise the default is the use of the abstract domain of intervals (useful for simple for loops) - { - AI.Lattice lattice = AbstractDomainBuilder.BuildIntervalsAbstractDomain().Lattice; - Contract.Assert(lattice != null); - ApplyAbstractInterpretation(program, lattice); - } - - program.InstrumentWithInvariants(); - - if (CommandLineOptions.Clo.Trace) { - DateTime end = DateTime.UtcNow; - TimeSpan elapsed = end - start; - Console.WriteLine(" [{0} s]", elapsed.TotalSeconds); - Console.Out.Flush(); - } - } - } - - static void ApplyAbstractInterpretation(Program program, AI.Lattice lattice) { - Contract.Requires(program != null); - Contract.Requires(lattice != null); - AbstractionEngine engine = new AbstractionEngine(lattice); - engine.ComputeProgramInvariants(program); - } - } - -} // namespace \ No newline at end of file diff --git a/Source/AbsInt/ExprFactories.cs b/Source/AbsInt/ExprFactories.cs deleted file mode 100644 index 9b1ea0a0..00000000 --- a/Source/AbsInt/ExprFactories.cs +++ /dev/null @@ -1,275 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using Microsoft.Boogie; -using AI = Microsoft.AbstractInterpretationFramework; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; - -namespace Microsoft.Boogie.AbstractInterpretation { - - public class BoogiePropFactory : BoogieFactory, AI.IPropExprFactory - { - public AI.IFunApp False { - get { - Contract.Ensures(Contract.Result() != null); - - return Expr.False; - } - } - public AI.IFunApp True { - get { - Contract.Ensures(Contract.Result() != null); - - return Expr.True; - } - } - - public AI.IFunApp Not(AI.IExpr p) { - //Contract.Requires(p != null); - Contract.Ensures(Contract.Result() != null); - - return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, IExpr2Expr(p)); - } - - public AI.IFunApp And(AI.IExpr p, AI.IExpr q) { - //Contract.Requires(p != null); - //Contract.Requires(q != null); - Contract.Ensures(Contract.Result() != null); - - return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q)); - } - - public AI.IFunApp Or(AI.IExpr p, AI.IExpr q) { - //Contract.Requires(p != null); - //Contract.Requires(q != null); - Contract.Ensures(Contract.Result() != null); - return Expr.Binary(BinaryOperator.Opcode.Or, IExpr2Expr(p), IExpr2Expr(q)); - } - - public AI.IFunApp Implies(AI.IExpr p, AI.IExpr q) { - //Contract.Requires(p != null); - //Contract.Requires(q != null); - Contract.Ensures(Contract.Result() != null); - return Expr.Binary(BinaryOperator.Opcode.Imp, IExpr2Expr(p), IExpr2Expr(q)); - } - - public AI.IFunApp Exists(AI.IFunction p) { - //Contract.Requires(p != null); - Contract.Ensures(Contract.Result() != null); - - return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr; - } - - public AI.IFunApp Forall(AI.IFunction p) { - //Contract.Requires(p != null); - Contract.Ensures(Contract.Result() != null); - - return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr; - } - } - - public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory { - public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) { - //Contract.Requires(e0 != null); - //Contract.Requires(e1 != null); - Contract.Ensures(Contract.Result() != null); - - return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1)); - } - public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) { - //Contract.Requires(e0 != null); - //Contract.Requires(e1 != null); - Contract.Ensures(Contract.Result() != null); - return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1)); - } - } - - public class BoogieNullnessFactory : BoogieFactory, AI.INullnessFactory { - public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) { - //Contract.Requires(e0 != null); - //Contract.Requires(e1 != null); - Contract.Ensures(Contract.Result() != null); - return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1)); - } - - public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) { - //Contract.Requires(e0 != null); - //Contract.Requires(e1 != null); - Contract.Ensures(Contract.Result() != null); - return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1)); - } - - public AI.IFunApp Null { - get { - Contract.Assert(false); // don't know where to get null from\ - throw new cce.UnreachableException(); - } - } - } - - public class BoogieIntFactory : BoogieValueFactory, AI.IIntExprFactory { - public AI.IFunApp Const(BigNum i) { - Contract.Ensures(Contract.Result() != null); - - return new LiteralExpr(Token.NoToken, i); - } - } - - public class BoogieLinearFactory : BoogieIntFactory, AI.ILinearExprFactory { - public AI.IFunApp AtMost(AI.IExpr e0, AI.IExpr e1) { - //Contract.Requires(e0 != null); - //Contract.Requires(e1 != null); - Contract.Ensures(Contract.Result() != null); - return Expr.Le(IExpr2Expr(e0), IExpr2Expr(e1)); - } - public AI.IFunApp Add(AI.IExpr e0, AI.IExpr e1) { - //Contract.Requires(e0 != null); - //Contract.Requires(e1 != null); - Contract.Ensures(Contract.Result() != null); - return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1)); - } - public AI.IExpr Term(Rational r, AI.IVariable var) { - Contract.Ensures(Contract.Result() != null); - - if (var != null && r == Rational.ONE) { - return var; - } else { - Expr product; - if (r.IsIntegral) { - product = Expr.Literal(r.AsBigNum); - } else { - product = Expr.Div(Expr.Literal(r.Numerator), Expr.Literal(r.Denominator)); - } - if (var != null) { - product = Expr.Mul(product, IExpr2Expr(var)); - } - return product.IExpr; - } - } - - public AI.IFunApp False { - get { - Contract.Ensures(Contract.Result() != null); - - return Expr.False; - } - } - public AI.IFunApp True { - get { - Contract.Ensures(Contract.Result() != null); - - return Expr.True; - } - } - public AI.IFunApp And(AI.IExpr p, AI.IExpr q) { - //Contract.Requires(p != null); - //Contract.Requires(q != null); - Contract.Ensures(Contract.Result() != null); - - return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q)); - } - } - - public class BoogieTypeFactory : BoogieFactory, AI.ITypeExprFactory { - /// - /// Returns an expression denoting the top of the type hierarchy. - /// - public AI.IExpr RootType { - get { - Contract.Assert(false); // BUGBUG: TODO - throw new System.NotImplementedException(); - } - } - - /// - /// Returns true iff "t" denotes a type constant. - /// - [Pure] - public bool IsTypeConstant(AI.IExpr t) { - //Contract.Requires(t != null); - Contract.Ensures(Contract.Result() == (t is Constant)); - return t is Constant; - } - - /// - /// Returns true iff t0 and t1 are types such that t0 and t1 are equal. - /// - [Pure] - public bool IsTypeEqual(AI.IExpr t0, AI.IExpr t1) { - //Contract.Requires(t0 != null); - //Contract.Requires(t1 != null); - Constant c0 = t0 as Constant; - Constant c1 = t1 as Constant; - return c0 != null && c1 != null && c0 == c1; - } - - /// - /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1. - /// - [Pure] - public bool IsSubType(AI.IExpr t0, AI.IExpr t1) { - //Contract.Requires(t0 != null); - //Contract.Requires(t1 != null); - - Contract.Assert(false); // BUGBUG: TODO - throw new cce.UnreachableException(); - } - - /// - /// Returns the most derived supertype of both "t0" and "t1". A precondition is - /// that "t0" and "t1" both represent types. - /// - public AI.IExpr JoinTypes(AI.IExpr t0, AI.IExpr t1) { - //Contract.Requires(t0 != null); - //Contract.Requires(t1 != null); - Contract.Ensures(Contract.Result() != null); - - - Contract.Assert(false); // BUGBUG: TODO - throw new cce.UnreachableException(); - } - - public AI.IFunApp IsExactlyA(AI.IExpr e, AI.IExpr type) { - //PM: We need this assume because Boogie does not yet allow us to use the - //PM: inherited precondition "requires IsTypeConstant(type)". - //PM: Note that that precondition is currently commented out. - //Contract.Requires(e != null); - //Contract.Requires(type != null); - Contract.Ensures(Contract.Result() != null); - - Contract.Assume(type is Constant); - Constant theType = (Constant)type; - Contract.Assert(false); - throw new cce.UnreachableException(); - Expr typeofExpr = new NAryExpr(Token.NoToken, - new FunctionCall(new IdentifierExpr(Token.NoToken, "$typeof", Type.Int // Name - )), - new ExprSeq(IExpr2Expr(e))); - return Expr.Eq(typeofExpr, Expr.Ident(theType)); - } - - public AI.IFunApp IsA(AI.IExpr e, AI.IExpr type) { - //Contract.Requires(e != null); - //Contract.Requires(type != null); - Contract.Ensures(Contract.Result() != null); - //PM: We need this assume because Boogie does not yet allow us to use the - //PM: inherited precondition "requires IsTypeConstant(type)". - //PM: Note that that precondition is currently commented out. - - - Contract.Assume(type is Constant); - Contract.Assert(false); - throw new cce.UnreachableException(); - Expr typeofExpr = new NAryExpr(Token.NoToken, - new FunctionCall(new IdentifierExpr(Token.NoToken, "$typeof", Type.Int // Name - )), - new ExprSeq(IExpr2Expr(e))); - return new NAryExpr(Token.NoToken, - new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Subtype), - new ExprSeq(typeofExpr, IExpr2Expr(e))); - } - } -} diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs deleted file mode 100644 index b61b1445..00000000 --- a/Source/AbsInt/LoopInvariantsOnDemand.cs +++ /dev/null @@ -1,84 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -namespace Microsoft.Boogie.AbstractInterpretation { - using System; - using System.Collections; - using System.Collections.Generic; - using System.Diagnostics.Contracts; - using AI = Microsoft.AbstractInterpretationFramework; - using Boogie = Microsoft.Boogie; - - - - /// - /// A visitor of an abstract interpretation expression that collects the free variables - /// - class FreeVariablesVisitor : AI.ExprVisitor { - [Peer] - List variables; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(variables)); - Contract.Invariant(cce.NonNullElements(varNames)); - } - - public List FreeVariables { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - return this.variables; - } - } - - List varNames; // used to check the consinstency! - - public FreeVariablesVisitor() { - this.variables = new List(); - this.varNames = new List(); - } - - override public object Default(AI.IExpr expr) { - - if (expr is AI.IVariable) { - if (!variables.Contains((AI.IVariable)expr)) { - this.variables.Add((AI.IVariable)expr); - - Contract.Assert(!this.varNames.Contains(expr.ToString())); // If we get there, we have an error: two variables with the same name but different identity - - this.varNames.Add(expr.ToString()); - } - return null; - } else if (expr is AI.IFunApp) - return VisitFunApp((AI.IFunApp)expr); - else if (expr is AI.IFunction) - return VisitFunction((AI.IFunction)expr); - else if (expr is AI.IUnknown) - return null; - else { - Contract.Assert(false); - throw new cce.UnreachableException(); - } - } - - public override object VisitFunApp(AI.IFunApp funapp) { - - foreach (AI.IExpr arg in funapp.Arguments) { - Contract.Assert(arg != null); - arg.DoVisit(this); - } - return true; - } - - public override object VisitFunction(AI.IFunction fun) { - //Contract.Requires(fun != null); - fun.Body.DoVisit(this); - this.variables.Remove(fun.Param); - return true; - } - - } - -} \ No newline at end of file diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs index f5bf1e03..4fccc14b 100644 --- a/Source/AbsInt/NativeLattice.cs +++ b/Source/AbsInt/NativeLattice.cs @@ -6,6 +6,7 @@ using System; using System.Collections.Generic; +using System.Linq; using System.Text; using System.Diagnostics.Contracts; using Microsoft.Boogie; @@ -95,7 +96,7 @@ namespace Microsoft.Boogie.AbstractInterpretation } if (lattice != null) { - Dictionary procedureImplementations = AbstractionEngine.ComputeProcImplMap(program); + Dictionary procedureImplementations = ComputeProcImplMap(program); ComputeProgramInvariants(program, procedureImplementations, lattice); if (CommandLineOptions.Clo.Ai.DebugStatistics) { Console.Error.WriteLine(lattice); @@ -110,9 +111,22 @@ namespace Microsoft.Boogie.AbstractInterpretation } } + private static Dictionary ComputeProcImplMap(Program program) { + Contract.Requires(program != null); + // Since implementations call procedures (impl. signatures) + // rather than directly calling other implementations, we first + // need to compute which implementations implement which + // procedures and remember which implementations call which + // procedures. + + return program + .TopLevelDeclarations + .Where(d => d is Implementation).Select(i => (Implementation)i) + .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc); + } + /// - /// Compute and apply the invariants for the program using the underlying abstract domain (using native Boogie - /// expressions, not the abstracted AI.Expr's). + /// Compute and apply the invariants for the program using the underlying abstract domain. /// public static void ComputeProgramInvariants(Program program, Dictionary procedureImplementations, NativeLattice lattice) { Contract.Requires(program != null); diff --git a/Source/Boogie.sln b/Source/Boogie.sln index e1565043..106a9b74 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -17,8 +17,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "Core\Core.csproj", EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3api", "Provers\Z3api\Z3api.csproj", "{966DD87B-A29D-4F3C-9406-F680A61DC0E0}" EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AIFramework", "AIFramework\AIFramework.csproj", "{39B0658D-C955-41C5-9A43-48C97A1EF5FD}" -EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "Graph\Graph.csproj", "{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}" EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Basetypes", "Basetypes\Basetypes.csproj", "{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}" @@ -229,31 +227,6 @@ Global {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU {966DD87B-A29D-4F3C-9406-F680A61DC0E0}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|.NET.ActiveCfg = Checked|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.ActiveCfg = Checked|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Any CPU.Build.0 = Checked|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Checked|x86.ActiveCfg = Checked|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|.NET.ActiveCfg = Debug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|Any CPU.Build.0 = Debug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Debug|x86.ActiveCfg = Debug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|.NET.ActiveCfg = Release|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Any CPU.ActiveCfg = Release|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Any CPU.Build.0 = Release|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Mixed Platforms.Build.0 = Release|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|x86.ActiveCfg = Release|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU - {39B0658D-C955-41C5-9A43-48C97A1EF5FD}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|.NET.ActiveCfg = Checked|Any CPU {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|Any CPU.ActiveCfg = Checked|Any CPU {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|Any CPU.Build.0 = Checked|Any CPU diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 1653b723..75ba7372 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -20,7 +20,6 @@ namespace Microsoft.Boogie { using System.Diagnostics; using System.Linq; using VC; - using AI = Microsoft.AbstractInterpretationFramework; using BoogiePL = Microsoft.Boogie; /* @@ -583,11 +582,13 @@ namespace Microsoft.Boogie { // ---------- Infer invariants -------------------------------------------------------- // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch) - if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial) { - Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); - } else { - Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program); + if (CommandLineOptions.Clo.UseAbstractInterpretation) { + if (!CommandLineOptions.Clo.Ai.J_Intervals && !CommandLineOptions.Clo.Ai.J_Trivial) { + // use /infer:j as the default + CommandLineOptions.Clo.Ai.J_Intervals = true; + } } + Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); if (CommandLineOptions.Clo.LoopUnrollCount != -1) { program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount); diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 51a10002..9edd2df7 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -214,10 +214,6 @@ {0EFA3E43-690B-48DC-A72C-384A3EA7F31F} AbsInt - - {39B0658D-C955-41C5-9A43-48C97A1EF5FD} - AIFramework - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} Basetypes diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 9df982d9..b64a9e5e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -11,56 +11,40 @@ namespace Microsoft.Boogie.AbstractInterpretation { using System.Diagnostics.Contracts; using System.Collections; using System.Collections.Generic; - using AI = Microsoft.AbstractInterpretationFramework; public class CallSite { public readonly Implementation/*!*/ Impl; public readonly Block/*!*/ Block; public readonly int Statement; // invariant: Block[Statement] is CallCmd - public readonly AI.Lattice.Element/*!*/ KnownBeforeCall; public readonly ProcedureSummaryEntry/*!*/ SummaryEntry; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Impl != null); Contract.Invariant(Block != null); - Contract.Invariant(KnownBeforeCall != null); Contract.Invariant(SummaryEntry != null); } - public CallSite(Implementation impl, Block b, int stmt, AI.Lattice.Element e, ProcedureSummaryEntry summaryEntry) { + public CallSite(Implementation impl, Block b, int stmt, ProcedureSummaryEntry summaryEntry) { Contract.Requires(summaryEntry != null); - Contract.Requires(e != null); Contract.Requires(b != null); Contract.Requires(impl != null); this.Impl = impl; this.Block = b; this.Statement = stmt; - this.KnownBeforeCall = e; this.SummaryEntry = summaryEntry; } } public class ProcedureSummaryEntry { - public AI.Lattice/*!*/ Lattice; - public AI.Lattice.Element/*!*/ OnEntry; - public AI.Lattice.Element/*!*/ OnExit; public HashSet/*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(Lattice != null); - Contract.Invariant(OnEntry != null); - Contract.Invariant(OnExit != null); Contract.Invariant(ReturnPoints != null); } - public ProcedureSummaryEntry(AI.Lattice lattice, AI.Lattice.Element onEntry) { - Contract.Requires(onEntry != null); - Contract.Requires(lattice != null); - this.Lattice = lattice; - this.OnEntry = onEntry; - this.OnExit = lattice.Bottom; + public ProcedureSummaryEntry() { this.ReturnPoints = new HashSet(); // base(); } @@ -93,7 +77,6 @@ namespace Microsoft.Boogie { using System.Collections.Generic; using System.Diagnostics.Contracts; using Microsoft.Boogie.AbstractInterpretation; - using AI = Microsoft.AbstractInterpretationFramework; using Graphing; using Set = GSet; @@ -349,12 +332,6 @@ namespace Microsoft.Boogie { } } - public void InstrumentWithInvariants() { - foreach (Declaration d in this.TopLevelDeclarations) { - d.InstrumentWithInvariants(); - } - } - /// /// Reset the abstract stated computed before /// @@ -1044,14 +1021,6 @@ namespace Microsoft.Boogie { public virtual void ComputeStronglyConnectedComponents() { /* Does nothing */ } - /// - /// This method inserts the abstract-interpretation-inferred invariants - /// as assume (or possibly assert) statements in the statement sequences of - /// each block. - /// - public virtual void InstrumentWithInvariants() { - } - /// /// Reset the abstract stated computed before /// @@ -1388,7 +1357,7 @@ namespace Microsoft.Boogie { } } - public abstract class Variable : NamedDeclaration, AI.IVariable { + public abstract class Variable : NamedDeclaration { public TypedIdent/*!*/ TypedIdent; [ContractInvariantMethod] void ObjectInvariant() { @@ -1446,11 +1415,6 @@ namespace Microsoft.Boogie { TypecheckAttributes(tc); this.TypedIdent.Typecheck(tc); } - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitVariable(this); - } } public class VariableComparer : IComparer { @@ -2354,12 +2318,6 @@ namespace Microsoft.Boogie { for (int s = 0; s < this.Summary.Count; s++) { ProcedureSummaryEntry/*!*/ entry = cce.NonNull(this.Summary[s]); stream.Write(level + 1, "// "); - Expr e; - e = (Expr)entry.Lattice.ToPredicate(entry.OnEntry); - e.Emit(stream); - stream.Write(" ==> "); - e = (Expr)entry.Lattice.ToPredicate(entry.OnExit); - e.Emit(stream); stream.WriteLine(); } } @@ -2861,53 +2819,6 @@ namespace Microsoft.Boogie { } } - /// - /// Instrument the blocks with the inferred invariants - /// - public override void InstrumentWithInvariants() { - foreach (Block b in this.Blocks) { - if (b.Lattice != null) { - Contract.Assert(b.PreInvariant != null); /* If the pre-abstract state is null, then something is wrong */ - Contract.Assert(b.PostInvariant != null); /* If the post-state is null, then something is wrong */ - - bool instrumentEntry; - bool instrumentExit; - switch (CommandLineOptions.Clo.InstrumentInfer) { - case CommandLineOptions.InstrumentationPlaces.Everywhere: - instrumentEntry = true; - instrumentExit = true; - break; - case CommandLineOptions.InstrumentationPlaces.LoopHeaders: - instrumentEntry = b.widenBlock; - instrumentExit = false; - break; - default: { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // unexpected InstrumentationPlaces value - } - - if (instrumentEntry || instrumentExit) { - CmdSeq newCommands = new CmdSeq(); - if (instrumentEntry) { - Expr inv = (Expr)b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/ - var kv = new QKeyValue(Token.NoToken, "inferred", new List(), null); - PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv); - newCommands.Add(cmd); - } - newCommands.AddRange(b.Cmds); - if (instrumentExit) { - Expr inv = (Expr)b.Lattice.ToPredicate(b.PostInvariant); - var kv = new QKeyValue(Token.NoToken, "inferred", new List(), null); - PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv); - newCommands.Add(cmd); - } - b.Cmds = newCommands; - } - } - } - } - /// /// Return a collection of blocks that are reachable from the block passed as a parameter. /// The block must be defined in the current implementation @@ -3148,113 +3059,6 @@ namespace Microsoft.Boogie { } } - /// - /// Conceptually, a LatticeElementList is a infinite array indexed from 0, - /// where some finite number of elements have a non-null value. All elements - /// have type Lattice.Element. - /// - /// The Count property returns the first index above all non-null values. - /// - /// The [i] getter returns the element at position i, which may be null. The - /// index i is not allowed to be negative. - /// The [i] setter sets the element at position i. As a side effect, this - /// operation may increase Count. The index i is not allowed to be negative. - /// The right-hand value of the setter is not allowed to be null; that is, - /// null can occur in the list only as an "unused" element. - /// - public class LatticeElementList : ArrayList { - public new /*Maybe null*/ AI.Lattice.Element this[int i] { - get { - if (i < Count) { - return (AI.Lattice.Element)base[i]; - } else { - return null; - } - } - set { - System.Diagnostics.Debug.Assert(value != null); - while (Count <= i) { - Add(null); - } - base[i] = value; - } - } - /// - /// Returns the disjunction of (the expression formed from) the - /// non-null lattice elements in the list. The expressions are - /// formed according to the given "lattice", which is assumed to - /// be the lattice of the lattice elements stored in the list. - /// - /// - /// - public Expr GetDisjunction(AI.Lattice lattice) { - Contract.Requires(lattice != null); - Expr disjunction = null; - foreach (AI.Lattice.Element el in this) { - if (el != null) { - Expr e = (Expr)lattice.ToPredicate(el); - if (disjunction == null) { - disjunction = e; - } else { - disjunction = Expr.Or(disjunction, e); - } - } - } - if (disjunction == null) { - return Expr.False; - } else { - return disjunction; - } - } - } - - public abstract class BoogieFactory { - public static Expr IExpr2Expr(AI.IExpr e) { - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - Variable v = e as Variable; - if (v != null) { - return new IdentifierExpr(Token.NoToken, v); - } else if (e is AI.IVariable) { // but not a Variable - return new AIVariableExpr(Token.NoToken, (AI.IVariable)e); - } else if (e is IdentifierExpr.ConstantFunApp) { - return ((IdentifierExpr.ConstantFunApp)e).IdentifierExpr; - } else if (e is QuantifierExpr.AIQuantifier) { - return ((QuantifierExpr.AIQuantifier)e).arg.RealQuantifier; - } else { - return (Expr)e; - } - } - public static ExprSeq IExprArray2ExprSeq(IList/**/ a) { - Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - Expr[] e = new Expr[a.Count]; - int i = 0; - foreach (AI.IExpr/*!*/ aei in a) { - Contract.Assert(aei != null); - e[i] = IExpr2Expr(aei); - i++; - } - return new ExprSeq(e); - } - - // Convert a Boogie type into an AIType if possible. This should be - // extended when AIFramework gets more types. - public static AI.AIType Type2AIType(Type t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); - // if (t.IsRef) - // return AI.Ref.Type; - // else - if (t.IsInt) - return AI.Int.Type; - // else if (t.IsName) PR: how to handle this case? - // return AI.FieldName.Type; - else - return AI.Value.Type; - } - } - #region Generic Sequences //--------------------------------------------------------------------- // Generic Sequences diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index c6b66585..607848ed 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -13,7 +13,6 @@ namespace Microsoft.Boogie { using System.Diagnostics; using System.Collections.Generic; using Microsoft.Boogie.AbstractInterpretation; - using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Set = GSet; @@ -818,13 +817,6 @@ namespace Microsoft.Boogie { public bool widenBlock; public int iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not - // Block-specific invariants... - public AI.Lattice Lattice; // The lattice used for the analysis of this block - public AI.Lattice.Element PreInvariant; // The initial abstract states for this block - public AI.Lattice.Element PostInvariant; // The exit abstract states for this block - // KRML: We want to include the following invariant, but at the moment, doing so causes a run-time error (something about committed): - //invariant ; - // VC generation and SCC computation public BlockSeq/*!*/ Predecessors; @@ -837,7 +829,6 @@ namespace Microsoft.Boogie { Contract.Invariant(Label != null); Contract.Invariant(Cmds != null); Contract.Invariant(cce.NonNullElements(liveVarsBefore, true)); - Contract.Invariant((PreInvariant != null) == (PostInvariant != null)); } public bool IsLive(Variable v) { @@ -860,8 +851,6 @@ namespace Microsoft.Boogie { this.Label = label; this.Cmds = cmds; this.TransferCmd = transferCmd; - this.PreInvariant = null; - this.PostInvariant = null; this.Predecessors = new BlockSeq(); this.liveVarsBefore = null; this.TraversingStatus = VisitState.ToVisit; @@ -920,9 +909,6 @@ namespace Microsoft.Boogie { // this.currentlyTraversed = false; this.TraversingStatus = VisitState.ToVisit; this.iterations = 0; - this.Lattice = null; - this.PreInvariant = null; - this.PostInvariant = null; } [Pure] diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index e274fcc3..f2ed5790 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -13,8 +13,6 @@ namespace Microsoft.Boogie { using System.Diagnostics; using System.Collections.Generic; using Microsoft.Boogie.AbstractInterpretation; - using AI = Microsoft.AbstractInterpretationFramework; - using Microsoft.AbstractInterpretationFramework;//DANGER: Added? using System.Diagnostics.Contracts; using Microsoft.Basetypes; @@ -379,21 +377,6 @@ namespace Microsoft.Boogie { args.Add(subexpr); return new NAryExpr(x, new TypeCoercion(x, type), args); } - - - /// - /// This property returns a representation for the expression suitable for use - /// by the AIFramework. Usually, the property just returns "this", but not - /// every Expr is an AI.IExpr (besides, AI.IExpr is to be thought of as an - /// abstract interface--any class that implements AI.IExpr is supposed to - /// implement some proper subinterface of AI.IExpr). - /// The converse operations of this property are found in AbsInt\ExprFactories.ssc. - /// - public abstract AI.IExpr/*!*/ IExpr { - [Peer] - get; - } - } [ContractClassFor(typeof(Expr))] public abstract class ExprContracts : Expr { @@ -412,19 +395,12 @@ namespace Microsoft.Boogie { get { Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - public override Microsoft.AbstractInterpretationFramework.IExpr IExpr { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); } } } - public class LiteralExpr : Expr, AI.IFunApp { + public class LiteralExpr : Expr { public readonly object/*!*/ Val; // false, true, a BigNum, or a BvConst [ContractInvariantMethod] void ObjectInvariant() { @@ -532,12 +508,6 @@ namespace Microsoft.Boogie { return Val is bool && ((bool)Val) == true; } } - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - return this; - } - } // should be eliminated after converting everything to BigNums private int asInt { @@ -572,64 +542,6 @@ namespace Microsoft.Boogie { } } - public AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - if (Val is bool) { - if ((bool)Val) { - return AI.Prop.True; - } else { - return AI.Prop.False; - } - } else if (Val is BigNum) { - return AI.Int.Const((BigNum)Val); - } else if (Val is BvConst) { - return AI.Bv.Const(((BvConst)Val).Value, ((BvConst)Val).Bits); - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // like, where did this value come from?! - } - } - } - public IList/**//*!*/ Arguments { - get { - Contract.Ensures(Contract.Result() != null); - - return ArrayList.ReadOnly(new AI.IExpr[0]); - } - } - public Microsoft.AbstractInterpretationFramework.IFunApp CloneWithArguments(IList/**/ args) { - //Contract.Requires(args != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assert(args.Count == 0); - return this; - } - public AI.AIType/*!*/ AIType { - get { - Contract.Requires(AIType != null); - if (Val is bool) { - return AI.Prop.Type; - } else if (Val is BigNum) { - return AI.Int.Type; - } else if (Val is BvConst) { - return AI.Bv.Type; - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // like, where did this value come from?! - } - } - } - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitFunApp(this); - } - public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); @@ -688,86 +600,6 @@ namespace Microsoft.Boogie { } } - public class AIVariableExpr : Expr { - - public string Name; // identifier symbol - public AI.IVariable/*!*/ Decl; // identifier declaration - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Decl != null); - } - - - /// - /// Creates an unresolved identifier expression. - /// - /// - /// - public AIVariableExpr(IToken/*!*/ tok, AI.IVariable/*!*/ var) - : base(tok) { - Contract.Requires(tok != null); - Contract.Requires(var != null); - Name = var.ToString(); - Decl = var; - } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object obj) { - if (obj == null) - return false; - if (!(obj is AIVariableExpr)) - return false; - - AIVariableExpr other = (AIVariableExpr)obj; - return object.Equals(this.Name, other.Name) && object.Equals(this.Decl, other.Decl); - } - [Pure] - public override int GetHashCode() { - int h = this.Name == null ? 0 : this.Name.GetHashCode(); - h ^= this.Decl == null ? 0 : this.Decl.GetHashCode(); - return h; - } - public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { - //Contract.Requires(stream != null); - if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { - stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h" + this.Decl.GetHashCode()); - } - stream.Write(this, "{0}", this.Name); - } - public override void Resolve(ResolutionContext rc) { - //Contract.Requires(rc != null); - } - public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { - //Contract.Requires(freeVars != null); - if (Decl is Variable) { - freeVars.Add((Variable)Decl); - } - } - public override void Typecheck(TypecheckingContext tc) { - //Contract.Requires(tc != null); - throw new System.NotImplementedException(); - } - public override Type/*!*/ ShallowType { - get { - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - } - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - - return Decl; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitAIVariableExpr(this); - } - } - public class IdentifierExpr : Expr { public string/*!*/ Name; // identifier symbol public Variable Decl; // identifier declaration @@ -894,12 +726,11 @@ namespace Microsoft.Boogie { } } - public sealed class ConstantFunApp : AI.IFunApp { + public sealed class ConstantFunApp { private IdentifierExpr/*!*/ identifierExpr; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(identifierExpr != null); - Contract.Invariant(symbol != null); Contract.Invariant(emptyArgs != null); } @@ -910,14 +741,6 @@ namespace Microsoft.Boogie { } } - private AI.IFunctionSymbol/*!*/ symbol; - public AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - return symbol; - } - } - private static IList/*!*/ emptyArgs = ArrayList.ReadOnly(cce.NonNull((IList/*!*/)new ArrayList())); public IList/*!*/ Arguments { get { @@ -926,44 +749,14 @@ namespace Microsoft.Boogie { } } - public AI.IFunApp CloneWithArguments(IList newargs) { - //Contract.Requires(newargs != null); - Contract.Ensures(Contract.Result() != null); - return this; - } - - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitFunApp(this); - } - public ConstantFunApp(IdentifierExpr ie, Constant c) { Contract.Requires(c != null); Contract.Requires(ie != null); this.identifierExpr = ie; - this.symbol = - new AI.NamedSymbol(c.TypedIdent.Name, BoogieFactory.Type2AIType(c.TypedIdent.Type)); // base(); } } - private AI.IExpr iexprCache = null; - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - - if (iexprCache == null) { - if (Decl is Constant) - iexprCache = new ConstantFunApp(this, (Constant)Decl); - else { - Contract.Assume(this.Decl != null); - iexprCache = Decl; - } - } - return iexprCache; - } - } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); @@ -972,7 +765,7 @@ namespace Microsoft.Boogie { } } - public class OldExpr : Expr, AI.IFunApp // HACK + public class OldExpr : Expr { public Expr/*!*/ Expr; [ContractInvariantMethod] @@ -1030,67 +823,6 @@ namespace Microsoft.Boogie { return Expr.ShallowType; } } - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - - // Put back these lines when "HACK" removed - // // An Old expression has no AI.IExpr representation - // {Contract.Assert(false);throw new cce.UnreachableException();} - return this; // HACK - } - } - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitFunApp(this); - } - public AI.IFunApp CloneWithArguments(IList/**/ args) { - //Contract.Requires(args != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assume(args.Count == 1); - AI.IExpr/*!*/ iexpr = (AI.IExpr)cce.NonNull(args[0]); - return new OldExpr(Token.NoToken, BoogieFactory.IExpr2Expr(iexpr)); - } - private IList/*?*/ argCache = null; - public IList/*() != null); - - if (argCache == null) { - IList l = new ArrayList(1); - l.Add(Expr.IExpr); - argCache = ArrayList.ReadOnly(l); - } - return argCache; - } - } - private sealed class OldFunctionSymbol : AI.IFunctionSymbol { - private static readonly AI.AIType/*!*/ aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type); - - public AI.AIType/*!*/ AIType { - get { - Contract.Ensures(Contract.Result() != null); - return aitype; - } - } - private OldFunctionSymbol() { - } - internal static readonly OldFunctionSymbol/*!*/ Sym = new OldFunctionSymbol(); - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - return "old"; - } - } - public AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - return OldFunctionSymbol.Sym; - } - } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); @@ -1198,10 +930,6 @@ namespace Microsoft.Boogie { /// Type/*!*/ ShallowType(ExprSeq/*!*/ args); - AI.IFunctionSymbol/*!*/ AIFunctionSymbol { - get; - } - T Dispatch(IAppliableVisitor/*!*/ visitor); } [ContractClassFor(typeof(IAppliable))] @@ -1250,13 +978,6 @@ namespace Microsoft.Boogie { throw new NotImplementedException(); } - public IFunctionSymbol AIFunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - public T Dispatch(IAppliableVisitor visitor) { Contract.Requires(visitor != null); throw new NotImplementedException(); @@ -1334,19 +1055,6 @@ namespace Microsoft.Boogie { } } - public AI.IFunctionSymbol/*!*/ AIFunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - switch (this.op) { - case Opcode.Not: - return AI.Prop.Not; - } - System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString()); - throw new Exception(); - } - } - public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); @@ -1537,50 +1245,6 @@ namespace Microsoft.Boogie { } } - public AI.IFunctionSymbol/*!*/ AIFunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - switch (this.op) { - - case Opcode.Add: - return AI.Int.Add; - case Opcode.Sub: - return AI.Int.Sub; - case Opcode.Mul: - return AI.Int.Mul; - case Opcode.Div: - return AI.Int.Div; - case Opcode.Mod: - return AI.Int.Mod; - case Opcode.Eq: - return AI.Value.Eq; - case Opcode.Neq: - return AI.Value.Neq; - case Opcode.Gt: - return AI.Int.Greater; - case Opcode.Ge: - return AI.Int.AtLeast; - case Opcode.Lt: - return AI.Int.Less; - case Opcode.Le: - return AI.Int.AtMost; - case Opcode.And: - return AI.Prop.And; - case Opcode.Or: - return AI.Prop.Or; - case Opcode.Imp: - return AI.Prop.Implies; - case Opcode.Iff: - return AI.Value.Eq; - case Opcode.Subtype: - return AI.Value.Subtype; - } - System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString()); - throw new Exception(); - } - } - public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); @@ -1917,7 +1581,7 @@ namespace Microsoft.Boogie { } - public class FunctionCall : IAppliable, AI.IFunctionSymbol { + public class FunctionCall : IAppliable { private IdentifierExpr/*!*/ name; public Function Func; public FunctionCall(IdentifierExpr name) { @@ -1940,25 +1604,6 @@ namespace Microsoft.Boogie { Contract.Invariant(name != null); } - public FunctionCall createUnresolvedCopy() - { - return new FunctionCall(new IdentifierExpr(name.tok, name.Name, name.Type)); - } - - public AI.IFunctionSymbol/*!*/ AIFunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - if (name.Name == "$typeof") { - return AI.Value.Typeof; - } else if (name.Name == "$allocated") { - return AI.FieldName.Allocated; - } else { - return this; - } - } - } - [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); @@ -1977,15 +1622,6 @@ namespace Microsoft.Boogie { return Func.GetHashCode(); } - public AI.AIType/*!*/ AIType { - get { - Contract.Ensures(Contract.Result() != null); - - Contract.Assume(this.Func != null); - return AI.Value.FunctionType(this.Func.InParams.Length); - } - } - virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); @@ -2139,16 +1775,6 @@ namespace Microsoft.Boogie { return this.Type; } - public AI.IFunctionSymbol/*!*/ AIFunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - // not really clear what should be returned here ... - // should the operation be completely invisible for the abstract interpretation? - return AI.Heap.UnsupportedHeapOp; - } - } - public T Dispatch(IAppliableVisitor visitor) { //Contract.Requires(visitor != null); return visitor.Visit(this); @@ -2156,7 +1782,7 @@ namespace Microsoft.Boogie { } - public class NAryExpr : Expr, AI.IFunApp { + public class NAryExpr : Expr { [Additive] [Peer] public IAppliable/*!*/ Fun; @@ -2264,44 +1890,6 @@ namespace Microsoft.Boogie { } } - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - - return this; - } - } - public AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - - Contract.Ensures(Contract.Result() != null); - - return Fun.AIFunctionSymbol; - } - } - public IList/**//*!*/ Arguments { - get { - Contract.Ensures(Contract.Result() != null); - - AI.IExpr[] a = new AI.IExpr[Args.Length]; - for (int i = 0; i < Args.Length; i++) { - a[i] = cce.NonNull(Args[i]).IExpr; - } - return ArrayList.ReadOnly(a); - } - } - public AI.IFunApp CloneWithArguments(IList/**/ args) { - //Contract.Requires(args != null); - Contract.Ensures(Contract.Result() != null); - return new NAryExpr(this.tok, this.Fun, BoogieFactory.IExprArray2ExprSeq(args)); - } - - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitFunApp(this); - } - public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); @@ -2309,7 +1897,7 @@ namespace Microsoft.Boogie { } } - public class MapSelect : IAppliable, AI.IFunctionSymbol { + public class MapSelect : IAppliable { public readonly int Arity; private readonly IToken/*!*/ tok; @@ -2484,40 +2072,13 @@ namespace Microsoft.Boogie { return Type.InferValueType(mapType.TypeParameters, mapType.Arguments, mapType.Result, actualArgTypes); } - public AI.IFunctionSymbol/*!*/ AIFunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - switch (Arity) { - case 1: - return AI.Heap.Select1; - case 2: - return AI.Heap.Select2; - default: - // Maps with Arity arguments are not fully supported yet - return AI.Heap.UnsupportedHeapOp; - } - } - } - - public AI.AIType/*!*/ AIType { - [Rep] - [ResultNotNewlyAllocated] - get { - Contract.Ensures(Contract.Result() != null); - - return AI.Prop.Type; // THAT is a type? PR: no idea whether this makes sense, - // but it is the type of select1 - } - } - public T Dispatch(IAppliableVisitor visitor) { //Contract.Requires(visitor != null); return visitor.Visit(this); } } - public class MapStore : IAppliable, AI.IFunctionSymbol { + public class MapStore : IAppliable { public readonly int Arity; public readonly IToken/*!*/ tok; @@ -2631,32 +2192,6 @@ namespace Microsoft.Boogie { return cce.NonNull(args[0]).ShallowType; } - public AI.IFunctionSymbol/*!*/ AIFunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - switch (Arity) { - case 1: - return AI.Heap.Update1; - case 2: - return AI.Heap.Update2; - default: - // Maps with Arity arguments are not fully supported yet - return AI.Heap.UnsupportedHeapOp; - } - } - } - - public AI.AIType/*!*/ AIType { - [Rep] - [ResultNotNewlyAllocated] - get { - Contract.Ensures(Contract.Result() != null); - - return AI.Heap.Type; - } - } - public T Dispatch(IAppliableVisitor visitor) { //Contract.Requires(visitor != null); return visitor.Visit(this); @@ -2664,7 +2199,7 @@ namespace Microsoft.Boogie { } - public class IfThenElse : IAppliable, AI.IFunctionSymbol { + public class IfThenElse : IAppliable { public IToken/*!*/ tok; [ContractInvariantMethod] @@ -2758,23 +2293,6 @@ namespace Microsoft.Boogie { return cce.NonNull(args[1]).ShallowType; } - public AI.IFunctionSymbol/*!*/ AIFunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - return this; - } - } - - public AI.AIType/*!*/ AIType { - [Rep] - [ResultNotNewlyAllocated] - get { - Contract.Ensures(Contract.Result() != null); - - return AI.Value.FunctionType(3); - } - } - public T Dispatch(IAppliableVisitor visitor) { //Contract.Requires(visitor != null); return visitor.Visit(this); @@ -2783,7 +2301,7 @@ namespace Microsoft.Boogie { - public class CodeExpr : Expr, AI.IUnknown { + public class CodeExpr : Expr { public VariableSeq/*!*/ LocVars; [Rep] public List/*!*/ Blocks; @@ -2802,18 +2320,6 @@ namespace Microsoft.Boogie { Blocks = blocks; } - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - return this; - } - } - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return this; - } - public override void ComputeFreeVariables(Set /*Variable*/ freeVars) { //Contract.Requires(freeVars != null); // Treat a BlockEexpr as if it has no free variables at all @@ -2894,7 +2400,7 @@ namespace Microsoft.Boogie { } } - public class BvExtractExpr : Expr, AI.IFunApp { + public class BvExtractExpr : Expr { public /*readonly--except in StandardVisitor*/ Expr/*!*/ Bitvector; [ContractInvariantMethod] void ObjectInvariant() { @@ -2987,56 +2493,6 @@ namespace Microsoft.Boogie { } } - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - - return this; - } - } - public AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - return AI.Bv.Extract; - } - } - public IList/**//*!*/ Arguments { - get { - Contract.Ensures(Contract.Result() != null); - - AI.IExpr[] a = new AI.IExpr[3]; - a[0] = Bitvector.IExpr; - a[1] = new LiteralExpr(Token.NoToken, BigNum.FromInt(End)); - a[2] = new LiteralExpr(Token.NoToken, BigNum.FromInt(Start)); - return ArrayList.ReadOnly(a); - } - } - public AI.IFunApp CloneWithArguments(IList/**/ args) { - //Contract.Requires(args != null); - Contract.Ensures(Contract.Result() != null); - AI.IFunApp retFun; - - if (args.Count == 3) { - retFun = new BvExtractExpr(this.tok, - BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr)args[0])), - cce.NonNull((LiteralExpr/*!*/)args[1]).asBigNum.ToIntSafe, - cce.NonNull((LiteralExpr/*!*/)args[2]).asBigNum.ToIntSafe); - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // If we are something wrong is happended - } - return retFun; - } - - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitFunApp(this); - } - public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); @@ -3044,7 +2500,7 @@ namespace Microsoft.Boogie { } } - public class BvConcatExpr : Expr, AI.IFunApp { + public class BvConcatExpr : Expr { public /*readonly--except in StandardVisitor*/ Expr/*!*/ E0, E1; [ContractInvariantMethod] void ObjectInvariant() { @@ -3137,53 +2593,6 @@ namespace Microsoft.Boogie { } } - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - - return this; - } - } - public AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - return AI.Bv.Concat; - } - } - public IList/**//*!*/ Arguments { - get { - Contract.Ensures(Contract.Result() != null); - - AI.IExpr[] a = new AI.IExpr[2]; - a[0] = E0.IExpr; - a[1] = E1.IExpr; - return ArrayList.ReadOnly(a); - } - } - public AI.IFunApp CloneWithArguments(IList/**/ args) { - //Contract.Requires(args != null); - Contract.Ensures(Contract.Result() != null); - AI.IFunApp/*!*/ retFun; - - if (args.Count == 2) { - retFun = new BvConcatExpr(this.tok, - BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr/*!*/)args[0])), - BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr/*!*/)args[1]))); - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // If we are something wrong is happended - } - return retFun; - } - - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitFunApp(this); - } - public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 3f798fd2..05fdb7e4 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -13,7 +13,6 @@ namespace Microsoft.Boogie { using System.Diagnostics; using System.Collections.Generic; using Microsoft.Boogie.AbstractInterpretation; - using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; @@ -38,24 +37,11 @@ namespace Microsoft.Boogie { public BinderExprContracts():base(null,null,null,null,null){ } - public override Microsoft.AbstractInterpretationFramework.IFunctionSymbol FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - public override Type ShallowType { get { throw new NotImplementedException(); } } - - public override Microsoft.AbstractInterpretationFramework.IExpr IExpr { - get { - throw new NotImplementedException(); - } - } } [ContractClass(typeof(BinderExprContracts))] public abstract class BinderExpr : Expr { @@ -217,211 +203,6 @@ namespace Microsoft.Boogie { } return unmentionedParameters; } - - - public abstract AI.IFunctionSymbol/*!*/ FunctionSymbol { - get; - } - - internal sealed class AIQuantifier : AI.IFunApp { - internal readonly AIFunctionRep/*!*/ arg; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(arg != null); - } - - internal AIQuantifier(BinderExpr/*!*/ realQuantifier, int dummyIndex) - : this(new AIFunctionRep(realQuantifier, dummyIndex)) { - Contract.Requires(realQuantifier != null); - } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object obj) { - if (obj == null) - return false; - if (!(obj is AIQuantifier)) - return false; - - AIQuantifier other = (AIQuantifier)obj; - return object.Equals(this.arg, other.arg); - } - [Pure] - public override int GetHashCode() { - return this.arg.GetHashCode(); - } - - private AIQuantifier(AIFunctionRep arg) { - Contract.Requires(arg != null); - this.arg = arg; - // base(); - } - - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitFunApp(this); - } - - public AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - return arg.RealQuantifier.FunctionSymbol; - } - } - - private IList/*?*/ argCache = null; - public IList/**//*!*/ Arguments { - - get { - Contract.Ensures(Contract.Result() != null); - - if (argCache == null) { - IList a = new ArrayList(1); - a.Add(arg); - argCache = ArrayList.ReadOnly(a); - } - return argCache; - } - } - - public AI.IFunApp CloneWithArguments(IList/**/ args) { - //Contract.Requires(args != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assume(args.Count == 1); - - AIFunctionRep rep = args[0] as AIFunctionRep; - if (rep != null) - return new AIQuantifier(rep); - else - throw new System.NotImplementedException(); - } - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - return string.Format("{0}({1})", FunctionSymbol, arg); - } - } - - internal sealed class AIFunctionRep : AI.IFunction { - internal readonly BinderExpr/*!*/ RealQuantifier; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(RealQuantifier != null); - } - - private readonly int dummyIndex; - - internal AIFunctionRep(BinderExpr realQuantifier, int dummyIndex) { - Contract.Requires(realQuantifier != null); - this.RealQuantifier = realQuantifier; - this.dummyIndex = dummyIndex; - Contract.Assert(realQuantifier.TypeParameters.Length == 0); // PR: don't know how to handle this yet - // base(); - } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object obj) { - if (obj == null) - return false; - if (!(obj is AIFunctionRep)) - return false; - - AIFunctionRep other = (AIFunctionRep)obj; - return object.Equals(this.RealQuantifier, other.RealQuantifier) && this.dummyIndex == other.dummyIndex; - } - [Pure] - public override int GetHashCode() { - return this.RealQuantifier.GetHashCode() ^ dummyIndex; - } - - [Pure] - public object DoVisit(AI.ExprVisitor visitor) { - //Contract.Requires(visitor != null); - return visitor.VisitFunction(this); - } - - public AI.IVariable/*!*/ Param { - - get { - Contract.Ensures(Contract.Result() != null); - return cce.NonNull(RealQuantifier.Dummies[dummyIndex]); - } - } - public AI.AIType/*!*/ ParamType { - get { - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - } - - // We lazily convert to 1 dummy per quantifier representation for AIFramework - private AI.IExpr/*?*/ bodyCache = null; - public AI.IExpr/*!*/ Body { - get { - Contract.Ensures(Contract.Result() != null); - - if (bodyCache == null) { - int dummyi = dummyIndex; - int dummylen = RealQuantifier.Dummies.Length; - Contract.Assume(dummylen > dummyi); - - // return the actual body if there are no more dummies - if (dummyi + 1 == dummylen) - bodyCache = RealQuantifier.Body.IExpr; - else { - AIQuantifier innerquant = new AIQuantifier(RealQuantifier, dummyi + 1); - bodyCache = innerquant; - } - } - return bodyCache; - } - } - public AI.IFunction CloneWithBody(AI.IExpr body) { - //Contract.Requires(body != null); - Contract.Ensures(Contract.Result() != null); - BinderExpr realquant; - - AIQuantifier innerquant = body as AIQuantifier; - if (innerquant == null) { - // new quantifier body, clone the real quantifier - realquant = (BinderExpr)RealQuantifier.Clone(); - realquant.Body = BoogieFactory.IExpr2Expr(body); - } else { - if (innerquant.arg.dummyIndex > 0) { - realquant = innerquant.arg.RealQuantifier; - } else { - realquant = (BinderExpr)RealQuantifier.Clone(); - VariableSeq/*!*/ newdummies = new VariableSeq(); - newdummies.Add(Param); - newdummies.AddRange(innerquant.arg.RealQuantifier.Dummies); - realquant.Dummies = newdummies; - realquant.Body = innerquant.arg.RealQuantifier.Body; - } - } - - return new AIFunctionRep(realquant, dummyIndex); - } - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - return string.Format("\\{0} :: {1}", Param, Body); - } - } - - private AI.IExpr aiexprCache = null; - public override AI.IExpr/*!*/ IExpr { - get { - Contract.Ensures(Contract.Result() != null); - - if (TypeParameters.Length > 0) - return new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "anon", Type.Bool)); - if (aiexprCache == null) { - aiexprCache = new AIQuantifier(this, 0); - } - return aiexprCache; - } - } } public class QKeyValue : Absy { @@ -678,13 +459,6 @@ namespace Microsoft.Boogie { Contract.Requires(dummies.Length + typeParams.Length > 0); //:base(tok, typeParams, dummies, null, null, body); // here for aesthetic reasons } - public override AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - return AI.Prop.Forall; - } - } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); @@ -726,13 +500,6 @@ namespace Microsoft.Boogie { Contract.Requires(dummies.Length > 0); //:base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons } - public override AI.IFunctionSymbol/*!*/ FunctionSymbol { - get { - Contract.Ensures(Contract.Result() != null); - - return AI.Prop.Exists; - } - } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); @@ -1006,15 +773,6 @@ namespace Microsoft.Boogie { } } - public override AI.IFunctionSymbol/*!*/ FunctionSymbol { - - get { - Contract.Ensures(Contract.Result() != null); - - return AI.Prop.Lambda; - } - } - public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index a22ece7d..706d6298 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -13,7 +13,6 @@ namespace Microsoft.Boogie { using System.Diagnostics; using System.Collections.Generic; using Microsoft.Boogie.AbstractInterpretation; - using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; //===================================================================== diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 9c721703..a2ad40f6 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -12,7 +12,6 @@ using System.Text; using Microsoft.Boogie; using Microsoft.Basetypes; using Bpl = Microsoft.Boogie; -using AI = Microsoft.AbstractInterpretationFramework; COMPILER BoogiePL @@ -115,7 +114,6 @@ private class BvBounds : Expr { {Contract.Assert(false);throw new cce.UnreachableException();} } public override void ComputeFreeVariables(GSet/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} } - public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } } } /*--------------------------------------------------------------------------*/ diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 73fa8946..55f15454 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -609,26 +609,9 @@ namespace Microsoft.Boogie { } public class AiFlags { - public bool Intervals = false; - public bool Constant = false; - public bool DynamicType = false; - public bool Nullness = false; - public bool Polyhedra = false; public bool J_Trivial = false; public bool J_Intervals = false; public bool DebugStatistics = false; - - public bool AnySet { - get { - return Intervals - || Constant - || DynamicType - || Nullness - || Polyhedra - || J_Trivial - || J_Intervals; - } - } } public AiFlags/*!*/ Ai = new AiFlags(); @@ -639,26 +622,6 @@ namespace Microsoft.Boogie { if (ps.ConfirmArgumentCount(1)) { foreach (char c in cce.NonNull(args[ps.i])) { switch (c) { - case 'i': - Ai.Intervals = true; - UseAbstractInterpretation = true; - break; - case 'c': - Ai.Constant = true; - UseAbstractInterpretation = true; - break; - case 'd': - Ai.DynamicType = true; - UseAbstractInterpretation = true; - break; - case 'n': - Ai.Nullness = true; - UseAbstractInterpretation = true; - break; - case 'p': - Ai.Polyhedra = true; - UseAbstractInterpretation = true; - break; case 't': Ai.J_Trivial = true; UseAbstractInterpretation = true; @@ -697,12 +660,6 @@ namespace Microsoft.Boogie { } return true; - case "logInfer": - if (ps.ConfirmArgumentCount(0)) { - Microsoft.AbstractInterpretationFramework.Lattice.LogSwitch = true; - } - return true; - case "break": case "launch": if (ps.ConfirmArgumentCount(0)) { @@ -1502,7 +1459,6 @@ namespace Microsoft.Boogie { perform interprocedural inference (deprecated, not supported) /contractInfer perform procedure contract inference - /logInfer print debug output during inference /instrumentInfer h - instrument inferred invariants only at beginning of loop headers (default) diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 9a24b6b2..3a2f421a 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -172,10 +172,6 @@ - - {39B0658D-C955-41C5-9A43-48C97A1EF5FD} - AIFramework - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} Basetypes diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 69f505bc..e95bccda 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -6,7 +6,6 @@ using System.Text; using Microsoft.Boogie; using Microsoft.Basetypes; using Bpl = Microsoft.Boogie; -using AI = Microsoft.AbstractInterpretationFramework; @@ -134,7 +133,6 @@ private class BvBounds : Expr { {Contract.Assert(false);throw new cce.UnreachableException();} } public override void ComputeFreeVariables(GSet/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} } - public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } } } /*--------------------------------------------------------------------------*/ diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 9bbeada1..66eee658 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -63,11 +63,6 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return node.StdDispatch(this); } - public virtual AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) { - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - return node; - } public virtual Cmd VisitAssertCmd(AssertCmd node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 64f5fbbb..39733c8e 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -22,7 +22,6 @@ namespace Microsoft.Dafny using System.Diagnostics; using VC; using System.CodeDom.Compiler; - using AI = Microsoft.AbstractInterpretationFramework; public class DafnyDriver { @@ -536,9 +535,6 @@ namespace Microsoft.Dafny if (CommandLineOptions.Clo.UseAbstractInterpretation) { if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial) { Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); - } else if (CommandLineOptions.Clo.Ai.AnySet) { - // run one of the old domains - Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program); } else { // use /infer:j as the default CommandLineOptions.Clo.Ai.J_Intervals = true; diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index b47512bd..f27cd410 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -11,7 +11,6 @@ using Microsoft.Boogie.VCExprAST; using VC; using System.Collections; using System.IO; -using Microsoft.AbstractInterpretationFramework; using Graphing; namespace Microsoft.Boogie.Houdini { @@ -485,17 +484,18 @@ namespace Microsoft.Boogie.Houdini { public bool MatchCandidate(Expr boogieExpr, out Variable candidateConstant) { candidateConstant = null; - IExpr antecedent, consequent; - IExpr expr = boogieExpr as IExpr; - if (expr != null && ExprUtil.Match(expr, Prop.Implies, out antecedent, out consequent)) { - IdentifierExpr.ConstantFunApp constantFunApp = antecedent as IdentifierExpr.ConstantFunApp; - if (constantFunApp != null && houdiniConstants.Contains(constantFunApp.IdentifierExpr.Decl)) { - candidateConstant = constantFunApp.IdentifierExpr.Decl; + NAryExpr e = boogieExpr as NAryExpr; + if (e != null && e.Fun is BinaryOperator && ((BinaryOperator)e.Fun).Op == BinaryOperator.Opcode.Imp) { + Expr antecedent = e.Args[0]; + Expr consequent = e.Args[1]; + + IdentifierExpr id = antecedent as IdentifierExpr; + if (id != null && id.Decl is Constant && houdiniConstants.Contains((Constant)id.Decl)) { + candidateConstant = id.Decl; return true; } - var e = consequent as Expr; - if (e != null && MatchCandidate(e, out candidateConstant)) + if (MatchCandidate(consequent, out candidateConstant)) return true; } return false; diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index af1755a3..97d26001 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -82,10 +82,6 @@ - - {39B0658D-C955-41C5-9A43-48C97A1EF5FD} - AIFramework - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} Basetypes diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj index 3dc042a6..c2d68fc8 100644 --- a/Source/Provers/SMTLib/SMTLib.csproj +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -159,10 +159,6 @@ - - {39B0658D-C955-41C5-9A43-48C97A1EF5FD} - AIFramework - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} Basetypes diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index f9511dbd..bf123823 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -129,10 +129,6 @@ - - {39B0658D-C955-41C5-9A43-48C97A1EF5FD} - AIFramework - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} Basetypes diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 4e9c5c10..1561aec0 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -339,15 +339,6 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////// - public override AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assert(false); - throw new cce.UnreachableException(); - } - - /////////////////////////////////////////////////////////////////////////////////// - public override Expr VisitIdentifierExpr(IdentifierExpr node) { //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj index 18455b6e..bd426125 100644 --- a/Source/VCExpr/VCExpr.csproj +++ b/Source/VCExpr/VCExpr.csproj @@ -162,10 +162,6 @@ - - {39B0658D-C955-41C5-9A43-48C97A1EF5FD} - AIFramework - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} Basetypes diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 9837626d..ca0c0e59 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -11,7 +11,6 @@ using System.Threading; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs index 8571caee..d7e297cd 100644 --- a/Source/VCGeneration/DoomCheck.cs +++ b/Source/VCGeneration/DoomCheck.cs @@ -12,7 +12,6 @@ using System.Threading; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs index b0821240..5f00a3cf 100644 --- a/Source/VCGeneration/DoomErrorHandler.cs +++ b/Source/VCGeneration/DoomErrorHandler.cs @@ -6,7 +6,6 @@ using System.Threading; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/DoomedLoopUnrolling.cs b/Source/VCGeneration/DoomedLoopUnrolling.cs index 9d58d227..5469a1db 100644 --- a/Source/VCGeneration/DoomedLoopUnrolling.cs +++ b/Source/VCGeneration/DoomedLoopUnrolling.cs @@ -6,7 +6,6 @@ using System.Threading; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/DoomedStrategy.cs b/Source/VCGeneration/DoomedStrategy.cs index 18de31c7..c08662b1 100644 --- a/Source/VCGeneration/DoomedStrategy.cs +++ b/Source/VCGeneration/DoomedStrategy.cs @@ -11,7 +11,6 @@ using System.Threading; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/HasseDiagram.cs b/Source/VCGeneration/HasseDiagram.cs index db777336..d5fdfb66 100644 --- a/Source/VCGeneration/HasseDiagram.cs +++ b/Source/VCGeneration/HasseDiagram.cs @@ -11,7 +11,6 @@ using System.Threading; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index a2ad1bd3..5c6a5f68 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -8,7 +8,6 @@ using System.Text; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index e7f5999a..6efae58c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -12,7 +12,6 @@ using System.Threading; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index 15c6e2aa..962f9f26 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -11,7 +11,6 @@ using System.Threading; using System.IO; using Microsoft.Boogie; using Graphing; -using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts; using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index fe7ddc70..98958c66 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -1,228 +1,224 @@ - - - - Debug - AnyCPU - 9.0.21022 - 2.0 - {E1F10180-C7B9-4147-B51F-FA1B701966DC} - Library - Properties - VCGeneration - VCGeneration - v4.0 - 512 - 1 - true - ..\InterimKey.snk - - - 3.5 - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - false - true - Client - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - False - False - True - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - - - - - - - Full - %28none%29 - AllRules.ruleset - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - AllRules.ruleset - - - true - bin\z3apidebug\ - DEBUG;TRACE - full - AnyCPU - - - true - GlobalSuppressions.cs - prompt - Migrated rules for VCGeneration.ruleset - true - - - true - bin\Checked\ - DEBUG;TRACE - full - AnyCPU - bin\Debug\VCGeneration.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - AllRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - False - Full - Build - 0 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - {39B0658D-C955-41C5-9A43-48C97A1EF5FD} - AIFramework - - - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} - Basetypes - - - {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} - CodeContractsExtender - - - {B230A69C-C466-4065-B9C1-84D80E76D802} - Core - - - {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} - Graph - - - {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} - Model - - - {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} - ParserHelper - - - {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} - VCExpr - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Windows Installer 3.1 - true - - - + + + + Debug + AnyCPU + 9.0.21022 + 2.0 + {E1F10180-C7B9-4147-B51F-FA1B701966DC} + Library + Properties + VCGeneration + VCGeneration + v4.0 + 512 + 1 + true + ..\InterimKey.snk + + + 3.5 + + publish\ + true + Disk + false + Foreground + 7 + Days + false + false + true + 0 + 1.0.0.%2a + false + false + true + Client + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + False + False + True + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + + + + + + + Full + %28none%29 + AllRules.ruleset + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + AllRules.ruleset + + + true + bin\z3apidebug\ + DEBUG;TRACE + full + AnyCPU + + + true + GlobalSuppressions.cs + prompt + Migrated rules for VCGeneration.ruleset + true + + + true + bin\Checked\ + DEBUG;TRACE + full + AnyCPU + bin\Debug\VCGeneration.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + True + False + True + False + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + False + Full + Build + 0 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} + Basetypes + + + {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} + CodeContractsExtender + + + {B230A69C-C466-4065-B9C1-84D80E76D802} + Core + + + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} + Graph + + + {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} + Model + + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + + + {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} + VCExpr + + + + + + + + False + .NET Framework 3.5 SP1 Client Profile + false + + + False + .NET Framework 3.5 SP1 + true + + + False + Windows Installer 3.1 + true + + + + --> \ No newline at end of file diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer index 73a9509c..fe848aab 100644 --- a/Test/aitest0/Answer +++ b/Test/aitest0/Answer @@ -23,29 +23,29 @@ implementation Join(b: bool) x := 3; y := 4; z := x + y; - assume {:inferred} x == 3 && y == 4 && z == 7; - goto Then, Else; + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; + goto Then, Else; Then: - assume {:inferred} x == 3 && y == 4 && z == 7; + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; assume b <==> true; x := x + 1; - assume {:inferred} x == 4 && y == 4 && z == 7; + assume {:inferred} GlobalFlag && x == 4 && y == 4 && z == 7 && b; goto join; Else: - assume {:inferred} x == 3 && y == 4 && z == 7; + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; assume b <==> false; y := 4; - assume {:inferred} x == 3 && y == 4 && z == 7; + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7 && !b; goto join; join: - assume {:inferred} y == 4 && z == 7; + assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7; assert y == 4; assert z == 7; assert GlobalFlag <==> true; - assume {:inferred} y == 4 && z == 7; + assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7; return; } @@ -68,20 +68,20 @@ implementation Loop() goto test; test: // cut point - assume {:inferred} c == 0; - assume {:inferred} c == 0; + assume {:inferred} c == 0 && 0 <= i && i < 11; + assume {:inferred} c == 0 && 0 <= i && i < 11; goto Then, Else; Then: - assume {:inferred} c == 0; + assume {:inferred} c == 0 && 0 <= i && i < 11; assume i < 10; i := i + 1; - assume {:inferred} c == 0; + assume {:inferred} c == 0 && 1 <= i && i < 11; goto test; Else: - assume {:inferred} c == 0; - assume {:inferred} c == 0; + assume {:inferred} c == 0 && 0 <= i && i < 11; + assume {:inferred} c == 0 && 0 <= i && i < 11; return; } diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat index 1cb7a60c..b6ab77f0 100644 --- a/Test/aitest0/runtest.bat +++ b/Test/aitest0/runtest.bat @@ -3,5 +3,5 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe -%BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl +%BGEXE% %* -infer:j -instrumentInfer:e -printInstrumented -noVerify constants.bpl %BGEXE% %* -infer:j Intervals.bpl diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer index 718e7171..dd5bcff2 100644 --- a/Test/aitest1/Answer +++ b/Test/aitest1/Answer @@ -14,21 +14,21 @@ implementation SimpleLoop() goto test; test: // cut point - assume {:inferred} 0 <= i; - assume {:inferred} 0 <= i; + assume {:inferred} 0 <= i && i < 11; + assume {:inferred} 0 <= i && i < 11; goto Then, Else; Then: - assume {:inferred} 0 <= i; + assume {:inferred} 0 <= i && i < 11; assume i < 10; i := i + 1; - assume {:inferred} i <= 10 && 1 <= i; + assume {:inferred} 1 <= i && i < 11; goto test; Else: - assume {:inferred} 0 <= i; + assume {:inferred} 0 <= i && i < 11; assume !(i < 10); - assume {:inferred} 10 <= i; + assume {:inferred} 0 <= i && i < 11; return; } @@ -57,13 +57,13 @@ implementation VariableBoundLoop(n: int) assume {:inferred} 0 <= i; assume i < n; i := i + 1; - assume {:inferred} i <= n && 1 <= i; + assume {:inferred} 1 <= i && 1 <= n; goto test; Else: assume {:inferred} 0 <= i; assume !(i < n); - assume {:inferred} n <= i && 0 <= i; + assume {:inferred} 0 <= i; return; } @@ -104,7 +104,7 @@ implementation FooToo() i := 3 * (i + 1); i := 1 + 3 * i; i := (i + 1) * 3; - assume {:inferred} 1 / 3 * i == 155; + assume {:inferred} i == 465; return; } @@ -125,7 +125,7 @@ implementation FooTooStepByStep() i := 3 * (i + 1); i := 1 + 3 * i; i := (i + 1) * 3; - assume {:inferred} 1 / 3 * i == 155; + assume {:inferred} i == 465; return; } @@ -212,7 +212,7 @@ implementation p() start: assume {:inferred} true; assume x < y; - assume {:inferred} x + 1 <= y; + assume {:inferred} true; return; } @@ -235,18 +235,18 @@ implementation p() A: assume {:inferred} true; assume x < y; - assume {:inferred} x + 1 <= y; + assume {:inferred} true; goto B, C; B: - assume {:inferred} x + 1 <= y; + assume {:inferred} true; x := x * x; assume {:inferred} true; return; C: - assume {:inferred} x + 1 <= y; - assume {:inferred} x + 1 <= y; + assume {:inferred} true; + assume {:inferred} true; return; } @@ -275,19 +275,19 @@ implementation p() B: assume {:inferred} -1 <= x; assume x < y; - assume {:inferred} x + 1 <= y && -1 <= x; + assume {:inferred} -1 <= x && 0 <= y; goto C, E; C: - assume {:inferred} x + 1 <= y && -1 <= x; + assume {:inferred} -1 <= x && 0 <= y; x := x * x; - assume {:inferred} 0 <= y; + assume {:inferred} x < 2 && 0 <= y; goto D, E; D: - assume {:inferred} 0 <= y; + assume {:inferred} x < 2 && 0 <= y; x := y; - assume {:inferred} x == y && 0 <= y; + assume {:inferred} 0 <= x && 0 <= y; return; E: @@ -333,8 +333,8 @@ implementation p() goto D; D: - assume {:inferred} 9 <= x && x <= 10; - assume {:inferred} 9 <= x && x <= 10; + assume {:inferred} 9 <= x && x < 11; + assume {:inferred} 9 <= x && x < 11; return; } @@ -363,13 +363,13 @@ implementation p() B: assume {:inferred} true; assume x <= 0; - assume {:inferred} x <= 0; + assume {:inferred} x < 1; goto D; C: assume {:inferred} true; assume y <= 0; - assume {:inferred} y <= 0; + assume {:inferred} y < 1; goto D; D: @@ -402,7 +402,7 @@ implementation foo() i := i + 1; i := i + 1; j := j + 1; - assume {:inferred} i == j + 4 && j == 1 && n == 0; + assume {:inferred} i == 5 && j == 1 && n == 0; return; } @@ -425,20 +425,20 @@ implementation foo() assume n >= 4; i := 0; j := i + 1; - assume {:inferred} j == i + 1 && i == 0 && 4 <= n; + assume {:inferred} i == 0 && j == 1 && 4 <= n; goto exit, loop0; loop0: // cut point - assume {:inferred} 4 <= n && 0 <= i && j == i + 1; + assume {:inferred} 0 <= i && 1 <= j && 4 <= n; assume j <= n; i := i + 1; j := j + 1; - assume {:inferred} j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n; + assume {:inferred} 1 <= i && 2 <= j && 4 <= n; goto loop0, exit; exit: - assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1; - assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1; + assume {:inferred} 0 <= i && 1 <= j && 4 <= n; + assume {:inferred} 0 <= i && 1 <= j && 4 <= n; return; } @@ -446,5 +446,10 @@ implementation foo() Boogie program verifier finished with 0 verified, 0 errors -------------------- Bound.bpl -------------------- +Bound.bpl(24,3): Error BP5001: This assertion might not hold. +Execution trace: + Bound.bpl(8,1): start + Bound.bpl(14,1): LoopHead + Bound.bpl(22,1): AfterLoop -Boogie program verifier finished with 1 verified, 0 errors +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/aitest1/runtest.bat b/Test/aitest1/runtest.bat index 3b2c382c..6e8a7bb1 100644 --- a/Test/aitest1/runtest.bat +++ b/Test/aitest1/runtest.bat @@ -7,11 +7,11 @@ for %%f in (ineq.bpl Linear0.bpl Linear1.bpl Linear2.bpl Linear3.bpl Linear4.bpl Linear5.bpl Linear6.bpl Linear7.bpl Linear8.bpl Linear9.bpl) do ( echo -------------------- %%f -------------------- - %BGEXE% %* -infer:p -instrumentInfer:e -printInstrumented -noVerify %%f + %BGEXE% %* -infer:j -instrumentInfer:e -printInstrumented -noVerify %%f ) for %%f in (Bound.bpl) do ( echo -------------------- %%f -------------------- - %BGEXE% %* -infer:p %%f + %BGEXE% %* -infer:j %%f ) diff --git a/Test/aitest9/runtest.bat b/Test/aitest9/runtest.bat index bafa6961..e66f7e2b 100644 --- a/Test/aitest9/runtest.bat +++ b/Test/aitest9/runtest.bat @@ -7,5 +7,5 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe for %%f in (VarMapFixPoint.bpl TestIntervals.bpl) do ( echo. echo -------------------- %%f -------------------- - %BPLEXE% %* %%f /infer:i + %BPLEXE% %* %%f /infer:j ) -- cgit v1.2.3