From c415283fcb6ff8c454549586f89c094a9a69988d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 26 Aug 2024 14:57:07 +0200 Subject: [PATCH 1/9] Add 'check' commands, a variation of assert command --- Source/Core/AST/AbsyCmd.cs | 10 +- Source/Core/BoogiePL.atg | 4 + Source/Core/Parser.cs | 550 +++++++++--------- Source/Core/Scanner.cs | 135 ++--- Source/VCGeneration/CommandTransformations.cs | 13 +- Source/VCGeneration/FocusAttribute.cs | 2 +- Source/VCGeneration/ManualSplitFinder.cs | 15 +- .../VerificationConditionGenerator.cs | 4 - Test/test0/Split/Foo.split.1.bpl.expect | 2 +- Test/test0/Split/Foo.split.2.bpl.expect | 2 +- Test/test0/Split/Foo.split.3.bpl.expect | 2 - Test/test0/Split/Split.bpl | 4 +- 12 files changed, 384 insertions(+), 359 deletions(-) diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 3583e68b5..5d55ff98a 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -2995,8 +2995,12 @@ public EEDTemplate(string reason, List /*!*/ exprList) } } - public class AssertCmd : PredicateCmd - { + public class AssertCmd : PredicateCmd { + /// + /// Whether to remember the asserted fact, after it has been asserted + /// Particularly relevant when doing splits + /// + public bool Remember { get; set; } = true; public Expr OrigExpr; public Dictionary IncarnationMap; @@ -3048,7 +3052,7 @@ public AssertCmd(IToken tok, Expr expr, QKeyValue kv = null) public override void Emit(TokenTextWriter stream, int level) { - stream.Write(this, level, "assert "); + stream.Write(this, level, Remember ? "assert " : "check "); EmitAttributes(stream, Attributes); this.Expr.Emit(stream); stream.WriteLine(";"); diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 66c5789aa..956787fc5 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1149,6 +1149,10 @@ LabelOrCmd { Attribute } Proposition (. c = new AssertCmd(x, e, kv); .) ";" + | "check" (. x = t; .) + { Attribute } + Proposition (. c = new AssertCmd(x, e, kv) { Remember = false }; .) + ";" | "assume" (. x = t; .) { Attribute } Proposition (. c = new AssumeCmd(x, e, kv); .) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 0094b0fc3..f7e4d9dc2 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -36,7 +36,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 = 125; const bool _T = true; const bool _x = false; @@ -304,7 +304,7 @@ void BoogiePL() { Pgm.AddTopLevelDeclaration(im); } - } else SynErr(125); + } else SynErr(126); break; } case 36: case 37: case 38: case 42: case 43: case 44: case 45: case 46: { @@ -328,7 +328,7 @@ void BoogiePL() { } isPure = false; - } else SynErr(126); + } else SynErr(127); break; } case 51: { @@ -367,7 +367,7 @@ void Consts(out List/*!*/ ds) { axioms.Add(axiom); ds.Add(axiom); } Expect(27); - } else SynErr(127); + } else SynErr(128); foreach(TypedIdent/*!*/ x in xs){ Contract.Assert(x != null); var constant = new Constant(y, x, u, kv, axioms); @@ -421,7 +421,7 @@ void Function(out List/*!*/ ds) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(128); + } else SynErr(129); if (la.kind == 26) { Get(); Expression(out tmp); @@ -446,7 +446,7 @@ void Function(out List/*!*/ ds) { Expect(27); } else if (la.kind == 10) { Get(); - } else SynErr(129); + } else SynErr(130); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -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(131); ypDecl = new YieldProcedureDecl(name, name.val, moverType, ins, outs, pre, mods, post, yieldRequires, yieldEnsures, yieldPreserves, refinedAction, kv); } @@ -670,7 +670,7 @@ void Procedure(bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implemen 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(132); proc = new Procedure(x, x.val, typeParams, ins, outs, isPure, pre, mods, post, kv); } @@ -722,7 +722,7 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, 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(132); + } else SynErr(133); if (isPure) { if (moverType == MoverType.None) { @@ -860,7 +860,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(134); } void AttributesIdsTypeWhere(bool allowWhereClauses, string context, System.Action action ) { @@ -896,7 +896,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(137); } void MapType(out Bpl.Type/*!*/ ty) { @@ -1156,7 +1156,7 @@ void MoverQualifier(ref MoverType moverType) { } else if (la.kind == 45) { Get(); moverType = MoverType.Atomic; - } else SynErr(137); + } else SynErr(138); } void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List mods, List creates, List requires, List yieldRequires, List asserts) { @@ -1177,7 +1177,7 @@ void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantActi SpecYieldRequires(requires, yieldRequires); } else if (la.kind == 47) { SpecAsserts(asserts); - } else SynErr(138); + } else SynErr(139); } void ImplBody(out List/*!*/ locals, out StmtList/*!*/ stmtList) { @@ -1232,10 +1232,10 @@ void SpecYieldRequires(List pre, List yieldRequires ) { } Proposition(out e); pre.Add(new Requires(tok, false, e, null, kv)); - } else if (la.kind == 37 || la.kind == 52 || la.kind == 70) { + } else if (la.kind == 37 || la.kind == 52 || la.kind == 71) { CallCmd(out cmd); yieldRequires.Add((CallCmd)cmd); - } else SynErr(139); + } else SynErr(140); Expect(10); } @@ -1263,7 +1263,7 @@ void SpecYieldPrePost(ref ActionDeclRef refinedAction, List pre, List< SpecYieldPreserves(yieldPreserves); } else if (la.kind == 53) { SpecModifies(mods); - } else SynErr(140); + } else SynErr(141); } void CallCmd(out Cmd c) { @@ -1281,7 +1281,7 @@ void CallCmd(out Cmd c) { Get(); isFree = true; } - Expect(70); + Expect(71); x = t; CallParams(isAsync, isFree, x, out c); @@ -1297,10 +1297,10 @@ void SpecYieldEnsures(List post, List yieldEnsures ) { } Proposition(out e); post.Add(new Ensures(tok, false, e, null, kv)); - } else if (la.kind == 37 || la.kind == 52 || la.kind == 70) { + } else if (la.kind == 37 || la.kind == 52 || la.kind == 71) { CallCmd(out cmd); yieldEnsures.Add((CallCmd)cmd); - } else SynErr(141); + } else SynErr(142); Expect(10); } @@ -1340,7 +1340,7 @@ void Spec(List pre, List mods, List post) { SpecPrePost(true, pre, post); } else if (la.kind == 48 || la.kind == 49) { SpecPrePost(false, pre, post); - } else SynErr(142); + } else SynErr(143); } void SpecPrePost(bool free, List/*!*/ pre, List/*!*/ post) { @@ -1363,7 +1363,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(143); + } else SynErr(144); } void StmtList(out StmtList/*!*/ stmtList) { @@ -1457,7 +1457,7 @@ void LabelOrCmd(out Cmd c, out IToken label) { hideRevealId = new IdentifierExpr(t, t.val); } else if (la.kind == 59) { Get(); - } else SynErr(144); + } else SynErr(145); c = hideRevealId == null ? new HideRevealCmd(t, mode) : new HideRevealCmd(hideRevealId, mode); Expect(10); } else if (la.kind == 63) { @@ -1486,9 +1486,18 @@ void LabelOrCmd(out Cmd c, out IToken label) { Attribute(ref kv); } Proposition(out e); - c = new AssumeCmd(x, e, kv); + c = new AssertCmd(x, e, kv) { Remember = false }; Expect(10); } else if (la.kind == 67) { + Get(); + x = t; + while (la.kind == 26) { + Attribute(ref kv); + } + Proposition(out e); + c = new AssumeCmd(x, e, kv); + Expect(10); + } else if (la.kind == 68) { Get(); x = t; Idents(out xs); @@ -1500,14 +1509,14 @@ void LabelOrCmd(out Cmd c, out IToken label) { } c = new HavocCmd(x,ids); - } else if (la.kind == 37 || la.kind == 52 || la.kind == 70) { + } else if (la.kind == 37 || la.kind == 52 || la.kind == 71) { CallCmd(out cn); Expect(10); c = cn; - } else if (la.kind == 71) { + } else if (la.kind == 72) { ParCallCmd(out cn); c = cn; - } else SynErr(145); + } else SynErr(146); } void StructuredCmd(out StructuredCmd/*!*/ ec) { @@ -1523,7 +1532,7 @@ void StructuredCmd(out StructuredCmd/*!*/ ec) { } else if (la.kind == 60) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(146); + } else SynErr(147); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1543,7 +1552,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) { } else if (la.kind == 55) { Get(); tc = new ReturnCmd(t); - } else SynErr(147); + } else SynErr(148); Expect(10); } @@ -1568,7 +1577,7 @@ void IfCmd(out IfCmd/*!*/ ifcmd) { Get(); StmtList(out els); elseOption = els; - } else SynErr(148); + } else SynErr(149); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1604,10 +1613,10 @@ void WhileCmd(out WhileCmd wcmd) { } kv = null; - } else if (la.kind == 37 || la.kind == 52 || la.kind == 70) { + } else if (la.kind == 37 || la.kind == 52 || la.kind == 71) { CallCmd(out cmd); yields.Add((CallCmd)cmd); - } else SynErr(149); + } else SynErr(150); Expect(10); } Expect(26); @@ -1638,7 +1647,7 @@ void Guard(out Expr e) { } else if (StartOf(19)) { Expression(out ee); e = ee; - } else SynErr(150); + } else SynErr(151); Expect(12); } @@ -1664,7 +1673,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(68); + Expect(69); x = t; /* use location of := */ while (la.kind == 26) { Attribute(ref kv); @@ -1676,7 +1685,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { } else if (StartOf(20)) { lhss = new List(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 19 || la.kind == 69) { + while (la.kind == 19 || la.kind == 70) { if (la.kind == 19) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); @@ -1690,7 +1699,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 == 69) { + while (la.kind == 19 || la.kind == 70) { if (la.kind == 19) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); @@ -1701,7 +1710,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { } lhss.Add(lhs); } - Expect(68); + Expect(69); x = t; /* use location of := */ while (la.kind == 26) { Attribute(ref kv); @@ -1716,7 +1725,7 @@ void LabelOrAssign(out Cmd c, out IToken label) { } Expect(10); c = new AssignCmd(x, lhss, rhss, kv); - } else SynErr(151); + } else SynErr(152); } void ParCallCmd(out Cmd d) { @@ -1725,11 +1734,11 @@ void ParCallCmd(out Cmd d) { Cmd c = null; List callCmds = new List(); - Expect(71); + Expect(72); x = t; CallParams(false, false, x, out c); callCmds.Add((CallCmd)c); - while (la.kind == 72) { + while (la.kind == 73) { Get(); CallParams(false, false, x, out c); callCmds.Add((CallCmd)c); @@ -1758,7 +1767,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(69); + Expect(70); x = t; Ident(out id); fieldAccess = new FieldAccess(id, id.val); @@ -1790,7 +1799,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 == 68) { + } else if (la.kind == 14 || la.kind == 69) { ids.Add(new IdentifierExpr(first, first.val)); if (la.kind == 14) { Get(); @@ -1802,7 +1811,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) { ids.Add(new IdentifierExpr(p, p.val)); } } - Expect(68); + Expect(69); Ident(out first); Expect(11); if (StartOf(19)) { @@ -1816,7 +1825,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(152); + } else SynErr(153); } void Expressions(out List/*!*/ es) { @@ -1834,7 +1843,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); if (StartOf(21)) { - if (la.kind == 75 || la.kind == 76) { + if (la.kind == 76 || la.kind == 77) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1846,7 +1855,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 == 78 || la.kind == 79) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1857,23 +1866,23 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { } void EquivOp() { - if (la.kind == 73) { + if (la.kind == 74) { Get(); - } else if (la.kind == 74) { + } else if (la.kind == 75) { Get(); - } else SynErr(153); + } else SynErr(154); } void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); if (StartOf(22)) { - if (la.kind == 79 || la.kind == 80) { + if (la.kind == 80 || la.kind == 81) { 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 == 80 || la.kind == 81) { AndOp(); x = t; RelationalExpression(out e1); @@ -1884,7 +1893,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 == 82 || la.kind == 83) { OrOp(); x = t; RelationalExpression(out e1); @@ -1895,19 +1904,19 @@ void LogicalExpression(out Expr/*!*/ e0) { } void ImpliesOp() { - if (la.kind == 75) { + if (la.kind == 76) { Get(); - } else if (la.kind == 76) { + } else if (la.kind == 77) { Get(); - } else SynErr(154); + } else SynErr(155); } void ExpliesOp() { - if (la.kind == 77) { + if (la.kind == 78) { Get(); - } else if (la.kind == 78) { + } else if (la.kind == 79) { Get(); - } else SynErr(155); + } else SynErr(156); } void RelationalExpression(out Expr/*!*/ e0) { @@ -1921,25 +1930,25 @@ void RelationalExpression(out Expr/*!*/ e0) { } void AndOp() { - if (la.kind == 79) { + if (la.kind == 80) { Get(); - } else if (la.kind == 80) { + } else if (la.kind == 81) { Get(); - } else SynErr(156); + } else SynErr(157); } void OrOp() { - if (la.kind == 81) { + if (la.kind == 82) { Get(); - } else if (la.kind == 82) { + } else if (la.kind == 83) { Get(); - } else SynErr(157); + } else SynErr(158); } 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 == 91) { Get(); x = t; Term(out e1); @@ -1950,7 +1959,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 84: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; @@ -1965,44 +1974,44 @@ void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { x = t; op=BinaryOperator.Opcode.Gt; break; } - case 84: { + case 85: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 85: { + case 86: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 86: { + case 87: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 87: { + case 88: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 88: { + case 89: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 89: { + case 90: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(158); break; + default: SynErr(159); 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 == 92 || la.kind == 93) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -2021,19 +2030,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 == 92) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 92) { + } else if (la.kind == 93) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(159); + } else SynErr(160); } 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 == 97) { Get(); x = t; Power(out e1); @@ -2046,22 +2055,22 @@ void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { if (la.kind == 59) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 93) { + } else if (la.kind == 94) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 94) { + } else if (la.kind == 95) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else if (la.kind == 95) { + } else if (la.kind == 96) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(160); + } else SynErr(161); } 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 == 98) { Get(); x = t; Ident(out id); @@ -2075,27 +2084,27 @@ void UnaryExpression(out Expr/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; - if (la.kind == 92) { + if (la.kind == 93) { 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 == 99 || la.kind == 100) { NegOp(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(25)) { CoercionExpression(out e); - } else SynErr(161); + } else SynErr(162); } void NegOp() { - if (la.kind == 98) { + if (la.kind == 99) { Get(); - } else if (la.kind == 99) { + } else if (la.kind == 100) { Get(); - } else SynErr(162); + } else SynErr(163); } void CoercionExpression(out Expr/*!*/ e) { @@ -2119,7 +2128,7 @@ void CoercionExpression(out Expr/*!*/ e) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(163); + } else SynErr(164); } } @@ -2131,7 +2140,7 @@ void ArrayExpression(out Expr/*!*/ e) { List/*!*/ allArgs = dummyExprSeq; AtomExpression(out e); - while (la.kind == 19 || la.kind == 69) { + while (la.kind == 19 || la.kind == 70) { if (la.kind == 19) { Get(); x = t; allArgs = new List (); @@ -2153,7 +2162,7 @@ void ArrayExpression(out Expr/*!*/ e) { allArgs.Add(e1); } - if (la.kind == 68) { + if (la.kind == 69) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -2186,12 +2195,12 @@ void ArrayExpression(out Expr/*!*/ e) { } else if (la.kind == 11) { Get(); Ident(out id); - Expect(68); + Expect(69); x = t; Expression(out e1); Expect(12); e = new NAryExpr(x, new FieldUpdate(id, id.val), new List { e, e1 }); - } else SynErr(164); + } else SynErr(165); } } } @@ -2218,18 +2227,18 @@ void AtomExpression(out Expr/*!*/ e) { List/*!*/ blocks; switch (la.kind) { - case 100: { + case 101: { Get(); e = new LiteralExpr(t, false); break; } - case 101: { + case 102: { Get(); e = new LiteralExpr(t, true); break; } - case 102: case 103: { - if (la.kind == 102) { + case 103: case 104: { + if (la.kind == 103) { Get(); } else { Get(); @@ -2237,8 +2246,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RNE); break; } - case 104: case 105: { - if (la.kind == 104) { + case 105: case 106: { + if (la.kind == 105) { Get(); } else { Get(); @@ -2246,8 +2255,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RNA); break; } - case 106: case 107: { - if (la.kind == 106) { + case 107: case 108: { + if (la.kind == 107) { Get(); } else { Get(); @@ -2255,8 +2264,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RTP); break; } - case 108: case 109: { - if (la.kind == 108) { + case 109: case 110: { + if (la.kind == 109) { Get(); } else { Get(); @@ -2264,8 +2273,8 @@ void AtomExpression(out Expr/*!*/ e) { e = new LiteralExpr(t, RoundingMode.RTN); break; } - case 110: case 111: { - if (la.kind == 110) { + case 111: case 112: { + if (la.kind == 111) { Get(); } else { Get(); @@ -2308,12 +2317,12 @@ void AtomExpression(out Expr/*!*/ e) { e = new NAryExpr(x, new FunctionCall(id), es); } else if (la.kind == 12) { e = new NAryExpr(x, new FunctionCall(id), new List()); - } else SynErr(165); + } else SynErr(166); Expect(12); } break; } - case 112: { + case 113: { Get(); x = t; Expect(11); @@ -2346,19 +2355,19 @@ void AtomExpression(out Expr/*!*/ e) { 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 == 117 || la.kind == 118) { 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 == 119 || la.kind == 120) { 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 == 121 || la.kind == 122) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -2368,7 +2377,7 @@ void AtomExpression(out Expr/*!*/ e) { e = new LambdaExpr(x, typeParams, ds, kv, e); } else if (la.kind == 9) { LetExpr(out e); - } else SynErr(166); + } else SynErr(167); Expect(12); break; } @@ -2376,12 +2385,12 @@ void AtomExpression(out Expr/*!*/ e) { IfThenElseExpression(out e); break; } - case 113: { + case 114: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(167); break; + default: SynErr(168); break; } } @@ -2393,7 +2402,7 @@ void Dec(out BigDec n) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(168); + } else SynErr(169); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -2433,11 +2442,11 @@ void BvLit(out BigNum n, out int m) { } void Forall() { - if (la.kind == 116) { + if (la.kind == 117) { Get(); - } else if (la.kind == 117) { + } else if (la.kind == 118) { Get(); - } else SynErr(169); + } else SynErr(170); } void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out List/*!*/ ds, @@ -2455,7 +2464,7 @@ void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out L } } else if (StartOf(12)) { BoundVars(out ds); - } else SynErr(170); + } else SynErr(171); QSep(); while (la.kind == 26) { AttributeOrTrigger(ref kv, ref trig); @@ -2464,19 +2473,19 @@ void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out L } void Exists() { - if (la.kind == 118) { + if (la.kind == 119) { Get(); - } else if (la.kind == 119) { + } else if (la.kind == 120) { Get(); - } else SynErr(171); + } else SynErr(172); } void Lambda() { - if (la.kind == 120) { + if (la.kind == 121) { Get(); - } else if (la.kind == 121) { + } else if (la.kind == 122) { Get(); - } else SynErr(172); + } else SynErr(173); } void LetExpr(out Expr/*!*/ letexpr) { @@ -2497,7 +2506,7 @@ void LetExpr(out Expr/*!*/ letexpr) { LetVar(out v); ds.Add(v); } - Expect(68); + Expect(69); Expression(out e0); rhss.Add(e0); while (la.kind == 14) { @@ -2521,7 +2530,7 @@ void IfThenElseExpression(out Expr/*!*/ e) { Expect(56); tok = t; Expression(out e0); - Expect(115); + Expect(116); Expression(out e1); Expect(57); Expression(out e2); @@ -2532,7 +2541,7 @@ void CodeExpression(out List/*!*/ locals, out List/*!*/ bl 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(114); while (la.kind == 9) { LocalVars(locals); } @@ -2542,7 +2551,7 @@ void CodeExpression(out List/*!*/ locals, out List/*!*/ bl SpecBlock(out b); blocks.Add(b); } - Expect(114); + Expect(115); } void SpecBlock(out Block/*!*/ b) { @@ -2579,7 +2588,7 @@ void SpecBlock(out Block/*!*/ b) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(173); + } else SynErr(174); Expect(10); } @@ -2636,7 +2645,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(174); + } else SynErr(175); Expect(27); } @@ -2651,15 +2660,15 @@ void AttributeParameter(out object/*!*/ o) { } else if (StartOf(19)) { Expression(out e); o = e; - } else SynErr(175); + } else SynErr(176); } void QSep() { - if (la.kind == 122) { + if (la.kind == 123) { Get(); - } else if (la.kind == 123) { + } else if (la.kind == 124) { Get(); - } else SynErr(176); + } else SynErr(177); } void LetVar(out Variable/*!*/ v) { @@ -2688,33 +2697,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,_x,_T,_T, _T,_x,_T,_x, _T,_T,_T,_x, _x,_x,_T,_T, _T,_T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_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,_T,_T, _T,_T,_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,_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, _T,_x,_x,_x, _x,_x,_x,_x, _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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_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,_x,_x, _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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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, _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,_x, _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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x}, - {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_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, _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,_T, _T,_x,_x,_x, _x,_x,_x,_T, _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,_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,_T,_T, _T,_T,_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,_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,_T,_T, _T,_T,_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,_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,_T,_T, _T,_T,_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,_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,_T,_T, _T,_T,_x,_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,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_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,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_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,_x,_T,_T, _T,_T,_x,_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,_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,_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,_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,_x,_T,_T, _T,_T,_x,_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,_x,_T,_T, _T,_T,_x,_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} + {_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,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _T,_x,_T,_x, _T,_T,_T,_x, _x,_x,_T,_T, _T,_T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_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,_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,_T,_T, _T,_T,_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,_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, _T,_x,_x,_x, _x,_x,_x,_x, _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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, + {_x,_x,_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,_x,_x, _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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x}, + {_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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, _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,_T,_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, _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, _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,_T,_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, _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,_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,_T,_T, _T,_T,_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,_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}, + {_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,_T,_T, _T,_T,_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,_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,_T,_T, _T,_T,_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,_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,_T,_T, _T,_T,_x,_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,_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,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _T,_x,_T,_x, _T,_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,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _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,_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,_T,_T, _T,_T,_x,_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,_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,_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,_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,_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,_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,_x,_x,_x, _x,_x,_x,_x, _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,_T,_T, _T,_T,_x,_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, _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,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_T,_T,_T, _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,_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 @@ -2805,117 +2814,118 @@ string GetSyntaxErrorString(int n) { case 63: s = "\"pop\" expected"; break; case 64: s = "\"push\" expected"; break; case 65: s = "\"assert\" expected"; break; - case 66: s = "\"assume\" expected"; break; - case 67: s = "\"havoc\" expected"; break; - case 68: s = "\":=\" expected"; break; - case 69: s = "\"->\" expected"; break; - case 70: s = "\"call\" expected"; break; - case 71: s = "\"par\" 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 66: s = "\"check\" 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 = "\"par\" expected"; break; + case 73: s = "\"|\" expected"; break; + case 74: s = "\"<==>\" expected"; break; + case 75: s = "\"\\u21d4\" expected"; break; + case 76: s = "\"==>\" expected"; break; + case 77: s = "\"\\u21d2\" expected"; break; + case 78: s = "\"<==\" expected"; break; + case 79: s = "\"\\u21d0\" expected"; break; + case 80: s = "\"&&\" expected"; break; + case 81: s = "\"\\u2227\" expected"; break; + case 82: s = "\"||\" expected"; break; + case 83: s = "\"\\u2228\" expected"; break; + case 84: s = "\"==\" expected"; break; + case 85: s = "\"<=\" expected"; break; + case 86: s = "\">=\" expected"; break; + case 87: s = "\"!=\" expected"; break; + case 88: s = "\"\\u2260\" expected"; break; + case 89: s = "\"\\u2264\" expected"; break; + case 90: s = "\"\\u2265\" expected"; break; + case 91: s = "\"++\" expected"; break; + case 92: s = "\"+\" expected"; break; + case 93: s = "\"-\" expected"; break; + case 94: s = "\"div\" expected"; break; + case 95: s = "\"mod\" expected"; break; + case 96: s = "\"/\" expected"; break; + case 97: s = "\"**\" expected"; break; + case 98: s = "\"is\" expected"; break; + case 99: s = "\"!\" expected"; break; + case 100: s = "\"\\u00ac\" expected"; break; + case 101: s = "\"false\" expected"; break; + case 102: s = "\"true\" expected"; break; + case 103: s = "\"roundNearestTiesToEven\" expected"; break; + case 104: s = "\"RNE\" expected"; break; + case 105: s = "\"roundNearestTiesToAway\" expected"; break; + case 106: s = "\"RNA\" expected"; break; + case 107: s = "\"roundTowardPositive\" expected"; break; + case 108: s = "\"RTP\" expected"; break; + case 109: s = "\"roundTowardNegative\" expected"; break; + case 110: s = "\"RTN\" expected"; break; + case 111: s = "\"roundTowardZero\" expected"; break; + case 112: s = "\"RTZ\" expected"; break; + case 113: s = "\"old\" expected"; break; + case 114: s = "\"|{\" expected"; break; + case 115: s = "\"}|\" expected"; break; + case 116: s = "\"then\" expected"; break; + case 117: s = "\"forall\" expected"; break; + case 118: s = "\"\\u2200\" expected"; break; + case 119: s = "\"exists\" expected"; break; + case 120: s = "\"\\u2203\" expected"; break; + case 121: s = "\"lambda\" expected"; break; + case 122: s = "\"\\u03bb\" expected"; break; + case 123: s = "\"::\" expected"; break; + case 124: s = "\"\\u2022\" expected"; break; + case 125: s = "??? expected"; break; case 126: s = "invalid BoogiePL"; break; - case 127: s = "invalid Consts"; break; - case 128: s = "invalid Function"; break; + case 127: s = "invalid BoogiePL"; break; + case 128: s = "invalid Consts"; 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 SpecYieldRequires"; break; - case 140: s = "invalid SpecYieldPrePost"; 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 130: s = "invalid Function"; break; + case 131: s = "invalid YieldProcedureDecl"; break; + case 132: s = "invalid Procedure"; break; + case 133: s = "invalid ActionDecl"; break; + case 134: s = "invalid Type"; break; + case 135: s = "invalid TypeAtom"; break; + case 136: s = "invalid Ident"; break; + case 137: s = "invalid TypeArgs"; break; + case 138: s = "invalid MoverQualifier"; break; + case 139: s = "invalid SpecAction"; break; + case 140: s = "invalid SpecYieldRequires"; break; + case 141: s = "invalid SpecYieldPrePost"; break; + case 142: s = "invalid SpecYieldEnsures"; break; + case 143: s = "invalid Spec"; break; + case 144: s = "invalid SpecPrePost"; 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 146: s = "invalid LabelOrCmd"; break; + case 147: s = "invalid StructuredCmd"; break; + case 148: s = "invalid TransferCmd"; break; + case 149: s = "invalid IfCmd"; break; + case 150: s = "invalid WhileCmd"; break; + case 151: s = "invalid Guard"; break; + case 152: s = "invalid LabelOrAssign"; break; + case 153: s = "invalid CallParams"; break; + case 154: s = "invalid EquivOp"; break; + case 155: s = "invalid ImpliesOp"; break; + case 156: s = "invalid ExpliesOp"; break; + case 157: s = "invalid AndOp"; break; + case 158: s = "invalid OrOp"; break; + case 159: s = "invalid RelOp"; break; + case 160: s = "invalid AddOp"; break; + case 161: s = "invalid MulOp"; break; + case 162: s = "invalid UnaryExpression"; break; + case 163: s = "invalid NegOp"; break; + case 164: s = "invalid CoercionExpression"; break; + case 165: s = "invalid ArrayExpression"; break; case 166: s = "invalid AtomExpression"; break; case 167: s = "invalid AtomExpression"; 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; + case 168: s = "invalid AtomExpression"; break; + case 169: s = "invalid Dec"; break; + case 170: s = "invalid Forall"; break; + case 171: s = "invalid QuantifierBody"; break; + case 172: s = "invalid Exists"; break; + case 173: s = "invalid Lambda"; break; + case 174: s = "invalid SpecBlock"; break; + case 175: s = "invalid AttributeOrTrigger"; break; + case 176: s = "invalid AttributeParameter"; break; + case 177: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index 6bd51d22a..068c49517 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 = 125; + const int noSym = 125; [ContractInvariantMethod] @@ -558,30 +558,31 @@ void CheckLiteral() { case "pop": t.kind = 63; break; case "push": t.kind = 64; break; case "assert": t.kind = 65; break; - case "assume": t.kind = 66; break; - case "havoc": t.kind = 67; break; - case "call": t.kind = 70; break; - case "par": 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 "check": t.kind = 66; break; + case "assume": t.kind = 67; break; + case "havoc": t.kind = 68; break; + case "call": t.kind = 71; break; + case "par": t.kind = 72; break; + case "div": t.kind = 94; break; + case "mod": t.kind = 95; break; + case "is": t.kind = 98; break; + case "false": t.kind = 101; break; + case "true": t.kind = 102; break; + case "roundNearestTiesToEven": t.kind = 103; break; + case "RNE": t.kind = 104; break; + case "roundNearestTiesToAway": t.kind = 105; break; + case "RNA": t.kind = 106; break; + case "roundTowardPositive": t.kind = 107; break; + case "RTP": t.kind = 108; break; + case "roundTowardNegative": t.kind = 109; break; + case "RTN": t.kind = 110; break; + case "roundTowardZero": t.kind = 111; break; + case "RTZ": t.kind = 112; break; + case "old": t.kind = 113; break; + case "then": t.kind = 116; break; + case "forall": t.kind = 117; break; + case "exists": t.kind = 119; break; + case "lambda": t.kind = 121; break; default: break; } } @@ -865,67 +866,67 @@ void CheckLiteral() { case 67: {t.kind = 26; break;} case 68: - {t.kind = 68; break;} - case 69: {t.kind = 69; break;} + case 69: + {t.kind = 70; break;} case 70: - {t.kind = 73; break;} - case 71: {t.kind = 74; break;} - case 72: + case 71: {t.kind = 75; break;} - case 73: + case 72: {t.kind = 76; break;} + case 73: + {t.kind = 77; break;} case 74: - {t.kind = 78; break;} + {t.kind = 79; break;} case 75: if (ch == '&') {AddCh(); goto case 76;} else {goto case 0;} case 76: - {t.kind = 79; break;} - case 77: {t.kind = 80; break;} - case 78: + case 77: {t.kind = 81; break;} - case 79: + case 78: {t.kind = 82; break;} + case 79: + {t.kind = 83; break;} case 80: - {t.kind = 85; break;} - case 81: {t.kind = 86; break;} - case 82: + case 81: {t.kind = 87; break;} - case 83: + case 82: {t.kind = 88; break;} - case 84: + case 83: {t.kind = 89; break;} - case 85: + case 84: {t.kind = 90; break;} + case 85: + {t.kind = 91; break;} case 86: - {t.kind = 95; break;} - case 87: {t.kind = 96; break;} + case 87: + {t.kind = 97; break;} case 88: - {t.kind = 99; break;} + {t.kind = 100; break;} case 89: - {t.kind = 113; break;} - case 90: {t.kind = 114; break;} + case 90: + {t.kind = 115; break;} case 91: - {t.kind = 117; break;} + {t.kind = 118; break;} case 92: - {t.kind = 119; break;} + {t.kind = 120; break;} case 93: - {t.kind = 121; break;} - case 94: {t.kind = 122; break;} - case 95: + case 94: {t.kind = 123; break;} + case 95: + {t.kind = 124; break;} case 96: - recEnd = pos; recKind = 92; + recEnd = pos; recKind = 93; if (ch == '0') {AddCh(); goto case 16;} else if (ch == '>') {AddCh(); goto case 69;} - else {t.kind = 92; break;} + else {t.kind = 93; break;} case 97: recEnd = pos; recKind = 13; if (ch == '=') {AddCh(); goto case 68;} @@ -952,30 +953,30 @@ void CheckLiteral() { if (ch == '*') {AddCh(); goto case 87;} else {t.kind = 59; break;} case 103: - recEnd = pos; recKind = 72; + recEnd = pos; recKind = 73; if (ch == '|') {AddCh(); goto case 78;} else if (ch == '{') {AddCh(); goto case 89;} - else {t.kind = 72; break;} + else {t.kind = 73; break;} case 104: - recEnd = pos; recKind = 98; + recEnd = pos; recKind = 99; if (ch == '=') {AddCh(); goto case 81;} - else {t.kind = 98; break;} + else {t.kind = 99; break;} case 105: - recEnd = pos; recKind = 91; + recEnd = pos; recKind = 92; if (ch == '+') {AddCh(); goto case 85;} - else {t.kind = 91; break;} + else {t.kind = 92; break;} case 106: - recEnd = pos; recKind = 84; + recEnd = pos; recKind = 85; if (ch == '=') {AddCh(); goto case 108;} - else {t.kind = 84; break;} + else {t.kind = 85; break;} case 107: - recEnd = pos; recKind = 83; + recEnd = pos; recKind = 84; if (ch == '>') {AddCh(); goto case 72;} - else {t.kind = 83; break;} + else {t.kind = 84; break;} case 108: - recEnd = pos; recKind = 77; + recEnd = pos; recKind = 78; if (ch == '>') {AddCh(); goto case 70;} - else {t.kind = 77; break;} + else {t.kind = 78; break;} } t.val = new String(tval, 0, tlen); diff --git a/Source/VCGeneration/CommandTransformations.cs b/Source/VCGeneration/CommandTransformations.cs index 114fa805a..bef142df2 100644 --- a/Source/VCGeneration/CommandTransformations.cs +++ b/Source/VCGeneration/CommandTransformations.cs @@ -1,3 +1,5 @@ +using System.Collections.Generic; +using System.Linq; using Microsoft.Boogie; using VC; @@ -5,13 +7,14 @@ namespace VCGeneration; public static class CommandTransformations { - public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c) + public static IEnumerable AssertIntoAssumes(VCGenOptions options, Cmd cmd) { - if (c is AssertCmd assertCmd) - { - return VerificationConditionGenerator.AssertTurnedIntoAssume(options, assertCmd); + if (cmd is AssertCmd assertCmd) { + return assertCmd.Remember + ? new[] { VerificationConditionGenerator.AssertTurnedIntoAssume(options, assertCmd) } + : Enumerable.Empty(); } - return c; + return new[] {cmd}; } } \ No newline at end of file diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs index ebaeedf60..c1f7a734e 100644 --- a/Source/VCGeneration/FocusAttribute.cs +++ b/Source/VCGeneration/FocusAttribute.cs @@ -59,7 +59,7 @@ void FocusRec(IToken focusToken, int focusIndex, IReadOnlyList blocksToIn // Their assertions turn into assumes and any splits inside them are disabled. if(freeAssumeBlocks.Contains(block)) { - newBlock.Cmds = block.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(DisableSplits).ToList(); + newBlock.Cmds = block.Cmds.SelectMany(c => CommandTransformations.AssertIntoAssumes(options, c)).Select(DisableSplits).ToList(); } if (block.TransferCmd is GotoCmd gtc) { diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs index 41bd02472..cdb0e1f66 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -112,7 +112,12 @@ private static List DoPreAssignedManualSplit(VCGenOptions options, List DoPreAssignedManualSplit(VCGenOptions options, List(); foreach (Cmd command in currentBlock.Cmds) { verify = !ShouldSplitHere(command, splitOnEveryAssert) && verify; - newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command)); + if (verify) { + newCmds.Add(command); + } else { + newCmds.AddRange(CommandTransformations.AssertIntoAssumes(options, command)); + } } newBlock.Cmds = newCmds; } else { - newBlock.Cmds = currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(options, x)).ToList(); + newBlock.Cmds = currentBlock.Cmds.SelectMany(cmd => CommandTransformations.AssertIntoAssumes(options, cmd)).ToList(); } } // Patch the edges between the new blocks diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index bdff1b0f2..13cb94928 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -82,10 +82,6 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a return assume; } - #region Soundness smoke tester - - #endregion - public class CodeExprConversionClosure { private readonly TextWriter traceWriter; diff --git a/Test/test0/Split/Foo.split.1.bpl.expect b/Test/test0/Split/Foo.split.1.bpl.expect index bc4ea17f5..46c752201 100644 --- a/Test/test0/Split/Foo.split.1.bpl.expect +++ b/Test/test0/Split/Foo.split.1.bpl.expect @@ -23,7 +23,7 @@ implementation Foo() returns (y: int) anon6_Then: assume {:partition} x#AT#1 < 3; - assert 2 < 2; + check 2 < 2; assume y#AT#1 * y#AT#1 > 4; goto ; } diff --git a/Test/test0/Split/Foo.split.2.bpl.expect b/Test/test0/Split/Foo.split.2.bpl.expect index b07405c80..39301f352 100644 --- a/Test/test0/Split/Foo.split.2.bpl.expect +++ b/Test/test0/Split/Foo.split.2.bpl.expect @@ -23,7 +23,7 @@ implementation Foo() returns (y: int) anon6_Else: assume {:partition} 3 <= x#AT#1; - assert {:split_here} y#AT#1 * y#AT#1 * y#AT#1 < 8; + check {:split_here} y#AT#1 * y#AT#1 * y#AT#1 < 8; assert 2 < 2; goto ; } diff --git a/Test/test0/Split/Foo.split.3.bpl.expect b/Test/test0/Split/Foo.split.3.bpl.expect index 9ef24510f..b71832fb4 100644 --- a/Test/test0/Split/Foo.split.3.bpl.expect +++ b/Test/test0/Split/Foo.split.3.bpl.expect @@ -23,7 +23,6 @@ implementation Foo() returns (y: int) anon6_Else: assume {:partition} 3 <= x#AT#1; - assume y#AT#1 * y#AT#1 * y#AT#1 < 8; assume 2 < 2; goto anon4; @@ -36,7 +35,6 @@ implementation Foo() returns (y: int) anon6_Then: assume {:partition} x#AT#1 < 3; - assume 2 < 2; assume y#AT#1 * y#AT#1 > 4; goto anon4; } diff --git a/Test/test0/Split/Split.bpl b/Test/test0/Split/Split.bpl index e99d76351..82493b214 100644 --- a/Test/test0/Split/Split.bpl +++ b/Test/test0/Split/Split.bpl @@ -19,11 +19,11 @@ procedure Foo() returns (y: int) assert {:split_here} (x+y) * (x+y) > 25; y := y + 1; if (x < 3) { - assert 2 < 2; + check 2 < 2; assert {:split_here} y*y > 4; } else { - assert {:split_here} y*y*y < 8; + check {:split_here} y*y*y < 8; assert 2 < 2; } assert {:split_here} (x+y) * (x+y) == 25; From 49f48cf2e22a570f194e1cfa99a71180d88d98f4 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 26 Aug 2024 15:07:30 +0200 Subject: [PATCH 2/9] Add blank line --- Source/VCGeneration/ManualSplitFinder.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs index 8967a3b25..12b3a705f 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -120,6 +120,7 @@ private static List SplitOnAssert(VCGenOptions options, List oldBl AddBlockJumps(oldBlocks, oldToNewBlockMap); return newBlocks; } + private static List? DoPreAssignedManualSplit(VCGenOptions options, List blocks, Dictionary blockAssignments, int splitNumberWithinBlock, Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) { From f9cf8072b2bac78027f052cadb9a56fbd7b8e1d6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 16 Sep 2024 14:15:51 +0200 Subject: [PATCH 3/9] Move structured commands into separate files --- Source/Core/AST/AbsyCmd.cs | 761 ------------------ Source/Core/AST/BigBlocksResolutionContext.cs | 591 ++++++++++++++ .../Core/AST/StructuredCommands/ByProofCmd.cs | 16 + Source/Core/AST/StructuredCommands/IfCmd.cs | 108 +++ .../Core/AST/StructuredCommands/WhileCmd.cs | 74 ++ 5 files changed, 789 insertions(+), 761 deletions(-) create mode 100644 Source/Core/AST/BigBlocksResolutionContext.cs create mode 100644 Source/Core/AST/StructuredCommands/ByProofCmd.cs create mode 100644 Source/Core/AST/StructuredCommands/IfCmd.cs create mode 100644 Source/Core/AST/StructuredCommands/WhileCmd.cs diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index b64271504..24ace542c 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -351,592 +351,6 @@ public void AddLocalVariable(string name) } } - class BigBlocksResolutionContext - { - StmtList /*!*/ - stmtList; - - [Peer] List blocks; - - string /*!*/ - prefix = "anon"; - - int anon = 0; - - int FreshAnon() - { - return anon++; - } - - HashSet allLabels = new HashSet(); - - Errors /*!*/ - errorHandler; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(stmtList != null); - Contract.Invariant(cce.NonNullElements(blocks, true)); - Contract.Invariant(prefix != null); - Contract.Invariant(cce.NonNullElements(allLabels, true)); - Contract.Invariant(errorHandler != null); - } - - private void ComputeAllLabels(StmtList stmts) - { - if (stmts == null) - { - return; - } - - foreach (BigBlock bb in stmts.BigBlocks) - { - if (bb.LabelName != null) - { - allLabels.Add(bb.LabelName); - } - - ComputeAllLabels(bb.ec); - } - } - - private void ComputeAllLabels(StructuredCmd cmd) - { - if (cmd == null) - { - return; - } - - if (cmd is IfCmd) - { - IfCmd ifCmd = (IfCmd) cmd; - ComputeAllLabels(ifCmd.thn); - ComputeAllLabels(ifCmd.elseIf); - ComputeAllLabels(ifCmd.elseBlock); - } - else if (cmd is WhileCmd) - { - WhileCmd whileCmd = (WhileCmd) cmd; - ComputeAllLabels(whileCmd.Body); - } - } - - public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) - { - Contract.Requires(errorHandler != null); - Contract.Requires(stmtList != null); - this.stmtList = stmtList; - // Inject an empty big block at the end of the body of a while loop if its current end is another while loop. - // This transformation creates a suitable jump target for break statements inside the nested while loop. - InjectEmptyBigBlockInsideWhileLoopBody(stmtList); - this.errorHandler = errorHandler; - ComputeAllLabels(stmtList); - } - - public List /*!*/ Blocks - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - if (blocks == null) - { - blocks = new List(); - - int startErrorCount = this.errorHandler.count; - // Check that all goto statements go to a label in allLabels, and no break statement to a non-enclosing loop. - // Also, determine a good value for "prefix". - CheckLegalLabels(stmtList, null, null); - - // fill in names of anonymous blocks - NameAnonymousBlocks(stmtList); - - // determine successor blocks - RecordSuccessors(stmtList, null); - - if (this.errorHandler.count == startErrorCount) - { - // generate blocks from the big blocks - CreateBlocks(stmtList, null); - } - } - - return blocks; - } - } - - void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) - { - foreach (var bb in stmtList.BigBlocks) - { - InjectEmptyBigBlockInsideWhileLoopBody(bb.ec); - } - } - - void InjectEmptyBigBlockInsideWhileLoopBody(StructuredCmd structuredCmd) - { - if (structuredCmd is WhileCmd whileCmd) - { - InjectEmptyBigBlockInsideWhileLoopBody(whileCmd.Body); - if (whileCmd.Body.BigBlocks.Count > 0 && whileCmd.Body.BigBlocks.Last().ec is WhileCmd) - { - var newBigBlocks = new List(whileCmd.Body.BigBlocks); - newBigBlocks.Add(new BigBlock(Token.NoToken, null, new List(), null, null)); - whileCmd.Body = new StmtList(newBigBlocks, whileCmd.Body.EndCurly); - } - } - else if (structuredCmd is IfCmd ifCmd) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.thn); - if (ifCmd.elseBlock != null) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseBlock); - } - - if (ifCmd.elseIf != null) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseIf); - } - } - } - - void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) - { - Contract.Requires(stmtList != null); - Contract.Requires((parentContext == null) == (parentBigBlock == null)); - Contract.Requires(stmtList.ParentContext == null); // it hasn't been set yet - //modifies stmtList.*; - Contract.Ensures(stmtList.ParentContext == parentContext); - stmtList.ParentContext = parentContext; - stmtList.ParentBigBlock = parentBigBlock; - - // record the labels declared in this StmtList - foreach (BigBlock b in stmtList.BigBlocks) - { - if (b.LabelName != null) - { - string n = b.LabelName; - if (n.StartsWith(prefix)) - { - if (prefix.Length < n.Length && n[prefix.Length] == '0') - { - prefix += "1"; - } - else - { - prefix += "0"; - } - } - - stmtList.AddLabel(b.LabelName); - } - } - - // check that labels in this and nested StmtList's are legal - foreach (BigBlock b in stmtList.BigBlocks) - { - // goto's must reference blocks in enclosing blocks - if (b.tc is GotoCmd) - { - GotoCmd g = (GotoCmd) b.tc; - foreach (string /*!*/ lbl in cce.NonNull(g.labelNames)) - { - Contract.Assert(lbl != null); - /* - bool found = false; - for (StmtList sl = stmtList; sl != null; sl = sl.ParentContext) { - if (sl.Labels.Contains(lbl)) { - found = true; - break; - } - } - if (!found) { - this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach"); - } - */ - if (!allLabels.Contains(lbl)) - { - this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined"); - } - } - } - - // break labels must refer to an enclosing while statement - else if (b.ec is BreakCmd) - { - BreakCmd bcmd = (BreakCmd) b.ec; - Contract.Assert(bcmd.BreakEnclosure == null); // it hasn't been initialized yet - bool found = false; - for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) - { - cce.LoopInvariant(sl != null); - BigBlock bb = sl.ParentBigBlock; - - if (bcmd.Label == null) - { - // a label-less break statement breaks out of the innermost enclosing while statement - if (bb.ec is WhileCmd) - { - bcmd.BreakEnclosure = bb; - found = true; - break; - } - } - else if (bcmd.Label == bb.LabelName) - { - // a break statement with a label can break out of both if statements and while statements - if (bb.simpleCmds.Count == 0) - { - // this is a good target: the label refers to the if/while statement - bcmd.BreakEnclosure = bb; - } - else - { - // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement - this.errorHandler.SemErr(bcmd.tok, - "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); - } - - found = true; // don't look any further, since we've found a matching label - break; - } - } - - if (!found) - { - if (bcmd.Label == null) - { - this.errorHandler.SemErr(bcmd.tok, "Error: break statement is not inside a loop"); - } - else - { - this.errorHandler.SemErr(bcmd.tok, - "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); - } - } - } - - // recurse - else if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - CheckLegalLabels(wcmd.Body, stmtList, b); - } - else - { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - CheckLegalLabels(ifcmd.thn, stmtList, b); - if (ifcmd.elseBlock != null) - { - CheckLegalLabels(ifcmd.elseBlock, stmtList, b); - } - } - } - } - } - - void NameAnonymousBlocks(StmtList stmtList) - { - Contract.Requires(stmtList != null); - foreach (BigBlock b in stmtList.BigBlocks) - { - if (b.LabelName == null) - { - b.LabelName = prefix + FreshAnon(); - } - - if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - NameAnonymousBlocks(wcmd.Body); - } - else - { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - NameAnonymousBlocks(ifcmd.thn); - if (ifcmd.elseBlock != null) - { - NameAnonymousBlocks(ifcmd.elseBlock); - } - } - } - } - } - - void RecordSuccessors(StmtList stmtList, BigBlock successor) - { - Contract.Requires(stmtList != null); - for (int i = stmtList.BigBlocks.Count; 0 <= --i;) - { - BigBlock big = stmtList.BigBlocks[i]; - big.successorBigBlock = successor; - - if (big.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) big.ec; - RecordSuccessors(wcmd.Body, big); - } - else - { - for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - RecordSuccessors(ifcmd.thn, successor); - if (ifcmd.elseBlock != null) - { - RecordSuccessors(ifcmd.elseBlock, successor); - } - } - } - - successor = big; - } - } - - // If the enclosing context is a loop, then "runOffTheEndLabel" is the loop head label; - // otherwise, it is null. - void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) - { - Contract.Requires(stmtList != null); - Contract.Requires(blocks != null); - List cmdPrefixToApply = stmtList.PrefixCommands; - - int n = stmtList.BigBlocks.Count; - foreach (BigBlock b in stmtList.BigBlocks) - { - n--; - Contract.Assert(b.LabelName != null); - List theSimpleCmds; - if (cmdPrefixToApply == null) - { - theSimpleCmds = b.simpleCmds; - } - else - { - theSimpleCmds = new List(); - theSimpleCmds.AddRange(cmdPrefixToApply); - theSimpleCmds.AddRange(b.simpleCmds); - cmdPrefixToApply = null; // now, we've used 'em up - } - - if (b.tc != null) - { - // this BigBlock has the very same components as a Block - Contract.Assert(b.ec == null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, b.tc); - blocks.Add(block); - } - else if (b.ec == null) - { - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(stmtList.EndCurly, b); - } - - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, trCmd); - blocks.Add(block); - } - else if (b.ec is BreakCmd) - { - BreakCmd bcmd = (BreakCmd) b.ec; - Contract.Assert(bcmd.BreakEnclosure != null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, GotoSuccessor(b.ec.tok, bcmd.BreakEnclosure)); - blocks.Add(block); - } - else if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - var a = FreshAnon(); - string loopHeadLabel = prefix + a + "_LoopHead"; - string /*!*/ - loopBodyLabel = prefix + a + "_LoopBody"; - string loopDoneLabel = prefix + a + "_LoopDone"; - - List ssBody = new List(); - List ssDone = new List(); - if (wcmd.Guard != null) - { - var ac = new AssumeCmd(wcmd.tok, wcmd.Guard); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); - ssBody.Add(ac); - - ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard)); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); - ssDone.Add(ac); - } - - // Try to squeeze in ssBody into the first block of wcmd.Body - bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); - - // ... goto LoopHead; - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, - new GotoCmd(wcmd.tok, new List {loopHeadLabel})); - blocks.Add(block); - - // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; - List ssHead = new List(); - foreach (CallCmd yield in wcmd.Yields) - { - ssHead.Add(yield); - } - foreach (PredicateCmd inv in wcmd.Invariants) - { - ssHead.Add(inv); - } - - block = new Block(wcmd.tok, loopHeadLabel, ssHead, - new GotoCmd(wcmd.tok, new List {loopDoneLabel, loopBodyLabel})); - blocks.Add(block); - - if (!bodyGuardTakenCareOf) - { - // LoopBody: assume guard; goto firstLoopBlock; - block = new Block(wcmd.tok, loopBodyLabel, ssBody, - new GotoCmd(wcmd.tok, new List {wcmd.Body.BigBlocks[0].LabelName})); - blocks.Add(block); - } - - // recurse to create the blocks for the loop body - CreateBlocks(wcmd.Body, loopHeadLabel); - - // LoopDone: assume !guard; goto loopSuccessor; - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(wcmd.tok, b); - } - - block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); - blocks.Add(block); - } - else - { - IfCmd ifcmd = (IfCmd) b.ec; - string predLabel = b.LabelName; - List predCmds = theSimpleCmds; - - for (; ifcmd != null; ifcmd = ifcmd.elseIf) - { - var a = FreshAnon(); - string thenLabel = prefix + a + "_Then"; - Contract.Assert(thenLabel != null); - string elseLabel = prefix + a + "_Else"; - Contract.Assert(elseLabel != null); - - List ssThen = new List(); - List ssElse = new List(); - if (ifcmd.Guard != null) - { - var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - ssThen.Add(ac); - - ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - ssElse.Add(ac); - } - - // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock - bool thenGuardTakenCareOf = ifcmd.thn.PrefixFirstBlock(ssThen, ref thenLabel); - bool elseGuardTakenCareOf = false; - if (ifcmd.elseBlock != null) - { - elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel); - } - - // ... goto Then, Else; - var jumpBlock = new Block(b.tok, predLabel, predCmds, - new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); - blocks.Add(jumpBlock); - - if (!thenGuardTakenCareOf) - { - // Then: assume guard; goto firstThenBlock; - var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen, - new GotoCmd(ifcmd.tok, new List {ifcmd.thn.BigBlocks[0].LabelName})); - blocks.Add(thenJumpBlock); - } - - // recurse to create the blocks for the then branch - CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null); - - if (ifcmd.elseBlock != null) - { - Contract.Assert(ifcmd.elseIf == null); - if (!elseGuardTakenCareOf) - { - // Else: assume !guard; goto firstElseBlock; - var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse, - new GotoCmd(ifcmd.tok, new List {ifcmd.elseBlock.BigBlocks[0].LabelName})); - blocks.Add(elseJumpBlock); - } - - // recurse to create the blocks for the else branch - CreateBlocks(ifcmd.elseBlock, n == 0 ? runOffTheEndLabel : null); - } - else if (ifcmd.elseIf != null) - { - // this is an "else if" - predLabel = elseLabel; - predCmds = new List(); - if (ifcmd.Guard != null) - { - var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - predCmds.Add(ac); - } - } - else - { - // no else alternative is specified, so else branch is just "skip" - // Else: assume !guard; goto ifSuccessor; - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(ifcmd.tok, b); - } - - var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); - blocks.Add(block); - } - } - } - } - } - - TransferCmd GotoSuccessor(IToken tok, BigBlock b) - { - Contract.Requires(b != null); - Contract.Requires(tok != null); - Contract.Ensures(Contract.Result() != null); - if (b.successorBigBlock != null) - { - return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); - } - else - { - return new ReturnCmd(tok); - } - } - } - [ContractClass(typeof(StructuredCmdContracts))] public abstract class StructuredCmd { @@ -986,181 +400,6 @@ public StructuredCmdContracts() : base(null) } } - public class IfCmd : StructuredCmd - { - public Expr Guard; - - private StmtList /*!*/ - _thn; - - public StmtList /*!*/ thn - { - get - { - Contract.Ensures(Contract.Result() != null); - return this._thn; - } - set - { - Contract.Requires(value != null); - this._thn = value; - } - } - - private IfCmd _elseIf; - - public IfCmd elseIf - { - get { return this._elseIf; } - set - { - Contract.Requires(value == null || this.elseBlock == null); - this._elseIf = value; - } - } - - private StmtList _elseBlock; - - public StmtList elseBlock - { - get { return this._elseBlock; } - set - { - Contract.Requires(value == null || this.elseIf == null); - this._elseBlock = value; - } - } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(this._thn != null); - Contract.Invariant(this._elseIf == null || this._elseBlock == null); - } - - public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, StmtList elseBlock) - : base(tok) - { - Contract.Requires(tok != null); - Contract.Requires(thn != null); - Contract.Requires(elseIf == null || elseBlock == null); - this.Guard = guard; - this._thn = thn; - this._elseIf = elseIf; - this._elseBlock = elseBlock; - } - - public override void Emit(TokenTextWriter stream, int level) - { - stream.Write(level, "if ("); - IfCmd /*!*/ - ifcmd = this; - while (true) - { - if (ifcmd.Guard == null) - { - stream.Write("*"); - } - else - { - ifcmd.Guard.Emit(stream); - } - - stream.WriteLine(")"); - - stream.WriteLine(level, "{"); - ifcmd.thn.Emit(stream, level + 1); - stream.WriteLine(level, "}"); - - if (ifcmd.elseIf != null) - { - stream.Write(level, "else if ("); - ifcmd = ifcmd.elseIf; - continue; - } - else if (ifcmd.elseBlock != null) - { - stream.WriteLine(level, "else"); - stream.WriteLine(level, "{"); - ifcmd.elseBlock.Emit(stream, level + 1); - stream.WriteLine(level, "}"); - } - - break; - } - } - } - - public class WhileCmd : StructuredCmd - { - [Peer] public Expr Guard; - - public List Invariants; - - public List Yields; - - public StmtList Body; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(Body != null); - Contract.Invariant(cce.NonNullElements(Invariants)); - } - - public WhileCmd(IToken tok, [Captured] Expr guard, List invariants, List yields, StmtList body) - : base(tok) - { - Contract.Requires(cce.NonNullElements(invariants)); - Contract.Requires(body != null); - Contract.Requires(tok != null); - this.Guard = guard; - this.Invariants = invariants; - this.Yields = yields; - this.Body = body; - } - - public override void Emit(TokenTextWriter stream, int level) - { - stream.Write(level, "while ("); - if (Guard == null) - { - stream.Write("*"); - } - else - { - Guard.Emit(stream); - } - - stream.WriteLine(")"); - - foreach (var yield in Yields) - { - stream.Write(level + 1, "invariant"); - yield.Emit(stream, level + 1); - } - foreach (var inv in Invariants) - { - if (inv is AssumeCmd) - { - stream.Write(level + 1, "free invariant "); - } - else - { - stream.Write(level + 1, "invariant "); - } - - Cmd.EmitAttributes(stream, inv.Attributes); - inv.Expr.Emit(stream); - stream.WriteLine(";"); - } - - stream.WriteLine(level, "{"); - Body.Emit(stream, level + 1); - stream.WriteLine(level, "}"); - } - } - public class BreakCmd : StructuredCmd { public string Label; diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs new file mode 100644 index 000000000..9d7a20fd5 --- /dev/null +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -0,0 +1,591 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie; + +class BigBlocksResolutionContext +{ + StmtList /*!*/ stmtList; + + [Peer] List blocks; + + string /*!*/ + prefix = "anon"; + + int anon = 0; + + int FreshAnon() + { + return anon++; + } + + HashSet allLabels = new HashSet(); + + Errors /*!*/ + errorHandler; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(stmtList != null); + Contract.Invariant(cce.NonNullElements(blocks, true)); + Contract.Invariant(prefix != null); + Contract.Invariant(cce.NonNullElements(allLabels, true)); + Contract.Invariant(errorHandler != null); + } + + private void ComputeAllLabels(StmtList stmts) + { + if (stmts == null) + { + return; + } + + foreach (BigBlock bb in stmts.BigBlocks) + { + if (bb.LabelName != null) + { + allLabels.Add(bb.LabelName); + } + + ComputeAllLabels(bb.ec); + } + } + + private void ComputeAllLabels(StructuredCmd cmd) + { + if (cmd == null) + { + return; + } + + if (cmd is IfCmd) + { + IfCmd ifCmd = (IfCmd) cmd; + ComputeAllLabels(ifCmd.thn); + ComputeAllLabels(ifCmd.elseIf); + ComputeAllLabels(ifCmd.elseBlock); + } + else if (cmd is WhileCmd) + { + WhileCmd whileCmd = (WhileCmd) cmd; + ComputeAllLabels(whileCmd.Body); + } + } + + public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) + { + Contract.Requires(errorHandler != null); + Contract.Requires(stmtList != null); + this.stmtList = stmtList; + // Inject an empty big block at the end of the body of a while loop if its current end is another while loop. + // This transformation creates a suitable jump target for break statements inside the nested while loop. + InjectEmptyBigBlockInsideWhileLoopBody(stmtList); + this.errorHandler = errorHandler; + ComputeAllLabels(stmtList); + } + + public List /*!*/ Blocks + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + if (blocks == null) + { + blocks = new List(); + + int startErrorCount = this.errorHandler.count; + // Check that all goto statements go to a label in allLabels, and no break statement to a non-enclosing loop. + // Also, determine a good value for "prefix". + CheckLegalLabels(stmtList, null, null); + + // fill in names of anonymous blocks + NameAnonymousBlocks(stmtList); + + // determine successor blocks + RecordSuccessors(stmtList, null); + + if (this.errorHandler.count == startErrorCount) + { + // generate blocks from the big blocks + CreateBlocks(stmtList, null); + } + } + + return blocks; + } + } + + void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) + { + foreach (var bb in stmtList.BigBlocks) + { + InjectEmptyBigBlockInsideWhileLoopBody(bb.ec); + } + } + + void InjectEmptyBigBlockInsideWhileLoopBody(StructuredCmd structuredCmd) + { + if (structuredCmd is WhileCmd whileCmd) + { + InjectEmptyBigBlockInsideWhileLoopBody(whileCmd.Body); + if (whileCmd.Body.BigBlocks.Count > 0 && whileCmd.Body.BigBlocks.Last().ec is WhileCmd) + { + var newBigBlocks = new List(whileCmd.Body.BigBlocks); + newBigBlocks.Add(new BigBlock(Token.NoToken, null, new List(), null, null)); + whileCmd.Body = new StmtList(newBigBlocks, whileCmd.Body.EndCurly); + } + } + else if (structuredCmd is IfCmd ifCmd) + { + InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.thn); + if (ifCmd.elseBlock != null) + { + InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseBlock); + } + + if (ifCmd.elseIf != null) + { + InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseIf); + } + } + } + + void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) + { + Contract.Requires(stmtList != null); + Contract.Requires((parentContext == null) == (parentBigBlock == null)); + Contract.Requires(stmtList.ParentContext == null); // it hasn't been set yet + //modifies stmtList.*; + Contract.Ensures(stmtList.ParentContext == parentContext); + stmtList.ParentContext = parentContext; + stmtList.ParentBigBlock = parentBigBlock; + + // record the labels declared in this StmtList + foreach (BigBlock b in stmtList.BigBlocks) + { + if (b.LabelName != null) + { + string n = b.LabelName; + if (n.StartsWith(prefix)) + { + if (prefix.Length < n.Length && n[prefix.Length] == '0') + { + prefix += "1"; + } + else + { + prefix += "0"; + } + } + + stmtList.AddLabel(b.LabelName); + } + } + + // check that labels in this and nested StmtList's are legal + foreach (BigBlock b in stmtList.BigBlocks) + { + // goto's must reference blocks in enclosing blocks + if (b.tc is GotoCmd) + { + GotoCmd g = (GotoCmd) b.tc; + foreach (string /*!*/ lbl in cce.NonNull(g.labelNames)) + { + Contract.Assert(lbl != null); + /* + bool found = false; + for (StmtList sl = stmtList; sl != null; sl = sl.ParentContext) { + if (sl.Labels.Contains(lbl)) { + found = true; + break; + } + } + if (!found) { + this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach"); + } + */ + if (!allLabels.Contains(lbl)) + { + this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined"); + } + } + } + + // break labels must refer to an enclosing while statement + else if (b.ec is BreakCmd) + { + BreakCmd bcmd = (BreakCmd) b.ec; + Contract.Assert(bcmd.BreakEnclosure == null); // it hasn't been initialized yet + bool found = false; + for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) + { + cce.LoopInvariant(sl != null); + BigBlock bb = sl.ParentBigBlock; + + if (bcmd.Label == null) + { + // a label-less break statement breaks out of the innermost enclosing while statement + if (bb.ec is WhileCmd) + { + bcmd.BreakEnclosure = bb; + found = true; + break; + } + } + else if (bcmd.Label == bb.LabelName) + { + // a break statement with a label can break out of both if statements and while statements + if (bb.simpleCmds.Count == 0) + { + // this is a good target: the label refers to the if/while statement + bcmd.BreakEnclosure = bb; + } + else + { + // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement + this.errorHandler.SemErr(bcmd.tok, + "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); + } + + found = true; // don't look any further, since we've found a matching label + break; + } + } + + if (!found) + { + if (bcmd.Label == null) + { + this.errorHandler.SemErr(bcmd.tok, "Error: break statement is not inside a loop"); + } + else + { + this.errorHandler.SemErr(bcmd.tok, + "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); + } + } + } + + // recurse + else if (b.ec is WhileCmd) + { + WhileCmd wcmd = (WhileCmd) b.ec; + CheckLegalLabels(wcmd.Body, stmtList, b); + } + else + { + for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) + { + CheckLegalLabels(ifcmd.thn, stmtList, b); + if (ifcmd.elseBlock != null) + { + CheckLegalLabels(ifcmd.elseBlock, stmtList, b); + } + } + } + } + } + + void NameAnonymousBlocks(StmtList stmtList) + { + Contract.Requires(stmtList != null); + foreach (BigBlock b in stmtList.BigBlocks) + { + if (b.LabelName == null) + { + b.LabelName = prefix + FreshAnon(); + } + + if (b.ec is WhileCmd) + { + WhileCmd wcmd = (WhileCmd) b.ec; + NameAnonymousBlocks(wcmd.Body); + } + else + { + for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) + { + NameAnonymousBlocks(ifcmd.thn); + if (ifcmd.elseBlock != null) + { + NameAnonymousBlocks(ifcmd.elseBlock); + } + } + } + } + } + + void RecordSuccessors(StmtList stmtList, BigBlock successor) + { + Contract.Requires(stmtList != null); + for (int i = stmtList.BigBlocks.Count; 0 <= --i;) + { + BigBlock big = stmtList.BigBlocks[i]; + big.successorBigBlock = successor; + + if (big.ec is WhileCmd) + { + WhileCmd wcmd = (WhileCmd) big.ec; + RecordSuccessors(wcmd.Body, big); + } + else + { + for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) + { + RecordSuccessors(ifcmd.thn, successor); + if (ifcmd.elseBlock != null) + { + RecordSuccessors(ifcmd.elseBlock, successor); + } + } + } + + successor = big; + } + } + + // If the enclosing context is a loop, then "runOffTheEndLabel" is the loop head label; + // otherwise, it is null. + void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) + { + Contract.Requires(stmtList != null); + Contract.Requires(blocks != null); + List cmdPrefixToApply = stmtList.PrefixCommands; + + int n = stmtList.BigBlocks.Count; + foreach (BigBlock b in stmtList.BigBlocks) + { + n--; + Contract.Assert(b.LabelName != null); + List theSimpleCmds; + if (cmdPrefixToApply == null) + { + theSimpleCmds = b.simpleCmds; + } + else + { + theSimpleCmds = new List(); + theSimpleCmds.AddRange(cmdPrefixToApply); + theSimpleCmds.AddRange(b.simpleCmds); + cmdPrefixToApply = null; // now, we've used 'em up + } + + if (b.tc != null) + { + // this BigBlock has the very same components as a Block + Contract.Assert(b.ec == null); + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, b.tc); + blocks.Add(block); + } + else if (b.ec == null) + { + TransferCmd trCmd; + if (n == 0 && runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); + } + else + { + trCmd = GotoSuccessor(stmtList.EndCurly, b); + } + + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, trCmd); + blocks.Add(block); + } + else if (b.ec is BreakCmd) + { + BreakCmd bcmd = (BreakCmd) b.ec; + Contract.Assert(bcmd.BreakEnclosure != null); + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, GotoSuccessor(b.ec.tok, bcmd.BreakEnclosure)); + blocks.Add(block); + } + else if (b.ec is WhileCmd) + { + WhileCmd wcmd = (WhileCmd) b.ec; + var a = FreshAnon(); + string loopHeadLabel = prefix + a + "_LoopHead"; + string /*!*/ + loopBodyLabel = prefix + a + "_LoopBody"; + string loopDoneLabel = prefix + a + "_LoopDone"; + + List ssBody = new List(); + List ssDone = new List(); + if (wcmd.Guard != null) + { + var ac = new AssumeCmd(wcmd.tok, wcmd.Guard); + ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); + ssBody.Add(ac); + + ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard)); + ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); + ssDone.Add(ac); + } + + // Try to squeeze in ssBody into the first block of wcmd.Body + bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); + + // ... goto LoopHead; + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, + new GotoCmd(wcmd.tok, new List {loopHeadLabel})); + blocks.Add(block); + + // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; + List ssHead = new List(); + foreach (CallCmd yield in wcmd.Yields) + { + ssHead.Add(yield); + } + foreach (PredicateCmd inv in wcmd.Invariants) + { + ssHead.Add(inv); + } + + block = new Block(wcmd.tok, loopHeadLabel, ssHead, + new GotoCmd(wcmd.tok, new List {loopDoneLabel, loopBodyLabel})); + blocks.Add(block); + + if (!bodyGuardTakenCareOf) + { + // LoopBody: assume guard; goto firstLoopBlock; + block = new Block(wcmd.tok, loopBodyLabel, ssBody, + new GotoCmd(wcmd.tok, new List {wcmd.Body.BigBlocks[0].LabelName})); + blocks.Add(block); + } + + // recurse to create the blocks for the loop body + CreateBlocks(wcmd.Body, loopHeadLabel); + + // LoopDone: assume !guard; goto loopSuccessor; + TransferCmd trCmd; + if (n == 0 && runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); + } + else + { + trCmd = GotoSuccessor(wcmd.tok, b); + } + + block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); + blocks.Add(block); + } + else + { + IfCmd ifcmd = (IfCmd) b.ec; + string predLabel = b.LabelName; + List predCmds = theSimpleCmds; + + for (; ifcmd != null; ifcmd = ifcmd.elseIf) + { + var a = FreshAnon(); + string thenLabel = prefix + a + "_Then"; + Contract.Assert(thenLabel != null); + string elseLabel = prefix + a + "_Else"; + Contract.Assert(elseLabel != null); + + List ssThen = new List(); + List ssElse = new List(); + if (ifcmd.Guard != null) + { + var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); + ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + ssThen.Add(ac); + + ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); + ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + ssElse.Add(ac); + } + + // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock + bool thenGuardTakenCareOf = ifcmd.thn.PrefixFirstBlock(ssThen, ref thenLabel); + bool elseGuardTakenCareOf = false; + if (ifcmd.elseBlock != null) + { + elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel); + } + + // ... goto Then, Else; + var jumpBlock = new Block(b.tok, predLabel, predCmds, + new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); + blocks.Add(jumpBlock); + + if (!thenGuardTakenCareOf) + { + // Then: assume guard; goto firstThenBlock; + var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen, + new GotoCmd(ifcmd.tok, new List {ifcmd.thn.BigBlocks[0].LabelName})); + blocks.Add(thenJumpBlock); + } + + // recurse to create the blocks for the then branch + CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null); + + if (ifcmd.elseBlock != null) + { + Contract.Assert(ifcmd.elseIf == null); + if (!elseGuardTakenCareOf) + { + // Else: assume !guard; goto firstElseBlock; + var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse, + new GotoCmd(ifcmd.tok, new List {ifcmd.elseBlock.BigBlocks[0].LabelName})); + blocks.Add(elseJumpBlock); + } + + // recurse to create the blocks for the else branch + CreateBlocks(ifcmd.elseBlock, n == 0 ? runOffTheEndLabel : null); + } + else if (ifcmd.elseIf != null) + { + // this is an "else if" + predLabel = elseLabel; + predCmds = new List(); + if (ifcmd.Guard != null) + { + var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); + ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + predCmds.Add(ac); + } + } + else + { + // no else alternative is specified, so else branch is just "skip" + // Else: assume !guard; goto ifSuccessor; + TransferCmd trCmd; + if (n == 0 && runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); + } + else + { + trCmd = GotoSuccessor(ifcmd.tok, b); + } + + var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); + blocks.Add(block); + } + } + } + } + } + + TransferCmd GotoSuccessor(IToken tok, BigBlock b) + { + Contract.Requires(b != null); + Contract.Requires(tok != null); + Contract.Ensures(Contract.Result() != null); + if (b.successorBigBlock != null) + { + return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); + } + else + { + return new ReturnCmd(tok); + } + } +} \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/ByProofCmd.cs b/Source/Core/AST/StructuredCommands/ByProofCmd.cs new file mode 100644 index 000000000..d899b8c71 --- /dev/null +++ b/Source/Core/AST/StructuredCommands/ByProofCmd.cs @@ -0,0 +1,16 @@ +namespace Microsoft.Boogie; + +public class ByProofCmd : StructuredCmd +{ + public StmtList Body; + public StmtList Proof; + + public ByProofCmd(IToken tok) : base(tok) + { + } + + public override void Emit(TokenTextWriter stream, int level) + { + throw new System.NotImplementedException(); + } +} \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/IfCmd.cs b/Source/Core/AST/StructuredCommands/IfCmd.cs new file mode 100644 index 000000000..5f29f407d --- /dev/null +++ b/Source/Core/AST/StructuredCommands/IfCmd.cs @@ -0,0 +1,108 @@ +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie; + +public class IfCmd : StructuredCmd +{ + public Expr Guard; + + private StmtList /*!*/ + _thn; + + public StmtList /*!*/ thn + { + get + { + Contract.Ensures(Contract.Result() != null); + return this._thn; + } + set + { + Contract.Requires(value != null); + this._thn = value; + } + } + + private IfCmd _elseIf; + + public IfCmd elseIf + { + get { return this._elseIf; } + set + { + Contract.Requires(value == null || this.elseBlock == null); + this._elseIf = value; + } + } + + private StmtList _elseBlock; + + public StmtList elseBlock + { + get { return this._elseBlock; } + set + { + Contract.Requires(value == null || this.elseIf == null); + this._elseBlock = value; + } + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(this._thn != null); + Contract.Invariant(this._elseIf == null || this._elseBlock == null); + } + + public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, StmtList elseBlock) + : base(tok) + { + Contract.Requires(tok != null); + Contract.Requires(thn != null); + Contract.Requires(elseIf == null || elseBlock == null); + this.Guard = guard; + this._thn = thn; + this._elseIf = elseIf; + this._elseBlock = elseBlock; + } + + public override void Emit(TokenTextWriter stream, int level) + { + stream.Write(level, "if ("); + IfCmd /*!*/ + ifcmd = this; + while (true) + { + if (ifcmd.Guard == null) + { + stream.Write("*"); + } + else + { + ifcmd.Guard.Emit(stream); + } + + stream.WriteLine(")"); + + stream.WriteLine(level, "{"); + ifcmd.thn.Emit(stream, level + 1); + stream.WriteLine(level, "}"); + + if (ifcmd.elseIf != null) + { + stream.Write(level, "else if ("); + ifcmd = ifcmd.elseIf; + continue; + } + else if (ifcmd.elseBlock != null) + { + stream.WriteLine(level, "else"); + stream.WriteLine(level, "{"); + ifcmd.elseBlock.Emit(stream, level + 1); + stream.WriteLine(level, "}"); + } + + break; + } + } +} \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/WhileCmd.cs b/Source/Core/AST/StructuredCommands/WhileCmd.cs new file mode 100644 index 000000000..135bd43ae --- /dev/null +++ b/Source/Core/AST/StructuredCommands/WhileCmd.cs @@ -0,0 +1,74 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie; + +public class WhileCmd : StructuredCmd +{ + [Peer] public Expr Guard; + + public List Invariants; + + public List Yields; + + public StmtList Body; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(Body != null); + Contract.Invariant(cce.NonNullElements(Invariants)); + } + + public WhileCmd(IToken tok, [Captured] Expr guard, List invariants, List yields, StmtList body) + : base(tok) + { + Contract.Requires(cce.NonNullElements(invariants)); + Contract.Requires(body != null); + Contract.Requires(tok != null); + this.Guard = guard; + this.Invariants = invariants; + this.Yields = yields; + this.Body = body; + } + + public override void Emit(TokenTextWriter stream, int level) + { + stream.Write(level, "while ("); + if (Guard == null) + { + stream.Write("*"); + } + else + { + Guard.Emit(stream); + } + + stream.WriteLine(")"); + + foreach (var yield in Yields) + { + stream.Write(level + 1, "invariant"); + yield.Emit(stream, level + 1); + } + foreach (var inv in Invariants) + { + if (inv is AssumeCmd) + { + stream.Write(level + 1, "free invariant "); + } + else + { + stream.Write(level + 1, "invariant "); + } + + Cmd.EmitAttributes(stream, inv.Attributes); + inv.Expr.Emit(stream); + stream.WriteLine(";"); + } + + stream.WriteLine(level, "{"); + Body.Emit(stream, level + 1); + stream.WriteLine(level, "}"); + } +} \ No newline at end of file From 30ba83891fdc2ad65539bebaaaff27d88374931c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 16 Sep 2024 14:40:31 +0200 Subject: [PATCH 4/9] Move some code into structured command sublcasses --- Source/Core/AST/AbsyCmd.cs | 60 ---- Source/Core/AST/BigBlocksResolutionContext.cs | 332 ++---------------- .../Core/AST/StructuredCommands/BreakCmd.cs | 98 ++++++ .../Core/AST/StructuredCommands/ByProofCmd.cs | 23 ++ Source/Core/AST/StructuredCommands/IfCmd.cs | 134 +++++++ .../AST/StructuredCommands/StructuredCmd.cs | 46 +++ .../Core/AST/StructuredCommands/WhileCmd.cs | 98 ++++++ 7 files changed, 427 insertions(+), 364 deletions(-) create mode 100644 Source/Core/AST/StructuredCommands/BreakCmd.cs create mode 100644 Source/Core/AST/StructuredCommands/StructuredCmd.cs diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 24ace542c..408619a1f 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -351,41 +351,6 @@ public void AddLocalVariable(string name) } } - [ContractClass(typeof(StructuredCmdContracts))] - public abstract class StructuredCmd - { - private IToken /*!*/ - _tok; - - public IToken /*!*/ tok - { - get - { - Contract.Ensures(Contract.Result() != null); - return this._tok; - } - set - { - Contract.Requires(value != null); - this._tok = value; - } - } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(this._tok != null); - } - - public StructuredCmd(IToken tok) - { - Contract.Requires(tok != null); - this._tok = tok; - } - - public abstract void Emit(TokenTextWriter /*!*/ stream, int level); - } - [ContractClassFor(typeof(StructuredCmd))] public abstract class StructuredCmdContracts : StructuredCmd { @@ -400,31 +365,6 @@ public StructuredCmdContracts() : base(null) } } - public class BreakCmd : StructuredCmd - { - public string Label; - public BigBlock BreakEnclosure; - - public BreakCmd(IToken tok, string label) - : base(tok) - { - Contract.Requires(tok != null); - this.Label = label; - } - - public override void Emit(TokenTextWriter stream, int level) - { - if (Label == null) - { - stream.WriteLine(level, "break;"); - } - else - { - stream.WriteLine(level, "break {0};", Label); - } - } - } - //--------------------------------------------------------------------- // Block diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs index 9d7a20fd5..3753558f2 100644 --- a/Source/Core/AST/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -1,30 +1,27 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; -using System.Linq; namespace Microsoft.Boogie; -class BigBlocksResolutionContext +public class BigBlocksResolutionContext { StmtList /*!*/ stmtList; [Peer] List blocks; - string /*!*/ - prefix = "anon"; + string /*!*/ prefix = "anon"; int anon = 0; - int FreshAnon() + public string FreshPrefix() { - return anon++; + return prefix + anon++; } - HashSet allLabels = new HashSet(); + HashSet allLabels = new(); - Errors /*!*/ - errorHandler; + public Errors ErrorHandler { get; } [ContractInvariantMethod] void ObjectInvariant() @@ -33,10 +30,10 @@ void ObjectInvariant() Contract.Invariant(cce.NonNullElements(blocks, true)); Contract.Invariant(prefix != null); Contract.Invariant(cce.NonNullElements(allLabels, true)); - Contract.Invariant(errorHandler != null); + Contract.Invariant(ErrorHandler != null); } - private void ComputeAllLabels(StmtList stmts) + public void ComputeAllLabels(StmtList stmts) { if (stmts == null) { @@ -50,7 +47,7 @@ private void ComputeAllLabels(StmtList stmts) allLabels.Add(bb.LabelName); } - ComputeAllLabels(bb.ec); + bb.ec?.ComputeAllLabels(this); } } @@ -60,19 +57,8 @@ private void ComputeAllLabels(StructuredCmd cmd) { return; } - - if (cmd is IfCmd) - { - IfCmd ifCmd = (IfCmd) cmd; - ComputeAllLabels(ifCmd.thn); - ComputeAllLabels(ifCmd.elseIf); - ComputeAllLabels(ifCmd.elseBlock); - } - else if (cmd is WhileCmd) - { - WhileCmd whileCmd = (WhileCmd) cmd; - ComputeAllLabels(whileCmd.Body); - } + + cmd.ComputeAllLabels(this); } public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) @@ -83,10 +69,15 @@ public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) // Inject an empty big block at the end of the body of a while loop if its current end is another while loop. // This transformation creates a suitable jump target for break statements inside the nested while loop. InjectEmptyBigBlockInsideWhileLoopBody(stmtList); - this.errorHandler = errorHandler; + this.ErrorHandler = errorHandler; ComputeAllLabels(stmtList); } + public void AddBlock(Block block) + { + blocks.Add(block); + } + public List /*!*/ Blocks { get @@ -96,7 +87,7 @@ public List /*!*/ Blocks { blocks = new List(); - int startErrorCount = this.errorHandler.count; + int startErrorCount = this.ErrorHandler.count; // Check that all goto statements go to a label in allLabels, and no break statement to a non-enclosing loop. // Also, determine a good value for "prefix". CheckLegalLabels(stmtList, null, null); @@ -107,7 +98,7 @@ public List /*!*/ Blocks // determine successor blocks RecordSuccessors(stmtList, null); - if (this.errorHandler.count == startErrorCount) + if (this.ErrorHandler.count == startErrorCount) { // generate blocks from the big blocks CreateBlocks(stmtList, null); @@ -118,42 +109,15 @@ public List /*!*/ Blocks } } - void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) + public void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) { foreach (var bb in stmtList.BigBlocks) { - InjectEmptyBigBlockInsideWhileLoopBody(bb.ec); - } - } - - void InjectEmptyBigBlockInsideWhileLoopBody(StructuredCmd structuredCmd) - { - if (structuredCmd is WhileCmd whileCmd) - { - InjectEmptyBigBlockInsideWhileLoopBody(whileCmd.Body); - if (whileCmd.Body.BigBlocks.Count > 0 && whileCmd.Body.BigBlocks.Last().ec is WhileCmd) - { - var newBigBlocks = new List(whileCmd.Body.BigBlocks); - newBigBlocks.Add(new BigBlock(Token.NoToken, null, new List(), null, null)); - whileCmd.Body = new StmtList(newBigBlocks, whileCmd.Body.EndCurly); - } - } - else if (structuredCmd is IfCmd ifCmd) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.thn); - if (ifCmd.elseBlock != null) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseBlock); - } - - if (ifCmd.elseIf != null) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseIf); - } + bb.ec.InjectEmptyBigBlockInsideWhileLoopBody(this); } } - void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) + public void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) { Contract.Requires(stmtList != null); Contract.Requires((parentContext == null) == (parentBigBlock == null)); @@ -209,82 +173,13 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent */ if (!allLabels.Contains(lbl)) { - this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined"); + this.ErrorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined"); } } } - - // break labels must refer to an enclosing while statement - else if (b.ec is BreakCmd) - { - BreakCmd bcmd = (BreakCmd) b.ec; - Contract.Assert(bcmd.BreakEnclosure == null); // it hasn't been initialized yet - bool found = false; - for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) - { - cce.LoopInvariant(sl != null); - BigBlock bb = sl.ParentBigBlock; - - if (bcmd.Label == null) - { - // a label-less break statement breaks out of the innermost enclosing while statement - if (bb.ec is WhileCmd) - { - bcmd.BreakEnclosure = bb; - found = true; - break; - } - } - else if (bcmd.Label == bb.LabelName) - { - // a break statement with a label can break out of both if statements and while statements - if (bb.simpleCmds.Count == 0) - { - // this is a good target: the label refers to the if/while statement - bcmd.BreakEnclosure = bb; - } - else - { - // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement - this.errorHandler.SemErr(bcmd.tok, - "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); - } - - found = true; // don't look any further, since we've found a matching label - break; - } - } - - if (!found) - { - if (bcmd.Label == null) - { - this.errorHandler.SemErr(bcmd.tok, "Error: break statement is not inside a loop"); - } - else - { - this.errorHandler.SemErr(bcmd.tok, - "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); - } - } - } - - // recurse - else if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - CheckLegalLabels(wcmd.Body, stmtList, b); - } else { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - CheckLegalLabels(ifcmd.thn, stmtList, b); - if (ifcmd.elseBlock != null) - { - CheckLegalLabels(ifcmd.elseBlock, stmtList, b); - } - } + b.ec.CheckLegalLabels(this, this.stmtList, b); } } } @@ -296,7 +191,7 @@ void NameAnonymousBlocks(StmtList stmtList) { if (b.LabelName == null) { - b.LabelName = prefix + FreshAnon(); + b.LabelName = FreshPrefix(); } if (b.ec is WhileCmd) @@ -349,7 +244,7 @@ void RecordSuccessors(StmtList stmtList, BigBlock successor) // If the enclosing context is a loop, then "runOffTheEndLabel" is the loop head label; // otherwise, it is null. - void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) + public void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) { Contract.Requires(stmtList != null); Contract.Requires(blocks != null); @@ -396,185 +291,14 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) Block block = new Block(b.tok, b.LabelName, theSimpleCmds, trCmd); blocks.Add(block); } - else if (b.ec is BreakCmd) - { - BreakCmd bcmd = (BreakCmd) b.ec; - Contract.Assert(bcmd.BreakEnclosure != null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, GotoSuccessor(b.ec.tok, bcmd.BreakEnclosure)); - blocks.Add(block); - } - else if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - var a = FreshAnon(); - string loopHeadLabel = prefix + a + "_LoopHead"; - string /*!*/ - loopBodyLabel = prefix + a + "_LoopBody"; - string loopDoneLabel = prefix + a + "_LoopDone"; - - List ssBody = new List(); - List ssDone = new List(); - if (wcmd.Guard != null) - { - var ac = new AssumeCmd(wcmd.tok, wcmd.Guard); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); - ssBody.Add(ac); - - ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard)); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); - ssDone.Add(ac); - } - - // Try to squeeze in ssBody into the first block of wcmd.Body - bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); - - // ... goto LoopHead; - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, - new GotoCmd(wcmd.tok, new List {loopHeadLabel})); - blocks.Add(block); - - // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; - List ssHead = new List(); - foreach (CallCmd yield in wcmd.Yields) - { - ssHead.Add(yield); - } - foreach (PredicateCmd inv in wcmd.Invariants) - { - ssHead.Add(inv); - } - - block = new Block(wcmd.tok, loopHeadLabel, ssHead, - new GotoCmd(wcmd.tok, new List {loopDoneLabel, loopBodyLabel})); - blocks.Add(block); - - if (!bodyGuardTakenCareOf) - { - // LoopBody: assume guard; goto firstLoopBlock; - block = new Block(wcmd.tok, loopBodyLabel, ssBody, - new GotoCmd(wcmd.tok, new List {wcmd.Body.BigBlocks[0].LabelName})); - blocks.Add(block); - } - - // recurse to create the blocks for the loop body - CreateBlocks(wcmd.Body, loopHeadLabel); - - // LoopDone: assume !guard; goto loopSuccessor; - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(wcmd.tok, b); - } - - block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); - blocks.Add(block); - } else { - IfCmd ifcmd = (IfCmd) b.ec; - string predLabel = b.LabelName; - List predCmds = theSimpleCmds; - - for (; ifcmd != null; ifcmd = ifcmd.elseIf) - { - var a = FreshAnon(); - string thenLabel = prefix + a + "_Then"; - Contract.Assert(thenLabel != null); - string elseLabel = prefix + a + "_Else"; - Contract.Assert(elseLabel != null); - - List ssThen = new List(); - List ssElse = new List(); - if (ifcmd.Guard != null) - { - var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - ssThen.Add(ac); - - ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - ssElse.Add(ac); - } - - // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock - bool thenGuardTakenCareOf = ifcmd.thn.PrefixFirstBlock(ssThen, ref thenLabel); - bool elseGuardTakenCareOf = false; - if (ifcmd.elseBlock != null) - { - elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel); - } - - // ... goto Then, Else; - var jumpBlock = new Block(b.tok, predLabel, predCmds, - new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); - blocks.Add(jumpBlock); - - if (!thenGuardTakenCareOf) - { - // Then: assume guard; goto firstThenBlock; - var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen, - new GotoCmd(ifcmd.tok, new List {ifcmd.thn.BigBlocks[0].LabelName})); - blocks.Add(thenJumpBlock); - } - - // recurse to create the blocks for the then branch - CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null); - - if (ifcmd.elseBlock != null) - { - Contract.Assert(ifcmd.elseIf == null); - if (!elseGuardTakenCareOf) - { - // Else: assume !guard; goto firstElseBlock; - var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse, - new GotoCmd(ifcmd.tok, new List {ifcmd.elseBlock.BigBlocks[0].LabelName})); - blocks.Add(elseJumpBlock); - } - - // recurse to create the blocks for the else branch - CreateBlocks(ifcmd.elseBlock, n == 0 ? runOffTheEndLabel : null); - } - else if (ifcmd.elseIf != null) - { - // this is an "else if" - predLabel = elseLabel; - predCmds = new List(); - if (ifcmd.Guard != null) - { - var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - predCmds.Add(ac); - } - } - else - { - // no else alternative is specified, so else branch is just "skip" - // Else: assume !guard; goto ifSuccessor; - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(ifcmd.tok, b); - } - - var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); - blocks.Add(block); - } - } + b.ec.CreateBlocks(this, b, theSimpleCmds, stmtList, n == 0 ? runOffTheEndLabel : null); } } } - TransferCmd GotoSuccessor(IToken tok, BigBlock b) + public static TransferCmd GotoSuccessor(IToken tok, BigBlock b) { Contract.Requires(b != null); Contract.Requires(tok != null); diff --git a/Source/Core/AST/StructuredCommands/BreakCmd.cs b/Source/Core/AST/StructuredCommands/BreakCmd.cs new file mode 100644 index 000000000..158f8f466 --- /dev/null +++ b/Source/Core/AST/StructuredCommands/BreakCmd.cs @@ -0,0 +1,98 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie; + +public class BreakCmd : StructuredCmd +{ + public string Label; + public BigBlock BreakEnclosure; + + public BreakCmd(IToken tok, string label) + : base(tok) + { + Contract.Requires(tok != null); + Label = label; + } + + public override void Emit(TokenTextWriter stream, int level) + { + if (Label == null) + { + stream.WriteLine(level, "break;"); + } + else + { + stream.WriteLine(level, "break {0};", Label); + } + } + + public override void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context) + { + } + + public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock) + { + Contract.Assert(BreakEnclosure == null); // it hasn't been initialized yet + bool found = false; + for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) + { + cce.LoopInvariant(sl != null); + BigBlock bb = sl.ParentBigBlock; + + if (Label == null) + { + // a label-less break statement breaks out of the innermost enclosing while statement + if (bb.ec is WhileCmd) + { + BreakEnclosure = bb; + found = true; + break; + } + } + else if (Label == bb.LabelName) + { + // a break statement with a label can break out of both if statements and while statements + if (bb.simpleCmds.Count == 0) + { + // this is a good target: the label refers to the if/while statement + BreakEnclosure = bb; + } + else + { + // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement + context.ErrorHandler.SemErr(tok, + "Error: break label '" + Label + "' must designate an enclosing statement"); + } + + found = true; // don't look any further, since we've found a matching label + break; + } + } + + if (!found) + { + if (Label == null) + { + context.ErrorHandler.SemErr(tok, "Error: break statement is not inside a loop"); + } + else + { + context.ErrorHandler.SemErr(tok, + "Error: break label '" + Label + "' must designate an enclosing statement"); + } + } + } + + public override void ComputeAllLabels(BigBlocksResolutionContext context) + { + } + + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, StmtList stmtList, + string runOffTheEndLabel) + { + Contract.Assert(this.BreakEnclosure != null); + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, BigBlocksResolutionContext.GotoSuccessor(b.ec.tok, BreakEnclosure)); + context.AddBlock(block); + } +} \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/ByProofCmd.cs b/Source/Core/AST/StructuredCommands/ByProofCmd.cs index d899b8c71..4fb49476c 100644 --- a/Source/Core/AST/StructuredCommands/ByProofCmd.cs +++ b/Source/Core/AST/StructuredCommands/ByProofCmd.cs @@ -1,3 +1,5 @@ +using System.Collections.Generic; + namespace Microsoft.Boogie; public class ByProofCmd : StructuredCmd @@ -13,4 +15,25 @@ public override void Emit(TokenTextWriter stream, int level) { throw new System.NotImplementedException(); } + + public override void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context) + { + throw new System.NotImplementedException(); + } + + public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock) + { + throw new System.NotImplementedException(); + } + + public override void ComputeAllLabels(BigBlocksResolutionContext context) + { + throw new System.NotImplementedException(); + } + + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, StmtList stmtList, + string runOffTheEndLabel) + { + throw new System.NotImplementedException(); + } } \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/IfCmd.cs b/Source/Core/AST/StructuredCommands/IfCmd.cs index 5f29f407d..bbac4e709 100644 --- a/Source/Core/AST/StructuredCommands/IfCmd.cs +++ b/Source/Core/AST/StructuredCommands/IfCmd.cs @@ -1,3 +1,5 @@ +using System; +using System.Collections.Generic; using System.Diagnostics.Contracts; namespace Microsoft.Boogie; @@ -105,4 +107,136 @@ public override void Emit(TokenTextWriter stream, int level) break; } } + + public override void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context) + { + context.InjectEmptyBigBlockInsideWhileLoopBody(thn); + if (elseBlock != null) + { + context.InjectEmptyBigBlockInsideWhileLoopBody(elseBlock); + } + + if (elseIf != null) + { + elseIf.InjectEmptyBigBlockInsideWhileLoopBody(context); + } + } + + public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock) + { + for (IfCmd ifcmd = this; ifcmd != null; ifcmd = ifcmd.elseIf) + { + context.CheckLegalLabels(ifcmd.thn, stmtList, bigBlock); + if (ifcmd.elseBlock != null) + { + context.CheckLegalLabels(ifcmd.elseBlock, stmtList, bigBlock); + } + } + } + + public override void ComputeAllLabels(BigBlocksResolutionContext context) + { + context.ComputeAllLabels(thn); + elseIf.ComputeAllLabels(context); + context.ComputeAllLabels(elseBlock); + } + + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, StmtList stmtList, + string runOffTheEndLabel) + { + IfCmd ifcmd = (IfCmd) b.ec; + string predLabel = b.LabelName; + List predCmds = theSimpleCmds; + + for (; ifcmd != null; ifcmd = ifcmd.elseIf) + { + var prefix = context.FreshPrefix(); + string thenLabel = prefix + "_Then"; + Contract.Assert(thenLabel != null); + string elseLabel = prefix + "_Else"; + Contract.Assert(elseLabel != null); + + List ssThen = new List(); + List ssElse = new List(); + if (ifcmd.Guard != null) + { + var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); + ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + ssThen.Add(ac); + + ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); + ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + ssElse.Add(ac); + } + + // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock + bool thenGuardTakenCareOf = ifcmd.thn.PrefixFirstBlock(ssThen, ref thenLabel); + bool elseGuardTakenCareOf = false; + if (ifcmd.elseBlock != null) + { + elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel); + } + + // ... goto Then, Else; + var jumpBlock = new Block(b.tok, predLabel, predCmds, + new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); + context.AddBlock(jumpBlock); + + if (!thenGuardTakenCareOf) + { + // Then: assume guard; goto firstThenBlock; + var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen, + new GotoCmd(ifcmd.tok, new List {ifcmd.thn.BigBlocks[0].LabelName})); + context.AddBlock(thenJumpBlock); + } + + // recurse to create the blocks for the then branch + context.CreateBlocks(ifcmd.thn, runOffTheEndLabel); + + if (ifcmd.elseBlock != null) + { + Contract.Assert(ifcmd.elseIf == null); + if (!elseGuardTakenCareOf) + { + // Else: assume !guard; goto firstElseBlock; + var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse, + new GotoCmd(ifcmd.tok, new List {ifcmd.elseBlock.BigBlocks[0].LabelName})); + context.AddBlock(elseJumpBlock); + } + + // recurse to create the blocks for the else branch + context.CreateBlocks(ifcmd.elseBlock, runOffTheEndLabel); + } + else if (ifcmd.elseIf != null) + { + // this is an "else if" + predLabel = elseLabel; + predCmds = new List(); + if (ifcmd.Guard != null) + { + var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); + ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + predCmds.Add(ac); + } + } + else + { + // no else alternative is specified, so else branch is just "skip" + // Else: assume !guard; goto ifSuccessor; + TransferCmd trCmd; + if (runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); + } + else + { + trCmd = BigBlocksResolutionContext.GotoSuccessor(ifcmd.tok, b); + } + + var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); + context.AddBlock(block); + } + } + } } \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/StructuredCmd.cs b/Source/Core/AST/StructuredCommands/StructuredCmd.cs new file mode 100644 index 000000000..cdf993ea0 --- /dev/null +++ b/Source/Core/AST/StructuredCommands/StructuredCmd.cs @@ -0,0 +1,46 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie; + +[ContractClass(typeof(StructuredCmdContracts))] +public abstract class StructuredCmd +{ + private IToken /*!*/ + _tok; + + public IToken /*!*/ tok + { + get + { + Contract.Ensures(Contract.Result() != null); + return this._tok; + } + set + { + Contract.Requires(value != null); + this._tok = value; + } + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(this._tok != null); + } + + public StructuredCmd(IToken tok) + { + Contract.Requires(tok != null); + this._tok = tok; + } + + public abstract void Emit(TokenTextWriter /*!*/ stream, int level); + + public abstract void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context); + public abstract void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock); + public abstract void ComputeAllLabels(BigBlocksResolutionContext context); + public abstract void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, + StmtList stmtList, + string runOffTheEndLabel); +} \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/WhileCmd.cs b/Source/Core/AST/StructuredCommands/WhileCmd.cs index 135bd43ae..99a99742e 100644 --- a/Source/Core/AST/StructuredCommands/WhileCmd.cs +++ b/Source/Core/AST/StructuredCommands/WhileCmd.cs @@ -1,5 +1,7 @@ +using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; namespace Microsoft.Boogie; @@ -71,4 +73,100 @@ public override void Emit(TokenTextWriter stream, int level) Body.Emit(stream, level + 1); stream.WriteLine(level, "}"); } + + public override void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context) + { + context.InjectEmptyBigBlockInsideWhileLoopBody(Body); + if (Body.BigBlocks.Count <= 0 || Body.BigBlocks.Last().ec is not WhileCmd) + { + return; + } + + var newBigBlocks = new List(Body.BigBlocks); + newBigBlocks.Add(new BigBlock(Token.NoToken, null, new List(), null, null)); + Body = new StmtList(newBigBlocks, Body.EndCurly); + } + + public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock) + { + context.CheckLegalLabels(Body, stmtList, bigBlock); + } + + public override void ComputeAllLabels(BigBlocksResolutionContext context) + { + context.ComputeAllLabels(Body); + } + + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, + StmtList stmtList, + string runOffTheEndLabel) + { + WhileCmd wcmd = (WhileCmd) this; + var prefix = context.FreshPrefix(); + string loopHeadLabel = prefix + "_LoopHead"; + string /*!*/ loopBodyLabel = prefix + "_LoopBody"; + string loopDoneLabel = prefix + "_LoopDone"; + + List ssBody = new List(); + List ssDone = new List(); + if (wcmd.Guard != null) + { + var ac = new AssumeCmd(wcmd.tok, wcmd.Guard); + ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); + ssBody.Add(ac); + + ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard)); + ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); + ssDone.Add(ac); + } + + // Try to squeeze in ssBody into the first block of wcmd.Body + bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); + + // ... goto LoopHead; + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, + new GotoCmd(wcmd.tok, new List {loopHeadLabel})); + context.AddBlock(block); + + // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; + List ssHead = new List(); + foreach (CallCmd yield in wcmd.Yields) + { + ssHead.Add(yield); + } + foreach (PredicateCmd inv in wcmd.Invariants) + { + ssHead.Add(inv); + } + + block = new Block(wcmd.tok, loopHeadLabel, ssHead, + new GotoCmd(wcmd.tok, new List {loopDoneLabel, loopBodyLabel})); + context.AddBlock(block); + + if (!bodyGuardTakenCareOf) + { + // LoopBody: assume guard; goto firstLoopBlock; + block = new Block(wcmd.tok, loopBodyLabel, ssBody, + new GotoCmd(wcmd.tok, new List {wcmd.Body.BigBlocks[0].LabelName})); + context.AddBlock(block); + } + + // recurse to create the blocks for the loop body + context.CreateBlocks(wcmd.Body, loopHeadLabel); + + // LoopDone: assume !guard; goto loopSuccessor; + TransferCmd trCmd; + if (runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); + } + else + { + trCmd = BigBlocksResolutionContext.GotoSuccessor(wcmd.tok, b); + } + + block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); + context.AddBlock(block); + } } \ No newline at end of file From f690907c9141edf8098f539d3bba3c9510a7c439 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 16 Sep 2024 15:05:28 +0200 Subject: [PATCH 5/9] Further refactoring --- Source/Core/AST/BigBlocksResolutionContext.cs | 60 +++++-------------- .../Core/AST/StructuredCommands/BreakCmd.cs | 14 +++-- .../Core/AST/StructuredCommands/ByProofCmd.cs | 7 ++- Source/Core/AST/StructuredCommands/IfCmd.cs | 43 +++++++++---- .../AST/StructuredCommands/StructuredCmd.cs | 8 ++- .../Core/AST/StructuredCommands/WhileCmd.cs | 18 +++--- 6 files changed, 72 insertions(+), 78 deletions(-) diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs index 3753558f2..7f3ee70eb 100644 --- a/Source/Core/AST/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -33,7 +33,7 @@ void ObjectInvariant() Contract.Invariant(ErrorHandler != null); } - public void ComputeAllLabels(StmtList stmts) + private void ComputeAllLabels(StmtList stmts) { if (stmts == null) { @@ -47,18 +47,16 @@ public void ComputeAllLabels(StmtList stmts) allLabels.Add(bb.LabelName); } - bb.ec?.ComputeAllLabels(this); - } - } - - private void ComputeAllLabels(StructuredCmd cmd) - { - if (cmd == null) - { - return; + if (bb.ec == null) + { + continue; + } + + foreach (var list in bb.ec.StatementLists) + { + ComputeAllLabels(list); + } } - - cmd.ComputeAllLabels(this); } public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) @@ -194,26 +192,14 @@ void NameAnonymousBlocks(StmtList stmtList) b.LabelName = FreshPrefix(); } - if (b.ec is WhileCmd) + foreach (var l in b.ec.StatementLists) { - WhileCmd wcmd = (WhileCmd) b.ec; - NameAnonymousBlocks(wcmd.Body); - } - else - { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - NameAnonymousBlocks(ifcmd.thn); - if (ifcmd.elseBlock != null) - { - NameAnonymousBlocks(ifcmd.elseBlock); - } - } + NameAnonymousBlocks(l); } } } - void RecordSuccessors(StmtList stmtList, BigBlock successor) + public void RecordSuccessors(StmtList stmtList, BigBlock successor) { Contract.Requires(stmtList != null); for (int i = stmtList.BigBlocks.Count; 0 <= --i;) @@ -221,23 +207,7 @@ void RecordSuccessors(StmtList stmtList, BigBlock successor) BigBlock big = stmtList.BigBlocks[i]; big.successorBigBlock = successor; - if (big.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) big.ec; - RecordSuccessors(wcmd.Body, big); - } - else - { - for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - RecordSuccessors(ifcmd.thn, successor); - if (ifcmd.elseBlock != null) - { - RecordSuccessors(ifcmd.elseBlock, successor); - } - } - } - + big.ec.RecordSuccessors(this, big); successor = big; } } @@ -293,7 +263,7 @@ public void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) } else { - b.ec.CreateBlocks(this, b, theSimpleCmds, stmtList, n == 0 ? runOffTheEndLabel : null); + b.ec.CreateBlocks(this, b, theSimpleCmds, n == 0 ? runOffTheEndLabel : null); } } } diff --git a/Source/Core/AST/StructuredCommands/BreakCmd.cs b/Source/Core/AST/StructuredCommands/BreakCmd.cs index 158f8f466..4d30a955d 100644 --- a/Source/Core/AST/StructuredCommands/BreakCmd.cs +++ b/Source/Core/AST/StructuredCommands/BreakCmd.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; namespace Microsoft.Boogie; @@ -84,15 +85,16 @@ public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtLi } } - public override void ComputeAllLabels(BigBlocksResolutionContext context) - { - } - - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, StmtList stmtList, + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, string runOffTheEndLabel) { Contract.Assert(this.BreakEnclosure != null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, BigBlocksResolutionContext.GotoSuccessor(b.ec.tok, BreakEnclosure)); + Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, BigBlocksResolutionContext.GotoSuccessor(bigBlock.ec.tok, BreakEnclosure)); context.AddBlock(block); } + + public override IEnumerable StatementLists => Enumerable.Empty(); + public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock) + { + } } \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/ByProofCmd.cs b/Source/Core/AST/StructuredCommands/ByProofCmd.cs index 4fb49476c..818c50700 100644 --- a/Source/Core/AST/StructuredCommands/ByProofCmd.cs +++ b/Source/Core/AST/StructuredCommands/ByProofCmd.cs @@ -26,13 +26,14 @@ public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtLi throw new System.NotImplementedException(); } - public override void ComputeAllLabels(BigBlocksResolutionContext context) + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, + string runOffTheEndLabel) { throw new System.NotImplementedException(); } - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, StmtList stmtList, - string runOffTheEndLabel) + public override IEnumerable StatementLists => new[] { Body, Proof }; + public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock) { throw new System.NotImplementedException(); } diff --git a/Source/Core/AST/StructuredCommands/IfCmd.cs b/Source/Core/AST/StructuredCommands/IfCmd.cs index bbac4e709..c4a9300c5 100644 --- a/Source/Core/AST/StructuredCommands/IfCmd.cs +++ b/Source/Core/AST/StructuredCommands/IfCmd.cs @@ -134,18 +134,11 @@ public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtLi } } - public override void ComputeAllLabels(BigBlocksResolutionContext context) - { - context.ComputeAllLabels(thn); - elseIf.ComputeAllLabels(context); - context.ComputeAllLabels(elseBlock); - } - - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, StmtList stmtList, + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, string runOffTheEndLabel) { - IfCmd ifcmd = (IfCmd) b.ec; - string predLabel = b.LabelName; + IfCmd ifcmd = (IfCmd) bigBlock.ec; + string predLabel = bigBlock.LabelName; List predCmds = theSimpleCmds; for (; ifcmd != null; ifcmd = ifcmd.elseIf) @@ -178,7 +171,7 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b } // ... goto Then, Else; - var jumpBlock = new Block(b.tok, predLabel, predCmds, + var jumpBlock = new Block(bigBlock.tok, predLabel, predCmds, new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); context.AddBlock(jumpBlock); @@ -231,7 +224,7 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b } else { - trCmd = BigBlocksResolutionContext.GotoSuccessor(ifcmd.tok, b); + trCmd = BigBlocksResolutionContext.GotoSuccessor(ifcmd.tok, bigBlock); } var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); @@ -239,4 +232,30 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b } } } + + public override IEnumerable StatementLists { + get + { + for (var ifcmd = this; ifcmd != null; ifcmd = ifcmd.elseIf) + { + yield return ifcmd.thn; + if (ifcmd.elseBlock != null) + { + yield return ifcmd.elseBlock; + } + } + } + } + + public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock) + { + for (var ifcmd = this; ifcmd != null; ifcmd = ifcmd.elseIf) + { + context.RecordSuccessors(ifcmd.thn, bigBlock.successorBigBlock); + if (ifcmd.elseBlock != null) + { + context.RecordSuccessors(ifcmd.elseBlock, bigBlock.successorBigBlock); + } + } + } } \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/StructuredCmd.cs b/Source/Core/AST/StructuredCommands/StructuredCmd.cs index cdf993ea0..ac386320f 100644 --- a/Source/Core/AST/StructuredCommands/StructuredCmd.cs +++ b/Source/Core/AST/StructuredCommands/StructuredCmd.cs @@ -39,8 +39,10 @@ public StructuredCmd(IToken tok) public abstract void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context); public abstract void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock); - public abstract void ComputeAllLabels(BigBlocksResolutionContext context); - public abstract void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, - StmtList stmtList, + + public abstract void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, string runOffTheEndLabel); + + public abstract IEnumerable StatementLists { get; } + public abstract void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock); } \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/WhileCmd.cs b/Source/Core/AST/StructuredCommands/WhileCmd.cs index 99a99742e..80aa07cd1 100644 --- a/Source/Core/AST/StructuredCommands/WhileCmd.cs +++ b/Source/Core/AST/StructuredCommands/WhileCmd.cs @@ -92,13 +92,7 @@ public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtLi context.CheckLegalLabels(Body, stmtList, bigBlock); } - public override void ComputeAllLabels(BigBlocksResolutionContext context) - { - context.ComputeAllLabels(Body); - } - - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List theSimpleCmds, - StmtList stmtList, + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, string runOffTheEndLabel) { WhileCmd wcmd = (WhileCmd) this; @@ -124,7 +118,7 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); // ... goto LoopHead; - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, + Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, new GotoCmd(wcmd.tok, new List {loopHeadLabel})); context.AddBlock(block); @@ -163,10 +157,16 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b } else { - trCmd = BigBlocksResolutionContext.GotoSuccessor(wcmd.tok, b); + trCmd = BigBlocksResolutionContext.GotoSuccessor(wcmd.tok, bigBlock); } block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); context.AddBlock(block); } + + public override IEnumerable StatementLists => new [] { Body }; + public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock) + { + context.RecordSuccessors(Body, bigBlock); + } } \ No newline at end of file From d879869516f051b97fbe6dc3fe8ca9c57f138cff Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 16 Sep 2024 16:34:41 +0200 Subject: [PATCH 6/9] Renames --- Source/Concurrency/LinearTypeChecker.cs | 14 +- Source/Core/AST/AbsyCmd.cs | 341 +----------------- Source/Core/AST/BigBlocksResolutionContext.cs | 152 ++++---- Source/Core/AST/Block.cs | 3 +- Source/Core/AST/Cmd.cs | 173 +++++++++ Source/Core/AST/Implementation.cs | 4 +- Source/Core/AST/StateCmd.cs | 136 +++++++ .../Core/AST/StructuredCommands/BreakCmd.cs | 61 +--- .../Core/AST/StructuredCommands/ByProofCmd.cs | 18 +- Source/Core/AST/StructuredCommands/IfCmd.cs | 151 ++++---- .../AST/StructuredCommands/StructuredCmd.cs | 5 +- .../Core/AST/StructuredCommands/WhileCmd.cs | 144 ++++---- 12 files changed, 555 insertions(+), 647 deletions(-) create mode 100644 Source/Core/AST/Cmd.cs create mode 100644 Source/Core/AST/StateCmd.cs diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 69e48cd62..e0dfaa0ee 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -764,8 +764,8 @@ private void CheckLinearStoreAccessInGuards() while (stmtLists.Count > 0) { var stmtList = stmtLists.Pop(); - stmtList.BigBlocks.Where(bigBlock => bigBlock.ec != null).ForEach(bigBlock => { - switch (bigBlock.ec) { + stmtList.BigBlocks.Where(bigBlock => bigBlock.Ec != null).ForEach(bigBlock => { + switch (bigBlock.Ec) { case IfCmd ifCmd: void ProcessIfCmd(IfCmd ifCmd) { @@ -773,14 +773,14 @@ void ProcessIfCmd(IfCmd ifCmd) { checkingContext.Error(ifCmd.tok, "access to linear store not allowed"); } - stmtLists.Push(ifCmd.thn); - if (ifCmd.elseIf != null) + stmtLists.Push(ifCmd.Thn); + if (ifCmd.ElseIf != null) { - ProcessIfCmd(ifCmd.elseIf); + ProcessIfCmd(ifCmd.ElseIf); } - else if (ifCmd.elseBlock != null) + else if (ifCmd.ElseBlock != null) { - stmtLists.Push(ifCmd.elseBlock); + stmtLists.Push(ifCmd.ElseBlock); } } ProcessIfCmd(ifCmd); diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 408619a1f..7296082ce 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -16,12 +16,11 @@ void ObjectInvariant() { Contract.Invariant(tok != null); Contract.Invariant(Anonymous || this.labelName != null); - Contract.Invariant(this._ec == null || this._tc == null); - Contract.Invariant(this._simpleCmds != null); + Contract.Invariant(this.ec == null || this._tc == null); + Contract.Invariant(this.prefixCmds != null); } - public readonly IToken /*!*/ - tok; + public readonly IToken /*!*/ tok; public readonly bool Anonymous; @@ -41,34 +40,34 @@ public string LabelName } } - [Rep] private List /*!*/ _simpleCmds; + [Rep] private List /*!*/ prefixCmds; /// /// These come before the structured command /// - public List /*!*/ simpleCmds + public List /*!*/ PrefixCmds { get { Contract.Ensures(Contract.Result>() != null); - return this._simpleCmds; + return this.prefixCmds; } set { Contract.Requires(value != null); - this._simpleCmds = value; + this.prefixCmds = value; } } - private StructuredCmd _ec; + private StructuredCmd ec; - public StructuredCmd ec + public StructuredCmd Ec { - get { return this._ec; } + get => ec; set { Contract.Requires(value == null || this.tc == null); - this._ec = value; + this.ec = value; } } @@ -79,24 +78,23 @@ public TransferCmd tc get { return this._tc; } set { - Contract.Requires(value == null || this.ec == null); + Contract.Requires(value == null || this.Ec == null); this._tc = value; } } - public BigBlock - successorBigBlock; // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized) + public BigBlock Successor; // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized) - public BigBlock(IToken tok, string labelName, [Captured] List simpleCmds, StructuredCmd ec, TransferCmd tc) + public BigBlock(IToken tok, string labelName, [Captured] List prefixCmds, StructuredCmd ec, TransferCmd tc) { - Contract.Requires(simpleCmds != null); + Contract.Requires(prefixCmds != null); Contract.Requires(tok != null); Contract.Requires(ec == null || tc == null); this.tok = tok; this.Anonymous = labelName == null; this.labelName = labelName; - this._simpleCmds = simpleCmds; - this._ec = ec; + this.prefixCmds = prefixCmds; + this.ec = ec; this._tc = tc; } @@ -111,15 +109,15 @@ public void Emit(TokenTextWriter stream, int level) : this.LabelName); } - foreach (Cmd /*!*/ c in this.simpleCmds) + foreach (Cmd /*!*/ c in this.PrefixCmds) { Contract.Assert(c != null); c.Emit(stream, level + 1); } - if (this.ec != null) + if (this.Ec != null) { - this.ec.Emit(stream, level + 1); + this.Ec.Emit(stream, level + 1); } else if (this.tc != null) { @@ -505,174 +503,6 @@ public static byte[] CombineChecksums(byte[] first, byte[] second, bool unordere } } - /// - /// Could have also been called a statement. - /// - /// Does not include commands that contain other commands, - /// for those, look at StructuredCmd - /// - /// - [ContractClass(typeof(CmdContracts))] - public abstract class Cmd : Absy - { - public List Layers; - - public byte[] Checksum { get; internal set; } - public byte[] SugaredCmdChecksum { get; internal set; } - public bool IrrelevantForChecksumComputation { get; set; } - - public Cmd(IToken /*!*/ tok) - : base(tok) - { - Contract.Assert(tok != null); - } - - public abstract void Emit(TokenTextWriter /*!*/ stream, int level); - - /// - /// Should only be called after resolution - /// - public IEnumerable GetAssignedVariables() { - List ids = new(); - AddAssignedIdentifiers(ids); - return ids.Select(id => id.Decl); - } - - public abstract void AddAssignedIdentifiers(List /*!*/ vars); - - public void CheckAssignments(TypecheckingContext tc) - { - Contract.Requires(tc != null); - var /*!*/ vars = GetAssignedVariables().ToList(); - foreach (Variable /*!*/ v in vars) - { - Contract.Assert(v != null); - if (!v.IsMutable) - { - tc.Error(this, "command assigns to an immutable variable: {0}", v.Name); - } - else if (tc.CheckModifies && v is GlobalVariable) - { - if (!tc.Yields && !tc.InFrame(v)) - { - tc.Error(this, - "command assigns to a global variable that is not in the enclosing {0} modifies clause: {1}", - tc.Proc is ActionDecl ? "action's" : "procedure's", v.Name); - } - } - } - } - - // Methods to simulate the old SimpleAssignCmd and MapAssignCmd - public static AssignCmd SimpleAssign(IToken tok, IdentifierExpr lhs, Expr rhs) - { - Contract.Requires(rhs != null); - Contract.Requires(lhs != null); - Contract.Requires(tok != null); - Contract.Ensures(Contract.Result() != null); - List /*!*/ - lhss = new List(); - List /*!*/ - rhss = new List(); - - lhss.Add(new SimpleAssignLhs(lhs.tok, lhs)); - rhss.Add(rhs); - - return new AssignCmd(tok, lhss, rhss); - } - - public static AssignCmd /*!*/ MapAssign(IToken tok, - IdentifierExpr /*!*/ map, - List /*!*/ indexes, Expr /*!*/ rhs) - { - Contract.Requires(tok != null); - Contract.Requires(map != null); - Contract.Requires(indexes != null); - Contract.Requires(rhs != null); - Contract.Ensures(Contract.Result() != null); - List /*!*/ - lhss = new List(); - List /*!*/ - rhss = new List(); - List /*!*/ - indexesList = new List(); - - - foreach (Expr e in indexes) - { - indexesList.Add(cce.NonNull(e)); - } - - lhss.Add(new MapAssignLhs(map.tok, - new SimpleAssignLhs(map.tok, map), - indexesList)); - rhss.Add(rhs); - - return new AssignCmd(tok, lhss, rhss); - } - - public static AssignCmd /*!*/ MapAssign(IToken tok, - IdentifierExpr /*!*/ map, - params Expr[] /*!*/ args) - { - Contract.Requires(tok != null); - Contract.Requires(map != null); - Contract.Requires(args != null); - Contract.Requires(args.Length > 0); // at least the rhs - Contract.Requires(Contract.ForAll(args, i => i != null)); - Contract.Ensures(Contract.Result() != null); - - List /*!*/ - lhss = new List(); - List /*!*/ - rhss = new List(); - List /*!*/ - indexesList = new List(); - - for (int i = 0; i < args.Length - 1; ++i) - { - indexesList.Add(cce.NonNull(args[i])); - } - - lhss.Add(new MapAssignLhs(map.tok, - new SimpleAssignLhs(map.tok, map), - indexesList)); - rhss.Add(cce.NonNull(args[args.Length - 1])); - - return new AssignCmd(tok, lhss, rhss); - } - - /// - /// This is a helper routine for printing a linked list of attributes. Each attribute - /// is terminated by a space. - /// - public static void EmitAttributes(TokenTextWriter stream, QKeyValue attributes) - { - Contract.Requires(stream != null); - - if (stream.UseForComputingChecksums) - { - return; - } - - for (QKeyValue kv = attributes; kv != null; kv = kv.Next) - { - kv.Emit(stream); - stream.Write(" "); - } - } - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - System.IO.StringWriter buffer = new System.IO.StringWriter(); - using TokenTextWriter stream = new TokenTextWriter("", buffer, false, false, PrintOptions.Default); - this.Emit(stream, 0); - - return buffer.ToString(); - } - } - public class CommentCmd : Cmd // just a convenience for debugging { public readonly string /*!*/ @@ -1528,137 +1358,6 @@ protected override Cmd ComputeDesugaring(PrintOptions options) } } - /// - /// A StateCmd is like an imperative-let binding around a sequence of commands. - /// There is no user syntax for a StateCmd. Instead, a StateCmd is only used - /// temporarily during the desugaring phase inside the VC generator. - /// - public class StateCmd : Cmd - { - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(this._locals != null); - Contract.Invariant(this._cmds != null); - } - - private List _locals; - - public /*readonly, except for the StandardVisitor*/ List /*!*/ Locals - { - get - { - Contract.Ensures(Contract.Result>() != null); - return this._locals; - } - internal set - { - Contract.Requires(value != null); - this._locals = value; - } - } - - private List _cmds; - - public /*readonly, except for the StandardVisitor*/ List /*!*/ Cmds - { - get - { - Contract.Ensures(Contract.Result>() != null); - return this._cmds; - } - set - { - Contract.Requires(value != null); - this._cmds = value; - } - } - - public StateCmd(IToken tok, List /*!*/ locals, List /*!*/ cmds) - : base(tok) - { - Contract.Requires(locals != null); - Contract.Requires(cmds != null); - Contract.Requires(tok != null); - this._locals = locals; - this._cmds = cmds; - } - - public override void Resolve(ResolutionContext rc) - { - //Contract.Requires(rc != null); - rc.PushVarContext(); - foreach (Variable /*!*/ v in Locals) - { - Contract.Assert(v != null); - rc.AddVariable(v); - } - - foreach (Cmd /*!*/ cmd in Cmds) - { - Contract.Assert(cmd != null); - cmd.Resolve(rc); - } - - rc.PopVarContext(); - } - - public override void AddAssignedIdentifiers(List vars) { - var vs = new List(); - foreach (Cmd cmd in Cmds) - { - Contract.Assert(cmd != null); - cmd.AddAssignedIdentifiers(vs); - } - - var localsSet = new HashSet(this.Locals); - foreach (var v in vs) - { - Debug.Assert(v.Decl != null); - if (!localsSet.Contains(v.Decl)) - { - vars.Add(v); - } - } - } - - public override void Typecheck(TypecheckingContext tc) - { - //Contract.Requires(tc != null); - foreach (Cmd /*!*/ cmd in Cmds) - { - Contract.Assert(cmd != null); - cmd.Typecheck(tc); - } - } - - public override void Emit(TokenTextWriter stream, int level) - { - //Contract.Requires(stream != null); - stream.WriteLine(this, level, "{"); - foreach (Variable /*!*/ v in Locals) - { - Contract.Assert(v != null); - v.Emit(stream, level + 1); - } - - foreach (Cmd /*!*/ c in Cmds) - { - Contract.Assert(c != null); - c.Emit(stream, level + 1); - } - - stream.WriteLine(level, "}"); - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitStateCmd(this); - } - } - [ContractClass(typeof(SugaredCmdContracts))] public abstract class SugaredCmd : Cmd { diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs index 7f3ee70eb..dcce234f9 100644 --- a/Source/Core/AST/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -6,27 +6,23 @@ namespace Microsoft.Boogie; public class BigBlocksResolutionContext { - StmtList /*!*/ stmtList; - - [Peer] List blocks; - - string /*!*/ prefix = "anon"; - - int anon = 0; - + private readonly StmtList /*!*/ rootList; + + [Peer] private List blocks; + private string /*!*/ prefix = "anon"; + private int anon = 0; + private readonly HashSet allLabels = new(); + private Errors ErrorHandler { get; } + public string FreshPrefix() { return prefix + anon++; } - HashSet allLabels = new(); - - public Errors ErrorHandler { get; } - [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(stmtList != null); + Contract.Invariant(rootList != null); Contract.Invariant(cce.NonNullElements(blocks, true)); Contract.Invariant(prefix != null); Contract.Invariant(cce.NonNullElements(allLabels, true)); @@ -47,28 +43,29 @@ private void ComputeAllLabels(StmtList stmts) allLabels.Add(bb.LabelName); } - if (bb.ec == null) + if (bb.Ec == null) { continue; } - foreach (var list in bb.ec.StatementLists) + foreach (var list in bb.Ec.StatementLists) { ComputeAllLabels(list); } } } - public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) + public BigBlocksResolutionContext(StmtList rootList, Errors errorHandler) { Contract.Requires(errorHandler != null); - Contract.Requires(stmtList != null); - this.stmtList = stmtList; + Contract.Requires(rootList != null); + this.rootList = rootList; + this.ErrorHandler = errorHandler; + // Inject an empty big block at the end of the body of a while loop if its current end is another while loop. // This transformation creates a suitable jump target for break statements inside the nested while loop. - InjectEmptyBigBlockInsideWhileLoopBody(stmtList); - this.ErrorHandler = errorHandler; - ComputeAllLabels(stmtList); + InjectEmptyBigBlockInsideWhileLoopBody(rootList); + ComputeAllLabels(rootList); } public void AddBlock(Block block) @@ -76,46 +73,62 @@ public void AddBlock(Block block) blocks.Add(block); } - public List /*!*/ Blocks + public List /*!*/ GetOrComputeBlocks { get { Contract.Ensures(cce.NonNullElements(Contract.Result>())); - if (blocks == null) + if (blocks != null) { - blocks = new List(); + return blocks; + } - int startErrorCount = this.ErrorHandler.count; - // Check that all goto statements go to a label in allLabels, and no break statement to a non-enclosing loop. - // Also, determine a good value for "prefix". - CheckLegalLabels(stmtList, null, null); + blocks = new List(); - // fill in names of anonymous blocks - NameAnonymousBlocks(stmtList); + int startErrorCount = this.ErrorHandler.count; + // Check that all goto statements go to a label in allLabels, and no break statement to a non-enclosing loop. + // Also, determine a good value for "prefix". + CheckLegalLabels(rootList, null, null); - // determine successor blocks - RecordSuccessors(stmtList, null); + // fill in names of anonymous blocks + NameAnonymousBlocks(rootList); - if (this.ErrorHandler.count == startErrorCount) - { - // generate blocks from the big blocks - CreateBlocks(stmtList, null); - } + // determine successor blocks + RecordSuccessors(rootList, null); + + if (this.ErrorHandler.count == startErrorCount) + { + // generate blocks from the big blocks + CreateBlocks(rootList, null); } return blocks; } } - public void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) + private static void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) { foreach (var bb in stmtList.BigBlocks) { - bb.ec.InjectEmptyBigBlockInsideWhileLoopBody(this); + foreach (var childList in bb.Ec.StatementLists) + { + InjectEmptyBigBlockInsideWhileLoopBody(childList); + } + + if (bb.Ec is not WhileCmd whileCmd) + { + continue; + } + + var newBigBlocks = new List(whileCmd.Body.BigBlocks) + { + new(Token.NoToken, null, new List(), null, null) + }; + whileCmd.Body = new StmtList(newBigBlocks, whileCmd.Body.EndCurly); } } - public void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) + private void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) { Contract.Requires(stmtList != null); Contract.Requires((parentContext == null) == (parentBigBlock == null)); @@ -148,13 +161,12 @@ public void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock } // check that labels in this and nested StmtList's are legal - foreach (BigBlock b in stmtList.BigBlocks) + foreach (var bigBlock in stmtList.BigBlocks) { // goto's must reference blocks in enclosing blocks - if (b.tc is GotoCmd) + if (bigBlock.tc is GotoCmd gotoCmd) { - GotoCmd g = (GotoCmd) b.tc; - foreach (string /*!*/ lbl in cce.NonNull(g.labelNames)) + foreach (string /*!*/ lbl in cce.NonNull(gotoCmd.labelNames)) { Contract.Assert(lbl != null); /* @@ -171,28 +183,28 @@ public void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock */ if (!allLabels.Contains(lbl)) { - this.ErrorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined"); + this.ErrorHandler.SemErr(gotoCmd.tok, "Error: goto label '" + lbl + "' is undefined"); } } } else { - b.ec.CheckLegalLabels(this, this.stmtList, b); + foreach (var childList in bigBlock.Ec.StatementLists) + { + CheckLegalLabels(childList, this.rootList, bigBlock); + } } } } - void NameAnonymousBlocks(StmtList stmtList) + private void NameAnonymousBlocks(StmtList stmtList) { Contract.Requires(stmtList != null); - foreach (BigBlock b in stmtList.BigBlocks) + foreach (var b in stmtList.BigBlocks) { - if (b.LabelName == null) - { - b.LabelName = FreshPrefix(); - } + b.LabelName ??= FreshPrefix(); - foreach (var l in b.ec.StatementLists) + foreach (var l in b.Ec.StatementLists) { NameAnonymousBlocks(l); } @@ -205,9 +217,9 @@ public void RecordSuccessors(StmtList stmtList, BigBlock successor) for (int i = stmtList.BigBlocks.Count; 0 <= --i;) { BigBlock big = stmtList.BigBlocks[i]; - big.successorBigBlock = successor; + big.Successor = successor; - big.ec.RecordSuccessors(this, big); + big.Ec.RecordSuccessors(this, big); successor = big; } } @@ -218,52 +230,52 @@ public void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) { Contract.Requires(stmtList != null); Contract.Requires(blocks != null); - List cmdPrefixToApply = stmtList.PrefixCommands; + var cmdPrefixToApply = stmtList.PrefixCommands; int n = stmtList.BigBlocks.Count; - foreach (BigBlock b in stmtList.BigBlocks) + foreach (var childBigBlock in stmtList.BigBlocks) { n--; - Contract.Assert(b.LabelName != null); + Contract.Assert(childBigBlock.LabelName != null); List theSimpleCmds; if (cmdPrefixToApply == null) { - theSimpleCmds = b.simpleCmds; + theSimpleCmds = childBigBlock.PrefixCmds; } else { theSimpleCmds = new List(); theSimpleCmds.AddRange(cmdPrefixToApply); - theSimpleCmds.AddRange(b.simpleCmds); + theSimpleCmds.AddRange(childBigBlock.PrefixCmds); cmdPrefixToApply = null; // now, we've used 'em up } - if (b.tc != null) + if (childBigBlock.tc != null) { // this BigBlock has the very same components as a Block - Contract.Assert(b.ec == null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, b.tc); + Contract.Assert(childBigBlock.Ec == null); + var block = new Block(childBigBlock.tok, childBigBlock.LabelName, theSimpleCmds, childBigBlock.tc); blocks.Add(block); } - else if (b.ec == null) + else if (childBigBlock.Ec == null) { TransferCmd trCmd; if (n == 0 && runOffTheEndLabel != null) { // goto the given label instead of the textual successor block - trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); + trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); } else { - trCmd = GotoSuccessor(stmtList.EndCurly, b); + trCmd = GotoSuccessor(stmtList.EndCurly, childBigBlock); } - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, trCmd); + Block block = new Block(childBigBlock.tok, childBigBlock.LabelName, theSimpleCmds, trCmd); blocks.Add(block); } else { - b.ec.CreateBlocks(this, b, theSimpleCmds, n == 0 ? runOffTheEndLabel : null); + childBigBlock.Ec.CreateBlocks(this, childBigBlock, theSimpleCmds, n == 0 ? runOffTheEndLabel : null); } } } @@ -273,9 +285,9 @@ public static TransferCmd GotoSuccessor(IToken tok, BigBlock b) Contract.Requires(b != null); Contract.Requires(tok != null); Contract.Ensures(Contract.Result() != null); - if (b.successorBigBlock != null) + if (b.Successor != null) { - return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); + return new GotoCmd(tok, new List {b.Successor.LabelName}); } else { diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/Block.cs index bcc077050..f5680c764 100644 --- a/Source/Core/AST/Block.cs +++ b/Source/Core/AST/Block.cs @@ -49,8 +49,7 @@ public IEnumerable Exits() } [Rep] //PM: needed to verify Traverse.Visit - public TransferCmd - TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) + public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) public byte[] Checksum; diff --git a/Source/Core/AST/Cmd.cs b/Source/Core/AST/Cmd.cs new file mode 100644 index 000000000..80238910b --- /dev/null +++ b/Source/Core/AST/Cmd.cs @@ -0,0 +1,173 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie; + +/// +/// Could have also been called a statement. +/// +/// Does not include commands that contain other commands, +/// for those, look at StructuredCmd +/// +/// +[ContractClass(typeof(CmdContracts))] +public abstract class Cmd : Absy +{ + public List Layers; + + public byte[] Checksum { get; internal set; } + public byte[] SugaredCmdChecksum { get; internal set; } + public bool IrrelevantForChecksumComputation { get; set; } + + public Cmd(IToken /*!*/ tok) + : base(tok) + { + Contract.Assert(tok != null); + } + + public abstract void Emit(TokenTextWriter /*!*/ stream, int level); + + /// + /// Should only be called after resolution + /// + public IEnumerable GetAssignedVariables() { + List ids = new(); + AddAssignedIdentifiers(ids); + return ids.Select(id => id.Decl); + } + + public abstract void AddAssignedIdentifiers(List /*!*/ vars); + + protected void CheckAssignments(TypecheckingContext tc) + { + Contract.Requires(tc != null); + var /*!*/ vars = GetAssignedVariables().ToList(); + foreach (Variable /*!*/ v in vars) + { + Contract.Assert(v != null); + if (!v.IsMutable) + { + tc.Error(this, "command assigns to an immutable variable: {0}", v.Name); + } + else if (tc.CheckModifies && v is GlobalVariable) + { + if (!tc.Yields && !tc.InFrame(v)) + { + tc.Error(this, + "command assigns to a global variable that is not in the enclosing {0} modifies clause: {1}", + tc.Proc is ActionDecl ? "action's" : "procedure's", v.Name); + } + } + } + } + + // Methods to simulate the old SimpleAssignCmd and MapAssignCmd + public static AssignCmd SimpleAssign(IToken tok, IdentifierExpr lhs, Expr rhs) + { + Contract.Requires(rhs != null); + Contract.Requires(lhs != null); + Contract.Requires(tok != null); + Contract.Ensures(Contract.Result() != null); + List /*!*/ + lhss = new List(); + List /*!*/ + rhss = new List(); + + lhss.Add(new SimpleAssignLhs(lhs.tok, lhs)); + rhss.Add(rhs); + + return new AssignCmd(tok, lhss, rhss); + } + + public static AssignCmd /*!*/ MapAssign(IToken tok, + IdentifierExpr /*!*/ map, + List /*!*/ indexes, Expr /*!*/ rhs) + { + Contract.Requires(tok != null); + Contract.Requires(map != null); + Contract.Requires(indexes != null); + Contract.Requires(rhs != null); + Contract.Ensures(Contract.Result() != null); + List /*!*/ + lhss = new List(); + List /*!*/ + rhss = new List(); + List /*!*/ + indexesList = new List(); + + + foreach (Expr e in indexes) + { + indexesList.Add(cce.NonNull(e)); + } + + lhss.Add(new MapAssignLhs(map.tok, + new SimpleAssignLhs(map.tok, map), + indexesList)); + rhss.Add(rhs); + + return new AssignCmd(tok, lhss, rhss); + } + + public static AssignCmd /*!*/ MapAssign(IToken tok, + IdentifierExpr /*!*/ map, + params Expr[] /*!*/ args) + { + Contract.Requires(tok != null); + Contract.Requires(map != null); + Contract.Requires(args != null); + Contract.Requires(args.Length > 0); // at least the rhs + Contract.Requires(Contract.ForAll(args, i => i != null)); + Contract.Ensures(Contract.Result() != null); + + List /*!*/ + lhss = new List(); + List /*!*/ + rhss = new List(); + List /*!*/ + indexesList = new List(); + + for (int i = 0; i < args.Length - 1; ++i) + { + indexesList.Add(cce.NonNull(args[i])); + } + + lhss.Add(new MapAssignLhs(map.tok, + new SimpleAssignLhs(map.tok, map), + indexesList)); + rhss.Add(cce.NonNull(args[^1])); + + return new AssignCmd(tok, lhss, rhss); + } + + /// + /// This is a helper routine for printing a linked list of attributes. Each attribute + /// is terminated by a space. + /// + public static void EmitAttributes(TokenTextWriter stream, QKeyValue attributes) + { + Contract.Requires(stream != null); + + if (stream.UseForComputingChecksums) + { + return; + } + + for (QKeyValue kv = attributes; kv != null; kv = kv.Next) + { + kv.Emit(stream); + stream.Write(" "); + } + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + System.IO.StringWriter buffer = new System.IO.StringWriter(); + using TokenTextWriter stream = new TokenTextWriter("", buffer, false, false, PrintOptions.Default); + this.Emit(stream, 0); + + return buffer.ToString(); + } +} \ No newline at end of file diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs index 9169f014b..8259d629a 100644 --- a/Source/Core/AST/Implementation.cs +++ b/Source/Core/AST/Implementation.cs @@ -388,8 +388,8 @@ public Implementation(IToken /*!*/ tok, Contract.Requires(errorHandler != null); LocVars = localVariables; StructuredStmts = structuredStmts; - BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts, errorHandler); - Blocks = ctx.Blocks; + var ctx = new BigBlocksResolutionContext(structuredStmts, errorHandler); + Blocks = ctx.GetOrComputeBlocks; BlockPredecessorsComputed = false; scc = null; Attributes = kv; diff --git a/Source/Core/AST/StateCmd.cs b/Source/Core/AST/StateCmd.cs new file mode 100644 index 000000000..0df5c45e7 --- /dev/null +++ b/Source/Core/AST/StateCmd.cs @@ -0,0 +1,136 @@ +using System.Collections.Generic; +using System.Diagnostics; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie; + +/// +/// A StateCmd is like an imperative-let binding around a sequence of commands. +/// There is no user syntax for a StateCmd. Instead, a StateCmd is only used +/// temporarily during the desugaring phase inside the VC generator. +/// +public class StateCmd : Cmd +{ + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(this.locals != null); + Contract.Invariant(this.cmds != null); + } + + private List locals; + + public /*readonly, except for the StandardVisitor*/ List /*!*/ Locals + { + get + { + Contract.Ensures(Contract.Result>() != null); + return this.locals; + } + internal set + { + Contract.Requires(value != null); + this.locals = value; + } + } + + private List cmds; + + public /*readonly, except for the StandardVisitor*/ List /*!*/ Cmds + { + get + { + Contract.Ensures(Contract.Result>() != null); + return this.cmds; + } + set + { + Contract.Requires(value != null); + this.cmds = value; + } + } + + public StateCmd(IToken tok, List /*!*/ locals, List /*!*/ cmds) + : base(tok) + { + Contract.Requires(locals != null); + Contract.Requires(cmds != null); + Contract.Requires(tok != null); + this.locals = locals; + this.cmds = cmds; + } + + public override void Resolve(ResolutionContext rc) + { + //Contract.Requires(rc != null); + rc.PushVarContext(); + foreach (Variable /*!*/ v in Locals) + { + Contract.Assert(v != null); + rc.AddVariable(v); + } + + foreach (Cmd /*!*/ cmd in Cmds) + { + Contract.Assert(cmd != null); + cmd.Resolve(rc); + } + + rc.PopVarContext(); + } + + public override void AddAssignedIdentifiers(List vars) { + var vs = new List(); + foreach (Cmd cmd in Cmds) + { + Contract.Assert(cmd != null); + cmd.AddAssignedIdentifiers(vs); + } + + var localsSet = new HashSet(this.Locals); + foreach (var v in vs) + { + Debug.Assert(v.Decl != null); + if (!localsSet.Contains(v.Decl)) + { + vars.Add(v); + } + } + } + + public override void Typecheck(TypecheckingContext tc) + { + //Contract.Requires(tc != null); + foreach (Cmd /*!*/ cmd in Cmds) + { + Contract.Assert(cmd != null); + cmd.Typecheck(tc); + } + } + + public override void Emit(TokenTextWriter stream, int level) + { + //Contract.Requires(stream != null); + stream.WriteLine(this, level, "{"); + foreach (Variable /*!*/ v in Locals) + { + Contract.Assert(v != null); + v.Emit(stream, level + 1); + } + + foreach (Cmd /*!*/ c in Cmds) + { + Contract.Assert(c != null); + c.Emit(stream, level + 1); + } + + stream.WriteLine(level, "}"); + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitStateCmd(this); + } +} \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/BreakCmd.cs b/Source/Core/AST/StructuredCommands/BreakCmd.cs index 4d30a955d..f02c266d3 100644 --- a/Source/Core/AST/StructuredCommands/BreakCmd.cs +++ b/Source/Core/AST/StructuredCommands/BreakCmd.cs @@ -28,68 +28,11 @@ public override void Emit(TokenTextWriter stream, int level) } } - public override void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context) - { - } - - public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock) - { - Contract.Assert(BreakEnclosure == null); // it hasn't been initialized yet - bool found = false; - for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) - { - cce.LoopInvariant(sl != null); - BigBlock bb = sl.ParentBigBlock; - - if (Label == null) - { - // a label-less break statement breaks out of the innermost enclosing while statement - if (bb.ec is WhileCmd) - { - BreakEnclosure = bb; - found = true; - break; - } - } - else if (Label == bb.LabelName) - { - // a break statement with a label can break out of both if statements and while statements - if (bb.simpleCmds.Count == 0) - { - // this is a good target: the label refers to the if/while statement - BreakEnclosure = bb; - } - else - { - // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement - context.ErrorHandler.SemErr(tok, - "Error: break label '" + Label + "' must designate an enclosing statement"); - } - - found = true; // don't look any further, since we've found a matching label - break; - } - } - - if (!found) - { - if (Label == null) - { - context.ErrorHandler.SemErr(tok, "Error: break statement is not inside a loop"); - } - else - { - context.ErrorHandler.SemErr(tok, - "Error: break label '" + Label + "' must designate an enclosing statement"); - } - } - } - - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List incomingCommands, string runOffTheEndLabel) { Contract.Assert(this.BreakEnclosure != null); - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, BigBlocksResolutionContext.GotoSuccessor(bigBlock.ec.tok, BreakEnclosure)); + Block block = new Block(bigBlock.tok, bigBlock.LabelName, incomingCommands, BigBlocksResolutionContext.GotoSuccessor(bigBlock.Ec.tok, BreakEnclosure)); context.AddBlock(block); } diff --git a/Source/Core/AST/StructuredCommands/ByProofCmd.cs b/Source/Core/AST/StructuredCommands/ByProofCmd.cs index 818c50700..32a78c6ea 100644 --- a/Source/Core/AST/StructuredCommands/ByProofCmd.cs +++ b/Source/Core/AST/StructuredCommands/ByProofCmd.cs @@ -16,25 +16,17 @@ public override void Emit(TokenTextWriter stream, int level) throw new System.NotImplementedException(); } - public override void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context) - { - throw new System.NotImplementedException(); - } - - public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock) - { - throw new System.NotImplementedException(); - } - - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List incomingCommands, string runOffTheEndLabel) { - throw new System.NotImplementedException(); + bigBlock.LabelName + context.CreateBlocks(Proof, null); + context.CreateBlocks(Body, runOffTheEndLabel); } public override IEnumerable StatementLists => new[] { Body, Proof }; public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock) { - throw new System.NotImplementedException(); + context.RecordSuccessors(Body, bigBlock.Successor); } } \ No newline at end of file diff --git a/Source/Core/AST/StructuredCommands/IfCmd.cs b/Source/Core/AST/StructuredCommands/IfCmd.cs index c4a9300c5..29207f0fa 100644 --- a/Source/Core/AST/StructuredCommands/IfCmd.cs +++ b/Source/Core/AST/StructuredCommands/IfCmd.cs @@ -6,12 +6,11 @@ namespace Microsoft.Boogie; public class IfCmd : StructuredCmd { - public Expr Guard; + public readonly Expr Guard; - private StmtList /*!*/ - _thn; + private StmtList /*!*/ _thn; - public StmtList /*!*/ thn + public StmtList /*!*/ Thn { get { @@ -25,27 +24,27 @@ public StmtList /*!*/ thn } } - private IfCmd _elseIf; + private IfCmd elseIf; - public IfCmd elseIf + public IfCmd ElseIf { - get { return this._elseIf; } + get => this.elseIf; set { - Contract.Requires(value == null || this.elseBlock == null); - this._elseIf = value; + Contract.Requires(value == null || this.ElseBlock == null); + this.elseIf = value; } } - private StmtList _elseBlock; + private StmtList elseBlock; - public StmtList elseBlock + public StmtList ElseBlock { - get { return this._elseBlock; } + get => this.elseBlock; set { - Contract.Requires(value == null || this.elseIf == null); - this._elseBlock = value; + Contract.Requires(value == null || this.ElseIf == null); + this.elseBlock = value; } } @@ -53,7 +52,7 @@ public StmtList elseBlock void ObjectInvariant() { Contract.Invariant(this._thn != null); - Contract.Invariant(this._elseIf == null || this._elseBlock == null); + Contract.Invariant(this.elseIf == null || this.elseBlock == null); } public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, StmtList elseBlock) @@ -64,8 +63,8 @@ public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, Stm Contract.Requires(elseIf == null || elseBlock == null); this.Guard = guard; this._thn = thn; - this._elseIf = elseIf; - this._elseBlock = elseBlock; + this.elseIf = elseIf; + this.elseBlock = elseBlock; } public override void Emit(TokenTextWriter stream, int level) @@ -87,20 +86,20 @@ public override void Emit(TokenTextWriter stream, int level) stream.WriteLine(")"); stream.WriteLine(level, "{"); - ifcmd.thn.Emit(stream, level + 1); + ifcmd.Thn.Emit(stream, level + 1); stream.WriteLine(level, "}"); - if (ifcmd.elseIf != null) + if (ifcmd.ElseIf != null) { stream.Write(level, "else if ("); - ifcmd = ifcmd.elseIf; + ifcmd = ifcmd.ElseIf; continue; } - else if (ifcmd.elseBlock != null) + else if (ifcmd.ElseBlock != null) { stream.WriteLine(level, "else"); stream.WriteLine(level, "{"); - ifcmd.elseBlock.Emit(stream, level + 1); + ifcmd.ElseBlock.Emit(stream, level + 1); stream.WriteLine(level, "}"); } @@ -108,108 +107,86 @@ public override void Emit(TokenTextWriter stream, int level) } } - public override void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context) - { - context.InjectEmptyBigBlockInsideWhileLoopBody(thn); - if (elseBlock != null) - { - context.InjectEmptyBigBlockInsideWhileLoopBody(elseBlock); - } - - if (elseIf != null) - { - elseIf.InjectEmptyBigBlockInsideWhileLoopBody(context); - } - } - - public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock) - { - for (IfCmd ifcmd = this; ifcmd != null; ifcmd = ifcmd.elseIf) - { - context.CheckLegalLabels(ifcmd.thn, stmtList, bigBlock); - if (ifcmd.elseBlock != null) - { - context.CheckLegalLabels(ifcmd.elseBlock, stmtList, bigBlock); - } - } - } - - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List incomingCommands, string runOffTheEndLabel) { - IfCmd ifcmd = (IfCmd) bigBlock.ec; - string predLabel = bigBlock.LabelName; - List predCmds = theSimpleCmds; + var ifcmd = this; + string previousLabel = bigBlock.LabelName; + var previousCommands = incomingCommands; - for (; ifcmd != null; ifcmd = ifcmd.elseIf) + for (; ifcmd != null; ifcmd = ifcmd.ElseIf) { var prefix = context.FreshPrefix(); string thenLabel = prefix + "_Then"; - Contract.Assert(thenLabel != null); string elseLabel = prefix + "_Else"; - Contract.Assert(elseLabel != null); - List ssThen = new List(); - List ssElse = new List(); + var ssThen = new List(); + var ssElse = new List(); if (ifcmd.Guard != null) { - var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard) + { + Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null) + }; ssThen.Add(ac); - ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)) + { + Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null) + }; ssElse.Add(ac); } // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock - bool thenGuardTakenCareOf = ifcmd.thn.PrefixFirstBlock(ssThen, ref thenLabel); + bool thenGuardTakenCareOf = ifcmd.Thn.PrefixFirstBlock(ssThen, ref thenLabel); bool elseGuardTakenCareOf = false; - if (ifcmd.elseBlock != null) + if (ifcmd.ElseBlock != null) { - elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel); + elseGuardTakenCareOf = ifcmd.ElseBlock.PrefixFirstBlock(ssElse, ref elseLabel); } // ... goto Then, Else; - var jumpBlock = new Block(bigBlock.tok, predLabel, predCmds, - new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); + var jumpBlock = new Block(bigBlock.tok, previousLabel, previousCommands, + new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); context.AddBlock(jumpBlock); if (!thenGuardTakenCareOf) { // Then: assume guard; goto firstThenBlock; var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen, - new GotoCmd(ifcmd.tok, new List {ifcmd.thn.BigBlocks[0].LabelName})); + new GotoCmd(ifcmd.tok, new List {ifcmd.Thn.BigBlocks[0].LabelName})); context.AddBlock(thenJumpBlock); } // recurse to create the blocks for the then branch - context.CreateBlocks(ifcmd.thn, runOffTheEndLabel); + context.CreateBlocks(ifcmd.Thn, runOffTheEndLabel); - if (ifcmd.elseBlock != null) + if (ifcmd.ElseBlock != null) { - Contract.Assert(ifcmd.elseIf == null); + Contract.Assert(ifcmd.ElseIf == null); if (!elseGuardTakenCareOf) { // Else: assume !guard; goto firstElseBlock; var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse, - new GotoCmd(ifcmd.tok, new List {ifcmd.elseBlock.BigBlocks[0].LabelName})); + new GotoCmd(ifcmd.tok, new List {ifcmd.ElseBlock.BigBlocks[0].LabelName})); context.AddBlock(elseJumpBlock); } // recurse to create the blocks for the else branch - context.CreateBlocks(ifcmd.elseBlock, runOffTheEndLabel); + context.CreateBlocks(ifcmd.ElseBlock, runOffTheEndLabel); } - else if (ifcmd.elseIf != null) + else if (ifcmd.ElseIf != null) { // this is an "else if" - predLabel = elseLabel; - predCmds = new List(); + previousLabel = elseLabel; + previousCommands = new List(); if (ifcmd.Guard != null) { - var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - predCmds.Add(ac); + var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)) + { + Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null) + }; + previousCommands.Add(ac); } } else @@ -220,7 +197,7 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b if (runOffTheEndLabel != null) { // goto the given label instead of the textual successor block - trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); + trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); } else { @@ -236,12 +213,12 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b public override IEnumerable StatementLists { get { - for (var ifcmd = this; ifcmd != null; ifcmd = ifcmd.elseIf) + for (var ifcmd = this; ifcmd != null; ifcmd = ifcmd.ElseIf) { - yield return ifcmd.thn; - if (ifcmd.elseBlock != null) + yield return ifcmd.Thn; + if (ifcmd.ElseBlock != null) { - yield return ifcmd.elseBlock; + yield return ifcmd.ElseBlock; } } } @@ -249,12 +226,12 @@ public override IEnumerable StatementLists { public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock) { - for (var ifcmd = this; ifcmd != null; ifcmd = ifcmd.elseIf) + for (var ifcmd = this; ifcmd != null; ifcmd = ifcmd.ElseIf) { - context.RecordSuccessors(ifcmd.thn, bigBlock.successorBigBlock); - if (ifcmd.elseBlock != null) + context.RecordSuccessors(ifcmd.Thn, bigBlock.Successor); + if (ifcmd.ElseBlock != null) { - context.RecordSuccessors(ifcmd.elseBlock, bigBlock.successorBigBlock); + context.RecordSuccessors(ifcmd.ElseBlock, bigBlock.Successor); } } } diff --git a/Source/Core/AST/StructuredCommands/StructuredCmd.cs b/Source/Core/AST/StructuredCommands/StructuredCmd.cs index ac386320f..57be50ed6 100644 --- a/Source/Core/AST/StructuredCommands/StructuredCmd.cs +++ b/Source/Core/AST/StructuredCommands/StructuredCmd.cs @@ -37,10 +37,7 @@ public StructuredCmd(IToken tok) public abstract void Emit(TokenTextWriter /*!*/ stream, int level); - public abstract void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context); - public abstract void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock); - - public abstract void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, + public abstract void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List incomingCommands, string runOffTheEndLabel); public abstract IEnumerable StatementLists { get; } diff --git a/Source/Core/AST/StructuredCommands/WhileCmd.cs b/Source/Core/AST/StructuredCommands/WhileCmd.cs index 80aa07cd1..42e49da31 100644 --- a/Source/Core/AST/StructuredCommands/WhileCmd.cs +++ b/Source/Core/AST/StructuredCommands/WhileCmd.cs @@ -1,7 +1,6 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; -using System.Linq; namespace Microsoft.Boogie; @@ -28,10 +27,10 @@ public WhileCmd(IToken tok, [Captured] Expr guard, List invariants Contract.Requires(cce.NonNullElements(invariants)); Contract.Requires(body != null); Contract.Requires(tok != null); - this.Guard = guard; - this.Invariants = invariants; - this.Yields = yields; - this.Body = body; + Guard = guard; + Invariants = invariants; + Yields = yields; + Body = body; } public override void Emit(TokenTextWriter stream, int level) @@ -74,97 +73,78 @@ public override void Emit(TokenTextWriter stream, int level) stream.WriteLine(level, "}"); } - public override void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context) + public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List incomingCommands, + string runOffTheEndLabel) { - context.InjectEmptyBigBlockInsideWhileLoopBody(Body); - if (Body.BigBlocks.Count <= 0 || Body.BigBlocks.Last().ec is not WhileCmd) + var prefix = context.FreshPrefix(); + string loopHeadLabel = prefix + "_LoopHead"; + string /*!*/ loopBodyLabel = prefix + "_LoopBody"; + string loopDoneLabel = prefix + "_LoopDone"; + + List ssBody = new List(); + List ssDone = new List(); + if (Guard != null) { - return; - } + var ac = new AssumeCmd(tok, Guard); + ac.Attributes = new QKeyValue(tok, "partition", new List(), null); + ssBody.Add(ac); - var newBigBlocks = new List(Body.BigBlocks); - newBigBlocks.Add(new BigBlock(Token.NoToken, null, new List(), null, null)); - Body = new StmtList(newBigBlocks, Body.EndCurly); - } + ac = new AssumeCmd(tok, Expr.Not(Guard)); + ac.Attributes = new QKeyValue(tok, "partition", new List(), null); + ssDone.Add(ac); + } - public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock) - { - context.CheckLegalLabels(Body, stmtList, bigBlock); - } + // Try to squeeze in ssBody into the first block of wcmd.Body + bool bodyGuardTakenCareOf = Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List theSimpleCmds, - string runOffTheEndLabel) - { - WhileCmd wcmd = (WhileCmd) this; - var prefix = context.FreshPrefix(); - string loopHeadLabel = prefix + "_LoopHead"; - string /*!*/ loopBodyLabel = prefix + "_LoopBody"; - string loopDoneLabel = prefix + "_LoopDone"; - - List ssBody = new List(); - List ssDone = new List(); - if (wcmd.Guard != null) - { - var ac = new AssumeCmd(wcmd.tok, wcmd.Guard); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); - ssBody.Add(ac); + // ... goto LoopHead; + Block block = new Block(bigBlock.tok, bigBlock.LabelName, incomingCommands, + new GotoCmd(tok, new List {loopHeadLabel})); + context.AddBlock(block); - ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard)); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); - ssDone.Add(ac); - } + // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; + List ssHead = new List(); + foreach (CallCmd yield in Yields) + { + ssHead.Add(yield); + } + foreach (PredicateCmd inv in Invariants) + { + ssHead.Add(inv); + } - // Try to squeeze in ssBody into the first block of wcmd.Body - bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); + block = new Block(tok, loopHeadLabel, ssHead, + new GotoCmd(tok, new List {loopDoneLabel, loopBodyLabel})); + context.AddBlock(block); - // ... goto LoopHead; - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, - new GotoCmd(wcmd.tok, new List {loopHeadLabel})); - context.AddBlock(block); - - // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; - List ssHead = new List(); - foreach (CallCmd yield in wcmd.Yields) - { - ssHead.Add(yield); - } - foreach (PredicateCmd inv in wcmd.Invariants) - { - ssHead.Add(inv); - } - - block = new Block(wcmd.tok, loopHeadLabel, ssHead, - new GotoCmd(wcmd.tok, new List {loopDoneLabel, loopBodyLabel})); + if (!bodyGuardTakenCareOf) + { + // LoopBody: assume guard; goto firstLoopBlock; + block = new Block(tok, loopBodyLabel, ssBody, + new GotoCmd(tok, new List {Body.BigBlocks[0].LabelName})); context.AddBlock(block); + } - if (!bodyGuardTakenCareOf) - { - // LoopBody: assume guard; goto firstLoopBlock; - block = new Block(wcmd.tok, loopBodyLabel, ssBody, - new GotoCmd(wcmd.tok, new List {wcmd.Body.BigBlocks[0].LabelName})); - context.AddBlock(block); - } - - // recurse to create the blocks for the loop body - context.CreateBlocks(wcmd.Body, loopHeadLabel); + // recurse to create the blocks for the loop body + context.CreateBlocks(Body, loopHeadLabel); - // LoopDone: assume !guard; goto loopSuccessor; - TransferCmd trCmd; - if (runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = BigBlocksResolutionContext.GotoSuccessor(wcmd.tok, bigBlock); - } + // LoopDone: assume !guard; goto loopSuccessor; + TransferCmd trCmd; + if (runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(tok, new List {runOffTheEndLabel}); + } + else + { + trCmd = BigBlocksResolutionContext.GotoSuccessor(tok, bigBlock); + } - block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); - context.AddBlock(block); + block = new Block(tok, loopDoneLabel, ssDone, trCmd); + context.AddBlock(block); } - public override IEnumerable StatementLists => new [] { Body }; + public override IEnumerable StatementLists => new[] { Body }; public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock) { context.RecordSuccessors(Body, bigBlock); From b03d169830a3a362632ea91c2abdd0afe259feb0 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 23 Sep 2024 16:24:15 +0200 Subject: [PATCH 7/9] Allow marking variables so that they're not havocced after a loop --- Source/Core/AST/Absy.cs | 3 +- Source/Core/AST/CallCmd.cs | 6 ++-- .../Core/AST/StructuredCommands/ByProofCmd.cs | 32 ------------------- Source/VCGeneration/Split.cs | 4 +++ .../VerificationConditionGenerator.cs | 19 ++++++----- 5 files changed, 17 insertions(+), 47 deletions(-) delete mode 100644 Source/Core/AST/StructuredCommands/ByProofCmd.cs diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 307f898cf..c02f61267 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -1286,7 +1286,7 @@ void ObjectInvariant() Contract.Invariant(this.typedIdent != null); } - public Variable(IToken tok, TypedIdent typedIdent) + protected Variable(IToken tok, TypedIdent typedIdent) : base(tok, typedIdent.Name) { Contract.Requires(tok != null); @@ -1304,6 +1304,7 @@ public Variable(IToken tok, TypedIdent typedIdent, QKeyValue kv) } public abstract bool IsMutable { get; } + public bool MayBeHavoccedAfterLoop { get; } public override void Emit(TokenTextWriter stream, int level) { diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs index d39768d22..bf0c52a29 100644 --- a/Source/Core/AST/CallCmd.cs +++ b/Source/Core/AST/CallCmd.cs @@ -14,11 +14,9 @@ public class CallCmd : CallCommonality // Element of the following lists can be null, which means that // the call happens with * as these parameters - public List /*!*/ - Ins; + public List /*!*/ Ins; - public List /*!*/ - Outs; + public List /*!*/ Outs; [ContractInvariantMethod] void ObjectInvariant() diff --git a/Source/Core/AST/StructuredCommands/ByProofCmd.cs b/Source/Core/AST/StructuredCommands/ByProofCmd.cs deleted file mode 100644 index 32a78c6ea..000000000 --- a/Source/Core/AST/StructuredCommands/ByProofCmd.cs +++ /dev/null @@ -1,32 +0,0 @@ -using System.Collections.Generic; - -namespace Microsoft.Boogie; - -public class ByProofCmd : StructuredCmd -{ - public StmtList Body; - public StmtList Proof; - - public ByProofCmd(IToken tok) : base(tok) - { - } - - public override void Emit(TokenTextWriter stream, int level) - { - throw new System.NotImplementedException(); - } - - public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List incomingCommands, - string runOffTheEndLabel) - { - bigBlock.LabelName - context.CreateBlocks(Proof, null); - context.CreateBlocks(Body, runOffTheEndLabel); - } - - public override IEnumerable StatementLists => new[] { Body, Proof }; - public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock) - { - context.RecordSuccessors(Body, bigBlock.Successor); - } -} \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 7cf747118..89b2874aa 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -119,6 +119,10 @@ private void PrintSplitDeclarations(TokenTextWriter writer) foreach (var declaration in PrunedDeclarations.Except(functionAxioms.Concat(constantAxioms)).ToList()) { + if (declaration is Implementation || declaration is Procedure) + { + continue; + } declaration.Emit(writer, 0); } diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index b53424ac4..d9a82286a 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -935,23 +935,22 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary varsToHavoc = VarsAssignedInLoop(g, header); - List havocExprs = new List(); - foreach (Variable v in varsToHavoc) + var havocExprs = new HashSet(); + foreach (Variable variable in varsToHavoc) { - Contract.Assert(v != null); - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - if (!havocExprs.Contains(ie)) + Contract.Assert(variable != null); + if (variable.MayBeHavoccedAfterLoop) { - havocExprs.Add(ie); + continue; } + havocExprs.Add(new IdentifierExpr(Token.NoToken, variable)); } // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct // the source location for this later on - HavocCmd hc = new HavocCmd(header.tok, havocExprs); - List newCmds = new List(); - newCmds.Add(hc); - foreach (Cmd c in header.Cmds) + HavocCmd hc = new HavocCmd(header.tok, havocExprs.ToList()); + var newCmds = new List { hc }; + foreach (var c in header.Cmds) { newCmds.Add(c); } From 90ac56d6ddca857dab99aa11c65b021fd108d99a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 23 Sep 2024 16:25:58 +0200 Subject: [PATCH 8/9] Rename --- Source/Core/AST/Absy.cs | 2 +- Source/VCGeneration/VerificationConditionGenerator.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index c02f61267..1863112a8 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -1304,7 +1304,7 @@ public Variable(IToken tok, TypedIdent typedIdent, QKeyValue kv) } public abstract bool IsMutable { get; } - public bool MayBeHavoccedAfterLoop { get; } + public bool Monotonic { get; } public override void Emit(TokenTextWriter stream, int level) { diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index d9a82286a..40575c1cb 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -939,7 +939,7 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary Date: Wed, 25 Sep 2024 15:09:18 +0200 Subject: [PATCH 9/9] Format atg --- Source/Core/AST/BigBlocksResolutionContext.cs | 1 + Source/Core/BoogiePL.atg | 8 ++++---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs index dcce234f9..2d195907e 100644 --- a/Source/Core/AST/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; namespace Microsoft.Boogie; diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 0cdf885ff..569365335 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1153,10 +1153,10 @@ LabelOrCmd { Attribute } Proposition (. c = new AssertCmd(x, e, kv); .) ";" - | "check" (. x = t; .) - { Attribute } - Proposition (. c = new AssertCmd(x, e, kv) { Remember = false }; .) - ";" + | "check" (. x = t; .) + { Attribute } + Proposition (. c = new AssertCmd(x, e, kv) { Remember = false }; .) + ";" | "assume" (. x = t; .) { Attribute } Proposition (. c = new AssumeCmd(x, e, kv); .)