diff options
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/BigLiteralAbstracter.ssc | 198 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.ssc | 853 | ||||
| -rw-r--r-- | Source/VCExpr/Clustering.ssc | 449 | ||||
| -rw-r--r-- | Source/VCExpr/LetBindingSorter.ssc | 135 | ||||
| -rw-r--r-- | Source/VCExpr/NameClashResolver.ssc | 129 | ||||
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.ssc | 795 | ||||
| -rw-r--r-- | Source/VCExpr/TermFormulaFlattening.ssc | 222 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.ssc | 1160 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasureArguments.ssc | 618 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasurePremisses.ssc | 1025 | ||||
| -rw-r--r-- | Source/VCExpr/VCExpr.sscproj | 141 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprAST.ssc | 1285 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTPrinter.ssc | 240 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.ssc | 999 |
14 files changed, 8249 insertions, 0 deletions
diff --git a/Source/VCExpr/BigLiteralAbstracter.ssc b/Source/VCExpr/BigLiteralAbstracter.ssc new file mode 100644 index 00000000..fac34a8d --- /dev/null +++ b/Source/VCExpr/BigLiteralAbstracter.ssc @@ -0,0 +1,198 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+
+// Code for replacing large integer literals in VCExpr with
+// constants. This is necessary for Simplify, which cannot deal with
+// literals larger than 32 bits
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+ public class BigLiteralAbstracter : MutatingVCExprVisitor<bool>, ICloneable {
+
+ public BigLiteralAbstracter(VCExpressionGenerator! gen) {
+ base(gen);
+ DummyVar = gen.Variable("x", Type.Int);
+ IncAxioms = new List<VCExpr!> ();
+ Literals = new List<KeyValuePair<BigNum, VCExprVar!>> ();
+ }
+
+ private BigLiteralAbstracter(BigLiteralAbstracter! abstracter) {
+ base(abstracter.Gen);
+ DummyVar = abstracter.DummyVar;
+ IncAxioms = new List<VCExpr!> (abstracter.IncAxioms);
+ Literals = new List<KeyValuePair<BigNum, VCExprVar!>> (abstracter.Literals);
+ }
+
+ public Object! Clone() {
+ return new BigLiteralAbstracter(this);
+ }
+
+ private static readonly BigNum ConstantDistance = BigNum.FromLong(100000);
+ private static readonly BigNum NegConstantDistance = BigNum.FromLong(-100000);
+ // distance twice plus one
+ private static readonly BigNum ConstantDistanceTPO = BigNum.FromLong(200001);
+ private static readonly BigNum ConstantDistancePO = BigNum.FromLong(100001);
+
+ public VCExpr! Abstract(VCExpr! expr) {
+ return Mutate(expr, true);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // list in which axioms are incrementally collected
+ private readonly List<VCExpr!>! IncAxioms;
+
+ private void AddAxiom(VCExpr! axiom) {
+ IncAxioms.Add(axiom);
+ }
+
+ // Return all axioms that were added since the last time NewAxioms
+ // was called
+ public VCExpr! GetNewAxioms() {
+ VCExpr! res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms);
+ IncAxioms.Clear();
+ return res;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // All named integer literals known to the visitor, in ascending
+ // order. Such literals are always positive, and the distance
+ // between two literals is always more than ConstantDistance.
+ private readonly List<KeyValuePair<BigNum, VCExprVar!>>! Literals;
+
+ private class EntryComparerC : IComparer<KeyValuePair<BigNum, VCExprVar!>> {
+ public int Compare(KeyValuePair<BigNum, VCExprVar!> a,
+ KeyValuePair<BigNum, VCExprVar!> b) {
+ return a.Key.CompareTo(b.Key);
+ }
+ }
+
+ private static readonly EntryComparerC EntryComparer = new EntryComparerC ();
+
+ // variable used when searching for entries in the literal list
+ private readonly VCExprVar! DummyVar;
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Construct an expression to represent the given (large) integer
+ // literal. Constants are defined and axiomatised if necessary
+ private VCExpr! Represent(BigNum lit)
+ requires NegConstantDistance > lit || lit > ConstantDistance; {
+
+ if (lit.IsNegative)
+ return Gen.Function(VCExpressionGenerator.SubOp,
+ Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg));
+ else
+ return RepresentPos(lit);
+ }
+
+ private VCExpr! RepresentPos(BigNum lit)
+ requires lit > ConstantDistance; {
+
+ int index = GetIndexFor(lit);
+ if (index >= 0)
+ // precise match
+ return Literals[index].Value;
+
+ // check whether a constant is defined that is at most
+ // ConstantDistance away from lit
+ index = ~index;
+ VCExpr res = null;
+ BigNum resDistance = ConstantDistancePO;
+
+ if (index > 0) {
+ BigNum dist = lit - Literals[index - 1].Key;
+ if (dist < resDistance) {
+ resDistance = dist;
+ res = Gen.Function(VCExpressionGenerator.AddOp,
+ Literals[index - 1].Value, Gen.Integer(dist));
+ }
+ }
+
+ if (index < Literals.Count) {
+ BigNum dist = Literals[index].Key - lit;
+ if (dist < resDistance) {
+ resDistance = dist;
+ res = Gen.Function(VCExpressionGenerator.SubOp,
+ Literals[index].Value, Gen.Integer(dist));
+ }
+ }
+
+ if (res != null)
+ return res;
+
+ // otherwise, define a new constant to represent this literal
+ return AddConstantFor(lit);
+ }
+
+ private VCExpr! AddConstantFor(BigNum lit)
+ requires lit > ConstantDistance; {
+
+ VCExprVar! res = Gen.Variable("int#" + lit, Type.Int);
+ int index = GetIndexFor(lit);
+ assert index < 0;
+ index = ~index;
+
+ Literals.Insert(index, new KeyValuePair<BigNum, VCExprVar!>(lit, res));
+
+ // relate the new constant to the predecessor and successor
+ if (index > 0)
+ DefineRelationship(Literals[index - 1].Value, Literals[index - 1].Key,
+ res, lit);
+ else
+ DefineRelationship(Gen.Integer(BigNum.ZERO), BigNum.ZERO, res, lit);
+
+ if (index < Literals.Count - 1)
+ DefineRelationship(res, lit,
+ Literals[index + 1].Value, Literals[index + 1].Key);
+
+ return res;
+ }
+
+ private void DefineRelationship(VCExpr! aExpr, BigNum aValue,
+ VCExpr! bExpr, BigNum bValue)
+ requires aValue < bValue; {
+
+ BigNum dist = bValue - aValue;
+ VCExpr! distExpr = Gen.Function(VCExpressionGenerator.SubOp, bExpr, aExpr);
+ if (dist <= ConstantDistanceTPO)
+ // constants that are sufficiently close to each other are put
+ // into a precise relationship
+ AddAxiom(Gen.Eq(distExpr, Gen.Integer(dist)));
+ else
+ AddAxiom(Gen.Function(VCExpressionGenerator.GtOp,
+ distExpr, Gen.Integer(ConstantDistanceTPO)));
+ }
+
+ private int GetIndexFor(BigNum lit) {
+ return Literals.BinarySearch(new KeyValuePair<BigNum, VCExprVar!>
+ (lit, DummyVar),
+ EntryComparer);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprLiteral! node, bool arg) {
+ VCExprIntLit intLit = node as VCExprIntLit;
+ if (intLit != null) {
+ if (NegConstantDistance > intLit.Val || intLit.Val > ConstantDistance)
+ return Represent(intLit.Val);
+ }
+ return node;
+ }
+
+ }
+
+}
\ No newline at end of file diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc new file mode 100644 index 00000000..b344c03d --- /dev/null +++ b/Source/VCExpr/Boogie2VCExpr.ssc @@ -0,0 +1,853 @@ +//-----------------------------------------------------------------------------
+//
+// 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 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;
+ }
+
+ public override Expr! VisitLoopPredicate(LoopPredicate! node)
+ {
+ return this.VisitNAryExpr(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]))
+ buf.Append(filename[i]);
+ }
+ buf.Append('.').Append(v.Line).Append(':').Append(v.Col);
+ qid = buf.ToString();
+ }
+ return qid;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public override ExtractExpr! VisitExtractExpr(ExtractExpr! node)
+ {
+ Push(TranslateExtractExpr(node));
+ return node;
+ }
+
+ private VCExpr! TranslateExtractExpr(ExtractExpr! 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;
+ }
+ public override Expr! VisitBlockExpr(BlockExpr! node)
+ {
+ assert false;
+ }
+ 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(LoopPredicateName! loopPredicateName) {
+ return Gen.Variable(loopPredicateName.Name, Type.Bool); // We generate a variable. Intuition: it is a second order variable
+ }
+
+ 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];
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////
+
+ 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;
+ }
+ }
+}
diff --git a/Source/VCExpr/Clustering.ssc b/Source/VCExpr/Clustering.ssc new file mode 100644 index 00000000..7692ceb1 --- /dev/null +++ b/Source/VCExpr/Clustering.ssc @@ -0,0 +1,449 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+using Microsoft.Boogie.VCExprAST;
+
+// Code for managing and clusterings sets of terms; this is used to
+// compress the input given to the theorem prover
+
+namespace Microsoft.Boogie.Clustering
+{
+ using Microsoft.Boogie.VCExprAST;
+
+
+ public class SubtermCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+
+ private readonly VCExpressionGenerator! Gen;
+
+ public SubtermCollector(VCExpressionGenerator! gen) {
+ Gen = gen;
+ }
+
+ // variables that are global and treated like constants
+ private readonly IDictionary<VCExprVar!, VCExprVar!>! GlobalVariables =
+ new Dictionary<VCExprVar!, VCExprVar!> ();
+
+ private readonly IDictionary<VCExprOp!, TermClustersSameHead!>! SubtermClusters =
+ new Dictionary<VCExprOp!, TermClustersSameHead!> ();
+
+ public void UnifyClusters() {
+ foreach (KeyValuePair<VCExprOp!, TermClustersSameHead!> pair
+ in SubtermClusters)
+ pair.Value.UnifyClusters();
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ protected override bool StandardResult(VCExpr! node, bool arg) {
+ return false; // by default, do not collect terms containing node
+ }
+
+ public override bool Visit(VCExprLiteral! node, bool arg) {
+ return true;
+ }
+
+ public override bool Visit(VCExprNAry! node, bool arg) {
+ VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
+ if (op == null) {
+ base.Visit(node, arg);
+ return false;
+ }
+
+ bool res = true;
+ foreach (VCExpr! subexpr in node)
+ res &= this.Traverse(subexpr, arg);
+
+ if (res) {
+ TermClustersSameHead clusters;
+ if (!SubtermClusters.TryGetValue(op, out clusters)) {
+ clusters = new TermClustersSameHead(op, GlobalVariables, Gen);
+ SubtermClusters.Add(op, clusters);
+ }
+ ((!)clusters).AddExpr(node);
+ }
+
+ return res;
+ }
+
+ public override bool Visit(VCExprVar! node, bool arg) {
+ if (!BoundTermVars.Contains(node))
+ GlobalVariables[node] = node;
+ return true;
+ }
+
+ [Pure]
+ public override string! ToString()
+ {
+ string! res = "";
+ foreach (KeyValuePair<VCExprOp!, TermClustersSameHead!> pair
+ in SubtermClusters)
+ res = res + pair.Value + "\n";
+ return res;
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ // Class for managing and clustering a set of terms that all start
+ // with the same function symbol
+ internal class TermClustersSameHead {
+
+ public readonly VCExprOp! Op;
+ private readonly VCExpressionGenerator! Gen;
+
+ public TermClustersSameHead(VCExprOp! op,
+ IDictionary<VCExprVar!, VCExprVar!>! globalVars,
+ VCExpressionGenerator! gen) {
+ Op = op;
+ GlobalVariables = globalVars;
+ Gen = gen;
+ }
+
+ // variables that are global and treated like constants
+ private readonly IDictionary<VCExprVar!, VCExprVar!>! GlobalVariables;
+
+ private readonly List<Cluster>! Clusters = new List<Cluster> ();
+
+ private struct Cluster {
+ public readonly VCExprNAry! Generator;
+ public readonly int Size;
+
+ public Cluster(VCExprNAry! generator, int size) {
+ Generator = generator;
+ Size = size;
+ }
+ }
+
+ private int Distance(Cluster a, Cluster b) {
+ AntiUnificationVisitor! visitor = new AntiUnificationVisitor (Gen);
+ visitor.AntiUnify(a.Generator, b.Generator);
+
+ int reprSizeA, reprSizeB;
+ visitor.RepresentationSize(GlobalVariables, out reprSizeA, out reprSizeB);
+ return (a.Size - 1) * reprSizeA + (b.Size - 1) * reprSizeB;
+ }
+
+ private bool EqualUpToRenaming(Cluster a, Cluster b) {
+ AntiUnificationVisitor! visitor = new AntiUnificationVisitor (Gen);
+ visitor.AntiUnify(a.Generator, b.Generator);
+ return visitor.RepresentationIsRenaming(GlobalVariables);
+ }
+
+ private Cluster Merge(Cluster a, Cluster b) {
+ AntiUnificationVisitor! visitor = new AntiUnificationVisitor (Gen);
+ VCExpr! generator = visitor.AntiUnify(a.Generator, b.Generator);
+ VCExprNAry generatorNAry = generator as VCExprNAry;
+ assert generatorNAry != null && Op.Equals(generatorNAry.Op);
+ return new Cluster(generatorNAry, a.Size + b.Size);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public void AddExpr(VCExprNAry! expr)
+ requires Op.Equals(expr.Op); {
+
+ Cluster c = new Cluster (expr, 1);
+ for (int i = 0; i < Clusters.Count; ++i) {
+ Cluster d = Clusters[i];
+ if (EqualUpToRenaming(c, d)) {
+ Clusters[i] = new Cluster (d.Generator, d.Size + 1);
+ return;
+ }
+ }
+
+ Clusters.Add(c);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private struct ClusteringMatrix {
+
+ private readonly VCExpressionGenerator! Gen;
+ private readonly IDictionary<VCExprVar!, VCExprVar!>! GlobalVariables;
+
+ public readonly List<Cluster>! Clusters;
+ public readonly bool[]! RemainingClusters;
+
+ public readonly Distance[,]! Distances;
+
+ public struct Distance {
+ public readonly int Dist;
+ public readonly VCExprNAry! Generator;
+
+ public Distance(Cluster a, Cluster b,
+ IDictionary<VCExprVar!, VCExprVar!>! globalVars,
+ VCExpressionGenerator! gen) {
+ AntiUnificationVisitor! visitor = new AntiUnificationVisitor (gen);
+ Generator = (VCExprNAry)visitor.AntiUnify(a.Generator, b.Generator);
+
+ int reprSizeA, reprSizeB;
+ visitor.RepresentationSize(globalVars, out reprSizeA, out reprSizeB);
+ Dist = (a.Size - 1) * reprSizeA + (b.Size - 1) * reprSizeB;
+ }
+ }
+
+ public ClusteringMatrix(List<Cluster>! clusters,
+ IDictionary<VCExprVar!, VCExprVar!>! globalVars,
+ VCExpressionGenerator! gen) {
+ List<Cluster>! c = new List<Cluster> ();
+ c.AddRange(clusters);
+ Clusters = c;
+
+ GlobalVariables = globalVars;
+ Gen = gen;
+
+ bool[] remaining = new bool [clusters.Count];
+ RemainingClusters = remaining;
+ for (int i = 0; i < remaining.Length; ++i)
+ remaining[i] = true;
+
+ Distance[,]! distances = new Distance [clusters.Count, clusters.Count];
+ Distances = distances;
+ for (int i = 1; i < clusters.Count; ++i)
+ for (int j = 0; j < i; ++j)
+ distances[i, j] =
+ new Distance (clusters[i], clusters[j], GlobalVariables, Gen);
+ }
+
+ public void UnifyClusters(int maxDist) {
+ while (true) {
+ int i, j;
+ int minDist = FindMinDistance(out i, out j);
+
+ if (minDist > maxDist)
+ return;
+
+ MergeClusters(i, j);
+ }
+ }
+
+ public void ResultingClusters(List<Cluster>! clusters) {
+ clusters.Clear();
+ for (int i = 0; i < Clusters.Count; ++i)
+ if (RemainingClusters[i])
+ clusters.Add(Clusters[i]);
+ }
+
+ //////////////////////////////////////////////////////////////////////////
+
+ private void Update(int i) {
+ for (int j = 0; j < i; ++j) {
+ if (RemainingClusters[j])
+ Distances[i, j] =
+ new Distance (Clusters[i], Clusters[j], GlobalVariables, Gen);
+ }
+ for (int j = i + 1; j < Clusters.Count; ++j) {
+ if (RemainingClusters[j])
+ Distances[j, i] =
+ new Distance (Clusters[j], Clusters[i], GlobalVariables, Gen);
+ }
+ }
+
+ private int FindMinDistance(out int c0, out int c1) {
+ int minDist = int.MaxValue;
+ c0 = -1;
+ c1 = -1;
+
+ for (int i = 0; i < Clusters.Count; ++i)
+ if (RemainingClusters[i]) {
+ for (int j = 0; j < i; ++j)
+ if (RemainingClusters[j]) {
+ if (Distances[i, j].Dist < minDist) {
+ minDist = Distances[i, j].Dist;
+ c0 = i;
+ c1 = j;
+ }
+ }
+ }
+
+ assert c0 == -1 && c1 == -1 || c0 > c1 && c1 >= 0;
+ return minDist;
+ }
+
+ private void MergeClusters(int i, int j)
+ requires j >= 0 && i > j &&
+ RemainingClusters[i] && RemainingClusters[j]; {
+ Clusters[i] = new Cluster (Distances[i, j].Generator,
+ Clusters[i].Size + Clusters[j].Size);
+ RemainingClusters[j] = false;
+ Update(i);
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public void UnifyClusters() {
+ ClusteringMatrix matrix =
+ new ClusteringMatrix (Clusters, GlobalVariables, Gen);
+ matrix.UnifyClusters(50);
+ matrix.ResultingClusters(Clusters);
+ }
+
+ [Pure]
+ public override string! ToString()
+ {
+ string! res = "";
+ foreach (Cluster c in Clusters)
+ res = res + c.Generator + "\t" + c.Size + "\n";
+ return res;
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ internal class AntiUnificationVisitor : TraversingVCExprVisitor<VCExpr!, VCExpr!> {
+
+ private readonly VCExpressionGenerator! Gen;
+
+ public AntiUnificationVisitor(VCExpressionGenerator! gen) {
+ Gen = gen;
+ }
+
+ // Sub-expressions in the first and second expression to be
+ // anti-unified that are replaced with variables
+ private readonly IDictionary<ExprPair, VCExprVar!>! Representation =
+ new Dictionary<ExprPair, VCExprVar!> ();
+
+ private struct ExprPair {
+ public readonly VCExpr! Expr0, Expr1;
+ public ExprPair(VCExpr! expr0, VCExpr! expr1) {
+ Expr0 = expr0;
+ Expr1 = expr1;
+ }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (that is ExprPair) {
+ ExprPair thatPair = (ExprPair)that;
+ return this.Expr0.Equals(thatPair.Expr0) &&
+ this.Expr1.Equals(thatPair.Expr1);
+ }
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Expr0.GetHashCode() + Expr1.GetHashCode() * 13;
+ }
+ }
+
+ public void Reset() {
+ Representation.Clear ();
+ }
+
+ public bool RepresentationIsRenaming(IDictionary<VCExprVar!, VCExprVar!>! globalVars) {
+ if (!forall{KeyValuePair<ExprPair, VCExprVar!> pair in Representation;
+ pair.Key.Expr0 is VCExprVar &&
+ pair.Key.Expr1 is VCExprVar &&
+ !globalVars.ContainsKey((VCExprVar!)pair.Key.Expr0) &&
+ !globalVars.ContainsKey((VCExprVar!)pair.Key.Expr1)})
+ return false;
+ // check that all substituted variables are distinct
+ // TODO: optimise
+ return
+ forall{KeyValuePair<ExprPair, VCExprVar!> pair1 in Representation;
+ forall{KeyValuePair<ExprPair, VCExprVar!> pair2 in Representation;
+ pair1.Value.Equals(pair2.Value) || !pair1.Key.Expr0.Equals(pair2.Key.Expr0)
+ && !pair1.Key.Expr1.Equals(pair2.Key.Expr1)
+ }};
+ }
+
+ public void RepresentationSize(IDictionary<VCExprVar!, VCExprVar!>! globalVars,
+ out int expr0Size, out int expr1Size) {
+ ReprSizeComputingVisitor! size0Visitor = new ReprSizeComputingVisitor ();
+ ReprSizeComputingVisitor! size1Visitor = new ReprSizeComputingVisitor ();
+
+ foreach (KeyValuePair<ExprPair, VCExprVar!> pair in Representation) {
+ size0Visitor.ComputeSize(pair.Key.Expr0, globalVars);
+ size1Visitor.ComputeSize(pair.Key.Expr1, globalVars);
+ }
+
+ expr0Size = size0Visitor.Size;
+ expr1Size = size1Visitor.Size;
+ }
+
+ public VCExpr! AntiUnify(VCExpr! s, VCExpr! t)
+ requires s.Type.Equals(t.Type); {
+ return Traverse(s, t);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private VCExprVar! AbstractWithVariable(VCExpr! s, VCExpr! t)
+ requires s.Type.Equals(t.Type); {
+
+ ExprPair pair = new ExprPair (s, t);
+ VCExprVar repr;
+ if (!Representation.TryGetValue(pair, out repr)) {
+ repr = Gen.Variable("abs" + Representation.Count, s.Type);
+ Representation.Add(pair, repr);
+ }
+ return (!)repr;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprLiteral! node, VCExpr! that) {
+ if (node.Equals(that))
+ return node;
+ return AbstractWithVariable(node, that);
+ }
+
+ public override VCExpr! Visit(VCExprNAry! node, VCExpr! that) {
+ VCExprNAry thatNAry = that as VCExprNAry;
+ if (thatNAry != null && node.Op.Equals(thatNAry.Op)) {
+ // type parameters should already have been eliminated at this
+ // stage
+ assert node.TypeParamArity == 0 && thatNAry.TypeParamArity == 0 &&
+ node.Arity == thatNAry.Arity;
+
+ List<VCExpr!>! unifiedArgs = new List<VCExpr!> ();
+ for (int i = 0; i < node.Arity; ++i)
+ unifiedArgs.Add(Traverse(node[i], thatNAry[i]));
+
+ return Gen.Function(node.Op, unifiedArgs);
+ }
+ return AbstractWithVariable(node, that);
+ }
+
+ public override VCExpr! Visit(VCExprVar! node, VCExpr! that) {
+ if (node.Equals(that))
+ return node;
+ return AbstractWithVariable(node, that);
+ }
+
+ protected override VCExpr! StandardResult(VCExpr! node, VCExpr! that) {
+ assert false; // not handled here
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ internal class ReprSizeComputingVisitor
+ : TraversingVCExprVisitor<bool,
+ // variables considered as global constants
+ IDictionary<VCExprVar!, VCExprVar!>!> {
+
+ public int Size = 0;
+
+ public void ComputeSize(VCExpr! expr,
+ IDictionary<VCExprVar!, VCExprVar!>! globalVars) {
+ Traverse(expr, globalVars);
+ }
+
+ protected override bool StandardResult(VCExpr! node,
+ IDictionary<VCExprVar!, VCExprVar!>! globalVars) {
+ VCExprVar nodeAsVar = node as VCExprVar;
+ if (nodeAsVar == null || globalVars.ContainsKey(nodeAsVar))
+ Size = Size + 1;
+ return true;
+ }
+ }
+}
\ No newline at end of file diff --git a/Source/VCExpr/LetBindingSorter.ssc b/Source/VCExpr/LetBindingSorter.ssc new file mode 100644 index 00000000..96eb0af2 --- /dev/null +++ b/Source/VCExpr/LetBindingSorter.ssc @@ -0,0 +1,135 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+
+// Sort the bindings in a let-expression so that terms bound earlier do
+// not contain variables bound later
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+ // (argument is not used)
+ public class LetBindingSorter : MutatingVCExprVisitor<bool> {
+
+ private readonly FreeVariableCollector! FreeVarCollector =
+ new FreeVariableCollector ();
+
+ private List<VCExprVar!>! FreeVarsIn(VCExpr! expr) {
+ FreeVarCollector.Collect(expr);
+ List<VCExprVar!>! freeVars = new List<VCExprVar!> (FreeVarCollector.FreeTermVars.Keys);
+ FreeVarCollector.Reset();
+ return freeVars;
+ }
+
+ public LetBindingSorter(VCExpressionGenerator! gen) {
+ base(gen);
+ }
+
+ public override VCExpr! Visit(VCExprLet! node, bool arg) {
+ IDictionary<VCExprVar!, Binding!> boundVars =
+ new Dictionary<VCExprVar!, Binding!> ();
+
+ // recurse and collect the free variables in bound terms and formulae
+ foreach (VCExprLetBinding! binding in node) {
+ VCExpr! newE = Mutate(binding.E, arg);
+ Binding! b = new Binding (binding.V, newE, FreeVarsIn(newE));
+ boundVars.Add(b.V, b);
+ }
+
+ // generate the occurrence edges
+ foreach (KeyValuePair<VCExprVar!, Binding!> pair in boundVars) {
+ Binding! b = pair.Value;
+ foreach (VCExprVar! v in b.FreeVars) {
+ Binding b2;
+ if (boundVars.TryGetValue(v, out b2)) {
+ ((!)b2).Occurrences.Add(b);
+ b.InvOccurrencesNum = b.InvOccurrencesNum + 1;
+ }
+ }
+ }
+
+ // topological sort
+ Stack<Binding!> rootBindings = new Stack<Binding!> ();
+ foreach (KeyValuePair<VCExprVar!, Binding!> pair in boundVars)
+ if (pair.Value.InvOccurrencesNum == 0)
+ rootBindings.Push(pair.Value);
+
+ List<Binding!>! sortedBindings = new List<Binding!> ();
+ while (rootBindings.Count > 0) {
+ Binding! b = rootBindings.Pop();
+ sortedBindings.Add(b);
+ foreach (Binding! b2 in b.Occurrences) {
+ b2.InvOccurrencesNum = b2.InvOccurrencesNum - 1;
+ if (b2.InvOccurrencesNum == 0)
+ rootBindings.Push(b2);
+ }
+ }
+
+ if (exists{KeyValuePair<VCExprVar!, Binding!> pair in boundVars;
+ pair.Value.InvOccurrencesNum > 0})
+ System.Diagnostics.Debug.Fail("Cyclic let-bindings");
+
+ assert node.Length == sortedBindings.Count;
+
+ // check which of the bindings can be dropped
+ VCExpr! newBody = Mutate(node.Body, arg);
+
+ IDictionary<VCExprVar!, VCExprVar!>! usedVars =
+ new Dictionary<VCExprVar!, VCExprVar!> ();
+ foreach (VCExprVar! v in FreeVarsIn(newBody))
+ if (!usedVars.ContainsKey(v))
+ usedVars.Add(v, v);
+
+ for (int i = sortedBindings.Count - 1; i >= 0; --i) {
+ if (usedVars.ContainsKey(sortedBindings[i].V)) {
+ foreach (VCExprVar! v in sortedBindings[i].FreeVars)
+ if (!usedVars.ContainsKey(v))
+ usedVars.Add(v, v);
+ } else {
+ sortedBindings.RemoveAt(i);
+ }
+ }
+
+ // assemble the resulting let-expression
+ List<VCExprLetBinding!>! newBindings = new List<VCExprLetBinding!> ();
+ foreach (Binding b in sortedBindings)
+ newBindings.Add(Gen.LetBinding(b.V, b.E));
+
+ return Gen.Let(newBindings, newBody);
+ }
+
+ private class Binding {
+ public readonly VCExprVar! V;
+ public readonly VCExpr! E;
+ public readonly List<VCExprVar!>! FreeVars;
+
+ // list of all bound expression in which the variable V occurs
+ // (outgoing edges)
+ public readonly List<Binding>! Occurrences;
+
+ // number of variables that are bound in this let-expression
+ // and that occur in FreeVars
+ // (incoming edges)
+ public int InvOccurrencesNum;
+
+ public Binding(VCExprVar! v, VCExpr! e, List<VCExprVar!>! freeVars) {
+ this.V = v;
+ this.E = e;
+ this.FreeVars = freeVars;
+ this.Occurrences = new List<Binding> ();
+ this.InvOccurrencesNum = 0;
+ }
+ }
+
+ }
+
+}
diff --git a/Source/VCExpr/NameClashResolver.ssc b/Source/VCExpr/NameClashResolver.ssc new file mode 100644 index 00000000..28a974a6 --- /dev/null +++ b/Source/VCExpr/NameClashResolver.ssc @@ -0,0 +1,129 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+
+// Visitor that establishes unique variable (or constant) names in a VCExpr.
+// This is done by adding a counter as suffix if name clashes occur
+
+// TODO: also handle type variables here
+
+namespace Microsoft.Boogie.VCExprAST {
+ using TEHelperFuns = Microsoft.Boogie.TypeErasure.HelperFuns;
+
+ public class UniqueNamer : ICloneable {
+
+ public UniqueNamer() {
+ GlobalNames = new Dictionary<Object!, string!> ();
+ LocalNames = TEHelperFuns.ToList(new Dictionary<Object!, string!> ()
+ as IDictionary<Object!, string!>);
+ UsedNames = new Dictionary<string!, bool> ();
+ CurrentCounters = new Dictionary<string!, int> ();
+ }
+
+ private UniqueNamer(UniqueNamer! namer) {
+ GlobalNames = new Dictionary<Object!, string!> (namer.GlobalNames);
+
+ List<IDictionary<Object!, string!>!>! localNames =
+ new List<IDictionary<Object!, string!>!> ();
+ LocalNames = localNames;
+
+ foreach (IDictionary<Object!, string!>! d in namer.LocalNames)
+ localNames.Add(new Dictionary<Object!, string!> (d));
+
+ UsedNames = new Dictionary<string!, bool> (namer.UsedNames);
+ CurrentCounters = new Dictionary<string!, int> (namer.CurrentCounters);
+ }
+
+ public Object! Clone() {
+ return new UniqueNamer (this);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private readonly IDictionary<Object!, string!>! GlobalNames;
+ private readonly List<IDictionary<Object!, string!>!>! LocalNames;
+
+ // dictionary of all names that have already been used
+ // (locally or globally)
+ private readonly IDictionary<string!, bool>! UsedNames;
+ private readonly IDictionary<string!, int>! CurrentCounters;
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public void PushScope() {
+ LocalNames.Add(new Dictionary<Object!, string!> ());
+ }
+
+ public void PopScope() {
+ LocalNames.RemoveAt(LocalNames.Count - 1);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private string! NextFreeName(string! baseName) {
+ string! candidate;
+ int counter;
+
+ if (CurrentCounters.TryGetValue(baseName, out counter)) {
+ candidate = baseName + "@@" + counter;
+ counter = counter + 1;
+ } else {
+ candidate = baseName;
+ counter = 0;
+ }
+
+ bool dummy;
+ while (UsedNames.TryGetValue(candidate, out dummy)) {
+ candidate = baseName + "@@" + counter;
+ counter = counter + 1;
+ }
+
+ UsedNames.Add(candidate, true);
+ CurrentCounters[baseName] = counter;
+ return candidate;
+ }
+
+ // retrieve the name of a thingie; if it does not have a name yet,
+ // generate a unique name for it (as close as possible to its inherent
+ // name) and register it globally
+ public string! GetName(Object! thingie, string! inherentName) {
+ string res = this[thingie];
+
+ if (res != null)
+ return res;
+
+ // if the object is not yet registered, create a name for it
+ res = NextFreeName(inherentName);
+ GlobalNames.Add(thingie, res);
+
+ return res;
+ }
+
+ [Pure]
+ public string this[Object! thingie] { get {
+ string res;
+ for (int i = LocalNames.Count - 1; i >= 0; --i) {
+ if (LocalNames[i].TryGetValue(thingie, out res))
+ return res;
+ }
+
+ GlobalNames.TryGetValue(thingie, out res);
+ return res;
+ } }
+
+ public string! GetLocalName(Object! thingie, string! inherentName) {
+ string! res = NextFreeName(inherentName);
+ LocalNames[LocalNames.Count - 1][thingie] = res;
+ return res;
+ }
+ }
+}
diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc new file mode 100644 index 00000000..7aff8e87 --- /dev/null +++ b/Source/VCExpr/SimplifyLikeLineariser.ssc @@ -0,0 +1,795 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+using Microsoft.Boogie.VCExprAST;
+
+// a naive method to turn VCExprs into strings that can be fed into Simplify
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+ // Options for the linearisation. Here one can choose, for instance,
+ // whether Simplify or Z3 output is to be produced
+ public abstract class LineariserOptions {
+
+ public readonly bool AsTerm;
+ public abstract LineariserOptions! SetAsTerm(bool newVal);
+
+ public abstract bool QuantifierIds { get; }
+
+ public virtual bool UseWeights { get { return false; } }
+
+ public virtual bool InverseImplies { get { return false; } }
+
+ // whether to include type specifications in quantifiers
+ public abstract bool UseTypes { get; }
+
+ public virtual CommandLineOptions.BvHandling Bitvectors { get {
+ return CommandLineOptions.BvHandling.None;
+ } }
+
+ // variables representing formulas in let-bindings have to be
+ // printed in a different way than other variables
+ public virtual List<VCExprVar!>! LetVariables { get {
+ return EmptyList;
+ } }
+
+ public virtual LineariserOptions! AddLetVariable(VCExprVar! furtherVar) {
+ return this;
+ }
+
+ private static readonly List<VCExprVar!>! EmptyList = new List<VCExprVar!>();
+
+ public bool NativeBv { get {
+ return Bitvectors == CommandLineOptions.BvHandling.Z3Native;
+ } }
+
+ public bool IntBv { get {
+ return Bitvectors == CommandLineOptions.BvHandling.ToInt;
+ } }
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ protected LineariserOptions(bool asTerm) {
+ this.AsTerm = asTerm;
+ }
+
+ public static readonly LineariserOptions! SimplifyDefault = new SimplifyOptions (false);
+ internal static readonly LineariserOptions! SimplifyDefaultTerm = new SimplifyOptions (true);
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ private class SimplifyOptions : LineariserOptions {
+ internal SimplifyOptions(bool asTerm) {
+ base(asTerm);
+ }
+ public override bool QuantifierIds { get {
+ return false;
+ } }
+ public override bool UseTypes { get {
+ return false;
+ } }
+ public override LineariserOptions! SetAsTerm(bool newVal) {
+ if (newVal)
+ return SimplifyDefaultTerm;
+ else
+ return SimplifyDefault;
+ }
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ // Lineariser for expressions. The result (bool) is currently not used for anything
+ public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {
+
+ public static string! ToSimplifyString(VCExpr! e, UniqueNamer! namer) {
+ StringWriter sw = new StringWriter();
+ SimplifyLikeExprLineariser! lin = new SimplifyLikeExprLineariser (sw, namer);
+ lin.Linearise(e, LineariserOptions.SimplifyDefault);
+ return (!)sw.ToString();
+ }
+
+ public static string! ToString(VCExpr! e, LineariserOptions! options,
+ UniqueNamer! namer) {
+ StringWriter sw = new StringWriter();
+ SimplifyLikeExprLineariser! lin = new SimplifyLikeExprLineariser (sw, namer);
+ lin.Linearise(e, options);
+ return (!)sw.ToString();
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ private readonly TextWriter! wr;
+ private SimplifyLikeOpLineariser OpLinObject = null;
+ private IVCExprOpVisitor<bool, LineariserOptions!>! OpLineariser { get {
+ if (OpLinObject == null)
+ OpLinObject = new SimplifyLikeOpLineariser (this, wr);
+ return OpLinObject;
+ } }
+
+ internal readonly UniqueNamer! Namer;
+
+ public SimplifyLikeExprLineariser(TextWriter! wr, UniqueNamer! namer) {
+ this.wr = wr;
+ this.Namer = namer;
+ }
+
+ public void Linearise(VCExpr! expr, LineariserOptions! options) {
+ expr.Accept<bool, LineariserOptions!>(this, options);
+ }
+
+ public void LineariseAsTerm(VCExpr! expr, LineariserOptions! options) {
+ Linearise(expr, options.SetAsTerm(true));
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public static string! MakeIdPrintable(string! s) {
+ // make sure that no keywords are used as identifiers
+ switch(s) {
+ case andName:
+ case orName:
+ case notName:
+ case impliesName:
+ case iffName:
+ case eqName:
+ case neqName:
+ case distinctName:
+ case TRUEName:
+ case FALSEName:
+ s = "nonkeyword_" + s;
+ break;
+ }
+
+ if (CommandLineOptions.Clo.BracketIdsInVC == 0) {
+ // In this form, we go with any identifier, so we don't ever bother about brackets.
+ // Except: @true and @false are always written with brackets
+ return s;
+ }
+ bool looksLikeOperator = true;
+ bool looksLikeSimpleId = true;
+ bool useBrackets = false;
+ foreach (char ch in s) {
+ switch (ch) {
+ case '=':
+ case '<':
+ case '>':
+ case '+':
+ case '-':
+ case '*':
+ case '/':
+ case '%':
+ case ':':
+ // looks like operator, not simple id
+ looksLikeSimpleId = false;
+ break;
+ default:
+ if (Char.IsLetterOrDigit(ch)) {
+ // looks like simple id, not operator
+ looksLikeOperator = false;
+ } else {
+ // looks like neither operator nor simple id
+ looksLikeOperator = false;
+ looksLikeSimpleId = false;
+ }
+ break;
+ }
+ if (!looksLikeOperator && !looksLikeSimpleId) {
+ useBrackets = true;
+ break;
+ }
+ }
+ if (useBrackets) {
+ return "|" + s + "|";
+ } else {
+ return s;
+ }
+ }
+
+ public static string! TypeToString(Type! t) {
+ if (t.IsBool)
+ return "$bool";
+ else if (t.IsInt)
+ return "$int";
+ else if (t.IsBv)
+ return "$bv" + t.BvBits;
+ else {
+ // at this point, only the types U, T, and bitvector types should be left
+ if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic)
+ return "U";
+ else {
+ System.IO.StringWriter buffer = new System.IO.StringWriter();
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
+ t.Emit(stream);
+ }
+ return buffer.ToString();
+ }
+ }
+ }
+
+ public static string! BvConcatOpName(VCExprNAry! node)
+ requires node.Op.Equals(VCExpressionGenerator.BvConcatOp); {
+ int bits1 = node[0].Type.BvBits;
+ int bits2 = node[1].Type.BvBits;
+ return "$bv" + (bits1 + bits2) + "_concat[" + bits1 + "." + bits2 + "]";
+ }
+
+ public static string! BvExtractOpName(VCExprNAry! node)
+ requires node.Op is VCExprBvExtractOp; {
+ VCExprBvExtractOp! op = (VCExprBvExtractOp)node.Op;
+ return "$bv" + node.Type.BvBits + "_extract[" + op.Start + ":" + op.End + "]";
+ }
+
+ internal void WriteId(string! s) {
+ wr.Write(MakeIdPrintable(s));
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ /// <summary>
+ /// The name for logical conjunction in Simplify
+ /// </summary>
+ internal const string! andName = "AND"; // conjunction
+ internal const string! orName = "OR"; // disjunction
+ internal const string! notName = "NOT"; // negation
+ internal const string! impliesName = "IMPLIES"; // implication
+ internal const string! iffName = "IFF"; // logical equivalence
+ internal const string! eqName = "EQ"; // equality
+ internal const string! neqName = "NEQ"; // inequality
+ internal const string! lessName = "<";
+ internal const string! greaterName = ">";
+ internal const string! atmostName = "<=";
+ internal const string! atleastName = ">=";
+ internal const string! TRUEName = "TRUE"; // nullary predicate that is always true
+ internal const string! FALSEName = "FALSE"; // nullary predicate that is always false
+ internal const string! subtypeName = "<:";
+ internal const string! subtypeArgsName = "<::";
+
+ internal const string! distinctName = "DISTINCT";
+ /// <summary>
+ /// name of the main inclusion relation
+ /// </summary>
+ internal const string! boolTrueName = "|@true|";
+ internal const string! boolFalseName = "|@false|";
+ internal const string! boolAndName = "boolAnd";
+ internal const string! boolOrName = "boolOr";
+ internal const string! boolNotName = "boolNot";
+ internal const string! termEqName = "anyEqual";
+ internal const string! termNeqName = "anyNeq";
+ internal const string! termLessName = "intLess";
+ internal const string! termGreaterName = "intGreater";
+ internal const string! termAtmostName = "intAtMost";
+ internal const string! termAtleastName = "intAtLeast";
+ internal const string! intAddName = "+";
+ internal const string! intAddNameReflect = "Reflect$Add";
+ internal const string! intSubName = "-";
+ internal const string! intMulName = "*";
+ internal const string! intDivName = "/";
+ internal const string! intModName = "%";
+
+ internal void AssertAsTerm(string! x, LineariserOptions! options) {
+ if (!options.AsTerm)
+ System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");
+ }
+
+ internal void AssertAsFormula(string! x, LineariserOptions! options) {
+ if (options.AsTerm)
+ System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprLiteral! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+
+ if (node == VCExpressionGenerator.True)
+ wr.Write(options.UseTypes ? TRUEName : boolTrueName);
+ else if (node == VCExpressionGenerator.False)
+ wr.Write(options.UseTypes ? FALSEName : boolFalseName);
+ else if (node is VCExprIntLit) {
+ wr.Write(((VCExprIntLit)node).Val);
+ } else
+ assert false;
+
+ } else {
+
+ if (node == VCExpressionGenerator.True)
+ wr.Write(TRUEName);
+ else if (node == VCExpressionGenerator.False)
+ wr.Write(FALSEName);
+ else if (node is VCExprIntLit) {
+ System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");
+ } else
+ assert false;
+
+ }
+
+ return true;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprNAry! node, LineariserOptions! options) {
+ VCExprOp! op = node.Op;
+
+ if (!options.AsTerm &&
+ (op.Equals(VCExpressionGenerator.AndOp) ||
+ op.Equals(VCExpressionGenerator.OrOp))) {
+ // handle these operators without recursion
+
+ wr.Write("({0}",
+ op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);
+ IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node);
+ while (enumerator.MoveNext()) {
+ VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ wr.Write(" ");
+ Linearise((VCExpr!)enumerator.Current, options);
+ }
+ }
+
+ wr.Write(")");
+
+ return true;
+ }
+
+ return node.Accept<bool, LineariserOptions!>(OpLineariser, options);
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprVar! node, LineariserOptions! options) {
+ string! printedName = Namer.GetName(node, node.Name);
+
+ if (options.AsTerm ||
+ // variables for formulas bound in a let-binding are never
+ // written as an equation
+ options.LetVariables.Contains(node) ||
+ // if variables are properly typed, they cannot be written as
+ // equation either
+ options.UseTypes) {
+ WriteId(printedName);
+ } else {
+ wr.Write("({0} ", eqName);
+ WriteId(printedName);
+ wr.Write(" {0})", boolTrueName);
+ }
+
+ return true;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprQuantifier! node, LineariserOptions! options) {
+ AssertAsFormula(node.Quan.ToString(), options);
+ assert node.TypeParameters.Count == 0;
+
+ Namer.PushScope(); try {
+
+ string! kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";
+ wr.Write("({0} (", kind);
+
+ for (int i = 0; i < node.BoundVars.Count; i++)
+ {
+ VCExprVar! var = node.BoundVars[i];
+ string! printedName = Namer.GetLocalName(var, var.Name);
+ if (i != 0)
+ wr.Write(" ");
+ WriteId(printedName);
+ if (options.UseTypes)
+ wr.Write(" :TYPE {0}", TypeToString(var.Type));
+ }
+ wr.Write(") ");
+
+ WriteTriggers(node.Triggers, options);
+
+ if (options.QuantifierIds) {
+ // only needed for Z3
+ VCQuantifierInfos! infos = node.Infos;
+ if (infos.qid != null) {
+ wr.Write("(QID ");
+ wr.Write(infos.qid);
+ wr.Write(") ");
+ }
+ if (0 <= infos.uniqueId) {
+ wr.Write("(SKOLEMID ");
+ wr.Write(infos.uniqueId);
+ wr.Write(") ");
+ }
+ }
+
+ if (options.UseWeights) {
+ int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);
+ if (weight != 1) {
+ wr.Write("(WEIGHT ");
+ wr.Write(weight);
+ wr.Write(") ");
+ }
+ }
+
+ Linearise(node.Body, options);
+ wr.Write(")");
+
+ return true;
+
+ } finally {
+ Namer.PopScope();
+ }
+ }
+
+ private void WriteTriggers(List<VCTrigger!>! triggers, LineariserOptions! options) {
+ // first, count how many neg/pos triggers there are
+ int negTriggers = 0;
+ int posTriggers = 0;
+ foreach (VCTrigger! vcTrig in triggers) {
+ if (vcTrig.Pos) {
+ posTriggers++;
+ } else {
+ negTriggers++;
+ }
+ }
+
+ if (posTriggers > 0) {
+ wr.Write("(PATS");
+ foreach (VCTrigger! vcTrig in triggers) {
+ if (vcTrig.Pos) {
+ if (vcTrig.Exprs.Count > 1) {
+ wr.Write(" (MPAT");
+ }
+ foreach (VCExpr! e in vcTrig.Exprs) {
+ wr.Write(" ");
+ LineariseAsTerm(e, options);
+ }
+ if (vcTrig.Exprs.Count > 1) {
+ wr.Write(")");
+ }
+ }
+ }
+ wr.Write(") ");
+ } else if (negTriggers > 0) {
+ // if also positive triggers are given, the SMT solver (at least Z3)
+ // will ignore the negative patterns and output a warning. Therefore
+ // we never specify both negative and positive triggers
+ wr.Write("(NOPATS");
+ foreach (VCTrigger! vcTrig in triggers) {
+ if (!vcTrig.Pos) {
+ wr.Write(" ");
+ assert vcTrig.Exprs.Count == 1;
+ LineariseAsTerm(vcTrig.Exprs[0], options);
+ }
+ }
+ wr.Write(") ");
+ }
+
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprLet! node, LineariserOptions! options) {
+ Namer.PushScope(); try {
+
+ wr.Write("(LET (");
+
+ LineariserOptions! optionsWithVars = options;
+ foreach (VCExprVar! var in node.BoundVars)
+ optionsWithVars = optionsWithVars.AddLetVariable(var);
+
+ string s = "(";
+ foreach (VCExprLetBinding! b in node) {
+ wr.Write(s);
+ string! printedName = Namer.GetLocalName(b.V, b.V.Name);
+
+ bool formula = b.V.Type.IsBool;
+ if (formula)
+ wr.Write("FORMULA ");
+ else
+ wr.Write("TERM ");
+ WriteId(printedName);
+ wr.Write(" ");
+ Linearise(b.E, optionsWithVars.SetAsTerm(!formula));
+ wr.Write(")");
+ s = " (";
+ }
+ wr.Write(") ");
+ Linearise(node.Body, optionsWithVars);
+ wr.Write(")");
+
+ return true;
+
+ } finally {
+ Namer.PopScope();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ // Lineariser for operator terms. The result (bool) is currently not used for anything
+ internal class SimplifyLikeOpLineariser : IVCExprOpVisitor<bool, LineariserOptions!> {
+ private readonly SimplifyLikeExprLineariser! ExprLineariser;
+ private readonly TextWriter! wr;
+
+ public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser! ExprLineariser, TextWriter! wr) {
+ this.ExprLineariser = ExprLineariser;
+ this.wr = wr;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options,
+ bool argsAsTerms) {
+ WriteApplication(op, op, args, options, argsAsTerms);
+ }
+
+ private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options) {
+ WriteApplication(op, op, args, options, options.AsTerm);
+ }
+
+ private void WriteTermApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options) {
+ ExprLineariser.AssertAsTerm(op, options);
+ WriteApplication(op, op, args, options, options.AsTerm);
+ }
+
+ private void WriteApplication(string! termOp, string! predOp,
+ IEnumerable<VCExpr!>! args, LineariserOptions! options) {
+ WriteApplication(termOp, predOp, args, options, options.AsTerm);
+ }
+
+ private void WriteApplication(string! termOp, string! predOp,
+ IEnumerable<VCExpr!>! args, LineariserOptions! options,
+ // change the AsTerm option for the arguments?
+ bool argsAsTerms) {
+ wr.Write("({0}", options.AsTerm ? termOp : predOp);
+
+ LineariserOptions! newOptions = options.SetAsTerm(argsAsTerms);
+ foreach (VCExpr! e in args) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, newOptions);
+ }
+
+ wr.Write(")");
+ }
+
+ // write an application that can only be a term.
+ // if the expression is supposed to be printed as a formula,
+ // it is turned into an equation (EQ (f args) |@true|)
+ private void WriteApplicationTermOnly(string! termOp,
+ IEnumerable<VCExpr!>! args, LineariserOptions! options) {
+ if (!options.AsTerm)
+ // Write: (EQ (f args) |@true|)
+ // where "args" are written as terms
+ wr.Write("({0} ", eqName);
+
+ WriteApplication(termOp, args, options, true);
+
+ if (!options.AsTerm)
+ wr.Write(" {0})", boolTrueName);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public bool VisitNotOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(boolNotName, notName, node, options); // arguments can be both terms and formulas
+ return true;
+ }
+
+ public bool VisitEqOp (VCExprNAry! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+ // use equality on terms, also if the arguments have type bool
+ WriteApplication(termEqName, node, options);
+ } else {
+ if (node[0].Type.IsBool) {
+ assert node[1].Type.IsBool;
+ // use equivalence
+ WriteApplication(iffName, node, options);
+ } else {
+ assert !node[1].Type.IsBool;
+ // use equality and write the arguments as terms
+ WriteApplication(eqName, node, options, true);
+ }
+ }
+
+ return true;
+ }
+
+ public bool VisitNeqOp (VCExprNAry! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+ // use equality on terms, also if the arguments have type bool
+ WriteApplication(termNeqName, node, options);
+ } else {
+ if (node[0].Type.IsBool) {
+ assert node[1].Type.IsBool;
+ // use equivalence and negate the whole thing
+ wr.Write("({0} ", notName);
+ WriteApplication(iffName, node, options);
+ wr.Write(")");
+ } else {
+ // use equality and write the arguments as terms
+ WriteApplication(neqName, node, options, true);
+ }
+ }
+
+ return true;
+ }
+
+ public bool VisitAndOp (VCExprNAry! node, LineariserOptions! options) {
+ assert options.AsTerm;
+ WriteApplication(boolAndName, andName, node, options); // arguments can be both terms and formulas
+ return true;
+ }
+
+ public bool VisitOrOp (VCExprNAry! node, LineariserOptions! options) {
+ assert options.AsTerm;
+ WriteApplication(boolOrName, orName, node, options); // arguments can be both terms and formulas
+ return true;
+ }
+
+ public bool VisitImpliesOp (VCExprNAry! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+ wr.Write("({0} ({1} ", boolOrName, boolNotName);
+ ExprLineariser.Linearise(node[0], options);
+ wr.Write(") ");
+ ExprLineariser.Linearise(node[1], options);
+ wr.Write(")");
+ } else if (options.InverseImplies) {
+ wr.Write("({0} ", orName);
+ ExprLineariser.Linearise(node[1], options);
+ wr.Write(" ({0} ", notName);
+ ExprLineariser.Linearise(node[0], options);
+ wr.Write("))");
+ } else {
+ WriteApplication(impliesName, node, options);
+ }
+ return true;
+ }
+
+ public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) {
+ ExprLineariser.AssertAsFormula(distinctName, options);
+
+ if (node.Length < 2) {
+ ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+ } else {
+ wr.Write("({0}", distinctName);
+ foreach (VCExpr! e in node) {
+ wr.Write(" ");
+ ExprLineariser.LineariseAsTerm(e, options);
+ }
+ wr.Write(")");
+ }
+
+ return true;
+ }
+
+ public bool VisitLabelOp (VCExprNAry! node, LineariserOptions! options) {
+ VCExprLabelOp! op = (VCExprLabelOp)node.Op;
+ wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));
+ ExprLineariser.Linearise(node[0], options); wr.Write(")");
+ return true;
+ }
+
+ public bool VisitSelectOp (VCExprNAry! node, LineariserOptions! options) {
+ assert false; // should not occur in the output
+ }
+
+ public bool VisitStoreOp (VCExprNAry! node, LineariserOptions! options) {
+ assert false; // should not occur in the output
+ }
+
+ public bool VisitBvOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);
+ return true;
+ }
+
+ public bool VisitBvExtractOp(VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(BvExtractOpName(node), node, options);
+ return true;
+ }
+
+ public bool VisitBvConcatOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(BvConcatOpName(node), node, options);
+ return true;
+ }
+
+ public bool VisitAddOp (VCExprNAry! node, LineariserOptions! options) {
+ if (CommandLineOptions.Clo.ReflectAdd) {
+ WriteTermApplication(intAddNameReflect, node, options);
+ } else {
+ WriteTermApplication(intAddName, node, options);
+ }
+ return true;
+ }
+
+ public bool VisitSubOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intSubName, node, options);
+ return true;
+ }
+
+ public bool VisitMulOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intMulName, node, options);
+ return true;
+ }
+
+ public bool VisitDivOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intDivName, node, options);
+ return true;
+ }
+
+ public bool VisitModOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(intModName, node, options);
+ return true;
+ }
+
+ public bool VisitLtOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(termLessName, lessName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitLeOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(termAtmostName, atmostName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitGtOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(termGreaterName, greaterName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitGeOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(termAtleastName, atleastName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitSubtypeOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(subtypeName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitSubtype3Op (VCExprNAry! node, LineariserOptions! options) {
+ WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitBoogieFunctionOp (VCExprNAry! node, LineariserOptions! options) {
+ VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op;
+ string! funcName = op.Func.Name;
+ string? bvzName = op.Func.FindStringAttribute("external");
+ string! printedName = ExprLineariser.Namer.GetName(op.Func, funcName);
+ if (bvzName != null) printedName = bvzName;
+
+ if (options.UseTypes) {
+ // we use term notation for arguments whose type is not bool, and
+ // formula notation for boolean arguments
+
+ wr.Write("(");
+ ExprLineariser.WriteId(printedName);
+
+ foreach (VCExpr! e in node) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
+ }
+
+ wr.Write(")");
+ } else {
+ // arguments are always terms
+ WriteApplicationTermOnly(SimplifyLikeExprLineariser.MakeIdPrintable(printedName),
+ node, options);
+ }
+ return true;
+ }
+
+ }
+ }
+
+}
diff --git a/Source/VCExpr/TermFormulaFlattening.ssc b/Source/VCExpr/TermFormulaFlattening.ssc new file mode 100644 index 00000000..bfb8cb3a --- /dev/null +++ b/Source/VCExpr/TermFormulaFlattening.ssc @@ -0,0 +1,222 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+using Microsoft.Boogie.VCExprAST;
+
+// Ensure that no formulas (expressions of type boolean that are not
+// just a variable) occur with terms (expressions of some other
+// type). This is done by introducing let-binders for boolean
+// variables.
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+ public struct FlattenerState {
+ public readonly int Polarity;
+ public readonly bool InTerm;
+
+ public static FlattenerState INITIAL = new FlattenerState(1, false);
+
+ public FlattenerState(int polarity, bool inTerm) {
+ Polarity = polarity;
+ InTerm = inTerm;
+ }
+
+ public FlattenerState TogglePolarity { get {
+ return new FlattenerState(-Polarity, InTerm);
+ } }
+
+ public FlattenerState ZeroPolarity { get {
+ return new FlattenerState(0, InTerm);
+ } }
+
+ public FlattenerState EnterTerm { get {
+ return new FlattenerState(Polarity, true);
+ } }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ public class TermFormulaFlattener : MutatingVCExprVisitor<FlattenerState> {
+
+ public TermFormulaFlattener(VCExpressionGenerator! gen) {
+ base(gen);
+ }
+
+ private readonly IDictionary<VCExpr!, VCExprVar!>! Bindings =
+ new Dictionary<VCExpr!, VCExprVar!> ();
+
+ private int varNameCounter = 0;
+
+ public VCExpr! Flatten(VCExpr! expr) {
+ VCExpr! res = Mutate(expr, FlattenerState.INITIAL);
+ while (Bindings.Count > 0) {
+ List<VCExprLetBinding!>! letBindings = new List<VCExprLetBinding!> ();
+ foreach (KeyValuePair<VCExpr!, VCExprVar!> pair in Bindings)
+ letBindings.Add(Gen.LetBinding(pair.Value, pair.Key));
+ Bindings.Clear();
+ res = AddBindings(letBindings, res, FlattenerState.INITIAL);
+ }
+ return res;
+ }
+
+ private VCExprVar! GetVarFor(VCExpr! expr) requires expr.Type.IsBool; {
+ VCExprVar res;
+ if (!Bindings.TryGetValue(expr, out res)) {
+ string! name = "flt" + varNameCounter;
+ varNameCounter = varNameCounter + 1;
+ res = Gen.Variable(name, Type.Bool);
+ Bindings.Add(expr, res);
+ }
+ return (!)res;
+ }
+
+ // Remove all let-bindings from the field bindings whose rhs
+ // contains any of the specified variables
+ private List<VCExprLetBinding!>!
+ RemoveBindingsWithVars(List<VCExprVar!>! boundVars,
+ List<TypeVariable!>! boundTypeVars) {
+
+ List<VCExprLetBinding!>! res = new List<VCExprLetBinding!> ();
+ FreeVariableCollector! coll = new FreeVariableCollector ();
+
+ foreach (KeyValuePair<VCExpr!, VCExprVar!> pair in Bindings) {
+ coll.Collect(pair.Key);
+ if (exists{VCExprVar! var in boundVars; coll.FreeTermVars.ContainsKey(var)} ||
+ exists{TypeVariable! var in boundTypeVars; coll.FreeTypeVars.Contains(var)})
+ res.Add(Gen.LetBinding(pair.Value, pair.Key));
+ coll.Reset();
+ }
+
+ foreach (VCExprLetBinding! b in res)
+ Bindings.Remove(b.E);
+
+ return res;
+ }
+
+ // Add bindings to a formula using an implication or
+ // conjunction. The bindings themselves will be flattened as well,
+ // which might introduce further bindings
+ private VCExpr! AddBindings(List<VCExprLetBinding!>! bindings,
+ VCExpr! body,
+ FlattenerState state)
+ requires body.Type.IsBool; {
+
+ List<VCExprLetBinding!>! mutatedBindings = FlattenBindings(bindings, state);
+ VCExpr! bindingEquations = Gen.AsEquations(mutatedBindings);
+ switch(state.Polarity) {
+ case 1:
+ return Gen.Implies(bindingEquations, body);
+ case -1:
+ return Gen.And(bindingEquations, body);
+ case 0:
+ // also add explicit quantifiers for the bound variables
+ List<VCExprVar!>! vars = new List<VCExprVar!> ();
+ foreach (VCExprLetBinding! binding in mutatedBindings)
+ vars.Add(binding.V);
+ return Gen.Forall(vars, new List<VCTrigger!>(),
+ Gen.Implies(bindingEquations, body));
+ }
+ assert false;
+ }
+
+ private List<VCExprLetBinding!>! FlattenBindings(List<VCExprLetBinding!>! bindings,
+ FlattenerState state) {
+ FlattenerState stateInBindings = state.ZeroPolarity;
+ List<VCExprLetBinding!>! mutatedBindings = new List<VCExprLetBinding!> ();
+ foreach (VCExprLetBinding! b in bindings)
+ mutatedBindings.Add(Gen.LetBinding(b.V, Mutate(b.E, stateInBindings)));
+ return mutatedBindings;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprNAry! node, FlattenerState state) {
+ // track the polarity to know whether implications or conjunctions
+ // are to be introduced
+
+ if (node.Op.Equals(VCExpressionGenerator.NotOp))
+ return Gen.Not(Mutate(node[0], state.TogglePolarity));
+
+ if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) {
+ VCExpr! newArg0 = Mutate(node[0], state.TogglePolarity);
+ VCExpr! newArg1 = Mutate(node[1], state);
+ return Gen.Implies(newArg0, newArg1);
+ }
+
+ if (!node.Type.IsBool)
+ state = state.EnterTerm;
+
+ if (!node.Op.Equals(VCExpressionGenerator.AndOp) &&
+ !node.Op.Equals(VCExpressionGenerator.OrOp) &&
+ !(node.Op is VCExprLabelOp))
+ // standard is to set the polarity to 0 (fits most operators)
+ return base.Visit(node, state.ZeroPolarity);
+
+ return base.Visit(node, state);
+ }
+
+ public override VCExpr! Visit(VCExprQuantifier! node, FlattenerState state) {
+ if (state.InTerm)
+ return GetVarFor(node);
+
+ // we only flatten within the matrix of the quantified formula,
+ // not within the triggers (since SMT-solvers do not seem to
+ // appreciate triggers with let-binders)
+ VCExpr! newBody = Mutate(node.Body, state);
+
+ // Check whether any of the extracted terms contain variables
+ // bound by this quantifier. In this case, we have to add
+ // let-binders and remove the extracted terms
+ bool cont = true;
+ while (cont) {
+ List<VCExprLetBinding!>! localBindings =
+ RemoveBindingsWithVars(node.BoundVars, node.TypeParameters);
+ if (localBindings.Count > 0)
+ newBody = AddBindings(localBindings, newBody, state);
+ else
+ cont = false;
+ }
+
+ return Gen.Quantify(node.Quan, node.TypeParameters,
+ node.BoundVars, node.Triggers,
+ node.Infos, newBody);
+ }
+
+ public override VCExpr! Visit(VCExprLet! node, FlattenerState state) {
+ if (state.InTerm)
+ return GetVarFor(node);
+
+ VCExprLet! prelimRes = (VCExprLet!)base.Visit(node, state);
+
+ List<VCExprLetBinding!>! allBindings = new List<VCExprLetBinding!> ();
+ allBindings.AddRange(prelimRes);
+
+ // Check whether any of the extracted terms contain variables
+ // bound by this binder. In this case, we have to add
+ // let-binders and remove the extracted terms
+ bool cont = true;
+ while (cont) {
+ List<VCExprLetBinding!>! localBindings =
+ RemoveBindingsWithVars(prelimRes.BoundVars, new List<TypeVariable!> ());
+ if (localBindings.Count > 0)
+ allBindings.AddRange(FlattenBindings(localBindings, state));
+ else
+ cont = false;
+ }
+
+ return Gen.Let(allBindings, prelimRes.Body);
+ }
+
+ }
+
+}
\ No newline at end of file diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc new file mode 100644 index 00000000..9cbd829a --- /dev/null +++ b/Source/VCExpr/TypeErasure.ssc @@ -0,0 +1,1160 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+using Microsoft.Boogie.VCExprAST;
+
+// different classes for erasing complex types in VCExprs, replacing them
+// with axioms that can be handled by theorem provers and SMT solvers
+
+namespace Microsoft.Boogie.TypeErasure
+{
+ using Microsoft.Boogie.VCExprAST;
+
+ // some functionality that is needed in many places (and that should
+ // really be provided by the Spec# container classes; maybe one
+ // could integrate the functions in a nicer way?)
+ public class HelperFuns {
+
+ public static Function! BoogieFunction(string! name, List<TypeVariable!>! typeParams,
+ params Type[]! types)
+ requires types.Length > 0;
+ requires forall{int i in (0:types.Length); types[i] != null};
+ {
+ VariableSeq! args = new VariableSeq ();
+ for (int i = 0; i < types.Length - 1; ++i)
+ args.Add(new Formal (Token.NoToken,
+ new TypedIdent (Token.NoToken, "arg" + i, (!)types[i]),
+ true));
+ Formal! result = new Formal (Token.NoToken,
+ new TypedIdent (Token.NoToken, "res",
+ (!)types[types.Length - 1]),
+ false);
+ return new Function (Token.NoToken, name, ToSeq(typeParams), args, result);
+ }
+
+ public static Function! BoogieFunction(string! name, params Type[]! types) {
+ return BoogieFunction(name, new List<TypeVariable!> (), types);
+ }
+
+ // boogie function where all arguments and the result have the same type U
+ public static Function! UniformBoogieFunction(string! name, int arity, Type! U) {
+ Type[]! types = new Type [arity + 1];
+ for (int i = 0; i < arity + 1; ++i)
+ types[i] = U;
+ return BoogieFunction(name, types);
+ }
+
+ public static List<VCExprVar!>! GenVarsForInParams(Function! fun,
+ VCExpressionGenerator! gen) {
+ List<VCExprVar!>! arguments = new List<VCExprVar!> (fun.InParams.Length);
+ foreach (Formal! f in fun.InParams) {
+ VCExprVar! var = gen.Variable(f.Name, f.TypedIdent.Type);
+ arguments.Add(var);
+ }
+ return arguments;
+ }
+
+ public static List<T!>! ToList<T> (params T[]! args) {
+ List<T!>! res = new List<T!> (args.Length);
+ foreach (T t in args)
+ res.Add((!)t);
+ return res;
+ }
+
+ public static List<TypeVariable!>! ToList(TypeVariableSeq! seq) {
+ List<TypeVariable!>! res = new List<TypeVariable!> (seq.Length);
+ foreach (TypeVariable! var in seq)
+ res.Add(var);
+ return res;
+ }
+
+ public static TypeVariableSeq! ToSeq(List<TypeVariable!>! list) {
+ TypeVariableSeq! res = new TypeVariableSeq ();
+ foreach (TypeVariable! var in list)
+ res.Add(var);
+ return res;
+ }
+
+ public static List<T>! Intersect<T>(List<T>! a, List<T>! b) {
+ List<T>! res = new List<T> (Math.Min(a.Count, b.Count));
+ foreach (T x in a)
+ if (b.Contains(x))
+ res.Add(x);
+ res.TrimExcess();
+ return res;
+ }
+
+ public static List<KeyValuePair<T1, T2>>! ToPairList<T1, T2>(IDictionary<T1, T2>! dict) {
+ List<KeyValuePair<T1, T2>>! res = new List<KeyValuePair<T1, T2>> (dict);
+ return res;
+ }
+
+ public static void AddRangeWithoutDups<T>(IEnumerable<T>! fromList, List<T>! toList) {
+ foreach (T t in fromList)
+ if (!toList.Contains(t))
+ toList.Add(t);
+ }
+
+ public static void AddFreeVariablesWithoutDups(Type! type, List<TypeVariable!>! toList) {
+ foreach (TypeVariable! var in type.FreeVariables) {
+ if (!toList.Contains(var))
+ toList.Add(var);
+ }
+ }
+
+ public static List<VCExpr!>! ToVCExprList(List<VCExprVar!>! list) {
+ List<VCExpr!>! res = new List<VCExpr!> (list.Count);
+ foreach (VCExprVar! var in list)
+ res.Add(var);
+ return res;
+ }
+
+ public static List<VCExprVar!>! VarVector(string! baseName, int num, Type! type,
+ VCExpressionGenerator! gen) {
+ List<VCExprVar!>! res = new List<VCExprVar!> (num);
+ for (int i = 0; i < num; ++i)
+ res.Add(gen.Variable(baseName + i, type));
+ return res;
+ }
+
+ public static List<VCExprVar!>! VarVector(string! baseName, List<Type!>! types,
+ VCExpressionGenerator! gen) {
+ List<VCExprVar!>! res = new List<VCExprVar!> (types.Count);
+ for (int i = 0; i < types.Count; ++i)
+ res.Add(gen.Variable(baseName + i, types[i]));
+ return res;
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ internal struct TypeCtorRepr {
+ // function that represents the application of the type constructor
+ // to smaller types
+ public readonly Function! Ctor;
+ // left-inverse functions that extract the subtypes of a compound type
+ public readonly List<Function!>! Dtors;
+
+ public TypeCtorRepr(Function! ctor, List<Function!>! dtors)
+ requires ctor.InParams.Length == dtors.Count; {
+ this.Ctor = ctor;
+ this.Dtors = dtors;
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ // The class responsible for creating and keeping track of all
+ // axioms related to the type system. This abstract class is made
+ // concrete in two subclasses, one for type erasure with type
+ // premisses in quantifiers (the semantic approach), and one for
+ // type erasure with explicit type arguments of polymorphic
+ // functions (the syntacted approach).
+ public abstract class TypeAxiomBuilder : ICloneable {
+
+ protected readonly VCExpressionGenerator! Gen;
+
+ internal abstract MapTypeAbstractionBuilder! MapTypeAbstracter { get; }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Type Axioms
+
+ // list in which all typed axioms are collected
+ private readonly List<VCExpr!>! AllTypeAxioms;
+
+ // list in which type axioms are incrementally collected
+ private readonly List<VCExpr!>! IncTypeAxioms;
+
+ internal void AddTypeAxiom(VCExpr! axiom) {
+ AllTypeAxioms.Add(axiom);
+ IncTypeAxioms.Add(axiom);
+ }
+
+ // Return all axioms that were added since the last time NewAxioms
+ // was called
+ public VCExpr! GetNewAxioms() {
+ VCExpr! res = Gen.NAry(VCExpressionGenerator.AndOp, IncTypeAxioms);
+ IncTypeAxioms.Clear();
+ return res;
+ }
+
+ // mapping from a type to its constructor number/index
+ private readonly Function! Ctor;
+ private BigNum CurrentCtorNum;
+
+ private VCExpr! GenCtorAssignment(VCExpr! typeRepr) {
+ if (CommandLineOptions.Clo.TypeEncodingMethod
+ == CommandLineOptions.TypeEncoding.None)
+ return VCExpressionGenerator.True;
+
+ VCExpr! res = Gen.Eq(Gen.Function(Ctor, typeRepr),
+ Gen.Integer(CurrentCtorNum));
+ CurrentCtorNum = CurrentCtorNum + BigNum.ONE;
+ return res;
+ }
+
+ private VCExpr! GenCtorAssignment(Function! typeRepr) {
+ if (CommandLineOptions.Clo.TypeEncodingMethod
+ == CommandLineOptions.TypeEncoding.None)
+ return VCExpressionGenerator.True;
+
+ List<VCExprVar!>! quantifiedVars = HelperFuns.GenVarsForInParams(typeRepr, Gen);
+ VCExpr! eq =
+ GenCtorAssignment(Gen.Function(typeRepr,
+ HelperFuns.ToVCExprList(quantifiedVars)));
+
+ if (typeRepr.InParams.Length == 0)
+ return eq;
+
+ return Gen.Forall(quantifiedVars, new List<VCTrigger!> (),
+ "ctor:" + typeRepr.Name, eq);
+ }
+
+ // generate an axiom (forall x0, x1, ... :: invFun(fun(x0, x1, ...) == xi)
+ protected VCExpr! GenLeftInverseAxiom(Function! fun, Function! invFun, int dtorNum) {
+ List<VCExprVar!>! quantifiedVars = HelperFuns.GenVarsForInParams(fun, Gen);
+
+ VCExpr! funApp = Gen.Function(fun, HelperFuns.ToVCExprList(quantifiedVars));
+ VCExpr! lhs = Gen.Function(invFun, funApp);
+ VCExpr! rhs = quantifiedVars[dtorNum];
+ VCExpr! eq = Gen.Eq(lhs, rhs);
+
+ List<VCTrigger!>! triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
+ return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, eq);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ // the type of everything that is not int, bool, or a type
+ private readonly TypeCtorDecl! UDecl;
+ public readonly Type! U;
+
+ // the type of types
+ private readonly TypeCtorDecl! TDecl;
+ public readonly Type! T;
+
+ public abstract Type! TypeAfterErasure(Type! type);
+ public abstract bool UnchangedType(Type! type);
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Symbols for representing types
+
+ private readonly IDictionary<Type!, VCExpr!>! BasicTypeReprs;
+
+ private VCExpr! GetBasicTypeRepr(Type! type)
+ requires type.IsBasic || type.IsBv; {
+ VCExpr res;
+ if (!BasicTypeReprs.TryGetValue(type, out res)) {
+ res = Gen.Function(HelperFuns.BoogieFunction(type.ToString() + "Type", T));
+ AddTypeAxiom(GenCtorAssignment(res));
+ BasicTypeReprs.Add(type, res);
+ }
+ return (!)res;
+ }
+
+ private readonly IDictionary<TypeCtorDecl!, TypeCtorRepr>! TypeCtorReprs;
+
+ internal TypeCtorRepr GetTypeCtorReprStruct(TypeCtorDecl! decl) {
+ TypeCtorRepr reprSet;
+ if (!TypeCtorReprs.TryGetValue(decl, out reprSet)) {
+ Function! ctor = HelperFuns.UniformBoogieFunction(decl.Name + "Type", decl.Arity, T);
+ AddTypeAxiom(GenCtorAssignment(ctor));
+
+ List<Function!>! dtors = new List<Function!>(decl.Arity);
+ for (int i = 0; i < decl.Arity; ++i) {
+ Function! dtor = HelperFuns.UniformBoogieFunction(decl.Name + "TypeInv" + i, 1, T);
+ dtors.Add(dtor);
+ AddTypeAxiom(GenLeftInverseAxiom(ctor, dtor, i));
+ }
+
+ reprSet = new TypeCtorRepr(ctor, dtors);
+ TypeCtorReprs.Add(decl, reprSet);
+ }
+
+ return reprSet;
+ }
+
+ public Function! GetTypeCtorRepr(TypeCtorDecl! decl) {
+ return GetTypeCtorReprStruct(decl).Ctor;
+ }
+
+ public Function! GetTypeDtor(TypeCtorDecl! decl, int num) {
+ return GetTypeCtorReprStruct(decl).Dtors[num];
+ }
+
+ // mapping from free type variables to VCExpr variables
+ private readonly IDictionary<TypeVariable!, VCExprVar!>! TypeVariableMapping;
+
+ public VCExprVar! Typed2Untyped(TypeVariable! var) {
+ VCExprVar res;
+ if (!TypeVariableMapping.TryGetValue(var, out res)) {
+ res = new VCExprVar (var.Name, T);
+ TypeVariableMapping.Add(var, res);
+ }
+ return (!)res;
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Symbols for representing variables and constants
+
+ // Globally defined variables
+ private readonly IDictionary<VCExprVar!, VCExprVar!>! Typed2UntypedVariables;
+
+ // This method must only be used for free (unbound) variables
+ public VCExprVar! Typed2Untyped(VCExprVar! var) {
+ VCExprVar res;
+ if (!Typed2UntypedVariables.TryGetValue(var, out res)) {
+ res = Gen.Variable(var.Name, TypeAfterErasure(var.Type));
+ Typed2UntypedVariables.Add(var, res);
+ AddVarTypeAxiom(res, var.Type);
+ }
+ return (!)res;
+ }
+
+ protected abstract void AddVarTypeAxiom(VCExprVar! var, Type! originalType);
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Translation function from types to their term representation
+
+ public VCExpr! Type2Term(Type! type,
+ IDictionary<TypeVariable!, VCExpr!>! varMapping) {
+ //
+ if (type.IsBasic || type.IsBv) {
+ //
+ return GetBasicTypeRepr(type);
+ //
+ } else if (type.IsCtor) {
+ //
+ CtorType ctype = type.AsCtor;
+ Function! repr = GetTypeCtorRepr(ctype.Decl);
+ List<VCExpr!>! args = new List<VCExpr!> (ctype.Arguments.Length);
+ foreach (Type! t in ctype.Arguments)
+ args.Add(Type2Term(t, varMapping));
+ return Gen.Function(repr, args);
+ //
+ } else if (type.IsVariable) {
+ //
+ VCExpr res;
+ if (!varMapping.TryGetValue(type.AsVariable, out res))
+ // then the variable is free and we bind it at this point to a term
+ // variable
+ res = Typed2Untyped(type.AsVariable);
+ return (!)res;
+ //
+ } else if (type.IsMap) {
+ //
+ return Type2Term(MapTypeAbstracter.AbstractMapType(type.AsMap), varMapping);
+ //
+ } else {
+ System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + type);
+ assert false; // please the compiler
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public TypeAxiomBuilder(VCExpressionGenerator! gen) {
+ this.Gen = gen;
+ AllTypeAxioms = new List<VCExpr!> ();
+ IncTypeAxioms = new List<VCExpr!> ();
+ BasicTypeReprs = new Dictionary<Type!, VCExpr!> ();
+ CurrentCtorNum = BigNum.ZERO;
+ TypeCtorReprs = new Dictionary<TypeCtorDecl!, TypeCtorRepr> ();
+ TypeVariableMapping = new Dictionary<TypeVariable!, VCExprVar!> ();
+ Typed2UntypedVariables = new Dictionary<VCExprVar!, VCExprVar!> ();
+
+ TypeCtorDecl! uDecl = new TypeCtorDecl(Token.NoToken, "U", 0);
+ UDecl = uDecl;
+ Type! u = new CtorType (Token.NoToken, uDecl, new TypeSeq ());
+ U = u;
+
+ TypeCtorDecl! tDecl = new TypeCtorDecl(Token.NoToken, "T", 0);
+ TDecl = tDecl;
+ Type! t = new CtorType (Token.NoToken, tDecl, new TypeSeq ());
+ T = t;
+
+ Ctor = HelperFuns.BoogieFunction("Ctor", t, Type.Int);
+ }
+
+ public virtual void Setup() {
+ GetBasicTypeRepr(Type.Int);
+ GetBasicTypeRepr(Type.Bool);
+ }
+
+ // constructor to allow cloning
+ internal TypeAxiomBuilder(TypeAxiomBuilder! builder) {
+ Gen = builder.Gen;
+ AllTypeAxioms = new List<VCExpr!> (builder.AllTypeAxioms);
+ IncTypeAxioms = new List<VCExpr!> (builder.IncTypeAxioms);
+
+ UDecl = builder.UDecl;
+ U = builder.U;
+
+ TDecl = builder.TDecl;
+ T = builder.T;
+
+ Ctor = builder.Ctor;
+ CurrentCtorNum = builder.CurrentCtorNum;
+
+ BasicTypeReprs = new Dictionary<Type!, VCExpr!> (builder.BasicTypeReprs);
+ TypeCtorReprs = new Dictionary<TypeCtorDecl!, TypeCtorRepr> (builder.TypeCtorReprs);
+
+ TypeVariableMapping =
+ new Dictionary<TypeVariable!, VCExprVar!> (builder.TypeVariableMapping);
+ Typed2UntypedVariables =
+ new Dictionary<VCExprVar!, VCExprVar!> (builder.Typed2UntypedVariables);
+ }
+
+ public abstract Object! Clone();
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ // Subclass of the TypeAxiomBuilder that provides all functionality
+ // to deal with native sorts of a theorem prover (that are the only
+ // types left after erasing all other types). Currently, these are:
+ //
+ // U ... sort of all individuals/objects/values
+ // T ... sort of all types
+ // int ... integers
+ // bool ... booleans
+
+ public abstract class TypeAxiomBuilderIntBoolU : TypeAxiomBuilder {
+
+ public TypeAxiomBuilderIntBoolU(VCExpressionGenerator! gen) {
+ base(gen);
+ TypeCasts = new Dictionary<Type!, TypeCastSet> ();
+ }
+
+ // constructor to allow cloning
+ internal TypeAxiomBuilderIntBoolU(TypeAxiomBuilderIntBoolU! builder) {
+ base(builder);
+ TypeCasts = new Dictionary<Type!, TypeCastSet> (builder.TypeCasts);
+ }
+
+ public override void Setup() {
+ base.Setup();
+
+ GetTypeCasts(Type.Int);
+ GetTypeCasts(Type.Bool);
+ }
+
+ // generate inverse axioms for casts (castToU(castFromU(x)) = x, under certain premisses)
+ protected abstract VCExpr! GenReverseCastAxiom(Function! castToU, Function! castFromU);
+
+ protected VCExpr! GenReverseCastEq(Function! castToU, Function! castFromU,
+ out VCExprVar! var, out List<VCTrigger!>! triggers) {
+ var = Gen.Variable("x", U);
+
+ VCExpr! lhs = Gen.Function(castToU, Gen.Function(castFromU, var));
+ triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(lhs)));
+
+ return Gen.Eq(lhs, var);
+ }
+
+ protected abstract VCExpr! GenCastTypeAxioms(Function! castToU, Function! castFromU);
+
+ ///////////////////////////////////////////////////////////////////////////
+ // storage of type casts for types that are supposed to be left over in the
+ // VCs (like int, bool, bitvectors)
+
+ private readonly IDictionary<Type!, TypeCastSet>! TypeCasts;
+
+ private TypeCastSet GetTypeCasts(Type! type) {
+ TypeCastSet res;
+ if (!TypeCasts.TryGetValue(type, out res)) {
+ Function! castToU = HelperFuns.BoogieFunction(type.ToString() + "_2_U", type, U);
+ Function! castFromU = HelperFuns.BoogieFunction("U_2_" + type.ToString(), U, type);
+
+ AddTypeAxiom(GenLeftInverseAxiom(castToU, castFromU, 0));
+ AddTypeAxiom(GenReverseCastAxiom(castToU, castFromU));
+ AddTypeAxiom(GenCastTypeAxioms(castToU, castFromU));
+
+ res = new TypeCastSet (castToU, castFromU);
+ TypeCasts.Add(type, res);
+ }
+ return res;
+ }
+
+ public Function! CastTo(Type! type)
+ requires UnchangedType(type); {
+ return GetTypeCasts(type).CastFromU;
+ }
+
+ public Function! CastFrom(Type! type)
+ requires UnchangedType(type); {
+ return GetTypeCasts(type).CastToU;
+ }
+
+ private struct TypeCastSet {
+ public readonly Function! CastToU;
+ public readonly Function! CastFromU;
+
+ public TypeCastSet(Function! castToU, Function! castFromU) {
+ CastToU = castToU;
+ CastFromU = castFromU;
+ }
+ }
+
+ public bool IsCast(Function! fun) {
+ if (fun.InParams.Length != 1)
+ return false;
+ Type! inType = ((!)fun.InParams[0]).TypedIdent.Type;
+ if (inType.Equals(U)) {
+ Type! outType = ((!)fun.OutParams[0]).TypedIdent.Type;
+ if (!TypeCasts.ContainsKey(outType))
+ return false;
+ return fun.Equals(CastTo(outType));
+ } else {
+ if (!TypeCasts.ContainsKey(inType))
+ return false;
+ Type! outType = ((!)fun.OutParams[0]).TypedIdent.Type;
+ if (!outType.Equals(U))
+ return false;
+ return fun.Equals(CastFrom(inType));
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // the only types that we allow in "untyped" expressions are U,
+ // Type.Int, and Type.Bool
+
+ public override Type! TypeAfterErasure(Type! type) {
+ if (UnchangedType(type))
+ // these types are kept
+ return type;
+ else
+ // all other types are replaced by U
+ return U;
+ }
+
+ [Pure]
+ public override bool UnchangedType(Type! type) {
+ return type.IsInt || type.IsBool || type.IsBv;
+ }
+
+ public VCExpr! Cast(VCExpr! expr, Type! toType)
+ requires expr.Type.Equals(U) || UnchangedType(expr.Type);
+ requires toType.Equals(U) || UnchangedType(toType);
+ {
+ if (expr.Type.Equals(toType))
+ return expr;
+
+ if (toType.Equals(U)) {
+ return Gen.Function(CastFrom(expr.Type), expr);
+ } else {
+ assert expr.Type.Equals(U);
+ return Gen.Function(CastTo(toType), expr);
+ }
+ }
+
+ public List<VCExpr!>! CastSeq(List<VCExpr!>! exprs, Type! toType) {
+ List<VCExpr!>! res = new List<VCExpr!> (exprs.Count);
+ foreach (VCExpr! expr in exprs)
+ res.Add(Cast(expr, toType));
+ return res;
+ }
+
+
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+ // Class for computing most general abstractions of map types. An abstraction
+ // of a map type t is a maptype t' in which closed proper subtypes have been replaced
+ // with type variables. E.g., an abstraction of <a>[C a, int]a would be <a>[C a, b]a.
+ // We subsequently consider most general abstractions as ordinary parametrised types,
+ // i.e., "<a>[C a, b]a" would be considered as a type "M b" with polymorphically typed
+ // access functions
+ //
+ // select<a,b>(M b, C a, b) returns (a)
+ // store<a,b>(M b, C a, b, a) returns (M b)
+
+ internal abstract class MapTypeAbstractionBuilder {
+
+ protected readonly TypeAxiomBuilder! AxBuilder;
+ protected readonly VCExpressionGenerator! Gen;
+
+ internal MapTypeAbstractionBuilder(TypeAxiomBuilder! axBuilder,
+ VCExpressionGenerator! gen) {
+ this.AxBuilder = axBuilder;
+ this.Gen = gen;
+ AbstractionVariables = new List<TypeVariable!> ();
+ ClassRepresentations = new Dictionary<MapType!, MapTypeClassRepresentation> ();
+ }
+
+ // constructor for cloning
+ internal MapTypeAbstractionBuilder(TypeAxiomBuilder! axBuilder,
+ VCExpressionGenerator! gen,
+ MapTypeAbstractionBuilder! builder) {
+ this.AxBuilder = axBuilder;
+ this.Gen = gen;
+ AbstractionVariables =
+ new List<TypeVariable!> (builder.AbstractionVariables);
+ ClassRepresentations =
+ new Dictionary<MapType!, MapTypeClassRepresentation> (builder.ClassRepresentations);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Type variables used in the abstractions. We use the same variables in the
+ // same order in all abstractions in order to obtain comparable abstractions
+ // (equals, hashcode)
+
+ private readonly List<TypeVariable!>! AbstractionVariables;
+
+ private TypeVariable! AbstractionVariable(int num)
+ requires num >= 0; {
+ while (AbstractionVariables.Count <= num)
+ AbstractionVariables.Add(new TypeVariable (Token.NoToken,
+ "aVar" + AbstractionVariables.Count));
+ return AbstractionVariables[num];
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // The untyped representation of a class of map types, i.e., of a map type
+ // <a0, a1, ...>[A0, A1, ...] R, where the argument types and the result type
+ // possibly contain free type variables. For each such class, a separate type
+ // constructor and separate select/store functions are introduced.
+
+ protected struct MapTypeClassRepresentation {
+ public readonly TypeCtorDecl! RepresentingType;
+ public readonly Function! Select;
+ public readonly Function! Store;
+
+ public MapTypeClassRepresentation(TypeCtorDecl! representingType,
+ Function! select, Function! store) {
+ this.RepresentingType = representingType;
+ this.Select = select;
+ this.Store = store;
+ }
+ }
+
+ private readonly IDictionary<MapType!, MapTypeClassRepresentation>! ClassRepresentations;
+
+ protected MapTypeClassRepresentation GetClassRepresentation(MapType! abstractedType) {
+ MapTypeClassRepresentation res;
+ if (!ClassRepresentations.TryGetValue(abstractedType, out res)) {
+ int num = ClassRepresentations.Count;
+ TypeCtorDecl! synonym =
+ new TypeCtorDecl(Token.NoToken, "MapType" + num, abstractedType.FreeVariables.Length);
+
+ Function! select, store;
+ GenSelectStoreFunctions(abstractedType, synonym, out select, out store);
+
+ res = new MapTypeClassRepresentation(synonym, select, store);
+ ClassRepresentations.Add(abstractedType, res);
+ }
+ return res;
+ }
+
+ // the actual select and store functions are generated by the
+ // concrete subclasses of this class
+ protected abstract void GenSelectStoreFunctions(MapType! abstractedType,
+ TypeCtorDecl! synonymDecl,
+ out Function! select, out Function! store);
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ public Function! Select(MapType! rawType, out TypeSeq! instantiations) {
+ return AbstractAndGetRepresentation(rawType, out instantiations).Select;
+ }
+
+ public Function! Store(MapType! rawType, out TypeSeq! instantiations) {
+ return AbstractAndGetRepresentation(rawType, out instantiations).Store;
+ }
+
+ private MapTypeClassRepresentation
+ AbstractAndGetRepresentation(MapType! rawType, out TypeSeq! instantiations) {
+ instantiations = new TypeSeq ();
+ MapType! abstraction = ThinOutMapType(rawType, instantiations);
+ return GetClassRepresentation(abstraction);
+ }
+
+ public CtorType! AbstractMapType(MapType! rawType) {
+ TypeSeq! instantiations = new TypeSeq ();
+ MapType! abstraction = ThinOutMapType(rawType, instantiations);
+
+ MapTypeClassRepresentation repr = GetClassRepresentation(abstraction);
+ assume repr.RepresentingType.Arity == instantiations.Length;
+ return new CtorType(Token.NoToken, repr.RepresentingType, instantiations);
+ }
+
+ // TODO: cache the result of this operation
+ protected MapType! ThinOutMapType(MapType! rawType,
+ TypeSeq! instantiations) {
+ TypeSeq! newArguments = new TypeSeq ();
+ foreach (Type! subtype in rawType.Arguments)
+ newArguments.Add(ThinOutType(subtype, rawType.TypeParameters,
+ instantiations));
+ Type! newResult = ThinOutType(rawType.Result, rawType.TypeParameters,
+ instantiations);
+ return new MapType(Token.NoToken, rawType.TypeParameters, newArguments, newResult);
+ }
+
+ private Type! ThinOutType(Type! rawType, TypeVariableSeq! boundTypeParams,
+ // the instantiations of inserted type variables,
+ // the order corresponds to the order in which
+ // "AbstractionVariable(int)" delivers variables
+ TypeSeq! instantiations) {
+
+ if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))
+ return rawType;
+
+ if (forall{TypeVariable! var in rawType.FreeVariables;
+ !boundTypeParams.Has(var)}) {
+ // Bingo!
+ // if the type does not contain any bound variables, we can simply
+ // replace it with a type variable
+ TypeVariable! abstractionVar = AbstractionVariable(instantiations.Length);
+ assume !boundTypeParams.Has(abstractionVar);
+ instantiations.Add(rawType);
+ return abstractionVar;
+ }
+
+ if (rawType.IsVariable) {
+ //
+ // then the variable has to be bound, we cannot do anything
+ TypeVariable! rawVar = rawType.AsVariable;
+ assume boundTypeParams.Has(rawVar);
+ return rawVar;
+ //
+ } else if (rawType.IsMap) {
+ //
+ // recursively abstract this map type and continue abstracting
+ CtorType! abstraction = AbstractMapType(rawType.AsMap);
+ return ThinOutType(abstraction, boundTypeParams, instantiations);
+ //
+ } else if (rawType.IsCtor) {
+ //
+ // traverse the subtypes
+ CtorType! rawCtorType = rawType.AsCtor;
+ TypeSeq! newArguments = new TypeSeq ();
+ foreach (Type! subtype in rawCtorType.Arguments)
+ newArguments.Add(ThinOutType(subtype, boundTypeParams,
+ instantiations));
+ return new CtorType(Token.NoToken, rawCtorType.Decl, newArguments);
+ //
+ } else {
+ System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + rawType);
+ return rawType; // compiler appeasement policy
+ }
+ }
+
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ public class VariableBindings {
+ public readonly IDictionary<VCExprVar!, VCExprVar!>! VCExprVarBindings;
+ public readonly IDictionary<TypeVariable!, VCExpr!>! TypeVariableBindings;
+
+ public VariableBindings(IDictionary<VCExprVar!, VCExprVar!>! vcExprVarBindings,
+ IDictionary<TypeVariable!, VCExpr!>! typeVariableBindings) {
+ this.VCExprVarBindings = vcExprVarBindings;
+ this.TypeVariableBindings = typeVariableBindings;
+ }
+
+ public VariableBindings() {
+ this (new Dictionary<VCExprVar!, VCExprVar!> (),
+ new Dictionary<TypeVariable!, VCExpr!> ());
+ }
+
+ public VariableBindings! Clone() {
+ IDictionary<VCExprVar!, VCExprVar!>! newVCExprVarBindings =
+ new Dictionary<VCExprVar!, VCExprVar!> ();
+ foreach (KeyValuePair<VCExprVar!, VCExprVar!> pair in VCExprVarBindings)
+ newVCExprVarBindings.Add(pair);
+ IDictionary<TypeVariable!, VCExpr!>! newTypeVariableBindings =
+ new Dictionary<TypeVariable!, VCExpr!> ();
+ foreach (KeyValuePair<TypeVariable!, VCExpr!> pair in TypeVariableBindings)
+ newTypeVariableBindings.Add(pair);
+ return new VariableBindings(newVCExprVarBindings, newTypeVariableBindings);
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ // The central class for turning types VCExprs into untyped
+ // VCExprs. This class makes use of the type axiom builder to manage
+ // the available types and symbols.
+
+ public abstract class TypeEraser : MutatingVCExprVisitor<VariableBindings!> {
+
+ protected readonly TypeAxiomBuilderIntBoolU! AxBuilder;
+
+ protected abstract OpTypeEraser! OpEraser { get; }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public TypeEraser(TypeAxiomBuilderIntBoolU! axBuilder, VCExpressionGenerator! gen) {
+ base(gen);
+ AxBuilder = axBuilder;
+ }
+
+ public VCExpr! Erase(VCExpr! expr, int polarity)
+ requires polarity >= -1 && polarity <= 1; {
+ this.Polarity = polarity;
+ return Mutate(expr, new VariableBindings ());
+ }
+
+ internal int Polarity = 1; // 1 for positive, -1 for negative, 0 for both
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprLiteral! node, VariableBindings! bindings) {
+ assume node.Type == Type.Bool || node.Type == Type.Int;
+ return node;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprNAry! node, VariableBindings! bindings) {
+ VCExprOp! op = node.Op;
+ if (op == VCExpressionGenerator.AndOp || op == VCExpressionGenerator.OrOp)
+ // more efficient on large conjunctions/disjunctions
+ return base.Visit(node, bindings);
+
+ // the visitor that handles all other operators
+ return node.Accept<VCExpr!, VariableBindings!>(OpEraser, bindings);
+ }
+
+ // this method is called by MutatingVCExprVisitor.Visit(VCExprNAry, ...)
+ protected override VCExpr! UpdateModifiedNode(VCExprNAry! originalNode,
+ List<VCExpr!>! newSubExprs,
+ bool changed,
+ VariableBindings! bindings) {
+ assume originalNode.Op == VCExpressionGenerator.AndOp ||
+ originalNode.Op == VCExpressionGenerator.OrOp;
+ return Gen.Function(originalNode.Op,
+ AxBuilder.Cast(newSubExprs[0], Type.Bool),
+ AxBuilder.Cast(newSubExprs[1], Type.Bool));
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprVar! node, VariableBindings! bindings) {
+ VCExprVar res;
+ if (!bindings.VCExprVarBindings.TryGetValue(node, out res))
+ return AxBuilder.Typed2Untyped(node);
+ return (!)res;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ protected bool IsUniversalQuantifier(VCExprQuantifier! node) {
+ return Polarity == 1 && node.Quan == Quantifier.EX ||
+ Polarity == -1 && node.Quan == Quantifier.ALL;
+ }
+
+ protected List<VCExprVar!>! BoundVarsAfterErasure(List<VCExprVar!>! oldBoundVars,
+ // the mapping between old and new variables
+ // is added to this bindings-object
+ VariableBindings! bindings) {
+ List<VCExprVar!>! newBoundVars = new List<VCExprVar!> (oldBoundVars.Count);
+ foreach (VCExprVar! var in oldBoundVars) {
+ Type! newType = AxBuilder.TypeAfterErasure(var.Type);
+ VCExprVar! newVar = Gen.Variable(var.Name, newType);
+ newBoundVars.Add(newVar);
+ bindings.VCExprVarBindings.Add(var, newVar);
+ }
+ return newBoundVars;
+ }
+
+ // We check whether casts Int2U or Bool2U on the bound variables
+ // occur in triggers. In case a trigger like f(Int2U(x)) occurs,
+ // it may be better to give variable x the type U and remove the
+ // cast. The following method returns true if the quantifier
+ // should be translated again with a different typing
+ protected bool RedoQuantifier(VCExprQuantifier! node,
+ VCExprQuantifier! newNode,
+ // the bound vars that actually occur in the body or
+ // in any of the triggers
+ List<VCExprVar!>! occurringVars,
+ VariableBindings! oldBindings,
+ out VariableBindings! newBindings,
+ out List<VCExprVar!>! newBoundVars) {
+ List<VCExprVar!> castVariables =
+ VariableCastCollector.FindCastVariables(node, newNode, AxBuilder);
+ if (castVariables.Count == 0) {
+ newBindings = oldBindings; // to make the compiler happy
+ newBoundVars = newNode.BoundVars; // to make the compiler happy
+ return false;
+ }
+
+ // redo everything with a different typing ...
+
+ newBindings = oldBindings.Clone();
+ newBoundVars = new List<VCExprVar!> (node.BoundVars.Count);
+ foreach (VCExprVar! var in node.BoundVars) {
+ Type! newType =
+ castVariables.Contains(var) ? AxBuilder.U
+ : AxBuilder.TypeAfterErasure(var.Type);
+ VCExprVar! newVar = Gen.Variable(var.Name, newType);
+ newBoundVars.Add(newVar);
+ newBindings.VCExprVarBindings.Add(var, newVar);
+ }
+
+ return true;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprLet! node, VariableBindings! bindings) {
+ VariableBindings! newVarBindings = bindings.Clone();
+
+ List<VCExprVar!>! newBoundVars = new List<VCExprVar!> (node.BoundVars.Count);
+ foreach (VCExprVar! var in node.BoundVars) {
+ Type! newType = AxBuilder.TypeAfterErasure(var.Type);
+ VCExprVar! newVar = Gen.Variable(var.Name, newType);
+ newBoundVars.Add(newVar);
+ newVarBindings.VCExprVarBindings.Add(var, newVar);
+ }
+
+ List<VCExprLetBinding!>! newbindings = new List<VCExprLetBinding!> (node.Length);
+ for (int i = 0; i < node.Length; ++i) {
+ VCExprLetBinding! binding = node[i];
+ VCExprVar! newVar = newBoundVars[i];
+ Type! newType = newVar.Type;
+
+ VCExpr! newE = AxBuilder.Cast(Mutate(binding.E, newVarBindings), newType);
+ newbindings.Add(Gen.LetBinding(newVar, newE));
+ }
+
+ VCExpr! newbody = Mutate(node.Body, newVarBindings);
+ return Gen.Let(newbindings, newbody);
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ public abstract class OpTypeEraser : StandardVCExprOpVisitor<VCExpr!, VariableBindings!> {
+
+ protected readonly TypeAxiomBuilderIntBoolU! AxBuilder;
+
+ protected readonly TypeEraser! Eraser;
+ protected readonly VCExpressionGenerator! Gen;
+
+ public OpTypeEraser(TypeEraser! eraser, TypeAxiomBuilderIntBoolU! axBuilder,
+ VCExpressionGenerator! gen) {
+ this.AxBuilder = axBuilder;
+ this.Eraser = eraser;
+ this.Gen = gen;
+ }
+
+ protected override VCExpr! StandardResult(VCExprNAry! node, VariableBindings! bindings) {
+ System.Diagnostics.Debug.Fail("Don't know how to erase types in this expression: " + node);
+ assert false; // to please the compiler
+ }
+
+ private List<VCExpr!>! MutateSeq(VCExprNAry! node, VariableBindings! bindings,
+ int newPolarity) {
+ int oldPolarity = Eraser.Polarity;
+ Eraser.Polarity = newPolarity;
+ List<VCExpr!>! newArgs = Eraser.MutateSeq(node, bindings);
+ Eraser.Polarity = oldPolarity;
+ return newArgs;
+ }
+
+ private VCExpr! CastArguments(VCExprNAry! node, Type! argType, VariableBindings! bindings,
+ int newPolarity) {
+ return Gen.Function(node.Op,
+ AxBuilder.CastSeq(MutateSeq(node, bindings, newPolarity),
+ argType));
+ }
+
+ // Cast the arguments of the node to their old type if necessary and possible; otherwise use
+ // their new type (int, bool, or U)
+ private VCExpr! CastArgumentsToOldType(VCExprNAry! node, VariableBindings! bindings,
+ int newPolarity)
+ requires node.Arity > 0; {
+
+ List<VCExpr!>! newArgs = MutateSeq(node, bindings, newPolarity);
+ Type! oldType = node[0].Type;
+ if (AxBuilder.UnchangedType(oldType) &&
+ forall{int i in (1:node.Arity); node[i].Type.Equals(oldType)})
+ return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType));
+ else
+ return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! VisitNotOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Bool, bindings, -Eraser.Polarity);
+ }
+ public override VCExpr! VisitEqOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr! VisitNeqOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr! VisitImpliesOp (VCExprNAry! node, VariableBindings! bindings) {
+ // UGLY: the code for tracking polarities should be factored out
+ List<VCExpr!>! newArgs = new List<VCExpr!> (2);
+ Eraser.Polarity = -Eraser.Polarity;
+ newArgs.Add(Eraser.Mutate(node[0], bindings));
+ Eraser.Polarity = -Eraser.Polarity;
+ newArgs.Add(Eraser.Mutate(node[1], bindings));
+ return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, Type.Bool));
+ }
+ public override VCExpr! VisitDistinctOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr! VisitLabelOp (VCExprNAry! node, VariableBindings! bindings) {
+ // argument of the label operator should always be a formula
+ // (at least for Simplify ... should this be ensured at a later point?)
+ return CastArguments(node, Type.Bool, bindings, Eraser.Polarity);
+ }
+ public override VCExpr! VisitAddOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitSubOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitMulOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitDivOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitModOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitLtOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitLeOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitGtOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitGeOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, Type.Int, bindings, 0);
+ }
+ public override VCExpr! VisitSubtypeOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArguments(node, AxBuilder.U, bindings, 0);
+ }
+ public override VCExpr! VisitBvOp (VCExprNAry! node, VariableBindings! bindings) {
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr! VisitBvExtractOp(VCExprNAry! node, VariableBindings! bindings) {
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr! VisitBvConcatOp (VCExprNAry! node, VariableBindings! bindings) {
+ List<VCExpr!>! newArgs = MutateSeq(node, bindings, 0);
+
+ // each argument is cast to its old type
+ assert newArgs.Count == node.Arity && newArgs.Count == 2;
+ VCExpr! arg0 = AxBuilder.Cast(newArgs[0], node[0].Type);
+ VCExpr! arg1 = AxBuilder.Cast(newArgs[1], node[1].Type);
+
+ return Gen.Function(node.Op, arg0, arg1);
+ }
+
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ /// <summary>
+ /// Collect all variables x occurring in expressions of the form Int2U(x) or Bool2U(x), and
+ /// collect all variables x occurring outside such forms.
+ /// </summary>
+ internal class VariableCastCollector : TraversingVCExprVisitor<bool, bool> {
+ /// <summary>
+ /// Determine those bound variables in "oldNode" <em>all</em> of whose relevant uses
+ /// have to be cast in potential triggers in "newNode". It is assume that
+ /// the bound variables of "oldNode" correspond to the first bound
+ /// variables of "newNode".
+ /// </summary>
+ public static List<VCExprVar!>! FindCastVariables(VCExprQuantifier! oldNode,
+ VCExprQuantifier! newNode,
+ TypeAxiomBuilderIntBoolU! axBuilder) {
+ VariableCastCollector! collector = new VariableCastCollector(axBuilder);
+ if (exists{VCTrigger! trigger in newNode.Triggers; trigger.Pos}) {
+ // look in the given triggers
+ foreach (VCTrigger! trigger in newNode.Triggers)
+ if (trigger.Pos)
+ foreach (VCExpr! expr in trigger.Exprs)
+ collector.Traverse(expr, true);
+ } else {
+ // look in the body of the quantifier
+ collector.Traverse(newNode.Body, true);
+ }
+
+ List<VCExprVar!>! castVariables = new List<VCExprVar!> (collector.varsInCasts.Count);
+ foreach (VCExprVar! castVar in collector.varsInCasts) {
+ int i = newNode.BoundVars.IndexOf(castVar);
+ if (0 <= i && i < oldNode.BoundVars.Count && !collector.varsOutsideCasts.ContainsKey(castVar))
+ castVariables.Add(oldNode.BoundVars[i]);
+ }
+ return castVariables;
+ }
+
+ public VariableCastCollector(TypeAxiomBuilderIntBoolU! axBuilder) {
+ this.AxBuilder = axBuilder;
+ }
+
+ readonly List<VCExprVar!>! varsInCasts = new List<VCExprVar!> ();
+ readonly Dictionary<VCExprVar!,object>! varsOutsideCasts = new Dictionary<VCExprVar!,object> ();
+
+ readonly TypeAxiomBuilderIntBoolU! AxBuilder;
+
+ protected override bool StandardResult(VCExpr! node, bool arg) {
+ return true; // not used
+ }
+
+ public override bool Visit(VCExprNAry! node, bool arg) {
+ if (node.Op is VCExprBoogieFunctionOp) {
+ Function! func = ((VCExprBoogieFunctionOp)node.Op).Func;
+ if ((AxBuilder.IsCast(func)) && node[0] is VCExprVar) {
+ VCExprVar castVar = (VCExprVar)node[0];
+ if (!varsInCasts.Contains(castVar))
+ varsInCasts.Add(castVar);
+ return true;
+ }
+ } else if (node.Op is VCExprNAryOp) {
+ VCExpressionGenerator.SingletonOp op = VCExpressionGenerator.SingletonOpDict[node.Op];
+ switch(op) {
+ // the following operators cannot be used in triggers, so disregard any uses of variables as direct arguments
+ case VCExpressionGenerator.SingletonOp.NotOp:
+ case VCExpressionGenerator.SingletonOp.EqOp:
+ case VCExpressionGenerator.SingletonOp.NeqOp:
+ case VCExpressionGenerator.SingletonOp.AndOp:
+ case VCExpressionGenerator.SingletonOp.OrOp:
+ case VCExpressionGenerator.SingletonOp.ImpliesOp:
+ case VCExpressionGenerator.SingletonOp.LtOp:
+ case VCExpressionGenerator.SingletonOp.LeOp:
+ case VCExpressionGenerator.SingletonOp.GtOp:
+ case VCExpressionGenerator.SingletonOp.GeOp:
+ foreach (VCExpr n in node) {
+ if (!(n is VCExprVar)) { // don't recurse on VCExprVar argument
+ n.Accept<bool,bool>(this, arg);
+ }
+ }
+ return true;
+ default:
+ break;
+ }
+ }
+ return base.Visit(node, arg);
+ }
+
+ public override bool Visit(VCExprVar! node, bool arg) {
+ if (!varsOutsideCasts.ContainsKey(node))
+ varsOutsideCasts.Add(node, null);
+ return true;
+ }
+ }
+
+}
diff --git a/Source/VCExpr/TypeErasureArguments.ssc b/Source/VCExpr/TypeErasureArguments.ssc new file mode 100644 index 00000000..434866f8 --- /dev/null +++ b/Source/VCExpr/TypeErasureArguments.ssc @@ -0,0 +1,618 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+using Microsoft.Boogie.VCExprAST;
+
+// Erasure of types using explicit type parameters for functions
+
+namespace Microsoft.Boogie.TypeErasure
+{
+ using Microsoft.Boogie.VCExprAST;
+ using HFNS = Microsoft.Boogie.VCExprAST.HelperFuns;
+
+ public class TypeAxiomBuilderArguments : TypeAxiomBuilderIntBoolU {
+
+ public TypeAxiomBuilderArguments(VCExpressionGenerator! gen) {
+ base(gen);
+ Typed2UntypedFunctions = new Dictionary<Function!, Function!> ();
+ }
+
+ // constructor to allow cloning
+ [NotDelayed]
+ internal TypeAxiomBuilderArguments(TypeAxiomBuilderArguments! builder) {
+ Typed2UntypedFunctions =
+ new Dictionary<Function!, Function!> (builder.Typed2UntypedFunctions);
+ base(builder);
+
+ MapTypeAbstracterAttr =
+ builder.MapTypeAbstracterAttr == null ?
+ null : new MapTypeAbstractionBuilderArguments(this, builder.Gen,
+ builder.MapTypeAbstracterAttr);
+ }
+
+ public override Object! Clone() {
+ return new TypeAxiomBuilderArguments(this);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////
+
+ // generate axioms of the kind "forall x:U. {Int2U(U2Int(x))} Int2U(U2Int(x))==x"
+ // (this makes use of the assumption that only well-typed terms are generated
+ // by the SMT-solver, i.e., that U2Int is only applied to terms that actually
+ // are of type int)
+ protected override VCExpr! GenReverseCastAxiom(Function! castToU,
+ Function! castFromU) {
+ List<VCTrigger!>! triggers;
+ VCExprVar! var;
+ VCExpr! eq = GenReverseCastEq(castToU, castFromU, out var, out triggers);
+ return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, eq);
+ }
+
+ protected override VCExpr! GenCastTypeAxioms(Function! castToU,
+ Function! castFromU) {
+ // nothing
+ return VCExpressionGenerator.True;
+ }
+
+ private MapTypeAbstractionBuilderArguments MapTypeAbstracterAttr = null;
+
+ internal override MapTypeAbstractionBuilder! MapTypeAbstracter { get {
+ if (MapTypeAbstracterAttr == null)
+ MapTypeAbstracterAttr = new MapTypeAbstractionBuilderArguments (this, Gen);
+ return MapTypeAbstracterAttr;
+ } }
+
+ protected override void AddVarTypeAxiom(VCExprVar! var, Type! originalType) {
+ // no axioms are needed for variable or function types
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Symbols for representing functions
+
+ // Globally defined functions
+ private readonly IDictionary<Function!, Function!>! Typed2UntypedFunctions;
+
+ public Function! Typed2Untyped(Function! fun) {
+ Function res;
+ if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {
+ assert fun.OutParams.Length == 1;
+
+ // if all of the parameters are int or bool, the function does
+ // not have to be changed
+ if (forall{Formal f in fun.InParams; UnchangedType(((!)f).TypedIdent.Type)} &&
+ UnchangedType(((!)fun.OutParams[0]).TypedIdent.Type)) {
+ res = fun;
+ } else {
+ Type[]! types = new Type [fun.TypeParameters.Length + fun.InParams.Length + 1];
+
+ int i = 0;
+ // the first arguments are the explicit type parameters
+ for (int j = 0; j < fun.TypeParameters.Length; ++j) {
+ types[i] = T;
+ i = i + 1;
+ }
+ // followed by the actual parameters
+ foreach (Variable! x in fun.InParams) {
+ types[i] = TypeAfterErasure(x.TypedIdent.Type);
+ i = i + 1;
+ }
+
+ types[types.Length - 1] = TypeAfterErasure(((!)fun.OutParams[0]).TypedIdent.Type);
+
+ res = HelperFuns.BoogieFunction(fun.Name, types);
+ res.Attributes = fun.Attributes;
+ }
+
+ Typed2UntypedFunctions.Add(fun, res);
+ }
+ return (!)res;
+ }
+
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ internal class MapTypeAbstractionBuilderArguments : MapTypeAbstractionBuilder {
+
+ private readonly TypeAxiomBuilderArguments! AxBuilderArguments;
+
+ internal MapTypeAbstractionBuilderArguments(TypeAxiomBuilderArguments! axBuilder,
+ VCExpressionGenerator! gen) {
+ base(axBuilder, gen);
+ this.AxBuilderArguments = axBuilder;
+ }
+
+ // constructor for cloning
+ internal MapTypeAbstractionBuilderArguments(TypeAxiomBuilderArguments! axBuilder,
+ VCExpressionGenerator! gen,
+ MapTypeAbstractionBuilderArguments! builder) {
+ base(axBuilder, gen, builder);
+ this.AxBuilderArguments = axBuilder;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ protected override void GenSelectStoreFunctions(MapType! abstractedType,
+ TypeCtorDecl! synonym,
+ out Function! select,
+ out Function! store) {
+ string! baseName = synonym.Name;
+ int typeParamNum = abstractedType.FreeVariables.Length +
+ abstractedType.TypeParameters.Length;
+ int arity = typeParamNum + abstractedType.Arguments.Length;
+
+ Type![]! selectTypes = new Type! [arity + 2];
+ Type![]! storeTypes = new Type! [arity + 3];
+
+ int i = 0;
+ // Fill in the free variables and type parameters
+ for (; i < typeParamNum; i++) {
+ selectTypes[i] = AxBuilder.T;
+ storeTypes[i] = AxBuilder.T;
+ }
+ // Fill in the map type
+ selectTypes[i] = AxBuilder.U;
+ storeTypes[i] = AxBuilder.U;
+ i++;
+ // Fill in the index types
+ foreach (Type! type in abstractedType.Arguments)
+ {
+ if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type))
+ {
+ selectTypes[i] = type;
+ storeTypes[i] = type;
+ }
+ else
+ {
+ selectTypes[i] = AxBuilder.U;
+ storeTypes[i] = AxBuilder.U;
+ }
+ i++;
+ }
+ // Fill in the output type for select function which also happens
+ // to be the type of the last argument to the store function
+ if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(abstractedType.Result))
+ {
+ selectTypes[i] = abstractedType.Result;
+ storeTypes[i] = abstractedType.Result;
+ }
+ else
+ {
+ selectTypes[i] = AxBuilder.U;
+ storeTypes[i] = AxBuilder.U;
+ }
+ i++;
+ // Fill in the map type which is the output of the store function
+ storeTypes[i] = AxBuilder.U;
+ NonNullType.AssertInitialized(selectTypes);
+ NonNullType.AssertInitialized(storeTypes);
+
+ select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);
+ store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes);
+
+ AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,
+ abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));
+ AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store,
+ abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // The normal axioms of the theory of arrays (right now without extensionality)
+
+ private VCExpr! Select(Function! select, List<VCExprVar!>! types,
+ VCExpr! map, List<VCExprVar!>! indexes) {
+ List<VCExpr!>! selectArgs = new List<VCExpr!> ();
+ selectArgs.AddRange(HelperFuns.ToVCExprList(types));
+ selectArgs.Add(map);
+ selectArgs.AddRange(HelperFuns.ToVCExprList(indexes));
+ return Gen.Function(select, selectArgs);
+ }
+
+ private VCExpr! Store(Function! store, List<VCExprVar!>! types,
+ VCExpr! map, List<VCExprVar!>! indexes, VCExpr! val) {
+ List<VCExpr!>! storeArgs = new List<VCExpr!> ();
+ storeArgs.AddRange(HelperFuns.ToVCExprList(types));
+ storeArgs.Add(map);
+ storeArgs.AddRange(HelperFuns.ToVCExprList(indexes));
+ storeArgs.Add(val);
+ return Gen.Function(store, storeArgs);
+ }
+
+ private VCExpr! GenMapAxiom0(Function! select, Function! store,
+ // bound type variables in the map type
+ int mapTypeParamNum,
+ // free type variables in the map
+ // type (abstraction)
+ int mapAbstractionVarNum) {
+ int arity = select.InParams.Length - 1 - mapTypeParamNum - mapAbstractionVarNum;
+ List<VCExprVar!>! types =
+ HelperFuns.VarVector("t", mapTypeParamNum + mapAbstractionVarNum,
+ AxBuilder.T, Gen);
+
+ List<Type!> indexTypes = new List<Type!>();
+ for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++)
+ {
+ indexTypes.Add(((!)select.InParams[i]).TypedIdent.Type);
+ }
+ assert arity == indexTypes.Count;
+
+ List<VCExprVar!>! indexes = HelperFuns.VarVector("x", indexTypes, Gen);
+
+ VCExprVar! m = Gen.Variable("m", AxBuilder.U);
+ VCExprVar! val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type);
+
+ VCExpr! storeExpr = Store(store, types, m, indexes, val);
+ VCExpr! selectExpr = Select(select, types, storeExpr, indexes);
+
+ List<VCExprVar!>! quantifiedVars = new List<VCExprVar!> ();
+ quantifiedVars.AddRange(types);
+ quantifiedVars.Add(val);
+ quantifiedVars.Add(m);
+ quantifiedVars.AddRange(indexes);
+
+ VCExpr! eq = Gen.Eq(selectExpr, val);
+ return Gen.Forall(quantifiedVars, new List<VCTrigger!> (),
+ "mapAx0:" + select.Name, eq);
+ }
+
+ private VCExpr! GenMapAxiom1(Function! select, Function! store,
+ // bound type variables in the map
+ // type
+ int mapTypeParamNum,
+ // free type variables in the map
+ // type (abstraction)
+ int mapAbstractionVarNum) {
+ int arity = select.InParams.Length - 1 - mapTypeParamNum - mapAbstractionVarNum;
+
+ List<VCExprVar!>! freeTypeVars =
+ HelperFuns.VarVector("u", mapAbstractionVarNum, AxBuilder.T, Gen);
+ List<VCExprVar!>! boundTypeVars0 =
+ HelperFuns.VarVector("s", mapTypeParamNum, AxBuilder.T, Gen);
+ List<VCExprVar!>! boundTypeVars1 =
+ HelperFuns.VarVector("t", mapTypeParamNum, AxBuilder.T, Gen);
+
+ List<VCExprVar!>! types0 = new List<VCExprVar!> (boundTypeVars0);
+ types0.AddRange(freeTypeVars);
+
+ List<VCExprVar!>! types1 = new List<VCExprVar!> (boundTypeVars1);
+ types1.AddRange(freeTypeVars);
+
+ List<Type!> indexTypes = new List<Type!>();
+ for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++)
+ {
+ indexTypes.Add(((!)select.InParams[i]).TypedIdent.Type);
+ }
+ assert arity == indexTypes.Count;
+
+ List<VCExprVar!>! indexes0 = HelperFuns.VarVector("x", indexTypes, Gen);
+ List<VCExprVar!>! indexes1 = HelperFuns.VarVector("y", indexTypes, Gen);
+
+ VCExprVar! m = Gen.Variable("m", AxBuilder.U);
+ VCExprVar! val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type);
+
+ VCExpr! storeExpr = Store(store, types0, m, indexes0, val);
+ VCExpr! selectWithoutStoreExpr = Select(select, types1, m, indexes1);
+ VCExpr! selectExpr = Select(select, types1, storeExpr, indexes1);
+
+ VCExpr! selectEq = Gen.Eq(selectExpr, selectWithoutStoreExpr);
+
+ List<VCExprVar!>! quantifiedVars = new List<VCExprVar!> ();
+ quantifiedVars.AddRange(freeTypeVars);
+ quantifiedVars.AddRange(boundTypeVars0);
+ quantifiedVars.AddRange(boundTypeVars1);
+ quantifiedVars.Add(val);
+ quantifiedVars.Add(m);
+ quantifiedVars.AddRange(indexes0);
+ quantifiedVars.AddRange(indexes1);
+
+ List<VCTrigger!>! triggers = new List<VCTrigger!> ();
+
+ // different value arguments or different type arguments are sufficient
+ // to conclude that that value of the map at some point (after an update)
+ // has not changed
+
+ List<VCExpr!>! indexEqs = new List<VCExpr!> ();
+ for (int i = 0; i < mapTypeParamNum; ++i)
+ indexEqs.Add(Gen.Eq(boundTypeVars0[i], boundTypeVars1[i]));
+ for (int i = 0; i < arity; ++i)
+ indexEqs.Add(Gen.Eq(indexes0[i], indexes1[i]));
+
+ VCExpr! axiom = VCExpressionGenerator.True;
+ int n = 0;
+ foreach (VCExpr! indexesEq in indexEqs) {
+ VCExpr! matrix = Gen.Or(indexesEq, selectEq);
+ VCExpr! conjunct = Gen.Forall(quantifiedVars, triggers,
+ "mapAx1:" + select.Name + ":" + n, matrix);
+ axiom = Gen.AndSimp(axiom, conjunct);
+ n = n + 1;
+ }
+
+ return axiom;
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ public class TypeEraserArguments : TypeEraser {
+
+ private readonly TypeAxiomBuilderArguments! AxBuilderArguments;
+
+ private OpTypeEraser OpEraserAttr = null;
+ protected override OpTypeEraser! OpEraser { get {
+ if (OpEraserAttr == null)
+ OpEraserAttr = new OpTypeEraserArguments(this, AxBuilderArguments, Gen);
+ return OpEraserAttr;
+ } }
+
+ public TypeEraserArguments(TypeAxiomBuilderArguments! axBuilder,
+ VCExpressionGenerator! gen) {
+ base(axBuilder, gen);
+ this.AxBuilderArguments = axBuilder;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprQuantifier! node,
+ VariableBindings! oldBindings) {
+ VariableBindings! bindings = oldBindings.Clone();
+
+ // bound term variables are replaced with bound term variables
+ // typed in a simpler way
+ List<VCExprVar!>! newBoundVars =
+ BoundVarsAfterErasure(node.BoundVars, bindings);
+
+ // type variables are replaced with ordinary quantified variables
+ GenBoundVarsForTypeParams(node.TypeParameters, newBoundVars, bindings);
+ VCExpr! newNode = HandleQuantifier(node, newBoundVars, bindings);
+
+ if (!(newNode is VCExprQuantifier) || !IsUniversalQuantifier(node))
+ return newNode;
+
+ VariableBindings! bindings2;
+ if (!RedoQuantifier(node, (VCExprQuantifier)newNode, node.BoundVars, oldBindings,
+ out bindings2, out newBoundVars))
+ return newNode;
+
+ GenBoundVarsForTypeParams(node.TypeParameters, newBoundVars, bindings2);
+ return HandleQuantifier(node, newBoundVars, bindings2);
+ }
+
+ private void GenBoundVarsForTypeParams(List<TypeVariable!>! typeParams,
+ List<VCExprVar!>! newBoundVars,
+ VariableBindings! bindings) {
+ foreach (TypeVariable! tvar in typeParams) {
+ VCExprVar! var = Gen.Variable(tvar.Name, AxBuilder.T);
+ newBoundVars.Add(var);
+ bindings.TypeVariableBindings.Add(tvar, var);
+ }
+ }
+
+ private VCExpr! HandleQuantifier(VCExprQuantifier! node,
+ List<VCExprVar!>! newBoundVars,
+ VariableBindings! bindings) {
+ List<VCTrigger!>! newTriggers = MutateTriggers(node.Triggers, bindings);
+ VCExpr! newBody = Mutate(node.Body, bindings);
+ newBody = AxBuilder.Cast(newBody, Type.Bool);
+
+ if (newBoundVars.Count == 0) // might happen that no bound variables are left
+ return newBody;
+ return Gen.Quantify(node.Quan, new List<TypeVariable!> (), newBoundVars,
+ newTriggers, node.Infos, newBody);
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ public class OpTypeEraserArguments : OpTypeEraser {
+
+ protected readonly TypeAxiomBuilderArguments! AxBuilderArguments;
+
+ public OpTypeEraserArguments(TypeEraserArguments! eraser,
+ TypeAxiomBuilderArguments! axBuilder,
+ VCExpressionGenerator! gen) {
+ base(eraser, axBuilder, gen);
+ this.AxBuilderArguments = axBuilder;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private VCExpr! AssembleOpExpression(OpTypesPair opTypes,
+ IEnumerable<VCExpr!>! oldArgs,
+ VariableBindings! bindings) {
+ // UGLY: the code for tracking polarities should be factored out
+ int oldPolarity = Eraser.Polarity;
+ Eraser.Polarity = 0;
+
+ List<VCExpr!>! newArgs = new List<VCExpr!> ();
+ // explicit type parameters
+ foreach (Type! t in opTypes.Types)
+ newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));
+
+ // and the actual value parameters
+ Function! newFun = ((VCExprBoogieFunctionOp)opTypes.Op).Func;
+ // ^ we only allow this operator at this point
+ int i = opTypes.Types.Count;
+ foreach (VCExpr! arg in oldArgs) {
+ newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings),
+ ((!)newFun.InParams[i]).TypedIdent.Type));
+ i = i + 1;
+ }
+
+ Eraser.Polarity = oldPolarity;
+ return Gen.Function(opTypes.Op, newArgs);
+ }
+
+ // for the time being, we store both the types of the arguments and the explicit
+ // type parameters (for most operators, this is more than actually necessary)
+ private OpTypesPair OriginalOpTypes(VCExprNAry! node) {
+ List<Type!>! originalTypes = new List<Type!> ();
+ foreach (VCExpr! expr in node)
+ originalTypes.Add(expr.Type);
+ originalTypes.AddRange(node.TypeArguments);
+ return new OpTypesPair (node.Op, originalTypes);
+ }
+
+ private VCExpr! EqualTypes(Type! t0, Type! t1, VariableBindings! bindings) {
+ if (t0.Equals(t1))
+ return VCExpressionGenerator.True;
+ VCExpr! t0Expr = AxBuilder.Type2Term(t0, bindings.TypeVariableBindings);
+ VCExpr! t1Expr = AxBuilder.Type2Term(t1, bindings.TypeVariableBindings);
+ return Gen.Eq(t0Expr, t1Expr);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! VisitEqOp (VCExprNAry! node, VariableBindings! bindings) {
+ // we also have to state that the types are equal, because the
+ // translation does not contain any information about the
+ // relationship between values and types
+ return Gen.AndSimp(base.VisitEqOp(node, bindings),
+ EqualTypes(node[0].Type, node[1].Type, bindings));
+ }
+
+ public override VCExpr! VisitNeqOp (VCExprNAry! node, VariableBindings! bindings) {
+ // we also have to state that the types are (un)equal, because the
+ // translation does not contain any information about the
+ // relationship between values and types
+ return Gen.OrSimp(base.VisitNeqOp(node, bindings),
+ Gen.Not(EqualTypes(node[0].Type, node[1].Type, bindings)));
+ }
+
+ public override VCExpr! VisitSubtypeOp (VCExprNAry! node, VariableBindings! bindings) {
+ // UGLY: the code for tracking polarities should be factored out
+ int oldPolarity = Eraser.Polarity;
+ Eraser.Polarity = 0;
+
+ VCExpr! res =
+ Gen.Function(VCExpressionGenerator.Subtype3Op,
+ AxBuilder.Type2Term(node[0].Type,
+ bindings.TypeVariableBindings),
+ AxBuilder.Cast(Eraser.Mutate(node[0], bindings),
+ AxBuilder.U),
+ AxBuilder.Cast(Eraser.Mutate(node[1], bindings),
+ AxBuilder.U));
+
+ Eraser.Polarity = oldPolarity;
+ return res;
+ }
+
+ public override VCExpr! VisitSelectOp (VCExprNAry! node, VariableBindings! bindings) {
+ OpTypesPair originalOpTypes = OriginalOpTypes(node);
+ OpTypesPair newOpTypes;
+
+ if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {
+ MapType! rawType = node[0].Type.AsMap;
+ TypeSeq! abstractionInstantiation;
+ Function! select =
+ AxBuilder.MapTypeAbstracter.Select(rawType, out abstractionInstantiation);
+
+ newOpTypes = TypesPairForSelectStore(node, select, abstractionInstantiation);
+ NewOpCache.Add(originalOpTypes, newOpTypes);
+ }
+
+ return AssembleOpExpression(newOpTypes, node, bindings);
+ }
+
+ public override VCExpr! VisitStoreOp (VCExprNAry! node, VariableBindings! bindings) {
+ OpTypesPair originalOpTypes = OriginalOpTypes(node);
+ OpTypesPair newOpTypes;
+
+ if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {
+ MapType! rawType = node[0].Type.AsMap;
+ TypeSeq! abstractionInstantiation;
+ Function! store =
+ AxBuilder.MapTypeAbstracter.Store(rawType, out abstractionInstantiation);
+
+ newOpTypes = TypesPairForSelectStore(node, store, abstractionInstantiation);
+ NewOpCache.Add(originalOpTypes, newOpTypes);
+ }
+
+ return AssembleOpExpression(newOpTypes, node, bindings);
+ }
+
+ private OpTypesPair TypesPairForSelectStore(VCExprNAry! node, Function! untypedOp,
+ // instantiation of the abstract map type parameters
+ TypeSeq! abstractionInstantiation) {
+ List<Type!>! inferredTypeArgs = new List<Type!> ();
+ foreach (Type! t in node.TypeArguments)
+// inferredTypeArgs.Add(AxBuilder.MapTypeAbstracter.AbstractMapTypeRecursively(t));
+ inferredTypeArgs.Add(t);
+ foreach (Type! t in abstractionInstantiation)
+ inferredTypeArgs.Add(t);
+
+ assert untypedOp.InParams.Length == inferredTypeArgs.Count + node.Arity;
+ return new OpTypesPair (Gen.BoogieFunctionOp(untypedOp), inferredTypeArgs);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! VisitBoogieFunctionOp (VCExprNAry! node, VariableBindings! bindings) {
+ OpTypesPair originalOpTypes = OriginalOpTypes(node);
+ OpTypesPair newOpTypes;
+
+ if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {
+ Function! oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;
+
+ List<Type!>! inferredTypeArgs = new List<Type!> ();
+ foreach (Type! t in node.TypeArguments)
+// inferredTypeArgs.Add(AxBuilder.MapTypeAbstracter.AbstractMapTypeRecursively(t));
+ inferredTypeArgs.Add(t);
+
+ VCExprOp! newOp = Gen.BoogieFunctionOp(AxBuilderArguments.Typed2Untyped(oriFun));
+ newOpTypes = new OpTypesPair (newOp, inferredTypeArgs);
+
+ NewOpCache.Add(originalOpTypes, newOpTypes);
+ }
+
+ return AssembleOpExpression(newOpTypes, node, bindings);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ // cache from the typed operators to the untyped operators with
+ // explicit type arguments. the keys are pairs of the typed
+ // operator and the actual types of the argument expressions, the
+ // values are pairs of the new operators and the types that have
+ // to be given as explicit type arguments
+ private readonly IDictionary<OpTypesPair, OpTypesPair>! NewOpCache =
+ new Dictionary<OpTypesPair, OpTypesPair>();
+
+ private struct OpTypesPair {
+ public readonly VCExprOp! Op;
+ public readonly List<Type!>! Types;
+
+ public OpTypesPair(VCExprOp! op, List<Type!>! types) {
+ this.Op = op;
+ this.Types = types;
+ this.HashCode = HFNS.PolyHash(op.GetHashCode(), 17, types);
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (that is OpTypesPair) {
+ OpTypesPair thatPair = (OpTypesPair)that;
+ return this.Op.Equals(thatPair.Op) &&
+ HFNS.SameElements(this.Types, thatPair.Types);
+ }
+ return false;
+ }
+
+ private readonly int HashCode;
+
+ [Pure]
+ public override int GetHashCode() {
+ return HashCode;
+ }
+ }
+ }
+
+}
diff --git a/Source/VCExpr/TypeErasurePremisses.ssc b/Source/VCExpr/TypeErasurePremisses.ssc new file mode 100644 index 00000000..16ec87e6 --- /dev/null +++ b/Source/VCExpr/TypeErasurePremisses.ssc @@ -0,0 +1,1025 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+using Microsoft.Boogie.VCExprAST;
+
+// Erasure of types using premisses (forall x :: type(x)=T ==> p(x))
+
+namespace Microsoft.Boogie.TypeErasure
+{
+ using Microsoft.Boogie.VCExprAST;
+
+ // When using type premisses, we can distinguish two kinds of type
+ // parameters of a function or map: parameters that occur in the
+ // formal argument types of the function are "implicit" because they
+ // can be inferred from the actual argument types; parameters that
+ // only occur in the result type of the function are "explicit"
+ // because they are not inferrable and have to be given to the
+ // function as additional arguments.
+ //
+ // The following structure is used to store the untyped version of a
+ // typed function, together with the lists of implicit and explicit
+ // type parameters (in the same order as they occur in the signature
+ // of the original function).
+
+ internal struct UntypedFunction {
+ public readonly Function! Fun;
+ // type parameters that can be extracted from the value parameters
+ public readonly List<TypeVariable!>! ImplicitTypeParams;
+ // type parameters that have to be given explicitly
+ public readonly List<TypeVariable!>! ExplicitTypeParams;
+
+ public UntypedFunction(Function! fun,
+ List<TypeVariable!>! implicitTypeParams,
+ List<TypeVariable!>! explicitTypeParams) {
+ Fun = fun;
+ ImplicitTypeParams = implicitTypeParams;
+ ExplicitTypeParams = explicitTypeParams;
+ }
+ }
+
+ public class TypeAxiomBuilderPremisses : TypeAxiomBuilderIntBoolU {
+
+ public TypeAxiomBuilderPremisses(VCExpressionGenerator! gen) {
+ base(gen);
+ TypeFunction = HelperFuns.BoogieFunction("dummy", Type.Int);
+ Typed2UntypedFunctions = new Dictionary<Function!, UntypedFunction> ();
+ MapTypeAbstracterAttr = null;
+ }
+
+ // constructor to allow cloning
+ [NotDelayed]
+ internal TypeAxiomBuilderPremisses(TypeAxiomBuilderPremisses! builder) {
+ TypeFunction = builder.TypeFunction;
+ Typed2UntypedFunctions =
+ new Dictionary<Function!, UntypedFunction> (builder.Typed2UntypedFunctions);
+ base(builder);
+
+ MapTypeAbstracterAttr =
+ builder.MapTypeAbstracterAttr == null ?
+ null : new MapTypeAbstractionBuilderPremisses(this, builder.Gen,
+ builder.MapTypeAbstracterAttr);
+ }
+
+ public override Object! Clone() {
+ return new TypeAxiomBuilderPremisses(this);
+ }
+
+ public override void Setup() {
+ TypeFunction = HelperFuns.BoogieFunction("type", U, T);
+ base.Setup();
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // generate axioms of the kind "forall x:U. {Int2U(U2Int(x))}
+ // type(x)=int ==> Int2U(U2Int(x))==x"
+ protected override VCExpr! GenReverseCastAxiom(Function! castToU, Function! castFromU) {
+ List<VCTrigger!>! triggers;
+ VCExprVar! var;
+ VCExpr! eq = GenReverseCastEq(castToU, castFromU, out var, out triggers);
+ VCExpr! premiss;
+ if (CommandLineOptions.Clo.TypeEncodingMethod
+ == CommandLineOptions.TypeEncoding.None)
+ premiss = VCExpressionGenerator.True;
+ else
+ premiss = GenVarTypeAxiom(var, ((!)castFromU.OutParams[0]).TypedIdent.Type,
+ // we don't have any bindings available
+ new Dictionary<TypeVariable!, VCExpr!> ());
+ VCExpr! matrix = Gen.ImpliesSimp(premiss, eq);
+ return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, matrix);
+ }
+
+ protected override VCExpr! GenCastTypeAxioms(Function! castToU, Function! castFromU) {
+ Type! fromType = ((!)castToU.InParams[0]).TypedIdent.Type;
+ return GenFunctionAxiom(castToU, new List<TypeVariable!> (), new List<TypeVariable!> (),
+ HelperFuns.ToList(fromType), fromType);
+ }
+
+ private MapTypeAbstractionBuilderPremisses MapTypeAbstracterAttr;
+
+ internal override MapTypeAbstractionBuilder! MapTypeAbstracter { get {
+ if (MapTypeAbstracterAttr == null)
+ MapTypeAbstracterAttr = new MapTypeAbstractionBuilderPremisses (this, Gen);
+ return MapTypeAbstracterAttr;
+ } }
+
+ internal MapTypeAbstractionBuilderPremisses! MapTypeAbstracterPremisses { get {
+ return (MapTypeAbstractionBuilderPremisses)MapTypeAbstracter;
+ } }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // function that maps individuals to their type
+ // the field is overwritten with its actual value in "Setup"
+ private Function! TypeFunction;
+
+ public VCExpr! TypeOf(VCExpr! expr) {
+ return Gen.Function(TypeFunction, expr);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Generate type premisses and type parameter bindings for quantifiers, functions, procedures
+
+ // let-bindings to extract the instantiations of type parameters
+ public List<VCExprLetBinding!>!
+ GenTypeParamBindings(// the original bound variables and (implicit) type parameters
+ List<TypeVariable!>! typeParams, List<VCExprVar!>! oldBoundVars,
+ // VariableBindings to which the translation
+ // TypeVariable -> VCExprVar is added
+ VariableBindings! bindings) {
+ // type variables are replaced with ordinary variables that are bound using a
+ // let-expression
+ foreach (TypeVariable! tvar in typeParams)
+ bindings.TypeVariableBindings.Add(tvar, Gen.Variable(tvar.Name, T));
+
+ // extract the values of type variables from the term variables
+ List<VCExprVar!>! UtypedVars = new List<VCExprVar!> (oldBoundVars.Count);
+ List<Type!>! originalTypes = new List<Type!> (oldBoundVars.Count);
+ for (int i = 0; i < oldBoundVars.Count; ++i) {
+ VCExprVar! newVar = bindings.VCExprVarBindings[oldBoundVars[i]];
+ if (newVar.Type.Equals(U)) {
+ UtypedVars.Add(newVar);
+ originalTypes.Add(oldBoundVars[i].Type);
+ }
+ }
+
+ UtypedVars.TrimExcess();
+ originalTypes.TrimExcess();
+
+ return BestTypeVarExtractors(typeParams, originalTypes, UtypedVars,
+ bindings);
+ }
+
+
+ public VCExpr! AddTypePremisses(List<VCExprLetBinding!>! typeVarBindings,
+ VCExpr! typePremisses, bool universal,
+ VCExpr! body) {
+ VCExpr! bodyWithPremisses;
+ if (universal)
+ bodyWithPremisses = Gen.ImpliesSimp(typePremisses, body);
+ else
+ bodyWithPremisses = Gen.AndSimp(typePremisses, body);
+
+ return Gen.Let(typeVarBindings, bodyWithPremisses);
+ }
+
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Extract the instantiations of type variables from the concrete types of
+ // term variables. E.g., for a function f<a>(x : C a), we would extract the
+ // instantiation of "a" by looking at the concrete type of "x".
+
+ public List<VCExprLetBinding!>!
+ BestTypeVarExtractors(List<TypeVariable!>! vars, List<Type!>! types,
+ List<VCExprVar!>! concreteTypeSources,
+ VariableBindings! bindings) {
+ List<VCExprLetBinding!>! typeParamBindings = new List<VCExprLetBinding!> ();
+ foreach (TypeVariable! var in vars) {
+ VCExpr extractor = BestTypeVarExtractor(var, types, concreteTypeSources);
+ if (extractor != null)
+ typeParamBindings.Add(
+ Gen.LetBinding((VCExprVar)bindings.TypeVariableBindings[var],
+ extractor));
+ }
+ return typeParamBindings;
+ }
+
+ private VCExpr BestTypeVarExtractor(TypeVariable! var, List<Type!>! types,
+ List<VCExprVar!>! concreteTypeSources) {
+ List<VCExpr!> allExtractors = TypeVarExtractors(var, types, concreteTypeSources);
+ if (allExtractors.Count == 0)
+ return null;
+
+ VCExpr bestExtractor = allExtractors[0];
+ int bestExtractorSize = SizeComputingVisitor.ComputeSize(bestExtractor);
+ for (int i = 1; i < allExtractors.Count; ++i) {
+ int newSize = SizeComputingVisitor.ComputeSize(allExtractors[i]);
+ if (newSize < bestExtractorSize) {
+ bestExtractor = allExtractors[i];
+ bestExtractorSize = newSize;
+ }
+ }
+
+ return bestExtractor;
+ }
+
+ private List<VCExpr!>! TypeVarExtractors(TypeVariable! var, List<Type!>! types,
+ List<VCExprVar!>! concreteTypeSources)
+ requires types.Count == concreteTypeSources.Count; {
+ List<VCExpr!>! res = new List<VCExpr!>();
+ for (int i = 0; i < types.Count; ++i)
+ TypeVarExtractors(var, types[i], TypeOf(concreteTypeSources[i]), res);
+
+ return res;
+ }
+
+ private void TypeVarExtractors(TypeVariable! var, Type! completeType,
+ VCExpr! innerTerm, List<VCExpr!>! extractors) {
+ if (completeType.IsVariable) {
+ if (var.Equals(completeType)) {
+ extractors.Add(innerTerm);
+ } // else nothing
+ } else if (completeType.IsBasic) {
+ // nothing
+ } else if (completeType.IsCtor) {
+ CtorType! ctorType = completeType.AsCtor;
+ if (ctorType.Arguments.Length > 0) {
+ // otherwise there are no chances of extracting any
+ // instantiations from this type
+ TypeCtorRepr repr = GetTypeCtorReprStruct(ctorType.Decl);
+ for (int i = 0; i < ctorType.Arguments.Length; ++i) {
+ VCExpr! newInnerTerm = Gen.Function(repr.Dtors[i], innerTerm);
+ TypeVarExtractors(var, ctorType.Arguments[i], newInnerTerm, extractors);
+ }
+ }
+ } else if (completeType.IsMap) {
+ TypeVarExtractors(var, MapTypeAbstracter.AbstractMapType(completeType.AsMap),
+ innerTerm, extractors);
+ } else {
+ System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + completeType);
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Symbols for representing functions
+
+ // Globally defined functions
+ private readonly IDictionary<Function!, UntypedFunction>! Typed2UntypedFunctions;
+
+ // distinguish between implicit and explicit type parameters
+ internal static void SeparateTypeParams(List<Type!>! valueArgumentTypes,
+ TypeVariableSeq! allTypeParams,
+ out List<TypeVariable!>! implicitParams,
+ out List<TypeVariable!>! explicitParams) {
+ TypeVariableSeq! varsInInParamTypes = new TypeVariableSeq ();
+ foreach (Type! t in valueArgumentTypes)
+ varsInInParamTypes.AppendWithoutDups(t.FreeVariables);
+
+ implicitParams = new List<TypeVariable!> (allTypeParams.Length);
+ explicitParams = new List<TypeVariable!> (allTypeParams.Length);
+
+ foreach (TypeVariable! var in allTypeParams) {
+ if (varsInInParamTypes.Has(var))
+ implicitParams.Add(var);
+ else
+ explicitParams.Add(var);
+ }
+
+ implicitParams.TrimExcess();
+ explicitParams.TrimExcess();
+ }
+
+ internal UntypedFunction Typed2Untyped(Function! fun) {
+ UntypedFunction res;
+ if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {
+ assert fun.OutParams.Length == 1;
+
+ // if all of the parameters are int or bool, the function does
+ // not have to be changed
+ if (forall{Formal f in fun.InParams; UnchangedType(((!)f).TypedIdent.Type)} &&
+ UnchangedType(((!)fun.OutParams[0]).TypedIdent.Type) &&
+ fun.TypeParameters.Length == 0) {
+ res = new UntypedFunction(fun, new List<TypeVariable!> (), new List<TypeVariable!> ());
+ } else {
+ List<Type!>! argTypes = new List<Type!> ();
+ foreach (Variable! v in fun.InParams)
+ argTypes.Add(v.TypedIdent.Type);
+
+ List<TypeVariable!>! implicitParams, explicitParams;
+ SeparateTypeParams(argTypes, fun.TypeParameters, out implicitParams, out explicitParams);
+
+ Type[]! types = new Type [explicitParams.Count + fun.InParams.Length + 1];
+ int i = 0;
+ for (int j = 0; j < explicitParams.Count; ++j) {
+ types[i] = T;
+ i = i + 1;
+ }
+ for (int j = 0; j < fun.InParams.Length; ++i, ++j)
+ types[i] = TypeAfterErasure(((!)fun.InParams[j]).TypedIdent.Type);
+ types[types.Length - 1] = TypeAfterErasure(((!)fun.OutParams[0]).TypedIdent.Type);
+
+ Function! untypedFun = HelperFuns.BoogieFunction(fun.Name, types);
+ untypedFun.Attributes = fun.Attributes;
+ res = new UntypedFunction(untypedFun, implicitParams, explicitParams);
+ if (U.Equals(types[types.Length - 1]))
+ AddTypeAxiom(GenFunctionAxiom(res, fun));
+ }
+
+ Typed2UntypedFunctions.Add(fun, res);
+ }
+ return res;
+ }
+
+ private VCExpr! GenFunctionAxiom(UntypedFunction fun, Function! originalFun) {
+ List<Type!>! originalInTypes = new List<Type!> (originalFun.InParams.Length);
+ foreach (Formal! f in originalFun.InParams)
+ originalInTypes.Add(f.TypedIdent.Type);
+
+ return GenFunctionAxiom(fun.Fun, fun.ImplicitTypeParams, fun.ExplicitTypeParams,
+ originalInTypes,
+ ((!)originalFun.OutParams[0]).TypedIdent.Type);
+ }
+
+ internal VCExpr! GenFunctionAxiom(Function! fun,
+ List<TypeVariable!>! implicitTypeParams,
+ List<TypeVariable!>! explicitTypeParams,
+ List<Type!>! originalInTypes,
+ Type! originalResultType)
+ requires originalInTypes.Count +
+ explicitTypeParams.Count ==
+ fun.InParams.Length; {
+
+ if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {
+ return VCExpressionGenerator.True;
+ }
+
+ List<VCExprVar!>! typedInputVars = new List<VCExprVar!>(originalInTypes.Count);
+ int i = 0;
+ foreach (Type! t in originalInTypes) {
+ typedInputVars.Add(Gen.Variable("arg" + i, t));
+ i = i + 1;
+ }
+
+ VariableBindings! bindings = new VariableBindings ();
+
+ // type parameters that have to be given explicitly are replaced
+ // with universally quantified type variables
+ List<VCExprVar!>! boundVars = new List<VCExprVar!> (explicitTypeParams.Count + typedInputVars.Count);
+ foreach (TypeVariable! var in explicitTypeParams) {
+ VCExprVar! newVar = Gen.Variable(var.Name, T);
+ boundVars.Add(newVar);
+ bindings.TypeVariableBindings.Add(var, newVar);
+ }
+
+
+ // bound term variables are replaced with bound term variables typed in
+ // a simpler way
+ foreach (VCExprVar! var in typedInputVars) {
+ Type! newType = TypeAfterErasure(var.Type);
+ VCExprVar! newVar = Gen.Variable(var.Name, newType);
+ boundVars.Add(newVar);
+ bindings.VCExprVarBindings.Add(var, newVar);
+ }
+
+ List<VCExprLetBinding!>! typeVarBindings =
+ GenTypeParamBindings(implicitTypeParams, typedInputVars, bindings);
+
+ VCExpr! funApp = Gen.Function(fun, HelperFuns.ToVCExprList(boundVars));
+ VCExpr! conclusion = Gen.Eq(TypeOf(funApp),
+ Type2Term(originalResultType, bindings.TypeVariableBindings));
+ VCExpr conclusionWithPremisses =
+ // leave out antecedents of function type axioms ... they don't appear necessary,
+ // because a function can always be extended to all U-values (right?)
+// AddTypePremisses(typeVarBindings, typePremisses, true, conclusion);
+ Gen.Let(typeVarBindings, conclusion);
+
+ if (boundVars.Count > 0) {
+ List<VCTrigger!>! triggers =
+ HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
+ return Gen.Forall(boundVars, triggers,
+ "funType:" + fun.Name, conclusionWithPremisses);
+ } else {
+ return conclusionWithPremisses;
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ protected override void AddVarTypeAxiom(VCExprVar! var, Type! originalType) {
+ if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) return;
+ AddTypeAxiom(GenVarTypeAxiom(var, originalType,
+ // we don't have any bindings available
+ new Dictionary<TypeVariable!, VCExpr!> ()));
+ }
+
+ public VCExpr! GenVarTypeAxiom(VCExprVar! var, Type! originalType,
+ IDictionary<TypeVariable!, VCExpr!>! varMapping) {
+ if (!var.Type.Equals(originalType)) {
+ VCExpr! typeRepr = Type2Term(originalType, varMapping);
+ return Gen.Eq(TypeOf(var), typeRepr);
+ }
+ return VCExpressionGenerator.True;
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////
+
+ internal class MapTypeAbstractionBuilderPremisses : MapTypeAbstractionBuilder {
+
+ private readonly TypeAxiomBuilderPremisses! AxBuilderPremisses;
+
+ internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses! axBuilder,
+ VCExpressionGenerator! gen) {
+ base(axBuilder, gen);
+ this.AxBuilderPremisses = axBuilder;
+ }
+
+ // constructor for cloning
+ internal MapTypeAbstractionBuilderPremisses(TypeAxiomBuilderPremisses! axBuilder,
+ VCExpressionGenerator! gen,
+ MapTypeAbstractionBuilderPremisses! builder) {
+ base(axBuilder, gen, builder);
+ this.AxBuilderPremisses = axBuilder;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Determine the type parameters of a map type that have to be
+ // given explicitly when applying the select function (the
+ // parameters that only occur in the result type of the
+ // map). These parameters are given as a list of indexes sorted in
+ // ascending order; the index i refers to the i'th bound variable
+ // in a type <a0, a1, ..., an>[...]...
+ public List<int>! ExplicitSelectTypeParams(MapType! type) {
+ List<int> res;
+ if (!explicitSelectTypeParamsCache.TryGetValue(type, out res)) {
+ List<TypeVariable!>! explicitParams, implicitParams;
+ TypeAxiomBuilderPremisses.SeparateTypeParams(type.Arguments.ToList(),
+ type.TypeParameters,
+ out implicitParams,
+ out explicitParams);
+ res = new List<int> (explicitParams.Count);
+ foreach (TypeVariable! var in explicitParams)
+ res.Add(type.TypeParameters.IndexOf(var));
+ explicitSelectTypeParamsCache.Add(type, res);
+ }
+ return (!)res;
+ }
+
+ private IDictionary<MapType!, List<int>!>! explicitSelectTypeParamsCache =
+ new Dictionary<MapType!, List<int>!> ();
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ protected override void GenSelectStoreFunctions(MapType! abstractedType,
+ TypeCtorDecl! synonym,
+ out Function! select,
+ out Function! store) {
+ Type! mapTypeSynonym;
+ List<TypeVariable!>! typeParams;
+ List<Type!>! originalInTypes;
+ GenTypeAxiomParams(abstractedType, synonym, out mapTypeSynonym,
+ out typeParams, out originalInTypes);
+
+ // select
+ List<TypeVariable!>! explicitSelectParams;
+ select = CreateAccessFun(typeParams, originalInTypes,
+ abstractedType.Result, synonym.Name + "Select",
+ out explicitSelectParams);
+
+ // store, which gets one further argument: the assigned rhs
+ originalInTypes.Add(abstractedType.Result);
+
+ List<TypeVariable!>! explicitStoreParams;
+ store = CreateAccessFun(typeParams, originalInTypes,
+ mapTypeSynonym, synonym.Name + "Store",
+ out explicitStoreParams);
+
+ // the store function does not have any explicit type parameters
+ assert explicitStoreParams.Count == 0;
+
+ AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,
+ abstractedType.Result,
+ explicitSelectParams));
+ AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store,
+ abstractedType.Result,
+ explicitSelectParams));
+ }
+
+ protected void GenTypeAxiomParams(MapType! abstractedType, TypeCtorDecl! synonymDecl,
+ out Type! mapTypeSynonym,
+ out List<TypeVariable!>! typeParams,
+ out List<Type!>! originalIndexTypes) {
+ typeParams = new List<TypeVariable!> (abstractedType.TypeParameters.Length + abstractedType.FreeVariables.Length);
+ typeParams.AddRange(abstractedType.TypeParameters.ToList());
+ typeParams.AddRange(abstractedType.FreeVariables.ToList());
+
+ originalIndexTypes = new List<Type!> (abstractedType.Arguments.Length + 1);
+ TypeSeq! mapTypeParams = new TypeSeq ();
+ foreach (TypeVariable! var in abstractedType.FreeVariables)
+ mapTypeParams.Add(var);
+ mapTypeSynonym = new CtorType (Token.NoToken, synonymDecl, mapTypeParams);
+ originalIndexTypes.Add(mapTypeSynonym);
+ originalIndexTypes.AddRange(abstractedType.Arguments.ToList());
+ }
+
+ // method to actually create the select or store function
+ private Function! CreateAccessFun(List<TypeVariable!>! originalTypeParams,
+ List<Type!>! originalInTypes,
+ Type! originalResult,
+ string! name,
+ out List<TypeVariable!>! explicitTypeParams) {
+ // select and store are basically handled like normal functions: the type
+ // parameters are split into the implicit parameters, and into the parameters
+ // that have to be given explicitly
+ List<TypeVariable!>! implicitParams;
+ TypeAxiomBuilderPremisses.SeparateTypeParams(originalInTypes,
+ HelperFuns.ToSeq(originalTypeParams),
+ out implicitParams,
+ out explicitTypeParams);
+ Type[]! ioTypes = new Type [explicitTypeParams.Count + originalInTypes.Count + 1];
+ int i = 0;
+ for (; i < explicitTypeParams.Count; ++i)
+ ioTypes[i] = AxBuilder.T;
+ foreach (Type! type in originalInTypes)
+ {
+ if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type))
+ ioTypes[i] = type;
+ else
+ ioTypes[i] = AxBuilder.U;
+ i++;
+ }
+ if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(originalResult))
+ ioTypes[i] = originalResult;
+ else
+ ioTypes[i] = AxBuilder.U;
+
+ Function! res = HelperFuns.BoogieFunction(name, ioTypes);
+
+ if (AxBuilder.U.Equals(ioTypes[i]))
+ {
+ AxBuilder.AddTypeAxiom(
+ AxBuilderPremisses.GenFunctionAxiom(res,
+ implicitParams, explicitTypeParams,
+ originalInTypes, originalResult));
+ }
+ return res;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // The normal axioms of the theory of arrays (without extensionality)
+
+ private VCExpr! Select(Function! select,
+ // in general, the select function has to
+ // receive explicit type parameters (which
+ // are here already represented as VCExpr
+ // of type T)
+ List<VCExpr!>! typeParams,
+ VCExpr! map,
+ List<VCExprVar!>! indexes) {
+ List<VCExpr!>! selectArgs = new List<VCExpr!> (typeParams.Count + indexes.Count + 1);
+ selectArgs.AddRange(typeParams);
+ selectArgs.Add(map);
+ selectArgs.AddRange(HelperFuns.ToVCExprList(indexes));
+ return Gen.Function(select, selectArgs);
+ }
+
+ private VCExpr! Store(Function! store,
+ VCExpr! map,
+ List<VCExprVar!>! indexes,
+ VCExpr! val) {
+ List<VCExpr!>! storeArgs = new List<VCExpr!> (indexes.Count + 2);
+ storeArgs.Add(map);
+ storeArgs.AddRange(HelperFuns.ToVCExprList(indexes));
+ storeArgs.Add(val);
+ return Gen.Function(store, storeArgs);
+ }
+
+ private VCExpr! GenMapAxiom0(Function! select, Function! store,
+ Type! mapResult,
+ List<TypeVariable!>! explicitSelectParams) {
+ int arity = store.InParams.Length - 2;
+ VCExprVar! typedVal = Gen.Variable("val", mapResult);
+ VCExprVar! val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type);
+
+ VariableBindings! bindings = new VariableBindings ();
+ bindings.VCExprVarBindings.Add(typedVal, val);
+
+ // explicit type parameters are handled using a let-binder
+ List<VCExprLetBinding!>! letBindings =
+ AxBuilderPremisses.GenTypeParamBindings(explicitSelectParams,
+ HelperFuns.ToList(typedVal),
+ bindings);
+ List<VCExpr!>! typeParams = new List<VCExpr!> (explicitSelectParams.Count);
+ foreach (TypeVariable! var in explicitSelectParams)
+ typeParams.Add(bindings.TypeVariableBindings[var]);
+
+ List<Type!> indexTypes = new List<Type!>();
+ for (int i = 1; i < store.InParams.Length-1; i++)
+ {
+ indexTypes.Add(((!)store.InParams[i]).TypedIdent.Type);
+ }
+ assert arity == indexTypes.Count;
+
+ List<VCExprVar!> indexes = HelperFuns.VarVector("x", indexTypes, Gen);
+ VCExprVar! m = Gen.Variable("m", AxBuilder.U);
+
+ VCExpr! storeExpr = Store(store, m, indexes, val);
+ VCExpr! selectExpr = Select(select, typeParams, storeExpr, indexes);
+
+ List<VCExprVar!>! quantifiedVars = new List<VCExprVar!> (indexes.Count + 2);
+ quantifiedVars.Add(val);
+ quantifiedVars.Add(m);
+ quantifiedVars.AddRange(indexes);
+
+ VCExpr! eq = Gen.Eq(selectExpr, val);
+ VCExpr! letEq = Gen.Let(letBindings, eq);
+ return Gen.Forall(quantifiedVars, new List<VCTrigger!> (),
+ "mapAx0:" + select.Name, letEq);
+ }
+
+ private VCExpr! GenMapAxiom1(Function! select, Function! store,
+ Type! mapResult,
+ List<TypeVariable!>! explicitSelectParams) {
+ int arity = store.InParams.Length - 2;
+
+ List<Type!> indexTypes = new List<Type!>();
+ for (int i = 1; i < store.InParams.Length-1; i++)
+ {
+ indexTypes.Add(((!)store.InParams[i]).TypedIdent.Type);
+ }
+ assert indexTypes.Count == arity;
+
+ List<VCExprVar!>! indexes0 = HelperFuns.VarVector("x", indexTypes, Gen);
+ List<VCExprVar!>! indexes1 = HelperFuns.VarVector("y", indexTypes, Gen);
+ VCExprVar! m = Gen.Variable("m", AxBuilder.U);
+ VCExprVar! val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type);
+
+ // extract the explicit type parameters from the actual result type ...
+ VCExprVar! typedVal = Gen.Variable("val", mapResult);
+ VariableBindings! bindings = new VariableBindings ();
+ bindings.VCExprVarBindings.Add(typedVal, val);
+
+ List<VCExprLetBinding!>! letBindings =
+ AxBuilderPremisses.GenTypeParamBindings(explicitSelectParams,
+ HelperFuns.ToList(typedVal),
+ bindings);
+
+ // ... and quantify the introduced term variables for type
+ // parameters universally
+ List<VCExprVar!>! typeParams = new List<VCExprVar!> (explicitSelectParams.Count);
+ List<VCExpr!>! typeParamsExpr = new List<VCExpr!> (explicitSelectParams.Count);
+ foreach (TypeVariable! var in explicitSelectParams) {
+ VCExprVar! newVar = (VCExprVar)bindings.TypeVariableBindings[var];
+ typeParams.Add(newVar);
+ typeParamsExpr.Add(newVar);
+ }
+
+ VCExpr! storeExpr = Store(store, m, indexes0, val);
+ VCExpr! selectWithoutStoreExpr = Select(select, typeParamsExpr, m, indexes1);
+ VCExpr! selectExpr = Select(select, typeParamsExpr, storeExpr, indexes1);
+
+ VCExpr! selectEq = Gen.Eq(selectExpr, selectWithoutStoreExpr);
+
+ List<VCExprVar!>! quantifiedVars = new List<VCExprVar!> (indexes0.Count + indexes1.Count + 2);
+ quantifiedVars.Add(val);
+ quantifiedVars.Add(m);
+ quantifiedVars.AddRange(indexes0);
+ quantifiedVars.AddRange(indexes1);
+ quantifiedVars.AddRange(typeParams);
+
+ List<VCTrigger!>! triggers = new List<VCTrigger!> ();
+
+ VCExpr! axiom = VCExpressionGenerator.True;
+
+ // first non-interference criterium: the queried location is
+ // different from the assigned location
+ for (int i = 0; i < arity; ++i) {
+ VCExpr! indexesEq = Gen.Eq(indexes0[i], indexes1[i]);
+ VCExpr! matrix = Gen.Or(indexesEq, selectEq);
+ VCExpr! conjunct = Gen.Forall(quantifiedVars, triggers,
+ "mapAx1:" + select.Name + ":" + i, matrix);
+ axiom = Gen.AndSimp(axiom, conjunct);
+ }
+
+ // second non-interference criterion: the queried type is
+ // different from the assigned type
+ VCExpr! typesEq = VCExpressionGenerator.True;
+ foreach (VCExprLetBinding! b in letBindings)
+ typesEq = Gen.AndSimp(typesEq, Gen.Eq(b.V, b.E));
+ VCExpr! matrix2 = Gen.Or(typesEq, selectEq);
+ VCExpr! conjunct2 = Gen.Forall(quantifiedVars, triggers,
+ "mapAx2:" + select.Name, matrix2);
+ axiom = Gen.AndSimp(axiom, conjunct2);
+
+ return axiom;
+ }
+
+ }
+
+ /////////////////////////////////////////////////////////////////////////////
+
+ public class TypeEraserPremisses : TypeEraser {
+
+ private readonly TypeAxiomBuilderPremisses! AxBuilderPremisses;
+
+ private OpTypeEraser OpEraserAttr = null;
+ protected override OpTypeEraser! OpEraser { get {
+ if (OpEraserAttr == null)
+ OpEraserAttr = new OpTypeEraserPremisses(this, AxBuilderPremisses, Gen);
+ return OpEraserAttr;
+ } }
+
+ public TypeEraserPremisses(TypeAxiomBuilderPremisses! axBuilder,
+ VCExpressionGenerator! gen) {
+ base(axBuilder, gen);
+ this.AxBuilderPremisses = axBuilder;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public override VCExpr! Visit(VCExprQuantifier! node,
+ VariableBindings! oldBindings) {
+ VariableBindings bindings = oldBindings.Clone();
+
+ // determine the bound vars that actually occur in the body or
+ // in any of the triggers (if some variables do not occur, we
+ // need to take special care of type parameters that only occur
+ // in the types of such variables)
+ FreeVariableCollector coll = new FreeVariableCollector ();
+ coll.Collect(node.Body);
+ foreach (VCTrigger trigger in node.Triggers) {
+ if (trigger.Pos)
+ foreach (VCExpr! e in trigger.Exprs)
+ coll.Collect(e);
+ }
+
+ List<VCExprVar!> occurringVars = new List<VCExprVar!> (node.BoundVars.Count);
+ foreach (VCExprVar var in node.BoundVars)
+ if (coll.FreeTermVars.ContainsKey(var))
+ occurringVars.Add(var);
+
+ occurringVars.TrimExcess();
+
+ // bound term variables are replaced with bound term variables typed in
+ // a simpler way
+ List<VCExprVar!>! newBoundVars =
+ BoundVarsAfterErasure(occurringVars, bindings);
+ VCExpr! newNode = HandleQuantifier(node, occurringVars,
+ newBoundVars, bindings);
+
+ if (!(newNode is VCExprQuantifier) || !IsUniversalQuantifier(node))
+ return newNode;
+
+ VariableBindings! bindings2;
+ if (!RedoQuantifier(node, (VCExprQuantifier)newNode, occurringVars, oldBindings,
+ out bindings2, out newBoundVars))
+ return newNode;
+
+ return HandleQuantifier(node, occurringVars,
+ newBoundVars, bindings2);
+ }
+
+ private VCExpr! GenTypePremisses(List<VCExprVar!>! oldBoundVars,
+ List<VCExprVar!>! newBoundVars,
+ IDictionary<TypeVariable!, VCExpr!>!
+ typeVarTranslation,
+ List<VCExprLetBinding!>! typeVarBindings,
+ out List<VCTrigger!>! triggers) {
+ // build a substitution of the type variables that it can be checked
+ // whether type premisses are trivial
+ VCExprSubstitution! typeParamSubstitution = new VCExprSubstitution ();
+ foreach (VCExprLetBinding! binding in typeVarBindings)
+ typeParamSubstitution[binding.V] = binding.E;
+ SubstitutingVCExprVisitor! substituter = new SubstitutingVCExprVisitor (Gen);
+
+ List<VCExpr!>! typePremisses = new List<VCExpr!> (newBoundVars.Count);
+ triggers = new List<VCTrigger!> (newBoundVars.Count);
+
+ for (int i = 0; i < newBoundVars.Count; ++i) {
+ VCExprVar! oldVar = oldBoundVars[i];
+ VCExprVar! newVar = newBoundVars[i];
+
+ VCExpr! typePremiss =
+ AxBuilderPremisses.GenVarTypeAxiom(newVar, oldVar.Type,
+ typeVarTranslation);
+
+ if (!IsTriviallyTrue(substituter.Mutate(typePremiss,
+ typeParamSubstitution))) {
+ typePremisses.Add(typePremiss);
+ // generate a negative trigger for the variable occurrence
+ // in the type premiss
+ triggers.Add(Gen.Trigger(false,
+ HelperFuns.ToList(AxBuilderPremisses.TypeOf(newVar))));
+ }
+ }
+
+ typePremisses.TrimExcess();
+ triggers.TrimExcess();
+
+ return Gen.NAry(VCExpressionGenerator.AndOp, typePremisses);
+ }
+
+ // these optimisations should maybe be moved into a separate
+ // visitor (peep-hole optimisations)
+ private bool IsTriviallyTrue(VCExpr! expr) {
+ if (expr.Equals(VCExpressionGenerator.True))
+ return true;
+
+ if (expr is VCExprNAry) {
+ VCExprNAry! naryExpr = (VCExprNAry)expr;
+ if (naryExpr.Op.Equals(VCExpressionGenerator.EqOp) &&
+ naryExpr[0].Equals(naryExpr[1]))
+ return true;
+ }
+
+ return false;
+ }
+
+ private VCExpr! HandleQuantifier(VCExprQuantifier! node,
+ List<VCExprVar!>! occurringVars,
+ List<VCExprVar!>! newBoundVars,
+ VariableBindings! bindings) {
+ List<VCExprLetBinding!>! typeVarBindings =
+ AxBuilderPremisses.GenTypeParamBindings(node.TypeParameters,
+ occurringVars, bindings);
+
+ // Check whether some of the type parameters could not be
+ // determined from the bound variable types. In this case, we
+ // quantify explicitly over these variables
+ if (typeVarBindings.Count < node.TypeParameters.Count) {
+ foreach (TypeVariable! var in node.TypeParameters) {
+ if (!exists{VCExprLetBinding! b in typeVarBindings; b.V.Equals(var)})
+ newBoundVars.Add((VCExprVar)bindings.TypeVariableBindings[var]);
+ }
+ }
+
+ // the lists of old and new bound variables for which type
+ // antecedents are to be generated
+ List<VCExprVar!>! varsWithTypeSpecs = new List<VCExprVar!> ();
+ List<VCExprVar!>! newVarsWithTypeSpecs = new List<VCExprVar!> ();
+ if (!IsUniversalQuantifier(node) ||
+ CommandLineOptions.Clo.TypeEncodingMethod
+ == CommandLineOptions.TypeEncoding.Predicates) {
+ foreach (VCExprVar! oldVar in occurringVars) {
+ varsWithTypeSpecs.Add(oldVar);
+ newVarsWithTypeSpecs.Add(bindings.VCExprVarBindings[oldVar]);
+ }
+ } // else, no type antecedents are created for any variables
+
+ List<VCTrigger!>! furtherTriggers;
+ VCExpr! typePremisses =
+ GenTypePremisses(varsWithTypeSpecs, newVarsWithTypeSpecs,
+ bindings.TypeVariableBindings,
+ typeVarBindings, out furtherTriggers);
+
+ List<VCTrigger!>! newTriggers = MutateTriggers(node.Triggers, bindings);
+ newTriggers.AddRange(furtherTriggers);
+ newTriggers = AddLets2Triggers(newTriggers, typeVarBindings);
+
+ VCExpr! newBody = Mutate(node.Body, bindings);
+
+ // assemble the new quantified formula
+
+ if (CommandLineOptions.Clo.TypeEncodingMethod
+ == CommandLineOptions.TypeEncoding.None) {
+ typePremisses = VCExpressionGenerator.True;
+ }
+
+ VCExpr! bodyWithPremisses =
+ AxBuilderPremisses.AddTypePremisses(typeVarBindings, typePremisses,
+ node.Quan == Quantifier.ALL,
+ AxBuilder.Cast(newBody, Type.Bool));
+
+ if (newBoundVars.Count == 0) // might happen that no bound variables are left
+ return bodyWithPremisses;
+
+ foreach(VCExprVar! v in newBoundVars) {
+ if (v.Type == AxBuilderPremisses.U) {
+ newTriggers.Add(Gen.Trigger(false, AxBuilderPremisses.Cast(v, Type.Int)));
+ newTriggers.Add(Gen.Trigger(false, AxBuilderPremisses.Cast(v, Type.Bool)));
+ }
+ }
+
+ return Gen.Quantify(node.Quan, new List<TypeVariable!> (), newBoundVars,
+ newTriggers, node.Infos, bodyWithPremisses);
+ }
+
+ // check whether we need to add let-binders for any of the type
+ // parameters to the triggers (otherwise, the triggers will
+ // contain unbound/dangling variables for such parameters)
+ private List<VCTrigger!>! AddLets2Triggers(List<VCTrigger!>! triggers,
+ List<VCExprLetBinding!>! typeVarBindings) {
+ List<VCTrigger!>! triggersWithLets = new List<VCTrigger!> (triggers.Count);
+
+ foreach (VCTrigger! t in triggers) {
+ List<VCExpr!>! exprsWithLets = new List<VCExpr!> (t.Exprs.Count);
+
+ bool changed = false;
+ foreach (VCExpr! e in t.Exprs) {
+ Dictionary<VCExprVar!,object>! freeVars =
+ FreeVariableCollector.FreeTermVariables(e);
+
+ if (exists{VCExprLetBinding! b in typeVarBindings;
+ freeVars.ContainsKey(b.V)}) {
+ exprsWithLets.Add(Gen.Let(typeVarBindings, e));
+ changed = true;
+ } else {
+ exprsWithLets.Add(e);
+ }
+ }
+
+ if (changed)
+ triggersWithLets.Add(Gen.Trigger(t.Pos, exprsWithLets));
+ else
+ triggersWithLets.Add(t);
+ }
+
+ return triggersWithLets;
+ }
+
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ public class OpTypeEraserPremisses : OpTypeEraser {
+
+ private TypeAxiomBuilderPremisses! AxBuilderPremisses;
+
+ public OpTypeEraserPremisses(TypeEraserPremisses! eraser,
+ TypeAxiomBuilderPremisses! axBuilder,
+ VCExpressionGenerator! gen) {
+ base(eraser, axBuilder, gen);
+ this.AxBuilderPremisses = axBuilder;
+ }
+
+ private VCExpr! HandleFunctionOp(Function! newFun,
+ List<Type!>! typeArgs,
+ IEnumerable<VCExpr!>! oldArgs,
+ VariableBindings! bindings) {
+ // UGLY: the code for tracking polarities should be factored out
+ int oldPolarity = Eraser.Polarity;
+ Eraser.Polarity = 0;
+
+ List<VCExpr!>! newArgs = new List<VCExpr!> (typeArgs.Count);
+
+ // translate the explicit type arguments
+ foreach (Type! t in typeArgs)
+ newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));
+
+ // recursively translate the value arguments
+ foreach (VCExpr! arg in oldArgs) {
+ Type! newType = ((!)newFun.InParams[newArgs.Count]).TypedIdent.Type;
+ newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings), newType));
+ }
+
+ Eraser.Polarity = oldPolarity;
+ return Gen.Function(newFun, newArgs);
+ }
+
+ public override VCExpr! VisitSelectOp (VCExprNAry! node,
+ VariableBindings! bindings) {
+ MapType! mapType = node[0].Type.AsMap;
+ TypeSeq! instantiations; // not used
+ Function! select =
+ AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations);
+
+ List<int>! explicitTypeParams =
+ AxBuilderPremisses.MapTypeAbstracterPremisses
+ .ExplicitSelectTypeParams(mapType);
+ assert select.InParams.Length == explicitTypeParams.Count + node.Arity;
+
+ List<Type!>! typeArgs = new List<Type!> (explicitTypeParams.Count);
+ foreach (int i in explicitTypeParams)
+ typeArgs.Add(node.TypeArguments[i]);
+ return HandleFunctionOp(select, typeArgs, node, bindings);
+ }
+
+ public override VCExpr! VisitStoreOp (VCExprNAry! node,
+ VariableBindings! bindings) {
+ TypeSeq! instantiations; // not used
+ Function! store =
+ AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out instantiations);
+ return HandleFunctionOp(store,
+ // the store function never has explicit
+ // type parameters
+ new List<Type!> (),
+ node, bindings);
+ }
+
+ public override VCExpr! VisitBoogieFunctionOp (VCExprNAry! node,
+ VariableBindings! bindings) {
+ Function! oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;
+ UntypedFunction untypedFun = AxBuilderPremisses.Typed2Untyped(oriFun);
+ assert untypedFun.Fun.InParams.Length ==
+ untypedFun.ExplicitTypeParams.Count + node.Arity;
+
+ List<Type!>! typeArgs =
+ ExtractTypeArgs(node,
+ oriFun.TypeParameters, untypedFun.ExplicitTypeParams);
+ return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings);
+ }
+
+ private List<Type!>! ExtractTypeArgs(VCExprNAry! node,
+ TypeVariableSeq! allTypeParams,
+ List<TypeVariable!>! explicitTypeParams) {
+ List<Type!>! res = new List<Type!> (explicitTypeParams.Count);
+ foreach (TypeVariable! var in explicitTypeParams)
+ // this lookup could be optimised
+ res.Add(node.TypeArguments[allTypeParams.IndexOf(var)]);
+ return res;
+ }
+ }
+
+
+}
diff --git a/Source/VCExpr/VCExpr.sscproj b/Source/VCExpr/VCExpr.sscproj new file mode 100644 index 00000000..3f3a903a --- /dev/null +++ b/Source/VCExpr/VCExpr.sscproj @@ -0,0 +1,141 @@ +<?xml version="1.0" encoding="utf-8"?>
+<VisualStudioProject>
+ <XEN ProjectType="Local"
+ SchemaVersion="1.0"
+ Name="VCExpr"
+ ProjectGuid="cf42b700-10aa-4da9-8992-48a800251c11"
+ >
+ <Build>
+ <Settings ApplicationIcon=""
+ AssemblyName="VCExpr"
+ OutputType="Library"
+ RootNamespace="VCExpr"
+ StartupObject=""
+ StandardLibraryLocation=""
+ TargetPlatform="v2"
+ TargetPlatformLocation=""
+ >
+ <Config Name="Debug"
+ AllowUnsafeBlocks="False"
+ BaseAddress="285212672"
+ CheckForOverflowUnderflow="False"
+ ConfigurationOverrideFile=""
+ DefineConstants="DEBUG;TRACE"
+ DocumentationFile=""
+ DebugSymbols="True"
+ FileAlignment="4096"
+ IncrementalBuild="True"
+ Optimize="False"
+ OutputPath="bin\debug"
+ RegisterForComInterop="False"
+ RemoveIntegerChecks="false"
+ TreatWarningsAsErrors="False"
+ WarningLevel="4"
+ CheckContractAdmissibility="True"
+ CheckPurity="False"
+ />
+ <Config Name="Release"
+ AllowUnsafeBlocks="false"
+ BaseAddress="285212672"
+ CheckForOverflowUnderflow="false"
+ ConfigurationOverrideFile=""
+ DefineConstants="TRACE"
+ DocumentationFile=""
+ DebugSymbols="false"
+ FileAlignment="4096"
+ IncrementalBuild="false"
+ Optimize="true"
+ OutputPath="bin\release"
+ RegisterForComInterop="false"
+ RemoveIntegerChecks="false"
+ TreatWarningsAsErrors="false"
+ WarningLevel="4"
+ CheckContractAdmissibility="True"
+ CheckPurity="False"
+ />
+ </Settings>
+ <References>
+ <Reference Name="System"
+ AssemblyName="System"
+ Private="false"
+ />
+ <Reference Name="System.Data"
+ AssemblyName="System.Data"
+ Private="false"
+ />
+ <Reference Name="System.Xml"
+ AssemblyName="System.Xml"
+ Private="false"
+ />
+ <Reference Name="Core"
+ Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
+ Private="true"
+ />
+ <Reference Name="Basetypes"
+ Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
+ Private="true"
+ />
+ </References>
+ </Build>
+ <Files>
+ <Include>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="VCExprAST.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="VCExprASTVisitors.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Boogie2VCExpr.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="VCExprASTPrinter.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="SimplifyLikeLineariser.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="TypeErasure.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="NameClashResolver.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="LetBindingSorter.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="TypeErasurePremisses.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="TypeErasureArguments.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="TermFormulaFlattening.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Clustering.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="BigLiteralAbstracter.ssc"
+ />
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="..\version.ssc"
+ />
+ </Include>
+ </Files>
+ </XEN>
+</VisualStudioProject>
\ No newline at end of file diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc new file mode 100644 index 00000000..330c76c4 --- /dev/null +++ b/Source/VCExpr/VCExprAST.ssc @@ -0,0 +1,1285 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+
+// Prover-independent syntax trees for representing verification conditions
+// The language can be seen as a simple polymorphically typed first-order logic,
+// very similar to the expression language of Boogie
+
+namespace Microsoft.Boogie
+{
+ using Microsoft.Boogie.VCExprAST;
+
+ public class VCExpressionGenerator
+ {
+ public static readonly VCExpr! False = new VCExprLiteral (Type.Bool);
+ public static readonly VCExpr! True = new VCExprLiteral (Type.Bool);
+
+ public VCExpr! Integer(BigNum x) {
+ return new VCExprIntLit(x);
+ }
+
+ public VCExpr! Function(VCExprOp! op,
+ List<VCExpr!>! arguments,
+ List<Type!>! typeArguments) {
+ if (typeArguments.Count > 0)
+ return new VCExprMultiAry(op, arguments, typeArguments);
+
+ switch (arguments.Count) {
+ case 0: return new VCExprNullary(op);
+ case 1: return new VCExprUnary(op, arguments);
+ case 2: return new VCExprBinary(op, arguments);
+ default: return new VCExprMultiAry(op, arguments);
+ }
+ }
+
+ public VCExpr! Function(VCExprOp! op, List<VCExpr!>! arguments) {
+ return Function(op, arguments, VCExprNAry.EMPTY_TYPE_LIST);
+ }
+
+ public VCExpr! Function(VCExprOp! op, params VCExpr[]! arguments)
+ requires forall{int i in (0:arguments.Length); arguments[i] != null};
+ {
+ return Function(op,
+ HelperFuns.ToNonNullList(arguments),
+ VCExprNAry.EMPTY_TYPE_LIST);
+ }
+
+ public VCExpr! Function(VCExprOp! op, VCExpr[]! arguments, Type[]! typeArguments)
+ requires forall{int i in (0:arguments.Length); arguments[i] != null};
+ requires forall{int i in (0:typeArguments.Length); typeArguments[i] != null};
+ {
+ return Function(op,
+ HelperFuns.ToNonNullList(arguments),
+ HelperFuns.ToNonNullList(typeArguments));
+ }
+
+ public VCExpr! Function(Function! op, List<VCExpr!>! arguments) {
+ return Function(BoogieFunctionOp(op), arguments, VCExprNAry.EMPTY_TYPE_LIST);
+ }
+
+ public VCExpr! Function(Function! op, params VCExpr[]! arguments)
+ requires forall{int i in (0:arguments.Length); arguments[i] != null};
+ {
+ return Function(BoogieFunctionOp(op), arguments);
+ }
+
+
+ // The following method should really be called "ReduceLeft". It must
+ // only be used for the binary operators "and" and "or"
+ public VCExpr! NAry(VCExprOp! op, List<VCExpr!>! args) {
+ return NAry(op, args.ToArray());
+ }
+
+ public VCExpr! NAry(VCExprOp! op, params VCExpr[]! args)
+ requires forall{int i in (0:args.Length); args[i] != null};
+ requires op == AndOp || op == OrOp; {
+ bool and = (op == AndOp);
+
+ VCExpr! e = and ? True : False;
+ foreach (VCExpr a in args) {
+ e = and ? AndSimp(e, (!)a) : OrSimp(e, (!)a);
+ }
+ return e;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////
+
+ public static readonly VCExprOp! NotOp = new VCExprNAryOp (1, Type.Bool);
+ public static readonly VCExprOp! EqOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp! NeqOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp! AndOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp! OrOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp! ImpliesOp = new VCExprNAryOp (2, Type.Bool);
+
+ public VCExprDistinctOp! DistinctOp(int arity) {
+ return new VCExprDistinctOp (arity);
+ }
+
+ public VCExpr! Not(List<VCExpr!>! args)
+ requires args.Count == 1; {
+ return Function(NotOp, args);
+ }
+
+ public VCExpr! Not(VCExpr! e0) {
+ return Function(NotOp, e0);
+ }
+ public VCExpr! Eq(VCExpr! e0, VCExpr! e1) {
+ return Function(EqOp, e0, e1);
+ }
+ public VCExpr! Neq(VCExpr! e0, VCExpr! e1) {
+ return Function(NeqOp, e0, e1);
+ }
+ public VCExpr! And(VCExpr! e0, VCExpr! e1) {
+ return Function(AndOp, e0, e1);
+ }
+ public VCExpr! Or(VCExpr! e0, VCExpr! e1) {
+ return Function(OrOp, e0, e1);
+ }
+ public VCExpr! Implies(VCExpr! e0, VCExpr! e1) {
+ return Function(ImpliesOp, e0, e1);
+ }
+ public VCExpr! Distinct(List<VCExpr!>! args) {
+ if (args.Count <= 1)
+ // trivial case
+ return True;
+ return Function(DistinctOp(args.Count), args);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // Versions of the propositional operators that automatically simplify in
+ // certain cases (if one of the operators is True or False)
+
+ public VCExpr! NotSimp(VCExpr! e0) {
+ if (e0.Equals(True))
+ return False;
+ if (e0.Equals(False))
+ return True;
+ return Not(e0);
+ }
+ public VCExpr! AndSimp(VCExpr! e0, VCExpr! e1) {
+ if (e0.Equals(True))
+ return e1;
+ if (e1.Equals(True))
+ return e0;
+ if (e0.Equals(False) || e1.Equals(False))
+ return False;
+ return And(e0, e1);
+ }
+ public VCExpr! OrSimp(VCExpr! e0, VCExpr! e1) {
+ if (e0.Equals(False))
+ return e1;
+ if (e1.Equals(False))
+ return e0;
+ if (e0.Equals(True) || e1.Equals(True))
+ return True;
+ return Or(e0, e1);
+ }
+ public VCExpr! ImpliesSimp(VCExpr! e0, VCExpr! e1) {
+ if (e0.Equals(True))
+ return e1;
+ if (e1.Equals(False))
+ return NotSimp(e0);
+ if (e0.Equals(False) || e1.Equals(True))
+ return True;
+ return Implies(e0, e1);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////
+ // Further operators
+
+ public static readonly VCExprOp! AddOp = new VCExprNAryOp (2, Type.Int);
+ public static readonly VCExprOp! SubOp = new VCExprNAryOp (2, Type.Int);
+ public static readonly VCExprOp! MulOp = new VCExprNAryOp (2, Type.Int);
+ public static readonly VCExprOp! DivOp = new VCExprNAryOp (2, Type.Int);
+ public static readonly VCExprOp! ModOp = new VCExprNAryOp (2, Type.Int);
+ public static readonly VCExprOp! LtOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp! LeOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp! GtOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp! GeOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp! SubtypeOp = new VCExprNAryOp (2, Type.Bool);
+ // ternary version of the subtype operator, the first argument of which gives
+ // the type of the compared terms
+ public static readonly VCExprOp! Subtype3Op = new VCExprNAryOp (3, Type.Bool);
+
+ public VCExprOp! BoogieFunctionOp(Function! func) {
+ return new VCExprBoogieFunctionOp(func);
+ }
+
+ // Bitvector nodes
+
+ public VCExpr! Bitvector(BvConst! bv) {
+ return Function(new VCExprBvOp(bv.Bits), Integer(bv.Value));
+ }
+
+ public VCExpr! BvExtract(VCExpr! bv, int bits, int start, int end) {
+ return Function(new VCExprBvExtractOp (start, end), bv);
+ }
+
+ public static readonly VCExprBvConcatOp! BvConcatOp = new VCExprBvConcatOp();
+ public VCExpr! BvConcat(VCExpr! bv1, VCExpr! bv2) {
+ return Function(BvConcatOp, bv1, bv2);
+ }
+
+ public VCExpr! AtMost(VCExpr! smaller, VCExpr! greater) {
+ return Function(SubtypeOp, smaller, greater);
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////////
+ // Dispatcher for the visitor
+
+ // the declared singleton operators
+ internal enum SingletonOp { NotOp, EqOp, NeqOp, AndOp, OrOp, ImpliesOp,
+ AddOp, SubOp, MulOp,
+ DivOp, ModOp, LtOp, LeOp, GtOp, GeOp, SubtypeOp,
+ Subtype3Op, BvConcatOp };
+ internal static Dictionary<VCExprOp!, SingletonOp>! SingletonOpDict;
+
+ static VCExpressionGenerator() {
+ SingletonOpDict = new Dictionary<VCExprOp!, SingletonOp> ();
+ SingletonOpDict.Add(NotOp, SingletonOp.NotOp);
+ SingletonOpDict.Add(EqOp, SingletonOp.EqOp);
+ SingletonOpDict.Add(NeqOp, SingletonOp.NeqOp);
+ SingletonOpDict.Add(AndOp, SingletonOp.AndOp);
+ SingletonOpDict.Add(OrOp, SingletonOp.OrOp);
+ SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp);
+ SingletonOpDict.Add(AddOp, SingletonOp.AddOp);
+ SingletonOpDict.Add(SubOp, SingletonOp.SubOp);
+ SingletonOpDict.Add(MulOp, SingletonOp.MulOp);
+ SingletonOpDict.Add(DivOp, SingletonOp.DivOp);
+ SingletonOpDict.Add(ModOp, SingletonOp.ModOp);
+ SingletonOpDict.Add(LtOp, SingletonOp.LtOp);
+ SingletonOpDict.Add(LeOp, SingletonOp.LeOp);
+ SingletonOpDict.Add(GtOp, SingletonOp.GtOp);
+ SingletonOpDict.Add(GeOp, SingletonOp.GeOp);
+ SingletonOpDict.Add(SubtypeOp, SingletonOp.SubtypeOp);
+ SingletonOpDict.Add(Subtype3Op,SingletonOp.Subtype3Op);
+ SingletonOpDict.Add(BvConcatOp,SingletonOp.BvConcatOp);
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////
+
+
+ // Let-bindings
+
+ public VCExprLetBinding! LetBinding(VCExprVar! v, VCExpr! e) {
+ return new VCExprLetBinding(v, e);
+ }
+
+ // A "real" let expression. All let-bindings happen simultaneously, i.e.,
+ // at this level the order of the bindings does not matter. It is possible to
+ // create expressions like "let x = y, y = 5 in ...". All bound variables are
+ // bound in all bound terms/formulas and can occur there, but the dependencies
+ // have to be acyclic
+ public VCExpr! Let(List<VCExprLetBinding!>! bindings, VCExpr! body) {
+ if (bindings.Count == 0)
+ // no empty let-bindings
+ return body;
+ return new VCExprLet(bindings, body);
+ }
+
+ public VCExpr! Let(VCExpr! body, params VCExprLetBinding[]! bindings)
+ requires forall{int i in (0:bindings.Length); bindings[i] != null};
+ {
+ return Let(HelperFuns.ToNonNullList(bindings), body);
+ }
+
+
+ /// <summary>
+ /// In contrast to the previous method, the following methods are not a general LET.
+ /// Instead, it
+ /// is a boolean "LET b = P in Q", where P and Q are predicates, that is allowed to be
+ /// encoded as "(b == P) ==> Q" or even as "(P ==> b) ==> Q"
+ /// (or "(P ==> b) and Q" in negative positions).
+ /// The method assumes that the variables in the bindings are unique in the entire formula
+ /// to be produced, which allows the implementation to ignore scope issues in the event that
+ /// it needs to generate an alternate expression for LET.
+ /// </summary>
+
+
+ // Turn let-bindings let v = E in ... into implications E ==> v
+ public VCExpr! AsImplications(List<VCExprLetBinding!>! bindings) {
+ VCExpr! antecedents = True;
+ foreach (VCExprLetBinding b in bindings)
+ // turn "LET_binding v = E" into "v <== E"
+ antecedents = AndSimp(antecedents, Implies(b.E, b.V));
+ return antecedents;
+ }
+
+ // Turn let-bindings let v = E in ... into equations v == E
+ public VCExpr! AsEquations(List<VCExprLetBinding!>! bindings) {
+ VCExpr! antecedents = True;
+ foreach (VCExprLetBinding b in bindings)
+ // turn "LET_binding v = E" into "v <== E"
+ antecedents = AndSimp(antecedents, Eq(b.E, b.V));
+ return antecedents;
+ }
+
+
+
+ // Maps
+
+ public VCExpr! Select(params VCExpr[]! allArgs)
+ requires forall{int i in (0:allArgs.Length); allArgs[i] != null};
+ {
+ return Function(new VCExprSelectOp(allArgs.Length - 1, 0),
+ HelperFuns.ToNonNullList(allArgs),
+ VCExprNAry.EMPTY_TYPE_LIST);
+ }
+
+ public VCExpr! Select(VCExpr[]! allArgs, Type[]! typeArgs)
+ requires 1 <= allArgs.Length;
+ requires forall{int i in (0:allArgs.Length); allArgs[i] != null};
+ requires forall{int i in (0:typeArgs.Length); typeArgs[i] != null};
+ {
+ return Function(new VCExprSelectOp(allArgs.Length - 1, typeArgs.Length),
+ allArgs, typeArgs);
+ }
+
+ public VCExpr! Select(List<VCExpr!>! allArgs, List<Type!>! typeArgs)
+ requires 1 <= allArgs.Count;
+ {
+ return Function(new VCExprSelectOp(allArgs.Count - 1, typeArgs.Count),
+ allArgs, typeArgs);
+ }
+
+ public VCExpr! Store(params VCExpr[]! allArgs)
+ requires forall{int i in (0:allArgs.Length); allArgs[i] != null};
+ {
+ return Function(new VCExprStoreOp(allArgs.Length - 2, 0),
+ HelperFuns.ToNonNullList(allArgs),
+ VCExprNAry.EMPTY_TYPE_LIST);
+ }
+
+ public VCExpr! Store(VCExpr[]! allArgs, Type[]! typeArgs)
+ requires 2 <= allArgs.Length;
+ requires forall{int i in (0:allArgs.Length); allArgs[i] != null};
+ requires forall{int i in (0:typeArgs.Length); typeArgs[i] != null};
+ {
+ return Function(new VCExprStoreOp(allArgs.Length - 2, typeArgs.Length),
+ allArgs, typeArgs);
+ }
+
+ public VCExpr! Store(List<VCExpr!>! allArgs, List<Type!>! typeArgs)
+ requires 2 <= allArgs.Count;
+ {
+ return Function(new VCExprStoreOp(allArgs.Count - 2, typeArgs.Count),
+ allArgs, typeArgs);
+ }
+
+
+ // Labels
+
+ public VCExprLabelOp! LabelOp(bool pos, string! l) {
+ return new VCExprLabelOp(pos, l);
+ }
+
+ public VCExpr! LabelNeg(string! label, VCExpr! e) {
+ return Function(LabelOp(false, label), e);
+ }
+ public VCExpr! LabelPos(string! label, VCExpr! e) {
+ return Function(LabelOp(true, label), e);
+ }
+
+ // Quantifiers
+
+ public VCExpr! Quantify(Quantifier quan,
+ List<TypeVariable!>! typeParams, List<VCExprVar!>! vars,
+ List<VCTrigger!>! triggers, VCQuantifierInfos! infos,
+ VCExpr! body) {
+ return new VCExprQuantifier(quan, typeParams, vars, triggers, infos, body);
+ }
+
+ public VCExpr! Forall(List<TypeVariable!>! typeParams, List<VCExprVar!>! vars,
+ List<VCTrigger!>! triggers, VCQuantifierInfos! infos,
+ VCExpr! body) {
+ return Quantify(Quantifier.ALL, typeParams, vars, triggers, infos, body);
+ }
+ public VCExpr! Forall(List<VCExprVar!>! vars,
+ List<VCTrigger!>! triggers,
+ string! qid, VCExpr! body) {
+ return Quantify(Quantifier.ALL, new List<TypeVariable!> (), vars,
+ triggers, new VCQuantifierInfos (qid, -1, false, null), body);
+ }
+ public VCExpr! Forall(List<VCExprVar!>! vars,
+ List<VCTrigger!>! triggers,
+ VCExpr! body) {
+ return Quantify(Quantifier.ALL, new List<TypeVariable!> (), vars,
+ triggers, new VCQuantifierInfos (null, -1, false, null), body);
+ }
+ public VCExpr! Forall(VCExprVar! var, VCTrigger! trigger, VCExpr! body) {
+ return Forall(HelperFuns.ToNonNullList(var), HelperFuns.ToNonNullList(trigger), body);
+ }
+ public VCExpr! Exists(List<TypeVariable!>! typeParams, List<VCExprVar!>! vars,
+ List<VCTrigger!>! triggers, VCQuantifierInfos! infos,
+ VCExpr! body) {
+ return Quantify(Quantifier.EX, typeParams, vars, triggers, infos, body);
+ }
+ public VCExpr! Exists(List<VCExprVar!>! vars,
+ List<VCTrigger!>! triggers,
+ VCExpr! body) {
+ return Quantify(Quantifier.EX, new List<TypeVariable!> (), vars,
+ triggers, new VCQuantifierInfos (null, -1, false, null), body);
+ }
+ public VCExpr! Exists(VCExprVar! var, VCTrigger! trigger, VCExpr! body) {
+ return Exists(HelperFuns.ToNonNullList(var), HelperFuns.ToNonNullList(trigger), body);
+ }
+
+ public VCTrigger! Trigger(bool pos, List<VCExpr!>! exprs) {
+ return new VCTrigger(pos, exprs);
+ }
+
+ public VCTrigger! Trigger(bool pos, params VCExpr[]! exprs)
+ requires forall{int i in (0:exprs.Length); exprs[i] != null};
+ {
+ return Trigger(pos, HelperFuns.ToNonNullList(exprs));
+ }
+
+ // Reference to a bound or free variable
+
+ public VCExprVar! Variable(string! name, Type! type) {
+ return new VCExprVar(name, type);
+ }
+ }
+}
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+ public class HelperFuns {
+ public static bool SameElements(IEnumerable! a, IEnumerable! b) {
+ IEnumerator ia = a.GetEnumerator();
+ IEnumerator ib = b.GetEnumerator();
+ while (true) {
+ if (ia.MoveNext()) {
+ if (ib.MoveNext()) {
+ if (!((!)ia.Current).Equals(ib.Current))
+ return false;
+ } else {
+ return false;
+ }
+ } else {
+ return !ib.MoveNext();
+ }
+ }
+ return true;
+ }
+
+ public static int PolyHash(int init, int factor, IEnumerable! a) {
+ int res = init;
+ foreach(object x in a)
+ res = res * factor + ((!)x).GetHashCode();
+ return res;
+ }
+
+ public static List<T>! ToList<T>(IEnumerable<T>! l) {
+ List<T>! res = new List<T> ();
+ foreach (T x in l)
+ res.Add(x);
+ return res;
+ }
+
+ public static TypeSeq! ToTypeSeq(VCExpr[]! exprs, int startIndex)
+ requires forall{int i in (0:exprs.Length); exprs[i] != null};
+ {
+ TypeSeq! res = new TypeSeq ();
+ for (int i = startIndex; i < exprs.Length; ++i)
+ res.Add(((!)exprs[i]).Type);
+ return res;
+ }
+
+ public static List<T!>! ToNonNullList<T> (params T[]! args) {
+ List<T!>! res = new List<T!> (args.Length);
+ foreach (T t in args)
+ res.Add((!)t);
+ return res;
+ }
+
+ public static IDictionary<A, B>! Clone<A,B>(IDictionary<A,B>! dict) {
+ IDictionary<A,B>! res = new Dictionary<A,B> (dict.Count);
+ foreach (KeyValuePair<A,B> pair in dict)
+ res.Add(pair);
+ return res;
+ }
+ }
+
+ public abstract class VCExpr {
+ public abstract Type! Type { get; }
+
+ public abstract Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg);
+
+ [Pure]
+ public override string! ToString() {
+ StringWriter! sw = new StringWriter();
+ VCExprPrinter! printer = new VCExprPrinter ();
+ printer.Print(this, sw);
+ return (!)sw.ToString();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // Literal expressions
+
+ public class VCExprLiteral : VCExpr {
+ private readonly Type! LitType;
+ public override Type! Type { get { return LitType; } }
+ internal VCExprLiteral(Type! type) {
+ this.LitType = type;
+ }
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.Visit(this, arg);
+ }
+ }
+
+ public class VCExprIntLit : VCExprLiteral
+ {
+ public readonly BigNum Val;
+ internal VCExprIntLit(BigNum val) {
+ base(Type.Int);
+ this.Val = val;
+ }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprIntLit)
+ return Val == ((VCExprIntLit)that).Val;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Val.GetHashCode() * 72321;
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // Operator expressions with fixed arity
+
+ public abstract class VCExprNAry : VCExpr, IEnumerable<VCExpr!> {
+ public readonly VCExprOp! Op;
+ public int Arity { get { return Op.Arity; } }
+ public int TypeParamArity { get { return Op.TypeParamArity; } }
+ public int Length { get { return Arity; } }
+ // the sub-expressions of the expression
+ public abstract VCExpr! this[int index] { get; }
+
+ // the type arguments
+ public abstract List<Type!>! TypeArguments { get; }
+
+ [Pure] [GlobalAccess(false)] [Escapes(true,false)]
+ public IEnumerator<VCExpr!>! GetEnumerator() {
+ for (int i = 0; i < Arity; ++i)
+ yield return this[i];
+ }
+ [Pure] [GlobalAccess(false)] [Escapes(true,false)]
+ IEnumerator! System.Collections.IEnumerable.GetEnumerator() {
+ for (int i = 0; i < Arity; ++i)
+ yield return this[i];
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprNAry) {
+ // we compare the subterms iteratively (not recursively)
+ // to avoid stack overflows
+
+ VCExprNAryEnumerator enum0 = new VCExprNAryEnumerator(this);
+ VCExprNAryEnumerator enum1 = new VCExprNAryEnumerator((VCExprNAry)that);
+
+ while (true) {
+ bool next0 = enum0.MoveNext();
+ bool next1 = enum1.MoveNext();
+ if (next0 != next1)
+ return false;
+ if (!next0)
+ return true;
+
+ VCExprNAry nextExprNAry0 = enum0.Current as VCExprNAry;
+ VCExprNAry nextExprNAry1 = enum1.Current as VCExprNAry;
+
+ if ((nextExprNAry0 == null) != (nextExprNAry1 == null))
+ return false;
+ if (nextExprNAry0 != null && nextExprNAry1 != null) {
+ if (!nextExprNAry0.Op.Equals(nextExprNAry1.Op))
+ return false;
+ } else {
+ if (!((!)enum0.Current).Equals(enum1.Current))
+ return false;
+ }
+ }
+ }
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return HelperFuns.PolyHash(Op.GetHashCode() * 123 + Arity * 61521,
+ 3, this);
+ }
+
+ internal VCExprNAry(VCExprOp! op) {
+ this.Op = op;
+ }
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.Visit(this, arg);
+ }
+ public Result Accept<Result, Arg>(IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return Op.Accept(this, visitor, arg);
+ }
+
+ internal static readonly List<Type!>! EMPTY_TYPE_LIST = new List<Type!> ();
+ internal static readonly List<VCExpr!>! EMPTY_VCEXPR_LIST = new List<VCExpr!> ();
+ }
+
+ // We give specialised implementations for nullary, unary and binary expressions
+
+ internal class VCExprNullary : VCExprNAry {
+ private readonly Type! ExprType;
+ public override Type! Type { get { return ExprType; } }
+ public override VCExpr! this[int index] { get {
+ assert false; // no arguments
+ } }
+
+ // the type arguments
+ public override List<Type!>! TypeArguments { get {
+ return EMPTY_TYPE_LIST;
+ } }
+
+ internal VCExprNullary(VCExprOp! op)
+ requires op.Arity == 0 && op.TypeParamArity == 0; {
+ base(op);
+ this.ExprType = op.InferType(EMPTY_VCEXPR_LIST, EMPTY_TYPE_LIST);
+ }
+ }
+
+ internal class VCExprUnary : VCExprNAry {
+ private readonly VCExpr! Argument;
+ private readonly Type! ExprType;
+ public override Type! Type { get { return ExprType; } }
+ public override VCExpr! this[int index] { get {
+ assume index == 0;
+ return Argument;
+ } }
+
+ // the type arguments
+ public override List<Type!>! TypeArguments { get {
+ return EMPTY_TYPE_LIST;
+ } }
+
+ internal VCExprUnary(VCExprOp! op, List<VCExpr!>! arguments)
+ requires op.Arity == 1 && op.TypeParamArity == 0 && arguments.Count == 1; {
+ base(op);
+ this.Argument = arguments[0];
+ this.ExprType =
+ op.InferType(arguments, EMPTY_TYPE_LIST);
+ }
+
+ internal VCExprUnary(VCExprOp! op, VCExpr! argument)
+ requires op.Arity == 1 && op.TypeParamArity == 0; {
+ base(op);
+ this.Argument = argument;
+ // PR: could be optimised so that the argument does
+ // not have to be boxed in an array each time
+ this.ExprType =
+ op.InferType(HelperFuns.ToNonNullList(argument), EMPTY_TYPE_LIST);
+ }
+ }
+
+ internal class VCExprBinary : VCExprNAry {
+ private readonly VCExpr! Argument0;
+ private readonly VCExpr! Argument1;
+ private readonly Type! ExprType;
+ public override Type! Type { get { return ExprType; } }
+ public override VCExpr! this[int index] { get {
+ switch (index) {
+ case 0: return Argument0;
+ case 1: return Argument1;
+ default: assert false;
+ }
+ } }
+
+ // the type arguments
+ public override List<Type!>! TypeArguments { get {
+ return EMPTY_TYPE_LIST;
+ } }
+
+ internal VCExprBinary(VCExprOp! op, List<VCExpr!>! arguments)
+ requires op.Arity == 2 && op.TypeParamArity == 0 && arguments.Count == 2; {
+ base(op);
+ this.Argument0 = arguments[0];
+ this.Argument1 = arguments[1];
+ this.ExprType = op.InferType(arguments, EMPTY_TYPE_LIST);
+ }
+
+ internal VCExprBinary(VCExprOp! op, VCExpr! argument0, VCExpr! argument1)
+ requires op.Arity == 2 && op.TypeParamArity == 0; {
+ base(op);
+ this.Argument0 = argument0;
+ this.Argument1 = argument1;
+ // PR: could be optimised so that the arguments do
+ // not have to be boxed in an array each time
+ this.ExprType =
+ op.InferType(HelperFuns.ToNonNullList(argument0, argument1),
+ EMPTY_TYPE_LIST);
+ }
+ }
+
+ internal class VCExprMultiAry : VCExprNAry {
+ private readonly List<VCExpr!>! Arguments;
+ private readonly List<Type!>! TypeArgumentsAttr;
+
+ private readonly Type! ExprType;
+ public override Type! Type { get { return ExprType; } }
+ public override VCExpr! this[int index] { get {
+ assume index >= 0 && index < Arity;
+ return (!)Arguments[index];
+ } }
+
+ // the type arguments
+ public override List<Type!>! TypeArguments { get {
+ return TypeArgumentsAttr;
+ } }
+
+ internal VCExprMultiAry(VCExprOp! op, List<VCExpr!>! arguments) {
+ this(op, arguments, EMPTY_TYPE_LIST);
+ }
+ internal VCExprMultiAry(VCExprOp! op, List<VCExpr!>! arguments, List<Type!>! typeArguments)
+ requires (arguments.Count > 2 || typeArguments.Count > 0);
+ requires op.Arity == arguments.Count;
+ requires op.TypeParamArity == typeArguments.Count;
+ {
+ base(op);
+ this.Arguments = arguments;
+ this.TypeArgumentsAttr = typeArguments;
+ this.ExprType = op.InferType(arguments, typeArguments);
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // The various operators available
+
+ public abstract class VCExprOp {
+ // the number of value parameters
+ public abstract int Arity { get; }
+ // the number of type parameters
+ public abstract int TypeParamArity { get; }
+
+ public abstract Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs);
+
+ public virtual Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ VCExpressionGenerator.SingletonOp op;
+ if (VCExpressionGenerator.SingletonOpDict.TryGetValue(this, out op)) {
+ switch(op) {
+ case VCExpressionGenerator.SingletonOp.NotOp:
+ return visitor.VisitNotOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.EqOp:
+ return visitor.VisitEqOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.NeqOp:
+ return visitor.VisitNeqOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.AndOp:
+ return visitor.VisitAndOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.OrOp:
+ return visitor.VisitOrOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.ImpliesOp:
+ return visitor.VisitImpliesOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.AddOp:
+ return visitor.VisitAddOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.SubOp:
+ return visitor.VisitSubOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.MulOp:
+ return visitor.VisitMulOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.DivOp:
+ return visitor.VisitDivOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.ModOp:
+ return visitor.VisitModOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.LtOp:
+ return visitor.VisitLtOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.LeOp:
+ return visitor.VisitLeOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.GtOp:
+ return visitor.VisitGtOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.GeOp:
+ return visitor.VisitGeOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.SubtypeOp:
+ return visitor.VisitSubtypeOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.Subtype3Op:
+ return visitor.VisitSubtype3Op(expr, arg);
+ case VCExpressionGenerator.SingletonOp.BvConcatOp:
+ return visitor.VisitBvConcatOp(expr, arg);
+ default:
+ assert false;
+ }
+ } else {
+ assert false;
+ }
+ }
+ }
+
+ public class VCExprNAryOp : VCExprOp {
+ private readonly Type! OpType;
+ private readonly int OpArity;
+
+ public override int Arity { get { return OpArity; } }
+ public override int TypeParamArity { get { return 0; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ return OpType;
+ }
+
+ internal VCExprNAryOp(int arity, Type! type) {
+ this.OpArity = arity;
+ this.OpType = type;
+ }
+ }
+
+ public class VCExprDistinctOp : VCExprNAryOp {
+ internal VCExprDistinctOp(int arity) {
+ base(arity, Type.Bool);
+ }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprDistinctOp)
+ return Arity == ((VCExprDistinctOp)that).Arity;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Arity * 917632481;
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitDistinctOp(expr, arg);
+ }
+ }
+
+ public class VCExprLabelOp : VCExprOp {
+ public override int Arity { get { return 1; } }
+ public override int TypeParamArity { get { return 0; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ return args[0].Type;
+ }
+
+ public readonly bool pos;
+ public readonly string! label;
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprLabelOp) {
+ VCExprLabelOp! thatOp = (VCExprLabelOp)that;
+ return this.pos == thatOp.pos && this.label.Equals(thatOp.label);
+ }
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return (pos ? 9817231 : 7198639) + label.GetHashCode();
+ }
+
+ internal VCExprLabelOp(bool pos, string! l) {
+ this.pos = pos;
+ this.label = pos ? "+" + l : "@" + l;
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitLabelOp(expr, arg);
+ }
+ }
+
+ public class VCExprSelectOp : VCExprOp {
+ private readonly int MapArity;
+ private readonly int MapTypeParamArity;
+ public override int Arity { get { return MapArity + 1; } }
+ public override int TypeParamArity { get { return MapTypeParamArity; } }
+
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ MapType! mapType = args[0].Type.AsMap;
+ assert TypeParamArity == mapType.TypeParameters.Length;
+ IDictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!> ();
+ for (int i = 0; i < TypeParamArity; ++i)
+ subst.Add(mapType.TypeParameters[i], typeArgs[i]);
+ return mapType.Result.Substitute(subst);
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprSelectOp)
+ return Arity == ((VCExprSelectOp)that).Arity &&
+ TypeParamArity == ((VCExprSelectOp)that).TypeParamArity;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Arity * 1212481 + TypeParamArity * 298741;
+ }
+
+ internal VCExprSelectOp(int arity, int typeParamArity)
+ requires 0 <= arity && 0 <= typeParamArity;
+ {
+ this.MapArity = arity;
+ this.MapTypeParamArity = typeParamArity;
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitSelectOp(expr, arg);
+ }
+ }
+
+ public class VCExprStoreOp : VCExprOp {
+ private readonly int MapArity;
+ private readonly int MapTypeParamArity;
+ public override int Arity { get { return MapArity + 2; } }
+ // stores never need explicit type parameters, because also the
+ // rhs is a value argument
+ public override int TypeParamArity { get { return MapTypeParamArity; } }
+
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ return args[0].Type;
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprStoreOp)
+ return Arity == ((VCExprStoreOp)that).Arity;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Arity * 91361821;
+ }
+
+ internal VCExprStoreOp(int arity, int typeParamArity)
+ requires 0 <= arity && 0 <= typeParamArity;
+ {
+ this.MapArity = arity;
+ this.MapTypeParamArity = typeParamArity;
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitStoreOp(expr, arg);
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // Bitvector operators
+
+ public class VCExprBvOp : VCExprOp {
+ public readonly int Bits;
+
+ public override int Arity { get { return 1; } }
+ public override int TypeParamArity { get { return 0; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ return Type.GetBvType(Bits);
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprBvOp)
+ return this.Bits == ((VCExprBvOp)that).Bits;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Bits * 81748912;
+ }
+
+ internal VCExprBvOp(int bits) {
+ this.Bits = bits;
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitBvOp(expr, arg);
+ }
+ }
+
+ public class VCExprBvExtractOp : VCExprOp {
+ public readonly int Start;
+ public readonly int End;
+
+ public override int Arity { get { return 1; } }
+ public override int TypeParamArity { get { return 0; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ return Type.GetBvType(End - Start);
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprBvExtractOp) {
+ VCExprBvExtractOp! thatExtract = (VCExprBvExtractOp)that;
+ return this.Start == thatExtract.Start && this.End == thatExtract.End;
+ }
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Start * 81912 + End * 978132;
+ }
+
+ internal VCExprBvExtractOp(int start, int end) {
+ this.Start = start;
+ this.End = end;
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitBvExtractOp(expr, arg);
+ }
+ }
+
+ // singleton class
+ public class VCExprBvConcatOp : VCExprOp {
+ public override int Arity { get { return 2; } }
+ public override int TypeParamArity { get { return 0; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ return Type.GetBvType(args[0].Type.BvBits + args[1].Type.BvBits);
+ }
+ internal VCExprBvConcatOp() {}
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // References to user-defined Boogie functions
+
+ public class VCExprBoogieFunctionOp : VCExprOp {
+ public readonly Function! Func;
+
+ public override int Arity { get { return Func.InParams.Length; } }
+ public override int TypeParamArity { get { return Func.TypeParameters.Length; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ assert TypeParamArity == Func.TypeParameters.Length;
+ if (TypeParamArity == 0)
+ return ((!)Func.OutParams[0]).TypedIdent.Type;
+ IDictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!> (TypeParamArity);
+ for (int i = 0; i < TypeParamArity; ++i)
+ subst.Add(Func.TypeParameters[i], typeArgs[i]);
+ return ((!)Func.OutParams[0]).TypedIdent.Type.Substitute(subst);
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprBoogieFunctionOp)
+ return this.Func.Equals(((VCExprBoogieFunctionOp)that).Func);
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Func.GetHashCode() + 18731;
+ }
+
+ // we require that the result type of the expression is specified, because we
+ // do not want to perform full type inference at this point
+ internal VCExprBoogieFunctionOp(Function! func) {
+ this.Func = func;
+ }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitBoogieFunctionOp(expr, arg);
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // Binders (quantifiers and let-expressions). We introduce our own class for
+ // term variables, but use the Boogie-AST class for type variables
+
+ public class VCExprVar : VCExpr {
+ // the name of the variable. Note that the name is not used for comparison,
+ // i.e., there can be two distinct variables with the same name
+ public readonly string! Name;
+ private readonly Type! VarType;
+ public override Type! Type { get { return VarType; } }
+
+ internal VCExprVar(string! name, Type! type) {
+ this.Name = name;
+ this.VarType = type;
+ }
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.Visit(this, arg);
+ }
+ }
+
+ public abstract class VCExprBinder : VCExpr {
+ public readonly VCExpr! Body;
+ public readonly List<TypeVariable!>! TypeParameters;
+ public readonly List<VCExprVar!>! BoundVars;
+
+ public override Type! Type { get { return Body.Type; } }
+
+ internal VCExprBinder(List<TypeVariable!>! typeParams,
+ List<VCExprVar!>! boundVars,
+ VCExpr! body)
+ requires boundVars.Count + typeParams.Count > 0; { // only nontrivial binders ...
+ this.TypeParameters = typeParams;
+ this.BoundVars = boundVars;
+ this.Body = body;
+ }
+ }
+
+ public class VCTrigger {
+ public readonly bool Pos;
+ public readonly List<VCExpr!>! Exprs;
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCTrigger) {
+ VCTrigger! thatTrigger = (VCTrigger)that;
+ return this.Pos == thatTrigger.Pos &&
+ HelperFuns.SameElements(this.Exprs, thatTrigger.Exprs);
+ }
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return (Pos ? 913821 : 871334) +
+ HelperFuns.PolyHash(123, 7, this.Exprs);
+ }
+
+ public VCTrigger(bool pos, List<VCExpr!>! exprs) {
+ this.Pos = pos;
+ this.Exprs = exprs;
+ }
+ }
+
+ public class VCQuantifierInfos {
+ public readonly string qid;
+ public readonly int uniqueId;
+ public readonly bool bvZ3Native;
+ public QKeyValue attributes;
+
+ public VCQuantifierInfos(string qid, int uniqueId, bool bvZ3Native, QKeyValue attributes) {
+ this.qid = qid;
+ this.uniqueId = uniqueId;
+ this.bvZ3Native = bvZ3Native;
+ this.attributes = attributes;
+ }
+ }
+
+ public enum Quantifier { ALL, EX };
+
+ public class VCExprQuantifier : VCExprBinder {
+ public readonly Quantifier Quan;
+
+ public readonly List<VCTrigger!>! Triggers;
+ public readonly VCQuantifierInfos! Infos;
+
+ // Equality is /not/ modulo bound renaming at this point
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprQuantifier) {
+ VCExprQuantifier! thatQuan = (VCExprQuantifier)that;
+ return this.Quan == thatQuan.Quan &&
+ HelperFuns.SameElements(this.Triggers, thatQuan.Triggers) &&
+ HelperFuns.SameElements(this.TypeParameters, thatQuan.TypeParameters) &&
+ HelperFuns.SameElements(this.BoundVars, thatQuan.BoundVars) &&
+ this.Body.Equals(thatQuan.Body);
+ }
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Quan.GetHashCode() +
+ HelperFuns.PolyHash(973219, 7, TypeParameters) +
+ HelperFuns.PolyHash(998431, 9, BoundVars) +
+ HelperFuns.PolyHash(123, 11, Triggers);
+ }
+
+ internal VCExprQuantifier(Quantifier kind,
+ List<TypeVariable!>! typeParams,
+ List<VCExprVar!>! boundVars,
+ List<VCTrigger!>! triggers,
+ VCQuantifierInfos! infos,
+ VCExpr! body) {
+ base(typeParams, boundVars, body);
+ this.Quan = kind;
+ this.Triggers = triggers;
+ this.Infos = infos;
+ }
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.Visit(this, arg);
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // Let-Bindings
+
+ public class VCExprLetBinding {
+ public readonly VCExprVar! V;
+ public readonly VCExpr! E;
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprLetBinding) {
+ VCExprLetBinding! thatB = (VCExprLetBinding)that;
+ return this.V.Equals(thatB.V) && this.E.Equals(thatB.E);
+ }
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return V.GetHashCode() * 71261 + E.GetHashCode();
+ }
+
+ internal VCExprLetBinding(VCExprVar! v, VCExpr! e) {
+ this.V = v;
+ this.E = e;
+ assert v.Type.Equals(e.Type);
+ }
+ }
+
+ public class VCExprLet : VCExprBinder, IEnumerable<VCExprLetBinding!> {
+ private readonly List<VCExprLetBinding!>! Bindings;
+
+ public int Length { get { return Bindings.Count; } }
+ public VCExprLetBinding! this[int index] { get {
+ return Bindings[index];
+ } }
+
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprLet) {
+ VCExprLet! thatLet = (VCExprLet)that;
+ return this.Body.Equals(thatLet.Body) &&
+ HelperFuns.SameElements(this, (VCExprLet)that);
+ }
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return HelperFuns.PolyHash(Body.GetHashCode(), 9, Bindings);
+ }
+
+ [Pure] [GlobalAccess(false)] [Escapes(true,false)]
+ public IEnumerator<VCExprLetBinding!>! GetEnumerator() {
+ return Bindings.GetEnumerator();
+ }
+ [Pure] [GlobalAccess(false)] [Escapes(true,false)]
+ IEnumerator! System.Collections.IEnumerable.GetEnumerator() {
+ return Bindings.GetEnumerator();
+ }
+
+ private static List<VCExprVar!>! toSeq(List<VCExprLetBinding!>! bindings) {
+ List<VCExprVar!>! res = new List<VCExprVar!> ();
+ foreach (VCExprLetBinding! b in bindings)
+ res.Add(b.V);
+ return res;
+ }
+
+ internal VCExprLet(List<VCExprLetBinding!>! bindings,
+ VCExpr! body) {
+ base(new List<TypeVariable!> (), toSeq(bindings), body);
+ this.Bindings = bindings;
+ }
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.Visit(this, arg);
+ }
+ }
+}
diff --git a/Source/VCExpr/VCExprASTPrinter.ssc b/Source/VCExpr/VCExprASTPrinter.ssc new file mode 100644 index 00000000..1c143516 --- /dev/null +++ b/Source/VCExpr/VCExprASTPrinter.ssc @@ -0,0 +1,240 @@ +//-----------------------------------------------------------------------------
+//
+// 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 simple visitor for turning a VCExpr into a human-readable string
+// (S-expr syntax)
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+ public class VCExprPrinter : IVCExprVisitor<bool, TextWriter!> {
+ private VCExprOpPrinter OpPrinterVar = null;
+ private VCExprOpPrinter! OpPrinter { get {
+ if (OpPrinterVar == null)
+ OpPrinterVar = new VCExprOpPrinter(this);
+ return OpPrinterVar;
+ } }
+
+ public void Print(VCExpr! expr, TextWriter! wr) {
+ expr.Accept<bool, TextWriter!>(this, wr);
+ }
+
+ public bool Visit(VCExprLiteral! node, TextWriter! wr) {
+ if (node == VCExpressionGenerator.True)
+ wr.Write("true");
+ else if (node == VCExpressionGenerator.False)
+ wr.Write("false");
+ else if (node is VCExprIntLit) {
+ wr.Write(((VCExprIntLit)node).Val);
+ } else
+ assert false;
+ return true;
+ }
+ public bool Visit(VCExprNAry! node, TextWriter! wr) {
+ VCExprOp! op = node.Op;
+
+ if (op.Equals(VCExpressionGenerator.AndOp) ||
+ op.Equals(VCExpressionGenerator.OrOp)) {
+ // handle these operators without recursion
+
+ wr.Write("({0}",
+ op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");
+ IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node);
+ while (enumerator.MoveNext()) {
+ VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ wr.Write(" ");
+ Print((VCExpr!)enumerator.Current, wr);
+ }
+ }
+
+ wr.Write(")");
+
+ return true;
+ }
+
+ return node.Accept<bool, TextWriter!>(OpPrinter, wr);
+ }
+ public bool Visit(VCExprVar! node, TextWriter! wr) {
+ wr.Write(node.Name);
+ return true;
+ }
+ public bool Visit(VCExprQuantifier! node, TextWriter! wr) {
+ string! quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";
+
+ wr.Write("({0} ", quan);
+
+ if (node.TypeParameters.Count > 0) {
+ wr.Write("<");
+ string! sep = "";
+ foreach (TypeVariable! v in node.TypeParameters) {
+ wr.Write(sep);
+ sep = ", ";
+ wr.Write("{0}", v.Name);
+ }
+ wr.Write("> ");
+ }
+
+ if (node.BoundVars.Count > 0) {
+ string! sep = "";
+ foreach (VCExprVar! v in node.BoundVars) {
+ wr.Write(sep);
+ sep = ", ";
+ Print(v, wr);
+ }
+ wr.Write(" ");
+ }
+
+ wr.Write(":: ");
+
+ if (node.Triggers.Count > 0) {
+ wr.Write("{0} ", "{");
+ string! sep = "";
+ foreach (VCTrigger! t in node.Triggers) {
+ wr.Write(sep);
+ sep = ", ";
+ string! sep2 = "";
+ foreach (VCExpr! e in t.Exprs) {
+ wr.Write(sep2);
+ sep2 = "+";
+ Print(e, wr);
+ }
+ }
+ wr.Write(" {0} ", "}");
+ }
+
+ Print(node.Body, wr);
+ wr.Write(")");
+ return true;
+ }
+ public bool Visit(VCExprLet! node, TextWriter! wr) {
+ wr.Write("(Let ");
+
+ string! sep = "";
+ foreach (VCExprLetBinding! b in node) {
+ wr.Write(sep);
+ sep = ", ";
+ Print(b.V, wr);
+ wr.Write(" = ");
+ Print(b.E, wr);
+ }
+ wr.Write(" ");
+
+ Print(node.Body, wr);
+ wr.Write(")");
+ return true;
+ }
+ }
+
+ public class VCExprOpPrinter : IVCExprOpVisitor<bool, TextWriter!> {
+ private VCExprPrinter! ExprPrinter;
+
+ public VCExprOpPrinter(VCExprPrinter! exprPrinter) {
+ this.ExprPrinter = exprPrinter;
+ }
+
+ private bool PrintNAry(string! op, VCExprNAry! node, TextWriter! wr) {
+ wr.Write("({0}", op);
+ foreach (VCExpr! arg in node) {
+ wr.Write(" ");
+ ExprPrinter.Print(arg, wr);
+ }
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitNotOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("!", node, wr);
+ }
+ public bool VisitEqOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("==", node, wr);
+ }
+ public bool VisitNeqOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("!=", node, wr);
+ }
+ public bool VisitAndOp (VCExprNAry! node, TextWriter! wr) {
+ assert false;
+ }
+ public bool VisitOrOp (VCExprNAry! node, TextWriter! wr) {
+ assert false;
+ }
+ public bool VisitImpliesOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Implies", node, wr);
+ }
+ public bool VisitDistinctOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Distinct", node, wr);
+ }
+ public bool VisitLabelOp (VCExprNAry! node, TextWriter! wr) {
+ VCExprLabelOp! op = (VCExprLabelOp)node.Op;
+ return PrintNAry("Label " + op.label, node, wr);
+ }
+ public bool VisitSelectOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Select", node, wr);
+ }
+ public bool VisitStoreOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Store", node, wr);
+ }
+ public bool VisitBvOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Bv", node, wr);
+ }
+ public bool VisitBvExtractOp(VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("BvExtract", node, wr);
+ }
+ public bool VisitBvConcatOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("BvConcat", node, wr);
+ }
+ public bool VisitAddOp (VCExprNAry! node, TextWriter! wr) {
+ if (CommandLineOptions.Clo.ReflectAdd) {
+ return PrintNAry("Reflect$Add", node, wr);
+ } else {
+ return PrintNAry("+", node, wr);
+ }
+ }
+ public bool VisitSubOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("-", node, wr);
+ }
+ public bool VisitMulOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("*", node, wr);
+ }
+ public bool VisitDivOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("/", node, wr);
+ }
+ public bool VisitModOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("%", node, wr);
+ }
+ public bool VisitLtOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("<", node, wr);
+ }
+ public bool VisitLeOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("<=", node, wr);
+ }
+ public bool VisitGtOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry(">", node, wr);
+ }
+ public bool VisitGeOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry(">=", node, wr);
+ }
+ public bool VisitSubtypeOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("<:", node, wr);
+ }
+ public bool VisitSubtype3Op (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("<::", node, wr);
+ }
+ public bool VisitBoogieFunctionOp (VCExprNAry! node, TextWriter! wr) {
+ VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op;
+ return PrintNAry(op.Func.Name, node, wr);
+ }
+ }
+
+
+}
\ No newline at end of file diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc new file mode 100644 index 00000000..cbb4ab8f --- /dev/null +++ b/Source/VCExpr/VCExprASTVisitors.ssc @@ -0,0 +1,999 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+
+// Some visitor skeletons for the VCExpression AST
+
+namespace Microsoft.Boogie.VCExprAST
+{
+ using Microsoft.Boogie;
+
+ public interface IVCExprVisitor<Result, Arg> {
+ Result Visit(VCExprLiteral! node, Arg arg);
+ Result Visit(VCExprNAry! node, Arg arg);
+ Result Visit(VCExprVar! node, Arg arg);
+ Result Visit(VCExprQuantifier! node, Arg arg);
+ Result Visit(VCExprLet! node, Arg arg);
+ }
+
+ public interface IVCExprOpVisitor<Result, Arg> {
+ Result VisitNotOp (VCExprNAry! node, Arg arg);
+ Result VisitEqOp (VCExprNAry! node, Arg arg);
+ Result VisitNeqOp (VCExprNAry! node, Arg arg);
+ Result VisitAndOp (VCExprNAry! node, Arg arg);
+ Result VisitOrOp (VCExprNAry! node, Arg arg);
+ Result VisitImpliesOp (VCExprNAry! node, Arg arg);
+ Result VisitDistinctOp (VCExprNAry! node, Arg arg);
+ Result VisitLabelOp (VCExprNAry! node, Arg arg);
+ Result VisitSelectOp (VCExprNAry! node, Arg arg);
+ Result VisitStoreOp (VCExprNAry! node, Arg arg);
+ Result VisitBvOp (VCExprNAry! node, Arg arg);
+ Result VisitBvExtractOp(VCExprNAry! node, Arg arg);
+ Result VisitBvConcatOp (VCExprNAry! node, Arg arg);
+ Result VisitAddOp (VCExprNAry! node, Arg arg);
+ Result VisitSubOp (VCExprNAry! node, Arg arg);
+ Result VisitMulOp (VCExprNAry! node, Arg arg);
+ Result VisitDivOp (VCExprNAry! node, Arg arg);
+ Result VisitModOp (VCExprNAry! node, Arg arg);
+ Result VisitLtOp (VCExprNAry! node, Arg arg);
+ Result VisitLeOp (VCExprNAry! node, Arg arg);
+ Result VisitGtOp (VCExprNAry! node, Arg arg);
+ Result VisitGeOp (VCExprNAry! node, Arg arg);
+ Result VisitSubtypeOp (VCExprNAry! node, Arg arg);
+ Result VisitSubtype3Op (VCExprNAry! node, Arg arg);
+ Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg);
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+ // Standard implementations that make it easier to create own visitors
+
+ // Simple traversal of VCExprs. The Visit implementations work
+ // recursively, apart from the implementation for VCExprNAry that
+ // uses a stack when applied to nested nodes with the same
+ // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary
+ // to avoid stack overflows
+
+ public abstract class TraversingVCExprVisitor<Result, Arg>
+ : IVCExprVisitor<Result, Arg> {
+ protected abstract Result StandardResult(VCExpr! node, Arg arg);
+
+ public Result Traverse(VCExpr! node, Arg arg) {
+ return node.Accept(this, arg);
+ }
+
+ public virtual Result Visit(VCExprLiteral! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+
+ public virtual Result Visit(VCExprNAry! node, Arg arg) {
+ Result res = StandardResult(node, arg);
+
+ if (node.TypeParamArity == 0) {
+ VCExprOp! op = node.Op;
+
+ IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
+ enumerator.MoveNext();
+
+ while (enumerator.MoveNext()) {
+ VCExpr! expr = (VCExpr!)enumerator.Current;
+ VCExprNAry naryExpr = expr as VCExprNAry;
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ expr.Accept(this, arg);
+ } else {
+ StandardResult(expr, arg);
+ }
+ }
+ } else {
+ foreach (VCExpr! e in node)
+ e.Accept(this, arg);
+ }
+
+ return res;
+ }
+
+ public virtual Result Visit(VCExprVar! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result Visit(VCExprQuantifier! node, Arg arg) {
+ Result res = StandardResult(node, arg);
+ foreach (VCTrigger! trigger in node.Triggers)
+ foreach (VCExpr! expr in trigger.Exprs)
+ expr.Accept(this, arg);
+ node.Body.Accept(this, arg);
+ return res;
+ }
+ public virtual Result Visit(VCExprLet! node, Arg arg) {
+ Result res = StandardResult(node, arg);
+ // visit the bound expressions first
+ foreach (VCExprLetBinding! binding in node)
+ binding.E.Accept(this, arg);
+ node.Body.Accept(this, arg);
+ return res;
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+ // Class to iterate over the nodes of a tree of VCExprNAry. This is
+ // used to avoid handling such VCExpr recursively, which can easily
+ // lead to stack overflows
+
+ public class VCExprNAryEnumerator : IEnumerator {
+
+ private readonly VCExprNAry! CompleteExpr;
+ private VCExpr CurrentExpr = null;
+ private readonly Stack<VCExpr!>! ExprTodo = new Stack<VCExpr!> ();
+
+ public VCExprNAryEnumerator(VCExprNAry! completeExpr) {
+ this.CompleteExpr = completeExpr;
+ Stack<VCExpr!>! exprTodo = new Stack<VCExpr!> ();
+ exprTodo.Push(completeExpr);
+ ExprTodo = exprTodo;
+ }
+
+ // Method using which a subclass can decide whether the
+ // subexpressions of an expression should be enumerated as well
+ // The default is to enumerate all nodes
+ protected virtual bool Descend(VCExprNAry! expr) {
+ return true;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public bool MoveNext() {
+ if (ExprTodo.Count == 0)
+ return false;
+
+ CurrentExpr = ExprTodo.Pop();
+ VCExprNAry currentNAry = CurrentExpr as VCExprNAry;
+ if (currentNAry != null && Descend(currentNAry)) {
+ for (int i = currentNAry.Arity - 1; i >= 0; --i)
+ ExprTodo.Push(currentNAry[i]);
+ }
+
+ return true;
+ }
+
+ public object Current {
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ get {
+ return (!)CurrentExpr;
+ } }
+
+ public void Reset() {
+ ExprTodo.Clear();
+ CurrentExpr = null;
+ ExprTodo.Push(CompleteExpr);
+ }
+ }
+
+
+ //////////////////////////////////////////////////////////////////////////////
+
+ public class VCExprNAryUniformOpEnumerator : VCExprNAryEnumerator {
+ private readonly VCExprOp! Op;
+ public VCExprNAryUniformOpEnumerator(VCExprNAry! completeExpr) {
+ base(completeExpr);
+ this.Op = completeExpr.Op;
+ }
+ protected override bool Descend(VCExprNAry! expr) {
+ return expr.Op.Equals(Op) &&
+ // we never skip nodes with type parameters
+ // (those are too interesting ...)
+ expr.TypeParamArity == 0;
+ }
+ }
+
+ //////////////////////////////////////////////////////////////////////////////
+ // Visitor that knows about the variables bound at each location in a VCExpr
+
+ public abstract class BoundVarTraversingVCExprVisitor<Result, Arg>
+ : TraversingVCExprVisitor<Result, Arg> {
+ // Maps with all variables bound above a certain location in the VCExpression.
+ // The value of the map tells how often a particular symbol was bound
+ private readonly IDictionary<VCExprVar!, int>! BoundTermVarsDict =
+ new Dictionary<VCExprVar!, int> ();
+ private readonly IDictionary<TypeVariable!, int>! BoundTypeVarsDict =
+ new Dictionary<TypeVariable!, int> ();
+
+ protected ICollection<VCExprVar!>! BoundTermVars { get {
+ return BoundTermVarsDict.Keys;
+ } }
+ protected ICollection<TypeVariable!>! BoundTypeVars { get {
+ return BoundTypeVarsDict.Keys;
+ } }
+
+ private void AddBoundVar<T>(IDictionary<T!, int>! dict, T! sym) {
+ int n;
+ if (dict.TryGetValue(sym, out n))
+ dict[sym] = n + 1;
+ else
+ dict[sym] = 1;
+ }
+
+ private void RemoveBoundVar<T>(IDictionary<T!, int>! dict, T! sym) {
+ int n;
+ bool b = dict.TryGetValue(sym, out n);
+ assert b && n > 0;
+ if (n == 1)
+ dict.Remove(sym);
+ else
+ dict[sym] = n - 1;
+ }
+
+ public override Result Visit(VCExprQuantifier! node, Arg arg) {
+ // we temporarily add bound (term and type) variables to the
+ // corresponding lists
+ foreach (VCExprVar! v in node.BoundVars)
+ AddBoundVar<VCExprVar>(BoundTermVarsDict, v);
+ foreach (TypeVariable! v in node.TypeParameters)
+ AddBoundVar<TypeVariable>(BoundTypeVarsDict, v);
+
+ Result res;
+ try {
+ res = VisitAfterBinding(node, arg);
+ } finally {
+ foreach (VCExprVar! v in node.BoundVars)
+ RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);
+ foreach (TypeVariable! v in node.TypeParameters)
+ RemoveBoundVar<TypeVariable>(BoundTypeVarsDict, v);
+ }
+ return res;
+ }
+ public override Result Visit(VCExprLet! node, Arg arg) {
+ // we temporarily add bound term variables to the
+ // corresponding lists
+ foreach (VCExprVar! v in node.BoundVars)
+ AddBoundVar<VCExprVar>(BoundTermVarsDict, v);
+
+ Result res;
+ try {
+ res = VisitAfterBinding(node, arg);
+ } finally {
+ foreach (VCExprVar! v in node.BoundVars)
+ RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);
+ }
+ return res;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+ // The possibility is provided to look at a (quantifier or let) node
+ // after its bound variables have been registered
+ // (when overriding the normal visit-methods, the node will be visited
+ // before the binding happens)
+
+ protected virtual Result VisitAfterBinding(VCExprQuantifier! node, Arg arg) {
+ return base.Visit(node, arg);
+ }
+
+ protected virtual Result VisitAfterBinding(VCExprLet! node, Arg arg) {
+ return base.Visit(node, arg);
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+ // General visitor for recursively collecting information in a VCExpr.
+ // As the visitor is not used anywhere for the time being, it maybe should
+ // be removed
+
+ public abstract class CollectingVCExprVisitor<Result, Arg>
+ : IVCExprVisitor<Result, Arg> {
+ protected abstract Result CombineResults(List<Result>! results, Arg arg);
+
+ public Result Collect(VCExpr! node, Arg arg) {
+ return node.Accept(this, arg);
+ }
+
+ public virtual Result Visit(VCExprLiteral! node, Arg arg) {
+ return CombineResults(new List<Result> (), arg);
+ }
+ public virtual Result Visit(VCExprNAry! node, Arg arg) {
+ List<Result>! results = new List<Result> ();
+ foreach (VCExpr! subnode in node)
+ results.Add(subnode.Accept(this, arg));
+ return CombineResults(results, arg);
+ }
+ public virtual Result Visit(VCExprVar! node, Arg arg) {
+ return CombineResults(new List<Result> (), arg);
+ }
+ public virtual Result Visit(VCExprQuantifier! node, Arg arg) {
+ List<Result>! result = new List<Result> ();
+ result.Add(node.Body.Accept(this, arg));
+ foreach (VCTrigger! trigger in node.Triggers)
+ foreach (VCExpr! expr in trigger.Exprs)
+ result.Add(expr.Accept(this, arg));
+ return CombineResults(result, arg);
+ }
+ public virtual Result Visit(VCExprLet! node, Arg arg) {
+ List<Result>! results = new List<Result> ();
+ // visit the bound expressions first
+ foreach (VCExprLetBinding! binding in node)
+ results.Add(binding.E.Accept(this, arg));
+ results.Add(node.Body.Accept(this, arg));
+ return CombineResults(results, arg);
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public class SizeComputingVisitor : TraversingVCExprVisitor<bool, bool> {
+
+ private int Size = 0;
+
+ public static int ComputeSize(VCExpr! expr) {
+ SizeComputingVisitor! visitor = new SizeComputingVisitor();
+ visitor.Traverse(expr, true);
+ return visitor.Size;
+ }
+
+ protected override bool StandardResult(VCExpr! node, bool arg) {
+ Size = Size + 1;
+ return true;
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Collect all free term and type variables in a VCExpr. Type variables
+ // can occur free either in the types of bound variables, or in the type
+ // parameters of VCExprNAry.
+
+ // the result and argument (of type bool) are not used currently
+ public class FreeVariableCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+ public readonly Dictionary<VCExprVar!,object>! FreeTermVars = new Dictionary<VCExprVar!,object> ();
+ public readonly List<TypeVariable!>! FreeTypeVars = new List<TypeVariable!> ();
+
+ // not used
+ protected override bool StandardResult(VCExpr! node, bool arg) {
+ return true;
+ }
+
+ public static Dictionary<VCExprVar!,object>! FreeTermVariables(VCExpr! node) {
+ FreeVariableCollector collector = new FreeVariableCollector ();
+ collector.Traverse(node, true);
+ return collector.FreeTermVars;
+ }
+
+ public static List<TypeVariable!>! FreeTypeVariables(VCExpr! node) {
+ FreeVariableCollector collector = new FreeVariableCollector ();
+ collector.Traverse(node, true);
+ return collector.FreeTypeVars;
+ }
+
+ public void Reset() {
+ FreeTermVars.Clear();
+ FreeTypeVars.Clear();
+ }
+
+ public void Collect(VCExpr! node) {
+ Traverse(node, true);
+ }
+
+ public void Collect(Type! type) {
+ AddTypeVariables(type.FreeVariables.ToList());
+ }
+
+ /////////////////////////////////////////////////////////////////////////
+
+ private void CollectTypeVariables(IEnumerable<VCExprVar!>! boundVars) {
+ foreach (VCExprVar! var in boundVars)
+ Collect(var.Type);
+ }
+
+ private void AddTypeVariables(IEnumerable<TypeVariable!>! typeVars) {
+ foreach (TypeVariable! tvar in typeVars)
+ if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar))
+ FreeTypeVars.Add(tvar);
+ }
+
+ public override bool Visit(VCExprVar! node, bool arg) {
+ if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) {
+ FreeTermVars.Add(node, null);
+ Collect(node.Type);
+ }
+ return true;
+ }
+
+ public override bool Visit(VCExprNAry! node, bool arg) {
+ foreach (Type! t in node.TypeArguments)
+ Collect(t);
+ return base.Visit(node, arg);
+ }
+
+ protected override bool VisitAfterBinding(VCExprQuantifier! node, bool arg) {
+ CollectTypeVariables(node.BoundVars);
+ return base.VisitAfterBinding(node, arg);
+ }
+
+ protected override bool VisitAfterBinding(VCExprLet! node, bool arg) {
+ CollectTypeVariables(node.BoundVars);
+ return base.VisitAfterBinding(node, arg);
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Framework for mutating VCExprs
+
+ // The Visit implementations in the following visitor work
+ // recursively, apart from the implementation for VCExprNAry that
+ // uses its own stack when applied to nested nodes with the same
+ // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary
+ // to avoid stack overflows (like in TraversingVCExprVisitor)
+
+ public abstract class MutatingVCExprVisitor<Arg>
+ : IVCExprVisitor<VCExpr!, Arg> {
+ protected readonly VCExpressionGenerator! Gen;
+
+ public MutatingVCExprVisitor(VCExpressionGenerator! gen) {
+ this.Gen = gen;
+ }
+
+ public VCExpr! Mutate(VCExpr! expr, Arg arg) {
+ return expr.Accept(this, arg);
+ }
+
+ public List<VCExpr!>! MutateSeq(IEnumerable<VCExpr!>! exprs, Arg arg) {
+ List<VCExpr!>! res = new List<VCExpr!> ();
+ foreach (VCExpr! expr in exprs)
+ res.Add(expr.Accept(this, arg));
+ return res;
+ }
+
+ private List<VCExpr!>! MutateList(List<VCExpr!>! exprs, Arg arg) {
+ bool changed = false;
+ List<VCExpr!>! res = new List<VCExpr!> ();
+ foreach (VCExpr! expr in exprs) {
+ VCExpr! newExpr = expr.Accept(this, arg);
+ if (!Object.ReferenceEquals(expr, newExpr))
+ changed = true;
+ res.Add(newExpr);
+ }
+ if (!changed)
+ return exprs;
+ return res;
+ }
+
+ public virtual VCExpr! Visit(VCExprLiteral! node, Arg arg) {
+ return node;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Special element used to mark the positions in the todo-stack where
+ // results have to be popped from the result-stack.
+ private static readonly VCExpr! CombineResultsMarker = new VCExprLiteral (Type.Bool);
+
+ // The todo-stack contains records of the shape
+ //
+ // arg0
+ // arg1
+ // arg2
+ // ...
+ // CombineResultsMarker
+ // f(arg0, arg1, arg2, ...) (the original expression)
+
+ private readonly Stack<VCExpr!>! NAryExprTodoStack = new Stack<VCExpr!> ();
+ private readonly Stack<VCExpr!>! NAryExprResultStack = new Stack<VCExpr!> ();
+
+ private void PushTodo(VCExprNAry! exprTodo) {
+ NAryExprTodoStack.Push(exprTodo);
+ NAryExprTodoStack.Push(CombineResultsMarker);
+ for (int i = exprTodo.Arity - 1; i >= 0; --i)
+ NAryExprTodoStack.Push(exprTodo[i]);
+ }
+
+ public virtual VCExpr! Visit(VCExprNAry! node, Arg arg) {
+ VCExprOp! op = node.Op;
+ int initialStackSize = NAryExprTodoStack.Count;
+ int initialResultStackSize = NAryExprResultStack.Count;
+
+ PushTodo(node);
+
+ while (NAryExprTodoStack.Count > initialStackSize) {
+ VCExpr! subExpr = NAryExprTodoStack.Pop();
+
+ if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) {
+ //
+ // assemble a result
+ VCExprNAry! originalExpr = (VCExprNAry)NAryExprTodoStack.Pop();
+ bool changed = false;
+ List<VCExpr!>! newSubExprs = new List<VCExpr!> ();
+
+ for (int i = op.Arity - 1; i >= 0; --i) {
+ VCExpr! nextSubExpr = NAryExprResultStack.Pop();
+ if (!Object.ReferenceEquals(nextSubExpr, originalExpr[i]))
+ changed = true;
+ newSubExprs.Insert(0, nextSubExpr);
+ }
+
+ NAryExprResultStack.Push(UpdateModifiedNode(originalExpr, newSubExprs, changed, arg));
+ //
+ } else {
+ //
+ VCExprNAry narySubExpr = subExpr as VCExprNAry;
+ if (narySubExpr != null && narySubExpr.Op.Equals(op) &&
+ // as in VCExprNAryUniformOpEnumerator, all expressions with
+ // type parameters are allowed to be inspected more closely
+ narySubExpr.TypeParamArity == 0) {
+ PushTodo(narySubExpr);
+ } else {
+ NAryExprResultStack.Push(subExpr.Accept(this, arg));
+ }
+ //
+ }
+ }
+
+ assert NAryExprTodoStack.Count == initialStackSize &&
+ NAryExprResultStack.Count == initialResultStackSize + 1;
+ return NAryExprResultStack.Pop();
+ }
+
+ protected virtual VCExpr! UpdateModifiedNode(VCExprNAry! originalNode,
+ List<VCExpr!>! newSubExprs,
+ // has any of the subexpressions changed?
+ bool changed,
+ Arg arg) {
+ if (changed)
+ return Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ return originalNode;
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public virtual VCExpr! Visit(VCExprVar! node, Arg arg) {
+ return node;
+ }
+
+ protected List<VCTrigger!>! MutateTriggers(List<VCTrigger!>! triggers, Arg arg) {
+ List<VCTrigger!>! newTriggers = new List<VCTrigger!> ();
+ bool changed = false;
+ foreach (VCTrigger! trigger in triggers) {
+ List<VCExpr!>! exprs = trigger.Exprs;
+ List<VCExpr!>! newExprs = MutateList(exprs, arg);
+ if (Object.ReferenceEquals(exprs, newExprs)) {
+ newTriggers.Add(trigger);
+ } else {
+ newTriggers.Add(Gen.Trigger(trigger.Pos, newExprs));
+ changed = true;
+ }
+ }
+ if (!changed)
+ return triggers;
+ return newTriggers;
+ }
+
+ public virtual VCExpr! Visit(VCExprQuantifier! node, Arg arg) {
+ bool changed = false;
+
+ VCExpr! body = node.Body;
+ VCExpr! newbody = body.Accept(this, arg);
+ if (!Object.ReferenceEquals(body, newbody))
+ changed = true;
+
+ // visit the trigger expressions as well
+ List<VCTrigger!>! triggers = node.Triggers;
+ List<VCTrigger!>! newTriggers = MutateTriggers(triggers, arg);
+ if (!Object.ReferenceEquals(triggers, newTriggers))
+ changed = true;
+
+ if (!changed)
+ return node;
+ return Gen.Quantify(node.Quan, node.TypeParameters, node.BoundVars,
+ newTriggers, node.Infos, newbody);
+ }
+
+ public virtual VCExpr! Visit(VCExprLet! node, Arg arg) {
+ bool changed = false;
+
+ VCExpr! body = node.Body;
+ VCExpr! newbody = body.Accept(this, arg);
+ if (!Object.ReferenceEquals(body, newbody))
+ changed = true;
+
+ List<VCExprLetBinding!>! newbindings = new List<VCExprLetBinding!> ();
+ for (int i = 0; i < node.Length; ++i) {
+ VCExprLetBinding! binding = node[i];
+ VCExpr! e = binding.E;
+ VCExpr! newE = e.Accept(this, arg);
+ if (Object.ReferenceEquals(e, newE)) {
+ newbindings.Add(binding);
+ } else {
+ changed = true;
+ newbindings.Add(Gen.LetBinding(binding.V, newE));
+ }
+ }
+
+ if (!changed)
+ return node;
+ return Gen.Let(newbindings, newbody);
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Substitutions and a visitor for applying substitutions. A substitution can
+ // substitute both type variables and term variables
+
+ public class VCExprSubstitution {
+ private readonly List<IDictionary<VCExprVar!, VCExpr!>!>! TermSubsts;
+ private readonly List<IDictionary<TypeVariable!, Type!>!>! TypeSubsts;
+
+ public VCExprSubstitution(IDictionary<VCExprVar!, VCExpr!>! termSubst,
+ IDictionary<TypeVariable!, Type!>! typeSubst) {
+ List<IDictionary<VCExprVar!, VCExpr!>!>! termSubsts =
+ new List<IDictionary<VCExprVar!, VCExpr!>!> ();
+ termSubsts.Add(termSubst);
+ List<IDictionary<TypeVariable!, Type!>!>! typeSubsts =
+ new List<IDictionary<TypeVariable!, Type!>!> ();
+ typeSubsts.Add(typeSubst);
+ this.TermSubsts = termSubsts;
+ this.TypeSubsts = typeSubsts;
+ }
+
+ public VCExprSubstitution() {
+ this(new Dictionary<VCExprVar!, VCExpr!> (), new Dictionary<TypeVariable!, Type!> ());
+ }
+
+ public void PushScope() {
+ TermSubsts.Add(new Dictionary<VCExprVar!, VCExpr!> ());
+ TypeSubsts.Add(new Dictionary<TypeVariable!, Type!> ());
+ }
+
+ public void PopScope() {
+ TermSubsts.RemoveAt(TermSubsts.Count - 1);
+ TypeSubsts.RemoveAt(TypeSubsts.Count - 1);
+ }
+
+ public VCExpr this[VCExprVar! var] {
+ get {
+ VCExpr res;
+ for (int i = TermSubsts.Count - 1; i >= 0; --i) {
+ if (TermSubsts[i].TryGetValue(var, out res))
+ return res;
+ }
+ return null;
+ }
+ set {
+ TermSubsts[TermSubsts.Count - 1][var] = (!)value;
+ }
+ }
+
+ public Type this[TypeVariable! var] {
+ get {
+ Type res;
+ for (int i = TypeSubsts.Count - 1; i >= 0; --i) {
+ if (TypeSubsts[i].TryGetValue(var, out res))
+ return res;
+ }
+ return null;
+ }
+ set {
+ TypeSubsts[TypeSubsts.Count - 1][var] = (!)value;
+ }
+ }
+
+ public bool ContainsKey(VCExprVar! var) {
+ return this[var] != null;
+ }
+
+ public bool ContainsKey(TypeVariable! var) {
+ return this[var] != null;
+ }
+
+ public bool TermSubstIsEmpty { get {
+ return forall{IDictionary<VCExprVar!, VCExpr!>! dict in TermSubsts;
+ dict.Count == 0};
+ } }
+
+ public bool TypeSubstIsEmpty { get {
+ return forall{IDictionary<TypeVariable!, Type!>! dict in TypeSubsts;
+ dict.Count == 0};
+ } }
+
+ public IDictionary<TypeVariable!, Type!>! ToTypeSubst { get {
+ IDictionary<TypeVariable!, Type!>! res = new Dictionary<TypeVariable!, Type!> ();
+ foreach (IDictionary<TypeVariable!, Type!>! dict in TypeSubsts)
+ foreach (KeyValuePair<TypeVariable!, Type!> pair in dict)
+ // later ones overwrite earlier ones
+ res[pair.Key] = pair.Value;
+ return res;
+ } }
+
+ // the variables that are not mapped to themselves
+ public IEnumerable<VCExprVar!>! TermDomain { get {
+ Dictionary<VCExprVar!, bool>! domain = new Dictionary<VCExprVar!, bool> ();
+ foreach (IDictionary<VCExprVar!, VCExpr!>! dict in TermSubsts)
+ foreach (VCExprVar! var in dict.Keys)
+ if (!var.Equals(this[var]))
+ domain.Add(var, true);
+ return domain.Keys;
+ } }
+
+ // the variables that are not mapped to themselves
+ public IEnumerable<TypeVariable!>! TypeDomain { get {
+ Dictionary<TypeVariable!, bool>! domain = new Dictionary<TypeVariable!, bool> ();
+ foreach (IDictionary<TypeVariable!, Type!>! dict in TypeSubsts)
+ foreach (TypeVariable! var in dict.Keys)
+ if (!var.Equals(this[var]))
+ domain.Add(var, true);
+ return domain.Keys;
+ } }
+
+ public FreeVariableCollector! Codomains { get {
+ FreeVariableCollector! coll = new FreeVariableCollector ();
+ foreach (VCExprVar! var in TermDomain)
+ coll.Collect((!)this[var]);
+ foreach (TypeVariable! var in TypeDomain)
+ coll.Collect((!)this[var]);
+ return coll;
+ } }
+
+ public VCExprSubstitution! Clone() {
+ VCExprSubstitution! res = new VCExprSubstitution ();
+ foreach (IDictionary<VCExprVar!, VCExpr!>! dict in TermSubsts)
+ res.TermSubsts.Add(HelperFuns.Clone(dict));
+ foreach (IDictionary<TypeVariable!, Type!>! dict in TypeSubsts)
+ res.TypeSubsts.Add(HelperFuns.Clone(dict));
+ return res;
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////
+
+ public class SubstitutingVCExprVisitor
+ : MutatingVCExprVisitor<VCExprSubstitution!> {
+ public SubstitutingVCExprVisitor(VCExpressionGenerator! gen) {
+ base(gen);
+ }
+
+ // when descending across a binder, we have to check that no collisions
+ // or variable capture can occur. if this might happen, we replace the
+ // term and type variables bound by the binder with fresh variables
+ private bool CollisionPossible(IEnumerable<TypeVariable!>! typeParams,
+ IEnumerable<VCExprVar!>! boundVars,
+ VCExprSubstitution! substitution) {
+ // variables can be shadowed by a binder
+ if (exists{TypeVariable! var in typeParams; substitution.ContainsKey(var)} ||
+ exists{VCExprVar! var in boundVars; substitution.ContainsKey(var)})
+ return true;
+ // compute the codomain of the substitution
+ FreeVariableCollector! coll = substitution.Codomains;
+ // variables could be captured when applying the substitution
+ return exists{TypeVariable! var in typeParams; coll.FreeTypeVars.Contains(var)} ||
+ exists{VCExprVar! var in boundVars; coll.FreeTermVars.ContainsKey(var)};
+ }
+
+ // can be overwritten if names of bound variables are to be changed
+ protected virtual string! ChooseNewVariableName(string! oldName) {
+ return oldName;
+ }
+
+ // handle type parameters in VCExprNAry
+ protected override VCExpr! UpdateModifiedNode(VCExprNAry! originalNode,
+ List<VCExpr!>! newSubExprs,
+ bool changed,
+ VCExprSubstitution! substitution) {
+ List<Type!>! typeParams = new List<Type!> ();
+ foreach (Type! t in originalNode.TypeArguments) {
+ Type! newType = t.Substitute(substitution.ToTypeSubst);
+ if (!ReferenceEquals(t, newType))
+ changed = true;
+ typeParams.Add(newType);
+ }
+ if (changed)
+ return Gen.Function(originalNode.Op, newSubExprs, typeParams);
+ else
+ return originalNode;
+ }
+
+ public override VCExpr! Visit(VCExprQuantifier! node,
+ VCExprSubstitution! substitution) {
+ // the default is to refresh bound variables only if necessary
+ // because of collisions
+ return Visit(node, substitution, false);
+ }
+
+ public VCExpr! Visit(VCExprQuantifier! node,
+ VCExprSubstitution! substitution,
+ bool refreshBoundVariables) {
+ substitution.PushScope(); try {
+
+ List<TypeVariable!>! typeParams = node.TypeParameters;
+ bool refreshAllVariables = refreshBoundVariables ||
+ CollisionPossible(node.TypeParameters, node.BoundVars, substitution);
+ if (refreshAllVariables) {
+ // we introduce fresh type variables to ensure that none gets captured
+ typeParams = new List<TypeVariable!> ();
+ foreach (TypeVariable! var in node.TypeParameters) {
+ TypeVariable! freshVar =
+ new TypeVariable (Token.NoToken, ChooseNewVariableName(var.Name));
+ typeParams.Add(freshVar);
+ substitution[var] = freshVar;
+ // this might overwrite other elements of the substitution, deliberately
+ }
+ }
+
+ List<VCExprVar!>! boundVars = node.BoundVars;
+ if (refreshAllVariables || !substitution.TypeSubstIsEmpty) {
+ // collisions are possible, or we also substitute type variables. in this case
+ // the bound term variables have to be replaced with fresh variables with the
+ // right types
+ boundVars = new List<VCExprVar!> ();
+ IDictionary<TypeVariable!, Type!>! typeSubst = substitution.ToTypeSubst;
+ foreach (VCExprVar! var in node.BoundVars) {
+ VCExprVar! freshVar =
+ Gen.Variable(ChooseNewVariableName(var.Name),
+ var.Type.Substitute(typeSubst));
+ boundVars.Add(freshVar);
+ substitution[var] = freshVar;
+ // this might overwrite other elements of the substitution, deliberately
+ }
+ }
+
+ List<VCTrigger!>! newTriggers = new List<VCTrigger!> ();
+ foreach (VCTrigger! trigger in node.Triggers)
+ newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution)));
+
+ VCExpr! newBody = Mutate(node.Body, substitution);
+
+ return Gen.Quantify(node.Quan, typeParams, boundVars,
+ newTriggers, node.Infos, newBody);
+
+ } finally {
+ substitution.PopScope();
+ }
+ }
+
+ public override VCExpr! Visit(VCExprVar! node,
+ VCExprSubstitution! substitution) {
+ VCExpr res = substitution[node];
+ if (res != null)
+ return res;
+ return node;
+ }
+
+ public override VCExpr! Visit(VCExprLet! node,
+ VCExprSubstitution! substitution) {
+ // the default is to refresh bound variables only if necessary
+ // because of collisions
+ return Visit(node, substitution, false);
+ }
+
+ public VCExpr! Visit(VCExprLet! node,
+ VCExprSubstitution! substitution,
+ bool refreshBoundVariables) {
+ // let-expressions do not have type parameters (fortunately ...)
+ substitution.PushScope (); try {
+
+ bool refreshAllVariables =
+ refreshBoundVariables ||
+ !substitution.TypeSubstIsEmpty ||
+ CollisionPossible(new List<TypeVariable!> (), node.BoundVars, substitution);
+
+ List<VCExprVar!>! newBoundVars = node.BoundVars;
+ if (refreshAllVariables) {
+ // collisions are possible, or we also substitute type variables. in this case
+ // the bound term variables have to be replaced with fresh variables with the
+ // right types
+ newBoundVars = new List<VCExprVar!> ();
+ IDictionary<TypeVariable!, Type!>! typeSubst = substitution.ToTypeSubst;
+ foreach (VCExprVar! var in node.BoundVars) {
+ VCExprVar! freshVar =
+ Gen.Variable(ChooseNewVariableName(var.Name),
+ var.Type.Substitute(typeSubst));
+ newBoundVars.Add(freshVar);
+ substitution[var] = freshVar;
+ // this might overwrite other elements of the substitution, deliberately
+ }
+ }
+
+ List<VCExprLetBinding!>! newbindings = new List<VCExprLetBinding!> ();
+ for (int i = 0; i < node.Length; ++i) {
+ VCExprLetBinding! binding = node[i];
+ newbindings.Add(Gen.LetBinding(newBoundVars[i], Mutate(binding.E, substitution)));
+ }
+
+ VCExpr! newBody = Mutate(node.Body, substitution);
+ return Gen.Let(newbindings, newBody);
+
+ } finally {
+ substitution.PopScope();
+ }
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ public abstract class StandardVCExprOpVisitor<Result, Arg>
+ : IVCExprOpVisitor<Result, Arg> {
+ protected abstract Result StandardResult(VCExprNAry! node, Arg arg);
+
+ public virtual Result VisitNotOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitEqOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitNeqOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitAndOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitOrOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitImpliesOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitDistinctOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLabelOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSelectOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitStoreOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvExtractOp(VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvConcatOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitAddOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitMulOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitDivOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitModOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLtOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLeOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitGtOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitGeOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubtypeOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubtype3Op (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
+ }
+
+}
+
+
|