diff options
Diffstat (limited to 'Source')
27 files changed, 1383 insertions, 413 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 0d2676f2..2fd37463 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -698,9 +698,13 @@ namespace Microsoft.Boogie.AbstractInterpretation lo = Lo; hi = Hi; if (hi != null) { Lo = node.Type.IsReal ? -hi : 1 - hi; + } else { + Lo = null; } if (lo != null) { Hi = node.Type.IsReal ? -lo : 1 - lo; + } else { + Hi = null; } } else if (op.Op == UnaryOperator.Opcode.Not) { @@ -880,6 +884,10 @@ namespace Microsoft.Boogie.AbstractInterpretation if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { Lo = BigInteger.Zero; Hi = hi1; + if (lo0 < lo1 && hi0 != null && hi0 < lo1) { + Lo = lo0; + Hi = hi0; + } } break; case BinaryOperator.Opcode.RealDiv: diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/CivlRefinement.cs index 2ad08024..75ff2358 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/CivlRefinement.cs @@ -13,7 +13,7 @@ namespace Microsoft.Boogie { public class MyDuplicator : Duplicator { - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; public int layerNum; Procedure enclosingProc; Implementation enclosingImpl; @@ -23,9 +23,9 @@ namespace Microsoft.Boogie public HashSet<Procedure> yieldingProcs; public List<Implementation> impls; - public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum) + public MyDuplicator(CivlTypeChecker civlTypeChecker, int layerNum) { - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.layerNum = layerNum; this.enclosingProc = null; this.enclosingImpl = null; @@ -38,11 +38,19 @@ namespace Microsoft.Boogie private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds) { - int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; + int enclosingProcLayerNum = civlTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; Procedure originalProc = originalCallCmd.Proc; - if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) + + if (civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc)) + { + if (civlTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum)) + { + newCmds.Add(callCmd); + } + } + else if (civlTypeChecker.procToActionInfo.ContainsKey(originalProc)) { - AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; + AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum) { newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); @@ -57,8 +65,12 @@ namespace Microsoft.Boogie newCmds.Add(Substituter.Apply(subst, assertCmd)); } } + newCmds.Add(callCmd); + } + else + { + Debug.Assert(false); } - newCmds.Add(callCmd); } private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds) @@ -66,7 +78,7 @@ namespace Microsoft.Boogie int maxCalleeLayerNum = 0; foreach (CallCmd iter in originalParCallCmd.CallCmds) { - int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; + int calleeLayerNum = civlTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; if (calleeLayerNum > maxCalleeLayerNum) maxCalleeLayerNum = calleeLayerNum; } @@ -144,7 +156,7 @@ namespace Microsoft.Boogie public override Procedure VisitProcedure(Procedure node) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(node)) + if (!civlTypeChecker.procToActionInfo.ContainsKey(node)) return node; if (!procMap.ContainsKey(node)) { @@ -155,7 +167,7 @@ namespace Microsoft.Boogie proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies); proc.OutParams = this.VisitVariableSeq(node.OutParams); - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node]; if (actionInfo.createdAtLayerNum < layerNum) { proc.Requires = new List<Requires>(); @@ -198,7 +210,7 @@ namespace Microsoft.Boogie } procMap[node] = proc; proc.Modifies = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); } return procMap[node]; } @@ -220,7 +232,7 @@ namespace Microsoft.Boogie Requires requires = base.VisitRequires(node); if (node.Free) return requires; - if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) requires.Condition = Expr.True; return requires; } @@ -230,12 +242,12 @@ namespace Microsoft.Boogie Ensures ensures = base.VisitEnsures(node); if (node.Free) return ensures; - AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; + AtomicActionInfo atomicActionInfo = civlTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node; - if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) { ensures.Condition = Expr.True; - ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes); + ensures.Attributes = CivlRefinement.RemoveMoverAttribute(ensures.Attributes); } return ensures; } @@ -243,16 +255,16 @@ namespace Microsoft.Boogie public override Cmd VisitAssertCmd(AssertCmd node) { AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); - if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum)) assertCmd.Expr = Expr.True; return assertCmd; } } - public class OwickiGries + public class CivlRefinement { LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; Dictionary<Absy, Absy> absyMap; Dictionary<Implementation, Implementation> implMap; HashSet<Procedure> yieldingProcs; @@ -269,17 +281,17 @@ namespace Microsoft.Boogie Expr beta; HashSet<Variable> frame; - public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator) + public CivlRefinement(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, MyDuplicator duplicator) { this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.absyMap = duplicator.absyMap; this.layerNum = duplicator.layerNum; this.implMap = duplicator.implMap; this.yieldingProcs = duplicator.yieldingProcs; Program program = linearTypeChecker.program; globalMods = new List<IdentifierExpr>(); - foreach (Variable g in moverTypeChecker.SharedVariables) + foreach (Variable g in civlTypeChecker.SharedVariables) { globalMods.Add(Expr.Ident(g)); } @@ -291,7 +303,24 @@ namespace Microsoft.Boogie private IEnumerable<Variable> AvailableLinearVars(Absy absy) { - return linearTypeChecker.AvailableLinearVars(absyMap[absy]); + HashSet<Variable> availableVars = new HashSet<Variable>(linearTypeChecker.AvailableLinearVars(absyMap[absy])); + foreach (var g in civlTypeChecker.globalVarToSharedVarInfo.Keys) + { + SharedVariableInfo info = civlTypeChecker.globalVarToSharedVarInfo[g]; + if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum)) + { + availableVars.Remove(g); + } + } + foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys) + { + LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v]; + if (layerNum < info.layer) + { + availableVars.Remove(v); + } + } + return availableVars; } private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar) @@ -715,7 +744,7 @@ namespace Microsoft.Boogie } Procedure originalProc = implMap[impl].Proc; - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc]; if (actionInfo.createdAtLayerNum == this.layerNum) { pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); @@ -738,19 +767,14 @@ namespace Microsoft.Boogie foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); } Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); - frame = new HashSet<Variable>(moverTypeChecker.SharedVariables); - HashSet<Variable> introducedVars = new HashSet<Variable>(); - foreach (Variable v in moverTypeChecker.SharedVariables) + frame = new HashSet<Variable>(civlTypeChecker.SharedVariables); + foreach (Variable v in civlTypeChecker.SharedVariables) { - if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || - moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) + if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || + civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) { frame.Remove(v); } - if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum) - { - introducedVars.Add(v); - } } AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; if (atomicActionInfo == null) @@ -764,7 +788,7 @@ namespace Microsoft.Boogie } else { - Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute(true); + Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true); beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); Expr alphaExpr = Expr.True; foreach (AssertCmd assertCmd in atomicActionInfo.gate) @@ -1175,31 +1199,31 @@ namespace Microsoft.Boogie return decls; } - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) + foreach (int layerNum in civlTypeChecker.AllLayerNums) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; - MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum); + MyDuplicator duplicator = new MyDuplicator(civlTypeChecker, layerNum); foreach (var proc in program.Procedures) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue; + if (!civlTypeChecker.procToActionInfo.ContainsKey(proc)) continue; Procedure duplicateProc = duplicator.VisitProcedure(proc); decls.Add(duplicateProc); } decls.AddRange(duplicator.impls); - OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator); + CivlRefinement civlTransform = new CivlRefinement(linearTypeChecker, civlTypeChecker, duplicator); foreach (var impl in program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) + if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) continue; Implementation duplicateImpl = duplicator.VisitImplementation(impl); - ogTransform.TransformImpl(duplicateImpl); + civlTransform.TransformImpl(duplicateImpl); decls.Add(duplicateImpl); } - decls.AddRange(ogTransform.Collect()); + decls.AddRange(civlTransform.Collect()); } } } diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/CivlTypeChecker.cs index c821117a..b426d9ed 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -280,22 +280,111 @@ namespace Microsoft.Boogie } } - public class MoverTypeChecker : ReadOnlyVisitor + public class LayerRange + { + public int lowerLayerNum; + public int upperLayerNum; + public LayerRange(int layer) + { + this.lowerLayerNum = layer; + this.upperLayerNum = layer; + } + public LayerRange(int lower, int upper) + { + this.lowerLayerNum = lower; + this.upperLayerNum = upper; + } + public LayerRange(IEnumerable<int> layerNums) + { + int min = int.MaxValue; + int max = int.MinValue; + foreach (var layerNum in layerNums) + { + if (layerNum < min) + { + min = layerNum; + } + if (max < layerNum) + { + max = layerNum; + } + } + this.lowerLayerNum = min; + this.upperLayerNum = max; + } + public bool Contains(int layerNum) + { + return lowerLayerNum <= layerNum && layerNum <= upperLayerNum; + } + public bool Subset(int lower, int upper) + { + return lower <= lowerLayerNum && upperLayerNum <= upper; + } + public bool Equal(int lower, int upper) + { + return lower == lowerLayerNum && upperLayerNum == upper; + } + public bool Subset(LayerRange info) + { + return info.lowerLayerNum <= lowerLayerNum && upperLayerNum <= info.upperLayerNum; + } + } + + public class AtomicProcedureInfo + { + public bool isPure; + public LayerRange layerRange; + public AtomicProcedureInfo() + { + this.isPure = true; + this.layerRange = null; + } + public AtomicProcedureInfo(LayerRange layerRange) + { + this.isPure = false; + this.layerRange = layerRange; + } + } + + public class LocalVariableInfo + { + public int layer; + public LocalVariableInfo(int layer) + { + this.layer = layer; + } + } + + public class CivlTypeChecker : ReadOnlyVisitor { CheckingContext checkingContext; - public int errorCount; - public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo; Procedure enclosingProc; Implementation enclosingImpl; - public Dictionary<Procedure, ActionInfo> procToActionInfo; + HashSet<Variable> sharedVarsAccessed; + int introducedLocalVarsUpperBound; + public Program program; - bool canAccessSharedVars; - bool canAccessGhostVars; - int minLayerNum; - int maxLayerNum; + public int errorCount; + public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo; + public Dictionary<Procedure, ActionInfo> procToActionInfo; + public Dictionary<Procedure, AtomicProcedureInfo> procToAtomicProcedureInfo; public Dictionary<Absy, HashSet<int>> absyToLayerNums; - HashSet<Variable> ghostVars; - public int leastUnimplementedLayerNum; + public Dictionary<Variable, LocalVariableInfo> localVarToLocalVariableInfo; + Dictionary<CallCmd, int> pureCallLayer; + + public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum) + { + Debug.Assert(procToAtomicProcedureInfo.ContainsKey(callCmd.Proc)); + var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc]; + if (atomicProcedureInfo.isPure) + { + return pureCallLayer[callCmd] <= layerNum; + } + else + { + return enclosingProcLayerNum == layerNum; + } + } private static List<int> FindLayers(QKeyValue kv) { @@ -316,6 +405,19 @@ namespace Microsoft.Boogie return layers; } + private static int Least(IEnumerable<int> layerNums) + { + int least = int.MaxValue; + foreach (var layer in layerNums) + { + if (layer < least) + { + least = layer; + } + } + return least; + } + private static MoverType GetMoverType(Ensures e) { if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic")) @@ -329,28 +431,29 @@ namespace Microsoft.Boogie return MoverType.Top; } - public MoverTypeChecker(Program program) + public CivlTypeChecker(Program program) { - this.ghostVars = new HashSet<Variable>(); - this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>(); - this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>(); - this.procToActionInfo = new Dictionary<Procedure, ActionInfo>(); this.errorCount = 0; this.checkingContext = new CheckingContext(null); this.program = program; this.enclosingProc = null; this.enclosingImpl = null; - this.canAccessSharedVars = false; - this.canAccessGhostVars = false; - this.minLayerNum = int.MaxValue; - this.maxLayerNum = -1; - this.leastUnimplementedLayerNum = int.MaxValue; + this.sharedVarsAccessed = null; + this.introducedLocalVarsUpperBound = int.MinValue; + + this.localVarToLocalVariableInfo = new Dictionary<Variable, LocalVariableInfo>(); + this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>(); + this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>(); + this.procToActionInfo = new Dictionary<Procedure, ActionInfo>(); + this.procToAtomicProcedureInfo = new Dictionary<Procedure, AtomicProcedureInfo>(); + this.pureCallLayer = new Dictionary<CallCmd, int>(); + foreach (var g in program.GlobalVariables) { List<int> layerNums = FindLayers(g.Attributes); if (layerNums.Count == 0) { - // Cannot access atomic actions + // Inaccessible from yielding and atomic procedures } else if (layerNums.Count == 1) { @@ -366,28 +469,137 @@ namespace Microsoft.Boogie } } } - - private HashSet<int> allCreatedLayerNums; - public IEnumerable<int> AllCreatedLayerNums + + private HashSet<int> allLayerNums; + public IEnumerable<int> AllLayerNums { get { - if (allCreatedLayerNums == null) + if (allLayerNums == null) { - allCreatedLayerNums = new HashSet<int>(); + allLayerNums = new HashSet<int>(); foreach (ActionInfo actionInfo in procToActionInfo.Values) { - allCreatedLayerNums.Add(actionInfo.createdAtLayerNum); + allLayerNums.Add(actionInfo.createdAtLayerNum); + } + foreach (var layerNums in absyToLayerNums.Values) + { + foreach (var layer in layerNums) + { + allLayerNums.Add(layer); + } } } - return allCreatedLayerNums; + return allLayerNums; + } + } + + private LayerRange FindLayerRange() + { + int maxIntroLayerNum = int.MinValue; + int minHideLayerNum = int.MaxValue; + foreach (var g in sharedVarsAccessed) + { + if (globalVarToSharedVarInfo[g].introLayerNum > maxIntroLayerNum) + { + maxIntroLayerNum = globalVarToSharedVarInfo[g].introLayerNum; + } + if (globalVarToSharedVarInfo[g].hideLayerNum < minHideLayerNum) + { + minHideLayerNum = globalVarToSharedVarInfo[g].hideLayerNum; + } } + return new LayerRange(maxIntroLayerNum, minHideLayerNum); } public void TypeCheck() { foreach (var proc in program.Procedures) { + if (!QKeyValue.FindBoolAttribute(proc.Attributes, "pure")) continue; + if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) + { + Error(proc, "Pure procedure must not yield"); + continue; + } + if (QKeyValue.FindBoolAttribute(proc.Attributes, "layer")) + { + Error(proc, "Pure procedure must not have layers"); + continue; + } + if (proc.Modifies.Count > 0) + { + Error(proc, "Pure procedure must not modify a global variable"); + continue; + } + procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(); + } + foreach (var proc in program.Procedures) + { + if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; + var procLayerNums = FindLayers(proc.Attributes); + if (procLayerNums.Count == 0) continue; + foreach (IdentifierExpr ie in proc.Modifies) + { + if (!globalVarToSharedVarInfo.ContainsKey(ie.Decl)) + { + Error(proc, "Atomic procedure cannot modify a global variable without layer numbers"); + continue; + } + } + int lower, upper; + if (procLayerNums.Count == 1) + { + lower = procLayerNums[0]; + upper = procLayerNums[0]; + } + else if (procLayerNums.Count == 2) + { + lower = procLayerNums[0]; + upper = procLayerNums[1]; + if (lower >= upper) + { + Error(proc, "Lower layer must be less than upper layer"); + continue; + } + } + else + { + Error(proc, "Atomic procedure must specify a layer range"); + continue; + } + LayerRange layerRange = new LayerRange(lower, upper); + procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(layerRange); + } + if (errorCount > 0) return; + + foreach (Implementation impl in program.Implementations) + { + if (!procToAtomicProcedureInfo.ContainsKey(impl.Proc)) continue; + var atomicProcedureInfo = procToAtomicProcedureInfo[impl.Proc]; + if (atomicProcedureInfo.isPure) + { + this.enclosingImpl = impl; + (new PurityChecker(this)).VisitImplementation(impl); + } + else + { + this.enclosingImpl = impl; + this.sharedVarsAccessed = new HashSet<Variable>(); + (new PurityChecker(this)).VisitImplementation(impl); + LayerRange upperBound = FindLayerRange(); + LayerRange lowerBound = atomicProcedureInfo.layerRange; + if (!lowerBound.Subset(upperBound)) + { + Error(impl, "Atomic procedure cannot access global variable"); + } + this.sharedVarsAccessed = null; + } + } + if (errorCount > 0) return; + + foreach (var proc in program.Procedures) + { if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; int createdAtLayerNum; // must be initialized by the following code, otherwise it is an error @@ -428,25 +640,21 @@ namespace Microsoft.Boogie continue; } - minLayerNum = int.MaxValue; - maxLayerNum = -1; - canAccessSharedVars = true; + sharedVarsAccessed = new HashSet<Variable>(); enclosingProc = proc; enclosingImpl = null; base.VisitEnsures(e); - canAccessSharedVars = false; - if (maxLayerNum > createdAtLayerNum) - { - Error(e, "A variable being accessed is introduced after this action is created"); - } - else if (availableUptoLayerNum > minLayerNum) + LayerRange upperBound = FindLayerRange(); + LayerRange lowerBound = new LayerRange(createdAtLayerNum, availableUptoLayerNum); + if (lowerBound.Subset(upperBound)) { - Error(e, "A variable being accessed is hidden before this action becomes unavailable"); + procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum); } else { - procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum); + Error(e, "A variable being accessed in this action is unavailable"); } + sharedVarsAccessed = null; } if (errorCount > 0) continue; if (!procToActionInfo.ContainsKey(proc)) @@ -463,52 +671,63 @@ namespace Microsoft.Boogie } } if (errorCount > 0) return; + foreach (var impl in program.Implementations) { if (!procToActionInfo.ContainsKey(impl.Proc)) continue; + ActionInfo actionInfo = procToActionInfo[impl.Proc]; procToActionInfo[impl.Proc].hasImplementation = true; - } - foreach (var proc in procToActionInfo.Keys) - { - ActionInfo actionInfo = procToActionInfo[proc]; - if (actionInfo.isExtern && actionInfo.hasImplementation) + if (actionInfo.isExtern) { - Error(proc, "Extern procedure cannot have an implementation"); - continue; + Error(impl.Proc, "Extern procedure cannot have an implementation"); } - if (actionInfo.isExtern || actionInfo.hasImplementation) continue; - if (leastUnimplementedLayerNum == int.MaxValue) + } + if (errorCount > 0) return; + + foreach (Procedure proc in procToActionInfo.Keys) + { + for (int i = 0; i < proc.InParams.Count; i++) { - leastUnimplementedLayerNum = actionInfo.createdAtLayerNum; + Variable v = proc.InParams[i]; + var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } - else if (leastUnimplementedLayerNum != actionInfo.createdAtLayerNum) + for (int i = 0; i < proc.OutParams.Count; i++) { - Error(proc, "All unimplemented atomic actions must be created at the same layer"); + Variable v = proc.OutParams[i]; + var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } } - foreach (var g in this.globalVarToSharedVarInfo.Keys) + foreach (Implementation node in program.Implementations) { - var info = globalVarToSharedVarInfo[g]; - if (!this.AllCreatedLayerNums.Contains(info.introLayerNum)) + if (!procToActionInfo.ContainsKey(node.Proc)) continue; + foreach (Variable v in node.LocVars) { - Error(g, "Variable must be introduced with creation of some atomic action"); + var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum); + if (layer == int.MinValue) continue; + localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer); } - if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum)) + for (int i = 0; i < node.Proc.InParams.Count; i++) { - Error(g, "Variable must be hidden with creation of some atomic action"); + Variable v = node.Proc.InParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(v)) continue; + var layer = localVarToLocalVariableInfo[v].layer; + localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(layer); } - } - if (errorCount > 0) return; - this.VisitProgram(program); - foreach (Procedure proc in program.Procedures) - { - if (procToActionInfo.ContainsKey(proc)) continue; - foreach (var ie in proc.Modifies) + for (int i = 0; i < node.Proc.OutParams.Count; i++) { - if (!SharedVariables.Contains(ie.Decl)) continue; - Error(proc, "A ghost procedure must not modify a global variable with layer annotation"); + Variable v = node.Proc.OutParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(v)) continue; + var layer = localVarToLocalVariableInfo[v].layer; + localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(layer); } } + if (errorCount > 0) return; + + this.VisitProgram(program); if (errorCount > 0) return; YieldTypeChecker.PerformYieldSafeCheck(this); new LayerEraser().VisitProgram(program); @@ -516,9 +735,26 @@ namespace Microsoft.Boogie public IEnumerable<Variable> SharedVariables { - get { return this.globalVarToSharedVarInfo.Keys; } + get { return this.globalVarToSharedVarInfo.Keys; } } - + + private int FindLocalVariableLayer(Declaration decl, Variable v, int enclosingProcLayerNum) + { + var layers = FindLayers(v.Attributes); + if (layers.Count == 0) return int.MinValue; + if (layers.Count > 1) + { + Error(decl, "Incorrect number of layers"); + return int.MinValue; + } + if (layers[0] > enclosingProcLayerNum) + { + Error(decl, "Layer of local variable cannot be greater than the creation layer of enclosing procedure"); + return int.MinValue; + } + return layers[0]; + } + public override Implementation VisitImplementation(Implementation node) { if (!procToActionInfo.ContainsKey(node.Proc)) @@ -527,17 +763,9 @@ namespace Microsoft.Boogie } this.enclosingImpl = node; this.enclosingProc = null; - ghostVars = new HashSet<Variable>(); - foreach (Variable v in node.LocVars) - { - if (QKeyValue.FindBoolAttribute(v.Attributes, "ghost")) - { - ghostVars.Add(v); - } - } return base.VisitImplementation(node); } - + public override Procedure VisitProcedure(Procedure node) { if (!procToActionInfo.ContainsKey(node)) @@ -584,23 +812,117 @@ namespace Microsoft.Boogie { Error(node, "The callee is not available in the caller procedure"); } - return base.VisitCallCmd(node); + for (int i = 0; i < node.Ins.Count; i++) + { + Visit(node.Ins[i]); + if (introducedLocalVarsUpperBound != int.MinValue) + { + var formal = node.Proc.InParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(formal) || + introducedLocalVarsUpperBound > localVarToLocalVariableInfo[formal].layer) + { + Error(node, "An introduced local variable is accessed but not available"); + } + introducedLocalVarsUpperBound = int.MinValue; + } + } + for (int i = 0; i < node.Outs.Count; i++) + { + var formal = node.Proc.OutParams[i]; + if (!localVarToLocalVariableInfo.ContainsKey(formal)) continue; + var actual = node.Outs[i].Decl; + if (localVarToLocalVariableInfo.ContainsKey(actual) && + localVarToLocalVariableInfo[formal].layer <= localVarToLocalVariableInfo[actual].layer) + continue; + Error(node, "Formal parameter of call must be introduced no later than the actual parameter"); + } + return node; } - else + else if (procToAtomicProcedureInfo.ContainsKey(node.Proc)) { - foreach (var ie in node.Outs) + var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; + if (atomicProcedureInfo.isPure) { - if (ghostVars.Contains(ie.Decl)) continue; - Error(node, "The output of a ghost procedure must be assigned to a ghost variable"); + if (node.Outs.Count > 0) + { + int inferredLayer = int.MinValue; + foreach (var ie in node.Outs) + { + if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) continue; + if (inferredLayer < localVarToLocalVariableInfo[ie.Decl].layer) + { + inferredLayer = localVarToLocalVariableInfo[ie.Decl].layer; + } + } + pureCallLayer[node] = inferredLayer; + if (inferredLayer != int.MinValue) + { + foreach (var ie in node.Outs) + { + if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) + { + Error(node, "Output variable must be introduced"); + } + else if (inferredLayer != localVarToLocalVariableInfo[ie.Decl].layer) + { + Error(node, "All output variables must be introduced at the same layer"); + } + } + } + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + foreach (var e in node.Ins) + { + Visit(e); + if (inferredLayer < introducedLocalVarsUpperBound) + { + Error(node, "An introduced local variable is not accessible"); + } + introducedLocalVarsUpperBound = int.MinValue; + } + } + else + { + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + int inferredLayer = int.MinValue; + foreach (var e in node.Ins) + { + Visit(e); + if (inferredLayer < introducedLocalVarsUpperBound) + { + inferredLayer = introducedLocalVarsUpperBound; + } + introducedLocalVarsUpperBound = int.MinValue; + } + pureCallLayer[node] = inferredLayer; + } } - bool savedCanAccessSharedVars = canAccessSharedVars; - bool savedCanAccessAuxVars = canAccessGhostVars; - canAccessSharedVars = true; - canAccessGhostVars = true; - var retVal = base.VisitCallCmd(node); - canAccessSharedVars = savedCanAccessSharedVars; - canAccessGhostVars = savedCanAccessAuxVars; - return retVal; + else + { + if (enclosingProcLayerNum != atomicProcedureInfo.layerRange.upperLayerNum) + { + Error(node, "Creation layer of caller must be the upper bound of the layer range of callee"); + } + foreach (var ie in node.Proc.Modifies) + { + if (enclosingProcLayerNum != globalVarToSharedVarInfo[ie.Decl].introLayerNum) + { + Error(node, "Creation layer of caller must be identical to the introduction layer of modified variable"); + } + } + foreach (var ie in node.Outs) + { + if (localVarToLocalVariableInfo.ContainsKey(ie.Decl) && + enclosingProcLayerNum == localVarToLocalVariableInfo[ie.Decl].layer) + continue; + Error(node, "Output variable must be introduced at the creation layer of caller"); + } + } + return node; + } + else + { + Error(node, "A yielding procedure can call only atomic or yielding procedures"); + return node; } } @@ -618,8 +940,8 @@ namespace Microsoft.Boogie isLeftMover = isLeftMover && actionInfo.IsLeftMover; isRightMover = isRightMover && actionInfo.IsRightMover; if (actionInfo.createdAtLayerNum > maxCalleeLayerNum) - { - maxCalleeLayerNum = actionInfo.createdAtLayerNum; + { + maxCalleeLayerNum = actionInfo.createdAtLayerNum; } if (actionInfo is AtomicActionInfo) { @@ -645,66 +967,36 @@ namespace Microsoft.Boogie return base.VisitParCallCmd(node); } - public override Cmd VisitAssignCmd(AssignCmd node) - { - Contract.Ensures(Contract.Result<Cmd>() == node); - for (int i = 0; i < node.Lhss.Count; ++i) - { - bool savedCanAccessSharedVars = canAccessSharedVars; - bool savedCanAccessAuxVars = canAccessGhostVars; - Variable v = node.Lhss[i].DeepAssignedVariable; - if (v is LocalVariable && ghostVars.Contains(v)) - { - canAccessSharedVars = true; - canAccessGhostVars = true; - } - this.Visit(node.Lhss[i]); - this.Visit(node.Rhss[i]); - canAccessSharedVars = savedCanAccessSharedVars; - canAccessGhostVars = savedCanAccessAuxVars; - } - return node; - } - public override Expr VisitIdentifierExpr(IdentifierExpr node) { if (node.Decl is GlobalVariable) { - if (!canAccessSharedVars) + if (sharedVarsAccessed == null) { Error(node, "Shared variable can be accessed only in atomic actions or specifications"); } else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl)) { - if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum) - { - minLayerNum = this.globalVarToSharedVarInfo[node.Decl].hideLayerNum; - } - if (this.globalVarToSharedVarInfo[node.Decl].introLayerNum > maxLayerNum) - { - maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum; - } + sharedVarsAccessed.Add(node.Decl); } else { Error(node, "Accessed shared variable must have layer annotation"); } } - else if (node.Decl is LocalVariable && ghostVars.Contains(node.Decl) && !canAccessGhostVars) + else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl)) { - Error(node, "Ghost variable can be accessed only in assertions"); - } - + var localVariableInfo = localVarToLocalVariableInfo[node.Decl]; + if (introducedLocalVarsUpperBound < localVariableInfo.layer) + { + introducedLocalVarsUpperBound = localVariableInfo.layer; + } + } return base.VisitIdentifierExpr(node); } - + public override Ensures VisitEnsures(Ensures ensures) { - minLayerNum = int.MaxValue; - maxLayerNum = -1; - canAccessSharedVars = true; - Ensures ret = base.VisitEnsures(ensures); - canAccessSharedVars = false; ActionInfo actionInfo = procToActionInfo[enclosingProc]; AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; if (atomicActionInfo != null && atomicActionInfo.ensures == ensures) @@ -713,35 +1005,53 @@ namespace Microsoft.Boogie } else { + sharedVarsAccessed = new HashSet<Variable>(); + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + base.VisitEnsures(ensures); CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum); + if (introducedLocalVarsUpperBound > Least(FindLayers(ensures.Attributes))) + { + Error(ensures, "An introduced local variable is accessed but not available"); + } + introducedLocalVarsUpperBound = int.MinValue; + sharedVarsAccessed = null; } - return ret; + return ensures; } - + public override Requires VisitRequires(Requires requires) { - minLayerNum = int.MaxValue; - maxLayerNum = -1; - canAccessSharedVars = true; - Requires ret = base.VisitRequires(requires); - canAccessSharedVars = false; + sharedVarsAccessed = new HashSet<Variable>(); + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + base.VisitRequires(requires); CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum); - return ret; + if (introducedLocalVarsUpperBound > Least(FindLayers(requires.Attributes))) + { + Error(requires, "An introduced local variable is accessed but not available"); + } + introducedLocalVarsUpperBound = int.MinValue; + sharedVarsAccessed = null; + return requires; } public override Cmd VisitAssertCmd(AssertCmd node) { if (enclosingImpl == null) + { + // in this case, we are visiting an assert inside a CodeExpr return base.VisitAssertCmd(node); - minLayerNum = int.MaxValue; - maxLayerNum = -1; - canAccessSharedVars = true; - canAccessGhostVars = true; - Cmd ret = base.VisitAssertCmd(node); - canAccessGhostVars = false; - canAccessSharedVars = false; + } + sharedVarsAccessed = new HashSet<Variable>(); + Debug.Assert(introducedLocalVarsUpperBound == int.MinValue); + base.VisitAssertCmd(node); CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum); - return ret; + if (introducedLocalVarsUpperBound > Least(FindLayers(node.Attributes))) + { + Error(node, "An introduced local variable is accessed but not available"); + } + introducedLocalVarsUpperBound = int.MinValue; + sharedVarsAccessed = null; + return node; } private List<int> RemoveDuplicatesAndSort(List<int> attrs) @@ -760,18 +1070,15 @@ namespace Microsoft.Boogie Error(node, "layer not present"); return; } + LayerRange upperBound = FindLayerRange(); absyToLayerNums[node] = new HashSet<int>(); foreach (int layerNum in attrs) { - if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum)) - { - Error(node, "Illegal layer number"); - } - else if (layerNum > enclosingProcLayerNum) + if (layerNum > enclosingProcLayerNum) { Error(node, "The layer cannot be greater than the layer of enclosing procedure"); } - else if (maxLayerNum < layerNum && layerNum <= minLayerNum) + else if (upperBound.Contains(layerNum)) { absyToLayerNums[node].Add(layerNum); } @@ -787,5 +1094,67 @@ namespace Microsoft.Boogie checkingContext.Error(node, message); errorCount++; } + + private class PurityChecker : StandardVisitor + { + private CivlTypeChecker civlTypeChecker; + + public PurityChecker(CivlTypeChecker civlTypeChecker) + { + this.civlTypeChecker = civlTypeChecker; + } + + public override Cmd VisitCallCmd(CallCmd node) + { + Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc; + if (!civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc)) + { + civlTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure"); + return base.VisitCallCmd(node); + } + var callerInfo = civlTypeChecker.procToAtomicProcedureInfo[enclosingProc]; + var calleeInfo = civlTypeChecker.procToAtomicProcedureInfo[node.Proc]; + if (calleeInfo.isPure) + { + // do nothing + } + else if (callerInfo.isPure) + { + civlTypeChecker.Error(node, "Pure procedure can only call pure procedures"); + } + else if (!callerInfo.layerRange.Subset(calleeInfo.layerRange)) + { + civlTypeChecker.Error(node, "Caller layers must be subset of callee layers"); + } + return base.VisitCallCmd(node); + } + + public override Cmd VisitParCallCmd(ParCallCmd node) + { + civlTypeChecker.Error(node, "Atomic procedures cannot make parallel calls"); + return node; + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc; + if (node.Decl is GlobalVariable) + { + if (civlTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure) + { + civlTypeChecker.Error(node, "Pure procedure cannot access global variables"); + } + else if (!civlTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl)) + { + civlTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers"); + } + else + { + civlTypeChecker.sharedVarsAccessed.Add(node.Decl); + } + } + return node; + } + } } -}
\ No newline at end of file +} diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj index f15ebca3..113019fd 100644 --- a/Source/Concurrency/Concurrency.csproj +++ b/Source/Concurrency/Concurrency.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" /> <PropertyGroup> @@ -73,11 +73,11 @@ <ItemGroup> <Compile Include="LinearSets.cs" /> <Compile Include="MoverCheck.cs" /> - <Compile Include="OwickiGries.cs" /> + <Compile Include="CivlRefinement.cs" /> <Compile Include="Program.cs" /> <Compile Include="Properties\AssemblyInfo.cs" /> <Compile Include="SimulationRelation.cs" /> - <Compile Include="TypeCheck.cs" /> + <Compile Include="CivlTypeChecker.cs" /> <Compile Include="YieldTypeChecker.cs" /> </ItemGroup> <ItemGroup> @@ -112,4 +112,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project>
\ No newline at end of file +</Project> diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index 0fa04b1b..f654b688 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -626,10 +626,9 @@ namespace Microsoft.Boogie var domainName = FindDomainName(v); domainNameToScope[domainName].Add(v); } - foreach (Variable v in program.GlobalVariables) + foreach (Variable v in globalVarToDomainName.Keys) { var domainName = FindDomainName(v); - if (domainName == null) continue; domainNameToScope[domainName].Add(v); } foreach (string domainName in linearDomains.Keys) diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 7c6d4ac4..732bcaa4 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -10,29 +10,29 @@ namespace Microsoft.Boogie public class MoverCheck { LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; List<Declaration> decls; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache; HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache; - private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.decls = decls; this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); } - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls) { - if (moverTypeChecker.procToActionInfo.Count == 0) + if (civlTypeChecker.procToActionInfo.Count == 0) return; - List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; }); - List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(civlTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; }); Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>(); @@ -60,8 +60,8 @@ namespace Microsoft.Boogie currPool = pools[currLayerNum]; } - Program program = moverTypeChecker.program; - MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls); + Program program = civlTypeChecker.program; + MoverCheck moverChecking = new MoverCheck(linearTypeChecker, civlTypeChecker, decls); foreach (int layerNum in pools.Keys) { foreach (AtomicActionInfo first in pools[layerNum]) @@ -537,7 +537,7 @@ namespace Microsoft.Boogie ensures.Add(ensureCheck); string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks); impl.Proc = proc; @@ -580,7 +580,7 @@ namespace Microsoft.Boogie requires.Add(new Requires(false, assertCmd.Expr)); string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks); impl.Proc = proc; @@ -628,7 +628,7 @@ namespace Microsoft.Boogie requires.Add(new Requires(false, assertCmd.Expr)); string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks); impl.Proc = proc; @@ -662,7 +662,7 @@ namespace Microsoft.Boogie blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken))); string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name); List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks); impl.Proc = proc; diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index b56e1cf3..1be7cc07 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -7,20 +7,20 @@ namespace Microsoft.Boogie { public class Concurrency { - public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker) + public static void Transform(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker) { List<Declaration> originalDecls = new List<Declaration>(); Program program = linearTypeChecker.program; foreach (var decl in program.TopLevelDeclarations) { Procedure proc = decl as Procedure; - if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc)) + if (proc != null && civlTypeChecker.procToActionInfo.ContainsKey(proc)) { originalDecls.Add(proc); continue; } Implementation impl = decl as Implementation; - if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) + if (impl != null && civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) { originalDecls.Add(impl); } @@ -29,12 +29,12 @@ namespace Microsoft.Boogie List<Declaration> decls = new List<Declaration>(); if (!CommandLineOptions.Clo.TrustAtomicityTypes) { - MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls); + MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls); } - OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls); + CivlRefinement.AddCheckers(linearTypeChecker, civlTypeChecker, decls); foreach (Declaration decl in decls) { - decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes); + decl.Attributes = CivlRefinement.RemoveYieldsAttribute(decl.Attributes); } program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x)); program.AddTopLevelDeclarations(decls); diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index a698c8fd..ed59d3ad 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -81,7 +81,7 @@ namespace Microsoft.Boogie Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); } } @@ -97,7 +97,7 @@ namespace Microsoft.Boogie Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); } } @@ -115,7 +115,7 @@ namespace Microsoft.Boogie Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation(); if (simulationRelation[initialState].Count == 0) { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); } } @@ -124,7 +124,7 @@ namespace Microsoft.Boogie foreach (Cmd cmd in block.Cmds) { AssertCmd assertCmd = cmd as AssertCmd; - if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum)) + if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && civlTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum)) { return true; } @@ -132,25 +132,25 @@ namespace Microsoft.Boogie return false; } - public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker) + public static void PerformYieldSafeCheck(CivlTypeChecker civlTypeChecker) { - foreach (var impl in moverTypeChecker.program.Implementations) + foreach (var impl in civlTypeChecker.program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; + if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; impl.PruneUnreachableBlocks(); Graph<Block> implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); - int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) + int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; + foreach (int layerNum in civlTypeChecker.AllLayerNums) { if (layerNum > specLayerNum) continue; - YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers); + YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers); } } } int stateCounter; - MoverTypeChecker moverTypeChecker; + CivlTypeChecker civlTypeChecker; Implementation impl; int currLayerNum; Dictionary<Absy, int> absyToNode; @@ -160,9 +160,9 @@ namespace Microsoft.Boogie Dictionary<Tuple<int, int>, int> edgeLabels; IEnumerable<Block> loopHeaders; - private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders) + private YieldTypeChecker(CivlTypeChecker civlTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders) { - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.impl = impl; this.currLayerNum = currLayerNum; this.loopHeaders = loopHeaders; @@ -226,20 +226,20 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd; if (callCmd.IsAsync) { - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; if (currLayerNum <= actionInfo.createdAtLayerNum) edgeLabels[edge] = 'L'; else edgeLabels[edge] = 'B'; } - else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc)) + else if (!civlTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc)) { edgeLabels[edge] = 'P'; } else { MoverType moverType; - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; if (actionInfo.createdAtLayerNum >= currLayerNum) { moverType = MoverType.Top; @@ -280,7 +280,7 @@ namespace Microsoft.Boogie bool isLeftMover = true; foreach (CallCmd callCmd in parCallCmd.CallCmds) { - if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) + if (civlTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) { isYield = true; } @@ -294,7 +294,7 @@ namespace Microsoft.Boogie int numAtomicActions = 0; foreach (CallCmd callCmd in parCallCmd.CallCmds) { - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; isRightMover = isRightMover && actionInfo.IsRightMover; isLeftMover = isLeftMover && actionInfo.IsLeftMover; if (actionInfo is AtomicActionInfo) diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 36c99b7b..8a8558bf 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -696,6 +696,8 @@ namespace Microsoft.Boogie { } } + public readonly ISet<string> NecessaryAssumes = new HashSet<string>(); + public IEnumerable<Block> Blocks() { return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); @@ -733,6 +735,45 @@ namespace Microsoft.Boogie { } } + + /// <summary> + /// Finds blocks that break out of a loop in NaturalLoops(header, backEdgeNode) + /// </summary> + /// <param name="header"></param> + /// <param name="backEdgeNode"></param> + /// <returns></returns> + private HashSet<Block> GetBreakBlocksOfLoop(Block header, Block backEdgeNode, Graph<Block/*!*/>/*!*/ g) + { + Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option"); + var immSuccBlks = new HashSet<Block>(); + var loopBlocks = g.NaturalLoops(header, backEdgeNode); + foreach (Block/*!*/ block in loopBlocks) + { + Contract.Assert(block != null); + var auxCmd = block.TransferCmd as GotoCmd; + if (auxCmd == null) continue; + foreach (var bl in auxCmd.labelTargets) + { + if (loopBlocks.Contains(bl)) continue; + immSuccBlks.Add(bl); + } + } + return immSuccBlks; + } + + private HashSet<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g) + { + Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option"); + var allBlocksInNaturalLoops = new HashSet<Block>(); + foreach (Block/*!*/ source in g.BackEdgeNodes(header)) + { + Contract.Assert(source != null); + g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b)); + } + return allBlocksInNaturalLoops; + } + + void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g, List<Implementation/*!*/>/*!*/ loopImpls, Dictionary<string, Dictionary<string, Block>> fullMap) { @@ -788,7 +829,13 @@ namespace Microsoft.Boogie { foreach (Block/*!*/ b in g.BackEdgeNodes(header)) { Contract.Assert(b != null); - foreach (Block/*!*/ block in g.NaturalLoops(header, b)) + HashSet<Block> immSuccBlks = new HashSet<Block>(); + if (detLoopExtract) + { + //Need to get the blocks that exit the loop, as we need to add them to targets and footprint + immSuccBlks = GetBreakBlocksOfLoop(header, b, g); + } + foreach (Block/*!*/ block in g.NaturalLoops(header, b).Union(immSuccBlks)) { Contract.Assert(block != null); foreach (Cmd/*!*/ cmd in block.Cmds) @@ -943,18 +990,16 @@ namespace Microsoft.Boogie { GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd; Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null && auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1); + //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode + var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source); foreach(var bl in auxGotoCmd.labelTargets) { - bool found = false; - foreach(var n in g.NaturalLoops(header, source)) { //very expensive, can we do a contains? - if (bl == n) { //clarify: is this the right comparison? - found = true; - break; - } - } - if (!found) { + if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g) + !loopNodes.Contains(bl)) { Block auxNewBlock = new Block(); auxNewBlock.Label = ((Block)bl).Label; - auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds); + //these blocks may have read/write locals that are not present in naturalLoops + //we need to capture these variables + auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds); //add restoration code for such blocks if (loopHeaderToAssignCmd.ContainsKey(header)) { @@ -2196,6 +2241,7 @@ namespace Microsoft.Boogie { } public class Incarnation : LocalVariable { public int incarnationNumber; + public readonly Variable OriginalVariable; public Incarnation(Variable/*!*/ var, int i) : base( var.tok, @@ -2203,6 +2249,7 @@ namespace Microsoft.Boogie { ) { Contract.Requires(var != null); incarnationNumber = i; + OriginalVariable = var; } } diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 404945a9..2e33e1dd 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2463,6 +2463,12 @@ namespace Microsoft.Boogie { } finally { rc.TypeBinderState = previousTypeBinderState; } + + var id = QKeyValue.FindStringAttribute(Attributes, "id"); + if (id != null) + { + rc.AddStatementId(tok, id); + } } public override void AddAssignedVariables(List<Variable> vars) { @@ -2890,6 +2896,12 @@ namespace Microsoft.Boogie { public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); Expr.Resolve(rc); + + var id = QKeyValue.FindStringAttribute(Attributes, "id"); + if (id != null) + { + rc.AddStatementId(tok, id); + } } public override void AddAssignedVariables(List<Variable> vars) { //Contract.Requires(vars != null); @@ -3206,8 +3218,14 @@ namespace Microsoft.Boogie { this.Expr.Emit(stream); stream.WriteLine(";"); } + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + ResolveAttributes(Attributes, rc); + base.Resolve(rc); + } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); + TypecheckAttributes(Attributes, tc); Expr.Typecheck(tc); Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition if (!Expr.Type.Unify(Type.Bool)) { diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 9f94490b..3a27eddf 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -338,6 +338,17 @@ namespace Microsoft.Boogie { public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); + + if ((Key == "minimize" || Key == "maximize") && Params.Count != 1) + { + rc.Error(this, "attributes :minimize and :maximize accept only one argument"); + } + + if (Key == "verified_under" && Params.Count != 1) + { + rc.Error(this, "attribute :verified_under accepts only one argument"); + } + foreach (object p in Params) { if (p is Expr) { ((Expr)p).Resolve(rc); @@ -348,8 +359,20 @@ namespace Microsoft.Boogie { public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); foreach (object p in Params) { - if (p is Expr) { - ((Expr)p).Typecheck(tc); + var expr = p as Expr; + if (expr != null) { + expr.Typecheck(tc); + } + if ((Key == "minimize" || Key == "maximize") + && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv))) + { + tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv"); + break; + } + if (Key == "verified_under" && (expr == null || !expr.Type.IsBool)) + { + tc.Error(this, "attribute :verified_under accepts only one argument of type bool"); + break; } } } diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2be1cdf7..e9aa3ceb 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -11,6 +11,7 @@ using System.IO; using System.Linq; using System.Diagnostics; using System.Diagnostics.Contracts; +using System.Text.RegularExpressions; namespace Microsoft.Boogie { public class CommandLineOptionEngine @@ -478,6 +479,8 @@ namespace Microsoft.Boogie { public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; public bool PrintAssignment = false; + // TODO(wuestholz): Add documentation for this flag. + public bool PrintNecessaryAssumes = false; public int InlineDepth = -1; public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values public bool UseUncheckedContracts = false; @@ -588,7 +591,7 @@ namespace Microsoft.Boogie { } } - public string OwickiGriesDesugaredOutputFile = null; + public string CivlDesugaredFile = null; public bool TrustAtomicityTypes = false; public bool TrustNonInterference = false; public int TrustLayersUpto = -1; @@ -915,9 +918,9 @@ namespace Microsoft.Boogie { } return true; - case "OwickiGries": + case "CivlDesugaredFile": if (ps.ConfirmArgumentCount(1)) { - OwickiGriesDesugaredOutputFile = args[ps.i]; + CivlDesugaredFile = args[ps.i]; } return true; @@ -1502,7 +1505,7 @@ namespace Microsoft.Boogie { return true; case "verifySnapshots": - ps.GetNumericArgument(ref VerifySnapshots, 3); + ps.GetNumericArgument(ref VerifySnapshots, 4); return true; case "traceCaching": @@ -1618,6 +1621,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) || ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) || ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || + ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) || ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) || ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) || ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) || @@ -1700,7 +1704,7 @@ namespace Microsoft.Boogie { // no preference return true; } - return ProcsToCheck.Contains(methodFullname); + return ProcsToCheck.Any(s => Regex.IsMatch(methodFullname, "^" + Regex.Escape(s).Replace(@"\*", ".*") + "$")); } public virtual StringCollection ParseNamedArgumentList(string argList) { @@ -1857,7 +1861,15 @@ namespace Microsoft.Boogie { Multiple .bpl files supplied on the command line are concatenated into one Boogie program. - /proc:<p> : limits which procedures to check + /proc:<p> : Only check procedures matched by pattern <p>. This option + may be specified multiple times to match multiple patterns. + The pattern <p> matches the whole procedure name (i.e. + pattern ""foo"" will only match a procedure called foo and + not fooBar). The pattern <p> may contain * wildcards which + match any character zero or more times. For example the + pattern ""ab*d"" would match abd, abcd and abccd but not + Aabd nor abdD. The pattern ""*ab*d*"" would match abd, + abcd, abccd, Abd and abdD. /noResolve : parse only /noTypecheck : parse and resolve only @@ -1961,6 +1973,10 @@ namespace Microsoft.Boogie { 0 - do not use any verification result caching (default) 1 - use the basic verification result caching 2 - use the more advanced verification result caching + 3 - use the more advanced caching and report errors according + to the new source locations for errors and their + related locations (but not /errorTrace and CaptureState + locations) /verifySeparately verify each input program separately /removeEmptyBlocks:<c> diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 474a91dd..279e00bf 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -339,6 +339,18 @@ namespace Microsoft.Boogie { varContext = varContext.ParentContext; } + public readonly ISet<string> StatementIds = new HashSet<string>(); + + public void AddStatementId(IToken tok, string name) + { + if (StatementIds.Contains(name)) + { + Error(tok, "more than one statement with same id: " + name); + return; + } + StatementIds.Add(name); + } + public void AddVariable(Variable var, bool global) { Contract.Requires(var != null); var previous = FindVariable(cce.NonNull(var.Name), !global); diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index f2d58045..9bc855be 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -135,7 +135,7 @@ namespace Microsoft.Boogie foreach (var e in errorInfo.Aux) { - if (!(skipExecutionTrace && e.Category.Contains("Execution trace"))) + if (!(skipExecutionTrace && e.Category != null && e.Category.Contains("Execution trace"))) { ReportBplError(e.Tok, e.FullMsg, false, tw); } @@ -151,25 +151,18 @@ namespace Microsoft.Boogie { Contract.Requires(message != null); - if (category != null) - { + if (category != null) { message = string.Format("{0}: {1}", category, message); } string s; - if (tok != null) - { + if (tok != null) { s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message); - } - else - { + } else { s = message; } - if (error) - { + if (error) { ErrorWriteLine(tw, s); - } - else - { + } else { tw.WriteLine(s); } } @@ -489,8 +482,8 @@ namespace Microsoft.Boogie } LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; - PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out moverTypeChecker); + CivlTypeChecker civlTypeChecker; + PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out civlTypeChecker); if (oc != PipelineOutcome.ResolvedAndTypeChecked) return; @@ -507,13 +500,13 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.StratifiedInlining == 0) { - Concurrency.Transform(linearTypeChecker, moverTypeChecker); + Concurrency.Transform(linearTypeChecker, civlTypeChecker); (new LinearEraser()).VisitProgram(program); - if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null) + if (CommandLineOptions.Clo.CivlDesugaredFile != null) { int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; CommandLineOptions.Clo.PrintUnstructured = 1; - PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint); + PrintBplFile(CommandLineOptions.Clo.CivlDesugaredFile, program, false, false, CommandLineOptions.Clo.PrettyPrint); CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; } } @@ -699,13 +692,13 @@ namespace Microsoft.Boogie /// - TypeCheckingError if a type checking error occurred /// - ResolvedAndTypeChecked if both resolution and type checking succeeded /// </summary> - public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out MoverTypeChecker moverTypeChecker) + public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out CivlTypeChecker civlTypeChecker) { Contract.Requires(program != null); Contract.Requires(bplFileName != null); linearTypeChecker = null; - moverTypeChecker = null; + civlTypeChecker = null; // ---------- Resolve ------------------------------------------------------------ @@ -742,11 +735,11 @@ namespace Microsoft.Boogie CollectModSets(program); - moverTypeChecker = new MoverTypeChecker(program); - moverTypeChecker.TypeCheck(); - if (moverTypeChecker.errorCount != 0) + civlTypeChecker = new CivlTypeChecker(program); + civlTypeChecker.TypeCheck(); + if (civlTypeChecker.errorCount != 0) { - Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, GetFileNameForConsole(bplFileName)); + Console.WriteLine("{0} type checking errors detected in {1}", civlTypeChecker.errorCount, GetFileNameForConsole(bplFileName)); return PipelineOutcome.TypeCheckingError; } @@ -1015,6 +1008,11 @@ namespace Microsoft.Boogie CleanupCheckers(requestId); } + if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any()) + { + Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes)); + } + cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close(); outputCollector.WriteMoreOutput(); @@ -1114,23 +1112,23 @@ namespace Microsoft.Boogie printer.Inform(string.Format("Verifying {0} ...", impl.Name), output); int priority = 0; - if (0 < CommandLineOptions.Clo.VerifySnapshots) - { - verificationResult = Cache.Lookup(impl, out priority); - } - var wasCached = false; - if (verificationResult != null && priority == Priority.SKIP) - { - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start); - } + if (0 < CommandLineOptions.Clo.VerifySnapshots) { + var cachedResults = Cache.Lookup(impl, out priority); + if (cachedResults != null && priority == Priority.SKIP) { + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start); + } - printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output); - wasCached = true; + printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output); + if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) { + verificationResult = cachedResults; + wasCached = true; + } + } } - else + + if (!wasCached) { #region Verify the implementation @@ -1365,8 +1363,8 @@ namespace Microsoft.Boogie Program p = ParseBoogieProgram(new List<string> { filename }, false); System.Diagnostics.Debug.Assert(p != null); LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; - PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out moverTypeChecker); + CivlTypeChecker civlTypeChecker; + PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out civlTypeChecker); System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked); return p; } @@ -1466,11 +1464,11 @@ namespace Microsoft.Boogie printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw); - ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit); + ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors); } - private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit) + private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List<Counterexample> errors) { ErrorInformation errorInfo = null; @@ -1479,10 +1477,69 @@ namespace Microsoft.Boogie case VCGen.Outcome.ReachedBound: tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound)); break; + case VCGen.Outcome.Errors: case VCGen.Outcome.TimedOut: if (implName != null && implTok != null) { - errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId); + if (outcome == ConditionGeneration.Outcome.TimedOut || (errors != null && errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts))) + { + errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification of '{1}' timed out after {0} seconds", timeLimit, implName), requestId); + } + + // Report timed out assertions as auxiliary info. + if (errors != null) + { + var cmpr = new CounterexampleComparer(); + var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList(); + timedOutAssertions.Sort(cmpr); + if (0 < timedOutAssertions.Count) + { + errorInfo.Msg += string.Format(" with {0} check(s) that timed out individually", timedOutAssertions.Count); + } + foreach (Counterexample error in timedOutAssertions) + { + var callError = error as CallCounterexample; + var returnError = error as ReturnCounterexample; + var assertError = error as AssertCounterexample; + IToken tok = null; + string msg = null; + if (callError != null) + { + tok = callError.FailingCall.tok; + msg = callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold."; + } + else if (returnError != null) + { + tok = returnError.FailingReturn.tok; + msg = "A postcondition might not hold on this return path."; + } + else + { + tok = assertError.FailingAssert.tok; + if (assertError.FailingAssert is LoopInitAssertCmd) + { + msg = "This loop invariant might not hold on entry."; + } + else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd) + { + msg = "This loop invariant might not be maintained by the loop."; + } + else + { + msg = assertError.FailingAssert.ErrorData as string; + if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null) + { + msg = assertError.FailingAssert.ErrorMessage; + } + if (msg == null) + { + msg = "This assertion might not hold."; + } + } + } + errorInfo.AddAuxInfo(tok, msg, "Unverified check due to timeout"); + } + } } break; case VCGen.Outcome.OutOfMemory: @@ -1509,6 +1566,10 @@ namespace Microsoft.Boogie er(errorInfo); } } + else + { + printer.WriteErrorInformation(errorInfo, tw); + } } } @@ -1582,8 +1643,9 @@ namespace Microsoft.Boogie } else { - Interlocked.Add(ref stats.ErrorCount, errors.Count); - if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, errors.Count); } + int cnt = errors.Where(e => !e.IsAuxiliaryCexForDiagnosingTimeouts).Count(); + Interlocked.Add(ref stats.ErrorCount, cnt); + if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, cnt); } } break; } @@ -1599,6 +1661,10 @@ namespace Microsoft.Boogie errors.Sort(new CounterexampleComparer()); foreach (Counterexample error in errors) { + if (error.IsAuxiliaryCexForDiagnosingTimeouts) + { + continue; + } var errorInfo = CreateErrorInformation(error, outcome); errorInfo.ImplementationName = implName; diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index dfe32103..3159238c 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -172,48 +172,28 @@ namespace Microsoft.Boogie var vr = ExecutionEngine.Cache.Lookup(impl, out priority); if (vr != null && vr.ProgramId == programId) { - if (priority == Priority.LOW) - { + if (priority == Priority.LOW) { run.LowPriorityImplementationCount++; - if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) - { - SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr); - if (vr.ProgramId != null) - { - var p = ExecutionEngine.CachedProgram(vr.ProgramId); - if (p != null) - { - eai.Inject(impl, p); - run.TransformedImplementationCount++; - } - } - } - } - else if (priority == Priority.MEDIUM) - { + } else if (priority == Priority.MEDIUM) { run.MediumPriorityImplementationCount++; - if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) - { + } else if (priority == Priority.HIGH) { + run.HighPriorityImplementationCount++; + } else if (priority == Priority.SKIP) { + run.SkippedImplementationCount++; + } + + if (priority == Priority.LOW || priority == Priority.MEDIUM || 3 <= CommandLineOptions.Clo.VerifySnapshots) { + if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) { SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr); - if (vr.ProgramId != null) - { + if (vr.ProgramId != null) { var p = ExecutionEngine.CachedProgram(vr.ProgramId); - if (p != null) - { + if (p != null) { eai.Inject(impl, p); run.TransformedImplementationCount++; } } } } - else if (priority == Priority.HIGH) - { - run.HighPriorityImplementationCount++; - } - else if (priority == Priority.SKIP) - { - run.SkippedImplementationCount++; - } } } run.End = DateTime.UtcNow; diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index e93ecee9..300fbc10 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -86,6 +86,21 @@ namespace Microsoft.Boogie.SMTLib } } + public override void AssertNamed(VCExpr vc, bool polarity, string name) + { + string vcString; + if (polarity) + { + vcString = VCExpr2String(vc, 1); + } + else + { + vcString = "(not " + VCExpr2String(vc, 1) + ")"; + } + AssertAxioms(); + SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); + } + private void SetupAxiomBuilder(VCExpressionGenerator gen) { switch (CommandLineOptions.Clo.TypeEncodingMethod) @@ -246,9 +261,9 @@ namespace Microsoft.Boogie.SMTLib // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 ) - if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)) + if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))) { - SendThisVC("(set-option :produce-unsat-cores true)"); + SendCommon("(set-option :produce-unsat-cores true)"); this.usingUnsatCore = true; } @@ -401,6 +416,8 @@ namespace Microsoft.Boogie.SMTLib PrepareCommon(); + OptimizationRequests.Clear(); + string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; FlushAxioms(); @@ -408,7 +425,11 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(push 1)"); SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); + SendThisVC(vcString); + + SendOptimizationRequests(); + FlushLogFile(); if (Process != null) { @@ -418,10 +439,21 @@ namespace Microsoft.Boogie.SMTLib Process.Inspector.NewProblem(descriptiveName, vc, handler); } - SendThisVC("(check-sat)"); + SendCheckSat(); FlushLogFile(); } + private void SendOptimizationRequests() + { + if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count) + { + foreach (var r in OptimizationRequests) + { + SendThisVC(r); + } + } + } + public override void Reset(VCExpressionGenerator gen) { if (options.Solver == SolverKind.Z3) @@ -446,6 +478,7 @@ namespace Microsoft.Boogie.SMTLib if (options.Solver == SolverKind.Z3) { this.gen = gen; + SendThisVC("(reset)"); Namer.Reset(); common.Clear(); SetupAxiomBuilder(gen); @@ -456,6 +489,8 @@ namespace Microsoft.Boogie.SMTLib ctx.KnownDatatypeConstructors.Clear(); ctx.parent = this; DeclCollector.Reset(); + NamedAssumes.Clear(); + UsedNamedAssumes = null; SendThisVC("; did a full reset"); } } @@ -1264,6 +1299,38 @@ namespace Microsoft.Boogie.SMTLib result = GetResponse(); + var reporter = handler as VC.VCGen.ErrorReporter; + // TODO(wuestholz): Is the reporter ever null? + if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count) + { + if (usingUnsatCore) + { + UsedNamedAssumes = new HashSet<string>(); + SendThisVC("(get-unsat-core)"); + var resp = Process.GetProverResponse(); + if (resp.Name != "") + { + UsedNamedAssumes.Add(resp.Name); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length)); + } + } + foreach (var arg in resp.Arguments) + { + UsedNamedAssumes.Add(arg.Name); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length)); + } + } + } + else + { + UsedNamedAssumes = null; + } + } + if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut) { #region Run timeout diagnostics @@ -1423,13 +1490,13 @@ namespace Microsoft.Boogie.SMTLib expr = "false"; } SendThisVC("(assert " + expr + ")"); - SendThisVC("(check-sat)"); + SendCheckSat(); } else { string source = labels[labels.Length - 2]; string target = labels[labels.Length - 1]; SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))"); - SendThisVC("(check-sat)"); + SendCheckSat(); } } @@ -1474,7 +1541,7 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)"); } FlushLogFile(); - SendThisVC("(check-sat)"); + SendCheckSat(); queries++; return GetResponse(); } @@ -1812,6 +1879,7 @@ namespace Microsoft.Boogie.SMTLib private Model GetErrorModel() { if (!options.ExpectingModel()) return null; + SendThisVC("(get-model)"); Process.Ping(); Model theModel = null; @@ -1906,6 +1974,9 @@ namespace Microsoft.Boogie.SMTLib result = Outcome.Invalid; wasUnknown = true; break; + case "objectives": + // We ignore this. + break; default: HandleProverError("Unexpected prover response: " + resp.ToString()); break; @@ -1944,6 +2015,8 @@ namespace Microsoft.Boogie.SMTLib return result; } + readonly IList<string> OptimizationRequests = new List<string>(); + protected string VCExpr2String(VCExpr expr, int polarity) { Contract.Requires(expr != null); @@ -1983,10 +2056,8 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.Collect(sortedExpr); FeedTypeDeclsToProver(); - - - AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options)); - string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options); + AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, namedAssumes: NamedAssumes)); + string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, NamedAssumes, OptimizationRequests); Contract.Assert(res != null); if (CommandLineOptions.Clo.Trace) @@ -2094,19 +2165,20 @@ namespace Microsoft.Boogie.SMTLib throw new NotImplementedException(); } - public override void Assert(VCExpr vc, bool polarity) + public override void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1) { - string a = ""; - if (polarity) - { - a = "(assert " + VCExpr2String(vc, 1) + ")"; + OptimizationRequests.Clear(); + string assert = "assert"; + if (options.Solver == SolverKind.Z3 && isSoft) { + assert += "-soft"; } - else - { - a = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; + var expr = polarity ? VCExpr2String(vc, 1) : "(not\n" + VCExpr2String(vc, 1) + "\n)"; + if (options.Solver == SolverKind.Z3 && isSoft) { + expr += " :weight " + weight; } AssertAxioms(); - SendThisVC(a); + SendThisVC("(" + assert + " " + expr + ")"); + SendOptimizationRequests(); } public override void DefineMacro(Macro f, VCExpr vc) { @@ -2126,9 +2198,15 @@ namespace Microsoft.Boogie.SMTLib public override void Check() { PrepareCommon(); - SendThisVC("(check-sat)"); + SendCheckSat(); FlushLogFile(); } + + public void SendCheckSat() + { + UsedNamedAssumes = null; + SendThisVC("(check-sat)"); + } public override void SetTimeOut(int ms) { @@ -2325,21 +2403,6 @@ namespace Microsoft.Boogie.SMTLib return opts; } - public override void AssertNamed(VCExpr vc, bool polarity, string name) - { - string vcString; - if (polarity) - { - vcString = VCExpr2String(vc, 1); - } - else - { - vcString = "(not " + VCExpr2String(vc, 1) + ")"; - } - AssertAxioms(); - SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); - } - public override VCExpr ComputeInterpolant(VCExpr A, VCExpr B) { string A_str = VCExpr2String(A, 1); diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index dcf95bd2..06aa5bbe 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -34,14 +34,14 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> { - public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts) + public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null, ISet<VCExprVar> tryAssumes = null) { Contract.Requires(e != null); Contract.Requires(namer != null); Contract.Ensures(Contract.Result<string>() != null); StringWriter sw = new StringWriter(); - SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts); + SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, namedAssumes, optReqs); Contract.Assert(lin != null); lin.Linearise(e, LineariserOptions.Default); return cce.NonNull(sw.ToString()); @@ -74,12 +74,17 @@ namespace Microsoft.Boogie.SMTLib internal int UnderQuantifier = 0; internal readonly SMTLibProverOptions ProverOptions; - public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts) + readonly IList<string> OptimizationRequests; + readonly ISet<VCExprVar> NamedAssumes; + + public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null) { Contract.Requires(wr != null); Contract.Requires(namer != null); this.wr = wr; this.Namer = namer; this.ProverOptions = opts; + this.OptimizationRequests = optReqs; + this.NamedAssumes = namedAssumes; } public void Linearise(VCExpr expr, LineariserOptions options) @@ -263,6 +268,26 @@ namespace Microsoft.Boogie.SMTLib } return true; } + if (OptimizationRequests != null + && (node.Op.Equals(VCExpressionGenerator.MinimizeOp) || node.Op.Equals(VCExpressionGenerator.MaximizeOp))) + { + string optOp = node.Op.Equals(VCExpressionGenerator.MinimizeOp) ? "minimize" : "maximize"; + OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, NamedAssumes))); + Linearise(node[1], options); + return true; + } + if (node.Op is VCExprSoftOp) + { + Linearise(node[1], options); + return true; + } + if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) + { + var exprVar = node[0] as VCExprVar; + NamedAssumes.Add(exprVar); + Linearise(node[1], options); + return true; + } return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options); } diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 900bdbcc..f1179159 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -47,7 +47,7 @@ namespace Microsoft.Boogie.SMTLib "flet", "implies", "!=", "if_then_else", // Z3 extensions "lblneg", "lblpos", "lbl-lit", - "if", "&&", "||", "equals", "equiv", "bool", + "if", "&&", "||", "equals", "equiv", "bool", "minimize", "maximize", // Boogie-defined "real_pow", "UOrdering2", "UOrdering3", // Floating point (final draft SMTLIB-v2.5) diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 32e28560..eaed83e9 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -210,7 +210,18 @@ void ObjectInvariant() if (node.Op is VCExprStoreOp) RegisterStore(node); else if (node.Op is VCExprSelectOp) RegisterSelect(node); - else { + else if (node.Op is VCExprSoftOp) { + var exprVar = node[0] as VCExprVar; + AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); + AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp)node.Op).Weight)); + } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) { + var exprVar = node[0] as VCExprVar; + AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); + } + } else { VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp; if (op != null && !(op.Func is DatatypeConstructor) && !(op.Func is DatatypeMembership) && !(op.Func is DatatypeSelector) && @@ -255,7 +266,10 @@ void ObjectInvariant() RegisterType(node.Type); string decl = "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; - AddDeclaration(decl); + if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$"))) + { + AddDeclaration(decl); + } KnownVariables.Add(node); if(declHandler != null) declHandler.VarDecl(node); diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index 6077f327..dc9ad10f 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -1115,7 +1115,7 @@ namespace Microsoft.Boogie.TypeErasure if (typeVarBindings.Count < node.TypeParameters.Count) { foreach (TypeVariable/*!*/ var in node.TypeParameters) { Contract.Assert(var != null); - if (typeVarBindings.All(b => !b.V.Equals(var))) + if (typeVarBindings.All(b => !b.V.Equals(bindings.TypeVariableBindings[var]))) newBoundVars.Add((VCExprVar)bindings.TypeVariableBindings[var]); } } diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 0a9ba6b3..2c77a252 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -341,6 +341,10 @@ namespace Microsoft.Boogie { public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool); + public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool); + public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool); + public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool); + public VCExprOp BoogieFunctionOp(Function func) { Contract.Requires(func != null); Contract.Ensures(Contract.Result<VCExprOp>() != null); @@ -1565,6 +1569,16 @@ namespace Microsoft.Boogie.VCExprAST { } } + public class VCExprSoftOp : VCExprCustomOp + { + public readonly int Weight; + + public VCExprSoftOp(int weight) : base("soft##dummy", 2, Microsoft.Boogie.Type.Bool) + { + Weight = weight; + } + } + public class VCExprCustomOp : VCExprOp { public readonly string/*!*/ Name; int arity; diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 3c3b5cae..7bda0022 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -356,7 +356,7 @@ namespace Microsoft.Boogie { hasOutput = false; outputExn = null; this.handler = handler; - + thmProver.Reset(gen); SetTimeout(); proverStart = DateTime.UtcNow; @@ -386,6 +386,7 @@ namespace Microsoft.Boogie { // ----------------------------------------------------------------------------------------------- public abstract class ProverInterface { + public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) { Contract.Requires(prog != null); @@ -452,6 +453,10 @@ namespace Microsoft.Boogie { Undetermined, Bounded } + + public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>(); + public ISet<string> UsedNamedAssumes { get; protected set; } + public class ErrorHandler { // Used in CheckOutcomeCore public virtual int StartingProcId() @@ -542,7 +547,7 @@ namespace Microsoft.Boogie { } // (assert vc) - public virtual void Assert(VCExpr vc, bool polarity) + public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1) { throw new NotImplementedException(); } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 1f010757..19438924 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -85,6 +85,7 @@ namespace Microsoft.Boogie { public string RequestId; public abstract byte[] Checksum { get; } public byte[] SugaredCmdChecksum; + public bool IsAuxiliaryCexForDiagnosingTimeouts; public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples; @@ -313,7 +314,7 @@ namespace Microsoft.Boogie { public abstract int GetLocation(); } - public class CounterexampleComparer : IComparer<Counterexample> { + public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> { private int Compare(List<Block> bs1, List<Block> bs2) { @@ -375,6 +376,16 @@ namespace Microsoft.Boogie { } return -1; } + + public bool Equals(Counterexample x, Counterexample y) + { + return Compare(x, y) == 0; + } + + public int GetHashCode(Counterexample obj) + { + return 0; + } } public class AssertCounterexample : Counterexample { @@ -1122,7 +1133,8 @@ namespace VC { } if (returnBlocks > 1) { string unifiedExitLabel = "GeneratedUnifiedExit"; - Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken)); + Block unifiedExit; + unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); Contract.Assert(unifiedExit != null); foreach (Block b in impl.Blocks) { if (b.TransferCmd is ReturnCmd) { @@ -1528,6 +1540,26 @@ namespace VC { PredicateCmd pc = (PredicateCmd)c.Clone(); Contract.Assert(pc != null); + QKeyValue current = pc.Attributes; + while (current != null) + { + if (current.Key == "minimize" || current.Key == "maximize") { + Contract.Assume(current.Params.Count == 1); + var param = current.Params[0] as Expr; + Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv)); + current.ClearParams(); + current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param)); + } + if (current.Key == "verified_under") { + Contract.Assume(current.Params.Count == 1); + var param = current.Params[0] as Expr; + Contract.Assume(param != null && param.Type.IsBool); + current.ClearParams(); + current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param)); + } + current = current.Next; + } + Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr); if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) { string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState"); diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 0e598267..789f86f5 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -584,9 +584,6 @@ namespace VC { vcgen.ConvertCFG2DAG(impl); vcgen.PassifyImpl(impl, out mvInfo); - if (PassiveImplInstrumentation != null) - PassiveImplInstrumentation(impl); - VCExpressionGenerator gen = proverInterface.VCExprGen; var exprGen = proverInterface.Context.ExprGen; var translator = proverInterface.Context.BoogieExprTranslator; @@ -599,6 +596,9 @@ namespace VC { vcgen.InstrumentCallSites(impl); + if (PassiveImplInstrumentation != null) + PassiveImplInstrumentation(impl); + label2absy = new Dictionary<int, Absy>(); VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context); translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition); @@ -639,6 +639,7 @@ namespace VC { public abstract class StratifiedVCGenBase : VCGen { public readonly static string recordProcName = "boogie_si_record"; + public readonly static string callSiteVarAttr = "callSiteVar"; public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo; public ProverInterface prover; @@ -699,7 +700,9 @@ namespace VC { if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue; Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "SICS" + callSiteId, Microsoft.Boogie.Type.Bool)); implementation.LocVars.Add(callSiteVar); - newCmds.Add(new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar))); + var toInsert = new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar), + new QKeyValue(Token.NoToken, callSiteVarAttr, new List<object>(), null)); + newCmds.Add(toInsert); callSiteId++; } block.Cmds = newCmds; diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index bf25e042..6e43e917 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1519,7 +1519,7 @@ namespace VC { } } - public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) + public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); @@ -1527,10 +1527,10 @@ namespace VC { Contract.Ensures(Contract.Result<VCExpr>() != null); label2absy = new Dictionary<int, Absy>(); - return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext); + return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars); } - public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) { + public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); Contract.Ensures(Contract.Result<VCExpr>() != null); @@ -1632,7 +1632,7 @@ namespace VC { //use Duplicator and Substituter rather than new //nested IToken? //document expand attribute (search for {:ignore}, for example) - //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs + //fix up new CallCmd, new Requires, new Ensures in CivlRefinement.cs Func<Expr,Expr,Expr> withType = (Expr from, Expr to) => { NAryExpr nFrom = from as NAryExpr; @@ -1763,9 +1763,18 @@ namespace VC { { var checksum = a.Checksum; var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample; - if (oldCex != null) - { - callback.OnCounterexample(oldCex, null); + if (oldCex != null) { + if (CommandLineOptions.Clo.VerifySnapshots < 3) { + callback.OnCounterexample(oldCex, null); + } else { + // If possible, we use the old counterexample, but with the location information of "a" + var cex = AssertCmdToCloneCounterexample(a, oldCex); + callback.OnCounterexample(cex, null); + // OnCounterexample may have had side effects on the RequestId and OriginalRequestId fields. We make + // any such updates available in oldCex. (Is this really a good design? --KRML) + oldCex.RequestId = cex.RequestId; + oldCex.OriginalRequestId = cex.OriginalRequestId; + } } } } @@ -2012,6 +2021,16 @@ namespace VC { protected ProverContext/*!*/ context; Program/*!*/ program; + public IEnumerable<string> NecessaryAssumes + { + get { return program.NecessaryAssumes; } + } + + public void AddNecessaryAssume(string id) + { + program.NecessaryAssumes.Add(id); + } + public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins, Dictionary<int, Absy>/*!*/ label2absy, List<Block/*!*/>/*!*/ blocks, @@ -2104,6 +2123,7 @@ namespace VC { foreach (var cmd in assertCmds) { Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context); + cex.IsAuxiliaryCexForDiagnosingTimeouts = true; callback.OnCounterexample(cex, msg); } } @@ -2219,10 +2239,11 @@ namespace VC { impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }))); ResetPredecessors(impl.Blocks); - if(CommandLineOptions.Clo.KInductionDepth < 0) { + var k = Math.Max(CommandLineOptions.Clo.KInductionDepth, QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1)); + if(k < 0) { ConvertCFG2DAGStandard(impl, edgesCut, taskID); } else { - ConvertCFG2DAGKInduction(impl, edgesCut, taskID); + ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k); } #region Debug Tracing @@ -2487,14 +2508,12 @@ namespace VC { return referencedVars; } - private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID) { + private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID, int inductionK) { // K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses Contract.Requires(edgesCut == null); Contract.Requires(taskID == -1); - - int inductionK = CommandLineOptions.Clo.KInductionDepth; - Contract.Assume(inductionK >= 0); + Contract.Requires(0 <= inductionK); bool contRuleApplication = true; while (contRuleApplication) { @@ -2809,6 +2828,11 @@ namespace VC { mvInfo = new ModelViewInfo(program, impl); Convert2PassiveCmd(impl, mvInfo); + if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation")) + { + InstrumentWithMayUnverifiedConditions(impl, exitBlock); + } + #region Peep-hole optimizations if (CommandLineOptions.Clo.RemoveEmptyBlocks){ #region Get rid of empty blocks @@ -2844,6 +2868,190 @@ namespace VC { return gotoCmdOrigins; } + #region Simplified May-Unverified Analysis and Instrumentation + + static void InstrumentWithMayUnverifiedConditions(Implementation impl, Block unifiedExitBlock) + { + var q = new Queue<Block>(); + q.Enqueue(unifiedExitBlock); + var conditionOnBlockEntry = new Dictionary<Block, HashSet<Variable>>(); + while (q.Any()) + { + var block = q.Dequeue(); + + if (conditionOnBlockEntry.ContainsKey(block)) + { + continue; + } + + var gotoCmd = block.TransferCmd as GotoCmd; + if (gotoCmd != null && gotoCmd.labelTargets.Any(b => !conditionOnBlockEntry.ContainsKey(b))) + { + q.Enqueue(block); + continue; + } + + HashSet<Variable> cond = new HashSet<Variable>(); + if (gotoCmd != null) + { + var mayInstrs = new List<Block>(); + bool noInstr = true; + foreach (var succ in gotoCmd.labelTargets) + { + var c = conditionOnBlockEntry[succ]; + if (c != null) + { + mayInstrs.Add(succ); + } + else + { + noInstr = false; + } + cond = JoinVariableSets(cond, c); + } + if (!noInstr) + { + foreach (var instr in mayInstrs) + { + InstrumentWithCondition(instr, 0, conditionOnBlockEntry[instr]); + } + } + } + + for (int i = block.Cmds.Count - 1; 0 <= i; i--) + { + var cmd = block.Cmds[i]; + if (cond == null) { break; } + + var assertCmd = cmd as AssertCmd; + if (assertCmd != null) + { + var litExpr = assertCmd.Expr as LiteralExpr; + if (litExpr != null && litExpr.IsTrue) + { + continue; + } + + HashSet<Variable> vu = null; + if (assertCmd.VerifiedUnder == null) + { + vu = null; + } + else + { + HashSet<Variable> vars; + if (IsConjunctionOfAssumptionVariables(assertCmd.VerifiedUnder, out vars)) + { + vu = vars; + // TODO(wuestholz): Maybe drop the :verified_under attribute. + } + else + { + vu = null; + } + } + + if (vu == null) + { + InstrumentWithCondition(block, i + 1, cond); + } + + cond = JoinVariableSets(cond, vu); + } + } + + if (cond != null && block.Predecessors.Count == 0) + { + // TODO(wuestholz): Should we rather instrument each block? + InstrumentWithCondition(block, 0, cond); + } + + foreach (var pred in block.Predecessors) + { + q.Enqueue(pred); + } + + conditionOnBlockEntry[block] = cond; + } + } + + private static void InstrumentWithCondition(Block block, int idx, HashSet<Variable> condition) + { + var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr)new IdentifierExpr(Token.NoToken, v)).ToList()); + block.Cmds.Insert(idx, new AssumeCmd(Token.NoToken, Expr.Not(conj))); + } + + static HashSet<Variable> JoinVariableSets(HashSet<Variable> c0, HashSet<Variable> c1) + { + // We use the following lattice: + // - Top: null (i.e., true) + // - Bottom: new HashSet<Variable>() (i.e., false) + // - Other Elements: new HashSet<Variable>(...) (i.e., conjunctions of assumption variables) + + if (c0 == null || c1 == null) + { + return null; + } + var result = new HashSet<Variable>(c0); + result.UnionWith(c1); + return result; + } + + static bool IsAssumptionVariableOrIncarnation(Variable v) + { + if (QKeyValue.FindBoolAttribute(v.Attributes, "assumption")) { return true; } + var incar = v as Incarnation; + return incar == null || QKeyValue.FindBoolAttribute(incar.OriginalVariable.Attributes, "assumption"); + } + + static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet<Variable> variables) + { + Contract.Requires(expr != null); + + variables = null; + var litExpr = expr as LiteralExpr; + if (litExpr != null && (litExpr.IsFalse || litExpr.IsTrue)) + { + if (litExpr.IsTrue) + { + variables = new HashSet<Variable>(); + } + return true; + } + + var idExpr = expr as IdentifierExpr; + if (idExpr != null && IsAssumptionVariableOrIncarnation(idExpr.Decl)) + { + variables = new HashSet<Variable>(); + variables.Add(idExpr.Decl); + return true; + } + + var andExpr = expr as NAryExpr; + if (andExpr != null) + { + var fun = andExpr.Fun as BinaryOperator; + if (fun != null && fun.Op == BinaryOperator.Opcode.And && andExpr.Args != null) + { + bool res = true; + variables = new HashSet<Variable>(); + foreach (var op in andExpr.Args) + { + HashSet<Variable> vars; + var r = IsConjunctionOfAssumptionVariables(op, out vars); + res &= r; + variables = JoinVariableSets(variables, vars); + if (!res) { break; } + } + return res; + } + } + + return false; + } + + #endregion + private static void HandleSelectiveChecking(Implementation impl) { if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") || @@ -3137,6 +3345,31 @@ namespace VC { } } + /// <summary> + /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt". + /// </summary> + public static Counterexample AssertCmdToCloneCounterexample(AssertCmd assrt, Counterexample cex) { + Contract.Requires(assrt != null); + Contract.Requires(cex != null); + Contract.Ensures(Contract.Result<Counterexample>() != null); + + List<string> relatedInformation = new List<string>(); + + Counterexample cc; + if (assrt is AssertRequiresCmd) { + var aa = (AssertRequiresCmd)assrt; + cc = new CallCounterexample(cex.Trace, aa.Call, aa.Requires, cex.Model, cex.MvInfo, cex.Context, aa.Checksum); + } else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) { + var aa = (AssertEnsuresCmd)assrt; + var oldCex = (ReturnCounterexample)cex; + cc = new ReturnCounterexample(cex.Trace, oldCex.FailingReturn, aa.Ensures, cex.Model, cex.MvInfo, cex.Context, aa.Checksum); + } else { + cc = new AssertCounterexample(cex.Trace, assrt, cex.Model, cex.MvInfo, cex.Context); + } + cc.relatedInformation = relatedInformation; + return cc; + } + static VCExpr LetVC(Block startBlock, VCExpr controlFlowVariableExpr, Dictionary<int, Absy> label2absy, diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index b4ee4c09..cad5914b 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -87,7 +87,7 @@ namespace VC { /// <summary> /// Computes the wlp for an assert or assume command "cmd". /// </summary> - public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { + internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { Contract.Requires(cmd != null); Contract.Requires(N != null); Contract.Requires(ctxt != null); @@ -186,17 +186,48 @@ namespace VC { if (naryExpr.Fun is FunctionCall) { int id = ac.UniqueId; ctxt.Label2absy[id] = ac; - return gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N); + return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N)); } } } - return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N); + var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); + + var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); + if (aid != null) + { + var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); + var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool); + expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr)); + } + var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft"); + var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0); + if ((soft || 0 < softWeight) && aid != null) + { + var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool); + expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr)); + } + return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N)); } else { Console.WriteLine(cmd.ToString()); Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command } } - + + private static VCExpr MaybeWrapWithOptimization(VCContext ctxt, VCExpressionGenerator gen, QKeyValue attrs, VCExpr expr) + { + var min = QKeyValue.FindExprAttribute(attrs, "minimize"); + if (min != null) + { + expr = gen.Function(VCExpressionGenerator.MinimizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(min), expr); + } + var max = QKeyValue.FindExprAttribute(attrs, "maximize"); + if (max != null) + { + expr = gen.Function(VCExpressionGenerator.MaximizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(max), expr); + } + return expr; + } + public static CommandLineOptions.SubsumptionOption Subsumption(AssertCmd ac) { Contract.Requires(ac != null); int n = QKeyValue.FindIntAttribute(ac.Attributes, "subsumption", -1); diff --git a/Source/version.ssc b/Source/version.ssc deleted file mode 100644 index 5bdcf170..00000000 --- a/Source/version.ssc +++ /dev/null @@ -1,12 +0,0 @@ -// ==++== -// -// -// -// ==--== -// Warning: Automatically generated file. DO NOT EDIT -// Generated at Dienstag, 5. Juli 2011 11:26:45 - -using System.Reflection; -[assembly: AssemblyVersion("2.2.30705.1126")] -[assembly: AssemblyFileVersion("2.2.30705.1126")] - |