Slicing

[DKLoehr]

This branch primarily implements a new transformation which I call Attribute Slicing. After we have fully simplified the network (map unrolling, tuple flattening, etc), it splits the assertion into conjuncts -- if the assertion is not a conjunction, this does nothing. Assuming the attribute is a tuple, it then runs dependency analysis to see which elements of the attribute each conjunct depends upon.

For each conjunct, it creates a "slice" of the network, which is an equivalent nv program in which the attribute only contains the elements that the conjunct depends upon. It then runs our SMT solver on each of the slices, and reports a success iff all the slices do. The hope is that this will allow us to speed up analysis of large networks with complicated attributes, by splitting them into smaller pieces which can be run in parallel.

If any slice fails, we return a model as usual. Since the slice does not necessarily have all the elements of the attribute, we fill in the remaining elements with dummy values. We also keep a "mask" value as part of the Solution.t type -- this is a Syntax.value which has the same structure as the attribute values, but whose base types have been replaced with booleans. When printing the attribute values for the user, we only display those values whose boolean in the mask is true.

Major structural changes to the code:

• Attribute slicing has been added into the pipeline when running smt classic encoding
• The type Solution.t has been extended to contain an optional mask value. All transformations must now map back the mask value as well as attribute and symbolic values.

Minor changes:

• Added a design pattern in Mutators.ml which hopefully captures the essence of many of our code transformations. It has so far only been used to implement two simple transformations; in the future I hope to update our existing transformations to use it as well.
• Pulled out several transformations which were happening at the same time as others, in order to make them more general and explicit. These are: Removing 0- and 1-element tuples (previously a part of map unrolling) Replacing units with bools (previously a part of option unboxing) ** Replacing edges with pairs of nodes (previously a part of tuple flattening)
• We can now register dependencies between command-line options -- for example, map unrolling requires inlining, so the -unroll option implies the -inline option. This makes it easier for us to tell what requirements a transformation has, and means we don't have to check lots of booleans at the site of the transformation.
• Added several end-to-end tests for the slicing transformation.
• Various bugfixes

[nickgian]

Overall looks of great use! The minor changes are very nice. Haven't looked into this too deeply but here are some questions:

1. In the (partial) evaluation, in the tget/tset cases when you cannot simplify them you create a match statement. Is this necessary? It seems a bit costly as it involves building and traversing lists and then introduces auxiliary variables in the SMT encoding (that will be thrown away by optimizations but this costs too -- I am obsessive with performance sorry!) My gut feeling is that you can very easily implement these operations in the unboxed (well in the boxed too but who cares) SMT encoding and then you don't need to create match statements. tget(lo,hi,expr) = lst <- encode[expr]; lst[lo,hi] tset(lo,hi,e1,e2) = lst1 <- encode[e1]; lst2 <- encode[e2]; ... (replace elements in the lists) Does that make sense? If that's the only reason you are doing this transformation we should definitely try to implement them in the SMT encoding. I can help with that.
2. "has been added into the pipeline when running smt classic encoding" Is there any roadblock to do the same for the functional encoding? Last time I checked it's somewhat faster especially in computing the encoding of the network, so it would be nice if we can keep it in sync.

Let me know about these, if you/we can fix them, then let's fix them and then merge, otherwise go ahead and merge.

Less important:

1. "if the assertion is not a conjunction, this does nothing." It still does the attribute slicing right?
2. "We can now register dependencies between command-line options" That's great! At some point, we should make it so that what transformations are required is computed based on the requested analyses and they are all done in one place instead of all over. That may not be entirely possible, but right now it is messy.

[DKLoehr]

My gut feeling is that you can very easily implement these operations in the unboxed (well in the boxed too but who cares) SMT encoding and then you don't need to create match statements. The TGet and TSet stuff is from a lot earlier; I just moved it to a new file. So I don't entirely remember my reasoning, but I think the only reason was so we wouldn't have to worry about TGets and TSets during SMT encoding. Having looked at the encoding (at least the unboxed one) it does seem like we could implement the operations there and have it be more efficient. I'm not totally sure how quickly I could do that, so perhaps we can create an issue and leave it for later.

Is there any roadblock to do the same for the functional encoding? I'm afraid I've been rather neglecting the functional encoding; last I heard it wasn't working very well (that was a long time ago, though). Since it seems like it's still alive, I agree that it would be good to keep it in sync -- this probably involves creating tests that use it, since all the current ones use the classic encoding.

There's no fundamental reason we can't do slicing on the functional encoding. However, if I try to run our test suite with functional encoding, I get lots of errors (I actually get significantly fewer on the slicing branch, but still a lot). I wouldn't want to mess with it until it's in a working state. After that, we would need to modify run_smt_func; it ideally wouldn't use the srp type (sticking with Syntax.network) until the very end, since slicing operates on networks. While we're at it, it seems like run_smt_func and run_smt_classic share a lot of code that could be unified.

"if the assertion is not a conjunction, this does nothing." It still does the attribute slicing right? Right.

At some point, we should make it so that what transformations are required is computed based on the requested analyses and they are all done in one place instead of all over. Even more ambitiously, it would be lovely if we could come up with a way to combine these transformations so we don't have to do as many passes over the network. Essentially a way to do the transformations lazily.

In the meantime, I agree that it would be nice to have them all in one place. Right now I think most of them are in parse_input, with a couple in the solve_smt functions. I'm liking the idea of just making a dedicated transformation function that does all of them that are required.

---

The transformation function seems straightforward, so I can probably put that together tomorrow morning. The rest seem potentially longer and not directly related to the pull request, so I think I'll merge sooner rather than later and either work on them on master or create an issue.

[nickgian]

The functional encoding won't work if you flatten tuples. You first need to create something of type SRP and then do all those transformations.

Also the functional encoding used to work, but some change seems to have broken it. On the example I tried renaming causes a crash, but I can't figure out why, other than that the code produced when converting to an SRP type seems wrong, but after three months of changes it's too hard for me to see why is that the case, especially since with the splitting of files history doesn't seem preserved so it's impossible to know what has changed.

Anyway, probably something we need to figure out, but irrelevant to this PR (making another issue for that).