summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/AbsInt/IntervalDomain.cs8
-rw-r--r--Source/Concurrency/CivlRefinement.cs14
-rw-r--r--Source/Concurrency/CivlTypeChecker.cs219
-rw-r--r--Source/Core/Absy.cs28
-rw-r--r--Source/Core/AbsyCmd.cs18
-rw-r--r--Source/Core/AbsyQuant.cs27
-rw-r--r--Source/Core/CommandLineOptions.cs16
-rw-r--r--Source/Core/ResolutionContext.cs12
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs5
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs59
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs17
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs2
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs5
-rw-r--r--Source/VCExpr/VCExprAST.cs3
-rw-r--r--Source/VCGeneration/Check.cs8
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs23
-rw-r--r--Source/VCGeneration/VC.cs228
-rw-r--r--Source/VCGeneration/Wlp.cs36
-rw-r--r--Source/version.ssc12
19 files changed, 568 insertions, 172 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/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs
index dfe50ef9..75ff2358 100644
--- a/Source/Concurrency/CivlRefinement.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -315,19 +315,9 @@ namespace Microsoft.Boogie
foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys)
{
LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v];
- if (info.isGhost)
+ if (layerNum < info.layer)
{
- if (info.layer != layerNum)
- {
- availableVars.Remove(v);
- }
- }
- else
- {
- if (layerNum < info.layer)
- {
- availableVars.Remove(v);
- }
+ availableVars.Remove(v);
}
}
return availableVars;
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index 71feb927..b426d9ed 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -333,26 +333,24 @@ namespace Microsoft.Boogie
public class AtomicProcedureInfo
{
public bool isPure;
- public HashSet<int> layers;
+ public LayerRange layerRange;
public AtomicProcedureInfo()
{
this.isPure = true;
- this.layers = null;
+ this.layerRange = null;
}
- public AtomicProcedureInfo(HashSet<int> layers)
+ public AtomicProcedureInfo(LayerRange layerRange)
{
this.isPure = false;
- this.layers = layers;
+ this.layerRange = layerRange;
}
}
public class LocalVariableInfo
{
- public bool isGhost;
public int layer;
- public LocalVariableInfo(bool isGhost, int layer)
+ public LocalVariableInfo(int layer)
{
- this.isGhost = isGhost;
this.layer = layer;
}
}
@@ -364,7 +362,6 @@ namespace Microsoft.Boogie
Implementation enclosingImpl;
HashSet<Variable> sharedVarsAccessed;
int introducedLocalVarsUpperBound;
- int ghostVarIntroLayerAllowed;
public Program program;
public int errorCount;
@@ -373,28 +370,15 @@ namespace Microsoft.Boogie
public Dictionary<Procedure, AtomicProcedureInfo> procToAtomicProcedureInfo;
public Dictionary<Absy, HashSet<int>> absyToLayerNums;
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 (callCmd.Proc.Modifies.Count > 0)
- {
- return enclosingProcLayerNum == layerNum;
- }
- if (callCmd.Outs.Count == 0)
- {
- return true;
- }
- var outputVar = callCmd.Outs[0].Decl;
- var localVariableInfo = localVarToLocalVariableInfo[outputVar];
- if (localVariableInfo.isGhost)
- {
- return localVariableInfo.layer == layerNum;
- }
if (atomicProcedureInfo.isPure)
{
- return localVariableInfo.layer <= layerNum;
+ return pureCallLayer[callCmd] <= layerNum;
}
else
{
@@ -456,13 +440,13 @@ namespace Microsoft.Boogie
this.enclosingImpl = null;
this.sharedVarsAccessed = null;
this.introducedLocalVarsUpperBound = int.MinValue;
- this.ghostVarIntroLayerAllowed = 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.procToAtomicProcedureInfo = new Dictionary<Procedure, AtomicProcedureInfo>();
+ this.pureCallLayer = new Dictionary<CallCmd, int>();
foreach (var g in program.GlobalVariables)
{
@@ -553,27 +537,39 @@ namespace Microsoft.Boogie
foreach (var proc in program.Procedures)
{
if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
- var procLayerNums = RemoveDuplicatesAndSort(FindLayers(proc.Attributes));
+ 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;
}
- else if (globalVarToSharedVarInfo[ie.Decl].introLayerNum != procLayerNums[0])
- {
- Error(proc, "The introduction layer of a modified global variable must be identical to the layer of the atomic procedure");
- }
}
- if (proc.Modifies.Count == 0 || procLayerNums.Count == 1)
+ int lower, upper;
+ if (procLayerNums.Count == 1)
+ {
+ lower = procLayerNums[0];
+ upper = procLayerNums[0];
+ }
+ else if (procLayerNums.Count == 2)
{
- procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(new HashSet<int>(procLayerNums));
+ lower = procLayerNums[0];
+ upper = procLayerNums[1];
+ if (lower >= upper)
+ {
+ Error(proc, "Lower layer must be less than upper layer");
+ continue;
+ }
}
else
{
- Error(proc, "An atomic procedure with more than one layer must not modify a global variable");
+ 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;
@@ -592,7 +588,7 @@ namespace Microsoft.Boogie
this.sharedVarsAccessed = new HashSet<Variable>();
(new PurityChecker(this)).VisitImplementation(impl);
LayerRange upperBound = FindLayerRange();
- LayerRange lowerBound = new LayerRange(atomicProcedureInfo.layers);
+ LayerRange lowerBound = atomicProcedureInfo.layerRange;
if (!lowerBound.Subset(upperBound))
{
Error(impl, "Atomic procedure cannot access global variable");
@@ -695,14 +691,14 @@ namespace Microsoft.Boogie
Variable v = proc.InParams[i];
var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
if (layer == int.MinValue) continue;
- localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+ localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
}
for (int i = 0; i < proc.OutParams.Count; i++)
{
Variable v = proc.OutParams[i];
var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
if (layer == int.MinValue) continue;
- localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+ localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
}
}
foreach (Implementation node in program.Implementations)
@@ -712,21 +708,21 @@ namespace Microsoft.Boogie
{
var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum);
if (layer == int.MinValue) continue;
- localVarToLocalVariableInfo[v] = new LocalVariableInfo(QKeyValue.FindBoolAttribute(node.Attributes, "ghost"), layer);
+ localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
}
for (int i = 0; i < node.Proc.InParams.Count; i++)
{
Variable v = node.Proc.InParams[i];
if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
var layer = localVarToLocalVariableInfo[v].layer;
- localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(false, layer);
+ localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(layer);
}
for (int i = 0; i < node.Proc.OutParams.Count; i++)
{
Variable v = node.Proc.OutParams[i];
if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
var layer = localVarToLocalVariableInfo[v].layer;
- localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(false, layer);
+ localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(layer);
}
}
if (errorCount > 0) return;
@@ -818,13 +814,17 @@ namespace Microsoft.Boogie
}
for (int i = 0; i < node.Ins.Count; i++)
{
- var formal = node.Proc.InParams[i];
- if (localVarToLocalVariableInfo.ContainsKey(formal))
+ Visit(node.Ins[i]);
+ if (introducedLocalVarsUpperBound != int.MinValue)
{
- introducedLocalVarsUpperBound = localVarToLocalVariableInfo[formal].layer;
+ 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;
}
- Visit(node.Ins[i]);
- introducedLocalVarsUpperBound = int.MinValue;
}
for (int i = 0; i < node.Outs.Count; i++)
{
@@ -840,69 +840,83 @@ namespace Microsoft.Boogie
}
else if (procToAtomicProcedureInfo.ContainsKey(node.Proc))
{
- // 1. Outputs are either all ghost or all introduced.
- // 2. All outputs have the same layer; call it output layer.
- // 3. If callee is impure and has outputs, output layer is a member of layer set of callee.
- // 4. If callee is impure and has introduced outputs, then creation number of caller belongs to layer set of callee.
- // 5. If callee is impure and modifies globals, then creation number of caller belongs to layer set of callee.
-
- Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
- bool isGhost = false; // This assignment stops the compiler from complaining.
- // In the absence of errors, isGhost is initialized by loop below.
- foreach (var ie in node.Outs)
+ var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
+ if (atomicProcedureInfo.isPure)
{
- if (localVarToLocalVariableInfo.ContainsKey(ie.Decl))
+ if (node.Outs.Count > 0)
{
- var localVariableInfo = localVarToLocalVariableInfo[ie.Decl];
- if (introducedLocalVarsUpperBound == int.MinValue)
+ int inferredLayer = int.MinValue;
+ foreach (var ie in node.Outs)
{
- introducedLocalVarsUpperBound = localVariableInfo.layer;
- isGhost = localVariableInfo.isGhost;
- var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
- if (!atomicProcedureInfo.isPure)
+ if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) continue;
+ if (inferredLayer < localVarToLocalVariableInfo[ie.Decl].layer)
{
- if (!atomicProcedureInfo.layers.Contains(introducedLocalVarsUpperBound))
+ 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, "Layer of output variable must be a layer of the callee");
+ Error(node, "Output variable must be introduced");
}
- if (!isGhost && !atomicProcedureInfo.layers.Contains(enclosingProcLayerNum))
+ else if (inferredLayer != localVarToLocalVariableInfo[ie.Decl].layer)
{
- Error(node, "The creation layer of caller must be a layer of the callee");
+ Error(node, "All output variables must be introduced at the same layer");
}
}
}
- else
+ Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+ foreach (var e in node.Ins)
{
- if (localVariableInfo.layer != introducedLocalVarsUpperBound)
+ Visit(e);
+ if (inferredLayer < introducedLocalVarsUpperBound)
{
- Error(node, "All outputs must have the same layer");
- }
- if (localVariableInfo.isGhost != isGhost)
- {
- Error(node, "Outputs are either all ghost or all introduced");
+ Error(node, "An introduced local variable is not accessible");
}
+ introducedLocalVarsUpperBound = int.MinValue;
}
}
else
{
- Error(node, "Output variable must be a ghost or introduced local variable");
+ 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;
}
}
-
- if (node.Proc.Modifies.Count > 0)
+ else
{
- var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
- if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum))
+ if (enclosingProcLayerNum != atomicProcedureInfo.layerRange.upperLayerNum)
{
- Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee");
+ 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");
}
- introducedLocalVarsUpperBound = enclosingProcLayerNum;
- }
- foreach (var e in node.Ins)
- {
- Visit(e);
}
- introducedLocalVarsUpperBound = int.MinValue;
return node;
}
else
@@ -973,19 +987,9 @@ namespace Microsoft.Boogie
else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl))
{
var localVariableInfo = localVarToLocalVariableInfo[node.Decl];
- if (localVariableInfo.isGhost)
+ if (introducedLocalVarsUpperBound < localVariableInfo.layer)
{
- if (ghostVarIntroLayerAllowed != localVariableInfo.layer)
- {
- Error(node, "Ghost variable inaccessible");
- }
- }
- else
- {
- if (introducedLocalVarsUpperBound < localVariableInfo.layer)
- {
- Error(node, "Introduced variable inaccessible");
- }
+ introducedLocalVarsUpperBound = localVariableInfo.layer;
}
}
return base.VisitIdentifierExpr(node);
@@ -1003,9 +1007,12 @@ namespace Microsoft.Boogie
{
sharedVarsAccessed = new HashSet<Variable>();
Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
- introducedLocalVarsUpperBound = Least(FindLayers(ensures.Attributes));
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;
}
@@ -1016,9 +1023,12 @@ namespace Microsoft.Boogie
{
sharedVarsAccessed = new HashSet<Variable>();
Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
- introducedLocalVarsUpperBound = Least(FindLayers(requires.Attributes));
base.VisitRequires(requires);
CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);
+ if (introducedLocalVarsUpperBound > Least(FindLayers(requires.Attributes)))
+ {
+ Error(requires, "An introduced local variable is accessed but not available");
+ }
introducedLocalVarsUpperBound = int.MinValue;
sharedVarsAccessed = null;
return requires;
@@ -1033,16 +1043,13 @@ namespace Microsoft.Boogie
}
sharedVarsAccessed = new HashSet<Variable>();
Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
- var layerNums = FindLayers(node.Attributes);
- introducedLocalVarsUpperBound = Least(layerNums);
- if (layerNums.Count == 1)
- {
- ghostVarIntroLayerAllowed = layerNums[0];
- }
base.VisitAssertCmd(node);
CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);
+ if (introducedLocalVarsUpperBound > Least(FindLayers(node.Attributes)))
+ {
+ Error(node, "An introduced local variable is accessed but not available");
+ }
introducedLocalVarsUpperBound = int.MinValue;
- ghostVarIntroLayerAllowed = int.MinValue;
sharedVarsAccessed = null;
return node;
}
@@ -1115,7 +1122,7 @@ namespace Microsoft.Boogie
{
civlTypeChecker.Error(node, "Pure procedure can only call pure procedures");
}
- else if (!callerInfo.layers.IsSubsetOf(calleeInfo.layers))
+ else if (!callerInfo.layerRange.Subset(calleeInfo.layerRange))
{
civlTypeChecker.Error(node, "Caller layers must be subset of callee layers");
}
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c2e68002..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);
@@ -750,15 +752,28 @@ namespace Microsoft.Boogie {
Contract.Assert(block != null);
var auxCmd = block.TransferCmd as GotoCmd;
if (auxCmd == null) continue;
- foreach(var bl in auxCmd.labelTargets)
+ foreach (var bl in auxCmd.labelTargets)
{
if (loopBlocks.Contains(bl)) continue;
- immSuccBlks.Add(bl);
+ 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) {
@@ -975,10 +990,11 @@ namespace Microsoft.Boogie {
GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null &&
auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
- var blksThatBreakOut = GetBreakBlocksOfLoop(header, source, g);
- var loopNodes = g.NaturalLoops(header, source);
+ //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) {
- if (!loopNodes.Contains(bl)) {
+ 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;
//these blocks may have read/write locals that are not present in naturalLoops
@@ -2225,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,
@@ -2232,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 f4cba1dc..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;
@@ -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
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 9623139a..9bc855be 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1008,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();
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e93ecee9..7e98e8f8 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -246,9 +246,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 +401,8 @@ namespace Microsoft.Boogie.SMTLib
PrepareCommon();
+ OptimizationRequests.Clear();
+
string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
FlushAxioms();
@@ -408,7 +410,20 @@ namespace Microsoft.Boogie.SMTLib
SendThisVC("(push 1)");
SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
+
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null)
+ {
+ foreach (var v in NamedAssumeVars)
+ {
+ SendThisVC(string.Format("(declare-fun {0} () Bool)", v));
+ SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name));
+ }
+ }
+
SendThisVC(vcString);
+
+ SendOptimizationRequests();
+
FlushLogFile();
if (Process != null) {
@@ -422,6 +437,17 @@ namespace Microsoft.Boogie.SMTLib
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 +472,7 @@ namespace Microsoft.Boogie.SMTLib
if (options.Solver == SolverKind.Z3)
{
this.gen = gen;
+ SendThisVC("(reset)");
Namer.Reset();
common.Clear();
SetupAxiomBuilder(gen);
@@ -1264,6 +1291,22 @@ namespace Microsoft.Boogie.SMTLib
result = GetResponse();
+ var reporter = handler as VC.VCGen.ErrorReporter;
+ // TODO(wuestholz): Is the reporter ever null?
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null)
+ {
+ SendThisVC("(get-unsat-core)");
+ var resp = Process.GetProverResponse();
+ if (resp.Name != "")
+ {
+ reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+ }
+ foreach (var arg in resp.Arguments)
+ {
+ reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+ }
+ }
+
if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)
{
#region Run timeout diagnostics
@@ -1812,6 +1855,7 @@ namespace Microsoft.Boogie.SMTLib
private Model GetErrorModel() {
if (!options.ExpectingModel())
return null;
+
SendThisVC("(get-model)");
Process.Ping();
Model theModel = null;
@@ -1906,6 +1950,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 +1991,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 +2032,8 @@ namespace Microsoft.Boogie.SMTLib
DeclCollector.Collect(sortedExpr);
FeedTypeDeclsToProver();
-
-
AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));
- string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);
+ string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, OptimizationRequests);
Contract.Assert(res != null);
if (CommandLineOptions.Clo.Trace)
@@ -2096,6 +2143,7 @@ namespace Microsoft.Boogie.SMTLib
public override void Assert(VCExpr vc, bool polarity)
{
+ OptimizationRequests.Clear();
string a = "";
if (polarity)
{
@@ -2107,6 +2155,7 @@ namespace Microsoft.Boogie.SMTLib
}
AssertAxioms();
SendThisVC(a);
+ SendOptimizationRequests();
}
public override void DefineMacro(Macro f, VCExpr vc) {
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index dcf95bd2..de8798b8 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, IList<string> optReqs = 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, optReqs);
Contract.Assert(lin != null);
lin.Linearise(e, LineariserOptions.Default);
return cce.NonNull(sw.ToString());
@@ -74,12 +74,15 @@ namespace Microsoft.Boogie.SMTLib
internal int UnderQuantifier = 0;
internal readonly SMTLibProverOptions ProverOptions;
- public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts)
+ readonly IList<string> OptimizationRequests;
+
+ public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null)
{
Contract.Requires(wr != null); Contract.Requires(namer != null);
this.wr = wr;
this.Namer = namer;
this.ProverOptions = opts;
+ this.OptimizationRequests = optReqs;
}
public void Linearise(VCExpr expr, LineariserOptions options)
@@ -263,6 +266,14 @@ 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)));
+ 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..1c23c22f 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -255,7 +255,10 @@ void ObjectInvariant()
RegisterType(node.Type);
string decl =
"(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
- AddDeclaration(decl);
+ if (!printedName.StartsWith("assume$$"))
+ {
+ AddDeclaration(decl);
+ }
KnownVariables.Add(node);
if(declHandler != null)
declHandler.VarDecl(node);
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 0a9ba6b3..2fbb102c 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -341,6 +341,9 @@ 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 VCExprOp BoogieFunctionOp(Function func) {
Contract.Requires(func != null);
Contract.Ensures(Contract.Result<VCExprOp>() != null);
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3c3b5cae..8c1ae407 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -346,7 +346,7 @@ namespace Microsoft.Boogie {
}
}
- public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
+ public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList<VCExprVar> namedAssumeVars = null) {
Contract.Requires(descriptiveName != null);
Contract.Requires(vc != null);
Contract.Requires(handler != null);
@@ -356,10 +356,11 @@ namespace Microsoft.Boogie {
hasOutput = false;
outputExn = null;
this.handler = handler;
-
+
thmProver.Reset(gen);
SetTimeout();
proverStart = DateTime.UtcNow;
+ thmProver.NamedAssumeVars = namedAssumeVars;
thmProver.BeginCheck(descriptiveName, vc, handler);
// gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
@@ -386,6 +387,9 @@ namespace Microsoft.Boogie {
// -----------------------------------------------------------------------------------------------
public abstract class ProverInterface {
+
+ public IList<VCExprVar> NamedAssumeVars;
+
public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
Contract.Requires(prog != null);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index ae0a1147..19438924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1133,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) {
@@ -1539,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/VC.cs b/Source/VCGeneration/VC.cs
index 33e2f928..ad067c04 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1386,7 +1386,8 @@ namespace VC {
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
+ var namedAssumeVars = new List<VCExprVar>();
+ VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars);
Contract.Assert(vc != null);
if (!CommandLineOptions.Clo.UseLabels)
@@ -1414,7 +1415,7 @@ namespace VC {
string desc = cce.NonNull(impl.Name);
if (no >= 0)
desc += "_split" + no;
- checker.BeginCheck(desc, vc, reporter);
+ checker.BeginCheck(desc, vc, reporter, namedAssumeVars);
}
private void SoundnessCheck(HashSet<List<Block>/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {
@@ -1519,7 +1520,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 +1528,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);
@@ -1567,7 +1568,8 @@ namespace VC {
}
break;
case CommandLineOptions.VCVariety.DagIterative:
- vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
+ // TODO(wuestholz): Support named assume statements not just for this encoding.
+ vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars);
break;
case CommandLineOptions.VCVariety.Doomed:
vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);
@@ -2021,6 +2023,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,
@@ -2229,10 +2241,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
@@ -2497,14 +2510,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) {
@@ -2819,6 +2830,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
@@ -2854,6 +2870,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") ||
@@ -3193,7 +3393,7 @@ namespace VC {
Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount,
- bool isPositiveContext = true)
+ bool isPositiveContext = true, IList<VCExprVar> namedAssumeVars = null)
{
Contract.Requires(blocks != null);
Contract.Requires(proverCtxt != null);
@@ -3253,7 +3453,7 @@ namespace VC {
}
VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);
- VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+ VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars);
assertionCount += context.AssertionCount;
VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b4ee4c09..508a1400 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -48,7 +48,7 @@ namespace VC {
public class Wlp
{
- public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)
+ public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList<VCExprVar> namedAssumeVars = null)
//modifies ctxt.*;
{
Contract.Requires(b != null);
@@ -63,7 +63,7 @@ namespace VC {
for (int i = b.Cmds.Count; --i >= 0; )
{
- res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);
+ res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars);
}
int id = b.UniqueId;
@@ -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, IList<VCExprVar> namedAssumeVars = null) {
Contract.Requires(cmd != null);
Contract.Requires(N != null);
Contract.Requires(ctxt != null);
@@ -186,17 +186,41 @@ 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 (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null && namedAssumeVars != null)
+ {
+ var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool);
+ namedAssumeVars.Add(v);
+ expr = 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")]
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 19:56:36 +0000