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>, Sequence<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, Sequence<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, Sequence<SymGraphTerm<TFunc>>> EqualTermsMap { get; private set; }
 113                 public DoubleImmutableMap<SymValue, MultiEdge<TFunc, TADomain>, Sequence<SymValue>> MultiEdgeMap { get; private set; }
 114                 public DoubleImmutableMap<SymValue, TFunc, SymValue> TermMap { get; private set; }
 115                 public int IdGenerator { get; private set; }
 116                 public Sequence<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                                         Sequence<SymValue> list = MultiEdgeMap [args [i], edge];
 168                                         if (isTermEqual && !Sequence<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, Sequence<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                                 Sequence<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)
 380             {
 381                 throw new NotImplementedException();
 382             }
 383
 384             public SymGraph<TFunc, TADomain> Join (SymGraph<TFunc, TADomain> that, bool widening, out bool weaker)
 385                 {
 386                         IMergeInfo info;
 387                         SymGraph<TFunc, TADomain> join = Join (that, out info, widening);
 388                         weaker = info.Changed;
 389                         return join;
 390                 }
 391
 392             public SymGraph<TFunc, TADomain> Widen(SymGraph<TFunc, TADomain> that)
 393             {
 394                 throw new NotImplementedException();
 395             }
 396
 397             public SymGraph<TFunc, TADomain> Join (SymGraph<TFunc, TADomain> that, out IMergeInfo mergeInfo, bool widen)
 398                 {
 399                         SymGraph<TFunc, TADomain> egraph = this;
 400                         int updateSize;
 401                         SymGraph<TFunc, TADomain> commonTail = ComputeCommonTail (egraph, that, out updateSize);
 402                 bool hasCommonTail = commonTail != null;
 403
 404                 bool doingIncrementalJoin = hasCommonTail & commonTail != egraph.root_graph & !widen & DoIncrementalJoin;
 405
 406                         //debug
 407
 408                         if (DebugOptions.Debug)
 409                         {
 410                                 Console.WriteLine ("SymGraph {0}", widen ? "widen" : "join");
 411                                 if (commonTail != null)
 412                                         Console.WriteLine ("Last common symbol: {0}", commonTail.LastSymbolId);
 413
 414                                 Console.WriteLine ("  Doing {0}", doingIncrementalJoin ? "incremental join" : "full join");
 415                         }
 416
 417                         SymGraph<TFunc, TADomain> result;
 418                         MergeInfo<TFunc, TADomain> mergeState;
 419                         if (doingIncrementalJoin) {
 420                                 result = new SymGraph<TFunc, TADomain> (commonTail);
 421                                 mergeState = new MergeInfo<TFunc, TADomain> (result, egraph, that, widen);
 422                                 mergeState.Replay (commonTail);
 423                                 mergeState.Commit ();
 424                         } else {
 425                                 result = new SymGraph<TFunc, TADomain> (commonTail);
 426                                 mergeState = new MergeInfo<TFunc, TADomain> (result, egraph, that, widen);
 427                                 mergeState.ReplayEliminations (commonTail);
 428                                 mergeState.AddMapping (egraph.const_root, that.const_root, result.const_root);
 429                                 mergeState.JoinSymbolicValue (egraph.const_root, that.const_root, result.const_root);
 430                                 mergeState.Commit ();
 431                         }
 432                         mergeInfo = mergeState;
 433
 434                         if (DebugOptions.Debug)
 435                         {
 436                                 Console.WriteLine ("  Result update size {0}", result.Updates.Length ());
 437                                 Console.WriteLine ("Done with Egraph join: changed = {0}", mergeInfo.Changed ? 1 : 0);
 438                         }
 439
 440                         return result;
 441                 }
 442
 443                 public void Dump (TextWriter tw)
 444                 {
 445                         var set = new HashSet<SymValue> ();
 446                         var workList = new WorkList<SymValue> ();
 447                         IImmutableMap<SymValue, int> triggers = ImmutableIntKeyMap<SymValue, int>.Empty (SymValue.GetUniqueKey);
 448                         tw.WriteLine ("EGraphId: {0}", this.egraph_id);
 449                         tw.WriteLine ("LastSymbolId: {0}", LastSymbolId);
 450
 451                         foreach (TFunc function in TermMap.Keys2 (this.const_root)) {
 452                                 SymValue sv = this [this.const_root, function];
 453                                 tw.WriteLine ("{0} = {1}", function, sv);
 454                                 workList.Add (sv);
 455                         }
 456
 457                         while (!workList.IsEmpty ()) {
 458                                 SymValue sv = workList.Pull ();
 459                                 if (!set.Add (sv))
 460                                         continue;
 461
 462                                 foreach (TFunc function in TermMap.Keys2 (sv)) {
 463                                         SymValue target = this [sv, function];
 464
 465                                         tw.WriteLine ("{0}({2}) = {1})", function, target, sv);
 466                                         workList.Add (target);
 467                                 }
 468                                 foreach (var edge in MultiEdgeMap.Keys2 (sv)) {
 469                                         foreach (SymValue target in MultiEdgeMap [sv, edge].AsEnumerable ()) {
 470                                                 if (!UpdateTrigger (target, edge, ref triggers))
 471                                                         continue;
 472                                                 SymGraphTerm<TFunc> term = EqualMultiTermsMap [target];
 473                                                 if (term.Args != null) {
 474                                                         tw.WriteLine ("{0}({1}) = {2}",
 475                                                                       term.Function,
 476                                                                       term.Args.ToString (", "), target);
 477                                                         workList.Add (target);
 478                                                 }
 479                                         }
 480                                 }
 481                         }
 482
 483                         tw.WriteLine ("**Abstract value map");
 484                         foreach (SymValue sv in set) {
 485                                 TADomain abstractValue = this [sv];
 486                                 if (!abstractValue.IsTop)
 487                                         tw.WriteLine ("{0} -> {1}", sv, abstractValue);
 488                         }
 489                 }
 490                 #endregion
 491
 492                 #region Implementation of IAbstractDomain<SymGraph<Constant,AbstractValue>>
 493                 public SymGraph<TFunc, TADomain> Meet (SymGraph<TFunc, TADomain> that)
 494                 {
 495                         if (this == that || IsBottom || that.IsTop)
 496                                 return this;
 497                         if (that.IsBottom || IsTop)
 498                                 return that;
 499
 500                         return this;
 501                 }
 502
 503                 public bool LessEqual (SymGraph<TFunc, TADomain> that)
 504                 {
 505                         IImmutableMap<SymValue, Sequence<SymValue>> forwardMap;
 506                         IImmutableMap<SymValue, SymValue> backwardMap;
 507
 508                         return LessEqual (that, out forwardMap, out backwardMap);
 509                 }
 510
 511                 public SymGraph<TFunc, TADomain> ImmutableVersion ()
 512                 {
 513                         MarkAsImmutable ();
 514                         return this;
 515                 }
 516
 517                 public bool LessEqual (SymGraph<TFunc, TADomain> that,
 518                         out IImmutableMap<SymValue, Sequence<SymValue>> forward,
 519                         out IImmutableMap<SymValue, SymValue> backward)
 520                 {
 521                         if (!IsSameEGraph (that))
 522                                 return InternalLessEqual (this, that, out forward, out backward);
 523
 524                         forward = null;
 525                         backward = null;
 526                         return true;
 527                 }
 528                 #endregion
 529
 530                 public bool HasAllBottomFields (SymValue sv)
 531                 {
 532                         if (sv == null)
 533                                 return false;
 534
 535                         return this [sv].HasAllBottomFields;
 536                 }
 537
 538                 public SymValue LookupOrManifest (TFunc function, SymValue arg, out bool fresh)
 539                 {
 540                         int oldCnt = IdGenerator;
 541                         SymValue result = this [function, arg];
 542
 543                         fresh = oldCnt < IdGenerator;
 544                         return result;
 545                 }
 546
 547                 public SymValue TryLookup (TFunc function, params SymValue[] args)
 548                 {
 549                         if (args.Length == 0 || args.Length == 1)
 550                                 return LookupWithoutManifesting (this.const_root, function);
 551                         return LookupWithoutManifesting (args, function);
 552                 }
 553
 554                 public SymValue LookupWithoutManifesting (SymValue sv, TFunc function)
 555                 {
 556                         if (sv == null)
 557                                 return null;
 558                         sv = Find (sv);
 559                         SymValue result = TermMap [sv, function];
 560
 561                         if (result == null)
 562                                 return null;
 563                         return Find (result);
 564                 }
 565
 566                 public SymValue LookupWithoutManifesting (SymValue[] args, TFunc function)
 567                 {
 568                         int length = args.Length;
 569                         for (int i = 0; i < length; i++)
 570                                 args [i] = Find (args [i]);
 571                         return FindCandidate (args, function);
 572                 }
 573
 574                 public SymValue LookupOrBottomPlaceHolder (SymValue arg, TFunc function, out bool isPlaceHolder)
 575                 {
 576                         SymValue result = LookupWithoutManifesting (arg, function);
 577
 578                         isPlaceHolder = result == null;
 579                         return isPlaceHolder ? this.BottomPlaceHolder : result;
 580                 }
 581
 582                 private SymValue Find (SymValue v)
 583                 {
 584                         SymValue forw = this.forw_map [v];
 585                         if (forw == null)
 586                                 return v;
 587
 588                         return Find (forw);
 589                 }
 590
 591                 private bool IsOldSymbol (SymValue sv)
 592                 {
 593                         if (this.Parent == null)
 594                                 return false;
 595                         return sv.UniqueId <= this.Parent.LastSymbolId;
 596                 }
 597
 598                 private SymValue FindCandidate (SymValue[] args, TFunc function)
 599                 {
 600                         int length = args.Length;
 601                         var multiEdge = new MultiEdge<TFunc, TADomain> (function, 0, length);
 602                         for (Sequence<SymValue> list = MultiEdgeMap [args [0], multiEdge]; list != null; list = list.Tail) {
 603                                 SymGraphTerm<TFunc> term = EqualMultiTermsMap [list.Head];
 604                                 if (term.Args.Length == length) {
 605                                         bool found = true;
 606
 607                                         for (int i = 0; i < length; ++i) {
 608                                                 if (Find (term.Args [i]) != args [i]) {
 609                                                         found = false;
 610                                                         break;
 611                                                 }
 612                                         }
 613
 614                                         if (found)
 615                                                 return list.Head;
 616                                 }
 617                         }
 618                         return null;
 619                 }
 620
 621                 private bool TryPushEquality (WorkList<EqualityPair<TFunc, TADomain>> workList, SymValue sv1, SymValue sv2)
 622                 {
 623                         if (sv1 != sv2) {
 624                                 workList.Add (new EqualityPair<TFunc, TADomain> (sv1, sv2));
 625                                 return true;
 626                         }
 627
 628                         return false;
 629                 }
 630
 631                 private void DrainEqualityWorkList (WorkList<EqualityPair<TFunc, TADomain>> workList)
 632                 {
 633                         while (!workList.IsEmpty ()) {
 634                                 EqualityPair<TFunc, TADomain> equalityPair = workList.Pull ();
 635                                 SymValue sv1 = Find (equalityPair.Sv1);
 636                                 SymValue sv2 = Find (equalityPair.Sv2);
 637                                 if (sv1 != sv2) {
 638                                         if (sv1.UniqueId < sv2.UniqueId) {
 639                                                 SymValue tmp = sv1;
 640                                                 sv1 = sv2;
 641                                                 sv2 = tmp;
 642                                         }
 643
 644                                         foreach (TFunc function in Functions (sv1)) {
 645                                                 SymValue v2 = LookupWithoutManifesting (sv2, function);
 646                                                 if (v2 == null)
 647                                                         this [sv2, function] = this [sv1, function];
 648                                                 else
 649                                                         TryPushEquality (workList, this [sv1, function], v2);
 650                                         }
 651                                         TADomain thisValue = this [sv1];
 652                                         TADomain thatValue = this [sv2];
 653                                         foreach (var elem in EqualTermsMap [sv1].AsEnumerable ())
 654                                                 EqualTermsMap = EqualTermsMap.Add (sv2, EqualTermsMap [sv2].Cons (elem));
 655
 656                                         this.forw_map = this.forw_map.Add (sv1, sv2);
 657                                         this [sv2] = thisValue.Meet (thatValue);
 658                                 }
 659                         }
 660                 }
 661
 662                 private IEnumerable<MultiEdge<TFunc, TADomain>> MultiEdges (SymValue sv)
 663                 {
 664                         return MultiEdgeMap.Keys2 (Find (sv));
 665                 }
 666
 667                 public IEnumerable<SymGraphTerm<TFunc>> EqMultiTerms (SymValue sv)
 668                 {
 669                         SymGraphTerm<TFunc> term = EqualMultiTermsMap [sv];
 670                         if (term.Args != null && IsValidMultiTerm (term))
 671                                 yield return term;
 672                 }
 673
 674                 public bool IsValidSymbol (SymValue sv)
 675                 {
 676                         return EqualTermsMap.ContainsKey (sv);
 677                 }
 678
 679                 private bool IsValidMultiTerm (SymGraphTerm<TFunc> term)
 680                 {
 681                         return LookupWithoutManifesting (term.Args, term.Function) != null;
 682                 }
 683
 684                 private static SymGraph<TFunc, TADomain> ComputeCommonTail (SymGraph<TFunc, TADomain> g1, SymGraph<TFunc, TADomain> g2, out int updateSize)
 685                 {
 686                         SymGraph<TFunc, TADomain> graph1 = g1;
 687                         SymGraph<TFunc, TADomain> graph2 = g2;
 688                         while (graph1 != graph2) {
 689                                 if (graph1 == null)
 690                                         break;
 691                                 if (graph2 == null) {
 692                                         graph1 = null;
 693                                         break;
 694                                 }
 695                                 if (graph1.history_size > graph2.history_size)
 696                                         graph1 = graph1.Parent;
 697                                 else if (graph2.history_size > graph1.history_size)
 698                                         graph2 = graph2.Parent;
 699                                 else {
 700                                         graph1 = graph1.Parent;
 701                                         graph2 = graph2.Parent;
 702                                 }
 703                         }
 704                         SymGraph<TFunc, TADomain> tail = graph1;
 705                         int historySize = tail != null ? tail.history_size : 0;
 706                         updateSize = g1.history_size + g2.history_size - 2*historySize;
 707                         return tail;
 708                 }
 709
 710                 private static bool InternalLessEqual (SymGraph<TFunc, TADomain> thisG, SymGraph<TFunc, TADomain> thatG,
 711                                                        out IImmutableMap<SymValue, Sequence<SymValue>> forward,
 712                                                        out IImmutableMap<SymValue, SymValue> backward)
 713                 {
 714                         int updateSize;
 715                         SymGraph<TFunc, TADomain> commonTail = ComputeCommonTail (thisG, thatG, out updateSize);
 716                         if (thisG.IsImmutable)
 717                                 thisG = thisG.Clone ();
 718
 719                         var workList = new WorkList<EqualityPair<TFunc, TADomain>> ();
 720                         workList.Add (new EqualityPair<TFunc, TADomain> (thisG.const_root, thatG.const_root));
 721                         IImmutableSet<SymValue> backwardManifested = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
 722                         IImmutableMap<SymValue, SymValue> backwardMap = ImmutableIntKeyMap<SymValue, SymValue>.Empty (SymValue.GetUniqueKey);
 723                         IImmutableMap<SymValue, Sequence<SymValue>> forwardMap = ImmutableIntKeyMap<SymValue, Sequence<SymValue>>.Empty (SymValue.GetUniqueKey);
 724                         IImmutableMap<SymValue, int> triggers = ImmutableIntKeyMap<SymValue, int>.Empty (SymValue.GetUniqueKey);
 725
 726                         while (!workList.IsEmpty ()) {
 727                                 EqualityPair<TFunc, TADomain> equalityPair = workList.Pull ();
 728                                 SymValue sv1 = equalityPair.Sv1;
 729                                 SymValue sv2 = equalityPair.Sv2;
 730
 731                                 SymValue s;
 732                                 if (VisitedBefore (sv2, backwardManifested, backwardMap, out s)) {
 733                                         if (s != null && s == sv1)
 734                                                 continue;
 735
 736                                         if (DebugOptions.Debug)
 737                                                 Console.WriteLine ("---LessEqual fails due to pre-existing relation: {0} <- {1}", s, sv2);
 738                                         forward = null;
 739                                         backward = null;
 740                                         return false;
 741                                 }
 742
 743                                 TADomain val1 = sv1 == null ? thisG.UnderlyingTopValue.ForManifestedField () : thisG [sv1];
 744                                 TADomain val2 = thatG [sv2];
 745                                 if (!val1.LessEqual (val2)) {
 746                                         if (DebugOptions.Debug)
 747                                                 Console.WriteLine ("---LessEqual fails due to abstract values: !({0} <= {1})", val1, val2);
 748                                         forward = null;
 749                                         backward = null;
 750                                         return false;
 751                                 }
 752                                 if (sv1 != null) {
 753                                         backwardMap = backwardMap.Add (sv2, sv1);
 754                                         forwardMap = forwardMap.Add (sv1, forwardMap [sv1].Cons (sv2));
 755                                 } else
 756                                         backwardManifested = backwardManifested.Add (sv2);
 757                                 if (thisG.HasAllBottomFields (sv1))
 758                                         continue;
 759                                 if (thatG.HasAllBottomFields (sv2)) {
 760                                         if (DebugOptions.Debug)
 761                                         {
 762                                                 Console.WriteLine ("---LessEqual fails due to bottom field difference");
 763                                         }
 764                                         forward = null;
 765                                         backward = null;
 766                                         return false;
 767                                 }
 768
 769                                 foreach (TFunc function in thatG.Functions (sv2)) {
 770                                         SymValue v1 = thisG [function, sv1];
 771                                         SymValue v2 = thatG [function, sv2];
 772                                         if (DebugOptions.Debug)
 773                                                 Console.WriteLine ("    {0}-{1}->{2} <=? {3}-{4}->{5}", sv1, function, v1, sv2, function, v2);
 774                                         workList.Add (new EqualityPair<TFunc, TADomain> (v1, v2));
 775                                 }
 776
 777                                 foreach (var e in thatG.MultiEdges (sv2)) {
 778                                         foreach (SymValue sv in thatG.MultiEdgeMap [sv2, e].AsEnumerable ()) {
 779                                                 if (!UpdateTrigger (sv, e, ref triggers))
 780                                                         continue;
 781
 782                                                 SymGraphTerm<TFunc> term = thatG.EqualMultiTermsMap [sv];
 783                                                 var args = new SymValue[term.Args.Length];
 784                                                 for (int i = 0; i < args.Length; i++)
 785                                                         args [i] = backwardMap [term.Args [i]];
 786
 787                                                 SymValue v1 = thisG.LookupWithoutManifesting (args, e.Function);
 788                                                 if (v1 == null) {
 789                                                         if (DebugOptions.Debug)
 790                                                                 Console.WriteLine ("---LessEqual fails due to missing multi term {0}({1})",
 791                                                                                    e.Function,
 792                                                                                    string.Join (", ", term.Args.Select (it => it.ToString ())));
 793                                                         forward = null;
 794                                                         backward = null;
 795                                                         return false;
 796                                                 }
 797
 798                                                 workList.Add (new EqualityPair<TFunc, TADomain> (v1, sv));
 799                                         }
 800                                 }
 801                         }
 802                         forward = forwardMap;
 803                         backward = CompleteWithCommon (backwardMap, thisG, commonTail.IdGenerator);
 804                         return true;
 805                 }
 806
 807                 private static IImmutableMap<SymValue, SymValue> CompleteWithCommon (IImmutableMap<SymValue, SymValue> map,
 808                                                                                      SymGraph<TFunc, TADomain> thisGraph, int lastCommonId)
 809                 {
 810                         IEnumerable<SymValue> symValues = thisGraph.EqualTermsMap.Keys.Concat (thisGraph.EqualMultiTermsMap.Keys);
 811                         foreach (SymValue sv in symValues) {
 812                                 if (IsCommon (sv, lastCommonId) && !map.ContainsKey (sv))
 813                                         map = map.Add (sv, sv);
 814                         }
 815                         return map;
 816                 }
 817
 818                 private static bool IsCommon (SymValue sv, int lastCommonId)
 819                 {
 820                         return sv.UniqueId <= lastCommonId;
 821                 }
 822
 823                 private static bool UpdateTrigger (SymValue sv, MultiEdge<TFunc, TADomain> edge, ref IImmutableMap<SymValue, int> triggers)
 824                 {
 825                         int val = triggers [sv] + 1;
 826                         triggers = triggers.Add (sv, val);
 827                         return (val == edge.Arity);
 828                 }
 829
 830                 private static bool VisitedBefore (SymValue sv2,
 831                                                    IImmutableSet<SymValue> backwardManifested,
 832                                                    IImmutableMap<SymValue, SymValue> backward,
 833                                                    out SymValue sv1)
 834                 {
 835                         sv1 = backward [sv2];
 836                         return sv1 != null || backwardManifested.Contains (sv2);
 837                 }
 838
 839                 private bool IsSameEGraph (SymGraph<TFunc, TADomain> that)
 840                 {
 841                         if (this == that)
 842                                 return true;
 843                         if (that.Parent == this)
 844                                 return that.Updates == Updates;
 845
 846                         return false;
 847                 }
 848
 849                 private void MarkAsImmutable ()
 850                 {
 851                         this.is_immutable = true;
 852                 }
 853
 854                 #region Merge updates
 855                 private void AddUpdate (Update<TFunc, TADomain> update)
 856                 {
 857                         Updates = Updates.Cons (update);
 858                 }
 859
 860                 private void AddAbstractValueUpdate (SymValue sv)
 861                 {
 862                         if (!IsOldSymbol (sv))
 863                                 return;
 864                         AddUpdate (new AbstractDomainUpdate<TFunc, TADomain> (sv));
 865                 }
 866
 867                 private void AddEqualityUpdate (SymValue sv1, SymValue sv2)
 868                 {
 869                         if (!IsOldSymbol (sv1) || !IsOldSymbol (sv2))
 870                                 return;
 871                         AddUpdate (new EqualityUpdate<TFunc, TADomain> (sv1, sv2));
 872                 }
 873
 874                 private void AddEdgeUpdate (SymValue from, TFunc function)
 875                 {
 876                         if (!IsOldSymbol (from))
 877                                 return;
 878                         AddUpdate (new EdgeUpdate<TFunc, TADomain> (from, function));
 879                 }
 880
 881                 private void AddEliminateAllUpdate (SymValue from)
 882                 {
 883                         if (!IsOldSymbol (from))
 884                                 return;
 885                         foreach (TFunc function in TermMap.Keys2 (from))
 886                                 AddUpdate (new EliminateEdgeUpdate<TFunc, TADomain> (from, function));
 887                 }
 888
 889                 private void AddEliminateEdgeUpdate (SymValue from, TFunc function)
 890                 {
 891                         if (!IsOldSymbol (from))
 892                                 return;
 893                         AddUpdate (new EliminateEdgeUpdate<TFunc, TADomain> (from, function));
 894                 }
 895
 896                 private void AddMultiEdgeUpdate (SymValue[] from, TFunc function)
 897                 {
 898                         for (int i = 0; i < from.Length; i++) {
 899                                 if (!IsOldSymbol (from [i]))
 900                                         return;
 901                         }
 902
 903                         AddUpdate (new MultiEdgeUpdate<TFunc, TADomain> (from, function));
 904                 }
 905                 #endregion
 906
 907                 public IImmutableMap<SymValue, Sequence<SymValue>> GetForwardIdentityMap ()
 908                 {
 909                         var res = ImmutableIntKeyMap<SymValue, Sequence<SymValue>>.Empty (SymValue.GetUniqueKey);
 910                         foreach (var sv in this.EqualTermsMap.Keys.Union (this.EqualMultiTermsMap.Keys)) {
 911                                 res = res.Add (sv, Sequence<SymValue>.Cons (sv, null));
 912                         }
 913                         return res;
 914                 }
 915         }
 916 }