diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/AbsInt/AbsInt.csproj | 124 | ||||
| -rw-r--r-- | Source/AbsInt/AbstractInterpretation.cs | 1046 | ||||
| -rw-r--r-- | Source/AbsInt/AssemblyInfo.cs | 4 | ||||
| -rw-r--r-- | Source/AbsInt/ExprFactories.cs | 231 | ||||
| -rw-r--r-- | Source/AbsInt/LoopInvariantsOnDemand.cs | 78 | ||||
| -rw-r--r-- | Source/AbsInt/Traverse.cs | 182 |
6 files changed, 1665 insertions, 0 deletions
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj new file mode 100644 index 00000000..d0efb860 --- /dev/null +++ b/Source/AbsInt/AbsInt.csproj @@ -0,0 +1,124 @@ +<?xml version="1.0" encoding="utf-8"?>
+<VisualStudioProject>
+ <XEN ProjectType="Local"
+ SchemaVersion="1.0"
+ Name="AbsInt"
+ ProjectGuid="11d06232-2039-4bca-853b-c596e2a4edb0"
+ >
+ <Build>
+ <Settings ApplicationIcon=""
+ AssemblyName="AbsInt"
+ OutputType="Library"
+ RootNamespace="AbsInt"
+ StartupObject=""
+ TargetPlatform="v2"
+ TargetPlatformLocation=""
+ ShadowedAssembly=""
+ StandardLibraryLocation=""
+ >
+ <Config Name="Debug"
+ AllowUnsafeBlocks="False"
+ BaseAddress="285212672"
+ CheckForOverflowUnderflow="False"
+ ConfigurationOverrideFile=""
+ DefineConstants="DEBUG;TRACE"
+ DocumentationFile=""
+ DebugSymbols="True"
+ FileAlignment="4096"
+ IncrementalBuild="True"
+ Optimize="False"
+ OutputPath="bin\Debug"
+ RegisterForComInterop="False"
+ RemoveIntegerChecks="false"
+ TreatWarningsAsErrors="False"
+ WarningLevel="4"
+ RunProgramVerifier="False"
+ ProgramVerifierCommandLineOptions=""
+ ReferenceTypesAreNonNullByDefault="False"
+ RunProgramVerifierWhileEditing="False"
+ AllowPointersToManagedStructures="False"
+ CheckContractAdmissibility="True"
+ CheckPurity="False"
+ />
+ <Config Name="Release"
+ AllowUnsafeBlocks="false"
+ BaseAddress="285212672"
+ CheckForOverflowUnderflow="false"
+ ConfigurationOverrideFile=""
+ DefineConstants="TRACE"
+ DocumentationFile=""
+ DebugSymbols="false"
+ FileAlignment="4096"
+ IncrementalBuild="false"
+ Optimize="true"
+ OutputPath="bin\release"
+ RegisterForComInterop="false"
+ RemoveIntegerChecks="false"
+ TreatWarningsAsErrors="True"
+ WarningLevel="4"
+ />
+ </Settings>
+ <References>
+ <Reference Name="Mscorlib.Contracts"
+ AssemblyName="Mscorlib.Contracts"
+ Private="false"
+ HintPath="../../Binaries/Mscorlib.Contracts.dll"
+ />
+ <Reference Name="System"
+ AssemblyName="System"
+ Private="false"
+ />
+ <Reference Name="System.Compiler"
+ AssemblyName="System.Compiler"
+ Private="false"
+ HintPath="../../Binaries/System.Compiler.dll"
+ />
+ <Reference Name="System.Compiler.Framework"
+ AssemblyName="System.Compiler.Framework"
+ Private="false"
+ HintPath="../../Binaries/System.Compiler.Framework.dll"
+ />
+ <Reference Name="AIFramework"
+ Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
+ Private="true"
+ />
+ <Reference Name="Core"
+ Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
+ Private="true"
+ />
+ <Reference Name="Basetypes"
+ Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
+ Private="true"
+ />
+ </References>
+ </Build>
+ <Files>
+ <Include>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Traverse.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="AbstractInterpretation.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="ExprFactories.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="..\version.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="LoopInvariantsOnDemand.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="AssemblyInfo.ssc"
+ />
+ </Include>
+ </Files>
+ </XEN>
+</VisualStudioProject>
\ No newline at end of file diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs new file mode 100644 index 00000000..ee5a1f06 --- /dev/null +++ b/Source/AbsInt/AbstractInterpretation.cs @@ -0,0 +1,1046 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using Microsoft.Contracts;
+
+namespace Microsoft.Boogie.AbstractInterpretation
+{
+ using System;
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics;
+ using Microsoft.Boogie;
+ using Cci = System.Compiler;
+ using AI = Microsoft.AbstractInterpretationFramework;
+ using Microsoft.Contracts;
+
+ /// <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;
+ private Cci.IRelation/*<Procedure,Implementation>*/ procedureImplementations;
+
+ 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]
+
+ invariant 0 <= Index && Index < Proc.Summary.Count;
+
+ public ProcedureWorkItem ([Captured] Procedure! p, AI.Lattice.Element! v, AI.Lattice! lattice)
+ 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)
+ {
+ assume log.IsExposable; //PM: One would need static class invariants to prove this property
+ expose(log) {
+ log.Enabled = AI.Lattice.LogSwitch;
+ }
+ this.lattice = lattice;
+ this.procWorkItems = new Queue<ProcedureWorkItem!>();
+ this.callReturnWorkItems = new Queue();
+ }
+
+ private Cci.IGraphNavigator ComputeCallGraph (Program! program)
+ ensures this.procedureImplementations != 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.
+
+ Cci.IMutableRelation/*<Implementation,Procedure>*/ callsProcedure = new Cci.Relation();
+ Cci.IMutableRelation/*<Procedure,Implementation>*/ implementsProcedure = new Cci.Relation();
+ this.procedureImplementations = implementsProcedure;
+
+// ArrayList publics = new ArrayList();
+// publicImpls = publics;
+
+ foreach (Declaration member in program.TopLevelDeclarations)
+ {
+ Implementation impl = member as Implementation;
+ if (impl != null)
+ {
+ implementsProcedure.Add(impl.Proc, impl);
+ // if (impl.IsPublic) { publics.Add(impl); } // PR: what does "IsPublic" stand for?
+
+ foreach (Block block in impl.Blocks)
+ {
+ foreach (Cmd cmd in block.Cmds)
+ {
+ CallCmd call = cmd as CallCmd;
+ if (call != null)
+ {
+ callsProcedure.Add(impl, call.Proc);
+ }
+ }
+ }
+ }
+ }
+
+ // Now compute a graph from implementations to implementations.
+
+ Cci.GraphBuilder callGraph = new Cci.GraphBuilder();
+
+ IEnumerable callerImpls = callsProcedure.GetKeys();
+ assume callerImpls != null; // because of non-generic collection
+ foreach (Implementation caller in callerImpls)
+ {
+ IEnumerable callerProcs = callsProcedure.GetValues(caller);
+ assume callerProcs != null; // because of non-generic collection
+ foreach (Procedure callee in callerProcs)
+ {
+ IEnumerable calleeImpls = implementsProcedure.GetValues(callee);
+ assume calleeImpls != null; // because of non-generic collection
+ foreach (Implementation calleeImpl in calleeImpls)
+ {
+ callGraph.AddEdge(caller, calleeImpl);
+ }
+ }
+ }
+
+ return callGraph;
+ }
+
+#if OLDCODE
+ public void ComputeImplementationInvariants (Implementation impl)
+ {
+ // process each procedure implementation by recursively processing the first (entry) block...
+ ComputeBlockInvariants(impl.Blocks[0], lattice.Top);
+
+ // 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)
+ {
+ AI.Lattice.Element postValue = block.PostInvariantBuckets[invariantIndex];
+ Debug.Assert(postValue != null);
+ post = post.Join(postValue);
+ }
+ }
+ impl.PostInvariant = post;
+
+ // Now update the procedure to reflect the new properties
+ // of this implementation.
+
+ if (impl.Proc.PreInvariant <= impl.PreInvariant)
+ {
+ // Strengthen the precondition
+ impl.Proc.PreInvariant = impl.PreInvariant;
+ foreach (Implementation otherImpl in this.procedureImplementations.GetValues(impl.Proc))
+ {
+ if (otherImpl == impl) { continue; }
+ if (otherImpl.PreInvariant <= impl.Proc.PreInvariant)
+ {
+ // If another implementation of the same procedure has
+ // a weaker precondition, re-do it with the stronger
+ // precondition.
+ otherImpl.PreInvariant = impl.Proc.PreInvariant;
+ this.implWorkItems.Enqueue(otherImpl);
+ }
+ }
+ }
+ }
+#endif
+
+
+#if NOTYET
+ public void ComputeSccInvariants (IEnumerable/*<Implementation>*/ implementations)
+ {
+ Debug.Assert(this.implWorkItems.Count == 0); // no work left over from last SCC
+
+ foreach (Implementation impl in implementations)
+ {
+ impl.AbstractFunction = AbstractFunction.Empty.WithPair(this.lattice.Bottom, this.lattice.Bottom);
+ this.implWorkItems.Enqueue(impl);
+ }
+
+ while (this.implWorkItems.Count > 0) // until fixed point reached
+ {
+ Implementation impl = (Implementation)this.implWorkItems.Dequeue();
+ }
+ }
+#endif
+
+ public AI.Lattice.Element! ApplyProcedureSummary (CallCmd! call, Implementation! caller, AI.Lattice.Element! knownAtCallSite, CallSite! callSite)
+ requires call.Proc != null;
+ {
+ Procedure! proc = call.Proc;
+
+ // 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;
+ for (int i=0; i<proc.InParams.Length; i++)
+ {
+ // "Assign" the actual expressions to the corresponding formal variables.
+ assume proc.InParams[i] != null; //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;
+ assume call.Ins[i] != null; //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;
+ Expr equality = Expr.Eq(Expr.Ident( (!) proc.InParams[i]), (!) call.Ins[i]);
+ relevantToCall = lattice.Constrain(relevantToCall, equality.IExpr);
+ }
+ foreach (Variable! var in caller.LocVars) {
+ relevantToCall = this.lattice.Eliminate(relevantToCall, var);
+ }
+
+ ProcedureSummary! summary = proc.Summary;
+ ProcedureSummaryEntry applicableEntry = null;
+
+ for (int i=0; i<summary.Count; i++)
+ {
+ ProcedureSummaryEntry! current = (!) 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);
+ this.procWorkItems.Enqueue(newWorkItem);
+ applicableEntry = (!) 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, (!) call.Proc.OutParams[i], (!)((!) call.Outs[i]).Decl);
+ knownAtCallSite = this.lattice.Eliminate(knownAtCallSite, (!)((!) call.Outs[i]).Decl);
+ }
+
+ return this.lattice.Meet(atReturn, knownAtCallSite);
+ }
+
+ private Cci.IGraphNavigator callGraph;
+ public Cci.IGraphNavigator CallGraph {
+ get { return this.callGraph; }
+ }
+
+ /// <summary>
+ /// Compute the invariants for the program using the underlying abstract domain
+ /// </summary>
+ public void ComputeProgramInvariants (Program! program)
+ {
+
+#if NOT_YET
+ Cci.IGraphNavigator callGraph =
+#endif
+
+ callGraph = this.ComputeCallGraph(program);
+ assert this.procedureImplementations != null;
+ Cci.IRelation! procedureImplementations = this.procedureImplementations;
+
+#if NOT_YET
+ IEnumerable/*<IStronglyConnectedComponent>*/ sccs =
+ StronglyConnectedComponent.ConstructSCCs(publicImpls, callGraph);
+
+ IList/*<IStronglyConnectedComponent>*/ sortedSccs =
+ GraphUtil.TopologicallySortComponentGraph(sccs);
+
+ // Go bottom-up through the SCCs of the call graph
+ foreach (IStronglyConnectedComponent scc in sortedSccs)
+ {
+ this.ComputeSccInvariants(scc.Nodes);
+ }
+#endif
+ AI.Lattice.Element! initialElement = this.lattice.Top;
+ // 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 = (!) workItem.Proc.Summary[workItem.Index];
+
+ if (((!) procedureImplementations.GetValues(workItem.Proc)).Count == 0)
+ {
+ // 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 (!) procedureImplementations.GetValues(workItem.Proc))
+ {
+ // process each procedure implementation by recursively processing the first (entry) block...
+ ((!)impl.Blocks[0]).Lattice = lattice;
+ ComputeBlockInvariants(impl, (!) impl.Blocks[0], summaryEntry.OnEntry, summaryEntry);
+ AdjustProcedureSummary(impl, summaryEntry);
+ }
+ }
+ }
+
+
+ while (this.callReturnWorkItems.Count > 0)
+ {
+ CallSite callSite = (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)
+ {
+ 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)
+ {
+ atReturn = this.lattice.Eliminate(atReturn, var);
+ }
+ foreach (Variable! var in impl.InParams)
+ {
+ 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)
+ {
+ this.callReturnWorkItems.Enqueue(callSite);
+ }
+ }
+ }
+
+ private static int freshVarId = 0;
+ private static Variable! FreshVar(Boogie.Type! ty)
+ {
+ 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)
+ {
+ assume log.IsPeerConsistent;
+ 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 = (!) block.Cmds[cmdIndex]; // Fetch the command
+ currentValue = Step(cmd, currentValue, impl, // Apply the transition function
+ delegate (AI.Lattice.Element! currentValue)
+ {
+ return new CallSite(impl, block, cmdIndex, currentValue, 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}", ((!)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.
+ assume @goto.labelTargets != null;
+
+ // For all the successors of this block, propagate the abstract state
+ foreach (Block! succ in @goto.labelTargets)
+ {
+ 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)
+ {
+ assume log.IsPeerConsistent;
+ log.DbgMsg(string.Format("{0}", cmd)); log.DbgMsgIndent();
+
+ AI.Lattice.Element! currentValue = pre;
+
+ // Case split...
+ #region AssignCmd
+ if (cmd is AssignCmd) { // parallel assignment
+ // we first eliminate map assignments
+ AssignCmd! assmt = ((AssignCmd)cmd).AsSimpleAssignCmd;
+ //PM: Assume variables have been resolved
+ assume forall {AssignLhs! lhs in assmt.Lhss;
+ lhs.DeepAssignedVariable != null};
+
+ List<IdentifierExpr!>! freshLhs = new List<IdentifierExpr!> ();
+ foreach (AssignLhs! lhs in assmt.Lhss)
+ freshLhs.Add(Expr.Ident(FreshVar(((!)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)
+ currentValue =
+ this.lattice.Eliminate(currentValue, (!)lhs.DeepAssignedVariable);
+ for (int i = 0; i < freshLhs.Count; ++i)
+ currentValue =
+ this.lattice.Rename(currentValue, (!)freshLhs[i].Decl,
+ (!)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)
+ {
+ currentValue = this.lattice.Eliminate(currentValue, (!)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 = (!)((PredicateCmd)cmd).Expr;
+ List<Expr!>! conjuncts = flatConjunction(embeddedExpr); // Handle "assume P && Q" as if it was "assume P; assume Q"
+ foreach(Expr! c in conjuncts) {
+ 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) { currentValue = Step(callDesug, currentValue, impl, null); }
+
+ // Now, project out the local variables
+ foreach (Variable! local in statecmd.Locals) { 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) { currentValue = Step(callDesug, currentValue, impl, null); }
+ // Now, project out the local variables
+ foreach (Variable! local in statecmd.Locals) { currentValue = this.lattice.Eliminate(currentValue, local); }
+ } else {
+ currentValue = Step(desugaring, currentValue, impl, null);
+ }
+ }
+ else
+ {
+ assert false; // unknown command
+ }
+
+ log.DbgMsgUnindent();
+
+ return currentValue;
+ }
+
+ /// <summary>
+ /// Flat an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R]
+ /// </summary>
+ private List<Expr!>! flatConjunction(Expr! embeddedExpr)
+ {
+ List<Expr!>! 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)
+ {
+ List<Expr!>! 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)
+ {
+ if (block.PreInvariant == null) // block has not yet been processed
+ {
+ assert block.PostInvariant == null;
+
+ // To a first approximation the block is unreachable
+ block.PreInvariant = this.lattice.Bottom;
+ block.PostInvariant = this.lattice.Bottom;
+ }
+
+ assert block.PreInvariant != null;
+ 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, (!) 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()
+ {
+ AI.IQuantPropExprFactory 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);
+
+ 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()
+ {
+ AbstractAlgebra! retAlgebra;
+
+ AI.Lattice! returnLattice;
+
+ AI.IQuantPropExprFactory 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.IQuantPropExprFactory 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;
+
+ public AI.Lattice! Lattice
+ {
+ get
+ {
+ return lattice;
+ }
+ }
+
+ public AI.IQuantPropExprFactory 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.IQuantPropExprFactory propFactory,
+ AI.ILinearExprFactory linearFactory,
+ AI.IIntExprFactory intFactory,
+ AI.IValueExprFactory valueFactory,
+ AI.INullnessFactory nullFactory,
+ IComparer variableComparer)
+ requires propFactory != null ==> Owner.Same(lattice, propFactory);
+ requires linearFactory != null ==> Owner.Same(lattice, linearFactory);
+ requires intFactory != null ==> Owner.Same(lattice, intFactory);
+ requires valueFactory != null ==> Owner.Same(lattice, valueFactory);
+ requires nullFactory != null ==> Owner.Same(lattice, nullFactory);
+ requires variableComparer != null ==> Owner.Same(lattice, variableComparer);
+ // ensures Owner.Same(this, lattice); // KRML:
+ {
+ 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)
+ {
+ 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.Now;
+ }
+
+ 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;
+ ApplyAbstractInterpretation(program, lattice);
+ }
+
+ program.InstrumentWithInvariants();
+
+ if (CommandLineOptions.Clo.Trace) {
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ Console.WriteLine(" [{0} s]", elapsed.TotalSeconds);
+ Console.Out.Flush();
+ }
+ }
+ }
+
+ static void ApplyAbstractInterpretation (Program! program, AI.Lattice! lattice)
+ {
+ AbstractionEngine engine = new AbstractionEngine(lattice);
+ engine.ComputeProgramInvariants(program);
+ callGraph = engine.CallGraph;
+ }
+ private static Cci.IGraphNavigator callGraph;
+ public static Cci.IGraphNavigator CallGraph {
+ get { return callGraph; }
+ }
+
+
+}
+
+} // namespace
diff --git a/Source/AbsInt/AssemblyInfo.cs b/Source/AbsInt/AssemblyInfo.cs new file mode 100644 index 00000000..6ed99a25 --- /dev/null +++ b/Source/AbsInt/AssemblyInfo.cs @@ -0,0 +1,4 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+
+[assembly: AssemblyKeyFile("..\\InterimKey.snk")]
diff --git a/Source/AbsInt/ExprFactories.cs b/Source/AbsInt/ExprFactories.cs new file mode 100644 index 00000000..ad090f2b --- /dev/null +++ b/Source/AbsInt/ExprFactories.cs @@ -0,0 +1,231 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using Microsoft.Boogie;
+using AI = Microsoft.AbstractInterpretationFramework;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+
+namespace Microsoft.Boogie.AbstractInterpretation {
+
+ public class BoogiePropFactory : BoogieFactory, AI.IQuantPropExprFactory
+ {
+ public AI.IFunApp! False {
+ get {
+
+ return Expr.False;
+ }
+ }
+ public AI.IFunApp! True {
+ get {
+ return Expr.True;
+ }
+ }
+
+ public AI.IFunApp! Not(AI.IExpr! p) {
+ return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, IExpr2Expr(p));
+ }
+
+ public AI.IFunApp! And(AI.IExpr! p, AI.IExpr! q) {
+ return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));
+ }
+
+ public AI.IFunApp! Or(AI.IExpr! p, AI.IExpr! q) {
+ return Expr.Binary(BinaryOperator.Opcode.Or, IExpr2Expr(p), IExpr2Expr(q));
+ }
+
+ public AI.IFunApp! Implies(AI.IExpr! p, AI.IExpr! q) {
+ return Expr.Binary(BinaryOperator.Opcode.Imp, IExpr2Expr(p), IExpr2Expr(q));
+ }
+
+ public AI.IFunApp! Exists(AI.IFunction! p) {
+ return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;
+ }
+ public AI.IFunApp! Exists(AI.AIType paramType, AI.FunctionBody! bodygen) {
+ // generate a fresh new variable
+ Variable! var = FreshBoundVariable(paramType);
+ Expr! expr = IExpr2Expr(bodygen(var));
+ return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;
+ }
+
+ public AI.IFunApp! Forall(AI.IFunction! p) {
+ return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;
+ }
+ public AI.IFunApp! Forall(AI.AIType paramType, AI.FunctionBody! bodygen) {
+ // generate a fresh new variable
+ Variable! var = FreshBoundVariable(paramType);
+ Expr! expr = IExpr2Expr(bodygen(var));
+ return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;
+ }
+
+ private static int freshVarNum = 0;
+ private static Variable! FreshBoundVariable(AI.AIType paramType)
+ {
+ // TODO: Should use the AI.AIType given in Exists and Forall to determine what Boogie type
+ // to make this new variable? For now, we use Type.Any.
+ Type! t = Type.Int;
+ /*
+ if (paramType is AI.Ref)
+ t = Type.Ref;
+ else if (paramType is AI.FieldName)
+ t = Type.Name;
+ else
+ System.Console.WriteLine("*** unsupported type in AI {0}", paramType); */
+ assert false;
+ TypedIdent id = new TypedIdent(Token.NoToken, "propfactory_freshvar" + freshVarNum, t);
+ freshVarNum++;
+ return new BoundVariable(Token.NoToken, id);
+ }
+ }
+
+ public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory
+ {
+ public AI.IFunApp! Eq(AI.IExpr! e0, AI.IExpr! e1) {
+ return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));
+ }
+ public AI.IFunApp! Neq(AI.IExpr! e0, AI.IExpr! e1) {
+ return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));
+ }
+ }
+
+ public class BoogieNullnessFactory : BoogieFactory, AI.INullnessFactory
+ {
+ public AI.IFunApp! Eq(AI.IExpr! e0, AI.IExpr! e1) {
+ return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));
+ }
+
+ public AI.IFunApp! Neq(AI.IExpr! e0, AI.IExpr! e1) {
+ return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));
+ }
+
+ public AI.IFunApp! Null {
+ get {
+ assert false; // don't know where to get null from
+ }
+ }
+ }
+
+ public class BoogieIntFactory : BoogieValueFactory, AI.IIntExprFactory {
+ public AI.IFunApp! Const(BigNum i) {
+ return new LiteralExpr(Token.NoToken, i);
+ }
+ }
+
+ public class BoogieLinearFactory : BoogieIntFactory, AI.ILinearExprFactory {
+ public AI.IFunApp! AtMost(AI.IExpr! e0, AI.IExpr! e1) {
+ return Expr.Le(IExpr2Expr(e0), IExpr2Expr(e1));
+ }
+ public AI.IFunApp! Add(AI.IExpr! e0, AI.IExpr! e1) {
+ return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1));
+ }
+ public AI.IExpr! Term(Rational r, AI.IVariable var) {
+ 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 {
+ return Expr.False;
+ }
+ }
+ public AI.IFunApp! True {
+ get {
+ return Expr.True;
+ }
+ }
+ public AI.IFunApp! And(AI.IExpr! p, AI.IExpr! q) {
+ 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 {
+ 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)
+ ensures result == (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) {
+ 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) {
+ assert false; // BUGBUG: TODO
+ }
+
+ /// <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) {
+ assert false; // BUGBUG: TODO
+ }
+
+ 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.
+ assume type is Constant;
+ Constant theType = (Constant)type;
+ assert false;
+ 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) {
+ //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.
+ assume type is Constant;
+ assert false;
+ 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 new file mode 100644 index 00000000..1ebd11b2 --- /dev/null +++ b/Source/AbsInt/LoopInvariantsOnDemand.cs @@ -0,0 +1,78 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie.AbstractInterpretation
+{
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.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;
+ public List<AI.IVariable!>! FreeVariables
+ {
+ get
+ {
+ 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);
+
+ 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
+ {
+ assert false;
+ }
+ }
+
+ public override object VisitFunApp(AI.IFunApp! funapp)
+ {
+ foreach (AI.IExpr! arg in funapp.Arguments)
+ {
+ arg.DoVisit(this);
+ }
+ return true;
+ }
+
+ public override object VisitFunction(AI.IFunction! fun)
+ {
+ fun.Body.DoVisit(this);
+ this.variables.Remove(fun.Param);
+ return true;
+ }
+
+ }
+
+}
\ No newline at end of file diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs new file mode 100644 index 00000000..694811da --- /dev/null +++ b/Source/AbsInt/Traverse.cs @@ -0,0 +1,182 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie
+{
+ using System;
+ using System.Collections.Generic;
+ using Microsoft.Contracts;
+
+ /// <summary>
+ /// This class provides the functionality of traversing a program to determine which
+ /// blocks are blocks where the widening operator may need to be applied. Assumes
+ /// all 'currentlyTraversed' bits to be initially false, and leaves them that way in
+ /// the end. Assumes the 'widenBlock' bits are initially false, and sets them
+ /// appropriately.
+ /// </summary>
+ public class WidenPoints
+ {
+ /// <summary>
+ /// Compute the widen points of a program
+ /// </summary>
+ public static void Compute(Program! program)
+ {
+ expose (program)
+ {
+ foreach (Declaration m in program.TopLevelDeclarations)
+ {
+ Implementation impl = m as Implementation;
+ if (impl != null)
+ {
+ if (impl.Blocks != null && impl.Blocks.Count > 0)
+ {
+ assume impl.IsConsistent;
+ expose (impl) {
+ Block start = impl.Blocks[0];
+ assume start != null;
+ assume start.IsConsistent;
+ Visit(start);
+
+ // We reset the state...
+ foreach(Block b in impl.Blocks) {
+ expose (b) {
+ b.TraversingStatus = Block.VisitState.ToVisit;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ static void Visit(Block! b)
+ {
+ assume b.IsExposable;
+ if (b.TraversingStatus == Block.VisitState.BeingVisited)
+ {
+ expose (b)
+ {
+ // we got here through a back-edge
+ b.widenBlock = true;
+ }
+ }
+ else if(b.TraversingStatus == Block.VisitState.AlreadyVisited)
+ {
+ // do nothing... we already saw this node
+ }
+ else if (b.TransferCmd is GotoCmd)
+ {
+ assert b.TraversingStatus == Block.VisitState.ToVisit;
+
+ GotoCmd g = (GotoCmd)b.TransferCmd;
+ expose (b)
+ {
+ expose (g) { //PM: required for the subsequent expose (g.labelTargets)
+ b.TraversingStatus = Block.VisitState.BeingVisited;
+
+ // labelTargets is made non-null by Resolve, which we assume
+ // has already called in a prior pass.
+ assume g.labelTargets != null;
+ expose (g.labelTargets) {
+ foreach (Block succ in g.labelTargets)
+// invariant b.currentlyTraversed;
+ //PM: The following loop invariant will work once properties are axiomatized
+ //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);
+ {
+ assert succ != null;
+ Visit(succ);
+ }
+ }
+
+ assert b.TraversingStatus == Block.VisitState.BeingVisited;
+// System.Diagnostics.Debug.Assert(b.currentlyTraversed);
+
+ b.TraversingStatus = Block.VisitState.AlreadyVisited;
+
+ //PM: The folowing assumption is needed because we cannot prove that a simple field update
+ //PM: leaves the value of a property unchanged.
+ assume (g.labelNames != null ==> g.labelNames.Length == g.labelTargets.Length);
+ }
+ }
+ }
+ else
+ {
+ assert b.TransferCmd == null || b.TransferCmd is ReturnCmd; // It must be a returnCmd;
+ }
+ }
+
+ static private Block rootBlock = null; // The root point we have to consider
+
+ /// <summary>
+ /// Compute the blocks in the body loop.
+ /// <param name ="block"> Tt is the head of the loop. It must be a widen block </param>
+ /// <return> The blocks that are in the loop from block </return>
+ /// </summary>
+ public static List<Block!> ComputeLoopBodyFrom(Block! block)
+ requires block.widenBlock;
+ {
+ assert rootBlock == null;
+ rootBlock = block;
+
+ List<Block!> blocksInLoop = new List<Block!>(); // We use a list just because .net does not define a set
+ List<Block!> visitingPath = new List<Block!>(); // The order is important, as we want paths
+
+ blocksInLoop.Add(block);
+
+ DoDFSVisit(block, visitingPath, blocksInLoop);
+
+ visitingPath.Add(block);
+
+
+ rootBlock = null; // We reset the invariant
+
+ return blocksInLoop;
+ }
+
+ /// <summary>
+ /// Perform the Depth-first search of the so to find the loop
+ /// <param name = "block"> The block to visit </param>
+ /// <param name = "path"> The path we are visiting so far </param>
+ /// </summary>
+ private static void DoDFSVisit(Block! block, List<Block!>! path, List<Block!>! blocksInPath)
+ {
+ #region case 1. We visit the root => We are done, "path" is a path inside the loop
+ if(block == rootBlock && path.Count > 1)
+ {
+ blocksInPath.AddRange(path); // Add all the blocks in this path
+ }
+
+ #endregion
+ #region case 2. We visit a node that ends with a return => "path" is not inside the loop
+ if(block.TransferCmd is ReturnCmd)
+ {
+ return;
+ }
+ #endregion
+ #region case 3. We visit a node with successors => continue the exploration of its successors
+ {
+ assert block.TransferCmd is GotoCmd;
+ GotoCmd! successors = (GotoCmd) block.TransferCmd;
+
+ if (successors.labelTargets != null)
+ foreach (Block! nextBlock in successors.labelTargets)
+ {
+ if(path.Contains(nextBlock)) // If the current path has already seen the block, just skip it
+ continue;
+ // Otherwise we perform the DFS visit
+ path.Add(nextBlock);
+ DoDFSVisit(nextBlock, path, blocksInPath);
+
+ assert nextBlock == path[path.Count-1];
+ path.RemoveAt(path.Count-1);
+ }
+
+ }
+
+ #endregion
+ }
+ }
+}
|