diff --git a/Source/Concurrency/ActionRefinement.cs b/Source/Concurrency/ActionRefinement.cs new file mode 100644 index 000000000..a1bb98d8a --- /dev/null +++ b/Source/Concurrency/ActionRefinement.cs @@ -0,0 +1,70 @@ +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Boogie +{ + public class ActionRefinement + { + private CivlTypeChecker civlTypeChecker; + private Action targetAction; + private Implementation inlinedImpl; + + public static void AddCheckers(CivlTypeChecker civlTypeChecker, List decls) + { + foreach (var x in civlTypeChecker.ActionRefinements) + { + decls.AddRange([x.inlinedImpl, x.inlinedImpl.Proc]); + } + } + + public ActionRefinement(CivlTypeChecker civlTypeChecker, Action targetAction) + { + this.civlTypeChecker = civlTypeChecker; + this.targetAction = targetAction; + inlinedImpl = CreateInlinedImplementation(); + var refinedAction = targetAction.RefinedAction; + Dictionary map = new Dictionary(); + for (int i = 0; i < refinedAction.Impl.InParams.Count; i++) + { + map[refinedAction.Impl.InParams[i]] = Expr.Ident(inlinedImpl.Proc.InParams[i]); + } + for (int i = 0; i < refinedAction.Impl.OutParams.Count; i++) + { + map[refinedAction.Impl.OutParams[i]] = Expr.Ident(inlinedImpl.Proc.OutParams[i]); + } + var subst = Substituter.SubstitutionFromDictionary(map); + inlinedImpl.Proc.Requires = refinedAction.Gate.Select(g => new Requires(false, Substituter.Apply(subst, g.Expr))).ToList(); + var frame = new HashSet(civlTypeChecker.GlobalVariablesAtLayer(targetAction.LayerRange.UpperLayer)); + inlinedImpl.Proc.Ensures = new List(new[] + { + new Ensures(false, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame))) + { Description = new FailureOnlyDescription($"Refinement check of {targetAction.Name} failed") } + }); + } + + private Implementation CreateInlinedImplementation() + { + var decls = new List(); + var inlinedImpl = Action.CreateDuplicateImplementation(targetAction.ActionDecl.Impl, + $"{targetAction.ActionDecl.Name}_RefinementCheck"); + CivlAttributes.RemoveAttributes(inlinedImpl.Proc, new HashSet { "inline" }); + decls.Add(inlinedImpl); + decls.Add(inlinedImpl.Proc); + var oldTopLevelDeclarations = new List(civlTypeChecker.program.TopLevelDeclarations); + civlTypeChecker.program.AddTopLevelDeclarations(decls); + decls.OfType().ForEach(impl => + { + impl.OriginalBlocks = impl.Blocks; + impl.OriginalLocVars = impl.LocVars; + }); + Inliner.ProcessImplementation(civlTypeChecker.Options, civlTypeChecker.program, inlinedImpl); + civlTypeChecker.program.TopLevelDeclarations = oldTopLevelDeclarations; + decls.OfType().ForEach(impl => + { + impl.OriginalBlocks = null; + impl.OriginalLocVars = null; + }); + return inlinedImpl; + } + } +} \ No newline at end of file diff --git a/Source/Concurrency/CivlCoreTypes.cs b/Source/Concurrency/CivlCoreTypes.cs index cd1186a5d..cc3ccdc53 100644 --- a/Source/Concurrency/CivlCoreTypes.cs +++ b/Source/Concurrency/CivlCoreTypes.cs @@ -1,5 +1,4 @@ using System.Collections.Generic; -using System.Diagnostics; using System.Linq; namespace Microsoft.Boogie @@ -20,36 +19,12 @@ public class Action public List SecondGate; public Implementation SecondImpl; public Dictionary TriggerFunctions; - - public DatatypeTypeCtorDecl ChoiceDatatypeTypeCtorDecl; - public Implementation ImplWithChoice; - public Function InputOutputRelationWithChoice; - public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action refinedAction, bool isInvariant) + public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action refinedAction) { ActionDecl = actionDecl; RefinedAction = refinedAction; Impl = CreateDuplicateImplementation(actionDecl.Impl, actionDecl.Name); - if (PendingAsyncs.Any()) - { - DesugarCreateAsyncs(civlTypeChecker, Impl, ActionDecl); - if (isInvariant) - { - ImplWithChoice = CreateDuplicateImplementation(Impl, $"{Name}_With_Choice"); - var choiceDatatypeName = $"Choice_{Name}"; - ChoiceDatatypeTypeCtorDecl = - new DatatypeTypeCtorDecl(Token.NoToken, choiceDatatypeName, new List(), null); - PendingAsyncs.ForEach(elim => - { - var field = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType), true); - ChoiceDatatypeTypeCtorDecl.AddConstructor(Token.NoToken, $"{choiceDatatypeName}_{elim.Name}", - new List() { field }); - }); - civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl); - DesugarSetChoice(civlTypeChecker, ImplWithChoice); - } - DropSetChoice(Impl); - } AddGateSufficiencyCheckerAndHoistAsserts(civlTypeChecker); @@ -58,10 +33,6 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref UsedGlobalVarsInAction = new HashSet(VariableCollector.Collect(Impl).Where(x => x is GlobalVariable)); InputOutputRelation = ComputeInputOutputRelation(civlTypeChecker, Impl); - if (ImplWithChoice != null) - { - InputOutputRelationWithChoice = ComputeInputOutputRelation(civlTypeChecker, ImplWithChoice); - } AtomicActionDuplicator.SetupCopy(this, ref FirstGate, ref FirstImpl, "first_"); AtomicActionDuplicator.SetupCopy(this, ref SecondGate, ref SecondImpl, "second_"); @@ -76,10 +47,6 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref public LayerRange LayerRange => ActionDecl.LayerRange; - public IEnumerable PendingAsyncs => ActionDecl.CreateActionDecls; - - public bool HasPendingAsyncs => PendingAsyncs.Any(); - public bool IsRightMover => ActionDecl.MoverType == MoverType.Right || ActionDecl.MoverType == MoverType.Both; public bool IsLeftMover => ActionDecl.MoverType == MoverType.Left || ActionDecl.MoverType == MoverType.Both; @@ -88,27 +55,14 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref public bool IsUnconditionalLeftMover => IsLeftMover && !ActionDecl.HasPreconditions; - public int PendingAsyncStartIndex => ActionDecl.OutParams.Count; - public bool TriviallyCommutesWith(Action other) { return !this.ModifiedGlobalVars.Intersect(other.UsedGlobalVarsInAction).Any() && !this.UsedGlobalVarsInAction.Intersect(other.ModifiedGlobalVars).Any(); } - public Variable PAs(CtorType pendingAsyncType) - { - var pendingAsyncMultisetType = TypeHelper.MapType(pendingAsyncType, Type.Int); - return Impl.OutParams.Skip(PendingAsyncStartIndex).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType)); - } - public bool HasAssumeCmd => Impl.Blocks.Any(b => b.Cmds.Any(c => c is AssumeCmd)); - public DatatypeConstructor ChoiceConstructor(CtorType pendingAsyncType) - { - return ChoiceDatatypeTypeCtorDecl.Constructors.First(x => x.InParams[0].TypedIdent.Type.Equals(pendingAsyncType)); - } - public IEnumerable GetGateAsserts(Substitution subst, string msg) { foreach (var gate in Gate) @@ -124,30 +78,6 @@ public Expr GetTransitionRelation(CivlTypeChecker civlTypeChecker, HashSet map = new Dictionary(); - for (int i = 0; i < Impl.InParams.Count; i++) - { - map[Impl.InParams[i]] = Expr.Ident(to.Impl.InParams[i]); - } - for (int i = 0; i < PendingAsyncStartIndex; i++) - { - map[Impl.OutParams[i]] = Expr.Ident(to.Impl.OutParams[i]); - } - for (int i = PendingAsyncStartIndex; i < Impl.OutParams.Count; i++) - { - var formal = Impl.OutParams[i]; - var pendingAsyncType = (CtorType)((MapType)formal.TypedIdent.Type).Arguments[0]; - map[formal] = Expr.Ident(to.PAs(pendingAsyncType)); - } - return Substituter.SubstitutionFromDictionary(map); - } - public IEnumerable Preconditions(int layerNum, Substitution subst) { var errorMessage = $"this precondition of {Name} could not be proved"; @@ -265,133 +195,6 @@ private Function ComputeInputOutputRelation(CivlTypeChecker civlTypeChecker, Imp CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, inputOutputRelation.Body); return inputOutputRelation; } - - public static void DesugarCreateAsyncs(CivlTypeChecker civlTypeChecker, Implementation impl, ActionDecl actionDecl) - { - Debug.Assert(impl.OutParams.Count == actionDecl.OutParams.Count); - var pendingAsyncTypeToActionDecl = new Dictionary(); - var lhss = new List(); - var rhss = new List(); - actionDecl.CreateActionDecls.ForEach(decl => - { - pendingAsyncTypeToActionDecl[decl.PendingAsyncType] = decl; - var pa = civlTypeChecker.Formal($"PAs_{decl.Name}", decl.PendingAsyncMultisetType, false); - impl.Proc.OutParams.Add(pa); - impl.OutParams.Add(pa); - lhss.Add(Expr.Ident(pa)); - rhss.Add(ExprHelper.FunctionCall(decl.PendingAsyncConst, Expr.Literal(0))); - }); - var tc = new TypecheckingContext(null, civlTypeChecker.Options); - var initAssignCmd = CmdHelper.AssignCmd(lhss, rhss); - initAssignCmd.Typecheck(tc); - impl.Blocks[0].Cmds.Insert(0, initAssignCmd); - impl.Blocks.ForEach(block => - { - var newCmds = new List(); - foreach (var cmd in block.Cmds) - { - if (cmd is CallCmd callCmd) - { - var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(callCmd.Proc); - if (callCmd.IsAsync) - { - var actionDecl = (ActionDecl)callCmd.Proc; - var pendingAsyncMultiset = - Expr.Store( - ExprHelper.FunctionCall(actionDecl.PendingAsyncConst, Expr.Literal(0)), - ExprHelper.FunctionCall(actionDecl.PendingAsyncCtor, callCmd.Ins), - Expr.Literal(1)); - var pendingAsyncMultisetType = TypeHelper.MapType(actionDecl.PendingAsyncType, Type.Int); - var pendingAsyncCollector = impl.OutParams.Skip(actionDecl.OutParams.Count).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType)); - var updateAssignCmd = CmdHelper.AssignCmd(pendingAsyncCollector, - ExprHelper.FunctionCall(actionDecl.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), pendingAsyncMultiset)); - updateAssignCmd.Typecheck(tc); - newCmds.Add(updateAssignCmd); - continue; - } - else if (originalProc.Name == "create_asyncs" || originalProc.Name == "create_multi_asyncs") - { - var pendingAsyncType = - (CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; - var pendingAsync = pendingAsyncTypeToActionDecl[pendingAsyncType]; - var pendingAsyncMultiset = originalProc.Name == "create_asyncs" - ? ExprHelper.FunctionCall(pendingAsync.PendingAsyncIte, callCmd.Ins[0], - ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(1)), - ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0))) - : callCmd.Ins[0]; - var pendingAsyncMultisetType = TypeHelper.MapType(pendingAsyncType, Type.Int); - var pendingAsyncCollector = impl.OutParams.Skip(actionDecl.OutParams.Count).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType)); - var updateAssignCmd = CmdHelper.AssignCmd(pendingAsyncCollector, - ExprHelper.FunctionCall(pendingAsync.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), pendingAsyncMultiset)); - updateAssignCmd.Typecheck(tc); - newCmds.Add(updateAssignCmd); - continue; - } - } - newCmds.Add(cmd); - } - block.Cmds = newCmds; - }); - } - - private void DropSetChoice(Implementation impl) - { - impl.Blocks.ForEach(block => - { - var newCmds = new List(); - foreach (var cmd in block.Cmds) - { - if (cmd is CallCmd callCmd) - { - var originalProcName = Monomorphizer.GetOriginalDecl(callCmd.Proc).Name; - if (originalProcName == "set_choice") - { - continue; - } - } - newCmds.Add(cmd); - } - block.Cmds = newCmds; - }); - } - - private void DesugarSetChoice(CivlTypeChecker civlTypeChecker, Implementation impl) - { - var choice = civlTypeChecker.Formal("choice", TypeHelper.CtorType(ChoiceDatatypeTypeCtorDecl), false); - impl.Proc.OutParams.Add(choice); - impl.OutParams.Add(choice); - impl.Blocks.ForEach(block => - { - var newCmds = new List(); - foreach (var cmd in block.Cmds) - { - if (cmd is CallCmd callCmd) - { - var originalProcName = Monomorphizer.GetOriginalDecl(callCmd.Proc).Name; - if (originalProcName == "set_choice") - { - var pendingAsyncType = (CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; - var pendingAsync = PendingAsyncs.First(decl => decl.PendingAsyncType.Equals(pendingAsyncType)); - var tc = new TypecheckingContext(null, civlTypeChecker.Options); - var emptyExpr = Expr.Eq(Expr.Ident(PAs(pendingAsyncType)), - ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0))); - var memberExpr = Expr.Gt(Expr.Select(Expr.Ident(PAs(pendingAsyncType)), callCmd.Ins[0]), - Expr.Literal(0)); - var assertCmd = CmdHelper.AssertCmd(cmd.tok, Expr.Or(emptyExpr, memberExpr), - "Choice is not a created pending async"); - assertCmd.Typecheck(tc); - newCmds.Add(assertCmd); - var assignCmd = CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(Expr.Ident(choice), pendingAsyncType.Decl.Name), callCmd.Ins[0]); - assignCmd.Typecheck(tc); - newCmds.Add(assignCmd); - continue; - } - } - newCmds.Add(cmd); - } - block.Cmds = newCmds; - }); - } private void DeclareTriggerFunctions() { diff --git a/Source/Concurrency/CivlRewriter.cs b/Source/Concurrency/CivlRewriter.cs index 2979a379b..446f4c7a0 100644 --- a/Source/Concurrency/CivlRewriter.cs +++ b/Source/Concurrency/CivlRewriter.cs @@ -29,11 +29,6 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp civlTypeChecker.AtomicActions.ForEach(x => { decls.AddRange(new Declaration[] { x.Impl, x.Impl.Proc, x.InputOutputRelation }); - if (x.ImplWithChoice != null) - { - decls.AddRange(new Declaration[] - { x.ImplWithChoice, x.ImplWithChoice.Proc, x.InputOutputRelationWithChoice }); - } }); // Commutativity checks @@ -51,10 +46,7 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp if (!options.TrustRefinement) { YieldingProcChecker.AddRefinementCheckers(civlTypeChecker, decls); - if (!options.TrustSequentialization) - { - Sequentialization.AddCheckers(civlTypeChecker, decls); - } + ActionRefinement.AddCheckers(civlTypeChecker, decls); } foreach (var action in civlTypeChecker.AtomicActions) diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index 43edf6619..2e689d592 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -14,8 +14,7 @@ public class CivlTypeChecker public ActionDecl SkipActionDecl; private Dictionary actionDeclToAction; - private List sequentializations; - private Dictionary> implToPendingAsyncCollectors; + private List actionRefinements; private string namePrefix; public CivlTypeChecker(ConcurrencyOptions options, Program program) @@ -34,8 +33,7 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program) .OrderBy(layer => layer).Distinct().ToList(); this.actionDeclToAction = new Dictionary(); - this.sequentializations = new List(); - this.implToPendingAsyncCollectors = new Dictionary>(); + this.actionRefinements = new List(); IEnumerable declNames = program.TopLevelDeclarations.OfType().Select(x => x.Name); IEnumerable localVarNames = VariableNameCollector.Collect(program); @@ -52,9 +50,9 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program) } SkipActionDecl = new ActionDecl(Token.NoToken, AddNamePrefix("Skip"), MoverType.Both, new List(), - new List(), true, new List(), null, null, + new List(), true, null, new List(), new List(), new List(), new List(), - null, null); + null); var skipImplementation = DeclHelper.Implementation( SkipActionDecl, new List(), @@ -105,7 +103,7 @@ public void TypeCheck() { return; } - + var actionDecls = TypeCheckActions(); if (checkingContext.ErrorCount > 0) { @@ -120,7 +118,7 @@ public void TypeCheck() InlineAtomicActions(actionDecls); CreateAtomicActions(actionDecls); - CreateSequentializations(actionDecls); + CreateActionRefinements(actionDecls); AttributeEraser.Erase(this); YieldSufficiencyChecker.TypeCheck(this); } @@ -168,6 +166,7 @@ public static List InlineYieldEnsures(YieldProcedureDecl yieldProcedure } return ensures; } + private HashSet TypeCheckActions() { var actionDecls = program.Procedures.OfType().ToHashSet(); @@ -188,103 +187,11 @@ private HashSet TypeCheckActions() } actionDecls.Where(proc => proc.RefinedAction != null).ForEach(actionDecl => { - SignatureMatcher.CheckSequentializationSignature(actionDecl, actionDecl.RefinedAction.ActionDecl, - checkingContext); - if (actionDecl.InvariantAction != null) - { - SignatureMatcher.CheckSequentializationSignature(actionDecl, actionDecl.InvariantAction.ActionDecl, - checkingContext); - } + SignatureMatcher.CheckActionRefinementSignature(actionDecl, actionDecl.RefinedAction.ActionDecl, checkingContext); }); - actionDecls.Where(x => x.RefinedAction != null && x.InvariantAction == null) - .ForEach(x => TypeCheckInlineSequentializations(x)); return actionDecls; } - private void TypeCheckInlineSequentializations(ActionDecl actionDecl) - { - // compute eliminated actions and check that there is no async call cycle among eliminated actions - var refinedActionCreates = new HashSet(actionDecl.RefinedAction.ActionDecl.CreateActionDecls); - var refinedActionCreateNames = refinedActionCreates.Select(x => x.Name).ToHashSet(); - var stack = new Stack(); - var frontier = new HashSet(); // hashset representation of stack for efficient membership check - var visited = new HashSet(); - void Push(ActionDecl item) - { - stack.Push(item); - frontier.Add(item); - } - void Pop(ActionDecl item) - { - stack.Pop(); - frontier.Remove(item); - } - - Push(actionDecl); - while (stack.Count != 0) - { - var item = stack.Peek(); - if (visited.Contains(item)) - { - Pop(item); - continue; - } - CheckAsyncToSyncSafety(item, refinedActionCreateNames); - visited.Add(item); - var hitOnStack = item.CreateActionDecls.FirstOrDefault(x => frontier.Contains(x)); - if (hitOnStack != null) - { - var callCycle = stack.TakeWhile(elem => elem != hitOnStack).Append(hitOnStack).Select(elem => elem.Name); - Error(actionDecl, $"async call cycle detected: {string.Join(",", callCycle)}"); - break; - } - Pop(item); - item.CreateActionDecls.Except(refinedActionCreates).ForEach(Push); - } - } - - private void CheckAsyncToSyncSafety(ActionDecl actionDecl, HashSet refinedActionCreateNames) - { - actionDecl.Impl.Blocks.SelectMany(block => block.Cmds.OfType().Where(callCmd => - callCmd.Proc.OriginalDeclWithFormals is { Name: "create_asyncs" or "create_multi_asyncs" })).ForEach(callCmd => - { - var pendingAsyncType = (CtorType)program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; - if (!refinedActionCreateNames.Contains(pendingAsyncType.Decl.Name)) - { - Error(callCmd, "unable to eliminate unbounded pending asyncs without invariant specification"); - } - }); - - var graph = Program.GraphFromImpl(actionDecl.Impl, false); - var blocksLeadingToModifiedGlobals = new HashSet(); - graph.TopologicalSort().ForEach(block => - { - var modifiedGlobals = block.TransferCmd is GotoCmd gotoCmd && - gotoCmd.LabelTargets.Any(x => blocksLeadingToModifiedGlobals.Contains(x)); - for (int i = block.Cmds.Count - 1; 0 <= i; i--) - { - var cmd = block.Cmds[i]; - if (modifiedGlobals && cmd is CallCmd callCmd && callCmd.IsAsync) - { - var pendingAsyncType = (CtorType)program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; - if (!refinedActionCreateNames.Contains(pendingAsyncType.Decl.Name)) - { - Error(callCmd, "unable to eliminate pending async since a global is modified subsequently"); - } - } - var assignedVariables = cmd.GetAssignedVariables().ToList(); - if (assignedVariables.OfType().Any()) - { - modifiedGlobals = true; - } - } - if (modifiedGlobals) - { - blocksLeadingToModifiedGlobals.Add(block); - } - }); - } - private void TypeCheckYieldingProcedures() { foreach (var yieldingProc in program.Procedures.OfType()) @@ -299,42 +206,6 @@ private void TypeCheckYieldingProcedures() SignatureMatcher.CheckRefinementSignature(yieldingProc, checkingContext); } } - - // local collectors for pending asyncs - var pendingAsyncProcs = program.TopLevelDeclarations.OfType() - .Where(proc => proc.MaybePendingAsync).Select(proc => proc.Name).ToHashSet(); - var pendingAsyncMultisetTypes = program.TopLevelDeclarations.OfType() - .Where(decl => pendingAsyncProcs.Contains(decl.Name)).Select(decl => - TypeHelper.MapType(TypeHelper.CtorType(decl), Type.Int)).ToHashSet(); - foreach (Implementation impl in program.Implementations.Where(impl => impl.Proc is YieldProcedureDecl)) - { - var proc = (YieldProcedureDecl)impl.Proc; - implToPendingAsyncCollectors[impl] = new Dictionary(); - foreach (Variable v in impl.LocVars.Where(v => v.HasAttribute(CivlAttributes.PENDING_ASYNC))) - { - if (!pendingAsyncMultisetTypes.Contains(v.TypedIdent.Type)) - { - Error(v, "pending async collector is of incorrect type"); - } - else if (v.LayerRange.LowerLayer != proc.Layer) - { - Error(v, "pending async collector must be introduced at the layer of the enclosing procedure"); - } - else - { - var mapType = (MapType)v.TypedIdent.Type; - var ctorType = (CtorType)mapType.Arguments[0]; - if (implToPendingAsyncCollectors[impl].ContainsKey(ctorType)) - { - Error(v, "duplicate pending async collector"); - } - else - { - implToPendingAsyncCollectors[impl][ctorType] = v; - } - } - } - } } private void InlineAtomicActions(HashSet actionDecls) @@ -378,50 +249,35 @@ private void InlineAtomicActions(HashSet actionDecls) private void CreateAtomicActions(HashSet actionDecls) { - var invariantActionDecls = actionDecls.Where(decl => decl.InvariantAction != null) - .Select(decl => decl.InvariantAction.ActionDecl).ToHashSet(); - - // Initialize ActionDecls so that all the pending async machinery is set up. - actionDecls.ForEach(proc => proc.Initialize(program.monomorphizer)); - // Create all actions that do not refine another action. foreach (var actionDecl in actionDecls.Where(proc => proc.RefinedAction == null)) { - actionDeclToAction[actionDecl] = new Action(this, actionDecl, null, invariantActionDecls.Contains(actionDecl)); + actionDeclToAction[actionDecl] = new Action(this, actionDecl, null); } // Create all atomic actions that refine other actions. - actionDecls.Where(proc => proc.RefinedAction != null) - .ForEach(decl => CreateActionsThatRefineAnotherAction(decl, invariantActionDecls)); + actionDecls.Where(proc => proc.RefinedAction != null).ForEach(decl => CreateActionsThatRefineAnotherAction(decl)); } - private void CreateActionsThatRefineAnotherAction(ActionDecl actionDecl, HashSet invariantActionDecls) + private void CreateActionsThatRefineAnotherAction(ActionDecl actionDecl) { if (actionDeclToAction.ContainsKey(actionDecl)) { return; } - var refinedProc = actionDecl.RefinedAction.ActionDecl; - CreateActionsThatRefineAnotherAction(refinedProc, invariantActionDecls); - var refinedAction = actionDeclToAction[refinedProc]; + var refinedActionDecl = actionDecl.RefinedAction.ActionDecl; + CreateActionsThatRefineAnotherAction(refinedActionDecl); + var refinedAction = actionDeclToAction[refinedActionDecl]; actionDeclToAction[actionDecl] = - new Action(this, actionDecl, refinedAction, invariantActionDecls.Contains(actionDecl)); + new Action(this, actionDecl, refinedAction); } - private void CreateSequentializations(HashSet actionDecls) + private void CreateActionRefinements(HashSet actionDecls) { actionDecls.Where(actionDecl => actionDecl.RefinedAction != null).ForEach(actionDecl => { var action = actionDeclToAction[actionDecl]; - if (actionDecl.InvariantAction == null) - { - sequentializations.Add(new InlineSequentialization(this, action)); - } - else - { - var invariantActionDecl = actionDecl.InvariantAction.ActionDecl; - sequentializations.Add(new InductiveSequentialization(this, action, actionDeclToAction[invariantActionDecl])); - } + actionRefinements.Add(new ActionRefinement(this, action)); }); } @@ -439,7 +295,7 @@ public static void CheckRefinementSignature(YieldProcedureDecl proc, CheckingCon signatureMatcher.MatchFormals(procOutParams, actionOutParams, SignatureMatcher.OUT); } - public static void CheckSequentializationSignature(Procedure original, Procedure abstraction, CheckingContext checkingContext) + public static void CheckActionRefinementSignature(Procedure original, Procedure abstraction, CheckingContext checkingContext) { // Input and output parameters have to match exactly var signatureMatcher = new SignatureMatcher(original, abstraction, checkingContext); @@ -512,12 +368,7 @@ public Action Action(ActionDecl actionDecl) return actionDeclToAction[actionDecl]; } - public IEnumerable Sequentializations => sequentializations; - - public Dictionary PendingAsyncCollectors(Implementation impl) - { - return implToPendingAsyncCollectors[impl]; - } + public IEnumerable ActionRefinements => actionRefinements; public void Error(Absy node, string message) { diff --git a/Source/Concurrency/ConcurrencyOptions.cs b/Source/Concurrency/ConcurrencyOptions.cs index 5936f8da0..1e1abe454 100644 --- a/Source/Concurrency/ConcurrencyOptions.cs +++ b/Source/Concurrency/ConcurrencyOptions.cs @@ -3,7 +3,6 @@ namespace Microsoft.Boogie; public interface ConcurrencyOptions : CoreOptions { bool TrustMoverTypes { get; } - bool TrustSequentialization { get; } int TrustLayersDownto { get; } int TrustLayersUpto { get; } bool TrustNoninterference { get; } diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs deleted file mode 100644 index b342be395..000000000 --- a/Source/Concurrency/InductiveSequentialization.cs +++ /dev/null @@ -1,385 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using Microsoft.Boogie.GraphUtil; - -namespace Microsoft.Boogie -{ - public abstract class Sequentialization - { - protected CivlTypeChecker civlTypeChecker; - protected Action targetAction; - protected HashSet eliminatedActions; - - protected Sequentialization(CivlTypeChecker civlTypeChecker, Action targetAction) - { - this.civlTypeChecker = civlTypeChecker; - this.targetAction = targetAction; - this.eliminatedActions = new HashSet(EliminatedActionDecls.Select(x => civlTypeChecker.Action(x))); - } - - public IEnumerable EliminatedActionDecls => targetAction.ActionDecl.EliminatedActionDecls(); - - public IEnumerable EliminatedActions => eliminatedActions; - - public int Layer => targetAction.LayerRange.UpperLayer; - - protected virtual List GenerateCheckers() - { - return new List(); - } - - public static void AddCheckers(CivlTypeChecker civlTypeChecker, List decls) - { - foreach (var x in civlTypeChecker.Sequentializations) - { - decls.AddRange(x.GenerateCheckers()); - } - } - - protected AssertCmd GetCheck(IToken tok, Expr expr, string msg) - { - expr.Typecheck(new TypecheckingContext(null, civlTypeChecker.Options)); - return CmdHelper.AssertCmd(tok, expr, msg); - } - } - - public class InlineSequentialization : Sequentialization - { - private Implementation inlinedImpl; - - public InlineSequentialization(CivlTypeChecker civlTypeChecker, Action targetAction) - : base(civlTypeChecker, targetAction) - { - inlinedImpl = CreateInlinedImplementation(); - var refinedAction = targetAction.RefinedAction; - if (refinedAction.HasPendingAsyncs) - { - Action.DesugarCreateAsyncs(civlTypeChecker, inlinedImpl, refinedAction.ActionDecl); - } - Dictionary map = new Dictionary(); - for (int i = 0; i < refinedAction.Impl.InParams.Count; i++) - { - map[refinedAction.Impl.InParams[i]] = Expr.Ident(inlinedImpl.Proc.InParams[i]); - } - for (int i = 0; i < refinedAction.Impl.OutParams.Count; i++) - { - map[refinedAction.Impl.OutParams[i]] = Expr.Ident(inlinedImpl.Proc.OutParams[i]); - } - var subst = Substituter.SubstitutionFromDictionary(map); - inlinedImpl.Proc.Requires = refinedAction.Gate.Select(g => new Requires(false, Substituter.Apply(subst, g.Expr))).ToList(); - var frame = new HashSet(civlTypeChecker.GlobalVariablesAtLayer(targetAction.LayerRange.UpperLayer)); - inlinedImpl.Proc.Ensures = new List(new[] - { - new Ensures(false, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame))) - { Description = new FailureOnlyDescription($"Refinement check of {targetAction.Name} failed") } - }); - } - - protected override List GenerateCheckers() - { - var decls = base.GenerateCheckers(); - decls.AddRange(new List(new Declaration[] { inlinedImpl, inlinedImpl.Proc })); - return decls; - } - - private Implementation CreateInlinedImplementation() - { - var graph = new Graph(); - EliminatedActionDecls.ForEach(actionDecl => - { - graph.AddSource(actionDecl); - CollectionExtensions.ForEach(actionDecl.CreateActionDecls.Intersect(EliminatedActionDecls), x => graph.AddEdge(x, actionDecl)); - }); - var eliminatedPendingAsyncs = new Dictionary(); - var decls = new List(); - graph.TopologicalSort().ForEach(actionDecl => - { - var impl = Action.CreateDuplicateImplementation(actionDecl.Impl, - $"{actionDecl.Name}_RefinementCheck"); - eliminatedPendingAsyncs[actionDecl.PendingAsyncType] = impl; - decls.Add(impl); - decls.Add(impl.Proc); - }); - var inlinedImpl = Action.CreateDuplicateImplementation(targetAction.ActionDecl.Impl, - $"{targetAction.ActionDecl.Name}_RefinementCheck"); - CivlAttributes.RemoveAttributes(inlinedImpl.Proc, new HashSet { "inline" }); - decls.Add(inlinedImpl); - decls.Add(inlinedImpl.Proc); - decls.OfType().ForEach(impl => - { - var modifies = impl.Proc.Modifies.Select(ie => ie.Decl).ToHashSet(); - impl.Blocks.ForEach(block => - { - for (int i = 0; i < block.Cmds.Count; i++) - { - block.Cmds[i] = Transform(eliminatedPendingAsyncs, block.Cmds[i], modifies); - } - }); - impl.Proc.Modifies = modifies.Select(v => Expr.Ident(v)).ToList(); - }); - var oldTopLevelDeclarations = new List(civlTypeChecker.program.TopLevelDeclarations); - civlTypeChecker.program.AddTopLevelDeclarations(decls); - decls.OfType().ForEach(impl => - { - impl.OriginalBlocks = impl.Blocks; - impl.OriginalLocVars = impl.LocVars; - }); - Inliner.ProcessImplementation(civlTypeChecker.Options, civlTypeChecker.program, inlinedImpl); - civlTypeChecker.program.TopLevelDeclarations = oldTopLevelDeclarations; - decls.OfType().ForEach(impl => - { - impl.OriginalBlocks = null; - impl.OriginalLocVars = null; - }); - return inlinedImpl; - } - - private Cmd Transform(Dictionary eliminatedPendingAsyncs, Cmd cmd, HashSet modifies) - { - if (cmd is CallCmd callCmd && callCmd.IsAsync) - { - var actionDecl = (ActionDecl)callCmd.Proc; - var pendingAsyncType = actionDecl.PendingAsyncType; - if (eliminatedPendingAsyncs.ContainsKey(pendingAsyncType)) - { - var newCallee = eliminatedPendingAsyncs[pendingAsyncType].Proc; - var newCallCmd = new CallCmd(callCmd.tok, newCallee.Name, callCmd.Ins, new List()) - { - Proc = newCallee - }; - modifies.UnionWith(newCallee.Modifies.Select(ie => ie.Decl)); - return newCallCmd; - } - } - return cmd; - } - } - - public class InductiveSequentialization : Sequentialization - { - private Action invariantAction; - private IdentifierExpr choice; - private Dictionary newPAs; - - public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action targetAction, Action invariantAction) - : base(civlTypeChecker, targetAction) - { - // The type checker ensures that the set of modified variables of an invariant is a superset of - // - the modified set of each of each eliminated and abstract action associated with this invariant. - // - the target and refined action of every application of inductive sequentialization that refers to this invariant. - this.invariantAction = invariantAction; - choice = Expr.Ident(invariantAction.ImplWithChoice.OutParams.Last()); - newPAs = invariantAction.PendingAsyncs.ToDictionary(decl => decl.PendingAsyncType, - decl => (Variable)civlTypeChecker.LocalVariable($"newPAs_{decl.Name}", decl.PendingAsyncMultisetType)); - } - - private IEnumerable InputMapWellFormedExprs() - { - var scope = invariantAction.Impl.InParams.Union(invariantAction.UsedGlobalVars); - return civlTypeChecker.linearTypeChecker.MapWellFormedExpressions(scope); - } - - private IEnumerable InputDisjointnessExprs() - { - var scope = invariantAction.Impl.InParams.Union(invariantAction.UsedGlobalVars); - var linearScope = scope.Where(x => LinearTypeChecker.InKinds.Contains(LinearTypeChecker.FindLinearKind(x))); - return civlTypeChecker.linearTypeChecker.MapWellFormedExpressions(scope) - .Union(civlTypeChecker.linearTypeChecker.DisjointnessExprForEachDomain(linearScope)); - } - - private List GenerateBaseCaseChecker() - { - var inputDisjointnessExprs = InputDisjointnessExprs(); - var mapWellFormedExprs = InputMapWellFormedExprs(); - var requires = invariantAction.Gate.Select(g => new Requires(false, g.Expr)) - .Concat(inputDisjointnessExprs.Concat(mapWellFormedExprs).Select(expr => new Requires(false, expr))) - .ToList(); - - var subst = targetAction.GetSubstitution(invariantAction); - var cmds = targetAction.GetGateAsserts(subst, - $"Gate of {targetAction.Name} fails in base check against invariant {invariantAction.Name}").ToList(); - - // Construct call to targetAction - var pendingAsyncTypeToOutputParamIndex = invariantAction.PendingAsyncs.Select(x => x.PendingAsyncType) - .Zip(Enumerable.Range(invariantAction.PendingAsyncStartIndex, invariantAction.PendingAsyncs.Count())) - .ToDictionary(tuple => tuple.Item1, tuple => tuple.Item2); - var outputVars = new List(invariantAction.Impl.OutParams.Take(invariantAction.PendingAsyncStartIndex)); - outputVars.AddRange(targetAction.PendingAsyncs.Select(action => - invariantAction.Impl.OutParams[pendingAsyncTypeToOutputParamIndex[action.PendingAsyncType]])); - cmds.Add(CmdHelper.CallCmd(targetAction.Impl.Proc, invariantAction.Impl.InParams, outputVars)); - - // Assign empty multiset to the rest - var remainderPendingAsyncs = invariantAction.PendingAsyncs.Except(targetAction.PendingAsyncs); - if (remainderPendingAsyncs.Any()) - { - var lhss = remainderPendingAsyncs.Select(decl => - Expr.Ident(invariantAction.Impl.OutParams[pendingAsyncTypeToOutputParamIndex[decl.PendingAsyncType]])) - .ToList(); - var rhss = remainderPendingAsyncs.Select(decl => - ExprHelper.FunctionCall(decl.PendingAsyncConst, Expr.Literal(0))).ToList(); - cmds.Add(CmdHelper.AssignCmd(lhss, rhss)); - } - - var frame = new HashSet(invariantAction.ModifiedGlobalVars); - cmds.Add(GetCheck(targetAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame), - $"base of {targetAction.Name} failed")); - - return GetCheckerTuple($"Base_{targetAction.Name}", requires, invariantAction.Impl.InParams, - invariantAction.Impl.OutParams, new List(), cmds); - } - - private List GenerateConclusionChecker() - { - var inputDisjointnessExprs = InputDisjointnessExprs(); - var mapWellFormedExprs = InputMapWellFormedExprs(); - var refinedAction = targetAction.RefinedAction; - var subst = refinedAction.GetSubstitution(invariantAction); - var requires = refinedAction.Gate.Select(g => new Requires(false, Substituter.Apply(subst, g.Expr))) - .Concat(inputDisjointnessExprs.Concat(mapWellFormedExprs).Select(expr => new Requires(false, expr))) - .ToList(); - - var cmds = invariantAction.GetGateAsserts(null, - $"Gate of {invariantAction.Name} fails in conclusion check against {refinedAction.Name}").ToList(); - cmds.Add(CmdHelper.CallCmd(invariantAction.Impl.Proc, invariantAction.Impl.InParams, - invariantAction.Impl.OutParams)); - cmds.Add(CmdHelper.AssumeCmd(NoPendingAsyncs)); - var frame = new HashSet(civlTypeChecker.GlobalVariablesAtLayer(targetAction.LayerRange.UpperLayer)); - cmds.Add(GetCheck(targetAction.tok, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame)), - $"conclusion of {targetAction.Name} failed")); - - return GetCheckerTuple($"Conclusion_{targetAction.Name}", requires, invariantAction.Impl.InParams, - invariantAction.Impl.OutParams, new List(), cmds); - } - - private List GenerateStepChecker(Action pendingAsync) - { - var inputDisjointnessExprs = InputDisjointnessExprs(); - var mapWellFormedExprs = InputMapWellFormedExprs(); - var pendingAsyncType = pendingAsync.ActionDecl.PendingAsyncType; - var pendingAsyncCtor = pendingAsync.ActionDecl.PendingAsyncCtor; - var requires = invariantAction.Gate.Select(g => new Requires(false, g.Expr)) - .Concat(inputDisjointnessExprs.Concat(mapWellFormedExprs).Select(expr => new Requires(false, expr))) - .ToList(); - var locals = new List(); - List cmds = new List - { - CmdHelper.CallCmd(invariantAction.ImplWithChoice.Proc, invariantAction.ImplWithChoice.InParams, - invariantAction.ImplWithChoice.OutParams), - CmdHelper.AssumeCmd(ChoiceTest(pendingAsyncType)), - CmdHelper.AssumeCmd(Expr.Gt(Expr.Select(PAs(pendingAsyncType), Choice(pendingAsyncType)), - Expr.Literal(0))), - RemoveChoice(pendingAsyncType) - }; - - var inputExprs = new List(); - for (int i = 0; i < pendingAsync.Impl.InParams.Count; i++) - { - inputExprs.Add(ExprHelper.FieldAccess(Choice(pendingAsyncType), pendingAsyncCtor.InParams[i].Name)); - } - CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, inputExprs); - cmds.AddRange(pendingAsync.GetGateAsserts( - Substituter.SubstitutionFromDictionary(pendingAsync.Impl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2)), - $"Gate of {pendingAsync.Name} fails in induction step for invariant {invariantAction.Name}")); - cmds.AddRange(pendingAsync.Preconditions(Layer, - Substituter.SubstitutionFromDictionary(pendingAsync.ActionDecl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2)))); - - List outputExprs = new List(); - if (pendingAsync.HasPendingAsyncs) - { - pendingAsync.PendingAsyncs.ForEach(decl => - { - var ie = NewPAs(decl.PendingAsyncType); - locals.Add(ie.Decl); - outputExprs.Add(ie); - }); - } - cmds.Add(CmdHelper.CallCmd(pendingAsync.Impl.Proc, inputExprs, outputExprs)); - if (pendingAsync.HasPendingAsyncs) - { - var lhss = pendingAsync.PendingAsyncs.Select(decl => new SimpleAssignLhs(Token.NoToken, PAs(decl.PendingAsyncType))) - .ToList(); - var rhss = pendingAsync.PendingAsyncs.Select(decl => ExprHelper.FunctionCall(decl.PendingAsyncAdd, - PAs(decl.PendingAsyncType), NewPAs(decl.PendingAsyncType))).ToList(); - cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); - } - - var frame = new HashSet(invariantAction.ModifiedGlobalVars); - cmds.Add(GetCheck(invariantAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame), - $"step of {invariantAction.Name} with {pendingAsync.Name} failed")); - - return GetCheckerTuple($"Step_{invariantAction.Name}_{pendingAsync.Name}", requires, - invariantAction.ImplWithChoice.InParams, invariantAction.ImplWithChoice.OutParams, locals, cmds); - } - - private List GetCheckerTuple(string checkerName, List requires, List inParams, - List outParams, List locals, List cmds) - { - CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds, ResolutionContext.State.Two); - var proc = DeclHelper.Procedure( - civlTypeChecker.AddNamePrefix(checkerName), - inParams, - outParams, - requires, - new List(), - new List(), - invariantAction.ModifiedGlobalVars.Select(Expr.Ident).ToList()); - var impl = DeclHelper.Implementation( - proc, - proc.InParams, - proc.OutParams, - locals, - new List { BlockHelper.Block(checkerName, cmds) }); - return new List(new Declaration[] { proc, impl }); - } - - private IdentifierExpr PAs(CtorType pendingAsyncType) - { - return Expr.Ident(invariantAction.PAs(pendingAsyncType)); - } - - private IdentifierExpr NewPAs(CtorType pendingAsyncType) - { - return Expr.Ident(newPAs[pendingAsyncType]); - } - - private Expr Choice(CtorType pendingAsyncType) - { - return ExprHelper.FieldAccess(choice, pendingAsyncType.Decl.Name); - } - - private Expr ChoiceTest(CtorType pendingAsyncType) - { - return ExprHelper.IsConstructor(choice, invariantAction.ChoiceConstructor(pendingAsyncType).Name); - } - - private Expr NoPendingAsyncs - { - get - { - var expr = Expr.And(eliminatedActions.Select(action => Expr.Eq(PAs(action.ActionDecl.PendingAsyncType), - ExprHelper.FunctionCall(action.ActionDecl.PendingAsyncConst, Expr.Literal(0))))); - expr.Typecheck(new TypecheckingContext(null, civlTypeChecker.Options)); - return expr; - } - } - - private AssignCmd RemoveChoice(CtorType pendingAsyncType) - { - var rhs = Expr.Sub(Expr.Select(PAs(pendingAsyncType), Choice(pendingAsyncType)), Expr.Literal(1)); - return AssignCmd.MapAssign(Token.NoToken, PAs(pendingAsyncType), new List { Choice(pendingAsyncType) }, rhs); - } - - protected override List GenerateCheckers() - { - var decls = base.GenerateCheckers(); - decls.AddRange(GenerateBaseCaseChecker()); - decls.AddRange(GenerateConclusionChecker()); - foreach (var elim in eliminatedActions) - { - decls.AddRange(GenerateStepChecker(elim)); - } - return decls; - } - } -} \ No newline at end of file diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs index 621f33e50..f478a8c8e 100644 --- a/Source/Concurrency/LinearDomainCollector.cs +++ b/Source/Concurrency/LinearDomainCollector.cs @@ -1,5 +1,4 @@ using System.Collections.Generic; -using System.Diagnostics; using System.Linq; namespace Microsoft.Boogie diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index f061a5881..32351da2c 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -1,6 +1,5 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; -using System.Linq; namespace Microsoft.Boogie; @@ -39,11 +38,6 @@ private List RewriteCmdSeq(List cmdSeq) { newCmdSeq.AddRange(RewriteCallCmd(callCmd)); } - else if (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name == "create_asyncs") - { - newCmdSeq.AddRange(PreconditionsForCreateAsyncs(callCmd)); - newCmdSeq.Add(cmd); - } else { newCmdSeq.Add(cmd); @@ -57,91 +51,6 @@ private List RewriteCmdSeq(List cmdSeq) return newCmdSeq; } - private List PreconditionsForCreateAsyncs(CallCmd callCmd) - { - var cmds = new List(); - var attr = QKeyValue.FindAttribute(callCmd.Attributes, x => x.Key == "linear"); - if (attr == null) - { - return cmds; - } - - var sources = attr.Params.OfType(); - var pendingAsyncType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; - var actionDecl = linearTypeChecker.GetActionDeclFromCreateAsyncs(callCmd); - var iter = Enumerable.Range(0, actionDecl.InParams.Count).Where(i => { - var inParam = actionDecl.InParams[i]; - if (LinearTypeChecker.FindLinearKind(inParam) == LinearKind.ORDINARY) - { - return false; - } - if (inParam.TypedIdent.Type is not CtorType ctorType) - { - return false; - } - var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl); - return originalTypeCtorDecl.Name == "One" || originalTypeCtorDecl.Name == "Set"; - }); - var datatypeTypeCtorDecl = (DatatypeTypeCtorDecl) actionDecl.PendingAsyncType.Decl; - var constructor = datatypeTypeCtorDecl.Constructors[0]; - - var paVar = civlTypeChecker.BoundVariable("pa", actionDecl.PendingAsyncType); - var containsExpr = NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar)); - var containsCheckExprs = iter.Zip(sources).Select(kv => { - var i = kv.First; - var sourceExpr = kv.Second; - var inParam = actionDecl.InParams[i]; - var ctorType = (CtorType)inParam.TypedIdent.Type; - var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl); - var instanceType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(ctorType.Decl)[0]; - var fieldAccess = ExprHelper.FieldAccess(Expr.Ident(paVar), constructor.InParams[i].Name); - if (originalTypeCtorDecl.Name == "One") - { - fieldAccess = ExprHelper.FieldAccess(fieldAccess, "val"); - return ExprHelper.FunctionCall(SetContains(instanceType), sourceExpr, fieldAccess); - } - else - { - return ExprHelper.FunctionCall(SetIsSubset(instanceType), fieldAccess, sourceExpr); - } - }); - var containsCheckExpr = ExprHelper.ForallExpr( - new List(){ paVar }, - Expr.Imp(containsExpr, Expr.And(containsCheckExprs))); - cmds.Add(CmdHelper.AssertCmd(callCmd.tok, containsCheckExpr, "Contains check failed")); - - var paVar1 = civlTypeChecker.BoundVariable("pa1", actionDecl.PendingAsyncType); - var paVar2 = civlTypeChecker.BoundVariable("pa2", actionDecl.PendingAsyncType); - var guardExprs = new List() { - NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar1)), - NAryExpr.Select(callCmd.Ins[0], Expr.Ident(paVar2)), - Expr.Neq(Expr.Ident(paVar1), Expr.Ident(paVar2)) - }; - var distinctCheckExprs = iter.Select(i => { - var inParam = actionDecl.InParams[i]; - var ctorType = (CtorType)inParam.TypedIdent.Type; - var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl); - var instanceType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(ctorType.Decl)[0]; - var fieldAccess1 = ExprHelper.FieldAccess(Expr.Ident(paVar1), constructor.InParams[i].Name); - var fieldAccess2 = ExprHelper.FieldAccess(Expr.Ident(paVar2), constructor.InParams[i].Name); - if (originalTypeCtorDecl.Name == "One") - { - return Expr.Neq(fieldAccess1, fieldAccess2); - } - else - { - return ExprHelper.FunctionCall(SetIsDisjoint(instanceType), fieldAccess1, fieldAccess2); - } - }); - var distinctCheckExpr = ExprHelper.ForallExpr( - new List(){ paVar1, paVar2 }, - Expr.Imp(Expr.And(guardExprs), Expr.And(distinctCheckExprs))); - cmds.Add(CmdHelper.AssertCmd(callCmd.tok, distinctCheckExpr, "Distinct check failed")); - - ResolveAndTypecheck(options, cmds); - return cmds; - } - public List RewriteCallCmd(CallCmd callCmd) { switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index fc0774eea..b3be5bd58 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -13,7 +13,6 @@ public class LinearTypeChecker : ReadOnlyVisitor private CheckingContext checkingContext; private HashSet<(Absy, string)> errors; private CivlTypeChecker civlTypeChecker; - private Dictionary pendingAsyncTypeToActionDecl; private Dictionary permissionTypeToLinearDomain; private Dictionary> collectors; private Dictionary> availableLinearVars; @@ -24,11 +23,6 @@ public LinearTypeChecker(CivlTypeChecker civlTypeChecker) this.program = civlTypeChecker.program; this.checkingContext = civlTypeChecker.checkingContext; this.errors = new (); - this.pendingAsyncTypeToActionDecl = new (); - foreach (var actionDecl in program.TopLevelDeclarations.OfType().Where(actionDecl => actionDecl.MaybePendingAsync)) - { - pendingAsyncTypeToActionDecl[actionDecl.PendingAsyncType] = actionDecl; - } // other fields are initialized in the TypeCheck method } @@ -573,71 +567,6 @@ enclosingProc is not YieldProcedureDecl && } } } - - var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(node.Proc); - if (originalProc.Name == "create_multi_asyncs" || originalProc.Name == "create_asyncs") - { - var actionDecl = GetActionDeclFromCreateAsyncs(node); - if (originalProc.Name == "create_multi_asyncs") - { - foreach (var inParam in actionDecl.InParams.Where(inParam => FindLinearKind(inParam) != LinearKind.ORDINARY)) - { - Error(node, $"linear parameters not allowed on pending async"); - } - } - else if (originalProc.Name == "create_asyncs") - { - var linearArgumentTypes = new List(); - foreach (var inParam in actionDecl.InParams.Where(inParam => FindLinearKind(inParam) != LinearKind.ORDINARY)) - { - if (inParam.TypedIdent.Type is CtorType ctorType) - { - var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl); - if (originalTypeCtorDecl.Name == "One") - { - var typeInstantiation = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(ctorType.Decl); - var setType = TypeHelper.CtorType(civlTypeChecker.program.monomorphizer.InstantiateTypeCtorDecl("Set", typeInstantiation)); - linearArgumentTypes.Add(setType); - continue; - } - else if (originalTypeCtorDecl.Name == "Set") - { - linearArgumentTypes.Add(ctorType); - continue; - } - } - Error(node, $"linear parameter must be of type One or Set"); - } - var attr = QKeyValue.FindAttribute(node.Attributes, x => x.Key == "linear"); - var attrParams = attr == null ? new List() : attr.Params; - var identifierExprs = attrParams.OfType().ToList(); - if (identifierExprs.Count != attrParams.Count()) - { - Error(node, $"each linear source must be a variable"); - } - else if (identifierExprs.Count != linearArgumentTypes.Count) - { - Error(node, $"number of linear sources must match the number of linear parameters"); - } - else - { - foreach (var (ie, type) in identifierExprs.Zip(linearArgumentTypes)) - { - if (ie.Decl is LocalVariable || ie.Decl is Formal) - { - if (!ie.Decl.TypedIdent.Type.Equals(type)) - { - Error(ie, $"expected type {type}"); - } - } - else - { - Error(ie, $"expected local or formal variable"); - } - } - } - } - } return base.VisitCallCmd(node); } @@ -877,12 +806,6 @@ private Function MapWellFormedFunction(Monomorphizer monomorphizer, TypeCtorDecl return monomorphizer.InstantiateFunction("Map_WellFormed", typeParamInstantiationMap); } - public ActionDecl GetActionDeclFromCreateAsyncs(CallCmd callCmd) - { - var pendingAsyncType = civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"]; - return pendingAsyncTypeToActionDecl[pendingAsyncType]; - } - #endregion #region Annotation Eraser diff --git a/Source/Concurrency/RefinementInstrumentation.cs b/Source/Concurrency/RefinementInstrumentation.cs index 2b54506ff..580c3adaa 100644 --- a/Source/Concurrency/RefinementInstrumentation.cs +++ b/Source/Concurrency/RefinementInstrumentation.cs @@ -127,19 +127,6 @@ public ActionRefinementInstrumentation( } } - if (atomicAction.HasPendingAsyncs) - { - atomicAction.PendingAsyncs.ForEach(decl => - { - Variable collectedPAs = - civlTypeChecker.PendingAsyncCollectors(originalImpl)[decl.PendingAsyncType]; - alwaysMap[atomicAction.PAs(decl.PendingAsyncType)] = Expr.Ident(collectedPAs); - LocalVariable copy = Old(collectedPAs); - newLocalVars.Add(copy); - oldOutputMap[collectedPAs] = copy; - }); - } - Substitution always = Substituter.SubstitutionFromDictionary(alwaysMap); Substitution forold = Substituter.SubstitutionFromDictionary(foroldMap); Expr transitionRelationExpr = GetTransitionRelation(atomicAction); diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index 8e575def2..00525562c 100644 --- a/Source/Concurrency/YieldingProcDuplicator.cs +++ b/Source/Concurrency/YieldingProcDuplicator.cs @@ -1,4 +1,3 @@ -using System; using System.Collections.Generic; using System.Linq; using System.Diagnostics; @@ -129,44 +128,19 @@ public override Ensures VisitEnsures(Ensures node) #region Implementation duplication - private Implementation enclosingImpl; private YieldProcedureDecl enclosingYieldingProc; private Block enclosingBlock; private bool inPredicatePhase; - private Action RefinedAction => civlTypeChecker.Action(enclosingYieldingProc.RefinedAction.ActionDecl); - private List newCmdSeq; private Dictionary returnedPAs; private Dictionary addedLocalVariables; - private Variable ReturnedPAs(CtorType pendingAsyncType) - { - if (!returnedPAs.ContainsKey(pendingAsyncType)) - { - returnedPAs[pendingAsyncType] = civlTypeChecker.LocalVariable($"returnedPAs_{pendingAsyncType.Decl.Name}", - TypeHelper.MapType(pendingAsyncType, Type.Int)); - } - return returnedPAs[pendingAsyncType]; - } - - private Variable CollectedPAs(CtorType pendingAsyncType) - { - if (!civlTypeChecker.PendingAsyncCollectors(enclosingImpl).TryGetValue(pendingAsyncType, out var collectedPAs)) - { - collectedPAs = civlTypeChecker.LocalVariable($"collectedPAs_{pendingAsyncType.Decl.Name}", - TypeHelper.MapType(pendingAsyncType, Type.Int)); - civlTypeChecker.PendingAsyncCollectors(enclosingImpl)[pendingAsyncType] = collectedPAs; - } - return collectedPAs; - } - public override Implementation VisitImplementation(Implementation impl) { enclosingYieldingProc = (YieldProcedureDecl)impl.Proc; - enclosingImpl = impl; Debug.Assert(layerNum <= enclosingYieldingProc.Layer); returnedPAs = new Dictionary(); @@ -178,13 +152,6 @@ public override Implementation VisitImplementation(Implementation impl) newImpl.LocVars.AddRange(returnedPAs.Values); newImpl.LocVars.AddRange(addedLocalVariables.Values); - if (!enclosingYieldingProc.HasMoverType && RefinedAction.HasPendingAsyncs && doRefinementCheck) - { - var assumeExpr = EmptyPendingAsyncMultisetExpr(CollectedPAs, RefinedAction.PendingAsyncs); - newImpl.LocVars.AddRange(civlTypeChecker.PendingAsyncCollectors(impl).Values.Except(impl.LocVars)); - newImpl.Blocks.First().Cmds.Insert(0, CmdHelper.AssumeCmd(assumeExpr)); - } - absyMap[newImpl] = impl; return newImpl; } @@ -363,10 +330,6 @@ cmd is AssertCmd assertCmd && makeAssume // synchronize the called atomic action AddActionCall(newCall, yieldingProc); } - else if (doRefinementCheck) - { - AddPendingAsync(newCall, yieldingProc); - } } else { @@ -378,7 +341,6 @@ cmd is AssertCmd assertCmd && makeAssume else if (doRefinementCheck) { Debug.Assert(!yieldingProc.HasMoverType); - AddPendingAsync(newCall, yieldingProc); } else { @@ -521,12 +483,6 @@ private void AddActionCall(CallCmd newCall, YieldProcedureDecl calleeActionProc) InjectPreconditions(calleeRefinedAction, newCall); InjectGate(calleeRefinedAction, newCall, !doRefinementCheck); newCmdSeq.Add(newCall); - - if (calleeRefinedAction.HasPendingAsyncs) - { - Debug.Assert(newCall.Outs.Count == newCall.Proc.OutParams.Count - calleeRefinedAction.PendingAsyncs.Count()); - CollectReturnedPendingAsyncs(newCall, calleeRefinedAction); - } } private void InjectPreconditions(Action action, CallCmd callCmd) @@ -580,41 +536,6 @@ private void InjectGate(Action action, CallCmd callCmd, bool assume) newCmdSeq.Add(new CommentCmd("injected gate >>>")); } - private void CollectReturnedPendingAsyncs(CallCmd newCall, Action calleeRefinedAction) - { - // Inject pending async collection - newCall.Outs.AddRange(calleeRefinedAction.PendingAsyncs.Select(decl => Expr.Ident(ReturnedPAs(decl.PendingAsyncType)))); - if (!doRefinementCheck) - { - return; - } - - calleeRefinedAction.PendingAsyncs.ForEach(decl => - { - if (RefinedAction.PendingAsyncs.Contains(decl)) - { - newCmdSeq.Add(CmdHelper.AssignCmd(CollectedPAs(decl.PendingAsyncType), - ExprHelper.FunctionCall(decl.PendingAsyncAdd, Expr.Ident(CollectedPAs(decl.PendingAsyncType)), - Expr.Ident(ReturnedPAs(decl.PendingAsyncType))))); - } - else - { - newCmdSeq.Add(CmdHelper.AssertCmd(newCall.tok, - Expr.Eq(Expr.Ident(ReturnedPAs(decl.PendingAsyncType)), ExprHelper.FunctionCall(decl.PendingAsyncConst, Expr.Literal(0))), - $"Pending asyncs to action {decl.Name} created by this call are not summarized")); - } - }); - } - - private Expr EmptyPendingAsyncMultisetExpr(Func pendingAsyncMultisets, IEnumerable asyncActions) - { - var returnExpr = Expr.And(asyncActions.Select(decl => - Expr.Eq(Expr.Ident(pendingAsyncMultisets(decl.PendingAsyncType)), - ExprHelper.FunctionCall(decl.PendingAsyncConst, Expr.Literal(0)))).ToList()); - returnExpr.Typecheck(new TypecheckingContext(null, civlTypeChecker.Options)); - return returnExpr; - } - private void AddDuplicateCall(CallCmd newCall, bool makeParallel) { newCall.IsAsync = false; @@ -647,39 +568,6 @@ private void DesugarAsyncCall(CallCmd newCall) newCmdSeq.Add(newCall); } - private void AddPendingAsync(CallCmd newCall, YieldProcedureDecl calleeProc) - { - if (calleeProc.RefinedAction.ActionDecl == civlTypeChecker.SkipActionDecl) - { - return; - } - var calleeRefinedAction = calleeProc.Layer == enclosingYieldingProc.Layer - ? calleeProc.RefinedAction.ActionDecl - : calleeProc.RefinedActionAtLayer(layerNum); - - if (RefinedAction.PendingAsyncs.Contains(calleeRefinedAction)) - { - Expr[] newIns = new Expr[calleeRefinedAction.InParams.Count]; - for (int i = 0, j = 0; i < calleeProc.InParams.Count; i++) - { - if (calleeProc.VisibleFormals.Contains(calleeProc.InParams[i])) - { - newIns[j] = newCall.Ins[i]; - j++; - } - } - var collectedPAs = CollectedPAs(calleeRefinedAction.PendingAsyncType); - var pa = ExprHelper.FunctionCall(calleeRefinedAction.PendingAsyncCtor, newIns); - var inc = Expr.Add(Expr.Select(Expr.Ident(collectedPAs), pa), Expr.Literal(1)); - var add = CmdHelper.AssignCmd(collectedPAs, Expr.Store(Expr.Ident(collectedPAs), pa, inc)); - newCmdSeq.Add(add); - } - else - { - newCmdSeq.Add(CmdHelper.AssertCmd(newCall.tok, Expr.False, "This pending async is not summarized")); - } - } - #endregion public List Collect() diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 86f887463..13fd559f2 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -46,12 +46,7 @@ public static List TransformImplementations( decls.Add(yieldingProcInstrumentation.WrapperNoninterferenceCheckerImpl( yieldingProcInstrumentation.wrapperGlobalNoninterferenceCheckerProc, globalNoninterferenceCheckerProcs)); - if (yieldToYieldNoninterferenceCheckerProcs.Count() > 0) - { - decls.AddRange(yieldingProcInstrumentation.ActionNoninterferenceCheckers( - civlTypeChecker.MoverActions.Where(a => a.LayerRange.Contains(layerNum) && a.ActionDecl.MaybePendingAsync), - false)); - } + if (globalNoninterferenceCheckerProcs.Count() > 0) { decls.AddRange(yieldingProcInstrumentation.ActionNoninterferenceCheckers( diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index db84e32f4..5d8bb4b40 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -2870,12 +2870,9 @@ public enum MoverType public class ActionDecl : Procedure { public MoverType MoverType; - public List Creates; public ActionDeclRef RefinedAction; - public ActionDeclRef InvariantAction; public List YieldRequires; public List Asserts; - public DatatypeTypeCtorDecl PendingAsyncCtorDecl; public bool IsAnonymous; public Implementation Impl; // set when the implementation of this action is resolved @@ -2883,19 +2880,16 @@ public class ActionDecl : Procedure public ActionDecl(IToken tok, string name, MoverType moverType, List inParams, List outParams, bool isPure, - List creates, ActionDeclRef refinedAction, ActionDeclRef invariantAction, + ActionDeclRef refinedAction, List requires, List modifies, List yieldRequires, List asserts, - DatatypeTypeCtorDecl pendingAsyncCtorDecl, QKeyValue kv) : base(tok, name, + QKeyValue kv) : base(tok, name, new List(), inParams, outParams, isPure, requires, new List(), new List(), modifies, kv) { this.MoverType = moverType; - this.Creates = creates; this.RefinedAction = refinedAction; - this.InvariantAction = invariantAction; this.YieldRequires = yieldRequires; this.Asserts = asserts; - this.PendingAsyncCtorDecl = pendingAsyncCtorDecl; this.IsAnonymous = name == null; if (IsAnonymous) { @@ -2925,25 +2919,6 @@ public override void Resolve(ResolutionContext rc) Asserts.ForEach(assertCmd => assertCmd.Resolve(rc)); rc.PopVarContext(); rc.Proc = null; - if (Creates.Any()) - { - if (IsPure) - { - rc.Error(this, "unnecessary creates clause for pure action"); - } - else if (MoverType == MoverType.Right || MoverType == MoverType.Both) - { - rc.Error(this, "right mover may not create pending asyncs"); - } - } - Creates.ForEach(create => - { - create.Resolve(rc); - if (create.ActionDecl is { MaybePendingAsync: false }) - { - rc.Error(create, $"{create.ActionName} must be an async action"); - } - }); if (RefinedAction != null) { RefinedAction.Resolve(rc); @@ -2956,10 +2931,6 @@ public override void Resolve(ResolutionContext rc) RefinedAction.ActionDecl.MoverType = MoverType.Atomic; } } - if (InvariantAction != null) - { - InvariantAction.Resolve(rc); - } } public override void Typecheck(TypecheckingContext tc) @@ -2999,73 +2970,14 @@ public override void Typecheck(TypecheckingContext tc) } } - Creates.ForEach(actionDeclRef => - { - var pendingAsync = actionDeclRef.ActionDecl; - if (!LayerRange.Subset(pendingAsync.LayerRange)) - { - tc.Error(this, $"pending async {pendingAsync.Name} is not available on all layers of {Name}"); - } - }); - if (RefinedAction != null) { - EliminatedActionDecls().Where(actionDecl => !actionDecl.IsLeftMover).ForEach(actionDecl => { - tc.Error(actionDecl, $"eliminated action must be a left mover"); - }); var layer = LayerRange.UpperLayer; var refinedActionDecl = RefinedAction.ActionDecl; if (!refinedActionDecl.LayerRange.Contains(layer + 1)) { tc.Error(refinedActionDecl, $"refined action does not exist at layer {layer + 1}"); } - if (InvariantAction != null) - { - var actionCreates = CreateActionDecls.ToHashSet(); - var refinedActionCreates = refinedActionDecl.CreateActionDecls.ToHashSet(); - var invariantActionDecl = InvariantAction.ActionDecl; - if (!invariantActionDecl.LayerRange.Contains(layer)) - { - tc.Error(invariantActionDecl, $"invariant action does not exist at layer {layer}"); - } - var invariantCreates = invariantActionDecl.CreateActionDecls.ToHashSet(); - if (!actionCreates.IsSubsetOf(invariantCreates)) - { - tc.Error(this, - $"each pending async created by refining action must also be created by invariant action {invariantActionDecl.Name}"); - } - if (!refinedActionCreates.IsSubsetOf(invariantCreates)) - { - tc.Error(this, - $"each pending async created by refined action must also be created by invariant action {invariantActionDecl.Name}"); - } - var actionModifies = new HashSet(Modifies.Select(ie => ie.Decl)); - var refinedActionModifies = new HashSet(refinedActionDecl.Modifies.Select(ie => ie.Decl)); - var invariantModifies = new HashSet(invariantActionDecl.Modifies.Select(ie => ie.Decl)); - if (!actionModifies.IsSubsetOf(invariantModifies)) - { - tc.Error(this, $"modifies of {Name} must be subset of modifies of {invariantActionDecl.Name}"); - } - if (!refinedActionModifies.IsSubsetOf(invariantModifies)) - { - tc.Error(this, - $"modifies of {refinedActionDecl.Name} must be subset of modifies of {invariantActionDecl.Name}"); - } - foreach (var elimProc in invariantCreates.Except(refinedActionCreates)) - { - var elimCreates = elimProc.CreateActionDecls.ToHashSet(); - if (!elimCreates.IsSubsetOf(invariantCreates)) - { - tc.Error(this, - $"each pending async created by eliminated action {elimProc.Name} must also be created by invariant action {invariantActionDecl.Name}"); - } - var targetModifies = new HashSet(elimProc.Modifies.Select(ie => ie.Decl)); - if (!targetModifies.IsSubsetOf(invariantModifies)) - { - tc.Error(this, $"modifies of {elimProc.Name} must be subset of modifies of {invariantActionDecl.Name}"); - } - } - } } } @@ -3075,10 +2987,6 @@ protected override void EmitBegin(TokenTextWriter stream, int level) { stream.Write(this, level, "pure "); } - if (MaybePendingAsync) - { - stream.Write(level, "async "); - } if (!IsPure) { switch (MoverType) @@ -3105,93 +3013,24 @@ protected override void EmitEnd(TokenTextWriter stream, int level) if (RefinedAction != null) { stream.Write(level, $"refines {RefinedAction.ActionName}"); - if (InvariantAction == null) - { - stream.WriteLine(";"); - } - else - { - stream.WriteLine($" using {InvariantAction.ActionName};"); - } - } - if (Creates.Any()) - { - stream.WriteLine(level, $"creates {string.Join(",", Creates.Select(x => x.ActionName))};"); + stream.WriteLine(";"); } base.EmitEnd(stream, level); } - public IEnumerable EliminatedActionDecls() - { - var refinedProc = RefinedAction.ActionDecl; - var refinedActionCreates = refinedProc.CreateActionDecls.ToHashSet(); - HashSet FixpointCreates() - { - var currCreates = new HashSet(refinedActionCreates); - var frontier = CreateActionDecls.ToHashSet().Except(currCreates); - while (frontier.Any()) - { - currCreates.UnionWith(frontier); - frontier = frontier.SelectMany(actionDecl => actionDecl.CreateActionDecls).Except(currCreates); - } - return currCreates; - } - var allCreates = InvariantAction == null - ? FixpointCreates() - : InvariantAction.ActionDecl.CreateActionDecls; - return allCreates.Except(refinedActionCreates); - } - public IEnumerable ActionDeclRefs() { - return Creates.Append(RefinedAction).Append(InvariantAction); + return [RefinedAction]; } public bool HasPreconditions => Requires.Count > 0 || YieldRequires.Count > 0; - public IEnumerable CreateActionDecls => Creates.Select(x => x.ActionDecl); - - public bool MaybePendingAsync => PendingAsyncCtorDecl != null; - public bool HasMoverType => MoverType != MoverType.None; public bool IsRightMover => MoverType == MoverType.Right || MoverType == MoverType.Both; public bool IsLeftMover => MoverType == MoverType.Left || MoverType == MoverType.Both; - public DatatypeConstructor PendingAsyncCtor => PendingAsyncCtorDecl.GetConstructor(Name); - - public CtorType PendingAsyncType => new (PendingAsyncCtorDecl.tok, PendingAsyncCtorDecl, new List()); - - public MapType PendingAsyncMultisetType => new(Token.NoToken, new List(), - new List { PendingAsyncType }, Type.Int); - - public Function PendingAsyncAdd => pendingAsyncAdd; - private Function pendingAsyncAdd; - - public Function PendingAsyncConst => pendingAsyncConst; - private Function pendingAsyncConst; - - public Function PendingAsyncIte => pendingAsyncIte; - private Function pendingAsyncIte; - - // This method is needed to ensure that all support monomorphized functions can be generated during Civl type checking. - // Otherwise, during later passes, monomorphization might be invoked and cause program.TopLevelDeclarations to be modified - // while an iteration is being done on it. - public void Initialize(Monomorphizer monomorphizer) - { - if (PendingAsyncCtorDecl == null) - { - return; - } - pendingAsyncAdd = - monomorphizer.InstantiateFunction("MapAdd", new Dictionary { { "T", PendingAsyncType } }); - pendingAsyncConst = monomorphizer.InstantiateFunction("MapConst", - new Dictionary { { "T", PendingAsyncType }, { "U", Type.Int } }); - pendingAsyncIte = monomorphizer.InstantiateFunction("MapIte", - new Dictionary { { "T", PendingAsyncType }, { "U", Type.Int } }); - } - public override Absy StdDispatch(StandardVisitor visitor) { return visitor.VisitActionDecl(this); diff --git a/Source/Core/AST/Commands/CallCmd.cs b/Source/Core/AST/Commands/CallCmd.cs index bd75cd252..e3a0ee3ae 100644 --- a/Source/Core/AST/Commands/CallCmd.cs +++ b/Source/Core/AST/Commands/CallCmd.cs @@ -304,10 +304,6 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc) } else { - if (callerDecl.HasMoverType && highestRefinedActionDecl.Creates.Any()) - { - tc.Error(this, "caller must not be a mover procedure"); - } if (IsAsync) { if (isSynchronized) @@ -357,10 +353,6 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc) { tc.Error(this, $"called action is not available at layer {callerDecl.Layer + 1}"); } - else if (!highestRefinedAction.MaybePendingAsync) - { - tc.Error(this, $"action {highestRefinedAction.Name} refined by callee must be eligible to be a pending async"); - } } } } @@ -448,41 +440,12 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc) { // ok } - else if (Proc.OriginalDeclWithFormals != null && CivlPrimitives.Async.Contains(Proc.OriginalDeclWithFormals.Name)) - { - // ok - } else if (IsAsync) { - if (callerActionDecl.Creates.All(x => x.ActionName != Proc.Name)) - { - tc.Error(this, "pending async must be in the creates clause of caller"); - } - } - else if (CivlPrimitives.Async.Contains(Proc.Name)) - { - var type = TypeProxy.FollowProxy(TypeParameters[Proc.TypeParameters[0]].Expanded); - if (type is CtorType { Decl: DatatypeTypeCtorDecl datatypeTypeCtorDecl }) - { - if (callerActionDecl.Creates.All(x => x.ActionName != datatypeTypeCtorDecl.Name)) - { - tc.Error(this, "primitive call must be instantiated with a pending async type in the creates clause of caller"); - } - } - else - { - tc.Error(this, "primitive call must be instantiated with a pending async type"); - } + tc.Error(this, "async call not allowed in atomic action"); } else if (Proc is ActionDecl calleeActionDecl) { - foreach (var actionDeclRef in calleeActionDecl.Creates) - { - if (callerActionDecl.Creates.All(x => x.ActionDecl != actionDeclRef.ActionDecl)) - { - tc.Error(actionDeclRef, "callee creates a pending async not in the creates clause of caller"); - } - } if (!callerActionDecl.LayerRange.Subset(calleeActionDecl.LayerRange)) { tc.Error(this, diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 45ce01da8..7b983a22d 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -662,13 +662,10 @@ Pure ActionDecl = (. IToken name = null; - bool isAsync = false; MoverType moverType = MoverType.None; List ins, outs = new List(); List mods = new List(); - List creates = new List(); ActionDeclRef refinedAction = null; - ActionDeclRef invariantAction = null; List requires = new List(); List yieldRequires = new List(); List asserts = new List(); @@ -678,7 +675,6 @@ ActionDecl ] "action" { Attribute } @@ -686,8 +682,8 @@ ActionDecl [ "returns" ProcFormals ] ( ";" - { SpecAction } - | { SpecAction } + { SpecAction } + | { SpecAction } ImplBody (. impl = new Implementation(name, name.val, new List(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), @@ -705,33 +701,10 @@ ActionDecl 0) - { - this.SemErr("async action must not have output parameters"); - } - else - { - if (moverType == MoverType.None) - { - moverType = MoverType.Atomic; - } - datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List(), null); - var fields = ins.Select(v => new Formal(v.tok, new TypedIdent(v.TypedIdent.tok, v.Name, v.TypedIdent.Type), true, v.Attributes)).ToList(); - datatypeTypeCtorDecl.AddConstructor(name, name.val, fields); - } - } - actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, requires, mods, yieldRequires, asserts, datatypeTypeCtorDecl, kv); + actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, refinedAction, requires, mods, yieldRequires, asserts, kv); .) . -SpecCreates<.List creates.> -= - "creates" (. List cs; .) - Idents (. foreach(IToken c in cs) { creates.Add(new ActionDeclRef(c, c.val)); } .) - ";" - . - SpecRefinedActionForAtomicAction = (. IToken m; QKeyValue kv = null; .) @@ -745,6 +718,7 @@ SpecRefinedActionForAtomicAction this.SemErr("a refines specification already exists"); } .) + ";" . SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List ins, List outs.> @@ -766,8 +740,8 @@ SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name var outParams = new List(outs); outParams.RemoveAll(x => x.HasAttribute(CivlAttributes.HIDE)); var actionDecl = new ActionDecl(tok, actionName, moverType, Formal.StripWhereClauses(inParams), Formal.StripWhereClauses(outParams), - false, new List(), null, null, - new List(), new List(), new List(), new List(), null, akv); + false, null, + new List(), new List(), new List(), new List(), akv); Pgm.AddTopLevelDeclaration(actionDecl); var impl = new Implementation(tok, actionDecl.Name, new List(), Formal.StripWhereClauses(inParams), Formal.StripWhereClauses(outParams), locals, stmtList, akv == null ? null : (QKeyValue)akv.Clone()); @@ -790,15 +764,11 @@ SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name ) . -SpecAction<.ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List mods, List creates, List requires, List yieldRequires, List asserts.> +SpecAction<.ref ActionDeclRef refinedAction, List mods, List requires, List yieldRequires, List asserts.> = ( SpecRefinedActionForAtomicAction - (. IToken m; .) - ["using" Ident (. invariantAction = new ActionDeclRef(m, m.val); .)] - ";" | SpecModifies - | SpecCreates | SpecYieldRequires | SpecAsserts ) diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 03dc6b468..e3f235427 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -83,10 +83,9 @@ public static class CivlAttributes public const string LAYER = "layer"; public const string YIELDS = "yields"; public const string HIDE = "hide"; - public const string PENDING_ASYNC = "pending_async"; public const string SYNC = "sync"; - private static string[] CIVL_ATTRIBUTES = { LAYER, YIELDS, HIDE, PENDING_ASYNC, SYNC }; + private static string[] CIVL_ATTRIBUTES = { LAYER, YIELDS, HIDE, SYNC }; public const string LINEAR = "linear"; public const string LINEAR_IN = "linear_in"; @@ -248,10 +247,5 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); } } - - public static HashSet Async = new() - { - "create_asyncs", "create_multi_asyncs", "set_choice" - }; } } diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 32eec488b..328ac3e47 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -35,7 +35,7 @@ public class Parser { public const int _decimal = 5; public const int _dec_float = 6; public const int _float = 7; - public const int maxT = 124; + public const int maxT = 122; const bool _T = true; const bool _x = false; @@ -297,12 +297,12 @@ void BoogiePL() { Pgm.AddTopLevelDeclaration(im); } - } else SynErr(125); + } else SynErr(123); break; } - case 38: case 39: case 40: case 44: case 45: case 46: case 47: case 48: { + case 38: case 39: case 41: case 42: case 43: case 44: case 45: { Pure(ref isPure); - if (la.kind == 48) { + if (la.kind == 45) { Procedure(isPure, out pr, out im); Pgm.AddTopLevelDeclaration(pr); if (im != null) { @@ -321,10 +321,10 @@ void BoogiePL() { } isPure = false; - } else SynErr(126); + } else SynErr(124); break; } - case 52: { + case 49: { Implementation(out nnim); Pgm.AddTopLevelDeclaration(nnim); break; @@ -360,7 +360,7 @@ void Consts(out List ds) { axioms.Add(axiom); ds.Add(axiom); } Expect(27); - } else SynErr(127); + } else SynErr(125); foreach(TypedIdent x in xs){ Contract.Assert(x != null); var constant = new Constant(y, x, u, kv, axioms); @@ -419,7 +419,7 @@ void Function(out List ds) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(128); + } else SynErr(126); if (la.kind == 26) { Get(); Expression(out tmp); @@ -444,7 +444,7 @@ void Function(out List ds) { Expect(27); } else if (la.kind == 10) { Get(); - } else SynErr(129); + } else SynErr(127); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -609,7 +609,7 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl) if (StartOf(5)) { MoverQualifier(ref moverType); } - Expect(48); + Expect(45); while (la.kind == 26) { Attribute(ref kv); } @@ -632,7 +632,7 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl) impl = new Implementation(name, name.val, new List(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(130); + } else SynErr(128); ypDecl = new YieldProcedureDecl(name, name.val, moverType, ins, outs, pre, preserves, post, mods, yieldRequires, yieldPreserves, yieldEnsures, refinedAction, kv); } @@ -655,7 +655,7 @@ void Procedure(bool isPure, out Procedure proc, out /*maybe null*/ Implementatio QKeyValue kv = null; impl = null; - Expect(48); + Expect(45); ProcSignature(true, out x, out typeParams, out ins, out outs, out kv); if (la.kind == 10) { Get(); @@ -670,19 +670,16 @@ void Procedure(bool isPure, out Procedure proc, out /*maybe null*/ Implementatio impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(131); + } else SynErr(129); proc = new Procedure(x, x.val, typeParams, ins, outs, isPure, pre, new List(), post, mods, kv); } void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, out DatatypeTypeCtorDecl datatypeTypeCtorDecl) { IToken name = null; - bool isAsync = false; MoverType moverType = MoverType.None; List ins, outs = new List(); List mods = new List(); - List creates = new List(); ActionDeclRef refinedAction = null; - ActionDeclRef invariantAction = null; List requires = new List(); List yieldRequires = new List(); List asserts = new List(); @@ -692,14 +689,10 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, datatypeTypeCtorDecl = null; impl = null; - if (la.kind == 39) { - Get(); - isAsync = true; - } if (StartOf(5)) { MoverQualifier(ref moverType); } - Expect(40); + Expect(39); while (la.kind == 26) { Attribute(ref kv); } @@ -712,17 +705,17 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, if (la.kind == 10) { Get(); while (StartOf(10)) { - SpecAction(ref refinedAction, ref invariantAction, mods, creates, requires, yieldRequires, asserts); + SpecAction(ref refinedAction, mods, requires, yieldRequires, asserts); } } else if (StartOf(11)) { while (StartOf(10)) { - SpecAction(ref refinedAction, ref invariantAction, mods, creates, requires, yieldRequires, asserts); + SpecAction(ref refinedAction, mods, requires, yieldRequires, asserts); } ImplBody(out locals, out stmtList); impl = new Implementation(name, name.val, new List(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone()); - } else SynErr(132); + } else SynErr(130); if (isPure) { if (moverType == MoverType.None) { @@ -733,23 +726,7 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, this.SemErr("mover type unnecessary for pure action since it is a both mover"); } } - if (isAsync) { - if (outs.Count > 0) - { - this.SemErr("async action must not have output parameters"); - } - else - { - if (moverType == MoverType.None) - { - moverType = MoverType.Atomic; - } - datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List(), null); - var fields = ins.Select(v => new Formal(v.tok, new TypedIdent(v.TypedIdent.tok, v.Name, v.TypedIdent.Type), true, v.Attributes)).ToList(); - datatypeTypeCtorDecl.AddConstructor(name, name.val, fields); - } - } - actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, requires, mods, yieldRequires, asserts, datatypeTypeCtorDecl, kv); + actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, refinedAction, requires, mods, yieldRequires, asserts, kv); } @@ -761,7 +738,7 @@ void Implementation(out Implementation impl) { StmtList stmtList; QKeyValue kv; - Expect(52); + Expect(49); ProcSignature(false, out x, out typeParams, out ins, out outs, out kv); ImplBody(out locals, out stmtList); impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); @@ -860,7 +837,7 @@ void Type(out Bpl.Type ty) { ty = new UnresolvedTypeIdentifier (tok, tok.val, args); } else if (la.kind == 19 || la.kind == 21) { MapType(out ty); - } else SynErr(133); + } else SynErr(131); } void AttributesIdsTypeWhere(bool allowWhereClauses, string context, System.Action action ) { @@ -896,7 +873,7 @@ void IdsTypeWhere(bool allowWhereClauses, string context, System.Action ts) { } else if (la.kind == 19 || la.kind == 21) { MapType(out ty); ts.Add(ty); - } else SynErr(136); + } else SynErr(134); } void MapType(out Bpl.Type ty) { @@ -1144,40 +1121,31 @@ void Invariant(List invariants) { } void MoverQualifier(ref MoverType moverType) { - if (la.kind == 44) { + if (la.kind == 41) { Get(); moverType = MoverType.Left; - } else if (la.kind == 45) { + } else if (la.kind == 42) { Get(); moverType = MoverType.Right; - } else if (la.kind == 46) { + } else if (la.kind == 43) { Get(); moverType = MoverType.Both; - } else if (la.kind == 47) { + } else if (la.kind == 44) { Get(); moverType = MoverType.Atomic; - } else SynErr(137); + } else SynErr(135); } - void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List mods, List creates, List requires, List yieldRequires, List asserts) { - if (la.kind == 42) { + void SpecAction(ref ActionDeclRef refinedAction, List mods, List requires, List yieldRequires, List asserts) { + if (la.kind == 40) { SpecRefinedActionForAtomicAction(ref refinedAction); - IToken m; - if (la.kind == 43) { - Get(); - Ident(out m); - invariantAction = new ActionDeclRef(m, m.val); - } - Expect(10); - } else if (la.kind == 54) { + } else if (la.kind == 51) { SpecModifies(mods); - } else if (la.kind == 41) { - SpecCreates(creates); - } else if (la.kind == 50) { + } else if (la.kind == 47) { SpecYieldRequires(requires, yieldRequires); - } else if (la.kind == 49) { + } else if (la.kind == 46) { SpecAsserts(asserts); - } else SynErr(138); + } else SynErr(136); } void ImplBody(out List locals, out StmtList stmtList) { @@ -1189,17 +1157,9 @@ void ImplBody(out List locals, out StmtList stmtList) { StmtList(out stmtList); } - void SpecCreates(List creates) { - Expect(41); - List cs; - Idents(out cs); - foreach(IToken c in cs) { creates.Add(new ActionDeclRef(c, c.val)); } - Expect(10); - } - void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) { IToken m; QKeyValue kv = null; - Expect(42); + Expect(40); while (la.kind == 26) { Attribute(ref kv); } @@ -1210,19 +1170,20 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) { this.SemErr("a refines specification already exists"); } + Expect(10); } void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List ins, List outs) { IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.Atomic; List locals; StmtList stmtList; - Expect(42); + Expect(40); while (la.kind == 26) { Attribute(ref kv); } - if (StartOf(16)) { + if (StartOf(3)) { if (StartOf(5)) { MoverQualifier(ref moverType); } - Expect(40); + Expect(39); tok = t; while (la.kind == 26) { Attribute(ref akv); @@ -1236,8 +1197,8 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken var outParams = new List(outs); outParams.RemoveAll(x => x.HasAttribute(CivlAttributes.HIDE)); var actionDecl = new ActionDecl(tok, actionName, moverType, Formal.StripWhereClauses(inParams), Formal.StripWhereClauses(outParams), - false, new List(), null, null, - new List(), new List(), new List(), new List(), null, akv); + false, null, + new List(), new List(), new List(), new List(), akv); Pgm.AddTopLevelDeclaration(actionDecl); var impl = new Implementation(tok, actionDecl.Name, new List(), Formal.StripWhereClauses(inParams), Formal.StripWhereClauses(outParams), locals, stmtList, akv == null ? null : (QKeyValue)akv.Clone()); @@ -1256,12 +1217,12 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken } Expect(10); - } else SynErr(139); + } else SynErr(137); } void SpecModifies(List mods) { List ms; - Expect(54); + Expect(51); if (StartOf(14)) { Idents(out ms); foreach(IToken m in ms) { mods.Add(new IdentifierExpr(m, m.val)); } @@ -1271,24 +1232,24 @@ void SpecModifies(List mods) { void SpecYieldRequires(List pre, List yieldRequires ) { Expr e; Cmd cmd; Token tok; QKeyValue kv = null; - Expect(50); + Expect(47); tok = t; - if (StartOf(17)) { + if (StartOf(16)) { while (la.kind == 26) { Attribute(ref kv); } Proposition(out e); pre.Add(new Requires(tok, false, e, null, kv)); - } else if (la.kind == 39 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 50 || la.kind == 68 || la.kind == 69) { CallCmd(true, out cmd); yieldRequires.Add((CallCmd)cmd); - } else SynErr(140); + } else SynErr(138); Expect(10); } void SpecAsserts(List asserts ) { Expr e; Token tok; QKeyValue kv = null; - Expect(49); + Expect(46); tok = t; while (la.kind == 26) { Attribute(ref kv); @@ -1299,17 +1260,17 @@ void SpecAsserts(List asserts ) { } void SpecYieldPrePost(ref ActionDeclRef refinedAction, IToken name, List ins, List outs, List pre, List preserves, List post, List yieldRequires, List yieldPreserves, List yieldEnsures, List mods) { - if (la.kind == 42) { + if (la.kind == 40) { SpecRefinedActionForYieldProcedure(ref refinedAction, name, ins, outs); - } else if (la.kind == 50) { + } else if (la.kind == 47) { SpecYieldRequires(pre, yieldRequires); } else if (la.kind == 37) { SpecYieldPreserves(preserves, yieldPreserves); - } else if (la.kind == 51) { + } else if (la.kind == 48) { SpecYieldEnsures(post, yieldEnsures); - } else if (la.kind == 54) { + } else if (la.kind == 51) { SpecModifies(mods); - } else SynErr(141); + } else SynErr(139); } void CallCmd(bool inSpec, out Cmd c) { @@ -1320,19 +1281,19 @@ void CallCmd(bool inSpec, out Cmd c) { c = null; List callCmds = new List(); - if (la.kind == 39) { + if (la.kind == 68) { Get(); isAsync = true; } - if (la.kind == 53) { + if (la.kind == 50) { Get(); isFree = true; } - Expect(71); + Expect(69); x = t; CallParams(isAsync, isFree, x, out c); callCmds.Add((CallCmd)c); - while (la.kind == 72) { + while (la.kind == 70) { Get(); CallParams(false, false, x, out c); callCmds.Add((CallCmd)c); @@ -1351,33 +1312,33 @@ void SpecYieldPreserves(List preserves, List yieldPreserves ) Expr e; Cmd cmd; Token tok; QKeyValue kv = null; Expect(37); tok = t; - if (StartOf(17)) { + if (StartOf(16)) { while (la.kind == 26) { Attribute(ref kv); } Proposition(out e); preserves.Add(new Requires(tok, false, e, null, kv)); - } else if (la.kind == 39 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 50 || la.kind == 68 || la.kind == 69) { CallCmd(true, out cmd); yieldPreserves.Add((CallCmd)cmd); - } else SynErr(142); + } else SynErr(140); Expect(10); } void SpecYieldEnsures(List post, List yieldEnsures ) { Expr e; Cmd cmd; Token tok; QKeyValue kv = null; - Expect(51); + Expect(48); tok = t; - if (StartOf(17)) { + if (StartOf(16)) { while (la.kind == 26) { Attribute(ref kv); } Proposition(out e); post.Add(new Ensures(tok, false, e, null, kv)); - } else if (la.kind == 39 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 50 || la.kind == 68 || la.kind == 69) { CallCmd(true, out cmd); yieldEnsures.Add((CallCmd)cmd); - } else SynErr(143); + } else SynErr(141); Expect(10); } @@ -1401,19 +1362,19 @@ void ProcSignature(bool allowWhereClausesOnFormals, out IToken name, out List pre, List mods, List post) { - if (la.kind == 54) { + if (la.kind == 51) { SpecModifies(mods); - } else if (la.kind == 53) { + } else if (la.kind == 50) { Get(); SpecPrePost(true, pre, post); - } else if (la.kind == 50 || la.kind == 51) { + } else if (la.kind == 47 || la.kind == 48) { SpecPrePost(false, pre, post); - } else SynErr(144); + } else SynErr(142); } void SpecPrePost(bool free, List pre, List post) { Contract.Requires(pre != null); Contract.Requires(post != null); Expr e; Token tok = null; QKeyValue kv = null; - if (la.kind == 50) { + if (la.kind == 47) { Get(); tok = t; while (la.kind == 26) { @@ -1422,7 +1383,7 @@ void SpecPrePost(bool free, List pre, List post) { Proposition(out e); Expect(10); pre.Add(new Requires(tok, free, e, null, kv)); - } else if (la.kind == 51) { + } else if (la.kind == 48) { Get(); tok = t; while (la.kind == 26) { @@ -1431,7 +1392,7 @@ void SpecPrePost(bool free, List pre, List post) { Proposition(out e); Expect(10); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(145); + } else SynErr(143); } void StmtList(out StmtList stmtList) { @@ -1444,8 +1405,8 @@ void StmtList(out StmtList stmtList) { StructuredCmd ec = null; StructuredCmd ecn; TransferCmd tc = null; TransferCmd tcn; - while (StartOf(18)) { - if (StartOf(19)) { + while (StartOf(17)) { + if (StartOf(18)) { LabelOrCmd(out c, out label); Contract.Assert(c == null || label == null); if (c != null) { @@ -1467,7 +1428,7 @@ void StmtList(out StmtList stmtList) { cs = new List(); } - } else if (la.kind == 57 || la.kind == 59 || la.kind == 61) { + } else if (la.kind == 54 || la.kind == 56 || la.kind == 58) { StructuredCmd(out ecn); ec = ecn; if (startToken == null) { startToken = ec.tok; cs = new List(); } @@ -1512,8 +1473,8 @@ void LabelOrCmd(out Cmd c, out IToken label) { HideRevealCmd.Modes mode; IdentifierExpr hideRevealId = null; - if (la.kind == 62 || la.kind == 63) { - if (la.kind == 62) { + if (la.kind == 59 || la.kind == 60) { + if (la.kind == 59) { Get(); mode = HideRevealCmd.Modes.Reveal; } else { @@ -1523,22 +1484,22 @@ void LabelOrCmd(out Cmd c, out IToken label) { if (la.kind == 1) { Get(); hideRevealId = new IdentifierExpr(t, t.val); - } else if (la.kind == 60) { + } else if (la.kind == 57) { Get(); - } else SynErr(146); + } else SynErr(144); c = hideRevealId == null ? new HideRevealCmd(t, mode) : new HideRevealCmd(hideRevealId, mode); Expect(10); - } else if (la.kind == 64) { + } else if (la.kind == 61) { Get(); c = new ChangeScope(t, ChangeScope.Modes.Pop); Expect(10); - } else if (la.kind == 65) { + } else if (la.kind == 62) { Get(); c = new ChangeScope(t, ChangeScope.Modes.Push); Expect(10); } else if (StartOf(14)) { LabelOrAssign(out c, out label); - } else if (la.kind == 66) { + } else if (la.kind == 63) { Get(); x = t; while (la.kind == 26) { @@ -1547,7 +1508,7 @@ void LabelOrCmd(out Cmd c, out IToken label) { Proposition(out e); c = new AssertCmd(x, e, kv); Expect(10); - } else if (la.kind == 67) { + } else if (la.kind == 64) { Get(); x = t; while (la.kind == 26) { @@ -1556,7 +1517,7 @@ void LabelOrCmd(out Cmd c, out IToken label) { Proposition(out e); c = new AssumeCmd(x, e, kv); Expect(10); - } else if (la.kind == 68) { + } else if (la.kind == 65) { Get(); x = t; Idents(out xs); @@ -1568,27 +1529,27 @@ void LabelOrCmd(out Cmd c, out IToken label) { } c = new HavocCmd(x,ids); - } else if (la.kind == 39 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 50 || la.kind == 68 || la.kind == 69) { CallCmd(false, out cn); Expect(10); c = cn; - } else SynErr(147); + } else SynErr(145); } void StructuredCmd(out StructuredCmd ec) { Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(Cce.IsPeerConsistent(ec)); IfCmd ifcmd; WhileCmd wcmd; BreakCmd bcmd; - if (la.kind == 57) { + if (la.kind == 54) { IfCmd(out ifcmd); ec = ifcmd; - } else if (la.kind == 59) { + } else if (la.kind == 56) { WhileCmd(out wcmd); ec = wcmd; - } else if (la.kind == 61) { + } else if (la.kind == 58) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(148); + } else SynErr(146); } void TransferCmd(out TransferCmd tc) { @@ -1597,7 +1558,7 @@ void TransferCmd(out TransferCmd tc) { List ss = new List(); QKeyValue kv = null; - if (la.kind == 55) { + if (la.kind == 52) { Get(); y = t; while (la.kind == 26) { @@ -1611,13 +1572,13 @@ void TransferCmd(out TransferCmd tc) { Attributes = kv }; - } else if (la.kind == 56) { + } else if (la.kind == 53) { Get(); while (la.kind == 26) { Attribute(ref kv); } tc = new ReturnCmd(t) { Attributes = kv }; - } else SynErr(149); + } else SynErr(147); Expect(10); } @@ -1629,7 +1590,7 @@ void IfCmd(out IfCmd ifcmd) { StmtList els; StmtList elseOption = null; QKeyValue kv = null; - Expect(57); + Expect(54); x = t; while (la.kind == 26) { Attribute(ref kv); @@ -1637,16 +1598,16 @@ void IfCmd(out IfCmd ifcmd) { Guard(out guard); Expect(26); StmtList(out thn); - if (la.kind == 58) { + if (la.kind == 55) { Get(); - if (la.kind == 57) { + if (la.kind == 54) { IfCmd(out elseIf); elseIfOption = elseIf; } else if (la.kind == 26) { Get(); StmtList(out els); elseOption = els; - } else SynErr(150); + } else SynErr(148); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption, kv); } @@ -1659,13 +1620,13 @@ void WhileCmd(out WhileCmd wcmd) { StmtList body; QKeyValue kv = null; - Expect(59); + Expect(56); x = t; Guard(out guard); Contract.Assume(guard == null || Cce.Owner.None(guard)); - while (la.kind == 36 || la.kind == 53) { + while (la.kind == 36 || la.kind == 50) { isFree = false; z = la/*lookahead token*/; - if (la.kind == 53) { + if (la.kind == 50) { Get(); isFree = true; } @@ -1673,7 +1634,7 @@ void WhileCmd(out WhileCmd wcmd) { while (la.kind == 26) { Attribute(ref kv); } - if (StartOf(20)) { + if (StartOf(19)) { Expression(out e); if (isFree) { invariants.Add(new AssumeCmd(z, e, kv)); @@ -1682,12 +1643,12 @@ void WhileCmd(out WhileCmd wcmd) { } kv = null; - } else if (la.kind == 39 || la.kind == 53 || la.kind == 71) { + } else if (la.kind == 50 || la.kind == 68 || la.kind == 69) { CallCmd(true, out cmd); yields.Add((CallCmd)cmd); kv = null; - } else SynErr(151); + } else SynErr(149); Expect(10); } Expect(26); @@ -1699,7 +1660,7 @@ void BreakCmd(out BreakCmd bcmd) { Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken x; IToken y; string breakLabel = null; - Expect(61); + Expect(58); x = t; if (StartOf(14)) { Ident(out y); @@ -1712,13 +1673,13 @@ void BreakCmd(out BreakCmd bcmd) { void Guard(out Expr e) { Expr ee; e = null; Expect(11); - if (la.kind == 60) { + if (la.kind == 57) { Get(); e = null; - } else if (StartOf(20)) { + } else if (StartOf(19)) { Expression(out ee); e = ee; - } else SynErr(152); + } else SynErr(150); Expect(12); } @@ -1744,7 +1705,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { Expect(12); lhsExpr = new NAryExpr(x, new FunctionCall(new IdentifierExpr(id, id.val)), ids.Select(id => new IdentifierExpr(id, id.val)).ToList()); - Expect(69); + Expect(66); x = t; /* use location of := */ while (la.kind == 26) { Attribute(ref kv); @@ -1753,10 +1714,10 @@ void LabelOrAssign(out Cmd c, out IToken label) { Expect(10); c = new UnpackCmd(x, lhsExpr, e0, kv); - } else if (StartOf(21)) { + } else if (StartOf(20)) { lhss = new List(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 19 || la.kind == 70) { + while (la.kind == 19 || la.kind == 67) { if (la.kind == 19) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); @@ -1770,7 +1731,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { Get(); Ident(out id); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 19 || la.kind == 70) { + while (la.kind == 19 || la.kind == 67) { if (la.kind == 19) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); @@ -1781,7 +1742,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { } lhss.Add(lhs); } - Expect(69); + Expect(66); x = t; /* use location of := */ while (la.kind == 26) { Attribute(ref kv); @@ -1796,7 +1757,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { } Expect(10); c = new AssignCmd(x, lhss, rhss, kv); - } else SynErr(153); + } else SynErr(151); } void MapAssignIndex(out IToken x, out List indexes) { @@ -1805,7 +1766,7 @@ void MapAssignIndex(out IToken x, out List indexes) { Expect(19); x = t; - if (StartOf(20)) { + if (StartOf(19)) { Expression(out e); indexes.Add(e); while (la.kind == 14) { @@ -1819,7 +1780,7 @@ void MapAssignIndex(out IToken x, out List indexes) { void FieldAccess(out IToken x, out FieldAccess fieldAccess) { Contract.Ensures(Contract.ValueAtReturn(out fieldAccess) != null); IToken id; - Expect(70); + Expect(67); x = t; Ident(out id); fieldAccess = new FieldAccess(id, id.val); @@ -1840,7 +1801,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { Ident(out first); if (la.kind == 11) { Get(); - if (StartOf(20)) { + if (StartOf(19)) { Expression(out en); es.Add(en); while (la.kind == 14) { @@ -1851,7 +1812,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { } Expect(12); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else if (la.kind == 14 || la.kind == 69) { + } else if (la.kind == 14 || la.kind == 66) { ids.Add(new IdentifierExpr(first, first.val)); if (la.kind == 14) { Get(); @@ -1863,10 +1824,10 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { ids.Add(new IdentifierExpr(p, p.val)); } } - Expect(69); + Expect(66); Ident(out first); Expect(11); - if (StartOf(20)) { + if (StartOf(19)) { Expression(out en); es.Add(en); while (la.kind == 14) { @@ -1877,7 +1838,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { } Expect(12); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else SynErr(154); + } else SynErr(152); } void Expressions(out List es) { @@ -1894,8 +1855,8 @@ void Expressions(out List es) { void ImpliesExpression(bool noExplies, out Expr e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken x; Expr e1; LogicalExpression(out e0); - if (StartOf(22)) { - if (la.kind == 75 || la.kind == 76) { + if (StartOf(21)) { + if (la.kind == 73 || la.kind == 74) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1907,7 +1868,7 @@ void ImpliesExpression(bool noExplies, out Expr e0) { x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 77 || la.kind == 78) { + while (la.kind == 75 || la.kind == 76) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1918,23 +1879,23 @@ void ImpliesExpression(bool noExplies, out Expr e0) { } void EquivOp() { - if (la.kind == 73) { + if (la.kind == 71) { Get(); - } else if (la.kind == 74) { + } else if (la.kind == 72) { Get(); - } else SynErr(155); + } else SynErr(153); } void LogicalExpression(out Expr e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken x; Expr e1; RelationalExpression(out e0); - if (StartOf(23)) { - if (la.kind == 79 || la.kind == 80) { + if (StartOf(22)) { + if (la.kind == 77 || la.kind == 78) { AndOp(); x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 79 || la.kind == 80) { + while (la.kind == 77 || la.kind == 78) { AndOp(); x = t; RelationalExpression(out e1); @@ -1945,7 +1906,7 @@ void LogicalExpression(out Expr e0) { x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 81 || la.kind == 82) { + while (la.kind == 79 || la.kind == 80) { OrOp(); x = t; RelationalExpression(out e1); @@ -1956,25 +1917,25 @@ void LogicalExpression(out Expr e0) { } void ImpliesOp() { - if (la.kind == 75) { + if (la.kind == 73) { Get(); - } else if (la.kind == 76) { + } else if (la.kind == 74) { Get(); - } else SynErr(156); + } else SynErr(154); } void ExpliesOp() { - if (la.kind == 77) { + if (la.kind == 75) { Get(); - } else if (la.kind == 78) { + } else if (la.kind == 76) { Get(); - } else SynErr(157); + } else SynErr(155); } void RelationalExpression(out Expr e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken x; Expr e1; BinaryOperator.Opcode op; BvTerm(out e0); - if (StartOf(24)) { + if (StartOf(23)) { RelOp(out x, out op); BvTerm(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -1982,25 +1943,25 @@ void RelationalExpression(out Expr e0) { } void AndOp() { - if (la.kind == 79) { + if (la.kind == 77) { Get(); - } else if (la.kind == 80) { + } else if (la.kind == 78) { Get(); - } else SynErr(158); + } else SynErr(156); } void OrOp() { - if (la.kind == 81) { + if (la.kind == 79) { Get(); - } else if (la.kind == 82) { + } else if (la.kind == 80) { Get(); - } else SynErr(159); + } else SynErr(157); } void BvTerm(out Expr e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken x; Expr e1; Term(out e0); - while (la.kind == 90) { + while (la.kind == 88) { Get(); x = t; Term(out e1); @@ -2011,7 +1972,7 @@ void BvTerm(out Expr e0) { void RelOp(out IToken x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; switch (la.kind) { - case 83: { + case 81: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; @@ -2026,44 +1987,44 @@ void RelOp(out IToken x, out BinaryOperator.Opcode op) { x = t; op=BinaryOperator.Opcode.Gt; break; } - case 84: { + case 82: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 85: { + case 83: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 86: { + case 84: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 87: { + case 85: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 88: { + case 86: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 89: { + case 87: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(160); break; + default: SynErr(158); break; } } void Term(out Expr e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken x; Expr e1; BinaryOperator.Opcode op; Factor(out e0); - while (la.kind == 91 || la.kind == 92) { + while (la.kind == 89 || la.kind == 90) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -2073,7 +2034,7 @@ void Term(out Expr e0) { void Factor(out Expr e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken x; Expr e1; BinaryOperator.Opcode op; Power(out e0); - while (StartOf(25)) { + while (StartOf(24)) { MulOp(out x, out op); Power(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -2082,19 +2043,19 @@ void Factor(out Expr e0) { void AddOp(out IToken x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 91) { + if (la.kind == 89) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 92) { + } else if (la.kind == 90) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(161); + } else SynErr(159); } void Power(out Expr e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken x; Expr e1; IsConstructor(out e0); - if (la.kind == 96) { + if (la.kind == 94) { Get(); x = t; Power(out e1); @@ -2104,25 +2065,25 @@ void Power(out Expr e0) { void MulOp(out IToken x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 60) { + if (la.kind == 57) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 93) { + } else if (la.kind == 91) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 94) { + } else if (la.kind == 92) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else if (la.kind == 95) { + } else if (la.kind == 93) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(162); + } else SynErr(160); } void IsConstructor(out Expr e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken x, id; UnaryExpression(out e0); - if (la.kind == 97) { + if (la.kind == 95) { Get(); x = t; Ident(out id); @@ -2136,27 +2097,27 @@ void UnaryExpression(out Expr e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken x; e = dummyExpr; - if (la.kind == 92) { + if (la.kind == 90) { Get(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); - } else if (la.kind == 98 || la.kind == 99) { + } else if (la.kind == 96 || la.kind == 97) { NegOp(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); - } else if (StartOf(26)) { + } else if (StartOf(25)) { CoercionExpression(out e); - } else SynErr(163); + } else SynErr(161); } void NegOp() { - if (la.kind == 98) { + if (la.kind == 96) { Get(); - } else if (la.kind == 99) { + } else if (la.kind == 97) { Get(); - } else SynErr(164); + } else SynErr(162); } void CoercionExpression(out Expr e) { @@ -2180,7 +2141,7 @@ void CoercionExpression(out Expr e) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(165); + } else SynErr(163); } } @@ -2192,14 +2153,14 @@ void ArrayExpression(out Expr e) { List allArgs = dummyExprSeq; AtomExpression(out e); - while (la.kind == 19 || la.kind == 70) { + while (la.kind == 19 || la.kind == 67) { if (la.kind == 19) { Get(); x = t; allArgs = new List (); allArgs.Add(e); store = false; bvExtract = false; - if (StartOf(27)) { - if (StartOf(20)) { + if (StartOf(26)) { + if (StartOf(19)) { Expression(out index0); if (index0 is BvBounds) bvExtract = true; @@ -2214,7 +2175,7 @@ void ArrayExpression(out Expr e) { allArgs.Add(e1); } - if (la.kind == 69) { + if (la.kind == 66) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -2247,12 +2208,12 @@ void ArrayExpression(out Expr e) { } else if (la.kind == 11) { Get(); Ident(out id); - Expect(69); + Expect(66); x = t; Expression(out e1); Expect(12); e = new NAryExpr(x, new FieldUpdate(id, id.val), new List { e, e1 }); - } else SynErr(166); + } else SynErr(164); } } } @@ -2279,18 +2240,18 @@ void AtomExpression(out Expr e) { List blocks; switch (la.kind) { - case 100: { + case 98: { Get(); e = new LiteralExpr(t, false); break; } - case 101: { + case 99: { Get(); e = new LiteralExpr(t, true); break; } - case 102: case 103: { - if (la.kind == 102) { + case 100: case 101: { + if (la.kind == 100) { Get(); } else { Get(); @@ -2298,8 +2259,8 @@ void AtomExpression(out Expr e) { e = new LiteralExpr(t, RoundingMode.RNE); break; } - case 104: case 105: { - if (la.kind == 104) { + case 102: case 103: { + if (la.kind == 102) { Get(); } else { Get(); @@ -2307,8 +2268,8 @@ void AtomExpression(out Expr e) { e = new LiteralExpr(t, RoundingMode.RNA); break; } - case 106: case 107: { - if (la.kind == 106) { + case 104: case 105: { + if (la.kind == 104) { Get(); } else { Get(); @@ -2316,8 +2277,8 @@ void AtomExpression(out Expr e) { e = new LiteralExpr(t, RoundingMode.RTP); break; } - case 108: case 109: { - if (la.kind == 108) { + case 106: case 107: { + if (la.kind == 106) { Get(); } else { Get(); @@ -2325,8 +2286,8 @@ void AtomExpression(out Expr e) { e = new LiteralExpr(t, RoundingMode.RTN); break; } - case 110: case 111: { - if (la.kind == 110) { + case 108: case 109: { + if (la.kind == 108) { Get(); } else { Get(); @@ -2359,22 +2320,22 @@ void AtomExpression(out Expr e) { e = new LiteralExpr(t, t.val.Trim('"')); break; } - case 1: case 44: case 45: case 46: case 47: case 62: case 63: case 64: case 65: { + case 1: case 41: case 42: case 43: case 44: case 59: case 60: case 61: case 62: { Ident(out x); id = new IdentifierExpr(x, x.val); e = id; if (la.kind == 11) { Get(); - if (StartOf(20)) { + if (StartOf(19)) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); } else if (la.kind == 12) { e = new NAryExpr(x, new FunctionCall(id), new List()); - } else SynErr(167); + } else SynErr(165); Expect(12); } break; } - case 112: { + case 110: { Get(); x = t; Expect(11); @@ -2403,23 +2364,23 @@ void AtomExpression(out Expr e) { } case 11: { Get(); - if (StartOf(20)) { + if (StartOf(19)) { Expression(out e); if (e is BvBounds) this.SemErr("parentheses around bitvector bounds are not allowed"); - } else if (la.kind == 116 || la.kind == 117) { + } else if (la.kind == 114 || la.kind == 115) { Forall(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 118 || la.kind == 119) { + } else if (la.kind == 116 || la.kind == 117) { Exists(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 120 || la.kind == 121) { + } else if (la.kind == 118 || la.kind == 119) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -2429,20 +2390,20 @@ void AtomExpression(out Expr e) { e = new LambdaExpr(x, typeParams, ds, kv, e); } else if (la.kind == 9) { LetExpr(out e); - } else SynErr(168); + } else SynErr(166); Expect(12); break; } - case 57: { + case 54: { IfThenElseExpression(out e); break; } - case 113: { + case 111: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(169); break; + default: SynErr(167); break; } } @@ -2454,7 +2415,7 @@ void Dec(out BigDec n) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(170); + } else SynErr(168); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -2492,11 +2453,11 @@ void BvLit(out BigNum n, out int m) { } void Forall() { - if (la.kind == 116) { + if (la.kind == 114) { Get(); - } else if (la.kind == 117) { + } else if (la.kind == 115) { Get(); - } else SynErr(171); + } else SynErr(169); } void QuantifierBody(IToken q, out List typeParams, out List ds, @@ -2514,7 +2475,7 @@ void QuantifierBody(IToken q, out List typeParams, out List typeParams, out List{ e0, e1, e2 }); } @@ -2591,7 +2552,7 @@ void CodeExpression(out List locals, out List blocks) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List(); Block b; blocks = new List(); - Expect(113); + Expect(111); while (la.kind == 9) { LocalVars(locals); } @@ -2601,7 +2562,7 @@ void CodeExpression(out List locals, out List blocks) { SpecBlock(out b); blocks.Add(b); } - Expect(114); + Expect(112); } void SpecBlock(out Block b) { @@ -2616,7 +2577,7 @@ void SpecBlock(out Block b) { Ident(out x); Expect(13); - while (StartOf(19)) { + while (StartOf(18)) { LabelOrCmd(out c, out label); Contract.Assert(c == null || label == null); if (c != null) { @@ -2626,7 +2587,7 @@ void SpecBlock(out Block b) { } } - if (la.kind == 55) { + if (la.kind == 52) { Get(); y = t; while (la.kind == 26) { @@ -2640,7 +2601,7 @@ void SpecBlock(out Block b) { Attributes = kv }); - } else if (la.kind == 56) { + } else if (la.kind == 53) { Get(); while (la.kind == 26) { Attribute(ref kv); @@ -2650,7 +2611,7 @@ void SpecBlock(out Block b) { Attributes = kv }); - } else SynErr(175); + } else SynErr(173); Expect(10); } @@ -2665,7 +2626,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { Get(); Ident(out id); parameters = new List(); - if (StartOf(20)) { + if (StartOf(19)) { AttributeParameter(out param); parameters.Add(param); while (la.kind == 14) { @@ -2693,7 +2654,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { } } - } else if (StartOf(20)) { + } else if (StartOf(19)) { Expression(out e); es = new List { e }; while (la.kind == 14) { @@ -2707,7 +2668,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(176); + } else SynErr(174); Expect(27); } @@ -2719,18 +2680,18 @@ void AttributeParameter(out object o) { if (la.kind == 4) { Get(); o = t.val.Substring(1, t.val.Length-2); - } else if (StartOf(20)) { + } else if (StartOf(19)) { Expression(out e); o = e; - } else SynErr(177); + } else SynErr(175); } void QSep() { - if (la.kind == 122) { + if (la.kind == 120) { Get(); - } else if (la.kind == 123) { + } else if (la.kind == 121) { Get(); - } else SynErr(178); + } else SynErr(176); } void LetVar(out Variable v) { @@ -2759,34 +2720,33 @@ public void Parse() { } static readonly bool[,] set = { - {_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_T, _T,_T,_x,_T, _T,_x,_T,_T, _T,_x,_x,_x, _T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_T,_x,_T, _T,_T,_x,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x} + {_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_T, _T,_T,_x,_T, _T,_x,_T,_T, _x,_T,_T,_T, _T,_T,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _T,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _T,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_T,_T,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x}, + {_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x} }; } // end Parser @@ -2850,146 +2810,144 @@ string GetSyntaxErrorString(int n) { case 36: s = "\"invariant\" expected"; break; case 37: s = "\"preserves\" expected"; break; case 38: s = "\"pure\" expected"; break; - case 39: s = "\"async\" expected"; break; - case 40: s = "\"action\" expected"; break; - case 41: s = "\"creates\" expected"; break; - case 42: s = "\"refines\" expected"; break; - case 43: s = "\"using\" expected"; break; - case 44: s = "\"left\" expected"; break; - case 45: s = "\"right\" expected"; break; - case 46: s = "\"both\" expected"; break; - case 47: s = "\"atomic\" expected"; break; - case 48: s = "\"procedure\" expected"; break; - case 49: s = "\"asserts\" expected"; break; - case 50: s = "\"requires\" expected"; break; - case 51: s = "\"ensures\" expected"; break; - case 52: s = "\"implementation\" expected"; break; - case 53: s = "\"free\" expected"; break; - case 54: s = "\"modifies\" expected"; break; - case 55: s = "\"goto\" expected"; break; - case 56: s = "\"return\" expected"; break; - case 57: s = "\"if\" expected"; break; - case 58: s = "\"else\" expected"; break; - case 59: s = "\"while\" expected"; break; - case 60: s = "\"*\" expected"; break; - case 61: s = "\"break\" expected"; break; - case 62: s = "\"reveal\" expected"; break; - case 63: s = "\"hide\" expected"; break; - case 64: s = "\"pop\" expected"; break; - case 65: s = "\"push\" expected"; break; - case 66: s = "\"assert\" expected"; break; - case 67: s = "\"assume\" expected"; break; - case 68: s = "\"havoc\" expected"; break; - case 69: s = "\":=\" expected"; break; - case 70: s = "\"->\" expected"; break; - case 71: s = "\"call\" expected"; break; - case 72: s = "\"|\" expected"; break; - case 73: s = "\"<==>\" expected"; break; - case 74: s = "\"\\u21d4\" expected"; break; - case 75: s = "\"==>\" expected"; break; - case 76: s = "\"\\u21d2\" expected"; break; - case 77: s = "\"<==\" expected"; break; - case 78: s = "\"\\u21d0\" expected"; break; - case 79: s = "\"&&\" expected"; break; - case 80: s = "\"\\u2227\" expected"; break; - case 81: s = "\"||\" expected"; break; - case 82: s = "\"\\u2228\" expected"; break; - case 83: s = "\"==\" expected"; break; - case 84: s = "\"<=\" expected"; break; - case 85: s = "\">=\" expected"; break; - case 86: s = "\"!=\" expected"; break; - case 87: s = "\"\\u2260\" expected"; break; - case 88: s = "\"\\u2264\" expected"; break; - case 89: s = "\"\\u2265\" expected"; break; - case 90: s = "\"++\" expected"; break; - case 91: s = "\"+\" expected"; break; - case 92: s = "\"-\" expected"; break; - case 93: s = "\"div\" expected"; break; - case 94: s = "\"mod\" expected"; break; - case 95: s = "\"/\" expected"; break; - case 96: s = "\"**\" expected"; break; - case 97: s = "\"is\" expected"; break; - case 98: s = "\"!\" expected"; break; - case 99: s = "\"\\u00ac\" expected"; break; - case 100: s = "\"false\" expected"; break; - case 101: s = "\"true\" expected"; break; - case 102: s = "\"roundNearestTiesToEven\" expected"; break; - case 103: s = "\"RNE\" expected"; break; - case 104: s = "\"roundNearestTiesToAway\" expected"; break; - case 105: s = "\"RNA\" expected"; break; - case 106: s = "\"roundTowardPositive\" expected"; break; - case 107: s = "\"RTP\" expected"; break; - case 108: s = "\"roundTowardNegative\" expected"; break; - case 109: s = "\"RTN\" expected"; break; - case 110: s = "\"roundTowardZero\" expected"; break; - case 111: s = "\"RTZ\" expected"; break; - case 112: s = "\"old\" expected"; break; - case 113: s = "\"|{\" expected"; break; - case 114: s = "\"}|\" expected"; break; - case 115: s = "\"then\" expected"; break; - case 116: s = "\"forall\" expected"; break; - case 117: s = "\"\\u2200\" expected"; break; - case 118: s = "\"exists\" expected"; break; - case 119: s = "\"\\u2203\" expected"; break; - case 120: s = "\"lambda\" expected"; break; - case 121: s = "\"\\u03bb\" expected"; break; - case 122: s = "\"::\" expected"; break; - case 123: s = "\"\\u2022\" expected"; break; - case 124: s = "??? expected"; break; - case 125: s = "invalid BoogiePL"; break; - case 126: s = "invalid BoogiePL"; break; - case 127: s = "invalid Consts"; break; - case 128: s = "invalid Function"; break; - case 129: s = "invalid Function"; break; - case 130: s = "invalid YieldProcedureDecl"; break; - case 131: s = "invalid Procedure"; break; - case 132: s = "invalid ActionDecl"; break; - case 133: s = "invalid Type"; break; - case 134: s = "invalid TypeAtom"; break; - case 135: s = "invalid Ident"; break; - case 136: s = "invalid TypeArgs"; break; - case 137: s = "invalid MoverQualifier"; break; - case 138: s = "invalid SpecAction"; break; - case 139: s = "invalid SpecRefinedActionForYieldProcedure"; break; - case 140: s = "invalid SpecYieldRequires"; break; - case 141: s = "invalid SpecYieldPrePost"; break; - case 142: s = "invalid SpecYieldPreserves"; break; - case 143: s = "invalid SpecYieldEnsures"; break; - case 144: s = "invalid Spec"; break; - case 145: s = "invalid SpecPrePost"; break; - case 146: s = "invalid LabelOrCmd"; break; - case 147: s = "invalid LabelOrCmd"; break; - case 148: s = "invalid StructuredCmd"; break; - case 149: s = "invalid TransferCmd"; break; - case 150: s = "invalid IfCmd"; break; - case 151: s = "invalid WhileCmd"; break; - case 152: s = "invalid Guard"; break; - case 153: s = "invalid LabelOrAssign"; break; - case 154: s = "invalid CallParams"; break; - case 155: s = "invalid EquivOp"; break; - case 156: s = "invalid ImpliesOp"; break; - case 157: s = "invalid ExpliesOp"; break; - case 158: s = "invalid AndOp"; break; - case 159: s = "invalid OrOp"; break; - case 160: s = "invalid RelOp"; break; - case 161: s = "invalid AddOp"; break; - case 162: s = "invalid MulOp"; break; - case 163: s = "invalid UnaryExpression"; break; - case 164: s = "invalid NegOp"; break; - case 165: s = "invalid CoercionExpression"; break; - case 166: s = "invalid ArrayExpression"; break; + case 39: s = "\"action\" expected"; break; + case 40: s = "\"refines\" expected"; break; + case 41: s = "\"left\" expected"; break; + case 42: s = "\"right\" expected"; break; + case 43: s = "\"both\" expected"; break; + case 44: s = "\"atomic\" expected"; break; + case 45: s = "\"procedure\" expected"; break; + case 46: s = "\"asserts\" expected"; break; + case 47: s = "\"requires\" expected"; break; + case 48: s = "\"ensures\" expected"; break; + case 49: s = "\"implementation\" expected"; break; + case 50: s = "\"free\" expected"; break; + case 51: s = "\"modifies\" expected"; break; + case 52: s = "\"goto\" expected"; break; + case 53: s = "\"return\" expected"; break; + case 54: s = "\"if\" expected"; break; + case 55: s = "\"else\" expected"; break; + case 56: s = "\"while\" expected"; break; + case 57: s = "\"*\" expected"; break; + case 58: s = "\"break\" expected"; break; + case 59: s = "\"reveal\" expected"; break; + case 60: s = "\"hide\" expected"; break; + case 61: s = "\"pop\" expected"; break; + case 62: s = "\"push\" expected"; break; + case 63: s = "\"assert\" expected"; break; + case 64: s = "\"assume\" expected"; break; + case 65: s = "\"havoc\" expected"; break; + case 66: s = "\":=\" expected"; break; + case 67: s = "\"->\" expected"; break; + case 68: s = "\"async\" expected"; break; + case 69: s = "\"call\" expected"; break; + case 70: s = "\"|\" expected"; break; + case 71: s = "\"<==>\" expected"; break; + case 72: s = "\"\\u21d4\" expected"; break; + case 73: s = "\"==>\" expected"; break; + case 74: s = "\"\\u21d2\" expected"; break; + case 75: s = "\"<==\" expected"; break; + case 76: s = "\"\\u21d0\" expected"; break; + case 77: s = "\"&&\" expected"; break; + case 78: s = "\"\\u2227\" expected"; break; + case 79: s = "\"||\" expected"; break; + case 80: s = "\"\\u2228\" expected"; break; + case 81: s = "\"==\" expected"; break; + case 82: s = "\"<=\" expected"; break; + case 83: s = "\">=\" expected"; break; + case 84: s = "\"!=\" expected"; break; + case 85: s = "\"\\u2260\" expected"; break; + case 86: s = "\"\\u2264\" expected"; break; + case 87: s = "\"\\u2265\" expected"; break; + case 88: s = "\"++\" expected"; break; + case 89: s = "\"+\" expected"; break; + case 90: s = "\"-\" expected"; break; + case 91: s = "\"div\" expected"; break; + case 92: s = "\"mod\" expected"; break; + case 93: s = "\"/\" expected"; break; + case 94: s = "\"**\" expected"; break; + case 95: s = "\"is\" expected"; break; + case 96: s = "\"!\" expected"; break; + case 97: s = "\"\\u00ac\" expected"; break; + case 98: s = "\"false\" expected"; break; + case 99: s = "\"true\" expected"; break; + case 100: s = "\"roundNearestTiesToEven\" expected"; break; + case 101: s = "\"RNE\" expected"; break; + case 102: s = "\"roundNearestTiesToAway\" expected"; break; + case 103: s = "\"RNA\" expected"; break; + case 104: s = "\"roundTowardPositive\" expected"; break; + case 105: s = "\"RTP\" expected"; break; + case 106: s = "\"roundTowardNegative\" expected"; break; + case 107: s = "\"RTN\" expected"; break; + case 108: s = "\"roundTowardZero\" expected"; break; + case 109: s = "\"RTZ\" expected"; break; + case 110: s = "\"old\" expected"; break; + case 111: s = "\"|{\" expected"; break; + case 112: s = "\"}|\" expected"; break; + case 113: s = "\"then\" expected"; break; + case 114: s = "\"forall\" expected"; break; + case 115: s = "\"\\u2200\" expected"; break; + case 116: s = "\"exists\" expected"; break; + case 117: s = "\"\\u2203\" expected"; break; + case 118: s = "\"lambda\" expected"; break; + case 119: s = "\"\\u03bb\" expected"; break; + case 120: s = "\"::\" expected"; break; + case 121: s = "\"\\u2022\" expected"; break; + case 122: s = "??? expected"; break; + case 123: s = "invalid BoogiePL"; break; + case 124: s = "invalid BoogiePL"; break; + case 125: s = "invalid Consts"; break; + case 126: s = "invalid Function"; break; + case 127: s = "invalid Function"; break; + case 128: s = "invalid YieldProcedureDecl"; break; + case 129: s = "invalid Procedure"; break; + case 130: s = "invalid ActionDecl"; break; + case 131: s = "invalid Type"; break; + case 132: s = "invalid TypeAtom"; break; + case 133: s = "invalid Ident"; break; + case 134: s = "invalid TypeArgs"; break; + case 135: s = "invalid MoverQualifier"; break; + case 136: s = "invalid SpecAction"; break; + case 137: s = "invalid SpecRefinedActionForYieldProcedure"; break; + case 138: s = "invalid SpecYieldRequires"; break; + case 139: s = "invalid SpecYieldPrePost"; break; + case 140: s = "invalid SpecYieldPreserves"; break; + case 141: s = "invalid SpecYieldEnsures"; break; + case 142: s = "invalid Spec"; break; + case 143: s = "invalid SpecPrePost"; break; + case 144: s = "invalid LabelOrCmd"; break; + case 145: s = "invalid LabelOrCmd"; break; + case 146: s = "invalid StructuredCmd"; break; + case 147: s = "invalid TransferCmd"; break; + case 148: s = "invalid IfCmd"; break; + case 149: s = "invalid WhileCmd"; break; + case 150: s = "invalid Guard"; break; + case 151: s = "invalid LabelOrAssign"; break; + case 152: s = "invalid CallParams"; break; + case 153: s = "invalid EquivOp"; break; + case 154: s = "invalid ImpliesOp"; break; + case 155: s = "invalid ExpliesOp"; break; + case 156: s = "invalid AndOp"; break; + case 157: s = "invalid OrOp"; break; + case 158: s = "invalid RelOp"; break; + case 159: s = "invalid AddOp"; break; + case 160: s = "invalid MulOp"; break; + case 161: s = "invalid UnaryExpression"; break; + case 162: s = "invalid NegOp"; break; + case 163: s = "invalid CoercionExpression"; break; + case 164: s = "invalid ArrayExpression"; break; + case 165: s = "invalid AtomExpression"; break; + case 166: s = "invalid AtomExpression"; break; case 167: s = "invalid AtomExpression"; break; - case 168: s = "invalid AtomExpression"; break; - case 169: s = "invalid AtomExpression"; break; - case 170: s = "invalid Dec"; break; - case 171: s = "invalid Forall"; break; - case 172: s = "invalid QuantifierBody"; break; - case 173: s = "invalid Exists"; break; - case 174: s = "invalid Lambda"; break; - case 175: s = "invalid SpecBlock"; break; - case 176: s = "invalid AttributeOrTrigger"; break; - case 177: s = "invalid AttributeParameter"; break; - case 178: s = "invalid QSep"; break; + case 168: s = "invalid Dec"; break; + case 169: s = "invalid Forall"; break; + case 170: s = "invalid QuantifierBody"; break; + case 171: s = "invalid Exists"; break; + case 172: s = "invalid Lambda"; break; + case 173: s = "invalid SpecBlock"; break; + case 174: s = "invalid AttributeOrTrigger"; break; + case 175: s = "invalid AttributeParameter"; break; + case 176: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index 0d50aa106..28a8299fa 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -220,8 +220,8 @@ public override int Read() { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 124; - const int noSym = 124; + const int maxT = 122; + const int noSym = 122; [ContractInvariantMethod] @@ -532,56 +532,54 @@ void CheckLiteral() { case "invariant": t.kind = 36; break; case "preserves": t.kind = 37; break; case "pure": t.kind = 38; break; - case "async": t.kind = 39; break; - case "action": t.kind = 40; break; - case "creates": t.kind = 41; break; - case "refines": t.kind = 42; break; - case "using": t.kind = 43; break; - case "left": t.kind = 44; break; - case "right": t.kind = 45; break; - case "both": t.kind = 46; break; - case "atomic": t.kind = 47; break; - case "procedure": t.kind = 48; break; - case "asserts": t.kind = 49; break; - case "requires": t.kind = 50; break; - case "ensures": t.kind = 51; break; - case "implementation": t.kind = 52; break; - case "free": t.kind = 53; break; - case "modifies": t.kind = 54; break; - case "goto": t.kind = 55; break; - case "return": t.kind = 56; break; - case "if": t.kind = 57; break; - case "else": t.kind = 58; break; - case "while": t.kind = 59; break; - case "break": t.kind = 61; break; - case "reveal": t.kind = 62; break; - case "hide": t.kind = 63; break; - case "pop": t.kind = 64; break; - case "push": t.kind = 65; break; - case "assert": t.kind = 66; break; - case "assume": t.kind = 67; break; - case "havoc": t.kind = 68; break; - case "call": t.kind = 71; break; - case "div": t.kind = 93; break; - case "mod": t.kind = 94; break; - case "is": t.kind = 97; break; - case "false": t.kind = 100; break; - case "true": t.kind = 101; break; - case "roundNearestTiesToEven": t.kind = 102; break; - case "RNE": t.kind = 103; break; - case "roundNearestTiesToAway": t.kind = 104; break; - case "RNA": t.kind = 105; break; - case "roundTowardPositive": t.kind = 106; break; - case "RTP": t.kind = 107; break; - case "roundTowardNegative": t.kind = 108; break; - case "RTN": t.kind = 109; break; - case "roundTowardZero": t.kind = 110; break; - case "RTZ": t.kind = 111; break; - case "old": t.kind = 112; break; - case "then": t.kind = 115; break; - case "forall": t.kind = 116; break; - case "exists": t.kind = 118; break; - case "lambda": t.kind = 120; break; + case "action": t.kind = 39; break; + case "refines": t.kind = 40; break; + case "left": t.kind = 41; break; + case "right": t.kind = 42; break; + case "both": t.kind = 43; break; + case "atomic": t.kind = 44; break; + case "procedure": t.kind = 45; break; + case "asserts": t.kind = 46; break; + case "requires": t.kind = 47; break; + case "ensures": t.kind = 48; break; + case "implementation": t.kind = 49; break; + case "free": t.kind = 50; break; + case "modifies": t.kind = 51; break; + case "goto": t.kind = 52; break; + case "return": t.kind = 53; break; + case "if": t.kind = 54; break; + case "else": t.kind = 55; break; + case "while": t.kind = 56; break; + case "break": t.kind = 58; break; + case "reveal": t.kind = 59; break; + case "hide": t.kind = 60; break; + case "pop": t.kind = 61; break; + case "push": t.kind = 62; break; + case "assert": t.kind = 63; break; + case "assume": t.kind = 64; break; + case "havoc": t.kind = 65; break; + case "async": t.kind = 68; break; + case "call": t.kind = 69; break; + case "div": t.kind = 91; break; + case "mod": t.kind = 92; break; + case "is": t.kind = 95; break; + case "false": t.kind = 98; break; + case "true": t.kind = 99; break; + case "roundNearestTiesToEven": t.kind = 100; break; + case "RNE": t.kind = 101; break; + case "roundNearestTiesToAway": t.kind = 102; break; + case "RNA": t.kind = 103; break; + case "roundTowardPositive": t.kind = 104; break; + case "RTP": t.kind = 105; break; + case "roundTowardNegative": t.kind = 106; break; + case "RTN": t.kind = 107; break; + case "roundTowardZero": t.kind = 108; break; + case "RTZ": t.kind = 109; break; + case "old": t.kind = 110; break; + case "then": t.kind = 113; break; + case "forall": t.kind = 114; break; + case "exists": t.kind = 116; break; + case "lambda": t.kind = 118; break; default: break; } } @@ -865,67 +863,67 @@ Token NextToken() { case 67: {t.kind = 26; break;} case 68: - {t.kind = 69; break;} + {t.kind = 66; break;} case 69: - {t.kind = 70; break;} + {t.kind = 67; break;} case 70: - {t.kind = 73; break;} + {t.kind = 71; break;} case 71: - {t.kind = 74; break;} + {t.kind = 72; break;} case 72: - {t.kind = 75; break;} + {t.kind = 73; break;} case 73: - {t.kind = 76; break;} + {t.kind = 74; break;} case 74: - {t.kind = 78; break;} + {t.kind = 76; break;} case 75: if (ch == '&') {AddCh(); goto case 76;} else {goto case 0;} case 76: - {t.kind = 79; break;} + {t.kind = 77; break;} case 77: - {t.kind = 80; break;} + {t.kind = 78; break;} case 78: - {t.kind = 81; break;} + {t.kind = 79; break;} case 79: - {t.kind = 82; break;} + {t.kind = 80; break;} case 80: - {t.kind = 85; break;} + {t.kind = 83; break;} case 81: - {t.kind = 86; break;} + {t.kind = 84; break;} case 82: - {t.kind = 87; break;} + {t.kind = 85; break;} case 83: - {t.kind = 88; break;} + {t.kind = 86; break;} case 84: - {t.kind = 89; break;} + {t.kind = 87; break;} case 85: - {t.kind = 90; break;} + {t.kind = 88; break;} case 86: - {t.kind = 95; break;} + {t.kind = 93; break;} case 87: - {t.kind = 96; break;} + {t.kind = 94; break;} case 88: - {t.kind = 99; break;} + {t.kind = 97; break;} case 89: - {t.kind = 113; break;} + {t.kind = 111; break;} case 90: - {t.kind = 114; break;} + {t.kind = 112; break;} case 91: - {t.kind = 117; break;} + {t.kind = 115; break;} case 92: - {t.kind = 119; break;} + {t.kind = 117; break;} case 93: - {t.kind = 121; break;} + {t.kind = 119; break;} case 94: - {t.kind = 122; break;} + {t.kind = 120; break;} case 95: - {t.kind = 123; break;} + {t.kind = 121; break;} case 96: - recEnd = pos; recKind = 92; + recEnd = pos; recKind = 90; if (ch == '0') {AddCh(); goto case 16;} else if (ch == '>') {AddCh(); goto case 69;} - else {t.kind = 92; break;} + else {t.kind = 90; break;} case 97: recEnd = pos; recKind = 13; if (ch == '=') {AddCh(); goto case 68;} @@ -948,34 +946,34 @@ Token NextToken() { if (ch == '=') {AddCh(); goto case 107;} else {t.kind = 34; break;} case 102: - recEnd = pos; recKind = 60; + recEnd = pos; recKind = 57; if (ch == '*') {AddCh(); goto case 87;} - else {t.kind = 60; break;} + else {t.kind = 57; break;} case 103: - recEnd = pos; recKind = 72; + recEnd = pos; recKind = 70; if (ch == '|') {AddCh(); goto case 78;} else if (ch == '{') {AddCh(); goto case 89;} - else {t.kind = 72; break;} + else {t.kind = 70; break;} case 104: - recEnd = pos; recKind = 98; + recEnd = pos; recKind = 96; if (ch == '=') {AddCh(); goto case 81;} - else {t.kind = 98; break;} + else {t.kind = 96; break;} case 105: - recEnd = pos; recKind = 91; + recEnd = pos; recKind = 89; if (ch == '+') {AddCh(); goto case 85;} - else {t.kind = 91; break;} + else {t.kind = 89; break;} case 106: - recEnd = pos; recKind = 84; + recEnd = pos; recKind = 82; if (ch == '=') {AddCh(); goto case 108;} - else {t.kind = 84; break;} + else {t.kind = 82; break;} case 107: - recEnd = pos; recKind = 83; + recEnd = pos; recKind = 81; if (ch == '>') {AddCh(); goto case 72;} - else {t.kind = 83; break;} + else {t.kind = 81; break;} case 108: - recEnd = pos; recKind = 77; + recEnd = pos; recKind = 75; if (ch == '>') {AddCh(); goto case 70;} - else {t.kind = 77; break;} + else {t.kind = 75; break;} } t.val = new String(tval, 0, tlen); diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 741b61e59..65ce28d99 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -672,18 +672,10 @@ public virtual ActionDeclRef VisitActionDeclRef(ActionDeclRef node) public virtual Procedure VisitActionDecl(ActionDecl node) { - for (int i = 0; i < node.Creates.Count; i++) - { - node.Creates[i] = VisitActionDeclRef(node.Creates[i]); - } if (node.RefinedAction != null) { node.RefinedAction = VisitActionDeclRef(node.RefinedAction); } - if (node.InvariantAction != null) - { - node.InvariantAction = VisitActionDeclRef(node.InvariantAction); - } node.YieldRequires = VisitCallCmdSeq(node.YieldRequires); node.Asserts = VisitAssertCmdSeq(node.Asserts); return VisitProcedure(node); diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index ba8e0559e..01eb323c1 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -324,12 +324,6 @@ pure procedure {:inline 1} TaggedLocs_New(tags: Set T) returns ({:linear} { tagged_locs := Set((lambda x: One (TaggedLoc V T) :: x->val->loc == l->val && Set_Contains(tags, x->val->tag))); } -/// Async primitives -procedure create_async(PA: T); -procedure create_asyncs(PAs: [T]bool); -procedure create_multi_asyncs(PAs: [T]int); -procedure set_choice(choice: T); - /// Helpers pure procedure Copy(v: T) returns (v': T); ensures v' == v; diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 1cebba64d..76495f045 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -452,11 +452,6 @@ public bool TrustInvariants { public int TrustLayersDownto { get; set; } = int.MaxValue; - public bool TrustSequentialization { - get => trustSequentialization; - set => trustSequentialization = value; - } - public bool RemoveEmptyBlocks { get; set; } = true; public bool CoalesceBlocks { get; set; } = true; public bool PruneInfeasibleEdges { get; set; } = true; @@ -599,7 +594,6 @@ void ObjectInvariant5() private bool trustNoninterference = false; private bool trustRefinement = false; private bool trustInvariants = false; - private bool trustSequentialization = false; private int enhancedErrorMessages = 0; private int stagedHoudiniThreads = 1; private uint timeLimitPerAssertionInPercent = 10; @@ -1391,7 +1385,6 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("trustNoninterference", x => trustNoninterference = x) || ps.CheckBooleanFlag("trustRefinement", x => trustRefinement = x) || ps.CheckBooleanFlag("trustInvariants", x => trustInvariants = x) || - ps.CheckBooleanFlag("trustSequentialization", x => trustSequentialization = x) || ps.CheckBooleanFlag("useBaseNameForFileName", x => UseBaseNameForFileName = x) || ps.CheckBooleanFlag("freeVarLambdaLifting", x => FreeVarLambdaLifting = x) || ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) || @@ -1745,9 +1738,6 @@ Yielding loop. {:hide} Hidden input/output parameter. - {:pending_async} - Local variable collecting pending asyncs in yielding procedure. - {:sync} Synchronized async call. @@ -1904,8 +1894,6 @@ print Boogie program after it has been instrumented with do not verify layers and below /trustLayersDownto: do not verify layers and above - /trustSequentialization - do not perform sequentialization checks /civlDesugaredFile: print plain Boogie program to diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 0f9353c28..269456785 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -874,7 +874,7 @@ public Element TryGet(string varname) public void AddBinding(string varname, Element value) { vars.Add(varname); - valuations.Add(varname, value); + valuations.Add(varname, value); // SQ: exception occurs if a global variable and a local variable have the same name } // Change name of the state diff --git a/Test/civl/regression-tests/NoChoice.bpl b/Test/civl/regression-tests/NoChoice.bpl deleted file mode 100644 index a74e1b6c6..000000000 --- a/Test/civl/regression-tests/NoChoice.bpl +++ /dev/null @@ -1,32 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0,2} x:int; - -//////////////////////////////////////////////////////////////////////////////// - -atomic action {:layer 1} MAIN () -refines MAIN'; -creates INC, DEC; -{ - async call INC(); - async call DEC(); -} - -atomic action {:layer 2} MAIN' () -{ -} - -//////////////////////////////////////////////////////////////////////////////// - -async left action {:layer 1} INC () -modifies x; -{ - x := x + 1; -} - -async left action {:layer 1} DEC () -modifies x; -{ - x := x - 1; -} diff --git a/Test/civl/regression-tests/NoChoice.bpl.expect b/Test/civl/regression-tests/NoChoice.bpl.expect deleted file mode 100644 index a9949f2e7..000000000 --- a/Test/civl/regression-tests/NoChoice.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/civl/regression-tests/Pure1.bpl b/Test/civl/regression-tests/Pure1.bpl deleted file mode 100644 index b40ed0594..000000000 --- a/Test/civl/regression-tests/Pure1.bpl +++ /dev/null @@ -1,30 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var x: int; - -pure action E() -modifies x; -{ - var c: int; - c := x; -} - -async atomic action A() -{ -} - -pure action F() -creates A; -{ -} - -pure action G(d: int) -{ - x := d; -} - -pure action H() returns (d: int) -{ - d := x; -} diff --git a/Test/civl/regression-tests/Pure1.bpl.expect b/Test/civl/regression-tests/Pure1.bpl.expect deleted file mode 100644 index eb479b558..000000000 --- a/Test/civl/regression-tests/Pure1.bpl.expect +++ /dev/null @@ -1,6 +0,0 @@ -Pure1.bpl(6,12): Error: unnecessary modifies clause for pure action -Pure1.bpl(10,9): Error: cannot refer to a global variable in this context: x -Pure1.bpl(17,12): Error: unnecessary creates clause for pure action -Pure1.bpl(24,4): Error: cannot refer to a global variable in this context: x -Pure1.bpl(29,9): Error: cannot refer to a global variable in this context: x -5 name resolution errors detected in Pure1.bpl diff --git a/Test/civl/regression-tests/async3.bpl b/Test/civl/regression-tests/async3.bpl deleted file mode 100644 index 23410343a..000000000 --- a/Test/civl/regression-tests/async3.bpl +++ /dev/null @@ -1,28 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0,3} x:int; - -yield procedure {:layer 2} Client () -refines A_Inc; -{ - call Service(); -} - -atomic action {:layer 1} A_Service() -refines A_Inc; -creates A_Inc; -{ - async call A_Inc(); -} -yield procedure {:layer 0} Service () -refines A_Service; -{ - async call Callback(); -} - -async both action {:layer 1,3} A_Inc () -modifies x; -{ x := x + 1; } -yield procedure {:layer 0} Callback (); -refines A_Inc; diff --git a/Test/civl/regression-tests/async3.bpl.expect b/Test/civl/regression-tests/async3.bpl.expect deleted file mode 100644 index 3e3dc54b2..000000000 --- a/Test/civl/regression-tests/async3.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 7 verified, 0 errors diff --git a/Test/civl/regression-tests/async4.bpl b/Test/civl/regression-tests/async4.bpl deleted file mode 100644 index 47abdfa6d..000000000 --- a/Test/civl/regression-tests/async4.bpl +++ /dev/null @@ -1,32 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0,2} x:int; - -both action {:layer 2} A_Add (n: int) -modifies x; -{ assert 0 <= n; x := x + n; } - -action {:layer 1} INV(n: int) -creates A_Inc; -modifies x; -{ - var {:pool "A"} i: int; - assert 0 <= n; - assume {:add_to_pool "A", i} {:add_to_pool "A", i+1} 0 <= i && i <= n; - x := x + i; - call create_multi_asyncs(MapConst(0)[A_Inc() := n - i]); -} - -atomic action {:layer 1} Async_Add(n: int) -refines A_Add using INV; -creates A_Inc; -{ - assert 0 <= n; - assume {:add_to_pool "A", 0} true; - call create_multi_asyncs(MapConst(0)[A_Inc() := n]); -} - -async both action {:layer 1,2} A_Inc () -modifies x; -{ x := x + 1; } diff --git a/Test/civl/regression-tests/async4.bpl.expect b/Test/civl/regression-tests/async4.bpl.expect deleted file mode 100644 index 9823d44a8..000000000 --- a/Test/civl/regression-tests/async4.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/regression-tests/hide-params-pa-2.bpl b/Test/civl/regression-tests/hide-params-pa-2.bpl deleted file mode 100644 index 31e369cbc..000000000 --- a/Test/civl/regression-tests/hide-params-pa-2.bpl +++ /dev/null @@ -1,25 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -atomic action {:layer 1,2} SPEC () -creates A; -{ - async call A(1); -} - -yield procedure {:layer 1} b () -refines SPEC; -{ - async call a(true, 1, 2.3); // This call is already to action A when it is turned into a pending async. -} - -yield procedure {:layer 0} c () -refines SPEC; -{ - async call a(true, 1, 2.3); // This call is still to procedure a when it is turned into a pending async. -} - -async atomic action {:layer 1,2} A (i:int) { } - -yield procedure {:layer 0} a ({:hide} b:bool, i:int, {:hide} r:real); -refines A; diff --git a/Test/civl/regression-tests/hide-params-pa-2.bpl.expect b/Test/civl/regression-tests/hide-params-pa-2.bpl.expect deleted file mode 100644 index 3e6d423af..000000000 --- a/Test/civl/regression-tests/hide-params-pa-2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/civl/regression-tests/hide-params-pa.bpl b/Test/civl/regression-tests/hide-params-pa.bpl deleted file mode 100644 index 7218b7216..000000000 --- a/Test/civl/regression-tests/hide-params-pa.bpl +++ /dev/null @@ -1,35 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -async atomic action {:layer 2} SKIP () returns () { } - -yield procedure {:layer 1} b () -refines SKIP; -{ - var {:layer 0} b:bool; - var {:layer 0} b':bool; - var i:int; - var i':int; - var {:layer 0} r:real; - var {:layer 0} r':real; - - i := 1; - call b', i', r' := a(b, i, r); - // at layer 1 this call must be rewritten to - // call i', returnedPAs := A(i); -} - -atomic action {:layer 1} A (i:int) returns (i':int) -{ - assert i > 0; - assume i' > i; -} - -// In the refinement checker for a, the remaining formals of A must be -// properly mapped to the matching formals in a. -yield procedure {:layer 0} -a ({:hide} b:bool, i:int, {:hide} r:real) returns ({:hide} b':bool, i':int, {:hide} r':real) -refines A; -{ - i' := i + 1; -} diff --git a/Test/civl/regression-tests/hide-params-pa.bpl.expect b/Test/civl/regression-tests/hide-params-pa.bpl.expect deleted file mode 100644 index 3e6d423af..000000000 --- a/Test/civl/regression-tests/hide-params-pa.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/civl/regression-tests/left-mover.bpl b/Test/civl/regression-tests/left-mover.bpl index 709171ade..66af45af8 100644 --- a/Test/civl/regression-tests/left-mover.bpl +++ b/Test/civl/regression-tests/left-mover.bpl @@ -32,7 +32,7 @@ asserts {:add_to_pool "A", i+1} true; assume j > i; } -pure action intro (x:int) +pure action intro (k: int) { - assume x == 0; + assume k == 0; } diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl b/Test/civl/regression-tests/pa-noninterference-check.bpl deleted file mode 100644 index 5f8ecfae7..000000000 --- a/Test/civl/regression-tests/pa-noninterference-check.bpl +++ /dev/null @@ -1,32 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -atomic action {:layer 3} A_Foo() -creates A_Incr; -{ - async call A_Incr(); -} - -yield procedure {:layer 2} Foo() -refines A_Foo; -{ - async call Incr(); -} - -async atomic action {:layer 1,3} A_Incr() -modifies x; -{ - x := x + 1; -} - -yield procedure {:layer 0} Incr(); -refines A_Incr; - -yield invariant {:layer 1} Inv(); -preserves x == 0; - -var {:layer 0,3} x: int; - -yield procedure {:layer 1} Bar() -preserves call Inv(); -{ } diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect deleted file mode 100644 index 9a1d9163f..000000000 --- a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect +++ /dev/null @@ -1,7 +0,0 @@ -pa-noninterference-check.bpl(26,1): Error: Non-interference check failed -Execution trace: - pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Entry - pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0 - pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return - -Boogie program verifier finished with 5 verified, 1 error diff --git a/Test/civl/regression-tests/pending-async-1.bpl b/Test/civl/regression-tests/pending-async-1.bpl deleted file mode 100644 index cb5d23783..000000000 --- a/Test/civl/regression-tests/pending-async-1.bpl +++ /dev/null @@ -1,106 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -//////////////////////////////////////////////////////////////////////////////// - -async atomic action {:layer 1,2} A () {} - -left action {:layer 1} B () -creates A; -{ - async call A(); -} - -left action {:layer 1} C (flag:bool) -creates A; -{ - if (flag) { - async call A(); - } -} - -yield procedure {:layer 0} b (); -refines B; - -yield procedure {:layer 0} c (flag:bool); -refines C; - - -//////////////////////////////////////////////////////////////////////////////// - -// Verifies -yield procedure {:layer 1} test1 () -refines TEST1; -{ - call b(); - call b(); -} - -atomic action {:layer 2} TEST1 () -creates A; -{ - call create_multi_asyncs(MapConst(0)[A() := 2]); -} - -//////////////////////////////////////////////////////////////////////////////// - -// Fails -yield procedure {:layer 1} test2 () -refines TEST2; -{ - call b(); - call b(); -} - -atomic action {:layer 2} TEST2 () -creates A; -{ - async call A(); -} - -//////////////////////////////////////////////////////////////////////////////// - -// Fails -yield procedure {:layer 1} test3 () -refines TEST3; -{ - call c(true); -} - -atomic action {:layer 2} TEST3 () returns () {} - -//////////////////////////////////////////////////////////////////////////////// - -// Verifies -yield procedure {:layer 1} test4 () -refines TEST4; -{ - call c(false); -} - -atomic action {:layer 2} TEST4 () returns () {} - -//////////////////////////////////////////////////////////////////////////////// - -// Verifies -yield procedure {:layer 1} test5 () -refines TEST5; -{ - var i:int; - var {:pending_async}{:layer 1} PAs:[A]int; - - i := 0; - while (i < 10) - invariant {:layer 1} 0 <= i && i <= 10; - invariant {:layer 1} PAs == MapConst(0)[A() := i]; - { - call b(); - i := i + 1; - } -} - -atomic action {:layer 2} TEST5 () -creates A; -{ - call create_multi_asyncs(MapConst(0)[A() := 10]); -} diff --git a/Test/civl/regression-tests/pending-async-1.bpl.expect b/Test/civl/regression-tests/pending-async-1.bpl.expect deleted file mode 100644 index 514dcb05b..000000000 --- a/Test/civl/regression-tests/pending-async-1.bpl.expect +++ /dev/null @@ -1,16 +0,0 @@ -pending-async-1.bpl(48,28): Error: On some path no yield-to-yield fragment matched the refined atomic action -Execution trace: - pending-async-1.bpl(51,3): anon0 - pending-async-1.bpl(11,9): inline$B$0$anon0 - pending-async-1.bpl(51,3): anon0$1 - pending-async-1.bpl(11,9): inline$B$1$anon0 - pending-async-1.bpl(51,3): anon0$2 - (0,0): Civl_ReturnChecker -pending-async-1.bpl(67,3): Error: Pending asyncs to action A created by this call are not summarized -Execution trace: - pending-async-1.bpl(67,3): anon0 - pending-async-1.bpl(17,3): inline$C$0$anon0 - pending-async-1.bpl(18,11): inline$C$0$anon2_Then - pending-async-1.bpl(67,3): anon0$1 - -Boogie program verifier finished with 9 verified, 2 errors diff --git a/Test/civl/regression-tests/pending-async-2.bpl b/Test/civl/regression-tests/pending-async-2.bpl deleted file mode 100644 index d59c814c9..000000000 --- a/Test/civl/regression-tests/pending-async-2.bpl +++ /dev/null @@ -1,24 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -const n:int; -axiom n > 0; - -//////////////////////////////////////////////////////////////////////////////// - -async atomic action {:layer 1} A () {} -async atomic action {:layer 1} B () {} - -left action {:layer 1} C () -creates A; -{ - async call A(); - // create undeclared pending async to B - async call B(); -} - -left action {:layer 1} D () -creates A, B; -{ - // do nothing -} diff --git a/Test/civl/regression-tests/pending-async-2.bpl.expect b/Test/civl/regression-tests/pending-async-2.bpl.expect deleted file mode 100644 index e5c2e070d..000000000 --- a/Test/civl/regression-tests/pending-async-2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -pending-async-2.bpl(17,8): Error: pending async must be in the creates clause of caller -1 type checking errors detected in pending-async-2.bpl diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl deleted file mode 100644 index 551338913..000000000 --- a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl +++ /dev/null @@ -1,21 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0,1} x:int; - -yield invariant {:layer 1} yield_x(n: int); -preserves x >= n; - -async atomic action {:layer 1} A () -modifies x; -{ - x := x - 1; -} - -left action {:layer 1} ASYNC_A () -creates A; -{ - async call A(); -} - -yield procedure {:layer 1} dummy () {} diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect deleted file mode 100644 index a5a1e46d9..000000000 --- a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect +++ /dev/null @@ -1,7 +0,0 @@ -pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed -Execution trace: - pending-async-noninterference-fail.bpl(9,32): inline$A$0$Entry - pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0 - pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return - -Boogie program verifier finished with 2 verified, 1 error diff --git a/Test/civl/regression-tests/pending-async-noninterference-linear.bpl b/Test/civl/regression-tests/pending-async-noninterference-linear.bpl deleted file mode 100644 index 502d6a701..000000000 --- a/Test/civl/regression-tests/pending-async-noninterference-linear.bpl +++ /dev/null @@ -1,21 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0,1} x:[int]int; - -yield invariant {:layer 1} yield_x({:linear} tid: One int); -preserves x[tid->val] == 0; - -async atomic action {:layer 1} A ({:linear} tid: One int) -modifies x; -{ - x[tid->val] := 1; -} - -left action {:layer 1} ASYNC_A ({:linear_in} tid: One int) - creates A; -{ - async call A(tid); -} - -yield procedure {:layer 1} dummy () {} diff --git a/Test/civl/regression-tests/pending-async-noninterference-linear.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-linear.bpl.expect deleted file mode 100644 index a9949f2e7..000000000 --- a/Test/civl/regression-tests/pending-async-noninterference-linear.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/civl/regression-tests/pending-async-noninterference-ok.bpl b/Test/civl/regression-tests/pending-async-noninterference-ok.bpl deleted file mode 100644 index d68c5e8fe..000000000 --- a/Test/civl/regression-tests/pending-async-noninterference-ok.bpl +++ /dev/null @@ -1,21 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0,1} x:int; - -yield invariant {:layer 1} yield_x(n: int); -preserves x >= n; - -async atomic action {:layer 1} A () -modifies x; -{ - x := x + 1; -} - -left action {:layer 1} ASYNC_A () -creates A; -{ - async call A(); -} - -yield procedure {:layer 1} dummy () {} diff --git a/Test/civl/regression-tests/pending-async-noninterference-ok.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-ok.bpl.expect deleted file mode 100644 index a9949f2e7..000000000 --- a/Test/civl/regression-tests/pending-async-noninterference-ok.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/civl/regression-tests/rec-IS1.bpl b/Test/civl/regression-tests/rec-IS1.bpl deleted file mode 100644 index 748499a9a..000000000 --- a/Test/civl/regression-tests/rec-IS1.bpl +++ /dev/null @@ -1,30 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:linear} g: One int; - -async left action {:layer 1} main_f''({:linear_in} l: One int) -refines final using Inv; -creates main_f''; -{ - if (*) { - } else { - async call main_f''(l); - } -} - -action {:layer 2} final({:linear_in} l: One int) -{ - // conclusion check succeeds due to disjointness assumption -} - -action {:layer 1} Inv({:linear_in} l: One int) -creates main_f''; -{ - assert l != g; - if (*) { - } else { - async call main_f''(l); - call set_choice(main_f''(l)); - } -} \ No newline at end of file diff --git a/Test/civl/regression-tests/rec-IS1.bpl.expect b/Test/civl/regression-tests/rec-IS1.bpl.expect deleted file mode 100644 index a9949f2e7..000000000 --- a/Test/civl/regression-tests/rec-IS1.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/civl/samples/lock-service.bpl b/Test/civl/samples/lock-service.bpl deleted file mode 100644 index d3bce276e..000000000 --- a/Test/civl/samples/lock-service.bpl +++ /dev/null @@ -1,139 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type Tid = int; - -const nil:Tid; -var {:layer 0,4} l:Tid; -var {:layer 0,5} x:int; - -atomic action {:layer 5} A_Client () -modifies x; -{ - x := x + 1; -} -yield procedure {:layer 4} Client({:hide}{:linear_in} tid: One Tid) -refines A_Client; -requires {:layer 4} tid->val != nil; -{ - call GetLockAndCallback(tid); -} - -atomic action {:layer 4} A_GetLockAndCallback' ({:linear_in} tid: One Tid) -modifies x; -{ - assert tid->val != nil; - x := x + 1; -} - -async left action {:layer 3} A_Callback ({:linear_in} tid: One Tid) -modifies l, x; -{ - assert tid->val != nil && l == tid->val; - x := x + 1; - l := nil; -} -yield procedure {:layer 2} Callback ({:linear_in} tid: One Tid) -refines A_Callback; -{ - var tmp:int; - call tmp := read_x_lock(tid); - call write_x_lock(tmp+1, tid); - async call {:sync} ReleaseLock(tid); -} - -both action {:layer 2} A_read_x_lock ({:linear} tid: One Tid) returns (v:int) -{ assert tid->val != nil && l == tid->val; v := x; } -yield procedure {:layer 1} read_x_lock ({:linear} tid: One Tid) returns (v:int) -refines A_read_x_lock; -{ call v := read_x(); } - -both action {:layer 2} A_write_x_lock (v:int, {:linear} tid: One Tid) -modifies x; -{ assert tid->val != nil && l == tid->val; x := v; } -yield procedure {:layer 1} write_x_lock (v:int, {:linear} tid: One Tid) -refines A_write_x_lock; -{ call write_x(v); } - -atomic action {:layer 1} A_read_x () returns (v:int) -{ v := x; } -yield procedure {:layer 0} read_x () returns (v:int); -refines A_read_x; - -atomic action {:layer 1} A_write_x (v:int) -modifies x; -{ x := v; } -yield procedure {:layer 0} write_x (v:int); -refines A_write_x; - -// ----------------------------------------------------------------------------- - -atomic action {:layer 3} -A_GetLockAndCallback ({:linear_in} tid: One Tid) -refines A_GetLockAndCallback'; -creates A_Callback; -modifies l; -{ - assert tid->val != nil; - assume l == nil; - l := tid->val; - async call A_Callback(tid); -} -yield procedure {:layer 2} GetLockAndCallback ({:linear_in} tid: One Tid) -refines A_GetLockAndCallback; -{ - call GetLock(tid); - async call Callback(tid); -} - -atomic action {:layer 2} A_GetLock ({:linear} tid: One Tid) -modifies l; -{ - assert tid->val != nil; - assume l == nil; - l := tid->val; -} -yield procedure {:layer 1} GetLock ({:linear} tid: One Tid) -refines A_GetLock; -{ - var success:bool; - while (true) - invariant {:yields} true; - { - call success := cas_l(nil, tid->val); - if (success) { - return; - } - } -} - -left action {:layer 2} A_ReleaseLock ({:linear_in} tid: One Tid) -modifies l; -{ - assert tid->val != nil && l == tid->val; - l := nil; -} -yield procedure {:layer 1} ReleaseLock ({:linear_in} tid: One Tid) -refines A_ReleaseLock; -{ - call write_l(nil); -} - -atomic action {:layer 1} A_cas_l (oldval:Tid, newval:Tid) returns (success:bool) -modifies l; -{ - if (l == oldval) { - l := newval; - success := true; - } else { - success := false; - } -} -yield procedure {:layer 0} cas_l (oldval:Tid, newval:Tid) returns (success:bool); -refines A_cas_l; - -atomic action {:layer 1} A_write_l (v:Tid) -modifies l; -{ l := v; } -yield procedure {:layer 0} write_l (v:Tid); -refines A_write_l; diff --git a/Test/civl/samples/lock-service.bpl.expect b/Test/civl/samples/lock-service.bpl.expect deleted file mode 100644 index 129e60e25..000000000 --- a/Test/civl/samples/lock-service.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 39 verified, 0 errors