summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-04-25 16:47:36 -0700
committerGravatar qadeer <unknown>2014-04-25 16:47:36 -0700
commit1a114f457299c87f9e9548992659ffc726fe5e7a (patch)
treefe1e6b9c3d79d8547c22db8fb5a7f44315f5b5ce
parentb17515ca23fc7f5ae1fb8e6642366f761d0eeacf (diff)
updated the mover checks
-rw-r--r--Source/Concurrency/MoverCheck.cs51
-rw-r--r--Source/Concurrency/OwickiGries.cs14
-rw-r--r--Source/Concurrency/TypeCheck.cs2
-rw-r--r--Source/Core/AbsyCmd.cs14
-rw-r--r--Source/Core/ResolutionContext.cs4
-rw-r--r--Test/og/Answer6
6 files changed, 81 insertions, 10 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 4957c829..73c1163a 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -562,6 +562,10 @@ namespace Microsoft.Boogie
blocks.AddRange(firstBlocks);
blocks.AddRange(secondBlocks);
List<Requires> requires = DisjointnessRequires(program, first, second);
+ foreach (AssertCmd assertCmd in first.thatGate)
+ requires.Add(new Requires(false, assertCmd.Expr));
+ foreach (AssertCmd assertCmd in second.thisGate)
+ requires.Add(new Requires(false, assertCmd.Expr));
List<Ensures> ensures = new List<Ensures>();
Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).TransitionRelationCompute();
Ensures ensureCheck = new Ensures(false, transitionRelation);
@@ -604,6 +608,8 @@ namespace Microsoft.Boogie
ensureCheck.ErrorData = string.Format("Gate not preserved by {0}", second.proc.Name);
ensures.Add(ensureCheck);
}
+ foreach (AssertCmd assertCmd in second.thisGate)
+ requires.Add(new Requires(false, assertCmd.Expr));
string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));
@@ -618,6 +624,48 @@ namespace Microsoft.Boogie
{
if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
return;
+ 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.thatInParams);
+ inputs.AddRange(second.thisInParams);
+ List<Variable> outputs = new List<Variable>();
+ outputs.AddRange(first.thatOutParams);
+ outputs.AddRange(second.thisOutParams);
+ List<Variable> locals = new List<Variable>();
+ locals.AddRange(second.thisAction.LocVars);
+ List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ Expr gateExpr = Expr.True;
+ foreach (AssertCmd assertCmd in first.thatGate)
+ {
+ gateExpr = Expr.And(gateExpr, assertCmd.Expr);
+ }
+ requires.Add(new Requires(false, Expr.Not(gateExpr)));
+ List<Ensures> ensures = new List<Ensures>();
+ Ensures ensureCheck = new Ensures(false, Expr.Not(gateExpr));
+ ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);
+ ensures.Add(ensureCheck);
+ foreach (AssertCmd assertCmd in second.thisGate)
+ requires.Add(new Requires(false, assertCmd.Expr));
+ string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
+ program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));
+ Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
+ Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
+ impl.Proc = proc;
+ this.decls.Add(impl);
+ this.decls.Add(proc);
+ }
+
+ /*
+ private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
+ return;
Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
if (failurePreservationCheckerCache.Contains(actionPair))
@@ -660,7 +708,8 @@ namespace Microsoft.Boogie
this.decls.Add(impl);
this.decls.Add(proc);
}
-
+ */
+
private void CreateNonBlockingChecker(Program program, ActionInfo second)
{
List<Variable> inputs = new List<Variable>();
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index b646e8cf..9ec07854 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -1283,7 +1283,19 @@ namespace Microsoft.Boogie
duplicateProc.Modifies = new List<IdentifierExpr>();
program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(Expr.Ident(x)));
CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);
- Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, action.Blocks);
+
+ List<Cmd> cmds = new List<Cmd>();
+ foreach (AssertCmd assertCmd in moverTypeChecker.procToActionInfo[proc].thisGate)
+ {
+ cmds.Add(new AssumeCmd(Token.NoToken, (Expr)duplicator.Visit(assertCmd.Expr)));
+ }
+ Block newInitBlock = new Block(Token.NoToken, "_init", cmds,
+ new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),
+ new List<Block>(new Block[] { action.Blocks[0] })));
+ List<Block> newBlocks = new List<Block>();
+ newBlocks.Add(newInitBlock);
+ newBlocks.AddRange(action.Blocks);
+ Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, newBlocks);
impl.Proc = duplicateProc;
impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 5a15c707..5a8c81f6 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -84,7 +84,7 @@ namespace Microsoft.Boogie
AssertCmd assertCmd = cmds[i] as AssertCmd;
if (assertCmd == null) break;
thisGate.Add(assertCmd);
- cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
+ cmds[i] = new AssumeCmd(assertCmd.tok, Expr.True);
}
Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index e4451807..cd7a8edd 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -957,9 +957,19 @@ namespace Microsoft.Boogie {
{
tc.Error(this, "command assigns to an immutable variable: {0}", v.Name);
}
- else if (!CommandLineOptions.Clo.DoModSetAnalysis && v is GlobalVariable && !tc.InFrame(v))
+ else if (!CommandLineOptions.Clo.DoModSetAnalysis && v is GlobalVariable)
{
- tc.Error(this, "command assigns to a global variable that is not in the enclosing procedure's modifies clause: {0}", v.Name);
+ if (tc.Yields) {
+ // a yielding procedure is allowed to modify any global variable
+ }
+ else if (tc.Frame == null)
+ {
+ tc.Error(this, "update to a global variable allowed only inside an atomic action of a yielding procedure");
+ }
+ else if (!tc.InFrame(v))
+ {
+ tc.Error(this, "command assigns to a global variable that is not in the enclosing procedure's modifies clause: {0}", v.Name);
+ }
}
}
}
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index eb27c82a..741d2ac5 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -622,8 +622,8 @@ namespace Microsoft.Boogie {
public bool InFrame(Variable v) {
Contract.Requires(v != null);
- Contract.Requires(Yields || Frame != null);
- return Yields || Frame.Any(f => f.Decl == v);
+ Contract.Requires(Frame != null);
+ return Frame.Any(f => f.Decl == v);
}
}
}
diff --git a/Test/og/Answer b/Test/og/Answer
index f64868f7..a02a2838 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -98,7 +98,7 @@ Boogie program verifier finished with 1 verified, 1 error
-------------------- DeviceCache.bpl --------------------
-Boogie program verifier finished with 50 verified, 0 errors
+Boogie program verifier finished with 35 verified, 0 errors
-------------------- ticket.bpl --------------------
@@ -114,8 +114,8 @@ Boogie program verifier finished with 6 verified, 0 errors
-------------------- multiset.bpl --------------------
-Boogie program verifier finished with 104 verified, 0 errors
+Boogie program verifier finished with 85 verified, 0 errors
-------------------- civl-paper.bpl --------------------
-Boogie program verifier finished with 37 verified, 0 errors
+Boogie program verifier finished with 29 verified, 0 errors