mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph/SymGraph.cs

   1 //
   2 // SymGraph.cs
   3 //
   4 // Authors:
   5 //      Alexander Chebaturkin (chebaturkin@gmail.com)
   6 //
   7 // Copyright (C) 2011 Alexander Chebaturkin
   8 //
   9 // Permission is hereby granted, free of charge, to any person obtaining
  10 // a copy of this software and associated documentation files (the
  11 // "Software"), to deal in the Software without restriction, including
  12 // without limitation the rights to use, copy, modify, merge, publish,
  13 // distribute, sublicense, and/or sell copies of the Software, and to
  14 // permit persons to whom the Software is furnished to do so, subject to
  15 // the following conditions:
  16 //
  17 // The above copyright notice and this permission notice shall be
  18 // included in all copies or substantial portions of the Software.
  19 //
  20 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  21 // EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  22 // MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  23 // NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
  24 // LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
  25 // OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
  26 // WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  27 //
  28
  29 using System;
  30 using System.Collections.Generic;
  31 using System.IO;
  32 using System.Linq;
  33 using Mono.CodeContracts.Static.DataStructures;
  34 using Mono.CodeContracts.Static.Extensions;
  35
  36 namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph {
  37         class SymGraph<TFunc, TADomain> : ISymGraph<TFunc, TADomain, SymGraph<TFunc, TADomain>>
  38                 where TFunc : IEquatable<TFunc>, IConstantInfo
  39                 where TADomain : IAbstractDomainForEGraph<TADomain>, IEquatable<TADomain> {
  40                 public const bool DoIncrementalJoin = false;
  41                 private static int egraphIdGenerator;
  42                 private static SymGraph<TFunc, TADomain> BottomValue;
  43                 public readonly SymValue BottomPlaceHolder;
  44                 public readonly SymGraph<TFunc, TADomain> Parent;
  45                 public readonly TADomain UnderlyingTopValue;
  46
  47                 private readonly SymValue const_root;
  48                 private readonly int egraph_id;
  49                 private readonly int history_size;
  50
  51                 private readonly SymGraph<TFunc, TADomain> root_graph;
  52
  53                 private readonly TADomain underlying_bottom_value;
  54                 private IImmutableMap<SymValue, TADomain> abs_map;
  55                 private IImmutableMap<SymValue, SymValue> forw_map;
  56                 private bool is_immutable;
  57
  58                 public SymGraph (TADomain topValue, TADomain bottomValue)
  59                         : this (topValue, bottomValue, false)
  60                 {
  61                         if (BottomValue != null)
  62                                 return;
  63                         BottomValue = new SymGraph<TFunc, TADomain> (topValue, bottomValue, false);
  64                 }
  65
  66                 private SymGraph (TADomain topValue, TADomain bottomValue, bool _)
  67                 {
  68                         this.egraph_id = egraphIdGenerator++;
  69                         this.const_root = FreshSymbol ();
  70
  71                         TermMap = DoubleImmutableMap<SymValue, TFunc, SymValue>.Empty (SymValue.GetUniqueKey);
  72                         MultiEdgeMap = DoubleImmutableMap<SymValue, MultiEdge<TFunc, TADomain>, LispList<SymValue>>.Empty (SymValue.GetUniqueKey);
  73                         this.abs_map = ImmutableIntKeyMap<SymValue, TADomain>.Empty (SymValue.GetUniqueKey);
  74                         this.forw_map = ImmutableIntKeyMap<SymValue, SymValue>.Empty (SymValue.GetUniqueKey);
  75                         EqualTermsMap = ImmutableIntKeyMap<SymValue, LispList<SymGraphTerm<TFunc>>>.Empty (SymValue.GetUniqueKey);
  76                         EqualMultiTermsMap = ImmutableIntKeyMap<SymValue, SymGraphTerm<TFunc>>.Empty (SymValue.GetUniqueKey);
  77
  78                         this.BottomPlaceHolder = FreshSymbol ();
  79                         this.abs_map = this.abs_map.Add (this.BottomPlaceHolder, bottomValue);
  80                         this.is_immutable = false;
  81                         this.history_size = 1;
  82                         this.Parent = null;
  83                         this.root_graph = this;
  84                         Updates = null;
  85                         this.UnderlyingTopValue = topValue;
  86                         this.underlying_bottom_value = bottomValue;
  87                 }
  88
  89                 private SymGraph (SymGraph<TFunc, TADomain> from)
  90                 {
  91                         this.egraph_id = egraphIdGenerator++;
  92                         this.const_root = from.const_root;
  93                         this.BottomPlaceHolder = from.BottomPlaceHolder;
  94                         TermMap = from.TermMap;
  95                         MultiEdgeMap = from.MultiEdgeMap;
  96                         IdGenerator = from.IdGenerator;
  97                         this.abs_map = from.abs_map;
  98                         this.forw_map = from.forw_map;
  99                         EqualTermsMap = from.EqualTermsMap;
 100                         EqualMultiTermsMap = from.EqualMultiTermsMap;
 101                         this.UnderlyingTopValue = from.UnderlyingTopValue;
 102                         this.underlying_bottom_value = from.underlying_bottom_value;
 103                         Updates = from.Updates;
 104                         this.Parent = from;
 105                         this.root_graph = from.root_graph;
 106                         this.history_size = from.history_size + 1;
 107
 108                         from.MarkAsImmutable ();
 109                 }
 110
 111                 public IImmutableMap<SymValue, SymGraphTerm<TFunc>> EqualMultiTermsMap { get; private set; }
 112                 public IImmutableMap<SymValue, LispList<SymGraphTerm<TFunc>>> EqualTermsMap { get; private set; }
 113                 public DoubleImmutableMap<SymValue, MultiEdge<TFunc, TADomain>, LispList<SymValue>> MultiEdgeMap { get; private set; }
 114                 public DoubleImmutableMap<SymValue, TFunc, SymValue> TermMap { get; private set; }
 115                 public int IdGenerator { get; private set; }
 116                 public LispList<Update<TFunc, TADomain>> Updates { get; private set; }
 117
 118                 public bool IsImmutable
 119                 {
 120                         get { return this.is_immutable; }
 121                 }
 122
 123                 private int LastSymbolId
 124                 {
 125                         get { return IdGenerator; }
 126                 }
 127
 128                 public SymValue this [SymValue[] args, TFunc function]
 129                 {
 130                         get
 131                         {
 132                                 int len = args.Length;
 133                                 for (int i = 0; i < len; i++)
 134                                         args [i] = Find (args [i]);
 135
 136                                 SymValue candidate = FindCandidate (args, function);
 137                                 if (candidate != null)
 138                                         return candidate;
 139                                 candidate = FreshSymbol ();
 140                                 for (int i = 0; i < len; i++) {
 141                                         var edge = new MultiEdge<TFunc, TADomain> (function, i, len);
 142                                         MultiEdgeMap = MultiEdgeMap.Add (args [i], edge, MultiEdgeMap [args [i], edge].Cons (candidate));
 143                                 }
 144                                 EqualMultiTermsMap = EqualMultiTermsMap.Add (candidate, new SymGraphTerm<TFunc> (function, args));
 145                                 AddMultiEdgeUpdate (args, function);
 146                                 return candidate;
 147                         }
 148                         set
 149                         {
 150                                 int len = args.Length;
 151                                 for (int i = 0; i < len; i++)
 152                                         args [i] = Find (args [i]);
 153
 154                                 bool isTermEqual = true;
 155                                 SymGraphTerm<TFunc> term = EqualMultiTermsMap [value];
 156                                 if (term.Args != null) {
 157                                         for (int i = 0; i < len; i++) {
 158                                                 if (term.Args [i] != args [i]) {
 159                                                         isTermEqual = false;
 160                                                         break;
 161                                                 }
 162                                         }
 163                                 }
 164
 165                                 for (int i = 0; i < len; i++) {
 166                                         var edge = new MultiEdge<TFunc, TADomain> (function, i, len);
 167                                         LispList<SymValue> list = MultiEdgeMap [args [i], edge];
 168                                         if (isTermEqual && !LispList<SymValue>.Contains (list, value))
 169                                                 isTermEqual = false;
 170                                         if (!isTermEqual)
 171                                                 MultiEdgeMap = MultiEdgeMap.Add (args [i], edge, list.Cons (value));
 172                                 }
 173                                 if (isTermEqual)
 174                                         return;
 175                                 EqualMultiTermsMap = EqualMultiTermsMap.Add (value, new SymGraphTerm<TFunc> (function, args));
 176                                 AddMultiEdgeUpdate (args, function);
 177                         }
 178                 }
 179
 180                 public SymValue this [TFunc function, params SymValue[] args]
 181                 {
 182                         get { return this [args, function]; }
 183                 }
 184
 185                 private SymValue this [SymValue source, TFunc function]
 186                 {
 187                         get
 188                         {
 189                                 source = Find (source);
 190                                 SymValue sv = TermMap [source, function];
 191                                 SymValue key;
 192                                 if (sv == null) {
 193                                         key = FreshSymbol ();
 194                                         TermMap = TermMap.Add (source, function, key);
 195                                         EqualTermsMap = EqualTermsMap.Add (key, LispList<SymGraphTerm<TFunc>>.Cons (new SymGraphTerm<TFunc> (function, source), null));
 196                                         AddEdgeUpdate (source, function);
 197                                 } else
 198                                         key = Find (sv);
 199
 200                                 return key;
 201                         }
 202                         set
 203                         {
 204                                 source = Find (source);
 205                                 value = Find (value);
 206
 207                                 TermMap = TermMap.Add (source, function, value);
 208                                 LispList<SymGraphTerm<TFunc>> rest = EqualTermsMap [value];
 209                                 if (rest.IsEmpty () || (!rest.Head.Function.Equals (function) || rest.Head.Args [0] != source))
 210                                         EqualTermsMap = EqualTermsMap.Add (value, rest.Cons (new SymGraphTerm<TFunc> (function, source)));
 211
 212                                 AddEdgeUpdate (source, function);
 213                         }
 214                 }
 215
 216                 public IEnumerable<Pair<SymValue, SymGraphTerm<TFunc>>> ValidMultiTerms {
 217                         get
 218                         {
 219                                 foreach (SymValue sv in EqualMultiTermsMap.Keys) {
 220                                         SymGraphTerm<TFunc> term = EqualMultiTermsMap [sv];
 221                                         if (IsValidMultiTerm (term))
 222                                                 yield return new Pair<SymValue, SymGraphTerm<TFunc>> (sv, term);
 223                                 }
 224                         }
 225                 }
 226
 227                 public SymValue ConstRoot
 228                 {
 229                         get { return this.const_root; }
 230                 }
 231
 232                 #region ISymGraph<TFunc,TADomain,SymGraph<TFunc,TADomain>> Members
 233                 public TADomain this [SymValue symbol]
 234                 {
 235                         get
 236                         {
 237                                 symbol = Find (symbol);
 238                                 if (this.abs_map.ContainsKey (symbol))
 239                                         return this.abs_map [symbol];
 240
 241                                 return this.UnderlyingTopValue;
 242                         }
 243                         set
 244                         {
 245                                 SymValue newSym = Find (symbol);
 246                                 if (this [symbol].Equals (value))
 247                                         return;
 248                                 AddAbstractValueUpdate (newSym);
 249                                 if (value.IsTop)
 250                                         this.abs_map = this.abs_map.Remove (newSym);
 251                                 else
 252                                         this.abs_map = this.abs_map.Add (newSym, value);
 253                         }
 254                 }
 255
 256                 public SymValue this [TFunc function]
 257                 {
 258                         get { return this [this.const_root, function]; }
 259                         set { this [this.const_root, function] = value; }
 260                 }
 261
 262                 public SymValue this [TFunc function, SymValue arg]
 263                 {
 264                         get { return this [arg, function]; }
 265                         set { this [arg, function] = value; }
 266                 }
 267
 268                 public IEnumerable<TFunc> Constants
 269                 {
 270                         get { return TermMap.Keys2 (this.const_root); }
 271                 }
 272
 273                 public IEnumerable<SymValue> Variables
 274                 {
 275                         get { return TermMap.Keys1; }
 276                 }
 277
 278                 public SymGraph<TFunc, TADomain> Top
 279                 {
 280                         get { return new SymGraph<TFunc, TADomain> (this.UnderlyingTopValue, this.underlying_bottom_value); }
 281                 }
 282
 283                 public SymGraph<TFunc, TADomain> Bottom
 284                 {
 285                         get
 286                         {
 287                                 if (BottomValue == null) {
 288                                         BottomValue = new SymGraph<TFunc, TADomain> (this.UnderlyingTopValue, this.underlying_bottom_value);
 289                                         BottomValue.MarkAsImmutable ();
 290                                 }
 291                                 return BottomValue;
 292                         }
 293                 }
 294
 295                 public bool IsTop
 296                 {
 297                         get { return TermMap.Keys2Count (this.const_root) == 0; }
 298                 }
 299
 300                 public bool IsBottom
 301                 {
 302                         get { return this == BottomValue; }
 303                 }
 304
 305                 public SymValue FreshSymbol ()
 306                 {
 307                         return new SymValue (++IdGenerator);
 308                 }
 309
 310                 public SymValue TryLookup (TFunc function)
 311                 {
 312                         return LookupWithoutManifesting (this.const_root, function);
 313                 }
 314
 315                 public SymValue TryLookup (TFunc function, SymValue arg)
 316                 {
 317                         return LookupWithoutManifesting (arg, function);
 318                 }
 319
 320                 public void Eliminate (TFunc function, SymValue arg)
 321                 {
 322                         SymValue value = Find (arg);
 323                         DoubleImmutableMap<SymValue, TFunc, SymValue> newTermMap = TermMap.Remove (value, function);
 324                         if (newTermMap == TermMap)
 325                                 return;
 326                         TermMap = newTermMap;
 327                         AddEliminateEdgeUpdate (value, function);
 328                 }
 329
 330                 public void Eliminate (TFunc function)
 331                 {
 332                         TermMap = TermMap.Remove (this.const_root, function);
 333                         AddEliminateEdgeUpdate (this.const_root, function);
 334                 }
 335
 336                 public void EliminateAll (SymValue arg)
 337                 {
 338                         SymValue value = Find (arg);
 339                         AddEliminateAllUpdate (value);
 340                         TermMap = TermMap.RemoveAll (value);
 341                         this [arg] = this.UnderlyingTopValue;
 342                 }
 343
 344                 public void AssumeEqual (SymValue v1, SymValue v2)
 345                 {
 346                         var workList = new WorkList<EqualityPair<TFunc, TADomain>> ();
 347                         SymValue sv1 = Find (v1);
 348                         SymValue sv2 = Find (v2);
 349
 350                         if (TryPushEquality (workList, sv1, sv2))
 351                                 AddEqualityUpdate (sv1, sv2);
 352
 353                         DrainEqualityWorkList (workList);
 354                 }
 355
 356                 public bool IsEqual (SymValue v1, SymValue v2)
 357                 {
 358                         return Find (v1) == Find (v2);
 359                 }
 360
 361                 public IEnumerable<TFunc> Functions (SymValue sv)
 362                 {
 363                         return TermMap.Keys2 (Find (sv));
 364                 }
 365
 366                 public IEnumerable<SymGraphTerm<TFunc>> EqTerms (SymValue sv)
 367                 {
 368                         foreach (var term in EqualTermsMap [Find (sv)].AsEnumerable ()) {
 369                                 if (TryLookup (term.Function, term.Args) == sv)
 370                                         yield return term;
 371                         }
 372                 }
 373
 374                 public SymGraph<TFunc, TADomain> Clone ()
 375                 {
 376                         return new SymGraph<TFunc, TADomain> (this);
 377                 }
 378
 379                 public SymGraph<TFunc, TADomain> Join (SymGraph<TFunc, TADomain> that, bool widening, out bool weaker)
 380                 {
 381                         IMergeInfo info;
 382                         SymGraph<TFunc, TADomain> join = Join (that, out info, widening);
 383                         weaker = info.Changed;
 384                         return join;
 385                 }
 386
 387                 public SymGraph<TFunc, TADomain> Join (SymGraph<TFunc, TADomain> that, out IMergeInfo mergeInfo, bool widen)
 388                 {
 389                         SymGraph<TFunc, TADomain> egraph = this;
 390                         int updateSize;
 391                         SymGraph<TFunc, TADomain> commonTail = ComputeCommonTail (egraph, that, out updateSize);
 392                         bool hasCommonTail = true;
 393                         if (commonTail == null)
 394                                 hasCommonTail = false;
 395
 396                         bool doingIncrementalJoin = hasCommonTail & commonTail != egraph.root_graph & !widen & DoIncrementalJoin;
 397
 398                         //debug
 399
 400                         if (DebugOptions.Debug)
 401                         {
 402                                 Console.WriteLine ("SymGraph {0}", widen ? "widen" : "join");
 403                                 if (commonTail != null)
 404                                         Console.WriteLine ("Last common symbol: {0}", commonTail.LastSymbolId);
 405
 406                                 Console.WriteLine ("  Doing {0}", doingIncrementalJoin ? "incremental join" : "full join");
 407                         }
 408
 409                         SymGraph<TFunc, TADomain> result;
 410                         MergeInfo<TFunc, TADomain> mergeState;
 411                         if (doingIncrementalJoin) {
 412                                 result = new SymGraph<TFunc, TADomain> (commonTail);
 413                                 mergeState = new MergeInfo<TFunc, TADomain> (result, egraph, that, widen);
 414                                 mergeState.Replay (commonTail);
 415                                 mergeState.Commit ();
 416                         } else {
 417                                 result = new SymGraph<TFunc, TADomain> (commonTail);
 418                                 mergeState = new MergeInfo<TFunc, TADomain> (result, egraph, that, widen);
 419                                 mergeState.ReplayEliminations (commonTail);
 420                                 mergeState.AddMapping (egraph.const_root, that.const_root, result.const_root);
 421                                 mergeState.JoinSymbolicValue (egraph.const_root, that.const_root, result.const_root);
 422                                 mergeState.Commit ();
 423                         }
 424                         mergeInfo = mergeState;
 425
 426                         if (DebugOptions.Debug)
 427                         {
 428                                 Console.WriteLine ("  Result update size {0}", result.Updates.Length ());
 429                                 Console.WriteLine ("Done with Egraph join: changed = {0}", mergeInfo.Changed ? 1 : 0);
 430                         }
 431
 432                         return result;
 433                 }
 434
 435                 public void Dump (TextWriter tw)
 436                 {
 437                         var set = new HashSet<SymValue> ();
 438                         var workList = new WorkList<SymValue> ();
 439                         IImmutableMap<SymValue, int> triggers = ImmutableIntKeyMap<SymValue, int>.Empty (SymValue.GetUniqueKey);
 440                         tw.WriteLine ("EGraphId: {0}", this.egraph_id);
 441                         tw.WriteLine ("LastSymbolId: {0}", LastSymbolId);
 442
 443                         foreach (TFunc function in TermMap.Keys2 (this.const_root)) {
 444                                 SymValue sv = this [this.const_root, function];
 445                                 tw.WriteLine ("{0} = {1}", function, sv);
 446                                 workList.Add (sv);
 447                         }
 448
 449                         while (!workList.IsEmpty ()) {
 450                                 SymValue sv = workList.Pull ();
 451                                 if (!set.Add (sv))
 452                                         continue;
 453
 454                                 foreach (TFunc function in TermMap.Keys2 (sv)) {
 455                                         SymValue target = this [sv, function];
 456
 457                                         tw.WriteLine ("{0}({2}) = {1})", function, target, sv);
 458                                         workList.Add (target);
 459                                 }
 460                                 foreach (var edge in MultiEdgeMap.Keys2 (sv)) {
 461                                         foreach (SymValue target in MultiEdgeMap [sv, edge].AsEnumerable ()) {
 462                                                 if (!UpdateTrigger (target, edge, ref triggers))
 463                                                         continue;
 464                                                 SymGraphTerm<TFunc> term = EqualMultiTermsMap [target];
 465                                                 if (term.Args != null) {
 466                                                         tw.WriteLine ("{0}({1}) = {2}",
 467                                                                       term.Function,
 468                                                                       term.Args.ToString (", "), target);
 469                                                         workList.Add (target);
 470                                                 }
 471                                         }
 472                                 }
 473                         }
 474
 475                         tw.WriteLine ("**Abstract value map");
 476                         foreach (SymValue sv in set) {
 477                                 TADomain abstractValue = this [sv];
 478                                 if (!abstractValue.IsTop)
 479                                         tw.WriteLine ("{0} -> {1}", sv, abstractValue);
 480                         }
 481                 }
 482                 #endregion
 483
 484                 #region Implementation of IAbstractDomain<SymGraph<Constant,AbstractValue>>
 485                 public SymGraph<TFunc, TADomain> Meet (SymGraph<TFunc, TADomain> that)
 486                 {
 487                         if (this == that || IsBottom || that.IsTop)
 488                                 return this;
 489                         if (that.IsBottom || IsTop)
 490                                 return that;
 491
 492                         return this;
 493                 }
 494
 495                 public bool LessEqual (SymGraph<TFunc, TADomain> that)
 496                 {
 497                         IImmutableMap<SymValue, LispList<SymValue>> forwardMap;
 498                         IImmutableMap<SymValue, SymValue> backwardMap;
 499
 500                         return LessEqual (that, out forwardMap, out backwardMap);
 501                 }
 502
 503                 public SymGraph<TFunc, TADomain> ImmutableVersion ()
 504                 {
 505                         MarkAsImmutable ();
 506                         return this;
 507                 }
 508
 509                 public bool LessEqual (SymGraph<TFunc, TADomain> that,
 510                         out IImmutableMap<SymValue, LispList<SymValue>> forward,
 511                         out IImmutableMap<SymValue, SymValue> backward)
 512                 {
 513                         if (!IsSameEGraph (that))
 514                                 return InternalLessEqual (this, that, out forward, out backward);
 515
 516                         forward = null;
 517                         backward = null;
 518                         return true;
 519                 }
 520                 #endregion
 521
 522                 public bool HasAllBottomFields (SymValue sv)
 523                 {
 524                         if (sv == null)
 525                                 return false;
 526
 527                         return this [sv].HasAllBottomFields;
 528                 }
 529
 530                 public SymValue LookupOrManifest (TFunc function, SymValue arg, out bool fresh)
 531                 {
 532                         int oldCnt = IdGenerator;
 533                         SymValue result = this [function, arg];
 534
 535                         fresh = oldCnt < IdGenerator;
 536                         return result;
 537                 }
 538
 539                 public SymValue TryLookup (TFunc function, params SymValue[] args)
 540                 {
 541                         if (args.Length == 0 || args.Length == 1)
 542                                 return LookupWithoutManifesting (this.const_root, function);
 543                         return LookupWithoutManifesting (args, function);
 544                 }
 545
 546                 public SymValue LookupWithoutManifesting (SymValue sv, TFunc function)
 547                 {
 548                         if (sv == null)
 549                                 return null;
 550                         sv = Find (sv);
 551                         SymValue result = TermMap [sv, function];
 552
 553                         if (result == null)
 554                                 return null;
 555                         return Find (result);
 556                 }
 557
 558                 public SymValue LookupWithoutManifesting (SymValue[] args, TFunc function)
 559                 {
 560                         int length = args.Length;
 561                         for (int i = 0; i < length; i++)
 562                                 args [i] = Find (args [i]);
 563                         return FindCandidate (args, function);
 564                 }
 565
 566                 public SymValue LookupOrBottomPlaceHolder (SymValue arg, TFunc function, out bool isPlaceHolder)
 567                 {
 568                         SymValue result = LookupWithoutManifesting (arg, function);
 569
 570                         isPlaceHolder = result == null;
 571                         return isPlaceHolder ? this.BottomPlaceHolder : result;
 572                 }
 573
 574                 private SymValue Find (SymValue v)
 575                 {
 576                         SymValue forw = this.forw_map [v];
 577                         if (forw == null)
 578                                 return v;
 579
 580                         return Find (forw);
 581                 }
 582
 583                 private bool IsOldSymbol (SymValue sv)
 584                 {
 585                         if (this.Parent == null)
 586                                 return false;
 587                         return sv.UniqueId <= this.Parent.LastSymbolId;
 588                 }
 589
 590                 private SymValue FindCandidate (SymValue[] args, TFunc function)
 591                 {
 592                         int length = args.Length;
 593                         var multiEdge = new MultiEdge<TFunc, TADomain> (function, 0, length);
 594                         for (LispList<SymValue> list = MultiEdgeMap [args [0], multiEdge]; list != null; list = list.Tail) {
 595                                 SymGraphTerm<TFunc> term = EqualMultiTermsMap [list.Head];
 596                                 if (term.Args.Length == length) {
 597                                         bool found = true;
 598
 599                                         for (int i = 0; i < length; ++i) {
 600                                                 if (Find (term.Args [i]) != args [i]) {
 601                                                         found = false;
 602                                                         break;
 603                                                 }
 604                                         }
 605
 606                                         if (found)
 607                                                 return list.Head;
 608                                 }
 609                         }
 610                         return null;
 611                 }
 612
 613                 private bool TryPushEquality (WorkList<EqualityPair<TFunc, TADomain>> workList, SymValue sv1, SymValue sv2)
 614                 {
 615                         if (sv1 != sv2) {
 616                                 workList.Add (new EqualityPair<TFunc, TADomain> (sv1, sv2));
 617                                 return true;
 618                         }
 619
 620                         return false;
 621                 }
 622
 623                 private void DrainEqualityWorkList (WorkList<EqualityPair<TFunc, TADomain>> workList)
 624                 {
 625                         while (!workList.IsEmpty ()) {
 626                                 EqualityPair<TFunc, TADomain> equalityPair = workList.Pull ();
 627                                 SymValue sv1 = Find (equalityPair.Sv1);
 628                                 SymValue sv2 = Find (equalityPair.Sv2);
 629                                 if (sv1 != sv2) {
 630                                         if (sv1.UniqueId < sv2.UniqueId) {
 631                                                 SymValue tmp = sv1;
 632                                                 sv1 = sv2;
 633                                                 sv2 = tmp;
 634                                         }
 635
 636                                         foreach (TFunc function in Functions (sv1)) {
 637                                                 SymValue v2 = LookupWithoutManifesting (sv2, function);
 638                                                 if (v2 == null)
 639                                                         this [sv2, function] = this [sv1, function];
 640                                                 else
 641                                                         TryPushEquality (workList, this [sv1, function], v2);
 642                                         }
 643                                         TADomain thisValue = this [sv1];
 644                                         TADomain thatValue = this [sv2];
 645                                         foreach (var elem in EqualTermsMap [sv1].AsEnumerable ())
 646                                                 EqualTermsMap = EqualTermsMap.Add (sv2, EqualTermsMap [sv2].Cons (elem));
 647
 648                                         this.forw_map = this.forw_map.Add (sv1, sv2);
 649                                         this [sv2] = thisValue.Meet (thatValue);
 650                                 }
 651                         }
 652                 }
 653
 654                 private IEnumerable<MultiEdge<TFunc, TADomain>> MultiEdges (SymValue sv)
 655                 {
 656                         return MultiEdgeMap.Keys2 (Find (sv));
 657                 }
 658
 659                 public IEnumerable<SymGraphTerm<TFunc>> EqMultiTerms (SymValue sv)
 660                 {
 661                         SymGraphTerm<TFunc> term = EqualMultiTermsMap [sv];
 662                         if (term.Args != null && IsValidMultiTerm (term))
 663                                 yield return term;
 664                 }
 665
 666                 public bool IsValidSymbol (SymValue sv)
 667                 {
 668                         return EqualTermsMap.ContainsKey (sv);
 669                 }
 670
 671                 private bool IsValidMultiTerm (SymGraphTerm<TFunc> term)
 672                 {
 673                         return LookupWithoutManifesting (term.Args, term.Function) != null;
 674                 }
 675
 676                 private static SymGraph<TFunc, TADomain> ComputeCommonTail (SymGraph<TFunc, TADomain> g1, SymGraph<TFunc, TADomain> g2, out int updateSize)
 677                 {
 678                         SymGraph<TFunc, TADomain> graph1 = g1;
 679                         SymGraph<TFunc, TADomain> graph2 = g2;
 680                         while (graph1 != graph2) {
 681                                 if (graph1 == null)
 682                                         break;
 683                                 if (graph2 == null) {
 684                                         graph1 = null;
 685                                         break;
 686                                 }
 687                                 if (graph1.history_size > graph2.history_size)
 688                                         graph1 = graph1.Parent;
 689                                 else if (graph2.history_size > graph1.history_size)
 690                                         graph2 = graph2.Parent;
 691                                 else {
 692                                         graph1 = graph1.Parent;
 693                                         graph2 = graph2.Parent;
 694                                 }
 695                         }
 696                         SymGraph<TFunc, TADomain> tail = graph1;
 697                         int historySize = tail != null ? tail.history_size : 0;
 698                         updateSize = g1.history_size + g2.history_size - 2*historySize;
 699                         return tail;
 700                 }
 701
 702                 private static bool InternalLessEqual (SymGraph<TFunc, TADomain> thisG, SymGraph<TFunc, TADomain> thatG,
 703                                                        out IImmutableMap<SymValue, LispList<SymValue>> forward,
 704                                                        out IImmutableMap<SymValue, SymValue> backward)
 705                 {
 706                         int updateSize;
 707                         SymGraph<TFunc, TADomain> commonTail = ComputeCommonTail (thisG, thatG, out updateSize);
 708                         if (thisG.IsImmutable)
 709                                 thisG = thisG.Clone ();
 710
 711                         var workList = new WorkList<EqualityPair<TFunc, TADomain>> ();
 712                         workList.Add (new EqualityPair<TFunc, TADomain> (thisG.const_root, thatG.const_root));
 713                         IImmutableSet<SymValue> backwardManifested = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
 714                         IImmutableMap<SymValue, SymValue> backwardMap = ImmutableIntKeyMap<SymValue, SymValue>.Empty (SymValue.GetUniqueKey);
 715                         IImmutableMap<SymValue, LispList<SymValue>> forwardMap = ImmutableIntKeyMap<SymValue, LispList<SymValue>>.Empty (SymValue.GetUniqueKey);
 716                         IImmutableMap<SymValue, int> triggers = ImmutableIntKeyMap<SymValue, int>.Empty (SymValue.GetUniqueKey);
 717
 718                         while (!workList.IsEmpty ()) {
 719                                 EqualityPair<TFunc, TADomain> equalityPair = workList.Pull ();
 720                                 SymValue sv1 = equalityPair.Sv1;
 721                                 SymValue sv2 = equalityPair.Sv2;
 722
 723                                 SymValue s;
 724                                 if (VisitedBefore (sv2, backwardManifested, backwardMap, out s)) {
 725                                         if (s != null && s == sv1)
 726                                                 continue;
 727
 728                                         if (DebugOptions.Debug)
 729                                                 Console.WriteLine ("---LessEqual fails due to pre-existing relation: {0} <- {1}", s, sv2);
 730                                         forward = null;
 731                                         backward = null;
 732                                         return false;
 733                                 }
 734
 735                                 TADomain val1 = sv1 == null ? thisG.UnderlyingTopValue.ForManifestedField () : thisG [sv1];
 736                                 TADomain val2 = thatG [sv2];
 737                                 if (!val1.LessEqual (val2)) {
 738                                         if (DebugOptions.Debug)
 739                                                 Console.WriteLine ("---LessEqual fails due to abstract values: !({0} <= {1})", val1, val2);
 740                                         forward = null;
 741                                         backward = null;
 742                                         return false;
 743                                 }
 744                                 if (sv1 != null) {
 745                                         backwardMap = backwardMap.Add (sv2, sv1);
 746                                         forwardMap = forwardMap.Add (sv1, forwardMap [sv1].Cons (sv2));
 747                                 } else
 748                                         backwardManifested = backwardManifested.Add (sv2);
 749                                 if (thisG.HasAllBottomFields (sv1))
 750                                         continue;
 751                                 if (thatG.HasAllBottomFields (sv2)) {
 752                                         if (DebugOptions.Debug)
 753                                         {
 754                                                 Console.WriteLine ("---LessEqual fails due to bottom field difference");
 755                                         }
 756                                         forward = null;
 757                                         backward = null;
 758                                         return false;
 759                                 }
 760
 761                                 foreach (TFunc function in thatG.Functions (sv2)) {
 762                                         SymValue v1 = thisG [function, sv1];
 763                                         SymValue v2 = thatG [function, sv2];
 764                                         if (DebugOptions.Debug)
 765                                                 Console.WriteLine ("    {0}-{1}->{2} <=? {3}-{4}->{5}", sv1, function, v1, sv2, function, v2);
 766                                         workList.Add (new EqualityPair<TFunc, TADomain> (v1, v2));
 767                                 }
 768
 769                                 foreach (var e in thatG.MultiEdges (sv2)) {
 770                                         foreach (SymValue sv in thatG.MultiEdgeMap [sv2, e].AsEnumerable ()) {
 771                                                 if (!UpdateTrigger (sv, e, ref triggers))
 772                                                         continue;
 773
 774                                                 SymGraphTerm<TFunc> term = thatG.EqualMultiTermsMap [sv];
 775                                                 var args = new SymValue[term.Args.Length];
 776                                                 for (int i = 0; i < args.Length; i++)
 777                                                         args [i] = backwardMap [term.Args [i]];
 778
 779                                                 SymValue v1 = thisG.LookupWithoutManifesting (args, e.Function);
 780                                                 if (v1 == null) {
 781                                                         if (DebugOptions.Debug)
 782                                                                 Console.WriteLine ("---LessEqual fails due to missing multi term {0}({1})",
 783                                                                                    e.Function,
 784                                                                                    string.Join (", ", term.Args.Select (it => it.ToString ())));
 785                                                         forward = null;
 786                                                         backward = null;
 787                                                         return false;
 788                                                 }
 789
 790                                                 workList.Add (new EqualityPair<TFunc, TADomain> (v1, sv));
 791                                         }
 792                                 }
 793                         }
 794                         forward = forwardMap;
 795                         backward = CompleteWithCommon (backwardMap, thisG, commonTail.IdGenerator);
 796                         return true;
 797                 }
 798
 799                 private static IImmutableMap<SymValue, SymValue> CompleteWithCommon (IImmutableMap<SymValue, SymValue> map,
 800                                                                                      SymGraph<TFunc, TADomain> thisGraph, int lastCommonId)
 801                 {
 802                         IEnumerable<SymValue> symValues = thisGraph.EqualTermsMap.Keys.Concat (thisGraph.EqualMultiTermsMap.Keys);
 803                         foreach (SymValue sv in symValues) {
 804                                 if (IsCommon (sv, lastCommonId) && !map.ContainsKey (sv))
 805                                         map = map.Add (sv, sv);
 806                         }
 807                         return map;
 808                 }
 809
 810                 private static bool IsCommon (SymValue sv, int lastCommonId)
 811                 {
 812                         return sv.UniqueId <= lastCommonId;
 813                 }
 814
 815                 private static bool UpdateTrigger (SymValue sv, MultiEdge<TFunc, TADomain> edge, ref IImmutableMap<SymValue, int> triggers)
 816                 {
 817                         int val = triggers [sv] + 1;
 818                         triggers = triggers.Add (sv, val);
 819                         return (val == edge.Arity);
 820                 }
 821
 822                 private static bool VisitedBefore (SymValue sv2,
 823                                                    IImmutableSet<SymValue> backwardManifested,
 824                                                    IImmutableMap<SymValue, SymValue> backward,
 825                                                    out SymValue sv1)
 826                 {
 827                         sv1 = backward [sv2];
 828                         return sv1 != null || backwardManifested.Contains (sv2);
 829                 }
 830
 831                 private bool IsSameEGraph (SymGraph<TFunc, TADomain> that)
 832                 {
 833                         if (this == that)
 834                                 return true;
 835                         if (that.Parent == this)
 836                                 return that.Updates == Updates;
 837
 838                         return false;
 839                 }
 840
 841                 private void MarkAsImmutable ()
 842                 {
 843                         this.is_immutable = true;
 844                 }
 845
 846                 #region Merge updates
 847                 private void AddUpdate (Update<TFunc, TADomain> update)
 848                 {
 849                         Updates = Updates.Cons (update);
 850                 }
 851
 852                 private void AddAbstractValueUpdate (SymValue sv)
 853                 {
 854                         if (!IsOldSymbol (sv))
 855                                 return;
 856                         AddUpdate (new AbstractDomainUpdate<TFunc, TADomain> (sv));
 857                 }
 858
 859                 private void AddEqualityUpdate (SymValue sv1, SymValue sv2)
 860                 {
 861                         if (!IsOldSymbol (sv1) || !IsOldSymbol (sv2))
 862                                 return;
 863                         AddUpdate (new EqualityUpdate<TFunc, TADomain> (sv1, sv2));
 864                 }
 865
 866                 private void AddEdgeUpdate (SymValue from, TFunc function)
 867                 {
 868                         if (!IsOldSymbol (from))
 869                                 return;
 870                         AddUpdate (new EdgeUpdate<TFunc, TADomain> (from, function));
 871                 }
 872
 873                 private void AddEliminateAllUpdate (SymValue from)
 874                 {
 875                         if (!IsOldSymbol (from))
 876                                 return;
 877                         foreach (TFunc function in TermMap.Keys2 (from))
 878                                 AddUpdate (new EliminateEdgeUpdate<TFunc, TADomain> (from, function));
 879                 }
 880
 881                 private void AddEliminateEdgeUpdate (SymValue from, TFunc function)
 882                 {
 883                         if (!IsOldSymbol (from))
 884                                 return;
 885                         AddUpdate (new EliminateEdgeUpdate<TFunc, TADomain> (from, function));
 886                 }
 887
 888                 private void AddMultiEdgeUpdate (SymValue[] from, TFunc function)
 889                 {
 890                         for (int i = 0; i < from.Length; i++) {
 891                                 if (!IsOldSymbol (from [i]))
 892                                         return;
 893                         }
 894
 895                         AddUpdate (new MultiEdgeUpdate<TFunc, TADomain> (from, function));
 896                 }
 897                 #endregion
 898
 899                 public IImmutableMap<SymValue, LispList<SymValue>> GetForwardIdentityMap ()
 900                 {
 901                         var res = ImmutableIntKeyMap<SymValue, LispList<SymValue>>.Empty (SymValue.GetUniqueKey);
 902                         foreach (var sv in this.EqualTermsMap.Keys.Union (this.EqualMultiTermsMap.Keys)) {
 903                                 res = res.Add (sv, LispList<SymValue>.Cons (sv, null));
 904                         }
 905                         return res;
 906                 }
 907         }
 908 }