summaryrefslogtreecommitdiff
path: root/Source/Concurrency
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 /Source/Concurrency
parentb17515ca23fc7f5ae1fb8e6642366f761d0eeacf (diff)
updated the mover checks
Diffstat (limited to 'Source/Concurrency')
-rw-r--r--Source/Concurrency/MoverCheck.cs51
-rw-r--r--Source/Concurrency/OwickiGries.cs14
-rw-r--r--Source/Concurrency/TypeCheck.cs2
3 files changed, 64 insertions, 3 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>();