Switching to immutable Expr classes

Nov 27, 2014 at 7:35 PM
Hi All,

I make heavy use of Boogie's Expr classes in a project I'm working on and I've discovered that I need GetHashCode() to be much faster because it's a bottleneck for me.

A possible solution for this is to make Expr node immutable so the hash code only needs to be computed once (on construction of node). This fits in perfectly with my use case but I'm not sure if it suits everyone else so this is why I've started a discussion.

If we were to transition to immutable Expr classes I would image we would do it something like this.

1 Introduce a static flag in Expr "Immutable". If enabled it can't be disabled and it forces the GetHashCode() computation to be done on construction of nodes and stores it's value in the node and returns it when GetHashCode() is called. By default this flag will be set to false so it won't break existing code but it allows me to have the fast GetHashCode() behaviour I desire.

2. Add methods to all the Expr types that allow
  • Retrieval of the number of children
  • Access to a child based on index number
  • Access to other things like triggers
  • A set of "CreateNewNodeWithChildren()" methods that are passed new children which returns a copy of the new node with the new children (the original node is left untouched). If the current children are passed in to this method it is a no-op (to prevent pointless copying).
3. Change the StandardVisitor family of classes so they use this new immutable Expr API (other program stuff like Blocks, Cmds, etc would be left alone). A disadvantage of this approach is if a node is changed deep in an Expr tree it will trigger a re-construction of all nodes on the path from that node to the root. With the current StandardVisitor classes that would not happen. The garbage collector ought to be able to handle this though.

4. Switch all code to this new "immutable" Expr style. This would require
  • making various fields of the Expr classes protected so they can't be modified by accident
  • Remove the Immutable flag as Expr are always immutable and always pre-compute the hashcode on construction (i.e. constructor or "CreateNewNodeWithChildren()).
  • Add debug statements that check that the pre-computed hash code matches the current in various methods as a sanity check.
How do people feel about this? This is a very invasive change but I feel it would be a useful one.
Nov 27, 2014 at 9:04 PM
I like the idea of immutable expressions. I'm not clear on why the methods of point (2) above are necessary, though.