diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-11-07 15:15:31 +0000 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-11-07 15:15:31 +0000 |
| commit | 762424bf2a12558fd5a1eacbc056ebff3193b318 (patch) | |
| tree | 88e3cd562f43ac07771d6b8c76f0c4613a3032b1 | |
| parent | 98791d48723b060293b0f0c376aec2fa242c67fe (diff) | |
| parent | 0c7c0b197f96d2ca8bd0b3c654dab783047ecb94 (diff) | |
Merge
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 7 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 8 | ||||
| -rw-r--r-- | Source/Core/Core.csproj | 1 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 6 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 18 | ||||
| -rw-r--r-- | Source/Core/MoverChecking.cs | 641 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 104 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 28 | ||||
| -rw-r--r-- | Source/Graph/Graph.cs | 32 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 169 | ||||
| -rw-r--r-- | Source/Predication/SmartBlockPredicator.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 3 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 516 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 2 | ||||
| -rw-r--r-- | Test/stratifiedinline/Answer | 11 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar12.bpl | 8 | ||||
| -rw-r--r-- | Test/stratifiedinline/bar13.bpl | 34 | ||||
| -rw-r--r-- | Test/stratifiedinline/runtest.bat | 6 |
18 files changed, 1078 insertions, 518 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 2c5e1d89..9afa4f45 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2142,6 +2142,13 @@ namespace Microsoft.Boogie { newBlockBody.Add(a);
}
}
+ else if (CommandLineOptions.Clo.StratifiedInlining > 0)
+ {
+ // inject free requires as assume statements at the call site
+ AssumeCmd/*!*/ a = new AssumeCmd(req.tok, Substituter.Apply(s, req.Condition));
+ Contract.Assert(a != null);
+ newBlockBody.Add(a);
+ }
}
if (hasWildcard) {
if (preConjunction == null) {
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 5c18ddfe..95b57a74 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -595,8 +595,6 @@ namespace Microsoft.Boogie { public int RecursionBound = 500;
public bool NonUniformUnfolding = false;
public string inferLeastForUnsat = null;
- public string CoverageReporterPath = null;
- public Process coverageReporter = null; // used internally for debugging
// Inference mode for fixed point engine
public enum FixedPointInferenceMode {
@@ -1118,12 +1116,6 @@ namespace Microsoft.Boogie { }
return true;
- case "coverageReporter":
- if (ps.ConfirmArgumentCount(1)) {
- CoverageReporterPath = args[ps.i];
- }
- return true;
-
case "stratifiedInlineOption":
if (ps.ConfirmArgumentCount(1)) {
StratifiedInliningOption = Int32.Parse(cce.NonNull(args[ps.i]));
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 6d5b7bd9..03eefccd 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -156,6 +156,7 @@ <Compile Include="AbsyQuant.cs" />
<Compile Include="AbsyType.cs" />
<Compile Include="BitvectorAnalysis.cs" />
+ <Compile Include="MoverChecking.cs" />
<Compile Include="InterProceduralReachabilityGraph.cs" />
<Compile Include="CommandLineOptions.cs" />
<Compile Include="DeadVarElim.cs" />
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index ef958fa6..402ea7dc 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -407,9 +407,9 @@ namespace Microsoft.Boogie { /// <summary>
/// Apply a substitution to an expression replacing "old" expressions.
/// Outside "old" expressions, the substitution "always" is applied; any variable not in
- /// domain(always) is not changed. Inside "old" expressions, apply map "oldExpr" to
- /// variables in domain(oldExpr), apply map "always" to variables in
- /// domain(always)-domain(oldExpr), and leave variable unchanged otherwise.
+ /// domain(always) is not changed. Inside "old" expressions, apply map "forOld" to
+ /// variables in domain(forOld), apply map "always" to variables in
+ /// domain(always)-domain(forOld), and leave variable unchanged otherwise.
/// </summary>
public static Expr ApplyReplacingOldExprs(Substitution always, Substitution forold, Expr expr) {
Contract.Requires(expr != null);
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 3a9de5fb..51f7f328 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -23,7 +23,7 @@ namespace Microsoft.Boogie }
}
- public class LinearTypechecker : StandardVisitor
+ public class LinearTypeChecker : StandardVisitor
{
public Program program;
public int errorCount;
@@ -35,7 +35,7 @@ namespace Microsoft.Boogie public Dictionary<Variable, string> globalVarToDomainName;
public Dictionary<string, LinearDomain> linearDomains;
- public LinearTypechecker(Program program)
+ public LinearTypeChecker(Program program)
{
this.program = program;
this.errorCount = 0;
@@ -416,7 +416,7 @@ namespace Microsoft.Boogie Formal f = new Formal(
Token.NoToken,
new TypedIdent(Token.NoToken,
- domainName + "_in",
+ "linear_" + domainName + "_in",
new MapType(Token.NoToken, new List<TypeVariable>(),
new List<Type> { domain.elementType }, Type.Bool)), true);
impl.InParams.Add(f);
@@ -545,7 +545,7 @@ namespace Microsoft.Boogie {
proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName])));
var domain = linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
proc.InParams.Add(f);
domainNameToOutputScope[domainName].Add(f);
proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName])));
@@ -621,7 +621,7 @@ namespace Microsoft.Boogie MapType mapTypeBool = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Bool);
MapType mapTypeInt = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Int);
- this.mapOrBool = new Function(Token.NoToken, domainName + "_linear_MapOr",
+ this.mapOrBool = new Function(Token.NoToken, "linear_" + domainName + "_MapOr",
new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) },
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
@@ -649,7 +649,7 @@ namespace Microsoft.Boogie axioms.Add(new Axiom(Token.NoToken, axiomExpr));
}
- this.mapImpBool = new Function(Token.NoToken, domainName + "_linear_MapImp",
+ this.mapImpBool = new Function(Token.NoToken, "linear_" + domainName + "_MapImp",
new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) },
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
@@ -677,7 +677,7 @@ namespace Microsoft.Boogie axioms.Add(new Axiom(Token.NoToken, axiomExpr));
}
- this.mapConstBool = new Function(Token.NoToken, domainName + "_linear_MapConstBool",
+ this.mapConstBool = new Function(Token.NoToken, "linear_" + domainName + "_MapConstBool",
new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true) },
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
if (CommandLineOptions.Clo.UseArrayTheory)
@@ -700,7 +700,7 @@ namespace Microsoft.Boogie axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr));
}
- this.mapEqInt = new Function(Token.NoToken, domainName + "_linear_MapEq",
+ this.mapEqInt = new Function(Token.NoToken, "linear_" + domainName + "_MapEq",
new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true) },
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
@@ -728,7 +728,7 @@ namespace Microsoft.Boogie axioms.Add(new Axiom(Token.NoToken, axiomExpr));
}
- this.mapConstInt = new Function(Token.NoToken, domainName + "_linear_MapConstInt",
+ this.mapConstInt = new Function(Token.NoToken, "linear_" + domainName + "_MapConstInt",
new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true) },
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));
if (CommandLineOptions.Clo.UseArrayTheory)
diff --git a/Source/Core/MoverChecking.cs b/Source/Core/MoverChecking.cs new file mode 100644 index 00000000..aeea3947 --- /dev/null +++ b/Source/Core/MoverChecking.cs @@ -0,0 +1,641 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie
+{
+ /*
+ * Typechecking rules:
+ * At most one atomic specification per procedure
+ * The gate of an atomic specification refers only to global and input variables
+ */
+ public class MoverChecking
+ {
+ HashSet<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;
+ HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;
+ HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;
+ LinearTypeChecker linearTypeChecker;
+ Program moverCheckerProgram;
+ private MoverChecking(LinearTypeChecker linearTypeChecker)
+ {
+ this.commutativityCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
+ this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
+ this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
+ this.linearTypeChecker = linearTypeChecker;
+ this.moverCheckerProgram = new Program();
+ foreach (Declaration decl in linearTypeChecker.program.TopLevelDeclarations)
+ {
+ if (decl is TypeCtorDecl || decl is TypeSynonymDecl || decl is Constant || decl is Function || decl is Axiom)
+ this.moverCheckerProgram.TopLevelDeclarations.Add(decl);
+ }
+ foreach (Variable v in linearTypeChecker.program.GlobalVariables())
+ {
+ this.moverCheckerProgram.TopLevelDeclarations.Add(v);
+ }
+ }
+ private sealed class MySubstituter : Duplicator
+ {
+ private readonly Substitution outsideOld;
+ private readonly Substitution insideOld;
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(insideOld != null);
+ }
+
+ public MySubstituter(Substitution outsideOld, Substitution insideOld)
+ : base()
+ {
+ Contract.Requires(outsideOld != null && insideOld != null);
+ this.outsideOld = outsideOld;
+ this.insideOld = insideOld;
+ }
+
+ private bool insideOldExpr = false;
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ Expr e = null;
+
+ if (insideOldExpr)
+ {
+ e = insideOld(node.Decl);
+ }
+ else
+ {
+ e = outsideOld(node.Decl);
+ }
+ return e == null ? base.VisitIdentifierExpr(node) : e;
+ }
+
+ public override Expr VisitOldExpr(OldExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ bool previouslyInOld = insideOldExpr;
+ insideOldExpr = true;
+ Expr tmp = (Expr)this.Visit(node.Expr);
+ OldExpr e = new OldExpr(node.tok, tmp);
+ insideOldExpr = previouslyInOld;
+ return e;
+ }
+ }
+
+ enum MoverType
+ {
+ Top,
+ Atomic,
+ Right,
+ Left,
+ Both
+ }
+
+ class ActionInfo
+ {
+ public Procedure proc;
+ public MoverType moverType;
+ public List<AssertCmd> thisGate;
+ public CodeExpr thisAction;
+ public List<Variable> thisInParams;
+ public List<Variable> thisOutParams;
+ public List<AssertCmd> thatGate;
+ public CodeExpr thatAction;
+ public List<Variable> thatInParams;
+ public List<Variable> thatOutParams;
+
+ public bool IsRightMover
+ {
+ get { return moverType == MoverType.Right || moverType == MoverType.Both; }
+ }
+
+ public bool IsLeftMover
+ {
+ get { return moverType == MoverType.Left || moverType == MoverType.Both; }
+ }
+
+ public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType)
+ {
+ this.proc = proc;
+ this.moverType = moverType;
+ this.thisGate = new List<AssertCmd>();
+ this.thisAction = codeExpr;
+ this.thisInParams = new List<Variable>();
+ this.thisOutParams = new List<Variable>();
+ this.thatGate = new List<AssertCmd>();
+ this.thatInParams = new List<Variable>();
+ this.thatOutParams = new List<Variable>();
+
+ var cmds = thisAction.Blocks[0].Cmds;
+ for (int i = 0; i < cmds.Count; i++)
+ {
+ AssertCmd assertCmd = cmds[i] as AssertCmd;
+ if (assertCmd == null) break;
+ thisGate.Add(assertCmd);
+ cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ foreach (Variable x in proc.InParams)
+ {
+ this.thisInParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);
+ this.thatInParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ foreach (Variable x in proc.OutParams)
+ {
+ this.thisOutParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ this.thatOutParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ List<Variable> otherLocVars = new List<Variable>();
+ foreach (Variable x in thisAction.LocVars)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ otherLocVars.Add(y);
+ }
+ Contract.Assume(proc.TypeParameters.Count == 0);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ foreach (AssertCmd assertCmd in thisGate)
+ {
+ thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
+ }
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> otherBlocks = new List<Block>();
+ foreach (Block block in thisAction.Blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(Substituter.Apply(subst, cmd));
+ }
+ Block otherBlock = new Block();
+ otherBlock.Cmds = otherCmds;
+ otherBlock.Label = "that_" + block.Label;
+ block.Label = "this_" + block.Label;
+ otherBlocks.Add(otherBlock);
+ blockMap[block] = otherBlock;
+ if (block.TransferCmd is GotoCmd)
+ {
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ for (int i = 0; i < gotoCmd.labelNames.Count; i++)
+ {
+ gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
+ }
+ }
+ }
+ foreach (Block block in thisAction.Blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);
+ continue;
+ }
+ List<Block> otherGotoCmdLabelTargets = new List<Block>();
+ List<string> otherGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ otherGotoCmdLabelTargets.Add(blockMap[target]);
+ otherGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+ }
+ this.thatAction = new CodeExpr(otherLocVars, otherBlocks);
+ }
+ }
+
+ public static void AddCheckers(LinearTypeChecker linearTypeChecker)
+ {
+ Program program = linearTypeChecker.program;
+ List<ActionInfo> gatedActions = new List<ActionInfo>();
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ foreach (Ensures e in proc.Ensures)
+ {
+ MoverType moverType = GetMoverType(e);
+ if (moverType == MoverType.Top) continue;
+ CodeExpr codeExpr = e.Condition as CodeExpr;
+ if (codeExpr == null)
+ {
+ Console.WriteLine("Warning: an atomic action must be a CodeExpr");
+ continue;
+ }
+ ActionInfo info = new ActionInfo(proc, codeExpr, moverType);
+ gatedActions.Add(info);
+ }
+ }
+ if (gatedActions.Count == 0)
+ return;
+ MoverChecking moverChecking = new MoverChecking(linearTypeChecker);
+ foreach (ActionInfo first in gatedActions)
+ {
+ Debug.Assert(first.moverType != MoverType.Top);
+ if (first.moverType == MoverType.Atomic)
+ continue;
+ foreach (ActionInfo second in gatedActions)
+ {
+ if (first.IsRightMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, first, second);
+ moverChecking.CreateGatePreservationChecker(program, second, first);
+ }
+ if (first.IsLeftMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, second, first);
+ moverChecking.CreateGatePreservationChecker(program, first, second);
+ moverChecking.CreateFailurePreservationChecker(program, second, first);
+ }
+ }
+ }
+ var eraser = new LinearEraser();
+ eraser.VisitProgram(moverChecking.moverCheckerProgram);
+ {
+ int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ CommandLineOptions.Clo.PrintUnstructured = 1;
+ using (TokenTextWriter writer = new TokenTextWriter("MoverChecker.bpl", false))
+ {
+ if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never)
+ {
+ writer.WriteLine("// " + CommandLineOptions.Clo.Version);
+ writer.WriteLine("// " + CommandLineOptions.Clo.Environment);
+ }
+ writer.WriteLine();
+ moverChecking.moverCheckerProgram.Emit(writer);
+ }
+ CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
+ }
+
+ private static MoverType GetMoverType(Ensures e)
+ {
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
+ return MoverType.Atomic;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
+ return MoverType.Right;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
+ return MoverType.Left;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
+ return MoverType.Both;
+ else
+ return MoverType.Top;
+ }
+
+ class TransitionRelationComputation
+ {
+ private Program program;
+ private ActionInfo first;
+ private ActionInfo second;
+ private Stack<Block> dfsStack;
+ private Expr transitionRelation;
+
+ public TransitionRelationComputation(Program program, ActionInfo second)
+ {
+ this.program = program;
+ this.first = null;
+ this.second = second;
+ this.dfsStack = new Stack<Block>();
+ this.transitionRelation = Expr.False;
+ }
+
+ public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)
+ {
+ this.program = program;
+ this.first = first;
+ this.second = second;
+ this.dfsStack = new Stack<Block>();
+ this.transitionRelation = Expr.False;
+ }
+
+ public Expr Compute()
+ {
+ Search(second.thatAction.Blocks[0], false);
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ List<Variable> boundVars = new List<Variable>();
+ if (first != null)
+ {
+ foreach (Variable v in first.thisAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ boundVars.Add(bv);
+ }
+ }
+ foreach (Variable v in second.thatAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ boundVars.Add(bv);
+ }
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ if (boundVars.Count > 0)
+ return new ExistsExpr(Token.NoToken, boundVars, Substituter.Apply(subst, transitionRelation));
+ else
+ return transitionRelation;
+ }
+
+ private Expr CalculatePathCondition()
+ {
+ Expr returnExpr = Expr.True;
+ foreach (Variable v in program.GlobalVariables())
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ if (first != null)
+ {
+ foreach (Variable v in first.thisOutParams)
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ }
+ foreach (Variable v in second.thatOutParams)
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ Block[] dfsStackAsArray = dfsStack.Reverse().ToArray();
+ for (int i = dfsStackAsArray.Length - 1; i >= 0; i--)
+ {
+ Block b = dfsStackAsArray[i];
+ for (int j = b.Cmds.Count - 1; j >= 0; j--)
+ {
+ Cmd cmd = b.Cmds[j];
+ if (cmd is AssumeCmd)
+ {
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);
+ }
+ else if (cmd is AssignCmd)
+ {
+ AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd;
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ for (int k = 0; k < assignCmd.Lhss.Count; k++)
+ {
+ map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];
+ }
+ Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);
+ returnExpr = (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr);
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ }
+ }
+ return returnExpr;
+ }
+
+ private void Search(Block b, bool inFirst)
+ {
+ dfsStack.Push(b);
+ if (b.TransferCmd is ReturnExprCmd)
+ {
+ if (first == null || inFirst)
+ {
+ transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition());
+ }
+ else
+ {
+ Search(first.thisAction.Blocks[0], true);
+ }
+ }
+ else
+ {
+ GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ Search(target, inFirst);
+ }
+ }
+ dfsStack.Pop();
+ }
+ }
+
+ private static List<Block> CloneBlocks(List<Block> blocks)
+ {
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> otherBlocks = new List<Block>();
+ foreach (Block block in blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(cmd);
+ }
+ Block otherBlock = new Block();
+ otherBlock.Cmds = otherCmds;
+ otherBlock.Label = block.Label;
+ otherBlocks.Add(otherBlock);
+ blockMap[block] = otherBlock;
+ }
+ foreach (Block block in blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
+ continue;
+ }
+ List<Block> otherGotoCmdLabelTargets = new List<Block>();
+ List<string> otherGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ otherGotoCmdLabelTargets.Add(blockMap[target]);
+ otherGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+ }
+ return otherBlocks;
+ }
+
+ private List<Requires> DisjointnessRequires(Program program, ActionInfo first, ActionInfo second)
+ {
+ List<Requires> requires = new List<Requires>();
+ Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ domainNameToScope[domainName] = new HashSet<Variable>();
+ }
+ foreach (Variable v in program.GlobalVariables())
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ foreach (Variable v in first.thisInParams)
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ for (int i = 0; i < second.thatInParams.Count; i++)
+ {
+ var domainName = linearTypeChecker.FindDomainName(second.thisInParams[i]);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(second.thatInParams[i]);
+ }
+ foreach (string domainName in domainNameToScope.Keys)
+ {
+ requires.Add(new Requires(false, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ return requires;
+ }
+
+ private void CreateCommutativityChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (commutativityCheckerCache.Contains(actionPair))
+ return;
+ commutativityCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+ List<Variable> outputs = new List<Variable>();
+ outputs.AddRange(first.thisOutParams);
+ outputs.AddRange(second.thatOutParams);
+ List<Variable> locals = new List<Variable>();
+ locals.AddRange(first.thisAction.LocVars);
+ locals.AddRange(second.thatAction.LocVars);
+ List<Block> firstBlocks = CloneBlocks(first.thisAction.Blocks);
+ List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);
+ foreach (Block b in firstBlocks)
+ {
+ if (b.TransferCmd is ReturnCmd)
+ {
+ List<Block> bs = new List<Block>();
+ bs.Add(secondBlocks[0]);
+ List<string> ls = new List<string>();
+ ls.Add(secondBlocks[0].Label);
+ b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs);
+ }
+ }
+ List<Block> blocks = new List<Block>();
+ blocks.AddRange(firstBlocks);
+ blocks.AddRange(secondBlocks);
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ List<Ensures> ensures = new List<Ensures>();
+ Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).Compute();
+ ensures.Add(new Ensures(false, transitionRelation));
+ string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);
+ Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);
+ impl.Proc = proc;
+ this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
+ this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
+ }
+
+ private void CreateGatePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (gatePreservationCheckerCache.Contains(actionPair))
+ return;
+ gatePreservationCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+ List<Variable> outputs = new List<Variable>();
+ outputs.AddRange(first.thisOutParams);
+ outputs.AddRange(second.thatOutParams);
+ List<Variable> locals = new List<Variable>();
+ locals.AddRange(second.thatAction.LocVars);
+ List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ List<Ensures> ensures = new List<Ensures>();
+ foreach (AssertCmd assertCmd in first.thisGate)
+ {
+ requires.Add(new Requires(false, assertCmd.Expr));
+ ensures.Add(new Ensures(false, assertCmd.Expr));
+ }
+ string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);
+ Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
+ impl.Proc = proc;
+ this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
+ this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
+ }
+
+ private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (failurePreservationCheckerCache.Contains(actionPair))
+ return;
+ failurePreservationCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+
+ Expr transitionRelation = (new TransitionRelationComputation(program, second)).Compute();
+ Expr expr = Expr.True;
+ foreach (AssertCmd assertCmd in first.thisGate)
+ {
+ expr = Expr.And(assertCmd.Expr, expr);
+ }
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ requires.Add(new Requires(false, Expr.Not(expr)));
+ foreach (AssertCmd assertCmd in second.thatGate)
+ {
+ requires.Add(new Requires(false, assertCmd.Expr));
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> oldMap = new Dictionary<Variable, Expr>();
+ List<Variable> boundVars = new List<Variable>();
+ foreach (Variable v in program.GlobalVariables())
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ foreach (Variable v in second.thatOutParams)
+ {
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ oldMap[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ }
+ foreach (Variable v in second.thatAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ oldMap[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+
+ Expr ensuresExpr = Expr.And(transitionRelation, Expr.Not(expr));
+ if (boundVars.Count > 0)
+ {
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);
+ ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, (Expr)new MySubstituter(subst, oldSubst).Visit(ensuresExpr));
+ }
+ List<Ensures> ensures = new List<Ensures>();
+ ensures.Add(new Ensures(false, ensuresExpr));
+ List<Block> blocks = new List<Block>();
+ blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
+ string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, new List<IdentifierExpr>(), ensures);
+ Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
+ impl.Proc = proc;
+ this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
+ this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
+ }
+ }
+}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index dd6276c2..4f0c7a4b 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -13,16 +13,16 @@ namespace Microsoft.Boogie public class OwickiGriesTransform
{
List<IdentifierExpr> globalMods;
- LinearTypechecker linearTypechecker;
+ LinearTypeChecker linearTypeChecker;
Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
List<Procedure> yieldCheckerProcs;
List<Implementation> yieldCheckerImpls;
Procedure yieldProc;
- public OwickiGriesTransform(LinearTypechecker linearTypechecker)
+ public OwickiGriesTransform(LinearTypeChecker linearTypeChecker)
{
- this.linearTypechecker = linearTypechecker;
- Program program = linearTypechecker.program;
+ this.linearTypeChecker = linearTypeChecker;
+ Program program = linearTypeChecker.program;
globalMods = new List<IdentifierExpr>();
foreach (Variable g in program.GlobalVariables())
{
@@ -37,7 +37,7 @@ namespace Microsoft.Boogie private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
{
List<Expr> exprSeq = new List<Expr>();
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
}
@@ -48,10 +48,10 @@ namespace Microsoft.Boogie if (yieldProc == null)
{
List<Variable> inputs = new List<Variable>();
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
- var domain = linearTypechecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+ var domain = linearTypeChecker.linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
inputs.Add(f);
}
foreach (IdentifierExpr ie in globalMods)
@@ -70,7 +70,7 @@ namespace Microsoft.Boogie private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)
{
Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
- foreach (var domainName in linearTypechecker.linearDomains.Keys)
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
{
var expr = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
expr.Resolve(new ResolutionContext(null));
@@ -79,10 +79,10 @@ namespace Microsoft.Boogie }
foreach (Variable v in availableLinearVars)
{
- var domainName = linearTypechecker.FindDomainName(v);
- var domain = linearTypechecker.linearDomains[domainName];
+ var domainName = linearTypeChecker.FindDomainName(v);
+ var domain = linearTypeChecker.linearDomains[domainName];
IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
- var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName] });
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] });
expr.Resolve(new ResolutionContext(null));
expr.Typecheck(new TypecheckingContext(null));
domainNameToExpr[domainName] = expr;
@@ -94,7 +94,7 @@ namespace Microsoft.Boogie {
List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
- foreach (var domainName in linearTypechecker.linearDomains.Keys)
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
{
lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName])));
rhss.Add(domainNameToExpr[domainName]);
@@ -118,7 +118,7 @@ namespace Microsoft.Boogie {
newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
}
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[yieldCmd], domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[yieldCmd], domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
for (int j = 0; j < cmds.Count; j++)
@@ -194,14 +194,14 @@ namespace Microsoft.Boogie {
if (yields.Count == 0) return;
- Program program = linearTypechecker.program;
+ Program program = linearTypeChecker.program;
List<Variable> locals = new List<Variable>();
List<Variable> inputs = new List<Variable>();
foreach (IdentifierExpr ie in map.Values)
{
locals.Add(ie.Decl);
}
- for (int i = 0; i < decl.InParams.Count - linearTypechecker.linearDomains.Count; i++)
+ for (int i = 0; i < decl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
{
Variable inParam = decl.InParams[i];
Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
@@ -209,8 +209,8 @@ namespace Microsoft.Boogie map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);
}
{
- int i = decl.InParams.Count - linearTypechecker.linearDomains.Count;
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ int i = decl.InParams.Count - linearTypeChecker.linearDomains.Count;
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
Variable inParam = decl.InParams[i];
Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
@@ -252,7 +252,7 @@ namespace Microsoft.Boogie int yieldCount = 0;
foreach (List<Cmd> cs in yields)
{
- var linearDomains = linearTypechecker.linearDomains;
+ var linearDomains = linearTypeChecker.linearDomains;
List<Cmd> newCmds = new List<Cmd>();
foreach (Cmd cmd in cs)
{
@@ -342,7 +342,7 @@ namespace Microsoft.Boogie }
}
- Program program = linearTypechecker.program;
+ Program program = linearTypeChecker.program;
Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
foreach (Variable local in impl.LocVars)
{
@@ -360,8 +360,8 @@ namespace Microsoft.Boogie Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
Dictionary<string, Variable> domainNameToLocalVar = new Dictionary<string, Variable>();
{
- int i = impl.InParams.Count - linearTypechecker.linearDomains.Count;
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
Variable inParam = impl.InParams[i];
domainNameToInputVar[domainName] = inParam;
@@ -440,10 +440,10 @@ namespace Microsoft.Boogie if (callCmd.InParallelWith != null || callCmd.IsAsync ||
QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
{
- HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypechecker.availableLinearVars[callCmd]);
+ HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypeChecker.availableLinearVars[callCmd]);
foreach (IdentifierExpr ie in callCmd.Outs)
{
- if (linearTypechecker.FindDomainName(ie.Decl) == null) continue;
+ if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue;
availableLinearVars.Add(ie.Decl);
}
Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
@@ -473,14 +473,14 @@ namespace Microsoft.Boogie foreach (Block header in yieldingHeaders)
{
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[header], domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[header], domainNameToInputVar);
foreach (Block pred in header.Predecessors)
{
AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
}
List<Cmd> newCmds = new List<Cmd>();
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
}
@@ -497,20 +497,20 @@ namespace Microsoft.Boogie List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
- foreach (var domainName in linearTypechecker.linearDomains.Keys)
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
{
domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
}
- for (int i = 0; i < impl.InParams.Count - linearTypechecker.linearDomains.Count; i++)
+ for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
{
Variable v = impl.InParams[i];
- var domainName = linearTypechecker.FindDomainName(v);
+ var domainName = linearTypeChecker.FindDomainName(v);
if (domainName == null) continue;
- var domain = linearTypechecker.linearDomains[domainName];
+ var domain = linearTypeChecker.linearDomains[domainName];
IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
- domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName] });
+ domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] });
}
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName])));
rhss.Add(domainNameToExpr[domainName]);
@@ -534,11 +534,11 @@ namespace Microsoft.Boogie {
if (!QKeyValue.FindBoolAttribute(proc.Attributes, "stable")) return;
- Program program = linearTypechecker.program;
+ Program program = linearTypeChecker.program;
Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
{
- int i = proc.InParams.Count - linearTypechecker.linearDomains.Count;
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count;
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
Variable inParam = proc.InParams[i];
domainNameToInputVar[domainName] = inParam;
@@ -552,27 +552,27 @@ namespace Microsoft.Boogie if (proc.Requires.Count > 0)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearTypechecker.linearDomains.Keys)
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
{
domainNameToScope[domainName] = new HashSet<Variable>();
domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);
}
foreach (Variable v in program.GlobalVariables())
{
- var domainName = linearTypechecker.FindDomainName(v);
+ var domainName = linearTypeChecker.FindDomainName(v);
if (domainName == null) continue;
domainNameToScope[domainName].Add(v);
}
- for (int i = 0; i < proc.InParams.Count - linearTypechecker.linearDomains.Count; i++)
+ for (int i = 0; i < proc.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
{
Variable v = proc.InParams[i];
- var domainName = linearTypechecker.FindDomainName(v);
+ var domainName = linearTypeChecker.FindDomainName(v);
if (domainName == null) continue;
domainNameToScope[domainName].Add(v);
}
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
- cmds.Add(new AssumeCmd(Token.NoToken, linearTypechecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
}
foreach (Requires r in proc.Requires)
{
@@ -591,27 +591,27 @@ namespace Microsoft.Boogie if (proc.Ensures.Count > 0)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearTypechecker.linearDomains.Keys)
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
{
domainNameToScope[domainName] = new HashSet<Variable>();
domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);
}
foreach (Variable v in program.GlobalVariables())
{
- var domainName = linearTypechecker.FindDomainName(v);
+ var domainName = linearTypeChecker.FindDomainName(v);
if (domainName == null) continue;
domainNameToScope[domainName].Add(v);
}
for (int i = 0; i < proc.OutParams.Count; i++)
{
Variable v = proc.OutParams[i];
- var domainName = linearTypechecker.FindDomainName(v);
+ var domainName = linearTypeChecker.FindDomainName(v);
if (domainName == null) continue;
domainNameToScope[domainName].Add(v);
}
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
- cmds.Add(new AssumeCmd(Token.NoToken, linearTypechecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
}
foreach (Ensures e in proc.Ensures)
{
@@ -634,12 +634,12 @@ namespace Microsoft.Boogie {
if (yieldProc == null) return;
- Program program = linearTypechecker.program;
+ Program program = linearTypeChecker.program;
List<Variable> inputs = new List<Variable>();
- foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
- var domain = linearTypechecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+ var domain = linearTypeChecker.linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
inputs.Add(f);
}
foreach (IdentifierExpr ie in globalMods)
@@ -689,7 +689,9 @@ namespace Microsoft.Boogie public void Transform()
{
- Program program = linearTypechecker.program;
+ MoverChecking.AddCheckers(linearTypeChecker);
+
+ Program program = linearTypeChecker.program;
foreach (var decl in program.TopLevelDeclarations)
{
Implementation impl = decl as Implementation;
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 92cc7429..80114fda 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -419,8 +419,8 @@ namespace Microsoft.Boogie PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
}
- LinearTypechecker linearTypechecker;
- PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypechecker);
+ LinearTypeChecker linearTypeChecker;
+ PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker);
if (oc != PipelineOutcome.ResolvedAndTypeChecked)
return;
@@ -443,11 +443,9 @@ namespace Microsoft.Boogie }
}
- EliminateDeadVariablesAndInline(program);
-
if (CommandLineOptions.Clo.StratifiedInlining == 0)
{
- OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypechecker);
+ OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypeChecker);
ogTransform.Transform();
var eraser = new LinearEraser();
eraser.VisitProgram(program);
@@ -460,6 +458,8 @@ namespace Microsoft.Boogie }
}
+ EliminateDeadVariablesAndInline(program);
+
var stats = new PipelineStatistics();
oc = InferAndVerify(program, stats);
switch (oc)
@@ -576,12 +576,12 @@ 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)
+ public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker)
{
Contract.Requires(program != null);
Contract.Requires(bplFileName != null);
- linearTypechecker = null;
+ linearTypeChecker = null;
// ---------- Resolve ------------------------------------------------------------
@@ -611,15 +611,15 @@ namespace Microsoft.Boogie return PipelineOutcome.TypeCheckingError;
}
- linearTypechecker = new LinearTypechecker(program);
- linearTypechecker.Typecheck();
- if (linearTypechecker.errorCount == 0)
+ linearTypeChecker = new LinearTypeChecker(program);
+ linearTypeChecker.Typecheck();
+ if (linearTypeChecker.errorCount == 0)
{
- linearTypechecker.Transform();
+ linearTypeChecker.Transform();
}
else
{
- Console.WriteLine("{0} type checking errors detected in {1}", linearTypechecker.errorCount, bplFileName);
+ Console.WriteLine("{0} type checking errors detected in {1}", linearTypeChecker.errorCount, bplFileName);
return PipelineOutcome.TypeCheckingError;
}
@@ -1142,8 +1142,8 @@ namespace Microsoft.Boogie private static Program ProgramFromFile(string filename) {
Program p = ParseBoogieProgram(new List<string> { filename }, false);
System.Diagnostics.Debug.Assert(p != null);
- LinearTypechecker linearTypechecker;
- PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypechecker);
+ LinearTypeChecker linearTypeChecker;
+ PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker);
System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
return p;
}
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 4a78c27f..8e5479e3 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -956,8 +956,12 @@ namespace Microsoft.Boogie.GraphUtil { }
var successors = new List<int>[n];
+ var predecessors = new List<int>[n];
int[] incomingEdges = new int[n];
+ for (int i = 0; i < n; i++)
+ predecessors[i] = new List<int>();
+
foreach (var e in g.Edges)
{
Contract.Assert(e.Item1 != null);
@@ -970,33 +974,47 @@ namespace Microsoft.Boogie.GraphUtil { successors[source].Add(target);
incomingEdges[target]++;
}
+ predecessors[target].Add(source);
}
var sortedNodes = new List<Tuple<Node, bool>>();
+ var sortedNodesInternal = new List<int>();
var regionStack = new Stack<Tuple<Node, List<int>>>();
regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
while (regionStack.Count != 0)
{
- int rootIndex = -1;
+ var rootIndexes = new List<int>();
foreach (var i in regionStack.Peek().Item2)
{
if (incomingEdges[i] == 0)
- {
- rootIndex = i;
- break;
- }
+ rootIndexes.Add(i);
}
- if (rootIndex == -1)
+ if (rootIndexes.Count() == 0)
{
var region = regionStack.Pop();
- if (regionStack.Count != 0)
+ if (regionStack.Count != 0) {
sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
+ sortedNodesInternal.Add(nodeToNumber[region.Item1]);
+ }
continue;
}
+ int rootIndex = rootIndexes[0];
+ int maxPredIndex = -1;
+ foreach (var i in rootIndexes) {
+ foreach (var p in predecessors[i]) {
+ int predIndex =
+ sortedNodesInternal.FindLastIndex(x => x == p);
+ if (predIndex > maxPredIndex) {
+ rootIndex = i;
+ maxPredIndex = predIndex;
+ }
+ }
+ }
incomingEdges[rootIndex] = -1;
sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
+ sortedNodesInternal.Add(rootIndex);
if (successors[rootIndex] != null)
foreach (int s in successors[rootIndex])
incomingEdges[s]--;
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 7acd2f6f..ac5ba95f 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -99,7 +99,7 @@ namespace Microsoft.Boogie.Houdini { Inline();
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
- this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
+ this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
this.proverTime = TimeSpan.Zero;
this.numProverQueries = 0;
@@ -219,7 +219,17 @@ namespace Microsoft.Boogie.Houdini { Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString());
if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
- return new VCGenOutcome(proverOutcome, new List<Counterexample>());
+ {
+ // pick some function; make it true and keep going
+ bool changed = false;
+ foreach (var f in impl2functionsAsserted[impl])
+ {
+ function2Value[f] = function2Value[f].MakeTop(out changed);
+ if (changed) break;
+ }
+ if(!changed)
+ return new VCGenOutcome(proverOutcome, new List<Counterexample>());
+ }
if (CommandLineOptions.Clo.Trace)
Console.WriteLine(collector.numErrors > 0 ? "SAT" : "UNSAT");
@@ -577,6 +587,9 @@ namespace Microsoft.Boogie.Houdini { vcgen.ConvertCFG2DAG(impl);
var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);
+ // Inline functions
+ (new InlineFunctionCalls()).VisitBlockList(impl.Blocks);
+
ExtractQuantifiedExprs(impl);
StripOutermostForall(impl);
@@ -787,6 +800,48 @@ namespace Microsoft.Boogie.Houdini { }
+ class InlineFunctionCalls : StandardVisitor
+ {
+ public Stack<string> inlinedFunctionsStack;
+
+ public InlineFunctionCalls()
+ {
+ inlinedFunctionsStack = new Stack<string>();
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ var fc = node.Fun as FunctionCall;
+ if (fc != null && fc.Func.Body != null && QKeyValue.FindBoolAttribute(fc.Func.Attributes, "inline"))
+ {
+ if (inlinedFunctionsStack.Contains(fc.Func.Name))
+ {
+ // recursion detected
+ throw new AbsHoudiniInternalError("Recursion detected in function declarations");
+ }
+
+ // create a substitution
+ var subst = new Dictionary<Variable, Expr>();
+ for (int i = 0; i < node.Args.Count; i++)
+ {
+ subst.Add(fc.Func.InParams[i], node.Args[i]);
+ }
+
+ var e =
+ Substituter.Apply(new Substitution(v => subst.ContainsKey(v) ? subst[v] : Expr.Ident(v)), fc.Func.Body);
+
+ inlinedFunctionsStack.Push(fc.Func.Name);
+
+ e = base.VisitExpr(e);
+
+ inlinedFunctionsStack.Pop();
+
+ return e;
+ }
+ return base.VisitNAryExpr(node);
+ }
+ }
+
class ReplaceFunctionCalls : StandardVisitor
{
public List<Tuple<string, Function, NAryExpr>> functionsUsed;
@@ -1150,6 +1205,17 @@ namespace Microsoft.Boogie.Houdini { return new Intervals();
}
+ public IAbstractDomain MakeTop(out bool changed)
+ {
+ if (lower == Int32.MinValue && upper == Int32.MaxValue)
+ {
+ changed = false;
+ return this;
+ }
+ changed = true;
+ return new Intervals(Int32.MinValue, Int32.MaxValue, 0);
+ }
+
public IAbstractDomain Join(List<Model.Element> states)
{
Debug.Assert(states.Count == 1);
@@ -1315,6 +1381,19 @@ namespace Microsoft.Boogie.Houdini { return new PredicateAbsElem();
}
+ public IAbstractDomain MakeTop(out bool changed)
+ {
+ if (conjuncts.Count == 0)
+ {
+ changed = false;
+ return this;
+ }
+ changed = true;
+ var ret = new PredicateAbsElem();
+ ret.isFalse = false;
+ return ret;
+ }
+
public IAbstractDomain Join(List<Model.Element> state)
{
if (state.Any(me => !(me is Model.Boolean)))
@@ -1413,6 +1492,14 @@ namespace Microsoft.Boogie.Houdini { return GetBottom();
}
+ public IAbstractDomain MakeTop(out bool changed)
+ {
+ changed = false;
+ if (isTop) return this;
+ changed = true;
+ return GetTop();
+ }
+
public IAbstractDomain Join(List<Model.Element> states)
{
Debug.Assert(states.Count == 1);
@@ -1481,6 +1568,17 @@ namespace Microsoft.Boogie.Houdini { return new PowDomain(Val.FALSE) as IAbstractDomain;
}
+ public IAbstractDomain MakeTop(out bool changed)
+ {
+ if (isTop)
+ {
+ changed = false;
+ return this;
+ }
+ changed = true;
+ return new PowDomain(Val.TRUE);
+ }
+
IAbstractDomain IAbstractDomain.Bottom()
{
return GetBottom();
@@ -1563,6 +1661,17 @@ namespace Microsoft.Boogie.Houdini { return GetBottom();
}
+ public IAbstractDomain MakeTop(out bool changed)
+ {
+ if (equalities.Count == 0)
+ {
+ changed = false;
+ return this;
+ }
+ changed = true;
+ return new EqualitiesDomain(false, new List<HashSet<int>>());
+ }
+
IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)
{
// find the guys that are equal
@@ -1676,6 +1785,16 @@ namespace Microsoft.Boogie.Houdini { return GetBottom();
}
+ public IAbstractDomain MakeTop(out bool changed)
+ {
+ if(val == Val.TRUE) {
+ changed = false;
+ return this;
+ }
+ changed = true;
+ return new ImplicationDomain(Val.TRUE);
+ }
+
public IAbstractDomain Join(List<Model.Element> states)
{
Debug.Assert(states.Count == 2);
@@ -1760,6 +1879,16 @@ namespace Microsoft.Boogie.Houdini { return new ConstantProp(null, false, true);
}
+ public IAbstractDomain MakeTop(out bool changed) {
+ if (isTop)
+ {
+ changed = false;
+ return this;
+ }
+ changed = true;
+ return GetTop();
+ }
+
private ConstantProp Join(ConstantProp that)
{
if (isBottom) return that;
@@ -1871,6 +2000,41 @@ namespace Microsoft.Boogie.Houdini { return new IndependentAttribute<T>();
}
+ public IAbstractDomain MakeTop(out bool changed)
+ {
+ var mt = new Func<IAbstractDomain>(() =>
+ {
+ var ret = new IndependentAttribute<T>();
+ ret.isBottom = true;
+ ret.numVars = numVars;
+ ret.underlyingInstance = underlyingInstance;
+ ret.varVal = new List<T>();
+ bool tmp;
+ for (int i = 0; i < varVal.Count; i++)
+ ret.varVal.Add(varVal[i].MakeTop(out tmp) as T);
+ return ret;
+ });
+
+ if (!isBottom)
+ {
+ foreach (var t in varVal)
+ {
+ var top = t.MakeTop(out changed);
+ if (changed)
+ {
+ return mt();
+ }
+ }
+ }
+ else
+ {
+ changed = true;
+ return mt();
+ }
+
+ changed = false;
+ return this;
+ }
public IAbstractDomain Join(List<Model.Element> state)
{
SetUnderlyingInstance();
@@ -2002,6 +2166,7 @@ namespace Microsoft.Boogie.Houdini { public interface IAbstractDomain
{
IAbstractDomain Bottom();
+ IAbstractDomain MakeTop(out bool changed);
IAbstractDomain Join(List<Model.Element> state);
Expr Gamma(List<Expr> vars);
bool TypeCheck(List<Type> argTypes, out string msg);
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 5222061f..ea526591 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -429,7 +429,7 @@ public class SmartBlockPredicator { var oldCmdSeq = block.Cmds;
block.Cmds = new List<Cmd>();
newBlocks.Add(block);
- if (prevBlock != null) {
+ if (prevBlock != null && !((prevBlock.TransferCmd is ReturnCmd) && uni != null && uni.IsUniform(impl.Name, block))) {
prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { block });
}
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index b46e6fea..fe749852 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -855,7 +855,8 @@ namespace Microsoft.Boogie.SMTLib labels = CalculatePath(handler.StartingProcId());
xlabels = labels;
}
- Model model = GetErrorModel();
+ Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory) ? null :
+ GetErrorModel();
handler.OnModel(xlabels, model);
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 086dde15..e4f63315 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -770,303 +770,6 @@ namespace VC { }
}
- public class CoverageGraphManager {
- public static int timeStamp = 0;
-
- public class Task {
- public enum TaskType { NONE, STEP, INLINE, BLOCK, REACHABLE };
-
- public TaskType type;
- private string query_string;
- public List<int> nodes;
- public int queryNode {
- get {
- Debug.Assert(nodes.Count == 1);
- return nodes[0];
- }
- }
-
- public Task(string q, FCallHandler calls) {
- query_string = q;
- nodes = new List<int>();
- if (q.StartsWith("step")) {
- type = TaskType.STEP;
- return;
- }
- var split = q.Split(' ');
- switch (split[0].ToLower()) {
- case "inline":
- type = TaskType.INLINE;
- break;
- case "block":
- type = TaskType.BLOCK;
- break;
- case "reachable":
- type = TaskType.REACHABLE;
- break;
- default:
- Debug.Assert(false);
- break;
- }
- for (int i = 1; i < split.Length; i++) {
- var node = calls.getCandidateFromGraphNode(split[i]);
- if (node != -1) {
- nodes.Add(node);
- }
-
- }
- // Prune nodes according to which are current candidates
- var pruned = new List<int>();
- foreach (var n in nodes) {
- if (calls.currCandidates.Contains(n)) {
- if (type == TaskType.INLINE || type == TaskType.BLOCK) {
- pruned.Add(n);
- }
- }
- else {
- if (type == TaskType.REACHABLE) {
- pruned.Add(n);
- }
- }
- }
-
- nodes = pruned;
- if (type == TaskType.REACHABLE && nodes.Count != 1) {
- type = TaskType.NONE;
- }
- else if (nodes.Count == 0) {
- type = TaskType.NONE;
- }
- }
-
- public bool isStep() {
- return (type == TaskType.STEP);
- }
-
- public override string ToString() {
- return query_string;
- }
- }
-
- public string getQuery(int ts) {
- var ret = "";
- while (true) {
- string str = coverageProcess.StandardOutput.ReadLine();
- if (str.StartsWith("query ")) {
- var split = str.Split(' ');
- if (split.Length < 1) continue;
- if (ts.ToString() == split[1]) {
- for (int i = 2; i < split.Length; i++) ret = ret + split[i] + " ";
- break;
- }
- }
- }
- return ret;
- }
-
- public static Process coverageProcess;
- public bool stopCoverageProcess;
- //private System.Threading.Thread readerThread;
- private FCallHandler calls;
- // Set of edges to send off to the coverageProcess
- private List<KeyValuePair<int, int>> edges;
- // Set of nodes to send off to the coverageProcess
- private HashSet<int> newNodes;
- // Set of nodes already declared
- private HashSet<int> declaredNodes;
-
- public CoverageGraphManager(FCallHandler calls) {
- stopCoverageProcess = true;
- coverageProcess = null;
- this.calls = calls;
- this.edges = new List<KeyValuePair<int, int>>();
- declaredNodes = new HashSet<int>();
- newNodes = new HashSet<int>();
-
- coverageProcess = CommandLineOptions.Clo.coverageReporter;
- if (coverageProcess != null) {
- stopCoverageProcess = false;
- if (!coverageProcess.StartInfo.RedirectStandardInput) {
- coverageProcess = null;
- }
- }
- else {
- if (CommandLineOptions.Clo.CoverageReporterPath != null) {
- coverageProcess = new Process();
- var coverageProcessInfo = new ProcessStartInfo();
- coverageProcessInfo.CreateNoWindow = true;
- coverageProcessInfo.FileName = CommandLineOptions.Clo.CoverageReporterPath + @"\CoverageGraph.exe";
- coverageProcessInfo.RedirectStandardInput = true;
- coverageProcessInfo.RedirectStandardOutput = true;
- coverageProcessInfo.RedirectStandardError = false;
- coverageProcessInfo.UseShellExecute = false;
- coverageProcessInfo.Arguments = "interactive";
-
- coverageProcess.StartInfo = coverageProcessInfo;
- try {
- coverageProcess.Start();
- }
- catch (System.ComponentModel.Win32Exception) {
- coverageProcess.Dispose();
- coverageProcess = null;
- }
- //readerThread = new System.Threading.Thread(new System.Threading.ThreadStart(CoverageGraphInterface));
- //readerThread.Start();
- }
- }
-
- if (coverageProcess != null) {
- coverageProcess.StandardInput.WriteLine("clear-all");
- }
- }
-
- public void addMain() {
- newNodes.Add(0);
- foreach (var n in calls.currCandidates) {
- addEdge(0, n);
- }
- calls.recentlyAddedCandidates = new HashSet<int>();
- }
-
- public void addNode(int src) {
- newNodes.Add(src);
- }
-
- public void addEdge(int src_id, int tgt_id) {
- newNodes.Add(src_id);
- newNodes.Add(tgt_id);
- edges.Add(new KeyValuePair<int, int>(src_id, tgt_id));
- }
-
- public void addRecentEdges(int src_id) {
- newNodes.Add(src_id);
- foreach (var tgt in calls.recentlyAddedCandidates) {
- addEdge(src_id, tgt);
- }
- calls.recentlyAddedCandidates = new HashSet<int>();
- }
-
- private void declareNodes() {
- var send = false;
- var declarenode = "declare-node";
- foreach (var n in newNodes) {
- if (declaredNodes.Contains(n)) continue;
- declaredNodes.Add(n);
- send = true;
- declarenode += string.Format(" {0} {1}", calls.getPersistentId(n), calls.getProc(n));
- }
- if (send)
- coverageProcess.StandardInput.WriteLine(declarenode);
- }
-
- private void declareEdges() {
- if (edges.Count == 0) return;
-
- var declareedge = "declare-edge";
- foreach (var e in edges) {
- declareedge += string.Format(" {0} {1}", calls.getPersistentId(e.Key), calls.getPersistentId(e.Value));
- }
- coverageProcess.StandardInput.WriteLine(declareedge);
- }
-
- public void syncGraph() {
- if (coverageProcess == null || newNodes.Count == 0) {
- edges.Clear();
- return;
- }
-
- coverageProcess.StandardInput.WriteLine("batch-graph-command-begin");
- coverageProcess.StandardInput.WriteLine("reset-color");
-
- // Go through the edges
- var greenNodes = new HashSet<int>();
- var redNodes = new HashSet<int>();
- foreach (var node in calls.currCandidates) {
- if (calls.getRecursionBound(node) > CommandLineOptions.Clo.RecursionBound) {
- redNodes.Add(node);
- }
- else {
- greenNodes.Add(node);
- }
-
- }
- // Send data across
- declareNodes();
- declareEdges();
-
- if (greenNodes.Count != 0) {
- var color = "color green";
- foreach (var n in greenNodes) {
- color += string.Format(" {0}", calls.getPersistentId(n));
- }
- coverageProcess.StandardInput.WriteLine(color);
- }
-
- if (redNodes.Count != 0) {
- var color = "color red";
- foreach (var n in redNodes) {
- color += string.Format(" {0}", calls.getPersistentId(n));
- }
- coverageProcess.StandardInput.WriteLine(color);
- }
-
- coverageProcess.StandardInput.WriteLine("batch-graph-command-end");
-
- edges.Clear();
- newNodes = new HashSet<int>();
- }
-
- public void reportBug() {
- if (coverageProcess == null) return;
- coverageProcess.StandardInput.WriteLine("set-status bug");
- }
-
- public void reportCorrect() {
- if (coverageProcess == null) return;
- coverageProcess.StandardInput.WriteLine("set-status correct");
- }
-
- public void reportCorrect(int bound) {
- if (coverageProcess == null) return;
- coverageProcess.StandardInput.WriteLine("set-status bound {0}", bound);
- }
-
- public void reportError() {
- if (coverageProcess == null) return;
- coverageProcess.StandardInput.WriteLine("set-status error");
- }
-
- public Task getNextTask() {
- if (coverageProcess == null) return new Task("step", calls);
- if (coverageProcess.HasExited) {
- coverageProcess = null;
- return new Task("step", calls);
- }
-
- var ts = getNextTimeStamp();
- coverageProcess.StandardInput.WriteLine("get-input " + ts.ToString());
- string q = getQuery(ts);
- return new Task(q, calls);
- }
-
- public void stop() {
- if (coverageProcess != null) {
- if (stopCoverageProcess) {
- coverageProcess.StandardInput.WriteLine("done");
- do {
- coverageProcess.WaitForExit(100);
- coverageProcess.StandardInput.WriteLine();
- } while (!coverageProcess.HasExited);
- }
- }
- }
-
- public int getNextTimeStamp() {
- timeStamp++;
- return timeStamp - 1;
- }
- }
-
public class ApiChecker {
public ProverInterface prover;
public ProverInterface.ErrorHandler reporter;
@@ -1114,8 +817,6 @@ namespace VC { // The call tree
public FCallHandler calls;
public ApiChecker checker;
- // The coverage graph reporter
- public CoverageGraphManager coverageManager;
// For statistics
public int vcSize;
public int expansionCount;
@@ -1167,7 +868,6 @@ namespace VC { // Put all of the necessary state into one object
var vState = new VerificationState(vcMain, calls, prover, new EmptyErrorHandler());
- vState.coverageManager = null;
// We'll restore the original state of the theorem prover at the end
// of this procedure
@@ -1370,11 +1070,6 @@ namespace VC { // Identify summary candidates: Match ensure clauses with the appropriate call site
if (useSummary) calls.matchSummaries();
- // create a process for displaying coverage information
- var coverageManager = new CoverageGraphManager(calls);
- coverageManager.addMain();
-
-
// We'll restore the original state of the theorem prover at the end
// of this procedure
prover.Push();
@@ -1382,7 +1077,6 @@ namespace VC { // Put all of the necessary state into one object
var vState = new VerificationState(vc, calls, prover, reporter, prover2, new EmptyErrorHandler());
vState.vcSize += SizeComputingVisitor.ComputeSize(vc);
- vState.coverageManager = coverageManager;
if (useSummary) summaryComputation = new SummaryComputation(vState, computeUnderBound);
@@ -1420,11 +1114,9 @@ namespace VC { }
#endregion
- #region Coverage reporter
if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
Console.WriteLine(">> SI: Size of VC after eager inlining: {0}", vState.vcSize);
}
- #endregion
// Under-approx query is only needed if something was inlined since
// the last time an under-approx query was made
@@ -1446,157 +1138,137 @@ namespace VC { // or we reached the recursion bound) and the task is "step"
// case 2: (bug) We find a bug
// case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
- while (true) {
- // Check timeout
- if (CommandLineOptions.Clo.ProverKillTime != -1) {
- if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime) {
- ret = Outcome.TimedOut;
- break;
+ while (true)
+ {
+ // Check timeout
+ if (CommandLineOptions.Clo.ProverKillTime != -1)
+ {
+ if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)
+ {
+ ret = Outcome.TimedOut;
+ break;
+ }
}
- }
- // Note: in the absence of a coverage graph process, the task is always "step"
- coverageManager.syncGraph();
- var task = coverageManager.getNextTask();
- if (task.type == CoverageGraphManager.Task.TaskType.INLINE) {
- if (done == 2) continue;
- foreach (var id in task.nodes) {
- calls.setRecursionIncrement(id, 0);
- coverageManager.addNode(id);
- }
- DoExpansion(task.nodes, vState);
- }
- else if (task.type == CoverageGraphManager.Task.TaskType.BLOCK) {
- if (done == 2) continue;
- foreach (var id in task.nodes) {
- calls.setRecursionIncrement(id, CommandLineOptions.Clo.RecursionBound + 1);
- coverageManager.addNode(id);
- }
- }
- else if (task.type == CoverageGraphManager.Task.TaskType.STEP) {
- if (done > 0) {
- break;
+ if (done > 0)
+ {
+ break;
}
VCExpr summary = null;
if (useSummary) summary = summaryComputation.getSummary();
- if (useSummary && summary != null) {
- vState.checker.prover.Push();
- vState.checker.prover.Assert(summary, true);
+ if (useSummary && summary != null)
+ {
+ vState.checker.prover.Push();
+ vState.checker.prover.Assert(summary, true);
}
// Stratified Step
ret = stratifiedStep(bound, vState, block);
iters++;
- if (useSummary && summary != null) {
- vState.checker.prover.Pop();
+ if (useSummary && summary != null)
+ {
+ vState.checker.prover.Pop();
}
// Sorry, out of luck (time/memory)
- if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut) {
- done = 3;
- coverageManager.reportError();
- continue;
+ if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut)
+ {
+ done = 3;
+ continue;
}
- if (ret == Outcome.Errors && reporter.underapproximationMode) {
- // Found a bug
- done = 2;
- coverageManager.reportBug();
+ if (ret == Outcome.Errors && reporter.underapproximationMode)
+ {
+ // Found a bug
+ done = 2;
}
- else if (ret == Outcome.Correct) {
- if (block.Count == 0) {
- // Correct
- done = 1;
- coverageManager.reportCorrect();
- }
- else {
- Contract.Assert(useSummary);
- // reset blocked and continue loop
- block.Clear();
- }
+ else if (ret == Outcome.Correct)
+ {
+ if (block.Count == 0)
+ {
+ // Correct
+ done = 1;
+ }
+ else
+ {
+ Contract.Assert(useSummary);
+ // reset blocked and continue loop
+ block.Clear();
+ }
}
- else if (ret == Outcome.ReachedBound) {
- if (block.Count == 0) {
- // Increment bound
- bound++;
- if (useSummary) summaryComputation.boundChanged();
-
- if (bound > CommandLineOptions.Clo.RecursionBound) {
- // Correct under bound
- done = 1;
- coverageManager.reportCorrect(bound);
+ else if (ret == Outcome.ReachedBound)
+ {
+ if (block.Count == 0)
+ {
+ // Increment bound
+ bound++;
+ if (useSummary) summaryComputation.boundChanged();
+
+ if (bound > CommandLineOptions.Clo.RecursionBound)
+ {
+ // Correct under bound
+ done = 1;
+ }
+ }
+ else
+ {
+ Contract.Assert(useSummary);
+ // reset blocked and continue loop
+ block.Clear();
}
- }
- else {
- Contract.Assert(useSummary);
- // reset blocked and continue loop
- block.Clear();
- }
}
- else {
- // Do inlining
- Debug.Assert(ret == Outcome.Errors && !reporter.underapproximationMode);
- Contract.Assert(reporter.candidatesToExpand.Count != 0);
- if (useSummary) {
- // compute candidates to block
- block = new HashSet<int>(calls.currCandidates);
- block.ExceptWith(reporter.candidatesToExpand);
- }
+ else
+ {
+ // Do inlining
+ Debug.Assert(ret == Outcome.Errors && !reporter.underapproximationMode);
+ Contract.Assert(reporter.candidatesToExpand.Count != 0);
+ if (useSummary)
+ {
+ // compute candidates to block
+ block = new HashSet<int>(calls.currCandidates);
+ block.ExceptWith(reporter.candidatesToExpand);
+ }
- #region expand call tree
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
- Console.Write(">> SI Inlining: ");
- reporter.candidatesToExpand
- .Select(c => calls.getProc(c))
- .Iter(c => { if (!isSkipped(c)) Console.Write("{0} ", c); });
+ #region expand call tree
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
+ {
+ Console.Write(">> SI Inlining: ");
+ reporter.candidatesToExpand
+ .Select(c => calls.getProc(c))
+ .Iter(c => { if (!isSkipped(c)) Console.Write("{0} ", c); });
- Console.WriteLine();
- Console.Write(">> SI Skipping: ");
- reporter.candidatesToExpand
- .Select(c => calls.getProc(c))
- .Iter(c => { if (isSkipped(c)) Console.Write("{0} ", c); });
+ Console.WriteLine();
+ Console.Write(">> SI Skipping: ");
+ reporter.candidatesToExpand
+ .Select(c => calls.getProc(c))
+ .Iter(c => { if (isSkipped(c)) Console.Write("{0} ", c); });
- Console.WriteLine();
+ Console.WriteLine();
- }
+ }
- // Expand and try again
- vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
- DoExpansion(reporter.candidatesToExpand, vState);
- vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
+ // Expand and try again
+ vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
+ DoExpansion(reporter.candidatesToExpand, vState);
+ vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
- #endregion
+ #endregion
}
- }
- else if (task.type == CoverageGraphManager.Task.TaskType.REACHABLE) {
- if (done == 2) continue;
- var node = task.queryNode;
- // assert that any path must pass through this node
- var expr = calls.getTrueExpr(node);
- vState.checker.prover.Assert(expr, true);
- }
- else {
- Console.WriteLine("Ignoring task: " + task.ToString());
- }
-
}
// Pop off everything that we pushed so that there are no side effects from
// this call to VerifyImplementation
vState.checker.prover.Pop();
- #region Coverage reporter
if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);
Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);
Console.WriteLine(">> SI: Candidates skipped: {0}", calls.currCandidates.Where(i => isSkipped(i, calls)).Count());
Console.WriteLine(">> SI: VC Size: {0}", vState.vcSize);
}
- #endregion
- coverageManager.stop();
numInlined = (calls.candidateParent.Keys.Count + 1) - (calls.currCandidates.Count);
@@ -1801,7 +1473,6 @@ namespace VC { calls.setCurrProc(procName);
expansion = calls.Mutate(expansion, true);
if (useSummary) calls.matchSummaries();
- if (vState.coverageManager != null) vState.coverageManager.addRecentEdges(id);
//expansion = checker.VCExprGen.Eq(calls.id2ControlVar[id], expansion);
expansion = prover.VCExprGen.Implies(calls.id2ControlVar[id], expansion);
@@ -2178,9 +1849,9 @@ namespace VC { string calleeName = naryExpr.Fun.FunctionName;
VCExprNAry callExpr = retnary[0] as VCExprNAry;
- Contract.Assert(callExpr != null);
if (implName2StratifiedInliningInfo.ContainsKey(calleeName)) {
+ Contract.Assert(callExpr != null);
int candidateId = GetNewId(callExpr);
boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId;
candidateParent[candidateId] = currInlineCount;
@@ -2193,13 +1864,16 @@ namespace VC { return Gen.LabelPos(label, id2ControlVar[candidateId]);
}
else if (calleeName.StartsWith(recordProcName)) {
+ Contract.Assert(callExpr != null);
Debug.Assert(callExpr.Length == 1);
Debug.Assert(callExpr[0] != null);
recordExpr2Var[new BoogieCallExpr(naryExpr, currInlineCount)] = callExpr[0];
return callExpr;
}
else {
- return callExpr;
+ // callExpr can be null; this happens when the FunctionCall was on a
+ // pure function (not procedure) and the function got inlined
+ return retnary[0];
}
}
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index bb2a2785..c9b7ae83 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -152,7 +152,7 @@ namespace VC { if (pname != null) {
return gen.ImpliesSimp(gen.LabelPos("candidate_" + pname.ToString(), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
}
-
+
// Label the assume if it is a procedure call
NAryExpr naryExpr = ac.Expr as NAryExpr;
if (naryExpr != null) {
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index dd5344e8..bed39837 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -502,3 +502,14 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
+----- Running regression test bar12.bpl
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar12.bpl(6,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar13.bpl
+
+Boogie program verifier finished with 1 verified, 0 errors
+-----
diff --git a/Test/stratifiedinline/bar12.bpl b/Test/stratifiedinline/bar12.bpl new file mode 100644 index 00000000..863f9dc0 --- /dev/null +++ b/Test/stratifiedinline/bar12.bpl @@ -0,0 +1,8 @@ +function {:inline} f(a:bool) : bool { true }
+
+procedure {:entrypoint} main()
+{
+ var x: int;
+ assume f(x >= 0);
+ assume x >= 0;
+}
diff --git a/Test/stratifiedinline/bar13.bpl b/Test/stratifiedinline/bar13.bpl new file mode 100644 index 00000000..bdeaaa51 --- /dev/null +++ b/Test/stratifiedinline/bar13.bpl @@ -0,0 +1,34 @@ +var alloc: int;
+var assertsPassed: bool;
+procedure boogie_si_record_li2bpl_int(x: int);
+
+procedure __HAVOC_malloc(size: int) returns (ret: int);
+ free requires size >= 0;
+ modifies alloc;
+ free ensures ret == old(alloc);
+ free ensures alloc >= old(alloc) + size;
+
+
+procedure foo(arg: int)
+ modifies alloc;
+{
+ var tt: int;
+
+ anon0__unique__1:
+ // assume NumberOfBytes_2 >= 0;
+ call boogie_si_record_li2bpl_int(arg);
+ call tt := __HAVOC_malloc(arg);
+ call boogie_si_record_li2bpl_int(alloc);
+ return;
+}
+
+procedure {:entrypoint} main()
+ modifies alloc;
+{
+ var t1: int;
+
+ assume alloc > 0;
+ call foo(t1);
+ assume alloc < 0;
+}
+
diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat index 07261c4d..eb5ff634 100644 --- a/Test/stratifiedinline/runtest.bat +++ b/Test/stratifiedinline/runtest.bat @@ -34,4 +34,10 @@ echo ----- echo ----- Running regression test bar11.bpl
%BGEXE% %* /stratifiedInline:1 /vc:i bar11.bpl
echo -----
+echo ----- Running regression test bar12.bpl
+%BGEXE% %* /stratifiedInline:1 /vc:i bar12.bpl
+echo -----
+echo ----- Running regression test bar13.bpl
+%BGEXE% %* /stratifiedInline:1 /vc:i bar13.bpl
+echo -----
|