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 /Source/AbsInt | |
| 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.
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/AbsInt.csproj | 7 | ||||
| -rw-r--r-- | Source/AbsInt/AbstractInterpretation.cs | 916 | ||||
| -rw-r--r-- | Source/AbsInt/ExprFactories.cs | 275 | ||||
| -rw-r--r-- | Source/AbsInt/LoopInvariantsOnDemand.cs | 84 | ||||
| -rw-r--r-- | Source/AbsInt/NativeLattice.cs | 20 |
5 files changed, 17 insertions, 1285 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);
|