diff --git a/Source/Core/Visitors/ReadOnlyVisitor.cs b/Source/Core/Visitors/ReadOnlyVisitor.cs
new file mode 100644
index 000000000..a215fec8a
--- /dev/null
+++ b/Source/Core/Visitors/ReadOnlyVisitor.cs
@@ -0,0 +1,711 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace Microsoft.Boogie;
+
+///
+/// A ReadOnlyVisitor visits all the nodes of a given Absy. The visitor may collect information from
+/// the nodes, may change fields contained in the data structure, but may not replace any nodes in the
+/// data structure. To enforce this, all Visit...(node) methods have a postcondition that says that
+/// the return value is equal to the given "node".
+///
+public abstract class ReadOnlyVisitor : StandardVisitor
+{
+ public ReadOnlyVisitor()
+ {
+ }
+
+ public ReadOnlyVisitor(Visitor callingVisitor)
+ {
+ this.callingVisitor = callingVisitor;
+ }
+
+ public override Absy Visit(Absy node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node.StdDispatch(this);
+ }
+
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+
+ public override Cmd VisitAssignCmd(AssignCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ for (int i = 0; i < node.Lhss.Count; ++i)
+ {
+ this.Visit(node.Lhss[i]);
+ this.VisitExpr(node.Rhss[i]);
+ }
+ return node;
+ }
+
+ public override Cmd VisitUnpackCmd(UnpackCmd node)
+ {
+ this.VisitExpr(node.Lhs);
+ this.VisitExpr(node.Rhs);
+ return node;
+ }
+
+ public override Cmd VisitAssumeCmd(AssumeCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+
+ public override AtomicRE VisitAtomicRE(AtomicRE node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitBlock(node.b);
+ return node;
+ }
+
+ public override Axiom VisitAxiom(Axiom node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+
+ public override Type VisitBasicType(BasicType node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return this.VisitType(node);
+ }
+
+ public override Expr VisitBvConcatExpr(BvConcatExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExpr(node.E0);
+ this.VisitExpr(node.E1);
+ return node;
+ }
+
+ public override Type VisitBvType(BvType node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return this.VisitType(node);
+ }
+
+ public override Type VisitBvTypeProxy(BvTypeProxy node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ // if the type proxy is instantiated with some more
+ // specific type, we visit the instantiation
+ if (node.ProxyFor != null)
+ {
+ this.Visit(node.ProxyFor);
+ }
+
+ return this.VisitType(node);
+ }
+
+ public override Block VisitBlock(Block node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitCmdSeq(node.Cmds);
+ this.Visit(cce.NonNull(node.TransferCmd));
+ return node;
+ }
+
+ public override Expr VisitCodeExpr(CodeExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitVariableSeq(node.LocVars);
+ this.VisitBlockList(node.Blocks);
+ return node;
+ }
+
+ public override List VisitBlockSeq(List blockSeq)
+ {
+ Contract.Ensures(Contract.Result>() == blockSeq);
+ for (int i = 0, n = blockSeq.Count; i < n; i++)
+ {
+ this.VisitBlock(cce.NonNull(blockSeq[i]));
+ }
+
+ return blockSeq;
+ }
+
+ public override List /*!*/ VisitBlockList(List /*!*/ blocks)
+ {
+ Contract.Ensures(Contract.Result>() == blocks);
+ for (int i = 0, n = blocks.Count; i < n; i++)
+ {
+ this.VisitBlock(blocks[i]);
+ }
+
+ return blocks;
+ }
+
+ public override BoundVariable VisitBoundVariable(BoundVariable node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return (BoundVariable) this.VisitVariable(node);
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ for (int i = 0; i < node.Ins.Count; ++i)
+ {
+ if (node.Ins[i] != null)
+ {
+ this.VisitExpr(node.Ins[i]);
+ }
+ }
+
+ for (int i = 0; i < node.Outs.Count; ++i)
+ {
+ if (node.Outs[i] != null)
+ {
+ this.VisitIdentifierExpr(node.Outs[i]);
+ }
+ }
+
+ return node;
+ }
+
+ public override Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ for (int i = 0; i < node.CallCmds.Count; i++)
+ {
+ if (node.CallCmds[i] != null)
+ {
+ this.VisitCallCmd(node.CallCmds[i]);
+ }
+ }
+
+ return node;
+ }
+
+ public override List VisitCmdSeq(List cmdSeq)
+ {
+ Contract.Ensures(Contract.Result>() == cmdSeq);
+ for (int i = 0, n = cmdSeq.Count; i < n; i++)
+ {
+ this.Visit(cce.NonNull(
+ cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor
+ }
+
+ return cmdSeq;
+ }
+
+ public override Choice VisitChoice(Choice node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitRESeq(node.rs);
+ return node;
+ }
+
+ public override Cmd VisitCommentCmd(CommentCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node;
+ }
+
+ public override Constant VisitConstant(Constant node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node;
+ }
+
+ public override CtorType VisitCtorType(CtorType node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ {
+ this.Visit(node.Arguments[i]);
+ }
+
+ return node;
+ }
+
+ public override Declaration VisitDeclaration(Declaration node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node;
+ }
+
+ public override List /*!*/ VisitDeclarationList(List /*!*/ declarationList)
+ {
+ Contract.Ensures(Contract.Result>() == declarationList);
+ for (int i = 0, n = declarationList.Count; i < n; i++)
+ {
+ this.Visit(declarationList[i]);
+ }
+
+ return declarationList;
+ }
+
+ public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitVariableSeq(node.InParams);
+ this.VisitVariableSeq(node.OutParams);
+ return node;
+ }
+
+ public override Expr VisitExistsExpr(ExistsExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return (ExistsExpr) this.VisitQuantifierExpr(node);
+ }
+
+ public override Expr VisitBvExtractExpr(BvExtractExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExpr(node.Bitvector);
+ return node;
+ }
+
+ public override Expr VisitExpr(Expr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return (Expr) this.Visit(node);
+ }
+
+ public override IList VisitExprSeq(IList exprSeq)
+ {
+ Contract.Ensures(Contract.Result>() == exprSeq);
+ for (int i = 0, n = exprSeq.Count; i < n; i++)
+ {
+ this.VisitExpr(cce.NonNull(exprSeq[i]));
+ }
+
+ return exprSeq;
+ }
+
+ public override Requires VisitRequires(Requires requires)
+ {
+ Contract.Ensures(Contract.Result() == requires);
+ this.VisitExpr(requires.Condition);
+ return requires;
+ }
+
+ public override List VisitRequiresSeq(List requiresSeq)
+ {
+ Contract.Ensures(Contract.Result>() == requiresSeq);
+ for (int i = 0, n = requiresSeq.Count; i < n; i++)
+ {
+ this.VisitRequires(requiresSeq[i]);
+ }
+
+ return requiresSeq;
+ }
+
+ public override Ensures VisitEnsures(Ensures ensures)
+ {
+ Contract.Ensures(Contract.Result() == ensures);
+ this.VisitExpr(ensures.Condition);
+ return ensures;
+ }
+
+ public override List VisitEnsuresSeq(List ensuresSeq)
+ {
+ Contract.Ensures(Contract.Result>() == ensuresSeq);
+ for (int i = 0, n = ensuresSeq.Count; i < n; i++)
+ {
+ this.VisitEnsures(ensuresSeq[i]);
+ }
+
+ return ensuresSeq;
+ }
+
+ public override Expr VisitForallExpr(ForallExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return (ForallExpr) this.VisitQuantifierExpr(node);
+ }
+
+ public override Expr VisitLambdaExpr(LambdaExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return this.VisitBinderExpr(node);
+ }
+
+ public override Expr VisitLetExpr(LetExpr node)
+ {
+ this.VisitExprSeq(node.Rhss);
+ this.VisitVariableSeq(node.Dummies);
+ this.VisitExpr(node.Body);
+ return node;
+ }
+
+ public override Formal VisitFormal(Formal node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node;
+ }
+
+ public override Function VisitFunction(Function node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ node = (Function) this.VisitDeclWithFormals(node);
+ if (node.Body != null)
+ {
+ Contract.Assert(node.DefinitionBody == null);
+ this.VisitExpr(node.Body);
+ }
+ else if (node.DefinitionBody != null)
+ {
+ this.VisitExpr(node.DefinitionBody);
+ }
+
+ return node;
+ }
+
+ public override GlobalVariable VisitGlobalVariable(GlobalVariable node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return (GlobalVariable) this.VisitVariable(node);
+ }
+
+ public override GotoCmd VisitGotoCmd(GotoCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ // do not visit the labelTargets, or control-flow loops will lead to a looping visitor
+ return node;
+ }
+
+ public override Cmd VisitHavocCmd(HavocCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitIdentifierExprSeq(node.Vars);
+ return node;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ if (node.Decl != null)
+ {
+ this.VisitVariable(node.Decl);
+ }
+
+ return node;
+ }
+
+ public override List VisitIdentifierExprSeq(List identifierExprSeq)
+ {
+ Contract.Ensures(Contract.Result>() == identifierExprSeq);
+ for (int i = 0, n = identifierExprSeq.Count; i < n; i++)
+ {
+ this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));
+ }
+
+ return identifierExprSeq;
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitVariableSeq(node.LocVars);
+ this.VisitBlockList(node.Blocks);
+ node.Proc = (Procedure)node.Proc.StdDispatch(this);
+ return (Implementation) this.VisitDeclWithFormals(node); // do this first or last?
+ }
+
+ public override Expr VisitLiteralExpr(LiteralExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node;
+ }
+
+ public override LocalVariable VisitLocalVariable(LocalVariable node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node;
+ }
+
+ public override AssignLhs VisitMapAssignLhs(MapAssignLhs node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.Visit(node.Map);
+ for (int i = 0; i < node.Indexes.Count; ++i)
+ {
+ this.VisitExpr(node.Indexes[i]);
+ }
+
+ return node;
+ }
+
+ public override Type VisitMapType(MapType node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ // not doing anything about the bound variables ... maybe
+ // these should be visited as well ...
+ //
+ // NOTE: when overriding this method, you have to make sure that
+ // the bound variables of the map type are updated correctly
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ {
+ this.Visit(node.Arguments[i]);
+ }
+
+ this.Visit(node.Result);
+ return node;
+ }
+
+ public override Type VisitMapTypeProxy(MapTypeProxy node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ // if the type proxy is instantiated with some more
+ // specific type, we visit the instantiation
+ if (node.ProxyFor != null)
+ {
+ this.Visit(node.ProxyFor);
+ }
+
+ return this.VisitType(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExprSeq(node.Args);
+ return node;
+ }
+
+ public override Expr VisitOldExpr(OldExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitEnsuresSeq(node.Ensures);
+ this.VisitVariableSeq(node.InParams);
+ this.VisitIdentifierExprSeq(node.Modifies);
+ this.VisitVariableSeq(node.OutParams);
+ this.VisitRequiresSeq(node.Requires);
+ return node;
+ }
+
+ public override Program VisitProgram(Program node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitDeclarationList(node.TopLevelDeclarations.ToList());
+ return node;
+ }
+
+ public override QKeyValue VisitQKeyValue(QKeyValue node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ for (int i = 0, n = node.Params.Count; i < n; i++)
+ {
+ var e = node.Params[i] as Expr;
+ if (e != null)
+ {
+ this.Visit(e);
+ }
+ }
+
+ if (node.Next != null)
+ {
+ this.Visit(node.Next);
+ }
+
+ return node;
+ }
+
+ public override Expr VisitBinderExpr(BinderExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExpr(node.Body);
+ this.VisitVariableSeq(node.Dummies);
+ // this.VisitType(node.Type);
+ return node;
+ }
+
+ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitBinderExpr(node);
+ if (node.Triggers != null)
+ {
+ this.VisitTrigger(node.Triggers);
+ }
+
+ return node;
+ }
+
+ public override Cmd VisitRE(RE node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return (Cmd) this.Visit(node); // Call general visit so subtypes get visited by their particular visitor
+ }
+
+ public override List VisitRESeq(List reSeq)
+ {
+ Contract.Ensures(Contract.Result>() == reSeq);
+ for (int i = 0, n = reSeq.Count; i < n; i++)
+ {
+ this.VisitRE(cce.NonNull(reSeq[i]));
+ }
+
+ return reSeq;
+ }
+
+ public override ReturnCmd VisitReturnCmd(ReturnCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return (ReturnCmd) this.VisitTransferCmd(node);
+ }
+
+ public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+
+ public override Sequential VisitSequential(Sequential node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitRE(node.first);
+ this.VisitRE(node.second);
+ return node;
+ }
+
+ public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitIdentifierExpr(node.AssignedVariable);
+ return node;
+ }
+
+ public override Cmd VisitStateCmd(StateCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitVariableSeq(node.Locals);
+ this.VisitCmdSeq(node.Cmds);
+ return node;
+ }
+
+ public override TransferCmd VisitTransferCmd(TransferCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node;
+ }
+
+ public override Trigger VisitTrigger(Trigger node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ Trigger origNext = node.Next;
+ if (origNext != null)
+ {
+ this.VisitTrigger(origNext);
+ }
+
+ this.VisitExprSeq(node.Tr.ToList());
+ return node;
+ }
+
+ // called by default for all nullary type constructors and type variables
+ public override Type VisitType(Type node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return node;
+ }
+
+ public override TypedIdent VisitTypedIdent(TypedIdent node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.Visit(node.Type);
+ return node;
+ }
+
+ public override Declaration VisitTypeCtorDecl(TypeCtorDecl node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return this.VisitDeclaration(node);
+ }
+
+ public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ node.ExpandedType = cce.NonNull((Type /*!*/) this.Visit(node.ExpandedType));
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ {
+ this.Visit(node.Arguments[i]);
+ }
+
+ return node;
+ }
+
+ public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return this.VisitDeclaration(node);
+ }
+
+ public override Type VisitTypeVariable(TypeVariable node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return this.VisitType(node);
+ }
+
+ public override Type VisitTypeProxy(TypeProxy node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ // if the type proxy is instantiated with some more
+ // specific type, we visit the instantiation
+ if (node.ProxyFor != null)
+ {
+ this.Visit(node.ProxyFor);
+ }
+
+ return this.VisitType(node);
+ }
+
+ public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ return this.VisitType(node);
+ }
+
+ public override Variable VisitVariable(Variable node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitTypedIdent(node.TypedIdent);
+ return node;
+ }
+
+ public override List VisitVariableSeq(List variableSeq)
+ {
+ Contract.Ensures(Contract.Result>() == variableSeq);
+ for (int i = 0, n = variableSeq.Count; i < n; i++)
+ {
+ this.VisitVariable(cce.NonNull(variableSeq[i]));
+ }
+
+ return variableSeq;
+ }
+
+ public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitEnsures(node.Ensures);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+
+ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node)
+ {
+ Contract.Ensures(Contract.Result() == node);
+ this.VisitRequires(node.Requires);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+}
\ No newline at end of file
diff --git a/Source/Core/Visitors/StandardVisitor.cs b/Source/Core/Visitors/StandardVisitor.cs
new file mode 100644
index 000000000..1ce361ebb
--- /dev/null
+++ b/Source/Core/Visitors/StandardVisitor.cs
@@ -0,0 +1,947 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace Microsoft.Boogie
+{
+ ///
+ /// Walks an IR, mutating it into a new form. (For a subclass that does not mutate the IR, see ReadOnlyVisitor.)
+ ///
+ public abstract class StandardVisitor : Visitor
+ {
+ public Visitor callingVisitor;
+
+ public StandardVisitor()
+ {
+ }
+
+ public StandardVisitor(Visitor callingVisitor)
+ {
+ this.callingVisitor = callingVisitor;
+ }
+
+ public override Absy Visit(Absy node)
+ {
+ return node.StdDispatch(this);
+ }
+
+ public virtual Cmd VisitAssertCmd(AssertCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Expr = this.VisitExpr(node.Expr);
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual Cmd VisitAssignCmd(AssignCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ for (int i = 0; i < node.Lhss.Count; ++i)
+ {
+ node.SetLhs(i, cce.NonNull((AssignLhs) this.Visit(node.Lhss[i])));
+ node.SetRhs(i, cce.NonNull((Expr /*!*/) this.VisitExpr(node.Rhss[i])));
+ }
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual Cmd VisitUnpackCmd(UnpackCmd node)
+ {
+ node.Lhs = (NAryExpr)this.Visit(node.Lhs);
+ node.Rhs = (Expr)this.Visit(node.Rhs);
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual Cmd VisitAssumeCmd(AssumeCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Expr = this.VisitExpr(node.Expr);
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual AtomicRE VisitAtomicRE(AtomicRE node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.b = this.VisitBlock(node.b);
+ return node;
+ }
+
+ public virtual Axiom VisitAxiom(Axiom node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Expr = this.VisitExpr(node.Expr);
+ return node;
+ }
+
+ public virtual Type VisitBasicType(BasicType node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return this.VisitType(node);
+ }
+
+ public virtual Type VisitFloatType(FloatType node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return this.VisitType(node);
+ }
+
+ public virtual Expr VisitBvConcatExpr(BvConcatExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.E0 = this.VisitExpr(node.E0);
+ node.E1 = this.VisitExpr(node.E1);
+ return node;
+ }
+
+ public virtual Type VisitBvType(BvType node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return this.VisitType(node);
+ }
+
+ public virtual Type VisitBvTypeProxy(BvTypeProxy node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ // if the type proxy is instantiated with some more
+ // specific type, we visit the instantiation
+ if (node.ProxyFor != null)
+ {
+ return (Type) this.Visit(node.ProxyFor);
+ }
+
+ return this.VisitType(node);
+ }
+
+ public virtual Block VisitBlock(Block node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Cmds = this.VisitCmdSeq(node.Cmds);
+ node.TransferCmd = (TransferCmd) this.Visit(cce.NonNull(node.TransferCmd));
+ return node;
+ }
+
+ public virtual Expr VisitCodeExpr(CodeExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.LocVars = this.VisitVariableSeq(node.LocVars);
+ node.Blocks = this.VisitBlockList(node.Blocks);
+ return node;
+ }
+
+ public virtual List VisitBlockSeq(List blockSeq)
+ {
+ Contract.Requires(blockSeq != null);
+ Contract.Ensures(Contract.Result>() != null);
+ lock (blockSeq)
+ {
+ for (int i = 0, n = blockSeq.Count; i < n; i++)
+ {
+ blockSeq[i] = this.VisitBlock(cce.NonNull(blockSeq[i]));
+ }
+ }
+
+ return blockSeq;
+ }
+
+ public virtual List /*!*/ VisitBlockList(List /*!*/ blocks)
+ {
+ Contract.Requires(blocks != null);
+ Contract.Ensures(Contract.Result>() != null);
+ for (int i = 0, n = blocks.Count; i < n; i++)
+ {
+ blocks[i] = this.VisitBlock(blocks[i]);
+ }
+
+ return blocks;
+ }
+
+ public virtual BoundVariable VisitBoundVariable(BoundVariable node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node = (BoundVariable) this.VisitVariable(node);
+ return node;
+ }
+
+ public virtual Cmd VisitCallCmd(CallCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ for (int i = 0; i < node.Ins.Count; ++i)
+ {
+ if (node.Ins[i] != null)
+ {
+ node.Ins[i] = this.VisitExpr(cce.NonNull(node.Ins[i]));
+ }
+ }
+
+ for (int i = 0; i < node.Outs.Count; ++i)
+ {
+ if (node.Outs[i] != null)
+ {
+ node.Outs[i] = (IdentifierExpr) this.VisitIdentifierExpr(cce.NonNull(node.Outs[i]));
+ }
+ }
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual List VisitCallCmdSeq(List callCmds)
+ {
+ for (int i = 0; i < callCmds.Count; i++)
+ {
+ callCmds[i] = (CallCmd)VisitCallCmd(callCmds[i]);
+ }
+ return callCmds;
+ }
+
+ public virtual Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ for (int i = 0; i < node.CallCmds.Count; i++)
+ {
+ if (node.CallCmds[i] != null)
+ {
+ node.CallCmds[i] = (CallCmd) this.VisitCallCmd(node.CallCmds[i]);
+ }
+ }
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual List VisitCmdSeq(List cmdSeq)
+ {
+ Contract.Requires(cmdSeq != null);
+ Contract.Ensures(Contract.Result>() != null);
+ lock (cmdSeq)
+ {
+ for (int i = 0, n = cmdSeq.Count; i < n; i++)
+ {
+ cmdSeq[i] = (Cmd) this.Visit(
+ cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor
+ }
+ }
+
+ return cmdSeq;
+ }
+
+ public virtual Choice VisitChoice(Choice node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.rs = this.VisitRESeq(node.rs);
+ return node;
+ }
+
+ public virtual Cmd VisitCommentCmd(CommentCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return node;
+ }
+
+ public virtual Constant VisitConstant(Constant node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return node;
+ }
+
+ public virtual CtorType VisitCtorType(CtorType node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ lock (node)
+ {
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ {
+ node.Arguments[i] = cce.NonNull((Type /*!*/) this.Visit(node.Arguments[i]));
+ }
+ }
+
+ return node;
+ }
+
+ public virtual Declaration VisitDeclaration(Declaration node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return node;
+ }
+
+ public virtual List /*!*/ VisitDeclarationList(List /*!*/ declarationList)
+ {
+ Contract.Requires(declarationList != null);
+ Contract.Ensures(Contract.Result>() != null);
+ for (int i = 0, n = declarationList.Count; i < n; i++)
+ {
+ declarationList[i] = cce.NonNull((Declaration /*!*/) this.Visit(declarationList[i]));
+ }
+
+ return declarationList;
+ }
+
+ public virtual DeclWithFormals VisitDeclWithFormals(DeclWithFormals node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.InParams = this.VisitVariableSeq(node.InParams);
+ node.OutParams = this.VisitVariableSeq(node.OutParams);
+ return node;
+ }
+
+ public virtual Expr VisitExistsExpr(ExistsExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node = (ExistsExpr) this.VisitQuantifierExpr(node);
+ return node;
+ }
+
+ public virtual Expr VisitBvExtractExpr(BvExtractExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Bitvector = this.VisitExpr(node.Bitvector);
+ return node;
+ }
+
+ public virtual Expr VisitExpr(Expr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ Expr e = (Expr) this.Visit(node);
+ return e;
+ }
+
+ public override IList VisitExprSeq(IList exprSeq)
+ {
+ //Contract.Requires(exprSeq != null);
+ Contract.Ensures(Contract.Result>() != null);
+ for (int i = 0, n = exprSeq.Count; i < n; i++)
+ {
+ exprSeq[i] = this.VisitExpr(cce.NonNull(exprSeq[i]));
+ }
+
+ return exprSeq;
+ }
+
+ public virtual Requires VisitRequires(Requires @requires)
+ {
+ Contract.Requires(@requires != null);
+ Contract.Ensures(Contract.Result() != null);
+ @requires.Condition = this.VisitExpr(@requires.Condition);
+ return @requires;
+ }
+
+ public virtual List VisitRequiresSeq(List requiresSeq)
+ {
+ Contract.Requires(requiresSeq != null);
+ Contract.Ensures(Contract.Result>() != null);
+ for (int i = 0, n = requiresSeq.Count; i < n; i++)
+ {
+ requiresSeq[i] = this.VisitRequires(requiresSeq[i]);
+ }
+
+ return requiresSeq;
+ }
+
+ public virtual Ensures VisitEnsures(Ensures @ensures)
+ {
+ Contract.Requires(@ensures != null);
+ Contract.Ensures(Contract.Result() != null);
+ @ensures.Condition = this.VisitExpr(@ensures.Condition);
+ return @ensures;
+ }
+
+ public virtual List VisitEnsuresSeq(List ensuresSeq)
+ {
+ Contract.Requires(ensuresSeq != null);
+ Contract.Ensures(Contract.Result>() != null);
+ for (int i = 0, n = ensuresSeq.Count; i < n; i++)
+ {
+ ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);
+ }
+
+ return ensuresSeq;
+ }
+
+ public virtual Expr VisitForallExpr(ForallExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node = (ForallExpr) this.VisitQuantifierExpr(node);
+ return node;
+ }
+
+ public virtual Expr VisitLambdaExpr(LambdaExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node = (LambdaExpr) this.VisitBinderExpr(node);
+ return node;
+ }
+
+ public virtual Expr VisitLetExpr(LetExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Rhss = this.VisitExprSeq(node.Rhss);
+ node.Dummies = this.VisitVariableSeq(node.Dummies);
+ node.Body = this.VisitExpr(node.Body);
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual Formal VisitFormal(Formal node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return node;
+ }
+
+ public virtual Function VisitFunction(Function node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node = (Function) this.VisitDeclWithFormals(node);
+ if (node.Body != null)
+ {
+ Contract.Assert(node.DefinitionBody == null);
+ node.Body = this.VisitExpr(node.Body);
+ }
+ else if (node.DefinitionBody != null)
+ {
+ node.DefinitionBody = (NAryExpr) this.VisitExpr(node.DefinitionBody);
+ }
+ return node;
+ }
+
+ public virtual GlobalVariable VisitGlobalVariable(GlobalVariable node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node = (GlobalVariable) this.VisitVariable(node);
+ return node;
+ }
+
+ public virtual GotoCmd VisitGotoCmd(GotoCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ // do not visit the labelTargets, or control-flow loops will lead to a looping visitor
+ return node;
+ }
+
+ public virtual Cmd VisitHavocCmd(HavocCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Vars = this.VisitIdentifierExprSeq(node.Vars);
+ return node;
+ }
+
+ public virtual Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ if (node.Decl != null)
+ {
+ node.Decl = this.VisitVariable(node.Decl);
+ }
+
+ return node;
+ }
+
+ public virtual List VisitIdentifierExprSeq(List identifierExprSeq)
+ {
+ Contract.Requires(identifierExprSeq != null);
+ Contract.Ensures(Contract.Result>() != null);
+ lock (identifierExprSeq)
+ {
+ for (int i = 0, n = identifierExprSeq.Count; i < n; i++)
+ {
+ identifierExprSeq[i] = (IdentifierExpr) this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));
+ }
+ }
+
+ return identifierExprSeq;
+ }
+
+ public virtual Implementation VisitImplementation(Implementation node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.LocVars = this.VisitVariableSeq(node.LocVars);
+ node.Blocks = this.VisitBlockList(node.Blocks);
+ node.Proc = (Procedure)node.Proc.StdDispatch(this);
+ node = (Implementation) this.VisitDeclWithFormals(node); // do this first or last?
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual Expr VisitLiteralExpr(LiteralExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return node;
+ }
+
+ public virtual LocalVariable VisitLocalVariable(LocalVariable node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ return node;
+ }
+
+ public virtual AssignLhs VisitMapAssignLhs(MapAssignLhs node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Map = cce.NonNull((AssignLhs) this.Visit(node.Map));
+ for (int i = 0; i < node.Indexes.Count; ++i)
+ {
+ node.Indexes[i] = cce.NonNull((Expr) this.VisitExpr(node.Indexes[i]));
+ }
+
+ return node;
+ }
+
+ public virtual AssignLhs VisitFieldAssignLhs(FieldAssignLhs node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Datatype = cce.NonNull((AssignLhs) this.Visit(node.Datatype));
+ return node;
+ }
+
+ public virtual Type VisitMapType(MapType node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ // not doing anything about the bound variables ... maybe
+ // these should be visited as well ...
+ //
+ // NOTE: when overriding this method, you have to make sure that
+ // the bound variables of the map type are updated correctly
+ lock (node.Arguments)
+ {
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ {
+ node.Arguments[i] = cce.NonNull((Type /*!*/) this.Visit(node.Arguments[i]));
+ }
+ }
+
+ node.Result = cce.NonNull((Type /*!*/) this.Visit(node.Result));
+ return node;
+ }
+
+ public virtual Type VisitMapTypeProxy(MapTypeProxy node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ // if the type proxy is instantiated with some more
+ // specific type, we visit the instantiation
+ if (node.ProxyFor != null)
+ {
+ return (Type) this.Visit(node.ProxyFor);
+ }
+
+ return this.VisitType(node);
+ }
+
+ public virtual Expr VisitNAryExpr(NAryExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Args = this.VisitExprSeq(node.Args);
+ return node;
+ }
+
+ public virtual Expr VisitOldExpr(OldExpr node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Expr = this.VisitExpr(node.Expr);
+ return node;
+ }
+
+ public virtual Procedure VisitProcedure(Procedure node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ node.Ensures = this.VisitEnsuresSeq(node.Ensures);
+ node.InParams = this.VisitVariableSeq(node.InParams);
+ node.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
+ node.OutParams = this.VisitVariableSeq(node.OutParams);
+ node.Requires = this.VisitRequiresSeq(node.Requires);
+ VisitAttributes(node);
+ return node;
+ }
+
+ public virtual ActionDeclRef VisitActionDeclRef(ActionDeclRef node)
+ {
+ return node;
+ }
+
+ public virtual ElimDecl VisitElimDecl(ElimDecl node)
+ {
+ node.Abstraction = VisitActionDeclRef(node.Abstraction);
+ node.Target = VisitActionDeclRef(node.Target);
+ return node;
+ }
+
+ public virtual List VisitElimDeclSeq(List node)
+ {
+ for (int i = 0; i < node.Count; i++)
+ {
+ node[i] = VisitElimDecl(node[i]);
+ }
+ return node;
+ }
+
+ public virtual Procedure VisitActionDecl(ActionDecl node)
+ {
+ for (int i = 0; i < node.Creates.Count; i++)
+ {
+ node.Creates[i] = VisitActionDeclRef(node.Creates[i]);
+ }
+ if (node.RefinedAction != null)
+ {
+ node.RefinedAction = VisitActionDeclRef(node.RefinedAction);
+ }
+ if (node.InvariantAction != null)
+ {
+ node.InvariantAction = VisitActionDeclRef(node.InvariantAction);
+ }
+ node.Eliminates = VisitElimDeclSeq(node.Eliminates);
+ return VisitProcedure(node);
+ }
+
+ public virtual YieldingLoop VisitYieldingLoop(YieldingLoop node)
+ {
+ node.YieldInvariants = VisitCallCmdSeq(node.YieldInvariants);
+ return node;
+ }
+
+ public virtual Dictionary VisitYieldingLoops(Dictionary node)
+ {
+ foreach (var block in node.Keys)
+ {
+ node[block] = VisitYieldingLoop(node[block]);
+ }
+ return node;
+ }
+
+ public virtual HashSet VisitVariableSet(HashSet node)
+ {
+ return node;
+ }
+
+ public virtual Procedure VisitYieldProcedureDecl(YieldProcedureDecl node)
+ {
+ node.YieldRequires = VisitCallCmdSeq(node.YieldRequires);
+ node.YieldEnsures = VisitCallCmdSeq(node.YieldEnsures);
+ node.YieldPreserves = VisitCallCmdSeq(node.YieldPreserves);
+ node.RefinedAction = VisitActionDeclRef(node.RefinedAction);
+ node.VisibleFormals = VisitVariableSet(node.VisibleFormals);
+ node.YieldingLoops = VisitYieldingLoops(node.YieldingLoops);
+ return VisitProcedure(node);
+ }
+
+ public virtual Procedure VisitYieldInvariantDecl(YieldInvariantDecl node)
+ {
+ return VisitProcedure(node);
+ }
+
+ public virtual Program VisitProgram(Program node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ var decls = node.TopLevelDeclarations.ToList();
+ node.ClearTopLevelDeclarations();
+ node.AddTopLevelDeclarations(this.VisitDeclarationList(decls));
+ return node;
+ }
+
+ public virtual QKeyValue VisitQKeyValue(QKeyValue node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ var newParams = new List