From 21926244abf754a7546ae48b0ba53b1369ae164b Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 10 Jan 2014 13:33:26 -0800 Subject: extended NormalSubstituter so that it can take in a forold substitution optimized the FailurePreservationChecker to eliminate some quantifiers --- Source/Concurrency/MoverCheck.cs | 42 +++++++++----------- Source/Core/Duplicator.cs | 84 ++++++++++++++++++++++++++++++++++++---- 2 files changed, 95 insertions(+), 31 deletions(-) diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 4f538c52..61e3bf02 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -462,7 +462,7 @@ namespace Microsoft.Boogie this.decls.Add(proc); } - private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second) + private void CreateFailurePreservationCheckerForall(Program program, ActionInfo first, ActionInfo second) { Debug.Assert(second.isNonBlocking); if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0) @@ -505,7 +505,7 @@ namespace Microsoft.Boogie this.decls.Add(proc); } - private void CreateFailurePreservationCheckerOld(Program program, ActionInfo first, ActionInfo second) + private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second) { if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0 && second.isNonBlocking) return; @@ -519,54 +519,50 @@ namespace Microsoft.Boogie inputs.AddRange(first.thatInParams); inputs.AddRange(second.thisInParams); - Expr transitionRelation = (new TransitionRelationComputation(program, second)).Compute(); - Expr expr = Expr.True; + Expr requiresExpr = Expr.True; foreach (AssertCmd assertCmd in first.thatGate) { - expr = Expr.And(assertCmd.Expr, expr); + requiresExpr = Expr.And(assertCmd.Expr, requiresExpr); } + requiresExpr = Expr.Not(requiresExpr); List requires = DisjointnessRequires(program, first, second); - requires.Add(new Requires(false, Expr.Not(expr))); + requires.Add(new Requires(false, requiresExpr)); foreach (AssertCmd assertCmd in second.thisGate) { requires.Add(new Requires(false, assertCmd.Expr)); } - + Dictionary map = new Dictionary(); Dictionary oldMap = new Dictionary(); List boundVars = new List(); 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.thisOutParams) - { + if (second.modifiedGlobalVars.Contains(v)) { 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); } + else { - 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); + map[v] = new OldExpr(Token.NoToken, Expr.Ident(v)); } + oldMap[v] = Expr.Ident(v); } - foreach (Variable v in second.thisAction.LocVars) + foreach (Variable v in second.thisOutParams) { - BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type)); + BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type)); boundVars.Add(bv); - oldMap[v] = new IdentifierExpr(Token.NoToken, bv); + map[v] = new IdentifierExpr(Token.NoToken, bv); } - Expr ensuresExpr = Expr.And(transitionRelation, Expr.Not(expr)); + Expr ensuresExpr = Expr.And((new TransitionRelationComputation(program, second)).Compute(), requiresExpr); + Substitution subst = Substituter.SubstitutionFromHashtable(map); + Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap); + ensuresExpr = Substituter.Apply(subst, oldSubst, ensuresExpr); 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)); + ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, ensuresExpr); } List ensures = new List(); ensures.Add(new Ensures(false, ensuresExpr)); diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 07ccba77..a11c93ec 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -423,6 +423,22 @@ namespace Microsoft.Boogie { return (Expr)new NormalSubstituter(subst).Visit(expr); } + /// + /// Apply a substitution to an expression. + /// Outside "old" expressions, the substitution "always" is applied; any variable not in + /// 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. + /// + public static Expr Apply(Substitution always, Substitution forold, Expr expr) + { + Contract.Requires(expr != null); + Contract.Requires(always != null); + Contract.Requires(forold != null); + Contract.Ensures(Contract.Result() != null); + return (Expr)new NormalSubstituter(always, forold).Visit(expr); + } + /// /// Apply a substitution to a command. Any variables not in domain(subst) /// is not changed. The substitutions applies within the "old", but the "old" @@ -435,6 +451,22 @@ namespace Microsoft.Boogie { return (Cmd)new NormalSubstituter(subst).Visit(cmd); } + /// + /// Apply a substitution to a command. + /// Outside "old" expressions, the substitution "always" is applied; any variable not in + /// 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. + /// + public static Cmd Apply(Substitution always, Substitution forold, Cmd cmd) + { + Contract.Requires(cmd != null); + Contract.Requires(always != null); + Contract.Requires(forold != null); + Contract.Ensures(Contract.Result() != null); + return (Cmd)new NormalSubstituter(always, forold).Visit(cmd); + } + /// /// Apply a substitution to an expression replacing "old" expressions. /// Outside "old" expressions, the substitution "always" is applied; any variable not in @@ -466,23 +498,59 @@ namespace Microsoft.Boogie { } private sealed class NormalSubstituter : Duplicator { - private readonly Substitution/*!*/ subst; + private readonly Substitution/*!*/ always; + private readonly Substitution/*!*/ forold; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(subst != null); + Contract.Invariant(always != null); + Contract.Invariant(forold != null); } public NormalSubstituter(Substitution subst) : base() { Contract.Requires(subst != null); - this.subst = subst; + this.always = subst; + this.forold = Substituter.SubstitutionFromHashtable(new Dictionary()); } - public override Expr VisitIdentifierExpr(IdentifierExpr node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - Expr/*?*/ e = subst(cce.NonNull(node.Decl)); - return e == null ? base.VisitIdentifierExpr(node) : e; + public NormalSubstituter(Substitution subst, Substitution forold) + : base() + { + Contract.Requires(subst != null); + this.always = subst; + this.forold = forold; + } + + private bool insideOldExpr = false; + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + Expr/*?*/ e = null; + + if (insideOldExpr) + { + e = forold(cce.NonNull(node.Decl)); + } + + if (e == null) + { + e = always(cce.NonNull(node.Decl)); + } + + return e == null ? base.VisitIdentifierExpr(node) : e; + } + + public override Expr VisitOldExpr(OldExpr node) + { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + bool previouslyInOld = insideOldExpr; + insideOldExpr = true; + Expr/*!*/ e = (Expr/*!*/)cce.NonNull(this.Visit(node.Expr)); + insideOldExpr = previouslyInOld; + return new OldExpr(node.tok, e); } } -- cgit v1.2.3