diff options
| author |  tabarbe <unknown> | 2010-08-13 00:43:11 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-13 00:43:11 +0000 |
| commit | 85ffcd8f1392bf871e585fe8efb60e38bfdb2f72 (patch) | |
| tree | e697a9f2d08a51d866aaa19a53b016b2749c090b /Source/VCExpr/Boogie2VCExpr.cs | |
| parent | eb284abb4172c6162ac31b865dc2a7e9661fe413 (diff) | |
Boogie: Renaming VCExpr sources in preparation for port commit
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 865 |
1 files changed, 865 insertions, 0 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs new file mode 100644 index 00000000..df966c2d --- /dev/null +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -0,0 +1,865 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+
+// A translator from the Boogie AST to the VCExpr AST.
+// This was previously realised in the methods AbsyExpr.VCView
+
+namespace Microsoft.Boogie.VCExprAST
+{
+ using Microsoft.Boogie;
+
+ public class VCGenerationOptions {
+ private readonly List<string!>! SupportedProverCommands;
+
+ public bool IsProverCommandSupported(string! kind)
+ {
+ return SupportedProverCommands.Contains(kind);
+ }
+
+ public bool IsAnyProverCommandSupported(string! kinds)
+ {
+ if (kinds.IndexOf(',') < 0) {
+ return IsProverCommandSupported(kinds);
+ } else {
+ return exists{string k in kinds.Split(',', ' '); IsProverCommandSupported(k)};
+ }
+ }
+
+ public VCGenerationOptions(List<string!>! supportedProverCommands) {
+ this.SupportedProverCommands = supportedProverCommands;
+ }
+ }
+
+ public delegate VCExpr! CodeExprConverter(CodeExpr! codeExpr, Hashtable/*<Block, VCExprVar!>*/! blockVariables, List<VCExprLetBinding!>! bindings);
+
+ public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {
+ // Stack on which the various Visit-methods put the result of the translation
+ private readonly Stack<VCExpr!>! SubExpressions = new Stack<VCExpr!> ();
+
+ private void Push(VCExpr! expr) {
+ SubExpressions.Push(expr);
+ }
+
+ private VCExpr! Pop() {
+ return SubExpressions.Pop();
+ }
+
+ public VCExpr! Translate(Expr! expr) {
+ this.Visit(expr);
+ return Pop();
+ }
+
+ public List<VCExpr!>! Translate(ExprSeq! exprs) {
+ List<VCExpr!>! res = new List<VCExpr!> ();
+ foreach(Expr e in exprs)
+ res.Add(Translate((!)e));
+ return res;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////
+
+ internal readonly VCExpressionGenerator! Gen;
+
+ public Boogie2VCExprTranslator(VCExpressionGenerator! gen,
+ VCGenerationOptions! genOptions) {
+ this.Gen = gen;
+ this.GenerationOptions = genOptions;
+ UnboundVariables = new VariableMapping<Variable> ();
+ BoundVariables = new VariableMapping<BoundVariable> ();
+ Formals = new VariableMapping<Formal> ();
+ }
+
+ private Boogie2VCExprTranslator(Boogie2VCExprTranslator! tl) {
+ this.Gen = tl.Gen;
+ this.GenerationOptions = tl.GenerationOptions;
+ UnboundVariables =
+ (VariableMapping<Variable>)tl.UnboundVariables.Clone();
+ BoundVariables = new VariableMapping<BoundVariable> ();
+ Formals = new VariableMapping<Formal> ();
+ }
+
+ public object! Clone() {
+ return new Boogie2VCExprTranslator(this);
+ }
+
+ private IAppliableTranslator IAppTranslatorAttr = null;
+ private IAppliableTranslator! IAppTranslator { get {
+ if (IAppTranslatorAttr == null)
+ IAppTranslatorAttr = new IAppliableTranslator (this);
+ return IAppTranslatorAttr;
+ } }
+
+ ///////////////////////////////////////////////////////////////////////////////
+ // Class for handling occurring variables
+
+ private class VariableMapping<VarKind> : ICloneable {
+ private readonly List<Dictionary<VarKind!, VCExprVar!>!>! Mapping;
+
+ public VariableMapping() {
+ List<Dictionary<VarKind!, VCExprVar!>!>! mapping =
+ new List<Dictionary<VarKind!, VCExprVar!>!> ();
+ mapping.Add(new Dictionary<VarKind!, VCExprVar!> ());
+ this.Mapping = mapping;
+ }
+
+ private VariableMapping(VariableMapping<VarKind>! vm) {
+ List<Dictionary<VarKind!, VCExprVar!>!>! mapping =
+ new List<Dictionary<VarKind!, VCExprVar!>!> ();
+ foreach (Dictionary<VarKind!, VCExprVar!>! d in vm.Mapping)
+ mapping.Add(new Dictionary<VarKind!, VCExprVar!> (d));
+ this.Mapping = mapping;
+ }
+
+ public object! Clone() {
+ return new VariableMapping<VarKind> (this);
+ }
+
+ public void PushScope() {
+ Mapping.Add(new Dictionary<VarKind!, VCExprVar!> ());
+ }
+
+ public void PopScope() {
+ assume Mapping.Count > 0;
+ Mapping.RemoveAt(Mapping.Count - 1);
+ }
+
+ public void Bind(VarKind! boogieVar, VCExprVar! vcExprVar)
+ requires !Contains(boogieVar); {
+ Mapping[Mapping.Count - 1].Add(boogieVar, vcExprVar);
+ }
+
+ public VCExprVar! Lookup(VarKind! boogieVar) {
+ VCExprVar res = LookupHelp(boogieVar);
+ assume res != null;
+ return res;
+ }
+
+ [Pure]
+ public bool Contains(VarKind! boogieVar) {
+ return LookupHelp(boogieVar) != null;
+ }
+
+ public bool TryGetValue(VarKind! boogieVar, out VCExprVar res) {
+ res = LookupHelp(boogieVar);
+ return res != null;
+ }
+
+ [Pure]
+ private VCExprVar LookupHelp(VarKind! boogieVar) {
+ VCExprVar res;
+ foreach (Dictionary<VarKind!, VCExprVar!>! d in Mapping) {
+ if (d.TryGetValue(boogieVar, out res))
+ return res;
+ }
+ return null;
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////////
+
+ private readonly VariableMapping<Variable>! UnboundVariables;
+ private readonly VariableMapping<BoundVariable>! BoundVariables;
+ // used when translating the bodies of function expansions
+ private readonly VariableMapping<Formal>! Formals;
+
+ internal void PushBoundVariableScope() {
+ BoundVariables.PushScope();
+ }
+ internal void PopBoundVariableScope() {
+ BoundVariables.PopScope();
+ }
+
+ internal void PushFormalsScope() {
+ Formals.PushScope();
+ }
+ internal void PopFormalsScope() {
+ Formals.PopScope();
+ }
+
+ public VCExprVar! BindVariable(Variable! boogieVar) {
+ if (boogieVar is BoundVariable) {
+ VCExprVar! newVar = Gen.Variable(boogieVar.Name, boogieVar.TypedIdent.Type);
+ BoundVariables.Bind((BoundVariable)boogieVar, newVar);
+ return newVar;
+ } else if (boogieVar is Formal) {
+ VCExprVar! newVar = Gen.Variable(boogieVar.Name, boogieVar.TypedIdent.Type);
+ Formals.Bind((Formal)boogieVar, newVar);
+ return newVar;
+ } else {
+ // only bound variables and formals are declared explicitly
+ assert false;
+ }
+ }
+
+ public VCExprVar! LookupVariable(Variable! boogieVar) {
+
+ BoundVariable bv = boogieVar as BoundVariable;
+ if (bv != null) {
+ return BoundVariables.Lookup(bv);
+ }
+ VCExprVar res;
+ Formal fml = boogieVar as Formal;
+ if (fml != null && Formals.TryGetValue(fml, out res))
+ return (!)res;
+
+ // global variables, local variables, incarnations, etc. are
+ // bound the first time they occur
+ if (!UnboundVariables.TryGetValue(boogieVar, out res)) {
+ res = new VCExprVar (boogieVar.Name, boogieVar.TypedIdent.Type);
+ UnboundVariables.Bind(boogieVar, res);
+ }
+ return (!)res;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ internal readonly VCGenerationOptions! GenerationOptions;
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public override LiteralExpr! VisitLiteralExpr(LiteralExpr! node) {
+ Push(TranslateLiteralExpr(node));
+ return node;
+ }
+ private VCExpr! TranslateLiteralExpr(LiteralExpr! node) {
+ if ( node.Val is bool )
+ {
+ bool b = (bool) node.Val;
+ if ( b ) {
+ return VCExpressionGenerator.True;
+ } else {
+ return VCExpressionGenerator.False;
+ }
+ }
+ else if ( node.Val is BigNum )
+ {
+ return Gen.Integer(node.asBigNum);
+ }
+ else if ( node.Val is BvConst )
+ {
+ return Gen.Bitvector((BvConst)node.Val);
+ }
+ else
+ {
+ System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString());
+ assert false;
+ }
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public override AIVariableExpr! VisitAIVariableExpr(AIVariableExpr! node)
+ {
+ assert false;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public override Expr! VisitIdentifierExpr(IdentifierExpr! node) {
+ assume node.Decl != null; // the expression has to be resolved
+ Push(LookupVariable(node.Decl));
+ return node;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ // Because of our scheme for numbering incarnations of variables, the pre-state
+ // value of a variable x is always just "x". (The first update to it in a method
+ // causes it to become "x0". So we just remove old expressions with a visitor
+ // before transforming it into a VCExpr.
+ public override Expr! VisitOldExpr(OldExpr! node)
+ {
+ assert false;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public override Expr! VisitNAryExpr(NAryExpr! node)
+ {
+ Push(TranslateNAryExpr(node));
+ return node;
+ }
+
+ private VCExpr! TranslateNAryExpr(NAryExpr! node) {
+ int n = node.Args.Length;
+ List<VCExpr!>! vcs = new List<VCExpr!> (n);
+ for(int i = 0; i < n; i++)
+ {
+ vcs.Add(Translate((!)node.Args[i]));
+ }
+
+ if (node.Type == null) {
+ System.Console.WriteLine("*** type is null for {0}", node);
+ assert false;
+ }
+
+ return IAppTranslator.Translate(node.Fun, node.Type, vcs,
+ ToList((!)node.TypeParameters));
+ }
+
+
+ private static List<Type!>! EMPTY_TYPE_LIST = new List<Type!> ();
+
+ private List<Type!>! ToList(TypeParamInstantiation! insts) {
+ if (insts.FormalTypeParams.Count == 0)
+ return EMPTY_TYPE_LIST;
+
+ List<Type!>! typeArgs = new List<Type!> ();
+ foreach (TypeVariable! var in insts.FormalTypeParams)
+ typeArgs.Add(insts[var]);
+ return typeArgs;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public override QuantifierExpr! VisitQuantifierExpr(QuantifierExpr! node) {
+ Push(TranslateQuantifierExpr(node));
+ return node;
+ }
+
+ public override ExistsExpr! VisitExistsExpr(ExistsExpr! node)
+ {
+ node = (ExistsExpr) this.VisitQuantifierExpr(node);
+ return node;
+ }
+
+ public override ForallExpr! VisitForallExpr(ForallExpr! node)
+ {
+ node = (ForallExpr) this.VisitQuantifierExpr(node);
+ return node;
+ }
+
+ private VCExpr! TranslateQuantifierExpr(QuantifierExpr! node)
+ {
+ List<TypeVariable!>! typeParams = new List<TypeVariable!> ();
+ foreach (TypeVariable! v in node.TypeParameters)
+ typeParams.Add(v);
+
+ PushBoundVariableScope();
+
+ List<VCExprVar!>! boundVars = new List<VCExprVar!> ();
+ foreach (Variable! v in node.Dummies)
+ boundVars.Add(BindVariable(v));
+
+ try {
+ List<VCTrigger!>! triggers = TranslateTriggers(node.Triggers);
+ VCExpr! body = Translate(node.Body);
+ VCQuantifierInfos! infos = GenerateQuantifierInfos(node);
+
+ Quantifier quan;
+ if (node is ForallExpr)
+ quan = Quantifier.ALL;
+ else if (node is ExistsExpr)
+ quan = Quantifier.EX;
+ else
+ assert false;
+
+ return Gen.Quantify(quan, typeParams, boundVars, triggers, infos, body);
+ } finally {
+ PopBoundVariableScope();
+ }
+ }
+
+ private List<VCTrigger!>! TranslateTriggers(Trigger node)
+ {
+ List<VCTrigger!>! res = new List<VCTrigger!> ();
+ Trigger curTrigger = node;
+ while (curTrigger != null) {
+ res.Add(Gen.Trigger(curTrigger.Pos, Translate(curTrigger.Tr)));
+ curTrigger = curTrigger.Next;
+ }
+ return res;
+ }
+
+ private VCQuantifierInfos! GenerateQuantifierInfos(QuantifierExpr! node) {
+ string qid = getQidNameFromQKeyValue(node.Dummies, node.Attributes);
+ return new VCQuantifierInfos(qid, node.SkolemId, false, node.Attributes);
+ }
+
+ private string getQidNameFromQKeyValue(VariableSeq! vars, QKeyValue attributes) {
+ // Check for a 'qid, name' pair in keyvalues
+ string qid = QKeyValue.FindStringAttribute(attributes, "qid");
+ if (qid == null && vars.Length != 0){
+ // generate default name (line:column position in .bpl file)
+ Variable v = vars[0];
+ assert v != null; // Rustan's claim!
+ // Include the first 8 characters of the filename in QID (helpful in case we use /concat)
+ // We limit it to 8, so the SX file doesn't grow too big, and who on earth would need
+ // more than 8 characters in a filename anyways.
+ int max = 8;
+ StringBuilder buf = new StringBuilder(max + 20);
+ string filename = v.tok.filename;
+ if (filename == null) filename = "unknown";
+ for (int i = 0; i < filename.Length; ++i) {
+ if (filename[i] == '/' || filename[i] == '\\') buf.Length = 0;
+ if (buf.Length < max && char.IsLetterOrDigit(filename[i])) {
+ if (buf.Length == 0 && char.IsDigit(filename[i])) {
+ // Z3 does not like QID's to start with a digit, so we prepend another character
+ buf.Append('_');
+ }
+ buf.Append(filename[i]);
+ }
+ }
+ buf.Append('.').Append(v.Line).Append(':').Append(v.Col);
+ qid = buf.ToString();
+ }
+ return qid;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public override BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)
+ {
+ Push(TranslateBvExtractExpr(node));
+ return node;
+ }
+
+ private VCExpr! TranslateBvExtractExpr(BvExtractExpr! node)
+ requires node.Start <= node.End; {
+ VCExpr! bv = Translate(node.Bitvector);
+ return Gen.BvExtract(bv, ((!)node.Bitvector.Type).BvBits, node.Start, node.End);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public override BvConcatExpr! VisitBvConcatExpr(BvConcatExpr! node)
+ {
+ Push(TranslateBvConcatExpr(node));
+ return node;
+ }
+
+ private VCExpr! TranslateBvConcatExpr(BvConcatExpr! node) {
+ VCExpr! bv0 = Translate(node.E0);
+ VCExpr! bv1 = Translate(node.E1);
+ return Gen.BvConcat(bv0, bv1);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+ // all the other cases should never happen
+
+ public override Cmd! VisitAssertCmd(AssertCmd! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitAssignCmd(AssignCmd! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitAssumeCmd(AssumeCmd! node)
+ {
+ assert false;
+ }
+ public override AtomicRE! VisitAtomicRE(AtomicRE! node)
+ {
+ assert false;
+ }
+ public override Axiom! VisitAxiom(Axiom! node)
+ {
+ assert false;
+ }
+ public override Type! VisitBasicType(BasicType! node)
+ {
+ assert false;
+ }
+ public override Type! VisitBvType(BvType! node)
+ {
+ assert false;
+ }
+ public override Block! VisitBlock(Block! node)
+ {
+ assert false;
+ }
+ CodeExprConverter codeExprConverter = null;
+ public void SetCodeExprConverter(CodeExprConverter f){
+ this.codeExprConverter = f;
+ }
+ public override Expr! VisitCodeExpr(CodeExpr! codeExpr)
+ {
+ assume codeExprConverter != null;
+
+ Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
+ List<VCExprLetBinding!> bindings = new List<VCExprLetBinding!>();
+ VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings);
+ Push(e);
+ return codeExpr;
+ }
+ public override BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)
+ {
+ assert false;
+ }
+ public override List<Block!>! VisitBlockList(List<Block!>! blocks)
+ {
+ assert false;
+ }
+ public override BoundVariable! VisitBoundVariable(BoundVariable! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitCallCmd(CallCmd! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitCallForallCmd(CallForallCmd! node)
+ {
+ assert false;
+ }
+ public override CmdSeq! VisitCmdSeq(CmdSeq! cmdSeq)
+ {
+ assert false;
+ }
+ public override Choice! VisitChoice(Choice! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitCommentCmd(CommentCmd! node)
+ {
+ assert false;
+ }
+ public override Constant! VisitConstant(Constant! node)
+ {
+ assert false;
+ }
+ public override CtorType! VisitCtorType(CtorType! node)
+ {
+ assert false;
+ }
+ public override Declaration! VisitDeclaration(Declaration! node)
+ {
+ assert false;
+ }
+ public override List<Declaration!>! VisitDeclarationList(List<Declaration!>! declarationList)
+ {
+ assert false;
+ }
+ public override DeclWithFormals! VisitDeclWithFormals(DeclWithFormals! node)
+ {
+ assert false;
+ }
+ public override Requires! VisitRequires(Requires! @requires)
+ {
+ assert false;
+ }
+ public override RequiresSeq! VisitRequiresSeq(RequiresSeq! requiresSeq)
+ {
+ assert false;
+ }
+ public override Ensures! VisitEnsures(Ensures! @ensures)
+ {
+ assert false;
+ }
+ public override EnsuresSeq! VisitEnsuresSeq(EnsuresSeq! ensuresSeq)
+ {
+ assert false;
+ }
+ public override Formal! VisitFormal(Formal! node)
+ {
+ assert false;
+ }
+ public override Function! VisitFunction(Function! node)
+ {
+ assert false;
+ }
+ public override GlobalVariable! VisitGlobalVariable(GlobalVariable! node)
+ {
+ assert false;
+ }
+ public override GotoCmd! VisitGotoCmd(GotoCmd! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitHavocCmd(HavocCmd! node)
+ {
+ assert false;
+ }
+ public override Implementation! VisitImplementation(Implementation! node)
+ {
+ assert false;
+ }
+ public override LocalVariable! VisitLocalVariable(LocalVariable! node)
+ {
+ assert false;
+ }
+ public override AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)
+ {
+ assert false;
+ }
+ public override MapType! VisitMapType(MapType! node)
+ {
+ assert false;
+ }
+ public override Procedure! VisitProcedure(Procedure! node)
+ {
+ assert false;
+ }
+ public override Program! VisitProgram(Program! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitRE(RE! node)
+ {
+ assert false;
+ }
+ public override RESeq! VisitRESeq(RESeq! reSeq)
+ {
+ assert false;
+ }
+ public override ReturnCmd! VisitReturnCmd(ReturnCmd! node)
+ {
+ assert false;
+ }
+ public override ReturnExprCmd! VisitReturnExprCmd(ReturnExprCmd! node)
+ {
+ assert false;
+ }
+ public override Sequential! VisitSequential(Sequential! node)
+ {
+ assert false;
+ }
+ public override AssignLhs! VisitSimpleAssignLhs(SimpleAssignLhs! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitStateCmd(StateCmd! node)
+ {
+ assert false;
+ }
+ public override TransferCmd! VisitTransferCmd(TransferCmd! node)
+ {
+ assert false;
+ }
+ public override Trigger! VisitTrigger(Trigger! node)
+ {
+ assert false;
+ }
+ public override Type! VisitType(Type! node)
+ {
+ assert false;
+ }
+ public override TypedIdent! VisitTypedIdent(TypedIdent! node)
+ {
+ assert false;
+ }
+ public override Type! VisitTypeSynonymAnnotation(TypeSynonymAnnotation! node)
+ {
+ assert false;
+ }
+ public override Type! VisitTypeVariable(TypeVariable! node)
+ {
+ assert false;
+ }
+ public override Variable! VisitVariable(Variable! node)
+ {
+ assert false;
+ }
+ public override VariableSeq! VisitVariableSeq(VariableSeq! variableSeq)
+ {
+ assert false;
+ }
+ public override Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
+ {
+ assert false;
+ }
+ public override Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
+ {
+ assert false;
+ }
+
+ }
+
+
+ /////////////////////////////////////////////////////////////////////////////////
+
+ public class IAppliableTranslator : IAppliableVisitor<VCExpr!> {
+
+ private readonly Boogie2VCExprTranslator! BaseTranslator;
+
+ private VCExpressionGenerator! Gen { get {
+ return BaseTranslator.Gen;
+ } }
+ private VCGenerationOptions! GenerationOptions { get {
+ return BaseTranslator.GenerationOptions;
+ } }
+
+ public IAppliableTranslator(Boogie2VCExprTranslator! baseTranslator) {
+ this.BaseTranslator = baseTranslator;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////
+
+ private List<VCExpr!>! args = new List<VCExpr!>();
+ private List<Type!>! typeArgs = new List<Type!>();
+
+ public VCExpr! Translate(IAppliable! app, Type! ty, List<VCExpr!>! args, List<Type!>! typeArgs) {
+
+ List<VCExpr!>! oldArgs = this.args;
+ List<Type!>! oldTypeArgs = this.typeArgs;
+ this.args = args;
+ this.typeArgs = typeArgs;
+ VCExpr! result = app.Dispatch<VCExpr!>(this);
+ this.args = oldArgs;
+ this.typeArgs = oldTypeArgs;
+ return result;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////
+
+
+
+ public VCExpr! Visit(UnaryOperator! unaryOperator) {
+ assert unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1;
+ return Gen.Not(this.args);
+ }
+
+ public VCExpr! Visit(BinaryOperator! binaryOperator) {
+ return TranslateBinaryOperator(binaryOperator, this.args);
+ }
+
+ public VCExpr! Visit(FunctionCall! functionCall) {
+ return TranslateFunctionCall(functionCall, this.args, this.typeArgs);
+ }
+
+ public VCExpr! Visit(MapSelect! mapSelect) {
+ return Gen.Select(this.args, this.typeArgs);
+ }
+
+ public VCExpr! Visit(MapStore! mapStore) {
+ return Gen.Store(this.args, this.typeArgs);
+ }
+
+ public VCExpr! Visit(TypeCoercion! typeCoercion) {
+ assert this.args.Count == 1;
+ return this.args[0];
+ }
+
+ public VCExpr! Visit(IfThenElse! ite) {
+ return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////
+
+ private VCExpr! TranslateBinaryOperator(BinaryOperator! app, List<VCExpr!>! args) {
+ assert args.Count == 2;
+
+ switch (app.Op) {
+ case BinaryOperator.Opcode.Add:
+ return Gen.Function(VCExpressionGenerator.AddOp, args);
+ case BinaryOperator.Opcode.Sub:
+ return Gen.Function(VCExpressionGenerator.SubOp, args);
+ case BinaryOperator.Opcode.Mul:
+ return Gen.Function(VCExpressionGenerator.MulOp, args);
+ case BinaryOperator.Opcode.Div:
+ return Gen.Function(VCExpressionGenerator.DivOp, args);
+ case BinaryOperator.Opcode.Mod:
+ return Gen.Function(VCExpressionGenerator.ModOp, args);
+ case BinaryOperator.Opcode.Eq:
+ case BinaryOperator.Opcode.Iff:
+ // we don't distinguish between equality and equivalence at this point
+ return Gen.Function(VCExpressionGenerator.EqOp, args);
+ case BinaryOperator.Opcode.Neq:
+ return Gen.Function(VCExpressionGenerator.NeqOp, args);
+ case BinaryOperator.Opcode.Lt:
+ return Gen.Function(VCExpressionGenerator.LtOp, args);
+ case BinaryOperator.Opcode.Le:
+ return Gen.Function(VCExpressionGenerator.LeOp, args);
+ case BinaryOperator.Opcode.Ge:
+ return Gen.Function(VCExpressionGenerator.GeOp, args);
+ case BinaryOperator.Opcode.Gt:
+ return Gen.Function(VCExpressionGenerator.GtOp, args);
+ case BinaryOperator.Opcode.Imp:
+ return Gen.Function(VCExpressionGenerator.ImpliesOp, args);
+ case BinaryOperator.Opcode.And:
+ return Gen.Function(VCExpressionGenerator.AndOp, args);
+ case BinaryOperator.Opcode.Or:
+ return Gen.Function(VCExpressionGenerator.OrOp, args);
+ case BinaryOperator.Opcode.Subtype:
+ return Gen.Function(VCExpressionGenerator.SubtypeOp, args);
+ default:
+ assert false; // unexpected binary operator
+ }
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////
+
+ private VCExpr! TranslateFunctionCall(FunctionCall! app,
+ List<VCExpr!>! args, List<Type!>! typeArgs) {
+ assert app.Func != null; // resolution must have happened
+
+ VCExpr res = ApplyExpansion(app, args, typeArgs);
+ if (res != null)
+ return res;
+
+ VCExprOp! functionOp = Gen.BoogieFunctionOp(app.Func);
+ return Gen.Function(functionOp, args, typeArgs);
+ }
+
+ private VCExpr ApplyExpansion(FunctionCall! app,
+ List<VCExpr!>! args, List<Type!>! typeArgs) {
+ assert app.Func != null; // resolution must have happened
+
+ if (app.Func.doingExpansion) {
+ System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
+ return null;
+ }
+
+ Expansion exp = FindExpansion(app.Func);
+ if (exp == null)
+ return null;
+
+ VCExpr! translatedBody;
+ VCExprSubstitution! subst = new VCExprSubstitution();
+ try {
+ BaseTranslator.PushFormalsScope();
+ BaseTranslator.PushBoundVariableScope();
+ app.Func.doingExpansion = true;
+
+ // first bind the formals to VCExpr variables, which are later
+ // substituted with the actual parameters
+ for (int i = 0; i < exp.formals.Length; ++i)
+ subst[BaseTranslator.BindVariable((!)exp.formals[i])] = args[i];
+
+ // recursively translate the body of the expansion
+ translatedBody = BaseTranslator.Translate(exp.body);
+ } finally {
+ BaseTranslator.PopFormalsScope();
+ BaseTranslator.PopBoundVariableScope();
+ app.Func.doingExpansion = false;
+ }
+
+ // substitute the formals with the actual parameters in the body
+ assert typeArgs.Count == exp.TypeParameters.Length;
+ for (int i = 0; i < typeArgs.Count; ++i)
+ subst[exp.TypeParameters[i]] = typeArgs[i];
+ SubstitutingVCExprVisitor! substituter = new SubstitutingVCExprVisitor (Gen);
+ return substituter.Mutate(translatedBody, subst);
+ }
+
+ private Expansion? FindExpansion(Function! func)
+ {
+ if (func.expansions == null) return null;
+
+ Expansion? exp = null;
+ foreach (Expansion! e in func.expansions) {
+ if (e.ignore == null || !GenerationOptions.IsAnyProverCommandSupported(e.ignore)) {
+ if (exp == null) {
+ exp = e;
+ } else {
+ System.Console.WriteLine("*** more than one possible expansion for {0}", func);
+ return null;
+ }
+ }
+ }
+
+ return exp;
+ }
+ }
+}
|