From 72349460a6896518a1bac2644f1f9efc681209fa Mon Sep 17 00:00:00 2001 From: qadeer Date: Thu, 9 Jan 2014 21:47:40 -0800 Subject: implemented a simple quantifier elimination for havoc commands in computing transition relation changed the type checking of left movers; they are required to be non-blocking now --- Source/Concurrency/MoverCheck.cs | 112 ++++++++++++++++++++++++++++++--------- 1 file changed, 86 insertions(+), 26 deletions(-) (limited to 'Source/Concurrency/MoverCheck.cs') diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 781fcb36..4f538c52 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -148,7 +148,6 @@ namespace Microsoft.Boogie private ActionInfo second; // corresponds to this* private Stack path; private Expr transitionRelation; - private int boundVariableCount; public TransitionRelationComputation(Program program, ActionInfo second) { @@ -157,7 +156,6 @@ namespace Microsoft.Boogie this.second = second; this.path = new Stack(); this.transitionRelation = Expr.False; - this.boundVariableCount = 0; } public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second) @@ -167,12 +165,6 @@ namespace Microsoft.Boogie this.second = second; this.path = new Stack(); this.transitionRelation = Expr.False; - this.boundVariableCount = 0; - } - - private BoundVariable GetBoundVariable(Type type) - { - return new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, type)); } public Expr Compute() @@ -189,27 +181,39 @@ namespace Microsoft.Boogie return transitionRelation; } + private void Substitute(Dictionary map, ref Expr returnExpr, ref Dictionary varToExpr) + { + Substitution subst = Substituter.SubstitutionFromHashtable(map); + returnExpr = Substituter.Apply(subst, returnExpr); + Dictionary oldVarToExpr = varToExpr; + varToExpr = new Dictionary(); + foreach (Variable v in oldVarToExpr.Keys) + { + varToExpr[v] = Substituter.Apply(subst, oldVarToExpr[v]); + } + } + private Expr CalculatePathCondition() { - Expr returnExpr = Expr.True; + HashSet existsVars = new HashSet(); + Dictionary varToExpr = new Dictionary(); 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); + varToExpr[v] = Expr.Ident(v); } if (first != null) { foreach (Variable v in first.thatOutParams) { - var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); - returnExpr = Expr.And(eqExpr, returnExpr); + varToExpr[v] = Expr.Ident(v); } } foreach (Variable v in second.thisOutParams) { - var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); - returnExpr = Expr.And(eqExpr, returnExpr); + varToExpr[v] = Expr.Ident(v); } + Expr returnExpr = Expr.True; + int boundVariableCount = 0; foreach (Cmd cmd in path) { if (cmd is AssumeCmd) @@ -225,30 +229,45 @@ namespace Microsoft.Boogie { map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k]; } - Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary()); - Substitution oldSubst = Substituter.SubstitutionFromHashtable(map); - returnExpr = (Expr)new MySubstituter(subst, oldSubst).Visit(returnExpr); + Substitute(map, ref returnExpr, ref varToExpr); } else if (cmd is HavocCmd) { HavocCmd havocCmd = cmd as HavocCmd; - List existVars = new List(); Dictionary map = new Dictionary(); foreach (IdentifierExpr ie in havocCmd.Vars) { - BoundVariable bv = GetBoundVariable(ie.Decl.TypedIdent.Type); + BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, ie.Decl.TypedIdent.Type)); map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv); - existVars.Add(bv); + existsVars.Add(bv); } - Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary()); - Substitution oldSubst = Substituter.SubstitutionFromHashtable(map); - returnExpr = new ExistsExpr(Token.NoToken, existVars, (Expr)new MySubstituter(subst, oldSubst).Visit(returnExpr)); + Substitute(map, ref returnExpr, ref varToExpr); } else { Debug.Assert(false); } } + Dictionary existsMap = new Dictionary(); + foreach (Variable v in varToExpr.Keys) + { + IdentifierExpr ie = varToExpr[v] as IdentifierExpr; + if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl)) + { + existsMap[ie.Decl] = Expr.Ident(v); + existsVars.Remove(ie.Decl); + } + } + Substitute(existsMap, ref returnExpr, ref varToExpr); + returnExpr = new OldExpr(Token.NoToken, returnExpr); + foreach (Variable v in varToExpr.Keys) + { + returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), varToExpr[v])); + } + if (existsVars.Count > 0) + { + returnExpr = new ExistsExpr(Token.NoToken, new List(existsVars), returnExpr); + } return returnExpr; } @@ -364,7 +383,6 @@ namespace Microsoft.Boogie return; if (first.CommutesWith(second)) return; - Tuple actionPair = new Tuple(first, second); if (commutativityCheckerCache.Contains(actionPair)) return; @@ -413,7 +431,6 @@ namespace Microsoft.Boogie { if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0) return; - Tuple actionPair = new Tuple(first, second); if (gatePreservationCheckerCache.Contains(actionPair)) return; @@ -446,6 +463,49 @@ namespace Microsoft.Boogie } private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second) + { + Debug.Assert(second.isNonBlocking); + if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0) + return; + Tuple actionPair = new Tuple(first, second); + if (failurePreservationCheckerCache.Contains(actionPair)) + return; + failurePreservationCheckerCache.Add(actionPair); + + List inputs = new List(); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); + + Expr failureExpr = Expr.True; + foreach (AssertCmd assertCmd in first.thatGate) + { + failureExpr = Expr.And(assertCmd.Expr, failureExpr); + } + failureExpr = Expr.Not(failureExpr); + + List requires = DisjointnessRequires(program, first, second); + requires.Add(new Requires(false, failureExpr)); + + List ensures = new List(); + ensures.Add(new Ensures(false, failureExpr)); + + List outputs = new List(); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); + List locals = new List(); + locals.AddRange(second.thisAction.LocVars); + List secondBlocks = CloneBlocks(second.thisAction.Blocks); + string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); + List globalVars = new List(); + program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, outputs, locals, secondBlocks); + impl.Proc = proc; + this.decls.Add(impl); + this.decls.Add(proc); + } + + private void CreateFailurePreservationCheckerOld(Program program, ActionInfo first, ActionInfo second) { if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0 && second.isNonBlocking) return; -- cgit v1.2.3