diff options
| author |  boehmes <unknown> | 2012-09-27 17:13:40 +0200 |
|---|---|---|
| committer | boehmes <unknown> | 2012-09-27 17:13:40 +0200 |
| commit | ed83becd12d7079e6ce2853fbebace20b1e7df5a (patch) | |
| tree | 129c09df268f51abf941aec3971e213bd19eac06 | |
| parent | ac41d9d5613640f06e8b553869cbba65c4183967 (diff) | |
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.
40 files changed, 317 insertions, 2753 deletions
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 @@ <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
- <Compile Include="AbstractInterpretation.cs" />
- <Compile Include="ExprFactories.cs" />
<Compile Include="IntervalDomain.cs" />
- <Compile Include="LoopInvariantsOnDemand.cs" />
<Compile Include="TrivialDomain.cs" />
<Compile Include="NativeLattice.cs" />
<Compile Include="Traverse.cs" />
<Compile Include="..\version.cs" />
</ItemGroup>
<ItemGroup>
- <ProjectReference Include="..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
<Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
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;
-
-
- /// <summary>
- /// Defines invariant propagation methods over ASTs for an abstract interpretation policy.
- /// </summary>
- public class AbstractionEngine {
- private AI.Lattice lattice;
- private Queue<ProcedureWorkItem> procWorkItems; //PM: changed to generic queue
- private Queue/*<CallSite>*/ 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<ProcedureWorkItem>();
- this.callReturnWorkItems = new Queue();
- }
-
- public static Dictionary<Procedure, Implementation[]> 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<AI.Lattice.Element>() != 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<Variable!>;
- Contract.Assume(call.Ins[i] != null); //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;
- 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);
- }
-
- /// <summary>
- /// Compute the invariants for the program using the underlying abstract domain
- /// </summary>
- public void ComputeProgramInvariants(Program program) {
- Contract.Requires(program != null);
-
- Dictionary<Procedure, Implementation[]> 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<Variable>() != 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);
-
- /// <summary>
- /// Given a basic block, it propagates the abstract state at the entry point through the exit point of the block
- /// <param name="impl"> The implementation that owns the block </param>
- /// <param name="block"> The from where we propagate </param>
- /// <param name="statementIndex"> </param>
- /// <param name="currentValue"> The initial value </param>
- /// </summary>
- 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
- }
-
- /// <summary>
- /// The abstract transition relation.
- /// </summary>
- 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<AI.Lattice.Element>() != 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<AssignLhs>(assmt.Lhss, lhs => lhs.DeepAssignedVariable != null));//TODO: Check my work, please, Mike.
-
- List<IdentifierExpr/*!>!*/> freshLhs = new List<IdentifierExpr/*!*/>();
- 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<Expr/*!>!*/> 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;
- }
-
- /// <summary>
- /// Flatten an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R]
- /// </summary>
- private List<Expr/*!>!*/> flatConjunction(Expr embeddedExpr) {
- Contract.Requires(embeddedExpr != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expr>>()));
-
- var retValue = new List<Expr/*!*/>();
- 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;
- }
-
- /// <summary>
- /// Compute the invariants for a basic block
- /// <param name="impl"> The implementation the block belongs to </param>
- /// <param name="block"> The block for which we compute the invariants </param>
- /// <param name="incomingValue"> The "init" abstract state for the block </param>
- /// </summary>
- 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<AI.IVariable!>! freeVarsOfA = freeVarsVisitorForA.FreeVariables;
- List<AI.IVariable!>! 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<AI.IVariable!>! vars)
- {
- string s = "";
-
- foreach(AI.IVariable! v in vars)
- {
- s += v.Name +" ";
- }
- return s;
- }
-#endif
-
- } // class
-
-
- /// <summary>
- /// Defines a class for building the abstract domain according to the parameters switch
- /// </summary>
- public class AbstractDomainBuilder {
-
- private AbstractDomainBuilder() { /* do nothing */
- }
-
- /// <summary>
- /// Return a fresh instance of the abstract domain of intervals
- /// </summary>
- static public AbstractAlgebra BuildIntervalsAbstractDomain() {
- Contract.Ensures(Contract.Result<AbstractAlgebra>() != 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;
- }
-
- /// <summary>
- /// Return a fresh abstract domain, according to the parameters specified by the command line
- /// </summary>
- static public AbstractAlgebra BuildAbstractDomain() {
- Contract.Ensures(Contract.Result<AbstractAlgebra>() != 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;
-
- }
- }
-
- /// <summary>
- /// An Abstract Algebra is a tuple made of a Lattice and several factories
- /// </summary>
- 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<AI.Lattice>() != 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 {
- /// <summary>
- /// Run the abstract interpretation.
- /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn
- /// </summary>
- 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<AI.IFunApp>() != null);
-
- return Expr.False;
- }
- }
- public AI.IFunApp True {
- get {
- Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
-
- return Expr.True;
- }
- }
-
- public AI.IFunApp Not(AI.IExpr p) {
- //Contract.Requires(p != null);
- Contract.Ensures(Contract.Result<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != null);
- return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1));
- }
- public AI.IExpr Term(Rational r, AI.IVariable var) {
- Contract.Ensures(Contract.Result<AI.IExpr>() != 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<AI.IFunApp>() != null);
-
- return Expr.False;
- }
- }
- public AI.IFunApp True {
- get {
- Contract.Ensures(Contract.Result<AI.IFunApp>() != 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<AI.IFunApp>() != null);
-
- return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));
- }
- }
-
- public class BoogieTypeFactory : BoogieFactory, AI.ITypeExprFactory {
- /// <summary>
- /// Returns an expression denoting the top of the type hierarchy.
- /// </summary>
- public AI.IExpr RootType {
- get {
- Contract.Assert(false); // BUGBUG: TODO
- throw new System.NotImplementedException();
- }
- }
-
- /// <summary>
- /// Returns true iff "t" denotes a type constant.
- /// </summary>
- [Pure]
- public bool IsTypeConstant(AI.IExpr t) {
- //Contract.Requires(t != null);
- Contract.Ensures(Contract.Result<bool>() == (t is Constant));
- return t is Constant;
- }
-
- /// <summary>
- /// Returns true iff t0 and t1 are types such that t0 and t1 are equal.
- /// </summary>
- [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;
- }
-
- /// <summary>
- /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.
- /// </summary>
- [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();
- }
-
- /// <summary>
- /// Returns the most derived supertype of both "t0" and "t1". A precondition is
- /// that "t0" and "t1" both represent types.
- /// </summary>
- public AI.IExpr JoinTypes(AI.IExpr t0, AI.IExpr t1) {
- //Contract.Requires(t0 != null);
- //Contract.Requires(t1 != null);
- Contract.Ensures(Contract.Result<AI.IExpr>() != 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<AI.IFunApp>() != 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<AI.IFunApp>() != 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;
-
-
-
- /// <summary>
- /// A visitor of an abstract interpretation expression that collects the free variables
- /// </summary>
- class FreeVariablesVisitor : AI.ExprVisitor {
- [Peer]
- List<AI.IVariable> variables;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(variables));
- Contract.Invariant(cce.NonNullElements(varNames));
- }
-
- public List<AI.IVariable> FreeVariables {
- get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<AI.IVariable>>()));
-
- return this.variables;
- }
- }
-
- List<string> varNames; // used to check the consinstency!
-
- public FreeVariablesVisitor() {
- this.variables = new List<AI.IVariable>();
- this.varNames = new List<string>();
- }
-
- 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<Procedure, Implementation[]> procedureImplementations = AbstractionEngine.ComputeProcImplMap(program);
+ Dictionary<Procedure, Implementation[]> 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<Procedure, Implementation[]> 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);
+ }
+
/// <summary>
- /// 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.
/// </summary>
public static void ComputeProgramInvariants(Program program, Dictionary<Procedure, Implementation[]> 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 @@ <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>
<Name>AbsInt</Name>
</ProjectReference>
- <ProjectReference Include="..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
<Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
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<CallSite>/*!*/ 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<CallSite>();
// 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<object>;
@@ -349,12 +332,6 @@ namespace Microsoft.Boogie { }
}
- public void InstrumentWithInvariants() {
- foreach (Declaration d in this.TopLevelDeclarations) {
- d.InstrumentWithInvariants();
- }
- }
-
/// <summary>
/// Reset the abstract stated computed before
/// </summary>
@@ -1045,14 +1022,6 @@ namespace Microsoft.Boogie { }
/// <summary>
- /// This method inserts the abstract-interpretation-inferred invariants
- /// as assume (or possibly assert) statements in the statement sequences of
- /// each block.
- /// </summary>
- public virtual void InstrumentWithInvariants() {
- }
-
- /// <summary>
/// Reset the abstract stated computed before
/// </summary>
public virtual void ResetAbstractInterpretationState() { /* does nothing */
@@ -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();
}
}
@@ -2862,53 +2820,6 @@ namespace Microsoft.Boogie { }
/// <summary>
- /// Instrument the blocks with the inferred invariants
- /// </summary>
- 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<object>(), 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<object>(), 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;
- }
- }
- }
- }
-
- /// <summary>
/// Return a collection of blocks that are reachable from the block passed as a parameter.
/// The block must be defined in the current implementation
/// </summary>
@@ -3148,113 +3059,6 @@ namespace Microsoft.Boogie { }
}
- /// <summary>
- /// 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.
- /// </summary>
- 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;
- }
- }
- /// <summary>
- /// 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.
- /// </summary>
- /// <param name="lattice"></param>
- /// <returns></returns>
- 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<Expr>() != 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/*<AI.IExpr!>*/ a) {
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExprSeq>() != 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<AI.AIType>() != 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<object>;
@@ -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);
}
-
-
- /// <summary>
- /// 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.
- /// </summary>
- public abstract AI.IExpr/*!*/ IExpr {
- [Peer]
- get;
- }
-
}
[ContractClassFor(typeof(Expr))]
public abstract class ExprContracts : Expr {
@@ -415,16 +398,9 @@ namespace Microsoft.Boogie { throw new NotImplementedException();
}
}
- public override Microsoft.AbstractInterpretationFramework.IExpr IExpr {
- get {
- Contract.Ensures(Contract.Result<Microsoft.AbstractInterpretationFramework.IExpr>() != 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<AI.IExpr>() != 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<IFunctionSymbol>() != 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/*<AI.IExpr!>*//*!*/ Arguments {
- get {
- Contract.Ensures(Contract.Result<IList>() != null);
-
- return ArrayList.ReadOnly(new AI.IExpr[0]);
- }
- }
- public Microsoft.AbstractInterpretationFramework.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<Microsoft.AbstractInterpretationFramework.IFunApp>() != 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<Absy>() != 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);
- }
-
-
- /// <summary>
- /// Creates an unresolved identifier expression.
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="name"></param>
- 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<Type>() != null);
- throw new System.NotImplementedException();
- }
- }
- public override AI.IExpr/*!*/ IExpr {
- get {
- Contract.Ensures(Contract.Result<AI.IExpr>() != null);
-
- return Decl;
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != 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<IFunctionSymbol>() != 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<AI.IFunApp>() != 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<IExpr>() != 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<IExpr>() != 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/*<IExpr!>*/ args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<AI.IFunApp>() != 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/*<IExpr!*//*!*/ Arguments {
-
- get {
- Contract.Ensures(Contract.Result<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<AIType>() != null);
- return aitype;
- }
- }
- private OldFunctionSymbol() {
- }
- internal static readonly OldFunctionSymbol/*!*/ Sym = new OldFunctionSymbol();
-
- [Pure]
- public override string ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return "old";
- }
- }
- public AI.IFunctionSymbol/*!*/ FunctionSymbol {
- get {
- Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
- return OldFunctionSymbol.Sym;
- }
- }
public override Absy StdDispatch(StandardVisitor visitor) {
//Contract.Requires(visitor != null);
@@ -1198,10 +930,6 @@ namespace Microsoft.Boogie { /// </summary>
Type/*!*/ ShallowType(ExprSeq/*!*/ args);
- AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
- get;
- }
-
T Dispatch<T>(IAppliableVisitor<T>/*!*/ visitor);
}
[ContractClassFor(typeof(IAppliable))]
@@ -1250,13 +978,6 @@ namespace Microsoft.Boogie { throw new NotImplementedException();
}
- public IFunctionSymbol AIFunctionSymbol {
- get {
- Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
- throw new NotImplementedException();
- }
- }
-
public T Dispatch<T>(IAppliableVisitor<T> visitor) {
Contract.Requires(visitor != null);
throw new NotImplementedException();
@@ -1334,19 +1055,6 @@ namespace Microsoft.Boogie { }
}
- public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
- get {
- Contract.Ensures(Contract.Result<IFunctionSymbol>() != 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<IFunctionSymbol>() != 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<IFunctionSymbol>() != 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<string>() != null);
@@ -1977,15 +1622,6 @@ namespace Microsoft.Boogie { return Func.GetHashCode();
}
- public AI.AIType/*!*/ AIType {
- get {
- Contract.Ensures(Contract.Result<AIType>() != 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<IFunctionSymbol>() != 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<T>(IAppliableVisitor<T> 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<IExpr>() != null);
-
- return this;
- }
- }
- public AI.IFunctionSymbol/*!*/ FunctionSymbol {
- get {
-
- Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
-
- return Fun.AIFunctionSymbol;
- }
- }
- public IList/*<AI.IExpr!>*//*!*/ Arguments {
- get {
- Contract.Ensures(Contract.Result<IList>() != 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/*<AI.IExpr!>*/ args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<AI.IFunApp>() != 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<Absy>() != 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<IFunctionSymbol>() != 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<AIType>() != 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<T>(IAppliableVisitor<T> 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<IFunctionSymbol>() != 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<AIType>() != null);
-
- return AI.Heap.Type;
- }
- }
-
public T Dispatch<T>(IAppliableVisitor<T> 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<IFunctionSymbol>() != null);
- return this;
- }
- }
-
- public AI.AIType/*!*/ AIType {
- [Rep]
- [ResultNotNewlyAllocated]
- get {
- Contract.Ensures(Contract.Result<AIType>() != null);
-
- return AI.Value.FunctionType(3);
- }
- }
-
public T Dispatch<T>(IAppliableVisitor<T> 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<Block/*!*/>/*!*/ Blocks;
@@ -2802,18 +2320,6 @@ namespace Microsoft.Boogie { Blocks = blocks;
}
- public override AI.IExpr/*!*/ IExpr {
- get {
- Contract.Ensures(Contract.Result<IExpr>() != 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<IExpr>() != null);
-
- return this;
- }
- }
- public AI.IFunctionSymbol/*!*/ FunctionSymbol {
- get {
- Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
-
- return AI.Bv.Extract;
- }
- }
- public IList/*<AI.IExpr!>*//*!*/ Arguments {
- get {
- Contract.Ensures(Contract.Result<IList>() != 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/*<AI.IExpr!>*/ args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<AI.IFunApp>() != 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<Absy>() != 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<IExpr>() != null);
-
- return this;
- }
- }
- public AI.IFunctionSymbol/*!*/ FunctionSymbol {
- get {
- Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
- return AI.Bv.Concat;
- }
- }
- public IList/*<AI.IExpr!>*//*!*/ Arguments {
- get {
- Contract.Ensures(Contract.Result<IList>() != 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/*<AI.IExpr!>*/ args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<AI.IFunApp>() != 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<Absy>() != 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<AI.IFunctionSymbol>() != 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<AI.IFunctionSymbol>() != null);
- return arg.RealQuantifier.FunctionSymbol;
- }
- }
-
- private IList/*?*/ argCache = null;
- public IList/*<IExpr!>*//*!*/ Arguments {
-
- get {
- Contract.Ensures(Contract.Result<IList>() != null);
-
- if (argCache == null) {
- IList a = new ArrayList(1);
- a.Add(arg);
- argCache = ArrayList.ReadOnly(a);
- }
- return argCache;
- }
- }
-
- public AI.IFunApp CloneWithArguments(IList/*<IExpr!>*/ args) {
- //Contract.Requires(args != null);
- Contract.Ensures(Contract.Result<AI.IFunApp>() != 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<string>() != 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<AI.IVariable>() != null);
- return cce.NonNull(RealQuantifier.Dummies[dummyIndex]);
- }
- }
- public AI.AIType/*!*/ ParamType {
- get {
- Contract.Ensures(Contract.Result<AI.AIType>() != 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<AI.IExpr>() != 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<AI.IFunction>() != 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<string>() != null);
- return string.Format("\\{0} :: {1}", Param, Body);
- }
- }
-
- private AI.IExpr aiexprCache = null;
- public override AI.IExpr/*!*/ IExpr {
- get {
- Contract.Ensures(Contract.Result<AI.IExpr>() != 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<AI.IFunctionSymbol>() != 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<AI.IFunctionSymbol>() != 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<AI.IFunctionSymbol>() != null);
-
- return AI.Prop.Lambda;
- }
- }
-
public override Absy StdDispatch(StandardVisitor visitor) {
//Contract.Requires(visitor != null);
Contract.Ensures(Contract.Result<Absy>() != 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<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
- public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=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 @@ <Compile Include="Xml.cs" />
</ItemGroup>
<ItemGroup>
- <ProjectReference Include="..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
<Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
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<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
- public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=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<Absy>() != null);
return node.StdDispatch(this);
}
- public virtual AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<AIVariableExpr>() != null);
- return node;
- }
public virtual Cmd VisitAssertCmd(AssertCmd node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != 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 @@ <Compile Include="Houdini.cs" />
</ItemGroup>
<ItemGroup>
- <ProjectReference Include="..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
<Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
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 @@ <Compile Include="Z3.cs" />
</ItemGroup>
<ItemGroup>
- <ProjectReference Include="..\..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
<ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
<Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
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 @@ <Reference Include="System.XML" />
</ItemGroup>
<ItemGroup>
- <ProjectReference Include="..\..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
<ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
<Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
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<AIVariableExpr>() != null);
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
-
- ///////////////////////////////////////////////////////////////////////////////////
-
public override Expr VisitIdentifierExpr(IdentifierExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != 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 @@ <Compile Include="VCExprASTVisitors.cs" />
</ItemGroup>
<ItemGroup>
- <ProjectReference Include="..\AIFramework\AIFramework.csproj">
- <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
- <Name>AIFramework</Name>
- </ProjectReference>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
<Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
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 @@ -<?xml version="1.0" encoding="utf-8"?> -<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> - <PropertyGroup> - <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> - <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform> - <ProductVersion>9.0.21022</ProductVersion> - <SchemaVersion>2.0</SchemaVersion> - <ProjectGuid>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</ProjectGuid> - <OutputType>Library</OutputType> - <AppDesignerFolder>Properties</AppDesignerFolder> - <RootNamespace>VCGeneration</RootNamespace> - <AssemblyName>VCGeneration</AssemblyName> - <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> - <FileAlignment>512</FileAlignment> - <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> - <SignAssembly>true</SignAssembly> - <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile> - <FileUpgradeFlags> - </FileUpgradeFlags> - <OldToolsVersion>3.5</OldToolsVersion> - <UpgradeBackupLocation /> - <PublishUrl>publish\</PublishUrl> - <Install>true</Install> - <InstallFrom>Disk</InstallFrom> - <UpdateEnabled>false</UpdateEnabled> - <UpdateMode>Foreground</UpdateMode> - <UpdateInterval>7</UpdateInterval> - <UpdateIntervalUnits>Days</UpdateIntervalUnits> - <UpdatePeriodically>false</UpdatePeriodically> - <UpdateRequired>false</UpdateRequired> - <MapFileExtensions>true</MapFileExtensions> - <ApplicationRevision>0</ApplicationRevision> - <ApplicationVersion>1.0.0.%2a</ApplicationVersion> - <IsWebBootstrapper>false</IsWebBootstrapper> - <UseApplicationTrust>false</UseApplicationTrust> - <BootstrapperEnabled>true</BootstrapperEnabled> - <TargetFrameworkProfile>Client</TargetFrameworkProfile> - </PropertyGroup> - <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> - <DebugSymbols>true</DebugSymbols> - <DebugType>full</DebugType> - <Optimize>false</Optimize> - <OutputPath>bin\Debug\</OutputPath> - <DefineConstants>DEBUG;TRACE</DefineConstants> - <ErrorReport>prompt</ErrorReport> - <WarningLevel>4</WarningLevel> - <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking> - <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface> - <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure> - <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires> - <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis> - <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations> - <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations> - <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations> - <CodeContractsPointerObligations>False</CodeContractsPointerObligations> - <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis> - <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions> - <CodeContractsRunInBackground>True</CodeContractsRunInBackground> - <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies> - <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine> - <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs> - <CodeContractsCustomRewriterAssembly> - </CodeContractsCustomRewriterAssembly> - <CodeContractsCustomRewriterClass> - </CodeContractsCustomRewriterClass> - <CodeContractsLibPaths> - </CodeContractsLibPaths> - <CodeContractsExtraRewriteOptions> - </CodeContractsExtraRewriteOptions> - <CodeContractsExtraAnalysisOptions> - </CodeContractsExtraAnalysisOptions> - <CodeContractsBaseLineFile> - </CodeContractsBaseLineFile> - <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel> - <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly> - <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> - </PropertyGroup> - <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' "> - <DebugType>pdbonly</DebugType> - <Optimize>true</Optimize> - <OutputPath>bin\Release\</OutputPath> - <DefineConstants>TRACE</DefineConstants> - <ErrorReport>prompt</ErrorReport> - <WarningLevel>4</WarningLevel> - <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> - </PropertyGroup> - <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' "> - <DebugSymbols>true</DebugSymbols> - <OutputPath>bin\z3apidebug\</OutputPath> - <DefineConstants>DEBUG;TRACE</DefineConstants> - <DebugType>full</DebugType> - <PlatformTarget>AnyCPU</PlatformTarget> - <CodeAnalysisRuleAssemblies> - </CodeAnalysisRuleAssemblies> - <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> - <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> - <ErrorReport>prompt</ErrorReport> - <CodeAnalysisRuleSet>Migrated rules for VCGeneration.ruleset</CodeAnalysisRuleSet> - <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules> - </PropertyGroup> - <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'"> - <DebugSymbols>true</DebugSymbols> - <OutputPath>bin\Checked\</OutputPath> - <DefineConstants>DEBUG;TRACE</DefineConstants> - <DebugType>full</DebugType> - <PlatformTarget>AnyCPU</PlatformTarget> - <CodeAnalysisLogFile>bin\Debug\VCGeneration.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile> - <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> - <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> - <ErrorReport>prompt</ErrorReport> - <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> - <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> - <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> - <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking> - <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface> - <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure> - <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires> - <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers> - <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis> - <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations> - <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations> - <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations> - <CodeContractsEnumObligations>False</CodeContractsEnumObligations> - <CodeContractsPointerObligations>False</CodeContractsPointerObligations> - <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions> - <CodeContractsRunInBackground>True</CodeContractsRunInBackground> - <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies> - <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine> - <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs> - <CodeContractsCustomRewriterAssembly /> - <CodeContractsCustomRewriterClass /> - <CodeContractsLibPaths /> - <CodeContractsExtraRewriteOptions /> - <CodeContractsExtraAnalysisOptions /> - <CodeContractsBaseLineFile /> - <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults> - <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel> - <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly> - <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel> - </PropertyGroup> - <ItemGroup> - <Reference Include="System" /> - <Reference Include="System.Data" /> - <Reference Include="System.Xml" /> - </ItemGroup> - <ItemGroup> - <Compile Include="BlockPredicator.cs" /> - <Compile Include="Check.cs" /> - <Compile Include="ConditionGeneration.cs" /> - <Compile Include="Context.cs" /> - <Compile Include="DoomCheck.cs" /> - <Compile Include="DoomedLoopUnrolling.cs" /> - <Compile Include="DoomedStrategy.cs" /> - <Compile Include="DoomErrorHandler.cs" /> - <Compile Include="GraphAlgorithms.cs" /> - <Compile Include="HasseDiagram.cs" /> - <Compile Include="OrderingAxioms.cs" /> - <Compile Include="SmartBlockPredicator.cs" /> - <Compile Include="StratifiedVC.cs" /> - <Compile Include="UniformityAnalyser.cs" /> - <Compile Include="VC.cs" /> - <Compile Include="VCDoomed.cs" /> - <Compile Include="..\version.cs" /> - <Compile Include="Wlp.cs" /> - </ItemGroup> - <ItemGroup> - <ProjectReference Include="..\AIFramework\AIFramework.csproj"> - <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project> - <Name>AIFramework</Name> - </ProjectReference> - <ProjectReference Include="..\Basetypes\Basetypes.csproj"> - <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> - <Name>Basetypes</Name> - </ProjectReference> - <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj"> - <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project> - <Name>CodeContractsExtender</Name> - </ProjectReference> - <ProjectReference Include="..\Core\Core.csproj"> - <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project> - <Name>Core</Name> - </ProjectReference> - <ProjectReference Include="..\Graph\Graph.csproj"> - <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project> - <Name>Graph</Name> - </ProjectReference> - <ProjectReference Include="..\Model\Model.csproj"> - <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project> - <Name>Model</Name> - </ProjectReference> - <ProjectReference Include="..\ParserHelper\ParserHelper.csproj"> - <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project> - <Name>ParserHelper</Name> - </ProjectReference> - <ProjectReference Include="..\VCExpr\VCExpr.csproj"> - <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project> - <Name>VCExpr</Name> - </ProjectReference> - </ItemGroup> - <ItemGroup> - <Folder Include="Properties\" /> - </ItemGroup> - <ItemGroup> - <BootstrapperPackage Include="Microsoft.Net.Client.3.5"> - <Visible>False</Visible> - <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName> - <Install>false</Install> - </BootstrapperPackage> - <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1"> - <Visible>False</Visible> - <ProductName>.NET Framework 3.5 SP1</ProductName> - <Install>true</Install> - </BootstrapperPackage> - <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1"> - <Visible>False</Visible> - <ProductName>Windows Installer 3.1</ProductName> - <Install>true</Install> - </BootstrapperPackage> - </ItemGroup> - <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" /> +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>9.0.21022</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>VCGeneration</RootNamespace>
+ <AssemblyName>VCGeneration</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
+ <SignAssembly>true</SignAssembly>
+ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ <FileUpgradeFlags>
+ </FileUpgradeFlags>
+ <OldToolsVersion>3.5</OldToolsVersion>
+ <UpgradeBackupLocation />
+ <PublishUrl>publish\</PublishUrl>
+ <Install>true</Install>
+ <InstallFrom>Disk</InstallFrom>
+ <UpdateEnabled>false</UpdateEnabled>
+ <UpdateMode>Foreground</UpdateMode>
+ <UpdateInterval>7</UpdateInterval>
+ <UpdateIntervalUnits>Days</UpdateIntervalUnits>
+ <UpdatePeriodically>false</UpdatePeriodically>
+ <UpdateRequired>false</UpdateRequired>
+ <MapFileExtensions>true</MapFileExtensions>
+ <ApplicationRevision>0</ApplicationRevision>
+ <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
+ <IsWebBootstrapper>false</IsWebBootstrapper>
+ <UseApplicationTrust>false</UseApplicationTrust>
+ <BootstrapperEnabled>true</BootstrapperEnabled>
+ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly>
+ </CodeContractsCustomRewriterAssembly>
+ <CodeContractsCustomRewriterClass>
+ </CodeContractsCustomRewriterClass>
+ <CodeContractsLibPaths>
+ </CodeContractsLibPaths>
+ <CodeContractsExtraRewriteOptions>
+ </CodeContractsExtraRewriteOptions>
+ <CodeContractsExtraAnalysisOptions>
+ </CodeContractsExtraAnalysisOptions>
+ <CodeContractsBaseLineFile>
+ </CodeContractsBaseLineFile>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\z3apidebug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisRuleAssemblies>
+ </CodeAnalysisRuleAssemblies>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>Migrated rules for VCGeneration.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\Checked\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Debug\VCGeneration.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="BlockPredicator.cs" />
+ <Compile Include="Check.cs" />
+ <Compile Include="ConditionGeneration.cs" />
+ <Compile Include="Context.cs" />
+ <Compile Include="DoomCheck.cs" />
+ <Compile Include="DoomedLoopUnrolling.cs" />
+ <Compile Include="DoomedStrategy.cs" />
+ <Compile Include="DoomErrorHandler.cs" />
+ <Compile Include="GraphAlgorithms.cs" />
+ <Compile Include="HasseDiagram.cs" />
+ <Compile Include="OrderingAxioms.cs" />
+ <Compile Include="SmartBlockPredicator.cs" />
+ <Compile Include="StratifiedVC.cs" />
+ <Compile Include="UniformityAnalyser.cs" />
+ <Compile Include="VC.cs" />
+ <Compile Include="VCDoomed.cs" />
+ <Compile Include="..\version.cs" />
+ <Compile Include="Wlp.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
+ <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+ <Name>CodeContractsExtender</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Core\Core.csproj">
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Graph\Graph.csproj">
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
+ <Name>Graph</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Model\Model.csproj">
+ <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
+ <Name>Model</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+ <Name>ParserHelper</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\VCExpr\VCExpr.csproj">
+ <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
+ <Name>VCExpr</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <Folder Include="Properties\" />
+ </ItemGroup>
+ <ItemGroup>
+ <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
+ <Visible>False</Visible>
+ <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
+ <Install>false</Install>
+ </BootstrapperPackage>
+ <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
+ <Visible>False</Visible>
+ <ProductName>.NET Framework 3.5 SP1</ProductName>
+ <Install>true</Install>
+ </BootstrapperPackage>
+ <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
+ <Visible>False</Visible>
+ <ProductName>Windows Installer 3.1</ProductName>
+ <Install>true</Install>
+ </BootstrapperPackage>
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<!-- To modify your build process, add your task inside one of the targets below and uncomment it. Other similar extension points exist, see Microsoft.Common.targets. <Target Name="BeforeBuild"> </Target> <Target Name="AfterBuild"> </Target> - --> + -->
</Project>
\ 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
)
|