From 7417fddf0c8fd0caaa3df0c2700231253e92e117 Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 21 Jan 2014 22:53:07 -0800 Subject: various bug fixes added "cnst" feature --- Source/Concurrency/LinearSets.cs | 163 +++++++++++++++++++++++++++----------- Source/Concurrency/MoverCheck.cs | 150 +++++++++++++++++++++++++---------- Source/Concurrency/OwickiGries.cs | 61 ++++++-------- Source/Concurrency/TypeCheck.cs | 6 +- 4 files changed, 252 insertions(+), 128 deletions(-) (limited to 'Source') diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index 0b6cf232..f7b14836 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -4,6 +4,7 @@ using System.Linq; using System.Text; using System.Threading.Tasks; using Microsoft.Boogie; +using System.Diagnostics; namespace Microsoft.Boogie { @@ -13,7 +14,9 @@ namespace Microsoft.Boogie { if (iter == null) return null; iter.Next = RemoveLinearAttribute(iter.Next); - return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next; + bool iterIsNonLinear = QKeyValue.FindStringAttribute(iter, "linear") == null && + QKeyValue.FindStringAttribute(iter, "cnst") == null; + return iterIsNonLinear ? iter : iter.Next; } public override Variable VisitVariable(Variable node) @@ -23,14 +26,20 @@ namespace Microsoft.Boogie } } + public enum LinearKind { + LINEAR, + CONST + } + public class LinearTypeChecker : StandardVisitor { public Program program; public int errorCount; public CheckingContext checkingContext; public Dictionary domainNameToType; - public Dictionary> availableLinearVars; - public Dictionary inoutParamToDomainName; + private Dictionary> availableLinearVars; + public Dictionary inParamToLinearQualifier; + public Dictionary outParamToDomainName; public Dictionary varToDomainName; public Dictionary globalVarToDomainName; public Dictionary linearDomains; @@ -42,7 +51,8 @@ namespace Microsoft.Boogie this.checkingContext = new CheckingContext(null); this.domainNameToType = new Dictionary(); this.availableLinearVars = new Dictionary>(); - this.inoutParamToDomainName = new Dictionary(); + this.inParamToLinearQualifier = new Dictionary(); + this.outParamToDomainName = new Dictionary(); this.varToDomainName = new Dictionary(); this.linearDomains = new Dictionary(); } @@ -77,10 +87,11 @@ namespace Microsoft.Boogie HashSet start = new HashSet(globalVarToDomainName.Keys); for (int i = 0; i < node.InParams.Count; i++) { - string domainName = FindDomainName(node.Proc.InParams[i]); + Variable v = node.Proc.InParams[i]; + string domainName = FindDomainName(v); if (domainName != null) { - inoutParamToDomainName[node.InParams[i]] = domainName; + inParamToLinearQualifier[node.InParams[i]] = new LinearQualifier(domainName, FindLinearKind(v)); start.Add(node.InParams[i]); } } @@ -89,7 +100,7 @@ namespace Microsoft.Boogie string domainName = FindDomainName(node.Proc.OutParams[i]); if (domainName != null) { - inoutParamToDomainName[node.OutParams[i]] = domainName; + outParamToDomainName[node.OutParams[i]] = domainName; } } @@ -144,6 +155,29 @@ namespace Microsoft.Boogie } return impl; } + public void AddAvailableVars(CallCmd callCmd, HashSet start) + { + foreach (IdentifierExpr ie in callCmd.Outs) + { + if (FindDomainName(ie.Decl) == null) continue; + start.Add(ie.Decl); + } + for (int i = 0; i < callCmd.Proc.InParams.Count; i++) + { + IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr; + if (ie == null) continue; + Variable v = callCmd.Proc.InParams[i]; + if (FindDomainName(v) == null || FindLinearKind(v) == LinearKind.LINEAR) continue; + start.Add(ie.Decl); + } + } + public void AddAvailableVars(ParCallCmd parCallCmd, HashSet start) + { + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + AddAvailableVars(callCmd, start); + } + } private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) { HashSet start = new HashSet(availableLinearVars[b]); foreach (Cmd cmd in b.Cmds) @@ -155,13 +189,17 @@ namespace Microsoft.Boogie { if (FindDomainName(assignCmd.Lhss[i].DeepAssignedVariable) == null) continue; IdentifierExpr ie = assignCmd.Rhss[i] as IdentifierExpr; - if (start.Contains(ie.Decl)) + if (!start.Contains(ie.Decl)) { - start.Remove(ie.Decl); + Error(ie, "unavailable source for a linear read"); } - else + else if (FindLinearKind(ie.Decl) == LinearKind.CONST) { - Error(ie, "unavailable source for a linear read"); + Error(ie, "const linear vars cannot occur on the right side of a linear assignment"); + } + else + { + start.Remove(ie.Decl); } } foreach (AssignLhs assignLhs in assignCmd.Lhss) @@ -183,19 +221,15 @@ namespace Microsoft.Boogie IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr; if (start.Contains(ie.Decl)) { - start.Remove(ie.Decl); + start.Remove(ie.Decl); } else { - Error(ie, "unavailable source for a linear read"); + Error(ie, "unavailable source for a linear read"); } } availableLinearVars[callCmd] = new HashSet(start); - foreach (IdentifierExpr ie in callCmd.Outs) - { - if (FindDomainName(ie.Decl) == null) continue; - start.Add(ie.Decl); - } + AddAvailableVars(callCmd, start); } else if (cmd is ParCallCmd) { @@ -221,14 +255,7 @@ namespace Microsoft.Boogie } } availableLinearVars[parCallCmd] = new HashSet(start); - foreach (CallCmd callCmd in parCallCmd.CallCmds) - { - foreach (IdentifierExpr ie in callCmd.Outs) - { - if (FindDomainName(ie.Decl) == null) continue; - start.Add(ie.Decl); - } - } + AddAvailableVars(parCallCmd, start); } else if (cmd is HavocCmd) { @@ -254,9 +281,37 @@ namespace Microsoft.Boogie { if (globalVarToDomainName.ContainsKey(v)) return globalVarToDomainName[v]; - if (inoutParamToDomainName.ContainsKey(v)) - return inoutParamToDomainName[v]; - return QKeyValue.FindStringAttribute(v.Attributes, "linear"); + if (inParamToLinearQualifier.ContainsKey(v)) + return inParamToLinearQualifier[v].domainName; + if (outParamToDomainName.ContainsKey(v)) + return outParamToDomainName[v]; + string domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear"); + if (domainName != null) + return domainName; + return QKeyValue.FindStringAttribute(v.Attributes, "cnst"); + } + public LinearKind FindLinearKind(Variable v) + { + if (globalVarToDomainName.ContainsKey(v)) + return LinearKind.LINEAR; + if (inParamToLinearQualifier.ContainsKey(v)) + return inParamToLinearQualifier[v].kind; + if (outParamToDomainName.ContainsKey(v)) + return LinearKind.LINEAR; + + if (QKeyValue.FindStringAttribute(v.Attributes, "cnst") != null) + { + return LinearKind.CONST; + } + else if (QKeyValue.FindStringAttribute(v.Attributes, "linear") != null) + { + return LinearKind.LINEAR; + } + else + { + Debug.Assert(false); + return LinearKind.CONST; + } } public override Variable VisitVariable(Variable node) { @@ -364,6 +419,11 @@ namespace Microsoft.Boogie Error(node, "Only local linear variable can be an actual input parameter of a procedure call"); continue; } + if (FindLinearKind(formal) == LinearKind.LINEAR && FindLinearKind(actual.Decl) == LinearKind.CONST) + { + Error(node, "Only non-const linear variable can be an actual parameter to a non-const input parameter of a procedure call"); + continue; + } if (inVars.Contains(actual.Decl)) { Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name)); @@ -420,7 +480,7 @@ namespace Microsoft.Boogie return base.VisitParCallCmd(node); } - private IEnumerable AvailableLinearVars(Absy absy) + public IEnumerable AvailableLinearVars(Absy absy) { if (availableLinearVars.ContainsKey(absy)) return availableLinearVars[absy]; @@ -493,13 +553,13 @@ namespace Microsoft.Boogie Dictionary domainNameToExpr = new Dictionary(); foreach (var domainName in linearDomains.Keys) { - domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); + domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]); } foreach (Variable v in AvailableLinearVars(callCmd)) { var domainName = FindDomainName(v); var domain = linearDomains[domainName]; - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + IdentifierExpr ie = Expr.Ident(v); var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] }); expr.Resolve(new ResolutionContext(null)); @@ -634,9 +694,9 @@ namespace Microsoft.Boogie int count = 0; foreach (Variable v in scope) { - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + IdentifierExpr ie = Expr.Ident(v); Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new List{ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)) } ); - e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List { new IdentifierExpr(Token.NoToken, partition), e } ); + e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List { Expr.Ident(partition), e } ); e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e } ); e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.True })); disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr); @@ -648,6 +708,17 @@ namespace Microsoft.Boogie } } + public class LinearQualifier + { + public string domainName; + public LinearKind kind; + public LinearQualifier(string domainName, LinearKind kind) + { + this.domainName = domainName; + this.kind = kind; + } + } + public class LinearDomain { public Microsoft.Boogie.Type elementType; @@ -676,11 +747,11 @@ namespace Microsoft.Boogie else { BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool)); - IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); + IdentifierExpr aie = Expr.Ident(a); BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool)); - IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); + IdentifierExpr bie = Expr.Ident(b); BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + IdentifierExpr xie = Expr.Ident(x); var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new List { aie, bie } ); var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie } ); var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or, @@ -704,11 +775,11 @@ namespace Microsoft.Boogie else { BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool)); - IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); + IdentifierExpr aie = Expr.Ident(a); BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool)); - IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); + IdentifierExpr bie = Expr.Ident(b); BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + IdentifierExpr xie = Expr.Ident(x); var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new List { aie, bie }); var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie }); var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp, @@ -731,7 +802,7 @@ namespace Microsoft.Boogie else { BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + IdentifierExpr xie = Expr.Ident(x); var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List { Expr.True }), xie }); var trueAxiomExpr = new ForallExpr(Token.NoToken, new List { x }, trueTerm); @@ -755,11 +826,11 @@ namespace Microsoft.Boogie else { BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt)); - IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); + IdentifierExpr aie = Expr.Ident(a); BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt)); - IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); + IdentifierExpr bie = Expr.Ident(b); BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + IdentifierExpr xie = Expr.Ident(x); var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new List { aie, bie }); var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie }); var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq, @@ -782,9 +853,9 @@ namespace Microsoft.Boogie else { BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", Type.Int)); - IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); + IdentifierExpr aie = Expr.Ident(a); BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + IdentifierExpr xie = Expr.Ident(x); var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new List { aie }), xie }); var axiomExpr = new ForallExpr(Token.NoToken, new List { a, x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie)); axiomExpr.Typecheck(new TypecheckingContext(null)); diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 78943c1b..ce6a3cdf 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -114,15 +114,10 @@ namespace Microsoft.Boogie private ActionInfo first; // corresponds to that* private ActionInfo second; // corresponds to this* private Stack path; - private Expr transitionRelation; + private List paths; - public TransitionRelationComputation(Program program, ActionInfo second) + public TransitionRelationComputation(Program program, ActionInfo second) : this(program, null, second) { - this.program = program; - this.first = null; - this.second = second; - this.path = new Stack(); - this.transitionRelation = Expr.False; } public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second) @@ -131,27 +126,27 @@ namespace Microsoft.Boogie this.first = first; this.second = second; this.path = new Stack(); - this.transitionRelation = Expr.False; - } - - public Expr Compute() - { + this.paths = new List(); List havocVars = new List(); - second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v))); - second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v))); + this.second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v))); + this.second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v))); if (havocVars.Count > 0) { HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars); path.Push(havocCmd); } - Search(second.thisAction.Blocks[0], false); - return transitionRelation; + Search(this.second.thisAction.Blocks[0], false); } - private void Substitute(Dictionary map, ref Expr returnExpr, ref Dictionary varToExpr) + private void Substitute(Dictionary map, ref List pathExprs, ref Dictionary varToExpr) { Substitution subst = Substituter.SubstitutionFromHashtable(map); - returnExpr = Substituter.Apply(subst, returnExpr); + List oldPathExprs = pathExprs; + pathExprs = new List(); + foreach (Expr pathExpr in oldPathExprs) + { + pathExprs.Add(Substituter.Apply(subst, pathExpr)); + } Dictionary oldVarToExpr = varToExpr; varToExpr = new Dictionary(); foreach (Variable v in oldVarToExpr.Keys) @@ -164,18 +159,17 @@ namespace Microsoft.Boogie { public HashSet existsVars; public Dictionary varToExpr; - public Expr pathExpr; + public List pathExprs; - public PathInfo(HashSet existsVars, Dictionary varToExpr, Expr pathExpr) + public PathInfo(HashSet existsVars, Dictionary varToExpr, List pathExprs) { this.existsVars = existsVars; this.varToExpr = varToExpr; - this.pathExpr = pathExpr; + this.pathExprs = pathExprs; } } - private List paths = new List(); - private Expr CalculatePathCondition() + private void AddPath() { HashSet existsVars = new HashSet(); Dictionary varToExpr = new Dictionary(); @@ -194,14 +188,14 @@ namespace Microsoft.Boogie { varToExpr[v] = Expr.Ident(v); } - Expr pathExpr = Expr.True; + List pathExprs = new List(); int boundVariableCount = 0; foreach (Cmd cmd in path) { if (cmd is AssumeCmd) { AssumeCmd assumeCmd = cmd as AssumeCmd; - pathExpr = Expr.And(assumeCmd.Expr, pathExpr); + pathExprs.Add(assumeCmd.Expr); } else if (cmd is AssignCmd) { @@ -211,7 +205,7 @@ namespace Microsoft.Boogie { map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k]; } - Substitute(map, ref pathExpr, ref varToExpr); + Substitute(map, ref pathExprs, ref varToExpr); } else if (cmd is HavocCmd) { @@ -220,19 +214,25 @@ namespace Microsoft.Boogie foreach (IdentifierExpr ie in havocCmd.Vars) { BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, ie.Decl.TypedIdent.Type)); - map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv); + map[ie.Decl] = Expr.Ident(bv); existsVars.Add(bv); } - Substitute(map, ref pathExpr, ref varToExpr); + Substitute(map, ref pathExprs, ref varToExpr); } else { Debug.Assert(false); } } - paths.Add(new PathInfo(existsVars, varToExpr, pathExpr)); + paths.Add(new PathInfo(new HashSet(existsVars), varToExpr, pathExprs)); + } + private Expr CalculatePathCondition(PathInfo path) + { + HashSet existsVars = path.existsVars; Dictionary existsMap = new Dictionary(); + + Dictionary varToExpr = path.varToExpr; foreach (Variable v in varToExpr.Keys) { IdentifierExpr ie = varToExpr[v] as IdentifierExpr; @@ -242,17 +242,58 @@ namespace Microsoft.Boogie existsVars.Remove(ie.Decl); } } - pathExpr = (new MyDuplicator()).VisitExpr(pathExpr); + + List pathExprs = new List(); + path.pathExprs.ForEach(x => pathExprs.Add((new MyDuplicator()).VisitExpr(x))); + foreach (Expr x in pathExprs) + { + Variable boundVar; + Expr boundVarExpr; + if (InferSubstitution(x, out boundVar, out boundVarExpr) && existsVars.Contains(boundVar)) + { + existsMap[boundVar] = boundVarExpr; + existsVars.Remove(boundVar); + } + } + + Expr returnExpr = Expr.True; + pathExprs.ForEach(x => Expr.And(returnExpr, x)); foreach (Variable v in varToExpr.Keys) { - pathExpr = Expr.And(pathExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v]))); + returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v]))); } - pathExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), pathExpr); + returnExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), returnExpr); if (existsVars.Count > 0) { - pathExpr = new ExistsExpr(Token.NoToken, new List(existsVars), pathExpr); + returnExpr = new ExistsExpr(Token.NoToken, new List(existsVars), returnExpr); } - return pathExpr; + return returnExpr; + } + + bool InferSubstitution(Expr x, out Variable var, out Expr expr) + { + var = null; + expr = null; + NAryExpr naryExpr = x as NAryExpr; + if (naryExpr == null || naryExpr.Fun.FunctionName != "==") + { + return false; + } + IdentifierExpr arg0 = naryExpr.Args[0] as IdentifierExpr; + if (arg0 != null && arg0.Decl is BoundVariable) + { + var = arg0.Decl; + expr = naryExpr.Args[1]; + return true; + } + IdentifierExpr arg1 = naryExpr.Args[1] as IdentifierExpr; + if (arg1 != null && arg1.Decl is BoundVariable) + { + var = arg1.Decl; + expr = naryExpr.Args[0]; + return true; + } + return false; } public Expr LeftMoverCompute(Expr failureExpr) @@ -261,7 +302,22 @@ namespace Microsoft.Boogie foreach (PathInfo path in paths) { Expr expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(path.varToExpr), failureExpr); - expr = Expr.And(path.pathExpr, expr); + Dictionary subst = new Dictionary(); + foreach (Expr x in path.pathExprs) + { + Variable boundVar; + Expr boundVarExpr; + if (InferSubstitution(x, out boundVar, out boundVarExpr) && path.existsVars.Contains(boundVar)) + { + subst[boundVar] = boundVarExpr; + path.existsVars.Remove(boundVar); + } + else + { + expr = Expr.And(expr, x); + } + } + expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), expr); expr = new OldExpr(Token.NoToken, expr); if (path.existsVars.Count > 0) { @@ -272,6 +328,16 @@ namespace Microsoft.Boogie return returnExpr; } + public Expr TransitionRelationCompute() + { + Expr transitionRelation = Expr.False; + foreach (PathInfo path in paths) + { + transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition(path)); + } + return transitionRelation; + } + private void Search(Block b, bool inFirst) { int pathSizeAtEntry = path.Count; @@ -283,7 +349,7 @@ namespace Microsoft.Boogie { if (first == null || inFirst) { - transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition()); + AddPath(); } else { @@ -418,13 +484,13 @@ namespace Microsoft.Boogie blocks.AddRange(secondBlocks); List requires = DisjointnessRequires(program, first, second); List ensures = new List(); - Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).Compute(); + Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).TransitionRelationCompute(); Ensures ensureCheck = new Ensures(false, transitionRelation); ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name); ensures.Add(ensureCheck); string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name); List globalVars = new List(); - program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x))); + program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(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, blocks); impl.Proc = proc; @@ -461,7 +527,7 @@ namespace Microsoft.Boogie } string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); List globalVars = new List(); - program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x))); + program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(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; @@ -496,9 +562,7 @@ namespace Microsoft.Boogie requires.Add(new Requires(false, assertCmd.Expr)); } - TransitionRelationComputation transitionRelationComputation = new TransitionRelationComputation(program, second); - transitionRelationComputation.Compute(); - Expr ensuresExpr = transitionRelationComputation.LeftMoverCompute(failureExpr); + Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(failureExpr); List ensures = new List(); Ensures ensureCheck = new Ensures(false, ensuresExpr); ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name); @@ -508,7 +572,7 @@ namespace Microsoft.Boogie blocks.Add(new Block(Token.NoToken, "L", new List(), new ReturnCmd(Token.NoToken))); 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))); + program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x))); Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, new List(), requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, new List(), new List(), blocks); impl.Proc = proc; diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 435e72bf..d9f23cb3 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -253,7 +253,7 @@ namespace Microsoft.Boogie globalMods = new List(); foreach (Variable g in program.GlobalVariables()) { - globalMods.Add(new IdentifierExpr(Token.NoToken, g)); + globalMods.Add(Expr.Ident(g)); } asyncAndParallelCallDesugarings = new Dictionary(); yieldCheckerProcs = new List(); @@ -261,9 +261,9 @@ namespace Microsoft.Boogie yieldProc = null; } - private HashSet AvailableLinearVars(Absy absy) + private IEnumerable AvailableLinearVars(Absy absy) { - return linearTypeChecker.availableLinearVars[absyMap[absy]]; + return linearTypeChecker.AvailableLinearVars(absyMap[absy]); } private void AddCallToYieldProc(IToken tok, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) @@ -328,12 +328,12 @@ namespace Microsoft.Boogie } } - private Dictionary ComputeAvailableExprs(HashSet availableLinearVars, Dictionary domainNameToInputVar) + private Dictionary ComputeAvailableExprs(IEnumerable availableLinearVars, Dictionary domainNameToInputVar) { Dictionary domainNameToExpr = new Dictionary(); foreach (var domainName in linearTypeChecker.linearDomains.Keys) { - var expr = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); + var expr = Expr.Ident(domainNameToInputVar[domainName]); expr.Resolve(new ResolutionContext(null)); expr.Typecheck(new TypecheckingContext(null)); domainNameToExpr[domainName] = expr; @@ -342,7 +342,7 @@ namespace Microsoft.Boogie { var domainName = linearTypeChecker.FindDomainName(v); var domain = linearTypeChecker.linearDomains[domainName]; - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + IdentifierExpr ie = Expr.Ident(v); var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] }); expr.Resolve(new ResolutionContext(null)); expr.Typecheck(new TypecheckingContext(null)); @@ -357,13 +357,13 @@ namespace Microsoft.Boogie List rhss = new List(); foreach (var domainName in linearTypeChecker.linearDomains.Keys) { - lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName]))); + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); rhss.Add(domainNameToExpr[domainName]); } foreach (Variable g in ogOldGlobalMap.Keys) { lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); - rhss.Add(new IdentifierExpr(Token.NoToken, g)); + rhss.Add(Expr.Ident(g)); } if (lhss.Count > 0) { @@ -446,13 +446,13 @@ namespace Microsoft.Boogie { Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true); inParams.Add(y); - map[x] = new IdentifierExpr(Token.NoToken, y); + map[x] = Expr.Ident(y); } foreach (Variable x in callCmd.Proc.OutParams) { Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), false); outParams.Add(y); - map[x] = new IdentifierExpr(Token.NoToken, y); + map[x] = Expr.Ident(y); } Contract.Assume(callCmd.Proc.TypeParameters.Count == 0); Substitution subst = Substituter.SubstitutionFromHashtable(map); @@ -488,7 +488,7 @@ namespace Microsoft.Boogie Variable inParam = proc.InParams[i]; Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type)); locals.Add(copy); - map[proc.InParams[i]] = new IdentifierExpr(Token.NoToken, copy); + map[proc.InParams[i]] = Expr.Ident(copy); } { int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count; @@ -497,7 +497,7 @@ namespace Microsoft.Boogie Variable inParam = proc.InParams[i]; Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true); inputs.Add(copy); - map[proc.InParams[i]] = new IdentifierExpr(Token.NoToken, copy); + map[proc.InParams[i]] = Expr.Ident(copy); i++; } } @@ -507,7 +507,7 @@ namespace Microsoft.Boogie Variable outParam = proc.OutParams[i]; var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type)); locals.Add(copy); - map[proc.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy); + map[proc.OutParams[i]] = Expr.Ident(copy); } foreach (IdentifierExpr ie in globalMods) { @@ -594,7 +594,7 @@ namespace Microsoft.Boogie Variable inParam = decl.InParams[i]; Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type)); locals.Add(copy); - map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy); + map[decl.InParams[i]] = Expr.Ident(copy); } { int i = decl.InParams.Count - linearTypeChecker.linearDomains.Count; @@ -603,7 +603,7 @@ namespace Microsoft.Boogie Variable inParam = decl.InParams[i]; Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true); inputs.Add(copy); - map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy); + map[decl.InParams[i]] = Expr.Ident(copy); i++; } } @@ -612,7 +612,7 @@ namespace Microsoft.Boogie Variable outParam = decl.OutParams[i]; var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type)); locals.Add(copy); - map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy); + map[decl.OutParams[i]] = Expr.Ident(copy); } Dictionary ogOldLocalMap = new Dictionary(); Dictionary assumeMap = new Dictionary(map); @@ -740,7 +740,7 @@ namespace Microsoft.Boogie foreach (Variable local in impl.LocVars) { var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); - map[local] = new IdentifierExpr(Token.NoToken, copy); + map[local] = Expr.Ident(copy); } Dictionary ogOldGlobalMap = new Dictionary(); foreach (IdentifierExpr ie in globalMods) @@ -777,7 +777,7 @@ namespace Microsoft.Boogie foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); } Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); - Expr betaExpr = new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo).Compute(); + Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo)).TransitionRelationCompute(); beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); Expr alphaExpr = Expr.True; foreach (AssertCmd assertCmd in actionInfo.thisGate) @@ -868,11 +868,7 @@ namespace Microsoft.Boogie if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) { HashSet availableLinearVars = new HashSet(AvailableLinearVars(callCmd)); - foreach (IdentifierExpr ie in callCmd.Outs) - { - if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue; - availableLinearVars.Add(ie.Decl); - } + linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars); Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); } @@ -888,14 +884,7 @@ namespace Microsoft.Boogie newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Or(Expr.Ident(pc), alpha))); } HashSet availableLinearVars = new HashSet(AvailableLinearVars(parCallCmd)); - foreach (CallCmd callCmd in parCallCmd.CallCmds) - { - foreach (IdentifierExpr ie in callCmd.Outs) - { - if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue; - availableLinearVars.Add(ie.Decl); - } - } + linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars); Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); } @@ -966,7 +955,7 @@ namespace Microsoft.Boogie } foreach (Variable v in ogOldGlobalMap.Keys) { - newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), Expr.Ident(ogOldGlobalMap[v])))); + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v])))); } newCmds.AddRange(header.Cmds); header.Cmds = newCmds; @@ -986,7 +975,7 @@ namespace Microsoft.Boogie Dictionary domainNameToExpr = new Dictionary(); foreach (var domainName in linearTypeChecker.linearDomains.Keys) { - domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); + domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]); } for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) { @@ -994,12 +983,12 @@ namespace Microsoft.Boogie var domainName = linearTypeChecker.FindDomainName(v); if (domainName == null) continue; var domain = linearTypeChecker.linearDomains[domainName]; - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + IdentifierExpr ie = Expr.Ident(v); domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] }); } foreach (string domainName in linearTypeChecker.linearDomains.Keys) { - lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName]))); + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); rhss.Add(domainNameToExpr[domainName]); } foreach (Variable g in ogOldGlobalMap.Keys) @@ -1151,7 +1140,7 @@ namespace Microsoft.Boogie List exprSeq = new List(); foreach (Variable v in inputs) { - exprSeq.Add(new IdentifierExpr(Token.NoToken, v)); + exprSeq.Add(Expr.Ident(v)); } CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List()); callCmd.Proc = proc; diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 2e7881f6..a3e35a70 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -90,20 +90,20 @@ namespace Microsoft.Boogie this.thisInParams.Add(x); Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes); this.thatInParams.Add(y); - map[x] = new IdentifierExpr(Token.NoToken, y); + map[x] = Expr.Ident(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, x.Attributes); this.thatOutParams.Add(y); - map[x] = new IdentifierExpr(Token.NoToken, y); + map[x] = Expr.Ident(y); } List thatLocVars = new List(); 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); + map[x] = Expr.Ident(y); thatLocVars.Add(y); } Contract.Assume(proc.TypeParameters.Count == 0); -- cgit v1.2.3