//----------------------------------------------------------------------------- // // Copyright (C) Microsoft Corporation. All Rights Reserved. // //----------------------------------------------------------------------------- //--------------------------------------------------------------------------------------------- // BoogiePL - Absy.cs //--------------------------------------------------------------------------------------------- namespace Microsoft.Boogie { using System; using System.Collections; using System.Diagnostics; using System.Collections.Generic; using Microsoft.Boogie.AbstractInterpretation; using AI = Microsoft.AbstractInterpretationFramework; using Microsoft.Contracts; //--------------------------------------------------------------------- // BigBlock public class BigBlock { public readonly IToken! tok; public string LabelName; public readonly bool Anonymous; invariant !Anonymous ==> LabelName != null; [Rep] public CmdSeq! simpleCmds; public StructuredCmd ec; public TransferCmd tc; invariant ec == null || tc == null; public BigBlock successorBigBlock; // null if successor is end of proceduure body (or if field has not yet been initialized) public BigBlock(IToken! tok, string? labelName, [Captured] CmdSeq! simpleCmds, StructuredCmd? ec, TransferCmd? tc) requires ec == null || tc == null; { this.tok = tok; this.LabelName = labelName; this.Anonymous = labelName == null; this.simpleCmds = simpleCmds; this.ec = ec; this.tc = tc; } public void Emit(TokenTextWriter! stream, int level) { if (!Anonymous) { stream.WriteLine(level, "{0}:", CommandLineOptions.Clo.PrintWithUniqueASTIds ? String.Format("h{0}^^{1}", this.GetHashCode(), this.LabelName) : this.LabelName); } foreach (Cmd! c in this.simpleCmds) { c.Emit(stream, level+1); } if (this.ec != null) { this.ec.Emit(stream, level+1); } else if (this.tc != null) { this.tc.Emit(stream, level+1); } } } public class StmtList { [Rep] public readonly List! BigBlocks; public CmdSeq PrefixCommands; public readonly IToken! EndCurly; public StmtList ParentContext; public BigBlock ParentBigBlock; public Set! Labels = new Set(); public StmtList([Captured] List! bigblocks, IToken! endCurly) requires bigblocks.Count > 0; { this.BigBlocks = bigblocks; this.EndCurly = endCurly; } // prints the list of statements, not the surrounding curly braces public void Emit(TokenTextWriter! stream, int level) { bool needSeperator = false; foreach (BigBlock b in BigBlocks) { assume b.IsPeerConsistent; if (needSeperator) { stream.WriteLine(); } b.Emit(stream, level); needSeperator = true; } } /// /// Tries to insert the commands "prefixCmds" at the beginning of the first block /// of the StmtList, and returns "true" iff it succeeded. /// In the event of success, the "suggestedLabel" returns as the name of the /// block inside StmtList where "prefixCmds" were inserted. This name may be the /// same as the one passed in, in case this StmtList has no preference as to what /// to call its first block. In the event of failure, "suggestedLabel" is returned /// as its input value. /// Note, to be conservative (that is, ignoring the possible optimization that this /// method enables), this method can do nothing and return false. /// public bool PrefixFirstBlock([Captured] CmdSeq! prefixCmds, ref string! suggestedLabel) ensures !result ==> Owner.None(prefixCmds); // "prefixCmds" is captured only on success { assume PrefixCommands == null; // prefix has not been used BigBlock bb0 = BigBlocks[0]; if (prefixCmds.Length == 0) { // This is always a success, since there is nothing to insert. Now, decide // which name to use for the first block. if (bb0.Anonymous) { bb0.LabelName = suggestedLabel; } else { assert bb0.LabelName != null; suggestedLabel = bb0.LabelName; } return true; } else { // There really is something to insert. We can do this inline only if the first // block is anonymous (which implies there is no branch to it from within the block). if (bb0.Anonymous) { PrefixCommands = prefixCmds; bb0.LabelName = suggestedLabel; return true; } else { return false; } } } } /// /// The AST for Boogie structured commands was designed to support backward compatibility with /// the Boogie unstructured commands. This has made the structured commands hard to construct. /// The StmtListBuilder class makes it easier to build structured commands. /// public class StmtListBuilder { List! bigBlocks = new List(); string label; CmdSeq simpleCmds; void Dump(StructuredCmd scmd, TransferCmd tcmd) requires scmd == null || tcmd == null; ensures label == null && simpleCmds == null; { if (label == null && simpleCmds == null && scmd == null && tcmd == null) { // nothing to do } else { if (simpleCmds == null) { simpleCmds = new CmdSeq(); } bigBlocks.Add(new BigBlock(Token.NoToken, label, simpleCmds, scmd, tcmd)); label = null; simpleCmds = null; } } /// /// Collects the StmtList built so far and returns it. The StmtListBuilder should no longer /// be used once this method has been invoked. /// public StmtList! Collect(IToken! endCurlyBrace) { Dump(null, null); if (bigBlocks.Count == 0) { simpleCmds = new CmdSeq(); // the StmtList constructor doesn't like an empty list of BigBlock's Dump(null, null); } return new StmtList(bigBlocks, endCurlyBrace); } public void Add(Cmd! cmd) { if (simpleCmds == null) { simpleCmds = new CmdSeq(); } simpleCmds.Add(cmd); } public void Add(StructuredCmd! scmd) { Dump(scmd, null); } public void Add(TransferCmd! tcmd) { Dump(null, tcmd); } public void AddLabelCmd(string! label) { Dump(null, null); this.label = label; } public void AddLocalVariable(string! name) { // TODO } } class BigBlocksResolutionContext { StmtList! stmtList; [Peer] List blocks; string! prefix = "anon"; int anon = 0; Set allLabels = new Set(); Errors! errorHandler; public BigBlocksResolutionContext(StmtList! stmtList, Errors! errorHandler) { this.stmtList = stmtList; this.errorHandler = errorHandler; } public List! Blocks { get { if (blocks == null) { blocks = new List(); int startErrorCount = this.errorHandler.count; // Check that there are no goto's into the middle of a block, 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 CheckLegalLabels(StmtList! stmtList, StmtList parentContext, BigBlock parentBigBlock) requires parentContext == null <==> parentBigBlock == null; requires stmtList.ParentContext == null; // it hasn't been set yet modifies stmtList.*; 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.Labels.Add(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 (!)g.labelNames) { 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"); } } } // break labels must refer to an enclosing while statement else if (b.ec is BreakCmd) { BreakCmd bcmd = (BreakCmd)b.ec; assert bcmd.BreakEnclosure == null; // it hasn't been initialized yet bool found = false; for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) invariant 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.Length == 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) { foreach (BigBlock b in stmtList.BigBlocks) { if (b.LabelName == null) { b.LabelName = prefix + anon; anon++; } 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) { 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, successor); } 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) requires blocks != null; { CmdSeq cmdPrefixToApply = stmtList.PrefixCommands; int n = stmtList.BigBlocks.Count; foreach (BigBlock b in stmtList.BigBlocks) { n--; assert b.LabelName != null; CmdSeq theSimpleCmds; if (cmdPrefixToApply == null) { theSimpleCmds = b.simpleCmds; } else { theSimpleCmds = new CmdSeq(); 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 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 StringSeq(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; 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; string loopHeadLabel = prefix + anon + "_LoopHead"; string! loopBodyLabel = prefix + anon + "_LoopBody"; string loopDoneLabel = prefix + anon + "_LoopDone"; anon++; CmdSeq ssBody = new CmdSeq(); CmdSeq ssDone = new CmdSeq(); if (wcmd.Guard != null) { ssBody.Add(new AssumeCmd(wcmd.tok, wcmd.Guard)); ssDone.Add(new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard))); } // 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 StringSeq(loopHeadLabel))); blocks.Add(block); // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; CmdSeq ssHead = new CmdSeq(); foreach (PredicateCmd inv in wcmd.Invariants) { ssHead.Add(inv); } block = new Block(wcmd.tok, loopHeadLabel, ssHead, new GotoCmd(wcmd.tok, new StringSeq(loopDoneLabel, loopBodyLabel))); blocks.Add(block); if (!bodyGuardTakenCareOf) { // LoopBody: assume guard; goto firstLoopBlock; block = new Block(wcmd.tok, loopBodyLabel, ssBody, new GotoCmd(wcmd.tok, new StringSeq(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 StringSeq(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; CmdSeq predCmds = theSimpleCmds; for (; ifcmd != null; ifcmd = ifcmd.elseIf) { string! thenLabel = prefix + anon + "_Then"; string! elseLabel = prefix + anon + "_Else"; anon++; CmdSeq ssThen = new CmdSeq(); CmdSeq ssElse = new CmdSeq(); if (ifcmd.Guard != null) { ssThen.Add(new AssumeCmd(ifcmd.tok, ifcmd.Guard)); ssElse.Add(new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard))); } // 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; Block block = new Block(b.tok, predLabel, predCmds, new GotoCmd(ifcmd.tok, new StringSeq(thenLabel, elseLabel))); blocks.Add(block); if (!thenGuardTakenCareOf) { // Then: assume guard; goto firstThenBlock; block = new Block(ifcmd.tok, thenLabel, ssThen, new GotoCmd(ifcmd.tok, new StringSeq(ifcmd.thn.BigBlocks[0].LabelName))); blocks.Add(block); } // recurse to create the blocks for the then branch CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null); if (ifcmd.elseBlock != null) { assert ifcmd.elseIf == null; if (!elseGuardTakenCareOf) { // Else: assume !guard; goto firstElseBlock; block = new Block(ifcmd.tok, elseLabel, ssElse, new GotoCmd(ifcmd.tok, new StringSeq(ifcmd.elseBlock.BigBlocks[0].LabelName))); blocks.Add(block); } // 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 CmdSeq(); if (ifcmd.Guard != null) { predCmds.Add(new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard))); } } 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 StringSeq(runOffTheEndLabel)); } else { trCmd = GotoSuccessor(ifcmd.tok, b); } block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); blocks.Add(block); } } } } } TransferCmd! GotoSuccessor(IToken! tok, BigBlock! b) { if (b.successorBigBlock != null) { return new GotoCmd(tok, new StringSeq(b.successorBigBlock.LabelName)); } else { return new ReturnCmd(tok); } } } public abstract class StructuredCmd { public IToken! tok; public StructuredCmd(IToken! tok) { this.tok = tok; } public abstract void Emit(TokenTextWriter! stream, int level); } public class IfCmd : StructuredCmd { public Expr? Guard; public StmtList! thn; public IfCmd? elseIf; public StmtList elseBlock; invariant elseIf == null || elseBlock == null; public IfCmd(IToken! tok, Expr? guard, StmtList! thn, IfCmd? elseIf, StmtList elseBlock) : base(tok) requires elseIf == null || elseBlock == null; { this.Guard = guard; this.thn = thn; this.elseIf = elseIf; this.elseBlock = elseBlock; // base(tok); } 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 StmtList! Body; public WhileCmd(IToken! tok, [Captured] Expr? guard, List! invariants, StmtList! body) : base(tok) { this.Guard = guard; this.Invariants = invariants; this.Body = body; /// base(tok); } public override void Emit(TokenTextWriter! stream, int level) { stream.Write(level, "while ("); if (Guard == null) { stream.Write("*"); } else { Guard.Emit(stream); } stream.WriteLine(")"); foreach (PredicateCmd inv in Invariants) { if (inv is AssumeCmd) { stream.Write(level + 1, "free invariant "); } else { stream.Write(level + 1, "invariant "); } inv.Expr.Emit(stream); stream.WriteLine(";"); } stream.WriteLine(level, "{"); Body.Emit(stream, level + 1); stream.WriteLine(level, "}"); } } public class BreakCmd : StructuredCmd { public string Label; public BigBlock BreakEnclosure; public BreakCmd(IToken! tok, string? label) : base(tok) { this.Label = label; // base(tok); } public override void Emit(TokenTextWriter! stream, int level) { if (Label == null) { stream.WriteLine(level, "break;"); } else { stream.WriteLine(level, "break {0};", Label); } } } //--------------------------------------------------------------------- // Block public sealed class Block : Absy { public string! Label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal [Rep] [ElementsPeer] public CmdSeq! Cmds; [Rep] //PM: needed to verify Traverse.Visit public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) // Abstract interpretation // public bool currentlyTraversed; public enum VisitState {ToVisit, BeingVisited, AlreadyVisited}; // used by WidenPoints.Compute public VisitState TraversingStatus; public bool widenBlock; public int iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not // Block-specific invariants... public AI.Lattice Lattice; // The lattice used for the analysis of this block public AI.Lattice.Element PreInvariant; // The initial abstract states for this block public AI.Lattice.Element PostInvariant; // The exit abstract states for this block // KRML: We want to include the following invariant, but at the moment, doing so causes a run-time error (something about committed): invariant PreInvariant != null <==> PostInvariant != null; // VC generation and SCC computation public BlockSeq! Predecessors; public Set liveVarsBefore; public bool IsLive(Variable! v) { if (liveVarsBefore == null) return true; return liveVarsBefore.Contains(v); } public Block() { this(Token.NoToken, "", new CmdSeq(), new ReturnCmd(Token.NoToken));} public Block (IToken! tok, string! label, CmdSeq! cmds, TransferCmd transferCmd) : base(tok) { this.Label = label; this.Cmds = cmds; this.TransferCmd = transferCmd; this.PreInvariant = null; this.PostInvariant = null; this.Predecessors = new BlockSeq(); this.liveVarsBefore = null; this.TraversingStatus = VisitState.ToVisit; this.iterations = 0; // base(tok); } public void Emit (TokenTextWriter! stream, int level) { stream.WriteLine(); stream.WriteLine( this, level, "{0}:{1}", CommandLineOptions.Clo.PrintWithUniqueASTIds ? String.Format("h{0}^^{1}", this.GetHashCode(), this.Label) : this.Label, this.widenBlock ? " // cut point" : ""); foreach (Cmd! c in this.Cmds) { c.Emit(stream, level + 1); } assume this.TransferCmd != null; this.TransferCmd.Emit(stream, level + 1); } public void Register (ResolutionContext! rc) { rc.AddBlock(this); } public override void Resolve (ResolutionContext! rc) { foreach (Cmd! c in Cmds) { c.Resolve(rc); } assume this.TransferCmd != null; TransferCmd.Resolve(rc); } public override void Typecheck (TypecheckingContext! tc) { foreach (Cmd! c in Cmds) { c.Typecheck(tc); } assume this.TransferCmd != null; TransferCmd.Typecheck(tc); } /// /// Reset the abstract intepretation state of this block. It does this by putting the iterations to 0 and the pre and post states to null /// public void ResetAbstractInterpretationState() { // this.currentlyTraversed = false; this.TraversingStatus = VisitState.ToVisit; this.iterations = 0; this.Lattice = null; this.PreInvariant = null; this.PostInvariant = null; } [Pure] public override string! ToString() { return this.Label + (this.widenBlock? "[w]" : ""); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitBlock(this); } } //--------------------------------------------------------------------- // Commands public abstract class Cmd : Absy { public Cmd(IToken! tok) : base(tok) { } public abstract void Emit(TokenTextWriter! stream, int level); public abstract void AddAssignedVariables(VariableSeq! vars); public void CheckAssignments(TypecheckingContext! tc) { VariableSeq! vars = new VariableSeq(); this.AddAssignedVariables(vars); foreach (Variable! v in vars) { if (!v.IsMutable) { tc.Error(this, "command assigns to an immutable variable: {0}", v.Name); } else if (v is GlobalVariable && !tc.InFrame(v)) { tc.Error(this, "command assigns to a global variable that is not in the enclosing method's modifies clause: {0}", v.Name); } } } // Methods to simulate the old SimpleAssignCmd and MapAssignCmd public static AssignCmd! SimpleAssign(IToken! tok, IdentifierExpr! lhs, Expr! rhs) { 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, ExprSeq! indexes, Expr! rhs) { List! lhss = new List (); List! rhss = new List (); List! indexesList = new List (); foreach (Expr e in indexes) indexesList.Add((!)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) requires args.Length > 0; // at least the rhs requires forall{int i in (0:args.Length); args[i] != null}; { List! lhss = new List (); List! rhss = new List (); List! indexesList = new List (); for (int i = 0; i < args.Length - 1; ++i) indexesList.Add((!)args[i]); lhss.Add(new MapAssignLhs (map.tok, new SimpleAssignLhs (map.tok, map), indexesList)); rhss.Add((!)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) { for (QKeyValue kv = attributes; kv != null; kv = kv.Next) { kv.Emit(stream); stream.Write(" "); } } public static void ResolveAttributes(QKeyValue attributes, ResolutionContext! rc) { for (QKeyValue kv = attributes; kv != null; kv = kv.Next) { kv.Resolve(rc); } } public static void TypecheckAttributes(QKeyValue attributes, TypecheckingContext! tc) { for (QKeyValue kv = attributes; kv != null; kv = kv.Next) { kv.Typecheck(tc); } } } public class CommentCmd : Cmd // just a convenience for debugging { public readonly string! Comment; public CommentCmd (string! c) : base(Token.NoToken) { Comment = c; // base(Token.NoToken); } public override void Emit(TokenTextWriter! stream, int level) { if (this.Comment.Contains("\n")) { stream.WriteLine(this, level, "/* {0} */", this.Comment); } else { stream.WriteLine(this, level, "// {0}", this.Comment); } } public override void Resolve(ResolutionContext! rc) { } public override void AddAssignedVariables(VariableSeq! vars) { } public override void Typecheck(TypecheckingContext! tc) { } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitCommentCmd(this); } } // class for parallel assignments, which subsumes both the old // SimpleAssignCmd and the old MapAssignCmd public class AssignCmd : Cmd { public List! Lhss; public List! Rhss; public AssignCmd(IToken! tok, List! lhss, List! rhss) { base(tok); Lhss = lhss; Rhss = rhss; } public override void Emit(TokenTextWriter! stream, int level) { stream.Write(this, level, ""); string! sep = ""; foreach (AssignLhs! l in Lhss) { stream.Write(sep); sep = ", "; l.Emit(stream); } stream.Write(" := "); sep = ""; foreach (Expr! e in Rhss) { stream.Write(sep); sep = ", "; e.Emit(stream); } stream.WriteLine(";"); } public override void Resolve(ResolutionContext! rc) { if (Lhss.Count != Rhss.Count) rc.Error(this, "number of left-hand sides does not match number of right-hand sides"); foreach (AssignLhs! e in Lhss) e.Resolve(rc); foreach (Expr! e in Rhss) e.Resolve(rc); // check for double occurrences of assigned variables // (could be optimised) for (int i = 0; i < Lhss.Count; ++i) { for (int j = i + 1; j < Lhss.Count; ++j) { if (((!)Lhss[i].DeepAssignedVariable).Equals( Lhss[j].DeepAssignedVariable)) rc.Error(Lhss[j], "variable {0} is assigned more than once in parallel assignment", Lhss[j].DeepAssignedVariable); } } } public override void Typecheck(TypecheckingContext! tc) { foreach (AssignLhs! e in Lhss) e.Typecheck(tc); foreach (Expr! e in Rhss) e.Typecheck(tc); this.CheckAssignments(tc); for (int i = 0; i < Lhss.Count; ++i) { Type ltype = Lhss[i].Type; Type rtype = Rhss[i].Type; if (ltype != null && rtype != null) { // otherwise, there has already been an error when // typechecking the lhs or rhs if (!ltype.Unify(rtype)) tc.Error(Lhss[i], "mismatched types in assignment command (cannot assign {0} to {1})", rtype, ltype); } } } public override void AddAssignedVariables(VariableSeq! vars) { foreach (AssignLhs! l in Lhss) vars.Add(l.DeepAssignedVariable); } // transform away the syntactic sugar of map assignments and // determine an equivalent assignment in which all rhs are simple // variables public AssignCmd! AsSimpleAssignCmd { get { List! newLhss = new List (); List! newRhss = new List (); for (int i = 0; i < Lhss.Count; ++i) { IdentifierExpr! newLhs; Expr! newRhs; Lhss[i].AsSimpleAssignment(Rhss[i], out newLhs, out newRhs); newLhss.Add(new SimpleAssignLhs(Token.NoToken, newLhs)); newRhss.Add(newRhs); } return new AssignCmd(Token.NoToken, newLhss, newRhss); } } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitAssignCmd(this); } } // There are two different kinds of left-hand sides in assignments: // simple variables (identifiers), or locations of a map public abstract class AssignLhs : Absy { // The type of the lhs is determined during typechecking public abstract Type Type { get; } // Determine the variable that is actually assigned in this lhs public abstract IdentifierExpr! DeepAssignedIdentifier { get; } public abstract Variable DeepAssignedVariable { get; } public AssignLhs(IToken! tok) : base(tok) {} public abstract void Emit(TokenTextWriter! stream); public abstract Expr! AsExpr { get; } // transform away the syntactic sugar of map assignments and // determine an equivalent simple assignment internal abstract void AsSimpleAssignment(Expr! rhs, out IdentifierExpr! simpleLhs, out Expr! simpleRhs); } public class SimpleAssignLhs : AssignLhs { public IdentifierExpr! AssignedVariable; public override Type Type { get { return AssignedVariable.Type; } } public override IdentifierExpr! DeepAssignedIdentifier { get { return AssignedVariable; } } public override Variable DeepAssignedVariable { get { return AssignedVariable.Decl; } } public SimpleAssignLhs(IToken! tok, IdentifierExpr! assignedVariable) { base(tok); AssignedVariable = assignedVariable; } public override void Resolve(ResolutionContext! rc) { AssignedVariable.Resolve(rc); } public override void Typecheck(TypecheckingContext! tc) { AssignedVariable.Typecheck(tc); } public override void Emit(TokenTextWriter! stream) { AssignedVariable.Emit(stream); } public override Expr! AsExpr { get { return AssignedVariable; } } internal override void AsSimpleAssignment(Expr! rhs, out IdentifierExpr! simpleLhs, out Expr! simpleRhs) { simpleLhs = AssignedVariable; simpleRhs = rhs; } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitSimpleAssignLhs(this); } } // A map-assignment-lhs (m[t1, t2, ...] := ...) is quite similar to // a map select expression, but it is cleaner to keep those two // things separate public class MapAssignLhs : AssignLhs { public AssignLhs! Map; public List! Indexes; // The instantiation of type parameters of the map that is // determined during type checking. public TypeParamInstantiation TypeParameters = null; private Type TypeAttr = null; public override Type Type { get { return TypeAttr; } } public override IdentifierExpr! DeepAssignedIdentifier { get { return Map.DeepAssignedIdentifier; } } public override Variable DeepAssignedVariable { get { return Map.DeepAssignedVariable; } } public MapAssignLhs(IToken! tok, AssignLhs! map, List! indexes) { base(tok); Map = map; Indexes = indexes; } public override void Resolve(ResolutionContext! rc) { Map.Resolve(rc); foreach (Expr! e in Indexes) e.Resolve(rc); } public override void Typecheck(TypecheckingContext! tc) { Map.Typecheck(tc); foreach (Expr! e in Indexes) e.Typecheck(tc); // we use the same typechecking code as in MapSelect ExprSeq! selectArgs = new ExprSeq (); foreach (Expr! e in Indexes) selectArgs.Add(e); TypeParamInstantiation! tpInsts; TypeAttr = MapSelect.Typecheck((!)Map.Type, Map, selectArgs, out tpInsts, tc, tok, "map assignment"); TypeParameters = tpInsts; } public override void Emit(TokenTextWriter! stream) { Map.Emit(stream); stream.Write("["); string! sep = ""; foreach (Expr! e in Indexes) { stream.Write(sep); sep = ", "; e.Emit(stream); } stream.Write("]"); } public override Expr! AsExpr { get { NAryExpr! res = Expr.Select(Map.AsExpr, Indexes); res.TypeParameters = this.TypeParameters; return res; } } internal override void AsSimpleAssignment(Expr! rhs, out IdentifierExpr! simpleLhs, out Expr! simpleRhs) { NAryExpr! newRhs = Expr.Store(Map.AsExpr, Indexes, rhs); newRhs.TypeParameters = this.TypeParameters; Map.AsSimpleAssignment(newRhs, out simpleLhs, out simpleRhs); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitMapAssignLhs(this); } } /// /// 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 { public /*readonly, except for the StandardVisitor*/ VariableSeq! Locals; public /*readonly, except for the StandardVisitor*/ CmdSeq! Cmds; public StateCmd(IToken! tok, VariableSeq! locals, CmdSeq! cmds) : base(tok) { this.Locals = locals; this.Cmds = cmds; // base(tok); } public override void Resolve(ResolutionContext! rc) { rc.PushVarContext(); foreach (Variable! v in Locals) { rc.AddVariable(v, false); } foreach (Cmd! cmd in Cmds) { cmd.Resolve(rc); } rc.PopVarContext(); } public override void AddAssignedVariables(VariableSeq! vars) { VariableSeq! vs = new VariableSeq(); foreach (Cmd! cmd in this.Cmds) { cmd.AddAssignedVariables(vs); } System.Collections.Hashtable! localsSet = new System.Collections.Hashtable(); foreach (Variable! local in this.Locals) { localsSet[local] = bool.TrueString; } foreach (Variable! v in vs) { if (!localsSet.ContainsKey(v)) { vars.Add(v); } } } public override void Typecheck(TypecheckingContext! tc) { foreach (Cmd! cmd in Cmds) { cmd.Typecheck(tc); } } public override void Emit(TokenTextWriter! stream, int level) { stream.WriteLine(this, level, "{"); foreach (Variable! v in Locals) { v.Emit(stream, level+1); } foreach (Cmd! c in Cmds) { c.Emit(stream, level+1); } stream.WriteLine(level, "}"); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitStateCmd(this); } } abstract public class SugaredCmd : Cmd { private Cmd desugaring; // null until desugared public SugaredCmd(IToken! tok) : base(tok) {} public Cmd! Desugaring { get { if (desugaring == null) { desugaring = ComputeDesugaring(); } return desugaring; } } protected abstract Cmd! ComputeDesugaring(); public override void Emit(TokenTextWriter! stream, int level) { if (CommandLineOptions.Clo.PrintDesugarings) { stream.WriteLine(this, level, "/*** desugaring:"); Desugaring.Emit(stream, level); stream.WriteLine(level, "**** end desugaring */"); } } } public abstract class CallCommonality : SugaredCmd { public QKeyValue Attributes; protected CallCommonality(IToken! tok, QKeyValue kv) { base(tok); Attributes = kv; } protected enum TempVarKind { Formal, Old, Bound } // We have to give the type explicitly, because the type of the formal "likeThisOne" can contain type variables protected Variable! CreateTemporaryVariable(VariableSeq! tempVars, Variable! likeThisOne, Type! ty, TempVarKind kind) { string! tempNamePrefix; switch (kind) { case TempVarKind.Formal: tempNamePrefix = "formal@"; break; case TempVarKind.Old: tempNamePrefix = "old@"; break; case TempVarKind.Bound: tempNamePrefix = "forall@"; break; default: assert false; // unexpected kind } TypedIdent ti = likeThisOne.TypedIdent; TypedIdent newTi = new TypedIdent(ti.tok, "call" + UniqueId + tempNamePrefix + ti.Name, ty); Variable! v; if (kind == TempVarKind.Bound) { v = new BoundVariable(likeThisOne.tok, newTi); } else { v = new LocalVariable(likeThisOne.tok, newTi); tempVars.Add(v); } return v; } } public class CallCmd : CallCommonality, IPotentialErrorNode { string! callee; public Procedure Proc; // Element of the following lists can be null, which means that // the call happens with * as these parameters public List! Ins; public List! Outs; //public Lattice.Element StateAfterCall; // The instantiation of type parameters that is determined during // type checking public TypeParamInstantiation TypeParameters = null; // TODO: convert to use generics private object errorData; public object ErrorData { get { return errorData; } set { errorData = value; } } public CallCmd(IToken! tok, string! callee, ExprSeq! ins, IdentifierExprSeq! outs) { List! insList = new List (); List! outsList = new List (); foreach (Expr e in ins) insList.Add(e); foreach (IdentifierExpr e in outs) outsList.Add(e); this(tok, callee, insList, outsList); } public CallCmd(IToken! tok, string! callee, List! ins, List! outs) { base(tok, null); this.callee = callee; this.Ins = ins; this.Outs = outs; } public CallCmd(IToken! tok, string! callee, List! ins, List! outs, QKeyValue kv) { base(tok, kv); this.callee = callee; this.Ins = ins; this.Outs = outs; } public override void Emit(TokenTextWriter! stream, int level) { stream.Write(this, level, "call "); EmitAttributes(stream, Attributes); string sep = ""; if (Outs.Count > 0) { foreach (Expr arg in Outs) { stream.Write(sep); sep = ", "; if (arg == null) { stream.Write("*"); } else { arg.Emit(stream); } } stream.Write(" := "); } stream.Write(TokenTextWriter.SanitizeIdentifier(callee)); stream.Write("("); sep = ""; foreach (Expr arg in Ins) { stream.Write(sep); sep = ", "; if (arg == null) { stream.Write("*"); } else { arg.Emit(stream); } } stream.WriteLine(");"); base.Emit(stream, level); } public override void Resolve(ResolutionContext! rc) { if (Proc != null) { // already resolved return; } ResolveAttributes(Attributes, rc); Proc = rc.LookUpProcedure(callee) as Procedure; if (Proc == null) { rc.Error(this, "call to undeclared procedure: {0}", callee); } foreach (Expr e in Ins) { if (e!=null) { e.Resolve(rc); } } Set/**/ actualOuts = new Set/**/ (Outs.Count); foreach (IdentifierExpr ide in Outs) { if (ide != null) { ide.Resolve(rc); if (ide.Decl != null) { if (actualOuts[ide.Decl]) { rc.Error(this, "left-hand side of call command contains variable twice: {0}", ide.Name); } else { actualOuts.Add(ide.Decl); } } } } if (Proc == null) return; // first make sure that the right number of parameters is given // (a similar check is in CheckArgumentTypes, but we are not // able to call this method because it cannot cope with Ins/Outs // that are null) if (Ins.Count != Proc.InParams.Length) { rc.Error(this.tok, "wrong number of arguments in call to {0}: {1}", callee, Ins.Count); return; } if (Outs.Count != Proc.OutParams.Length) { rc.Error(this.tok, "wrong number of result variables in call to {0}: {1}", callee, Outs.Count); return; } if (QKeyValue.FindBoolAttribute(this.Attributes, "async")) { if (Proc.OutParams.Length > 1) { rc.Error(this.tok, "a procedure called asynchronously can have at most one output parameter"); return; } } // Check that type parameters can be determined using the given // actual i/o arguments. This is done already during resolution // because CheckBoundVariableOccurrences needs a resolution // context TypeSeq! formalInTypes = new TypeSeq(); TypeSeq! formalOutTypes = new TypeSeq(); for (int i = 0; i < Ins.Count; ++i) if (Ins[i] != null) formalInTypes.Add(((!)Proc.InParams[i]).TypedIdent.Type); for (int i = 0; i < Outs.Count; ++i) if (Outs[i] != null) formalOutTypes.Add(((!)Proc.OutParams[i]).TypedIdent.Type); // we need to bind the type parameters for this // (this is expected by CheckBoundVariableOccurrences) int previousTypeBinderState = rc.TypeBinderState; try { foreach (TypeVariable! v in Proc.TypeParameters) rc.AddTypeBinder(v); Type.CheckBoundVariableOccurrences(Proc.TypeParameters, formalInTypes, formalOutTypes, this.tok, "types of given arguments", rc); } finally { rc.TypeBinderState = previousTypeBinderState; } } public override void AddAssignedVariables(VariableSeq! vars) { foreach (IdentifierExpr e in Outs) { if (e!=null) { vars.Add(e.Decl); } } assume this.Proc != null; foreach (IdentifierExpr! e in this.Proc.Modifies) { vars.Add(e.Decl); } } public override void Typecheck(TypecheckingContext! tc) { assume this.Proc != null; // we assume the CallCmd has been successfully resolved before calling this Typecheck method TypecheckAttributes(Attributes, tc); // typecheck in-parameters foreach (Expr e in Ins) if (e!=null) e.Typecheck(tc); foreach (Expr e in Outs) if (e!=null) e.Typecheck(tc); this.CheckAssignments(tc); TypeSeq! formalInTypes = new TypeSeq(); TypeSeq! formalOutTypes = new TypeSeq(); ExprSeq! actualIns = new ExprSeq(); IdentifierExprSeq! actualOuts = new IdentifierExprSeq(); for (int i = 0; i < Ins.Count; ++i) { if (Ins[i] != null) { formalInTypes.Add(((!)Proc.InParams[i]).TypedIdent.Type); actualIns.Add(Ins[i]); } } for (int i = 0; i < Outs.Count; ++i) { if (Outs[i] != null) { formalOutTypes.Add(((!)Proc.OutParams[i]).TypedIdent.Type); actualOuts.Add(Outs[i]); } } if (QKeyValue.FindBoolAttribute(this.Attributes, "async") && Outs.Count > 0) { Type returnType = ((!)Outs[0]).ShallowType; if (!returnType.Equals(Type.Int)) { tc.Error(this.tok, "the return from an asynchronous call should be an integer"); return; } } // match actuals with formals List! actualTypeParams; Type.CheckArgumentTypes(Proc.TypeParameters, out actualTypeParams, formalInTypes, actualIns, formalOutTypes, actualOuts, this.tok, "call to " + callee, tc); TypeParameters = SimpleTypeParamInstantiation.From(Proc.TypeParameters, actualTypeParams); } private IDictionary! TypeParamSubstitution() { assume TypeParameters != null; IDictionary! res = new Dictionary (); foreach (TypeVariable! v in TypeParameters.FormalTypeParams) res.Add(v, TypeParameters[v]); return res; } protected override Cmd! ComputeDesugaring() { CmdSeq newBlockBody = new CmdSeq(); Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/(); Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/(); Hashtable /*Variable -> Expr*/ substMapBound = new Hashtable/*Variable -> Expr*/(); VariableSeq! tempVars = new VariableSeq(); // proc P(ins) returns (outs) // requires Pre // modifies frame // ensures Post // // call aouts := P(ains) // ins : formal in parameters of procedure // frame : a list of global variables from the modifies clause // outs : formal out parameters of procedure // ains : actual in arguments passed to call // aouts : actual variables assigned to from call // cins : new variables created just for this call, one per ains // cframe : new variables created just for this call, to keep track of OLD values // couts : new variables created just for this call, one per aouts // WildcardVars : new variables created just for this call, one per null in ains #region Create cins; each one is an incarnation of the corresponding in parameter VariableSeq! cins = new VariableSeq(); VariableSeq wildcardVars = new VariableSeq(); assume this.Proc != null; for (int i = 0; i < this.Proc.InParams.Length; ++i) { Variable! param = (!)this.Proc.InParams[i]; bool isWildcard = this.Ins[i] == null; Type! actualType; if (isWildcard) actualType = param.TypedIdent.Type.Substitute(TypeParamSubstitution()); else // during type checking, we have ensured that the type of the actual // parameter Ins[i] is correct, so we can use it here actualType = (!)((!)Ins[i]).Type; Variable cin = CreateTemporaryVariable(tempVars, param, actualType, TempVarKind.Formal); cins.Add(cin); IdentifierExpr ie = new IdentifierExpr(cin.tok, cin); substMap.Add(param, ie); if (isWildcard) { cin = CreateTemporaryVariable(tempVars, param, actualType, TempVarKind.Bound); wildcardVars.Add(cin); ie = new IdentifierExpr(cin.tok, cin); } substMapBound.Add(param, ie); } #endregion #region call aouts := P(ains) becomes: (open outlining one level to see) #region cins := ains (or havoc cin when ain is null) for (int i = 0, n = this.Ins.Count; i < n; i++) { IdentifierExpr! cin_exp = new IdentifierExpr(((!)cins[i]).tok, (!) cins[i]); if (this.Ins[i] != null) { AssignCmd assign = Cmd.SimpleAssign(Token.NoToken, cin_exp, (!) this.Ins[i]); newBlockBody.Add(assign); } else { IdentifierExprSeq! ies = new IdentifierExprSeq(); ies.Add(cin_exp); HavocCmd havoc = new HavocCmd(Token.NoToken, ies); newBlockBody.Add(havoc); } } #endregion #region assert (exists wildcardVars :: Pre[ins := cins]) Substitution s = Substituter.SubstitutionFromHashtable(substMapBound); bool hasWildcard = (wildcardVars.Length != 0); Expr preConjunction = null; for (int i = 0; i < this.Proc.Requires.Length; i++) { Requires! req = (!) this.Proc.Requires[i]; if (!req.Free) { if (hasWildcard) { Expr pre = Substituter.Apply(s, req.Condition); if (preConjunction == null) { preConjunction = pre; } else { preConjunction = Expr.And(preConjunction, pre); } } else { Requires! reqCopy = (Requires!) req.Clone(); reqCopy.Condition = Substituter.Apply(s, req.Condition); AssertCmd! a = new AssertRequiresCmd(this, reqCopy); a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced; newBlockBody.Add(a); } } } if (hasWildcard) { if (preConjunction == null) { preConjunction = Expr.True; } Expr! expr = new ExistsExpr(tok, wildcardVars, preConjunction); AssertCmd! a = new AssertCmd(tok, expr); a.ErrorDataEnhanced = AssertCmd.GenerateBoundVarMiningStrategy(expr); newBlockBody.Add(a); } #endregion #region assume Pre[ins := cins] with formal paramters if (hasWildcard) { s = Substituter.SubstitutionFromHashtable(substMap); for (int i = 0; i < this.Proc.Requires.Length; i++) { Requires! req = (!) this.Proc.Requires[i]; if (!req.Free) { Requires! reqCopy = (Requires!) req.Clone(); reqCopy.Condition = Substituter.Apply(s, req.Condition); AssumeCmd! a = new AssumeCmd(tok, reqCopy.Condition); newBlockBody.Add(a); } } } #endregion #region cframe := frame (to hold onto frame values in case they are referred to in the postcondition) IdentifierExprSeq havocVarExprs = new IdentifierExprSeq(); foreach (IdentifierExpr! f in this.Proc.Modifies) { assume f.Decl != null; assert f.Type != null; Variable v = CreateTemporaryVariable(tempVars, f.Decl, f.Type, TempVarKind.Old); IdentifierExpr v_exp = new IdentifierExpr(v.tok, v); substMapOld.Add(f.Decl, v_exp); // this assumes no duplicates in this.Proc.Modifies AssignCmd assign = Cmd.SimpleAssign(f.tok, v_exp, f); newBlockBody.Add(assign); // fra if(!havocVarExprs.Has(f)) havocVarExprs.Add(f); } #endregion #region Create couts VariableSeq! couts = new VariableSeq(); for (int i = 0; i < this.Proc.OutParams.Length; ++i) { Variable! param = (!)this.Proc.OutParams[i]; bool isWildcard = this.Outs[i] == null; Type! actualType; if (isWildcard) actualType = param.TypedIdent.Type.Substitute(TypeParamSubstitution()); else // during type checking, we have ensured that the type of the actual // out parameter Outs[i] is correct, so we can use it here actualType = (!)((!)Outs[i]).Type; Variable cout = CreateTemporaryVariable(tempVars, param, actualType, TempVarKind.Formal); couts.Add(cout); IdentifierExpr ie = new IdentifierExpr(cout.tok, cout); substMap.Add(param, ie); if(!havocVarExprs.Has(ie)) havocVarExprs.Add(ie); } // add the where clauses, now that we have the entire substitution map foreach (Variable! param in this.Proc.OutParams) { Expr w = param.TypedIdent.WhereExpr; if (w != null) { IdentifierExpr ie = (IdentifierExpr!)substMap[param]; assert ie.Decl != null; ie.Decl.TypedIdent.WhereExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(substMap), w); } } #endregion #region havoc frame, couts // pass on this's token HavocCmd hc = new HavocCmd(this.tok, havocVarExprs); newBlockBody.Add(hc); #endregion #region assume Post[ins, outs, old(frame) := cins, couts, cframe] Substitution s2 = Substituter.SubstitutionFromHashtable(substMap); Substitution s2old = Substituter.SubstitutionFromHashtable(substMapOld); foreach (Ensures! e in this.Proc.Ensures) { Expr copy = Substituter.ApplyReplacingOldExprs(s2, s2old, e.Condition); AssumeCmd assume = new AssumeCmd(this.tok, copy); newBlockBody.Add(assume); } #endregion #region aouts := couts for (int i = 0, n = this.Outs.Count; i < n; i++) { if (this.Outs[i]!=null) { Variable! param_i = (!) this.Proc.OutParams[i]; Expr! cout_exp = new IdentifierExpr(((!)couts[i]).tok, (!) couts[i]); AssignCmd assign = Cmd.SimpleAssign(param_i.tok, (!) this.Outs[i], cout_exp); newBlockBody.Add(assign); } } #endregion #endregion return new StateCmd(this.tok, tempVars, newBlockBody); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitCallCmd(this); } } public class CallForallCmd : CallCommonality { string! callee; public Procedure Proc; public List! Ins; // the types of the formal in-parameters after instantiating all // type variables whose value could be inferred using the given // actual non-wildcard arguments public TypeSeq InstantiatedTypes; public CallForallCmd(IToken! tok, string! callee, List! ins) { base(tok, null); this.callee = callee; this.Ins = ins; } public CallForallCmd(IToken! tok, string! callee, List! ins, QKeyValue kv) { base(tok, kv); this.callee = callee; this.Ins = ins; } public override void Emit(TokenTextWriter! stream, int level) { stream.Write(this, level, "call "); EmitAttributes(stream, Attributes); stream.Write("forall "); stream.Write(TokenTextWriter.SanitizeIdentifier(callee)); stream.Write("("); string sep = ""; foreach (Expr arg in Ins) { stream.Write(sep); sep = ", "; if (arg == null) { stream.Write("*"); } else { arg.Emit(stream); } } stream.WriteLine(");"); base.Emit(stream, level); } public override void Resolve(ResolutionContext! rc) { if (Proc != null) { // already resolved return; } ResolveAttributes(Attributes, rc); Proc = rc.LookUpProcedure(callee) as Procedure; if (Proc == null) { rc.Error(this, "call to undeclared procedure: {0}", callee); } foreach (Expr e in Ins) { if (e != null) { e.Resolve(rc); } } } public override void AddAssignedVariables(VariableSeq! vars) { } public override void Typecheck(TypecheckingContext! tc) { TypecheckAttributes(Attributes, tc); // typecheck in-parameters foreach (Expr e in Ins) { if (e != null) { e.Typecheck(tc); } } if (this.Proc == null) { // called procedure didn't resolve, so bug out return; } // match actuals with formals if (Ins.Count != Proc.InParams.Length) { tc.Error(this, "wrong number of in-parameters in call: {0}", callee); } else { // determine the lists of formal and actual arguments that need // to be matched (stars are left out) TypeSeq! formalTypes = new TypeSeq (); ExprSeq! actualArgs = new ExprSeq (); for (int i = 0; i < Ins.Count; i++) if (Ins[i] != null) { formalTypes.Add(((!)Proc.InParams[i]).TypedIdent.Type); actualArgs.Add(Ins[i]); } IDictionary! subst = Type.MatchArgumentTypes(Proc.TypeParameters, formalTypes, actualArgs, null, null, "call forall to " + callee, tc); InstantiatedTypes = new TypeSeq (); foreach (Variable! var in Proc.InParams) { InstantiatedTypes.Add(var.TypedIdent.Type.Substitute(subst)); } } // if (Proc.OutParams.Length != 0) // { // tc.Error(this, "call forall is allowed only on procedures with no out-parameters: {0}", callee); // } if (Proc.Modifies.Length != 0) { tc.Error(this, "call forall is allowed only on procedures with no modifies clause: {0}", callee); } } protected override Cmd! ComputeDesugaring() { CmdSeq newBlockBody = new CmdSeq(); Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/(); VariableSeq! tempVars = new VariableSeq(); // proc P(ins) returns () // requires Pre; // modifies ; // ensures Post; // // call forall P(ains); // ins : formal in-parameters of procedure // ains : actual in-arguments passed to call // cins : new variables created just for this call, one per ains // wildcardVars : the bound variables to be wrapped up in a quantification #region Create cins; each one is an incarnation of the corresponding in parameter VariableSeq! cins = new VariableSeq(); VariableSeq wildcardVars = new VariableSeq(); assume this.Proc != null; for (int i = 0, n = this.Proc.InParams.Length; i < n; i++) { Variable param = (!)this.Proc.InParams[i]; Type! paramType = ((!)this.InstantiatedTypes)[i]; // might contain type variables bool isWildcard = this.Ins[i] == null; Variable cin = CreateTemporaryVariable(tempVars, param, paramType, isWildcard ? TempVarKind.Bound : TempVarKind.Formal); if (isWildcard) { cins.Add(null); wildcardVars.Add(cin); } else { cins.Add(cin); } IdentifierExpr ie = new IdentifierExpr(cin.tok, cin); substMap.Add(param, ie); } #endregion #region call forall P(ains) becomes: (open outlining one level to see) #region cins := ains for (int i = 0, n = this.Ins.Count; i < n; i++) { if (this.Ins[i] != null) { IdentifierExpr! cin_exp = new IdentifierExpr(((!)cins[i]).tok, (!) cins[i]); AssignCmd assign = Cmd.SimpleAssign(Token.NoToken, cin_exp, (!) this.Ins[i]); newBlockBody.Add(assign); } } #endregion #region assert Pre[ins := cins] Substitution s = Substituter.SubstitutionFromHashtable(substMap); Expr preConjunction = null; for (int i = 0; i < this.Proc.Requires.Length; i++) { Requires! req = (!) this.Proc.Requires[i]; if (!req.Free) { Expr pre = Substituter.Apply(s, req.Condition); if (preConjunction == null) { preConjunction = pre; } else { preConjunction = Expr.And(preConjunction, pre); } } } if (preConjunction == null) { preConjunction = Expr.True; } #endregion #region Create couts VariableSeq! couts = new VariableSeq(); foreach ( Variable! param in this.Proc.OutParams ) { Variable cout = CreateTemporaryVariable(tempVars, param, param.TypedIdent.Type, TempVarKind.Bound); couts.Add(cout); IdentifierExpr ie = new IdentifierExpr(cout.tok, cout); substMap.Add(param, ie); } // add the where clauses, now that we have the entire substitution map foreach (Variable! param in this.Proc.OutParams) { Expr w = param.TypedIdent.WhereExpr; if (w != null) { IdentifierExpr ie = (IdentifierExpr!)substMap[param]; assert ie.Decl != null; ie.Decl.TypedIdent.WhereExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(substMap), w); } } #endregion #region assume Post[ins := cins] s = Substituter.SubstitutionFromHashtable(substMap); Expr postConjunction = null; foreach (Ensures! e in this.Proc.Ensures) { Expr post = Substituter.Apply(s, e.Condition); if (postConjunction == null) { postConjunction = post; } else { postConjunction = Expr.And(postConjunction, post); } } if (postConjunction == null) { postConjunction = Expr.True; } #endregion #region assume (forall wildcardVars :: Pre ==> Post); Expr body = postConjunction; if (couts.Length > 0) { body = new ExistsExpr(tok, couts, body); } body = Expr.Imp(preConjunction, body); if (wildcardVars.Length != 0) { TypeVariableSeq! typeParams = Type.FreeVariablesIn((!)InstantiatedTypes); body = new ForallExpr(tok, typeParams, wildcardVars, body); } newBlockBody.Add(new AssumeCmd(tok, body)); #endregion #endregion return new StateCmd(this.tok, tempVars, newBlockBody); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitCallForallCmd(this); } } public abstract class PredicateCmd : Cmd { public /*readonly--except in StandardVisitor*/ Expr! Expr; public PredicateCmd(IToken! tok, Expr! expr) : base(tok) { Expr = expr; } public override void Resolve(ResolutionContext! rc) { Expr.Resolve(rc); } public override void AddAssignedVariables(VariableSeq! vars) { } } public abstract class MiningStrategy { // abstract class to bind all MiningStrategys, i.e., all types of enhanced error data // types together } public class ListOfMiningStrategies : MiningStrategy { public List! msList; public ListOfMiningStrategies (List! l) { this.msList = l; } } public class EEDTemplate : MiningStrategy { public string! reason; public List! exprList; public EEDTemplate (string! reason, List! exprList) { this.reason = reason; this.exprList = exprList; } } public class AssertCmd : PredicateCmd, IPotentialErrorNode { public Expr OrigExpr; public Hashtable /*Variable -> Expr*/ IncarnationMap; // TODO: convert to use generics private object errorData; public object ErrorData { get { return errorData; } set { errorData = value; } } public string ErrorMessage { get { return QKeyValue.FindStringAttribute(Attributes, "msg"); } } public QKeyValue Attributes; private MiningStrategy errorDataEnhanced; public MiningStrategy ErrorDataEnhanced { get { return errorDataEnhanced; } set { errorDataEnhanced = value; } } public AssertCmd(IToken! tok, Expr! expr) : base(tok, expr) { errorDataEnhanced = GenerateBoundVarMiningStrategy(expr); } public AssertCmd(IToken! tok, Expr! expr, QKeyValue kv) : base(tok, expr) { errorDataEnhanced = GenerateBoundVarMiningStrategy(expr); Attributes = kv; } public override void Emit(TokenTextWriter! stream, int level) { stream.Write(this, level, "assert "); EmitAttributes(stream, Attributes); this.Expr.Emit(stream); stream.WriteLine(";"); } public override void Resolve(ResolutionContext! rc) { ResolveAttributes(Attributes, rc); base.Resolve(rc); } public override void Typecheck(TypecheckingContext! tc) { TypecheckAttributes(Attributes, tc); Expr.Typecheck(tc); assert Expr.Type != null; // follows from Expr.Typecheck postcondition if (!Expr.Type.Unify(Type.Bool)) { tc.Error(this, "an asserted expression must be of type bool (got: {0})", Expr.Type); } } public static MiningStrategy GenerateBoundVarMiningStrategy (Expr! expr) { List l = new List(); if (expr != null) { l = GenerateBoundVarListForMining(expr, l); } return new ListOfMiningStrategies(l); } public static List! GenerateBoundVarListForMining (Expr! expr, List! l) { // go through the origExpr and identify all bound variables in the AST. if (expr is LiteralExpr || expr is IdentifierExpr) { //end recursion } else if (expr is NAryExpr) { NAryExpr e = (NAryExpr)expr; foreach (Expr! arg in e.Args) { l = GenerateBoundVarListForMining(arg, l); } } else if (expr is OldExpr) { OldExpr e = (OldExpr)expr; l = GenerateBoundVarListForMining(e.Expr, l); } else if (expr is QuantifierExpr) { QuantifierExpr qe = (QuantifierExpr) expr; VariableSeq vs = qe.Dummies; foreach (Variable! x in vs) { string name = x.Name; if (name.StartsWith("^")) { name = name.Substring(1); List exprList = new List(); exprList.Add(new IdentifierExpr(Token.NoToken, x.ToString(), x.TypedIdent.Type)); MiningStrategy eed = new EEDTemplate("The bound variable " + name + " has the value {0}.", exprList); l.Add(eed); } } l = GenerateBoundVarListForMining(qe.Body, l); } return l; } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitAssertCmd(this); } } // An AssertCmd that is a loop invariant check before the loop iteration starts public class LoopInitAssertCmd : AssertCmd { public LoopInitAssertCmd(IToken! tok, Expr! expr) : base(tok, expr) { } } // An AssertCmd that is a loop invariant check to maintain the invariant after iteration public class LoopInvMaintainedAssertCmd : AssertCmd { public LoopInvMaintainedAssertCmd(IToken! tok, Expr! expr) : base(tok, expr) { } } /// /// An AssertCmd that is introduced in translation from the requires on a call. /// public class AssertRequiresCmd : AssertCmd { public CallCmd! Call; public Requires! Requires; public AssertRequiresCmd(CallCmd! call, Requires! @requires) : base(call.tok, @requires.Condition) { this.Call = call; this.Requires = @requires; // base(call.tok, @requires.Condition); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitAssertRequiresCmd(this); } } /// /// An AssertCmd that is introduced in translation from an ensures /// declaration. /// public class AssertEnsuresCmd : AssertCmd { public Ensures! Ensures; public AssertEnsuresCmd(Ensures! ens) : base(ens.tok, ens.Condition) { this.Ensures = ens; // base(ens.tok, ens.Condition); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitAssertEnsuresCmd(this); } } public class AssumeCmd : PredicateCmd { public AssumeCmd(IToken! tok, Expr! expr) : base(tok, expr) { //Debug.Assert(expr != null); } public override void Emit(TokenTextWriter! stream, int level) { stream.Write(this, level, "assume "); this.Expr.Emit(stream); stream.WriteLine(";"); } public override void Typecheck(TypecheckingContext! tc) { Expr.Typecheck(tc); assert Expr.Type != null; // follows from Expr.Typecheck postcondition if (!Expr.Type.Unify(Type.Bool)) { tc.Error(this, "an assumed expression must be of type bool (got: {0})", Expr.Type); } } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitAssumeCmd(this); } } public class ReturnExprCmd : ReturnCmd { public Expr! Expr; public ReturnExprCmd(IToken! tok, Expr! expr) : base(tok) { Expr = expr; } public override void Emit(TokenTextWriter! stream, int level) { stream.Write(this, level, "return "); this.Expr.Emit(stream); stream.WriteLine(";"); } public override void Typecheck(TypecheckingContext! tc) { Expr.Typecheck(tc); assert Expr.Type != null; // follows from Expr.Typecheck postcondition if (!Expr.Type.Unify(Type.Bool)) { tc.Error(this, "a return expression must be of type bool (got: {0})", Expr.Type); } } public override void Resolve(ResolutionContext! rc) { Expr.Resolve(rc); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitReturnExprCmd(this); } } public class HavocCmd : Cmd { public IdentifierExprSeq! Vars; public HavocCmd(IToken! tok, IdentifierExprSeq! vars) : base(tok) { Vars = vars; } public override void Emit(TokenTextWriter! stream, int level) { stream.Write(this, level, "havoc "); Vars.Emit(stream, true); stream.WriteLine(";"); } public override void Resolve(ResolutionContext! rc) { foreach (IdentifierExpr! ide in Vars) { ide.Resolve(rc); } } public override void AddAssignedVariables(VariableSeq! vars) { foreach (IdentifierExpr! e in this.Vars) { vars.Add(e.Decl); } } public override void Typecheck(TypecheckingContext! tc) { this.CheckAssignments(tc); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitHavocCmd(this); } } //--------------------------------------------------------------------- // Transfer commands public abstract class TransferCmd : Absy { internal TransferCmd(IToken! tok) : base(tok) { } public abstract void Emit(TokenTextWriter! stream, int level); public override void Typecheck(TypecheckingContext! tc) { // nothing to typecheck } } public class ReturnCmd : TransferCmd { public ReturnCmd(IToken! tok) : base(tok) { } public override void Emit(TokenTextWriter! stream, int level) { stream.WriteLine(this, level, "return;"); } public override void Resolve(ResolutionContext! rc) { // nothing to resolve } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitReturnCmd(this); } } public class GotoCmd : TransferCmd { [Rep] public StringSeq labelNames; [Rep] public BlockSeq labelTargets; invariant labelNames != null && labelTargets != null ==> labelNames.Length == labelTargets.Length; [NotDelayed] public GotoCmd(IToken! tok, StringSeq! labelSeq) : base (tok) { this.labelNames = labelSeq; } public GotoCmd(IToken! tok, StringSeq! labelSeq, BlockSeq! blockSeq) : base (tok) { Debug.Assert(labelSeq.Length == blockSeq.Length); for (int i=0; i blockSeq[i].Label != null; StringSeq labelSeq = new StringSeq(); for (int i=0; i 0 || labelTargets.Length == labelNames.Length); } public override Absy! StdDispatch(StandardVisitor! visitor) { return visitor.VisitGotoCmd(this); } } }